Lang.Crucible.CFG.Generator

This module provides a monadic interface for constructing control flow graph expressions. The goal is to make it easy to convert languages into CFGs.

The CFGs generated by this interface are similar to, but not quite the same as, the CFGs defined in Lang.Crucible.CFG.Core. The module Lang.Crucible.CFG.SSAConversion contains code that converts the CFGs produced by this interface into Core CFGs in SSA form.

Generator

data Generator ext s (t :: Type -> Type) (ret :: CrucibleType) m a

A generator is used for constructing a CFG from a sequence of monadic actions.

The ext parameter indicates the syntax extension. The s parameter is the phantom parameter for CFGs. The t parameter is the parameterized type that allows user-defined state. The ret parameter is the return type of the CFG. The m parameter is a monad over which the generator is lifted The a parameter is the value returned by the monad.

Instances

Monad m => MonadState (t s) (Generator ext s t ret m)

Defined in Lang.Crucible.CFG.Generator

Methods

get :: Generator ext s t ret m (t s)

put :: t s -> Generator ext s t ret m ()

state :: (t s -> (a, t s)) -> Generator ext s t ret m a

MonadTrans (Generator ext s t ret)

Defined in Lang.Crucible.CFG.Generator

Methods

lift :: Monad m => m a -> Generator ext s t ret m a

MonadFail m => MonadFail (Generator ext s t ret m)

Defined in Lang.Crucible.CFG.Generator

Methods

fail :: String -> Generator ext s t ret m a

MonadIO m => MonadIO (Generator ext s t ret m)

Defined in Lang.Crucible.CFG.Generator

Methods

liftIO :: IO a -> Generator ext s t ret m a

Applicative (Generator ext s t ret m)

Defined in Lang.Crucible.CFG.Generator

Methods

pure :: a -> Generator ext s t ret m a

(<*>) :: Generator ext s t ret m (a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b

liftA2 :: (a -> b -> c) -> Generator ext s t ret m a -> Generator ext s t ret m b -> Generator ext s t ret m c

(*>) :: Generator ext s t ret m a -> Generator ext s t ret m b -> Generator ext s t ret m b

(<*) :: Generator ext s t ret m a -> Generator ext s t ret m b -> Generator ext s t ret m a

Functor (Generator ext s t ret m)

Defined in Lang.Crucible.CFG.Generator

Methods

fmap :: (a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b

(<$) :: a -> Generator ext s t ret m b -> Generator ext s t ret m a

Monad m => Monad (Generator ext s t ret m)

Defined in Lang.Crucible.CFG.Generator

Methods

(>>=) :: Generator ext s t ret m a -> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b

(>>) :: Generator ext s t ret m a -> Generator ext s t ret m b -> Generator ext s t ret m b

return :: a -> Generator ext s t ret m a

MonadCatch m => MonadCatch (Generator ext s t ret m)

Defined in Lang.Crucible.CFG.Generator

Methods

catch :: (HasCallStack, Exception e) => Generator ext s t ret m a -> (e -> Generator ext s t ret m a) -> Generator ext s t ret m a

MonadThrow m => MonadThrow (Generator ext s t ret m)

Defined in Lang.Crucible.CFG.Generator

Methods

throwM :: (HasCallStack, Exception e) => e -> Generator ext s t ret m a

type FunctionDef ext t init ret m = forall s. Assignment (Atom s) init -> (t s, Generator ext s t ret m (Expr ext s ret))

Given the arguments, this returns the initial state, and an action for computing the return value.

defineFunction

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Position

Source position for the function

-> Some (NonceGenerator m)

Nonce generator for internal use

-> FnHandle init ret

Handle for the generated function

-> FunctionDef ext t init ret m

Generator action and initial state

-> m (SomeCFG ext init ret, [AnyCFG ext])

Generated CFG and inner function definitions

The given FunctionDef action is run to generate a registerized CFG. The return value of defineFunction is the generated CFG, and a list of CFGs for any other auxiliary function definitions generated along the way (e.g., for anonymous or inner functions).

This is the same as defineFunctionOpt with the identity transformation.

defineFunctionOpt

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Position

Source position for the function

-> Some (NonceGenerator m)

Nonce generator for internal use

-> FnHandle init ret

Handle for the generated function

-> FunctionDef ext t init ret m

Generator action and initial state

-> (forall s. NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret))

Transformation pass

-> m (SomeCFG ext init ret, [AnyCFG ext])

Generated CFG and inner function definitions

The main API for generating CFGs for a Crucible function.

The given FunctionDef action is run to generate a registerized CFG. The return value of defineFunction is the generated CFG, and a list of CFGs for any other auxiliary function definitions generated along the way (e.g., for anonymous or inner functions).

The caller can supply a transformation to run over the generated CFG (i.e. an optimization pass)

Positions

getPosition :: Generator ext s t ret m Position

Get the current position.

setPosition :: Position -> Generator ext s t ret m ()

Set the current position.

withPosition :: Monad m => Position -> Generator ext s t ret m a -> Generator ext s t ret m a

Set the current position temporarily, and reset it afterwards.

Expressions and statements

newReg :: (Monad m, IsSyntaxExtension ext) => Expr ext s tp -> Generator ext s t ret m (Reg s tp)

Generate a new virtual register with the given initial value.

newUnassignedReg :: Monad m => TypeRepr tp -> Generator ext s t ret m (Reg s tp)

Produce a new virtual register without giving it an initial value. NOTE! If you fail to initialize this register with a subsequent call to assignReg, errors will arise during SSA conversion.

readReg :: (Monad m, IsSyntaxExtension ext) => Reg s tp -> Generator ext s t ret m (Expr ext s tp)

Get the current value of a register.

assignReg :: (Monad m, IsSyntaxExtension ext) => Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()

Update the value of a register.

modifyReg :: (Monad m, IsSyntaxExtension ext) => Reg s tp -> (Expr ext s tp -> Expr ext s tp) -> Generator ext s t ret m ()

Modify the value of a register.

modifyRegM :: (Monad m, IsSyntaxExtension ext) => Reg s tp -> (Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)) -> Generator ext s t ret m ()

