Add ESBMC as a verification backend

[rafaelsamenezes]

Requested feature: Allow Kani to hand the goto binary it already produces to
ESBMC instead of CBMC, behind the unstable option -Z esbmc.

Use case: User can use another verification backend that can be used to confirm the results. Secondarily, ESBMC has a different symbolic execution engine, memory model and SMT encoding, so harnesses that one tool cannot finish may be tractable for the other.

Link to relevant documentation (Rust reference, Nomicon, RFC):

• ESBMC: https://github.com/esbmc/esbmc
• Proof of concept: https://github.com/rafaelsamenezes/kani/tree/esbmc-backend-mvp
• RFC draft

Test case:

// kani main_true.rs -Z esbmc   =>  VERIFICATION:- SUCCESSFUL
#[kani::proof]
fn main() {
    let a: u8 = kani::any();
    kani::assume(a < 100);
    assert!(a as u16 + 1 > a as u16);
}
// kani main_false.rs -Z esbmc  =>  VERIFICATION:- FAILED
#[kani::proof]
fn main() {
    let a: u8 = kani::any();
    let b: u8 = kani::any();
    assert!(a >= b);
}

[feliperodri]

cc. @tautschnig @celinval

[feliperodri]

@rafaelsamenezes I'm assuming there will be no difference between user experience when using Kani features with ESBMC, is that correct? For example, we will still have the same support for concrete playback etc. Overall it looks good to me and you can send a PR for us to discuss the details of the RFC.

[feliperodri]

@rafaelsamenezes There is also a question of maintainability that I didn't quite grasp in the RFC. We have a nightly build on CBMC, automatic PRs to keep the version of CBMC up to date, and so on... ESBMC is a very active project and the value proposition to me is to have access to all SMT backend solvers plus the algorithms like k-induction incremental BMC. However, it's important to have a clear statement on the maintenance of a new backend in Kani.

[feliperodri]

I'd also would like to see some performance comparison using our regression test suite as a baseline.

[rafaelsamenezes]

I'm assuming there will be no difference between user experience when using Kani features with ESBMC, is that correct?

Regarding GOTO, ideally yes. But even if ESBMC has full equivalence to the current CBMC. The main risk is:

1. New ireps from CBMC might be used by Kani. Supporting it in ESBMC should be trivial enough but would take some extra time.
2. New safety properties that are added during symex. Some properties may be added during an specific operational model or construct in CBMC. For example, CBMC detects an UB of counting leading zeros from zero.

Both should be fast enough to keep in sync with ESBMC though.

For example, we will still have the same support for concrete playback etc.

I have to test it out. If we mean using Kani (with CBMC backend) to replay an ESBMC trace. It is a matter of adding a similar JSON output in ESBMC that CBMC has. Once implemented, should always be compatible.

There is also a question of maintainability that I didn't quite grasp in the RFC.

You mean as in ensuring that the latest versions of ESBMC will keep the support for Kani and automatically update?

I'd also would like to see some performance comparison using our regression test suite as a baseline.

Working on it, will open the RFC PR once I have the results.