Pure Functions

To use a function in specifications (requires, ensures, assert etc.) you need to mark it with ispure.

Pure Function Body

Such functions are not required to have a body, however if they do, the body cannot update the heap, even allocation of heapified local variables (local variables for which you take an address) is forbidden. If this restriction is violated, VCC will produce one of the following errors:

error VC9703: Memory allocation in pure context is not allowed.
error VC9703: Writing memory location 'p' in pure context is not allowed.

Format of Pure Postconditions

There are however restrictions on the form of the contract of a pure function. Such restrictions are in place to ensure that the pure functions are well-defined. For example, the following functions that are not well defined (that is no implementation for them could exist):

ispure int f()
  ensures(result == result + 1);
ispure int g()
  ensures(result == h());
ispure int h()
  ensures(result == g() + 1);


A valid pure postcondition has one of the following forms:
  1. result.f1.f2...fN == EXPR where EXPR doesn't contain result and N >= 0 (that is result == EXPR is also allowed)
  2. (a let expression) exists(T v; v == EXPR; POST) where EXPR doesn't contain result and doesn't contains v, and POST is a valid pure postcondition

A pure function can have any number of valid pure postconditions, either as separate ensures(...) clauses or conjoined with &&.

However, two different postconditions of the form result.f1...fN == EXPR1 and result.f1...fM == EXPR2 where N <= M are not allowed. This is to prevent specification of a substructure as a whole and then some of its components, e.g., result.x == { .y = 10, .z = 20 } && result.x.y = 30 .

Take a directed graph, where nodes are pure functions. If a contract of function f calls function g then there is an edge going from f to g. This graph is not allowed to have cycles.

For example, the following are valid pure function definitions:

struct IN {
  int d0;
  int d1;
  int d2;
};

struct A {
  int x;
  int y;
};

ispure
struct A ok1(struct IN *x)
  requires(thread_local(x))
  ensures(result.x == x->d0 && result.y == x->d0)
  reads(x);

struct B {
  struct A a;
  int z;
};

ispure
struct A ok2(struct IN *x)
  requires(thread_local(x))
  ensures(result == { .x = x->d0, .y = 7 })
  reads(x);


Given a pure function:

ispure T f(P)
  requires(R)
  ensures(E);

The following definition axiom is generated:

axiom(forall(P; E [result := f(P)]))

That is the requires(...) clause is ignored in the axiom. Still, if you call f in non-contract context (i.e., assign its result to a local ghost variable), the pre-condition will be checked.

For example:

ispure int f(int x)
  ensures(result == x + 7);

will generate:

axiom(forall(int x; {f(x)} f(x) == x + 7))


If you want to have a post-condition in a pure function of a different form, you need to use an explicit axiom, for example:

ispure int f(int x);
axiom(forall(int x; {f(x)} f(x) > 0))

Then it is however up to you to make sure such a function, characterized by the axiom, actually exists.

Frame Axioms

Contracts of pure functions can refer to the heap, at the time of call. In such case a reads(...) clause needs to be specified on a pure function. The reads clause lists the pointers in the heap that the function is allowed to read (note that pointer sets cannot currently be specified, see array_range not handled properly). Thus, the BoogiePL function will take an additional state parameter (i.e., int f(int x) will be translated to int f(state_t s, int x)). For example:

ispure bool isPositive(int *x)
  reads(x)
  ensures(result == (*x > 0));

However, if you list precisely what location a pure function reads, then you would expect it to depend not on the entire heap, but only on those locations. This is where a frame axiom comes into play. If you add frameaxiom specifier to the function above, VCC will implicitly generate the following:

bool isPositive_frame(int vx, int *x);
axiom(forall(state_t s; int vx; int *x;
  isPositive(s, x) == isPositive_frame(s[x], x)));

Thus, if VCC has two states s1 and s2, and knows they are the same at x, then it will also know isPositive(s1, x) == isPositive(s2, x).

Now, you might wonder why to bother with passing pointers, if we end up dereferencing them at call site anyway, with this additional axiom. The reason is that you might also list a root of ownership domain, and be allowed to read the entire ownership domain.

TODO need an example here

A good question is why we don't always generate a frame axiom. The answer is that it is costly for the prover to instantiate those, so we only want them when they are really needed.

Reads Check

Because VCC is generating frame axioms from reads(...) clauses, it also needs to make sure the information provided there is correct. This is done with a reads check. For a pure function f(P) you essentially need to prove f(s1,P) == f(s2,P), given that s1[x] == s2[x] for all things listed in reads clause of f and given the definition axiom of f (i.e., you do not get to prove anything from the body, only from the spec!).

Note that the reads(...) clause has only any positive effects on verification, when you also have frameaxiom. Otherwise it's only informational, but still generates a reads check. If you don't need the frameaxiom, and have a pure function that reads the state you can say reads(set_universe()), which will prevent generation of a reads check.

Arithmetic in Pure Function Contracts

VCC sticks in an implicit unchecked around EXPR in valid pure postconditions. Otherwise we generally get into trouble in the following situation:

ispure
unsigned foo(unsigned x)
  ensures(result == x - 10);
...
unsigned tmp = foo(0);


Because the pure function has no body, there is no place to put the check that x - 10 does not overflow. Still, even if we required a body, the fix would be to add precondition x >= 10 to foo(...). Such precondition would again go unchecked when the function would be called in contract context.

Non-determinism

Consider:

ispure int foo()
{
  int uninitialized;
  return uninitialized;
}
...
int x1 = foo();
int x2 = foo();
assert(x1 == x2);


Before we would generate a free postcondition on Boogie procedure foo(), binding the result returned to result of function #foo(), representing the pure function. Now this postcondition is not free, preventing this kinds of problem.

Last edited Nov 13, 2009 at 1:06 PM by stobies, version 8

Comments

No comments yet.