Abstract Arithmetisation of the Heap

Coq formalisation and abstract VcGen

download

Annotated programs

2D Matrix

// Initialise a 2D matrix
mat = n@a; <br>
i = 0;
while(i<n){
  tb = m@b ;
  mat[i] = tb ;
  hint {{
      i < n
	&& mat.lb = @a && mat.ts  = @a.ts && mat.of = 0
	&& ((mat.lb = LbO && mat.ts = TsO) => (Size = n && (0 <= OffO && OffO <= i => (LbD = @b && TsD = @b.ts - i + OffO ))))
	&& ((LbO = @b && @b.ts - i <= TsO && TsO <= @b.ts ) => Size =m)
	}};
  i = i + 1
    };
assume {{ j < n }};
len = (mat[j]).length ;
ensure {{ len = m }}

Array Initialisation

// Array initialisation [Halbwachs & Péron, PLDI'08]
A[1] = n;
for(i=2; i<= n; i+1){
  hint {{
      A.of >= 0 && A.ts >= 0 && A.lb >= 0
	&& 2 <= i &&    i <= n
	&& (LbO = A.lb && TsO = A.ts && 1 +  A.of <= OffO && OffO < A.of + i => (LbD = 0 && TsD = 0 && OffD = n + OffO - A.of - 1)) }};
  A[i] = A[i - 1] + 1;
 };
assume {{ 1 <= j }};
assume {{ j <= n }};
v = (int) (A [j]) ;
r = n + j -1 ;
ensure {{ v = r}};

First Non-Null

// First non-null element of an array [Halbwachs & Péron, PLDI'08]
s = n + 1;
for ( i = 1 ; i <= n ; i+1) {
  hint {{
      i <= n && i >= 1
	&& A.lb >= 0 && A.ts >= 0 && A.of >= 0 && s >= 1
	&& (s < i || s = n + 1)
	&& (s = n + 1 =>
	    ((LbO = A.lb && TsO = A.ts && A.of +1 <= OffO && OffO < A.of + i) => (LbD = 0 && TsD = 0 && OffD = 0)))
	&&
 	( s < i  =>
 	  (
	   ((LbO = A.lb && TsO = A.ts && A.of +1 <= OffO && OffO < A.of + s) => (LbD = 0 && TsD = 0 && OffD = 0))
	   &&
	   ( (LbO = A.lb && TsO = A.ts && OffO = A.of + s) => (~ (LbD = 0 && TsD = 0 && OffD = 0)))
 	   ))
	}};
  if (s >= n + 1 )  if (A[i] != null)  s = i;
 };
assume {{1 <= j && j < s && s <= n}};
v = A[j];
ensure {{v == null}}

Linked-List

// Create a null-terminated linked list of integers
assume {{ n > 0 }};
i = 0 ;
lst = 2@l;
lsti = lst;
while (i < n ) {
  lsti[0] = (0,0,?);
  rst = 2@r ;
  lsti[1] = rst ;
  lsti = rst ;
  hint {{
      // basic numeric invariants
      0 <= i
	&& i < n && n > 0 && @l.ts > 0 && @r.ts > 0
	// invariant of the head of the list
	&& lst.lb = @l && lst.ts = @l.ts && lst.of = 0
	// invariant of the newly created cell
	&& rst.lb = @r  && rst.ts = @r.ts && rst.of = 0
	// rst = lsti
	&& lsti.lb = rst.lb && lsti.ts = rst.ts && rst.of = lsti.of
	// Heap invariants
	// head
	&& ( (LbO = @l && TsO = @l.ts) =>
	     ( (OffO = 0 => (LbD = 0 && TsD = 0 ))
	       &&
	       (OffO = 1 => (LbD = @r && TsD = @r.ts - i && OffD = 0)) )
	     )
	// tail
	&& (LbO = @r && @r.ts - i <= TsO && TsO < @r.ts && OffO = 1  => (LbD = @r && TsD = TsO + 1 && OffD = 0))
	&& ((LbO = @r && TsO = @r.ts)  => (LbD = 0 && TsD = 0 && OffD = 0))
	}};
  i = i + 1;
 };
