Copyright	(c) Galois Inc 2014-2016
License	BSD3
Maintainer	Joe Hendrix <jhendrix@galois.com>
Safe Haskell	None
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 (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 :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext blocks init ret -> SomeCFG ext init ret
class HasSomeCFG (f :: k -> Type) ext (init :: Ctx CrucibleType) (ret :: CrucibleType) | f -> ext, f -> init, f -> ret where
- getCFG :: forall (b :: k). f b -> SomeCFG ext init ret
data AnyCFG ext where
- AnyCFG :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext blocks init ret -> AnyCFG ext
ppCFG :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType) ann. PrettyExt ext => Bool -> CFG ext blocks init ret -> Doc ann
ppCFG' :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType) ann. PrettyExt ext => Bool -> CFGPostdom blocks -> CFG ext blocks init ret -> Doc ann
cfgArgTypes :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext blocks init ret -> CtxRepr init
cfgReturnType :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext blocks init ret -> TypeRepr ret
type CFGPostdom (blocks :: Ctx (Ctx CrucibleType)) = Assignment (Const [Some (BlockID blocks)] :: Ctx CrucibleType -> Type) blocks
type BlockMap ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) = Assignment (Block ext blocks ret) blocks
getBlock :: forall (blocks :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType) ext (ret :: CrucibleType). BlockID blocks args -> BlockMap ext blocks ret -> Block ext blocks ret args
extendBlockMap :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (b :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType). 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 :: forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType). KnownDiff l r => BlockID l tp -> BlockID r tp
extendBlockID' :: forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType). Diff l r -> BlockID l tp -> BlockID r tp
data Block ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) = Block {
- blockID :: !(BlockID blocks ctx)
- blockInputs :: !(CtxRepr ctx)
- _blockStmts :: !(StmtSeq ext blocks ret ctx)
}
blockLoc :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). Block ext blocks ret ctx -> ProgramLoc
blockStmts :: forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType) (c :: Ctx CrucibleType) f. Functor f => (StmtSeq ext b r c -> f (StmtSeq ext b r c)) -> Block ext b r c -> f (Block ext b r c)
withBlockTermStmt :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (args :: Ctx CrucibleType) r. Block ext blocks ret args -> (forall (ctx :: Ctx CrucibleType). ProgramLoc -> TermStmt blocks ret ctx -> r) -> r
nextBlocks :: forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType) (a :: Ctx CrucibleType). Block ext b r a -> [Some (BlockID b)]
data JumpTarget (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) where
- JumpTarget :: forall (blocks :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType) (ctx :: Ctx CrucibleType). !(BlockID blocks args) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> JumpTarget blocks ctx
extendJumpTarget :: forall (blocks' :: Ctx (Ctx CrucibleType)) (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType). Diff blocks' blocks -> JumpTarget blocks' ctx -> JumpTarget blocks ctx
jumpTargetID :: forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType). JumpTarget blocks ctx -> Some (BlockID blocks)
data SwitchTarget (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) (tp :: CrucibleType) where
- SwitchTarget :: forall (blocks :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType) (tp :: CrucibleType) (ctx :: Ctx CrucibleType). !(BlockID blocks (args ::> tp)) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> SwitchTarget blocks ctx tp
switchTargetID :: forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) (tp :: CrucibleType). SwitchTarget blocks ctx tp -> Some (BlockID blocks)
extendSwitchTarget :: forall (blocks' :: Ctx (Ctx CrucibleType)) (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) (tp :: CrucibleType). Diff blocks' blocks -> SwitchTarget blocks' ctx tp -> SwitchTarget blocks ctx tp
data StmtSeq ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) where
- ConsStmt :: forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType). !ProgramLoc -> !(Stmt ext ctx ctx') -> !(StmtSeq ext blocks ret ctx') -> StmtSeq ext blocks ret ctx
- TermStmt :: forall (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) ext. !ProgramLoc -> !(TermStmt blocks ret ctx) -> StmtSeq ext blocks ret ctx
firstStmtLoc :: forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType) (ctx :: Ctx CrucibleType). StmtSeq ext b r ctx -> ProgramLoc
stmtSeqTermStmt :: forall f (b :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ext (b' :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType). Functor f => (forall (ctx :: Ctx CrucibleType). (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 :: forall (tp :: CrucibleType) ext (ctx :: Ctx CrucibleType). !(TypeRepr tp) -> !(Expr ext ctx tp) -> Stmt ext ctx (ctx '::> tp)
- ExtendAssign :: forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType). !(StmtExtension ext (Reg ctx) tp) -> Stmt ext ctx (ctx '::> tp)
- CallHandle :: forall (ret :: CrucibleType) (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType) ext. !(TypeRepr ret) -> !(Reg ctx (FunctionHandleType args ret)) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> Stmt ext ctx (ctx '::> ret)
- Print :: forall (ctx :: Ctx CrucibleType) ext. !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
- ReadGlobal :: forall (tp :: CrucibleType) ext (ctx :: Ctx CrucibleType). !(GlobalVar tp) -> Stmt ext ctx (ctx '::> tp)
- WriteGlobal :: forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) ext. !(GlobalVar tp) -> !(Reg ctx tp) -> Stmt ext ctx ctx
- FreshConstant :: forall (bt :: BaseType) ext (ctx :: Ctx CrucibleType). !(BaseTypeRepr bt) -> !(Maybe SolverSymbol) -> Stmt ext ctx (ctx '::> BaseToType bt)
- FreshFloat :: forall (fi :: FloatInfo) ext (ctx :: Ctx CrucibleType). !(FloatInfoRepr fi) -> !(Maybe SolverSymbol) -> Stmt ext ctx (ctx '::> FloatType fi)
- FreshNat :: forall ext (ctx :: Ctx CrucibleType). !(Maybe SolverSymbol) -> Stmt ext ctx (ctx '::> NatType)
- NewRefCell :: forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) ext. !(TypeRepr tp) -> !(Reg ctx tp) -> Stmt ext ctx (ctx '::> ReferenceType tp)
- NewEmptyRefCell :: forall (tp :: CrucibleType) ext (ctx :: Ctx CrucibleType). !(TypeRepr tp) -> Stmt ext ctx (ctx '::> ReferenceType tp)
- ReadRefCell :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType) ext. !(Reg ctx (ReferenceType tp)) -> Stmt ext ctx (ctx '::> tp)
- WriteRefCell :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType) ext. !(Reg ctx (ReferenceType tp)) -> !(Reg ctx tp) -> Stmt ext ctx ctx
- DropRefCell :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType) ext. !(Reg ctx (ReferenceType tp)) -> Stmt ext ctx ctx
- Assert :: forall (ctx :: Ctx CrucibleType) ext. !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
- Assume :: forall (ctx :: Ctx CrucibleType) ext. !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
ppStmt :: forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) ann. PrettyExt ext => Size ctx -> Stmt ext ctx ctx' -> Doc ann
nextStmtHeight :: forall (ctx :: Ctx CrucibleType) ext (ctx' :: Ctx CrucibleType). Size ctx -> Stmt ext ctx ctx' -> Size ctx'
applyEmbeddingStmt :: forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) (sctx :: Ctx CrucibleType). TraverseExt ext => CtxEmbedding ctx ctx' -> Stmt ext ctx sctx -> Pair (Stmt ext ctx') (CtxEmbedding sctx)
data TermStmt (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) where
- Jump :: forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) (ret :: CrucibleType). !(JumpTarget blocks ctx) -> TermStmt blocks ret ctx
- Br :: forall (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType). !(Reg ctx BoolType) -> !(JumpTarget blocks ctx) -> !(JumpTarget blocks ctx) -> TermStmt blocks ret ctx
- MaybeBranch :: forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType). !(TypeRepr tp) -> !(Reg ctx (MaybeType tp)) -> !(SwitchTarget blocks ctx tp) -> !(JumpTarget blocks ctx) -> TermStmt blocks ret ctx
- VariantElim :: forall (varctx :: Ctx CrucibleType) (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType). !(CtxRepr varctx) -> !(Reg ctx (VariantType varctx)) -> !(Assignment (SwitchTarget blocks ctx) varctx) -> TermStmt blocks ret ctx
- Return :: forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)). !(Reg ctx ret) -> TermStmt blocks ret ctx
- TailCall :: forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType) (ret :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)). !(Reg ctx (FunctionHandleType args ret)) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> TermStmt blocks ret ctx
- ErrorStmt :: forall (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType). !(Reg ctx (StringType Unicode)) -> TermStmt blocks ret ctx
termStmtNextBlocks :: forall (b :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). 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 :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType) (r :: CrucibleType). Reg ctx tp -> Reg (ctx ::> r) tp
lastReg :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType). 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 (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 :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType). 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 :: k -> Type) ext (init :: Ctx CrucibleType) (ret :: CrucibleType) | f -> ext, f -> init, f -> ret where Source #

