{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fprint-explicit-kinds -Wall #-}
module Lang.Crucible.Simulator.ExecutionTree
(
GlobalPair(..)
, gpValue
, gpGlobals
, TopFrame
, crucibleTopFrame
, overrideTopFrame
, CrucibleBranchTarget(..)
, ppBranchTarget
, AbortedResult(..)
, SomeFrame(..)
, filterCrucibleFrames
, arFrames
, ppExceptionContext
, PartialResult(..)
, PartialResultFrame
, partialValue
, ExecResult(..)
, ExecState(..)
, ExecCont
, RunningStateInfo(..)
, ResolvedCall(..)
, resolvedCallHandle
, execResultContext
, execStateContext
, execStateSimState
, ValueFromValue(..)
, ValueFromFrame(..)
, PendingPartialMerges(..)
, ResolvedJump(..)
, ControlResumption(..)
, PausedFrame(..)
, VFFOtherPath(..)
, FrameRetType
, ReturnHandler(..)
, ActiveTree(..)
, singletonTree
, activeFrames
, actContext
, actFrame
, Override(..)
, FnState(..)
, FunctionBindings(..)
, ExtensionImpl(..)
, EvalStmtFunc
, emptyExtensionImpl
, IsSymInterfaceProof
, SimContext(..)
, Metric(..)
, initSimContext
, withBackend
, ctxSymInterface
, functionBindings
, cruciblePersonality
, profilingMetrics
, SimState(..)
, SomeSimState(..)
, initSimState
, stateLocation
, AbortHandler(..)
, CrucibleState
, stateTree
, abortHandler
, stateContext
, stateCrucibleFrame
, stateSymInterface
, stateSolverProof
, stateIntrinsicTypes
, stateOverrideFrame
, stateGlobals
, stateConfiguration
) where
import Control.Lens
import Control.Monad.Reader
import Data.Kind
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Parameterized.Ctx
import qualified Data.Parameterized.Context as Ctx
import Data.Text (Text)
import System.Exit (ExitCode)
import System.IO
import qualified Prettyprinter as PP
import What4.Config (Config)
import What4.Interface (Pred, getConfiguration)
import What4.FunctionName (FunctionName, startFunctionName)
import What4.ProgramLoc (ProgramLoc, plSourceLoc)
import Lang.Crucible.Backend
( IsSymInterface, IsSymBackend(..), HasSymInterface(..)
, AbortExecReason, SomeBackend(..), FrameIdentifier, Assumptions
)
import Lang.Crucible.CFG.Core (BlockID, CFG, CFGPostdom, StmtSeq)
import Lang.Crucible.CFG.Extension (StmtExtension, ExprExtension)
import Lang.Crucible.FunctionHandle (FnHandleMap, HandleAllocator, mkHandle')
import Lang.Crucible.Simulator.CallFrame
import Lang.Crucible.Simulator.Evaluation (EvalAppFunc)
import Lang.Crucible.Simulator.GlobalState (SymGlobalState)
import Lang.Crucible.Simulator.Intrinsics (IntrinsicTypes)
import Lang.Crucible.Simulator.RegMap (RegMap, emptyRegMap, RegValue, RegEntry)
import Lang.Crucible.Types
data GlobalPair sym (v :: Type) =
GlobalPair
{ forall sym v. GlobalPair sym v -> v
_gpValue :: !v
, forall sym v. GlobalPair sym v -> SymGlobalState sym
_gpGlobals :: !(SymGlobalState sym)
}
gpValue :: Lens (GlobalPair sym u) (GlobalPair sym v) u v
gpValue :: forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue = (GlobalPair sym u -> u)
-> (GlobalPair sym u -> v -> GlobalPair sym v)
-> Lens (GlobalPair sym u) (GlobalPair sym v) u v
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens GlobalPair sym u -> u
forall sym v. GlobalPair sym v -> v
_gpValue (\GlobalPair sym u
s v
v -> GlobalPair sym u
s { _gpValue = v })
gpGlobals :: Simple Lens (GlobalPair sym u) (SymGlobalState sym)
gpGlobals :: forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals = (GlobalPair sym u -> SymGlobalState sym)
-> (GlobalPair sym u -> SymGlobalState sym -> GlobalPair sym u)
-> Lens
(GlobalPair sym u)
(GlobalPair sym u)
(SymGlobalState sym)
(SymGlobalState sym)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens GlobalPair sym u -> SymGlobalState sym
forall sym v. GlobalPair sym v -> SymGlobalState sym
_gpGlobals (\GlobalPair sym u
s SymGlobalState sym
v -> GlobalPair sym u
s { _gpGlobals = v })
type TopFrame sym ext f a = GlobalPair sym (SimFrame sym ext f a)
crucibleTopFrame ::
Lens (TopFrame sym ext (CrucibleLang blocks r) ('Just args))
(TopFrame sym ext (CrucibleLang blocks r) ('Just args'))
(CallFrame sym ext blocks r args)
(CallFrame sym ext blocks r args')
crucibleTopFrame :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(r :: CrucibleType) (args :: Ctx CrucibleType)
(args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r args
-> f (CallFrame sym ext blocks r args'))
-> TopFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
-> f (TopFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args'))
crucibleTopFrame = (SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args')))
-> GlobalPair
sym
(SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args))
-> f (GlobalPair
sym
(SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args')))
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue ((SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args')))
-> GlobalPair
sym
(SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args))
-> f (GlobalPair
sym
(SimFrame
sym
ext
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) args'))))
-> ((CallFrame sym ext blocks r args
-> f (CallFrame sym ext blocks r args'))
-> SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args')))
-> (CallFrame sym ext blocks r args
-> f (CallFrame sym ext blocks r args'))
-> GlobalPair
sym
(SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args))
-> f (GlobalPair
sym
(SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args')))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CallFrame sym ext blocks r args
-> f (CallFrame sym ext blocks r args'))
-> SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args'))
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(r :: CrucibleType) (args :: Ctx CrucibleType)
(blocks' :: Ctx (Ctx CrucibleType)) (r' :: CrucibleType)
(args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r args
-> f (CallFrame sym ext blocks' r' args'))
-> SimFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
sym
ext
(CrucibleLang blocks' r')
('Just @(Ctx CrucibleType) args'))
crucibleSimFrame
{-# INLINE crucibleTopFrame #-}
overrideTopFrame ::
Lens (TopFrame sym ext (OverrideLang r) ('Just args))
(TopFrame sym ext (OverrideLang r') ('Just args'))
(OverrideFrame sym r args)
(OverrideFrame sym r' args')
overrideTopFrame :: forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType)
(r' :: CrucibleType) (args' :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> TopFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
-> f (TopFrame
sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args'))
overrideTopFrame = (SimFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args')))
-> GlobalPair
sym
(SimFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args))
-> f (GlobalPair
sym
(SimFrame
sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args')))
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue ((SimFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args')))
-> GlobalPair
sym
(SimFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args))
-> f (GlobalPair
sym
(SimFrame
sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args'))))
-> ((OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> SimFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args')))
-> (OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> GlobalPair
sym
(SimFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args))
-> f (GlobalPair
sym
(SimFrame
sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args')))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> SimFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args'))
forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType)
(r' :: CrucibleType) (args' :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> SimFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args'))
overrideSimFrame
{-# INLINE overrideTopFrame #-}
data AbortedResult sym ext where
AbortedExec ::
!AbortExecReason ->
!(GlobalPair sym (SimFrame sym ext l args)) ->
AbortedResult sym ext
AbortedExit ::
!ExitCode ->
AbortedResult sym ext
AbortedBranch ::
!ProgramLoc ->
!(Pred sym) ->
!(AbortedResult sym ext) ->
!(AbortedResult sym ext) ->
AbortedResult sym ext
data SomeFrame (f :: fk -> argk -> Type) = forall l a . SomeFrame !(f l a)
filterCrucibleFrames :: SomeFrame (SimFrame sym ext) -> Maybe ProgramLoc
filterCrucibleFrames :: forall sym ext.
SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> Maybe ProgramLoc
filterCrucibleFrames (SomeFrame (MF CallFrame sym ext blocks ret args1
f)) = ProgramLoc -> Maybe ProgramLoc
forall a. a -> Maybe a
Just (CallFrame sym ext blocks ret args1 -> ProgramLoc
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> ProgramLoc
frameProgramLoc CallFrame sym ext blocks ret args1
f)
filterCrucibleFrames SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
_ = Maybe ProgramLoc
forall a. Maybe a
Nothing
arFrames :: Simple Traversal (AbortedResult sym ext) (SomeFrame (SimFrame sym ext))
arFrames :: forall sym ext (f :: Type -> Type).
Applicative f =>
(SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
@Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)))
-> AbortedResult sym ext -> f (AbortedResult sym ext)
arFrames SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
@Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
h (AbortedExec AbortExecReason
e GlobalPair sym (SimFrame sym ext l args)
p) =
(\(SomeFrame SimFrame sym ext l a
f') -> AbortExecReason
-> GlobalPair sym (SimFrame sym ext l a) -> AbortedResult sym ext
forall sym ext l (args :: Maybe (Ctx CrucibleType)).
AbortExecReason
-> GlobalPair sym (SimFrame sym ext l args)
-> AbortedResult sym ext
AbortedExec AbortExecReason
e (GlobalPair sym (SimFrame sym ext l args)
p GlobalPair sym (SimFrame sym ext l args)
-> (GlobalPair sym (SimFrame sym ext l args)
-> GlobalPair sym (SimFrame sym ext l a))
-> GlobalPair sym (SimFrame sym ext l a)
forall a b. a -> (a -> b) -> b
& (SimFrame sym ext l args -> Identity (SimFrame sym ext l a))
-> GlobalPair sym (SimFrame sym ext l args)
-> Identity (GlobalPair sym (SimFrame sym ext l a))
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue ((SimFrame sym ext l args -> Identity (SimFrame sym ext l a))
-> GlobalPair sym (SimFrame sym ext l args)
-> Identity (GlobalPair sym (SimFrame sym ext l a)))
-> SimFrame sym ext l a
-> GlobalPair sym (SimFrame sym ext l args)
-> GlobalPair sym (SimFrame sym ext l a)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ SimFrame sym ext l a
f'))
(SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> AbortedResult sym ext)
-> f (SomeFrame
@Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
-> f (AbortedResult sym ext)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
@Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
h (SimFrame sym ext l args
-> SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
forall fk argk (f :: fk -> argk -> Type) (l :: fk) (a :: argk).
f l a -> SomeFrame @fk @argk f
SomeFrame (GlobalPair sym (SimFrame sym ext l args)
pGlobalPair sym (SimFrame sym ext l args)
-> Getting
(SimFrame sym ext l args)
(GlobalPair sym (SimFrame sym ext l args))
(SimFrame sym ext l args)
-> SimFrame sym ext l args
forall s a. s -> Getting a s a -> a
^.Getting
(SimFrame sym ext l args)
(GlobalPair sym (SimFrame sym ext l args))
(SimFrame sym ext l args)
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue))
arFrames SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
@Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
_ (AbortedExit ExitCode
ec) = AbortedResult sym ext -> f (AbortedResult sym ext)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ExitCode -> AbortedResult sym ext
forall sym ext. ExitCode -> AbortedResult sym ext
AbortedExit ExitCode
ec)
arFrames SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
@Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
h (AbortedBranch ProgramLoc
predicate Pred sym
loc AbortedResult sym ext
r AbortedResult sym ext
s) =
ProgramLoc
-> Pred sym
-> AbortedResult sym ext
-> AbortedResult sym ext
-> AbortedResult sym ext
forall sym ext.
ProgramLoc
-> Pred sym
-> AbortedResult sym ext
-> AbortedResult sym ext
-> AbortedResult sym ext
AbortedBranch ProgramLoc
predicate Pred sym
loc (AbortedResult sym ext
-> AbortedResult sym ext -> AbortedResult sym ext)
-> f (AbortedResult sym ext)
-> f (AbortedResult sym ext -> AbortedResult sym ext)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
@Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)))
-> AbortedResult sym ext -> f (AbortedResult sym ext)
forall sym ext (f :: Type -> Type).
Applicative f =>
(SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
@Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)))
-> AbortedResult sym ext -> f (AbortedResult sym ext)
arFrames SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
@Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
h AbortedResult sym ext
r
f (AbortedResult sym ext -> AbortedResult sym ext)
-> f (AbortedResult sym ext) -> f (AbortedResult sym ext)
forall a b. f (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
@Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)))
-> AbortedResult sym ext -> f (AbortedResult sym ext)
forall sym ext (f :: Type -> Type).
Applicative f =>
(SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
@Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)))
-> AbortedResult sym ext -> f (AbortedResult sym ext)
arFrames SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
@Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
h AbortedResult sym ext
s
ppExceptionContext :: [SomeFrame (SimFrame sym ext)] -> PP.Doc ann
ppExceptionContext :: forall sym ext ann.
[SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
-> Doc ann
ppExceptionContext [] = Doc ann
forall a. Monoid a => a
mempty
ppExceptionContext [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
frames = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat ((SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> Doc ann)
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
-> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> Doc ann
forall sym ext ann.
SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> Doc ann
pp ([SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall a. HasCallStack => [a] -> [a]
init [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
frames))
where
pp :: SomeFrame (SimFrame sym ext) -> PP.Doc ann
pp :: forall sym ext ann.
SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> Doc ann
pp (SomeFrame (OF OverrideFrame sym ret args1
f)) =
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"When calling" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> FunctionName -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow (OverrideFrame sym ret args1
fOverrideFrame sym ret args1
-> Getting FunctionName (OverrideFrame sym ret args1) FunctionName
-> FunctionName
forall s a. s -> Getting a s a -> a
^.Getting FunctionName (OverrideFrame sym ret args1) FunctionName
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(FunctionName -> f FunctionName)
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args)
override)
pp (SomeFrame (MF CallFrame sym ext blocks ret args1
f)) =
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"In" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> SomeHandle -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow (CallFrame sym ext blocks ret args1 -> SomeHandle
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> SomeHandle
frameHandle CallFrame sym ext blocks ret args1
f) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+>
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"at" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Position -> Doc ann
PP.pretty (ProgramLoc -> Position
plSourceLoc (CallFrame sym ext blocks ret args1 -> ProgramLoc
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> ProgramLoc
frameProgramLoc CallFrame sym ext blocks ret args1
f))
pp (SomeFrame (RF FunctionName
nm RegEntry sym (FrameRetType l)
_v)) =
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"While returning value from" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> FunctionName -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow FunctionName
nm
data PartialResult sym ext (v :: Type)
= TotalRes !(GlobalPair sym v)
| PartialRes !ProgramLoc
!(Pred sym)
!(GlobalPair sym v)
!(AbortedResult sym ext)
partialValue ::
Lens (PartialResult sym ext u)
(PartialResult sym ext v)
(GlobalPair sym u)
(GlobalPair sym v)
partialValue :: forall sym ext u v (f :: Type -> Type).
Functor f =>
(GlobalPair sym u -> f (GlobalPair sym v))
-> PartialResult sym ext u -> f (PartialResult sym ext v)
partialValue GlobalPair sym u -> f (GlobalPair sym v)
f (TotalRes GlobalPair sym u
x) = GlobalPair sym v -> PartialResult sym ext v
forall sym ext v. GlobalPair sym v -> PartialResult sym ext v
TotalRes (GlobalPair sym v -> PartialResult sym ext v)
-> f (GlobalPair sym v) -> f (PartialResult sym ext v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GlobalPair sym u -> f (GlobalPair sym v)
f GlobalPair sym u
x
partialValue GlobalPair sym u -> f (GlobalPair sym v)
f (PartialRes ProgramLoc
loc Pred sym
p GlobalPair sym u
x AbortedResult sym ext
r) = (\GlobalPair sym v
y -> ProgramLoc
-> Pred sym
-> GlobalPair sym v
-> AbortedResult sym ext
-> PartialResult sym ext v
forall sym ext v.
ProgramLoc
-> Pred sym
-> GlobalPair sym v
-> AbortedResult sym ext
-> PartialResult sym ext v
PartialRes ProgramLoc
loc Pred sym
p GlobalPair sym v
y AbortedResult sym ext
r) (GlobalPair sym v -> PartialResult sym ext v)
-> f (GlobalPair sym v) -> f (PartialResult sym ext v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GlobalPair sym u -> f (GlobalPair sym v)
f GlobalPair sym u
x
{-# INLINE partialValue #-}
data ResolvedCall p sym ext ret where
OverrideCall ::
!(Override p sym ext args ret) ->
!(OverrideFrame sym ret args) ->
ResolvedCall p sym ext ret
CrucibleCall ::
!(BlockID blocks args) ->
!(CallFrame sym ext blocks ret args) ->
ResolvedCall p sym ext ret
resolvedCallHandle :: ResolvedCall p sym ext ret -> SomeHandle
resolvedCallHandle :: forall p sym ext (ret :: CrucibleType).
ResolvedCall p sym ext ret -> SomeHandle
resolvedCallHandle (OverrideCall Override p sym ext args ret
_ OverrideFrame sym ret args
frm) = OverrideFrame sym ret args
frm OverrideFrame sym ret args
-> Getting SomeHandle (OverrideFrame sym ret args) SomeHandle
-> SomeHandle
forall s a. s -> Getting a s a -> a
^. Getting SomeHandle (OverrideFrame sym ret args) SomeHandle
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(SomeHandle -> f SomeHandle)
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args)
overrideHandle
resolvedCallHandle (CrucibleCall BlockID blocks args
_ CallFrame sym ext blocks ret args
frm) = CallFrame sym ext blocks ret args -> SomeHandle
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> SomeHandle
frameHandle CallFrame sym ext blocks ret args
frm
data ExecResult p sym ext (r :: Type)
=
FinishedResult !(SimContext p sym ext) !(PartialResult sym ext r)
| AbortedResult !(SimContext p sym ext) !(AbortedResult sym ext)
| TimeoutResult !(ExecState p sym ext r)
execResultContext :: ExecResult p sym ext r -> SimContext p sym ext
execResultContext :: forall p sym ext r. ExecResult p sym ext r -> SimContext p sym ext
execResultContext (FinishedResult SimContext p sym ext
ctx PartialResult sym ext r
_) = SimContext p sym ext
ctx
execResultContext (AbortedResult SimContext p sym ext
ctx AbortedResult sym ext
_) = SimContext p sym ext
ctx
execResultContext (TimeoutResult ExecState p sym ext r
exst) = ExecState p sym ext r -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
execStateContext ExecState p sym ext r
exst
execStateContext :: ExecState p sym ext r -> SimContext p sym ext
execStateContext :: forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
execStateContext = \case
ResultState ExecResult p sym ext r
res -> ExecResult p sym ext r -> SimContext p sym ext
forall p sym ext r. ExecResult p sym ext r -> SimContext p sym ext
execResultContext ExecResult p sym ext r
res
AbortState AbortExecReason
_ SimState p sym ext r f a
st -> SimState p sym ext r f a
stSimState p sym ext r f a
-> Getting
(SimContext p sym ext)
(SimState p sym ext r f a)
(SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
(SimContext p sym ext)
(SimState p sym ext r f a)
(SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
UnwindCallState ValueFromValue p sym ext r r
_ AbortedResult sym ext
_ SimState p sym ext r f a
st -> SimState p sym ext r f a
stSimState p sym ext r f a
-> Getting
(SimContext p sym ext)
(SimState p sym ext r f a)
(SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
(SimContext p sym ext)
(SimState p sym ext r f a)
(SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
CallState ReturnHandler ret p sym ext r f a
_ ResolvedCall p sym ext ret
_ SimState p sym ext r f a
st -> SimState p sym ext r f a
stSimState p sym ext r f a
-> Getting
(SimContext p sym ext)
(SimState p sym ext r f a)
(SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
(SimContext p sym ext)
(SimState p sym ext r f a)
(SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
TailCallState ValueFromValue p sym ext r ret
_ ResolvedCall p sym ext ret
_ SimState p sym ext r f a
st -> SimState p sym ext r f a
stSimState p sym ext r f a
-> Getting
(SimContext p sym ext)
(SimState p sym ext r f a)
(SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
(SimContext p sym ext)
(SimState p sym ext r f a)
(SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
ReturnState FunctionName
_ ValueFromValue p sym ext r ret
_ RegEntry sym ret
_ SimState p sym ext r f a
st -> SimState p sym ext r f a
stSimState p sym ext r f a
-> Getting
(SimContext p sym ext)
(SimState p sym ext r f a)
(SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
(SimContext p sym ext)
(SimState p sym ext r f a)
(SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
ControlTransferState ControlResumption p sym ext r f
_ SimState p sym ext r f ('Just @(Ctx CrucibleType) a)
st -> SimState p sym ext r f ('Just @(Ctx CrucibleType) a)
stSimState p sym ext r f ('Just @(Ctx CrucibleType) a)
-> Getting
(SimContext p sym ext)
(SimState p sym ext r f ('Just @(Ctx CrucibleType) a))
(SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
(SimContext p sym ext)
(SimState p sym ext r f ('Just @(Ctx CrucibleType) a))
(SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
RunningState RunningStateInfo blocks args
_ SimState
p
sym
ext
r
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) args)
st -> SimState
p
sym
ext
r
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) args)
stSimState
p
sym
ext
r
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) args)
-> Getting
(SimContext p sym ext)
(SimState
p
sym
ext
r
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) args))
(SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
(SimContext p sym ext)
(SimState
p
sym
ext
r
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) args))
(SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
SymbolicBranchState Pred sym
_ PausedFrame p sym ext r f
_ PausedFrame p sym ext r f
_ CrucibleBranchTarget f postdom_args
_ SimState p sym ext r f ('Just @(Ctx CrucibleType) args)
st -> SimState p sym ext r f ('Just @(Ctx CrucibleType) args)
stSimState p sym ext r f ('Just @(Ctx CrucibleType) args)
-> Getting
(SimContext p sym ext)
(SimState p sym ext r f ('Just @(Ctx CrucibleType) args))
(SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
(SimContext p sym ext)
(SimState p sym ext r f ('Just @(Ctx CrucibleType) args))
(SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
OverrideState Override p sym ext args ret
_ SimState
p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
st -> SimState
p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
stSimState
p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
-> Getting
(SimContext p sym ext)
(SimState
p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args))
(SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
(SimContext p sym ext)
(SimState
p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args))
(SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
BranchMergeState CrucibleBranchTarget f args
_ SimState p sym ext r f args
st -> SimState p sym ext r f args
stSimState p sym ext r f args
-> Getting
(SimContext p sym ext)
(SimState p sym ext r f args)
(SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
(SimContext p sym ext)
(SimState p sym ext r f args)
(SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
InitialState SimContext p sym ext
stctx SymGlobalState sym
_ AbortHandler p sym ext (RegEntry sym ret)
_ TypeRepr ret
_ ExecCont
p
sym
ext
(RegEntry sym ret)
(OverrideLang ret)
('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
_ -> SimContext p sym ext
stctx
execStateSimState :: ExecState p sym ext r
-> Maybe (SomeSimState p sym ext r)
execStateSimState :: forall p sym ext r.
ExecState p sym ext r -> Maybe (SomeSimState p sym ext r)
execStateSimState = \case
ResultState ExecResult p sym ext r
_ -> Maybe (SomeSimState p sym ext r)
forall a. Maybe a
Nothing
AbortState AbortExecReason
_ SimState p sym ext r f a
st -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f a
st)
UnwindCallState ValueFromValue p sym ext r r
_ AbortedResult sym ext
_ SimState p sym ext r f a
st -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f a
st)
CallState ReturnHandler ret p sym ext r f a
_ ResolvedCall p sym ext ret
_ SimState p sym ext r f a
st -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f a
st)
TailCallState ValueFromValue p sym ext r ret
_ ResolvedCall p sym ext ret
_ SimState p sym ext r f a
st -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f a
st)
ReturnState FunctionName
_ ValueFromValue p sym ext r ret
_ RegEntry sym ret
_ SimState p sym ext r f a
st -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f a
st)
ControlTransferState ControlResumption p sym ext r f
_ SimState p sym ext r f ('Just @(Ctx CrucibleType) a)
st -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f ('Just @(Ctx CrucibleType) a)
-> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f ('Just @(Ctx CrucibleType) a)
st)
RunningState RunningStateInfo blocks args
_ SimState
p
sym
ext
r
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) args)
st -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState
p
sym
ext
r
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) args)
-> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState
p
sym
ext
r
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) args)
st)
SymbolicBranchState Pred sym
_ PausedFrame p sym ext r f
_ PausedFrame p sym ext r f
_ CrucibleBranchTarget f postdom_args
_ SimState p sym ext r f ('Just @(Ctx CrucibleType) args)
st -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f ('Just @(Ctx CrucibleType) args)
-> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f ('Just @(Ctx CrucibleType) args)
st)
OverrideState Override p sym ext args ret
_ SimState
p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
st -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState
p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
-> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState
p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
st)
BranchMergeState CrucibleBranchTarget f args
_ SimState p sym ext r f args
st -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f args -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f args
st)
InitialState SimContext p sym ext
_ SymGlobalState sym
_ AbortHandler p sym ext (RegEntry sym ret)
_ TypeRepr ret
_ ExecCont
p
sym
ext
(RegEntry sym ret)
(OverrideLang ret)
('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
_ -> Maybe (SomeSimState p sym ext r)
forall a. Maybe a
Nothing
data ExecState p sym ext (rtp :: Type)
= ResultState
!(ExecResult p sym ext rtp)
| forall f a.
AbortState
!AbortExecReason
!(SimState p sym ext rtp f a)
| forall f a r.
UnwindCallState
!(ValueFromValue p sym ext rtp r)
!(AbortedResult sym ext)
!(SimState p sym ext rtp f a)
| forall f a ret.
CallState
!(ReturnHandler ret p sym ext rtp f a)
!(ResolvedCall p sym ext ret)
!(SimState p sym ext rtp f a)
| forall f a ret.
TailCallState
!(ValueFromValue p sym ext rtp ret)
!(ResolvedCall p sym ext ret)
!(SimState p sym ext rtp f a)
| forall f a ret.
ReturnState
!FunctionName
!(ValueFromValue p sym ext rtp ret)
!(RegEntry sym ret)
!(SimState p sym ext rtp f a)
| forall blocks r args.
RunningState
!(RunningStateInfo blocks args)
!(SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
| forall f args postdom_args.
SymbolicBranchState
!(Pred sym)
!(PausedFrame p sym ext rtp f)
!(PausedFrame p sym ext rtp f)
!(CrucibleBranchTarget f postdom_args)
!(SimState p sym ext rtp f ('Just args))
| forall f a.
ControlTransferState
!(ControlResumption p sym ext rtp f)
!(SimState p sym ext rtp f ('Just a))
| forall args ret.
OverrideState
!(Override p sym ext args ret)
!(SimState p sym ext rtp (OverrideLang ret) ('Just args))
| forall f args.
BranchMergeState
!(CrucibleBranchTarget f args)
!(SimState p sym ext rtp f args)
| forall ret. rtp ~ RegEntry sym ret =>
InitialState
!(SimContext p sym ext)
!(SymGlobalState sym)
!(AbortHandler p sym ext (RegEntry sym ret))
!(TypeRepr ret)
!(ExecCont p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx))
type ExecCont p sym ext r f a =
ReaderT (SimState p sym ext r f a) IO (ExecState p sym ext r)
data RunningStateInfo blocks args
= RunBlockStart !(BlockID blocks args)
| RunBlockEnd !(Some (BlockID blocks))
| RunReturnFrom !FunctionName
| RunPostBranchMerge !(BlockID blocks args)
data ResolvedJump sym blocks
= forall args.
ResolvedJump
!(BlockID blocks args)
!(RegMap sym args)
data ControlResumption p sym ext rtp f where
ContinueResumption ::
!(ResolvedJump sym blocks) ->
ControlResumption p sym ext rtp (CrucibleLang blocks r)
CheckMergeResumption ::
!(ResolvedJump sym blocks) ->
ControlResumption p sym ext rtp (CrucibleLang blocks r)
SwitchResumption ::
![(Pred sym, ResolvedJump sym blocks)] ->
ControlResumption p sym ext rtp (CrucibleLang blocks r)
OverrideResumption ::
ExecCont p sym ext rtp (OverrideLang r) ('Just args) ->
!(RegMap sym args) ->
ControlResumption p sym ext rtp (OverrideLang r)
data PausedFrame p sym ext rtp f
= forall old_args.
PausedFrame
{ ()
pausedFrame :: !(PartialResultFrame sym ext f ('Just old_args))
, forall p sym ext rtp f.
PausedFrame p sym ext rtp f -> ControlResumption p sym ext rtp f
resume :: !(ControlResumption p sym ext rtp f)
, forall p sym ext rtp f.
PausedFrame p sym ext rtp f -> Maybe ProgramLoc
pausedLoc :: !(Maybe ProgramLoc)
}
data VFFOtherPath p sym ext ret f args
= VFFActivePath
!(PausedFrame p sym ext ret f)
| VFFCompletePath
!(Assumptions sym)
!(PartialResultFrame sym ext f args)
data ValueFromFrame p sym ext (ret :: Type) (f :: Type)
= forall args.
VFFBranch
!(ValueFromFrame p sym ext ret f)
!FrameIdentifier
!ProgramLoc
!(Pred sym)
!(VFFOtherPath p sym ext ret f args)
!(CrucibleBranchTarget f args)
| VFFPartial
!(ValueFromFrame p sym ext ret f)
!ProgramLoc
!(Pred sym)
!(AbortedResult sym ext)
!PendingPartialMerges
| VFFEnd
!(ValueFromValue p sym ext ret (FrameRetType f))
data PendingPartialMerges =
NoNeedToAbort
| NeedsToBeAborted
data ValueFromValue p sym ext (ret :: Type) (top_return :: CrucibleType)
= forall args caller.
VFVCall
!(ValueFromFrame p sym ext ret caller)
!(SimFrame sym ext caller args)
!(ReturnHandler top_return p sym ext ret caller args)
| VFVPartial
!(ValueFromValue p sym ext ret top_return)
!ProgramLoc
!(Pred sym)
!(AbortedResult sym ext)
| (ret ~ RegEntry sym top_return) => VFVEnd
instance PP.Pretty (ValueFromValue p ext sym root rp) where
pretty :: forall ann. ValueFromValue p ext sym root rp -> Doc ann
pretty = ValueFromValue p ext sym root rp -> Doc ann
forall p ext sym root (rp :: CrucibleType) ann.
ValueFromValue p ext sym root rp -> Doc ann
ppValueFromValue
instance PP.Pretty (ValueFromFrame p ext sym ret f) where
pretty :: forall ann. ValueFromFrame p ext sym ret f -> Doc ann
pretty = ValueFromFrame p ext sym ret f -> Doc ann
forall p ext sym ret f ann.
ValueFromFrame p ext sym ret f -> Doc ann
ppValueFromFrame
instance PP.Pretty (VFFOtherPath ctx sym ext r f a) where
pretty :: forall ann. VFFOtherPath ctx sym ext r f a -> Doc ann
pretty (VFFActivePath PausedFrame ctx sym ext r f
_) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"active_path"
pretty (VFFCompletePath Assumptions sym
_ PartialResultFrame sym ext f a
_) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"complete_path"
ppValueFromFrame :: ValueFromFrame p sym ext ret f -> PP.Doc ann
ppValueFromFrame :: forall p ext sym ret f ann.
ValueFromFrame p ext sym ret f -> Doc ann
ppValueFromFrame ValueFromFrame p sym ext ret f
vff =
case ValueFromFrame p sym ext ret f
vff of
VFFBranch ValueFromFrame p sym ext ret f
ctx FrameIdentifier
_ ProgramLoc
_ Pred sym
_ VFFOtherPath p sym ext ret f args
other CrucibleBranchTarget f args
mp ->
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
[ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"intra_branch"
, Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
2 (VFFOtherPath p sym ext ret f args -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. VFFOtherPath p sym ext ret f args -> Doc ann
PP.pretty VFFOtherPath p sym ext ret f args
other)
, Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
2 (String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (CrucibleBranchTarget f args -> String
forall f (args :: Maybe (Ctx CrucibleType)).
CrucibleBranchTarget f args -> String
ppBranchTarget CrucibleBranchTarget f args
mp))
, ValueFromFrame p sym ext ret f -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ValueFromFrame p sym ext ret f -> Doc ann
PP.pretty ValueFromFrame p sym ext ret f
ctx
]
VFFPartial ValueFromFrame p sym ext ret f
ctx ProgramLoc
_ Pred sym
_ AbortedResult sym ext
_ PendingPartialMerges
_ ->
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
[ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"intra_partial"
, ValueFromFrame p sym ext ret f -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ValueFromFrame p sym ext ret f -> Doc ann
PP.pretty ValueFromFrame p sym ext ret f
ctx
]
VFFEnd ValueFromValue p sym ext ret (FrameRetType f)
ctx ->
ValueFromValue p sym ext ret (FrameRetType f) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann.
ValueFromValue p sym ext ret (FrameRetType f) -> Doc ann
PP.pretty ValueFromValue p sym ext ret (FrameRetType f)
ctx
ppValueFromValue :: ValueFromValue p sym ext root tp -> PP.Doc ann
ppValueFromValue :: forall p ext sym root (rp :: CrucibleType) ann.
ValueFromValue p ext sym root rp -> Doc ann
ppValueFromValue ValueFromValue p sym ext root tp
vfv =
case ValueFromValue p sym ext root tp
vfv of
VFVCall ValueFromFrame p sym ext root caller
ctx SimFrame sym ext caller args
_ ReturnHandler tp p sym ext root caller args
_ ->
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
[ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"call"
, ValueFromFrame p sym ext root caller -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ValueFromFrame p sym ext root caller -> Doc ann
PP.pretty ValueFromFrame p sym ext root caller
ctx
]
VFVPartial ValueFromValue p sym ext root tp
ctx ProgramLoc
_ Pred sym
_ AbortedResult sym ext
_ ->
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
[ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"inter_partial"
, ValueFromValue p sym ext root tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ValueFromValue p sym ext root tp -> Doc ann
PP.pretty ValueFromValue p sym ext root tp
ctx
]
ValueFromValue p sym ext root tp
VFVEnd -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"root"
parentFrames :: ValueFromFrame p sym ext r a -> [SomeFrame (SimFrame sym ext)]
parentFrames :: forall p sym ext r a.
ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
parentFrames ValueFromFrame p sym ext r a
c0 =
case ValueFromFrame p sym ext r a
c0 of
VFFBranch ValueFromFrame p sym ext r a
c FrameIdentifier
_ ProgramLoc
_ Pred sym
_ VFFOtherPath p sym ext r a args
_ CrucibleBranchTarget a args
_ -> ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall p sym ext r a.
ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
parentFrames ValueFromFrame p sym ext r a
c
VFFPartial ValueFromFrame p sym ext r a
c ProgramLoc
_ Pred sym
_ AbortedResult sym ext
_ PendingPartialMerges
_ -> ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall p sym ext r a.
ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
parentFrames ValueFromFrame p sym ext r a
c
VFFEnd ValueFromValue p sym ext r (FrameRetType a)
vfv -> ValueFromValue p sym ext r (FrameRetType a)
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall p sym ext r (a :: CrucibleType).
ValueFromValue p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
vfvParents ValueFromValue p sym ext r (FrameRetType a)
vfv
vfvParents :: ValueFromValue p sym ext r a -> [SomeFrame (SimFrame sym ext)]
vfvParents :: forall p sym ext r (a :: CrucibleType).
ValueFromValue p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
vfvParents ValueFromValue p sym ext r a
c0 =
case ValueFromValue p sym ext r a
c0 of
VFVCall ValueFromFrame p sym ext r caller
c SimFrame sym ext caller args
f ReturnHandler a p sym ext r caller args
_ -> SimFrame sym ext caller args
-> SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
forall fk argk (f :: fk -> argk -> Type) (l :: fk) (a :: argk).
f l a -> SomeFrame @fk @argk f
SomeFrame SimFrame sym ext caller args
f SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall a. a -> [a] -> [a]
: ValueFromFrame p sym ext r caller
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall p sym ext r a.
ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
parentFrames ValueFromFrame p sym ext r caller
c
VFVPartial ValueFromValue p sym ext r a
c ProgramLoc
_ Pred sym
_ AbortedResult sym ext
_ -> ValueFromValue p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall p sym ext r (a :: CrucibleType).
ValueFromValue p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
vfvParents ValueFromValue p sym ext r a
c
ValueFromValue p sym ext r a
VFVEnd -> []
data ReturnHandler (ret :: CrucibleType) p sym ext root f args where
ReturnToOverride ::
(RegEntry sym ret -> SimState p sym ext root (OverrideLang r) ('Just args) -> IO (ExecState p sym ext root))
->
ReturnHandler ret p sym ext root (OverrideLang r) ('Just args)
ReturnToCrucible ::
TypeRepr ret ->
StmtSeq ext blocks r (ctx ::> ret) ->
ReturnHandler ret p sym ext root (CrucibleLang blocks r) ('Just ctx)
TailReturnToCrucible ::
(ret ~ r) =>
ReturnHandler ret p sym ext root (CrucibleLang blocks r) ctx
type PartialResultFrame sym ext f args =
PartialResult sym ext (SimFrame sym ext f args)
data ActiveTree p sym ext root (f :: Type) args
= ActiveTree
{ forall p sym ext root f (args :: Maybe (Ctx CrucibleType)).
ActiveTree p sym ext root f args -> ValueFromFrame p sym ext root f
_actContext :: !(ValueFromFrame p sym ext root f)
, forall p sym ext root f (args :: Maybe (Ctx CrucibleType)).
ActiveTree p sym ext root f args
-> PartialResultFrame sym ext f args
_actResult :: !(PartialResultFrame sym ext f args)
}
singletonTree ::
TopFrame sym ext f args ->
ActiveTree p sym ext (RegEntry sym (FrameRetType f)) f args
singletonTree :: forall sym ext f (args :: Maybe (Ctx CrucibleType)) p.
TopFrame sym ext f args
-> ActiveTree p sym ext (RegEntry sym (FrameRetType f)) f args
singletonTree TopFrame sym ext f args
f = ActiveTree { _actContext :: ValueFromFrame p sym ext (RegEntry sym (FrameRetType f)) f
_actContext = ValueFromValue
p sym ext (RegEntry sym (FrameRetType f)) (FrameRetType f)
-> ValueFromFrame p sym ext (RegEntry sym (FrameRetType f)) f
forall p sym ext ret f.
ValueFromValue p sym ext ret (FrameRetType f)
-> ValueFromFrame p sym ext ret f
VFFEnd ValueFromValue
p sym ext (RegEntry sym (FrameRetType f)) (FrameRetType f)
forall p sym ext ret (top_return :: CrucibleType).
((ret :: Type) ~ (RegEntry sym top_return :: Type)) =>
ValueFromValue p sym ext ret top_return
VFVEnd
, _actResult :: PartialResultFrame sym ext f args
_actResult = TopFrame sym ext f args -> PartialResultFrame sym ext f args
forall sym ext v. GlobalPair sym v -> PartialResult sym ext v
TotalRes TopFrame sym ext f args
f
}
actContext ::
Lens (ActiveTree p sym ext root f args)
(ActiveTree p sym ext root f args)
(ValueFromFrame p sym ext root f)
(ValueFromFrame p sym ext root f)
actContext :: forall p sym ext root f (args :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(ValueFromFrame p sym ext root f
-> f (ValueFromFrame p sym ext root f))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args)
actContext = (ActiveTree p sym ext root f args
-> ValueFromFrame p sym ext root f)
-> (ActiveTree p sym ext root f args
-> ValueFromFrame p sym ext root f
-> ActiveTree p sym ext root f args)
-> Lens
(ActiveTree p sym ext root f args)
(ActiveTree p sym ext root f args)
(ValueFromFrame p sym ext root f)
(ValueFromFrame p sym ext root f)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens ActiveTree p sym ext root f args -> ValueFromFrame p sym ext root f
forall p sym ext root f (args :: Maybe (Ctx CrucibleType)).
ActiveTree p sym ext root f args -> ValueFromFrame p sym ext root f
_actContext (\ActiveTree p sym ext root f args
s ValueFromFrame p sym ext root f
v -> ActiveTree p sym ext root f args
s { _actContext = v })
actResult ::
Lens (ActiveTree p sym ext root f args0)
(ActiveTree p sym ext root f args1)
(PartialResult sym ext (SimFrame sym ext f args0))
(PartialResult sym ext (SimFrame sym ext f args1))
actResult :: forall p sym ext root f (args0 :: Maybe (Ctx CrucibleType))
(args1 :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(PartialResult sym ext (SimFrame sym ext f args0)
-> f (PartialResult sym ext (SimFrame sym ext f args1)))
-> ActiveTree p sym ext root f args0
-> f (ActiveTree p sym ext root f args1)
actResult = (ActiveTree p sym ext root f args0
-> PartialResult sym ext (SimFrame sym ext f args0))
-> (ActiveTree p sym ext root f args0
-> PartialResult sym ext (SimFrame sym ext f args1)
-> ActiveTree p sym ext root f args1)
-> Lens
(ActiveTree p sym ext root f args0)
(ActiveTree p sym ext root f args1)
(PartialResult sym ext (SimFrame sym ext f args0))
(PartialResult sym ext (SimFrame sym ext f args1))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens ActiveTree p sym ext root f args0
-> PartialResult sym ext (SimFrame sym ext f args0)
forall p sym ext root f (args :: Maybe (Ctx CrucibleType)).
ActiveTree p sym ext root f args
-> PartialResultFrame sym ext f args
_actResult ActiveTree p sym ext root f args0
-> PartialResult sym ext (SimFrame sym ext f args1)
-> ActiveTree p sym ext root f args1
forall {p} {sym} {ext} {root} {f}
{args :: Maybe (Ctx CrucibleType)}
{args :: Maybe (Ctx CrucibleType)}.
ActiveTree p sym ext root f args
-> PartialResultFrame sym ext f args
-> ActiveTree p sym ext root f args
setter
where setter :: ActiveTree p sym ext root f args
-> PartialResultFrame sym ext f args
-> ActiveTree p sym ext root f args
setter ActiveTree p sym ext root f args
s PartialResultFrame sym ext f args
v = ActiveTree { _actContext :: ValueFromFrame p sym ext root f
_actContext = ActiveTree p sym ext root f args -> ValueFromFrame p sym ext root f
forall p sym ext root f (args :: Maybe (Ctx CrucibleType)).
ActiveTree p sym ext root f args -> ValueFromFrame p sym ext root f
_actContext ActiveTree p sym ext root f args
s
, _actResult :: PartialResultFrame sym ext f args
_actResult = PartialResultFrame sym ext f args
v
}
{-# INLINE actResult #-}
actFrame ::
Lens (ActiveTree p sym ext root f args)
(ActiveTree p sym ext root f args')
(TopFrame sym ext f args)
(TopFrame sym ext f args')
actFrame :: forall p sym ext root f (args :: Maybe (Ctx CrucibleType))
(args' :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
actFrame = (PartialResult sym ext (SimFrame sym ext f args)
-> f (PartialResult sym ext (SimFrame sym ext f args')))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
forall p sym ext root f (args0 :: Maybe (Ctx CrucibleType))
(args1 :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(PartialResult sym ext (SimFrame sym ext f args0)
-> f (PartialResult sym ext (SimFrame sym ext f args1)))
-> ActiveTree p sym ext root f args0
-> f (ActiveTree p sym ext root f args1)
actResult ((PartialResult sym ext (SimFrame sym ext f args)
-> f (PartialResult sym ext (SimFrame sym ext f args')))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args'))
-> ((TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> PartialResult sym ext (SimFrame sym ext f args)
-> f (PartialResult sym ext (SimFrame sym ext f args')))
-> (TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> PartialResult sym ext (SimFrame sym ext f args)
-> f (PartialResult sym ext (SimFrame sym ext f args'))
forall sym ext u v (f :: Type -> Type).
Functor f =>
(GlobalPair sym u -> f (GlobalPair sym v))
-> PartialResult sym ext u -> f (PartialResult sym ext v)
partialValue
{-# INLINE actFrame #-}
activeFrames :: ActiveTree ctx sym ext root a args ->
[SomeFrame (SimFrame sym ext)]
activeFrames :: forall ctx sym ext root a (args :: Maybe (Ctx CrucibleType)).
ActiveTree ctx sym ext root a args
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
activeFrames (ActiveTree ValueFromFrame ctx sym ext root a
ctx PartialResultFrame sym ext a args
ar) =
SimFrame sym ext a args
-> SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
forall fk argk (f :: fk -> argk -> Type) (l :: fk) (a :: argk).
f l a -> SomeFrame @fk @argk f
SomeFrame (PartialResultFrame sym ext a args
arPartialResultFrame sym ext a args
-> Getting
(GlobalPair sym (SimFrame sym ext a args))
(PartialResultFrame sym ext a args)
(GlobalPair sym (SimFrame sym ext a args))
-> GlobalPair sym (SimFrame sym ext a args)
forall s a. s -> Getting a s a -> a
^.Getting
(GlobalPair sym (SimFrame sym ext a args))
(PartialResultFrame sym ext a args)
(GlobalPair sym (SimFrame sym ext a args))
forall sym ext u v (f :: Type -> Type).
Functor f =>
(GlobalPair sym u -> f (GlobalPair sym v))
-> PartialResult sym ext u -> f (PartialResult sym ext v)
partialValueGlobalPair sym (SimFrame sym ext a args)
-> Getting
(SimFrame sym ext a args)
(GlobalPair sym (SimFrame sym ext a args))
(SimFrame sym ext a args)
-> SimFrame sym ext a args
forall s a. s -> Getting a s a -> a
^.Getting
(SimFrame sym ext a args)
(GlobalPair sym (SimFrame sym ext a args))
(SimFrame sym ext a args)
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue) SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall a. a -> [a] -> [a]
: ValueFromFrame ctx sym ext root a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall p sym ext r a.
ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
parentFrames ValueFromFrame ctx sym ext root a
ctx
data Override p sym ext (args :: Ctx CrucibleType) ret
= Override { forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Override p sym ext args ret -> FunctionName
overrideName :: FunctionName
, forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Override p sym ext args ret
-> forall r.
ExecCont
p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
overrideHandler :: forall r. ExecCont p sym ext r (OverrideLang ret) ('Just args)
}
data FnState p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType)
= UseOverride !(Override p sym ext args ret)
| forall blocks . UseCFG !(CFG ext blocks args ret) !(CFGPostdom blocks)
newtype FunctionBindings p sym ext = FnBindings { forall p sym ext.
FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
fnBindings :: FnHandleMap (FnState p sym ext) }
type EvalStmtFunc p sym ext =
forall rtp blocks r ctx tp'.
StmtExtension ext (RegEntry sym) tp' ->
CrucibleState p sym ext rtp blocks r ctx ->
IO (RegValue sym tp', CrucibleState p sym ext rtp blocks r ctx)
data ExtensionImpl p sym ext
= ExtensionImpl
{ forall p sym ext.
ExtensionImpl p sym ext
-> forall bak rtp (blocks :: Ctx (Ctx CrucibleType))
(r :: CrucibleType) (ctx :: Ctx CrucibleType).
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> (Int -> String -> IO ())
-> CrucibleState p sym ext rtp blocks r ctx
-> EvalAppFunc sym (ExprExtension ext)
extensionEval ::
forall bak rtp blocks r ctx.
IsSymBackend sym bak =>
bak ->
IntrinsicTypes sym ->
(Int -> String -> IO ()) ->
CrucibleState p sym ext rtp blocks r ctx ->
EvalAppFunc sym (ExprExtension ext)
, forall p sym ext. ExtensionImpl p sym ext -> EvalStmtFunc p sym ext
extensionExec :: EvalStmtFunc p sym ext
}
emptyExtensionImpl :: ExtensionImpl p sym ()
emptyExtensionImpl :: forall p sym. ExtensionImpl p sym ()
emptyExtensionImpl =
ExtensionImpl
{ extensionEval :: forall bak rtp (blocks :: Ctx (Ctx CrucibleType))
(r :: CrucibleType) (ctx :: Ctx CrucibleType).
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> (Int -> String -> IO ())
-> CrucibleState p sym () rtp blocks r ctx
-> EvalAppFunc sym (ExprExtension ())
extensionEval = \bak
_sym IntrinsicTypes sym
_iTypes Int -> String -> IO ()
_log CrucibleState p sym () rtp blocks r ctx
_f forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
_state -> ExprExtension () f tp -> IO (RegValue sym tp)
\case
, extensionExec :: EvalStmtFunc p sym ()
extensionExec = StmtExtension () (RegEntry sym) tp'
-> CrucibleState p sym () rtp blocks r ctx
-> IO (RegValue sym tp', CrucibleState p sym () rtp blocks r ctx)
EvalStmtFunc p sym ()
\case
}
type IsSymInterfaceProof sym a = (IsSymInterface sym => a) -> a
newtype Metric p sym ext =
Metric {
forall p sym ext.
Metric p sym ext
-> forall rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> IO Integer
runMetric :: forall rtp f args. SimState p sym ext rtp f args -> IO Integer
}
data SimContext (personality :: Type) (sym :: Type) (ext :: Type)
= SimContext { forall personality sym ext.
SimContext personality sym ext -> SomeBackend sym
_ctxBackend :: !(SomeBackend sym)
, forall personality sym ext.
SimContext personality sym ext
-> forall a. IsSymInterfaceProof sym a
ctxSolverProof :: !(forall a . IsSymInterfaceProof sym a)
, forall personality sym ext.
SimContext personality sym ext -> IntrinsicTypes sym
ctxIntrinsicTypes :: !(IntrinsicTypes sym)
, forall personality sym ext.
SimContext personality sym ext -> HandleAllocator
simHandleAllocator :: !(HandleAllocator)
, forall personality sym ext.
SimContext personality sym ext -> Handle
printHandle :: !Handle
, forall personality sym ext.
SimContext personality sym ext -> ExtensionImpl personality sym ext
extensionImpl :: ExtensionImpl personality sym ext
, forall personality sym ext.
SimContext personality sym ext
-> FunctionBindings personality sym ext
_functionBindings :: !(FunctionBindings personality sym ext)
, forall personality sym ext.
SimContext personality sym ext -> personality
_cruciblePersonality :: !personality
, forall personality sym ext.
SimContext personality sym ext
-> Map Text (Metric personality sym ext)
_profilingMetrics :: !(Map Text (Metric personality sym ext))
}
initSimContext ::
IsSymBackend sym bak =>
bak ->
IntrinsicTypes sym ->
HandleAllocator ->
Handle ->
FunctionBindings personality sym ext ->
ExtensionImpl personality sym ext ->
personality ->
SimContext personality sym ext
initSimContext :: forall sym bak personality ext.
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> HandleAllocator
-> Handle
-> FunctionBindings personality sym ext
-> ExtensionImpl personality sym ext
-> personality
-> SimContext personality sym ext
initSimContext bak
bak IntrinsicTypes sym
muxFns HandleAllocator
halloc Handle
h FunctionBindings personality sym ext
bindings ExtensionImpl personality sym ext
extImpl personality
personality =
SimContext { _ctxBackend :: SomeBackend sym
_ctxBackend = bak -> SomeBackend sym
forall sym bak. IsSymBackend sym bak => bak -> SomeBackend sym
SomeBackend bak
bak
, ctxSolverProof :: forall a. IsSymInterfaceProof sym a
ctxSolverProof = \IsSymInterface sym => a
a -> a
IsSymInterface sym => a
a
, ctxIntrinsicTypes :: IntrinsicTypes sym
ctxIntrinsicTypes = IntrinsicTypes sym
muxFns
, simHandleAllocator :: HandleAllocator
simHandleAllocator = HandleAllocator
halloc
, printHandle :: Handle
printHandle = Handle
h
, extensionImpl :: ExtensionImpl personality sym ext
extensionImpl = ExtensionImpl personality sym ext
extImpl
, _functionBindings :: FunctionBindings personality sym ext
_functionBindings = FunctionBindings personality sym ext
bindings
, _cruciblePersonality :: personality
_cruciblePersonality = personality
personality
, _profilingMetrics :: Map Text (Metric personality sym ext)
_profilingMetrics = Map Text (Metric personality sym ext)
forall k a. Map k a
Map.empty
}
withBackend ::
SimContext personality sym ext ->
(forall bak. IsSymBackend sym bak => bak -> a) ->
a
withBackend :: forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimContext personality sym ext
ctx forall bak. IsSymBackend sym bak => bak -> a
f = case SimContext personality sym ext -> SomeBackend sym
forall personality sym ext.
SimContext personality sym ext -> SomeBackend sym
_ctxBackend SimContext personality sym ext
ctx of SomeBackend bak
bak -> bak -> a
forall bak. IsSymBackend sym bak => bak -> a
f bak
bak
ctxSymInterface :: Getter (SimContext p sym ext) sym
ctxSymInterface :: forall p sym ext (f :: Type -> Type).
(Contravariant f, Functor f) =>
(sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
ctxSymInterface = (SimContext p sym ext -> sym)
-> (sym -> f sym)
-> SimContext p sym ext
-> f (SimContext p sym ext)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' @Type @Type p f s a
to (\SimContext p sym ext
ctx ->
case SimContext p sym ext -> SomeBackend sym
forall personality sym ext.
SimContext personality sym ext -> SomeBackend sym
_ctxBackend SimContext p sym ext
ctx of
SomeBackend bak
bak -> bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak)
functionBindings :: Lens' (SimContext p sym ext) (FunctionBindings p sym ext)
functionBindings :: forall p sym ext (f :: Type -> Type).
Functor f =>
(FunctionBindings p sym ext -> f (FunctionBindings p sym ext))
-> SimContext p sym ext -> f (SimContext p sym ext)
functionBindings = (SimContext p sym ext -> FunctionBindings p sym ext)
-> (SimContext p sym ext
-> FunctionBindings p sym ext -> SimContext p sym ext)
-> Lens
(SimContext p sym ext)
(SimContext p sym ext)
(FunctionBindings p sym ext)
(FunctionBindings p sym ext)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens SimContext p sym ext -> FunctionBindings p sym ext
forall personality sym ext.
SimContext personality sym ext
-> FunctionBindings personality sym ext
_functionBindings (\SimContext p sym ext
s FunctionBindings p sym ext
v -> SimContext p sym ext
s { _functionBindings = v })
cruciblePersonality :: Lens' (SimContext p sym ext) p
cruciblePersonality :: forall p sym ext (f :: Type -> Type).
Functor f =>
(p -> f p) -> SimContext p sym ext -> f (SimContext p sym ext)
cruciblePersonality = (SimContext p sym ext -> p)
-> (SimContext p sym ext -> p -> SimContext p sym ext)
-> Lens (SimContext p sym ext) (SimContext p sym ext) p p
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens SimContext p sym ext -> p
forall personality sym ext.
SimContext personality sym ext -> personality
_cruciblePersonality (\SimContext p sym ext
s p
v -> SimContext p sym ext
s{ _cruciblePersonality = v })
profilingMetrics :: Lens' (SimContext p sym ext) (Map Text (Metric p sym ext))
profilingMetrics :: forall p sym ext (f :: Type -> Type).
Functor f =>
(Map Text (Metric p sym ext) -> f (Map Text (Metric p sym ext)))
-> SimContext p sym ext -> f (SimContext p sym ext)
profilingMetrics = (SimContext p sym ext -> Map Text (Metric p sym ext))
-> (SimContext p sym ext
-> Map Text (Metric p sym ext) -> SimContext p sym ext)
-> Lens
(SimContext p sym ext)
(SimContext p sym ext)
(Map Text (Metric p sym ext))
(Map Text (Metric p sym ext))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens SimContext p sym ext -> Map Text (Metric p sym ext)
forall personality sym ext.
SimContext personality sym ext
-> Map Text (Metric personality sym ext)
_profilingMetrics (\SimContext p sym ext
s Map Text (Metric p sym ext)
v -> SimContext p sym ext
s { _profilingMetrics = v })
newtype AbortHandler p sym ext rtp
= AH { forall p sym ext rtp.
AbortHandler p sym ext rtp
-> forall l (args :: Maybe (Ctx CrucibleType)).
AbortExecReason -> ExecCont p sym ext rtp l args
runAH :: forall (l :: Type) args.
AbortExecReason ->
ExecCont p sym ext rtp l args
}
data SimState p sym ext rtp f (args :: Maybe (Ctx.Ctx CrucibleType))
= SimState { forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SimContext p sym ext
_stateContext :: !(SimContext p sym ext)
, forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> AbortHandler p sym ext rtp
_abortHandler :: !(AbortHandler p sym ext rtp)
, forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> ActiveTree p sym ext rtp f args
_stateTree :: !(ActiveTree p sym ext rtp f args)
}
data SomeSimState p sym ext rtp =
forall f args. SomeSimState !(SimState p sym ext rtp f args)
type CrucibleState p sym ext rtp blocks ret args
= SimState p sym ext rtp (CrucibleLang blocks ret) ('Just args)
initSimState ::
SimContext p sym ext ->
SymGlobalState sym ->
AbortHandler p sym ext (RegEntry sym ret) ->
TypeRepr ret ->
IO (SimState p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx))
initSimState :: forall p sym ext (ret :: CrucibleType).
SimContext p sym ext
-> SymGlobalState sym
-> AbortHandler p sym ext (RegEntry sym ret)
-> TypeRepr ret
-> IO
(SimState
p
sym
ext
(RegEntry sym ret)
(OverrideLang ret)
('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType)))
initSimState SimContext p sym ext
ctx SymGlobalState sym
globals AbortHandler p sym ext (RegEntry sym ret)
ah TypeRepr ret
ret =
do let halloc :: HandleAllocator
halloc = SimContext p sym ext -> HandleAllocator
forall personality sym ext.
SimContext personality sym ext -> HandleAllocator
simHandleAllocator SimContext p sym ext
ctx
FnHandle (EmptyCtx @CrucibleType) ret
h <- HandleAllocator
-> FunctionName
-> Assignment @CrucibleType TypeRepr (EmptyCtx @CrucibleType)
-> TypeRepr ret
-> IO (FnHandle (EmptyCtx @CrucibleType) ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
HandleAllocator
-> FunctionName
-> Assignment @CrucibleType TypeRepr args
-> TypeRepr ret
-> IO (FnHandle args ret)
mkHandle' HandleAllocator
halloc FunctionName
startFunctionName Assignment @CrucibleType TypeRepr (EmptyCtx @CrucibleType)
forall {k} (ctx :: Ctx k) (f :: k -> Type).
((ctx :: Ctx k) ~ (EmptyCtx @k :: Ctx k)) =>
Assignment @k f ctx
Ctx.Empty TypeRepr ret
ret
let startFrame :: OverrideFrame sym ret (EmptyCtx @CrucibleType)
startFrame = OverrideFrame { _override :: FunctionName
_override = FunctionName
startFunctionName
, _overrideHandle :: SomeHandle
_overrideHandle = FnHandle (EmptyCtx @CrucibleType) ret -> SomeHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeHandle
SomeHandle FnHandle (EmptyCtx @CrucibleType) ret
h
, _overrideRegMap :: RegMap sym (EmptyCtx @CrucibleType)
_overrideRegMap = RegMap sym (EmptyCtx @CrucibleType)
forall sym. RegMap sym (EmptyCtx @CrucibleType)
emptyRegMap
}
let startGP :: GlobalPair
sym
(SimFrame
sym
ext
(OverrideLang ret)
('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType)))
startGP = SimFrame
sym
ext
(OverrideLang ret)
('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
-> SymGlobalState sym
-> GlobalPair
sym
(SimFrame
sym
ext
(OverrideLang ret)
('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType)))
forall sym v. v -> SymGlobalState sym -> GlobalPair sym v
GlobalPair (OverrideFrame sym ret (EmptyCtx @CrucibleType)
-> SimFrame
sym
ext
(OverrideLang ret)
('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
forall sym (ret :: CrucibleType) (args1 :: Ctx CrucibleType) ext.
OverrideFrame sym ret args1
-> SimFrame
sym ext (OverrideLang ret) ('Just @(Ctx CrucibleType) args1)
OF OverrideFrame sym ret (EmptyCtx @CrucibleType)
startFrame) SymGlobalState sym
globals
SimState
p
sym
ext
(RegEntry sym ret)
(OverrideLang ret)
('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
-> IO
(SimState
p
sym
ext
(RegEntry sym ret)
(OverrideLang ret)
('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType)))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return
SimState
{ _stateContext :: SimContext p sym ext
_stateContext = SimContext p sym ext
ctx
, _abortHandler :: AbortHandler p sym ext (RegEntry sym ret)
_abortHandler = AbortHandler p sym ext (RegEntry sym ret)
ah
, _stateTree :: ActiveTree
p
sym
ext
(RegEntry sym ret)
(OverrideLang ret)
('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
_stateTree = GlobalPair
sym
(SimFrame
sym
ext
(OverrideLang ret)
('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType)))
-> ActiveTree
p
sym
ext
(RegEntry sym (FrameRetType (OverrideLang ret)))
(OverrideLang ret)
('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
forall sym ext f (args :: Maybe (Ctx CrucibleType)) p.
TopFrame sym ext f args
-> ActiveTree p sym ext (RegEntry sym (FrameRetType f)) f args
singletonTree GlobalPair
sym
(SimFrame
sym
ext
(OverrideLang ret)
('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType)))
startGP
}
stateLocation :: Getter (SimState p sym ext r f a) (Maybe ProgramLoc)
stateLocation :: forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
(Contravariant f, Functor f) =>
(Maybe ProgramLoc -> f (Maybe ProgramLoc))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateLocation = (SimState p sym ext r f a -> Maybe ProgramLoc)
-> (Maybe ProgramLoc -> f (Maybe ProgramLoc))
-> SimState p sym ext r f a
-> f (SimState p sym ext r f a)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' @Type @Type p f s a
to SimState p sym ext r f a -> Maybe ProgramLoc
forall p sym ext r f (a :: Maybe (Ctx CrucibleType)).
SimState p sym ext r f a -> Maybe ProgramLoc
f
where
f :: SimState p sym ext r f a -> Maybe ProgramLoc
f :: forall p sym ext r f (a :: Maybe (Ctx CrucibleType)).
SimState p sym ext r f a -> Maybe ProgramLoc
f SimState p sym ext r f a
st = case SimState p sym ext r f a
stSimState p sym ext r f a
-> Getting
(SimFrame sym ext f a)
(SimState p sym ext r f a)
(SimFrame sym ext f a)
-> SimFrame sym ext f a
forall s a. s -> Getting a s a -> a
^.(ActiveTree p sym ext r f a
-> Const @Type (SimFrame sym ext f a) (ActiveTree p sym ext r f a))
-> SimState p sym ext r f a
-> Const @Type (SimFrame sym ext f a) (SimState p sym ext r f a)
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)) g
(b :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(ActiveTree p sym ext rtp f a -> f (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f a -> f (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext r f a
-> Const @Type (SimFrame sym ext f a) (ActiveTree p sym ext r f a))
-> SimState p sym ext r f a
-> Const @Type (SimFrame sym ext f a) (SimState p sym ext r f a))
-> ((SimFrame sym ext f a
-> Const @Type (SimFrame sym ext f a) (SimFrame sym ext f a))
-> ActiveTree p sym ext r f a
-> Const @Type (SimFrame sym ext f a) (ActiveTree p sym ext r f a))
-> Getting
(SimFrame sym ext f a)
(SimState p sym ext r f a)
(SimFrame sym ext f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext f a
-> Const @Type (SimFrame sym ext f a) (TopFrame sym ext f a))
-> ActiveTree p sym ext r f a
-> Const @Type (SimFrame sym ext f a) (ActiveTree p sym ext r f a)
forall p sym ext root f (args :: Maybe (Ctx CrucibleType))
(args' :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
actFrame ((TopFrame sym ext f a
-> Const @Type (SimFrame sym ext f a) (TopFrame sym ext f a))
-> ActiveTree p sym ext r f a
-> Const @Type (SimFrame sym ext f a) (ActiveTree p sym ext r f a))
-> ((SimFrame sym ext f a
-> Const @Type (SimFrame sym ext f a) (SimFrame sym ext f a))
-> TopFrame sym ext f a
-> Const @Type (SimFrame sym ext f a) (TopFrame sym ext f a))
-> (SimFrame sym ext f a
-> Const @Type (SimFrame sym ext f a) (SimFrame sym ext f a))
-> ActiveTree p sym ext r f a
-> Const @Type (SimFrame sym ext f a) (ActiveTree p sym ext r f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimFrame sym ext f a
-> Const @Type (SimFrame sym ext f a) (SimFrame sym ext f a))
-> TopFrame sym ext f a
-> Const @Type (SimFrame sym ext f a) (TopFrame sym ext f a)
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue of
MF CallFrame sym ext blocks ret args1
cf -> ProgramLoc -> Maybe ProgramLoc
forall a. a -> Maybe a
Just (ProgramLoc -> Maybe ProgramLoc) -> ProgramLoc -> Maybe ProgramLoc
forall a b. (a -> b) -> a -> b
$! (CallFrame sym ext blocks ret args1 -> ProgramLoc
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> ProgramLoc
frameProgramLoc CallFrame sym ext blocks ret args1
cf)
OF OverrideFrame sym ret args1
_ -> Maybe ProgramLoc
forall a. Maybe a
Nothing
RF FunctionName
_ RegEntry sym (FrameRetType f)
_ -> Maybe ProgramLoc
forall a. Maybe a
Nothing
stateContext :: Simple Lens (SimState p sym ext r f a) (SimContext p sym ext)
stateContext :: forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext = (SimState p sym ext r f a -> SimContext p sym ext)
-> (SimState p sym ext r f a
-> SimContext p sym ext -> SimState p sym ext r f a)
-> Lens
(SimState p sym ext r f a)
(SimState p sym ext r f a)
(SimContext p sym ext)
(SimContext p sym ext)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens SimState p sym ext r f a -> SimContext p sym ext
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SimContext p sym ext
_stateContext (\SimState p sym ext r f a
s SimContext p sym ext
v -> SimState p sym ext r f a
s { _stateContext = v })
{-# INLINE stateContext #-}
abortHandler :: Simple Lens (SimState p sym ext r f a) (AbortHandler p sym ext r)
abortHandler :: forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(AbortHandler p sym ext r -> f (AbortHandler p sym ext r))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
abortHandler = (SimState p sym ext r f a -> AbortHandler p sym ext r)
-> (SimState p sym ext r f a
-> AbortHandler p sym ext r -> SimState p sym ext r f a)
-> Lens
(SimState p sym ext r f a)
(SimState p sym ext r f a)
(AbortHandler p sym ext r)
(AbortHandler p sym ext r)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens SimState p sym ext r f a -> AbortHandler p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> AbortHandler p sym ext rtp
_abortHandler (\SimState p sym ext r f a
s AbortHandler p sym ext r
v -> SimState p sym ext r f a
s { _abortHandler = v })
stateTree ::
Lens (SimState p sym ext rtp f a)
(SimState p sym ext rtp g b)
(ActiveTree p sym ext rtp f a)
(ActiveTree p sym ext rtp g b)
stateTree :: forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)) g
(b :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(ActiveTree p sym ext rtp f a -> f (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f a -> f (SimState p sym ext rtp g b)
stateTree = (SimState p sym ext rtp f a -> ActiveTree p sym ext rtp f a)
-> (SimState p sym ext rtp f a
-> ActiveTree p sym ext rtp g b -> SimState p sym ext rtp g b)
-> Lens
(SimState p sym ext rtp f a)
(SimState p sym ext rtp g b)
(ActiveTree p sym ext rtp f a)
(ActiveTree p sym ext rtp g b)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens SimState p sym ext rtp f a -> ActiveTree p sym ext rtp f a
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> ActiveTree p sym ext rtp f args
_stateTree (\SimState p sym ext rtp f a
s ActiveTree p sym ext rtp g b
v -> SimState p sym ext rtp f a
s { _stateTree = v })
{-# INLINE stateTree #-}
stateCrucibleFrame ::
Lens (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a))
(SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
(CallFrame sym ext blocks r a)
(CallFrame sym ext blocks r a')
stateCrucibleFrame :: forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
(r :: CrucibleType) (a :: Ctx CrucibleType)
(a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState
p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (SimState
p
sym
ext
rtp
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) a'))
stateCrucibleFrame = (ActiveTree
p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
p
sym
ext
rtp
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) a')))
-> SimState
p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (SimState
p
sym
ext
rtp
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) a'))
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)) g
(b :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(ActiveTree p sym ext rtp f a -> f (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f a -> f (SimState p sym ext rtp g b)
stateTree ((ActiveTree
p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
p
sym
ext
rtp
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) a')))
-> SimState
p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (SimState
p
sym
ext
rtp
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) a')))
-> ((CallFrame sym ext blocks r a
-> f (CallFrame sym ext blocks r a'))
-> ActiveTree
p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
p
sym
ext
rtp
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) a')))
-> (CallFrame sym ext blocks r a
-> f (CallFrame sym ext blocks r a'))
-> SimState
p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (SimState
p
sym
ext
rtp
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) a'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (TopFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a')))
-> ActiveTree
p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
p
sym
ext
rtp
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) a'))
forall p sym ext root f (args :: Maybe (Ctx CrucibleType))
(args' :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
actFrame ((TopFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (TopFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a')))
-> ActiveTree
p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
p
sym
ext
rtp
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) a')))
-> ((CallFrame sym ext blocks r a
-> f (CallFrame sym ext blocks r a'))
-> TopFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (TopFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a')))
-> (CallFrame sym ext blocks r a
-> f (CallFrame sym ext blocks r a'))
-> ActiveTree
p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
p
sym
ext
rtp
(CrucibleLang blocks r)
('Just @(Ctx CrucibleType) a'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> TopFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (TopFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a'))
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(r :: CrucibleType) (args :: Ctx CrucibleType)
(args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r args
-> f (CallFrame sym ext blocks r args'))
-> TopFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
-> f (TopFrame
sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args'))
crucibleTopFrame
{-# INLINE stateCrucibleFrame #-}
stateOverrideFrame ::
Lens
(SimState p sym ext q (OverrideLang r) ('Just a))
(SimState p sym ext q (OverrideLang r) ('Just a'))
(OverrideFrame sym r a)
(OverrideFrame sym r a')
stateOverrideFrame :: forall p sym ext q (r :: CrucibleType) (a :: Ctx CrucibleType)
(a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> SimState
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (SimState
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
stateOverrideFrame = (ActiveTree
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> SimState
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (SimState
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)) g
(b :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(ActiveTree p sym ext rtp f a -> f (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f a -> f (SimState p sym ext rtp g b)
stateTree ((ActiveTree
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> SimState
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (SimState
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> ((OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> ActiveTree
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> (OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> SimState
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (SimState
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (TopFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> ActiveTree
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall p sym ext root f (args :: Maybe (Ctx CrucibleType))
(args' :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
actFrame ((TopFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (TopFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> ActiveTree
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> ((OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> TopFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (TopFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> (OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> ActiveTree
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (SimFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> TopFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (TopFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue ((SimFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (SimFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> TopFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (TopFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> ((OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> SimFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (SimFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> (OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> TopFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (TopFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> SimFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (SimFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType)
(r' :: CrucibleType) (args' :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> SimFrame
sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args'))
overrideSimFrame
stateGlobals :: Simple Lens (SimState p sym ext q f args) (SymGlobalState sym)
stateGlobals :: forall p sym ext q f (args :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> SimState p sym ext q f args -> f (SimState p sym ext q f args)
stateGlobals = (ActiveTree p sym ext q f args
-> f (ActiveTree p sym ext q f args))
-> SimState p sym ext q f args -> f (SimState p sym ext q f args)
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)) g
(b :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(ActiveTree p sym ext rtp f a -> f (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f a -> f (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext q f args
-> f (ActiveTree p sym ext q f args))
-> SimState p sym ext q f args -> f (SimState p sym ext q f args))
-> ((SymGlobalState sym -> f (SymGlobalState sym))
-> ActiveTree p sym ext q f args
-> f (ActiveTree p sym ext q f args))
-> (SymGlobalState sym -> f (SymGlobalState sym))
-> SimState p sym ext q f args
-> f (SimState p sym ext q f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext f args -> f (TopFrame sym ext f args))
-> ActiveTree p sym ext q f args
-> f (ActiveTree p sym ext q f args)
forall p sym ext root f (args :: Maybe (Ctx CrucibleType))
(args' :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
actFrame ((TopFrame sym ext f args -> f (TopFrame sym ext f args))
-> ActiveTree p sym ext q f args
-> f (ActiveTree p sym ext q f args))
-> ((SymGlobalState sym -> f (SymGlobalState sym))
-> TopFrame sym ext f args -> f (TopFrame sym ext f args))
-> (SymGlobalState sym -> f (SymGlobalState sym))
-> ActiveTree p sym ext q f args
-> f (ActiveTree p sym ext q f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym -> f (SymGlobalState sym))
-> TopFrame sym ext f args -> f (TopFrame sym ext f args)
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals
stateSymInterface :: Getter (SimState p sym ext r f a) sym
stateSymInterface :: forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
(Contravariant f, Functor f) =>
(sym -> f sym)
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateSymInterface = (SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext ((SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a))
-> ((sym -> f sym)
-> SimContext p sym ext -> f (SimContext p sym ext))
-> (sym -> f sym)
-> SimState p sym ext r f a
-> f (SimState p sym ext r f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
forall p sym ext (f :: Type -> Type).
(Contravariant f, Functor f) =>
(sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
ctxSymInterface
stateIntrinsicTypes :: Getter (SimState p sym ext r f args) (IntrinsicTypes sym)
stateIntrinsicTypes :: forall p sym ext r f (args :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
(Contravariant f, Functor f) =>
(IntrinsicTypes sym -> f (IntrinsicTypes sym))
-> SimState p sym ext r f args -> f (SimState p sym ext r f args)
stateIntrinsicTypes = (SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f args -> f (SimState p sym ext r f args)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext ((SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f args -> f (SimState p sym ext r f args))
-> ((IntrinsicTypes sym -> f (IntrinsicTypes sym))
-> SimContext p sym ext -> f (SimContext p sym ext))
-> (IntrinsicTypes sym -> f (IntrinsicTypes sym))
-> SimState p sym ext r f args
-> f (SimState p sym ext r f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimContext p sym ext -> IntrinsicTypes sym)
-> (IntrinsicTypes sym -> f (IntrinsicTypes sym))
-> SimContext p sym ext
-> f (SimContext p sym ext)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' @Type @Type p f s a
to SimContext p sym ext -> IntrinsicTypes sym
forall personality sym ext.
SimContext personality sym ext -> IntrinsicTypes sym
ctxIntrinsicTypes
stateConfiguration :: Getter (SimState p sym ext r f args) Config
stateConfiguration :: forall p sym ext r f (args :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
(Contravariant f, Functor f) =>
(Config -> f Config)
-> SimState p sym ext r f args -> f (SimState p sym ext r f args)
stateConfiguration = (SimState p sym ext r f args -> Config)
-> (Config -> f Config)
-> SimState p sym ext r f args
-> f (SimState p sym ext r f args)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' @Type @Type p f s a
to (\SimState p sym ext r f args
s -> SimState p sym ext r f args -> forall a. IsSymInterfaceProof sym a
forall p sym ext r f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext r f args -> forall a. IsSymInterfaceProof sym a
stateSolverProof SimState p sym ext r f args
s (sym -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration (SimState p sym ext r f args
sSimState p sym ext r f args
-> Getting sym (SimState p sym ext r f args) sym -> sym
forall s a. s -> Getting a s a -> a
^.Getting sym (SimState p sym ext r f args) sym
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
(Contravariant f, Functor f) =>
(sym -> f sym)
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateSymInterface)))
stateSolverProof :: SimState p sym ext r f args -> (forall a . IsSymInterfaceProof sym a)
stateSolverProof :: forall p sym ext r f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext r f args -> forall a. IsSymInterfaceProof sym a
stateSolverProof SimState p sym ext r f args
s = SimContext p sym ext -> forall a. IsSymInterfaceProof sym a
forall personality sym ext.
SimContext personality sym ext
-> forall a. IsSymInterfaceProof sym a
ctxSolverProof (SimState p sym ext r f args
sSimState p sym ext r f args
-> Getting
(SimContext p sym ext)
(SimState p sym ext r f args)
(SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
(SimContext p sym ext)
(SimState p sym ext r f args)
(SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext)