CBMC invariant violation for getrandom and rand_core

[zhassan-aws]

The combination of the getrandom and rand_core crates seems to cause a CBMC invariant check failure.

These are the steps to reproduce:

1. Create a new project with cargo:

cargo new foo

2. Add getrandom and rand as dependencies in the Cargo.toml:

[dependencies]
getrandom = "0.2"
rand = "0.8.0"

3. Run RMC on the project:

mkdir ~/foo-target
CARGO_TARGET_DIR=~/foo-target RUST_BACKTRACE=1 RUSTFLAGS="-Z trim-diagnostic-paths=no -Z codegen-backend=gotoc --cfg=rmc" RUSTC=rmc-rustc cargo build --target x86_64-unknown-linux-gnu -j1

4. Run symtab2gb:

cd ~/foo-target/x86_64-unknown-linux-gnu/debug/deps/
symtab2gb getrandom-6f345ac2a566ca4c.json rand_core-f501d635a961dbb4.json   --out a.out

This produces the following invariant violation report:

--- begin invariant violation report ---
Invariant check failed
File: ../src/langapi/mode.cpp:91 function: get_language_from_identifier
Condition: language
Reason: symbol 'tag-std::backtrace::BytesOrWide::951697206286575092-union::Bytes' has unknown mode 'C'
Backtrace:
symtab2gb(print_backtrace(std::ostream&)+0x50) [0x556f951b7d90]
symtab2gb(get_backtrace[abi:cxx11]()+0x169) [0x556f951b8339]
symtab2gb(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) [0x556f951a30a8]
symtab2gb(get_language_from_identifier(namespacet const&, dstringt const&)+0x22f) [0x556f9532e6cf]
symtab2gb(type_to_name[abi:cxx11](namespacet const&, dstringt const&, typet const&)+0x34) [0x556f9532d204]
symtab2gb(linkingt::rename_symbols(std::unordered_set<dstringt, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<dstringt> > const&)+0x88) [0x556f952fc4c8]
symtab2gb(linkingt::typecheck()+0x10e) [0x556f952fe5de]
symtab2gb(typecheckt::typecheck_main()+0x52) [0x556f95323e32]
symtab2gb(link_goto_model(goto_modelt&, goto_modelt&, message_handlert&)+0x462) [0x556f952a70c2]
symtab2gb(+0x9e03e) [0x556f951a503e]
symtab2gb(symtab2gb_parse_optionst::doit()+0x1b5) [0x556f951a56c5]
symtab2gb(parse_options_baset::main()+0x8f) [0x556f9519f96f]
symtab2gb(main+0x39) [0x556f9519f199]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f62c8f760b3]
symtab2gb(_start+0x2e) [0x556f951a2cfe]


--- end invariant violation report ---

Running symtab2gb on either of the two json files by itself does not result in an invariant check failure.

[zhassan-aws]

Adding rand only as a dependency in step 2 is sufficient for triggering the issue.

[tautschnig]

This problem was fixed in diffblue/cbmc#6233.

[tautschnig]

(And, therefore, all versions of CBMC from 5.36.0 onwards include this fix.)