Copyright	(c) Galois Inc 2014
License	BSD3
Maintainer	Joe Hendrix <jhendrix@galois.com>
Stability	provisional
Safe Haskell	Safe-Inferred
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 :: !(BlockID blocks args) -> CrucibleBranchTarget (CrucibleLang blocks r) ('Just args)
- ReturnTarget :: CrucibleBranchTarget f 'Nothing
ppBranchTarget :: CrucibleBranchTarget f args -> String
data CallFrame sym ext blocks ret args = forall initialArgs.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 :: CFG ext blocks init ret -> CFGPostdom blocks -> RegMap sym init -> CallFrame sym ext blocks ret init
mkBlockFrame :: CFG ext blocks init ret -> BlockID blocks args -> CFGPostdom blocks -> RegMap sym args -> CallFrame sym ext blocks ret args
framePostdomMap :: Simple Lens (CallFrame sym ext blocks ret ctx) (CFGPostdom blocks)
frameBlockMap :: CallFrame sym ext blocks ret ctx -> BlockMap ext blocks ret
frameHandle :: CallFrame sym ext blocks ret ctx -> SomeHandle
frameReturnType :: CallFrame sym ext blocks ret ctx -> TypeRepr ret
frameBlockID :: Simple Lens (CallFrame sym ext blocks ret ctx) (Some (BlockID blocks))
frameRegs :: Simple Lens (CallFrame sym ext blocks ret args) (RegMap sym args)
frameStmts :: Simple Lens (CallFrame sym ext blocks ret ctx) (StmtSeq ext blocks ret ctx)
framePostdom :: Simple Lens (CallFrame sym ext blocks ret ctx) (Some (CrucibleBranchTarget (CrucibleLang blocks ret)))
frameProgramLoc :: CallFrame sym ext blocks ret ctx -> ProgramLoc
setFrameBlock :: BlockID blocks args -> RegMap sym args -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret args
setFrameBreakpointPostdomInfo :: [BreakpointName] -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret ctx
extendFrame :: 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 :: RegMap sym ctx' -> BlockID blocks ctx -> StmtSeq ext blocks ret ctx' -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret ctx'
mergeCallFrame :: IsSymInterface sym => sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (CallFrame sym ext blocks ret args)
data SomeHandle where
- SomeHandle :: !(FnHandle args ret) -> SomeHandle
data SimFrame sym ext l (args :: Maybe (Ctx CrucibleType)) where
- OF :: !(OverrideFrame sym ret args) -> SimFrame sym ext (OverrideLang ret) ('Just args)
- MF :: !(CallFrame sym ext blocks ret args) -> SimFrame sym ext (CrucibleLang blocks ret) ('Just args)
- RF :: !FunctionName -> !(RegEntry sym (FrameRetType f)) -> SimFrame sym ext f 'Nothing
data CrucibleLang (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
data OverrideLang (ret :: CrucibleType)
type family FrameRetType (f :: Type) :: CrucibleType where ...
data OverrideFrame sym (ret :: CrucibleType) args = OverrideFrame {
- _override :: !FunctionName
- _overrideHandle :: !SomeHandle
- _overrideRegMap :: !(RegMap sym args)
}
override :: Simple Lens (OverrideFrame sym ret args) FunctionName
overrideHandle :: Simple Lens (OverrideFrame sym ret args) SomeHandle
overrideRegMap :: Lens (OverrideFrame sym ret args) (OverrideFrame sym ret args') (RegMap sym args) (RegMap sym args')
overrideSimFrame :: Lens (SimFrame sym ext (OverrideLang r) ('Just args)) (SimFrame sym ext (OverrideLang r') ('Just args')) (OverrideFrame sym r args) (OverrideFrame sym r' args')
crucibleSimFrame :: Lens (SimFrame sym ext (CrucibleLang blocks r) ('Just args)) (SimFrame sym ext (CrucibleLang blocks' r') ('Just args')) (CallFrame sym ext blocks r args) (CallFrame sym ext blocks' r' args')
fromCallFrame :: SimFrame sym ext (CrucibleLang b r) ('Just a) -> CallFrame sym ext b r a
fromReturnFrame :: SimFrame sym ext f 'Nothing -> RegEntry sym (FrameRetType f)
frameFunctionName :: Getter (SimFrame sym ext f a) FunctionName

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 :: !(BlockID blocks args) -> CrucibleBranchTarget (CrucibleLang blocks r) ('Just args)
ReturnTarget :: CrucibleBranchTarget f 'Nothing

Instances

Instances details

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

ppBranchTarget :: CrucibleBranchTarget f args -> String Source #

Call frame

data CallFrame sym ext blocks ret args Source #

A call frame for a crucible block.

Constructors

forall initialArgs. 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

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

:: 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 :: Simple Lens (CallFrame sym ext blocks ret ctx) (CFGPostdom blocks) Source #

frameBlockMap :: CallFrame sym ext blocks ret ctx -> BlockMap ext blocks ret Source #

frameHandle :: CallFrame sym ext blocks ret ctx -> SomeHandle Source #

frameReturnType :: CallFrame sym ext blocks ret ctx -> TypeRepr ret Source #

frameBlockID :: Simple Lens (CallFrame sym ext blocks ret ctx) (Some (BlockID blocks)) Source #

frameRegs :: Simple Lens (CallFrame sym ext blocks ret args) (RegMap sym args) Source #

frameStmts :: Simple Lens (CallFrame sym ext blocks ret ctx) (StmtSeq ext blocks ret ctx) Source #

List of statements to execute next.

framePostdom :: Simple Lens (CallFrame sym ext blocks ret ctx) (Some (CrucibleBranchTarget (CrucibleLang blocks ret))) Source #

List of statements to execute next.

frameProgramLoc :: CallFrame sym ext blocks ret ctx -> ProgramLoc Source #

Return program location associated with frame.

setFrameBlock :: BlockID blocks args -> RegMap sym args -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret args Source #

setFrameBreakpointPostdomInfo :: [BreakpointName] -> CallFrame sym ext blocks ret ctx -> CallFrame sym ext blocks ret ctx Source #

extendFrame :: 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 :: 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 :: 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 :: !(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 l (args :: Maybe (Ctx CrucibleType)) where Source #

Constructors

OF :: !(OverrideFrame sym ret args) -> SimFrame sym ext (OverrideLang ret) ('Just args)	Custom code to execute, typically for "overrides"
MF :: !(CallFrame sym ext blocks ret args) -> SimFrame sym ext (CrucibleLang blocks ret) ('Just args)	We are executing some Crucible instructions
RF :: !FunctionName -> !(RegEntry sym (FrameRetType f)) -> SimFrame sym ext f 'Nothing	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 :: Type) :: CrucibleType where ... Source #

Equations

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

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

Frame in call to override.

Constructors

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

override :: Simple Lens (OverrideFrame sym ret args) FunctionName Source #

overrideHandle :: Simple Lens (OverrideFrame sym ret args) SomeHandle Source #

overrideRegMap :: Lens (OverrideFrame sym ret args) (OverrideFrame sym ret args') (RegMap sym args) (RegMap sym args') Source #

overrideSimFrame :: Lens (SimFrame sym ext (OverrideLang r) ('Just args)) (SimFrame sym ext (OverrideLang r') ('Just args')) (OverrideFrame sym r args) (OverrideFrame sym r' args') Source #

crucibleSimFrame :: Lens (SimFrame sym ext (CrucibleLang blocks r) ('Just args)) (SimFrame sym ext (CrucibleLang blocks' r') ('Just args')) (CallFrame sym ext blocks r args) (CallFrame sym ext blocks' r' args') Source #

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

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

frameFunctionName :: Getter (SimFrame sym ext f a) FunctionName Source #