Modify the value of a register.

readGlobal :: (Monad m, IsSyntaxExtension ext) => GlobalVar tp -> Generator ext s t ret m (Expr ext s tp)

Read a global variable.

writeGlobal :: (Monad m, IsSyntaxExtension ext) => GlobalVar tp -> Expr ext s tp -> Generator ext s t ret m ()

Write to a global variable.

References

newRef :: (Monad m, IsSyntaxExtension ext) => Expr ext s tp -> Generator ext s t ret m (Expr ext s (ReferenceType tp))

Generate a new reference cell with the given initial contents.

newEmptyRef :: (Monad m, IsSyntaxExtension ext) => TypeRepr tp -> Generator ext s t ret m (Expr ext s (ReferenceType tp))

Generate a new empty reference cell. If an unassigned reference is later read, it will generate a runtime error.

readRef :: (Monad m, IsSyntaxExtension ext) => Expr ext s (ReferenceType tp) -> Generator ext s t ret m (Expr ext s tp)

Read the current value of a reference cell.

writeRef :: (Monad m, IsSyntaxExtension ext) => Expr ext s (ReferenceType tp) -> Expr ext s tp -> Generator ext s t ret m ()

Write the given value into the reference cell.

dropRef :: (Monad m, IsSyntaxExtension ext) => Expr ext s (ReferenceType tp) -> Generator ext s t ret m ()

Deallocate the given reference cell, returning it to an uninialized state. The reference cell can still be used; subsequent writes will succeed, and reads will succeed if some value is written first.

call

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Expr ext s (FunctionHandleType args ret)

function to call

-> Assignment (Expr ext s) args

function arguments

-> Generator ext s t r m (Expr ext s ret)

Call a function.

assertExpr

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Expr ext s BoolType

assertion

-> Expr ext s (StringType Unicode)

error message

-> Generator ext s t ret m ()

Add an assert statement.

assumeExpr

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Expr ext s BoolType

assumption

-> Expr ext s (StringType Unicode)

reason message

-> Generator ext s t ret m ()

Add an assume statement.

addPrintStmt :: (Monad m, IsSyntaxExtension ext) => Expr ext s (StringType Unicode) -> Generator ext s t ret m ()

Add a statement to print a value.

addBreakpointStmt

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Text

breakpoint name

-> Assignment (Value s) args

breakpoint values

-> Generator ext s t r m ()

Add a breakpoint.

extensionStmt :: (Monad m, IsSyntaxExtension ext) => StmtExtension ext (Expr ext s) tp -> Generator ext s t ret m (Expr ext s tp)

Add a statement from the syntax extension to the current basic block.

mkAtom :: (Monad m, IsSyntaxExtension ext) => Expr ext s tp -> Generator ext s t ret m (Atom s tp)

