source: src/Clight/toCminorOps.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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 (block_id 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.