Figuring out proper loop invariant when appending to a linked list with verifiable C

Question

I'm working on the beta 5th software foundations module which covers verifiable C. I'm on the final portion, which has to do with operations on a hash map (which requires operations on a linked list).

https://www.cs.princeton.edu/~appel/vc/vc-0.9.5/Verif_hash.html

I'm a bit stuck on body_incr_list.

The code being verified:

void incr_list (struct cell **r0, char *s) {
  struct cell *p, **r;
  for(r=r0; ; r=&p->next) {
    p = *r;
    if (!p) { *r = new_cell(s,1,NULL); return; }
    if (strcmp(p->key, s)==0) {p->count++; return;}
  }
}

This does a couple of new things...a pointer of pointers, and the fact that p is null going into the loop, but then is guaranteed to have a value if it loops. The spec given by the module is:

Definition incr_list_spec : ident × funspec :=
 DECLARE _incr_list
 WITH r0: val, al: list (list byte × Z), s: val,
      sigma : list byte, gv: globals
 PRE [ _r0 OF tptr (tptr tcell), _s OF tptr tschar ]
    PROP (list_get sigma al < Int.max_unsigned)
    LOCAL (temp _r0 r0; temp _s s; gvars gv)
    SEP (listboxrep al r0; cstring Ews sigma s; mem_mgr gv)
 POST [ tvoid ]
      PROP ( ) LOCAL ()
      SEP (listboxrep (list_incr sigma al) r0;
           cstring Ews sigma s; mem_mgr gv).

The whole exercise hinges on a proper loop invariant. Here was my attempt

forward_loop (EX al':list (list byte * Z), EX r0': val,
PROP ()
LOCAL (temp _r r0'; temp _r0 r0; temp _s s; gvars gv)
SEP (
  listboxrep al' r0';
  cstring Ews sigma s;
  mem_mgr gv;
  listboxrep al' r0' -* (ALL sigma:list byte, listrep (list_incr sigma []) nullval -* listboxrep (list_incr sigma al) r0)
)).

With this I'm able to make some basic progress, but I get stuck on the processing of:

    if (!p) { *r = new_cell(s,1,NULL); return; }

The reason is that right now in the SEP clause, I have listboxrep al' r0', but in order to make it past the line

    p = *r;

I need to unfold it into data_at Ews (tptr tcell) p r0' * listrep al' p. Again, not a huge issue but in the case where p is null and it creates the new cell (*r = new_cell(s,1,NULL); return;), I get a proof target that I don't know if it can be solved.

This is because data_at Ews (tptr tcell) p r0' gets converted into data_at Ews (tptr tcell) vret r0', but we still just have listrep al' p, not listrep al' vret. Though in this case, al' is probable to be [], which means we have listrep [] p, though I'm not really sure what can be done with that. If I follow this through, I end up getting to the following entailment:

(list_cell sigma 1 (Vint (Int.repr 0)) vret *
 data_at Ews (tptr tcell) vret r0' *
 ((EX p : val, data_at Ews (tptr tcell) p r0' * (!! (p = nullval) && emp)) -*
  (ALL sigma0 : list byte,
   (EX y : val, list_cell sigma0 1 y nullval * (!! (y = nullval) && emp)) -*
   listboxrep (list_incr sigma0 al) r0)))%logic
|-- listboxrep (list_incr sigma al) r0

This leads me to believe that my invariant is incorrect...for example, if I do the munging to set the p in

EX p : val, data_at Ews (tptr tcell) p r0' * (!! (p = nullval) && emp)

Then of course it needs to be nullval. But the value that we have is data_at Ews (tptr tcell) vret r0'...

So I don't know. I am pretty sure that I need to refine my invariant, but am not sure how! Would appreciate any pointers.

Answer 1

Let's focus on the SEP clause of your proposed invariant:

SEP (
 listboxrep al' r0';
 cstring Ews sigma s;
 mem_mgr gv;
 listboxrep al' r0' -* (ALL sigma:list byte, listrep (list_incr sigma []) nullval -* listboxrep (list_incr sigma al) r0)
)).

First, the expression listrep (list_incr sigma []) nullval is equivalent to (list_incr sigma [] = nil && emp), so you might ask yourself, is that what you meant?

Second, think about your magic-wand, listboxrep al' r0' -* .... The first clause of your SEP says, "right now I have listboxrep al' r0' ". The wand-expression says, "I can fill the r0' hole with exactly the list al'. But list-incr is going to modify the contents of the hole. So you don't want exactly al' in the (left side of) the magic wand, you want some universally quantified list-value, that you can fill in later.