CBMC reporting incosistently assertion failures

[salvadorer]

Hi,
I notice that if I invoke cbmc without any arguments on the following code I see a warning about the assertion:

#include <assert.h>
extern void __VERIFIER_assume(int cond);
extern int __VERIFIER_nondet_int(void);
int main() {
  int N;
  if (__VERIFIER_nondet_int()) {
    N = 5;
  } else {
    N = 6;
    __VERIFIER_assume(0);
  }
  int arr[N];
  int j = 5;
  arr[j] = 5;
  assert(arr[j] == 5);
  return 0;
}

Result:
[main.assertion.1] line 15 assertion arr[j] == 5: FAILURE

I know that arr[j] is out-of bounds. Still the behavior is surprising since dropping the assumption results in 0 warnings even tough the array access might also be out of bounds in this case.

CBMC version: 5.95.1
Operating system: Ubuntu 22.04.3
Exact command line resulting in the issue: cbmc test.c

[kroening]

After removing the assumption, I get the following result:
[main.array_bounds.2] line 14 array 'arr' upper bound in arr[(signed long int)j]: FAILURE
This is undefined behaviour, i.e., the program after that point has no semantics, and the result for the assertion is meaningless. We are contemplating to remove the output for those.

[salvadorer]

This is what I get when removing the assertion:

:$ cbmc test.c 
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.000647728s
size of program expression: 36 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 6.136e-06s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000158277s
Running propositional reduction
Post-processing
Runtime Post-process: 6.5948e-05s
Solving with MiniSAT 2.2.1 with simplifier
366 variables, 296 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 7.4708e-05s
Runtime decision procedure: 0.000250526s

** Results:
test.c function main
[main.assertion.1] line 14 assertion arr[j] == 5: SUCCESS

** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL

So I do not get warnings about out-of-bounds accesses. Also how come that the verification result differs once I replace usages of j by 5?

[kroening]

On version 5.95.1 you need to add the option --bounds-check to enable the array bounds checks. This behaviour changes with version 6.0, where it is on by default.

[salvadorer]

Even with --bounds-check, we get the following results:
Version with assumption:

** Results:
test.c function main
[main.array_bounds.1] line 14 array 'arr' lower bound in arr[(signed long int)j]: SUCCESS
[main.array_bounds.2] line 14 array 'arr' upper bound in arr[(signed long int)j]: FAILURE
[main.assertion.1] line 15 assertion arr[j] == 5: FAILURE

Version without assumption:

** Results:
test.c function main
[main.array_bounds.1] line 14 array 'arr' lower bound in arr[(signed long int)j]: SUCCESS
[main.array_bounds.2] line 14 array 'arr' upper bound in arr[(signed long int)j]: FAILURE
[main.assertion.1] line 15 assertion arr[j] == 5: SUCCESS

It is very confusing from a user's perspective that when there is must-undefined-behavior (for the version with the assumption), the assertion on line 15 fails, and when there is may-undefined-behavior (for the version without the assumption), the assertion succeeds. Shouldn't CBMC be consistent in handling these two programs?

[kroening]

It is very confusing from a user's perspective that when there is must-undefined-behavior (for the version with the assumption), the assertion on line 15 fails, and when there is may-undefined-behavior (for the version without the assumption), the assertion succeeds. Shouldn't CBMC be consistent in handling these two programs?

Once there is undefined behavior, there can't be a promise of consistency anymore (because then you are defining behaviour). We'll make the assertion report s.th. like "inconclusive" going forward.

[tautschnig]

When removing the assumption we now (with #8314 in place) print:

[main.array_bounds.1] line 14 array 'arr' lower bound in arr[(signed long int)j]: SUCCESS
[main.array_bounds.2] line 14 array 'arr' upper bound in arr[(signed long int)j]: FAILURE
[main.assertion.1] line 15 assertion arr[j] == 5: UNKNOWN

Resolving.