Merge pull request #858 from GaloisInc/T842

`crux-llvm`: Add some missing `__VERIFIER_nondet_*` overrides
GaloisInc · Sep 20, 2021 · 00a69d9 · 00a69d9
2 parents 0498a53 + b6c1881
commit 00a69d9
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 2 deletions.
diff --git a/crux-llvm/crux-llvm.cabal b/crux-llvm/crux-llvm.cabal
@@ -89,7 +89,7 @@ library
   build-depends:
     aeson,
     bv-sized,
-    config-schema,
+    config-schema >= 1.2.2.0,
     data-binary-ieee754,
     logict,
     llvm-pretty,

diff --git a/crux-llvm/src/Crux/LLVM/Overrides.hs b/crux-llvm/src/Crux/LLVM/Overrides.hs
@@ -251,13 +251,34 @@ svCompOverrides ::
   [OverrideTemplate (personality sym) sym arch rtp l a]
 svCompOverrides =
   [ basic_llvm_override $
+        [llvmOvr| i64 @__VERIFIER_nondet_longlong() |]
+        (sv_comp_fresh_bits (knownNat @64))
+
+    -- loff_t is pretty Linux-specific, so we can't point to the C or POSIX
+    -- standards for justification about what size it should be. The man page
+    -- for lseek64 (https://linux.die.net/man/3/lseek64) is as close to a
+    -- definitive reference for this as I can find, which says
+    -- "The type loff_t is a 64-bit signed type".
+  , basic_llvm_override $
+        [llvmOvr| i64 @__VERIFIER_nondet_loff_t() |]
+        (sv_comp_fresh_bits (knownNat @64))
+
+  , basic_llvm_override $
         [llvmOvr| size_t @__VERIFIER_nondet_ulong() |]
         (sv_comp_fresh_bits ?ptrWidth)
 
   , basic_llvm_override $
         [llvmOvr| size_t @__VERIFIER_nondet_long() |]
         (sv_comp_fresh_bits ?ptrWidth)
 
+  , basic_llvm_override $
+        [llvmOvr| i32 @__VERIFIER_nondet_unsigned() |]
+        (sv_comp_fresh_bits (knownNat @32))
+
+  , basic_llvm_override $
+        [llvmOvr| i32 @__VERIFIER_nondet_u32() |]
+        (sv_comp_fresh_bits (knownNat @32))
+
   , basic_llvm_override $
         [llvmOvr| i32 @__VERIFIER_nondet_uint() |]
         (sv_comp_fresh_bits (knownNat @32))
@@ -266,6 +287,10 @@ svCompOverrides =
         [llvmOvr| i32 @__VERIFIER_nondet_int() |]
         (sv_comp_fresh_bits (knownNat @32))
 
+  , basic_llvm_override $
+        [llvmOvr| i16 @__VERIFIER_nondet_u16() |]
+        (sv_comp_fresh_bits (knownNat @16))
+
   , basic_llvm_override $
         [llvmOvr| i16 @__VERIFIER_nondet_ushort() |]
         (sv_comp_fresh_bits (knownNat @16))
@@ -274,6 +299,10 @@ svCompOverrides =
         [llvmOvr| i16 @__VERIFIER_nondet_short() |]
         (sv_comp_fresh_bits (knownNat @16))
 
+  , basic_llvm_override $
+        [llvmOvr| i8 @__VERIFIER_nondet_u8() |]
+        (sv_comp_fresh_bits (knownNat @8))
+
   , basic_llvm_override $
         [llvmOvr| i8 @__VERIFIER_nondet_uchar() |]
         (sv_comp_fresh_bits (knownNat @8))
@@ -286,6 +315,10 @@ svCompOverrides =
         [llvmOvr| i1 @__VERIFIER_nondet_bool() |]
         (sv_comp_fresh_bits (knownNat @1))
 
+  , basic_llvm_override $
+        [llvmOvr| size_t @__VERIFIER_nondet_size_t() |]
+        (sv_comp_fresh_bits ?ptrWidth)
+
   , basic_llvm_override $
         [llvmOvr| float @__VERIFIER_nondet_float() |]
         (sv_comp_fresh_float SingleFloatRepr)

diff --git a/crux/crux.cabal b/crux/crux.cabal
@@ -54,7 +54,7 @@ library
     raw-strings-qq,
     simple-get-opt,
     config-value,
-    config-schema,
+    config-schema >= 1.2.2.0,
     semigroupoids,
     unordered-containers,
     xml,