Advice for encapsulating structures?

[Elias Keis]

Hello,

is there a smart way to handle reading from and writing to encapsulating structures like linked lists? We have tried different aproaches like the following one to describe lists with VeriFast:

struct boxedint_list_node {
    struct boxedint_list_node* next;
    struct boxedint value;
};

struct boxedint_list {
    struct boxedint_list_node* head;
    int size;
};

/*@
predicate boxedint_list_abs(struct boxedint_list* l; list<boxedint> abs) =
    boxedint_list_abs_ptrs(l, ?vl) &*& boxedint_list_abs_foreach(vl, abs);

predicate boxedint_list_abs_ptrs(struct boxedint_list* l; list<struct boxedint*> vl) =
    l->head |-> ?head &*& l->size |-> ?size &*& boxedint_list_abs_ptrs_nodes(head, vl);

predicate boxedint_list_abs_ptrs_nodes(struct boxedint_list_node* node; list<struct boxedint*> vl) =
    node == NULL ? (vl == nil) : (boxedint_list_node_abs_meta(node, ?next, ?value) &*& boxedint_list_abs_ptrs_nodes(next, ?vl_tail) &*& vl == cons(value, vl_tail));

predicate boxedint_list_node_abs_meta(const struct boxedint_list_node* node; struct boxedint_list_node* next, struct boxedint* valueptr) =
    node->next |-> next &*& struct_boxedint_padding(&node->value) &*& valueptr == &node->value &*& malloc_block_boxedint_list_node(node);
   
predicate boxedint_list_abs_foreach(list<struct boxedint*> vl; list<boxedint> vlabs) =
    switch (vl) {
      case nil:
        return vlabs == nil;
      case cons(head, tail):
        return boxedint_abs(head, ?headabs) &*& boxedint_list_abs_foreach(tail, ?tailabs) &*& vlabs == cons(headabs, tailabs);
    };
@*/

struct boxedint stands for a complex structure that is stored in the list that we do not want to copy out of the list when read an element at a given index but just return a pointer on it instead.

The problem is that when we want to pass such a pointer to another function that needs the corresponding predicate, let us say a function void print_value(struct boxedint* bi) that needs a boxedint_abs(bi, ?val) as precondition, we have to break the boxedint_list_abs_foreach predicate in order to obtain the needed boxedint_abs predicate. This per se is fine, but when the list is needed as a whole again (e.g. to call a function contains(list, find_me)), we have to merge everything we split before, and if we want to use the pointer we already used before again, we have to break the list once again, also when we want to read more entries and so on. When we want to use the pointer to update values inside the list, things get even more ugly.

Our goal is to have C code generated automatically already correctly annotated for VeriFast. This mostly works great, but lists make life hard at the moment due to above reasons. Just declaring the lemmas for splitting/joining as lemma_auto does not work since even VeriFast seems to have problems to find out when they are ment to be applied. Generating the explicit application of the lemmas on the other hand would make it necessary to track for every pointer if it points into a list, so that that list can be opened before and closed after usage of the pointer.

Recommendations for a more generic approach would be really appreciated!

[Bart Jacobs]

Hi Elias,

The following works:

struct foo;

/*@

predicate foo(struct foo *foo;);

predicate foreach_foo(list<struct foo *> elems;);

lemma_auto void foreach_foo_remove(struct foo *foo);

    requires foreach_foo(?elems) &*& mem(foo, elems) == true;

    ensures foreach_foo(remove(foo, elems)) &*& foo(foo);

lemma_auto void foreach_foo_unremove(list<struct foo *> elems, struct foo *foo);

    requires foreach_foo(?elems0) &*& foo(foo) &*& mem(foo, elems) == true &*& elems0 == remove(foo, elems);

    ensures foreach_foo(elems);

@*/

void update_foo(struct foo *foo);

    //@ requires foo(foo);

    //@ ensures foo(foo);

