Copyright	(c) Galois Inc 2014
License	BSD3
Maintainer	Joe Hendrix <jhendrix@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

Lang.Crucible.Simulator.CallFrame

Contents

CrucibleBranchTarget
Call frame
SomeHandle
Simulator frames

Description

Call frames are used to record information about suspended stack frames when functions are called.

Synopsis

data CrucibleBranchTarget f (args :: Maybe (Ctx CrucibleType)) where
- BlockTarget :: forall (blocks :: Ctx (Ctx CrucibleType)) (args1 :: Ctx CrucibleType) (r :: CrucibleType). !(BlockID blocks args1) -> CrucibleBranchTarget (CrucibleLang blocks r) ('Just args1)
- ReturnTarget :: forall f. CrucibleBranchTarget f ('Nothing :: Maybe (Ctx CrucibleType))
ppBranchTarget :: forall f (args :: Maybe (Ctx CrucibleType)). CrucibleBranchTarget f args -> String
data CallFrame sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (args :: Ctx CrucibleType) = CallFrame {
- _frameCFG :: CFG ext blocks initialArgs ret
- _framePostdomMap :: !(CFGPostdom blocks)
- _frameBlockID :: !(Some (BlockID blocks))
- _frameRegs :: !(RegMap sym args)
- _frameStmts :: !(StmtSeq ext blocks ret args)
- _framePostdom :: !(Some (CrucibleBranchTarget (CrucibleLang blocks ret)))
}
mkCallFrame :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType) sym. CFG ext blocks init ret -> CFGPostdom blocks -> RegMap sym init -> CallFrame sym ext blocks ret init
mkBlockFrame :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType) (args :: Ctx CrucibleType) sym. CFG ext blocks init ret -> BlockID blocks args -> CFGPostdom blocks -> RegMap sym args -> CallFrame sym ext blocks ret args
framePostdomMap :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) f. Functor f => (CFGPostdom blocks -> f (CFGPostdom blocks)) -> CallFrame sym ext blocks ret ctx -> f (CallFrame sym ext blocks ret ctx)
frameBlockMap :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). CallFrame sym ext blocks ret ctx -> BlockMap ext blocks ret
frameHandle :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). CallFrame sym ext blocks ret ctx -> SomeHandle
frameReturnType :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). CallFrame sym ext blocks ret ctx -> TypeRepr ret
frameBlockID :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) f. Functor f => (Some (BlockID blocks) -> f (Some (BlockID blocks))) -> CallFrame sym ext blocks ret ctx -> f (CallFrame sym ext blocks ret ctx)
frameRegs :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (args :: Ctx CrucibleType) f. Functor f => (RegMap sym args -> f (RegMap sym args)) -> CallFrame sym ext blocks ret args -> f (CallFrame sym ext blocks ret args)
frameStmts :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) f. Functor f => (StmtSeq ext blocks ret ctx -> f (StmtSeq ext blocks ret ctx)) -> CallFrame sym ext blocks ret ctx -> f (CallFrame sym ext blocks ret ctx)
framePostdom :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) f. Functor f => (Some (CrucibleBranchTarget (CrucibleLang blocks ret)) -> f (Some (CrucibleBranchTarget (CrucibleLang blocks ret)))) -> CallFrame sym ext blocks ret ctx -> f (CallFrame sym ext blocks ret ctx)
frameProgramLoc :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). CallFrame sym ext blocks ret ctx -> ProgramLoc
setFrameBlock :: forall (blocks :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType) sym ext (ret :: CrucibleType) (ctx :: Ctx CrucibleType). BlockID blocks args -> RegMap sym args -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret args
setFrameBreakpointPostdomInfo :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). [BreakpointName] -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret ctx
extendFrame :: forall (tp :: CrucibleType) sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). TypeRepr tp -> RegValue sym tp -> StmtSeq ext blocks ret (ctx ::> tp) -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret (ctx ::> tp)
updateFrame :: forall sym (ctx' :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) ext (ret :: CrucibleType). RegMap sym ctx' -> BlockID blocks ctx -> StmtSeq ext blocks ret ctx' -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret ctx'
mergeCallFrame :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (args :: Ctx CrucibleType). IsSymInterface sym => sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (CallFrame sym ext blocks ret args)
data SomeHandle where
- SomeHandle :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType). !(FnHandle args ret) -> SomeHandle
data SimFrame sym ext f (args :: Maybe (Ctx CrucibleType)) where
- OF :: forall sym (ret :: CrucibleType) (args1 :: Ctx CrucibleType) ext. !(OverrideFrame sym ret args1) -> SimFrame sym ext (OverrideLang ret) ('Just args1)
- MF :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (args1 :: Ctx CrucibleType). !(CallFrame sym ext blocks ret args1) -> SimFrame sym ext (CrucibleLang blocks ret) ('Just args1)
- RF :: forall sym f ext. !FunctionName -> !(RegEntry sym (FrameRetType f)) -> SimFrame sym ext f ('Nothing :: Maybe (Ctx CrucibleType))
data CrucibleLang (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
data OverrideLang (ret :: CrucibleType)
type family FrameRetType f :: CrucibleType where ...
data OverrideFrame sym (ret :: CrucibleType) (args :: Ctx CrucibleType) = OverrideFrame {
- _override :: !FunctionName
- _overrideHandle :: !SomeHandle
- _overrideRegMap :: !(RegMap sym args)
}
override :: forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType) f. Functor f => (FunctionName -> f FunctionName) -> OverrideFrame sym ret args -> f (OverrideFrame sym ret args)
overrideHandle :: forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType) f. Functor f => (SomeHandle -> f SomeHandle) -> OverrideFrame sym ret args -> f (OverrideFrame sym ret args)
overrideRegMap :: forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType) (args' :: Ctx CrucibleType) f. Functor f => (RegMap sym args -> f (RegMap sym args')) -> OverrideFrame sym ret args -> f (OverrideFrame sym ret args')
overrideSimFrame :: forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType) (r' :: CrucibleType) (args' :: Ctx CrucibleType) f. Functor f => (OverrideFrame sym r args -> f (OverrideFrame sym r' args')) -> SimFrame sym ext (OverrideLang r) ('Just args) -> f (SimFrame sym ext (OverrideLang r') ('Just args'))
crucibleSimFrame :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType) (args :: Ctx CrucibleType) (blocks' :: Ctx (Ctx CrucibleType)) (r' :: CrucibleType) (args' :: Ctx CrucibleType) f. Functor f => (CallFrame sym ext blocks r args -> f (CallFrame sym ext blocks' r' args')) -> SimFrame sym ext (CrucibleLang blocks r) ('Just args) -> f (SimFrame sym ext (CrucibleLang blocks' r') ('Just args'))
fromCallFrame :: forall sym ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType) (a :: Ctx CrucibleType). SimFrame sym ext (CrucibleLang b r) ('Just a) -> CallFrame sym ext b r a
fromReturnFrame :: SimFrame sym ext f ('Nothing :: Maybe (Ctx CrucibleType)) -> RegEntry sym (FrameRetType f)
frameFunctionName :: forall sym ext f1 (a :: Maybe (Ctx CrucibleType)) f2. (Contravariant f2, Functor f2) => (FunctionName -> f2 FunctionName) -> SimFrame sym ext f1 a -> f2 (SimFrame sym ext f1 a)

CrucibleBranchTarget

data CrucibleBranchTarget f (args :: Maybe (Ctx CrucibleType)) where Source #

A CrucibleBranchTarget identifies a program location that is a potential join point. Each label is a merge point, and there is an additional implicit join point at function returns.

Constructors

BlockTarget :: forall (blocks :: Ctx (Ctx CrucibleType)) (args1 :: Ctx CrucibleType) (r :: CrucibleType). !(BlockID blocks args1) -> CrucibleBranchTarget (CrucibleLang blocks r) ('Just args1)
ReturnTarget :: forall f. CrucibleBranchTarget f ('Nothing :: Maybe (Ctx CrucibleType))

Instances

Instances details

TestEquality (CrucibleBranchTarget f :: Maybe (Ctx CrucibleType) -> Type) Source #
Instance details Defined in Lang.Crucible.Simulator.CallFrame Methods testEquality :: forall (a :: Maybe (Ctx CrucibleType)) (b :: Maybe (Ctx CrucibleType)). CrucibleBranchTarget f a -> CrucibleBranchTarget f b -> Maybe (a :~: b) #

ppBranchTarget :: forall f (args :: Maybe (Ctx CrucibleType)). CrucibleBranchTarget f args -> String Source #

Call frame

data CallFrame sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (args :: Ctx CrucibleType) Source #

A call frame for a crucible block.

Constructors

CallFrame

Fields

_frameCFG :: CFG ext blocks initialArgs ret
Handle to control flow graph for the current frame.
_framePostdomMap :: !(CFGPostdom blocks)
Post-dominator map for control flow graph associated with this function.
_frameBlockID :: !(Some (BlockID blocks))
_frameRegs :: !(RegMap sym args)
_frameStmts :: !(StmtSeq ext blocks ret args)
_framePostdom :: !(Some (CrucibleBranchTarget (CrucibleLang blocks ret)))

mkCallFrame Source #

Arguments

:: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType) sym. CFG ext blocks init ret	Control flow graph
-> CFGPostdom blocks	Post dominator information.
-> RegMap sym init	Initial arguments
-> CallFrame sym ext blocks ret init

Create a new call frame.

mkBlockFrame Source #

Arguments

:: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType) (args :: Ctx CrucibleType) sym. CFG ext blocks init ret	Control flow graph
-> BlockID blocks args	Entry point
-> CFGPostdom blocks	Post dominator information
-> RegMap sym args	Initial arguments
-> CallFrame sym ext blocks ret args

Create a new call frame.

framePostdomMap :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) f. Functor f => (CFGPostdom blocks -> f (CFGPostdom blocks)) -> CallFrame sym ext blocks ret ctx -> f (CallFrame sym ext blocks ret ctx) Source #

frameBlockMap :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). CallFrame sym ext blocks ret ctx -> BlockMap ext blocks ret Source #

