Add overrides for llvm.prefetch{.p018} (#839)

Fixes #838.
GaloisInc · Sep 3, 2021 · e5d7499 · e5d7499
1 parent 5ec0854
commit e5d7499
Show file tree

Hide file tree

Showing 4 changed files with 39 additions and 0 deletions.
diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs
@@ -185,6 +185,9 @@ declare_overrides =
   , basic_llvm_override LLVM.llvmObjectsizeOverride_32_null_dynamic
   , basic_llvm_override LLVM.llvmObjectsizeOverride_64_null_dynamic
 
+  , basic_llvm_override LLVM.llvmPrefetchOverride
+  , basic_llvm_override LLVM.llvmPrefetchOverride_preLLVM10
+
   , basic_llvm_override LLVM.llvmStacksave
   , basic_llvm_override LLVM.llvmStackrestore
 

diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs
@@ -367,6 +367,36 @@ llvmObjectsizeOverride_64_null_dynamic =
   [llvmOvr| i64 @llvm.objectsize.i64.p0i8( i8*, i1, i1, i1 ) |]
   (\memOps sym args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic sym memOps knownNat) args)
 
+-- | This instruction is a hint to code generators, which means that it is a
+-- no-op for us.
+--
+-- <https://releases.llvm.org/12.0.0/docs/LangRef.html#llvm-prefetch-intrinsic LLVM docs>
+llvmPrefetchOverride ::
+  (IsSymInterface sym, HasPtrWidth wptr) =>
+  LLVMOverride p sym
+    (EmptyCtx ::> LLVMPointerType wptr ::> BVType 32 ::> BVType 32 ::> BVType 32)
+    UnitType
+llvmPrefetchOverride =
+  [llvmOvr| void @llvm.prefetch.p0i8( i8*, i32, i32, i32 ) |]
+  (\_memOps _sym _args -> pure ())
+
+-- | This instruction is a hint to code generators, which means that it is a
+-- no-op for us.
+--
+-- See also 'llvmPrefetchOverride'. This version exists for compatibility with
+-- pre-10 versions of LLVM, where llvm.prefetch always assumed that the first
+-- argument resides in address space 0.
+--
+-- <https://releases.llvm.org/12.0.0/docs/LangRef.html#llvm-prefetch-intrinsic LLVM docs>
+llvmPrefetchOverride_preLLVM10 ::
+  (IsSymInterface sym, HasPtrWidth wptr) =>
+  LLVMOverride p sym
+    (EmptyCtx ::> LLVMPointerType wptr ::> BVType 32 ::> BVType 32 ::> BVType 32)
+    UnitType
+llvmPrefetchOverride_preLLVM10 =
+  [llvmOvr| void @llvm.prefetch( i8*, i32, i32, i32 ) |]
+  (\_memOps _sym _args -> pure ())
+
 llvmFshl ::
   (1 <= w, IsSymInterface sym) =>
   NatRepr w ->

diff --git a/crux-llvm/test-data/golden/T838.c b/crux-llvm/test-data/golden/T838.c
@@ -0,0 +1,5 @@
+int main() {
+  int x = 0;
+  __builtin_prefetch(&x);
+  return x;
+}
diff --git a/crux-llvm/test-data/golden/T838.good b/crux-llvm/test-data/golden/T838.good
@@ -0,0 +1 @@
+[Crux] Overall status: Valid.