haybale: Symbolic execution of LLVM IR, written in Rust

[RubberDuck]

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 https://klee.github.io/, 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.

https://github.com/PLSysSec/haybale

[DARKER]

Z dokumentacie (github.com/PLSysSec/haybale):

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.

Zaujimava funkcia :-)