void test(struct foo *foo)

    //@ requires foreach_foo(?elems) &*& mem(foo, elems) == true;

    //@ ensures foreach_foo(elems);

{

    update_foo(foo);

}

And so does this:

struct foo;

/*@

predicate foo(struct foo *foo;);

predicate foolist(; list<struct foo *> elems);

predicate foreach_foo(list<struct foo *> elems;);

lemma_auto void foreach_foo_remove(struct foo *foo);

    requires foreach_foo(?elems) &*& mem(foo, elems) == true;

    ensures foreach_foo(remove(foo, elems)) &*& foo(foo);

lemma_auto void foreach_foo_unremove(list<struct foo *> elems, struct foo *foo);

    requires foreach_foo(?elems0) &*& foo(foo) &*& elems0 == remove(foo, elems) &*& mem(foo, elems) == true;

    ensures foreach_foo(elems);

lemma_auto void foreach_foo_unremove_remove(struct foo *foo2);

    requires foolist(?elems) &*& foreach_foo(?elems0) &*& foo(?foo1) &*& mem(foo1, elems) == true &*& elems0 == remove(foo1, elems) &*& mem(foo2, elems) == true;

    ensures foolist(elems) &*& foreach_foo(remove(foo2, elems)) &*& foo(foo2);

@*/

void update_foo(struct foo *foo);

    //@ requires foo(foo);

    //@ ensures foo(foo);

void test(struct foo *foo1, struct foo *foo2)

    //@ requires foolist(?elems) &*& foreach_foo(elems) &*& mem(foo1, elems) == true &*& mem(foo2, elems) == true;

    //@ ensures foolist(elems) &*& foreach_foo(elems);

{

    update_foo(foo1);

    update_foo(foo2);

}

Best regards,

Bart

[Elias Keis]

Hi Bart,

thank you very much for your fast and very helpful answer! Indeed your code looks very clean, works great and in a very generic way.

However, when extending your code a bit, we came across similar problems as we did before. Ultimately, they all seem to break down into the lemmas we write not being suitable as auto lemmas.

For example, we tried this:

void update_foos(struct foo *foo1, struct foo *foo2);
    //@ requires foo(foo1) &*& foo(foo2);
    //@ ensures foo(foo1) &*& foo(foo2);

void test(struct foo *foo1, struct foo *foo2)
    //@
 requires foolist(?elems) &*& foreach_foo(elems) &*&
mem(foo1, elems) == true &*& mem(foo2, elems) == true

&*& foo1 != foo2;

    //@ ensures foolist(elems) &*& foreach_foo(elems);
{

    update_foos(foo1, foo2);
}

and found out that probably a lemma like the following is needed, so that the requirement mem(foo2, remove(foo1, elems)) of lemma foreach_foo_remove can be fullfilled for its second application:

lemma void list_remove_other<t>(list<t> list, t t1, t t2);
    requires mem(t1, list) == true &*& mem(t2, list) == true &*& t1 != t2;
    ensures mem(t1, remove(t2, list)) == true;

However, when declaring this lemma as lemma_auto, there is an error "no suitable predicates found in postcondition to generate rules".

We stumble across that message all the time, e.g. also when we tried to add a list with the abstract values of the elements as an output of the foreach_foo predicate (so that a contract not only could specify that the function uses a list, but also that it does not change its content):

struct foo;

