Array copy set test

s2nTests/docker/awslc.dockerfile

@@ -7,7 +7,7 @@ WORKDIR /saw-script
 RUN mkdir -p /saw-script && \
     git clone https://github.com/GaloisInc/aws-lc-verification.git && \
     cd aws-lc-verification && \
-    git checkout 7acbcfadd2e040b63cc33e8143e3f8e972408288 && \
+    git checkout f3af1103541e3ba4c27fa7f511a4b6311e34e62a && \
     git config --file=.gitmodules submodule.src.url https://github.com/awslabs/aws-lc && \
     git submodule sync && \
     git submodule update --init

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

@@ -222,6 +222,7 @@ initialState readFileFn =
                 , rwDebugIntrinsics = True
                 , rwWhat4HashConsing = False
                 , rwWhat4HashConsingX86 = False
+                , rwWhat4Eval = False
                 , rwStackBaseAlign = defaultStackBaseAlign
                 , rwProofs = []
                 , rwPreservedRegs = []

src/SAWScript/Crucible/Common.hs

@@ -24,7 +24,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 +41,18 @@ 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 =
   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 10000
      return sym
 
 sawCoreState :: Sym -> IO (SAWCoreState Nonce.GlobalNonceGenerator)

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -57,6 +57,7 @@ module SAWScript.Crucible.LLVM.Builtins
     , llvm_alloc_readonly
     , llvm_alloc_readonly_aligned
     , llvm_alloc_with_size
+    , llvm_alloc_sym_init
     , llvm_symbolic_alloc
     , llvm_alloc_global
     , llvm_fresh_expanded_val
@@ -156,6 +157,7 @@ import qualified Lang.Crucible.LLVM.Bytes as Crucible
 import qualified Lang.Crucible.LLVM.Intrinsics as Crucible
 import qualified Lang.Crucible.LLVM.MemModel as Crucible
 import qualified Lang.Crucible.LLVM.MemType as Crucible
+-- import qualified Lang.Crucible.LLVM.SimpleLoopFixpoint as Crucible
 import qualified Lang.Crucible.LLVM.Translation as Crucible
 
 import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible
@@ -487,7 +489,7 @@ withMethodSpec ::
   LLVMModule arch ->
   String            {- ^ Name of the function -} ->
   LLVMCrucibleSetupM () {- ^ Boundary specification -} ->
