diff --git a/src/SAWScript/Crucible/Common/Override.hs b/src/SAWScript/Crucible/Common/Override.hs index aa9296bbae..2e8ac639f4 100644 --- a/src/SAWScript/Crucible/Common/Override.hs +++ b/src/SAWScript/Crucible/Common/Override.hs @@ -22,6 +22,7 @@ module SAWScript.Crucible.Common.Override ( Pointer , OverrideState(..) , osAsserts + , osArgAsserts , osAssumes , osFree , osLocation @@ -104,6 +105,11 @@ data OverrideState ext = OverrideState -- | Accumulated assertions , _osAsserts :: [LabeledPred Sym] + -- | Assertions about the values of function arguments + -- + -- These come from @crucible_execute_func@. + , _osArgAsserts :: [[W4.LabeledPred (W4.Pred Sym) PP.Doc]] + -- | Accumulated assumptions , _osAssumes :: [W4.Pred Sym] @@ -131,6 +137,7 @@ initialState :: OverrideState ext initialState sym globals allocs terms free loc = OverrideState { _osAsserts = [] + , _osArgAsserts = [] , _osAssumes = [] , _syminterface = sym , _overrideGlobals = globals diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 54b0491805..b72fe13fd2 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -63,7 +63,7 @@ import Control.Monad.State hiding (fail) import Control.Monad.Fail (MonadFail(..)) import qualified Data.Bimap as Bimap import Data.Char (isDigit) -import Data.Foldable (for_, toList, find) +import Data.Foldable (toList, find) import Data.Function import Data.IORef import Data.List @@ -98,7 +98,6 @@ import Data.Parameterized.Some import qualified What4.Concrete as W4 import qualified What4.Config as W4 import qualified What4.FunctionName as W4 -import qualified What4.LabeledPred as W4 import qualified What4.ProgramLoc as W4 import qualified What4.Interface as W4 import qualified What4.Expr.Builder as W4 @@ -863,14 +862,23 @@ verifyPoststate opts sc cc mspec env0 globals ret = (view (MS.csPostState . MS.csFreshVars) mspec)) matchPost <- io $ runOverrideMatcher sym globals env0 terms0 initialFree poststateLoc $ - do matchResult + do -- Assert that the function returned the correct value + retAsserts <- matchResult + liftIO $ forM_ retAsserts $ + Crucible.addAssertion sym . labelWithSimError poststateLoc + (\doc -> unlines [ "When checking a crucible_return statement:" + , show doc + ]) + + -- Assert other post-state conditions (equalities, points-to) learnCond opts sc cc mspec PostState (mspec ^. MS.csPostState) st <- case matchPost of Left err -> fail (show err) Right (_, st) -> return st - io $ for_ (view osAsserts st) $ \(W4.LabeledPred p r) -> - Crucible.addAssertion sym (Crucible.LabeledPred p r) + + io $ mapM_ (Crucible.addAssertion sym) (st ^. osAsserts) + when (not (null (st ^. osArgAsserts))) $ fail "verifyPoststate: impossible" obligations <- io $ Crucible.getProofObligations sym io $ Crucible.clearProofObligations sym @@ -890,7 +898,7 @@ verifyPoststate opts sc cc mspec env0 globals ret = (Just (rty,r), Just expect) -> matchArg opts sc cc mspec PostState r rty expect (Nothing , Just _ ) -> fail "verifyPoststate: unexpected crucible_return specification" - _ -> return () + _ -> return [] -------------------------------------------------------------------------------- diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 5bf03ce4a2..71c8eb10f1 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -30,9 +30,12 @@ module SAWScript.Crucible.LLVM.Override ( OverrideMatcher(..) , runOverrideMatcher + , labelWithSimError + , setupValueSub , executeFreshPointer , osAsserts + , osArgAsserts , termSub , learnCond @@ -54,7 +57,7 @@ import Data.Foldable (for_, traverse_) import Data.List (tails) import Data.Map (Map) import qualified Data.Map as Map -import Data.Maybe (fromMaybe, catMaybes) +import Data.Maybe (fromMaybe, catMaybes, maybeToList) import Data.Proxy import Data.Set (Set) import qualified Data.Set as Set @@ -111,8 +114,33 @@ import SAWScript.Crucible.LLVM.ResolveSetupValue import SAWScript.Options import SAWScript.Utils (bullets, handleException) +------------------------------------------------------------------------ + +type LabeledPred' sym = W4.LabeledPred (W4.Pred sym) PP.Doc type LabeledPred sym = W4.LabeledPred (W4.Pred sym) Crucible.SimError +-- | Convert a predicate with a 'PP.Doc' label to one with a 'Crucible.SimError' +labelWithSimError :: + W4.ProgramLoc -> + (PP.Doc -> String) -> + LabeledPred' Sym -> + LabeledPred Sym +labelWithSimError loc conv lp = + lp & W4.labeledPredMsg + %~ (Crucible.SimError loc . Crucible.AssertFailureSimError . conv) + +-- | Retrieve pre-state assertions, ready to be passed to 'Crucible.addAssertion' +prestateAsserts :: OverrideState (LLVM arch) -> [LabeledPred Sym] +prestateAsserts os = (os ^. osAsserts) ++ labelWithArgNum (os ^. osArgAsserts) + where + labelWithArgNum asserts = + foldMap (\(n, as) -> map (helper n) as) (zip [1..] asserts) + where helper :: Int -> LabeledPred' Sym -> LabeledPred Sym + helper n = labelWithSimError (os ^. osLocation) $ \doc -> unlines + ["In argument #" ++ show n ++ " to crucible_execute_func:", show doc] + +------------------------------------------------------------------------ + type instance Pointer (LLVM arch) = LLVMPtr (Crucible.ArchWidth arch) -- | An override packaged together with its preconditions, labeled with some @@ -198,25 +226,23 @@ notEqual :: (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => PrePost -> Options {- ^ output/verbosity options -} -> - W4.ProgramLoc {- ^ where is the assertion from? -} -> LLVMCrucibleContext arch -> SharedContext {- ^ context for constructing SAW terms -} -> MS.CrucibleMethodSpecIR (LLVM arch) {- ^ for name and typing environments -} -> SetupValue (Crucible.LLVM arch) {- ^ the value from the spec -} -> Crucible.LLVMVal Sym {- ^ the value from the simulator -} -> - OverrideMatcher (LLVM arch) w Crucible.SimError -notEqual cond opts loc cc sc spec expected actual = do + OverrideMatcher (LLVM arch) w PP.Doc +notEqual cond opts cc sc spec expected actual = do prettyLLVMVal <- ppLLVMVal cc actual prettySetupLLVMVal <- ppSetupValueAsLLVMVal opts cc sc spec expected - pure $ - Crucible.SimError loc $ Crucible.AssertFailureSimError $ unlines $ - [ "Equality " ++ stateCond cond - , "Expected value (as a SAW value): " - , show (MS.ppSetupValue expected) - , "Expected value (as a Crucible value): " - , show prettySetupLLVMVal - , "Actual value: " - , show prettyLLVMVal + pure $ PP.vcat $ + [ PP.text $ "Equality " ++ stateCond cond + , PP.text "Expected value (as a SAW value): " + , PP.indent 2 (MS.ppSetupValue expected) + , PP.text "Expected value (as a Crucible value): " + , PP.indent 2 prettySetupLLVMVal + , PP.text "Actual value: " + , PP.indent 2 prettyLLVMVal ] ------------------------------------------------------------------------ @@ -366,19 +392,19 @@ methodSpecHandler opts sc cc top_loc css retTy = do MS.ppMethodSpec methodSpec PP.<$$> ppOverrideFailure failureReason in case partitionEithers prestates of - (errs, []) -> - fail $ show $ - PP.text "All overrides failed during structural matching:" - PP.<$$> - PP.vcat - (map (\(cs, err) -> - PP.text "*" PP.<> PP.indent 2 (prettyError cs err)) - (zip css errs)) - PP.<$$> PP.text "Actual function return type: " PP.<> - PP.text (show (retTy)) - (_, ss) -> liftIO $ - forM ss $ \(cs,st) -> - return (OverrideWithPreconditions (st^.osAsserts) cs st) + (errs, []) -> + fail $ show $ + PP.text "All overrides failed during structural matching:" + PP.<$$> + PP.vcat + (map (\(cs, err) -> + PP.text "*" PP.<> PP.indent 2 (prettyError cs err)) + (zip css errs)) + PP.<$$> PP.text "Actual function return type: " PP.<> + PP.text (show (retTy)) + (_, ss) -> liftIO $ + forM ss $ \(cs,st) -> + return (OverrideWithPreconditions (prestateAsserts st) cs st) -- Now we do a second phase of simple compatibility checking: we check to see -- if any of the preconditions of the various overrides are concretely false. @@ -548,7 +574,9 @@ methodSpecHandler_prestate opts sc cc args cs = -- todo: fail if list lengths mismatch xs <- liftIO (zipWithM aux expectedArgTypes (assignmentToList args)) - sequence_ [ matchArg opts sc cc cs PreState x y z | (x, y, z) <- xs] + argAsserts <- forM xs $ \(actual, expectedType, expected) -> + matchArg opts sc cc cs PreState actual expectedType expected + osArgAsserts .= argAsserts learnCond opts sc cc cs PreState (cs ^. MS.csPreState) @@ -582,7 +610,13 @@ learnCond :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWi learnCond opts sc cc cs prepost ss = do let loc = cs ^. MS.csLoc matchPointsTos opts sc cc cs prepost (ss ^. MS.csPointsTos) - traverse_ (learnSetupCondition opts sc cc cs prepost) (ss ^. MS.csConditions) + + asserts <- catMaybes <$> + traverse + (learnSetupCondition opts sc cc cs prepost) + (ss ^. MS.csConditions) + osAsserts %= (asserts ++) + enforceDisjointness loc ss enforceCompleteSubstitution loc ss @@ -816,18 +850,16 @@ assignVar cc loc var val = assignTerm :: SharedContext {- ^ context for constructing SAW terms -} -> LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} -> - W4.ProgramLoc -> PrePost -> VarIndex {- ^ external constant index -} -> Term {- ^ value -} -> - OverrideMatcher (LLVM arch) md () + OverrideMatcher (LLVM arch) md (Maybe (LabeledPred' Sym)) -assignTerm sc cc loc prepost var val = +assignTerm sc cc prepost var val = do mb <- OM (use (termSub . at var)) case mb of - Nothing -> OM (termSub . at var ?= val) - Just old -> - matchTerm sc cc loc prepost val old + Nothing -> OM (termSub . at var ?= val) >> pure Nothing + Just old -> matchTerm sc cc prepost val old -- do t <- liftIO $ scEq sc old val -- p <- liftIO $ resolveSAWPred cc t @@ -836,6 +868,7 @@ assignTerm sc cc loc prepost var val = ------------------------------------------------------------------------ + -- | Match the value of a function argument with a symbolic 'SetupValue'. matchArg :: Options {- ^ saw script print out opts -} -> @@ -848,7 +881,7 @@ matchArg :: {- ^ concrete simulation value -} -> Crucible.MemType {- ^ expected memory type -} -> SetupValue (Crucible.LLVM arch) {- ^ expected specification value -} -> - OverrideMatcher (LLVM arch) md () + OverrideMatcher (LLVM arch) md [LabeledPred' Sym] matchArg opts sc cc cs prepost actual expectedTy expected = case (actual, expectedTy, expected) of @@ -858,11 +891,12 @@ matchArg opts sc cc cs prepost actual expectedTy expected = -> do sym <- Ov.getSymInterface failMsg <- mkStructuralMismatch opts cc sc cs actual expected expectedTy realTerm <- valueToSC sym (cs ^. MS.csLoc) failMsg tval actual - matchTerm sc cc (cs ^. MS.csLoc) prepost realTerm (ttTerm expectedTT) + maybeToList <$> + matchTerm sc cc prepost realTerm (ttTerm expectedTT) -- match the fields of struct point-wise (Crucible.LLVMValStruct xs, Crucible.StructType fields, SetupStruct () _ zs) -> - sequence_ + concat <$> sequence [ matchArg opts sc cc cs prepost x y z | ((_,x),y,z) <- zip3 (V.toList xs) (V.toList (Crucible.fiType <$> Crucible.siFields fields)) @@ -872,25 +906,28 @@ matchArg opts sc cc cs prepost actual expectedTy expected = (_, Crucible.PtrType _, SetupField () _ _) -> resolveAndMatch (_, _, SetupGlobalInitializer () _) -> resolveAndMatch - (Crucible.LLVMValInt blk off, _, _) -> + (Crucible.LLVMValInt blk off, _, _) -> maybeToList <$> + case expected of SetupVar var | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth -> do assignVar cc (cs ^. MS.csLoc) var (Crucible.LLVMPointer blk off) + return Nothing SetupNull () | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth -> do sym <- Ov.getSymInterface - p <- liftIO (Crucible.ptrIsNull sym Crucible.PtrWidth (Crucible.LLVMPointer blk off)) - addAssert p =<< - notEqual prepost opts (cs ^. MS.csLoc) cc sc cs expected actual + lp <- W4.LabeledPred + <$> liftIO (Crucible.ptrIsNull sym Crucible.PtrWidth (Crucible.LLVMPointer blk off)) + <*> notEqual prepost opts cc sc cs expected actual + return (Just lp) SetupGlobal () name | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth -> do let mem = cc^.ccLLVMEmptyMem sym <- Ov.getSymInterface ptr2 <- liftIO $ Crucible.doResolveGlobal sym mem (L.Symbol name) - pred_ <- liftIO $ - Crucible.ptrEq sym Crucible.PtrWidth (Crucible.LLVMPointer blk off) ptr2 - addAssert pred_ =<< - notEqual prepost opts (cs ^. MS.csLoc) cc sc cs expected actual + lp <- W4.LabeledPred + <$> liftIO (Crucible.ptrEq sym Crucible.PtrWidth (Crucible.LLVMPointer blk off) ptr2) + <*> notEqual prepost opts cc sc cs expected actual + return (Just lp) _ -> failure (cs ^. MS.csLoc) =<< mkStructuralMismatch opts cc sc cs actual expected expectedTy @@ -908,9 +945,8 @@ matchArg opts sc cc cs prepost actual expectedTy expected = else liftIO (Crucible.testEqual sym val actual) >>= \case Nothing -> failure (cs ^. MS.csLoc) BadEqualityComparison - Just pred_ -> - addAssert pred_ =<< - notEqual prepost opts (cs ^. MS.csLoc) cc sc cs expected actual + Just pred_ -> (:[]) . W4.LabeledPred pred_ <$> + notEqual prepost opts cc sc cs expected actual ------------------------------------------------------------------------ @@ -1000,24 +1036,23 @@ typeToSC sc t = matchTerm :: SharedContext {- ^ context for constructing SAW terms -} -> LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} -> - W4.ProgramLoc -> PrePost -> Term {- ^ exported concrete term -} -> Term {- ^ expected specification term -} -> - OverrideMatcher (LLVM arch) md () + OverrideMatcher (LLVM arch) md (Maybe (LabeledPred' Sym)) -matchTerm _ _ _ _ real expect | real == expect = return () -matchTerm sc cc loc prepost real expect = +matchTerm _ _ _ real expect | real == expect = return Nothing +matchTerm sc cc prepost real expect = do free <- OM (use osFree) case unwrapTermF expect of FTermF (ExtCns ec) | Set.member (ecVarIndex ec) free -> - do assignTerm sc cc loc prepost (ecVarIndex ec) real + do assignTerm sc cc prepost (ecVarIndex ec) real _ -> do t <- liftIO $ scEq sc real expect p <- liftIO $ resolveSAWPred cc t - addAssert p $ Crucible.SimError loc $ Crucible.AssertFailureSimError $ unlines $ + return $ Just $ W4.LabeledPred p $ PP.vcat $ map PP.text [ "Literal equality " ++ stateCond prepost , "Expected term: " ++ prettyTerm expect , "Actual term: " ++ prettyTerm real @@ -1039,9 +1074,9 @@ learnSetupCondition :: MS.CrucibleMethodSpecIR (LLVM arch) -> PrePost -> MS.SetupCondition (LLVM arch) -> - OverrideMatcher (LLVM arch) md () -learnSetupCondition opts sc cc spec prepost (MS.SetupCond_Equal loc val1 val2) = learnEqual opts sc cc spec loc prepost val1 val2 -learnSetupCondition _opts sc cc _ prepost (MS.SetupCond_Pred loc tm) = learnPred sc cc loc prepost (ttTerm tm) + OverrideMatcher (LLVM arch) md (Maybe (LabeledPred Sym)) +learnSetupCondition opts sc cc spec prepost (MS.SetupCond_Equal loc val1 val2) = Just <$> learnEqual opts sc cc spec loc prepost val1 val2 +learnSetupCondition _opts sc cc _ prepost (MS.SetupCond_Pred loc tm) = Just <$> learnPred sc cc loc prepost (ttTerm tm) learnSetupCondition _opts sc cc _ prepost (MS.SetupCond_Ghost () loc var val) = learnGhost sc cc loc prepost var val @@ -1055,10 +1090,11 @@ learnGhost :: PrePost -> MS.GhostGlobal -> TypedTerm -> - OverrideMatcher (LLVM arch) md () + OverrideMatcher (LLVM arch) md (Maybe (LabeledPred Sym)) learnGhost sc cc loc prepost var expected = do actual <- readGlobal var - matchTerm sc cc loc prepost (ttTerm actual) (ttTerm expected) + maybeAssert <- matchTerm sc cc prepost (ttTerm actual) (ttTerm expected) + pure $ fmap (labelWithSimError loc show) maybeAssert ------------------------------------------------------------------------ @@ -1155,13 +1191,14 @@ learnEqual :: PrePost -> SetupValue (Crucible.LLVM arch) {- ^ first value to compare -} -> SetupValue (Crucible.LLVM arch) {- ^ second value to compare -} -> - OverrideMatcher (LLVM arch) md () + OverrideMatcher (LLVM arch) md (LabeledPred Sym) learnEqual opts sc cc spec loc prepost v1 v2 = do (_, val1) <- resolveSetupValueLLVM opts cc sc spec v1 (_, val2) <- resolveSetupValueLLVM opts cc sc spec v2 p <- liftIO (equalValsPred cc val1 val2) let name = "equality " ++ stateCond prepost - addAssert p (Crucible.SimError loc (Crucible.AssertFailureSimError name)) + return $ + W4.LabeledPred p (Crucible.SimError loc (Crucible.AssertFailureSimError name)) -- | Process a "crucible_precond" statement from the precondition -- section of the CrucibleSetup block. @@ -1171,12 +1208,13 @@ learnPred :: W4.ProgramLoc -> PrePost -> Term {- ^ the precondition to learn -} -> - OverrideMatcher (LLVM arch) md () + OverrideMatcher (LLVM arch) md (LabeledPred Sym) learnPred sc cc loc prepost t = do s <- OM (use termSub) u <- liftIO $ scInstantiateExt sc s t p <- liftIO $ resolveSAWPred cc u - addAssert p (Crucible.SimError loc (Crucible.AssertFailureSimError (stateCond prepost))) + return $ + W4.LabeledPred p (Crucible.SimError loc (Crucible.AssertFailureSimError (stateCond prepost))) ------------------------------------------------------------------------