source: src/RTLabs/RTLAbstoRTL.ma @ 1073

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

more changes from today

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