Struct haybale::State

pub struct State<'p, B: Backend> {
    pub solver: B::SolverRef,
    pub config: Config<'p, B>,
    pub proj: &'p Project,
    pub cur_loc: Location<'p>,
    /* private fields */
}

A State describes the full program state at a given moment during symbolic execution.

Fields

solver: B::SolverRef

Reference to the solver instance being used

config: Config<'p, B>

The configuration being used

proj: &'p Project

Referece to the Project being used

cur_loc: Location<'p>

Indicates the instruction which is currently being executed

Implementations

impl<'p, B> State<'p, B>where B: 'p + Backend,

pub fn new( project: &'p Project, start_loc: Location<'p>, config: Config<'p, B> ) -> Self

start_loc: the Location where the State should begin executing. As of this writing, start_loc should be the entry point of a function, or you will have problems.

pub fn fork(&self) -> Self

Fully duplicate the State. Unlike with clone(), the State this function returns will have a fully separate (fully duplicated) solver instance. (With clone(), the states will still share references to the same solver instance.)

pub fn sat(&self) -> Result<bool>

Returns true if current constraints are satisfiable, false if not.

Returns Error::SolverError if the query failed (e.g., was interrupted or timed out).

pub fn sat_with_extra_constraints<'b>( &'b self, constraints: impl IntoIterator<Item = &'b B::BV> ) -> Result<bool>

Returns true if the current constraints plus the given additional constraints are together satisfiable, or false if not.

Returns Error::SolverError if the query failed (e.g., was interrupted or timed out).

Does not permanently add the given constraints to the solver.

pub fn get_bv_by_irname<'s>( &'s self, funcname: &String, name: &Name ) -> &'s B::BV

Get the BV corresponding to the given IR Name (from the given Function name).

There should already have been a BV created for this Name on this path; this won’t attempt to create a BV if there isn’t already one for this Name.

pub fn bvs_must_be_equal(&self, a: &B::BV, b: &B::BV) -> Result<bool>

Returns true if under the current constraints, a and b must have the same value. Returns false if a and b may have different values. (If the current constraints are themselves unsatisfiable, that will result in true.)

A common use case for this function is to test whether some BV must be equal to a given concrete value. You can do this with something like state.bvs_must_be_equal(bv, &state.bv_from_u64(...)).

This function and bvs_can_be_equal() are both more efficient than get_a_solution() or get_possible_solutions()-type functions, as they do not require full model generation. You should prefer this function or bvs_can_be_equal() if they are sufficient for your needs.

pub fn bvs_can_be_equal(&self, a: &B::BV, b: &B::BV) -> Result<bool>

Returns true if under the current constraints, a and b can have the same value. Returns false if a and b cannot have the same value. (If the current constraints are themselves unsatisfiable, that will also result in false.)

A common use case for this function is to test whether some BV can be equal to a given concrete value. You can do this with something like state.bvs_can_be_equal(bv, &state.bv_from_u64(...)).

This function and bvs_must_be_equal() are both more efficient than get_a_solution() or get_possible_solutions()-type functions, as they do not require full model generation. You should prefer this function or bvs_must_be_equal() if they are sufficient for your needs.

pub fn get_a_solution_for_bv(&self, bv: &B::BV) -> Result<Option<BVSolution>>

Get one possible concrete value for the BV. Returns Ok(None) if no possible solution, or Error::SolverError if the solver query failed.

pub fn get_a_solution_for_irname( &mut self, funcname: &String, name: &Name ) -> Result<Option<BVSolution>>

Get one possible concrete value for the given IR Name (from the given Function name). Returns Ok(None) if no possible solution, or Error::SolverError if the solver query failed.

pub fn get_possible_solutions_for_bv( &self, bv: &B::BV, n: usize ) -> Result<PossibleSolutions<BVSolution>>

Get a description of the possible solutions for the BV.

n: Maximum number of distinct solutions to check for. If there are more than n possible solutions, this returns a PossibleSolutions::AtLeast containing n+1 solutions.

These solutions will be disambiguated - see docs on boolector::BVSolution.

If there are no possible solutions, this returns Ok with an empty PossibleSolutions, rather than returning an Err with Error::Unsat.

pub fn get_possible_solutions_for_irname( &mut self, funcname: &String, name: &Name, n: usize ) -> Result<PossibleSolutions<BVSolution>>

Get a description of the possible solutions for the given IR Name (from the given Function name).