Create an atom equivalent to the given expression if it is not already an AtomExpr.

mkFresh :: (Monad m, IsSyntaxExtension ext) => BaseTypeRepr tp -> Maybe SolverSymbol -> Generator ext s t ret m (Atom s (BaseToType tp))

mkFreshFloat :: (Monad m, IsSyntaxExtension ext) => FloatInfoRepr fi -> Maybe SolverSymbol -> Generator ext s t ret m (Atom s (FloatType fi))

forceEvaluation :: (Monad m, IsSyntaxExtension ext) => Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)

Evaluate an expression to an AtomExpr, so that it can be reused multiple times later.

Labels

newLabel :: Monad m => Generator ext s t ret m (Label s)

Create a new block label.

newLambdaLabel :: Monad m => KnownRepr TypeRepr tp => Generator ext s t ret m (LambdaLabel s tp)

Create a new lambda label.

newLambdaLabel' :: Monad m => TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)

Create a new lambda label, using an explicit TypeRepr.

currentBlockID :: Generator ext s t ret m (BlockID s)

Return the label of the current basic block.

Block-terminating statements

The following operations produce block-terminating statements, and have early termination behavior in the Generator monad: Like fail, they have polymorphic return types and cause any following monadic actions to be skipped.

jump :: (Monad m, IsSyntaxExtension ext) => Label s -> Generator ext s t ret m a

Jump to the given label.

jumpToLambda :: (Monad m, IsSyntaxExtension ext) => LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a

Jump to the given label with output.

branch

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Expr ext s BoolType

condition

-> Label s

true label

-> Label s

false label

-> Generator ext s t ret m a

Branch between blocks.

returnFromFunction :: (Monad m, IsSyntaxExtension ext) => Expr ext s ret -> Generator ext s t ret m a

Return from this function with the given return value.

reportError :: (Monad m, IsSyntaxExtension ext) => Expr ext s (StringType Unicode) -> Generator ext s t ret m a

Report an error message.

branchMaybe

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Expr ext s (MaybeType tp)

-> LambdaLabel s tp

label for Just

-> Label s

label for Nothing

-> Generator ext s t ret m a

Branch between blocks based on a Maybe value.

branchVariant

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Expr ext s (VariantType varctx)

value to scrutinize

-> Assignment (LambdaLabel s) varctx

target labels

-> Generator ext s t ret m a

Switch on a variant value. Examine the tag of the variant and jump to the appropriate switch target.

tailCall

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Expr ext s (FunctionHandleType args ret)

function to call

-> Assignment (Expr ext s) args

function arguments

-> Generator ext s t ret m a

End a block with a tail call to a function.

Defining blocks

The block-defining commands should be used with a Generator action ending with a block-terminating statement, which gives it a polymorphic type.

defineBlock :: (Monad m, IsSyntaxExtension ext) => Label s -> (forall a. Generator ext s t ret m a) -> Generator ext s t ret m ()

Define a block with an ordinary label.

defineLambdaBlock :: (Monad m, IsSyntaxExtension ext) => LambdaLabel s tp -> (forall a. Expr ext s tp -> Generator ext s t ret m a) -> Generator ext s t ret m ()

Define a block that has a lambda label.

defineBlockLabel :: (Monad m, IsSyntaxExtension ext) => (forall a. Generator ext s t ret m a) -> Generator ext s t ret m (Label s)

Define a block with a fresh label, returning the label.

recordCFG :: AnyCFG ext -> Generator ext s t ret m ()

Stash the given CFG away for later retrieval. This is primarily used when translating inner and anonymous functions in the context of an outer function.

Control-flow combinators

continue

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Label s

label for new block

-> (forall a. Generator ext s t ret m a)

action to end current block

-> Generator ext s t ret m ()

End the translation of the current block, and then continue generating a new block with the given label.

continueLambda

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> LambdaLabel s tp

label for new block

-> (forall a. Generator ext s t ret m a)

action to end current block

-> Generator ext s t ret m (Expr ext s tp)

End the translation of the current block, and then continue generating a new lambda block with the given label. The return value is the argument to the lambda block.

whenCond :: (Monad m, IsSyntaxExtension ext) => Expr ext s BoolType -> Generator ext s t ret m () -> Generator ext s t ret m ()

Run a computation when a condition is true.

unlessCond :: (Monad m, IsSyntaxExtension ext) => Expr ext s BoolType -> Generator ext s t ret m () -> Generator ext s t ret m ()

