Embedding, byte arrays and claims

Editor
Dec 10, 2010 at 7:36 PM

Hi all,

The following C code fails to verify (assertion failure):

#include <vcc.h>
#include <stdlib.h>

void toto(unsigned char* ptr, unsigned long len, foo* bar claimp(c))
maintains(is_thread_local_array(ptr,len))
maintains(forall(mathint i; 0 <= i && i < len ==> typed(ptr + i)))
always(c, closed(bar))
writes(c)
{
  spec(claim_t tmp;)

  speconly(tmp = claim(c, closed(bar));)
  assert(is_thread_local_array(ptr,len));
}

I had a long "trying to figure it out" session with the boogie code and managed to make Z3 admit that it thought the claim object could actually be the embedding of all the array elements. Is it actually possible for a claim to be the embedding of any kind of physical object? If not, could this be soundly made into an axiom (for example, axiom (forall #p:$ptr, S:$state :: $typ($emb(S,$ptr)) != ^^claim); seems to do the trick, although I don't know about its impact on performance).

Cheers,
Francois

Coordinator
Dec 13, 2010 at 8:57 PM

Hi Francois,

  this behavior is more general, namely that thread-locality of pointers (in your case the thread-locality of the character pointers "ptr+0", "ptr+1", ..., "ptr + (len -1)") is not preserved across functions calls writing the state / the heap (in your case the claim creation operation "claim()") unless you know a stronger property that might guarantee this (in your case, say, by substituting "is_thread_local_array()" with "is_mutable_array()", or by providing a mutable / wrapped embedding for the array elements). In the general case, fixing this is not so easy (it must be known that the thread-local pointers are not in the domain of any objects being written to in a given function call). In the special case of "claim()", it may be possible to provide a fix (I guess for the contract of claim() rather than as a general axiom), but performance is probably an issue - maybe others can comment.

Best, Mark

Editor
Dec 14, 2010 at 10:58 AM

Hi Mark,

Thanks for the answer. The problem is that, for this particular function, I may not be able to require a stronger property, as the implementation may well pass in a string literal (but doesn't have to), for which the only known properties are that all bytes are typed and thread_local. But I also think that my issue is a bit deeper than this.

When looking at the generated Boogie code (sorry if it is bad practice, or too early in the day for that), and focusing on the eventful part, I see the following [red and green assertions added by me]:

    claim#0s0 := $s;
    call claim#0 := $alloc_claim();
    assume $claims_obj(claim#0, $ptr(^^claim, SP#c));
    SL#tmp := $ref(claim#0);
    assume $local_value_is($s, #tok$1^14.25, #loc.tmp, $ptr_to_int($ptr(^^claim, SL#tmp)), $spec_ptr_to(^^claim)) && $local_value_is_ptr($s, #tok$1^14.25, #loc.tmp, $ptr(^^claim, SL#tmp), $spec_ptr_to(^^claim));
    assume $full_stop_ext(#tok$1^14.25, $s);
    assert (forall i:int :: 0 <= i && i < P#len ==> $emb(claim#0s0, $idx($ptr(^^u1, P#ptr), i, ^^u1)) == $emb($s, $idx($ptr(^^u1, P#ptr), i, ^^u1)));
    assert (forall i:int :: 0 <= i && i < P#len ==> $emb($s, $idx($ptr(^^u1, P#ptr), i, ^^u1)) != claim#0);
    assert $is_thread_local_array($s, $ptr(^^u1, P#ptr), ^^u1, P#len);

The first green assertion says that the embedding of all array elements is unchanged through the call to $alloc_claim() and succeeds without trouble. The red assertion fails despite the fact that, by contract of $alloc_claim()claim#0 is fresh and could not have possibly been the embedding of my array elements in state claim#0s0. My idea was that this should not have been an issue to begin with because claims do not have fields (and hence nothing can be embedded in them), but I don't even know if it is true in general, or only in the particular case of my simple example.

Cheers,
Francois


Editor
Feb 14, 2011 at 9:51 AM

Sorry for resurrecting this. I am slowly getting back to this issue, and I found the following line in VccPrelude.bpl:

 

axiom (forall ts:$type_state :: {$ts_emb(ts)} $kind_of($typ($ts_emb(ts))) != $kind_primitive && $is_non_primitive($typ($ts_emb(ts))) );

 

It seems to simply say that a primitive object cannot have embedded objects. However, the kind for claims is defined earlier as being composite, so this does not apply. I also noticed in a comment at the beginning of the file that claims used to have their own kind. Would it make sense to at least run performance tests with a modified version of the above axiom, for example the one below?

axiom (forall ts:$type_state :: {$ts_emb(ts)} $kind_of($typ($ts_emb(ts))) != $kind_primitive && $is_non_primitive($typ($ts_emb(ts))) && $typ($ts_emb(ts)) != ^^claim);

Alternatively, is there any way I can run your standard performance tests on my own, or do they involve unpublished code?

Cheers,
Francois 

Coordinator
Feb 14, 2011 at 6:50 PM

I think it’s fine to do this change. It probably won’t affect performance.

Michal

Editor
Feb 15, 2011 at 10:25 AM

Thanks, Michal.