CBMC 5.95.1 crashes on proof of simple array equality function

[rod-chapman]

CBMC version: 5.95.1
Operating system: macOS 13.6.6
Exact command line resulting in the issue: See linked GitHub Repo
What behaviour did you expect: proof
What happened instead: crash.

CBMC crashes trying to prove correctness of a simple function that compares arrays for equality.
See code in
https://github.com/rod-chapman/cbmc-examples/blob/20a559b99287945ab8a390689b14fb35316ea882/arrays/ar.c#L169

In that directory, the command

make TARGET=constant_time_equals_strict

produces

goto-cc --function constant_time_equals_strict_harness -DCBMC -o ar.goto ar.c
goto-instrument --dfcc constant_time_equals_strict_harness --apply-loop-contracts --enforce-contract constant_time_equals_strict ar.goto ar_contracts.goto
Reading GOTO program from 'ar.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Loading CPROVER C library (arm64)
Adding the cprover_contracts library (arm64)
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
Instrumenting harness function 'constant_time_equals_strict_harness'
Wrapping 'constant_time_equals_strict' with contract 'constant_time_equals_strict' in CHECK mode
No decrease clause provided for loop constant_time_equals_strict_wrapped_for_contract_checking.0 at file ar.c line 175 function constant_time_equals_strict. Termination will not be checked.
no body for function '__CPROVER_assignable'
Instrumenting 'f1'
Instrumenting 'f3_harness'
Instrumenting 'f2'
Instrumenting 'arsum_blocks1'
No invariant provided for loop arsum_blocks1.0 at file ar.c line 49 function arsum_blocks1. Using 'true' as a sound default invariant. Please provide an invariant the default is too weak.
No decrease clause provided for loop arsum_blocks1.0 at file ar.c line 49 function arsum_blocks1. Termination will not be checked.
no body for function '__CPROVER_assignable'
Instrumenting 'assign_st2'
No decrease clause provided for loop assign_st2.0 at file ar.c line 150 function assign_st2. Termination will not be checked.
file ar.c line 151 function assign_st2: no body for function '__CPROVER_object_whole'
no body for function '__CPROVER_assignable'
Instrumenting 'f3'
Instrumenting '__builtin___memcpy_chk'
Instrumenting 'assign_st2_harness'
Instrumenting 'arsum_blocks1_harness'
Instrumenting 'assign_st3_harness'
Instrumenting 'arsum_blocks2'
No decrease clause provided for loop arsum_blocks2.0 at file ar.c line 75 function arsum_blocks2. Termination will not be checked.
no body for function '__CPROVER_assignable'
Instrumenting 'arsum_bytes1'
No invariant provided for loop arsum_bytes1.0 at file ar.c line 100 function arsum_bytes1. Using 'true' as a sound default invariant. Please provide an invariant the default is too weak.
No decrease clause provided for loop arsum_bytes1.0 at file ar.c line 100 function arsum_bytes1. Termination will not be checked.
no body for function '__CPROVER_assignable'
Instrumenting 'arsum_blocks2_harness'
Instrumenting 'arsum_bytes2'
No decrease clause provided for loop arsum_bytes2.0 at file ar.c line 118 function arsum_bytes2. Termination will not be checked.
no body for function '__CPROVER_assignable'
Instrumenting 'assign_st1'
Instrumenting 'arsum_bytes1_harness'
Instrumenting 'assign_st3'
Instrumenting 'arsum_bytes2_harness'
Instrumenting 'f1_harness'
Instrumenting 'f2_harness'
Instrumenting 'assign_st1_harness'
Instrumenting 'malloc'
Instrumenting 'free'
Specializing cprover_contracts functions for assigns clauses of at most 3 targets
Removing unused functions
Dropping 77 of 99 functions (22 used)
Updating init function
Setting entry point to constant_time_equals_strict_harness
Writing GOTO program to 'ar_contracts.goto'
cbmc --verbosity 6 --bounds-check --pointer-check --memory-cleanup-check --div-by-zero-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --external-sat-solver cadical ar_contracts.goto
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 macos
Reading GOTO program from file ar_contracts.goto
Generating GOTO Program
Adding CPROVER library (arm64)
file <builtin-library-__builtin___memcpy_chk> line 2: warning:  "__builtin___memcpy_chk"
old definition in module  file <builtin-architecture-strings> line 20
void * (void *__param$0, const void *__param$1, __CPROVER_size_t __param$2, __CPROVER_size_t __param$3, __CPROVER_contracts_write_set_ptr_t __write_set_to_check)
new definition in module <built-in-library> file <builtin-library-__builtin___memcpy_chk> line 2
void * (void *dst, const void *src, __CPROVER_size_t n, __CPROVER_size_t size)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
--- begin invariant violation report ---
Invariant check failed
File: /tmp/cbmc-20231030-8059-htxuhd/src/goto-symex/renaming_level.cpp:36 function: symex_level0
Condition: found_l0
Reason: level0: failed to find constant_time_equals_strict::1::1::1::j
Backtrace:
0   cbmc                                0x00000001051b2980 _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 120
1   cbmc                                0x00000001051b2cd0 _Z13get_backtracev + 44
2   cbmc                                0x0000000104ce3960 _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 52
3   cbmc                                0x0000000104ce392c _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 0
4   cbmc                                0x0000000104dd9904 _Z12symex_level09ssa_exprtRK10namespacetm + 412
5   cbmc                                0x0000000104dbe5cc _ZN17goto_symex_statet11set_indicesIL6levelt1EEE8renamedtI9ssa_exprtXT_EES3_RK10namespacet + 68
6   cbmc                                0x0000000104dbef40 _ZN17goto_symex_statet10rename_ssaIL6levelt1EEE8renamedtI9ssa_exprtXT_EES3_RK10namespacet + 72
7   cbmc                                0x0000000104dc4504 _ZN17goto_symex_statet6renameIL6levelt1EEE8renamedtI5exprtXT_EES3_RK10namespacet + 156
8   cbmc                                0x0000000104dc46d0 _ZN17goto_symex_statet6renameIL6levelt1EEE8renamedtI5exprtXT_EES3_RK10namespacet + 616
9   cbmc                                0x0000000104dc4794 _ZN17goto_symex_statet6renameIL6levelt1EEE8renamedtI5exprtXT_EES3_RK10namespacet + 812
10  cbmc                                0x0000000104dc4794 _ZN17goto_symex_statet6renameIL6levelt1EEE8renamedtI5exprtXT_EES3_RK10namespacet + 812
11  cbmc                                0x0000000104dc4794 _ZN17goto_symex_statet6renameIL6levelt1EEE8renamedtI5exprtXT_EES3_RK10namespacet + 812
12  cbmc                                0x0000000104dfe9ac _ZN11goto_symext11dereferenceER5exprtR17goto_symex_statetb + 268
13  cbmc                                0x0000000104dfac18 _ZN11goto_symext10clean_exprE5exprtR17goto_symex_statetb + 84
14  cbmc                                0x0000000104e09a64 _ZN11goto_symext12symex_assertERKN13goto_programt12instructiontER17goto_symex_statet + 76
15  cbmc                                0x0000000104e0c410 _ZN11goto_symext24execute_next_instructionERKNSt3__18functionIFRK14goto_functiontRK8dstringtEEER17goto_symex_statet + 440
16  cbmc                                0x0000000104e0c240 _ZN11goto_symext10symex_stepERKNSt3__18functionIFRK14goto_functiontRK8dstringtEEER17goto_symex_statet + 52
17  cbmc                                0x0000000104d0c76c _ZN10symex_bmct10symex_stepERKNSt3__18functionIFRK14goto_functiontRK8dstringtEEER17goto_symex_statet + 600
18  cbmc                                0x0000000104e0af28 _ZN11goto_symext19symex_threaded_stepER17goto_symex_statetRKNSt3__18functionIFRK14goto_functiontRK8dstringtEEE + 44
19  cbmc                                0x0000000104e0b194 _ZN11goto_symext16symex_with_stateER17goto_symex_statetRKNSt3__18functionIFRK14goto_functiontRK8dstringtEEE + 184
20  cbmc                                0x0000000104e0ba68 _ZN11goto_symext25symex_from_entry_point_ofERKNSt3__18functionIFRK14goto_functiontRK8dstringtEEERK32shadow_memory_field_definitionst + 124
21  cbmc                                0x0000000104cfbae0 _ZN30multi_path_symex_only_checkert17generate_equationEv + 112
22  cbmc                                0x0000000104cfaae0 _ZN25multi_path_symex_checkertclERNSt3__13mapI8dstringt14property_infotNS0_4lessIS2_EENS0_9allocatorINS0_4pairIKS2_S3_EEEEEE + 92
23  cbmc                                0x0000000104cf25e0 _ZN43all_properties_verifier_with_trace_storagetI25multi_path_symex_checkertEclEv + 64
24  cbmc                                0x0000000104cea404 _ZN19cbmc_parse_optionst4doitEv + 2908
25  cbmc                                0x00000001051db210 _ZN19parse_options_baset4mainEv + 180
26  cbmc                                0x0000000104ce3270 main + 48
27  dyld                                0x0000000182407f28 start + 2236


--- end invariant violation report ---
make: *** [results] Abort trap: 6

[qinheping]

In loop contracts, we replace quantified variables with a tmp variable and add the tmp variable to the symbol map. However, the detection of the quantified variables is not complete now: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/contracts/utils.cpp#L425. It does not include equal expression. The error doesn't persist once I add the equal expression to the detection.

[qinheping]

As a workaround before the fix is merged, you may want to use the boolean variable arrays_not_match and invariant arrays_not_match != __CPROVER_forall instead.

[rod-chapman]

Please let me know when this fix is merged.

[rod-chapman]

I tried inverting the logic and using != instead of ==, but I don't like it because it makes the code much harder to read and understand.

With that change, I get 2 warnings that say "warning: ignoring forall" which are followed by a print out of some syntax tree. What does that mean?

[remi-delmas-3000]

"warning: ignoring forall"

The SAT backend eagerly grounds quantifiers when domains are small, but ignores them when domains are too large, which is seems to be the case here. You should try using the SMT back-end to solve this example, quantifiers are passed to the SMT back-end and grounded using the solver's heuristics.

[rod-chapman]

OK. Please improve the error message to make it clearer what's wrong and what the corrective action should be.

[qinheping]

Please let me know when this fix is merged.

#8299 was merged.