frameHandle :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). CallFrame sym ext blocks ret ctx -> SomeHandle Source #

frameReturnType :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). CallFrame sym ext blocks ret ctx -> TypeRepr ret Source #

frameBlockID :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) f. Functor f => (Some (BlockID blocks) -> f (Some (BlockID blocks))) -> CallFrame sym ext blocks ret ctx -> f (CallFrame sym ext blocks ret ctx) Source #

frameRegs :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (args :: Ctx CrucibleType) f. Functor f => (RegMap sym args -> f (RegMap sym args)) -> CallFrame sym ext blocks ret args -> f (CallFrame sym ext blocks ret args) Source #

frameStmts :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) f. Functor f => (StmtSeq ext blocks ret ctx -> f (StmtSeq ext blocks ret ctx)) -> CallFrame sym ext blocks ret ctx -> f (CallFrame sym ext blocks ret ctx) Source #

List of statements to execute next.

framePostdom :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) f. Functor f => (Some (CrucibleBranchTarget (CrucibleLang blocks ret)) -> f (Some (CrucibleBranchTarget (CrucibleLang blocks ret)))) -> CallFrame sym ext blocks ret ctx -> f (CallFrame sym ext blocks ret ctx) Source #

List of statements to execute next.

frameProgramLoc :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). CallFrame sym ext blocks ret ctx -> ProgramLoc Source #