Run a computation when a condition is false.

ifte

Arguments

:: (Monad m, IsSyntaxExtension ext, KnownRepr TypeRepr tp)

=> Expr ext s BoolType

-> Generator ext s t ret m (Expr ext s tp)

true branch

-> Generator ext s t ret m (Expr ext s tp)

false branch

-> Generator ext s t ret m (Expr ext s tp)

Expression-level if-then-else.

ifte'

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> TypeRepr tp

-> Expr ext s BoolType

-> Generator ext s t ret m (Expr ext s tp)

true branch

-> Generator ext s t ret m (Expr ext s tp)

false branch

-> Generator ext s t ret m (Expr ext s tp)

ifte_

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Expr ext s BoolType

-> Generator ext s t ret m ()

true branch

-> Generator ext s t ret m ()

false branch

-> Generator ext s t ret m ()

Statement-level if-then-else.

ifteM

Arguments

:: (Monad m, IsSyntaxExtension ext, KnownRepr TypeRepr tp)

=> Generator ext s t ret m (Expr ext s BoolType)

-> Generator ext s t ret m (Expr ext s tp)

true branch

-> Generator ext s t ret m (Expr ext s tp)

false branch

-> Generator ext s t ret m (Expr ext s tp)

Expression-level if-then-else with a monadic condition.

data MatchMaybe j r

Constructors

MatchMaybe

Fields

• onJust :: j -> r
• onNothing :: r

caseMaybe

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Expr ext s (MaybeType tp)

expression to scrutinize

-> TypeRepr r

result type

-> MatchMaybe (Expr ext s tp) (Generator ext s t ret m (Expr ext s r))

case branches

-> Generator ext s t ret m (Expr ext s r)

Compute an expression by cases over a Maybe value.

caseMaybe_

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Expr ext s (MaybeType tp)

expression to scrutinize

-> MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())

case branches

-> Generator ext s t ret m ()

Evaluate different statements by cases over a Maybe value.

fromJustExpr

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Expr ext s (MaybeType tp)

-> Expr ext s (StringType Unicode)

error message

-> Generator ext s t ret m (Expr ext s tp)

Return the argument of a Just value, or call reportError if the value is Nothing.

assertedJustExpr

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> Expr ext s (MaybeType tp)

-> Expr ext s (StringType Unicode)

error message

-> Generator ext s t ret m (Expr ext s tp)

This asserts that the value in the expression is a Just value, and returns the underlying value.

while

Arguments

:: (Monad m, IsSyntaxExtension ext)

=> (Position, Generator ext s t ret m (Expr ext s BoolType))

test condition

-> (Position, Generator ext s t ret m ())

loop body

-> Generator ext s t ret m ()

Execute the loop body as long as the test condition is true.

Re-exports

data Ctx k

Kind Ctx k comprises lists of types of kind k.

Constructors

EmptyCtx

(Ctx k) ::> k

Instances

FoldableFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

foldMapFC :: forall f m. Monoid m => (forall (x :: k0). f x -> m) -> forall (x :: l). Assignment f x -> m

foldrFC :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> Assignment f x -> b

