From 4fecf3d2d3f00a053f1c72907cba41cb5d3990aa Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 19 Apr 2019 10:30:08 -0700 Subject: [PATCH 01/14] [WIP] use labeled predicates --- src/SAWScript/CrucibleOverride.hs | 67 +++++++++++++++++++++++++++---- 1 file changed, 59 insertions(+), 8 deletions(-) diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index 68a6e39f01..4e299245ce 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -47,6 +47,7 @@ import Data.List (tails) import Data.IORef (readIORef) import Data.Map (Map) import qualified Data.Map as Map +import Data.Maybe (catMaybes) import Data.Proxy import Data.Set (Set) import qualified Data.Set as Set @@ -74,11 +75,12 @@ import qualified Lang.Crucible.Simulator.SimError as Crucible --import qualified Lang.Crucible.Types as Crucible import qualified What4.BaseTypes as W4 -import qualified What4.Interface as W4 import qualified What4.Expr.Builder as W4 -import qualified What4.Symbol as W4 +import qualified What4.Interface as W4 +import qualified What4.LabeledPred as W4 import qualified What4.Partial as W4 import qualified What4.ProgramLoc as W4 +import qualified What4.Symbol as W4 import qualified SAWScript.CrucibleLLVM as Crucible @@ -113,6 +115,19 @@ deriving instance MonadError (OverrideFailure arch) (OverrideMatcher arch mode) type AllocMap arch = Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) +-- | A labeled assertion is a predicate together with: +-- 1. A reason that it needs to be true +-- 2. Its constant value, if any (computed via 'asConstantPred') +-- +-- TODO: Consider merging with Crucible's @LabledPred@ type. +data LabeledAssertion sym = + LabeledAssertion + { _labeledPred :: W4.Pred sym + , _labeledLabel :: Crucible.SimError + , _labeledConstValue :: Maybe Bool + } + deriving (Generic) + data OverrideState arch = OverrideState { -- | Substitution for memory allocations _setupValueSub :: AllocMap arch @@ -124,7 +139,7 @@ data OverrideState arch = OverrideState , _osFree :: Set VarIndex -- | Accumulated assertions - , _osAsserts :: [(W4.Pred Sym, Crucible.SimError)] + , _osAsserts :: [LabeledAssertion Sym] -- | Accumulated assumptions , _osAssumes :: [W4.Pred Sym] @@ -275,7 +290,8 @@ addAssert :: W4.Pred Sym {- ^ property -} -> Crucible.SimError {- ^ reason -} -> OverrideMatcher arch md () -addAssert p r = OM (osAsserts %= cons (p,r)) +addAssert p r = + OM (osAsserts %= cons (LabeledAssertion p r (W4.asConstantPred p))) addAssume :: W4.Pred Sym {- ^ property -} -> @@ -312,6 +328,30 @@ failure loc e = OM (lift (throwE (OF loc e))) ------------------------------------------------------------------------ +data OverrideWithPreconditions arch sym = + OverrideWithPreconditions + { _owpPreconditions :: [LabeledAssertion sym] -- ^ c.f. '_osAsserts' + , _owpMethodSpec :: CrucibleMethodSpecIR + , _owpState :: OverrideState arch + } + deriving (Generic) + +-- | Are any of the preconditions concretely false? +concretePreconditionFailure :: + OverrideWithPreconditions arch sym -> + Bool +concretePreconditionFailure = + or . catMaybes . map (fmap not . _labeledConstValue) . _owpPreconditions + +-- | Partition the preconditions of this override into three sets: +-- Concretely true, concretely false, and unknown/symbolic. +-- +-- This might be useful to generalize to an operation on @Pred@? +partitionPreconditions :: + OverrideWithPreconditions arch sym -> + ([LabeledAssertion sym], [LabeledAssertion sym], [LabeledAssertion sym]) +partitionPreconditions = _ + -- | This function is responsible for implementing the \"override\" behavior -- of method specifications. The main work done in this function to manage -- the process of selecting between several possible different override @@ -389,8 +429,19 @@ methodSpecHandler opts sc cc top_loc css retTy = do PP.text (show (retTy)) (_, ss) -> liftIO $ forM ss $ \(cs,st) -> - do precond <- W4.andAllOf sym (folded._1) (st^.osAsserts) - return ( precond, cs, st ) + return (OverrideWithPreconditions (st^.osAsserts) 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. + -- If so, there's no use in branching on them with @symbolicBranches@. + let branches' :: [OverrideWithPreconditions arch Sym] + branches' = filter (not . concretePreconditionFailure) branches + + -- Collapse the preconditions to a single predicate + branches'' <- liftIO $ forM branches $ + \(OverrideWithPreconditions preconds cs st) -> + W4.andAllOf sym (folded._1) (map _labeledPred preconds) <&> + \precond -> (precond, cs, st) -- Now use crucible's symbolic branching machinery to select between the branches. -- Essentially, we are doing an n-way if statement on the precondition predicates @@ -430,11 +481,11 @@ methodSpecHandler opts sc cc top_loc css retTy = do Crucible.overrideReturn' (Crucible.RegEntry retTy ret) , Just (W4.plSourceLoc (cs^.csLoc)) ) - | (precond, cs, st) <- branches + | (precond, cs, st) <- branches'' ] ++ [ - let fnName = case branches of + let fnName = case branches'' of (_, cs, _) : _ -> cs^.csName _ -> "unknown function" in From cb3cf321f0b14c6b4e3923e4c978e37cc08f7390 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Mon, 22 Apr 2019 10:12:41 -0700 Subject: [PATCH 02/14] Print concretely failing override preconditions --- src/SAWScript/CrucibleOverride.hs | 120 ++++++++++++++++++------------ 1 file changed, 71 insertions(+), 49 deletions(-) diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index 4e299245ce..da9e09f098 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -47,7 +47,6 @@ import Data.List (tails) import Data.IORef (readIORef) import Data.Map (Map) import qualified Data.Map as Map -import Data.Maybe (catMaybes) import Data.Proxy import Data.Set (Set) import qualified Data.Set as Set @@ -114,19 +113,7 @@ deriving instance MonadState (OverrideState arch) (OverrideMatcher arch mode) deriving instance MonadError (OverrideFailure arch) (OverrideMatcher arch mode) type AllocMap arch = Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) - --- | A labeled assertion is a predicate together with: --- 1. A reason that it needs to be true --- 2. Its constant value, if any (computed via 'asConstantPred') --- --- TODO: Consider merging with Crucible's @LabledPred@ type. -data LabeledAssertion sym = - LabeledAssertion - { _labeledPred :: W4.Pred sym - , _labeledLabel :: Crucible.SimError - , _labeledConstValue :: Maybe Bool - } - deriving (Generic) +type LabeledPred sym = W4.LabeledPred (W4.Pred sym) Crucible.SimError data OverrideState arch = OverrideState { -- | Substitution for memory allocations @@ -139,7 +126,7 @@ data OverrideState arch = OverrideState , _osFree :: Set VarIndex -- | Accumulated assertions - , _osAsserts :: [LabeledAssertion Sym] + , _osAsserts :: [LabeledPred Sym] -- | Accumulated assumptions , _osAssumes :: [W4.Pred Sym] @@ -291,7 +278,7 @@ addAssert :: Crucible.SimError {- ^ reason -} -> OverrideMatcher arch md () addAssert p r = - OM (osAsserts %= cons (LabeledAssertion p r (W4.asConstantPred p))) + OM (osAsserts %= cons (W4.LabeledPred p r)) addAssume :: W4.Pred Sym {- ^ property -} -> @@ -330,27 +317,52 @@ failure loc e = OM (lift (throwE (OF loc e))) data OverrideWithPreconditions arch sym = OverrideWithPreconditions - { _owpPreconditions :: [LabeledAssertion sym] -- ^ c.f. '_osAsserts' + { _owpPreconditions :: [LabeledPred sym] -- ^ c.f. '_osAsserts' , _owpMethodSpec :: CrucibleMethodSpecIR - , _owpState :: OverrideState arch + , owpState :: OverrideState arch } deriving (Generic) --- | Are any of the preconditions concretely false? -concretePreconditionFailure :: - OverrideWithPreconditions arch sym -> - Bool -concretePreconditionFailure = - or . catMaybes . map (fmap not . _labeledConstValue) . _owpPreconditions - --- | Partition the preconditions of this override into three sets: --- Concretely true, concretely false, and unknown/symbolic. +makeLenses ''OverrideWithPreconditions + +-- | Partition into three groups: +-- * Preconditions concretely succeed +-- * Preconditions concretely fail +-- * Preconditions are symbolic +partitionOWPs :: forall arch sym. + W4.IsExprBuilder sym => + sym -> + [OverrideWithPreconditions arch sym] -> + IO ([OverrideWithPreconditions arch sym], [OverrideWithPreconditions arch sym], [OverrideWithPreconditions arch sym]) +partitionOWPs sym = + let t :: Traversal' (OverrideWithPreconditions arch sym) (W4.Pred sym) + t = owpPreconditions . each . W4.labeledPred + in W4.partitionByPredsM (Just sym) $ + foldlMOf t (W4.andPred sym) (W4.truePred sym) + +-- | Print a message about concrete failure of an override's preconditions -- --- This might be useful to generalize to an operation on @Pred@? -partitionPreconditions :: +-- Assumes that the override it's being passed does have concretely failing +-- preconditions. Otherwise, the error won't make much sense. +ppConcreteFailure :: forall arch sym. + W4.IsExprBuilder sym => OverrideWithPreconditions arch sym -> - ([LabeledAssertion sym], [LabeledAssertion sym], [LabeledAssertion sym]) -partitionPreconditions = _ + PP.Doc +ppConcreteFailure owp = + let (_, false, _) = + W4.partitionLabeledPreds (Proxy :: Proxy sym) (owp ^. owpPreconditions) + in + PP.text "-" PP.<+> + PP.indent 2 + (PP.vcat [ PP.text $ "Failed preconditions for override " + , PP.text $ "Name: " <> (owp ^. owpMethodSpec . csName) + , "Location: " <> + PP.pretty + (W4.plSourceLoc (owp ^. owpMethodSpec . csLoc)) + ]) + PP.<$$> + PP.vcat (map ((PP.text "*" PP.<+>) . Crucible.ppSimError) + (false ^.. traverse . W4.labeledPredMsg)) -- | This function is responsible for implementing the \"override\" behavior -- of method specifications. The main work done in this function to manage @@ -434,13 +446,12 @@ methodSpecHandler opts sc cc top_loc css retTy = do -- 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. -- If so, there's no use in branching on them with @symbolicBranches@. - let branches' :: [OverrideWithPreconditions arch Sym] - branches' = filter (not . concretePreconditionFailure) branches + (true, false, unknown) <- liftIO $ partitionOWPs sym branches -- Collapse the preconditions to a single predicate - branches'' <- liftIO $ forM branches $ - \(OverrideWithPreconditions preconds cs st) -> - W4.andAllOf sym (folded._1) (map _labeledPred preconds) <&> + branches' <- liftIO $ forM (true ++ unknown) $ + \(OverrideWithPreconditions preconds cs st) -> + W4.andAllOf sym (folded . W4.labeledPred) preconds <&> \precond -> (precond, cs, st) -- Now use crucible's symbolic branching machinery to select between the branches. @@ -481,20 +492,31 @@ methodSpecHandler opts sc cc top_loc css retTy = do Crucible.overrideReturn' (Crucible.RegEntry retTy ret) , Just (W4.plSourceLoc (cs^.csLoc)) ) - | (precond, cs, st) <- branches'' + | (precond, cs, st) <- branches' ] ++ - [ - - let fnName = case branches'' of - (_, cs, _) : _ -> cs^.csName - _ -> "unknown function" - in - ( W4.truePred sym - , liftIO $ Crucible.addFailedAssertion sym (Crucible.GenericSimError $ "no override specification applies for " ++ fnName) - , Just (W4.plSourceLoc top_loc) - ) - ] - )) + [ let fnName = case branches' of + (_, cs, _) : _ -> cs^.csName + _ -> "" + + e = show $ + (PP.hcat $ map PP.text + [ "No override specification applies for ", fnName, "." + , if not (null false) + then unwords $ + [ "The following overrides had some preconditions " + , "that failed concretely:" + ] + else "" + ]) + PP.<$$> PP.vcat (map ppConcreteFailure false) + + + in + ( W4.truePred sym + , liftIO $ Crucible.addFailedAssertion sym (Crucible.GenericSimError e) + , Just (W4.plSourceLoc top_loc) + ) + ])) (Crucible.RegMap args) ------------------------------------------------------------------------ From dec81cdb833dd2feab0c563e276bc290aa14cda9 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Mon, 22 Apr 2019 10:32:54 -0700 Subject: [PATCH 03/14] Prettier printing of override matching failure --- src/SAWScript/CrucibleBuiltins.hs | 3 ++- src/SAWScript/CrucibleMethodSpecIR.hs | 35 ++++++++++++++++-------- src/SAWScript/CrucibleOverride.hs | 38 +++++++++------------------ 3 files changed, 38 insertions(+), 38 deletions(-) diff --git a/src/SAWScript/CrucibleBuiltins.hs b/src/SAWScript/CrucibleBuiltins.hs index 2eb6656d89..d8dcb77bf3 100644 --- a/src/SAWScript/CrucibleBuiltins.hs +++ b/src/SAWScript/CrucibleBuiltins.hs @@ -91,6 +91,7 @@ import Data.Parameterized.Some 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 @@ -654,7 +655,7 @@ verifyPoststate opts sc cc mspec env0 globals ret = st <- case matchPost of Left err -> fail (show err) Right (_, st) -> return st - io $ for_ (view osAsserts st) $ \(p, r) -> + io $ for_ (view osAsserts st) $ \(W4.LabeledPred p r) -> Crucible.addAssertion sym (Crucible.LabeledPred p r) obligations <- io $ Crucible.getProofObligations sym diff --git a/src/SAWScript/CrucibleMethodSpecIR.hs b/src/SAWScript/CrucibleMethodSpecIR.hs index 460bee143d..0ff3487870 100644 --- a/src/SAWScript/CrucibleMethodSpecIR.hs +++ b/src/SAWScript/CrucibleMethodSpecIR.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DeriveFunctor #-} {- | Module : SAWScript.CrucibleMethodSpecIR Description : Provides type-checked representation for Crucible/LLVM function @@ -31,17 +32,17 @@ import qualified Data.Map as Map import Control.Monad.Trans.Maybe import Control.Monad.Trans (lift) import Control.Lens -import Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>), (<>)) +import Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>), (<>)) -import qualified Text.LLVM.AST as L -import qualified Text.LLVM.PP as L import Data.IORef import Data.Monoid ((<>)) +import qualified Text.LLVM.AST as L +import qualified Text.LLVM.PP as L import qualified Data.Parameterized.Map as MapF import qualified Data.Parameterized.Nonce as Crucible -import SAWScript.Prover.SolverStats +import SAWScript.Prover.SolverStats import qualified What4.Expr.Builder as B import What4.ProgramLoc (ProgramLoc) @@ -58,12 +59,13 @@ import qualified Lang.Crucible.Simulator.GlobalState as Crucible (SymGlobalState --import qualified Lang.Crucible.LLVM.Translation as CL import qualified Lang.Crucible.Simulator.Intrinsics as Crucible (IntrinsicClass(Intrinsic, muxIntrinsic), IntrinsicMuxFn(IntrinsicMuxFn)) +import qualified What4.ProgramLoc as W4 (plSourceLoc) import qualified SAWScript.CrucibleLLVM as CL -import Verifier.SAW.SharedTerm -import Verifier.SAW.TypedTerm -import SAWScript.Options +import Verifier.SAW.SharedTerm +import Verifier.SAW.TypedTerm +import SAWScript.Options newtype AllocIndex = AllocIndex Int deriving (Eq, Ord, Show) @@ -180,14 +182,26 @@ data CrucibleMethodSpecIR' t = , _csSolverStats :: SolverStats -- ^ statistics about the proof that produced this , _csLoc :: ProgramLoc } - deriving (Show) - -type CrucibleMethodSpecIR = CrucibleMethodSpecIR' CL.MemType + deriving (Functor, Show) type GhostValue = "GhostValue" type GhostType = Crucible.IntrinsicType GhostValue Crucible.EmptyCtx type GhostGlobal = Crucible.GlobalVar GhostType +makeLenses ''CrucibleMethodSpecIR' + +type CrucibleMethodSpecIR = CrucibleMethodSpecIR' CL.MemType + +ppMethodSpec :: CrucibleMethodSpecIR -> PP.Doc +ppMethodSpec methodSpec = + PP.text "Name: " <> PP.text (methodSpec ^. csName) + PP.<$$> PP.text "Location: " <> PP.pretty (W4.plSourceLoc (methodSpec ^. csLoc)) + PP.<$$> PP.text "Argument types: " + PP.<$$> PP.indent 2 (PP.vcat (map (PP.text . show) (methodSpec ^. csArgs))) + PP.<$$> PP.text "Return type: " <> case methodSpec ^. csRet of + Nothing -> PP.text "" + Just ret -> PP.text (show ret) + instance Crucible.IntrinsicClass (Crucible.SAWCoreBackend n solver (B.Flags B.FloatReal)) GhostValue where type Intrinsic (Crucible.SAWCoreBackend n solver (B.Flags B.FloatReal)) GhostValue ctx = TypedTerm muxIntrinsic sym _ _namerep _ctx prd thn els = @@ -198,7 +212,6 @@ instance Crucible.IntrinsicClass (Crucible.SAWCoreBackend n solver (B.Flags B.Fl res <- scIte sc typ prd' (ttTerm thn) (ttTerm els) return thn { ttTerm = res } -makeLenses ''CrucibleMethodSpecIR' makeLenses ''StateSpec' csAllocations :: CrucibleMethodSpecIR -> Map AllocIndex (ProgramLoc, CL.MemType) diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index da9e09f098..5240d43823 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -340,6 +340,9 @@ partitionOWPs sym = in W4.partitionByPredsM (Just sym) $ foldlMOf t (W4.andPred sym) (W4.truePred sym) +bullets :: Char -> [PP.Doc] -> PP.Doc +bullets c = PP.vcat . map (PP.hang 2 . (PP.text [c] PP.<+>)) + -- | Print a message about concrete failure of an override's preconditions -- -- Assumes that the override it's being passed does have concretely failing @@ -351,18 +354,9 @@ ppConcreteFailure :: forall arch sym. ppConcreteFailure owp = let (_, false, _) = W4.partitionLabeledPreds (Proxy :: Proxy sym) (owp ^. owpPreconditions) - in - PP.text "-" PP.<+> - PP.indent 2 - (PP.vcat [ PP.text $ "Failed preconditions for override " - , PP.text $ "Name: " <> (owp ^. owpMethodSpec . csName) - , "Location: " <> - PP.pretty - (W4.plSourceLoc (owp ^. owpMethodSpec . csLoc)) - ]) - PP.<$$> - PP.vcat (map ((PP.text "*" PP.<+>) . Crucible.ppSimError) - (false ^.. traverse . W4.labeledPredMsg)) + in ppMethodSpec (owp ^. owpMethodSpec) + PP.<$$> bullets '*' (map Crucible.ppSimError + (false ^.. traverse . W4.labeledPredMsg)) -- | This function is responsible for implementing the \"override\" behavior -- of method specifications. The main work done in this function to manage @@ -418,15 +412,7 @@ methodSpecHandler opts sc cc top_loc css retTy = do -- various overrides. branches <- let prettyError methodSpec failureReason = - PP.text "Name: " - PP.<> PP.text (methodSpec ^. csName) - PP.<$$> PP.text "Argument types: " - PP.<$$> PP.indent 2 (PP.vcat (map (PP.text . show) (methodSpec ^. csArgs))) - PP.<$$> PP.text "Return type: " - PP.<> case methodSpec ^. csRet of - Nothing -> PP.text "" - Just ret -> PP.text (show ret) - PP.<$$> ppOverrideFailure failureReason + ppMethodSpec methodSpec PP.<$$> ppOverrideFailure failureReason in case partitionEithers prestates of (errs, []) -> @@ -494,12 +480,12 @@ methodSpecHandler opts sc cc top_loc css retTy = do ) | (precond, cs, st) <- branches' ] ++ - [ let fnName = case branches' of - (_, cs, _) : _ -> cs^.csName - _ -> "" + [ let fnName = case branches of + owp : _ -> owp ^. owpMethodSpec . csName + _ -> "" e = show $ - (PP.hcat $ map PP.text + (PP.text $ unlines $ [ "No override specification applies for ", fnName, "." , if not (null false) then unwords $ @@ -508,7 +494,7 @@ methodSpecHandler opts sc cc top_loc css retTy = do ] else "" ]) - PP.<$$> PP.vcat (map ppConcreteFailure false) + PP.<$$> bullets '-' (map ppConcreteFailure false) in From 66af2c202dee795ae647122a2696f45eaf4056e9 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Mon, 22 Apr 2019 10:40:08 -0700 Subject: [PATCH 04/14] More specific error messages for preconditions involving globals --- src/SAWScript/CrucibleOverride.hs | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index 5240d43823..799d772e90 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -486,7 +486,7 @@ methodSpecHandler opts sc cc top_loc css retTy = do e = show $ (PP.text $ unlines $ - [ "No override specification applies for ", fnName, "." + [ "No override specification applies for " ++ fnName ++ "." , if not (null false) then unwords $ [ "The following overrides had some preconditions " @@ -879,7 +879,12 @@ matchArg opts sc cc cs prepost actual expectedTy g@(SetupGlobalInitializer n) = Nothing -> failure (cs ^. csLoc) (BadEqualityComparison n) Just pred_ -> let err = Crucible.SimError (cs ^. csLoc) . Crucible.AssertFailureSimError - in addAssert pred_ $ err ("global initializer equality " ++ stateCond prepost) + in addAssert pred_ $ err $ unwords $ + [ "global initializer equality" + , stateCond prepost -- either 'precondition' or 'postcondition' + , "for global" + , n + ] matchArg _opts _sc cc cs prepost actual@(Crucible.LLVMValInt blk off) expectedTy setupval = case setupval of @@ -889,7 +894,8 @@ matchArg _opts _sc cc cs prepost actual@(Crucible.LLVMValInt blk off) expectedTy SetupNull | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth -> do sym <- getSymInterface p <- liftIO (Crucible.ptrIsNull sym Crucible.PtrWidth (Crucible.LLVMPointer blk off)) - addAssert p (Crucible.SimError (cs ^. csLoc) (Crucible.AssertFailureSimError ("null-equality " ++ stateCond prepost))) + let err = Crucible.SimError (cs ^. csLoc) . Crucible.AssertFailureSimError + addAssert p $ err $ ("null-equality " ++ stateCond prepost) SetupGlobal name | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth -> do let mem = cc^.ccLLVMEmptyMem @@ -897,7 +903,13 @@ matchArg _opts _sc cc cs prepost actual@(Crucible.LLVMValInt blk off) expectedTy ptr2 <- liftIO $ Crucible.doResolveGlobal sym mem (L.Symbol name) pred_ <- liftIO $ Crucible.ptrEq sym Crucible.PtrWidth (Crucible.LLVMPointer blk off) ptr2 - addAssert pred_ (Crucible.SimError (cs ^. csLoc) (Crucible.AssertFailureSimError ("global-equality " ++ stateCond prepost))) + let err = Crucible.SimError (cs ^. csLoc) . Crucible.AssertFailureSimError + addAssert pred_ $ err $ unwords + [ "global variable equality" + , stateCond prepost -- either 'precondition' or 'postcondition' + , "for global" + , name + ] _ -> failure (cs ^. csLoc) (StructuralMismatch actual setupval expectedTy) From f123d08f574c24ec2903bc2f66b5f75313b0049a Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Mon, 22 Apr 2019 10:52:27 -0700 Subject: [PATCH 05/14] Update Crucible submodule (for What4.LabeledPred) --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index 703b4bf80f..581d44f06a 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 703b4bf80ff0472b00af2a666b18ee6c78b15c3e +Subproject commit 581d44f06a15cda2e614cb6ab48ede6c3e07a4d1 From 4395c171fede3b1afe326199ac2fc27babc0497d Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Mon, 22 Apr 2019 13:56:32 -0700 Subject: [PATCH 06/14] Update Crucible submodule: Pretty instance for LLVMVal --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index 581d44f06a..4da68a1c71 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 581d44f06a15cda2e614cb6ab48ede6c3e07a4d1 +Subproject commit 4da68a1c71c95e715deeeba9b40526fa43054b9c From ec8220c3f7e2f55d08be9aa26f7b101c6a08349a Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Mon, 22 Apr 2019 14:11:38 -0700 Subject: [PATCH 07/14] Show both expected and actual values on equality preconditions --- src/SAWScript/CrucibleOverride.hs | 35 ++++++++++++++++--------------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index 799d772e90..457d3b52d9 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -839,6 +839,21 @@ assignTerm sc cc loc prepost var val = ------------------------------------------------------------------------ +-- | Create an error stating that the 'LLVMVal' was not equal to the 'SetupValue' +notEqual :: + W4.IsExpr (W4.SymExpr sym) => + PrePost -> + W4.ProgramLoc {- ^ where is the assertion from? -} -> + SetupValue {- ^ expected value -} -> + Crucible.LLVMVal sym {- ^ value from Crucible -} -> + Crucible.SimError +notEqual cond loc expected actual = + Crucible.SimError loc $ Crucible.AssertFailureSimError $ unlines $ + [ "Equality " ++ stateCond cond + , "Expected value: " ++ show (ppSetupValue expected) + , "Actual value: " ++ show (PP.pretty actual) + ] + -- | Match the value of a function argument with a symbolic 'SetupValue'. matchArg :: Options {- ^ saw script print out opts -} -> @@ -877,14 +892,7 @@ matchArg opts sc cc cs prepost actual expectedTy g@(SetupGlobalInitializer n) = else liftIO (Crucible.testEqual sym globInitVal actual) >>= \case Nothing -> failure (cs ^. csLoc) (BadEqualityComparison n) - Just pred_ -> - let err = Crucible.SimError (cs ^. csLoc) . Crucible.AssertFailureSimError - in addAssert pred_ $ err $ unwords $ - [ "global initializer equality" - , stateCond prepost -- either 'precondition' or 'postcondition' - , "for global" - , n - ] + Just pred_ -> addAssert pred_ $ notEqual prepost (cs ^. csLoc) g actual matchArg _opts _sc cc cs prepost actual@(Crucible.LLVMValInt blk off) expectedTy setupval = case setupval of @@ -894,8 +902,7 @@ matchArg _opts _sc cc cs prepost actual@(Crucible.LLVMValInt blk off) expectedTy SetupNull | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth -> do sym <- getSymInterface p <- liftIO (Crucible.ptrIsNull sym Crucible.PtrWidth (Crucible.LLVMPointer blk off)) - let err = Crucible.SimError (cs ^. csLoc) . Crucible.AssertFailureSimError - addAssert p $ err $ ("null-equality " ++ stateCond prepost) + addAssert p $ notEqual prepost (cs ^. csLoc) setupval actual SetupGlobal name | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth -> do let mem = cc^.ccLLVMEmptyMem @@ -903,13 +910,7 @@ matchArg _opts _sc cc cs prepost actual@(Crucible.LLVMValInt blk off) expectedTy ptr2 <- liftIO $ Crucible.doResolveGlobal sym mem (L.Symbol name) pred_ <- liftIO $ Crucible.ptrEq sym Crucible.PtrWidth (Crucible.LLVMPointer blk off) ptr2 - let err = Crucible.SimError (cs ^. csLoc) . Crucible.AssertFailureSimError - addAssert pred_ $ err $ unwords - [ "global variable equality" - , stateCond prepost -- either 'precondition' or 'postcondition' - , "for global" - , name - ] + addAssert pred_ $ notEqual prepost (cs ^. csLoc) setupval actual _ -> failure (cs ^. csLoc) (StructuralMismatch actual setupval expectedTy) From 12a1190548a7ffd8b17dba9c9b9e4e57c197c43e Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Mon, 22 Apr 2019 14:26:19 -0700 Subject: [PATCH 08/14] Add some newlines (the actual value may be a large, complex struct) --- src/SAWScript/CrucibleOverride.hs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index 457d3b52d9..7916f2e819 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -850,8 +850,10 @@ notEqual :: notEqual cond loc expected actual = Crucible.SimError loc $ Crucible.AssertFailureSimError $ unlines $ [ "Equality " ++ stateCond cond - , "Expected value: " ++ show (ppSetupValue expected) - , "Actual value: " ++ show (PP.pretty actual) + , "Expected value: " + , show (ppSetupValue expected) + , "Actual value: " + , show (PP.pretty actual) ] -- | Match the value of a function argument with a symbolic 'SetupValue'. From 66c9fbccedc529a38aae8612eaac06a628cd67d8 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Mon, 22 Apr 2019 16:34:51 -0700 Subject: [PATCH 09/14] Show symbolically failing override preconditions when possible This should be redone with unsat cores, but that will be a bit more complicated. For now, fixes #414. --- src/SAWScript/CrucibleOverride.hs | 126 +++++++++++++++++++++--------- 1 file changed, 89 insertions(+), 37 deletions(-) diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index 7916f2e819..ed23a8e929 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -47,6 +47,7 @@ import Data.List (tails) import Data.IORef (readIORef) import Data.Map (Map) import qualified Data.Map as Map +import Data.Maybe (fromMaybe, catMaybes) import Data.Proxy import Data.Set (Set) import qualified Data.Set as Set @@ -63,6 +64,8 @@ import qualified Cryptol.Utils.PP as Cryptol import qualified Lang.Crucible.Backend as Crucible import qualified Lang.Crucible.Backend.SAWCore as Crucible +import qualified Lang.Crucible.Backend.SAWCore as CrucibleSAW +import qualified Lang.Crucible.Backend.Online as Crucible import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr(UnitRepr), GlobalVar) import qualified Lang.Crucible.CFG.Extension.Safety as Crucible @@ -87,8 +90,8 @@ import Data.Parameterized.Classes ((:~:)(..), testEquality) import qualified Data.Parameterized.TraversableFC as Ctx import qualified Data.Parameterized.Context as Ctx -import Verifier.SAW.SharedTerm import Verifier.SAW.Prelude (scEq) +import Verifier.SAW.SharedTerm import Verifier.SAW.TypedAST --import Verifier.SAW.Term.Pretty import Verifier.SAW.Recognizer @@ -315,9 +318,12 @@ failure loc e = OM (lift (throwE (OF loc e))) ------------------------------------------------------------------------ -data OverrideWithPreconditions arch sym = +bullets :: Char -> [PP.Doc] -> PP.Doc +bullets c = PP.vcat . map (PP.hang 2 . (PP.text [c] PP.<+>)) + +data OverrideWithPreconditions arch = OverrideWithPreconditions - { _owpPreconditions :: [LabeledPred sym] -- ^ c.f. '_osAsserts' + { _owpPreconditions :: [LabeledPred Sym] -- ^ c.f. '_osAsserts' , _owpMethodSpec :: CrucibleMethodSpecIR , owpState :: OverrideState arch } @@ -329,34 +335,65 @@ makeLenses ''OverrideWithPreconditions -- * Preconditions concretely succeed -- * Preconditions concretely fail -- * Preconditions are symbolic -partitionOWPs :: forall arch sym. - W4.IsExprBuilder sym => - sym -> - [OverrideWithPreconditions arch sym] -> - IO ([OverrideWithPreconditions arch sym], [OverrideWithPreconditions arch sym], [OverrideWithPreconditions arch sym]) -partitionOWPs sym = - let t :: Traversal' (OverrideWithPreconditions arch sym) (W4.Pred sym) - t = owpPreconditions . each . W4.labeledPred +partitionOWPsConcrete :: forall arch. + Sym -> + [OverrideWithPreconditions arch] -> + IO ([OverrideWithPreconditions arch], [OverrideWithPreconditions arch], [OverrideWithPreconditions arch]) +partitionOWPsConcrete sym = + let traversal = owpPreconditions . each . W4.labeledPred in W4.partitionByPredsM (Just sym) $ - foldlMOf t (W4.andPred sym) (W4.truePred sym) - -bullets :: Char -> [PP.Doc] -> PP.Doc -bullets c = PP.vcat . map (PP.hang 2 . (PP.text [c] PP.<+>)) + foldlMOf traversal (W4.andPred sym) (W4.truePred sym) + +-- | Like 'W4.partitionByPreds', but partitions on solver responses, not just +-- concretized values. +partitionBySymbolicPreds :: + (Foldable t) => + Sym {- ^ solver connection -} -> + (a -> W4.Pred Sym) {- ^ how to extract predicates -} -> + t a -> + IO (Map Crucible.BranchResult [a]) +partitionBySymbolicPreds sym getPred = + let step mp a = + CrucibleSAW.considerSatisfiability sym Nothing (getPred a) <&> \k -> + Map.insertWith (++) k [a] mp + in foldM step Map.empty + +-- | Find individual preconditions that are symbolically false +-- +-- We should probably be using unsat cores for this. +findFalsePreconditions :: + Sym -> + OverrideWithPreconditions arch -> + IO [LabeledPred Sym] +findFalsePreconditions sym owp = + fromMaybe [] . Map.lookup (Crucible.NoBranch False) <$> + partitionBySymbolicPreds sym (view W4.labeledPred) (owp ^. owpPreconditions) + +-- | Print a message about failure of an override's preconditions +ppFailure :: + OverrideWithPreconditions arch -> + [LabeledPred Sym] -> + PP.Doc +ppFailure owp false = + ppMethodSpec (owp ^. owpMethodSpec) + PP.<$$> bullets '*' (map Crucible.ppSimError + (false ^.. traverse . W4.labeledPredMsg)) -- | Print a message about concrete failure of an override's preconditions -- -- Assumes that the override it's being passed does have concretely failing -- preconditions. Otherwise, the error won't make much sense. -ppConcreteFailure :: forall arch sym. - W4.IsExprBuilder sym => - OverrideWithPreconditions arch sym -> - PP.Doc +ppConcreteFailure :: OverrideWithPreconditions arch -> PP.Doc ppConcreteFailure owp = let (_, false, _) = - W4.partitionLabeledPreds (Proxy :: Proxy sym) (owp ^. owpPreconditions) - in ppMethodSpec (owp ^. owpMethodSpec) - PP.<$$> bullets '*' (map Crucible.ppSimError - (false ^.. traverse . W4.labeledPredMsg)) + W4.partitionLabeledPreds (Proxy :: Proxy Sym) (owp ^. owpPreconditions) + in ppFailure owp false + +-- | Print a message about symbolic failure of an override's preconditions +ppSymbolicFailure :: + (OverrideWithPreconditions arch, [LabeledPred Sym]) -> + PP.Doc +ppSymbolicFailure = uncurry ppFailure -- | This function is responsible for implementing the \"override\" behavior -- of method specifications. The main work done in this function to manage @@ -432,7 +469,7 @@ methodSpecHandler opts sc cc top_loc css retTy = do -- 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. -- If so, there's no use in branching on them with @symbolicBranches@. - (true, false, unknown) <- liftIO $ partitionOWPs sym branches + (true, false, unknown) <- liftIO $ partitionOWPsConcrete sym branches -- Collapse the preconditions to a single predicate branches' <- liftIO $ forM (true ++ unknown) $ @@ -484,22 +521,37 @@ methodSpecHandler opts sc cc top_loc css retTy = do owp : _ -> owp ^. owpMethodSpec . csName _ -> "" - e = show $ - (PP.text $ unlines $ - [ "No override specification applies for " ++ fnName ++ "." - , if not (null false) - then unwords $ - [ "The following overrides had some preconditions " - , "that failed concretely:" - ] - else "" - ]) - PP.<$$> bullets '-' (map ppConcreteFailure false) - + e symFalse = show $ + PP.text + ("No override specification applies for " ++ fnName ++ ".") + PP.<$$> + if null false + then "" + else PP.text (unwords + [ "The following overrides had some preconditions " + , "that failed concretely:" + ]) PP.<$$> bullets '-' (map ppConcreteFailure false) + PP.<$$> + if null symFalse + then "" + else PP.text (unwords + [ "The following overrides had some preconditions " + , "that failed symbolically:" + ]) PP.<$$> bullets '-' (map ppSymbolicFailure symFalse) in ( W4.truePred sym - , liftIO $ Crucible.addFailedAssertion sym (Crucible.GenericSimError e) + , liftIO $ do + -- Now that we're failing, do the additional work of figuring out + -- if any overrides had symbolically false preconditions + symFalse <- catMaybes <$> (forM unknown $ \owp -> + findFalsePreconditions sym owp <&> + \case + [] -> Nothing + ps -> Just (owp, ps)) + + Crucible.addFailedAssertion sym + (Crucible.GenericSimError (e symFalse)) , Just (W4.plSourceLoc top_loc) ) ])) From 97ce94c4764acd3e3694c5497a0b040e57f9ec79 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Mon, 22 Apr 2019 16:55:42 -0700 Subject: [PATCH 10/14] Add a message when no preconditions symbolically _or_ concretely fail The user will still be wondering what happened. --- src/SAWScript/CrucibleOverride.hs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index ed23a8e929..495f70d370 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -538,6 +538,13 @@ methodSpecHandler opts sc cc top_loc css retTy = do [ "The following overrides had some preconditions " , "that failed symbolically:" ]) PP.<$$> bullets '-' (map ppSymbolicFailure symFalse) + PP.<$$> + if null false && null symFalse + then PP.text $ unwords $ + [ "No overrides had any single concretely or symbolically" + , "failing preconditions. This can mean that your override" + , "has mutually inconsistent preconditions." + ] in ( W4.truePred sym From f0ec30020a3b0303cd72037998f3141dccad49bf Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 14 May 2019 14:20:22 -0700 Subject: [PATCH 11/14] fix merge conflict --- src/SAWScript/CrucibleOverride.hs | 36 +++++++++++++++---------------- 1 file changed, 17 insertions(+), 19 deletions(-) diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index c7240ff85c..ea833ee83b 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -78,7 +78,6 @@ import qualified What4.BaseTypes as W4 import qualified What4.Expr.Builder as W4 import qualified What4.Interface as W4 import qualified What4.LabeledPred as W4 -import qualified What4.Symbol as W4 import qualified What4.Partial as W4 import qualified What4.ProgramLoc as W4 import qualified What4.Symbol as W4 @@ -542,27 +541,26 @@ methodSpecHandler opts sc cc top_loc css retTy = do ]) PP.<$$> bullets '-' (map ppSymbolicFailure symFalse) PP.<$$> if null false && null symFalse - then PP.text $ unwords $ + then PP.text (unwords [ "No overrides had any single concretely or symbolically" , "failing preconditions. This can mean that your override" , "has mutually inconsistent preconditions." - ] - - in - ( W4.truePred sym - , liftIO $ do - -- Now that we're failing, do the additional work of figuring out - -- if any overrides had symbolically false preconditions - symFalse <- catMaybes <$> (forM unknown $ \owp -> - findFalsePreconditions sym owp <&> - \case - [] -> Nothing - ps -> Just (owp, ps)) - - Crucible.addFailedAssertion sym - (Crucible.GenericSimError (e symFalse)) - , Just (W4.plSourceLoc top_loc) - ) + ]) + else PP.empty + in ( W4.truePred sym + , liftIO $ do + -- Now that we're failing, do the additional work of figuring out + -- if any overrides had symbolically false preconditions + symFalse <- catMaybes <$> (forM unknown $ \owp -> + findFalsePreconditions sym owp <&> + \case + [] -> Nothing + ps -> Just (owp, ps)) + + Crucible.addFailedAssertion sym + (Crucible.GenericSimError (e symFalse)) + , Just (W4.plSourceLoc top_loc) + ) ])) (Crucible.RegMap args) From a09ad894582985ef902f23dbc1f5be09f59a4060 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 14 May 2019 14:26:07 -0700 Subject: [PATCH 12/14] Don't print symbolic override matching failures --- src/SAWScript/CrucibleOverride.hs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index ea833ee83b..01d1b8010a 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -391,10 +391,14 @@ ppConcreteFailure owp = in ppFailure owp false -- | Print a message about symbolic failure of an override's preconditions +-- +-- TODO: Needs additional testing. Are these messages useful? +{- ppSymbolicFailure :: (OverrideWithPreconditions arch, [LabeledPred Sym]) -> PP.Doc ppSymbolicFailure = uncurry ppFailure +-} -- | This function is responsible for implementing the \"override\" behavior -- of method specifications. The main work done in this function to manage @@ -532,6 +536,9 @@ methodSpecHandler opts sc cc top_loc css retTy = do [ "The following overrides had some preconditions " , "that failed concretely:" ]) PP.<$$> bullets '-' (map ppConcreteFailure false) + -- See comment on ppSymbolicFailure: needs more testing to + -- decide if it's useful. + {- PP.<$$> if null symFalse then "" @@ -539,6 +546,7 @@ methodSpecHandler opts sc cc top_loc css retTy = do [ "The following overrides had some preconditions " , "that failed symbolically:" ]) PP.<$$> bullets '-' (map ppSymbolicFailure symFalse) + -} PP.<$$> if null false && null symFalse then PP.text (unwords From fe054b4a908f4801d21f22fbf89afa79bf537506 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 14 May 2019 14:46:03 -0700 Subject: [PATCH 13/14] fix logging bug: null -> not null --- src/SAWScript/CrucibleOverride.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index 01d1b8010a..ec688b4982 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -530,7 +530,7 @@ methodSpecHandler opts sc cc top_loc css retTy = do PP.text ("No override specification applies for " ++ fnName ++ ".") PP.<$$> - if null false + if not (null false) then "" else PP.text (unwords [ "The following overrides had some preconditions " @@ -540,7 +540,7 @@ methodSpecHandler opts sc cc top_loc css retTy = do -- decide if it's useful. {- PP.<$$> - if null symFalse + if not (null symFalse) then "" else PP.text (unwords [ "The following overrides had some preconditions " From e7c8b891d493b1881f1e94d2fad1ed5e90b09021 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 14 May 2019 16:01:44 -0700 Subject: [PATCH 14/14] Allow the user to see all overrides with --sim-verbose=3 --- src/SAWScript/CrucibleOverride.hs | 50 ++++++++++++++++++------------- 1 file changed, 29 insertions(+), 21 deletions(-) diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index ec688b4982..0a698ace3b 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -6,6 +6,7 @@ {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ParallelListComp #-} {-# LANGUAGE PatternGuards #-} @@ -526,35 +527,42 @@ methodSpecHandler opts sc cc top_loc css retTy = do owp : _ -> owp ^. owpMethodSpec . csName _ -> "" - e symFalse = show $ + e _symFalse = show $ PP.text ("No override specification applies for " ++ fnName ++ ".") PP.<$$> - if not (null false) - then "" - else PP.text (unwords - [ "The following overrides had some preconditions " + if | not (null false) -> + PP.text (unwords + [ "The following overrides had some preconditions" , "that failed concretely:" ]) PP.<$$> bullets '-' (map ppConcreteFailure false) - -- See comment on ppSymbolicFailure: needs more testing to - -- decide if it's useful. - {- - PP.<$$> - if not (null symFalse) - then "" - else PP.text (unwords + -- See comment on ppSymbolicFailure: both of the following + -- need more examination to see if they're useful. + {- + | not (null symFalse) -> + PP.text (unwords [ "The following overrides had some preconditions " , "that failed symbolically:" ]) PP.<$$> bullets '-' (map ppSymbolicFailure symFalse) - -} - PP.<$$> - if null false && null symFalse - then PP.text (unwords - [ "No overrides had any single concretely or symbolically" - , "failing preconditions. This can mean that your override" - , "has mutually inconsistent preconditions." - ]) - else PP.empty + | null false && null symFalse -> + PP.text (unwords + [ "No overrides had any single concretely or" + , "symbolically failing preconditions. This can mean" + , "that your override has mutually inconsistent" + , "preconditions." + ]) + PP.<$$> + -} + | simVerbose opts < 3 -> + PP.text $ unwords + [ "Run SAW with --sim-verbose=3 to see a description" + , "of each override." + ] + | otherwise -> + PP.text "Here are the descriptions of each override:" + PP.<$$> + bullets '-' + (branches ^.. each . owpMethodSpec . to ppMethodSpec) in ( W4.truePred sym , liftIO $ do -- Now that we're failing, do the additional work of figuring out