1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
module PtrCursor
use int.Int
use map.MapEq
use mach.int.Int32
use mach.c.C
use array.Array
(* we assume that a non-null pointer exists *)
val ghost dummy_nonnull () : ptr int32
ensures { is_not_null result /\ plength result = 1 /\ offset result = 0 }
ensures { min result = 0 /\ max result = plength result }
ensures { writable result }
ensures { (data result)[0] = 0 }
type cursor = {
current : ptr int32;
mutable new : bool;
len : int32;
ghost mutable freed : bool;
bound : int32
}
invariant { 0 < len }
invariant { not freed ->
(plength current = len /\
offset current = 0 /\
valid current len /\
min current = 0 /\
max current = len /\
is_not_null current /\
writable current /\
forall i. 0 <= i < len -> (data current)[i] < bound) }
by { current = dummy_nonnull (); new = true;
len = 1; freed = false; bound = 42 }
val ([]) (a: array 'a) (i: int32) : 'a
requires { [@expl:index in array bounds] 0 <= i < length a }
ensures { result = ([]) a i }
val ([]<-) (a: array 'a) (i: int32) (v: 'a) : unit writes {a}
requires { [@expl:index in array bounds] 0 <= i < length a }
ensures { a.elts = Map.set (old a).elts i v }
ensures { a = ([<-]) (old a) i v }
let partial create_cursor (l:int32) (b: int32) : cursor
requires { 0 < l }
requires { 0 < b }
ensures { result.len = l }
ensures { not result.freed }
ensures { forall i. 0 <= i < l -> (data result.current)[i] = 0 }
ensures { bound result = b }
= let a = malloc (UInt32.of_int32 l) in
c_assert (is_not_null a);
for i = 0 to l-1 do
invariant { forall j. 0 <= j < i -> (data a)[j] = 0 }
set_ofs a i 0;
done;
{ current = a; new = true; len = l; freed = false; bound = b }
let free_cursor (c:cursor) : unit
requires { not c.freed }
ensures { c.freed }
writes { c.freed }
writes { c.current }
writes { c.current.data }
= free c.current;
c.freed <- true
val get_current (c:cursor) : array int32
requires { not c.freed }
ensures { length result = plength c.current }
ensures { map_eq_sub result.elts (pelts c.current) 0 c.len }
alias { c.current.data with result }
let next (c: cursor) : unit
requires { not c.freed }
requires { 0 < c.bound < max_int32 }
= let a = get_current c in
label L in
let n = c.len in
let b = c.bound in
let ref r = (n-1) in
while r >= 0 && a[r] = b - 1 do
invariant { -1 <= r < n }
invariant { forall s. r < s < c.len -> a[s] = b - 1 }
variant { r }
r <- r - 1
done;
if (r < 0) then
c.new <- false
else begin
a[r] <- a[r] + 1;
assert { a[r] < b };
for i = r+1 to n-1 do
invariant { forall j. r+1 <= j < i -> a[j] = 0 }
invariant { forall j. 0 <= j < r -> a[j] = a[j] at L }
invariant { a[r] = a[r] at L + 1 }
a[i] <- 0
done;
c.new <- true;
end
let partial main () : int32
= let c = create_cursor 4 4 in
for i = 0:int32 to 255 do
invariant { not c.freed }
invariant { forall i. 0 <= i < c.len -> (data c.current)[i] < c.bound }
c_assert c.new;
next c;
done;
c_assert (not c.new);
free_cursor c;
0
end
|