/*@

inductive foo = nat;

predicate foo(struct foo *foo; foo fooabs);

predicate foolist(; list<struct foo *> elems);

predicate foreach_foo(list<struct foo *> elems; list<foo> abs);

lemma_auto void foreach_foo_remove(struct foo *foo);

    requires foreach_foo(?elems, ?abs) &*& mem(foo, elems) == true;
    ensures foo(foo, ?fooabs) &*& foreach_foo(remove(foo, elems), remove(fooabs, abs));

// "no suitable predicates found in postcondition to generate rules"
lemma_auto void foreach_foo_unremove(list<struct foo *> elems, struct foo *foo, list<foo> abs);
    requires foreach_foo(?elems0, ?abs0) &*& foo(foo, ?fooabs) &*& elems0 == remove(foo, elems) &*& mem(foo, elems) == true &*&
      abs0 == remove(fooabs, abs) &*& mem(fooabs, abs) == true;
    ensures foreach_foo(elems, abs);

// "no suitable predicates found in postcondition to generate rules"
lemma_auto void foreach_foo_unremove_remove(struct foo *foo2, list<foo> abs);
    requires foolist(?elems) &*& foreach_foo(?elems0, ?abs0) &*& foo(?foo1, ?foo1abs) &*& mem(foo1, elems) == true &*& elems0 == remove(foo1, elems) &*& mem(foo2, elems) == true &*&
      mem(foo1abs, abs) == true &*& abs0 == remove(foo1abs, abs);
    ensures foolist(elems) &*& foo(foo2, ?foo2abs) &*& foreach_foo(remove(foo2, elems), remove(foo2abs, abs));
@*/

Another error we occasionally get is "precondition of auto lemma <name> has wrong form". Is there any documentation about what auto lemmas should look like, or could you briefly outline what these errors are caused by?

Thanks again!

Elias

[Bart Jacobs]

Hi Elias,

This verifies:

struct foo;

/*@

predicate foo(struct foo *foo;);

predicate foolist(; list<struct foo *> elems);

predicate foreach_foo(list<struct foo *> elems;);

lemma_auto void foreach_foo_remove(struct foo *foo);

    requires foreach_foo(?elems) &*& mem(foo, elems) == true;

    ensures foreach_foo(remove(foo, elems)) &*& foo(foo);

lemma_auto void foreach_foo_unremove(list<struct foo *> elems, struct foo *foo);

    requires foreach_foo(?elems0) &*& foo(foo) &*& elems0 == remove(foo, elems) &*& mem(foo, elems) == true;

    ensures foreach_foo(elems);

lemma_auto void foreach_foo_unremove2(list<struct foo *> elems, struct foo *foo1, struct foo *foo2);

    requires foreach_foo(?elems0) &*& foo(foo1) &*& foo(foo2) &*& elems0 == remove(foo2, remove(foo1, elems)) &*& mem(foo1, elems) == true &*& mem(foo2, elems) == true &*& foo1 != foo2;

    ensures foreach_foo(elems);

lemma_auto void foreach_foo_unremove_remove(struct foo *foo2);

    requires foolist(?elems) &*& foreach_foo(?elems0) &*& foo(?foo1) &*& mem(foo1, elems) == true &*& elems0 == remove(foo1, elems) &*& mem(foo2, elems) == true;

    ensures foolist(elems) &*& foreach_foo(remove(foo2, elems)) &*& foo(foo2);

lemma_auto void list_remove_other<t>(list<t> list, t t1, t t2);

    requires mem(t1, list) == true && mem(t2, list) == true && t1 != t2;

    ensures mem(t1, remove(t2, list)) == true;

@*/

void update_foos(struct foo *foo1, struct foo *foo2);

    //@ requires foo(foo1) &*& foo(foo2);

    //@ ensures foo(foo1) &*& foo(foo2);

void test(struct foo *foo1, struct foo *foo2)

    //@ requires foolist(?elems) &*& foreach_foo(elems) &*& mem(foo1, elems) == true &*& mem(foo2, elems) == true &*& foo1 != foo2;

    //@ ensures foolist(elems) &*& foreach_foo(elems);

{

    update_foos(foo1, foo2);

}

and so does this:

//@ #include <listex.gh>

struct foo;

