From 4c415e13544fe65ac16e4518b3c52a553aaf6043 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Fri, 11 Nov 2022 23:02:21 +0000 Subject: [PATCH 01/27] Find SMT array write of a fixed size. --- deps/crucible | 2 +- src/SAWScript/Crucible/LLVM/Override.hs | 25 ++++++++++++++++++++++++- 2 files changed, 25 insertions(+), 2 deletions(-) diff --git a/deps/crucible b/deps/crucible index 0515e64ab5..98428da33b 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 0515e64ab5c39036c6577e06bbe4272d39de5656 +Subproject commit 98428da33b1840e7adb37a74470d9a9246c3c03b diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index d193f73864..67104ba974 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -124,6 +124,7 @@ import Verifier.SAW.SharedTerm import Verifier.SAW.TypedAST 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 @@ -1684,7 +1685,29 @@ 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) + case maybe_matching_array of + Just (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 cc md prepost arr_tm $ ttTerm expected_arr_tm + return Nothing + + _ -> return $ Just errMsg + + _ -> return $ Just errMsg -- | Like 'matchPointsToValue', but specifically geared towards the needs -- of fields within bitfields. In particular, this performs all of the From b9651e35dc743b3a9fe1edfb071431702961c57f Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Wed, 22 Feb 2023 14:52:19 +0000 Subject: [PATCH 02/27] Load SMT array with concrete size. --- src/SAWScript/Crucible/LLVM/Override.hs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 67104ba974..d8e8e7fc04 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1697,17 +1697,22 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val = 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) - case maybe_matching_array of - Just (ok, arr) -> + 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 cc md prepost arr_tm $ ttTerm expected_arr_tm return Nothing - _ -> return $ Just errMsg + Left{} -> return $ Just errMsg + + Nothing -> return $ Just errMsg - _ -> return $ Just errMsg -- | Like 'matchPointsToValue', but specifically geared towards the needs -- of fields within bitfields. In particular, this performs all of the From 94a7226ac41f4fa70e3884d19c9c3f6298ff8f19 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Wed, 22 Feb 2023 13:54:57 +0000 Subject: [PATCH 03/27] Add test. --- .../Makefile | 11 +++ .../test_smt_array_load_concrete_size/Mix.cry | 8 +++ .../test_smt_array_load_concrete_size/test.bc | Bin 0 -> 3452 bytes .../test_smt_array_load_concrete_size/test.c | 13 ++++ .../test.saw | 66 ++++++++++++++++++ .../test_smt_array_load_concrete_size/test.sh | 6 ++ 6 files changed, 104 insertions(+) create mode 100644 intTests/test_smt_array_load_concrete_size/Makefile create mode 100644 intTests/test_smt_array_load_concrete_size/Mix.cry create mode 100644 intTests/test_smt_array_load_concrete_size/test.bc create mode 100644 intTests/test_smt_array_load_concrete_size/test.c create mode 100644 intTests/test_smt_array_load_concrete_size/test.saw create mode 100755 intTests/test_smt_array_load_concrete_size/test.sh diff --git a/intTests/test_smt_array_load_concrete_size/Makefile b/intTests/test_smt_array_load_concrete_size/Makefile new file mode 100644 index 0000000000..dffb75bb76 --- /dev/null +++ b/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 diff --git a/intTests/test_smt_array_load_concrete_size/Mix.cry b/intTests/test_smt_array_load_concrete_size/Mix.cry new file mode 100644 index 0000000000..2b51da1e58 --- /dev/null +++ b/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) diff --git a/intTests/test_smt_array_load_concrete_size/test.bc b/intTests/test_smt_array_load_concrete_size/test.bc new file mode 100644 index 0000000000000000000000000000000000000000..6e209292979a6f91f64ad330f4305d67ab11afeb GIT binary patch literal 3452 zcma)94NP0t6~2#W{G4FymxQ)wp;OW7GqzdDGg8{rbe4$A_m#`kI>`@v1p07U>)DFdIBlvj%T!3~*xD zKnW}rmWjg#u~865+NhDV$S0|+_U4rKI>ErfHK%R?=~gE-GkWbB=*eo9CbiR14GPMr z;grau#4w!llAr-|yyS6%IG7ekl49c(F~m?2D}@wjT6=S{^2U@l58AMX$_2eRNKL_S4jHPc|~q^5LyQLkD2U&m8o$V`nGDBeqc-#~>&#juwQ z3Sy&I45XNQJ*4osSRXiOw2Mj#+5Dk2jHJ0T#Tgo-?LhZZ9& z6$H)RSh$UXE07Y6L3nj@lbUr1ETOwiWU1y%tT97Ag=FAG*evpCv5^&d85Oxeg$-gD zy~}Af31xw+%oDrUY&uvhOlmiymG5#o@DxZ0_;s5C7O?FuV%8^hix74Wf~FJTc5pD< zCJv%RBp`-mU=Qerpv8va3hNgUdmU?A;B+^quxEuNIaVyzgu1W%L=r5LFHeb{fty zva!k&dn7i%-!p(i3CufAT2=e$Lr%?(GWS^0fOhPEDN9=Jm0Qv=0NEg51rT$AddV9L z2E<5#+j?tWdM8c6xXDl>h=MTlX)4H2{Yc3NsKMeIGfNu)QydjaQ^QuOKdFEblk?Iw zfr57)WT?@3>0N<}(A040U{U%Tn&Jg&r(W)Bk01QkbaJaohKdP}lU^nes&7@Q%OnC2 zrN$!rfw|`e1TNigQfp7l+VKj3gc?X%DR51?6s_LYo*dt@|LGZteT+B6_ZVW^(Iq(a zV~{t<1kJT&O>Y&^lCYcOx$)K_qJpVG`5IE*p%otqiUxVBZW@D7)613@x5akl$(C7r z%Q)GR9~}<`sN(>nHZc&OA^~!ER17ep8j^n_saR%}epb1%sn~QV8t7~Ii3@t|v{Tp1 zp0ZqxS?29cm&xXSY@mkkm4n(5LF@+Dt03>h za4K4JcT;h9N%7CDVuK}nW+ydJ0rJIh(W$wv*IbKguREphChbkL_NG*Eypl6d*v$#j zGLfr;OFtX4yhBoE% z2JPY$&Z!%a>`~p~l4f;Tdz;YpsyfUW`%~v)mb_!{eMdNPWRx0Bb+mt!RN@HeUeH~4 zYS#6*cD+pCl9ktMH=WXFPsGgmoF!v#fq;BA-MnhIB!J9~|8XmLDvp3XkULN}Qqisz zTCtH;+;S*BWUHrc*mSGQj}?}+H^G25wIvg4xg6US&zZ;VP5E5&m8quL9QfFrZ@WAQ zrH`Wqi*-Z&*BQkIr@XTSa8}-8mA4q>#}0*`R;;iJAU|A^{%uLI>QLNctKZvj;u2R_ zeryA(t6qBzO0-_PuHW6uyk@y-Z@EG?O~jh=omb)Y!C5FNkv4H8Kp_-n5PA_X#_QS` zdqS?>!kgNd>gf2HGjAVC(*}2Qy{Yxpr2eO)%qPUm;}f>($A5=Ho?xifRp%Y(_tZK4 zZrUww&4#h_qA&P%X zaQ2RhfIN)d&cL~x`7&WSA8VO_&lmLe{TfB(o6pBA=O8J`mUOHc5;U2^CC|wqG!OF* zi4B*tVkwlA8>~-)ogc6Wodn*Vr)QHLN0X;uiE=b0?%Z4XI?Hp14qN4te%~lyrTA<< zzpHP^?Wr3zH+DB3#1AqwYCPs2f;R*p1w(GwXdHsUU+cw_x%>Y)7YYYF!CG&3_x&S7 z{-E!e-{WR5W-zb8)Ez2G@#>)%B>x2_46GuU>Pi3wn3qfjs%G?hPbfAO|Cj6@H#qwlB+Pviemk5(ZBNr0ykpfJNCWhs-fkAn_D~xUN0tqH6PDEkc>e zY^-@c*0K~Eiq_lcx^NL5k+>jf%e+2NqpdRW3%oXx7 zS=`piO01A5&<2?j-=v`T#L+bV{3$jMocao^wv!Va&NsaK0CfD_&<-8*I-%o+XRJF7 z9XCinv;(>wI^JKz0L*FV584ABrXQ^F3{m(T?JezeX_`pKn z1Do;x9kBTgOhb<2np@lN>30RfwE@;=E)BlMgGGV6=UDBqvv0^#N~`+?AmI9<29zo? HRtD`quJDB( literal 0 HcmV?d00001 diff --git a/intTests/test_smt_array_load_concrete_size/test.c b/intTests/test_smt_array_load_concrete_size/test.c new file mode 100644 index 0000000000..14e059ae58 --- /dev/null +++ b/intTests/test_smt_array_load_concrete_size/test.c @@ -0,0 +1,13 @@ +#include +#include + +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; +} diff --git a/intTests/test_smt_array_load_concrete_size/test.saw b/intTests/test_smt_array_load_concrete_size/test.saw new file mode 100644 index 0000000000..1cf9dc6343 --- /dev/null +++ b/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 []; + })); + diff --git a/intTests/test_smt_array_load_concrete_size/test.sh b/intTests/test_smt_array_load_concrete_size/test.sh new file mode 100755 index 0000000000..d5f2c8ea02 --- /dev/null +++ b/intTests/test_smt_array_load_concrete_size/test.sh @@ -0,0 +1,6 @@ +#!/usr/bin/env bash + +set -e + +$SAW test.saw + From 45be7c40ab4bc7835b918be52ff070765ca104df Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 28 Jun 2023 01:58:27 +0000 Subject: [PATCH 04/27] Add noSatisfyingWriteFreshConstant option. --- src/SAWScript/Crucible/LLVM/Builtins.hs | 1 + src/SAWScript/Crucible/LLVM/X86.hs | 1 + 2 files changed, 2 insertions(+) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 3ddc66f29b..652117dea8 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -1741,6 +1741,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 () diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 8cadba3856..ed32b0dc4e 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -371,6 +371,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 From d514af1e566156e9f07b8fedef0dbcf1cce1042d Mon Sep 17 00:00:00 2001 From: Andrei Date: Thu, 18 Jan 2024 06:12:14 +0000 Subject: [PATCH 05/27] Add invariant substitution to getPoststateObligations. --- src/SAWScript/Crucible/LLVM/Builtins.hs | 35 +++++++++++++++---------- src/SAWScript/Crucible/LLVM/X86.hs | 8 +++--- 2 files changed, 26 insertions(+), 17 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index ca4ae24655..aa15d17612 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -131,6 +131,8 @@ import qualified Control.Monad.Trans.Maybe as MaybeT -- parameterized-utils import Data.Parameterized.Classes +import Data.Parameterized.Map (MapF) +import qualified Data.Parameterized.Map as MapF import Data.Parameterized.NatRepr import Data.Parameterized.Some import qualified Data.Parameterized.Context as Ctx @@ -645,14 +647,15 @@ verifyMethodSpec cc methodSpec lemmas checkSat tactic asp = printOutLnTop Info $ unwords ["Simulating", (methodSpec ^. csName) , "..."] top_loc <- toW4Loc "llvm_verify" <$> getPosition - (ret, globals3) <- - io $ verifySimulate opts cc pfs methodSpec args assumes top_loc lemmas globals2 checkSat asp mdMap + (ret, globals3, invSubst) <- + verifySimulate opts cc pfs methodSpec args assumes top_loc lemmas globals2 checkSat asp mdMap -- collect the proof obligations (asserts, post_override_state) <- verifyPoststate cc methodSpec env globals3 ret mdMap + invSubst -- restore previous assumption state _ <- io $ Crucible.popAssumptionFrame bak frameIdent @@ -752,6 +755,7 @@ refineMethodSpec cc methodSpec lemmas tactic = verifyPoststate cc methodSpec env globals3 ret mdMap + MapF.empty -- restore previous assumption state _ <- io $ Crucible.popAssumptionFrame bak frameIdent @@ -1431,11 +1435,11 @@ verifySimulate :: Bool -> Maybe (IORef (Map Text.Text [Crucible.FunctionProfile])) -> IORef MetadataMap -> - IO (Maybe (Crucible.MemType, LLVMVal), Crucible.SymGlobalState Sym) -verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat asp mdMap = - withCfgAndBlockId opts cc mspec $ \cfg entryId -> - ccWithBackend cc $ \bak -> - do let sym = cc^.ccSym + TopLevel (Maybe (Crucible.MemType, LLVMVal), Crucible.SymGlobalState Sym, MapF (W4.SymFnWrapper Sym) (W4.SymFnWrapper Sym)) +verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat asp mdMap = do + sc <- getSharedContext + io $ withCfgAndBlockId opts cc mspec $ \cfg entryId -> ccWithBackend cc $ \bak -> do + let sym = cc^.ccSym let argTys = Crucible.blockInputs $ Crucible.getBlock entryId $ Crucible.cfgBlockMap cfg let retTy = Crucible.handleReturnType $ Crucible.cfgHandle cfg @@ -1503,7 +1507,7 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat as (Crucible.regType retval) (Crucible.regValue retval) return (Just (ret_mt, v)) - return (retval', globals1) + return (retval', globals1, MapF.empty) Crucible.TimeoutResult _ -> fail $ "Symbolic execution timed out" @@ -1627,9 +1631,10 @@ verifyPoststate :: Crucible.SymGlobalState Sym {- ^ global variables -} -> Maybe (Crucible.MemType, LLVMVal) {- ^ optional return value -} -> IORef MetadataMap {- ^ metadata map -} -> + MapF (W4.SymFnWrapper Sym) (W4.SymFnWrapper Sym) {- ^ invariant substitution -} -> TopLevel ([(String, MS.ConditionMetadata, Term)], OverrideState (LLVM arch)) {- ^ generated labels and verification conditions -} -verifyPoststate cc mspec env0 globals ret mdMap = +verifyPoststate cc mspec env0 globals ret mdMap invSubst = ccWithBackend cc $ \bak -> do poststateLoc <- toW4Loc "_SAW_verify_poststate" <$> getPosition sc <- getSharedContext @@ -1670,7 +1675,7 @@ verifyPoststate cc mspec env0 globals ret mdMap = modifyIORef mdMap (Map.insert ann md) Crucible.addAssertion bak (Crucible.LabeledPred p' r) - sc_obligations <- io $ getPoststateObligations sc bak mdMap + sc_obligations <- io $ getPoststateObligations sc bak mdMap invSubst return (sc_obligations, st) where @@ -1692,14 +1697,16 @@ verifyPoststate cc mspec env0 globals ret mdMap = -- | Translate the proof obligations from the Crucible backend into SAWCore -- terms. For each proof oblication, return a triple consisting of the error --- message, the metadata, and the SAWCore. +-- message, the metadata, and the SAWCore. For each proof obligation, substitute +-- the uninterpreted invaiants with their definitions. getPoststateObligations :: Crucible.IsSymBackend Sym bak => SharedContext -> bak -> IORef MetadataMap -> + MapF (W4.SymFnWrapper Sym) (W4.SymFnWrapper Sym) {- ^ invariant substitution -} -> IO [(String, MS.ConditionMetadata, Term)] -getPoststateObligations sc bak mdMap = +getPoststateObligations sc bak mdMap invSubst = do obligations <- maybe [] Crucible.goalsToList <$> Crucible.getProofObligations bak Crucible.clearProofObligations bak @@ -1711,8 +1718,8 @@ getPoststateObligations sc bak mdMap = verifyObligation finalMdMap (Crucible.ProofGoal hyps (Crucible.LabeledPred concl err@(Crucible.SimError loc _))) = do st <- Common.sawCoreState sym - hypTerm <- toSC sym st =<< Crucible.assumptionsPred sym hyps - conclTerm <- toSC sym st concl + hypTerm <- toSC sym st =<< W4.substituteSymFns sym invSubst =<< Crucible.assumptionsPred sym hyps + conclTerm <- toSC sym st =<< W4.substituteSymFns sym invSubst concl obligation <- scImplies sc hypTerm conclTerm let defaultMd = MS.ConditionMetadata { MS.conditionLoc = loc diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 26aca27d81..d6f911b63b 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -62,6 +62,7 @@ import Data.Maybe import qualified Text.LLVM.AST as LLVM import Data.Parameterized.Some +import Data.Parameterized.Map (MapF) import qualified Data.Parameterized.Map as MapF import Data.Parameterized.NatRepr import Data.Parameterized.Nonce (GlobalNonceGenerator) @@ -583,7 +584,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec liftIO $ void $ runX86Sim finalState $ assertPost env (preState ^. x86Mem) (preState ^. x86Regs) mdMap - (stats,vcstats) <- checkGoals bak opts nm sc tactic mdMap + (stats,vcstats) <- checkGoals bak opts nm sc tactic mdMap MapF.empty end <- io getCurrentTime let diff = diffUTCTime end start @@ -1387,9 +1388,10 @@ checkGoals :: SharedContext -> ProofScript () -> IORef MetadataMap {- ^ metadata map -} -> + MapF (W4.SymFnWrapper Sym) (W4.SymFnWrapper Sym) -> TopLevel (SolverStats, [MS.VCStats]) -checkGoals bak opts nm sc tactic mdMap = do - gs <- liftIO $ getPoststateObligations sc bak mdMap +checkGoals bak opts nm sc tactic mdMap invSubst = do + gs <- liftIO $ getPoststateObligations sc bak mdMap invSubst liftIO . printOutLn opts Info $ mconcat [ "Simulation finished, running solver on " , show $ length gs From 66ff80e6f537f9fc32476fe8c25cd5c97593cd66 Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 19 Jan 2024 04:39:53 +0000 Subject: [PATCH 06/27] Bump what4. --- deps/what4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/what4 b/deps/what4 index e46dff4209..670c8aca55 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit e46dff42096550d860d210bd9cf6e435d8cd7ce5 +Subproject commit 670c8aca552e8b748b20d127d1310430880a45e8 From 94050cb65b57a80ff742f1c6088d1c728335072f Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 19 Jan 2024 05:56:11 +0000 Subject: [PATCH 07/27] wip --- src/SAWScript/Crucible/LLVM/X86.hs | 102 +++++++++++++++++++++-------- 1 file changed, 74 insertions(+), 28 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index d6f911b63b..128eec5178 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -33,7 +33,7 @@ module SAWScript.Crucible.LLVM.X86 import Control.Lens.TH (makeLenses) -import System.IO (stdout) +import System.IO import Control.Exception (throw) import Control.Lens (Getter, to, view, use, (&), (^.), (.~), (%~), (.=)) import Control.Monad (forM, forM_, unless, when, zipWithM) @@ -287,6 +287,8 @@ doPtrCmp f = Macaw.ptrOp $ \bak mem w xPtr xBits yPtr yBits x y -> do ok <- W4.orPred sym is_valid =<< W4.andPred sym is_negative_offset is_not_overflow return (ptr_as_bv, ok) + -- is_valid <- Macaw.isValidPtr sym mem w ptr + -- return (llvmPointerOffset ptr, is_valid) both_bits <- W4.andPred sym xBits yBits both_ptrs <- W4.andPred sym xPtr yPtr same_region <- W4.natEq sym (llvmPointerBlock x) (llvmPointerBlock y) @@ -297,9 +299,16 @@ doPtrCmp f = Macaw.ptrOp $ \bak mem w xPtr xBits yPtr yBits x y -> do =<< W4.andPred sym ok_x ok_y res_both_bits <- f sym (llvmPointerOffset x) (llvmPointerOffset y) res_both_ptrs <- f sym x_ptr_as_bv y_ptr_as_bv - undef <- Macaw.mkUndefinedBool sym "ptr_cmp" - W4.itePred sym both_bits res_both_bits - =<< W4.itePred sym ok_both_ptrs res_both_ptrs undef + + if| Just True <- W4.asConstantPred both_bits -> + return res_both_bits + | Just True <- W4.asConstantPred both_ptrs -> do + C.assert bak ok_both_ptrs $ C.AssertFailureSimError "" "" + return res_both_ptrs + | otherwise -> do + undef <- Macaw.mkUndefinedBool sym "ptr_cmp" + W4.itePred sym both_bits res_both_bits + =<< W4.itePred sym ok_both_ptrs res_both_ptrs undef ------------------------------------------------------------------------------- -- ** Entrypoint @@ -526,6 +535,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec forM_ assumes $ \(C.LabeledPred p (md, reason)) -> do expr <- resolveSAWPred cc p let loc = MS.conditionLoc md + putStrLn $ "resolveSAWPred: " ++ show expr C.addAssumption bak (C.GenericAssumption loc reason expr) C.regValue <$> @@ -540,12 +550,17 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec else pure [] - simpleLoopFixpointFeature <- + -- rw_ref <- liftIO . newIORef =<< getTopLevelRW + (simpleLoopFixpointFeature, maybe_ref) <- case fixpointSelect of - NoFixpoint -> return [] + NoFixpoint -> return ([], Nothing) SimpleFixpoint func -> - do f <- liftIO (setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func) - return [f] + do let ?ptrWidth = knownNat @64 + -- (f, ref) <- liftIO $ Crucible.LLVM.Fixpoint.simpleLoopFixpoint sym cfg mvar Nothing + -- (f, ref) <- liftIO $ Crucible.LLVM.Fixpoint.simpleLoopFixpoint sym cfg mvar $ + -- Just $ simpleLoopFixpointFunction sc sym rw_ref $ methodSpec ^. csName + (f, ref) <- liftIO $ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func + return ([f], Just ref) SimpleInvariant loopFixpointSymbol loopNum func -> do (loopaddr :: Macaw.MemSegmentOff 64) <- case findSymbols (symMap relf) . encodeUtf8 $ Text.pack loopFixpointSymbol of @@ -557,7 +572,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec do let printFn = printOutLn opts Info f <- liftIO (setupSimpleLoopInvariantFeature sym printFn loopNum sc sawst mdMap loopcfg mvar func) - return [f] + return ([f], Nothing) let execFeatures = simpleLoopFixpointFeature ++ psatf @@ -579,12 +594,22 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec ] C.TimeoutResult{} -> fail "Execution timed out" + (invSubst, loopFunEquivConds) <- liftIO $ case maybe_ref of + Just fixpoint_state_ref -> do + uninterp_inv_fns <- Crucible.LLVM.Fixpoint.executionFeatureContextInvPreds <$> readIORef fixpoint_state_ref + subst <- C.runCHC bak uninterp_inv_fns + loop_fun_equiv_conds <- Crucible.LLVM.Fixpoint.executionFeatureContextLoopFunEquivConds <$> readIORef fixpoint_state_ref + return (subst, loop_fun_equiv_conds) + Nothing -> return (MapF.empty, []) + liftIO $ printOutLn opts Info "Examining specification to determine postconditions" liftIO $ void $ runX86Sim finalState $ assertPost env (preState ^. x86Mem) (preState ^. x86Regs) mdMap - (stats,vcstats) <- checkGoals bak opts nm sc tactic mdMap MapF.empty + (stats,vcstats) <- checkGoals bak opts nm (methodSpec ^. MS.csLoc) sc tactic mdMap invSubst loopFunEquivConds + + -- putTopLevelRW =<< liftIO (readIORef rw_ref) end <- io getCurrentTime let diff = diffUTCTime end start @@ -608,31 +633,37 @@ setupSimpleLoopFixpointFeature :: C.CFG ext blocks init ret -> C.GlobalVar C.LLVM.Mem -> TypedTerm -> - IO (C.ExecutionFeature p sym ext rtp) + IO (C.ExecutionFeature p sym ext rtp, IORef (Crucible.LLVM.Fixpoint.ExecutionFeatureContext sym 64 ext)) -setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = - Crucible.LLVM.Fixpoint.simpleLoopFixpoint sym cfg mvar fixpoint_func +setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = do + let ?ptrWidth = knownNat @64 + Crucible.LLVM.Fixpoint.simpleLoopFixpoint sym cfg mvar $ Just fixpoint_func where fixpoint_func fixpoint_substitution condition = do let fixpoint_substitution_as_list = reverse $ MapF.toList fixpoint_substitution + let header_exprs = map (mapSome $ Crucible.LLVM.Fixpoint.headerValue) (MapF.elems fixpoint_substitution) let body_exprs = map (mapSome $ Crucible.LLVM.Fixpoint.bodyValue) (MapF.elems fixpoint_substitution) let uninterpreted_constants = foldMap (viewSome $ Set.map (mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym) - (Some condition : body_exprs) + (Some condition : body_exprs ++ header_exprs) let filtered_uninterpreted_constants = Set.toList $ Set.filter (\(Some variable) -> - not (List.isPrefixOf "creg_join_var" $ show $ W4.printSymExpr variable) + not (List.isPrefixOf "cindex_var" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "creg_join_var" $ show $ W4.printSymExpr variable) && not (List.isPrefixOf "cmem_join_var" $ show $ W4.printSymExpr variable) && not (List.isPrefixOf "cundefined" $ show $ W4.printSymExpr variable) && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable)) uninterpreted_constants - body_tms <- mapM (viewSome $ toSC sym sawst) filtered_uninterpreted_constants - implicit_parameters <- mapM (scExtCns sc) $ Set.toList $ foldMap getAllExtSet body_tms + tms <- mapM (viewSome $ toSC sym sawst) filtered_uninterpreted_constants + implicit_parameters <- mapM (scExtCns sc) $ Set.toList $ foldMap getAllExtSet tms + + putStrLn $ "implicit_parameters: " ++ show (map showTerm implicit_parameters) 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) $ implicit_parameters ++ arguments + arguments_tuple <- scTuple sc arguments + applied_func <- scApplyAll sc (ttTerm func) $ implicit_parameters ++ [arguments_tuple] 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 @@ -643,28 +674,28 @@ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = explicit_parameters <- forM fixpoint_substitution_as_list $ \(MapF.Pair variable _) -> toSC sym sawst variable + explicit_parameters_tuple <- scTuple sc explicit_parameters + inner_func <- case asConstant (ttTerm func) of Just (_, Just (asApplyAll -> (isGlobalDef "Prelude.fix" -> Just (), [_, inner_func]))) -> return inner_func _ -> fail $ "not Prelude.fix: " ++ showTerm (ttTerm func) func_body <- betaNormalize sc - =<< scApplyAll sc inner_func ((ttTerm func) : (implicit_parameters ++ explicit_parameters)) + =<< scApplyAll sc inner_func ((ttTerm func) : (implicit_parameters ++ [explicit_parameters_tuple])) step_arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) -> toSC sym sawst $ Crucible.LLVM.Fixpoint.bodyValue fixpoint_entry - tail_applied_func <- scApplyAll sc (ttTerm func) $ implicit_parameters ++ step_arguments - explicit_parameters_tuple <- scTuple sc explicit_parameters - let lhs = Prelude.last step_arguments - w <- scNat sc 64 - rhs <- scBvMul sc w (head implicit_parameters) =<< scBvNat sc w =<< scNat sc 128 - loop_condition <- scBvULt sc w lhs rhs + step_arguments_tuple <- scTuple sc step_arguments + tail_applied_func <- scApplyAll sc (ttTerm func) $ implicit_parameters ++ [step_arguments_tuple] + + loop_condition <- toSC sym sawst condition output_tuple_type <- scTupleType sc =<< mapM (scTypeOf sc) explicit_parameters loop_body <- scIte sc output_tuple_type loop_condition tail_applied_func explicit_parameters_tuple induction_step_condition <- scEq sc loop_body func_body result_condition <- bindSAWTerm sym sawst W4.BaseBoolRepr induction_step_condition - return (result_substitution, result_condition) + return (result_substitution, Just result_condition) -- | This procedure sets up the simple loop fixpoint feature. @@ -1385,13 +1416,28 @@ checkGoals :: bak -> Options -> String -> + W4.ProgramLoc -> SharedContext -> ProofScript () -> IORef MetadataMap {- ^ metadata map -} -> MapF (W4.SymFnWrapper Sym) (W4.SymFnWrapper Sym) -> + [W4.Pred Sym] -> TopLevel (SolverStats, [MS.VCStats]) -checkGoals bak opts nm sc tactic mdMap invSubst = do - gs <- liftIO $ getPoststateObligations sc bak mdMap invSubst +checkGoals bak opts nm loc sc tactic mdMap invSubst loopFunEquivConds = do + poststate_gs <- liftIO $ getPoststateObligations sc bak mdMap invSubst + loop_gs <- liftIO $ forM loopFunEquivConds $ \cond -> do + let sym = C.backendGetSym bak + st <- Common.sawCoreState sym + condTerm <- toSC sym st =<< W4.substituteSymFns sym invSubst cond + let defaultMd = MS.ConditionMetadata + { MS.conditionLoc = loc + , MS.conditionTags = mempty + , MS.conditionType = "loop function equivalence" + , MS.conditionContext = "" + } + return ("", defaultMd, condTerm) + let gs = poststate_gs ++ loop_gs + liftIO . printOutLn opts Info $ mconcat [ "Simulation finished, running solver on " , show $ length gs From e89b1abfcfd46d1d6021988416f9b016815d27dc Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 19 Jan 2024 06:28:22 +0000 Subject: [PATCH 08/27] wip --- deps/crucible | 2 +- src/SAWScript/Crucible/Common.hs | 12 +++++++++++- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/deps/crucible b/deps/crucible index c4e01c5306..803a8bef50 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit c4e01c5306e4af2aacc860fd1201cc3a4f8188f4 +Subproject commit 803a8bef50f9b39039d3d4520c7ded9734191f60 diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs index 4d27e816e4..246f6fdfe9 100644 --- a/src/SAWScript/Crucible/Common.hs +++ b/src/SAWScript/Crucible/Common.hs @@ -35,9 +35,10 @@ import Lang.Crucible.Simulator.Profiling import Lang.Crucible.Backend (AbortExecReason(..), ppAbortExecReason, IsSymInterface, IsSymBackend(..), HasSymInterface(..), SomeBackend(..)) -import Lang.Crucible.Backend.Online (OnlineBackend, newOnlineBackend) +import Lang.Crucible.Backend.Online (OnlineBackend, newOnlineBackend, solverInteractionFile) import qualified Data.Parameterized.Nonce as Nonce import What4.Protocol.Online (OnlineSolver(..)) +import qualified What4.Solver.CVC5 as CVC5 import qualified What4.Solver.Z3 as Z3 import qualified What4.Solver.Yices as Yices import qualified What4.Protocol.SMTLib2 as SMT2 @@ -48,6 +49,7 @@ import qualified What4.Interface as W4 import qualified What4.ProgramLoc as W4 (plSourceLoc) import Control.Lens ( (^.) ) +import qualified Data.Text as Text import System.Directory (createDirectoryIfMissing) import System.FilePath (()) import qualified Prettyprinter as PP @@ -89,14 +91,22 @@ newSAWCoreBackend pss sym = newSAWCoreBackendWithTimeout pss sym 0 newSAWCoreBackendWithTimeout :: PathSatSolver -> Sym -> Integer -> IO SomeOnlineBackend newSAWCoreBackendWithTimeout PathSat_Yices sym timeout = do bak <- newOnlineBackend sym Yices.yicesDefaultFeatures + W4.extendConfig Z3.z3Options (W4.getConfiguration sym) W4.extendConfig Yices.yicesOptions (W4.getConfiguration sym) + W4.extendConfig CVC5.cvc5Options (W4.getConfiguration sym) yicesTimeoutSetting <- W4.getOptionSetting Yices.yicesGoalTimeout (W4.getConfiguration sym) _ <- W4.setOpt yicesTimeoutSetting timeout + + auxOutSetting <- W4.getOptionSetting solverInteractionFile (W4.getConfiguration sym) + _ <- W4.setOpt auxOutSetting $ Text.pack "foo.smt2" + return (SomeOnlineBackend (bak :: Backend Yices.Connection)) newSAWCoreBackendWithTimeout PathSat_Z3 sym timeout = do bak <- newOnlineBackend sym (SMT2.defaultFeatures Z3.Z3) W4.extendConfig Z3.z3Options (W4.getConfiguration sym) + W4.extendConfig Yices.yicesOptions (W4.getConfiguration sym) + W4.extendConfig CVC5.cvc5Options (W4.getConfiguration sym) z3TimeoutSetting <- W4.getOptionSetting Z3.z3Timeout (W4.getConfiguration sym) _ <- W4.setOpt z3TimeoutSetting timeout return (SomeOnlineBackend (bak :: Backend (SMT2.Writer Z3.Z3))) From 9f037bc8546a462cb69b7a3252ae6cae7b53e116 Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 24 Jan 2024 07:43:12 +0000 Subject: [PATCH 09/27] Use simplified term in resolveSAWPred. --- src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index b5fd1bdbf6..7cc8e135c9 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -749,7 +749,7 @@ resolveSAWPred cc tm = do mx <- case getAllExts tm' of -- concretely evaluate if it is a closed term [] -> do modmap <- scGetModuleMap sc - let v = Concrete.evalSharedTerm modmap mempty mempty tm + let v = Concrete.evalSharedTerm modmap mempty mempty tm' pure (Just (Concrete.toBool v)) _ -> return Nothing case mx of From bf2b68d2bc073837dcd9afa37c8f35b039fe1d98 Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 24 Jan 2024 08:38:10 +0000 Subject: [PATCH 10/27] Bump crucible. --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index c4e01c5306..23cc439654 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit c4e01c5306e4af2aacc860fd1201cc3a4f8188f4 +Subproject commit 23cc439654abbc0c3714a7035d026453c234d9c4 From b8280daa9006e92bc2769b6746c9271859e67372 Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 24 Jan 2024 11:45:43 +0000 Subject: [PATCH 11/27] Remove unused sc. --- src/SAWScript/Crucible/LLVM/Builtins.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index aa15d17612..b9aae0e654 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -1437,7 +1437,6 @@ verifySimulate :: IORef MetadataMap -> TopLevel (Maybe (Crucible.MemType, LLVMVal), Crucible.SymGlobalState Sym, MapF (W4.SymFnWrapper Sym) (W4.SymFnWrapper Sym)) verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat asp mdMap = do - sc <- getSharedContext io $ withCfgAndBlockId opts cc mspec $ \cfg entryId -> ccWithBackend cc $ \bak -> do let sym = cc^.ccSym let argTys = Crucible.blockInputs $ From 741a87f0e10af3e4587e9244a25e68f738c98223 Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 24 Jan 2024 07:43:12 +0000 Subject: [PATCH 12/27] Use simplified term in resolveSAWPred. --- src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index b5fd1bdbf6..7cc8e135c9 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -749,7 +749,7 @@ resolveSAWPred cc tm = do mx <- case getAllExts tm' of -- concretely evaluate if it is a closed term [] -> do modmap <- scGetModuleMap sc - let v = Concrete.evalSharedTerm modmap mempty mempty tm + let v = Concrete.evalSharedTerm modmap mempty mempty tm' pure (Just (Concrete.toBool v)) _ -> return Nothing case mx of From 4d91a1e0f0658d083bd73cb534ebd5ecec0dacef Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 24 Jan 2024 18:58:57 +0000 Subject: [PATCH 13/27] Bump crucible. --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index 803a8bef50..c428da04d2 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 803a8bef50f9b39039d3d4520c7ded9734191f60 +Subproject commit c428da04d2ebfa166c113d49ae17b93fecc82635 From 1f11420b73fa81742a7581094df3e9b733d7a704 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Wed, 24 Jan 2024 11:31:22 -0800 Subject: [PATCH 14/27] Update src/SAWScript/Crucible/LLVM/Builtins.hs Co-authored-by: Ryan Scott --- src/SAWScript/Crucible/LLVM/Builtins.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index b9aae0e654..38dfe1128b 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -1697,7 +1697,7 @@ verifyPoststate cc mspec env0 globals ret mdMap invSubst = -- | Translate the proof obligations from the Crucible backend into SAWCore -- terms. For each proof oblication, return a triple consisting of the error -- message, the metadata, and the SAWCore. For each proof obligation, substitute --- the uninterpreted invaiants with their definitions. +-- the uninterpreted invariants with their definitions. getPoststateObligations :: Crucible.IsSymBackend Sym bak => SharedContext -> From 9ee2db86d74000590eacc5876d60e55f7138c6cb Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sat, 17 Feb 2024 21:59:34 -0500 Subject: [PATCH 15/27] Fix -Wunused-matches warning --- src/SAWScript/Crucible/LLVM/Builtins.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index aa15d17612..378ab95a97 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -1436,8 +1436,7 @@ verifySimulate :: Maybe (IORef (Map Text.Text [Crucible.FunctionProfile])) -> IORef MetadataMap -> TopLevel (Maybe (Crucible.MemType, LLVMVal), Crucible.SymGlobalState Sym, MapF (W4.SymFnWrapper Sym) (W4.SymFnWrapper Sym)) -verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat asp mdMap = do - sc <- getSharedContext +verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat asp mdMap = io $ withCfgAndBlockId opts cc mspec $ \cfg entryId -> ccWithBackend cc $ \bak -> do let sym = cc^.ccSym let argTys = Crucible.blockInputs $ From c300e513ee24afe41d690f2a3edec5c7ae6ec752 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 13:37:11 -0500 Subject: [PATCH 16/27] Bump crucible, what4 submodules This bumps: * The `crucible` submodule to bring in the changes from GaloisInc/crucible#1178 * The `what4` submodule to bring in the changes from GaloisInc/what4#256 --- deps/crucible | 2 +- deps/what4 | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/deps/crucible b/deps/crucible index 9a5d6cc32c..b938c6eebb 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 9a5d6cc32c8351722ab8b489a634b78f62337805 +Subproject commit b938c6eebb3c0c0dda0fb3913d69a45a50058995 diff --git a/deps/what4 b/deps/what4 index e46dff4209..72dd5ff574 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit e46dff42096550d860d210bd9cf6e435d8cd7ce5 +Subproject commit 72dd5ff5741caee5a40ca5f5791201a54f6064b7 From 19e17e26453eaa3db0ad94f2a626ecc06d90d26d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 14:04:30 -0500 Subject: [PATCH 17/27] Remove debugging-only code --- src/SAWScript/Crucible/Common.hs | 9 ++------- src/SAWScript/Crucible/LLVM/X86.hs | 4 ---- 2 files changed, 2 insertions(+), 11 deletions(-) diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs index 246f6fdfe9..61c8e60fa0 100644 --- a/src/SAWScript/Crucible/Common.hs +++ b/src/SAWScript/Crucible/Common.hs @@ -35,7 +35,7 @@ import Lang.Crucible.Simulator.Profiling import Lang.Crucible.Backend (AbortExecReason(..), ppAbortExecReason, IsSymInterface, IsSymBackend(..), HasSymInterface(..), SomeBackend(..)) -import Lang.Crucible.Backend.Online (OnlineBackend, newOnlineBackend, solverInteractionFile) +import Lang.Crucible.Backend.Online (OnlineBackend, newOnlineBackend) import qualified Data.Parameterized.Nonce as Nonce import What4.Protocol.Online (OnlineSolver(..)) import qualified What4.Solver.CVC5 as CVC5 @@ -49,7 +49,6 @@ import qualified What4.Interface as W4 import qualified What4.ProgramLoc as W4 (plSourceLoc) import Control.Lens ( (^.) ) -import qualified Data.Text as Text import System.Directory (createDirectoryIfMissing) import System.FilePath (()) import qualified Prettyprinter as PP @@ -69,7 +68,7 @@ type Sym = W4.ExprBuilder Nonce.GlobalNonceGenerator SAWCoreState (W4.Flags W4.F type Backend solver = OnlineBackend solver Nonce.GlobalNonceGenerator SAWCoreState (W4.Flags W4.FloatReal) data SomeOnlineBackend = - forall solver. OnlineSolver solver => + forall solver. OnlineSolver solver => SomeOnlineBackend (Backend solver) data SAWCruciblePersonality sym = SAWCruciblePersonality @@ -96,10 +95,6 @@ newSAWCoreBackendWithTimeout PathSat_Yices sym timeout = W4.extendConfig CVC5.cvc5Options (W4.getConfiguration sym) yicesTimeoutSetting <- W4.getOptionSetting Yices.yicesGoalTimeout (W4.getConfiguration sym) _ <- W4.setOpt yicesTimeoutSetting timeout - - auxOutSetting <- W4.getOptionSetting solverInteractionFile (W4.getConfiguration sym) - _ <- W4.setOpt auxOutSetting $ Text.pack "foo.smt2" - return (SomeOnlineBackend (bak :: Backend Yices.Connection)) newSAWCoreBackendWithTimeout PathSat_Z3 sym timeout = diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 04c01f97b1..0cfea2df62 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -536,7 +536,6 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec forM_ assumes $ \(C.LabeledPred p (md, reason)) -> do expr <- resolveSAWPred cc p let loc = MS.conditionLoc md - putStrLn $ "resolveSAWPred: " ++ show expr C.addAssumption bak (C.GenericAssumption loc reason expr) C.regValue <$> @@ -658,9 +657,6 @@ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = do uninterpreted_constants tms <- mapM (viewSome $ toSC sym sawst) filtered_uninterpreted_constants implicit_parameters <- mapM (scExtCns sc) $ Set.toList $ foldMap getAllExtSet tms - - putStrLn $ "implicit_parameters: " ++ show (map showTerm implicit_parameters) - arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) -> toSC sym sawst $ Crucible.LLVM.Fixpoint.headerValue fixpoint_entry arguments_tuple <- scTuple sc arguments From 6aeaf27c6014af2d41d3841f76457e4df9233203 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 15:12:14 -0500 Subject: [PATCH 18/27] Bump cryptol-specs to incorporate GaloisInc/cryptol-specs#72 --- deps/cryptol-specs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/cryptol-specs b/deps/cryptol-specs index 423fd3f381..1073bec7ba 160000 --- a/deps/cryptol-specs +++ b/deps/cryptol-specs @@ -1 +1 @@ -Subproject commit 423fd3f381b3337c9d9ac52760019bf03f4314ae +Subproject commit 1073bec7ba9f05b6af1f85adbc43999be568abd1 From a39ccf4258e9e76a36f0fa27e880bfe66ac391c1 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 4 Mar 2024 13:31:47 -0500 Subject: [PATCH 19/27] Repair AES example to work with `type Nk = AES256` --- examples/aes/aes.saw | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/examples/aes/aes.saw b/examples/aes/aes.saw index 4ad6a9e578..59dd0d4fb6 100644 --- a/examples/aes/aes.saw +++ b/examples/aes/aes.saw @@ -5,20 +5,22 @@ print "Proving encrypt_lemma..."; encrypt_lemma <- time (prove_print (unint_z3 ["AESRound"]) (rewrite (cryptol_ss()) - {{ \(state0 : State) (ks : [9]RoundKey) -> + {{ \(state0 : State) (ks : [13]RoundKey) -> (rounds where rounds = [state0] # [ AESRound (rk, s) | rk <- ks | s <- rounds ]) ! 0 == - AESRound(ks@8,AESRound(ks@7,AESRound(ks@6,AESRound(ks@5,AESRound(ks@4, - AESRound(ks@3,AESRound(ks@2,AESRound(ks@1,AESRound(ks@0,state0))))))))) + AESRound(ks@12,AESRound(ks@11,AESRound(ks@10,AESRound(ks@9, + AESRound(ks@8,AESRound(ks@7,AESRound(ks@6,AESRound(ks@5,AESRound(ks@4, + AESRound(ks@3,AESRound(ks@2,AESRound(ks@1,AESRound(ks@0,state0))))))))))))) }})); print "Proving decrypt_lemma..."; decrypt_lemma <- time (prove_print (unint_z3 ["AESInvRound"]) (rewrite (cryptol_ss()) - {{ \(state0 : State) (ks : [9]RoundKey) -> + {{ \(state0 : State) (ks : [13]RoundKey) -> (rounds where rounds = [state0] # [ AESInvRound (rk, s) | rk <- reverse ks | s <- rounds ]) ! 0 == AESInvRound(ks@0,AESInvRound(ks@1,AESInvRound(ks@2,AESInvRound(ks@3,AESInvRound(ks@4, - AESInvRound(ks@5,AESInvRound(ks@6,AESInvRound(ks@7,AESInvRound(ks@8,state0))))))))) + AESInvRound(ks@5,AESInvRound(ks@6,AESInvRound(ks@7,AESInvRound(ks@8, + AESInvRound(ks@9,AESInvRound(ks@10,AESInvRound(ks@11,AESInvRound(ks@12,state0))))))))))))) }})); print "Proving msgToState_stateToMsg(rme)..."; @@ -65,7 +67,7 @@ InvMixColumns_MixColumns <- print "Proving aesDecrypt_aesEncrypt(rewriting)..."; dec_enc <- time (prove_print do { - unfolding ["aesEncrypt", "aesDecrypt"]; + unfolding ["aesEncrypt", "aesEncryptWithKeySchedule", "aesDecrypt"]; simplify (addsimps [encrypt_lemma, decrypt_lemma] (cryptol_ss())); @@ -112,7 +114,7 @@ MixColumns_InvMixColumns <- print "Proving aesEncrypt_aesDecrypt(rewriting)..."; enc_dec <- time (prove_print do { - unfolding ["aesEncrypt", "aesDecrypt"]; + unfolding ["aesEncrypt", "aesEncryptWithKeySchedule", "aesDecrypt"]; simplify (addsimps [encrypt_lemma, decrypt_lemma] (cryptol_ss())); From df84d91eb1823438aa440faf55ba31de1c0d7405 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 7 Mar 2024 11:19:14 -0500 Subject: [PATCH 20/27] Add expert options for enabling What4-, Crucible-related SyGuS features --- saw-remote-api/src/SAWServer.hs | 2 + src/SAWScript/Crucible/LLVM/Builtins.hs | 7 +++- src/SAWScript/Crucible/LLVM/X86.hs | 10 +++-- src/SAWScript/Interpreter.hs | 53 +++++++++++++++++++++++++ src/SAWScript/Value.hs | 5 ++- 5 files changed, 72 insertions(+), 5 deletions(-) diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 76a5600590..41863eb001 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -270,6 +270,8 @@ initialState readFileFn = , rwProofs = [] , rwPreservedRegs = [] , rwAllocSymInitCheck = True + , rwWhat4PushMuxOps = False + , rwNoSatisfyingWriteFreshConstant = True , rwCrucibleTimeout = CC.defaultSAWCoreBackendTimeout , rwPathSatSolver = CC.PathSat_Z3 , rwSkipSafetyProofs = False diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 2dbae6d68c..17c48842ce 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -1750,8 +1750,10 @@ setupLLVMCrucibleContext pathSat lm action = smt_array_memory_model_enabled <- gets rwSMTArrayMemoryModel crucible_assert_then_assume_enabled <- gets rwCrucibleAssertThenAssume what4HashConsing <- gets rwWhat4HashConsing + what4PushMuxOps <- gets rwWhat4PushMuxOps laxPointerOrdering <- gets rwLaxPointerOrdering laxLoadsAndStores <- gets rwLaxLoadsAndStores + noSatisfyingWriteFreshConstant <- gets rwNoSatisfyingWriteFreshConstant pathSatSolver <- gets rwPathSatSolver what4Eval <- gets rwWhat4Eval allocSymInitCheck <- gets rwAllocSymInitCheck @@ -1762,7 +1764,7 @@ setupLLVMCrucibleContext pathSat lm action = let ?memOpts = Crucible.defaultMemOptions { Crucible.laxPointerOrdering = laxPointerOrdering , Crucible.laxLoadsAndStores = laxLoadsAndStores - , Crucible.noSatisfyingWriteFreshConstant = False + , Crucible.noSatisfyingWriteFreshConstant = noSatisfyingWriteFreshConstant } let ?intrinsicsOpts = Crucible.defaultIntrinsicsOptions let ?recordLLVMAnnotation = \_ _ _ -> return () @@ -1782,6 +1784,9 @@ setupLLVMCrucibleContext pathSat lm action = cacheTermsSetting <- W4.getOptionSetting W4.cacheTerms cfg _ <- W4.setOpt cacheTermsSetting what4HashConsing + pushMuxOpsSetting <- W4.getOptionSetting W4.pushMuxOpsOption cfg + _ <- W4.setOpt pushMuxOpsSetting what4PushMuxOps + -- enable online solver interactions if path sat checking is on enableOnlineSetting <- W4.getOptionSetting Crucible.enableOnlineBackend cfg _ <- W4.setOpt enableOnlineSetting pathSat diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 0cfea2df62..0065eba95b 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -381,11 +381,12 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec $ modTrans llvmModule ^. C.LLVM.transContext = do start <- io getCurrentTime laxLoadsAndStores <- gets rwLaxLoadsAndStores + noSatisfyingWriteFreshConstant <- gets rwNoSatisfyingWriteFreshConstant pathSatSolver <- gets rwPathSatSolver let ?ptrWidth = knownNat @64 let ?memOpts = C.LLVM.defaultMemOptions { C.LLVM.laxLoadsAndStores = laxLoadsAndStores - , C.LLVM.noSatisfyingWriteFreshConstant = False + , C.LLVM.noSatisfyingWriteFreshConstant = noSatisfyingWriteFreshConstant } let ?recordLLVMAnnotation = \_ _ _ -> return () sc <- getSharedContext @@ -396,15 +397,18 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec mdMap <- liftIO $ newIORef mempty SomeOnlineBackend bak <- liftIO $ newSAWCoreBackendWithTimeout pathSatSolver sym $ rwCrucibleTimeout rw - cacheTermsSetting <- liftIO $ W4.getOptionSetting W4.B.cacheTerms $ W4.getConfiguration sym + let config = W4.getConfiguration sym + cacheTermsSetting <- liftIO $ W4.getOptionSetting W4.B.cacheTerms config _ <- liftIO $ W4.setOpt cacheTermsSetting $ rwWhat4HashConsingX86 rw + pushMuxOpsSetting <- liftIO $ W4.getOptionSetting W4.B.pushMuxOpsOption config + _ <- liftIO $ W4.setOpt pushMuxOpsSetting $ rwWhat4PushMuxOps rw liftIO $ W4.extendConfig [ W4.opt LO.enableSMTArrayMemoryModel (W4.ConcreteBool $ rwSMTArrayMemoryModel rw) ("Enable SMT array memory model" :: Text) ] - (W4.getConfiguration sym) + config let ?w4EvalTactic = W4EvalTactic { doW4Eval = rwWhat4Eval rw } sawst <- liftIO $ sawCoreState sym halloc <- getHandleAlloc diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 701dc1475a..0ab8c9e765 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -515,6 +515,8 @@ buildTopLevelEnv proxy opts = , rwPreservedRegs = [] , rwStackBaseAlign = defaultStackBaseAlign , rwAllocSymInitCheck = True + , rwWhat4PushMuxOps = False + , rwNoSatisfyingWriteFreshConstant = True , rwCrucibleTimeout = CC.defaultSAWCoreBackendTimeout , rwPathSatSolver = CC.PathSat_Z3 , rwSkipSafetyProofs = False @@ -737,6 +739,26 @@ disable_alloc_sym_init_check = do rw <- getTopLevelRW putTopLevelRW rw { rwAllocSymInitCheck = False } +enable_no_satisfying_write_fresh_constant :: TopLevel () +enable_no_satisfying_write_fresh_constant = do + rw <- getTopLevelRW + putTopLevelRW rw { rwNoSatisfyingWriteFreshConstant = True } + +disable_no_satisfying_write_fresh_constant :: TopLevel () +disable_no_satisfying_write_fresh_constant = do + rw <- getTopLevelRW + putTopLevelRW rw { rwNoSatisfyingWriteFreshConstant = False } + +enable_what4_push_mux_ops :: TopLevel () +enable_what4_push_mux_ops = do + rw <- getTopLevelRW + putTopLevelRW rw { rwWhat4PushMuxOps = True } + +disable_what4_push_mux_ops :: TopLevel () +disable_what4_push_mux_ops = do + rw <- getTopLevelRW + putTopLevelRW rw { rwWhat4PushMuxOps = False } + set_crucible_timeout :: Integer -> TopLevel () set_crucible_timeout t = do rw <- getTopLevelRW @@ -3466,6 +3488,37 @@ primitives = Map.fromList , "This makes the implicit assumption that there is some unspecified byte at any valid memory address." ] + , prim "enable_no_satisfying_write_fresh_constant" "TopLevel ()" + (pureVal enable_no_satisfying_write_fresh_constant) + Experimental + [ "When simulating LLVM code that performs an invalid write, make a fresh" + , "constant as a proof obligation. This constant will always fail, but it" + , "will also not be constant-folded away." + ] + + , prim "disable_no_satisfying_write_fresh_constant" "TopLevel ()" + (pureVal disable_no_satisfying_write_fresh_constant) + Experimental + [ "When simulating LLVM code that performs an invalid write, return 'false'" + , "as a proof obligation." + ] + + , prim "enable_what4_push_mux_ops" "TopLevel ()" + (pureVal enable_what4_push_mux_ops) + Experimental + [ "Push certain What4 operations (e.g., 'zext') down to the branches of" + , "'ite' expressions as much as possible. In some (but not all) circumstances," + , "this can result in operations that are easier for SMT solvers to reason" + , "about." + ] + + , prim "disable_what4_push_mux_ops" "TopLevel ()" + (pureVal disable_what4_push_mux_ops) + Experimental + [ "Do not push certain What4 operations (e.g., 'zext') down to the branches" + , "of 'ite' expressions as much as possible." + ] + , prim "set_crucible_timeout" "Int -> TopLevel ()" (pureVal set_crucible_timeout) Experimental diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 709b422a58..5f2a525da8 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -333,7 +333,7 @@ showRefnset opts ss = ppFunAssumpRHS ctx (OpaqueFunAssump f args) = ppTermAppInCtx opts' ctx (funNameTerm f) args ppFunAssumpRHS ctx (RewriteFunAssump rhs) = - SAWCorePP.ppTermInCtx opts' (map fst $ mrVarCtxInnerToOuter ctx) rhs + SAWCorePP.ppTermInCtx opts' (map fst $ mrVarCtxInnerToOuter ctx) rhs opts' = sawPPOpts opts showsPrecValue :: PPOpts -> SAWNamingEnv -> Int -> Value -> ShowS @@ -587,6 +587,9 @@ data TopLevelRW = , rwAllocSymInitCheck :: Bool + , rwWhat4PushMuxOps :: Bool + , rwNoSatisfyingWriteFreshConstant :: Bool + , rwCrucibleTimeout :: Integer , rwPathSatSolver :: Common.PathSatSolver From 49c40a07d3a61e85f2c7426dd13bea5ad3ee3a65 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 7 Mar 2024 11:48:05 -0500 Subject: [PATCH 21/27] Split off separate llvm_verify_fixpoint_chc_x86 command --- deps/crucible | 2 +- src/SAWScript/Crucible/LLVM/X86.hs | 117 ++++++++++++++++++++++++++--- src/SAWScript/Interpreter.hs | 13 ++++ 3 files changed, 120 insertions(+), 12 deletions(-) diff --git a/deps/crucible b/deps/crucible index b938c6eebb..6b7d94c61f 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit b938c6eebb3c0c0dda0fb3913d69a45a50058995 +Subproject commit 6b7d94c61fca303f2ee155e2f3ee6a36ebb804cc diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 0065eba95b..55c4280dd5 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -27,6 +27,7 @@ Stability : provisional module SAWScript.Crucible.LLVM.X86 ( llvm_verify_x86 , llvm_verify_fixpoint_x86 + , llvm_verify_fixpoint_chc_x86 , llvm_verify_x86_with_invariant , defaultStackBaseAlign ) where @@ -131,6 +132,7 @@ 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.SimpleLoopFixpointCHC as Crucible.LLVM.FixpointCHC import qualified Lang.Crucible.LLVM.SimpleLoopInvariant as SimpleInvariant import qualified Lang.Crucible.LLVM.Translation as C.LLVM import qualified Lang.Crucible.LLVM.TypeContext as C.LLVM @@ -344,6 +346,26 @@ llvm_verify_fixpoint_x86 :: llvm_verify_fixpoint_x86 llvmModule path nm globsyms checkSat f = llvm_verify_x86_common llvmModule path nm globsyms checkSat (SimpleFixpoint 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). +-- +-- This differs from 'llvm_verify_fixpoint_x86' in that it leverages Z3's +-- constrained horn-clause (CHC) functionality to synthesize some of the loop's +-- properties. +llvm_verify_fixpoint_chc_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 {- ^ Function specifying the loop -} -> + LLVMCrucibleSetupM () {- ^ Specification to verify against -} -> + ProofScript () {- ^ Tactic used to use when discharging goals -} -> + TopLevel (SomeLLVM MS.ProvedSpec) +llvm_verify_fixpoint_chc_x86 llvmModule path nm globsyms checkSat f = + llvm_verify_x86_common llvmModule path nm globsyms checkSat (SimpleFixpointCHC 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). @@ -364,6 +386,7 @@ llvm_verify_x86_with_invariant llvmModule path nm globsyms checkSat (loopName,lo data FixpointSelect = NoFixpoint | SimpleFixpoint TypedTerm + | SimpleFixpointCHC TypedTerm | SimpleInvariant String Integer TypedTerm llvm_verify_x86_common :: @@ -559,11 +582,14 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec case fixpointSelect of NoFixpoint -> return ([], Nothing) SimpleFixpoint func -> + do f <- liftIO $ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func + return ([f], Nothing) + SimpleFixpointCHC func -> do let ?ptrWidth = knownNat @64 -- (f, ref) <- liftIO $ Crucible.LLVM.Fixpoint.simpleLoopFixpoint sym cfg mvar Nothing -- (f, ref) <- liftIO $ Crucible.LLVM.Fixpoint.simpleLoopFixpoint sym cfg mvar $ -- Just $ simpleLoopFixpointFunction sc sym rw_ref $ methodSpec ^. csName - (f, ref) <- liftIO $ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func + (f, ref) <- liftIO $ setupSimpleLoopFixpointCHCFeature sym sc sawst cfg mvar func return ([f], Just ref) SimpleInvariant loopFixpointSymbol loopNum func -> do (loopaddr :: Macaw.MemSegmentOff 64) <- @@ -600,9 +626,9 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec (invSubst, loopFunEquivConds) <- liftIO $ case maybe_ref of Just fixpoint_state_ref -> do - uninterp_inv_fns <- Crucible.LLVM.Fixpoint.executionFeatureContextInvPreds <$> readIORef fixpoint_state_ref + uninterp_inv_fns <- Crucible.LLVM.FixpointCHC.executionFeatureContextInvPreds <$> readIORef fixpoint_state_ref subst <- C.runCHC bak uninterp_inv_fns - loop_fun_equiv_conds <- Crucible.LLVM.Fixpoint.executionFeatureContextLoopFunEquivConds <$> readIORef fixpoint_state_ref + loop_fun_equiv_conds <- Crucible.LLVM.FixpointCHC.executionFeatureContextLoopFunEquivConds <$> readIORef fixpoint_state_ref return (subst, loop_fun_equiv_conds) Nothing -> return (MapF.empty, []) @@ -622,9 +648,78 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec | otherwise = fail "LLVM module must be 64-bit" +setupSimpleLoopFixpointFeature :: + ( sym ~ W4.B.ExprBuilder n st fs + , C.IsSymInterface sym + , ?memOpts::C.LLVM.MemOptions + , C.LLVM.HasLLVMAnn sym + , C.IsSyntaxExtension ext + ) => + sym -> + SharedContext -> + SAWCoreState n -> + C.CFG ext blocks init ret -> + C.GlobalVar C.LLVM.Mem -> + TypedTerm -> + IO (C.ExecutionFeature p sym ext rtp) +setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = + Crucible.LLVM.Fixpoint.simpleLoopFixpoint sym cfg mvar fixpoint_func -setupSimpleLoopFixpointFeature :: + where + fixpoint_func fixpoint_substitution condition = + do let fixpoint_substitution_as_list = reverse $ MapF.toList fixpoint_substitution + let body_exprs = map (mapSome $ Crucible.LLVM.Fixpoint.bodyValue) (MapF.elems fixpoint_substitution) + let uninterpreted_constants = foldMap + (viewSome $ Set.map (mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym) + (Some condition : body_exprs) + let filtered_uninterpreted_constants = Set.toList $ Set.filter + (\(Some variable) -> + not (List.isPrefixOf "creg_join_var" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "cmem_join_var" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "cundefined" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable)) + uninterpreted_constants + body_tms <- mapM (viewSome $ toSC sym sawst) filtered_uninterpreted_constants + implicit_parameters <- mapM (scExtCns sc) $ Set.toList $ foldMap getAllExtSet body_tms + + 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) $ implicit_parameters ++ arguments + 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 + + explicit_parameters <- forM fixpoint_substitution_as_list $ \(MapF.Pair variable _) -> + toSC sym sawst variable + inner_func <- case asConstant (ttTerm func) of + Just (_, Just (asApplyAll -> (isGlobalDef "Prelude.fix" -> Just (), [_, inner_func]))) -> + return inner_func + _ -> fail $ "not Prelude.fix: " ++ showTerm (ttTerm func) + func_body <- betaNormalize sc + =<< scApplyAll sc inner_func ((ttTerm func) : (implicit_parameters ++ explicit_parameters)) + + step_arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) -> + toSC sym sawst $ Crucible.LLVM.Fixpoint.bodyValue fixpoint_entry + tail_applied_func <- scApplyAll sc (ttTerm func) $ implicit_parameters ++ step_arguments + explicit_parameters_tuple <- scTuple sc explicit_parameters + let lhs = Prelude.last step_arguments + w <- scNat sc 64 + rhs <- scBvMul sc w (head implicit_parameters) =<< scBvNat sc w =<< scNat sc 128 + loop_condition <- scBvULt sc w lhs rhs + output_tuple_type <- scTupleType sc =<< mapM (scTypeOf sc) explicit_parameters + loop_body <- scIte sc output_tuple_type loop_condition tail_applied_func explicit_parameters_tuple + + induction_step_condition <- scEq sc loop_body func_body + result_condition <- bindSAWTerm sym sawst W4.BaseBoolRepr induction_step_condition + + return (result_substitution, result_condition) + +setupSimpleLoopFixpointCHCFeature :: ( sym ~ W4.B.ExprBuilder n st fs , C.IsSymInterface sym , ?memOpts::C.LLVM.MemOptions @@ -637,17 +732,17 @@ setupSimpleLoopFixpointFeature :: C.CFG ext blocks init ret -> C.GlobalVar C.LLVM.Mem -> TypedTerm -> - IO (C.ExecutionFeature p sym ext rtp, IORef (Crucible.LLVM.Fixpoint.ExecutionFeatureContext sym 64 ext)) + IO (C.ExecutionFeature p sym ext rtp, IORef (Crucible.LLVM.FixpointCHC.ExecutionFeatureContext sym 64 ext)) -setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = do +setupSimpleLoopFixpointCHCFeature sym sc sawst cfg mvar func = do let ?ptrWidth = knownNat @64 - Crucible.LLVM.Fixpoint.simpleLoopFixpoint sym cfg mvar $ Just fixpoint_func + Crucible.LLVM.FixpointCHC.simpleLoopFixpoint sym cfg mvar $ Just fixpoint_func where fixpoint_func fixpoint_substitution condition = do let fixpoint_substitution_as_list = reverse $ MapF.toList fixpoint_substitution - let header_exprs = map (mapSome $ Crucible.LLVM.Fixpoint.headerValue) (MapF.elems fixpoint_substitution) - let body_exprs = map (mapSome $ Crucible.LLVM.Fixpoint.bodyValue) (MapF.elems fixpoint_substitution) + let header_exprs = map (mapSome $ Crucible.LLVM.FixpointCHC.headerValue) (MapF.elems fixpoint_substitution) + let body_exprs = map (mapSome $ Crucible.LLVM.FixpointCHC.bodyValue) (MapF.elems fixpoint_substitution) let uninterpreted_constants = foldMap (viewSome $ Set.map (mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym) (Some condition : body_exprs ++ header_exprs) @@ -662,7 +757,7 @@ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = do tms <- mapM (viewSome $ toSC sym sawst) filtered_uninterpreted_constants implicit_parameters <- mapM (scExtCns sc) $ Set.toList $ foldMap getAllExtSet tms arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) -> - toSC sym sawst $ Crucible.LLVM.Fixpoint.headerValue fixpoint_entry + toSC sym sawst $ Crucible.LLVM.FixpointCHC.headerValue fixpoint_entry arguments_tuple <- scTuple sc arguments applied_func <- scApplyAll sc (ttTerm func) $ implicit_parameters ++ [arguments_tuple] applied_func_selectors <- forM [1 .. (length fixpoint_substitution_as_list)] $ \i -> @@ -685,7 +780,7 @@ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = do =<< scApplyAll sc inner_func ((ttTerm func) : (implicit_parameters ++ [explicit_parameters_tuple])) step_arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) -> - toSC sym sawst $ Crucible.LLVM.Fixpoint.bodyValue fixpoint_entry + toSC sym sawst $ Crucible.LLVM.FixpointCHC.bodyValue fixpoint_entry step_arguments_tuple <- scTuple sc step_arguments tail_applied_func <- scApplyAll sc (ttTerm func) $ implicit_parameters ++ [step_arguments_tuple] diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 0ab8c9e765..e49e94c471 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3399,6 +3399,19 @@ primitives = Map.fromList , "the live variables in the loop evolve as the loop computes." ] + , prim "llvm_verify_fixpoint_chc_x86" + "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> Term -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec" + (pureVal llvm_verify_fixpoint_chc_x86) + Experimental + [ "An experimental variant of 'llvm_verify_x86'. This variant can prove some properties" + , "involving simple loops with the help of a user-provided term that describes how" + , "the live variables in the loop evolve as the loop computes." + , "" + , "This differs from 'llvm_verify_fixpoint_x86' in that it leverages Z3's" + , "constrained horn-clause (CHC) functionality to synthesize some of the" + , "loop's properties." + ] + , prim "llvm_verify_x86_with_invariant" "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> (String, Int, Term) -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec" (pureVal llvm_verify_x86_with_invariant) From 5fc0d5ff7d389905e03c6f854682e52274d9b31b Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 8 Mar 2024 13:10:03 -0500 Subject: [PATCH 22/27] Only enable doPtrCmp optimizations with SimpleFixpointCHC --- src/SAWScript/Crucible/LLVM/X86.hs | 31 +++++++++++++++++------------- 1 file changed, 18 insertions(+), 13 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 55c4280dd5..bb5b55c220 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -275,9 +275,10 @@ llvmPointerOffset = snd . C.LLVM.llvmPointerView -- the unsigned comparison between pointer1 and pointer2 is equivalent with the -- unsigned comparison between offset1 + 4096 and offset2 + 4096. doPtrCmp :: + FixpointSelect -> (sym -> W4.SymBV sym w -> W4.SymBV sym w -> IO (W4.Pred sym)) -> Macaw.PtrOp sym w (C.RegValue sym C.BoolType) -doPtrCmp f = Macaw.ptrOp $ \bak mem w xPtr xBits yPtr yBits x y -> do +doPtrCmp fixpointSelect f = Macaw.ptrOp $ \bak mem w xPtr xBits yPtr yBits x y -> do let sym = backendGetSym bak let ptr_as_bv_for_cmp ptr = do page_size <- W4.bvLit sym (W4.bvWidth $ llvmPointerOffset ptr) $ @@ -301,16 +302,20 @@ doPtrCmp f = Macaw.ptrOp $ \bak mem w xPtr xBits yPtr yBits x y -> do =<< W4.andPred sym ok_x ok_y res_both_bits <- f sym (llvmPointerOffset x) (llvmPointerOffset y) res_both_ptrs <- f sym x_ptr_as_bv y_ptr_as_bv - - if| Just True <- W4.asConstantPred both_bits -> - return res_both_bits - | Just True <- W4.asConstantPred both_ptrs -> do - C.assert bak ok_both_ptrs $ C.AssertFailureSimError "" "" - return res_both_ptrs - | otherwise -> do - undef <- Macaw.mkUndefinedBool sym "ptr_cmp" - W4.itePred sym both_bits res_both_bits - =<< W4.itePred sym ok_both_ptrs res_both_ptrs undef + let ptrCmpDefault = do + undef <- Macaw.mkUndefinedBool sym "ptr_cmp" + W4.itePred sym both_bits res_both_bits + =<< W4.itePred sym ok_both_ptrs res_both_ptrs undef + case fixpointSelect of + SimpleFixpointCHC{} -> + if | Just True <- W4.asConstantPred both_bits -> + return res_both_bits + | Just True <- W4.asConstantPred both_ptrs -> do + C.assert bak ok_both_ptrs $ C.AssertFailureSimError "" "" + return res_both_ptrs + | otherwise -> + ptrCmpDefault + _ -> ptrCmpDefault ------------------------------------------------------------------------------- -- ** Entrypoint @@ -531,8 +536,8 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec archEvalFns mvar mmConf sawMacawExtensions = defaultMacawExtensions_x86_64 { C.extensionExec = \s0 st -> case s0 of - Macaw.PtrLt w x y -> doPtrCmp W4.bvUlt st mvar w x y - Macaw.PtrLeq w x y -> doPtrCmp W4.bvUle st mvar w x y + Macaw.PtrLt w x y -> doPtrCmp fixpointSelect W4.bvUlt st mvar w x y + Macaw.PtrLeq w x y -> doPtrCmp fixpointSelect W4.bvUle st mvar w x y _ -> (C.extensionExec defaultMacawExtensions_x86_64) s0 st } ctx :: C.SimContext (Macaw.MacawSimulatorState Sym) Sym (Macaw.MacawExt Macaw.X86_64) From 9ee45fdb7c5a6b923b081f98d6591ca92f32a8a4 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 11 Mar 2024 14:53:57 -0400 Subject: [PATCH 23/27] crucible: Revert popFrame refactoring --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index 6b7d94c61f..9913bbc60b 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 6b7d94c61fca303f2ee155e2f3ee6a36ebb804cc +Subproject commit 9913bbc60b293db332ae127d7eae0b950964155a From 48dcbf7bc2551709e3dacd5c682795a039ae2635 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 22 Apr 2024 10:00:10 -0400 Subject: [PATCH 24/27] Uniformly apply pushMuxOps option to all ExprBuilders SAW creates a variety of different ExprBuilders in the course of a typical SAW script, but we were only applying the pushMuxOps option to some of them. This patch makes the treatment a bit more comprehensive. Unfortunately, doing so requires a rather uncomfortable amount of extra plumbing in `SAWScript.Proof`, but I'm not sure how to do better without refactoring all of `SAWScript.Proof` to use `TopLevel` instead of `IO` (and it's unclear if that is desirable). --- src/SAWScript/Builtins.hs | 6 ++- src/SAWScript/Crucible/Common.hs | 10 +++-- src/SAWScript/Crucible/JVM/Builtins.hs | 2 +- src/SAWScript/Crucible/JVM/BuiltinsJVM.hs | 2 +- src/SAWScript/Crucible/LLVM/Builtins.hs | 2 +- src/SAWScript/Crucible/LLVM/X86.hs | 2 +- src/SAWScript/Crucible/MIR/Builtins.hs | 2 +- src/SAWScript/Proof.hs | 38 ++++++++-------- src/SAWScript/Prover/Exporter.hs | 16 ++++--- src/SAWScript/Prover/What4.hs | 53 +++++++++++++++-------- src/SAWScript/Value.hs | 3 +- src/SAWScript/X86.hs | 2 +- src/SAWScript/Yosys.hs | 2 +- 13 files changed, 86 insertions(+), 54 deletions(-) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index f262c70629..1e5816455d 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -717,7 +717,8 @@ goal_eval unints = execTactic $ tacticChange $ \goal -> do sc <- getSharedContext unintSet <- resolveNames unints - sqt' <- traverseSequentWithFocus (io . evalProp sc unintSet) (goalSequent goal) + what4PushMuxOps <- gets rwWhat4PushMuxOps + sqt' <- traverseSequentWithFocus (io . evalProp sc what4PushMuxOps unintSet) (goalSequent goal) return (sqt', EvalEvidence unintSet) extract_uninterp :: @@ -2097,7 +2098,8 @@ specialize_theorem thm ts = do sc <- getSharedContext db <- SV.getTheoremDB pos <- SV.getPosition - (thm', db') <- io (specializeTheorem sc db pos "specialize_theorem" thm (map ttTerm ts)) + what4PushMuxOps <- gets rwWhat4PushMuxOps + (thm', db') <- io (specializeTheorem sc what4PushMuxOps db pos "specialize_theorem" thm (map ttTerm ts)) SV.putTheoremDB db' SV.returnProof thm' diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs index 61c8e60fa0..6c353abae4 100644 --- a/src/SAWScript/Crucible/Common.hs +++ b/src/SAWScript/Crucible/Common.hs @@ -45,6 +45,7 @@ import qualified What4.Protocol.SMTLib2 as SMT2 import qualified What4.Config as W4 import qualified What4.Expr as W4 +import qualified What4.Expr.Builder as W4 import qualified What4.Interface as W4 import qualified What4.ProgramLoc as W4 (plSourceLoc) @@ -76,10 +77,13 @@ data SAWCruciblePersonality sym = SAWCruciblePersonality sawCoreState :: Sym -> IO (SAWCoreState Nonce.GlobalNonceGenerator) sawCoreState sym = pure (sym ^. W4.userState) -newSAWCoreExprBuilder :: SC.SharedContext -> IO Sym -newSAWCoreExprBuilder sc = +newSAWCoreExprBuilder :: SC.SharedContext -> Bool -> IO Sym +newSAWCoreExprBuilder sc what4PushMuxOps = do st <- newSAWCoreState sc - W4.newExprBuilder W4.FloatRealRepr st Nonce.globalNonceGenerator + sym <- W4.newExprBuilder W4.FloatRealRepr st Nonce.globalNonceGenerator + pushMuxOpsSetting <- W4.getOptionSetting W4.pushMuxOpsOption $ W4.getConfiguration sym + _ <- W4.setOpt pushMuxOpsSetting what4PushMuxOps + pure sym defaultSAWCoreBackendTimeout :: Integer defaultSAWCoreBackendTimeout = 10000 diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index f2a55d93b4..53d5f1c1d5 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -841,7 +841,7 @@ setupCrucibleContext jclass = cb <- getJavaCodebase sc <- getSharedContext pathSatSolver <- gets rwPathSatSolver - sym <- io $ newSAWCoreExprBuilder sc + sym <- io $ newSAWCoreExprBuilder sc False bak <- io $ newSAWCoreBackend pathSatSolver sym opts <- getOptions io $ CJ.setSimulatorVerbosity (simVerbose opts) sym diff --git a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs index 0ea687e26f..4ed6096231 100644 --- a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs +++ b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs @@ -159,7 +159,7 @@ jvm_extract c mname = do ctx <- getJVMTrans io $ do -- only the IO monad, nothing else - sym <- newSAWCoreExprBuilder sc + sym <- newSAWCoreExprBuilder sc False SomeOnlineBackend bak <- newSAWCoreBackend pathSatSolver sym st <- sawCoreState sym CJ.setSimulatorVerbosity verbosity sym diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 17c48842ce..e088a3e835 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -1773,7 +1773,7 @@ setupLLVMCrucibleContext pathSat lm action = cc <- io $ do let verbosity = simVerbose opts - sym <- Common.newSAWCoreExprBuilder sc + sym <- Common.newSAWCoreExprBuilder sc False Common.SomeOnlineBackend bak <- Common.newSAWCoreBackendWithTimeout pathSatSolver sym crucibleTimeout diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index bb5b55c220..57fdf0277b 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -421,7 +421,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec opts <- getOptions basic_ss <- getBasicSS rw <- getTopLevelRW - sym <- liftIO $ newSAWCoreExprBuilder sc + sym <- liftIO $ newSAWCoreExprBuilder sc False mdMap <- liftIO $ newIORef mempty SomeOnlineBackend bak <- liftIO $ newSAWCoreBackendWithTimeout pathSatSolver sym $ rwCrucibleTimeout rw diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index 37f0de32db..28fae3a3b2 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -1382,7 +1382,7 @@ setupCrucibleContext rm = do halloc <- getHandleAlloc sc <- getSharedContext pathSatSolver <- gets rwPathSatSolver - sym <- io $ newSAWCoreExprBuilder sc + sym <- io $ newSAWCoreExprBuilder sc False someBak@(SomeOnlineBackend bak) <- io $ newSAWCoreBackend pathSatSolver sym let cs = rm ^. Mir.rmCS let col = cs ^. Mir.collection diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs index cb685c2889..65a9e25547 100644 --- a/src/SAWScript/Proof.hs +++ b/src/SAWScript/Proof.hs @@ -466,15 +466,15 @@ unbindAndFreshenProp sc (Prop p0) = loop [] [] p0 -- | Evaluate the given proposition by round-tripping -- through the What4 formula representation. This will -- perform a variety of simplifications and rewrites. -evalProp :: SharedContext -> Set VarIndex -> Prop -> IO Prop -evalProp sc unints p = +evalProp :: SharedContext -> Bool -> Set VarIndex -> Prop -> IO Prop +evalProp sc what4PushMuxOps unints p = do (ecs, body) <- unbindAndFreshenProp sc p body' <- case asEqTrue body of Just t -> pure t Nothing -> fail ("goal_eval: expected EqTrue\n" ++ scPrettyTerm defaultPPOpts (unProp p)) - sym <- Common.newSAWCoreExprBuilder sc + sym <- Common.newSAWCoreExprBuilder sc what4PushMuxOps st <- Common.sawCoreState sym (_names, (_mlabels, p')) <- W4Sim.w4Eval sym st sc mempty unints body' t1 <- W4Sim.toSC sym st p' @@ -949,11 +949,11 @@ reachableTheorems db roots = Set.foldl' (loop (theoremMap db)) mempty roots -- does not totally guarantee the theorem is true, as it does -- not verify any solver-provided proofs, and it accepts admitted -- propositions and quickchecked propositions as valid. -validateTheorem :: SharedContext -> TheoremDB -> Theorem -> IO () +validateTheorem :: SharedContext -> Bool -> TheoremDB -> Theorem -> IO () -validateTheorem sc db Theorem{ _thmProp = p, _thmEvidence = e, _thmDepends = thmDep } = +validateTheorem sc what4PushMuxOps db Theorem{ _thmProp = p, _thmEvidence = e, _thmDepends = thmDep } = do let hyps = Map.keysSet (theoremMap db) - (deps,_) <- checkEvidence sc e p + (deps,_) <- checkEvidence sc what4PushMuxOps e p unless (Set.isSubsetOf deps thmDep && Set.isSubsetOf thmDep hyps) (fail $ unlines ["Theorem failed to declare its dependencies correctly" , show deps, show thmDep ]) @@ -1188,6 +1188,7 @@ proofByTerm sc db prf loc rsn = -- error will be raised. constructTheorem :: SharedContext -> + Bool -> TheoremDB -> Prop -> Evidence -> @@ -1196,8 +1197,8 @@ constructTheorem :: Text -> NominalDiffTime -> IO (Theorem, TheoremDB) -constructTheorem sc db p e loc ploc rsn elapsed = - do (deps,sy) <- checkEvidence sc e p +constructTheorem sc what4PushMuxOps db p e loc ploc rsn elapsed = + do (deps,sy) <- checkEvidence sc what4PushMuxOps e p n <- freshNonce globalNonceGenerator let thm = Theorem @@ -1220,14 +1221,14 @@ constructTheorem sc db p e loc ploc rsn elapsed = -- specializes the leading quantifiers with the given terms. -- This will fail if the given terms to not match the quantifier structure -- of the given theorem. -specializeTheorem :: SharedContext -> TheoremDB -> Pos -> Text -> Theorem -> [Term] -> IO (Theorem, TheoremDB) -specializeTheorem _sc db _loc _rsn thm [] = return (thm, db) -specializeTheorem sc db loc rsn thm ts = +specializeTheorem :: SharedContext -> Bool -> TheoremDB -> Pos -> Text -> Theorem -> [Term] -> IO (Theorem, TheoremDB) +specializeTheorem _sc _what4PushMuxOps db _loc _rsn thm [] = return (thm, db) +specializeTheorem sc what4PushMuxOps db loc rsn thm ts = do res <- specializeProp sc (_thmProp thm) ts case res of Left err -> fail (unlines (["specialize_theorem: failed to specialize"] ++ TC.prettyTCError err)) Right p' -> - constructTheorem sc db p' (ApplyEvidence thm (map Left ts)) loc Nothing rsn 0 + constructTheorem sc what4PushMuxOps db p' (ApplyEvidence thm (map Left ts)) loc Nothing rsn 0 specializeProp :: SharedContext -> Prop -> [Term] -> IO (Either TC.TCError Prop) specializeProp sc (Prop p0) ts0 = TC.runTCM (loop p0 ts0) sc Nothing [] @@ -1528,8 +1529,9 @@ normalizeConclBoolCommit sc b = -- | Verify that the given evidence in fact supports the given proposition. -- Returns the identifiers of all the theorems depended on while checking evidence. -checkEvidence :: SharedContext -> Evidence -> Prop -> IO (Set TheoremNonce, TheoremSummary) -checkEvidence sc = \e p -> do nenv <- scGetNamingEnv sc +checkEvidence :: SharedContext -> Bool -> Evidence -> Prop -> IO (Set TheoremNonce, TheoremSummary) +checkEvidence sc what4PushMuxOps = \e p -> do + nenv <- scGetNamingEnv sc check nenv e (propToSequent p) where @@ -1683,7 +1685,7 @@ checkEvidence sc = \e p -> do nenv <- scGetNamingEnv sc check nenv e' sqt' EvalEvidence vars e' -> - do sqt' <- traverseSequentWithFocus (evalProp sc vars) sqt + do sqt' <- traverseSequentWithFocus (evalProp sc what4PushMuxOps vars) sqt check nenv e' sqt' ConversionEvidence sqt' e' -> @@ -1814,17 +1816,19 @@ finishProof :: ProofState -> Bool {- ^ should we record the theorem in the database? -} -> Bool {- ^ do we need to normalize the sequent to match the final goal ? -} -> + Bool {- ^ If 'True', push certain @ExprBuilder@ operations (e.g., @zext@) down + to the branches of @ite@ expressions -} -> IO (ProofResult, TheoremDB) finishProof sc db conclProp ps@(ProofState gs (concl,loc,ploc,rsn) stats _ checkEv start) - recordThm useSequentGoals = + recordThm useSequentGoals what4PushMuxOps = case gs of [] -> do e <- checkEv [] let e' = if useSequentGoals then NormalizeSequentEvidence concl e else e - (deps,sy) <- checkEvidence sc e' conclProp + (deps,sy) <- checkEvidence sc what4PushMuxOps e' conclProp n <- freshNonce globalNonceGenerator end <- getCurrentTime let theorem = diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs index 12c4ed2293..951446c3cb 100644 --- a/src/SAWScript/Prover/Exporter.hs +++ b/src/SAWScript/Prover/Exporter.hs @@ -49,6 +49,7 @@ import Data.Foldable(toList) import Control.Monad (unless) import Control.Monad.Except (runExceptT) +import Control.Monad.State (gets) import qualified Data.AIG as AIG import qualified Data.ByteString as BS import Data.Maybe (mapMaybe) @@ -103,7 +104,7 @@ import SAWScript.Value import qualified What4.Interface as W4 import qualified What4.Expr.Builder as W4 -import What4.Config (extendConfig) +import What4.Config (extendConfig, getOptionSetting, setOpt) import What4.Interface (getConfiguration, IsSymExprBuilder) import What4.Protocol.SMTLib2 (writeDefaultSMT2) import What4.Protocol.SMTLib2.Response (smtParseOptions) @@ -312,11 +313,16 @@ writeSMTLib2 f satq = getSharedContext >>= \sc -> io $ -- | Write a SAT query an SMT-Lib version 2 file. -- This version uses What4 instead of SBV. writeSMTLib2What4 :: FilePath -> SATQuery -> TopLevel () -writeSMTLib2What4 f satq = getSharedContext >>= \sc -> io $ - do sym <- W4.newExprBuilder W4.FloatRealRepr St globalNonceGenerator +writeSMTLib2What4 f satq = do + sc <- getSharedContext + what4PushMuxOps <- gets rwWhat4PushMuxOps + io $ do + sym <- W4.newExprBuilder W4.FloatRealRepr St globalNonceGenerator (_varMap, lits) <- W.w4Solve sym sc satq let cfg = getConfiguration sym extendConfig smtParseOptions cfg + pushMuxOpsSetting <- getOptionSetting W4.pushMuxOpsOption cfg + _ <- setOpt pushMuxOpsSetting what4PushMuxOps withFile f WriteMode $ \h -> writeDefaultSMT2 () "Offline SMTLib2" defaultWriteSMTLIB2Features Nothing sym h lits @@ -328,7 +334,7 @@ write_verilog sc path t = io $ writeVerilog sc path t writeVerilogSAT :: FilePath -> SATQuery -> TopLevel [(ExtCns Term, FiniteType)] writeVerilogSAT path satq = getSharedContext >>= \sc -> io $ - do sym <- newSAWCoreExprBuilder sc + do sym <- newSAWCoreExprBuilder sc False -- For SAT checking, we don't care what order the variables are in, -- but only that we can correctly keep track of the connection -- between inputs and assignments. @@ -380,7 +386,7 @@ flattenSValue _ sval = fail $ "write_verilog: unsupported result type: " ++ show writeVerilog :: SharedContext -> FilePath -> Term -> IO () writeVerilog sc path t = do - sym <- newSAWCoreExprBuilder sc + sym <- newSAWCoreExprBuilder sc False st <- sawCoreState sym -- For writing Verilog in the general case, it's convenient for any -- lambda-bound inputs to appear first in the module input list, in diff --git a/src/SAWScript/Prover/What4.hs b/src/SAWScript/Prover/What4.hs index 52de3e941e..69f289d6c8 100644 --- a/src/SAWScript/Prover/What4.hs +++ b/src/SAWScript/Prover/What4.hs @@ -9,6 +9,7 @@ module SAWScript.Prover.What4 where import Control.Lens ((^.)) +import Control.Monad.State (gets) import Data.List (nub) import Data.Set (Set) import qualified Data.Map as Map @@ -20,7 +21,7 @@ import Verifier.SAW.FiniteValue import Verifier.SAW.SATQuery (SATQuery(..)) import SAWScript.Proof(Sequent, sequentToSATQuery, CEX) -import SAWScript.Value (TopLevel, io, getSharedContext) +import SAWScript.Value (TopLevel, io, getSharedContext, rwWhat4PushMuxOps) import Data.Parameterized.Nonce @@ -41,15 +42,21 @@ import qualified What4.Expr.Builder as B -- trivial state data St t = St -setupWhat4_sym :: Bool -> IO (B.ExprBuilder - GlobalNonceGenerator - St - (B.Flags B.FloatReal)) -setupWhat4_sym hashConsing = +setupWhat4_sym :: + Bool -> + Bool -> + IO (B.ExprBuilder + GlobalNonceGenerator + St + (B.Flags B.FloatReal)) +setupWhat4_sym hashConsing what4PushMuxOps = do -- TODO: get rid of GlobalNonceGenerator ??? sym <- B.newExprBuilder B.FloatRealRepr St globalNonceGenerator - cacheTermsSetting <- getOptionSetting B.cacheTerms $ getConfiguration sym + let cfg = getConfiguration sym + cacheTermsSetting <- getOptionSetting B.cacheTerms cfg _ <- setOpt cacheTermsSetting hashConsing + pushMuxOpsSetting <- getOptionSetting B.pushMuxOpsOption cfg + _ <- setOpt pushMuxOpsSetting what4PushMuxOps return sym what4Theories :: @@ -57,9 +64,11 @@ what4Theories :: Bool -> Sequent -> TopLevel [String] -what4Theories unintSet hashConsing goal = - getSharedContext >>= \sc -> io $ - do sym <- setupWhat4_sym hashConsing +what4Theories unintSet hashConsing goal = do + sc <- getSharedContext + what4PushMuxOps <- gets rwWhat4PushMuxOps + io $ do + sym <- setupWhat4_sym hashConsing what4PushMuxOps satq <- sequentToSATQuery sc unintSet goal (_varMap, lits) <- W.w4Solve sym sc satq let pf lit = (predicateVarInfo lit)^.problemFeatures @@ -86,9 +95,11 @@ proveWhat4_sym :: Bool -> SATQuery -> TopLevel (Maybe CEX, String) -proveWhat4_sym solver hashConsing satq = - getSharedContext >>= \sc -> io $ - do sym <- setupWhat4_sym hashConsing +proveWhat4_sym solver hashConsing satq = do + sc <- getSharedContext + what4PushMuxOps <- gets rwWhat4PushMuxOps + io $ do + sym <- setupWhat4_sym hashConsing what4PushMuxOps proveWhat4_solver solver sym sc satq (return ()) proveExportWhat4_sym :: @@ -97,9 +108,11 @@ proveExportWhat4_sym :: FilePath -> SATQuery -> TopLevel (Maybe CEX, String) -proveExportWhat4_sym solver hashConsing outFilePath satq = - getSharedContext >>= \sc -> io $ - do sym <- setupWhat4_sym hashConsing +proveExportWhat4_sym solver hashConsing outFilePath satq = do + sc <- getSharedContext + what4PushMuxOps <- gets rwWhat4PushMuxOps + io $ do + sym <- setupWhat4_sym hashConsing what4PushMuxOps -- Write smt out (_, _, lits, solver_name) <- setupWhat4_solver solver sym sc satq @@ -131,9 +144,11 @@ proveWhat4_z3_using :: Bool {- ^ Hash-consing of What4 terms -}-> SATQuery {- ^ The query to be proved -} -> TopLevel (Maybe CEX, String) -proveWhat4_z3_using tactic hashConsing satq = - getSharedContext >>= \sc -> io $ - do sym <- setupWhat4_sym hashConsing +proveWhat4_z3_using tactic hashConsing satq = do + sc <- getSharedContext + what4PushMuxOps <- gets rwWhat4PushMuxOps + io $ do + sym <- setupWhat4_sym hashConsing what4PushMuxOps proveWhat4_solver z3Adapter sym sc satq $ do z3TacticSetting <- getOptionSetting z3Tactic $ getConfiguration sym _ <- setOpt z3TacticSetting $ Text.pack tactic diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 5f2a525da8..282ba109f6 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -955,7 +955,8 @@ runProofScript (ProofScript m) concl gl ploc rsn recordThm useSequentGoals = Right _ -> do sc <- getSharedContext db <- getTheoremDB - (thmResult, db') <- io (finishProof sc db concl pstate recordThm useSequentGoals) + what4PushMuxOps <- gets rwWhat4PushMuxOps + (thmResult, db') <- io (finishProof sc db concl pstate recordThm useSequentGoals what4PushMuxOps) putTheoremDB db' pure thmResult diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index e61a44b0dd..c3ef53d37e 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -209,7 +209,7 @@ proof fileReader pss archi file mbCry globs fun = halloc <- newHandleAllocator scLoadPreludeModule sc scLoadCryptolModule sc - sym <- newSAWCoreExprBuilder sc + sym <- newSAWCoreExprBuilder sc False SomeOnlineBackend bak <- newSAWCoreBackend pss sym let ?fileReader = fileReader cenv <- loadCry sym mbCry diff --git a/src/SAWScript/Yosys.hs b/src/SAWScript/Yosys.hs index fbcd657886..2cc2d18667 100644 --- a/src/SAWScript/Yosys.hs +++ b/src/SAWScript/Yosys.hs @@ -252,5 +252,5 @@ yosys_verify_sequential_sally :: TopLevel () yosys_verify_sequential_sally s path q fixed = do sc <- getSharedContext - sym <- liftIO $ Common.newSAWCoreExprBuilder sc + sym <- liftIO $ Common.newSAWCoreExprBuilder sc False queryModelChecker sym sc s path q . Set.fromList $ Text.pack <$> fixed From eeb33b6581629fd22712021a5df3349d1046ae9d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 13 May 2024 16:59:02 -0400 Subject: [PATCH 25/27] Bump cryptol-specs, what4, crucible submodules to latest --- deps/crucible | 2 +- deps/cryptol-specs | 2 +- deps/what4 | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/deps/crucible b/deps/crucible index 9913bbc60b..5040e5709e 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 9913bbc60b293db332ae127d7eae0b950964155a +Subproject commit 5040e5709ed839241ce6e1042a635141f22ac6ea diff --git a/deps/cryptol-specs b/deps/cryptol-specs index 1073bec7ba..4066cc0637 160000 --- a/deps/cryptol-specs +++ b/deps/cryptol-specs @@ -1 +1 @@ -Subproject commit 1073bec7ba9f05b6af1f85adbc43999be568abd1 +Subproject commit 4066cc0637c23c7d880dd0330c332821dc805f2c diff --git a/deps/what4 b/deps/what4 index 72dd5ff574..512eca6637 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit 72dd5ff5741caee5a40ca5f5791201a54f6064b7 +Subproject commit 512eca66373a900be1175c1e06aed4041bcf6f54 From 799d89c48d58f182207ddce4e8d32777f5d92dc7 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 14 May 2024 11:14:54 -0400 Subject: [PATCH 26/27] Bump what4, crucible submodules --- deps/crucible | 2 +- deps/what4 | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/deps/crucible b/deps/crucible index 5040e5709e..ac948b4363 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 5040e5709ed839241ce6e1042a635141f22ac6ea +Subproject commit ac948b4363745e10e2226c843339bad16bf198fa diff --git a/deps/what4 b/deps/what4 index 512eca6637..8c9401b5d2 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit 512eca66373a900be1175c1e06aed4041bcf6f54 +Subproject commit 8c9401b5d21d20451d224d4834bd611fc83b850b From adb59e2c7594979acc25cc7128d95431ff0cc321 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 14 May 2024 09:14:52 -0400 Subject: [PATCH 27/27] Adapt to recent crucible-llvm API changes --- src/SAWScript/Crucible/LLVM/Builtins.hs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index e088a3e835..cb38394fa2 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -167,6 +167,7 @@ import qualified Lang.Crucible.Simulator.PathSatisfiability as Crucible import qualified Lang.Crucible.LLVM.ArraySizeProfile as Crucible import qualified Lang.Crucible.LLVM.DataLayout as Crucible import qualified Lang.Crucible.LLVM.Bytes as Crucible +import qualified Lang.Crucible.LLVM.Functions 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 @@ -1820,7 +1821,9 @@ setupLLVMCrucibleContext pathSat lm action = do -- register all the functions defined in the LLVM module Crucible.registerLazyModule (handleTranslationWarning opts) mtrans -- register the callable override functions - Crucible.register_llvm_overrides llvm_mod saw_llvm_overrides saw_llvm_overrides ctx + _ <- Crucible.register_llvm_overrides llvm_mod saw_llvm_overrides saw_llvm_overrides ctx + + pure () let initExecState = Crucible.InitialState simctx globals Crucible.defaultAbortHandler Crucible.UnitRepr $ @@ -1856,19 +1859,20 @@ handleTranslationWarning opts (Crucible.LLVMTranslationWarning s p msg) = saw_llvm_overrides :: ( Crucible.IsSymInterface sym, Crucible.HasLLVMAnn sym, Crucible.HasPtrWidth wptr ) => - [Crucible.OverrideTemplate p sym arch rtp l a] + [Crucible.OverrideTemplate p sym ext arch] saw_llvm_overrides = [ Crucible.basic_llvm_override saw_assert_override ] saw_assert_override :: ( Crucible.IsSymInterface sym, Crucible.HasLLVMAnn sym, Crucible.HasPtrWidth wptr ) => - Crucible.LLVMOverride p sym + Crucible.LLVMOverride p sym ext (Crucible.EmptyCtx Crucible.::> Crucible.BVType 32) Crucible.UnitType saw_assert_override = [llvmOvr| void @saw_assert( i32 ) |] - (\_memOps bak (Ctx.Empty Ctx.:> p) -> + (\_memOps (Ctx.Empty Ctx.:> p) -> + Crucible.ovrWithBackend $ \bak -> do let sym = Crucible.backendGetSym bak let msg = Crucible.GenericSimError "saw_assert" liftIO $