goto-synthesizer crash

[hargoniX]

I tried this code:

fn zeroize(buffer: &mut [u8]) {
    for i in 0..buffer.len() {
        buffer[i] = 0;
    }
}

#[cfg(kani)]
#[kani::proof]
fn check_zeroize() {
    let size: usize = kani::any();
    kani::assume(size > 0);
    kani::assume(size < 32);
    let mut buffer: Vec<u8> = vec![10; size];

    zeroize(&mut buffer);
    let index: usize = kani::any();
    kani::assume(index < buffer.len());
    assert!(buffer[index] == 0);
}

using the following command line invocation:

cargo kani --enable-unstable --synthesize-loop-contracts

with Kani version: cargo-kani 0.42.0 It also appears that Kani does right now not ship the goto-synthesizer binary (at least it complained that it couldn't find it) so I downloaded CBMC 5.95.1 and compiled it from source using:

 cmake -S . -Bbuild -DCMAKE_BUILD_TYPE=RelWithDebInfo -DWITH_JBMC=OFF

Then I copied the goto-synthesizer binary into Kani's bin directory.

I expected to see this happen: Either a successful verification or a sensible error

Instead, this happened: The goto-synthesizer crashed with the following output:

Reading GOTO program from 'exp/target/kani/x86_64-unknown-linux-gnu/debug/deps/exp-20988881b71a0f51__RNvCs4LpoI43CPiG_3exp13check_zeroize.out'
--- begin invariant violation report ---
Invariant check failed
File: cbmc/cbmc-cbmc-5.95.1/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp:213 function: synthesize_assigns
Condition: false
Reason: Failed to synthesize a new assigns target.
Backtrace:
goto-synthesizer() [0xb936af]
goto-synthesizer() [0xb94534]
goto-synthesizer() [0x4f00b4]
goto-synthesizer() [0x50057b]
goto-synthesizer() [0x505062]
goto-synthesizer() [0x4f3295]
goto-synthesizer() [0x4ee725]
goto-synthesizer() [0x4e43ed]
/lib64/libc.so.6(+0x2814a) [0x7f3f9244614a]
/lib64/libc.so.6(__libc_start_main+0x8b) [0x7f3f9244620b]
goto-synthesizer() [0x4ef725]


--- end invariant violation report ---
error: goto-synthesizer exited with status signal: 6 (SIGABRT) (core dumped)

The coredump contains the following backtrace in GDB:

#0  0x00007f3f924ae834 in __pthread_kill_implementation () from /lib64/libc.so.6
Missing separate debuginfos, use: dnf debuginfo-install glibc-2.38-11.fc39.x86_64 libgcc-13.2.1-4.fc39.x86_64 libstdc++-13.2.1-4.fc39.x86_64
(gdb) bt
#0  0x00007f3f924ae834 in __pthread_kill_implementation () from /lib64/libc.so.6
#1  0x00007f3f9245c8ee in raise () from /lib64/libc.so.6
#2  0x00007f3f924448ff in abort () from /lib64/libc.so.6
#3  0x00000000004f018c in invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&> (
    file="cbmc/cbmc-cbmc-5.95.1/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp", function="synthesize_assigns", line=line@entry=213, condition="false")
    at cbmc/cbmc-cbmc-5.95.1/src/util/invariant.h:260
#4  0x000000000050057b in invariant_violated_string (reason="Failed to synthesize a new assigns target.", condition="false", line=213, function="synthesize_assigns",
    file="cbmc/cbmc-cbmc-5.95.1/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp") at cbmc/cbmc-cbmc-5.95.1/src/util/invariant.h:282
#5  enumerative_loop_contracts_synthesizert::synthesize_assigns (this=this@entry=0x7ffcdfdcc140, checked_pointer=..., cause_loop_ids=std::__cxx11::list = {...})
    at cbmc/cbmc-cbmc-5.95.1/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp:213
#6  0x0000000000505062 in enumerative_loop_contracts_synthesizert::synthesize_all (this=this@entry=0x7ffcdfdcc140)
    at cbmc/cbmc-cbmc-5.95.1/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp:437
#7  0x00000000004f3295 in goto_synthesizer_parse_optionst::doit (this=0x7ffcdfdcc7d0) at cbmc/cbmc-cbmc-5.95.1/src/goto-synthesizer/goto_synthesizer_parse_options.cpp:81
#8  0x00000000004ee725 in parse_options_baset::main (this=this@entry=0x7ffcdfdcc7d0) at cbmc/cbmc-cbmc-5.95.1/src/util/parse_options.cpp:97
#9  0x00000000004e43ed in main (argc=<optimized out>, argv=<optimized out>) at cbmc/cbmc-cbmc-5.95.1/src/goto-synthesizer/goto_synthesizer_main.cpp:26

I'm not sure if this qualifies as a Kani or a CBMC bug? If I should report to CBMC instead what information should I provide there?

[zhassan-aws]

@qinheping can you take a look?

[qinheping]

The error message indicates that the synthesizer failed to synthesize a new assign target---the memory location that are going to be written during the loops---, while it found that the current assigns targets is not an over-approximation of the written location. In the case, the synthesis fails and terminate.

The reason of the failure is that Kani encode vector using structs. And now the pointer analysis in CBMC is field-insensitive, and doesn't accurate enough for struct members. We are working on a more accurate assigns-inference algorithm, which may resolve this issue.

I also realize that this error should be reported as synthesis failure instead of exception.