n: Maximum number of distinct solutions to check for. If there are more than n possible solutions, this returns a PossibleSolutions::AtLeast containing n+1 solutions.

These solutions will be disambiguated - see docs on boolector::BVSolution.

If there are no possible solutions, this returns Ok with an empty PossibleSolutions, rather than returning an Err with Error::Unsat.

pub fn max_possible_solution_for_bv_as_u64( &self, bv: &B::BV ) -> Result<Option<u64>>

Get the maximum possible solution for the BV: that is, the highest value for which the current set of constraints is still satisfiable. “Maximum” will be interpreted in an unsigned fashion.

Returns Ok(None) if there is no solution for the BV, that is, if the current set of constraints is unsatisfiable. Only returns Err if a solver query itself fails. Panics if the BV is wider than 64 bits.

pub fn max_possible_solution_for_irname_as_u64( &mut self, funcname: &String, name: &Name ) -> Result<Option<u64>>

Get the maximum possible solution for the given IR Name (from the given Function name): that is, the highest value for which the current set of constraints is still satisfiable. “Maximum” will be interpreted in an unsigned fashion.

Returns Ok(None) if there is no solution for the BV, that is, if the current set of constraints is unsatisfiable. Only returns Err if a solver query itself fails. Panics if the BV is wider than 64 bits.

pub fn min_possible_solution_for_bv_as_u64( &self, bv: &B::BV ) -> Result<Option<u64>>

Get the minimum possible solution for the BV: that is, the lowest value for which the current set of constraints is still satisfiable. “Minimum” will be interpreted in an unsigned fashion.

Returns Ok(None) if there is no solution for the BV, that is, if the current set of constraints is unsatisfiable. Only returns Err if a solver query itself fails. Panics if the BV is wider than 64 bits.

pub fn min_possible_solution_for_irname_as_u64( &self, funcname: &String, name: &Name ) -> Result<Option<u64>>

Get the minimum possible solution for the given IR Name (from the given Function name): that is, the lowest value for which the current set of constraints is still satisfiable. “Minimum” will be interpreted in an unsigned fashion.

Returns Ok(None) if there is no solution for the BV, that is, if the current set of constraints is unsatisfiable. Only returns Err if a solver query itself fails. Panics if the BV is wider than 64 bits.

pub fn bv_from_bool(&self, b: bool) -> B::BV

Create a BV constant representing the given bool (either constant true or constant false). The resulting BV will be either constant 0 or constant 1, and will have bitwidth 1.

pub fn bv_from_i32(&self, i: i32, width: u32) -> B::BV

Create a BV representing the given constant i32 value, with the given bitwidth.

pub fn bv_from_u32(&self, u: u32, width: u32) -> B::BV

Create a BV representing the given constant u32 value, with the given bitwidth.

pub fn bv_from_i64(&self, i: i64, width: u32) -> B::BV

Create a BV representing the given constant i64 value, with the given bitwidth.

pub fn bv_from_u64(&self, u: u64, width: u32) -> B::BV

Create a BV representing the given constant u64 value, with the given bitwidth.

pub fn zero(&self, width: u32) -> B::BV

Create a BV representing the constant 0 of the given bitwidth. This is equivalent to self.bv_from_i32(0, width) but may be more efficient.

pub fn one(&self, width: u32) -> B::BV

Create a BV representing the constant 1 of the given bitwidth. This is equivalent to self.bv_from_i32(1, width) but may be more efficient.

pub fn ones(&self, width: u32) -> B::BV

Create a BV constant of the given width, where all bits are set to one. This is equivalent to self.bv_from_i32(-1, width) but may be more efficient.

pub fn new_bv_with_name(&mut self, name: Name, bits: u32) -> Result<B::BV>

Create a new (unconstrained) BV for the given Name (in the current function).

This function performs uniquing, so if you call it twice with the same Name-Function pair, you will get two different BVs.

Returns the new BV, or Err if it can’t be created.

(As of this writing, the only Err that might be returned is Error::LoopBoundExceeded, which is returned if creating the new BV would exceed max_versions_of_name – see Config.)

Also, we assume that no two Functions share the same name.

pub fn assign_bv_to_name(&mut self, name: Name, bv: B::BV) -> Result<()>

Assign the given BV to the given Name (in the current function).

This function performs uniquing, so it creates a new version of the variable represented by the (String, Name) pair rather than overwriting the current version.

