Find SMT array write of a fixed size.

intTests/test_smt_array_load_concrete_size/Makefile

@@ -0,0 +1,11 @@
+CC = clang
+CFLAGS = -g -emit-llvm -frecord-command-line -O1
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc

intTests/test_smt_array_load_concrete_size/Mix.cry

@@ -0,0 +1,8 @@
+module Mix where
+
+import Array
+
+type ByteArray = Array[64][8]
+
+mix : {l} (width l <= 64) => ByteArray -> [64] -> [l][8] -> ByteArray
+mix block n data = arrayCopy block n (arrayRangeUpdate (arrayConstant 0) 0 data) 0 `(l)

intTests/test_smt_array_load_concrete_size/test.c

@@ -0,0 +1,13 @@
+#include <stdint.h>
+#include <string.h>
+
+int mix(uint8_t block[128], uint32_t n, uint8_t *data, size_t len) {
+  size_t left = 128 - n;
+
+  if (len < left) {
+    memcpy(block + n, data, len);
+  } else {
+    memcpy(block + n, data, left);
+  }
+  return 1;
+}

intTests/test_smt_array_load_concrete_size/test.saw

@@ -0,0 +1,66 @@
+enable_experimental;
+
+import "Mix.cry";
+let arrayRangeEq = parse_core "arrayRangeEq 64 (Vec 8 Bool)";
+
+m <- llvm_load_module "test.bc";
+
+let i8 = llvm_int 8;
+let i32 = llvm_int 32;
+
+let alloc_init_readonly ty v = do {
+  p <- llvm_alloc_readonly ty;
+  llvm_points_to p v;
+  return p;
+};
+
+let ptr_to_fresh_readonly n ty = do {
+  x <- llvm_fresh_var n ty;
+  p <- alloc_init_readonly ty (llvm_term x);
+  return (x, p);
+};
+
+let mix_spec len res_block_len range_eq_len = do {
+  block <- llvm_fresh_cryptol_var "block" {| ByteArray |};
+  block_ptr <- llvm_symbolic_alloc false 1 {{ 128:[64] }};
+  llvm_points_to_array_prefix block_ptr block {{ 128:[64] }};
+
+  (data, data_ptr) <- ptr_to_fresh_readonly "data" (llvm_array len i8);
+
+  n <- llvm_fresh_var "n" i32;
+  llvm_precond({{ n < 128 }});
+
+  llvm_execute_func [block_ptr, (llvm_term n), data_ptr, (llvm_term {{ `len : [64] }})];
+
+  let res = {{ mix block (0 # n) data }};
+  res_block <- llvm_fresh_cryptol_var "res_block" {| ByteArray |};
+  llvm_points_to_array_prefix block_ptr res_block {{ `res_block_len:[64] }};
+  llvm_postcond {{ arrayRangeEq res_block 0 res 0 `range_eq_len }};
+
+  llvm_return (llvm_term {{ 1 : [32]}});
+};
+
+llvm_verify m "mix"
+  []
+  true
+  (mix_spec 1 128 128)
+  (do {
+    w4_unint_z3 [];
+  });
+
+llvm_verify m "mix"
+  []
+  true
+  (mix_spec 1 0 0)
+  (do {
+    w4_unint_z3 [];
+  });
+
+fails (llvm_verify m "mix"
+  []
+  true
+  (mix_spec 1 129 0)
+  (do {
+    w4_unint_z3 [];
+  }));
+

intTests/test_smt_array_load_concrete_size/test.sh

@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+
+set -e
+
+$SAW test.saw
+

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -1756,6 +1756,7 @@ setupLLVMCrucibleContext pathSat lm action =
           let ?memOpts = Crucible.defaultMemOptions
                           { Crucible.laxPointerOrdering = laxPointerOrdering
                           , Crucible.laxLoadsAndStores = laxLoadsAndStores
+                          , Crucible.noSatisfyingWriteFreshConstant = False
                           }
           let ?intrinsicsOpts = Crucible.defaultIntrinsicsOptions
           let ?recordLLVMAnnotation = \_ _ _ -> return ()

src/SAWScript/Crucible/LLVM/Override.hs

@@ -119,6 +119,7 @@ import qualified Data.BitVector.Sized as BV
 import           Verifier.SAW.SharedTerm
 import           Verifier.SAW.Recognizer
 import           Verifier.SAW.TypedTerm
+import           Verifier.SAW.Simulator.TermModel
 import           Verifier.SAW.Simulator.What4.ReturnTrip (SAWCoreState(..), toSC, bindSAWTerm)
 
 import           SAWScript.Crucible.Common
@@ -1485,7 +1486,34 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val =
 
                    return Nothing
 
-              _ -> return $ Just errMsg
+              _ ->
+                do sub <- OM (use termSub)
+                   modmap <- liftIO $ scGetModuleMap sc
+                   instantiated_expected_sz_tm <- liftIO $ scInstantiateExt sc sub $ ttTerm expected_sz_tm
+                   normalized_expected_sz_tm <- liftIO $
+                     normalizeSharedTerm sc modmap mempty mempty mempty instantiated_expected_sz_tm
+                   case asUnsignedConcreteBv normalized_expected_sz_tm of
+                     Just sz_nat ->
+                       do sz_bv <- liftIO $
+                            W4.bvLit sym Crucible.PtrWidth $ BV.mkBV Crucible.PtrWidth $ fromIntegral sz_nat
+                          maybe_matching_array <- liftIO $
+                            Crucible.asMemMatchingArrayStore sym Crucible.PtrWidth ptr sz_bv (Crucible.memImplHeap mem)
+                          res <- case maybe_matching_array of
+                            Just (ok, arr) -> return $ Right (ok, arr)
+                            Nothing -> liftIO $ Crucible.loadArrayConcreteSizeRaw sym mem ptr sz_nat alignment
+
+                          case res of
+                            Right (ok, arr) ->
+                              do addAssert ok md $ Crucible.SimError loc $ Crucible.GenericSimError $ show errMsg
+                                 st <- liftIO (sawCoreState sym)
+                                 arr_tm <- liftIO $ toSC sym st arr
+                                 instantiateExtMatchTerm sc md prepost arr_tm $ ttTerm expected_arr_tm
+                                 return Nothing
+
+                            Left{} -> return $ Just errMsg
+
+                     Nothing -> return $ Just errMsg
+
 
 -- | Like 'matchPointsToValue', but specifically geared towards the needs
 -- of fields within bitfields. In particular, this performs all of the

src/SAWScript/Crucible/LLVM/X86.hs

@@ -375,6 +375,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
       let ?ptrWidth = knownNat @64
       let ?memOpts = C.LLVM.defaultMemOptions
                        { C.LLVM.laxLoadsAndStores = laxLoadsAndStores
+                       , C.LLVM.noSatisfyingWriteFreshConstant = False
                        }
       let ?recordLLVMAnnotation = \_ _ _ -> return ()
       sc <- getSharedContext