source: src/RTLabs/RTLAbstoRTL.ma @ 1064

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

changes from today, nearly complete rtlabs translation pass

File size: 64.9 KB
Line 
1include "RTLabs/syntax.ma".
2include "RTL/RTL.ma".
3include "common/AssocList.ma".
4include "common/Graphs.ma".
5include "common/FrontEndOps.ma".
6
7definition add_graph ≝
8  λl: label.
9  λstmt.
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_sig' ≝ rtl_if_sig p in
14  let rtl_if_result' ≝ rtl_if_result p in
15  let rtl_if_params' ≝ rtl_if_params p in
16  let rtl_if_locals' ≝ rtl_if_locals p in
17  let rtl_if_stacksize' ≝ rtl_if_stacksize p in
18  let rtl_if_graph' ≝ add ? ? (rtl_if_graph p) l stmt in
19  let rtl_if_entry' ≝ rtl_if_entry p in
20  let rtl_if_exit' ≝ rtl_if_exit p in
21    mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig'
22                             rtl_if_params' rtl_if_params' rtl_if_locals'
23                             rtl_if_stacksize' rtl_if_graph' rtl_if_entry'
24                             rtl_if_exit'.
25     
26definition fresh_label: rtl_internal_function → rtl_internal_function × label ≝
27  λdef.
28    let 〈lbl, new_univ〉 ≝ fresh LabelTag (rtl_if_luniverse def) in
29    let locals ≝ rtl_if_locals def in
30    let rtl_if_luniverse' ≝ new_univ in
31    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
32    let rtl_if_sig' ≝ rtl_if_sig def in
33    let rtl_if_result' ≝ rtl_if_result def in
34    let rtl_if_params' ≝ rtl_if_params def in
35    let rtl_if_locals' ≝ rtl_if_locals def in
36    let rtl_if_stacksize' ≝ rtl_if_stacksize def in
37    let rtl_if_graph' ≝ rtl_if_graph def in
38    let rtl_if_entry' ≝ rtl_if_entry def in
39    let rtl_if_exit' ≝ rtl_if_exit def in
40      〈mk_rtl_internal_function
41        rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig' rtl_if_result'
42        rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
43        rtl_if_entry' rtl_if_exit', lbl〉.
44
45axiom register_fresh: universe RegisterTag → register.
46
47definition fresh_reg: rtl_internal_function → rtl_internal_function × register ≝
48  λdef.
49    let r ≝ register_fresh (rtl_if_runiverse def) in
50    let locals ≝ r :: rtl_if_locals def in
51    let rtl_if_luniverse' ≝ rtl_if_luniverse def in
52    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
53    let rtl_if_sig' ≝ rtl_if_sig def in
54    let rtl_if_result' ≝ rtl_if_result def in
55    let rtl_if_params' ≝ rtl_if_params def in
56    let rtl_if_locals' ≝ locals in
57    let rtl_if_stacksize' ≝ rtl_if_stacksize def in
58    let rtl_if_graph' ≝ rtl_if_graph def in
59    let rtl_if_entry' ≝ rtl_if_entry def in
60    let rtl_if_exit' ≝ rtl_if_exit def in
61      〈mk_rtl_internal_function
62        rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig' rtl_if_result'
63        rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
64        rtl_if_entry' rtl_if_exit', r〉.
65       
66let rec fresh_regs (def: rtl_internal_function) (n: nat) on n ≝
67  match n with
68  [ O   ⇒ 〈def, [ ]〉
69  | S n ⇒
70    let 〈def, res〉 ≝ fresh_regs def n in
71    let 〈def, r〉 ≝ fresh_reg def in
72      〈def, r :: res〉
73  ].
74
75axiom fresh_regs_length:
76  ∀def: rtl_internal_function.
77  ∀n: nat.
78    |(\snd (fresh_regs def n))| = n.
79   
80definition addr_regs ≝
81  λregs.
82  match regs with
83  [ cons hd tl ⇒
84    match tl with
85    [ cons hd' tl' ⇒ Some (register × register) 〈hd, hd'〉
86    | nil          ⇒ None (register × register)
87    ]
88  | nil ⇒ None (register × register) (* registers are not an address *)
89  ].
90
91let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
92  match n with
93  [ O ⇒ [ ]
94  | S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n')
95  ].
96
97definition choose_rest ≝
98  λA: Type[0].
99  λleft, right: list A.
100  λprfl: 0 < |left|.
101  λprfr: 0 < |right|.
102  match left return λx. 0 < |x| → list A with
103  [ nil ⇒ λnil_prf.
104    match right return λx. 0 < |x| → list A with
105    [ nil ⇒ λnil_nil_absrd. ?
106    | _ ⇒ λnil_cons_prf. right
107    ] prfr
108  | _ ⇒ λcons_prf. right
109  ] prfl.
110  normalize in nil_prf;
111  cases(not_le_Sn_O 0)
112  #HYP
113  cases(HYP nil_prf)
114qed.
115
116definition complete_regs ≝
117  λdef.
118  λsrcrs1.
119  λsrcrs2.
120  let nb_added ≝ abs ((length ? srcrs1) - (length ? srcrs2)) in
121  let 〈def, added_regs〉 ≝ fresh_regs def nb_added in
122    if gtb nb_added 0 then
123      〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
124    else
125      〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
126
127(* obvious, but proof doesn't look easy! *)
128axiom complete_regs_length:
129  ∀def.
130  ∀left.
131  ∀right.
132    |\fst (\fst (complete_regs def left right))| = |\snd (\fst (complete_regs def left right))|.
133
134definition size_of_sig_type ≝
135  λsig.
136  match sig with
137  [ ASTint isize sign ⇒
138    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
139      isize' ÷ (nat_of_bitvector ? int_size)
140  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
141  | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
142  ].
143  cases not_implemented;
144qed.
145
146inductive register_type: Type[0] ≝
147  | register_int: register → register_type
148  | register_ptr: register → register → register_type.
149
150definition local_env ≝ BitVectorTrie (list register).
151
152definition mem_local_env ≝
153  λr: register.
154  match r with
155  [ an_identifier w ⇒ member (list register) 16 w
156  ].
157
158definition add_local_env ≝
159  λr: register.
160  match r with
161  [ an_identifier w ⇒ insert (list register) 16 w
162  ].
163
164definition find_local_env ≝
165  λr: register.
166  λbvt.
167  match r with
168  [ an_identifier w ⇒ lookup (list register) 16 w bvt [ ]
169  ].
170
171definition initialize_local_env_internal ≝
172  λruniverse.
173  λlenv.
174  λr_sig.
175  let 〈r, sig〉 ≝ r_sig in
176  let size ≝ size_of_sig_type sig in
177  let rs ≝ register_freshes runiverse size in
178    add_local_env r rs lenv.
179
180definition initialize_local_env ≝
181  λruniverse.
182  λregisters.
183  λresult.
184  let registers ≝ registers @
185    match result with
186    [ None ⇒ [ ]
187    | Some rt ⇒ [ rt ]
188    ]
189  in
190    foldl ? ? (initialize_local_env_internal runiverse) (Stub …) registers.
191 
192definition map_list_local_env_internal ≝
193  λlenv.
194  λres.
195  λr.
196    res @ (find_local_env r lenv).
197   
198definition map_list_local_env ≝
199  λlenv.
200  λregs.
201    foldl ? ? (map_list_local_env_internal lenv) [ ] regs.
202
203definition make_addr ≝
204  λA.
205  λlst: list A.
206  λprf: length A lst = 2. (* do not use on arguments other than those of length 2 *)
207  match lst return λx. length A x = 2 → A × A with
208  [ nil ⇒ λlst_nil_prf. ?
209  | cons hd tl ⇒ λprf.
210    match tl return λx. length A x = 1 → A × A with
211    [ nil ⇒ λtl_nil_prf. ?
212    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
213    ] ?
214  ] prf.
215  [1: normalize in lst_nil_prf;
216      destruct(lst_nil_prf);
217  |2: normalize in prf;
218      destruct(prf)
219      @e0
220  |3: normalize in tl_nil_prf;
221      destruct(tl_nil_prf);
222  ]
223qed.
224
225definition find_and_addr ≝
226  λr.
227  λlenv.
228    make_addr ? (find_local_env r lenv).
229
230definition rtl_args ≝
231  λregs_list.
232  λlenv.
233    flatten ? (map ? ? (
234      λr. find_local_env r lenv) regs_list).
235
236definition change_label ≝
237  λlbl.
238  λstmt: rtl_statement.
239  match stmt with
240  [ rtl_st_skip _ ⇒ rtl_st_skip lbl
241  | rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl
242  | rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl
243  | rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl
244  | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
245  | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
246  | rtl_st_opaccs opaccs d s1 s2 s3 _ ⇒ rtl_st_opaccs opaccs d s1 s2 s3 lbl
247  | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
248  | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
249  | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl
250  | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl
251  | rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl
252  | rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl
253  | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a
254  | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
255  | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2
256  | rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl
257  | rtl_st_set_carry l ⇒ rtl_st_set_carry lbl
258  | rtl_st_return r ⇒ rtl_st_return r
259  ].
260
261(* Ack! Should generating a fresh label ever fail?  This seems to be a side-effect
262   of implementing everything as a bitvector, which is bounded.  If we implemented
263   labels as unbounded nats then this function will never fail.
264*)
265(* Fixed with changes to label generation.
266*)
267let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝
268  match stmt_list with
269  [ nil ⇒ def
270  | cons hd tl ⇒
271    match tl with
272    [ nil ⇒ add_graph start_lbl (change_label dest_lbl hd) def
273    | cons hd' tl' ⇒
274      let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
275      let stmt ≝ change_label tmp_lbl hd in
276      let def ≝ add_graph start_lbl stmt new_def in
277        adds_graph tl tmp_lbl dest_lbl new_def
278    ]
279  ].
280
281let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
282                       (def: ?) on translate_list ≝
283  match translate_list with
284  [ nil ⇒ def
285  | cons hd tl ⇒
286    match tl with
287    [ nil ⇒ hd start_lbl dest_lbl def
288    | cons hd' tl' ⇒
289      let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
290      let applied ≝ hd start_lbl tmp_lbl new_def in
291        add_translates tl tmp_lbl dest_lbl applied
292    ]
293  ].
294
295definition translate_cst_int_internal ≝
296  λdest_lbl.
297  λr.
298  λi.
299    rtl_st_int r i dest_lbl.
300
301axiom translate_cst:
302  ∀cst: constant.
303  ∀destrs: list register.
304  ∀start_lbl: label.
305  ∀dest_lbl: label.
306  ∀def: rtl_internal_function.
307    rtl_internal_function.
308
309definition translate_move_internal ≝
310  λstart_lbl: label.
311  λdestr: register.
312  λsrcr: register.
313    rtl_st_move destr srcr start_lbl.
314
315definition translate_move ≝
316  λdestrs: list register.
317  λsrcrs: list register.
318  λstart_lbl: label.
319    match reduce_strong register destrs srcrs with
320    [ dp crl_crr len_proof ⇒
321      let commonl ≝ \fst (\fst crl_crr) in
322      let commonr ≝ \fst (\snd crl_crr) in
323      let restl ≝ \snd (\fst crl_crr) in
324      let restr ≝ \snd (\snd crl_crr) in
325      let f_common ≝ translate_move_internal start_lbl in
326      let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
327      let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
328        add_translates [ translate1 ; translate2 ] start_lbl
329    ].
330    @len_proof
331qed.
332
333let rec make
334  (A: Type[0]) (elt: A) (n: nat) on n ≝
335  match n with
336  [ O ⇒ [ ]
337  | S n' ⇒ elt :: make A elt n'
338  ].
339 
340lemma make_length:
341  ∀A: Type[0].
342  ∀elt: A.
343  ∀n: nat.
344    n = length ? (make A elt n).
345  #A #ELT #N
346  elim N
347  [ normalize %
348  | #N #IH
349    normalize <IH %
350  ]
351qed.
352
353definition translate_cast_unsigned ≝
354  λdestrs.
355  λstart_lbl.
356  λdest_lbl.
357  λdef.
358  let 〈def, tmp_zero〉 ≝ fresh_reg def in
359  let zeros ≝ make ? tmp_zero (length ? destrs) in
360    add_translates [
361      adds_graph [
362        rtl_st_int tmp_zero (bitvector_of_nat ? 0) start_lbl
363        ];
364      translate_move destrs zeros
365    ] start_lbl dest_lbl def.
366
367definition translate_cast_signed ≝
368  λdestrs.
369  λsrcr.
370  λstart_lbl.
371  λdest_lbl.
372  λdef.
373  let 〈def, tmp_128〉 ≝ fresh_reg def in
374  let 〈def, tmp_255〉 ≝ fresh_reg def in
375  let 〈def, tmpr〉 ≝ fresh_reg def in
376  let 〈def, dummy〉 ≝ fresh_reg def in
377  let insts ≝ [
378    rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl;
379    rtl_st_op2 And tmpr tmp_128 srcr start_lbl;
380    rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl;
381    rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl;
382    rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl
383  ] in
384  let srcrs ≝ make ? tmpr (length ? destrs) in
385    add_translates [
386      adds_graph insts;
387      translate_move destrs srcrs
388    ] start_lbl dest_lbl def.
389
390definition translate_cast ≝
391  λsrc_size.
392  λsrc_sign.
393  λdest_size.
394  λdestrs.
395  λsrcrs.
396  match | srcrs | return λx. | srcrs | = x → ? with
397  [ O ⇒ λzero_prf. adds_graph [ ]
398  | S n' ⇒ λsucc_prf.
399    if ltb dest_size src_size then
400      translate_move destrs srcrs
401    else
402      match reduce_strong ? destrs srcrs with
403      [ dp crl len_proof ⇒
404        let commonl ≝ \fst (\fst crl) in
405        let commonr ≝ \fst (\snd crl) in
406        let restl ≝ \snd (\fst crl) in
407        let restr ≝ \snd (\snd crl) in
408        let insts_common ≝ translate_move commonl commonr in
409        let sign_reg ≝ last_safe ? srcrs ? in
410        let insts_sign ≝
411          match src_sign with
412          [ Unsigned ⇒ translate_cast_unsigned restl
413          | Signed ⇒ translate_cast_signed restl sign_reg
414          ]
415        in
416          add_translates [ insts_common; insts_sign ]
417      ]
418  ] (refl ? (|srcrs|)).
419  >succ_prf //
420qed.
421
422definition translate_negint ≝
423  λdestrs.
424  λsrcrs.
425  λstart_lbl.
426  λdest_lbl.
427  λdef.
428  λprf: | destrs | = | srcrs |. (* assert in caml code *)
429  let 〈def, tmpr〉 ≝ fresh_reg def in
430  let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
431  let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in
432  let insts_init ≝ [
433    rtl_st_set_carry start_lbl;
434    rtl_st_int tmpr (zero ?) start_lbl
435  ] in
436  let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lbl in
437  let insts_add ≝ map … f_add destrs in
438    adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
439
440definition translate_notbool ≝
441  λdestrs.
442  λsrcrs.
443  λstart_lbl.
444  λdest_lbl.
445  λdef.
446  match destrs with
447  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
448  | cons destr destrs ⇒
449    let 〈def, tmpr〉 ≝ fresh_reg def in
450    let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in
451    let save_srcrs ≝ translate_move tmp_srcrs srcrs in
452    let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lbl in
453    let f ≝ λtmp_srcr. [
454      rtl_st_clear_carry start_lbl;
455      rtl_st_int tmpr (zero ?) start_lbl;
456      rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl;
457      rtl_st_int tmpr (zero ?) start_lbl;
458      rtl_st_op2 Addc tmpr tmpr tmpr start_lbl;
459      rtl_st_op2 Xor destr destr tmpr start_lbl
460    ] in
461    let insts ≝ init_destr :: (flatten ? (map … f tmp_srcrs)) in
462    let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in
463      add_translates [
464        save_srcrs; adds_graph insts; epilogue
465      ] start_lbl dest_lbl def
466  ].
467
468definition translate_op1 ≝
469  λop1: op1.
470  λdestrs: list register.
471  λsrcrs: list register.
472  λprf: |destrs| = |srcrs|.
473  λstart_lbl: label.
474  λdest_lbl: label.
475  λdef: rtl_internal_function.
476  match op1 with
477  [ op_cast src_size src_sign dest_size ⇒
478      translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
479  | op_neg_int ⇒
480      translate_negint destrs srcrs start_lbl dest_lbl def prf
481  | op_not_bool ⇒
482      translate_notbool destrs srcrs start_lbl dest_lbl def
483  | op_not_int ⇒
484    let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
485    let l ≝ map2 … f destrs srcrs prf in
486      adds_graph l start_lbl dest_lbl def
487  | op_ptr_of_int ⇒
488      translate_move destrs srcrs start_lbl dest_lbl def
489  | op_int_of_ptr ⇒
490      translate_move destrs srcrs start_lbl dest_lbl def
491  | op_id ⇒
492      translate_move destrs srcrs start_lbl dest_lbl def
493  ].
494 
495definition translate_op ≝
496  λop.
497  λdestrs.
498  λsrcrs1.
499  λsrcrs2.
500  λprf: |srcrs1| = |srcrs2|.
501  λstart_lbl.
502  λdest_lbl.
503  λdef.
504  match reduce_strong ? srcrs1 srcrs2 with
505  [ dp reduced first_reduced_proof ⇒
506    let srcrsl_common ≝ \fst (\fst reduced) in
507    let srcrsr_common ≝ \fst (\snd reduced) in
508    let srcrsl_rest ≝ \snd (\fst reduced) in
509    let srcrsr_rest ≝ \snd (\snd reduced) in
510    let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ? in
511    match reduce_strong ? destrs srcrsl_common with
512    [ dp reduced second_reduced_proof ⇒
513      let destrs_common ≝ \fst (\fst reduced) in
514      let destrs_rest ≝ \snd (\fst reduced) in
515      match reduce_strong ? destrs_rest srcrs_rest with
516      [ dp reduced third_reduced_proof ⇒
517        let destrs_cted ≝ \fst (\fst reduced) in
518        let destrs_rest ≝ \snd (\fst reduced) in
519        let srcrs_cted ≝ \fst (\snd reduced) in
520        let 〈def, tmpr〉 ≝ fresh_reg def in
521        let insts_init ≝ [
522          rtl_st_clear_carry start_lbl;
523          rtl_st_int tmpr (zero ?) start_lbl
524        ] in
525        let f_add ≝ λdestr. λsrcr1. λsrcr2. rtl_st_op2 op destr srcr1 srcr2 start_lbl in
526        let insts_add ≝ map3 … f_add destrs_common srcrsl_common srcrsr_common ? ? in
527        let f_add_cted ≝ λdestr. λsrcr. rtl_st_op2 op destr srcr tmpr start_lbl in
528        let insts_add_cted ≝ map2 ? ? ? f_add_cted destrs_cted srcrs_cted ? in
529        let f_rest ≝ λdestr. rtl_st_op2 op destr tmpr tmpr start_lbl in
530        let insts_rest ≝ map … f_rest destrs_rest in
531          adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
532      ]
533    ]
534  ].
535cases not_implemented (* problem here with lengths of lists: possible bug? *)
536qed.
537
538let rec translate_mul1
539  (dummy: register) (tmpr: register) (destrs: list register)
540  (srcrs1: list register) (srcr2: register) (start_lbl: label)
541    on srcrs1 ≝
542  match destrs with
543  [ nil ⇒ adds_graph [ rtl_st_skip start_lbl ] start_lbl
544  | cons destr tl ⇒
545    match tl with
546    [ nil ⇒
547      match srcrs1 with
548      [ nil ⇒
549        adds_graph [
550          rtl_st_int tmpr (zero ?) start_lbl;
551          rtl_st_op2 Addc destr destr tmpr start_lbl
552        ] start_lbl
553      | cons srcr1 tl' ⇒
554        adds_graph [
555          rtl_st_opaccs Mul tmpr dummy srcr2 srcr1 start_lbl;
556          rtl_st_op2 Addc destr destr tmpr start_lbl
557        ] start_lbl
558      ]
559    | cons destr2 destrs ⇒
560      match srcrs1 with
561      [ nil ⇒
562        add_translates [
563          adds_graph [
564            rtl_st_int tmpr (zero ?) start_lbl;
565            rtl_st_op2 Addc destr destr tmpr start_lbl;
566            rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
567          ];
568          translate_cst (Ointconst I8 (zero ?)) destrs
569        ] start_lbl
570      | cons srcr1 srcrs1 ⇒
571        match destrs 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 destr2 destrs ⇒
582          add_translates [
583            adds_graph [
584              rtl_st_opaccs Mul tmpr destr2 srcr2 srcr1 start_lbl;
585              rtl_st_op2 Addc destr destr tmpr start_lbl
586            ];
587            translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2
588          ] start_lbl
589        ]
590      ]
591    ]
592  ].
593
594definition translate_muli ≝
595  λdummy: register.
596  λtmpr: register.
597  λdestrs: list register.
598  λtmp_destrs: list register.
599  λdestrs_prf: |destrs| = |tmp_destrs|.
600  λsrcrs1: list register.
601  λdummy_lbl: label.
602  λi: nat.
603  λi_prf.
604  λtranslates: list ?.
605  λsrcr2i: register.
606  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split ? tmp_destrs i i_prf in
607  let tmp_destrs2' ≝
608    match tmp_destrs2 with
609    [ nil ⇒ [ ]
610    | cons tmp_destr2 tmp_destrs2 ⇒ [
611        adds_graph [
612          rtl_st_clear_carry dummy_lbl;
613          rtl_st_int tmp_destr2 (zero ?) dummy_lbl
614        ];
615        translate_mul1 dummy tmpr tmp_destrs2 srcrs1 srcr2i;
616        translate_cst (Ointconst I8 (zero ?)) tmp_destrs1;
617        adds_graph [
618          rtl_st_clear_carry dummy_lbl
619        ];
620        translate_op Addc destrs destrs tmp_destrs destrs_prf
621      ]
622    ]
623  in
624    translates @ tmp_destrs2'.
625
626axiom translate_mul:
627  ∀destrs: list register.
628  ∀srcrs1: list register.
629  ∀srcrs2: list register.
630  ∀start_lbl: label.
631  ∀dest_lbl: label.
632  ∀def: rtl_internal_function.
633    rtl_internal_function.
634
635(*
636definition 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  let 〈def, dummy〉 ≝ fresh_reg def in
644  let 〈def, tmpr〉 ≝ fresh_reg def in
645  let 〈def, tmp_destrs〉 ≝ fresh_regs def (|destrs|) in
646  let 〈def, fresh_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
647  let 〈def, fresh_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
648  let insts_init ≝ [
649    translate_move fresh_srcrs1 srcrs1;
650    translate_move fresh_srcrs2 srcrs2;
651    translate_cst (Ointconst I8 (zero ?)) destrs
652  ]
653  in
654  let f ≝ λi. translate_muli dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in
655  let insts_mul ≝ foldi ? ? [ ] srcrs2 in ?. [5: check insts_init.
656    add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
657*)
658
659definition translate_divumodu8 ≝
660  λorder: bool.
661  λdestrs: list register.
662  λsrcr1: register.
663  λsrcr2: register.
664  λstart_lbl: label.
665  λdest_lbl: label.
666  λdef: rtl_internal_function.
667  match destrs with
668  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
669  | cons destr destrs ⇒
670    let 〈def, dummy〉 ≝ fresh_reg def in
671    let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉 | _ ⇒ 〈dummy, destr〉 ] in
672    let inst_div ≝ adds_graph [
673      rtl_st_opaccs DivuModu destr1 destr2 srcr1 srcr2 start_lbl
674    ]
675    in
676    let insts_rest ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
677      add_translates [ inst_div; insts_rest ] start_lbl dest_lbl def
678  ].
679
680definition translate_ne: ? → ? → ? → ? → ? → ? → rtl_internal_function ≝
681  λdestrs: list register.
682  λsrcrs1: list register.
683  λsrcrs2: list register.
684  λstart_lbl: label.
685  λdest_lbl: label.
686  λdef: rtl_internal_function.
687  match destrs with
688  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
689  | cons destr destrs ⇒
690    let 〈def, tmpr〉 ≝ fresh_reg def in
691    let 〈def, tmp_zero〉 ≝ fresh_reg def in
692    let 〈def, tmp_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
693    let save_srcrs1 ≝ translate_move tmp_srcrs1 srcrs1 in
694    let 〈def, tmp_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
695    let save_srcrs2 ≝ translate_move tmp_srcrs2 srcrs2 in
696    match reduce_strong ? tmp_srcrs1 tmp_srcrs2 with
697    [ dp crl their_proof ⇒
698      let commonl ≝ \fst (\fst crl) in
699      let commonr ≝ \fst (\snd crl) in
700      let restl ≝ \snd (\snd crl) in
701      let restr ≝ \snd (\snd crl) in
702      let rest ≝ choose_rest ? restl restr ? ? in
703      let inits ≝ [
704        rtl_st_int destr (zero ?) start_lbl;
705        rtl_st_int tmp_zero (zero ?) start_lbl
706      ]
707      in
708      let f_common ≝ λtmp_srcr1. λtmp_srcr2. [
709        rtl_st_clear_carry start_lbl;
710        rtl_st_op2 Sub tmpr tmp_srcr1 tmp_srcr2 start_lbl;
711        rtl_st_op2 Or destr destr tmpr start_lbl
712      ]
713      in
714      let insts_common ≝ flatten ? (map2 … f_common commonl commonr ?) in
715      let f_rest ≝ λtmp_srcr. [
716        rtl_st_clear_carry start_lbl;
717        rtl_st_op2 Sub tmpr tmp_zero tmp_srcr start_lbl;
718        rtl_st_op2 Or destr destr tmpr start_lbl
719      ]
720      in
721      let insts_rest ≝ flatten ? (map ? ? f_rest rest) in
722      let insts ≝ inits @ insts_common @ insts_rest in
723      let epilogue ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
724        add_translates [
725          save_srcrs1; save_srcrs2; adds_graph insts; epilogue
726        ] start_lbl dest_lbl def
727    ]
728  ].
729  [1: @their_proof
730  |*: cases not_implemented (* choose rest requires non-emptiness proofs but
731                               these appear impossible to obtain, similar proof
732                               to above *)
733  ]
734qed.
735
736definition translate_eq_reg ≝
737  λtmp_zero: register.
738  λtmp_one: register.
739  λtmpr1: register.
740  λtmpr2: register.
741  λdestr: register.
742  λdummy_lbl: label.
743  λsrcr12: register × register.
744  let 〈srcr1, srcr2〉 ≝ srcr12 in
745  [ rtl_st_clear_carry dummy_lbl;
746    rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
747    rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
748    rtl_st_op2 Sub tmpr2 srcr2 srcr1 dummy_lbl;
749    rtl_st_op2 Addc tmpr2 tmp_zero tmp_zero dummy_lbl;
750    rtl_st_op2 Or tmpr1 tmpr1 tmpr2 dummy_lbl;
751    rtl_st_op2 Xor tmpr1 tmpr1 tmp_one dummy_lbl;
752    rtl_st_op2 And destr destr tmpr1 dummy_lbl ].
753
754definition translate_eq_list ≝
755  λtmp_zero: register.
756  λtmp_one: register.
757  λtmpr1: register.
758  λtmpr2: register.
759  λdestr: register.
760  λleq: list (register × register).
761  λdummy_lbl: label.
762  let f ≝ translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
763    (rtl_st_int destr (bitvector_of_nat ? 1) dummy_lbl) ::
764      flatten ? (map ? ? f leq).
765
766definition translate_atom ≝
767  λtmp_zero: register.
768  λtmp_one: register.
769  λtmpr1: register.
770  λtmpr2: register.
771  λtmpr3: register.
772  λdestr: register.
773  λdummy_lbl: label.
774  λleq: list (register × register).
775  λsrcr1: register.
776  λsrcr2: register.
777    translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
778    [ rtl_st_clear_carry dummy_lbl;
779      rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
780      rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
781      rtl_st_op2 And tmpr3 tmpr3 tmpr1 dummy_lbl;
782      rtl_st_op2 Or destr destr tmpr3 dummy_lbl ].
783
784definition translate_lt_main ≝
785  λtmp_zero: register.
786  λtmp_one: register.
787  λtmpr1: register.
788  λtmpr2: register.
789  λtmpr3: register.
790  λdestr: register.
791  λdummy_lbl: label.
792  λsrcrs1: list register.
793  λsrcrs2: list register.
794  λproof: |srcrs1| = |srcrs2|.
795  let f ≝ λinsts_leq. λsrcr1. λsrcr2.
796    let 〈insts, leq〉 ≝ insts_leq in
797    let added_insts ≝ translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
798      〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉
799  in
800    \fst (fold_left2 ? ? ? f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).
801
802definition fresh_regs_strong:
803  rtl_internal_function → ∀n: nat. Σfresh: rtl_internal_function × (list register). |\snd fresh| = n ≝
804  λdef.
805  λn.
806    fresh_regs def n.
807  @fresh_regs_length
808qed.
809
810definition complete_regs_strong:
811  rtl_internal_function → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
812  λdef.
813  λleft.
814  λright.
815    complete_regs def left right.
816  @complete_regs_length
817qed.
818
819definition translate_lt ≝
820  λdestrs: list register.
821  λprf_destrs: lt 0 (|destrs|).
822  λsrcrs1: list register.
823  λsrcrs2: list register.
824  λprf_srcrs: |srcrs1| = |srcrs2|.
825  λstart_lbl: label.
826  λdest_lbl: label.
827  λdef: rtl_internal_function.
828  match destrs with
829  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
830  | _ ⇒
831    match fresh_regs_strong def (|destrs|) with
832    [ dp def_tmp_destrs tmp_destrs_proof ⇒
833      let def ≝ \fst def_tmp_destrs in
834      let tmp_destrs ≝ \snd def_tmp_destrs in
835      let tmp_destr ≝ hd_safe ? tmp_destrs ? in
836      let 〈def, tmp_zero〉 ≝ fresh_reg def in
837      let 〈def, tmp_one〉 ≝ fresh_reg def in
838      let 〈def, tmpr1〉 ≝ fresh_reg def in
839      let 〈def, tmpr2〉 ≝ fresh_reg def in
840      let 〈def, tmpr3〉 ≝ fresh_reg def in
841      match complete_regs_strong def srcrs1 srcrs2 with
842      [ dp srcrs12_added srcrs12_proof ⇒
843        let srcrs1 ≝ \fst (\fst srcrs12_added) in
844        let srcrs2 ≝ \snd (\fst srcrs12_added) in
845        let added ≝ \snd srcrs12_added in
846        let srcrs1' ≝ rev ? srcrs1 in
847        let srcrs2' ≝ rev ? srcrs2 in
848        let insts_init ≝ [
849          translate_cst (Ointconst I8 (zero ?)) tmp_destrs;
850          translate_cst (Ointconst I8 (zero ?)) added;
851          adds_graph [
852            rtl_st_int tmp_zero (zero ?) start_lbl;
853            rtl_st_int tmp_one (bitvector_of_nat ? 1) start_lbl
854          ]
855        ]
856        in
857        let insts_main ≝
858          translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
859          let insts_main ≝ [ adds_graph insts_main ] in
860          let insts_exit ≝ [ translate_move destrs tmp_destrs ] in
861            add_translates (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
862      ]
863    ]
864  ].
865  [2: >tmp_destrs_proof @prf_destrs
866  |1: normalize nodelta
867      generalize in match srcrs12_proof
868      #HYP >rev_length >rev_length @HYP
869  ]
870qed.
871
872definition add_128_to_last ≝
873  λtmp_128: register.
874  λrs.
875  λprf: 0 < |rs|.
876  λstart_lbl: label.
877  match rs with
878  [ nil ⇒ adds_graph [ ] start_lbl
879  | _ ⇒
880    let r ≝ last_safe ? rs prf in
881      adds_graph [
882        rtl_st_op2 Add r r tmp_128 start_lbl
883      ] start_lbl
884  ].
885
886definition translate_lts ≝
887  λdestrs: list register.
888  λdestrs_prf: lt 0 (|destrs|).
889  λsrcrs1: list register.
890  λsrcrs2: list register.
891  λsrcrs_prf: |srcrs1| = |srcrs2|.
892  λsrcrs1_lt_prf: 0 < |srcrs1|.
893  λstart_lbl: label.
894  λdest_lbl: label.
895  λdef: rtl_internal_function.
896  match fresh_regs_strong def (|srcrs1|) with
897  [ dp def_tmp_srcrs1 srcrs1_prf ⇒
898    let def ≝ \fst def_tmp_srcrs1 in
899    let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
900    match fresh_regs_strong def (|srcrs2|) with
901    [ dp def_tmp_srcrs2 srcrs2_prf ⇒
902      let def ≝ \fst def_tmp_srcrs2 in
903      let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
904      let 〈def, tmp_128〉 ≝ fresh_reg def in
905        add_translates [
906          translate_move tmp_srcrs1 srcrs1;
907          translate_move tmp_srcrs2 srcrs2;
908          adds_graph [
909            rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl
910          ];
911          add_128_to_last tmp_128 tmp_srcrs1 ?;
912          add_128_to_last tmp_128 tmp_srcrs2 ?;
913          translate_lt destrs destrs_prf tmp_srcrs1 tmp_srcrs2 ?
914        ] start_lbl dest_lbl def
915    ]
916  ].
917  [2: >srcrs2_prf >srcrs1_prf @srcrs_prf
918  |3: >srcrs2_prf <srcrs_prf @srcrs1_lt_prf
919  |1: >srcrs1_prf @srcrs1_lt_prf
920  ]
921qed.
922
923definition translate_op2 ≝
924  λop2.
925  λdestrs: list register.
926  λdestrs_prf: lt 0 (|destrs|).
927  λsrcrs1: list register.
928  λsrcrs2: list register.
929  λsrcrs_prf: |srcrs1| = |srcrs2|.
930  λstart_lbl: label.
931  λdest_lbl: label.
932  λdef: rtl_internal_function.
933  match op2 with
934  [ op_add ⇒
935    translate_op Addc destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
936  | op_addp ⇒
937    translate_op Addc destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
938  | op_sub ⇒
939    translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
940  | op_subp ⇒
941    translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
942  | op_subpp ⇒
943    translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
944  | op_mul ⇒
945    translate_op Mul destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
946  | op_divu ⇒ ?
947  | op_modu ⇒ ?
948  | op_and ⇒
949    translate_op And destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
950  | op_or ⇒
951    translate_op Or destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
952  | op_xor ⇒
953    translate_op Xor destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
954  | op_cmp c ⇒
955    match c with
956    [ Compare_Equal ⇒
957      add_translates [
958        translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def;
959        translate_op1 op_not_bool destrs destrs (refl ? (|destrs|))
960      ] start_lbl dest_lbl def
961    | Compare_NotEqual ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
962    | Compare_Less ⇒ translate_lts destrs destrs_prf srcrs1 srcrs2 srcrs_prf ? start_lbl dest_lbl def
963    | Compare_Greater ⇒ translate_lts destrs destrs_prf srcrs2 srcrs1 srcrs_prf ? start_lbl dest_lbl def
964    | Compare_LessEqual ⇒
965      add_translates [
966        translate_lts destrs destrs_prf srcrs2 srcrs1 srcrs_prf ? start_lbl dest_lbl def;
967        translate_op1 op_not_bool destrs destrs (refl ? (|destrs|))
968      ] start_lbl dest_lbl def
969    | Compare_GreaterEqual ⇒
970      add_translates [
971        translate_lts destrs destrs_prf srcrs1 srcrs2 srcrs_prf ? start_lbl dest_lbl def;
972        translate_op1 op_not_bool destrs destrs (refl ? (|destrs|))
973      ] start_lbl dest_lbl def
974    ]
975  | _ ⇒ ?
976  ].
977
978let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
979  match op2 with
980
981    | AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
982      translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2)
983        start_lbl dest_lbl def
984
985    | AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
986      translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2)
987        start_lbl dest_lbl def
988
989    | AST.Op_cmp AST.Cmp_eq
990    | AST.Op_cmpu AST.Cmp_eq
991    | AST.Op_cmpp AST.Cmp_eq ->
992      add_translates
993        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) destrs srcrs1 srcrs2 ;
994         translate_op1 AST.Op_notbool destrs destrs]
995        start_lbl dest_lbl def
996
997    | AST.Op_cmp AST.Cmp_ne
998    | AST.Op_cmpu AST.Cmp_ne
999    | AST.Op_cmpp AST.Cmp_ne ->
1000      translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
1001
1002    | AST.Op_cmp AST.Cmp_lt ->
1003      translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def
1004
1005    | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt ->
1006      translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def
1007
1008    | AST.Op_cmp AST.Cmp_le ->
1009      add_translates
1010        [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
1011         translate_op1 AST.Op_notbool destrs destrs]
1012        start_lbl dest_lbl def
1013
1014    | AST.Op_cmpu AST.Cmp_le ->
1015      add_translates
1016        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs2 srcrs1 ;
1017         translate_op1 AST.Op_notbool destrs destrs]
1018        start_lbl dest_lbl def
1019
1020    | AST.Op_cmpp AST.Cmp_le ->
1021      add_translates
1022        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
1023         translate_op1 AST.Op_notbool destrs destrs]
1024        start_lbl dest_lbl def
1025
1026    | AST.Op_cmp AST.Cmp_gt ->
1027      translate_op2 (AST.Op_cmp AST.Cmp_lt)
1028        destrs srcrs2 srcrs1 start_lbl dest_lbl def
1029
1030    | AST.Op_cmpu AST.Cmp_gt ->
1031      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
1032        destrs srcrs2 srcrs1 start_lbl dest_lbl def
1033
1034    | AST.Op_cmpp AST.Cmp_gt ->
1035      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
1036        destrs srcrs2 srcrs1 start_lbl dest_lbl def
1037
1038    | AST.Op_cmp AST.Cmp_ge ->
1039      add_translates
1040        [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
1041         translate_op1 AST.Op_notbool destrs destrs]
1042        start_lbl dest_lbl def
1043
1044    | AST.Op_cmpu AST.Cmp_ge ->
1045      add_translates
1046        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
1047         translate_op1 AST.Op_notbool destrs destrs]
1048        start_lbl dest_lbl def
1049
1050    | AST.Op_cmpp AST.Cmp_ge ->
1051      add_translates
1052        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
1053         translate_op1 AST.Op_notbool destrs destrs]
1054        start_lbl dest_lbl def
1055
1056    | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl
1057    | AST.Op_shr | AST.Op_shru ->
1058      (* Unsupported, should have been replaced by a runtime function. *)
1059      assert false
1060
1061
1062definition filter_and_to_list_local_env_internal ≝
1063  λlenv.
1064  λl.
1065  λr.
1066  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
1067  [ Some entry ⇒
1068    match entry with
1069    [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ])
1070    | register_int r ⇒ (l @ [ r ])
1071    ]
1072  | None       ⇒ [ ] (* dpm: should this be none? *)
1073  ].
1074
1075definition filter_and_to_list_local_env ≝
1076  λlenv.
1077  λregisters.
1078    foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers.
1079
1080definition list_of_register_type ≝
1081  λrt.
1082  match rt with
1083  [ register_ptr r1 r2 ⇒ [ r1; r2 ]
1084  | register_int r ⇒ [ r ]
1085  ].
1086
1087definition find_and_list ≝
1088  λr.
1089  λlenv.
1090  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
1091  [ None      ⇒ [ ] (* dpm: should this be none? *)
1092  | Some lkup ⇒ list_of_register_type lkup
1093  ].
1094
1095definition find_and_list_args ≝
1096  λargs.
1097  λlenv.
1098    map ? ? (λr. find_and_list r lenv) args.
1099 
1100(* dpm: horrendous, use dependent types.
1101  length destr = length srcrs *)
1102let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label)
1103                       (dest_lbl: label) (def: ?) ≝
1104  match destrs with
1105  [ nil ⇒
1106    match srcrs with
1107    [ nil        ⇒ Some ? def
1108    | cons hd tl ⇒ None ?
1109    ]
1110  | cons hd tl ⇒
1111    match srcrs with
1112    [ nil        ⇒ None ?
1113    | cons hd' tl' ⇒
1114      match tl with
1115      [ nil            ⇒
1116        match tl' with
1117        (* one element lists *)
1118        [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def)
1119        | cons hd'' tl'' ⇒ None ?
1120        ]
1121      | cons hd'' tl'' ⇒
1122        match tl' with
1123        [ nil ⇒ None ?
1124        (* multielement lists *)
1125        | cons hd''' tl''' ⇒
1126          let tmp_lbl ≝ fresh_label def in
1127          match tmp_lbl with
1128          [ None ⇒ None ?
1129          | Some tmp_lbl ⇒
1130            let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in
1131              translate_move tl tl' tmp_lbl dest_lbl def
1132          ]
1133        ]
1134      ]
1135    ]
1136  ].
1137
1138definition extract_singleton ≝
1139  λA: Type[0].
1140  λl: list A.
1141  match l with
1142  [ nil ⇒ None ?
1143  | cons hd tl ⇒
1144    match tl with
1145    [ nil ⇒ Some ? hd
1146    | cons hd tl ⇒ None ?
1147    ]
1148  ].
1149
1150definition extract_pair ≝
1151  λA: Type[0].
1152  λl: list A.
1153  match l with
1154  [ nil ⇒ None ?
1155  | cons hd tl ⇒
1156    match tl with
1157    [ nil ⇒ None ?
1158    | cons hd' tl' ⇒
1159      match tl' with
1160      [ nil ⇒ Some ? 〈hd, hd'〉
1161      | cons hd'' tl'' ⇒ None ?
1162      ]
1163    ]
1164  ].
1165
1166definition translate_op1 ≝
1167  λop1.
1168  λdestrs.
1169  λsrcrs.
1170  λstart_lbl.
1171  λdest_lbl.
1172  λdef.
1173  match op1 with
1174  [ op_cast8_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1175  | op_cast8_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1176  | op_cast16_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1177  | op_cast16_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1178  | op_neg_int ⇒
1179    let dstr ≝ extract_singleton ? destrs in
1180    let srcr ≝ extract_singleton ? srcrs in
1181    match dstr with
1182    [ None ⇒ None ?
1183    | Some dstr ⇒
1184      match srcr with
1185      [ None ⇒ None ?
1186      | Some srcr ⇒
1187        adds_graph [
1188          rtl_st_op1 Cmpl dstr srcr start_lbl;
1189          rtl_st_op1 Inc dstr dstr start_lbl
1190        ] start_lbl dest_lbl def
1191      ]
1192    ]
1193  | op_not_int ⇒
1194    let dstr ≝ extract_singleton ? destrs in
1195    let srcr ≝ extract_singleton ? srcrs in
1196    match dstr with
1197    [ None ⇒ None ?
1198    | Some dstr ⇒
1199      match srcr with
1200      [ None ⇒ None ?
1201      | Some srcr ⇒
1202        adds_graph [
1203          rtl_st_op1 Cmpl dstr srcr start_lbl
1204        ] start_lbl dest_lbl def
1205      ]
1206    ]
1207  | op_id ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1208  | op_ptr_of_int ⇒
1209    let destr12 ≝ extract_pair ? destrs in
1210    let srcr ≝ extract_singleton ? srcrs in
1211    match destr12 with
1212    [ None ⇒ None ?
1213    | Some destr12 ⇒
1214      let 〈destr1, destr2〉 ≝ destr12 in
1215      match srcr with
1216      [ None ⇒ None ?
1217      | Some srcr ⇒
1218        adds_graph [
1219          rtl_st_move destr1 srcr dest_lbl;
1220          rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl
1221        ] start_lbl dest_lbl def
1222      ]
1223    ]
1224  | op_int_of_ptr ⇒
1225    let destr ≝ extract_singleton ? destrs in
1226    match destr with
1227    [ None ⇒ None ?
1228    | Some destr ⇒
1229      match srcrs with
1230      [ nil ⇒ None ?
1231      | cons srcr tl ⇒
1232        Some ? (add_graph start_lbl (rtl_st_move destr srcr dest_lbl) def)
1233      ]
1234    ]
1235  | op_not_bool ⇒
1236    let destr ≝ extract_singleton ? destrs in
1237    let srcrs ≝ extract_singleton ? srcrs in
1238    match destr with
1239    [ None ⇒ None ?
1240    | Some destr ⇒
1241      match srcrs with
1242      [ None ⇒ None ?
1243      | Some srcr ⇒
1244        let 〈def, tmpr〉 ≝ fresh_reg def in
1245        adds_graph [
1246          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
1247          rtl_st_clear_carry start_lbl;
1248          rtl_st_op2 Sub destr tmpr srcr start_lbl;
1249          rtl_st_int destr (bitvector_of_nat ? 0) dest_lbl;
1250          rtl_st_op2 Addc destr destr destr start_lbl;
1251          rtl_st_int tmpr (bitvector_of_nat ? 1) dest_lbl;
1252          rtl_st_op2 Xor destr destr tmpr start_lbl
1253        ] start_lbl dest_lbl def
1254      ]
1255    ]
1256  | _ ⇒ None ? (* error float *)
1257  ].
1258
1259definition translate_condptr ≝
1260  λr1.
1261  λr2.
1262  λstart_lbl: label.
1263  λlbl_true: label.
1264  λlbl_false: label.
1265  λdef.
1266  let 〈def, tmpr〉 ≝ fresh_reg def in
1267    adds_graph [
1268      rtl_st_op2 Or tmpr r1 r2 start_lbl;
1269      rtl_st_cond_acc tmpr lbl_true lbl_false
1270    ] start_lbl start_lbl def.
1271   
1272   
1273
1274(*
1275let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?)
1276                      (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝
1277  match op2 with
1278  [ op_add ⇒
1279    let destr ≝ extract_singleton ? destrs in
1280    let srcr1 ≝ extract_singleton ? srcrs1 in
1281    let srcr2 ≝ extract_singleton ? srcrs2 in
1282    match destr with
1283    [ None ⇒ None ?
1284    | Some destr ⇒
1285      match srcr1 with
1286      [ None ⇒ None ?
1287      | Some srcr1 ⇒
1288        match srcr2 with
1289        [ None ⇒ None ?
1290        | Some srcr2 ⇒
1291          adds_graph [
1292            rtl_st_op2 Add destr srcr1 srcr2 start_lbl
1293          ] start_lbl dest_lbl def
1294        ]
1295      ]
1296    ]
1297  | op_sub ⇒
1298    let destr ≝ extract_singleton ? destrs in
1299    let srcr1 ≝ extract_singleton ? srcrs1 in
1300    let srcr2 ≝ extract_singleton ? srcrs2 in
1301    match destr with
1302    [ None ⇒ None ?
1303    | Some destr ⇒
1304      match srcr1 with
1305      [ None ⇒ None ?
1306      | Some srcr1 ⇒
1307        match srcr2 with
1308        [ None ⇒ None ?
1309        | Some srcr2 ⇒
1310          adds_graph [
1311            rtl_st_clear_carry start_lbl;
1312            rtl_st_op2 Sub destr srcr1 srcr2 start_lbl
1313          ] start_lbl dest_lbl def
1314        ]
1315      ]
1316    ]
1317  | op_mul ⇒
1318    let destr ≝ extract_singleton ? destrs in
1319    let srcr1 ≝ extract_singleton ? srcrs1 in
1320    let srcr2 ≝ extract_singleton ? srcrs2 in
1321    match destr with
1322    [ None ⇒ None ?
1323    | Some destr ⇒
1324      match srcr1 with
1325      [ None ⇒ None ?
1326      | Some srcr1 ⇒
1327        match srcr2 with
1328        [ None ⇒ None ?
1329        | Some srcr2 ⇒
1330          adds_graph [
1331            rtl_st_opaccs Mul destr srcr1 srcr2 start_lbl
1332          ] start_lbl dest_lbl def
1333        ]
1334      ]
1335    ]
1336  | op_div ⇒ None ? (* signed div not supported *)
1337  | op_divu ⇒
1338    let destr ≝ extract_singleton ? destrs in
1339    let srcr1 ≝ extract_singleton ? srcrs1 in
1340    let srcr2 ≝ extract_singleton ? srcrs2 in
1341    match destr with
1342    [ None ⇒ None ?
1343    | Some destr ⇒
1344      match srcr1 with
1345      [ None ⇒ None ?
1346      | Some srcr1 ⇒
1347        match srcr2 with
1348        [ None ⇒ None ?
1349        | Some srcr2 ⇒
1350          adds_graph [
1351            rtl_st_opaccs Divu destr srcr1 srcr2 start_lbl
1352          ] start_lbl dest_lbl def
1353        ]
1354      ]
1355    ]
1356  | op_modu ⇒
1357    let destr ≝ extract_singleton ? destrs in
1358    let srcr1 ≝ extract_singleton ? srcrs1 in
1359    let srcr2 ≝ extract_singleton ? srcrs2 in
1360    match destr with
1361    [ None ⇒ None ?
1362    | Some destr ⇒
1363      match srcr1 with
1364      [ None ⇒ None ?
1365      | Some srcr1 ⇒
1366        match srcr2 with
1367        [ None ⇒ None ?
1368        | Some srcr2 ⇒
1369          adds_graph [
1370            rtl_st_opaccs Modu destr srcr1 srcr2 start_lbl
1371          ] start_lbl dest_lbl def
1372        ]
1373      ]
1374    ]
1375  | op_mod ⇒ None ? (* signed mod not supported *)
1376  | op_and ⇒
1377    let destr ≝ extract_singleton ? destrs in
1378    let srcr1 ≝ extract_singleton ? srcrs1 in
1379    let srcr2 ≝ extract_singleton ? srcrs2 in
1380    match destr with
1381    [ None ⇒ None ?
1382    | Some destr ⇒
1383      match srcr1 with
1384      [ None ⇒ None ?
1385      | Some srcr1 ⇒
1386        match srcr2 with
1387        [ None ⇒ None ?
1388        | Some srcr2 ⇒
1389          adds_graph [
1390            rtl_st_op2 And destr srcr1 srcr2 start_lbl
1391          ] start_lbl dest_lbl def
1392        ]
1393      ]
1394    ]
1395  | op_or ⇒
1396    let destr ≝ extract_singleton ? destrs in
1397    let srcr1 ≝ extract_singleton ? srcrs1 in
1398    let srcr2 ≝ extract_singleton ? srcrs2 in
1399    match destr with
1400    [ None ⇒ None ?
1401    | Some destr ⇒
1402      match srcr1 with
1403      [ None ⇒ None ?
1404      | Some srcr1 ⇒
1405        match srcr2 with
1406        [ None ⇒ None ?
1407        | Some srcr2 ⇒
1408          adds_graph [
1409            rtl_st_op2 Or destr srcr1 srcr2 start_lbl
1410          ] start_lbl dest_lbl def
1411        ]
1412      ]
1413    ]
1414  | op_xor ⇒
1415    let destr ≝ extract_singleton ? destrs in
1416    let srcr1 ≝ extract_singleton ? srcrs1 in
1417    let srcr2 ≝ extract_singleton ? srcrs2 in
1418    match destr with
1419    [ None ⇒ None ?
1420    | Some destr ⇒
1421      match srcr1 with
1422      [ None ⇒ None ?
1423      | Some srcr1 ⇒
1424        match srcr2 with
1425        [ None ⇒ None ?
1426        | Some srcr2 ⇒
1427          adds_graph [
1428            rtl_st_op2 Xor destr srcr1 srcr2 start_lbl
1429          ] start_lbl dest_lbl def
1430        ]
1431      ]
1432    ]
1433  | op_shru ⇒ None ? (* shifts not supported *)
1434  | op_shr ⇒ None ?
1435  | op_shl ⇒ None ?
1436  | op_addf ⇒ None ? (* floats not supported *)
1437  | op_subf ⇒ None ?
1438  | op_mulf ⇒ None ?
1439  | op_divf ⇒ None ?
1440  | op_cmpf _ ⇒ None ?
1441  | op_addp ⇒
1442    let destr12 ≝ extract_pair ? destrs in
1443    match destr12 with
1444    [ None         ⇒ None ?
1445    | Some destr12 ⇒
1446      let 〈destr1, destr2〉 ≝ destr12 in
1447      let srcr12 ≝ extract_pair ? srcrs1 in
1448      match srcr12 with
1449      [ None ⇒
1450        let srcr2 ≝ extract_singleton ? srcrs1 in
1451        match srcr2 with
1452        [ None ⇒ None ?
1453        | Some srcr2 ⇒
1454          let srcr12 ≝ extract_pair ? srcrs2 in
1455          match srcr12 with
1456          [ None ⇒ None ?
1457          | Some srcr12 ⇒
1458            let 〈srcr11, srcr12〉 ≝ srcr12 in
1459            let 〈def, tmpr1〉 ≝ fresh_reg def in
1460            let 〈def, tmpr2〉 ≝ fresh_reg def in
1461              adds_graph [
1462                rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
1463                rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
1464                rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
1465                rtl_st_move destr1 tmpr1 start_lbl
1466              ] start_lbl dest_lbl def
1467          ]
1468        ]
1469      | Some srcr12 ⇒
1470        let 〈srcr11, srcr12〉 ≝ srcr12 in
1471        let srcr2 ≝ extract_singleton ? srcrs2 in
1472        match srcr2 with
1473        [ None       ⇒ None ?
1474        | Some srcr2 ⇒
1475          let 〈def, tmpr1〉 ≝ fresh_reg def in
1476          let 〈def, tmpr2〉 ≝ fresh_reg def in
1477            adds_graph [
1478              rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
1479              rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
1480              rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
1481              rtl_st_move destr1 tmpr1 start_lbl
1482            ] start_lbl dest_lbl def
1483        ]
1484      ]
1485    ]
1486  | op_subp ⇒
1487    let destr ≝ extract_singleton ? destrs in
1488    match destr with
1489    [ None ⇒
1490      let destr12 ≝ extract_pair ? destrs in
1491      match destr12 with
1492      [ None ⇒ None ?
1493      | Some destr12 ⇒
1494        let 〈destr1, destr2〉 ≝ destr12 in
1495        let srcr12 ≝ extract_pair ? srcrs1 in
1496        match srcr12 with
1497        [ None ⇒ None ?
1498        | Some srcr12 ⇒
1499          let 〈srcr11, srcr12〉 ≝ srcr12 in
1500          let srcr2 ≝ extract_singleton ? srcrs2 in
1501          match srcr2 with
1502          [ None ⇒ None ?
1503          | Some srcr2 ⇒
1504            adds_graph [
1505              rtl_st_clear_carry start_lbl;
1506              rtl_st_op2 Sub destr1 srcr11 srcr2 start_lbl;
1507              rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl;
1508              rtl_st_op2 Sub destr2 srcr12 destr2 start_lbl
1509            ] start_lbl dest_lbl def
1510          ]
1511        ]
1512      ]
1513    | Some destr ⇒
1514      match srcrs1 with
1515      [ nil ⇒ None ?
1516      | cons srcr1 tl ⇒
1517        match srcrs2 with
1518        [ nil ⇒ None ?
1519        | cons srcr2 tl' ⇒
1520          let 〈def, tmpr1〉 ≝ fresh_reg def in
1521          let 〈def, tmpr2〉 ≝ fresh_reg def in
1522            adds_graph [
1523              rtl_st_op1 Cmpl tmpr1 srcr2 start_lbl;
1524              rtl_st_int tmpr2 (bitvector_of_nat ? 1) start_lbl;
1525              rtl_st_op2 Add tmpr1 tmpr1 tmpr2 start_lbl;
1526              rtl_st_op2 Add destr srcr1 tmpr1 start_lbl
1527            ] start_lbl dest_lbl def
1528        ]
1529      ]
1530    ]
1531  | op_cmp cmp ⇒
1532    match cmp with
1533    [ Compare_Equal ⇒
1534      add_translates [
1535        translate_op2 op_sub destrs srcrs1 srcrs2;
1536        translate_op1 op_not_bool destrs destrs
1537      ] start_lbl dest_lbl def
1538    | Compare_NotEqual ⇒
1539      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
1540    | _ ⇒ None ?
1541    ]
1542  | op_cmpu cmp ⇒
1543    match cmp with
1544    [ Compare_Equal ⇒
1545      add_translates [
1546        translate_op2 op_sub destrs srcrs1 srcrs2;
1547        translate_op1 op_not_bool destrs destrs
1548      ] start_lbl dest_lbl def
1549    | Compare_NotEqual ⇒
1550      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
1551    | Compare
1552    | _ ⇒ None ?
1553    ]
1554  | _ ⇒ ?
1555  ].
1556
1557    | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
1558      let (def, tmpr) = fresh_reg def in
1559      adds_graph
1560        [RTL.St_clear_carry start_lbl ;
1561         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
1562         RTL.St_int (destr, 0, start_lbl) ;
1563         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
1564        start_lbl dest_lbl def
1565
1566    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
1567      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
1568        destrs srcrs2 srcrs1 start_lbl dest_lbl def
1569
1570    | AST.Op_cmpu AST.Cmp_le, _, _, _ ->
1571      add_translates
1572        [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ;
1573         translate_op1 AST.Op_notbool destrs destrs]
1574        start_lbl dest_lbl def
1575
1576    | AST.Op_cmpu AST.Cmp_ge, _, _, _ ->
1577      add_translates
1578        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
1579         translate_op1 AST.Op_notbool destrs destrs]
1580        start_lbl dest_lbl def
1581
1582    | AST.Op_cmp cmp, _, _, _ ->
1583      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
1584      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
1585      add_translates
1586        [translate_cst (AST.Cst_int 128) tmprs1 ;
1587         translate_cst (AST.Cst_int 128) tmprs2 ;
1588         translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ;
1589         translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ;
1590         translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2]
1591        start_lbl dest_lbl def
1592
1593    | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
1594      let (def, tmpr) = fresh_reg def in
1595      add_translates
1596        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ;
1597         translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ;
1598         translate_op2 AST.Op_or [destr] [destr] [tmpr] ;
1599         adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ;
1600         translate_op2 AST.Op_xor [destr] [destr] [tmpr]]
1601        start_lbl dest_lbl def
1602
1603    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
1604      let (def, tmpr1) = fresh_reg def in
1605      let (def, tmpr2) = fresh_reg def in
1606      add_translates
1607        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
1608         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
1609         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
1610         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
1611         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
1612        start_lbl dest_lbl def
1613
1614    | AST.Op_cmpp AST.Cmp_gt, _, _, _ ->
1615      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
1616        destrs srcrs2 srcrs1 start_lbl dest_lbl def
1617
1618    | AST.Op_cmpp AST.Cmp_le, _, _, _ ->
1619      add_translates
1620        [translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ;
1621         translate_op1 AST.Op_notbool destrs destrs]
1622        start_lbl dest_lbl def
1623
1624    | AST.Op_cmpp AST.Cmp_ge, _, _, _ ->
1625      add_translates
1626        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
1627         translate_op1 AST.Op_notbool destrs destrs]
1628        start_lbl dest_lbl def
1629
1630    | _ -> assert false (* wrong number of arguments *)
1631*)
1632
1633definition translate_condcst ≝
1634  λcst.
1635  λstart_lbl: label.
1636  λlbl_true: label.
1637  λlbl_false: label.
1638  λdef.
1639  match cst with
1640  [ cast_int i ⇒
1641    let 〈def, tmpr〉 ≝ fresh_reg def in
1642    adds_graph [
1643      rtl_st_int tmpr i start_lbl;
1644      rtl_st_cond_acc tmpr lbl_true lbl_false
1645    ] start_lbl start_lbl def
1646  | cast_addr_symbol x ⇒
1647    let 〈def, r1〉 ≝ fresh_reg def in
1648    let 〈def, r2〉 ≝ fresh_reg def in
1649    let lbl ≝ fresh_label def in
1650    match lbl with
1651    [ None ⇒ None ?
1652    | Some lbl ⇒
1653      let def ≝ add_graph start_lbl (rtl_st_addr r1 r2 x lbl) def in
1654        translate_condptr r1 r2 lbl lbl_true lbl_false def
1655    ]
1656  | cast_stack_offset off ⇒
1657    let 〈def, r1〉 ≝ fresh_reg def in
1658    let 〈def, r2〉 ≝ fresh_reg def in
1659    let tmp_lbl ≝ fresh_label def in
1660    match tmp_lbl with
1661    [ None ⇒ None ?
1662    | Some tmp_lbl ⇒
1663      let def ≝ translate_cst (cast_stack_offset off) [r1; r2] start_lbl tmp_lbl def in
1664      match def with
1665      [ None ⇒ None ?
1666      | Some def ⇒ translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def
1667      ]
1668    ]
1669  | cast_float f ⇒ None ? (* error_float *)
1670  ].
1671
1672definition size_of_op1_ret ≝
1673  λop.
1674  match op with
1675  [ op_cast8_unsigned ⇒ Some ? 1
1676  | op_cast8_signed ⇒ Some ? 1
1677  | op_cast16_unsigned ⇒ Some ? 1
1678  | op_cast16_signed ⇒ Some ? 1
1679  | op_neg_int ⇒ Some ? 1
1680  | op_not_int ⇒ Some ? 1
1681  | op_int_of_ptr ⇒ Some ? 1
1682  | op_ptr_of_int ⇒ Some ? 2
1683  | op_id ⇒ None ? (* invalid_argument *)
1684  | _ ⇒ None ? (* error_float *)
1685  ].
1686
1687definition translate_cond1 ≝
1688  λop1.
1689  λsrcrs: list register.
1690  λstart_lbl: label.
1691  λlbl_true: label.
1692  λlbl_false: label.
1693  λdef.
1694  match op1 with
1695  [ op_id ⇒
1696    let srcr ≝ extract_singleton ? srcrs in
1697    match srcr with
1698    [ None ⇒
1699      let srcr12 ≝ extract_pair ? srcrs in
1700      match srcr12 with
1701      [ None ⇒ None ?
1702      | Some srcr12 ⇒
1703        let 〈srcr1, srcr2〉 ≝ srcr12 in
1704          translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def
1705      ]
1706    | Some srcr ⇒
1707      adds_graph [
1708        rtl_st_cond_acc srcr lbl_true lbl_false
1709      ] start_lbl start_lbl def
1710    ]
1711  | _     ⇒
1712    let size ≝ size_of_op1_ret op1 in
1713    match size with
1714    [ None ⇒ None ?
1715    | Some size ⇒
1716      let 〈def, destrs〉 ≝ fresh_regs def size in
1717      let lbl ≝ fresh_label def in
1718      match lbl with
1719      [ None ⇒ None ?
1720      | Some lbl ⇒
1721        let def ≝ translate_op1 op1 destrs srcrs start_lbl lbl def in
1722        match def with
1723        [ None ⇒ None ?
1724        | Some def ⇒
1725          let destr ≝ extract_singleton ? destrs in
1726          match destr with
1727          [ None ⇒
1728            let destr12 ≝ extract_pair ? destrs in
1729            match destr12 with
1730            [ None ⇒ None ?
1731            | Some destr12 ⇒
1732              let 〈destr1, destr2〉 ≝ destr12 in
1733                translate_condptr destr1 destr2 start_lbl lbl_true lbl_false def
1734            ]
1735          | Some destr ⇒
1736            adds_graph [
1737              rtl_st_cond_acc destr lbl_true lbl_false
1738            ] start_lbl start_lbl def
1739          ]
1740        ]
1741      ]
1742    ]
1743  ].
1744
1745definition size_of_op2_ret ≝
1746  λn: nat.
1747  λop2.
1748  match op2 with
1749  [ op_add ⇒ Some ? 1
1750  | op_sub ⇒ Some ? 1
1751  | op_mul ⇒ Some ? 1
1752  | op_div ⇒ Some ? 1
1753  | op_divu ⇒ Some ? 1
1754  | op_mod ⇒ Some ? 1
1755  | op_modu ⇒ Some ? 1
1756  | op_and ⇒ Some ? 1
1757  | op_or ⇒ Some ? 1
1758  | op_xor ⇒ Some ? 1
1759  | op_shl ⇒ Some ? 1
1760  | op_shr ⇒ Some ? 1
1761  | op_shru ⇒ Some ? 1
1762  | op_cmp _ ⇒ Some ? 1
1763  | op_cmpu _ ⇒ Some ? 1
1764  | op_cmpp _ ⇒ Some ? 1
1765  | op_addp ⇒ Some ? 2
1766  | op_subp ⇒
1767    if eq_nat n 4 then
1768      Some ? 1
1769    else
1770      Some ? 2
1771  | _ ⇒ None ? (* error_float *)
1772  ].
1773
1774axiom translate_op2:
1775  op2 → list register → list register → list register → label → label → rtl_internal_function → option rtl_internal_function.
1776
1777definition translate_cond2 ≝
1778  λop2.
1779  λsrcrs1: list register.
1780  λsrcrs2: list register.
1781  λstart_lbl: label.
1782  λlbl_true: label.
1783  λlbl_false: label.
1784  λdef.
1785  match op2 with
1786  [ op_cmp cmp ⇒
1787    match cmp with
1788    [ Compare_Equal ⇒
1789      let srcr1 ≝ extract_singleton ? srcrs1 in
1790      match srcr1 with
1791      [ None ⇒ None ?
1792      | Some srcr1 ⇒
1793        let srcr2 ≝ extract_singleton ? srcrs2 in
1794        match srcr2 with
1795        [ None ⇒ None ?
1796        | Some srcr2 ⇒
1797          let 〈def, tmpr〉 ≝ fresh_reg def in
1798          adds_graph [
1799            rtl_st_clear_carry start_lbl;
1800            rtl_st_op2 Sub tmpr srcr1 srcr2 start_lbl;
1801            rtl_st_cond_acc tmpr lbl_false lbl_true
1802          ] start_lbl start_lbl def
1803        ]
1804      ]
1805    | _ ⇒
1806      let n ≝ length ? srcrs1 + length ? srcrs2 in
1807      match size_of_op2_ret n op2 with
1808      [ None ⇒ None ?
1809      | Some size ⇒
1810        let 〈def, destrs〉 ≝ fresh_regs def size in
1811        let lbl ≝ fresh_label def in
1812        match lbl with
1813        [ None ⇒ None ?
1814        | Some lbl ⇒
1815          match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
1816          [ None ⇒ None ?
1817          | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
1818          ]
1819        ]
1820      ]
1821    ]
1822  | _ ⇒
1823    let n ≝ length ? srcrs1 + length ? srcrs2 in
1824    match size_of_op2_ret n op2 with
1825    [ None ⇒ None ?
1826    | Some size ⇒
1827      let 〈def, destrs〉 ≝ fresh_regs def size in
1828      let lbl ≝ fresh_label def in
1829      match lbl with
1830      [ None ⇒ None ?
1831      | Some lbl ⇒
1832        match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
1833        [ None ⇒ None ?
1834        | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
1835        ]
1836      ]
1837    ]
1838  ].
1839
1840let rec addressing_pointer (mode: ?) (args: ?) (destr1: ?)
1841                           (destr2: ?) (start_lbl: label)
1842                           (dest_lbl: label) (def: rtl_internal_function) ≝
1843  let destrs ≝ [ destr1; destr2 ] in
1844  match mode with
1845  [ Aindexed off ⇒
1846    let srcr12 ≝ extract_singleton ? args in
1847    match srcr12 with
1848    [ None ⇒ None ?
1849    | Some srcr12 ⇒
1850      let srcr12 ≝ extract_pair ? srcr12 in
1851      match srcr12 with
1852      [ None ⇒ None ?
1853      | Some srcr12 ⇒
1854        let 〈srcr1, srcr2〉 ≝ srcr12 in
1855        let 〈def, tmpr〉 ≝ fresh_reg def in
1856        add_translates [
1857          adds_graph [
1858            rtl_st_int tmpr off start_lbl
1859          ];
1860          translate_op2 op_addp destrs [ srcr1 ; srcr2 ] [tmpr]
1861        ] start_lbl dest_lbl def
1862      ]
1863    ]
1864  | Aindexed2 ⇒
1865    let args_pair ≝ extract_pair ? args in
1866    match args_pair with
1867    [ None ⇒ None ?
1868    | Some args_pair ⇒
1869      let 〈lft, rgt〉 ≝ args_pair in
1870      let srcr1112 ≝ extract_pair ? lft in
1871      let srcr2 ≝ extract_singleton ? rgt in
1872      match srcr1112 with
1873      [ None ⇒
1874        let srcr2 ≝ extract_singleton ? rgt in
1875        let srcr1112 ≝ extract_pair ? lft in
1876        match srcr2 with
1877        [ None ⇒ None ?
1878        | Some srcr2 ⇒
1879          match srcr1112 with
1880          [ None ⇒ None ?
1881          | Some srcr1112 ⇒
1882            let 〈srcr11, srcr12〉 ≝ srcr1112 in
1883            translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
1884          ]
1885        ]
1886      | Some srcr1112 ⇒
1887        let 〈srcr11, srcr12〉 ≝ srcr1112 in
1888        match srcr2 with
1889        [ None ⇒ None ?
1890        | Some srcr2 ⇒
1891          translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
1892        ]
1893      ]
1894    ]
1895  | Aglobal x off ⇒
1896    let 〈def, tmpr〉 ≝ fresh_reg def in
1897    add_translates [
1898      adds_graph [
1899        rtl_st_int tmpr off start_lbl;
1900        rtl_st_addr destr1 destr2 x start_lbl
1901      ];
1902      translate_op2 op_addp destrs destrs [ tmpr ]
1903    ] start_lbl dest_lbl def
1904  | Abased x off ⇒
1905    let srcrs ≝ extract_singleton ? args in
1906    match srcrs with
1907    [ None ⇒ None ?
1908    | Some srcrs ⇒
1909      let 〈def, tmpr1〉 ≝ fresh_reg def in
1910      let 〈def, tmpr2〉 ≝ fresh_reg def in
1911      (* mode, args, destr1, destr2, start_lbl, dest_lbl, def *)
1912      (* addressing_pointer (Aglobal x off) [ ] tmpr1 tmpr2; *)
1913      let address_unfold ≝
1914        let 〈def, tmpr〉 ≝ fresh_reg def in
1915          add_translates [
1916            adds_graph [
1917              rtl_st_int tmpr off start_lbl;
1918              rtl_st_addr tmpr1 tmpr2 x start_lbl
1919           ];
1920            translate_op2 op_addp destrs destrs [ tmpr ]
1921         ]
1922      in
1923      add_translates [
1924        address_unfold;
1925        translate_op2 op_addp destrs [ tmpr1; tmpr2 ] srcrs
1926      ] start_lbl dest_lbl def
1927    ]
1928  | Ainstack off ⇒
1929    let 〈def, tmpr〉 ≝ fresh_reg def in
1930    add_translates [
1931      adds_graph [
1932        rtl_st_int tmpr off start_lbl;
1933        rtl_st_stack_addr destr1 destr2 start_lbl
1934      ];
1935      translate_op2 op_addp destrs destrs [ tmpr ]
1936    ] start_lbl dest_lbl def
1937  | _ ⇒ None ? (* wrong number of arguments *)
1938  ].
1939
1940definition translate_load ≝
1941  λq.
1942  λmode.
1943  λargs.
1944  λdestrs.
1945  λstart_lbl: label.
1946  λdest_lbl: label.
1947  λdef.
1948  match q with
1949  [ q_int b ⇒
1950    if eq_bv ? b (bitvector_of_nat ? 1) then
1951      match extract_singleton ? destrs with
1952      [ None ⇒ None ? (* error: size error in load *)
1953      | Some destr ⇒
1954        let 〈def, addr1〉 ≝ fresh_reg def in
1955        let 〈def, addr2〉 ≝ fresh_reg def in
1956          Some ? (add_translates [
1957            addressing_pointer mode args addr1 addr2;
1958            adds_graph [
1959              rtl_st_load destr addr1 addr2 start_lbl
1960            ]
1961          ] start_lbl dest_lbl def)
1962      ]
1963    else
1964      None ? (* error: size error in load *)
1965  | q_ptr ⇒
1966    match extract_pair ? destrs with
1967    [ None ⇒ None ? (* error: size error in load *)
1968    | Some destr12 ⇒
1969      let 〈destr1, destr2〉 ≝ destr12 in
1970      let 〈def, addr1〉 ≝ fresh_reg def in
1971      let 〈def, addr2〉 ≝ fresh_reg def in
1972      let addr ≝ [ addr1; addr2 ] in
1973      let 〈def, tmpr〉 ≝ fresh_reg def in
1974        Some ? (
1975          add_translates [
1976            addressing_pointer mode args addr1 addr2;
1977            adds_graph [
1978              rtl_st_load destr1 addr1 addr2 start_lbl;
1979              rtl_st_int tmpr (bitvector_of_nat ? 1) start_lbl
1980            ];
1981            translate_op2 op_addp addr addr [ tmpr ];
1982            adds_graph [
1983              rtl_st_load destr2 addr1 addr2 start_lbl
1984            ]
1985          ] start_lbl dest_lbl def
1986        )
1987    ]
1988  | _ ⇒ None ? (* error: size error in load *)
1989  ].
1990 
1991definition make_addr ≝
1992  λA: Type[0].
1993  λlst: list A.
1994  match lst with
1995  [ cons hd tl ⇒
1996    match tl with
1997    [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
1998    | _ ⇒ None ? (* do not use on these arguments *)
1999    ]
2000  | _ ⇒ None ? (* do not use on these arguments *)
2001  ].
2002 
2003definition translate_store_internal ≝
2004  λaddr.
2005  λtmp_addr.
2006  λtmpr.
2007  λstart_lbl.
2008  λdest_lbl.
2009  λtmp_addr1.
2010  λtmp_addr2.
2011  λtranslates_off.
2012  λsrcr.
2013    let 〈translates, off〉 ≝ translates_off in
2014    let translates ≝ translates @
2015      [ adds_graph [
2016          rtl_st_int tmpr off start_lbl
2017        ];
2018        translate_op2 op_addp tmp_addr addr [ tmpr ];
2019        adds_graph [
2020          rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
2021        ]
2022      ]
2023    in
2024    let 〈ignore, result〉 ≝ half_add ? off int_size in
2025      〈translates, result〉.
2026 
2027definition translate_store ≝
2028  λaddr.
2029  λsrcrs.
2030  λstart_lbl.
2031  λdest_lbl.
2032  λdef.
2033    let 〈def, tmp_addr〉 ≝ fresh_regs def (length ? addr) in
2034    match make_addr ? tmp_addr with
2035    [ None ⇒ None ?
2036    | Some tmp_addr12 ⇒
2037      let 〈tmp_addr1, tmp_addr2〉 ≝ tmp_addr12 in
2038      let 〈def, tmpr〉 ≝ fresh_reg def in
2039      let f ≝ translate_store_internal addr tmp_addr tmpr start_lbl dest_lbl tmp_addr1 tmp_addr2 in
2040      let 〈translates, ignore〉 ≝ foldl ? ? f 〈[], zero ?〉 srcrs in
2041        add_translates translates start_lbl dest_lbl def
2042    ].
2043
2044definition translate_stmt ≝
2045  λlenv.
2046  λlbl.
2047  λstmt.
2048  λdef.
2049  match stmt with
2050  [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
2051  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
2052  | St_cast destr cst lbl' ⇒
2053      translate_cst cst (find_local_env destr lenv) lbl lbl' def
2054  | _ ⇒ ?
2055  ].
2056
2057let translate_stmt lenv lbl stmt def = match stmt with
2058
2059  | RTLabs.St_skip lbl' ->
2060    add_graph lbl (RTL.St_skip lbl') def
2061
2062  | RTLabs.St_cost (cost_lbl, lbl') ->
2063    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
2064
2065  | RTLabs.St_cst (destr, cst, lbl') ->
2066    translate_cst cst (find_local_env destr lenv) lbl lbl' def
2067
2068  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
2069    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
2070      lbl lbl' def
2071
2072  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
2073    translate_op2 op2 (find_local_env destr lenv)
2074      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
2075
2076  | RTLabs.St_load (_, addr, destr, lbl') ->
2077    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
2078      lbl lbl' def
2079
2080  | RTLabs.St_store (_, addr, srcr, lbl') ->
2081    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
2082      lbl lbl' def
2083
2084  | RTLabs.St_call_id (f, args, None, _, lbl') ->
2085    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
2086
2087  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
2088    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
2089                                   find_local_env retr lenv, lbl')) def
2090
2091  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
2092    let (f1, f2) = find_and_addr f lenv in
2093    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
2094
2095  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
2096    let (f1, f2) = find_and_addr f lenv in
2097    add_graph lbl
2098      (RTL.St_call_ptr
2099         (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
2100
2101  | RTLabs.St_tailcall_id (f, args, _) ->
2102    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
2103
2104  | RTLabs.St_tailcall_ptr (f, args, _) ->
2105    let (f1, f2) = find_and_addr f lenv in
2106    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
2107
2108  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
2109    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
2110
2111  | RTLabs.St_jumptable _ ->
2112    error "Jump tables not supported yet."
2113
2114  | RTLabs.St_return None ->
2115    add_graph lbl (RTL.St_return []) def
2116
2117  | RTLabs.St_return (Some r) ->
2118    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
Note: See TracBrowser for help on using the repository browser.