Copyright	(c) Galois Inc 2014-2016
License	BSD3
Maintainer	Joe Hendrix <jhendrix@galois.com>
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.CFG.Core

Contents

CFG
Blocks
Jump targets
Statements
Expressions
Re-exports

Description

Define a SSA-based control flow graph data structure using a side-effect free expression syntax.

Unlike usual SSA forms, we do not use phi-functions, but instead rely on an argument-passing formulation for basic blocks. In this form, concrete values are bound to formal parameters instead of using phi-functions that switch on the place from which you jumped.

Synopsis

data CFG (ext :: Type) (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType) = CFG {
- cfgHandle :: FnHandle init ret
- cfgBlockMap :: !(BlockMap ext blocks ret)
- cfgEntryBlockID :: !(BlockID blocks init)
- cfgBreakpoints :: !(Bimap BreakpointName (Some (BlockID blocks)))
}
data SomeCFG ext (init :: Ctx CrucibleType) (ret :: CrucibleType) where
- SomeCFG :: CFG ext blocks init ret -> SomeCFG ext init ret
class HasSomeCFG f ext init ret | f -> ext, f -> init, f -> ret where
- getCFG :: f b -> SomeCFG ext init ret
data AnyCFG ext where
- AnyCFG :: CFG ext blocks init ret -> AnyCFG ext
ppCFG :: PrettyExt ext => Bool -> CFG ext blocks init ret -> Doc ann
ppCFG' :: PrettyExt ext => Bool -> CFGPostdom blocks -> CFG ext blocks init ret -> Doc ann
cfgArgTypes :: CFG ext blocks init ret -> CtxRepr init
cfgReturnType :: CFG ext blocks init ret -> TypeRepr ret
type CFGPostdom blocks = Assignment (Const [Some (BlockID blocks)]) blocks
type BlockMap ext blocks ret = Assignment (Block ext blocks ret) blocks
getBlock :: BlockID blocks args -> BlockMap ext blocks ret -> Block ext blocks ret args
extendBlockMap :: Assignment (Block ext blocks ret) b -> Assignment (Block ext (blocks ::> args) ret) b
newtype BlockID (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType) = BlockID {
- blockIDIndex :: Index blocks tp
}
extendBlockID :: KnownDiff l r => BlockID l tp -> BlockID r tp
extendBlockID' :: Diff l r -> BlockID l tp -> BlockID r tp
data Block ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ctx = Block {
- blockID :: !(BlockID blocks ctx)
- blockInputs :: !(CtxRepr ctx)
- _blockStmts :: !(StmtSeq ext blocks ret ctx)
}
blockLoc :: Block ext blocks ret ctx -> ProgramLoc
blockStmts :: Simple Lens (Block ext b r c) (StmtSeq ext b r c)
withBlockTermStmt :: Block ext blocks ret args -> (forall ctx. ProgramLoc -> TermStmt blocks ret ctx -> r) -> r
nextBlocks :: Block ext b r a -> [Some (BlockID b)]
data JumpTarget blocks ctx where
- JumpTarget :: !(BlockID blocks args) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> JumpTarget blocks ctx
extendJumpTarget :: Diff blocks' blocks -> JumpTarget blocks' ctx -> JumpTarget blocks ctx
jumpTargetID :: JumpTarget blocks ctx -> Some (BlockID blocks)
data SwitchTarget blocks ctx tp where
- SwitchTarget :: !(BlockID blocks (args ::> tp)) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> SwitchTarget blocks ctx tp
switchTargetID :: SwitchTarget blocks ctx tp -> Some (BlockID blocks)
extendSwitchTarget :: Diff blocks' blocks -> SwitchTarget blocks' ctx tp -> SwitchTarget blocks ctx tp
data StmtSeq ext blocks (ret :: CrucibleType) ctx where
- ConsStmt :: !ProgramLoc -> !(Stmt ext ctx ctx') -> !(StmtSeq ext blocks ret ctx') -> StmtSeq ext blocks ret ctx
- TermStmt :: !ProgramLoc -> !(TermStmt blocks ret ctx) -> StmtSeq ext blocks ret ctx
firstStmtLoc :: StmtSeq ext b r ctx -> ProgramLoc
stmtSeqTermStmt :: Functor f => (forall ctx. (ProgramLoc, TermStmt b ret ctx) -> f (StmtSeq ext b' ret ctx)) -> StmtSeq ext b ret args -> f (StmtSeq ext b' ret args)
data Stmt ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) where
- SetReg :: !(TypeRepr tp) -> !(Expr ext ctx tp) -> Stmt ext ctx (ctx ::> tp)
- ExtendAssign :: !(StmtExtension ext (Reg ctx) tp) -> Stmt ext ctx (ctx ::> tp)
- CallHandle :: !(TypeRepr ret) -> !(Reg ctx (FunctionHandleType args ret)) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> Stmt ext ctx (ctx ::> ret)
- Print :: !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
- ReadGlobal :: !(GlobalVar tp) -> Stmt ext ctx (ctx ::> tp)
- WriteGlobal :: !(GlobalVar tp) -> !(Reg ctx tp) -> Stmt ext ctx ctx
- FreshConstant :: !(BaseTypeRepr bt) -> !(Maybe SolverSymbol) -> Stmt ext ctx (ctx ::> BaseToType bt)
- FreshFloat :: !(FloatInfoRepr fi) -> !(Maybe SolverSymbol) -> Stmt ext ctx (ctx ::> FloatType fi)
- FreshNat :: !(Maybe SolverSymbol) -> Stmt ext ctx (ctx ::> NatType)
- NewRefCell :: !(TypeRepr tp) -> !(Reg ctx tp) -> Stmt ext ctx (ctx ::> ReferenceType tp)
- NewEmptyRefCell :: !(TypeRepr tp) -> Stmt ext ctx (ctx ::> ReferenceType tp)
- ReadRefCell :: !(Reg ctx (ReferenceType tp)) -> Stmt ext ctx (ctx ::> tp)
- WriteRefCell :: !(Reg ctx (ReferenceType tp)) -> !(Reg ctx tp) -> Stmt ext ctx ctx
- DropRefCell :: !(Reg ctx (ReferenceType tp)) -> Stmt ext ctx ctx
- Assert :: !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
- Assume :: !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
ppStmt :: PrettyExt ext => Size ctx -> Stmt ext ctx ctx' -> Doc ann
nextStmtHeight :: Size ctx -> Stmt ext ctx ctx' -> Size ctx'
applyEmbeddingStmt :: forall ext ctx ctx' sctx. TraverseExt ext => CtxEmbedding ctx ctx' -> Stmt ext ctx sctx -> Pair (Stmt ext ctx') (CtxEmbedding sctx)
data TermStmt blocks (ret :: CrucibleType) (ctx :: Ctx CrucibleType) where
- Jump :: !(JumpTarget blocks ctx) -> TermStmt blocks ret ctx
- Br :: !(Reg ctx BoolType) -> !(JumpTarget blocks ctx) -> !(JumpTarget blocks ctx) -> TermStmt blocks ret ctx
- MaybeBranch :: !(TypeRepr tp) -> !(Reg ctx (MaybeType tp)) -> !(SwitchTarget blocks ctx tp) -> !(JumpTarget blocks ctx) -> TermStmt blocks rtp ctx
- VariantElim :: !(CtxRepr varctx) -> !(Reg ctx (VariantType varctx)) -> !(Assignment (SwitchTarget blocks ctx) varctx) -> TermStmt blocks ret ctx
- Return :: !(Reg ctx ret) -> TermStmt blocks ret ctx
- TailCall :: !(Reg ctx (FunctionHandleType args ret)) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> TermStmt blocks ret ctx
- ErrorStmt :: !(Reg ctx (StringType Unicode)) -> TermStmt blocks ret ctx
termStmtNextBlocks :: TermStmt b ret ctx -> Maybe [Some (BlockID b)]
newtype Expr ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType) = App (App ext (Reg ctx) tp)
newtype Reg (ctx :: Ctx CrucibleType) (tp :: CrucibleType) = Reg {
- regIndex :: Index ctx tp
}
extendReg :: Reg ctx tp -> Reg (ctx ::> r) tp
lastReg :: KnownContext ctx => Reg (ctx ::> tp) tp
module Lang.Crucible.Types
module Lang.Crucible.CFG.Common
module Data.Parameterized.Classes
module Data.Parameterized.Some

