Lang.Crucible.Simulator.CallFrame

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

CrucibleBranchTarget

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

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

TestEquality (CrucibleBranchTarget f :: Maybe (Ctx CrucibleType) -> Type)

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

Call frame

data CallFrame sym ext blocks ret args

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

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

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)

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)

List of statements to execute next.

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

List of statements to execute next.

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

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

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)

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'

mergeCallFrame :: IsSymInterface sym => sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (CallFrame sym ext blocks ret args)

SomeHandle

data SomeHandle where

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

Show SomeHandle

Defined in Lang.Crucible.FunctionHandle

Methods

showsPrec :: Int -> SomeHandle -> ShowS

show :: SomeHandle -> String

showList :: [SomeHandle] -> ShowS

Eq SomeHandle

Defined in Lang.Crucible.FunctionHandle

Methods

(==) :: SomeHandle -> SomeHandle -> Bool

(/=) :: SomeHandle -> SomeHandle -> Bool

Ord SomeHandle

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

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

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)

Nominal type for identifying override frames.

data OverrideLang (ret :: CrucibleType)

Nominal type for identifying override frames.

Instances

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

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

Equations

FrameRetType (CrucibleLang b r) = r

FrameRetType (OverrideLang r) = r

data OverrideFrame sym (ret :: CrucibleType) args

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

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