Symbolic execution of LLVM IR with an engine written in Rust

UCSD PLSysSec

Last update: Jan 1, 2023

Related tags

Security tools haybale

Overview

`haybale`: Symbolic execution of LLVM IR, written in Rust

haybale is a general-purpose symbolic execution engine written in Rust. It operates on LLVM IR, which allows it to analyze programs written in C/C++, Rust, Swift, or any other language which compiles to LLVM IR. In this way, it may be compared to KLEE, as it has similar goals, except that haybale is written in Rust and makes some different design decisions. That said, haybale makes no claim of being at feature parity with KLEE.

Okay, but what is a symbolic execution engine?

A symbolic execution engine is a way of reasoning - rigorously and mathematically - about the behavior of a function or program. It can reason about all possible inputs to a function without literally brute-forcing every single one. For instance, a symbolic execution engine like haybale can answer questions like:

Are there any inputs to (some function) that cause it to return 0? What are they?
Is it possible for this loop to execute exactly 17 times?
Can this pointer ever be NULL?

Symbolic execution engines answer these questions by converting each variable in the program or function into a mathematical expression which depends on the function or program inputs. Then they use an SMT solver to answer questions about these expressions, such as the questions listed above.

Getting started

1. Install

haybale is on crates.io, so you can simply add it as a dependency in your Cargo.toml, selecting the feature corresponding to the LLVM version you want:

[dependencies]
haybale = { version = "0.7.1", features = ["llvm-13"] }

Currently, the supported LLVM versions are llvm-9, llvm-10, llvm-11, llvm-12, and llvm-13.

haybale depends (indirectly) on the LLVM and Boolector libraries.

LLVM must be available on your system, in the version which matches the selected feature. (For instance, if you select the llvm-13 feature, LLVM 13 must be available on your system.) For more details and instructions on installing LLVM and making sure Cargo can find it, see the llvm-sys README.
For Boolector you have two options:
- You can compile and install Boolector 3.2.1 on your system as a shared library. (Make sure you configure it as a shared library, e.g., using ./configure.sh --shared, and install it, using make install.)
- Or, you can enable the haybale feature vendor-boolector. With this option, Cargo will automatically download and build Boolector and statically link to it. E.g.,
```
[dependencies]
haybale = { version = "0.7.1", features = ["llvm-13", "vendor-boolector"] }
```
  This option probably only works on Linux and macOS, and requires standard build tools to be available on your system -- e.g., for Debian-based distributions, build-essential, cmake, curl, and git.

2. Acquire bitcode to analyze

Since haybale operates on LLVM bitcode, you'll need some bitcode to get started. If the program or function you want to analyze is written in C, you can generate LLVM bitcode (*.bc files) with clang's -c and -emit-llvm flags:

clang -c -emit-llvm source.c -o source.bc

For debugging purposes, you may also want LLVM text-format (*.ll) files, which you can generate with clang's -S and -emit-llvm flags:

clang -S -emit-llvm source.c -o source.ll

If the program or function you want to analyze is written in Rust, you can likewise use rustc's --emit=llvm-bc and --emit=llvm-ir flags.

Note that in order for haybale to print source-location information (e.g., source filename and line number) in error messages and backtraces, the LLVM bitcode will need to include debuginfo. You can ensure debuginfo is included by passing the -g flag to clang, clang++, or rustc when generating bitcode.

3. Create a Project

A haybale Project contains all of the code currently being analyzed, which may be one or more LLVM modules. To get started, simply create a Project from a single bitcode file:

let project = Project::from_bc_path("/path/to/file.bc")?;

For more ways to create Projects, including analyzing entire libraries, see the Project documentation.

4. Use built-in analyses

haybale currently includes two simple built-in analyses: get_possible_return_values_of_func(), which describes all the possible values a function could return for any input, and find_zero_of_func(), which finds a set of inputs to a function such that it returns 0. These analyses are provided both because they may be of some use themselves, but also because they illustrate how to use haybale.

For an introductory example, let's suppose foo is the following C function:

int foo(int a, int b) {
    if (a > b) {
        return (a-1) * (b-1);
    } else {
        return (a + b) % 3 + 10;
    }
}

We can use find_zero_of_func() to find inputs such that foo will return 0:

match find_zero_of_func("foo", &project, Config::default(), None) {
    Ok(None) => println!("foo can never return 0"),
    Ok(Some(inputs)) => println!("Inputs for which foo returns 0: {:?}", inputs),
    Err(e) => panic!("{}", e),  // use the pretty Display impl for errors
}

Writing custom analyses

haybale can do much more than just describe possible function return values and find function zeroes. In this section, we'll walk through how we could find a zero of the function foo above without using the built-in find_zero_of_func(). This will illustrate how to write a custom analysis using haybale.

ExecutionManager

All analyses will use an ExecutionManager to control the progress of the symbolic execution. In the code snippet below, we call symex_function() to create an ExecutionManager which will analyze the function foo - it will start at the top of the function, and end when the function returns. In between, it will also analyze any functions called by foo, as necessary and depending on the Config settings.

let mut em = symex_function("foo", &project, Config::<DefaultBackend>::default(), None);

Here it was necessary to not only specify the default haybale configuration, as we did when calling find_zero_of_func(), but also what "backend" we want to use. The DefaultBackend should be fine for most purposes.

Paths

The ExecutionManager acts like an Iterator over paths through the function foo. Each path is one possible sequence of control-flow decisions (e.g., which direction do we take at each if statement) leading to the function returning some value. The function foo in this example has two paths, one following the "true" branch and one following the "false" branch of the if.

Let's examine the first path through the function:

let result = em.next().expect("Expected at least one path");

