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

Lang.Crucible.CFG.Reg

Contents

CFG
Atoms
Values
Blocks
Statements
Expressions
Re-exports

Description

This module defines CFGs that feature mutable registers, in contrast to the Core CFGs (Lang.Crucible.CFG.Core), which are in SSA form. Register CFGs can be translated into SSA CFGs using the Lang.Crucible.CFG.SSAConversion module.

Module Lang.Crucible.CFG.Generator provides a high-level monadic interface for producing register CFGs.

Synopsis

data CFG ext s (init :: Ctx CrucibleType) (ret :: CrucibleType) = CFG {
- cfgHandle :: !(FnHandle init ret)
- cfgEntryLabel :: !(Label s)
- cfgBlocks :: ![Block ext s ret]
}
cfgEntryBlock :: CFG ext s init ret -> Block ext s ret
cfgInputTypes :: CFG ext s init ret -> CtxRepr init
cfgArgTypes :: CFG ext s init ret -> CtxRepr init
cfgReturnType :: CFG ext s init ret -> TypeRepr ret
substCFG :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> CFG ext s init ret -> m (CFG ext s' init ret)
data SomeCFG ext init ret = forall s. SomeCFG !(CFG ext s init ret)
data AnyCFG ext where
- AnyCFG :: CFG ext blocks init ret -> AnyCFG ext
newtype Label s = Label {
- labelId :: Nonce s UnitType
}
substLabel :: Functor m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Label s -> m (Label s')
data LambdaLabel (s :: Type) (tp :: CrucibleType) = LambdaLabel {
- lambdaId :: !(Nonce s tp)
- lambdaAtom :: Atom s tp
}
substLambdaLabel :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> LambdaLabel s tp -> m (LambdaLabel s' tp)
data BlockID (s :: Type) where
- LabelID :: Label s -> BlockID s
- LambdaID :: LambdaLabel s tp -> BlockID s
substBlockID :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> BlockID s -> m (BlockID s')
data Reg s (tp :: CrucibleType) = Reg {
- regPosition :: !Position
- regId :: !(Nonce s tp)
- typeOfReg :: !(TypeRepr tp)
}
substReg :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Reg s tp -> m (Reg s' tp)
traverseCFG :: (Monad m, TraverseExt ext) => (genv -> penv -> Block ext s ret -> m (genv, penv)) -> genv -> penv -> Block ext s ret -> CFG ext s init ret -> m genv
data Atom s (tp :: CrucibleType) = Atom {
- atomPosition :: !Position
- atomId :: !(Nonce s tp)
- atomSource :: !(AtomSource s tp)
- typeOfAtom :: !(TypeRepr tp)
}
substAtom :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Atom s tp -> m (Atom s' tp)
data AtomSource s (tp :: CrucibleType)
- = Assigned
- | FnInput
- | LambdaArg !(LambdaLabel s tp)
substAtomSource :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> AtomSource s tp -> m (AtomSource s' tp)
mkInputAtoms :: forall m s init. Monad m => NonceGenerator m s -> Position -> CtxRepr init -> m (Assignment (Atom s) init)
data AtomValue ext s (tp :: CrucibleType) where
- EvalApp :: !(App ext (Atom s) tp) -> AtomValue ext s tp
- ReadReg :: !(Reg s tp) -> AtomValue ext s tp
- EvalExt :: !(StmtExtension ext (Atom s) tp) -> AtomValue ext s tp
- ReadGlobal :: !(GlobalVar tp) -> AtomValue ext s tp
- ReadRef :: !(Atom s (ReferenceType tp)) -> AtomValue ext s tp
- NewRef :: !(Atom s tp) -> AtomValue ext s (ReferenceType tp)
- NewEmptyRef :: !(TypeRepr tp) -> AtomValue ext s (ReferenceType tp)
- FreshConstant :: !(BaseTypeRepr bt) -> !(Maybe SolverSymbol) -> AtomValue ext s (BaseToType bt)
- FreshFloat :: !(FloatInfoRepr fi) -> !(Maybe SolverSymbol) -> AtomValue ext s (FloatType fi)
- FreshNat :: !(Maybe SolverSymbol) -> AtomValue ext s NatType
- Call :: !(Atom s (FunctionHandleType args ret)) -> !(Assignment (Atom s) args) -> !(TypeRepr ret) -> AtomValue ext s ret
typeOfAtomValue :: (TypeApp (StmtExtension ext), TypeApp (ExprExtension ext)) => AtomValue ext s tp -> TypeRepr tp
substAtomValue :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> AtomValue ext s tp -> m (AtomValue ext s' tp)
data Value s (tp :: CrucibleType)
- = RegValue !(Reg s tp)
- | AtomValue !(Atom s tp)
typeOfValue :: Value s tp -> TypeRepr tp
substValue :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Value s tp -> m (Value s' tp)
type ValueSet s = Set (Some (Value s))
substValueSet :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> ValueSet s -> m (ValueSet s')
data Block ext s (ret :: CrucibleType)
mkBlock :: forall ext s ret. TraverseExt ext => BlockID s -> ValueSet s -> Seq (Posd (Stmt ext s)) -> Posd (TermStmt s ret) -> Block ext s ret
blockID :: Block ext s ret -> BlockID s
blockStmts :: Block ext s ret -> Seq (Posd (Stmt ext s))
blockTerm :: Block ext s ret -> Posd (TermStmt s ret)
blockExtraInputs :: Block ext s ret -> ValueSet s
blockKnownInputs :: Block ext s ret -> ValueSet s
blockAssignedValues :: Block ext s ret -> ValueSet s
substBlock :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Block ext s ret -> m (Block ext s' ret)
data Stmt ext s
- = forall tp. SetReg !(Reg s tp) !(Atom s tp)
- | forall tp. WriteGlobal !(GlobalVar tp) !(Atom s tp)
- | forall tp. WriteRef !(Atom s (ReferenceType tp)) !(Atom s tp)
- | forall tp. DropRef !(Atom s (ReferenceType tp))
- | forall tp. DefineAtom !(Atom s tp) !(AtomValue ext s tp)
- | Print !(Atom s (StringType Unicode))
- | Assert !(Atom s BoolType) !(Atom s (StringType Unicode))
- | Assume !(Atom s BoolType) !(Atom s (StringType Unicode))
- | forall args. Breakpoint BreakpointName !(Assignment (Value s) args)
substStmt :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Stmt ext s -> m (Stmt ext s')
substPosdStmt :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Posd (Stmt ext s) -> m (Posd (Stmt ext s'))
mapStmtAtom :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Atom s x -> m (Atom s x)) -> Stmt ext s -> m (Stmt ext s)
data TermStmt s (ret :: CrucibleType) where
- Jump :: !(Label s) -> TermStmt s ret
- Br :: !(Atom s BoolType) -> !(Label s) -> !(Label s) -> TermStmt s ret
- MaybeBranch :: !(TypeRepr tp) -> !(Atom s (MaybeType tp)) -> !(LambdaLabel s tp) -> !(Label s) -> TermStmt s ret
- VariantElim :: !(CtxRepr varctx) -> !(Atom s (VariantType varctx)) -> !(Assignment (LambdaLabel s) varctx) -> TermStmt s ret
- Return :: !(Atom s ret) -> TermStmt s ret
- TailCall :: !(Atom s (FunctionHandleType args ret)) -> !(CtxRepr args) -> !(Assignment (Atom s) args) -> TermStmt s ret
- ErrorStmt :: !(Atom s (StringType Unicode)) -> TermStmt s ret
- Output :: !(LambdaLabel s tp) -> !(Atom s tp) -> TermStmt s ret
termStmtInputs :: TermStmt s ret -> ValueSet s
termNextLabels :: TermStmt s ret -> Maybe [BlockID s]
substTermStmt :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> TermStmt s ret -> m (TermStmt s' ret)
substPosdTermStmt :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Posd (TermStmt s ret) -> m (Posd (TermStmt s' ret))
foldStmtInputs :: TraverseExt ext => (forall x. Value s x -> b -> b) -> Stmt ext s -> b -> b
data Expr ext s (tp :: CrucibleType)
- = App !(App ext (Expr ext s) tp)
- | AtomExpr !(Atom s tp)
exprType :: IsExpr e => e tp -> TypeRepr tp
substExpr :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Expr ext s tp -> m (Expr ext s' tp)
module Lang.Crucible.CFG.Common

CFG

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

A CFG using registers instead of SSA form.

Parameter ext is the syntax extension, s is a phantom type parameter identifying a particular CFG, init is the list of input types of the CFG, and ret is the return type.

Constructors

CFG
Fields cfgHandle :: !(FnHandle init ret) cfgEntryLabel :: !(Label s) cfgBlocks :: ![Block ext s ret]

Instances

Instances details

PrettyExt ext => Show (CFG ext s init ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> CFG ext s init ret -> ShowS # show :: CFG ext s init ret -> String # showList :: [CFG ext s init ret] -> ShowS #
PrettyExt ext => Pretty (CFG ext s init ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: CFG ext s init ret -> Doc ann # prettyList :: [CFG ext s init ret] -> Doc ann #

cfgEntryBlock :: CFG ext s init ret -> Block ext s ret Source #

cfgInputTypes :: CFG ext s init ret -> CtxRepr init Source #

Deprecated: Use cfgArgTypes instead

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

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

substCFG :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> CFG ext s init ret -> m (CFG ext s' init ret) Source #

Rename all the atoms, labels, and other named things in the CFG. Useful for rewriting, since the names can be generated from a nonce generator the client controls (and can thus keep using to generate fresh names).

data SomeCFG ext init ret Source #

SomeCFG is a CFG with an arbitrary parameter s.

Constructors

forall s. SomeCFG !(CFG ext s init ret)

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.Reg Methods showsPrec :: Int -> AnyCFG ext -> ShowS # show :: AnyCFG ext -> String # showList :: [AnyCFG ext] -> ShowS #

newtype Label s Source #

A label for a block that does not expect an input.

Constructors

Label
Fields labelId :: Nonce s UnitType

Instances

Instances details

Show (Label s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> Label s -> ShowS # show :: Label s -> String # showList :: [Label s] -> ShowS #
Eq (Label s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods (==) :: Label s -> Label s -> Bool # (/=) :: Label s -> Label s -> Bool #
Ord (Label s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compare :: Label s -> Label s -> Ordering # (<) :: Label s -> Label s -> Bool # (<=) :: Label s -> Label s -> Bool # (>) :: Label s -> Label s -> Bool # (>=) :: Label s -> Label s -> Bool # max :: Label s -> Label s -> Label s # min :: Label s -> Label s -> Label s #
Pretty (Label s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: Label s -> Doc ann # prettyList :: [Label s] -> Doc ann #

substLabel :: Functor m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Label s -> m (Label s') Source #

data LambdaLabel (s :: Type) (tp :: CrucibleType) Source #

A label for a block that expects an argument of a specific type.

Constructors

LambdaLabel
Fields lambdaId :: !(Nonce s tp) Nonce that uniquely identifies this label within the CFG. lambdaAtom :: Atom s tp The atom to store the output result in. Note. This must be lazy to break a recursive cycle.

Instances

Instances details

TestEquality (LambdaLabel s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods testEquality :: forall (a :: k) (b :: k). LambdaLabel s a -> LambdaLabel s b -> Maybe (a :~: b) #
OrdF (LambdaLabel s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compareF :: forall (x :: k) (y :: k). LambdaLabel s x -> LambdaLabel s y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). LambdaLabel s x -> LambdaLabel s y -> Bool # ltF :: forall (x :: k) (y :: k). LambdaLabel s x -> LambdaLabel s y -> Bool # geqF :: forall (x :: k) (y :: k). LambdaLabel s x -> LambdaLabel s y -> Bool # gtF :: forall (x :: k) (y :: k). LambdaLabel s x -> LambdaLabel s y -> Bool #
Show (LambdaLabel s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> LambdaLabel s tp -> ShowS # show :: LambdaLabel s tp -> String # showList :: [LambdaLabel s tp] -> ShowS #
Pretty (LambdaLabel s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: LambdaLabel s tp -> Doc ann # prettyList :: [LambdaLabel s tp] -> Doc ann #

substLambdaLabel :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> LambdaLabel s tp -> m (LambdaLabel s' tp) Source #

data BlockID (s :: Type) where Source #

A label for a block is either a standard label, or a label expecting an input.

Constructors

LabelID :: Label s -> BlockID s
LambdaID :: LambdaLabel s tp -> BlockID s

Instances

Instances details

Show (BlockID s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> BlockID s -> ShowS # show :: BlockID s -> String # showList :: [BlockID s] -> ShowS #
Eq (BlockID s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods (==) :: BlockID s -> BlockID s -> Bool # (/=) :: BlockID s -> BlockID s -> Bool #
Ord (BlockID s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compare :: BlockID s -> BlockID s -> Ordering # (<) :: BlockID s -> BlockID s -> Bool # (<=) :: BlockID s -> BlockID s -> Bool # (>) :: BlockID s -> BlockID s -> Bool # (>=) :: BlockID s -> BlockID s -> Bool # max :: BlockID s -> BlockID s -> BlockID s # min :: BlockID s -> BlockID s -> BlockID s #

substBlockID :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> BlockID s -> m (BlockID s') Source #

data Reg s (tp :: CrucibleType) Source #

A mutable value in the control flow graph.

Constructors

Reg
Fields regPosition :: !Position Position where register was declared (used for debugging). regId :: !(Nonce s tp) Unique identifier for register. typeOfReg :: !(TypeRepr tp) Type of register.

Instances

Instances details

TestEquality (Reg s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods testEquality :: forall (a :: k) (b :: k). Reg s a -> Reg s b -> Maybe (a :~: b) #
OrdF (Reg s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compareF :: forall (x :: k) (y :: k). Reg s x -> Reg s y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). Reg s x -> Reg s y -> Bool # ltF :: forall (x :: k) (y :: k). Reg s x -> Reg s y -> Bool # geqF :: forall (x :: k) (y :: k). Reg s x -> Reg s y -> Bool # gtF :: forall (x :: k) (y :: k). Reg s x -> Reg s y -> Bool #
ShowF (Reg s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods withShow :: forall p q (tp :: k) a. p (Reg s) -> q tp -> (Show (Reg s tp) => a) -> a # showF :: forall (tp :: k). Reg s tp -> String # showsPrecF :: forall (tp :: k). Int -> Reg s tp -> String -> String #
Show (Reg s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> Reg s tp -> ShowS # show :: Reg s tp -> String # showList :: [Reg s tp] -> ShowS #
Pretty (Reg s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: Reg s tp -> Doc ann # prettyList :: [Reg s tp] -> Doc ann #

substReg :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Reg s tp -> m (Reg s' tp) Source #

traverseCFG :: (Monad m, TraverseExt ext) => (genv -> penv -> Block ext s ret -> m (genv, penv)) -> genv -> penv -> Block ext s ret -> CFG ext s init ret -> m genv Source #

Run a computation along all of the paths in a cfg, without taking backedges.

The computation has access to an environment that is specific to the current path being explored, as well as a global environment that is maintained across the entire computation.

Atoms

data Atom s (tp :: CrucibleType) Source #

An expression in the control flow graph with a unique identifier. Unlike registers, atoms must be assigned exactly once.

Constructors

Atom
Fields atomPosition :: !Position Position where register was declared (used for debugging). atomId :: !(Nonce s tp) Unique identifier for atom. atomSource :: !(AtomSource s tp) How the atom expression was defined. typeOfAtom :: !(TypeRepr tp)

Instances

Instances details

TestEquality (Atom s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods testEquality :: forall (a :: k) (b :: k). Atom s a -> Atom s b -> Maybe (a :~: b) #
OrdF (Atom s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compareF :: forall (x :: k) (y :: k). Atom s x -> Atom s y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). Atom s x -> Atom s y -> Bool # ltF :: forall (x :: k) (y :: k). Atom s x -> Atom s y -> Bool # geqF :: forall (x :: k) (y :: k). Atom s x -> Atom s y -> Bool # gtF :: forall (x :: k) (y :: k). Atom s x -> Atom s y -> Bool #
Show (Atom s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> Atom s tp -> ShowS # show :: Atom s tp -> String # showList :: [Atom s tp] -> ShowS #
Pretty (Atom s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: Atom s tp -> Doc ann # prettyList :: [Atom s tp] -> Doc ann #

substAtom :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Atom s tp -> m (Atom s' tp) Source #

data AtomSource s (tp :: CrucibleType) Source #

Identifies what generated an atom.

Constructors

Assigned
FnInput	Input argument to function. They are ordered before other inputs to a program.
LambdaArg !(LambdaLabel s tp)	Value passed into a lambda label. This must appear after other expressions.

substAtomSource :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> AtomSource s tp -> m (AtomSource s' tp) Source #

mkInputAtoms :: forall m s init. Monad m => NonceGenerator m s -> Position -> CtxRepr init -> m (Assignment (Atom s) init) Source #

data AtomValue ext s (tp :: CrucibleType) where Source #

The value of an assigned atom.

Constructors

EvalApp :: !(App ext (Atom s) tp) -> AtomValue ext s tp
ReadReg :: !(Reg s tp) -> AtomValue ext s tp
EvalExt :: !(StmtExtension ext (Atom s) tp) -> AtomValue ext s tp
ReadGlobal :: !(GlobalVar tp) -> AtomValue ext s tp
ReadRef :: !(Atom s (ReferenceType tp)) -> AtomValue ext s tp
NewRef :: !(Atom s tp) -> AtomValue ext s (ReferenceType tp)
NewEmptyRef :: !(TypeRepr tp) -> AtomValue ext s (ReferenceType tp)
FreshConstant :: !(BaseTypeRepr bt) -> !(Maybe SolverSymbol) -> AtomValue ext s (BaseToType bt)
FreshFloat :: !(FloatInfoRepr fi) -> !(Maybe SolverSymbol) -> AtomValue ext s (FloatType fi)
FreshNat :: !(Maybe SolverSymbol) -> AtomValue ext s NatType
Call :: !(Atom s (FunctionHandleType args ret)) -> !(Assignment (Atom s) args) -> !(TypeRepr ret) -> AtomValue ext s ret

Instances

Instances details

PrettyExt ext => Show (AtomValue ext s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> AtomValue ext s tp -> ShowS # show :: AtomValue ext s tp -> String # showList :: [AtomValue ext s tp] -> ShowS #
PrettyExt ext => Pretty (AtomValue ext s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: AtomValue ext s tp -> Doc ann # prettyList :: [AtomValue ext s tp] -> Doc ann #

typeOfAtomValue :: (TypeApp (StmtExtension ext), TypeApp (ExprExtension ext)) => AtomValue ext s tp -> TypeRepr tp Source #

substAtomValue :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> AtomValue ext s tp -> m (AtomValue ext s' tp) Source #

Values

data Value s (tp :: CrucibleType) Source #

A value is either a register or an atom.

Constructors

RegValue !(Reg s tp)
AtomValue !(Atom s tp)

Instances

Instances details

TestEquality (Value s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods testEquality :: forall (a :: k) (b :: k). Value s a -> Value s b -> Maybe (a :~: b) #
OrdF (Value s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compareF :: forall (x :: k) (y :: k). Value s x -> Value s y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). Value s x -> Value s y -> Bool # ltF :: forall (x :: k) (y :: k). Value s x -> Value s y -> Bool # geqF :: forall (x :: k) (y :: k). Value s x -> Value s y -> Bool # gtF :: forall (x :: k) (y :: k). Value s x -> Value s y -> Bool #
ShowF (Value s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods withShow :: forall p q (tp :: k) a. p (Value s) -> q tp -> (Show (Value s tp) => a) -> a # showF :: forall (tp :: k). Value s tp -> String # showsPrecF :: forall (tp :: k). Int -> Value s tp -> String -> String #
Pretty (ValueSet s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: ValueSet s -> Doc ann # prettyList :: [ValueSet s] -> Doc ann #
Show (Value s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> Value s tp -> ShowS # show :: Value s tp -> String # showList :: [Value s tp] -> ShowS #
Pretty (Value s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: Value s tp -> Doc ann # prettyList :: [Value s tp] -> Doc ann #

typeOfValue :: Value s tp -> TypeRepr tp Source #

substValue :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Value s tp -> m (Value s' tp) Source #

type ValueSet s = Set (Some (Value s)) Source #

A set of values.

substValueSet :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> ValueSet s -> m (ValueSet s') Source #

Blocks

data Block ext s (ret :: CrucibleType) Source #

A basic block within a function.

Instances

Instances details

PrettyExt ext => Show (Block ext s ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> Block ext s ret -> ShowS # show :: Block ext s ret -> String # showList :: [Block ext s ret] -> ShowS #
Eq (Block ext s ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods (==) :: Block ext s ret -> Block ext s ret -> Bool # (/=) :: Block ext s ret -> Block ext s ret -> Bool #
Ord (Block ext s ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compare :: Block ext s ret -> Block ext s ret -> Ordering # (<) :: Block ext s ret -> Block ext s ret -> Bool # (<=) :: Block ext s ret -> Block ext s ret -> Bool # (>) :: Block ext s ret -> Block ext s ret -> Bool # (>=) :: Block ext s ret -> Block ext s ret -> Bool # max :: Block ext s ret -> Block ext s ret -> Block ext s ret # min :: Block ext s ret -> Block ext s ret -> Block ext s ret #
PrettyExt ext => Pretty (Block ext s ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: Block ext s ret -> Doc ann # prettyList :: [Block ext s ret] -> Doc ann #

mkBlock Source #

Arguments

:: forall ext s ret. TraverseExt ext
=> BlockID s
-> ValueSet s	Extra inputs to block (only non-empty for initial block)
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> Block ext s ret

blockID :: Block ext s ret -> BlockID s Source #

blockStmts :: Block ext s ret -> Seq (Posd (Stmt ext s)) Source #

blockTerm :: Block ext s ret -> Posd (TermStmt s ret) Source #

blockExtraInputs :: Block ext s ret -> ValueSet s Source #

blockKnownInputs :: Block ext s ret -> ValueSet s Source #

Registers that are known to be needed as inputs for this block. For the first block, this includes the function arguments. It also includes registers read by this block before they are assigned. It does not include the lambda reg for lambda blocks.

blockAssignedValues :: Block ext s ret -> ValueSet s Source #

Registers assigned by statements in block. This is a field so that its value can be memoized.

substBlock :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Block ext s ret -> m (Block ext s' ret) Source #

Statements

data Stmt ext s Source #

Statement in control flow graph.

Constructors

forall tp. SetReg !(Reg s tp) !(Atom s tp)
forall tp. WriteGlobal !(GlobalVar tp) !(Atom s tp)
forall tp. WriteRef !(Atom s (ReferenceType tp)) !(Atom s tp)
forall tp. DropRef !(Atom s (ReferenceType tp))
forall tp. DefineAtom !(Atom s tp) !(AtomValue ext s tp)
Print !(Atom s (StringType Unicode))
Assert !(Atom s BoolType) !(Atom s (StringType Unicode))	Assert that the given expression is true.
Assume !(Atom s BoolType) !(Atom s (StringType Unicode))	Assume the given expression.
forall args. Breakpoint BreakpointName !(Assignment (Value s) args)

Instances

Instances details

PrettyExt ext => Show (Stmt ext s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> Stmt ext s -> ShowS # show :: Stmt ext s -> String # showList :: [Stmt ext s] -> ShowS #
PrettyExt ext => Pretty (Stmt ext s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: Stmt ext s -> Doc ann # prettyList :: [Stmt ext s] -> Doc ann #

substStmt :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Stmt ext s -> m (Stmt ext s') Source #

substPosdStmt :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Posd (Stmt ext s) -> m (Posd (Stmt ext s')) Source #

mapStmtAtom :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Atom s x -> m (Atom s x)) -> Stmt ext s -> m (Stmt ext s) Source #

data TermStmt s (ret :: CrucibleType) where Source #

Statement that terminates a basic block in a control flow graph.

Constructors

Jump :: !(Label s) -> TermStmt s ret
Br :: !(Atom s BoolType) -> !(Label s) -> !(Label s) -> TermStmt s ret
MaybeBranch :: !(TypeRepr tp) -> !(Atom s (MaybeType tp)) -> !(LambdaLabel s tp) -> !(Label s) -> TermStmt s ret
VariantElim :: !(CtxRepr varctx) -> !(Atom s (VariantType varctx)) -> !(Assignment (LambdaLabel s) varctx) -> TermStmt s ret
Return :: !(Atom s ret) -> TermStmt s ret
TailCall :: !(Atom s (FunctionHandleType args ret)) -> !(CtxRepr args) -> !(Assignment (Atom s) args) -> TermStmt s ret
ErrorStmt :: !(Atom s (StringType Unicode)) -> TermStmt s ret
Output :: !(LambdaLabel s tp) -> !(Atom s tp) -> TermStmt s ret

Instances

Instances details

Show (TermStmt s ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> TermStmt s ret -> ShowS # show :: TermStmt s ret -> String # showList :: [TermStmt s ret] -> ShowS #
Pretty (TermStmt s ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: TermStmt s ret -> Doc ann # prettyList :: [TermStmt s ret] -> Doc ann #

termStmtInputs :: TermStmt s ret -> ValueSet s Source #

Returns the set of registers appearing as inputs to a terminal statement.

termNextLabels :: TermStmt s ret -> Maybe [BlockID s] Source #

Returns the next labels for the given block. Error statements have no next labels, while return/tail call statements return Nothing.

substTermStmt :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> TermStmt s ret -> m (TermStmt s' ret) Source #

substPosdTermStmt :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Posd (TermStmt s ret) -> m (Posd (TermStmt s' ret)) Source #

foldStmtInputs :: TraverseExt ext => (forall x. Value s x -> b -> b) -> Stmt ext s -> b -> b Source #

Fold all registers that are inputs tostmt.

Expressions

data Expr ext s (tp :: CrucibleType) Source #

An expression in RTL representation.

The type arguments are:

ext: the extensions currently in use (use () for no extension)
s: a dummy variable that should almost always be universally quantified
tp: the Crucible type of the expression

Constructors

App !(App ext (Expr ext s) tp)	An application of an expression
AtomExpr !(Atom s tp)	An evaluated expession

Instances

Instances details

PrettyExt ext => ShowF (Expr ext s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods withShow :: forall p q (tp :: k) a. p (Expr ext s) -> q tp -> (Show (Expr ext s tp) => a) -> a # showF :: forall (tp :: k). Expr ext s tp -> String # showsPrecF :: forall (tp :: k). Int -> Expr ext s tp -> String -> String #
TypeApp (ExprExtension ext) => IsExpr (Expr ext s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Associated Types type ExprExt (Expr ext s) Source # Methods app :: forall (tp :: CrucibleType). App (ExprExt (Expr ext s)) (Expr ext s) tp -> Expr ext s tp Source # asApp :: forall (tp :: CrucibleType). Expr ext s tp -> Maybe (App (ExprExt (Expr ext s)) (Expr ext s) tp) Source # exprType :: forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp Source #
IsString (Expr ext s (StringType Unicode)) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods fromString :: String -> Expr ext s (StringType Unicode) #
PrettyExt ext => Show (Expr ext s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> Expr ext s tp -> ShowS # show :: Expr ext s tp -> String # showList :: [Expr ext s tp] -> ShowS #
PrettyExt ext => Pretty (Expr ext s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: Expr ext s tp -> Doc ann # prettyList :: [Expr ext s tp] -> Doc ann #
type ExprExt (Expr ext s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg type ExprExt (Expr ext s) = ext

exprType :: IsExpr e => e tp -> TypeRepr tp Source #

substExpr :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Expr ext s tp -> m (Expr ext s' tp) Source #

Re-exports

module Lang.Crucible.CFG.Common