sk_hack in new syntax

Sep 28, 2010 at 11:19 PM

Hello, how can I generate the intermediate code

   __invariant(__forall(PLIST_ENTRY p; {_vcc_set_in0(p->Flink,_vcc_owns(__this))} {_vcc_sk_hack(_vcc_set_in0(p->Flink,_vcc_owns(__this)))}

from new syntax? Thanks ...

(Context is a (started) attempt to convert List.c to new syntax - of couse the "#if 0" are to be incommented later)


 * This file provides a sample implementation of doubly-linked lists.


#include "vcc.h"


 * Required forward definitions/declarations.



extern void* malloc(unsigned int size);


 * Forward declaration of ghost type _LIST_MANAGER.




 * 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.

    _(ghost PLIST_MANAGER Manager)


#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. 


typedef _(dynamic_owns) struct _LIST_MANAGER


    // Number of entries in the list

    unsigned int size;

    // Pointer to the designated list head

    _(ghost PLIST_ENTRY ListHead)

    // A map for the housekeeping of the order of referenced pointers in the list.

    _(ghost unsigned int index[PLIST_ENTRY])

    // All objects are of the type LIST_ENTRY

#if 0 

    _(invariant \forall \object p; {p \in0 \this->\owns}

        p \in0 \this->\owns ==> p \is LIST_ENTRY && p->\valid)


    // The "Manager" back-pointer of each LIST_ENTRY points back to this list manager.

#if 0

    _(invariant \forall PLIST_ENTRY p; {:hint p \in0 \this->\owns}

        p \in0 \this->\owns ==> p->Manager == \this)


    // The ListHead is owned by the list manager.

    _(invariant ListHead \in0 \this->\owns)

    // 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; {p->Flink \in0 \this->\owns} {:hint p->Flink \in0 \this->\owns}

		//{:sk_hack p->Flink \in0 \this->\owns} 

        p \in0 \this->\owns ==> (p->Flink \in0 \this->\owns && (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.

#if 0 

    _(invariant \forall PLIST_ENTRY p; {:hint p->Blink \in0 \this->\owns}

        p \in0 \this->\owns ==> (p->Blink \in0 \this->\owns && (p->Blink->Flink == p)))


#if 0

    // 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_in0(p->Flink,owns(this)))} trigger introduces a witness of

    // an set_in0(p->Flink,owns(this)) entry, that is required for the prove to succeed.

    _(invariant \forall PLIST_ENTRY p; {:hint p->Flink \in0 \this->\owns}

        (p \in0 \this->\owns && (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; {e \in0 \this->\owns}

        e \in0 \this->\owns ==> ((0 <= index[e]) && (index[e] < size)))

    // Each element in the list is only contained once.

    _(invariant \forall PLIST_ENTRY e1, e2; {e1 \in0 \this->\owns, e2 \in0 \this->\owns}

        (e1 \in0 \this->\owns && e2 \in0 \this->\owns && (e1 != e2)) ==> (index[e1] != index[e2]))



// Since set_in() triggers all over the prelude use set_in0, which triggers less

// axioms. But this requires, that we trigger the transfer from set_in0 to set_in

// at selected points throughout the annotations. This macro provides this trigger.

#define trigger_set_in0(S) \

  forall(obj_t p; {set_in0(p, S), set_in(p, old(S))} set_in(p, old(S)) <==> set_in0(p, old(S)))



 * 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 ListHead \in0 (ListHead->Manager)->\owns)

    _(requires \mutable(Entry))

    _(requires Entry->\owns == {})

    _(ensures Entry \in (ListHead->Manager)->\owns)

    _(requires ListHead->Manager->size < MAXUINT)

    _(ensures ListHead->Manager->size == \old(ListHead->Manager->size) + 1)

    _(ensures (ListHead->Manager)->\owns == \old((ListHead->Manager)->\owns) \union {Entry})

    _(ensures Entry->Manager == ListHead->Manager)

    _(writes ListHead->Manager,\extent(Entry))


    _(ghost PLIST_MANAGER ListManager = ListHead->Manager)

    _(assert ListHead \in \domain(ListManager))

    _(assert ListHead->Flink \in \domain(ListManager))

    Entry->Blink = ListHead;

    Entry->Flink = ListHead->Flink;

    _(ghost Entry->Manager = ListManager;)

    _(wrap Entry)

    _(unwrap ListManager);

    _(wrap ListManager);

#if 0

    _(unwrapping ListHead->Flink) {

        ListHead->Flink->Blink = Entry;


     _(unwrapping ListHead) {

         ListHead->Flink = Entry;



        ListManager->size = ListManager->size + 1;

        ListManager->\owns += Entry;

        ListManager->index = \lambda PLIST_ENTRY x;  

			x \in ListManager->\owns;

		//### /* range restriction ignored */ 

			((x==Entry) ?

				ListManager->index[ListHead] +1 : 

               ((ListManager->index[x] <= 


                  ? ListManager->index[x]:

			      ListManager->index[x] +1; )))

        _(assert Entry->Manager == ListManager)

        //_(assert trigger_set_in0(ListManager->\owns))

        _(assert ListManager->ListHead->Blink \in0 ListManager->\owns)



Or has that already been done by someone else?

Oct 4, 2010 at 2:34 PM

Hi Holger,

  sk_hack's are called "hints" in the new syntax, cf. Appendix A.3 in the tutorial ( To my knowledge, the old list example in SVN hasn't yet been translated to the new syntax, although there is a (different, singly-linked) list example in the tutorial (Section 6).

  Hope this helps, Mark

Oct 5, 2010 at 2:47 PM
Edited Oct 5, 2010 at 3:03 PM

Hi Mark,

I'm not that sure whether that is enough. As you can see above in the example posted in the top of the thread I did try to convert those to *:hint". However, I can't get that to verify (the version in the old syntax happily verifies). I think the particular thing about the old List.h (you'll find in the SVN at Test/testsuite/examples/List.h) were idioms like "{keeps(p->Flink)} {sk_hack(keeps(p->Flink)}" which are two different kind of hints with the same starting point. I do not know how to reproduce these two different kind of hints (with the same starting point) in the new syntax. Maybe those two different kinds of hints are not necessary any longer, but then, nonetheless, I do not know how to verify the code snippet posted above (if copy-pasting is a nuisance, simply regenerate it yourself by syntax-converting Test/testsuite/examples/List.h. For the time being cut off all the methods, I think once structure admissibility of "struct _LIST_MANAGER" is accepted then the task is perhaps solved - porting it to the methods is just more of the same which could be left to me.)

(Addendum: I've also checked the singly-linked-list example at Docs/Tutorial/c/07_list.c but apparently that works without using ":hint" at all.)

Cheers, Holger

Oct 5, 2010 at 3:26 PM

Sorry, I didn't look at your example code too closely.

It seems that there might be a parsing problem with multiple triggers in invariants, which I now reported:

Best, Mark

Oct 5, 2010 at 3:46 PM

Also, with the trigger inference option (-it), it should automatically add the {:hint ...} annotations when the triggers is of the form keeps() or set_in().


Oct 5, 2010 at 6:56 PM

thanks michal, with /it basically seems to work ... have to check the details though (just a quick feedback as i'm offline tomorrow morning)

Oct 5, 2010 at 9:18 PM

on a second look, one thing that now fails with the otherwise useful /it switch is code that uses constructs like

_(invariant \forall unsigned char *c ; ([10])c \in Manger->owns ==> object_root(c))

with "invariant ... forbids unwrapping"   

any idea?

Oct 6, 2010 at 1:39 PM

quick update: the "invariant ... forbids unwrapping" 
seems to be related when groups are used

_(invariant :somegroup \forall unsigned char *c ; ([10])c \in Manger->owns ==> object_root(c)

(i'm still investigating but suggestions welcome)