kani Linking the Rust standard library

Rust toolchains come with a pre-built shared object file for the standard library, so it seems likely that what we need to do is ship a pre-built goto-c object file for the standard library.

We need a way to build this object file.
We need to ensure we have sufficient and sound program-slicing to cull it down to size, so that unused functions do not blow up verification times.
We can think about pre-linking more things (like "rmc c lib") into it. However if we want to support no_std then maybe not?

Tracking issue

Would fix https://github.com/model-checking/kani/issues/87
Related https://github.com/model-checking/kani/issues/208
Would fix https://github.com/model-checking/kani/issues/241
Related https://github.com/model-checking/kani/issues/556
Related https://github.com/model-checking/kani/issues/564
Related https://github.com/model-checking/kani/issues/576 (Comment on this one extracted into this issue's tasks)
Would fix https://github.com/model-checking/kani/issues/581 (Kind of precursor to this issue)

May 23 '22 22:05 tedinski

ALTERNATIVELY!

It sounds like MIRI does "normal" compilation (to rlib) every step of the way until the very end, where it also pulls in the standard library rlib and then does a final translation to (in our case) goto-c at the end. Needs investigation.

May 24 '22 19:05 tedinski

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

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

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

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

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:

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

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 ---

Jun 01 '22 01:06 zhassan-aws

I'm closing this issue since users can use --mir-linker to properly link against the standard library. I added all the related issues to the linker stabilization milestone so we don't forget to clean them up.

Oct 11 '22 19:10 celinval