Class for types that embed a CFG of some sort.

Methods

getCFG :: forall (b :: k). 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 :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType). 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

:: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType) ann. 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

:: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType) ann. 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 :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext blocks init ret -> CtxRepr init Source #

cfgReturnType :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext blocks init ret -> TypeRepr ret Source #

type CFGPostdom (blocks :: Ctx (Ctx CrucibleType)) = Assignment (Const [Some (BlockID blocks)] :: Ctx CrucibleType -> Type) 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 :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) = Assignment (Block ext blocks ret) blocks Source #

A mapping from block indices to CFG blocks

getBlock :: forall (blocks :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType) ext (ret :: CrucibleType). BlockID blocks args -> BlockMap ext blocks ret -> Block ext blocks ret args Source #

extendBlockMap :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (b :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType). 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 :: Ctx CrucibleType) (b :: Ctx CrucibleType). 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 :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> OrderingF x y # leqF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> Bool # ltF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> Bool # geqF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> Bool # gtF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). 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 :: Ctx CrucibleType) a. p (BlockID blocks) -> q tp -> (Show (BlockID blocks tp) => a) -> a # showF :: forall (tp :: Ctx CrucibleType). BlockID blocks tp -> String # showsPrecF :: forall (tp :: Ctx CrucibleType). 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 :: forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType). KnownDiff l r => BlockID l tp -> BlockID r tp Source #