ensure {{ tt }}

Sentinel

// sentinel [Halbwachs & Péron, PLDI'08 ]
assume {{n > 1}};
A[n] = x ;
 i = 1 ;
 while (A[i] != x){
   hint {{
       LbO = A.lb && TsO = A.ts && OffO = A.of + n => (LbD = x.lb && TsD = x.ts && OffD = x.of)
       && i < n
	 }};
   i = i + 1;
 };
ensure {{ i <= n}}

Triangular Matrix

// Ensure that we construct a triangular matrix
i = 0;
t = n@a1;
while (i < n){
 ti = i@a ;
  *t = ti ;
  hint {{
        t.lb = @a1
	&& t.ts = @a1.ts
	&& ((t.lb = LbO && t.ts = TsO) => (Size = n && (0 <= OffO && OffO <= t.of => (LbD = @a && TsD = @a.ts - i + OffO ))))
	&& t.of = i
	&& ti.lb = @a && i < n && ti.ts = @a.ts
	&& ((LbO = @a && @a.ts - i <= TsO && TsO <= @a.ts ) => Size = TsO - @a.ts + i) }};
 i = i + 1;
 t = t ++ 1
   };
assume {{ k < n }} ;
tf = (t.lb, @a1.ts  ,k);
len = (*tf).length;
ensure {{ len = k }}

Array Maximum

// Array maximum [Halbwachs & Péron, PLDI'08]
max = (int) (A[1]);
for( i = 2 ; i<= n ; i+1){
  hint {{
      A.of >= 0
	&& i >= 2 && i <= n
	&& ( (LbO = A.lb && TsO = A.ts && A.of + 1 <= OffO && OffO < A.of + i => max >= OffD))
	}};
  if (max < A[i])
    max = (int) (A[i]);
 };
assume {{ 1 <= j && j <= n }};
v = (int) (A[j]);
ensure {{ max >= v}}

Length List

// Ensure that the length of a list of length n IS n
#include  <linkedList.c>

//[lst] contains a linked-list
list = lst ;
list = list[1]; // pointing on the first @r node
i=0;
 while (list != null){
    hint HH {{
        n > 0 && i < n &&
        // Heap invariant
        (LbO = @r && @r.ts - n +1 <= TsO && TsO < @r.ts && OffO = 1  => (LbD = @r && TsD = TsO + 1 && OffD = 0))
  	&& ((LbO = @r && TsO = @r.ts )  => (LbD = 0 && TsD = 0 && OffD = 0))
  	&& @r.ts > 0 && @l.ts > 0
  	// Other invariants
  	&& list.of = 0
  	&& list.lb = @r && list.ts = @r.ts - n + 1 + i
   	}};
   list = list[1];
   i  = i + 1;
  };
 ensure {{ i = n }}

Reverse List

// Reversal of a linked list
#include  <linkedList.c>

//[lst] contains a linked-list
list = lst ;
list = list[1]; // pointing on the first @r node

res = null;
assume {{n=2}};
while (list!=null) {
   hint {{
       n =2
	 // Invariant of [list]
	 && list.of = 0
	 && list.lb = @r
	 && @r.ts > 0 && @l.ts > 0
	 && @r.ts - n + 1 <= list.ts && list.ts <= @r.ts
	 // Invariant of [res]
	 && res.of = 0
	 && (list.ts = @r.ts - n + 1 => (res.lb = 0 && res.ts = 0 ))
	 && ((~ (list.ts = @r.ts - n + 1)) => (res.lb = @r && res.ts = list.ts -1))
	 // Heap invariant 'after' the [list] pointer
	 && ((LbO = @r && list.ts <= TsO && TsO < @r.ts && OffO = 1)  => (LbD = @r && TsD = TsO + 1 && OffD = 0))
	 && ((LbO = @r && TsO = @r.ts )  => (LbD = 0 && TsD = 0 && OffD = 0))
	 // Heap invariant 'before' the [list] pointer
	 && ((LbO = @r && @r.ts - n + 1  < TsO && TsO < list.ts && OffO = 1) => (LbD = @r && TsD = TsO - 1 && OffD = 0))
	 && ((LbO = @r && @r.ts - n + 1  = TsO && TsO < list.ts && OffO = 1) => (LbD = 0 && TsD = 0 && OffD = 0))
	 }};
  temp = list[1];
  list[1] = res;
  res = list;
  list = temp;
 }

