crucible-llvm-0.6: Support for translating and executing LLVM code in Crucible
Copyright(c) Galois Inc 2015-2016
LicenseBSD3
Maintainerrdockins@galois.com
Stabilityprovisional
Safe HaskellSafe-Inferred
LanguageHaskell2010

Lang.Crucible.LLVM.Extension

Description

Syntax extension definitions for LLVM

Synopsis

Documentation

data LLVMArch Source #

Data kind for representing LLVM architectures. Currently only X86 variants are supported.

Instances

Instances details
Generic LLVMArch Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Arch

Associated Types

type Rep LLVMArch :: Type -> Type #

Methods

from :: LLVMArch -> Rep LLVMArch x #

to :: Rep LLVMArch x -> LLVMArch #

TestEquality ArchRepr Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Arch

Methods

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

TestEquality ModuleTranslation Source # 
Instance details

Defined in Lang.Crucible.LLVM.Translation

Methods

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

OrdF ArchRepr Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Arch

Methods

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

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

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

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

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

type Rep LLVMArch Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Arch

type Rep LLVMArch = D1 ('MetaData "LLVMArch" "Lang.Crucible.LLVM.Extension.Arch" "crucible-llvm-0.6-JJ7tfvbGrbFFTkl5eJBN3H" 'False) (C1 ('MetaCons "X86" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)))

type X86 = 'X86 Source #

LLVM Architecture tag for X86 variants

X86 :: Nat -> LLVMArch

type family ArchWidth (arch :: LLVMArch) :: Nat where ... Source #

Type family defining the native machine word size for a given architecture.

Equations

ArchWidth (X86 wptr) = wptr 

data ArchRepr (arch :: LLVMArch) where Source #

Runtime representation of architectures.

Constructors

X86Repr :: NatRepr w -> ArchRepr (X86 w) 

Instances

Instances details
TestEquality ArchRepr Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Arch

Methods

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

OrdF ArchRepr Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Arch

Methods

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

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

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

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

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

data LLVMSideCondition (f :: CrucibleType -> Type) Source #

Constructors

LLVMSideCondition (f BoolType) (UndefinedBehavior f) 

Instances

Instances details
OrdC LLVMSideCondition Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

compareC :: (forall (x :: k) (y :: k). f x -> g y -> OrderingF x y) -> LLVMSideCondition f -> LLVMSideCondition g -> Ordering #

TestEqualityC LLVMSideCondition Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

testEqualityC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> LLVMSideCondition f -> LLVMSideCondition f -> Bool #

FoldableF LLVMSideCondition Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

foldMapF :: Monoid m => (forall (s :: k). e s -> m) -> LLVMSideCondition e -> m #

foldrF :: (forall (s :: k). e s -> b -> b) -> b -> LLVMSideCondition e -> b #

foldlF :: (forall (s :: k). b -> e s -> b) -> b -> LLVMSideCondition e -> b #

foldrF' :: (forall (s :: k). e s -> b -> b) -> b -> LLVMSideCondition e -> b #

foldlF' :: (forall (s :: k). b -> e s -> b) -> b -> LLVMSideCondition e -> b #

toListF :: (forall (tp :: k). f tp -> a) -> LLVMSideCondition f -> [a] #

FunctorF LLVMSideCondition Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

fmapF :: (forall (x :: k). f x -> g x) -> LLVMSideCondition f -> LLVMSideCondition g #

TraversableF LLVMSideCondition Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

traverseF :: Applicative m => (forall (s :: k). e s -> m (f s)) -> LLVMSideCondition e -> m (LLVMSideCondition f) #

data LLVMExtensionExpr :: (CrucibleType -> Type) -> CrucibleType -> Type where Source #

Constructors

X86Expr :: !(ExtX86 f t) -> LLVMExtensionExpr f t 
LLVM_SideConditions :: !(GlobalVar Mem) -> !(TypeRepr tp) -> !(NonEmpty (LLVMSideCondition f)) -> !(f tp) -> LLVMExtensionExpr f tp 
LLVM_PointerExpr :: 1 <= w => !(NatRepr w) -> !(f NatType) -> !(f (BVType w)) -> LLVMExtensionExpr f (LLVMPointerType w) 
LLVM_PointerBlock :: 1 <= w => !(NatRepr w) -> !(f (LLVMPointerType w)) -> LLVMExtensionExpr f NatType 
LLVM_PointerOffset :: 1 <= w => !(NatRepr w) -> !(f (LLVMPointerType w)) -> LLVMExtensionExpr f (BVType w) 
LLVM_PointerIte :: 1 <= w => !(NatRepr w) -> !(f BoolType) -> !(f (LLVMPointerType w)) -> !(f (LLVMPointerType w)) -> LLVMExtensionExpr f (LLVMPointerType w) 

Instances

Instances details
TypeApp LLVMExtensionExpr Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

appType :: forall (f :: CrucibleType -> Type) (x :: CrucibleType). LLVMExtensionExpr f x -> TypeRepr x #

PrettyApp LLVMExtensionExpr Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

ppApp :: (forall (x :: k). f x -> Doc ann) -> forall (x :: k). LLVMExtensionExpr f x -> Doc ann #

FoldableFC LLVMExtensionExpr Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). LLVMExtensionExpr f x -> m #

foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> LLVMExtensionExpr f x -> b #

foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> LLVMExtensionExpr f x -> b #

foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> LLVMExtensionExpr f x -> b #

foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> LLVMExtensionExpr f x -> b #

toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). LLVMExtensionExpr f x -> [a] #

