diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,40 @@ +# 0.10 -- 2026-09-10 + +* Add support for GHC 9.12 (at 9.12.2) and bump from 9.10.1 to 9.10.3. +* Fix `uniquelyConcRegMap` blocking clause: use disjunction (OR) instead of + conjunction (AND). The old code would falsely report a `RegMap` as uniquely + concretized whenever any single component was unique, even if other components + had multiple possible values. +* **BREAKING:** Rename various bits associated with the "breakpoint" + feature in accordance with renaming the feature to "cut" or + "cutpoint". + Exported Haskell symbols renamed: + - `Lang.Crucible.Simulator.Breakpoint` -> `Lang.Crucible.Simulator.Cut` + - `BreakpointName` -> `CutpointName` + - `Breakpoint` -> `Cut` + - `addBreakpointStmt` -> `addCutStmt` + - `breakAndReturn` -> `cutAndReturn` + - `breakpointPostdomInfo` -> `cutpointPostdomInfo` + - `cfgBreakpoints` -> `cfgCutpoints` + - `setFrameBreakpointPostdomInfo` -> `setFrameCutpointPostdomInfo` +* Add `reverseSymSequence` to `Lang.Crucible.Simulator.SymSequence` +* **BREAKING:** Add `FloatRound` constructor tp `App` in + `Lang.Crucible.CFG.Expr` for rounding floating-point values to the nearest + representable integral value. +* **BREAKING:** Add `SequenceReverse` constructor to `App` in + `Lang.Crucible.CFG.Expr` for reversing symbolic sequences. +* **BREAKING:** Change the signature of `getRecordedTrace` in + `Lang.Crucible.Simulator.RecordAndReplay` to remove the `evalBool` parameter, + as the implementation no longer concretizes the trace. +* Add `Lang.Crucible.Simulator.RecordAndReplay.getConcreteRecordedTrace` for + performant trace reversal when concretization is desired. +* Add `withStateBackend` and additional infrastructure for including stack + traces in `SimError` and `IsSymBackend` +* Fix `onlineProve` to properly negate goals before checking satisfiability +* Avoid sending trivially-true goals to the solver in `Backend.Prove`. +* Fix bug in `execResultGlobals` that caused it to erroneously always return the + non-aborted branch of a `FinishedResult ... (PartialRes ...)`. + # 0.9 -- 2026-01-29 # 0.8.0 -- 2025-11-09 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.9 +Version: 0.10 Author: Galois Inc. Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com Copyright: (c) Galois, Inc 2014-2022 @@ -34,12 +34,120 @@ Default: True common bldflags - ghc-options: -Wall - -Werror=incomplete-patterns - -Werror=missing-methods - -Werror=overlapping-patterns - -Wpartial-fields - -Wincomplete-uni-patterns + -- Note [Export lists] + -- ------------------- + -- + -- We don't allow modules without export lists. + -- + -- From the GHC docs: + -- + -- Declaring an explicit export list [...] enables GHC dead code analysis, + -- prevents accidental export of names and can ease optimizations like + -- inlining. + -- + -- It also makes it easier to organize the Haddocks using section headers, and + -- allows for internal/hidden definitions and constructors. + -- + -- We can't use -Werror=missing-export-lists here because it interferes with + -- ghcid. However, we enable it in CI, see ../cabal.project.ci. + ghc-options: + -Wmissing-export-lists + + -- Specifying -Wall and -Werror can cause the project to fail to build on + -- newer versions of GHC simply due to new warnings being added to -Wall. To + -- prevent this from happening we manually list which warnings should be + -- considered errors. We also list some warnings that are not in -Wall, though + -- try to avoid "opinionated" warnings (though this judgement is clearly + -- subjective). + -- + -- Warnings are grouped by the GHC version that introduced them, and then + -- alphabetically. + -- + -- A list of warnings and the GHC version in which they were introduced is + -- available here: + -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html + + -- Since GHC 9.6 or earlier: + ghc-options: + -Wall + -Werror=ambiguous-fields + -Werror=deferred-type-errors + -Werror=deprecated-flags + -Werror=deprecations + -Werror=deriving-defaults + -Werror=deriving-typeable + -Werror=dodgy-foreign-imports + -Werror=duplicate-exports + -Werror=empty-enumerations + -Werror=gadt-mono-local-binds + -Werror=identities + -Werror=inaccessible-code + -Werror=incomplete-patterns + -Werror=incomplete-record-updates + -Werror=incomplete-uni-patterns + -Werror=inline-rule-shadowing + -Werror=misplaced-pragmas + -Werror=missed-extra-shared-lib + -Werror=missing-exported-signatures + -Werror=missing-fields + -Werror=missing-home-modules + -Werror=missing-methods + -Werror=missing-pattern-synonym-signatures + -Werror=missing-signatures + -Werror=name-shadowing + -Werror=noncanonical-monad-instances + -Werror=noncanonical-monoid-instances + -Werror=operator-whitespace + -Werror=operator-whitespace-ext-conflict + -Werror=orphans + -Werror=overflowed-literals + -Werror=overlapping-patterns + -Werror=partial-fields + -Werror=partial-type-signatures + -Werror=redundant-bang-patterns + -Werror=redundant-record-wildcards + -Werror=redundant-strictness-flags + -Werror=simplifiable-class-constraints + -Werror=star-binder + -Werror=star-is-type + -Werror=tabs + -Werror=type-defaults + -Werror=typed-holes + -Werror=type-equality-out-of-scope + -Werror=type-equality-requires-operators + -Werror=unicode-bidirectional-format-characters + -Werror=unrecognised-pragmas + -Werror=unrecognised-warning-flags + -Werror=unsupported-calling-conventions + -Werror=unsupported-llvm-version + -Werror=unused-do-bind + -Werror=unused-imports + -Werror=unused-record-wildcards + -Werror=warnings-deprecations + -Werror=wrong-do-bind + + if impl(ghc < 9.8) + ghc-options: + -Werror=forall-identifier + + if impl(ghc >= 9.8) + ghc-options: + -Werror=incomplete-export-warnings + -Werror=inconsistent-flags + + if impl(ghc >= 9.10) + ghc-options: + -Werror=badly-staged-types + -Werror=data-kinds-tc + -Werror=incomplete-record-selectors + + if impl(ghc < 9.12) + ghc-options: + -Werror=compat-unqualified-imports + + -- TODO(#1308): Enable and fix this warning when GHC 9.6 is dropped from CI + -- -Werror=deprecated-type-abstractions + ghc-prof-options: -O2 -fprof-auto-exported default-language: Haskell2010 @@ -48,7 +156,7 @@ import: bldflags build-depends: async, - base >= 4.13 && < 4.21, + base >= 4.13 && < 4.22, bimap, bv-sized >= 1.0.0 && < 1.1, containers >= 0.5.9.0, @@ -56,15 +164,17 @@ fgl, hashable, json >= 0.9 && < 1.0, - lens, + microlens >= 0.5, + microlens-mtl, + microlens-th, mtl, panic >= 0.3, - parameterized-utils >= 1.0.8 && < 2.2, + parameterized-utils >= 2.3 && < 2.4, prettyprinter >= 1.7.0, template-haskell, text, time >= 1.8 && < 2.0, - th-abstraction >=0.1 && <0.7, + th-abstraction >=0.1 && <0.8, transformers, unordered-containers, vector, @@ -81,7 +191,6 @@ exposed-modules: Lang.Crucible.Analysis.DFS - Lang.Crucible.Analysis.ForwardDataflow Lang.Crucible.Analysis.Fixpoint Lang.Crucible.Analysis.Fixpoint.Components Lang.Crucible.Analysis.Postdom @@ -106,10 +215,10 @@ Lang.Crucible.FunctionHandle Lang.Crucible.README Lang.Crucible.Simulator - Lang.Crucible.Simulator.Breakpoint Lang.Crucible.Simulator.BoundedExec Lang.Crucible.Simulator.BoundedRecursion Lang.Crucible.Simulator.CallFrame + Lang.Crucible.Simulator.Cut Lang.Crucible.Simulator.Evaluation Lang.Crucible.Simulator.EvalStmt Lang.Crucible.Simulator.ExecutionTree @@ -170,12 +279,14 @@ hs-source-dirs: test/helpers other-modules: SymSequence + SymSequence.Properties + SymSequence.Reverse main-is: Main.hs build-depends: base, hspec >= 2.5, crucible, hedgehog, - lens, + microlens, panic >= 0.3, parameterized-utils, tasty >= 0.10, 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 @@ -85,13 +85,13 @@ ) where import Control.Exception(Exception(..), throwIO) -import Control.Lens ((^.)) import Control.Monad import Control.Monad.IO.Class import Data.Foldable (toList) import Data.Set (Set) -import qualified Prettyprinter as PP import GHC.Stack +import Lens.Micro ((^.)) +import qualified Prettyprinter as PP import Data.Parameterized.Map (MapF) @@ -318,6 +318,12 @@ -- In contrast to 'saveAssumptionState', this also includes the goals. getBackendState :: bak -> IO (AssumptionState sym) + -- | An additional exception context for more detailed SimErrors + getExceptionContext :: bak -> Maybe ProgramStack + + -- | Make a backend just like this but with a different error context + withExceptionContext :: bak -> ProgramStack -> bak + assertThenAssumeConfigOption :: ConfigOption BaseBoolType assertThenAssumeConfigOption = configOption knownRepr "assertThenAssume" @@ -375,7 +381,8 @@ assert bak p msg = do let sym = backendGetSym bak loc <- getCurrentProgramLoc sym - addAssertion bak (LabeledPred p (SimError loc msg)) + let ctx = getExceptionContext bak + addAssertion bak (LabeledPred p (mkSimError loc msg ctx)) -- | Add a proof obligation for False. This always aborts execution -- of the current path, because after asserting false, we get to assume it, @@ -385,7 +392,8 @@ addFailedAssertion bak msg = do let sym = backendGetSym bak loc <- getCurrentProgramLoc sym - let err = SimError loc msg + let ctx = getExceptionContext bak + let err = mkSimError loc msg ctx addProofObligation bak (LabeledPred (falsePred sym) err) abortExecBecause (AssertionFailure err) @@ -424,7 +432,8 @@ readPartExpr bak (PE p v) msg = do let sym = backendGetSym bak loc <- getCurrentProgramLoc sym - addAssertion bak (LabeledPred p (SimError loc msg)) + let ctx = getExceptionContext bak + addAssertion bak (LabeledPred p (mkSimError loc msg ctx)) return v @@ -496,7 +505,7 @@ ppGl = PP.indent 2 $ - PP.vsep [ppSimError (gl^.labeledPredMsg), printSymExpr (gl^.labeledPred)] + PP.vsep [ppSimError (gl ^. labeledPredMsg), printSymExpr (gl ^. labeledPred)] -- | Pretty-printer for 'AssumptionState'. ppAssumptionState :: 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 @@ -176,7 +176,7 @@ case gcPop gc of Left (ident', _assumes, mg, gc1) | ident == ident' -> (gc',n) - | otherwise -> go (n+1) gc' + | otherwise -> go (n + 1) gc' where gc' = case mg of Nothing -> gc1 Just g -> gcAddGoals g gc1 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 @@ -46,14 +46,14 @@ ) where -import Control.Lens (Traversal, folded) import Data.Kind (Type) import qualified Data.Foldable as F -import Data.Functor.Identity import Data.Functor.Const +import Data.Functor.Identity import qualified Data.Parameterized.TraversableF as TF -import qualified Data.Sequence as Seq import Data.Sequence (Seq) +import qualified Data.Sequence as Seq +import Lens.Micro (Traversal, folded) import qualified Prettyprinter as PP import What4.Expr.Builder 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 @@ -78,20 +78,19 @@ , withSTPOnlineBackend ) where -import Control.Lens ( (^.) ) import Control.Monad -import Control.Monad.Fix (mfix) import Control.Monad.Catch +import Control.Monad.Fix (mfix) import Control.Monad.IO.Class import Data.Bits import Data.Data (Data) import Data.Foldable import Data.IORef -import Data.Typeable (Typeable) -import GHC.Generics (Generic) -import System.IO import qualified Data.Text as Text +import GHC.Generics (Generic) +import Lens.Micro ((^.)) import qualified Prettyprinter as PP +import System.IO import What4.Config import What4.Concrete @@ -184,6 +183,8 @@ -- ^ action for checking if online features are currently enabled , onlineExprBuilder :: B.ExprBuilder scope st fs + + , onlineExceptionContext :: !(Maybe ProgramStack) } newOnlineBackend :: @@ -209,6 +210,7 @@ , currentFeatures = featref , onlineEnabled = getOpt enableOpt , onlineExprBuilder = sym + , onlineExceptionContext = Nothing } -- | Do something with an online backend. @@ -433,6 +435,9 @@ getBackendState bak = readIORef (AS.proofObligations (assumptionStack bak)) + getExceptionContext = onlineExceptionContext + withExceptionContext bak ec = bak { onlineExceptionContext = Just ec } + -------------------------------------------------------------------------------- -- Branch satisfiability @@ -450,7 +455,7 @@ -- | The context before considering the given predicate was already -- unsatisfiable. | UnsatisfiableContext - deriving (Data, Eq, Generic, Ord, Typeable) + deriving (Data, Eq, Generic, Ord) considerSatisfiability :: OnlineSolver solver => 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 @@ -30,9 +30,9 @@ , B.Flags ) where -import Control.Lens ( (^.) ) import Control.Monad (void) import Data.IORef (readIORef) +import Lens.Micro ((^.)) import What4.Config import What4.Interface @@ -56,8 +56,10 @@ SimpleBackend { sbAssumptionStack :: AS t , sbExprBuilder :: B.ExprBuilder t st fs + , sbExceptionContext :: Maybe ProgramStack } + newSimpleBackend :: B.ExprBuilder t st fs -> IO (SimpleBackend t st fs) @@ -67,6 +69,7 @@ return SimpleBackend { sbAssumptionStack = as , sbExprBuilder = sym + , sbExceptionContext = Nothing } instance HasSymInterface (B.ExprBuilder t st fs) (SimpleBackend t st fs) where @@ -114,3 +117,6 @@ AS.restoreAssumptionStack newstk (sbAssumptionStack bak) getBackendState bak = readIORef (AS.proofObligations (sbAssumptionStack bak)) + + withExceptionContext bak ec = bak { sbExceptionContext = Just ec } + getExceptionContext = sbExceptionContext 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 @@ -667,10 +667,11 @@ pure (Const p) let RM.RegMap mAssign = m preds <- Ctx.zipWithM notEq concM mAssign + -- not (modelA_1 == modelB_1) \/ ... \/ not (modelA_n == modelB_n) p <- foldlMFC - (\p (Const p') -> W4I.andPred sym p p') - (W4I.truePred sym) + (\p (Const p') -> W4I.orPred sym p p') + (W4I.falsePred sym) preds frm <- CB.pushAssumptionFrame bak 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 --- a/src/Lang/Crucible/README.hs +++ b/src/Lang/Crucible/README.hs @@ -1,6 +1,7 @@ {- | This module is only for documentation purposes, and provides a high level overview of Crucible aimed at developers. -} {-# OPTIONS_GHC -Wno-unused-imports #-} +{-# OPTIONS_GHC -Wno-missing-export-lists #-} module Lang.Crucible.README where import What4.Interface 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 @@ -236,7 +236,7 @@ SimState p sym ext rtp f args -> ([Either FunctionName FrameBoundData] -> [Either FunctionName FrameBoundData]) -> IO (ExecutionFeatureResult p sym ext rtp) - modifyStackState gvRef mkSt st f = do + modifyStackState gvRef mkSt st f = do currGv <- readIORef gvRef let err = panic "modifyStackState" ["Global variable not initialized"] let gv = fromMaybe err currGv @@ -253,16 +253,15 @@ SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a) -> IO (ExecutionFeatureResult p sym ext rtp) onTransition gvRef tgt_id res st = stateSolverProof st $ - do let sym = st^.stateSymInterface - let simCtx = st^.stateContext - (globals', overLimit) <- checkBackedge gvRef (st^.stateCrucibleFrame.frameBlockID) tgt_id (st^.stateGlobals) + do let sym = st ^. stateSymInterface + (globals', overLimit) <- checkBackedge gvRef (st ^. stateCrucibleFrame.frameBlockID) tgt_id (st ^. stateGlobals) let st' = st & stateGlobals .~ globals' case overLimit of Just n -> do let msg = "reached maximum number of loop iterations (" ++ show n ++ ")" - let loc = st^.stateCrucibleFrame.to frameProgramLoc + let loc = st ^. stateCrucibleFrame.to frameProgramLoc let err = SimError loc (ResourceExhausted msg) - when generateSideConditions $ withBackend simCtx $ \bak -> + when generateSideConditions $ withStateBackend st $ \bak -> addProofObligation bak (LabeledPred (falsePred sym) err) return (ExecutionFeatureNewState (AbortState (AssertionFailure err) st')) Nothing -> return (ExecutionFeatureModifiedState (ControlTransferState res st')) @@ -276,8 +275,8 @@ InitialState simctx globals ah ret cont -> do let halloc = simHandleAllocator simctx currGv <- readIORef gvRef - ngv <- case currGv of - Nothing -> do + ngv <- case currGv of + Nothing -> do gv <- freshGlobalVar halloc (Text.pack "BoundedExecFrameData") knownRepr writeIORef gvRef (Just gv) pure gv 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 @@ -109,26 +110,25 @@ SimState p sym ext rtp f args -> IO (ExecutionFeatureResult p sym ext rtp) pushFrame gvRef rebuildStack h mkSt st = stateSolverProof st $ - do let sym = st^.stateSymInterface - let simCtx = st^.stateContext + do let sym = st ^. stateSymInterface currGv <- readIORef gvRef let err = panic "pushFrame" ["Uninitialized global!"] let gv = fromMaybe err currGv case lookupGlobal gv (st ^. stateGlobals) of Nothing -> panic "bounded recursion" ["global not defined!"] Just [] -> panic "bounded recursion" ["empty stack!"] - Just (x:xs) -> do + Just (x:xs) -> do mb <- getRecursionBound h let v = 1 + fromMaybe 0 (Map.lookup h x) case mb of - Just b | v > b -> do + Just b | v > b -> do loc <- getCurrentProgramLoc sym let msg = ("reached maximum number of recursive calls to function " ++ show h ++ " (" ++ show b ++ ")") let simerr = SimError loc (ResourceExhausted msg) - when generateSideConditions $ withBackend simCtx $ \bak -> + when generateSideConditions $ withStateBackend st $ \bak -> addProofObligation bak (LabeledPred (falsePred sym) simerr) return (ExecutionFeatureNewState (AbortState (AssertionFailure simerr) st)) - _ -> do + _ -> do let x' = Map.insert h v x let st' = st & stateGlobals %~ insertGlobal gv (rebuildStack x' x xs) x' `seq` return (ExecutionFeatureModifiedState (mkSt st')) @@ -143,9 +143,9 @@ InitialState simctx globals ah ret cont -> do let halloc = simHandleAllocator simctx - currGv <- readIORef gvRef - gv <- case currGv of - Just gv -> pure gv + currGv <- readIORef gvRef + gv <- case currGv of + Just gv -> pure gv Nothing -> do gv <- freshGlobalVar halloc (Text.pack "BoundedRecursionData") knownRepr writeIORef gvRef (Just gv) 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') @@ -323,8 +325,16 @@ -> RegEntry sym (FrameRetType f) fromReturnFrame (RF _ x) = x -frameFunctionName :: Getter (SimFrame sym ext f a) FunctionName +frameFunctionName :: SimpleGetter (SimFrame sym ext f a) FunctionName frameFunctionName = to $ \case - OF f -> f^.override + OF f -> f ^. override MF f -> case frameHandle f of SomeHandle h -> handleName h RF n _ -> n + +-- | Get a location for a stack frame, or Nothing if this is a return frame +frameStackLoc :: (SimFrame sym ext f a) -> Maybe ProgramLoc +frameStackLoc frame = + case frame of + sf@(OF _) -> Just $ mkProgramLoc (sf ^. frameFunctionName) InternalPos + (MF f) -> Just $ frameProgramLoc f + (RF _ _) -> Nothing 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 @@ -116,12 +116,16 @@ , IsSymInterfaceProof , SimContext(..) , Metric(..) + , ExceptionContextConfig(..) , initSimContext , withBackend + , withStateBackend , ctxSymInterface , functionBindings , cruciblePersonality , profilingMetrics + , exceptionContextConfig + , parseExceptionContextConfig -- * SimState , SimState(..) @@ -143,18 +147,22 @@ , stateOverrideFrame , stateGlobals , stateConfiguration + , stateProgramStack ) where -import Control.Lens import Control.Monad.Reader +import Data.Function ((&)) import Data.Kind import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map +import Data.Maybe(maybeToList) import Data.Parameterized.Ctx import qualified Data.Parameterized.Context as Ctx import Data.Text (Text) +import Lens.Micro ((^.), (.~), Lens', Lens, SimpleGetter, Traversal', lens, to) import System.Exit (ExitCode) import System.IO +import Text.Read(readMaybe) import qualified Prettyprinter as PP import What4.Config (Config) @@ -174,6 +182,7 @@ import Lang.Crucible.Simulator.GlobalState (SymGlobalState) import Lang.Crucible.Simulator.Intrinsics (IntrinsicTypes) import Lang.Crucible.Simulator.RegMap (RegMap, emptyRegMap, RegValue, RegEntry) +import Lang.Crucible.Simulator.SimError(ProgramStack(..)) import Lang.Crucible.Types ------------------------------------------------------------------------ @@ -197,7 +206,7 @@ gpValue = lens _gpValue (\s v -> s { _gpValue = v }) -- | Access the globals stored in the global pair. -gpGlobals :: Simple Lens (GlobalPair sym u) (SymGlobalState sym) +gpGlobals :: Lens' (GlobalPair sym u) (SymGlobalState sym) gpGlobals = lens _gpGlobals (\s v -> s { _gpGlobals = v }) @@ -285,13 +294,13 @@ filterCrucibleFrames _ = Nothing -- | Iterate over frames in the result. -arFrames :: Simple Traversal (AbortedResult sym ext) (SomeFrame (SimFrame sym ext)) +arFrames :: Traversal' (AbortedResult sym ext) (SomeFrame (SimFrame sym ext)) arFrames h (AbortedExec e p) = (\(SomeFrame f') -> AbortedExec e (p & gpValue .~ f')) - <$> h (SomeFrame (p^.gpValue)) + <$> h (SomeFrame (p ^. gpValue)) arFrames h (AbortedExit ec p) = (\(SomeFrame f') -> AbortedExit ec (p & gpValue .~ f')) - <$> h (SomeFrame (p^.gpValue)) + <$> h (SomeFrame (p ^. gpValue)) arFrames h (AbortedBranch predicate loc r s) = AbortedBranch predicate loc <$> arFrames h r <*> arFrames h s @@ -303,7 +312,7 @@ where pp :: SomeFrame (SimFrame sym ext) -> PP.Doc ann pp (SomeFrame (OF f)) = - PP.pretty "When calling" PP.<+> PP.viaShow (f^.override) + PP.pretty "When calling" PP.<+> PP.viaShow (f ^. override) pp (SomeFrame (MF f)) = PP.pretty "In" PP.<+> PP.viaShow (frameHandle f) PP.<+> PP.pretty "at" PP.<+> PP.pretty (plSourceLoc (frameProgramLoc f)) @@ -424,16 +433,16 @@ execStateContext :: ExecState p sym ext r -> SimContext p sym ext execStateContext = \case ResultState res -> execResultContext res - AbortState _ st -> st^.stateContext - UnwindCallState _ _ st -> st^.stateContext - CallState _ _ st -> st^.stateContext - TailCallState _ _ st -> st^.stateContext - ReturnState _ _ _ st -> st^.stateContext - ControlTransferState _ st -> st^.stateContext - RunningState _ st -> st^.stateContext - SymbolicBranchState _ _ _ _ st -> st^.stateContext - OverrideState _ st -> st^.stateContext - BranchMergeState _ st -> st^.stateContext + AbortState _ st -> st ^. stateContext + UnwindCallState _ _ st -> st ^. stateContext + CallState _ _ st -> st ^. stateContext + TailCallState _ _ st -> st ^. stateContext + ReturnState _ _ _ st -> st ^. stateContext + ControlTransferState _ st -> st ^. stateContext + RunningState _ st -> st ^. stateContext + SymbolicBranchState _ _ _ _ st -> st ^. stateContext + OverrideState _ st -> st ^. stateContext + BranchMergeState _ st -> st ^. stateContext InitialState stctx _ _ _ _ -> stctx setExecStateContext :: @@ -472,7 +481,7 @@ abortedGlobals :: Monad f => - -- | How to handle 'AbortedBranch'. + -- | How to handle branches (e.g., 'AbortedBranch', 'PartialRes'). -- -- Common options include concretizing the 'Pred' or returning a partial -- result (e.g., 'Nothing'). @@ -491,7 +500,7 @@ -- | Extract the 'SymGlobalState' from an 'ExecResult'. execResultGlobals :: Monad f => - -- | How to handle 'AbortedBranch'. + -- | How to handle branches (e.g., 'AbortedBranch', 'PartialRes'). -- -- Common options include concretizing the 'Pred' or returning a partial -- result (e.g., 'Nothing'). @@ -500,7 +509,13 @@ f (SymGlobalState sym) execResultGlobals handleBranch = \case - FinishedResult _ctx partial -> pure (partial ^. partialValue . gpGlobals) + FinishedResult simCtx partial -> + case partial of + TotalRes gp -> pure (gp ^. gpGlobals) + PartialRes loc p gp aborted -> do + let l = gp ^. gpGlobals + r <- abortedGlobals (handleBranch simCtx) aborted + handleBranch simCtx loc p l r TimeoutResult st -> execStateGlobals handleBranch st AbortedResult simCtx aborted -> abortedGlobals (handleBranch simCtx) aborted @@ -508,7 +523,7 @@ -- | Extract the 'SymGlobalState' from an 'ExecState'. execStateGlobals :: Monad f => - -- | How to handle 'AbortedBranch'. + -- | How to handle branches (e.g., 'AbortedBranch', 'PartialRes'). -- -- Common options include concretizing the 'Pred' or returning a partial -- result (e.g., 'Nothing'). @@ -1153,7 +1168,7 @@ activeFrames :: ActiveTree ctx sym ext root a args -> [SomeFrame (SimFrame sym ext)] activeFrames (ActiveTree ctx ar) = - SomeFrame (ar^.partialValue^.gpValue) : parentFrames ctx + SomeFrame (ar ^. partialValue ^. gpValue) : parentFrames ctx ------------------------------------------------------------------------ @@ -1265,6 +1280,24 @@ runMetric :: forall rtp f args. SimState p sym ext rtp f args -> IO Integer } +data ExceptionContextConfig = + ECCNone -- ^ do not include exceptions with context + | ECCLimited Int + | ECCNoLimit + deriving(Eq, Ord, Show, Read) + +parseExceptionContextConfig :: String -> Either String ExceptionContextConfig +parseExceptionContextConfig s = + case s of + "none" -> Right ECCNone + "nolimit" -> Right ECCNoLimit + _ | Just limit <- readMaybe s -> + if limit > 0 + then Right (ECCLimited limit) + else Left "exception context frame limit cannot be 0 or less" + _ -> Left "invalid exception context config - valid inputs are `none`, `nolimit`, and integers greater than 0" + + -- | Top-level state record for the simulator. The state contained in this record -- remains persistent across all symbolic simulator actions. In particular, it -- is not rolled back when the simulator returns previous program points to @@ -1277,19 +1310,20 @@ -- - @ext@: language extension, see "Lang.Crucible.CFG.Extension" type SimContext :: Type -> Type -> Type -> Type data SimContext p sym ext - = SimContext { _ctxBackend :: !(SomeBackend sym) + = SimContext { _ctxBackend :: !(SomeBackend sym) -- | Class dictionary for @'IsSymInterface' sym@ - , ctxSolverProof :: !(forall a . IsSymInterfaceProof sym a) - , ctxIntrinsicTypes :: !(IntrinsicTypes sym) + , ctxSolverProof :: !(forall a . IsSymInterfaceProof sym a) + , ctxIntrinsicTypes :: !(IntrinsicTypes sym) -- | Allocator for function handles - , simHandleAllocator :: !(HandleAllocator) + , simHandleAllocator :: !(HandleAllocator) -- | Handle to write messages to. - , printHandle :: !Handle - , extensionImpl :: ExtensionImpl p sym ext - , _functionBindings :: !(FunctionBindings p sym ext) + , printHandle :: !Handle + , extensionImpl :: ExtensionImpl p sym ext + , _functionBindings :: !(FunctionBindings p sym ext) -- | See 'cruciblePersonality'. - , _cruciblePersonality :: !p - , _profilingMetrics :: !(Map Text (Metric p sym ext)) + , _cruciblePersonality :: !p + , _profilingMetrics :: !(Map Text (Metric p sym ext)) + , _exceptionContextConfig :: ExceptionContextConfig } -- | Create a new 'SimContext' with the given bindings. @@ -1304,15 +1338,16 @@ personality {- ^ Initial value for custom user state -} -> SimContext personality sym ext initSimContext bak muxFns halloc h bindings extImpl personality = - SimContext { _ctxBackend = SomeBackend bak - , ctxSolverProof = \a -> a - , ctxIntrinsicTypes = muxFns - , simHandleAllocator = halloc - , printHandle = h - , extensionImpl = extImpl - , _functionBindings = bindings - , _cruciblePersonality = personality - , _profilingMetrics = Map.empty + SimContext { _ctxBackend = SomeBackend bak + , ctxSolverProof = \a -> a + , ctxIntrinsicTypes = muxFns + , simHandleAllocator = halloc + , printHandle = h + , extensionImpl = extImpl + , _functionBindings = bindings + , _cruciblePersonality = personality + , _profilingMetrics = Map.empty + , _exceptionContextConfig = ECCNone } withBackend :: @@ -1321,8 +1356,27 @@ a withBackend ctx f = case _ctxBackend ctx of SomeBackend bak -> f bak +-- | Get a backend from a SimState and populate the error context +-- from the current simulation state. This differs from `withBackend` +-- because it can use the dynamic state of the simulator for things +-- like getting stack traces for exceptions and should be preferred +-- to `withBackend` where it is possible to use. +withStateBackend :: + SimState p sym ext rtp f args -> + (forall bak. IsSymBackend sym bak => bak -> a) -> a +withStateBackend st f = + if shouldHaveContext then + let ec = stateProgramStack st + in withBackend (st ^. stateContext) $ \bak -> + f (withExceptionContext bak ec) + else + withBackend (st ^. stateContext) f + where + shouldHaveContext = + st ^. stateContext . exceptionContextConfig /= ECCNone + -- | Access the symbolic backend inside a 'SimContext'. -ctxSymInterface :: Getter (SimContext p sym ext) sym +ctxSymInterface :: SimpleGetter (SimContext p sym ext) sym ctxSymInterface = to (\ctx -> case _ctxBackend ctx of SomeBackend bak -> backendGetSym bak) @@ -1361,6 +1415,9 @@ profilingMetrics :: Lens' (SimContext p sym ext) (Map Text (Metric p sym ext)) profilingMetrics = lens _profilingMetrics (\s v -> s { _profilingMetrics = v }) +exceptionContextConfig :: Lens' (SimContext p sym ext) ExceptionContextConfig +exceptionContextConfig = lens _exceptionContextConfig (\s v -> s { _exceptionContextConfig = v }) + ------------------------------------------------------------------------ -- SimState @@ -1436,23 +1493,23 @@ } -stateLocation :: Getter (SimState p sym ext r f a) (Maybe ProgramLoc) +stateLocation :: SimpleGetter (SimState p sym ext r f a) (Maybe ProgramLoc) stateLocation = to f where f :: SimState p sym ext r f a -> Maybe ProgramLoc - f st = case st^.stateTree . actFrame . gpValue of + f st = case st ^. stateTree . actFrame . gpValue of MF cf -> Just $! (frameProgramLoc cf) OF _ -> Nothing RF _ _ -> Nothing -- | Access the 'SimContext' inside a 'SimState' -stateContext :: Simple Lens (SimState p sym ext r f a) (SimContext p sym ext) +stateContext :: Lens' (SimState p sym ext r f a) (SimContext p sym ext) stateContext = lens _stateContext (\s v -> s { _stateContext = v }) {-# INLINE stateContext #-} -- | Access the current abort handler of a state. -abortHandler :: Simple Lens (SimState p sym ext r f a) (AbortHandler p sym ext r) +abortHandler :: Lens' (SimState p sym ext r f a) (AbortHandler p sym ext r) abortHandler = lens _abortHandler (\s v -> s { _abortHandler = v }) -- | Access the active tree associated with a state. @@ -1483,21 +1540,49 @@ stateOverrideFrame = stateTree . actFrame . gpValue . overrideSimFrame -- | Access the globals inside a 'SimState' -stateGlobals :: Simple Lens (SimState p sym ext q f args) (SymGlobalState sym) +stateGlobals :: Lens' (SimState p sym ext q f args) (SymGlobalState sym) stateGlobals = stateTree . actFrame . gpGlobals -- | Get the symbolic interface out of a 'SimState' -stateSymInterface :: Getter (SimState p sym ext r f a) sym +stateSymInterface :: SimpleGetter (SimState p sym ext r f a) sym stateSymInterface = stateContext . ctxSymInterface -- | Get the intrinsic type map out of a 'SimState' -stateIntrinsicTypes :: Getter (SimState p sym ext r f args) (IntrinsicTypes sym) +stateIntrinsicTypes :: SimpleGetter (SimState p sym ext r f args) (IntrinsicTypes sym) stateIntrinsicTypes = stateContext . to ctxIntrinsicTypes -- | Get the configuration object out of a 'SimState' -stateConfiguration :: Getter (SimState p sym ext r f args) Config -stateConfiguration = to (\s -> stateSolverProof s (getConfiguration (s^.stateSymInterface))) +stateConfiguration :: SimpleGetter (SimState p sym ext r f args) Config +stateConfiguration = to (\s -> stateSolverProof s (getConfiguration (s ^. stateSymInterface))) -- | Provide the 'IsSymInterface' typeclass dictionary from a 'SimState' stateSolverProof :: SimState p sym ext r f args -> (forall a . IsSymInterfaceProof sym a) -stateSolverProof s = ctxSolverProof (s^.stateContext) +stateSolverProof s = ctxSolverProof (s ^. stateContext) + +-- | Get the program stack from a SimState +stateProgramStack :: SimState p sym ext r f args -> ProgramStack +stateProgramStack st = + ProgramStack + { psFrameOmitCount = length omitted + , psFrames = relevantFrames + } + where + + (relevantFrames, omitted) = + case eccConfig of + ECCNoLimit -> (rawFrames, []) + ECCLimited limit -> splitAt limit rawFrames + ECCNone -> ([],[]) + + eccConfig = st ^. stateContext . exceptionContextConfig + + isStartFrame (SomeFrame (OF frm)) = (frm ^. override) == startFunctionName + isStartFrame _ = False + removeStartFrame [] = [] + removeStartFrame [f] | isStartFrame f = [] + removeStartFrame (h:t) = h:removeStartFrame t + + rawFrames = + [ loc | SomeFrame sf <- removeStartFrame $ activeFrames (st ^. stateTree) + , loc <- maybeToList (frameStackLoc sf) + ] 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 -} -> @@ -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 @@ -84,7 +84,6 @@ ) where import Control.Exception -import Control.Lens import Control.Monad hiding (fail) import qualified Control.Monad.Catch as X import Control.Monad.IO.Class (MonadIO(..)) @@ -92,17 +91,19 @@ import Control.Monad.ST import Control.Monad.State.Strict (StateT(..)) import qualified Data.Foldable as Foldable +import Data.Function ((&)) import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.TraversableFC (fmapFC) import Data.Proxy import qualified Data.Text as T import Data.Traversable (for) +import Lens.Micro ((^.), (.~), to) +import Lens.Micro.Mtl (use, view, (.=), (%=)) import Numeric.Natural (Natural) import System.Exit import System.IO import System.IO.Error -import Data.Parameterized.TraversableFC (fmapFC) - import What4.Config import What4.Interface import What4.FunctionName @@ -165,7 +166,7 @@ TotalRes e -> e PartialRes _loc _pred ex _ar1 -> ex Sim $ StateContT $ \_c s -> - return $ ResultState $ AbortedResult (s^.stateContext) (AbortedExit ec gp) + return $ ResultState $ AbortedResult (s ^. stateContext) (AbortedExit ec gp) bindOverrideSim :: OverrideSim p sym ext rtp args r a -> @@ -224,13 +225,14 @@ (forall bak. IsSymBackend sym bak => bak -> OverrideSim p sym ext rtp args ret a) -> OverrideSim p sym ext rtp args ret a ovrWithBackend k = - do simCtx <- use stateContext - ctxSolverProof simCtx (withBackend simCtx k) + do simSt <- get + simCtx <- use stateContext + ctxSolverProof simCtx (withStateBackend simSt k) instance MonadVerbosity (OverrideSim p sym ext rtp args ret) where getVerbosity = do ctx <- getContext - let cfg = ctxSolverProof ctx (getConfiguration (ctx^.ctxSymInterface)) + let cfg = ctxSolverProof ctx (getConfiguration (ctx ^. ctxSymInterface)) v <- liftIO (getOpt =<< getOptionSetting verbosity cfg) return (fromInteger v) @@ -580,7 +582,7 @@ go !i ((p,m,mpos):xs) = let msg = T.pack ("after branch " ++ show i) m' = ReaderT (runStateContT (unSim m) c') - in overrideSymbolicBranch p all_args m' mpos old_args (go (i+1) xs) (Just (OtherPos msg)) + in overrideSymbolicBranch p all_args m' mpos old_args (go (i + 1) xs) (Just (OtherPos msg)) go (0::Integer) xs0 -- | Non-deterministically choose among several feasible branches. 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 @@ -25,8 +25,8 @@ , BranchResult(..) ) where -import Control.Lens( (^.) ) import Control.Monad.Reader +import Lens.Micro ((^.)) import qualified Prettyprinter as PP import Lang.Crucible.Backend @@ -88,11 +88,11 @@ considerSatisfiability ploc p >>= \case IndeterminateBranchResult -> return ExecutionFeatureNoChange - NoBranch chosen_branch -> withBackend (st ^. stateContext) $ \bak -> + NoBranch chosen_branch -> withStateBackend st $ \bak -> do p' <- if chosen_branch then return p else notPred sym p let frm = if chosen_branch then tp else fp addAssumption bak (BranchCondition loc (pausedLoc frm) p') - ExecutionFeatureNewState <$> runReaderT (resumeFrame frm (asContFrame (st^.stateTree))) st + ExecutionFeatureNewState <$> runReaderT (resumeFrame frm (asContFrame (st ^. stateTree))) st UnsatisfiableContext -> return (ExecutionFeatureNewState (AbortState (InfeasibleBranch loc) st)) where 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 --- a/src/Lang/Crucible/Simulator/RecordAndReplay.hs +++ b/src/Lang/Crucible/Simulator/RecordAndReplay.hs @@ -20,6 +20,7 @@ replayTraceLength, RecordedTrace, getRecordedTrace, + getConcreteRecordedTrace, recordFeature, replayFeature, initialTrace, @@ -28,22 +29,23 @@ ) where import Control.Exception qualified as X -import Control.Lens ((%~), (&), (^.)) -import Control.Lens qualified as Lens import Data.Foldable qualified as F +import Data.Function ((&)) import Data.Kind (Type) -import Data.Text qualified as Text import Data.Sequence qualified as Seq +import Data.Text qualified as Text import Lang.Crucible.Backend qualified as CB import Lang.Crucible.CFG.Core qualified as C import Lang.Crucible.FunctionHandle qualified as C -import Lang.Crucible.Panic (panic) import Lang.Crucible.Simulator qualified as C import Lang.Crucible.Simulator.EvalStmt qualified as C import Lang.Crucible.Simulator.ExecutionTree qualified as C import Lang.Crucible.Simulator.GlobalState qualified as C import Lang.Crucible.Simulator.SymSequence qualified as CSSS import Lang.Crucible.Types qualified as CT +import Lens.Micro ((^.), (%~)) +import Lens.Micro qualified as Lens +import Lens.Micro.TH (makeLenses) import What4.Interface qualified as W4 import What4.Partial qualified as W4P @@ -83,7 +85,7 @@ , _initialTrace :: (RecordedTrace sym) } -- ^ constructor intentionally not exported -Lens.makeLenses ''ReplayState +makeLenses ''ReplayState -- | Constructor for 'RecordState' mkRecordState :: @@ -254,10 +256,22 @@ -- API, but it could be exported in the future if necessary. -- | Obtain a 'RecordedTrace' after execution. --- --- This currently requires concretizing the trace, because there is no efficient --- reverse operation for 'CSSS.SymSequence'. getRecordedTrace :: + C.SymGlobalState sym -> + RecordState p sym ext rtp -> + sym -> + IO (RecordedTrace sym) +getRecordedTrace globals (RecordState g) sym = do + case C.lookupGlobal g globals of + Nothing -> X.throw TraceGlobalNotDefined + Just s -> RecordedTrace <$> CSSS.reverseSymSequence sym s + +-- | Obtain a 'RecordedTrace' after execution using concrete evaluation. +-- +-- When a concrete evaluation function for 'W4.Pred's is available and only the +-- concretized trace is desired, this is more performant than the more general +-- 'getRecordedTrace'. +getConcreteRecordedTrace :: W4.IsExprBuilder sym => C.SymGlobalState sym -> RecordState p sym ext rtp -> @@ -265,26 +279,15 @@ -- | Evaluation for booleans, usually a 'What4.Expr.GroundEval.GroundEvalFn' (W4.Pred sym -> IO Bool) -> IO (RecordedTrace sym) -getRecordedTrace globals (RecordState g) sym evalBool = do +getConcreteRecordedTrace globals (RecordState g) sym evalBool = do case C.lookupGlobal g globals of Nothing -> X.throw TraceGlobalNotDefined Just s -> RecordedTrace <$> concretizeAndReverseTrace s where concretizeAndReverseTrace s = do - concretized <- CSSS.concretizeSymSequence evalBool (evalStr sym) s + concretized <- CSSS.concretizeSymSequence evalBool pure s let reversed = Seq.reverse concretized - symbolized <- mapM (W4.stringLit sym . W4.UnicodeLiteral) reversed - CSSS.fromListSymSequence sym (F.toList symbolized) - - evalStr :: - W4.IsExpr (W4.SymExpr sym) => - sym -> - W4.SymString sym W4.Unicode -> - IO Text.Text - evalStr _sym s = - case W4.asString s of - Just (W4.UnicodeLiteral s') -> pure s' - Nothing -> panic "getRecordedTrace" ["Non-literal trace element?"] + CSSS.fromListSymSequence sym (F.toList reversed) {- | Inserts a recorded trace into the state's replay trace variable The replay feature will follow this trace if it is enabled @@ -338,7 +341,7 @@ | stop -> badPath | otherwise -> pure C.ExecutionFeatureNoChange W4P.PE valid (expectedLoc, rest) -> - C.withBackend (st ^. C.stateContext) $ \bak -> do + C.withStateBackend st $ \bak -> do let msg = "Trace must be valid" CB.assert bak valid (C.AssertFailureSimError msg "") 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 @@ -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 @@ -2,9 +2,9 @@ module Main (main) where -import Control.Lens ((^.)) import Data.List (isInfixOf) import Data.Maybe (fromMaybe) +import Lens.Micro ((^.)) import Test.Hspec import Test.Tasty diff --git a/test/helpers/SymSequence.hs b/test/helpers/SymSequence.hs --- a/test/helpers/SymSequence.hs +++ b/test/helpers/SymSequence.hs @@ -1,300 +1,15 @@ -{-# LANGUAGE EmptyDataDeriving #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} {-# LANGUAGE ImportQualifiedPost #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} module SymSequence (tests) where -import Control.Monad.IO.Class (liftIO) -import Data.Foldable qualified as F -import Data.List qualified as List -import Data.Maybe qualified as Maybe -import Data.Parameterized.Nonce qualified as Nonce -import Data.Parameterized.Some (Some(Some)) -import Hedgehog (Gen) -import Hedgehog qualified as H -import Hedgehog.Gen qualified as Gen -import Hedgehog.Range qualified as Range -import Lang.Crucible.Backend (SomeBackend(SomeBackend), backendGetSym) -import Lang.Crucible.Backend.Simple (newSimpleBackend) -import Lang.Crucible.Simulator.SymSequence (SymSequence) -import Lang.Crucible.Simulator.SymSequence qualified as S import Test.Tasty qualified as TT -import Test.Tasty.Hedgehog qualified as TTH -import What4.Expr (EmptyExprBuilderState(EmptyExprBuilderState)) -import What4.Expr.Builder (newExprBuilder) -import What4.FloatMode (FloatModeRepr(FloatIEEERepr)) -import What4.Interface qualified as WI -import What4.Partial qualified as WP ---------------------------------------------------------------------- --- Tests +import SymSequence.Properties qualified as Properties +import SymSequence.Reverse qualified as Reverse tests :: TT.TestTree tests = - TTH.testProperty - "propSame" - -- This is a big API, so we want adequate coverage (default is 100) - (H.withTests 4096 propSame) - --- | Check that a generated API interaction has the same effect when interpreted --- with either 'SymSequence' or lists. -propSame :: H.Property -propSame = - H.property $ do - Some (SomeBackend bak) <- liftIO mkBackend - let sym = backendGetSym bak - op <- H.forAll (Gen.sized $ \n -> genList (H.unSize n) Gen.bool) - let l = opList op - s <- liftIO (opSeq sym op) - l' <- liftIO (F.toList <$> asSeq sym s) - l H.=== l' - where - asSeq sym = - S.concretizeSymSequence (pure . asConstPred (Just sym)) pure - ---------------------------------------------------------------------- --- Helpers - -mkBackend :: IO (Some SomeBackend) -mkBackend = do - sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState Nonce.globalNonceGenerator - Some . SomeBackend <$> newSimpleBackend sym - --- Requires that the predicate is concrete -asConstPred :: - WI.IsExprBuilder sym => - proxy sym -> - WI.Pred sym -> - Bool -asConstPred _proxy p = - case WI.asConstantPred p of - Just True -> True - Just False -> False - Nothing -> error "non-constant predicate?" - ---------------------------------------------------------------------- --- Op - -data Elem a deriving Show - -data List a deriving Show - --- TODO: Replace with `Seq` for performance -type family AsList t where - AsList (List a) = [a] - AsList (Elem a) = a - AsList (Maybe a) = Maybe (AsList a) - AsList (a, b) = (AsList a, AsList b) - AsList a = a - -type family AsSeq sym t where - AsSeq sym (List a) = SymSequence sym a - AsSeq sym (Elem a) = a - AsSeq sym (Maybe a) = Maybe (AsSeq sym a) - AsSeq sym (a, b) = (AsSeq sym a, AsSeq sym b) - AsSeq sym a = a - --- | An interaction with the 'SymSequence' API -data Op a t where - -- Generic functions - OTrue :: Op a Bool - OFalse :: Op a Bool - OFst :: Op a (l, r) -> Op a l - OSnd :: Op a (l, r) -> Op a r - OElem :: a -> Op a (Elem a) - OFromMaybe :: Op a t -> Op a (Maybe t) -> Op a t - - -- Constructors - ONil :: Op a (List a) - OCons :: Op a (Elem a) -> Op a (List a) -> Op a (List a) - OAppend :: Op a (List a) -> Op a (List a) -> Op a (List a) - OMux :: Op a Bool -> Op a (List a) -> Op a (List a) -> Op a (List a) - - -- Operations - OUncons :: Op a (List a) -> Op a (Maybe (Elem a), (List a)) - OLength :: Op a (List a) -> Op a Integer - -- TODO: isNil, head, tail - -sexp :: [String] -> String -sexp s = '(' : (unwords s ++ ")") - -fun :: String -> [String] -> String -fun f s = sexp (f:s) - -fun1 :: Show a => String -> a -> String -fun1 f a = fun f [show a] - -fun2 :: (Show a, Show b) => String -> a -> b -> String -fun2 f a b = fun f [show a, show b] - -fun3 :: (Show a, Show b, Show c) => String -> a -> b -> c -> String -fun3 f a b c = fun f [show a, show b, show c] - -instance Show a => Show (Op a t) where - show = - \case - -- Generic functions - OTrue -> "true" - OFalse -> "false" - OFst t -> fun1 "fst" t - OSnd t -> fun1 "snd" t - OElem a -> show a - OFromMaybe a m -> fun2 "fromMaybe" a m - - -- Constructors - ONil -> "nil" - OCons l r -> fun2 "cons" l r - OAppend l r -> fun2 "append" l r - OMux b l r -> fun3 "mux" b l r - - -- Operations - OUncons l -> fun1 "uncons" l - OLength l -> fun1 "length" l - ---------------------------------------------------------------------- --- Generating Op - -genBool :: Gen (Op a Bool) -genBool = - Gen.choice - [ pure OTrue - , pure OFalse + TT.testGroup "SymSequence" + [ Properties.tests + , Reverse.tests ] - -genElem :: - Int -> - Gen a -> - Gen (Op a (Elem a)) -genElem sz genA = - if sz <= 0 - then OElem <$> genA - else - Gen.choice - [ OElem <$> genA - , OFromMaybe - <$> genElem (sz - 1) genA - <*> (OFst <$> (OUncons <$> genList (sz - 1) genA)) - ] - -genList :: - Int -> - Gen a -> - Gen (Op a (List a)) -genList sz genA = - if sz <= 0 - then pure ONil - else - Gen.choice - [ genCons - , genAppend - , genMux - ] - where - sub1 = genList (sz - 1) genA - sub2 = do - let budget = max 0 (sz - 1) - bl <- Gen.integral (Range.linear 0 budget) - let br = max 0 (budget - bl) - l <- genList bl genA - r <- genList br genA - pure (l, r) - - genCons = OCons <$> genElem (sz - 1) genA <*> sub1 - - genAppend = uncurry OAppend <$> sub2 - - genMux = do - b <- genBool - uncurry (OMux b) <$> sub2 - ---------------------------------------------------------------------- --- Interpreting Op - -opList :: Op a t -> AsList t -opList = - \case - -- Generic functions - OTrue -> True - OFalse -> False - OFst t -> fst (opList t) - OSnd t -> snd (opList t) - OElem a -> a - OFromMaybe a m -> Maybe.fromMaybe (opList a) (opList m) - - -- Constructors - ONil -> [] - OCons a l -> opList a : opList l - OAppend l r -> opList l ++ opList r - OMux b l r -> if opList b then opList l else opList r - - -- Operations - OUncons l -> - let l' = opList l in - case List.uncons l' of - Just (hd, tl) -> (Just hd, tl) - Nothing -> (Nothing, l') - OLength l -> fromIntegral @Int @Integer (length (opList l)) -- safe - -opSeq :: - WI.IsExprBuilder sym => - sym -> - Op a t -> - IO (AsSeq sym t) -opSeq sym = - \case - -- Generic functions - OTrue -> pure True - OFalse -> pure False - OFst t -> fst <$> opSeq sym t - OSnd t -> snd <$> opSeq sym t - OElem a -> pure a - OFromMaybe a m -> - Maybe.fromMaybe - <$> opSeq sym a - <*> opSeq sym m - - -- Constructors - ONil -> pure S.SymSequenceNil - OCons a l -> - S.SymSequenceCons - <$> Nonce.freshNonce Nonce.globalNonceGenerator - <*> opSeq sym a - <*> opSeq sym l - OAppend l r -> - S.SymSequenceAppend - <$> Nonce.freshNonce Nonce.globalNonceGenerator - <*> opSeq sym l - <*> opSeq sym r - OMux b l r -> do - b' <- opSeq sym b - let b'' = if b' then WI.truePred sym else WI.falsePred sym - S.SymSequenceMerge - <$> Nonce.freshNonce Nonce.globalNonceGenerator - <*> pure b'' - <*> opSeq sym l - <*> opSeq sym r - - -- Operations - OUncons l -> do - l' <- opSeq sym l - let interpPred p x y = - if asConstPred (Just sym) p - then pure x - else pure y - pe <- S.unconsSymSequence sym interpPred l' - case pe of - WP.Unassigned -> pure (Nothing, l') - WP.PE _ (hd, tl) -> -- TODO: assert pred is truePred - pure (Just hd, tl) - OLength s -> do - l <- S.lengthSymSequence sym =<< opSeq sym s - case WI.asInteger (WI.natToIntegerPure l) of - Just l' -> pure l' - Nothing -> error "SymSequence: symbolic length" 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