Indexing into a slice of an array with a non-zero offset causes a CBMC invariant violation #708
Description
I tried this code:
fn main() {
let arr = [1, 2, 3];
let s = &arr[1..];
assert!(s[0] == 2);
assert!(s[1] == 3);
}using the following command line invocation:
rmc test.rs
with RMC version: 371faaebc7c
I expected to see this happen: Verification successful
Instead, this happened: CBMC invariant violation:
$ rmc test.rs
CBMC version 5.46.0 (cbmc-5.46.0) 64-bit x86_64 linux
Reading GOTO program from file
Reading: test.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
Runtime Symex: 0.00918048s
size of program expression: 318 steps
simple slicing removed 9 assignments
Generated 35 VCC(s), 7 remaining after simplification
Runtime Postprocess Equation: 1.5481e-05s
Passing problem to propositional reduction
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/flattening/boolbv_add_sub.cpp:68 function: convert_add_sub
Condition: it->type() == type
Reason: add/sub with mixed types:
+
* type: signedbv
* width: 64
* #c_type: signed_long_int
0: constant
* type: signedbv
* width: 64
* #c_type: signed_long_int
* value: 1
1: constant
* type: unsignedbv
* #source_location:
* file: <built-in-additions>
* line: 1
* working_directory: /home/ubuntu/examples/new-iss
* width: 64
* #typedef: __CPROVER_size_t
* #c_type: unsigned_long_int
* value: 1
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x50) [0x55863b8aa5e0]
cbmc(get_backtrace[abi:cxx11]()+0x169) [0x55863b8aab89]
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) [0x55863b148558]
cbmc(boolbvt::convert_add_sub(exprt const&)+0x1869) [0x55863b63fd39]
cbmc(boolbvt::convert_bitvector(exprt const&)+0x124) [0x55863b6357d4]
cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x101) [0x55863b67d061]
cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0xc0) [0x55863b638d80]
cbmc(boolbvt::convert_equality(equal_exprt const&)+0xd2) [0x55863b64c352]
cbmc(boolbvt::convert_rest(exprt const&)+0x24d) [0x55863b63664d]
cbmc(bv_pointerst::convert_rest(exprt const&)+0xab) [0x55863b678c0b]
cbmc(prop_conv_solvert::convert_bool(exprt const&)+0x2db) [0x55863b6b5fdb]
cbmc(prop_conv_solvert::convert(exprt const&)+0x127) [0x55863b6b7d97]
cbmc(prop_conv_solvert::convert_bool(exprt const&)+0x54f) [0x55863b6b624f]
cbmc(prop_conv_solvert::convert(exprt const&)+0x127) [0x55863b6b7d97]
cbmc(boolbvt::convert_index(index_exprt const&)+0x106e) [0x55863b659ffe]
cbmc(boolbvt::convert_bitvector(exprt const&)+0x1de) [0x55863b63588e]
cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x101) [0x55863b67d061]
cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0xc0) [0x55863b638d80]
cbmc(boolbvt::boolbv_set_equality_to_true(equal_exprt const&)+0xea) [0x55863b63533a]
cbmc(boolbvt::set_to(exprt const&, bool)+0x78) [0x55863b635408]
cbmc(symex_target_equationt::convert_assignments(decision_proceduret&)+0xd1) [0x55863b371771]
cbmc(symex_target_equationt::convert_without_assertions(decision_proceduret&)+0x7a) [0x55863b379ffa]
cbmc(symex_target_equationt::convert(decision_proceduret&)+0x42) [0x55863b37ab42]
cbmc(convert_symex_target_equation(symex_target_equationt&, decision_proceduret&, message_handlert&)+0x334) [0x55863b1652c4]
cbmc(prepare_property_decider(std::map<dstringt, property_infot, std::less<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&, symex_target_equationt&, goto_symex_property_decidert&, ui_message_handlert&)+0x3c5) [0x55863b165745]
cbmc(multi_path_symex_checkert::operator()(std::map<dstringt, property_infot, std::less<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&)+0x155) [0x55863b1753d5]
cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator()()+0x89) [0x55863b153539]
cbmc(cbmc_parse_optionst::doit()+0xf8e) [0x55863b14f9fe]
cbmc(parse_options_baset::main()+0x8f) [0x55863b14666f]
cbmc(main+0x39) [0x55863b134fa9]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7ff7e7e790b3]
cbmc(_start+0x2e) [0x55863b147f6e]
--- end invariant violation report ---
The invariant violation is due to the second assert (assert!(s[1] == 3). If I comment out this assert, verification passes. Verification also passes if the slice has zero offset into the array, e.g.:
fn main() {
let arr = [1, 2, 3];
let s = &arr[0..2];
assert!(s[0] == 1);
assert!(s[1] == 2);
}So, it appears that the issue occurs when adding the index into the slice to the offset of the array.