FunctorFC LLVMExtensionExpr Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). LLVMExtensionExpr f x -> LLVMExtensionExpr g x #

OrdFC LLVMExtensionExpr Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). LLVMExtensionExpr f x -> LLVMExtensionExpr f y -> OrderingF x y #

TestEqualityFC LLVMExtensionExpr Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). LLVMExtensionExpr f x -> LLVMExtensionExpr f y -> Maybe (x :~: y) #

TraversableFC LLVMExtensionExpr Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: l). LLVMExtensionExpr f x -> m (LLVMExtensionExpr g x) #

data LLVMStmt (f :: CrucibleType -> Type) :: CrucibleType -> Type where Source #

Extension statements for LLVM. These statements represent the operations necessary to interact with the LLVM memory model.

Constructors

LLVM_PushFrame :: !Text -> !(GlobalVar Mem) -> LLVMStmt f UnitType

Indicate the beginning of a new stack frame upon entry to a function.

LLVM_PopFrame :: !(GlobalVar Mem) -> LLVMStmt f UnitType

Indicate the end of the current stack frame upon exit from a function.

LLVM_Alloca :: HasPtrWidth wptr => !(NatRepr wptr) -> !(GlobalVar Mem) -> !(f (BVType wptr)) -> !Alignment -> !String -> LLVMStmt f (LLVMPointerType wptr)

Allocate a new memory object in the current stack frame. This memory will be automatically deallocated when the corresponding PopFrame statement is executed.

LLVM_Load :: HasPtrWidth wptr => !(GlobalVar Mem) -> !(f (LLVMPointerType wptr)) -> !(TypeRepr tp) -> !StorageType -> !Alignment -> LLVMStmt f tp

Load a value from the memory. The load is defined only if the given pointer is a live pointer; if the bytes in the memory at that location can be read and reconstructed into a value of the desired type; and if the given pointer is actually aligned according to the given alignment value.

LLVM_Store :: HasPtrWidth wptr => !(GlobalVar Mem) -> !(f (LLVMPointerType wptr)) -> !(TypeRepr tp) -> !StorageType -> !Alignment -> !(f tp) -> LLVMStmt f UnitType

Store a value in to the memory. The store is defined only if the given pointer is a live pointer; if the given value fits into the memory object at the location pointed to; and the given pointer is aligned according to the given alignment value.

