source: src/RTLabs/RTLAbstoRTL.ma @ 1063

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

changes from today

File size: 51.5 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
127definition size_of_sig_type ≝
128  λsig.
129  match sig with
130  [ ASTint isize sign ⇒
131    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
132      isize' ÷ (nat_of_bitvector ? int_size)
133  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
134  | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
135  ].
136  cases not_implemented;
137qed.
138
139inductive register_type: Type[0] ≝
140  | register_int: register → register_type
141  | register_ptr: register → register → register_type.
142
143definition local_env ≝ BitVectorTrie (list register).
144
145definition mem_local_env ≝
146  λr: register.
147  match r with
148  [ an_identifier w ⇒ member (list register) 16 w
149  ].
150
151definition add_local_env ≝
152  λr: register.
153  match r with
154  [ an_identifier w ⇒ insert (list register) 16 w
155  ].
156
157definition find_local_env ≝
158  λr: register.
159  λbvt.
160  match r with
161  [ an_identifier w ⇒ lookup (list register) 16 w bvt [ ]
162  ].
163
164definition initialize_local_env_internal ≝
165  λruniverse.
166  λlenv.
167  λr_sig.
168  let 〈r, sig〉 ≝ r_sig in
169  let size ≝ size_of_sig_type sig in
170  let rs ≝ register_freshes runiverse size in
171    add_local_env r rs lenv.
172
173definition initialize_local_env ≝
174  λruniverse.
175  λregisters.
176  λresult.
177  let registers ≝ registers @
178    match result with
179    [ None ⇒ [ ]
180    | Some rt ⇒ [ rt ]
181    ]
182  in
183    foldl ? ? (initialize_local_env_internal runiverse) (Stub …) registers.
184 
185definition map_list_local_env_internal ≝
186  λlenv.
187  λres.
188  λr.
189    res @ (find_local_env r lenv).
190   
191definition map_list_local_env ≝
192  λlenv.
193  λregs.
194    foldl ? ? (map_list_local_env_internal lenv) [ ] regs.
195
196definition make_addr ≝
197  λA.
198  λlst: list A.
199  λprf: length A lst = 2. (* do not use on arguments other than those of length 2 *)
200  match lst return λx. length A x = 2 → A × A with
201  [ nil ⇒ λlst_nil_prf. ?
202  | cons hd tl ⇒ λprf.
203    match tl return λx. length A x = 1 → A × A with
204    [ nil ⇒ λtl_nil_prf. ?
205    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
206    ] ?
207  ] prf.
208  [1: normalize in lst_nil_prf;
209      destruct(lst_nil_prf);
210  |2: normalize in prf;
211      destruct(prf)
212      @e0
213  |3: normalize in tl_nil_prf;
214      destruct(tl_nil_prf);
215  ]
216qed.
217
218definition find_and_addr ≝
219  λr.
220  λlenv.
221    make_addr ? (find_local_env r lenv).
222
223definition rtl_args ≝
224  λregs_list.
225  λlenv.
226    flatten ? (map ? ? (
227      λr. find_local_env r lenv) regs_list).
228
229definition change_label ≝
230  λlbl.
231  λstmt: rtl_statement.
232  match stmt with
233  [ rtl_st_skip _ ⇒ rtl_st_skip lbl
234  | rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl
235  | rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl
236  | rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl
237  | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
238  | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
239  | rtl_st_opaccs opaccs d s1 s2 s3 _ ⇒ rtl_st_opaccs opaccs d s1 s2 s3 lbl
240  | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
241  | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
242  | rtl_st_clear_carry _ ⇒ rtl_st_clear_carry lbl
243  | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl
244  | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl
245  | rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl
246  | rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl
247  | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a
248  | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
249  | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2
250  | rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl
251  | rtl_st_set_carry l ⇒ rtl_st_set_carry lbl
252  | rtl_st_return r ⇒ rtl_st_return r
253  ].
254
255(* Ack! Should generating a fresh label ever fail?  This seems to be a side-effect
256   of implementing everything as a bitvector, which is bounded.  If we implemented
257   labels as unbounded nats then this function will never fail.
258*)
259(* Fixed with changes to label generation.
260*)
261let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝
262  match stmt_list with
263  [ nil ⇒ def
264  | cons hd tl ⇒
265    match tl with
266    [ nil ⇒ add_graph start_lbl (change_label dest_lbl hd) def
267    | cons hd' tl' ⇒
268      let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
269      let stmt ≝ change_label tmp_lbl hd in
270      let def ≝ add_graph start_lbl stmt new_def in
271        adds_graph tl tmp_lbl dest_lbl new_def
272    ]
273  ].
274
275let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
276                       (def: ?) on translate_list ≝
277  match translate_list with
278  [ nil ⇒ def
279  | cons hd tl ⇒
280    match tl with
281    [ nil ⇒ hd start_lbl dest_lbl def
282    | cons hd' tl' ⇒
283      let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
284      let applied ≝ hd start_lbl tmp_lbl new_def in
285        add_translates tl tmp_lbl dest_lbl applied
286    ]
287  ].
288
289definition translate_cst_int_internal ≝
290  λdest_lbl.
291  λr.
292  λi.
293    rtl_st_int r i dest_lbl.
294
295axiom translate_cst:
296  ∀cst: constant.
297  ∀destrs: list register.
298  ∀start_lbl: label.
299  ∀dest_lbl: label.
300  ∀def: rtl_internal_function.
301    rtl_internal_function.
302
303definition translate_move_internal ≝
304  λstart_lbl: label.
305  λdestr: register.
306  λsrcr: register.
307    rtl_st_move destr srcr start_lbl.
308
309definition translate_move ≝
310  λdestrs: list register.
311  λsrcrs: list register.
312  λstart_lbl: label.
313    match reduce_strong register destrs srcrs with
314    [ dp crl_crr len_proof ⇒
315      let commonl ≝ \fst (\fst crl_crr) in
316      let commonr ≝ \fst (\snd crl_crr) in
317      let restl ≝ \snd (\fst crl_crr) in
318      let restr ≝ \snd (\snd crl_crr) in
319      let f_common ≝ translate_move_internal start_lbl in
320      let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
321      let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
322        add_translates [ translate1 ; translate2 ] start_lbl
323    ].
324    @len_proof
325qed.
326
327let rec make
328  (A: Type[0]) (elt: A) (n: nat) on n ≝
329  match n with
330  [ O ⇒ [ ]
331  | S n' ⇒ elt :: make A elt n'
332  ].
333 
334lemma make_length:
335  ∀A: Type[0].
336  ∀elt: A.
337  ∀n: nat.
338    n = length ? (make A elt n).
339  #A #ELT #N
340  elim N
341  [ normalize %
342  | #N #IH
343    normalize <IH %
344  ]
345qed.
346
347definition translate_cast_unsigned ≝
348  λdestrs.
349  λstart_lbl.
350  λdest_lbl.
351  λdef.
352  let 〈def, tmp_zero〉 ≝ fresh_reg def in
353  let zeros ≝ make ? tmp_zero (length ? destrs) in
354    add_translates [
355      adds_graph [
356        rtl_st_int tmp_zero (bitvector_of_nat ? 0) start_lbl
357        ];
358      translate_move destrs zeros
359    ] start_lbl dest_lbl def.
360
361definition translate_cast_signed ≝
362  λdestrs.
363  λsrcr.
364  λstart_lbl.
365  λdest_lbl.
366  λdef.
367  let 〈def, tmp_128〉 ≝ fresh_reg def in
368  let 〈def, tmp_255〉 ≝ fresh_reg def in
369  let 〈def, tmpr〉 ≝ fresh_reg def in
370  let 〈def, dummy〉 ≝ fresh_reg def in
371  let insts ≝ [
372    rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl;
373    rtl_st_op2 And tmpr tmp_128 srcr start_lbl;
374    rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl;
375    rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl;
376    rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl
377  ] in
378  let srcrs ≝ make ? tmpr (length ? destrs) in
379    add_translates [
380      adds_graph insts;
381      translate_move destrs srcrs
382    ] start_lbl dest_lbl def.
383
384definition translate_cast ≝
385  λsrc_size.
386  λsrc_sign.
387  λdest_size.
388  λdestrs.
389  λsrcrs.
390  match | srcrs | return λx. | srcrs | = x → ? with
391  [ O ⇒ λzero_prf. adds_graph [ ]
392  | S n' ⇒ λsucc_prf.
393    if ltb dest_size src_size then
394      translate_move destrs srcrs
395    else
396      match reduce_strong ? destrs srcrs with
397      [ dp crl len_proof ⇒
398        let commonl ≝ \fst (\fst crl) in
399        let commonr ≝ \fst (\snd crl) in
400        let restl ≝ \snd (\fst crl) in
401        let restr ≝ \snd (\snd crl) in
402        let insts_common ≝ translate_move commonl commonr in
403        let sign_reg ≝ last_safe ? srcrs ? in
404        let insts_sign ≝
405          match src_sign with
406          [ Unsigned ⇒ translate_cast_unsigned restl
407          | Signed ⇒ translate_cast_signed restl sign_reg
408          ]
409        in
410          add_translates [ insts_common; insts_sign ]
411      ]
412  ] (refl ? (|srcrs|)).
413  >succ_prf //
414qed.
415
416definition translate_negint ≝
417  λdestrs.
418  λsrcrs.
419  λstart_lbl.
420  λdest_lbl.
421  λdef.
422  λprf: | destrs | = | srcrs |. (* assert in caml code *)
423  let 〈def, tmpr〉 ≝ fresh_reg def in
424  let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
425  let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in
426  let insts_init ≝ [
427    rtl_st_set_carry start_lbl;
428    rtl_st_int tmpr (zero ?) start_lbl
429  ] in
430  let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lbl in
431  let insts_add ≝ map … f_add destrs in
432    adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
433
434definition translate_notbool ≝
435  λdestrs.
436  λsrcrs.
437  λstart_lbl.
438  λdest_lbl.
439  λdef.
440  match destrs with
441  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
442  | cons destr destrs ⇒
443    let 〈def, tmpr〉 ≝ fresh_reg def in
444    let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in
445    let save_srcrs ≝ translate_move tmp_srcrs srcrs in
446    let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lbl in
447    let f ≝ λtmp_srcr. [
448      rtl_st_clear_carry start_lbl;
449      rtl_st_int tmpr (zero ?) start_lbl;
450      rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl;
451      rtl_st_int tmpr (zero ?) start_lbl;
452      rtl_st_op2 Addc tmpr tmpr tmpr start_lbl;
453      rtl_st_op2 Xor destr destr tmpr start_lbl
454    ] in
455    let insts ≝ init_destr :: (flatten ? (map … f tmp_srcrs)) in
456    let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in
457      add_translates [
458        save_srcrs; adds_graph insts; epilogue
459      ] start_lbl dest_lbl def
460  ].
461
462definition translate_intermediate_op1 ≝
463  λop1.
464  λdestrs.
465  λsrcrs.
466  λstart_lbl.
467  λdest_lbl.
468  λdef.
469  λprf: |destrs| = |srcrs|.
470  match op1 with
471  [ intermediate_op1_cast src_size src_sign dest_size ⇒
472      translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
473  | intermediate_op1_negint ⇒
474      translate_negint destrs srcrs start_lbl dest_lbl def prf
475  | intermediate_op1_notbool ⇒
476      translate_notbool destrs srcrs start_lbl dest_lbl def
477  | intermediate_op1_notint ⇒
478    let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
479    let l ≝ map2 … f destrs srcrs prf in
480      adds_graph l start_lbl dest_lbl def
481  | intermediate_op1_ptrofint ⇒
482      translate_move destrs srcrs start_lbl dest_lbl def
483  | intermediate_op1_intofptr ⇒
484      translate_move destrs srcrs start_lbl dest_lbl def
485  | intermediate_op1_id ⇒
486      translate_move destrs srcrs start_lbl dest_lbl def
487  ].
488 
489definition translate_op ≝
490  λop.
491  λdestrs.
492  λsrcrs1.
493  λsrcrs2.
494  λprf: |srcrs1| = |srcrs2|.
495  λstart_lbl.
496  λdest_lbl.
497  λdef.
498  match reduce_strong ? srcrs1 srcrs2 with
499  [ dp reduced first_reduced_proof ⇒
500    let srcrsl_common ≝ \fst (\fst reduced) in
501    let srcrsr_common ≝ \fst (\snd reduced) in
502    let srcrsl_rest ≝ \snd (\fst reduced) in
503    let srcrsr_rest ≝ \snd (\snd reduced) in
504    let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ? in
505    match reduce_strong ? destrs srcrsl_common with
506    [ dp reduced second_reduced_proof ⇒
507      let destrs_common ≝ \fst (\fst reduced) in
508      let destrs_rest ≝ \snd (\fst reduced) in
509      match reduce_strong ? destrs_rest srcrs_rest with
510      [ dp reduced third_reduced_proof ⇒
511        let destrs_cted ≝ \fst (\fst reduced) in
512        let destrs_rest ≝ \snd (\fst reduced) in
513        let srcrs_cted ≝ \fst (\snd reduced) in
514        let 〈def, tmpr〉 ≝ fresh_reg def in
515        let insts_init ≝ [
516          rtl_st_clear_carry start_lbl;
517          rtl_st_int tmpr (zero ?) start_lbl
518        ] in
519        let f_add ≝ λdestr. λsrcr1. λsrcr2. rtl_st_op2 op destr srcr1 srcr2 start_lbl in
520        let insts_add ≝ map3 … f_add destrs_common srcrsl_common srcrsr_common ? ? in
521        let f_add_cted ≝ λdestr. λsrcr. rtl_st_op2 op destr srcr tmpr start_lbl in
522        let insts_add_cted ≝ map2 ? ? ? f_add_cted destrs_cted srcrs_cted ? in
523        let f_rest ≝ λdestr. rtl_st_op2 op destr tmpr tmpr start_lbl in
524        let insts_rest ≝ map … f_rest destrs_rest in
525          adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
526      ]
527    ]
528  ].
529cases not_implemented (* problem here with lengths of lists: possible bug? *)
530qed.
531
532let rec translate_mul1
533  (dummy: register) (tmpr: register) (destrs: list register)
534  (srcrs1: list register) (srcr2: register) (start_lbl: label)
535    on srcrs1 ≝
536  match destrs with
537  [ nil ⇒ adds_graph [ rtl_st_skip start_lbl ] start_lbl
538  | cons destr tl ⇒
539    match tl with
540    [ nil ⇒
541      match srcrs1 with
542      [ nil ⇒
543        adds_graph [
544          rtl_st_int tmpr (zero ?) start_lbl;
545          rtl_st_op2 Addc destr destr tmpr start_lbl
546        ] start_lbl
547      | cons srcr1 tl' ⇒
548        adds_graph [
549          rtl_st_opaccs Mul tmpr dummy srcr2 srcr1 start_lbl;
550          rtl_st_op2 Addc destr destr tmpr start_lbl
551        ] start_lbl
552      ]
553    | cons destr2 destrs ⇒
554      match srcrs1 with
555      [ nil ⇒
556        add_translates [
557          adds_graph [
558            rtl_st_int tmpr (zero ?) start_lbl;
559            rtl_st_op2 Addc destr destr tmpr start_lbl;
560            rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
561          ];
562          translate_cst (Ointconst I8 (zero ?)) destrs
563        ] start_lbl
564      | cons srcr1 srcrs1 ⇒
565        match destrs with
566        [ nil ⇒
567          add_translates [
568            adds_graph [
569              rtl_st_int tmpr (zero ?) start_lbl;
570              rtl_st_op2 Addc destr destr tmpr start_lbl;
571              rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
572            ];
573            translate_cst (Ointconst I8 (zero ?)) destrs
574          ] start_lbl
575        | cons destr2 destrs ⇒
576          add_translates [
577            adds_graph [
578              rtl_st_opaccs Mul tmpr destr2 srcr2 srcr1 start_lbl;
579              rtl_st_op2 Addc destr destr tmpr start_lbl
580            ];
581            translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2
582          ] start_lbl
583        ]
584      ]
585    ]
586  ].
587
588definition translate_muli ≝
589  λdummy: register.
590  λtmpr: register.
591  λdestrs: list register.
592  λtmp_destrs: list register.
593  λdestrs_prf: |destrs| = |tmp_destrs|.
594  λsrcrs1: list register.
595  λdummy_lbl: label.
596  λi: nat.
597  λi_prf.
598  λtranslates: list ?.
599  λsrcr2i: register.
600  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split ? tmp_destrs i i_prf in
601  let tmp_destrs2' ≝
602    match tmp_destrs2 with
603    [ nil ⇒ [ ]
604    | cons tmp_destr2 tmp_destrs2 ⇒ [
605        adds_graph [
606          rtl_st_clear_carry dummy_lbl;
607          rtl_st_int tmp_destr2 (zero ?) dummy_lbl
608        ];
609        translate_mul1 dummy tmpr tmp_destrs2 srcrs1 srcr2i;
610        translate_cst (Ointconst I8 (zero ?)) tmp_destrs1;
611        adds_graph [
612          rtl_st_clear_carry dummy_lbl
613        ];
614        translate_op Addc destrs destrs tmp_destrs destrs_prf
615      ]
616    ]
617  in
618    translates @ tmp_destrs2'.
619
620definition translate_mul ≝
621  λdestrs: list register.
622  λsrcrs1: list register.
623  λsrcrs2: list register.
624  λstart_lbl: label.
625  λdest_lbl: label.
626  λdef: rtl_internal_function.
627  let 〈def, dummy〉 ≝ fresh_reg def in
628  let 〈def, tmpr〉 ≝ fresh_reg def in
629  let 〈def, tmp_destrs〉 ≝ fresh_regs def (|destrs|) in
630  let 〈def, fresh_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
631  let 〈def, fresh_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
632  let insts_init ≝ [
633    translate_move fresh_srcrs1 srcrs1;
634    translate_move fresh_srcrs2 srcrs2;
635    translate_cst (Ointconst I8 (zero ?)) destrs
636  ]
637  in
638  let f ≝ λi. translate_muli dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in
639  let insts_mul ≝ foldi ? ? [ ] srcrs2 in ?. [5: check insts_init.
640    add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
641
642let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
643  let (def, dummy) = fresh_reg def in
644  let (def, tmpr) = fresh_reg def in
645  let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
646  let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in
647  let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in
648  let insts_init =
649    [translate_move fresh_srcrs1 srcrs1 ;
650     translate_move fresh_srcrs2 srcrs2 ;
651     translate_cst (AST.Cst_int 0) destrs] in
652  let f = λi. translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl i ? in
653  let insts_mul = MiscPottier.foldi f [] srcrs2 in
654  add_translates (insts_init @ insts_mul) start_lbl dest_lbl def
655
656definition filter_and_to_list_local_env_internal ≝
657  λlenv.
658  λl.
659  λr.
660  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
661  [ Some entry ⇒
662    match entry with
663    [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ])
664    | register_int r ⇒ (l @ [ r ])
665    ]
666  | None       ⇒ [ ] (* dpm: should this be none? *)
667  ].
668
669definition filter_and_to_list_local_env ≝
670  λlenv.
671  λregisters.
672    foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers.
673
674definition list_of_register_type ≝
675  λrt.
676  match rt with
677  [ register_ptr r1 r2 ⇒ [ r1; r2 ]
678  | register_int r ⇒ [ r ]
679  ].
680
681definition find_and_list ≝
682  λr.
683  λlenv.
684  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
685  [ None      ⇒ [ ] (* dpm: should this be none? *)
686  | Some lkup ⇒ list_of_register_type lkup
687  ].
688
689definition find_and_list_args ≝
690  λargs.
691  λlenv.
692    map ? ? (λr. find_and_list r lenv) args.
693 
694(* dpm: horrendous, use dependent types.
695  length destr = length srcrs *)
696let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label)
697                       (dest_lbl: label) (def: ?) ≝
698  match destrs with
699  [ nil ⇒
700    match srcrs with
701    [ nil        ⇒ Some ? def
702    | cons hd tl ⇒ None ?
703    ]
704  | cons hd tl ⇒
705    match srcrs with
706    [ nil        ⇒ None ?
707    | cons hd' tl' ⇒
708      match tl with
709      [ nil            ⇒
710        match tl' with
711        (* one element lists *)
712        [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def)
713        | cons hd'' tl'' ⇒ None ?
714        ]
715      | cons hd'' tl'' ⇒
716        match tl' with
717        [ nil ⇒ None ?
718        (* multielement lists *)
719        | cons hd''' tl''' ⇒
720          let tmp_lbl ≝ fresh_label def in
721          match tmp_lbl with
722          [ None ⇒ None ?
723          | Some tmp_lbl ⇒
724            let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in
725              translate_move tl tl' tmp_lbl dest_lbl def
726          ]
727        ]
728      ]
729    ]
730  ].
731
732definition extract_singleton ≝
733  λA: Type[0].
734  λl: list A.
735  match l with
736  [ nil ⇒ None ?
737  | cons hd tl ⇒
738    match tl with
739    [ nil ⇒ Some ? hd
740    | cons hd tl ⇒ None ?
741    ]
742  ].
743
744definition extract_pair ≝
745  λA: Type[0].
746  λl: list A.
747  match l with
748  [ nil ⇒ None ?
749  | cons hd tl ⇒
750    match tl with
751    [ nil ⇒ None ?
752    | cons hd' tl' ⇒
753      match tl' with
754      [ nil ⇒ Some ? 〈hd, hd'〉
755      | cons hd'' tl'' ⇒ None ?
756      ]
757    ]
758  ].
759
760definition translate_op1 ≝
761  λop1.
762  λdestrs.
763  λsrcrs.
764  λstart_lbl.
765  λdest_lbl.
766  λdef.
767  match op1 with
768  [ op_cast8_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
769  | op_cast8_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
770  | op_cast16_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
771  | op_cast16_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
772  | op_neg_int ⇒
773    let dstr ≝ extract_singleton ? destrs in
774    let srcr ≝ extract_singleton ? srcrs in
775    match dstr with
776    [ None ⇒ None ?
777    | Some dstr ⇒
778      match srcr with
779      [ None ⇒ None ?
780      | Some srcr ⇒
781        adds_graph [
782          rtl_st_op1 Cmpl dstr srcr start_lbl;
783          rtl_st_op1 Inc dstr dstr start_lbl
784        ] start_lbl dest_lbl def
785      ]
786    ]
787  | op_not_int ⇒
788    let dstr ≝ extract_singleton ? destrs in
789    let srcr ≝ extract_singleton ? srcrs in
790    match dstr with
791    [ None ⇒ None ?
792    | Some dstr ⇒
793      match srcr with
794      [ None ⇒ None ?
795      | Some srcr ⇒
796        adds_graph [
797          rtl_st_op1 Cmpl dstr srcr start_lbl
798        ] start_lbl dest_lbl def
799      ]
800    ]
801  | op_id ⇒ translate_move destrs srcrs start_lbl dest_lbl def
802  | op_ptr_of_int ⇒
803    let destr12 ≝ extract_pair ? destrs in
804    let srcr ≝ extract_singleton ? srcrs in
805    match destr12 with
806    [ None ⇒ None ?
807    | Some destr12 ⇒
808      let 〈destr1, destr2〉 ≝ destr12 in
809      match srcr with
810      [ None ⇒ None ?
811      | Some srcr ⇒
812        adds_graph [
813          rtl_st_move destr1 srcr dest_lbl;
814          rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl
815        ] start_lbl dest_lbl def
816      ]
817    ]
818  | op_int_of_ptr ⇒
819    let destr ≝ extract_singleton ? destrs in
820    match destr with
821    [ None ⇒ None ?
822    | Some destr ⇒
823      match srcrs with
824      [ nil ⇒ None ?
825      | cons srcr tl ⇒
826        Some ? (add_graph start_lbl (rtl_st_move destr srcr dest_lbl) def)
827      ]
828    ]
829  | op_not_bool ⇒
830    let destr ≝ extract_singleton ? destrs in
831    let srcrs ≝ extract_singleton ? srcrs in
832    match destr with
833    [ None ⇒ None ?
834    | Some destr ⇒
835      match srcrs with
836      [ None ⇒ None ?
837      | Some srcr ⇒
838        let 〈def, tmpr〉 ≝ fresh_reg def in
839        adds_graph [
840          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
841          rtl_st_clear_carry start_lbl;
842          rtl_st_op2 Sub destr tmpr srcr start_lbl;
843          rtl_st_int destr (bitvector_of_nat ? 0) dest_lbl;
844          rtl_st_op2 Addc destr destr destr start_lbl;
845          rtl_st_int tmpr (bitvector_of_nat ? 1) dest_lbl;
846          rtl_st_op2 Xor destr destr tmpr start_lbl
847        ] start_lbl dest_lbl def
848      ]
849    ]
850  | _ ⇒ None ? (* error float *)
851  ].
852
853definition translate_condptr ≝
854  λr1.
855  λr2.
856  λstart_lbl: label.
857  λlbl_true: label.
858  λlbl_false: label.
859  λdef.
860  let 〈def, tmpr〉 ≝ fresh_reg def in
861    adds_graph [
862      rtl_st_op2 Or tmpr r1 r2 start_lbl;
863      rtl_st_cond_acc tmpr lbl_true lbl_false
864    ] start_lbl start_lbl def.
865
866(*
867let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?)
868                      (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝
869  match op2 with
870  [ op_add ⇒
871    let destr ≝ extract_singleton ? destrs in
872    let srcr1 ≝ extract_singleton ? srcrs1 in
873    let srcr2 ≝ extract_singleton ? srcrs2 in
874    match destr with
875    [ None ⇒ None ?
876    | Some destr ⇒
877      match srcr1 with
878      [ None ⇒ None ?
879      | Some srcr1 ⇒
880        match srcr2 with
881        [ None ⇒ None ?
882        | Some srcr2 ⇒
883          adds_graph [
884            rtl_st_op2 Add destr srcr1 srcr2 start_lbl
885          ] start_lbl dest_lbl def
886        ]
887      ]
888    ]
889  | op_sub ⇒
890    let destr ≝ extract_singleton ? destrs in
891    let srcr1 ≝ extract_singleton ? srcrs1 in
892    let srcr2 ≝ extract_singleton ? srcrs2 in
893    match destr with
894    [ None ⇒ None ?
895    | Some destr ⇒
896      match srcr1 with
897      [ None ⇒ None ?
898      | Some srcr1 ⇒
899        match srcr2 with
900        [ None ⇒ None ?
901        | Some srcr2 ⇒
902          adds_graph [
903            rtl_st_clear_carry start_lbl;
904            rtl_st_op2 Sub destr srcr1 srcr2 start_lbl
905          ] start_lbl dest_lbl def
906        ]
907      ]
908    ]
909  | op_mul ⇒
910    let destr ≝ extract_singleton ? destrs in
911    let srcr1 ≝ extract_singleton ? srcrs1 in
912    let srcr2 ≝ extract_singleton ? srcrs2 in
913    match destr with
914    [ None ⇒ None ?
915    | Some destr ⇒
916      match srcr1 with
917      [ None ⇒ None ?
918      | Some srcr1 ⇒
919        match srcr2 with
920        [ None ⇒ None ?
921        | Some srcr2 ⇒
922          adds_graph [
923            rtl_st_opaccs Mul destr srcr1 srcr2 start_lbl
924          ] start_lbl dest_lbl def
925        ]
926      ]
927    ]
928  | op_div ⇒ None ? (* signed div not supported *)
929  | op_divu ⇒
930    let destr ≝ extract_singleton ? destrs in
931    let srcr1 ≝ extract_singleton ? srcrs1 in
932    let srcr2 ≝ extract_singleton ? srcrs2 in
933    match destr with
934    [ None ⇒ None ?
935    | Some destr ⇒
936      match srcr1 with
937      [ None ⇒ None ?
938      | Some srcr1 ⇒
939        match srcr2 with
940        [ None ⇒ None ?
941        | Some srcr2 ⇒
942          adds_graph [
943            rtl_st_opaccs Divu destr srcr1 srcr2 start_lbl
944          ] start_lbl dest_lbl def
945        ]
946      ]
947    ]
948  | op_modu ⇒
949    let destr ≝ extract_singleton ? destrs in
950    let srcr1 ≝ extract_singleton ? srcrs1 in
951    let srcr2 ≝ extract_singleton ? srcrs2 in
952    match destr with
953    [ None ⇒ None ?
954    | Some destr ⇒
955      match srcr1 with
956      [ None ⇒ None ?
957      | Some srcr1 ⇒
958        match srcr2 with
959        [ None ⇒ None ?
960        | Some srcr2 ⇒
961          adds_graph [
962            rtl_st_opaccs Modu destr srcr1 srcr2 start_lbl
963          ] start_lbl dest_lbl def
964        ]
965      ]
966    ]
967  | op_mod ⇒ None ? (* signed mod not supported *)
968  | op_and ⇒
969    let destr ≝ extract_singleton ? destrs in
970    let srcr1 ≝ extract_singleton ? srcrs1 in
971    let srcr2 ≝ extract_singleton ? srcrs2 in
972    match destr with
973    [ None ⇒ None ?
974    | Some destr ⇒
975      match srcr1 with
976      [ None ⇒ None ?
977      | Some srcr1 ⇒
978        match srcr2 with
979        [ None ⇒ None ?
980        | Some srcr2 ⇒
981          adds_graph [
982            rtl_st_op2 And destr srcr1 srcr2 start_lbl
983          ] start_lbl dest_lbl def
984        ]
985      ]
986    ]
987  | op_or ⇒
988    let destr ≝ extract_singleton ? destrs in
989    let srcr1 ≝ extract_singleton ? srcrs1 in
990    let srcr2 ≝ extract_singleton ? srcrs2 in
991    match destr with
992    [ None ⇒ None ?
993    | Some destr ⇒
994      match srcr1 with
995      [ None ⇒ None ?
996      | Some srcr1 ⇒
997        match srcr2 with
998        [ None ⇒ None ?
999        | Some srcr2 ⇒
1000          adds_graph [
1001            rtl_st_op2 Or destr srcr1 srcr2 start_lbl
1002          ] start_lbl dest_lbl def
1003        ]
1004      ]
1005    ]
1006  | op_xor ⇒
1007    let destr ≝ extract_singleton ? destrs in
1008    let srcr1 ≝ extract_singleton ? srcrs1 in
1009    let srcr2 ≝ extract_singleton ? srcrs2 in
1010    match destr with
1011    [ None ⇒ None ?
1012    | Some destr ⇒
1013      match srcr1 with
1014      [ None ⇒ None ?
1015      | Some srcr1 ⇒
1016        match srcr2 with
1017        [ None ⇒ None ?
1018        | Some srcr2 ⇒
1019          adds_graph [
1020            rtl_st_op2 Xor destr srcr1 srcr2 start_lbl
1021          ] start_lbl dest_lbl def
1022        ]
1023      ]
1024    ]
1025  | op_shru ⇒ None ? (* shifts not supported *)
1026  | op_shr ⇒ None ?
1027  | op_shl ⇒ None ?
1028  | op_addf ⇒ None ? (* floats not supported *)
1029  | op_subf ⇒ None ?
1030  | op_mulf ⇒ None ?
1031  | op_divf ⇒ None ?
1032  | op_cmpf _ ⇒ None ?
1033  | op_addp ⇒
1034    let destr12 ≝ extract_pair ? destrs in
1035    match destr12 with
1036    [ None         ⇒ None ?
1037    | Some destr12 ⇒
1038      let 〈destr1, destr2〉 ≝ destr12 in
1039      let srcr12 ≝ extract_pair ? srcrs1 in
1040      match srcr12 with
1041      [ None ⇒
1042        let srcr2 ≝ extract_singleton ? srcrs1 in
1043        match srcr2 with
1044        [ None ⇒ None ?
1045        | Some srcr2 ⇒
1046          let srcr12 ≝ extract_pair ? srcrs2 in
1047          match srcr12 with
1048          [ None ⇒ None ?
1049          | Some srcr12 ⇒
1050            let 〈srcr11, srcr12〉 ≝ srcr12 in
1051            let 〈def, tmpr1〉 ≝ fresh_reg def in
1052            let 〈def, tmpr2〉 ≝ fresh_reg def in
1053              adds_graph [
1054                rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
1055                rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
1056                rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
1057                rtl_st_move destr1 tmpr1 start_lbl
1058              ] start_lbl dest_lbl def
1059          ]
1060        ]
1061      | Some srcr12 ⇒
1062        let 〈srcr11, srcr12〉 ≝ srcr12 in
1063        let srcr2 ≝ extract_singleton ? srcrs2 in
1064        match srcr2 with
1065        [ None       ⇒ None ?
1066        | Some srcr2 ⇒
1067          let 〈def, tmpr1〉 ≝ fresh_reg def in
1068          let 〈def, tmpr2〉 ≝ fresh_reg def in
1069            adds_graph [
1070              rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
1071              rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
1072              rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
1073              rtl_st_move destr1 tmpr1 start_lbl
1074            ] start_lbl dest_lbl def
1075        ]
1076      ]
1077    ]
1078  | op_subp ⇒
1079    let destr ≝ extract_singleton ? destrs in
1080    match destr with
1081    [ None ⇒
1082      let destr12 ≝ extract_pair ? destrs in
1083      match destr12 with
1084      [ None ⇒ None ?
1085      | Some destr12 ⇒
1086        let 〈destr1, destr2〉 ≝ destr12 in
1087        let srcr12 ≝ extract_pair ? srcrs1 in
1088        match srcr12 with
1089        [ None ⇒ None ?
1090        | Some srcr12 ⇒
1091          let 〈srcr11, srcr12〉 ≝ srcr12 in
1092          let srcr2 ≝ extract_singleton ? srcrs2 in
1093          match srcr2 with
1094          [ None ⇒ None ?
1095          | Some srcr2 ⇒
1096            adds_graph [
1097              rtl_st_clear_carry start_lbl;
1098              rtl_st_op2 Sub destr1 srcr11 srcr2 start_lbl;
1099              rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl;
1100              rtl_st_op2 Sub destr2 srcr12 destr2 start_lbl
1101            ] start_lbl dest_lbl def
1102          ]
1103        ]
1104      ]
1105    | Some destr ⇒
1106      match srcrs1 with
1107      [ nil ⇒ None ?
1108      | cons srcr1 tl ⇒
1109        match srcrs2 with
1110        [ nil ⇒ None ?
1111        | cons srcr2 tl' ⇒
1112          let 〈def, tmpr1〉 ≝ fresh_reg def in
1113          let 〈def, tmpr2〉 ≝ fresh_reg def in
1114            adds_graph [
1115              rtl_st_op1 Cmpl tmpr1 srcr2 start_lbl;
1116              rtl_st_int tmpr2 (bitvector_of_nat ? 1) start_lbl;
1117              rtl_st_op2 Add tmpr1 tmpr1 tmpr2 start_lbl;
1118              rtl_st_op2 Add destr srcr1 tmpr1 start_lbl
1119            ] start_lbl dest_lbl def
1120        ]
1121      ]
1122    ]
1123  | op_cmp cmp ⇒
1124    match cmp with
1125    [ Compare_Equal ⇒
1126      add_translates [
1127        translate_op2 op_sub destrs srcrs1 srcrs2;
1128        translate_op1 op_not_bool destrs destrs
1129      ] start_lbl dest_lbl def
1130    | Compare_NotEqual ⇒
1131      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
1132    | _ ⇒ None ?
1133    ]
1134  | op_cmpu cmp ⇒
1135    match cmp with
1136    [ Compare_Equal ⇒
1137      add_translates [
1138        translate_op2 op_sub destrs srcrs1 srcrs2;
1139        translate_op1 op_not_bool destrs destrs
1140      ] start_lbl dest_lbl def
1141    | Compare_NotEqual ⇒
1142      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
1143    | Compare
1144    | _ ⇒ None ?
1145    ]
1146  | _ ⇒ ?
1147  ].
1148
1149    | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
1150      let (def, tmpr) = fresh_reg def in
1151      adds_graph
1152        [RTL.St_clear_carry start_lbl ;
1153         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
1154         RTL.St_int (destr, 0, start_lbl) ;
1155         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
1156        start_lbl dest_lbl def
1157
1158    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
1159      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
1160        destrs srcrs2 srcrs1 start_lbl dest_lbl def
1161
1162    | AST.Op_cmpu AST.Cmp_le, _, _, _ ->
1163      add_translates
1164        [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ;
1165         translate_op1 AST.Op_notbool destrs destrs]
1166        start_lbl dest_lbl def
1167
1168    | AST.Op_cmpu AST.Cmp_ge, _, _, _ ->
1169      add_translates
1170        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
1171         translate_op1 AST.Op_notbool destrs destrs]
1172        start_lbl dest_lbl def
1173
1174    | AST.Op_cmp cmp, _, _, _ ->
1175      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
1176      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
1177      add_translates
1178        [translate_cst (AST.Cst_int 128) tmprs1 ;
1179         translate_cst (AST.Cst_int 128) tmprs2 ;
1180         translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ;
1181         translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ;
1182         translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2]
1183        start_lbl dest_lbl def
1184
1185    | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
1186      let (def, tmpr) = fresh_reg def in
1187      add_translates
1188        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ;
1189         translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ;
1190         translate_op2 AST.Op_or [destr] [destr] [tmpr] ;
1191         adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ;
1192         translate_op2 AST.Op_xor [destr] [destr] [tmpr]]
1193        start_lbl dest_lbl def
1194
1195    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
1196      let (def, tmpr1) = fresh_reg def in
1197      let (def, tmpr2) = fresh_reg def in
1198      add_translates
1199        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
1200         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
1201         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
1202         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
1203         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
1204        start_lbl dest_lbl def
1205
1206    | AST.Op_cmpp AST.Cmp_gt, _, _, _ ->
1207      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
1208        destrs srcrs2 srcrs1 start_lbl dest_lbl def
1209
1210    | AST.Op_cmpp AST.Cmp_le, _, _, _ ->
1211      add_translates
1212        [translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ;
1213         translate_op1 AST.Op_notbool destrs destrs]
1214        start_lbl dest_lbl def
1215
1216    | AST.Op_cmpp AST.Cmp_ge, _, _, _ ->
1217      add_translates
1218        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
1219         translate_op1 AST.Op_notbool destrs destrs]
1220        start_lbl dest_lbl def
1221
1222    | _ -> assert false (* wrong number of arguments *)
1223*)
1224
1225definition translate_condcst ≝
1226  λcst.
1227  λstart_lbl: label.
1228  λlbl_true: label.
1229  λlbl_false: label.
1230  λdef.
1231  match cst with
1232  [ cast_int i ⇒
1233    let 〈def, tmpr〉 ≝ fresh_reg def in
1234    adds_graph [
1235      rtl_st_int tmpr i start_lbl;
1236      rtl_st_cond_acc tmpr lbl_true lbl_false
1237    ] start_lbl start_lbl def
1238  | cast_addr_symbol x ⇒
1239    let 〈def, r1〉 ≝ fresh_reg def in
1240    let 〈def, r2〉 ≝ fresh_reg def in
1241    let lbl ≝ fresh_label def in
1242    match lbl with
1243    [ None ⇒ None ?
1244    | Some lbl ⇒
1245      let def ≝ add_graph start_lbl (rtl_st_addr r1 r2 x lbl) def in
1246        translate_condptr r1 r2 lbl lbl_true lbl_false def
1247    ]
1248  | cast_stack_offset off ⇒
1249    let 〈def, r1〉 ≝ fresh_reg def in
1250    let 〈def, r2〉 ≝ fresh_reg def in
1251    let tmp_lbl ≝ fresh_label def in
1252    match tmp_lbl with
1253    [ None ⇒ None ?
1254    | Some tmp_lbl ⇒
1255      let def ≝ translate_cst (cast_stack_offset off) [r1; r2] start_lbl tmp_lbl def in
1256      match def with
1257      [ None ⇒ None ?
1258      | Some def ⇒ translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def
1259      ]
1260    ]
1261  | cast_float f ⇒ None ? (* error_float *)
1262  ].
1263
1264definition size_of_op1_ret ≝
1265  λop.
1266  match op with
1267  [ op_cast8_unsigned ⇒ Some ? 1
1268  | op_cast8_signed ⇒ Some ? 1
1269  | op_cast16_unsigned ⇒ Some ? 1
1270  | op_cast16_signed ⇒ Some ? 1
1271  | op_neg_int ⇒ Some ? 1
1272  | op_not_int ⇒ Some ? 1
1273  | op_int_of_ptr ⇒ Some ? 1
1274  | op_ptr_of_int ⇒ Some ? 2
1275  | op_id ⇒ None ? (* invalid_argument *)
1276  | _ ⇒ None ? (* error_float *)
1277  ].
1278
1279definition translate_cond1 ≝
1280  λop1.
1281  λsrcrs: list register.
1282  λstart_lbl: label.
1283  λlbl_true: label.
1284  λlbl_false: label.
1285  λdef.
1286  match op1 with
1287  [ op_id ⇒
1288    let srcr ≝ extract_singleton ? srcrs in
1289    match srcr with
1290    [ None ⇒
1291      let srcr12 ≝ extract_pair ? srcrs in
1292      match srcr12 with
1293      [ None ⇒ None ?
1294      | Some srcr12 ⇒
1295        let 〈srcr1, srcr2〉 ≝ srcr12 in
1296          translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def
1297      ]
1298    | Some srcr ⇒
1299      adds_graph [
1300        rtl_st_cond_acc srcr lbl_true lbl_false
1301      ] start_lbl start_lbl def
1302    ]
1303  | _     ⇒
1304    let size ≝ size_of_op1_ret op1 in
1305    match size with
1306    [ None ⇒ None ?
1307    | Some size ⇒
1308      let 〈def, destrs〉 ≝ fresh_regs def size in
1309      let lbl ≝ fresh_label def in
1310      match lbl with
1311      [ None ⇒ None ?
1312      | Some lbl ⇒
1313        let def ≝ translate_op1 op1 destrs srcrs start_lbl lbl def in
1314        match def with
1315        [ None ⇒ None ?
1316        | Some def ⇒
1317          let destr ≝ extract_singleton ? destrs in
1318          match destr with
1319          [ None ⇒
1320            let destr12 ≝ extract_pair ? destrs in
1321            match destr12 with
1322            [ None ⇒ None ?
1323            | Some destr12 ⇒
1324              let 〈destr1, destr2〉 ≝ destr12 in
1325                translate_condptr destr1 destr2 start_lbl lbl_true lbl_false def
1326            ]
1327          | Some destr ⇒
1328            adds_graph [
1329              rtl_st_cond_acc destr lbl_true lbl_false
1330            ] start_lbl start_lbl def
1331          ]
1332        ]
1333      ]
1334    ]
1335  ].
1336
1337definition size_of_op2_ret ≝
1338  λn: nat.
1339  λop2.
1340  match op2 with
1341  [ op_add ⇒ Some ? 1
1342  | op_sub ⇒ Some ? 1
1343  | op_mul ⇒ Some ? 1
1344  | op_div ⇒ Some ? 1
1345  | op_divu ⇒ Some ? 1
1346  | op_mod ⇒ Some ? 1
1347  | op_modu ⇒ Some ? 1
1348  | op_and ⇒ Some ? 1
1349  | op_or ⇒ Some ? 1
1350  | op_xor ⇒ Some ? 1
1351  | op_shl ⇒ Some ? 1
1352  | op_shr ⇒ Some ? 1
1353  | op_shru ⇒ Some ? 1
1354  | op_cmp _ ⇒ Some ? 1
1355  | op_cmpu _ ⇒ Some ? 1
1356  | op_cmpp _ ⇒ Some ? 1
1357  | op_addp ⇒ Some ? 2
1358  | op_subp ⇒
1359    if eq_nat n 4 then
1360      Some ? 1
1361    else
1362      Some ? 2
1363  | _ ⇒ None ? (* error_float *)
1364  ].
1365
1366axiom translate_op2:
1367  op2 → list register → list register → list register → label → label → rtl_internal_function → option rtl_internal_function.
1368
1369definition translate_cond2 ≝
1370  λop2.
1371  λsrcrs1: list register.
1372  λsrcrs2: list register.
1373  λstart_lbl: label.
1374  λlbl_true: label.
1375  λlbl_false: label.
1376  λdef.
1377  match op2 with
1378  [ op_cmp cmp ⇒
1379    match cmp with
1380    [ Compare_Equal ⇒
1381      let srcr1 ≝ extract_singleton ? srcrs1 in
1382      match srcr1 with
1383      [ None ⇒ None ?
1384      | Some srcr1 ⇒
1385        let srcr2 ≝ extract_singleton ? srcrs2 in
1386        match srcr2 with
1387        [ None ⇒ None ?
1388        | Some srcr2 ⇒
1389          let 〈def, tmpr〉 ≝ fresh_reg def in
1390          adds_graph [
1391            rtl_st_clear_carry start_lbl;
1392            rtl_st_op2 Sub tmpr srcr1 srcr2 start_lbl;
1393            rtl_st_cond_acc tmpr lbl_false lbl_true
1394          ] start_lbl start_lbl def
1395        ]
1396      ]
1397    | _ ⇒
1398      let n ≝ length ? srcrs1 + length ? srcrs2 in
1399      match size_of_op2_ret n op2 with
1400      [ None ⇒ None ?
1401      | Some size ⇒
1402        let 〈def, destrs〉 ≝ fresh_regs def size in
1403        let lbl ≝ fresh_label def in
1404        match lbl with
1405        [ None ⇒ None ?
1406        | Some lbl ⇒
1407          match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
1408          [ None ⇒ None ?
1409          | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
1410          ]
1411        ]
1412      ]
1413    ]
1414  | _ ⇒
1415    let n ≝ length ? srcrs1 + length ? srcrs2 in
1416    match size_of_op2_ret n op2 with
1417    [ None ⇒ None ?
1418    | Some size ⇒
1419      let 〈def, destrs〉 ≝ fresh_regs def size in
1420      let lbl ≝ fresh_label def in
1421      match lbl with
1422      [ None ⇒ None ?
1423      | Some lbl ⇒
1424        match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
1425        [ None ⇒ None ?
1426        | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
1427        ]
1428      ]
1429    ]
1430  ].
1431
1432let rec addressing_pointer (mode: ?) (args: ?) (destr1: ?)
1433                           (destr2: ?) (start_lbl: label)
1434                           (dest_lbl: label) (def: rtl_internal_function) ≝
1435  let destrs ≝ [ destr1; destr2 ] in
1436  match mode with
1437  [ Aindexed off ⇒
1438    let srcr12 ≝ extract_singleton ? args in
1439    match srcr12 with
1440    [ None ⇒ None ?
1441    | Some srcr12 ⇒
1442      let srcr12 ≝ extract_pair ? srcr12 in
1443      match srcr12 with
1444      [ None ⇒ None ?
1445      | Some srcr12 ⇒
1446        let 〈srcr1, srcr2〉 ≝ srcr12 in
1447        let 〈def, tmpr〉 ≝ fresh_reg def in
1448        add_translates [
1449          adds_graph [
1450            rtl_st_int tmpr off start_lbl
1451          ];
1452          translate_op2 op_addp destrs [ srcr1 ; srcr2 ] [tmpr]
1453        ] start_lbl dest_lbl def
1454      ]
1455    ]
1456  | Aindexed2 ⇒
1457    let args_pair ≝ extract_pair ? args in
1458    match args_pair with
1459    [ None ⇒ None ?
1460    | Some args_pair ⇒
1461      let 〈lft, rgt〉 ≝ args_pair in
1462      let srcr1112 ≝ extract_pair ? lft in
1463      let srcr2 ≝ extract_singleton ? rgt in
1464      match srcr1112 with
1465      [ None ⇒
1466        let srcr2 ≝ extract_singleton ? rgt in
1467        let srcr1112 ≝ extract_pair ? lft in
1468        match srcr2 with
1469        [ None ⇒ None ?
1470        | Some srcr2 ⇒
1471          match srcr1112 with
1472          [ None ⇒ None ?
1473          | Some srcr1112 ⇒
1474            let 〈srcr11, srcr12〉 ≝ srcr1112 in
1475            translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
1476          ]
1477        ]
1478      | Some srcr1112 ⇒
1479        let 〈srcr11, srcr12〉 ≝ srcr1112 in
1480        match srcr2 with
1481        [ None ⇒ None ?
1482        | Some srcr2 ⇒
1483          translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
1484        ]
1485      ]
1486    ]
1487  | Aglobal x off ⇒
1488    let 〈def, tmpr〉 ≝ fresh_reg def in
1489    add_translates [
1490      adds_graph [
1491        rtl_st_int tmpr off start_lbl;
1492        rtl_st_addr destr1 destr2 x start_lbl
1493      ];
1494      translate_op2 op_addp destrs destrs [ tmpr ]
1495    ] start_lbl dest_lbl def
1496  | Abased x off ⇒
1497    let srcrs ≝ extract_singleton ? args in
1498    match srcrs with
1499    [ None ⇒ None ?
1500    | Some srcrs ⇒
1501      let 〈def, tmpr1〉 ≝ fresh_reg def in
1502      let 〈def, tmpr2〉 ≝ fresh_reg def in
1503      (* mode, args, destr1, destr2, start_lbl, dest_lbl, def *)
1504      (* addressing_pointer (Aglobal x off) [ ] tmpr1 tmpr2; *)
1505      let address_unfold ≝
1506        let 〈def, tmpr〉 ≝ fresh_reg def in
1507          add_translates [
1508            adds_graph [
1509              rtl_st_int tmpr off start_lbl;
1510              rtl_st_addr tmpr1 tmpr2 x start_lbl
1511           ];
1512            translate_op2 op_addp destrs destrs [ tmpr ]
1513         ]
1514      in
1515      add_translates [
1516        address_unfold;
1517        translate_op2 op_addp destrs [ tmpr1; tmpr2 ] srcrs
1518      ] start_lbl dest_lbl def
1519    ]
1520  | Ainstack off ⇒
1521    let 〈def, tmpr〉 ≝ fresh_reg def in
1522    add_translates [
1523      adds_graph [
1524        rtl_st_int tmpr off start_lbl;
1525        rtl_st_stack_addr destr1 destr2 start_lbl
1526      ];
1527      translate_op2 op_addp destrs destrs [ tmpr ]
1528    ] start_lbl dest_lbl def
1529  | _ ⇒ None ? (* wrong number of arguments *)
1530  ].
1531
1532definition translate_load ≝
1533  λq.
1534  λmode.
1535  λargs.
1536  λdestrs.
1537  λstart_lbl: label.
1538  λdest_lbl: label.
1539  λdef.
1540  match q with
1541  [ q_int b ⇒
1542    if eq_bv ? b (bitvector_of_nat ? 1) then
1543      match extract_singleton ? destrs with
1544      [ None ⇒ None ? (* error: size error in load *)
1545      | Some destr ⇒
1546        let 〈def, addr1〉 ≝ fresh_reg def in
1547        let 〈def, addr2〉 ≝ fresh_reg def in
1548          Some ? (add_translates [
1549            addressing_pointer mode args addr1 addr2;
1550            adds_graph [
1551              rtl_st_load destr addr1 addr2 start_lbl
1552            ]
1553          ] start_lbl dest_lbl def)
1554      ]
1555    else
1556      None ? (* error: size error in load *)
1557  | q_ptr ⇒
1558    match extract_pair ? destrs with
1559    [ None ⇒ None ? (* error: size error in load *)
1560    | Some destr12 ⇒
1561      let 〈destr1, destr2〉 ≝ destr12 in
1562      let 〈def, addr1〉 ≝ fresh_reg def in
1563      let 〈def, addr2〉 ≝ fresh_reg def in
1564      let addr ≝ [ addr1; addr2 ] in
1565      let 〈def, tmpr〉 ≝ fresh_reg def in
1566        Some ? (
1567          add_translates [
1568            addressing_pointer mode args addr1 addr2;
1569            adds_graph [
1570              rtl_st_load destr1 addr1 addr2 start_lbl;
1571              rtl_st_int tmpr (bitvector_of_nat ? 1) start_lbl
1572            ];
1573            translate_op2 op_addp addr addr [ tmpr ];
1574            adds_graph [
1575              rtl_st_load destr2 addr1 addr2 start_lbl
1576            ]
1577          ] start_lbl dest_lbl def
1578        )
1579    ]
1580  | _ ⇒ None ? (* error: size error in load *)
1581  ].
1582 
1583definition make_addr ≝
1584  λA: Type[0].
1585  λlst: list A.
1586  match lst with
1587  [ cons hd tl ⇒
1588    match tl with
1589    [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
1590    | _ ⇒ None ? (* do not use on these arguments *)
1591    ]
1592  | _ ⇒ None ? (* do not use on these arguments *)
1593  ].
1594 
1595definition translate_store_internal ≝
1596  λaddr.
1597  λtmp_addr.
1598  λtmpr.
1599  λstart_lbl.
1600  λdest_lbl.
1601  λtmp_addr1.
1602  λtmp_addr2.
1603  λtranslates_off.
1604  λsrcr.
1605    let 〈translates, off〉 ≝ translates_off in
1606    let translates ≝ translates @
1607      [ adds_graph [
1608          rtl_st_int tmpr off start_lbl
1609        ];
1610        translate_op2 op_addp tmp_addr addr [ tmpr ];
1611        adds_graph [
1612          rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
1613        ]
1614      ]
1615    in
1616    let 〈ignore, result〉 ≝ half_add ? off int_size in
1617      〈translates, result〉.
1618 
1619definition translate_store ≝
1620  λaddr.
1621  λsrcrs.
1622  λstart_lbl.
1623  λdest_lbl.
1624  λdef.
1625    let 〈def, tmp_addr〉 ≝ fresh_regs def (length ? addr) in
1626    match make_addr ? tmp_addr with
1627    [ None ⇒ None ?
1628    | Some tmp_addr12 ⇒
1629      let 〈tmp_addr1, tmp_addr2〉 ≝ tmp_addr12 in
1630      let 〈def, tmpr〉 ≝ fresh_reg def in
1631      let f ≝ translate_store_internal addr tmp_addr tmpr start_lbl dest_lbl tmp_addr1 tmp_addr2 in
1632      let 〈translates, ignore〉 ≝ foldl ? ? f 〈[], zero ?〉 srcrs in
1633        add_translates translates start_lbl dest_lbl def
1634    ].
1635
1636definition translate_stmt ≝
1637  λlenv.
1638  λlbl.
1639  λstmt.
1640  λdef.
1641  match stmt with
1642  [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
1643  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
1644  | St_cast destr cst lbl' ⇒
1645      translate_cst cst (find_local_env destr lenv) lbl lbl' def
1646  | _ ⇒ ?
1647  ].
1648
1649let translate_stmt lenv lbl stmt def = match stmt with
1650
1651  | RTLabs.St_skip lbl' ->
1652    add_graph lbl (RTL.St_skip lbl') def
1653
1654  | RTLabs.St_cost (cost_lbl, lbl') ->
1655    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
1656
1657  | RTLabs.St_cst (destr, cst, lbl') ->
1658    translate_cst cst (find_local_env destr lenv) lbl lbl' def
1659
1660  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
1661    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
1662      lbl lbl' def
1663
1664  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
1665    translate_op2 op2 (find_local_env destr lenv)
1666      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
1667
1668  | RTLabs.St_load (_, addr, destr, lbl') ->
1669    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
1670      lbl lbl' def
1671
1672  | RTLabs.St_store (_, addr, srcr, lbl') ->
1673    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
1674      lbl lbl' def
1675
1676  | RTLabs.St_call_id (f, args, None, _, lbl') ->
1677    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
1678
1679  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
1680    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
1681                                   find_local_env retr lenv, lbl')) def
1682
1683  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
1684    let (f1, f2) = find_and_addr f lenv in
1685    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
1686
1687  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
1688    let (f1, f2) = find_and_addr f lenv in
1689    add_graph lbl
1690      (RTL.St_call_ptr
1691         (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
1692
1693  | RTLabs.St_tailcall_id (f, args, _) ->
1694    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
1695
1696  | RTLabs.St_tailcall_ptr (f, args, _) ->
1697    let (f1, f2) = find_and_addr f lenv in
1698    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
1699
1700  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
1701    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
1702
1703  | RTLabs.St_jumptable _ ->
1704    error "Jump tables not supported yet."
1705
1706  | RTLabs.St_return None ->
1707    add_graph lbl (RTL.St_return []) def
1708
1709  | RTLabs.St_return (Some r) ->
1710    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
Note: See TracBrowser for help on using the repository browser.