Skip to content

Make array manipulation more robust #126

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
xbauch opened this issue Feb 18, 2019 · 2 comments
Open

Make array manipulation more robust #126

xbauch opened this issue Feb 18, 2019 · 2 comments

Comments

@xbauch
Copy link
Contributor

xbauch commented Feb 18, 2019 •
edited
Loading

For example on the following Ada code (in PR#124):

procedure Array_Append_Irep is
   type Arr_Long is array (1..4) of Integer;
   Full_Arr : Arr_Long := (1,2,3,4);
   Part1_Arr : Arr_Long := (1,2,0,0);
   Part2_Arr : Arr_Long := (3,4,0,0);
begin
   Full_Arr(1..4) := Full_Arr(3..4) & Full_Arr(1..2);
   pragma Assert(Full_Arr(1)=3);
   pragma Assert(Full_Arr(2)=4);
   pragma Assert(Full_Arr(3)=1);
   pragma Assert(Full_Arr(4)=2);
   Full_Arr(1..4) := Part2_Arr(1..2) & Part1_Arr(1..2);
   pragma Assert(Full_Arr(1)=3);
end Array_Append_Irep;

CBMC verification succeeds.

procedure Array_Append_Irep is
   type Arr_Long is array (1..4) of Integer;
   Full_Arr : Arr_Long := (1,2,3,4);
   Part1_Arr : Arr_Long := (1,2,0,0);
   Part2_Arr : Arr_Long := (3,4,0,0);
begin
   Full_Arr(1..4) := Full_Arr(3..4) & Full_Arr(1..2);
   pragma Assert(Full_Arr(1)=3);
   --pragma Assert(Full_Arr(2)=4);
   pragma Assert(Full_Arr(3)=1);
   pragma Assert(Full_Arr(4)=2);
   Full_Arr(1..4) := Part2_Arr(1..2) & Part1_Arr(1..2);
   pragma Assert(Full_Arr(1)=3);
end Array_Append_Irep;

CBMC verification fails in one memcpy overlap.

procedure Array_Append_Irep is
   type Arr_Long is array (1..4) of Integer;
   Full_Arr : Arr_Long := (1,2,3,4);
   Part1_Arr : Arr_Long := (1,2,0,0);
   Part2_Arr : Arr_Long := (3,4,0,0);
begin
   Full_Arr(1..4) := Full_Arr(3..4) & Full_Arr(1..2);
   pragma Assert(Full_Arr(1)=3);
   --pragma Assert(Full_Arr(2)=4);
   pragma Assert(Full_Arr(3)=1);
   --pragma Assert(Full_Arr(4)=2);
   Full_Arr(1..4) := Part2_Arr(1..2) & Part1_Arr(1..2);
   pragma Assert(Full_Arr(1)=3);
end Array_Append_Irep;

CBMC crashed in symex (because the size of memcpy(ed) array is not known to be constant).
@xbauch
Copy link
Contributor Author

xbauch commented Feb 18, 2019

Here's the error output for the crash case:

$ cbmc array_append_irep.json_symtab 
CBMC version 5.11 (cbmc-5.11-850-g71bdebf63) 64-bit x86_64 linux
Parsing array_append_irep.json_symtab
Converting
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
size of program expression: 651 steps
simple slicing removed 2 assignments
Generated 42 VCC(s), 4 remaining after simplification
Passing problem to propositional reduction
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: /home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/solvers/lowering/byte_operators.cpp:361 function: lower_byte_update
Condition: size of type in bytes must be known
Reason: element_size_opt.has_value()
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x4d) [0x55d0846e23ba]
cbmc(get_backtrace[abi:cxx11]()+0x45) [0x55d0846e25c1]
cbmc(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> >&&)+0x53) [0x55d08429c7bb]
cbmc(void report_invariant_failure<irep_pretty_diagnosticst>(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> >, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, irep_pretty_diagnosticst&&)+0x72) [0x55d08429c5d6]
cbmc(+0xa954ab) [0x55d08457f4ab]
cbmc(+0xa97a6b) [0x55d084581a6b]
cbmc(lower_byte_operators(exprt const&, namespacet const&)+0x15f) [0x55d084581d34]
cbmc(lower_byte_operators(exprt const&, namespacet const&)+0xb4) [0x55d084581c89]
cbmc(boolbvt::convert_equality(equal_exprt const&)+0x24a) [0x55d08452ba88]
cbmc(boolbvt::convert_rest(exprt const&)+0x1fe) [0x55d084513eaa]
cbmc(bv_pointerst::convert_rest(exprt const&)+0x898) [0x55d084556356]
cbmc(prop_conv_solvert::convert_bool(exprt const&)+0x13ec) [0x55d08458aab6]
cbmc(prop_conv_solvert::convert(exprt const&)+0x19d) [0x55d084589619]
cbmc(prop_conv_solvert::set_to(exprt const&, bool)+0x797) [0x55d08458b7f3]
cbmc(boolbvt::set_to(exprt const&, bool)+0x1bc) [0x55d0845167d6]
cbmc(decision_proceduret::set_to_true(exprt const&)+0x30) [0x55d0843b15ae]
cbmc(symex_target_equationt::convert_assignments(decision_proceduret&) const+0x104) [0x55d0843abf58]
cbmc(symex_target_equationt::convert(prop_convt&)+0x48) [0x55d0843abcce]
cbmc(convert_symex_target_equation(symex_target_equationt&, prop_convt&, message_handlert&)+0x91) [0x55d084150ad3]
cbmc(bmc_all_propertiest::operator()()+0x152) [0x55d084148378]
cbmc(bmct::all_properties(goto_functionst const&)+0x8b) [0x55d08414a2ff]
cbmc(bmct::decide(goto_functionst const&)+0xe7) [0x55d08411ff67]
cbmc(bmct::execute(abstract_goto_modelt&)+0x8a6) [0x55d08411f942]
cbmc(bmct::run(abstract_goto_modelt&)+0xb4) [0x55d08411fe6a]
cbmc(bmct::do_language_agnostic_bmc(optionst const&, abstract_goto_modelt&, ui_message_handlert&, std::function<void (bmct&, symbol_tablet const&)>, std::function<bool ()>)+0x2d3) [0x55d0841208b3]
cbmc(cbmc_parse_optionst::doit()+0xa1b) [0x55d08411253f]
cbmc(parse_options_baset::main()+0x10f) [0x55d0847078a7]
cbmc(main+0x55) [0x55d084108ebf]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7) [0x7f7f63fbfb97]
cbmc(_start+0x2a) [0x55d084108d8a]

