From cc2d973360f197070a688e6319e965d6a4212c34 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 18 Jun 2024 14:24:38 -0400 Subject: [PATCH 1/9] Factor assumptions into their own module --- crucible/crucible.cabal | 3 + crucible/src/Lang/Crucible/Backend.hs | 273 ++---------------- .../src/Lang/Crucible/Backend/Assumptions.hs | 268 +++++++++++++++++ .../src/Lang/Crucible/Backend/ProofGoals.hs | 9 + 4 files changed, 304 insertions(+), 249 deletions(-) create mode 100644 crucible/src/Lang/Crucible/Backend/Assumptions.hs diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal index 4540ec190..d4e6431a4 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 diff --git a/crucible/src/Lang/Crucible/Backend.hs b/crucible/src/Lang/Crucible/Backend.hs index 130173396..5fa447629 100644 --- a/crucible/src/Lang/Crucible/Backend.hs +++ b/crucible/src/Lang/Crucible/Backend.hs @@ -43,36 +43,14 @@ module Lang.Crucible.Backend , 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 , ProofObligation , ProofObligations , AssumptionState , assert + , impossibleAssumption -- ** Reexports + , module Lang.Crucible.Backend.Assumptions , LabeledPred(..) , labeledPred , labeledPredMsg @@ -107,15 +85,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 +103,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 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 +140,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 +162,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/ProofGoals.hs b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs index 38ea32b42..4b52a32fa 100644 --- a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs @@ -18,6 +18,7 @@ module Lang.Crucible.Backend.ProofGoals , traverseGoals, traverseOnlyGoals , traverseGoalsWithAssumptions , traverseGoalsSeq + -- ** Proving goals -- * Goal collector , FrameIdentifier(..), GoalCollector @@ -45,6 +46,14 @@ import Data.Sequence (Seq) import qualified Data.Sequence as Seq import Data.Word +import qualified What4.Interface as W4 +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 + -- | A proof goal consists of a collection of assumptions -- that were in scope when an assertion was made, together -- with the given assertion. From 79f17f2cc9434ece4e77d2f9aec00518b675c597 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 18 Jun 2024 14:46:21 -0400 Subject: [PATCH 2/9] Helpers for proving goals --- crucible/crucible.cabal | 1 + crucible/src/Lang/Crucible/Backend.hs | 3 +- .../src/Lang/Crucible/Backend/ProofGoals.hs | 8 --- crucible/src/Lang/Crucible/Backend/Prove.hs | 54 +++++++++++++++++++ 4 files changed, 57 insertions(+), 9 deletions(-) create mode 100644 crucible/src/Lang/Crucible/Backend/Prove.hs diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal index d4e6431a4..c1c8ec833 100644 --- a/crucible/crucible.cabal +++ b/crucible/crucible.cabal @@ -74,6 +74,7 @@ library other-modules: Lang.Crucible.Backend.Assumptions + Lang.Crucible.Backend.Prove exposed-modules: Lang.Crucible.Analysis.DFS diff --git a/crucible/src/Lang/Crucible/Backend.hs b/crucible/src/Lang/Crucible/Backend.hs index 5fa447629..75b346284 100644 --- a/crucible/src/Lang/Crucible/Backend.hs +++ b/crucible/src/Lang/Crucible/Backend.hs @@ -42,6 +42,7 @@ module Lang.Crucible.Backend ( IsSymBackend(..) , IsSymInterface , HasSymInterface(..) + , Assertion , SomeBackend(..) , ProofObligation , ProofObligations @@ -112,7 +113,7 @@ import qualified Lang.Crucible.Backend.AssumptionStack as AS import qualified Lang.Crucible.Backend.ProofGoals as PG import Lang.Crucible.Simulator.SimError -type Assertion sym = LabeledPred (Pred sym) SimError +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) diff --git a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs index 4b52a32fa..3e0b86cc2 100644 --- a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs @@ -46,14 +46,6 @@ import Data.Sequence (Seq) import qualified Data.Sequence as Seq import Data.Word -import qualified What4.Interface as W4 -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 - -- | A proof goal consists of a collection of assumptions -- that were in scope when an assertion was made, together -- with the given assertion. diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs new file mode 100644 index 000000000..e1c9f8470 --- /dev/null +++ b/crucible/src/Lang/Crucible/Backend/Prove.hs @@ -0,0 +1,54 @@ +{-| +Module : Lang.Crucible.Backend.Prove +Description : Proving goals under assumptions +Copyright : (c) Galois, Inc 2024 +License : BSD3 +-} + +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeOperators #-} + +module Lang.Crucible.Backend.Prove + ( proveGoal + , proveProofGoal + ) where + +import Control.Lens ((^.)) + +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) + +proveGoal :: + (sym ~ WE.ExprBuilder t st fs) => + W4.IsSymExprBuilder sym => + sym -> + WSA.LogData -> + WSA.SolverAdapter st -> + Assumptions sym -> + CB.Assertion sym -> + (W4R.SatResult (WE.GroundEvalFn t, Maybe (WE.ExprRangeBindings 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 + +proveProofGoal :: + (sym ~ WE.ExprBuilder t st fs) => + W4.IsSymExprBuilder sym => + sym -> + WSA.LogData -> + WSA.SolverAdapter st -> + CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) -> + (W4R.SatResult (WE.GroundEvalFn t, Maybe (WE.ExprRangeBindings t)) () -> IO r) -> + IO r +proveProofGoal sym ld adapter (CB.ProofGoal asms goal) = + proveGoal sym ld adapter asms goal From 7d42be42154dda2c9f76cd11350338dc758c8692 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 18 Jun 2024 14:51:07 -0400 Subject: [PATCH 3/9] Dedicated result type for goal-proving helpers --- crucible/src/Lang/Crucible/Backend/Prove.hs | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs index e1c9f8470..f9003a5a8 100644 --- a/crucible/src/Lang/Crucible/Backend/Prove.hs +++ b/crucible/src/Lang/Crucible/Backend/Prove.hs @@ -5,9 +5,10 @@ Copyright : (c) Galois, Inc 2024 License : BSD3 -} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeOperators #-} module Lang.Crucible.Backend.Prove @@ -25,6 +26,11 @@ import qualified What4.SatResult as W4R import qualified Lang.Crucible.Backend as CB import Lang.Crucible.Backend.Assumptions (Assumptions) +data ProofResult sym t + = Proved + | Disproved (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t)) + | Unknown + proveGoal :: (sym ~ WE.ExprBuilder t st fs) => W4.IsSymExprBuilder sym => @@ -33,13 +39,18 @@ proveGoal :: WSA.SolverAdapter st -> Assumptions sym -> CB.Assertion sym -> - (W4R.SatResult (WE.GroundEvalFn t, Maybe (WE.ExprRangeBindings t)) () -> IO r) -> + (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 + WSA.solver_adapter_check_sat adapter sym ld [asmsPred, notGoal] $ + k . + \case + W4R.Sat (gfn, binds) -> Disproved gfn binds + W4R.Unsat () -> Proved + W4R.Unknown -> Unknown proveProofGoal :: (sym ~ WE.ExprBuilder t st fs) => @@ -48,7 +59,7 @@ proveProofGoal :: WSA.LogData -> WSA.SolverAdapter st -> CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) -> - (W4R.SatResult (WE.GroundEvalFn t, Maybe (WE.ExprRangeBindings t)) () -> IO r) -> + (ProofResult sym t -> IO r) -> IO r proveProofGoal sym ld adapter (CB.ProofGoal asms goal) = proveGoal sym ld adapter asms goal From 856dbe60afcf7d70ba958d7e351d953f44e7634f Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 18 Jun 2024 15:20:58 -0400 Subject: [PATCH 4/9] Additional helpers for proving goals and obligations --- crucible/src/Lang/Crucible/Backend/Prove.hs | 65 ++++++++++++++++++--- 1 file changed, 56 insertions(+), 9 deletions(-) diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs index f9003a5a8..0a1fa9b3b 100644 --- a/crucible/src/Lang/Crucible/Backend/Prove.hs +++ b/crucible/src/Lang/Crucible/Backend/Prove.hs @@ -7,16 +7,19 @@ License : BSD3 {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} module Lang.Crucible.Backend.Prove - ( proveGoal + ( 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 @@ -25,11 +28,14 @@ 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) + +type Goal sym = CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) data ProofResult sym t - = Proved - | Disproved (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t)) - | Unknown + = Proved (Goal sym) + | Disproved (Goal sym) (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t)) + | Unknown (Goal sym) proveGoal :: (sym ~ WE.ExprBuilder t st fs) => @@ -45,12 +51,13 @@ proveGoal sym ld adapter asms goal k = do let goalPred = goal ^. CB.labeledPred asmsPred <- CB.assumptionsPred sym asms notGoal <- W4.notPred sym goalPred + let goal' = CB.ProofGoal asms goal WSA.solver_adapter_check_sat adapter sym ld [asmsPred, notGoal] $ k . \case - W4R.Sat (gfn, binds) -> Disproved gfn binds - W4R.Unsat () -> Proved - W4R.Unknown -> Unknown + W4R.Sat (gfn, binds) -> Disproved goal' gfn binds + W4R.Unsat () -> Proved goal' + W4R.Unknown -> Unknown goal' proveProofGoal :: (sym ~ WE.ExprBuilder t st fs) => @@ -63,3 +70,43 @@ proveProofGoal :: IO r proveProofGoal sym ld adapter (CB.ProofGoal asms goal) = proveGoal sym ld adapter asms goal + +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) -> + (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 + +proveObligations :: + (Monoid m, sym ~ WE.ExprBuilder t st fs) => + sym -> + WSA.LogData -> + WSA.SolverAdapter st -> + CB.ProofObligations 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 + +proveCurrentObligations :: + (Monoid m, CB.IsSymBackend sym bak, sym ~ WE.ExprBuilder t st fs) => + bak -> + WSA.LogData -> + WSA.SolverAdapter st -> + (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 From 1e281dff4901ff68e98b6b00d15b1ad3bfca040d Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 18 Jun 2024 15:28:48 -0400 Subject: [PATCH 5/9] Use goal-proving helpers in crucible-symio test suite --- crucible-symio/tests/TestMain.hs | 27 ++++++++------------------- crucible/crucible.cabal | 2 +- 2 files changed, 9 insertions(+), 20 deletions(-) diff --git a/crucible-symio/tests/TestMain.hs b/crucible-symio/tests/TestMain.hs index d2070f8c2..50e9e7503 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 @@ -133,26 +134,14 @@ 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 $ + \case + CB.Proved {} -> return () + CB.Unknown {} -> T.assertFailure "Inconclusive" + CB.Disproved (CB.ProofGoal asms goal) _ _ -> do + 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 c1c8ec833..c778eca6b 100644 --- a/crucible/crucible.cabal +++ b/crucible/crucible.cabal @@ -74,7 +74,6 @@ library other-modules: Lang.Crucible.Backend.Assumptions - Lang.Crucible.Backend.Prove exposed-modules: Lang.Crucible.Analysis.DFS @@ -87,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 From b37a9fa3323bb58164f2b6a37d2b10aaecbef1ea Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 18 Jun 2024 15:50:31 -0400 Subject: [PATCH 6/9] Haddocks for goal-proving helpers --- crucible/src/Lang/Crucible/Backend/Prove.hs | 25 ++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs index 0a1fa9b3b..d0b20395f 100644 --- a/crucible/src/Lang/Crucible/Backend/Prove.hs +++ b/crucible/src/Lang/Crucible/Backend/Prove.hs @@ -32,11 +32,24 @@ import Lang.Crucible.Backend.ProofGoals (traverseGoalsWithAssumptions) type Goal sym = CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) +-- | 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 - = Proved (Goal sym) + = -- | The goal was proved + -- + -- Corresponds to 'W4R.Unsat'. + Proved (Goal sym) + -- | The goal was disproved, and a model that falsifies it is available. + -- + -- Corresponds to 'W4R.Sat'. | Disproved (Goal sym) (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t)) + -- | The SMT solver returned \"unknown\". + -- + -- Corresponds to 'W4R.Unknown'. | Unknown (Goal sym) +-- | Prove a single goal. proveGoal :: (sym ~ WE.ExprBuilder t st fs) => W4.IsSymExprBuilder sym => @@ -45,6 +58,7 @@ proveGoal :: WSA.SolverAdapter st -> Assumptions sym -> CB.Assertion sym -> + -- | Continuation to process the 'ProofResult'. (ProofResult sym t -> IO r) -> IO r proveGoal sym ld adapter asms goal k = do @@ -59,6 +73,7 @@ proveGoal sym ld adapter asms goal k = do W4R.Unsat () -> Proved goal' W4R.Unknown -> Unknown goal' +-- | Prove a single 'CB.ProofGoal'. proveProofGoal :: (sym ~ WE.ExprBuilder t st fs) => W4.IsSymExprBuilder sym => @@ -66,11 +81,13 @@ proveProofGoal :: WSA.LogData -> WSA.SolverAdapter st -> CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) -> + -- | Continuation to process the 'ProofResult'. (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 => @@ -78,6 +95,7 @@ proveGoals :: WSA.LogData -> WSA.SolverAdapter st -> CB.Goals (CB.Assumptions sym) (CB.Assertion sym) -> + -- | Continuation to process the 'ProofResult'. (ProofResult sym t -> IO m) -> IO m proveGoals sym ld adapter goals k = @@ -86,12 +104,14 @@ proveGoals sym ld adapter goals k = (\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 the 'ProofResult'. (ProofResult sym t -> IO m) -> IO m proveObligations sym ld adapter obligations k = @@ -99,11 +119,14 @@ proveObligations sym ld adapter obligations k = 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 the 'ProofResult'. (ProofResult sym t -> IO m) -> IO m proveCurrentObligations bak ld adapter k = do From 672f0a0f4132974d4899797d17d9396d3410c104 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 20 Jun 2024 09:17:54 -0400 Subject: [PATCH 7/9] crucible-cli: Use new goal-proving helpers --- crucible-cli/src/Lang/Crucible/CLI.hs | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs index 4038a3928..31a5724d2 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(..), proveProofGoal) 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 @@ -184,14 +184,11 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks = 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" - ) + proveProofGoal sym defaultLogData z3Adapter g $ + \case + Proved {} -> hPutStrLn outh "PROVED" + Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE" + Unknown {} -> hPutStrLn outh "UNKNOWN" ) _ -> hPutStrLn outh "No suitable main function found" From ee97a5deb895019046becd34818cd4d0780c63e7 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 20 Jun 2024 09:29:02 -0400 Subject: [PATCH 8/9] Refactoring of goal-proving helpers, more use in crucible-cli --- crucible-cli/src/Lang/Crucible/CLI.hs | 19 ++++++------- .../override-nondet-test-both.out.good | 8 +++--- .../simulate/override-test2.out.good | 4 +-- crucible-symio/tests/TestMain.hs | 6 ++--- crucible/src/Lang/Crucible/Backend/Prove.hs | 27 +++++++++---------- 5 files changed, 29 insertions(+), 35 deletions(-) diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs index 31a5724d2..744ea359d 100644 --- a/crucible-cli/src/Lang/Crucible/CLI.hs +++ b/crucible-cli/src/Lang/Crucible/CLI.hs @@ -49,7 +49,7 @@ import Lang.Crucible.Syntax.SExpr import Lang.Crucible.Analysis.Postdom import Lang.Crucible.Backend -import Lang.Crucible.Backend.Prove (ProofResult(..), proveProofGoal) +import Lang.Crucible.Backend.Prove (ProofResult(..), proveCurrentObligations) import Lang.Crucible.Backend.Simple import Lang.Crucible.FunctionHandle import Lang.Crucible.Simulator @@ -180,16 +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 - proveProofGoal sym defaultLogData z3Adapter g $ - \case - Proved {} -> hPutStrLn outh "PROVED" - Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE" - 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 50e9e7503..24fc89b6a 100644 --- a/crucible-symio/tests/TestMain.hs +++ b/crucible-symio/tests/TestMain.hs @@ -57,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 @@ -135,11 +134,12 @@ runFSTest' bak (FSTest fsTest) = do putStrLn $ showF p T.assertFailure "Partial Result" - CB.proveCurrentObligations bak WSA.defaultLogData W4Y.yicesAdapter $ + CB.proveCurrentObligations bak WSA.defaultLogData W4Y.yicesAdapter $ \obligation -> \case CB.Proved {} -> return () CB.Unknown {} -> T.assertFailure "Inconclusive" - CB.Disproved (CB.ProofGoal asms goal) _ _ -> do + CB.Disproved _ _ -> do + CB.ProofGoal asms goal <- pure obligation asmsPred <- CB.assumptionsPred sym asms let goalPred = goal ^. CB.labeledPred putStrLn (showF asmsPred) diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs index d0b20395f..c74cb7d8b 100644 --- a/crucible/src/Lang/Crucible/Backend/Prove.hs +++ b/crucible/src/Lang/Crucible/Backend/Prove.hs @@ -30,8 +30,6 @@ import qualified Lang.Crucible.Backend as CB import Lang.Crucible.Backend.Assumptions (Assumptions) import Lang.Crucible.Backend.ProofGoals (traverseGoalsWithAssumptions) -type Goal sym = CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) - -- | The result of attempting to prove a goal with an SMT solver. -- -- The constructors of this type correspond to those of 'W4R.SatResult'. @@ -39,15 +37,15 @@ data ProofResult sym t = -- | The goal was proved -- -- Corresponds to 'W4R.Unsat'. - Proved (Goal sym) + Proved -- | The goal was disproved, and a model that falsifies it is available. -- -- Corresponds to 'W4R.Sat'. - | Disproved (Goal sym) (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t)) + | Disproved (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t)) -- | The SMT solver returned \"unknown\". -- -- Corresponds to 'W4R.Unknown'. - | Unknown (Goal sym) + | Unknown -- | Prove a single goal. proveGoal :: @@ -59,19 +57,18 @@ proveGoal :: Assumptions sym -> CB.Assertion sym -> -- | Continuation to process the 'ProofResult'. - (ProofResult sym t -> IO r) -> + (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 - let goal' = CB.ProofGoal asms goal WSA.solver_adapter_check_sat adapter sym ld [asmsPred, notGoal] $ - k . + k (CB.ProofGoal asms goal) . \case - W4R.Sat (gfn, binds) -> Disproved goal' gfn binds - W4R.Unsat () -> Proved goal' - W4R.Unknown -> Unknown goal' + W4R.Sat (gfn, binds) -> Disproved gfn binds + W4R.Unsat () -> Proved + W4R.Unknown -> Unknown -- | Prove a single 'CB.ProofGoal'. proveProofGoal :: @@ -82,7 +79,7 @@ proveProofGoal :: WSA.SolverAdapter st -> CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) -> -- | Continuation to process the 'ProofResult'. - (ProofResult sym t -> IO r) -> + (CB.ProofObligation sym -> ProofResult sym t -> IO r) -> IO r proveProofGoal sym ld adapter (CB.ProofGoal asms goal) = proveGoal sym ld adapter asms goal @@ -96,7 +93,7 @@ proveGoals :: WSA.SolverAdapter st -> CB.Goals (CB.Assumptions sym) (CB.Assertion sym) -> -- | Continuation to process the 'ProofResult'. - (ProofResult sym t -> IO m) -> + (CB.ProofObligation sym -> ProofResult sym t -> IO m) -> IO m proveGoals sym ld adapter goals k = getConst $ @@ -112,7 +109,7 @@ proveObligations :: WSA.SolverAdapter st -> CB.ProofObligations sym -> -- | Continuation to process the 'ProofResult'. - (ProofResult sym t -> IO m) -> + (CB.ProofObligation sym -> ProofResult sym t -> IO m) -> IO m proveObligations sym ld adapter obligations k = case obligations of @@ -127,7 +124,7 @@ proveCurrentObligations :: WSA.LogData -> WSA.SolverAdapter st -> -- | Continuation to process the 'ProofResult'. - (ProofResult sym t -> IO m) -> + (CB.ProofObligation sym -> ProofResult sym t -> IO m) -> IO m proveCurrentObligations bak ld adapter k = do obligations <- CB.getProofObligations bak From 3b3ae5567d8398b5bc3eb243ca6dcd2a34822483 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 20 Jun 2024 10:57:37 -0400 Subject: [PATCH 9/9] Haddocks for goal-proving helpers --- .../src/Lang/Crucible/Backend/ProofGoals.hs | 1 - crucible/src/Lang/Crucible/Backend/Prove.hs | 27 +++++++++++++++---- 2 files changed, 22 insertions(+), 6 deletions(-) diff --git a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs index 3e0b86cc2..38ea32b42 100644 --- a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs @@ -18,7 +18,6 @@ module Lang.Crucible.Backend.ProofGoals , traverseGoals, traverseOnlyGoals , traverseGoalsWithAssumptions , traverseGoalsSeq - -- ** Proving goals -- * Goal collector , FrameIdentifier(..), GoalCollector diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs index c74cb7d8b..01c14e85b 100644 --- a/crucible/src/Lang/Crucible/Backend/Prove.hs +++ b/crucible/src/Lang/Crucible/Backend/Prove.hs @@ -34,7 +34,7 @@ import Lang.Crucible.Backend.ProofGoals (traverseGoalsWithAssumptions) -- -- The constructors of this type correspond to those of 'W4R.SatResult'. data ProofResult sym t - = -- | The goal was proved + = -- | The goal was proved. -- -- Corresponds to 'W4R.Unsat'. Proved @@ -47,7 +47,24 @@ data ProofResult sym t -- Corresponds to 'W4R.Unknown'. | Unknown --- | Prove a single goal. +-- | 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 => @@ -92,7 +109,7 @@ proveGoals :: WSA.LogData -> WSA.SolverAdapter st -> CB.Goals (CB.Assumptions sym) (CB.Assertion sym) -> - -- | Continuation to process the 'ProofResult'. + -- | Continuation to process each 'ProofResult'. (CB.ProofObligation sym -> ProofResult sym t -> IO m) -> IO m proveGoals sym ld adapter goals k = @@ -108,7 +125,7 @@ proveObligations :: WSA.LogData -> WSA.SolverAdapter st -> CB.ProofObligations sym -> - -- | Continuation to process the 'ProofResult'. + -- | Continuation to process each 'ProofResult'. (CB.ProofObligation sym -> ProofResult sym t -> IO m) -> IO m proveObligations sym ld adapter obligations k = @@ -123,7 +140,7 @@ proveCurrentObligations :: bak -> WSA.LogData -> WSA.SolverAdapter st -> - -- | Continuation to process the 'ProofResult'. + -- | Continuation to process each 'ProofResult'. (CB.ProofObligation sym -> ProofResult sym t -> IO m) -> IO m proveCurrentObligations bak ld adapter k = do