Now we’re back to something easy.

#include "vcc.h"
#include <limits.h>

int lsearch(int elt, int *ar, unsigned int sz)
  requires(0 <= sz)
  requires(sz < INT_MAX / sizeof(int))
  requires( wrapped( as_array( ar, sz ) ) )
  ensures(result >= 0 ==> ar[result] == elt)
  ensures(result < 0 ==> forall(int i; 0 <= i && i < (int)sz ==> ar[i] != elt))
{
    int i;
    for (i = 0; i < (int)sz; i++)
      invariant(0 <= i && i <= (int)sz)
      invariant(forall(int j; 0 <= j && j < i ==> ar[j] != elt))
    {
        if (ar[i] == elt) return i;
    }

    return -1;
}

This example shows how to state validity of an array. It is required to specify, that ar is accessed as an array with the size sz. This is achieved by specifying requires( wrapped( as_array( ar, sz ) ) ) , which states, that the integer pointer ar must be accessed as a wrapped array with sz elements. Since this example only reads the array values, the array remained wrapped. Otherwise an unwrap(as_array( ar, sz )) would be required to write to the array and its elements.

SMT solvers, including Z3 which is used in VCC, handle quantifier reasoning through instantiation. The basic ideas is that certain subterms of the quantified formula are designated as triggers. For example consider the following satisfiability query:

  forall (int x; {f(x)} f(x) > 0) && f(1) == -42

Now, the solver is sitting there, trying to disprove f(1) == -42, and has an axiom with f(x) as a trigger (footnote: The syntax for explicit triggers is {...}) floating around. So it will go and add the following clause, which is a first order tautology:

  forall (int x; f(x) > 0) ==> f(1) > 0

i.e. it will try to instantiate the axiom with x:=1. This leads to contradiction.

However this is only part of the picture, for example consider:

  forall (int x; {f(g(x))} f(g(x)) == 3) && c == g(7) && f(c) == 42

Here the trigger for the axiom is f(g(x)). The solver asserts c == g(7) and f(c) == 42. There is no explicit f(g(x)), but there is one modulo the current congruence relation. Therefore the solver will instantiate the axiom with x:=7.

One can have also several triggers, in which case it is enough for one of them to match. For example:

  forall (int x; {f(x)} {g(x)} f(x) == g(x) + 1)

Here we want the axiom to be instantiated whenever the prover is interested in g(7) or f(10).

It is also possible for each of those to be a multi-trigger, one good example here is transitivity:

 forall (int x, y, z; {f(x,y), f(y,z)} f(x,y) && f(y,z) ==> f(x,z))

The trigger will only match if both f(x,y) and f(y,z) match simultaneously, for example if one has f(1,2) and f(2,7) it will generate x:=1, y:=2 and z:=7, but not if one has only f(1,2) and f(3,4) it won't generate a match. On the other hand f(3,3) would also generate a match with x,y,z:=3.

The user can write the triggers explicitly or rely on the "wisdom" of the SMT solver for finding them. The algorithm currently employed in Z3 is to select any smallest subterm that has all the bound variables in it. Logical connectives, equality, disequality, arithmetic predicates and operators are not consider parts of terms. If there is at least one such subterm, all of them are selected as triggers.

If there is no such subterm, some multi-trigger is selected, which is most often not the one you want. In such cases it is always good idea to specify the multi-trigger explicitly instead.

Z3 does not match on theory symbols, and arithmetic operators are theory symbols. It will match on constants though.

One examples when it bites you is:

  forall (UINT64 x; 0 <= x && x <= 7 ==> a[x+1] == x)

The only trigger possible here is a[x+1] , but it involves arithmetic so it won't match anything. The example should be therefore rewritten as:

  forall (UINT64 x; 1 <= x && x <= 8 ==> a[x] == x - 1)

If there is really nothing to match on, or if the triggers are not sufficient, there is another trick coming to rescue: you can use match_int(x) as a part of the quantified formula. It is a predicate that is always true, but allows you to connect different quantifiers so one triggers when another is instantiated. It is especially useful when there are several interconnected loop invariants. There are also match_uint(x), match_ulong(x) , ... and match_ptr(x) .

#include "vcc.h"

typedef unsigned __int8 UINT8;
typedef unsigned __int64 UINT64;


int ispure Contains(UINT8 a[], UINT64 count, UINT8 elem)
  reads(set_universe())
  ensures(result == exists(UINT64 j; match_ulong(j) && 0 <= j && j < count && a[j] == elem));

int ispure SameElements(UINT8 a[], UINT8 b[], UINT64 count)
  reads(set_universe())
  ensures(result == forall(UINT64 i; match_ulong(i) && 0 <= i && i < count 
    ==> Contains(a, count, b[i]) && Contains(b, count, a[i])));


void foo()
{
  UINT64 i;
  UINT8 A[256];
  for (i = 0; i < 256; i++)
    invariant(0 <= i && i <= 256)
    invariant(forall(UINT64 j; match_ulong(j) && 0 <= j && j < i ==> A[j] == j))
    invariant(forall(UINT64 j; match_ulong(j) && 0 <= j && j < i ==> Contains(A, i, (UINT8)j)))
    invariant(SameElements(A, A, i))
  {
    A[i] = (UINT8)i;
  }
}

Last edited Nov 13, 2009 at 12:02 PM by stobies, version 7

Comments

No comments yet.