Traverse List

// Traversal of a linked list
#include  <linkedList.c>

//[lst] contains a linked-list
list = lst ;
list = list[1]; // pointing on the first @r node
while (list != null){
   hint {{
       n > 0 &&
       // Heap invariant
       (LbO = @r && @r.ts - n +1 <= TsO && TsO < @r.ts && OffO = 1  => (LbD = @r && TsD = TsO + 1 && OffD = 0))
 	&& ((LbO = @r && TsO = @r.ts )  => (LbD = 0 && TsD = 0 && OffD = 0))
 	&& @r.ts > 0 && @l.ts > 0
 	// Other invariants
 	&& list.of = 0
 	&& list.lb = @r && @r.ts - n + 1 <= list.ts && list.ts <= @r.ts
  	}};
  list = list[1];
 };

Until Pivot

// Snipet from the partition routine of Quicksort
assume {{ i < n }} ;
e = (int)(t [ n ]) ;
while (t[i] < e) {
  hint {{
      (t.ts = TsO && t.lb = LbO && t.of + n = OffO => OffD = e)
	&&
      i < n
	}};
  i = i + 1 }

Insertion Sort

// sorted until i (included) j exluded
#define sorted(s1,s2,i,j)					      \
  ( ((A.reg = RegO@s1 && A.ts = TsO@s1  && OffO@s1 >= i && OffO@s1 < j && \
      A.reg = RegO@s2 && A.ts = TsO@s2  && OffO@s2 >= i && OffO@s2 < j && \
      OffO@s1 <= OffO@s2) => OffD@s1 <= OffD@s2))

#define x_lt(s1) \
  ( ((A.reg = RegO@s1 && A.ts = TsO@s1 && j + 1 <= OffO@s1 && OffO@s1 <= i) => x < OffD@s1))


#define A_idx_val(s,A,idx,cmp,v)			\
  ( ((A.reg = RegO@s && A.ts = TsO@s && OffO@s = idx) => OffD@s cmp v) )

#define sorted_except(s1,s2) \
  ((A.reg = RegO@s1 && A.ts = TsO@s1 && 0 <= OffO@s1 &&  \
	  A.reg = RegO@s2 && A.ts = TsO@s2 && OffO@s1 <= OffO@s2 && OffO@s2 <= i \
    && OffO@s1 <> j && OffO@s2 <> j) => OffD@s1 <= OffD@s2 )




assume {{A.of = 0}};
for(i = 1 ; i<= n ; i+1){
  hint Main {{
      1 <= i && i <= n
	&& A.of = 0
	&& OffO@0 >= 0
	&& OffO@1 >= 0
	&& sorted(0,1,0,i)
	}};
  x =(A[i]).of;
  j =i ;
  while (j > 0 &&  A[j-1] > x) {
    hint Inner {{ 0 < j && j <= i && i <= n
	  && A.of = 0
	  && OffO@0 >= 0
	  && OffO@1 >= 0
	  && A_idx_val(0,A,(j-1),>,x)
	  && sorted_except(0,1)
	  && x_lt(1)
	  }};
    A[j] =A[j-1];
    j = j - 1;
  };
  A[j ] = x;
 } ;
hint End {{ A.of = 0 && sorted(0,1,0,n+1) }} ;
assume {{ k <= l && l <= n }};
ensure {{ A[k] <= A[l] }}

Arrays and Lists

#include "macros.h"
#define next(y)  y[0]
#define len(y)   y[1]
#define data(y)  y[2]


#define is_list(i) \
  ( ((RegO = @r && TsO < i && OffO = 0) =>	\
     (RegD = @r && TsD = TsO + 1 && OffD = 0) ) \
    )						\

