source: src/RTLabs/RTLAbstoRTL.ma @ 1072

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

changes the specific form that the added proofs take to use None, not Some, hence removing the exitential

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