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?

[SaswatPadhi]

Sorry about the late response. We had discussed this issue briefly during our weekly meeting with Diffblue. @jimgrundy and @feliperodri have been working on function contracts and haven't encountered this issue any more, so we believe it's fixed now.
As you suggested above, we can close to issue since it was about specific change that has now been reverted. We could track array handling issues separately.

Thanks again for the fix!