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

Lang.Crucible.LLVM.Intrinsics

Contents

register_llvm_override

Description

Synopsis

data LLVM
llvmIntrinsicTypes :: IsSymInterface sym => IntrinsicTypes sym
data LLVMOverride p sym args ret = LLVMOverride {
- llvmOverride_declare :: Declare
- llvmOverride_args :: CtxRepr args
- llvmOverride_ret :: TypeRepr ret
- llvmOverride_def :: forall bak. IsSymBackend sym bak => GlobalVar Mem -> bak -> Assignment (RegEntry sym) args -> forall rtp args' ret'. OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret)
}
register_llvm_overrides :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) => Module -> [OverrideTemplate p sym arch rtp l a] -> [OverrideTemplate p sym arch rtp l a] -> LLVMContext arch -> OverrideSim p sym LLVM rtp l a ()
register_llvm_overrides_ :: LLVMContext arch -> [OverrideTemplate p sym arch rtp l a] -> [Declare] -> OverrideSim p sym LLVM rtp l a ()
llvmDeclToFunHandleRepr :: HasPtrWidth wptr => FunDecl -> (forall args ret. CtxRepr args -> TypeRepr ret -> a) -> a
data LLVMOverride p sym args ret = LLVMOverride {
- llvmOverride_declare :: Declare
- llvmOverride_args :: CtxRepr args
- llvmOverride_ret :: TypeRepr ret
- llvmOverride_def :: forall bak. IsSymBackend sym bak => GlobalVar Mem -> bak -> Assignment (RegEntry sym) args -> forall rtp args' ret'. OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret)
}
data SomeLLVMOverride p sym = forall args ret. SomeLLVMOverride (LLVMOverride p sym args ret)
type RegOverrideM p sym arch rtp l a = ReaderT (Declare, Maybe DecodedName, LLVMContext arch) (MaybeT (OverrideSim p sym LLVM rtp l a))
llvmSizeT :: HasPtrWidth wptr => Type
llvmSSizeT :: HasPtrWidth wptr => Type
data OverrideTemplate p sym arch rtp l a = OverrideTemplate {
- overrideTemplateMatcher :: TemplateMatcher
- overrideTemplateAction :: RegOverrideM p sym arch rtp l a ()
}
data TemplateMatcher
- = ExactMatch String
- | PrefixMatch String
- | SubstringsMatch [String]
callStackFromMemVar' :: GlobalVar Mem -> OverrideSim p sym ext r args ret CallStack
basic_llvm_override :: forall p args ret sym arch wptr l a rtp. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
polymorphic1_llvm_override :: forall p sym arch wptr l a rtp. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => String -> (forall w. 1 <= w => NatRepr w -> SomeLLVMOverride p sym) -> OverrideTemplate p sym arch rtp l a
build_llvm_override :: HasLLVMAnn sym => FunctionName -> CtxRepr args -> TypeRepr ret -> CtxRepr args' -> TypeRepr ret' -> (forall bak rtp' l' a'. IsSymBackend sym bak => bak -> Assignment (RegEntry sym) args -> OverrideSim p sym LLVM rtp' l' a' (RegValue sym ret)) -> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret')
register_llvm_override :: forall p args ret sym arch wptr l a rtp. (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) => LLVMOverride p sym args ret -> RegOverrideM p sym arch rtp l a ()
register_1arg_polymorphic_override :: forall p sym arch wptr l a rtp. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => String -> (forall w. 1 <= w => NatRepr w -> SomeLLVMOverride p sym) -> RegOverrideM p sym arch rtp l a ()
bind_llvm_handle :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMContext arch -> Symbol -> FnHandle args ret -> FnState p sym LLVM args ret -> OverrideSim p sym LLVM rtp l a ()
bind_llvm_func :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMContext arch -> Symbol -> Assignment TypeRepr args -> TypeRepr ret -> FnState p sym LLVM args ret -> OverrideSim p sym LLVM rtp l a ()
do_register_llvm_override :: forall p args ret sym arch wptr l a rtp. (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) => LLVMContext arch -> LLVMOverride p sym args ret -> OverrideSim p sym LLVM rtp l a ()
alloc_and_register_override :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => bak -> LLVMContext arch -> LLVMOverride p sym args ret -> [Symbol] -> OverrideSim p sym LLVM rtp l a ()
newtype IntrinsicsOptions = IntrinsicsOptions {
- abnormalExitBehavior :: AbnormalExitBehavior
}
data AbnormalExitBehavior
- = AlwaysFail
- | OnlyAssertFail
- | NeverFail
defaultIntrinsicsOptions :: IntrinsicsOptions

