Copyright	(c) Galois Inc 2017
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.CFG.Extension

Contents

Empty extension

Description

This module provides basic definitions necessary for handling syntax extensions in Crucible. Syntax extensions provide a mechanism for users of the Crucible library to add new syntactic forms to the base control-flow-graph representation of programs.

Syntax extensions are more flexible and less tedious for some use cases than other extension methods (e.g., override functions).

Synopsis

type family ExprExtension (ext :: Type) :: (CrucibleType -> Type) -> CrucibleType -> Type
type family StmtExtension (ext :: Type) :: (CrucibleType -> Type) -> CrucibleType -> Type
class (OrdFC (ExprExtension ext), TraversableFC (ExprExtension ext), PrettyApp (ExprExtension ext), TypeApp (ExprExtension ext), TraversableFC (StmtExtension ext), PrettyApp (StmtExtension ext), TypeApp (StmtExtension ext)) => IsSyntaxExtension ext
class PrettyApp (app :: (k -> Type) -> k -> Type) where
- ppApp :: forall f ann. (forall x. f x -> Doc ann) -> forall x. app f x -> Doc ann
class TypeApp (app :: (CrucibleType -> Type) -> CrucibleType -> Type) where
- appType :: app f x -> TypeRepr x
type PrettyExt ext = (PrettyApp (ExprExtension ext), PrettyApp (StmtExtension ext))
type TraverseExt ext = (TraversableFC (ExprExtension ext), TraversableFC (StmtExtension ext))
data EmptyExprExtension :: (CrucibleType -> Type) -> CrucibleType -> Type
data EmptyStmtExtension :: (CrucibleType -> Type) -> CrucibleType -> Type

Documentation

type family ExprExtension (ext :: Type) :: (CrucibleType -> Type) -> CrucibleType -> Type Source #

Instances

Instances details

type ExprExtension () Source #
Instance details Defined in Lang.Crucible.CFG.Extension type ExprExtension () = EmptyExprExtension

type family StmtExtension (ext :: Type) :: (CrucibleType -> Type) -> CrucibleType -> Type Source #

Instances

Instances details

type StmtExtension () Source #
Instance details Defined in Lang.Crucible.CFG.Extension type StmtExtension () = EmptyStmtExtension

class (OrdFC (ExprExtension ext), TraversableFC (ExprExtension ext), PrettyApp (ExprExtension ext), TypeApp (ExprExtension ext), TraversableFC (StmtExtension ext), PrettyApp (StmtExtension ext), TypeApp (StmtExtension ext)) => IsSyntaxExtension ext Source #

This class captures all the grungy technical capabilities that are needed for syntax extensions. These capabilities allow syntax to be tested for equality, ordered, put into hashtables, traversed and printed, etc.

The actual meat of implementing the semantics of syntax extensions is left to a later phase. See the ExtensionImpl record defined in Lang.Crucible.Simulator.ExecutionTree.

Instances

Instances details

IsSyntaxExtension () Source #
Instance details Defined in Lang.Crucible.CFG.Extension

class PrettyApp (app :: (k -> Type) -> k -> Type) where Source #

Methods

ppApp :: forall f ann. (forall x. f x -> Doc ann) -> forall x. app f x -> Doc ann Source #

Instances

Instances details

