Enable CBMC's slicer

[zhassan-aws]

Description of changes:

Enable CBMC's slicer (--reachability-slice) to remove code that does not impact any of the checks from the goto binary. This change required moving all the check options (e.g. --bounds-check, --pointer-check, etc.) from the cbmc step to goto-instrument to make sure they're injected into the goto binary before the slicer is applied (see discussion here).

Resolved issues:

Resolves #683

Should help with standard library linking (e.g. #576)

Call-outs:

This change breaks Kani's --cbmc-args option even further: specifying any check options, e.g. --signed-overflow-check may not have an impact since they will be applied after the possible removal of code relevant to those checks by the slicer.

Testing:

• How is this change tested? Current regressions

• Is this a refactor change? No

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[adpaco-aws]

Can you explain why some checks are not triggered anymore? Sorry, didn't pay attention to the call-outs section.

[adpaco-aws]

Can you run a quick experiment to quantify the improvement?

Please take this version and one that doesn't add the --reachability-slice option, and use both to run a few non-trivial regression tests (the Firecracker regression is a good candidate here), comparing the number of checks and functions.

[danielsn]

Why do these disappear?

[zhassan-aws]

This is pointed out in the call-outs: specifying any additional checks to the CBMC command (e.g. --signed-overflow-check) may become a no-op since the slicer potentially removes code checked by that particular check.

[zhassan-aws]

Can you run a quick experiment to quantify the improvement?

Please take this version and one that doesn't add the --reachability-slice option, and use both to run a few non-trivial regression tests (the Firecracker regression is a good candidate here), comparing the number of checks and functions.

Ran some experiments, and the improvement is mostly marginal:

	Without Slicer			With Slicer
Benchmark	Checks	Time (s)	Memory (MB)	Checks	Time (s)	Memory (MB)
s2n-quic check_vetored_copy_u8	359	125.8	2658	353	123.4	2649
firecracker block example	318	4.75	213	298	3.83	195
rectangle example	42	6.28	106	40	7.2	107
vecdeque CVE	402	0.57	191	389	0.55	191

[zhassan-aws]

Attempted to re-do the std library linking experiment using the following steps:

1. cargo new --lib lstd
2. Put the following in src/lib.rs:

#[kani::proof]
fn check_format() {
    assert!("2021".parse::<u32>().unwrap() == 2021);
}

3. Build using:

KANIFLAGS="--goto-c --ignore-global-asm --log-level=error --assertion-reach-checks -C symbol-mangling-version=v0" RUSTC="/home/ubuntu/git/kani/target/debug/kani-compiler" RUSTFLAGS="--kani-flags" cargo +nightly-2022-05-17 build --target x86_64-unknown-linux-gnu -Z build-std --lib --target-dir target

4. Convert symbol table json files to goto binaries using

cd target/x86_64-unknown-linux-gnu/debug/deps && ls *.symtab.json | parallel -j 16 symtab2gb {} --out {.}.out

but ran into a bunch of issue:

1. In step 3, got many errors of the form:

error: duplicate lang item in crate `std` (which `kani` depends on): `panic_impl`.
  |
  = note: the lang item is first defined in crate `std` (which `lstd` depends on)
  = note: first definition in `std` loaded from /home/ubuntu/examples/lstd/target/x86_64-unknown-linux-gnu/debug/deps/libstd-9f9e8af9b2102e2a.rmeta
  = note: second definition in `std` loaded from /home/ubuntu/.rustup/toolchains/nightly-2022-05-17-x86_64-unknown-linux-gnu/lib/rustlib/x86_64-unknown-linux-gnu/lib/libstd-977ece543e1e3d2f.rlib

error: duplicate lang item in crate `std` (which `kani` depends on): `begin_panic`.
  |
  = note: the lang item is first defined in crate `std` (which `lstd` depends on)
  = note: first definition in `std` loaded from /home/ubuntu/examples/lstd/target/x86_64-unknown-linux-gnu/debug/deps/libstd-9f9e8af9b2102e2a.rmeta
  = note: second definition in `std` loaded from /home/ubuntu/.rustup/toolchains/nightly-2022-05-17-x86_64-unknown-linux-gnu/lib/rustlib/x86_64-unknown-linux-gnu/lib/libstd-977ece543e1e3d2f.rlib

error: duplicate lang item in crate `std` (which `kani` depends on): `oom`.
  |
  = note: the lang item is first defined in crate `std` (which `lstd` depends on)
  = note: first definition in `std` loaded from /home/ubuntu/examples/lstd/target/x86_64-unknown-linux-gnu/debug/deps/libstd-9f9e8af9b2102e2a.rmeta
  = note: second definition in `std` loaded from /home/ubuntu/.rustup/toolchains/nightly-2022-05-17-x86_64-unknown-linux-gnu/lib/rustlib/x86_64-unknown-linux-gnu/lib/libstd-977ece543e1e3d2f.rlib

error: duplicate lang item in crate `std` (which `kani` depends on): `start`.
  |
  = note: the lang item is first defined in crate `std` (which `lstd` depends on)
  = note: first definition in `std` loaded from /home/ubuntu/examples/lstd/target/x86_64-unknown-linux-gnu/debug/deps/libstd-9f9e8af9b2102e2a.rmeta
  = note: second definition in `std` loaded from /home/ubuntu/.rustup/toolchains/nightly-2022-05-17-x86_64-unknown-linux-gnu/lib/rustlib/x86_64-unknown-linux-gnu/lib/libstd-977ece543e1e3d2f.rlib

error: duplicate lang item in crate `std` (which `kani` depends on): `termination`.
  |
  = note: the lang item is first defined in crate `std` (which `lstd` depends on)
  = note: first definition in `std` loaded from /home/ubuntu/examples/lstd/target/x86_64-unknown-linux-gnu/debug/deps/libstd-9f9e8af9b2102e2a.rmeta
  = note: second definition in `std` loaded from /home/ubuntu/.rustup/toolchains/nightly-2022-05-17-x86_64-unknown-linux-gnu/lib/rustlib/x86_64-unknown-linux-gnu/lib/libstd-977ece543e1e3d2f.rlib

error: duplicate lang item in crate `core` (which `std` depends on): `sized`.
  |
  = note: the lang item is first defined in crate `core` (which `std` depends on)
  = note: first definition in `core` loaded from /home/ubuntu/examples/lstd/target/x86_64-unknown-linux-gnu/debug/deps/libcore-6d9d14315cbfc8dc.rmeta
  = note: second definition in `core` loaded from /home/ubuntu/.rustup/toolchains/nightly-2022-05-17-x86_64-unknown-linux-gnu/lib/rustlib/x86_64-unknown-linux-gnu/lib/libcore-0e3656b1fda5fd7b.rlib

error[E0034]: multiple applicable items in scope
 --> src/lib.rs:3:20
  |
3 |     assert!("2021".parse::<u32>().unwrap() == 2021);
  |                    ^^^^^ multiple `parse` found
  |
  = note: candidate #1 is defined in an impl for the type `str`
  = note: candidate #2 is defined in an impl for the type `str`

For more information about this error, try `rustc --explain E0034`.
Error: "Failed to compile crate."
error: could not compile `lstd` due to 113 previous errors

2. If I ignore those errors and proceed with step 4, I got some CBMC invariant violations:

--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-programs/goto_convert_functions.cpp:173 function: convert_function
Condition: parameter identifier must be a known symbol
Reason: symbol_table.has_symbol(p)
Backtrace:
symtab2gb(print_backtrace(std::ostream&)+0x50) [0x5641cf9429d0]
symtab2gb(get_backtrace[abi:cxx11]()+0x169) [0x5641cf942f79]
symtab2gb(std::enable_if<std::is_base_of<invariant_failedt, invariant_with_diagnostics_failedt>::value, void>::type invariant_violated_structured<invariant_with_diagnostics_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >(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> >&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&&)+0x44) [0x5641cf95f144]
symtab2gb(goto_convert_functionst::convert_function(dstringt const&, goto_functiont&)+0x238e) [0x5641cfb2562e]
symtab2gb(goto_convert_functionst::goto_convert(goto_functionst&)+0x11c) [0x5641cfb2660c]
symtab2gb(goto_convert(symbol_table_baset&, goto_functionst&, message_handlert&)+0x497) [0x5641cfb27657]
symtab2gb(goto_convert(goto_modelt&, message_handlert&)+0x89) [0x5641cfb27869]
symtab2gb(+0xe73b8) [0x5641cf92f3b8]
symtab2gb(symtab2gb_parse_optionst::doit()+0x13d) [0x5641cf92fa0d]
symtab2gb(parse_options_baset::main()+0x8f) [0x5641cf9281cf]
symtab2gb(main+0x39) [0x5641cf9279f9]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f117a7af0b3]
symtab2gb(_start+0x2e) [0x5641cf92d40e]

Diagnostics: 
<< EXTRA DIAGNOSTICS >>
function:
_RNvMs_NtNtCsely0tNBvcUY_10proc_macro6bridge7closureINtB4_7ClosureINtNtB6_6buffer6BufferhEB11_E4callB8_
parameter:
_RNvMs_NtNtCsely0tNBvcUY_10proc_macro6bridge7closureINtB4_7ClosureINtNtB6_6buffer6BufferhEB11_E4callB8_::1::var_1::self
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---

[adpaco-aws]

I'm fine with moving the arguments to goto-instrument, which appears to be something we should've done anyway. Considering these result, do you still want to keep the slicing step?

[adpaco-aws]

Why not exit gracefully if it errors out?

[zhassan-aws]

As discussed above, we did not find a compelling case for enabling CBMC's --reachability-slice option by default. The other refactoring changes related to moving the *-checks flags from the cbmc command to the goto-instrument command will be handled as part of the complete fix for #368. Closing this PR.