Skip to content

Invariant check failed when using memset #5389

Closed
@feliperodri

Description

@feliperodri

CBMC version: 5.12 (cbmc-5.12.1-10-gdf2638c59)
Operating system: macOS Mojave Version 10.14.6
Exact command line resulting in the issue: Run s2n_array_new proof.
What behaviour did you expect: Verification Successful.
What happened instead: Invariant check failed.

To reproduce the error, clone cbmc-array-set-predicates branch and go to s2n/tests/cbmc/proofs/s2n_array_new dir. To run the proof harness, just enter make cbmc (you need goto-cc, goto-instrument, goto-analyzer, and cbmc on your $PATH). I got the following error message:

--- begin invariant violation report ---
Invariant check failed
File: flattening/boolbv_extractbits.cpp:37 function: convert_extractbits
Condition: upper end of extracted bits must be within the bitvector
Reason: upper_as_int >= 0 && upper_as_int < src_bv.size()
Backtrace:
0   cbmc                                0x000000010229f8ea _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
1   cbmc                                0x000000010229fe92 _Z13get_backtracev + 210
2   cbmc                                0x00000001022c3140 _Z29invariant_violated_structuredI34invariant_with_diagnostics_failedtJRNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEES7_EENS1_9enable_ifIXsr3std10is_base_ofI17invariant_failedtT_EE5valueEvE4typeERKS7_SF_iSF_DpOT0_ + 48
3   cbmc                                0x00000001020ffe88 _Z24report_invariant_failureIJRK16source_locationt24irep_pretty_diagnosticstEEvRKNSt3__112basic_stringIcNS4_11char_traitsIcEENS4_9allocatorIcEEEESC_iSA_SA_DpOT_ + 72
4   cbmc                                0x0000000102114c8f _ZN7boolbvt19convert_extractbitsERK17extractbits_exprt + 2031
5   cbmc                                0x0000000102100537 _ZN7boolbvt17convert_bitvectorERK5exprt + 1575
6   cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
7   cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
8   cbmc                                0x000000010211b71d _ZN7boolbvt10convert_ifERK8if_exprt + 173
9   cbmc                                0x0000000102100221 _ZN7boolbvt17convert_bitvectorERK5exprt + 785
10  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
11  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
12  cbmc                                0x0000000102109953 _ZN7boolbvt15convert_bitwiseERK5exprt + 387
13  cbmc                                0x00000001021005c5 _ZN7boolbvt17convert_bitvectorERK5exprt + 1717
14  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
15  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
16  cbmc                                0x0000000102129726 _ZN7boolbvt19convert_bv_typecastERK14typecast_exprt + 70
17  cbmc                                0x0000000102100275 _ZN7boolbvt17convert_bitvectorERK5exprt + 869
18  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
19  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
20  cbmc                                0x0000000102128677 _ZN7boolbvt14convert_structERK12struct_exprt + 391
21  cbmc                                0x0000000102100717 _ZN7boolbvt17convert_bitvectorERK5exprt + 2055
22  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
23  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
24  cbmc                                0x0000000102128677 _ZN7boolbvt14convert_structERK12struct_exprt + 391
25  cbmc                                0x0000000102100717 _ZN7boolbvt17convert_bitvectorERK5exprt + 2055
26  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
27  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
28  cbmc                                0x000000010210c466 _ZN7boolbvt19convert_byte_updateERK17byte_update_exprt + 182
29  cbmc                                0x00000001021006e7 _ZN7boolbvt17convert_bitvectorERK5exprt + 2007
30  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
31  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
32  cbmc                                0x000000010211b6f7 _ZN7boolbvt10convert_ifERK8if_exprt + 135
33  cbmc                                0x0000000102100221 _ZN7boolbvt17convert_bitvectorERK5exprt + 785
34  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
35  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
36  cbmc                                0x0000000102104238 _ZN7boolbvt27boolbv_set_equality_to_trueERK11equal_exprt + 200
37  cbmc                                0x0000000102104315 _ZN7boolbvt6set_toERK5exprtb + 101
38  cbmc                                0x00000001020247ec _ZN22symex_target_equationt19convert_assignmentsER19decision_proceduret + 204
39  cbmc                                0x0000000102024495 _ZN22symex_target_equationt26convert_without_assertionsER19decision_proceduret + 117
40  cbmc                                0x0000000102025ce2 _ZN22symex_target_equationt7convertER19decision_proceduret + 18
41  cbmc                                0x0000000101ecf7d6 _Z29convert_symex_target_equationR22symex_target_equationtR19decision_proceduretR16message_handlert + 342
42  cbmc                                0x0000000101ed16a9 _Z24prepare_property_deciderRNSt3__113unordered_mapI8dstringt14property_infotNS_4hashIS1_EENS_8equal_toIS1_EENS_9allocatorINS_4pairIKS1_S2_EEEEEER22symex_target_equationtR28goto_symex_property_decidertR19ui_message_handlert + 441
43  cbmc                                0x0000000101ed9288 _ZN25multi_path_symex_checkertclERNSt3__113unordered_mapI8dstringt14property_infotNS0_4hashIS2_EENS0_8equal_toIS2_EENS0_9allocatorINS0_4pairIKS2_S3_EEEEEE + 264
44  cbmc                                0x0000000102342237 _ZN40cover_goals_verifier_with_trace_storagetI25multi_path_symex_checkertEclEv + 87
45  cbmc                                0x000000010234047d _ZN19cbmc_parse_optionst4doitEv + 3565
46  cbmc                                0x00000001022b94e2 _ZN19parse_options_baset4mainEv + 242
47  cbmc                                0x000000010233b7f8 main + 40
48  libdyld.dylib                       0x00007fff5d05d3d5 start + 1
49  ???                                 0x000000000000000b 0x0 + 11