Return program location associated with frame.

setFrameBlock :: forall (blocks :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType) sym ext (ret :: CrucibleType) (ctx :: Ctx CrucibleType). BlockID blocks args -> RegMap sym args -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret args Source #

setFrameBreakpointPostdomInfo :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). [BreakpointName] -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret ctx Source #

extendFrame :: forall (tp :: CrucibleType) sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). TypeRepr tp -> RegValue sym tp -> StmtSeq ext blocks ret (ctx ::> tp) -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret (ctx ::> tp) Source #

Extend frame with new register.

updateFrame :: forall sym (ctx' :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) ext (ret :: CrucibleType). RegMap sym ctx' -> BlockID blocks ctx -> StmtSeq ext blocks ret ctx' -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret ctx' Source #

mergeCallFrame :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (args :: Ctx CrucibleType). IsSymInterface sym => sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (CallFrame sym ext blocks ret args) Source #

SomeHandle

data SomeHandle where Source #

A function handle is a reference to a function in a given run of the simulator. It has a set of expected arguments and return type.

Constructors

SomeHandle :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType). !(FnHandle args ret) -> SomeHandle

Instances

Instances details

Show SomeHandle Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods showsPrec :: Int -> SomeHandle -> ShowS # show :: SomeHandle -> String # showList :: [SomeHandle] -> ShowS #
Eq SomeHandle Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods (==) :: SomeHandle -> SomeHandle -> Bool # (/=) :: SomeHandle -> SomeHandle -> Bool #
Ord SomeHandle Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods compare :: SomeHandle -> SomeHandle -> Ordering # (<) :: SomeHandle -> SomeHandle -> Bool # (<=) :: SomeHandle -> SomeHandle -> Bool # (>) :: SomeHandle -> SomeHandle -> Bool # (>=) :: SomeHandle -> SomeHandle -> Bool # max :: SomeHandle -> SomeHandle -> SomeHandle # min :: SomeHandle -> SomeHandle -> SomeHandle #
Hashable SomeHandle Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods hashWithSalt :: Int -> SomeHandle -> Int # hash :: SomeHandle -> Int #

