-
Notifications
You must be signed in to change notification settings - Fork 0
/
tfs_exists2.v
447 lines (440 loc) · 19.3 KB
/
tfs_exists2.v
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
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
intros tfs h h' fs' tfsres WfP Tch Dtfs Red TRed.
destruct tfsres.
* (* Some from typed_red *)
destruct tfs as [| tfr ?].
** simpl in Red.
discriminate Red.
** destruct tfr.
destruct TFRfr.
destruct A.
*** (* A=Some j *)
destruct E; destruct Ctx;simpl in Red; auto_destr_discr Red.
****
destruct tfs as [| tfr ?]; try discriminate Red.
simpl FSofTFS in *.
simpl in Red.
destruct tfr.
simpl in Red.
simpl in TRed.
destruct l.
+ auto_destr_discr TRed.
finish_tfs_for_fs.
+ auto_destr_discr TRed.
destr_discr TRed.
auto_destr_discr TRed.
(* here starts one case where red really goes to Some...
[] [[l]]_Some j :: Ctx [[JFInvoke]]_None :: _ *)
(* exception propagates to method call *)
finish_tfs_for_fs.
**** simpl in TRed.
(* exception propagates through let *)
finish_tfs_for_fs.
**** simpl in TRed.
(* exception comes to try *)
destr_discr TRed.
*****
(* exception handled here *)
finish_tfs_for_fs.
*****
(* exception passes through (wrong) try *)
finish_tfs_for_fs.
*** (* A=None *)
Opaque Heap.find.
simpl in Red; auto_destr_discr Red; simpl in TRed; try finish_tfs_for_fs.
(* empty context *)
**** (* alloc *)
repeat destr_discr Red.
finish_tfs_for_fs.
**** (* method call *)
unfold getInvokeBody in *.
repeat destr_discr Red.
repeat destr_discr TRed.
finish_tfs_for_fs.
**** (* assign *)
repeat destr_discr Red; finish_tfs_for_fs.
**** (* method return *)
destr_discr TRed.
destruct t0.
simpl in *.
repeat destr_discr Red.
repeat destr_discr TRed.
finish_tfs_for_fs.
**** (* lookup *)
repeat destr_discr Red.
repeat destr_discr TRed.
finish_tfs_for_fs.
**** (* throw *)
destr_discr Red.
finish_tfs_for_fs.
* (* None from typed_red *)
unfold typed_red2 in TRed.
destruct tfs as [| tfr ?].
**
simpl in Red.
discriminate Red.
**
destruct tfr.
destruct TFRfr.
simpl in Red.
simpl in TRed.
generalize Dtfs;intros.
unfold DerivableTFS in Dtfs0.
destruct Dtfs0 as [IsTFS DerTFR].
generalize DerTFR;intros.
apply Forall_inv in DerTFR0.
unfold DerivableTFR in DerTFR0.
destruct DerTFR0 as (Fcls & MthdLkp & TpsCtx).
destruct A.
*** (* A = Some _ *)
destruct TpsCtx.
destruct H as [Eeq TpsCtx].
subst E.
unfold typesCtx in TpsCtx.
destruct Ctx.
****
simpl in TpsCtx.
destruct x; try discriminate Red; try discriminate TRed.
destruct tfs as [| tfr ?].
+ simpl in Red;discriminate Red.
+ simpl in Red.
destruct (TFRfr tfr) eqn:tfrfre.
destruct E;try discriminate Red.
destruct A; try discriminate Red.
generalize Dtfs; intro Wffs.
apply DerivableTFS_wfs in Wffs.
simpl in Wffs.
rewrite tfrfre in Wffs.
destruct v; try contradiction.
destruct l0;try contradiction.
generalize DerTFR;intros.
assert (Forall (DerivableTFR CC) (tfr::tfs)). {
clear -DerTFR0.
apply Forall_forall.
intros.
eapply Forall_forall in DerTFR0.
eauto 1.
eauto 2 using in_cons.
}
eapply Forall_inv in H.
destruct tfr.
simpl in H.
simpl in tfrfre.
subst TFRfr.
simpl in TRed.
destruct H as (Fcls1 & MthdLkp1 & TpsCtx1).
eapply typesCtx_typesCtxExt1 in TpsCtx1;eauto 2.
destruct TpsCtx1 as [Xi1 [Acid1]].
eapply typesCtxExt_types in H; eauto 1.
destruct Acid1.
destruct TFRAcid.
eapply inversion_Throw in TpsCtx; eauto 2.
destruct TpsCtx as [m' [C [D' [mu' [mname [cname [TpsVal [IsLeqIn TpsCtx]]]]]]]].
destruct l.
++ (* l=null *)
discriminate TRed.
++ (* l=non_null *)
eapply inversion_JFVal1_nonnull in TpsVal; eauto 2; try discriminate.
destruct TpsVal as [C'' [mu'' [LeqIsLs [Inn Tpsn0]]]].
eapply DerNU_first in Dtfs.
eapply In_find in Inn; eauto 2.
simpl in Inn.
rewrite Inn in TRed.
discriminate TRed.
****
destruct j0.
+ destruct x;try discriminate Red; try discriminate TRed.
+ destruct x;try discriminate Red; try discriminate TRed.
destruct (subtype_class_bool CC j C); discriminate TRed.
*** (* A = None *)
eapply typesCtx_typesCtxExt1 in TpsCtx;eauto 2.
destruct TpsCtx as [Xi1 [Acid1]].
destruct Ctx.
**** (* empty context *)
destruct E; try discriminate Red;
simpl in TRed;
try discriminate TRed.
+ (* JFNew normal *)
repeat destr_discr Red.
finish_tfs_for_fs.
+ (* JFIf normal *)
destruct v1;destruct v2; try discriminate Red.
destruct (Loc_dec l l0); discriminate TRed.
+ (* JFInvoke normal *)
destruct v; try destruct l;
try discriminate TRed;try discriminate Red.
unfold getInvokeBody in *.
unfold getClassName in *.
unfold type_correct_heap in Tch.
case_eq (Heap.find (elt:=Obj) n h);
[intros o Hf|intros Hf;rewrite Hf in *];
try discriminate Red.
destruct o.
rewrite Hf in *.
destruct (methodLookup CC j m ); try discriminate Red.
destruct (substList (map JFVar (params_of_md j0)) vs
(substExpr JFThis (JFLoc n) (body_of_md j0)));
try discriminate Red.
apply Tch in Hf.
destruct Hf as [ [? Fcls'] ?].
rewrite Fcls' in *.
discriminate TRed.
+ (* JFAssign normal *)
destruct vx; destruct j;try discriminate Red.
destruct l;destruct v; try discriminate TRed;
try discriminate Red.
destruct (Heap.find (elt:=Obj) n h);try discriminate Red.
destruct o;discriminate TRed.
+ (* JFVal1 normal *)
auto_destr_discr Red.
auto_destr_discr TRed.
++ simpl in Red.
discriminate Red.
++ simpl in Red.
destruct (TFRfr t0) eqn:TFRfreeq.
auto_destr_discr Red.
generalize Dtfs; intro Wffs.
apply DerivableTFS_wfs in Wffs.
destruct v eqn:veq; try destruct l0; try contradiction.
+++ simpl in Wffs.
rewrite TFRfreeq in Wffs.
contradiction.
+++ edestruct getClassName_forDTFS;
try eapply TFRfreeq; eauto 1.
{ simpl.
unfold DerivableTFS.
split; eauto 2 using ConsistentTFS_further.
eapply Forall_forall.
intros.
eapply Forall_forall.
eapply DerTFR.
eauto 2 using in_cons.
}
rewrite H0 in *.
edestruct methodLookup_forDTFS;
try eapply Ecefreeq; eauto 1.
rewrite H1 in *.
destruct (rettyp_of_md x0).
discriminate TRed.
+++ simpl in Wffs.
rewrite TFRfreeq in Wffs.
contradiction.
+ (* JFVal2 normal *)
destruct vx;try destruct j; try destruct l;try discriminate TRed;
try discriminate Red.
(* preparations *)
apply Forall_inv in DerTFR.
inversion DerTFR as (Fcls1 & MthdLkp1 & TpsCtx1).
edestruct typesCtx_typesCtxExt in TpsCtx1; eauto 1.
simpl in *.
subst.
apply typesCtxExt_types in H.
apply Inversion_JFVal2 in H; eauto 2.
destruct H as [C' [C'' [mu [mu' [fldlst [rep]]]]]].
destruct H as [Tps [IsLS [Flds [InFlds [IsLS' [NIsLS
[TpsInd LeqIsLS]]]]]]].
(* Heap reference is left *)
destruct (Heap.find (elt:=Obj) n h) eqn:Hpfnd;
try discriminate Red.
destruct o as [oo C].
generalize Hpfnd;intros.
eapply find_field_in_subclass in Hpfnd0; eauto 3.
++
destruct Hpfnd0.
rewrite H in *.
generalize Tch;intros.
eapply type_correct_heap_find_class in Tch0; eauto 1.
destruct Tch0.
eapply find_class_flds_aux in H1; eauto 2.
destruct H1.
replace (get_class_height CC C + 0) with (get_class_height CC C) in H1 by auto with zarith.
erewrite H1 in TRed.
edestruct type_correct_heap_find_field; eauto 2.
rewrite H2 in TRed;destruct x3;discriminate TRed.
++ eapply inversion_JFVal1_nonnull in Tps;eauto 2;try discriminate.
destruct Tps as [C0 [mu0 [LeqIsLS0 [Inn Tps]]]].
replace TFRGamma with (JaRedInvariants.TFRGamma {|
TFRcdecl := TFRcdecl;
TFRmdecl := TFRmdecl;
TFRXi := TFRXi;
TFRGamma := TFRGamma;
TFRfr := [] [[JFVal2 (JFVLoc (JFLoc n), j0) ]]_ None;
TFRAcid := TFRAcid |}) in Inn by (simpl;trivial).
eapply ConsistentTFR_subtyping in Hpfnd;
try eapply Inn; eauto 2 using DerivableTFS_ConsistentTFR.
inversion LeqIsLS0.
+++ injection H2;injection H3;intros;subst.
eapply subtrans; eauto 2.
+++ injection H2;injection H3;intros;subst.
eapply subtrans; eauto 2.
+ (* JFThrow normal *)
destruct v;try destruct l; try destruct (class h n);
try discriminate Red;try discriminate TRed.
**** (* non-empty context *)
destruct j.
+ destruct E;try discriminate TRed.
++ destruct (list_map_opt loc_of_val vs); try discriminate Red; try discriminate TRed.
destruct (alloc_init CC h cn l); try destruct p; try discriminate Red; try discriminate TRed.
++ destruct v1; try discriminate Red; try discriminate TRed.
destruct v2; try discriminate Red.
destruct (Loc_dec l l0); try discriminate TRed.
++ destruct v; try destruct l;
try discriminate TRed; try discriminate Red.
rewrite Red in TRed.
edestruct getClassName_forDTFS; simpl; eauto 1;simpl;eauto 1.
rewrite H0 in TRed.
edestruct getInvokeBody_Some; eauto 1.
destruct H1 as [hd2 [fs'eq heq]].
subst.
unfold getInvokeBody in Red.
destruct (getClassName h' n) in *; try discriminate Red.
injection H0;intros.
subst x0; clear H0.
destruct (methodLookup CC j m) eqn:MthdLkpj in *;
try discriminate Red.
edestruct methodLookup_find_class; try eapply MthdLkpj.
rewrite H0 in TRed.
discriminate TRed.
++ destruct vx;destruct j; try discriminate TRed; try discriminate Red.
destruct l; try discriminate TRed; try discriminate Red.
destruct v; try discriminate Red; try discriminate TRed.
destruct v; try discriminate Red; try discriminate TRed.
destruct (Heap.find (elt:=Obj) n h); try discriminate Red; try discriminate TRed.
destruct o; try discriminate TRed.
++ destruct v; try discriminate Red; try discriminate TRed.
++ (* JFVal2 normal *)
destruct vx;try destruct j; try destruct l;try discriminate TRed;
try discriminate Red.
(* preparations *)
apply Forall_inv in DerTFR.
inversion DerTFR as (Fcls1 & MthdLkp1 & TpsCtx1).
edestruct typesCtx_typesCtxExt in TpsCtx1; eauto 1.
simpl in *.
subst.
apply typesCtxExt_types in H.
apply Inversion_JFVal2 in H; eauto 2.
destruct H as [C' [C'' [mu [mu' [fldlst [rep]]]]]].
destruct H as [Tps [IsLS [Flds [InFlds [IsLS' [NIsLS
[TpsInd LeqIsLS]]]]]]].
(* Heap reference is left *)
destruct (Heap.find (elt:=Obj) n h) eqn:Hpfnd;
try discriminate Red.
destruct o as [oo Ci].
generalize Hpfnd;intros.
eapply find_field_in_subclass in Hpfnd0; eauto 3.
+++
destruct Hpfnd0.
rewrite H in *.
generalize Tch;intros.
eapply type_correct_heap_find_class in Tch0; eauto 1.
destruct Tch0.
eapply find_class_flds_aux in H1; eauto 2.
destruct H1.
replace (get_class_height CC Ci + 0) with (get_class_height CC Ci) in H1 by
auto with zarith.
erewrite H1 in TRed.
edestruct type_correct_heap_find_field; eauto 2.
rewrite H2 in TRed; destruct x4; discriminate TRed.
+++
eapply inversion_JFVal1_nonnull in Tps; try congruence; eauto 2.
destruct Tps as [C''' [mu''' [LeqIsLSC'' [Inn Tps]]]].
inversion LeqIsLSC''.
++++
injection H2;intros.
injection H3;intros.
subst.
eapply subtrans;try eapply H4;eauto 2.
eapply ConsistentTFR_subtyping; eauto 2 using DerivableTFS_ConsistentTFR.
++++
injection H2;intros.
injection H3;intros.
subst.
eapply subtrans;try eapply H4;eauto 2.
eapply ConsistentTFR_subtyping; eauto 2 using DerivableTFS_ConsistentTFR.
++ destruct v; try discriminate Red.
destruct l; try discriminate TRed.
destruct (class h n);try discriminate Red;try discriminate TRed.
+ destruct E;try discriminate TRed.
++ destruct (list_map_opt loc_of_val vs);try discriminate TRed; try discriminate Red.
destruct ( alloc_init CC h cn l);try discriminate TRed; try discriminate Red.
destruct p;try discriminate TRed; try discriminate Red.
++ destruct v1; try discriminate Red; try discriminate TRed.
destruct v2; try discriminate Red.
destruct (Loc_dec l l0); try discriminate TRed.
++ (* JFInvoke *)
destruct v; try destruct l;
try discriminate TRed;try discriminate Red.
edestruct getInvokeBody_Some_ClassName; eauto 1.
rewrite H0 in TRed.
rewrite <- H0 in TRed.
rewrite Red in TRed.
edestruct getInvokeBody_Some;eauto 1.
destruct H1 as [x2 [fs'eq heq]].
subst.
edestruct getInvokeBody_Some_find_class. {
rewrite H0 in Red. eauto 1.
}
edestruct getInvokeBody_Some_methodLookup. {
rewrite H0 in Red. eauto 1.
}
rewrite H2 in TRed.
rewrite H1 in TRed.
discriminate TRed.
++ destruct vx;destruct j; try discriminate TRed; try discriminate Red.
destruct l; try discriminate TRed; try discriminate Red.
destruct v; try discriminate Red; try discriminate TRed.
destruct v; try discriminate Red; try discriminate TRed.
destruct (Heap.find (elt:=Obj) n h); try discriminate Red; try discriminate TRed.
destruct o; try discriminate TRed.
++ destruct v; try discriminate Red; try discriminate TRed.
++ (* JFVal2 *)
destruct vx;try destruct j; try destruct l;try discriminate TRed;
try discriminate Red.
(* preparations *)
apply Forall_inv in DerTFR.
inversion DerTFR as (Fcls1 & MthdLkp1 & TpsCtx1).
edestruct typesCtx_typesCtxExt in TpsCtx1; eauto 1.
simpl in *.
subst.
apply typesCtxExt_types in H.
apply Inversion_JFVal2 in H; try eauto 2.
destruct H as [C' [C'' [mu' [mu'' [fldlst [rep]]]]]].
destruct H as [Tps [IsLS [Flds [InFlds [IsLS' [NIsLS
[TpsInd LeqIsLS]]]]]]].
(* Heap reference is left *)
destruct (Heap.find (elt:=Obj) n h) eqn:Hpfnd;
try discriminate Red.
destruct o as [oo Ci].
generalize Hpfnd;intros.
eapply find_field_in_subclass in Hpfnd0; eauto 3.
+++
destruct Hpfnd0.
rewrite H in *.
generalize Tch;intros.
eapply type_correct_heap_find_class in Tch0; eauto 2.
destruct Tch0.
eapply find_class_flds_aux in H1; eauto 2.
destruct H1.
replace (get_class_height CC Ci + 0) with (get_class_height CC Ci) in H1
by auto with zarith.
erewrite H1 in TRed.
edestruct type_correct_heap_find_field; eauto 1.
rewrite H2 in TRed;destruct x4;discriminate TRed.
+++
eapply inversion_JFVal1_nonnull in Tps;try congruence;eauto 2.
destruct Tps as [C''' [mu''' [LeqIsLSC'' [Inn Tps]]]].
inversion LeqIsLSC''.
++++
injection H2;intros.
injection H3;intros.
subst.
eapply subtrans;try eapply H4;eauto 2.
eapply ConsistentTFR_subtyping; eauto 2 using DerivableTFS_ConsistentTFR.
++++
injection H2; intros.
injection H3;intros.
subst.
eapply subtrans;try eapply H4;eauto 2.
eapply ConsistentTFR_subtyping; eauto 2 using DerivableTFS_ConsistentTFR.
++ destruct v; try discriminate Red; try discriminate TRed.
destruct l; try discriminate TRed; try discriminate Red.
destruct (class h n);try discriminate TRed; try discriminate Red.