source: src/Clight/toCminorOps.ma @ 2896

Last change on this file since 2896 was 2608, checked in by garnier, 7 years ago

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

File size: 6.4 KB
Line 
1include "Clight/toCminor.ma".
2include "Clight/Cexec.ma".
3include "Clight/Clight_abstract.ma".
4include "Cminor/Cminor_abstract.ma".
5include "Clight/frontend_misc.ma".
6include "Clight/memoryInjections.ma".
7
8
9lemma translate_notbool_to_cminor :
10  ∀t,sg,arg.
11  ∀cmop. translate_unop (typ_of_type t) (ASTint I32 sg) Onotbool = OK ? cmop →
12  ∀res. sem_unary_operation Onotbool arg t = Some ? res →
13        eval_unop (typ_of_type t) (ASTint I32 sg) cmop arg = Some ? res.
14*
15[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
16| #structname #fieldspec | #unionname #fieldspec | #id ]
17normalize in match (typ_of_type ?);
18#sg #arg #cmop
19whd in ⊢ (??%% → ?); #Heq destruct (Heq)
20cases arg
21[ | #vsz #vi | | #vp
22| | #vsz #vi | | #vp
23| | #vsz #vi | | #vp
24| | #vsz #vi | | #vp
25| | #vsz #vi | | #vp
26| | #vsz #vi | | #vp
27| | #vsz #vi | | #vp
28| | #vsz #vi | | #vp ]
29#res
30whd in ⊢ ((??%?) → ?);
31#Heq
32[ 6,11,12: | *: destruct (Heq) ]
33[ 2,3: destruct (Heq) whd in match (eval_unop ????); @refl
34| 1: lapply Heq -Heq @(eq_intsize_elim … sz vsz)
35     #H normalize nodelta #Heq destruct
36     whd in match (eval_unop ????);
37     cases (eq_bv (bitsize_of_intsize vsz) vi (zero (bitsize_of_intsize vsz))) @refl
38] qed.
39
40lemma translate_notint_to_cminor :
41  ∀t,t',arg.
42  ∀cmop. translate_unop (typ_of_type t) t' Onotint = OK ? cmop →
43  ∀res. sem_unary_operation Onotint arg t = Some ? res →
44        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
45#ty *
46[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
47#sz #sg #arg #cmop
48whd in match (translate_unop ???);
49@(match typ_eq (ASTint sz sg) (typ_of_type ty)
50  with
51  [ inl H ⇒ ?
52  | inr H ⇒ ? ])
53normalize nodelta
54[ 2: #Heq destruct ]
55lapply H -H
56lapply cmop -cmop
57cases ty
58[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
59| #structname #fieldspec | #unionname #fieldspec | #id ]
60normalize nodelta
61#cmop normalize in match (typ_of_type ?); #H destruct
62#H' normalize in H';
63destruct (H')
64#res
65whd in match (sem_unary_operation ???);
66cases arg
67[ | #vsz #vi | | #vp
68| | #vsz #vi | | #vp
69| | #vsz #vi | | #vp
70| | #vsz #vi | | #vp ]
71whd in match (sem_notint ?);
72#H destruct (H) @refl
73qed.
74
75
76lemma translate_negint_to_cminor :
77  ∀t,t',arg.
78  ∀cmop. translate_unop (typ_of_type t) t' Oneg = OK ? cmop →
79  ∀res. sem_unary_operation Oneg arg t = Some ? res →
80        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
81#ty *
82[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
83#sz #sg #arg #cmop
84whd in match (translate_unop ???);
85@(match typ_eq (ASTint sz sg) (typ_of_type ty)
86  with
87  [ inl H ⇒ ?
88  | inr H ⇒ ? ])
89normalize nodelta
90[ 2: #Heq destruct ]
91lapply H -H
92lapply cmop -cmop
93cases ty
94[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
95| #structname #fieldspec | #unionname #fieldspec | #id ]
96normalize nodelta
97#cmop normalize in match (typ_of_type ?); #H destruct
98#H' normalize in H';
99destruct (H')
100#res
101whd in match (sem_unary_operation ???);
102cases arg
103[ | #vsz #vi | | #vp
104| | #vsz #vi | | #vp
105| | #vsz #vi | | #vp
106| | #vsz #vi | | #vp ]
107whd in match (sem_neg ??);
108#H destruct (H)
109whd in match (eval_unop ????);
110cases (eq_intsize sz' vsz) in H; normalize nodelta
111#H destruct @refl
112qed.
113
114
115lemma translate_unop :
116  ∀ty,sg,op,cmop.
117  translate_unop (typ_of_type ty) (ASTint I32 sg) op = OK ? cmop →
118  ∀arg,res. sem_unary_operation op arg ty = Some ? res →
119            eval_unop (typ_of_type ty) (ASTint I32 sg) cmop arg = Some ? res.
120#ty #sg * #cmop #Htranslate #arg
121[ @translate_notbool_to_cminor assumption
122| @translate_notint_to_cminor assumption
123| @translate_negint_to_cminor assumption ]
124qed.
125
126
127lemma classify_add_inversion :
128  ∀ty1,ty2.
129    (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_ii sz sg) ∨
130    (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_pi n ty' sz sg) ∨
131    (∃n,sz,sg,ty'. ty1 = Tint sz sg ∧ ty2 = ptr_type ty' n ∧ classify_add ty1 ty2 ≃ add_case_ip n sz sg ty') ∨
132    (classify_add ty1 ty2 = add_default ty1 ty2).
133#ty1 #ty2
134cases (classify_add ty1 ty2)
135[ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
136| #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
137| #n #sz #sg #ty %1 %2 %{n} %{sz} %{sg} %{ty} @conj try @conj try @refl @refl_jmeq
138| #tya #tyb %2 @refl ]
139qed.
140
141lemma classify_sub_inversion :
142  ∀ty1,ty2.
143    (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_sub ty1 ty2 ≃ sub_case_ii sz sg) ∨
144    (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_sub ty1 ty2 ≃ sub_case_pi n ty' sz sg) ∨
145    (∃ty1',ty2',n1,n2. ty1 = ptr_type ty1' n1 ∧ ty2 = ptr_type ty2' n2 ∧ classify_sub ty1 ty2 ≃ sub_case_pp n1 n2 ty1' ty2') ∨
146    (classify_sub ty1 ty2 = sub_default ty1 ty2).
147#ty1 #ty2
148cases (classify_sub ty1 ty2)
149[ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
150| #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
151| #n1 #n2 #t1 #t2 %1 %2 %{t1} %{t2} %{n1} %{n2} @conj try @conj try @refl @refl_jmeq
152| #tya #tyb %2 @refl ]
153qed.
154
155lemma classify_aop_inversion :
156  ∀ty1,ty2.
157    (∃sz,sg. ty1 = (Tint sz sg) ∧ ty2 = (Tint sz sg) ∧ classify_aop ty1 ty2 ≃ aop_case_ii sz sg) ∨
158    classify_aop ty1 ty2 = aop_default ty1 ty2.
159#ty1 #ty2
160cases (classify_aop ty1 ty2)
161[ #sz #sg %1 %{sz} %{sg} @conj try @conj try @refl_jmeq
162| #ty #ty' %2 @refl ]
163qed.
164
165
166lemma complete_cmp_inversion :
167  ∀ty:type.
168  ∀e:expr (ASTint I8 Unsigned).
169  ∀r:expr (typ_of_type ty).
170   complete_cmp ty e = return r →
171   ∃sz,sg. ty = Tint sz sg ∧
172           r ≃ Op1 (ASTint I8 Unsigned) (ASTint sz sg) (Ocastint I8 Unsigned sz sg) e.
173*
174[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
175| #structname #fieldspec | #unionname #fieldspec | #id ]
176#e whd in match (typ_of_type ?);
177#r whd in ⊢ ((??%%) → ?);
178#H destruct
179%{sz} %{sg} @conj try @refl @refl_jmeq
180qed.
181
182
183lemma pointer_translation_eq_block :
184  ∀E,p1,p2,p1',p2'.
185  pointer_translation p1 E = Some ? p1' →
186  pointer_translation p2 E = Some ? p2' →
187  eq_block (pblock p1) (pblock p2) = true →
188  eq_block (pblock p1') (pblock p2') = true.
189#E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2'
190#H1 #H2 #Heq_block
191lapply (eq_block_to_refl … Heq_block) #H destruct (H)
192lapply H1 lapply H2 -H1 -H2
193whd in ⊢ ((??%?) → (??%?) → ?);
194cases (E b2) normalize nodelta
195[ #Habsurd destruct ]
196* #bx #ox normalize nodelta #Heq1 #Heq2 destruct
197@eq_block_b_b
198qed.
Note: See TracBrowser for help on using the repository browser.