[−][src]Struct haybale::config::Config
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)
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>
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 Project
s with only a single bitcode
file, or if the LLVM module is clear from the function name.
Default is true
.
Implementations
impl<'p, B: Backend> Config<'p, B>
[src]
pub fn new() -> Self
[src]
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 + Backend> Clone for Config<'p, B>
[src]
impl<'p, B: Backend> Default for Config<'p, B>
[src]
fn default() -> Self
[src]
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()
.
Auto Trait Implementations
impl<'p, B> !RefUnwindSafe for Config<'p, B>
impl<'p, B> !Send for Config<'p, B>
impl<'p, B> !Sync for Config<'p, B>
impl<'p, B> Unpin for Config<'p, B>
impl<'p, B> !UnwindSafe for Config<'p, B>
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,