haybale is a symbolic execution engine for LLVM Intermediate Representation (IR), written in Rust. It allows for rigorous, mathematical analysis of program behavior, enabling users to determine all possible inputs that lead to specific outcomes or to answer complex questions about program logic without brute-force testing. This makes it valuable for security researchers, software testers, and developers seeking to verify program correctness and identify potential vulnerabilities.

How It Works

haybale operates by converting program variables into mathematical expressions dependent on program inputs. It then leverages an SMT solver (Boolector) to analyze these expressions and answer queries about program behavior. The engine processes LLVM bitcode, allowing analysis of programs written in languages that compile to LLVM IR, such as C, C++, and Rust. Its design in Rust aims for performance and memory safety, with a modular architecture that allows for custom analysis development.

Quick Start & Requirements

• Install via Cargo: cargo add haybale --features "llvm-14" (replace llvm-14 with your LLVM version, e.g., llvm-9 to llvm-14).
• Prerequisites: LLVM (matching the selected feature) and Boolector (either system-installed or vendored via vendor-boolector feature).
• Generate LLVM bitcode (.bc files) using clang or rustc with -emit-llvm and -g for debug info.
• See docs.rs for full documentation.

Highlighted Details

• Analyzes programs compiled to LLVM IR from various languages (C, C++, Rust, etc.).
• Integrates with the Boolector SMT solver for constraint satisfaction.
• Supports LLVM versions 9 through 14 via feature flags.
• Provides built-in analyses like find_zero_of_func and get_possible_return_values_of_func.
• Allows for custom analysis development by iterating through execution paths and inspecting program states.

Maintenance & Community

• Active development with regular releases, the latest being 0.7.2 (October 2023).
• Supports LLVM 14 and includes a feature to vendor Boolector for easier builds.
• Documentation is available on docs.rs.

Licensing & Compatibility

• MIT License.
• Compatible with commercial and closed-source projects.

Limitations & Caveats

• Does not claim feature parity with KLEE.
• LLVM 8 and earlier are not supported in current releases; an unmaintained branch exists for LLVM 8.
• Vendoring Boolector may only work on Linux and macOS and requires build tools.