crucible 0.9 → 0.10

raw patch · 55 files changed

+1479/−1157 lines, 55 filesdep +microlensdep +microlens-mtldep +microlens-thdep −lensdep ~basedep ~parameterized-utilsdep ~th-abstractionPVP ok

version bump matches the API change (PVP)

Dependencies added: microlens, microlens-mtl, microlens-th

Dependencies removed: lens

Dependency ranges changed: base, parameterized-utils, th-abstraction

API changes (from Hackage documentation)

Files

• CHANGELOG.md +37/−0
• crucible.cabal +125/−14
• src/Lang/Crucible/Analysis/Fixpoint.hs +13/−10
• src/Lang/Crucible/Analysis/Fixpoint/Components.hs +2/−1
• src/Lang/Crucible/Analysis/ForwardDataflow.hs +0/−309
• src/Lang/Crucible/Analysis/Postdom.hs +12/−12
• src/Lang/Crucible/Analysis/Reachable.hs +3/−3
• src/Lang/Crucible/Backend.hs +15/−6
• src/Lang/Crucible/Backend/AssumptionStack.hs +1/−1
• src/Lang/Crucible/Backend/Assumptions.hs +3/−3
• src/Lang/Crucible/Backend/Online.hs +11/−6
• src/Lang/Crucible/Backend/Prove.hs +74/−24
• src/Lang/Crucible/Backend/Simple.hs +7/−1
• src/Lang/Crucible/CFG/Common.hs +4/−4
• src/Lang/Crucible/CFG/Core.hs +6/−6
• src/Lang/Crucible/CFG/EarlyMergeLoops.hs +4/−4
• src/Lang/Crucible/CFG/Expr.hs +18/−6
• src/Lang/Crucible/CFG/ExtractSubgraph.hs +9/−8
• src/Lang/Crucible/CFG/Generator.hs +24/−22
• src/Lang/Crucible/CFG/Reg.hs +7/−7
• src/Lang/Crucible/CFG/SSAConversion.hs +47/−47
• src/Lang/Crucible/Concretize.hs +3/−2
• src/Lang/Crucible/FunctionHandle.hs +1/−1
• src/Lang/Crucible/README.hs +1/−0
• src/Lang/Crucible/Simulator.hs +3/−0
• src/Lang/Crucible/Simulator/BoundedExec.hs +17/−18
• src/Lang/Crucible/Simulator/BoundedRecursion.hs +11/−11
• src/Lang/Crucible/Simulator/Breakpoint.hs +0/−109
• src/Lang/Crucible/Simulator/CallFrame.hs +30/−20
• src/Lang/Crucible/Simulator/Cut.hs +110/−0
• src/Lang/Crucible/Simulator/EvalStmt.hs +22/−19
• src/Lang/Crucible/Simulator/Evaluation.hs +7/−2
• src/Lang/Crucible/Simulator/ExecutionTree.hs +135/−50
• src/Lang/Crucible/Simulator/Operations.hs +39/−36
• src/Lang/Crucible/Simulator/OverrideSim.hs +10/−8
• src/Lang/Crucible/Simulator/PathSatisfiability.hs +3/−3
• src/Lang/Crucible/Simulator/PathSplitting.hs +3/−4
• src/Lang/Crucible/Simulator/PositionTracking.hs +2/−3
• src/Lang/Crucible/Simulator/Profiling.hs +14/−13
• src/Lang/Crucible/Simulator/RecordAndReplay.hs +26/−23
• src/Lang/Crucible/Simulator/SimError.hs +58/−15
• src/Lang/Crucible/Simulator/SymSequence.hs +36/−1
• src/Lang/Crucible/Syntax.hs +12/−10
• src/Lang/Crucible/Types.hs +2/−2
• src/Lang/Crucible/Utils/BitSet.hs +14/−13
• src/Lang/Crucible/Utils/CoreRewrite.hs +2/−2
• src/Lang/Crucible/Utils/MuxTree.hs +1/−2
• src/Lang/Crucible/Utils/Structural.hs +2/−1
• src/Lang/Crucible/Vector.hs +1/−1
• test/absint/Max.hs +1/−1
• test/absint/WTO.hs +3/−2
• test/helpers/Main.hs +1/−1
• test/helpers/SymSequence.hs +5/−290
• test/helpers/SymSequence/Properties.hs +308/−0
• test/helpers/SymSequence/Reverse.hs +174/−0

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

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crucible-Version:       0.9+Version:       0.10 Author:        Galois Inc. Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com Copyright:     (c) Galois, Inc 2014-2022@@ -34,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 @@ -48,7 +156,7 @@   import: bldflags   build-depends:     async,-    base >= 4.13 && < 4.21,+    base >= 4.13 && < 4.22,     bimap,     bv-sized >= 1.0.0 && < 1.1,     containers >= 0.5.9.0,@@ -56,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,@@ -81,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@@ -106,10 +215,10 @@     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@@ -170,12 +279,14 @@   hs-source-dirs: test/helpers   other-modules:     SymSequence+    SymSequence.Properties+    SymSequence.Reverse   main-is: Main.hs   build-depends: base,                  hspec >= 2.5,                  crucible,                  hedgehog,-                 lens,+                 microlens,                  panic >= 0.3,                  parameterized-utils,                  tasty >= 0.10,

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

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

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

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

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

