Copyright | (c) Galois Inc 2014-2016 |
---|---|
License | BSD3 |
Maintainer | Joe Hendrix <jhendrix@galois.com> |
Stability | provisional |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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 {}
- 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
- newtype Label s = Label {}
- 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
- substBlockID :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> BlockID s -> m (BlockID s')
- data Reg s (tp :: CrucibleType) = Reg {}
- 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)
- 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)
- 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.
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 AnyCFG ext where Source #
Control flow graph. This data type closes existentially
over all the type parameters except ext
.
A label for a block that does not expect an input.
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.
LambdaLabel | |
|
Instances
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.
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.
Instances
TestEquality (Reg s :: CrucibleType -> Type) Source # | |
Defined in Lang.Crucible.CFG.Reg | |
OrdF (Reg s :: CrucibleType -> Type) Source # | |
Defined in Lang.Crucible.CFG.Reg 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 # | |
Show (Reg s tp) Source # | |
Pretty (Reg s tp) Source # | |
Defined in Lang.Crucible.CFG.Reg |
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.
Atom | |
|
Instances
TestEquality (Atom s :: CrucibleType -> Type) Source # | |
Defined in Lang.Crucible.CFG.Reg | |
OrdF (Atom s :: CrucibleType -> Type) Source # | |
Defined in Lang.Crucible.CFG.Reg 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 # | |
Pretty (Atom s tp) Source # | |
Defined in Lang.Crucible.CFG.Reg |
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.
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.
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 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.
Instances
TestEquality (Value s :: CrucibleType -> Type) Source # | |
Defined in Lang.Crucible.CFG.Reg | |
OrdF (Value s :: CrucibleType -> Type) Source # | |
Defined in Lang.Crucible.CFG.Reg 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 # | |
Pretty (ValueSet s) Source # | |
Defined in Lang.Crucible.CFG.Reg | |
Show (Value s tp) Source # | |
Pretty (Value s tp) Source # | |
Defined in Lang.Crucible.CFG.Reg |
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 #
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
PrettyExt ext => Show (Block ext s ret) Source # | |
Eq (Block ext s ret) Source # | |
Ord (Block ext s ret) Source # | |
Defined in Lang.Crucible.CFG.Reg 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 # | |
Defined in Lang.Crucible.CFG.Reg |
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
Statement in control flow graph.
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) |
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.
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 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
App !(App ext (Expr ext s) tp) | An application of an expression |
AtomExpr !(Atom s tp) | An evaluated expession |
Instances
PrettyExt ext => ShowF (Expr ext s :: CrucibleType -> Type) Source # | |
TypeApp (ExprExtension ext) => IsExpr (Expr ext s) Source # | |
Defined in Lang.Crucible.CFG.Reg | |
IsString (Expr ext s (StringType Unicode)) Source # | |
Defined in Lang.Crucible.CFG.Reg fromString :: String -> Expr ext s (StringType Unicode) # | |
PrettyExt ext => Show (Expr ext s tp) Source # | |
PrettyExt ext => Pretty (Expr ext s tp) Source # | |
Defined in Lang.Crucible.CFG.Reg | |
type ExprExt (Expr ext s) Source # | |
Defined in Lang.Crucible.CFG.Reg |
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