In the common case, result contains the function return value on this path, as a Boolector BV (bitvector) wrapped in the ReturnValue enum. Since we know that foo isn't a void-typed function (and won't throw an exception or abort), we can simply unwrap the ReturnValue to get the BV:

let retval = match result {
    Ok(ReturnValue::Return(r)) => r,
    Ok(ReturnValue::ReturnVoid) => panic!("Function shouldn't return void"),
    Ok(ReturnValue::Throw(_)) => panic!("Function shouldn't throw an exception"),
    Ok(ReturnValue::Abort) => panic!("Function shouldn't panic or exit()"),
    ...

result could also be an Err describing an Error which was encountered while processing the path. In this case, we could just ignore the error and keep calling next() to try to find paths which didn't have errors. Or we could get information about the error like this:

    ...
    Err(e) => panic!("{}", em.state().full_error_message_with_context(e)),
};

This gets information about the error from the program State, which we'll discuss next. But for the rest of this tutorial, we'll assume that we got the Ok result, and at this point retval is a BV representing the function return value on the first path.

States

For each path, the ExecutionManager provides not only the final result of the path (either aReturnValue or an Error), but also the final program State at the end of that path. We can get immutable access to the State with state(), or mutable access with mut_state().

let state = em.mut_state();  // the final program state along this path

To test whether retval can be equal to 0 in this State, we can use state.bvs_can_be_equal():

let zero = state.zero(32);  // The 32-bit constant 0
if state.bvs_can_be_equal(&retval, &zero)? {
    println!("retval can be 0!");
}

Getting solutions for variables

If retval can be 0, let's find what values of the function parameters would cause that. First, we'll add a constraint to the State requiring that the return value must be 0:

retval._eq(&zero).assert();

and then we'll ask for solutions for each of the parameters, given this constraint:

// Get a possible solution for the first parameter.
// In this case, from looking at the text-format LLVM IR, we know the variable
// we're looking for is variable #0 in the function "foo".
let a = state.get_a_solution_for_irname(&String::from("foo"), Name::from(0))?
    .expect("Expected there to be a solution")
    .as_u64()
    .expect("Expected solution to fit in 64 bits");

// Likewise the second parameter, which is variable #1 in "foo"
let b = state.get_a_solution_for_irname(&String::from("foo"), Name::from(1))?
    .expect("Expected there to be a solution")
    .as_u64()
    .expect("Expected solution to fit in 64 bits");

println!("Parameter values for which foo returns 0: a = {}, b = {}", a, b);

Alternately, we could also have gotten the parameter BVs from the ExecutionManager like this:

let a_bv = em.param_bvs()[0].clone();
let b_bv = em.param_bvs()[1].clone();

let a = em.state().get_a_solution_for_bv(&a_bv)?
    .expect("Expected there to be a solution")
    .as_u64()
    .expect("Expected solution to fit in 64 bits");

let b = em.state().get_a_solution_for_bv(&b_bv)?
    .expect("Expected there to be a solution")
    .as_u64()
    .expect("Expected solution to fit in 64 bits");

println!("Parameter values for which foo returns 0: a = {}, b = {}", a, b);

Documentation

Full documentation for haybale can be found on docs.rs, or of course you can generate local documentation with cargo doc --open.

Compatibility

Currently, the official crates.io releases of haybale (0.7.0 and later) depend on Boolector 3.2.1 and LLVM 9, 10, 11, 12, or 13, selected via feature flags llvm-9 through llvm-13. As of this writing, choosing an LLVM version has essentially no effect on haybale's features or interface; the only difference is the ability to analyze bitcode generated with newer LLVMs. (And the LLVM 10+ versions can process AtomicRMW instructions; see #12.)

For LLVM 8, you can try the llvm-8 branch of this repo. This branch is unmaintained, and is approximately at feature parity with haybale 0.2.1. It may work for your purposes; or you can update to LLVM 9 or later and the latest haybale.

LLVM 7 and earlier are not supported.

haybale works on stable Rust, and requires Rust 1.45 or later.

Under the hood

haybale is built using the Rust llvm-ir crate and the Boolector SMT solver (via the Rust boolector crate).

Changelog

Version 0.7.1 (Oct 21, 2021)

Support for LLVM 13 via the llvm-13 feature
haybale now requires Rust 1.45+ (previously 1.43 or 1.44)

Version 0.7.0 (Aug 26, 2021)

Support for LLVM 12 via the llvm-12 feature
New Cargo feature to vendor Boolector: automatically download, build, and statically link Boolector as part of the haybale build process. See the "Install" section of the README above.
symex_function() now takes an additional argument params. You can use this argument to specify constraints for the function parameters, or even specify specific hardcoded values. Or, you can just pass None and get the previous haybale behavior, treating all parameters as completely unconstrained.
find_zero_of_func() and get_possible_return_values_of_func() likewise now take a params argument to specify constraints on function parameters.
State has a new public field proj providing access to the Project.
Function hooks no longer take a Project parameter explicitly. Instead, you can access the Project through the proj field of the State object.
ExecutionManager has a new public method .func() which provides access to the toplevel Function.
State has a new public method get_path_length(), also available as the toplevel function get_path_length().
Updated llvm-ir dependency to 0.8.0, which results in minor breaking changes to parts of haybale's API, where llvm-ir types are exposed.

Version 0.6.4 (Apr 22, 2021)

