CBMC crash if CPROVER_loop_entry is used inside an assertion inside a loop

[rod-chapman]

CBMC version: 6.2.0
Operating system: macOS

CBMC crashes if the __CPROVER_loop_entry() contract is used inside a __CPROVER_assert()
contract that is within a loop body.

Is this usage legal or not? It should either work, or should result in a clear error message.

Example code to follow.

[rod-chapman]

Example code here:
https://github.com/rod-chapman/cbmc-examples/tree/main/issues/8453

In that directory

make

yields

cbmc --bitwuzla main_contracts.goto
CBMC version 6.2.0 (cbmc-6.2.0) 64-bit arm64 macos
Reading GOTO program from file main_contracts.goto
Generating GOTO Program
Adding CPROVER library (arm64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to SMT2 QF_AUFBV (with FPA) using Bitwuzla
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: /Users/rodchap/Desktop/rod/tools/src/cbmc/src/solvers/smt2/smt2_conv.cpp:2483 function: convert_expr
Condition: smt2_convt::convert_expr should not be applied to unsupported type
Reason: false
Backtrace:
0   cbmc                                0x0000000102a4d118 _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 124
1   cbmc                                0x0000000102a4d5a4 _Z13get_backtracev + 160
2   cbmc                                0x00000001025722f0 _Z29invariant_violated_structuredI34invariant_with_diagnostics_failedtJRNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEES7_EENS1_9enable_ifIXsr3std10is_base_ofI17invariant_failedtT_EE5valueEvE4typeERKS7_SF_iSF_DpOT0_ + 60
3   cbmc                                0x00000001028950a4 _Z24report_invariant_failureIJRKNSt3__112basic_stringIcNS0_11char_traitsIcEENS0_9allocatorIcEEEEEEvS8_S8_iS6_S6_DpOT_ + 84
4   cbmc                                0x000000010290e8b8 _ZN10smt2_convt12convert_exprERK5exprt + 19124
5   cbmc                                0x000000010290d424 _ZN10smt2_convt12convert_exprERK5exprt + 13856
6   cbmc                                0x000000010290d424 _ZN10smt2_convt12convert_exprERK5exprt + 13856
7   cbmc                                0x000000010291091c _ZN10smt2_convt7convertERK5exprt + 916
8   cbmc                                0x0000000102915724 _ZN10smt2_convt6handleERK5exprt + 88
9   cbmc                                0x00000001026b36a4 _ZN22symex_target_equationt18convert_assertionsER19decision_proceduretb + 912
10  cbmc                                0x00000001026b32a0 _ZN22symex_target_equationt7convertER19decision_proceduret + 64
11  cbmc                                0x000000010254a6a0 _Z29convert_symex_target_equationR22symex_target_equationtR19decision_proceduretR16message_handlert + 264
12  cbmc                                0x000000010254bd7c _Z24prepare_property_deciderRNSt3__13mapI8dstringt14property_infotNS_4lessIS1_EENS_9allocatorINS_4pairIKS1_S2_EEEEEER22symex_target_equationtR28goto_symex_property_decidertR19ui_message_handlert + 380
13  cbmc                                0x0000000102557c54 _ZN25multi_path_symex_checkertclERNSt3__13mapI8dstringt14property_infotNS0_4lessIS2_EENS0_9allocatorINS0_4pairIKS2_S3_EEEEEE + 236
14  cbmc                                0x000000010254870c _ZN43all_properties_verifier_with_trace_storagetI25multi_path_symex_checkertEclEv + 84
15  cbmc                                0x0000000102540164 _ZN19cbmc_parse_optionst4doitEv + 3060
16  cbmc                                0x0000000102a77640 _ZN19parse_options_baset4mainEv + 180
17  cbmc                                0x0000000102534678 main + 40
18  dyld                                0x00000001a939bfd8 start + 2412

Diagnostics: 
<< EXTRA DIAGNOSTICS >>
loop_entry
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---

[qinheping]

loop_entry should only be used in loop contracts. Will clarify in the error massage.

[rod-chapman]

Why is it not permitted? I see no reason that it should not be allowed and work fine within an assertions that is within a loop. This form works perfectly well in SPARK, so what is the technical reason that CBMC should not allow it?

[qinheping]

Currently, we create a snapshot upon the entry of loop/function for each history variable we found in the contracts, and replace them with the snapshot variable. This happen when we apply contracts during goto-instrument. In genera, if we support the usage of history variables in assertions, such finding-snapshotting-replacing pass should be done cbmc as the assertions can be in some loops without loop contracts, which will be a substantial change to the current implementation.

Also, what the loop_entry of a variable referring to could be confusing in the cases of nested loops.
For example, in

    for (int i = 0; i < N; i++)
    __CPROVER_loop_invariants(1==1)
    {
        r[i] ++;
        for (int j = 0; j < N; j++)
        {
            int t = r[j];
            __CPROVER_assert(t == __CPROVER_loop_entry(r[j]), "Initial value of r[j]");
            r[j] = t + 1;
        }
    }

__CPROVER_loop_entry(r[j]) can refer to the history value of r[j] upon the entry of either the inner or the outer loop.

We may need a general history variable function __CPROVER_history(v, label) which refers to the value of v upon label.

[rod-chapman]

Ah yes... I can see the nesting issue... same in SPARK, where a loop can be optionally labelled with a name, and the "Loop_Entry" attribute can state the name. Without the name, it means "most closely enclosing loop statement." See section 5.5.3.1 here for all the rules:
https://docs.adacore.com/spark2014-docs/html/lrm/statements.html

I also see how this would be problematic if loop_entry was allowed in an assertion in a loop that didn't have an invariant. Perhaps it could be allowed only if the enclosing loop really did have an invariant?

[qinheping]

Perhaps it could be allowed only if the enclosing loop really did have an invariant?

Yes, this can be done by extending the current loop_entry usage. But its UX will still be confusing. If both nested loops have loop contracts, users won't be able to use loop_entry to refer to then entry of the outer loop.

Is any proof blocked by the lack of support of loop_entry in assertions? I think maybe we can implement the partial support if it is the case. @tautschnig What do you think?

[rod-chapman]

I had tried to use loop_entry in an assert to help me debug a failing proof, but it appears that the root cause of that is a related failing loop invariant proof. Once that's resolved, I think the other proofs will sort themselves out, so it's not blocking right now.

[rod-chapman]

On my test case (linked above), I see no change in behaviour at all from the latest wavefront build of CBMC. Did I miss something?

[qinheping]

No. Sorry I misunderstood your comment above. This issue should not be closed. I also reopened the PR #8456.