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
|
(* Why3 specification file for selected code in the sudoers crate.
All proof goals generated by Why3 1.5.1 can be discharged using CVC4 1.8 *)
module Sudoers
use array.Array
use option.Option
use ref.Ref
use int.Int
(* loose models for the types in sudoers::Ast *)
type metavar 'a = All | Only 'a
type qualified 'a = Yes 'a | No 'a
type spec 'tag 'a = { inner: qualified (metavar 'a); info: 'tag }
predicate contains (pred: 'a -> bool) (a: array 'a)
= exists i. 0 <= i < length a /\ pred a[i]
function who (item: spec 'tag 'a): metavar 'a
= match item.inner with
| Yes x -> x
| No x -> x
end
function condition (item: spec 'tag 'a): option 'tag
= match item with
| { inner = Yes _; info = tag } -> Some tag
| _ -> None
end
function matched_by (pred: 'a -> bool) (item: spec 'tag 'a): bool
= match who item with
| All -> true
| Only x -> pred x
end
let function bool_then (b: bool) (x: 'a): option 'a
= if b then Some x else None
predicate final_match (pred: 'a -> bool) (a: array 'a) (f: 'a -> 'b) (x: 'b)
= exists i. 0 <= i < length a /\ pred a[i] /\ f a[i] = x /\ forall k. i < k < length a -> not pred a[k]
(* Why3 model of the sudoers::find_item function *)
let find_item (items: array (spec 'tag 'a)) (pred: 'a -> bool): option 'tag
returns {
| Some tag -> final_match (matched_by pred) items condition (Some tag)
| None -> not contains (matched_by pred) items \/ final_match (matched_by pred) items condition None
}
= let result = ref None in
for i = 0 to items.length - 1 do
invariant { forall tag. !result = Some tag <->
exists j. 0 <= j < i /\ matched_by pred items[j] /\ Some tag = condition items[j] /\
forall k. j < k < i -> not matched_by pred items[k] }
let (judgement, who) = match items[i].inner with
| No x -> (false, x)
| Yes x -> (true, x)
end in
let info = items[i].info in
match who with
| All -> result := judgement.bool_then(info)
| Only id -> if pred id then result := judgement.bool_then(info);
end;
done;
(* perform a "virtual loop" to strength the case !result = None;
this could also be solved by adding a ghost variable above *)
ghost if is_none !result && contains (matched_by pred) items then
for i = items.length - 1 downto 0 do
invariant { forall k. i < k < items.length -> not matched_by pred items[k] }
invariant { exists k. 0 <= k <= i /\ matched_by pred items[k] }
if matched_by pred items[i] then break
done;
!result;
end
|