CFG

data CFG (ext :: Type) (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType) Source #

A CFG consists of:

a function handle, uniquely identifying the function this CFG implements;
a block map, representing the main CFG data structure;
and the identifier of the function entry point.

The blocks type parameter maps each block identifier to the formal arguments it expects. The init type parameter identifies the formal arguments of the function represented by this control-flow graph, which correspond to the formal arguments of the CFG entry point. The ret type parameter indicates the return type of the function.

Constructors

CFG
Fields cfgHandle :: FnHandle init ret cfgBlockMap :: !(BlockMap ext blocks ret) cfgEntryBlockID :: !(BlockID blocks init) cfgBreakpoints :: !(Bimap BreakpointName (Some (BlockID blocks)))

Instances

Instances details

PrettyExt ext => Show (CFG ext blocks init ret) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods showsPrec :: Int -> CFG ext blocks init ret -> ShowS # show :: CFG ext blocks init ret -> String # showList :: [CFG ext blocks init ret] -> ShowS #

data SomeCFG ext (init :: Ctx CrucibleType) (ret :: CrucibleType) where Source #

Control flow graph with some blocks. This data type closes existentially over the blocks type parameter.

Constructors

SomeCFG :: CFG ext blocks init ret -> SomeCFG ext init ret

Instances