Documentation

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

llvmIntrinsicTypes :: IsSymInterface sym => IntrinsicTypes sym Source #

data LLVMOverride p sym args ret Source #

This type represents an implementation of an LLVM intrinsic function in Crucible.

Constructors

LLVMOverride

Fields

llvmOverride_declare :: Declare
An LLVM name and signature for this intrinsic
llvmOverride_args :: CtxRepr args
A representation of the argument types
llvmOverride_ret :: TypeRepr ret
A representation of the return type
llvmOverride_def :: forall bak. IsSymBackend sym bak => GlobalVar Mem -> bak -> Assignment (RegEntry sym) args -> forall rtp args' ret'. OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret)
The implementation of the intrinsic in the simulator monad (OverrideSim).

register_llvm_overrides Source #

Arguments

:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions)
=> Module
-> [OverrideTemplate p sym arch rtp l a]	Additional "define" overrides
-> [OverrideTemplate p sym arch rtp l a]	Additional "declare" overrides
-> LLVMContext arch
-> OverrideSim p sym LLVM rtp l a ()

Register all declare and define overrides

register_llvm_overrides_ :: LLVMContext arch -> [OverrideTemplate p sym arch rtp l a] -> [Declare] -> OverrideSim p sym LLVM rtp l a () Source #

Helper function for registering overrides

llvmDeclToFunHandleRepr :: HasPtrWidth wptr => FunDecl -> (forall args ret. CtxRepr args -> TypeRepr ret -> a) -> a Source #

Compute the function Crucible function signature that corresponds to the given LLVM function declaration.

data LLVMOverride p sym args ret Source #

This type represents an implementation of an LLVM intrinsic function in Crucible.

Constructors

LLVMOverride

Fields

llvmOverride_declare :: Declare
An LLVM name and signature for this intrinsic
llvmOverride_args :: CtxRepr args
A representation of the argument types
llvmOverride_ret :: TypeRepr ret
A representation of the return type
llvmOverride_def :: forall bak. IsSymBackend sym bak => GlobalVar Mem -> bak -> Assignment (RegEntry sym) args -> forall rtp args' ret'. OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret)
The implementation of the intrinsic in the simulator monad (OverrideSim).

data SomeLLVMOverride p sym Source #

Constructors

forall args ret. SomeLLVMOverride (LLVMOverride p sym args ret)

type RegOverrideM p sym arch rtp l a = ReaderT (Declare, Maybe DecodedName, LLVMContext arch) (MaybeT (OverrideSim p sym LLVM rtp l a)) Source #

llvmSizeT :: HasPtrWidth wptr => Type Source #

Convenient LLVM representation of the size_t type.

llvmSSizeT :: HasPtrWidth wptr => Type Source #

Convenient LLVM representation of the ssize_t type.

data OverrideTemplate p sym arch rtp l a Source #

Constructors

OverrideTemplate
Fields overrideTemplateMatcher :: TemplateMatcher overrideTemplateAction :: RegOverrideM p sym arch rtp l a ()

data TemplateMatcher Source #

This type controls whether an override is installed for a given name found in a module. See filterTemplates.

Constructors

ExactMatch String
PrefixMatch String
SubstringsMatch [String]

callStackFromMemVar' :: GlobalVar Mem -> OverrideSim p sym ext r args ret CallStack Source #

register_llvm_override

basic_llvm_override :: forall p args ret sym arch wptr l a rtp. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a Source #

polymorphic1_llvm_override :: forall p sym arch wptr l a rtp. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => String -> (forall w. 1 <= w => NatRepr w -> SomeLLVMOverride p sym) -> OverrideTemplate p sym arch rtp l a Source #

