Array copy set prep (#1515)

* Use correct llvm mem in matchArg.

* Change SMT solver for symbolic execution to Z3. Add timeout.

* Translate a SAWCore constant to a What4 constant in mkUninterpretedSAW, instead of an uninterpreted function without parameters.

* Add option for SAWCore to What4 translation for Crucible symbolic execution.

* Refactor SAWScript.Crucible.LLVM.X86.

* Add llvm_alloc_sym_init SAW command.

* Match arrays at non-zero offsets.

* Fix typo.

* Add W4EvalTactic newtype.

* Add LLVMAllocSpecInit datatype.

* Add set_crucible_timeout command.

* Edit changelog.

* Set crucible timeout in saw-remote-api.

* Handle llvm_alloc_sym_init in LLVM X86.

* Add disable_alloc_sym_init_check command.

* Improve documentation.

CHANGES.md

@@ -1,3 +1,19 @@
+# Nightly
+
+* New commands `enable_what4_eval` and `disable_what4_eval` to enable or
+  disable What4 translation for SAWCore expressions during Crucible symbolic
+  execution.
+
+* New command `llvm_alloc_sym_init` like `llvm_alloc`, but assume that the
+  allocation is initialized with symbolic bytes.  New commands
+  `disable_alloc_sym_init_check` and `enable_alloc_sym_init_check` to
+  disable or enable the allocation initialization check associated with
+  `llvm_alloc_sym_init` during override application.
+
+* New command `set_crucible_timeout` to set the timeout for the SMT solver
+  during the LLVM and X86 Crucible symbolic execution. This is used for
+  path-sat checks, and sat checks when applying overrides.
+
 # Version 0.9
 
 ## New Features

intTests/test0070_llvm_alloc_sym_init/test.c

@@ -0,0 +1,19 @@
+#include <stdlib.h>
+
+int f(int *x)
+{
+  return *x;
+}
+
+int test_f_calloc()
+{
+  int *x = (int *) calloc(1, sizeof(int));
+  return f(x);
+}
+
+int test_f_malloc()
+{
+  int *x = (int *) malloc(sizeof(int));
+  return f(x);
+}
+

intTests/test0070_llvm_alloc_sym_init/test.saw

@@ -0,0 +1,25 @@
+enable_experimental;
+
+m <- llvm_load_module "test.bc";
+
+let f_spec = do {
+  x_ptr <- llvm_alloc_sym_init (llvm_int 32);
+  llvm_execute_func [x_ptr];
+  x <- llvm_fresh_var "x" (llvm_int 32);
+  llvm_return (llvm_term x);
+};
+
+let test_spec = do {
+  llvm_execute_func [];
+  x <- llvm_fresh_var "x" (llvm_int 32);
+  llvm_return (llvm_term x);
+};
+
+f_ov <- llvm_verify m "f" [] false f_spec trivial;
+llvm_verify m "test_f_calloc" [f_ov] false test_spec trivial;
+fails (llvm_verify m "test_f_malloc" [f_ov] false test_spec trivial);
+disable_alloc_sym_init_check;
+llvm_verify m "test_f_malloc" [f_ov] false test_spec trivial;
+enable_alloc_sym_init_check;
+fails (llvm_verify m "test_f_malloc" [f_ov] false test_spec trivial);
+

intTests/test0070_llvm_alloc_sym_init/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

@@ -1320,21 +1320,21 @@ parseUninterpretedSAW sym st sc ref trm app ty =
               parseUninterpretedSAW sym st sc ref trm' app' t2
 
     VBoolType
-      -> VBool <$> mkUninterpretedSAW sym st ref trm app BaseBoolRepr
+      -> VBool <$> mkUninterpretedSAW sym st sc ref trm app BaseBoolRepr
 
     VIntType
-      -> VInt  <$> mkUninterpretedSAW sym st ref trm app BaseIntegerRepr
+      -> VInt  <$> mkUninterpretedSAW sym st sc ref trm app BaseIntegerRepr
 
     VIntModType n
-      -> VIntMod n <$> mkUninterpretedSAW sym st ref (ArgTermFromIntMod n trm) app BaseIntegerRepr
+      -> VIntMod n <$> mkUninterpretedSAW sym st sc ref (ArgTermFromIntMod n trm) app BaseIntegerRepr
 
     -- 0 width bitvector is a constant
     VVecType 0 VBoolType
       -> return $ VWord ZBV
 
     VVecType n VBoolType
       | Just (Some (PosNat w)) <- somePosNat n
-      -> (VWord . DBV) <$> mkUninterpretedSAW sym st ref trm app (BaseBVRepr w)
+      -> (VWord . DBV) <$> mkUninterpretedSAW sym st sc ref trm app (BaseBVRepr w)
 
     VVecType n ety | n >= 0
       ->  do ety' <- termOfTValue sc ety
@@ -1349,7 +1349,7 @@ parseUninterpretedSAW sym st sc ref trm app ty =
       | Just (Some idx_repr) <- valueAsBaseType ity
       , Just (Some elm_repr) <- valueAsBaseType ety
       -> (VArray . SArray) <$>
-          mkUninterpretedSAW sym st ref trm app (BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr)
+          mkUninterpretedSAW sym st sc ref trm app (BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr)
 
     VUnitType
       -> return VUnit
@@ -1367,12 +1367,16 @@ mkUninterpretedSAW ::
   forall n st fs t.
   B.ExprBuilder n st fs ->
   SAWCoreState n ->
+  SharedContext ->
   IORef (SymFnCache (B.ExprBuilder n st fs)) ->
   ArgTerm ->
   UnintApp (SymExpr (B.ExprBuilder n st fs)) ->
   BaseTypeRepr t ->
   IO (SymExpr (B.ExprBuilder n st fs) t)
-mkUninterpretedSAW sym st ref trm (UnintApp nm args tys) ret =
+mkUninterpretedSAW sym st sc ref trm (UnintApp nm args tys) ret
+  | Just Refl <- testEquality Ctx.empty tys =
+    bindSAWTerm sym st ret =<< reconstructArgTerm trm sc []
+  | otherwise =
   do fn <- mkSymFn sym ref nm tys ret
      sawRegisterSymFunInterp st fn (reconstructArgTerm trm)
      W.applySymFn sym fn args

saw-remote-api/src/SAWServer.hs

@@ -47,6 +47,7 @@ import Verifier.SAW.TypedTerm (TypedTerm, CryptolModule)
 
 import SAWScript.Crucible.LLVM.Builtins (CheckPointsToType)
 import SAWScript.Crucible.LLVM.X86 (defaultStackBaseAlign)
+import qualified SAWScript.Crucible.Common as CC (defaultSAWCoreBackendTimeout)
 import qualified SAWScript.Crucible.Common.MethodSpec as CMS (ProvedSpec, GhostGlobal)
 import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (SomeLLVM, LLVMModule)
 import SAWScript.Options (Options(..), processEnv, defaultOptions)
@@ -220,9 +221,12 @@ initialState readFileFn =
                 , rwDebugIntrinsics = True
                 , rwWhat4HashConsing = False
                 , rwWhat4HashConsingX86 = False
+                , rwWhat4Eval = False
                 , rwStackBaseAlign = defaultStackBaseAlign
                 , rwProofs = []
                 , rwPreservedRegs = []
+                , rwAllocSymInitCheck = True
+                , rwCrucibleTimeout = CC.defaultSAWCoreBackendTimeout
                 }
      return (SAWState emptyEnv bic [] ro rw M.empty)
 