@@ -85,13 +85,13 @@   ) 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) @@ -318,6 +318,12 @@   -- 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" @@ -375,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,@@ -385,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) @@ -424,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  @@ -496,7 +505,7 @@   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 ::

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

@@ -46,14 +46,14 @@   ) where  -import           Control.Lens (Traversal, folded) import           Data.Kind (Type) import qualified Data.Foldable as F-import           Data.Functor.Identity import           Data.Functor.Const+import           Data.Functor.Identity import qualified Data.Parameterized.TraversableF as TF-import qualified Data.Sequence as Seq import           Data.Sequence (Seq)+import qualified Data.Sequence as Seq+import           Lens.Micro (Traversal, folded) import qualified Prettyprinter as PP  import           What4.Expr.Builder

@@ -78,20 +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@@ -184,6 +183,8 @@     -- ^ action for checking if online features are currently enabled    , onlineExprBuilder :: B.ExprBuilder scope st fs++  , onlineExceptionContext :: !(Maybe ProgramStack)   }  newOnlineBackend ::@@ -209,6 +210,7 @@                    , currentFeatures = featref                    , onlineEnabled = getOpt enableOpt                    , onlineExprBuilder = sym+                   , onlineExceptionContext = Nothing                    }  -- | Do something with an online backend.@@ -433,6 +435,9 @@    getBackendState bak = readIORef (AS.proofObligations (assumptionStack bak)) +  getExceptionContext = onlineExceptionContext+  withExceptionContext bak ec = bak { onlineExceptionContext = Just ec }+ -------------------------------------------------------------------------------- -- Branch satisfiability @@ -450,7 +455,7 @@      -- | The context before considering the given predicate was already      --   unsatisfiable.    | UnsatisfiableContext-   deriving (Data, Eq, Generic, Ord, Typeable)+   deriving (Data, Eq, Generic, Ord)  considerSatisfiability ::   OnlineSolver solver =>

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

@@ -30,9 +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@@ -56,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)@@ -67,6 +69,7 @@      return SimpleBackend             { sbAssumptionStack = as             , sbExprBuilder = sym+            , sbExceptionContext = Nothing             }  instance HasSymInterface (B.ExprBuilder t st fs) (SimpleBackend t st fs) where@@ -114,3 +117,6 @@     AS.restoreAssumptionStack newstk (sbAssumptionStack bak)    getBackendState bak = readIORef (AS.proofObligations (sbAssumptionStack bak))++  withExceptionContext bak ec = bak { sbExceptionContext = Just ec }+  getExceptionContext = sbExceptionContext

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

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

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

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

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

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

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

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

