CBMC invariant violation with an RMC/Bolero integration example

[zhassan-aws]

In an attempt to integrate RMC within Bolero, the following CBMC invariant violation was reported:

--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/flattening/boolbv_width.cpp:197 function: get_entry
Condition: false
Reason: Unimplemented
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x50) [0x564a9925b4b0]
cbmc(get_backtrace[abi:cxx11]()+0x169) [0x564a9925ba59]
cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x48) [0x564a98b4dc78]
cbmc(boolbv_widtht::get_entry(typet const&) const+0x278) [0x564a99053de8]
cbmc(bv_pointerst::bv_pointers_widtht::operator()(typet const&) const+0x3d) [0x564a9905b91d]
cbmc(boolbvt::conversion_failed(exprt const&)+0xa6) [0x564a9901a5f6]
cbmc(boolbvt::convert_bitvector(exprt const&)+0x653) [0x564a9901bb53]
cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x101) [0x564a9905e791]
cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0xc0) [0x564a9901de50]
cbmc(boolbvt::convert_byte_update(byte_update_exprt const&)+0x2c4) [0x564a9902acb4]
cbmc(boolbvt::convert_bitvector(exprt const&)+0x869) [0x564a9901bd69]
cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x101) [0x564a9905e791]
cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0xc0) [0x564a9901de50]
cbmc(boolbvt::boolbv_set_equality_to_true(equal_exprt const&)+0xea) [0x564a9901aa8a]
cbmc(boolbvt::set_to(exprt const&, bool)+0x78) [0x564a9901ab58]
cbmc(symex_target_equationt::convert_assignments(decision_proceduret&)+0xd1) [0x564a98d6fb91]
cbmc(symex_target_equationt::convert_without_assertions(decision_proceduret&)+0x7a) [0x564a98d7841a]
cbmc(symex_target_equationt::convert(decision_proceduret&)+0x42) [0x564a98d78f62]
cbmc(convert_symex_target_equation(symex_target_equationt&, decision_proceduret&, message_handlert&)+0x334) [0x564a98b69574]
cbmc(prepare_property_decider(std::unordered_map<dstringt, property_infot, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&, symex_target_equationt&, goto_symex_property_decidert&, ui_message_handlert&)+0x3c5) [0x564a98b699f5]
cbmc(multi_path_symex_checkert::operator()(std::unordered_map<dstringt, property_infot, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&)+0x155) [0x564a98b797c5]
cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator()()+0x92) [0x564a98b5ca52]
cbmc(cbmc_parse_optionst::doit()+0xc6a) [0x564a98b5524a]
cbmc(parse_options_baset::main()+0x8f) [0x564a98b4be3f]
cbmc(main+0x39) [0x564a98b3b4e9]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f5f61ff10b3]
cbmc(_start+0x2e) [0x564a98b4d68e]


--- end invariant violation report ---

Here are the steps to reproduce:

1. Clone Bolero's rmc-integration branch:

git clone --branch rmc-integration https://github.com/camshaft/bolero

2. Create a library project using cargo:

cargo new --lib foo

3. Add the following dependencies to foo's Cargo.toml:

[dependencies]
bolero = { path = "../bolero/bolero" }
bolero-generator = { path = "../bolero/bolero-generator" }

4. Put the following code in src/lib.rs:

use bolero::{check, generator::*};

#[no_mangle]
fn foo() {
    check!().with_type::<u8>().cloned().for_each(|v| {
        assert!(v != 5);
    })
}

5. Run cargo rmc:

RUST_BACKTRACE=1 RUSTFLAGS="-Z trim-diagnostic-paths=no -Z codegen-backend=gotoc --cfg=rmc --cfg=fuzzing_rmc --cfg=fuzzing" RUSTC=rmc-rustc cargo build --target x86_64-unknown-linux-gnu -j 1

6. cd into the directory with the generated json files:

cd target/x86_64-unknown-linux-gnu/debug/deps

7. Run symtab2gb on all the json files:

ls *.json | parallel -j 16 symtab2gb {} --out {.}.out

8. Run the following commands:

goto-cc --function foo *.out -o a.out
goto-instrument --drop-unused-functions a.out a.out
cbmc a.out

I expected to see this happen: CBMC to report a violation for the assert in src/lib.rs.

Instead, this happened: CBMC reported an invariant check failure.

[zhassan-aws]

Depends on diffblue/cbmc#6163.

[tautschnig]

The CBMC issue should now be fixed.

[zhassan-aws]

Thanks @tautschnig! I confirmed that the example above goes through with the fix to the CBMC issue. I will close the issue once we upgrade RMC to use a CBMC release that includes the fix.