LLVM_MemClear :: HasPtrWidth wptr => !(GlobalVar Mem) -> !(f (LLVMPointerType wptr)) -> !Bytes -> LLVMStmt f UnitType

Clear a region of memory by setting all the bytes in it to the zero byte. This is primarily used for initializing the value of global variables, but can also result from zero initializers.

LLVM_LoadHandle :: HasPtrWidth wptr => !(GlobalVar Mem) -> !(Maybe Type) -> !(f (LLVMPointerType wptr)) -> !(CtxRepr args) -> !(TypeRepr ret) -> LLVMStmt f (FunctionHandleType args ret)

Load the Crucible function handle that corresponds to a function pointer value. This load is defined only if the given pointer was previously allocated as a function pointer value and associated with a Crucible function handle of the expected type.

LLVM_ResolveGlobal :: HasPtrWidth wptr => !(NatRepr wptr) -> !(GlobalVar Mem) -> GlobalSymbol -> LLVMStmt f (LLVMPointerType wptr)

Resolve the given global symbol name to a pointer value.

LLVM_PtrEq :: HasPtrWidth wptr => !(GlobalVar Mem) -> !(f (LLVMPointerType wptr)) -> !(f (LLVMPointerType wptr)) -> LLVMStmt f BoolType

Test two pointer values for equality. Note! This operation is defined only in case both pointers are live or null.

LLVM_PtrLe :: HasPtrWidth wptr => !(GlobalVar Mem) -> !(f (LLVMPointerType wptr)) -> !(f (LLVMPointerType wptr)) -> LLVMStmt f BoolType

Test two pointer values for ordering. Note! This operation is only defined if both pointers are live pointers into the same memory object.

LLVM_PtrAddOffset :: HasPtrWidth wptr => !(NatRepr wptr) -> !(GlobalVar Mem) -> !(f (LLVMPointerType wptr)) -> !(f (BVType wptr)) -> LLVMStmt f (LLVMPointerType wptr)

Add an offset value to a pointer. Note! This operation is only defined if both the input pointer is a live pointer, and the resulting computed pointer remains in the bounds of its associated memory object (or one past the end).

LLVM_PtrSubtract :: HasPtrWidth wptr => !(NatRepr wptr) -> !(GlobalVar Mem) -> !(f (LLVMPointerType wptr)) -> !(f (LLVMPointerType wptr)) -> LLVMStmt f (BVType wptr)

Compute the offset between two pointer values. Note! This operation is only defined if both pointers are live pointers into the same memory object.

LLVM_Debug :: !(LLVM_Dbg f c) -> LLVMStmt f UnitType

Debug information

Instances

Instances details
TypeApp LLVMStmt Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

appType :: forall (f :: CrucibleType -> Type) (x :: CrucibleType). LLVMStmt f x -> TypeRepr x #

PrettyApp LLVMStmt Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

ppApp :: (forall (x :: k). f x -> Doc ann) -> forall (x :: k). LLVMStmt f x -> Doc ann #

FoldableFC LLVMStmt Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). LLVMStmt f x -> m #

foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> LLVMStmt f x -> b #

foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> LLVMStmt f x -> b #

foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> LLVMStmt f x -> b #

foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> LLVMStmt f x -> b #

toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). LLVMStmt f x -> [a] #

FunctorFC LLVMStmt Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). LLVMStmt f x -> LLVMStmt g x #

OrdFC LLVMStmt Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). LLVMStmt f x -> LLVMStmt f y -> OrderingF x y #

TestEqualityFC LLVMStmt Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). LLVMStmt f x -> LLVMStmt f y -> Maybe (x :~: y) #

TraversableFC LLVMStmt Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: l). LLVMStmt f x -> m (LLVMStmt g x) #

data LLVM_Dbg f c where Source #

Debug statement variants - these have no semantic meaning

Constructors

LLVM_Dbg_Addr :: HasPtrWidth wptr => !(f (LLVMPointerType wptr)) -> DILocalVariable -> DIExpression -> LLVM_Dbg f (LLVMPointerType wptr)

