Documentation

The Crucible extension type marker for LLVM.

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

This is parameterized over ext so that LLVMOverrides can more easily be reused in the context of other language extensions that are also based on the LLVM memory model, such as Macaw.

Match two sets of OverrideTemplates against the declares and defines in a Module, registering all the overrides that apply and returning them as a list.

Match a set of OverrideTemplates against a set of Declares, registering all the overrides that apply and returning them as a list.

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

Register overrides for declared-but-not-defined functions

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

This is parameterized over ext so that LLVMOverrides can more easily be reused in the context of other language extensions that are also based on the LLVM memory model, such as Macaw.

A funcion that inspects an LLVM declaration (along with some other data), and constructs an override for the declaration if it can.

Convenient LLVM representation of the size_t type.

Convenient LLVM representation of the ssize_t type.

Checking if an override applies to a given declaration happens in two "phases", corresponding to the fields of this struct.

Create an OverrideTemplate for a polymorphic LLVM override involving a vector type. For example, the llvm.vector.reduce.add.* intrinsic can be instantiated at multiple types, including:

• i32 @llvm.vector.reduce.add.v4i32(x i32)

• i64 @llvm.vector.reduce.add.v2i64(x i64)

• etc.

Note that the intrinsic can vary both by the size of the vector type (4, 2, etc.) and the size of the integer type used as the vector element type (i32, i64, etc.) Therefore, the fn argument that this function accepts is parameterized by both the vector size (vecSz) and the integer size (intSz).

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 a polymorphic LLVM override involving a vector type. (See the Haddocks for polymorphic1_vec_llvm_override for details on what this means.) This function is responsible for parsing the suffix in the intrinsic's name, which encodes the sizes of the vector and integer types. As some examples:

• .v4i32 (vector size 4, integer size 32)
• .v2i64 (vector size 2, integer size 64)

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.

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

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

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

The default translation options:

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

Check whether a TemplateMatcher matches a given function name.

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

Remove all prefixes and suffixes that might occur in a Darwin alias for a function name. See Note [Darwin aliases].