Simulator frames

data SimFrame sym ext f (args :: Maybe (Ctx CrucibleType)) where Source #

A frame on the stack.

Type parameters:

f: the type of the top frame (CrucibleLang or OverrideLang)
args: arguments; Just for call frames, Nothing for a return frame

Constructors

OF :: forall sym (ret :: CrucibleType) (args1 :: Ctx CrucibleType) ext. !(OverrideFrame sym ret args1) -> SimFrame sym ext (OverrideLang ret) ('Just args1)	Custom code to execute, typically for "overrides"
MF :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (args1 :: Ctx CrucibleType). !(CallFrame sym ext blocks ret args1) -> SimFrame sym ext (CrucibleLang blocks ret) ('Just args1)	We are executing some Crucible instructions
RF :: forall sym f ext. !FunctionName -> !(RegEntry sym (FrameRetType f)) -> SimFrame sym ext f ('Nothing :: Maybe (Ctx CrucibleType))	We should return this value.

data CrucibleLang (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) Source #

Nominal type for identifying override frames.

data OverrideLang (ret :: CrucibleType) Source #

Nominal type for identifying override frames.

Instances

Instances details

MonadState (SimState p sym ext rtp (OverrideLang ret) ('Just args)) (OverrideSim p sym ext rtp args ret) Source #

Instance details

Defined in Lang.Crucible.Simulator.OverrideSim

Methods

get :: OverrideSim p sym ext rtp args ret (SimState p sym ext rtp (OverrideLang ret) ('Just args)) #

put :: SimState p sym ext rtp (OverrideLang ret) ('Just args) -> OverrideSim p sym ext rtp args ret () #

state :: (SimState p sym ext rtp (OverrideLang ret) ('Just args) -> (a, SimState p sym ext rtp (OverrideLang ret) ('Just args))) -> OverrideSim p sym ext rtp args ret a #

type family FrameRetType f :: CrucibleType where ... Source #

Equations

FrameRetType (CrucibleLang b r) = r
FrameRetType (OverrideLang r) = r

data OverrideFrame sym (ret :: CrucibleType) (args :: Ctx CrucibleType) Source #

Frame in call to override.

Constructors

OverrideFrame
Fields _override :: !FunctionName _overrideHandle :: !SomeHandle _overrideRegMap :: !(RegMap sym args) Arguments to override.

override :: forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType) f. Functor f => (FunctionName -> f FunctionName) -> OverrideFrame sym ret args -> f (OverrideFrame sym ret args) Source #

overrideHandle :: forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType) f. Functor f => (SomeHandle -> f SomeHandle) -> OverrideFrame sym ret args -> f (OverrideFrame sym ret args) Source #

overrideRegMap :: forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType) (args' :: Ctx CrucibleType) f. Functor f => (RegMap sym args -> f (RegMap sym args')) -> OverrideFrame sym ret args -> f (OverrideFrame sym ret args') Source #

overrideSimFrame :: forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType) (r' :: CrucibleType) (args' :: Ctx CrucibleType) f. Functor f => (OverrideFrame sym r args -> f (OverrideFrame sym r' args')) -> SimFrame sym ext (OverrideLang r) ('Just args) -> f (SimFrame sym ext (OverrideLang r') ('Just args')) Source #

crucibleSimFrame :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType) (args :: Ctx CrucibleType) (blocks' :: Ctx (Ctx CrucibleType)) (r' :: CrucibleType) (args' :: Ctx CrucibleType) f. Functor f => (CallFrame sym ext blocks r args -> f (CallFrame sym ext blocks' r' args')) -> SimFrame sym ext (CrucibleLang blocks r) ('Just args) -> f (SimFrame sym ext (CrucibleLang blocks' r') ('Just args')) Source #

fromCallFrame :: forall sym ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType) (a :: Ctx CrucibleType). SimFrame sym ext (CrucibleLang b r) ('Just a) -> CallFrame sym ext b r a Source #

fromReturnFrame :: SimFrame sym ext f ('Nothing :: Maybe (Ctx CrucibleType)) -> RegEntry sym (FrameRetType f) Source #

frameFunctionName :: forall sym ext f1 (a :: Maybe (Ctx CrucibleType)) f2. (Contravariant f2, Functor f2) => (FunctionName -> f2 FunctionName) -> SimFrame sym ext f1 a -> f2 (SimFrame sym ext f1 a) Source #