@@ -667,10 +667,11 @@                 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.andPred sym p p')-              (W4I.truePred sym)+              (\p (Const p') -> W4I.orPred sym p p')+              (W4I.falsePred sym)               preds            frm <- CB.pushAssumptionFrame bak

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

@@ -1,6 +1,7 @@ {- | 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

@@ -87,11 +87,14 @@     -- ** SimContext record   , IsSymInterfaceProof   , SimContext(..)+  , ExceptionContextConfig(..)   , initSimContext   , ctxSymInterface   , functionBindings   , cruciblePersonality   , profilingMetrics+  , exceptionContextConfig+  , parseExceptionContextConfig      -- * SimState   , SimState

@@ -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@@ -236,7 +236,7 @@    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 + modifyStackState gvRef mkSt st f = do     currGv <- readIORef gvRef     let err = panic "modifyStackState" ["Global variable not initialized"]     let gv = fromMaybe err currGv@@ -253,16 +253,15 @@    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'))@@ -276,8 +275,8 @@    InitialState simctx globals ah ret cont ->      do let halloc = simHandleAllocator simctx         currGv <- readIORef gvRef-        ngv <- case currGv of -          Nothing -> do +        ngv <- case currGv of+          Nothing -> do             gv <- freshGlobalVar halloc (Text.pack "BoundedExecFrameData") knownRepr             writeIORef gvRef (Just gv)             pure gv

@@ -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@@ -109,26 +110,25 @@    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+     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 +          Just (x:xs) -> do             mb <- getRecursionBound h             let v = 1 + fromMaybe 0 (Map.lookup h x)             case mb of-              Just b | v > b -> do +              Just b | v > b -> do                 loc <- getCurrentProgramLoc sym                 let msg = ("reached maximum number of recursive calls to function " ++ show h ++ " (" ++ show b ++ ")")                 let simerr = SimError loc (ResourceExhausted msg)-                when generateSideConditions $ withBackend simCtx $ \bak ->+                when generateSideConditions $ withStateBackend st $ \bak ->                   addProofObligation bak (LabeledPred (falsePred sym) simerr)                 return (ExecutionFeatureNewState (AbortState (AssertionFailure simerr) st))-              _ -> do +              _ -> do                 let x'  = Map.insert h v x                 let st' = st & stateGlobals %~ insertGlobal gv (rebuildStack x' x xs)                 x' `seq` return (ExecutionFeatureModifiedState (mkSt st'))@@ -143,9 +143,9 @@     InitialState simctx globals ah ret cont ->      do let halloc = simHandleAllocator simctx-        currGv <- readIORef gvRef -        gv <- case currGv of -          Just gv -> pure 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)

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

@@ -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')@@ -323,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

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

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

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

@@ -116,12 +116,16 @@   , IsSymInterfaceProof   , SimContext(..)   , Metric(..)+  , ExceptionContextConfig(..)   , initSimContext   , withBackend+  , withStateBackend   , ctxSymInterface   , functionBindings   , cruciblePersonality   , profilingMetrics+  , exceptionContextConfig+  , parseExceptionContextConfig      -- * SimState   , SimState(..)@@ -143,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)@@ -174,6 +182,7 @@ 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  ------------------------------------------------------------------------@@ -197,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 })  @@ -285,13 +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))+     <$> h (SomeFrame (p ^. gpValue)) arFrames h (AbortedExit ec p) =   (\(SomeFrame f') -> AbortedExit ec (p & gpValue .~ f'))-     <$> h (SomeFrame (p^.gpValue))+     <$> h (SomeFrame (p ^. gpValue)) arFrames h (AbortedBranch predicate loc r s) =   AbortedBranch predicate loc <$> arFrames h r                               <*> arFrames h s@@ -303,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))@@ -424,16 +433,16 @@ 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 ::@@ -472,7 +481,7 @@  abortedGlobals ::   Monad f =>-  -- | How to handle 'AbortedBranch'.+  -- | How to handle branches (e.g., 'AbortedBranch', 'PartialRes').   --   -- Common options include concretizing the 'Pred' or returning a partial   -- result (e.g., 'Nothing').@@ -491,7 +500,7 @@ -- | Extract the 'SymGlobalState' from an 'ExecResult'. execResultGlobals ::   Monad f =>-  -- | How to handle 'AbortedBranch'.+  -- | How to handle branches (e.g., 'AbortedBranch', 'PartialRes').   --   -- Common options include concretizing the 'Pred' or returning a partial   -- result (e.g., 'Nothing').@@ -500,7 +509,13 @@   f (SymGlobalState sym) execResultGlobals handleBranch =   \case-    FinishedResult _ctx partial -> pure (partial ^. partialValue . gpGlobals)+    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@@ -508,7 +523,7 @@ -- | Extract the 'SymGlobalState' from an 'ExecState'. execStateGlobals ::   Monad f =>-  -- | How to handle 'AbortedBranch'.+  -- | How to handle branches (e.g., 'AbortedBranch', 'PartialRes').   --   -- Common options include concretizing the 'Pred' or returning a partial   -- result (e.g., 'Nothing').@@ -1153,7 +1168,7 @@ 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   ------------------------------------------------------------------------@@ -1265,6 +1280,24 @@     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@@ -1277,19 +1310,20 @@ --   - @ext@: language extension, see "Lang.Crucible.CFG.Extension" type SimContext :: Type -> Type -> Type -> Type data SimContext p sym ext-   = SimContext { _ctxBackend            :: !(SomeBackend sym)+   = 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 p sym ext-                , _functionBindings      :: !(FunctionBindings p 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))+                , _cruciblePersonality       :: !p+                , _profilingMetrics          :: !(Map Text (Metric p sym ext))+                , _exceptionContextConfig    :: ExceptionContextConfig                 }  -- | Create a new 'SimContext' with the given bindings.@@ -1304,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 ::@@ -1321,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)@@ -1361,6 +1415,9 @@ 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 @@ -1436,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.@@ -1483,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)+        ]

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

