diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,22 @@ +# 0.9 -- 2026-01-29 + +# 0.8.0 -- 2025-11-09 + +* Add `setExecResultContext`, `setExecStateContext` +* Add `Lang.Crucible.Simulator.RecordAndReplay`, a module with two new execution + features for recording and replaying control-flow traces. +* Add a `GlobalPair` argument to `AbortedExit`. +* Add new helpers for extracting `SymGlobalState`s: `exec{Result,State}Globals`. +* Add `typedOverride` for constructing `TypedOverride`s with statically-known + signatures. +* Add `bindTypedOverride` for binding `TypedOverride`s to `FnHandle`s. +* Add `FunctorF`, `FoldableF`, and `TraversableF` instances for `CrucibleEvent`, + `CrucibleAssumption`, and `CrucibleAssumptions`. +* Add `gcAddTopLevelAssume`, for making top-level assumptions. +* Rename functions in `Lang.Crucible.Concretize` to match What4's conventions. + In particular, rename `concRegValue` to `groundRegValue`, `concRegEntry` to + `groundRegEntry`, and `concRegMap` to `groundRegMap`. + # 0.7.2 -- 2025-03-21 * Add support for Bitwuzla as an online SMT solver backend. diff --git a/crucible.cabal b/crucible.cabal --- a/crucible.cabal +++ b/crucible.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: crucible -Version: 0.7.2 +Version: 0.9 Author: Galois Inc. Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com Copyright: (c) Galois, Inc 2014-2022 @@ -14,6 +14,9 @@ (SSA) form control flow graphs, and a symbolic simulation engine for executing programs expressed in this format. It also provides support for communicating with a variety of SAT and SMT solvers, including Z3, CVC4, Yices, STP, and dReal. + . + For an overview of Crucible please have a look at "Lang.Crucible.README" + extra-doc-files: CHANGELOG.md source-repository head @@ -45,7 +48,7 @@ import: bldflags build-depends: async, - base >= 4.13 && < 4.20, + base >= 4.13 && < 4.21, bimap, bv-sized >= 1.0.0 && < 1.1, containers >= 0.5.9.0, @@ -101,6 +104,7 @@ Lang.Crucible.CFG.SSAConversion Lang.Crucible.CFG.EarlyMergeLoops Lang.Crucible.FunctionHandle + Lang.Crucible.README Lang.Crucible.Simulator Lang.Crucible.Simulator.Breakpoint Lang.Crucible.Simulator.BoundedExec @@ -117,6 +121,7 @@ Lang.Crucible.Simulator.PathSplitting Lang.Crucible.Simulator.PositionTracking Lang.Crucible.Simulator.Profiling + Lang.Crucible.Simulator.RecordAndReplay Lang.Crucible.Simulator.RegMap Lang.Crucible.Simulator.RegValue Lang.Crucible.Simulator.SimError @@ -163,15 +168,18 @@ import: bldflags type: exitcode-stdio-1.0 hs-source-dirs: test/helpers --- other-modules: + other-modules: + SymSequence main-is: Main.hs build-depends: base, hspec >= 2.5, crucible, + hedgehog, lens, panic >= 0.3, parameterized-utils, tasty >= 0.10, tasty-hspec >= 1.1, + tasty-hedgehog >= 1.2, tasty-hunit, what4 diff --git a/src/Lang/Crucible/Backend.hs b/src/Lang/Crucible/Backend.hs --- a/src/Lang/Crucible/Backend.hs +++ b/src/Lang/Crucible/Backend.hs @@ -4,8 +4,8 @@ License : BSD3 Maintainer : Joe Hendrix -This module provides an interface that symbolic backends must provide -for interacting with the symbolic simulator. +This module provides the interface that the symbolic simulator uses when +interacting with symbolic backends (i.e., SMT solvers). Compared to the solver connections provided by What4, Crucible backends provide a facility for managing an /assumption stack/ (see 'AS.AssumptionStack'). Note @@ -81,6 +81,7 @@ , ppProofObligation , backendOptions , assertThenAssumeConfigOption + , ppAssumptionState ) where import Control.Exception(Exception(..), throwIO) @@ -110,6 +111,7 @@ import qualified Lang.Crucible.Backend.AssumptionStack as AS import qualified Lang.Crucible.Backend.ProofGoals as PG import Lang.Crucible.Simulator.SimError +import Lang.Crucible.Backend.ProofGoals (ppGoalCollector) type Assertion sym = LabeledPred (Pred sym) SimError type ProofObligation sym = AS.ProofGoal (Assumptions sym) (Assertion sym) @@ -311,6 +313,11 @@ resetAssumptionState :: bak -> IO () resetAssumptionState bak = restoreAssumptionState bak PG.emptyGoalCollector + -- | Get the state of the backend + -- + -- In contrast to 'saveAssumptionState', this also includes the goals. + getBackendState :: bak -> IO (AssumptionState sym) + assertThenAssumeConfigOption :: ConfigOption BaseBoolType assertThenAssumeConfigOption = configOption knownRepr "assertThenAssume" @@ -490,3 +497,21 @@ ppGl = PP.indent 2 $ PP.vsep [ppSimError (gl^.labeledPredMsg), printSymExpr (gl^.labeledPred)] + +-- | Pretty-printer for 'AssumptionState'. +ppAssumptionState :: + IsExpr (SymExpr sym) => + proxy sym -> + AssumptionState sym -> + PP.Doc ann +ppAssumptionState _proxy = ppGoalCollector ppAssumptions ppPred + where + ppPred (LabeledPred p simErr) = + PP.vcat + [ "Labeled predicate:" + , PP.indent 2 $ + PP.vcat + [ printSymExpr p + , ppSimError simErr + ] + ] diff --git a/src/Lang/Crucible/Backend/AssumptionStack.hs b/src/Lang/Crucible/Backend/AssumptionStack.hs --- a/src/Lang/Crucible/Backend/AssumptionStack.hs +++ b/src/Lang/Crucible/Backend/AssumptionStack.hs @@ -4,17 +4,16 @@ License : BSD3 Maintainer : Rob Dockins -This module provides management support for keeping track -of a context of logical assumptions. The API provided here -is similar to the interactive mode of an SMT solver. Logical -conditions can be assumed into the current context, and bundles -of assumptions are organized into frames which are pushed and -popped by the user to manage the state. +This module provides management support for keeping track of a context of +logical assumptions and proof obligations that arise from symbolic simulation. +The API provided here is similar to the interactive mode of an SMT solver. +Logical conditions can be assumed into the current context, and conjunctions +of assumptions are organized into frames which are pushed and popped by the +simulator to manage the state. -Additionally, proof goals can be asserted to the system. These will be -turned into complete logical statements by assuming the current context -and be stashed in a collection of remembered goals for later dispatch to -solvers. +Additionally, proof goals can be asserted to the system. These will be turned +into complete logical statements by assuming the current context and will be +stashed in a collection of remembered goals for later dispatch to SMT solvers. -} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} @@ -70,11 +69,13 @@ , assumeFrameCond :: asmp } --- | An assumption stack is a data structure for tracking --- logical assumptions and proof obligations. Assumptions --- can be added to the current stack frame, and stack frames --- may be pushed (to remember a previous state) or popped --- to restore a previous state. +-- | An assumption stack is a data structure for tracking logical assumptions +-- and proof obligations that arise from symbolic simulation. Assumptions +-- can be added to the current stack frame, and stack frames may be pushed (to +-- remember a previous state) or popped (to restore a previous state). +-- +-- The main use of 'AssumptionStack' is as the state of the simple or online +-- backends. data AssumptionStack asmp ast = AssumptionStack { assumeStackGen :: IO FrameIdentifier diff --git a/src/Lang/Crucible/Backend/Assumptions.hs b/src/Lang/Crucible/Backend/Assumptions.hs --- a/src/Lang/Crucible/Backend/Assumptions.hs +++ b/src/Lang/Crucible/Backend/Assumptions.hs @@ -41,13 +41,17 @@ , assumptionsPred , flattenAssumptions , assumptionsTopLevelLocs + , ppAssumptions' + , ppAssumptions ) where import Control.Lens (Traversal, folded) import Data.Kind (Type) +import qualified Data.Foldable as F import Data.Functor.Identity import Data.Functor.Const +import qualified Data.Parameterized.TraversableF as TF import qualified Data.Sequence as Seq import Data.Sequence (Seq) import qualified Prettyprinter as PP @@ -76,6 +80,13 @@ -- ^ An assumption justified by a proof of the impossibility of -- a certain simulator error. +instance TF.FunctorF CrucibleAssumption where + fmapF = TF.fmapFDefault +instance TF.FoldableF CrucibleAssumption where + foldMapF = TF.foldMapFDefault +instance TF.TraversableF CrucibleAssumption where + traverseF = traverseAssumption + -- | 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. @@ -91,13 +102,24 @@ ProgramLoc -> CrucibleEvent e +instance TF.FunctorF CrucibleEvent where + fmapF = TF.fmapFDefault +instance TF.FoldableF CrucibleEvent where + foldMapF = TF.foldMapFDefault +instance TF.TraversableF CrucibleEvent where + traverseF = traverseEvent + -- | 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) = +ppEvent' :: (forall t. e t -> PP.Doc ann) -> CrucibleEvent e -> PP.Doc ann +ppEvent' ppExp (CreateVariableEvent loc nm _tpr v) = + "create var" PP.<+> PP.pretty nm PP.<+> "=" PP.<+> ppExp v PP.<+> "at" PP.<+> PP.pretty (plSourceLoc loc) +ppEvent' _ppExp (LocationReachedEvent loc) = "reached" PP.<+> PP.pretty (plSourceLoc loc) PP.<+> "in" PP.<+> PP.pretty (plFunction loc) +-- | Pretty print an event +ppEvent :: IsExpr e => CrucibleEvent e -> PP.Doc ann +ppEvent = ppEvent' printSymExpr + -- | Return the program location associated with an event eventLoc :: CrucibleEvent e -> ProgramLoc eventLoc (CreateVariableEvent loc _ _ _) = loc @@ -152,6 +174,21 @@ instance Monoid (CrucibleAssumptions e) where mempty = ManyAssumptions mempty +instance TF.FunctorF CrucibleAssumptions where + fmapF = TF.fmapFDefault +instance TF.FoldableF CrucibleAssumptions where + foldMapF = TF.foldMapFDefault +instance TF.TraversableF CrucibleAssumptions where + traverseF f = \case + SingleAssumption a -> + SingleAssumption <$> TF.traverseF f a + SingleEvent e -> + SingleEvent <$> TF.traverseF f e + ManyAssumptions xs -> + ManyAssumptions <$> traverse (TF.traverseF f) xs + MergeAssumptions c xs ys -> + MergeAssumptions <$> f c <*> TF.traverseF f xs <*> TF.traverseF f ys + singleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e singleAssumption x = SingleAssumption x @@ -239,6 +276,8 @@ ppAssumption :: (forall tp. e tp -> PP.Doc ann) -> CrucibleAssumption e -> PP.Doc ann ppAssumption ppDoc e = + -- TODO(lb): These should really all be `align`ed, but that breaks a bunch + -- of tests. case e of GenericAssumption l msg p -> PP.vsep [ ppLocated l (PP.pretty msg) @@ -266,3 +305,27 @@ ppLoc :: ProgramLoc -> PP.Doc ann ppLoc l = PP.pretty (plSourceLoc l) + +-- | Pretty-print 'CrucibleAssumptions'. +ppAssumptions' :: + -- | How to print expressions. If @'IsExpr' e@ holds, then see 'ppAssumptions' + -- for a version that uses 'printSymExpr'. + (forall tp. e tp -> PP.Doc ann) -> + CrucibleAssumptions e -> + PP.Doc ann +ppAssumptions' ppExp = + \case + SingleAssumption asmp -> ppAssumption ppExp asmp + SingleEvent e -> ppEvent' ppExp e + ManyAssumptions asmps -> PP.list (map (ppAssumptions' ppExp) (F.toList asmps)) + MergeAssumptions b thn els -> + PP.align $ + PP.vcat + [ "if " <> PP.align (ppExp b) + , "then " <> PP.align (ppAssumptions' ppExp thn) + , "else " <> PP.align (ppAssumptions' ppExp els) + ] + +-- | @'ppAssumptions' = `ppAssumptions'` 'printSymExpr'@ +ppAssumptions :: IsExpr e => CrucibleAssumptions e -> PP.Doc ann +ppAssumptions = ppAssumptions' printSymExpr diff --git a/src/Lang/Crucible/Backend/Goals.hs b/src/Lang/Crucible/Backend/Goals.hs --- a/src/Lang/Crucible/Backend/Goals.hs +++ b/src/Lang/Crucible/Backend/Goals.hs @@ -7,12 +7,14 @@ proof obligations, and the current state of assumptions. -} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TupleSections #-} module Lang.Crucible.Backend.Goals ( ProofGoal(..) , Goals(..) + , ppGoals , goalsToList , assuming , proveAll @@ -29,6 +31,7 @@ import Data.Functor.Const (Const(..)) import Data.Sequence (Seq) import qualified Data.Sequence as Seq +import qualified Prettyprinter as PP -- | A proof goal consists of a collection of assumptions -- that were in scope when an assertion was made, together @@ -52,6 +55,35 @@ -- | A conjunction of two goals. | ProveConj !(Goals asmp goal) !(Goals asmp goal) deriving Show + +-- | Intended for debugging, this is not generally a user-facing datatype. +ppGoals :: + (asmp -> PP.Doc ann) -> + (goal -> PP.Doc ann) -> + Goals asmp goal -> + PP.Doc ann +ppGoals ppAsmp ppGoal = + \case + Assuming asmp gls -> + PP.align $ + PP.vcat + [ PP.pretty "Assuming:" + , PP.indent 2 (ppAsmp asmp) + , PP.pretty "Prove:" + , PP.indent 2 (ppGoals ppAsmp ppGoal gls) + ] + Prove gl -> ppGoal gl + ProveConj gls gls' -> + PP.align $ + PP.vcat + [ PP.pretty "Prove both:" + , PP.indent 2 (ppGoals ppAsmp ppGoal gls) + , PP.indent 2 (ppGoals ppAsmp ppGoal gls') + ] + +-- | Intended for debugging, this is not generally a user-facing datatype. +instance (PP.Pretty asmp, PP.Pretty goal) => PP.Pretty (Goals asmp goal) where + pretty = ppGoals PP.pretty PP.pretty -- | Construct a goal that first assumes a collection of -- assumptions and then states a goal. diff --git a/src/Lang/Crucible/Backend/Online.hs b/src/Lang/Crucible/Backend/Online.hs --- a/src/Lang/Crucible/Backend/Online.hs +++ b/src/Lang/Crucible/Backend/Online.hs @@ -4,19 +4,26 @@ -- Description : A solver backend that maintains a persistent connection -- Copyright : (c) Galois, Inc 2015-2016 -- License : BSD3 --- Maintainer : Joe Hendrix +-- Maintainer : Ryan Scott , Langston Barrett -- Stability : provisional -- --- The online backend maintains an open connection to an SMT solver --- that is used to prune unsatisfiable execution traces during simulation. --- At every symbolic branch point, the SMT solver is queried to determine --- if one or both symbolic branches are unsatisfiable. --- Only branches with satisfiable branch conditions are explored. +-- A solver backend ('IsSymBackend') that maintains an open connection to an +-- SMT solver (in contrast to "Lang.Crucible.Backend.Simple"). -- --- The online backend also allows override definitions access to a --- persistent SMT solver connection. This can be useful for some --- kinds of algorithms that benefit from quickly performing many --- small solver queries in a tight interaction loop. +-- The primary intended use-case is to prune unsatisfiable execution +-- traces during simulation using the execution feature provided by +-- "Lang.Crucible.Simulator.PathSatisfiability". That execution feature is +-- parameterized over a function argument that can be instantiated with this +-- module's 'considerSatisfiability'. +-- +-- The online backend also allows override definitions access to a persistent +-- SMT solver connection. This can be useful for some kinds of algorithms +-- that benefit from quickly performing many small solver queries in a tight +-- interaction loop. +-- +-- The online backend is not currently used to dispatch proof obligations during +-- symbolic execution, see [GaloisInc/crucible#369, \"Interleave proof with +-- simulation\"](https://github.com/GaloisInc/crucible/issues/369). ------------------------------------------------------------------------ {-# LANGUAGE DeriveDataTypeable #-} @@ -27,9 +34,14 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} + module Lang.Crucible.Backend.Online - ( -- * OnlineBackend - OnlineBackend + ( -- * Configuration options + solverInteractionFile + , enableOnlineBackend + , onlineBackendOptions + -- * OnlineBackend + , OnlineBackend , withOnlineBackend , newOnlineBackend , checkSatisfiable @@ -39,13 +51,10 @@ , restoreSolverState , UnsatFeatures(..) , unsatFeaturesToProblemFeatures - -- ** Configuration options - , solverInteractionFile - , enableOnlineBackend - , onlineBackendOptions - -- ** Branch satisfiability + -- * Branch satisfiability , BranchResult(..) , considerSatisfiability + -- * Backends for different solvers -- ** Yices , YicesOnlineBackend , withYicesOnlineBackend @@ -69,7 +78,6 @@ , withSTPOnlineBackend ) where - import Control.Lens ( (^.) ) import Control.Monad import Control.Monad.Fix (mfix) @@ -104,10 +112,13 @@ import qualified What4.Solver.Z3 as Z3 import Lang.Crucible.Backend -import Lang.Crucible.Backend.AssumptionStack as AS +import qualified Lang.Crucible.Backend.AssumptionStack as AS import qualified Lang.Crucible.Backend.ProofGoals as PG import Lang.Crucible.Simulator.SimError +-------------------------------------------------------------------------------- +-- Configuration options + data UnsatFeatures = NoUnsatFeatures -- ^ Do not compute unsat cores or assumptions @@ -181,7 +192,7 @@ ProblemFeatures -> IO (OnlineBackend solver scope st fs) newOnlineBackend sym feats = - do stk <- initAssumptionStack (sym ^. B.exprCounter) + do stk <- AS.initAssumptionStack (sym ^. B.exprCounter) procref <- newIORef SolverNotStarted featref <- newIORef feats @@ -224,176 +235,6 @@ ) -type YicesOnlineBackend scope st fs = OnlineBackend Yices.Connection scope st fs - --- | Do something with a Yices online backend. --- The backend is only valid in the continuation. --- --- The Yices configuration options will be automatically --- installed into the backend configuration object. --- --- n.b. the explicit forall allows the fs to be expressed as the --- first argument so that it can be dictated easily from the caller. --- Example: --- --- > withYicesOnlineBackend FloatRealRepr ng f' -withYicesOnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - UnsatFeatures -> - ProblemFeatures -> - (YicesOnlineBackend scope st fs -> m a) -> - m a -withYicesOnlineBackend sym unsatFeat extraFeatures action = - let feat = Yices.yicesDefaultFeatures .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures in - withOnlineBackend sym feat $ \bak -> - do liftIO $ tryExtendConfig Yices.yicesOptions (getConfiguration sym) - action bak - -type Z3OnlineBackend scope st fs = OnlineBackend (SMT2.Writer Z3.Z3) scope st fs - --- | Do something with a Z3 online backend. --- The backend is only valid in the continuation. --- --- The Z3 configuration options will be automatically --- installed into the backend configuration object. --- --- n.b. the explicit forall allows the fs to be expressed as the --- first argument so that it can be dictated easily from the caller. --- Example: --- --- > withz3OnlineBackend FloatRealRepr ng f' -withZ3OnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - UnsatFeatures -> - ProblemFeatures -> - (Z3OnlineBackend scope st fs -> m a) -> - m a -withZ3OnlineBackend sym unsatFeat extraFeatures action = - let feat = (SMT2.defaultFeatures Z3.Z3 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in - withOnlineBackend sym feat $ \bak -> - do liftIO $ tryExtendConfig Z3.z3Options (getConfiguration sym) - action bak - -type BitwuzlaOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Bitwuzla.Bitwuzla) scope st fs - --- | Do something with a Bitwuzla online backend. --- The backend is only valid in the continuation. --- --- The Bitwuzla configuration options will be automatically --- installed into the backend configuration object. --- --- > withBitwuzlaOnineBackend FloatRealRepr ng f' -withBitwuzlaOnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - UnsatFeatures -> - ProblemFeatures -> - (BitwuzlaOnlineBackend scope st fs -> m a) -> - m a -withBitwuzlaOnlineBackend sym unsatFeat extraFeatures action = - let feat = (SMT2.defaultFeatures Bitwuzla.Bitwuzla .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in - withOnlineBackend sym feat $ \bak -> do - liftIO $ tryExtendConfig Bitwuzla.bitwuzlaOptions (getConfiguration sym) - action bak - -type BoolectorOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Boolector.Boolector) scope st fs - --- | Do something with a Boolector online backend. --- The backend is only valid in the continuation. --- --- The Boolector configuration options will be automatically --- installed into the backend configuration object. --- --- > withBoolectorOnineBackend FloatRealRepr ng f' -withBoolectorOnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - UnsatFeatures -> - (BoolectorOnlineBackend scope st fs -> m a) -> - m a -withBoolectorOnlineBackend sym unsatFeat action = - let feat = (SMT2.defaultFeatures Boolector.Boolector .|. unsatFeaturesToProblemFeatures unsatFeat) in - withOnlineBackend sym feat $ \bak -> do - liftIO $ tryExtendConfig Boolector.boolectorOptions (getConfiguration sym) - action bak - -type CVC4OnlineBackend scope st fs = OnlineBackend (SMT2.Writer CVC4.CVC4) scope st fs - --- | Do something with a CVC4 online backend. --- The backend is only valid in the continuation. --- --- The CVC4 configuration options will be automatically --- installed into the backend configuration object. --- --- n.b. the explicit forall allows the fs to be expressed as the --- first argument so that it can be dictated easily from the caller. --- Example: --- --- > withCVC4OnlineBackend FloatRealRepr ng f' -withCVC4OnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - UnsatFeatures -> - ProblemFeatures -> - (CVC4OnlineBackend scope st fs -> m a) -> - m a -withCVC4OnlineBackend sym unsatFeat extraFeatures action = - let feat = (SMT2.defaultFeatures CVC4.CVC4 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in - withOnlineBackend sym feat $ \bak -> do - liftIO $ tryExtendConfig CVC4.cvc4Options (getConfiguration sym) - action bak - -type CVC5OnlineBackend scope st fs = OnlineBackend (SMT2.Writer CVC5.CVC5) scope st fs - --- | Do something with a CVC5 online backend. --- The backend is only valid in the continuation. --- --- The CVC5 configuration options will be automatically --- installed into the backend configuration object. --- --- n.b. the explicit forall allows the fs to be expressed as the --- first argument so that it can be dictated easily from the caller. --- Example: --- --- > withCVC5OnlineBackend FloatRealRepr ng f' -withCVC5OnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - UnsatFeatures -> - ProblemFeatures -> - (CVC5OnlineBackend scope st fs -> m a) -> - m a -withCVC5OnlineBackend sym unsatFeat extraFeatures action = - let feat = (SMT2.defaultFeatures CVC5.CVC5 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in - withOnlineBackend sym feat $ \bak -> do - liftIO $ tryExtendConfig CVC5.cvc5Options (getConfiguration sym) - action bak - -type STPOnlineBackend scope st fs = OnlineBackend (SMT2.Writer STP.STP) scope st fs - --- | Do something with a STP online backend. --- The backend is only valid in the continuation. --- --- The STO configuration options will be automatically --- installed into the backend configuration object. --- --- n.b. the explicit forall allows the fs to be expressed as the --- first argument so that it can be dictated easily from the caller. --- Example: --- --- > withSTPOnlineBackend FloatRealRepr ng f' -withSTPOnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - (STPOnlineBackend scope st fs -> m a) -> - m a -withSTPOnlineBackend sym action = - withOnlineBackend sym (SMT2.defaultFeatures STP.STP) $ \bak -> do - liftIO $ tryExtendConfig STP.stpOptions (getConfiguration sym) - action bak - -- | Shutdown any currently-active solver process. -- A fresh solver process will be started on the -- next call to `getSolverProcess`. @@ -497,30 +338,13 @@ withSolverConn bak k = withSolverProcess bak (pure ()) (k . solverConn) --- | Result of attempting to branch on a predicate. -data BranchResult - -- | The both branches of the predicate might be satisfiable - -- (although satisfiablility of either branch is not guaranteed). - = IndeterminateBranchResult - - -- | Commit to the branch where the given predicate is equal to - -- the returned boolean. The opposite branch is unsatisfiable - -- (although the given branch is not necessarily satisfiable). - | NoBranch !Bool - - -- | The context before considering the given predicate was already - -- unsatisfiable. - | UnsatisfiableContext - deriving (Data, Eq, Generic, Ord, Typeable) - - restoreAssumptionFrames :: OnlineSolver solver => OnlineBackend solver scope st fs -> SolverProcess scope solver -> - AssumptionFrames (CrucibleAssumptions (B.Expr scope)) -> + AS.AssumptionFrames (CrucibleAssumptions (B.Expr scope)) -> IO () -restoreAssumptionFrames bak proc (AssumptionFrames base frms) = +restoreAssumptionFrames bak proc (AS.AssumptionFrames base frms) = do let sym = onlineExprBuilder bak -- assume the base-level assumptions SMT.assume (solverConn proc) =<< assumptionsPred sym base @@ -530,29 +354,6 @@ do push proc SMT.assume (solverConn proc) =<< assumptionsPred sym frm -considerSatisfiability :: - OnlineSolver solver => - OnlineBackend solver scope st fs -> - Maybe ProgramLoc -> - B.BoolExpr scope -> - IO BranchResult -considerSatisfiability bak mbPloc p = - let sym = onlineExprBuilder bak in - withSolverProcess bak (pure IndeterminateBranchResult) $ \proc -> - do pnot <- notPred sym p - let locDesc = case mbPloc of - Just ploc -> show (plSourceLoc ploc) - Nothing -> "(unknown location)" - let rsn = "branch sat: " ++ locDesc - p_res <- checkSatisfiable proc rsn p - pnot_res <- checkSatisfiable proc rsn pnot - case (p_res, pnot_res) of - (Unsat{}, Unsat{}) -> return UnsatisfiableContext - (_ , Unsat{}) -> return (NoBranch True) - (Unsat{}, _ ) -> return (NoBranch False) - _ -> return IndeterminateBranchResult - - instance HasSymInterface (B.ExprBuilder t st fs) (OnlineBackend solver t st fs) where backendGetSym = onlineExprBuilder @@ -587,7 +388,7 @@ withSolverConn bak $ \conn -> SMT.assume conn p -- Add assertions to list - appendAssumptions as (assumptionStack bak) + AS.appendAssumptions as (assumptionStack bak) collectAssumptions bak = AS.collectAssumptions (assumptionStack bak) @@ -596,11 +397,11 @@ -- NB, don't push a frame in the assumption stack unless -- pushing to the solver succeeded do withSolverProcess bak (pure ()) push - pushFrame (assumptionStack bak) + AS.pushFrame (assumptionStack bak) popAssumptionFrame bak ident = -- NB, pop the frame whether or not the solver pop succeeds - do frm <- popFrame ident (assumptionStack bak) + do frm <- AS.popFrame ident (assumptionStack bak) withSolverProcess bak (pure ()) pop return frm @@ -612,7 +413,7 @@ popAssumptionFrameAndObligations bak ident = do -- NB, pop the frames whether or not the solver pop succeeds - do frmAndGls <- popFrameAndGoals ident (assumptionStack bak) + do frmAndGls <- AS.popFrameAndGoals ident (assumptionStack bak) withSolverProcess bak (pure ()) pop return frmAndGls @@ -629,3 +430,185 @@ do restoreSolverState bak gc -- restore the previous assumption stack AS.restoreAssumptionStack gc (assumptionStack bak) + + getBackendState bak = readIORef (AS.proofObligations (assumptionStack bak)) + +-------------------------------------------------------------------------------- +-- Branch satisfiability + +-- | Result of attempting to branch on a predicate. +data BranchResult + -- | The both branches of the predicate might be satisfiable + -- (although satisfiablility of either branch is not guaranteed). + = IndeterminateBranchResult + + -- | Commit to the branch where the given predicate is equal to + -- the returned boolean. The opposite branch is unsatisfiable + -- (although the given branch is not necessarily satisfiable). + | NoBranch !Bool + + -- | The context before considering the given predicate was already + -- unsatisfiable. + | UnsatisfiableContext + deriving (Data, Eq, Generic, Ord, Typeable) + +considerSatisfiability :: + OnlineSolver solver => + OnlineBackend solver scope st fs -> + Maybe ProgramLoc -> + B.BoolExpr scope -> + IO BranchResult +considerSatisfiability bak mbPloc p = + let sym = onlineExprBuilder bak in + withSolverProcess bak (pure IndeterminateBranchResult) $ \proc -> + do pnot <- notPred sym p + let locDesc = case mbPloc of + Just ploc -> show (plSourceLoc ploc) + Nothing -> "(unknown location)" + let rsn = "branch sat: " ++ locDesc + p_res <- checkSatisfiable proc rsn p + pnot_res <- checkSatisfiable proc rsn pnot + case (p_res, pnot_res) of + (Unsat{}, Unsat{}) -> return UnsatisfiableContext + (_ , Unsat{}) -> return (NoBranch True) + (Unsat{}, _ ) -> return (NoBranch False) + _ -> return IndeterminateBranchResult + +-------------------------------------------------------------------------------- +-- Backends for different solvers + +type YicesOnlineBackend scope st fs = OnlineBackend Yices.Connection scope st fs + +-- | Do something with a Yices online backend. +-- The backend is only valid in the continuation. +-- +-- The Yices configuration options will be automatically +-- installed into the backend configuration object. +withYicesOnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + UnsatFeatures -> + ProblemFeatures -> + (YicesOnlineBackend scope st fs -> m a) -> + m a +withYicesOnlineBackend sym unsatFeat extraFeatures action = + let feat = Yices.yicesDefaultFeatures .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures in + withOnlineBackend sym feat $ \bak -> + do liftIO $ tryExtendConfig Yices.yicesOptions (getConfiguration sym) + action bak + +type Z3OnlineBackend scope st fs = OnlineBackend (SMT2.Writer Z3.Z3) scope st fs + +-- | Do something with a Z3 online backend. +-- The backend is only valid in the continuation. +-- +-- The Z3 configuration options will be automatically +-- installed into the backend configuration object. +withZ3OnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + UnsatFeatures -> + ProblemFeatures -> + (Z3OnlineBackend scope st fs -> m a) -> + m a +withZ3OnlineBackend sym unsatFeat extraFeatures action = + let feat = (SMT2.defaultFeatures Z3.Z3 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in + withOnlineBackend sym feat $ \bak -> + do liftIO $ tryExtendConfig Z3.z3Options (getConfiguration sym) + action bak + +type BitwuzlaOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Bitwuzla.Bitwuzla) scope st fs + +-- | Do something with a Bitwuzla online backend. +-- The backend is only valid in the continuation. +-- +-- The Bitwuzla configuration options will be automatically +-- installed into the backend configuration object. +withBitwuzlaOnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + UnsatFeatures -> + ProblemFeatures -> + (BitwuzlaOnlineBackend scope st fs -> m a) -> + m a +withBitwuzlaOnlineBackend sym unsatFeat extraFeatures action = + let feat = (SMT2.defaultFeatures Bitwuzla.Bitwuzla .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in + withOnlineBackend sym feat $ \bak -> do + liftIO $ tryExtendConfig Bitwuzla.bitwuzlaOptions (getConfiguration sym) + action bak + +type BoolectorOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Boolector.Boolector) scope st fs + +-- | Do something with a Boolector online backend. +-- The backend is only valid in the continuation. +-- +-- The Boolector configuration options will be automatically +-- installed into the backend configuration object. +withBoolectorOnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + UnsatFeatures -> + (BoolectorOnlineBackend scope st fs -> m a) -> + m a +withBoolectorOnlineBackend sym unsatFeat action = + let feat = (SMT2.defaultFeatures Boolector.Boolector .|. unsatFeaturesToProblemFeatures unsatFeat) in + withOnlineBackend sym feat $ \bak -> do + liftIO $ tryExtendConfig Boolector.boolectorOptions (getConfiguration sym) + action bak + +type CVC4OnlineBackend scope st fs = OnlineBackend (SMT2.Writer CVC4.CVC4) scope st fs + +-- | Do something with a CVC4 online backend. +-- The backend is only valid in the continuation. +-- +-- The CVC4 configuration options will be automatically +-- installed into the backend configuration object. +withCVC4OnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + UnsatFeatures -> + ProblemFeatures -> + (CVC4OnlineBackend scope st fs -> m a) -> + m a +withCVC4OnlineBackend sym unsatFeat extraFeatures action = + let feat = (SMT2.defaultFeatures CVC4.CVC4 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in + withOnlineBackend sym feat $ \bak -> do + liftIO $ tryExtendConfig CVC4.cvc4Options (getConfiguration sym) + action bak + +type CVC5OnlineBackend scope st fs = OnlineBackend (SMT2.Writer CVC5.CVC5) scope st fs + +-- | Do something with a CVC5 online backend. +-- The backend is only valid in the continuation. +-- +-- The CVC5 configuration options will be automatically +-- installed into the backend configuration object. +withCVC5OnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + UnsatFeatures -> + ProblemFeatures -> + (CVC5OnlineBackend scope st fs -> m a) -> + m a +withCVC5OnlineBackend sym unsatFeat extraFeatures action = + let feat = (SMT2.defaultFeatures CVC5.CVC5 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in + withOnlineBackend sym feat $ \bak -> do + liftIO $ tryExtendConfig CVC5.cvc5Options (getConfiguration sym) + action bak + +type STPOnlineBackend scope st fs = OnlineBackend (SMT2.Writer STP.STP) scope st fs + +-- | Do something with a STP online backend. +-- The backend is only valid in the continuation. +-- +-- The STO configuration options will be automatically +-- installed into the backend configuration object. +withSTPOnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + (STPOnlineBackend scope st fs -> m a) -> + m a +withSTPOnlineBackend sym action = + withOnlineBackend sym (SMT2.defaultFeatures STP.STP) $ \bak -> do + liftIO $ tryExtendConfig STP.stpOptions (getConfiguration sym) + action bak diff --git a/src/Lang/Crucible/Backend/ProofGoals.hs b/src/Lang/Crucible/Backend/ProofGoals.hs --- a/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/src/Lang/Crucible/Backend/ProofGoals.hs @@ -3,10 +3,11 @@ Copyright : (c) Galois, Inc 2014-2018 License : BSD3 -This module defines a data strucutre for storing a collection of -proof obligations, and the current state of assumptions. +This module defines a data structure ('GoalCollector') for storing the current +state of assumptions and a collection of proof obligations. -} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} @@ -22,6 +23,7 @@ -- * Goal collector , FrameIdentifier(..), GoalCollector , emptyGoalCollector + , ppGoalCollector -- ** traversals , traverseGoalCollector @@ -29,7 +31,7 @@ -- ** Context management , gcAddAssumes, gcProve - , gcPush, gcPop, gcAddGoals, + , gcPush, gcPop, gcAddGoals, gcAddTopLevelAssume, -- ** Global operations on context gcRemoveObligations, gcRestore, gcReset, gcFinish @@ -40,9 +42,11 @@ where import Control.Monad.Reader +import qualified Data.Foldable as F import Data.Sequence (Seq) import qualified Data.Sequence as Seq import Data.Word (Word64) +import qualified Prettyprinter as PP import Lang.Crucible.Backend.Goals @@ -55,16 +59,80 @@ deriving(Eq,Ord,Show) --- | A data-strucutre that can incrementally collect goals in context. +-- | A data-structure that can incrementally collect goals in context. -- It keeps track both of the collection of assumptions that lead to -- the current state, as well as any proof obligations incurred along -- the way. +-- +-- The main use of 'GoalCollector' is as the state of an +-- 'Lang.Crucible.Backend.AssumptionStack.AssumptionStack', which itself is +-- part of the state of the simple and online backends. +-- +-- 'GoalCollector' can be somewhat counter-intuitive. The "top" +-- ('TopCollector') is the *leaf* when 'GoalCollector' is considered as +-- a tree (which is a common way to conceptualize recursive algebraic +-- data types such as this one). A 'GoalCollector' is shaped like a +-- cons-list with three different cons-like constructors ('CollectorFrame', +-- 'CollectingAssumptions', and 'CollectingGoals') and one nil-like +-- constructor 'TopCollector'. That is to say, a 'GoalCollector' is a sequence +-- that always ends in a single 'TopCollector'. +-- +-- Furthermore, the frame identified by the first ('FrameIdentifier') argument +-- of 'CollectorFrame' does not conceptually contain the goals *inside* the +-- second ('GoalCollector') argument, but rather contains all the assumptions +-- and goals in whatever 'GoalCollector' *contains* the 'CollectorFrame' +-- constructor (everything *outside* of the 'CollectorFrame'). Concretely, in +-- the expression +-- @ +-- 'CollectingGoals' gls ('CollectingAssumptions' asmps ('CollectorFrame' frm ('TopCollector' gls0))) +-- @ +-- the goals @gls@ and assumptions @asmps@ are in the frame @frm@, rather than +-- the top-level goals @gls0@. +-- +-- This inside-out structure is reflected in the pretty-printer +-- 'ppGoalCollector' below. The Crucible-CLI test-case @assumption-state@ +-- shows this pretty-printer in action in a Crucible program with branching, +-- which can be helpful in understanding 'GoalCollector'. data GoalCollector asmp goal = TopCollector !(Seq (Goals asmp goal)) | CollectorFrame !FrameIdentifier !(GoalCollector asmp goal) | CollectingAssumptions !asmp !(GoalCollector asmp goal) | CollectingGoals !(Seq (Goals asmp goal)) !(GoalCollector asmp goal) +ppGoalCollector :: + forall asmp goal ann. + (asmp -> PP.Doc ann) -> + (goal -> PP.Doc ann) -> + GoalCollector asmp goal -> + PP.Doc ann +ppGoalCollector ppAsmp ppGoal = go mempty + where + go :: PP.Doc ann -> GoalCollector asmp goal -> PP.Doc ann + go remainder = + \case + TopCollector gls -> + PP.vcat + [ PP.pretty "Top-level goals:" + , PP.list (map (ppGoals ppAsmp ppGoal) (F.toList gls)) + , remainder + ] + CollectorFrame (FrameIdentifier fid) gc -> + let pLines = [PP.pretty "Frame " <> PP.viaShow fid <> PP.pretty ":", remainder] in + go (PP.hang 2 (PP.vcat pLines)) gc + CollectingAssumptions asmp gc -> + let pLines = [PP.pretty "Assumptions:" , ppAsmp asmp, remainder] in + go (PP.hang 2 (PP.vcat pLines)) gc + CollectingGoals gls gc -> + let pLines = [ PP.pretty "Prove all:" + , PP.list (map (ppGoals ppAsmp ppGoal) (F.toList gls)) + , remainder + ] in + go (PP.hang 2 (PP.vcat pLines)) gc + +-- | Intended for debugging, this is not generally a user-facing datatype. +instance (PP.Pretty asmp, PP.Pretty goal) => PP.Pretty (GoalCollector asmp goal) where + pretty = ppGoalCollector PP.pretty PP.pretty + -- | A collector with no goals and no context. emptyGoalCollector :: GoalCollector asmp goal emptyGoalCollector = TopCollector mempty @@ -141,6 +209,30 @@ gcAddGoals g (TopCollector gs) = TopCollector (gs Seq.|> g) gcAddGoals g (CollectingGoals gs gc) = CollectingGoals (gs Seq.|> g) gc gcAddGoals g gc = CollectingGoals (Seq.singleton g) gc + +-- | Add an assumption that is in scope for all goals, even ones in earlier +-- frames. +gcAddTopLevelAssume :: + Monoid asmp => + asmp -> + GoalCollector asmp goal -> + GoalCollector asmp goal +gcAddTopLevelAssume asmp = + \case + TopCollector gls -> + -- Syntactically, it appears that `asmp` is duplicated here, perhaps + -- unnecessarily. In fact, this is necessary. The `CollectingAssumptions` + -- constructor brings the assumption into scope for all the goals + -- *outside* of the top-level (see the comment on `GoalCollector` for + -- the "inside-out" structure of `GoalCollector`), whereas the `assuming` + -- brings it into scope for top-level goals. + CollectingAssumptions asmp (TopCollector (assuming asmp <$> gls)) + CollectorFrame frm gc -> + CollectorFrame frm (gcAddTopLevelAssume asmp gc) + CollectingAssumptions asmp' gc -> + CollectingAssumptions asmp' (gcAddTopLevelAssume asmp gc) + CollectingGoals gls gc -> + CollectingGoals gls (gcAddTopLevelAssume asmp gc) -- | Add a new proof obligation to the current context. gcProve :: goal -> GoalCollector asmp goal -> GoalCollector asmp goal diff --git a/src/Lang/Crucible/Backend/Simple.hs b/src/Lang/Crucible/Backend/Simple.hs --- a/src/Lang/Crucible/Backend/Simple.hs +++ b/src/Lang/Crucible/Backend/Simple.hs @@ -4,13 +4,13 @@ -- Description : The "simple" solver backend -- Copyright : (c) Galois, Inc 2015-2016 -- License : BSD3 --- Maintainer : Rob Dockins +-- Maintainer : Ryan Scott , Langston Barrett -- Stability : provisional -- --- An "offline" backend for communicating with solvers. This backend --- does not maintain a persistent connection to a solver, and does --- not perform satisfiability checks at symbolic branch points. ------------------------------------------------------------------------- +-- An "offline" backend for communicating with SMT solvers. In contrast to +-- "Lang.Crucible.Backend.Online", this backend does not maintain a persistent +-- connection to a solver. +-- ---------------------------------------------------------------------- {-# LANGUAGE GADTs #-} {-# LANGUAGE FlexibleContexts #-} @@ -32,6 +32,7 @@ import Control.Lens ( (^.) ) import Control.Monad (void) +import Data.IORef (readIORef) import What4.Config import What4.Interface @@ -42,7 +43,7 @@ import Lang.Crucible.Simulator.SimError ------------------------------------------------------------------------ --- SimpleBackendState +-- SimpleBackend -- | This represents the state of the backend along a given execution. -- It contains the current assertion stack. @@ -111,3 +112,5 @@ restoreAssumptionState bak newstk = do AS.restoreAssumptionStack newstk (sbAssumptionStack bak) + + getBackendState bak = readIORef (AS.proofObligations (sbAssumptionStack bak)) diff --git a/src/Lang/Crucible/Concretize.hs b/src/Lang/Crucible/Concretize.hs --- a/src/Lang/Crucible/Concretize.hs +++ b/src/Lang/Crucible/Concretize.hs @@ -7,15 +7,27 @@ -- Maintainer : Langston Barrett -- Stability : provisional -- --- This module defines 'concRegValue', a function that takes a 'RegValue' (i.e., --- a symbolic value), and a model from the SMT solver ('W4GE.GroundEvalFn'), and --- returns the concrete value that the symbolic value takes in the model. +-- This module defines three different kinds of functions. In order of how much +-- work they perform: -- --- This can be used to report specific values that lead to violations of --- assertions, including safety assertions. +-- * /Grounding/ functions (e.g., 'groundRegValue') take symbolic values +-- ('RegValue's) and a model from an SMT solver ('W4GE.GroundEvalFn'), and +-- return the concrete value ('ConcRegValue') that the symbolic value takes in +-- the model. These functions can be used to report specific values that lead +-- to violations of assertions, including safety assertions. +-- * /Concretization/ functions (e.g., 'concRegValue') request a model that is +-- consistent with the current assumptions (e.g., path conditions) from the +-- symbolic backend, and then ground a value in that model. These can be used +-- to reduce the size and complexity of later queries to SMT solvers, at the +-- cost of no longer being sound from a verification standpoint. +-- * /Unique concretization/ functions (e.g., 'uniquelyConcRegValue') do the +-- same thing as concretization functions, but then check if the concrete +-- value is the /only possible/ value for the given symbolic expression in +-- /any/ model. ------------------------------------------------------------------------ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE StandaloneKindSignatures #-} @@ -30,24 +42,38 @@ module Lang.Crucible.Concretize ( ConcRegValue , ConcRV'(..) + , asConcRegValue + , asConcRegEntry + , asConcRegMap , ConcAnyValue(..) , ConcIntrinsic , IntrinsicConcFn(..) , ConcCtx(..) + -- * Grounding + , groundRegValue + , groundRegEntry + , groundRegMap + -- * Concretization , concRegValue , concRegEntry , concRegMap + -- * Unique concretization + , uniquelyConcRegValue + , uniquelyConcRegEntry + , uniquelyConcRegMap -- * There and back again , IntrinsicConcToSymFn(..) , concToSym ) where import qualified Data.Foldable as F +import Data.Functor.Const (Const(..)) import Data.Kind (Type) import Data.List.NonEmpty (NonEmpty) import qualified Data.List.NonEmpty as NE import Data.Map (Map) import qualified Data.Map as Map +import Data.Proxy (Proxy(Proxy)) import Data.Sequence (Seq) import Data.Text (Text) import qualified Data.Text as Text @@ -57,14 +83,20 @@ import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Map (MapF) import qualified Data.Parameterized.Map as MapF -import Data.Parameterized.TraversableFC (traverseFC) +import Data.Parameterized.TraversableFC (traverseFC, foldlMFC) +import qualified What4.Concretize as W4C +import qualified What4.Config as W4Cfg import What4.Expr (Expr, ExprBuilder, Flags, FloatModeRepr(..)) import qualified What4.Expr.GroundEval as W4GE import What4.Interface (SymExpr) import qualified What4.Interface as W4I import qualified What4.Partial as W4P +import qualified What4.Protocol.Online as WPO +import qualified What4.SatResult as WSat +import qualified Lang.Crucible.Backend as CB +import qualified Lang.Crucible.Backend.Online as CBO import Lang.Crucible.FunctionHandle (FnHandle, RefCell) import Lang.Crucible.Simulator.Intrinsics (Intrinsic) import Lang.Crucible.Simulator.RegMap (RegEntry, RegMap) @@ -84,7 +116,7 @@ -- | Defines the \"concrete\" interpretations of 'CrucibleType' (as opposed -- to the \"symbolic\" interpretations, which are defined by 'RegValue'), as --- returned by 'concRegValue'. +-- returned by 'groundRegValue'. -- -- Unlike What4\'s 'W4GE.GroundValue', this type family is parameterized -- by @sym@, the symbolic backend. This is because Crucible makes use of @@ -112,10 +144,40 @@ ConcRegValue sym (IntrinsicType nm ctx) = ConcIntrinsic nm ctx ConcRegValue sym (StringMapType tp) = Map Text (ConcRV' sym tp) +-- | Check if a 'RegValue' is actually concrete +asConcRegValue :: + W4I.IsExpr (SymExpr sym) => + proxy sym -> + TypeRepr tp -> + RegValue sym tp -> + Maybe (ConcRegValue sym tp) +asConcRegValue _proxy tp val = + -- TODO: More cases could be added here. + case asBaseType tp of + AsBaseType {} -> W4GE.asGround val + _ -> Nothing + +-- | Check if a 'RM.RegEntry' is actually concrete +asConcRegEntry :: + forall sym tp. + W4I.IsExpr (SymExpr sym) => + RM.RegEntry sym tp -> + Maybe (ConcRegValue sym tp) +asConcRegEntry (RM.RegEntry t v) = asConcRegValue (Proxy @sym) t v + +-- | Check if a 'RM.RegMap' is actually concrete +asConcRegMap :: + forall sym tp. + W4I.IsExpr (SymExpr sym) => + RM.RegMap sym tp -> + Maybe (Ctx.Assignment (ConcRV' sym) tp) +asConcRegMap (RM.RegMap assign) = + traverseFC (\re -> ConcRV' <$> asConcRegEntry re) assign + --------------------------------------------------------------------- -- * ConcCtx --- | Context needed for 'concRegValue' +-- | Context needed for 'groundRegValue' -- -- The @t@ parameter matches that on 'W4GE.GroundEvalFn' and 'Expr', namely, it -- is a phantom type brand used to relate nonces to a specific nonce generator @@ -172,7 +234,7 @@ W4P.Partial (W4I.Pred sym) (RegValue sym tp) -> IO (Maybe (ConcRegValue sym tp)) concPartial ctx tp (W4P.Partial p v) = - iteIO ctx p (Just <$> concRegValue ctx tp v) (pure Nothing) + iteIO ctx p (Just <$> groundRegValue ctx tp v) (pure Nothing) -- | Helper, not exported concPartialWithErr :: @@ -224,13 +286,13 @@ --------------------------------------------------------------------- -- * Any --- | An 'AnyValue' concretized by 'concRegValue' +-- | An 'AnyValue' concretized by 'groundRegValue' data ConcAnyValue sym = forall tp. ConcAnyValue (TypeRepr tp) (ConcRV' sym tp) --------------------------------------------------------------------- -- * FnVal --- | A 'FnVal' concretized by 'concRegValue' +-- | A 'FnVal' concretized by 'groundRegValue' data ConcFnVal (sym :: Type) (args :: Ctx CrucibleType) (res :: CrucibleType) where ConcClosureFnVal :: !(ConcFnVal sym (args ::> tp) ret) -> @@ -260,7 +322,7 @@ \case RV.ClosureFnVal fv t v -> do concV <- concFnVal ctx (args Ctx.:> t) ret fv - v' <- concRegValue ctx t v + v' <- groundRegValue ctx t v pure (ConcClosureFnVal concV t (ConcRV' v')) RV.VarargsFnVal hdl extra -> pure (ConcVarargsFnVal hdl extra) @@ -306,7 +368,7 @@ concSymSequence ctx tp = SymSeq.concretizeSymSequence (ground ctx) - (fmap ConcRV' . concRegValue ctx tp) + (fmap ConcRV' . groundRegValue ctx tp) --------------------------------------------------------------------- -- * StringMap @@ -331,7 +393,7 @@ --------------------------------------------------------------------- -- * Variant --- | Note that we do not attempt to \"normalize\" variants in 'concRegValue' +-- | Note that we do not attempt to \"normalize\" variants in 'groundRegValue' -- in any way. If the model reports that multiple branches of a variant are -- plausible, then multiple branches might be included as 'Just's. newtype ConcVariantBranch sym tp @@ -356,21 +418,21 @@ Nothing -> pure (ConcVariantBranch Nothing) --------------------------------------------------------------------- --- * 'concRegValue' +-- * 'groundRegValue' -- | Pick a feasible concrete value from the model -- -- This function does not attempt to \"normalize\" variants nor mux trees in any -- way. If the model reports that multiple branches of a variant or mux tree are -- plausible, then multiple branches might be included in the result. -concRegValue :: +groundRegValue :: (SymExpr sym ~ Expr t) => W4I.IsExprBuilder sym => ConcCtx sym t -> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp) -concRegValue ctx tp v = +groundRegValue ctx tp v = case (tp, v) of -- Base types (BoolRepr, _) -> ground ctx v @@ -391,13 +453,13 @@ -- Simple recursive cases (AnyRepr, RV.AnyValue tp' v') -> - ConcAnyValue tp' . ConcRV' <$> concRegValue ctx tp' v' + ConcAnyValue tp' . ConcRV' <$> groundRegValue ctx tp' v' (RecursiveRepr symb tyCtx, RV.RolledType v') -> - concRegValue ctx (unrollType symb tyCtx) v' + groundRegValue ctx (unrollType symb tyCtx) v' (StructRepr tps, _) -> - Ctx.zipWithM (\tp' (RV.RV v') -> ConcRV' <$> concRegValue ctx tp' v') tps v + Ctx.zipWithM (\tp' (RV.RV v') -> ConcRV' <$> groundRegValue ctx tp' v') tps v (VectorRepr tp', _) -> - traverse (fmap ConcRV' . concRegValue ctx tp') v + traverse (fmap ConcRV' . groundRegValue ctx tp') v -- Cases with helper functions (MaybeRepr tp', _) -> @@ -422,26 +484,209 @@ -- Incomplete cases (WordMapRepr _ _, _) -> pure () --- | Like 'concRegValue', but for 'RegEntry' -concRegEntry :: +-- | Like 'groundRegValue', but for 'RegEntry' +groundRegEntry :: (SymExpr sym ~ Expr t) => W4I.IsExprBuilder sym => ConcCtx sym t -> RegEntry sym tp -> IO (ConcRegValue sym tp) -concRegEntry ctx e = concRegValue ctx (RM.regType e) (RM.regValue e) +groundRegEntry ctx e = groundRegValue ctx (RM.regType e) (RM.regValue e) --- | Like 'concRegEntry', but for a whole 'RegMap' -concRegMap :: +-- | Like 'groundRegEntry', but for a whole 'RegMap' +groundRegMap :: (SymExpr sym ~ Expr t) => W4I.IsExprBuilder sym => ConcCtx sym t -> RegMap sym tps -> IO (Ctx.Assignment (ConcRV' sym) tps) -concRegMap ctx (RM.RegMap m) = traverseFC (fmap ConcRV' . concRegEntry ctx) m +groundRegMap ctx (RM.RegMap m) = traverseFC (fmap ConcRV' . groundRegEntry ctx) m --------------------------------------------------------------------- --- * concToSym +-- * 'concRegValue' + +-- | Generate a model and pick a feasible concrete value from it +concRegValue :: + forall tp sym bak solver scope st fs. + ( CB.IsSymBackend sym bak + , sym ~ ExprBuilder scope st fs + , SymExpr sym ~ Expr scope + , bak ~ CBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + ) => + bak -> + MapF SymbolRepr (IntrinsicConcFn scope) -> + TypeRepr tp -> + RegValue sym tp -> + IO (Either W4C.ConcretizationFailure (ConcRegValue sym tp)) +concRegValue bak iFns tp v = concRegEntry bak iFns (RM.RegEntry tp v) + +-- | Generate a model and pick a feasible concrete value from it +concRegEntry :: + forall tp sym bak solver scope st fs. + ( CB.IsSymBackend sym bak + , sym ~ ExprBuilder scope st fs + , SymExpr sym ~ Expr scope + , bak ~ CBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + ) => + bak -> + MapF SymbolRepr (IntrinsicConcFn scope) -> + RM.RegEntry sym tp -> + IO (Either W4C.ConcretizationFailure (ConcRegValue sym tp)) +concRegEntry bak iFns re = do + res <- concRegMap bak iFns (RM.RegMap (Ctx.singleton re)) + case res of + Left e -> pure (Left e) + Right (Ctx.Empty Ctx.:> ConcRV' concV) -> pure (Right concV) + +-- | Like 'concRegValue', but for a whole 'RegMap' +concRegMap :: + forall tps sym bak solver scope st fs. + ( CB.IsSymBackend sym bak + , sym ~ ExprBuilder scope st fs + , SymExpr sym ~ Expr scope + , bak ~ CBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + ) => + bak -> + MapF SymbolRepr (IntrinsicConcFn scope) -> + RegMap sym tps -> + IO (Either W4C.ConcretizationFailure (Ctx.Assignment (ConcRV' sym) tps)) +concRegMap bak iFns m = do + case asConcRegMap m of + Just concM -> pure (Right concM) + Nothing -> + withEnabledOnline $ do + let err = panic "concRegValue" ["requires online solving to be enabled"] + cond <- CB.getPathCondition bak + CBO.withSolverProcess bak err $ \sp -> do + msat <- WPO.checkWithAssumptionsAndModel sp "concRegValue" [cond] + case msat of + WSat.Unknown -> pure $ Left W4C.SolverUnknown + WSat.Unsat {} -> pure $ Left W4C.UnsatInitialAssumptions + WSat.Sat mdl -> do + let ctx = ConcCtx { model = mdl, intrinsicConcFuns = iFns } + expr <- groundRegMap @sym ctx m + pure (Right expr) + where + withEnabledOnline f = do + let sym = CB.backendGetSym bak + let conf = W4I.getConfiguration sym + enabledOpt <- W4Cfg.getOptionSetting CBO.enableOnlineBackend conf + wasEnabled <- W4Cfg.getOpt enabledOpt + _ <- W4Cfg.setOpt enabledOpt True + r <- f + _ <- W4Cfg.setOpt enabledOpt wasEnabled + pure r + +--------------------------------------------------------------------- +-- * 'uniquelyConcRegValue' + +-- | Generate a model and pick a feasible concrete value from it +uniquelyConcRegValue :: + forall tp sym bak solver scope st fm. + ( CB.IsSymBackend sym bak + , sym ~ ExprBuilder scope st (Flags fm) + , SymExpr sym ~ Expr scope + , bak ~ CBO.OnlineBackend solver scope st (Flags fm) + , WPO.OnlineSolver solver + ) => + bak -> + FloatModeRepr fm -> + MapF SymbolRepr (IntrinsicConcFn scope) -> + MapF SymbolRepr IntrinsicConcToSymFn -> + TypeRepr tp -> + RegValue sym tp -> + IO (Either W4C.UniqueConcretizationFailure (ConcRegValue sym tp)) +uniquelyConcRegValue bak fm iFns sFns tp v = + uniquelyConcRegEntry bak fm iFns sFns (RM.RegEntry tp v) + +-- | Generate a model and pick a feasible concrete value from it +uniquelyConcRegEntry :: + forall tp sym bak solver scope st fm. + ( CB.IsSymBackend sym bak + , sym ~ ExprBuilder scope st (Flags fm) + , SymExpr sym ~ Expr scope + , bak ~ CBO.OnlineBackend solver scope st (Flags fm) + , WPO.OnlineSolver solver + ) => + bak -> + FloatModeRepr fm -> + MapF SymbolRepr (IntrinsicConcFn scope) -> + MapF SymbolRepr IntrinsicConcToSymFn -> + RM.RegEntry sym tp -> + IO (Either W4C.UniqueConcretizationFailure (ConcRegValue sym tp)) +uniquelyConcRegEntry bak fm iFns sFns re = do + res <- uniquelyConcRegMap bak fm iFns sFns (RM.RegMap (Ctx.singleton re)) + case res of + Left e -> pure (Left e) + Right (Ctx.Empty Ctx.:> ConcRV' concV) -> pure (Right concV) + +-- | Like 'concRegValue', but for a whole 'RegMap' +uniquelyConcRegMap :: + forall tps sym bak solver scope st fm. + ( CB.IsSymBackend sym bak + , sym ~ ExprBuilder scope st (Flags fm) + , SymExpr sym ~ Expr scope + , bak ~ CBO.OnlineBackend solver scope st (Flags fm) + , WPO.OnlineSolver solver + ) => + bak -> + FloatModeRepr fm -> + MapF SymbolRepr (IntrinsicConcFn scope) -> + MapF SymbolRepr IntrinsicConcToSymFn -> + RegMap sym tps -> + IO (Either W4C.UniqueConcretizationFailure (Ctx.Assignment (ConcRV' sym) tps)) +uniquelyConcRegMap bak fm iFns sFns m = do + case asConcRegMap m of + Just concM -> pure (Right concM) + Nothing -> do + -- First, check to see if there are a models of the symbolic values. + concM_ <- concRegMap bak iFns m + case concM_ of + Left e -> pure (Left (W4C.GroundingFailure e)) + Right concM -> do + -- We found a model, so check to see if this is the only possible + -- model for these symbolic values. We do this by adding a blocking + -- clause that assumes the `RegValue`s are /not/ equal to the + -- model we found in the previous step. If this is unsatisfiable, + -- the `RegValue`s can only be equal to the first model, so we can + -- conclude they are concrete. If it is satisfiable, on the other + -- hand, the `RegValue`s can be multiple values, so they are truly + -- symbolic. + let sym = CB.backendGetSym bak + let notEq :: + forall tp. + ConcRV' sym tp -> + RM.RegEntry sym tp -> + IO (Const (W4I.Pred sym) tp) + notEq (ConcRV' concV) (RM.RegEntry tp v) = do + symV <- concToSym sym sFns fm tp concV + p <- W4I.notPred sym =<< RV.eqRegValue sym tp symV v + pure (Const p) + let RM.RegMap mAssign = m + preds <- Ctx.zipWithM notEq concM mAssign + p <- + foldlMFC + (\p (Const p') -> W4I.andPred sym p p') + (W4I.truePred sym) + preds + + frm <- CB.pushAssumptionFrame bak + loc <- W4I.getCurrentProgramLoc sym + CB.addAssumption bak (CB.GenericAssumption loc "uniquelyConcRegMap" p) + concM_' <- concRegMap bak iFns m + res <- + case concM_' of + Left W4C.UnsatInitialAssumptions -> pure (Right concM) + Left e -> pure (Left (W4C.GroundingFailure e)) + Right _ -> pure (Left W4C.MultipleModels) + _ <- CB.popAssumptionFrame bak frm + pure res + +--------------------------------------------------------------------- +-- * 'concToSym' -- | Function for re-symbolizing an intrinsic type type IntrinsicConcToSymFn :: Symbol -> Type diff --git a/src/Lang/Crucible/README.hs b/src/Lang/Crucible/README.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/README.hs @@ -0,0 +1,113 @@ +{- | This module is only for documentation purposes, and provides a high +level overview of Crucible aimed at developers. -} +{-# OPTIONS_GHC -Wno-unused-imports #-} +module Lang.Crucible.README where + +import What4.Interface +import What4.Expr.App +import What4.BaseTypes +import Lang.Crucible.Backend + +import Lang.Crucible.Types +import Lang.Crucible.CFG.Expr +import Lang.Crucible.CFG.Core hiding (Expr) +import Lang.Crucible.CFG.SSAConversion + +import Lang.Crucible.Simulator.RegValue +import Lang.Crucible.Simulator.RegMap +import Lang.Crucible.Simulator.ExecutionTree +import Lang.Crucible.Simulator.EvalStmt +import Lang.Crucible.Simulator.Evaluation +import Lang.Crucible.Simulator.Intrinsics + + + +-- * Crucible Types + +{- $ +The types of the Crucible language are defined in "Lang.Crucible.Types". +Types are encoded using [singletons](https://github.com/Galoisinc/parameterized-utils?tab=readme-ov-file#parameterized-types-motivation): + +* 'CrucibleType' is the Haskell type-level description of all Crucible types +* 'TypeRepr' are the associated value-level singletons, which + are used when we pass around types, or store them in data structures. +-} + +-- * Crucible Values + +{- $ +The inhabitants of each type are specified via the type function 'RegValue'. +We also have 'RegValue'' which is just a @newtype@ wrapper around 'RegValue', +because in Haskell type families may not be partially applied but @newtype@s can. + +An important subset of the Crucible types are the base types (see 'BaseToType'), +which is for the symbolic expression we can construct +(see 'SymExpr' in [what4](https://github.com/Galoisinc/what4)). +Only these types may contain variables. In practice, we always use @what4@'s +'Expr' type to represent symbolic expressions. + +Also, in some cases we use 'RegEntry' which +is just a pair of a 'RegValue' and its associated 'TypeRepr'. + +There's also 'BaseTerm', which is similar to 'RegEntry' but +for base types---it contains a @what4@'s 'BaseTypeRepr' and a value of the corresponding +base type (usually; the type is parameterized on exactly what we package +with the type). +-} + +-- * Crucible Programs + +{- $ +The program executed by the simulator is in the form of a control flow +graph (CFG). A typical way to construct them is as follows: + + 1. use the functions in "Lang.Crucible.CFG.Generator" to produce a CFG with + assignments ("Lang.Crucible.CFG.Reg") + 2. use 'toSSA' to translate this to a CFG without assignments + ("Lang.Crucible.CFG.Core") + +The core 'CFG' contains basic blocks with 'Stmt's and terminated +by 'TermStmt'. The expression language for the core 'Core.CFG' is +the type 'App'. +-} + +-- * Symbolic Simulator + +{- $ +The state of a running simulator is described in "Lang.Crucible.Simulator.ExecutionTree": + + * 'ExecState' is the current state of execution. + We start with 'InitialState', and keep performing steps until we get + to a 'ResultState'. + * As the simulator executes, it keeps track of its state in 'SimState', + which is stored in the current `ExecState`. + * 'SimContext' is the part of the state that persists across branches + (e.g, after we explore the @then@ part of an @if@ statement, we'll + roll back some of the state changes before simulating the @else@ part, + but the data in 'SimContext's persists). An important part of the + 'SimContext' is the simulator's backend ('_ctxBackend'), which is how the + simulator communicates with a solver, and builds symbolic expressions + ('IsSymBackend'). + + +To evaluate a 'CFG' we evaluate the statements as described in +"Lang.Crucible.Simulator.EvalStmt" (details in 'stepStmt', 'stepTerm'). +Details about expressions evaluation are in 'evalApp' in "Lang.Crucible.Simulator.Evaluation". + +A lot of useful functionality relevant to the simulator can be accessed +from module "Lang.Crucible.Simulator". + +The simulator supports mutable global variables. Our tools use one such +global to store a language specific memory model, which records information +about various memory operations. +-} + +-- * Intrinsics + +{- $ + +Crucible type may be extended using 'IntrinsicType's. An intrinsic type is +a type-level string, which can be given meaning by making an instance of +'IntrinsicClass'. +-} + diff --git a/src/Lang/Crucible/Simulator/BoundedExec.hs b/src/Lang/Crucible/Simulator/BoundedExec.hs --- a/src/Lang/Crucible/Simulator/BoundedExec.hs +++ b/src/Lang/Crucible/Simulator/BoundedExec.hs @@ -183,7 +183,7 @@ Bool {- ^ Produce a proof obligation when resources are exhausted? -} -> IO (GenericExecutionFeature sym) boundedExecFeature getLoopBounds generateSideConditions = - do gvRef <- newIORef (error "Global variable for BoundedExecFrameData not initialized") + do gvRef <- newIORef Nothing return $ GenericExecutionFeature $ onStep gvRef where @@ -202,48 +202,52 @@ } checkBackedge :: - IORef BoundedExecGlobal -> + IORef (Maybe BoundedExecGlobal) -> Some (BlockID blocks) -> BlockID blocks tgt_args -> SymGlobalState sym -> IO (SymGlobalState sym, Maybe Word64) - checkBackedge gvRef (Some bid_curr) bid_tgt globals = - do gv <- readIORef gvRef - case fromMaybe [] (lookupGlobal gv globals) of - ( Right fbd : rest ) -> - do let id_curr = Ctx.indexVal (blockIDIndex bid_curr) - let id_tgt = Ctx.indexVal (blockIDIndex bid_tgt) - let m = frameWtoMap fbd - case (Map.lookup id_curr m, Map.lookup id_tgt m) of - (Just (cx, _cd), Just (tx, td)) | tx <= cx -> - do let cs = frameBoundCounts fbd - let (cs', q) = incrementBoundCount cs td - let fbd' = fbd{ frameBoundCounts = cs' } - let globals' = insertGlobal gv (Right fbd' : rest) globals - if q > frameBoundLimit fbd then - return (globals', Just (frameBoundLimit fbd)) - else - return (globals', Nothing) - - _ -> return (globals, Nothing) - _ -> return (globals, Nothing) + checkBackedge gvRef (Some bid_curr) bid_tgt globals = do + let err = panic "checkBackedge" ["Global not initialized"] + currGv <- readIORef gvRef + let gv = fromMaybe err currGv + case fromMaybe [] (lookupGlobal gv globals) of + (Right fbd : rest) -> do + let id_curr = Ctx.indexVal (blockIDIndex bid_curr) + let id_tgt = Ctx.indexVal (blockIDIndex bid_tgt) + let m = frameWtoMap fbd + case (Map.lookup id_curr m, Map.lookup id_tgt m) of + (Just (cx, _cd), Just (tx, td)) | tx <= cx -> do + let cs = frameBoundCounts fbd + let (cs', q) = incrementBoundCount cs td + let fbd' = fbd{frameBoundCounts = cs'} + let globals' = insertGlobal gv (Right fbd' : rest) globals + if q > frameBoundLimit fbd + then + return (globals', Just (frameBoundLimit fbd)) + else + return (globals', Nothing) + _ -> return (globals, Nothing) + _ -> return (globals, Nothing) modifyStackState :: - IORef BoundedExecGlobal -> + IORef (Maybe BoundedExecGlobal) -> (SimState p sym ext rtp f args -> ExecState p sym ext rtp) -> SimState p sym ext rtp f args -> ([Either FunctionName FrameBoundData] -> [Either FunctionName FrameBoundData]) -> IO (ExecutionFeatureResult p sym ext rtp) - modifyStackState gvRef mkSt st f = - do gv <- readIORef gvRef - let xs = case lookupGlobal gv (st ^. stateGlobals) of - Nothing -> error "bounded execution global not defined!" - Just v -> v - let st' = st & stateGlobals %~ insertGlobal gv (f xs) - return (ExecutionFeatureModifiedState (mkSt st')) + modifyStackState gvRef mkSt st f = do + currGv <- readIORef gvRef + let err = panic "modifyStackState" ["Global variable not initialized"] + let gv = fromMaybe err currGv + let xs = case lookupGlobal gv (st ^. stateGlobals) of + Nothing -> panic "modifyStackState" ["Global variable not defined!"] + Just v -> v + let st' = st & stateGlobals %~ insertGlobal gv (f xs) + return (ExecutionFeatureModifiedState (mkSt st')) onTransition :: - IORef BoundedExecGlobal -> + IORef (Maybe BoundedExecGlobal) -> BlockID blocks tgt_args -> ControlResumption p sym ext rtp (CrucibleLang blocks ret) -> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a) -> @@ -264,16 +268,21 @@ Nothing -> return (ExecutionFeatureModifiedState (ControlTransferState res st')) onStep :: - IORef BoundedExecGlobal -> + IORef (Maybe BoundedExecGlobal) -> ExecState p sym ext rtp -> IO (ExecutionFeatureResult p sym ext rtp) onStep gvRef = \case InitialState simctx globals ah ret cont -> do let halloc = simHandleAllocator simctx - gv <- freshGlobalVar halloc (Text.pack "BoundedExecFrameData") knownRepr - writeIORef gvRef gv - let globals' = insertGlobal gv [Left "_init"] globals + currGv <- readIORef gvRef + ngv <- case currGv of + Nothing -> do + gv <- freshGlobalVar halloc (Text.pack "BoundedExecFrameData") knownRepr + writeIORef gvRef (Just gv) + pure gv + Just gv -> pure gv + let globals' = insertGlobal ngv [Left "_init"] globals let simctx' = simctx{ ctxIntrinsicTypes = MapF.insert (knownSymbol @"BoundedExecFrameData") IntrinsicMuxFn (ctxIntrinsicTypes simctx) } return (ExecutionFeatureModifiedState (InitialState simctx' globals' ah ret cont)) diff --git a/src/Lang/Crucible/Simulator/BoundedRecursion.hs b/src/Lang/Crucible/Simulator/BoundedRecursion.hs --- a/src/Lang/Crucible/Simulator/BoundedRecursion.hs +++ b/src/Lang/Crucible/Simulator/BoundedRecursion.hs @@ -81,26 +81,28 @@ IO (GenericExecutionFeature sym) boundedRecursionFeature getRecursionBound generateSideConditions = - do gvRef <- newIORef (error "Global variable for BoundedRecursionData not initialized") + do gvRef <- newIORef Nothing return $ GenericExecutionFeature $ onStep gvRef where popFrame :: - IORef BoundedRecursionGlobal -> + IORef (Maybe BoundedRecursionGlobal) -> (SimState p sym ext rtp f args -> ExecState p sym ext rtp) -> SimState p sym ext rtp f args -> IO (ExecutionFeatureResult p sym ext rtp) - popFrame gvRef mkSt st = - do gv <- readIORef gvRef - case lookupGlobal gv (st ^. stateGlobals) of - Nothing -> panic "bounded recursion" ["global not defined!"] - Just [] -> panic "bounded recursion" ["pop on empty stack!"] - Just (_:xs) -> - do let st' = st & stateGlobals %~ insertGlobal gv xs - return (ExecutionFeatureModifiedState (mkSt st')) + popFrame gvRef mkSt st = do + currGv <- readIORef gvRef + let err = panic "bounded recursion" ["gv not initialized"] + let gv = fromMaybe err currGv + case lookupGlobal gv (st ^. stateGlobals) of + Nothing -> panic "bounded recursion" ["global not defined!"] + Just [] -> panic "bounded recursion" ["pop on empty stack!"] + Just (_ : xs) -> do + let st' = st & stateGlobals %~ insertGlobal gv xs + return (ExecutionFeatureModifiedState (mkSt st')) pushFrame :: - IORef BoundedRecursionGlobal -> + IORef (Maybe BoundedRecursionGlobal) -> (BoundedRecursionMap -> BoundedRecursionMap -> [BoundedRecursionMap] -> [BoundedRecursionMap]) -> SomeHandle -> (SimState p sym ext rtp f args -> ExecState p sym ext rtp) -> @@ -109,28 +111,31 @@ pushFrame gvRef rebuildStack h mkSt st = stateSolverProof st $ do let sym = st^.stateSymInterface let simCtx = st^.stateContext - gv <- readIORef gvRef + currGv <- readIORef gvRef + let err = panic "pushFrame" ["Uninitialized global!"] + let gv = fromMaybe err currGv case lookupGlobal gv (st ^. stateGlobals) of Nothing -> panic "bounded recursion" ["global not defined!"] Just [] -> panic "bounded recursion" ["empty stack!"] - Just (x:xs) -> - do mb <- getRecursionBound h - let v = 1 + fromMaybe 0 (Map.lookup h x) - case mb of - Just b | v > b -> - do loc <- getCurrentProgramLoc sym - let msg = ("reached maximum number of recursive calls to function " ++ show h ++ " (" ++ show b ++ ")") - let err = SimError loc (ResourceExhausted msg) - when generateSideConditions $ withBackend simCtx $ \bak -> - addProofObligation bak (LabeledPred (falsePred sym) err) - return (ExecutionFeatureNewState (AbortState (AssertionFailure err) st)) - _ -> - do let x' = Map.insert h v x - let st' = st & stateGlobals %~ insertGlobal gv (rebuildStack x' x xs) - x' `seq` return (ExecutionFeatureModifiedState (mkSt st')) + Just (x:xs) -> do + mb <- getRecursionBound h + let v = 1 + fromMaybe 0 (Map.lookup h x) + case mb of + Just b | v > b -> do + loc <- getCurrentProgramLoc sym + let msg = ("reached maximum number of recursive calls to function " ++ show h ++ " (" ++ show b ++ ")") + let simerr = SimError loc (ResourceExhausted msg) + when generateSideConditions $ withBackend simCtx $ \bak -> + addProofObligation bak (LabeledPred (falsePred sym) simerr) + return (ExecutionFeatureNewState (AbortState (AssertionFailure simerr) st)) + _ -> do + let x' = Map.insert h v x + let st' = st & stateGlobals %~ insertGlobal gv (rebuildStack x' x xs) + x' `seq` return (ExecutionFeatureModifiedState (mkSt st')) + onStep :: - IORef BoundedRecursionGlobal -> + IORef (Maybe BoundedRecursionGlobal) -> ExecState p sym ext rtp -> IO (ExecutionFeatureResult p sym ext rtp) @@ -138,8 +143,13 @@ InitialState simctx globals ah ret cont -> do let halloc = simHandleAllocator simctx - gv <- freshGlobalVar halloc (Text.pack "BoundedRecursionData") knownRepr - writeIORef gvRef gv + currGv <- readIORef gvRef + gv <- case currGv of + Just gv -> pure gv + Nothing -> do + gv <- freshGlobalVar halloc (Text.pack "BoundedRecursionData") knownRepr + writeIORef gvRef (Just gv) + pure gv let simctx' = simctx{ ctxIntrinsicTypes = MapF.insert (knownSymbol @"BoundedRecursionData") IntrinsicMuxFn diff --git a/src/Lang/Crucible/Simulator/CallFrame.hs b/src/Lang/Crucible/Simulator/CallFrame.hs --- a/src/Lang/Crucible/Simulator/CallFrame.hs +++ b/src/Lang/Crucible/Simulator/CallFrame.hs @@ -281,7 +281,13 @@ FrameRetType (CrucibleLang b r) = r FrameRetType (OverrideLang r) = r -data SimFrame sym ext l (args :: Maybe (Ctx CrucibleType)) where +-- | A frame on the stack. +-- +-- Type parameters: +-- +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +-- - @args@: arguments; 'Just' for call frames, 'Nothing' for a return frame +data SimFrame sym ext f (args :: Maybe (Ctx CrucibleType)) where -- | Custom code to execute, typically for "overrides" OF :: !(OverrideFrame sym ret args) -> SimFrame sym ext (OverrideLang ret) ('Just args) diff --git a/src/Lang/Crucible/Simulator/ExecutionTree.hs b/src/Lang/Crucible/Simulator/ExecutionTree.hs --- a/src/Lang/Crucible/Simulator/ExecutionTree.hs +++ b/src/Lang/Crucible/Simulator/ExecutionTree.hs @@ -30,6 +30,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fprint-explicit-kinds -Wall #-} @@ -68,8 +69,12 @@ , ResolvedCall(..) , resolvedCallHandle , execResultContext + , setExecResultContext , execStateContext + , setExecStateContext , execStateSimState + , execResultGlobals + , execStateGlobals -- * Simulator context trees -- ** Main context data structures @@ -174,8 +179,14 @@ ------------------------------------------------------------------------ -- GlobalPair --- | A value of some type 'v' together with a global state. -data GlobalPair sym (v :: Type) = +-- | A value of some type @v@ together with a global state. +-- +-- Type parameters: +-- +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @v@: type of the value +type GlobalPair :: Type -> Type -> Type +data GlobalPair sym v = GlobalPair { _gpValue :: !v , _gpGlobals :: !(SymGlobalState sym) @@ -194,7 +205,15 @@ -- TopFrame -- | The currently-executing frame plus the global state associated with it. -type TopFrame sym ext f a = GlobalPair sym (SimFrame sym ext f a) +-- +-- Type parameters: +-- +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +-- - @args@: arguments to this frame (see 'SimFrame') +type TopFrame :: Type -> Type -> Type -> Maybe (Ctx CrucibleType) -> Type +type TopFrame sym ext f args = GlobalPair sym (SimFrame sym ext f args) -- | Access the Crucible call frame inside a 'TopFrame'. crucibleTopFrame :: @@ -222,6 +241,12 @@ -- path might abort because it became infeasible (inconsistent path -- conditions), because the program called an exit primitive, or -- because of a true error condition (e.g., a failed assertion). +-- +-- Type parameters: +-- +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +type AbortedResult :: Type -> Type -> Type data AbortedResult sym ext where -- | A single aborted execution with the execution state at time of the abort and the reason. AbortedExec :: @@ -229,9 +254,10 @@ !(GlobalPair sym (SimFrame sym ext l args)) -> AbortedResult sym ext - -- | An aborted execution that was ended by a call to 'exit'. + -- | An aborted execution that was ended by a call to @exit@. AbortedExit :: !ExitCode -> + !(GlobalPair sym (SimFrame sym ext l args)) -> AbortedResult sym ext -- | Two separate threads of execution aborted after a symbolic branch, @@ -248,7 +274,10 @@ -- | This represents an execution frame where its frame type -- and arguments have been hidden. -data SomeFrame (f :: fk -> argk -> Type) = forall l a . SomeFrame !(f l a) +-- +-- The type parameter @f@ is usually 'SimFrame'. +type SomeFrame :: forall fk argk. (fk -> argk -> Type) -> Type +data SomeFrame f = forall l a . SomeFrame !(f l a) -- | Return the program locations of all the Crucible frames. filterCrucibleFrames :: SomeFrame (SimFrame sym ext) -> Maybe ProgramLoc @@ -260,7 +289,9 @@ arFrames h (AbortedExec e p) = (\(SomeFrame f') -> AbortedExec e (p & gpValue .~ f')) <$> h (SomeFrame (p^.gpValue)) -arFrames _ (AbortedExit ec) = pure (AbortedExit ec) +arFrames h (AbortedExit ec p) = + (\(SomeFrame f') -> AbortedExit ec (p & gpValue .~ f')) + <$> h (SomeFrame (p^.gpValue)) arFrames h (AbortedBranch predicate loc r s) = AbortedBranch predicate loc <$> arFrames h r <*> arFrames h s @@ -289,7 +320,14 @@ -- 'PartialResult', then some of the computation paths that led to -- this result aborted for some reason, and the resulting value is -- only defined if the associated condition is true. -data PartialResult sym ext (v :: Type) +-- +-- Type parameters: +-- +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @v@: Type of the result of the computation +type PartialResult :: Type -> Type -> Type -> Type +data PartialResult sym ext v {- | A 'TotalRes' indicates that the the global pair is always defined. -} = TotalRes !(GlobalPair sym v) @@ -318,6 +356,14 @@ {-# INLINE partialValue #-} -- | The result of resolving a function call. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @ret@: 'CrucibleType' of the return value +type ResolvedCall :: Type -> Type -> Type -> CrucibleType -> Type data ResolvedCall p sym ext ret where -- | A resolved function call to an override. OverrideCall :: @@ -341,15 +387,23 @@ -- | Executions that have completed either due to (partial or total) -- successful completion or by some abort condition. -data ExecResult p sym ext (r :: Type) +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +type ExecResult :: Type -> Type -> Type -> Type -> Type +data ExecResult p sym ext rtp = -- | At least one execution path resulted in some return result. - FinishedResult !(SimContext p sym ext) !(PartialResult sym ext r) + FinishedResult !(SimContext p sym ext) !(PartialResult sym ext rtp) -- | All execution paths resulted in an abort condition, and there is -- no result to return. | AbortedResult !(SimContext p sym ext) !(AbortedResult sym ext) -- | An execution stopped somewhere in the middle of a run because -- a timeout condition occurred. - | TimeoutResult !(ExecState p sym ext r) + | TimeoutResult !(ExecState p sym ext rtp) execResultContext :: ExecResult p sym ext r -> SimContext p sym ext @@ -357,6 +411,16 @@ execResultContext (AbortedResult ctx _) = ctx execResultContext (TimeoutResult exst) = execStateContext exst +setExecResultContext :: + SimContext p sym ext -> + ExecResult p sym ext r -> + ExecResult p sym ext r +setExecResultContext ctx = + \case + FinishedResult _ x -> FinishedResult ctx x + AbortedResult _ x -> AbortedResult ctx x + TimeoutResult execState -> TimeoutResult (setExecStateContext ctx execState) + execStateContext :: ExecState p sym ext r -> SimContext p sym ext execStateContext = \case ResultState res -> execResultContext res @@ -372,6 +436,24 @@ BranchMergeState _ st -> st^.stateContext InitialState stctx _ _ _ _ -> stctx +setExecStateContext :: + SimContext p sym ext -> + ExecState p sym ext r -> + ExecState p sym ext r +setExecStateContext ctx = \case + ResultState res -> ResultState (setExecResultContext ctx res) + AbortState x st -> AbortState x (st & stateContext .~ ctx) + UnwindCallState x y st -> UnwindCallState x y (st & stateContext .~ ctx) + CallState x y st -> CallState x y (st & stateContext .~ ctx) + TailCallState x y st -> TailCallState x y (st & stateContext .~ ctx) + ReturnState x y z st -> ReturnState x y z (st & stateContext .~ ctx) + ControlTransferState x st -> ControlTransferState x (st & stateContext .~ ctx) + RunningState x st -> RunningState x (st & stateContext .~ ctx) + SymbolicBranchState u v x y st -> SymbolicBranchState u v x y (st & stateContext .~ ctx) + OverrideState x st -> OverrideState x (st & stateContext .~ ctx) + BranchMergeState x st -> BranchMergeState x (st & stateContext .~ ctx) + InitialState _ u v x y -> InitialState ctx u v x y + execStateSimState :: ExecState p sym ext r -> Maybe (SomeSimState p sym ext r) execStateSimState = \case @@ -388,6 +470,66 @@ BranchMergeState _ st -> Just (SomeSimState st) InitialState _ _ _ _ _ -> Nothing +abortedGlobals :: + Monad f => + -- | How to handle 'AbortedBranch'. + -- + -- Common options include concretizing the 'Pred' or returning a partial + -- result (e.g., 'Nothing'). + (ProgramLoc -> Pred sym -> SymGlobalState sym -> SymGlobalState sym -> f (SymGlobalState sym)) -> + AbortedResult sym ext -> + f (SymGlobalState sym) +abortedGlobals handleBranch = + \case + AbortedExec _ gp -> pure (gp ^. gpGlobals) + AbortedExit _ gp -> pure (gp ^. gpGlobals) + AbortedBranch loc p rl rr -> do + l <- abortedGlobals handleBranch rl + r <- abortedGlobals handleBranch rr + handleBranch loc p l r + +-- | Extract the 'SymGlobalState' from an 'ExecResult'. +execResultGlobals :: + Monad f => + -- | How to handle 'AbortedBranch'. + -- + -- Common options include concretizing the 'Pred' or returning a partial + -- result (e.g., 'Nothing'). + (SimContext p sym ext -> ProgramLoc -> Pred sym -> SymGlobalState sym -> SymGlobalState sym -> f (SymGlobalState sym)) -> + ExecResult p sym ext rtp -> + f (SymGlobalState sym) +execResultGlobals handleBranch = + \case + FinishedResult _ctx partial -> pure (partial ^. partialValue . gpGlobals) + TimeoutResult st -> execStateGlobals handleBranch st + AbortedResult simCtx aborted -> + abortedGlobals (handleBranch simCtx) aborted + +-- | Extract the 'SymGlobalState' from an 'ExecState'. +execStateGlobals :: + Monad f => + -- | How to handle 'AbortedBranch'. + -- + -- Common options include concretizing the 'Pred' or returning a partial + -- result (e.g., 'Nothing'). + (SimContext p sym ext -> ProgramLoc -> Pred sym -> SymGlobalState sym -> SymGlobalState sym -> f (SymGlobalState sym)) -> + ExecState p sym ext rtp -> + f (SymGlobalState sym) +execStateGlobals handleBranch = + \case + AbortState _ st -> pure (st ^. stateGlobals) + BranchMergeState _ st -> pure (st ^. stateGlobals) + CallState _ _ st -> pure (st ^. stateGlobals) + ControlTransferState _ st -> pure (st ^. stateGlobals) + InitialState _ globState _ _ _ -> pure globState + OverrideState _ st -> pure (st ^. stateGlobals) + ResultState r -> execResultGlobals handleBranch r + ReturnState _ _ _ st -> pure (st ^. stateGlobals) + RunningState _ st -> pure (st ^. stateGlobals) + SymbolicBranchState _ _ _ _ st -> pure (st ^. stateGlobals) + TailCallState _ _ st -> pure (st ^. stateGlobals) + UnwindCallState _ _ st -> pure (st ^. stateGlobals) + ----------------------------------------------------------------------- -- ExecState @@ -395,7 +537,15 @@ -- Crucible program. The Crucible simulator executes by transitioning -- between these different states until it results in a 'ResultState', -- indicating the program has completed. -data ExecState p sym ext (rtp :: Type) +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +type ExecState :: Type -> Type -> Type -> Type -> Type +data ExecState p sym ext rtp {- | The 'ResultState' is used to indicate that the program has completed. -} = ResultState !(ExecResult p sym ext rtp) @@ -532,11 +682,27 @@ -- | An action which will construct an 'ExecState' given a current -- 'SimState'. Such continuations correspond to a single transition -- of the simulator transition system. -type ExecCont p sym ext r f a = - ReaderT (SimState p sym ext r f a) IO (ExecState p sym ext r) +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +-- - @args@: arguments to the current frame (see 'SimFrame') +type ExecCont :: Type -> Type -> Type -> Type -> Type -> Maybe (Ctx.Ctx CrucibleType) -> Type +type ExecCont p sym ext rtp f args = + ReaderT (SimState p sym ext rtp f args) IO (ExecState p sym ext rtp) -- | Some additional information attached to a @RunningState@ -- that indicates how we got to this running state. +-- +-- Type parameters: +-- +-- - @blocks@: types of variables in scope from previous blocks +-- - @args@: arguments to this block +type RunningStateInfo :: Ctx (Ctx CrucibleType) -> Ctx CrucibleType -> Type data RunningStateInfo blocks args -- | This indicates that we are now in a @RunningState@ because -- we transferred execution to the start of a basic block. @@ -554,6 +720,12 @@ -- | A 'ResolvedJump' is a block label together with a collection of -- actual arguments that are expected by that block. These data -- are sufficient to actually transfer control to the named label. +-- +-- Type parameters: +-- +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @blocks@: types of variables in scope from previous blocks +type ResolvedJump :: Type -> Ctx (Ctx CrucibleType) -> Type data ResolvedJump sym blocks = forall args. ResolvedJump @@ -564,6 +736,15 @@ -- (while it first explores other paths), a 'ControlResumption' -- indicates what actions must later be taken in order to resume -- execution of that path. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +type ControlResumption :: Type -> Type -> Type -> Type -> Type -> Type data ControlResumption p sym ext rtp f where {- | When resuming a paused frame with a @ContinueResumption@, no special work needs to be done, simply begin executing @@ -603,6 +784,15 @@ -- while other paths are explored. It consists of a (potentially partial) -- 'SimFrame' together with some information about how to resume execution -- of that frame. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +type PausedFrame :: Type -> Type -> Type -> Type -> Type -> Type data PausedFrame p sym ext rtp f = forall old_args. PausedFrame @@ -619,6 +809,16 @@ -- stored in the 'VFFCompletePath' state until the second path also -- reaches its merge point. The two paths will then be merged, -- and execution will continue beyond the merge point. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +-- - @args@: arguments to this frame (see 'SimFrame') +type VFFOtherPath :: Type -> Type -> Type -> Type -> Type -> Maybe (Ctx CrucibleType) -> Type data VFFOtherPath p sym ext ret f args {- | This corresponds the a path that still needs to be analyzed. -} @@ -639,20 +839,17 @@ of the branching structure of a program. The 'ValueFromFrame' states correspond to the structure of symbolic branching that occurs within a single function call. -The type parameters have the following meanings: - - * @p@ is the personality of the simulator (i.e., custom user state). - - * @sym@ is the simulator backend being used. - - * @ext@ specifies what extensions to the Crucible language are enabled - - * @ret@ is the global return type of the entire execution. +Type parameters: - * @f@ is the type of the top frame. +- @p@: see 'cruciblePersonality' +- @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +- @ext@: language extension, see "Lang.Crucible.CFG.Extension" +- @ret@: global return type of the entire execution +- @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') -} -data ValueFromFrame p sym ext (ret :: Type) (f :: Type) +type ValueFromFrame :: Type -> Type -> Type -> Type -> Type -> Type +data ValueFromFrame p sym ext ret f {- | We are working on a branch; this could be the first or the second of both branches (see the 'VFFOtherPath' field). -} @@ -715,6 +912,7 @@ -- occur or not. If the context sill expects a merge, we need to -- take some actions to indicate that the merge will not occur; -- otherwise there is no special work to be done. +type PendingPartialMerges :: Type data PendingPartialMerges = {- | Don't indicate an abort condition in the context -} NoNeedToAbort @@ -728,19 +926,14 @@ of the branching structure of a program. The 'ValueFromValue' states correspond to stack call frames in a more traditional simulator environment. -The type parameters have the following meanings: - - * @p@ is the personality of the simulator (i.e., custom user state). - - * @sym@ is the simulator backend being used. - - * @ext@ specifies what extensions to the Crucible language are enabled - - * @ret@ is the global return type of the entire computation - - * @top_return@ is the return type of the top-most call on the stack. +- @p@: see 'cruciblePersonality' +- @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +- @ext@: language extension, see "Lang.Crucible.CFG.Extension" +- @ret@: global return type of the entire execution +- @top_return@: return type of the top-most call on the stack. -} -data ValueFromValue p sym ext (ret :: Type) (top_return :: CrucibleType) +type ValueFromValue :: Type -> Type -> Type -> Type -> CrucibleType -> Type +data ValueFromValue p sym ext ret top_return {- | 'VFVCall' denotes a call site in the outer context, and represents the point to which a function higher on the stack will @@ -851,23 +1044,18 @@ executing in a caller's context once a function call has completed and the return value is available. -The type parameters have the following meanings: - - * @ret@ is the type of the return value that is expected. - - * @p@ is the personality of the simulator (i.e., custom user state). - - * @sym@ is the simulator backend being used. - - * @ext@ specifies what extensions to the Crucible language are enabled. - - * @root@ is the global return type of the entire computation. - - * @f@ is the stack type of the caller. +Type parameters: - * @args@ is the type of the local variables in scope prior to the call. +- @ret@: the type of the return value that is expected +- @p@: see 'cruciblePersonality' +- @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +- @ext@: language extension, see "Lang.Crucible.CFG.Extension" +- @root@: global return type of the entire computation +- @f@: the frame type of the caller ('CrucibleLang' or 'OverrideLang') +- @args@: types of the local variables in scope prior to the call (see 'SimFrame') -} -data ReturnHandler (ret :: CrucibleType) p sym ext root f args where +type ReturnHandler :: CrucibleType -> Type -> Type -> Type -> Type -> Type -> Maybe (Ctx CrucibleType) -> Type +data ReturnHandler ret p sym ext root f args where {- | The 'ReturnToOverride' constructor indicates that the calling context is primitive code written directly in Haskell. -} @@ -899,13 +1087,25 @@ ------------------------------------------------------------------------ -- ActiveTree +type PartialResultFrame :: Type -> Type -> Type -> Maybe (Ctx CrucibleType) -> Type type PartialResultFrame sym ext f args = PartialResult sym ext (SimFrame sym ext f args) {- | An active execution tree contains at least one active execution. The data structure is organized so that the current execution - can be accessed rapidly. -} -data ActiveTree p sym ext root (f :: Type) args + can be accessed rapidly. + + Type parameters: + + - @p@: see 'cruciblePersonality' + - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' + - @ext@: language extension, see "Lang.Crucible.CFG.Extension" + - @root@: global return type of the entire computation + - @f@: the frame type of the caller ('CrucibleLang' or 'OverrideLang') +-- - @args@: arguments to the current frame (see 'SimFrame') +-} +type ActiveTree :: Type -> Type -> Type -> Type -> Type -> Maybe (Ctx.Ctx CrucibleType) -> Type +data ActiveTree p sym ext root f args = ActiveTree { _actContext :: !(ValueFromFrame p sym ext root f) , _actResult :: !(PartialResultFrame sym ext f args) @@ -960,6 +1160,15 @@ -- SimContext -- | A definition of a function's semantics, given as a Haskell action. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @args@: types of arguments to the override +-- - @ret@: return type of the override +type Override :: Type -> Type -> Type -> Ctx CrucibleType -> CrucibleType -> Type data Override p sym ext (args :: Ctx CrucibleType) ret = Override { overrideName :: FunctionName , overrideHandler :: forall r. ExecCont p sym ext r (OverrideLang ret) ('Just args) @@ -968,16 +1177,39 @@ -- | State used to indicate what to do when function is called. A function -- may either be defined by writing a Haskell 'Override' or by giving -- a Crucible control-flow graph representation. -data FnState p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType) +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @args@: argument types +-- - @ret@: return type +type FnState :: Type -> Type -> Type -> Ctx CrucibleType -> CrucibleType -> Type +data FnState p sym ext args ret = UseOverride !(Override p sym ext args ret) | forall blocks . UseCFG !(CFG ext blocks args ret) !(CFGPostdom blocks) -- | A map from function handles to their semantics. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +type FunctionBindings :: Type -> Type -> Type -> Type newtype FunctionBindings p sym ext = FnBindings { fnBindings :: FnHandleMap (FnState p sym ext) } -- | The type of functions that interpret extension statements. These -- have access to the main simulator state, and can make fairly arbitrary -- changes to it. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +type EvalStmtFunc :: Type -> Type -> Type -> Type type EvalStmtFunc p sym ext = forall rtp blocks r ctx tp'. StmtExtension ext (RegEntry sym) tp' -> @@ -987,6 +1219,13 @@ -- | In order to start executing a simulator, one must provide an implementation -- of the extension syntax. This includes an evaluator for the added -- expression forms, and an evaluator for the added statement forms. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +type ExtensionImpl :: Type -> Type -> Type -> Type data ExtensionImpl p sym ext = ExtensionImpl { extensionEval :: @@ -1010,8 +1249,17 @@ , extensionExec = \case } +type IsSymInterfaceProof :: Type -> Type -> Type type IsSymInterfaceProof sym a = (IsSymInterface sym => a) -> a +-- | Some kind of 'Integer' to be collected during execution. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +type Metric :: Type -> Type -> Type -> Type newtype Metric p sym ext = Metric { runMetric :: forall rtp f args. SimState p sym ext rtp f args -> IO Integer @@ -1021,7 +1269,14 @@ -- remains persistent across all symbolic simulator actions. In particular, it -- is not rolled back when the simulator returns previous program points to -- explore additional paths, etc. -data SimContext (personality :: Type) (sym :: Type) (ext :: Type) +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +type SimContext :: Type -> Type -> Type -> Type +data SimContext p sym ext = SimContext { _ctxBackend :: !(SomeBackend sym) -- | Class dictionary for @'IsSymInterface' sym@ , ctxSolverProof :: !(forall a . IsSymInterfaceProof sym a) @@ -1030,10 +1285,11 @@ , simHandleAllocator :: !(HandleAllocator) -- | Handle to write messages to. , printHandle :: !Handle - , extensionImpl :: ExtensionImpl personality sym ext - , _functionBindings :: !(FunctionBindings personality sym ext) - , _cruciblePersonality :: !personality - , _profilingMetrics :: !(Map Text (Metric personality sym ext)) + , extensionImpl :: ExtensionImpl p sym ext + , _functionBindings :: !(FunctionBindings p sym ext) + -- | See 'cruciblePersonality'. + , _cruciblePersonality :: !p + , _profilingMetrics :: !(Map Text (Metric p sym ext)) } -- | Create a new 'SimContext' with the given bindings. @@ -1075,7 +1331,30 @@ functionBindings :: Lens' (SimContext p sym ext) (FunctionBindings p sym ext) functionBindings = lens _functionBindings (\s v -> s { _functionBindings = v }) --- | Access the custom user-state inside the 'SimContext'. +-- | Custom state inside the 'SimContext'. +-- +-- Crucible itself is entirely polymorphic over @p@. Downstream applications can +-- instantiate it to any sort of state that they would like to associate with a +-- 'SimContext'. +-- +-- For example, applications based on +-- [@macaw-symbolic@](https://github.com/GaloisInc/macaw/tree/master/symbolic) +-- can instantiate this to a structure holding enough information to perform +-- incremental code discovery. See @ambient-verifier@'s +-- [@AmbientSimulatorState@](https://github.com/GaloisInc/ambient-verifier/blob/eab04abb9750825a25ec0cbe0379add63f05f6c6/src/Ambient/Extensions.hs#L1092-1137). +-- +-- Code that needs to store some state in the personality but doesn\'t wish to +-- fix a particular type can use the \"classy lenses\" approach, e.g., +-- +-- @ +-- class HasFooState p where +-- fooState :: `Lens'` p FooState +-- @ +-- +-- For examples of this approach, see +-- +-- * [@HasMacawLazySimulatorState@](https://github.com/GaloisInc/macaw/blob/cbec559b428fdd194398d07fc08c8c570a1d3bab/symbolic/src/Data/Macaw/Symbolic/MemOps.hs#L385-L394) +-- * [@HasGreaseSimulatorState@](https://github.com/GaloisInc/grease/blob/a50d54d2f414d15974dcf2d21654fbfe3527f0fa/src/Grease/Macaw/SimulatorState.hs#L90-L97) cruciblePersonality :: Lens' (SimContext p sym ext) p cruciblePersonality = lens _cruciblePersonality (\s v -> s{ _cruciblePersonality = v }) @@ -1094,6 +1373,13 @@ -- may be desirable to take additional or alternate actions on abort -- events; in which case, the library user may replace the default -- abort handler with their own. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value newtype AbortHandler p sym ext rtp = AH { runAH :: forall (l :: Type) args. AbortExecReason -> @@ -1103,12 +1389,23 @@ -- | A SimState contains the execution context, an error handler, and -- the current execution tree. It captures the entire state -- of the symbolic simulator. -data SimState p sym ext rtp f (args :: Maybe (Ctx.Ctx CrucibleType)) +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +-- - @args@: arguments to the current frame (see 'SimFrame') +type SimState :: Type -> Type -> Type -> Type -> Type -> Maybe (Ctx.Ctx CrucibleType) -> Type +data SimState p sym ext rtp f args = SimState { _stateContext :: !(SimContext p sym ext) , _abortHandler :: !(AbortHandler p sym ext rtp) , _stateTree :: !(ActiveTree p sym ext rtp f args) } +type SomeSimState :: Type -> Type -> Type -> Type -> Type data SomeSimState p sym ext rtp = forall f args. SomeSimState !(SimState p sym ext rtp f args) diff --git a/src/Lang/Crucible/Simulator/Operations.hs b/src/Lang/Crucible/Simulator/Operations.hs --- a/src/Lang/Crucible/Simulator/Operations.hs +++ b/src/Lang/Crucible/Simulator/Operations.hs @@ -125,8 +125,8 @@ AbortedResult sym ext -> AbortedResult sym ext -> AbortedResult sym ext -mergeAbortedResult _ _ (AbortedExit ec) _ = AbortedExit ec -mergeAbortedResult _ _ _ (AbortedExit ec) = AbortedExit ec +mergeAbortedResult _ _ ae@(AbortedExit {}) _ = ae +mergeAbortedResult _ _ _ ae@(AbortedExit {}) = ae mergeAbortedResult loc pred q r = AbortedBranch loc pred q r mergePartialAndAbortedResult :: diff --git a/src/Lang/Crucible/Simulator/OverrideSim.hs b/src/Lang/Crucible/Simulator/OverrideSim.hs --- a/src/Lang/Crucible/Simulator/OverrideSim.hs +++ b/src/Lang/Crucible/Simulator/OverrideSim.hs @@ -75,8 +75,10 @@ , useIntrinsic -- * Typed overrides , TypedOverride(..) + , typedOverride , SomeTypedOverride(..) , runTypedOverride + , bindTypedOverride -- * Re-exports , Lang.Crucible.Simulator.ExecutionTree.Override ) where @@ -89,7 +91,7 @@ import Control.Monad.Reader (ReaderT(..)) import Control.Monad.ST import Control.Monad.State.Strict (StateT(..)) -import Data.List (foldl') +import qualified Data.Foldable as Foldable import qualified Data.Parameterized.Context as Ctx import Data.Proxy import qualified Data.Text as T @@ -135,7 +137,7 @@ -- -- Type parameters: -- --- * 'p' the "personality", i.e. user-defined state parameterized by @sym@ +-- * 'p' see 'Lang.Crucible.Simulator.ExecutionTree.cruciblePersonality' -- * 'sym' the symbolic backend -- * 'ext' the syntax extension ("Lang.Crucible.CFG.Extension") -- * 'rtp' global return type @@ -156,8 +158,14 @@ -- | Exit from the current execution by ignoring the continuation -- and immediately returning an aborted execution result. exitExecution :: IsSymInterface sym => ExitCode -> OverrideSim p sym ext rtp args r a -exitExecution ec = Sim $ StateContT $ \_c s -> - return $ ResultState $ AbortedResult (s^.stateContext) (AbortedExit ec) +exitExecution ec = do + ActiveTree _ctx ar0 <- use stateTree + let gp = + case ar0 of + TotalRes e -> e + PartialRes _loc _pred ex _ar1 -> ex + Sim $ StateContT $ \_c s -> + return $ ResultState $ AbortedResult (s^.stateContext) (AbortedExit ec gp) bindOverrideSim :: OverrideSim p sym ext rtp args r a -> @@ -627,7 +635,7 @@ -- | Build a map of function bindings from a list of -- handle/binding pairs. fnBindingsFromList :: [FnBinding p sym ext] -> FunctionBindings p sym ext -fnBindingsFromList = foldl' insertFnBinding $ FnBindings emptyHandleMap +fnBindingsFromList = Foldable.foldl' insertFnBinding $ FnBindings emptyHandleMap registerFnBinding :: FnBinding p sym ext -> OverrideSim p sym ext rtp a r () @@ -690,6 +698,21 @@ , typedOverrideRet :: TypeRepr ret } +-- | Create a 'TypedOverride' with a statically-known signature +typedOverride :: + KnownRepr (Ctx.Assignment TypeRepr) args => + KnownRepr TypeRepr ret => + (forall rtp args' ret'. + Ctx.Assignment (RegValue' sym) args -> + OverrideSim p sym ext rtp args' ret' (RegValue sym ret)) -> + TypedOverride p sym ext args ret +typedOverride handler = + TypedOverride + { typedOverrideHandler = handler + , typedOverrideArgs = knownRepr + , typedOverrideRet = knownRepr + } + -- | A 'TypedOverride' with the type parameters @args@, @ret@ existentially -- quantified data SomeTypedOverride p sym ext = @@ -703,3 +726,11 @@ runTypedOverride nm typedOvr = mkOverride' nm (typedOverrideRet typedOvr) $ do RegMap args <- getOverrideArgs typedOverrideHandler typedOvr (fmapFC (RV . regValue) args) + +-- | Bind a 'TypedOverride' to a 'FnHandle' +bindTypedOverride :: + FnHandle args ret -> + TypedOverride p sym ext args ret -> + OverrideSim p sym ext rtp args' ret' () +bindTypedOverride hdl ov = + bindFnHandle hdl (UseOverride (runTypedOverride (handleName hdl) ov)) diff --git a/src/Lang/Crucible/Simulator/PathSatisfiability.hs b/src/Lang/Crucible/Simulator/PathSatisfiability.hs --- a/src/Lang/Crucible/Simulator/PathSatisfiability.hs +++ b/src/Lang/Crucible/Simulator/PathSatisfiability.hs @@ -5,7 +5,7 @@ -- at symbolic branch points -- Copyright : (c) Galois, Inc 2018 -- License : BSD3 --- Maintainer : Rob Dockins +-- Maintainer : Ryan Scott , Langston Barrett -- Stability : provisional ------------------------------------------------------------------------ {-# LANGUAGE DataKinds #-} @@ -54,14 +54,20 @@ (Just (ConcreteBool True)) ] - +-- | Prune unsatisfiable execution traces during simulation. +-- +-- At every symbolic branch point, an SMT solver is queried to determine if one +-- or both symbolic branches are unsatisfiable. Only branches with satisfiable +-- branch conditions are explored. pathSatisfiabilityFeature :: forall sym. IsSymInterface sym => sym -> - (Maybe ProgramLoc -> Pred sym -> IO BranchResult) - {- ^ An action for considering the satisfiability of a predicate. - In the current state of the symbolic interface, indicate what - we can determine about the given predicate. -} -> + -- | An action for considering the satisfiability of a predicate. In the + -- current state of the symbolic interface, indicate what we can determine + -- about the given predicate. + -- + -- Usually, this is set to 'Lang.Crucible.Backend.Online.considerSatisfiability'. + (Maybe ProgramLoc -> Pred sym -> IO BranchResult) -> IO (GenericExecutionFeature sym) pathSatisfiabilityFeature sym considerSatisfiability = do tryExtendConfig pathSatOptions (getConfiguration sym) diff --git a/src/Lang/Crucible/Simulator/RecordAndReplay.hs b/src/Lang/Crucible/Simulator/RecordAndReplay.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Simulator/RecordAndReplay.hs @@ -0,0 +1,365 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} + +module Lang.Crucible.Simulator.RecordAndReplay ( + HasRecordState(..), + RecordState, + mkRecordState, + HasReplayState(..), + ReplayState, + mkReplayState, + recordTraceLength, + replayTraceLength, + RecordedTrace, + getRecordedTrace, + recordFeature, + replayFeature, + initialTrace, + traceGlobal, + emptyRecordedTrace +) where + +import Control.Exception qualified as X +import Control.Lens ((%~), (&), (^.)) +import Control.Lens qualified as Lens +import Data.Foldable qualified as F +import Data.Kind (Type) +import Data.Text qualified as Text +import Data.Sequence qualified as Seq +import Lang.Crucible.Backend qualified as CB +import Lang.Crucible.CFG.Core qualified as C +import Lang.Crucible.FunctionHandle qualified as C +import Lang.Crucible.Panic (panic) +import Lang.Crucible.Simulator qualified as C +import Lang.Crucible.Simulator.EvalStmt qualified as C +import Lang.Crucible.Simulator.ExecutionTree qualified as C +import Lang.Crucible.Simulator.GlobalState qualified as C +import Lang.Crucible.Simulator.SymSequence qualified as CSSS +import Lang.Crucible.Types qualified as CT +import What4.Interface qualified as W4 +import What4.Partial qualified as W4P + +-- | A trace consists of the 'W4.ProgramLoc's returned by +-- 'W4.getCurrentProgramLoc' in 'C.RunningState's during symbolic execution. +-- +-- Intentionally not part of the API so as to keep the implementation abstract. +type TraceType = CT.SequenceType (CT.StringType W4.Unicode) + +-- | Type parameters: +-- +-- * @p@: see 'C.cruciblePersonality' +-- * @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- * @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- * @rtp@: type of the simulator return value +type RecordState :: Type -> Type -> Type -> Type -> Type +newtype RecordState p sym ext rtp + = RecordState (C.GlobalVar TraceType) + -- ^ constructor intentionally not exported + +{- | A trace from 'recordFeature', processed and ready for consumption by +'replayFeature'. +-} +newtype RecordedTrace sym + = RecordedTrace (C.RegValue sym TraceType) + +-- | Type parameters: +-- +-- * @p@: see 'C.cruciblePersonality' +-- * @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- * @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- * @rtp@: type of the simulator return value +type ReplayState :: Type -> Type -> Type -> Type -> Type +data ReplayState p sym ext rtp + = ReplayState + { _traceGlobal :: (C.GlobalVar TraceType) + , _initialTrace :: (RecordedTrace sym) + } + -- ^ constructor intentionally not exported +Lens.makeLenses ''ReplayState + +-- | Constructor for 'RecordState' +mkRecordState :: + C.HandleAllocator -> IO (RecordState p sym ext rtp) +mkRecordState halloc = + RecordState <$> C.freshGlobalVar halloc "recordState" W4.knownRepr + +-- | Constructor for 'ReplayState' +mkReplayState :: + C.HandleAllocator -> RecordedTrace sym -> IO (ReplayState p sym ext rtp) +mkReplayState halloc rt = + ReplayState <$> C.freshGlobalVar halloc "replayState" W4.knownRepr <*> pure rt + +-- | A class for Crucible personality types @p@ which contain a +-- 'RecordState'. This execution feature is polymorphic over +-- 'RecordState' so that downstream users can supply their own +-- personality types that extend 'RecordState' further. +class HasRecordState p r sym ext rtp | p -> r sym ext rtp where + recordState :: Lens.Lens' p (RecordState r sym ext rtp) + +instance HasRecordState (RecordState p sym ext rtp) p sym ext rtp where + recordState = id + {-# INLINE recordState #-} + +-- | A class for Crucible personality types @p@ which contain a +-- 'ReplayState'. This execution feature is polymorphic over +-- 'ReplayState' so that downstream users can supply their own +-- personality types that extend 'ReplayState' further. +class HasReplayState p r sym ext rtp | p -> r sym ext rtp where + replayState :: Lens.Lens' p (ReplayState r sym ext rtp) + +instance HasReplayState (ReplayState p sym ext rtp) p sym ext rtp where + replayState = id + {-# INLINE replayState #-} + +data TraceGlobalNotDefined = TraceGlobalNotDefined + +instance Show TraceGlobalNotDefined where + show _ = "record and replay trace global not defined" + +instance X.Exception TraceGlobalNotDefined + +locAsStr :: + W4.IsExprBuilder sym => + sym -> + IO (C.RegValue sym (CT.StringType W4.Unicode)) +locAsStr sym = do + loc <- W4.getCurrentProgramLoc sym + let txtLoc = Text.pack (show loc) + W4.stringLit sym (W4.UnicodeLiteral txtLoc) + +emptyRecordedTrace :: sym -> IO (RecordedTrace sym) +emptyRecordedTrace sym = RecordedTrace <$> CSSS.nilSymSequence sym + +getRecordTrace :: + HasRecordState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + Maybe (C.RegValue sym TraceType) +getRecordTrace simState = do + let ctx = simState ^. C.stateContext + let RecordState g = ctx ^. C.cruciblePersonality . recordState + C.lookupGlobal g (simState ^. C.stateGlobals) + +-- | Get the length of the currently recorded trace +recordTraceLength :: + W4.IsExprBuilder sym => + HasRecordState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + IO (Maybe (W4.SymNat sym)) +recordTraceLength simState = do + let sym = simState ^. C.stateSymInterface + case getRecordTrace simState of + Nothing -> pure Nothing + Just s -> Just <$> CSSS.lengthSymSequence sym s + +getReplayTrace :: + HasReplayState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + Maybe (C.RegValue sym TraceType) +getReplayTrace simState = do + let ctx = simState ^. C.stateContext + let g = ctx ^. C.cruciblePersonality . replayState . traceGlobal + C.lookupGlobal g (simState ^. C.stateGlobals) + +-- | Get the length of the trace being replayed +replayTraceLength :: + W4.IsExprBuilder sym => + HasReplayState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + IO (Maybe (W4.SymNat sym)) +replayTraceLength simState = do + let sym = simState ^. C.stateSymInterface + case getReplayTrace simState of + Nothing -> pure Nothing + Just s -> Just <$> CSSS.lengthSymSequence sym s + +-- | An 'C.ExecutionFeature' to record traces. +-- +-- During execution this logs program locations to a Crucible global variable. +-- After execution, this variable may be read with 'getRecordedTrace' and the +-- 'RecordedTrace' can be passed to 'replayFeature' to \"replay\" it, i.e., to +-- abort all branches that deviate from it. +-- +-- If this is not called with 'C.InitialState' before any other 'C.ExecState', +-- it may throw a 'TraceGlobalNotDefined' exception. +recordFeature :: + ( HasRecordState p p sym ext rtp + , W4.IsExprBuilder sym + ) => + C.ExecutionFeature p sym ext rtp +recordFeature = + C.ExecutionFeature $ + \case + C.InitialState simCtx globals abortHandler retTy cont -> do + globals' <- insertNewTrace simCtx globals + let iState = C.InitialState simCtx globals' abortHandler retTy cont + return $ C.ExecutionFeatureModifiedState iState + C.RunningState runStateInfo st -> do + loc <- locAsStr (st ^. C.stateSymInterface) + st' <- consTrace st loc + let rState = C.RunningState runStateInfo st' + return $ C.ExecutionFeatureModifiedState rState + _ -> pure C.ExecutionFeatureNoChange + where + insertNewTrace :: + HasRecordState p p sym ext rtp => + C.SimContext p sym ext -> + C.SymGlobalState sym -> + IO (C.SymGlobalState sym) + insertNewTrace simCtx globals = do + let RecordState g = simCtx ^. C.cruciblePersonality . recordState + let sym = simCtx ^. C.ctxSymInterface + nil <- CSSS.nilSymSequence sym + return (C.insertGlobal g nil globals) + + getTraceOrThrow :: + HasRecordState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + IO (C.RegValue sym TraceType) + getTraceOrThrow st = + case getRecordTrace st of + Nothing -> X.throw TraceGlobalNotDefined + Just t -> pure t + + insertTrace :: + HasRecordState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + C.RegValue sym TraceType -> + C.SimState p sym ext rtp f args + insertTrace st v = do + let simCtx = st ^. C.stateContext + let RecordState g = simCtx ^. C.cruciblePersonality . recordState + st & C.stateGlobals %~ C.insertGlobal g v + + consTrace :: + HasRecordState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + C.RegValue sym (CT.StringType W4.Unicode) -> + IO (C.SimState p sym ext rtp f args) + consTrace st v = do + s <- getTraceOrThrow st + let sym = st ^. C.stateSymInterface + s' <- CSSS.consSymSequence sym v s + pure (insertTrace st s') + + + -- ^ constructor intentionally not exported to keep 'TraceType' out of the + -- API, but it could be exported in the future if necessary. + +-- | Obtain a 'RecordedTrace' after execution. +-- +-- This currently requires concretizing the trace, because there is no efficient +-- reverse operation for 'CSSS.SymSequence'. +getRecordedTrace :: + W4.IsExprBuilder sym => + C.SymGlobalState sym -> + RecordState p sym ext rtp -> + sym -> + -- | Evaluation for booleans, usually a 'What4.Expr.GroundEval.GroundEvalFn' + (W4.Pred sym -> IO Bool) -> + IO (RecordedTrace sym) +getRecordedTrace globals (RecordState g) sym evalBool = do + case C.lookupGlobal g globals of + Nothing -> X.throw TraceGlobalNotDefined + Just s -> RecordedTrace <$> concretizeAndReverseTrace s + where + concretizeAndReverseTrace s = do + concretized <- CSSS.concretizeSymSequence evalBool (evalStr sym) s + let reversed = Seq.reverse concretized + symbolized <- mapM (W4.stringLit sym . W4.UnicodeLiteral) reversed + CSSS.fromListSymSequence sym (F.toList symbolized) + + evalStr :: + W4.IsExpr (W4.SymExpr sym) => + sym -> + W4.SymString sym W4.Unicode -> + IO Text.Text + evalStr _sym s = + case W4.asString s of + Just (W4.UnicodeLiteral s') -> pure s' + Nothing -> panic "getRecordedTrace" ["Non-literal trace element?"] + +{- | Inserts a recorded trace into the state's replay trace variable +The replay feature will follow this trace if it is enabled +-} +insertReplayTrace :: + (HasReplayState p p sym ext rtp) => + C.SimState p sym ext rtp f args -> + C.RegValue sym TraceType -> + C.SimState p sym ext rtp f args +insertReplayTrace st v = do + let simCtx = st ^. C.stateContext + let g = simCtx ^. C.cruciblePersonality . replayState . traceGlobal + st & C.stateGlobals %~ C.insertGlobal g v + +-- | An 'C.ExecutionFeature' to replay traces recorded with 'recordFeature'. +-- +-- Branches that deviate from the given trace will be aborted with +-- 'C.InfeasibleBranch'. +-- +-- If this is not called with 'C.InitialState' before any other 'C.ExecState', +-- it may throw a 'TraceGlobalNotDefined' exception. +replayFeature :: + ( HasReplayState p p sym ext rtp + , W4.IsExprBuilder sym + ) => + -- | Whether to stop at the end of the trace. If this is 'True' and execution + -- has exhausted the trace, then any further execution will be aborted via + -- 'C.InfeasibleBranch'. + Bool -> + C.ExecutionFeature p sym ext rtp +replayFeature stop = + C.ExecutionFeature $ + \case + C.InitialState simCtx globals abortHandler retTy cont -> do + let rstate = simCtx ^. C.cruciblePersonality . replayState + let g = rstate ^. traceGlobal + let RecordedTrace trace = rstate ^. initialTrace + let globals' = C.insertGlobal g trace globals + let iState = C.InitialState simCtx globals' abortHandler retTy cont + return $ C.ExecutionFeatureModifiedState iState + C.RunningState runStateInfo st -> do + let sym = st ^. C.stateSymInterface + s <- getTraceOrThrow st + partExpr <- CSSS.unconsSymSequence sym (W4.stringIte sym) s + let badPath = do + loc <- W4.getCurrentProgramLoc sym + let st' = C.AbortState (CB.InfeasibleBranch loc) st + pure (C.ExecutionFeatureNewState st') + case partExpr of + W4P.Unassigned + | stop -> badPath + | otherwise -> pure C.ExecutionFeatureNoChange + W4P.PE valid (expectedLoc, rest) -> + C.withBackend (st ^. C.stateContext) $ \bak -> do + let msg = "Trace must be valid" + CB.assert bak valid (C.AssertFailureSimError msg "") + + currLoc <- locAsStr sym + atExpectedLoc <- W4.stringEq sym currLoc expectedLoc + case W4.asConstantPred atExpectedLoc of + Just False -> badPath + _ -> do + let msg' = "Execution deviated from trace" + CB.assert bak atExpectedLoc (C.AssertFailureSimError msg' "") + let st' = insertReplayTrace st rest + let rState = C.RunningState runStateInfo st' + pure (C.ExecutionFeatureModifiedState rState) + + _ -> pure C.ExecutionFeatureNoChange + where + getTraceOrThrow :: + HasReplayState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + IO (C.RegValue sym TraceType) + getTraceOrThrow st = + case getReplayTrace st of + Nothing -> X.throw TraceGlobalNotDefined + Just t -> pure t diff --git a/src/Lang/Crucible/Simulator/RegValue.hs b/src/Lang/Crucible/Simulator/RegValue.hs --- a/src/Lang/Crucible/Simulator/RegValue.hs +++ b/src/Lang/Crucible/Simulator/RegValue.hs @@ -48,6 +48,8 @@ , muxVector , muxSymSequence , muxHandle + -- * Equality + , eqRegValue ) where import Control.Monad @@ -361,3 +363,41 @@ p (unVB (x Ctx.! i)) (unVB (y Ctx.! i)) + +------------------------------------------------------------------------ +-- Equality + +-- | Equality of 'RegValue's. +-- +-- This is only supported for a few types, see #1582. +eqRegValue :: + forall sym tp. + IsInterpretedFloatExprBuilder sym => + sym -> + TypeRepr tp -> + RegValue sym tp -> + RegValue sym tp -> + IO (Pred sym) +eqRegValue sym tp x y = + case tp of + -- Base types + BoolRepr -> eqPred sym x y + BVRepr _width -> bvEq sym x y + ComplexRealRepr -> cplxEq sym x y + FloatRepr @fi _ -> iFloatEq @_ @fi sym x y + IEEEFloatRepr _fpp -> floatEq sym x y + IntegerRepr -> intEq sym x y + NatRepr -> natEq sym x y + RealValRepr -> realEq sym x y + SymbolicStructRepr _tys -> structEq sym x y + SymbolicArrayRepr _idxs _tp -> arrayEq sym x y + StringRepr _si -> stringEq sym x y + + -- Trivial cases + UnitRepr -> pure (truePred sym) + CharRepr -> + if x == y + then pure (truePred sym) + else pure (falsePred sym) + + _ -> fail ("eqRegValue not supported for " ++ show tp) diff --git a/src/Lang/Crucible/Utils/BitSet.hs b/src/Lang/Crucible/Utils/BitSet.hs --- a/src/Lang/Crucible/Utils/BitSet.hs +++ b/src/Lang/Crucible/Utils/BitSet.hs @@ -35,7 +35,7 @@ import Data.Word import Data.Hashable import qualified Data.List as List -import Prelude hiding (null, foldr, foldl) +import Prelude hiding (null, foldr, foldl, foldl') newtype BitSet a = BitSet { getBits :: Integer } deriving (Show, Eq, Ord) diff --git a/test/helpers/Main.hs b/test/helpers/Main.hs --- a/test/helpers/Main.hs +++ b/test/helpers/Main.hs @@ -1,6 +1,7 @@ {-# LANGUAGE AllowAmbiguousTypes #-} -module Main where +module Main (main) where + import Control.Lens ((^.)) import Data.List (isInfixOf) import Data.Maybe (fromMaybe) @@ -26,9 +27,12 @@ import qualified Panic as P +import qualified SymSequence as S + main :: IO () -main = - defaultMain =<< panicTests +main = do + p <- panicTests + defaultMain (testGroup "crucible" [p, backendTests, S.tests]) mkBackend :: IO (Some SomeBackend) mkBackend = do @@ -81,7 +85,7 @@ c <- W4I.freshConstant sym (W4I.safeSymbol "c") W4I.BaseBoolRepr assumePred bak "assuming c" c d <- W4I.freshConstant sym (W4I.safeSymbol "d") W4I.BaseBoolRepr - LCB.assert bak c (GenericSimError "asserting d") + LCB.assert bak d (GenericSimError "asserting d") (_asmps, mbGoals) <- LCB.popAssumptionFrameAndObligations bak frm [LCB.ProofGoal asmps gl] <- pure (fromMaybe [] (LCB.goalsToList <$> mbGoals)) asmpsPred <- LCB.assumptionsPred sym asmps diff --git a/test/helpers/SymSequence.hs b/test/helpers/SymSequence.hs new file mode 100644 --- /dev/null +++ b/test/helpers/SymSequence.hs @@ -0,0 +1,300 @@ +{-# LANGUAGE EmptyDataDeriving #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} + +module SymSequence (tests) where + +import Control.Monad.IO.Class (liftIO) +import Data.Foldable qualified as F +import Data.List qualified as List +import Data.Maybe qualified as Maybe +import Data.Parameterized.Nonce qualified as Nonce +import Data.Parameterized.Some (Some(Some)) +import Hedgehog (Gen) +import Hedgehog qualified as H +import Hedgehog.Gen qualified as Gen +import Hedgehog.Range qualified as Range +import Lang.Crucible.Backend (SomeBackend(SomeBackend), backendGetSym) +import Lang.Crucible.Backend.Simple (newSimpleBackend) +import Lang.Crucible.Simulator.SymSequence (SymSequence) +import Lang.Crucible.Simulator.SymSequence qualified as S +import Test.Tasty qualified as TT +import Test.Tasty.Hedgehog qualified as TTH +import What4.Expr (EmptyExprBuilderState(EmptyExprBuilderState)) +import What4.Expr.Builder (newExprBuilder) +import What4.FloatMode (FloatModeRepr(FloatIEEERepr)) +import What4.Interface qualified as WI +import What4.Partial qualified as WP + +--------------------------------------------------------------------- +-- Tests + +tests :: TT.TestTree +tests = + TTH.testProperty + "propSame" + -- This is a big API, so we want adequate coverage (default is 100) + (H.withTests 4096 propSame) + +-- | Check that a generated API interaction has the same effect when interpreted +-- with either 'SymSequence' or lists. +propSame :: H.Property +propSame = + H.property $ do + Some (SomeBackend bak) <- liftIO mkBackend + let sym = backendGetSym bak + op <- H.forAll (Gen.sized $ \n -> genList (H.unSize n) Gen.bool) + let l = opList op + s <- liftIO (opSeq sym op) + l' <- liftIO (F.toList <$> asSeq sym s) + l H.=== l' + where + asSeq sym = + S.concretizeSymSequence (pure . asConstPred (Just sym)) pure + +--------------------------------------------------------------------- +-- Helpers + +mkBackend :: IO (Some SomeBackend) +mkBackend = do + sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState Nonce.globalNonceGenerator + Some . SomeBackend <$> newSimpleBackend sym + +-- Requires that the predicate is concrete +asConstPred :: + WI.IsExprBuilder sym => + proxy sym -> + WI.Pred sym -> + Bool +asConstPred _proxy p = + case WI.asConstantPred p of + Just True -> True + Just False -> False + Nothing -> error "non-constant predicate?" + +--------------------------------------------------------------------- +-- Op + +data Elem a deriving Show + +data List a deriving Show + +-- TODO: Replace with `Seq` for performance +type family AsList t where + AsList (List a) = [a] + AsList (Elem a) = a + AsList (Maybe a) = Maybe (AsList a) + AsList (a, b) = (AsList a, AsList b) + AsList a = a + +type family AsSeq sym t where + AsSeq sym (List a) = SymSequence sym a + AsSeq sym (Elem a) = a + AsSeq sym (Maybe a) = Maybe (AsSeq sym a) + AsSeq sym (a, b) = (AsSeq sym a, AsSeq sym b) + AsSeq sym a = a + +-- | An interaction with the 'SymSequence' API +data Op a t where + -- Generic functions + OTrue :: Op a Bool + OFalse :: Op a Bool + OFst :: Op a (l, r) -> Op a l + OSnd :: Op a (l, r) -> Op a r + OElem :: a -> Op a (Elem a) + OFromMaybe :: Op a t -> Op a (Maybe t) -> Op a t + + -- Constructors + ONil :: Op a (List a) + OCons :: Op a (Elem a) -> Op a (List a) -> Op a (List a) + OAppend :: Op a (List a) -> Op a (List a) -> Op a (List a) + OMux :: Op a Bool -> Op a (List a) -> Op a (List a) -> Op a (List a) + + -- Operations + OUncons :: Op a (List a) -> Op a (Maybe (Elem a), (List a)) + OLength :: Op a (List a) -> Op a Integer + -- TODO: isNil, head, tail + +sexp :: [String] -> String +sexp s = '(' : (unwords s ++ ")") + +fun :: String -> [String] -> String +fun f s = sexp (f:s) + +fun1 :: Show a => String -> a -> String +fun1 f a = fun f [show a] + +fun2 :: (Show a, Show b) => String -> a -> b -> String +fun2 f a b = fun f [show a, show b] + +fun3 :: (Show a, Show b, Show c) => String -> a -> b -> c -> String +fun3 f a b c = fun f [show a, show b, show c] + +instance Show a => Show (Op a t) where + show = + \case + -- Generic functions + OTrue -> "true" + OFalse -> "false" + OFst t -> fun1 "fst" t + OSnd t -> fun1 "snd" t + OElem a -> show a + OFromMaybe a m -> fun2 "fromMaybe" a m + + -- Constructors + ONil -> "nil" + OCons l r -> fun2 "cons" l r + OAppend l r -> fun2 "append" l r + OMux b l r -> fun3 "mux" b l r + + -- Operations + OUncons l -> fun1 "uncons" l + OLength l -> fun1 "length" l + +--------------------------------------------------------------------- +-- Generating Op + +genBool :: Gen (Op a Bool) +genBool = + Gen.choice + [ pure OTrue + , pure OFalse + ] + +genElem :: + Int -> + Gen a -> + Gen (Op a (Elem a)) +genElem sz genA = + if sz <= 0 + then OElem <$> genA + else + Gen.choice + [ OElem <$> genA + , OFromMaybe + <$> genElem (sz - 1) genA + <*> (OFst <$> (OUncons <$> genList (sz - 1) genA)) + ] + +genList :: + Int -> + Gen a -> + Gen (Op a (List a)) +genList sz genA = + if sz <= 0 + then pure ONil + else + Gen.choice + [ genCons + , genAppend + , genMux + ] + where + sub1 = genList (sz - 1) genA + sub2 = do + let budget = max 0 (sz - 1) + bl <- Gen.integral (Range.linear 0 budget) + let br = max 0 (budget - bl) + l <- genList bl genA + r <- genList br genA + pure (l, r) + + genCons = OCons <$> genElem (sz - 1) genA <*> sub1 + + genAppend = uncurry OAppend <$> sub2 + + genMux = do + b <- genBool + uncurry (OMux b) <$> sub2 + +--------------------------------------------------------------------- +-- Interpreting Op + +opList :: Op a t -> AsList t +opList = + \case + -- Generic functions + OTrue -> True + OFalse -> False + OFst t -> fst (opList t) + OSnd t -> snd (opList t) + OElem a -> a + OFromMaybe a m -> Maybe.fromMaybe (opList a) (opList m) + + -- Constructors + ONil -> [] + OCons a l -> opList a : opList l + OAppend l r -> opList l ++ opList r + OMux b l r -> if opList b then opList l else opList r + + -- Operations + OUncons l -> + let l' = opList l in + case List.uncons l' of + Just (hd, tl) -> (Just hd, tl) + Nothing -> (Nothing, l') + OLength l -> fromIntegral @Int @Integer (length (opList l)) -- safe + +opSeq :: + WI.IsExprBuilder sym => + sym -> + Op a t -> + IO (AsSeq sym t) +opSeq sym = + \case + -- Generic functions + OTrue -> pure True + OFalse -> pure False + OFst t -> fst <$> opSeq sym t + OSnd t -> snd <$> opSeq sym t + OElem a -> pure a + OFromMaybe a m -> + Maybe.fromMaybe + <$> opSeq sym a + <*> opSeq sym m + + -- Constructors + ONil -> pure S.SymSequenceNil + OCons a l -> + S.SymSequenceCons + <$> Nonce.freshNonce Nonce.globalNonceGenerator + <*> opSeq sym a + <*> opSeq sym l + OAppend l r -> + S.SymSequenceAppend + <$> Nonce.freshNonce Nonce.globalNonceGenerator + <*> opSeq sym l + <*> opSeq sym r + OMux b l r -> do + b' <- opSeq sym b + let b'' = if b' then WI.truePred sym else WI.falsePred sym + S.SymSequenceMerge + <$> Nonce.freshNonce Nonce.globalNonceGenerator + <*> pure b'' + <*> opSeq sym l + <*> opSeq sym r + + -- Operations + OUncons l -> do + l' <- opSeq sym l + let interpPred p x y = + if asConstPred (Just sym) p + then pure x + else pure y + pe <- S.unconsSymSequence sym interpPred l' + case pe of + WP.Unassigned -> pure (Nothing, l') + WP.PE _ (hd, tl) -> -- TODO: assert pred is truePred + pure (Just hd, tl) + OLength s -> do + l <- S.lengthSymSequence sym =<< opSeq sym s + case WI.asInteger (WI.natToIntegerPure l) of + Just l' -> pure l' + Nothing -> error "SymSequence: symbolic length"