Returns Err if the assignment can’t be performed.

(As of this writing, the only Err that might be returned is Error::LoopBoundExceeded, which is returned if creating the new version of the BV would exceed max_versions_of_name – see Config.)

pub fn record_bv_result( &mut self, thing: &impl HasResult, resultval: B::BV ) -> Result<()>

Record the result of thing to be resultval. Assumes thing is in the current function. Will fail with Error::LoopBoundExceeded if that would exceed max_versions_of_name (see Config).

pub fn overwrite_latest_version_of_bv(&mut self, name: &Name, bv: B::BV)

Overwrite the latest version of the given Name to instead be bv. Assumes Name is in the current function.

pub fn type_of<T: Typed + ?Sized>(&self, t: &T) -> TypeRef

Convenience function to get the Type of anything that is Typed.

pub fn operand_to_bv(&self, op: &Operand) -> Result<B::BV>

Convert an Operand to the appropriate BV. Assumes the Operand is in the current function. (All Operands should be either a constant or a variable we previously added to the state.)

pub fn const_to_bv(&self, c: &Constant) -> Result<B::BV>

Convert a Constant to the appropriate BV.

pub fn get_pointer_to_function( &self, funcname: impl Into<String> ) -> Option<&B::BV>

Get a pointer to the given function name. The name must be the fully-mangled function name, as it appears in the LLVM. The name will be resolved in the current module; this means that it will first look for a module-private (e.g., C static) definition in the current module, then search for a public definition in the same or different module. It will never return a module-private definition from a different module.

Returns None if no function was found with that name.

pub fn get_pointer_to_function_hook(&self, funcname: &str) -> Option<&B::BV>

Get a pointer to the currently active hook for the given function name.

Returns None if no function was found with that name, or if there is no currently active hook for that function.

pub fn get_func_by_name( &self, funcname: impl Into<String> ) -> Option<(&'p Function, &'p Module)>

Get a Function by name. The name must be the fully-mangled function name, as it appears in the LLVM. The name will be resolved in the current module; this means that it will first look for a module-private (e.g., C static) definition in the current module, then search for a public definition in the same or different module. It will never return a module-private definition from a different module.

Also returns the Module in which the prevailing definition of the Function was found.

Returns None if no function was found with that name.

pub fn read(&self, addr: &B::BV, bits: u32) -> Result<B::BV>

Read a value bits bits long from memory at addr. Note that bits can be arbitrarily large.

pub fn write(&mut self, addr: &B::BV, val: B::BV) -> Result<()>

Write a value into memory at addr. Note that val can be an arbitrarily large bitvector.

pub fn size_in_bits(&self, ty: &Type) -> Option<u32>

Get the size of the Type, in bits.

Accounts for the Project’s pointer size and named struct definitions.

Note that some types have size 0 bits, and this may return Some(0).

Returns None for structs which have no definition in the entire Project, or for structs/arrays/vectors where one of the elements is a struct with no definition in the entire Project.

pub fn fp_size_in_bits(fpt: FPType) -> u32

pub fn get_offset_constant_index( &self, base_type: &Type, index: usize ) -> Result<(u32, TypeRef)>

Get the offset (in bytes) of the element at the given index, as well as the Type of the element at that index.

If base_type is a NamedStructType, the struct should be defined in the current module.

