CBMC wavefront does not terminate on simple decreases clause in loop

[rod-chapman]

CBMC version: 6.0.0-preview (cbmc-6.0.0-alpha-400-gc320360eef)
Operating system: macOS 13.6.6 (Apple Silcon)

See new code in https://github.com/rod-chapman/cbmc-examples/blob/52d6ddeb15a23ed75802b15f69611dc735b6fe78/arrays/ar.c#L179

I added a "decreases" clause to the loop. CBMC 5.95.1 terminates OK after about 10 seconds.
CBMC 6.0.0-preview fails to terminate, with repeated messages, such as:

Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.920661s
Runtime decision procedure: 0.920808s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.926316s
Runtime decision procedure: 0.926462s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.955392s
Runtime decision procedure: 0.955532s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.918986s
Runtime decision procedure: 0.919128s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.925166s
Runtime decision procedure: 0.92531s

and so on.

Please fix. This is blocking progress on verification of s2n-tls.

[rod-chapman]

Command line is:

make TARGET=constant_time_equals_strict

[qinheping]

I tried a simpler version without loops.

#include <stdbool.h>
#include <stddef.h>
#include <stdint.h>

#define C 8

bool constant_time_equals_strict(
  const uint8_t *const a,
  const uint8_t *const b,
  const uint32_t len)
{
  bool arrays_differ = false;
  size_t i;
  arrays_differ = arrays_differ || (a[i] != b[i]);
  uint8_t c = a[i] - b[i];

  __CPROVER_assert(
    arrays_differ !=
      __CPROVER_forall {
        size_t j;
        (j >= 0 && j < len) ==> (a[j] == b[j])
      },
    "Post-loop assertion");
  return !arrays_differ;
}

void main()
{
  uint32_t len;
  uint8_t *a = malloc(sizeof(uint8_t) * len);
  uint8_t *b = malloc(sizeof(uint8_t) * len);
  bool result;
  __CPROVER_assume(a != NULL);
  __CPROVER_assume(b != NULL);
  __CPROVER_assume(len >= 1);
  result = constant_time_equals_strict(a, b, len);
}

I run the program with CBMC develop and with the following commands

goto-cc main.c
goto-instrument --dfcc main --apply-loop-contracts a.out b.out
cbmc b.out -- smt2

CBMC didn't terminate. My z3 version is 4.12.5. I also tried to run CBMC with cvc4 and cvc5 but got

** 4 of 1380 failed (2 iterations)
VERIFICATION ERROR

without detailed error message.

I think the problem could be caused by the smt encoding for quantified expression. More investigation are needed to find the cause of error.

[rod-chapman]

Many thanks for the update. Please keep digging! This is blocking my work on unbounded verification of s2n-tls.

[rod-chapman]

See the latest code here: https://github.com/rod-chapman/cbmc-examples/tree/main/arrays

make TARGET=constant_time_equals_strict

now works as expected with the latest CBMC 6.0.0-alpha (built today), following your fix to make "==" work inside quantifiers.

BUT... I have added a new function constant_time_equals_total() (that calls constant_time_equals_strict).

Verification of that with
make TARGET=constant_time_equals_total

does not terminate. Is this the same problem as that reported above? Or perhaps a new issue?

[qinheping]

I observed the same issue that removing or adding a simple statement, such as uint8_t c = a[i] - b[i]; in my above example will result in CBMC not terminating from terminating. So I suppose they are the same problem.

[tautschnig]

A couple of observations:

1. Using CVC5 instead of Z3 (via --cvc5 instead of --smt2) makes it terminate pretty quickly, but then CVC5 actually says "unknown" for a number of properties. I don't know how to debug this, perhaps @martin-cs can contribute some insight?
2. With the branch from Quantifier instantiation via simplistic E-matching #8224 (and then dropping --smt2) this solves in under 10 seconds with MiniSat as back-end and under 18 seconds with CaDiCaL as back-end.

[rod-chapman]

This problem still affects the function constant_time_equals_total() in my examples. Can I get an update or a workaround please?

[rod-chapman]

This might be the same problem as #8365