Global variables: implicit separation assumptions

Dec 13, 2010 at 9:44 AM

Hello all,

in the following code snippet I can show some separation of a global variable and a field of a function-local structure that seems to be triggered by VCC's memory model:

#include "vcc.h"

typedef struct a_str {
    unsigned int a;
} a_t;

typedef struct b_str {
    int dummy;
    a_t a;
} b_t;

a_t a;

void test(unsigned char *u)
requires(u == (unsigned char *)2000)
requires(is_object_root(as_array(u, sizeof(b_t))))
requires(wrapped(as_array(u, sizeof(b_t))))
writes(as_array(u, sizeof(b_t)))
{
   b_t *b;
   assert(in_domain(as_array(u, sizeof(b_t)), as_array(u, sizeof(b_t))));
   unwrap(as_array(u, sizeof(b_t)));
   b = (b_t *)u;
   from_bytes(b, false);
   assert(&b->a != &a); //H1: why does vcc know that &a is not 2000
   assert(&b->a == (a_t *)2004); //H2: helper step for H3
  assert(&a != (a_t *)2004); //H3: why does vcc know that &a->t is not 2004? assert(&a != (a_t *)2000); //H4: if vcc knows that &a->t is not 2004(H3), // how could it &a be equal to the containing struct assert(&a != (a_t *)2001); //H5: more of the above ... }

Mostly out of curisioty (a work-around is to assign fixed values to function-local pointers) we (Thorsten and me) would like to understand why H1 to H3 hold, and H4 to H5 do not hold ("feature or bug"?).

Regards, Holger

Coordinator
Dec 13, 2010 at 9:37 PM

Hi Holger,

  feature :) This is indeed related to VCC's memory model, which gives you inequality of the pointers "&b->a" and "&a" via their different embeddings / their "object root"-property: the embedding of "&b->a" is "b", while "&a" (as a global) is an object root that is not embedded in another object. This explains H1-3. With regards to H4-5: pointer equality is in some sense partial for differently typed pointers (the way that VCC reasons about pointer aliasing is via types, field references, and embeddings, not field offsets), so VCC wouldn't do the derivation you did in your comments. Note that this is not related to global variables (if you have an a_t structure embedded in a c_t structure, the results should be the same).

  Can you elaborate what you are trying to "work around"?

  Best, Mark

Dec 14, 2010 at 6:59 PM
Edited Dec 14, 2010 at 7:02 PM

Well if you ask ... Currently, I'm toying around with some initialization code:

 

$ cat unwrap.c 
#include "vcc.h"

struct map_str {
unsigned int a;
spec ( unsigned int m[unsigned int]; )
};

void test (unsigned char *c, struct map_str *m claimp(cl))
requires(wrapped(cl) && valid_claim(cl) && claims(cl, closed(m)))
requires(m == (struct map_str *)100)
requires(c == (void *)1000)
// requires(cl == (void ^)200) <- incommenting this gives inconsistency
writes(as_array(c, 100))
requires(wrapped(as_array(c, 100)))
requires(forall(unsigned int i; m->m[i] == 0))

{

assert(forall(unsigned int i; m->m[i] == 0));

unwrap(as_array(c, 100));

assert(forall(unsigned int i; m->m[i] == 0));

}

 

output:

~/sandbox/elementary/claim$ vcc /ps:32 unwrap.c
Verification of test [1,52s] failed.
p:\tool\vcc\sandbox\elementary\claim\unwrap.c(23,14) : error VC9500: Assertion
+'__forall(unsigned int i; m->m[i] == 0)' did not verify.
Time: 3,67s total, 2,05s compiler, 0,00s Boogie, 1,61s method verification.
Detected verification errors in 1 methods.
Exiting with 3 (1 error(s).)

Greetings. Holger

Coordinator
Dec 14, 2010 at 7:10 PM

Hi Holger,

  about the commented requirement in your code: internally, VCC places ghost objects at adresses beyond the physical address range (>= 2^32 in your case, and >= 2^64 without specifying /ps:32). So, if you require a wrapped claim to be placed at address 200 you can directly derive false:

#include "vcc.h"

void test(claimp(cl)) 
    requires(wrapped(cl))
    requires(cl == (void ^)200)
{
    assert(0);
}

  (You couldn't construct a claim fulfillling such a requirement using "claim()")

  Hope that helps,

  Mark

Editor
Dec 14, 2010 at 7:54 PM

Hi Holger, Mark,

As for the question of why VCC fails on the second assertion, it seems to be trigger related... Try inserting assert(forall(unsigned int i; unchanged(m->m[i]))); between the unwrap() and your second assertion: it works for me.

Cheers,
Francois

Dec 15, 2010 at 6:39 PM

@Francois, yes that inded fixes it here too. Thanks... @Mark: o.k. that makes it much clearer. Maybe put the phrase "In its implementation, VCC simply places ghost objects at adresses beyond the physical address range" somewhere as a footnote into the user documentation if it is not in there because it is really short "constructive" explanation for an otherwise ("non-constructive"/"opaque") behavior (section 6 "Ghosts" in the tutorial).