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;
};