source: src/RTLabs/RTLabsToRTL.ma @ 1343

Last change on this file since 1343 was 1343, checked in by mulligan, 8 years ago

fixed some bugs in the translation

File size: 44.8 KB
Line 
1include "RTLabs/syntax.ma".
2include "RTL/RTL.ma".
3include "common/AssocList.ma".
4include "common/FrontEndOps.ma".
5include "common/Graphs.ma".
6include "joint/TranslateUtils.ma".
7
8let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
9  match n with
10  [ O ⇒ 〈[],runiverse〉
11  | S n' ⇒
12     let 〈r,runiverse〉 ≝ fresh … runiverse in
13     let 〈res,runiverse〉 ≝ register_freshes runiverse n' in
14      〈r::res,runiverse〉 ].
15
16definition complete_regs ≝
17  λglobals.
18  λdef.
19  λsrcrs1.
20  λsrcrs2.
21  if leb (length … srcrs2) (length … srcrs1) then
22   let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs1) (length ? srcrs2)) in
23    〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
24  else
25   let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs2) (length ? srcrs1)) in
26    〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
27
28lemma complete_regs_length:
29  ∀globals,def,left,right.
30   |\fst (\fst (complete_regs globals def left right))| = |\snd (\fst (complete_regs globals def left right))|.
31 #globals #def #left #right
32 whd in match complete_regs normalize nodelta
33 @leb_elim normalize nodelta #H
34 [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right)))
35 | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)))]
36 cases (fresh_regs ????) #def' #fresh normalize >append_length
37 generalize in match H -H;
38 generalize in match (length … left) generalize in match (length … right) generalize in match (length … fresh)
39 [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H) -H #H #E >E >commutative_plus
40         <plus_minus_m_m /2/ ]
41qed.
42
43definition size_of_sig_type ≝
44  λsig.
45  match sig with
46  [ ASTint isize sign ⇒
47    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
48      isize' ÷ (nat_of_bitvector ? int_size)
49  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
50  | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
51  ].
52  cases not_implemented;
53qed.
54
55inductive register_type: Type[0] ≝
56  | register_int: register → register_type
57  | register_ptr: register → register → register_type.
58
59definition local_env ≝ BitVectorTrie (list register) 16.
60
61definition mem_local_env : register → local_env → bool ≝
62  λr. member … (word_of_identifier … r).
63
64definition add_local_env : register → list register → local_env → local_env ≝
65  λr. insert … (word_of_identifier … r).
66
67definition find_local_env : register → local_env → list register ≝
68  λr: register.λbvt. lookup … (word_of_identifier … r) bvt [].
69
70definition initialize_local_env_internal ≝
71  λlenv_runiverse.
72  λr_sig.
73  let 〈lenv,runiverse〉 ≝ lenv_runiverse in
74  let 〈r, sig〉 ≝ r_sig in
75  let size ≝ size_of_sig_type sig in
76  let 〈rs,runiverse〉 ≝ register_freshes runiverse size in
77    〈add_local_env r rs lenv,runiverse〉.
78
79definition initialize_local_env ≝
80  λruniverse.
81  λregisters.
82  λresult.
83  let registers ≝ registers @
84    match result with
85    [ None ⇒ [ ]
86    | Some rt ⇒ [ rt ]
87    ]
88  in
89    foldl ? ? initialize_local_env_internal 〈Stub …,runiverse〉 registers.
90
91definition map_list_local_env_internal ≝
92  λlenv,res,r. res @ (find_local_env r lenv).
93   
94definition map_list_local_env ≝
95  λlenv,regs. foldl … (map_list_local_env_internal lenv) [ ] regs.
96
97definition make_addr ≝
98  λA.
99  λlst: list A.
100  λprf: 2 = length A lst.
101  match lst return λx. 2 = |x| → A × A with
102  [ nil ⇒ λlst_nil_prf. ?
103  | cons hd tl ⇒ λprf.
104    match tl return λx. 1 = |x| → A × A with
105    [ nil ⇒ λtl_nil_prf. ?
106    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
107    ] ?
108  ] prf.
109  [1: normalize in lst_nil_prf;
110      destruct(lst_nil_prf)
111  |2: normalize in prf;
112      @injective_S
113      assumption
114  |3: normalize in tl_nil_prf;
115      destruct(tl_nil_prf)
116  ]
117qed.
118
119definition find_and_addr ≝
120  λr,lenv. make_addr ? (find_local_env r lenv).
121
122definition rtl_args ≝
123  λregs_list,lenv. flatten … (map … (λr. find_local_env r lenv) regs_list).
124
125definition translate_cst_int_internal ≝
126  λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl.
127
128axiom split_into_bytes:
129  ∀size.
130  ∀int: bvint size.
131    Σbytes: list Byte. |bytes| = size_intsize size.
132
133lemma eqb_implies_eq:
134  ∀m, n: nat.
135    eqb m n = true → m = n.
136  #M
137  elim M
138  [1: #N normalize
139      cases N
140      [1: normalize //
141      |2: #M' normalize #HYP destruct(HYP)
142      ]
143  |2: #M' #IND_HYP #N
144      normalize
145      cases N
146      [1: normalize #HYP destruct(HYP)
147      |2: #M'' normalize #HYP
148          @eq_f @(IND_HYP M'')
149          assumption
150      ]
151   ]
152qed.
153
154definition translate_op: ∀globals. ? → list register → list register → list register →
155  label → label → rtl_internal_function globals → rtl_internal_function globals ≝
156  λglobals: list ident.
157  λop.
158  λdestrs: list register.
159  λsrcrs1: list register.
160  λsrcrs2: list register.
161  λstart_lbl: label.
162  λdest_lbl: label.
163  λdef: rtl_internal_function globals.
164  match reduce_strong register register srcrs1 srcrs2 with
165  [ dp reduced first_reduced_proof ⇒
166    let srcrsl_common ≝ \fst (\fst reduced) in
167    let srcrsr_common ≝ \fst (\snd reduced) in
168    let srcrsl_rest ≝ \snd (\fst reduced) in
169    let srcrsr_rest ≝ \snd (\snd reduced) in
170    let srcrs_rest ≝ srcrsl_rest @ srcrsr_rest in
171    match reduce_strong register register destrs srcrsl_common with
172    [ dp reduced second_reduced_proof ⇒
173      let destrs_common ≝ \fst (\fst reduced) in
174      let destrs_rest ≝ \snd (\fst reduced) in
175      match reduce_strong register register destrs_rest srcrs_rest with
176      [ dp reduced third_reduced_proof ⇒
177        let destrs_cted ≝ \fst (\fst reduced) in
178        let destrs_rest ≝ \snd (\fst reduced) in
179        let srcrs_cted ≝ \fst (\snd reduced) in
180        let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
181        let insts_init ≝ [
182          sequential … (CLEAR_CARRY …);
183          sequential … (INT rtl_params_ globals tmpr (zero …))
184        ] in
185        let f_add ≝ λdestr. λsrcr1. λsrcr2. sequential … (OP2 rtl_params_ globals op destr srcr1 srcr2) in
186        let insts_add ≝ map3 ? ? ? ? f_add destrs_common srcrsl_common srcrsr_common ? ? in
187        let f_add_cted ≝ λdestr. λsrcr. sequential … (OP2 rtl_params_ globals op destr srcr tmpr) in
188        let insts_add_cted ≝ map2 … f_add_cted destrs_cted srcrs_cted ? in
189        let f_rest ≝ λdestr. sequential … (OP2 rtl_params_ globals op destr tmpr tmpr) in
190        let insts_rest ≝ map … f_rest destrs_rest in
191          adds_graph rtl_params1 globals (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
192      ]
193    ]
194  ].
195  [1: @third_reduced_proof
196  |3: @first_reduced_proof
197  |*: cases daemon (* XXX: some of these look like they may be false *)
198  ]
199qed.
200
201let rec translate_cst
202  (globals: list ident) (cst: constant) (destrs: list register)
203    (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals)
204      on cst: rtl_internal_function globals ≝
205  match cst with
206  [ Ointconst size const ⇒
207    match destrs with
208    [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
209    | _   ⇒
210      let size' ≝ size_intsize size in
211        match eqb size' (|destrs|) return λx. (eqb size' (|destrs|)) = x → rtl_internal_function globals with
212        [ true  ⇒ λgood_case.
213          match split_into_bytes size const with
214          [ dp bytes bytes_length_proof ⇒
215            let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in
216              adds_graph rtl_params1 globals mapped start_lbl dest_lbl def
217          ]
218        | false ⇒ λbad_case. ?
219        ] (refl … (eqb size' (|destrs|)))
220    ]
221  | Ofloatconst float ⇒ ⊥
222  | Oaddrsymbol id offset ⇒
223    let 〈r1, r2〉 ≝ make_addr … destrs ? in
224    let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def in
225    let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in
226      def
227  | Oaddrstack offset ⇒
228    let 〈r1, r2〉 ≝ make_addr … destrs ? in
229    let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (extension rtl_params_ globals (rtl_st_ext_stack_address r1 r2)) dest_lbl) def in
230    let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in
231      def
232  ].
233  [1: >bytes_length_proof
234      cut(size' = |destrs|)
235      [1: @eqb_implies_eq
236          assumption
237      |2: #EQ_HYP
238          <EQ_HYP %
239      ]
240  |2: cases daemon (* XXX: bad case where destrs is of the wrong length *)
241  |3: cases not_implemented (* XXX: float, error_float in o'caml *)
242  |*: cases daemon (* XXX: various proofs to be filled in *)
243  ].
244qed.
245 
246definition translate_move_internal ≝
247  λglobals.
248  λdestr: register.
249  λsrcr: register.
250    sequential rtl_params_ globals (MOVE … 〈destr,srcr〉).
251
252definition translate_move ≝
253  λglobals.
254  λdestrs: list register.
255  λsrcrs: list register.
256  λstart_lbl: label.
257    match reduce_strong register register destrs srcrs with
258    [ dp crl_crr len_proof ⇒
259      let commonl ≝ \fst (\fst crl_crr) in
260      let commonr ≝ \fst (\snd crl_crr) in
261      let restl ≝ \snd (\fst crl_crr) in
262      let restr ≝ \snd (\snd crl_crr) in
263      let f_common ≝ translate_move_internal globals in
264      let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in
265      let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
266        add_translates … [ translate1 ; translate2 ] start_lbl
267    ].
268    @len_proof
269qed.
270
271let rec make
272  (A: Type[0]) (elt: A) (n: nat) on n ≝
273  match n with
274  [ O ⇒ [ ]
275  | S n' ⇒ elt :: make A elt n'
276  ].
277 
278lemma make_length:
279  ∀A: Type[0].
280  ∀elt: A.
281  ∀n: nat.
282    n = length ? (make A elt n).
283  #A #ELT #N
284  elim N
285  [ normalize %
286  | #N #IH
287    normalize <IH %
288  ]
289qed.
290
291definition translate_cast_unsigned ≝
292  λglobals.
293  λdestrs.
294  λstart_lbl.
295  λdest_lbl.
296  λdef: joint_internal_function … (rtl_params globals).
297  let 〈def, tmp_zero〉 ≝ fresh_reg … def in
298  let zeros ≝ make … tmp_zero (length … destrs) in
299    add_translates … [
300      adds_graph rtl_params1 … [
301        sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0))
302        ];
303      translate_move globals destrs zeros
304    ] start_lbl dest_lbl def.
305
306definition translate_cast_signed:
307    ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
308  λglobals: list ident.
309  λdestrs.
310  λsrcr.
311  λstart_lbl.
312  λdest_lbl.
313  λdef.
314  let 〈def, tmp_128〉 ≝ fresh_reg … def in
315  let 〈def, tmp_255〉 ≝ fresh_reg … def in
316  let 〈def, tmpr〉 ≝ fresh_reg … def in
317  let 〈def, dummy〉 ≝ fresh_reg … def in
318  let insts ≝ [
319    sequential  … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128));
320    sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr);
321    sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128);
322    sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255));
323    sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255)
324  ]
325  in
326  let srcrs ≝ make … tmpr (length … destrs) in
327    add_translates rtl_params1 globals [
328      adds_graph rtl_params1 globals insts;
329      translate_move globals destrs srcrs
330    ] start_lbl dest_lbl def.
331
332definition translate_cast ≝
333  λglobals: list ident.
334  λsrc_size: nat.
335  λsrc_sign: signedness.
336  λdest_size: nat.
337  λdestrs: list register.
338  λsrcrs: list register.
339  match |srcrs| return λx. |srcrs| = x → ? with
340  [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ]
341  | S n' ⇒ λsucc_prf.
342    if ltb dest_size src_size then
343      translate_move globals destrs srcrs
344    else
345      match reduce_strong register register destrs srcrs with
346      [ dp crl len_proof ⇒
347        let commonl ≝ \fst (\fst crl) in
348        let commonr ≝ \fst (\snd crl) in
349        let restl ≝ \snd (\fst crl) in
350        let restr ≝ \snd (\snd crl) in
351        let insts_common ≝ translate_move globals commonl commonr in
352        let sign_reg ≝ last_safe ? srcrs ? in
353        let insts_sign ≝
354          match src_sign with
355          [ Unsigned ⇒ translate_cast_unsigned globals restl
356          | Signed ⇒ translate_cast_signed globals restl sign_reg
357          ]
358        in
359          add_translates rtl_params1 globals [ insts_common; insts_sign ]
360      ]
361  ] (refl ? (|srcrs|)).
362  >succ_prf //
363qed.
364
365definition translate_negint ≝
366  λglobals: list ident.
367  λdestrs: list register.
368  λsrcrs: list register.
369  λstart_lbl: label.
370  λdest_lbl: label.
371  λdef: rtl_internal_function globals.
372  λprf: |destrs| = |srcrs|. (* assert in caml code *)
373  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
374  let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in
375  let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in
376  let insts_init ≝ [
377    sequential … (SET_CARRY …);
378    sequential … (INT rtl_params_ globals tmpr (zero ?))
379  ] in
380  let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in
381  let insts_add ≝ map … f_add destrs in
382    adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
383
384definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
385  λglobals: list ident.
386  λdestrs: list register.
387  λsrcrs: list register.
388  λstart_lbl: label.
389  λdest_lbl: label.
390  λdef: rtl_internal_function globals.
391  match destrs with
392  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def
393  | cons destr destrs ⇒
394    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
395    let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in
396    let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in
397    let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in
398    let f ≝ λtmp_srcr. [
399      sequential … (CLEAR_CARRY rtl_params_ globals);
400      sequential … (INT rtl_params_ globals tmpr (zero ?));
401      sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr);
402      sequential … (INT rtl_params_ globals tmpr (zero ?));
403      sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr);
404      sequential … (OP2 rtl_params_ globals Xor destr destr tmpr)
405    ] in
406    let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in
407    let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
408      add_translates rtl_params1 globals [
409        save_srcrs; adds_graph rtl_params1 globals insts; epilogue
410      ] start_lbl dest_lbl def
411  ].
412
413(* TODO: examine this properly.  This is a change from the O'caml code due
414   to us dropping the explicit use of a cast destination size field.  We
415   instead infer the size of the cast's destination from the context.  Is
416   this correct?
417*)
418definition translate_op1 ≝
419  λglobals: list ident.
420  λop1: unary_operation.
421  λdestrs: list register.
422  λsrcrs: list register.
423  λprf: |destrs| = |srcrs|.
424  λstart_lbl: label.
425  λdest_lbl: label.
426  λdef: rtl_internal_function globals.
427  match op1 with
428  [ Ocastint src_sign src_size ⇒
429    let dest_size ≝ |destrs| * 8 in
430    let src_size ≝ bitsize_of_intsize src_size in
431      translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
432  | Onegint ⇒
433      translate_negint globals destrs srcrs start_lbl dest_lbl def prf
434  | Onotbool ⇒
435      translate_notbool globals destrs srcrs start_lbl dest_lbl def
436  | Onotint ⇒
437    let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in
438    let l ≝ map2 … f destrs srcrs prf in
439      adds_graph rtl_params1 globals l start_lbl dest_lbl def
440  | Optrofint r ⇒
441      translate_move globals destrs srcrs start_lbl dest_lbl def
442  | Ointofptr r ⇒
443      translate_move globals destrs srcrs start_lbl dest_lbl def
444  | Oid ⇒
445      translate_move globals destrs srcrs start_lbl dest_lbl def
446  | _ ⇒ ? (* float operations implemented in runtime *)
447  ].
448  cases not_implemented
449qed.
450
451let rec translate_mul1
452  (globals: list ident) (dummy: register) (tmpr: register)
453    (destrs: list register) (srcrs1: list register) (srcr2: register)
454      (start_lbl: label)
455        on srcrs1 ≝
456  match destrs with
457  [ nil ⇒ adds_graph rtl_params1 globals [ GOTO … ] start_lbl
458  | cons destr tl ⇒
459    match tl with
460    [ nil ⇒
461      match srcrs1 with
462      [ nil ⇒
463        adds_graph rtl_params1 globals [
464          sequential … (INT rtl_params_ globals tmpr (zero …));
465          sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
466        ] start_lbl
467      | cons srcr1 tl' ⇒
468        adds_graph rtl_params1 globals [
469          sequential … (OPACCS rtl_params_ globals Mul tmpr dummy srcr2 srcr1);
470          sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
471        ] start_lbl
472      ]
473    | cons destr2 destrs ⇒
474      match srcrs1 with
475      [ nil ⇒
476        add_translates rtl_params1 globals [
477          adds_graph rtl_params1 globals [
478            sequential … (INT rtl_params_ globals tmpr (zero …));
479            sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
480            sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
481          ];
482          translate_cst globals (Ointconst I8 (zero …)) destrs
483        ] start_lbl
484      | cons srcr1 srcrs1 ⇒
485        match destrs with
486        [ nil ⇒
487          add_translates rtl_params1 globals [
488            adds_graph rtl_params1 globals [
489              sequential … (INT rtl_params_ globals tmpr (zero …));
490              sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
491              sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
492            ];
493            translate_cst globals (Ointconst I8 (zero ?)) destrs
494          ] start_lbl
495        | cons destr2 destrs ⇒
496          add_translates rtl_params1 globals [
497            adds_graph rtl_params1 globals [
498              sequential … (OPACCS rtl_params_ globals Mul tmpr destr2 srcr2 srcr1);
499              sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
500            ];
501            translate_mul1 globals dummy tmpr (destr2 :: destrs) srcrs1 srcr2
502          ] start_lbl
503        ]
504      ]
505    ]
506  ].
507
508definition translate_muli ≝
509  λglobals: list ident.
510  λdummy: register.
511  λtmpr: register.
512  λdestrs: list register.
513  λtmp_destrs: list register.
514  λsrcrs1: list register.
515  λdummy_lbl: label.
516  λi: nat.
517  λi_prf: i ≤ |tmp_destrs|.
518  λtranslates: list ?.
519  λsrcr2i: register.
520  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split … tmp_destrs i i_prf in
521  let tmp_destrs2' ≝
522    match tmp_destrs2 with
523    [ nil ⇒ [ ]
524    | cons tmp_destr2 tmp_destrs2 ⇒ [
525        adds_graph rtl_params1 globals [
526          sequential rtl_params_ globals (CLEAR_CARRY …);
527          sequential … (INT rtl_params_ globals tmp_destr2 (zero …))
528        ];
529        translate_mul1 globals dummy tmpr tmp_destrs2 srcrs1 srcr2i;
530        translate_cst globals (Ointconst I8 (zero …)) tmp_destrs1;
531        adds_graph rtl_params1 globals [
532          sequential rtl_params_ globals (CLEAR_CARRY …)
533        ];
534        translate_op globals Addc destrs destrs tmp_destrs
535      ]
536    ]
537  in
538    translates @ tmp_destrs2'.
539 
540axiom foldi_strong:
541  ∀a: Type[0].
542  ∀b: Type[0].
543  ∀the_list: list b.
544  ∀f: (∀i: nat. ∀proof: i ≤ |the_list|. a → b → a).
545  ∀seed: a.
546    a.
547 
548definition translate_mul ≝
549  λglobals: list ident.
550  λdestrs: list register.
551  λsrcrs1: list register.
552  λsrcrs2: list register.
553  λregs_proof: |destrs| = |srcrs2|.
554  λstart_lbl: label.
555  λdest_lbl: label.
556  λdef: rtl_internal_function globals.
557  let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
558  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
559    match fresh_regs_strong rtl_params0 globals def (|destrs|) with
560    [ dp def_tmp_destrs tmp_destrs_prf ⇒
561      let def ≝ \fst def_tmp_destrs in
562      let tmp_destrs ≝ \snd def_tmp_destrs in
563      let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
564      let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
565      let insts_init ≝ [
566        translate_move globals fresh_srcrs1 srcrs1;
567        translate_move globals fresh_srcrs2 srcrs2;
568        translate_cst globals (Ointconst I8 (zero …)) destrs
569      ]
570      in
571        let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
572        let f' ≝ λi. λi_proof: i ≤ |srcrs2|. f i ? in
573        let insts_mul ≝ foldi_strong … srcrs2 f' [ ] in
574          add_translates rtl_params1 globals (insts_init @ insts_mul) start_lbl dest_lbl def
575    ].
576  >tmp_destrs_prf
577  >regs_proof
578  assumption
579qed.
580
581definition translate_divumodu8 ≝
582  λglobals: list ident.
583  λorder: bool.
584  λdestrs: list register.
585  λsrcr1: register.
586  λsrcr2: register.
587  λstart_lbl: label.
588  λdest_lbl: label.
589  λdef: rtl_internal_function globals.
590  match destrs with
591  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
592  | cons destr destrs ⇒
593    let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
594    let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉 | _ ⇒ 〈dummy, destr〉 ] in
595    let inst_div ≝ adds_graph rtl_params1 globals [
596      sequential rtl_params_ globals (OPACCS … DivuModu destr1 destr2 srcr1 srcr2)
597    ]
598    in
599    let insts_rest ≝ translate_cst globals (Ointconst I8 (zero ?)) destrs in
600      add_translates rtl_params1 globals [ inst_div; insts_rest ] start_lbl dest_lbl def
601  ].
602
603definition translate_ne: ∀globals: list ident. ? → ? → ? → ? → ? → ? → rtl_internal_function globals ≝
604  λglobals: list ident.
605  λdestrs: list register.
606  λsrcrs1: list register.
607  λsrcrs2: list register.
608  λstart_lbl: label.
609  λdest_lbl: label.
610  λdef: rtl_internal_function globals.
611  match destrs with
612  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
613  | cons destr destrs ⇒
614    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
615    let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params0 globals def in
616    let 〈def, tmp_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
617    let save_srcrs1 ≝ translate_move globals tmp_srcrs1 srcrs1 in
618    let 〈def, tmp_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
619    let save_srcrs2 ≝ translate_move globals tmp_srcrs2 srcrs2 in
620    match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
621    [ dp crl their_proof ⇒
622      let commonl ≝ \fst (\fst crl) in
623      let commonr ≝ \fst (\snd crl) in
624      let restl ≝ \snd (\snd crl) in
625      let restr ≝ \snd (\snd crl) in
626      let rest ≝ restl @ restr in
627      let inits ≝ [
628        sequential … (INT rtl_params_ globals destr (zero …));
629        sequential … (INT rtl_params_ globals tmp_zero (zero …))
630      ]
631      in
632      let f_common ≝ λtmp_srcr1. λtmp_srcr2. [
633        sequential … (CLEAR_CARRY …);
634        sequential … (OP2 rtl_params_ globals Sub tmpr tmp_srcr1 tmp_srcr2);
635        sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
636      ]
637      in
638      let insts_common ≝ flatten … (map2 … f_common commonl commonr ?) in
639      let f_rest ≝ λtmp_srcr. [
640        sequential … (CLEAR_CARRY …);
641        sequential … (OP2 rtl_params_ globals Sub tmpr tmp_zero tmp_srcr);
642        sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
643      ]
644      in
645      let insts_rest ≝ flatten … (map … f_rest rest) in
646      let insts ≝ inits @ insts_common @ insts_rest in
647      let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
648        add_translates rtl_params1 globals [
649          save_srcrs1; save_srcrs2; adds_graph rtl_params1 globals insts; epilogue
650        ] start_lbl dest_lbl def
651    ]
652  ].
653  @their_proof
654qed.
655
656definition translate_eq_reg ≝
657  λglobals: list ident.
658  λtmp_zero: register.
659  λtmp_one: register.
660  λtmpr1: register.
661  λtmpr2: register.
662  λdestr: register.
663  λdummy_lbl: label.
664  λsrcr12: register × register.
665  let 〈srcr1, srcr2〉 ≝ srcr12 in
666  [ sequential … (CLEAR_CARRY …);
667    sequential rtl_params_ globals (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
668    sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
669    sequential … (OP2 rtl_params_ globals Sub tmpr2 srcr2 srcr1);
670    sequential … (OP2 rtl_params_ globals Addc tmpr2 tmp_zero tmp_zero);
671    sequential … (OP2 rtl_params_ globals Or tmpr1 tmpr1 tmpr2);
672    sequential … (OP2 rtl_params_ globals Xor tmpr1 tmpr1 tmp_one);
673    sequential … (OP2 rtl_params_ globals And destr destr tmpr1) ].
674
675definition translate_eq_list ≝
676  λglobals: list ident.
677  λtmp_zero: register.
678  λtmp_one: register.
679  λtmpr1: register.
680  λtmpr2: register.
681  λdestr: register.
682  λleq: list (register × register).
683  λdummy_lbl: label.
684  let f ≝ translate_eq_reg globals tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
685    (sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1))) ::
686      flatten … (map … f leq).
687
688definition translate_atom ≝
689  λglobals: list ident.
690  λtmp_zero: register.
691  λtmp_one: register.
692  λtmpr1: register.
693  λtmpr2: register.
694  λtmpr3: register.
695  λdestr: register.
696  λdummy_lbl: label.
697  λleq: list (register × register).
698  λsrcr1: register.
699  λsrcr2: register.
700    translate_eq_list globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
701    [ sequential … (CLEAR_CARRY …);
702      sequential … (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
703      sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
704      sequential … (OP2 rtl_params_ globals And tmpr3 tmpr3 tmpr1);
705      sequential … (OP2 rtl_params_ globals Or destr destr tmpr3) ].
706
707definition translate_lt_main ≝
708  λglobals: list ident.
709  λtmp_zero: register.
710  λtmp_one: register.
711  λtmpr1: register.
712  λtmpr2: register.
713  λtmpr3: register.
714  λdestr: register.
715  λdummy_lbl: label.
716  λsrcrs1: list register.
717  λsrcrs2: list register.
718  λproof: |srcrs1| = |srcrs2|.
719  let f ≝ λinsts_leq. λsrcr1. λsrcr2.
720    let 〈insts, leq〉 ≝ insts_leq in
721    let added_insts ≝ translate_atom globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
722      〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉
723  in
724    \fst (fold_left2 … f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).
725
726definition fresh_regs_strong:
727  ∀globals. rtl_internal_function globals → ∀n: nat. Σfresh: (rtl_internal_function globals) × (list register). |\snd fresh| = n ≝
728  λglobals: list ident.
729  λdef.
730  λn.
731    fresh_regs rtl_params0 globals def n.
732  @fresh_regs_length
733qed.
734
735definition complete_regs_strong:
736  ∀globals: list ident. rtl_internal_function globals → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
737  λglobals: list ident.
738  λdef.
739  λleft.
740  λright.
741    complete_regs globals def left right.
742  @complete_regs_length
743qed.
744
745definition translate_lt ≝
746  λglobals: list ident.
747  λdestrs: list register.
748  λprf_destrs: 0 < |destrs|.
749  λsrcrs1: list register.
750  λsrcrs2: list register.
751  λstart_lbl: label.
752  λdest_lbl: label.
753  λdef: rtl_internal_function globals.
754  match destrs with
755  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
756  | _ ⇒
757    match fresh_regs_strong globals def (|destrs|) with
758    [ dp def_tmp_destrs tmp_destrs_proof ⇒
759      let def ≝ \fst def_tmp_destrs in
760      let tmp_destrs ≝ \snd def_tmp_destrs in
761      let tmp_destr ≝ hd_safe ? tmp_destrs ? in
762      let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params1 globals def in
763      let 〈def, tmp_one〉 ≝ fresh_reg rtl_params1 globals def in
764      let 〈def, tmpr1〉 ≝ fresh_reg rtl_params1 globals def in
765      let 〈def, tmpr2〉 ≝ fresh_reg rtl_params1 globals def in
766      let 〈def, tmpr3〉 ≝ fresh_reg rtl_params1 globals def in
767      match complete_regs_strong globals def srcrs1 srcrs2 with
768      [ dp srcrs12_added srcrs12_proof ⇒
769        let srcrs1 ≝ \fst (\fst srcrs12_added) in
770        let srcrs2 ≝ \snd (\fst srcrs12_added) in
771        let added ≝ \snd srcrs12_added in
772        let srcrs1' ≝ rev … srcrs1 in
773        let srcrs2' ≝ rev … srcrs2 in
774        let insts_init ≝ [
775          translate_cst globals (Ointconst I8 (zero ?)) tmp_destrs;
776          translate_cst globals (Ointconst I8 (zero ?)) added;
777          adds_graph rtl_params1 globals [
778            sequential rtl_params_ globals (INT rtl_params_ globals tmp_zero (zero …));
779            sequential rtl_params_ globals (INT rtl_params_ globals tmp_one (bitvector_of_nat … 1))
780          ]
781        ]
782        in
783        let insts_main ≝
784          translate_lt_main globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
785          let insts_main ≝ [ adds_graph rtl_params1 globals insts_main ] in
786          let insts_exit ≝ [ translate_move globals destrs tmp_destrs ] in
787            add_translates rtl_params1 globals (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
788      ]
789    ]
790  ].
791  [2: >tmp_destrs_proof @prf_destrs
792  |1: normalize nodelta
793      generalize in match srcrs12_proof
794      #HYP >rev_length >rev_length @HYP
795  ]
796qed.
797
798definition add_128_to_last ≝
799  λglobals: list ident.
800  λtmp_128: register.
801  λrs.
802  λprf: 0 < |rs|.
803  λstart_lbl: label.
804  match rs with
805  [ nil ⇒ adds_graph rtl_params1 globals [ ] start_lbl
806  | _ ⇒
807    let r ≝ last_safe … rs prf in
808      adds_graph rtl_params1 globals [
809        sequential rtl_params_ globals (OP2 rtl_params_ globals Add r r tmp_128)
810      ] start_lbl
811  ].
812
813definition translate_lts ≝
814  λglobals: list ident.
815  λdestrs: list register.
816  λdestrs_prf: 0 < |destrs|.
817  λsrcrs1: list register.
818  λsrcrs2: list register.
819  λsrcrs1_lt_prf: 0 < |srcrs1|.
820  λsrcrs2_lt_prf: 0 < |srcrs2|.
821  λstart_lbl: label.
822  λdest_lbl: label.
823  λdef: rtl_internal_function globals.
824  match fresh_regs_strong globals def (|srcrs1|) with
825  [ dp def_tmp_srcrs1 srcrs1_prf ⇒
826    let def ≝ \fst def_tmp_srcrs1 in
827    let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
828    match fresh_regs_strong globals def (|srcrs2|) with
829    [ dp def_tmp_srcrs2 srcrs2_prf ⇒
830      let def ≝ \fst def_tmp_srcrs2 in
831      let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
832      let 〈def, tmp_128〉 ≝ fresh_reg rtl_params0 globals def in
833        add_translates rtl_params1 globals [
834          translate_move globals tmp_srcrs1 srcrs1;
835          translate_move globals tmp_srcrs2 srcrs2;
836          adds_graph rtl_params1 globals [
837            sequential rtl_params_ globals (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128))
838          ];
839          add_128_to_last globals tmp_128 tmp_srcrs1 ?;
840          add_128_to_last globals tmp_128 tmp_srcrs2 ?;
841          translate_lt globals destrs destrs_prf tmp_srcrs1 tmp_srcrs2
842        ] start_lbl dest_lbl def
843    ]
844  ].
845  [1: >srcrs1_prf @srcrs1_lt_prf
846  |2: >srcrs2_prf @srcrs2_lt_prf
847  ]
848qed.
849
850definition translate_op2 ≝
851  λglobals: list ident.
852  λop2.
853  λdestrs: list register.
854  λdestrs_prf: 0 < |destrs|.
855  λsrcrs1: list register.
856  λsrcrs2: list register.
857  λsrcrs2_destrs_prf: |srcrs2| = |destrs|.
858  λsrcrs1_destrs_prf: |srcrs1| = |destrs|.
859  λstart_lbl: label.
860  λdest_lbl: label.
861  λdef: rtl_internal_function globals.
862  match op2 with
863  [ Oadd ⇒
864    translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
865  | Oaddp ⇒
866    translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
867  | Osub ⇒
868    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
869  | Osubpi ⇒
870    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
871  | Osubpp sz ⇒
872    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
873  | Omul ⇒
874    translate_mul globals destrs srcrs1 srcrs2 ? start_lbl dest_lbl def
875  | Odivu ⇒
876    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
877    [ cons hd tl ⇒ λcons_prf.
878      match tl with
879      [ nil ⇒ translate_divumodu8 globals true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
880      | _ ⇒ ? (* not implemented *)
881      ]
882    | nil ⇒ λnil_absrd. ?
883    ] ?
884  | Omodu ⇒
885    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
886    [ cons hd tl ⇒ λcons_prf.
887      match tl with
888      [ nil ⇒ translate_divumodu8 globals false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
889      | _ ⇒ ? (* not implemented *)
890      ]
891    | nil ⇒ λnil_absrd. ?
892    ] ?
893  | Oand ⇒
894    translate_op globals And destrs srcrs1 srcrs2 start_lbl dest_lbl def
895  | Oor ⇒
896    translate_op globals Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
897  | Oxor ⇒
898    translate_op globals Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
899  | Ocmp c ⇒
900    match c with
901    [ Ceq ⇒
902      add_translates rtl_params1 globals [
903        translate_ne globals destrs srcrs1 srcrs2;
904        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
905      ] start_lbl dest_lbl def
906    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
907    | Clt ⇒ translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def
908    | Cgt ⇒ translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def
909    | Cle ⇒
910      add_translates rtl_params1 globals [
911        translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ?;
912        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
913      ] start_lbl dest_lbl def
914    | Cge ⇒
915      add_translates rtl_params1 globals [
916        translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ?;
917        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
918      ] start_lbl dest_lbl def
919    ]
920  | Ocmpu c ⇒
921    match c with
922    [ Ceq ⇒
923      add_translates rtl_params1 globals [
924        translate_ne globals destrs srcrs1 srcrs2;
925        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
926      ] start_lbl dest_lbl def
927    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
928    | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
929    | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
930    | Cle ⇒
931      add_translates rtl_params1 globals [
932        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
933        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
934      ] start_lbl dest_lbl def
935    | Cge ⇒
936      add_translates rtl_params1 globals [
937        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
938        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
939      ] start_lbl dest_lbl def
940    ]
941  | Ocmpp c ⇒
942    match c with
943    [ Ceq ⇒
944      add_translates rtl_params1 globals [
945        translate_ne globals destrs srcrs1 srcrs2;
946        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
947      ] start_lbl dest_lbl def
948    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
949    | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
950    | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
951    | Cle ⇒
952      add_translates rtl_params1 globals [
953        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
954        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
955      ] start_lbl dest_lbl def
956    | Cge ⇒
957      add_translates rtl_params1 globals [
958        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
959        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
960      ] start_lbl dest_lbl def
961    ]
962  | _ ⇒ ? (* assert false, implemented in run time or float op *)
963  ].
964  [1:
965    @sym_eq
966    assumption
967  |3,8,19,22,24,25:
968    >srcrs1_destrs_prf
969    assumption
970  |4,9:
971    normalize in nil_absrd;
972    cases(not_le_Sn_O 0)
973    #HYP cases(HYP nil_absrd)
974  |5,10,20,21,23,26:
975    >srcrs2_destrs_prf
976    assumption
977  |*:
978    cases not_implemented (* XXX: yes, really *)
979  ]
980qed.
981
982definition translate_cond: ∀globals: list ident. list register → label → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
983  λglobals: list ident.
984  λsrcrs: list register.
985  λstart_lbl: label.
986  λlbl_true: label.
987  λlbl_false: label.
988  λdef: rtl_internal_function globals.
989  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
990  let 〈tmp_lbl, def〉 ≝ fresh_label rtl_params1 globals def in
991  let init ≝ sequential rtl_params_ globals (INT rtl_params_ globals tmpr (zero …)) in
992  let f ≝ λsrcr. sequential rtl_params_ globals (OP2 rtl_params_ globals Or tmpr tmpr srcr) in
993  let def ≝ adds_graph rtl_params1 globals (init :: (map ? ? f srcrs)) start_lbl tmp_lbl def in
994    add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true) lbl_false) def.
995
996definition translate_load ≝
997  λglobals: list ident.
998  λaddr.
999  λaddr_prf: 2 = |addr|.
1000  λdestrs: list register.
1001  λstart_lbl: label.
1002  λdest_lbl: label.
1003  λdef: rtl_internal_function globals.
1004  match fresh_regs_strong rtl_params0 globals def (|addr|) with
1005  [ dp def_save_addr save_addr_prf ⇒
1006    let def ≝ \fst def_save_addr in
1007    let save_addr ≝ \snd def_save_addr in
1008    match fresh_regs_strong rtl_params0 globals def (|addr|) with
1009    [ dp def_tmp_addr tmp_addr_prf ⇒
1010      let def ≝ \fst def_tmp_addr in
1011      let tmp_addr ≝ \snd def_tmp_addr in
1012      let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
1013      let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
1014      let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
1015      let insts_save_addr ≝ translate_move globals save_addr addr in
1016      let f ≝ λtranslates_off. λr.
1017        let 〈translates, off〉 ≝ translates_off in
1018        let translates ≝ translates @ [
1019          adds_graph rtl_params1 globals [
1020            sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
1021          ];
1022          translate_op2 globals Oaddp tmp_addr ? save_addr [dummy; tmpr] ? ?;
1023          adds_graph rtl_params1 globals [
1024            sequential rtl_params_ globals (LOAD rtl_params_ globals r tmp_addr1 tmp_addr2)
1025          ]
1026        ]
1027        in
1028        let 〈carry, result〉 ≝ half_add … off int_size in
1029          〈translates, result〉
1030      in
1031      let 〈translates, ignore〉 ≝ foldl … f 〈[ ], (zero ?)〉 destrs in
1032        add_translates rtl_params1 globals (insts_save_addr :: translates) start_lbl dest_lbl def
1033    ]
1034  ].
1035  [1: >tmp_addr_prf >save_addr_prf %
1036  |2: >save_addr_prf >tmp_addr_prf
1037      @addr_prf
1038  |3: >tmp_addr_prf normalize
1039      <addr_prf //
1040  |4: >tmp_addr_prf assumption
1041  ]
1042qed.
1043
1044definition translate_store ≝
1045  λglobals: list ident.
1046  λaddr.
1047  λaddr_prf: 2 = |addr|.
1048  λsrcrs: list register.
1049  λstart_lbl: label.
1050  λdest_lbl: label.
1051  λdef: rtl_internal_function globals.
1052  match fresh_regs_strong rtl_params0 globals def (|addr|) with
1053  [ dp def_tmp_addr tmp_addr_prf ⇒
1054    let def ≝ \fst def_tmp_addr in
1055    let tmp_addr ≝ \snd def_tmp_addr in
1056    let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
1057    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
1058    let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
1059    let f ≝ λtranslate_off. λsrcr.
1060      let 〈translates, off〉 ≝ translate_off in
1061      let translates ≝ translates @ [
1062        adds_graph rtl_params1 globals [
1063          sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
1064        ];
1065        translate_op2 globals Oaddp tmp_addr … addr [dummy; tmpr] ? ?;
1066        adds_graph rtl_params1 globals [
1067          sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr)
1068        ]
1069      ]
1070      in
1071        let 〈carry, result〉 ≝ half_add … off int_size in
1072          〈translates, result〉
1073    in
1074    let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero …〉 srcrs in
1075      add_translates rtl_params1 globals translates start_lbl dest_lbl def
1076  ].
1077  [1: >tmp_addr_prf %
1078  |2: >tmp_addr_prf normalize
1079      <addr_prf //
1080  |3: >tmp_addr_prf <addr_prf //
1081  |4: >tmp_addr_prf @addr_prf
1082  ]
1083qed.
1084
1085axiom fake_label: label.
1086
1087(* XXX: following conversation with CSC about the mix up in extension statements
1088        and extension instructions in RTL, use fake_label in calls to
1089        tailcall_* instructions. *)
1090definition translate_stmt ≝
1091  λglobals: list ident.
1092  λlenv: local_env.
1093  λlbl: label.
1094  λstmt.
1095  λdef: rtl_internal_function globals.
1096  match stmt with
1097  [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
1098  | St_cost cost_lbl lbl' ⇒ add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (COST_LABEL rtl_params_ globals cost_lbl) lbl') def
1099  | St_const destr cst lbl' ⇒
1100    translate_cst globals cst (find_local_env destr lenv) lbl lbl' def
1101  | St_op1 op1 destr srcr lbl' ⇒
1102    translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
1103  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
1104    translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
1105    (* XXX: should we be ignoring this? *)
1106  | St_load ignore addr destr lbl' ⇒
1107    translate_load globals (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
1108    (* XXX: should we be ignoring this? *)
1109  | St_store ignore addr srcr lbl' ⇒
1110    translate_store globals (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
1111  | St_call_id f args retr lbl' ⇒
1112    match retr with
1113    [ Some retr ⇒
1114      add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) (find_local_env retr lenv)) lbl') def
1115    | None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) [ ]) lbl') def
1116    ]
1117  | St_call_ptr f args retr lbl' ⇒
1118    match retr with
1119    [ None ⇒
1120      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1121        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])) lbl') def
1122    | Some retr ⇒
1123      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1124        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv))) lbl') def
1125    ]
1126  | St_tailcall_id f args ⇒
1127    add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params_ globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) fake_label) def
1128  | St_tailcall_ptr f args ⇒
1129    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1130      add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params1 globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) fake_label) def
1131  | St_cond r lbl_true lbl_false ⇒
1132    translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def
1133  | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
1134  | St_return ⇒ add_graph rtl_params1 globals lbl (RETURN …) def
1135  ].
1136  [10: cases not_implemented (* jtable case *)
1137  |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *)
1138  ]
1139qed.
1140
1141(* XXX: we use a "hack" here to circumvent the proof obligations required to
1142   create res, an empty internal_function record.  we insert into our graph
1143   the start and end nodes to ensure that they are in, and place dummy
1144   skip instructions at these nodes. *)
1145definition translate_internal ≝
1146  λglobals: list ident.
1147  λdef.
1148  let runiverse ≝ f_reggen def in
1149  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
1150    (f_params def @ f_locals def) (f_result def) in
1151  let params ≝ map_list_local_env lenv (map … \fst (f_params def)) in
1152  let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in
1153  let result ≝
1154    match (f_result def) with
1155    [ None ⇒ [ ]
1156    | Some r_typ ⇒
1157      let 〈r, typ〉 ≝ r_typ in
1158        find_local_env r lenv
1159    ]
1160  in
1161  let luniverse' ≝ f_labgen def in
1162  let runiverse' ≝ runiverse in
1163  let result' ≝ result in
1164  let params' ≝ params in
1165  let locals' ≝ locals in
1166  let stack_size' ≝ f_stacksize def in
1167  let entry' ≝ f_entry def in
1168  let exit' ≝ f_exit def in
1169  let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params_ globals entry') in
1170  let graph' ≝ add LabelTag ? graph' exit' (GOTO rtl_params_ globals exit') in
1171  let res ≝
1172    mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
1173     locals' stack_size' graph' ? ? in
1174    foldi … (translate_stmt globals … lenv) (f_graph def) res.
1175[ % [@entry' | @graph_add_lookup @graph_add]
1176| % [@exit'  | @graph_add]]
1177qed.
1178
1179(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
1180  because of CompCert heritage *)
1181definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
1182 λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
Note: See TracBrowser for help on using the repository browser.