This project is read-only.

Preserving is_object_root

May 21, 2010 at 2:26 PM

Dear all,

in the below snippet there is the invariant that all elements in a manager are is_object_root (motivation for this is the customized memory manager, as is_object_root is a precondition for using memory via from_bytes).

Question: how do we preserve "is_object_root" in this situation?

#include "vcc.h"

struct node_str;

spec (
typedef struct vcc(dynamic_owns) manager_str {
    int dummy;
    bool set_f[struct node_str*]; 
	invariant(forall(struct node_str *i; set_f[i] ==> set_in(i, owns(this))))
} manager_t;
);

typedef struct node_str {
	int dummy;
	spec( manager_t ^m; )
} node_t;

typedef struct A_str {
    int dummy;
    spec (manager_t ^e;)
	spec (manager_t ^f;)

    invariant(keeps(e))
    invariant(keeps(f)) 
    invariant(forall(node_t *i; f->set_f[i] ==> is_object_root(i)))

    invariant(e != f)  
} A_t;

void interfere(spec(manager_t ^m))
	writes(m)
	maintains(wrapped(m));

void testIt(A_t *a)
	requires(wrapped(a))
	writes(a)
{
	spec(state_t s0;)
	unwrap(a);
	assert(in_domain(a->f, a->f));
	assert(in_domain(a->e, a->e));
	assert(a->e != a->f);
	
 	assert(forall(node_t *i; a->f->set_f[i] ==> is_object_root(i)));
 	assert(forall(node_t *i; a->f->set_f[i] ==> in_domain(i, a->f)));
 	assert(forall(node_t *i; a->f->set_f[i] ==> !set_in(i, owns(a->e))));
 	assert(forall(node_t *i; a->e->set_f[i] ==> in_domain(i, a->e)));

	speconly(s0 = current_state();)
	interfere(spec(a->e));

	assert(forall(node_t *i; a->f->set_f[i] <==> in_state(s0,  a->f->set_f[i])));
	//this fails
	assert(forall(node_t *i; a->f->set_f[i] ==> is_object_root(i)));

	wrap(a);
}

This is currently giving:

Verification of manager_str#adm (smoke:0) (2) [3,45s] succeeded.
Verification of A_str#adm (smoke:0) (1) [2,71s] succeeded.
Verification of testIt [2,39s] failed.
p:\tool\vcc\sandbox\elementary\ptrset\ptrset-map-usage-simple-object_root.c(54,11) : error VC9500: Assertion '__forall(node_t *i; a->f->set_f[i] ==> _vcc_is_object_root(i))' did not verify.
Time: 10,53s total, 1,93s compiler, 0,00s Boogie, 8,59s method verification.
Detected verification errors in 1 methods.
Exiting with 3 (1 error(s).)

Many thanks, Holger (and Thorsten)

May 21, 2010 at 3:16 PM

The problem is that VCC can't derive

   assert(forall(obj_t o; set_in(o,owns(a->f)); unchanged(emb(o))));

after the call, which would allow it to still know that a->f's objects are still objects root.

Unfortunately, the regular domain mechanism does not keep the embeddings from changing since the "embedding" of an object is not an object field (at the Boogie level, the domain axiom only apply to $mem not to the typestate $ts). Fixing this would be nice also in other scenarios (list entries and containing records). Would be nice, if Michal can comment on this...

