This project is read-only.

Conditional claims

Feb 1, 2011 at 8:58 AM

Hello,

 

#include "vcc.h"

vcc(claimable) struct A_str {
    unsigned int a;
} A_g;

struct B_str {
    unsigned int a;
    spec(claim_t c;)

    invariant(keeps(c));
    invariant(a == A_g.a);
    invariant(true ==> (claims(c, closed(&A_g)))); //I1
    //invariant(claims(c, closed(&A_g))); //I2
};

isadmissibilitycheck
void dStrAdm(struct B_str *p) {
    assert(valid_claim(p->c));
    havoc_others(p);
}

void interfere() {};

void test_B (struct B_str *b)
maintains(wrapped(b))
writes(b)
{
    unwrap(b);
    interfere();
    wrap(b);
}

 

gives

$ vcc conditionalSimp.c 
Verification of B_str#adm succeeded.
Verification of dStrAdm succeeded.
Verification of interfere succeeded.
Verification of test_B failed.
p:\tool\vcc\sandbox\elementary\claim\conditionalSimp.c(31,15) : error VC8014: invariant(a == A_g.a) of B_str fails on wrap.
p:\tool\vcc\sandbox\elementary\claim\conditionalSimp.c(12,17) : error VC9599: (related information) location of the invariant.
Exiting with 3 (1 error(s).)

Interestingly, once one commets out the line marked with "I1" and comments in the line marked with "I2" verification succeeds smoothly. I1 and I2 only differ by antecedent "true" (which semantically should be equivalent) ...

Is there anything in the use of claimes we are conceptually missing here? - Thanks for any suggestion.

Holger and Thorsten.

Feb 10, 2011 at 3:33 PM

To give some more context (why do they want that "true"?) here: In the code the previous example had been derived from the precondition was a check for initialization a bit like line 144 in RwLock.c from http://www.verisoftxt.de/d/src/RwLock-SSV09-2.tar.gz .

The code with intialization would be:

#include "vcc.h"

vcc(claimable) struct A_str {
    unsigned int a;
} A_g;

struct vcc(dynamic_owns) B_str {
    unsigned int a;
    spec(claim_t c;)
    spec(unsigned int initialized;)
    //invariant(initialized ==> keeps(&A_g)); //KEEPS
    invariant(initialized ==> set_in(c, owns(this)));
    invariant(initialized ==> a == A_g.a);
    invariant(initialized ==> (claims(c, closed(&A_g))));
};

void interfere() {};

void test_B (struct B_str *b)
requires(b->initialized)
maintains(wrapped(b))
writes(b)
{
    unwrap(b);
    interfere();
    wrap(b);
}

Giving:

~/sandbox/elementary/claim$ vcc conditionalSimp-keeps.c 
Verification of B_str#adm failed.
p:\tool\vcc\sandbox\elementary\claim\conditionalSimp-keeps.c(13,17) : error VC8012: invariant(initialized ==> a == A_g.a) of B_str is not admissible.
Verification of interfere succeeded.
Verification of test_B failed.
p:\tool\vcc\sandbox\elementary\claim\conditionalSimp-keeps.c(26,15) : error VC8014: invariant(initialized ==> a == A_g.a) of B_str fails on wrap.
p:\tool\vcc\sandbox\elementary\claim\conditionalSimp-keeps.c(13,17) : error VC9599: (related information) location of the invariant.
Exiting with 3 (2 error(s).)
Similar to the example posted on 1 Feb, the error message in line 13 can be cured by adding a custom admissibility check after the declaration of B_str (maybe this is unsound?): 

isadmissibilitycheck
void dStrAdm(struct B_str *p) {
    assert(p->initialized ==> valid_claim(p->c));
    havoc_others(p);
}

Incommenting the line outcommented with the comment "KEEPS" would solve both error messages at line 13 and 26 at the same time. However, the intended semantics is that many struct B_str's can assert closedness of the global object A_g.a at the same time, so incommenting keeps seems to strong (there is only one owner at the time). Thanks, Holger

 

Feb 11, 2011 at 9:14 AM

Hi Holger,

  in your example, the admissibility of B_str relies on the fact that the non-volatile field A_g.a cannot change by virtue of the claim c. To make VCC use that fact, you have to use the "by_claim()" annotation (which is sometimes inserted by VCC implicitly, cf. http://vcc.codeplex.com/wikipage?title=Inference&referringTitle=Documentation). The fixed example, using "by_claim()" in B_str and test_B, looks like this:

#include "vcc.h"

vcc(claimable) struct A_str {
    unsigned int a;
} A_g;

struct vcc(dynamic_owns) B_str {
    unsigned int a;
    spec(claim_t c;)
    spec(unsigned int initialized;)
    invariant(initialized ==> set_in(c, owns(this)));
    invariant(initialized ==> a == by_claim(c,A_g.a));
    invariant(initialized ==> (claims(c, closed(&A_g))));
};

void interfere() {};

void test_B (struct B_str *b)
requires(b->initialized)
maintains(wrapped(b))
writes(b)
{
    unwrap(b);
    assert(valid_claim(b->c));
    interfere();
    assert(old(A_g.a)==by_claim(b->c,A_g.a));
    wrap(b);
}

/*`
Verification of B_str#adm succeeded.
Verification of interfere succeeded.
Verification of test_B succeeded.
`*/

Best, Mark

Feb 24, 2011 at 10:59 AM

Hi Mark,

to quickly "close" this one: works perfectly also in larger examples - thanks :-) Holger