source: src/RTLabs/RTLabsToRTL.ma @ 1314

Last change on this file since 1314 was 1314, checked in by mulligan, 10 years ago

name changes so that bash tab completion actually works with some predictability

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