src/SAWScript/Crucible/Common.hs

@@ -14,6 +14,8 @@ module SAWScript.Crucible.Common
   , setupProfiling
   , SAWCruciblePersonality(..)
   , newSAWCoreBackend
+  , newSAWCoreBackendWithTimeout
+  , defaultSAWCoreBackendTimeout
   , sawCoreState
   ) where
 
@@ -24,7 +26,8 @@ import           Lang.Crucible.Simulator.Profiling
 import           Lang.Crucible.Backend (AbortExecReason(..), ppAbortExecReason, IsSymInterface)
 import           Lang.Crucible.Backend.Online
 import qualified Data.Parameterized.Nonce as Nonce
-import qualified What4.Solver.Yices as Yices
+import qualified What4.Solver.Z3 as Z3
+import qualified What4.Protocol.SMTLib2 as SMT2
 import qualified What4.Config as W4
 import qualified What4.Expr as W4
 import qualified What4.Interface as W4
@@ -40,16 +43,24 @@ import Verifier.SAW.SharedTerm as SC
 import Verifier.SAW.Simulator.What4.ReturnTrip (SAWCoreState, newSAWCoreState)
 
 -- | The symbolic backend we use for SAW verification
-type Sym = OnlineBackendUserSt Nonce.GlobalNonceGenerator Yices.Connection SAWCoreState (W4.Flags W4.FloatReal)
+type Sym = OnlineBackendUserSt Nonce.GlobalNonceGenerator (SMT2.Writer Z3.Z3) SAWCoreState (W4.Flags W4.FloatReal)
 
 data SAWCruciblePersonality sym = SAWCruciblePersonality
 
 
 newSAWCoreBackend :: SC.SharedContext -> IO Sym
-newSAWCoreBackend sc =
+newSAWCoreBackend sc = newSAWCoreBackendWithTimeout sc 0
+
+defaultSAWCoreBackendTimeout :: Integer
+defaultSAWCoreBackendTimeout = 10000
+
+newSAWCoreBackendWithTimeout :: SC.SharedContext -> Integer -> IO Sym
+newSAWCoreBackendWithTimeout sc timeout =
   do st <- newSAWCoreState sc
-     sym <- newOnlineBackend W4.FloatRealRepr Nonce.globalNonceGenerator Yices.yicesDefaultFeatures st
-     W4.extendConfig Yices.yicesOptions (W4.getConfiguration sym)
+     sym <- newOnlineBackend W4.FloatRealRepr Nonce.globalNonceGenerator (SMT2.defaultFeatures Z3.Z3) st
+     W4.extendConfig Z3.z3Options (W4.getConfiguration sym)
+     z3TimeoutSetting <- W4.getOptionSetting Z3.z3Timeout (W4.getConfiguration sym)
+     _ <- W4.setOpt z3TimeoutSetting timeout
      return sym
 
 sawCoreState :: Sym -> IO (SAWCoreState Nonce.GlobalNonceGenerator)