foldlFC :: forall f b. (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> Assignment f x -> b

foldrFC' :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> Assignment f x -> b

foldlFC' :: forall f b. (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> Assignment f x -> b

toListFC :: (forall (x :: k0). f x -> a) -> forall (x :: l). Assignment f x -> [a]

FunctorFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

fmapFC :: (forall (x :: k0). f x -> g x) -> forall (x :: l). Assignment f x -> Assignment g x

OrdFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

compareFC :: (forall (x :: k0) (y :: k0). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). Assignment f x -> Assignment f y -> OrderingF x y

TestEqualityFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

testEqualityFC :: (forall (x :: k0) (y :: k0). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). Assignment f x -> Assignment f y -> Maybe (x :~: y)

TraversableFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

traverseFC :: forall f g m. Applicative m => (forall (x :: k0). f x -> m (g x)) -> forall (x :: l). Assignment f x -> m (Assignment g x)

FoldableFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

ifoldMapFC :: forall f m (z :: l). Monoid m => (forall (x :: k0). IndexF (Assignment f z) x -> f x -> m) -> Assignment f z -> m

ifoldrFC :: forall (z :: l) f b. (forall (x :: k0). IndexF (Assignment f z) x -> f x -> b -> b) -> b -> Assignment f z -> b

ifoldlFC :: forall f b (z :: l). (forall (x :: k0). IndexF (Assignment f z) x -> b -> f x -> b) -> b -> Assignment f z -> b

ifoldrFC' :: forall f b (z :: l). (forall (x :: k0). IndexF (Assignment f z) x -> f x -> b -> b) -> b -> Assignment f z -> b

ifoldlFC' :: forall f b. (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> Assignment f x -> b

itoListFC :: forall f a (z :: l). (forall (x :: k0). IndexF (Assignment f z) x -> f x -> a) -> Assignment f z -> [a]

FunctorFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

imapFC :: forall f g (z :: l). (forall (x :: k0). IndexF (Assignment f z) x -> f x -> g x) -> Assignment f z -> Assignment g z

TraversableFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

itraverseFC :: forall m (z :: l) f g. Applicative m => (forall (x :: k0). IndexF (Assignment f z) x -> f x -> m (g x)) -> Assignment f z -> m (Assignment g z)

OrdFC (BalancedTree h :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

compareFC :: (forall (x :: k0) (y :: k0). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). BalancedTree h f x -> BalancedTree h f y -> OrderingF x y

OrdFC (BinomialTree h :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

compareFC :: (forall (x :: k0) (y :: k0). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). BinomialTree h f x -> BinomialTree h f y -> OrderingF x y

TestEqualityFC (BalancedTree h :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

testEqualityFC :: (forall (x :: k0) (y :: k0). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). BalancedTree h f x -> BalancedTree h f y -> Maybe (x :~: y)

TestEqualityFC (BinomialTree h :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

testEqualityFC :: (forall (x :: k0) (y :: k0). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). BinomialTree h f x -> BinomialTree h f y -> Maybe (x :~: y)

Category (Diff :: Ctx k -> Ctx k -> Type)

Implemented with noDiff and addDiff

Defined in Data.Parameterized.Context.Unsafe

Methods

id :: forall (a :: k0). Diff a a

(.) :: forall (b :: k0) (c :: k0) (a :: k0). Diff b c -> Diff a b -> Diff a c

TestEquality (BlockID blocks :: Ctx CrucibleType -> Type)

Defined in Lang.Crucible.CFG.Core

Methods

testEquality :: forall (a :: k) (b :: k). BlockID blocks a -> BlockID blocks b -> Maybe (a :~: b)

TestEquality (MatlabFnWrapper t :: Ctx BaseType -> Type)

Defined in What4.Expr.Builder

Methods

testEquality :: forall (a :: k) (b :: k). MatlabFnWrapper t a -> MatlabFnWrapper t b -> Maybe (a :~: b)

IsSymFn (SymFn sym) => TestEquality (SymFnWrapper sym :: Ctx BaseType -> Type)

Defined in What4.Interface

Methods

testEquality :: forall (a :: k) (b :: k). SymFnWrapper sym a -> SymFnWrapper sym b -> Maybe (a :~: b)

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

Defined in Lang.Crucible.Simulator.CallFrame

Methods

testEquality :: forall (a :: k) (b :: k). CrucibleBranchTarget f a -> CrucibleBranchTarget f b -> Maybe (a :~: b)

HashableF (MatlabFnWrapper t :: Ctx BaseType -> Type)

Defined in What4.Expr.Builder

Methods

hashWithSaltF :: forall (tp :: k). Int -> MatlabFnWrapper t tp -> Int

hashF :: forall (tp :: k). MatlabFnWrapper t tp -> Int

OrdF (BlockID blocks :: Ctx CrucibleType -> Type)

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

IsSymFn (SymFn sym) => OrdF (SymFnWrapper sym :: Ctx BaseType -> Type)

Defined in What4.Interface

Methods

compareF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> OrderingF x y

leqF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool

ltF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool

geqF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool

gtF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool

ShowF (BlockID blocks :: Ctx CrucibleType -> Type)

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

ShowF (Size :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: forall p q (tp :: k0) a. p Size -> q tp -> (Show (Size tp) => a) -> a

showF :: forall (tp :: k0). Size tp -> String

showsPrecF :: forall (tp :: k0). Int -> Size tp -> String -> String

TestEquality f => TestEquality (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

testEquality :: forall (a :: k0) (b :: k0). Assignment f a -> Assignment f b -> Maybe (a :~: b)

(HashableF f, TestEquality f) => HashableF (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

hashWithSaltF :: forall (tp :: k0). Int -> Assignment f tp -> Int

hashF :: forall (tp :: k0). Assignment f tp -> Int

OrdF f => OrdF (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

compareF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> OrderingF x y

leqF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> Bool

ltF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> Bool

geqF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> Bool

gtF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> Bool

ShowF dom => ShowF (PointAbstraction blocks dom :: Ctx CrucibleType -> Type)

Defined in Lang.Crucible.Analysis.Fixpoint

Methods

withShow :: forall p q (tp :: k) a. p (PointAbstraction blocks dom) -> q tp -> (Show (PointAbstraction blocks dom tp) => a) -> a

showF :: forall (tp :: k). PointAbstraction blocks dom tp -> String

showsPrecF :: forall (tp :: k). Int -> PointAbstraction blocks dom tp -> String -> String

ShowF f => ShowF (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: forall p q (tp :: k0) a. p (Assignment f) -> q tp -> (Show (Assignment f tp) => a) -> a

showF :: forall (tp :: k0). Assignment f tp -> String

showsPrecF :: forall (tp :: k0). Int -> Assignment f tp -> String -> String

KnownRepr (Assignment f :: Ctx k -> Type) (EmptyCtx :: Ctx k)

Defined in Data.Parameterized.Context.Unsafe

Methods

knownRepr :: Assignment f EmptyCtx

(KnownRepr (Assignment f) ctx, KnownRepr f bt) => KnownRepr (Assignment f :: Ctx k -> Type) (ctx ::> bt :: Ctx k)

Defined in Data.Parameterized.Context.Unsafe

Methods

knownRepr :: Assignment f (ctx ::> bt)

HashableF f => HashableF (BalancedTree h f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

hashWithSaltF :: forall (tp :: k0). Int -> BalancedTree h f tp -> Int

hashF :: forall (tp :: k0). BalancedTree h f tp -> Int

HashableF f => HashableF (BinomialTree h f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

hashWithSaltF :: forall (tp :: k0). Int -> BinomialTree h f tp -> Int

hashF :: forall (tp :: k0). BinomialTree h f tp -> Int

PrettyExt ext => ShowF (Block ext blocks ret :: Ctx CrucibleType -> Type)

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

ShowF f => ShowF (BalancedTree h f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: forall p q (tp :: k0) a. p (BalancedTree h f) -> q tp -> (Show (BalancedTree h f tp) => a) -> a

showF :: forall (tp :: k0). BalancedTree h f tp -> String

showsPrecF :: forall (tp :: k0). Int -> BalancedTree h f tp -> String -> String

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

Defined in Lang.Crucible.Simulator.OverrideSim

Methods

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

put :: SimState p sym ext rtp (OverrideLang ret) ('Just args) -> OverrideSim p sym ext rtp args ret ()

state :: (SimState p sym ext rtp (OverrideLang ret) ('Just args) -> (a, SimState p sym ext rtp (OverrideLang ret) ('Just args))) -> OverrideSim p sym ext rtp args ret a

data Position

Instances

Show Position

Defined in What4.ProgramLoc

Methods

showsPrec :: Int -> Position -> ShowS

show :: Position -> String

showList :: [Position] -> ShowS

NFData Position

Defined in What4.ProgramLoc

Methods

rnf :: Position -> ()

Eq Position

Defined in What4.ProgramLoc

Methods

(==) :: Position -> Position -> Bool

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

Ord Position

Defined in What4.ProgramLoc

Methods

compare :: Position -> Position -> Ordering

(<) :: Position -> Position -> Bool

(<=) :: Position -> Position -> Bool

(>) :: Position -> Position -> Bool

(>=) :: Position -> Position -> Bool

max :: Position -> Position -> Position

min :: Position -> Position -> Position

Pretty Position

Defined in What4.ProgramLoc

Methods

pretty :: Position -> Doc ann

prettyList :: [Position] -> Doc ann

data Stmt ext s

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

PrettyExt ext => Show (Stmt ext s)

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)

Defined in Lang.Crucible.CFG.Reg

Methods

pretty :: Stmt ext s -> Doc ann

prettyList :: [Stmt ext s] -> Doc ann

data Value s (tp :: CrucibleType)

A value is either a register or an atom.

Constructors

RegValue !(Reg s tp)

AtomValue !(Atom s tp)

Instances

TestEquality (Value s :: CrucibleType -> Type)

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)

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)

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)

Defined in Lang.Crucible.CFG.Reg

Methods

pretty :: ValueSet s -> Doc ann

prettyList :: [ValueSet s] -> Doc ann

Show (Value s tp)

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)

Defined in Lang.Crucible.CFG.Reg

Methods

pretty :: Value s tp -> Doc ann

prettyList :: [Value s tp] -> Doc ann

data Atom s (tp :: CrucibleType)

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

TestEquality (Atom s :: CrucibleType -> Type)

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)

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)

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)

Defined in Lang.Crucible.CFG.Reg

Methods

pretty :: Atom s tp -> Doc ann

prettyList :: [Atom s tp] -> Doc ann

newtype Label s

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

Constructors

Label

Fields

• labelId :: Nonce s UnitType

Instances

Show (Label s)

Defined in Lang.Crucible.CFG.Reg

Methods

showsPrec :: Int -> Label s -> ShowS

show :: Label s -> String

showList :: [Label s] -> ShowS

Eq (Label s)

Defined in Lang.Crucible.CFG.Reg

Methods

(==) :: Label s -> Label s -> Bool

(/=) :: Label s -> Label s -> Bool

Ord (Label s)

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)

Defined in Lang.Crucible.CFG.Reg

Methods

pretty :: Label s -> Doc ann

prettyList :: [Label s] -> Doc ann

data Expr ext s (tp :: CrucibleType)

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

PrettyExt ext => ShowF (Expr ext s :: CrucibleType -> Type)

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)

Defined in Lang.Crucible.CFG.Reg

Associated Types

type ExprExt (Expr ext s)

Methods

app :: forall (tp :: CrucibleType). App (ExprExt (Expr ext s)) (Expr ext s) tp -> Expr ext s tp

asApp :: forall (tp :: CrucibleType). Expr ext s tp -> Maybe (App (ExprExt (Expr ext s)) (Expr ext s) tp)

exprType :: forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp

IsString (Expr ext s (StringType Unicode))

Defined in Lang.Crucible.CFG.Reg

Methods

fromString :: String -> Expr ext s (StringType Unicode)

PrettyExt ext => Show (Expr ext s tp)

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)

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)

Defined in Lang.Crucible.CFG.Reg

type ExprExt (Expr ext s) = ext

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

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

PrettyExt ext => Show (CFG ext s init ret)

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)

