[Question] Syntax Error with `__CPROVER_loop_invariant` in CBMC 6.4.1 Docker

[zhoulaifu]

Dear CBMC Developers,

Thank you for your outstanding work on CBMC, which has been invaluable for my verification efforts. I am writing to ask a question on a parsing error I encountered when using __CPROVER_loop_invariant in a simple C program with CBMC 6.4.1 running inside a cbmc Docker container. I would greatly appreciate your guidance:

Code (loop_invariant2.c)

int sum_array(int arr[], int n) {
    int result = 0;

    for (int i = 0; i < n; i++) {
        __CPROVER_loop_invariant(i >= 0 && i <= n); // Invariant: i is within array bounds
        result += arr[i]; 
    }

    return result;
}

CBMC Commands and Output

I executed the following command inside the Docker container:

cbmc loop_invariant2.c --function sum_array

Output:

CBMC version 6.4.1 (n/a) 64-bit x86_64 linux
file loop_invariant2.c line 7 function sum_array: syntax error before '__CPROVER_loop_invariant'
PARSING ERROR

I guess we need to use some special CBMC options so that __CPROVER_loop_invariant can be recognized by CBMC? Thank you for your guidance.

[remi-delmas-3000]

int sum_array(int arr[], int n) {
    int result = 0;

    for (int i = 0; i < n; i++) 
        __CPROVER_loop_invariant(i >= 0 && i <= n) // Invariant: i is within array bounds
   {
        result += arr[i]; 
    }

    return result;
}

The loop invariant clause must be placed after the for () statement, not in the body, without semicolon.

[remi-delmas-3000]

To activate contracts you need to apply a pass of goto-instrument

If you just want to use the loop contract in the context of a normal proof harness you can write something like that

#include <stdlib.h>
int sum_array(int arr[], int n) {
  int result = 0;

  for (int i = 0; i < n; i++)
    __CPROVER_assigns(i, result)
    __CPROVER_loop_invariant(0 <= i && i <= n)
    {
      result += arr[i];
    }

  return result;
}
int main() {
  int arr[1000];
  sum_array(arr, 1000);
  return 0;
}

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

but without more assumptions about the contents of the array the running sum will overflow.

[sum_array.overflow.3] line 14 arithmetic overflow on signed + in result + arr[(signed long int)i]: FAILURE

You can also use function contracts to express preconditions about the contents of the array (bounds for each value that are strong enough to avoid overflow)

#include <stdlib.h>
int sum_array(int arr[], int n)
__CPROVER_requires(n < 0 && n < 10000)
__CPROVER_requires(__CPROVER_is_fresh(arr, n * sizeof(int)))
__CPROVER_requires(__CPROVER_forall{int i; 0 <= i && i < n ==> arr[i] <= 10})
{
  int result = 0;

  for (int i = 0; i < n; i++)
    __CPROVER_assigns(i, result)
    __CPROVER_loop_invariant(0 <= i && i <= n)
    __CPROVER_loop_invariant(result <= i * 10)
    {
      result += arr[i];
    }

  return result;
}
int main() {
  int *arr;
  int n;
  sum_array(arr, n);
  return 0;
}

goto-cc main.c -o a.out
goto-instrument --dfcc main --enforce-contract sum_array --apply-loop-contracts a.out b.out
cbmc b.out --z3
...
** 0 of 68 failed (1 iterations)
VERIFICATION SUCCESSFUL

Since the contract uses quantifiers you need to use the --z3 or bitwuzla backend.

But to safely implement a sum function like this one, you should detect overflow in the loop and bail, returning the number of summed elements before the overflow occurred.

#include <stdlib.h>
#include <limits.h>

