source: src/Clight/toCminorOps.ma @ 3178

Last change on this file since 3178 was 3171, checked in by mckinna, 6 years ago

removed redundant dependencies

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