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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
(* $Id$ *)
open Names
open Nameops
open Pmisc
(* The type of effects.
*
* An effect is composed of two lists (r,w) of variables.
* The first one is the list of read-only variables
* and the second one is the list of read-write variables.
*
* INVARIANT: 1. each list is sorted in decreasing order for Pervasives.compare
* 2. there are no duplicate elements in each list
* 3. the two lists are disjoint
*)
type t = identifier list * identifier list
(* the empty effect *)
let bottom = ([], [])
(* basic operations *)
let push x l =
let rec push_rec = function
[] -> [x]
| (y::rem) as l ->
if x = y then l else if x > y then x::l else y :: push_rec rem
in
push_rec l
let basic_remove x l =
let rec rem_rec = function
[] -> []
| y::l -> if x = y then l else y :: rem_rec l
in
rem_rec l
let mem x (r,w) = (List.mem x r) or (List.mem x w)
let rec basic_union = function
[], s2 -> s2
| s1, [] -> s1
| ((v1::l1) as s1), ((v2::l2) as s2) ->
if v1 > v2 then
v1 :: basic_union (l1,s2)
else if v1 < v2 then
v2 :: basic_union (s1,l2)
else
v1 :: basic_union (l1,l2)
(* adds reads and writes variables *)
let add_read id ((r,w) as e) =
(* if the variable is already a RW it is ok, otherwise adds it as a RO. *)
if List.mem id w then
e
else
push id r, w
let add_write id (r,w) =
(* if the variable is a RO then removes it from RO. Adds it to RW. *)
if List.mem id r then
basic_remove id r, push id w
else
r, push id w
(* access *)
let get_reads = basic_union
let get_writes = snd
let get_repr e = (get_reads e, get_writes e)
(* tests *)
let is_read (r,_) id = List.mem id r
let is_write (_,w) id = List.mem id w
(* union and disjunction *)
let union (r1,w1) (r2,w2) = basic_union (r1,r2), basic_union (w1,w2)
let rec diff = function
[], s2 -> []
| s1, [] -> s1
| ((v1::l1) as s1), ((v2::l2) as s2) ->
if v1 > v2 then
v1 :: diff (l1,s2)
else if v1 < v2 then
diff (s1,l2)
else
diff (l1,l2)
let disj (r1,w1) (r2,w2) =
let w1_w2 = diff (w1,w2) and w2_w1 = diff (w2,w1) in
let r = basic_union (basic_union (r1,r2), basic_union (w1_w2,w2_w1))
and w = basic_union (w1,w2) in
r,w
(* comparison relation *)
let le e1 e2 = failwith "effects: le: not yet implemented"
let inf e1 e2 = failwith "effects: inf: not yet implemented"
(* composition *)
let compose (r1,w1) (r2,w2) =
let r = basic_union (r1, diff (r2,w1)) in
let w = basic_union (w1,w2) in
r,w
(* remove *)
let remove (r,w) name = basic_remove name r, basic_remove name w
(* substitution *)
let subst_list (x,x') l =
if List.mem x l then push x' (basic_remove x l) else l
let subst_one (r,w) s = subst_list s r, subst_list s w
let subst s e = List.fold_left subst_one e s
(* pretty-print *)
open Pp
open Util
open Himsg
let pp (r,w) =
hov 0 (if r<>[] then
(str"reads " ++
prlist_with_sep (fun () -> (str"," ++ spc ())) pr_id r)
else (mt ()) ++
spc () ++
if w<>[] then
(str"writes " ++
prlist_with_sep (fun ()-> (str"," ++ spc ())) pr_id w)
else (mt ())
)
let ppr e =
Pp.pp (pp e)
|