I see two ways to fix this now: (i) move the object root invariant to the manager_t struct. (ii) add a ghost map obj_t embed[struct node_str*] to the manager struct that stores the embeddings of the owned objects (invariant(forall(struct node_str *i; set_f[i] ==> set_in(i, owns(this)) && embed[i]==emb(i))). By asserting f's invariant, the embedding information can then be "recovered".

HTH, Mark

 

 

May 21, 2010 at 8:01 PM
 

Hi Mark, thanks for the suggestions for the work-around. To give feedback: both worked out of the box. (i) would e.g. in a linked list setting too severely limit the nodes one can have (not good for code reuse) so for the record here is (ii, this is just literally following Mark's instruction but may be it's useful for some third party following the forum). It's very reassuring to have this clarified before the week-end :-). One thing I have not tested yet that it scales up in a more complicated setting, and I also join Mark in being curious for Michal's feedback concerning whether including the embeddings as object fields makes sense/is doable/would be desirable.

#include "vcc.h"

struct node_str;

spec (
typedef struct vcc(dynamic_owns) manager_str {
    int dummy;
    bool set_f[struct node_str*]; 
    obj_t embed[struct node_str*];
	invariant(forall(struct node_str *i; set_f[i] ==> set_in(i, owns(this)) 
        && embed[i] == emb(i)))
} manager_t;
);

typedef struct node_str {
	int dummy;
} node_t;

typedef struct A_str {
    int dummy;
    spec (manager_t ^e;)
	spec (manager_t ^f;)

    invariant(keeps(e))
    invariant(keeps(f)) 
    //invariant(forall(node_t *i; f->set_f[i] ==> is_object_root(i)))

    invariant(e != f)  
} A_t;

void interfere(spec(manager_t ^m))
	writes(m)
	maintains(wrapped(m));

void testIt(A_t *a)
	requires(wrapped(a))
	writes(a)
    requires(forall(node_t *i; a->f->set_f[i] ==> is_object_root(i)))
{
	spec(state_t s0;)
	
	unwrap(a);
	assert(in_domain(a->f, a->f));
	assert(in_domain(a->e, a->e));
	assert(a->e != a->f);
	
	assert(forall(node_t *i; a->f->set_f[i] ==> is_object_root(i)));
	assert(forall(node_t *i; a->f->set_f[i] ==> in_domain(i, a->f)));
	assert(forall(node_t *i; a->e->set_f[i] ==> in_domain(i, a->e)));

	speconly(s0 = current_state();)
	interfere(spec(a->e));

	assert(a->e != a->f);
	assert(forall(node_t *i; a->f->set_f[i] <==> in_state(s0,  a->f->set_f[i])));
	assert(in_domain(a->f, a->f)); //f's object invariant
	assert(forall(node_t *i; a->f->set_f[i] ==> is_object_root(i)));

	wrap(a);
}
 
May 25, 2010 at 4:28 PM

Dear all,

below is my attempt to use this in a list-based memory manager where the invariant on all elements in the list l (sentinel: LIST_ENTRY *l) is that they they are object roots.

#include "List.c"

spec (
typedef vcc(dynamic_owns) struct spec_str {

    bool set_f[LIST_ENTRY *];
    obj_t embed[LIST_ENTRY *];

} spec_t;
)

typedef vcc(dynamic_owns) struct big_str {

    LIST_ENTRY *l;
    spec(spec_t ^s;)
    invariant(keeps(s))
    invariant(keeps(l->Manager))
    invariant(set_in(l, owns(l->Manager)))
    invariant(l->Manager->ListHead == l)
    invariant(forall(LIST_ENTRY *e; s->set_f[e] ==> set_in(e, owns(l->Manager)) && emb(e) == s->embed[e]))
    invariant(!set_in(s, owns(l->Manager)));
    invariant(!set_in(this, owns(l->Manager)));

} big_t;

void test_insert(big_t *big, LIST_ENTRY *e) 
maintains(wrapped(big))
requires(wrapped(e))
writes(big)
requires(big->l->Manager->size == 10) //arbitrary small size for testing
requires(forall(LIST_ENTRY *i; big->s->set_f[i] ==> is_object_root(i)))
requires(is_object_root(e))
writes(e)
{
    unwrap(big);
    assert(forall(LIST_ENTRY *l; big->s->set_f[l] ==> is_object_root(l)));
    spec(state_t s0 = current_state(););
    assert(forall(LIST_ENTRY *l; in_state(s0, big->s->set_f[l]) == big->s->set_f[l]));
    assert(forall(LIST_ENTRY *l; big->s->set_f[l] ==> big->s->embed[l] == emb(l)));
    assert(in_domain(big->s, big->s));

    // update implementation object
    InsertHeadList(big->l, e);
    assert(forall(LIST_ENTRY *l; in_state(s0, big->s->set_f[l]) == big->s->set_f[l]));
    assert(forall(LIST_ENTRY *l; big->s->set_f[l] ==> big->s->embed[l] == emb(l))); // <-- point of failure

    // update specification object
    unwrap(big->s);
    speconly ( 
        big->s->set_f[e] = 1;
        set_owner(e, big->s);
        big->s->embed[e] = emb(e);
    )
    assert(big->s->embed[e] == emb(e)); 
    wrap(big->s);

    wrap(big);
}

This is giving

~/sandbox/list$ vc list-microsoft-client-map.c /functions:test_insert
Verification of test_insert [1,91s] failed.
p:\tool\vcc\sandbox\list\list-microsoft-client-map.c(45,14) : error VC9500: Assertion '__forall(LIST_ENTRY *l; big->s->set_f[l] ==> big->s->embed[l] == _vcc_emb(l))' did not verify.

For simplicity, the list implementation is basically List.c SVN examples  (with slightly stronger annotations on  InsertHeadList).

/*
 * This file provides a sample implementation of doubly-linked lists.
 */
#include "vcc.h"

/*
 * Required forward definitions/declarations.
 */
#define MAXUINT 0x7FFFFFFF

#ifdef VERIFY
/*
 * Forward declaration of ghost type _LIST_MANAGER.
 */
typedef struct _LIST_MANAGER LIST_MANAGER, *PLIST_MANAGER;
#endif

/*
 * Define the doubly-linked list type.
 */
typedef struct _LIST_ENTRY
{
    struct _LIST_ENTRY *Flink;
    struct _LIST_ENTRY *Blink;

    // Each list entry contains a back link to its corresponding list manager.
    spec(LIST_MANAGER ^Manager;)
} LIST_ENTRY, *PLIST_ENTRY;

#ifdef VERIFY
/*
 * This ghost type _LIST_MANAGER is used to manage the list entries in an abstract way.
 * The list manager is the owner of all list entries and contains a pointer to that
 * designated LIST_ENTRY, that is considered as the list head.
 * The list structure is modeled by a map of pointers to LIST_ENTRY structs to integer
 * values in the range of 0 to size-1, which represent the position of the pointer in 
 * the list. 
 */
spec (
struct vcc(dynamic_owns) _LIST_MANAGER
{ 
    // Number of entries in the list
    unsigned int size;
    // Pointer to the designated list head
    spec(PLIST_ENTRY ListHead;)
    // A map for the housekeeping of the order of referenced pointers in the list.
    spec(unsigned int index[PLIST_ENTRY];)

    // All objects are of the type LIST_ENTRY
    invariant(forall(obj_t p; {set_in(p,owns(this))}
        set_in(p,owns(this)) ==> is(p,LIST_ENTRY) && typed_phys(p)))

    // The "Manager" back-pointer of each LIST_ENTRY points back to this list manager.
    invariant(forall(PLIST_ENTRY p; {set_in(p,owns(this))}
        set_in(p,owns(this)) ==> p->Manager == this))

    // The ListHead is owned by the list manager.
    invariant(set_in(ListHead,owns(this)))

    // Each list entry, that can be reached via a Flink is also in the ownership
    // domain of the list manager. Additionally each Blink of an entry p->Flink points
    // back to p.
    invariant(forall(PLIST_ENTRY p; {set_in(p->Flink, owns(this))} {sk_hack(set_in(p->Flink, owns(this)))}
        set_in(p,owns(this)) ==> set_in(p->Flink,owns(this)) && p->Flink->Blink == p))

    // Each list entry, that can be reached via a Blink is also in the ownership
    // domain of the list manager. Additionally each Flink of an entry p->Blink points
    // back to p.
    invariant(forall(PLIST_ENTRY p; {set_in(p->Blink, owns(this))} {sk_hack(set_in(p->Blink, owns(this)))}
        set_in(p,owns(this)) ==> set_in(p->Blink,owns(this)) && p->Blink->Flink == p))

    // The index[] map always increases by 1 for each object that can be reached by 
    // an Flink pointer. Except if the Flink points to the list head, which implies
    // the end of the list.
    // 
    // The {sk_hack(set_in(p->Flink,owns(this)))} trigger introduces a witness of
    // an set_in(p->Flink,owns(this)) entry, that is required for the prove to succeed.
    invariant(forall(PLIST_ENTRY p; {set_in(p, owns(this))} {sk_hack(set_in(p->Flink,owns(this)))}
        set_in(p,owns(this)) && p->Flink != ListHead ==> index[p] + 1 == index[p->Flink]))

    // Specify index[] for well known objects.
    invariant(index[ListHead] == 0)
    invariant(index[ListHead->Blink] == size - 1)

    // Specify range of the index[] map.
    invariant(forall(PLIST_ENTRY e; {set_in(e,owns(this))}
        set_in(e,owns(this)) ==> 0 <= index[e] && index[e] < size))

    // Each element in the list is only contained once.
    invariant(forall(PLIST_ENTRY e1, e2; {set_in(e1,owns(this)), set_in(e2,owns(this))}
        set_in(e1,owns(this)) && set_in(e2,owns(this)) && e1 != e2 ==> index[e1] != index[e2]))

};)

typedef struct _LIST_MANAGER LIST_MANAGER, PLIST_MANAGER;

#endif


/**
 * InsertHeadList
 * ==============
 * 
 * The InsertHeadList routine inserts an entry at the head of a doubly-linked list of 
 * LIST_ENTRY structures.
 * 
 * Parameters:
 *   ListHead  : Pointer to the LIST_ENTRY structure that represents the head 
 *               of the list. 
 *   Entry     : Pointer to a LIST_ENTRY structure that represents the entry to 
 *               be inserted into the list.
 * 
 * Return Value:
 *   None
 */
void InsertHeadList( PLIST_ENTRY ListHead, PLIST_ENTRY Entry )
    maintains(wrapped(ListHead->Manager))
    maintains(set_in(ListHead,owns(ListHead->Manager)))
    requires(wrapped(Entry))
    ensures(set_in(Entry,owns(ListHead->Manager)))
    requires(ListHead->Manager->size < MAXUINT)
    ensures(ListHead->Manager->size == old(ListHead->Manager->size) + 1)
    ensures(set_eq(owns(ListHead->Manager),set_union(old(owns(ListHead->Manager)),SET(Entry))))
    ensures(Entry->Manager == ListHead->Manager)
    ensures(unchanged(ListHead->Manager->ListHead))
    ensures(unchanged(ListHead->Manager))
    writes(Entry,ListHead->Manager)
{
    spec(LIST_MANAGER ^ListManager = ListHead->Manager;)

    assert(in_domain(ListHead,ListManager));
    assert(in_domain(ListHead->Flink,ListManager));

    unwrap(Entry);
    Entry->Blink = ListHead;
    Entry->Flink = ListHead->Flink;
    speconly(Entry->Manager = ListManager;)
    wrap(Entry);
    expose(ListManager) {
        expose(ListHead->Flink) {
            ListHead->Flink->Blink = Entry;
        }
        expose(ListHead) {
            ListHead->Flink = Entry;
        }

speconly(
        ListManager->size = ListManager->size + 1;
        set_owner(Entry,ListManager);
        ListManager->index = lambda(PLIST_ENTRY x; set_in(x,owns(ListManager)); 
            x==Entry
                ? ListManager->index[ListHead] + 1
                : (ListManager->index[x] <= ListManager->index[ListHead]
                    ? ListManager->index[x]
                    : ListManager->index[x] + 1));
        )
    }
}


Does anyone see an obvious error (perhaps in the specification approach)?
May 25, 2010 at 9:57 PM

The spec of InsertHeadList (and similarly for other List.c functions) should be extended by the postcondition "ensures(forall(PLIST_ENTRY x; set_in(x,owns(ListHead->Manager)); unchanged(emb(x))))" (I already did this for some list functions and contracts elsewhere, but I'll extend List.c accordingly as well). This might get rid on the necessity of the "embed" field. The emb() is really sort of awkward, I don't think there is currently an alternative to the suggested contract...

 

Best, Mark

 

May 26, 2010 at 11:57 AM

Hi Mark, thanks insertions works nicely (see test_insert below, verifies), is there also a way to use this trick for removal (see test_remove, not yet verifying yet, below) ?

Moreover something I should ask (for understanding) is whether the precondition is_object_root is really strictly needed to reinterpret memory (why?) or whether it is merely an "educational" suggestion for good programming style like we had with the reinterpretation of global variables (that was http://vcc.codeplex.com/Thread/View.aspx?ThreadId=211647).

#include "List.c"

typedef vcc(dynamic_owns) struct big_str {

    LIST_ENTRY *l;
    invariant(keeps(l->Manager))
    invariant(set_in(l, owns(l->Manager)))
    invariant(l->Manager->ListHead == l)
    invariant(forall(LIST_ENTRY *e; set_in(e, owns(l->Manager)); is_object_root(e)))

} big_t;

void test_insert(big_t *big, LIST_ENTRY *e) 
maintains(wrapped(big))
requires(wrapped(e))
writes(big)
requires(big->l->Manager->size == 10) //arbitrary small size for testing
requires(is_object_root(e))
writes(e)
{
    unwrap(big);
    InsertHeadList(big->l, e);

    wrap(big);
}

void test_remove(big_t *big)
maintains(wrapped(big))
requires(big->l->Manager->size == 10)
requires(big->l->Flink != big->l->Manager->ListHead)
writes(big)
{
    LIST_ENTRY *e;

    unwrap(big);
    assert(in_domain(big->l->Manager, big->l->Manager));
    e = RemoveHeadList(big->l);
    assert(in_domain(big->l->Manager, big->l->Manager));
    assert(is_object_root(e)); //<- fails
    wrap(big);
}

This gives on test_remove

Verification of test_remove [2,17s] failed.
p:\tool\vcc\sandbox\list\list-microsoft-client-is_object_root.c(39,14) : error VC9500: Assertion '_vcc_is_object_root(e)' did not verify.
Time: 4,66s total, 2,40s compiler, 0,00s Boogie, 2,25s method verification.
Detected verification errors in 1 methods.
Exiting with 3 (1 error(s).)

The adapted part of List.c is:

/**
 * RemoveHeadList
 * ==============
 * 
 * The RemoveHeadList routine removes an entry from the beginning of a doubly linked 
 * list of LIST_ENTRY structures. This function must only be called, if the list
 * is not empty.
 * 
 * Parameters:
 *   ListHead : Pointer to the LIST_ENTRY structure that serves as the list header. 
 * 
 * Return Value:
 *   RemoveHeadList returns a pointer to the entry removed from the list.
 */
PLIST_ENTRY RemoveHeadList( PLIST_ENTRY ListHead )
    maintains(set_in(ListHead,owns(ListHead->Manager)))
    maintains(wrapped(ListHead->Manager))
    requires(ListHead->Flink != ListHead->Manager->ListHead)
    ensures(ListHead->Manager->size == old(ListHead->Manager->size) - 1)
    ensures(set_equal(owns(ListHead->Manager),set_difference(old(owns(ListHead->Manager)),SET(result))))
    ensures(wrapped(result))
    writes(ListHead->Manager)
    ensures(unchanged(ListHead->Manager))
    maintains(ListHead->Manager->ListHead == ListHead)
    ensures(forall(PLIST_ENTRY x; set_in(x, old(owns(ListHead->Manager))); unchanged(emb(x))))
    ensures(unchanged(emb(result)))
{
    PLIST_ENTRY Flink, Entry;
    spec(LIST_MANAGER ^ListManager = ListHead->Manager;)

    assert(in_domain(ListHead,ListManager));
    assert(in_domain(ListHead->Flink,ListManager));
    assert(in_domain(ListHead->Flink->Flink,ListManager));

    Entry = ListHead->Flink;
    Flink = ListHead->Flink->Flink;
    expose(ListManager) {
        expose(ListHead) {
            ListHead->Flink = Flink;
        }
        expose(Flink) {
            Flink->Blink = ListHead;
        }

speconly(
        ListManager->size = ListManager->size - 1;
        giveup_owner(Entry,ListManager);
        ListManager->index = lambda(PLIST_ENTRY x; set_in(x,owns(ListManager)); 
            ListManager->index[x] < ListManager->index[Entry]
                ? ListManager->index[x]
                : ListManager->index[x] - 1);
        )
    }
    return Entry;
}


 Thanks, Holger

May 26, 2010 at 6:02 PM

Found one way to fix the test_remove in my last post ... Add an "requires(forall(LIST_ENTRY *i; is_object_root(i)))" to the preconditions of test_remove and it runs just fine :-)

May 26, 2010 at 7:14 PM

Moreover something I should ask (for understanding) is whether the precondition is_object_root is really strictly needed to reinterpret memory (why?) or whether it is merely an "educational" suggestion for good programming style like we had with the reinterpretation of global variables (that was http://vcc.codeplex.com/Thread/View.aspx?ThreadId=211647).

For a definitions:

struct A {

struct B { int x; } b;

int c;

}

we generate an axiom saying forall(A *a; typed(a) ==> typed(&a->b)). If you were allowed to reinterpret b at will, it would be unsound.

Hope this helps!

Michal

May 26, 2010 at 8:47 PM

Maybe as an RFC to Holger: since the above would represent the standard use case for the list implementation (with LIST_ENTRY being type B and A being the type for a containing record), I'm sort of wondering what the use case of list entries actually being object roots is. I can see the use case for the containing record type being an object root... (Note that the unchanged(emb()) extensions would still be needed for the generic list library).

 

Best, Mark

May 27, 2010 at 10:46 AM
Edited May 27, 2010 at 10:47 AM
Hi Mark,

it is helpful that you ask for the use case ...

We all know that MMU helps to separate tasks by maintaining 
page tables that map task virtual addresses and a task ID 
to physical addresses. 

Basically, these MILS separation kernels (for an accessible intro see 
http://www.stsc.hill.af.mil/crosstalk/2005/08/0508Vanfleet_etal.html ) 
add another layer: you want to be able to group several tasks 
to a partition and control communication between partitions. 
For this it helps to have some control structures that (virtually) 
group certain pages to a partition. A page then can be dynamically used for 
other data structures (and a performant way to do this in some 
cases is simply to cast it). The use case during run-time 
is thus with an address m as a trace over a time slice: 

void *m;
(some_struct)m; <-- cast to some struct
// do some work with some_struct
(void*)m; <-- release m
(other_struct)m; <-- cast to other struct
// do some work with other_struct
(void*)m; <-- release m

You might want to ask, why one does not use shadow page 
tables in hardware-assisted virtualization for this (why have 
this in software at all?), but the answer is simply that many
embedded systems run on simpler architectures.

To address this too, of course boot-time set-up is a different 
thing and more resembles the memory manager you had once posted on 27 April 
in the thread "Memory reinterpretation for non-root objects", but as I hoped 
to make clear it is also not my current point of focus. 

Now indeed my quick shot yesterday night at 07:02 was premature: 
"requires(forall(LIST_ENTRY *i; is_object_root(i)))" is too strong 
a precondition (indeed not all list entries in all lists are object roots!) 
as I only want 
"requires(forall(LIST_ENTRY *i; set_in(i, b->l->Manager); is_object_root(i)))",
but with this weaker precondition this again I can't get to verify. The tricky 
things seems to be that after popping (removing) an entry from the 
list qua function call RemoveListHead VCC automatically forgets 
anything about the environment, whereas I would really need that 
info about the list element after is has been popped. Have you solved this in 
your List.c annotations? 
Thanks, Holger
May 27, 2010 at 11:46 AM

But, again, do your list entries not appear as a field of other structures? Like in struct A { LIST_ENTRY x; };? Basically, in the latter setup, &a.x cannot be an object root, as Michal pointer out. If you do not use LIST_ENTRY embedded in another object,, how do you associated payload with list entries? Do you put payload and list entries side by side (just to clarify my understanding of the use case)?

Thanks, Mark

May 27, 2010 at 12:32 PM

Just to get this very clear, if they appear as pointer in other structures like in struct A { LIST_ENTRY* x;} that is no conceptual problem if is_object_root(x) holds, right (meaning this pointer is not pointing to anything in an arbitrary object)? And, yes there are (1) situations where list entries occur within other structures like in struct A { LIST_ENTRY x}, there are (2) situations where list entries pointers occur within other structures as pointers struct A {LIST_ENTRY *x;}. In case (2) for some of the lists it holds that all list entry pointers are object roots (2a), and for other that not all list entries are object roots (2b). I'm interested in developing a (modular) specification for (2a) here. 

Hope that clarifies, Holger

May 27, 2010 at 6:02 PM
Edited May 27, 2010 at 6:03 PM

Hi Holger,

 right, "struct A { LIST_ENTRY* x;} a" is consistent with "is_object_root(a.x)".

  Regarding your test_remove() problem: it seems that the RemoveHeadList() is underspecified with respect to the result; basically adding "returns(old(ListHead->Flink))" solved the problem for me.

Best, Mark

 

May 28, 2010 at 11:08 AM

Hi Mark,

yes that fixes the list thing. Still another small one on casting (no particular relation to lists, but rounds well into the thread's topic).

#include "vcc.h"

typedef struct a_str {
    int dummy;
} a_t;

void test(a_t *A) 
requires(is_object_root(A))
{

    void *B;
    assert(is_object_root(A));
    B = (void *)A;
    assert(A == B);
    assert(is_object_root(A));
    assert(is_object_root(B)); //here we fail

}

Gives.

Verification of test [2,44s] failed.
p:\tool\vcc\sandbox\elementary\emb\emb-cast.c(16,14) : error VC9500: Assertion '_vcc_is_object_root(B)' did not verify.
Time: 4,73s total, 2,23s compiler, 0,00s Boogie, 2,49s method verification.
Detected verification errors in 1 methods.
Exiting with 3 (1 error(s).)

(Just want to understand why: is_object_root seems to be a syntactical and not semantical property here. This does not seem to be a show stopper, as an alternative is to preserve the info in specification structures rather than the void pointer.)

Thanks, Holger

May 28, 2010 at 1:09 PM
Hi Holger,

pointers are modeled as pairs of types and addresses in VCC. The way
your second assertion works is that VCC will compare only the address
part, which it why it will succeed.
Now, is_object_root is a predicate on the whole pair, however, which is
why your assertion fails. (Generally "is_object_root(a) &&
is_object_root(b)" for "a==b" and differently typed "a" and "b" would
violate VCC's typestate invariants).

Best, Mark
Jun 6, 2010 at 11:45 AM

Thx. For third parties: Follow-up is that with the current SVN version of Test/testsuite/examples/List.c e.g. the following works fine:

#include "List.c"

typedef vcc(dynamic_owns) struct big_str {

    LIST_ENTRY *l;
    invariant(keeps(l->Manager))
    invariant(set_in(l, owns(l->Manager)))
    invariant(l->Manager->ListHead == l)
    invariant(forall(LIST_ENTRY *e; set_in(e, owns(l->Manager)); is_object_root(e)))

} big_t;

void test_insert(big_t *big, LIST_ENTRY *e) 
maintains(wrapped(big))
requires(wrapped(e))
writes(big)
requires(big->l->Manager->size == 10) //arbitrary small size for testing
requires(is_object_root(e))
writes(e)
{
    unwrap(big);
    InsertHeadList(big->l, e);

    wrap(big);
}

void test_remove(big_t *big)
maintains(wrapped(big))
requires(big->l->Manager->size == 10)
requires(big->l->Flink != big->l->Manager->ListHead)
requires(forall(LIST_ENTRY *i; set_in(i, owns(big->l->Manager)); is_object_root(i)))
writes(big)
{
    LIST_ENTRY *e;

    unwrap(big);
    assert(in_domain(big->l->Manager, big->l->Manager));
    e = RemoveHeadList(big->l);
    unwrap(e);
    assert(in_domain(big->l->Manager, big->l->Manager));
    assert(is_object_root(e));
    wrap(big);
}


Cheers(there still might be other related questions but this one is definitely solved), Holger