-  ((?lc :: Crucible.TypeContext, ?memOpts::Crucible.MemOptions, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
+  ((?lc :: Crucible.TypeContext, ?memOpts::Crucible.MemOptions, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
    LLVMCrucibleContext arch -> MS.CrucibleMethodSpecIR (LLVM arch) -> TopLevel a) ->
   TopLevel a
 withMethodSpec pathSat lm nm setup action =
@@ -533,6 +535,7 @@ withMethodSpec pathSat lm nm setup action =
 verifyMethodSpec ::
   ( ?lc :: Crucible.TypeContext
   , ?memOpts::Crucible.MemOptions
+  , ?doW4Eval :: Bool
   , Crucible.HasPtrWidth (Crucible.ArchWidth arch)
   , Crucible.HasLLVMAnn Sym
   ) =>
@@ -739,7 +742,7 @@ checkSpecReturnType cc mspec =
 -- Returns a tuple of (arguments, preconditions, pointer values,
 -- memory).
 verifyPrestate ::
-  (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
+  (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
   Options ->
   LLVMCrucibleContext arch ->
   MS.CrucibleMethodSpecIR (LLVM arch) ->
@@ -853,7 +856,7 @@ checkRegisterCompatibility mt mt' =
      return (st == st')
 
 resolveArguments ::
-  (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
+  (?lc :: Crucible.TypeContext, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
   LLVMCrucibleContext arch       ->
   Crucible.MemImpl Sym ->
   MS.CrucibleMethodSpecIR (LLVM arch)       ->
@@ -925,7 +928,7 @@ setupGlobalAllocs cc mspec mem0 = foldM go mem0 $ mspec ^. MS.csGlobalAllocs
 -- function spec, write the given value to the address of the given
 -- pointer.
 setupPrePointsTos :: forall arch.
-  (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
+  (?lc :: Crucible.TypeContext, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
   MS.CrucibleMethodSpecIR (LLVM arch)       ->
   Options ->
   LLVMCrucibleContext arch       ->
@@ -954,7 +957,7 @@ setupPrePointsTos mspec opts cc env pts mem0 = foldM go mem0 pts
 -- | Sets up globals (ghost variable), and collects boolean terms
 -- that should be assumed to be true.
 setupPrestateConditions ::
-  (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
+  (?lc :: Crucible.TypeContext, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
   MS.CrucibleMethodSpecIR (LLVM arch)        ->
   LLVMCrucibleContext arch        ->
   Crucible.MemImpl Sym ->
@@ -1007,20 +1010,19 @@ assertEqualVals cc v1 v2 =
 
 -- TODO(langston): combine with/move to executeAllocation
 doAlloc ::
-  (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
+  (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
   LLVMCrucibleContext arch       ->
   AllocIndex ->
   LLVMAllocSpec ->
   StateT MemImpl IO (LLVMPtr (Crucible.ArchWidth arch))
-doAlloc cc i (LLVMAllocSpec mut _memTy alignment sz loc fresh)
+doAlloc cc i (LLVMAllocSpec mut _memTy alignment sz loc fresh symSz)
   | fresh = liftIO $ executeFreshPointer cc i
   | otherwise =
   StateT $ \mem ->
   do let sym = cc^.ccBackend
      sz' <- liftIO $ resolveSAWSymBV cc Crucible.PtrWidth sz
      let l = show (W4.plSourceLoc loc)
-     liftIO $
-       Crucible.doMalloc sym Crucible.HeapAlloc mut l mem sz' alignment
+     liftIO $ doAllocSymInit sym mem mut alignment sz' l symSz
 
 --------------------------------------------------------------------------------
 
@@ -1045,6 +1047,7 @@ ppGlobalPair cc gp =
 registerOverride ::
   ( ?lc :: Crucible.TypeContext
   , ?memOpts::Crucible.MemOptions
+  , ?doW4Eval :: Bool
   , Crucible.HasPtrWidth wptr
   , wptr ~ Crucible.ArchWidth arch
   , Crucible.HasLLVMAnn Sym
@@ -1087,6 +1090,7 @@ registerOverride opts cc sim_ctx top_loc cs =
 registerInvariantOverride ::
   ( ?lc :: Crucible.TypeContext
   , ?memOpts::Crucible.MemOptions
+  , ?doW4Eval :: Bool
   , Crucible.HasPtrWidth (Crucible.ArchWidth arch)
   , Crucible.HasLLVMAnn Sym
   ) =>
@@ -1168,6 +1172,7 @@ withBreakpointCfgAndBlockId context name parent k =
 verifySimulate ::
   ( ?lc :: Crucible.TypeContext
   , ?memOpts::Crucible.MemOptions
+  , ?doW4Eval :: Bool
   , Crucible.HasPtrWidth wptr
   , wptr ~ Crucible.ArchWidth arch
   , Crucible.HasLLVMAnn Sym
@@ -1217,12 +1222,15 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat as
        (registerInvariantOverride opts cc top_loc (HashMap.fromList breakpoints))
        (groupOn (view csName) invLemmas)
 
+    --  simpleLoopFixpointFeature <- Crucible.simpleLoopFixpoint sym cfg undefined
+
      additionalFeatures <-
        mapM (Crucible.arraySizeProfile (ccLLVMContext cc)) $ maybeToList asp
 
      let execFeatures =
            invariantExecFeatures ++
            map Crucible.genericToExecutionFeature (patSatGenExecFeature ++ pfs) ++
+          --  (simpleLoopFixpointFeature : additionalFeatures)
            additionalFeatures
 
      let initExecState =
@@ -1287,6 +1295,7 @@ scAndList sc = conj . filter nontrivial
 verifyPoststate ::
   ( ?lc :: Crucible.TypeContext
   , ?memOpts::Crucible.MemOptions
+  , ?doW4Eval :: Bool
   , Crucible.HasPtrWidth wptr
   , wptr ~ Crucible.ArchWidth arch
   , Crucible.HasLLVMAnn Sym
@@ -1355,7 +1364,7 @@ verifyPoststate cc mspec env0 globals ret =
 setupLLVMCrucibleContext ::
   Bool {- ^ enable path sat checking -} ->
   LLVMModule arch ->
-  ((?lc :: Crucible.TypeContext, ?memOpts::Crucible.MemOptions, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
+  ((?lc :: Crucible.TypeContext, ?memOpts::Crucible.MemOptions, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
    LLVMCrucibleContext arch -> TopLevel a) ->
   TopLevel a
 setupLLVMCrucibleContext pathSat lm action =
@@ -1370,6 +1379,7 @@ setupLLVMCrucibleContext pathSat lm action =
      crucible_assert_then_assume_enabled <- gets rwCrucibleAssertThenAssume
      what4HashConsing <- gets rwWhat4HashConsing
      laxPointerOrdering <- gets rwLaxPointerOrdering
+     what4Eval <- gets rwWhat4Eval
      Crucible.llvmPtrWidth ctx $ \wptr ->
        Crucible.withPtrWidth wptr $
        do let ?lc = ctx^.Crucible.llvmTypeCtx
@@ -1378,6 +1388,7 @@ setupLLVMCrucibleContext pathSat lm action =
                           }
           let ?intrinsicsOpts = Crucible.defaultIntrinsicsOptions
           let ?recordLLVMAnnotation = \_ _ -> return ()
+          let ?doW4Eval = what4Eval
           cc <-
             io $
             do let verbosity = simVerbose opts
@@ -1866,9 +1877,10 @@ llvm_alloc_with_mutability_and_size ::
   Crucible.Mutability    ->
   Maybe (Crucible.Bytes) ->
   Maybe Crucible.Alignment ->
+  Bool ->
   L.Type           ->
   LLVMCrucibleSetupM (AllLLVM SetupValue)
-llvm_alloc_with_mutability_and_size mut sz alignment lty =
+llvm_alloc_with_mutability_and_size mut sz alignment symSz lty =
   LLVMCrucibleSetupM $
   do cctx <- getLLVMCrucibleContext
      loc <- getW4Position "llvm_alloc"
@@ -1913,13 +1925,14 @@ llvm_alloc_with_mutability_and_size mut sz alignment lty =
        , _allocSpecBytes = sz''
        , _allocSpecLoc = loc
        , _allocSpecFresh = False
+       , _allocSpecSymSz = symSz
        }
 
 llvm_alloc ::
   L.Type         ->
   LLVMCrucibleSetupM (AllLLVM SetupValue)
 llvm_alloc =
-  llvm_alloc_with_mutability_and_size Crucible.Mutable Nothing Nothing
+  llvm_alloc_with_mutability_and_size Crucible.Mutable Nothing Nothing False
 
 llvm_alloc_aligned ::
   Int            ->
@@ -1932,7 +1945,7 @@ llvm_alloc_readonly ::
   L.Type         ->
   LLVMCrucibleSetupM (AllLLVM SetupValue)
 llvm_alloc_readonly =
-  llvm_alloc_with_mutability_and_size Crucible.Immutable Nothing Nothing
+  llvm_alloc_with_mutability_and_size Crucible.Immutable Nothing Nothing False
 
 llvm_alloc_readonly_aligned ::
   Int            ->
@@ -1952,6 +1965,7 @@ llvm_alloc_aligned_with_mutability mut n lty =
        mut
        Nothing
        (Just alignment)
+       False
        lty
 
 coerceAlignment :: Int -> CrucibleSetup (LLVM arch) Crucible.Alignment
@@ -1975,8 +1989,12 @@ llvm_alloc_with_size sz lty =
     Crucible.Mutable
     (Just (Crucible.toBytes sz))
     Nothing
+    False
     lty
 
+llvm_alloc_sym_init :: L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue)
+llvm_alloc_sym_init = llvm_alloc_with_mutability_and_size Crucible.Mutable Nothing Nothing True
+
 llvm_symbolic_alloc ::
   Bool ->
   Int ->
@@ -2008,6 +2026,7 @@ llvm_symbolic_alloc ro align_bytes sz =
            , _allocSpecBytes = sz
            , _allocSpecLoc = loc
            , _allocSpecFresh = False
+           , _allocSpecSymSz = False
            }
      n <- Setup.csVarCounter <<%= nextAllocIndex
      Setup.currentState . MS.csAllocs . at n ?= spec
@@ -2057,6 +2076,7 @@ constructFreshPointer mid loc memTy =
                      , _allocSpecBytes = sz
                      , _allocSpecLoc = loc
                      , _allocSpecFresh = True
+                     , _allocSpecSymSz = False
                      }
      -- TODO: refactor
      case mid of

src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

@@ -45,6 +45,7 @@ module SAWScript.Crucible.LLVM.MethodSpecIR
   , allocSpecLoc
   , allocSpecBytes
   , allocSpecFresh
+  , allocSpecSymSz
   , mutIso
   , isMut
     -- * LLVMModule
@@ -196,6 +197,7 @@ data LLVMAllocSpec =
     , _allocSpecBytes :: Term
     , _allocSpecLoc   :: ProgramLoc
     , _allocSpecFresh :: Bool -- ^ Whether declared with @crucible_fresh_pointer@
+    , _allocSpecSymSz :: Bool
     }
   deriving (Eq, Show)