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. There are internal pre-determined overrides that will be applied, as well as any additional overrides supplied by the user (internal overrides will supercede user overrides).

The "define" overrides are applied to *both* the Defines and Declares elements found within a module.

The "declare" overrides are applied only to the Declares found within a module. The intent is that these overrides should only apply to Declares, whereas the "define" overrides should apply to any matching symbol in the LLVM Module.

If both lists specify an override that matches a declare, the declare override takes precedence over the define override.

Match a set of OverrideTemplates against a provided set of definitions and declarations, registering all the overrides that apply and returning them as a pair of lists: the registered definition overrides and the registered declaration overrides.

This is an alternative entrypoint for registering overrides. The functionality here is largely the same as register_llvm_overrides except the list of declares and defines are provided manually by the caller instead of being extracted from the LLVM Module.

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.

Map llvmOverride_decl inside a SomeLLVMOverride.

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

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.

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