/*@

abstract_type foo;

fixpoint foo update_foo(foo value);

fixpoint list<t> insert<t>(int index, t x, list<t> xs);

fixpoint list<t> insert2<t>(int index1, t x1, int index2, t x2, list<t> xs);

predicate foo(struct foo *foo; foo value);

predicate foolist(; list<struct foo *> elems);

predicate foreach_foo(list<struct foo *> elems; list<foo> values);

lemma_auto void foreach_foo_remove(struct foo *foo);

    requires foreach_foo(?elems, ?vs) &*& mem(foo, elems) == true;

    ensures foreach_foo(remove(foo, elems), remove_nth(index_of(foo, elems), vs)) &*& foo(foo, nth(index_of(foo, elems), vs));

lemma_auto void foreach_foo_unremove(list<struct foo *> elems, struct foo *foo);

    requires foreach_foo(?elems0, ?vs0) &*& foo(foo, ?v) &*& elems0 == remove(foo, elems) &*& mem(foo, elems) == true;

    ensures foreach_foo(elems, insert(index_of(foo, elems), v, vs0));

lemma_auto void foreach_foo_unremove2(list<struct foo *> elems, struct foo *foo1, struct foo *foo2);

    requires foreach_foo(?elems0, ?vs0) &*& foo(foo1, ?v1) &*& foo(foo2, ?v2) &*& elems0 == remove(foo2, remove(foo1, elems)) &*& mem(foo1, elems) == true &*& mem(foo2, elems) == true &*& foo1 != foo2;

    ensures foreach_foo(elems, insert2(index_of(foo1, elems), v1, index_of(foo2, elems), v2, vs0));

lemma_auto void foreach_foo_unremove_remove(struct foo *foo2);

    requires foolist(?elems) &*& foreach_foo(?elems0, ?vs0) &*& foo(?foo1, ?v1) &*& mem(foo1, elems) == true &*& elems0 == remove(foo1, elems) &*& mem(foo2, elems) == true;

    ensures foolist(elems) &*& foreach_foo(remove(foo2, elems), remove_nth(index_of(foo2, elems), insert(index_of(foo1, elems), v1, vs0))) &*& foo(foo2, nth(index_of(foo2, elems), insert(index_of(foo1, elems), v1, vs0)));

lemma_auto void list_remove_other<t>(list<t> list, t t1, t t2);

    requires mem(t1, list) == true && mem(t2, list) == true && t1 != t2;

    ensures mem(t1, remove(t2, list)) == true;

@*/

void update_foos(struct foo *foo1, struct foo *foo2);

    //@ requires foo(foo1, ?v1) &*& foo(foo2, ?v2);

    //@ ensures foo(foo1, update_foo(v1)) &*& foo(foo2, update_foo(v2));

void test(struct foo *foo1, struct foo *foo2)

    //@ requires foolist(?elems) &*& foreach_foo(elems, ?vs) &*& mem(foo1, elems) == true &*& mem(foo2, elems) == true &*& foo1 != foo2;

    //@ ensures foolist(elems) &*& foreach_foo(elems, ?vs1);

{

    update_foos(foo1, foo2);

}

VeriFast supports two kinds of autolemmas: pure ones and spatial ones. Pure ones have to have just a single boolean expression as their precondition and as their postcondition. The problem with list_remove_other was simply that it used separating conjunctions instead of plain conjunctions.

Before we get into the causes of the error messages produced by the other lemmas, let me point out that they are sound only if different elements always have different abstract values. Otherwise, remove(fooabs, abs) might not do the right thing.

The problem with foreach_foo_unremove is that you (correctly) declared the second parameter of predicate foreach_foo as an output parameter. As a result, the automation logic will assume that the value for this parameter will not be available when the autolemma needs to be applied. As a result, the two final conjuncts of the precondition cannot be evaluated. Notice that the lemma is accepted if you move the semicolon in the parameter list of predicate foreach to declare the second parameter as an input parameter.

Lemma foreach_foo_unremove_remove suffers from a similar problem: VeriFast cannot figure out how to come up with a value for abs so that it can evaluate the boolean conditions that mention it. In this case, it's not so easy to fix.

Best regards,

Bart

[Elias Keis]

Hi Bart,

thank you for clarifying this! This will help us a lot with generating code for lists and similar structures.

Best regards,

Elias