Defined in Lang.Crucible.CFG.Reg

Methods

pretty :: CFG ext s init ret -> Doc ann

prettyList :: [CFG ext s init ret] -> Doc ann

data BlockID (s :: Type) where

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

Show (BlockID s)

Defined in Lang.Crucible.CFG.Reg

Methods

showsPrec :: Int -> BlockID s -> ShowS

show :: BlockID s -> String

showList :: [BlockID s] -> ShowS

Eq (BlockID s)

Defined in Lang.Crucible.CFG.Reg

Methods

(==) :: BlockID s -> BlockID s -> Bool

(/=) :: BlockID s -> BlockID s -> Bool

Ord (BlockID s)

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

data GlobalVar (tp :: CrucibleType)

A global variable.

Constructors

GlobalVar

Fields

• globalNonce :: !(Nonce GlobalNonceGenerator tp)
• globalName :: !Text
• globalType :: !(TypeRepr tp)

Instances

TestEquality GlobalVar

Defined in Lang.Crucible.CFG.Common

Methods

testEquality :: forall (a :: k) (b :: k). GlobalVar a -> GlobalVar b -> Maybe (a :~: b)

OrdF GlobalVar

Defined in Lang.Crucible.CFG.Common

Methods

compareF :: forall (x :: k) (y :: k). GlobalVar x -> GlobalVar y -> OrderingF x y