Instances details

PrettyExt ext => Show (SomeCFG ext i r) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods showsPrec :: Int -> SomeCFG ext i r -> ShowS # show :: SomeCFG ext i r -> String # showList :: [SomeCFG ext i r] -> ShowS #

class HasSomeCFG f ext init ret | f -> ext, f -> init, f -> ret where Source #

Class for types that embed a CFG of some sort.

Methods

getCFG :: f b -> SomeCFG ext init ret Source #

data AnyCFG ext where Source #

Control flow graph. This data type closes existentially over all the type parameters except ext.

Constructors

AnyCFG :: CFG ext blocks init ret -> AnyCFG ext

Instances

Instances details

PrettyExt ext => Show (AnyCFG ext) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods showsPrec :: Int -> AnyCFG ext -> ShowS # show :: AnyCFG ext -> String # showList :: [AnyCFG ext] -> ShowS #

ppCFG Source #

Arguments

:: PrettyExt ext
=> Bool	Flag indicates if we should print line numbers
-> CFG ext blocks init ret
-> Doc ann

Pretty print a CFG.

ppCFG' Source #

Arguments

:: PrettyExt ext
=> Bool	Flag indicates if we should print line numbers
-> CFGPostdom blocks
-> CFG ext blocks init ret
-> Doc ann

Pretty print CFG with postdom information.

cfgArgTypes :: CFG ext blocks init ret -> CtxRepr init Source #

cfgReturnType :: CFG ext blocks init ret -> TypeRepr ret Source #

type CFGPostdom blocks = Assignment (Const [Some (BlockID blocks)]) blocks Source #

Postdominator information about a CFG. The assignment maps each block to the postdominators of the given block. The postdominators are ordered with nearest postdominator first.

Blocks

type BlockMap ext blocks ret = Assignment (Block ext blocks ret) blocks Source #

A mapping from block indices to CFG blocks

getBlock :: BlockID blocks args -> BlockMap ext blocks ret -> Block ext blocks ret args Source #

extendBlockMap :: Assignment (Block ext blocks ret) b -> Assignment (Block ext (blocks ::> args) ret) b Source #

newtype BlockID (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType) Source #

A BlockID uniquely identifies a block in a control-flow graph. Each block has an associated context, indicating the formal arguments it expects to find in registers from its calling locations.

