This project is read-only.

Over conservative writes() clause on spec arguments

Feb 9, 2010 at 4:30 PM
Edited Feb 9, 2010 at 4:45 PM

Hi all,

In the following code, VCC seems to be "a bit" over conservative during calls to foo(), and simply writes wherever in memory. Do you have any idea what causes this?

#include <vcc.h>

typedef struct dbytes_s
{
	char *ptr;
	unsigned int len;

	invariant(keeps(as_array(ptr,len)))
	invariant(is_array(ptr,len))
} dbytes_c;

typedef struct predicates
{
	int dummy;
} preds;

dbytes_c *foo(spec(preds ^P))
maintains(inv(P))
maintains(mutable(P))
writes(P)
ensures(is_fresh(result))
ensures(is_fresh(as_array(result->ptr,result->len)))
ensures(wrapped(result));

void test(spec(preds ^P))
requires(inv(P))
requires(mutable(P))
writes(P)
{
	spec(state_t pre;)
	dbytes_c *f1, *f2;

	f1 = foo(spec(P));

	speconly(pre = current_state();)
	f2 = foo(spec(P));

	assert(shallow_eq(*f1, in_state(pre, *f1)));
}

In my opinion, the fact that the writes() clause is over a spec argument should allow VCC to prove that no physical memory (other than the result) gets written. This leaves us with the cases where the result overwrites some previously allocated location on the heap, but this should be prevented by the freshness annotation.

Cheers,
Francois

Feb 9, 2010 at 11:23 PM

Hi Francois, the example can be fixed by ensuring "wrapped_dom(result)" in foo() (which is short for "wrapped(result) && in_domain(result,result)") or asserting "in_domain(result,result)" in between the calls.

The reason is that VCC overapproximates writes clauses. Usually non-written mutable data and all data in a non-written domain should be preserved across calls (where a domain is all data transitively owned by a wrapped object). Domains are however not automatically determined, but only as guided by in_domain assertions. in_domain(x,x) can be established for a wrapped object (a.k.a. domain root). in_domain(y,x) can be established if in_domain(z,x) and set_in(y,owns(z)) is known. So, in the example, all fields of f1 are known to be unchanged by asserting in_domain(f1,f1).

Hope that helps, Mark

Feb 10, 2010 at 9:23 AM

Yes it did help, thanks a lot, Mark.

Is there a reason, other than performance, to not automatically infer in_domain(x,x) from wrapped(x)? However simple the shorthand, it would be more practical to not have to worry ourselves about giving obvious hints to VCC.

Cheers,
Francois

Feb 10, 2010 at 11:30 AM

Hi Francois, I don't know of another reason. (Note that in addition to its use for 'establishing domains', in_domain() also has a second use to assert / trigger the invariants of its first argument, which might also be performance-relevant). I agree that it would be nice if this wouldn't have to be stated explicitly. Note that there is some automatic inference for in_domain (see http://vcc.codeplex.com/wikipage?title=Inference), but not in this specific case.

Best, Mark