Commit `cd1ec89b` breaks proofs

[SaswatPadhi]

CBMC version: develop (currently 06c563a)
Operating system: Mac OS / Linux

Exact command line resulting in the issue:
We don't have a "small" example yet, but here is a broken proof harness from s2n:

$ git clone https://github.com/aws/s2n-tls.git && cd s2n-tls
$ git submodule update --init --checkout --recursive
$ cd tests/cbmc/proofs/s2n_socket_write_cork
$ make result

What behaviour did you expect:
This harnesses can still be verified after updating CBMC.

What happened instead:
CBMC crashes with an invariant violation:

--- begin invariant violation report ---
Invariant check failed
File: /Users/jmgruj/cbmc/src/solvers/flattening/arrays.cpp:200 function: collect_arrays
Condition: struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol
Reason: unexpected array expression: member with 'member'
Backtrace:
0   cbmc                                0x000000010ab25eea _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
1   cbmc                                0x000000010ab26482 _Z13get_backtracev + 210
2   cbmc                                0x000000010a56130c _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 44
3   cbmc                                0x000000010a5612d9 _Z25invariant_violated_stringRKNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEES7_iS7_S7_ + 9
4   cbmc                                0x000000010a9081ab _ZN7arrayst14collect_arraysERK5exprt + 1451
5   cbmc                                0x000000010a9077e6 _ZN7arrayst21record_array_equalityERK11equal_exprt + 422
6   cbmc                                0x000000010a94de01 _ZN12bv_pointerst12convert_restERK5exprt + 1185
7   cbmc                                0x000000010a9a5358 _ZN17prop_conv_solvert12convert_boolERK5exprt + 2616
8   cbmc                                0x000000010a9a48a9 _ZN17prop_conv_solvert7convertERK5exprt + 905
9   cbmc                                0x000000010a9a62d2 _ZN17prop_conv_solvert23add_constraints_to_propERK5exprtb + 1026
10  cbmc                                0x000000010a6e4d55 _ZN22symex_target_equationt19convert_assignmentsER19decision_proceduret + 261
11  cbmc                                0x000000010a6e49b5 _ZN22symex_target_equationt26convert_without_assertionsER19decision_proceduret + 117
12  cbmc                                0x000000010a6e6163 _ZN22symex_target_equationt7convertER19decision_proceduret + 35
13  cbmc                                0x000000010a5775f6 _Z29convert_symex_target_equationR22symex_target_equationtR19decision_proceduretR16message_handlert + 342
14  cbmc                                0x000000010a5795a9 _Z24prepare_property_deciderRNSt3__113unordered_mapI8dstringt14property_infotNS_4hashIS1_EENS_8equal_toIS1_EENS_9allocatorINS_4pairIKS1_S2_EEEEEER22symex_target_equationtR28goto_symex_property_decidertR19ui_message_handlert + 441
15  cbmc                                0x000000010a581757 _ZN25multi_path_symex_checkertclERNSt3__113unordered_mapI8dstringt14property_infotNS0_4hashIS2_EENS0_8equal_toIS2_EENS0_9allocatorINS0_4pairIKS2_S3_EEEEEE + 247
16  cbmc                                0x000000010a575283 _ZN43all_properties_verifier_with_trace_storagetI25multi_path_symex_checkertEclEv + 51
17  cbmc                                0x000000010a56b372 _ZN19cbmc_parse_optionst4doitEv + 4290
18  cbmc                                0x000000010ab4290c _ZN19parse_options_baset4mainEv + 140
19  cbmc                                0x000000010a560a98 main + 40
20  libdyld.dylib                       0x00007fff203c8f5d start + 1
21  ???                                 0x0000000000000017 0x0 + 23
 
 
--- end invariant violation report ---

Additional context:

I have verified that cd1ec89 is indeed the buggy commit. I tried:

$ cd cbmc
$ git revert cd1ec89b -m 1
$ ... recompile ...

And the generated binaries no longer crash on the harness.

[SaswatPadhi]

cc: @feliperodri @jimgrundy

[martin-cs]

My apologies; I approved #6194 . This looks like a crash caused by a knock-on effect of one of these changes rather than directly in the code. If I had to speculate I might guess the change from unbounded_arrayt::U_NONE to unbounded_arrayt::U_AUTO might be it. If you have a moment to test, you could try just reverting that.

It feels like it should be safe to revert this and attempt the PR again with more testing.

[SaswatPadhi]

Thanks @martin-cs!

Yes, reverting to unbounded_arrayt::U_NONE from unbounded_arrayt::U_AUTO indeed fixes this crash.

[martin-cs]

#6232 reverts just that part of #6194 and should do as a hot fix. If you have a test case that triggers the problem, that would be a great addition to the patch. My guess is that it is something that involves an unusually large or sort-of dynamically sized array.

[martin-cs]

#6232 has been merged and #6243 adds your test case. Please confirm whether this is fixed.

[SaswatPadhi]

On my simpler example and the s2n harness, the fix works as expected. Thanks!

@jimgrundy could you please retry the s2n harness that had contracts (since I don't have it).

Should we keep this issue open until we figure out why cd1ec89b introduced this crash (and why reverting to unbounded_arrayt::U_NONE fixed it)?

[martin-cs]

@SaswatPadhi I would rather further investigations and changes to the array handling were on a separate issue because I think there is a non-trivial amount of work to do there. If the break is resolved then I would suggest closing this issue (but, by all means, open another one on the topic).

[SaswatPadhi]

Thanks, makes sense. I would check with Jim and we can close this issue by EoD tomorrow if this is fully resolved (most likely it is).

[martin-cs]

@SaswatPadhi Ping?