source: src/RTLabs/RTLabsToRTL.ma @ 1356

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

deleted redundant directory. added outlines for both reports, and added a few sections to report for D4.2. more work on foldi_strong in rtlabs to rtl

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