leqF :: forall (x :: k) (y :: k). GlobalVar x -> GlobalVar y -> Bool

ltF :: forall (x :: k) (y :: k). GlobalVar x -> GlobalVar y -> Bool

geqF :: forall (x :: k) (y :: k). GlobalVar x -> GlobalVar y -> Bool

gtF :: forall (x :: k) (y :: k). GlobalVar x -> GlobalVar y -> Bool

ShowF GlobalVar

Defined in Lang.Crucible.CFG.Common

Methods

withShow :: forall p q (tp :: k) a. p GlobalVar -> q tp -> (Show (GlobalVar tp) => a) -> a

showF :: forall (tp :: k). GlobalVar tp -> String

showsPrecF :: forall (tp :: k). Int -> GlobalVar tp -> String -> String

Show (GlobalVar tp)

Defined in Lang.Crucible.CFG.Common

Methods

showsPrec :: Int -> GlobalVar tp -> ShowS

show :: GlobalVar tp -> String

showList :: [GlobalVar tp] -> ShowS

Pretty (GlobalVar tp)

Defined in Lang.Crucible.CFG.Common

Methods

pretty :: GlobalVar tp -> Doc ann

prettyList :: [GlobalVar tp] -> Doc ann

newtype BreakpointName

Constructors

BreakpointName

