From b6c188128c27647e611afd77c612336a2a682e0d Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 20 Sep 2021 10:21:36 -0400
Subject: [PATCH] crux-llvm: Add some missing __VERIFIER_nondet_* overrides

This adds `crux-llvm` overrides for the `u8`, `u16`, `u32`,
`unsigned`, `size_t`, `loff_t`, and `longlong` variants of
`__VERIFIER_nondet_*`.

This checks off several boxes in #842.
---
 crux-llvm/src/Crux/LLVM/Overrides.hs | 33 ++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/crux-llvm/src/Crux/LLVM/Overrides.hs b/crux-llvm/src/Crux/LLVM/Overrides.hs
index d115973da..256703fa9 100644
--- a/crux-llvm/src/Crux/LLVM/Overrides.hs
+++ b/crux-llvm/src/Crux/LLVM/Overrides.hs
@@ -251,6 +251,19 @@ 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)
 
@@ -258,6 +271,14 @@ svCompOverrides =
         [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)