This project is read-only.

Spec Functions with Reads Set / Reads Check Error

Aug 25, 2009 at 1:37 PM

Hi everyone,

i recently experimented with spec functions in order to define some sort of uninterpreted functions. To avoid inconsistencies i tied pure specification functions to some memory location which they are supposed to read from to generate their result.

see the example below:

#include "vcc.h"

spec(
     unsigned int ispure func(unsigned int ^ r)
        reads(r);
)

For this simple function i got the following error:

Verification of func#reads [1,38s] failed.
...
error VC8007: the value of 'result' changed (in reads check of 'func').

As far as I understood the generated boogie code the prover tries to assert that the result of the function is unchanged in case there are is a transition without writes to memory. Why is this actually necessary and is there some way to fix this problem? maybe some magic annotation keyword i'm missing?

Thanks for your help,

Christoph

Aug 25, 2009 at 2:30 PM

Hi Christoph, I think for all practical purposes you can currently get away with reads(set_universe()). Maybe Michal can comment.

Cheers, Mark

Aug 26, 2009 at 9:11 AM

Yes, then you also don't need to introduce this 'r' parameter (if it doesn't make sense, that is).

Michal

Aug 26, 2009 at 9:44 AM

yay, it works!

Thanks a lot! without the memory reference it's even more elegant now

Oct 15, 2009 at 1:15 PM

Hi all,

It appears that the behaviour of the reads() clauses has changed over the summer. In my verification effort, i would like to define a pure function

 

spec(ispure mathint encode(char *input, unsigned long length);)

 

that is injective in the underlying byte array (that is, the value of bytes input[0] to input[length-1]).

Just to make sure I am understood, what I would ideally like to do is write:

 

spec(ispure mathint encode(char *input, unsigned long length)
reads(array_range(input, length));)
axiom(forall(unsigned long l; char* b1, b2; encode(b1, l) == encode(b2, l) ==> forall(unsigned long i; i < l ==> b1[i] == b2[i]))

 

and have the assertion fail in the following code:

char *bytes = malloc(42);
spec(mathint bCode = encode(bytes, 42);)

bytes[3] = 't';
assert(bCode == encode(bytes, 42));

Right now, this causes VCC to fail with "error VC9619: non-pointer reads clauses are not supported". Is there anyway to do this cleanly? (I was so far using a macro that explicitly defined an encoding function, but performance with it was, understandably, awful).

Cheers,
Francois

Oct 15, 2009 at 2:04 PM

Hi Francois,

  currently VCC only supports regular pointers in the reads clauses, not pointer sets. See http://vcc.codeplex.com/WorkItem/View.aspx?WorkItemId=2937 for the associated issue, it looks like this restriction on reads() clauses can be relaxed in the future.  To my knowledge, VCC doesn't make much out of the reads() clause, unless "frameaxiom" is also defined, which would lead VCC to generate a frame axiom as shown. If you provide that manually (because of the restrictions), maybe you can just specify reads(set_universe()) for encode() (which will make VCC not do any reads check at all; also the error shouldn't arise). You can find some frameaxiom examples in the vcc/Test/testsuite/vcc2/pure file of the distribution. Also, Michal has recently updated http://vcc.codeplex.com/Wiki/View.aspx?title=Pure%20functions&version=4 somewhat.

  Hope that helps,

  Mark

 

Oct 15, 2009 at 3:01 PM

I did try with set_universe() before posting here, and VCC returns the same error message (for example, on the following code).

#include <vcc2.h>

spec(frameaxiom mathint encode(char *bytearray, unsigned long length)
reads(set_universe());)

axiom(forall(char* b1, b2; unsigned long l; encode(b1, l) == encode(b2, l) ==> forall(unsigned long i; i < l1 ==> b1[i] == b2[i])));

void main()
{
return;
}

I guess I can indeed try generating the frame axiom manually.

Thanks for the idea.
Francois.

Oct 15, 2009 at 3:20 PM

Ah, yes, you're right. For reads(set_universe()) it's not clever enough to generate "the right" frameaxiom; with ispure but without frameaxiom, it just suppresses the reads check (this is done in the compiler).