examples/list_removal.mlw

   1
   2 (** Removing an element from a singly-linked list.
   3
   4     Authors: Jean-Christophe Filliâtre (CNRS)
   5              Andrei Paskevich (Univ Paris-Saclay)
   6
   7   The following is inspired by this interview of Linus Torvalds:
   8
   9     https://www.youtube.com/watch?v=o8NPllzkFhE
  10
  11   Assume that you are given singly-linked lists in C, like this:
  12
  13     typedef struct Entry *entry;
  14     struct Entry { entry next; };
  15     typedef struct List { entry head; } *list;
  16
  17   That is, there is a header structure (struct List) with a 'head'
  18   field to the first element of a singly-linked list of list cells
  19   (struct Entry).
  20
  21   You are given a list 'l' and some entry 'e' that belongs to the list,
  22   and you have to remove it from the list. There is a pedestrian way of
  23   doing it, like this:
  24
  25     void remove(list l, entry e) {
  26       entry prev = NULL, curr = l->head;
  27       while (curr != e) {
  28         prev = curr;
  29         curr = curr->next;
  30       }
  31       if (prev)
  32         prev->next = curr->next;
  33       else
  34         l->head = curr->next;
  35     }
  36
  37   But there is another one which avoids making a particular case for the
  38   first element, like this:
  39
  40     void remove2(list l, entry e) {
  41       entry *ind = &l->head;
  42       while ( *ind != e )
  43         ind = &( *ind )->next;
  44       *ind = ( *ind )->next;
  45     }
  46
  47   In the following, we explore the loop invariants involved in the
  48   verification of these two programs. We make the following two
  49   simplifications:
  50
  51   - The memory model does not make a distinction between the two types of
  52     structures. In practice, this is an important point in the discussion.
  53     But here we are rather focusing on the loop invariants.
  54
  55   - In the function contract, we underspecify the problem, using only
  56     the length of the list, not its contents.
  57
  58 *)
  59
  60 use int.Int
  61 use map.Map
  62
  63 (** Minimal memory model *)
  64
  65 type loc
  66 val (=) (x y: loc) : bool ensures { result <-> x=y }
  67
  68 type mem = loc -> loc
  69 val ref mem: mem
  70
  71 val constant null: loc
  72
  73 val constant head: loc
  74 val constant entry: loc (* the entry to be removed from the list *)
  75
  76 (** Program global variables *)
  77
  78 axiom head_is_not_null : head <> null
  79 axiom entry_is_not_null: entry <> null
  80 axiom head_is_not_entry: head <> entry
  81
  82 (** Chains of pointers. *)
  83
  84 (** When starting from `x` and dereferencing pointers `n` times we get `y` *)
  85 let rec predicate list (mem: loc -> loc) (x: loc) (n :int) (y: loc)
  86   requires { n >= 0 }
  87   variant  { n }
  88 = if n = 0 then x = y
  89   else x <> null && list mem mem[x] (n - 1) y
  90
  91 val get (x: loc) : loc
  92   requires { x <> null }
  93   ensures  { result = mem[x] }
  94
  95 val set (x y: loc) : unit
  96   requires { x <> null }
  97   writes   { mem }
  98   ensures  { mem = (old mem)[x <- y] }
  99
 100 let rec lemma list_concat
 101   (mem: mem) (x: loc) (n1: int) (y: loc) (n2: int) (z: loc)
 102   requires { n1 >= 0 } requires { n2 >= 0 }
 103   requires { list mem x n1 y }
 104   requires { y <> null }
 105   requires { list mem mem[y] n2 z }
 106   ensures  { list mem x (n1 + 1 + n2) z }
 107   variant  { n1 }
 108 = if n1 > 0 then list_concat mem mem[x] (n1 - 1) y n2 z
 109
 110 lemma path_shorten:
 111   forall mem x n y. list mem x n y -> n > 0 -> list mem mem[x] (n - 1) y
 112
 113 lemma path_extend:
 114   forall mem x n y. n >= 0 -> list mem y n x -> x <> null ->
 115   list mem y (n + 1) mem[x]
 116
 117 let rec lemma no_cycle_to_null (mem: mem) (e: loc) (n n': int)
 118   requires { 0 < n } requires { 0 <= n' } requires { e <> null }
 119   requires { list mem e n e }
 120   requires { list mem e n' null } ensures { false }
 121   variant  { n' }
 122 = if n' > 0 then begin
 123     list_concat mem mem[e] (n-1) e 0 mem[e];
 124     no_cycle_to_null mem mem[e] n (n' - 1)
 125   end
 126
 127 let lemma jump_over (mem: mem) (x: loc) (n1: int) (y: loc) (n2: int)
 128   requires { n1 >= 0   } requires { list mem x n1 y }
 129   requires { y <> null } requires { mem[y] <> null }
 130   requires { n2 > 0    } requires { list mem mem[y] n2 null }
 131   ensures  { list mem[y <- mem[mem[y]]] x (n1 + n2) null }
 132 = assert { list mem mem[mem[y]] (n2 - 1) null };
 133   let mem' = mem[y <- mem[mem[y]]] in
 134   let rec frame_after (n': int) (z: loc) (n: int)
 135      requires { 0 <= n' } requires { list mem y n' z    } requires { z <> y }
 136      requires { 0 <= n  } requires { list mem z n  null }
 137      ensures  { list mem' z n null }
 138      variant  { n }
 139   = if n > 0 then frame_after (n' + 1) mem[z] (n - 1) in
 140   let rec frame_before (z: loc) (n: int)
 141     requires { n >= 0 }
 142     requires { list mem  z n y }
 143     ensures  { list mem' z n y }
 144     variant  { n }
 145   = if n > 0 then frame_before mem[z] (n - 1) in
 146   frame_after 1 mem[y] n2;
 147   assert { list mem' mem[mem[y]] (n2 - 1) null };
 148   assert { list mem' y n2 null };
 149   frame_before x n1;
 150   ()
 151
 152 (* Code 1 *)
 153
 154 let remove1 (ghost n1 n2: int) : unit
 155   requires { n1 > 0 } requires { n2 > 0 }
 156   requires { list mem head  n1 entry }
 157   requires { list mem entry n2 null }
 158   ensures  { list mem head  (n1 + n2 - 1) null }
 159 = let ref prev = null in
 160   let ref curr = get head in
 161   let ghost ref n = 1 in
 162   while curr <> entry do
 163     invariant { 0 < n <= n1 }
 164     invariant { list mem head n curr }
 165     invariant { curr <> null }
 166     invariant { prev = null -> n = 1 }
 167     invariant { prev <> null -> mem[prev] = curr }
 168     invariant { prev <> null -> list mem head (n - 1) prev }
 169     invariant { list mem curr (n1 - n) entry }
 170     invariant { list mem entry n2 null }
 171     variant   { n1 - n }
 172     prev <- curr;
 173     curr <- get curr;
 174     n <- n + 1
 175   done;
 176   if prev = null then (
 177     jump_over mem head 0 head n2;
 178     set head (get curr);
 179   ) else
 180     set prev (get curr)
 181
 182 (* Code 2 *)
 183
 184 let remove2 (ghost n1 n2: int) : unit
 185   requires { n1 > 0 } requires { n2 > 0 }
 186   requires { list mem head  n1 entry }
 187   requires { list mem entry n2 null }
 188   ensures  { list mem head  (n1 + n2 - 1) null }
 189 = let ref ind = head in
 190   let ghost ref n = 1 in
 191   while get ind <> entry do
 192     invariant { 0 < n <= n1 }
 193     invariant { ind <> null }
 194     invariant { list mem head (n - 1) ind }
 195     invariant { list mem mem[ind] (n1 - n) entry }
 196     invariant { list mem entry n2 null }
 197     variant   { n1 - n }
 198     ind <- get ind;
 199     n <- n + 1
 200   done;
 201   set ind (get entry)