#define is_list_of_lengh(x,i)						\
  ( (is_null(x)	=> i = 0)						\
    &&  (~ is_null(x) =>						\
	 (i > 0 && x.reg = @r && x.of = 0 && x.ts = 0))			\
    && is_list(i-1)							\
    &&									\
    ( (RegO = @r && TsO = i-1 && OffO = 0) =>				\
      (RegD = 0 && TsD = 0 && OffD = 0) )				\
    )									\

// Ensure that that 'x' is a list
// Instead of doing assume we could *simply*
// update list elements with fresh inceasing time-stamps
assume {{ x.of = 0}};
i = 0;
l = x;
while (l != null) {
  assume  {{ l.reg = @r && l.of = 0 && l.ts = i}};
  hint {{ x.reg = @r && x.of = 0 && x.ts = 0 &&
	l.reg = @r && l.of = 0 && l.ts = i &&
	is_list(i)
	}};
  l = l[0]; i = i + 1 ;
 };
//hint IList {{ is_list_of_lengh(x,i) }};

j = 0 ;
for (y = x ; y != null ; next(y)) {
  hint IData {{
      is_list_of_lengh(x,i)
	&& x.reg = @r
	&& ~ (is_null(y))
	&& y.reg = x.reg && y.ts = j && y.of = 0
	&& j < i
	&& @data.ts >= 0
	&& @data.ts - j >= 0
	&& ((RegO = @r && TsO < j && OffO = 2) =>
	    (RegD = @data && OffD = 0 && TsD = @data.ts - j + TsO + 1) )
	&& ((RegO@0 = @r && TsO@0 < j && OffO@0 = 1
	     && RegO@1 = @data && TsO@1 = @data.ts - j + TsO@0 + 1
	     ) => (RegD@0 = 0 && TsD@0 = 0 &&  4* OffD@0 = Size@1) )
	}};
  t = ? ;
  len(y) = t ;
  d = (4*t)@data  ;
  data(y) = d ;
  j = j + 1;
 };

 j = 0 ;
 for (y = x ; y != null ; next(y)) {
   hint IOut {{ is_list_of_lengh(x,i)
 	&& ~ (is_null(y))
 	&& y.reg = x.reg && y.ts = j && y.of = 0
 	&& j < i
 	&& ((RegO = @r && TsO < i && OffO = 2) =>
 	    (RegD = @data && OffD = 0 && TsD = @data.ts - i + TsO + 1) )
 	&& ((RegO@0 = @r && TsO@0 < i && OffO@0 = 1
 	     && RegO@1 = @data && TsO@1 = @data.ts - i + TsO@0 + 1
 	     ) => (RegD@0 = 0 && TsD@0 = 0 &&  4* OffD@0 = Size@1) )
 	}};
    lg1 = len(y).of ;
    lg2 = data(y).length ;
    ensure {{ 4*lg1 = lg2 }};
   j = j + 1
  }

Binary Tree

#define Node() 2@node
#define left(n) n[0]
#define right(n) n[1]

// Initialise an array
sz = 2 * n + 1;
t = sz@r;
for(i=0; i<sz ; i+1){
  hint {{
      // purely numeric invariants
      sz = 2 * n + 1
	&& i < sz
	&& @node.ts - i >= 0
      // Invariant of t
	&&
      (t.reg = @r && t.ts = @r.ts && t.of = 0)
	// Content of t
	&& ((RegO = @r && TsO = t.ts && 0<= OffO && OffO < i)  => (RegD = @node && TsD = @node.ts - i +1 +OffO  && OffD = 0))
	// Content of node
	&& ((RegO = @node && @node.ts - i + 1 <= TsO && TsO <= @node.ts) => (RegD = 0 && TsD = 0 && OffD = 0))
	}};
  nd = Node();
  t[i] = nd
 }