Fix the build with Rust 1.51+ (#16). (Minimum Rust version for haybale remains unchanged: 1.43+ for LLVM 9 or 10 users, or 1.44+ for LLVM 11 users.)

Version 0.6.3 (Oct 26, 2020)

Fix the documentation build on docs.rs (#13)

Version 0.6.2 (Oct 20, 2020)

Support for LLVM 11 via the llvm-11 feature
get_possible_return_values_of_func() now handles void functions properly (#10)
Support LLVM atomicrmw instructions (only for LLVM 10+) (#12)
Support LLVM freeze instructions (which only exist in LLVM 10+)
Built-in support for a few more Rust standard-library functions related to panic handling
State has a new public method get_bv_by_irname()
LLVM 11 users need Rust 1.44+, due to requirements of llvm-ir. LLVM 9 or 10 users still need only Rust 1.43+.

Version 0.6.1 (Sep 17, 2020)

Both State and Project now have a method size_in_bits() which gets the size of any Type in bits, accounting for the Project's pointer size and struct definitions. This is intended to replace state.size() and state.size_opaque_aware(), both of which are now deprecated and will be removed in haybale 0.7.0. Likewise, state.fp_size() was deprecated and renamed to state.fp_size_in_bits().
- Note: these deprecated methods were actually removed in 0.7.1.

Version 0.6.0 (Sep 1, 2020)

haybale now supports both LLVM 9 and LLVM 10, using the same branch and same crates.io releases. When using haybale, you must choose either the llvm-9 or the llvm-10 feature.
Updated llvm-ir dependency to 0.7.1 (from 0.6.0), which includes runtime and memory-usage performance improvements, particularly for large bitcode files. This also involves a few breaking changes to parts of haybale's API.
haybale now requires Rust 1.43+ (previously 1.40+) due to requirements of llvm-ir 0.7.1.

Version 0.5.1 (Aug 31, 2020)

Fix for issue #9 regarding zero-element arrays (which particularly may appear when analyzing Rust code)
Built-in support for the llvm.ctlz and llvm.cttz intrinsics

Version 0.5.0 (Jul 29, 2020)

Compatibility:

haybale now depends on LLVM 10 by default (up from LLVM 9). LLVM 9 is still supported on a separate branch; see "Compatibility" above.
Updated boolector dependency to crate version 0.4.0, which requires Boolector version 3.2.1 (up from 3.1.0).

Renames which affect the public API:

Rename SimpleMemoryBackend to DefaultBackend and make it default. Rename BtorBackend to CellMemoryBackend, and the memory module to cell_memory.
Remove the layout module. Its functions are now available as methods on State. Also, many of these functions now return u32 instead of usize.

32-bit targets and related changes:

With DefaultBackend, haybale now supports LLVM bitcode which was compiled for 32-bit targets (previously only supported 64-bit targets).
The new_uninitialized() and new_zero_initialized() methods on the backend::Memory trait, simple_memory::Memory, and cell_memory::Memory now take an additional parameter indicating the pointer size.
Project has a new public method pointer_size_bits().

Other:

Built-in support for the llvm.expect intrinsic, and built-in support for the llvm.bswap intrinsic with vector operands (previously only supported scalar operands)
solver_utils::PossibleSolutions has new constructors empty(), exactly_one(), and exactly_two() (useful for testing), and also implements FromIterator, allowing you to .collect() an iterator into it
Bugfix for the {min,max}_possible_solution_for_bv_as_binary_str() functions in the solver_utils module

Version 0.4.0 (Mar 31, 2020)

New features:

Support LLVM cmpxchg instructions
Support for instruction callbacks - see Config.callbacks. This allows you to take arbitrary actions based on the instruction about to be processed.

Config:

Config.null_detection has been renamed to Config.null_pointer_checking, and its type has been changed to allow for additional options.
Config::new() now takes no parameters. It is now the same as Config::default() except that it comes with no function hooks.

Other utility functions/methods:

The hook_utils module now includes two new functions memset_bv and memcpy_bv.
layout::size_opaque_aware now returns an Option rather than panicking.
The to_string_* methods on Location are now public, rather than internal to the crate, allowing users more control over the String representation of a Location.

Error handling:

Error has three new variants UnreachableInstruction, FailedToResolveFunctionPointer, and HookReturnValueMismatch. All of these were previously reported as Error::OtherError, but now have dedicated variants.
Error::LoopBoundExceeded now also includes the value of the loop bound which was exceeded.

Other notes:

haybale no longer selects features of the log crate. This allows downstream users to select these features or not, and in particular, allows users to enable debug logging in release builds.

Version 0.3.2 (Feb 28, 2020)

New option Config.max_callstack_depth allows you to limit the callstack depth for an analysis - automatically ignoring calls of LLVM functions which would exceed that callstack depth. The default for this setting is no limit, matching the previous behavior of haybale.
New option Config.max_memcpy_length allows you to limit the maximum size of memcpy, memset, and memmove operations. The default for this setting is no limit, matching the previous behavior of haybale.
New method FunctionHooks::add_default_hook() allows you to supply a "default hook" which will be used when no other definition or hook is found for a function call. If no default hook is provided, this will result in a FunctionNotFound error, just as it did previously.
Performance improvements for analyzing calls of function pointers.
Improved a few error messages.

Version 0.3.1 (Feb 5, 2020)

Fix some broken links in the README and docs. No functional changes.

Version 0.3.0 (Feb 5, 2020)

Solver timeouts:

New setting Config.solver_query_timeout controls the maximum amount of time haybale will spend on a single solver query before returning Error::SolverError. This setting defaults to 300 seconds (5 minutes). The setting can also be disabled entirely, which results in the same behavior as previous versions of haybale (no time limit on solver queries).

Error handling:

The errors returned by ExecutionManager.next() are now haybale::Errors instead of Strings, allowing callers to more easily handle different kinds of errors different ways. To get a string representation of the Error, .to_string() gives the short description, while State.full_error_message_with_context() gives the full description which previously was returned by ExecutionManager.next(). The usage example in the README has been updated accordingly.
The toplevel function find_zero_of_func() now returns a Result, with the error type being String.
New setting Config.squash_unsats controls whether Error::Unsats are silently squashed (the default behavior, and the behavior of previous versions of haybale), or returned to the user. For more details, see the docs on that setting.

Logging, error messages, backtraces, etc:

haybale now prints source-location information (e.g., source filename and line number) in error messages and backtraces when it is available. Similarly, the HAYBALE_DUMP_PATH environment variable now has the options LLVM, SRC, and BOTH. For more details on all of this, see Config.print_source_info.
You can also now disable printing the LLVM module name along with LLVM location info in error messages, backtraces, path dumps, and log messages. For more details, see Config.print_module_name.
haybale will now by default autodetect when C++ or Rust demangling is appropriate for the Project, unless a different setting is chosen in Config.demangling.
Numeric constants representing BV values in log messages, HAYBALE_DUMP_VARS dumps, etc are now all printed in hexadecimal (previously binary, or an inconsistent mix of binary and hexadecimal).

Function hooks and intrinsics:

Built-in support for LLVM arithmetic-with-overflow intrinsics.
Built-in support for LLVM saturating-arithmetic intrinsics.
Built-in support for the llvm.assume intrinsic, with an associated setting Config.trust_llvm_assumes.
Built-in support for the llvm.bswap intrinsic with argument sizes 48 or 64 bits (previously only supported 16 or 32 bits).
Default hooks for a number of Rust standard-library functions which always panic, such as core::result::unwrap_failed().
New module hook_utils contains the implementations of memset and memcpy used by the corresponding built-in hooks. These are now publically available for use in custom hooks for other functions.

Changes to data structures and traits:

The Location and PathEntry structs have been refactored to include source-location information when it is available, to be capable of indicating basic block terminators in addition to normal instructions, and to support some internal refactoring.
The backend::BV trait has a new required method, get_solver(), which returns a SolverRef of the appropriate type. (This is similar to the same method on the backend::Memory trait.)
Saturating-arithmetic methods (signed and unsigned addition and subtraction) are now available on backend::BV, with default implementations in terms of the other trait methods. That means that these come "for free" once the required trait methods are implemented.
zero_extend_to_bits() and sign_extend_to_bits() are also now available as trait methods on backend::BV, with default implementations in terms of the other trait methods. Previously they were private utility functions in haybale.
Many other structures have had minor changes and improvements, including some small breaking changes.

Compatibility:

Updated boolector dependency to crate version 0.3.0, which requires Boolector version 3.1.0 (up from 3.0.0).
This version of haybale now requires Rust 1.40+, up from 1.36+ for previous versions of haybale.

Version 0.2.1 (Jan 15, 2020)

New HAYBALE_DUMP_PATH and HAYBALE_DUMP_VARS environment-variable options
- HAYBALE_DUMP_PATH: if set to 1, then on error, haybale will print a description of the path to the error: every LLVM basic block touched from the top of the function until the error location, in order.
- HAYBALE_DUMP_VARS: if set to 1, then on error, haybale will print the latest value assigned to each variable in the function containing the error.
New setting Config.demangling allows you to apply C++ or Rust demangling to function names in error messages and backtraces
Support hooking calls to inline assembly, with some limitations inherited from llvm-ir (see comments on FunctionHooks::add_inline_asm_hook())
Built-in support for (the most common cases of) the llvm.bswap intrinsic
Other tiny tweaks - e.g., downgrade one panic to a warning

Version 0.2.0 (Jan 8, 2020)

Support LLVM extractvalue and insertvalue instructions
Support LLVM invoke, resume, and landingpad instructions, and thus C++ throw/catch. Also provide built-in hooks for some related C++ ABI functions such as __cxa_throw(). This support isn't perfect, particularly surrounding the matching of catch blocks to exceptions: haybale may explore some additional paths which aren't actually valid. But all actually valid paths should be found and explored correctly.
Since functions can be called not only with the LLVM call instruction but also with the LLVM invoke instruction, function hooks now receive a &dyn IsCall object which may represent either a call or invoke instruction.
haybale now uses LLVM 9 rather than LLVM 8. See the "Compatibility" section in the README.
Improvements for Projects containing C++ and/or Rust code:
- For the function-name arguments to symex_function(), get_possible_return_values_of_func(), find_zero_of_func(), and Project::get_func_by_name(), you may now pass either the (mangled) function name as it appears in LLVM (as was supported previously), or the demangled function name. That is, you can pass in "foo::bar" rather than "_ZN3foo3barE".
- Likewise, you may add function hooks based on the demangled name of the hooked function. See FunctionHooks::add_cpp_demangled() and FunctionHooks::add_rust_demangled().
- Also, llvm-ir versions 0.3.3 and later contain an important bugfix for parsing LLVM bitcode generated by rustc. haybale 0.2.0 uses llvm-ir 0.4.1.
The ReturnValue enum now has additional options Throw, indicating an uncaught exception, and Abort, indicating a program abort (e.g. Rust panic, or call to C exit()).
Relatedly, haybale now has built-in hooks for the C exit() function and for Rust panics (and for a few more LLVM intrinsics).
haybale also now contains a built-in generic_stub_hook and abort_hook which you can supply as hooks for any functions which you want to ignore the implementation of, or which always abort, respectively. See docs on the function_hooks module.
Config.initial_mem_watchpoints is now a HashMap instead of a HashSet of pairs.

Version 0.1.3 (Jan 1, 2020)

Memory watchpoints: specify a range of memory addresses, and get a log message for any memory operation which reads or writes any data in that range. See State::add_mem_watchpoint().
Convenience methods on State for constructing constant-valued BVs (rather than having to use the corresponding methods on BV and pass state.solver): bv_from_i32(), bv_from_u32(), bv_from_i64(), bv_from_u64(), bv_from_bool(), zero(), one(), and ones().
Some internal code refactoring to prepare for 0.2.0 features

Version 0.1.2 (Dec 18, 2019)

New method Project::get_inner_struct_type_from_named() which handles opaque struct types by searching the entire Project for a definition of the given struct
Support memory reads of size 1-7 bits (in particular, reads of LLVM i1)
Performance optimization: during State initialization, global variables are now only allocated, and not initialized until first use (lazy initialization). This gives the SMT solver fewer memory writes to think about, and helps especially for large Projects which may contain many global variables that won't actually be used in a given analysis.
Minor bugfixes and improved error messages

Version 0.1.1 (Nov 26, 2019)

Changes to README text only; no functional changes.

Version 0.1.0 (Nov 25, 2019)

Initial release!

Comments

Viewing path through non-inlined function in another crate

Hi,

I have been using execution_manager.state().get_path() to parse the instruction path taken by a single symbolic execution of a function. However, I have found that if a function includes cross-crate function calls (even if the crates are in the same workspace), that the execution within the function is not included in the returned path. Is there a way to view the path taken through a function in a different crate from the function being analyzed?

I have found that marking the function as #[inline(always)] works, but I do not want to have this requirement.

Here is some example code to illustrate my issue.

File being analyzed:

use othercrate::not_inlined;

#[no_mangle]
fn two_paths(a: u8) -> u8 {
    if a < 25 {
        a + 3
    } else {
        let mut tmp = a + 2;
        tmp *= 3;
        not_inlined(tmp - 7)
    }
}

Function defined in another crate:

#[inline(never)]
pub fn not_inlined(input: u8) -> u8 {
    let mut input = input;
    let mut iterations = 0;
    while input != 0 {
        iterations += 1;
        input = if input % 4 == 1 {
            (input + 4) % 3
        } else if input % 3 == 2 {
            (input + 2) % 5
        } else {
            (input + 3) % 7
        };
    }
    iterations
}

Haybale code:

/// Print all LLVM IR instructions in a given symbolic execution
pub fn print_instrs<'p>(path: &Vec<PathEntry<'p>>) {
    for entry in path {
        let location = &entry.0;
        match location.instr {
            BBInstrIndex::Instr(idx) => {
                for instr in location.bb.instrs.iter().skip(idx) {
                    println!("instruction: {:?}", instr);
                }
            }
            BBInstrIndex::Terminator => println!("Terminator."),
        }
    }
}


fn main() -> Result<(), String> {
    //...
    let project = Project::from_bc_path(&path)?;
    let mut em: ExecutionManager<BtorBackend> = symex_function(funcname, project, config);
    em.next();
    let state = em.state();
    print_instrs(state.get_path());

If I run this as written with not_inlined() in another crate, the output is as follows:

instruction: ICmp(ICmp { predicate: ULT, operand0: LocalOperand { name: Name("a"), ty: IntegerType { bits: 8 } }, operand1: ConstantOperand(Int { bits: 8, value: 25 }), dest: Name("_2"), debugloc: None })
instruction: Mul(Mul { operand0: LocalOperand { name: Name("a"), ty: IntegerType { bits: 8 } }, operand1: ConstantOperand(Int { bits: 8, value: 3 }), dest: Number(0), debugloc: None })
instruction: Add(Add { operand0: LocalOperand { name: Number(0), ty: IntegerType { bits: 8 } }, operand1: ConstantOperand(Int { bits: 8, value: 255 }), dest: Name("_7"), debugloc: None })
instruction: Call(Call { function: Right(ConstantOperand(GlobalReference { name: Name("_ZN3tmp5stuff12not_too_long17h9dcf6846dc92353cE"), ty: FuncType { result_type: IntegerType { bits: 8 }, param_types: [IntegerType { bits: 8 }], is_var_arg: false } })), arguments: [(LocalOperand { name: Name("_7"), ty: IntegerType { bits: 8 } }, [])], return_attributes: [], dest: Some(Number(1)), function_attributes: [], is_tail_call: true, calling_convention: C, debugloc: None })

As you can see, there are no instructions after the function call. However if I move the code to a file in the same crate as two_paths(), this is the (truncated) output:

instruction: ICmp(ICmp { predicate: ULT, operand0: LocalOperand { name: Name("a"), ty: IntegerType { bits: 8 } }, operand1: ConstantOperand(Int { bits: 8, value: 25 }), dest: Name("_2"), debugloc: None })
instruction: Mul(Mul { operand0: LocalOperand { name: Name("a"), ty: IntegerType { bits: 8 } }, operand1: ConstantOperand(Int { bits: 8, value: 3 }), dest: Number(0), debugloc: None })
instruction: Add(Add { operand0: LocalOperand { name: Number(0), ty: IntegerType { bits: 8 } }, operand1: ConstantOperand(Int { bits: 8, value: 255 }), dest: Name("_7"), debugloc: None })
instruction: Call(Call { function: Right(ConstantOperand(GlobalReference { name: Name("_ZN12haybale_test5stuff11not_inlined17hf8de0e1e8ce05140E"), ty: FuncType { result_type: IntegerType { bits: 8 }, param_types: [IntegerType { bits: 8 }], is_var_arg: false } })), arguments: [(LocalOperand { name: Name("_7"), ty: IntegerType { bits: 8 } }, [])], return_attributes: [], dest: Some(Number(1)), function_attributes: [], is_tail_call: true, calling_convention: Fast, debugloc: None })
instruction: ICmp(ICmp { predicate: EQ, operand0: LocalOperand { name: Name("input"), ty: IntegerType { bits: 8 } }, operand1: ConstantOperand(Int { bits: 8, value: 0 }), dest: Name("_45"), debugloc: None })
instruction: Phi(Phi { incoming_values: [(LocalOperand { name: Number(1), ty: IntegerType { bits: 8 } }, Name("bb9")), (LocalOperand { name: Name("input"), ty: IntegerType { bits: 8 } }, Name("start"))], dest: Name("input1.07"), to_type: IntegerType { bits: 8 }, debugloc: None })
instruction: Phi(Phi { incoming_values: [(LocalOperand { name: Number(0), ty: IntegerType { bits: 8 } }, Name("bb9")), (ConstantOperand(Int { bits: 8, value: 0 }), Name("start"))], dest: Name("iterations.06"), to_type: IntegerType { bits: 8 }, debugloc: None })
instruction: Add(Add { operand0: LocalOperand { name: Name("iterations.06"), ty: IntegerType { bits: 8 } }, operand1: ConstantOperand(Int { bits: 8, value: 1 }), dest: Number(0), debugloc: None })
instruction: And(And { operand0: LocalOperand { name: Name("input1.07"), ty: IntegerType { bits: 8 } }, operand1: ConstantOperand(Int { bits: 8, value: 3 }), dest: Name("_8"), debugloc: None })
instruction: ICmp(ICmp { predicate: EQ, operand0: LocalOperand { name: Name("_8"), ty: IntegerType { bits: 8 } }, operand1: ConstantOperand(Int { bits: 8, value: 1 }), dest: Name("_7"), debugloc: None })
instruction: URem(URem { operand0: LocalOperand { name: Name("input1.07"), ty: IntegerType { bits: 8 } }, operand1: ConstantOperand(Int { bits: 8, value: 3 }), dest: Name("_13"), debugloc: None })
...

In this case, the llvm instructions from within the called function are present. Any recommendation on how I can make sure that these are included even in multi-crate analyses?

Thanks in advance! Sorry for the long post.

opened by hudson-ayers 12

Are there any methods provided by haybale for constraining certain variables?
e.g.

int foo(struct Context* context) { //assert(context->x == 1); if (context->x == 0) return 0; if (context->y < 0) return -1; else return 1; }

So I just want to take "context->y" as a symbolic value and restrict "context->x" to 1. Can we reach this but not modify the origin LLVM IR ?
opened by Just1ceP4rtn3r 7
LLVM unreachable instruction
While symbolically executing a function, Haybale threw the following error:

'UnreachableInstruction`: Reached an LLVM 'Unreachable' instruction

Should I interpret this to mean the code under analysis is somehow invalid?
opened by hudson-ayers 7
assert failures for code compiled for 32 bit platforms
I have the following function in a rust program

#[no_mangle] pub fn handle_interrupt(&self) { unsafe { let ptr = 0x4000_8308 as *mut u32; ptr.write(0 as u32); } }

This rust program is compiled for a 32 bit Arm Cortex-M4 MCU via cargo rustc --target=thumbv7em-none-eabi --release -- --e mit=llvm-ir --emit=llvm-bc

I wrote the following haybale code to analyze this function:

//... let em: ExecutionManager<BtorBackend> = symex_function("handle_interrupt", project, config); em.next()

Unfortunately, this code fails with the following error:

thread 'main' panicked at 'assertion failed: `(left == right)` left: `32`, right: `64`', /home/hudson/.cargo/git/checkouts/haybale-12b18082e7030da8/695e1fa/src/state.rs:1085:17

I assume this has something to do with the target CPU having a different pointer width than the host CPU on which I am running my haybale analyses, as the same function works if I compile for my host machine. Any suggestions for how I can fix this? Or is haybale incompatible with analysis of code compiled for 32 bit platforms?
opened by hudson-ayers 7

`UnsupportedInstruction`: encountered an LLVM instruction which is not currently supported: terminator Invoke

Hello,

I'm just playing around with this and seem to have got stuck. My code:

use std::path::Path;
use haybale;
use rustc_demangle::demangle;

fn main() {
    let proj = haybale::Project::from_bc_path(&Path::new("../rustls-llvm8.bc"))
        .expect("cannot open bitcode");
    for (func, _module) in proj.all_functions() {
        if demangle(&func.name).to_string() == "<rustls::client::tls12::ExpectServerDone as rustls::client::hs::State>::handle::h9460148ae7f0b07f" {
            println!("func {:?} ret {:?} param {:#?}", demangle(&func.name), func.return_type, func.parameters);

            for (i, bb) in func.basic_blocks.iter().enumerate() {
                println!("bb {}: {:?}", i, bb);
            }

            let mut cfg = haybale::Config::<haybale::backend::BtorBackend>::default();
            cfg.null_detection = false;
            let mut em = haybale::symex_function(&func.name,
                                                 &proj,
                                                 cfg);

            loop {
                let n = em.next();
                if n.is_none() {
                    break;
                }
                println!("n {:?}", n);
                let st = em.state();
                println!("state 0 {:?}", st.cur_loc);
            }


        }
    }
}

I've attached my input file.

This produces an error:

n Some(Err("Received the following error:\n  `UnsupportedInstruction`: encountered an LLVM instruction which is not currently supported: terminator Invoke(Invoke { function: Right(ConstantOperand(GlobalReference { name: Name(\"_ZN6rustls7hash_hs13HandshakeHash11add_message17h8f65251448a5a012E\"), ty: FuncType { result_type: PointerType { pointee_type: NamedStructType { name: \"hash_hs::HandshakeHash\", ty: Some((Weak)) }, addr_space: 0 }, param_types: [PointerType { pointee_type: NamedStructType { name: \"hash_hs::HandshakeHash\", ty: Some((Weak)) }, addr_space: 0 }, PointerType { pointee_type: NamedStructType { name: \"msgs::message::Message\", ty: Some((Weak)) }, addr_space: 0 }], is_var_arg: false } })), arguments: [(LocalOperand { name: Number(7), ty: PointerType { pointee_type: NamedStructType { name: \"hash_hs::HandshakeHash\", ty: Some((Weak)) }, addr_space: 0 } }, [EnumAttribute { kind: 1, value: Some(8) }, EnumAttribute { kind: 9, value: Some(256) }]), (LocalOperand { name: Number(3), ty: PointerType { pointee_type: NamedStructType { name: \"msgs::message::Message\", ty: Some((Weak)) }, addr_space: 0 } }, [EnumAttribute { kind: 20, value: None }, EnumAttribute { kind: 37, value: None }, EnumAttribute { kind: 1, value: Some(8) }, EnumAttribute { kind: 9, value: Some(184) }])], return_attributes: [EnumAttribute { kind: 1, value: Some(8) }, EnumAttribute { kind: 9, value: Some(256) }], result: Number(8), return_label: Name(\"bb1\"), exception_label: Name(\"cleanup\"), function_attributes: [], calling_convention: C })\nLLVM backtrace:\n  #1: {../rustls-llvm8.bc: _ZN85_$LT$rustls..client..tls12..ExpectServerDone$u20$as$u20$rustls..client..hs..State$GT$6handle17h9460148ae7f0b07fE \"start\", instr 137}\n\n"))

Which I think originates from https://github.com/PLSysSec/haybale/blob/master/src/symex.rs#L191 when there's a function invocation in basic block tail position? Is there any plan to support that case?

opened by ctz 6

Docs do not build for 0.6.2

See: https://docs.rs/crate/haybale/0.6.2 . Not a huge deal because you can just visit an older version of the docs, but thought you might want to be aware because all of the links in the README are now broken.

opened by hudson-ayers 5
Boolector failures for functions that return 0 length slices
If Haybale encounters a function that returns a 0 length slice (e.g. &mut []) when symbolically exectuing rust code, it aborts with the following boolector failure:

[boolector] boolector_bitvec_sort: 'width' must be > 0

I can't see any reason why this case should be impossible for haybale to analyze, so I am assuming this is a bug. My apologies if this is the intended behavior.

An example of a test that triggers this can be found here: https://github.com/hudson-ayers/haybale/commit/1150cbdb2fae783cdd63f629cce086d5b51d2951 . Feel free to incorporate this test into your repo if you like. Notably, if you replace &mut [] with self.a in ez2(), the test passes.
opened by hudson-ayers 5

Can't compile haybale

rustc version 1.52.1, Cargo.toml:

haybale = { version = "0.7.0", features = ["llvm-9", "vendor-boolector"] }

Output:

   Compiling regex v1.5.4
   Compiling llvm-sys v90.2.0
error: failed to run custom build command for `boolector-sys v0.6.3`

Caused by:
  process didn't exit successfully: `/home/mgh/code/projects/symex-exp/problems/trivial/haybale/trivial-hb/target/debug/build/boolector-sys-38fa6a76279ef757/build-script-build` (exit code: 101)
  --- stdout
  running "/usr/bin/env" "bash" "/home/mgh/code/projects/symex-exp/problems/trivial/haybale/trivial-hb/target/debug/build/boolector-sys-7b0d25cc0db9615f/out/vendor-build/contrib/setup-lingeling.sh"
  lingeling-03b4860d14016f42213ea271014f2f13d181f504/
...
  In file included from /home/mgh/code/projects/symex-exp/problems/trivial/haybale/trivial-hb/target/debug/build/boolector-sys-7b0d25cc0db9615f/out/build/googletest/googletest-src/googletest/src/gtest-all.cc:42:
  /home/mgh/code/projects/symex-exp/problems/trivial/haybale/trivial-hb/target/debug/build/boolector-sys-7b0d25cc0db9615f/out/build/googletest/googletest-src/googletest/src/gtest-death-test.cc: In function ‘bool testing::internal::StackGrowsDown()’:
  /home/mgh/code/projects/symex-exp/problems/trivial/haybale/trivial-hb/target/debug/build/boolector-sys-7b0d25cc0db9615f/out/build/googletest/googletest-src/googletest/src/gtest-death-test.cc:1301:24: error: ‘dummy’ may be used uninitialized [-Werror=maybe-uninitialized]
   1301 |   StackLowerThanAddress(&dummy, &result);
        |   ~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~
  /home/mgh/code/projects/symex-exp/problems/trivial/haybale/trivial-hb/target/debug/build/boolector-sys-7b0d25cc0db9615f/out/build/googletest/googletest-src/googletest/src/gtest-death-test.cc:1290:13: note: by argument 1 of type ‘const void*’ to ‘void testing::internal::StackLowerThanAddress(const void*, bool*)’ declared here
   1290 | static void StackLowerThanAddress(const void* ptr, bool* result) {
        |             ^~~~~~~~~~~~~~~~~~~~~
  /home/mgh/code/projects/symex-exp/problems/trivial/haybale/trivial-hb/target/debug/build/boolector-sys-7b0d25cc0db9615f/out/build/googletest/googletest-src/googletest/src/gtest-death-test.cc:1299:7: note: ‘dummy’ declared here
   1299 |   int dummy;
        |       ^~~~~
  cc1plus: all warnings being treated as errors
  make[2]: *** [googletest/googletest-build/googletest/CMakeFiles/gtest.dir/build.make:76: googletest/googletest-build/googletest/CMakeFiles/gtest.dir/src/gtest-all.cc.o] Error 1
  make[1]: *** [CMakeFiles/Makefile2:396: googletest/googletest-build/googletest/CMakeFiles/gtest.dir/all] Error 2
  make: *** [Makefile:146: all] Error 2
  thread 'main' panicked at '
  command did not execute successfully, got: exit code: 2

  build script failed, must exit now', /home/mgh/.cargo/registry/src/github.com-1ecc6299db9ec823/cmake-0.1.45/src/lib.rs:894:5

opened by sp1ff 3

add helper function for printing instruction traces / getting path length

This PR adds a helper function for printing an LLVM IR instruction trace for a State, as well as a helper function for getting the number of LLVM IR instructions in a given path. Both functions only provide accurate output if no hooked functions are contained in the Path being analyzed (per discussion in #5 ).

For pretty_path_llvm_instructions(), I ended up just using a lookahead cache approach to see if a given Call leaves the current basic block. I played for awhile with trying to use resolve_function(call) to see if it returns NoHookActive, but resolve_function() mutates the State under analysis, which seems clearly undesirable here. And pulling out the minimum logic from within resolve_function() necessary was actually a lot of repeated code that would likely fall out of data if updates were made to resolve_function() in the future.

This PR also adds a test of both functions, which simply checks that the number of instructions in the pretty print is equal to the number the returned length. Unfortunately, I consistently find that there is one more instruction in the pretty path than the length function reports there should be -- if you see any logic error by me that could lead to this, please let me know.

I understand these functions may be of limited use for most users, who might often have hooked functions in their path -- I am not sure if you want to go further than I did to make these functions only usable alongside a particular configuration, for example.

I struggled to get cargo fmt to work correctly with your modified rustfmt.toml. cargo fmt fails, saying a nightly toolchain is required. cargo +nightly fmt leads to tons of changes in files I did not touch, so it seems to not be what you used. So you may want to add a formatting commit to this PR.

opened by hudson-ayers 3
LLVM AtomicRMW Instruction

Would it be possible to support the LLVm AtomicRMW Instruction? I am running into the following error:

UnsupportedInstruction: encountered an LLVM instruction which is not currently supported: instruction AtomicRMW.

Or does handling atomic instructions add significant complexity?

opened by hudson-ayers 3

Trouble analyzing basic Rust programs

Hi, I am interested in using this tool for analyzing Rust source code. However I have found I am unable to use either example analysis on even an extremely simple rust program:

The program I am analyzing, compiled to bitcode using cargo rustc -- -g --emit=llvm-bc --emit=llvm-ir:

fn ez(input: u32) -> u32 {
    input * 2
}

fn main() {
    let out = ez(1);
    println!("out: {}", out);
}

My haybale code (in a separate repository):

use haybale::*;
use std::path::Path;
use std::result::Result;
use std::string::String;

fn main() -> Result<(), String> {
    let project = Project::from_bc_path(&Path::new("/home/hudsonayers/test2/target/debug/deps/test2-ad7a69efa56795e2.bc"))?;
    let ret = get_possible_return_values_of_func("ez", vec!(Some(1)), &project, Config::default(), None, 10);
    println!("ret: {:?}", ret);
    /*match find_zero_of_func("ez", &project, Config::default()) {
        Ok(None) => println!("foo can never return 0"),
        Ok(Some(inputs)) => println!("returns 0 for: {:?}", inputs),
        Err(e) => panic!("{}", e),
    }*/
    Ok(())
}

This code compiles, but fails when run.

The output I get:

thread 'main' panicked at '`FunctionNotFound`: encountered a call of a function named "llvm.expect.i1", but failed to find an LLVM definition, a function hook, or a built-in handler for it

Backtrace:
  #1: {/home/hudsonayers/test2/target/debug/deps/test2-ad7a69efa56795e2.bc: ez, bb "start", instr 7}
         (/home/hudsonayers/test2/src/main.rs, line 3, col 4)

I get the same result if I call find_zero_of_func() instead. The code runs fine if I just construct the project but do not use it.

Both repositories are using rust 1.40.0 (also tried later versions). I have boolector 3.1.0 installed. I am using llvm 9, installed per the instructions at https://apt.llvm.org/ . My machine is running debian 10, though I also tried on an ubuntu 20.04 machine with equivalent results.

Any advice? Is this an issue with my llvm installation? Something else I am missing?

Thanks in advance.

opened by hudson-ayers 3

Function pointer multiple dispatch

Hi, I am curious if you have any thoughts on what it would take to support function pointers which could resolve to multiple target functions. This line seems to be the relevant location where Haybale currently gives up if a function pointer can resolve to multiple functions. Would it be possible for other (still small) values of n to treat function pointer calls as effectively branching points, with each possibly destination representing an additional path? Presumably there are reasons this is difficult and as such not supported currently.

I am mostly curious because I have been maintaining a fork of Haybale which uses custom, Rust specific logic to handle Rust dynamic dispatch by identifying possible targets of dynamic dispatch by parsing LLVM-IR debug info + Rust's MIR to find valid concrete functions at dynamic dispatch points. If Haybale had general support for function pointers with multiple targets, I could simplify this implementation such that it could maybe just be a user-defined hook rather than a direct modification of Haybale itself.

opened by hudson-ayers 0

error-handled `loop_bound`

Here is a simple c code

void foo()
{
int a = strlen("123");;
int b = strlen("123");
}

When I test it with loop_bound=2, haybale will throw a LoopBoundExceeded error because strlen was called multiple times. Thus varmap.active_version store ("strlen", "%21", BV) twice. Debug info:

  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %1, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %47, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: mosquitto__calloc, bb %2, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %47, starting at instr 1}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %53, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %77, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %93, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %114, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %123, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %133, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %156, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %161, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %174, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %178, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %249, starting at terminator}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %250, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %253, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %258, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %269, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %304, starting at terminator}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %305, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %313, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %335, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %342, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %1, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %17, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %20, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %20, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %29, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %38, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %43, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %342, starting at instr 6}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %1, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %17, starting at instr 0}
  {/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %20, starting at instr 0}

opened by Just1ceP4rtn3r 4