source: src/RTLabs/RTLAbstoRTL.ma @ 797

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

Changes from this morning.

File size: 22.6 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 
179(* dpm: had to lift this into option *)
180let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
181                       (def: ?) on translate_list ≝
182  match translate_list with
183  [ nil ⇒ Some ? def
184  | cons hd tl ⇒
185    match tl with
186    [ nil ⇒ hd start_lbl dest_lbl def
187    | cons hd' tl' ⇒
188      let tmp_lbl ≝ fresh_label def in
189      match tmp_lbl with
190      [ None ⇒ None ?
191      | Some tmp_lbl ⇒
192        match hd start_lbl tmp_lbl def with
193        [ None ⇒ None ?
194        | Some def ⇒ add_translates tl tmp_lbl dest_lbl def
195        ]
196      ]
197    ]
198  ].
199 
200
201(* dpm: horrendous, use dependent types.
202  length destr = length srcrs *)
203let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label)
204                       (dest_lbl: label) (def: ?) ≝
205  match destrs with
206  [ nil ⇒
207    match srcrs with
208    [ nil        ⇒ Some ? def
209    | cons hd tl ⇒ None ?
210    ]
211  | cons hd tl ⇒
212    match srcrs with
213    [ nil        ⇒ None ?
214    | cons hd' tl' ⇒
215      match tl with
216      [ nil            ⇒
217        match tl' with
218        (* one element lists *)
219        [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def)
220        | cons hd'' tl'' ⇒ None ?
221        ]
222      | cons hd'' tl'' ⇒
223        match tl' with
224        [ nil ⇒ None ?
225        (* multielement lists *)
226        | cons hd''' tl''' ⇒
227          let tmp_lbl ≝ fresh_label def in
228          match tmp_lbl with
229          [ None ⇒ None ?
230          | Some tmp_lbl ⇒
231            let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in
232              translate_move tl tl' tmp_lbl dest_lbl def
233          ]
234        ]
235      ]
236    ]
237  ].
238
239definition translate_cst ≝
240  λcst.
241  λdestrs.
242  λstart_lbl.
243  λdest_lbl.
244  λdef.
245  match cst with
246  [ cast_int i ⇒
247    match destrs with
248    [ nil ⇒ None ?
249    | cons hd tl ⇒
250      match tl with
251      [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_int hd i dest_lbl) def)
252      | cons hd' tl' ⇒ None ?
253      ]
254    ]
255  | cast_addr_symbol id ⇒
256    match destrs with
257    [ nil ⇒ None ?
258    | cons hd tl ⇒
259      match tl with
260      [ nil ⇒ None ?
261      | cons hd' tl' ⇒
262        Some ? (add_graph start_lbl (rtl_st_addr hd hd' id dest_lbl) def)
263      ]
264    ]
265  | cast_stack_offset off ⇒
266    match destrs with
267    [ nil ⇒ None ?
268    | cons hd tl ⇒
269      match tl with
270      [ nil ⇒ None ?
271      | cons hd' tl' ⇒
272        let 〈def, tmpr〉 ≝ fresh_reg def in
273        adds_graph [
274          rtl_st_stack_addr hd hd' start_lbl;
275          rtl_st_int tmpr off start_lbl;
276          rtl_st_op2 Add hd hd tmpr start_lbl;
277          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
278          rtl_st_op2 Addc hd' hd' tmpr start_lbl
279        ] start_lbl dest_lbl def
280      ]
281    ]
282  | cast_float f ⇒ None ?
283  ].
284
285definition extract_singleton ≝
286  λA: Type[0].
287  λl: list A.
288  match l with
289  [ nil ⇒ None ?
290  | cons hd tl ⇒
291    match tl with
292    [ nil ⇒ Some ? hd
293    | cons hd tl ⇒ None ?
294    ]
295  ].
296
297definition extract_pair ≝
298  λA: Type[0].
299  λl: list A.
300  match l with
301  [ nil ⇒ None ?
302  | cons hd tl ⇒
303    match tl with
304    [ nil ⇒ None ?
305    | cons hd' tl' ⇒
306      match tl' with
307      [ nil ⇒ Some ? 〈hd, hd'〉
308      | cons hd'' tl'' ⇒ None ?
309      ]
310    ]
311  ].
312
313definition translate_op1 ≝
314  λop1.
315  λdestrs.
316  λsrcrs.
317  λstart_lbl.
318  λdest_lbl.
319  λdef.
320  match op1 with
321  [ op_cast8_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
322  | op_cast8_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
323  | op_cast16_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
324  | op_cast16_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
325  | op_neg_int ⇒
326    let dstr ≝ extract_singleton ? destrs in
327    let srcr ≝ extract_singleton ? srcrs in
328    match dstr with
329    [ None ⇒ None ?
330    | Some dstr ⇒
331      match srcr with
332      [ None ⇒ None ?
333      | Some srcr ⇒
334        adds_graph [
335          rtl_st_op1 Cmpl dstr srcr start_lbl;
336          rtl_st_op1 Inc dstr dstr start_lbl
337        ] start_lbl dest_lbl def
338      ]
339    ]
340  | op_not_int ⇒
341    let dstr ≝ extract_singleton ? destrs in
342    let srcr ≝ extract_singleton ? srcrs in
343    match dstr with
344    [ None ⇒ None ?
345    | Some dstr ⇒
346      match srcr with
347      [ None ⇒ None ?
348      | Some srcr ⇒
349        adds_graph [
350          rtl_st_op1 Cmpl dstr srcr start_lbl
351        ] start_lbl dest_lbl def
352      ]
353    ]
354  | op_id ⇒ translate_move destrs srcrs start_lbl dest_lbl def
355  | op_ptr_of_int ⇒
356    let destr12 ≝ extract_pair ? destrs in
357    let srcr ≝ extract_singleton ? srcrs in
358    match destr12 with
359    [ None ⇒ None ?
360    | Some destr12 ⇒
361      let 〈destr1, destr2〉 ≝ destr12 in
362      match srcr with
363      [ None ⇒ None ?
364      | Some srcr ⇒
365        adds_graph [
366          rtl_st_move destr1 srcr dest_lbl;
367          rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl
368        ] start_lbl dest_lbl def
369      ]
370    ]
371  | op_int_of_ptr ⇒
372    let destr ≝ extract_singleton ? destrs in
373    match destr with
374    [ None ⇒ None ?
375    | Some destr ⇒
376      match srcrs with
377      [ nil ⇒ None ?
378      | cons srcr tl ⇒
379        Some ? (add_graph start_lbl (rtl_st_move destr srcr dest_lbl) def)
380      ]
381    ]
382  | op_not_bool ⇒
383    let destr ≝ extract_singleton ? destrs in
384    let srcrs ≝ extract_singleton ? srcrs in
385    match destr with
386    [ None ⇒ None ?
387    | Some destr ⇒
388      match srcrs with
389      [ None ⇒ None ?
390      | Some srcr ⇒
391        let 〈def, tmpr〉 ≝ fresh_reg def in
392        adds_graph [
393          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
394          rtl_st_clear_carry start_lbl;
395          rtl_st_op2 Sub destr tmpr srcr start_lbl;
396          rtl_st_int destr (bitvector_of_nat ? 0) dest_lbl;
397          rtl_st_op2 Addc destr destr destr start_lbl;
398          rtl_st_int tmpr (bitvector_of_nat ? 1) dest_lbl;
399          rtl_st_op2 Xor destr destr tmpr start_lbl
400        ] start_lbl dest_lbl def
401      ]
402    ]
403  | _ ⇒ None ? (* error float *)
404  ].
405
406definition translate_condptr ≝
407  λr1.
408  λr2.
409  λstart_lbl: label.
410  λlbl_true: label.
411  λlbl_false: label.
412  λdef.
413  let 〈def, tmpr〉 ≝ fresh_reg def in
414    adds_graph [
415      rtl_st_op2 Or tmpr r1 r2 start_lbl;
416      rtl_st_cond_acc tmpr lbl_true lbl_false
417    ] start_lbl start_lbl def.
418
419let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?)
420                      (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝
421  match op2 with
422  [ op_add ⇒
423    let destr ≝ extract_singleton ? destrs in
424    let srcr1 ≝ extract_singleton ? srcrs1 in
425    let srcr2 ≝ extract_singleton ? srcrs2 in
426    match destr with
427    [ None ⇒ None ?
428    | Some destr ⇒
429      match srcr1 with
430      [ None ⇒ None ?
431      | Some srcr1 ⇒
432        match srcr2 with
433        [ None ⇒ None ?
434        | Some srcr2 ⇒
435          adds_graph [
436            rtl_st_op2 Add destr srcr1 srcr2 start_lbl
437          ] start_lbl dest_lbl def
438        ]
439      ]
440    ]
441  | op_sub ⇒
442    let destr ≝ extract_singleton ? destrs in
443    let srcr1 ≝ extract_singleton ? srcrs1 in
444    let srcr2 ≝ extract_singleton ? srcrs2 in
445    match destr with
446    [ None ⇒ None ?
447    | Some destr ⇒
448      match srcr1 with
449      [ None ⇒ None ?
450      | Some srcr1 ⇒
451        match srcr2 with
452        [ None ⇒ None ?
453        | Some srcr2 ⇒
454          adds_graph [
455            rtl_st_clear_carry start_lbl;
456            rtl_st_op2 Sub destr srcr1 srcr2 start_lbl
457          ] start_lbl dest_lbl def
458        ]
459      ]
460    ]
461  | op_mul ⇒
462    let destr ≝ extract_singleton ? destrs in
463    let srcr1 ≝ extract_singleton ? srcrs1 in
464    let srcr2 ≝ extract_singleton ? srcrs2 in
465    match destr with
466    [ None ⇒ None ?
467    | Some destr ⇒
468      match srcr1 with
469      [ None ⇒ None ?
470      | Some srcr1 ⇒
471        match srcr2 with
472        [ None ⇒ None ?
473        | Some srcr2 ⇒
474          adds_graph [
475            rtl_st_opaccs Mul destr srcr1 srcr2 start_lbl
476          ] start_lbl dest_lbl def
477        ]
478      ]
479    ]
480  | op_div ⇒ None ? (* signed div not supported *)
481  | op_divu ⇒
482    let destr ≝ extract_singleton ? destrs in
483    let srcr1 ≝ extract_singleton ? srcrs1 in
484    let srcr2 ≝ extract_singleton ? srcrs2 in
485    match destr with
486    [ None ⇒ None ?
487    | Some destr ⇒
488      match srcr1 with
489      [ None ⇒ None ?
490      | Some srcr1 ⇒
491        match srcr2 with
492        [ None ⇒ None ?
493        | Some srcr2 ⇒
494          adds_graph [
495            rtl_st_opaccs Divu destr srcr1 srcr2 start_lbl
496          ] start_lbl dest_lbl def
497        ]
498      ]
499    ]
500  | op_modu ⇒
501    let destr ≝ extract_singleton ? destrs in
502    let srcr1 ≝ extract_singleton ? srcrs1 in
503    let srcr2 ≝ extract_singleton ? srcrs2 in
504    match destr with
505    [ None ⇒ None ?
506    | Some destr ⇒
507      match srcr1 with
508      [ None ⇒ None ?
509      | Some srcr1 ⇒
510        match srcr2 with
511        [ None ⇒ None ?
512        | Some srcr2 ⇒
513          adds_graph [
514            rtl_st_opaccs Modu destr srcr1 srcr2 start_lbl
515          ] start_lbl dest_lbl def
516        ]
517      ]
518    ]
519  | op_mod ⇒ None ? (* signed mod not supported *)
520  | op_and ⇒
521    let destr ≝ extract_singleton ? destrs in
522    let srcr1 ≝ extract_singleton ? srcrs1 in
523    let srcr2 ≝ extract_singleton ? srcrs2 in
524    match destr with
525    [ None ⇒ None ?
526    | Some destr ⇒
527      match srcr1 with
528      [ None ⇒ None ?
529      | Some srcr1 ⇒
530        match srcr2 with
531        [ None ⇒ None ?
532        | Some srcr2 ⇒
533          adds_graph [
534            rtl_st_op2 And destr srcr1 srcr2 start_lbl
535          ] start_lbl dest_lbl def
536        ]
537      ]
538    ]
539  | op_or ⇒
540    let destr ≝ extract_singleton ? destrs in
541    let srcr1 ≝ extract_singleton ? srcrs1 in
542    let srcr2 ≝ extract_singleton ? srcrs2 in
543    match destr with
544    [ None ⇒ None ?
545    | Some destr ⇒
546      match srcr1 with
547      [ None ⇒ None ?
548      | Some srcr1 ⇒
549        match srcr2 with
550        [ None ⇒ None ?
551        | Some srcr2 ⇒
552          adds_graph [
553            rtl_st_op2 Or destr srcr1 srcr2 start_lbl
554          ] start_lbl dest_lbl def
555        ]
556      ]
557    ]
558  | op_xor ⇒
559    let destr ≝ extract_singleton ? destrs in
560    let srcr1 ≝ extract_singleton ? srcrs1 in
561    let srcr2 ≝ extract_singleton ? srcrs2 in
562    match destr with
563    [ None ⇒ None ?
564    | Some destr ⇒
565      match srcr1 with
566      [ None ⇒ None ?
567      | Some srcr1 ⇒
568        match srcr2 with
569        [ None ⇒ None ?
570        | Some srcr2 ⇒
571          adds_graph [
572            rtl_st_op2 Xor destr srcr1 srcr2 start_lbl
573          ] start_lbl dest_lbl def
574        ]
575      ]
576    ]
577  | op_shru ⇒ None ? (* shifts not supported *)
578  | op_shr ⇒ None ?
579  | op_shl ⇒ None ?
580  | op_addf ⇒ None ? (* floats not supported *)
581  | op_subf ⇒ None ?
582  | op_mulf ⇒ None ?
583  | op_divf ⇒ None ?
584  | op_cmpf _ ⇒ None ?
585  | op_addp ⇒
586    let destr12 ≝ extract_pair ? destrs in
587    match destr12 with
588    [ None         ⇒ None ?
589    | Some destr12 ⇒
590      let 〈destr1, destr2〉 ≝ destr12 in
591      let srcr12 ≝ extract_pair ? srcrs1 in
592      match srcr12 with
593      [ None ⇒
594        let srcr2 ≝ extract_singleton ? srcrs1 in
595        match srcr2 with
596        [ None ⇒ None ?
597        | Some srcr2 ⇒
598          let srcr12 ≝ extract_pair ? srcrs2 in
599          match srcr12 with
600          [ None ⇒ None ?
601          | Some srcr12 ⇒
602            let 〈srcr11, srcr12〉 ≝ srcr12 in
603            let 〈def, tmpr1〉 ≝ fresh_reg def in
604            let 〈def, tmpr2〉 ≝ fresh_reg def in
605              adds_graph [
606                rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
607                rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
608                rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
609                rtl_st_move destr1 tmpr1 start_lbl
610              ] start_lbl dest_lbl def
611          ]
612        ]
613      | Some srcr12 ⇒
614        let 〈srcr11, srcr12〉 ≝ srcr12 in
615        let srcr2 ≝ extract_singleton ? srcrs2 in
616        match srcr2 with
617        [ None       ⇒ None ?
618        | Some srcr2 ⇒
619          let 〈def, tmpr1〉 ≝ fresh_reg def in
620          let 〈def, tmpr2〉 ≝ fresh_reg def in
621            adds_graph [
622              rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
623              rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
624              rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
625              rtl_st_move destr1 tmpr1 start_lbl
626            ] start_lbl dest_lbl def
627        ]
628      ]
629    ]
630  | op_subp ⇒
631    let destr ≝ extract_singleton ? destrs in
632    match destr with
633    [ None ⇒
634      let destr12 ≝ extract_pair ? destrs in
635      match destr12 with
636      [ None ⇒ None ?
637      | Some destr12 ⇒
638        let 〈destr1, destr2〉 ≝ destr12 in
639        let srcr12 ≝ extract_pair ? srcrs1 in
640        match srcr12 with
641        [ None ⇒ None ?
642        | Some srcr12 ⇒
643          let 〈srcr11, srcr12〉 ≝ srcr12 in
644          let srcr2 ≝ extract_singleton ? srcrs2 in
645          match srcr2 with
646          [ None ⇒ None ?
647          | Some srcr2 ⇒
648            adds_graph [
649              rtl_st_clear_carry start_lbl;
650              rtl_st_op2 Sub destr1 srcr11 srcr2 start_lbl;
651              rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl;
652              rtl_st_op2 Sub destr2 srcr12 destr2 start_lbl
653            ] start_lbl dest_lbl def
654          ]
655        ]
656      ]
657    | Some destr ⇒
658      match srcrs1 with
659      [ nil ⇒ None ?
660      | cons srcr1 tl ⇒
661        match srcrs2 with
662        [ nil ⇒ None ?
663        | cons srcr2 tl' ⇒
664          let 〈def, tmpr1〉 ≝ fresh_reg def in
665          let 〈def, tmpr2〉 ≝ fresh_reg def in
666            adds_graph [
667              rtl_st_op1 Cmpl tmpr1 srcr2 start_lbl;
668              rtl_st_int tmpr2 (bitvector_of_nat ? 1) start_lbl;
669              rtl_st_op2 Add tmpr1 tmpr1 tmpr2 start_lbl;
670              rtl_st_op2 Add destr srcr1 tmpr1 start_lbl
671            ] start_lbl dest_lbl def
672        ]
673      ]
674    ]
675  | op_cmp cmp ⇒
676    match cmp with
677    [ Compare_Equal ⇒
678      add_translates [
679        translate_op2 op_sub destrs srcrs1 srcrs2;
680        translate_op1 op_not_bool destrs destrs
681      ] start_lbl dest_lbl def
682    | Compare_NotEqual ⇒
683      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
684    | _ ⇒ None ?
685    ]
686  | op_cmpu cmp ⇒
687    match cmp with
688    [ Compare_Equal ⇒
689      add_translates [
690        translate_op2 op_sub destrs srcrs1 srcrs2;
691        translate_op1 op_not_bool destrs destrs
692      ] start_lbl dest_lbl def
693    | Compare_NotEqual ⇒
694      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
695    | _ ⇒ None ?
696    ]
697  | _ ⇒ ?
698  ].
699
700    | AST.Op_cmp AST.Cmp_ne, _, _, _
701    | AST.Op_cmpu AST.Cmp_ne, _, _, _ ->
702      translate_op2 AST.Op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
703
704    | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
705      let (def, tmpr) = fresh_reg def in
706      adds_graph
707        [RTL.St_clear_carry start_lbl ;
708         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
709         RTL.St_int (destr, 0, start_lbl) ;
710         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
711        start_lbl dest_lbl def
712
713    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
714      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
715        destrs srcrs2 srcrs1 start_lbl dest_lbl def
716
717    | AST.Op_cmpu AST.Cmp_le, _, _, _ ->
718      add_translates
719        [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ;
720         translate_op1 AST.Op_notbool destrs destrs]
721        start_lbl dest_lbl def
722
723    | AST.Op_cmpu AST.Cmp_ge, _, _, _ ->
724      add_translates
725        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
726         translate_op1 AST.Op_notbool destrs destrs]
727        start_lbl dest_lbl def
728
729    | AST.Op_cmp cmp, _, _, _ ->
730      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
731      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
732      add_translates
733        [translate_cst (AST.Cst_int 128) tmprs1 ;
734         translate_cst (AST.Cst_int 128) tmprs2 ;
735         translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ;
736         translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ;
737         translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2]
738        start_lbl dest_lbl def
739
740    | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
741      let (def, tmpr) = fresh_reg def in
742      add_translates
743        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ;
744         translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ;
745         translate_op2 AST.Op_or [destr] [destr] [tmpr] ;
746         adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ;
747         translate_op2 AST.Op_xor [destr] [destr] [tmpr]]
748        start_lbl dest_lbl def
749
750    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
751      let (def, tmpr1) = fresh_reg def in
752      let (def, tmpr2) = fresh_reg def in
753      add_translates
754        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
755         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
756         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
757         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
758         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
759        start_lbl dest_lbl def
760
761    | AST.Op_cmpp AST.Cmp_gt, _, _, _ ->
762      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
763        destrs srcrs2 srcrs1 start_lbl dest_lbl def
764
765    | AST.Op_cmpp AST.Cmp_le, _, _, _ ->
766      add_translates
767        [translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ;
768         translate_op1 AST.Op_notbool destrs destrs]
769        start_lbl dest_lbl def
770
771    | AST.Op_cmpp AST.Cmp_ge, _, _, _ ->
772      add_translates
773        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
774         translate_op1 AST.Op_notbool destrs destrs]
775        start_lbl dest_lbl def
776
777    | _ -> assert false (* wrong number of arguments *)
Note: See TracBrowser for help on using the repository browser.