Struct haybale_pitchfork::Config

#[non_exhaustive]
pub struct Config<'p, B> where
    B: Backend,  {
    pub loop_bound: usize,
    pub max_callstack_depth: Option<usize>,
    pub solver_query_timeout: Option<Duration>,
    pub null_pointer_checking: NullPointerChecking,
    pub concretize_memcpy_lengths: Concretize,
    pub max_memcpy_length: Option<u64>,
    pub squash_unsats: bool,
    pub trust_llvm_assumes: bool,
    pub function_hooks: FunctionHooks<'p, B>,
    pub callbacks: Callbacks<'p, B>,
    pub initial_mem_watchpoints: HashMap<String, Watchpoint, RandomState>,
    pub demangling: Option<Demangling>,
    pub print_source_info: bool,
    pub print_module_name: bool,
}

Various settings which affect how the symbolic execution is performed.

Config uses the (new-to-Rust-1.40) #[non_exhaustive] attribute to indicate that fields may be added even in a point release (that is, without incrementing the major or minor version). See here for more details.

In general, you'll want to start with Config::default() and then change the settings you want to change; #[non_exhaustive] will prevent users from constructing a Config directly.

Fields (Non-exhaustive)

Non-exhaustive structs could have additional fields added in future. Therefore, non-exhaustive structs cannot be constructed in external crates using the traditional Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.

loop_bound: usize

Maximum number of times to execute any given line of LLVM IR. This bounds both the number of iterations of loops, and also the depth of recursion. For inner loops, this bounds the number of total iterations across all invocations of the loop.

Default is 10.

max_callstack_depth: Option<usize>

Maximum callstack depth to allow when symbolically executing. If symbolic execution encounters a call which would result in a stack depth exceeding this number, and the call is not hooked (see function_hooks), then the call will simply be ignored - as if generic_stub_hook were applied to that call.

For example, if this setting is set to Some(1), and we're executing a function foo() which calls bar() which calls baz(), then the call to bar() will be fully analyzed, but fully calling baz() would result in a stack depth of 2, so instead, bar()'s call to baz() will be ignored.

As another example, the setting Some(0) means that all calls will be ignored, unless they are hooked in function_hooks.

Note that this considers the LLVM callstack depth. If calls have been inlined in the LLVM bitcode, haybale sees this as a single function, and "entering" an inlined function doesn't affect the callstack depth.

A value of None for this setting indicates no limit to the callstack depth; all calls will be fully analyzed, to the extent possible and unless overridden by function_hooks.

Default is None.

solver_query_timeout: Option<Duration>

Maximum amount of time to allow for any single solver query.

If Some, any solver query lasting longer than the given limit will be killed. This will result in an Error::SolverError for that path.

If None, there will be no time limit for solver queries.

Default is 300 seconds (5 minutes).

null_pointer_checking: NullPointerChecking

Should we check each memory access for possible NULL dereference, and if so, how should we report any errors?

Default is NullPointerChecking::Simple.

concretize_memcpy_lengths: Concretize

When encountering a memcpy, memset, or memmove with multiple possible lengths, how (if at all) should we concretize the length?

Default is Concretize::Symbolic - that is, no concretization.

max_memcpy_length: Option<u64>

Maximum supported length of a memcpy, memset, or memmove operation.

Setting this to Some(x) means that if we encounter a memcpy, memset, or memmove with length which may be greater than x bytes, we will constrain the length to be at most x bytes. (haybale will also emit a warning when doing this.) If the only possible values for the length are greater than x bytes, we will raise an error.

Setting this to None means that there is no limit to the size of these operations.

Default is None - that is, no limit.

squash_unsats: bool

Error::Unsat is an error type which is used internally, but may not be useful for ExecutionManager.next() to return to consumers. In most cases, consumers probably don't care about paths which were partially explored and resulted in an unsat error; they are probably interested in only those paths that are actually feasible, or ended in one of the other error types.

If this setting is false, the ExecutionManager will return an Error::Unsat to the consumer whenever one is encountered, just as it does for other error types. If this setting is true, paths ending in Error::Unsat will be silently ignored by the ExecutionManager, and it will move on to the next path, as if a filter were applied to the iterator.

Note that many unsat paths are never even started processing, so they never actually result in an unsat error. In fact, many executions may never encounter an unsat error, despite having unsat paths. Furthermore, haybale's behavior regarding which unsat paths actually result in an unsat error is not guaranteed to be stable, and may change even in point releases (that is, without incrementing the major or minor version).

Default is true.

trust_llvm_assumes: bool

When encountering the llvm.assume() intrinsic, should we only consider paths where the assumption holds (true), or should we also consider paths where the assumption does not hold, if that is possible (false)?

Note that you may also provide a custom hook for llvm.assume() in function_hooks. If you do, that overrides this setting.

Default is true.

function_hooks: FunctionHooks<'p, B>

The set of currently active function hooks; see FunctionHooks for more details.

Default is FunctionHooks::default(); see docs there for more details.

callbacks: Callbacks<'p, B>

The set of currently active callbacks; see Callbacks for more details.

Default is no callbacks.

initial_mem_watchpoints: HashMap<String, Watchpoint, RandomState>

The initial memory watchpoints when a State is created (mapping from watchpoint name to the actual watchpoint).

More watchpoints may be added or removed at any time with state.add_mem_watchpoint() and state.rm_mem_watchpoint().

Default is no watchpoints.

demangling: Option<Demangling>

Controls the (attempted) demangling of function names in error messages and backtraces.

If None, haybale will attempt to autodetect which mangling is appropriate, based on the LLVM metadata.

Some can be used to force haybale to attempt to demangle with a particular demangler.

Any symbol that isn't valid for the chosen demangler will simply be left unchanged, regardless of this setting.

Default is None.

print_source_info: bool

If true, then haybale will attempt to print source location info (e.g., filename, line number, column number) along with the LLVM location info in error messages and backtraces. (This applies to error messages returned by State.full_error_message_with_context().)

For this to work, the LLVM bitcode must contain debuginfo. For example, C/C++ or Rust sources must be compiled with the -g flag to clang, clang++, or rustc.

In addition, some LLVM instructions simply don't correspond to a particular source location; e.g., they may be just setting up the stack frame for a function.

For path dumps in the case of error, the value of the environment variable HAYBALE_DUMP_PATH has precedence over this setting. HAYBALE_DUMP_PATH may be set to: LLVM for a list of the LLVM basic blocks in the path; SRC for a list of the source-language locations in the path; BOTH for both of the above.

Default is true.

print_module_name: bool

If true, then haybale will include the module name along with the LLVM location info in error messages, backtraces, log messages, and when dumping paths. If false, the module name will be omitted. You may want to use false for Projects with only a single bitcode file, or if the LLVM module is clear from the function name.

Default is true.

Methods

impl<'p, B> Config<'p, B> where
    B: Backend, 

pub fn new() -> Config<'p, B>

Creates a new Config with defaults for all the options, except with no function hooks.

You may want to consider Config::default(), which comes with predefined hooks for common functions.

Trait Implementations

impl<'p, B> Clone for Config<'p, B> where
    B: Clone + Backend, 

fn clone(&self) -> Config<'p, B>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'p, B> Default for Config<'p, B> where
    B: Backend, 

fn default() -> Config<'p, B>

Default values for all configuration parameters.

In particular, this uses FunctionHooks::default(), and therefore comes with a set of predefined hooks for common functions.

For more information, see FunctionHooks::default().