diff --git a/deps/crucible b/deps/crucible index 05a4e082e6..542e54a49e 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 05a4e082e6a29e81d75babba9f5918863c5f65ee +Subproject commit 542e54a49e9457f4d1e81f7604532e53f3e98deb diff --git a/deps/what4 b/deps/what4 index 26ce30ef10..53d1f9055a 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit 26ce30ef102d517270212e7c5e98f6ee80dd1037 +Subproject commit 53d1f9055a9b3e7ddfdce1ab866cc28614c042d6 diff --git a/s2nTests/docker/awslc.dockerfile b/s2nTests/docker/awslc.dockerfile index 7f5267fb45..76199684f6 100644 --- a/s2nTests/docker/awslc.dockerfile +++ b/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 diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index cd58c24f62..8e106a03ae 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -1320,13 +1320,13 @@ 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 @@ -1334,7 +1334,7 @@ parseUninterpretedSAW sym st sc ref trm app ty = 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 diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 66c93c1e2d..36f5dcc753 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -220,6 +220,7 @@ initialState readFileFn = , rwDebugIntrinsics = True , rwWhat4HashConsing = False , rwWhat4HashConsingX86 = False + , rwWhat4Eval = False , rwStackBaseAlign = defaultStackBaseAlign , rwProofs = [] , rwPreservedRegs = [] diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs index 45f9681972..b3286da571 100644 --- a/src/SAWScript/Crucible/Common.hs +++ b/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,7 +41,7 @@ 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 @@ -48,8 +49,10 @@ 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) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 70252b74d5..6d2bfd49c0 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/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 diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index d82f3146f0..0e9940e33f 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/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) diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 398a0a15a8..2fd383e45f 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -45,6 +45,7 @@ module SAWScript.Crucible.LLVM.Override , methodSpecHandler , valueToSC , storePointsToValue + , doAllocSymInit , diffMemTypes @@ -158,7 +159,7 @@ ppLLVMVal cc val = do -- | Resolve a 'SetupValue' into a 'LLVMVal' and pretty-print it ppSetupValueAsLLVMVal :: - (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options {- ^ output/verbosity options -} -> LLVMCrucibleContext arch -> SharedContext {- ^ context for constructing SAW terms -} -> @@ -194,7 +195,7 @@ mkStructuralMismatch _opts cc _sc spec llvmval setupval memTy = -- | Instead of using 'ppPointsTo', which prints 'SetupValue', translate -- expressions to 'LLVMVal'. ppPointsToAsLLVMVal :: - (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options {- ^ output/verbosity options -} -> LLVMCrucibleContext arch -> SharedContext {- ^ context for constructing SAW terms -} -> @@ -213,7 +214,7 @@ ppPointsToAsLLVMVal opts cc sc spec (LLVMPointsTo loc cond ptr val) = do -- | Create an error stating that the 'LLVMVal' was not equal to the 'SetupValue' notEqual :: - (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => PrePost -> Options {- ^ output/verbosity options -} -> W4.ProgramLoc {- ^ where is the assertion from? -} -> @@ -370,6 +371,7 @@ methodSpecHandler :: forall arch rtp args ret. ( ?lc :: Crucible.TypeContext , ?memOpts::Crucible.MemOptions + , ?doW4Eval :: Bool , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -592,6 +594,7 @@ methodSpecHandler_prestate :: forall arch ctx. ( ?lc :: Crucible.TypeContext , ?memOpts::Crucible.MemOptions + , ?doW4Eval :: Bool , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -626,7 +629,7 @@ methodSpecHandler_prestate opts sc cc args cs = -- and computing postcondition predicates. methodSpecHandler_poststate :: forall arch ret. - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + (?lc :: Crucible.TypeContext, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => Options {- ^ output/verbosity options -} -> SharedContext {- ^ context for constructing SAW terms -} -> LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} -> @@ -641,6 +644,7 @@ methodSpecHandler_poststate opts sc cc retTy cs = learnCond :: ( ?lc :: Crucible.TypeContext , ?memOpts::Crucible.MemOptions + , ?doW4Eval :: Bool , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -664,6 +668,7 @@ learnCond opts sc cc cs prepost globals extras ss = assertTermEqualities :: + (?doW4Eval :: Bool) => SharedContext -> LLVMCrucibleContext arch -> OverrideMatcher (LLVM arch) md () @@ -696,7 +701,7 @@ enforceCompleteSubstitution loc ss = -- execute a pre/post condition -executeCond :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) +executeCond :: (?lc :: Crucible.TypeContext, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => Options -> SharedContext -> LLVMCrucibleContext arch @@ -734,7 +739,7 @@ refreshTerms sc ss = -- override's precondition are allocated, and meet the appropriate -- requirements for alignment and mutability. enforcePointerValidity :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => SharedContext -> LLVMCrucibleContext arch -> W4.ProgramLoc -> @@ -763,7 +768,7 @@ enforcePointerValidity sc cc loc ss = addAssert c $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" - | (LLVMAllocSpec mut _pty alignment psz _ploc fresh, ptr) <- mems + | (LLVMAllocSpec mut _pty alignment psz _ploc fresh _sym_sz, ptr) <- mems , not fresh -- Fresh symbolic pointers are not assumed to be valid; don't check them ] @@ -773,7 +778,7 @@ enforcePointerValidity sc cc loc ss = -- an override's precondition are disjoint. Read-only allocations are -- allowed to alias other read-only allocations, however. enforceDisjointness :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => SharedContext -> LLVMCrucibleContext arch -> W4.ProgramLoc -> @@ -815,7 +820,7 @@ enforceDisjointness sc cc loc globals extras ss = -- not be disjoint. Similarly, fresh pointers need not be checked for -- disjointness. enforceDisjointAllocSpec :: - (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => SharedContext -> LLVMCrucibleContext arch -> Sym -> W4.ProgramLoc -> @@ -823,8 +828,8 @@ enforceDisjointAllocSpec :: (LLVMAllocSpec, LLVMPtr (Crucible.ArchWidth arch)) -> OverrideMatcher (LLVM arch) md () enforceDisjointAllocSpec sc cc sym loc - (LLVMAllocSpec pmut _pty _palign psz ploc pfresh, p) - (LLVMAllocSpec qmut _qty _qalign qsz qloc qfresh, q) + (LLVMAllocSpec pmut _pty _palign psz ploc pfresh _p_sym_sz, p) + (LLVMAllocSpec qmut _qty _qalign qsz qloc qfresh _q_sym_sz, q) | (pmut, qmut) == (Crucible.Immutable, Crucible.Immutable) = pure () -- Read-only allocations may alias each other | pfresh || qfresh = @@ -856,7 +861,7 @@ enforceDisjointAllocGlobal :: (LLVMAllocGlobal arch, LLVMPtr (Crucible.ArchWidth arch)) -> OverrideMatcher (LLVM arch) md () enforceDisjointAllocGlobal sym loc - (LLVMAllocSpec _pmut _pty _palign psz ploc _pfresh, p) + (LLVMAllocSpec _pmut _pty _palign psz ploc _pfresh _p_sym_sz, p) (LLVMAllocGlobal qloc (L.Symbol qname), q) = do let Crucible.LLVMPointer pblk _ = p let Crucible.LLVMPointer qblk _ = q @@ -885,6 +890,7 @@ ppProgramLoc loc = matchPointsTos :: forall arch md. ( ?lc :: Crucible.TypeContext , ?memOpts :: Crucible.MemOptions + , ?doW4Eval :: Bool , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -952,7 +958,7 @@ matchPointsTos opts sc cc spec prepost = go False [] ------------------------------------------------------------------------ computeReturnValue :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options {- ^ saw script debug and print options -} -> LLVMCrucibleContext arch {- ^ context of the crucible simulation -} -> SharedContext {- ^ context for generating saw terms -} -> @@ -1071,6 +1077,7 @@ diffMemTypesList i ((x, y) : ts) = -- | Match the value of a function argument with a symbolic 'SetupValue'. matchArg :: + (?doW4Eval :: Bool) => Options {- ^ saw script print out opts -} -> Crucible.HasPtrWidth (Crucible.ArchWidth arch) => SharedContext {- ^ context for constructing SAW terms -} -> @@ -1084,10 +1091,7 @@ matchArg :: OverrideMatcher (LLVM arch) md () matchArg opts sc cc cs prepost actual expectedTy expected = do - let mvar = Crucible.llvmMemVar (ccLLVMContext cc) - mem <- case Crucible.lookupGlobal mvar $ cc ^. ccLLVMGlobals of - Nothing -> fail "internal error: LLVM Memory global not found" - Just mem -> pure mem + mem <- readGlobal $ Crucible.llvmMemVar $ ccLLVMContext cc case (actual, expectedTy, expected) of (_, _, SetupTerm expectedTT) | TypedTermSchema (Cryptol.Forall [] [] tyexpr) <- ttType expectedTT @@ -1301,7 +1305,7 @@ matchTerm sc cc loc prepost real expect = -- | Use the current state to learn about variable assignments based on -- preconditions for a procedure specification. learnSetupCondition :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> LLVMCrucibleContext arch -> @@ -1353,6 +1357,7 @@ learnPointsTo :: forall arch md ann. ( ?lc :: Crucible.TypeContext , ?memOpts :: Crucible.MemOptions + , ?doW4Eval :: Bool , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -1438,14 +1443,36 @@ learnPointsTo opts sc cc spec prepost (LLVMPointsTo loc maybe_cond ptr val) = ] case maybe_allocation_array of Just (ok, arr, sz) - | Crucible.LLVMPointer _ off <- ptr1 - , Just 0 <- BV.asUnsigned <$> W4.asBV off -> + | Crucible.LLVMPointer _ off <- ptr1 -> do addAssert ok $ Crucible.SimError loc $ Crucible.GenericSimError $ show errMsg + sub <- OM (use termSub) st <- liftIO (sawCoreState sym) - arr_tm <- liftIO $ toSC sym st arr - instantiateExtMatchTerm sc cc (spec ^. MS.csLoc) prepost arr_tm (ttTerm expected_arr_tm) + + ptr_width_tm <- liftIO $ scNat sc $ natValue ?ptrWidth + off_type_tm <- liftIO $ scBitvector sc $ natValue ?ptrWidth + off_tm <- liftIO $ toSC sym st off + foo_arr_tm <- liftIO $ toSC sym st arr + + arr_tm <- liftIO $ case BV.asUnsigned <$> W4.asBV off of + Just 0 -> return foo_arr_tm + _ -> + do byte_width_tm <- scNat sc 8 + byte_type_tm <- scBitvector sc 8 + + zero_off_tm <- scBvNat sc ptr_width_tm =<< scNat sc 0 + zero_byte_tm <- scBvNat sc byte_width_tm =<< scNat sc 0 + zero_arr_const_tm <- scArrayConstant sc off_type_tm byte_type_tm zero_byte_tm + + instantiated_expected_sz_tm <- scInstantiateExt sc sub $ ttTerm expected_sz_tm + scArrayCopy sc ptr_width_tm byte_type_tm zero_arr_const_tm zero_off_tm foo_arr_tm off_tm instantiated_expected_sz_tm + + instantiateExtMatchTerm sc cc loc prepost arr_tm (ttTerm expected_arr_tm) + sz_tm <- liftIO $ toSC sym st sz - instantiateExtMatchTerm sc cc (spec ^. MS.csLoc) prepost sz_tm (ttTerm expected_sz_tm) + foo_tm <- liftIO $ scBvAdd sc ptr_width_tm off_tm (ttTerm expected_sz_tm) + bar_tm <- liftIO $ scBvULe sc ptr_width_tm foo_tm sz_tm + learnPred sc cc loc prepost bar_tm + return Nothing _ -> return $ Just errMsg @@ -1459,7 +1486,7 @@ stateCond PostState = "postcondition" -- | Process an @llvm_equal@ statement from the precondition -- section of the CrucibleSetup block. learnEqual :: - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> LLVMCrucibleContext arch -> @@ -1479,6 +1506,7 @@ learnEqual opts sc cc spec loc prepost v1 v2 = do -- | Process an @llvm_precond@ statement from the precondition -- section of the CrucibleSetup block. learnPred :: + (?doW4Eval :: Bool) => SharedContext -> LLVMCrucibleContext arch -> W4.ProgramLoc -> @@ -1490,6 +1518,7 @@ learnPred sc cc loc prepost t = addAssert p (Crucible.SimError loc (Crucible.AssertFailureSimError (stateCond prepost) "")) instantiateExtResolveSAWPred :: + (?doW4Eval :: Bool) => SharedContext -> LLVMCrucibleContext arch -> Term -> @@ -1499,7 +1528,7 @@ instantiateExtResolveSAWPred sc cc cond = do liftIO $ resolveSAWPred cc =<< scInstantiateExt sc sub cond instantiateExtResolveSAWSymBV :: - (1 <= w) => + (?doW4Eval :: Bool, 1 <= w) => SharedContext -> LLVMCrucibleContext arch -> NatRepr w -> @@ -1518,6 +1547,7 @@ instantiateExtResolveSAWSymBV sc cc w tm = do -- Return a map containing the overwritten memory allocations. invalidateMutableAllocs :: ( ?lc :: Crucible.TypeContext + , ?doW4Eval :: Bool , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -1609,13 +1639,13 @@ invalidateMutableAllocs opts sc cc cs = do -- | Perform an allocation as indicated by an @llvm_alloc@ or -- @llvm_fresh_pointer@ statement from the postcondition section. executeAllocation :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => Options -> SharedContext -> LLVMCrucibleContext arch -> (AllocIndex, LLVMAllocSpec) -> OverrideMatcher (LLVM arch) RW () -executeAllocation opts sc cc (var, LLVMAllocSpec mut memTy alignment sz loc fresh) +executeAllocation opts sc cc (var, LLVMAllocSpec mut memTy alignment sz loc fresh symSz) | fresh = do ptr <- liftIO $ executeFreshPointer cc var OM (setupValueSub %= Map.insert var ptr) @@ -1631,17 +1661,38 @@ executeAllocation opts sc cc (var, LLVMAllocSpec mut memTy alignment sz loc fres mem <- readGlobal memVar sz' <- instantiateExtResolveSAWSymBV sc cc Crucible.PtrWidth sz let l = show (W4.plSourceLoc loc) ++ " (Poststate)" - (ptr, mem') <- liftIO $ - Crucible.doMalloc sym Crucible.HeapAlloc mut l mem sz' alignment + (ptr, mem') <- liftIO $ doAllocSymInit sym mem mut alignment sz' l symSz writeGlobal memVar mem' assignVar cc loc var ptr +doAllocSymInit :: + (Crucible.IsSymInterface sym, Crucible.HasPtrWidth wptr, Crucible.HasLLVMAnn sym) => + sym -> + Crucible.MemImpl sym -> + Crucible.Mutability -> + Crucible.Alignment -> + W4.SymBV sym wptr {- ^ allocation size -} -> + String {- ^ source location for use in error messages -} -> + Bool {- ^ source location for use in error messages -} -> + IO (Crucible.LLVMPtr sym wptr, Crucible.MemImpl sym) +doAllocSymInit sym mem mut alignment sz loc symSz = do + (ptr, mem') <- Crucible.doMalloc sym Crucible.HeapAlloc mut loc mem sz alignment + mem'' <- if symSz then do + arr <- W4.freshConstant + sym + (W4.systemSymbol "arr!") + (W4.BaseArrayRepr (Ctx.singleton $ W4.BaseBVRepr ?ptrWidth) (W4.BaseBVRepr (W4.knownNat @8))) + Crucible.doArrayConstStore sym mem' ptr alignment arr sz + else + return mem' + return (ptr, mem'') + ------------------------------------------------------------------------ -- | Update the simulator state based on the postconditions from the -- procedure specification. executeSetupCondition :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> LLVMCrucibleContext arch -> @@ -1680,7 +1731,7 @@ executeGhost _sc _var (TypedTerm tp _) = -- the CrucibleSetup block. First we compute the value indicated by -- 'val', and then write it to the address indicated by 'ptr'. executePointsTo :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + (?lc :: Crucible.TypeContext, ?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => Options -> SharedContext -> LLVMCrucibleContext arch -> @@ -1711,7 +1762,7 @@ executePointsTo opts sc cc spec overwritten_allocs (LLVMPointsTo _loc cond ptr v writeGlobal memVar mem' storePointsToValue :: - (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => Options -> LLVMCrucibleContext arch -> Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> @@ -1797,7 +1848,7 @@ storePointsToValue opts cc env tyenv nameEnv base_mem maybe_cond ptr val maybe_i -- | Process an @llvm_equal@ statement from the postcondition -- section of the CrucibleSetup block. executeEqual :: - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> LLVMCrucibleContext arch -> @@ -1814,6 +1865,7 @@ executeEqual opts sc cc spec v1 v2 = do -- | Process an @llvm_postcond@ statement from the postcondition -- section of the CrucibleSetup block. executePred :: + (?doW4Eval :: Bool) => SharedContext -> LLVMCrucibleContext arch -> TypedTerm {- ^ the term to assert as a postcondition -} -> @@ -1863,7 +1915,7 @@ instantiateSetupValue sc s v = ------------------------------------------------------------------------ resolveSetupValueLLVM :: - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> LLVMCrucibleContext arch -> SharedContext -> @@ -1882,7 +1934,7 @@ resolveSetupValueLLVM opts cc sc spec sval = return (memTy, lval) resolveSetupValue :: - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> LLVMCrucibleContext arch -> SharedContext -> diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index 333347729c..2ce323242a 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -39,6 +39,7 @@ import Data.Maybe (fromMaybe, listToMaybe, fromJust) import Data.Map (Map) import qualified Data.Map as Map +import qualified Data.Set as Set import qualified Data.Vector as V import Numeric.Natural @@ -46,6 +47,7 @@ import qualified Text.LLVM.AST as L import qualified Cryptol.Eval.Type as Cryptol (TValue(..), tValTy, evalValType) import qualified Cryptol.TypeCheck.AST as Cryptol (Schema(..)) +import qualified Verifier.SAW.Cryptol.Simpset as Cryptol import Data.Parameterized.Some (Some(..)) import Data.Parameterized.NatRepr @@ -64,7 +66,9 @@ import qualified Verifier.SAW.Prim as Prim import qualified Verifier.SAW.Simulator.Concrete as Concrete import Verifier.SAW.Cryptol (importType, emptyEnv) +import Verifier.SAW.Name import Verifier.SAW.TypedTerm +import Verifier.SAW.Simulator.What4 import Verifier.SAW.Simulator.What4.ReturnTrip import Text.LLVM.DebugUtils as L @@ -72,6 +76,7 @@ import SAWScript.Crucible.Common (Sym, sawCoreState) import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), SetupValue(..), ppTypedTermType) import SAWScript.Crucible.LLVM.MethodSpecIR +import qualified SAWScript.Proof as SP --import qualified SAWScript.LLVMBuiltins as LB @@ -292,7 +297,7 @@ resolveSetupElemIndexOrFail cc env nameEnv v i = do -- | Translate a SetupValue into a Crucible LLVM value, resolving -- references resolveSetupVal :: forall arch. - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => LLVMCrucibleContext arch -> Crucible.MemImpl Sym -> Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> @@ -353,7 +358,7 @@ resolveSetupVal cc mem env tyenv nameEnv val = do dl = Crucible.llvmDataLayout lc resolveTypedTerm :: - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => LLVMCrucibleContext arch -> TypedTerm -> IO LLVMVal @@ -368,6 +373,7 @@ resolveTypedTerm cc tm = ] resolveSAWPred :: + (?doW4Eval :: Bool) => LLVMCrucibleContext arch -> Term -> IO (W4.Pred Sym) @@ -385,10 +391,20 @@ resolveSAWPred cc tm = do _ -> return Nothing case mx of Just x -> return $ W4.backendPred sym x - Nothing -> bindSAWTerm sym st W4.BaseBoolRepr tm' + Nothing + | ?doW4Eval -> + do cryptol_ss <- Cryptol.mkCryptolSimpset @SP.TheoremNonce sc + (_,tm'') <- rewriteSharedTerm sc cryptol_ss tm' + (_,tm''') <- rewriteSharedTerm sc ss tm'' + if (filter (\(name, _, _) -> not (isPreludeName name)) $ Map.elems $ getConstantSet tm''') == [] then + do (_names, (_mlabels, p)) <- w4Eval sym st sc mempty Set.empty tm''' + return p + else bindSAWTerm sym st W4.BaseBoolRepr tm' + | otherwise -> + bindSAWTerm sym st W4.BaseBoolRepr tm' resolveSAWSymBV :: - (1 <= w) => + (?doW4Eval :: Bool, 1 <= w) => LLVMCrucibleContext arch -> NatRepr w -> Term -> @@ -405,10 +421,31 @@ resolveSAWSymBV cc w tm = _ -> return Nothing case mx of Just x -> W4.bvLit sym w (BV.mkBV w x) - Nothing -> bindSAWTerm sym st (W4.BaseBVRepr w) tm + Nothing + | ?doW4Eval -> + do let ss = cc^.ccBasicSS + (_,tm') <- rewriteSharedTerm sc ss tm + cryptol_ss <- Cryptol.mkCryptolSimpset @SP.TheoremNonce sc + (_,tm'') <- rewriteSharedTerm sc cryptol_ss tm' + (_,tm''') <- rewriteSharedTerm sc ss tm'' + if (filter (\(name, _, _) -> not (isPreludeName name)) $ Map.elems $ getConstantSet tm''') == [] then + do (_names, _, _, x) <- w4EvalAny sym st sc mempty Set.empty tm''' + case valueToSymExpr x of + Just (Some y) + | Just Refl <- testEquality (W4.BaseBVRepr w) (W4.exprType y) -> + return y + _ -> fail "" + else bindSAWTerm sym st (W4.BaseBVRepr w) tm + | otherwise -> + bindSAWTerm sym st (W4.BaseBVRepr w) tm + +isPreludeName :: NameInfo -> Bool +isPreludeName = \case + ModuleIdentifier ident -> identModule ident == preludeName + _ -> False resolveSAWTerm :: - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?doW4Eval :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => LLVMCrucibleContext arch -> Cryptol.TValue -> Term -> diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 57623d048c..c1b8782ada 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -25,6 +25,7 @@ Stability : provisional module SAWScript.Crucible.LLVM.X86 ( llvm_verify_x86 + , llvm_verify_fixpoint_x86 , defaultStackBaseAlign ) where @@ -41,11 +42,14 @@ import Data.Foldable (foldlM) import qualified Data.List.NonEmpty as NE import qualified Data.Vector as Vector import qualified Data.Text as Text -import Data.Set (Set) -import qualified Data.Set as Set +-- import Data.Set (Set) +-- import qualified Data.Set as Set import Data.Text (Text) import Data.Text.Encoding (decodeUtf8, encodeUtf8) import Data.Time.Clock (getCurrentTime, diffUTCTime) +import qualified Data.Set as Set +import Data.Set (Set) +import qualified Data.List as List import qualified Data.Map as Map import Data.Map (Map) import Data.Maybe @@ -53,12 +57,16 @@ import Data.Maybe import qualified Text.LLVM.AST as LLVM import Data.Parameterized.Some +import qualified Data.Parameterized.Map as MapF +-- import Data.Parameterized.Map (MapF) import Data.Parameterized.NatRepr -import Data.Parameterized.Context hiding (view) +import Data.Parameterized.Context hiding (view, zipWithM) import Verifier.SAW.CryptolEnv import Verifier.SAW.FiniteValue import Verifier.SAW.Name (toShortName) +import Verifier.SAW.Prelude +import Verifier.SAW.Recognizer import Verifier.SAW.SharedTerm import Verifier.SAW.TypedTerm @@ -84,6 +92,7 @@ import SAWScript.Crucible.LLVM.ResolveSetupValue import qualified SAWScript.Crucible.LLVM.Override as LO import qualified SAWScript.Crucible.LLVM.MethodSpecIR as LMS (LLVM) +import qualified What4.Concrete as W4 import qualified What4.Config as W4 import qualified What4.Expr as W4 import qualified What4.FunctionName as W4 @@ -112,6 +121,7 @@ import qualified Lang.Crucible.LLVM.Extension as C.LLVM import qualified Lang.Crucible.LLVM.Intrinsics as C.LLVM import qualified Lang.Crucible.LLVM.MemModel as C.LLVM import qualified Lang.Crucible.LLVM.MemType as C.LLVM +import qualified Lang.Crucible.LLVM.SimpleLoopFixpoint as Crucible.LLVM.Fixpoint import qualified Lang.Crucible.LLVM.Translation as C.LLVM import qualified Lang.Crucible.LLVM.TypeContext as C.LLVM @@ -141,6 +151,7 @@ type X86Constraints = , C.LLVM.HasLLVMAnn Sym , ?memOpts :: C.LLVM.MemOptions , ?lc :: C.LLVM.TypeContext + , ?doW4Eval :: Bool ) newtype X86Sim a = X86Sim { unX86Sim :: StateT X86State IO a } @@ -291,7 +302,39 @@ llvm_verify_x86 :: LLVMCrucibleSetupM () {- ^ Specification to verify against -} -> ProofScript () {- ^ Tactic used to use when discharging goals -} -> TopLevel (SomeLLVM MS.ProvedSpec) -llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat setup tactic +llvm_verify_x86 llvmModule path nm globsyms checkSat = + llvm_verify_x86' llvmModule path nm globsyms checkSat Nothing + +-- | Verify that an x86_64 function (following the System V AMD64 ABI) conforms +-- to an LLVM specification. This allows for compositional verification of LLVM +-- functions that call x86_64 functions (but not the other way around). +llvm_verify_fixpoint_x86 :: + Some LLVMModule {- ^ Module to associate with method spec -} -> + FilePath {- ^ Path to ELF file -} -> + String {- ^ Function's symbol in ELF file -} -> + [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} -> + Bool {- ^ Whether to enable path satisfiability checking -} -> + TypedTerm -> + LLVMCrucibleSetupM () {- ^ Specification to verify against -} -> + ProofScript () {- ^ Tactic used to use when discharging goals -} -> + TopLevel (SomeLLVM MS.ProvedSpec) +llvm_verify_fixpoint_x86 llvmModule path nm globsyms checkSat f = + llvm_verify_x86' llvmModule path nm globsyms checkSat (Just f) + +-- | Verify that an x86_64 function (following the System V AMD64 ABI) conforms +-- to an LLVM specification. This allows for compositional verification of LLVM +-- functions that call x86_64 functions (but not the other way around). +llvm_verify_x86' :: + Some LLVMModule {- ^ Module to associate with method spec -} -> + FilePath {- ^ Path to ELF file -} -> + String {- ^ Function's symbol in ELF file -} -> + [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} -> + Bool {- ^ Whether to enable path satisfiability checking -} -> + Maybe TypedTerm -> + LLVMCrucibleSetupM () {- ^ Specification to verify against -} -> + ProofScript () {- ^ Tactic used to use when discharging goals -} -> + TopLevel (SomeLLVM MS.ProvedSpec) +llvm_verify_x86' (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat maybeFixpointFunc setup tactic | Just Refl <- testEquality (C.LLVM.X86Repr $ knownNat @64) . C.LLVM.llvmArch $ modTrans llvmModule ^. C.LLVM.transContext = do start <- io getCurrentTime @@ -305,6 +348,14 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se rw <- getTopLevelRW cacheTermsSetting <- liftIO $ W4.getOptionSetting W4.B.cacheTerms $ W4.getConfiguration sym _ <- liftIO $ W4.setOpt cacheTermsSetting $ rwWhat4HashConsingX86 rw + liftIO $ W4.extendConfig + [ W4.opt + LO.enableSMTArrayMemoryModel + (W4.ConcreteBool $ rwSMTArrayMemoryModel rw) + ("Enable SMT array memory model" :: Text) + ] + (W4.getConfiguration sym) + let ?doW4Eval = rwWhat4Eval rw sawst <- liftIO $ sawCoreState sym halloc <- getHandleAlloc let mvar = C.LLVM.llvmMemVar . view C.LLVM.transContext $ modTrans llvmModule @@ -438,7 +489,63 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se else pure [] - let execFeatures = psatf + simpleLoopFixpointFeature <- maybeToList <$> mapM + (\func -> liftIO $ Crucible.LLVM.Fixpoint.simpleLoopFixpoint sym cfg mvar $ \fixpoint_substitution condition -> + do let fixpoint_substitution_as_list = reverse $ MapF.toList fixpoint_substitution + let foo = foldMap + (\(Some fixpoint_entry) -> + Set.map (mapSome $ W4.varExpr sym) $ W4.exprUninterpConstants sym $ Crucible.LLVM.Fixpoint.bodyValue fixpoint_entry) + (MapF.elems fixpoint_substitution) + let bar = Set.map (mapSome $ W4.varExpr sym) $ W4.exprUninterpConstants sym condition + let lala = Set.toList $ Set.filter + (\(Some variable) -> + not (List.isPrefixOf "cfoo" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "cbar" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "cundefined" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable)) + (Set.union foo bar) + lalala <- forM lala $ viewSome $ toSC sym sawst + baz <- mapM (scExtCns sc) $ Set.toList $ foldMap getAllExtSet lalala + -- lalala <- Set.fromList <$> mapM (scExtCns sc . tecExt) (methodSpec ^. MS.csPreState ^. MS.csFreshVars) + -- lala <- Set.fromList <$> mapM (viewSome $ toSC sym sawst) (Set.toList foo) + -- let baz = Set.toList $ Set.intersection lalala lala + arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) -> + toSC sym sawst $ Crucible.LLVM.Fixpoint.headerValue fixpoint_entry + applied_func <- scApplyAll sc (ttTerm func) $ baz ++ arguments + -- putStrLn $ scPrettyTerm Verifier.SAW.SharedTerm.defaultPPOpts applied_func + applied_func_selectors <- forM [1 .. (length fixpoint_substitution_as_list)] $ \i -> + scTupleSelector sc applied_func i (length fixpoint_substitution_as_list) + result_substitution <- MapF.fromList <$> zipWithM + (\(MapF.Pair variable _) applied_func_selector -> + MapF.Pair variable <$> bindSAWTerm sym sawst (W4.exprType variable) applied_func_selector) + fixpoint_substitution_as_list + applied_func_selectors + + lala_arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair variable _) -> + toSC sym sawst variable + let Just (_, foobar) = asConstant (ttTerm func) + let (foobar', [_, foobar'']) = asApplyAll foobar + when (isGlobalDef "Prelude.fix" foobar' == Nothing) $ fail $ "not Prelude.fix: " ++ showTerm foobar' + body <- betaNormalize sc =<< scApplyAll sc foobar'' ((ttTerm func) : (baz ++ lala_arguments)) + foo_arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) -> + toSC sym sawst $ Crucible.LLVM.Fixpoint.bodyValue fixpoint_entry + foo_applied_func <- scApplyAll sc (ttTerm func) $ baz ++ foo_arguments + foo_la <- scTuple sc lala_arguments + -- foo_condition <- toSC sym sawst condition + let lhs = Prelude.last foo_arguments + w <- scNat sc 64 + rhs <- scBvMul sc w (head baz) =<< scBvNat sc w =<< scNat sc 128 + foo_condition <- scBvULt sc w lhs rhs + -- putStrLn $ "foo_condition: " ++ scPrettyTerm Verifier.SAW.SharedTerm.defaultPPOpts foo_condition + foo_type <- scTupleType sc =<< mapM (scTypeOf sc) lala_arguments + foo_lala <- scIte sc foo_type foo_condition foo_applied_func foo_la + foo_lalala <- scEq sc foo_lala body + result_condition <- bindSAWTerm sym sawst W4.BaseBoolRepr foo_lalala + + return (result_substitution, result_condition)) + maybeFixpointFunc + + let execFeatures = simpleLoopFixpointFeature ++ psatf liftIO $ C.executeCrucible execFeatures initial >>= \case C.FinishedResult{} -> pure () @@ -724,7 +831,7 @@ assumeAllocation :: Map MS.AllocIndex Ptr -> (MS.AllocIndex, LLVMAllocSpec) {- ^ llvm_alloc statement -} -> X86Sim (Map MS.AllocIndex Ptr) -assumeAllocation env (i, LLVMAllocSpec mut _memTy align sz loc False) = do +assumeAllocation env (i, LLVMAllocSpec mut _memTy align sz loc False _symSz) = do cc <- use x86CrucibleContext sym <- use x86Sym mem <- use x86Mem @@ -746,15 +853,18 @@ assumePointsTo :: LLVMPointsTo LLVMArch {- ^ llvm_points_to statement from the precondition -} -> X86Sim () assumePointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tptval) = do - when (isJust cond) $ throwX86 "unsupported x86_64 command: llvm_conditional_points_to" - tval <- checkConcreteSizePointsToValue tptval - sym <- use x86Sym + -- when (isJust cond) $ throwX86 "unsupported x86_64 command: llvm_conditional_points_to" + -- tval <- checkConcreteSizePointsToValue tptval + -- sym <- use x86Sym + opts <- use x86Options cc <- use x86CrucibleContext mem <- use x86Mem ptr <- resolvePtrSetupValue env tyenv tptr - val <- liftIO $ resolveSetupVal cc mem env tyenv Map.empty tval - storTy <- liftIO $ C.LLVM.toStorableType =<< typeOfSetupValue cc tyenv nameEnv tval - mem' <- liftIO $ C.LLVM.storeConstRaw sym mem ptr storTy C.LLVM.noAlignment val + -- val <- liftIO $ resolveSetupVal cc mem env tyenv Map.empty tval + -- storTy <- liftIO $ C.LLVM.toStorableType =<< typeOfSetupValue cc tyenv nameEnv tval + -- mem' <- liftIO $ C.LLVM.storeConstRaw sym mem ptr storTy C.LLVM.noAlignment val + cond' <- liftIO $ mapM (resolveSAWPred cc . ttTerm) cond + mem' <- liftIO $ LO.storePointsToValue opts cc env tyenv nameEnv mem cond' ptr tptval Nothing x86Mem .= mem' resolvePtrSetupValue :: diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 02d0e99175..cce8ef1770 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -483,6 +483,7 @@ buildTopLevelEnv proxy opts = , rwDebugIntrinsics = True , rwWhat4HashConsing = False , rwWhat4HashConsingX86 = False + , rwWhat4Eval = False , rwPreservedRegs = [] , rwStackBaseAlign = defaultStackBaseAlign } @@ -595,6 +596,16 @@ disable_x86_what4_hash_consing = do rw <- getTopLevelRW putTopLevelRW rw { rwWhat4HashConsingX86 = False } +enable_what4_eval :: TopLevel () +enable_what4_eval = do + rw <- getTopLevelRW + putTopLevelRW rw { rwWhat4Eval = True } + +disable_what4_eval :: TopLevel () +disable_what4_eval = do + rw <- getTopLevelRW + putTopLevelRW rw { rwWhat4Eval = False } + add_x86_preserved_reg :: String -> TopLevel () add_x86_preserved_reg r = do rw <- getTopLevelRW @@ -2326,6 +2337,13 @@ primitives = Map.fromList Experimental [ "Legacy alternative name for `llvm_alloc_with_size`." ] + , prim "llvm_alloc_sym_init" "LLVMType -> LLVMSetup SetupValue" + (pureVal llvm_alloc_sym_init) + Experimental + [ "Like `llvm_alloc`, but assume that the allocation is initialized with" + , "symbolic bytes." + ] + , prim "llvm_symbolic_alloc" "Bool -> Int -> Term -> LLVMSetup SetupValue" (pureVal llvm_symbolic_alloc) Current @@ -2596,6 +2614,12 @@ primitives = Map.fromList Experimental [ "Legacy alternative name for `llvm_verify_x86`." ] + , prim "llvm_verify_fixpoint_x86" + "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> Term -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec" + (pureVal llvm_verify_fixpoint_x86) + Experimental + [] + , prim "enable_x86_what4_hash_consing" "TopLevel ()" (pureVal enable_x86_what4_hash_consing) Experimental @@ -2616,6 +2640,16 @@ primitives = Map.fromList Current [ "Use the default set of callee-saved registers during x86 verification." ] + , prim "enable_what4_eval" "TopLevel ()" + (pureVal enable_what4_eval) + Experimental + [ "Enable hash consing for What4 expressions during x86 verification." ] + + , prim "disable_what4_eval" "TopLevel ()" + (pureVal disable_what4_eval) + Current + [ "Disable hash consing for What4 expressions during x86 verification." ] + , prim "set_x86_stack_base_align" "Int -> TopLevel ()" (pureVal set_x86_stack_base_align) Experimental diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 34e178a4d6..7998692808 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -442,6 +442,8 @@ data TopLevelRW = , rwWhat4HashConsing :: Bool , rwWhat4HashConsingX86 :: Bool + , rwWhat4Eval :: Bool + , rwPreservedRegs :: [String] , rwStackBaseAlign :: Integer }