extendBlockID' :: forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType). Diff l r -> BlockID l tp -> BlockID r tp Source #

data Block ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) 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 :: Ctx CrucibleType) a. p (Block ext blocks ret) -> q tp -> (Show (Block ext blocks ret tp) => a) -> a # showF :: forall (tp :: Ctx CrucibleType). Block ext blocks ret tp -> String # showsPrecF :: forall (tp :: Ctx CrucibleType). 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 :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). Block ext blocks ret ctx -> ProgramLoc Source #

Return location of start of block.

blockStmts :: forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType) (c :: Ctx CrucibleType) f. Functor f => (StmtSeq ext b r c -> f (StmtSeq ext b r c)) -> Block ext b r c -> f (Block ext b r c) Source #

withBlockTermStmt :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (args :: Ctx CrucibleType) r. Block ext blocks ret args -> (forall (ctx :: Ctx CrucibleType). 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 :: forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType) (a :: Ctx CrucibleType). Block ext b r a -> [Some (BlockID b)] Source #

Jump targets

data JumpTarget (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) where Source #

Target for jump and branch statements

Constructors

JumpTarget :: forall (blocks :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType) (ctx :: Ctx CrucibleType). !(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 CrucibleType) (ctx' :: Ctx CrucibleType). 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 CrucibleType) (ctx' :: Ctx CrucibleType). 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 :: forall (blocks' :: Ctx (Ctx CrucibleType)) (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType). Diff blocks' blocks -> JumpTarget blocks' ctx -> JumpTarget blocks ctx Source #

jumpTargetID :: forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType). JumpTarget blocks ctx -> Some (BlockID blocks) Source #

data SwitchTarget (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) (tp :: CrucibleType) where Source #

Target for a switch statement.

Constructors

SwitchTarget :: forall (blocks :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType) (tp :: CrucibleType) (ctx :: Ctx CrucibleType). !(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 CrucibleType) (ctx' :: Ctx CrucibleType) (v :: CrucibleType). 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 CrucibleType) (ctx' :: Ctx CrucibleType) (v :: CrucibleType). Diff ctx ctx' -> SwitchTarget blocks ctx v -> SwitchTarget blocks ctx' v #

switchTargetID :: forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) (tp :: CrucibleType). SwitchTarget blocks ctx tp -> Some (BlockID blocks) Source #

extendSwitchTarget :: forall (blocks' :: Ctx (Ctx CrucibleType)) (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) (tp :: CrucibleType). Diff blocks' blocks -> SwitchTarget blocks' ctx tp -> SwitchTarget blocks ctx tp Source #

Statements

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

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

Constructors

ConsStmt :: forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType). !ProgramLoc -> !(Stmt ext ctx ctx') -> !(StmtSeq ext blocks ret ctx') -> StmtSeq ext blocks ret ctx
TermStmt :: forall (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType) ext. !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 CrucibleType) (ctx' :: Ctx CrucibleType). CtxEmbedding ctx ctx' -> StmtSeq ext blocks ret ctx -> StmtSeq ext blocks ret ctx' #

firstStmtLoc :: forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType) (ctx :: Ctx CrucibleType). StmtSeq ext b r ctx -> ProgramLoc Source #

Return the location of a statement.