Diagnostics: 
<< EXTRA DIAGNOSTICS >>
byte_update_little_endian
  * type: array
      * size: symbol
          * type: unsignedbv
              * width: 64
          * identifier: symex_dynamic::dynamic_object_size8!0#1
          * expression: symbol
              * type: unsignedbv
                  * width: 64
              * identifier: symex_dynamic::dynamic_object_size8
          * #SSA_symbol: 1
          * L0: 0
          * L2: 1
          * L1_object_identifier: symex_dynamic::dynamic_object_size8!0
      * #dynamic: 1
      0: unsignedbv
          * width: 8
          * #c_type: unsigned_char
  0: symbol
      * type: array
          * size: symbol
              * type: unsignedbv
                  * width: 64
              * identifier: symex_dynamic::dynamic_object_size8!0#1
              * expression: symbol
                  * type: unsignedbv
                      * width: 64
                  * identifier: symex_dynamic::dynamic_object_size8
              * #SSA_symbol: 1
              * L0: 0
              * L2: 1
              * L1_object_identifier: symex_dynamic::dynamic_object_size8!0
          * #dynamic: 1
          0: unsignedbv
              * width: 8
              * #c_type: unsigned_char
      * identifier: symex_dynamic::dynamic_object8#1
      * expression: symbol
          * type: array
              * size: symbol
                  * type: unsignedbv
                      * width: 64
                  * identifier: symex_dynamic::dynamic_object_size8!0#1
                  * expression: symbol
                      * type: unsignedbv
                          * width: 64
                      * identifier: symex_dynamic::dynamic_object_size8
                  * #SSA_symbol: 1
                  * L0: 0
                  * L2: 1
                  * L1_object_identifier: symex_dynamic::dynamic_object_size8!0
              * #dynamic: 1
              0: unsignedbv
                  * width: 8
                  * #c_type: unsigned_char
          * identifier: symex_dynamic::dynamic_object8
      * #SSA_symbol: 1
      * L2: 1
      * L1_object_identifier: symex_dynamic::dynamic_object8
  1: constant
      * type: signedbv
          * width: 64
          * #c_type: signed_long_int
      * value: 0
  2: symbol
      * type: array
          * #source_location: 
            * file: <builtin-library-memcpy>
            * line: 44
            * function: memcpy
            * working_directory: /home/diffblue/petr.bauch/code/gnat2goto/testsuite/gnat2goto/tests/array_append_irep
          * size: symbol
              * type: signedbv
                  * width: 64
                  * #c_type: signed_long_int
              * identifier: memcpy::1::1::src_n$array_size0!0@9#2
              * expression: symbol
                  * type: signedbv
                      * width: 64
                      * #c_type: signed_long_int
                  * identifier: memcpy::1::1::src_n$array_size0
              * #SSA_symbol: 1
              * L0: 0
              * L1: 9
              * L2: 2
              * L1_object_identifier: memcpy::1::1::src_n$array_size0!0@9
          0: signedbv
              * width: 8
              * #c_type: char
      * identifier: memcpy::1::1::src_n!0@9#2
      * expression: symbol
          * type: array
              * #source_location: 
                * file: <builtin-library-memcpy>
                * line: 44
                * function: memcpy
                * working_directory: /home/diffblue/petr.bauch/code/gnat2goto/testsuite/gnat2goto/tests/array_append_irep
              * size: symbol
                  * type: signedbv
                      * width: 64
                      * #c_type: signed_long_int
                  * identifier: memcpy::1::1::src_n$array_size0!0@9#2
                  * expression: symbol
                      * type: signedbv
                          * width: 64
                          * #c_type: signed_long_int
                      * identifier: memcpy::1::1::src_n$array_size0
                  * #SSA_symbol: 1
                  * L0: 0
                  * L1: 9
                  * L2: 2
                  * L1_object_identifier: memcpy::1::1::src_n$array_size0!0@9
              0: signedbv
                  * width: 8
                  * #c_type: char
          * #source_location: 
            * file: <builtin-library-memcpy>
            * line: 44
            * function: memcpy
            * working_directory: /home/diffblue/petr.bauch/code/gnat2goto/testsuite/gnat2goto/tests/array_append_irep
          * identifier: memcpy::1::1::src_n
      * #SSA_symbol: 1
      * L0: 0
      * L1: 9
      * L2: 2
      * L1_object_identifier: memcpy::1::1::src_n!0@9
