source: src/RTLabs/RTLabsToRTL.ma @ 1517

Last change on this file since 1517 was 1515, checked in by campbell, 10 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 47.0 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 ≝ identifier_map RegisterTag (list register).
62
63definition mem_local_env : register → local_env → bool ≝
64  λr,e. member … e r.
65
66definition add_local_env : register → list register → local_env → local_env ≝
67  λr,v,e. add … e r v.
68
69definition find_local_env : register → local_env → list register ≝
70  λr: register.λenv. lookup_def … env r [].
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 〈empty_map …,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: cases daemon (* XXX: to do *)
593  |2: generalize in match counter_proof;
594      >identity
595      #HYP
596      normalize in HYP:(???%);
597      generalize in match (minus_m_n_Sp_to_minus_m_Sn_p reference counter (|tl|) HYP);
598      #ASSM assumption
599  |3: >identity
600      normalize
601      normalize in proof;
602      generalize in match(le_S … proof);
603      #HYP assumption
604  ]
605qed.
606 
607definition foldi_strong ≝
608  λa: Type[0].
609  λb: Type[0].
610  λthe_list: list b.
611  λf: (∀i: nat. ∀proof: i < |the_list|. a → b → a).
612  λseed: a.
613    foldi_strong_internal a b (|the_list|) the_list f seed 0 ?.
614  //
615qed.
616 
617definition translate_mul ≝
618  λglobals: list ident.
619  λdestrs: list register.
620  λsrcrs1: list register.
621  λsrcrs2: list register.
622  λregs_proof: |destrs| = |srcrs2|.
623  λstart_lbl: label.
624  λdest_lbl: label.
625  λdef: rtl_internal_function globals.
626  let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
627  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
628    match fresh_regs_strong rtl_params0 globals def (|destrs|) with
629    [ dp def_tmp_destrs tmp_destrs_prf ⇒
630      let def ≝ \fst def_tmp_destrs in
631      let tmp_destrs ≝ \snd def_tmp_destrs in
632      let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
633      let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
634      let insts_init ≝ [
635        translate_move globals fresh_srcrs1 srcrs1;
636        translate_move globals fresh_srcrs2 srcrs2;
637        translate_cst globals (Ointconst I8 (zero …)) destrs
638      ]
639      in
640        let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
641        let f' ≝ λi. λi_proof: i < |srcrs2|. f i ? in
642        let insts_mul ≝ foldi_strong … srcrs2 f' [ ] in
643          add_translates rtl_params1 globals (insts_init @ insts_mul) start_lbl dest_lbl def
644    ].
645  >tmp_destrs_prf
646  >regs_proof
647  /2/
648qed.
649
650definition translate_divumodu8 ≝
651  λglobals: list ident.
652  λorder: bool.
653  λdestrs: list register.
654  λsrcr1: register.
655  λsrcr2: register.
656  λstart_lbl: label.
657  λdest_lbl: label.
658  λdef: rtl_internal_function globals.
659  match destrs with
660  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
661  | cons destr destrs ⇒
662    let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
663    let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉 | _ ⇒ 〈dummy, destr〉 ] in
664    let inst_div ≝ adds_graph rtl_params1 globals [
665      sequential rtl_params_ globals (OPACCS … DivuModu destr1 destr2 srcr1 srcr2)
666    ]
667    in
668    let insts_rest ≝ translate_cst globals (Ointconst I8 (zero ?)) destrs in
669      add_translates rtl_params1 globals [ inst_div; insts_rest ] start_lbl dest_lbl def
670  ].
671
672definition translate_ne: ∀globals: list ident. ? → ? → ? → ? → ? → ? → rtl_internal_function globals ≝
673  λglobals: list ident.
674  λdestrs: list register.
675  λsrcrs1: list register.
676  λsrcrs2: list register.
677  λstart_lbl: label.
678  λdest_lbl: label.
679  λdef: rtl_internal_function globals.
680  match destrs with
681  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
682  | cons destr destrs ⇒
683    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
684    let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params0 globals def in
685    let 〈def, tmp_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
686    let save_srcrs1 ≝ translate_move globals tmp_srcrs1 srcrs1 in
687    let 〈def, tmp_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
688    let save_srcrs2 ≝ translate_move globals tmp_srcrs2 srcrs2 in
689    match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
690    [ dp crl their_proof ⇒
691      let commonl ≝ \fst (\fst crl) in
692      let commonr ≝ \fst (\snd crl) in
693      let restl ≝ \snd (\snd crl) in
694      let restr ≝ \snd (\snd crl) in
695      let rest ≝ restl @ restr in
696      let inits ≝ [
697        sequential … (INT rtl_params_ globals destr (zero …));
698        sequential … (INT rtl_params_ globals tmp_zero (zero …))
699      ]
700      in
701      let f_common ≝ λtmp_srcr1. λtmp_srcr2. [
702        sequential … (CLEAR_CARRY …);
703        sequential … (OP2 rtl_params_ globals Sub tmpr tmp_srcr1 tmp_srcr2);
704        sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
705      ]
706      in
707      let insts_common ≝ flatten … (map2 … f_common commonl commonr ?) in
708      let f_rest ≝ λtmp_srcr. [
709        sequential … (CLEAR_CARRY …);
710        sequential … (OP2 rtl_params_ globals Sub tmpr tmp_zero tmp_srcr);
711        sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
712      ]
713      in
714      let insts_rest ≝ flatten … (map … f_rest rest) in
715      let insts ≝ inits @ insts_common @ insts_rest in
716      let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
717        add_translates rtl_params1 globals [
718          save_srcrs1; save_srcrs2; adds_graph rtl_params1 globals insts; epilogue
719        ] start_lbl dest_lbl def
720    ]
721  ].
722  @their_proof
723qed.
724
725definition translate_eq_reg ≝
726  λglobals: list ident.
727  λtmp_zero: register.
728  λtmp_one: register.
729  λtmpr1: register.
730  λtmpr2: register.
731  λdestr: register.
732  λdummy_lbl: label.
733  λsrcr12: register × register.
734  let 〈srcr1, srcr2〉 ≝ srcr12 in
735  [ sequential … (CLEAR_CARRY …);
736    sequential rtl_params_ globals (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
737    sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
738    sequential … (OP2 rtl_params_ globals Sub tmpr2 srcr2 srcr1);
739    sequential … (OP2 rtl_params_ globals Addc tmpr2 tmp_zero tmp_zero);
740    sequential … (OP2 rtl_params_ globals Or tmpr1 tmpr1 tmpr2);
741    sequential … (OP2 rtl_params_ globals Xor tmpr1 tmpr1 tmp_one);
742    sequential … (OP2 rtl_params_ globals And destr destr tmpr1) ].
743
744definition translate_eq_list ≝
745  λglobals: list ident.
746  λtmp_zero: register.
747  λtmp_one: register.
748  λtmpr1: register.
749  λtmpr2: register.
750  λdestr: register.
751  λleq: list (register × register).
752  λdummy_lbl: label.
753  let f ≝ translate_eq_reg globals tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
754    (sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1))) ::
755      flatten … (map … f leq).
756
757definition translate_atom ≝
758  λglobals: list ident.
759  λtmp_zero: register.
760  λtmp_one: register.
761  λtmpr1: register.
762  λtmpr2: register.
763  λtmpr3: register.
764  λdestr: register.
765  λdummy_lbl: label.
766  λleq: list (register × register).
767  λsrcr1: register.
768  λsrcr2: register.
769    translate_eq_list globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
770    [ sequential … (CLEAR_CARRY …);
771      sequential … (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
772      sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
773      sequential … (OP2 rtl_params_ globals And tmpr3 tmpr3 tmpr1);
774      sequential … (OP2 rtl_params_ globals Or destr destr tmpr3) ].
775
776definition translate_lt_main ≝
777  λglobals: list ident.
778  λtmp_zero: register.
779  λtmp_one: register.
780  λtmpr1: register.
781  λtmpr2: register.
782  λtmpr3: register.
783  λdestr: register.
784  λdummy_lbl: label.
785  λsrcrs1: list register.
786  λsrcrs2: list register.
787  λproof: |srcrs1| = |srcrs2|.
788  let f ≝ λinsts_leq. λsrcr1. λsrcr2.
789    let 〈insts, leq〉 ≝ insts_leq in
790    let added_insts ≝ translate_atom globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
791      〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉
792  in
793    \fst (fold_left2 … f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).
794
795definition fresh_regs_strong:
796  ∀globals. rtl_internal_function globals → ∀n: nat. Σfresh: (rtl_internal_function globals) × (list register). |\snd fresh| = n ≝
797  λglobals: list ident.
798  λdef.
799  λn.
800    fresh_regs rtl_params0 globals def n.
801  @fresh_regs_length
802qed.
803
804definition complete_regs_strong:
805  ∀globals: list ident. rtl_internal_function globals → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
806  λglobals: list ident.
807  λdef.
808  λleft.
809  λright.
810    complete_regs globals def left right.
811  @complete_regs_length
812qed.
813
814definition translate_lt ≝
815  λglobals: list ident.
816  λdestrs: list register.
817  λprf_destrs: 0 < |destrs|.
818  λsrcrs1: list register.
819  λsrcrs2: list register.
820  λstart_lbl: label.
821  λdest_lbl: label.
822  λdef: rtl_internal_function globals.
823  match destrs with
824  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
825  | _ ⇒
826    match fresh_regs_strong globals def (|destrs|) with
827    [ dp def_tmp_destrs tmp_destrs_proof ⇒
828      let def ≝ \fst def_tmp_destrs in
829      let tmp_destrs ≝ \snd def_tmp_destrs in
830      let tmp_destr ≝ hd_safe ? tmp_destrs ? in
831      let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params1 globals def in
832      let 〈def, tmp_one〉 ≝ fresh_reg rtl_params1 globals def in
833      let 〈def, tmpr1〉 ≝ fresh_reg rtl_params1 globals def in
834      let 〈def, tmpr2〉 ≝ fresh_reg rtl_params1 globals def in
835      let 〈def, tmpr3〉 ≝ fresh_reg rtl_params1 globals def in
836      match complete_regs_strong globals def srcrs1 srcrs2 with
837      [ dp srcrs12_added srcrs12_proof ⇒
838        let srcrs1 ≝ \fst (\fst srcrs12_added) in
839        let srcrs2 ≝ \snd (\fst srcrs12_added) in
840        let added ≝ \snd srcrs12_added in
841        let srcrs1' ≝ rev … srcrs1 in
842        let srcrs2' ≝ rev … srcrs2 in
843        let insts_init ≝ [
844          translate_cst globals (Ointconst I8 (zero ?)) tmp_destrs;
845          translate_cst globals (Ointconst I8 (zero ?)) added;
846          adds_graph rtl_params1 globals [
847            sequential rtl_params_ globals (INT rtl_params_ globals tmp_zero (zero …));
848            sequential rtl_params_ globals (INT rtl_params_ globals tmp_one (bitvector_of_nat … 1))
849          ]
850        ]
851        in
852        let insts_main ≝
853          translate_lt_main globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
854          let insts_main ≝ [ adds_graph rtl_params1 globals insts_main ] in
855          let insts_exit ≝ [ translate_move globals destrs tmp_destrs ] in
856            add_translates rtl_params1 globals (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
857      ]
858    ]
859  ].
860  [2: >tmp_destrs_proof @prf_destrs
861  |1: normalize nodelta
862      generalize in match srcrs12_proof
863      #HYP >rev_length >rev_length @HYP
864  ]
865qed.
866
867definition add_128_to_last ≝
868  λglobals: list ident.
869  λtmp_128: register.
870  λrs.
871  λprf: 0 < |rs|.
872  λstart_lbl: label.
873  match rs with
874  [ nil ⇒ adds_graph rtl_params1 globals [ ] start_lbl
875  | _ ⇒
876    let r ≝ last_safe … rs prf in
877      adds_graph rtl_params1 globals [
878        sequential rtl_params_ globals (OP2 rtl_params_ globals Add r r tmp_128)
879      ] start_lbl
880  ].
881
882definition translate_lts ≝
883  λglobals: list ident.
884  λdestrs: list register.
885  λdestrs_prf: 0 < |destrs|.
886  λsrcrs1: list register.
887  λsrcrs2: list register.
888  λsrcrs1_lt_prf: 0 < |srcrs1|.
889  λsrcrs2_lt_prf: 0 < |srcrs2|.
890  λstart_lbl: label.
891  λdest_lbl: label.
892  λdef: rtl_internal_function globals.
893  match fresh_regs_strong globals def (|srcrs1|) with
894  [ dp def_tmp_srcrs1 srcrs1_prf ⇒
895    let def ≝ \fst def_tmp_srcrs1 in
896    let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
897    match fresh_regs_strong globals def (|srcrs2|) with
898    [ dp def_tmp_srcrs2 srcrs2_prf ⇒
899      let def ≝ \fst def_tmp_srcrs2 in
900      let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
901      let 〈def, tmp_128〉 ≝ fresh_reg rtl_params0 globals def in
902        add_translates rtl_params1 globals [
903          translate_move globals tmp_srcrs1 srcrs1;
904          translate_move globals tmp_srcrs2 srcrs2;
905          adds_graph rtl_params1 globals [
906            sequential rtl_params_ globals (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128))
907          ];
908          add_128_to_last globals tmp_128 tmp_srcrs1 ?;
909          add_128_to_last globals tmp_128 tmp_srcrs2 ?;
910          translate_lt globals destrs destrs_prf tmp_srcrs1 tmp_srcrs2
911        ] start_lbl dest_lbl def
912    ]
913  ].
914  [1: >srcrs1_prf @srcrs1_lt_prf
915  |2: >srcrs2_prf @srcrs2_lt_prf
916  ]
917qed.
918
919definition translate_op2 ≝
920  λglobals: list ident.
921  λop2.
922  λdestrs: list register.
923  λdestrs_prf: 0 < |destrs|.
924  λsrcrs1: list register.
925  λsrcrs2: list register.
926  λsrcrs2_destrs_prf: |srcrs2| = |destrs|.
927  λsrcrs1_destrs_prf: |srcrs1| = |destrs|.
928  λstart_lbl: label.
929  λdest_lbl: label.
930  λdef: rtl_internal_function globals.
931  match op2 with
932  [ Oadd ⇒
933    translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
934  | Oaddp ⇒
935    translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
936  | Osub ⇒
937    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
938  | Osubpi ⇒
939    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
940  | Osubpp sz ⇒
941    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
942  | Omul ⇒
943    translate_mul globals destrs srcrs1 srcrs2 ? start_lbl dest_lbl def
944  | Odivu ⇒
945    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
946    [ cons hd tl ⇒ λcons_prf.
947      match tl with
948      [ nil ⇒ translate_divumodu8 globals true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
949      | _ ⇒ ? (* not implemented *)
950      ]
951    | nil ⇒ λnil_absrd. ?
952    ] ?
953  | Omodu ⇒
954    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
955    [ cons hd tl ⇒ λcons_prf.
956      match tl with
957      [ nil ⇒ translate_divumodu8 globals false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
958      | _ ⇒ ? (* not implemented *)
959      ]
960    | nil ⇒ λnil_absrd. ?
961    ] ?
962  | Oand ⇒
963    translate_op globals And destrs srcrs1 srcrs2 start_lbl dest_lbl def
964  | Oor ⇒
965    translate_op globals Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
966  | Oxor ⇒
967    translate_op globals Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
968  | Ocmp c ⇒
969    match c with
970    [ Ceq ⇒
971      add_translates rtl_params1 globals [
972        translate_ne globals destrs srcrs1 srcrs2;
973        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
974      ] start_lbl dest_lbl def
975    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
976    | Clt ⇒ translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def
977    | Cgt ⇒ translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def
978    | Cle ⇒
979      add_translates rtl_params1 globals [
980        translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ?;
981        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
982      ] start_lbl dest_lbl def
983    | Cge ⇒
984      add_translates rtl_params1 globals [
985        translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ?;
986        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
987      ] start_lbl dest_lbl def
988    ]
989  | Ocmpu c ⇒
990    match c with
991    [ Ceq ⇒
992      add_translates rtl_params1 globals [
993        translate_ne globals destrs srcrs1 srcrs2;
994        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
995      ] start_lbl dest_lbl def
996    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
997    | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
998    | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
999    | Cle ⇒
1000      add_translates rtl_params1 globals [
1001        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
1002        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
1003      ] start_lbl dest_lbl def
1004    | Cge ⇒
1005      add_translates rtl_params1 globals [
1006        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
1007        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
1008      ] start_lbl dest_lbl def
1009    ]
1010  | Ocmpp c ⇒
1011    match c with
1012    [ Ceq ⇒
1013      add_translates rtl_params1 globals [
1014        translate_ne globals destrs srcrs1 srcrs2;
1015        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
1016      ] start_lbl dest_lbl def
1017    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
1018    | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
1019    | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
1020    | Cle ⇒
1021      add_translates rtl_params1 globals [
1022        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
1023        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
1024      ] start_lbl dest_lbl def
1025    | Cge ⇒
1026      add_translates rtl_params1 globals [
1027        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
1028        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
1029      ] start_lbl dest_lbl def
1030    ]
1031  | _ ⇒ ? (* assert false, implemented in run time or float op *)
1032  ].
1033  [1:
1034    @sym_eq
1035    assumption
1036  |3,8,19,22,24,25:
1037    >srcrs1_destrs_prf
1038    assumption
1039  |4,9:
1040    normalize in nil_absrd;
1041    cases(not_le_Sn_O 0)
1042    #HYP cases(HYP nil_absrd)
1043  |5,10,20,21,23,26:
1044    >srcrs2_destrs_prf
1045    assumption
1046  |*:
1047    cases not_implemented (* XXX: yes, really *)
1048  ]
1049qed.
1050
1051definition translate_cond: ∀globals: list ident. list register → label → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
1052  λglobals: list ident.
1053  λsrcrs: list register.
1054  λstart_lbl: label.
1055  λlbl_true: label.
1056  λlbl_false: label.
1057  λdef: rtl_internal_function globals.
1058  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
1059  let 〈tmp_lbl, def〉 ≝ fresh_label rtl_params1 globals def in
1060  let init ≝ sequential rtl_params_ globals (INT rtl_params_ globals tmpr (zero …)) in
1061  let f ≝ λsrcr. sequential rtl_params_ globals (OP2 rtl_params_ globals Or tmpr tmpr srcr) in
1062  let def ≝ adds_graph rtl_params1 globals (init :: (map ? ? f srcrs)) start_lbl tmp_lbl def in
1063    add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true) lbl_false) def.
1064
1065definition translate_load ≝
1066  λglobals: list ident.
1067  λaddr.
1068  λaddr_prf: 2 = |addr|.
1069  λdestrs: list register.
1070  λstart_lbl: label.
1071  λdest_lbl: label.
1072  λdef: rtl_internal_function globals.
1073  match fresh_regs_strong rtl_params0 globals def (|addr|) with
1074  [ dp def_save_addr save_addr_prf ⇒
1075    let def ≝ \fst def_save_addr in
1076    let save_addr ≝ \snd def_save_addr in
1077    match fresh_regs_strong rtl_params0 globals def (|addr|) with
1078    [ dp def_tmp_addr tmp_addr_prf ⇒
1079      let def ≝ \fst def_tmp_addr in
1080      let tmp_addr ≝ \snd def_tmp_addr in
1081      let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
1082      let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
1083      let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
1084      let insts_save_addr ≝ translate_move globals save_addr addr in
1085      let f ≝ λtranslates_off. λr.
1086        let 〈translates, off〉 ≝ translates_off in
1087        let translates ≝ translates @ [
1088          adds_graph rtl_params1 globals [
1089            sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
1090          ];
1091          translate_op2 globals Oaddp tmp_addr ? save_addr [dummy; tmpr] ? ?;
1092          adds_graph rtl_params1 globals [
1093            sequential rtl_params_ globals (LOAD rtl_params_ globals r tmp_addr1 tmp_addr2)
1094          ]
1095        ]
1096        in
1097        let 〈carry, result〉 ≝ half_add … off int_size in
1098          〈translates, result〉
1099      in
1100      let 〈translates, ignore〉 ≝ foldl … f 〈[ ], (zero ?)〉 destrs in
1101        add_translates rtl_params1 globals (insts_save_addr :: translates) start_lbl dest_lbl def
1102    ]
1103  ].
1104  [1: >tmp_addr_prf >save_addr_prf %
1105  |2: >save_addr_prf >tmp_addr_prf
1106      @addr_prf
1107  |3: >tmp_addr_prf normalize
1108      <addr_prf //
1109  |4: >tmp_addr_prf assumption
1110  ]
1111qed.
1112
1113definition translate_store ≝
1114  λglobals: list ident.
1115  λaddr.
1116  λaddr_prf: 2 = |addr|.
1117  λsrcrs: list register.
1118  λstart_lbl: label.
1119  λdest_lbl: label.
1120  λdef: rtl_internal_function globals.
1121  match fresh_regs_strong rtl_params0 globals def (|addr|) with
1122  [ dp def_tmp_addr tmp_addr_prf ⇒
1123    let def ≝ \fst def_tmp_addr in
1124    let tmp_addr ≝ \snd def_tmp_addr in
1125    let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
1126    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
1127    let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
1128    let f ≝ λtranslate_off. λsrcr.
1129      let 〈translates, off〉 ≝ translate_off in
1130      let translates ≝ translates @ [
1131        adds_graph rtl_params1 globals [
1132          sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
1133        ];
1134        translate_op2 globals Oaddp tmp_addr … addr [dummy; tmpr] ? ?;
1135        adds_graph rtl_params1 globals [
1136          sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr)
1137        ]
1138      ]
1139      in
1140        let 〈carry, result〉 ≝ half_add … off int_size in
1141          〈translates, result〉
1142    in
1143    let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero …〉 srcrs in
1144      add_translates rtl_params1 globals translates start_lbl dest_lbl def
1145  ].
1146  [1: >tmp_addr_prf %
1147  |2: >tmp_addr_prf normalize
1148      <addr_prf //
1149  |3: >tmp_addr_prf <addr_prf //
1150  |4: >tmp_addr_prf @addr_prf
1151  ]
1152qed.
1153
1154axiom fake_label: label.
1155
1156(* XXX: following conversation with CSC about the mix up in extension statements
1157        and extension instructions in RTL, use fake_label in calls to
1158        tailcall_* instructions. *)
1159definition translate_stmt ≝
1160  λglobals: list ident.
1161  λlenv: local_env.
1162  λlbl: label.
1163  λstmt.
1164  λdef: rtl_internal_function globals.
1165  match stmt with
1166  [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
1167  | St_cost cost_lbl lbl' ⇒ add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (COST_LABEL rtl_params_ globals cost_lbl) lbl') def
1168  | St_const destr cst lbl' ⇒
1169    translate_cst globals cst (find_local_env destr lenv) lbl lbl' def
1170  | St_op1 op1 destr srcr lbl' ⇒
1171    translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
1172  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
1173    translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
1174    (* XXX: should we be ignoring this? *)
1175  | St_load ignore addr destr lbl' ⇒
1176    translate_load globals (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
1177    (* XXX: should we be ignoring this? *)
1178  | St_store ignore addr srcr lbl' ⇒
1179    translate_store globals (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
1180  | St_call_id f args retr lbl' ⇒
1181    match retr with
1182    [ Some retr ⇒
1183      add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) (find_local_env retr lenv)) lbl') def
1184    | None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) [ ]) lbl') def
1185    ]
1186  | St_call_ptr f args retr lbl' ⇒
1187    match retr with
1188    [ None ⇒
1189      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1190        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])) lbl') def
1191    | Some retr ⇒
1192      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1193        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
1194    ]
1195  | St_tailcall_id f args ⇒
1196    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
1197  | St_tailcall_ptr f args ⇒
1198    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1199      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
1200  | St_cond r lbl_true lbl_false ⇒
1201    translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def
1202  | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
1203  | St_return ⇒ add_graph rtl_params1 globals lbl (RETURN …) def
1204  ].
1205  [10: cases not_implemented (* jtable case *)
1206  |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *)
1207  ]
1208qed.
1209
1210(* XXX: we use a "hack" here to circumvent the proof obligations required to
1211   create res, an empty internal_function record.  we insert into our graph
1212   the start and end nodes to ensure that they are in, and place dummy
1213   skip instructions at these nodes. *)
1214definition translate_internal ≝
1215  λglobals: list ident.
1216  λdef.
1217  let runiverse ≝ f_reggen def in
1218  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
1219    (f_params def @ f_locals def) (f_result def) in
1220  let params ≝ map_list_local_env lenv (map … \fst (f_params def)) in
1221  let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in
1222  let result ≝
1223    match (f_result def) with
1224    [ None ⇒ [ ]
1225    | Some r_typ ⇒
1226      let 〈r, typ〉 ≝ r_typ in
1227        find_local_env r lenv
1228    ]
1229  in
1230  let luniverse' ≝ f_labgen def in
1231  let runiverse' ≝ runiverse in
1232  let result' ≝ result in
1233  let params' ≝ params in
1234  let locals' ≝ locals in
1235  let stack_size' ≝ f_stacksize def in
1236  let entry' ≝ f_entry def in
1237  let exit' ≝ f_exit def in
1238  let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params_ globals entry') in
1239  let graph' ≝ add LabelTag ? graph' exit' (GOTO rtl_params_ globals exit') in
1240  let res ≝
1241    mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
1242     locals' stack_size' graph' ? ? in
1243    foldi … (translate_stmt globals … lenv) (f_graph def) res.
1244[ % [@entry' | @graph_add_lookup @graph_add]
1245| % [@exit'  | @graph_add]]
1246qed.
1247
1248(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
1249  because of CompCert heritage *)
1250definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
1251 λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
Note: See TracBrowser for help on using the repository browser.