-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathDEX_ImplemProgramWithMap.v
1157 lines (995 loc) · 45.2 KB
/
DEX_ImplemProgramWithMap.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
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(** * Bicolano: Program syntax (interface implementation with maps) *)
(* Hendra : - Modified to suit DEX program.
- DEX has different instructions list from JVM.
- Also trim the system to contain only Arithmetic *)
Require Export DEX_Program.
Require Export ImplemSubClass.
Require Export Relation_Operators.
Require Export Lib.
Require ImplemSubClass.
Module MapP <: MAP with Definition key := positive := BinMap.
Module MapN <: MAP with Definition key := N := BinNatMap.
Module DEX_Make <: DEX_PROGRAM.
Definition eq_dec (A:Set) := forall x y:A, x=y \/~x=y.
Definition DEX_Reg := N.
Definition Reg_eq := Neq.
Lemma Reg_eq_dec : eq_dec DEX_Reg.
Proof.
intros x1 x2;assert (UU:= Neq_spec x1 x2);destruct (Neq x1 x2);auto.
Qed.
Definition Reg_toN : DEX_Reg -> nat := nat_of_N.
Definition N_toReg : nat -> DEX_Reg := N_of_nat.
Lemma Reg_toN_bij1 : forall v, N_toReg (Reg_toN v) = v.
Proof. exact nat_of_N_bij2. Qed.
Lemma Reg_toN_bij2 : forall n, Reg_toN (N_toReg n) = n.
Proof. exact nat_of_N_bij1. Qed.
Definition DEX_PC : Set := N.
Definition DEX_PC_eq := Neq.
Definition DEX_PC_eq_spec := Neq_spec.
Lemma DEX_PC_eq_dec : eq_dec DEX_PC.
Proof. exact Reg_eq_dec.
(*intros x1 x2;assert (UU:= Neq_spec x1 x2);destruct (Neq x1 x2);auto.*)
Qed.
Definition DEX_PackageName : Set := positive.
Definition DEX_ShortClassName : Set := positive.
Definition DEX_ShortMethodName : Set := positive.
Definition DEX_ShortFieldName : Set := positive.
Definition DEX_ClassName := DEX_PackageName * DEX_ShortClassName.
Definition DEX_InterfaceName := DEX_PackageName * DEX_ShortClassName.
Definition DEX_MethodName := DEX_ClassName * DEX_ShortMethodName.
Definition DEX_FieldName := DEX_ClassName * DEX_ShortFieldName.
Definition eqClassName : DEX_ClassName -> DEX_ClassName -> bool := prod_eq _ Peq _ Peq.
Lemma eqClassName_spec : forall x y, if eqClassName x y then x = y else x <> y.
Proof. exact (prod_eq_spec _ Peq Peq_spec _ Peq Peq_spec). Qed.
Lemma ClassName_eq_dec : eq_dec DEX_ClassName.
Proof. exact (Aeq_dec _ eqClassName eqClassName_spec). Qed.
Definition eqInterfaceName : DEX_InterfaceName ->DEX_InterfaceName -> bool :=
prod_eq _ Peq _ Peq.
Lemma eqInterfaceName_spec : forall x y, if eqInterfaceName x y then x = y else x <> y.
Proof. exact (prod_eq_spec _ Peq Peq_spec _ Peq Peq_spec). Qed.
Lemma InterfaceName_eq_dec : eq_dec DEX_InterfaceName.
Proof. exact (Aeq_dec _ eqClassName eqClassName_spec). Qed.
Definition eqMethodName : DEX_MethodName -> DEX_MethodName -> bool :=
prod_eq _ eqClassName _ Peq.
Lemma eqMethodName_spec : forall x y, if eqMethodName x y then x = y else x <> y.
Proof. exact (prod_eq_spec _ eqClassName eqClassName_spec _ Peq Peq_spec). Qed.
Lemma MethodName_eq_dec : eq_dec DEX_MethodName.
Proof. exact (Aeq_dec _ eqMethodName eqMethodName_spec). Qed.
Definition eqFieldName : DEX_FieldName -> DEX_FieldName -> bool :=
prod_eq _ eqClassName _ Peq.
Lemma eqFieldName_spec : forall x y, if eqFieldName x y then x = y else x <> y.
Proof. exact (prod_eq_spec _ eqClassName eqClassName_spec _ Peq Peq_spec). Qed.
Lemma FieldName_eq_dec : eq_dec DEX_FieldName.
Proof. exact (Aeq_dec _ eqFieldName eqFieldName_spec). Qed.
Open Scope positive_scope.
(* IMPORTANT CONSTANT CONVENTIONS FOR PARSER !! *)
Definition javaLang : DEX_PackageName := 1.
Definition EmptyPackageName : DEX_PackageName := 2.
Definition object : DEX_ShortClassName := 1.
(* DEX
Definition NullPointerException : ShortClassName := 2.
Definition ArrayIndexOutOfBoundsException : ShortClassName := 3.
Definition ArrayStoreException : ShortClassName := 4.
Definition NegativeArraySizeException : ShortClassName := 5.
Definition ClassCastException : ShortClassName := 6.
Definition ArithmeticException : ShortClassName := 7.
Definition throwable : ShortClassName := 8.
*)
Inductive DEX_Visibility : Set :=
Package | Protected | Private | Public.
Definition eqVisibility x y :=
match x, y with
| Package, Package => true
| Protected, Protected => true
| Private, Private => true
| Public, Public => true
| _, _ => false
end.
Lemma eqVisibility_spec : forall x y, if eqVisibility x y then x = y else x <> y.
Proof. destruct x;destruct y;simpl;trivial;intro; discriminate. Qed.
Lemma Visibility_eq_dec : eq_dec DEX_Visibility.
Proof. exact (Aeq_dec _ eqVisibility eqVisibility_spec). Qed.
Inductive DEX_type : Set :=
(*Hendra 10082016 - Only concerns DVM_I | DEX_ReferenceType (rt : DEX_refType) *)
| DEX_PrimitiveType (pt: DEX_primitiveType)
(* Hendra 10082016 - Only concerns DVM_I with DEX_refType :Set :=
| DEX_ArrayType (typ:DEX_type)
| DEX_ClassType (ct:DEX_ClassName)
| DEX_InterfaceType (it:DEX_InterfaceName) *)
with DEX_primitiveType : Set :=
| DEX_BOOLEAN | DEX_BYTE | DEX_SHORT | DEX_INT.
Scheme type_strong_rec := Induction for DEX_type Sort Set
(*with refType_strong_rec := Induction for DEX_refType Sort Set*).
Scheme type_strong_ind := Induction for DEX_type Sort Prop
(*with refType_strong_ind := Induction for DEX_refType Sort Prop*).
Definition eq_primitiveType x y :=
match x, y with
| DEX_BOOLEAN, DEX_BOOLEAN => true
| DEX_BYTE, DEX_BYTE => true
| DEX_SHORT, DEX_SHORT => true
| DEX_INT, DEX_INT => true
| _, _ => false
end.
Lemma eq_primitiveType_spec : forall x y, if eq_primitiveType x y then x = y else x <> y.
Proof.
destruct x;destruct y;simpl;trivial; intro;discriminate.
Qed.
Lemma primitiveType_dec : eq_dec DEX_primitiveType.
Proof. exact (Aeq_dec _ eq_primitiveType eq_primitiveType_spec). Qed.
Fixpoint eq_type (t1 t2:DEX_type) {struct t1} : bool :=
match t1, t2 with
(* Hendra 10082016 - Only concerns DVM_I | DEX_ReferenceType rt1, DEX_ReferenceType rt2 => eq_reftype rt1 rt2 *)
| DEX_PrimitiveType pt1, DEX_PrimitiveType pt2 => eq_primitiveType pt1 pt2
(*| _, _ => false*)
end
(* Hendra 10082016 - Only concerns DVM_I with eq_reftype (rt1 rt2: DEX_refType) {struct rt1} : bool :=
match rt1, rt2 with
| DEX_ArrayType t1, DEX_ArrayType t2 => eq_type t1 t2
| DEX_ClassType cn1, DEX_ClassType cn2 => eqClassName cn1 cn2
| DEX_InterfaceType in1, DEX_InterfaceType in2 => eqInterfaceName in1 in2
|_, _ => false
end*).
Lemma eq_type_spec : forall t1 t2, if eq_type t1 t2 then t1 = t2 else t1 <> t2.
Proof.
induction t1,t2.
simpl.
assert (UU := eq_primitiveType_spec pt pt0).
destruct eq_primitiveType.
subst; trivial.
intro H. injection H. auto.
(*
induction t1 using type_strong_ind with
(P0:=
fun rt1 => forall rt2, if eq_reftype rt1 rt2 then rt1 = rt2 else rt1 <> rt2);intros.
destruct t2;simpl;try (intro;discriminate;fail).
assert (UU:=IHt1 rt0);destruct (eq_reftype rt rt0);subst;trivial.
intro H;injection H;auto.
destruct t2;simpl;try (intro;discriminate;fail).
assert (UU := eq_primitiveType_spec pt pt0);destruct (eq_primitiveType pt pt0);subst;trivial.
intro H;injection H;auto.
destruct rt2;simpl;try (intro H;discriminate H).
assert (UU:=IHt1 typ);destruct (eq_type t1 typ);subst;trivial.
intro H;injection H;auto.
destruct rt2;simpl;intros;try (intro;discriminate;fail).
assert (UU := eqClassName_spec ct ct0);destruct (eqClassName ct ct0);subst;trivial.
intro H;injection H;auto.
destruct rt2;simpl;intros;try (intro;discriminate;fail).
assert (UU := eqInterfaceName_spec it it0);destruct (eqInterfaceName it it0);subst;trivial.
intro H;injection H;auto.
*)
Qed.
Lemma type_dec : eq_dec DEX_type.
Proof. exact (Aeq_dec _ eq_type eq_type_spec). Qed.
Inductive DEX_CompInt : Set :=
DEX_EqInt | DEX_NeInt | DEX_LtInt | DEX_LeInt | DEX_GtInt | DEX_GeInt.
(* DEX Inductive CompRef : Set := EqRef | NeRef. *)
Inductive DEX_BinopInt : Set :=
DEX_AddInt | DEX_AndInt | DEX_DivInt | DEX_MulInt | DEX_OrInt | DEX_RemInt
| DEX_ShlInt | DEX_ShrInt | DEX_SubInt | DEX_UshrInt | DEX_XorInt.
Module Type DEX_OFFSET_TYPE.
Parameter t : Set.
Parameter jump : DEX_PC -> t -> DEX_PC.
End DEX_OFFSET_TYPE.
Module DEX_OFFSET <: DEX_OFFSET_TYPE.
Definition t := Z.
Definition jump (pc:DEX_PC) (ofs:t) : DEX_PC := Zabs_N (Zplus (Z_of_N pc) ofs).
End DEX_OFFSET.
Module DEX_FIELDSIGNATURE.
Record t :Set := {
name : DEX_ShortFieldName;
type : DEX_type
}.
Definition eq_t (x y : t) :=
let (n1,t1) := x in
let (n2,t2) := y in
if Peq n1 n2 then eq_type t1 t2 else false.
Lemma eq_t_spec : forall x y, if eq_t x y then x = y else x <> y.
Proof.
intros (n1,t1) (n2,t2);simpl;generalize (Peq_spec n1 n2);
destruct (Peq n1 n2);intros.
generalize (eq_type_spec t1 t2);destruct (eq_type t1 t2);intros;subst;trivial.
intro H;injection H;auto.
intro H1;injection H1;auto.
Qed.
Lemma eq_dec : eq_dec t.
Proof. exact (Aeq_dec _ eq_t eq_t_spec). Qed.
End DEX_FIELDSIGNATURE.
Definition DEX_ShortFieldSignature := DEX_FIELDSIGNATURE.t.
Definition DEX_FieldSignature := (DEX_ClassName * DEX_FIELDSIGNATURE.t)%type.
Module Type DEX_FIELDSIGNATURE_TYPE.
Parameter name : DEX_ShortFieldSignature -> DEX_ShortFieldName.
Parameter type : DEX_ShortFieldSignature -> DEX_type.
Parameter eq_dec : forall f1 f2:DEX_ShortFieldSignature, f1=f2 \/ ~f1=f2.
End DEX_FIELDSIGNATURE_TYPE.
Module DEX_METHODSIGNATURE.
Record t :Set := {
name : DEX_ShortMethodName;
parameters : list DEX_type;
result : option DEX_type
}.
Definition eq_t (x y : t) :=
let (n1,p1,r1) := x in
let (n2,p2,r2) := y in
if Peq n1 n2 then
if list_eq _ eq_type p1 p2 then opt_eq _ eq_type r1 r2
else false
else false.
Lemma eq_t_spec : forall x y, if eq_t x y then x = y else x <> y.
Proof.
intros (n1,p1,r1) (n2,p2,r2);simpl;generalize (Peq_spec n1 n2);
destruct (Peq n1 n2);intros.
generalize (list_eq_spec _ eq_type eq_type_spec p1 p2);
destruct (list_eq _ eq_type p1 p2);intros.
generalize (opt_eq_spec _ eq_type eq_type_spec r1 r2);
destruct (opt_eq _ eq_type r1 r2);intros. subst;trivial.
intro UU;injection UU;auto.
intro UU;injection UU;auto.
intro H1;injection H1;auto.
Qed.
Lemma eq_dec : eq_dec t.
Proof. exact (Aeq_dec _ eq_t eq_t_spec). Qed.
End DEX_METHODSIGNATURE.
Definition DEX_ShortMethodSignature := DEX_METHODSIGNATURE.t.
Definition DEX_MethodSignature := (DEX_ClassName*DEX_METHODSIGNATURE.t)%type.
Module Type DEX_METHODSIGNATURE_TYPE.
Parameter name : DEX_ShortMethodSignature -> DEX_ShortMethodName.
Parameter parameters : DEX_ShortMethodSignature -> list DEX_type.
Parameter result : DEX_ShortMethodSignature -> option DEX_type.
Parameter eq_dec : forall mid1 mid2:DEX_ShortMethodSignature, mid1=mid2 \/~mid1=mid2.
End DEX_METHODSIGNATURE_TYPE.
(* Hendra 10082016 - Only concerns DVM_I
Inductive DEX_ArrayKind : Set :=
| DEX_Aarray
| DEX_Iarray
| DEX_Barray
| DEX_Sarray.
*)
Inductive DEX_ValKind : Set :=
(*| DEX_Aval*)
| DEX_Ival.
Inductive DEX_Instruction : Set :=
| DEX_Nop
| DEX_Move (k:DEX_ValKind) (rt:DEX_Reg) (rs:DEX_Reg)
(* DEX Method
| DEX_MoveResult (k:DEX_ValKind) (rt:DEX_Reg)
*)
| DEX_Return
| DEX_VReturn (k:DEX_ValKind) (rt:DEX_Reg)
| DEX_Const (k:DEX_ValKind) (rt:DEX_Reg) (v:Z)
(* DEX Objects
| DEX_InstanceOf (rt:DEX_Reg) (r:DEX_Reg) (t:DEX_refType)
| DEX_ArrayLength (rt:DEX_Reg) (rs:DEX_Reg)
| DEX_New (rt:DEX_Reg) (t:DEX_refType)
| DEX_NewArray (rt:DEX_Reg) (rl:DEX_Reg) (t:DEX_type)
*)
| DEX_Goto (o:DEX_OFFSET.t)
(*| DEX_PackedSwitch (rt:DEX_Reg) (firstKey:Z) (size:nat) (l:list DEX_OFFSET.t)
| DEX_SparseSwitch (rt:DEX_Reg) (size:nat) (l:list (Z * DEX_OFFSET.t))*)
| DEX_Ifcmp (cmp:DEX_CompInt) (ra:DEX_Reg) (rb:DEX_Reg) (o:DEX_OFFSET.t)
| DEX_Ifz (cmp:DEX_CompInt) (r:DEX_Reg) (o:DEX_OFFSET.t)
(* DEX Objects
| DEX_Aget (k:DEX_ArrayKind) (rt:DEX_Reg) (ra:DEX_Reg) (ri:DEX_Reg)
| DEX_Aput (k:DEX_ArrayKind) (rs:DEX_Reg) (ra:DEX_Reg) (ri:DEX_Reg)
| DEX_Iget (k:DEX_ValKind) (rt:DEX_Reg) (ro:DEX_Reg) (f:DEX_FieldSignature)
| DEX_Iput (k:DEX_ValKind) (rs:DEX_Reg) (ro:DEX_Reg) (f:DEX_FieldSignature)
*)
(* | Sget (k:ValKind) (rt:Var) (f:FieldSignature)
| Sput (k:ValKind) (rs:Var) (f:FieldSignature) *)
(* DEX Method
| DEX_Invokevirtual (m:DEX_MethodSignature) (n:Z) (p:list DEX_Reg)
| DEX_Invokesuper (m:DEX_MethodSignature) (n:Z) (p:list DEX_Reg)
| DEX_Invokedirect (m:DEX_MethodSignature) (n:Z) (p:list DEX_Reg)
| DEX_Invokestatic (m:DEX_MethodSignature) (n:Z) (p:list DEX_Reg)
| DEX_Invokeinterface (m:DEX_MethodSignature) (n:Z) (p:list DEX_Reg)
*)
| DEX_Ineg (rt:DEX_Reg) (rs:DEX_Reg)
| DEX_Inot (rt:DEX_Reg) (rs:DEX_Reg)
| DEX_I2b (rt:DEX_Reg) (rs:DEX_Reg)
| DEX_I2s (rt:DEX_Reg) (rs:DEX_Reg)
| DEX_Ibinop (op:DEX_BinopInt) (rt:DEX_Reg) (ra:DEX_Reg) (rb:DEX_Reg)
| DEX_IbinopConst (op:DEX_BinopInt) (rt:DEX_Reg) (r:DEX_Reg) (v:Z)
.
Module DEX_FIELD.
Inductive value : Set :=
| Int (v:Z)
| NULL
| UNDEF.
Definition eq_value x y :=
match x, y with
| Int z1, Int z2 => Zeq_bool z1 z2
| NULL, NULL => true
| UNDEF, UNDEF => true
| _, _ => false
end.
Lemma eq_value_spec : forall x y, if eq_value x y then x = y else x <> y.
Proof.
destruct x;destruct y;intros;simpl;trivial;try (intro;discriminate;fail).
generalize (Zeq_spec v v0);destruct (Zeq_bool v v0);intros. subst;trivial.
intro H1;injection H1;auto.
Qed.
Record t : Set := {
signature : DEX_ShortFieldSignature;
isFinal : bool;
isStatic : bool;
visibility : DEX_Visibility;
initValue : value
}.
Definition eq_t (x y:t) :=
let (s1,f1,st1,v1,val1) := x in
let (s2,f2,st2,v2,val2) := y in
if DEX_FIELDSIGNATURE.eq_t s1 s2 then
if bool_eq f1 f2 then
if bool_eq st1 st2 then
if eqVisibility v1 v2 then eq_value val1 val2
else false
else false
else false
else false.
Lemma eq_t_spec : forall x y, if eq_t x y then x = y else x <> y.
Proof with try (intro UU;injection UU;auto;fail).
intros (s1,f1,st1,v1,val1)(s2,f2,st2,v2,val2);simpl.
generalize (DEX_FIELDSIGNATURE.eq_t_spec s1 s2);destruct (DEX_FIELDSIGNATURE.eq_t s1 s2);intros...
generalize (bool_eq_spec f1 f2);destruct (bool_eq f1 f2);intros...
generalize (bool_eq_spec st1 st2);destruct (bool_eq st1 st2);intros...
generalize (eqVisibility_spec v1 v2);destruct (eqVisibility v1 v2);intros...
generalize (eq_value_spec val1 val2);destruct (eq_value val1 val2);intros...
subst;trivial.
Qed.
Lemma eq_dec : eq_dec t.
Proof. exact (Aeq_dec _ eq_t eq_t_spec). Qed.
End DEX_FIELD.
Definition DEX_Field := DEX_FIELD.t.
Module Type DEX_FIELD_TYPE.
Parameter signature : DEX_Field -> DEX_ShortFieldSignature.
Parameter isFinal : DEX_Field -> bool.
Parameter isStatic : DEX_Field -> bool.
Parameter visibility : DEX_Field -> DEX_Visibility.
Inductive value : Set :=
| Int (v:Z)
| NULL
| UNDEF.
Parameter initValue : DEX_Field -> value.
End DEX_FIELD_TYPE.
(*
Module EXCEPTIONHANDLER.
Record t : Set := {
catchType : option ClassName;
begin : PC;
end_e : PC;
handler : PC
}.
Definition eq_t (x y:t) :=
let (c1,b1,e1,h1) := x in
let (c2,b2,e2,h2) := y in
if opt_eq _ eqClassName c1 c2 then
if Neq b1 b2 then
if Neq e1 e2 then Neq h1 h2
else false
else false
else false.
Lemma eq_t_spec : forall x y, if eq_t x y then x = y else x <> y.
Proof with try (intro UU;injection UU;auto;fail).
intros (c1,b1,e1,h1)(c2,b2,e2,h2);simpl.
generalize (opt_eq_spec _ eqClassName eqClassName_spec c1 c2);
destruct (opt_eq ClassName eqClassName c1 c2);intros ...
generalize (Neq_spec b1 b2);destruct (Neq b1 b2);intros...
generalize (Neq_spec e1 e2);destruct (Neq e1 e2);intros ...
generalize (Neq_spec h1 h2);destruct (Neq h1 h2);intros ...
subst;trivial.
Qed.
(* TODO : check correctness of isPCinRange *)
Definition isPCinRange (ex:t) (i:PC) : bool :=
let (_,b,e,_) := ex in
match Ncompare b i with
| Gt => false
| _ =>
match Ncompare i e with
| Gt => false
| _ => true
end
end.
End EXCEPTIONHANDLER.
Definition ExceptionHandler := EXCEPTIONHANDLER.t.
Module Type EXCEPTIONHANDLER_TYPE.
Parameter catchType : ExceptionHandler -> option ClassName.
Parameter isPCinRange : ExceptionHandler -> PC -> bool.
Parameter handler : ExceptionHandler -> PC.
End EXCEPTIONHANDLER_TYPE.
*)
Module DEX_BYTECODEMETHOD.
Record t : Type := {
firstAddress : DEX_PC;
instr : MapN.t (DEX_Instruction*(option DEX_PC*list DEX_ClassName));
(*exceptionHandlers : list ExceptionHandler;*)
max_locals : nat;
max_operand_stack_size : nat;
(* DEX type system locR *)
locR : list DEX_Reg;
regs : list DEX_Reg;
noDup_regs : NoDup regs
}.
Definition instructionAt (bm:t) (pc:DEX_PC) : option DEX_Instruction :=
match MapN.get _ bm.(instr) pc with
|Some p => Some (fst p)
|None => None
end.
Definition nextAddress (bm:t) (pc:DEX_PC) : option DEX_PC :=
match MapN.get _ bm.(instr) pc with
| Some p => fst (snd p)
| None => None
end.
Definition DefinedInstruction (bm:t) (pc:DEX_PC) : Prop :=
exists i, instructionAt bm pc = Some i.
(*
Definition throwableAt (bm:t) (pc:PC) : list ClassName :=
match MapN.get _ bm.(instr) pc with
| Some p => snd (snd p)
| None => nil
end.
*)
End DEX_BYTECODEMETHOD.
Definition DEX_BytecodeMethod := DEX_BYTECODEMETHOD.t.
Module Type DEX_BYTECODEMETHOD_TYPE.
Parameter firstAddress : DEX_BytecodeMethod -> DEX_PC.
Parameter nextAddress : DEX_BytecodeMethod -> DEX_PC -> option DEX_PC.
Parameter instructionAt : DEX_BytecodeMethod -> DEX_PC -> option DEX_Instruction.
(*Parameter exceptionHandlers : BytecodeMethod -> list ExceptionHandler.*)
Parameter max_locals : DEX_BytecodeMethod -> nat.
Parameter max_operand_stack_size : DEX_BytecodeMethod -> nat.
(* DEX type system locR *)
Parameter locR : DEX_BytecodeMethod -> list DEX_Reg.
Parameter regs : DEX_BytecodeMethod -> list DEX_Reg.
Parameter noDup_regs : forall bm, NoDup (regs (bm)).
Definition DefinedInstruction (bm:DEX_BytecodeMethod) (pc:DEX_PC) : Prop :=
exists i, instructionAt bm pc = Some i.
End DEX_BYTECODEMETHOD_TYPE.
Module DEX_FieldProj.
Definition element:=DEX_Field.
Definition key:=positive.
Definition proj (f:element) := f.(DEX_FIELD.signature).(DEX_FIELDSIGNATURE.name).
End DEX_FieldProj.
Module DEX_MapField := MapProj DEX_FieldProj.
Module DEX_ShortMethodSignatureHash <: HASH_TYPE.
Definition t : Set := DEX_ShortMethodSignature.
Definition eq_t := DEX_METHODSIGNATURE.eq_t.
Definition eq_t_spec := DEX_METHODSIGNATURE.eq_t_spec.
Definition eq_dec := DEX_METHODSIGNATURE.eq_dec.
Definition key := DEX_ShortMethodName.
Definition hash := DEX_METHODSIGNATURE.name.
End DEX_ShortMethodSignatureHash.
Module DEX_MapMethSign_Base :=
MapHash_Base DEX_ShortMethodSignatureHash MapP.
Module DEX_MapShortMethSign <: MAP with Definition key := DEX_ShortMethodSignature :=
Map_Of_MapBase DEX_MapMethSign_Base.
Module DEX_METHOD.
Record t : Type := {
signature : DEX_ShortMethodSignature;
body : option DEX_BytecodeMethod;
isFinal : bool;
isStatic : bool;
isNative : bool;
visibility : DEX_Visibility
}.
Definition isAbstract (m : t) : bool :=
match body m with
None => true
| Some _ => false
end.
Definition valid_reg (m:t) (x:DEX_Reg) : Prop :=
forall bm, body m = Some bm ->
((Reg_toN x) <= (DEX_BYTECODEMETHOD.max_locals bm))%nat.
(* DEX
Definition valid_stack_size (m:t) (length:nat) : Prop :=
forall bm, body m = Some bm ->
(length <= (DEX_BYTECODEMETHOD.max_operand_stack_size bm))%nat.
*)
(* DEX type system locR *)
Definition within_locR (m:t) (x:DEX_Reg) : Prop :=
forall bm, body m = Some bm -> In x (DEX_BYTECODEMETHOD.locR bm).
(* ((Reg_toN x) <= (DEX_BYTECODEMETHOD.locR bm))%nat. *)
End DEX_METHOD.
Definition DEX_Method := DEX_METHOD.t.
Module Type DEX_METHOD_TYPE.
Parameter signature : DEX_Method -> DEX_ShortMethodSignature.
Parameter body : DEX_Method -> option DEX_BytecodeMethod.
Parameter isFinal : DEX_Method -> bool.
Parameter isStatic : DEX_Method -> bool.
Parameter isNative : DEX_Method -> bool.
Parameter visibility : DEX_Method -> DEX_Visibility.
Definition isAbstract (m : DEX_Method) : bool :=
match body m with
None => true
| Some _ => false
end.
Definition valid_reg (m:DEX_Method) (x:DEX_Reg) : Prop :=
forall bm, body m = Some bm ->
((Reg_toN x) <= (DEX_BYTECODEMETHOD.max_locals bm))%nat.
(* DEX
Definition valid_stack_size (m:Method) (length:nat) : Prop :=
forall bm, body m = Some bm ->
(length <= (DEX_BYTECODEMETHOD.max_operand_stack_size bm))%nat.
*)
(* DEX type system locR *)
Definition within_locR (m:DEX_Method) (x:DEX_Reg) : Prop :=
forall bm, body m = Some bm -> In x (DEX_BYTECODEMETHOD.locR bm).
(* ((Reg_toN x) <= (DEX_BYTECODEMETHOD.locR bm))%nat. *)
End DEX_METHOD_TYPE.
Module DEX_CLASS .
Record t : Type := {
name : DEX_ClassName;
superClass : option DEX_ClassName;
superInterfaces : list DEX_InterfaceName;
fields : DEX_MapField.t;
methods : DEX_MapShortMethSign.t DEX_Method;
isFinal : bool;
isPublic : bool;
isAbstract : bool
}.
Definition field (c:t) (f:DEX_ShortFieldName):option DEX_Field := DEX_MapField.get c.(fields) f.
Lemma field_shortname_prop : forall cl s f,
field cl s = Some f -> s = DEX_FIELDSIGNATURE.name (DEX_FIELD.signature f).
Proof.
unfold field;intros cl s f H.
assert (UU:= DEX_MapField.get_proj _ _ _ H);subst;trivial.
Qed.
Definition definedFields (c:DEX_CLASS.t) : list DEX_FIELD.t :=
DEX_MapField.elements (DEX_CLASS.fields c).
Lemma in_definedFields_field_some : forall (c:DEX_CLASS.t) (f:DEX_FIELD.t),
In f (definedFields c) ->
DEX_CLASS.field c (DEX_FIELDSIGNATURE.name (DEX_FIELD.signature f)) = Some f.
Proof.
intros c; apply (DEX_MapField.in_elements_get_some (DEX_CLASS.fields c)).
Qed.
Lemma field_some_in_definedFields : forall (c:DEX_CLASS.t) (f:DEX_FIELD.t) (sfs:DEX_ShortFieldName),
DEX_CLASS.field c sfs = Some f-> In f (definedFields c).
Proof.
unfold definedFields; intros.
apply DEX_MapField.get_some_in_elements with sfs; auto.
Qed.
Definition method (c:t) (msig:DEX_ShortMethodSignature) : option DEX_Method :=
match DEX_MapShortMethSign.get _ c.(methods) msig with
| Some m =>
if DEX_METHODSIGNATURE.eq_t msig m.(DEX_METHOD.signature) then Some m
else None
| None => None
end.
Lemma method_signature_prop : forall cl mid m,
method cl mid = Some m -> mid = DEX_METHOD.signature m.
Proof.
unfold method; intros p cl mid.
destruct DEX_MapShortMethSign.get;try (intros;discriminate).
generalize (DEX_METHODSIGNATURE.eq_t_spec cl (DEX_METHOD.signature d));
destruct (DEX_METHODSIGNATURE.eq_t cl (DEX_METHOD.signature d));intros.
injection H0;intros;subst;trivial.
discriminate.
Qed.
Definition defined_Method (cl:t) (m:DEX_Method) :=
method cl (DEX_METHOD.signature m) = Some m.
End DEX_CLASS.
Definition DEX_Class := DEX_CLASS.t.
Module Type DEX_CLASS_TYPE.
Parameter name : DEX_Class -> DEX_ClassName.
Parameter superClass : DEX_Class -> option DEX_ClassName.
Parameter superInterfaces : DEX_Class -> list DEX_InterfaceName.
Parameter field : DEX_Class -> DEX_ShortFieldName -> option DEX_Field.
Parameter definedFields : DEX_Class -> list DEX_Field.
Parameter in_definedFields_field_some : forall c f,
In f (definedFields c) ->
field c (DEX_FIELDSIGNATURE.name (DEX_FIELD.signature f)) = Some f.
Parameter field_some_in_definedFields : forall c f sfn,
field c sfn = Some f -> In f (definedFields c).
Parameter method : DEX_Class -> DEX_ShortMethodSignature -> option DEX_Method.
Parameter method_signature_prop : forall cl mid m,
method cl mid = Some m -> mid = DEX_METHOD.signature m.
Parameter isFinal : DEX_Class -> bool.
Parameter isPublic : DEX_Class -> bool.
Parameter isAbstract : DEX_Class -> bool.
Definition defined_Method (cl:DEX_Class) (m:DEX_Method) :=
method cl (DEX_METHOD.signature m) = Some m.
End DEX_CLASS_TYPE.
Module DEX_INTERFACE.
Record t : Type := {
name : DEX_InterfaceName;
superInterfaces : list DEX_InterfaceName;
fields : DEX_MapField.t;
methods : DEX_MapShortMethSign.t DEX_Method;
isFinal : bool;
isPublic : bool;
isAbstract : bool
}.
Definition field (c:t) (f:DEX_ShortFieldName):option DEX_Field := DEX_MapField.get c.(fields) f.
Lemma field_shortname_prop : forall cl s f,
field cl s = Some f -> s = DEX_FIELDSIGNATURE.name (DEX_FIELD.signature f).
Proof.
unfold field;intros cl s f H.
assert (UU:= DEX_MapField.get_proj _ _ _ H);subst;trivial.
Qed.
Definition method (c:t) (msig:DEX_ShortMethodSignature) : option DEX_Method :=
match DEX_MapShortMethSign.get _ c.(methods) msig with
| Some m =>
if DEX_METHODSIGNATURE.eq_t msig m.(DEX_METHOD.signature) then Some m
else None
| None => None
end.
Lemma method_signature_prop : forall cl mid m,
method cl mid = Some m -> mid = DEX_METHOD.signature m.
Proof.
unfold method; intros p cl mid.
destruct DEX_MapShortMethSign.get;try (intros;discriminate).
generalize (DEX_METHODSIGNATURE.eq_t_spec cl (DEX_METHOD.signature d));
destruct (DEX_METHODSIGNATURE.eq_t cl (DEX_METHOD.signature d));intros.
injection H0;intros;subst;trivial.
discriminate.
Qed.
End DEX_INTERFACE.
Definition DEX_Interface := DEX_INTERFACE.t.
Module Type DEX_INTERFACE_TYPE.
Parameter name : DEX_Interface -> DEX_InterfaceName.
Parameter superInterfaces : DEX_Interface -> list DEX_InterfaceName.
Parameter field : DEX_Interface -> DEX_ShortFieldName -> option DEX_Field.
Parameter method : DEX_Interface -> DEX_ShortMethodSignature -> option DEX_Method.
Parameter isFinal : DEX_Interface -> bool.
Parameter isPublic : DEX_Interface -> bool.
Parameter isAbstract : DEX_Interface -> bool.
End DEX_INTERFACE_TYPE.
Module DEX_PROG.
Module DEX_ClassNameProj.
Definition element:=DEX_Class.
Definition key1 := DEX_PackageName.
Definition key2 :=DEX_ShortClassName.
Definition proj := DEX_CLASS.name.
End DEX_ClassNameProj.
Module DEX_ClassNameProj1.
Definition element:=DEX_Class.
Definition key := DEX_PackageName.
Definition proj := fun (x:element) => fst (DEX_ClassNameProj.proj x).
End DEX_ClassNameProj1.
Module DEX_MapClNameProj1 := MapProj DEX_ClassNameProj1.
Module DEX_ClassNameProj2.
Definition element := (DEX_ShortClassName * DEX_MapClNameProj1.t)%type.
Definition key := DEX_ShortClassName.
Definition proj := fun x:element => fst x.
End DEX_ClassNameProj2.
Module DEX_MapClNameProj2 := MapProj DEX_ClassNameProj2.
Module DEX_MapClass := MapProjPair DEX_ClassNameProj DEX_MapClNameProj1 DEX_MapClNameProj2.
Module DEX_InterfaceNameProj.
Definition element:=DEX_Interface.
Definition key1 := DEX_PackageName.
Definition key2 :=DEX_ShortClassName.
Definition proj := DEX_INTERFACE.name.
End DEX_InterfaceNameProj.
Module DEX_InterfaceNameProj1.
Definition element:=DEX_Interface.
Definition key := DEX_PackageName.
Definition proj := fun (x:element) => fst (DEX_InterfaceNameProj.proj x).
End DEX_InterfaceNameProj1.
Module DEX_MapInterfaceNameProj1 := MapProj DEX_InterfaceNameProj1.
Module DEX_InterfaceNameProj2.
Definition element := (DEX_ShortClassName * DEX_MapInterfaceNameProj1.t)%type.
Definition key := DEX_ShortClassName.
Definition proj := fun x:element => fst x.
End DEX_InterfaceNameProj2.
Module DEX_MapInterfaceNameProj2 := MapProj DEX_InterfaceNameProj2.
Module DEX_MapInterface :=
MapProjPair DEX_InterfaceNameProj DEX_MapInterfaceNameProj1 DEX_MapInterfaceNameProj2.
Record t : Type := {
classes_map : DEX_MapClass.t;
interfaces_map : DEX_MapInterface.t
(* DEX throwableBy_map : DEX_MapShortMethSign.t (list DEX_ClassName) *)
}.
(* DEX
Definition throwableBy (p:t) (sms:ShortMethodSignature) : list ClassName :=
match MapShortMethSign.get _ p.(throwableBy_map) sms with
| Some l => l
| None => nil
end.
*)
Definition classes p := DEX_MapClass.elements p.(classes_map).
Definition class (p:t) (cn:DEX_ClassName) : option DEX_Class :=
DEX_MapClass.get p.(classes_map) cn.
Definition defined_Class (p:t) (cl:DEX_Class) :=
class p (DEX_CLASS.name cl) = Some cl.
Lemma name_class_invariant1 : forall p cn cl,
class p cn = Some cl -> cn = DEX_CLASS.name cl.
Proof.
unfold class; intros p cn cl H0.
assert (UU:= DEX_MapClass.get_proj _ _ _ H0);subst;trivial.
Qed.
Lemma In_classes_defined_Class : forall p cl,
distinct DEX_CLASS.name (classes p) ->
In cl (classes p) -> defined_Class p cl.
Proof.
unfold defined_Class,class;intros.
apply DEX_MapClass.in_elements_get_some;trivial.
Qed.
Lemma defined_Class_In_classes : forall p cl,
defined_Class p cl -> In cl (classes p).
Proof.
unfold defined_Class, classes,class ; intros.
eapply DEX_MapClass.get_some_in_elements;eauto.
Qed.
Definition interfaces p := DEX_MapInterface.elements p.(interfaces_map).
Definition interface (p:t) (i:DEX_InterfaceName): option DEX_Interface :=
DEX_MapInterface.get p.(interfaces_map) i.
Definition defined_Interface (p:t) (i:DEX_Interface) :=
interface p (DEX_INTERFACE.name i) = Some i.
Lemma name_interface_invariant1 : forall p iname i,
interface p iname = Some i -> iname = DEX_INTERFACE.name i.
Proof.
unfold interface; intros p iname i H0.
assert (UU:= DEX_MapInterface.get_proj _ _ _ H0);subst;trivial.
Qed.
End DEX_PROG.
Definition DEX_Program := DEX_PROG.t.
Module Type DEX_PROG_TYPE.
Parameter class : DEX_Program -> DEX_ClassName -> option DEX_Class.
Definition defined_Class (p:DEX_Program) (cl:DEX_Class) :=
class p (DEX_CLASS.name cl) = Some cl.
Parameter name_class_invariant1 : forall p cn cl,
class p cn = Some cl -> cn = DEX_CLASS.name cl.
Parameter interface : DEX_Program -> DEX_InterfaceName -> option DEX_Interface.
Definition defined_Interface (p:DEX_Program) (i:DEX_Interface) :=
interface p (DEX_INTERFACE.name i) = Some i.
Parameter name_interface_invariant1 : forall p cn cl,
interface p cn = Some cl -> cn = DEX_INTERFACE.name cl.
End DEX_PROG_TYPE.
Inductive isStatic (p:DEX_Program) (fs: DEX_FieldSignature) : Prop :=
isStatic_field : forall (cn:DEX_ClassName) (cl:DEX_Class) (f:DEX_Field),
DEX_PROG.class p (fst fs) = Some cl ->
DEX_CLASS.field cl (DEX_FIELDSIGNATURE.name (snd fs)) = Some f ->
DEX_FIELD.isStatic f = true ->
isStatic p fs.
Definition javaLangObject : DEX_ClassName := (javaLang,object).
(*Definition javaLangThrowable : ClassName := (javaLang,throwable).*)
Inductive direct_subclass (p:DEX_Program) (c:DEX_Class) (s:DEX_Class) : Prop :=
| direct_subclass1 :
DEX_PROG.defined_Class p c ->
DEX_PROG.defined_Class p s ->
DEX_CLASS.superClass c = Some (DEX_CLASS.name s) ->
direct_subclass p c s.
(** [subclass] is the reflexive transitive closure of the [direct_subclass] relation
(defined over the classes of the program) *)
Definition subclass (p:DEX_Program) : DEX_Class -> DEX_Class -> Prop :=
clos_refl_trans DEX_Class (direct_subclass p).
Inductive subclass_name (p:DEX_Program) : DEX_ClassName -> DEX_ClassName -> Prop :=
| subclass_name1 : forall c1 c2,
subclass p c1 c2 ->
subclass_name p (DEX_CLASS.name c1) (DEX_CLASS.name c2).
Inductive direct_subclass_name (p:DEX_Program) : DEX_ClassName -> DEX_ClassName -> Prop :=
| direct_subclass_name1 : forall c s,
direct_subclass p c s ->
direct_subclass_name p (DEX_CLASS.name c) (DEX_CLASS.name s).
(** Similar definitions for interfaces *)
Inductive direct_subinterface (p:DEX_Program) (c:DEX_Interface) (s:DEX_Interface) : Prop :=
| direct_subinterface1 :
DEX_PROG.defined_Interface p c ->
DEX_PROG.defined_Interface p s ->
In (DEX_INTERFACE.name s) (DEX_INTERFACE.superInterfaces c) ->
direct_subinterface p c s.
(** [subinterface] is the reflexive transitive closure of the [direct_subinterface]
relation (defined over the interfaces of the program) *)
Definition subinterface (p:DEX_Program) : DEX_Interface -> DEX_Interface -> Prop :=
clos_refl_trans DEX_Interface (direct_subinterface p).
Inductive subinterface_name (p:DEX_Program) : DEX_InterfaceName -> DEX_InterfaceName -> Prop :=
| subinterface_name1 : forall c1 c2,
subinterface p c1 c2 ->
subinterface_name p (DEX_INTERFACE.name c1) (DEX_INTERFACE.name c2).
Inductive direct_subinterface_name (p:DEX_Program) : DEX_InterfaceName -> DEX_InterfaceName -> Prop :=
| direct_subinterface_name1 : forall c s,
direct_subinterface p c s ->
direct_subinterface_name p (DEX_INTERFACE.name c) (DEX_INTERFACE.name s).
Inductive class_declares_field (p:DEX_Program) (cn:DEX_ClassName) (fd:DEX_ShortFieldSignature) : DEX_Field -> Prop :=
| class_decl_field : forall cl f,
DEX_PROG.class p cn = Some cl ->
DEX_CLASS.field cl (DEX_FIELDSIGNATURE.name fd) = Some f ->
class_declares_field p cn fd f.
Inductive interface_declares_field (p:DEX_Program) (cn:DEX_InterfaceName) (fd:DEX_ShortFieldSignature) : DEX_Field -> Prop :=
| interface_decl_field : forall cl f,
DEX_PROG.interface p cn = Some cl ->
DEX_INTERFACE.field cl (DEX_FIELDSIGNATURE.name fd) = Some f ->
interface_declares_field p cn fd f.
(** [defined_field p c fd] holds if the class [c] declares or inherits a field
of signature [fd] *)
Inductive is_defined_field (p:DEX_Program) : DEX_ClassName -> DEX_FieldSignature -> DEX_Field -> Prop :=
| def_class_field : forall cn fd cn' f,
subclass_name p cn cn' ->
class_declares_field p cn' fd f ->
is_defined_field p cn (cn',fd) f
| def_interface_field : forall cn fd cl i1 i' f,
DEX_PROG.class p cn = Some cl ->
In i1 (DEX_CLASS.superInterfaces cl) ->
subinterface_name p i1 i' ->
interface_declares_field p i' fd f ->
is_defined_field p cn (i',fd) f.
Definition defined_field (p:DEX_Program) (cn:DEX_ClassName) (fs:DEX_FieldSignature) : Prop :=
exists f, is_defined_field p cn fs f.
Definition findMethod (p:DEX_Program) (msig: DEX_MethodSignature) : option DEX_Method :=
let (cn,smsig) := msig in
match DEX_PROG.class p cn with
| None => None
| Some cl => DEX_CLASS.method cl smsig
end.
Definition findField (p:DEX_Program) (fd: DEX_FieldSignature) : option DEX_Field :=
let (cn,sfs) := fd in
match DEX_PROG.class p cn with
| None => None
| Some cl => DEX_CLASS.field cl (DEX_FIELDSIGNATURE.name sfs)
end.
Definition methodPackage (mname: DEX_MethodName) : DEX_PackageName := fst (fst mname).
(* Relations [check_visibility,check_signature,overrides] are needed
to define the method [lookup] algorithm **)
Inductive check_visibility : DEX_Visibility -> DEX_PackageName -> DEX_PackageName -> Prop :=
| check_public : forall p1 p2, check_visibility Public p1 p2
| check_protected :forall p1 p2, check_visibility Protected p1 p2
| check_package :forall p, check_visibility Package p p.
(*
(** [check_signature] verifies that the two methods share the same signature and that the defining classes belong to the [subclass] relation. *)
(* CAVEAT: the methods may not be defined in the program *)
Inductive check_signature (p:Program) : MethodName*Method -> MethodName*Method -> Prop :=
| check_signature_c : forall mn1 meth1 mn2 meth2,
subclass_name p (fst mn1) (fst mn2) ->
snd mn1 = snd mn2 ->
METHODSIGNATURE.parameters (METHOD.signature meth1) =
METHODSIGNATURE.parameters (METHOD.signature meth2) ->
METHODSIGNATURE.result (METHOD.signature meth1) =
METHODSIGNATURE.result (METHOD.signature meth2) ->
check_signature p (mn1,meth1) (mn2,meth2).
(* FIXME: lookup should deal with interfaces - fb *)
(** Definition of the #<a href=http://java.sun.com/docs/books/jls/third_edition/html/classes.html##8.4.8> overrides relation </a># *)
Inductive overrides (p:Program) : MethodName*Method -> MethodName*Method -> Prop :=
| overrides_here : forall mn1 meth1 mn2 meth2,
check_signature p (mn1,meth1) (mn2,meth2) ->
check_visibility (METHOD.visibility meth2) (methodPackage mn1) (methodPackage mn2) ->
overrides p (mn1,meth1) (mn2,meth2)
| overrides_trans : forall mn1 meth1 mn' meth' mn2 meth2,
(* In the spec, there is a side-condition which says that minter is different from msig1 and msig2 !?! *)
check_signature p (mn1,meth1) (mn2,meth2) ->
overrides p (mn1,meth1) (mn',meth') -> overrides p (mn',meth') (mn2,meth2) ->
overrides p (mn1,meth1) (mn2,meth2).
*)
Inductive lookup_here (p:DEX_Program) : DEX_ClassName -> DEX_ShortMethodSignature -> DEX_Method -> Prop :=
| lookup_here_c : forall cn msig meth,
findMethod p (cn,msig) = Some meth ->
lookup_here p cn msig meth.
Inductive lookup (p:DEX_Program) : DEX_ClassName -> DEX_ShortMethodSignature -> (DEX_ClassName*DEX_Method) -> Prop :=
| lookup_no_up : forall cn msig meth, lookup_here p cn msig meth -> lookup p cn msig (cn,meth)
| lookup_up : forall cn msig, (forall meth, ~ lookup_here p cn msig meth) ->
forall super res , direct_subclass_name p cn super -> lookup p super msig res -> lookup p cn msig res.
(*
Inductive handler_catch (p:Program) : ExceptionHandler -> PC -> ClassName -> Prop :=
(* The current handler catches all the exceptions in its range *)
| handler_catch_all : forall pc ex e,
EXCEPTIONHANDLER.catchType ex = None ->
EXCEPTIONHANDLER.isPCinRange ex pc = true ->
handler_catch p ex pc e
(* The current handler specifies the type of exception it catches *)
| handler_catch_one : forall pc ex cl1 cl2,
EXCEPTIONHANDLER.catchType ex = Some cl1 ->
EXCEPTIONHANDLER.isPCinRange ex pc = true ->
subclass_name p cl2 cl1 ->
handler_catch p ex pc cl2.
(** Lookup in the given list of exception handlers if one of them catches
the current exception *)