source: src/RTLabs/RTLAbstoRTL.ma @ 793

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

Work from today on rtlabs -> rtl pass.

File size: 20.2 KB
Line 
1include "RTLabs/syntax.ma".
2include "RTL/RTL.ma".
3include "common/AssocList.ma".
4include "common/Graphs.ma".
5
6definition add_graph ≝
7  λl: label.
8  λstmt.
9  λp.
10  let rtl_if_luniverse' ≝ rtl_if_luniverse p in
11  let rtl_if_runiverse' ≝ rtl_if_runiverse p in
12  let rtl_if_sig' ≝ rtl_if_sig p in
13  let rtl_if_result' ≝ rtl_if_result p in
14  let rtl_if_params' ≝ rtl_if_params p in
15  let rtl_if_locals' ≝ rtl_if_locals p in
16  let rtl_if_stacksize' ≝ rtl_if_stacksize p in
17  let rtl_if_graph' ≝ add ? ? (rtl_if_graph p) l stmt in
18  let rtl_if_entry' ≝ rtl_if_entry p in
19  let rtl_if_exit' ≝ rtl_if_exit p in
20    mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig'
21                             rtl_if_params' rtl_if_params' rtl_if_locals'
22                             rtl_if_stacksize' rtl_if_graph' rtl_if_entry'
23                             rtl_if_exit'.
24     
25definition fresh_label ≝
26  λdef.
27    match fresh LabelTag (rtl_if_luniverse def) with
28    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
29    | Error ⇒ None ?
30    ].
31
32axiom fresh_reg: rtl_internal_function → rtl_internal_function × register.
33
34let rec fresh_regs (def: rtl_internal_function) (n: nat) on n ≝
35  match n with
36  [ O   ⇒ 〈def, [ ]〉
37  | S n ⇒
38    let 〈def, res〉 ≝ fresh_regs def n in
39    let 〈def, r〉 ≝ fresh_reg def in
40      〈def, r :: res〉
41  ].
42
43definition addr_regs ≝
44  λregs.
45  match regs with
46  [ cons hd tl ⇒
47    match tl with
48    [ cons hd' tl' ⇒ Some (register × register) 〈hd, hd'〉
49    | nil          ⇒ None (register × register)
50    ]
51  | nil ⇒ None (register × register)
52  ].
53
54inductive register_type: Type[0] ≝
55  | register_int: register → register_type
56  | register_ptr: register → register → register_type.
57
58definition local_env ≝ assoc_list register register_type.
59
60definition initialize_local_env_internal ≝
61  λeq.
62  λruniverse.
63  λptrs.
64  λlenv.
65  λr.
66    let fresh ≝ snd ? ? (fresh_reg runiverse) in
67    let rt ≝
68      match member ? eq r ptrs with
69      [ true  ⇒ register_ptr r fresh
70      | false ⇒ register_int r
71      ]
72    in
73    assoc_list_add ? ? 〈r, rt〉 lenv.
74
75definition initialize_local_env ≝
76  λruniverse.
77  λptrs.
78  λregisters.
79    foldl ? ? (initialize_local_env_internal (eq_identifier RegisterTag) runiverse ptrs) [ ] registers.
80
81definition filter_and_to_list_local_env_internal ≝
82  λlenv.
83  λl.
84  λr.
85  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
86  [ Some entry ⇒
87    match entry with
88    [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ])
89    | register_int r ⇒ (l @ [ r ])
90    ]
91  | None       ⇒ [ ] (* dpm: should this be none? *)
92  ].
93
94definition filter_and_to_list_local_env ≝
95  λlenv.
96  λregisters.
97    foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers.
98
99definition list_of_register_type ≝
100  λrt.
101  match rt with
102  [ register_ptr r1 r2 ⇒ [ r1; r2 ]
103  | register_int r ⇒ [ r ]
104  ].
105
106definition find_and_list ≝
107  λr.
108  λlenv.
109  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
110  [ None      ⇒ [ ] (* dpm: should this be none? *)
111  | Some lkup ⇒ list_of_register_type lkup
112  ].
113
114definition find_and_list_args ≝
115  λargs.
116  λlenv.
117    map ? ? (λr. find_and_list r lenv) args.
118
119definition find_and_addr ≝
120  λr.
121  λlenv.
122  match find_and_list r lenv with
123  [ cons hd tl ⇒
124    match tl with
125    [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
126    | nil          ⇒ None ?
127    ]
128  | nil ⇒ None ? (* dpm: was assert false *)
129  ].
130
131definition rtl_args ≝
132  λregs_list.
133  λlenv.
134    flatten ? (find_and_list_args regs_list lenv).
135
136definition change_label ≝
137  λlbl.
138  λstmt: rtl_statement.
139  match stmt with
140  [ rtl_st_skip _ ⇒ rtl_st_skip lbl
141  | rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl
142  | rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl
143  | rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl
144  | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
145  | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
146  | rtl_st_opaccs opaccs d s1 s2 _ ⇒ rtl_st_opaccs opaccs d s1 s2 lbl
147  | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
148  | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
149  | rtl_st_clear_carry _ ⇒ rtl_st_clear_carry lbl
150  | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl
151  | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl
152  | rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl
153  | rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl
154  | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a
155  | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
156  | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2
157  | rtl_st_return r ⇒ rtl_st_return r
158  | _ ⇒ ?
159  ].
160
161let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝
162  match stmt_list with
163  [ nil ⇒ Some ? def
164  | cons hd tl ⇒
165    match tl with
166    [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
167    | cons hd' tl' ⇒
168      let tmp_lbl ≝ fresh_label def in
169      match tmp_lbl with
170      [ None ⇒ None ?
171      | Some tmp_lbl ⇒
172        let stmt ≝ change_label tmp_lbl hd in
173        let def ≝ add_graph start_lbl stmt def in
174          adds_graph tl tmp_lbl dest_lbl def
175      ]
176    ]
177  ].
178 
179let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
180                       (def: ?) on translate_list ≝
181  match translate_list with
182  [ nil ⇒ Some ? def
183  | cons hd tl ⇒
184    match tl with
185    [ nil ⇒ Some ? (hd start_lbl dest_lbl def)
186    | cons hd' tl' ⇒
187      let tmp_lbl ≝ fresh_label def in
188      match tmp_lbl with
189      [ None ⇒ None ?
190      | Some tmp_lbl ⇒
191        let def ≝ hd start_lbl tmp_lbl def in
192          add_translates tl tmp_lbl dest_lbl def
193      ]
194    ]
195  ].
196 
197
198(* dpm: horrendous, use dependent types.
199  length destr = length srcrs *)
200let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label)
201                       (dest_lbl: label) (def: ?) ≝
202  match destrs with
203  [ nil ⇒
204    match srcrs with
205    [ nil        ⇒ Some ? def
206    | cons hd tl ⇒ None ?
207    ]
208  | cons hd tl ⇒
209    match srcrs with
210    [ nil        ⇒ None ?
211    | cons hd' tl' ⇒
212      match tl with
213      [ nil            ⇒
214        match tl' with
215        (* one element lists *)
216        [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def)
217        | cons hd'' tl'' ⇒ None ?
218        ]
219      | cons hd'' tl'' ⇒
220        match tl' with
221        [ nil ⇒ None ?
222        (* multielement lists *)
223        | cons hd''' tl''' ⇒
224          let tmp_lbl ≝ fresh_label def in
225          match tmp_lbl with
226          [ None ⇒ None ?
227          | Some tmp_lbl ⇒
228            let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in
229              translate_move tl tl' tmp_lbl dest_lbl def
230          ]
231        ]
232      ]
233    ]
234  ].
235
236definition translate_cst ≝
237  λcst.
238  λdestrs.
239  λstart_lbl.
240  λdest_lbl.
241  λdef.
242  match cst with
243  [ cast_int i ⇒
244    match destrs with
245    [ nil ⇒ None ?
246    | cons hd tl ⇒
247      match tl with
248      [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_int hd i dest_lbl) def)
249      | cons hd' tl' ⇒ None ?
250      ]
251    ]
252  | cast_addr_symbol id ⇒
253    match destrs with
254    [ nil ⇒ None ?
255    | cons hd tl ⇒
256      match tl with
257      [ nil ⇒ None ?
258      | cons hd' tl' ⇒
259        Some ? (add_graph start_lbl (rtl_st_addr hd hd' id dest_lbl) def)
260      ]
261    ]
262  | cast_stack_offset off ⇒
263    match destrs with
264    [ nil ⇒ None ?
265    | cons hd tl ⇒
266      match tl with
267      [ nil ⇒ None ?
268      | cons hd' tl' ⇒
269        let 〈def, tmpr〉 ≝ fresh_reg def in
270        adds_graph [
271          rtl_st_stack_addr hd hd' start_lbl;
272          rtl_st_int tmpr off start_lbl;
273          rtl_st_op2 Add hd hd tmpr start_lbl;
274          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
275          rtl_st_op2 Addc hd' hd' tmpr start_lbl
276        ] start_lbl dest_lbl def
277      ]
278    ]
279  | cast_float f ⇒ None ?
280  ].
281
282definition extract_singleton ≝
283  λA: Type[0].
284  λl: list A.
285  match l with
286  [ nil ⇒ None ?
287  | cons hd tl ⇒
288    match tl with
289    [ nil ⇒ Some ? hd
290    | cons hd tl ⇒ None ?
291    ]
292  ].
293
294definition extract_pair ≝
295  λA: Type[0].
296  λl: list A.
297  match l with
298  [ nil ⇒ None ?
299  | cons hd tl ⇒
300    match tl with
301    [ nil ⇒ None ?
302    | cons hd' tl' ⇒
303      match tl' with
304      [ nil ⇒ Some ? 〈hd, hd'〉
305      | cons hd'' tl'' ⇒ None ?
306      ]
307    ]
308  ].
309
310definition translate_op1 ≝
311  λop1.
312  λdestrs.
313  λsrcrs.
314  λstart_lbl.
315  λdest_lbl.
316  λdef.
317  match op1 with
318  [ op_cast8_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
319  | op_cast8_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
320  | op_cast16_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
321  | op_cast16_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
322  | op_neg_int ⇒
323    let dstr ≝ extract_singleton ? destrs in
324    let srcr ≝ extract_singleton ? srcrs in
325    match dstr with
326    [ None ⇒ None ?
327    | Some dstr ⇒
328      match srcr with
329      [ None ⇒ None ?
330      | Some srcr ⇒
331        adds_graph [
332          rtl_st_op1 Cmpl dstr srcr start_lbl;
333          rtl_st_op1 Inc dstr dstr start_lbl
334        ] start_lbl dest_lbl def
335      ]
336    ]
337  | op_not_int ⇒
338    let dstr ≝ extract_singleton ? destrs in
339    let srcr ≝ extract_singleton ? srcrs in
340    match dstr with
341    [ None ⇒ None ?
342    | Some dstr ⇒
343      match srcr with
344      [ None ⇒ None ?
345      | Some srcr ⇒
346        adds_graph [
347          rtl_st_op1 Cmpl dstr srcr start_lbl
348        ] start_lbl dest_lbl def
349      ]
350    ]
351  | op_id ⇒ translate_move destrs srcrs start_lbl dest_lbl def
352  | op_ptr_of_int ⇒
353    let destr12 ≝ extract_pair ? destrs in
354    let srcr ≝ extract_singleton ? srcrs in
355    match destr12 with
356    [ None ⇒ None ?
357    | Some destr12 ⇒
358      let 〈destr1, destr2〉 ≝ destr12 in
359      match srcr with
360      [ None ⇒ None ?
361      | Some srcr ⇒
362        adds_graph [
363          rtl_st_move destr1 srcr dest_lbl;
364          rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl
365        ] start_lbl dest_lbl def
366      ]
367    ]
368  | op_int_of_ptr ⇒
369    let destr ≝ extract_singleton ? destrs in
370    match destr with
371    [ None ⇒ None ?
372    | Some destr ⇒
373      match srcrs with
374      [ nil ⇒ None ?
375      | cons srcr tl ⇒
376        Some ? (add_graph start_lbl (rtl_st_move destr srcr dest_lbl) def)
377      ]
378    ]
379  | op_not_bool ⇒
380    let destr ≝ extract_singleton ? destrs in
381    let srcrs ≝ extract_singleton ? srcrs in
382    match destr with
383    [ None ⇒ None ?
384    | Some destr ⇒
385      match srcrs with
386      [ None ⇒ None ?
387      | Some srcr ⇒
388        let 〈def, tmpr〉 ≝ fresh_reg def in
389        adds_graph [
390          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
391          rtl_st_clear_carry start_lbl;
392          rtl_st_op2 Sub destr tmpr srcr start_lbl;
393          rtl_st_int destr (bitvector_of_nat ? 0) dest_lbl;
394          rtl_st_op2 Addc destr destr destr start_lbl;
395          rtl_st_int tmpr (bitvector_of_nat ? 1) dest_lbl;
396          rtl_st_op2 Xor destr destr tmpr start_lbl
397        ] start_lbl dest_lbl def
398      ]
399    ]
400  | _ ⇒ None ? (* error float *)
401  ].
402
403definition translate_condptr ≝
404  λr1.
405  λr2.
406  λstart_lbl: label.
407  λlbl_true: label.
408  λlbl_false: label.
409  λdef.
410  let 〈def, tmpr〉 ≝ fresh_reg def in
411    adds_graph [
412      rtl_st_op2 Or tmpr r1 r2 start_lbl;
413      rtl_st_cond_acc tmpr lbl_true lbl_false
414    ] start_lbl start_lbl def.
415
416let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?)
417                      (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝
418  match op2 with
419  [ op_add ⇒
420    let destr ≝ extract_singleton ? destrs in
421    let srcr1 ≝ extract_singleton ? srcrs1 in
422    let srcr2 ≝ extract_singleton ? srcrs2 in
423    match destr with
424    [ None ⇒ None ?
425    | Some destr ⇒
426      match srcr1 with
427      [ None ⇒ None ?
428      | Some srcr1 ⇒
429        match srcr2 with
430        [ None ⇒ None ?
431        | Some srcr2 ⇒
432          adds_graph [
433            rtl_st_op2 Add destr srcr1 srcr2 start_lbl
434          ] start_lbl dest_lbl def
435        ]
436      ]
437    ]
438  | op_sub ⇒
439    let destr ≝ extract_singleton ? destrs in
440    let srcr1 ≝ extract_singleton ? srcrs1 in
441    let srcr2 ≝ extract_singleton ? srcrs2 in
442    match destr with
443    [ None ⇒ None ?
444    | Some destr ⇒
445      match srcr1 with
446      [ None ⇒ None ?
447      | Some srcr1 ⇒
448        match srcr2 with
449        [ None ⇒ None ?
450        | Some srcr2 ⇒
451          adds_graph [
452            rtl_st_clear_carry start_lbl;
453            rtl_st_op2 Sub destr srcr1 srcr2 start_lbl
454          ] start_lbl dest_lbl def
455        ]
456      ]
457    ]
458  | op_mul ⇒
459    let destr ≝ extract_singleton ? destrs in
460    let srcr1 ≝ extract_singleton ? srcrs1 in
461    let srcr2 ≝ extract_singleton ? srcrs2 in
462    match destr with
463    [ None ⇒ None ?
464    | Some destr ⇒
465      match srcr1 with
466      [ None ⇒ None ?
467      | Some srcr1 ⇒
468        match srcr2 with
469        [ None ⇒ None ?
470        | Some srcr2 ⇒
471          adds_graph [
472            rtl_st_opaccs Mul destr srcr1 srcr2 start_lbl
473          ] start_lbl dest_lbl def
474        ]
475      ]
476    ]
477  | op_div ⇒ None ? (* signed div not supported *)
478  | op_divu ⇒
479    let destr ≝ extract_singleton ? destrs in
480    let srcr1 ≝ extract_singleton ? srcrs1 in
481    let srcr2 ≝ extract_singleton ? srcrs2 in
482    match destr with
483    [ None ⇒ None ?
484    | Some destr ⇒
485      match srcr1 with
486      [ None ⇒ None ?
487      | Some srcr1 ⇒
488        match srcr2 with
489        [ None ⇒ None ?
490        | Some srcr2 ⇒
491          adds_graph [
492            rtl_st_opaccs Divu destr srcr1 srcr2 start_lbl
493          ] start_lbl dest_lbl def
494        ]
495      ]
496    ]
497  | op_modu ⇒
498    let destr ≝ extract_singleton ? destrs in
499    let srcr1 ≝ extract_singleton ? srcrs1 in
500    let srcr2 ≝ extract_singleton ? srcrs2 in
501    match destr with
502    [ None ⇒ None ?
503    | Some destr ⇒
504      match srcr1 with
505      [ None ⇒ None ?
506      | Some srcr1 ⇒
507        match srcr2 with
508        [ None ⇒ None ?
509        | Some srcr2 ⇒
510          adds_graph [
511            rtl_st_opaccs Modu destr srcr1 srcr2 start_lbl
512          ] start_lbl dest_lbl def
513        ]
514      ]
515    ]
516  | op_mod ⇒ None ? (* signed mod not supported *)
517  | op_and ⇒
518    let destr ≝ extract_singleton ? destrs in
519    let srcr1 ≝ extract_singleton ? srcrs1 in
520    let srcr2 ≝ extract_singleton ? srcrs2 in
521    match destr with
522    [ None ⇒ None ?
523    | Some destr ⇒
524      match srcr1 with
525      [ None ⇒ None ?
526      | Some srcr1 ⇒
527        match srcr2 with
528        [ None ⇒ None ?
529        | Some srcr2 ⇒
530          adds_graph [
531            rtl_st_op2 And destr srcr1 srcr2 start_lbl
532          ] start_lbl dest_lbl def
533        ]
534      ]
535    ]
536  | op_or ⇒
537    let destr ≝ extract_singleton ? destrs in
538    let srcr1 ≝ extract_singleton ? srcrs1 in
539    let srcr2 ≝ extract_singleton ? srcrs2 in
540    match destr with
541    [ None ⇒ None ?
542    | Some destr ⇒
543      match srcr1 with
544      [ None ⇒ None ?
545      | Some srcr1 ⇒
546        match srcr2 with
547        [ None ⇒ None ?
548        | Some srcr2 ⇒
549          adds_graph [
550            rtl_st_op2 Or destr srcr1 srcr2 start_lbl
551          ] start_lbl dest_lbl def
552        ]
553      ]
554    ]
555  | op_xor ⇒
556    let destr ≝ extract_singleton ? destrs in
557    let srcr1 ≝ extract_singleton ? srcrs1 in
558    let srcr2 ≝ extract_singleton ? srcrs2 in
559    match destr with
560    [ None ⇒ None ?
561    | Some destr ⇒
562      match srcr1 with
563      [ None ⇒ None ?
564      | Some srcr1 ⇒
565        match srcr2 with
566        [ None ⇒ None ?
567        | Some srcr2 ⇒
568          adds_graph [
569            rtl_st_op2 Xor destr srcr1 srcr2 start_lbl
570          ] start_lbl dest_lbl def
571        ]
572      ]
573    ]
574  | op_shru ⇒ None ? (* shifts not supported *)
575  | op_shr ⇒ None ?
576  | op_shl ⇒ None ?
577  | op_addf ⇒ None ? (* floats not supported *)
578  | op_subf ⇒ None ?
579  | op_mulf ⇒ None ?
580  | op_divf ⇒ None ?
581  | op_cmpf _ ⇒ None ?
582  | op_addp ⇒ ?
583  | _ ⇒ ?
584  ].
585
586    | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2]
587    | AST.Op_addp, [destr1 ; destr2], [srcr2], [srcr11 ; srcr12] ->
588      let (def, tmpr1) = fresh_reg def in
589      let (def, tmpr2) = fresh_reg def in
590      adds_graph
591        [RTL.St_op2 (I8051.Add, tmpr1, srcr11, srcr2, start_lbl) ;
592         RTL.St_int (tmpr2, 0, start_lbl) ;
593         RTL.St_op2 (I8051.Addc, destr2, tmpr2, srcr12, start_lbl) ;
594         RTL.St_move (destr1, tmpr1, start_lbl)]
595        start_lbl dest_lbl def
596
597    | AST.Op_subp, [destr], [srcr1 ; _], [srcr2 ; _] ->
598      let (def, tmpr1) = fresh_reg def in
599      let (def, tmpr2) = fresh_reg def in
600      adds_graph
601        [RTL.St_op1 (I8051.Cmpl, tmpr1, srcr2, start_lbl) ;
602         RTL.St_int (tmpr2, 1, start_lbl) ;
603         RTL.St_op2 (I8051.Add, tmpr1, tmpr1, tmpr2, start_lbl) ;
604         RTL.St_op2 (I8051.Add, destr, srcr1, tmpr1, start_lbl)]
605        start_lbl dest_lbl def
606
607    | AST.Op_subp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] ->
608      adds_graph
609        [RTL.St_clear_carry start_lbl ;
610         RTL.St_op2 (I8051.Sub, destr1, srcr11, srcr2, start_lbl) ;
611         RTL.St_int (destr2, 0, start_lbl) ;
612         RTL.St_op2 (I8051.Sub, destr2, srcr12, destr2, start_lbl)]
613        start_lbl dest_lbl def
614
615    | AST.Op_cmp AST.Cmp_eq, _, _, _
616    | AST.Op_cmpu AST.Cmp_eq, _, _, _ ->
617      add_translates
618        [translate_op2 AST.Op_sub destrs srcrs1 srcrs2 ;
619         translate_op1 AST.Op_notbool destrs destrs]
620        start_lbl dest_lbl def
621
622    | AST.Op_cmp AST.Cmp_ne, _, _, _
623    | AST.Op_cmpu AST.Cmp_ne, _, _, _ ->
624      translate_op2 AST.Op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
625
626    | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
627      let (def, tmpr) = fresh_reg def in
628      adds_graph
629        [RTL.St_clear_carry start_lbl ;
630         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
631         RTL.St_int (destr, 0, start_lbl) ;
632         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
633        start_lbl dest_lbl def
634
635    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
636      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
637        destrs srcrs2 srcrs1 start_lbl dest_lbl def
638
639    | AST.Op_cmpu AST.Cmp_le, _, _, _ ->
640      add_translates
641        [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ;
642         translate_op1 AST.Op_notbool destrs destrs]
643        start_lbl dest_lbl def
644
645    | AST.Op_cmpu AST.Cmp_ge, _, _, _ ->
646      add_translates
647        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
648         translate_op1 AST.Op_notbool destrs destrs]
649        start_lbl dest_lbl def
650
651    | AST.Op_cmp cmp, _, _, _ ->
652      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
653      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
654      add_translates
655        [translate_cst (AST.Cst_int 128) tmprs1 ;
656         translate_cst (AST.Cst_int 128) tmprs2 ;
657         translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ;
658         translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ;
659         translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2]
660        start_lbl dest_lbl def
661
662    | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
663      let (def, tmpr) = fresh_reg def in
664      add_translates
665        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ;
666         translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ;
667         translate_op2 AST.Op_or [destr] [destr] [tmpr] ;
668         adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ;
669         translate_op2 AST.Op_xor [destr] [destr] [tmpr]]
670        start_lbl dest_lbl def
671
672    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
673      let (def, tmpr1) = fresh_reg def in
674      let (def, tmpr2) = fresh_reg def in
675      add_translates
676        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
677         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
678         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
679         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
680         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
681        start_lbl dest_lbl def
682
683    | AST.Op_cmpp AST.Cmp_gt, _, _, _ ->
684      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
685        destrs srcrs2 srcrs1 start_lbl dest_lbl def
686
687    | AST.Op_cmpp AST.Cmp_le, _, _, _ ->
688      add_translates
689        [translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ;
690         translate_op1 AST.Op_notbool destrs destrs]
691        start_lbl dest_lbl def
692
693    | AST.Op_cmpp AST.Cmp_ge, _, _, _ ->
694      add_translates
695        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
696         translate_op1 AST.Op_notbool destrs destrs]
697        start_lbl dest_lbl def
698
699    | _ -> assert false (* wrong number of arguments *)
Note: See TracBrowser for help on using the repository browser.