KLEE logo It is inevitable that automatic verification tools will have performance problems because they push up against “the decidability ceiling”: trying to solve undecidable problems and often getting away with it. In an earlier article, we looked at how to profile the verification process to find which part of your program is causing the problem. But that is only half the problem: we need to actually fix the problem.1 So this article looks at one way that we can fix performance bottlenecks when verifying Rust code using the KLEE symbolic execution tool. In particular, it looks at using path-merging to overcome the path explosion problem.

The way that symbolic execution tools like KLEE work is that they enumerate all viable paths through your code and individually explore each one. By “viable”, what I mean is that each time KLEE finds a conditional branch, it uses a solver to decide whether the whether the branch condition must be true, must be false or could be either (depending on symbolic input data). This third situation where a branch depends on the symbolic input data is what distinguishes symbolic execution from conventional (concrete) execution because the symbolic executor will continue executing both paths.

This property of symbolically executing multiple paths through a program is a major cause of verification performance problems because the number of viable paths through a program can grow exponentially.

For example, consider a loop containing a branch.

for i in 0u32 .. N {
    if <condition> {
        x = x + 1;
    }
}

If the branch condition depends on symbolic values, then

  • the first time round the loop, there will be two viable paths to execute so there will be two paths at the end of the loop
  • the second time round the loop, each path will generate two viable paths to explore so there will be four paths at the end of the loop
  • …
  • at the end of the Nth time round the loop, there will be 2^N paths to explore.

(For more detail, see [bornholt:oopsla:2018] and [galea:arxiv:2018].)

Model checkers avoid this problem by always merging paths whenever they reach a control-flow join. In cases like this loop, that is exactly the right thing to do; in others, it causes an explosion in the state space. But I’m using a symbolic execution tool so what can I do?

While looking through KLEE’s documentation, I noticed that KLEE had some support for manually merging paths by calling the function klee_open_merge to start tracking path splits and later calling klee_close_merge to merge paths back together. There is not a lot of documentation but it seemed to be worth a shot so extended our KLEE support to provide these functions and a convenience macro to wrap a block of code.

pub fn open_merge();
pub fn close_merge();

/// Coherent blocks don't fork execution during verification.
#[macro_export]
macro_rules! coherent {
    ( $body:block ) => {
        $crate::open_merge();
        $body;
        $crate::close_merge();
    };
}

To test these, I wrote a small test to create an array, set each element of the array to a symbolic value

use verification_annotations::prelude::*;

#[test]
fn test_merged() {
    // An array
    let mut a = [0u32; N];

    // Set each element of array to a symbolic value
    for i in &a {
        *i = u32::abstract_value();
    }

    // A loop containing two branches - this will cause a performance problem
    // for conventional symbolic execution.
    for x in a.iter() {
        verifier::coherent!{
            verifier::assume((5..10).contains(x) || (15..20).contains(x))
        }
    }

    // A true assertion about an arbitrary element of the array
    verifier::assert!(a[3] < 20);
}

Running this test on KLEE with

    cargo verify --backend=klee --tests -vv --backend-flags=--use-merge |& grep 'generated tests'

should result in

    test_original: {"generated tests": 1024, "total instructions": 709566, "completed paths": 4093}
    test_merged: {"generated tests": 1, "completed paths": 41, "total instructions": 11852}

Indicating that the original version suffers from a path explosion and generates more tests, executes more instructions and explores more paths than the merged version.

  1. Arguably, profiling your code doesn’t even solve half the problem. Until you have actually fixed it, you can’t even be sure that the profiler has correctly identified the root case. ⤾