From cac3dae05765ad6b0752d26887bbf1bdf2acbf7e Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 3 Dec 2023 17:23:53 -0500 Subject: [PATCH 1/2] Introduce OverrideEnv' to OverrideMatcher' This patch adds a `ReaderT` component to the `OverrideMatcher'` monad transformer, where the reader portions are represented with the new `OverrideEnv'` data type. Currently, the only field of `OverrideEnv'` is `_oeConditionalPred`, which is used to represent a path condition for any assumptions or assertions created in a specification. See `Note [oeConditionalPred]` for a lengthier explanation. While introducing this does require a fair bit of refactoring, this patch in isolation does not change any user-visible behavior. In a subsequent commit, we will leverage `oeConditionalPred` to introduce a fix for #1945. --- src/SAWScript/Crucible/Common/Override.hs | 140 +++++++++++++++++++--- src/SAWScript/Crucible/JVM/Override.hs | 6 +- src/SAWScript/Crucible/LLVM/Override.hs | 6 +- src/SAWScript/Crucible/MIR/Override.hs | 6 +- 4 files changed, 138 insertions(+), 20 deletions(-) diff --git a/src/SAWScript/Crucible/Common/Override.hs b/src/SAWScript/Crucible/Common/Override.hs index fac57dcb20..8aa06f14de 100644 --- a/src/SAWScript/Crucible/Common/Override.hs +++ b/src/SAWScript/Crucible/Common/Override.hs @@ -34,6 +34,10 @@ module SAWScript.Crucible.Common.Override , termSub , termEqs -- + , OverrideEnv + , OverrideEnv'(..) + , oeConditionalPred + -- , OverrideFailureReason(..) , ppOverrideFailureReason , OverrideFailure(..) @@ -48,6 +52,7 @@ module SAWScript.Crucible.Common.Override , addTermEq , addAssert , addAssume + , withConditionalPred , readGlobal , writeGlobal , failure @@ -75,6 +80,7 @@ module SAWScript.Crucible.Common.Override import qualified Control.Exception as X import Control.Lens import Control.Monad (foldM, unless, when) +import Control.Monad.Reader (MonadReader(..), ReaderT(..)) import Control.Monad.Trans.State hiding (get, put) import Control.Monad.State.Class (MonadState(..)) import Control.Monad.Error.Class (MonadError) @@ -140,8 +146,19 @@ data OverrideState' sym ext = OverrideState -- | Substitution for SAW Core external constants , _termSub :: Map VarIndex Term - -- | Equalities of SAW Core terms - , _termEqs :: [(Term, ConditionMetadata, Crucible.SimError)] + -- | Equalities of SAW Core terms. The four elements of each tuple are: + -- + -- * A 'W4.Pred' representing the path condition for the part of the + -- program in which the term equality occurs. + -- See @Note [oeConditionalPred]@. + -- + -- * A 'Term' representing the term equality. + -- + -- * A 'ConditionMetadata' value describing the term equality. + -- + -- * A 'Crucible.SimError' to report in the event that the term equality + -- fails to hold. + , _termEqs :: [(W4.Pred sym, Term, ConditionMetadata, Crucible.SimError)] -- | Free variables available for unification , _osFree :: Set VarIndex @@ -188,6 +205,76 @@ initialState sym globals allocs terms free loc = OverrideState , _osLocation = loc } +-------------------------------------------------------------------------------- +-- ** OverrideEnv + +-- | The environment used in the reader portion of `OverrideMatcher'`. +newtype OverrideEnv' sym = OverrideEnv + { _oeConditionalPred :: W4.Pred sym + -- ^ The predicate that is used to construct an implication for any + -- assumption or assertion as part of the specification. + -- See @Note [oeConditionalPred]@. + } + +-- | `OverrideEnv'` instantiated at type 'Sym'. +type OverrideEnv = OverrideEnv' Sym + +makeLenses ''OverrideEnv' + +-- | The initial override matching environment starts with a trivial path +-- condition of @True@ (i.e., 'W4.truePred). See @Note [oeConditionalPred]@. +initialEnv :: + W4.IsExprBuilder sym => + sym -> + OverrideEnv' sym +initialEnv sym = OverrideEnv + { _oeConditionalPred = W4.truePred sym + } + +{- +Note [oeConditionalPred] +~~~~~~~~~~~~~~~~~~~~~~~~ +oeConditionalPred is a predicate that is used to construct an implication for +any assumption or assertion used in a specification. That is, oeConditionalPred +can be thought of as the path condition for the part of the specification where +the assumption/assertion is created. By default, the oeConditionalPred is +simply `True` (see `initialEnv`), so when an assertion is created, e.g., + + llvm_assert {{ x == 2*y }}; + +Then the overall assertion would be `True ==> (x == 2*y)`. An implication with +`True` as the premise is not very interesting, of course, but other parts of +the program may add additional premises (see the `withConditionalPred` +function). + +Currently, the only place in SAW where non-trivial `oeConditionalPred`s are +added is when matching against an `llvm_conditional_points_to` statement. For +instance, consider this spec (taken from #1945): + + let test_spec = do { + p <- llvm_alloc (llvm_int 8); + x <- llvm_fresh_var "x" (llvm_int 8); + llvm_points_to p (llvm_term x); + + llvm_execute_func [p]; + + llvm_conditional_points_to {{ x == 1 }} p (llvm_term {{ 1 : [8] }}); + }; + +The `llvm_conditional_points_to` statement in the postcondition generates an +assertion that checks `x` (the value that `p` points to) against `1 : [8]`. But +we only want to check this under the assumption that `x` already equals `1` due +to the `x == 1` part of the `llvm_conditional_points_to` statement. To do this, +the implementation of `llvm_conditional_points_to` will add `x == 1` to the +oeConditionalPred. This way, the assertion that gets generated will be: + + (x == 1 /\ True) ==> (x == 1) + +Here, leaving out the (x == 1) premise would be catastrophic, as that would +result in the far more general assertion `True ==> (x == 1)`. (This was +ultimately the cause of #1945.) +-} + -------------------------------------------------------------------------------- -- ** OverrideFailureReason @@ -313,18 +400,19 @@ data RW -- the Crucible simulation in order to compute the variable substitution -- and side-conditions needed to proceed. newtype OverrideMatcher' sym ext rorw m a = - OM (StateT (OverrideState' sym ext) (ExceptT (OverrideFailure ext) m) a) + OM (ReaderT (OverrideEnv' sym) (StateT (OverrideState' sym ext) (ExceptT (OverrideFailure ext) m)) a) deriving (Applicative, Functor, Generic, Generic1, Monad, MonadIO, MonadThrow) type OverrideMatcher ext rorw a = OverrideMatcher' Sym ext rorw IO a instance Wrapped (OverrideMatcher' sym ext rorw m a) where +deriving instance Monad m => MonadReader (OverrideEnv' sym) (OverrideMatcher' sym ext rorw m) deriving instance Monad m => MonadState (OverrideState' sym ext) (OverrideMatcher' sym ext rorw m) deriving instance Monad m => MonadError (OverrideFailure ext) (OverrideMatcher' sym ext rorw m) instance MonadTrans (OverrideMatcher' sym ext rorw) where - lift f = OM $ lift $ lift f + lift f = OM $ lift $ lift $ lift f throwOverrideMatcher :: Monad m => String -> OverrideMatcher' sym ext rorw m a throwOverrideMatcher msg = do @@ -337,7 +425,7 @@ instance Monad m => Fail.MonadFail (OverrideMatcher' sym ext rorw m) where -- | "Run" function for OverrideMatcher. The final result and state -- are returned. The state will contain the updated globals and substitutions runOverrideMatcher :: - Monad m => + (Monad m, W4.IsExprBuilder sym) => sym {- ^ simulator -} -> Crucible.SymGlobalState sym {- ^ initial global variables -} -> Map AllocIndex (Pointer' ext sym) {- ^ initial allocation substitution -} -> @@ -347,31 +435,55 @@ runOverrideMatcher :: OverrideMatcher' sym ext md m a {- ^ matching action -} -> m (Either (OverrideFailure ext) (a, OverrideState' sym ext)) runOverrideMatcher sym g a t free loc (OM m) = - runExceptT (runStateT m (initialState sym g a t free loc)) + runExceptT (runStateT (runReaderT m (initialEnv sym)) (initialState sym g a t free loc)) addTermEq :: Term {- ^ term equality -} -> ConditionMetadata -> Crucible.SimError {- ^ reason -} -> OverrideMatcher ext rorw () -addTermEq t md r = - OM (termEqs %= cons (t, md, r)) +addTermEq t md r = do + env <- ask + let cond = env ^. oeConditionalPred + OM (termEqs %= cons (cond, t, md, r)) addAssert :: - Monad m => + (MonadIO m, W4.IsExprBuilder sym) => W4.Pred sym {- ^ property -} -> ConditionMetadata -> Crucible.SimError {- ^ reason -} -> OverrideMatcher' sym ext rorw m () -addAssert p md r = - OM (osAsserts %= cons (md,W4.LabeledPred p r)) +addAssert p md r = do + sym <- getSymInterface + env <- ask + p' <- liftIO $ W4.impliesPred sym (env ^. oeConditionalPred) p + OM (osAsserts %= cons (md,W4.LabeledPred p' r)) addAssume :: - Monad m => + (MonadIO m, W4.IsExprBuilder sym) => W4.Pred sym {- ^ property -} -> ConditionMetadata -> OverrideMatcher' sym ext rorw m () -addAssume p md = OM (osAssumes %= cons (md,p)) +addAssume p md = do + sym <- getSymInterface + env <- ask + p' <- liftIO $ W4.impliesPred sym (env ^. oeConditionalPred) p + OM (osAssumes %= cons (md,p')) + +-- | Add an additional premise to the path condition when executing an +-- `OverrideMatcher'` subcomputation. See @Note [oeConditionalPred]@ for an +-- explanation of where this is used. +withConditionalPred :: + (MonadIO m, W4.IsExprBuilder sym) => + W4.Pred sym {- ^ The additional premise -} -> + OverrideMatcher' sym ext rorw m a {- ^ The subcomputation -} -> + OverrideMatcher' sym ext rorw m a +withConditionalPred premise om = do + sym <- getSymInterface + env <- ask + premise' <- liftIO $ W4.andPred sym premise (env ^. oeConditionalPred) + let env' = env & oeConditionalPred .~ premise' + local (const env') om readGlobal :: Monad m => @@ -397,7 +509,7 @@ failure :: W4.ProgramLoc -> OverrideFailureReason ext -> OverrideMatcher' sym ext md m a -failure loc e = OM (lift (throwE (OF loc e))) +failure loc e = OM (lift (lift (throwE (OF loc e)))) getSymInterface :: Monad m => OverrideMatcher' sym ext md m sym getSymInterface = OM (use syminterface) diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 680686ac8c..1bf1777e67 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -358,9 +358,11 @@ assertTermEqualities :: JVMCrucibleContext -> OverrideMatcher CJ.JVM md () assertTermEqualities sc cc = do - let assertTermEquality (t, md, e) = do + let sym = cc ^. jccSym + let assertTermEquality (cond, t, md, e) = do p <- instantiateExtResolveSAWPred sc cc t - addAssert p md e + p' <- liftIO $ W4.impliesPred sym cond p + addAssert p' md e traverse_ assertTermEquality =<< OM (use termEqs) diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 44dc4f89e4..1a0d1ed882 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -708,9 +708,11 @@ assertTermEqualities :: LLVMCrucibleContext arch -> OverrideMatcher (LLVM arch) md () assertTermEqualities sc cc = do - let assertTermEquality (t, md, e) = do + let sym = cc ^. ccSym + let assertTermEquality (cond, t, md, e) = do p <- instantiateExtResolveSAWPred sc cc t - addAssert p md e + p' <- liftIO $ W4.impliesPred sym cond p + addAssert p' md e traverse_ assertTermEquality =<< OM (use termEqs) diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index 0cee024cc5..666fcec74c 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -96,9 +96,11 @@ assertTermEqualities :: MIRCrucibleContext -> OverrideMatcher MIR md () assertTermEqualities sc cc = do - let assertTermEquality (t, md, e) = do + let sym = cc ^. mccSym + let assertTermEquality (cond, t, md, e) = do p <- instantiateExtResolveSAWPred sc cc t - addAssert p md e + p' <- liftIO $ W4.impliesPred sym cond p + addAssert p' md e F.traverse_ assertTermEquality =<< OM (use termEqs) -- | Assign the given reference value to the given allocation index in From 2e60608058fe61bd1365c9f66037cba4abccd03f Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 3 Dec 2023 17:29:51 -0500 Subject: [PATCH 2/2] Properly extend path condition for `llvm_conditional_points_to` This leverages the newly introduced `withConditionalPred` function (see the parent commit) to make `llvm_conditional_points_to cond ptr val` properly extend the path condition with `cond` before matching `val` against the value that `ptr` points to. Fixes #1945. --- intTests/test1945/Makefile | 11 ++++++++++ intTests/test1945/test.bc | Bin 0 -> 2760 bytes intTests/test1945/test.c | 3 +++ intTests/test1945/test.saw | 17 ++++++++++++++++ intTests/test1945/test.sh | 3 +++ src/SAWScript/Crucible/LLVM/Override.hs | 26 ++++++++++++++++++------ 6 files changed, 54 insertions(+), 6 deletions(-) create mode 100644 intTests/test1945/Makefile create mode 100644 intTests/test1945/test.bc create mode 100644 intTests/test1945/test.c create mode 100644 intTests/test1945/test.saw create mode 100755 intTests/test1945/test.sh diff --git a/intTests/test1945/Makefile b/intTests/test1945/Makefile new file mode 100644 index 0000000000..ebf9cc47cc --- /dev/null +++ b/intTests/test1945/Makefile @@ -0,0 +1,11 @@ +CC = clang +CFLAGS = -g -frecord-command-line -O0 + +all: test.bc + +test.bc: test.c + $(CC) $(CFLAGS) -c -emit-llvm $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc diff --git a/intTests/test1945/test.bc b/intTests/test1945/test.bc new file mode 100644 index 0000000000000000000000000000000000000000..f30cc928b26f7b5ec2788b1760845c32a16205c3 GIT binary patch literal 2760 zcma)8eM}q46(3{AV}ec1Un-kbMk=Iwj)es5-*9djF&a)b^bgxqqv>br0M*?0A;**8nhvF#$zY2^s@6(Lko zq(#8cYtV6`@>)|?a#pG|*(OD!^5X|&6&lIU+^q6+QS)R;^Qh8PZk4INchJ;4-WFQa zR<<1CCzMT-Mc%CJ!*a^eI!=8oGBuB?PU=o3jhAOGT%#7VVD}1z5CPnDOjb;}Taosg zRntoCaUd1nkdNI+I-9*0s4DMBV})qCvQamIn$1e5?B>Zo*otThoIR&Ps2%nnZLNI% zH8fEO73;*5Toy_4AwM7Xi{o)V8p6XmJcJe!>Qxc7rd6+}OIOq6eJ#0~F3qROdkM`( zlV)vGvyvcpMQUV4vcWiCo5Djf9A{xWAMtYoGCbUfSZ~yIbm=bm?MRlba`(z?xID()7lXXim(g_)wCM=u334v?o&JQ>A&9KqH!k zCe8gcxtlJ{rOAba=8GmUrC}{9e0fe>+bNFB@k2>m+sO_1@nt7xndXOdf;cqIhm*pB z%X6F^$%b#@K^rarsEFjBrx|O#QbyMW*JK^ZjrunQNy^yI+~eiX7NxQN2dGb zkC5WAl6b}vW_hz_VO|Zn@zDng%ebRCaYNS8Fd=Tp#U}t#@5=B{8y^B}g~S7KK1A^q zxiTW3B(`WpkXCH(5qlkkS-Gg*0Gw&n3oeb1zGA<_*_R!*S#kXxu6|T(&+U~DIPtrF zTql4P*RcXtLQXuO!voI`fZ0Ko?~?KTDn1OkpH7^5vPV4GB>p)^QAh z+{s5(d^E*Z+2iJcDOIbHepybG#Py}I>!UaNkjRWEAQkilK;8$RlN`yEHa zZLw{Nv*kMPK=vWnVeqq!9}EEihbV-`0ApcI8|4_6R}_a$ZB%7q;@Y(bEh(kWTW>Tq zzn9ehGE09@Bt69@DrzPttIkA9qD&-O?J@ZKdKp7_$QA7FiFo>=QA10gC)UdZqY*=! z%X29Z>;@jW#PswSBCep<-4_QwsE>HUfl$;C2u9C?orpoOX0+8<7>|jejqW;=kM=NL zuhCUkQ|B`KT(vfn$yejE{=gjzMq`wx2R=v*FyTm`FGv|{s_AN4Z;TZtjn&4ML08yE z{cwM}g>lEask1>}-z&|a$L|VvMFPW2$5{u}&I~X;9cNGP4`PE+m%E4YgfnL3_#^4SF4f`(WyD7ad%y|03UcINUw--Xx_XL6rrGJyA^d3sj z^ai4OVIQ@BV3fXZf8_QcR4E&$M_75KOlBNm%RvH0I^GsJ${-=a!v>8)i0%+cn&})} zGiJ{0sg~uAXq#DH`V-PYnijuxbQ8*6I|>)F+n^`+Kg zEBX!GKU(mifZT4OUS6x&b`qa=Kp84_ zgkn^D-a$N@VH0>rSGXnOJRn@Ck;}Ym@;kjB) zli7V>iykNug4-40T>TBsejP3caYKr$hl?Va5su15A>;>sSkhDv&jWf3`mrI@~S-bupyV0Q#6RGxljkMKm@!8A(a*u_! z7-?^v*XH)nF1NYX>$7!ry)+pMMgrYI#!CsfjYBNI`!)9zU5s<0Mx^{j;dexJ9=)Mt z=Tk*WF{R=faHEuAk!&U_I%R4To6)Dj2_W_~;T#hkan2nnh%l>xL2co;3awJ8cjk%` z)q!HWd`q5VkE~G$Ip1-%D<|PGGM5#(lM6GVGMR*ShY%%`wvK!SuQc}rh~iH`zLQgx zi(^uhGE48W?~9ORQTUATX8%YsC#0m%`YD9OFftL!W25Mb@XQq&11pZh=#Y3yC*)ID z1HXKQoVNoPbe+(JCUC*-xFA3i;yDam4_&~>E2FRGK~-2UaG|}L7dSZnHLBXz0mKS( y0vGhMQ!s$`4)`YMz_*AX3-}Rgy4vgRuJ$r;6@;1nOXww#LZ1I&X}|7;ZRo!ROp4I} literal 0 HcmV?d00001 diff --git a/intTests/test1945/test.c b/intTests/test1945/test.c new file mode 100644 index 0000000000..32ff9ad7fa --- /dev/null +++ b/intTests/test1945/test.c @@ -0,0 +1,3 @@ +#include + +void test(uint8_t *x) {} diff --git a/intTests/test1945/test.saw b/intTests/test1945/test.saw new file mode 100644 index 0000000000..2475cf87d8 --- /dev/null +++ b/intTests/test1945/test.saw @@ -0,0 +1,17 @@ +// Test a use of `llvm_conditional_points_to` where the value that the pointer +// points to will fail to match against the right-hand side value unless the +// condition is properly incorporated into the path condition. This serves as +// a regression test for https://github.com/GaloisInc/saw-script/issues/1945. + +let test_spec = do { + p <- llvm_alloc (llvm_int 8); + x <- llvm_fresh_var "x" (llvm_int 8); + llvm_points_to p (llvm_term x); + + llvm_execute_func [p]; + + llvm_conditional_points_to {{ x == 1 }} p (llvm_term {{ 1 : [8] }}); +}; + +m <- llvm_load_module "test.bc"; +llvm_verify m "test" [] false test_spec z3; diff --git a/intTests/test1945/test.sh b/intTests/test1945/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test1945/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 1a0d1ed882..8174385b8a 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1410,14 +1410,28 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val = let badLoadSummary = summarizeBadLoad cc memTy prepost ptr case res of Crucible.NoErr pred_ res_val -> do - pred_' <- case maybe_cond of - Just cond -> do - cond' <- instantiateExtResolveSAWPred sc cc (ttTerm cond) - liftIO $ W4.impliesPred sym cond' pred_ - Nothing -> return pred_ + -- If dealing with an `llvm_conditional_points_to` statement, + -- convert the condition to a `Pred`. If dealing with an + -- ordinary `llvm_points_to` statement, this condition will + -- simply be `True`. + cond' <- case maybe_cond of + Just cond -> + instantiateExtResolveSAWPred sc cc (ttTerm cond) + Nothing -> + pure $ W4.truePred sym + -- Next, construct an implication involving the condition and + -- assert it. + pred_' <- liftIO $ W4.impliesPred sym cond' pred_ addAssert pred_' md $ Crucible.SimError loc $ Crucible.AssertFailureSimError (show $ PP.vcat badLoadSummary) "" - pure Nothing <* matchArg opts sc cc spec prepost md res_val memTy val' + + -- Finally, match the value that the pointer points to against + -- the right-hand side value in the points_to statement. Make + -- sure to execute this match with an extended path condition + -- that takes the condition above into account. See also + -- Note [oeConditionalPred] in SAWScript.Crucible.Common.Override. + withConditionalPred cond' $ + pure Nothing <* matchArg opts sc cc spec prepost md res_val memTy val' _ -> do pure $ Just $ describeConcreteMemoryLoadFailure mem badLoadSummary ptr