source: src/RTLabs/RTLAbstoRTL.ma @ 1308

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

changes to translate_cst

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