<< END EXTRA DIAGNOSTICS >>

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

@xbauch
Copy link
Contributor Author

xbauch commented Feb 18, 2019

Relevant part of symex for each case:

(271) __dest_array50!0@1#1 == { .first1=1, .last1=4, .data=(int *)dynamic_object1 }
// 46 
(272) __array_rhs51!0@1#1 == { .first1=1, .last1=2, .data=(int *)dynamic_object3 }
// 46 
(273) __array_rhs52!0@1#1 == { .first1=1, .last1=2, .data=(int *)dynamic_object2 }
// 204 file array_append_irep.adb line 12 column 19
(274) __offset_step53!0#1 == 0
// 205 file array_append_irep.adb line 12 column 19
(275) __sum_size55!0#1 == 0
// 206 file array_append_irep.adb line 12 column 19
(276) __sum_size55!0#2 == 2
// 207 file array_append_irep.adb line 12 column 19
(277) __sum_size55!0#3 == 4
// 208 file array_append_irep.adb line 12 column 19
// 209 
// 209 
// 209 
(278) malloc_size!0@7#1 == 16

Correct case.

(270) __array_rhs51!0@1#1 == { .first1=1, .last1=4, .data=(int *)dynamic_object1 }
// 45 
(271) __array_rhs52!0@1#1 == { .first1=1, .last1=2, .data=(int *)dynamic_object3 }
// 203 file array_append_irep.adb line 12 column 19
(272) __offset_step53!0#1 == 0
// 204 file array_append_irep.adb line 12 column 19
(273) __sum_size55!0#1 == 0
// 205 file array_append_irep.adb line 12 column 19
(274) __sum_size55!0#2 == 4
// 206 file array_append_irep.adb line 12 column 19
(275) __sum_size55!0#3 == 6
// 207 file array_append_irep.adb line 12 column 19
// 208 
// 208 
// 208 
(276) malloc_size!0@7#1 == 24

Overlap case.

(269) __dest_array50!0@1#1 == { .first1=1, .last1=4, .data=(int *)dynamic_object1 }
// 44 
(270) __array_rhs52!0@1#1 == { .first1=1, .last1=2, .data=(int *)dynamic_object3 }
// 202 file array_append_irep.adb line 12 column 19
(271) __offset_step53!0#1 == 0
// 203 file array_append_irep.adb line 12 column 19
(272) __sum_size55!0#1 == 0
// 204 file array_append_irep.adb line 12 column 19
(273) __sum_size55!0#2 == (unsigned long int)(1 + __array_rhs51!0#0.last1 + -__array_rhs51!0#0.first1)
// 205 file array_append_irep.adb line 12 column 19
(274) __sum_size55!0#3 == 2 + __sum_size55!0#2
// 206 file array_append_irep.adb line 12 column 19
// 207 
// 207 
// 207 
(275) malloc_size!0@7#1 == 4 * __sum_size55!0#3

Crashing case.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@xbauch