diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,59 @@ +# 0.10 -- 2026-09-10 + +* Add support for GHC 9.12 (at 9.12.2) and bump from 9.10.1 to 9.10.3. +* Fix `uniquelyConcRegMap` blocking clause: use disjunction (OR) instead of + conjunction (AND). The old code would falsely report a `RegMap` as uniquely + concretized whenever any single component was unique, even if other components + had multiple possible values. +* **BREAKING:** Rename various bits associated with the "breakpoint" + feature in accordance with renaming the feature to "cut" or + "cutpoint". + Exported Haskell symbols renamed: + - `Lang.Crucible.Simulator.Breakpoint` -> `Lang.Crucible.Simulator.Cut` + - `BreakpointName` -> `CutpointName` + - `Breakpoint` -> `Cut` + - `addBreakpointStmt` -> `addCutStmt` + - `breakAndReturn` -> `cutAndReturn` + - `breakpointPostdomInfo` -> `cutpointPostdomInfo` + - `cfgBreakpoints` -> `cfgCutpoints` + - `setFrameBreakpointPostdomInfo` -> `setFrameCutpointPostdomInfo` +* Add `reverseSymSequence` to `Lang.Crucible.Simulator.SymSequence` +* **BREAKING:** Add `FloatRound` constructor tp `App` in + `Lang.Crucible.CFG.Expr` for rounding floating-point values to the nearest + representable integral value. +* **BREAKING:** Add `SequenceReverse` constructor to `App` in + `Lang.Crucible.CFG.Expr` for reversing symbolic sequences. +* **BREAKING:** Change the signature of `getRecordedTrace` in + `Lang.Crucible.Simulator.RecordAndReplay` to remove the `evalBool` parameter, + as the implementation no longer concretizes the trace. +* Add `Lang.Crucible.Simulator.RecordAndReplay.getConcreteRecordedTrace` for + performant trace reversal when concretization is desired. +* Add `withStateBackend` and additional infrastructure for including stack + traces in `SimError` and `IsSymBackend` +* Fix `onlineProve` to properly negate goals before checking satisfiability +* Avoid sending trivially-true goals to the solver in `Backend.Prove`. +* Fix bug in `execResultGlobals` that caused it to erroneously always return the + non-aborted branch of a `FinishedResult ... (PartialRes ...)`. + +# 0.9 -- 2026-01-29 + +# 0.8.0 -- 2025-11-09 + +* Add `setExecResultContext`, `setExecStateContext` +* Add `Lang.Crucible.Simulator.RecordAndReplay`, a module with two new execution + features for recording and replaying control-flow traces. +* Add a `GlobalPair` argument to `AbortedExit`. +* Add new helpers for extracting `SymGlobalState`s: `exec{Result,State}Globals`. +* Add `typedOverride` for constructing `TypedOverride`s with statically-known + signatures. +* Add `bindTypedOverride` for binding `TypedOverride`s to `FnHandle`s. +* Add `FunctorF`, `FoldableF`, and `TraversableF` instances for `CrucibleEvent`, + `CrucibleAssumption`, and `CrucibleAssumptions`. +* Add `gcAddTopLevelAssume`, for making top-level assumptions. +* Rename functions in `Lang.Crucible.Concretize` to match What4's conventions. + In particular, rename `concRegValue` to `groundRegValue`, `concRegEntry` to + `groundRegEntry`, and `concRegMap` to `groundRegMap`. + # 0.7.2 -- 2025-03-21 * Add support for Bitwuzla as an online SMT solver backend. diff --git a/crucible.cabal b/crucible.cabal --- a/crucible.cabal +++ b/crucible.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: crucible -Version: 0.7.2 +Version: 0.10 Author: Galois Inc. Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com Copyright: (c) Galois, Inc 2014-2022 @@ -14,6 +14,9 @@ (SSA) form control flow graphs, and a symbolic simulation engine for executing programs expressed in this format. It also provides support for communicating with a variety of SAT and SMT solvers, including Z3, CVC4, Yices, STP, and dReal. + . + For an overview of Crucible please have a look at "Lang.Crucible.README" + extra-doc-files: CHANGELOG.md source-repository head @@ -31,12 +34,120 @@ Default: True common bldflags - ghc-options: -Wall - -Werror=incomplete-patterns - -Werror=missing-methods - -Werror=overlapping-patterns - -Wpartial-fields - -Wincomplete-uni-patterns + -- Note [Export lists] + -- ------------------- + -- + -- We don't allow modules without export lists. + -- + -- From the GHC docs: + -- + -- Declaring an explicit export list [...] enables GHC dead code analysis, + -- prevents accidental export of names and can ease optimizations like + -- inlining. + -- + -- It also makes it easier to organize the Haddocks using section headers, and + -- allows for internal/hidden definitions and constructors. + -- + -- We can't use -Werror=missing-export-lists here because it interferes with + -- ghcid. However, we enable it in CI, see ../cabal.project.ci. + ghc-options: + -Wmissing-export-lists + + -- Specifying -Wall and -Werror can cause the project to fail to build on + -- newer versions of GHC simply due to new warnings being added to -Wall. To + -- prevent this from happening we manually list which warnings should be + -- considered errors. We also list some warnings that are not in -Wall, though + -- try to avoid "opinionated" warnings (though this judgement is clearly + -- subjective). + -- + -- Warnings are grouped by the GHC version that introduced them, and then + -- alphabetically. + -- + -- A list of warnings and the GHC version in which they were introduced is + -- available here: + -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html + + -- Since GHC 9.6 or earlier: + ghc-options: + -Wall + -Werror=ambiguous-fields + -Werror=deferred-type-errors + -Werror=deprecated-flags + -Werror=deprecations + -Werror=deriving-defaults + -Werror=deriving-typeable + -Werror=dodgy-foreign-imports + -Werror=duplicate-exports + -Werror=empty-enumerations + -Werror=gadt-mono-local-binds + -Werror=identities + -Werror=inaccessible-code + -Werror=incomplete-patterns + -Werror=incomplete-record-updates + -Werror=incomplete-uni-patterns + -Werror=inline-rule-shadowing + -Werror=misplaced-pragmas + -Werror=missed-extra-shared-lib + -Werror=missing-exported-signatures + -Werror=missing-fields + -Werror=missing-home-modules + -Werror=missing-methods + -Werror=missing-pattern-synonym-signatures + -Werror=missing-signatures + -Werror=name-shadowing + -Werror=noncanonical-monad-instances + -Werror=noncanonical-monoid-instances + -Werror=operator-whitespace + -Werror=operator-whitespace-ext-conflict + -Werror=orphans + -Werror=overflowed-literals + -Werror=overlapping-patterns + -Werror=partial-fields + -Werror=partial-type-signatures + -Werror=redundant-bang-patterns + -Werror=redundant-record-wildcards + -Werror=redundant-strictness-flags + -Werror=simplifiable-class-constraints + -Werror=star-binder + -Werror=star-is-type + -Werror=tabs + -Werror=type-defaults + -Werror=typed-holes + -Werror=type-equality-out-of-scope + -Werror=type-equality-requires-operators + -Werror=unicode-bidirectional-format-characters + -Werror=unrecognised-pragmas + -Werror=unrecognised-warning-flags + -Werror=unsupported-calling-conventions + -Werror=unsupported-llvm-version + -Werror=unused-do-bind + -Werror=unused-imports + -Werror=unused-record-wildcards + -Werror=warnings-deprecations + -Werror=wrong-do-bind + + if impl(ghc < 9.8) + ghc-options: + -Werror=forall-identifier + + if impl(ghc >= 9.8) + ghc-options: + -Werror=incomplete-export-warnings + -Werror=inconsistent-flags + + if impl(ghc >= 9.10) + ghc-options: + -Werror=badly-staged-types + -Werror=data-kinds-tc + -Werror=incomplete-record-selectors + + if impl(ghc < 9.12) + ghc-options: + -Werror=compat-unqualified-imports + + -- TODO(#1308): Enable and fix this warning when GHC 9.6 is dropped from CI + -- -Werror=deprecated-type-abstractions + ghc-prof-options: -O2 -fprof-auto-exported default-language: Haskell2010 @@ -45,7 +156,7 @@ import: bldflags build-depends: async, - base >= 4.13 && < 4.20, + base >= 4.13 && < 4.22, bimap, bv-sized >= 1.0.0 && < 1.1, containers >= 0.5.9.0, @@ -53,15 +164,17 @@ fgl, hashable, json >= 0.9 && < 1.0, - lens, + microlens >= 0.5, + microlens-mtl, + microlens-th, mtl, panic >= 0.3, - parameterized-utils >= 1.0.8 && < 2.2, + parameterized-utils >= 2.3 && < 2.4, prettyprinter >= 1.7.0, template-haskell, text, time >= 1.8 && < 2.0, - th-abstraction >=0.1 && <0.7, + th-abstraction >=0.1 && <0.8, transformers, unordered-containers, vector, @@ -78,7 +191,6 @@ exposed-modules: Lang.Crucible.Analysis.DFS - Lang.Crucible.Analysis.ForwardDataflow Lang.Crucible.Analysis.Fixpoint Lang.Crucible.Analysis.Fixpoint.Components Lang.Crucible.Analysis.Postdom @@ -101,11 +213,12 @@ Lang.Crucible.CFG.SSAConversion Lang.Crucible.CFG.EarlyMergeLoops Lang.Crucible.FunctionHandle + Lang.Crucible.README Lang.Crucible.Simulator - Lang.Crucible.Simulator.Breakpoint Lang.Crucible.Simulator.BoundedExec Lang.Crucible.Simulator.BoundedRecursion Lang.Crucible.Simulator.CallFrame + Lang.Crucible.Simulator.Cut Lang.Crucible.Simulator.Evaluation Lang.Crucible.Simulator.EvalStmt Lang.Crucible.Simulator.ExecutionTree @@ -117,6 +230,7 @@ Lang.Crucible.Simulator.PathSplitting Lang.Crucible.Simulator.PositionTracking Lang.Crucible.Simulator.Profiling + Lang.Crucible.Simulator.RecordAndReplay Lang.Crucible.Simulator.RegMap Lang.Crucible.Simulator.RegValue Lang.Crucible.Simulator.SimError @@ -163,15 +277,20 @@ import: bldflags type: exitcode-stdio-1.0 hs-source-dirs: test/helpers --- other-modules: + other-modules: + SymSequence + SymSequence.Properties + SymSequence.Reverse main-is: Main.hs build-depends: base, hspec >= 2.5, crucible, - lens, + hedgehog, + microlens, panic >= 0.3, parameterized-utils, tasty >= 0.10, tasty-hspec >= 1.1, + tasty-hedgehog >= 1.2, tasty-hunit, what4 diff --git a/src/Lang/Crucible/Analysis/Fixpoint.hs b/src/Lang/Crucible/Analysis/Fixpoint.hs --- a/src/Lang/Crucible/Analysis/Fixpoint.hs +++ b/src/Lang/Crucible/Analysis/Fixpoint.hs @@ -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' diff --git a/src/Lang/Crucible/Analysis/Fixpoint/Components.hs b/src/Lang/Crucible/Analysis/Fixpoint/Components.hs --- a/src/Lang/Crucible/Analysis/Fixpoint/Components.hs +++ b/src/Lang/Crucible/Analysis/Fixpoint/Components.hs @@ -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. diff --git a/src/Lang/Crucible/Analysis/ForwardDataflow.hs b/src/Lang/Crucible/Analysis/ForwardDataflow.hs deleted file mode 100644 --- a/src/Lang/Crucible/Analysis/ForwardDataflow.hs +++ /dev/null @@ -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 --- 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' diff --git a/src/Lang/Crucible/Analysis/Postdom.hs b/src/Lang/Crucible/Analysis/Postdom.hs --- a/src/Lang/Crucible/Analysis/Postdom.hs +++ b/src/Lang/Crucible/Analysis/Postdom.hs @@ -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 = diff --git a/src/Lang/Crucible/Analysis/Reachable.hs b/src/Lang/Crucible/Analysis/Reachable.hs --- a/src/Lang/Crucible/Analysis/Reachable.hs +++ b/src/Lang/Crucible/Analysis/Reachable.hs @@ -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 diff --git a/src/Lang/Crucible/Backend.hs b/src/Lang/Crucible/Backend.hs --- a/src/Lang/Crucible/Backend.hs +++ b/src/Lang/Crucible/Backend.hs @@ -4,8 +4,8 @@ License : BSD3 Maintainer : Joe Hendrix -This module provides an interface that symbolic backends must provide -for interacting with the symbolic simulator. +This module provides the interface that the symbolic simulator uses when +interacting with symbolic backends (i.e., SMT solvers). Compared to the solver connections provided by What4, Crucible backends provide a facility for managing an /assumption stack/ (see 'AS.AssumptionStack'). Note @@ -81,16 +81,17 @@ , ppProofObligation , backendOptions , assertThenAssumeConfigOption + , ppAssumptionState ) where import Control.Exception(Exception(..), throwIO) -import Control.Lens ((^.)) import Control.Monad import Control.Monad.IO.Class import Data.Foldable (toList) import Data.Set (Set) -import qualified Prettyprinter as PP import GHC.Stack +import Lens.Micro ((^.)) +import qualified Prettyprinter as PP import Data.Parameterized.Map (MapF) @@ -110,6 +111,7 @@ import qualified Lang.Crucible.Backend.AssumptionStack as AS import qualified Lang.Crucible.Backend.ProofGoals as PG import Lang.Crucible.Simulator.SimError +import Lang.Crucible.Backend.ProofGoals (ppGoalCollector) type Assertion sym = LabeledPred (Pred sym) SimError type ProofObligation sym = AS.ProofGoal (Assumptions sym) (Assertion sym) @@ -311,6 +313,17 @@ resetAssumptionState :: bak -> IO () resetAssumptionState bak = restoreAssumptionState bak PG.emptyGoalCollector + -- | Get the state of the backend + -- + -- In contrast to 'saveAssumptionState', this also includes the goals. + getBackendState :: bak -> IO (AssumptionState sym) + + -- | An additional exception context for more detailed SimErrors + getExceptionContext :: bak -> Maybe ProgramStack + + -- | Make a backend just like this but with a different error context + withExceptionContext :: bak -> ProgramStack -> bak + assertThenAssumeConfigOption :: ConfigOption BaseBoolType assertThenAssumeConfigOption = configOption knownRepr "assertThenAssume" @@ -368,7 +381,8 @@ assert bak p msg = do let sym = backendGetSym bak loc <- getCurrentProgramLoc sym - addAssertion bak (LabeledPred p (SimError loc msg)) + let ctx = getExceptionContext bak + addAssertion bak (LabeledPred p (mkSimError loc msg ctx)) -- | Add a proof obligation for False. This always aborts execution -- of the current path, because after asserting false, we get to assume it, @@ -378,7 +392,8 @@ addFailedAssertion bak msg = do let sym = backendGetSym bak loc <- getCurrentProgramLoc sym - let err = SimError loc msg + let ctx = getExceptionContext bak + let err = mkSimError loc msg ctx addProofObligation bak (LabeledPred (falsePred sym) err) abortExecBecause (AssertionFailure err) @@ -417,7 +432,8 @@ readPartExpr bak (PE p v) msg = do let sym = backendGetSym bak loc <- getCurrentProgramLoc sym - addAssertion bak (LabeledPred p (SimError loc msg)) + let ctx = getExceptionContext bak + addAssertion bak (LabeledPred p (mkSimError loc msg ctx)) return v @@ -489,4 +505,22 @@ ppGl = PP.indent 2 $ - PP.vsep [ppSimError (gl^.labeledPredMsg), printSymExpr (gl^.labeledPred)] + PP.vsep [ppSimError (gl ^. labeledPredMsg), printSymExpr (gl ^. labeledPred)] + +-- | Pretty-printer for 'AssumptionState'. +ppAssumptionState :: + IsExpr (SymExpr sym) => + proxy sym -> + AssumptionState sym -> + PP.Doc ann +ppAssumptionState _proxy = ppGoalCollector ppAssumptions ppPred + where + ppPred (LabeledPred p simErr) = + PP.vcat + [ "Labeled predicate:" + , PP.indent 2 $ + PP.vcat + [ printSymExpr p + , ppSimError simErr + ] + ] diff --git a/src/Lang/Crucible/Backend/AssumptionStack.hs b/src/Lang/Crucible/Backend/AssumptionStack.hs --- a/src/Lang/Crucible/Backend/AssumptionStack.hs +++ b/src/Lang/Crucible/Backend/AssumptionStack.hs @@ -4,17 +4,16 @@ License : BSD3 Maintainer : Rob Dockins -This module provides management support for keeping track -of a context of logical assumptions. The API provided here -is similar to the interactive mode of an SMT solver. Logical -conditions can be assumed into the current context, and bundles -of assumptions are organized into frames which are pushed and -popped by the user to manage the state. +This module provides management support for keeping track of a context of +logical assumptions and proof obligations that arise from symbolic simulation. +The API provided here is similar to the interactive mode of an SMT solver. +Logical conditions can be assumed into the current context, and conjunctions +of assumptions are organized into frames which are pushed and popped by the +simulator to manage the state. -Additionally, proof goals can be asserted to the system. These will be -turned into complete logical statements by assuming the current context -and be stashed in a collection of remembered goals for later dispatch to -solvers. +Additionally, proof goals can be asserted to the system. These will be turned +into complete logical statements by assuming the current context and will be +stashed in a collection of remembered goals for later dispatch to SMT solvers. -} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} @@ -70,11 +69,13 @@ , assumeFrameCond :: asmp } --- | An assumption stack is a data structure for tracking --- logical assumptions and proof obligations. Assumptions --- can be added to the current stack frame, and stack frames --- may be pushed (to remember a previous state) or popped --- to restore a previous state. +-- | An assumption stack is a data structure for tracking logical assumptions +-- and proof obligations that arise from symbolic simulation. Assumptions +-- can be added to the current stack frame, and stack frames may be pushed (to +-- remember a previous state) or popped (to restore a previous state). +-- +-- The main use of 'AssumptionStack' is as the state of the simple or online +-- backends. data AssumptionStack asmp ast = AssumptionStack { assumeStackGen :: IO FrameIdentifier @@ -175,7 +176,7 @@ case gcPop gc of Left (ident', _assumes, mg, gc1) | ident == ident' -> (gc',n) - | otherwise -> go (n+1) gc' + | otherwise -> go (n + 1) gc' where gc' = case mg of Nothing -> gc1 Just g -> gcAddGoals g gc1 diff --git a/src/Lang/Crucible/Backend/Assumptions.hs b/src/Lang/Crucible/Backend/Assumptions.hs --- a/src/Lang/Crucible/Backend/Assumptions.hs +++ b/src/Lang/Crucible/Backend/Assumptions.hs @@ -41,15 +41,19 @@ , assumptionsPred , flattenAssumptions , assumptionsTopLevelLocs + , ppAssumptions' + , ppAssumptions ) where -import Control.Lens (Traversal, folded) import Data.Kind (Type) -import Data.Functor.Identity +import qualified Data.Foldable as F import Data.Functor.Const -import qualified Data.Sequence as Seq +import Data.Functor.Identity +import qualified Data.Parameterized.TraversableF as TF import Data.Sequence (Seq) +import qualified Data.Sequence as Seq +import Lens.Micro (Traversal, folded) import qualified Prettyprinter as PP import What4.Expr.Builder @@ -76,6 +80,13 @@ -- ^ An assumption justified by a proof of the impossibility of -- a certain simulator error. +instance TF.FunctorF CrucibleAssumption where + fmapF = TF.fmapFDefault +instance TF.FoldableF CrucibleAssumption where + foldMapF = TF.foldMapFDefault +instance TF.TraversableF CrucibleAssumption where + traverseF = traverseAssumption + -- | This type describes events we can track during program execution. data CrucibleEvent (e :: BaseType -> Type) where -- | This event describes the creation of a symbolic variable. @@ -91,13 +102,24 @@ ProgramLoc -> CrucibleEvent e +instance TF.FunctorF CrucibleEvent where + fmapF = TF.fmapFDefault +instance TF.FoldableF CrucibleEvent where + foldMapF = TF.foldMapFDefault +instance TF.TraversableF CrucibleEvent where + traverseF = traverseEvent + -- | Pretty print an event -ppEvent :: IsExpr e => CrucibleEvent e -> PP.Doc ann -ppEvent (CreateVariableEvent loc nm _tpr v) = - "create var" PP.<+> PP.pretty nm PP.<+> "=" PP.<+> printSymExpr v PP.<+> "at" PP.<+> PP.pretty (plSourceLoc loc) -ppEvent (LocationReachedEvent loc) = +ppEvent' :: (forall t. e t -> PP.Doc ann) -> CrucibleEvent e -> PP.Doc ann +ppEvent' ppExp (CreateVariableEvent loc nm _tpr v) = + "create var" PP.<+> PP.pretty nm PP.<+> "=" PP.<+> ppExp v PP.<+> "at" PP.<+> PP.pretty (plSourceLoc loc) +ppEvent' _ppExp (LocationReachedEvent loc) = "reached" PP.<+> PP.pretty (plSourceLoc loc) PP.<+> "in" PP.<+> PP.pretty (plFunction loc) +-- | Pretty print an event +ppEvent :: IsExpr e => CrucibleEvent e -> PP.Doc ann +ppEvent = ppEvent' printSymExpr + -- | Return the program location associated with an event eventLoc :: CrucibleEvent e -> ProgramLoc eventLoc (CreateVariableEvent loc _ _ _) = loc @@ -152,6 +174,21 @@ instance Monoid (CrucibleAssumptions e) where mempty = ManyAssumptions mempty +instance TF.FunctorF CrucibleAssumptions where + fmapF = TF.fmapFDefault +instance TF.FoldableF CrucibleAssumptions where + foldMapF = TF.foldMapFDefault +instance TF.TraversableF CrucibleAssumptions where + traverseF f = \case + SingleAssumption a -> + SingleAssumption <$> TF.traverseF f a + SingleEvent e -> + SingleEvent <$> TF.traverseF f e + ManyAssumptions xs -> + ManyAssumptions <$> traverse (TF.traverseF f) xs + MergeAssumptions c xs ys -> + MergeAssumptions <$> f c <*> TF.traverseF f xs <*> TF.traverseF f ys + singleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e singleAssumption x = SingleAssumption x @@ -239,6 +276,8 @@ ppAssumption :: (forall tp. e tp -> PP.Doc ann) -> CrucibleAssumption e -> PP.Doc ann ppAssumption ppDoc e = + -- TODO(lb): These should really all be `align`ed, but that breaks a bunch + -- of tests. case e of GenericAssumption l msg p -> PP.vsep [ ppLocated l (PP.pretty msg) @@ -266,3 +305,27 @@ ppLoc :: ProgramLoc -> PP.Doc ann ppLoc l = PP.pretty (plSourceLoc l) + +-- | Pretty-print 'CrucibleAssumptions'. +ppAssumptions' :: + -- | How to print expressions. If @'IsExpr' e@ holds, then see 'ppAssumptions' + -- for a version that uses 'printSymExpr'. + (forall tp. e tp -> PP.Doc ann) -> + CrucibleAssumptions e -> + PP.Doc ann +ppAssumptions' ppExp = + \case + SingleAssumption asmp -> ppAssumption ppExp asmp + SingleEvent e -> ppEvent' ppExp e + ManyAssumptions asmps -> PP.list (map (ppAssumptions' ppExp) (F.toList asmps)) + MergeAssumptions b thn els -> + PP.align $ + PP.vcat + [ "if " <> PP.align (ppExp b) + , "then " <> PP.align (ppAssumptions' ppExp thn) + , "else " <> PP.align (ppAssumptions' ppExp els) + ] + +-- | @'ppAssumptions' = `ppAssumptions'` 'printSymExpr'@ +ppAssumptions :: IsExpr e => CrucibleAssumptions e -> PP.Doc ann +ppAssumptions = ppAssumptions' printSymExpr diff --git a/src/Lang/Crucible/Backend/Goals.hs b/src/Lang/Crucible/Backend/Goals.hs --- a/src/Lang/Crucible/Backend/Goals.hs +++ b/src/Lang/Crucible/Backend/Goals.hs @@ -7,12 +7,14 @@ proof obligations, and the current state of assumptions. -} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TupleSections #-} module Lang.Crucible.Backend.Goals ( ProofGoal(..) , Goals(..) + , ppGoals , goalsToList , assuming , proveAll @@ -29,6 +31,7 @@ import Data.Functor.Const (Const(..)) import Data.Sequence (Seq) import qualified Data.Sequence as Seq +import qualified Prettyprinter as PP -- | A proof goal consists of a collection of assumptions -- that were in scope when an assertion was made, together @@ -52,6 +55,35 @@ -- | A conjunction of two goals. | ProveConj !(Goals asmp goal) !(Goals asmp goal) deriving Show + +-- | Intended for debugging, this is not generally a user-facing datatype. +ppGoals :: + (asmp -> PP.Doc ann) -> + (goal -> PP.Doc ann) -> + Goals asmp goal -> + PP.Doc ann +ppGoals ppAsmp ppGoal = + \case + Assuming asmp gls -> + PP.align $ + PP.vcat + [ PP.pretty "Assuming:" + , PP.indent 2 (ppAsmp asmp) + , PP.pretty "Prove:" + , PP.indent 2 (ppGoals ppAsmp ppGoal gls) + ] + Prove gl -> ppGoal gl + ProveConj gls gls' -> + PP.align $ + PP.vcat + [ PP.pretty "Prove both:" + , PP.indent 2 (ppGoals ppAsmp ppGoal gls) + , PP.indent 2 (ppGoals ppAsmp ppGoal gls') + ] + +-- | Intended for debugging, this is not generally a user-facing datatype. +instance (PP.Pretty asmp, PP.Pretty goal) => PP.Pretty (Goals asmp goal) where + pretty = ppGoals PP.pretty PP.pretty -- | Construct a goal that first assumes a collection of -- assumptions and then states a goal. diff --git a/src/Lang/Crucible/Backend/Online.hs b/src/Lang/Crucible/Backend/Online.hs --- a/src/Lang/Crucible/Backend/Online.hs +++ b/src/Lang/Crucible/Backend/Online.hs @@ -4,19 +4,26 @@ -- Description : A solver backend that maintains a persistent connection -- Copyright : (c) Galois, Inc 2015-2016 -- License : BSD3 --- Maintainer : Joe Hendrix +-- Maintainer : Ryan Scott , Langston Barrett -- Stability : provisional -- --- The online backend maintains an open connection to an SMT solver --- that is used to prune unsatisfiable execution traces during simulation. --- At every symbolic branch point, the SMT solver is queried to determine --- if one or both symbolic branches are unsatisfiable. --- Only branches with satisfiable branch conditions are explored. +-- A solver backend ('IsSymBackend') that maintains an open connection to an +-- SMT solver (in contrast to "Lang.Crucible.Backend.Simple"). -- --- The online backend also allows override definitions access to a --- persistent SMT solver connection. This can be useful for some --- kinds of algorithms that benefit from quickly performing many --- small solver queries in a tight interaction loop. +-- The primary intended use-case is to prune unsatisfiable execution +-- traces during simulation using the execution feature provided by +-- "Lang.Crucible.Simulator.PathSatisfiability". That execution feature is +-- parameterized over a function argument that can be instantiated with this +-- module's 'considerSatisfiability'. +-- +-- The online backend also allows override definitions access to a persistent +-- SMT solver connection. This can be useful for some kinds of algorithms +-- that benefit from quickly performing many small solver queries in a tight +-- interaction loop. +-- +-- The online backend is not currently used to dispatch proof obligations during +-- symbolic execution, see [GaloisInc/crucible#369, \"Interleave proof with +-- simulation\"](https://github.com/GaloisInc/crucible/issues/369). ------------------------------------------------------------------------ {-# LANGUAGE DeriveDataTypeable #-} @@ -27,9 +34,14 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} + module Lang.Crucible.Backend.Online - ( -- * OnlineBackend - OnlineBackend + ( -- * Configuration options + solverInteractionFile + , enableOnlineBackend + , onlineBackendOptions + -- * OnlineBackend + , OnlineBackend , withOnlineBackend , newOnlineBackend , checkSatisfiable @@ -39,13 +51,10 @@ , restoreSolverState , UnsatFeatures(..) , unsatFeaturesToProblemFeatures - -- ** Configuration options - , solverInteractionFile - , enableOnlineBackend - , onlineBackendOptions - -- ** Branch satisfiability + -- * Branch satisfiability , BranchResult(..) , considerSatisfiability + -- * Backends for different solvers -- ** Yices , YicesOnlineBackend , withYicesOnlineBackend @@ -69,21 +78,19 @@ , withSTPOnlineBackend ) where - -import Control.Lens ( (^.) ) import Control.Monad -import Control.Monad.Fix (mfix) import Control.Monad.Catch +import Control.Monad.Fix (mfix) import Control.Monad.IO.Class import Data.Bits import Data.Data (Data) import Data.Foldable import Data.IORef -import Data.Typeable (Typeable) -import GHC.Generics (Generic) -import System.IO import qualified Data.Text as Text +import GHC.Generics (Generic) +import Lens.Micro ((^.)) import qualified Prettyprinter as PP +import System.IO import What4.Config import What4.Concrete @@ -104,10 +111,13 @@ import qualified What4.Solver.Z3 as Z3 import Lang.Crucible.Backend -import Lang.Crucible.Backend.AssumptionStack as AS +import qualified Lang.Crucible.Backend.AssumptionStack as AS import qualified Lang.Crucible.Backend.ProofGoals as PG import Lang.Crucible.Simulator.SimError +-------------------------------------------------------------------------------- +-- Configuration options + data UnsatFeatures = NoUnsatFeatures -- ^ Do not compute unsat cores or assumptions @@ -173,6 +183,8 @@ -- ^ action for checking if online features are currently enabled , onlineExprBuilder :: B.ExprBuilder scope st fs + + , onlineExceptionContext :: !(Maybe ProgramStack) } newOnlineBackend :: @@ -181,7 +193,7 @@ ProblemFeatures -> IO (OnlineBackend solver scope st fs) newOnlineBackend sym feats = - do stk <- initAssumptionStack (sym ^. B.exprCounter) + do stk <- AS.initAssumptionStack (sym ^. B.exprCounter) procref <- newIORef SolverNotStarted featref <- newIORef feats @@ -198,6 +210,7 @@ , currentFeatures = featref , onlineEnabled = getOpt enableOpt , onlineExprBuilder = sym + , onlineExceptionContext = Nothing } -- | Do something with an online backend. @@ -224,176 +237,6 @@ ) -type YicesOnlineBackend scope st fs = OnlineBackend Yices.Connection scope st fs - --- | Do something with a Yices online backend. --- The backend is only valid in the continuation. --- --- The Yices configuration options will be automatically --- installed into the backend configuration object. --- --- n.b. the explicit forall allows the fs to be expressed as the --- first argument so that it can be dictated easily from the caller. --- Example: --- --- > withYicesOnlineBackend FloatRealRepr ng f' -withYicesOnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - UnsatFeatures -> - ProblemFeatures -> - (YicesOnlineBackend scope st fs -> m a) -> - m a -withYicesOnlineBackend sym unsatFeat extraFeatures action = - let feat = Yices.yicesDefaultFeatures .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures in - withOnlineBackend sym feat $ \bak -> - do liftIO $ tryExtendConfig Yices.yicesOptions (getConfiguration sym) - action bak - -type Z3OnlineBackend scope st fs = OnlineBackend (SMT2.Writer Z3.Z3) scope st fs - --- | Do something with a Z3 online backend. --- The backend is only valid in the continuation. --- --- The Z3 configuration options will be automatically --- installed into the backend configuration object. --- --- n.b. the explicit forall allows the fs to be expressed as the --- first argument so that it can be dictated easily from the caller. --- Example: --- --- > withz3OnlineBackend FloatRealRepr ng f' -withZ3OnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - UnsatFeatures -> - ProblemFeatures -> - (Z3OnlineBackend scope st fs -> m a) -> - m a -withZ3OnlineBackend sym unsatFeat extraFeatures action = - let feat = (SMT2.defaultFeatures Z3.Z3 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in - withOnlineBackend sym feat $ \bak -> - do liftIO $ tryExtendConfig Z3.z3Options (getConfiguration sym) - action bak - -type BitwuzlaOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Bitwuzla.Bitwuzla) scope st fs - --- | Do something with a Bitwuzla online backend. --- The backend is only valid in the continuation. --- --- The Bitwuzla configuration options will be automatically --- installed into the backend configuration object. --- --- > withBitwuzlaOnineBackend FloatRealRepr ng f' -withBitwuzlaOnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - UnsatFeatures -> - ProblemFeatures -> - (BitwuzlaOnlineBackend scope st fs -> m a) -> - m a -withBitwuzlaOnlineBackend sym unsatFeat extraFeatures action = - let feat = (SMT2.defaultFeatures Bitwuzla.Bitwuzla .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in - withOnlineBackend sym feat $ \bak -> do - liftIO $ tryExtendConfig Bitwuzla.bitwuzlaOptions (getConfiguration sym) - action bak - -type BoolectorOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Boolector.Boolector) scope st fs - --- | Do something with a Boolector online backend. --- The backend is only valid in the continuation. --- --- The Boolector configuration options will be automatically --- installed into the backend configuration object. --- --- > withBoolectorOnineBackend FloatRealRepr ng f' -withBoolectorOnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - UnsatFeatures -> - (BoolectorOnlineBackend scope st fs -> m a) -> - m a -withBoolectorOnlineBackend sym unsatFeat action = - let feat = (SMT2.defaultFeatures Boolector.Boolector .|. unsatFeaturesToProblemFeatures unsatFeat) in - withOnlineBackend sym feat $ \bak -> do - liftIO $ tryExtendConfig Boolector.boolectorOptions (getConfiguration sym) - action bak - -type CVC4OnlineBackend scope st fs = OnlineBackend (SMT2.Writer CVC4.CVC4) scope st fs - --- | Do something with a CVC4 online backend. --- The backend is only valid in the continuation. --- --- The CVC4 configuration options will be automatically --- installed into the backend configuration object. --- --- n.b. the explicit forall allows the fs to be expressed as the --- first argument so that it can be dictated easily from the caller. --- Example: --- --- > withCVC4OnlineBackend FloatRealRepr ng f' -withCVC4OnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - UnsatFeatures -> - ProblemFeatures -> - (CVC4OnlineBackend scope st fs -> m a) -> - m a -withCVC4OnlineBackend sym unsatFeat extraFeatures action = - let feat = (SMT2.defaultFeatures CVC4.CVC4 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in - withOnlineBackend sym feat $ \bak -> do - liftIO $ tryExtendConfig CVC4.cvc4Options (getConfiguration sym) - action bak - -type CVC5OnlineBackend scope st fs = OnlineBackend (SMT2.Writer CVC5.CVC5) scope st fs - --- | Do something with a CVC5 online backend. --- The backend is only valid in the continuation. --- --- The CVC5 configuration options will be automatically --- installed into the backend configuration object. --- --- n.b. the explicit forall allows the fs to be expressed as the --- first argument so that it can be dictated easily from the caller. --- Example: --- --- > withCVC5OnlineBackend FloatRealRepr ng f' -withCVC5OnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - UnsatFeatures -> - ProblemFeatures -> - (CVC5OnlineBackend scope st fs -> m a) -> - m a -withCVC5OnlineBackend sym unsatFeat extraFeatures action = - let feat = (SMT2.defaultFeatures CVC5.CVC5 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in - withOnlineBackend sym feat $ \bak -> do - liftIO $ tryExtendConfig CVC5.cvc5Options (getConfiguration sym) - action bak - -type STPOnlineBackend scope st fs = OnlineBackend (SMT2.Writer STP.STP) scope st fs - --- | Do something with a STP online backend. --- The backend is only valid in the continuation. --- --- The STO configuration options will be automatically --- installed into the backend configuration object. --- --- n.b. the explicit forall allows the fs to be expressed as the --- first argument so that it can be dictated easily from the caller. --- Example: --- --- > withSTPOnlineBackend FloatRealRepr ng f' -withSTPOnlineBackend :: - (MonadIO m, MonadMask m) => - B.ExprBuilder scope st fs -> - (STPOnlineBackend scope st fs -> m a) -> - m a -withSTPOnlineBackend sym action = - withOnlineBackend sym (SMT2.defaultFeatures STP.STP) $ \bak -> do - liftIO $ tryExtendConfig STP.stpOptions (getConfiguration sym) - action bak - -- | Shutdown any currently-active solver process. -- A fresh solver process will be started on the -- next call to `getSolverProcess`. @@ -497,30 +340,13 @@ withSolverConn bak k = withSolverProcess bak (pure ()) (k . solverConn) --- | Result of attempting to branch on a predicate. -data BranchResult - -- | The both branches of the predicate might be satisfiable - -- (although satisfiablility of either branch is not guaranteed). - = IndeterminateBranchResult - - -- | Commit to the branch where the given predicate is equal to - -- the returned boolean. The opposite branch is unsatisfiable - -- (although the given branch is not necessarily satisfiable). - | NoBranch !Bool - - -- | The context before considering the given predicate was already - -- unsatisfiable. - | UnsatisfiableContext - deriving (Data, Eq, Generic, Ord, Typeable) - - restoreAssumptionFrames :: OnlineSolver solver => OnlineBackend solver scope st fs -> SolverProcess scope solver -> - AssumptionFrames (CrucibleAssumptions (B.Expr scope)) -> + AS.AssumptionFrames (CrucibleAssumptions (B.Expr scope)) -> IO () -restoreAssumptionFrames bak proc (AssumptionFrames base frms) = +restoreAssumptionFrames bak proc (AS.AssumptionFrames base frms) = do let sym = onlineExprBuilder bak -- assume the base-level assumptions SMT.assume (solverConn proc) =<< assumptionsPred sym base @@ -530,29 +356,6 @@ do push proc SMT.assume (solverConn proc) =<< assumptionsPred sym frm -considerSatisfiability :: - OnlineSolver solver => - OnlineBackend solver scope st fs -> - Maybe ProgramLoc -> - B.BoolExpr scope -> - IO BranchResult -considerSatisfiability bak mbPloc p = - let sym = onlineExprBuilder bak in - withSolverProcess bak (pure IndeterminateBranchResult) $ \proc -> - do pnot <- notPred sym p - let locDesc = case mbPloc of - Just ploc -> show (plSourceLoc ploc) - Nothing -> "(unknown location)" - let rsn = "branch sat: " ++ locDesc - p_res <- checkSatisfiable proc rsn p - pnot_res <- checkSatisfiable proc rsn pnot - case (p_res, pnot_res) of - (Unsat{}, Unsat{}) -> return UnsatisfiableContext - (_ , Unsat{}) -> return (NoBranch True) - (Unsat{}, _ ) -> return (NoBranch False) - _ -> return IndeterminateBranchResult - - instance HasSymInterface (B.ExprBuilder t st fs) (OnlineBackend solver t st fs) where backendGetSym = onlineExprBuilder @@ -587,7 +390,7 @@ withSolverConn bak $ \conn -> SMT.assume conn p -- Add assertions to list - appendAssumptions as (assumptionStack bak) + AS.appendAssumptions as (assumptionStack bak) collectAssumptions bak = AS.collectAssumptions (assumptionStack bak) @@ -596,11 +399,11 @@ -- NB, don't push a frame in the assumption stack unless -- pushing to the solver succeeded do withSolverProcess bak (pure ()) push - pushFrame (assumptionStack bak) + AS.pushFrame (assumptionStack bak) popAssumptionFrame bak ident = -- NB, pop the frame whether or not the solver pop succeeds - do frm <- popFrame ident (assumptionStack bak) + do frm <- AS.popFrame ident (assumptionStack bak) withSolverProcess bak (pure ()) pop return frm @@ -612,7 +415,7 @@ popAssumptionFrameAndObligations bak ident = do -- NB, pop the frames whether or not the solver pop succeeds - do frmAndGls <- popFrameAndGoals ident (assumptionStack bak) + do frmAndGls <- AS.popFrameAndGoals ident (assumptionStack bak) withSolverProcess bak (pure ()) pop return frmAndGls @@ -629,3 +432,188 @@ do restoreSolverState bak gc -- restore the previous assumption stack AS.restoreAssumptionStack gc (assumptionStack bak) + + getBackendState bak = readIORef (AS.proofObligations (assumptionStack bak)) + + getExceptionContext = onlineExceptionContext + withExceptionContext bak ec = bak { onlineExceptionContext = Just ec } + +-------------------------------------------------------------------------------- +-- Branch satisfiability + +-- | Result of attempting to branch on a predicate. +data BranchResult + -- | The both branches of the predicate might be satisfiable + -- (although satisfiablility of either branch is not guaranteed). + = IndeterminateBranchResult + + -- | Commit to the branch where the given predicate is equal to + -- the returned boolean. The opposite branch is unsatisfiable + -- (although the given branch is not necessarily satisfiable). + | NoBranch !Bool + + -- | The context before considering the given predicate was already + -- unsatisfiable. + | UnsatisfiableContext + deriving (Data, Eq, Generic, Ord) + +considerSatisfiability :: + OnlineSolver solver => + OnlineBackend solver scope st fs -> + Maybe ProgramLoc -> + B.BoolExpr scope -> + IO BranchResult +considerSatisfiability bak mbPloc p = + let sym = onlineExprBuilder bak in + withSolverProcess bak (pure IndeterminateBranchResult) $ \proc -> + do pnot <- notPred sym p + let locDesc = case mbPloc of + Just ploc -> show (plSourceLoc ploc) + Nothing -> "(unknown location)" + let rsn = "branch sat: " ++ locDesc + p_res <- checkSatisfiable proc rsn p + pnot_res <- checkSatisfiable proc rsn pnot + case (p_res, pnot_res) of + (Unsat{}, Unsat{}) -> return UnsatisfiableContext + (_ , Unsat{}) -> return (NoBranch True) + (Unsat{}, _ ) -> return (NoBranch False) + _ -> return IndeterminateBranchResult + +-------------------------------------------------------------------------------- +-- Backends for different solvers + +type YicesOnlineBackend scope st fs = OnlineBackend Yices.Connection scope st fs + +-- | Do something with a Yices online backend. +-- The backend is only valid in the continuation. +-- +-- The Yices configuration options will be automatically +-- installed into the backend configuration object. +withYicesOnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + UnsatFeatures -> + ProblemFeatures -> + (YicesOnlineBackend scope st fs -> m a) -> + m a +withYicesOnlineBackend sym unsatFeat extraFeatures action = + let feat = Yices.yicesDefaultFeatures .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures in + withOnlineBackend sym feat $ \bak -> + do liftIO $ tryExtendConfig Yices.yicesOptions (getConfiguration sym) + action bak + +type Z3OnlineBackend scope st fs = OnlineBackend (SMT2.Writer Z3.Z3) scope st fs + +-- | Do something with a Z3 online backend. +-- The backend is only valid in the continuation. +-- +-- The Z3 configuration options will be automatically +-- installed into the backend configuration object. +withZ3OnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + UnsatFeatures -> + ProblemFeatures -> + (Z3OnlineBackend scope st fs -> m a) -> + m a +withZ3OnlineBackend sym unsatFeat extraFeatures action = + let feat = (SMT2.defaultFeatures Z3.Z3 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in + withOnlineBackend sym feat $ \bak -> + do liftIO $ tryExtendConfig Z3.z3Options (getConfiguration sym) + action bak + +type BitwuzlaOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Bitwuzla.Bitwuzla) scope st fs + +-- | Do something with a Bitwuzla online backend. +-- The backend is only valid in the continuation. +-- +-- The Bitwuzla configuration options will be automatically +-- installed into the backend configuration object. +withBitwuzlaOnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + UnsatFeatures -> + ProblemFeatures -> + (BitwuzlaOnlineBackend scope st fs -> m a) -> + m a +withBitwuzlaOnlineBackend sym unsatFeat extraFeatures action = + let feat = (SMT2.defaultFeatures Bitwuzla.Bitwuzla .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in + withOnlineBackend sym feat $ \bak -> do + liftIO $ tryExtendConfig Bitwuzla.bitwuzlaOptions (getConfiguration sym) + action bak + +type BoolectorOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Boolector.Boolector) scope st fs + +-- | Do something with a Boolector online backend. +-- The backend is only valid in the continuation. +-- +-- The Boolector configuration options will be automatically +-- installed into the backend configuration object. +withBoolectorOnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + UnsatFeatures -> + (BoolectorOnlineBackend scope st fs -> m a) -> + m a +withBoolectorOnlineBackend sym unsatFeat action = + let feat = (SMT2.defaultFeatures Boolector.Boolector .|. unsatFeaturesToProblemFeatures unsatFeat) in + withOnlineBackend sym feat $ \bak -> do + liftIO $ tryExtendConfig Boolector.boolectorOptions (getConfiguration sym) + action bak + +type CVC4OnlineBackend scope st fs = OnlineBackend (SMT2.Writer CVC4.CVC4) scope st fs + +-- | Do something with a CVC4 online backend. +-- The backend is only valid in the continuation. +-- +-- The CVC4 configuration options will be automatically +-- installed into the backend configuration object. +withCVC4OnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + UnsatFeatures -> + ProblemFeatures -> + (CVC4OnlineBackend scope st fs -> m a) -> + m a +withCVC4OnlineBackend sym unsatFeat extraFeatures action = + let feat = (SMT2.defaultFeatures CVC4.CVC4 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in + withOnlineBackend sym feat $ \bak -> do + liftIO $ tryExtendConfig CVC4.cvc4Options (getConfiguration sym) + action bak + +type CVC5OnlineBackend scope st fs = OnlineBackend (SMT2.Writer CVC5.CVC5) scope st fs + +-- | Do something with a CVC5 online backend. +-- The backend is only valid in the continuation. +-- +-- The CVC5 configuration options will be automatically +-- installed into the backend configuration object. +withCVC5OnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + UnsatFeatures -> + ProblemFeatures -> + (CVC5OnlineBackend scope st fs -> m a) -> + m a +withCVC5OnlineBackend sym unsatFeat extraFeatures action = + let feat = (SMT2.defaultFeatures CVC5.CVC5 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in + withOnlineBackend sym feat $ \bak -> do + liftIO $ tryExtendConfig CVC5.cvc5Options (getConfiguration sym) + action bak + +type STPOnlineBackend scope st fs = OnlineBackend (SMT2.Writer STP.STP) scope st fs + +-- | Do something with a STP online backend. +-- The backend is only valid in the continuation. +-- +-- The STO configuration options will be automatically +-- installed into the backend configuration object. +withSTPOnlineBackend :: + (MonadIO m, MonadMask m) => + B.ExprBuilder scope st fs -> + (STPOnlineBackend scope st fs -> m a) -> + m a +withSTPOnlineBackend sym action = + withOnlineBackend sym (SMT2.defaultFeatures STP.STP) $ \bak -> do + liftIO $ tryExtendConfig STP.stpOptions (getConfiguration sym) + action bak diff --git a/src/Lang/Crucible/Backend/ProofGoals.hs b/src/Lang/Crucible/Backend/ProofGoals.hs --- a/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/src/Lang/Crucible/Backend/ProofGoals.hs @@ -3,10 +3,11 @@ Copyright : (c) Galois, Inc 2014-2018 License : BSD3 -This module defines a data strucutre for storing a collection of -proof obligations, and the current state of assumptions. +This module defines a data structure ('GoalCollector') for storing the current +state of assumptions and a collection of proof obligations. -} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} @@ -22,6 +23,7 @@ -- * Goal collector , FrameIdentifier(..), GoalCollector , emptyGoalCollector + , ppGoalCollector -- ** traversals , traverseGoalCollector @@ -29,7 +31,7 @@ -- ** Context management , gcAddAssumes, gcProve - , gcPush, gcPop, gcAddGoals, + , gcPush, gcPop, gcAddGoals, gcAddTopLevelAssume, -- ** Global operations on context gcRemoveObligations, gcRestore, gcReset, gcFinish @@ -40,9 +42,11 @@ where import Control.Monad.Reader +import qualified Data.Foldable as F import Data.Sequence (Seq) import qualified Data.Sequence as Seq import Data.Word (Word64) +import qualified Prettyprinter as PP import Lang.Crucible.Backend.Goals @@ -55,16 +59,80 @@ deriving(Eq,Ord,Show) --- | A data-strucutre that can incrementally collect goals in context. +-- | A data-structure that can incrementally collect goals in context. -- It keeps track both of the collection of assumptions that lead to -- the current state, as well as any proof obligations incurred along -- the way. +-- +-- The main use of 'GoalCollector' is as the state of an +-- 'Lang.Crucible.Backend.AssumptionStack.AssumptionStack', which itself is +-- part of the state of the simple and online backends. +-- +-- 'GoalCollector' can be somewhat counter-intuitive. The "top" +-- ('TopCollector') is the *leaf* when 'GoalCollector' is considered as +-- a tree (which is a common way to conceptualize recursive algebraic +-- data types such as this one). A 'GoalCollector' is shaped like a +-- cons-list with three different cons-like constructors ('CollectorFrame', +-- 'CollectingAssumptions', and 'CollectingGoals') and one nil-like +-- constructor 'TopCollector'. That is to say, a 'GoalCollector' is a sequence +-- that always ends in a single 'TopCollector'. +-- +-- Furthermore, the frame identified by the first ('FrameIdentifier') argument +-- of 'CollectorFrame' does not conceptually contain the goals *inside* the +-- second ('GoalCollector') argument, but rather contains all the assumptions +-- and goals in whatever 'GoalCollector' *contains* the 'CollectorFrame' +-- constructor (everything *outside* of the 'CollectorFrame'). Concretely, in +-- the expression +-- @ +-- 'CollectingGoals' gls ('CollectingAssumptions' asmps ('CollectorFrame' frm ('TopCollector' gls0))) +-- @ +-- the goals @gls@ and assumptions @asmps@ are in the frame @frm@, rather than +-- the top-level goals @gls0@. +-- +-- This inside-out structure is reflected in the pretty-printer +-- 'ppGoalCollector' below. The Crucible-CLI test-case @assumption-state@ +-- shows this pretty-printer in action in a Crucible program with branching, +-- which can be helpful in understanding 'GoalCollector'. data GoalCollector asmp goal = TopCollector !(Seq (Goals asmp goal)) | CollectorFrame !FrameIdentifier !(GoalCollector asmp goal) | CollectingAssumptions !asmp !(GoalCollector asmp goal) | CollectingGoals !(Seq (Goals asmp goal)) !(GoalCollector asmp goal) +ppGoalCollector :: + forall asmp goal ann. + (asmp -> PP.Doc ann) -> + (goal -> PP.Doc ann) -> + GoalCollector asmp goal -> + PP.Doc ann +ppGoalCollector ppAsmp ppGoal = go mempty + where + go :: PP.Doc ann -> GoalCollector asmp goal -> PP.Doc ann + go remainder = + \case + TopCollector gls -> + PP.vcat + [ PP.pretty "Top-level goals:" + , PP.list (map (ppGoals ppAsmp ppGoal) (F.toList gls)) + , remainder + ] + CollectorFrame (FrameIdentifier fid) gc -> + let pLines = [PP.pretty "Frame " <> PP.viaShow fid <> PP.pretty ":", remainder] in + go (PP.hang 2 (PP.vcat pLines)) gc + CollectingAssumptions asmp gc -> + let pLines = [PP.pretty "Assumptions:" , ppAsmp asmp, remainder] in + go (PP.hang 2 (PP.vcat pLines)) gc + CollectingGoals gls gc -> + let pLines = [ PP.pretty "Prove all:" + , PP.list (map (ppGoals ppAsmp ppGoal) (F.toList gls)) + , remainder + ] in + go (PP.hang 2 (PP.vcat pLines)) gc + +-- | Intended for debugging, this is not generally a user-facing datatype. +instance (PP.Pretty asmp, PP.Pretty goal) => PP.Pretty (GoalCollector asmp goal) where + pretty = ppGoalCollector PP.pretty PP.pretty + -- | A collector with no goals and no context. emptyGoalCollector :: GoalCollector asmp goal emptyGoalCollector = TopCollector mempty @@ -141,6 +209,30 @@ gcAddGoals g (TopCollector gs) = TopCollector (gs Seq.|> g) gcAddGoals g (CollectingGoals gs gc) = CollectingGoals (gs Seq.|> g) gc gcAddGoals g gc = CollectingGoals (Seq.singleton g) gc + +-- | Add an assumption that is in scope for all goals, even ones in earlier +-- frames. +gcAddTopLevelAssume :: + Monoid asmp => + asmp -> + GoalCollector asmp goal -> + GoalCollector asmp goal +gcAddTopLevelAssume asmp = + \case + TopCollector gls -> + -- Syntactically, it appears that `asmp` is duplicated here, perhaps + -- unnecessarily. In fact, this is necessary. The `CollectingAssumptions` + -- constructor brings the assumption into scope for all the goals + -- *outside* of the top-level (see the comment on `GoalCollector` for + -- the "inside-out" structure of `GoalCollector`), whereas the `assuming` + -- brings it into scope for top-level goals. + CollectingAssumptions asmp (TopCollector (assuming asmp <$> gls)) + CollectorFrame frm gc -> + CollectorFrame frm (gcAddTopLevelAssume asmp gc) + CollectingAssumptions asmp' gc -> + CollectingAssumptions asmp' (gcAddTopLevelAssume asmp gc) + CollectingGoals gls gc -> + CollectingGoals gls (gcAddTopLevelAssume asmp gc) -- | Add a new proof obligation to the current context. gcProve :: goal -> GoalCollector asmp goal -> GoalCollector asmp goal diff --git a/src/Lang/Crucible/Backend/Prove.hs b/src/Lang/Crucible/Backend/Prove.hs --- a/src/Lang/Crucible/Backend/Prove.hs +++ b/src/Lang/Crucible/Backend/Prove.hs @@ -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 diff --git a/src/Lang/Crucible/Backend/Simple.hs b/src/Lang/Crucible/Backend/Simple.hs --- a/src/Lang/Crucible/Backend/Simple.hs +++ b/src/Lang/Crucible/Backend/Simple.hs @@ -4,13 +4,13 @@ -- Description : The "simple" solver backend -- Copyright : (c) Galois, Inc 2015-2016 -- License : BSD3 --- Maintainer : Rob Dockins +-- Maintainer : Ryan Scott , Langston Barrett -- Stability : provisional -- --- An "offline" backend for communicating with solvers. This backend --- does not maintain a persistent connection to a solver, and does --- not perform satisfiability checks at symbolic branch points. ------------------------------------------------------------------------- +-- An "offline" backend for communicating with SMT solvers. In contrast to +-- "Lang.Crucible.Backend.Online", this backend does not maintain a persistent +-- connection to a solver. +-- ---------------------------------------------------------------------- {-# LANGUAGE GADTs #-} {-# LANGUAGE FlexibleContexts #-} @@ -30,8 +30,9 @@ , B.Flags ) where -import Control.Lens ( (^.) ) import Control.Monad (void) +import Data.IORef (readIORef) +import Lens.Micro ((^.)) import What4.Config import What4.Interface @@ -42,7 +43,7 @@ import Lang.Crucible.Simulator.SimError ------------------------------------------------------------------------ --- SimpleBackendState +-- SimpleBackend -- | This represents the state of the backend along a given execution. -- It contains the current assertion stack. @@ -55,8 +56,10 @@ SimpleBackend { sbAssumptionStack :: AS t , sbExprBuilder :: B.ExprBuilder t st fs + , sbExceptionContext :: Maybe ProgramStack } + newSimpleBackend :: B.ExprBuilder t st fs -> IO (SimpleBackend t st fs) @@ -66,6 +69,7 @@ return SimpleBackend { sbAssumptionStack = as , sbExprBuilder = sym + , sbExceptionContext = Nothing } instance HasSymInterface (B.ExprBuilder t st fs) (SimpleBackend t st fs) where @@ -111,3 +115,8 @@ restoreAssumptionState bak newstk = do AS.restoreAssumptionStack newstk (sbAssumptionStack bak) + + getBackendState bak = readIORef (AS.proofObligations (sbAssumptionStack bak)) + + withExceptionContext bak ec = bak { sbExceptionContext = Just ec } + getExceptionContext = sbExceptionContext diff --git a/src/Lang/Crucible/CFG/Common.hs b/src/Lang/Crucible/CFG/Common.hs --- a/src/Lang/Crucible/CFG/Common.hs +++ b/src/Lang/Crucible/CFG/Common.hs @@ -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 diff --git a/src/Lang/Crucible/CFG/Core.hs b/src/Lang/Crucible/CFG/Core.hs --- a/src/Lang/Crucible/CFG/Core.hs +++ b/src/Lang/Crucible/CFG/Core.hs @@ -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 diff --git a/src/Lang/Crucible/CFG/EarlyMergeLoops.hs b/src/Lang/Crucible/CFG/EarlyMergeLoops.hs --- a/src/Lang/Crucible/CFG/EarlyMergeLoops.hs +++ b/src/Lang/Crucible/CFG/EarlyMergeLoops.hs @@ -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 diff --git a/src/Lang/Crucible/CFG/Expr.hs b/src/Lang/Crucible/CFG/Expr.hs --- a/src/Lang/Crucible/CFG/Expr.hs +++ b/src/Lang/Crucible/CFG/Expr.hs @@ -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 diff --git a/src/Lang/Crucible/CFG/ExtractSubgraph.hs b/src/Lang/Crucible/CFG/ExtractSubgraph.hs --- a/src/Lang/Crucible/CFG/ExtractSubgraph.hs +++ b/src/Lang/Crucible/CFG/ExtractSubgraph.hs @@ -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 diff --git a/src/Lang/Crucible/CFG/Generator.hs b/src/Lang/Crucible/CFG/Generator.hs --- a/src/Lang/Crucible/CFG/Generator.hs +++ b/src/Lang/Crucible/CFG/Generator.hs @@ -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) diff --git a/src/Lang/Crucible/CFG/Reg.hs b/src/Lang/Crucible/CFG/Reg.hs --- a/src/Lang/Crucible/CFG/Reg.hs +++ b/src/Lang/Crucible/CFG/Reg.hs @@ -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 diff --git a/src/Lang/Crucible/CFG/SSAConversion.hs b/src/Lang/Crucible/CFG/SSAConversion.hs --- a/src/Lang/Crucible/CFG/SSAConversion.hs +++ b/src/Lang/Crucible/CFG/SSAConversion.hs @@ -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' diff --git a/src/Lang/Crucible/Concretize.hs b/src/Lang/Crucible/Concretize.hs --- a/src/Lang/Crucible/Concretize.hs +++ b/src/Lang/Crucible/Concretize.hs @@ -7,15 +7,27 @@ -- Maintainer : Langston Barrett -- Stability : provisional -- --- This module defines 'concRegValue', a function that takes a 'RegValue' (i.e., --- a symbolic value), and a model from the SMT solver ('W4GE.GroundEvalFn'), and --- returns the concrete value that the symbolic value takes in the model. +-- This module defines three different kinds of functions. In order of how much +-- work they perform: -- --- This can be used to report specific values that lead to violations of --- assertions, including safety assertions. +-- * /Grounding/ functions (e.g., 'groundRegValue') take symbolic values +-- ('RegValue's) and a model from an SMT solver ('W4GE.GroundEvalFn'), and +-- return the concrete value ('ConcRegValue') that the symbolic value takes in +-- the model. These functions can be used to report specific values that lead +-- to violations of assertions, including safety assertions. +-- * /Concretization/ functions (e.g., 'concRegValue') request a model that is +-- consistent with the current assumptions (e.g., path conditions) from the +-- symbolic backend, and then ground a value in that model. These can be used +-- to reduce the size and complexity of later queries to SMT solvers, at the +-- cost of no longer being sound from a verification standpoint. +-- * /Unique concretization/ functions (e.g., 'uniquelyConcRegValue') do the +-- same thing as concretization functions, but then check if the concrete +-- value is the /only possible/ value for the given symbolic expression in +-- /any/ model. ------------------------------------------------------------------------ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE StandaloneKindSignatures #-} @@ -30,24 +42,38 @@ module Lang.Crucible.Concretize ( ConcRegValue , ConcRV'(..) + , asConcRegValue + , asConcRegEntry + , asConcRegMap , ConcAnyValue(..) , ConcIntrinsic , IntrinsicConcFn(..) , ConcCtx(..) + -- * Grounding + , groundRegValue + , groundRegEntry + , groundRegMap + -- * Concretization , concRegValue , concRegEntry , concRegMap + -- * Unique concretization + , uniquelyConcRegValue + , uniquelyConcRegEntry + , uniquelyConcRegMap -- * There and back again , IntrinsicConcToSymFn(..) , concToSym ) where import qualified Data.Foldable as F +import Data.Functor.Const (Const(..)) import Data.Kind (Type) import Data.List.NonEmpty (NonEmpty) import qualified Data.List.NonEmpty as NE import Data.Map (Map) import qualified Data.Map as Map +import Data.Proxy (Proxy(Proxy)) import Data.Sequence (Seq) import Data.Text (Text) import qualified Data.Text as Text @@ -57,14 +83,20 @@ import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Map (MapF) import qualified Data.Parameterized.Map as MapF -import Data.Parameterized.TraversableFC (traverseFC) +import Data.Parameterized.TraversableFC (traverseFC, foldlMFC) +import qualified What4.Concretize as W4C +import qualified What4.Config as W4Cfg import What4.Expr (Expr, ExprBuilder, Flags, FloatModeRepr(..)) import qualified What4.Expr.GroundEval as W4GE import What4.Interface (SymExpr) import qualified What4.Interface as W4I import qualified What4.Partial as W4P +import qualified What4.Protocol.Online as WPO +import qualified What4.SatResult as WSat +import qualified Lang.Crucible.Backend as CB +import qualified Lang.Crucible.Backend.Online as CBO import Lang.Crucible.FunctionHandle (FnHandle, RefCell) import Lang.Crucible.Simulator.Intrinsics (Intrinsic) import Lang.Crucible.Simulator.RegMap (RegEntry, RegMap) @@ -84,7 +116,7 @@ -- | Defines the \"concrete\" interpretations of 'CrucibleType' (as opposed -- to the \"symbolic\" interpretations, which are defined by 'RegValue'), as --- returned by 'concRegValue'. +-- returned by 'groundRegValue'. -- -- Unlike What4\'s 'W4GE.GroundValue', this type family is parameterized -- by @sym@, the symbolic backend. This is because Crucible makes use of @@ -112,10 +144,40 @@ ConcRegValue sym (IntrinsicType nm ctx) = ConcIntrinsic nm ctx ConcRegValue sym (StringMapType tp) = Map Text (ConcRV' sym tp) +-- | Check if a 'RegValue' is actually concrete +asConcRegValue :: + W4I.IsExpr (SymExpr sym) => + proxy sym -> + TypeRepr tp -> + RegValue sym tp -> + Maybe (ConcRegValue sym tp) +asConcRegValue _proxy tp val = + -- TODO: More cases could be added here. + case asBaseType tp of + AsBaseType {} -> W4GE.asGround val + _ -> Nothing + +-- | Check if a 'RM.RegEntry' is actually concrete +asConcRegEntry :: + forall sym tp. + W4I.IsExpr (SymExpr sym) => + RM.RegEntry sym tp -> + Maybe (ConcRegValue sym tp) +asConcRegEntry (RM.RegEntry t v) = asConcRegValue (Proxy @sym) t v + +-- | Check if a 'RM.RegMap' is actually concrete +asConcRegMap :: + forall sym tp. + W4I.IsExpr (SymExpr sym) => + RM.RegMap sym tp -> + Maybe (Ctx.Assignment (ConcRV' sym) tp) +asConcRegMap (RM.RegMap assign) = + traverseFC (\re -> ConcRV' <$> asConcRegEntry re) assign + --------------------------------------------------------------------- -- * ConcCtx --- | Context needed for 'concRegValue' +-- | Context needed for 'groundRegValue' -- -- The @t@ parameter matches that on 'W4GE.GroundEvalFn' and 'Expr', namely, it -- is a phantom type brand used to relate nonces to a specific nonce generator @@ -172,7 +234,7 @@ W4P.Partial (W4I.Pred sym) (RegValue sym tp) -> IO (Maybe (ConcRegValue sym tp)) concPartial ctx tp (W4P.Partial p v) = - iteIO ctx p (Just <$> concRegValue ctx tp v) (pure Nothing) + iteIO ctx p (Just <$> groundRegValue ctx tp v) (pure Nothing) -- | Helper, not exported concPartialWithErr :: @@ -224,13 +286,13 @@ --------------------------------------------------------------------- -- * Any --- | An 'AnyValue' concretized by 'concRegValue' +-- | An 'AnyValue' concretized by 'groundRegValue' data ConcAnyValue sym = forall tp. ConcAnyValue (TypeRepr tp) (ConcRV' sym tp) --------------------------------------------------------------------- -- * FnVal --- | A 'FnVal' concretized by 'concRegValue' +-- | A 'FnVal' concretized by 'groundRegValue' data ConcFnVal (sym :: Type) (args :: Ctx CrucibleType) (res :: CrucibleType) where ConcClosureFnVal :: !(ConcFnVal sym (args ::> tp) ret) -> @@ -260,7 +322,7 @@ \case RV.ClosureFnVal fv t v -> do concV <- concFnVal ctx (args Ctx.:> t) ret fv - v' <- concRegValue ctx t v + v' <- groundRegValue ctx t v pure (ConcClosureFnVal concV t (ConcRV' v')) RV.VarargsFnVal hdl extra -> pure (ConcVarargsFnVal hdl extra) @@ -306,7 +368,7 @@ concSymSequence ctx tp = SymSeq.concretizeSymSequence (ground ctx) - (fmap ConcRV' . concRegValue ctx tp) + (fmap ConcRV' . groundRegValue ctx tp) --------------------------------------------------------------------- -- * StringMap @@ -331,7 +393,7 @@ --------------------------------------------------------------------- -- * Variant --- | Note that we do not attempt to \"normalize\" variants in 'concRegValue' +-- | Note that we do not attempt to \"normalize\" variants in 'groundRegValue' -- in any way. If the model reports that multiple branches of a variant are -- plausible, then multiple branches might be included as 'Just's. newtype ConcVariantBranch sym tp @@ -356,21 +418,21 @@ Nothing -> pure (ConcVariantBranch Nothing) --------------------------------------------------------------------- --- * 'concRegValue' +-- * 'groundRegValue' -- | Pick a feasible concrete value from the model -- -- This function does not attempt to \"normalize\" variants nor mux trees in any -- way. If the model reports that multiple branches of a variant or mux tree are -- plausible, then multiple branches might be included in the result. -concRegValue :: +groundRegValue :: (SymExpr sym ~ Expr t) => W4I.IsExprBuilder sym => ConcCtx sym t -> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp) -concRegValue ctx tp v = +groundRegValue ctx tp v = case (tp, v) of -- Base types (BoolRepr, _) -> ground ctx v @@ -391,13 +453,13 @@ -- Simple recursive cases (AnyRepr, RV.AnyValue tp' v') -> - ConcAnyValue tp' . ConcRV' <$> concRegValue ctx tp' v' + ConcAnyValue tp' . ConcRV' <$> groundRegValue ctx tp' v' (RecursiveRepr symb tyCtx, RV.RolledType v') -> - concRegValue ctx (unrollType symb tyCtx) v' + groundRegValue ctx (unrollType symb tyCtx) v' (StructRepr tps, _) -> - Ctx.zipWithM (\tp' (RV.RV v') -> ConcRV' <$> concRegValue ctx tp' v') tps v + Ctx.zipWithM (\tp' (RV.RV v') -> ConcRV' <$> groundRegValue ctx tp' v') tps v (VectorRepr tp', _) -> - traverse (fmap ConcRV' . concRegValue ctx tp') v + traverse (fmap ConcRV' . groundRegValue ctx tp') v -- Cases with helper functions (MaybeRepr tp', _) -> @@ -422,26 +484,210 @@ -- Incomplete cases (WordMapRepr _ _, _) -> pure () --- | Like 'concRegValue', but for 'RegEntry' -concRegEntry :: +-- | Like 'groundRegValue', but for 'RegEntry' +groundRegEntry :: (SymExpr sym ~ Expr t) => W4I.IsExprBuilder sym => ConcCtx sym t -> RegEntry sym tp -> IO (ConcRegValue sym tp) -concRegEntry ctx e = concRegValue ctx (RM.regType e) (RM.regValue e) +groundRegEntry ctx e = groundRegValue ctx (RM.regType e) (RM.regValue e) --- | Like 'concRegEntry', but for a whole 'RegMap' -concRegMap :: +-- | Like 'groundRegEntry', but for a whole 'RegMap' +groundRegMap :: (SymExpr sym ~ Expr t) => W4I.IsExprBuilder sym => ConcCtx sym t -> RegMap sym tps -> IO (Ctx.Assignment (ConcRV' sym) tps) -concRegMap ctx (RM.RegMap m) = traverseFC (fmap ConcRV' . concRegEntry ctx) m +groundRegMap ctx (RM.RegMap m) = traverseFC (fmap ConcRV' . groundRegEntry ctx) m --------------------------------------------------------------------- --- * concToSym +-- * 'concRegValue' + +-- | Generate a model and pick a feasible concrete value from it +concRegValue :: + forall tp sym bak solver scope st fs. + ( CB.IsSymBackend sym bak + , sym ~ ExprBuilder scope st fs + , SymExpr sym ~ Expr scope + , bak ~ CBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + ) => + bak -> + MapF SymbolRepr (IntrinsicConcFn scope) -> + TypeRepr tp -> + RegValue sym tp -> + IO (Either W4C.ConcretizationFailure (ConcRegValue sym tp)) +concRegValue bak iFns tp v = concRegEntry bak iFns (RM.RegEntry tp v) + +-- | Generate a model and pick a feasible concrete value from it +concRegEntry :: + forall tp sym bak solver scope st fs. + ( CB.IsSymBackend sym bak + , sym ~ ExprBuilder scope st fs + , SymExpr sym ~ Expr scope + , bak ~ CBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + ) => + bak -> + MapF SymbolRepr (IntrinsicConcFn scope) -> + RM.RegEntry sym tp -> + IO (Either W4C.ConcretizationFailure (ConcRegValue sym tp)) +concRegEntry bak iFns re = do + res <- concRegMap bak iFns (RM.RegMap (Ctx.singleton re)) + case res of + Left e -> pure (Left e) + Right (Ctx.Empty Ctx.:> ConcRV' concV) -> pure (Right concV) + +-- | Like 'concRegValue', but for a whole 'RegMap' +concRegMap :: + forall tps sym bak solver scope st fs. + ( CB.IsSymBackend sym bak + , sym ~ ExprBuilder scope st fs + , SymExpr sym ~ Expr scope + , bak ~ CBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + ) => + bak -> + MapF SymbolRepr (IntrinsicConcFn scope) -> + RegMap sym tps -> + IO (Either W4C.ConcretizationFailure (Ctx.Assignment (ConcRV' sym) tps)) +concRegMap bak iFns m = do + case asConcRegMap m of + Just concM -> pure (Right concM) + Nothing -> + withEnabledOnline $ do + let err = panic "concRegValue" ["requires online solving to be enabled"] + cond <- CB.getPathCondition bak + CBO.withSolverProcess bak err $ \sp -> do + msat <- WPO.checkWithAssumptionsAndModel sp "concRegValue" [cond] + case msat of + WSat.Unknown -> pure $ Left W4C.SolverUnknown + WSat.Unsat {} -> pure $ Left W4C.UnsatInitialAssumptions + WSat.Sat mdl -> do + let ctx = ConcCtx { model = mdl, intrinsicConcFuns = iFns } + expr <- groundRegMap @sym ctx m + pure (Right expr) + where + withEnabledOnline f = do + let sym = CB.backendGetSym bak + let conf = W4I.getConfiguration sym + enabledOpt <- W4Cfg.getOptionSetting CBO.enableOnlineBackend conf + wasEnabled <- W4Cfg.getOpt enabledOpt + _ <- W4Cfg.setOpt enabledOpt True + r <- f + _ <- W4Cfg.setOpt enabledOpt wasEnabled + pure r + +--------------------------------------------------------------------- +-- * 'uniquelyConcRegValue' + +-- | Generate a model and pick a feasible concrete value from it +uniquelyConcRegValue :: + forall tp sym bak solver scope st fm. + ( CB.IsSymBackend sym bak + , sym ~ ExprBuilder scope st (Flags fm) + , SymExpr sym ~ Expr scope + , bak ~ CBO.OnlineBackend solver scope st (Flags fm) + , WPO.OnlineSolver solver + ) => + bak -> + FloatModeRepr fm -> + MapF SymbolRepr (IntrinsicConcFn scope) -> + MapF SymbolRepr IntrinsicConcToSymFn -> + TypeRepr tp -> + RegValue sym tp -> + IO (Either W4C.UniqueConcretizationFailure (ConcRegValue sym tp)) +uniquelyConcRegValue bak fm iFns sFns tp v = + uniquelyConcRegEntry bak fm iFns sFns (RM.RegEntry tp v) + +-- | Generate a model and pick a feasible concrete value from it +uniquelyConcRegEntry :: + forall tp sym bak solver scope st fm. + ( CB.IsSymBackend sym bak + , sym ~ ExprBuilder scope st (Flags fm) + , SymExpr sym ~ Expr scope + , bak ~ CBO.OnlineBackend solver scope st (Flags fm) + , WPO.OnlineSolver solver + ) => + bak -> + FloatModeRepr fm -> + MapF SymbolRepr (IntrinsicConcFn scope) -> + MapF SymbolRepr IntrinsicConcToSymFn -> + RM.RegEntry sym tp -> + IO (Either W4C.UniqueConcretizationFailure (ConcRegValue sym tp)) +uniquelyConcRegEntry bak fm iFns sFns re = do + res <- uniquelyConcRegMap bak fm iFns sFns (RM.RegMap (Ctx.singleton re)) + case res of + Left e -> pure (Left e) + Right (Ctx.Empty Ctx.:> ConcRV' concV) -> pure (Right concV) + +-- | Like 'concRegValue', but for a whole 'RegMap' +uniquelyConcRegMap :: + forall tps sym bak solver scope st fm. + ( CB.IsSymBackend sym bak + , sym ~ ExprBuilder scope st (Flags fm) + , SymExpr sym ~ Expr scope + , bak ~ CBO.OnlineBackend solver scope st (Flags fm) + , WPO.OnlineSolver solver + ) => + bak -> + FloatModeRepr fm -> + MapF SymbolRepr (IntrinsicConcFn scope) -> + MapF SymbolRepr IntrinsicConcToSymFn -> + RegMap sym tps -> + IO (Either W4C.UniqueConcretizationFailure (Ctx.Assignment (ConcRV' sym) tps)) +uniquelyConcRegMap bak fm iFns sFns m = do + case asConcRegMap m of + Just concM -> pure (Right concM) + Nothing -> do + -- First, check to see if there are a models of the symbolic values. + concM_ <- concRegMap bak iFns m + case concM_ of + Left e -> pure (Left (W4C.GroundingFailure e)) + Right concM -> do + -- We found a model, so check to see if this is the only possible + -- model for these symbolic values. We do this by adding a blocking + -- clause that assumes the `RegValue`s are /not/ equal to the + -- model we found in the previous step. If this is unsatisfiable, + -- the `RegValue`s can only be equal to the first model, so we can + -- conclude they are concrete. If it is satisfiable, on the other + -- hand, the `RegValue`s can be multiple values, so they are truly + -- symbolic. + let sym = CB.backendGetSym bak + let notEq :: + forall tp. + ConcRV' sym tp -> + RM.RegEntry sym tp -> + IO (Const (W4I.Pred sym) tp) + notEq (ConcRV' concV) (RM.RegEntry tp v) = do + symV <- concToSym sym sFns fm tp concV + p <- W4I.notPred sym =<< RV.eqRegValue sym tp symV v + pure (Const p) + let RM.RegMap mAssign = m + preds <- Ctx.zipWithM notEq concM mAssign + -- not (modelA_1 == modelB_1) \/ ... \/ not (modelA_n == modelB_n) + p <- + foldlMFC + (\p (Const p') -> W4I.orPred sym p p') + (W4I.falsePred sym) + preds + + frm <- CB.pushAssumptionFrame bak + loc <- W4I.getCurrentProgramLoc sym + CB.addAssumption bak (CB.GenericAssumption loc "uniquelyConcRegMap" p) + concM_' <- concRegMap bak iFns m + res <- + case concM_' of + Left W4C.UnsatInitialAssumptions -> pure (Right concM) + Left e -> pure (Left (W4C.GroundingFailure e)) + Right _ -> pure (Left W4C.MultipleModels) + _ <- CB.popAssumptionFrame bak frm + pure res + +--------------------------------------------------------------------- +-- * 'concToSym' -- | Function for re-symbolizing an intrinsic type type IntrinsicConcToSymFn :: Symbol -> Type diff --git a/src/Lang/Crucible/FunctionHandle.hs b/src/Lang/Crucible/FunctionHandle.hs --- a/src/Lang/Crucible/FunctionHandle.hs +++ b/src/Lang/Crucible/FunctionHandle.hs @@ -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)) diff --git a/src/Lang/Crucible/README.hs b/src/Lang/Crucible/README.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/README.hs @@ -0,0 +1,114 @@ +{- | This module is only for documentation purposes, and provides a high +level overview of Crucible aimed at developers. -} +{-# OPTIONS_GHC -Wno-unused-imports #-} +{-# OPTIONS_GHC -Wno-missing-export-lists #-} +module Lang.Crucible.README where + +import What4.Interface +import What4.Expr.App +import What4.BaseTypes +import Lang.Crucible.Backend + +import Lang.Crucible.Types +import Lang.Crucible.CFG.Expr +import Lang.Crucible.CFG.Core hiding (Expr) +import Lang.Crucible.CFG.SSAConversion + +import Lang.Crucible.Simulator.RegValue +import Lang.Crucible.Simulator.RegMap +import Lang.Crucible.Simulator.ExecutionTree +import Lang.Crucible.Simulator.EvalStmt +import Lang.Crucible.Simulator.Evaluation +import Lang.Crucible.Simulator.Intrinsics + + + +-- * Crucible Types + +{- $ +The types of the Crucible language are defined in "Lang.Crucible.Types". +Types are encoded using [singletons](https://github.com/Galoisinc/parameterized-utils?tab=readme-ov-file#parameterized-types-motivation): + +* 'CrucibleType' is the Haskell type-level description of all Crucible types +* 'TypeRepr' are the associated value-level singletons, which + are used when we pass around types, or store them in data structures. +-} + +-- * Crucible Values + +{- $ +The inhabitants of each type are specified via the type function 'RegValue'. +We also have 'RegValue'' which is just a @newtype@ wrapper around 'RegValue', +because in Haskell type families may not be partially applied but @newtype@s can. + +An important subset of the Crucible types are the base types (see 'BaseToType'), +which is for the symbolic expression we can construct +(see 'SymExpr' in [what4](https://github.com/Galoisinc/what4)). +Only these types may contain variables. In practice, we always use @what4@'s +'Expr' type to represent symbolic expressions. + +Also, in some cases we use 'RegEntry' which +is just a pair of a 'RegValue' and its associated 'TypeRepr'. + +There's also 'BaseTerm', which is similar to 'RegEntry' but +for base types---it contains a @what4@'s 'BaseTypeRepr' and a value of the corresponding +base type (usually; the type is parameterized on exactly what we package +with the type). +-} + +-- * Crucible Programs + +{- $ +The program executed by the simulator is in the form of a control flow +graph (CFG). A typical way to construct them is as follows: + + 1. use the functions in "Lang.Crucible.CFG.Generator" to produce a CFG with + assignments ("Lang.Crucible.CFG.Reg") + 2. use 'toSSA' to translate this to a CFG without assignments + ("Lang.Crucible.CFG.Core") + +The core 'CFG' contains basic blocks with 'Stmt's and terminated +by 'TermStmt'. The expression language for the core 'Core.CFG' is +the type 'App'. +-} + +-- * Symbolic Simulator + +{- $ +The state of a running simulator is described in "Lang.Crucible.Simulator.ExecutionTree": + + * 'ExecState' is the current state of execution. + We start with 'InitialState', and keep performing steps until we get + to a 'ResultState'. + * As the simulator executes, it keeps track of its state in 'SimState', + which is stored in the current `ExecState`. + * 'SimContext' is the part of the state that persists across branches + (e.g, after we explore the @then@ part of an @if@ statement, we'll + roll back some of the state changes before simulating the @else@ part, + but the data in 'SimContext's persists). An important part of the + 'SimContext' is the simulator's backend ('_ctxBackend'), which is how the + simulator communicates with a solver, and builds symbolic expressions + ('IsSymBackend'). + + +To evaluate a 'CFG' we evaluate the statements as described in +"Lang.Crucible.Simulator.EvalStmt" (details in 'stepStmt', 'stepTerm'). +Details about expressions evaluation are in 'evalApp' in "Lang.Crucible.Simulator.Evaluation". + +A lot of useful functionality relevant to the simulator can be accessed +from module "Lang.Crucible.Simulator". + +The simulator supports mutable global variables. Our tools use one such +global to store a language specific memory model, which records information +about various memory operations. +-} + +-- * Intrinsics + +{- $ + +Crucible type may be extended using 'IntrinsicType's. An intrinsic type is +a type-level string, which can be given meaning by making an instance of +'IntrinsicClass'. +-} + diff --git a/src/Lang/Crucible/Simulator.hs b/src/Lang/Crucible/Simulator.hs --- a/src/Lang/Crucible/Simulator.hs +++ b/src/Lang/Crucible/Simulator.hs @@ -87,11 +87,14 @@ -- ** SimContext record , IsSymInterfaceProof , SimContext(..) + , ExceptionContextConfig(..) , initSimContext , ctxSymInterface , functionBindings , cruciblePersonality , profilingMetrics + , exceptionContextConfig + , parseExceptionContextConfig -- * SimState , SimState diff --git a/src/Lang/Crucible/Simulator/BoundedExec.hs b/src/Lang/Crucible/Simulator/BoundedExec.hs --- a/src/Lang/Crucible/Simulator/BoundedExec.hs +++ b/src/Lang/Crucible/Simulator/BoundedExec.hs @@ -30,8 +30,8 @@ ( boundedExecFeature ) where -import Control.Lens ( (^.), to, (&), (%~), (.~) ) import Control.Monad ( when ) +import Data.Function ((&)) import Data.IORef import Data.Map (Map) import qualified Data.Map as Map @@ -40,7 +40,7 @@ import qualified Data.Sequence as Seq import qualified Data.Text as Text import Data.Word - +import Lens.Micro ((^.), to, (%~), (.~)) import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.Map as MapF @@ -82,13 +82,13 @@ buildWTOMap = snd . go 0 0 Map.empty where go :: Int -> Int -> Map Int (Int,Int) -> [WTOComponent (Some (BlockID blocks))] -> (Int, Map Int (Int,Int)) - go !x !_ m [] = (x,m) - go !x !d m (Vertex (Some bid) : cs) = + go !x !_ !m [] = (x,m) + go x d m (Vertex (Some bid) : cs) = let m' = Map.insert (Ctx.indexVal (blockIDIndex bid)) (x,d) m - in go (x+1) d m' cs - go !x !d m (SCC scc : cs) = - let m' = viewSome (\hd -> Map.insert (Ctx.indexVal (blockIDIndex hd)) (x,d+1) m) (wtoHead scc) - (x',m'') = go (x+1) (d+1) m' $ wtoComps scc + in go (x + 1) d m' cs + go x d m (SCC scc : cs) = + let m' = viewSome (\hd -> Map.insert (Ctx.indexVal (blockIDIndex hd)) (x,d + 1) m) (wtoHead scc) + (x',m'') = go (x + 1) (d + 1) m' $ wtoComps scc in go x' d m'' cs @@ -100,8 +100,8 @@ incrementBoundCount cs depth = case Seq.lookup depth cs of Just n -> - do let n' = n+1 - let cs' = Seq.update depth n' $ Seq.take (depth+1) cs + do let n' = n + 1 + let cs' = Seq.update depth n' $ Seq.take (depth + 1) cs n' `seq` cs' `seq` (cs', n') Nothing -> do let cs' = cs <> Seq.replicate (depth - Seq.length cs) 0 <> Seq.singleton 1 @@ -183,7 +183,7 @@ Bool {- ^ Produce a proof obligation when resources are exhausted? -} -> IO (GenericExecutionFeature sym) boundedExecFeature getLoopBounds generateSideConditions = - do gvRef <- newIORef (error "Global variable for BoundedExecFrameData not initialized") + do gvRef <- newIORef Nothing return $ GenericExecutionFeature $ onStep gvRef where @@ -202,78 +202,86 @@ } checkBackedge :: - IORef BoundedExecGlobal -> + IORef (Maybe BoundedExecGlobal) -> Some (BlockID blocks) -> BlockID blocks tgt_args -> SymGlobalState sym -> IO (SymGlobalState sym, Maybe Word64) - checkBackedge gvRef (Some bid_curr) bid_tgt globals = - do gv <- readIORef gvRef - case fromMaybe [] (lookupGlobal gv globals) of - ( Right fbd : rest ) -> - do let id_curr = Ctx.indexVal (blockIDIndex bid_curr) - let id_tgt = Ctx.indexVal (blockIDIndex bid_tgt) - let m = frameWtoMap fbd - case (Map.lookup id_curr m, Map.lookup id_tgt m) of - (Just (cx, _cd), Just (tx, td)) | tx <= cx -> - do let cs = frameBoundCounts fbd - let (cs', q) = incrementBoundCount cs td - let fbd' = fbd{ frameBoundCounts = cs' } - let globals' = insertGlobal gv (Right fbd' : rest) globals - if q > frameBoundLimit fbd then - return (globals', Just (frameBoundLimit fbd)) - else - return (globals', Nothing) - - _ -> return (globals, Nothing) - _ -> return (globals, Nothing) + checkBackedge gvRef (Some bid_curr) bid_tgt globals = do + let err = panic "checkBackedge" ["Global not initialized"] + currGv <- readIORef gvRef + let gv = fromMaybe err currGv + case fromMaybe [] (lookupGlobal gv globals) of + (Right fbd : rest) -> do + let id_curr = Ctx.indexVal (blockIDIndex bid_curr) + let id_tgt = Ctx.indexVal (blockIDIndex bid_tgt) + let m = frameWtoMap fbd + case (Map.lookup id_curr m, Map.lookup id_tgt m) of + (Just (cx, _cd), Just (tx, td)) | tx <= cx -> do + let cs = frameBoundCounts fbd + let (cs', q) = incrementBoundCount cs td + let fbd' = fbd{frameBoundCounts = cs'} + let globals' = insertGlobal gv (Right fbd' : rest) globals + if q > frameBoundLimit fbd + then + return (globals', Just (frameBoundLimit fbd)) + else + return (globals', Nothing) + _ -> return (globals, Nothing) + _ -> return (globals, Nothing) modifyStackState :: - IORef BoundedExecGlobal -> + IORef (Maybe BoundedExecGlobal) -> (SimState p sym ext rtp f args -> ExecState p sym ext rtp) -> SimState p sym ext rtp f args -> ([Either FunctionName FrameBoundData] -> [Either FunctionName FrameBoundData]) -> IO (ExecutionFeatureResult p sym ext rtp) - modifyStackState gvRef mkSt st f = - do gv <- readIORef gvRef - let xs = case lookupGlobal gv (st ^. stateGlobals) of - Nothing -> error "bounded execution global not defined!" - Just v -> v - let st' = st & stateGlobals %~ insertGlobal gv (f xs) - return (ExecutionFeatureModifiedState (mkSt st')) + modifyStackState gvRef mkSt st f = do + currGv <- readIORef gvRef + let err = panic "modifyStackState" ["Global variable not initialized"] + let gv = fromMaybe err currGv + let xs = case lookupGlobal gv (st ^. stateGlobals) of + Nothing -> panic "modifyStackState" ["Global variable not defined!"] + Just v -> v + let st' = st & stateGlobals %~ insertGlobal gv (f xs) + return (ExecutionFeatureModifiedState (mkSt st')) onTransition :: - IORef BoundedExecGlobal -> + IORef (Maybe BoundedExecGlobal) -> BlockID blocks tgt_args -> ControlResumption p sym ext rtp (CrucibleLang blocks ret) -> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a) -> IO (ExecutionFeatureResult p sym ext rtp) onTransition gvRef tgt_id res st = stateSolverProof st $ - do let sym = st^.stateSymInterface - let simCtx = st^.stateContext - (globals', overLimit) <- checkBackedge gvRef (st^.stateCrucibleFrame.frameBlockID) tgt_id (st^.stateGlobals) + do let sym = st ^. stateSymInterface + (globals', overLimit) <- checkBackedge gvRef (st ^. stateCrucibleFrame.frameBlockID) tgt_id (st ^. stateGlobals) let st' = st & stateGlobals .~ globals' case overLimit of Just n -> do let msg = "reached maximum number of loop iterations (" ++ show n ++ ")" - let loc = st^.stateCrucibleFrame.to frameProgramLoc + let loc = st ^. stateCrucibleFrame.to frameProgramLoc let err = SimError loc (ResourceExhausted msg) - when generateSideConditions $ withBackend simCtx $ \bak -> + when generateSideConditions $ withStateBackend st $ \bak -> addProofObligation bak (LabeledPred (falsePred sym) err) return (ExecutionFeatureNewState (AbortState (AssertionFailure err) st')) Nothing -> return (ExecutionFeatureModifiedState (ControlTransferState res st')) onStep :: - IORef BoundedExecGlobal -> + IORef (Maybe BoundedExecGlobal) -> ExecState p sym ext rtp -> IO (ExecutionFeatureResult p sym ext rtp) onStep gvRef = \case InitialState simctx globals ah ret cont -> do let halloc = simHandleAllocator simctx - gv <- freshGlobalVar halloc (Text.pack "BoundedExecFrameData") knownRepr - writeIORef gvRef gv - let globals' = insertGlobal gv [Left "_init"] globals + currGv <- readIORef gvRef + ngv <- case currGv of + Nothing -> do + gv <- freshGlobalVar halloc (Text.pack "BoundedExecFrameData") knownRepr + writeIORef gvRef (Just gv) + pure gv + Just gv -> pure gv + let globals' = insertGlobal ngv [Left "_init"] globals let simctx' = simctx{ ctxIntrinsicTypes = MapF.insert (knownSymbol @"BoundedExecFrameData") IntrinsicMuxFn (ctxIntrinsicTypes simctx) } return (ExecutionFeatureModifiedState (InitialState simctx' globals' ah ret cont)) diff --git a/src/Lang/Crucible/Simulator/BoundedRecursion.hs b/src/Lang/Crucible/Simulator/BoundedRecursion.hs --- a/src/Lang/Crucible/Simulator/BoundedRecursion.hs +++ b/src/Lang/Crucible/Simulator/BoundedRecursion.hs @@ -32,13 +32,14 @@ ( boundedRecursionFeature ) where -import Control.Lens ( (^.), (&), (%~) ) import Control.Monad (when) +import Data.Function ((&)) import Data.IORef +import qualified Data.Map.Strict as Map import Data.Maybe import qualified Data.Text as Text import Data.Word -import qualified Data.Map.Strict as Map +import Lens.Micro ((^.), (%~)) import Data.Parameterized.Ctx import qualified Data.Parameterized.Map as MapF @@ -81,56 +82,60 @@ IO (GenericExecutionFeature sym) boundedRecursionFeature getRecursionBound generateSideConditions = - do gvRef <- newIORef (error "Global variable for BoundedRecursionData not initialized") + do gvRef <- newIORef Nothing return $ GenericExecutionFeature $ onStep gvRef where popFrame :: - IORef BoundedRecursionGlobal -> + IORef (Maybe BoundedRecursionGlobal) -> (SimState p sym ext rtp f args -> ExecState p sym ext rtp) -> SimState p sym ext rtp f args -> IO (ExecutionFeatureResult p sym ext rtp) - popFrame gvRef mkSt st = - do gv <- readIORef gvRef - case lookupGlobal gv (st ^. stateGlobals) of - Nothing -> panic "bounded recursion" ["global not defined!"] - Just [] -> panic "bounded recursion" ["pop on empty stack!"] - Just (_:xs) -> - do let st' = st & stateGlobals %~ insertGlobal gv xs - return (ExecutionFeatureModifiedState (mkSt st')) + popFrame gvRef mkSt st = do + currGv <- readIORef gvRef + let err = panic "bounded recursion" ["gv not initialized"] + let gv = fromMaybe err currGv + case lookupGlobal gv (st ^. stateGlobals) of + Nothing -> panic "bounded recursion" ["global not defined!"] + Just [] -> panic "bounded recursion" ["pop on empty stack!"] + Just (_ : xs) -> do + let st' = st & stateGlobals %~ insertGlobal gv xs + return (ExecutionFeatureModifiedState (mkSt st')) pushFrame :: - IORef BoundedRecursionGlobal -> + IORef (Maybe BoundedRecursionGlobal) -> (BoundedRecursionMap -> BoundedRecursionMap -> [BoundedRecursionMap] -> [BoundedRecursionMap]) -> SomeHandle -> (SimState p sym ext rtp f args -> ExecState p sym ext rtp) -> SimState p sym ext rtp f args -> IO (ExecutionFeatureResult p sym ext rtp) pushFrame gvRef rebuildStack h mkSt st = stateSolverProof st $ - do let sym = st^.stateSymInterface - let simCtx = st^.stateContext - gv <- readIORef gvRef + do let sym = st ^. stateSymInterface + currGv <- readIORef gvRef + let err = panic "pushFrame" ["Uninitialized global!"] + let gv = fromMaybe err currGv case lookupGlobal gv (st ^. stateGlobals) of Nothing -> panic "bounded recursion" ["global not defined!"] Just [] -> panic "bounded recursion" ["empty stack!"] - Just (x:xs) -> - do mb <- getRecursionBound h - let v = 1 + fromMaybe 0 (Map.lookup h x) - case mb of - Just b | v > b -> - do loc <- getCurrentProgramLoc sym - let msg = ("reached maximum number of recursive calls to function " ++ show h ++ " (" ++ show b ++ ")") - let err = SimError loc (ResourceExhausted msg) - when generateSideConditions $ withBackend simCtx $ \bak -> - addProofObligation bak (LabeledPred (falsePred sym) err) - return (ExecutionFeatureNewState (AbortState (AssertionFailure err) st)) - _ -> - do let x' = Map.insert h v x - let st' = st & stateGlobals %~ insertGlobal gv (rebuildStack x' x xs) - x' `seq` return (ExecutionFeatureModifiedState (mkSt st')) + Just (x:xs) -> do + mb <- getRecursionBound h + let v = 1 + fromMaybe 0 (Map.lookup h x) + case mb of + Just b | v > b -> do + loc <- getCurrentProgramLoc sym + let msg = ("reached maximum number of recursive calls to function " ++ show h ++ " (" ++ show b ++ ")") + let simerr = SimError loc (ResourceExhausted msg) + when generateSideConditions $ withStateBackend st $ \bak -> + addProofObligation bak (LabeledPred (falsePred sym) simerr) + return (ExecutionFeatureNewState (AbortState (AssertionFailure simerr) st)) + _ -> do + let x' = Map.insert h v x + let st' = st & stateGlobals %~ insertGlobal gv (rebuildStack x' x xs) + x' `seq` return (ExecutionFeatureModifiedState (mkSt st')) + onStep :: - IORef BoundedRecursionGlobal -> + IORef (Maybe BoundedRecursionGlobal) -> ExecState p sym ext rtp -> IO (ExecutionFeatureResult p sym ext rtp) @@ -138,8 +143,13 @@ InitialState simctx globals ah ret cont -> do let halloc = simHandleAllocator simctx - gv <- freshGlobalVar halloc (Text.pack "BoundedRecursionData") knownRepr - writeIORef gvRef gv + currGv <- readIORef gvRef + gv <- case currGv of + Just gv -> pure gv + Nothing -> do + gv <- freshGlobalVar halloc (Text.pack "BoundedRecursionData") knownRepr + writeIORef gvRef (Just gv) + pure gv let simctx' = simctx{ ctxIntrinsicTypes = MapF.insert (knownSymbol @"BoundedRecursionData") IntrinsicMuxFn diff --git a/src/Lang/Crucible/Simulator/Breakpoint.hs b/src/Lang/Crucible/Simulator/Breakpoint.hs deleted file mode 100644 --- a/src/Lang/Crucible/Simulator/Breakpoint.hs +++ /dev/null @@ -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 --- 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 diff --git a/src/Lang/Crucible/Simulator/CallFrame.hs b/src/Lang/Crucible/Simulator/CallFrame.hs --- a/src/Lang/Crucible/Simulator/CallFrame.hs +++ b/src/Lang/Crucible/Simulator/CallFrame.hs @@ -38,7 +38,7 @@ , framePostdom , frameProgramLoc , setFrameBlock - , setFrameBreakpointPostdomInfo + , setFrameCutpointPostdomInfo , extendFrame , updateFrame , mergeCallFrame @@ -58,15 +58,17 @@ , fromCallFrame , fromReturnFrame , frameFunctionName + , frameStackLoc ) where -import Control.Lens +import Data.Functor.Const (getConst) import Data.Kind import qualified Data.Parameterized.Context as Ctx +import Lens.Micro ((^.), Lens', Lens, SimpleGetter, lens, to) import What4.FunctionName import What4.Interface ( Pred ) -import What4.ProgramLoc ( ProgramLoc ) +import What4.ProgramLoc ( ProgramLoc, mkProgramLoc, Position(..) ) import Lang.Crucible.Analysis.Postdom import Lang.Crucible.CFG.Core @@ -129,22 +131,22 @@ frameReturnType :: CallFrame sym ext blocks ret ctx -> TypeRepr ret frameReturnType CallFrame { _frameCFG = g } = cfgReturnType g -framePostdomMap :: Simple Lens (CallFrame sym ext blocks ret ctx) (CFGPostdom blocks) +framePostdomMap :: Lens' (CallFrame sym ext blocks ret ctx) (CFGPostdom blocks) framePostdomMap = lens _framePostdomMap (\s x -> s{ _framePostdomMap = x }) -frameBlockID :: Simple Lens (CallFrame sym ext blocks ret ctx) (Some (BlockID blocks)) +frameBlockID :: Lens' (CallFrame sym ext blocks ret ctx) (Some (BlockID blocks)) frameBlockID = lens _frameBlockID (\s v -> s { _frameBlockID = v }) -- | List of statements to execute next. -frameStmts :: Simple Lens (CallFrame sym ext blocks ret ctx) (StmtSeq ext blocks ret ctx) +frameStmts :: Lens' (CallFrame sym ext blocks ret ctx) (StmtSeq ext blocks ret ctx) frameStmts = lens _frameStmts (\s v -> s { _frameStmts = v }) {-# INLINE frameStmts #-} -frameRegs :: Simple Lens (CallFrame sym ext blocks ret args) (RegMap sym args) +frameRegs :: Lens' (CallFrame sym ext blocks ret args) (RegMap sym args) frameRegs = lens _frameRegs (\s v -> s { _frameRegs = v }) -- | List of statements to execute next. -framePostdom :: Simple Lens (CallFrame sym ext blocks ret ctx) (Some (CrucibleBranchTarget (CrucibleLang blocks ret))) +framePostdom :: Lens' (CallFrame sym ext blocks ret ctx) (Some (CrucibleBranchTarget (CrucibleLang blocks ret))) framePostdom = lens _framePostdom (\s v -> s { _framePostdom = v }) -- | Create a new call frame. @@ -171,7 +173,7 @@ , _framePostdomMap = pdInfo , _frameBlockID = Some bid , _frameRegs = args - , _frameStmts = b^.blockStmts + , _frameStmts = b ^. blockStmts , _framePostdom = mkFramePostdom pds } @@ -182,7 +184,7 @@ -- | Return program location associated with frame. frameProgramLoc :: CallFrame sym ext blocks ret ctx -> ProgramLoc -frameProgramLoc cf = firstStmtLoc (cf^.frameStmts) +frameProgramLoc cf = firstStmtLoc (cf ^. frameStmts) setFrameBlock :: BlockID blocks args -> RegMap sym args @@ -190,20 +192,20 @@ -> CallFrame sym ext blocks ret args setFrameBlock bid@(BlockID block_id) args f = f' where b = frameBlockMap f Ctx.! block_id - pds = getConst $ (f^.framePostdomMap.ixF block_id) + pds = getConst $ (f ^. framePostdomMap.ixF block_id) f' = f { _frameBlockID = Some bid , _frameRegs = args - , _frameStmts = b^.blockStmts + , _frameStmts = b ^. blockStmts , _framePostdom = mkFramePostdom pds } -setFrameBreakpointPostdomInfo :: - [BreakpointName] -> +setFrameCutpointPostdomInfo :: + [CutpointName] -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret ctx -setFrameBreakpointPostdomInfo breakpoints f = case f of +setFrameCutpointPostdomInfo cutpoints f = case f of CallFrame{ _frameCFG = g, _frameBlockID = Some (BlockID block_id) } -> do - let pdInfo = breakpointPostdomInfo g breakpoints + let pdInfo = cutpointPostdomInfo g cutpoints f { _framePostdomMap = pdInfo , _framePostdom = mkFramePostdom (getConst $ pdInfo Ctx.! block_id) } @@ -257,10 +259,10 @@ -- ^ Arguments to override. } -override :: Simple Lens (OverrideFrame sym ret args) FunctionName +override :: Lens' (OverrideFrame sym ret args) FunctionName override = lens _override (\o x -> o{ _override = x }) -overrideHandle :: Simple Lens (OverrideFrame sym ret args) SomeHandle +overrideHandle :: Lens' (OverrideFrame sym ret args) SomeHandle overrideHandle = lens _overrideHandle (\o x -> o { _overrideHandle = x }) overrideRegMap :: Lens (OverrideFrame sym ret args) (OverrideFrame sym ret args') @@ -281,7 +283,13 @@ FrameRetType (CrucibleLang b r) = r FrameRetType (OverrideLang r) = r -data SimFrame sym ext l (args :: Maybe (Ctx CrucibleType)) where +-- | A frame on the stack. +-- +-- Type parameters: +-- +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +-- - @args@: arguments; 'Just' for call frames, 'Nothing' for a return frame +data SimFrame sym ext f (args :: Maybe (Ctx CrucibleType)) where -- | Custom code to execute, typically for "overrides" OF :: !(OverrideFrame sym ret args) -> SimFrame sym ext (OverrideLang ret) ('Just args) @@ -317,8 +325,16 @@ -> RegEntry sym (FrameRetType f) fromReturnFrame (RF _ x) = x -frameFunctionName :: Getter (SimFrame sym ext f a) FunctionName +frameFunctionName :: SimpleGetter (SimFrame sym ext f a) FunctionName frameFunctionName = to $ \case - OF f -> f^.override + OF f -> f ^. override MF f -> case frameHandle f of SomeHandle h -> handleName h RF n _ -> n + +-- | Get a location for a stack frame, or Nothing if this is a return frame +frameStackLoc :: (SimFrame sym ext f a) -> Maybe ProgramLoc +frameStackLoc frame = + case frame of + sf@(OF _) -> Just $ mkProgramLoc (sf ^. frameFunctionName) InternalPos + (MF f) -> Just $ frameProgramLoc f + (RF _ _) -> Nothing diff --git a/src/Lang/Crucible/Simulator/Cut.hs b/src/Lang/Crucible/Simulator/Cut.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Simulator/Cut.hs @@ -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 +-- 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 diff --git a/src/Lang/Crucible/Simulator/EvalStmt.hs b/src/Lang/Crucible/Simulator/EvalStmt.hs --- a/src/Lang/Crucible/Simulator/EvalStmt.hs +++ b/src/Lang/Crucible/Simulator/EvalStmt.hs @@ -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 -> diff --git a/src/Lang/Crucible/Simulator/Evaluation.hs b/src/Lang/Crucible/Simulator/Evaluation.hs --- a/src/Lang/Crucible/Simulator/Evaluation.hs +++ b/src/Lang/Crucible/Simulator/Evaluation.hs @@ -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 diff --git a/src/Lang/Crucible/Simulator/ExecutionTree.hs b/src/Lang/Crucible/Simulator/ExecutionTree.hs --- a/src/Lang/Crucible/Simulator/ExecutionTree.hs +++ b/src/Lang/Crucible/Simulator/ExecutionTree.hs @@ -30,6 +30,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fprint-explicit-kinds -Wall #-} @@ -68,8 +69,12 @@ , ResolvedCall(..) , resolvedCallHandle , execResultContext + , setExecResultContext , execStateContext + , setExecStateContext , execStateSimState + , execResultGlobals + , execStateGlobals -- * Simulator context trees -- ** Main context data structures @@ -111,12 +116,16 @@ , IsSymInterfaceProof , SimContext(..) , Metric(..) + , ExceptionContextConfig(..) , initSimContext , withBackend + , withStateBackend , ctxSymInterface , functionBindings , cruciblePersonality , profilingMetrics + , exceptionContextConfig + , parseExceptionContextConfig -- * SimState , SimState(..) @@ -138,18 +147,22 @@ , stateOverrideFrame , stateGlobals , stateConfiguration + , stateProgramStack ) where -import Control.Lens import Control.Monad.Reader +import Data.Function ((&)) import Data.Kind import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map +import Data.Maybe(maybeToList) import Data.Parameterized.Ctx import qualified Data.Parameterized.Context as Ctx import Data.Text (Text) +import Lens.Micro ((^.), (.~), Lens', Lens, SimpleGetter, Traversal', lens, to) import System.Exit (ExitCode) import System.IO +import Text.Read(readMaybe) import qualified Prettyprinter as PP import What4.Config (Config) @@ -169,13 +182,20 @@ import Lang.Crucible.Simulator.GlobalState (SymGlobalState) import Lang.Crucible.Simulator.Intrinsics (IntrinsicTypes) import Lang.Crucible.Simulator.RegMap (RegMap, emptyRegMap, RegValue, RegEntry) +import Lang.Crucible.Simulator.SimError(ProgramStack(..)) import Lang.Crucible.Types ------------------------------------------------------------------------ -- GlobalPair --- | A value of some type 'v' together with a global state. -data GlobalPair sym (v :: Type) = +-- | A value of some type @v@ together with a global state. +-- +-- Type parameters: +-- +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @v@: type of the value +type GlobalPair :: Type -> Type -> Type +data GlobalPair sym v = GlobalPair { _gpValue :: !v , _gpGlobals :: !(SymGlobalState sym) @@ -186,7 +206,7 @@ gpValue = lens _gpValue (\s v -> s { _gpValue = v }) -- | Access the globals stored in the global pair. -gpGlobals :: Simple Lens (GlobalPair sym u) (SymGlobalState sym) +gpGlobals :: Lens' (GlobalPair sym u) (SymGlobalState sym) gpGlobals = lens _gpGlobals (\s v -> s { _gpGlobals = v }) @@ -194,7 +214,15 @@ -- TopFrame -- | The currently-executing frame plus the global state associated with it. -type TopFrame sym ext f a = GlobalPair sym (SimFrame sym ext f a) +-- +-- Type parameters: +-- +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +-- - @args@: arguments to this frame (see 'SimFrame') +type TopFrame :: Type -> Type -> Type -> Maybe (Ctx CrucibleType) -> Type +type TopFrame sym ext f args = GlobalPair sym (SimFrame sym ext f args) -- | Access the Crucible call frame inside a 'TopFrame'. crucibleTopFrame :: @@ -222,6 +250,12 @@ -- path might abort because it became infeasible (inconsistent path -- conditions), because the program called an exit primitive, or -- because of a true error condition (e.g., a failed assertion). +-- +-- Type parameters: +-- +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +type AbortedResult :: Type -> Type -> Type data AbortedResult sym ext where -- | A single aborted execution with the execution state at time of the abort and the reason. AbortedExec :: @@ -229,9 +263,10 @@ !(GlobalPair sym (SimFrame sym ext l args)) -> AbortedResult sym ext - -- | An aborted execution that was ended by a call to 'exit'. + -- | An aborted execution that was ended by a call to @exit@. AbortedExit :: !ExitCode -> + !(GlobalPair sym (SimFrame sym ext l args)) -> AbortedResult sym ext -- | Two separate threads of execution aborted after a symbolic branch, @@ -248,7 +283,10 @@ -- | This represents an execution frame where its frame type -- and arguments have been hidden. -data SomeFrame (f :: fk -> argk -> Type) = forall l a . SomeFrame !(f l a) +-- +-- The type parameter @f@ is usually 'SimFrame'. +type SomeFrame :: forall fk argk. (fk -> argk -> Type) -> Type +data SomeFrame f = forall l a . SomeFrame !(f l a) -- | Return the program locations of all the Crucible frames. filterCrucibleFrames :: SomeFrame (SimFrame sym ext) -> Maybe ProgramLoc @@ -256,11 +294,13 @@ filterCrucibleFrames _ = Nothing -- | Iterate over frames in the result. -arFrames :: Simple Traversal (AbortedResult sym ext) (SomeFrame (SimFrame sym ext)) +arFrames :: Traversal' (AbortedResult sym ext) (SomeFrame (SimFrame sym ext)) arFrames h (AbortedExec e p) = (\(SomeFrame f') -> AbortedExec e (p & gpValue .~ f')) - <$> h (SomeFrame (p^.gpValue)) -arFrames _ (AbortedExit ec) = pure (AbortedExit ec) + <$> h (SomeFrame (p ^. gpValue)) +arFrames h (AbortedExit ec p) = + (\(SomeFrame f') -> AbortedExit ec (p & gpValue .~ f')) + <$> h (SomeFrame (p ^. gpValue)) arFrames h (AbortedBranch predicate loc r s) = AbortedBranch predicate loc <$> arFrames h r <*> arFrames h s @@ -272,7 +312,7 @@ where pp :: SomeFrame (SimFrame sym ext) -> PP.Doc ann pp (SomeFrame (OF f)) = - PP.pretty "When calling" PP.<+> PP.viaShow (f^.override) + PP.pretty "When calling" PP.<+> PP.viaShow (f ^. override) pp (SomeFrame (MF f)) = PP.pretty "In" PP.<+> PP.viaShow (frameHandle f) PP.<+> PP.pretty "at" PP.<+> PP.pretty (plSourceLoc (frameProgramLoc f)) @@ -289,7 +329,14 @@ -- 'PartialResult', then some of the computation paths that led to -- this result aborted for some reason, and the resulting value is -- only defined if the associated condition is true. -data PartialResult sym ext (v :: Type) +-- +-- Type parameters: +-- +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @v@: Type of the result of the computation +type PartialResult :: Type -> Type -> Type -> Type +data PartialResult sym ext v {- | A 'TotalRes' indicates that the the global pair is always defined. -} = TotalRes !(GlobalPair sym v) @@ -318,6 +365,14 @@ {-# INLINE partialValue #-} -- | The result of resolving a function call. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @ret@: 'CrucibleType' of the return value +type ResolvedCall :: Type -> Type -> Type -> CrucibleType -> Type data ResolvedCall p sym ext ret where -- | A resolved function call to an override. OverrideCall :: @@ -341,15 +396,23 @@ -- | Executions that have completed either due to (partial or total) -- successful completion or by some abort condition. -data ExecResult p sym ext (r :: Type) +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +type ExecResult :: Type -> Type -> Type -> Type -> Type +data ExecResult p sym ext rtp = -- | At least one execution path resulted in some return result. - FinishedResult !(SimContext p sym ext) !(PartialResult sym ext r) + FinishedResult !(SimContext p sym ext) !(PartialResult sym ext rtp) -- | All execution paths resulted in an abort condition, and there is -- no result to return. | AbortedResult !(SimContext p sym ext) !(AbortedResult sym ext) -- | An execution stopped somewhere in the middle of a run because -- a timeout condition occurred. - | TimeoutResult !(ExecState p sym ext r) + | TimeoutResult !(ExecState p sym ext rtp) execResultContext :: ExecResult p sym ext r -> SimContext p sym ext @@ -357,21 +420,49 @@ execResultContext (AbortedResult ctx _) = ctx execResultContext (TimeoutResult exst) = execStateContext exst +setExecResultContext :: + SimContext p sym ext -> + ExecResult p sym ext r -> + ExecResult p sym ext r +setExecResultContext ctx = + \case + FinishedResult _ x -> FinishedResult ctx x + AbortedResult _ x -> AbortedResult ctx x + TimeoutResult execState -> TimeoutResult (setExecStateContext ctx execState) + execStateContext :: ExecState p sym ext r -> SimContext p sym ext execStateContext = \case ResultState res -> execResultContext res - AbortState _ st -> st^.stateContext - UnwindCallState _ _ st -> st^.stateContext - CallState _ _ st -> st^.stateContext - TailCallState _ _ st -> st^.stateContext - ReturnState _ _ _ st -> st^.stateContext - ControlTransferState _ st -> st^.stateContext - RunningState _ st -> st^.stateContext - SymbolicBranchState _ _ _ _ st -> st^.stateContext - OverrideState _ st -> st^.stateContext - BranchMergeState _ st -> st^.stateContext + AbortState _ st -> st ^. stateContext + UnwindCallState _ _ st -> st ^. stateContext + CallState _ _ st -> st ^. stateContext + TailCallState _ _ st -> st ^. stateContext + ReturnState _ _ _ st -> st ^. stateContext + ControlTransferState _ st -> st ^. stateContext + RunningState _ st -> st ^. stateContext + SymbolicBranchState _ _ _ _ st -> st ^. stateContext + OverrideState _ st -> st ^. stateContext + BranchMergeState _ st -> st ^. stateContext InitialState stctx _ _ _ _ -> stctx +setExecStateContext :: + SimContext p sym ext -> + ExecState p sym ext r -> + ExecState p sym ext r +setExecStateContext ctx = \case + ResultState res -> ResultState (setExecResultContext ctx res) + AbortState x st -> AbortState x (st & stateContext .~ ctx) + UnwindCallState x y st -> UnwindCallState x y (st & stateContext .~ ctx) + CallState x y st -> CallState x y (st & stateContext .~ ctx) + TailCallState x y st -> TailCallState x y (st & stateContext .~ ctx) + ReturnState x y z st -> ReturnState x y z (st & stateContext .~ ctx) + ControlTransferState x st -> ControlTransferState x (st & stateContext .~ ctx) + RunningState x st -> RunningState x (st & stateContext .~ ctx) + SymbolicBranchState u v x y st -> SymbolicBranchState u v x y (st & stateContext .~ ctx) + OverrideState x st -> OverrideState x (st & stateContext .~ ctx) + BranchMergeState x st -> BranchMergeState x (st & stateContext .~ ctx) + InitialState _ u v x y -> InitialState ctx u v x y + execStateSimState :: ExecState p sym ext r -> Maybe (SomeSimState p sym ext r) execStateSimState = \case @@ -388,6 +479,72 @@ BranchMergeState _ st -> Just (SomeSimState st) InitialState _ _ _ _ _ -> Nothing +abortedGlobals :: + Monad f => + -- | How to handle branches (e.g., 'AbortedBranch', 'PartialRes'). + -- + -- Common options include concretizing the 'Pred' or returning a partial + -- result (e.g., 'Nothing'). + (ProgramLoc -> Pred sym -> SymGlobalState sym -> SymGlobalState sym -> f (SymGlobalState sym)) -> + AbortedResult sym ext -> + f (SymGlobalState sym) +abortedGlobals handleBranch = + \case + AbortedExec _ gp -> pure (gp ^. gpGlobals) + AbortedExit _ gp -> pure (gp ^. gpGlobals) + AbortedBranch loc p rl rr -> do + l <- abortedGlobals handleBranch rl + r <- abortedGlobals handleBranch rr + handleBranch loc p l r + +-- | Extract the 'SymGlobalState' from an 'ExecResult'. +execResultGlobals :: + Monad f => + -- | How to handle branches (e.g., 'AbortedBranch', 'PartialRes'). + -- + -- Common options include concretizing the 'Pred' or returning a partial + -- result (e.g., 'Nothing'). + (SimContext p sym ext -> ProgramLoc -> Pred sym -> SymGlobalState sym -> SymGlobalState sym -> f (SymGlobalState sym)) -> + ExecResult p sym ext rtp -> + f (SymGlobalState sym) +execResultGlobals handleBranch = + \case + FinishedResult simCtx partial -> + case partial of + TotalRes gp -> pure (gp ^. gpGlobals) + PartialRes loc p gp aborted -> do + let l = gp ^. gpGlobals + r <- abortedGlobals (handleBranch simCtx) aborted + handleBranch simCtx loc p l r + TimeoutResult st -> execStateGlobals handleBranch st + AbortedResult simCtx aborted -> + abortedGlobals (handleBranch simCtx) aborted + +-- | Extract the 'SymGlobalState' from an 'ExecState'. +execStateGlobals :: + Monad f => + -- | How to handle branches (e.g., 'AbortedBranch', 'PartialRes'). + -- + -- Common options include concretizing the 'Pred' or returning a partial + -- result (e.g., 'Nothing'). + (SimContext p sym ext -> ProgramLoc -> Pred sym -> SymGlobalState sym -> SymGlobalState sym -> f (SymGlobalState sym)) -> + ExecState p sym ext rtp -> + f (SymGlobalState sym) +execStateGlobals handleBranch = + \case + AbortState _ st -> pure (st ^. stateGlobals) + BranchMergeState _ st -> pure (st ^. stateGlobals) + CallState _ _ st -> pure (st ^. stateGlobals) + ControlTransferState _ st -> pure (st ^. stateGlobals) + InitialState _ globState _ _ _ -> pure globState + OverrideState _ st -> pure (st ^. stateGlobals) + ResultState r -> execResultGlobals handleBranch r + ReturnState _ _ _ st -> pure (st ^. stateGlobals) + RunningState _ st -> pure (st ^. stateGlobals) + SymbolicBranchState _ _ _ _ st -> pure (st ^. stateGlobals) + TailCallState _ _ st -> pure (st ^. stateGlobals) + UnwindCallState _ _ st -> pure (st ^. stateGlobals) + ----------------------------------------------------------------------- -- ExecState @@ -395,7 +552,15 @@ -- Crucible program. The Crucible simulator executes by transitioning -- between these different states until it results in a 'ResultState', -- indicating the program has completed. -data ExecState p sym ext (rtp :: Type) +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +type ExecState :: Type -> Type -> Type -> Type -> Type +data ExecState p sym ext rtp {- | The 'ResultState' is used to indicate that the program has completed. -} = ResultState !(ExecResult p sym ext rtp) @@ -532,11 +697,27 @@ -- | An action which will construct an 'ExecState' given a current -- 'SimState'. Such continuations correspond to a single transition -- of the simulator transition system. -type ExecCont p sym ext r f a = - ReaderT (SimState p sym ext r f a) IO (ExecState p sym ext r) +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +-- - @args@: arguments to the current frame (see 'SimFrame') +type ExecCont :: Type -> Type -> Type -> Type -> Type -> Maybe (Ctx.Ctx CrucibleType) -> Type +type ExecCont p sym ext rtp f args = + ReaderT (SimState p sym ext rtp f args) IO (ExecState p sym ext rtp) -- | Some additional information attached to a @RunningState@ -- that indicates how we got to this running state. +-- +-- Type parameters: +-- +-- - @blocks@: types of variables in scope from previous blocks +-- - @args@: arguments to this block +type RunningStateInfo :: Ctx (Ctx CrucibleType) -> Ctx CrucibleType -> Type data RunningStateInfo blocks args -- | This indicates that we are now in a @RunningState@ because -- we transferred execution to the start of a basic block. @@ -554,6 +735,12 @@ -- | A 'ResolvedJump' is a block label together with a collection of -- actual arguments that are expected by that block. These data -- are sufficient to actually transfer control to the named label. +-- +-- Type parameters: +-- +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @blocks@: types of variables in scope from previous blocks +type ResolvedJump :: Type -> Ctx (Ctx CrucibleType) -> Type data ResolvedJump sym blocks = forall args. ResolvedJump @@ -564,6 +751,15 @@ -- (while it first explores other paths), a 'ControlResumption' -- indicates what actions must later be taken in order to resume -- execution of that path. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +type ControlResumption :: Type -> Type -> Type -> Type -> Type -> Type data ControlResumption p sym ext rtp f where {- | When resuming a paused frame with a @ContinueResumption@, no special work needs to be done, simply begin executing @@ -603,6 +799,15 @@ -- while other paths are explored. It consists of a (potentially partial) -- 'SimFrame' together with some information about how to resume execution -- of that frame. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +type PausedFrame :: Type -> Type -> Type -> Type -> Type -> Type data PausedFrame p sym ext rtp f = forall old_args. PausedFrame @@ -619,6 +824,16 @@ -- stored in the 'VFFCompletePath' state until the second path also -- reaches its merge point. The two paths will then be merged, -- and execution will continue beyond the merge point. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +-- - @args@: arguments to this frame (see 'SimFrame') +type VFFOtherPath :: Type -> Type -> Type -> Type -> Type -> Maybe (Ctx CrucibleType) -> Type data VFFOtherPath p sym ext ret f args {- | This corresponds the a path that still needs to be analyzed. -} @@ -639,20 +854,17 @@ of the branching structure of a program. The 'ValueFromFrame' states correspond to the structure of symbolic branching that occurs within a single function call. -The type parameters have the following meanings: - - * @p@ is the personality of the simulator (i.e., custom user state). - - * @sym@ is the simulator backend being used. - - * @ext@ specifies what extensions to the Crucible language are enabled - - * @ret@ is the global return type of the entire execution. +Type parameters: - * @f@ is the type of the top frame. +- @p@: see 'cruciblePersonality' +- @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +- @ext@: language extension, see "Lang.Crucible.CFG.Extension" +- @ret@: global return type of the entire execution +- @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') -} -data ValueFromFrame p sym ext (ret :: Type) (f :: Type) +type ValueFromFrame :: Type -> Type -> Type -> Type -> Type -> Type +data ValueFromFrame p sym ext ret f {- | We are working on a branch; this could be the first or the second of both branches (see the 'VFFOtherPath' field). -} @@ -715,6 +927,7 @@ -- occur or not. If the context sill expects a merge, we need to -- take some actions to indicate that the merge will not occur; -- otherwise there is no special work to be done. +type PendingPartialMerges :: Type data PendingPartialMerges = {- | Don't indicate an abort condition in the context -} NoNeedToAbort @@ -728,19 +941,14 @@ of the branching structure of a program. The 'ValueFromValue' states correspond to stack call frames in a more traditional simulator environment. -The type parameters have the following meanings: - - * @p@ is the personality of the simulator (i.e., custom user state). - - * @sym@ is the simulator backend being used. - - * @ext@ specifies what extensions to the Crucible language are enabled - - * @ret@ is the global return type of the entire computation - - * @top_return@ is the return type of the top-most call on the stack. +- @p@: see 'cruciblePersonality' +- @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +- @ext@: language extension, see "Lang.Crucible.CFG.Extension" +- @ret@: global return type of the entire execution +- @top_return@: return type of the top-most call on the stack. -} -data ValueFromValue p sym ext (ret :: Type) (top_return :: CrucibleType) +type ValueFromValue :: Type -> Type -> Type -> Type -> CrucibleType -> Type +data ValueFromValue p sym ext ret top_return {- | 'VFVCall' denotes a call site in the outer context, and represents the point to which a function higher on the stack will @@ -851,23 +1059,18 @@ executing in a caller's context once a function call has completed and the return value is available. -The type parameters have the following meanings: - - * @ret@ is the type of the return value that is expected. - - * @p@ is the personality of the simulator (i.e., custom user state). - - * @sym@ is the simulator backend being used. - - * @ext@ specifies what extensions to the Crucible language are enabled. - - * @root@ is the global return type of the entire computation. - - * @f@ is the stack type of the caller. +Type parameters: - * @args@ is the type of the local variables in scope prior to the call. +- @ret@: the type of the return value that is expected +- @p@: see 'cruciblePersonality' +- @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +- @ext@: language extension, see "Lang.Crucible.CFG.Extension" +- @root@: global return type of the entire computation +- @f@: the frame type of the caller ('CrucibleLang' or 'OverrideLang') +- @args@: types of the local variables in scope prior to the call (see 'SimFrame') -} -data ReturnHandler (ret :: CrucibleType) p sym ext root f args where +type ReturnHandler :: CrucibleType -> Type -> Type -> Type -> Type -> Type -> Maybe (Ctx CrucibleType) -> Type +data ReturnHandler ret p sym ext root f args where {- | The 'ReturnToOverride' constructor indicates that the calling context is primitive code written directly in Haskell. -} @@ -899,13 +1102,25 @@ ------------------------------------------------------------------------ -- ActiveTree +type PartialResultFrame :: Type -> Type -> Type -> Maybe (Ctx CrucibleType) -> Type type PartialResultFrame sym ext f args = PartialResult sym ext (SimFrame sym ext f args) {- | An active execution tree contains at least one active execution. The data structure is organized so that the current execution - can be accessed rapidly. -} -data ActiveTree p sym ext root (f :: Type) args + can be accessed rapidly. + + Type parameters: + + - @p@: see 'cruciblePersonality' + - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' + - @ext@: language extension, see "Lang.Crucible.CFG.Extension" + - @root@: global return type of the entire computation + - @f@: the frame type of the caller ('CrucibleLang' or 'OverrideLang') +-- - @args@: arguments to the current frame (see 'SimFrame') +-} +type ActiveTree :: Type -> Type -> Type -> Type -> Type -> Maybe (Ctx.Ctx CrucibleType) -> Type +data ActiveTree p sym ext root f args = ActiveTree { _actContext :: !(ValueFromFrame p sym ext root f) , _actResult :: !(PartialResultFrame sym ext f args) @@ -953,13 +1168,22 @@ activeFrames :: ActiveTree ctx sym ext root a args -> [SomeFrame (SimFrame sym ext)] activeFrames (ActiveTree ctx ar) = - SomeFrame (ar^.partialValue^.gpValue) : parentFrames ctx + SomeFrame (ar ^. partialValue ^. gpValue) : parentFrames ctx ------------------------------------------------------------------------ -- SimContext -- | A definition of a function's semantics, given as a Haskell action. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @args@: types of arguments to the override +-- - @ret@: return type of the override +type Override :: Type -> Type -> Type -> Ctx CrucibleType -> CrucibleType -> Type data Override p sym ext (args :: Ctx CrucibleType) ret = Override { overrideName :: FunctionName , overrideHandler :: forall r. ExecCont p sym ext r (OverrideLang ret) ('Just args) @@ -968,16 +1192,39 @@ -- | State used to indicate what to do when function is called. A function -- may either be defined by writing a Haskell 'Override' or by giving -- a Crucible control-flow graph representation. -data FnState p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType) +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @args@: argument types +-- - @ret@: return type +type FnState :: Type -> Type -> Type -> Ctx CrucibleType -> CrucibleType -> Type +data FnState p sym ext args ret = UseOverride !(Override p sym ext args ret) | forall blocks . UseCFG !(CFG ext blocks args ret) !(CFGPostdom blocks) -- | A map from function handles to their semantics. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +type FunctionBindings :: Type -> Type -> Type -> Type newtype FunctionBindings p sym ext = FnBindings { fnBindings :: FnHandleMap (FnState p sym ext) } -- | The type of functions that interpret extension statements. These -- have access to the main simulator state, and can make fairly arbitrary -- changes to it. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +type EvalStmtFunc :: Type -> Type -> Type -> Type type EvalStmtFunc p sym ext = forall rtp blocks r ctx tp'. StmtExtension ext (RegEntry sym) tp' -> @@ -987,6 +1234,13 @@ -- | In order to start executing a simulator, one must provide an implementation -- of the extension syntax. This includes an evaluator for the added -- expression forms, and an evaluator for the added statement forms. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +type ExtensionImpl :: Type -> Type -> Type -> Type data ExtensionImpl p sym ext = ExtensionImpl { extensionEval :: @@ -1010,30 +1264,66 @@ , extensionExec = \case } +type IsSymInterfaceProof :: Type -> Type -> Type type IsSymInterfaceProof sym a = (IsSymInterface sym => a) -> a +-- | Some kind of 'Integer' to be collected during execution. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +type Metric :: Type -> Type -> Type -> Type newtype Metric p sym ext = Metric { runMetric :: forall rtp f args. SimState p sym ext rtp f args -> IO Integer } +data ExceptionContextConfig = + ECCNone -- ^ do not include exceptions with context + | ECCLimited Int + | ECCNoLimit + deriving(Eq, Ord, Show, Read) + +parseExceptionContextConfig :: String -> Either String ExceptionContextConfig +parseExceptionContextConfig s = + case s of + "none" -> Right ECCNone + "nolimit" -> Right ECCNoLimit + _ | Just limit <- readMaybe s -> + if limit > 0 + then Right (ECCLimited limit) + else Left "exception context frame limit cannot be 0 or less" + _ -> Left "invalid exception context config - valid inputs are `none`, `nolimit`, and integers greater than 0" + + -- | Top-level state record for the simulator. The state contained in this record -- remains persistent across all symbolic simulator actions. In particular, it -- is not rolled back when the simulator returns previous program points to -- explore additional paths, etc. -data SimContext (personality :: Type) (sym :: Type) (ext :: Type) - = SimContext { _ctxBackend :: !(SomeBackend sym) +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +type SimContext :: Type -> Type -> Type -> Type +data SimContext p sym ext + = SimContext { _ctxBackend :: !(SomeBackend sym) -- | Class dictionary for @'IsSymInterface' sym@ - , ctxSolverProof :: !(forall a . IsSymInterfaceProof sym a) - , ctxIntrinsicTypes :: !(IntrinsicTypes sym) + , ctxSolverProof :: !(forall a . IsSymInterfaceProof sym a) + , ctxIntrinsicTypes :: !(IntrinsicTypes sym) -- | Allocator for function handles - , simHandleAllocator :: !(HandleAllocator) + , simHandleAllocator :: !(HandleAllocator) -- | Handle to write messages to. - , printHandle :: !Handle - , extensionImpl :: ExtensionImpl personality sym ext - , _functionBindings :: !(FunctionBindings personality sym ext) - , _cruciblePersonality :: !personality - , _profilingMetrics :: !(Map Text (Metric personality sym ext)) + , printHandle :: !Handle + , extensionImpl :: ExtensionImpl p sym ext + , _functionBindings :: !(FunctionBindings p sym ext) + -- | See 'cruciblePersonality'. + , _cruciblePersonality :: !p + , _profilingMetrics :: !(Map Text (Metric p sym ext)) + , _exceptionContextConfig :: ExceptionContextConfig } -- | Create a new 'SimContext' with the given bindings. @@ -1048,15 +1338,16 @@ personality {- ^ Initial value for custom user state -} -> SimContext personality sym ext initSimContext bak muxFns halloc h bindings extImpl personality = - SimContext { _ctxBackend = SomeBackend bak - , ctxSolverProof = \a -> a - , ctxIntrinsicTypes = muxFns - , simHandleAllocator = halloc - , printHandle = h - , extensionImpl = extImpl - , _functionBindings = bindings - , _cruciblePersonality = personality - , _profilingMetrics = Map.empty + SimContext { _ctxBackend = SomeBackend bak + , ctxSolverProof = \a -> a + , ctxIntrinsicTypes = muxFns + , simHandleAllocator = halloc + , printHandle = h + , extensionImpl = extImpl + , _functionBindings = bindings + , _cruciblePersonality = personality + , _profilingMetrics = Map.empty + , _exceptionContextConfig = ECCNone } withBackend :: @@ -1065,8 +1356,27 @@ a withBackend ctx f = case _ctxBackend ctx of SomeBackend bak -> f bak +-- | Get a backend from a SimState and populate the error context +-- from the current simulation state. This differs from `withBackend` +-- because it can use the dynamic state of the simulator for things +-- like getting stack traces for exceptions and should be preferred +-- to `withBackend` where it is possible to use. +withStateBackend :: + SimState p sym ext rtp f args -> + (forall bak. IsSymBackend sym bak => bak -> a) -> a +withStateBackend st f = + if shouldHaveContext then + let ec = stateProgramStack st + in withBackend (st ^. stateContext) $ \bak -> + f (withExceptionContext bak ec) + else + withBackend (st ^. stateContext) f + where + shouldHaveContext = + st ^. stateContext . exceptionContextConfig /= ECCNone + -- | Access the symbolic backend inside a 'SimContext'. -ctxSymInterface :: Getter (SimContext p sym ext) sym +ctxSymInterface :: SimpleGetter (SimContext p sym ext) sym ctxSymInterface = to (\ctx -> case _ctxBackend ctx of SomeBackend bak -> backendGetSym bak) @@ -1075,13 +1385,39 @@ functionBindings :: Lens' (SimContext p sym ext) (FunctionBindings p sym ext) functionBindings = lens _functionBindings (\s v -> s { _functionBindings = v }) --- | Access the custom user-state inside the 'SimContext'. +-- | Custom state inside the 'SimContext'. +-- +-- Crucible itself is entirely polymorphic over @p@. Downstream applications can +-- instantiate it to any sort of state that they would like to associate with a +-- 'SimContext'. +-- +-- For example, applications based on +-- [@macaw-symbolic@](https://github.com/GaloisInc/macaw/tree/master/symbolic) +-- can instantiate this to a structure holding enough information to perform +-- incremental code discovery. See @ambient-verifier@'s +-- [@AmbientSimulatorState@](https://github.com/GaloisInc/ambient-verifier/blob/eab04abb9750825a25ec0cbe0379add63f05f6c6/src/Ambient/Extensions.hs#L1092-1137). +-- +-- Code that needs to store some state in the personality but doesn\'t wish to +-- fix a particular type can use the \"classy lenses\" approach, e.g., +-- +-- @ +-- class HasFooState p where +-- fooState :: `Lens'` p FooState +-- @ +-- +-- For examples of this approach, see +-- +-- * [@HasMacawLazySimulatorState@](https://github.com/GaloisInc/macaw/blob/cbec559b428fdd194398d07fc08c8c570a1d3bab/symbolic/src/Data/Macaw/Symbolic/MemOps.hs#L385-L394) +-- * [@HasGreaseSimulatorState@](https://github.com/GaloisInc/grease/blob/a50d54d2f414d15974dcf2d21654fbfe3527f0fa/src/Grease/Macaw/SimulatorState.hs#L90-L97) cruciblePersonality :: Lens' (SimContext p sym ext) p cruciblePersonality = lens _cruciblePersonality (\s v -> s{ _cruciblePersonality = v }) profilingMetrics :: Lens' (SimContext p sym ext) (Map Text (Metric p sym ext)) profilingMetrics = lens _profilingMetrics (\s v -> s { _profilingMetrics = v }) +exceptionContextConfig :: Lens' (SimContext p sym ext) ExceptionContextConfig +exceptionContextConfig = lens _exceptionContextConfig (\s v -> s { _exceptionContextConfig = v }) + ------------------------------------------------------------------------ -- SimState @@ -1094,6 +1430,13 @@ -- may be desirable to take additional or alternate actions on abort -- events; in which case, the library user may replace the default -- abort handler with their own. +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value newtype AbortHandler p sym ext rtp = AH { runAH :: forall (l :: Type) args. AbortExecReason -> @@ -1103,12 +1446,23 @@ -- | A SimState contains the execution context, an error handler, and -- the current execution tree. It captures the entire state -- of the symbolic simulator. -data SimState p sym ext rtp f (args :: Maybe (Ctx.Ctx CrucibleType)) +-- +-- Type parameters: +-- +-- - @p@: see 'cruciblePersonality' +-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- - @rtp@: type of the return value +-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang') +-- - @args@: arguments to the current frame (see 'SimFrame') +type SimState :: Type -> Type -> Type -> Type -> Type -> Maybe (Ctx.Ctx CrucibleType) -> Type +data SimState p sym ext rtp f args = SimState { _stateContext :: !(SimContext p sym ext) , _abortHandler :: !(AbortHandler p sym ext rtp) , _stateTree :: !(ActiveTree p sym ext rtp f args) } +type SomeSimState :: Type -> Type -> Type -> Type -> Type data SomeSimState p sym ext rtp = forall f args. SomeSimState !(SimState p sym ext rtp f args) @@ -1139,23 +1493,23 @@ } -stateLocation :: Getter (SimState p sym ext r f a) (Maybe ProgramLoc) +stateLocation :: SimpleGetter (SimState p sym ext r f a) (Maybe ProgramLoc) stateLocation = to f where f :: SimState p sym ext r f a -> Maybe ProgramLoc - f st = case st^.stateTree . actFrame . gpValue of + f st = case st ^. stateTree . actFrame . gpValue of MF cf -> Just $! (frameProgramLoc cf) OF _ -> Nothing RF _ _ -> Nothing -- | Access the 'SimContext' inside a 'SimState' -stateContext :: Simple Lens (SimState p sym ext r f a) (SimContext p sym ext) +stateContext :: Lens' (SimState p sym ext r f a) (SimContext p sym ext) stateContext = lens _stateContext (\s v -> s { _stateContext = v }) {-# INLINE stateContext #-} -- | Access the current abort handler of a state. -abortHandler :: Simple Lens (SimState p sym ext r f a) (AbortHandler p sym ext r) +abortHandler :: Lens' (SimState p sym ext r f a) (AbortHandler p sym ext r) abortHandler = lens _abortHandler (\s v -> s { _abortHandler = v }) -- | Access the active tree associated with a state. @@ -1186,21 +1540,49 @@ stateOverrideFrame = stateTree . actFrame . gpValue . overrideSimFrame -- | Access the globals inside a 'SimState' -stateGlobals :: Simple Lens (SimState p sym ext q f args) (SymGlobalState sym) +stateGlobals :: Lens' (SimState p sym ext q f args) (SymGlobalState sym) stateGlobals = stateTree . actFrame . gpGlobals -- | Get the symbolic interface out of a 'SimState' -stateSymInterface :: Getter (SimState p sym ext r f a) sym +stateSymInterface :: SimpleGetter (SimState p sym ext r f a) sym stateSymInterface = stateContext . ctxSymInterface -- | Get the intrinsic type map out of a 'SimState' -stateIntrinsicTypes :: Getter (SimState p sym ext r f args) (IntrinsicTypes sym) +stateIntrinsicTypes :: SimpleGetter (SimState p sym ext r f args) (IntrinsicTypes sym) stateIntrinsicTypes = stateContext . to ctxIntrinsicTypes -- | Get the configuration object out of a 'SimState' -stateConfiguration :: Getter (SimState p sym ext r f args) Config -stateConfiguration = to (\s -> stateSolverProof s (getConfiguration (s^.stateSymInterface))) +stateConfiguration :: SimpleGetter (SimState p sym ext r f args) Config +stateConfiguration = to (\s -> stateSolverProof s (getConfiguration (s ^. stateSymInterface))) -- | Provide the 'IsSymInterface' typeclass dictionary from a 'SimState' stateSolverProof :: SimState p sym ext r f args -> (forall a . IsSymInterfaceProof sym a) -stateSolverProof s = ctxSolverProof (s^.stateContext) +stateSolverProof s = ctxSolverProof (s ^. stateContext) + +-- | Get the program stack from a SimState +stateProgramStack :: SimState p sym ext r f args -> ProgramStack +stateProgramStack st = + ProgramStack + { psFrameOmitCount = length omitted + , psFrames = relevantFrames + } + where + + (relevantFrames, omitted) = + case eccConfig of + ECCNoLimit -> (rawFrames, []) + ECCLimited limit -> splitAt limit rawFrames + ECCNone -> ([],[]) + + eccConfig = st ^. stateContext . exceptionContextConfig + + isStartFrame (SomeFrame (OF frm)) = (frm ^. override) == startFunctionName + isStartFrame _ = False + removeStartFrame [] = [] + removeStartFrame [f] | isStartFrame f = [] + removeStartFrame (h:t) = h:removeStartFrame t + + rawFrames = + [ loc | SomeFrame sf <- removeStartFrame $ activeFrames (st ^. stateTree) + , loc <- maybeToList (frameStackLoc sf) + ] diff --git a/src/Lang/Crucible/Simulator/Operations.hs b/src/Lang/Crucible/Simulator/Operations.hs --- a/src/Lang/Crucible/Simulator/Operations.hs +++ b/src/Lang/Crucible/Simulator/Operations.hs @@ -76,17 +76,19 @@ import Prelude hiding (pred) import qualified Control.Exception as Ex -import Control.Lens import Control.Monad (when, void) import Control.Monad.IO.Class (MonadIO(..)) -import Control.Monad.Reader (ReaderT(..), withReaderT) +import Control.Monad.Reader (ReaderT(..), ask, withReaderT) import Control.Monad.Trans.Class (MonadTrans(..)) -import Data.Maybe (fromMaybe) +import Data.Function ((&)) import Data.List (isPrefixOf) +import Data.Maybe (fromMaybe) import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Some -import qualified Data.Vector as V import Data.Type.Equality hiding (sym) +import qualified Data.Vector as V +import Lens.Micro ((^.), (.~), (%~), _2, to, traverseOf) +import Lens.Micro.Mtl (view) import System.IO import qualified Prettyprinter as PP @@ -116,8 +118,8 @@ MuxFn p (SymGlobalState sym) -> MuxFn p (GlobalPair sym v) mergeGlobalPair merge_fn global_fn c x y = - GlobalPair <$> merge_fn c (x^.gpValue) (y^.gpValue) - <*> global_fn c (x^.gpGlobals) (y^.gpGlobals) + GlobalPair <$> merge_fn c (x ^. gpValue) (y ^. gpValue) + <*> global_fn c (x ^. gpGlobals) (y ^. gpGlobals) mergeAbortedResult :: ProgramLoc {- ^ Program location of control-flow branching -} -> @@ -125,8 +127,8 @@ AbortedResult sym ext -> AbortedResult sym ext -> AbortedResult sym ext -mergeAbortedResult _ _ (AbortedExit ec) _ = AbortedExit ec -mergeAbortedResult _ _ _ (AbortedExit ec) = AbortedExit ec +mergeAbortedResult _ _ ae@(AbortedExit {}) _ = ae +mergeAbortedResult _ _ _ ae@(AbortedExit {}) = ae mergeAbortedResult loc pred q r = AbortedBranch loc pred q r mergePartialAndAbortedResult :: @@ -156,12 +158,12 @@ BlockTarget _b_id -> do let x = fromCallFrame x0 let y = fromCallFrame y0 - z <- mergeRegs sym muxFns p (x^.frameRegs) (y^.frameRegs) + z <- mergeRegs sym muxFns p (x ^. frameRegs) (y ^. frameRegs) pure $! MF (x & frameRegs .~ z) ReturnTarget -> do let x = fromReturnFrame x0 let y = fromReturnFrame y0 - RF (x0^.frameFunctionName) <$> muxRegEntry sym muxFns p x y + RF (x0 ^. frameFunctionName) <$> muxRegEntry sym muxFns p x y mergePartialResult :: @@ -170,8 +172,8 @@ CrucibleBranchTarget f args -> MuxFn (Pred sym) (PartialResultFrame sym ext f args) mergePartialResult s tgt pred x y = - let sym = s^.stateSymInterface - iteFns = s^.stateIntrinsicTypes + let sym = s ^. stateSymInterface + iteFns = s ^. stateIntrinsicTypes merge_val = mergeCrucibleFrame sym iteFns tgt merge_fn = mergeGlobalPair merge_val (globalMuxFn sym iteFns) in @@ -254,7 +256,7 @@ SimFrame sym ext f a' -> IO (SimFrame sym ext f a') abortCrucibleFrame sym intrinsicFns (BlockTarget _) (MF x') = - do r' <- abortBranchRegs sym intrinsicFns (x'^.frameRegs) + do r' <- abortBranchRegs sym intrinsicFns (x' ^. frameRegs) return $! MF (x' & frameRegs .~ r') abortCrucibleFrame sym intrinsicFns ReturnTarget (RF nm x') = @@ -268,8 +270,8 @@ PartialResultFrame sym ext f a' -> IO (PartialResultFrame sym ext f a') abortPartialResult s tgt pr = - let sym = s^.stateSymInterface - muxFns = s^.stateIntrinsicTypes + let sym = s ^. stateSymInterface + muxFns = s ^. stateIntrinsicTypes abtGp (GlobalPair v g) = GlobalPair <$> abortCrucibleFrame sym muxFns tgt v <*> globalAbortBranch sym muxFns g in partialValue abtGp pr @@ -367,7 +369,7 @@ resolvedCallName :: ResolvedCall p sym ext ret -> FunctionName -resolvedCallName (OverrideCall _ f) = f^.override +resolvedCallName (OverrideCall _ f) = f ^. override resolvedCallName (CrucibleCall _ f) = case frameHandle f of SomeHandle h -> handleName h --------------------------------------------------------------------- @@ -404,11 +406,12 @@ SimState p sym ext rtp f args {- ^ Simulator state prior to the abort -} -> IO (ExecState p sym ext rtp) runErrorHandler msg st = - let ctx = st^.stateContext - sym = ctx^.ctxSymInterface - in withBackend ctx $ \bak -> + let ctx = st ^. stateContext + sym = ctx ^. ctxSymInterface + in withStateBackend st $ \bak -> do loc <- getCurrentProgramLoc sym - let err = SimError loc msg + let stk = stateProgramStack st + let err = mkSimError loc msg (Just stk) addProofObligation bak (LabeledPred (falsePred sym) err) return (AbortState (AssertionFailure err) st) @@ -464,7 +467,7 @@ ExecCont p sym ext rtp (CrucibleLang blocks ret) ('Just ctx) conditionalBranch p xjmp yjmp = do top_frame <- view (stateTree.actFrame) - Some pd <- return (top_frame^.crucibleTopFrame.framePostdom) + Some pd <- return (top_frame ^. crucibleTopFrame.framePostdom) x_frame <- cruciblePausedFrame xjmp top_frame pd y_frame <- cruciblePausedFrame yjmp top_frame pd @@ -495,7 +498,7 @@ variantCases ((p,jmp) : cs) = do top_frame <- view (stateTree.actFrame) - Some pd <- return (top_frame^.crucibleTopFrame.framePostdom) + Some pd <- return (top_frame ^. crucibleTopFrame.framePostdom) x_frame <- cruciblePausedFrame jmp top_frame pd let y_frame = PausedFrame (TotalRes top_frame) (SwitchResumption cs) Nothing @@ -581,9 +584,9 @@ performIntraFrameMerge tgt = do ActiveTree ctx0 er <- view stateTree - simCtx <- view stateContext + st <- ask sym <- view stateSymInterface - withBackend simCtx $ \bak -> + withStateBackend st $ \bak -> case ctx0 of VFFBranch ctx assume_frame loc pred other_branch tgt' @@ -639,9 +642,9 @@ continue (RunPostBranchMerge bid) ReturnTarget -> handleSimReturn - (er^.partialValue.gpValue.frameFunctionName) + (er ^. partialValue.gpValue.frameFunctionName) (returnContext ctx0) - (er^.partialValue.gpValue.to fromReturnFrame) + (er ^. partialValue.gpValue.to fromReturnFrame) --------------------------------------------------------------------- -- Abort handling @@ -701,9 +704,9 @@ AbortedResult sym ext {- ^ The execution that is being aborted. -} -> ExecCont p sym ext r g args resumeValueFromFrameAbort ctx0 ar0 = do - simCtx <- view stateContext + st <- ask sym <- view stateSymInterface - withBackend simCtx $ \bak -> + withStateBackend st $ \bak -> case ctx0 of -- This is the first abort. @@ -862,7 +865,7 @@ ExecCont p sym ext rtp (OverrideLang r) ('Just args) overrideSymbolicBranch p thn_args thn thn_pos els_args els els_pos = do top_frm <- view (stateTree.actFrame) - let fnm = top_frm^.gpValue.overrideSimFrame.override + let fnm = top_frm ^. gpValue.overrideSimFrame.override let thn_loc = mkProgramLoc fnm <$> thn_pos let els_loc = mkProgramLoc fnm <$> els_pos let thn_frm = PausedFrame (TotalRes top_frm) (OverrideResumption thn thn_args) thn_loc @@ -910,9 +913,9 @@ intra_branch p t_label f_label tgt = do ctx <- asContFrame <$> view stateTree - simCtx <- view stateContext + st <- ask sym <- view stateSymInterface - withBackend simCtx $ \bak -> + withStateBackend st $ \bak -> case asConstantPred p of Nothing -> ReaderT $ return . SymbolicBranchState p t_label f_label tgt @@ -943,13 +946,13 @@ ExecCont p sym ext rtp f ('Just dc_args) performIntraFrameSplit p a_frame o_frame tgt = do ctx <- asContFrame <$> view stateTree - simCtx <- view stateContext + st <- ask sym <- view stateSymInterface loc <- liftIO $ getCurrentProgramLoc sym a_frame' <- pushPausedFrame a_frame o_frame' <- pushPausedFrame o_frame - assume_frame <- withBackend simCtx $ \bak -> + assume_frame <- withStateBackend st $ \bak -> liftIO $ assumeInNewFrame bak (BranchCondition loc (pausedLoc a_frame') p) -- Create context for paused frame. @@ -1090,8 +1093,8 @@ ActiveTree p sym ext ret f args -> ActiveTree p sym ext ret f args extractCurrentPath t = - ActiveTree (vffSingleContext (t^.actContext)) - (TotalRes (t^.actFrame)) + ActiveTree (vffSingleContext (t ^. actContext)) + (TotalRes (t ^. actFrame)) vffSingleContext :: ValueFromFrame p sym ext ret f -> @@ -1118,9 +1121,9 @@ -- -- | Return all branch conditions along path to this node. -- branchConditions :: ActiveTree ctx sym ext ret f args -> [Pred sym] -- branchConditions t = --- case t^.actResult of --- TotalRes _ -> vffBranchConditions (t^.actContext) --- PartialRes p _ _ -> p : vffBranchConditions (t^.actContext) +-- case t ^. actResult of +-- TotalRes _ -> vffBranchConditions (t ^. actContext) +-- PartialRes p _ _ -> p : vffBranchConditions (t ^. actContext) -- vffBranchConditions :: ValueFromFrame p sym ext ret f -- -> [Pred sym] diff --git a/src/Lang/Crucible/Simulator/OverrideSim.hs b/src/Lang/Crucible/Simulator/OverrideSim.hs --- a/src/Lang/Crucible/Simulator/OverrideSim.hs +++ b/src/Lang/Crucible/Simulator/OverrideSim.hs @@ -75,32 +75,35 @@ , useIntrinsic -- * Typed overrides , TypedOverride(..) + , typedOverride , SomeTypedOverride(..) , runTypedOverride + , bindTypedOverride -- * Re-exports , Lang.Crucible.Simulator.ExecutionTree.Override ) where import Control.Exception -import Control.Lens import Control.Monad hiding (fail) import qualified Control.Monad.Catch as X import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Reader (ReaderT(..)) import Control.Monad.ST import Control.Monad.State.Strict (StateT(..)) -import Data.List (foldl') +import qualified Data.Foldable as Foldable +import Data.Function ((&)) import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.TraversableFC (fmapFC) import Data.Proxy import qualified Data.Text as T import Data.Traversable (for) +import Lens.Micro ((^.), (.~), to) +import Lens.Micro.Mtl (use, view, (.=), (%=)) import Numeric.Natural (Natural) import System.Exit import System.IO import System.IO.Error -import Data.Parameterized.TraversableFC (fmapFC) - import What4.Config import What4.Interface import What4.FunctionName @@ -135,7 +138,7 @@ -- -- Type parameters: -- --- * 'p' the "personality", i.e. user-defined state parameterized by @sym@ +-- * 'p' see 'Lang.Crucible.Simulator.ExecutionTree.cruciblePersonality' -- * 'sym' the symbolic backend -- * 'ext' the syntax extension ("Lang.Crucible.CFG.Extension") -- * 'rtp' global return type @@ -156,8 +159,14 @@ -- | Exit from the current execution by ignoring the continuation -- and immediately returning an aborted execution result. exitExecution :: IsSymInterface sym => ExitCode -> OverrideSim p sym ext rtp args r a -exitExecution ec = Sim $ StateContT $ \_c s -> - return $ ResultState $ AbortedResult (s^.stateContext) (AbortedExit ec) +exitExecution ec = do + ActiveTree _ctx ar0 <- use stateTree + let gp = + case ar0 of + TotalRes e -> e + PartialRes _loc _pred ex _ar1 -> ex + Sim $ StateContT $ \_c s -> + return $ ResultState $ AbortedResult (s ^. stateContext) (AbortedExit ec gp) bindOverrideSim :: OverrideSim p sym ext rtp args r a -> @@ -216,13 +225,14 @@ (forall bak. IsSymBackend sym bak => bak -> OverrideSim p sym ext rtp args ret a) -> OverrideSim p sym ext rtp args ret a ovrWithBackend k = - do simCtx <- use stateContext - ctxSolverProof simCtx (withBackend simCtx k) + do simSt <- get + simCtx <- use stateContext + ctxSolverProof simCtx (withStateBackend simSt k) instance MonadVerbosity (OverrideSim p sym ext rtp args ret) where getVerbosity = do ctx <- getContext - let cfg = ctxSolverProof ctx (getConfiguration (ctx^.ctxSymInterface)) + let cfg = ctxSolverProof ctx (getConfiguration (ctx ^. ctxSymInterface)) v <- liftIO (getOpt =<< getOptionSetting verbosity cfg) return (fromInteger v) @@ -572,7 +582,7 @@ go !i ((p,m,mpos):xs) = let msg = T.pack ("after branch " ++ show i) m' = ReaderT (runStateContT (unSim m) c') - in overrideSymbolicBranch p all_args m' mpos old_args (go (i+1) xs) (Just (OtherPos msg)) + in overrideSymbolicBranch p all_args m' mpos old_args (go (i + 1) xs) (Just (OtherPos msg)) go (0::Integer) xs0 -- | Non-deterministically choose among several feasible branches. @@ -627,7 +637,7 @@ -- | Build a map of function bindings from a list of -- handle/binding pairs. fnBindingsFromList :: [FnBinding p sym ext] -> FunctionBindings p sym ext -fnBindingsFromList = foldl' insertFnBinding $ FnBindings emptyHandleMap +fnBindingsFromList = Foldable.foldl' insertFnBinding $ FnBindings emptyHandleMap registerFnBinding :: FnBinding p sym ext -> OverrideSim p sym ext rtp a r () @@ -690,6 +700,21 @@ , typedOverrideRet :: TypeRepr ret } +-- | Create a 'TypedOverride' with a statically-known signature +typedOverride :: + KnownRepr (Ctx.Assignment TypeRepr) args => + KnownRepr TypeRepr ret => + (forall rtp args' ret'. + Ctx.Assignment (RegValue' sym) args -> + OverrideSim p sym ext rtp args' ret' (RegValue sym ret)) -> + TypedOverride p sym ext args ret +typedOverride handler = + TypedOverride + { typedOverrideHandler = handler + , typedOverrideArgs = knownRepr + , typedOverrideRet = knownRepr + } + -- | A 'TypedOverride' with the type parameters @args@, @ret@ existentially -- quantified data SomeTypedOverride p sym ext = @@ -703,3 +728,11 @@ runTypedOverride nm typedOvr = mkOverride' nm (typedOverrideRet typedOvr) $ do RegMap args <- getOverrideArgs typedOverrideHandler typedOvr (fmapFC (RV . regValue) args) + +-- | Bind a 'TypedOverride' to a 'FnHandle' +bindTypedOverride :: + FnHandle args ret -> + TypedOverride p sym ext args ret -> + OverrideSim p sym ext rtp args' ret' () +bindTypedOverride hdl ov = + bindFnHandle hdl (UseOverride (runTypedOverride (handleName hdl) ov)) diff --git a/src/Lang/Crucible/Simulator/PathSatisfiability.hs b/src/Lang/Crucible/Simulator/PathSatisfiability.hs --- a/src/Lang/Crucible/Simulator/PathSatisfiability.hs +++ b/src/Lang/Crucible/Simulator/PathSatisfiability.hs @@ -5,7 +5,7 @@ -- at symbolic branch points -- Copyright : (c) Galois, Inc 2018 -- License : BSD3 --- Maintainer : Rob Dockins +-- Maintainer : Ryan Scott , Langston Barrett -- Stability : provisional ------------------------------------------------------------------------ {-# LANGUAGE DataKinds #-} @@ -25,8 +25,8 @@ , BranchResult(..) ) where -import Control.Lens( (^.) ) import Control.Monad.Reader +import Lens.Micro ((^.)) import qualified Prettyprinter as PP import Lang.Crucible.Backend @@ -54,14 +54,20 @@ (Just (ConcreteBool True)) ] - +-- | Prune unsatisfiable execution traces during simulation. +-- +-- At every symbolic branch point, an SMT solver is queried to determine if one +-- or both symbolic branches are unsatisfiable. Only branches with satisfiable +-- branch conditions are explored. pathSatisfiabilityFeature :: forall sym. IsSymInterface sym => sym -> - (Maybe ProgramLoc -> Pred sym -> IO BranchResult) - {- ^ An action for considering the satisfiability of a predicate. - In the current state of the symbolic interface, indicate what - we can determine about the given predicate. -} -> + -- | An action for considering the satisfiability of a predicate. In the + -- current state of the symbolic interface, indicate what we can determine + -- about the given predicate. + -- + -- Usually, this is set to 'Lang.Crucible.Backend.Online.considerSatisfiability'. + (Maybe ProgramLoc -> Pred sym -> IO BranchResult) -> IO (GenericExecutionFeature sym) pathSatisfiabilityFeature sym considerSatisfiability = do tryExtendConfig pathSatOptions (getConfiguration sym) @@ -82,11 +88,11 @@ considerSatisfiability ploc p >>= \case IndeterminateBranchResult -> return ExecutionFeatureNoChange - NoBranch chosen_branch -> withBackend (st ^. stateContext) $ \bak -> + NoBranch chosen_branch -> withStateBackend st $ \bak -> do p' <- if chosen_branch then return p else notPred sym p let frm = if chosen_branch then tp else fp addAssumption bak (BranchCondition loc (pausedLoc frm) p') - ExecutionFeatureNewState <$> runReaderT (resumeFrame frm (asContFrame (st^.stateTree))) st + ExecutionFeatureNewState <$> runReaderT (resumeFrame frm (asContFrame (st ^. stateTree))) st UnsatisfiableContext -> return (ExecutionFeatureNewState (AbortState (InfeasibleBranch loc) st)) where diff --git a/src/Lang/Crucible/Simulator/PathSplitting.hs b/src/Lang/Crucible/Simulator/PathSplitting.hs --- a/src/Lang/Crucible/Simulator/PathSplitting.hs +++ b/src/Lang/Crucible/Simulator/PathSplitting.hs @@ -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 diff --git a/src/Lang/Crucible/Simulator/PositionTracking.hs b/src/Lang/Crucible/Simulator/PositionTracking.hs --- a/src/Lang/Crucible/Simulator/PositionTracking.hs +++ b/src/Lang/Crucible/Simulator/PositionTracking.hs @@ -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) diff --git a/src/Lang/Crucible/Simulator/Profiling.hs b/src/Lang/Crucible/Simulator/Profiling.hs --- a/src/Lang/Crucible/Simulator/Profiling.hs +++ b/src/Lang/Crucible/Simulator/Profiling.hs @@ -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 diff --git a/src/Lang/Crucible/Simulator/RecordAndReplay.hs b/src/Lang/Crucible/Simulator/RecordAndReplay.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Simulator/RecordAndReplay.hs @@ -0,0 +1,368 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} + +module Lang.Crucible.Simulator.RecordAndReplay ( + HasRecordState(..), + RecordState, + mkRecordState, + HasReplayState(..), + ReplayState, + mkReplayState, + recordTraceLength, + replayTraceLength, + RecordedTrace, + getRecordedTrace, + getConcreteRecordedTrace, + recordFeature, + replayFeature, + initialTrace, + traceGlobal, + emptyRecordedTrace +) where + +import Control.Exception qualified as X +import Data.Foldable qualified as F +import Data.Function ((&)) +import Data.Kind (Type) +import Data.Sequence qualified as Seq +import Data.Text qualified as Text +import Lang.Crucible.Backend qualified as CB +import Lang.Crucible.CFG.Core qualified as C +import Lang.Crucible.FunctionHandle qualified as C +import Lang.Crucible.Simulator qualified as C +import Lang.Crucible.Simulator.EvalStmt qualified as C +import Lang.Crucible.Simulator.ExecutionTree qualified as C +import Lang.Crucible.Simulator.GlobalState qualified as C +import Lang.Crucible.Simulator.SymSequence qualified as CSSS +import Lang.Crucible.Types qualified as CT +import Lens.Micro ((^.), (%~)) +import Lens.Micro qualified as Lens +import Lens.Micro.TH (makeLenses) +import What4.Interface qualified as W4 +import What4.Partial qualified as W4P + +-- | A trace consists of the 'W4.ProgramLoc's returned by +-- 'W4.getCurrentProgramLoc' in 'C.RunningState's during symbolic execution. +-- +-- Intentionally not part of the API so as to keep the implementation abstract. +type TraceType = CT.SequenceType (CT.StringType W4.Unicode) + +-- | Type parameters: +-- +-- * @p@: see 'C.cruciblePersonality' +-- * @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- * @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- * @rtp@: type of the simulator return value +type RecordState :: Type -> Type -> Type -> Type -> Type +newtype RecordState p sym ext rtp + = RecordState (C.GlobalVar TraceType) + -- ^ constructor intentionally not exported + +{- | A trace from 'recordFeature', processed and ready for consumption by +'replayFeature'. +-} +newtype RecordedTrace sym + = RecordedTrace (C.RegValue sym TraceType) + +-- | Type parameters: +-- +-- * @p@: see 'C.cruciblePersonality' +-- * @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface' +-- * @ext@: language extension, see "Lang.Crucible.CFG.Extension" +-- * @rtp@: type of the simulator return value +type ReplayState :: Type -> Type -> Type -> Type -> Type +data ReplayState p sym ext rtp + = ReplayState + { _traceGlobal :: (C.GlobalVar TraceType) + , _initialTrace :: (RecordedTrace sym) + } + -- ^ constructor intentionally not exported +makeLenses ''ReplayState + +-- | Constructor for 'RecordState' +mkRecordState :: + C.HandleAllocator -> IO (RecordState p sym ext rtp) +mkRecordState halloc = + RecordState <$> C.freshGlobalVar halloc "recordState" W4.knownRepr + +-- | Constructor for 'ReplayState' +mkReplayState :: + C.HandleAllocator -> RecordedTrace sym -> IO (ReplayState p sym ext rtp) +mkReplayState halloc rt = + ReplayState <$> C.freshGlobalVar halloc "replayState" W4.knownRepr <*> pure rt + +-- | A class for Crucible personality types @p@ which contain a +-- 'RecordState'. This execution feature is polymorphic over +-- 'RecordState' so that downstream users can supply their own +-- personality types that extend 'RecordState' further. +class HasRecordState p r sym ext rtp | p -> r sym ext rtp where + recordState :: Lens.Lens' p (RecordState r sym ext rtp) + +instance HasRecordState (RecordState p sym ext rtp) p sym ext rtp where + recordState = id + {-# INLINE recordState #-} + +-- | A class for Crucible personality types @p@ which contain a +-- 'ReplayState'. This execution feature is polymorphic over +-- 'ReplayState' so that downstream users can supply their own +-- personality types that extend 'ReplayState' further. +class HasReplayState p r sym ext rtp | p -> r sym ext rtp where + replayState :: Lens.Lens' p (ReplayState r sym ext rtp) + +instance HasReplayState (ReplayState p sym ext rtp) p sym ext rtp where + replayState = id + {-# INLINE replayState #-} + +data TraceGlobalNotDefined = TraceGlobalNotDefined + +instance Show TraceGlobalNotDefined where + show _ = "record and replay trace global not defined" + +instance X.Exception TraceGlobalNotDefined + +locAsStr :: + W4.IsExprBuilder sym => + sym -> + IO (C.RegValue sym (CT.StringType W4.Unicode)) +locAsStr sym = do + loc <- W4.getCurrentProgramLoc sym + let txtLoc = Text.pack (show loc) + W4.stringLit sym (W4.UnicodeLiteral txtLoc) + +emptyRecordedTrace :: sym -> IO (RecordedTrace sym) +emptyRecordedTrace sym = RecordedTrace <$> CSSS.nilSymSequence sym + +getRecordTrace :: + HasRecordState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + Maybe (C.RegValue sym TraceType) +getRecordTrace simState = do + let ctx = simState ^. C.stateContext + let RecordState g = ctx ^. C.cruciblePersonality . recordState + C.lookupGlobal g (simState ^. C.stateGlobals) + +-- | Get the length of the currently recorded trace +recordTraceLength :: + W4.IsExprBuilder sym => + HasRecordState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + IO (Maybe (W4.SymNat sym)) +recordTraceLength simState = do + let sym = simState ^. C.stateSymInterface + case getRecordTrace simState of + Nothing -> pure Nothing + Just s -> Just <$> CSSS.lengthSymSequence sym s + +getReplayTrace :: + HasReplayState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + Maybe (C.RegValue sym TraceType) +getReplayTrace simState = do + let ctx = simState ^. C.stateContext + let g = ctx ^. C.cruciblePersonality . replayState . traceGlobal + C.lookupGlobal g (simState ^. C.stateGlobals) + +-- | Get the length of the trace being replayed +replayTraceLength :: + W4.IsExprBuilder sym => + HasReplayState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + IO (Maybe (W4.SymNat sym)) +replayTraceLength simState = do + let sym = simState ^. C.stateSymInterface + case getReplayTrace simState of + Nothing -> pure Nothing + Just s -> Just <$> CSSS.lengthSymSequence sym s + +-- | An 'C.ExecutionFeature' to record traces. +-- +-- During execution this logs program locations to a Crucible global variable. +-- After execution, this variable may be read with 'getRecordedTrace' and the +-- 'RecordedTrace' can be passed to 'replayFeature' to \"replay\" it, i.e., to +-- abort all branches that deviate from it. +-- +-- If this is not called with 'C.InitialState' before any other 'C.ExecState', +-- it may throw a 'TraceGlobalNotDefined' exception. +recordFeature :: + ( HasRecordState p p sym ext rtp + , W4.IsExprBuilder sym + ) => + C.ExecutionFeature p sym ext rtp +recordFeature = + C.ExecutionFeature $ + \case + C.InitialState simCtx globals abortHandler retTy cont -> do + globals' <- insertNewTrace simCtx globals + let iState = C.InitialState simCtx globals' abortHandler retTy cont + return $ C.ExecutionFeatureModifiedState iState + C.RunningState runStateInfo st -> do + loc <- locAsStr (st ^. C.stateSymInterface) + st' <- consTrace st loc + let rState = C.RunningState runStateInfo st' + return $ C.ExecutionFeatureModifiedState rState + _ -> pure C.ExecutionFeatureNoChange + where + insertNewTrace :: + HasRecordState p p sym ext rtp => + C.SimContext p sym ext -> + C.SymGlobalState sym -> + IO (C.SymGlobalState sym) + insertNewTrace simCtx globals = do + let RecordState g = simCtx ^. C.cruciblePersonality . recordState + let sym = simCtx ^. C.ctxSymInterface + nil <- CSSS.nilSymSequence sym + return (C.insertGlobal g nil globals) + + getTraceOrThrow :: + HasRecordState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + IO (C.RegValue sym TraceType) + getTraceOrThrow st = + case getRecordTrace st of + Nothing -> X.throw TraceGlobalNotDefined + Just t -> pure t + + insertTrace :: + HasRecordState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + C.RegValue sym TraceType -> + C.SimState p sym ext rtp f args + insertTrace st v = do + let simCtx = st ^. C.stateContext + let RecordState g = simCtx ^. C.cruciblePersonality . recordState + st & C.stateGlobals %~ C.insertGlobal g v + + consTrace :: + HasRecordState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + C.RegValue sym (CT.StringType W4.Unicode) -> + IO (C.SimState p sym ext rtp f args) + consTrace st v = do + s <- getTraceOrThrow st + let sym = st ^. C.stateSymInterface + s' <- CSSS.consSymSequence sym v s + pure (insertTrace st s') + + + -- ^ constructor intentionally not exported to keep 'TraceType' out of the + -- API, but it could be exported in the future if necessary. + +-- | Obtain a 'RecordedTrace' after execution. +getRecordedTrace :: + C.SymGlobalState sym -> + RecordState p sym ext rtp -> + sym -> + IO (RecordedTrace sym) +getRecordedTrace globals (RecordState g) sym = do + case C.lookupGlobal g globals of + Nothing -> X.throw TraceGlobalNotDefined + Just s -> RecordedTrace <$> CSSS.reverseSymSequence sym s + +-- | Obtain a 'RecordedTrace' after execution using concrete evaluation. +-- +-- When a concrete evaluation function for 'W4.Pred's is available and only the +-- concretized trace is desired, this is more performant than the more general +-- 'getRecordedTrace'. +getConcreteRecordedTrace :: + W4.IsExprBuilder sym => + C.SymGlobalState sym -> + RecordState p sym ext rtp -> + sym -> + -- | Evaluation for booleans, usually a 'What4.Expr.GroundEval.GroundEvalFn' + (W4.Pred sym -> IO Bool) -> + IO (RecordedTrace sym) +getConcreteRecordedTrace globals (RecordState g) sym evalBool = do + case C.lookupGlobal g globals of + Nothing -> X.throw TraceGlobalNotDefined + Just s -> RecordedTrace <$> concretizeAndReverseTrace s + where + concretizeAndReverseTrace s = do + concretized <- CSSS.concretizeSymSequence evalBool pure s + let reversed = Seq.reverse concretized + CSSS.fromListSymSequence sym (F.toList reversed) + +{- | Inserts a recorded trace into the state's replay trace variable +The replay feature will follow this trace if it is enabled +-} +insertReplayTrace :: + (HasReplayState p p sym ext rtp) => + C.SimState p sym ext rtp f args -> + C.RegValue sym TraceType -> + C.SimState p sym ext rtp f args +insertReplayTrace st v = do + let simCtx = st ^. C.stateContext + let g = simCtx ^. C.cruciblePersonality . replayState . traceGlobal + st & C.stateGlobals %~ C.insertGlobal g v + +-- | An 'C.ExecutionFeature' to replay traces recorded with 'recordFeature'. +-- +-- Branches that deviate from the given trace will be aborted with +-- 'C.InfeasibleBranch'. +-- +-- If this is not called with 'C.InitialState' before any other 'C.ExecState', +-- it may throw a 'TraceGlobalNotDefined' exception. +replayFeature :: + ( HasReplayState p p sym ext rtp + , W4.IsExprBuilder sym + ) => + -- | Whether to stop at the end of the trace. If this is 'True' and execution + -- has exhausted the trace, then any further execution will be aborted via + -- 'C.InfeasibleBranch'. + Bool -> + C.ExecutionFeature p sym ext rtp +replayFeature stop = + C.ExecutionFeature $ + \case + C.InitialState simCtx globals abortHandler retTy cont -> do + let rstate = simCtx ^. C.cruciblePersonality . replayState + let g = rstate ^. traceGlobal + let RecordedTrace trace = rstate ^. initialTrace + let globals' = C.insertGlobal g trace globals + let iState = C.InitialState simCtx globals' abortHandler retTy cont + return $ C.ExecutionFeatureModifiedState iState + C.RunningState runStateInfo st -> do + let sym = st ^. C.stateSymInterface + s <- getTraceOrThrow st + partExpr <- CSSS.unconsSymSequence sym (W4.stringIte sym) s + let badPath = do + loc <- W4.getCurrentProgramLoc sym + let st' = C.AbortState (CB.InfeasibleBranch loc) st + pure (C.ExecutionFeatureNewState st') + case partExpr of + W4P.Unassigned + | stop -> badPath + | otherwise -> pure C.ExecutionFeatureNoChange + W4P.PE valid (expectedLoc, rest) -> + C.withStateBackend st $ \bak -> do + let msg = "Trace must be valid" + CB.assert bak valid (C.AssertFailureSimError msg "") + + currLoc <- locAsStr sym + atExpectedLoc <- W4.stringEq sym currLoc expectedLoc + case W4.asConstantPred atExpectedLoc of + Just False -> badPath + _ -> do + let msg' = "Execution deviated from trace" + CB.assert bak atExpectedLoc (C.AssertFailureSimError msg' "") + let st' = insertReplayTrace st rest + let rState = C.RunningState runStateInfo st' + pure (C.ExecutionFeatureModifiedState rState) + + _ -> pure C.ExecutionFeatureNoChange + where + getTraceOrThrow :: + HasReplayState p p sym ext rtp => + C.SimState p sym ext rtp f args -> + IO (C.RegValue sym TraceType) + getTraceOrThrow st = + case getReplayTrace st of + Nothing -> X.throw TraceGlobalNotDefined + Just t -> pure t diff --git a/src/Lang/Crucible/Simulator/RegValue.hs b/src/Lang/Crucible/Simulator/RegValue.hs --- a/src/Lang/Crucible/Simulator/RegValue.hs +++ b/src/Lang/Crucible/Simulator/RegValue.hs @@ -48,6 +48,8 @@ , muxVector , muxSymSequence , muxHandle + -- * Equality + , eqRegValue ) where import Control.Monad @@ -361,3 +363,41 @@ p (unVB (x Ctx.! i)) (unVB (y Ctx.! i)) + +------------------------------------------------------------------------ +-- Equality + +-- | Equality of 'RegValue's. +-- +-- This is only supported for a few types, see #1582. +eqRegValue :: + forall sym tp. + IsInterpretedFloatExprBuilder sym => + sym -> + TypeRepr tp -> + RegValue sym tp -> + RegValue sym tp -> + IO (Pred sym) +eqRegValue sym tp x y = + case tp of + -- Base types + BoolRepr -> eqPred sym x y + BVRepr _width -> bvEq sym x y + ComplexRealRepr -> cplxEq sym x y + FloatRepr @fi _ -> iFloatEq @_ @fi sym x y + IEEEFloatRepr _fpp -> floatEq sym x y + IntegerRepr -> intEq sym x y + NatRepr -> natEq sym x y + RealValRepr -> realEq sym x y + SymbolicStructRepr _tys -> structEq sym x y + SymbolicArrayRepr _idxs _tp -> arrayEq sym x y + StringRepr _si -> stringEq sym x y + + -- Trivial cases + UnitRepr -> pure (truePred sym) + CharRepr -> + if x == y + then pure (truePred sym) + else pure (falsePred sym) + + _ -> fail ("eqRegValue not supported for " ++ show tp) diff --git a/src/Lang/Crucible/Simulator/SimError.hs b/src/Lang/Crucible/Simulator/SimError.hs --- a/src/Lang/Crucible/Simulator/SimError.hs +++ b/src/Lang/Crucible/Simulator/SimError.hs @@ -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 + diff --git a/src/Lang/Crucible/Simulator/SymSequence.hs b/src/Lang/Crucible/Simulator/SymSequence.hs --- a/src/Lang/Crucible/Simulator/SymSequence.hs +++ b/src/Lang/Crucible/Simulator/SymSequence.hs @@ -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 diff --git a/src/Lang/Crucible/Syntax.hs b/src/Lang/Crucible/Syntax.hs --- a/src/Lang/Crucible/Syntax.hs +++ b/src/Lang/Crucible/Syntax.hs @@ -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!"] diff --git a/src/Lang/Crucible/Types.hs b/src/Lang/Crucible/Types.hs --- a/src/Lang/Crucible/Types.hs +++ b/src/Lang/Crucible/Types.hs @@ -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 diff --git a/src/Lang/Crucible/Utils/BitSet.hs b/src/Lang/Crucible/Utils/BitSet.hs --- a/src/Lang/Crucible/Utils/BitSet.hs +++ b/src/Lang/Crucible/Utils/BitSet.hs @@ -12,6 +12,7 @@ -- built on top of GHC-native Integers. ------------------------------------------------------------------------ module Lang.Crucible.Utils.BitSet +{-# DEPRECATED "This module is deprecated" #-} ( BitSet , getBits , empty @@ -35,7 +36,7 @@ import Data.Word import Data.Hashable import qualified Data.List as List -import Prelude hiding (null, foldr, foldl) +import Prelude hiding (null, foldr, foldl, foldl') newtype BitSet a = BitSet { getBits :: Integer } deriving (Show, Eq, Ord) @@ -47,7 +48,7 @@ empty = BitSet zeroBits null :: BitSet a -> Bool -null = (0==) . getBits +null = (0 ==) . getBits singleton :: Enum a => a -> BitSet a singleton a = BitSet (bit (fromEnum a)) @@ -81,19 +82,19 @@ where go :: Enum a => Integer -> Int -> [a] go 0 _ = [] go x i - | y .&. 0xffffffff == 0 = go (shiftR x 32) $! (i+32) - | y .&. 0x0000ffff == 0 = go (shiftR x 16) $! (i+16) - | y .&. 0x000000ff == 0 = go (shiftR x 8) $! (i+ 8) + | y .&. 0xffffffff == 0 = go (shiftR x 32) $! (i + 32) + | y .&. 0x0000ffff == 0 = go (shiftR x 16) $! (i + 16) + | y .&. 0x000000ff == 0 = go (shiftR x 8) $! (i + 8) | otherwise = concat - [ if testBit y 0 then [toEnum (i+0)] else [] - , if testBit y 1 then [toEnum (i+1)] else [] - , if testBit y 2 then [toEnum (i+2)] else [] - , if testBit y 3 then [toEnum (i+3)] else [] - , if testBit y 4 then [toEnum (i+4)] else [] - , if testBit y 5 then [toEnum (i+5)] else [] - , if testBit y 6 then [toEnum (i+6)] else [] - , if testBit y 7 then [toEnum (i+7)] else [] - , go (shiftR x 8) $! (i+8) + [ if testBit y 0 then [toEnum (i + 0)] else [] + , if testBit y 1 then [toEnum (i + 1)] else [] + , if testBit y 2 then [toEnum (i + 2)] else [] + , if testBit y 3 then [toEnum (i + 3)] else [] + , if testBit y 4 then [toEnum (i + 4)] else [] + , if testBit y 5 then [toEnum (i + 5)] else [] + , if testBit y 6 then [toEnum (i + 6)] else [] + , if testBit y 7 then [toEnum (i + 7)] else [] + , go (shiftR x 8) $! (i + 8) ] where y :: Word32 diff --git a/src/Lang/Crucible/Utils/CoreRewrite.hs b/src/Lang/Crucible/Utils/CoreRewrite.hs --- a/src/Lang/Crucible/Utils/CoreRewrite.hs +++ b/src/Lang/Crucible/Utils/CoreRewrite.hs @@ -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 diff --git a/src/Lang/Crucible/Utils/MuxTree.hs b/src/Lang/Crucible/Utils/MuxTree.hs --- a/src/Lang/Crucible/Utils/MuxTree.hs +++ b/src/Lang/Crucible/Utils/MuxTree.hs @@ -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 diff --git a/src/Lang/Crucible/Utils/Structural.hs b/src/Lang/Crucible/Utils/Structural.hs --- a/src/Lang/Crucible/Utils/Structural.hs +++ b/src/Lang/Crucible/Utils/Structural.hs @@ -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 diff --git a/src/Lang/Crucible/Vector.hs b/src/Lang/Crucible/Vector.hs --- a/src/Lang/Crucible/Vector.hs +++ b/src/Lang/Crucible/Vector.hs @@ -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 #-} diff --git a/test/absint/Max.hs b/test/absint/Max.hs --- a/test/absint/Max.hs +++ b/test/absint/Max.hs @@ -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 diff --git a/test/absint/WTO.hs b/test/absint/WTO.hs --- a/test/absint/WTO.hs +++ b/test/absint/WTO.hs @@ -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]) diff --git a/test/helpers/Main.hs b/test/helpers/Main.hs --- a/test/helpers/Main.hs +++ b/test/helpers/Main.hs @@ -1,9 +1,10 @@ {-# LANGUAGE AllowAmbiguousTypes #-} -module Main where -import Control.Lens ((^.)) +module Main (main) where + import Data.List (isInfixOf) import Data.Maybe (fromMaybe) +import Lens.Micro ((^.)) import Test.Hspec import Test.Tasty @@ -26,9 +27,12 @@ import qualified Panic as P +import qualified SymSequence as S + main :: IO () -main = - defaultMain =<< panicTests +main = do + p <- panicTests + defaultMain (testGroup "crucible" [p, backendTests, S.tests]) mkBackend :: IO (Some SomeBackend) mkBackend = do @@ -81,7 +85,7 @@ c <- W4I.freshConstant sym (W4I.safeSymbol "c") W4I.BaseBoolRepr assumePred bak "assuming c" c d <- W4I.freshConstant sym (W4I.safeSymbol "d") W4I.BaseBoolRepr - LCB.assert bak c (GenericSimError "asserting d") + LCB.assert bak d (GenericSimError "asserting d") (_asmps, mbGoals) <- LCB.popAssumptionFrameAndObligations bak frm [LCB.ProofGoal asmps gl] <- pure (fromMaybe [] (LCB.goalsToList <$> mbGoals)) asmpsPred <- LCB.assumptionsPred sym asmps diff --git a/test/helpers/SymSequence.hs b/test/helpers/SymSequence.hs new file mode 100644 --- /dev/null +++ b/test/helpers/SymSequence.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE ImportQualifiedPost #-} + +module SymSequence (tests) where + +import Test.Tasty qualified as TT + +import SymSequence.Properties qualified as Properties +import SymSequence.Reverse qualified as Reverse + +tests :: TT.TestTree +tests = + TT.testGroup "SymSequence" + [ Properties.tests + , Reverse.tests + ] diff --git a/test/helpers/SymSequence/Properties.hs b/test/helpers/SymSequence/Properties.hs new file mode 100644 --- /dev/null +++ b/test/helpers/SymSequence/Properties.hs @@ -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 diff --git a/test/helpers/SymSequence/Reverse.hs b/test/helpers/SymSequence/Reverse.hs new file mode 100644 --- /dev/null +++ b/test/helpers/SymSequence/Reverse.hs @@ -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