Implement inductive check for assigns clauses in loop contracts

[feliperodri]

CBMC version: 5.67.0
Operating system: N/A

Description

Currently the loop contract instrumentation havocs the given targets in the loop_assigns clause and instruments the body of the loop according to the assigns clause. This really means that we assume that the set of all locations where the function can write at any given iteration is correctly captured by the clause.

while(c)
__CPROVER_loop_invariant(inv)
__CPROVER_loop_decrases(dec)
__CPROVER_loop_assigns(t1, ..., tn)
{
 body;
}

PRE_LOOP:
havoc(t1, ..., tn);
assume(inv);
dec_begin = dec;
t1_CAR = CAR(t1);
...
tn_CAR = CAR(tn);
// instrument condition and body assignments with W = {t1_CAR, ... , tn_CAR}
if(c)
{
  body; 
  POST_LOOP:
  // check loop invariant and variants
  dec_end = dec;
  assert(dec_end < dec_begin);
  assert(inv);
}

Interpreting the assigns clause at different program locations can yield different Conditional Address Ranges (CARs), especially when slices that depend on loop counters are involved.

We miss a check demonstrating that that the loop assigns clause is an inductive invariant, i.e. a check demonstrating that CARs as evaluated at PRE_LOOP include the CARs as evaluated at POST_LOOP.

PRE_LOOP:
havoc(t1, ..., tn);
assume(inv);
dec_begin = dec;
t1_begin = CAR(t1);
...
tn_begin = CAR(tn);
if(c)
{
  body;

  // instrumentation
  dec_end = dec;
  assert(dec_end < dec_begin);
  assert(inv);

POST_LOOP:
  t1_end = CAR(t1);
  ...
  tn_and = CAR(tn);
  assert(t1_begin \in {t1_end, ..., tn_end})
  ...
  assert(tn_begin \in {t1_end, ..., tn_end})
}

Without this check, it is not established that the assigns clause correctly summarizes all reachable states of the loop.

Consider the example below:

int i = 0;
while(i < len)
loop_invariant(forall {j:int, 0 <= j < i ==> a[j]==0 })
loop_decreases(len-i)
loop_assigns(i, a[i])
{
  a[i] = 0;
  i++;
}

This program and its assigns clause are accepted because we only instrument the loop to check that it assigns i and a[i] and that's what it does.

However this program should be rejected because i, a[i] does not correctly capture the set of reachable states of the loop, which at an iteration i has touched a[0] to a[i-1] and then touches a[i]. To be safe to assume as induction hypothesis (through havoc + assume) we

We are only safe because the tool contains a hack, which detects that target a[i] depends on a non-const symbol i and changes havoc(&a[i]) to havoc_object(&a[i]).

The proper loop assigns clause should be loop_assigns(i, __CPROVER_object_slice(&a[0], i)).

Proposed solution:

implement an inclusion check that the CARs evaluated pre loop step are included in the CARs evaluated post loop step.

Remark:

it is perhaps easier to understand the assigns clause as an inductive invariant if we go back to the original intent (frame condition) and express it as a big conjunction over each byte of memory b allocated up to the program location of interest of formulas not_in(b, CAR(t1)) & ... & not_in(b, CAR(tn)) ==> b == \old(b)