@@ -84,7 +84,6 @@   ) 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(..))@@ -92,17 +91,19 @@ import           Control.Monad.ST import           Control.Monad.State.Strict (StateT(..)) 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@@ -165,7 +166,7 @@           TotalRes e -> e           PartialRes _loc _pred ex _ar1 -> ex   Sim $ StateContT $ \_c s ->-    return $ ResultState $ AbortedResult (s^.stateContext) (AbortedExit ec gp)+    return $ ResultState $ AbortedResult (s ^. stateContext) (AbortedExit ec gp)  bindOverrideSim ::   OverrideSim p sym ext rtp args r a ->@@ -224,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) @@ -580,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.

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

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

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

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

@@ -20,6 +20,7 @@   replayTraceLength,   RecordedTrace,   getRecordedTrace,+  getConcreteRecordedTrace,   recordFeature,   replayFeature,   initialTrace,@@ -28,22 +29,23 @@ ) where  import Control.Exception qualified as X-import Control.Lens ((%~), (&), (^.))-import Control.Lens qualified as Lens import Data.Foldable qualified as F+import Data.Function ((&)) import Data.Kind (Type)-import Data.Text qualified as Text 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.Panic (panic) import Lang.Crucible.Simulator qualified as C import Lang.Crucible.Simulator.EvalStmt qualified as C import Lang.Crucible.Simulator.ExecutionTree qualified as C import Lang.Crucible.Simulator.GlobalState qualified as C import Lang.Crucible.Simulator.SymSequence qualified as CSSS import Lang.Crucible.Types qualified as CT+import 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 @@ -83,7 +85,7 @@     , _initialTrace :: (RecordedTrace sym)     }     -- ^ constructor intentionally not exported-Lens.makeLenses ''ReplayState+makeLenses ''ReplayState  -- | Constructor for 'RecordState' mkRecordState ::@@ -254,10 +256,22 @@     -- API, but it could be exported in the future if necessary.  -- | Obtain a 'RecordedTrace' after execution.------ This currently requires concretizing the trace, because there is no efficient--- reverse operation for 'CSSS.SymSequence'. getRecordedTrace ::+  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 ->@@ -265,26 +279,15 @@   -- | Evaluation for booleans, usually a 'What4.Expr.GroundEval.GroundEvalFn'   (W4.Pred sym -> IO Bool) ->   IO (RecordedTrace sym)-getRecordedTrace globals (RecordState g) sym evalBool = do+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 (evalStr sym) s+      concretized <- CSSS.concretizeSymSequence evalBool pure s       let reversed = Seq.reverse concretized-      symbolized <- mapM (W4.stringLit sym . W4.UnicodeLiteral) reversed-      CSSS.fromListSymSequence sym (F.toList symbolized)--    evalStr ::-      W4.IsExpr (W4.SymExpr sym) =>-      sym ->-      W4.SymString sym W4.Unicode ->-      IO Text.Text-    evalStr _sym s =-      case W4.asString s of-        Just (W4.UnicodeLiteral s') -> pure s'-        Nothing -> panic "getRecordedTrace" ["Non-literal trace element?"]+      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@@ -338,7 +341,7 @@             | stop -> badPath             | otherwise -> pure C.ExecutionFeatureNoChange           W4P.PE valid (expectedLoc, rest) ->-            C.withBackend (st ^. C.stateContext) $ \bak -> do+            C.withStateBackend st $ \bak -> do               let msg = "Trace must be valid"               CB.assert bak valid (C.AssertFailureSimError msg "") 

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

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

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

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

@@ -12,6 +12,7 @@ -- built on top of GHC-native Integers. ------------------------------------------------------------------------ module Lang.Crucible.Utils.BitSet+{-# DEPRECATED "This module is deprecated" #-} ( BitSet , getBits , empty@@ -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

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

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

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

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

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

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

@@ -2,9 +2,9 @@  module Main (main) where -import Control.Lens ((^.)) import Data.List (isInfixOf) import Data.Maybe (fromMaybe)+import Lens.Micro ((^.))  import Test.Hspec import Test.Tasty

@@ -1,300 +1,15 @@-{-# LANGUAGE EmptyDataDeriving #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-} {-# LANGUAGE ImportQualifiedPost #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}  module SymSequence (tests) where -import Control.Monad.IO.Class (liftIO)-import Data.Foldable qualified as F-import Data.List qualified as List-import Data.Maybe qualified as Maybe-import Data.Parameterized.Nonce qualified as Nonce-import Data.Parameterized.Some (Some(Some))-import Hedgehog (Gen)-import Hedgehog qualified as H-import Hedgehog.Gen qualified as Gen-import Hedgehog.Range qualified as Range-import Lang.Crucible.Backend (SomeBackend(SomeBackend), backendGetSym)-import Lang.Crucible.Backend.Simple (newSimpleBackend)-import Lang.Crucible.Simulator.SymSequence (SymSequence)-import Lang.Crucible.Simulator.SymSequence qualified as S import Test.Tasty qualified as TT-import Test.Tasty.Hedgehog qualified as TTH-import What4.Expr (EmptyExprBuilderState(EmptyExprBuilderState))-import What4.Expr.Builder (newExprBuilder)-import What4.FloatMode (FloatModeRepr(FloatIEEERepr))-import What4.Interface qualified as WI-import What4.Partial qualified as WP ------------------------------------------------------------------------- Tests+import SymSequence.Properties qualified as Properties+import SymSequence.Reverse qualified as Reverse  tests :: TT.TestTree tests =-  TTH.testProperty-    "propSame"-    -- This is a big API, so we want adequate coverage (default is 100)-    (H.withTests 4096 propSame)---- | Check that a generated API interaction has the same effect when interpreted--- with either 'SymSequence' or lists.-propSame :: H.Property-propSame =-  H.property $ do-    Some (SomeBackend bak) <- liftIO mkBackend-    let sym = backendGetSym bak-    op <- H.forAll (Gen.sized $ \n -> genList (H.unSize n) Gen.bool)-    let l = opList op-    s <- liftIO (opSeq sym op)-    l' <- liftIO (F.toList <$> asSeq sym s)-    l H.=== l'-  where-    asSeq sym =-      S.concretizeSymSequence (pure . asConstPred (Just sym)) pure-------------------------------------------------------------------------- Helpers--mkBackend :: IO (Some SomeBackend)-mkBackend = do-  sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState Nonce.globalNonceGenerator-  Some . SomeBackend <$> newSimpleBackend sym---- Requires that the predicate is concrete-asConstPred ::-  WI.IsExprBuilder sym =>-  proxy sym ->-  WI.Pred sym ->-  Bool-asConstPred _proxy p =-  case WI.asConstantPred p of-    Just True -> True-    Just False -> False-    Nothing -> error "non-constant predicate?"-------------------------------------------------------------------------- Op--data Elem a deriving Show--data List a deriving Show---- TODO: Replace with `Seq` for performance-type family AsList t where-  AsList (List a) = [a]-  AsList (Elem a) = a-  AsList (Maybe a) = Maybe (AsList a)-  AsList (a, b) = (AsList a, AsList b)-  AsList a = a--type family AsSeq sym t where-  AsSeq sym (List a) = SymSequence sym a-  AsSeq sym (Elem a) = a-  AsSeq sym (Maybe a) = Maybe (AsSeq sym a)-  AsSeq sym (a, b) = (AsSeq sym a, AsSeq sym b)-  AsSeq sym a = a---- | An interaction with the 'SymSequence' API-data Op a t where-  -- Generic functions-  OTrue :: Op a Bool-  OFalse :: Op a Bool-  OFst :: Op a (l, r) -> Op a l-  OSnd :: Op a (l, r) -> Op a r-  OElem :: a -> Op a (Elem a)-  OFromMaybe :: Op a t -> Op a (Maybe t) -> Op a t--  -- Constructors-  ONil :: Op a (List a)-  OCons :: Op a (Elem a) -> Op a (List a) -> Op a (List a)-  OAppend :: Op a (List a) -> Op a (List a) -> Op a (List a)-  OMux :: Op a Bool -> Op a (List a) -> Op a (List a) -> Op a (List a)--  -- Operations-  OUncons :: Op a (List a) -> Op a (Maybe (Elem a), (List a))-  OLength :: Op a (List a) -> Op a Integer-  -- TODO: isNil, head, tail--sexp :: [String] -> String-sexp s = '(' : (unwords s ++ ")")--fun :: String -> [String] -> String-fun f s = sexp (f:s)--fun1 :: Show a => String -> a -> String-fun1 f a = fun f [show a]--fun2 :: (Show a, Show b) => String -> a -> b -> String-fun2 f a b = fun f [show a, show b]--fun3 :: (Show a, Show b, Show c) => String -> a -> b -> c -> String-fun3 f a b c = fun f [show a, show b, show c]--instance Show a => Show (Op a t) where-  show =-    \case-      -- Generic functions-      OTrue -> "true"-      OFalse -> "false"-      OFst t -> fun1 "fst" t-      OSnd t -> fun1 "snd" t-      OElem a -> show a-      OFromMaybe a m -> fun2 "fromMaybe" a m--      -- Constructors-      ONil -> "nil"-      OCons l r -> fun2 "cons" l r-      OAppend l r -> fun2 "append" l r-      OMux b l r -> fun3 "mux" b l r--      -- Operations-      OUncons l -> fun1 "uncons" l-      OLength l -> fun1 "length" l-------------------------------------------------------------------------- Generating Op--genBool :: Gen (Op a Bool)-genBool =-  Gen.choice-  [ pure OTrue-  , pure OFalse+  TT.testGroup "SymSequence"+  [ Properties.tests+  , Reverse.tests   ]--genElem ::-  Int ->-  Gen a ->-  Gen (Op a (Elem a))-genElem sz genA =-  if sz <= 0-  then OElem <$> genA-  else-    Gen.choice-    [ OElem <$> genA-    , OFromMaybe-      <$> genElem (sz - 1) genA-      <*> (OFst <$> (OUncons <$> genList (sz - 1) genA))-    ]--genList ::-  Int ->-  Gen a ->-  Gen (Op a (List a))-genList sz genA =-  if sz <= 0-  then pure ONil-  else-    Gen.choice-    [ genCons-    , genAppend-    , genMux-    ]-  where-    sub1 = genList (sz - 1) genA-    sub2 = do-      let budget = max 0 (sz - 1)-      bl <- Gen.integral (Range.linear 0 budget)-      let br = max 0 (budget - bl)-      l <- genList bl genA-      r <- genList br genA-      pure (l, r)--    genCons = OCons <$> genElem (sz - 1) genA <*> sub1--    genAppend = uncurry OAppend <$> sub2--    genMux = do-      b <- genBool-      uncurry (OMux b) <$> sub2-------------------------------------------------------------------------- Interpreting Op--opList :: Op a t -> AsList t-opList =-  \case-    -- Generic functions-    OTrue -> True-    OFalse -> False-    OFst t -> fst (opList t)-    OSnd t -> snd (opList t)-    OElem a -> a-    OFromMaybe a m -> Maybe.fromMaybe (opList a) (opList m)--    -- Constructors-    ONil -> []-    OCons a l -> opList a : opList l-    OAppend l r -> opList l ++ opList r-    OMux b l r -> if opList b then opList l else opList r--    -- Operations-    OUncons l ->-      let l' = opList l in-      case List.uncons l' of-        Just (hd, tl) -> (Just hd, tl)-        Nothing -> (Nothing, l')-    OLength l -> fromIntegral @Int @Integer (length (opList l))  -- safe--opSeq ::-  WI.IsExprBuilder sym =>-  sym ->-  Op a t ->-  IO (AsSeq sym t)-opSeq sym =-  \case-    -- Generic functions-    OTrue -> pure True-    OFalse -> pure False-    OFst t -> fst <$> opSeq sym t-    OSnd t -> snd <$> opSeq sym t-    OElem a -> pure a-    OFromMaybe a m ->-      Maybe.fromMaybe-      <$> opSeq sym a-      <*> opSeq sym m--    -- Constructors-    ONil -> pure S.SymSequenceNil-    OCons a l ->-      S.SymSequenceCons-      <$> Nonce.freshNonce Nonce.globalNonceGenerator-      <*> opSeq sym a-      <*> opSeq sym l-    OAppend l r ->-      S.SymSequenceAppend-      <$> Nonce.freshNonce Nonce.globalNonceGenerator-      <*> opSeq sym l-      <*> opSeq sym r-    OMux b l r -> do-      b' <- opSeq sym b-      let b'' = if b' then WI.truePred sym else WI.falsePred sym-      S.SymSequenceMerge-        <$> Nonce.freshNonce Nonce.globalNonceGenerator-        <*> pure b''-        <*> opSeq sym l-        <*> opSeq sym r--    -- Operations-    OUncons l -> do-      l' <- opSeq sym l-      let interpPred p x y =-            if asConstPred (Just sym) p-            then pure x-            else pure y-      pe <- S.unconsSymSequence sym interpPred l'-      case pe of-        WP.Unassigned -> pure (Nothing, l')-        WP.PE _ (hd, tl) -> -- TODO: assert pred is truePred-          pure (Just hd, tl)-    OLength s -> do-      l <- S.lengthSymSequence sym =<< opSeq sym s-      case WI.asInteger (WI.natToIntegerPure l) of-        Just l' -> pure l'-        Nothing -> error "SymSequence: symbolic length"

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

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