1 | include "RTLabs/syntax.ma". |
---|
2 | include "RTL/RTL_paolo.ma". |
---|
3 | include "common/AssocList.ma". |
---|
4 | include "common/FrontEndOps.ma". |
---|
5 | include "common/Graphs.ma". |
---|
6 | include "joint/TranslateUtils_paolo.ma". |
---|
7 | include "utilities/lists.ma". |
---|
8 | include alias "ASM/BitVector.ma". |
---|
9 | include alias "arithmetics/nat.ma". |
---|
10 | |
---|
11 | |
---|
12 | (* Paolo: to be moved elsewhere *) |
---|
13 | |
---|
14 | notation "r ← a1 .op. a2" with precedence 50 for |
---|
15 | @{'op2 $op $r $a1 $a2}. |
---|
16 | notation "r ← . op . a" with precedence 50 for |
---|
17 | @{'op1 $op $r $a}. |
---|
18 | notation "r ← a" with precedence 50 for |
---|
19 | @{'mov $r $a}. |
---|
20 | notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for |
---|
21 | @{'opaccs $op $r $s $a1 $a2}. |
---|
22 | |
---|
23 | interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2). |
---|
24 | interpretation "op1" 'op1 op r a = (OP1 ? ? op r a). |
---|
25 | interpretation "move" 'mov r a = (MOVE ? ? (REG r a)). |
---|
26 | interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2). |
---|
27 | |
---|
28 | |
---|
29 | definition size_of_sig_type ≝ |
---|
30 | λsig. |
---|
31 | match sig with |
---|
32 | [ ASTint isize sign ⇒ |
---|
33 | let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in |
---|
34 | isize' ÷ (nat_of_bitvector ? int_size) |
---|
35 | | ASTfloat _ ⇒ ? (* dpm: not implemented *) |
---|
36 | | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size |
---|
37 | ]. |
---|
38 | cases not_implemented; |
---|
39 | qed. |
---|
40 | |
---|
41 | inductive register_type: Type[0] ≝ |
---|
42 | | register_int: register → register_type |
---|
43 | | register_ptr: register → register → register_type. |
---|
44 | |
---|
45 | definition local_env ≝ identifier_map RegisterTag (list register). |
---|
46 | |
---|
47 | definition mem_local_env : register → local_env → bool ≝ |
---|
48 | λr,e. member … e r. |
---|
49 | |
---|
50 | definition add_local_env : register → list register → local_env → local_env ≝ |
---|
51 | λr,v,e. add … e r v. |
---|
52 | |
---|
53 | definition find_local_env : register → local_env → list register ≝ |
---|
54 | λr: register.λenv. lookup_def … env r []. |
---|
55 | |
---|
56 | definition find_local_env_arg ≝ |
---|
57 | λr,lenv. map … Reg (find_local_env r lenv). |
---|
58 | |
---|
59 | let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝ |
---|
60 | match n with |
---|
61 | [ O ⇒ 〈[],runiverse〉 |
---|
62 | | S n' ⇒ |
---|
63 | let 〈r,runiverse〉 ≝ fresh … runiverse in |
---|
64 | let 〈res,runiverse〉 ≝ register_freshes runiverse n' in |
---|
65 | 〈r::res,runiverse〉 ]. |
---|
66 | |
---|
67 | definition initialize_local_env_internal ≝ |
---|
68 | λlenv_runiverse. |
---|
69 | λr_sig. |
---|
70 | let 〈lenv,runiverse〉 ≝ lenv_runiverse in |
---|
71 | let 〈r, sig〉 ≝ r_sig in |
---|
72 | let size ≝ size_of_sig_type sig in |
---|
73 | let 〈rs,runiverse〉 ≝ register_freshes runiverse size in |
---|
74 | 〈add_local_env r rs lenv,runiverse〉. |
---|
75 | |
---|
76 | definition initialize_local_env ≝ |
---|
77 | λruniverse. |
---|
78 | λregisters. |
---|
79 | λresult. |
---|
80 | let registers ≝ |
---|
81 | match result with |
---|
82 | [ None ⇒ registers |
---|
83 | | Some rt ⇒ rt :: registers |
---|
84 | ] |
---|
85 | in |
---|
86 | foldl … initialize_local_env_internal 〈empty_map …,runiverse〉 registers. |
---|
87 | |
---|
88 | definition map_list_local_env_internal ≝ |
---|
89 | λlenv,res,r. res @ (find_local_env r lenv). |
---|
90 | |
---|
91 | definition map_list_local_env ≝ |
---|
92 | λlenv,regs. foldl … (map_list_local_env_internal lenv) [ ] regs. |
---|
93 | |
---|
94 | definition make_addr ≝ |
---|
95 | λA. |
---|
96 | λlst: list A. |
---|
97 | λprf: 2 = length A lst. |
---|
98 | match lst return λx. 2 = |x| → A × A with |
---|
99 | [ nil ⇒ λlst_nil_prf. ? |
---|
100 | | cons hd tl ⇒ λprf. |
---|
101 | match tl return λx. 1 = |x| → A × A with |
---|
102 | [ nil ⇒ λtl_nil_prf. ? |
---|
103 | | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉 |
---|
104 | ] ? |
---|
105 | ] prf. |
---|
106 | [1: normalize in lst_nil_prf; |
---|
107 | destruct(lst_nil_prf) |
---|
108 | |2: normalize in prf; |
---|
109 | @injective_S |
---|
110 | assumption |
---|
111 | |3: normalize in tl_nil_prf; |
---|
112 | destruct(tl_nil_prf) |
---|
113 | ] |
---|
114 | qed. |
---|
115 | |
---|
116 | definition find_and_addr ≝ |
---|
117 | λr,lenv. make_addr ? (find_local_env r lenv). |
---|
118 | |
---|
119 | definition rtl_args ≝ |
---|
120 | λregs_list,lenv. flatten … (map … (λr.find_local_env_arg r lenv) regs_list). |
---|
121 | |
---|
122 | definition split_into_bytes: |
---|
123 | ∀size. ∀int: bvint size. Σbytes: list Byte. |bytes| = size_intsize size ≝ |
---|
124 | λsize. |
---|
125 | match size return λsize.∀int: bvint size. Σbytes. |bytes| = size_intsize size with |
---|
126 | [ I8 ⇒ λint. ? | I16 ⇒ λint. ? | I32 ⇒ λint. ? ]. |
---|
127 | [ %[@[int]] // |
---|
128 | | %[@(let 〈h,l〉 ≝ split ? 8 … int in [l;h])] cases (split ????) normalize // |
---|
129 | | %[@(let 〈h1,l〉 ≝ split ? 8 … int in |
---|
130 | let 〈h2,l〉 ≝ split ? 8 … l in |
---|
131 | let 〈h3,l〉 ≝ split ? 8 … l in |
---|
132 | [l;h3;h2;h1])] |
---|
133 | cases (split ????) #h1 #l normalize |
---|
134 | cases (split ????) #h2 #l normalize |
---|
135 | cases (split ????) // ] |
---|
136 | qed. |
---|
137 | |
---|
138 | |
---|
139 | lemma eqb_implies_eq: |
---|
140 | ∀m, n: nat. |
---|
141 | eqb m n = true → m = n. |
---|
142 | #m#n@eqb_elim // #_ #F destruct(F) qed. |
---|
143 | |
---|
144 | definition translate_op: |
---|
145 | ∀globals. Op2 → |
---|
146 | ∀dests : list register. |
---|
147 | ∀srcrs1 : list rtl_argument. |
---|
148 | ∀srcrs2 : list rtl_argument. |
---|
149 | |dests| = |srcrs1| → |srcrs1| = |srcrs2| → |
---|
150 | list (rtl_instruction globals) |
---|
151 | ≝ |
---|
152 | λglobals: list ident. |
---|
153 | λop. |
---|
154 | λdestrs. |
---|
155 | λsrcrs1. |
---|
156 | λsrcrs2. |
---|
157 | λprf1,prf2. |
---|
158 | let f_add ≝ OP2 rtl_params globals in |
---|
159 | let res : list (rtl_instruction globals) ≝ |
---|
160 | map3 ???? (f_add op) destrs srcrs1 srcrs2 ?? in |
---|
161 | (* first, clear carry if op relies on it *) |
---|
162 | match op with |
---|
163 | [ Addc ⇒ [clear_carry ?] |
---|
164 | | Sub ⇒ [clear_carry ?] |
---|
165 | | _ ⇒ [ ] |
---|
166 | ] @ |
---|
167 | match op with |
---|
168 | (* if adding, we use a first Add op, that clear the carry, and then Addc's *) |
---|
169 | [ Add ⇒ |
---|
170 | match destrs return λx.|destrs| = |x| → list (rtl_instruction globals) with |
---|
171 | [ nil ⇒ λeq_destrs.[ ] |
---|
172 | | cons destr destrs' ⇒ λeq_destrs. |
---|
173 | match srcrs1 return λy.|srcrs1| = |y| → list (rtl_instruction globals) with |
---|
174 | [ nil ⇒ λeq_srcrs1.⊥ |
---|
175 | | cons srcr1 srcrs1' ⇒ λeq_srcrs1. |
---|
176 | match srcrs2 return λz.|srcrs2| = |z| → list (rtl_instruction globals) with |
---|
177 | [ nil ⇒ λeq_srcrs2.⊥ |
---|
178 | | cons srcr2 srcrs2' ⇒ λeq_srcrs2. |
---|
179 | f_add Add destr srcr1 srcr2 :: |
---|
180 | map3 ???? (f_add Addc) destrs' srcrs1' srcrs2' ?? |
---|
181 | ] (refl …) |
---|
182 | ] (refl …) |
---|
183 | ] (refl …) |
---|
184 | | _ ⇒ res |
---|
185 | ]. |
---|
186 | [5,6: assumption |
---|
187 | |1: >prf1 in eq_destrs; >eq_srcrs1 normalize // |
---|
188 | |2: >prf2 in eq_srcrs1; >eq_srcrs2 normalize // |
---|
189 | |3: >prf2 in eq_srcrs1; >eq_srcrs2 normalize #H destruct(H) |
---|
190 | |4: >prf1 in eq_destrs; >eq_srcrs1 normalize #H destruct(H) |
---|
191 | qed. |
---|
192 | |
---|
193 | let rec nat_to_args (size : nat) (k : nat) on size : Σl : list rtl_argument.|l| = size ≝ |
---|
194 | match size with |
---|
195 | [ O ⇒ [ ] |
---|
196 | | S size' ⇒ |
---|
197 | match nat_to_args size' (k ÷ 8) with |
---|
198 | [ mk_Sig res prf ⇒ |
---|
199 | imm_nat k :: res |
---|
200 | ] |
---|
201 | ]. normalize // qed. |
---|
202 | |
---|
203 | definition size_of_cst ≝ λcst.match cst with |
---|
204 | [ Ointconst size _ ⇒ size_intsize size |
---|
205 | | Ofloatconst float ⇒ ? (* not implemented *) |
---|
206 | | _ ⇒ 2 |
---|
207 | ]. |
---|
208 | cases not_implemented qed. |
---|
209 | |
---|
210 | definition cst_well_defd : list ident → constant → Prop ≝ λglobals,cst. |
---|
211 | match cst with |
---|
212 | [ Oaddrsymbol id offset ⇒ member id (eq_identifier ?) globals |
---|
213 | | _ ⇒ True |
---|
214 | ]. |
---|
215 | |
---|
216 | definition translate_cst : |
---|
217 | ∀globals: list ident. |
---|
218 | ∀cst_sig: Σcst : constant.cst_well_defd globals cst. |
---|
219 | ∀destrs: list register. |
---|
220 | |destrs| = size_of_cst cst_sig → list (rtl_instruction globals) |
---|
221 | ≝ |
---|
222 | λglobals,cst_sig,destrs,prf. |
---|
223 | match cst_sig return λy.cst_sig = y → list (rtl_instruction globals) with |
---|
224 | [ mk_Sig cst cst_good ⇒ λeqcst_sig. |
---|
225 | match cst return λx.cst = x → list (rtl_instruction globals) |
---|
226 | with |
---|
227 | [ Ointconst size const ⇒ λeqcst. |
---|
228 | match split_into_bytes size const with |
---|
229 | [ mk_Sig bytes bytes_length_proof ⇒ |
---|
230 | map2 … (reg_from_byte globals) destrs bytes ? |
---|
231 | ] |
---|
232 | | Ofloatconst float ⇒ λ_.⊥ |
---|
233 | | Oaddrsymbol id offset ⇒ λeqcst. |
---|
234 | let 〈r1, r2〉 ≝ make_addr … destrs ? in |
---|
235 | [ADDRESS rtl_params globals id ? r1 r2] |
---|
236 | | Oaddrstack offset ⇒ λeqcst. |
---|
237 | let 〈r1, r2〉 ≝ make_addr … destrs ? in |
---|
238 | [extension rtl_params globals (rtl_st_ext_stack_address r1 r2)] |
---|
239 | ] (refl …) |
---|
240 | ] (refl …). |
---|
241 | [2: cases not_implemented |
---|
242 | |3: >eqcst in cst_good; //] |
---|
243 | >eqcst_sig in prf; |
---|
244 | >eqcst whd in ⊢ (???% → ?); #prf |
---|
245 | [1: >bytes_length_proof |
---|
246 | >prf //] |
---|
247 | // |
---|
248 | qed. |
---|
249 | |
---|
250 | |
---|
251 | definition translate_move : |
---|
252 | ∀globals. |
---|
253 | ∀destrs: list register. |
---|
254 | ∀srcrs: list rtl_argument. |
---|
255 | |destrs| = |srcrs| → list (rtl_instruction globals) ≝ |
---|
256 | λglobals,destrs,srcrs,length_eq. |
---|
257 | map2 … (λdst,src.dst ← src) destrs srcrs length_eq. |
---|
258 | |
---|
259 | let rec make |
---|
260 | (A: Type[0]) (elt: A) (n: nat) on n ≝ |
---|
261 | match n with |
---|
262 | [ O ⇒ [ ] |
---|
263 | | S n' ⇒ elt :: make A elt n' |
---|
264 | ]. |
---|
265 | |
---|
266 | lemma make_length: |
---|
267 | ∀A: Type[0]. |
---|
268 | ∀elt: A. |
---|
269 | ∀n: nat. |
---|
270 | n = length ? (make A elt n). |
---|
271 | #A #ELT #N |
---|
272 | elim N |
---|
273 | [ normalize % |
---|
274 | | #N #IH |
---|
275 | normalize <IH % |
---|
276 | ] |
---|
277 | qed. |
---|
278 | |
---|
279 | definition sign_mask : ∀globals.register → register → list (rtl_instruction globals) ≝ |
---|
280 | (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that: |
---|
281 | byte in destr if srcr is: neg | pos |
---|
282 | destr ← srcr | 127 11...1 | 01...1 |
---|
283 | destr ← destr <rot< 1 1...11 | 1...10 |
---|
284 | destr ← INC destr 0....0 | 1....1 |
---|
285 | destr ← CPL destr 1....1 | 0....0 |
---|
286 | *) |
---|
287 | λglobals,destr,srcr. |
---|
288 | [destr ← srcr .Or. 127 ; |
---|
289 | destr ← .Rl. destr ; |
---|
290 | destr ← .Inc. destr ; |
---|
291 | destr ← .Cmpl. destr ]. |
---|
292 | |
---|
293 | definition translate_cast_signed : |
---|
294 | ∀globals : list ident. |
---|
295 | list register → register → bind_list register unit (rtl_instruction globals) ≝ |
---|
296 | λglobals,destrs,srcr. |
---|
297 | ν tmp in |
---|
298 | (sign_mask ? tmp srcr @ |
---|
299 | translate_move ? destrs (make ? (Reg tmp) (|destrs|)) (make_length …)). |
---|
300 | |
---|
301 | definition translate_cast_unsigned : |
---|
302 | ∀globals : list ident. |
---|
303 | list register → list (rtl_instruction globals) ≝ |
---|
304 | λglobals,destrs. |
---|
305 | match nat_to_args (|destrs|) 0 with |
---|
306 | [ mk_Sig res prf ⇒ translate_move ? destrs res ?]. |
---|
307 | // qed. |
---|
308 | |
---|
309 | theorem length_map : ∀A,B.∀f:A→B.∀l : list A.|map … f l| = |l|. |
---|
310 | #A#B#f #l elim l normalize // qed. |
---|
311 | |
---|
312 | (* using size of lists as size of ints *) |
---|
313 | definition translate_cast : |
---|
314 | ∀globals: list ident. |
---|
315 | signedness → list register → list register → |
---|
316 | bind_list register unit (rtl_instruction globals) ≝ |
---|
317 | λglobals,src_sign,destrs,srcrs. |
---|
318 | match srcrs |
---|
319 | return λy. y = srcrs → bind_list register unit (rtl_instruction globals) |
---|
320 | with |
---|
321 | [ nil ⇒ λ_.translate_cast_unsigned ? destrs (* srcrs = [ ] ⇒ we fill with 0 *) |
---|
322 | | _ ⇒ λeq_srcrs. |
---|
323 | match reduce_strong ? ? destrs srcrs with |
---|
324 | [ mk_Sig crl len_proof ⇒ |
---|
325 | (* move prefix of srcrs in destrs *) |
---|
326 | translate_move ? (\fst (\fst crl)) (map … Reg (\fst (\snd crl))) ? @ |
---|
327 | match \snd (\snd crl) with |
---|
328 | [ nil ⇒ |
---|
329 | match src_sign return λ_.bind_list register unit (rtl_instruction globals) with |
---|
330 | [ Unsigned ⇒ translate_cast_unsigned ? (\snd (\fst crl)) |
---|
331 | | Signed ⇒ |
---|
332 | translate_cast_signed ? (\snd (\fst crl)) (last_safe ? srcrs ?) |
---|
333 | ] |
---|
334 | | _ ⇒ [ ] (* nothing to do if |srcrs| > |destrs| *) |
---|
335 | ] |
---|
336 | ] |
---|
337 | ] (refl …). |
---|
338 | [ >len_proof >length_map @refl |
---|
339 | | <eq_srcrs normalize // |
---|
340 | ] qed. |
---|
341 | |
---|
342 | definition translate_notint : |
---|
343 | ∀globals : list ident. |
---|
344 | ∀destrs : list register. |
---|
345 | ∀srcrs_arg : list register. |
---|
346 | |destrs| = |srcrs_arg| → list (rtl_instruction globals) ≝ |
---|
347 | λglobals, destrs, srcrs, prf. |
---|
348 | map2 ??? (OP1 rtl_params globals Cmpl) destrs srcrs prf. |
---|
349 | |
---|
350 | |
---|
351 | definition translate_negint : ∀globals.? → ? → ? → bind_list register unit (rtl_instruction globals) ≝ |
---|
352 | λglobals: list ident. |
---|
353 | λdestrs: list register. |
---|
354 | λsrcrs: list register. |
---|
355 | λprf: |destrs| = |srcrs|. (* assert in caml code *) |
---|
356 | translate_notint … destrs srcrs prf @ |
---|
357 | match nat_to_args (|destrs|) 1 with |
---|
358 | [ mk_Sig res prf' ⇒ |
---|
359 | translate_op ? Add destrs (map … Reg destrs) res ?? |
---|
360 | ]. |
---|
361 | // qed. |
---|
362 | |
---|
363 | definition translate_notbool: |
---|
364 | ∀globals : list ident. |
---|
365 | list register → list register → |
---|
366 | bind_list register unit (rtl_instruction globals) ≝ |
---|
367 | λglobals,destrs,srcrs. |
---|
368 | match destrs with |
---|
369 | [ nil ⇒ [ ] |
---|
370 | | cons destr destrs' ⇒ |
---|
371 | translate_cast_unsigned ? destrs' @ (* fill destrs' with 0 *) |
---|
372 | match srcrs with |
---|
373 | [ nil ⇒ [destr ← 0] |
---|
374 | | cons srcr srcrs' ⇒ |
---|
375 | let f : register → rtl_instruction globals ≝ |
---|
376 | λr. OP2 ?? Or destr (Reg destr) (Reg r) in |
---|
377 | reg_from_reg … srcr destr :: |
---|
378 | map … f srcrs' @ |
---|
379 | (* now destr is non-null iff srcrs was non-null *) |
---|
380 | clear_carry … :: |
---|
381 | (* many uses of 0, better not use immediates *) |
---|
382 | ν tmp in |
---|
383 | [tmp ← 0 ; |
---|
384 | destr ← tmp .Sub. tmp ; |
---|
385 | (* now carry bit is set iff destr was non-null *) |
---|
386 | destr ← tmp .Addc. tmp] |
---|
387 | ] |
---|
388 | ]. |
---|
389 | |
---|
390 | definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? → |
---|
391 | bind_list register unit (rtl_instruction globals) ≝ |
---|
392 | λglobals. |
---|
393 | λty, ty'. |
---|
394 | λop1: unary_operation ty ty'. |
---|
395 | λdestrs: list register. |
---|
396 | λsrcrs: list register. |
---|
397 | λprf1: |destrs| = size_of_sig_type ty'. |
---|
398 | λprf2: |srcrs| = size_of_sig_type ty. |
---|
399 | match op1 |
---|
400 | return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' → |
---|
401 | bind_list register unit (rtl_instruction globals) with |
---|
402 | [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2. |
---|
403 | translate_cast globals src_sign destrs srcrs |
---|
404 | | Onegint sz sg ⇒ λeq1,eq2. |
---|
405 | translate_negint globals destrs srcrs ? |
---|
406 | | Onotbool _ _ _ _ ⇒ λeq1,eq2. |
---|
407 | translate_notbool globals destrs srcrs |
---|
408 | | Onotint sz sg ⇒ λeq1,eq2. |
---|
409 | translate_notint globals destrs srcrs ? |
---|
410 | | Optrofint sz sg r ⇒ λeq1,eq2. |
---|
411 | translate_cast globals Unsigned destrs srcrs |
---|
412 | | Ointofptr sz sg r ⇒ λeq1,eq2. |
---|
413 | translate_cast globals Unsigned destrs srcrs |
---|
414 | | Oid t ⇒ λeq1,eq2. |
---|
415 | translate_move globals destrs (map … Reg srcrs) ? |
---|
416 | | _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *) |
---|
417 | ] (refl …) (refl …). |
---|
418 | [3,4,5,6,7,8,9: cases not_implemented |
---|
419 | |*: destruct >prf1 >prf2 // |
---|
420 | ] |
---|
421 | qed. |
---|
422 | |
---|
423 | let rec range_strong_internal (start : ℕ) (count : ℕ) |
---|
424 | (* Paolo: no notation to avoid ambiguity *) |
---|
425 | on count : list (Σn : ℕ.lt n (plus start count)) ≝ |
---|
426 | match count return λx.count = x → list (Σn : ℕ. n < start + count) |
---|
427 | with |
---|
428 | [ O ⇒ λ_.[ ] |
---|
429 | | S count' ⇒ λEQ. |
---|
430 | let f : (Σn : ℕ. lt n (S start + count')) → Σn : ℕ. lt n (start + count) ≝ |
---|
431 | λsig.match sig with [mk_Sig n prf ⇒ n] in |
---|
432 | start :: map … f (range_strong_internal (S start) count') |
---|
433 | ] (refl …). |
---|
434 | destruct(EQ) // qed. |
---|
435 | |
---|
436 | definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝ |
---|
437 | λend.range_strong_internal 0 end. |
---|
438 | |
---|
439 | definition translate_mul_i : |
---|
440 | ∀globals. |
---|
441 | register → register → |
---|
442 | (* size of destination and sources *) |
---|
443 | ∀n : ℕ. |
---|
444 | (* the temporary destination, with a dummy register at the end *) |
---|
445 | ∀tmp_destrs_dummy : list register. |
---|
446 | ∀srcrs1,srcrs2 : list rtl_argument. |
---|
447 | |tmp_destrs_dummy| = S n → |
---|
448 | n = |srcrs1| → |
---|
449 | |srcrs1| = |srcrs2| → |
---|
450 | (* the position of the least significant byte of the result we compute at |
---|
451 | this stage (goes from 0 to n in the main function) *) |
---|
452 | ∀k : ℕ. |
---|
453 | lt k n → |
---|
454 | (* the position of the byte in the first source we will use in this stage. |
---|
455 | the position in the other source will be k - i *) |
---|
456 | (Σi.i<S k) → |
---|
457 | (* the accumulator *) |
---|
458 | list (rtl_instruction globals) → |
---|
459 | list (rtl_instruction globals) ≝ |
---|
460 | λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2, |
---|
461 | tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc. |
---|
462 | (* the following will expand to |
---|
463 | a, b ← srcrs1[i] * srcrs2[k-i] |
---|
464 | tmp_destrs_dummy[k] ← tmp_destrs_dummy[k] + a |
---|
465 | tmp_destrs_dummy[k+1] ← tmp_destrs_dummy[k+1] + b + C |
---|
466 | tmp_destrs_dummy[k+2] ← tmp_destrs_dummy[k+2] + 0 + C |
---|
467 | ... |
---|
468 | tmp_destrs_dummy[n] ← tmp_destrs_dummy[n] + 0 + C |
---|
469 | ( all calculations on tmp_destrs_dummy[n] will be eliminated with |
---|
470 | liveness analysis) *) |
---|
471 | match i_sig with |
---|
472 | [ mk_Sig i i_prf ⇒ |
---|
473 | (* we pad the result of a byte multiplication with zeros in order |
---|
474 | for the bit to be carried. Redundant calculations will be eliminated |
---|
475 | by constant propagation. *) |
---|
476 | let args : list rtl_argument ≝ |
---|
477 | [Reg a;Reg b] @ make ? (Imm (zero …)) (n - 1 - k) in |
---|
478 | let tmp_destrs_view : list register ≝ |
---|
479 | ltl ? tmp_destrs_dummy k in |
---|
480 | ❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?) :: |
---|
481 | translate_op … Add tmp_destrs_view (map … Reg tmp_destrs_view) args ?? @ |
---|
482 | acc |
---|
483 | ]. |
---|
484 | [ @lt_plus_to_minus [ @le_S_S_to_le assumption | <srcrs2_prf <srcrs1_prf |
---|
485 | whd >(plus_n_O (S k)) @le_plus // ] |
---|
486 | | <srcrs1_prf |
---|
487 | @(transitive_le … i_prf k_prf) |
---|
488 | | >length_map // |
---|
489 | | >length_map |
---|
490 | >length_ltl |
---|
491 | >tmp_destrs_dummy_prf >length_append |
---|
492 | <make_length |
---|
493 | normalize in ⊢ (???(?%?)); |
---|
494 | >plus_minus_commutative |
---|
495 | [2: @le_plus_to_minus_r <plus_n_Sm <plus_n_O assumption] |
---|
496 | cut (S n = 2 + (n - 1)) |
---|
497 | [2: #EQ >EQ //] |
---|
498 | >plus_minus_commutative |
---|
499 | [2: @(transitive_le … k_prf) //] |
---|
500 | @sym_eq |
---|
501 | @plus_to_minus |
---|
502 | <plus_n_Sm |
---|
503 | // |
---|
504 | ] qed. |
---|
505 | |
---|
506 | definition translate_mul : ∀globals.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝ |
---|
507 | λglobals : list ident. |
---|
508 | λdestrs : list register. |
---|
509 | λsrcrs1 : list rtl_argument. |
---|
510 | λsrcrs2 : list rtl_argument. |
---|
511 | λsrcrs1_prf : |destrs| = |srcrs1|. |
---|
512 | λsrcrs2_prf : |srcrs1| = |srcrs2|. |
---|
513 | (* needed fresh registers *) |
---|
514 | νa in |
---|
515 | νb in |
---|
516 | (* temporary registers for the result are created, so to avoid overwriting |
---|
517 | sources *) |
---|
518 | νν tmp_destrs × |destrs| with tmp_destrs_prf in |
---|
519 | νdummy in |
---|
520 | (* the step calculating all products with least significant byte going in the |
---|
521 | k-th position of the result *) |
---|
522 | let translate_mul_k : (Σk.k<|destrs|) → list (rtl_instruction globals) → |
---|
523 | list (rtl_instruction globals) ≝ |
---|
524 | λk_sig,acc.match k_sig with |
---|
525 | [ mk_Sig k k_prf ⇒ |
---|
526 | foldr … (translate_mul_i ? a b (|destrs|) |
---|
527 | (tmp_destrs @ [dummy]) srcrs1 srcrs2 |
---|
528 | ? srcrs1_prf srcrs2_prf k k_prf) acc (range_strong (S k)) |
---|
529 | ] in |
---|
530 | (* initializing tmp_destrs to zero |
---|
531 | dummy is intentionally uninitialized *) |
---|
532 | translate_cast_unsigned … tmp_destrs @ |
---|
533 | (* the main body, roughly: |
---|
534 | for k in 0 ... n-1 do |
---|
535 | for i in 0 ... k do |
---|
536 | translate_mul_i … k … i *) |
---|
537 | foldr … translate_mul_k [ ] (range_strong (|destrs|)) @ |
---|
538 | (* epilogue: saving the result *) |
---|
539 | translate_move … destrs (map … Reg tmp_destrs) ?. |
---|
540 | [ >length_map >tmp_destrs_prf // |
---|
541 | | >length_append <plus_n_Sm <plus_n_O // |
---|
542 | ] |
---|
543 | qed. |
---|
544 | |
---|
545 | definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→ |
---|
546 | bind_list register unit (rtl_instruction globals) ≝ |
---|
547 | λglobals: list ident. |
---|
548 | λdiv_not_mod: bool. |
---|
549 | λdestrs: list register. |
---|
550 | λsrcrs1: list rtl_argument. |
---|
551 | λsrcrs2: list rtl_argument. |
---|
552 | λsrcrs1_prf : |destrs| = |srcrs1|. |
---|
553 | λsrcrs2_prf : |srcrs1| = |srcrs2|. |
---|
554 | let return_type ≝ bind_list register unit (rtl_instruction globals) in |
---|
555 | match destrs return λx.x = destrs → return_type with |
---|
556 | [ nil ⇒ λ_.[ ] |
---|
557 | | cons destr destrs' ⇒ λeq_destrs. |
---|
558 | match destrs' with |
---|
559 | [ nil ⇒ |
---|
560 | match srcrs1 return λx.x = srcrs1 → return_type with |
---|
561 | [ nil ⇒ λeq_srcrs1.⊥ |
---|
562 | | cons srcr1 srcrs1' ⇒ λeq_srcrs1. |
---|
563 | match srcrs2 return λx.x = srcrs2 → return_type with |
---|
564 | [ nil ⇒ λeq_srcrs2.⊥ |
---|
565 | | cons srcr2 srcrs2' ⇒ λeq_srcrs2. |
---|
566 | νdummy in |
---|
567 | let 〈destr1, destr2〉 ≝ |
---|
568 | if div_not_mod then 〈destr, dummy〉 else 〈dummy, destr〉 in |
---|
569 | [❮destr1, destr2❯ ← srcr1 .DivuModu. srcr2] |
---|
570 | ] (refl …) |
---|
571 | ] (refl …) |
---|
572 | | _ ⇒ ? (* not implemented *) |
---|
573 | ] |
---|
574 | ] (refl …). |
---|
575 | [3: elim not_implemented] |
---|
576 | destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct qed. |
---|
577 | |
---|
578 | (* Paolo: to be moved elsewhere *) |
---|
579 | let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (f : A→B→C→C) (init : C) (l1 : list A) (l2 : list B) |
---|
580 | (prf : |l1| = |l2|) on l1 : C ≝ |
---|
581 | match l1 return λx.x = l1 → C with |
---|
582 | [ nil ⇒ λ_.init |
---|
583 | | cons a l1' ⇒ λeq_l1. |
---|
584 | match l2 return λy.y = l2 → C with |
---|
585 | [ nil ⇒ λeq_l2.⊥ |
---|
586 | | cons b l2' ⇒ λeq_l2. |
---|
587 | f a b (foldr2 A B C f init l1' l2' ?) |
---|
588 | ] (refl …) |
---|
589 | ] (refl …). |
---|
590 | destruct normalize in prf; [destruct|//] |
---|
591 | qed. |
---|
592 | |
---|
593 | definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝ |
---|
594 | λglobals: list ident. |
---|
595 | λdestrs: list register. |
---|
596 | λsrcrs1: list rtl_argument. |
---|
597 | λsrcrs2: list rtl_argument. |
---|
598 | λsrcrs1_prf : |destrs| = |srcrs1|. |
---|
599 | λsrcrs2_prf : |srcrs1| = |srcrs2|. |
---|
600 | let return_type ≝ bind_list register unit (rtl_instruction globals) in |
---|
601 | match destrs return λx.x = destrs → return_type with |
---|
602 | [ nil ⇒ λ_.[ ] |
---|
603 | | cons destr destrs' ⇒ λeq_destrs. |
---|
604 | match srcrs1 return λy.y = srcrs1 → return_type with |
---|
605 | [ nil ⇒ λeq_srcrs1.⊥ |
---|
606 | | cons srcr1 srcrs1' ⇒ λeq_srcrs1. |
---|
607 | match srcrs2 return λz.z = srcrs2 → return_type with |
---|
608 | [ nil ⇒ λeq_srcrs2.⊥ |
---|
609 | | cons srcr2 srcrs2' ⇒ λeq_srcrs2. |
---|
610 | νtmpr in |
---|
611 | let f : rtl_argument → rtl_argument → list (rtl_instruction globals) → list (rtl_instruction globals) ≝ |
---|
612 | λs1,s2,acc. |
---|
613 | tmpr ← s1 .Xor. s2 :: |
---|
614 | destr ← destr .Or. tmpr :: |
---|
615 | acc in |
---|
616 | let epilogue : list (rtl_instruction globals) ≝ |
---|
617 | [ clear_carry … ; |
---|
618 | tmpr ← 0 .Sub. destr ; |
---|
619 | (* now carry bit is 1 iff destrs != 0 *) |
---|
620 | destr ← 0 .Addc. 0 ] in |
---|
621 | translate_cast_unsigned … destrs' @ |
---|
622 | destr ← srcr1 .Xor. srcr2 :: |
---|
623 | foldr2 ??? f epilogue srcrs1' srcrs2' ? |
---|
624 | ] (refl …) |
---|
625 | ] (refl …) |
---|
626 | ] (refl …). |
---|
627 | destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct // qed. |
---|
628 | |
---|
629 | (* if destrs is 0 or 1, it inverses it. To be used after operations that |
---|
630 | ensure this. *) |
---|
631 | definition translate_toggle_bool : ∀globals.?→list (rtl_instruction globals) ≝ |
---|
632 | λglobals: list ident. |
---|
633 | λdestrs: list register. |
---|
634 | match destrs with |
---|
635 | [ nil ⇒ [ ] |
---|
636 | | cons destr _ ⇒ [destr ← .Cmpl. destr] |
---|
637 | ]. |
---|
638 | |
---|
639 | definition translate_lt_unsigned : |
---|
640 | ∀globals. |
---|
641 | ∀destrs: list register. |
---|
642 | ∀srcrs1: list rtl_argument. |
---|
643 | ∀srcrs2: list rtl_argument. |
---|
644 | |destrs| = |srcrs1| → |
---|
645 | |srcrs1| = |srcrs2| → |
---|
646 | list (rtl_instruction globals) ≝ |
---|
647 | λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf. |
---|
648 | match destrs with |
---|
649 | [ nil ⇒ [ ] |
---|
650 | | cons destr destrs' ⇒ |
---|
651 | translate_cast_unsigned … destrs' @ |
---|
652 | (* I perform a subtraction, but the only interest is in the carry bit *) |
---|
653 | translate_op ? Sub (make … destr (|destrs|)) srcrs1 srcrs2 ?? @ |
---|
654 | [ destr ← 0 .Addc. 0 ] |
---|
655 | ]. |
---|
656 | [ <make_length ] assumption qed. |
---|
657 | |
---|
658 | (* shifts signed integers by adding 128 to the most significant byte |
---|
659 | it replaces it with a fresh register which must be provided *) |
---|
660 | let rec shift_signed globals |
---|
661 | (tmp : register) |
---|
662 | (srcrs : list rtl_argument) on srcrs : |
---|
663 | (list rtl_argument) × (list (rtl_instruction globals)) ≝ |
---|
664 | match srcrs with |
---|
665 | [ nil ⇒ 〈[ ],[ ]〉 |
---|
666 | | cons srcr srcrs' ⇒ |
---|
667 | match srcrs' with |
---|
668 | [ nil ⇒ 〈[ Reg tmp ], [ tmp ← srcr .Add. 128 ]〉 |
---|
669 | | _ ⇒ |
---|
670 | let 〈new_srcrs', op〉 ≝ shift_signed globals tmp srcrs' in |
---|
671 | 〈srcr :: new_srcrs', op〉 |
---|
672 | ] |
---|
673 | ]. |
---|
674 | |
---|
675 | lemma shift_signed_length : ∀globals,tmp,srcrs. |
---|
676 | |\fst (shift_signed globals tmp srcrs)| = |srcrs|. |
---|
677 | #globals #tmp #srcrs elim srcrs [//] |
---|
678 | #srcr * [//] |
---|
679 | #srcr' #srcrs'' #Hi |
---|
680 | whd in ⊢ (??(??(???%))?); |
---|
681 | @pair_elim #new_srcrs' #op #EQ >EQ in Hi; |
---|
682 | normalize #Hi >Hi // |
---|
683 | qed. |
---|
684 | |
---|
685 | definition translate_lt_signed : |
---|
686 | ∀globals. |
---|
687 | ∀destrs: list register. |
---|
688 | ∀srcrs1: list rtl_argument. |
---|
689 | ∀srcrs2: list rtl_argument. |
---|
690 | |destrs| = |srcrs1| → |
---|
691 | |srcrs1| = |srcrs2| → |
---|
692 | bind_list register unit (rtl_instruction globals) ≝ |
---|
693 | λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf. |
---|
694 | νtmp_last_s1 in |
---|
695 | νtmp_last_s2 in |
---|
696 | let p1 ≝ shift_signed globals tmp_last_s1 srcrs1 in |
---|
697 | let new_srcrs1 ≝ \fst p1 in |
---|
698 | let shift_srcrs1 ≝ \snd p1 in |
---|
699 | let p2 ≝ shift_signed globals tmp_last_s2 srcrs2 in |
---|
700 | let new_srcrs2 ≝ \fst p2 in |
---|
701 | let shift_srcrs2 ≝ \snd p2 in |
---|
702 | shift_srcrs1 @ shift_srcrs2 @ |
---|
703 | translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2 ??. |
---|
704 | >shift_signed_length [2: >shift_signed_length] assumption qed. |
---|
705 | |
---|
706 | definition translate_lt : bool→∀globals.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝ |
---|
707 | λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf. |
---|
708 | if is_unsigned then |
---|
709 | translate_lt_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
710 | else |
---|
711 | translate_lt_signed globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf. |
---|
712 | |
---|
713 | definition translate_cmp ≝ |
---|
714 | λis_unsigned,globals,cmp,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf. |
---|
715 | match cmp with |
---|
716 | [ Ceq ⇒ |
---|
717 | translate_ne globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf @ |
---|
718 | translate_toggle_bool globals destrs |
---|
719 | | Cne ⇒ |
---|
720 | translate_ne globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
721 | | Clt ⇒ |
---|
722 | translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
723 | | Cgt ⇒ |
---|
724 | translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? ? |
---|
725 | | Cle ⇒ |
---|
726 | translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? ? @ |
---|
727 | translate_toggle_bool globals destrs |
---|
728 | | Cge ⇒ |
---|
729 | translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf @ |
---|
730 | translate_toggle_bool globals destrs |
---|
731 | ]. |
---|
732 | // qed. |
---|
733 | |
---|
734 | definition translate_op2 : |
---|
735 | ∀globals.?→?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝ |
---|
736 | λglobals: list ident. |
---|
737 | λop2. |
---|
738 | λdestrs: list register. |
---|
739 | λsrcrs1: list rtl_argument. |
---|
740 | λsrcrs2: list rtl_argument. |
---|
741 | λsrcrs1_prf: |destrs| = |srcrs1|. |
---|
742 | λsrcrs2_prf: |srcrs1| = |srcrs2|. |
---|
743 | match op2 with |
---|
744 | [ Oadd ⇒ |
---|
745 | translate_op globals Add destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
746 | | Oaddp ⇒ |
---|
747 | translate_op globals Add destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
748 | | Osub ⇒ |
---|
749 | translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
750 | | Osubpi ⇒ |
---|
751 | translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
752 | | Osubpp _ ⇒ |
---|
753 | translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
754 | | Omul ⇒ |
---|
755 | translate_mul globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
756 | | Odivu ⇒ |
---|
757 | translate_divumodu8 globals true destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
758 | | Omodu ⇒ |
---|
759 | translate_divumodu8 globals false destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
760 | | Oand ⇒ |
---|
761 | translate_op globals And destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
762 | | Oor ⇒ |
---|
763 | translate_op globals Or destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
764 | | Oxor ⇒ |
---|
765 | translate_op globals Xor destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
766 | | Ocmp c ⇒ |
---|
767 | translate_cmp false globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
768 | | Ocmpu c ⇒ |
---|
769 | translate_cmp true globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
770 | | Ocmpp c ⇒ |
---|
771 | translate_cmp true globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf |
---|
772 | | _ ⇒ ? (* assert false, implemented in run time or float op *) |
---|
773 | ]. |
---|
774 | cases not_implemented (* XXX: yes, really *) qed. |
---|
775 | |
---|
776 | definition translate_cond: ∀globals: list ident. list register → label → bind_list register unit (rtl_instruction globals) ≝ |
---|
777 | λglobals: list ident. |
---|
778 | λsrcrs: list register. |
---|
779 | λlbl_true: label. |
---|
780 | match srcrs with |
---|
781 | [ nil ⇒ [ ] |
---|
782 | | cons srcr srcrs' ⇒ |
---|
783 | ν tmpr in |
---|
784 | let f ≝ λr. OP2 rtl_params globals Or tmpr (Reg tmpr) (Reg r) in |
---|
785 | reg_from_reg globals tmpr srcr :: |
---|
786 | map … f srcrs' @ |
---|
787 | [ COND … tmpr lbl_true ] |
---|
788 | ]. |
---|
789 | |
---|
790 | (* Paolo: to be controlled (original seemed overly complex) *) |
---|
791 | definition translate_load ≝ |
---|
792 | λglobals: list ident. |
---|
793 | λaddr : list rtl_argument. |
---|
794 | λaddr_prf: 2 = |addr|. |
---|
795 | λdestrs: list register. |
---|
796 | ν tmp_addr_l in |
---|
797 | ν tmp_addr_h in |
---|
798 | let f ≝ λdestr : register.λacc : list (rtl_instruction globals). |
---|
799 | LOAD rtl_params globals destr (Reg tmp_addr_l) (Reg tmp_addr_h) :: |
---|
800 | translate_op … Add |
---|
801 | [tmp_addr_l ; tmp_addr_h] |
---|
802 | [Reg tmp_addr_l ; Reg tmp_addr_h] |
---|
803 | [imm_nat 0 ; Imm int_size] ? ? @ acc in |
---|
804 | translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @ |
---|
805 | foldr … f [ ] destrs. |
---|
806 | [1: <addr_prf] // qed. |
---|
807 | |
---|
808 | definition translate_store ≝ |
---|
809 | λglobals: list ident. |
---|
810 | λaddr : list rtl_argument. |
---|
811 | λaddr_prf: 2 = |addr|. |
---|
812 | λsrcrs: list rtl_argument. |
---|
813 | ν tmp_addr_l in |
---|
814 | ν tmp_addr_h in |
---|
815 | let f ≝ λsrcr : rtl_argument.λacc : list (rtl_instruction globals). |
---|
816 | STORE rtl_params globals (Reg tmp_addr_l) (Reg tmp_addr_h) srcr :: |
---|
817 | translate_op … Add |
---|
818 | [tmp_addr_l ; tmp_addr_h] |
---|
819 | [Reg tmp_addr_l ; Reg tmp_addr_h] |
---|
820 | [imm_nat 0 ; Imm int_size] ? ? @ acc in |
---|
821 | translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @ |
---|
822 | foldr … f [ ] srcrs. |
---|
823 | [1: <addr_prf] // qed. |
---|
824 | |
---|
825 | (* alias for b_adds_graph *) |
---|
826 | definition rtl_adds_graph ≝ |
---|
827 | λglobals.b_adds_graph rtl_params globals register unit |
---|
828 | (rtl_ertl_fresh_reg rtl_params rtl_params globals). |
---|
829 | |
---|
830 | axiom fake_label: label. |
---|
831 | |
---|
832 | definition stmt_not_return ≝ λstmt.match stmt with |
---|
833 | [ St_return ⇒ False |
---|
834 | | _ ⇒ True ]. |
---|
835 | |
---|
836 | (* XXX: following conversation with CSC about the mix up in extension statements |
---|
837 | and extension instructions in RTL, use fake_label in calls to |
---|
838 | tailcall_* instructions. *) |
---|
839 | definition translate_inst : ∀globals.?→?→?→ |
---|
840 | Prod (bind_list register unit (rtl_instruction globals)) label ≝ |
---|
841 | λglobals: list ident. |
---|
842 | λlenv: local_env. |
---|
843 | λstmt. |
---|
844 | λstmt_prf : stmt_not_return stmt. |
---|
845 | match stmt return λx.stmt = x → |
---|
846 | (bind_list register unit (rtl_instruction globals)) × label with |
---|
847 | [ St_skip lbl' ⇒ λ_. |
---|
848 | 〈[ ], lbl'〉 |
---|
849 | | St_cost cost_lbl lbl' ⇒ λ_. |
---|
850 | 〈[COST_LABEL … cost_lbl], lbl'〉 |
---|
851 | | St_const destr cst lbl' ⇒ λ_. |
---|
852 | 〈translate_cst globals cst (find_local_env destr lenv) ?, lbl'〉 |
---|
853 | | St_op1 ty ty' op1 destr srcr lbl' ⇒ λ_. |
---|
854 | 〈translate_op1 globals ty' ty op1 |
---|
855 | (find_local_env destr lenv) |
---|
856 | (find_local_env srcr lenv) ??, lbl'〉 |
---|
857 | | St_op2 op2 destr srcr1 srcr2 lbl' ⇒ λ_. |
---|
858 | 〈translate_op2 globals op2 |
---|
859 | (find_local_env destr lenv) |
---|
860 | (find_local_env_arg srcr1 lenv) |
---|
861 | (find_local_env_arg srcr2 lenv) ??, lbl'〉 |
---|
862 | (* XXX: should we be ignoring this? *) |
---|
863 | | St_load ignore addr destr lbl' ⇒ λ_. |
---|
864 | 〈translate_load globals |
---|
865 | (find_local_env_arg addr lenv) ? (find_local_env destr lenv), lbl'〉 |
---|
866 | (* XXX: should we be ignoring this? *) |
---|
867 | | St_store ignore addr srcr lbl' ⇒ λ_. |
---|
868 | 〈translate_store globals (find_local_env_arg addr lenv) ? |
---|
869 | (find_local_env_arg srcr lenv), lbl'〉 |
---|
870 | | St_call_id f args retr lbl' ⇒ λ_. |
---|
871 | (* Paolo: no notation to avoid ambiguity *) |
---|
872 | 〈bcons … ( |
---|
873 | match retr with |
---|
874 | [ Some retr ⇒ |
---|
875 | CALL_ID rtl_params globals f (rtl_args args lenv) (find_local_env retr lenv) |
---|
876 | | None ⇒ |
---|
877 | CALL_ID … f (rtl_args args lenv) [ ] |
---|
878 | ]) [ ], lbl'〉 |
---|
879 | | St_call_ptr f args retr lbl' ⇒ λ_. |
---|
880 | let 〈f1, f2〉 ≝ find_and_addr f lenv ? in |
---|
881 | (* Paolo: no notation to avoid ambiguity *) |
---|
882 | 〈bcons … ( |
---|
883 | match retr with |
---|
884 | [ Some retr ⇒ |
---|
885 | extension rtl_params globals (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv)) |
---|
886 | | None ⇒ |
---|
887 | extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ]) |
---|
888 | ]) [ ], lbl'〉 |
---|
889 | | St_tailcall_id f args ⇒ λ_. |
---|
890 | 〈[extension rtl_params globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))], fake_label〉 |
---|
891 | | St_tailcall_ptr f args ⇒ λ_. |
---|
892 | let 〈f1, f2〉 ≝ find_and_addr f lenv ? in |
---|
893 | 〈bcons … (extension rtl_params globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) [ ], fake_label〉 |
---|
894 | | St_cond r lbl_true lbl_false ⇒ λ_. |
---|
895 | 〈translate_cond globals (find_local_env r lenv) lbl_true, lbl_false〉 |
---|
896 | | St_jumptable r l ⇒ λ_.? (* assert false: not implemented yet *) |
---|
897 | | St_return ⇒ λeq_stmt.⊥ |
---|
898 | ] (refl …). |
---|
899 | [11: cases not_implemented (* jtable case *) |
---|
900 | |12: >eq_stmt in stmt_prf; normalize // |
---|
901 | |*: cases daemon |
---|
902 | (* TODO: proofs regarding lengths of lists, examine! *) |
---|
903 | (* Paolo: probably hypotheses need to be added *) |
---|
904 | ] |
---|
905 | qed. |
---|
906 | |
---|
907 | definition translate_stmt ≝ |
---|
908 | λglobals,lenv,lbl,stmt,def. |
---|
909 | match stmt return λx.stmt = x → rtl_internal_function globals with |
---|
910 | [ St_return ⇒ λ_.add_graph rtl_params globals lbl (RETURN …) def |
---|
911 | | _ ⇒ λstmt_eq. |
---|
912 | let 〈translation, lbl'〉 ≝ translate_inst globals lenv stmt ? in |
---|
913 | rtl_adds_graph globals translation lbl lbl' def |
---|
914 | ] (refl …). |
---|
915 | >stmt_eq normalize % qed. |
---|
916 | |
---|
917 | |
---|
918 | (* XXX: we use a "hack" here to circumvent the proof obligations required to |
---|
919 | create res, an empty internal_function record. we insert into our graph |
---|
920 | the start and end nodes to ensure that they are in, and place dummy |
---|
921 | skip instructions at these nodes. *) |
---|
922 | definition translate_internal ≝ |
---|
923 | λglobals: list ident. |
---|
924 | λdef. |
---|
925 | let runiverse ≝ f_reggen def in |
---|
926 | let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse |
---|
927 | (f_params def @ f_locals def) (f_result def) in |
---|
928 | let params ≝ map_list_local_env lenv (map … \fst (f_params def)) in |
---|
929 | let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in |
---|
930 | let result ≝ |
---|
931 | match (f_result def) with |
---|
932 | [ None ⇒ [ ] |
---|
933 | | Some r_typ ⇒ |
---|
934 | let 〈r, typ〉 ≝ r_typ in |
---|
935 | find_local_env r lenv |
---|
936 | ] |
---|
937 | in |
---|
938 | let luniverse' ≝ f_labgen def in |
---|
939 | let runiverse' ≝ runiverse in |
---|
940 | let result' ≝ result in |
---|
941 | let params' ≝ params in |
---|
942 | let locals' ≝ locals in |
---|
943 | let stack_size' ≝ f_stacksize def in |
---|
944 | let entry' ≝ f_entry def in |
---|
945 | let exit' ≝ f_exit def in |
---|
946 | let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params globals entry') in |
---|
947 | let graph' ≝ add LabelTag ? graph' exit' (RETURN rtl_params globals) in |
---|
948 | let res ≝ |
---|
949 | mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params' |
---|
950 | locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in |
---|
951 | foldi … (translate_stmt globals … lenv) (f_graph def) res. |
---|
952 | [ @graph_add_lookup @graph_add |
---|
953 | | @graph_add ] |
---|
954 | qed. |
---|
955 | |
---|
956 | (*CSC: here we are not doing any alignment on variables, like it is done in OCaml |
---|
957 | because of CompCert heritage *) |
---|
958 | definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝ |
---|
959 | λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))). |
---|