crucible 0.7 → 0.7.1

raw patch · 17 files changed

+1565/−269 lines, 17 filesdep +asyncdep ~basedep ~th-abstractiondep ~what4new-uploaderPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: async

Dependency ranges changed: base, th-abstraction, what4

API changes (from Hackage documentation)

Files

• CHANGELOG.md +6/−0
• crucible.cabal +11/−3
• src/Lang/Crucible/Analysis/Fixpoint/Components.hs +18/−0
• src/Lang/Crucible/Backend.hs +91/−250
• src/Lang/Crucible/Backend/Assumptions.hs +268/−0
• src/Lang/Crucible/Backend/ProofGoals.hs +1/−1
• src/Lang/Crucible/Backend/Prove.hs +455/−0
• src/Lang/Crucible/CFG/Expr.hs +0/−1
• src/Lang/Crucible/Concretize.hs +607/−0
• src/Lang/Crucible/FunctionHandle.hs +15/−0
• src/Lang/Crucible/Simulator/EvalStmt.hs +0/−1
• src/Lang/Crucible/Simulator/Evaluation.hs +2/−2
• src/Lang/Crucible/Simulator/Profiling.hs +6/−1
• src/Lang/Crucible/Simulator/SymSequence.hs +28/−0
• src/Lang/Crucible/Types.hs +1/−10
• src/Lang/Crucible/Utils/Seconds.hs +18/−0
• src/Lang/Crucible/Utils/Timeout.hs +38/−0

@@ -1,3 +1,9 @@+# 0.7.1 -- 2024-08-30++* Add support for GHC 9.8++* Deprecate `concreteizeSymSequence` in favor of `concretizeSymSequence`+ # 0.7 -- 2024-02-05  * Add `TypedOverride`, `SomeTypedOverride`, and `runTypedOverride` to

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crucible-Version:       0.7+Version:       0.7.1 Author:        Galois Inc. Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com Copyright:     (c) Galois, Inc 2014-2022@@ -44,7 +44,8 @@ library   import: bldflags   build-depends:-    base >= 4.13 && < 4.19,+    async,+    base >= 4.13 && < 4.20,     bimap,     bv-sized >= 1.0.0 && < 1.1,     containers >= 0.5.9.0,@@ -60,7 +61,7 @@     template-haskell,     text,     time >= 1.8 && < 2.0,-    th-abstraction >=0.1 && <0.6,+    th-abstraction >=0.1 && <0.7,     transformers,     unordered-containers,     vector,@@ -72,6 +73,9 @@    hs-source-dirs: src +  other-modules:+    Lang.Crucible.Backend.Assumptions+   exposed-modules:     Lang.Crucible.Analysis.DFS     Lang.Crucible.Analysis.ForwardDataflow@@ -83,7 +87,9 @@     Lang.Crucible.Backend.AssumptionStack     Lang.Crucible.Backend.ProofGoals     Lang.Crucible.Backend.Online+    Lang.Crucible.Backend.Prove     Lang.Crucible.Backend.Simple+    Lang.Crucible.Concretize     Lang.Crucible.CFG.Common     Lang.Crucible.CFG.Core     Lang.Crucible.CFG.Expr@@ -124,6 +130,8 @@     Lang.Crucible.Utils.MuxTree     Lang.Crucible.Utils.PrettyPrint     Lang.Crucible.Utils.RegRewrite+    Lang.Crucible.Utils.Seconds+    Lang.Crucible.Utils.Timeout     Lang.Crucible.Utils.StateContT     Lang.Crucible.Utils.Structural 

@@ -21,6 +21,7 @@   weakTopologicalOrdering,   WTOComponent(..),   SCC(..),+  parentWTOComponent,   -- * Special cases   cfgWeakTopologicalOrdering,   cfgSuccessors,@@ -238,6 +239,23 @@  maxLabel :: Label maxLabel = Label maxBound++-- | Construct a map from each vertex to the head of its parent WTO component.+-- In particular, the head of a component is not in the map. The vertices that+-- are not in any component are not in the map.+parentWTOComponent :: (Ord n) => [WTOComponent n] -> M.Map n n+parentWTOComponent = F.foldMap' $ \case+  SCC scc' -> parentWTOComponent' scc'+  Vertex{} -> M.empty++parentWTOComponent' :: (Ord n) => SCC n -> M.Map n n+parentWTOComponent' scc =+  F.foldMap'+    (\case+      SCC scc' -> parentWTOComponent' scc'+      Vertex v -> M.singleton v $ wtoHead scc)+    (wtoComps scc)+  {- Note [Bourdoncle Components] 

@@ -36,42 +36,22 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-} module Lang.Crucible.Backend   ( IsSymBackend(..)   , IsSymInterface   , HasSymInterface(..)-  , SomeBackend(..)--    -- * Assumption management-  , CrucibleAssumption(..)-  , CrucibleEvent(..)-  , CrucibleAssumptions(..)-  , Assumption   , Assertion-  , Assumptions--  , concretizeEvents-  , ppEvent-  , singleEvent-  , singleAssumption-  , trivialAssumption-  , impossibleAssumption-  , ppAssumption-  , assumptionLoc-  , eventLoc-  , mergeAssumptions-  , assumptionPred-  , forgetAssumption-  , assumptionsPred-  , flattenAssumptions-  , assumptionsTopLevelLocs+  , SomeBackend(..)   , ProofObligation   , ProofObligations   , AssumptionState   , assert+  , impossibleAssumption      -- ** Reexports+  , module Lang.Crucible.Backend.Assumptions   , LabeledPred(..)   , labeledPred   , labeledPredMsg@@ -95,222 +75,45 @@   , addFailedAssertion   , assertIsInteger   , readPartExpr+  , runCHC+  , proofObligationsAsImplications+  , convertProofObligationsAsImplications+  , proofObligationsUninterpConstants+  , pathConditionUninterpConstants   , ppProofObligation   , backendOptions   , assertThenAssumeConfigOption   ) where  import           Control.Exception(Exception(..), throwIO)-import           Control.Lens ((^.), Traversal, folded)+import           Control.Lens ((^.)) import           Control.Monad import           Control.Monad.IO.Class-import           Data.Kind (Type) import           Data.Foldable (toList)-import           Data.Functor.Identity-import           Data.Functor.Const-import qualified Data.Sequence as Seq-import           Data.Sequence (Seq)+import           Data.Set (Set) import qualified Prettyprinter as PP import           GHC.Stack +import           Data.Parameterized.Map (MapF)+ import           What4.Concrete import           What4.Config+import           What4.Expr.Builder import           What4.Interface import           What4.InterpretedFloatingPoint import           What4.LabeledPred import           What4.Partial import           What4.ProgramLoc-import           What4.Expr (GroundValue, GroundValueWrapper(..)) +import           What4.Solver+import qualified What4.Solver.Z3 as Z3++import           Lang.Crucible.Backend.Assumptions import qualified Lang.Crucible.Backend.AssumptionStack as AS import qualified Lang.Crucible.Backend.ProofGoals as PG import           Lang.Crucible.Simulator.SimError --- | This type describes assumptions made at some point during program execution.-data CrucibleAssumption (e :: BaseType -> Type)-  = GenericAssumption ProgramLoc String (e BaseBoolType)-    -- ^ An unstructured description of the source of an assumption.--  | BranchCondition ProgramLoc (Maybe ProgramLoc) (e BaseBoolType)-    -- ^ This arose because we want to explore a specific path.-    -- The first location is the location of the branch predicate.-    -- The second one is the location of the branch target.--  | AssumingNoError SimError (e BaseBoolType)-    -- ^ An assumption justified by a proof of the impossibility of-    -- a certain simulator error.---- | This type describes events we can track during program execution.-data CrucibleEvent (e :: BaseType -> Type) where-  -- | This event describes the creation of a symbolic variable.-  CreateVariableEvent ::-    ProgramLoc {- ^ location where the variable was created -} ->-    String {- ^ user-provided name for the variable -} ->-    BaseTypeRepr tp {- ^ type of the variable -} ->-    e tp {- ^ the variable expression -} ->-    CrucibleEvent e--  -- | This event describes reaching a particular program location.-  LocationReachedEvent ::-    ProgramLoc ->-    CrucibleEvent e---- | Pretty print an event-ppEvent :: IsExpr e => CrucibleEvent e -> PP.Doc ann-ppEvent (CreateVariableEvent loc nm _tpr v) =-  "create var" PP.<+> PP.pretty nm PP.<+> "=" PP.<+> printSymExpr v PP.<+> "at" PP.<+> PP.pretty (plSourceLoc loc)-ppEvent (LocationReachedEvent loc) =-  "reached" PP.<+> PP.pretty (plSourceLoc loc) PP.<+> "in" PP.<+> PP.pretty (plFunction loc)---- | Return the program location associated with an event-eventLoc :: CrucibleEvent e -> ProgramLoc-eventLoc (CreateVariableEvent loc _ _ _) = loc-eventLoc (LocationReachedEvent loc) = loc---- | Return the program location associated with an assumption-assumptionLoc :: CrucibleAssumption e -> ProgramLoc-assumptionLoc r =-  case r of-    GenericAssumption l _ _ -> l-    BranchCondition  l _ _   -> l-    AssumingNoError s _    -> simErrorLoc s---- | Get the predicate associated with this assumption-assumptionPred :: CrucibleAssumption e -> e BaseBoolType-assumptionPred (AssumingNoError _ p) = p-assumptionPred (BranchCondition _ _ p) = p-assumptionPred (GenericAssumption _ _ p) = p---- | If an assumption is clearly impossible, return an abort reason---   that can be used to unwind the execution of this branch.-impossibleAssumption :: IsExpr e => CrucibleAssumption e -> Maybe AbortExecReason-impossibleAssumption (AssumingNoError err p)-  | Just False <- asConstantPred p = Just (AssertionFailure err)-impossibleAssumption (BranchCondition loc _ p)-  | Just False <- asConstantPred p = Just (InfeasibleBranch loc)-impossibleAssumption (GenericAssumption loc _ p)-  | Just False <- asConstantPred p = Just (InfeasibleBranch loc)-impossibleAssumption _ = Nothing--forgetAssumption :: CrucibleAssumption e -> CrucibleAssumption (Const ())-forgetAssumption = runIdentity . traverseAssumption (\_ -> Identity (Const ()))--traverseAssumption :: Traversal (CrucibleAssumption e) (CrucibleAssumption e') (e BaseBoolType) (e' BaseBoolType)-traverseAssumption f = \case-  GenericAssumption loc msg p -> GenericAssumption loc msg <$> f p-  BranchCondition l t p -> BranchCondition l t <$> f p-  AssumingNoError err p -> AssumingNoError err <$> f p---- | This type tracks both logical assumptions and program events---   that are relevant when evaluating proof obligations arising---   from simulation.-data CrucibleAssumptions (e :: BaseType -> Type) where-  SingleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e-  SingleEvent      :: CrucibleEvent e -> CrucibleAssumptions e-  ManyAssumptions  :: Seq (CrucibleAssumptions e) -> CrucibleAssumptions e-  MergeAssumptions ::-    e BaseBoolType {- ^ branch condition -} ->-    CrucibleAssumptions e {- ^ "then" assumptions -} ->-    CrucibleAssumptions e {- ^ "else" assumptions -} ->-    CrucibleAssumptions e--instance Semigroup (CrucibleAssumptions e) where-  ManyAssumptions xs <> ManyAssumptions ys = ManyAssumptions (xs <> ys)-  ManyAssumptions xs <> y = ManyAssumptions (xs Seq.|> y)-  x <> ManyAssumptions ys = ManyAssumptions (x Seq.<| ys)-  x <> y = ManyAssumptions (Seq.fromList [x,y])--instance Monoid (CrucibleAssumptions e) where-  mempty = ManyAssumptions mempty--singleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e-singleAssumption x = SingleAssumption x--singleEvent :: CrucibleEvent e -> CrucibleAssumptions e-singleEvent x = SingleEvent x---- | Collect the program locations of all assumptions and---   events that did not occur in the context of a symbolic branch.---   These are locations that every program path represented by---   this @CrucibleAssumptions@ structure must have passed through.-assumptionsTopLevelLocs :: CrucibleAssumptions e -> [ProgramLoc]-assumptionsTopLevelLocs (SingleEvent e)      = [eventLoc e]-assumptionsTopLevelLocs (SingleAssumption a) = [assumptionLoc a]-assumptionsTopLevelLocs (ManyAssumptions as) = concatMap assumptionsTopLevelLocs as-assumptionsTopLevelLocs MergeAssumptions{}   = []---- | Compute the logical predicate corresponding to this collection of assumptions.-assumptionsPred :: IsExprBuilder sym => sym -> Assumptions sym -> IO (Pred sym)-assumptionsPred sym (SingleEvent _) =-  return (truePred sym)-assumptionsPred _sym (SingleAssumption a) =-  return (assumptionPred a)-assumptionsPred sym (ManyAssumptions xs) =-  andAllOf sym folded =<< traverse (assumptionsPred sym) xs-assumptionsPred sym (MergeAssumptions c xs ys) =-  do xs' <- assumptionsPred sym xs-     ys' <- assumptionsPred sym ys-     itePred sym c xs' ys'--traverseEvent :: Applicative m =>-  (forall tp. e tp -> m (e' tp)) ->-  CrucibleEvent e -> m (CrucibleEvent e')-traverseEvent f (CreateVariableEvent loc nm tpr v) = CreateVariableEvent loc nm tpr <$> f v-traverseEvent _ (LocationReachedEvent loc) = pure (LocationReachedEvent loc)---- | Given a ground evaluation function, compute a linear, ground-valued---   sequence of events corresponding to this program run.-concretizeEvents ::-  IsExpr e =>-  (forall tp. e tp -> IO (GroundValue tp)) ->-  CrucibleAssumptions e ->-  IO [CrucibleEvent GroundValueWrapper]-concretizeEvents f = loop-  where-    loop (SingleEvent e) =-      do e' <- traverseEvent (\v -> GVW <$> f v) e-         return [e']-    loop (SingleAssumption _) = return []-    loop (ManyAssumptions as) = concat <$> traverse loop as-    loop (MergeAssumptions p xs ys) =-      do b <- f p-         if b then loop xs else loop ys---- | Given a @CrucibleAssumptions@ structure, flatten all the muxed assumptions into---   a flat sequence of assumptions that have been appropriately weakened.---   Note, once these assumptions have been flattened, their order might no longer---   strictly correspond to any concrete program run.-flattenAssumptions :: IsExprBuilder sym => sym -> Assumptions sym -> IO [Assumption sym]-flattenAssumptions sym = loop Nothing-  where-    loop _mz (SingleEvent _) = return []-    loop mz (SingleAssumption a) =-      do a' <- maybe (pure a) (\z -> traverseAssumption (impliesPred sym z) a) mz-         if trivialAssumption a' then return [] else return [a']-    loop mz (ManyAssumptions as) =-      concat <$> traverse (loop mz) as-    loop mz (MergeAssumptions p xs ys) =-      do pnot <- notPred sym p-         px <- maybe (pure p) (andPred sym p) mz-         py <- maybe (pure pnot) (andPred sym pnot) mz-         xs' <- loop (Just px) xs-         ys' <- loop (Just py) ys-         return (xs' <> ys')---- | Merge the assumptions collected from the branches of a conditional.-mergeAssumptions ::-  IsExprBuilder sym =>-  sym ->-  Pred sym ->-  Assumptions sym ->-  Assumptions sym ->-  IO (Assumptions sym)-mergeAssumptions _sym p thens elses =-  return (MergeAssumptions p thens elses)--type Assertion sym  = LabeledPred (Pred sym) SimError-type Assumption sym = CrucibleAssumption (SymExpr sym)-type Assumptions sym = CrucibleAssumptions (SymExpr sym)+type Assertion sym = LabeledPred (Pred sym) SimError type ProofObligation sym = AS.ProofGoal (Assumptions sym) (Assertion sym) type ProofObligations sym = Maybe (AS.Goals (Assumptions sym) (Assertion sym)) type AssumptionState sym = PG.GoalCollector (Assumptions sym) (Assertion sym)@@ -338,6 +141,17 @@ instance Exception AbortExecReason  +-- | If an assumption is clearly impossible, return an abort reason+--   that can be used to unwind the execution of this branch.+impossibleAssumption :: IsExpr e => CrucibleAssumption e -> Maybe AbortExecReason+impossibleAssumption (AssumingNoError err p)+  | Just False <- asConstantPred p = Just (AssertionFailure err)+impossibleAssumption (BranchCondition loc _ p)+  | Just False <- asConstantPred p = Just (InfeasibleBranch loc)+impossibleAssumption (GenericAssumption loc _ p)+  | Just False <- asConstantPred p = Just (InfeasibleBranch loc)+impossibleAssumption _ = Nothing+ ppAbortExecReason :: AbortExecReason -> PP.Doc ann ppAbortExecReason e =   case e of@@ -349,47 +163,21 @@       ]     VariantOptionsExhausted l -> ppLocated l "Variant options exhausted."     EarlyExit l -> ppLocated l "Program exited early."+  where+    ppLocated :: ProgramLoc -> PP.Doc ann -> PP.Doc ann+    ppLocated l x = "in" PP.<+> ppFn l PP.<+> ppLoc l PP.<> ":" PP.<+> x -ppAssumption :: (forall tp. e tp -> PP.Doc ann) -> CrucibleAssumption e -> PP.Doc ann-ppAssumption ppDoc e =-  case e of-    GenericAssumption l msg p ->-      PP.vsep [ ppLocated l (PP.pretty msg)-              , ppDoc p-              ]-    BranchCondition l Nothing p ->-      PP.vsep [ "The branch in" PP.<+> ppFn l PP.<+> "at" PP.<+> ppLoc l-              , ppDoc p-              ]-    BranchCondition l (Just t) p ->-      PP.vsep [ "The branch in" PP.<+> ppFn l PP.<+> "from" PP.<+> ppLoc l PP.<+> "to" PP.<+> ppLoc t-              , ppDoc p-              ]-    AssumingNoError simErr p ->-      PP.vsep [ "Assuming the following error does not occur:"-              , PP.indent 2 (ppSimError simErr)-              , ppDoc p-              ]+    ppFn :: ProgramLoc -> PP.Doc ann+    ppFn l = PP.pretty (plFunction l) +    ppLoc :: ProgramLoc -> PP.Doc ann+    ppLoc l = PP.pretty (plSourceLoc l)+ throwUnsupported :: (IsExprBuilder sym, MonadIO m, HasCallStack) => sym -> String -> m a throwUnsupported sym msg = liftIO $   do loc <- getCurrentProgramLoc sym      throwIO $ SimError loc $ Unsupported callStack msg ---- | Check if an assumption is trivial (always true)-trivialAssumption :: IsExpr e => CrucibleAssumption e -> Bool-trivialAssumption a = asConstantPred (assumptionPred a) == Just True--ppLocated :: ProgramLoc -> PP.Doc ann -> PP.Doc ann-ppLocated l x = "in" PP.<+> ppFn l PP.<+> ppLoc l PP.<> ":" PP.<+> x--ppFn :: ProgramLoc -> PP.Doc ann-ppFn l = PP.pretty (plFunction l)--ppLoc :: ProgramLoc -> PP.Doc ann-ppLoc l = PP.pretty (plSourceLoc l)- type IsSymInterface sym =   ( IsSymExprBuilder sym   , IsInterpretedFloatSymExprBuilder sym@@ -612,6 +400,59 @@   loc <- getCurrentProgramLoc sym   addAssertion bak (LabeledPred p (SimError loc msg))   return v+++-- | Run the CHC solver on the current proof obligations, and return the+-- solution as a substitution from the uninterpreted functions to their+-- definitions.+runCHC ::+  (IsSymBackend sym bak, sym ~ ExprBuilder t st fs, MonadIO m) =>+  bak ->+  [SomeSymFn sym] ->+  m (MapF (SymFnWrapper sym) (SymFnWrapper sym))+runCHC bak uninterp_inv_fns  = liftIO $ do+  let sym = backendGetSym bak++  implications <- proofObligationsAsImplications bak+  clearProofObligations bak++  -- log to stdout+  let logData = defaultLogData+        { logCallbackVerbose = \_ -> putStrLn+        , logReason = "Crucible inv"+        }+  Z3.runZ3Horn sym True logData uninterp_inv_fns implications >>= \case+    Sat sub -> return sub+    Unsat{} -> fail "Prover returned Unsat"+    Unknown -> fail "Prover returned Unknown"+++-- | Get proof obligations as What4 implications.+proofObligationsAsImplications :: IsSymBackend sym bak => bak -> IO [Pred sym]+proofObligationsAsImplications bak = do+  let sym = backendGetSym bak+  convertProofObligationsAsImplications sym =<< getProofObligations bak++-- | Convert proof obligations to What4 implications.+convertProofObligationsAsImplications :: IsSymInterface sym => sym -> ProofObligations sym -> IO [Pred sym]+convertProofObligationsAsImplications sym goals = do+  let obligations = maybe [] PG.goalsToList goals+  forM obligations $ \(AS.ProofGoal hyps (LabeledPred concl _err)) -> do+    hyp <- assumptionsPred sym hyps+    impliesPred sym hyp concl++-- | Get the set of uninterpreted constants that appear in the path condition.+pathConditionUninterpConstants :: IsSymBackend sym bak => bak -> IO (Set (Some (BoundVar sym)))+pathConditionUninterpConstants bak = do+  let sym = backendGetSym bak+  exprUninterpConstants sym <$> getPathCondition bak++-- | Get the set of uninterpreted constants that appear in the proof obligations.+proofObligationsUninterpConstants :: IsSymBackend sym bak => bak -> IO (Set (Some (BoundVar sym)))+proofObligationsUninterpConstants bak = do+  let sym = backendGetSym bak+  foldMap (exprUninterpConstants sym) <$> proofObligationsAsImplications bak+  ppProofObligation :: IsExprBuilder sym => sym -> ProofObligation sym -> IO (PP.Doc ann) ppProofObligation sym (AS.ProofGoal asmps gl) =

@@ -0,0 +1,268 @@+{-|+Module      : Lang.Crucible.Backend.Assumptions+Copyright   : (c) Galois, Inc 2014-2024+License     : BSD3+Maintainer  : Langston Barrett <langston@galois.com>+-}++{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}++module Lang.Crucible.Backend.Assumptions+  ( CrucibleAssumption(..)+  , CrucibleEvent(..)+  , CrucibleAssumptions(..)+  , Assumption+  , Assumptions++  , concretizeEvents+  , ppEvent+  , singleEvent+  , singleAssumption+  , trivialAssumption+  , ppAssumption+  , assumptionLoc+  , eventLoc+  , mergeAssumptions+  , assumptionPred+  , forgetAssumption+  , assumptionsPred+  , flattenAssumptions+  , assumptionsTopLevelLocs+  ) where+++import           Control.Lens (Traversal, folded)+import           Data.Kind (Type)+import           Data.Functor.Identity+import           Data.Functor.Const+import qualified Data.Sequence as Seq+import           Data.Sequence (Seq)+import qualified Prettyprinter as PP++import           What4.Expr.Builder+import           What4.Interface+import           What4.ProgramLoc+import           What4.Expr (GroundValue, GroundValueWrapper(..))++import           Lang.Crucible.Simulator.SimError++type Assumption sym = CrucibleAssumption (SymExpr sym)+type Assumptions sym = CrucibleAssumptions (SymExpr sym)++-- | This type describes assumptions made at some point during program execution.+data CrucibleAssumption (e :: BaseType -> Type)+  = GenericAssumption ProgramLoc String (e BaseBoolType)+    -- ^ An unstructured description of the source of an assumption.++  | BranchCondition ProgramLoc (Maybe ProgramLoc) (e BaseBoolType)+    -- ^ This arose because we want to explore a specific path.+    -- The first location is the location of the branch predicate.+    -- The second one is the location of the branch target.++  | AssumingNoError SimError (e BaseBoolType)+    -- ^ An assumption justified by a proof of the impossibility of+    -- a certain simulator error.++-- | This type describes events we can track during program execution.+data CrucibleEvent (e :: BaseType -> Type) where+  -- | This event describes the creation of a symbolic variable.+  CreateVariableEvent ::+    ProgramLoc {- ^ location where the variable was created -} ->+    String {- ^ user-provided name for the variable -} ->+    BaseTypeRepr tp {- ^ type of the variable -} ->+    e tp {- ^ the variable expression -} ->+    CrucibleEvent e++  -- | This event describes reaching a particular program location.+  LocationReachedEvent ::+    ProgramLoc ->+    CrucibleEvent e++-- | Pretty print an event+ppEvent :: IsExpr e => CrucibleEvent e -> PP.Doc ann+ppEvent (CreateVariableEvent loc nm _tpr v) =+  "create var" PP.<+> PP.pretty nm PP.<+> "=" PP.<+> printSymExpr v PP.<+> "at" PP.<+> PP.pretty (plSourceLoc loc)+ppEvent (LocationReachedEvent loc) =+  "reached" PP.<+> PP.pretty (plSourceLoc loc) PP.<+> "in" PP.<+> PP.pretty (plFunction loc)++-- | Return the program location associated with an event+eventLoc :: CrucibleEvent e -> ProgramLoc+eventLoc (CreateVariableEvent loc _ _ _) = loc+eventLoc (LocationReachedEvent loc) = loc++-- | Return the program location associated with an assumption+assumptionLoc :: CrucibleAssumption e -> ProgramLoc+assumptionLoc r =+  case r of+    GenericAssumption l _ _ -> l+    BranchCondition  l _ _   -> l+    AssumingNoError s _    -> simErrorLoc s++-- | Get the predicate associated with this assumption+assumptionPred :: CrucibleAssumption e -> e BaseBoolType+assumptionPred (AssumingNoError _ p) = p+assumptionPred (BranchCondition _ _ p) = p+assumptionPred (GenericAssumption _ _ p) = p++forgetAssumption :: CrucibleAssumption e -> CrucibleAssumption (Const ())+forgetAssumption = runIdentity . traverseAssumption (\_ -> Identity (Const ()))++-- | Check if an assumption is trivial (always true)+trivialAssumption :: IsExpr e => CrucibleAssumption e -> Bool+trivialAssumption a = asConstantPred (assumptionPred a) == Just True++traverseAssumption :: Traversal (CrucibleAssumption e) (CrucibleAssumption e') (e BaseBoolType) (e' BaseBoolType)+traverseAssumption f = \case+  GenericAssumption loc msg p -> GenericAssumption loc msg <$> f p+  BranchCondition l t p -> BranchCondition l t <$> f p+  AssumingNoError err p -> AssumingNoError err <$> f p++-- | This type tracks both logical assumptions and program events+--   that are relevant when evaluating proof obligations arising+--   from simulation.+data CrucibleAssumptions (e :: BaseType -> Type) where+  SingleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e+  SingleEvent      :: CrucibleEvent e -> CrucibleAssumptions e+  ManyAssumptions  :: Seq (CrucibleAssumptions e) -> CrucibleAssumptions e+  MergeAssumptions ::+    e BaseBoolType {- ^ branch condition -} ->+    CrucibleAssumptions e {- ^ "then" assumptions -} ->+    CrucibleAssumptions e {- ^ "else" assumptions -} ->+    CrucibleAssumptions e++instance Semigroup (CrucibleAssumptions e) where+  ManyAssumptions xs <> ManyAssumptions ys = ManyAssumptions (xs <> ys)+  ManyAssumptions xs <> y = ManyAssumptions (xs Seq.|> y)+  x <> ManyAssumptions ys = ManyAssumptions (x Seq.<| ys)+  x <> y = ManyAssumptions (Seq.fromList [x,y])++instance Monoid (CrucibleAssumptions e) where+  mempty = ManyAssumptions mempty++singleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e+singleAssumption x = SingleAssumption x++singleEvent :: CrucibleEvent e -> CrucibleAssumptions e+singleEvent x = SingleEvent x++-- | Collect the program locations of all assumptions and+--   events that did not occur in the context of a symbolic branch.+--   These are locations that every program path represented by+--   this @CrucibleAssumptions@ structure must have passed through.+assumptionsTopLevelLocs :: CrucibleAssumptions e -> [ProgramLoc]+assumptionsTopLevelLocs (SingleEvent e)      = [eventLoc e]+assumptionsTopLevelLocs (SingleAssumption a) = [assumptionLoc a]+assumptionsTopLevelLocs (ManyAssumptions as) = concatMap assumptionsTopLevelLocs as+assumptionsTopLevelLocs MergeAssumptions{}   = []++-- | Compute the logical predicate corresponding to this collection of assumptions.+assumptionsPred :: IsExprBuilder sym => sym -> Assumptions sym -> IO (Pred sym)+assumptionsPred sym (SingleEvent _) =+  return (truePred sym)+assumptionsPred _sym (SingleAssumption a) =+  return (assumptionPred a)+assumptionsPred sym (ManyAssumptions xs) =+  andAllOf sym folded =<< traverse (assumptionsPred sym) xs+assumptionsPred sym (MergeAssumptions c xs ys) =+  do xs' <- assumptionsPred sym xs+     ys' <- assumptionsPred sym ys+     itePred sym c xs' ys'++traverseEvent :: Applicative m =>+  (forall tp. e tp -> m (e' tp)) ->+  CrucibleEvent e -> m (CrucibleEvent e')+traverseEvent f (CreateVariableEvent loc nm tpr v) = CreateVariableEvent loc nm tpr <$> f v+traverseEvent _ (LocationReachedEvent loc) = pure (LocationReachedEvent loc)++-- | Given a ground evaluation function, compute a linear, ground-valued+--   sequence of events corresponding to this program run.+concretizeEvents ::+  IsExpr e =>+  (forall tp. e tp -> IO (GroundValue tp)) ->+  CrucibleAssumptions e ->+  IO [CrucibleEvent GroundValueWrapper]+concretizeEvents f = loop+  where+    loop (SingleEvent e) =+      do e' <- traverseEvent (\v -> GVW <$> f v) e+         return [e']+    loop (SingleAssumption _) = return []+    loop (ManyAssumptions as) = concat <$> traverse loop as+    loop (MergeAssumptions p xs ys) =+      do b <- f p+         if b then loop xs else loop ys++-- | Given a @CrucibleAssumptions@ structure, flatten all the muxed assumptions into+--   a flat sequence of assumptions that have been appropriately weakened.+--   Note, once these assumptions have been flattened, their order might no longer+--   strictly correspond to any concrete program run.+flattenAssumptions :: IsExprBuilder sym => sym -> Assumptions sym -> IO [Assumption sym]+flattenAssumptions sym = loop Nothing+  where+    loop _mz (SingleEvent _) = return []+    loop mz (SingleAssumption a) =+      do a' <- maybe (pure a) (\z -> traverseAssumption (impliesPred sym z) a) mz+         if trivialAssumption a' then return [] else return [a']+    loop mz (ManyAssumptions as) =+      concat <$> traverse (loop mz) as+    loop mz (MergeAssumptions p xs ys) =+      do pnot <- notPred sym p+         px <- maybe (pure p) (andPred sym p) mz+         py <- maybe (pure pnot) (andPred sym pnot) mz+         xs' <- loop (Just px) xs+         ys' <- loop (Just py) ys+         return (xs' <> ys')++-- | Merge the assumptions collected from the branches of a conditional.+mergeAssumptions ::+  IsExprBuilder sym =>+  sym ->+  Pred sym ->+  Assumptions sym ->+  Assumptions sym ->+  IO (Assumptions sym)+mergeAssumptions _sym p thens elses =+  return (MergeAssumptions p thens elses)++ppAssumption :: (forall tp. e tp -> PP.Doc ann) -> CrucibleAssumption e -> PP.Doc ann+ppAssumption ppDoc e =+  case e of+    GenericAssumption l msg p ->+      PP.vsep [ ppLocated l (PP.pretty msg)+              , ppDoc p+              ]+    BranchCondition l Nothing p ->+      PP.vsep [ "The branch in" PP.<+> ppFn l PP.<+> "at" PP.<+> ppLoc l+              , ppDoc p+              ]+    BranchCondition l (Just t) p ->+      PP.vsep [ "The branch in" PP.<+> ppFn l PP.<+> "from" PP.<+> ppLoc l PP.<+> "to" PP.<+> ppLoc t+              , ppDoc p+              ]+    AssumingNoError simErr p ->+      PP.vsep [ "Assuming the following error does not occur:"+              , PP.indent 2 (ppSimError simErr)+              , ppDoc p+              ]+  where+    ppLocated :: ProgramLoc -> PP.Doc ann -> PP.Doc ann+    ppLocated l x = "in" PP.<+> ppFn l PP.<+> ppLoc l PP.<> ":" PP.<+> x++    ppFn :: ProgramLoc -> PP.Doc ann+    ppFn l = PP.pretty (plFunction l)++    ppLoc :: ProgramLoc -> PP.Doc ann+    ppLoc l = PP.pretty (plSourceLoc l)

@@ -166,7 +166,7 @@ --   primarily a debugging aid, to ensure that stack management --   remains well-bracketed. newtype FrameIdentifier = FrameIdentifier Word64- deriving(Eq,Ord)+ deriving(Eq,Ord,Show)   -- | A data-strucutre that can incrementally collect goals in context.

@@ -0,0 +1,455 @@+{-|+Module      : Lang.Crucible.Backend.Prove+Description : Proving goals under assumptions+Copyright   : (c) Galois, Inc 2024+License     : BSD3++This module contains helpers to dispatch the proof obligations arising from+symbolic execution using SMT solvers. There are several dimensions of+configurability, encapsulated in a 'ProofStrategy':++* Offline vs. online: Offline solvers ('offlineProver') are simpler to manage+  and more easily parallelized, but starting processes adds overhead, and online+  solvers ('onlineProver') can share state as assumptions are added. See the+  top-level README for What4 for further discussion of this choice.+* Failing fast ('failFast') vs. keeping going ('keepGoing')+* Timeouts: Proving with timeouts ('offlineProveWithTimeout') vs. without+  ('offlineProve')+* Parallelism: Not yet available via helpers in this module, but may be added to+  a 'ProofStrategy' by clients.++Once an appropriate strategy has been selected, it can be passed to entrypoints+such as 'proveObligations' to dispatch proof obligations.++When proving a single goal, the overall approach is:++* Gather all of the assumptions ('Assumptions') currently in scope (e.g.,+  from branch conditions).+* Negate the goal ('CB.Assertion') that we are trying to prove.+* Attempt to prove the conjunction of the assumptions and the negated goal.++If this goal is satisfiable ('W4R.Sat'), then there exists a counterexample+that makes the original goal false, so we have disproven the goal. If the+negated goal is unsatisfiable ('W4R.Unsat'), on the other hand, then the+original goal is proven.++Another way to think of this is as the negated material conditional+(implication) @not (assumptions -> assertion)@. This formula is equivalent+to @not ((not assumptions) and assertion)@, i.e., @assumptions and (not+assertion)@.+-}++{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Lang.Crucible.Backend.Prove+  ( -- * Strategy+    ProofResult(..)+  , ProofConsumer(..)+  , ProofStrategy(..)+    -- ** Combiner+  , SubgoalResult(..)+  , Combiner(..)+  , keepGoing+  , failFast+    -- ** Prover+  , Prover(..)+    -- *** Offline+  , offlineProve+  , offlineProveWithTimeout+  , offlineProver+    -- *** Online+  , onlineProve+  , onlineProver+    -- * Proving goals+  , proveGoals+  , proveObligations+  , proveCurrentObligations+  ) where++import           Control.Lens ((^.))+import           Control.Monad.Catch (MonadMask)+import           Control.Monad.Error.Class (MonadError, liftEither)+import           Control.Monad.IO.Class (MonadIO(liftIO))+import qualified Control.Monad.Reader as Reader++import qualified What4.Interface as W4+import qualified What4.Expr as WE+import qualified What4.Protocol.Online as WPO+import qualified What4.Protocol.SMTWriter as W4SMT+import qualified What4.SatResult as W4R+import qualified What4.Solver.Adapter as WSA++import qualified Lang.Crucible.Backend as CB+import           Lang.Crucible.Backend.Assumptions (Assumptions)+import           Lang.Crucible.Utils.Timeout (Timeout, TimedOut)+import qualified Lang.Crucible.Utils.Timeout as CTO++-- | Local helper+consumeGoals ::+  -- | Consume an 'Assuming'+  (asmp -> a -> a) ->+  -- | Consume a 'Prove'+  (goal -> a) ->+  -- | Consume a 'ProveConj'+  (a -> a -> a) ->+  CB.Goals asmp goal ->+  a+consumeGoals onAssumption onGoal onConj = go+  where+  go (CB.Prove gl) = onGoal gl+  go (CB.Assuming as gl) = onAssumption as (go gl)+  go (CB.ProveConj g1 g2) = onConj (go g1) (go g2)++-- | Local helper+consumeGoalsWithAssumptions ::+  forall asmp goal a.+  Monoid asmp =>+  -- | Consume a 'Prove'+  (asmp -> goal -> a) ->+  -- | Consume a 'ProveConj'+  (a -> a -> a) ->+  CB.Goals asmp goal ->+  a+consumeGoalsWithAssumptions onGoal onConj goals =+  Reader.runReader (go goals) mempty+  where+  go :: CB.Goals asmp goal -> Reader.Reader asmp a+  go =+    consumeGoals+      (\asmp gl -> Reader.local (<> asmp) gl)+      (\gl -> Reader.asks (\asmps -> onGoal asmps gl))+      (\g1 g2 -> onConj <$> g1 <*> g2)++---------------------------------------------------------------------+-- * Strategy++-- | The result of attempting to prove a goal with an SMT solver.+--+-- The constructors of this type correspond to those of 'W4R.SatResult'.+--+-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'+-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type)+data ProofResult sym t+   = -- | The goal was proved.+     --+     -- Corresponds to 'W4R.Unsat'.+     Proved+     -- | The goal was disproved, and a model that falsifies it is available.+     --+     -- The 'WE.GroundEvalFn' is only available for use during the execution of+     -- a 'ProofConsumer'. See 'WSA.SolverAdapter'.+     --+     -- The @'Maybe' 'WE.ExprRangeBindings'@ are 'Just' when using+     -- 'offlineProve' and 'Nothing' when using 'onlineProve'.+     --+     -- Corresponds to 'W4R.Sat'.+   | Disproved (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t))+     -- | The SMT solver returned \"unknown\".+     --+     -- Corresponds to 'W4R.Unknown'.+   | Unknown++-- | A 'ProofStrategy' dictates how results are proved.+--+-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'+-- * @m@ is the monad in which the 'Prover' and 'Combiner' run+-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type)+-- * @r@ is the return type of the eventual 'ProofConsumer'+data ProofStrategy sym m t r+  = ProofStrategy+    { -- | Generally 'offlineProver' or 'onlineProver'+      stratProver :: {-# UNPACK #-} !(Prover sym m t r)+    , stratCombine :: Combiner m r+    }++-- | A callback used to consume a 'ProofResult'.+--+-- If the result is 'Disproved', then this function must consume the+-- 'WE.GroundEvalFn' before returning. See 'WSA.SolverAdapter'.+--+-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'+-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type)+-- * @r@ is the return type of the callback+newtype ProofConsumer sym t r+  = ProofConsumer (CB.ProofObligation sym -> ProofResult sym t -> IO r)++---------------------------------------------------------------------+-- *** Combiner++-- | Whether or not a subgoal was proved, together with the result from a+-- 'ProofConsumer'.+data SubgoalResult r+  = SubgoalResult+    { subgoalWasProved :: !Bool+    , subgoalResult :: !r+    }+  deriving Functor++-- | How to combine results of proofs, used as part of a 'ProofStrategy'.+--+-- * @m@ is the monad in which the 'Prover' and 'Combiner' run+-- * @r@ is the return type of the eventual 'ProofConsumer'+newtype Combiner m r+  = Combiner+    { getCombiner ::+        m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r)+    }++-- | Combine 'SubgoalResult's using the '<>' operator. Keep going when subgoals+-- fail.+keepGoing :: Monad m => Semigroup r => Combiner m r+keepGoing = Combiner $ \a1 a2 -> subgoalAnd <$> a1 <*> a2+  where+  subgoalAnd ::+    Semigroup r =>+    SubgoalResult r ->+    SubgoalResult r ->+    SubgoalResult r+  subgoalAnd (SubgoalResult ok1 r1) (SubgoalResult ok2 r2) =+    SubgoalResult (ok1 && ok2) (r1 <> r2)++-- | Combine 'SubgoalResult's using the '<>' operator. After the first subgoal+-- fails, stop trying to prove further goals.+failFast :: Monad m => Semigroup r => Combiner m r+failFast = Combiner $ \sr1 sr2 -> do+  SubgoalResult ok1 r1 <- sr1+  if ok1+  then do+    SubgoalResult ok2 r2 <- sr2+    pure (SubgoalResult ok2 (r1 <> r2))+  else pure (SubgoalResult False r1)++isProved :: ProofResult sym t -> Bool+isProved =+  \case+    Proved {} -> True+    Disproved {} -> False+    Unknown {} -> False++---------------------------------------------------------------------+-- ** Prover++-- | A collection of functions used to prove goals as part of a 'ProofStrategy'.+data Prover sym m t r+  = Prover+    { -- | Prove a single goal under some 'Assumptions'.+      proverProve ::+        Assumptions sym ->+        CB.Assertion sym ->+        ProofConsumer sym t r ->+        m (SubgoalResult r)+      -- | Assume some 'Assumptions' in the scope of a subgoal.+    , proverAssume ::+        Assumptions sym ->+        m (SubgoalResult r) ->+        m (SubgoalResult r)+    }++---------------------------------------------------------------------+-- *** Offline++-- Not exported+offlineProveIO ::+  (sym ~ WE.ExprBuilder t st fs) =>+  W4.IsSymExprBuilder sym =>+  sym ->+  WSA.LogData ->+  WSA.SolverAdapter st ->+  Assumptions sym ->+  CB.Assertion sym ->+  ProofConsumer sym t r ->+  IO (SubgoalResult r)+offlineProveIO sym ld adapter asmps goal (ProofConsumer k) = do+  let goalPred = goal ^. CB.labeledPred+  asmsPred <- CB.assumptionsPred sym asmps+  notGoal <- W4.notPred sym goalPred+  WSA.solver_adapter_check_sat adapter sym ld [asmsPred, notGoal] $ \r ->+    let r' =+          case r of+            W4R.Sat (gfn, binds) -> Disproved gfn binds+            W4R.Unsat () -> Proved+            W4R.Unknown -> Unknown+    in SubgoalResult (isProved r') <$> k (CB.ProofGoal asmps goal) r'++-- | Prove a goal using an \"offline\" solver (i.e., one process per goal).+--+-- See 'offlineProveWithTimeout' for a version that integrates 'Timeout's.+--+-- See the module-level documentation for further discussion of offline vs.+-- online solving.+offlineProve ::+  MonadIO m =>+  (sym ~ WE.ExprBuilder t st fs) =>+  W4.IsSymExprBuilder sym =>+  sym ->+  WSA.LogData ->+  WSA.SolverAdapter st ->+  Assumptions sym ->+  CB.Assertion sym ->+  ProofConsumer sym t r ->+  m (SubgoalResult r)+offlineProve sym ld adapter asmps goal k =+  liftIO (offlineProveIO sym ld adapter asmps goal k)++-- | Prove a goal using an \"offline\" solver, with a timeout.+--+-- See 'offlineProveWithTimeout' for a version without 'Timeout's.+--+-- See the module-level documentation for further discussion of offline vs.+-- online solving.+offlineProveWithTimeout ::+  MonadError TimedOut m =>+  MonadIO m =>+  (sym ~ WE.ExprBuilder t st fs) =>+  W4.IsSymExprBuilder sym =>+  Timeout ->+  sym ->+  WSA.LogData ->+  WSA.SolverAdapter st ->+  Assumptions sym ->+  CB.Assertion sym ->+  ProofConsumer sym t r ->+  m (SubgoalResult r)+offlineProveWithTimeout to sym ld adapter asmps goal k = do+  r <- liftIO (CTO.withTimeout to (offlineProveIO sym ld adapter asmps goal k))+  liftEither r++-- | Prove goals using 'offlineProveWithTimeout'.+--+-- See the module-level documentation for further discussion of offline vs.+-- online solving.+offlineProver ::+  MonadError TimedOut m =>+  MonadIO m =>+  (sym ~ WE.ExprBuilder t st fs) =>+  Timeout ->+  W4.IsSymExprBuilder sym =>+  sym ->+  WSA.LogData ->+  WSA.SolverAdapter st ->+  Prover sym m t r+offlineProver to sym ld adapter =+  Prover+  { proverProve = offlineProveWithTimeout to sym ld adapter+  , proverAssume = \_asmps a -> a+  }++---------------------------------------------------------------------+-- *** Online++-- | Prove a goal using an \"online\" solver (i.e., one process for all goals).+--+-- See the module-level documentation for further discussion of offline vs.+-- online solving.+onlineProve ::+  MonadIO m =>+  W4SMT.SMTReadWriter solver =>+  (sym ~ WE.ExprBuilder t st fs) =>+  W4.IsSymExprBuilder sym =>+  WPO.SolverProcess t solver ->+  Assumptions sym ->+  CB.Assertion sym ->+  ProofConsumer sym t r ->+  m (SubgoalResult r)+onlineProve sProc asmps goal (ProofConsumer k) =+  liftIO $ WPO.checkSatisfiableWithModel sProc "prove" (goal ^. CB.labeledPred) $ \r ->+    let r' =+          case r of+            W4R.Sat gfn -> Disproved gfn Nothing+            W4R.Unsat () -> Proved+            W4R.Unknown -> Unknown+    in SubgoalResult (isProved r') <$> k (CB.ProofGoal asmps goal) r'++-- | Add an assumption by @push@ing a new frame ('WPO.inNewFrame').+onlineAssume :: +  MonadIO m =>+  MonadMask m =>+  W4SMT.SMTReadWriter solver =>+  W4.IsSymExprBuilder sym =>+  (W4.SymExpr sym ~ WE.Expr t) =>+  sym ->+  WPO.SolverProcess t solver ->+  Assumptions sym ->+  m r ->+  m r+onlineAssume sym sProc asmps a =+  WPO.inNewFrame sProc $ do+    liftIO $ do+      let conn = WPO.solverConn sProc+      asmpsPred <- CB.assumptionsPred sym asmps+      term <- W4SMT.mkFormula conn asmpsPred+      W4SMT.assumeFormula conn term+      pure ()+    a++-- | Prove goals using 'onlineProve' and 'onlineAssume'.+--+-- See the module-level documentation for further discussion of offline vs.+-- online solving.+onlineProver ::+  MonadIO m =>+  MonadMask m =>+  W4SMT.SMTReadWriter solver =>+  (sym ~ WE.ExprBuilder t st fs) =>+  W4.IsSymExprBuilder sym =>+  sym ->+  WPO.SolverProcess t solver ->+  Prover sym m t r+onlineProver sym sProc =+  Prover+  { proverProve = onlineProve sProc+  , proverAssume = onlineAssume sym sProc+  }++---------------------------------------------------------------------+-- * Proving goals++-- | Prove a collection of 'CB.Goals' using the specified 'ProofStrategy'.+proveGoals ::+  Functor m =>+  ProofStrategy sym m t r ->+  CB.Goals (CB.Assumptions sym) (CB.Assertion sym) ->+  ProofConsumer sym t r ->+  m r+proveGoals (ProofStrategy prover (Combiner comb)) goals k =+  fmap subgoalResult $+    consumeGoalsWithAssumptions+      (\asmps gl -> proverProve prover asmps gl k)+      comb+      goals++-- | Prove a collection of 'CB.ProofObligations' using a 'ProofStrategy'.+proveObligations ::+  Applicative m =>+  Monoid r =>+  (sym ~ WE.ExprBuilder t st fs) =>+  ProofStrategy sym m t r ->+  CB.ProofObligations sym ->+  ProofConsumer sym t r ->+  m r+proveObligations strat obligations k =+  case obligations of+    Nothing -> pure mempty+    Just goals -> proveGoals strat goals k++-- | Prove a the current collection of 'CB.ProofObligations' associated with the+-- symbolic backend (retrieved via 'CB.getProofObligations').+proveCurrentObligations ::+  MonadIO m =>+  Monoid r =>+  (sym ~ WE.ExprBuilder t st fs) =>+  CB.IsSymBackend sym bak =>+  bak ->+  ProofStrategy sym m t r ->+  ProofConsumer sym t r ->+  m r+proveCurrentObligations bak strat k = do+  obligations <- liftIO (CB.getProofObligations bak)+  proveObligations strat obligations k

@@ -75,7 +75,6 @@ import           Data.Parameterized.TraversableFC  import           What4.Interface (RoundingMode(..),StringLiteral(..), stringLiteralInfo)-import           What4.InterpretedFloatingPoint (X86_80Val(..))  import           Lang.Crucible.CFG.Extension import           Lang.Crucible.FunctionHandle

@@ -0,0 +1,607 @@+-----------------------------------------------------------------------+-- |+-- Module           : Lang.Crucible.Concretize+-- Description      : Get feasible concrete values from a model+-- Copyright        : (c) Galois, Inc 2024+-- License          : BSD3+-- 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 can be used to report specific values that lead to violations of+-- assertions, including safety assertions.+------------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}++module Lang.Crucible.Concretize+  ( ConcRegValue+  , ConcRV'(..)+  , ConcAnyValue(..)+  , ConcIntrinsic+  , IntrinsicConcFn(..)+  , ConcCtx(..)+  , concRegValue+  , concRegEntry+  , concRegMap+    -- * There and back again+  , IntrinsicConcToSymFn(..)+  , concToSym+  ) where++import qualified Data.Foldable as F+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.Sequence (Seq)+import           Data.Text (Text)+import qualified Data.Text as Text+import qualified Data.Vector as V+import           Data.Word (Word16)++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           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           Lang.Crucible.FunctionHandle (FnHandle, RefCell)+import           Lang.Crucible.Simulator.Intrinsics (Intrinsic)+import           Lang.Crucible.Simulator.RegMap (RegEntry, RegMap)+import qualified Lang.Crucible.Simulator.RegMap as RM+import           Lang.Crucible.Simulator.RegValue (RegValue, FnVal)+import qualified Lang.Crucible.Simulator.RegValue as RV+import qualified Lang.Crucible.Simulator.SymSequence as SymSeq+import qualified Lang.Crucible.Utils.MuxTree as MuxTree+import           Lang.Crucible.Types+import           Lang.Crucible.Panic (panic)++-- | Newtype to allow partial application of 'ConcRegValue'.+--+-- Type families cannot appear partially applied.+type ConcRV' :: Type -> CrucibleType -> Type+newtype ConcRV' sym tp = ConcRV' { unConcRV' :: ConcRegValue sym tp }++-- | Defines the \"concrete\" interpretations of 'CrucibleType' (as opposed+-- to the \"symbolic\" interpretations, which are defined by 'RegValue'), as+-- returned by 'concRegValue'.+--+-- Unlike What4\'s 'W4GE.GroundValue', this type family is parameterized+-- by @sym@, the symbolic backend. This is because Crucible makes use of+-- \"interpreted\" floating point numbers ('SymInterpretedFloatType'). What4\'s+-- @SymFloat@ always uses an IEEE-754 interpretation of symbolic floats, whereas+-- 'SymInterpretedFloatType' can use IEEE-754, real numbers, or uninterpreted+-- functions depending on how the symbolic backend is configured.+type ConcRegValue :: Type -> CrucibleType -> Type+type family ConcRegValue sym tp where+  ConcRegValue sym (BaseToType bt) = W4GE.GroundValue bt+  ConcRegValue sym (FloatType fi) = W4GE.GroundValue (SymInterpretedFloatType sym fi)+  ConcRegValue sym AnyType = ConcAnyValue sym+  ConcRegValue sym UnitType = ()+  ConcRegValue sym NatType = Integer+  ConcRegValue sym CharType = Word16+  ConcRegValue sym (FunctionHandleType a r) = ConcFnVal sym a r+  ConcRegValue sym (MaybeType tp) = Maybe (ConcRegValue sym tp)+  ConcRegValue sym (VectorType tp) = V.Vector (ConcRV' sym tp)+  ConcRegValue sym (SequenceType tp) = Seq (ConcRV' sym tp)+  ConcRegValue sym (StructType ctx) = Ctx.Assignment (ConcRV' sym) ctx+  ConcRegValue sym (VariantType ctx) = Ctx.Assignment (ConcVariantBranch sym) ctx+  ConcRegValue sym (ReferenceType tp) = NonEmpty (RefCell tp)+  ConcRegValue sym (WordMapType w tp) = ()  -- TODO: possible to do something meaningful?+  ConcRegValue sym (RecursiveType nm ctx) = ConcRegValue sym (UnrollType nm ctx)+  ConcRegValue sym (IntrinsicType nm ctx) = ConcIntrinsic nm ctx+  ConcRegValue sym (StringMapType tp) = Map Text (ConcRV' sym tp)++---------------------------------------------------------------------+-- * ConcCtx++-- | Context needed for 'concRegValue'+--+-- 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+-- (similar to the @s@ parameter of the @ST@ monad). It also appears as the+-- first argument to 'ExprBuilder'.+data ConcCtx sym t+  = ConcCtx+  { -- | Model returned from SMT solver+    model :: W4GE.GroundEvalFn t+    -- | How to ground intrinsics+  , intrinsicConcFuns :: MapF SymbolRepr (IntrinsicConcFn t)+  }++-- | Helper, not exported+ground ::+  ConcCtx sym t ->+  Expr t tp ->+  IO (ConcRegValue sym (BaseToType tp))+ground (ConcCtx (W4GE.GroundEvalFn ge) _) = ge++---------------------------------------------------------------------+-- * Helpers++-- | Helper, not exported+ite ::+  (SymExpr sym ~ Expr t) =>+  ConcCtx sym t ->+  W4I.Pred sym ->+  a ->+  a ->+  IO a+ite ctx p t f = do+  b <- ground ctx p+  pure (if b then t else f)++-- | Helper, not exported+iteIO ::+  (SymExpr sym ~ Expr t) =>+  ConcCtx sym t ->+  W4I.Pred sym ->+  IO a ->+  IO a ->+  IO a+iteIO ctx p t f = do+  b <- ground ctx p+  if b then t else f++-- | Helper, not exported+concPartial ::+  (SymExpr sym ~ Expr t) =>+  W4I.IsExprBuilder sym =>+  ConcCtx sym t ->+  TypeRepr tp ->+  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)++-- | Helper, not exported+concPartialWithErr ::+  (SymExpr sym ~ Expr t) =>+  W4I.IsExprBuilder sym =>+  ConcCtx sym t ->+  TypeRepr tp ->+  W4P.PartialWithErr e (W4I.Pred sym) (RegValue sym tp) ->+  IO (Maybe (ConcRegValue sym tp))+concPartialWithErr ctx tp =+  \case+    W4P.Err _ -> pure Nothing+    W4P.NoErr pv -> concPartial ctx tp pv++---------------------------------------------------------------------+-- * Intrinsics++-- | Open type family for defining how intrinsics are concretized+type ConcIntrinsic :: Symbol -> Ctx CrucibleType -> Type+type family ConcIntrinsic nm ctx++-- | Function for concretizing an intrinsic type+type IntrinsicConcFn :: Type -> Symbol -> Type+newtype IntrinsicConcFn t nm+  = IntrinsicConcFn+    (forall sym ctx.+      SymExpr sym ~ Expr t =>+      W4I.IsExprBuilder sym =>+      ConcCtx sym t ->+      Ctx.Assignment TypeRepr ctx ->+      Intrinsic sym nm ctx ->+      IO (ConcRegValue sym (IntrinsicType nm ctx)))++-- | Helper, not exported+tryConcIntrinsic ::+  forall sym nm ctx t.+  SymExpr sym ~ Expr t =>+  W4I.IsExprBuilder sym =>+  ConcCtx sym t ->+  SymbolRepr nm ->+  Ctx.Assignment TypeRepr ctx ->+  RegValue sym (IntrinsicType nm ctx) ->+  Maybe (IO (ConcRegValue sym (IntrinsicType nm ctx)))+tryConcIntrinsic ctx nm tyCtx v = do+    case MapF.lookup nm (intrinsicConcFuns ctx) of+      Nothing -> Nothing+      Just (IntrinsicConcFn f) -> Just (f @sym @ctx ctx tyCtx v)++---------------------------------------------------------------------+-- * Any++-- | An 'AnyValue' concretized by 'concRegValue'+data ConcAnyValue sym = forall tp. ConcAnyValue (TypeRepr tp) (ConcRV' sym tp)++---------------------------------------------------------------------+-- * FnVal++-- | A 'FnVal' concretized by 'concRegValue'+data ConcFnVal (sym :: Type) (args :: Ctx CrucibleType) (res :: CrucibleType) where+  ConcClosureFnVal ::+    !(ConcFnVal sym (args ::> tp) ret) ->+    !(TypeRepr tp) ->+    !(ConcRV' sym tp) ->+    ConcFnVal sym args ret++  ConcVarargsFnVal ::+    !(FnHandle (args ::> VectorType AnyType) ret) ->+    !(CtxRepr addlArgs) ->+    ConcFnVal sym (args <+> addlArgs) ret++  ConcHandleFnVal ::+    !(FnHandle a r) ->+    ConcFnVal sym a r++-- | Helper, not exported+concFnVal ::+  (SymExpr sym ~ Expr t) =>+  W4I.IsExprBuilder sym =>+  ConcCtx sym t ->+  CtxRepr args ->+  TypeRepr ret ->+  FnVal sym args ret ->+  IO (ConcFnVal sym args ret)+concFnVal ctx args ret =+  \case+    RV.ClosureFnVal fv t v -> do+      concV <- concFnVal ctx (args Ctx.:> t) ret fv+      v' <- concRegValue ctx t v+      pure (ConcClosureFnVal concV t (ConcRV' v'))+    RV.VarargsFnVal hdl extra ->+      pure (ConcVarargsFnVal hdl extra)+    RV.HandleFnVal hdl ->+      pure (ConcHandleFnVal hdl)++---------------------------------------------------------------------+-- * Reference++-- | Helper, not exported+concMux ::+  (SymExpr sym ~ Expr t) =>+  W4I.IsExprBuilder sym =>+  ConcCtx sym t ->+  MuxTree.MuxTree sym a ->+  IO (NonEmpty a)+concMux ctx mt = do+  l <- go (MuxTree.viewMuxTree mt)+  case NE.nonEmpty l of+    -- This is impossible because the only way to make a MuxTree is with+    -- `toMuxTree`, which uses `truePred`.+    Nothing ->+      panic "Lang.Crucible.Concretize.concMux"+        [ "Impossible: Mux tree had no feasible branches?" ]+    Just ne -> pure ne+  where+    go [] = pure []+    go ((val, p):xs) = do+      f <- ite ctx p (val:) id+      f <$> go xs++---------------------------------------------------------------------+-- * Sequence++-- | Helper, not exported+concSymSequence ::+  (SymExpr sym ~ Expr t) =>+  W4I.IsExprBuilder sym =>+  ConcCtx sym t ->+  TypeRepr tp ->+  SymSeq.SymSequence sym (RegValue sym tp) ->+  IO (Seq (ConcRV' sym tp))+concSymSequence ctx tp =+  SymSeq.concretizeSymSequence+    (ground ctx)+    (fmap ConcRV' . concRegValue ctx tp)++---------------------------------------------------------------------+-- * StringMap++-- | Helper, not exported+concStringMap ::+  (SymExpr sym ~ Expr t) =>+  W4I.IsExprBuilder sym =>+  ConcCtx sym t ->+  TypeRepr tp ->+  RegValue sym (StringMapType tp) ->+  IO (Map Text (ConcRV' sym tp))+concStringMap ctx tp v = Map.fromList <$> go (Map.toList v)+  where+    go [] = pure []+    go ((t, v'):xs) =+      concPartialWithErr ctx tp v' >>=+        \case+          Nothing -> go xs+          Just v'' -> ((t, ConcRV' v''):) <$> go xs++---------------------------------------------------------------------+-- * Variant++-- | Note that we do not attempt to \"normalize\" variants in 'concRegValue'+-- 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+  = ConcVariantBranch (Maybe (ConcRV' sym tp))++-- | Helper, not exported+concVariant ::+  forall sym variants t.+  (SymExpr sym ~ Expr t) =>+  W4I.IsExprBuilder sym =>+  ConcCtx sym t ->+  Ctx.Assignment TypeRepr variants ->+  RegValue sym (VariantType variants) ->+  IO (ConcRegValue sym (VariantType variants))+concVariant ctx tps vs = Ctx.zipWithM concBranch tps vs+  where+    concBranch :: forall tp. TypeRepr tp -> RV.VariantBranch sym tp -> IO (ConcVariantBranch sym tp)+    concBranch tp (RV.VB v) = do+      v' <- concPartialWithErr ctx tp v+      case v' of+        Just v'' -> pure (ConcVariantBranch (Just (ConcRV' v'')))+        Nothing -> pure (ConcVariantBranch Nothing)++---------------------------------------------------------------------+-- * 'concRegValue'++-- | 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 ::+  (SymExpr sym ~ Expr t) =>+  W4I.IsExprBuilder sym =>+  ConcCtx sym t ->+  TypeRepr tp ->+  RegValue sym tp ->+  IO (ConcRegValue sym tp)+concRegValue ctx tp v =+  case (tp, v) of+    -- Base types+    (BoolRepr, _) -> ground ctx v+    (BVRepr _width, _) -> ground ctx v+    (ComplexRealRepr, _) -> ground ctx v+    (FloatRepr _fpp, _) -> ground ctx v+    (IEEEFloatRepr _fpp, _) -> ground ctx v+    (IntegerRepr, _) -> ground ctx v+    (NatRepr, _) -> ground ctx (W4I.natToIntegerPure v)+    (RealValRepr, _) -> ground ctx v+    (StringRepr _, _) -> ground ctx v+    (SymbolicArrayRepr _idxs _tp', _) -> ground ctx v+    (SymbolicStructRepr _tys, _) -> ground ctx v++    -- Trivial cases+    (UnitRepr, ()) -> pure ()+    (CharRepr, _) -> pure v++    -- Simple recursive cases+    (AnyRepr, RV.AnyValue tp' v') ->+      ConcAnyValue tp' . ConcRV' <$> concRegValue ctx tp' v'+    (RecursiveRepr symb tyCtx, RV.RolledType v') ->+      concRegValue ctx (unrollType symb tyCtx) v'+    (StructRepr tps, _) ->+      Ctx.zipWithM (\tp' (RV.RV v') -> ConcRV' <$> concRegValue ctx tp' v') tps v+    (VectorRepr tp', _) ->+      traverse (fmap ConcRV' . concRegValue ctx tp') v++    -- Cases with helper functions+    (MaybeRepr tp', _) ->+      concPartialWithErr ctx tp' v+    (FunctionHandleRepr args ret, _) ->+      concFnVal ctx args ret v+    (IntrinsicRepr nm tyCtx, _) ->+      case tryConcIntrinsic ctx nm tyCtx v of+        Nothing ->+          let strNm = Text.unpack (symbolRepr nm) in+          fail ("Missing concretization function for intrinsic: " ++ strNm)+        Just r -> r+    (ReferenceRepr _, _) ->+      concMux ctx v+    (SequenceRepr tp', _) ->+      concSymSequence ctx tp' v+    (StringMapRepr tp', _) ->+      concStringMap ctx tp' v+    (VariantRepr tps, _) ->+      concVariant ctx tps v++    -- Incomplete cases+    (WordMapRepr _ _, _) -> pure ()++-- | Like 'concRegValue', but for 'RegEntry'+concRegEntry ::+  (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)++-- | Like 'concRegEntry', but for a whole 'RegMap'+concRegMap ::+  (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++---------------------------------------------------------------------+-- * concToSym++-- | Function for re-symbolizing an intrinsic type+type IntrinsicConcToSymFn :: Symbol -> Type+newtype IntrinsicConcToSymFn nm+  = IntrinsicConcToSymFn+    (forall sym ctx.+      W4I.IsExprBuilder sym =>+      sym ->+      Ctx.Assignment TypeRepr ctx ->+      ConcIntrinsic nm ctx ->+      IO (RegValue sym (IntrinsicType nm ctx)))++-- | Helper, not exported+concToSymAny ::+  (sym ~ ExprBuilder scope st (Flags fm)) =>+  sym ->+  MapF SymbolRepr IntrinsicConcToSymFn ->+  FloatModeRepr fm ->+  ConcRegValue sym AnyType ->+  IO (RegValue sym AnyType)+concToSymAny sym iFns fm (ConcAnyValue tp' (ConcRV' v')) =+  RV.AnyValue tp' <$> concToSym sym iFns fm tp' v'++-- | Helper, not exported+concToSymFn ::+  (sym ~ ExprBuilder scope st (Flags fm)) =>+  sym ->+  MapF SymbolRepr IntrinsicConcToSymFn ->+  FloatModeRepr fm ->+  Ctx.Assignment (TypeRepr) as ->+  TypeRepr r ->+  ConcRegValue sym (FunctionHandleType as r) ->+  IO (RegValue sym (FunctionHandleType as r))+concToSymFn sym iFns fm as r f =+  case f of+    ConcClosureFnVal clos vtp (ConcRV' v) -> do+      v' <- concToSym sym iFns fm vtp v+      clos' <- concToSymFn sym iFns fm (as Ctx.:> vtp) r clos+      pure (RV.ClosureFnVal clos' vtp v')++    ConcVarargsFnVal hdl extra ->+      pure (RV.VarargsFnVal hdl extra)++    ConcHandleFnVal hdl ->+      pure (RV.HandleFnVal hdl)++-- | Helper, not exported+concToSymIntrinsic ::+  W4I.IsExprBuilder sym =>+  sym ->+  MapF SymbolRepr IntrinsicConcToSymFn ->+  SymbolRepr nm ->+  CtxRepr ctx ->+  ConcRegValue sym (IntrinsicType nm ctx) ->+  IO (RegValue sym (IntrinsicType nm ctx))+concToSymIntrinsic sym iFns nm tyCtx v =+  case MapF.lookup nm iFns of+    Nothing ->+      let strNm = Text.unpack (symbolRepr nm) in+      fail ("Missing concretization function for intrinsic: " ++ strNm)+    Just (IntrinsicConcToSymFn f) -> f sym tyCtx v++-- | Helper, not exported+concToSymMaybe ::+  (sym ~ ExprBuilder scope st (Flags fm)) =>+  sym ->+  MapF SymbolRepr IntrinsicConcToSymFn ->+  FloatModeRepr fm ->+  TypeRepr tp ->+  ConcRegValue sym (MaybeType tp) ->+  IO (RegValue sym (MaybeType tp))+concToSymMaybe sym iFns fm tp =+  \case+    Nothing -> pure (W4P.Err ())+    Just v ->+      W4P.justPartExpr sym <$> concToSym sym iFns fm tp v++-- | Helper, not exported+concToSymRef ::+  W4I.IsExprBuilder sym =>+  sym ->+  ConcRegValue sym (ReferenceType tp) ->+  IO (RegValue sym (ReferenceType tp))+concToSymRef sym (v NE.:| _) = pure (MuxTree.toMuxTree sym v)++-- | Helper, not exported+concToSymVariant ::+  forall sym tps scope st fm.+  (sym ~ ExprBuilder scope st (Flags fm)) =>+  sym ->+  MapF SymbolRepr IntrinsicConcToSymFn ->+  FloatModeRepr fm ->+  CtxRepr tps ->+  ConcRegValue sym (VariantType tps) ->+  IO (RegValue sym (VariantType tps))+concToSymVariant sym iFns fm tps v = Ctx.zipWithM go tps v+  where+    go :: forall tp. TypeRepr tp -> ConcVariantBranch sym tp -> IO (RV.VariantBranch sym tp)+    go tp (ConcVariantBranch b) =+      case b of+        Nothing -> pure (RV.VB (W4P.Err ()))+        Just (ConcRV' v') ->+          RV.VB . W4P.justPartExpr sym <$> concToSym sym iFns fm tp v'++-- | Inject a 'ConcRegValue' back into a 'RegValue'.+concToSym ::+  (sym ~ ExprBuilder scope st (Flags fm)) =>+  sym ->+  MapF SymbolRepr IntrinsicConcToSymFn ->+  FloatModeRepr fm ->+  TypeRepr tp ->+  ConcRegValue sym tp ->+  IO (RegValue sym tp)+concToSym sym iFns fm tp v =+  case tp of+    -- Base types+    BoolRepr -> W4GE.groundToSym sym BaseBoolRepr v+    BVRepr width -> W4GE.groundToSym sym (BaseBVRepr width) v+    ComplexRealRepr -> W4GE.groundToSym sym BaseComplexRepr v+    FloatRepr fi ->+      case fm of+        FloatIEEERepr ->+          W4I.floatLit sym (floatInfoToPrecisionRepr fi) v+        FloatUninterpretedRepr -> do+          sv <- W4GE.groundToSym sym (floatInfoToBVTypeRepr fi) v+          iFloatFromBinary sym fi sv+        FloatRealRepr ->+          iFloatLitRational sym fi v+    IEEEFloatRepr fpp -> W4GE.groundToSym sym (BaseFloatRepr fpp) v+    IntegerRepr -> W4GE.groundToSym sym BaseIntegerRepr v+    NatRepr -> W4I.integerToNat sym =<< W4GE.groundToSym sym BaseIntegerRepr v+    RealValRepr -> W4GE.groundToSym sym BaseRealRepr v+    StringRepr si -> W4GE.groundToSym sym (BaseStringRepr si) v+    SymbolicArrayRepr idxs tp' -> W4GE.groundToSym sym (BaseArrayRepr idxs tp') v+    SymbolicStructRepr tys -> W4GE.groundToSym sym (BaseStructRepr tys) v++    -- Trivial cases+    UnitRepr -> pure ()+    CharRepr -> pure v++    -- Simple recursive cases+    RecursiveRepr symb tyCtx ->+      RV.RolledType <$> concToSym sym iFns fm (unrollType symb tyCtx) v+    SequenceRepr tp' -> do+      l <- traverse (concToSym sym iFns fm tp' . unConcRV') (F.toList v)+      SymSeq.fromListSymSequence sym l+    StringMapRepr tp' ->+      traverse (fmap (W4P.justPartExpr sym) . concToSym sym iFns fm tp' . unConcRV') v+    StructRepr tps ->+      Ctx.zipWithM (\tp' (ConcRV' v') -> RV.RV <$> concToSym sym iFns fm tp' v') tps v+    VectorRepr tp' ->+      traverse (concToSym sym iFns fm tp' . unConcRV') v++    -- Cases with helper functions+    AnyRepr -> concToSymAny sym iFns fm v+    MaybeRepr tp' -> concToSymMaybe sym iFns fm tp' v+    FunctionHandleRepr args ret -> concToSymFn sym iFns fm args ret v+    IntrinsicRepr nm tyCtx -> concToSymIntrinsic sym iFns nm tyCtx v+    ReferenceRepr _tp' -> concToSymRef sym v+    VariantRepr tps -> concToSymVariant sym iFns fm tps v++    -- Incomplete cases+    WordMapRepr _ _ -> fail "concToSym does not yet support WordMap"

@@ -34,6 +34,7 @@   , emptyHandleMap   , insertHandleMap   , lookupHandleMap+  , updateHandleMap   , searchHandleMap   , handleMapToHandles     -- * Reference cells@@ -44,6 +45,7 @@  import           Data.Hashable import           Data.Kind+import           Data.Functor.Identity import qualified Data.List as List import           Data.Ord (comparing) @@ -216,6 +218,19 @@   case MapF.lookup (handleID hdl) m of      Just (HandleElt _ x) -> Just x      Nothing -> Nothing++-- | Update the entry of the function handle in the map.+updateHandleMap :: (f args ret -> f args ret)+                -> FnHandle args ret+                -> FnHandleMap f+                -> FnHandleMap f+updateHandleMap f hdl (FnHandleMap m) =+  FnHandleMap $ MapF.updatedValue $ runIdentity $+    MapF.updateAtKey+      (handleID hdl)+      (Identity Nothing)+      (\(HandleElt hdl' x) -> Identity $ MapF.Set $ HandleElt hdl' $ f x)+      m  -- | Lookup the function name in the map by a linear scan of all -- entries.  This will be much slower than using 'lookupHandleMap' to

@@ -60,7 +60,6 @@  import           What4.Config import           What4.Interface-import           What4.InterpretedFloatingPoint (freshFloatConstant) import           What4.Partial import           What4.ProgramLoc 

@@ -792,8 +792,8 @@       bvSlt sym x y     BoolToBV w xe -> do       x <- evalSub xe-      one <- bvLit sym w (BV.one w)-      zro <- bvLit sym w (BV.zero w)+      one <- bvOne sym w+      zro <- bvZero sym w       bvIte sym x one zro     BVNonzero _ xe -> do       x <- evalSub xe

@@ -76,6 +76,7 @@  import           Lang.Crucible.Backend import           Lang.Crucible.CFG.Core+import           Lang.Crucible.Panic (panic) import           Lang.Crucible.Simulator.CallFrame import           Lang.Crucible.Simulator.EvalStmt import           Lang.Crucible.Simulator.ExecutionTree@@ -290,7 +291,11 @@  go xs (e Seq.:<| es) =    case cgEvent_type e of      ENTER -> go (e:xs) es-     EXIT  -> go (tail xs) es+     EXIT  -> case xs of+                (_:xss) -> go xss es+                _ -> panic+                       "openEventFrames"+                       ["Encountered an EXIT without a preceding ENTER"]      _     -> go xs es  openToCloseEvent :: UTCTime -> Metrics Identity -> CGEvent -> CGEvent

@@ -14,6 +14,7 @@ ( SymSequence(..) , nilSymSequence , consSymSequence+, fromListSymSequence , appendSymSequence , muxSymSequence , isNilSymSequence@@ -23,6 +24,7 @@ , unconsSymSequence , traverseSymSequence , concreteizeSymSequence+, concretizeSymSequence , prettySymSequence    -- * Low-level evaluation primitives@@ -40,6 +42,8 @@ import qualified Data.Map as Map import           Data.Parameterized.Nonce import qualified Data.Parameterized.Map as MapF+import           Data.Sequence (Seq)+import qualified Data.Sequence as Seq import           Prettyprinter (Doc) import qualified Prettyprinter as PP @@ -167,6 +171,12 @@   do n <- freshNonce globalNonceGenerator      pure (SymSequenceCons n x xs) +fromListSymSequence :: sym -> [a] -> IO (SymSequence sym a)+fromListSymSequence sym =+  \case+    [] -> nilSymSequence sym+    (x:xs) -> consSymSequence sym x =<< fromListSymSequence sym xs+ -- | Append two sequences appendSymSequence ::   sym ->@@ -400,6 +410,24 @@     loop SymSequenceNil = pure []     loop (SymSequenceCons _ v tl) = (:) <$> eval v <*> loop tl     loop (SymSequenceAppend _ xs ys) = (++) <$> loop xs <*> loop ys+    loop (SymSequenceMerge _ p xs ys) =+      do b <- conc p+         if b then loop xs else loop ys+{-# DEPRECATED concreteizeSymSequence "Use concretizeSymSequence instead" #-} ++-- | Using the given evaluation function for booleans, and an evaluation+--   function for values, compute a concrete sequence corresponding+--   to the given symbolic sequence.+concretizeSymSequence ::+  (Pred sym -> IO Bool) {- ^ evaluation for booleans -} ->+  (a -> IO b) {- ^ evaluation for values -} ->+  SymSequence sym a ->+  IO (Seq b)+concretizeSymSequence conc eval = loop+  where+    loop SymSequenceNil = pure Seq.empty+    loop (SymSequenceCons _ v tl) = (Seq.<|) <$> eval v <*> loop tl+    loop (SymSequenceAppend _ xs ys) = (Seq.><) <$> loop xs <*> loop ys     loop (SymSequenceMerge _ p xs ys) =       do b <- conc p          if b then loop xs else loop ys

@@ -95,16 +95,7 @@   , module Data.Parameterized.NatRepr   , module Data.Parameterized.SymbolRepr   , module What4.BaseTypes-  , FloatInfo-  , HalfFloat-  , SingleFloat-  , DoubleFloat-  , QuadFloat-  , X86_80Float-  , DoubleDoubleFloat-  , FloatInfoRepr(..)-  , FloatInfoToBitWidth-  , floatInfoToBVTypeRepr+  , module What4.InterpretedFloatingPoint   ) where  import           Data.Hashable

@@ -0,0 +1,18 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module Lang.Crucible.Utils.Seconds+  ( Seconds+  , secondsToInt+  , secondsFromInt+  , secondsToMicroseconds+  ) where++newtype Seconds = Seconds { secondsToInt :: Int }+  deriving (Eq, Num, Ord, Show)++-- | Inverse of 'secondsToInt'+secondsFromInt :: Int -> Seconds+secondsFromInt = Seconds++secondsToMicroseconds :: Seconds -> Int+secondsToMicroseconds = (* 1000000) . secondsToInt

@@ -0,0 +1,38 @@+module Lang.Crucible.Utils.Timeout+  ( Timeout(..)+  , TimedOut(..)+  , withTimeout+  ) where++import qualified Control.Concurrent as CC+import qualified Control.Concurrent.Async as CCA++import qualified Lang.Crucible.Utils.Seconds as Secs++-- | A timeout, in seconds.+newtype Timeout = Timeout { getTimeout :: Secs.Seconds }+  deriving (Eq, Ord, Show)++-- Private, not exported+timeoutToMicros :: Timeout -> Int+timeoutToMicros = Secs.secondsToMicroseconds . getTimeout++-- | A task timed out.+data TimedOut = TimedOut+  deriving Show++-- | Execute a task with a timeout.+--+-- Implemented via 'CCA.race', so re-throws exceptions that occur during the+-- task (if it completes before the timeout).+withTimeout ::+  -- | Timeout duration (seconds)+  Timeout ->+  -- | Task to attempt+  IO a ->+  IO (Either TimedOut a)+withTimeout to task = do+  let timeout = do+        CC.threadDelay (timeoutToMicros to)+        pure TimedOut+  CCA.race timeout task