Constructors

BlockID
Fields blockIDIndex :: Index blocks tp

Instances

Instances details

TestEquality (BlockID blocks :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods testEquality :: forall (a :: k) (b :: k). BlockID blocks a -> BlockID blocks b -> Maybe (a :~: b) #
OrdF (BlockID blocks :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods compareF :: forall (x :: k) (y :: k). BlockID blocks x -> BlockID blocks y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). BlockID blocks x -> BlockID blocks y -> Bool # ltF :: forall (x :: k) (y :: k). BlockID blocks x -> BlockID blocks y -> Bool # geqF :: forall (x :: k) (y :: k). BlockID blocks x -> BlockID blocks y -> Bool # gtF :: forall (x :: k) (y :: k). BlockID blocks x -> BlockID blocks y -> Bool #
ShowF (BlockID blocks :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods withShow :: forall p q (tp :: k) a. p (BlockID blocks) -> q tp -> (Show (BlockID blocks tp) => a) -> a # showF :: forall (tp :: k). BlockID blocks tp -> String # showsPrecF :: forall (tp :: k). Int -> BlockID blocks tp -> String -> String #
Show (BlockID blocks ctx) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods showsPrec :: Int -> BlockID blocks ctx -> ShowS # show :: BlockID blocks ctx -> String # showList :: [BlockID blocks ctx] -> ShowS #
Eq (BlockID blocks tp) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods (==) :: BlockID blocks tp -> BlockID blocks tp -> Bool # (/=) :: BlockID blocks tp -> BlockID blocks tp -> Bool #
Ord (BlockID blocks tp) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods compare :: BlockID blocks tp -> BlockID blocks tp -> Ordering # (<) :: BlockID blocks tp -> BlockID blocks tp -> Bool # (<=) :: BlockID blocks tp -> BlockID blocks tp -> Bool # (>) :: BlockID blocks tp -> BlockID blocks tp -> Bool # (>=) :: BlockID blocks tp -> BlockID blocks tp -> Bool # max :: BlockID blocks tp -> BlockID blocks tp -> BlockID blocks tp # min :: BlockID blocks tp -> BlockID blocks tp -> BlockID blocks tp #
Pretty (BlockID blocks tp) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods pretty :: BlockID blocks tp -> Doc ann # prettyList :: [BlockID blocks tp] -> Doc ann #

extendBlockID :: KnownDiff l r => BlockID l tp -> BlockID r tp Source #

extendBlockID' :: Diff l r -> BlockID l tp -> BlockID r tp Source #

data Block ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ctx Source #

A basic block within a function.

Constructors

Block
Fields blockID :: !(BlockID blocks ctx) The unique identifier of this block blockInputs :: !(CtxRepr ctx) The expected types of the formal arguments to this block _blockStmts :: !(StmtSeq ext blocks ret ctx) The sequence of statements in this block

Instances

Instances details

PrettyExt ext => ShowF (Block ext blocks ret :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods withShow :: forall p q (tp :: k) a. p (Block ext blocks ret) -> q tp -> (Show (Block ext blocks ret tp) => a) -> a # showF :: forall (tp :: k). Block ext blocks ret tp -> String # showsPrecF :: forall (tp :: k). Int -> Block ext blocks ret tp -> String -> String #
PrettyExt ext => Show (Block ext blocks ret args) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods showsPrec :: Int -> Block ext blocks ret args -> ShowS # show :: Block ext blocks ret args -> String # showList :: [Block ext blocks ret args] -> ShowS #

blockLoc :: Block ext blocks ret ctx -> ProgramLoc Source #

Return location of start of block.

blockStmts :: Simple Lens (Block ext b r c) (StmtSeq ext b r c) Source #

withBlockTermStmt :: Block ext blocks ret args -> (forall ctx. ProgramLoc -> TermStmt blocks ret ctx -> r) -> r Source #

Get the terminal statement of a basic block. This is implemented in a CPS style due to the block context.

nextBlocks :: Block ext b r a -> [Some (BlockID b)] Source #

Jump targets

data JumpTarget blocks ctx where Source #

Target for jump and branch statements

Constructors

JumpTarget :: !(BlockID blocks args) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> JumpTarget blocks ctx

Instances

Instances details

ApplyEmbedding (JumpTarget blocks :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods applyEmbedding :: forall (ctx :: Ctx k) (ctx' :: Ctx k). CtxEmbedding ctx ctx' -> JumpTarget blocks ctx -> JumpTarget blocks ctx' #
ExtendContext (JumpTarget blocks :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods extendContext :: forall (ctx :: Ctx k) (ctx' :: Ctx k). Diff ctx ctx' -> JumpTarget blocks ctx -> JumpTarget blocks ctx' #
Pretty (JumpTarget blocks ctx) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods pretty :: JumpTarget blocks ctx -> Doc ann # prettyList :: [JumpTarget blocks ctx] -> Doc ann #

extendJumpTarget :: Diff blocks' blocks -> JumpTarget blocks' ctx -> JumpTarget blocks ctx Source #

jumpTargetID :: JumpTarget blocks ctx -> Some (BlockID blocks) Source #

data SwitchTarget blocks ctx tp where Source #

Target for a switch statement.

Constructors

SwitchTarget :: !(BlockID blocks (args ::> tp)) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> SwitchTarget blocks ctx tp

Instances

Instances details

ApplyEmbedding' (SwitchTarget blocks :: Ctx CrucibleType -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods applyEmbedding' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'). CtxEmbedding ctx ctx' -> SwitchTarget blocks ctx v -> SwitchTarget blocks ctx' v #
ExtendContext' (SwitchTarget blocks :: Ctx CrucibleType -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods extendContext' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'). Diff ctx ctx' -> SwitchTarget blocks ctx v -> SwitchTarget blocks ctx' v #

switchTargetID :: SwitchTarget blocks ctx tp -> Some (BlockID blocks) Source #

extendSwitchTarget :: Diff blocks' blocks -> SwitchTarget blocks' ctx tp -> SwitchTarget blocks ctx tp Source #

Statements

data StmtSeq ext blocks (ret :: CrucibleType) ctx where Source #

A sequence of straight-line program statements that end with a terminating statement (return, jump, etc).

Constructors

ConsStmt :: !ProgramLoc -> !(Stmt ext ctx ctx') -> !(StmtSeq ext blocks ret ctx') -> StmtSeq ext blocks ret ctx
TermStmt :: !ProgramLoc -> !(TermStmt blocks ret ctx) -> StmtSeq ext blocks ret ctx

Instances

Instances details

TraverseExt ext => ApplyEmbedding (StmtSeq ext blocks ret :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods applyEmbedding :: forall (ctx :: Ctx k) (ctx' :: Ctx k). CtxEmbedding ctx ctx' -> StmtSeq ext blocks ret ctx -> StmtSeq ext blocks ret ctx' #

firstStmtLoc :: StmtSeq ext b r ctx -> ProgramLoc Source #

Return the location of a statement.

stmtSeqTermStmt :: Functor f => (forall ctx. (ProgramLoc, TermStmt b ret ctx) -> f (StmtSeq ext b' ret ctx)) -> StmtSeq ext b ret args -> f (StmtSeq ext b' ret args) Source #

A lens-like operation that gives one access to program location and term statement, and allows the terminal statement to be replaced with an arbitrary sequence of statements.

data Stmt ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) where Source #

A sequential statement that does not affect the program location within the current block or leave the current block.

Constructors

SetReg :: !(TypeRepr tp) -> !(Expr ext ctx tp) -> Stmt ext ctx (ctx ::> tp)
ExtendAssign :: !(StmtExtension ext (Reg ctx) tp) -> Stmt ext ctx (ctx ::> tp)
CallHandle :: !(TypeRepr ret) -> !(Reg ctx (FunctionHandleType args ret)) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> Stmt ext ctx (ctx ::> ret)
Print :: !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
ReadGlobal :: !(GlobalVar tp) -> Stmt ext ctx (ctx ::> tp)
WriteGlobal :: !(GlobalVar tp) -> !(Reg ctx tp) -> Stmt ext ctx ctx
FreshConstant :: !(BaseTypeRepr bt) -> !(Maybe SolverSymbol) -> Stmt ext ctx (ctx ::> BaseToType bt)
FreshFloat :: !(FloatInfoRepr fi) -> !(Maybe SolverSymbol) -> Stmt ext ctx (ctx ::> FloatType fi)
FreshNat :: !(Maybe SolverSymbol) -> Stmt ext ctx (ctx ::> NatType)
NewRefCell :: !(TypeRepr tp) -> !(Reg ctx tp) -> Stmt ext ctx (ctx ::> ReferenceType tp)
NewEmptyRefCell :: !(TypeRepr tp) -> Stmt ext ctx (ctx ::> ReferenceType tp)
ReadRefCell :: !(Reg ctx (ReferenceType tp)) -> Stmt ext ctx (ctx ::> tp)
WriteRefCell :: !(Reg ctx (ReferenceType tp)) -> !(Reg ctx tp) -> Stmt ext ctx ctx
DropRefCell :: !(Reg ctx (ReferenceType tp)) -> Stmt ext ctx ctx
Assert :: !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
Assume :: !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx

ppStmt :: PrettyExt ext => Size ctx -> Stmt ext ctx ctx' -> Doc ann Source #

nextStmtHeight :: Size ctx -> Stmt ext ctx ctx' -> Size ctx' Source #

applyEmbeddingStmt :: forall ext ctx ctx' sctx. TraverseExt ext => CtxEmbedding ctx ctx' -> Stmt ext ctx sctx -> Pair (Stmt ext ctx') (CtxEmbedding sctx) Source #

data TermStmt blocks (ret :: CrucibleType) (ctx :: Ctx CrucibleType) where Source #

Constructors

Jump :: !(JumpTarget blocks ctx) -> TermStmt blocks ret ctx
Br :: !(Reg ctx BoolType) -> !(JumpTarget blocks ctx) -> !(JumpTarget blocks ctx) -> TermStmt blocks ret ctx
MaybeBranch :: !(TypeRepr tp) -> !(Reg ctx (MaybeType tp)) -> !(SwitchTarget blocks ctx tp) -> !(JumpTarget blocks ctx) -> TermStmt blocks rtp ctx
VariantElim :: !(CtxRepr varctx) -> !(Reg ctx (VariantType varctx)) -> !(Assignment (SwitchTarget blocks ctx) varctx) -> TermStmt blocks ret ctx
Return :: !(Reg ctx ret) -> TermStmt blocks ret ctx
TailCall :: !(Reg ctx (FunctionHandleType args ret)) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> TermStmt blocks ret ctx
ErrorStmt :: !(Reg ctx (StringType Unicode)) -> TermStmt blocks ret ctx

Instances

Instances details

ApplyEmbedding (TermStmt blocks ret :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods applyEmbedding :: forall (ctx :: Ctx k) (ctx' :: Ctx k). CtxEmbedding ctx ctx' -> TermStmt blocks ret ctx -> TermStmt blocks ret ctx' #
ExtendContext (TermStmt blocks ret :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods extendContext :: forall (ctx :: Ctx k) (ctx' :: Ctx k). Diff ctx ctx' -> TermStmt blocks ret ctx -> TermStmt blocks ret ctx' #
Pretty (TermStmt blocks ret ctx) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods pretty :: TermStmt blocks ret ctx -> Doc ann # prettyList :: [TermStmt blocks ret ctx] -> Doc ann #

termStmtNextBlocks :: TermStmt b ret ctx -> Maybe [Some (BlockID b)] Source #

Return the set of possible next blocks from a TermStmt

Expressions

newtype Expr ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType) Source #

An expression is just an App applied to some registers.

Constructors

App (App ext (Reg ctx) tp)

Instances

Instances details

TraversableFC (ExprExtension ext) => ApplyEmbedding' (Expr ext :: Ctx CrucibleType -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods applyEmbedding' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'). CtxEmbedding ctx ctx' -> Expr ext ctx v -> Expr ext ctx' v #
TraversableFC (ExprExtension ext) => ExtendContext' (Expr ext :: Ctx CrucibleType -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods extendContext' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'). Diff ctx ctx' -> Expr ext ctx v -> Expr ext ctx' v #
IsString (Expr ext ctx (StringType Unicode)) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods fromString :: String -> Expr ext ctx (StringType Unicode) #
PrettyApp (ExprExtension ext) => Pretty (Expr ext ctx tp) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods pretty :: Expr ext ctx tp -> Doc ann # prettyList :: [Expr ext ctx tp] -> Doc ann #

newtype Reg (ctx :: Ctx CrucibleType) (tp :: CrucibleType) Source #

A temporary register identifier introduced during translation. These are unique to the current function. The ctx parameter is a context containing the types of all the temporary registers currently in scope, and the tp parameter indicates the type of this register (which necessarily appears somewhere in ctx)

Constructors

Reg
Fields regIndex :: Index ctx tp

Instances

Instances details

ApplyEmbedding' Reg Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods applyEmbedding' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'). CtxEmbedding ctx ctx' -> Reg ctx v -> Reg ctx' v #
ExtendContext' Reg Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods extendContext' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'). Diff ctx ctx' -> Reg ctx v -> Reg ctx' v #
TestEquality (Reg ctx :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods testEquality :: forall (a :: k) (b :: k). Reg ctx a -> Reg ctx b -> Maybe (a :~: b) #
OrdF (Reg ctx :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods compareF :: forall (x :: k) (y :: k). Reg ctx x -> Reg ctx y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). Reg ctx x -> Reg ctx y -> Bool # ltF :: forall (x :: k) (y :: k). Reg ctx x -> Reg ctx y -> Bool # geqF :: forall (x :: k) (y :: k). Reg ctx x -> Reg ctx y -> Bool # gtF :: forall (x :: k) (y :: k). Reg ctx x -> Reg ctx y -> Bool #
ShowF (Reg ctx :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods withShow :: forall p q (tp :: k) a. p (Reg ctx) -> q tp -> (Show (Reg ctx tp) => a) -> a # showF :: forall (tp :: k). Reg ctx tp -> String # showsPrecF :: forall (tp :: k). Int -> Reg ctx tp -> String -> String #
Show (Reg ctx tp) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods showsPrec :: Int -> Reg ctx tp -> ShowS # show :: Reg ctx tp -> String # showList :: [Reg ctx tp] -> ShowS #
Eq (Reg ctx tp) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods (==) :: Reg ctx tp -> Reg ctx tp -> Bool # (/=) :: Reg ctx tp -> Reg ctx tp -> Bool #
Ord (Reg ctx tp) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods compare :: Reg ctx tp -> Reg ctx tp -> Ordering # (<) :: Reg ctx tp -> Reg ctx tp -> Bool # (<=) :: Reg ctx tp -> Reg ctx tp -> Bool # (>) :: Reg ctx tp -> Reg ctx tp -> Bool # (>=) :: Reg ctx tp -> Reg ctx tp -> Bool # max :: Reg ctx tp -> Reg ctx tp -> Reg ctx tp # min :: Reg ctx tp -> Reg ctx tp -> Reg ctx tp #
Pretty (Reg ctx tp) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods pretty :: Reg ctx tp -> Doc ann # prettyList :: [Reg ctx tp] -> Doc ann #

extendReg :: Reg ctx tp -> Reg (ctx ::> r) tp Source #

Extend the set of registers in scope for a given register value without changing its index or type.

lastReg :: KnownContext ctx => Reg (ctx ::> tp) tp Source #

Finds the value of the most-recently introduced register in scope.

Re-exports

module Lang.Crucible.Types

module Lang.Crucible.CFG.Common

module Data.Parameterized.Classes

module Data.Parameterized.Some