Diagnostics: 
<< EXTRA DIAGNOSTICS >>
source location: 
extractbits
  * type: bv
      * width: 8
  0: typecast
      * type: bv
          * width: 1
      0: symbol
          * type: c_bit_field
              * #source_location: 
                * file: /Users/felisous/Documents/aws/crypto/s2n/utils/s2n_blob.h
                * line: 37
                * function: 
                * working_directory: /Users/felisous/Documents/aws/crypto/s2n/tests/cbmc/proofs/s2n_array_new
              * width: 1
              0: unsignedbv
                  * width: 32
                  * #c_type: unsigned_int
          * identifier: symex_dynamic::dynamic_object3#29..mem..growable
          * expression: member
              * type: c_bit_field
                  * #source_location: 
                    * file: /Users/felisous/Documents/aws/crypto/s2n/utils/s2n_blob.h
                    * line: 37
                    * function: 
                    * working_directory: /Users/felisous/Documents/aws/crypto/s2n/tests/cbmc/proofs/s2n_array_new
                  * width: 1
                  0: unsignedbv
                      * width: 32
                      * #c_type: unsigned_int
              * component_name: growable
              0: member
                  * type: struct_tag
                      * #source_location: 
                        * file: /Users/felisous/Documents/aws/crypto/s2n/utils/s2n_array.c
                        * line: 47
                        * function: s2n_array_new
                        * working_directory: /Users/felisous/Documents/aws/crypto/s2n/tests/cbmc/proofs/s2n_array_new
                      * identifier: tag-s2n_blob
                  * component_name: mem
                  0: symbol
                      * type: struct_tag
                          * #source_location: 
                            * file: s2n_array_new_harness.c
                            * line: 36
                            * function: s2n_array_new_harness
                            * working_directory: /Users/felisous/Documents/aws/crypto/s2n/tests/cbmc/proofs/s2n_array_new
                          * identifier: tag-s2n_array
                      * identifier: symex_dynamic::dynamic_object3
          * #SSA_symbol: 1
          * L2: 29
          * L1_object_identifier: symex_dynamic::dynamic_object3..mem..growable
  1: constant
      * type: signedbv
          * width: 64
          * #c_type: signed_long_int
      * value: 7
  2: constant
      * type: signedbv
          * width: 64
          * #c_type: signed_long_int
      * value: 0
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---

Metadata

Metadata

Assignees

No one assigned

    Labels

    awsBugs or features of importance to AWS CBMC users

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions