crucible 0.7.2 → 0.8.0.0

raw patch · 22 files changed

+1976/−443 lines, 22 filesdep +hedgehogdep +tasty-hedgehogdep ~basenew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies added: hedgehog, tasty-hedgehog

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.md +17/−0
• crucible.cabal +7/−3
• src/Lang/Crucible/Backend.hs +27/−2
• src/Lang/Crucible/Backend/AssumptionStack.hs +16/−15
• src/Lang/Crucible/Backend/Assumptions.hs +67/−4
• src/Lang/Crucible/Backend/Goals.hs +32/−0
• src/Lang/Crucible/Backend/Online.hs +219/−236
• src/Lang/Crucible/Backend/ProofGoals.hs +96/−4
• src/Lang/Crucible/Backend/Simple.hs +9/−6
• src/Lang/Crucible/Concretize.hs +273/−28
• src/Lang/Crucible/Simulator/BoundedExec.hs +44/−35
• src/Lang/Crucible/Simulator/BoundedRecursion.hs +40/−30
• src/Lang/Crucible/Simulator/CallFrame.hs +7/−1
• src/Lang/Crucible/Simulator/ExecutionTree.hs +358/−61
• src/Lang/Crucible/Simulator/Operations.hs +2/−2
• src/Lang/Crucible/Simulator/OverrideSim.hs +36/−5
• src/Lang/Crucible/Simulator/PathSatisfiability.hs +12/−6
• src/Lang/Crucible/Simulator/RecordAndReplay.hs +365/−0
• src/Lang/Crucible/Simulator/RegValue.hs +40/−0
• src/Lang/Crucible/Utils/BitSet.hs +1/−1
• test/helpers/Main.hs +8/−4
• test/helpers/SymSequence.hs +300/−0

@@ -1,3 +1,20 @@+# 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.

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crucible-Version:       0.7.2+Version:       0.8.0.0 Author:        Galois Inc. Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com Copyright:     (c) Galois, Inc 2014-2022@@ -45,7 +45,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,@@ -117,6 +117,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 +164,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

@@ -4,8 +4,8 @@ License     : BSD3 Maintainer  : Joe Hendrix <jhendrix@galois.com> -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+        ]+    ]

@@ -4,17 +4,16 @@ License     : BSD3 Maintainer  : Rob Dockins <rdockins@galois.com> -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

@@ -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

@@ -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.

@@ -4,19 +4,26 @@ -- Description : A solver backend that maintains a persistent connection -- Copyright   : (c) Galois, Inc 2015-2016 -- License     : BSD3--- Maintainer  : Joe Hendrix <jhendrix@galois.com>+-- Maintainer  : Ryan Scott <rscott@galois.com>, Langston Barrett <langston@galois.com> -- 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

@@ -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

@@ -4,13 +4,13 @@ -- Description : The "simple" solver backend -- Copyright   : (c) Galois, Inc 2015-2016 -- License     : BSD3--- Maintainer  : Rob Dockins <rdockins@galois.com>+-- Maintainer  : Ryan Scott <rscott@galois.com>, Langston Barrett <langston@galois.com> -- 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))

@@ -7,15 +7,27 @@ -- Maintainer       : Langston Barrett <langston@galois.com> -- 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

@@ -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)) 

@@ -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

@@ -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)

@@ -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) 

@@ -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 ::

@@ -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))

@@ -5,7 +5,7 @@ --                    at symbolic branch points -- Copyright        : (c) Galois, Inc 2018 -- License          : BSD3--- Maintainer       : Rob Dockins <rdockins@galois.com>+-- Maintainer       : Ryan Scott <rscott@galois.com>, Langston Barrett <langston@galois.com> -- 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)

@@ -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

@@ -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)

@@ -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)

@@ -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

@@ -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"