diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs index 4038a3928..744ea359d 100644 --- a/crucible-cli/src/Lang/Crucible/CLI.hs +++ b/crucible-cli/src/Lang/Crucible/CLI.hs @@ -20,7 +20,6 @@ module Lang.Crucible.CLI , execCommand ) where -import Control.Lens (view) import Control.Monad import Data.Foldable @@ -50,18 +49,19 @@ import Lang.Crucible.Syntax.SExpr import Lang.Crucible.Analysis.Postdom import Lang.Crucible.Backend +import Lang.Crucible.Backend.Prove (ProofResult(..), proveCurrentObligations) import Lang.Crucible.Backend.Simple import Lang.Crucible.FunctionHandle import Lang.Crucible.Simulator import Lang.Crucible.Simulator.Profiling import What4.Config -import What4.Interface (getConfiguration,notPred) +import What4.Interface (getConfiguration) import What4.Expr (ExprBuilder, newExprBuilder, EmptyExprBuilderState(..)) import What4.FunctionName import What4.ProgramLoc -import What4.SatResult -import What4.Solver (defaultLogData, runZ3InOverride, z3Options) +import What4.Solver (defaultLogData) +import What4.Solver.Z3 (z3Adapter, z3Options) -- | Allows users to hook into the various stages of 'simulateProgram'. data SimulateProgramHooks ext = SimulateProgramHooks @@ -180,19 +180,13 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks = getProofObligations bak >>= \case Nothing -> hPutStrLn outh "==== No proof obligations ====" - Just gs -> - do hPutStrLn outh "==== Proof obligations ====" - forM_ (goalsToList gs) (\g -> - do hPrint outh =<< ppProofObligation sym g - neggoal <- notPred sym (view labeledPred (proofGoal g)) - asms <- assumptionsPred sym (proofAssumptions g) - let bs = [neggoal, asms] - runZ3InOverride sym defaultLogData bs (\case - Sat _ -> hPutStrLn outh "COUNTEREXAMPLE" - Unsat _ -> hPutStrLn outh "PROVED" - Unknown -> hPutStrLn outh "UNKNOWN" - ) - ) + Just {} -> hPutStrLn outh "==== Proof obligations ====" + proveCurrentObligations bak defaultLogData z3Adapter $ \goal res -> do + hPrint outh =<< ppProofObligation sym goal + case res of + Proved {} -> hPutStrLn outh "PROVED" + Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE" + Unknown {} -> hPutStrLn outh "UNKNOWN" _ -> hPutStrLn outh "No suitable main function found" diff --git a/crucible-cli/test-data/simulate/override-nondet-test-both.out.good b/crucible-cli/test-data/simulate/override-nondet-test-both.out.good index 03a2abe54..3a72948e8 100644 --- a/crucible-cli/test-data/simulate/override-nondet-test-both.out.good +++ b/crucible-cli/test-data/simulate/override-nondet-test-both.out.good @@ -29,8 +29,8 @@ Assuming: in not (and v7 v12 (not (and v7 v12))) * The branch in nondetBranchesTest from after branch 0 to second branch let -- test-data/simulate/override-nondet-test-both.cbl:10:5 - v43 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i))) - in not v43 + v47 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i))) + in not v47 * The branch in main from test-data/simulate/override-nondet-test-both.cbl:7:12 to first branch let -- test-data/simulate/override-nondet-test-both.cbl:7:12 v7 = eq 0 cw@0:i @@ -55,8 +55,8 @@ Assuming: in not (and v7 v12 (not (and v7 v12))) * The branch in nondetBranchesTest from after branch 0 to second branch let -- test-data/simulate/override-nondet-test-both.cbl:10:5 - v54 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i))) - in not v54 + v58 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i))) + in not v58 * The branch in main from test-data/simulate/override-nondet-test-both.cbl:7:12 to first branch let -- test-data/simulate/override-nondet-test-both.cbl:7:12 v7 = eq 0 cw@0:i diff --git a/crucible-cli/test-data/simulate/override-test2.out.good b/crucible-cli/test-data/simulate/override-test2.out.good index da5a28651..157a31595 100644 --- a/crucible-cli/test-data/simulate/override-test2.out.good +++ b/crucible-cli/test-data/simulate/override-test2.out.good @@ -17,8 +17,8 @@ COUNTEREXAMPLE Assuming: * The branch in symbolicBranchesTest from after branch 1 to third branch let -- test-data/simulate/override-test2.cbl:7:5 - v30 = and (not (eq 1 cx@0:i)) (not (eq 2 cx@0:i)) (not (eq 3 cx@0:i)) - in not v30 + v37 = and (not (eq 1 cx@0:i)) (not (eq 2 cx@0:i)) (not (eq 3 cx@0:i)) + in not v37 Prove: test-data/simulate/override-test2.cbl:6:5: error: in main bogus! diff --git a/crucible-symio/tests/TestMain.hs b/crucible-symio/tests/TestMain.hs index d2070f8c2..24fc89b6a 100644 --- a/crucible-symio/tests/TestMain.hs +++ b/crucible-symio/tests/TestMain.hs @@ -42,6 +42,7 @@ import qualified Data.BitVector.Sized as BVS import qualified Test.Tasty as T import qualified Test.Tasty.HUnit as T +import qualified Lang.Crucible.Backend.Prove as CB import qualified Lang.Crucible.Backend.Simple as CB import qualified Lang.Crucible.Backend as CB import qualified Lang.Crucible.CFG.Core as CC @@ -56,7 +57,6 @@ import qualified What4.Expr as WE import qualified What4.Config as W4C import qualified What4.Solver.Yices as W4Y import qualified What4.Solver.Adapter as WSA -import qualified What4.SatResult as W4R import qualified What4.Partial as W4 import qualified What4.CachedArray as CA @@ -133,26 +133,15 @@ runFSTest' bak (FSTest fsTest) = do _ -> do putStrLn $ showF p T.assertFailure "Partial Result" - obligations <- CB.getProofObligations bak - mapM_ (proveGoal sym W4Y.yicesAdapter) (maybe [] CB.goalsToList obligations) - -proveGoal :: - (sym ~ WE.ExprBuilder t st fs) => - CB.IsSymInterface sym => - sym -> - WSA.SolverAdapter st -> - CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) -> - IO () -proveGoal sym adapter (CB.ProofGoal asms goal) = do - let goalPred = goal ^. CB.labeledPred - asmsPred <- CB.assumptionsPred sym asms - notgoal <- W4.notPred sym goalPred - WSA.solver_adapter_check_sat adapter sym WSA.defaultLogData [notgoal, asmsPred] $ \sr -> - case sr of - W4R.Unsat _ -> return () - W4R.Unknown -> T.assertFailure "Inconclusive" - W4R.Sat _ -> do + CB.proveCurrentObligations bak WSA.defaultLogData W4Y.yicesAdapter $ \obligation -> + \case + CB.Proved {} -> return () + CB.Unknown {} -> T.assertFailure "Inconclusive" + CB.Disproved _ _ -> do + CB.ProofGoal asms goal <- pure obligation + asmsPred <- CB.assumptionsPred sym asms + let goalPred = goal ^. CB.labeledPred putStrLn (showF asmsPred) putStrLn (showF goalPred) T.assertFailure "Assertion Failure" diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal index 4540ec190..c778eca6b 100644 --- a/crucible/crucible.cabal +++ b/crucible/crucible.cabal @@ -72,6 +72,9 @@ library hs-source-dirs: src + other-modules: + Lang.Crucible.Backend.Assumptions + exposed-modules: Lang.Crucible.Analysis.DFS Lang.Crucible.Analysis.ForwardDataflow @@ -83,6 +86,7 @@ library Lang.Crucible.Backend.AssumptionStack Lang.Crucible.Backend.ProofGoals Lang.Crucible.Backend.Online + Lang.Crucible.Backend.Prove Lang.Crucible.Backend.Simple Lang.Crucible.Concretize Lang.Crucible.CFG.Common diff --git a/crucible/src/Lang/Crucible/Backend.hs b/crucible/src/Lang/Crucible/Backend.hs index 130173396..75b346284 100644 --- a/crucible/src/Lang/Crucible/Backend.hs +++ b/crucible/src/Lang/Crucible/Backend.hs @@ -42,37 +42,16 @@ module Lang.Crucible.Backend ( IsSymBackend(..) , IsSymInterface , HasSymInterface(..) - , SomeBackend(..) - - -- * Assumption management - , CrucibleAssumption(..) - , CrucibleEvent(..) - , CrucibleAssumptions(..) - , Assumption , Assertion - , Assumptions - - , concretizeEvents - , ppEvent - , singleEvent - , singleAssumption - , trivialAssumption - , impossibleAssumption - , ppAssumption - , assumptionLoc - , eventLoc - , mergeAssumptions - , assumptionPred - , forgetAssumption - , assumptionsPred - , flattenAssumptions - , assumptionsTopLevelLocs + , SomeBackend(..) , ProofObligation , ProofObligations , AssumptionState , assert + , impossibleAssumption -- ** Reexports + , module Lang.Crucible.Backend.Assumptions , LabeledPred(..) , labeledPred , labeledPredMsg @@ -107,15 +86,10 @@ module Lang.Crucible.Backend ) where import Control.Exception(Exception(..), throwIO) -import Control.Lens ((^.), Traversal, folded) +import Control.Lens ((^.)) import Control.Monad import Control.Monad.IO.Class -import Data.Kind (Type) import Data.Foldable (toList) -import Data.Functor.Identity -import Data.Functor.Const -import qualified Data.Sequence as Seq -import Data.Sequence (Seq) import Data.Set (Set) import qualified Prettyprinter as PP import GHC.Stack @@ -130,199 +104,16 @@ import What4.InterpretedFloatingPoint import What4.LabeledPred import What4.Partial import What4.ProgramLoc -import What4.Expr (GroundValue, GroundValueWrapper(..)) + import What4.Solver import qualified What4.Solver.Z3 as Z3 +import Lang.Crucible.Backend.Assumptions import qualified Lang.Crucible.Backend.AssumptionStack as AS import qualified Lang.Crucible.Backend.ProofGoals as PG import Lang.Crucible.Simulator.SimError --- | This type describes assumptions made at some point during program execution. -data CrucibleAssumption (e :: BaseType -> Type) - = GenericAssumption ProgramLoc String (e BaseBoolType) - -- ^ An unstructured description of the source of an assumption. - - | BranchCondition ProgramLoc (Maybe ProgramLoc) (e BaseBoolType) - -- ^ This arose because we want to explore a specific path. - -- The first location is the location of the branch predicate. - -- The second one is the location of the branch target. - - | AssumingNoError SimError (e BaseBoolType) - -- ^ An assumption justified by a proof of the impossibility of - -- a certain simulator error. - --- | This type describes events we can track during program execution. -data CrucibleEvent (e :: BaseType -> Type) where - -- | This event describes the creation of a symbolic variable. - CreateVariableEvent :: - ProgramLoc {- ^ location where the variable was created -} -> - String {- ^ user-provided name for the variable -} -> - BaseTypeRepr tp {- ^ type of the variable -} -> - e tp {- ^ the variable expression -} -> - CrucibleEvent e - - -- | This event describes reaching a particular program location. - LocationReachedEvent :: - ProgramLoc -> - CrucibleEvent e - --- | Pretty print an event -ppEvent :: IsExpr e => CrucibleEvent e -> PP.Doc ann -ppEvent (CreateVariableEvent loc nm _tpr v) = - "create var" PP.<+> PP.pretty nm PP.<+> "=" PP.<+> printSymExpr v PP.<+> "at" PP.<+> PP.pretty (plSourceLoc loc) -ppEvent (LocationReachedEvent loc) = - "reached" PP.<+> PP.pretty (plSourceLoc loc) PP.<+> "in" PP.<+> PP.pretty (plFunction loc) - --- | Return the program location associated with an event -eventLoc :: CrucibleEvent e -> ProgramLoc -eventLoc (CreateVariableEvent loc _ _ _) = loc -eventLoc (LocationReachedEvent loc) = loc - --- | Return the program location associated with an assumption -assumptionLoc :: CrucibleAssumption e -> ProgramLoc -assumptionLoc r = - case r of - GenericAssumption l _ _ -> l - BranchCondition l _ _ -> l - AssumingNoError s _ -> simErrorLoc s - --- | Get the predicate associated with this assumption -assumptionPred :: CrucibleAssumption e -> e BaseBoolType -assumptionPred (AssumingNoError _ p) = p -assumptionPred (BranchCondition _ _ p) = p -assumptionPred (GenericAssumption _ _ p) = p - --- | If an assumption is clearly impossible, return an abort reason --- that can be used to unwind the execution of this branch. -impossibleAssumption :: IsExpr e => CrucibleAssumption e -> Maybe AbortExecReason -impossibleAssumption (AssumingNoError err p) - | Just False <- asConstantPred p = Just (AssertionFailure err) -impossibleAssumption (BranchCondition loc _ p) - | Just False <- asConstantPred p = Just (InfeasibleBranch loc) -impossibleAssumption (GenericAssumption loc _ p) - | Just False <- asConstantPred p = Just (InfeasibleBranch loc) -impossibleAssumption _ = Nothing - -forgetAssumption :: CrucibleAssumption e -> CrucibleAssumption (Const ()) -forgetAssumption = runIdentity . traverseAssumption (\_ -> Identity (Const ())) - -traverseAssumption :: Traversal (CrucibleAssumption e) (CrucibleAssumption e') (e BaseBoolType) (e' BaseBoolType) -traverseAssumption f = \case - GenericAssumption loc msg p -> GenericAssumption loc msg <$> f p - BranchCondition l t p -> BranchCondition l t <$> f p - AssumingNoError err p -> AssumingNoError err <$> f p - --- | This type tracks both logical assumptions and program events --- that are relevant when evaluating proof obligations arising --- from simulation. -data CrucibleAssumptions (e :: BaseType -> Type) where - SingleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e - SingleEvent :: CrucibleEvent e -> CrucibleAssumptions e - ManyAssumptions :: Seq (CrucibleAssumptions e) -> CrucibleAssumptions e - MergeAssumptions :: - e BaseBoolType {- ^ branch condition -} -> - CrucibleAssumptions e {- ^ "then" assumptions -} -> - CrucibleAssumptions e {- ^ "else" assumptions -} -> - CrucibleAssumptions e - -instance Semigroup (CrucibleAssumptions e) where - ManyAssumptions xs <> ManyAssumptions ys = ManyAssumptions (xs <> ys) - ManyAssumptions xs <> y = ManyAssumptions (xs Seq.|> y) - x <> ManyAssumptions ys = ManyAssumptions (x Seq.<| ys) - x <> y = ManyAssumptions (Seq.fromList [x,y]) - -instance Monoid (CrucibleAssumptions e) where - mempty = ManyAssumptions mempty - -singleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e -singleAssumption x = SingleAssumption x - -singleEvent :: CrucibleEvent e -> CrucibleAssumptions e -singleEvent x = SingleEvent x - --- | Collect the program locations of all assumptions and --- events that did not occur in the context of a symbolic branch. --- These are locations that every program path represented by --- this @CrucibleAssumptions@ structure must have passed through. -assumptionsTopLevelLocs :: CrucibleAssumptions e -> [ProgramLoc] -assumptionsTopLevelLocs (SingleEvent e) = [eventLoc e] -assumptionsTopLevelLocs (SingleAssumption a) = [assumptionLoc a] -assumptionsTopLevelLocs (ManyAssumptions as) = concatMap assumptionsTopLevelLocs as -assumptionsTopLevelLocs MergeAssumptions{} = [] - --- | Compute the logical predicate corresponding to this collection of assumptions. -assumptionsPred :: IsExprBuilder sym => sym -> Assumptions sym -> IO (Pred sym) -assumptionsPred sym (SingleEvent _) = - return (truePred sym) -assumptionsPred _sym (SingleAssumption a) = - return (assumptionPred a) -assumptionsPred sym (ManyAssumptions xs) = - andAllOf sym folded =<< traverse (assumptionsPred sym) xs -assumptionsPred sym (MergeAssumptions c xs ys) = - do xs' <- assumptionsPred sym xs - ys' <- assumptionsPred sym ys - itePred sym c xs' ys' - -traverseEvent :: Applicative m => - (forall tp. e tp -> m (e' tp)) -> - CrucibleEvent e -> m (CrucibleEvent e') -traverseEvent f (CreateVariableEvent loc nm tpr v) = CreateVariableEvent loc nm tpr <$> f v -traverseEvent _ (LocationReachedEvent loc) = pure (LocationReachedEvent loc) - --- | Given a ground evaluation function, compute a linear, ground-valued --- sequence of events corresponding to this program run. -concretizeEvents :: - IsExpr e => - (forall tp. e tp -> IO (GroundValue tp)) -> - CrucibleAssumptions e -> - IO [CrucibleEvent GroundValueWrapper] -concretizeEvents f = loop - where - loop (SingleEvent e) = - do e' <- traverseEvent (\v -> GVW <$> f v) e - return [e'] - loop (SingleAssumption _) = return [] - loop (ManyAssumptions as) = concat <$> traverse loop as - loop (MergeAssumptions p xs ys) = - do b <- f p - if b then loop xs else loop ys - --- | Given a @CrucibleAssumptions@ structure, flatten all the muxed assumptions into --- a flat sequence of assumptions that have been appropriately weakened. --- Note, once these assumptions have been flattened, their order might no longer --- strictly correspond to any concrete program run. -flattenAssumptions :: IsExprBuilder sym => sym -> Assumptions sym -> IO [Assumption sym] -flattenAssumptions sym = loop Nothing - where - loop _mz (SingleEvent _) = return [] - loop mz (SingleAssumption a) = - do a' <- maybe (pure a) (\z -> traverseAssumption (impliesPred sym z) a) mz - if trivialAssumption a' then return [] else return [a'] - loop mz (ManyAssumptions as) = - concat <$> traverse (loop mz) as - loop mz (MergeAssumptions p xs ys) = - do pnot <- notPred sym p - px <- maybe (pure p) (andPred sym p) mz - py <- maybe (pure pnot) (andPred sym pnot) mz - xs' <- loop (Just px) xs - ys' <- loop (Just py) ys - return (xs' <> ys') - --- | Merge the assumptions collected from the branches of a conditional. -mergeAssumptions :: - IsExprBuilder sym => - sym -> - Pred sym -> - Assumptions sym -> - Assumptions sym -> - IO (Assumptions sym) -mergeAssumptions _sym p thens elses = - return (MergeAssumptions p thens elses) - -type Assertion sym = LabeledPred (Pred sym) SimError -type Assumption sym = CrucibleAssumption (SymExpr sym) -type Assumptions sym = CrucibleAssumptions (SymExpr sym) +type Assertion sym = LabeledPred (Pred sym) SimError type ProofObligation sym = AS.ProofGoal (Assumptions sym) (Assertion sym) type ProofObligations sym = Maybe (AS.Goals (Assumptions sym) (Assertion sym)) type AssumptionState sym = PG.GoalCollector (Assumptions sym) (Assertion sym) @@ -350,6 +141,17 @@ data AbortExecReason = instance Exception AbortExecReason +-- | If an assumption is clearly impossible, return an abort reason +-- that can be used to unwind the execution of this branch. +impossibleAssumption :: IsExpr e => CrucibleAssumption e -> Maybe AbortExecReason +impossibleAssumption (AssumingNoError err p) + | Just False <- asConstantPred p = Just (AssertionFailure err) +impossibleAssumption (BranchCondition loc _ p) + | Just False <- asConstantPred p = Just (InfeasibleBranch loc) +impossibleAssumption (GenericAssumption loc _ p) + | Just False <- asConstantPred p = Just (InfeasibleBranch loc) +impossibleAssumption _ = Nothing + ppAbortExecReason :: AbortExecReason -> PP.Doc ann ppAbortExecReason e = case e of @@ -361,47 +163,21 @@ ppAbortExecReason e = ] VariantOptionsExhausted l -> ppLocated l "Variant options exhausted." EarlyExit l -> ppLocated l "Program exited early." + where + ppLocated :: ProgramLoc -> PP.Doc ann -> PP.Doc ann + ppLocated l x = "in" PP.<+> ppFn l PP.<+> ppLoc l PP.<> ":" PP.<+> x -ppAssumption :: (forall tp. e tp -> PP.Doc ann) -> CrucibleAssumption e -> PP.Doc ann -ppAssumption ppDoc e = - case e of - GenericAssumption l msg p -> - PP.vsep [ ppLocated l (PP.pretty msg) - , ppDoc p - ] - BranchCondition l Nothing p -> - PP.vsep [ "The branch in" PP.<+> ppFn l PP.<+> "at" PP.<+> ppLoc l - , ppDoc p - ] - BranchCondition l (Just t) p -> - PP.vsep [ "The branch in" PP.<+> ppFn l PP.<+> "from" PP.<+> ppLoc l PP.<+> "to" PP.<+> ppLoc t - , ppDoc p - ] - AssumingNoError simErr p -> - PP.vsep [ "Assuming the following error does not occur:" - , PP.indent 2 (ppSimError simErr) - , ppDoc p - ] + ppFn :: ProgramLoc -> PP.Doc ann + ppFn l = PP.pretty (plFunction l) + + ppLoc :: ProgramLoc -> PP.Doc ann + ppLoc l = PP.pretty (plSourceLoc l) throwUnsupported :: (IsExprBuilder sym, MonadIO m, HasCallStack) => sym -> String -> m a throwUnsupported sym msg = liftIO $ do loc <- getCurrentProgramLoc sym throwIO $ SimError loc $ Unsupported callStack msg - --- | Check if an assumption is trivial (always true) -trivialAssumption :: IsExpr e => CrucibleAssumption e -> Bool -trivialAssumption a = asConstantPred (assumptionPred a) == Just True - -ppLocated :: ProgramLoc -> PP.Doc ann -> PP.Doc ann -ppLocated l x = "in" PP.<+> ppFn l PP.<+> ppLoc l PP.<> ":" PP.<+> x - -ppFn :: ProgramLoc -> PP.Doc ann -ppFn l = PP.pretty (plFunction l) - -ppLoc :: ProgramLoc -> PP.Doc ann -ppLoc l = PP.pretty (plSourceLoc l) - type IsSymInterface sym = ( IsSymExprBuilder sym , IsInterpretedFloatSymExprBuilder sym diff --git a/crucible/src/Lang/Crucible/Backend/Assumptions.hs b/crucible/src/Lang/Crucible/Backend/Assumptions.hs new file mode 100644 index 000000000..f6df983ac --- /dev/null +++ b/crucible/src/Lang/Crucible/Backend/Assumptions.hs @@ -0,0 +1,268 @@ +{-| +Module : Lang.Crucible.Backend.Assumptions +Copyright : (c) Galois, Inc 2014-2024 +License : BSD3 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} + +module Lang.Crucible.Backend.Assumptions + ( CrucibleAssumption(..) + , CrucibleEvent(..) + , CrucibleAssumptions(..) + , Assumption + , Assumptions + + , concretizeEvents + , ppEvent + , singleEvent + , singleAssumption + , trivialAssumption + , ppAssumption + , assumptionLoc + , eventLoc + , mergeAssumptions + , assumptionPred + , forgetAssumption + , assumptionsPred + , flattenAssumptions + , assumptionsTopLevelLocs + ) where + + +import Control.Lens (Traversal, folded) +import Data.Kind (Type) +import Data.Functor.Identity +import Data.Functor.Const +import qualified Data.Sequence as Seq +import Data.Sequence (Seq) +import qualified Prettyprinter as PP + +import What4.Expr.Builder +import What4.Interface +import What4.ProgramLoc +import What4.Expr (GroundValue, GroundValueWrapper(..)) + +import Lang.Crucible.Simulator.SimError + +type Assumption sym = CrucibleAssumption (SymExpr sym) +type Assumptions sym = CrucibleAssumptions (SymExpr sym) + +-- | This type describes assumptions made at some point during program execution. +data CrucibleAssumption (e :: BaseType -> Type) + = GenericAssumption ProgramLoc String (e BaseBoolType) + -- ^ An unstructured description of the source of an assumption. + + | BranchCondition ProgramLoc (Maybe ProgramLoc) (e BaseBoolType) + -- ^ This arose because we want to explore a specific path. + -- The first location is the location of the branch predicate. + -- The second one is the location of the branch target. + + | AssumingNoError SimError (e BaseBoolType) + -- ^ An assumption justified by a proof of the impossibility of + -- a certain simulator error. + +-- | This type describes events we can track during program execution. +data CrucibleEvent (e :: BaseType -> Type) where + -- | This event describes the creation of a symbolic variable. + CreateVariableEvent :: + ProgramLoc {- ^ location where the variable was created -} -> + String {- ^ user-provided name for the variable -} -> + BaseTypeRepr tp {- ^ type of the variable -} -> + e tp {- ^ the variable expression -} -> + CrucibleEvent e + + -- | This event describes reaching a particular program location. + LocationReachedEvent :: + ProgramLoc -> + CrucibleEvent e + +-- | Pretty print an event +ppEvent :: IsExpr e => CrucibleEvent e -> PP.Doc ann +ppEvent (CreateVariableEvent loc nm _tpr v) = + "create var" PP.<+> PP.pretty nm PP.<+> "=" PP.<+> printSymExpr v PP.<+> "at" PP.<+> PP.pretty (plSourceLoc loc) +ppEvent (LocationReachedEvent loc) = + "reached" PP.<+> PP.pretty (plSourceLoc loc) PP.<+> "in" PP.<+> PP.pretty (plFunction loc) + +-- | Return the program location associated with an event +eventLoc :: CrucibleEvent e -> ProgramLoc +eventLoc (CreateVariableEvent loc _ _ _) = loc +eventLoc (LocationReachedEvent loc) = loc + +-- | Return the program location associated with an assumption +assumptionLoc :: CrucibleAssumption e -> ProgramLoc +assumptionLoc r = + case r of + GenericAssumption l _ _ -> l + BranchCondition l _ _ -> l + AssumingNoError s _ -> simErrorLoc s + +-- | Get the predicate associated with this assumption +assumptionPred :: CrucibleAssumption e -> e BaseBoolType +assumptionPred (AssumingNoError _ p) = p +assumptionPred (BranchCondition _ _ p) = p +assumptionPred (GenericAssumption _ _ p) = p + +forgetAssumption :: CrucibleAssumption e -> CrucibleAssumption (Const ()) +forgetAssumption = runIdentity . traverseAssumption (\_ -> Identity (Const ())) + +-- | Check if an assumption is trivial (always true) +trivialAssumption :: IsExpr e => CrucibleAssumption e -> Bool +trivialAssumption a = asConstantPred (assumptionPred a) == Just True + +traverseAssumption :: Traversal (CrucibleAssumption e) (CrucibleAssumption e') (e BaseBoolType) (e' BaseBoolType) +traverseAssumption f = \case + GenericAssumption loc msg p -> GenericAssumption loc msg <$> f p + BranchCondition l t p -> BranchCondition l t <$> f p + AssumingNoError err p -> AssumingNoError err <$> f p + +-- | This type tracks both logical assumptions and program events +-- that are relevant when evaluating proof obligations arising +-- from simulation. +data CrucibleAssumptions (e :: BaseType -> Type) where + SingleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e + SingleEvent :: CrucibleEvent e -> CrucibleAssumptions e + ManyAssumptions :: Seq (CrucibleAssumptions e) -> CrucibleAssumptions e + MergeAssumptions :: + e BaseBoolType {- ^ branch condition -} -> + CrucibleAssumptions e {- ^ "then" assumptions -} -> + CrucibleAssumptions e {- ^ "else" assumptions -} -> + CrucibleAssumptions e + +instance Semigroup (CrucibleAssumptions e) where + ManyAssumptions xs <> ManyAssumptions ys = ManyAssumptions (xs <> ys) + ManyAssumptions xs <> y = ManyAssumptions (xs Seq.|> y) + x <> ManyAssumptions ys = ManyAssumptions (x Seq.<| ys) + x <> y = ManyAssumptions (Seq.fromList [x,y]) + +instance Monoid (CrucibleAssumptions e) where + mempty = ManyAssumptions mempty + +singleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e +singleAssumption x = SingleAssumption x + +singleEvent :: CrucibleEvent e -> CrucibleAssumptions e +singleEvent x = SingleEvent x + +-- | Collect the program locations of all assumptions and +-- events that did not occur in the context of a symbolic branch. +-- These are locations that every program path represented by +-- this @CrucibleAssumptions@ structure must have passed through. +assumptionsTopLevelLocs :: CrucibleAssumptions e -> [ProgramLoc] +assumptionsTopLevelLocs (SingleEvent e) = [eventLoc e] +assumptionsTopLevelLocs (SingleAssumption a) = [assumptionLoc a] +assumptionsTopLevelLocs (ManyAssumptions as) = concatMap assumptionsTopLevelLocs as +assumptionsTopLevelLocs MergeAssumptions{} = [] + +-- | Compute the logical predicate corresponding to this collection of assumptions. +assumptionsPred :: IsExprBuilder sym => sym -> Assumptions sym -> IO (Pred sym) +assumptionsPred sym (SingleEvent _) = + return (truePred sym) +assumptionsPred _sym (SingleAssumption a) = + return (assumptionPred a) +assumptionsPred sym (ManyAssumptions xs) = + andAllOf sym folded =<< traverse (assumptionsPred sym) xs +assumptionsPred sym (MergeAssumptions c xs ys) = + do xs' <- assumptionsPred sym xs + ys' <- assumptionsPred sym ys + itePred sym c xs' ys' + +traverseEvent :: Applicative m => + (forall tp. e tp -> m (e' tp)) -> + CrucibleEvent e -> m (CrucibleEvent e') +traverseEvent f (CreateVariableEvent loc nm tpr v) = CreateVariableEvent loc nm tpr <$> f v +traverseEvent _ (LocationReachedEvent loc) = pure (LocationReachedEvent loc) + +-- | Given a ground evaluation function, compute a linear, ground-valued +-- sequence of events corresponding to this program run. +concretizeEvents :: + IsExpr e => + (forall tp. e tp -> IO (GroundValue tp)) -> + CrucibleAssumptions e -> + IO [CrucibleEvent GroundValueWrapper] +concretizeEvents f = loop + where + loop (SingleEvent e) = + do e' <- traverseEvent (\v -> GVW <$> f v) e + return [e'] + loop (SingleAssumption _) = return [] + loop (ManyAssumptions as) = concat <$> traverse loop as + loop (MergeAssumptions p xs ys) = + do b <- f p + if b then loop xs else loop ys + +-- | Given a @CrucibleAssumptions@ structure, flatten all the muxed assumptions into +-- a flat sequence of assumptions that have been appropriately weakened. +-- Note, once these assumptions have been flattened, their order might no longer +-- strictly correspond to any concrete program run. +flattenAssumptions :: IsExprBuilder sym => sym -> Assumptions sym -> IO [Assumption sym] +flattenAssumptions sym = loop Nothing + where + loop _mz (SingleEvent _) = return [] + loop mz (SingleAssumption a) = + do a' <- maybe (pure a) (\z -> traverseAssumption (impliesPred sym z) a) mz + if trivialAssumption a' then return [] else return [a'] + loop mz (ManyAssumptions as) = + concat <$> traverse (loop mz) as + loop mz (MergeAssumptions p xs ys) = + do pnot <- notPred sym p + px <- maybe (pure p) (andPred sym p) mz + py <- maybe (pure pnot) (andPred sym pnot) mz + xs' <- loop (Just px) xs + ys' <- loop (Just py) ys + return (xs' <> ys') + +-- | Merge the assumptions collected from the branches of a conditional. +mergeAssumptions :: + IsExprBuilder sym => + sym -> + Pred sym -> + Assumptions sym -> + Assumptions sym -> + IO (Assumptions sym) +mergeAssumptions _sym p thens elses = + return (MergeAssumptions p thens elses) + +ppAssumption :: (forall tp. e tp -> PP.Doc ann) -> CrucibleAssumption e -> PP.Doc ann +ppAssumption ppDoc e = + case e of + GenericAssumption l msg p -> + PP.vsep [ ppLocated l (PP.pretty msg) + , ppDoc p + ] + BranchCondition l Nothing p -> + PP.vsep [ "The branch in" PP.<+> ppFn l PP.<+> "at" PP.<+> ppLoc l + , ppDoc p + ] + BranchCondition l (Just t) p -> + PP.vsep [ "The branch in" PP.<+> ppFn l PP.<+> "from" PP.<+> ppLoc l PP.<+> "to" PP.<+> ppLoc t + , ppDoc p + ] + AssumingNoError simErr p -> + PP.vsep [ "Assuming the following error does not occur:" + , PP.indent 2 (ppSimError simErr) + , ppDoc p + ] + where + ppLocated :: ProgramLoc -> PP.Doc ann -> PP.Doc ann + ppLocated l x = "in" PP.<+> ppFn l PP.<+> ppLoc l PP.<> ":" PP.<+> x + + ppFn :: ProgramLoc -> PP.Doc ann + ppFn l = PP.pretty (plFunction l) + + ppLoc :: ProgramLoc -> PP.Doc ann + ppLoc l = PP.pretty (plSourceLoc l) diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs new file mode 100644 index 000000000..01c14e85b --- /dev/null +++ b/crucible/src/Lang/Crucible/Backend/Prove.hs @@ -0,0 +1,149 @@ +{-| +Module : Lang.Crucible.Backend.Prove +Description : Proving goals under assumptions +Copyright : (c) Galois, Inc 2024 +License : BSD3 +-} + +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TypeOperators #-} + +module Lang.Crucible.Backend.Prove + ( ProofResult(..) + , proveGoal + , proveProofGoal + , proveGoals + , proveObligations + , proveCurrentObligations + ) where + +import Control.Lens ((^.)) +import Data.Functor.Const (Const(Const, getConst)) + +import qualified What4.Interface as W4 +import qualified What4.Expr as WE +import qualified What4.Solver.Adapter as WSA +import qualified What4.SatResult as W4R + +import qualified Lang.Crucible.Backend as CB +import Lang.Crucible.Backend.Assumptions (Assumptions) +import Lang.Crucible.Backend.ProofGoals (traverseGoalsWithAssumptions) + +-- | The result of attempting to prove a goal with an SMT solver. +-- +-- The constructors of this type correspond to those of 'W4R.SatResult'. +data ProofResult sym t + = -- | The goal was proved. + -- + -- Corresponds to 'W4R.Unsat'. + Proved + -- | The goal was disproved, and a model that falsifies it is available. + -- + -- Corresponds to 'W4R.Sat'. + | Disproved (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t)) + -- | The SMT solver returned \"unknown\". + -- + -- Corresponds to 'W4R.Unknown'. + | Unknown + +-- | Prove a single goal ('CB.Assertion') under the supplied 'Assumptions'. +-- +-- The overall approach is: +-- +-- * Gather all of the assumptions ('Assumptions') currently in scope (e.g., +-- from branch conditions). +-- * Negate the goal ('CB.Assertion') that were are trying to prove. +-- * Attempt to prove the conjunction of the assumptions and the negated goal. +-- +-- If this goal is satisfiable ('W4R.Sat'), then there exists a counterexample +-- that makes the original goal false, so we have disproven the goal. If the +-- negated goal is unsatisfiable ('W4R.Unsat'), on the other hand, then the +-- original goal is proven. +-- +-- Another way to think of this is as the negated material conditional +-- (implication) @not (assumptions -> assertion)@. This formula is equivalent +-- to @not ((not assumptions) and assertion)@, i.e., @assumptions and (not +-- assertion)@. +proveGoal :: + (sym ~ WE.ExprBuilder t st fs) => + W4.IsSymExprBuilder sym => + sym -> + WSA.LogData -> + WSA.SolverAdapter st -> + Assumptions sym -> + CB.Assertion sym -> + -- | Continuation to process the 'ProofResult'. + (CB.ProofObligation sym -> ProofResult sym t -> IO r) -> + IO r +proveGoal sym ld adapter asms goal k = do + let goalPred = goal ^. CB.labeledPred + asmsPred <- CB.assumptionsPred sym asms + notGoal <- W4.notPred sym goalPred + WSA.solver_adapter_check_sat adapter sym ld [asmsPred, notGoal] $ + k (CB.ProofGoal asms goal) . + \case + W4R.Sat (gfn, binds) -> Disproved gfn binds + W4R.Unsat () -> Proved + W4R.Unknown -> Unknown + +-- | Prove a single 'CB.ProofGoal'. +proveProofGoal :: + (sym ~ WE.ExprBuilder t st fs) => + W4.IsSymExprBuilder sym => + sym -> + WSA.LogData -> + WSA.SolverAdapter st -> + CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) -> + -- | Continuation to process the 'ProofResult'. + (CB.ProofObligation sym -> ProofResult sym t -> IO r) -> + IO r +proveProofGoal sym ld adapter (CB.ProofGoal asms goal) = + proveGoal sym ld adapter asms goal + +-- | Prove a collection of 'CB.Goals'. +proveGoals :: + (Monoid m, sym ~ WE.ExprBuilder t st fs) => + W4.IsSymExprBuilder sym => + sym -> + WSA.LogData -> + WSA.SolverAdapter st -> + CB.Goals (CB.Assumptions sym) (CB.Assertion sym) -> + -- | Continuation to process each 'ProofResult'. + (CB.ProofObligation sym -> ProofResult sym t -> IO m) -> + IO m +proveGoals sym ld adapter goals k = + getConst $ + traverseGoalsWithAssumptions + (\as g -> Const (proveGoal sym ld adapter as g k)) + goals + +-- | Prove a collection of 'CB.ProofObligations'. +proveObligations :: + (Monoid m, sym ~ WE.ExprBuilder t st fs) => + sym -> + WSA.LogData -> + WSA.SolverAdapter st -> + CB.ProofObligations sym -> + -- | Continuation to process each 'ProofResult'. + (CB.ProofObligation sym -> ProofResult sym t -> IO m) -> + IO m +proveObligations sym ld adapter obligations k = + case obligations of + Nothing -> pure mempty + Just goals -> proveGoals sym ld adapter goals k + +-- | Prove a the current collection of 'CB.ProofObligations' associated with the +-- symbolic backend (retrieved via 'CB.getProofObligations'). +proveCurrentObligations :: + (Monoid m, CB.IsSymBackend sym bak, sym ~ WE.ExprBuilder t st fs) => + bak -> + WSA.LogData -> + WSA.SolverAdapter st -> + -- | Continuation to process each 'ProofResult'. + (CB.ProofObligation sym -> ProofResult sym t -> IO m) -> + IO m +proveCurrentObligations bak ld adapter k = do + obligations <- CB.getProofObligations bak + let sym = CB.backendGetSym bak + proveObligations sym ld adapter obligations k