source: src/RTLabs/RTLabsToRTL.ma @ 1352

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

This commit is made necessary by the last Matita change.
Inclusion is now order of magnitudes faster in some situations.
However, some explicit "include alias" are now required to
achieve the old semantics.

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