Fields

• breakpointNameText :: Text

Instances

Show BreakpointName

Defined in Lang.Crucible.CFG.Common

Methods

showsPrec :: Int -> BreakpointName -> ShowS

show :: BreakpointName -> String

showList :: [BreakpointName] -> ShowS

Eq BreakpointName

Defined in Lang.Crucible.CFG.Common

Methods

(==) :: BreakpointName -> BreakpointName -> Bool

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

Ord BreakpointName

Defined in Lang.Crucible.CFG.Common

Methods

compare :: BreakpointName -> BreakpointName -> Ordering

(<) :: BreakpointName -> BreakpointName -> Bool

(<=) :: BreakpointName -> BreakpointName -> Bool

(>) :: BreakpointName -> BreakpointName -> Bool

(>=) :: BreakpointName -> BreakpointName -> Bool

max :: BreakpointName -> BreakpointName -> BreakpointName

min :: BreakpointName -> BreakpointName -> BreakpointName

Pretty BreakpointName

Defined in Lang.Crucible.CFG.Common

Methods

pretty :: BreakpointName -> Doc ann

prettyList :: [BreakpointName] -> Doc ann

data SomeCFG ext init ret

SomeCFG is a CFG with an arbitrary parameter s.

Constructors

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

data Block ext s (ret :: CrucibleType)

A basic block within a function.

Instances

PrettyExt ext => Show (Block ext s ret)

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)

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)

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)

Defined in Lang.Crucible.CFG.Reg

Methods

pretty :: Block ext s ret -> Doc ann

prettyList :: [Block ext s ret] -> Doc ann

data TermStmt s (ret :: CrucibleType) where

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

Show (TermStmt s ret)

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)

Defined in Lang.Crucible.CFG.Reg

Methods

pretty :: TermStmt s ret -> Doc ann

prettyList :: [TermStmt s ret] -> Doc ann

data Reg s (tp :: CrucibleType)

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

TestEquality (Reg s :: CrucibleType -> Type)

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)

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)

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)

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)

Defined in Lang.Crucible.CFG.Reg

Methods

pretty :: Reg s tp -> Doc ann

prettyList :: [Reg s tp] -> Doc ann

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

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

TestEquality (LambdaLabel s :: CrucibleType -> Type)

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)

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)

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)

Defined in Lang.Crucible.CFG.Reg

Methods

pretty :: LambdaLabel s tp -> Doc ann

prettyList :: [LambdaLabel s tp] -> Doc ann

data AtomSource s (tp :: CrucibleType)

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.

data AtomValue ext s (tp :: CrucibleType) where

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

PrettyExt ext => Show (AtomValue ext s tp)

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)

Defined in Lang.Crucible.CFG.Reg

Methods

pretty :: AtomValue ext s tp -> Doc ann

prettyList :: [AtomValue ext s tp] -> Doc ann

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

A set of values.

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

freshGlobalVar :: HandleAllocator -> Text -> TypeRepr tp -> IO (GlobalVar tp)

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

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

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

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

Deprecated: Use cfgArgTypes instead

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)

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

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

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

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

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

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.

substAtom :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Atom s tp -> m (Atom 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)

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)

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)

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

mkBlock

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

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

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)

termStmtInputs :: TermStmt s ret -> ValueSet s

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

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

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)

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

Fold all registers that are inputs tostmt.

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

earlyMergeLoops :: (TraverseExt ext, Monad m, Show (CFG ext s init ret)) => NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret)

This is the main pass that attempts to optimize early exits in the loops in a CFG. In particular, this transformation ensures that the postdominator of the loop header is a member of the loop.

Given a natural loop, its members are a set of blocks bs. Let the exit edges be the edges from some block b in bs to either the loop header or a block not in bs.

Let (i, j) be such an exit edge.This transofrmation inserts a new block r such that in the transformed cfg there is an edge (i, r) and an edge (r, j). Moreover, the transformation ensures that [i, r, j'] is not feasible for j' != j. This works by setting a "destination" register d := j in each block i for each exit edge (i, j), and switching on the value of d in the block r.