source: src/RTLabs/RTLAbstoRTL.ma @ 1046

Last change on this file since 1046 was 1046, checked in by mulligan, 8 years ago

syntax of rtlabs was wrong: cast not const. more added to rtlabs --> rtl pass

File size: 36.8 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
419(*
420let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?)
421                      (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝
422  match op2 with
423  [ op_add ⇒
424    let destr ≝ extract_singleton ? destrs in
425    let srcr1 ≝ extract_singleton ? srcrs1 in
426    let srcr2 ≝ extract_singleton ? srcrs2 in
427    match destr with
428    [ None ⇒ None ?
429    | Some destr ⇒
430      match srcr1 with
431      [ None ⇒ None ?
432      | Some srcr1 ⇒
433        match srcr2 with
434        [ None ⇒ None ?
435        | Some srcr2 ⇒
436          adds_graph [
437            rtl_st_op2 Add destr srcr1 srcr2 start_lbl
438          ] start_lbl dest_lbl def
439        ]
440      ]
441    ]
442  | op_sub ⇒
443    let destr ≝ extract_singleton ? destrs in
444    let srcr1 ≝ extract_singleton ? srcrs1 in
445    let srcr2 ≝ extract_singleton ? srcrs2 in
446    match destr with
447    [ None ⇒ None ?
448    | Some destr ⇒
449      match srcr1 with
450      [ None ⇒ None ?
451      | Some srcr1 ⇒
452        match srcr2 with
453        [ None ⇒ None ?
454        | Some srcr2 ⇒
455          adds_graph [
456            rtl_st_clear_carry start_lbl;
457            rtl_st_op2 Sub destr srcr1 srcr2 start_lbl
458          ] start_lbl dest_lbl def
459        ]
460      ]
461    ]
462  | op_mul ⇒
463    let destr ≝ extract_singleton ? destrs in
464    let srcr1 ≝ extract_singleton ? srcrs1 in
465    let srcr2 ≝ extract_singleton ? srcrs2 in
466    match destr with
467    [ None ⇒ None ?
468    | Some destr ⇒
469      match srcr1 with
470      [ None ⇒ None ?
471      | Some srcr1 ⇒
472        match srcr2 with
473        [ None ⇒ None ?
474        | Some srcr2 ⇒
475          adds_graph [
476            rtl_st_opaccs Mul destr srcr1 srcr2 start_lbl
477          ] start_lbl dest_lbl def
478        ]
479      ]
480    ]
481  | op_div ⇒ None ? (* signed div not supported *)
482  | op_divu ⇒
483    let destr ≝ extract_singleton ? destrs in
484    let srcr1 ≝ extract_singleton ? srcrs1 in
485    let srcr2 ≝ extract_singleton ? srcrs2 in
486    match destr with
487    [ None ⇒ None ?
488    | Some destr ⇒
489      match srcr1 with
490      [ None ⇒ None ?
491      | Some srcr1 ⇒
492        match srcr2 with
493        [ None ⇒ None ?
494        | Some srcr2 ⇒
495          adds_graph [
496            rtl_st_opaccs Divu destr srcr1 srcr2 start_lbl
497          ] start_lbl dest_lbl def
498        ]
499      ]
500    ]
501  | op_modu ⇒
502    let destr ≝ extract_singleton ? destrs in
503    let srcr1 ≝ extract_singleton ? srcrs1 in
504    let srcr2 ≝ extract_singleton ? srcrs2 in
505    match destr with
506    [ None ⇒ None ?
507    | Some destr ⇒
508      match srcr1 with
509      [ None ⇒ None ?
510      | Some srcr1 ⇒
511        match srcr2 with
512        [ None ⇒ None ?
513        | Some srcr2 ⇒
514          adds_graph [
515            rtl_st_opaccs Modu destr srcr1 srcr2 start_lbl
516          ] start_lbl dest_lbl def
517        ]
518      ]
519    ]
520  | op_mod ⇒ None ? (* signed mod not supported *)
521  | op_and ⇒
522    let destr ≝ extract_singleton ? destrs in
523    let srcr1 ≝ extract_singleton ? srcrs1 in
524    let srcr2 ≝ extract_singleton ? srcrs2 in
525    match destr with
526    [ None ⇒ None ?
527    | Some destr ⇒
528      match srcr1 with
529      [ None ⇒ None ?
530      | Some srcr1 ⇒
531        match srcr2 with
532        [ None ⇒ None ?
533        | Some srcr2 ⇒
534          adds_graph [
535            rtl_st_op2 And destr srcr1 srcr2 start_lbl
536          ] start_lbl dest_lbl def
537        ]
538      ]
539    ]
540  | op_or ⇒
541    let destr ≝ extract_singleton ? destrs in
542    let srcr1 ≝ extract_singleton ? srcrs1 in
543    let srcr2 ≝ extract_singleton ? srcrs2 in
544    match destr with
545    [ None ⇒ None ?
546    | Some destr ⇒
547      match srcr1 with
548      [ None ⇒ None ?
549      | Some srcr1 ⇒
550        match srcr2 with
551        [ None ⇒ None ?
552        | Some srcr2 ⇒
553          adds_graph [
554            rtl_st_op2 Or destr srcr1 srcr2 start_lbl
555          ] start_lbl dest_lbl def
556        ]
557      ]
558    ]
559  | op_xor ⇒
560    let destr ≝ extract_singleton ? destrs in
561    let srcr1 ≝ extract_singleton ? srcrs1 in
562    let srcr2 ≝ extract_singleton ? srcrs2 in
563    match destr with
564    [ None ⇒ None ?
565    | Some destr ⇒
566      match srcr1 with
567      [ None ⇒ None ?
568      | Some srcr1 ⇒
569        match srcr2 with
570        [ None ⇒ None ?
571        | Some srcr2 ⇒
572          adds_graph [
573            rtl_st_op2 Xor destr srcr1 srcr2 start_lbl
574          ] start_lbl dest_lbl def
575        ]
576      ]
577    ]
578  | op_shru ⇒ None ? (* shifts not supported *)
579  | op_shr ⇒ None ?
580  | op_shl ⇒ None ?
581  | op_addf ⇒ None ? (* floats not supported *)
582  | op_subf ⇒ None ?
583  | op_mulf ⇒ None ?
584  | op_divf ⇒ None ?
585  | op_cmpf _ ⇒ None ?
586  | op_addp ⇒
587    let destr12 ≝ extract_pair ? destrs in
588    match destr12 with
589    [ None         ⇒ None ?
590    | Some destr12 ⇒
591      let 〈destr1, destr2〉 ≝ destr12 in
592      let srcr12 ≝ extract_pair ? srcrs1 in
593      match srcr12 with
594      [ None ⇒
595        let srcr2 ≝ extract_singleton ? srcrs1 in
596        match srcr2 with
597        [ None ⇒ None ?
598        | Some srcr2 ⇒
599          let srcr12 ≝ extract_pair ? srcrs2 in
600          match srcr12 with
601          [ None ⇒ None ?
602          | Some srcr12 ⇒
603            let 〈srcr11, srcr12〉 ≝ srcr12 in
604            let 〈def, tmpr1〉 ≝ fresh_reg def in
605            let 〈def, tmpr2〉 ≝ fresh_reg def in
606              adds_graph [
607                rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
608                rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
609                rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
610                rtl_st_move destr1 tmpr1 start_lbl
611              ] start_lbl dest_lbl def
612          ]
613        ]
614      | Some srcr12 ⇒
615        let 〈srcr11, srcr12〉 ≝ srcr12 in
616        let srcr2 ≝ extract_singleton ? srcrs2 in
617        match srcr2 with
618        [ None       ⇒ None ?
619        | Some srcr2 ⇒
620          let 〈def, tmpr1〉 ≝ fresh_reg def in
621          let 〈def, tmpr2〉 ≝ fresh_reg def in
622            adds_graph [
623              rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
624              rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
625              rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
626              rtl_st_move destr1 tmpr1 start_lbl
627            ] start_lbl dest_lbl def
628        ]
629      ]
630    ]
631  | op_subp ⇒
632    let destr ≝ extract_singleton ? destrs in
633    match destr with
634    [ None ⇒
635      let destr12 ≝ extract_pair ? destrs in
636      match destr12 with
637      [ None ⇒ None ?
638      | Some destr12 ⇒
639        let 〈destr1, destr2〉 ≝ destr12 in
640        let srcr12 ≝ extract_pair ? srcrs1 in
641        match srcr12 with
642        [ None ⇒ None ?
643        | Some srcr12 ⇒
644          let 〈srcr11, srcr12〉 ≝ srcr12 in
645          let srcr2 ≝ extract_singleton ? srcrs2 in
646          match srcr2 with
647          [ None ⇒ None ?
648          | Some srcr2 ⇒
649            adds_graph [
650              rtl_st_clear_carry start_lbl;
651              rtl_st_op2 Sub destr1 srcr11 srcr2 start_lbl;
652              rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl;
653              rtl_st_op2 Sub destr2 srcr12 destr2 start_lbl
654            ] start_lbl dest_lbl def
655          ]
656        ]
657      ]
658    | Some destr ⇒
659      match srcrs1 with
660      [ nil ⇒ None ?
661      | cons srcr1 tl ⇒
662        match srcrs2 with
663        [ nil ⇒ None ?
664        | cons srcr2 tl' ⇒
665          let 〈def, tmpr1〉 ≝ fresh_reg def in
666          let 〈def, tmpr2〉 ≝ fresh_reg def in
667            adds_graph [
668              rtl_st_op1 Cmpl tmpr1 srcr2 start_lbl;
669              rtl_st_int tmpr2 (bitvector_of_nat ? 1) start_lbl;
670              rtl_st_op2 Add tmpr1 tmpr1 tmpr2 start_lbl;
671              rtl_st_op2 Add destr srcr1 tmpr1 start_lbl
672            ] start_lbl dest_lbl def
673        ]
674      ]
675    ]
676  | op_cmp cmp ⇒
677    match cmp with
678    [ Compare_Equal ⇒
679      add_translates [
680        translate_op2 op_sub destrs srcrs1 srcrs2;
681        translate_op1 op_not_bool destrs destrs
682      ] start_lbl dest_lbl def
683    | Compare_NotEqual ⇒
684      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
685    | _ ⇒ None ?
686    ]
687  | op_cmpu cmp ⇒
688    match cmp with
689    [ Compare_Equal ⇒
690      add_translates [
691        translate_op2 op_sub destrs srcrs1 srcrs2;
692        translate_op1 op_not_bool destrs destrs
693      ] start_lbl dest_lbl def
694    | Compare_NotEqual ⇒
695      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
696    | Compare
697    | _ ⇒ None ?
698    ]
699  | _ ⇒ ?
700  ].
701
702    | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
703      let (def, tmpr) = fresh_reg def in
704      adds_graph
705        [RTL.St_clear_carry start_lbl ;
706         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
707         RTL.St_int (destr, 0, start_lbl) ;
708         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
709        start_lbl dest_lbl def
710
711    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
712      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
713        destrs srcrs2 srcrs1 start_lbl dest_lbl def
714
715    | AST.Op_cmpu AST.Cmp_le, _, _, _ ->
716      add_translates
717        [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ;
718         translate_op1 AST.Op_notbool destrs destrs]
719        start_lbl dest_lbl def
720
721    | AST.Op_cmpu AST.Cmp_ge, _, _, _ ->
722      add_translates
723        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
724         translate_op1 AST.Op_notbool destrs destrs]
725        start_lbl dest_lbl def
726
727    | AST.Op_cmp cmp, _, _, _ ->
728      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
729      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
730      add_translates
731        [translate_cst (AST.Cst_int 128) tmprs1 ;
732         translate_cst (AST.Cst_int 128) tmprs2 ;
733         translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ;
734         translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ;
735         translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2]
736        start_lbl dest_lbl def
737
738    | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
739      let (def, tmpr) = fresh_reg def in
740      add_translates
741        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ;
742         translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ;
743         translate_op2 AST.Op_or [destr] [destr] [tmpr] ;
744         adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ;
745         translate_op2 AST.Op_xor [destr] [destr] [tmpr]]
746        start_lbl dest_lbl def
747
748    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
749      let (def, tmpr1) = fresh_reg def in
750      let (def, tmpr2) = fresh_reg def in
751      add_translates
752        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
753         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
754         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
755         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
756         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
757        start_lbl dest_lbl def
758
759    | AST.Op_cmpp AST.Cmp_gt, _, _, _ ->
760      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
761        destrs srcrs2 srcrs1 start_lbl dest_lbl def
762
763    | AST.Op_cmpp AST.Cmp_le, _, _, _ ->
764      add_translates
765        [translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ;
766         translate_op1 AST.Op_notbool destrs destrs]
767        start_lbl dest_lbl def
768
769    | AST.Op_cmpp AST.Cmp_ge, _, _, _ ->
770      add_translates
771        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
772         translate_op1 AST.Op_notbool destrs destrs]
773        start_lbl dest_lbl def
774
775    | _ -> assert false (* wrong number of arguments *)
776*)
777
778definition translate_condcst ≝
779  λcst.
780  λstart_lbl: label.
781  λlbl_true: label.
782  λlbl_false: label.
783  λdef.
784  match cst with
785  [ cast_int i ⇒
786    let 〈def, tmpr〉 ≝ fresh_reg def in
787    adds_graph [
788      rtl_st_int tmpr i start_lbl;
789      rtl_st_cond_acc tmpr lbl_true lbl_false
790    ] start_lbl start_lbl def
791  | cast_addr_symbol x ⇒
792    let 〈def, r1〉 ≝ fresh_reg def in
793    let 〈def, r2〉 ≝ fresh_reg def in
794    let lbl ≝ fresh_label def in
795    match lbl with
796    [ None ⇒ None ?
797    | Some lbl ⇒
798      let def ≝ add_graph start_lbl (rtl_st_addr r1 r2 x lbl) def in
799        translate_condptr r1 r2 lbl lbl_true lbl_false def
800    ]
801  | cast_stack_offset off ⇒
802    let 〈def, r1〉 ≝ fresh_reg def in
803    let 〈def, r2〉 ≝ fresh_reg def in
804    let tmp_lbl ≝ fresh_label def in
805    match tmp_lbl with
806    [ None ⇒ None ?
807    | Some tmp_lbl ⇒
808      let def ≝ translate_cst (cast_stack_offset off) [r1; r2] start_lbl tmp_lbl def in
809      match def with
810      [ None ⇒ None ?
811      | Some def ⇒ translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def
812      ]
813    ]
814  | cast_float f ⇒ None ? (* error_float *)
815  ].
816
817definition size_of_op1_ret ≝
818  λop.
819  match op with
820  [ op_cast8_unsigned ⇒ Some ? 1
821  | op_cast8_signed ⇒ Some ? 1
822  | op_cast16_unsigned ⇒ Some ? 1
823  | op_cast16_signed ⇒ Some ? 1
824  | op_neg_int ⇒ Some ? 1
825  | op_not_int ⇒ Some ? 1
826  | op_int_of_ptr ⇒ Some ? 1
827  | op_ptr_of_int ⇒ Some ? 2
828  | op_id ⇒ None ? (* invalid_argument *)
829  | _ ⇒ None ? (* error_float *)
830  ].
831
832definition translate_cond1 ≝
833  λop1.
834  λsrcrs: list register.
835  λstart_lbl: label.
836  λlbl_true: label.
837  λlbl_false: label.
838  λdef.
839  match op1 with
840  [ op_id ⇒
841    let srcr ≝ extract_singleton ? srcrs in
842    match srcr with
843    [ None ⇒
844      let srcr12 ≝ extract_pair ? srcrs in
845      match srcr12 with
846      [ None ⇒ None ?
847      | Some srcr12 ⇒
848        let 〈srcr1, srcr2〉 ≝ srcr12 in
849          translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def
850      ]
851    | Some srcr ⇒
852      adds_graph [
853        rtl_st_cond_acc srcr lbl_true lbl_false
854      ] start_lbl start_lbl def
855    ]
856  | _     ⇒
857    let size ≝ size_of_op1_ret op1 in
858    match size with
859    [ None ⇒ None ?
860    | Some size ⇒
861      let 〈def, destrs〉 ≝ fresh_regs def size in
862      let lbl ≝ fresh_label def in
863      match lbl with
864      [ None ⇒ None ?
865      | Some lbl ⇒
866        let def ≝ translate_op1 op1 destrs srcrs start_lbl lbl def in
867        match def with
868        [ None ⇒ None ?
869        | Some def ⇒
870          let destr ≝ extract_singleton ? destrs in
871          match destr with
872          [ None ⇒
873            let destr12 ≝ extract_pair ? destrs in
874            match destr12 with
875            [ None ⇒ None ?
876            | Some destr12 ⇒
877              let 〈destr1, destr2〉 ≝ destr12 in
878                translate_condptr destr1 destr2 start_lbl lbl_true lbl_false def
879            ]
880          | Some destr ⇒
881            adds_graph [
882              rtl_st_cond_acc destr lbl_true lbl_false
883            ] start_lbl start_lbl def
884          ]
885        ]
886      ]
887    ]
888  ].
889
890definition size_of_op2_ret ≝
891  λn: nat.
892  λop2.
893  match op2 with
894  [ op_add ⇒ Some ? 1
895  | op_sub ⇒ Some ? 1
896  | op_mul ⇒ Some ? 1
897  | op_div ⇒ Some ? 1
898  | op_divu ⇒ Some ? 1
899  | op_mod ⇒ Some ? 1
900  | op_modu ⇒ Some ? 1
901  | op_and ⇒ Some ? 1
902  | op_or ⇒ Some ? 1
903  | op_xor ⇒ Some ? 1
904  | op_shl ⇒ Some ? 1
905  | op_shr ⇒ Some ? 1
906  | op_shru ⇒ Some ? 1
907  | op_cmp _ ⇒ Some ? 1
908  | op_cmpu _ ⇒ Some ? 1
909  | op_cmpp _ ⇒ Some ? 1
910  | op_addp ⇒ Some ? 2
911  | op_subp ⇒
912    if eq_nat n 4 then
913      Some ? 1
914    else
915      Some ? 2
916  | _ ⇒ None ? (* error_float *)
917  ].
918
919axiom translate_op2:
920  op2 → list register → list register → list register → label → label → rtl_internal_function → option rtl_internal_function.
921
922definition translate_cond2 ≝
923  λop2.
924  λsrcrs1: list register.
925  λsrcrs2: list register.
926  λstart_lbl: label.
927  λlbl_true: label.
928  λlbl_false: label.
929  λdef.
930  match op2 with
931  [ op_cmp cmp ⇒
932    match cmp with
933    [ Compare_Equal ⇒
934      let srcr1 ≝ extract_singleton ? srcrs1 in
935      match srcr1 with
936      [ None ⇒ None ?
937      | Some srcr1 ⇒
938        let srcr2 ≝ extract_singleton ? srcrs2 in
939        match srcr2 with
940        [ None ⇒ None ?
941        | Some srcr2 ⇒
942          let 〈def, tmpr〉 ≝ fresh_reg def in
943          adds_graph [
944            rtl_st_clear_carry start_lbl;
945            rtl_st_op2 Sub tmpr srcr1 srcr2 start_lbl;
946            rtl_st_cond_acc tmpr lbl_false lbl_true
947          ] start_lbl start_lbl def
948        ]
949      ]
950    | _ ⇒
951      let n ≝ length ? srcrs1 + length ? srcrs2 in
952      match size_of_op2_ret n op2 with
953      [ None ⇒ None ?
954      | Some size ⇒
955        let 〈def, destrs〉 ≝ fresh_regs def size in
956        let lbl ≝ fresh_label def in
957        match lbl with
958        [ None ⇒ None ?
959        | Some lbl ⇒
960          match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
961          [ None ⇒ None ?
962          | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
963          ]
964        ]
965      ]
966    ]
967  | _ ⇒
968    let n ≝ length ? srcrs1 + length ? srcrs2 in
969    match size_of_op2_ret n op2 with
970    [ None ⇒ None ?
971    | Some size ⇒
972      let 〈def, destrs〉 ≝ fresh_regs def size in
973      let lbl ≝ fresh_label def in
974      match lbl with
975      [ None ⇒ None ?
976      | Some lbl ⇒
977        match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
978        [ None ⇒ None ?
979        | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
980        ]
981      ]
982    ]
983  ].
984
985let rec addressing_pointer (mode: ?) (args: ?) (destr1: ?)
986                           (destr2: ?) (start_lbl: label)
987                           (dest_lbl: label) (def: rtl_internal_function) ≝
988  let destrs ≝ [ destr1; destr2 ] in
989  match mode with
990  [ Aindexed off ⇒
991    let srcr12 ≝ extract_singleton ? args in
992    match srcr12 with
993    [ None ⇒ None ?
994    | Some srcr12 ⇒
995      let srcr12 ≝ extract_pair ? srcr12 in
996      match srcr12 with
997      [ None ⇒ None ?
998      | Some srcr12 ⇒
999        let 〈srcr1, srcr2〉 ≝ srcr12 in
1000        let 〈def, tmpr〉 ≝ fresh_reg def in
1001        add_translates [
1002          adds_graph [
1003            rtl_st_int tmpr off start_lbl
1004          ];
1005          translate_op2 op_addp destrs [ srcr1 ; srcr2 ] [tmpr]
1006        ] start_lbl dest_lbl def
1007      ]
1008    ]
1009  | Aindexed2 ⇒
1010    let args_pair ≝ extract_pair ? args in
1011    match args_pair with
1012    [ None ⇒ None ?
1013    | Some args_pair ⇒
1014      let 〈lft, rgt〉 ≝ args_pair in
1015      let srcr1112 ≝ extract_pair ? lft in
1016      let srcr2 ≝ extract_singleton ? rgt in
1017      match srcr1112 with
1018      [ None ⇒
1019        let srcr2 ≝ extract_singleton ? rgt in
1020        let srcr1112 ≝ extract_pair ? lft in
1021        match srcr2 with
1022        [ None ⇒ None ?
1023        | Some srcr2 ⇒
1024          match srcr1112 with
1025          [ None ⇒ None ?
1026          | Some srcr1112 ⇒
1027            let 〈srcr11, srcr12〉 ≝ srcr1112 in
1028            translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
1029          ]
1030        ]
1031      | Some srcr1112 ⇒
1032        let 〈srcr11, srcr12〉 ≝ srcr1112 in
1033        match srcr2 with
1034        [ None ⇒ None ?
1035        | Some srcr2 ⇒
1036          translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
1037        ]
1038      ]
1039    ]
1040  | Aglobal x off ⇒
1041    let 〈def, tmpr〉 ≝ fresh_reg def in
1042    add_translates [
1043      adds_graph [
1044        rtl_st_int tmpr off start_lbl;
1045        rtl_st_addr destr1 destr2 x start_lbl
1046      ];
1047      translate_op2 op_addp destrs destrs [ tmpr ]
1048    ] start_lbl dest_lbl def
1049  | Abased x off ⇒
1050    let srcrs ≝ extract_singleton ? args in
1051    match srcrs with
1052    [ None ⇒ None ?
1053    | Some srcrs ⇒
1054      let 〈def, tmpr1〉 ≝ fresh_reg def in
1055      let 〈def, tmpr2〉 ≝ fresh_reg def in
1056      (* mode, args, destr1, destr2, start_lbl, dest_lbl, def *)
1057      (* addressing_pointer (Aglobal x off) [ ] tmpr1 tmpr2; *)
1058      let address_unfold ≝
1059        let 〈def, tmpr〉 ≝ fresh_reg def in
1060          add_translates [
1061            adds_graph [
1062              rtl_st_int tmpr off start_lbl;
1063              rtl_st_addr tmpr1 tmpr2 x start_lbl
1064           ];
1065            translate_op2 op_addp destrs destrs [ tmpr ]
1066         ]
1067      in
1068      add_translates [
1069        address_unfold;
1070        translate_op2 op_addp destrs [ tmpr1; tmpr2 ] srcrs
1071      ] start_lbl dest_lbl def
1072    ]
1073  | Ainstack off ⇒
1074    let 〈def, tmpr〉 ≝ fresh_reg def in
1075    add_translates [
1076      adds_graph [
1077        rtl_st_int tmpr off start_lbl;
1078        rtl_st_stack_addr destr1 destr2 start_lbl
1079      ];
1080      translate_op2 op_addp destrs destrs [ tmpr ]
1081    ] start_lbl dest_lbl def
1082  | _ ⇒ None ? (* wrong number of arguments *)
1083  ].
1084
1085definition translate_load ≝
1086  λq.
1087  λmode.
1088  λargs.
1089  λdestrs.
1090  λstart_lbl: label.
1091  λdest_lbl: label.
1092  λdef.
1093  match q with
1094  [ q_int b ⇒
1095    if eq_bv ? b (bitvector_of_nat ? 1) then
1096      match extract_singleton ? destrs with
1097      [ None ⇒ None ? (* error: size error in load *)
1098      | Some destr ⇒
1099        let 〈def, addr1〉 ≝ fresh_reg def in
1100        let 〈def, addr2〉 ≝ fresh_reg def in
1101          Some ? (add_translates [
1102            addressing_pointer mode args addr1 addr2;
1103            adds_graph [
1104              rtl_st_load destr addr1 addr2 start_lbl
1105            ]
1106          ] start_lbl dest_lbl def)
1107      ]
1108    else
1109      None ? (* error: size error in load *)
1110  | q_ptr ⇒
1111    match extract_pair ? destrs with
1112    [ None ⇒ None ? (* error: size error in load *)
1113    | Some destr12 ⇒
1114      let 〈destr1, destr2〉 ≝ destr12 in
1115      let 〈def, addr1〉 ≝ fresh_reg def in
1116      let 〈def, addr2〉 ≝ fresh_reg def in
1117      let addr ≝ [ addr1; addr2 ] in
1118      let 〈def, tmpr〉 ≝ fresh_reg def in
1119        Some ? (
1120          add_translates [
1121            addressing_pointer mode args addr1 addr2;
1122            adds_graph [
1123              rtl_st_load destr1 addr1 addr2 start_lbl;
1124              rtl_st_int tmpr (bitvector_of_nat ? 1) start_lbl
1125            ];
1126            translate_op2 op_addp addr addr [ tmpr ];
1127            adds_graph [
1128              rtl_st_load destr2 addr1 addr2 start_lbl
1129            ]
1130          ] start_lbl dest_lbl def
1131        )
1132    ]
1133  | _ ⇒ None ? (* error: size error in load *)
1134  ].
1135 
1136definition make_addr ≝
1137  λA: Type[0].
1138  λlst: list A.
1139  match lst with
1140  [ cons hd tl ⇒
1141    match tl with
1142    [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
1143    | _ ⇒ None ? (* do not use on these arguments *)
1144    ]
1145  | _ ⇒ None ? (* do not use on these arguments *)
1146  ].
1147 
1148definition translate_store_internal ≝
1149  λaddr.
1150  λtmp_addr.
1151  λtmpr.
1152  λstart_lbl.
1153  λdest_lbl.
1154  λtmp_addr1.
1155  λtmp_addr2.
1156  λtranslates_off.
1157  λsrcr.
1158    let 〈translates, off〉 ≝ translates_off in
1159    let translates ≝ translates @
1160      [ adds_graph [
1161          rtl_st_int tmpr off start_lbl
1162        ];
1163        translate_op2 op_addp tmp_addr addr [ tmpr ];
1164        adds_graph [
1165          rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
1166        ]
1167      ]
1168    in
1169    let 〈ignore, result〉 ≝ half_add ? off int_size in
1170      〈translates, result〉.
1171 
1172definition translate_store ≝
1173  λaddr.
1174  λsrcrs.
1175  λstart_lbl.
1176  λdest_lbl.
1177  λdef.
1178    let 〈def, tmp_addr〉 ≝ fresh_regs def (length ? addr) in
1179    match make_addr ? tmp_addr with
1180    [ None ⇒ None ?
1181    | Some tmp_addr12 ⇒
1182      let 〈tmp_addr1, tmp_addr2〉 ≝ tmp_addr12 in
1183      let 〈def, tmpr〉 ≝ fresh_reg def in
1184      let f ≝ translate_store_internal addr tmp_addr tmpr start_lbl dest_lbl tmp_addr1 tmp_addr2 in
1185      let 〈translates, ignore〉 ≝ foldl ? ? f 〈[], zero ?〉 srcrs in
1186        add_translates translates start_lbl dest_lbl def
1187    ].
1188
1189definition translate_stmt ≝
1190  λlenv.
1191  λlbl.
1192  λstmt.
1193  λdef.
1194  match stmt with
1195  [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
1196  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
1197  | St_cast destr cst lbl' ⇒
1198      translate_cst cst (find_local_env destr lenv) lbl lbl' def
1199  | _ ⇒ ?
1200  ].
1201
1202let translate_stmt lenv lbl stmt def = match stmt with
1203
1204  | RTLabs.St_skip lbl' ->
1205    add_graph lbl (RTL.St_skip lbl') def
1206
1207  | RTLabs.St_cost (cost_lbl, lbl') ->
1208    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
1209
1210  | RTLabs.St_cst (destr, cst, lbl') ->
1211    translate_cst cst (find_local_env destr lenv) lbl lbl' def
1212
1213  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
1214    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
1215      lbl lbl' def
1216
1217  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
1218    translate_op2 op2 (find_local_env destr lenv)
1219      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
1220
1221  | RTLabs.St_load (_, addr, destr, lbl') ->
1222    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
1223      lbl lbl' def
1224
1225  | RTLabs.St_store (_, addr, srcr, lbl') ->
1226    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
1227      lbl lbl' def
1228
1229  | RTLabs.St_call_id (f, args, None, _, lbl') ->
1230    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
1231
1232  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
1233    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
1234                                   find_local_env retr lenv, lbl')) def
1235
1236  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
1237    let (f1, f2) = find_and_addr f lenv in
1238    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
1239
1240  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
1241    let (f1, f2) = find_and_addr f lenv in
1242    add_graph lbl
1243      (RTL.St_call_ptr
1244         (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
1245
1246  | RTLabs.St_tailcall_id (f, args, _) ->
1247    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
1248
1249  | RTLabs.St_tailcall_ptr (f, args, _) ->
1250    let (f1, f2) = find_and_addr f lenv in
1251    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
1252
1253  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
1254    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
1255
1256  | RTLabs.St_jumptable _ ->
1257    error "Jump tables not supported yet."
1258
1259  | RTLabs.St_return None ->
1260    add_graph lbl (RTL.St_return []) def
1261
1262  | RTLabs.St_return (Some r) ->
1263    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
Note: See TracBrowser for help on using the repository browser.