pub fn get_offset_bv_index<'t, V: BV>( &self, base_type: &'t Type, index: &V, solver: V::SolverRef ) -> Result<(V, &'t Type)>

Get the offset (in bytes) of the element at the given index, as well as a reference to the Type of the element at that index.

This function differs from get_offset_constant_index in that it takes an arbitrary BV as index instead of a usize, and likewise returns its offset as a BV.

The result BV will have the same width as the input index.

pub fn add_mem_watchpoint( &mut self, name: impl Into<String>, watchpoint: Watchpoint ) -> bool

Add a memory watchpoint. It will be enabled unless/until disable_watchpoint() is called on it.

If a watchpoint with the same name was previously added, this will replace that watchpoint and return true. Otherwise, this will return false.

When any watched memory is read or written to, an INFO-level log message will be generated.

pub fn rm_mem_watchpoint(&mut self, name: &str) -> bool

Remove the memory watchpoint with the given name.

Returns true if the operation was successful, or false if no watchpoint with that name was found.

pub fn disable_watchpoint(&mut self, name: &str) -> bool

Disable the memory watchpoint with the given name. Disabled watchpoints will not generate any log messages unless/until enable_watchpoint() is called on them.

Returns true if the operation is successful, or false if no watchpoint with that name was found. Disabling an already-disabled watchpoint will have no effect and will return true.

pub fn enable_watchpoint(&mut self, name: &str) -> bool

Enable the memory watchpoint(s) with the given name.

Returns true if the operation is successful, or false if no watchpoint with that name was found. Enabling an already-enabled watchpoint will have no effect and will return true.

pub fn allocate(&mut self, bits: impl Into<u64>) -> B::BV

Allocate a value of size bits; return a pointer to the newly allocated object

pub fn get_allocation_size(&mut self, addr: &B::BV) -> Result<Option<u64>>

Get the size, in bits, of the allocation at the given address, or None if that address is not the result of an alloc().

pub fn record_path_entry(&mut self)

Record the current location as a PathEntry in the current path.

pub fn get_path(&self) -> &Vec<PathEntry<'p>>

Get the PathEntrys that have been recorded, in order

pub fn push_callsite(&mut self, call: &'p Call)

Record entering a normal Call at the current location

pub fn push_invokesite(&mut self, invoke: &'p Invoke)

Record entering the given Invoke at the current location

pub fn pop_callsite(&mut self) -> Option<Callsite<'p>>

Record leaving the current function. Returns the Callsite at which the current function was called, or None if the current function was the top-level function.

Also restores the caller’s local variables.

pub fn current_callstack_depth(&self) -> usize

Returns the current callstack depth. 0 indicates we’re in the toplevel function, 1 indicates we’re in a function directly called by the toplevel function, etc.

pub fn save_backtracking_point(&mut self, bb_to_enter: &Name, constraint: B::BV)

Save the current state, about to enter the BasicBlock with the given Name (which must be in the same Module and Function as state.cur_loc), as a backtracking point. The constraint will be added only if we end up backtracking to this point, and only then.

pub fn revert_to_backtracking_point(&mut self) -> Result<bool>

returns Ok(true) if the operation was successful, Ok(false) if there are no saved backtracking points, or Err for other errors

pub fn count_backtracking_points(&self) -> usize

returns the number of saved backtracking points

pub fn pretty_backtrace(&self) -> String

returns a String containing a formatted view of the current backtrace (in terms of LLVM locations, and possibly also source locations depending on the Config)

pub fn pretty_path_llvm(&self) -> String

returns a String containing a formatted view of the full path which led to this point, in terms of LLVM locations

pub fn pretty_path_llvm_instructions(&self) -> String

returns a String containing a formatted view of the full path which led to this point, in terms of LLVM IR instructions. If the Path includes any hooked functions, the instructions which might be contained within those functions are not included.

pub fn pretty_path_source(&self) -> String

returns a String containing a formatted view of the full path which led to this point, in terms of source locations

pub fn pretty_path_interleaved(&self) -> String

returns a String containing a formatted view of the full path which led to this point, in terms of both LLVM and source locations (interleaved appropriately)

pub fn get_path_length(&self) -> usize

Returns the number of LLVM instructions in the current path. The returned value is only accurate if the path under analysis does not include a panic, exception, exit, or any hooked calls (such as inline assembly).

pub fn demangle(&self, funcname: &str) -> String

Attempt to demangle the given funcname as appropriate based on the Config.

If this fails to demangle funcname, it just returns a copy of funcname unchanged.

pub fn all_vars_in_cur_fn(&self) -> impl Iterator<Item = (&Name, &B::BV)>

Get the most recent BV created for each Name in the current function. Returns pairs of the Name and the BV assigned to that Name.

Returned pairs will be sorted by Name.

pub fn current_assignments_as_pretty_string(&self) -> Result<String>

returns a String describing a set of satisfying assignments for all variables

pub fn full_error_message_with_context(&self, e: Error) -> String

Returns a String describing both the error and the context in which it occurred (backtrace, full path to error, variable values at the point of error, etc). Exactly which information is included is partially dependent on the environment variables HAYBALE_DUMP_PATH and HAYBALE_DUMP_VARS, as explained in the message.

Trait Implementations

impl<'p, B: Clone + Backend> Clone for State<'p, B>where B::SolverRef: Clone, B::BV: Clone, B::Memory: Clone,

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

Returns a copy of the value.

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

Performs copy-assignment from source.