build_llvm_override :: HasLLVMAnn sym => FunctionName -> CtxRepr args -> TypeRepr ret -> CtxRepr args' -> TypeRepr ret' -> (forall bak rtp' l' a'. IsSymBackend sym bak => bak -> Assignment (RegEntry sym) args -> OverrideSim p sym LLVM rtp' l' a' (RegValue sym ret)) -> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret') Source #

Do some pipe-fitting to match a Crucible override function into the shape expected by the LLVM calling convention. This basically just coerces between values of BVType w and values of LLVMPointerType w.

register_llvm_override :: forall p args ret sym arch wptr l a rtp. (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) => LLVMOverride p sym args ret -> RegOverrideM p sym arch rtp l a () Source #

register_1arg_polymorphic_override :: forall p sym arch wptr l a rtp. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => String -> (forall w. 1 <= w => NatRepr w -> SomeLLVMOverride p sym) -> RegOverrideM p sym arch rtp l a () Source #

bind_llvm_handle :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMContext arch -> Symbol -> FnHandle args ret -> FnState p sym LLVM args ret -> OverrideSim p sym LLVM rtp l a () Source #

Bind a function handle, and also bind the function to the global function allocation in the LLVM memory.

bind_llvm_func :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMContext arch -> Symbol -> Assignment TypeRepr args -> TypeRepr ret -> FnState p sym LLVM args ret -> OverrideSim p sym LLVM rtp l a () Source #

Low-level function to register LLVM functions.

Creates and binds a function handle, and also binds the function to the global function allocation in the LLVM memory.

do_register_llvm_override :: forall p args ret sym arch wptr l a rtp. (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) => LLVMContext arch -> LLVMOverride p sym args ret -> OverrideSim p sym LLVM rtp l a () Source #

Low-level function to register LLVM overrides.

Type-checks the LLVM override against the Declare it contains, adapting its arguments and return values as necessary. Then creates and binds a function handle, and also binds the function to the global function allocation in the LLVM memory.

Useful when you don't have access to a full LLVM AST, e.g., when parsing Crucible CFGs written in crucible-syntax. For more usual cases, use register_llvm_overrides.

alloc_and_register_override Source #

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)
=> bak
-> LLVMContext arch
-> LLVMOverride p sym args ret
-> [Symbol]	Aliases
-> OverrideSim p sym LLVM rtp l a ()

Create an allocation for an override and register it.

Useful when registering an override for a function in an LLVM memory that wasn't initialized with the functions in Lang.Crucible.LLVM.Globals, e.g., when parsing Crucible CFGs written in crucible-syntax. For more usual cases, use register_llvm_overrides.

c.f. allocLLVMFunPtr

newtype IntrinsicsOptions Source #

This datatype encodes a variety of tweakable settings that to LLVM overrides.

Constructors

IntrinsicsOptions
Fields abnormalExitBehavior :: AbnormalExitBehavior Should Crucible fail when simulating a function which triggers an abnormal exit, such as `abort()`?

data AbnormalExitBehavior Source #

Should Crucible fail when simulating a function which triggers an abnormal exit, such as abort()?

Constructors

AlwaysFail	Functions which trigger an abnormal exit will always cause Crucible to fail.
OnlyAssertFail	The `__assert_fail()` function will cause Crucible to fail, while other functions which triggern an abnormal exit will not cause failures. This option is primarily useful for SV-COMP.
NeverFail	Functions which trigger an abnormal exit will never cause Crucible to fail. This option is primarily useful for SV-COMP.

Instances

Instances details

Eq AbnormalExitBehavior Source #
Instance details Defined in Lang.Crucible.LLVM.Intrinsics.Options Methods (==) :: AbnormalExitBehavior -> AbnormalExitBehavior -> Bool # (/=) :: AbnormalExitBehavior -> AbnormalExitBehavior -> Bool #

defaultIntrinsicsOptions :: IntrinsicsOptions Source #

The default translation options:

Functions which trigger an abnormal exit will always cause Crucible to fail.