// Construct trees
for (i=0; i<n ; i+1){
  hint {{
      sz = 2* n + 1
	&& i < n
	&& @node.ts - sz >= 0
	&& (t.reg = @r && t.ts = @r.ts && t.of = 0)
	// Content of t
	&& ((RegO = @r && TsO = t.ts && 0<= OffO && OffO < sz)  => (RegD = @node && TsD = @node.ts - sz + 1 +OffO  && OffD = 0))

	// Content of trees
	&& ((RegO = @node && @node.ts - sz + 1 <= TsO && TsO < @node.ts -sz + 1 + i && OffO = 0) =>
	    (
	     (RegD = 0 && TsD = 0 && OffD = 0) || (RegD = @node && TsD = 2*TsO  - (@node.ts -sz) && OffD = 0)))

	&& ((RegO = @node && @node.ts - sz + 1 <= TsO && TsO < @node.ts -sz + 1 + i && OffO = 1) =>
	    (
	     (RegD = 0 && TsD = 0 && OffD = 0) || (RegD = @node && TsD = 2*TsO + 1 - (@node.ts -sz) && OffD = 0)))

	&& ((RegO = @node && @node.ts - sz + 1 + i <= TsO && TsO <= @node.ts) => (RegD = 0 && TsD = 0 && OffD = 0))

	}};
  if(i=?) left(t[i]) = t[2*i+1] else left(t[i]) = null ;
  if(i=?) right(t[i]) = t[2*i+2] else right(t[i]) = null ;
 };
  hint InvPapier {{
      sz = 2* n + 1
	&& @node.ts - sz >= 0
	&& (t.reg = @r && t.ts = @r.ts && t.of = 0)
	// Content of t
	&& ((RegO = @r && TsO = t.ts && 0<= OffO && OffO < sz)  => (RegD = @node && TsD = @node.ts - sz + 1 +OffO  && OffD = 0))

	// Content of trees
	&& ((RegO = @node && @node.ts - sz + 1 <= TsO && TsO < @node.ts -sz + 1 + n && OffO = 0) =>
	    (
	     (RegD = 0 && TsD = 0 && OffD = 0) || (RegD = @node && TsD = 2*TsO  - (@node.ts -sz) && OffD = 0)))

	&& ((RegO = @node && @node.ts - sz + 1 <= TsO && TsO < @node.ts -sz + 1 + n && OffO = 1) =>
	    (
	     (RegD = 0 && TsD = 0 && OffD = 0) || (RegD = @node && TsD = 2*TsO + 1 - (@node.ts -sz) && OffD = 0)))

	&& ((RegO = @node && @node.ts - sz + 1 + n <= TsO && TsO <= @node.ts) => (RegD = 0 && TsD = 0 && OffD = 0))

	}};
// prove that trees are acyclic
tr = t[0];
while(tr!=null) {
  hint {{
      sz = 2* n + 1
	&& @node.ts - sz >= 0
	&& (t.reg = @r && t.ts = @r.ts && t.of = 0)
	// Content of t
	&& ((RegO = @r && TsO = t.ts && 0<= OffO && OffO < sz)  => (RegD = @node && TsD = @node.ts - sz + 1 +OffO  && OffD = 0))

	// Content of trees
	&& ((RegO = @node && @node.ts - sz + 1 <= TsO && TsO < @node.ts -sz + 1 + n && OffO = 0) =>
	    (
	     (RegD = 0 && TsD = 0 && OffD = 0) || (RegD = @node && TsD = 2*TsO  - (@node.ts -sz) && OffD = 0)))

	&& ((RegO = @node && @node.ts - sz + 1 <= TsO && TsO < @node.ts -sz + 1 + n && OffO = 1) =>
	    (
	     (RegD = 0 && TsD = 0 && OffD = 0) || (RegD = @node && TsD = 2*TsO + 1 - (@node.ts -sz) && OffD = 0)))
	&& ((RegO = @node && @node.ts - sz + 1 + n <= TsO && TsO <= @node.ts) => (RegD = 0 && TsD = 0 && OffD = 0))
	&& tr.reg = @node && tr.of = 0 &&   @node.ts - sz + 1 <= tr.ts && tr.ts <= @node.ts

	}};
  if(i=?) tr1 = left(tr) else tr1 = right(tr) ;
  ensure {{ (tr.ts < tr1.ts) || (tr1 == null) }};
  tr = tr1;

    };