int sum_array(int arr[], int n)
__CPROVER_requires(n >= 0 && n < __CPROVER_max_malloc_size / sizeof(int))
__CPROVER_requires(__CPROVER_is_fresh(arr, n * sizeof(int)))
{
  int result = 0;
  int i;

  for (i = 0; i < n; i++)
    __CPROVER_assigns(i, result)
    __CPROVER_loop_invariant(0 <= i && i <= n)
    {
      // Check for potential overflow before adding
      if ((result > 0 && arr[i] > INT_MAX - result) ||
          (result < 0 && arr[i] < INT_MIN - result)) {
        // Overflow would occur, exit the loop
        return i;  // Return the number of elements summed before potential overflow
      }
      result += arr[i];
    }

  return n;  // All elements were summed without overflow
}

int main() {
  int *arr;
  int n;
  sum_array(arr, n);
  return 0;
}

Then you don't need z3 anymore since quantifiers are gone.

goto-cc main.c -o a.out
goto-instrument --dfcc main --enforce-contract sum_array --apply-loop-contracts a.out b.out
cbmc b.out

...

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

[zhoulaifu]

Thank you very much, Remi, for these great pointers.

You mentioned, "To activate contracts, you need to apply a pass of goto-instrument." Do you have any general documentation on this?

Specifically, I’m looking for documentation that explains:

goto-instrument --dfcc main --enforce-contract sum_array --apply-loop-contracts a.out b.out

Thanks again!

[remi-delmas-3000]

Not the greatest doc of all times but it has some useful bits:

• https://diffblue.github.io/cbmc//contracts-mainpage.html
  • https://diffblue.github.io/cbmc//contracts-dev.html explains how the goto-instrument transformation works.
  • https://diffblue.github.io/cbmc//contracts-user.html gives examples of how to use it

But the gist of it is that function contracts lets you specify pre/post conditions an footprint of a function (set of memory locations that may be assigned by the function). The preconditions of function contracts let you describe the memory layout of function arguments and automatically allocate objects from them https://diffblue.github.io/cbmc//contracts-memory-predicates.html.

ret_t foo(param_t params)
__CPROVER_requires(R)
__CPROVER_assigns(A)
__CPROVER_ensures(E)
{ 
  body(); 
}

Using --enforce-contract foo you can check foo against its contract, and goto instrument generates a wrapper around foo

assume(R);
ret_t __return_value = foo(args);
assume(E);

Using --replace-call-with-contract foo you can abstract a call to foo(args) with its contract,
which then becomes

assert(R[params<-args]);
havoc(A[params<-args]);
ret_t __return_value = nondet();
assume(E[params<-args, __CPROVER_return_value <-__return_value]);

Refs

• https://diffblue.github.io/cbmc//contracts-dev-spec-contract-checking.html
• https://diffblue.github.io/cbmc//contracts-dev-spec-contract-checking-rec.html
• https://diffblue.github.io/cbmc//contracts-dev-spec-contract-replacement.html

When using loop contracts:

while(cond)
__CPROVER_assigns(A)
__CPROVER_loop_invariant(I)
__CPROVER_decreases(D)
{
  body();
}

Using loop invariant and variants goto-instrument rewrites the loop into base case + inductive step case :

assert(I); // loop invariant base case
havoc(A); // jump to arbitrary step
assume(I); // assume loop invariant
old_D = D; // loop variant before step

// loop step from arbitrary state that satisfies I
if(cond)
{
  body(); 
  assert(I);  // invariant consecution
  assert(old_D < D); // loop variant check (for termination)
  assume(false); // stop progress
}

// continue execution from arbitrary state that satisfies I
...

In reality it is a little more involved than that because loops can be nested in other loops, we also instrument the all the loop body code to check that side effects are contained within the set of locations A declared by the function or the loop contract, loops can break early and lead to states that do not necessarily satisfy the loop invariant and downstream statements can execute from these states as well. And we support multi-dimensional loop variants with lexicographic ordering. But overall this is what goto-instrument is doing.

Using contracts you can decompose the analysis into smaller chunks, analyse the safety of loops over arbitrary numbers of iterations, and prove much larger programs than with unwinding alone.