Invariant violation coming from byte operators

[adpaco]

CBMC version: 5.20.1 (but appears to be present in 5.18 as well)
Operating system: macOs 10.15
Exact command line resulting in the issue: make on verification/cbmc/proofs/aws_cryptosdk_priv_unwrap_keys in branch CBMC-ISSUE-5718
What behaviour did you expect: No errors.
What happened instead: Received the following invariant violation report.

--- begin invariant violation report ---
Invariant check failed
File: /tmp/cbmc-20201210-58015-1j6vaer/src/solvers/lowering/byte_operators.cpp:1252 function: lower_byte_extract
Condition: subtype_bits.has_value() && *subtype_bits == 8
Reason: offset bits are byte aligned
Backtrace:
0   cbmc                                0x000000010a64b6fa _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
1   cbmc                                0x000000010a64bbeb _Z13get_backtracev + 167
2   cbmc                                0x000000010a6b469c _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 44
3   cbmc                                0x000000010a65c369 _Z25invariant_violated_stringRKNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEES7_iS7_S7_ + 9
4   cbmc                                0x000000010a52df9b _Z18lower_byte_extractRK18byte_extract_exprtRK10namespacet + 9291
5   cbmc                                0x000000010a52de07 _Z18lower_byte_extractRK18byte_extract_exprtRK10namespacet + 8887
6   cbmc                                0x000000010a53705e _Z20lower_byte_operatorsRK5exprtRK10namespacet + 275
7   cbmc                                0x000000010a536fc8 _Z20lower_byte_operatorsRK5exprtRK10namespacet + 125
8   cbmc                                0x000000010a536fc8 _Z20lower_byte_operatorsRK5exprtRK10namespacet + 125
9   cbmc                                0x000000010a4ecae4 _ZN7boolbvt16convert_equalityERK11equal_exprt + 180
10  cbmc                                0x000000010a50812c _ZN12bv_pointerst12convert_restERK5exprt + 940
11  cbmc                                0x000000010a544302 _ZN17prop_conv_solvert12convert_boolERK5exprt + 2548
12  cbmc                                0x000000010a543897 _ZN17prop_conv_solvert7convertERK5exprt + 687
13  cbmc                                0x000000010a54505e _ZN17prop_conv_solvert23add_constraints_to_propERK5exprtb + 992
14  cbmc                                0x000000010a34da87 _ZN22symex_target_equationt19convert_assignmentsER19decision_proceduret + 243
15  cbmc                                0x000000010a34d718 _ZN22symex_target_equationt26convert_without_assertionsER19decision_proceduret + 116
16  cbmc                                0x000000010a34eb85 _ZN22symex_target_equationt7convertER19decision_proceduret + 35
17  cbmc                                0x000000010a23f5e2 _Z29convert_symex_target_equationR22symex_target_equationtR19decision_proceduretR16message_handlert + 125
18  cbmc                                0x000000010a240b36 _Z24prepare_property_deciderRNSt3__113unordered_mapI8dstringt14property_infotNS_4hashIS1_EENS_8equal_toIS1_EENS_9allocatorINS_4pairIKS1_S2_EEEEEER22symex_target_equationtR28goto_symex_property_decidertR19ui_message_handlert + 223
19  cbmc                                0x000000010a246cc8 _ZN25multi_path_symex_checkertclERNSt3__113unordered_mapI8dstringt14property_infotNS0_4hashIS2_EENS0_8equal_toIS2_EENS0_9allocatorINS0_4pairIKS2_S3_EEEEEE + 218
20  cbmc                                0x000000010a23db9b _ZN43all_properties_verifier_with_trace_storagetI25multi_path_symex_checkertEclEv + 55
21  cbmc                                0x000000010a2378f3 _ZN19cbmc_parse_optionst4doitEv + 3647
22  cbmc                                0x000000010a6606ac _ZN19parse_options_baset4mainEv + 136
23  cbmc                                0x000000010a22f5ec main + 44
24  libdyld.dylib                       0x00007fff6fe9ccc9 start + 1


--- end invariant violation report ---

[tautschnig]

I do now have a patch for this problem, but still need to figure out what a small regression test could look like.

[adpaco]

That is great, @tautschnig! Can you explain where the problem comes from? I did not have time to debug this myself and I am curious 😀

[hannes-steffenhagen-diffblue]

Ah yes, we've been working on this (we're stuck at the same thing, coming up with a regression test).

@tautschnig We were thinking this was the problem - since unpack should return a byte array expression this should be bv_typet{8}, not the original subtype. Was that the same thing you saw or did you identify another problem? We were also currently in progress of trying to find a sensible reproducer that we could in our regression tests.

[tautschnig]

@adpaco-aws There now is a fix in #5750, but I do need to warn you that while this solves the original problem you'll now most likely run into out-of-memory problems as the resulting expressions very heavily rely on the array decision procedure. I stop my CBMC run at around 65 GB of memory. The culprit is that some of your code is trying to copy (via memcpy) an unconstrained number of bytes out of an allocation that itself has an unconstrained size. The allocation happens in line 160 of make_common_data_structures.c (list->data = bounded_malloc(sizeof(struct aws_cryptosdk_edk) * max_length);). You might have to consider ways of further constraining those allocations (or the amount at some point being copied) until we have an improved array decision procedure merged.

[hannes-steffenhagen-diffblue]

@tautschnig I fixed the PR reference in your comment