packages feed

crucible 0.7.2 → 0.10

raw patch · 58 files changed

Files

CHANGELOG.md view
@@ -1,3 +1,59 @@+# 0.10 -- 2026-09-10++* Add support for GHC 9.12 (at 9.12.2) and bump from 9.10.1 to 9.10.3.+* Fix `uniquelyConcRegMap` blocking clause: use disjunction (OR) instead of+  conjunction (AND). The old code would falsely report a `RegMap` as uniquely+  concretized whenever any single component was unique, even if other components+  had multiple possible values.+* **BREAKING:** Rename various bits associated with the "breakpoint"+  feature in accordance with renaming the feature to "cut" or+  "cutpoint".+  Exported Haskell symbols renamed:+  - `Lang.Crucible.Simulator.Breakpoint` -> `Lang.Crucible.Simulator.Cut`+  - `BreakpointName` -> `CutpointName`+  - `Breakpoint` -> `Cut`+  - `addBreakpointStmt` -> `addCutStmt`+  - `breakAndReturn` -> `cutAndReturn`+  - `breakpointPostdomInfo` -> `cutpointPostdomInfo`+  - `cfgBreakpoints` -> `cfgCutpoints`+  - `setFrameBreakpointPostdomInfo` -> `setFrameCutpointPostdomInfo`+* Add `reverseSymSequence` to `Lang.Crucible.Simulator.SymSequence`+* **BREAKING:** Add `FloatRound` constructor tp `App` in+  `Lang.Crucible.CFG.Expr` for rounding floating-point values to the nearest+  representable integral value.+* **BREAKING:** Add `SequenceReverse` constructor to `App` in+  `Lang.Crucible.CFG.Expr` for reversing symbolic sequences.+* **BREAKING:** Change the signature of `getRecordedTrace` in+  `Lang.Crucible.Simulator.RecordAndReplay` to remove the `evalBool` parameter,+  as the implementation no longer concretizes the trace.+* Add `Lang.Crucible.Simulator.RecordAndReplay.getConcreteRecordedTrace` for+  performant trace reversal when concretization is desired.+* Add `withStateBackend` and additional infrastructure for including stack+  traces in `SimError` and `IsSymBackend`+* Fix `onlineProve` to properly negate goals before checking satisfiability+* Avoid sending trivially-true goals to the solver in `Backend.Prove`.+* Fix bug in `execResultGlobals` that caused it to erroneously always return the+  non-aborted branch of a `FinishedResult ... (PartialRes ...)`.++# 0.9 -- 2026-01-29++# 0.8.0 -- 2025-11-09++* Add `setExecResultContext`, `setExecStateContext`+* Add `Lang.Crucible.Simulator.RecordAndReplay`, a module with two new execution+  features for recording and replaying control-flow traces.+* Add a `GlobalPair` argument to `AbortedExit`.+* Add new helpers for extracting `SymGlobalState`s: `exec{Result,State}Globals`.+* Add `typedOverride` for constructing `TypedOverride`s with statically-known+  signatures.+* Add `bindTypedOverride` for binding `TypedOverride`s to `FnHandle`s.+* Add `FunctorF`, `FoldableF`, and `TraversableF` instances for `CrucibleEvent`,+  `CrucibleAssumption`, and `CrucibleAssumptions`.+* Add `gcAddTopLevelAssume`, for making top-level assumptions.+* Rename functions in `Lang.Crucible.Concretize` to match What4's conventions.+  In particular, rename  `concRegValue` to `groundRegValue`, `concRegEntry` to+  `groundRegEntry`, and `concRegMap` to `groundRegMap`.+ # 0.7.2 -- 2025-03-21  * Add support for Bitwuzla as an online SMT solver backend.
crucible.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crucible-Version:       0.7.2+Version:       0.10 Author:        Galois Inc. Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com Copyright:     (c) Galois, Inc 2014-2022@@ -14,6 +14,9 @@   (SSA) form control flow graphs, and a symbolic simulation engine for executing   programs expressed in this format.  It also provides support for communicating with   a variety of SAT and SMT solvers, including Z3, CVC4, Yices, STP, and dReal.+  .+  For an overview of Crucible please have a look at "Lang.Crucible.README"+   extra-doc-files: CHANGELOG.md  source-repository head@@ -31,12 +34,120 @@   Default: True  common bldflags-  ghc-options: -Wall-               -Werror=incomplete-patterns-               -Werror=missing-methods-               -Werror=overlapping-patterns-               -Wpartial-fields-               -Wincomplete-uni-patterns+  -- Note [Export lists]+  -- -------------------+  --+  -- We don't allow modules without export lists.+  --+  -- From the GHC docs:+  --+  --     Declaring an explicit export list [...] enables GHC dead code analysis,+  --     prevents accidental export of names and can ease optimizations like+  --     inlining.+  --+  -- It also makes it easier to organize the Haddocks using section headers, and+  -- allows for internal/hidden definitions and constructors.+  --+  -- We can't use -Werror=missing-export-lists here because it interferes with+  -- ghcid. However, we enable it in CI, see ../cabal.project.ci.+  ghc-options:+    -Wmissing-export-lists++  -- Specifying -Wall and -Werror can cause the project to fail to build on+  -- newer versions of GHC simply due to new warnings being added to -Wall. To+  -- prevent this from happening we manually list which warnings should be+  -- considered errors. We also list some warnings that are not in -Wall, though+  -- try to avoid "opinionated" warnings (though this judgement is clearly+  -- subjective).+  --+  -- Warnings are grouped by the GHC version that introduced them, and then+  -- alphabetically.+  --+  -- A list of warnings and the GHC version in which they were introduced is+  -- available here:+  -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html++  -- Since GHC 9.6 or earlier:+  ghc-options:+    -Wall+    -Werror=ambiguous-fields+    -Werror=deferred-type-errors+    -Werror=deprecated-flags+    -Werror=deprecations+    -Werror=deriving-defaults+    -Werror=deriving-typeable+    -Werror=dodgy-foreign-imports+    -Werror=duplicate-exports+    -Werror=empty-enumerations+    -Werror=gadt-mono-local-binds+    -Werror=identities+    -Werror=inaccessible-code+    -Werror=incomplete-patterns+    -Werror=incomplete-record-updates+    -Werror=incomplete-uni-patterns+    -Werror=inline-rule-shadowing+    -Werror=misplaced-pragmas+    -Werror=missed-extra-shared-lib+    -Werror=missing-exported-signatures+    -Werror=missing-fields+    -Werror=missing-home-modules+    -Werror=missing-methods+    -Werror=missing-pattern-synonym-signatures+    -Werror=missing-signatures+    -Werror=name-shadowing+    -Werror=noncanonical-monad-instances+    -Werror=noncanonical-monoid-instances+    -Werror=operator-whitespace+    -Werror=operator-whitespace-ext-conflict+    -Werror=orphans+    -Werror=overflowed-literals+    -Werror=overlapping-patterns+    -Werror=partial-fields+    -Werror=partial-type-signatures+    -Werror=redundant-bang-patterns+    -Werror=redundant-record-wildcards+    -Werror=redundant-strictness-flags+    -Werror=simplifiable-class-constraints+    -Werror=star-binder+    -Werror=star-is-type+    -Werror=tabs+    -Werror=type-defaults+    -Werror=typed-holes+    -Werror=type-equality-out-of-scope+    -Werror=type-equality-requires-operators+    -Werror=unicode-bidirectional-format-characters+    -Werror=unrecognised-pragmas+    -Werror=unrecognised-warning-flags+    -Werror=unsupported-calling-conventions+    -Werror=unsupported-llvm-version+    -Werror=unused-do-bind+    -Werror=unused-imports+    -Werror=unused-record-wildcards+    -Werror=warnings-deprecations+    -Werror=wrong-do-bind++  if impl(ghc < 9.8)+    ghc-options:+      -Werror=forall-identifier++  if impl(ghc >= 9.8)+    ghc-options:+      -Werror=incomplete-export-warnings+      -Werror=inconsistent-flags++  if impl(ghc >= 9.10)+    ghc-options:+      -Werror=badly-staged-types+      -Werror=data-kinds-tc+      -Werror=incomplete-record-selectors+              +  if impl(ghc < 9.12)+    ghc-options:+      -Werror=compat-unqualified-imports++  -- TODO(#1308): Enable and fix this warning when GHC 9.6 is dropped from CI+  -- -Werror=deprecated-type-abstractions+   ghc-prof-options: -O2 -fprof-auto-exported   default-language: Haskell2010 @@ -45,7 +156,7 @@   import: bldflags   build-depends:     async,-    base >= 4.13 && < 4.20,+    base >= 4.13 && < 4.22,     bimap,     bv-sized >= 1.0.0 && < 1.1,     containers >= 0.5.9.0,@@ -53,15 +164,17 @@     fgl,     hashable,     json >= 0.9 && < 1.0,-    lens,+    microlens >= 0.5,+    microlens-mtl,+    microlens-th,     mtl,     panic >= 0.3,-    parameterized-utils >= 1.0.8 && < 2.2,+    parameterized-utils >= 2.3 && < 2.4,     prettyprinter >= 1.7.0,     template-haskell,     text,     time >= 1.8 && < 2.0,-    th-abstraction >=0.1 && <0.7,+    th-abstraction >=0.1 && <0.8,     transformers,     unordered-containers,     vector,@@ -78,7 +191,6 @@    exposed-modules:     Lang.Crucible.Analysis.DFS-    Lang.Crucible.Analysis.ForwardDataflow     Lang.Crucible.Analysis.Fixpoint     Lang.Crucible.Analysis.Fixpoint.Components     Lang.Crucible.Analysis.Postdom@@ -101,11 +213,12 @@     Lang.Crucible.CFG.SSAConversion     Lang.Crucible.CFG.EarlyMergeLoops     Lang.Crucible.FunctionHandle+    Lang.Crucible.README     Lang.Crucible.Simulator-    Lang.Crucible.Simulator.Breakpoint     Lang.Crucible.Simulator.BoundedExec     Lang.Crucible.Simulator.BoundedRecursion     Lang.Crucible.Simulator.CallFrame+    Lang.Crucible.Simulator.Cut     Lang.Crucible.Simulator.Evaluation     Lang.Crucible.Simulator.EvalStmt     Lang.Crucible.Simulator.ExecutionTree@@ -117,6 +230,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 +277,20 @@   import: bldflags   type: exitcode-stdio-1.0   hs-source-dirs: test/helpers---  other-modules:+  other-modules:+    SymSequence+    SymSequence.Properties+    SymSequence.Reverse   main-is: Main.hs   build-depends: base,                  hspec >= 2.5,                  crucible,-                 lens,+                 hedgehog,+                 microlens,                  panic >= 0.3,                  parameterized-utils,                  tasty >= 0.10,                  tasty-hspec >= 1.1,+                 tasty-hedgehog >= 1.2,                  tasty-hunit,                  what4
src/Lang/Crucible/Analysis/Fixpoint.hs view
@@ -51,11 +51,13 @@   ) where  import           Control.Applicative-import           Control.Lens.Operators ( (^.), (%=), (.~), (&), (%~) ) import qualified Control.Monad.State.Strict as St+import           Data.Function ((&)) import qualified Data.Functor.Identity as I import           Data.Kind import qualified Data.Set as S+import           Lens.Micro ((^.), (.~), (%~))+import           Lens.Micro.Mtl ((%=)) import           Text.Printf  import           Prelude@@ -68,6 +70,7 @@ import           Lang.Crucible.CFG.Core import           Lang.Crucible.CFG.Extension import           Lang.Crucible.Analysis.Fixpoint.Components+import           Lang.Crucible.Panic (panic)  -- | A wrapper around widening strategies data WideningStrategy = WideningStrategy (Int -> Bool)@@ -472,14 +475,14 @@           let assignment' = interpWriteGlobal interp gv reg assignment           in maybe assignment (joinPointAbstractions dom assignment) assignment' -        FreshConstant{} -> error "transferStmt: FreshConstant not supported"-        FreshFloat{} -> error "transferStmt: FreshFloat not supported"-        FreshNat{} -> error "transferStmt: FreshNat not supported"-        NewEmptyRefCell{} -> error "transferStmt: NewEmptyRefCell not supported"-        NewRefCell {} -> error "transferStmt: NewRefCell not supported"-        ReadRefCell {} -> error "transferStmt: ReadRefCell not supported"-        WriteRefCell {} -> error "transferStmt: WriteRefCell not supported"-        DropRefCell {} -> error "transferStmt: DropRefCell not supported"+        FreshConstant{} -> panic "transferStmt" ["FreshConstant not supported"]+        FreshFloat{} -> panic "transferStmt" ["FreshFloat not supported"]+        FreshNat{} -> panic "transferStmt" ["FreshNat not supported"]+        NewEmptyRefCell{} -> panic "transferStmt" ["NewEmptyRefCell not supported"]+        NewRefCell {} -> panic "transferStmt" ["NewRefCell not supported"]+        ReadRefCell {} -> panic "transferStmt" ["ReadRefCell not supported"]+        WriteRefCell {} -> panic "transferStmt" ["WriteRefCell not supported"]+        DropRefCell {} -> panic "transferStmt" ["DropRefCell not supported"]      -- Transfer a block terminator statement.     transferTerm :: forall ctx'@@ -528,7 +531,7 @@           isRetAbstr %= domJoin dom absVal           return S.empty -        VariantElim {} -> error "transferTerm: VariantElim terminator not supported"+        VariantElim {} -> panic "transferTerm" ["VariantElim terminator not supported"]       transferJump :: forall ctx'
src/Lang/Crucible/Analysis/Fixpoint/Components.hs view
@@ -40,6 +40,7 @@ import           Data.Parameterized.Some (Some(Some)) import           Lang.Crucible.CFG.Core (CFG, BlockID) import qualified Lang.Crucible.CFG.Core as CFG+import           Lang.Crucible.Panic (panic)  -- | Compute a weak topological ordering over a control flow graph. --@@ -109,7 +110,7 @@                   -- Otherwise, unwind the stack and add a full component                 unwindStack elt v                 makeComponent v-        Nothing -> error "Pop attempted on empty stack (Components:visit)"+        Nothing -> panic "visit" ["Pop attempted on empty stack"]   -- We return the least label in the strongly-connected component   -- containing this vertex, which is used if we have to unwind back   -- to the SCC head vertex.
− src/Lang/Crucible/Analysis/ForwardDataflow.hs 
@@ -1,309 +0,0 @@---------------------------------------------------------------------------- |--- Module      : Lang.Crucible.Analysis.ForwardDataflow--- Description : Forward dataflow analysis framework based on Kildall's algorithm--- Copyright   : (c) Galois, Inc 2015--- License     : BSD3--- Maintainer  : Rob Dockins <rdockins@galois.com>--- Stability   : provisional------ This module defines a generic framework for forward dataflow analysis,--- with some additional control-flow data on the side.------ We calculate a fixpoint of a given analysis via the straightforward--- method of iterating the transfer function until no more updates occur.------ Our current method for doing this is quite naive, and more efficient--- methods exist.---------------------------------------------------------------------------{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeSynonymInstances #-}--module Lang.Crucible.Analysis.ForwardDataflow-{-# DEPRECATED "Lang.Crucible.Analysis.Fixpoint is a better implementation of these ideas" #-}-where--import           Control.Lens-import           Control.Monad.State.Strict-import           Data.Kind-import           Data.Parameterized.Context ( Assignment )-import qualified Data.Parameterized.Context as Ctx-import           Data.Parameterized.TraversableFC-import           Data.Set (Set)-import qualified Data.Set as Set-import           Prelude hiding (foldr)-import           Prettyprinter---import           Lang.Crucible.Types-import           Lang.Crucible.CFG.Core-import           Lang.Crucible.CFG.Expr--import qualified Debug.Trace as Debug--------------------------data SymDom = Dead | Symbolic | Concrete-  deriving (Eq, Ord, Show)--symbolicResults-   :: IsSyntaxExtension ext-   => CFG ext blocks init ret-   -- -> Assignment (Ignore SymDom) init-   -> String-   -- -> (Assignment (KildallPair (Assignment (Ignore SymDom)) SymDom) blocks, Ignore SymDom ret, SymDom)-symbolicResults cfg = show $ kildall_forward symbolicAnalysis cfg (begin, Concrete)- where sz = Ctx.size (blockInputs (getBlock (cfgEntryBlockID cfg) (cfgBlockMap cfg)))-       begin = Ctx.generate sz (\_ -> Ignore Symbolic)---symlub :: SymDom -> SymDom -> SymDom-symlub Dead x = x-symlub x Dead = x-symlub Symbolic _ = Symbolic-symlub _ Symbolic = Symbolic-symlub Concrete Concrete = Concrete--sym_reg_transfer :: Reg ctx tp -> Assignment (Ignore SymDom) ctx -> SymDom-sym_reg_transfer reg asgn = ignoreOut $ asgn Ctx.! (regIndex reg)--sym_expr_transfer :: IsSyntaxExtension ext => Expr ext ctx tp -> Assignment (Ignore SymDom) ctx -> SymDom-sym_expr_transfer (App a) asgn-  = foldApp (\r z -> symlub z $ sym_reg_transfer r asgn) Dead a---- FIXME this whole shabang is bogus, and should be replace by something that works...--- we assume every function other than "matlabFunctionHandle" returns a symbolic--- output, but does not have control flow that depends on symbolic data...-sym_call_transfer-  :: CtxRepr args-  -> TypeRepr ret-  -> Reg ctx (FunctionHandleType args ret)-  -> Ignore SymDom (FunctionHandleType args ret)-  -> Assignment a args-  -> Ignore SymDom ret-sym_call_transfer _ _ ex _ _-  = Debug.trace (show $ pretty ex) $ Ignore Symbolic--symbolicAnalysis :: IsSyntaxExtension ext => KildallForward ext blocks (Ignore SymDom) SymDom-symbolicAnalysis =-  KildallForward-  { kfwd_lub = \(Ignore x) (Ignore y) -> Ignore (symlub x y)-  , kfwd_bot = Ignore Dead-  , kfwd_club = symlub-  , kfwd_cbot = Dead-  , kfwd_same = \(Ignore x) (Ignore y) -> x == y-  , kfwd_csame = \x y -> x == y-  , kfwd_br = \_ (Ignore x) y -> let z = symlub x y in (z, z)-  , kfwd_maybe = \_ _ (Ignore x) y -> let z = symlub x y in (z, Ignore x, z)-  , kfwd_reg  = \_ ex asgn -> Ignore $ sym_reg_transfer ex asgn-  , kfwd_expr = \_ ex asgn -> Ignore $ sym_expr_transfer ex asgn-  , kfwd_call = sym_call_transfer-  , kfwd_rdglobal = \_ -> Ignore Symbolic-             -- FIXME, here we make the totally pessimistic assumption-             -- that every global variable read is symbolic-  , kfwd_onentry = \_ x -> x-  }-----------------------data KildallPair (a::k -> Type) (c :: Type) (tp::k) = KP (a tp) c--instance (ShowF a, Show c) => Show (KildallPair a c tp) where-  show (KP x y) = "(" ++ showF x ++ ", " ++ show y ++ ")"--instance (ShowF a, Show c) => ShowF (KildallPair a c)--newtype Ignore a (b::k) = Ignore { ignoreOut :: a }- deriving (Eq, Ord)--instance Show a => Show (Ignore a tp) where-  show (Ignore x) = show x--instance Show a => ShowF (Ignore a)---data KildallForward ext blocks (a :: CrucibleType -> Type) c-  = KildallForward-    { kfwd_lub      :: forall tp. a tp -> a tp -> a tp-    , kfwd_bot      :: forall tp. a tp-    , kfwd_club     :: c -> c -> c-    , kfwd_cbot     :: c-    , kfwd_same     :: forall tp. a tp -> a tp -> Bool-    , kfwd_csame    :: c -> c -> Bool-    , kfwd_br       :: forall ctx. Reg ctx BoolType -> a BoolType -> c -> (c, c)-    , kfwd_maybe    :: forall ctx tp. TypeRepr tp -> Reg ctx (MaybeType tp) -> a (MaybeType tp) -> c -> (c, a tp, c)-    , kfwd_reg      :: !(forall ctx tp. TypeRepr tp -> Reg ctx tp  -> Assignment a ctx -> a tp)-    , kfwd_expr     :: !(forall ctx tp. TypeRepr tp -> Expr ext ctx tp -> Assignment a ctx -> a tp)-    , kfwd_call     :: forall ctx args ret. CtxRepr args-                                         -> TypeRepr ret-                                         -> Reg ctx (FunctionHandleType args ret)-                                         -> a (FunctionHandleType args ret)-                                         -> Assignment a args-                                         -> a ret-    , kfwd_rdglobal :: forall tp. GlobalVar tp -> a tp-    , kfwd_onentry  :: forall ctx. BlockID blocks ctx -> (Assignment a ctx, c) -> (Assignment a ctx, c)-    }--kildall_transfer-   :: forall ext a c blocks ret ctx-    . KildallForward ext blocks a c-   -> TypeRepr ret-   -> Block ext blocks ret ctx-   -> (Assignment a ctx, c)-   -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks)))-kildall_transfer analysis retRepr blk = transfer_seq (_blockStmts blk)- where transfer_seq :: forall ctx'-                     . StmtSeq ext blocks ret ctx'-                    -> (Assignment a ctx', c)-                    -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks)))--       transfer_seq (ConsStmt _loc stmt ss) x = transfer_seq ss (transfer_stmt stmt x)-       transfer_seq (TermStmt _loc term) x = transfer_term term x--       transfer_stmt :: forall ctx1 ctx2. Stmt ext ctx1 ctx2 -> (Assignment a ctx1, c) -> (Assignment a ctx2, c)-       transfer_stmt (SetReg tp ex) (asgn, c) = (Ctx.extend asgn (kfwd_expr analysis tp ex asgn), c)-       transfer_stmt (CallHandle rettp ex argstp actuals) (asgn, c) =-           let xs = Ctx.zipWith (\tp act -> kfwd_reg analysis tp act asgn) argstp actuals-               ex_sh = kfwd_reg analysis (FunctionHandleRepr argstp rettp) ex asgn-               a' = kfwd_call analysis argstp rettp ex ex_sh xs-            in (Ctx.extend asgn a', c)-       transfer_stmt (Print _) asgn = asgn-       transfer_stmt (ReadGlobal gv) (asgn, c) = (Ctx.extend asgn (kfwd_rdglobal analysis gv), c)-       transfer_stmt FreshConstant{} _ = error "forward dataflow: fresh constant!"-       transfer_stmt FreshFloat{} _ = error "forward dataflow: fresh float!"-       transfer_stmt FreshNat{} _ = error "forward dataflow: fresh nat!"-       transfer_stmt ExtendAssign{} _ = error "extension statement!"-       transfer_stmt NewRefCell{} _ = error "forward dataflow: reference cell!"-       transfer_stmt NewEmptyRefCell{} _ = error "forward dataflow: reference cell!"-       transfer_stmt ReadRefCell{} _ = error "forward dataflow: reference cell!"-       transfer_stmt WriteRefCell{} _ = error "forward dataflow: reference cell!"-       transfer_stmt DropRefCell{} _ = error "forward dataflow: reference cell!"-       transfer_stmt (WriteGlobal _ _) asgnc = asgnc -- FIXME? need to check something here, perhaps?-       transfer_stmt (Assert _ _) asgnc = asgnc -- FIXME? is it useful to remember assertions some way?-       transfer_stmt (Assume _ _) asgnc = asgnc -- FIXME? is it useful to remember assertions some way?--       transfer_term :: forall ctx'-                      . TermStmt blocks ret ctx'-                     -> (Assignment a ctx', c)-                     -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks)))--       transfer_term (ErrorStmt _) _ = return Set.empty--       transfer_term (Jump tgt) x = transfer_jump tgt x--       transfer_term (Br ex tgt1 tgt2) (asgn,c) = do-           let a = kfwd_reg analysis knownRepr ex asgn-           let (c1,c2) = kfwd_br analysis ex a c-           s1 <- transfer_jump tgt1 (asgn,c1)-           s2 <- transfer_jump tgt2 (asgn,c2)-           return (Set.union s1 s2)--       transfer_term (Return ex) (asgn, c) = do-           let a = kfwd_reg analysis retRepr ex asgn-           modify (\ (x,r,rc) -> (x, kfwd_lub analysis r a, kfwd_club analysis rc c))-           return Set.empty--       transfer_term (TailCall fn callargs actuals) (asgn, c) = do-           let xs = Ctx.zipWith (\tp act -> kfwd_reg analysis tp act asgn) callargs actuals-           let fn_sh = kfwd_reg analysis (FunctionHandleRepr callargs retRepr) fn asgn-           let a' = kfwd_call analysis callargs retRepr fn fn_sh xs-           modify (\ (x,r,rc) -> (x, kfwd_lub analysis r a', kfwd_club analysis rc c))-           return Set.empty--       transfer_term (MaybeBranch tp ex swtgt jmptgt) (asgn, c) = do-           let a = kfwd_reg analysis (MaybeRepr tp) ex asgn-           let (c1, a1, c2) = kfwd_maybe analysis tp ex a c-           s1 <- transfer_switch swtgt a1 (asgn, c1)-           s2 <- transfer_jump jmptgt (asgn, c2)-           return (Set.union s1 s2)--       transfer_term (VariantElim _ctx _ex _switch) (_asgn, _c) = do-           error "FIXME: transfer_term for VariantElim not implemented"--       transfer_switch :: forall ctx' tp-                        . SwitchTarget blocks ctx' tp-                       -> a tp-                       -> (Assignment a ctx', c)-                       -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks)))-       transfer_switch (SwitchTarget tgt argstp actuals) a1 (asgn, c) = do-           let xs = Ctx.zipWith (\tp act -> kfwd_reg analysis tp act asgn) argstp actuals-           let xs' = Ctx.extend xs a1-           transfer_target tgt (xs', c)--       transfer_jump :: forall ctx'-                      . JumpTarget blocks ctx'-                     -> (Assignment a ctx', c)-                     -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks)))--       transfer_jump (JumpTarget tgt argstp actuals) (asgn, c) = do-           let xs = Ctx.zipWith (\tp act -> kfwd_reg analysis tp act asgn) argstp actuals-           transfer_target tgt (xs, c)--       transfer_target :: forall ctx'-                        . BlockID blocks ctx'-                       -> (Assignment a ctx', c)-                       -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks)))-       transfer_target tgt@(BlockID idx) (asgn, c) = do-           (x,r,rc) <- get-           let KP old oldc = x Ctx.! idx-           let new = Ctx.zipWith (\a b -> kfwd_lub analysis a b) old asgn-           let zipsame = Ctx.zipWith (\a b -> Ignore $ kfwd_same analysis a b) old new-           let samex = foldlFC (\a (Ignore b) -> a && b) True zipsame-           let newc = kfwd_club analysis c oldc-           let same = samex && kfwd_csame analysis oldc newc-           if same-               then return Set.empty-               else do put (x & ixF idx .~ KP new newc, r, rc)-                       return (Set.singleton (Some tgt))----kildall_forward-  :: forall ext a c blocks ret init-   . KildallForward ext blocks a c-  -> CFG ext blocks init ret-  -> (Assignment a init, c)-  -> (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)-kildall_forward analysis cfg (asgn0,c0) =-    let initblk@(BlockID idx) = cfgEntryBlockID cfg--        freshAsgn :: Ctx.Index blocks ctx -> Assignment a ctx-        freshAsgn i = fmapFC (\_ -> kfwd_bot analysis)-                             (blockInputs (getBlock (BlockID i) (cfgBlockMap cfg)))--     in execState (loop (Set.singleton (Some initblk)))-                  ( Ctx.generate (Ctx.size (cfgBlockMap cfg)) $ \i ->-                      case testEquality i idx of-                        Just Refl -> KP asgn0 c0-                        Nothing -> KP (freshAsgn i) (kfwd_cbot analysis)-                  , kfwd_bot analysis-                  , kfwd_cbot analysis-                  )--  where visit :: Block ext blocks ret ctx-              -> (Assignment a ctx, c)-              -> Set (Some (BlockID blocks))-              -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) ()-        visit blk start worklist = do-            s <- kildall_transfer analysis (cfgReturnType cfg) blk start-            loop (Set.union s worklist)--        loop worklist =-           case Set.minView worklist of-              Nothing -> return ()-              Just (Some tgt@(BlockID idx), worklist') ->-                  do (x,_,_) <- get-                     let (KP a c) = x Ctx.! idx-                         (a',c') = kfwd_onentry analysis tgt (a,c)-                     visit (getBlock tgt (cfgBlockMap cfg)) (a',c') worklist'
src/Lang/Crucible/Analysis/Postdom.hs view
@@ -15,7 +15,7 @@ {-# LANGUAGE TupleSections #-} module Lang.Crucible.Analysis.Postdom   ( postdomInfo-  , breakpointPostdomInfo+  , cutpointPostdomInfo   , validatePostdom   ) where @@ -49,12 +49,12 @@     Just l -> (\(Some n) -> toNode n `reverseEdge` b) <$> l  inEdgeGraph :: BlockMap ext blocks ret -> [Some (BlockID blocks)] -> G.UGr-inEdgeGraph m breakpointIds = G.mkGraph ((,()) <$> nodes) edges+inEdgeGraph m cutpointIds = G.mkGraph ((,()) <$> nodes) edges   where nodes = 0 : toListFC (toNode . blockID) m         cfgEdges = foldMapFC inEdges m-        breakpointEdges = map (\(Some bid) -> reverseEdge 0 (getBlock bid m))-                              breakpointIds-        edges = cfgEdges ++ breakpointEdges+        cutpointEdges = map (\(Some bid) -> reverseEdge 0 (getBlock bid m))+                              cutpointIds+        edges = cfgEdges ++ cutpointEdges  -- | Return subgraph of nodes reachable from given node. reachableSubgraph :: G.Node -> G.UGr -> G.UGr@@ -76,8 +76,8 @@             . BlockMap ext blocks ret            -> [Some (BlockID blocks)]            -> Map (Some (BlockID blocks)) [Some (BlockID blocks)]-postdomMap m breakpointIds = r-  where g0 = inEdgeGraph m breakpointIds+postdomMap m cutpointIds = r+  where g0 = inEdgeGraph m cutpointIds         g = reachableSubgraph 0 g0          idMap = nodeToBlockIDMap m@@ -98,8 +98,8 @@                    . BlockMap ext blocks ret                   -> [Some (BlockID blocks)]                   -> CFGPostdom blocks-postdomAssignment m breakpointIds = fmapFC go m-  where pd = postdomMap m breakpointIds+postdomAssignment m cutpointIds = fmapFC go m+  where pd = postdomMap m cutpointIds         go :: Block ext blocks ret c -> Const [Some (BlockID blocks)] c         go b = Const $ fromMaybe [] (Map.lookup (Some (blockID b)) pd) @@ -107,9 +107,9 @@ postdomInfo :: CFG ext b i r -> CFGPostdom b postdomInfo g = postdomAssignment (cfgBlockMap g) [] -breakpointPostdomInfo :: CFG ext b i r -> [BreakpointName] -> CFGPostdom b-breakpointPostdomInfo g breakpointNames = postdomAssignment (cfgBlockMap g) $-  mapMaybe (\nm -> Bimap.lookup nm (cfgBreakpoints g)) breakpointNames+cutpointPostdomInfo :: CFG ext b i r -> [CutpointName] -> CFGPostdom b+cutpointPostdomInfo g cutpointNames = postdomAssignment (cfgBlockMap g) $+  mapMaybe (\nm -> Bimap.lookup nm (cfgCutpoints g)) cutpointNames  blockEndsWithError :: Block ext blocks ret args -> Bool blockEndsWithError b =
src/Lang/Crucible/Analysis/Reachable.hs view
@@ -98,7 +98,7 @@ exploreReachable' _ [] r = r exploreReachable' m (Some h:l) r =   case Map.lookup (Some h) r of-    Just c -> exploreReachable' m l (Map.insert (Some h) (c+1) r)+    Just c -> exploreReachable' m l (Map.insert (Some h) (c + 1) r)     Nothing -> do       let b = getBlock h m       exploreReachable' m (nextBlocks b ++ l) (Map.insert (Some h) 1 r)@@ -119,11 +119,11 @@                  SomeCFG g'         where oldToNew = mkOldMap newToOld               new_map = remapBlockMap oldToNew newToOld-              new_breakpoints = Bimap.mapR (mapSome $ remapBlockID oldToNew) (cfgBreakpoints g)+              new_cutpoints = Bimap.mapR (mapSome $ remapBlockID oldToNew) (cfgCutpoints g)               g' = CFG { cfgHandle = cfgHandle g                        , cfgBlockMap = new_map                        , cfgEntryBlockID = remapBlockID oldToNew entry_id-                       , cfgBreakpoints = new_breakpoints+                       , cfgCutpoints = new_cutpoints                        }   where old_map = cfgBlockMap g         entry_id = cfgEntryBlockID g
src/Lang/Crucible/Backend.hs view
@@ -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,16 +81,17 @@   , ppProofObligation   , backendOptions   , assertThenAssumeConfigOption+  , ppAssumptionState   ) where  import           Control.Exception(Exception(..), throwIO)-import           Control.Lens ((^.)) import           Control.Monad import           Control.Monad.IO.Class import           Data.Foldable (toList) import           Data.Set (Set)-import qualified Prettyprinter as PP import           GHC.Stack+import           Lens.Micro ((^.))+import qualified Prettyprinter as PP  import           Data.Parameterized.Map (MapF) @@ -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,17 @@   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)++  -- | An additional exception context for more detailed SimErrors+  getExceptionContext :: bak -> Maybe ProgramStack++  -- | Make a backend just like this but with a different error context+  withExceptionContext :: bak -> ProgramStack -> bak + assertThenAssumeConfigOption :: ConfigOption BaseBoolType assertThenAssumeConfigOption = configOption knownRepr "assertThenAssume" @@ -368,7 +381,8 @@ assert bak p msg =   do let sym = backendGetSym bak      loc <- getCurrentProgramLoc sym-     addAssertion bak (LabeledPred p (SimError loc msg))+     let ctx = getExceptionContext bak+     addAssertion bak (LabeledPred p (mkSimError loc msg ctx))  -- | Add a proof obligation for False. This always aborts execution -- of the current path, because after asserting false, we get to assume it,@@ -378,7 +392,8 @@ addFailedAssertion bak msg =   do let sym = backendGetSym bak      loc <- getCurrentProgramLoc sym-     let err = SimError loc msg+     let ctx = getExceptionContext bak+     let err = mkSimError loc msg ctx      addProofObligation bak (LabeledPred (falsePred sym) err)      abortExecBecause (AssertionFailure err) @@ -417,7 +432,8 @@ readPartExpr bak (PE p v) msg = do   let sym = backendGetSym bak   loc <- getCurrentProgramLoc sym-  addAssertion bak (LabeledPred p (SimError loc msg))+  let ctx = getExceptionContext bak+  addAssertion bak (LabeledPred p (mkSimError loc msg ctx))   return v  @@ -489,4 +505,22 @@   ppGl =    PP.indent 2 $-   PP.vsep [ppSimError (gl^.labeledPredMsg), printSymExpr (gl^.labeledPred)]+   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+        ]+    ]
src/Lang/Crucible/Backend/AssumptionStack.hs view
@@ -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@@ -175,7 +176,7 @@     case gcPop gc of       Left (ident', _assumes, mg, gc1)         | ident == ident' -> (gc',n)-        | otherwise -> go (n+1) gc'+        | otherwise -> go (n + 1) gc'        where gc' = case mg of                      Nothing -> gc1                      Just g  -> gcAddGoals g gc1
src/Lang/Crucible/Backend/Assumptions.hs view
@@ -41,15 +41,19 @@   , assumptionsPred   , flattenAssumptions   , assumptionsTopLevelLocs+  , ppAssumptions'+  , ppAssumptions   ) where  -import           Control.Lens (Traversal, folded) import           Data.Kind (Type)-import           Data.Functor.Identity+import qualified Data.Foldable as F import           Data.Functor.Const-import qualified Data.Sequence as Seq+import           Data.Functor.Identity+import qualified Data.Parameterized.TraversableF as TF import           Data.Sequence (Seq)+import qualified Data.Sequence as Seq+import           Lens.Micro (Traversal, folded) import qualified Prettyprinter as PP  import           What4.Expr.Builder@@ -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
src/Lang/Crucible/Backend/Goals.hs view
@@ -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.
src/Lang/Crucible/Backend/Online.hs view
@@ -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,21 +78,19 @@   , withSTPOnlineBackend   ) where --import           Control.Lens ( (^.) ) import           Control.Monad-import           Control.Monad.Fix (mfix) import           Control.Monad.Catch+import           Control.Monad.Fix (mfix) import           Control.Monad.IO.Class import           Data.Bits import           Data.Data (Data) import           Data.Foldable import           Data.IORef-import           Data.Typeable (Typeable)-import           GHC.Generics (Generic)-import           System.IO import qualified Data.Text as Text+import           GHC.Generics (Generic)+import           Lens.Micro ((^.)) import qualified Prettyprinter as PP+import           System.IO  import           What4.Config import           What4.Concrete@@ -104,10 +111,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@@ -173,6 +183,8 @@     -- ^ action for checking if online features are currently enabled    , onlineExprBuilder :: B.ExprBuilder scope st fs++  , onlineExceptionContext :: !(Maybe ProgramStack)   }  newOnlineBackend ::@@ -181,7 +193,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 @@ -198,6 +210,7 @@                    , currentFeatures = featref                    , onlineEnabled = getOpt enableOpt                    , onlineExprBuilder = sym+                   , onlineExceptionContext = Nothing                    }  -- | Do something with an online backend.@@ -224,176 +237,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 +340,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 +356,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 +390,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 +399,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 +415,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 +432,188 @@     do restoreSolverState bak gc        -- restore the previous assumption stack        AS.restoreAssumptionStack gc (assumptionStack bak)++  getBackendState bak = readIORef (AS.proofObligations (assumptionStack bak))++  getExceptionContext = onlineExceptionContext+  withExceptionContext bak ec = bak { onlineExceptionContext = Just ec }++--------------------------------------------------------------------------------+-- 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)++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
src/Lang/Crucible/Backend/ProofGoals.hs view
@@ -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
src/Lang/Crucible/Backend/Prove.hs view
@@ -73,11 +73,11 @@   , 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           Lens.Micro ((^.))  import qualified What4.Interface as W4 import qualified What4.Expr as WE@@ -111,19 +111,21 @@ consumeGoalsWithAssumptions ::   forall asmp goal a.   Monoid asmp =>-  -- | Consume a 'Prove'+  -- | What to do at 'Assuming' nodes (e.g., call 'proverAssume')+  (asmp -> a -> a) ->+  -- | Consume a 'Prove' with accumulated assumptions   (asmp -> goal -> a) ->   -- | Consume a 'ProveConj'   (a -> a -> a) ->   CB.Goals asmp goal ->   a-consumeGoalsWithAssumptions onGoal onConj goals =+consumeGoalsWithAssumptions onAssumption 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)+      (\asmp gl -> onAssumption asmp <$> Reader.local (<> asmp) gl)       (\gl -> Reader.asks (\asmps -> onGoal asmps gl))       (\g1 g2 -> onConj <$> g1 <*> g2) @@ -255,6 +257,44 @@ --------------------------------------------------------------------- -- *** Offline +-- | Check if a goal is trivially true without calling the solver.+--+-- Returns a @Right@ with proof result if the goal is trivially true, or+-- @Left (asmps and not goal)@ if consulting the solver is needed. See the+-- module-level Haddock for intepreting @asmps and not goal@.+--+-- We don't optimize trivially false goals because we need the solver to provide+-- concrete counterexample values ('WE.GroundEvalFn') for debugging and error+-- reporting.+--+-- You might wonder if this is redundant with e.g., the check in @Backend@'s+-- @addProofObligation@ or with 'Crucible.Backend.Assumption.trivialAssumption'.+-- It is not. Consider a situation with fresh booleans @p@ and @q@ and+-- assumptions @p@ and @not p@ and goal @q@. What4's simplifications allow us+-- to conclude that the conjunction of the assumptions and the negation of the+-- goal is trivially unsatisfiable, even though each assumption and the goal are+-- individually nontrivial.+checkTrivialGoal ::+  W4.IsSymExprBuilder sym =>+  sym ->+  Assumptions sym ->+  CB.Assertion sym ->+  ProofConsumer sym t r ->+  IO (Either (W4.Pred sym) (SubgoalResult r))+checkTrivialGoal sym asmps goal (ProofConsumer k) = do+  -- See module Haddock for intepreting (asmps and not goal)+  asmpsPred <- CB.assumptionsPred sym asmps+  notGoal <- W4.notPred sym (goal ^. CB.labeledPred)+  asmpsAndNotGoal <- W4.andPred sym asmpsPred notGoal++  case W4.asConstantPred asmpsAndNotGoal of+    Just False ->  -- false = definitely unsat = proved+      let r' = Proved in+      Right <$> (SubgoalResult (isProved r') <$> k (CB.ProofGoal asmps goal) r')+    _ ->+      -- return this so that offlineProve doesn't need to re-compute it+      pure (Left asmpsAndNotGoal)+ -- Not exported offlineProveIO ::   (sym ~ WE.ExprBuilder t st fs) =>@@ -266,17 +306,18 @@   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'+offlineProveIO sym ld adapter asmps goal k@(ProofConsumer kFn) =+  checkTrivialGoal sym asmps goal k >>=+    \case+      Right result -> pure result+      Left asmpsAndNotGoal ->+        WSA.solver_adapter_check_sat adapter sym ld [asmpsAndNotGoal] $ \r ->+          let r' =+                case r of+                  W4R.Sat (gfn, binds) -> Disproved gfn binds+                  W4R.Unsat () -> Proved+                  W4R.Unknown -> Unknown+          in SubgoalResult (isProved r') <$> kFn (CB.ProofGoal asmps goal) r'  -- | Prove a goal using an \"offline\" solver (i.e., one process per goal). --@@ -353,19 +394,27 @@   W4SMT.SMTReadWriter solver =>   (sym ~ WE.ExprBuilder t st fs) =>   W4.IsSymExprBuilder sym =>+  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'+onlineProve sym sProc asmps goal k@(ProofConsumer kFn) =+  liftIO (checkTrivialGoal sym asmps goal k) >>=+    \case+      Right result -> pure result+      Left _ -> liftIO $ do+        -- Note: assumptions are established via proverAssume before this is called+        let goalPred = goal ^. CB.labeledPred+        notGoal <- W4.notPred sym goalPred+        WPO.checkSatisfiableWithModel sProc "prove" notGoal $ \r ->+          let r' =+                case r of+                  W4R.Sat gfn -> Disproved gfn Nothing+                  W4R.Unsat () -> Proved+                  W4R.Unknown -> Unknown+          in SubgoalResult (isProved r') <$> kFn (CB.ProofGoal asmps goal) r'  -- | Add an assumption by @push@ing a new frame ('WPO.inNewFrame'). onlineAssume :: @@ -404,7 +453,7 @@   Prover sym m t r onlineProver sym sProc =   Prover-  { proverProve = onlineProve sProc+  { proverProve = onlineProve sym sProc   , proverAssume = onlineAssume sym sProc   } @@ -421,6 +470,7 @@ proveGoals (ProofStrategy prover (Combiner comb)) goals k =   fmap subgoalResult $     consumeGoalsWithAssumptions+      (proverAssume prover)       (\asmps gl -> proverProve prover asmps gl k)       comb       goals
src/Lang/Crucible/Backend/Simple.hs view
@@ -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 #-}@@ -30,8 +30,9 @@   , B.Flags   ) where -import           Control.Lens ( (^.) ) import           Control.Monad (void)+import           Data.IORef (readIORef)+import           Lens.Micro ((^.))  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.@@ -55,8 +56,10 @@   SimpleBackend   { sbAssumptionStack :: AS t   , sbExprBuilder :: B.ExprBuilder t st fs+  , sbExceptionContext :: Maybe ProgramStack   } + newSimpleBackend ::   B.ExprBuilder t st fs ->   IO (SimpleBackend t st fs)@@ -66,6 +69,7 @@      return SimpleBackend             { sbAssumptionStack = as             , sbExprBuilder = sym+            , sbExceptionContext = Nothing             }  instance HasSymInterface (B.ExprBuilder t st fs) (SimpleBackend t st fs) where@@ -111,3 +115,8 @@    restoreAssumptionState bak newstk = do     AS.restoreAssumptionStack newstk (sbAssumptionStack bak)++  getBackendState bak = readIORef (AS.proofObligations (sbAssumptionStack bak))++  withExceptionContext bak ec = bak { sbExceptionContext = Just ec }+  getExceptionContext = sbExceptionContext
src/Lang/Crucible/CFG/Common.hs view
@@ -15,7 +15,7 @@   ( -- * Global variables     GlobalVar(..)   , freshGlobalVar-  , BreakpointName(..)+  , CutpointName(..)   ) where  import           Data.Text (Text)@@ -65,8 +65,8 @@          , globalType  = tp          } -newtype BreakpointName = BreakpointName { breakpointNameText :: Text }+newtype CutpointName = CutpointName { cutpointNameText :: Text }   deriving (Eq, Ord, Show) -instance Pretty BreakpointName where-  pretty = pretty . breakpointNameText+instance Pretty CutpointName where+  pretty = pretty . cutpointNameText
src/Lang/Crucible/CFG/Core.hs view
@@ -91,7 +91,6 @@   ) where  import Control.Applicative-import Control.Lens import Data.Bimap (Bimap) import Data.Maybe (fromMaybe) import Data.Kind (Type)@@ -100,6 +99,7 @@ import Data.Parameterized.Some import Data.Parameterized.TraversableFC import Data.String+import Lens.Micro ((^.), Lens', lens) import Prettyprinter  import What4.ProgramLoc@@ -673,19 +673,19 @@              -- ^ The sequence of statements in this block            } -blockStmts :: Simple Lens (Block ext b r c) (StmtSeq ext b r c)+blockStmts :: Lens' (Block ext b r c) (StmtSeq ext b r c) blockStmts = lens _blockStmts (\b s -> b { _blockStmts = s })  -- | Return location of start of block. blockLoc :: Block ext blocks ret ctx -> ProgramLoc-blockLoc b = firstStmtLoc (b^.blockStmts)+blockLoc b = firstStmtLoc (b ^. blockStmts)  -- | Get the terminal statement of a basic block.  This is implemented -- in a CPS style due to the block context. withBlockTermStmt :: Block ext blocks ret args                   -> (forall ctx . ProgramLoc -> TermStmt blocks ret ctx -> r)                   -> r-withBlockTermStmt b f = getConst (stmtSeqTermStmt (Const . uncurry f) (b^.blockStmts))+withBlockTermStmt b f = getConst (stmtSeqTermStmt (Const . uncurry f) (b ^. blockStmts))  nextBlocks :: Block ext b r a -> [Some (BlockID b)] nextBlocks b =@@ -709,7 +709,7 @@            -- ^ Block to print.         -> Doc ann ppBlock ppLineNumbers ppBlockArgs mPda b = do-  let stmts = ppStmtSeq ppLineNumbers (blockInputCount b) (b^.blockStmts)+  let stmts = ppStmtSeq ppLineNumbers (blockInputCount b) (b ^. blockStmts)   let mPostdom = flip fmap mPda $ \ pda ->         let Const pd = pda ! blockIDIndex (blockID b)         in if Prelude.null pd@@ -781,7 +781,7 @@    = CFG { cfgHandle :: FnHandle init ret          , cfgBlockMap :: !(BlockMap ext blocks ret)          , cfgEntryBlockID :: !(BlockID blocks init)-         , cfgBreakpoints :: !(Bimap BreakpointName (Some (BlockID blocks)))+         , cfgCutpoints :: !(Bimap CutpointName (Some (BlockID blocks)))          }  cfgArgTypes :: CFG ext blocks init ret -> CtxRepr init
src/Lang/Crucible/CFG/EarlyMergeLoops.hs view
@@ -56,7 +56,7 @@  import           Lang.Crucible.CFG.Expr import           Lang.Crucible.CFG.Reg-import           Lang.Crucible.Panic+import           Lang.Crucible.Panic (panic) import           Lang.Crucible.Types  --------------------------@@ -342,7 +342,7 @@    Print {}       -> orig    Assert {}      -> orig    Assume {}      -> orig-   Breakpoint {}  -> orig+   Cut {}         -> orig    where     orig = pure (Seq.fromList [st])@@ -380,7 +380,7 @@     Print {}       -> lowerAtomReads ng pvals atomsToLower st     Assert {}      -> lowerAtomReads ng pvals atomsToLower st     Assume {}      -> lowerAtomReads ng pvals atomsToLower st-    Breakpoint {}  -> lowerAtomReads ng pvals atomsToLower st+    Cut {}         -> lowerAtomReads ng pvals atomsToLower st   where     atomsToLower :: [Some (Atom s)]     atomsToLower = Set.toList (foldStmtInputs addIfLowered (pos_val st) mempty)@@ -758,7 +758,7 @@           | Just Refl <- testEquality (lambdaId ll) (lambdaId l1) -> Output l1 (lambdaAtom l2)         (_, _:rest) -> bidToTerm origOut rest         _ ->-          error "Output blocks mismatched in routePaths"+          panic "routePaths" ["Output blocks mismatched"]        mkMapping = Ctx.generateM sz $ \idx ->       do n <- freshNonce ng
src/Lang/Crucible/CFG/Expr.hs view
@@ -402,6 +402,11 @@     -> !RoundingMode     -> !(f (FloatType fi'))     -> App ext f (FloatType fi)+  FloatRound+    :: !(FloatInfoRepr fi)+    -> !RoundingMode+    -> !(f (FloatType fi))+    -> App ext f (FloatType fi)   FloatFromBinary     :: !(FloatInfoRepr fi)     -> !(f (BVType (FloatInfoToBitWidth fi)))@@ -530,6 +535,11 @@                  -> !(f (SequenceType tp))                  -> App ext f (MaybeType (StructType (EmptyCtx ::> tp ::> SequenceType tp))) +  -- Reverse a sequence+  SequenceReverse :: !(TypeRepr tp)+                  -> !(f (SequenceType tp))+                  -> App ext f (SequenceType tp)+   ----------------------------------------------------------------------   -- Vector @@ -577,7 +587,7 @@   -- Create a closure that captures the last argument.   Closure :: !(CtxRepr args)           -> !(TypeRepr ret)-          -> !(f (FunctionHandleType (args::>tp) ret))+          -> !(f (FunctionHandleType (args ::> tp) ret))           -> !(TypeRepr tp)           -> !(f tp)           -> App ext f (FunctionHandleType args ret)@@ -628,12 +638,12 @@   BVLit :: (1 <= w) => NatRepr w -> BV.BV w -> App ext f (BVType w)    -- concatenate two bitvectors-  BVConcat :: (1 <= u, 1 <= v, 1 <= u+v)+  BVConcat :: (1 <= u, 1 <= v, 1 <= u + v)            => !(NatRepr u)            -> !(NatRepr v)            -> !(f (BVType u))       -- Most significant bits            -> !(f (BVType v))       -- Least significant bits-           -> App ext f (BVType (u+v))+           -> App ext f (BVType (u + v))    -- BVSelect idx n bv chooses bits [idx, .. , idx+n-1] from bitvector bv.   -- The resulting bitvector will have width n.@@ -645,19 +655,19 @@            -> !(f (BVType w))            -> App ext f (BVType len) -  BVTrunc :: (1 <= r, r+1 <= w)+  BVTrunc :: (1 <= r, r + 1 <= w)           => !(NatRepr r)           -> !(NatRepr w)           -> !(f (BVType w))           -> App ext f (BVType r) -  BVZext :: (1 <= w, 1 <= r, w+1 <= r)+  BVZext :: (1 <= w, 1 <= r, w + 1 <= r)          => !(NatRepr r)          -> !(NatRepr w)          -> !(f (BVType w))          -> App ext f (BVType r) -  BVSext :: (1 <= w, 1 <= r, w+1 <= r)+  BVSext :: (1 <= w, 1 <= r, w + 1 <= r)          => !(NatRepr r)          -> !(NatRepr w)          -> !(f (BVType w))@@ -1176,6 +1186,7 @@     FloatFpApart{} -> knownRepr     FloatIte fi _ _ _ -> FloatRepr fi     FloatCast fi _ _ -> FloatRepr fi+    FloatRound fi _ _ -> FloatRepr fi     FloatFromBinary fi _ -> FloatRepr fi     FloatToBinary fi _ -> case floatInfoToBVTypeRepr fi of       BaseBVRepr w -> BVRepr w@@ -1227,6 +1238,7 @@       MaybeRepr (StructRepr (Ctx.Empty Ctx.:> tpr Ctx.:> SequenceRepr tpr))     SequenceLength{} -> knownRepr     SequenceTail tpr _ -> MaybeRepr (SequenceRepr tpr)+    SequenceReverse tpr _ -> SequenceRepr tpr      ----------------------------------------------------------------------     -- SymbolicArrayType
src/Lang/Crucible/CFG/ExtractSubgraph.hs view
@@ -17,19 +17,20 @@   ( extractSubgraph   ) where -import           Control.Lens import qualified Data.Bimap as Bimap import           Data.Parameterized.Context as Ctx import           Data.Parameterized.Map as MapF import           Data.Set as S import qualified Data.Map as Map import           Debug.Trace+import           Lens.Micro ((^.))  import           What4.FunctionName import           What4.ProgramLoc  import           Lang.Crucible.CFG.Core import           Lang.Crucible.FunctionHandle+import           Lang.Crucible.Panic (panic)  -- | Given a CFG @cfg@, a set of blocks @cuts@ that take the return type as their sole -- argument, and a block @bi@ that takes the CFG's init type as its sole argument,@@ -43,7 +44,7 @@                 -> BlockID blocks init                 -> HandleAllocator                 -> IO (Maybe (SomeCFG ext init ret))-extractSubgraph (CFG{cfgBlockMap = orig, cfgBreakpoints = breakpoints}) cuts bi halloc =+extractSubgraph (CFG{cfgBlockMap = orig, cfgCutpoints = cutpoints}) cuts bi halloc =   extractSubgraphFirst orig cuts MapF.empty zeroSize bi $     \(SubgraphIntermediate finalMap finalInitMap _sz entryID cb) -> do         hn <- mkHandle halloc startFunctionName@@ -53,9 +54,9 @@             { cfgBlockMap = bm             , cfgEntryBlockID = entryID             , cfgHandle = hn-            , cfgBreakpoints = Bimap.fromList $ Map.toList $+            , cfgCutpoints = Bimap.fromList $ Map.toList $                 Map.mapMaybe (viewSome $ \bid -> Some <$> MapF.lookup bid finalMap) $-                Bimap.toMap breakpoints+                Bimap.toMap cutpoints             }  -- | Type for carrying intermediate results through subraph extraction@@ -95,7 +96,7 @@             visitChildNode orig cuts bi1 sgi1               $ \sgi2 -> visitChildNode orig cuts bi2 sgi2 f           Return _ -> f-          _ -> error "extractSubgraph': unexpected case!")+          _ -> panic "extractSubgraph'" ["unexpected case!"])                 (SubgraphIntermediate                   (MapF.insert bi (BlockID $ nextIndex sz) (MapF.map extendBlockID mapF))                   (MapF.map extendBlockID initMap)@@ -126,7 +127,7 @@             visitChildNode orig cuts bi1 sgi1               $ \sgi2 -> visitChildNode orig cuts bi2 sgi2 f           Return _ -> f-          _ -> error "extractSubgraphFirst: unexpected case!")+          _ -> panic "extractSubgraphFirst" ["unexpected case!"])                 (SubgraphIntermediate                   (if case S.minView cuts of                       Just (bi', _) -> case testEquality (blockInputs block) (blockInputs $ orig Ctx.! blockIDIndex bi') of@@ -194,7 +195,7 @@ cloneBlock :: MapF (BlockID old) (BlockID new)            -> BlockID new ctx -> Block ext old ret ctx -> Maybe (Block ext new ret ctx) cloneBlock mapF newID b = do-  stmts' <- cloneStmtSeq mapF (b^.blockStmts)+  stmts' <- cloneStmtSeq mapF (b ^. blockStmts)   return Block{ blockID       = newID               , blockInputs   = blockInputs b               , _blockStmts   = stmts'@@ -215,7 +216,7 @@   jt2' <- cloneJumpTarget mapF jt2   return $ Br reg jt1' jt2' cloneTerm _mapF (Return reg) = Just $ Return reg-cloneTerm _ _ = error "cloneTerm: unexpected case!"+cloneTerm _ _ = panic "cloneTerm" ["unexpected case!"]  cloneJumpTarget :: MapF (BlockID blocks1) (BlockID blocks2)                 -> JumpTarget blocks1 t
src/Lang/Crucible/CFG/Generator.hs view
@@ -60,7 +60,7 @@   , assertExpr   , assumeExpr   , addPrintStmt-  , addBreakpointStmt+  , addCutStmt   , extensionStmt   , mkAtom   , mkFresh@@ -109,7 +109,6 @@   , module Lang.Crucible.CFG.EarlyMergeLoops   ) where -import           Control.Lens hiding (Index) import           Control.Monad ((>=>)) import qualified Control.Monad.Fail as F import           Control.Monad.IO.Class (MonadIO(..))@@ -117,6 +116,7 @@ import           Control.Monad.Trans.Class (MonadTrans(..)) import           Control.Monad.Catch import qualified Data.Foldable as Fold+import           Data.Function ((&)) import           Data.Kind import           Data.Parameterized.Context as Ctx import           Data.Parameterized.Nonce@@ -127,6 +127,8 @@ import qualified Data.Set as Set import           Data.Text (Text) import           Data.Void+import           Lens.Micro ((^.), (.~), (%~), Lens', Lens, SimpleGetter, lens, to)+import           Lens.Micro.Mtl (use, (.=), (%=))  import           What4.ProgramLoc import           What4.Symbol@@ -162,7 +164,7 @@       }  -- | Statements translated so far in this block.-cbsStmts :: Simple Lens (CurrentBlockState ext s) (StmtSeq ext s)+cbsStmts :: Lens' (CurrentBlockState ext s) (StmtSeq ext s) cbsStmts = lens _cbsStmts (\s v -> s { _cbsStmts = v })  ------------------------------------------------------------------------@@ -186,14 +188,14 @@   IxGeneratorState ext s t ret m ()  -- | Label for entry block.-gsEntryLabel :: Getter (IxGeneratorState ext s t ret m i) (Label s)+gsEntryLabel :: SimpleGetter (IxGeneratorState ext s t ret m i) (Label s) gsEntryLabel = to _gsEntryLabel  -- | List of previously processed blocks.-gsBlocks :: Simple Lens (IxGeneratorState ext s t ret m i) (Seq (Block ext s ret))+gsBlocks :: Lens' (IxGeneratorState ext s t ret m i) (Seq (Block ext s ret)) gsBlocks = lens _gsBlocks (\s v -> s { _gsBlocks = v }) -gsNonceGen :: Getter (IxGeneratorState ext s t ret m i) (NonceGenerator m s)+gsNonceGen :: SimpleGetter (IxGeneratorState ext s t ret m i) (NonceGenerator m s) gsNonceGen = to _gsNonceGen  -- | Information about current block.@@ -201,15 +203,15 @@ gsCurrent = lens _gsCurrent (\s v -> s { _gsCurrent = v })  -- | Current source position.-gsPosition :: Simple Lens (IxGeneratorState ext s t ret m i) Position+gsPosition :: Lens' (IxGeneratorState ext s t ret m i) Position gsPosition = lens _gsPosition (\s v -> s { _gsPosition = v })  -- | User state for current block. This gets reset between blocks.-gsState :: Simple Lens (IxGeneratorState ext s t ret m i) (t s)+gsState :: Lens' (IxGeneratorState ext s t ret m i) (t s) gsState = lens _gsState (\s v -> s { _gsState = v })  -- | List of functions seen by current generator.-seenFunctions :: Simple Lens (IxGeneratorState ext s t ret m i) [AnyCFG ext]+seenFunctions :: Lens' (IxGeneratorState ext s t ret m i) [AnyCFG ext] seenFunctions = lens _seenFunctions (\s v -> s { _seenFunctions = v })  ------------------------------------------------------------------------@@ -229,10 +231,10 @@   GeneratorState ext s t ret m ->   EndState ext s t ret m terminateBlock term gs =-  do let p = gs^.gsPosition-     let cbs = gs^.gsCurrent+  do let p = gs ^. gsPosition+     let cbs = gs ^. gsCurrent      -- Define block-     let b = mkBlock (cbsBlockID cbs) (cbsInputValues cbs) (cbs^.cbsStmts) (Posd p term)+     let b = mkBlock (cbsBlockID cbs) (cbsInputValues cbs) (cbs ^. cbsStmts) (Posd p term)      -- Store block      let gs' = gs & gsCurrent .~ ()                   & gsBlocks  %~ (Seq.|> b)@@ -455,13 +457,13 @@   do e_a <- mkAtom e      addStmt (Print e_a) --- | Add a breakpoint.-addBreakpointStmt ::+-- | Add a cutpoint.+addCutStmt ::   (Monad m, IsSyntaxExtension ext) =>-  Text {- ^ breakpoint name -} ->-  Assignment (Value s) args {- ^ breakpoint values -} ->+  Text {- ^ cutpoint name -} ->+  Assignment (Value s) args {- ^ cutpoint values -} ->   Generator ext s t r m ()-addBreakpointStmt nm args = addStmt $ Breakpoint (BreakpointName nm) args+addCutStmt nm args = addStmt $ Cut (CutpointName nm) args  -- | Add an assert statement. assertExpr ::@@ -565,8 +567,8 @@   do let gs1 = startBlock l (gs0 & gsCurrent .~ ())      gs2 <- runGenerator next gs1      -- Reset current block and state.-     let gs3 = gs2 & gsPosition .~ gs0^.gsPosition-                   & gsCurrent .~ gs0^.gsCurrent+     let gs3 = gs2 & gsPosition .~ gs0 ^. gsPosition+                   & gsCurrent .~ gs0 ^. gsCurrent      cont () gs3  -- | Define a block with an ordinary label.@@ -891,8 +893,8 @@                  -> CFG ext s init ret cfgFromGenerator h s =   CFG { cfgHandle = h-      , cfgEntryLabel = s^.gsEntryLabel-      , cfgBlocks = Fold.toList (s^.gsBlocks)+      , cfgEntryLabel = s ^. gsEntryLabel+      , cfgBlocks = Fold.toList (s ^. gsBlocks)       }  -- | Given the arguments, this returns the initial state, and an action for@@ -953,4 +955,4 @@               }   ts' <- runGenerator (action >>= returnFromFunction) $! ts   g   <- optPass ng (cfgFromGenerator h ts')-  return (SomeCFG g, ts'^.seenFunctions)+  return (SomeCFG g, ts' ^. seenFunctions)
src/Lang/Crucible/CFG/Reg.hs view
@@ -586,7 +586,7 @@    | Assert !(Atom s BoolType) !(Atom s (StringType Unicode))      -- | Assume the given expression.    | Assume !(Atom s BoolType) !(Atom s (StringType Unicode))-   | forall args . Breakpoint BreakpointName !(Assignment (Value s) args)+   | forall args . Cut CutpointName !(Assignment (Value s) args)  instance PrettyExt ext => Show (Stmt ext s) where   show = show . pretty@@ -602,7 +602,7 @@       Print  v   -> "print"  <+> pretty v       Assert c m -> "assert" <+> pretty c <+> pretty m       Assume c m -> "assume" <+> pretty c <+> pretty m-      Breakpoint nm args -> "breakpoint" <+> pretty nm <+> parens (commas (toListFC pretty args))+      Cut nm args -> "cut" <+> pretty nm <+> parens (commas (toListFC pretty args))  -- | Return local value assigned by this statement or @Nothing@ if this -- does not modify a register.@@ -617,7 +617,7 @@     Print{} -> Nothing     Assert{} -> Nothing     Assume{} -> Nothing-    Breakpoint{} -> Nothing+    Cut{} -> Nothing  -- | Fold all registers that are inputs tostmt. foldStmtInputs :: TraverseExt ext => (forall x . Value s x -> b -> b) -> Stmt ext s -> b -> b@@ -631,7 +631,7 @@     Print  e     -> f (AtomValue e) b     Assert c m   -> f (AtomValue c) (f (AtomValue m) b)     Assume c m   -> f (AtomValue c) (f (AtomValue m) b)-    Breakpoint _ args -> foldrFC' f b args+    Cut _ args   -> foldrFC' f b args  substStmt :: ( Applicative m, TraverseExt ext )           => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))@@ -647,7 +647,7 @@     Print e -> Print <$> substAtom f e     Assert c m -> Assert <$> substAtom f c <*> substAtom f m     Assume c m -> Assume <$> substAtom f c <*> substAtom f m-    Breakpoint nm args -> Breakpoint nm <$> traverseFC (substValue f) args+    Cut nm args -> Cut nm <$> traverseFC (substValue f) args  mapStmtAtom :: ( Applicative m, TraverseExt ext )           => (forall (x :: CrucibleType). Atom s x -> m (Atom s x))@@ -663,7 +663,7 @@     Print e -> Print <$> f e     Assert c m -> Assert <$> f c <*> f m     Assume c m -> Assume <$> f c <*> f m-    Breakpoint nm args -> Breakpoint nm <$> traverseFC (substValueAtom f) args+    Cut nm args -> Cut nm <$> traverseFC (substValueAtom f) args  substPosdStmt :: ( Applicative m, TraverseExt ext )               => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))@@ -922,7 +922,7 @@ cfgEntryBlock :: CFG ext s init ret -> Block ext s ret cfgEntryBlock g =   fromMaybe-    (error "Missing entry block")+    (panic "cfgEntryBlock" ["Missing entry block"])     (Fold.find (\b -> blockID b == LabelID (cfgEntryLabel g)) (cfgBlocks g))  cfgInputTypes :: CFG ext s init ret -> CtxRepr init
src/Lang/Crucible/CFG/SSAConversion.hs view
@@ -30,11 +30,11 @@   ) where  import           Control.Exception (assert)-import           Control.Lens ((&)) import           Control.Monad.State.Strict import           Data.Bimap (Bimap) import qualified Data.Bimap as Bimap import qualified Data.Foldable as Fold+import           Data.Function ((&)) import           Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import           Data.Maybe (isJust, fromMaybe)@@ -129,11 +129,11 @@            , binputTerm       :: !(Posd (ExtendedTermStmt s blocks ret))            } --- The Breakpoint non-terminator statement becomes a jump during SSA conversion.--- This datatype temporarily adds breakpoint as a terminator statement.+-- The Cut non-terminator statement becomes a jump during SSA conversion.+-- This datatype temporarily adds cut as a terminator statement. data ExtendedTermStmt s blocks ret where   BaseTermStmt :: TermStmt s ret -> ExtendedTermStmt s blocks ret-  BreakStmt :: JumpInfo s blocks -> ExtendedTermStmt s blocks ret+  CutStmt :: JumpInfo s blocks -> ExtendedTermStmt s blocks ret  type BlockInputAssignment ext s blocks ret    = Assignment (BlockInput ext s blocks ret)@@ -144,21 +144,21 @@ extBlockInput ::   BlockInput ext s blocks ret args ->   BlockInput ext s (blocks ::> tp) ret arg-extBreakpoints ::-  Bimap BreakpointName (Some (C.BlockID blocks)) ->-  Bimap BreakpointName (Some (C.BlockID (blocks ::> tp)))+extCutpoints ::+  Bimap CutpointName (Some (C.BlockID blocks)) ->+  Bimap CutpointName (Some (C.BlockID (blocks ::> tp))) #ifdef UNSAFE_OPS extBlockInputAssignment = unsafeCoerce  extBlockInput = unsafeCoerce -extBreakpoints = unsafeCoerce+extCutpoints = unsafeCoerce #else extBlockInputAssignment = fmapFC extBlockInput  extBlockInput bi = bi { binputID = C.extendBlockID (binputID bi) } -extBreakpoints = Bimap.mapR (mapSome C.extendBlockID)+extCutpoints = Bimap.mapR (mapSome C.extendBlockID) #endif  ------------------------------------------------------------------------@@ -280,7 +280,7 @@       Just (SomeSwitchInfo tr si) -> Just $          case testEquality tr (typeOfAtom (lambdaAtom l)) of              Just Refl -> si-             Nothing   -> error "Lang.Crucible.SSAConversion.lookupSwitchInfo: type mismatch!"+             Nothing   -> panic "lookupSwitchInfo" ["type mismatch!"]  -- | Extend switch target extSwitchInfo :: SwitchInfo s blocks tp -> SwitchInfo s (blocks::>args) tp@@ -295,11 +295,11 @@   let blocks' = extBlockInputAssignment $ biBlocks bi   let jump_info' = extJumpInfoMap $ biJumpInfo bi   let switch_info' = extSwitchInfoMap $ biSwitchInfo bi-  let breakpoints' = extBreakpoints $ biBreakpoints bi+  let cutpoints' = extCutpoints $ biCutpoints bi   BI { biBlocks = extend blocks' binput      , biJumpInfo = jump_info'      , biSwitchInfo = switch_info'-     , biBreakpoints = breakpoints'+     , biCutpoints = cutpoints'      }  ------------------------------------------------------------------------@@ -393,7 +393,7 @@    = BI { biBlocks      :: !(Assignment (BlockInput ext s blocks ret) blocks)         , biJumpInfo    :: !(JumpInfoMap s blocks)         , biSwitchInfo  :: !(SwitchInfoMap s blocks)-        , biBreakpoints :: !(Bimap BreakpointName (Some (C.BlockID blocks)))+        , biCutpoints :: !(Bimap CutpointName (Some (C.BlockID blocks)))         }  -- | This infers the information given a set of blocks.@@ -403,7 +403,7 @@         bi0 = BI { biBlocks = empty                  , biJumpInfo = emptyJumpInfoMap                  , biSwitchInfo = emptySwitchInfoMap-                 , biBreakpoints = Bimap.empty+                 , biCutpoints = Bimap.empty                  }         resolveBlocks ::           BlockInfo ext s ret blocks ->@@ -432,7 +432,7 @@                   let bi' = extBlockInfo bi binput                   let ji = JumpInfo block_id crepr ra                   let bi'' = bi' { biJumpInfo = insertJumpInfo l ji (biJumpInfo bi') }-                  splitLastBlockInputOnBreakpoints bi'' rest+                  splitLastBlockInputOnCutpoints bi'' rest                 LambdaID l -> do                   let block_id = C.BlockID (nextIndex sz)                   let lastArg = AtomValue (lambdaAtom l)@@ -445,16 +445,16 @@                   let bi' = extBlockInfo bi binput                   let si = SwitchInfo block_id crepr ra                   let bi'' = bi' { biSwitchInfo = insertSwitchInfo l si (biSwitchInfo bi') }-                  splitLastBlockInputOnBreakpoints bi'' rest-        splitLastBlockInputOnBreakpoints ::+                  splitLastBlockInputOnCutpoints bi'' rest+        splitLastBlockInputOnCutpoints ::           BlockInfo ext s ret blocks ->           [Block ext s ret] ->           Some (BlockInfo ext s ret)-        splitLastBlockInputOnBreakpoints bi rest+        splitLastBlockInputOnCutpoints bi rest           | first_binputs :> last_binput <- biBlocks bi-          , (first_stmts, break_stmt Seq.:<| last_stmts) <--              Seq.breakl isBreakpoint (binputStmts last_binput)-          , Breakpoint nm args <- pos_val break_stmt = do+          , (first_stmts, cut_stmt Seq.:<| last_stmts) <-+              Seq.breakl isCut (binputStmts last_binput)+          , Cut nm args <- pos_val cut_stmt = do             let block_id = C.BlockID $ nextIndex $ size $ biBlocks bi              let first_binputs' = extBlockInputAssignment $ first_binputs@@ -462,7 +462,7 @@             let jump_info = JumpInfo block_id (fmapFC typeOfValue args) args             let last_binput' = (extBlockInput last_binput)                   { binputStmts = first_stmts-                  , binputTerm = break_stmt { pos_val = BreakStmt jump_info }+                  , binputTerm = cut_stmt { pos_val = CutStmt jump_info }                   }              let new_binput = (extBlockInput last_binput)@@ -471,23 +471,23 @@                   , binputStmts = last_stmts                   } -            let new_breakpoints = do-                  let try_new_breakpoints = Bimap.tryInsert nm (Some block_id) $-                        extBreakpoints $ biBreakpoints bi-                  if Bimap.pairMember (nm, (Some block_id)) try_new_breakpoints-                    then try_new_breakpoints-                    else error $ "Duplicate breakpoint: " ++ show nm+            let new_cutpoints = do+                  let try_new_cutpoints = Bimap.tryInsert nm (Some block_id) $+                        extCutpoints $ biCutpoints bi+                  if Bimap.pairMember (nm, (Some block_id)) try_new_cutpoints+                    then try_new_cutpoints+                    else error $ "Duplicate cutpoint: " ++ show nm             let bi' = BI                   { biBlocks = first_binputs' :> last_binput' :> new_binput                   , biJumpInfo = extJumpInfoMap $ biJumpInfo bi                   , biSwitchInfo = extSwitchInfoMap $ biSwitchInfo bi-                  , biBreakpoints = new_breakpoints+                  , biCutpoints = new_cutpoints                   }-            splitLastBlockInputOnBreakpoints bi' rest-        splitLastBlockInputOnBreakpoints bi rest = resolveBlocks bi rest-        isBreakpoint :: Posd (Stmt ext s) -> Bool-        isBreakpoint = \case-          Posd _ Breakpoint{} -> True+            splitLastBlockInputOnCutpoints bi' rest+        splitLastBlockInputOnCutpoints bi rest = resolveBlocks bi rest+        isCut :: Posd (Stmt ext s) -> Bool+        isCut = \case+          Posd _ Cut{} -> True           _ -> False  @@ -621,7 +621,7 @@                   -> C.JumpTarget blocks ctx resolveJumpTarget bi reg_map next_lbl = do   case lookupJumpInfo next_lbl (biJumpInfo bi) of-    Nothing -> error "Could not find label in resolveJumpTarget"+    Nothing -> panic "resolveJumpTarget" ["Could not find label"]     Just (JumpInfo next_id types inputs) -> do       let args = fmapFC (resolveReg reg_map) inputs       C.JumpTarget next_id types args@@ -634,7 +634,7 @@                     -> C.JumpTarget blocks ctx resolveLambdaAsJump bi reg_map next_lbl output =   case lookupSwitchInfo next_lbl (biSwitchInfo bi) of-    Nothing -> error "Could not find label in resolveLambdaAsJump"+    Nothing -> panic "resolveLambdaAsJump" ["Could not find label"]     Just (SwitchInfo block_id types inputs) -> do       let types' = types :> typeOfAtom (lambdaAtom next_lbl)       let args = fmapFC (resolveReg reg_map) inputs@@ -648,7 +648,7 @@                       -> C.SwitchTarget blocks ctx tp resolveLambdaAsSwitch bi reg_map next_lbl =   case lookupSwitchInfo next_lbl (biSwitchInfo bi) of-    Nothing -> error "Could not find label in resolveLambdaAsSwitch"+    Nothing -> panic "resolveLambdaAsSwitch" ["Could not find label"]     Just (SwitchInfo block_id types inputs) -> do       let args = fmapFC (resolveReg reg_map) inputs       C.SwitchTarget block_id types args@@ -695,7 +695,7 @@     ErrorStmt e -> C.ErrorStmt (resolveAtom reg_map e)      Output l e -> C.Jump (resolveLambdaAsJump bi reg_map l (resolveAtom reg_map e))-resolveTermStmt _ reg_map _ (BreakStmt (JumpInfo next_id types inputs)) = do+resolveTermStmt _ reg_map _ (CutStmt (JumpInfo next_id types inputs)) = do   let args = fmapFC (resolveReg reg_map) inputs   C.Jump $ C.JumpTarget next_id types args @@ -746,7 +746,7 @@      Nothing -> Nothing      Just (SomeReg tp r)         | Just Refl <- testEquality tp (C.appType app) -> Just r-     _ -> error "appRegMap_lookup: impossible!"+     _ -> panic "appRegMap_lookup" ["impossible!"]   appRegMap_empty :: AppRegMap ext ctx@@ -915,14 +915,14 @@                            (resolveAtom reg_map m))                  (resolveStmts nm bi sz reg_map bindings appMap rest t) -    -- breakpoint statements are eliminated during the inferBlockInfo phase-    Breakpoint{} -> error $-      "Unexpected breakpoint at position " ++ show p ++ ": " ++ show (Pretty.pretty s0)+    -- cut statements are eliminated during the inferBlockInfo phase+    Cut{} -> error $+      "Unexpected cut at position " ++ show p ++ ": " ++ show (Pretty.pretty s0)  data SomeBlockMap ext ret where   SomeBlockMap ::     Ctx.Index blocks tp ->-    Bimap BreakpointName (Some (C.BlockID blocks)) ->+    Bimap CutpointName (Some (C.BlockID blocks)) ->     C.BlockMap ext blocks ret ->     SomeBlockMap ext ret @@ -950,9 +950,9 @@   case inferBlockInfo blocks of     Some bi ->       case lookupJumpInfo entry (biJumpInfo bi) of-        Nothing -> error "Missing initial block."+        Nothing -> panic "resolveBlockMap" ["Missing initial block."]         Just (JumpInfo (C.BlockID idx) _ _) ->-          SomeBlockMap idx (biBreakpoints bi) $+          SomeBlockMap idx (biCutpoints bi) $             fmapFC (resolveBlock bi) (biBlocks bi)  ------------------------------------------------------------------------@@ -970,7 +970,7 @@   let entry = cfgEntryLabel g   let blocks = cfgBlocks g   case resolveBlockMap (handleName h) entry blocks of-    SomeBlockMap idx breakpoints block_map -> do+    SomeBlockMap idx cutpoints block_map -> do           let b = block_map ! idx           case C.blockInputs b `testEquality` initTypes of             Nothing -> error $@@ -981,6 +981,6 @@               let g' = C.CFG { C.cfgHandle = h                              , C.cfgBlockMap = block_map                              , C.cfgEntryBlockID = C.BlockID idx-                             , C.cfgBreakpoints = breakpoints+                             , C.cfgCutpoints = cutpoints                              }               reachableCFG g'
src/Lang/Crucible/Concretize.hs view
@@ -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,210 @@     -- 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+          -- not (modelA_1 == modelB_1) \/ ... \/ not (modelA_n == modelB_n)+          p <-+            foldlMFC+              (\p (Const p') -> W4I.orPred sym p p')+              (W4I.falsePred 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
src/Lang/Crucible/FunctionHandle.hs view
@@ -195,7 +195,7 @@ -- FnHandleMap  data HandleElt (f :: Ctx CrucibleType -> CrucibleType -> Type) ctx where-  HandleElt :: FnHandle args ret -> f args ret -> HandleElt f (args::>ret)+  HandleElt :: FnHandle args ret -> f args ret -> HandleElt f (args ::> ret)  newtype FnHandleMap f = FnHandleMap (MapF (Nonce GlobalNonceGenerator) (HandleElt f))
+ src/Lang/Crucible/README.hs view
@@ -0,0 +1,114 @@+{- | This module is only for documentation purposes, and provides a high+level overview of Crucible aimed at developers. -}+{-# OPTIONS_GHC -Wno-unused-imports #-}+{-# OPTIONS_GHC -Wno-missing-export-lists #-}+module Lang.Crucible.README where++import What4.Interface+import What4.Expr.App+import What4.BaseTypes+import Lang.Crucible.Backend++import Lang.Crucible.Types+import Lang.Crucible.CFG.Expr+import Lang.Crucible.CFG.Core hiding (Expr)+import Lang.Crucible.CFG.SSAConversion++import Lang.Crucible.Simulator.RegValue+import Lang.Crucible.Simulator.RegMap+import Lang.Crucible.Simulator.ExecutionTree+import Lang.Crucible.Simulator.EvalStmt+import Lang.Crucible.Simulator.Evaluation+import Lang.Crucible.Simulator.Intrinsics++++-- * Crucible Types++{- $+The types of the Crucible language are defined in "Lang.Crucible.Types".+Types are encoded using [singletons](https://github.com/Galoisinc/parameterized-utils?tab=readme-ov-file#parameterized-types-motivation):++* 'CrucibleType' is the Haskell type-level description of all Crucible types+* 'TypeRepr' are the associated value-level singletons, which+  are used when we pass around types, or store them in data structures.+-}++-- * Crucible Values++{- $+The inhabitants of each type are specified via the type function 'RegValue'.+We also have 'RegValue'' which is just a @newtype@ wrapper around 'RegValue',+because in Haskell type families may not be partially applied but @newtype@s can.++An important subset of the Crucible types are the base types (see 'BaseToType'),+which is for the symbolic expression we can construct+(see 'SymExpr' in [what4](https://github.com/Galoisinc/what4)).+Only these types may contain variables. In practice, we always use @what4@'s+'Expr' type to represent symbolic expressions.++Also, in some cases we use 'RegEntry' which+is just a pair of a 'RegValue' and its associated 'TypeRepr'.++There's also 'BaseTerm', which is similar to 'RegEntry' but+for base types---it contains a @what4@'s 'BaseTypeRepr' and a value of the corresponding+base type (usually;  the type is parameterized on exactly what we package+with the type).+-}+  +-- * Crucible Programs+  +{- $+The program executed by the simulator is in the form of a control flow+graph (CFG).  A typical way to construct them is as follows:++  1. use the functions in "Lang.Crucible.CFG.Generator" to produce a CFG with +     assignments ("Lang.Crucible.CFG.Reg")+  2. use 'toSSA' to translate this to a CFG without assignments+     ("Lang.Crucible.CFG.Core")++The core 'CFG' contains basic blocks with 'Stmt's and terminated+by 'TermStmt'.  The expression language for the core 'Core.CFG' is+the type 'App'.+-}+  +-- * Symbolic Simulator+  +{- $+The state of a running simulator is described in "Lang.Crucible.Simulator.ExecutionTree":++  * 'ExecState' is the current state of execution.+     We start with 'InitialState', and keep performing steps until we get+     to a 'ResultState'.+  * As the simulator executes, it keeps track of its state in 'SimState',+    which is stored in the current `ExecState`.+  * 'SimContext' is the part of the state that persists across branches+    (e.g, after we explore the @then@ part of an @if@ statement, we'll+    roll back some of the state changes before simulating the @else@ part,+    but the data in 'SimContext's persists).  An important part of the+    'SimContext' is the simulator's backend ('_ctxBackend'), which is how the+    simulator communicates with a solver, and builds symbolic expressions+    ('IsSymBackend').+++To evaluate a 'CFG' we evaluate the statements as described in+"Lang.Crucible.Simulator.EvalStmt" (details in 'stepStmt', 'stepTerm').+Details about expressions evaluation are in 'evalApp' in "Lang.Crucible.Simulator.Evaluation".++A lot of useful functionality relevant to the simulator can be accessed+from module "Lang.Crucible.Simulator".++The simulator supports mutable global variables.  Our tools use one such+global to store a language specific memory model, which records information+about various memory operations.+-}++-- * Intrinsics++{- $++Crucible type may be extended using 'IntrinsicType's.  An intrinsic type is+a type-level string, which can be given meaning by making an instance of+'IntrinsicClass'.+-}+
src/Lang/Crucible/Simulator.hs view
@@ -87,11 +87,14 @@     -- ** SimContext record   , IsSymInterfaceProof   , SimContext(..)+  , ExceptionContextConfig(..)   , initSimContext   , ctxSymInterface   , functionBindings   , cruciblePersonality   , profilingMetrics+  , exceptionContextConfig+  , parseExceptionContextConfig      -- * SimState   , SimState
src/Lang/Crucible/Simulator/BoundedExec.hs view
@@ -30,8 +30,8 @@   ( boundedExecFeature   ) where -import           Control.Lens ( (^.), to, (&), (%~), (.~) ) import           Control.Monad ( when )+import           Data.Function ((&)) import           Data.IORef import           Data.Map (Map) import qualified Data.Map as Map@@ -40,7 +40,7 @@ import qualified Data.Sequence as Seq import qualified Data.Text as Text import           Data.Word-+import           Lens.Micro ((^.), to, (%~), (.~))  import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.Map as MapF@@ -82,13 +82,13 @@ buildWTOMap = snd . go 0 0 Map.empty  where  go :: Int -> Int -> Map Int (Int,Int) -> [WTOComponent (Some (BlockID blocks))] -> (Int, Map Int (Int,Int))- go !x !_ m [] = (x,m)- go !x !d m (Vertex (Some bid) : cs) =+ go !x !_ !m [] = (x,m)+ go x d m (Vertex (Some bid) : cs) =     let m' = Map.insert (Ctx.indexVal (blockIDIndex bid)) (x,d) m-     in go (x+1) d m' cs- go !x !d m (SCC scc : cs) =-    let m'  = viewSome (\hd -> Map.insert (Ctx.indexVal (blockIDIndex hd)) (x,d+1) m) (wtoHead scc)-        (x',m'') = go (x+1) (d+1) m' $ wtoComps scc+     in go (x + 1) d m' cs+ go x d m (SCC scc : cs) =+    let m'  = viewSome (\hd -> Map.insert (Ctx.indexVal (blockIDIndex hd)) (x,d + 1) m) (wtoHead scc)+        (x',m'') = go (x + 1) (d + 1) m' $ wtoComps scc      in go x' d m'' cs  @@ -100,8 +100,8 @@ incrementBoundCount cs depth =   case Seq.lookup depth cs of      Just n ->-       do let n' = n+1-          let cs' = Seq.update depth n' $ Seq.take (depth+1) cs+       do let n' = n + 1+          let cs' = Seq.update depth n' $ Seq.take (depth + 1) cs           n' `seq` cs' `seq` (cs', n')      Nothing ->        do let cs' = cs <> Seq.replicate (depth - Seq.length cs) 0 <> Seq.singleton 1@@ -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,78 +202,86 @@                        }   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) ->    IO (ExecutionFeatureResult p sym ext rtp)  onTransition gvRef tgt_id res st = stateSolverProof st $-  do let sym = st^.stateSymInterface-     let simCtx = st^.stateContext-     (globals', overLimit) <- checkBackedge gvRef (st^.stateCrucibleFrame.frameBlockID) tgt_id (st^.stateGlobals)+  do let sym = st ^. stateSymInterface+     (globals', overLimit) <- checkBackedge gvRef (st ^. stateCrucibleFrame.frameBlockID) tgt_id (st ^. stateGlobals)      let st' = st & stateGlobals .~ globals'      case overLimit of        Just n ->          do let msg = "reached maximum number of loop iterations (" ++ show n ++ ")"-            let loc = st^.stateCrucibleFrame.to frameProgramLoc+            let loc = st ^. stateCrucibleFrame.to frameProgramLoc             let err = SimError loc (ResourceExhausted msg)-            when generateSideConditions $ withBackend simCtx $ \bak ->+            when generateSideConditions $ withStateBackend st $ \bak ->               addProofObligation bak (LabeledPred (falsePred sym) err)             return (ExecutionFeatureNewState (AbortState (AssertionFailure err) st'))        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))
src/Lang/Crucible/Simulator/BoundedRecursion.hs view
@@ -32,13 +32,14 @@   ( boundedRecursionFeature   ) where -import           Control.Lens ( (^.), (&), (%~) ) import           Control.Monad (when)+import           Data.Function ((&)) import           Data.IORef+import qualified Data.Map.Strict as Map import           Data.Maybe import qualified Data.Text as Text import           Data.Word-import qualified Data.Map.Strict as Map+import           Lens.Micro ((^.), (%~))  import           Data.Parameterized.Ctx import qualified Data.Parameterized.Map as MapF@@ -81,56 +82,60 @@   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) ->    SimState p sym ext rtp f args ->    IO (ExecutionFeatureResult p sym ext rtp)  pushFrame gvRef rebuildStack h mkSt st = stateSolverProof st $-     do let sym = st^.stateSymInterface-        let simCtx = st^.stateContext-        gv <- readIORef gvRef+     do let sym = st ^. stateSymInterface+        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 $ withStateBackend st $ \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
− src/Lang/Crucible/Simulator/Breakpoint.hs 
@@ -1,109 +0,0 @@--------------------------------------------------------------------------- |--- Module           : Lang.Crucible.Simulator.Breakpoint--- Description      : Support for symbolic execution breakpoints--- Copyright        : (c) Galois, Inc 2019--- License          : BSD3--- Maintainer       : Andrei Stefanescu <andrei@galois.com>--- Stability        : provisional------ This module provides execution features for changing the state on--- breakpoints.-------------------------------------------------------------------------{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE RecordWildCards #-}-module Lang.Crucible.Simulator.Breakpoint-  ( breakAndReturn-  ) where--import           Control.Lens-import           Control.Monad.Reader-import qualified Data.Bimap as Bimap-import           Data.HashMap.Strict (HashMap)-import qualified Data.HashMap.Strict as HashMap--import           Data.Parameterized.Classes-import qualified Data.Parameterized.Context as Ctx-import           Data.Parameterized.Some-import           Data.Parameterized.TraversableFC--import qualified Lang.Crucible.Backend as C-import qualified Lang.Crucible.CFG.Core as C-import qualified Lang.Crucible.CFG.Expr as C-import qualified Lang.Crucible.Simulator.CallFrame as C-import qualified Lang.Crucible.Simulator.EvalStmt as C-import qualified Lang.Crucible.Simulator.ExecutionTree as C-import qualified Lang.Crucible.Simulator.Operations as C-import qualified Lang.Crucible.Simulator.OverrideSim as C-import qualified Lang.Crucible.Simulator.RegValue as C-import qualified What4.FunctionName as W---- | This execution feature registers an override for a breakpoint.---   The override summarizes the execution from the breakpoint---   to the return from the function (similar to a tail call).---   This feature requires a map from each function handle---   to the list of breakpoints in the respective function with this---   execution feature.-breakAndReturn ::-  (C.IsSymInterface sym, C.IsSyntaxExtension ext) =>-  C.CFG ext blocks init ret ->-  C.BreakpointName ->-  Ctx.Assignment C.TypeRepr args ->-  C.TypeRepr ret ->-  C.OverrideSim p sym ext rtp args ret (C.RegValue sym ret) ->-  HashMap C.SomeHandle [C.BreakpointName] ->-  IO (C.ExecutionFeature p sym ext rtp)-breakAndReturn C.CFG{..} breakpoint_name arg_types ret_type override all_breakpoints =-  case Bimap.lookup breakpoint_name cfgBreakpoints of-    Just (Some breakpoint_block_id)-      | breakpoint_block <- C.getBlock breakpoint_block_id cfgBlockMap-      , Just Refl <- testEquality (C.blockInputs breakpoint_block) arg_types ->-        return $ C.ExecutionFeature $ \case-          C.RunningState (C.RunPostBranchMerge block_id) state-            | frame <- state ^. C.stateCrucibleFrame-            , C.SomeHandle cfgHandle == C.frameHandle frame-            , Just Refl <- testEquality-                (fmapFC C.blockInputs cfgBlockMap)-                (fmapFC C.blockInputs $ C.frameBlockMap frame)-            , Just Refl <- testEquality breakpoint_block_id block_id-            , Just Refl <- testEquality ret_type (C.frameReturnType frame) -> do-              let override_frame = C.OF $ C.OverrideFrame-                    { _override = W.functionNameFromText $-                        C.breakpointNameText breakpoint_name-                    , _overrideHandle = C.frameHandle frame-                    , _overrideRegMap = state ^.-                        C.stateCrucibleFrame . C.frameRegs-                    }-              result_state <- runReaderT (C.runOverrideSim ret_type override) $-                state & C.stateTree %~-                  C.pushCallFrame C.TailReturnToCrucible override_frame-              return $ C.ExecutionFeatureNewState result_state-          C.CallState return_handler (C.CrucibleCall block_id frame) state-            | Just breakpoints <- HashMap.lookup-                (C.frameHandle frame)-                all_breakpoints -> do-              let result_frame = C.setFrameBreakpointPostdomInfo-                    breakpoints-                    frame-              result_state <- runReaderT-                (C.performFunctionCall-                  return_handler-                  (C.CrucibleCall block_id result_frame))-                state-              return $ C.ExecutionFeatureNewState result_state-          C.TailCallState value_from_value (C.CrucibleCall block_id frame) state-            | Just breakpoints <- HashMap.lookup-                (C.frameHandle frame)-                all_breakpoints -> do-              let result_frame = C.setFrameBreakpointPostdomInfo-                    breakpoints-                    frame-              result_state <- runReaderT-                (C.performTailCall-                  value_from_value-                  (C.CrucibleCall block_id result_frame))-                state-              return $ C.ExecutionFeatureNewState result_state-          _ -> return C.ExecutionFeatureNoChange-    _ -> fail $ "unexpected breakpoint: " ++ show breakpoint_name
src/Lang/Crucible/Simulator/CallFrame.hs view
@@ -38,7 +38,7 @@   , framePostdom   , frameProgramLoc   , setFrameBlock-  , setFrameBreakpointPostdomInfo+  , setFrameCutpointPostdomInfo   , extendFrame   , updateFrame   , mergeCallFrame@@ -58,15 +58,17 @@   , fromCallFrame   , fromReturnFrame   , frameFunctionName+  , frameStackLoc   ) where -import           Control.Lens+import           Data.Functor.Const (getConst) import           Data.Kind import qualified Data.Parameterized.Context as Ctx+import           Lens.Micro ((^.), Lens', Lens, SimpleGetter, lens, to)  import           What4.FunctionName import           What4.Interface ( Pred )-import           What4.ProgramLoc ( ProgramLoc )+import           What4.ProgramLoc ( ProgramLoc, mkProgramLoc, Position(..) )  import           Lang.Crucible.Analysis.Postdom import           Lang.Crucible.CFG.Core@@ -129,22 +131,22 @@ frameReturnType :: CallFrame sym ext blocks ret ctx -> TypeRepr ret frameReturnType CallFrame { _frameCFG = g } = cfgReturnType g -framePostdomMap :: Simple Lens (CallFrame sym ext blocks ret ctx) (CFGPostdom blocks)+framePostdomMap :: Lens' (CallFrame sym ext blocks ret ctx) (CFGPostdom blocks) framePostdomMap = lens _framePostdomMap (\s x -> s{ _framePostdomMap = x }) -frameBlockID :: Simple Lens (CallFrame sym ext blocks ret ctx) (Some (BlockID blocks))+frameBlockID :: Lens' (CallFrame sym ext blocks ret ctx) (Some (BlockID blocks)) frameBlockID = lens _frameBlockID (\s v -> s { _frameBlockID = v })  -- | List of statements to execute next.-frameStmts :: Simple Lens (CallFrame sym ext blocks ret ctx) (StmtSeq ext blocks ret ctx)+frameStmts :: Lens' (CallFrame sym ext blocks ret ctx) (StmtSeq ext blocks ret ctx) frameStmts = lens _frameStmts (\s v -> s { _frameStmts = v }) {-# INLINE frameStmts #-} -frameRegs :: Simple Lens (CallFrame sym ext blocks ret args) (RegMap sym args)+frameRegs :: Lens' (CallFrame sym ext blocks ret args) (RegMap sym args) frameRegs = lens _frameRegs (\s v -> s { _frameRegs = v })  -- | List of statements to execute next.-framePostdom :: Simple Lens (CallFrame sym ext blocks ret ctx) (Some (CrucibleBranchTarget (CrucibleLang blocks ret)))+framePostdom :: Lens' (CallFrame sym ext blocks ret ctx) (Some (CrucibleBranchTarget (CrucibleLang blocks ret))) framePostdom = lens _framePostdom (\s v -> s { _framePostdom = v })  -- | Create a new call frame.@@ -171,7 +173,7 @@             , _framePostdomMap = pdInfo             , _frameBlockID  = Some bid             , _frameRegs     = args-            , _frameStmts    = b^.blockStmts+            , _frameStmts    = b ^. blockStmts             , _framePostdom  = mkFramePostdom pds             } @@ -182,7 +184,7 @@  -- | Return program location associated with frame. frameProgramLoc :: CallFrame sym ext blocks ret ctx -> ProgramLoc-frameProgramLoc cf = firstStmtLoc (cf^.frameStmts)+frameProgramLoc cf = firstStmtLoc (cf ^. frameStmts)  setFrameBlock :: BlockID blocks args               -> RegMap sym args@@ -190,20 +192,20 @@               -> CallFrame sym ext blocks ret args setFrameBlock bid@(BlockID block_id) args f = f'     where b = frameBlockMap f Ctx.! block_id-          pds = getConst $ (f^.framePostdomMap.ixF block_id)+          pds = getConst $ (f ^. framePostdomMap.ixF block_id)           f' = f { _frameBlockID = Some bid                  , _frameRegs =  args-                 , _frameStmts = b^.blockStmts+                 , _frameStmts = b ^. blockStmts                  , _framePostdom = mkFramePostdom pds                  } -setFrameBreakpointPostdomInfo ::-  [BreakpointName] ->+setFrameCutpointPostdomInfo ::+  [CutpointName] ->   CallFrame sym ext blocks ret ctx ->   CallFrame sym ext blocks ret ctx-setFrameBreakpointPostdomInfo breakpoints f = case f of+setFrameCutpointPostdomInfo cutpoints f = case f of   CallFrame{ _frameCFG = g, _frameBlockID = Some (BlockID block_id) } -> do-    let pdInfo = breakpointPostdomInfo g breakpoints+    let pdInfo = cutpointPostdomInfo g cutpoints     f { _framePostdomMap = pdInfo       , _framePostdom  = mkFramePostdom (getConst $ pdInfo Ctx.! block_id)       }@@ -257,10 +259,10 @@                      -- ^ Arguments to override.                    } -override :: Simple Lens (OverrideFrame sym ret args) FunctionName+override :: Lens' (OverrideFrame sym ret args) FunctionName override = lens _override (\o x -> o{ _override = x }) -overrideHandle :: Simple Lens (OverrideFrame sym ret args) SomeHandle+overrideHandle :: Lens' (OverrideFrame sym ret args) SomeHandle overrideHandle = lens _overrideHandle (\o x -> o { _overrideHandle = x })  overrideRegMap :: Lens (OverrideFrame sym ret args) (OverrideFrame sym ret args')@@ -281,7 +283,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)@@ -317,8 +325,16 @@                 -> RegEntry sym (FrameRetType f) fromReturnFrame (RF _ x) = x -frameFunctionName :: Getter (SimFrame sym ext f a) FunctionName+frameFunctionName :: SimpleGetter (SimFrame sym ext f a) FunctionName frameFunctionName = to $ \case-  OF f -> f^.override+  OF f -> f ^. override   MF f -> case frameHandle f of SomeHandle h -> handleName h   RF n _ -> n++-- | Get a location for a stack frame, or Nothing if this is a return frame+frameStackLoc :: (SimFrame sym ext f a) -> Maybe ProgramLoc+frameStackLoc frame =+    case frame of+      sf@(OF _) -> Just $ mkProgramLoc (sf ^. frameFunctionName) InternalPos+      (MF f) -> Just $ frameProgramLoc f+      (RF _ _) -> Nothing
+ src/Lang/Crucible/Simulator/Cut.hs view
@@ -0,0 +1,110 @@+-----------------------------------------------------------------------+-- |+-- Module           : Lang.Crucible.Simulator.Cut+-- Description      : Support for symbolic execution cuts+-- Copyright        : (c) Galois, Inc 2019+-- License          : BSD3+-- Maintainer       : Andrei Stefanescu <andrei@galois.com>+-- Stability        : provisional+--+-- This module provides execution features for changing the state on+-- cutpoints.+-----------------------------------------------------------------------+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RecordWildCards #-}+module Lang.Crucible.Simulator.Cut+  ( cutAndReturn+  ) where++import           Control.Monad.Reader+import qualified Data.Bimap as Bimap+import           Data.Function ((&))+import           Data.HashMap.Strict (HashMap)+import qualified Data.HashMap.Strict as HashMap+import           Lens.Micro ((^.), (%~))++import           Data.Parameterized.Classes+import qualified Data.Parameterized.Context as Ctx+import           Data.Parameterized.Some+import           Data.Parameterized.TraversableFC++import qualified Lang.Crucible.Backend as C+import qualified Lang.Crucible.CFG.Core as C+import qualified Lang.Crucible.CFG.Expr as C+import qualified Lang.Crucible.Simulator.CallFrame as C+import qualified Lang.Crucible.Simulator.EvalStmt as C+import qualified Lang.Crucible.Simulator.ExecutionTree as C+import qualified Lang.Crucible.Simulator.Operations as C+import qualified Lang.Crucible.Simulator.OverrideSim as C+import qualified Lang.Crucible.Simulator.RegValue as C+import qualified What4.FunctionName as W++-- | This execution feature registers an override for a cutpoint.+--   The override summarizes the execution from the cutpoint+--   to the return from the function (similar to a tail call).+--   This feature requires a map from each function handle+--   to the list of cutpoints in the respective function with this+--   execution feature.+cutAndReturn ::+  (C.IsSymInterface sym, C.IsSyntaxExtension ext) =>+  C.CFG ext blocks init ret ->+  C.CutpointName ->+  Ctx.Assignment C.TypeRepr args ->+  C.TypeRepr ret ->+  C.OverrideSim p sym ext rtp args ret (C.RegValue sym ret) ->+  HashMap C.SomeHandle [C.CutpointName] ->+  IO (C.ExecutionFeature p sym ext rtp)+cutAndReturn C.CFG{..} cutpoint_name arg_types ret_type override all_cutpoints =+  case Bimap.lookup cutpoint_name cfgCutpoints of+    Just (Some cutpoint_block_id)+      | cutpoint_block <- C.getBlock cutpoint_block_id cfgBlockMap+      , Just Refl <- testEquality (C.blockInputs cutpoint_block) arg_types ->+        return $ C.ExecutionFeature $ \case+          C.RunningState (C.RunPostBranchMerge block_id) state+            | frame <- state ^. C.stateCrucibleFrame+            , C.SomeHandle cfgHandle == C.frameHandle frame+            , Just Refl <- testEquality+                (fmapFC C.blockInputs cfgBlockMap)+                (fmapFC C.blockInputs $ C.frameBlockMap frame)+            , Just Refl <- testEquality cutpoint_block_id block_id+            , Just Refl <- testEquality ret_type (C.frameReturnType frame) -> do+              let override_frame = C.OF $ C.OverrideFrame+                    { _override = W.functionNameFromText $+                        C.cutpointNameText cutpoint_name+                    , _overrideHandle = C.frameHandle frame+                    , _overrideRegMap = state ^.+                        C.stateCrucibleFrame . C.frameRegs+                    }+              result_state <- runReaderT (C.runOverrideSim ret_type override) $+                state & C.stateTree %~+                  C.pushCallFrame C.TailReturnToCrucible override_frame+              return $ C.ExecutionFeatureNewState result_state+          C.CallState return_handler (C.CrucibleCall block_id frame) state+            | Just cutpoints <- HashMap.lookup+                (C.frameHandle frame)+                all_cutpoints -> do+              let result_frame = C.setFrameCutpointPostdomInfo+                    cutpoints+                    frame+              result_state <- runReaderT+                (C.performFunctionCall+                  return_handler+                  (C.CrucibleCall block_id result_frame))+                state+              return $ C.ExecutionFeatureNewState result_state+          C.TailCallState value_from_value (C.CrucibleCall block_id frame) state+            | Just cutpoints <- HashMap.lookup+                (C.frameHandle frame)+                all_cutpoints -> do+              let result_frame = C.setFrameCutpointPostdomInfo+                    cutpoints+                    frame+              result_state <- runReaderT+                (C.performTailCall+                  value_from_value+                  (C.CrucibleCall block_id result_frame))+                state+              return $ C.ExecutionFeatureNewState result_state+          _ -> return C.ExecutionFeatureNoChange+    _ -> fail $ "unexpected cutpoint: " ++ show cutpoint_name
src/Lang/Crucible/Simulator/EvalStmt.hs view
@@ -45,15 +45,17 @@   ) where  import qualified Control.Exception as Ex-import           Control.Lens import           Control.Monad (foldM, when) import           Control.Monad.IO.Class (MonadIO(..))-import           Control.Monad.Reader (ReaderT(..), withReaderT)+import           Control.Monad.Reader (ReaderT(..), withReaderT, ask)+import           Data.Function ((&)) import           Data.Maybe (fromMaybe) import qualified Data.Parameterized.Context as Ctx import           Data.Parameterized.TraversableFC import qualified Data.Text as Text import           Data.Time.Clock+import           Lens.Micro ((^.), (.~), (%~), to)+import           Lens.Micro.Mtl (view) import           System.IO import           System.IO.Error as Ex import           Prettyprinter@@ -100,7 +102,7 @@   String ->   IO () evalLogFn verb s n msg = do-  let h = s^.stateContext.to printHandle+  let h = s ^. stateContext.to printHandle   if verb >= n then       do hPutStr h msg          hFlush h@@ -114,12 +116,11 @@   Expr ext ctx tp ->   ReaderT (CrucibleState p sym ext rtp blocks r ctx) IO (RegValue sym tp) evalExpr verb (App a) = ReaderT $ \s ->-  do let iteFns = s^.stateIntrinsicTypes-     let simCtx = s^.stateContext+  do let iteFns = s ^. stateIntrinsicTypes      let logFn = evalLogFn verb s-     r <- withBackend simCtx $ \bak ->+     r <- withStateBackend s $ \bak ->             evalApp bak iteFns logFn-              (extensionEval (extensionImpl (s^.stateContext)) bak iteFns logFn s)+              (extensionEval (extensionImpl (s ^. stateContext)) bak iteFns logFn s)               (\r -> runReaderT (evalReg r) s)               a      return $! r@@ -138,7 +139,7 @@   Monad m =>   Ctx.Assignment (Reg ctx) args ->   ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)-evalArgs args = ReaderT $ \s -> return $! evalArgs' (s^.stateCrucibleFrame.frameRegs) args+evalArgs args = ReaderT $ \s -> return $! evalArgs' (s ^. stateCrucibleFrame.frameRegs) args {-# INLINE evalArgs #-}  -- | Resolve the arguments for a jump.@@ -207,8 +208,10 @@   StmtSeq ext blocks r ctx' {- ^ Remaining statements in the block -} ->   ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx) stepStmt verb stmt rest =-  do ctx <- view stateContext-     let sym = ctx^.ctxSymInterface++  do st <- ask+     ctx <- view stateContext+     let sym = ctx ^. ctxSymInterface      let iTypes = ctxIntrinsicTypes ctx      globals <- view (stateTree.actFrame.gpGlobals) @@ -217,7 +220,7 @@            ExecCont p sym ext rtp' f a          continueWith f = withReaderT f (checkConsTerm verb) -     withBackend ctx $ \bak ->+     withStateBackend st $ \bak ->        case stmt of          NewRefCell tpr x ->            do let halloc = simHandleAllocator ctx@@ -402,8 +405,8 @@  stepTerm _ (ErrorStmt msg) =   do msg' <- evalReg msg-     simCtx <- view stateContext-     withBackend simCtx $ \bak -> liftIO $+     st <- ask+     withStateBackend st $ \bak -> liftIO $        case asString msg' of          Just (UnicodeLiteral txt) ->                      addFailedAssertion bak@@ -421,9 +424,9 @@ checkConsTerm verb =      do cf <- view stateCrucibleFrame -        case cf^.frameStmts of+        case cf ^. frameStmts of           ConsStmt _ _ _ -> stepBasicBlock verb-          TermStmt _ _ -> continue (RunBlockEnd (cf^.frameBlockID))+          TermStmt _ _ -> continue (RunBlockEnd (cf ^. frameBlockID))  -- | Main evaluation operation for running a single step of --   basic block evaluation.@@ -435,15 +438,15 @@   ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx) stepBasicBlock verb =   do ctx <- view stateContext-     let sym = ctx^.ctxSymInterface+     let sym = ctx ^. ctxSymInterface      let h = printHandle ctx      cf <- view stateCrucibleFrame -     case cf^.frameStmts of+     case cf ^. frameStmts of        ConsStmt pl stmt rest ->          do liftIO $               do setCurrentProgramLoc sym pl-                 let sz = regMapSize (cf^.frameRegs)+                 let sz = regMapSize (cf ^. frameRegs)                  when (verb >= 4) $ ppStmtAndLoc h (frameHandle cf) pl (ppStmt sz stmt)             stepStmt verb stmt rest @@ -495,7 +498,7 @@          k cont st      AbortState rsn st ->-      let (AH handler) = st^.abortHandler in+      let (AH handler) = st ^. abortHandler in       k (handler rsn) st      OverrideState ovr st ->
src/Lang/Crucible/Simulator/Evaluation.hs view
@@ -35,14 +35,15 @@ import           Prelude hiding (pred)  import qualified Control.Exception as Ex-import           Control.Lens import           Control.Monad import qualified Data.BitVector.Sized as BV+import           Data.Function ((&)) import qualified Data.Map.Strict as Map import           Data.Maybe import qualified Data.Text as Text import qualified Data.Vector as V import           Data.Word+import           Lens.Micro ((.~)) import           Numeric ( showHex ) import           Numeric.Natural import           GHC.Stack@@ -80,7 +81,7 @@ -- Coercion functions  integerAsChar :: Integer -> Word16-integerAsChar i = fromInteger ((i `max` 0) `min` (2^(16::Int)-1))+integerAsChar i = fromInteger ((i `max` 0) `min` (2 ^ (16::Int)-1))  complexRealAsChar :: (MonadFail m, IsExpr val)                   => val BaseComplexType@@ -490,6 +491,8 @@       do xs' <- evalSub xs          mu <- unconsSymSequence sym (muxRegForType sym itefns tpr) xs'          traverse (\ (h,tl) -> pure (Ctx.Empty Ctx.:> RV h Ctx.:> RV tl)) mu+    SequenceReverse _tpr xs ->+      reverseSymSequence sym =<< evalSub xs      --------------------------------------------------------------------     -- Symbolic Arrays@@ -646,6 +649,8 @@       iFloatFpApart @_ @fi sym x y     FloatCast fi rm (x_expr :: f (FloatType fi')) ->       iFloatCast @_ @_ @fi' sym fi rm =<< evalSub x_expr+    FloatRound _ rm (x_expr :: f (FloatType fi)) ->+      iFloatRound @_ @fi sym rm =<< evalSub x_expr     FloatFromBinary fi x_expr -> iFloatFromBinary sym fi =<< evalSub x_expr     FloatToBinary fi x_expr -> iFloatToBinary sym fi =<< evalSub x_expr     FloatFromBV fi rm x_expr -> iBVToFloat sym fi rm =<< evalSub x_expr
src/Lang/Crucible/Simulator/ExecutionTree.hs view
@@ -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@@ -111,12 +116,16 @@   , IsSymInterfaceProof   , SimContext(..)   , Metric(..)+  , ExceptionContextConfig(..)   , initSimContext   , withBackend+  , withStateBackend   , ctxSymInterface   , functionBindings   , cruciblePersonality   , profilingMetrics+  , exceptionContextConfig+  , parseExceptionContextConfig      -- * SimState   , SimState(..)@@ -138,18 +147,22 @@   , stateOverrideFrame   , stateGlobals   , stateConfiguration+  , stateProgramStack   ) where -import           Control.Lens import           Control.Monad.Reader+import           Data.Function ((&)) import           Data.Kind import           Data.Map.Strict (Map) import qualified Data.Map.Strict as Map+import           Data.Maybe(maybeToList) import           Data.Parameterized.Ctx import qualified Data.Parameterized.Context as Ctx import           Data.Text (Text)+import           Lens.Micro ((^.), (.~), Lens', Lens, SimpleGetter, Traversal', lens, to) import           System.Exit (ExitCode) import           System.IO+import           Text.Read(readMaybe) import qualified Prettyprinter as PP  import           What4.Config (Config)@@ -169,13 +182,20 @@ import           Lang.Crucible.Simulator.GlobalState (SymGlobalState) import           Lang.Crucible.Simulator.Intrinsics (IntrinsicTypes) import           Lang.Crucible.Simulator.RegMap (RegMap, emptyRegMap, RegValue, RegEntry)+import           Lang.Crucible.Simulator.SimError(ProgramStack(..)) import           Lang.Crucible.Types  ------------------------------------------------------------------------ -- 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)@@ -186,7 +206,7 @@ gpValue = lens _gpValue (\s v -> s { _gpValue = v })  -- | Access the globals stored in the global pair.-gpGlobals :: Simple Lens (GlobalPair sym u) (SymGlobalState sym)+gpGlobals :: Lens' (GlobalPair sym u) (SymGlobalState sym) gpGlobals = lens _gpGlobals (\s v -> s { _gpGlobals = v })  @@ -194,7 +214,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 +250,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 +263,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 +283,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@@ -256,11 +294,13 @@ filterCrucibleFrames _ = Nothing  -- | Iterate over frames in the result.-arFrames :: Simple Traversal (AbortedResult sym ext) (SomeFrame (SimFrame sym ext))+arFrames :: Traversal' (AbortedResult sym ext) (SomeFrame (SimFrame sym ext)) arFrames h (AbortedExec e p) =   (\(SomeFrame f') -> AbortedExec e (p & gpValue .~ f'))-     <$> h (SomeFrame (p^.gpValue))-arFrames _ (AbortedExit ec) = pure (AbortedExit ec)+     <$> h (SomeFrame (p ^. gpValue))+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@@ -272,7 +312,7 @@  where    pp :: SomeFrame (SimFrame sym ext) -> PP.Doc ann    pp (SomeFrame (OF f)) =-      PP.pretty "When calling" PP.<+> PP.viaShow (f^.override)+      PP.pretty "When calling" PP.<+> PP.viaShow (f ^. override)    pp (SomeFrame (MF f)) =       PP.pretty "In" PP.<+> PP.viaShow (frameHandle f) PP.<+>       PP.pretty "at" PP.<+> PP.pretty (plSourceLoc (frameProgramLoc f))@@ -289,7 +329,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 +365,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 +396,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,21 +420,49 @@ 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-  AbortState _ st        -> st^.stateContext-  UnwindCallState _ _ st -> st^.stateContext-  CallState _ _ st       -> st^.stateContext-  TailCallState _ _ st   -> st^.stateContext-  ReturnState _ _ _ st   -> st^.stateContext-  ControlTransferState _ st -> st^.stateContext-  RunningState _ st      -> st^.stateContext-  SymbolicBranchState _ _ _ _ st -> st^.stateContext-  OverrideState _ st -> st^.stateContext-  BranchMergeState _ st -> st^.stateContext+  AbortState _ st        -> st ^. stateContext+  UnwindCallState _ _ st -> st ^. stateContext+  CallState _ _ st       -> st ^. stateContext+  TailCallState _ _ st   -> st ^. stateContext+  ReturnState _ _ _ st   -> st ^. stateContext+  ControlTransferState _ st -> st ^. stateContext+  RunningState _ st      -> st ^. stateContext+  SymbolicBranchState _ _ _ _ st -> st ^. stateContext+  OverrideState _ st -> st ^. stateContext+  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 +479,72 @@   BranchMergeState _ st          -> Just (SomeSimState st)   InitialState _ _ _ _ _         -> Nothing +abortedGlobals ::+  Monad f =>+  -- | How to handle branches (e.g., 'AbortedBranch', 'PartialRes').+  --+  -- 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 branches (e.g., 'AbortedBranch', 'PartialRes').+  --+  -- 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 simCtx partial ->+      case partial of+        TotalRes gp -> pure (gp ^. gpGlobals)+        PartialRes loc p gp aborted -> do+          let l = gp ^. gpGlobals+          r <- abortedGlobals (handleBranch simCtx) aborted+          handleBranch simCtx loc p l r+    TimeoutResult st -> execStateGlobals handleBranch st+    AbortedResult simCtx aborted ->+      abortedGlobals (handleBranch simCtx) aborted++-- | Extract the 'SymGlobalState' from an 'ExecState'.+execStateGlobals ::+  Monad f =>+  -- | How to handle branches (e.g., 'AbortedBranch', 'PartialRes').+  --+  -- 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 +552,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 +697,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 +735,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 +751,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 +799,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 +824,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 +854,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 +927,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 +941,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 +1059,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 +1102,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)@@ -953,13 +1168,22 @@ activeFrames :: ActiveTree ctx sym ext root a args ->                 [SomeFrame (SimFrame sym ext)] activeFrames (ActiveTree ctx ar) =-  SomeFrame (ar^.partialValue^.gpValue) : parentFrames ctx+  SomeFrame (ar ^. partialValue ^. gpValue) : parentFrames ctx   ------------------------------------------------------------------------ -- 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 +1192,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 +1234,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,30 +1264,66 @@   , 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   } +data ExceptionContextConfig = +    ECCNone -- ^ do not include exceptions with context +  | ECCLimited Int+  | ECCNoLimit+  deriving(Eq, Ord, Show, Read)++parseExceptionContextConfig :: String -> Either String ExceptionContextConfig+parseExceptionContextConfig s =+  case s of+    "none" -> Right ECCNone+    "nolimit" -> Right ECCNoLimit+    _ | Just limit <- readMaybe s ->+      if limit > 0 +        then Right (ECCLimited limit)+        else Left "exception context frame limit cannot be 0 or less"+    _ -> Left "invalid exception context config - valid inputs are `none`, `nolimit`, and integers greater than 0"++ -- | Top-level state record for the simulator.  The state contained in this record --   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)-   = SimContext { _ctxBackend            :: !(SomeBackend sym)+--+--   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)-                , ctxIntrinsicTypes      :: !(IntrinsicTypes sym)+                , ctxSolverProof             :: !(forall a . IsSymInterfaceProof sym a)+                , ctxIntrinsicTypes          :: !(IntrinsicTypes sym)                   -- | Allocator for function handles-                , simHandleAllocator     :: !(HandleAllocator)+                , 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))+                , printHandle                :: !Handle+                , extensionImpl              :: ExtensionImpl p sym ext+                , _functionBindings          :: !(FunctionBindings p sym ext)+                  -- | See 'cruciblePersonality'.+                , _cruciblePersonality       :: !p+                , _profilingMetrics          :: !(Map Text (Metric p sym ext))+                , _exceptionContextConfig    :: ExceptionContextConfig                 }  -- | Create a new 'SimContext' with the given bindings.@@ -1048,15 +1338,16 @@   personality {- ^ Initial value for custom user state -} ->   SimContext personality sym ext initSimContext bak muxFns halloc h bindings extImpl personality =-  SimContext { _ctxBackend          = SomeBackend bak-             , ctxSolverProof       = \a -> a-             , ctxIntrinsicTypes    = muxFns-             , simHandleAllocator   = halloc-             , printHandle          = h-             , extensionImpl        = extImpl-             , _functionBindings    = bindings-             , _cruciblePersonality = personality-             , _profilingMetrics    = Map.empty+  SimContext { _ctxBackend               = SomeBackend bak+             , ctxSolverProof            = \a -> a+             , ctxIntrinsicTypes         = muxFns+             , simHandleAllocator        = halloc+             , printHandle               = h+             , extensionImpl             = extImpl+             , _functionBindings         = bindings+             , _cruciblePersonality      = personality+             , _profilingMetrics         = Map.empty+             , _exceptionContextConfig   = ECCNone              }  withBackend ::@@ -1065,8 +1356,27 @@   a withBackend ctx f = case _ctxBackend ctx of SomeBackend bak -> f bak +-- | Get a backend from a SimState and populate the error context+-- from the current simulation state.  This differs from `withBackend`+-- because it can use the dynamic state of the simulator for things+-- like getting stack traces for exceptions and should be preferred+-- to `withBackend` where it is possible to use.+withStateBackend ::+  SimState p sym ext rtp f args ->+    (forall bak. IsSymBackend sym bak => bak -> a) -> a+withStateBackend st f = +  if shouldHaveContext then +    let ec = stateProgramStack st+    in withBackend (st ^. stateContext) $ \bak ->+        f (withExceptionContext bak ec)+  else +    withBackend (st ^. stateContext) f+  where+    shouldHaveContext = +      st ^. stateContext . exceptionContextConfig /= ECCNone+     -- | Access the symbolic backend inside a 'SimContext'.-ctxSymInterface :: Getter (SimContext p sym ext) sym+ctxSymInterface :: SimpleGetter (SimContext p sym ext) sym ctxSymInterface = to (\ctx ->   case _ctxBackend ctx of     SomeBackend bak -> backendGetSym bak)@@ -1075,13 +1385,39 @@ 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 })  profilingMetrics :: Lens' (SimContext p sym ext) (Map Text (Metric p sym ext)) profilingMetrics = lens _profilingMetrics (\s v -> s { _profilingMetrics = v }) +exceptionContextConfig :: Lens' (SimContext p sym ext) ExceptionContextConfig+exceptionContextConfig = lens _exceptionContextConfig (\s v -> s { _exceptionContextConfig = v })+ ------------------------------------------------------------------------ -- SimState @@ -1094,6 +1430,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 +1446,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) @@ -1139,23 +1493,23 @@        }  -stateLocation :: Getter (SimState p sym ext r f a) (Maybe ProgramLoc)+stateLocation :: SimpleGetter (SimState p sym ext r f a) (Maybe ProgramLoc) stateLocation = to f  where  f :: SimState p sym ext r f a -> Maybe ProgramLoc- f st = case st^.stateTree . actFrame . gpValue of+ f st = case st ^. stateTree . actFrame . gpValue of           MF cf -> Just $! (frameProgramLoc cf)           OF _ -> Nothing           RF _ _ -> Nothing   -- | Access the 'SimContext' inside a 'SimState'-stateContext :: Simple Lens (SimState p sym ext r f a) (SimContext p sym ext)+stateContext :: Lens' (SimState p sym ext r f a) (SimContext p sym ext) stateContext = lens _stateContext (\s v -> s { _stateContext = v }) {-# INLINE stateContext #-}  -- | Access the current abort handler of a state.-abortHandler :: Simple Lens (SimState p sym ext r f a) (AbortHandler p sym ext r)+abortHandler :: Lens' (SimState p sym ext r f a) (AbortHandler p sym ext r) abortHandler = lens _abortHandler (\s v -> s { _abortHandler = v })  -- | Access the active tree associated with a state.@@ -1186,21 +1540,49 @@ stateOverrideFrame = stateTree . actFrame . gpValue . overrideSimFrame  -- | Access the globals inside a 'SimState'-stateGlobals :: Simple Lens (SimState p sym ext q f args) (SymGlobalState sym)+stateGlobals :: Lens' (SimState p sym ext q f args) (SymGlobalState sym) stateGlobals = stateTree . actFrame . gpGlobals  -- | Get the symbolic interface out of a 'SimState'-stateSymInterface :: Getter (SimState p sym ext r f a) sym+stateSymInterface :: SimpleGetter (SimState p sym ext r f a) sym stateSymInterface = stateContext . ctxSymInterface  -- | Get the intrinsic type map out of a 'SimState'-stateIntrinsicTypes :: Getter (SimState p sym ext r f args) (IntrinsicTypes sym)+stateIntrinsicTypes :: SimpleGetter (SimState p sym ext r f args) (IntrinsicTypes sym) stateIntrinsicTypes = stateContext . to ctxIntrinsicTypes  -- | Get the configuration object out of a 'SimState'-stateConfiguration :: Getter (SimState p sym ext r f args) Config-stateConfiguration = to (\s -> stateSolverProof s (getConfiguration (s^.stateSymInterface)))+stateConfiguration :: SimpleGetter (SimState p sym ext r f args) Config+stateConfiguration = to (\s -> stateSolverProof s (getConfiguration (s ^. stateSymInterface)))  -- | Provide the 'IsSymInterface' typeclass dictionary from a 'SimState' stateSolverProof :: SimState p sym ext r f args -> (forall a . IsSymInterfaceProof sym a)-stateSolverProof s = ctxSolverProof (s^.stateContext)+stateSolverProof s = ctxSolverProof (s ^. stateContext)++-- | Get the program stack from a SimState+stateProgramStack :: SimState p sym ext r f args -> ProgramStack+stateProgramStack st = +  ProgramStack+    { psFrameOmitCount = length omitted+    , psFrames = relevantFrames+    }+  where+         +    (relevantFrames, omitted) = +      case eccConfig of+        ECCNoLimit -> (rawFrames, [])+        ECCLimited limit -> splitAt limit rawFrames+        ECCNone -> ([],[])++    eccConfig = st ^. stateContext . exceptionContextConfig++    isStartFrame (SomeFrame (OF frm)) = (frm ^. override) == startFunctionName +    isStartFrame _ = False+    removeStartFrame [] = []+    removeStartFrame [f] | isStartFrame f = []+    removeStartFrame (h:t) = h:removeStartFrame t++    rawFrames = +        [ loc | SomeFrame sf <- removeStartFrame $ activeFrames (st ^. stateTree) +        , loc <- maybeToList (frameStackLoc sf)+        ]
src/Lang/Crucible/Simulator/Operations.hs view
@@ -76,17 +76,19 @@ import Prelude hiding (pred)  import qualified Control.Exception as Ex-import           Control.Lens import           Control.Monad (when, void) import           Control.Monad.IO.Class (MonadIO(..))-import           Control.Monad.Reader (ReaderT(..), withReaderT)+import           Control.Monad.Reader (ReaderT(..), ask, withReaderT) import           Control.Monad.Trans.Class (MonadTrans(..))-import           Data.Maybe (fromMaybe)+import           Data.Function ((&)) import           Data.List (isPrefixOf)+import           Data.Maybe (fromMaybe) import qualified Data.Parameterized.Context as Ctx import           Data.Parameterized.Some-import qualified Data.Vector as V import           Data.Type.Equality hiding (sym)+import qualified Data.Vector as V+import           Lens.Micro ((^.), (.~), (%~), _2, to, traverseOf)+import           Lens.Micro.Mtl (view) import           System.IO import qualified Prettyprinter as PP @@ -116,8 +118,8 @@   MuxFn p (SymGlobalState sym) ->   MuxFn p (GlobalPair sym v) mergeGlobalPair merge_fn global_fn c x y =-  GlobalPair <$> merge_fn  c (x^.gpValue) (y^.gpValue)-             <*> global_fn c (x^.gpGlobals) (y^.gpGlobals)+  GlobalPair <$> merge_fn  c (x ^. gpValue) (y ^. gpValue)+             <*> global_fn c (x ^. gpGlobals) (y ^. gpGlobals)  mergeAbortedResult ::   ProgramLoc {- ^ Program location of control-flow branching -} ->@@ -125,8 +127,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 ::@@ -156,12 +158,12 @@     BlockTarget _b_id -> do       let x = fromCallFrame x0       let y = fromCallFrame y0-      z <- mergeRegs sym muxFns p (x^.frameRegs) (y^.frameRegs)+      z <- mergeRegs sym muxFns p (x ^. frameRegs) (y ^. frameRegs)       pure $! MF (x & frameRegs .~ z)     ReturnTarget -> do       let x = fromReturnFrame x0       let y = fromReturnFrame y0-      RF (x0^.frameFunctionName) <$> muxRegEntry sym muxFns p x y+      RF (x0 ^. frameFunctionName) <$> muxRegEntry sym muxFns p x y   mergePartialResult ::@@ -170,8 +172,8 @@   CrucibleBranchTarget f args ->   MuxFn (Pred sym) (PartialResultFrame sym ext f args) mergePartialResult s tgt pred x y =-  let sym       = s^.stateSymInterface-      iteFns    = s^.stateIntrinsicTypes+  let sym       = s ^. stateSymInterface+      iteFns    = s ^. stateIntrinsicTypes       merge_val = mergeCrucibleFrame sym iteFns tgt       merge_fn  = mergeGlobalPair merge_val (globalMuxFn sym iteFns)   in@@ -254,7 +256,7 @@   SimFrame sym ext f a' ->   IO (SimFrame sym ext f a') abortCrucibleFrame sym intrinsicFns (BlockTarget _) (MF x') =-  do r' <- abortBranchRegs sym intrinsicFns (x'^.frameRegs)+  do r' <- abortBranchRegs sym intrinsicFns (x' ^. frameRegs)      return $! MF (x' & frameRegs .~ r')  abortCrucibleFrame sym intrinsicFns ReturnTarget (RF nm x') =@@ -268,8 +270,8 @@   PartialResultFrame sym ext f a' ->   IO (PartialResultFrame sym ext f a') abortPartialResult s tgt pr =-  let sym                    = s^.stateSymInterface-      muxFns                 = s^.stateIntrinsicTypes+  let sym                    = s ^. stateSymInterface+      muxFns                 = s ^. stateIntrinsicTypes       abtGp (GlobalPair v g) = GlobalPair <$> abortCrucibleFrame sym muxFns tgt v                                           <*> globalAbortBranch sym muxFns g   in partialValue abtGp pr@@ -367,7 +369,7 @@   resolvedCallName :: ResolvedCall p sym ext ret -> FunctionName-resolvedCallName (OverrideCall _ f) = f^.override+resolvedCallName (OverrideCall _ f) = f ^. override resolvedCallName (CrucibleCall _ f) = case frameHandle f of SomeHandle h -> handleName h  ---------------------------------------------------------------------@@ -404,11 +406,12 @@   SimState p sym ext rtp f args {- ^ Simulator state prior to the abort -} ->   IO (ExecState p sym ext rtp) runErrorHandler msg st =-  let ctx = st^.stateContext-      sym = ctx^.ctxSymInterface-   in withBackend ctx $ \bak ->+  let ctx = st ^. stateContext+      sym = ctx ^. ctxSymInterface+   in withStateBackend st $ \bak ->       do loc <- getCurrentProgramLoc sym-         let err = SimError loc msg+         let stk = stateProgramStack st+         let err = mkSimError loc msg (Just stk)          addProofObligation bak (LabeledPred (falsePred sym) err)          return (AbortState (AssertionFailure err) st) @@ -464,7 +467,7 @@   ExecCont p sym ext rtp (CrucibleLang blocks ret) ('Just ctx) conditionalBranch p xjmp yjmp = do   top_frame <- view (stateTree.actFrame)-  Some pd <- return (top_frame^.crucibleTopFrame.framePostdom)+  Some pd <- return (top_frame ^. crucibleTopFrame.framePostdom)    x_frame <- cruciblePausedFrame xjmp top_frame pd   y_frame <- cruciblePausedFrame yjmp top_frame pd@@ -495,7 +498,7 @@  variantCases ((p,jmp) : cs) =   do top_frame <- view (stateTree.actFrame)-     Some pd <- return (top_frame^.crucibleTopFrame.framePostdom)+     Some pd <- return (top_frame ^. crucibleTopFrame.framePostdom)       x_frame <- cruciblePausedFrame jmp top_frame pd      let y_frame = PausedFrame (TotalRes top_frame) (SwitchResumption cs) Nothing@@ -581,9 +584,9 @@  performIntraFrameMerge tgt = do   ActiveTree ctx0 er <- view stateTree-  simCtx <- view stateContext+  st <- ask   sym <- view stateSymInterface-  withBackend simCtx $ \bak ->+  withStateBackend st $ \bak ->     case ctx0 of       VFFBranch ctx assume_frame loc pred other_branch tgt' @@ -639,9 +642,9 @@                continue (RunPostBranchMerge bid)              ReturnTarget ->                handleSimReturn-                 (er^.partialValue.gpValue.frameFunctionName)+                 (er ^. partialValue.gpValue.frameFunctionName)                  (returnContext ctx0)-                 (er^.partialValue.gpValue.to fromReturnFrame)+                 (er ^. partialValue.gpValue.to fromReturnFrame)  --------------------------------------------------------------------- -- Abort handling@@ -701,9 +704,9 @@   AbortedResult sym ext {- ^ The execution that is being aborted. -} ->   ExecCont p sym ext r g args resumeValueFromFrameAbort ctx0 ar0 = do-  simCtx <- view stateContext+  st <- ask   sym <- view stateSymInterface-  withBackend simCtx $ \bak ->+  withStateBackend st $ \bak ->     case ctx0 of        -- This is the first abort.@@ -862,7 +865,7 @@   ExecCont p sym ext rtp (OverrideLang r) ('Just args) overrideSymbolicBranch p thn_args thn thn_pos els_args els els_pos =   do top_frm <- view (stateTree.actFrame)-     let fnm     = top_frm^.gpValue.overrideSimFrame.override+     let fnm     = top_frm ^. gpValue.overrideSimFrame.override      let thn_loc = mkProgramLoc fnm <$> thn_pos      let els_loc = mkProgramLoc fnm <$> els_pos      let thn_frm = PausedFrame (TotalRes top_frm) (OverrideResumption thn thn_args) thn_loc@@ -910,9 +913,9 @@  intra_branch p t_label f_label tgt = do   ctx <- asContFrame <$> view stateTree-  simCtx <- view stateContext+  st <- ask   sym <- view stateSymInterface-  withBackend simCtx $ \bak ->+  withStateBackend st $ \bak ->     case asConstantPred p of       Nothing ->         ReaderT $ return . SymbolicBranchState p t_label f_label tgt@@ -943,13 +946,13 @@   ExecCont p sym ext rtp f ('Just dc_args) performIntraFrameSplit p a_frame o_frame tgt =   do ctx <- asContFrame <$> view stateTree-     simCtx <- view stateContext+     st <- ask      sym <- view stateSymInterface      loc <- liftIO $ getCurrentProgramLoc sym      a_frame' <- pushPausedFrame a_frame      o_frame' <- pushPausedFrame o_frame -     assume_frame <- withBackend simCtx $ \bak ->+     assume_frame <- withStateBackend st $ \bak ->        liftIO $ assumeInNewFrame bak (BranchCondition loc (pausedLoc a_frame') p)       -- Create context for paused frame.@@ -1090,8 +1093,8 @@   ActiveTree p sym ext ret f args ->   ActiveTree p sym ext ret f args extractCurrentPath t =-  ActiveTree (vffSingleContext (t^.actContext))-             (TotalRes (t^.actFrame))+  ActiveTree (vffSingleContext (t ^. actContext))+             (TotalRes (t ^. actFrame))  vffSingleContext ::   ValueFromFrame p sym ext ret f ->@@ -1118,9 +1121,9 @@ -- -- | Return all branch conditions along path to this node. -- branchConditions :: ActiveTree ctx sym ext ret f args -> [Pred sym] -- branchConditions t =---   case t^.actResult of---     TotalRes _ -> vffBranchConditions (t^.actContext)---     PartialRes p _ _ -> p : vffBranchConditions (t^.actContext)+--   case t ^. actResult of+--     TotalRes _ -> vffBranchConditions (t ^. actContext)+--     PartialRes p _ _ -> p : vffBranchConditions (t ^. actContext)  -- vffBranchConditions :: ValueFromFrame p sym ext ret f --                     -> [Pred sym]
src/Lang/Crucible/Simulator/OverrideSim.hs view
@@ -75,32 +75,35 @@   , useIntrinsic     -- * Typed overrides   , TypedOverride(..)+  , typedOverride   , SomeTypedOverride(..)   , runTypedOverride+  , bindTypedOverride     -- * Re-exports   , Lang.Crucible.Simulator.ExecutionTree.Override   ) where  import           Control.Exception-import           Control.Lens import           Control.Monad hiding (fail) import qualified Control.Monad.Catch as X import           Control.Monad.IO.Class (MonadIO(..)) 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           Data.Function ((&)) import qualified Data.Parameterized.Context as Ctx+import           Data.Parameterized.TraversableFC (fmapFC) import           Data.Proxy import qualified Data.Text as T import           Data.Traversable (for)+import           Lens.Micro ((^.), (.~), to)+import           Lens.Micro.Mtl (use, view, (.=), (%=)) import           Numeric.Natural (Natural) import           System.Exit import           System.IO import           System.IO.Error -import           Data.Parameterized.TraversableFC (fmapFC)- import           What4.Config import           What4.Interface import           What4.FunctionName@@ -135,7 +138,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 +159,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 ->@@ -216,13 +225,14 @@   (forall bak. IsSymBackend sym bak => bak -> OverrideSim p sym ext rtp args ret a) ->   OverrideSim p sym ext rtp args ret a ovrWithBackend k =-  do simCtx <- use stateContext-     ctxSolverProof simCtx (withBackend simCtx k)+  do simSt <- get+     simCtx <- use stateContext+     ctxSolverProof simCtx (withStateBackend simSt k)  instance MonadVerbosity (OverrideSim p sym ext rtp args ret) where   getVerbosity =     do ctx <- getContext-       let cfg = ctxSolverProof ctx (getConfiguration (ctx^.ctxSymInterface))+       let cfg = ctxSolverProof ctx (getConfiguration (ctx ^. ctxSymInterface))        v <- liftIO (getOpt =<< getOptionSetting verbosity cfg)        return (fromInteger v) @@ -572,7 +582,7 @@            go !i ((p,m,mpos):xs) =              let msg = T.pack ("after branch " ++ show i)                  m'  = ReaderT (runStateContT (unSim m) c')-              in overrideSymbolicBranch p all_args m' mpos old_args (go (i+1) xs) (Just (OtherPos msg))+              in overrideSymbolicBranch p all_args m' mpos old_args (go (i + 1) xs) (Just (OtherPos msg))        go (0::Integer) xs0  -- | Non-deterministically choose among several feasible branches.@@ -627,7 +637,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 +700,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 +728,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))
src/Lang/Crucible/Simulator/PathSatisfiability.hs view
@@ -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 #-}@@ -25,8 +25,8 @@   , BranchResult(..)   ) where -import           Control.Lens( (^.) ) import           Control.Monad.Reader+import           Lens.Micro ((^.)) import qualified Prettyprinter as PP  import           Lang.Crucible.Backend@@ -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)@@ -82,11 +88,11 @@           considerSatisfiability ploc p >>= \case                IndeterminateBranchResult ->                  return ExecutionFeatureNoChange-               NoBranch chosen_branch -> withBackend (st ^. stateContext) $ \bak ->+               NoBranch chosen_branch -> withStateBackend st $ \bak ->                  do p' <- if chosen_branch then return p else notPred sym p                     let frm = if chosen_branch then tp else fp                     addAssumption bak (BranchCondition loc (pausedLoc frm) p')-                    ExecutionFeatureNewState <$> runReaderT (resumeFrame frm (asContFrame (st^.stateTree))) st+                    ExecutionFeatureNewState <$> runReaderT (resumeFrame frm (asContFrame (st ^. stateTree))) st                UnsatisfiableContext ->                  return (ExecutionFeatureNewState (AbortState (InfeasibleBranch loc) st))    where
src/Lang/Crucible/Simulator/PathSplitting.hs view
@@ -35,12 +35,12 @@   , executeCrucibleDFSPaths   ) where -import           Control.Lens ( (^.) ) import           Control.Monad.Reader import           Data.IORef import           Data.Sequence( Seq ) import qualified Data.Sequence as Seq import           Data.Word+import           Lens.Micro ((^.))  import           What4.Interface import           What4.ProgramLoc@@ -97,8 +97,7 @@   IO (ExecState p sym ext rtp) restoreWorkItem (WorkItem branchPred loc frm st assumes) =   do let sym = st ^. stateSymInterface-     let simCtx = st ^. stateContext-     withBackend simCtx $ \bak ->+     withStateBackend st $ \bak ->       do setCurrentProgramLoc sym loc          restoreAssumptionState bak assumes          addAssumption bak (BranchCondition loc (pausedLoc frm) branchPred)@@ -117,7 +116,7 @@   ExecutionFeature p sym ext rtp pathSplittingFeature wl = ExecutionFeature $ \case   SymbolicBranchState p trueFrame falseFrame _bt st ->-    withBackend (st^.stateContext) $ \bak ->+    withStateBackend st $ \bak ->     do let sym = st ^. stateSymInterface        pnot <- notPred sym p        assumes <- saveAssumptionState bak
src/Lang/Crucible/Simulator/PositionTracking.hs view
@@ -21,8 +21,8 @@   ( positionTrackingFeature   ) where -import Control.Lens ((^.), to) import Control.Monad.IO.Class+import Lens.Micro ((^.), to)  import Lang.Crucible.Backend import Lang.Crucible.Simulator.CallFrame@@ -44,8 +44,7 @@      IO (ExecutionFeatureResult p sym ext rtp)    onStep exst@(RunningState (RunBlockStart _bid) st) =      do let loc = st ^. (stateCrucibleFrame.to frameProgramLoc)-        let simCtx = st ^. stateContext-        liftIO $ withBackend simCtx $ \bak ->+        liftIO $ withStateBackend st $ \bak ->           addAssumptions bak (singleEvent (LocationReachedEvent loc))         return (ExecutionFeatureModifiedState exst)
src/Lang/Crucible/Simulator/Profiling.hs view
@@ -47,9 +47,9 @@   ) where  import qualified Control.Exception as Ex-import           Control.Lens import           Control.Monad ((<=<), when) import           Data.Foldable (toList)+import           Data.Functor.Identity (Identity(..), runIdentity) import           Data.Hashable import           Data.HashSet (HashSet) import qualified Data.HashSet as HashSet@@ -64,6 +64,7 @@ import           Data.Time.Clock import           Data.Time.Clock.POSIX import           Data.Time.Format+import           Lens.Micro ((^.)) import           System.IO (withFile, IOMode(..), hPutStrLn) import           Text.JSON import           GHC.Generics (Generic)@@ -210,7 +211,7 @@ symProUIString :: String -> String -> ProfilingTable -> IO String symProUIString nm source tbl =   do js <- symProUIJSON nm source tbl-     return ("data.receiveData("++ encode js ++ ");")+     return ("data.receiveData(" ++ encode js ++ ");")   symProUIJSON :: String -> String -> ProfilingTable -> IO JSValue@@ -348,7 +349,7 @@ nextEventID :: ProfilingTable -> IO Integer nextEventID tbl =   do i <- readIORef (eventIDRef tbl)-     writeIORef (eventIDRef tbl) $! (i+1)+     writeIORef (eventIDRef tbl) $! (i + 1)      return i  dedupEvent :: ProfilingTable -> EventDedup -> IO () -> IO ()@@ -456,18 +457,18 @@       InitialState _ _ _ _ _ ->         enterEvent tbl startFunctionName Nothing       CallState _rh call st ->-        enterEvent tbl (resolvedCallName call) (st^.stateLocation)+        enterEvent tbl (resolvedCallName call) (st ^. stateLocation)       ReturnState nm _ _ _ ->         exitEvent tbl nm       TailCallState _ call st ->-        do exitEvent tbl (st^.stateTree.actFrame.gpValue.frameFunctionName)-           enterEvent tbl (resolvedCallName call) (st^.stateLocation)+        do exitEvent tbl (st ^. stateTree.actFrame.gpValue.frameFunctionName)+           enterEvent tbl (resolvedCallName call) (st ^. stateLocation)       SymbolicBranchState{} ->         modifyIORef' (metricSplits (metrics tbl)) succ       AbortState{} ->         modifyIORef' (metricAborts (metrics tbl)) succ       UnwindCallState _ _ st ->-        exitEvent tbl (st^.stateTree.actFrame.gpValue.frameFunctionName)+        exitEvent tbl (st ^. stateTree.actFrame.gpValue.frameFunctionName)       BranchMergeState tgt st ->         when (isMergeState tgt st)              (modifyIORef' (metricMerges (metrics tbl)) succ)@@ -476,16 +477,16 @@   when (recordCoverage filt) $     case exst of       ControlTransferState res st ->-        let funcName = st^.stateTree.actFrame.gpValue.frameFunctionName in+        let funcName = st ^. stateTree.actFrame.gpValue.frameFunctionName in         case res of           ContinueResumption (ResolvedJump blk _) ->-            blockEvent tbl funcName (st^.stateLocation) (Some blk)+            blockEvent tbl funcName (st ^. stateLocation) (Some blk)           CheckMergeResumption (ResolvedJump blk _) ->-            blockEvent tbl funcName (st^.stateLocation) (Some blk)+            blockEvent tbl funcName (st ^. stateLocation) (Some blk)           _ -> return ()       RunningState (RunBlockEnd _) st ->-        let funcName = st^.stateTree.actFrame.gpValue.frameFunctionName in-        case st^.stateTree.actFrame.gpValue.crucibleSimFrame.frameStmts of+        let funcName = st ^. stateTree.actFrame.gpValue.frameFunctionName in+        case st ^. stateTree.actFrame.gpValue.crucibleSimFrame.frameStmts of           TermStmt loc term             | Just blocks <- termStmtNextBlocks term,               length blocks >= 2 ->@@ -498,7 +499,7 @@   SimState p sym ext root f args ->   Bool isMergeState tgt st =-  case st^.stateTree.actContext of+  case st ^. stateTree.actContext of     VFFBranch _ctx _assume_frame _loc _p other_branch tgt'       | Just Refl <- testEquality tgt tgt' ->           case other_branch of
+ src/Lang/Crucible/Simulator/RecordAndReplay.hs view
@@ -0,0 +1,368 @@+{-# 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,+  getConcreteRecordedTrace,+  recordFeature,+  replayFeature,+  initialTrace,+  traceGlobal,+  emptyRecordedTrace+) where++import Control.Exception qualified as X+import Data.Foldable qualified as F+import Data.Function ((&))+import Data.Kind (Type)+import Data.Sequence qualified as Seq+import Data.Text qualified as Text+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.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 Lens.Micro ((^.), (%~))+import Lens.Micro qualified as Lens+import Lens.Micro.TH (makeLenses)+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+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.+getRecordedTrace ::+  C.SymGlobalState sym ->+  RecordState p sym ext rtp ->+  sym ->+  IO (RecordedTrace sym)+getRecordedTrace globals (RecordState g) sym = do+  case C.lookupGlobal g globals of+    Nothing -> X.throw TraceGlobalNotDefined+    Just s -> RecordedTrace <$> CSSS.reverseSymSequence sym s++-- | Obtain a 'RecordedTrace' after execution using concrete evaluation.+--+-- When a concrete evaluation function for 'W4.Pred's is available and only the+-- concretized trace is desired, this is more performant than the more general+-- 'getRecordedTrace'.+getConcreteRecordedTrace ::+  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)+getConcreteRecordedTrace 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 pure s+      let reversed = Seq.reverse concretized+      CSSS.fromListSymSequence sym (F.toList reversed)++{- | 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.withStateBackend st $ \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
src/Lang/Crucible/Simulator/RegValue.hs view
@@ -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)
src/Lang/Crucible/Simulator/SimError.hs view
@@ -16,23 +16,30 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE PatternSynonyms #-} module Lang.Crucible.Simulator.SimError (     SimErrorReason(..)-  , SimError(..)+  , SimError(.., SimError)+  , ProgramStack(..)+  , mkSimError+  , simErrorReason+  , simErrorLoc+  , simErrorContext   , simErrorReasonMsg   , simErrorDetailsMsg   , ppSimError+  , ppProgramStack   ) where  import GHC.Stack (CallStack)  import Control.Exception import Data.String-import Data.Typeable import Prettyprinter  import What4.ProgramLoc + ------------------------------------------------------------------------ -- SimError @@ -49,15 +56,23 @@    | ResourceExhausted String       -- ^ A loop iteration count, or similar resource limit,       --   was exceeded.- deriving (Typeable) -data SimError-   = SimError-   { simErrorLoc :: !ProgramLoc-   , simErrorReason :: !SimErrorReason-   }- deriving (Typeable)+data SimError +   = SimErrorWithContext !ProgramLoc !SimErrorReason !(Maybe ProgramStack)+ +-- | This pattern synonym constructs SimErrors without a program stack context when used +-- as an expression and ignores the program stack when used as a pattern.  It exists+-- because SimError did not used to have a `ProgramStack`, and there are many usages+-- in the code of the previous constructor which is approximated by this pattern.+--+-- Using SimErrorWithContext should be preferred.+pattern SimError :: ProgramLoc -> SimErrorReason -> SimError+pattern SimError { simErrorLoc, simErrorReason } <- SimErrorWithContext simErrorLoc simErrorReason _+  where SimError loc reason = SimErrorWithContext loc reason Nothing +simErrorContext :: SimError -> Maybe ProgramStack+simErrorContext (SimErrorWithContext _ _ c) = c+ simErrorReasonMsg :: SimErrorReason -> String simErrorReasonMsg (GenericSimError msg) = msg simErrorReasonMsg (Unsupported _ msg) = "Unsupported feature: " ++ msg@@ -70,6 +85,9 @@ simErrorDetailsMsg (Unsupported stk _) = show stk simErrorDetailsMsg _ = "" +mkSimError :: ProgramLoc -> SimErrorReason -> Maybe ProgramStack -> SimError+mkSimError loc reason mbCtx = SimErrorWithContext loc reason mbCtx+ instance IsString SimErrorReason where   fromString = GenericSimError @@ -83,13 +101,38 @@ ppSimError er =   vcat $ [ pretty (plSourceLoc loc) <> pretty ": error: in" <+> pretty (plFunction loc)          , pretty (simErrorReasonMsg rsn)-         ] ++ if null details-              then []-              else [ pretty "Details:"-                   , indent 2 (vcat (pretty <$> lines details))-                   ]+         ] ++ (if null details+               then []+               else [ pretty "Details:"+                    , indent 2 (vcat (pretty <$> lines details))+                    ])+          ++ (case simErrorContext er of+                Nothing -> []+                Just (ProgramStack _ []) -> []+                Just ctx -> [ pretty "Context:"+                            , indent 2 (ppProgramStack ctx)+                            ])  where loc = simErrorLoc er        details = simErrorDetailsMsg rsn-       rsn = simErrorReason er+       rsn = simErrorReason er           +-- | Representation of the program stack for providing dynamic+-- context for SimErrors+data ProgramStack = ProgramStack +  { -- | Number of calling frames omitted in the stack trace+    psFrameOmitCount :: Int+    -- | The visible part of the stack strace+  , psFrames :: [ProgramLoc]+  }++ppProgramStack :: ProgramStack -> Doc ann+ppProgramStack (ProgramStack omittedCount frames) = vcat ((ppLoc <$> frames) ++ omitLine)+  where+    omitLine =+      if omittedCount <= 0+        then []+        else [ pretty "..."  <+> pretty omittedCount <+> pretty "calling frames omitted" ]+    ppLoc l = pretty (plSourceLoc l) <> pretty ":" <+> pretty (plFunction l)+ instance Exception SimError+
src/Lang/Crucible/Simulator/SymSequence.hs view
@@ -25,6 +25,7 @@ , traverseSymSequence , concreteizeSymSequence , concretizeSymSequence+, reverseSymSequence , prettySymSequence    -- * Low-level evaluation primitives@@ -34,6 +35,7 @@ ) where  import           Control.Monad.State+import           Data.Coerce (coerce) import           Data.Functor.Const import           Data.Kind (Type) import           Data.IORef@@ -195,6 +197,39 @@      pure (SymSequenceAppend n xs ys)  +-- | Reverse a 'SymSequence'+reverseSymSequence :: forall sym a. sym -> SymSequence sym a -> IO (SymSequence sym a)+reverseSymSequence sym = \s -> coerce (evalWithFreshCache f s)+  where+    f :: (SymSequence sym a -> IO (Const (SymSequence sym a) a))+      -> SymSequence sym a -> IO (Const (SymSequence sym a) a)+    f loop = \case+      SymSequenceNil -> pure (coerce SymSequenceNil)+      s@(SymSequenceCons{}) -> coerce (reverseConsSpine loop SymSequenceNil s)+      SymSequenceAppend _ xs ys ->+        do xs' <- coerce (loop xs)+           ys' <- coerce (loop ys)+           coerce (appendSymSequence sym ys' xs')+      SymSequenceMerge _ p xs ys ->+        do xs' <- coerce (loop xs)+           ys' <- coerce (loop ys)+           coerce (muxSymSequence sym p xs' ys')++    -- Walk a cons-spine with an accumulator, producing a flat cons-list.+    -- Falls back to cached 'loop' when a non-Cons node is reached.+    reverseConsSpine ::+      (SymSequence sym a -> IO (Const (SymSequence sym a) a)) ->+      SymSequence sym a ->+      SymSequence sym a ->+      IO (SymSequence sym a)+    reverseConsSpine loop acc = \case+      SymSequenceCons _ v tl -> do+        acc' <- consSymSequence sym v acc+        reverseConsSpine loop acc' tl+      other -> do+        otherReversed <- coerce (loop other)+        appendSymSequence sym otherReversed acc+ -- | Test if a sequence is nil (is empty) isNilSymSequence :: forall sym a.   IsExprBuilder sym =>@@ -458,7 +493,7 @@ computeOccMap = loop   where     visit n k m-      | Just i <- Map.lookup n m = Map.insert n (i+1) m+      | Just i <- Map.lookup n m = Map.insert n (i + 1) m       | otherwise = k (Map.insert n 1 m)      loop SymSequenceNil = id
src/Lang/Crucible/Syntax.hs view
@@ -85,18 +85,20 @@   , littleEndianStore   ) where -import           Control.Lens import qualified Data.BitVector.Sized as BV+import           Data.Function ((&)) import           Data.Kind import           Data.Parameterized.Classes import qualified Data.Parameterized.Context as Ctx import           Data.Parameterized.Some import           Data.Text (Text) import qualified Data.Vector as V+import           Lens.Micro ((.~)) import           Numeric.Natural  import           Lang.Crucible.CFG.Expr import           Lang.Crucible.FunctionHandle+import           Lang.Crucible.Panic (panic) import           Lang.Crucible.Types  import           What4.Utils.StringLiteral@@ -330,7 +332,7 @@            , KnownRepr TypeRepr ret            , KnownCtx  TypeRepr args            )-        => e (FunctionHandleType (args::>tp) ret)+        => e (FunctionHandleType (args ::> tp) ret)         -> e tp         -> e (FunctionHandleType args ret) closure h a = app (Closure knownRepr knownRepr h knownRepr a)@@ -408,7 +410,7 @@                   (app $ BVAdd addrWidth basePtr (app $ BVLit addrWidth (BV.mkBV addrWidth (toInteger (n-1)))))                   (app $ BVSelect idx cellWidth valWidth v)                   (go (n-1))-        go _ = error "bad size parameters in bigEndianStore!"+        go _ = panic "bigEndianStore" ["bad size parameters!"]  littleEndianStore    :: (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)@@ -429,7 +431,7 @@                   (app $ BVAdd addrWidth basePtr (app $ BVLit addrWidth (BV.mkBV addrWidth (toInteger (n-1)))))                   (app $ BVSelect idx cellWidth valWidth v)                   (go (n-1))-        go _ = error "bad size parameters in littleEndianStore!"+        go _ = panic "littleEndianStore" ["bad size parameters!"]  concatExprs :: forall w a expr             .  (IsExpr expr, 1 <= w)@@ -438,7 +440,7 @@             -> (forall w'. (1 <= w') => NatRepr w' -> expr (BVType w') -> a)             -> a -concatExprs _ [] = \_ -> error "Cannot concatenate 0 elements together"+concatExprs _ [] = \_ -> panic "concatExprs" ["Cannot concatenate 0 elements together"] concatExprs w (a:as) = go a as   where go :: (1 <= w)@@ -448,7 +450,7 @@           -> a        go x0 [] k     = k w x0        go x0 (x:xs) k = go x xs (\(w'::NatRepr w') z ->-            withLeqProof (leqAdd LeqProof w' :: LeqProof 1 (w+w'))+            withLeqProof (leqAdd LeqProof w' :: LeqProof 1 (w + w'))               (k (addNat w w') (app $ BVConcat w w' x0 z)))  bigEndianLoad@@ -470,7 +472,7 @@           concatExprs cellWidth segs $ \w x ->             case testEquality w valWidth of               Just Refl -> x-              Nothing -> error "bad size parameters in bigEndianLoad!"+              Nothing -> panic "bigEndianLoad" ["bad size parameters!"]   bigEndianLoadDef@@ -494,7 +496,7 @@           concatExprs cellWidth segs $ \w x ->             case testEquality w valWidth of               Just Refl -> x-              Nothing -> error "bad size parameters in bigEndianLoadDef!"+              Nothing -> panic "bigEndianLoadDef" ["bad size parameters!"]  littleEndianLoad    :: (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)@@ -515,7 +517,7 @@           concatExprs cellWidth segs $ \w x ->             case testEquality w valWidth of               Just Refl -> x-              Nothing -> error "bad size parameters in littleEndianLoad!"+              Nothing -> panic "littleEndianLoad" ["bad size parameters!"]  littleEndianLoadDef    :: (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)@@ -538,4 +540,4 @@           concatExprs cellWidth segs $ \w x ->             case testEquality w valWidth of               Just Refl -> x-              Nothing -> error "bad size parameters in littleEndianLoadDef!"+              Nothing -> panic "littleEndianLoadDef" ["bad size parameters!"]
src/Lang/Crucible/Types.hs view
@@ -383,9 +383,9 @@     StringMapRepr :: !(TypeRepr tp) -> TypeRepr (StringMapType tp) -   SymbolicArrayRepr :: !(Ctx.Assignment BaseTypeRepr (idx::>tp))+   SymbolicArrayRepr :: !(Ctx.Assignment BaseTypeRepr (idx ::> tp))                      -> !(BaseTypeRepr t)-                     -> TypeRepr (SymbolicArrayType (idx::>tp) t)+                     -> TypeRepr (SymbolicArrayType (idx ::> tp) t)     -- A reference to a symbolic struct.    SymbolicStructRepr :: Ctx.Assignment BaseTypeRepr ctx
src/Lang/Crucible/Utils/BitSet.hs view
@@ -12,6 +12,7 @@ -- built on top of GHC-native Integers. ------------------------------------------------------------------------ module Lang.Crucible.Utils.BitSet+{-# DEPRECATED "This module is deprecated" #-} ( BitSet , getBits , empty@@ -35,7 +36,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)@@ -47,7 +48,7 @@ empty = BitSet zeroBits  null :: BitSet a -> Bool-null = (0==) . getBits+null = (0 ==) . getBits  singleton :: Enum a => a -> BitSet a singleton a = BitSet (bit (fromEnum a))@@ -81,19 +82,19 @@   where go :: Enum a => Integer -> Int -> [a]         go 0 _ = []         go x i-           | y .&. 0xffffffff == 0 = go (shiftR x 32) $! (i+32)-           | y .&. 0x0000ffff == 0 = go (shiftR x 16) $! (i+16)-           | y .&. 0x000000ff == 0 = go (shiftR x  8) $! (i+ 8)+           | y .&. 0xffffffff == 0 = go (shiftR x 32) $! (i + 32)+           | y .&. 0x0000ffff == 0 = go (shiftR x 16) $! (i + 16)+           | y .&. 0x000000ff == 0 = go (shiftR x  8) $! (i + 8)            | otherwise = concat-               [ if testBit y 0 then [toEnum (i+0)] else []-               , if testBit y 1 then [toEnum (i+1)] else []-               , if testBit y 2 then [toEnum (i+2)] else []-               , if testBit y 3 then [toEnum (i+3)] else []-               , if testBit y 4 then [toEnum (i+4)] else []-               , if testBit y 5 then [toEnum (i+5)] else []-               , if testBit y 6 then [toEnum (i+6)] else []-               , if testBit y 7 then [toEnum (i+7)] else []-               , go (shiftR x 8) $! (i+8)+               [ if testBit y 0 then [toEnum (i + 0)] else []+               , if testBit y 1 then [toEnum (i + 1)] else []+               , if testBit y 2 then [toEnum (i + 2)] else []+               , if testBit y 3 then [toEnum (i + 3)] else []+               , if testBit y 4 then [toEnum (i + 4)] else []+               , if testBit y 5 then [toEnum (i + 5)] else []+               , if testBit y 6 then [toEnum (i + 6)] else []+               , if testBit y 7 then [toEnum (i + 7)] else []+               , go (shiftR x 8) $! (i + 8)                ]            where y :: Word32
src/Lang/Crucible/Utils/CoreRewrite.hs view
@@ -22,11 +22,11 @@ ( annotateCFGStmts ) where -import           Control.Lens-+import           Data.Function ((&)) import qualified Data.Parameterized.Context as Ctx import           Data.Parameterized.Map (Pair(..)) import           Data.Parameterized.TraversableFC+import           Lens.Micro ((^.), (%~))  import           Lang.Crucible.CFG.Core import           Lang.Crucible.CFG.Extension
src/Lang/Crucible/Utils/MuxTree.hs view
@@ -34,11 +34,10 @@   , muxTreeGt   ) where -import           Control.Lens (folded)- import           Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import qualified Data.Map.Merge.Strict as Map+import           Lens.Micro (folded)  import           What4.Interface import           Lang.Crucible.Panic
src/Lang/Crucible/Utils/Structural.hs view
@@ -23,6 +23,7 @@ import Data.Parameterized.TH.GADT import Data.Parameterized.TraversableFC +import Lang.Crucible.Panic (panic) import Lang.Crucible.Utils.PrettyPrint (ppFn, commas)  ------------------------------------------------------------------------@@ -52,7 +53,7 @@   let vars = varE <$> nms   let nm' = case nameBase nm of               c:r -> toLower c : r-              [] -> error "matchPretty given constructor with empty name."+              [] -> panic "matchPretty" ["given constructor with empty name"]   let mkPP0 v tp = do         me <- matchPat tp         case me of
src/Lang/Crucible/Vector.hs view
@@ -102,6 +102,6 @@   Endian ->   NatRepr i {- ^ Split bit-vectors in this many parts -} ->   NatRepr w {- ^ Length of bit-vectors in the result -} ->-  Vector n (f (BVType (i * w))) -> Vector (n*i) (f (BVType w))+  Vector n (f (BVType (i * w))) -> Vector (n * i) (f (BVType w)) splitVecBV e i w xs = join i (fromBV e i w <$> xs) {-# Inline splitVecBV #-}
test/absint/Max.hs view
@@ -32,7 +32,7 @@ maxDom :: Domain Max' maxDom = d   where-    d = pointed j (==) (WTOWidening (>10) w)+    d = pointed j (==) (WTOWidening (> 10) w)     j (Max i1) (Max i2) = Pointed (Max (max i1 i2))     w _ _ = Top
test/absint/WTO.hs view
@@ -18,6 +18,7 @@ import qualified Test.Tasty.QuickCheck as T  import Lang.Crucible.Analysis.Fixpoint.Components+import Lang.Crucible.Panic (panic)  wtoTests :: T.TestTree wtoTests = T.testGroup "WeakTopologicalOrdering" [@@ -97,7 +98,7 @@ -- -- The graphs are not all connected. mkRandomGraph :: Int -> QC.Gen RandomGraph-mkRandomGraph ((+1) -> sz) = do+mkRandomGraph ((+ 1) -> sz) = do   nEdges <- QC.choose (2, 2*sz)   srcs <- replicateM nEdges (QC.choose (0, sz))   dsts <- replicateM nEdges (QC.choose (0, sz))@@ -161,7 +162,7 @@ -- -- Not defined for empty graphs toCFG :: RandomGraph -> (Int, (Int -> [Int]))-toCFG (RG []) = error "Empty graph"+toCFG (RG []) = panic "toCFG" ["Empty graph"] toCFG (RG edges@((s0, _) : _)) =   (s0, \n -> [ dst | (src, dst) <- edges, n == src])
test/helpers/Main.hs view
@@ -1,9 +1,10 @@ {-# LANGUAGE AllowAmbiguousTypes #-}-module Main where -import Control.Lens ((^.))+module Main (main) where+ import Data.List (isInfixOf) import Data.Maybe (fromMaybe)+import Lens.Micro ((^.))  import Test.Hspec import Test.Tasty@@ -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
+ test/helpers/SymSequence.hs view
@@ -0,0 +1,15 @@+{-# LANGUAGE ImportQualifiedPost #-}++module SymSequence (tests) where++import Test.Tasty qualified as TT++import SymSequence.Properties qualified as Properties+import SymSequence.Reverse qualified as Reverse++tests :: TT.TestTree+tests =+  TT.testGroup "SymSequence"+  [ Properties.tests+  , Reverse.tests+  ]
+ test/helpers/SymSequence/Properties.hs view
@@ -0,0 +1,308 @@+{-# LANGUAGE EmptyDataDeriving #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ImportQualifiedPost #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++module SymSequence.Properties (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.Panic (panic)+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 -> panic "asConstPred" ["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+  OReverse :: Op a (List a) -> Op a (List a)+  -- 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+      OReverse l -> fun1 "reverse" 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+    , genReverse+    ]+  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++    genReverse = OReverse <$> sub1++---------------------------------------------------------------------+-- 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+    OReverse l -> reverse (opList l)++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 -> panic "opSeq" ["SymSequence: symbolic length"]+    OReverse l -> S.reverseSymSequence sym =<< opSeq sym l
+ test/helpers/SymSequence/Reverse.hs view
@@ -0,0 +1,174 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ImportQualifiedPost #-}+{-# LANGUAGE RankNTypes #-}++module SymSequence.Reverse (tests) where++import Data.Parameterized.Nonce qualified as Nonce+import Data.Parameterized.Some (Some(Some))+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 System.Timeout (timeout)+import Test.Tasty qualified as TT+import Test.Tasty.HUnit qualified as TTU+import What4.Expr (EmptyExprBuilderState(EmptyExprBuilderState))+import What4.Expr.Builder (newExprBuilder)+import What4.FloatMode (FloatModeRepr(FloatIEEERepr))+import What4.Interface qualified as WI++---------------------------------------------------------------------+-- Tests++tests :: TT.TestTree+tests = TT.testGroup "reverse performance"++  -- Pure cons-list (no branching, no appends):+  --+  --   Cons -> Cons -> ... -> Cons -> Nil+  --+  [ reverseTest "reverse large cons-list" $ \sym ->+      buildSeq sym 1500000 $ \s _ acc ->+        S.consSymSequence s True acc++  -- Cons-list with a Mux node every 100 elements.+  -- At each Mux both branches point to the same shared tail:+  --+  --                                 /--true---\+  --   Cons -> ... -> Cons -> Mux ->            Cons -> ... -> Nil+  --                                 \--false--/+  --+  , reverseTest "reverse cons-list with periodic muxes" $ \sym ->+      buildSeq sym 250000 $ \s i acc -> do+        acc' <-+          if i `mod` 100 == 0+          then do+            t <- S.consSymSequence s True acc+            f <- S.consSymSequence s False acc+            S.muxSymSequence s (WI.truePred s) t f+          else pure acc+        S.consSymSequence s True acc'++  -- Left-nested chain of Appends:+  --+  --   Append -> Append -> ... -> Append -> Nil+  --+  , reverseTest "reverse left-nested appends" $ \sym ->+      buildSeq sym 250000 $ \s _ acc -> do+        singleton <- S.consSymSequence s True S.SymSequenceNil+        S.appendSymSequence s acc singleton++  -- Right-nested chain of Appends:+  --+  --   Append -> Append -> ... -> Append -> Nil+  --+  , reverseTest "reverse right-nested appends" $ \sym ->+      buildSeq sym 250000 $ \s _ acc -> do+        singleton <- S.consSymSequence s True S.SymSequenceNil+        S.appendSymSequence s singleton acc++  -- Left-deep chain of Muxes (true branch grows):+  --+  --   Mux -> Mux -> Mux -> ... -> Mux -> Nil+  --+  , reverseTest "reverse left-deep mux chain" $ \sym ->+      buildSeq sym 250000 $ \s _ acc -> do+        singleton <- S.consSymSequence s True S.SymSequenceNil+        S.muxSymSequence s (WI.truePred s) acc singleton++  -- Right-deep chain of Muxes (true branch is a leaf):+  --+  --   Mux -> Mux -> Mux -> ... -> Mux -> Nil+  --+  , reverseTest "reverse right-deep mux chain" $ \sym ->+      buildSeq sym 250000 $ \s _ acc -> do+        singleton <- S.consSymSequence s True S.SymSequenceNil+        S.muxSymSequence s (WI.truePred s) singleton acc++  -- Balanced binary tree of Appends over singletons:+  --+  --            Append+  --           /      \+  --       Append    Append+  --       /    \    /    \+  --     [1]  [2]  [3]  [4] ...+  --+  , reverseTest "reverse balanced appends" $ \sym ->+      buildBalanced sym 250000 $ \s acc1 acc2 ->+        S.appendSymSequence s acc1 acc2++  -- Balanced binary tree of Muxes over singletons:+  --+  --            Mux+  --           /   \+  --        Mux    Mux+  --       /   \  /   \+  --     [1] [2] [3] [4] ...+  --+  , reverseTest "reverse balanced muxes" $ \sym ->+      buildBalanced sym 250000 $ \s acc1 acc2 ->+        S.muxSymSequence s (WI.truePred s) acc1 acc2+  ]++---------------------------------------------------------------------+-- Helpers++mkBackend :: IO (Some SomeBackend)+mkBackend = do+  sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState Nonce.globalNonceGenerator+  Some . SomeBackend <$> newSimpleBackend sym++-- | Build a sequence, reverse it, and check that length is preserved.+--   Must complete within 5 seconds.+reverseTest ::+  String ->+  (forall sym. WI.IsExprBuilder sym => sym -> IO (SymSequence sym Bool)) ->+  TT.TestTree+reverseTest name build = TTU.testCase name $ do+  Some (SomeBackend bak) <- mkBackend+  let sym = backendGetSym bak+  s <- build sym+  origLen <- S.lengthSymSequence sym s+  result <- timeout (5 * 1000000) $ do+    r <- S.reverseSymSequence sym s+    S.lengthSymSequence sym r+  case result of+    Nothing -> TTU.assertFailure (name ++ " timed out (>5s)")+    Just revLen ->+      TTU.assertEqual "length preserved"+        (WI.asInteger (WI.natToIntegerPure origLen))+        (WI.asInteger (WI.natToIntegerPure revLen))++-- | Iterate a step function n times starting from nil.+buildSeq ::+  WI.IsExprBuilder sym =>+  sym ->+  Int ->+  (sym -> Int -> SymSequence sym Bool -> IO (SymSequence sym Bool)) ->+  IO (SymSequence sym Bool)+buildSeq sym n step = go n S.SymSequenceNil+  where+    go 0 acc = pure acc+    go i acc = go (i - 1) =<< step sym i acc++-- | Build a balanced binary tree of n singletons combined with the given+--   binary operation (e.g. appendSymSequence or muxSymSequence).+buildBalanced ::+  WI.IsExprBuilder sym =>+  sym ->+  Int ->+  (sym -> SymSequence sym Bool -> SymSequence sym Bool -> IO (SymSequence sym Bool)) ->+  IO (SymSequence sym Bool)+buildBalanced sym n combine = do+  leaves <- mapM (\_ -> S.consSymSequence sym True S.SymSequenceNil) [1..n]+  reduce leaves+  where+    reduce [] = pure S.SymSequenceNil+    reduce [x] = pure x+    reduce xs = reduce =<< pairUp xs+    pairUp [] = pure []+    pairUp [x] = pure [x]+    pairUp (x:y:rest) = do+      combined <- combine sym x y+      (combined :) <$> pairUp rest