stmtSeqTermStmt :: forall f (b :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ext (b' :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType). Functor f => (forall (ctx :: Ctx CrucibleType). (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 :: forall (tp :: CrucibleType) ext (ctx :: Ctx CrucibleType). !(TypeRepr tp) -> !(Expr ext ctx tp) -> Stmt ext ctx (ctx '::> tp)
ExtendAssign :: forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType). !(StmtExtension ext (Reg ctx) tp) -> Stmt ext ctx (ctx '::> tp)
CallHandle :: forall (ret :: CrucibleType) (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType) ext. !(TypeRepr ret) -> !(Reg ctx (FunctionHandleType args ret)) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> Stmt ext ctx (ctx '::> ret)
Print :: forall (ctx :: Ctx CrucibleType) ext. !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
ReadGlobal :: forall (tp :: CrucibleType) ext (ctx :: Ctx CrucibleType). !(GlobalVar tp) -> Stmt ext ctx (ctx '::> tp)
WriteGlobal :: forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) ext. !(GlobalVar tp) -> !(Reg ctx tp) -> Stmt ext ctx ctx
FreshConstant :: forall (bt :: BaseType) ext (ctx :: Ctx CrucibleType). !(BaseTypeRepr bt) -> !(Maybe SolverSymbol) -> Stmt ext ctx (ctx '::> BaseToType bt)
FreshFloat :: forall (fi :: FloatInfo) ext (ctx :: Ctx CrucibleType). !(FloatInfoRepr fi) -> !(Maybe SolverSymbol) -> Stmt ext ctx (ctx '::> FloatType fi)
FreshNat :: forall ext (ctx :: Ctx CrucibleType). !(Maybe SolverSymbol) -> Stmt ext ctx (ctx '::> NatType)
NewRefCell :: forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) ext. !(TypeRepr tp) -> !(Reg ctx tp) -> Stmt ext ctx (ctx '::> ReferenceType tp)
NewEmptyRefCell :: forall (tp :: CrucibleType) ext (ctx :: Ctx CrucibleType). !(TypeRepr tp) -> Stmt ext ctx (ctx '::> ReferenceType tp)
ReadRefCell :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType) ext. !(Reg ctx (ReferenceType tp)) -> Stmt ext ctx (ctx '::> tp)
WriteRefCell :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType) ext. !(Reg ctx (ReferenceType tp)) -> !(Reg ctx tp) -> Stmt ext ctx ctx
DropRefCell :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType) ext. !(Reg ctx (ReferenceType tp)) -> Stmt ext ctx ctx
Assert :: forall (ctx :: Ctx CrucibleType) ext. !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
Assume :: forall (ctx :: Ctx CrucibleType) ext. !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx

ppStmt :: forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) ann. PrettyExt ext => Size ctx -> Stmt ext ctx ctx' -> Doc ann Source #

nextStmtHeight :: forall (ctx :: Ctx CrucibleType) ext (ctx' :: Ctx CrucibleType). Size ctx -> Stmt ext ctx ctx' -> Size ctx' Source #

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

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

Constructors

Jump :: forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) (ret :: CrucibleType). !(JumpTarget blocks ctx) -> TermStmt blocks ret ctx
Br :: forall (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType). !(Reg ctx BoolType) -> !(JumpTarget blocks ctx) -> !(JumpTarget blocks ctx) -> TermStmt blocks ret ctx
MaybeBranch :: forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType). !(TypeRepr tp) -> !(Reg ctx (MaybeType tp)) -> !(SwitchTarget blocks ctx tp) -> !(JumpTarget blocks ctx) -> TermStmt blocks ret ctx
VariantElim :: forall (varctx :: Ctx CrucibleType) (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType). !(CtxRepr varctx) -> !(Reg ctx (VariantType varctx)) -> !(Assignment (SwitchTarget blocks ctx) varctx) -> TermStmt blocks ret ctx
Return :: forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)). !(Reg ctx ret) -> TermStmt blocks ret ctx
TailCall :: forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType) (ret :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)). !(Reg ctx (FunctionHandleType args ret)) -> !(CtxRepr args) -> !(Assignment (Reg ctx) args) -> TermStmt blocks ret ctx
ErrorStmt :: forall (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType). !(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 CrucibleType) (ctx' :: Ctx CrucibleType). 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 CrucibleType) (ctx' :: Ctx CrucibleType). 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 :: forall (b :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). 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 CrucibleType) (ctx' :: Ctx CrucibleType) (v :: CrucibleType). 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 CrucibleType) (ctx' :: Ctx CrucibleType) (v :: CrucibleType). 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 CrucibleType) (ctx' :: Ctx CrucibleType) (v :: CrucibleType). 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 CrucibleType) (ctx' :: Ctx CrucibleType) (v :: CrucibleType). 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 :: CrucibleType) (b :: CrucibleType). 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 :: CrucibleType) (y :: CrucibleType). Reg ctx x -> Reg ctx y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg ctx x -> Reg ctx y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg ctx x -> Reg ctx y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg ctx x -> Reg ctx y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). 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 :: CrucibleType) a. p (Reg ctx) -> q tp -> (Show (Reg ctx tp) => a) -> a # showF :: forall (tp :: CrucibleType). Reg ctx tp -> String # showsPrecF :: forall (tp :: CrucibleType). 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 :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType) (r :: CrucibleType). 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 :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType). 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