source: src/RTLabs/RTLAbstoRTL.ma @ 1068

Last change on this file since 1068 was 1068, checked in by mulligan, 9 years ago

rtlabs translation complete subject to axioms

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