Invariant violation due to add/sub with mixed types

[zhassan-aws]

CBMC crashes on the attached example generated by Kani with the following output:

$ cbmc test.out
CBMC version 5.52.0 (cbmc-5.52.0) 64-bit x86_64 linux
Reading GOTO program from file test.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00714568s
size of program expression: 288 steps
simple slicing removed 5 assignments
Generated 5 VCC(s), 4 remaining after simplification
Runtime Postprocess Equation: 3.6091e-05s
Passing problem to propositional reduction
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/flattening/boolbv_add_sub.cpp:69 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/iss708-2
          * width: 64
          * #typedef: __CPROVER_size_t
          * #c_type: unsigned_long_int
      * value: 1
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x50) [0x55e810ab8600]
cbmc(get_backtrace[abi:cxx11]()+0x169) [0x55e810ab8ba9]
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) [0x55e8103408d8]
cbmc(boolbvt::convert_add_sub(exprt const&)+0x1eb6) [0x55e810847476]
cbmc(boolbvt::convert_bitvector(exprt const&)+0x124) [0x55e81083cdc4]
cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x101) [0x55e8108862b1]
cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0xc0) [0x55e810840310]
cbmc(boolbvt::convert_equality(equal_exprt const&)+0xd2) [0x55e810854812]
cbmc(boolbvt::convert_rest(exprt const&)+0x24d) [0x55e81083e27d]
cbmc(bv_pointerst::convert_rest(exprt const&)+0xab) [0x55e8108823ab]
cbmc(prop_conv_solvert::convert_bool(exprt const&)+0x2db) [0x55e8108c041b]
cbmc(prop_conv_solvert::convert(exprt const&)+0x127) [0x55e8108c21d7]
cbmc(prop_conv_solvert::convert_bool(exprt const&)+0x54f) [0x55e8108c068f]
cbmc(prop_conv_solvert::convert(exprt const&)+0x127) [0x55e8108c21d7]
cbmc(boolbvt::convert_index(index_exprt const&)+0x106e) [0x55e81086259e]
cbmc(boolbvt::convert_bitvector(exprt const&)+0x1de) [0x55e81083ce7e]
cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x101) [0x55e8108862b1]
cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0xc0) [0x55e810840310]
cbmc(boolbvt::boolbv_set_equality_to_true(equal_exprt const&)+0xea) [0x55e81083c92a]
cbmc(boolbvt::set_to(exprt const&, bool)+0x78) [0x55e81083c9f8]
cbmc(symex_target_equationt::convert_assignments(decision_proceduret&)+0xd1) [0x55e8105709d1]
cbmc(symex_target_equationt::convert_without_assertions(decision_proceduret&)+0xd6) [0x55e810579326]
cbmc(symex_target_equationt::convert(decision_proceduret&)+0x42) [0x55e810579ed2]
cbmc(convert_symex_target_equation(symex_target_equationt&, decision_proceduret&, message_handlert&)+0x334) [0x55e81035c364]
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) [0x55e81035c7e5]
cbmc(multi_path_symex_checkert::operator()(std::map<dstringt, property_infot, std::less<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&)+0x155) [0x55e81036c615]
cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator()()+0x89) [0x55e81034ad79]
cbmc(cbmc_parse_optionst::doit()+0xf8e) [0x55e8103472de]
cbmc(parse_options_baset::main()+0x8f) [0x55e81033e9ef]
cbmc(main+0x39) [0x55e81032d269]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7fe7520080b3]
cbmc(_start+0x2e) [0x55e8103402ee]


--- end invariant violation report ---
Aborted (core dumped)

CBMC version: 5.52.0
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: cbmc test.out
What behaviour did you expect: Verification successful
What happened instead: Crash

test.out.tar.gz

[martin-cs]

I haven't looked in detail but when we were getting errors like this with gnat2goto it was because of a type mismatch in the goto that we were generating. It looks like you might be mixing up signed and unsigned numbers:

+
  * 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/iss708-2
          * width: 64
          * #typedef: __CPROVER_size_t
          * #c_type: unsigned_long_int
      * value: 1

Somewhere you are adding on a constant of type __CPROVER_size_t? Possibly computing an offset in an array? But the indexing variable is a signed int? You will need to cast one or the other.

HTH.

[zhassan-aws]

@martin-cs there is a related discussion on mixing signed/unsigned on model-checking/kani#708

[martin-cs]

Thanks for the crosslink @zhassan-aws . I am pleased that I was right about it being array indexing but even more pleased that @tautschnig is on the case.

[tautschnig]

@zhassan-aws Does Kani use signed types when doing pointer arithmetic? #6541 would fix this issue, but then @kroening suggested that we might want to enforce stricter rules when generating expressions, ensuring that all pointer arithmetic use signed types.

[zhassan-aws]

I think it does, but we might not be using signed types consistently. @danielsn, can you provide some insight?

[tautschnig]

For the example that you provided, the source statement triggering this bug is:

        // 23 file /home/ubuntu/examples/iss708-2/test.rs line 4 column 13 function main
        // Labels: bb2
     1: ASSIGN main::1::var_8 := *(main::1::var_2::s.data + main::1::var_9)

where var_9 appears to be an unsigned integer.

[danielsn]

We currently enforce is_integer() not is_signed()
https://github.com/model-checking/kani/blob/main/cprover_bindings/src/goto_program/expr.rs#L832

[tautschnig]

Resolving as #6541 has been merged. Kani may nevertheless want to move to a model where all pointer arithmetic uses signed bitvectors.