Annotates a value pointed to by a pointer with local-variable debug information

https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-addr

LLVM_Dbg_Declare :: HasPtrWidth wptr => !(f (LLVMPointerType wptr)) -> DILocalVariable -> DIExpression -> LLVM_Dbg f (LLVMPointerType wptr)

Annotates a value pointed to by a pointer with local-variable debug information

https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-declare

LLVM_Dbg_Value :: !(TypeRepr c) -> !(f c) -> DILocalVariable -> DIExpression -> LLVM_Dbg f c

Annotates a value with local-variable debug information

https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-value

Instances

Instances details
PrettyApp LLVM_Dbg Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

ppApp :: (forall (x :: k). f x -> Doc ann) -> forall (x :: k). LLVM_Dbg f x -> Doc ann #

FoldableFC LLVM_Dbg Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). LLVM_Dbg f x -> m #

foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> LLVM_Dbg f x -> b #

foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> LLVM_Dbg f x -> b #

foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> LLVM_Dbg f x -> b #

foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> LLVM_Dbg f x -> b #

toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). LLVM_Dbg f x -> [a] #

FunctorFC LLVM_Dbg Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). LLVM_Dbg f x -> LLVM_Dbg g x #

OrdFC LLVM_Dbg Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). LLVM_Dbg f x -> LLVM_Dbg f y -> OrderingF x y #

TestEqualityFC LLVM_Dbg Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). LLVM_Dbg f x -> LLVM_Dbg f y -> Maybe (x :~: y) #

TraversableFC LLVM_Dbg Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension.Syntax

Methods

traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: l). LLVM_Dbg f x -> m (LLVM_Dbg g x) #

traverseConds :: Applicative m => (forall s. f s -> m (g s)) -> NonEmpty (LLVMSideCondition f) -> m (NonEmpty (LLVMSideCondition g)) Source #

ppGlobalVar :: GlobalVar Mem -> Doc ann Source #

ppAlignment :: Alignment -> Doc ann Source #

data LLVM Source #

The Crucible extension type marker for LLVM.

Instances

Instances details
Data LLVM Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LLVM -> c LLVM #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LLVM #

toConstr :: LLVM -> Constr #

dataTypeOf :: LLVM -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LLVM) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LLVM) #

gmapT :: (forall b. Data b => b -> b) -> LLVM -> LLVM #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LLVM -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LLVM -> r #

gmapQ :: (forall d. Data d => d -> u) -> LLVM -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LLVM -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LLVM -> m LLVM #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LLVM -> m LLVM #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LLVM -> m LLVM #

Generic LLVM Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension

Associated Types

type Rep LLVM :: Type -> Type #

Methods

from :: LLVM -> Rep LLVM x #

to :: Rep LLVM x -> LLVM #

IsSyntaxExtension LLVM Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension

Eq LLVM Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension

Methods

(==) :: LLVM -> LLVM -> Bool #

(/=) :: LLVM -> LLVM -> Bool #

Ord LLVM Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension

Methods

compare :: LLVM -> LLVM -> Ordering #

(<) :: LLVM -> LLVM -> Bool #

(<=) :: LLVM -> LLVM -> Bool #

(>) :: LLVM -> LLVM -> Bool #

(>=) :: LLVM -> LLVM -> Bool #

max :: LLVM -> LLVM -> LLVM #

min :: LLVM -> LLVM -> LLVM #

type Rep LLVM Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension

type Rep LLVM = D1 ('MetaData "LLVM" "Lang.Crucible.LLVM.Extension" "crucible-llvm-0.6-JJ7tfvbGrbFFTkl5eJBN3H" 'False) (V1 :: Type -> Type)
type ExprExtension LLVM Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension

type ExprExtension LLVM = LLVMExtensionExpr
type StmtExtension LLVM Source # 
Instance details

Defined in Lang.Crucible.LLVM.Extension

type StmtExtension LLVM = LLVMStmt