Open rod-chapman opened 4 days ago
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 ---
loop_entry
should only be used in loop contracts. Will clarify in the error massage.
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?
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
.
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?
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?
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.
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.