PrettyApp EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods ppApp :: (forall (x :: k). f x -> Doc ann) -> forall (x :: k). EmptyExprExtension f x -> Doc ann Source #
PrettyApp EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods ppApp :: (forall (x :: k). f x -> Doc ann) -> forall (x :: k). EmptyStmtExtension f x -> Doc ann Source #
PrettyApp (ExprExtension ext) => PrettyApp (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods ppApp :: (forall (x :: k). f x -> Doc ann) -> forall (x :: k). App ext f x -> Doc ann Source #

class TypeApp (app :: (CrucibleType -> Type) -> CrucibleType -> Type) where Source #

Methods

appType :: app f x -> TypeRepr x Source #

Instances

Instances details

TypeApp EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods appType :: forall (f :: CrucibleType -> Type) (x :: CrucibleType). EmptyExprExtension f x -> TypeRepr x Source #
TypeApp EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods appType :: forall (f :: CrucibleType -> Type) (x :: CrucibleType). EmptyStmtExtension f x -> TypeRepr x Source #
TypeApp (ExprExtension ext) => TypeApp (App ext) Source #	Compute a run-time representation of the type of an application.
Instance details Defined in Lang.Crucible.CFG.Expr Methods appType :: forall (f :: CrucibleType -> Type) (x :: CrucibleType). App ext f x -> TypeRepr x Source #

type PrettyExt ext = (PrettyApp (ExprExtension ext), PrettyApp (StmtExtension ext)) Source #

type TraverseExt ext = (TraversableFC (ExprExtension ext), TraversableFC (StmtExtension ext)) Source #

Empty extension

data EmptyExprExtension :: (CrucibleType -> Type) -> CrucibleType -> Type Source #

The empty expression syntax extension, which adds no new syntactic forms.

Instances

Instances details

TypeApp EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods appType :: forall (f :: CrucibleType -> Type) (x :: CrucibleType). EmptyExprExtension f x -> TypeRepr x Source #
PrettyApp EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods ppApp :: (forall (x :: k). f x -> Doc ann) -> forall (x :: k). EmptyExprExtension f x -> Doc ann Source #
FoldableFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). EmptyExprExtension f x -> m # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> EmptyExprExtension f x -> b # foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> EmptyExprExtension f x -> b # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> EmptyExprExtension f x -> b # foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> EmptyExprExtension f x -> b # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). EmptyExprExtension f x -> [a] #
FunctorFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). EmptyExprExtension f x -> EmptyExprExtension g x #
HashableFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods hashWithSaltFC :: (forall (x :: k). Int -> f x -> Int) -> forall (x :: l). Int -> EmptyExprExtension f x -> Int #
OrdFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). EmptyExprExtension f x -> EmptyExprExtension f y -> OrderingF x y #
ShowFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods showFC :: (forall (x :: k). f x -> String) -> forall (x :: l). EmptyExprExtension f x -> String # showsPrecFC :: (forall (x :: k). Int -> f x -> ShowS) -> forall (x :: l). Int -> EmptyExprExtension f x -> ShowS #
TestEqualityFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). EmptyExprExtension f x -> EmptyExprExtension f y -> Maybe (x :~: y) #
TraversableFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: l). EmptyExprExtension f x -> m (EmptyExprExtension g x) #
Show (EmptyExprExtension f tp) Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods showsPrec :: Int -> EmptyExprExtension f tp -> ShowS # show :: EmptyExprExtension f tp -> String # showList :: [EmptyExprExtension f tp] -> ShowS #

data EmptyStmtExtension :: (CrucibleType -> Type) -> CrucibleType -> Type Source #

The empty statement syntax extension, which adds no new syntactic forms.

Instances

Instances details

TypeApp EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods appType :: forall (f :: CrucibleType -> Type) (x :: CrucibleType). EmptyStmtExtension f x -> TypeRepr x Source #
PrettyApp EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods ppApp :: (forall (x :: k). f x -> Doc ann) -> forall (x :: k). EmptyStmtExtension f x -> Doc ann Source #
FoldableFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). EmptyStmtExtension f x -> m # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> EmptyStmtExtension f x -> b # foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> EmptyStmtExtension f x -> b # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> EmptyStmtExtension f x -> b # foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> EmptyStmtExtension f x -> b # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). EmptyStmtExtension f x -> [a] #
FunctorFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). EmptyStmtExtension f x -> EmptyStmtExtension g x #
HashableFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods hashWithSaltFC :: (forall (x :: k). Int -> f x -> Int) -> forall (x :: l). Int -> EmptyStmtExtension f x -> Int #
OrdFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). EmptyStmtExtension f x -> EmptyStmtExtension f y -> OrderingF x y #
ShowFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods showFC :: (forall (x :: k). f x -> String) -> forall (x :: l). EmptyStmtExtension f x -> String # showsPrecFC :: (forall (x :: k). Int -> f x -> ShowS) -> forall (x :: l). Int -> EmptyStmtExtension f x -> ShowS #
TestEqualityFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). EmptyStmtExtension f x -> EmptyStmtExtension f y -> Maybe (x :~: y) #
TraversableFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: l). EmptyStmtExtension f x -> m (EmptyStmtExtension g x) #
Show (EmptyStmtExtension f tp) Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods showsPrec :: Int -> EmptyStmtExtension f tp -> ShowS # show :: EmptyStmtExtension f tp -> String # showList :: [EmptyStmtExtension f tp] -> ShowS #