-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathstrongestpost.ml
227 lines (209 loc) · 10.4 KB
/
strongestpost.ml
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
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
open Tuple
open Function
open Option
open Listutils
open Name
open Formula
open Location
open Assign
(* This file is part of Arsenic, a proofchecker for New Lace logic.
Copyright (c) 2015 Richard Bornat.
Licensed under the MIT license (sic): see LICENCE.txt or
https://opensource.org/licenses/MIT
*)
(* ******************** hatting *************************
****************************************************** *)
let enhat hatting orig_f =
let rec opt_hat f =
match f.fnode with
| Fvar(None,NoHook,v) -> _SomeSome (_recFvar (Some hatting) NoHook v)
| Bfr (None,NoHook,bf) -> if is_Tildehatting hatting
then _SomeSome (_recBfr (Some hatting) NoHook bf)
else _SomeSome (conjoin [f; hat bf]) (* because B(P)=>P *)
| Univ (NoHook,uf) -> _SomeSome (conjoin [f; hat uf]) (* because U(P)=>P *)
(* | Latest (None,NoHook,v) -> if hatting=InflightHat
then _SomeSome (_recLatest There NoHook v)
else Some None (* don't touch it! *)
*)
| Sofar (NoHook,sf) -> Some None (* because Sofar(P)=>enhat(P) anyway *)
| Ouat (None,NoHook,sf) -> _SomeSome (_recOuat (Some hatting) NoHook sf) (* Ouat is local, always hatted *)
| Since (None,NoHook,f1,f2) -> _SomeSome (_recSince (Some hatting) NoHook f1 f2) (* ditto Since *)
(* we hat even inside binders. Oh yes. Because binding a variable doesn't bind thread or epoch *)
| Binder (bk,n,bf) -> (ohat bf &~~ (_SomeSome <.> _recBinder bk n))
|~~ (fun () -> Some None)
| Fvar _
| Bfr _
| Univ _
| Sofar _
| Ouat _
| Since _ -> raise (Invalid_argument (Printf.sprintf "Strongestpost.enhat.opt_hat %s in %s %s"
(string_of_formula f)
(string_of_hatting hatting)
(string_of_formula orig_f)
)
)
| _ -> None
and ohat f = Formula.optmap opt_hat f
and hat f = Formula.map opt_hat f
in
hat orig_f
(* ******************** strongest-post substitution *************************
Takes an assoc list mapping, from names to formulas.
Bfr, Univ, Sofar, Ouat:
If P[mapping]=P then (M P)[mapping] = M P;
(M P)[regmapping] = M (P[regmapping]);
(_B P)[varmapping] = (-)_B(P)/\P[varmapping];
(_U P)[varmapping] = (-)_U(P)/\P[varmapping];
(_S P)[varmapping] = (-)_S(P)/\P[varmapping];
(_O P)[varmapping] = (-)_O(P)
Since:
If P[mapping]=P and Q[mapping]=Q then (P since Q)[mapping] = P since Q
(P since Q)[regmapping] = P[regmapping] since Q[regmapping]
(P since Q)[varmapping = (-)(P since Q) /\ P[varmapping]
************************************************************************** *)
let optsp_substitute mapping orig_f =
let isvarmapping mapping f =
if List.for_all (Name.is_anyvar <.> fstof2) mapping then true
else
if List.for_all (Name.is_anyreg <.> fstof2) mapping then false
else
raise (Invalid_argument ("sp_substitute [" ^
string_of_assoc Name.string_of_name string_of_formula ":" "; " mapping ^
"] " ^ string_of_formula orig_f ^
", which contains " ^ string_of_formula f))
in
let rec optsub mapping f =
let domodality mm condis mf =
(subopt mapping
&~ (fun mf' ->
if isvarmapping mapping f
then _SomeSome (condis [mm Hook mf; mf'])
else _SomeSome (mm NoHook mf')
)
) mf
|~~ (fun () -> Some None)
in
match f.fnode with
| Freg r -> (try _SomeSome (mapping <@> r) with Not_found -> None)
(* Flogc omitted deliberately: you can't assign to a logical constant *)
(* We only substitute for unhooked variables -- None+NoHook, There+NoHook *)
| Fvar (None,NoHook,v) -> (try _SomeSome (mapping <@> v) with Not_found -> None)
| Fvar (_,NoHook,v) -> None (* Formula.optmap leaves it alone *)
| Binder (bk,n,bf) -> (subopt (List.remove_assoc n mapping) &~ (_SomeSome <.> _recBinder bk n)) bf
|~~ (fun () -> Some None) (* don't touch it! *)
| Bfr (None,NoHook,bf) -> domodality (_recBfr None) conjoin bf
| Bfr (Some _,NoHook,_) -> Some None
| Ouat (None, NoHook, ouf) -> domodality (_recOuat None) (fun fs -> List.hd fs) ouf
| Ouat (Some _,NoHook,_) -> Some None
| Since (None,NoHook,f1,f2) -> (if isvarmapping mapping f
then (* x\xhook affects only f1 *)
subopt mapping f1
&~~ (fun f1' -> _SomeSome (conjoin [f; f1']))
else (* r\rhook affects both *)
optionpair_either (subopt mapping) f1 (subopt mapping) f2
&~~ (fun (f1,f2) -> _SomeSome (_recSince None NoHook f1 f2))
)
|~~ (fun () -> Some None)
| Since (Some _,NoHook,_,_) -> Some None
| Univ (NoHook,uf) -> domodality _recUniv conjoin uf
(* | Latest (pl,NoHook,v) -> if List.mem_assoc v mapping
then _SomeSome (_recLatest pl Hook v)
else Some None
*)
| Sofar (NoHook, sf) -> domodality _recSofar conjoin sf
| Fvar _
| Bfr _
| Univ _
(* | Latest _ *)
| Sofar _
| Ouat _
| Since _ -> raise (Invalid_argument (Printf.sprintf "sp_substitute [%s] %s, which contains %s"
(string_of_assoc string_of_name string_of_formula "->" ";" mapping)
(string_of_formula orig_f)
(string_of_formula f)
)
)
| _ -> None
and subopt mapping = Formula.optmap (optsub mapping)
in
subopt mapping orig_f
let sp_substitute mapping f =
(optsp_substitute mapping ||~ id) f
(* strongest_post generates new names, so feels no need to use Exists *)
let strongest_post with_result pre assign =
let decorate f = if with_result then f else _recTrue in
let old_name name =
if Name.is_anyvar name then _recFvar None Hook name
else _recFname (name ^ "!old")
in
let sp_multiple is_varsubst mapping locs es =
let sub = sp_substitute mapping in
(* only ns change in an is_varsubst mapping -- matters with modalities *)
let unchanged =
if is_varsubst then
((* collect modal variables *)
let rec vsof vset f =
let optvs fvs f =
match f.fnode with
| Fvar (None,NoHook,v) -> Some (NameSet.add v fvs)
| Binder (_,n,f) -> let bvs = vsof NameSet.empty f in
Some (NameSet.union fvs (NameSet.remove n bvs))
| _ -> None
in
Formula.fold optvs vset f
in
let mvs f =
let optmvs fvs f =
match f.fnode with
| Bfr (_,_,bf) -> Some (vsof fvs bf)
| Univ (_,uf) -> Some (vsof fvs uf)
| Sofar (_,sf) -> Some (vsof fvs sf)
| Ouat (_,_,sf) -> Some (vsof fvs sf)
| Since (_,_,f1,f2) -> Some (vsof (vsof fvs f1) f2)
| Binder (_,n,f) -> let bvs = vsof NameSet.empty f in
Some (NameSet.union fvs (NameSet.remove n bvs))
| _ -> None
in
Formula.fold optmvs NameSet.empty f
in
let vars = mvs pre in
let unchanged = NameSet.diff vars (NameSet.of_list (List.map fstof2 mapping)) in
conjoin (List.map (fun v -> _recEqual (_recFvar None NoHook v)
(_recFvar None Hook v)
)
(NameSet.elements unchanged)
)
)
else _recTrue
in
let effect (loc,e) =
match loc with
| VarLoc v -> _recEqual (_recFname v) (sub e) (* sub e for register assignments *)
in
conjoin (sub pre
:: (if !Settings.sp_unchanged then unchanged else _recTrue)
:: List.map (decorate <.> effect) (List.combine locs es)
)
in
match assign with
| RbecomesE (r,e) -> sp_multiple false [r, old_name r] [VarLoc r] [e]
| LocbecomesEs ((* b, *) loces) -> let locs, es = List.split loces in
sp_multiple true (List.map (function VarLoc v -> v, old_name v
)
locs
)
locs
es
| RsbecomeLocs ((* b, *) rslocs) -> let rss, locs = List.split rslocs in
let rs = List.concat rss in
let rs' = List.map old_name rs in
let sub = sp_substitute (List.combine rs rs') in
conjoin
(sub pre ::
List.map (fun (rs,loc) ->
decorate (_recEqual (singleton_or_tuple (List.map _recFreg rs))
(_recFloc loc)
)
)
rslocs
)