source: src/RTLabs/RTLAbstoRTL.ma @ 1049

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

more stuff added

File size: 39.1 KB
Line 
1include "RTLabs/syntax.ma".
2include "RTL/RTL.ma".
3include "common/AssocList.ma".
4include "common/Graphs.ma".
5include "common/Maps.ma".
6include "utilities/HMap.ma".
7
8definition add_graph ≝
9  λl: label.
10  λstmt.
11  λp.
12  let rtl_if_luniverse' ≝ rtl_if_luniverse p in
13  let rtl_if_runiverse' ≝ rtl_if_runiverse p in
14  let rtl_if_sig' ≝ rtl_if_sig p in
15  let rtl_if_result' ≝ rtl_if_result p in
16  let rtl_if_params' ≝ rtl_if_params p in
17  let rtl_if_locals' ≝ rtl_if_locals p in
18  let rtl_if_stacksize' ≝ rtl_if_stacksize p in
19  let rtl_if_graph' ≝ add ? ? (rtl_if_graph p) l stmt in
20  let rtl_if_entry' ≝ rtl_if_entry p in
21  let rtl_if_exit' ≝ rtl_if_exit p in
22    mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig'
23                             rtl_if_params' rtl_if_params' rtl_if_locals'
24                             rtl_if_stacksize' rtl_if_graph' rtl_if_entry'
25                             rtl_if_exit'.
26     
27definition fresh_label ≝
28  λdef.
29    match fresh LabelTag (rtl_if_luniverse def) with
30    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
31    | Error _ ⇒ None ?
32    ].
33
34axiom register_fresh: universe RegisterTag → register.
35
36definition fresh_reg: rtl_internal_function → rtl_internal_function × register ≝
37  λdef.
38    let r ≝ register_fresh (rtl_if_runiverse def) in
39    let locals ≝ r :: rtl_if_locals def in
40    let rtl_if_luniverse' ≝ rtl_if_luniverse def in
41    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
42    let rtl_if_sig' ≝ rtl_if_sig def in
43    let rtl_if_result' ≝ rtl_if_result def in
44    let rtl_if_params' ≝ rtl_if_params def in
45    let rtl_if_locals' ≝ locals in
46    let rtl_if_stacksize' ≝ rtl_if_stacksize def in
47    let rtl_if_graph' ≝ rtl_if_graph def in
48    let rtl_if_entry' ≝ rtl_if_entry def in
49    let rtl_if_exit' ≝ rtl_if_exit def in
50      〈mk_rtl_internal_function
51        rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig' rtl_if_result'
52        rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
53        rtl_if_entry' rtl_if_exit', r〉.
54       
55let rec fresh_regs (def: rtl_internal_function) (n: nat) on n ≝
56  match n with
57  [ O   ⇒ 〈def, [ ]〉
58  | S n ⇒
59    let 〈def, res〉 ≝ fresh_regs def n in
60    let 〈def, r〉 ≝ fresh_reg def in
61      〈def, r :: res〉
62  ].
63
64definition addr_regs ≝
65  λregs.
66  match regs with
67  [ cons hd tl ⇒
68    match tl with
69    [ cons hd' tl' ⇒ Some (register × register) 〈hd, hd'〉
70    | nil          ⇒ None (register × register)
71    ]
72  | nil ⇒ None (register × register) (* registers are not an address *)
73  ].
74
75let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
76  match n with
77  [ O ⇒ [ ]
78  | S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n')
79  ].
80
81definition choose_rest ≝
82  λA: Type[0].
83  λleft, right: list A.
84  match left with
85  [ nil ⇒
86    match right with
87    [ nil ⇒ None ?
88    | _ ⇒ Some ? right
89    ]
90  | _ ⇒ Some ? left
91  ].
92
93definition complete_regs ≝
94  λdef.
95  λsrcrs1.
96  λsrcrs2.
97  let nb_added ≝ abs ((length ? srcrs1) - (length ? srcrs2)) in
98  let 〈def, added_regs〉 ≝ fresh_regs def nb_added in
99    if gtb nb_added 0 then
100      〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
101    else
102      〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
103
104definition size_of_sig_type ≝
105  λsig.
106  match sig with
107  [ ASTint isize sign ⇒
108    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
109      Some ? (isize' ÷ (nat_of_bitvector ? int_size))
110  | ASTfloat _ ⇒ None ?
111  | ASToffset ⇒ Some ? (nat_of_bitvector ? int_size)
112  | ASTptr rgn ⇒ Some ? (nat_of_bitvector ? ptr_size)
113  ].
114
115inductive register_type: Type[0] ≝
116  | register_int: register → register_type
117  | register_ptr: register → register → register_type.
118
119definition local_env ≝ map register (list register).
120definition mem_local_env ≝ map_member register (list register) register_ord.
121definition add_local_env ≝ map_insert register (list register) register_ord.
122definition find_local_env ≝ map_lookup register (list register) register_ord.
123
124definition initialize_local_env_internal ≝
125  λeq.
126  λruniverse.
127  λptrs.
128  λlenv.
129  λr.
130    let fresh ≝ snd ? ? (fresh_reg runiverse) in
131    let rt ≝
132      match member ? eq r ptrs with
133      [ true  ⇒ register_ptr r fresh
134      | false ⇒ register_int r
135      ]
136    in
137    add_local_env ? ? 〈r, rt〉 lenv.
138
139definition initialize_local_env ≝
140  λruniverse.
141  λptrs.
142  λregisters.
143    foldl ? ? (initialize_local_env_internal (eq_identifier RegisterTag) runiverse ptrs) [ ] registers.
144
145definition filter_and_to_list_local_env_internal ≝
146  λlenv.
147  λl.
148  λr.
149  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
150  [ Some entry ⇒
151    match entry with
152    [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ])
153    | register_int r ⇒ (l @ [ r ])
154    ]
155  | None       ⇒ [ ] (* dpm: should this be none? *)
156  ].
157
158definition filter_and_to_list_local_env ≝
159  λlenv.
160  λregisters.
161    foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers.
162
163definition list_of_register_type ≝
164  λrt.
165  match rt with
166  [ register_ptr r1 r2 ⇒ [ r1; r2 ]
167  | register_int r ⇒ [ r ]
168  ].
169
170definition find_and_list ≝
171  λr.
172  λlenv.
173  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
174  [ None      ⇒ [ ] (* dpm: should this be none? *)
175  | Some lkup ⇒ list_of_register_type lkup
176  ].
177
178definition find_and_list_args ≝
179  λargs.
180  λlenv.
181    map ? ? (λr. find_and_list r lenv) args.
182
183definition find_and_addr ≝
184  λr.
185  λlenv.
186  match find_and_list r lenv with
187  [ cons hd tl ⇒
188    match tl with
189    [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
190    | nil          ⇒ None ?
191    ]
192  | nil ⇒ None ? (* dpm: was assert false *)
193  ].
194
195definition rtl_args ≝
196  λregs_list.
197  λlenv.
198    flatten ? (find_and_list_args regs_list lenv).
199
200definition change_label ≝
201  λlbl.
202  λstmt: rtl_statement.
203  match stmt with
204  [ rtl_st_skip _ ⇒ rtl_st_skip lbl
205  | rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl
206  | rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl
207  | rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl
208  | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
209  | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
210  | rtl_st_opaccs opaccs d s1 s2 _ ⇒ rtl_st_opaccs opaccs d s1 s2 lbl
211  | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
212  | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
213  | rtl_st_clear_carry _ ⇒ rtl_st_clear_carry lbl
214  | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl
215  | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl
216  | rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl
217  | rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl
218  | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a
219  | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
220  | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2
221  | rtl_st_return r ⇒ rtl_st_return r
222  | _ ⇒ ?
223  ].
224
225let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝
226  match stmt_list with
227  [ nil ⇒ Some ? def
228  | cons hd tl ⇒
229    match tl with
230    [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
231    | cons hd' tl' ⇒
232      let tmp_lbl ≝ fresh_label def in
233      match tmp_lbl with
234      [ None ⇒ None ?
235      | Some tmp_lbl ⇒
236        let stmt ≝ change_label tmp_lbl hd in
237        let def ≝ add_graph start_lbl stmt def in
238          adds_graph tl tmp_lbl dest_lbl def
239      ]
240    ]
241  ].
242 
243(* dpm: had to lift this into option *)
244let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
245                       (def: ?) on translate_list ≝
246  match translate_list with
247  [ nil ⇒ Some ? def
248  | cons hd tl ⇒
249    match tl with
250    [ nil ⇒ hd start_lbl dest_lbl def
251    | cons hd' tl' ⇒
252      let tmp_lbl ≝ fresh_label def in
253      match tmp_lbl with
254      [ None ⇒ None ?
255      | Some tmp_lbl ⇒
256        match hd start_lbl tmp_lbl def with
257        [ None ⇒ None ?
258        | Some def ⇒ add_translates tl tmp_lbl dest_lbl def
259        ]
260      ]
261    ]
262  ].
263 
264
265(* dpm: horrendous, use dependent types.
266  length destr = length srcrs *)
267let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label)
268                       (dest_lbl: label) (def: ?) ≝
269  match destrs with
270  [ nil ⇒
271    match srcrs with
272    [ nil        ⇒ Some ? def
273    | cons hd tl ⇒ None ?
274    ]
275  | cons hd tl ⇒
276    match srcrs with
277    [ nil        ⇒ None ?
278    | cons hd' tl' ⇒
279      match tl with
280      [ nil            ⇒
281        match tl' with
282        (* one element lists *)
283        [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def)
284        | cons hd'' tl'' ⇒ None ?
285        ]
286      | cons hd'' tl'' ⇒
287        match tl' with
288        [ nil ⇒ None ?
289        (* multielement lists *)
290        | cons hd''' tl''' ⇒
291          let tmp_lbl ≝ fresh_label def in
292          match tmp_lbl with
293          [ None ⇒ None ?
294          | Some tmp_lbl ⇒
295            let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in
296              translate_move tl tl' tmp_lbl dest_lbl def
297          ]
298        ]
299      ]
300    ]
301  ].
302
303definition translate_cst ≝
304  λcst.
305  λdestrs.
306  λstart_lbl.
307  λdest_lbl.
308  λdef.
309  match cst with
310  [ cast_int i ⇒
311    match destrs with
312    [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
313    | cons hd tl ⇒
314      match tl with
315      [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_int hd i dest_lbl) def)
316      | cons hd' tl' ⇒ None ?
317      ]
318    ]
319  | cast_addrsymbol id ⇒
320    match destrs with
321    [ nil ⇒ None ?
322    | cons hd tl ⇒
323      match tl with
324      [ nil ⇒ None ?
325      | cons hd' tl' ⇒
326        Some ? (add_graph start_lbl (rtl_st_addr hd hd' id dest_lbl) def)
327      ]
328    ]
329  | cast_offset off ⇒
330    match destrs with
331    [ nil ⇒ None ?
332    | cons hd tl ⇒
333      match tl with
334      [ nil ⇒ None ?
335      | cons hd' tl' ⇒
336        let 〈def, tmpr〉 ≝ fresh_reg def in
337        adds_graph [
338          rtl_st_stack_addr hd hd' start_lbl;
339          rtl_st_int tmpr off start_lbl;
340          rtl_st_op2 Add hd hd tmpr start_lbl;
341          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
342          rtl_st_op2 Addc hd' hd' tmpr start_lbl
343        ] start_lbl dest_lbl def
344      ]
345    ]
346  | cast_stack ⇒ ?
347  | cast_sizeof size ⇒ ?
348  (* | cast_float f ⇒ None ? *) (* what are we doing with floats? *)
349  ].
350
351definition extract_singleton ≝
352  λA: Type[0].
353  λl: list A.
354  match l with
355  [ nil ⇒ None ?
356  | cons hd tl ⇒
357    match tl with
358    [ nil ⇒ Some ? hd
359    | cons hd tl ⇒ None ?
360    ]
361  ].
362
363definition extract_pair ≝
364  λA: Type[0].
365  λl: list A.
366  match l with
367  [ nil ⇒ None ?
368  | cons hd tl ⇒
369    match tl with
370    [ nil ⇒ None ?
371    | cons hd' tl' ⇒
372      match tl' with
373      [ nil ⇒ Some ? 〈hd, hd'〉
374      | cons hd'' tl'' ⇒ None ?
375      ]
376    ]
377  ].
378
379definition translate_op1 ≝
380  λop1.
381  λdestrs.
382  λsrcrs.
383  λstart_lbl.
384  λdest_lbl.
385  λdef.
386  match op1 with
387  [ op_cast8_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
388  | op_cast8_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
389  | op_cast16_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
390  | op_cast16_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
391  | op_neg_int ⇒
392    let dstr ≝ extract_singleton ? destrs in
393    let srcr ≝ extract_singleton ? srcrs in
394    match dstr with
395    [ None ⇒ None ?
396    | Some dstr ⇒
397      match srcr with
398      [ None ⇒ None ?
399      | Some srcr ⇒
400        adds_graph [
401          rtl_st_op1 Cmpl dstr srcr start_lbl;
402          rtl_st_op1 Inc dstr dstr start_lbl
403        ] start_lbl dest_lbl def
404      ]
405    ]
406  | op_not_int ⇒
407    let dstr ≝ extract_singleton ? destrs in
408    let srcr ≝ extract_singleton ? srcrs in
409    match dstr with
410    [ None ⇒ None ?
411    | Some dstr ⇒
412      match srcr with
413      [ None ⇒ None ?
414      | Some srcr ⇒
415        adds_graph [
416          rtl_st_op1 Cmpl dstr srcr start_lbl
417        ] start_lbl dest_lbl def
418      ]
419    ]
420  | op_id ⇒ translate_move destrs srcrs start_lbl dest_lbl def
421  | op_ptr_of_int ⇒
422    let destr12 ≝ extract_pair ? destrs in
423    let srcr ≝ extract_singleton ? srcrs in
424    match destr12 with
425    [ None ⇒ None ?
426    | Some destr12 ⇒
427      let 〈destr1, destr2〉 ≝ destr12 in
428      match srcr with
429      [ None ⇒ None ?
430      | Some srcr ⇒
431        adds_graph [
432          rtl_st_move destr1 srcr dest_lbl;
433          rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl
434        ] start_lbl dest_lbl def
435      ]
436    ]
437  | op_int_of_ptr ⇒
438    let destr ≝ extract_singleton ? destrs in
439    match destr with
440    [ None ⇒ None ?
441    | Some destr ⇒
442      match srcrs with
443      [ nil ⇒ None ?
444      | cons srcr tl ⇒
445        Some ? (add_graph start_lbl (rtl_st_move destr srcr dest_lbl) def)
446      ]
447    ]
448  | op_not_bool ⇒
449    let destr ≝ extract_singleton ? destrs in
450    let srcrs ≝ extract_singleton ? srcrs in
451    match destr with
452    [ None ⇒ None ?
453    | Some destr ⇒
454      match srcrs with
455      [ None ⇒ None ?
456      | Some srcr ⇒
457        let 〈def, tmpr〉 ≝ fresh_reg def in
458        adds_graph [
459          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
460          rtl_st_clear_carry start_lbl;
461          rtl_st_op2 Sub destr tmpr srcr start_lbl;
462          rtl_st_int destr (bitvector_of_nat ? 0) dest_lbl;
463          rtl_st_op2 Addc destr destr destr start_lbl;
464          rtl_st_int tmpr (bitvector_of_nat ? 1) dest_lbl;
465          rtl_st_op2 Xor destr destr tmpr start_lbl
466        ] start_lbl dest_lbl def
467      ]
468    ]
469  | _ ⇒ None ? (* error float *)
470  ].
471
472definition translate_condptr ≝
473  λr1.
474  λr2.
475  λstart_lbl: label.
476  λlbl_true: label.
477  λlbl_false: label.
478  λdef.
479  let 〈def, tmpr〉 ≝ fresh_reg def in
480    adds_graph [
481      rtl_st_op2 Or tmpr r1 r2 start_lbl;
482      rtl_st_cond_acc tmpr lbl_true lbl_false
483    ] start_lbl start_lbl def.
484
485(*
486let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?)
487                      (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝
488  match op2 with
489  [ op_add ⇒
490    let destr ≝ extract_singleton ? destrs in
491    let srcr1 ≝ extract_singleton ? srcrs1 in
492    let srcr2 ≝ extract_singleton ? srcrs2 in
493    match destr with
494    [ None ⇒ None ?
495    | Some destr ⇒
496      match srcr1 with
497      [ None ⇒ None ?
498      | Some srcr1 ⇒
499        match srcr2 with
500        [ None ⇒ None ?
501        | Some srcr2 ⇒
502          adds_graph [
503            rtl_st_op2 Add destr srcr1 srcr2 start_lbl
504          ] start_lbl dest_lbl def
505        ]
506      ]
507    ]
508  | op_sub ⇒
509    let destr ≝ extract_singleton ? destrs in
510    let srcr1 ≝ extract_singleton ? srcrs1 in
511    let srcr2 ≝ extract_singleton ? srcrs2 in
512    match destr with
513    [ None ⇒ None ?
514    | Some destr ⇒
515      match srcr1 with
516      [ None ⇒ None ?
517      | Some srcr1 ⇒
518        match srcr2 with
519        [ None ⇒ None ?
520        | Some srcr2 ⇒
521          adds_graph [
522            rtl_st_clear_carry start_lbl;
523            rtl_st_op2 Sub destr srcr1 srcr2 start_lbl
524          ] start_lbl dest_lbl def
525        ]
526      ]
527    ]
528  | op_mul ⇒
529    let destr ≝ extract_singleton ? destrs in
530    let srcr1 ≝ extract_singleton ? srcrs1 in
531    let srcr2 ≝ extract_singleton ? srcrs2 in
532    match destr with
533    [ None ⇒ None ?
534    | Some destr ⇒
535      match srcr1 with
536      [ None ⇒ None ?
537      | Some srcr1 ⇒
538        match srcr2 with
539        [ None ⇒ None ?
540        | Some srcr2 ⇒
541          adds_graph [
542            rtl_st_opaccs Mul destr srcr1 srcr2 start_lbl
543          ] start_lbl dest_lbl def
544        ]
545      ]
546    ]
547  | op_div ⇒ None ? (* signed div not supported *)
548  | op_divu ⇒
549    let destr ≝ extract_singleton ? destrs in
550    let srcr1 ≝ extract_singleton ? srcrs1 in
551    let srcr2 ≝ extract_singleton ? srcrs2 in
552    match destr with
553    [ None ⇒ None ?
554    | Some destr ⇒
555      match srcr1 with
556      [ None ⇒ None ?
557      | Some srcr1 ⇒
558        match srcr2 with
559        [ None ⇒ None ?
560        | Some srcr2 ⇒
561          adds_graph [
562            rtl_st_opaccs Divu destr srcr1 srcr2 start_lbl
563          ] start_lbl dest_lbl def
564        ]
565      ]
566    ]
567  | op_modu ⇒
568    let destr ≝ extract_singleton ? destrs in
569    let srcr1 ≝ extract_singleton ? srcrs1 in
570    let srcr2 ≝ extract_singleton ? srcrs2 in
571    match destr with
572    [ None ⇒ None ?
573    | Some destr ⇒
574      match srcr1 with
575      [ None ⇒ None ?
576      | Some srcr1 ⇒
577        match srcr2 with
578        [ None ⇒ None ?
579        | Some srcr2 ⇒
580          adds_graph [
581            rtl_st_opaccs Modu destr srcr1 srcr2 start_lbl
582          ] start_lbl dest_lbl def
583        ]
584      ]
585    ]
586  | op_mod ⇒ None ? (* signed mod not supported *)
587  | op_and ⇒
588    let destr ≝ extract_singleton ? destrs in
589    let srcr1 ≝ extract_singleton ? srcrs1 in
590    let srcr2 ≝ extract_singleton ? srcrs2 in
591    match destr with
592    [ None ⇒ None ?
593    | Some destr ⇒
594      match srcr1 with
595      [ None ⇒ None ?
596      | Some srcr1 ⇒
597        match srcr2 with
598        [ None ⇒ None ?
599        | Some srcr2 ⇒
600          adds_graph [
601            rtl_st_op2 And destr srcr1 srcr2 start_lbl
602          ] start_lbl dest_lbl def
603        ]
604      ]
605    ]
606  | op_or ⇒
607    let destr ≝ extract_singleton ? destrs in
608    let srcr1 ≝ extract_singleton ? srcrs1 in
609    let srcr2 ≝ extract_singleton ? srcrs2 in
610    match destr with
611    [ None ⇒ None ?
612    | Some destr ⇒
613      match srcr1 with
614      [ None ⇒ None ?
615      | Some srcr1 ⇒
616        match srcr2 with
617        [ None ⇒ None ?
618        | Some srcr2 ⇒
619          adds_graph [
620            rtl_st_op2 Or destr srcr1 srcr2 start_lbl
621          ] start_lbl dest_lbl def
622        ]
623      ]
624    ]
625  | op_xor ⇒
626    let destr ≝ extract_singleton ? destrs in
627    let srcr1 ≝ extract_singleton ? srcrs1 in
628    let srcr2 ≝ extract_singleton ? srcrs2 in
629    match destr with
630    [ None ⇒ None ?
631    | Some destr ⇒
632      match srcr1 with
633      [ None ⇒ None ?
634      | Some srcr1 ⇒
635        match srcr2 with
636        [ None ⇒ None ?
637        | Some srcr2 ⇒
638          adds_graph [
639            rtl_st_op2 Xor destr srcr1 srcr2 start_lbl
640          ] start_lbl dest_lbl def
641        ]
642      ]
643    ]
644  | op_shru ⇒ None ? (* shifts not supported *)
645  | op_shr ⇒ None ?
646  | op_shl ⇒ None ?
647  | op_addf ⇒ None ? (* floats not supported *)
648  | op_subf ⇒ None ?
649  | op_mulf ⇒ None ?
650  | op_divf ⇒ None ?
651  | op_cmpf _ ⇒ None ?
652  | op_addp ⇒
653    let destr12 ≝ extract_pair ? destrs in
654    match destr12 with
655    [ None         ⇒ None ?
656    | Some destr12 ⇒
657      let 〈destr1, destr2〉 ≝ destr12 in
658      let srcr12 ≝ extract_pair ? srcrs1 in
659      match srcr12 with
660      [ None ⇒
661        let srcr2 ≝ extract_singleton ? srcrs1 in
662        match srcr2 with
663        [ None ⇒ None ?
664        | Some srcr2 ⇒
665          let srcr12 ≝ extract_pair ? srcrs2 in
666          match srcr12 with
667          [ None ⇒ None ?
668          | Some srcr12 ⇒
669            let 〈srcr11, srcr12〉 ≝ srcr12 in
670            let 〈def, tmpr1〉 ≝ fresh_reg def in
671            let 〈def, tmpr2〉 ≝ fresh_reg def in
672              adds_graph [
673                rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
674                rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
675                rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
676                rtl_st_move destr1 tmpr1 start_lbl
677              ] start_lbl dest_lbl def
678          ]
679        ]
680      | Some srcr12 ⇒
681        let 〈srcr11, srcr12〉 ≝ srcr12 in
682        let srcr2 ≝ extract_singleton ? srcrs2 in
683        match srcr2 with
684        [ None       ⇒ None ?
685        | Some srcr2 ⇒
686          let 〈def, tmpr1〉 ≝ fresh_reg def in
687          let 〈def, tmpr2〉 ≝ fresh_reg def in
688            adds_graph [
689              rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
690              rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
691              rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
692              rtl_st_move destr1 tmpr1 start_lbl
693            ] start_lbl dest_lbl def
694        ]
695      ]
696    ]
697  | op_subp ⇒
698    let destr ≝ extract_singleton ? destrs in
699    match destr with
700    [ None ⇒
701      let destr12 ≝ extract_pair ? destrs in
702      match destr12 with
703      [ None ⇒ None ?
704      | Some destr12 ⇒
705        let 〈destr1, destr2〉 ≝ destr12 in
706        let srcr12 ≝ extract_pair ? srcrs1 in
707        match srcr12 with
708        [ None ⇒ None ?
709        | Some srcr12 ⇒
710          let 〈srcr11, srcr12〉 ≝ srcr12 in
711          let srcr2 ≝ extract_singleton ? srcrs2 in
712          match srcr2 with
713          [ None ⇒ None ?
714          | Some srcr2 ⇒
715            adds_graph [
716              rtl_st_clear_carry start_lbl;
717              rtl_st_op2 Sub destr1 srcr11 srcr2 start_lbl;
718              rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl;
719              rtl_st_op2 Sub destr2 srcr12 destr2 start_lbl
720            ] start_lbl dest_lbl def
721          ]
722        ]
723      ]
724    | Some destr ⇒
725      match srcrs1 with
726      [ nil ⇒ None ?
727      | cons srcr1 tl ⇒
728        match srcrs2 with
729        [ nil ⇒ None ?
730        | cons srcr2 tl' ⇒
731          let 〈def, tmpr1〉 ≝ fresh_reg def in
732          let 〈def, tmpr2〉 ≝ fresh_reg def in
733            adds_graph [
734              rtl_st_op1 Cmpl tmpr1 srcr2 start_lbl;
735              rtl_st_int tmpr2 (bitvector_of_nat ? 1) start_lbl;
736              rtl_st_op2 Add tmpr1 tmpr1 tmpr2 start_lbl;
737              rtl_st_op2 Add destr srcr1 tmpr1 start_lbl
738            ] start_lbl dest_lbl def
739        ]
740      ]
741    ]
742  | op_cmp cmp ⇒
743    match cmp with
744    [ Compare_Equal ⇒
745      add_translates [
746        translate_op2 op_sub destrs srcrs1 srcrs2;
747        translate_op1 op_not_bool destrs destrs
748      ] start_lbl dest_lbl def
749    | Compare_NotEqual ⇒
750      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
751    | _ ⇒ None ?
752    ]
753  | op_cmpu cmp ⇒
754    match cmp with
755    [ Compare_Equal ⇒
756      add_translates [
757        translate_op2 op_sub destrs srcrs1 srcrs2;
758        translate_op1 op_not_bool destrs destrs
759      ] start_lbl dest_lbl def
760    | Compare_NotEqual ⇒
761      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
762    | Compare
763    | _ ⇒ None ?
764    ]
765  | _ ⇒ ?
766  ].
767
768    | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
769      let (def, tmpr) = fresh_reg def in
770      adds_graph
771        [RTL.St_clear_carry start_lbl ;
772         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
773         RTL.St_int (destr, 0, start_lbl) ;
774         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
775        start_lbl dest_lbl def
776
777    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
778      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
779        destrs srcrs2 srcrs1 start_lbl dest_lbl def
780
781    | AST.Op_cmpu AST.Cmp_le, _, _, _ ->
782      add_translates
783        [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ;
784         translate_op1 AST.Op_notbool destrs destrs]
785        start_lbl dest_lbl def
786
787    | AST.Op_cmpu AST.Cmp_ge, _, _, _ ->
788      add_translates
789        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
790         translate_op1 AST.Op_notbool destrs destrs]
791        start_lbl dest_lbl def
792
793    | AST.Op_cmp cmp, _, _, _ ->
794      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
795      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
796      add_translates
797        [translate_cst (AST.Cst_int 128) tmprs1 ;
798         translate_cst (AST.Cst_int 128) tmprs2 ;
799         translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ;
800         translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ;
801         translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2]
802        start_lbl dest_lbl def
803
804    | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
805      let (def, tmpr) = fresh_reg def in
806      add_translates
807        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ;
808         translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ;
809         translate_op2 AST.Op_or [destr] [destr] [tmpr] ;
810         adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ;
811         translate_op2 AST.Op_xor [destr] [destr] [tmpr]]
812        start_lbl dest_lbl def
813
814    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
815      let (def, tmpr1) = fresh_reg def in
816      let (def, tmpr2) = fresh_reg def in
817      add_translates
818        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
819         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
820         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
821         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
822         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
823        start_lbl dest_lbl def
824
825    | AST.Op_cmpp AST.Cmp_gt, _, _, _ ->
826      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
827        destrs srcrs2 srcrs1 start_lbl dest_lbl def
828
829    | AST.Op_cmpp AST.Cmp_le, _, _, _ ->
830      add_translates
831        [translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ;
832         translate_op1 AST.Op_notbool destrs destrs]
833        start_lbl dest_lbl def
834
835    | AST.Op_cmpp AST.Cmp_ge, _, _, _ ->
836      add_translates
837        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
838         translate_op1 AST.Op_notbool destrs destrs]
839        start_lbl dest_lbl def
840
841    | _ -> assert false (* wrong number of arguments *)
842*)
843
844definition translate_condcst ≝
845  λcst.
846  λstart_lbl: label.
847  λlbl_true: label.
848  λlbl_false: label.
849  λdef.
850  match cst with
851  [ cast_int i ⇒
852    let 〈def, tmpr〉 ≝ fresh_reg def in
853    adds_graph [
854      rtl_st_int tmpr i start_lbl;
855      rtl_st_cond_acc tmpr lbl_true lbl_false
856    ] start_lbl start_lbl def
857  | cast_addr_symbol x ⇒
858    let 〈def, r1〉 ≝ fresh_reg def in
859    let 〈def, r2〉 ≝ fresh_reg def in
860    let lbl ≝ fresh_label def in
861    match lbl with
862    [ None ⇒ None ?
863    | Some lbl ⇒
864      let def ≝ add_graph start_lbl (rtl_st_addr r1 r2 x lbl) def in
865        translate_condptr r1 r2 lbl lbl_true lbl_false def
866    ]
867  | cast_stack_offset off ⇒
868    let 〈def, r1〉 ≝ fresh_reg def in
869    let 〈def, r2〉 ≝ fresh_reg def in
870    let tmp_lbl ≝ fresh_label def in
871    match tmp_lbl with
872    [ None ⇒ None ?
873    | Some tmp_lbl ⇒
874      let def ≝ translate_cst (cast_stack_offset off) [r1; r2] start_lbl tmp_lbl def in
875      match def with
876      [ None ⇒ None ?
877      | Some def ⇒ translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def
878      ]
879    ]
880  | cast_float f ⇒ None ? (* error_float *)
881  ].
882
883definition size_of_op1_ret ≝
884  λop.
885  match op with
886  [ op_cast8_unsigned ⇒ Some ? 1
887  | op_cast8_signed ⇒ Some ? 1
888  | op_cast16_unsigned ⇒ Some ? 1
889  | op_cast16_signed ⇒ Some ? 1
890  | op_neg_int ⇒ Some ? 1
891  | op_not_int ⇒ Some ? 1
892  | op_int_of_ptr ⇒ Some ? 1
893  | op_ptr_of_int ⇒ Some ? 2
894  | op_id ⇒ None ? (* invalid_argument *)
895  | _ ⇒ None ? (* error_float *)
896  ].
897
898definition translate_cond1 ≝
899  λop1.
900  λsrcrs: list register.
901  λstart_lbl: label.
902  λlbl_true: label.
903  λlbl_false: label.
904  λdef.
905  match op1 with
906  [ op_id ⇒
907    let srcr ≝ extract_singleton ? srcrs in
908    match srcr with
909    [ None ⇒
910      let srcr12 ≝ extract_pair ? srcrs in
911      match srcr12 with
912      [ None ⇒ None ?
913      | Some srcr12 ⇒
914        let 〈srcr1, srcr2〉 ≝ srcr12 in
915          translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def
916      ]
917    | Some srcr ⇒
918      adds_graph [
919        rtl_st_cond_acc srcr lbl_true lbl_false
920      ] start_lbl start_lbl def
921    ]
922  | _     ⇒
923    let size ≝ size_of_op1_ret op1 in
924    match size with
925    [ None ⇒ None ?
926    | Some size ⇒
927      let 〈def, destrs〉 ≝ fresh_regs def size in
928      let lbl ≝ fresh_label def in
929      match lbl with
930      [ None ⇒ None ?
931      | Some lbl ⇒
932        let def ≝ translate_op1 op1 destrs srcrs start_lbl lbl def in
933        match def with
934        [ None ⇒ None ?
935        | Some def ⇒
936          let destr ≝ extract_singleton ? destrs in
937          match destr with
938          [ None ⇒
939            let destr12 ≝ extract_pair ? destrs in
940            match destr12 with
941            [ None ⇒ None ?
942            | Some destr12 ⇒
943              let 〈destr1, destr2〉 ≝ destr12 in
944                translate_condptr destr1 destr2 start_lbl lbl_true lbl_false def
945            ]
946          | Some destr ⇒
947            adds_graph [
948              rtl_st_cond_acc destr lbl_true lbl_false
949            ] start_lbl start_lbl def
950          ]
951        ]
952      ]
953    ]
954  ].
955
956definition size_of_op2_ret ≝
957  λn: nat.
958  λop2.
959  match op2 with
960  [ op_add ⇒ Some ? 1
961  | op_sub ⇒ Some ? 1
962  | op_mul ⇒ Some ? 1
963  | op_div ⇒ Some ? 1
964  | op_divu ⇒ Some ? 1
965  | op_mod ⇒ Some ? 1
966  | op_modu ⇒ Some ? 1
967  | op_and ⇒ Some ? 1
968  | op_or ⇒ Some ? 1
969  | op_xor ⇒ Some ? 1
970  | op_shl ⇒ Some ? 1
971  | op_shr ⇒ Some ? 1
972  | op_shru ⇒ Some ? 1
973  | op_cmp _ ⇒ Some ? 1
974  | op_cmpu _ ⇒ Some ? 1
975  | op_cmpp _ ⇒ Some ? 1
976  | op_addp ⇒ Some ? 2
977  | op_subp ⇒
978    if eq_nat n 4 then
979      Some ? 1
980    else
981      Some ? 2
982  | _ ⇒ None ? (* error_float *)
983  ].
984
985axiom translate_op2:
986  op2 → list register → list register → list register → label → label → rtl_internal_function → option rtl_internal_function.
987
988definition translate_cond2 ≝
989  λop2.
990  λsrcrs1: list register.
991  λsrcrs2: list register.
992  λstart_lbl: label.
993  λlbl_true: label.
994  λlbl_false: label.
995  λdef.
996  match op2 with
997  [ op_cmp cmp ⇒
998    match cmp with
999    [ Compare_Equal ⇒
1000      let srcr1 ≝ extract_singleton ? srcrs1 in
1001      match srcr1 with
1002      [ None ⇒ None ?
1003      | Some srcr1 ⇒
1004        let srcr2 ≝ extract_singleton ? srcrs2 in
1005        match srcr2 with
1006        [ None ⇒ None ?
1007        | Some srcr2 ⇒
1008          let 〈def, tmpr〉 ≝ fresh_reg def in
1009          adds_graph [
1010            rtl_st_clear_carry start_lbl;
1011            rtl_st_op2 Sub tmpr srcr1 srcr2 start_lbl;
1012            rtl_st_cond_acc tmpr lbl_false lbl_true
1013          ] start_lbl start_lbl def
1014        ]
1015      ]
1016    | _ ⇒
1017      let n ≝ length ? srcrs1 + length ? srcrs2 in
1018      match size_of_op2_ret n op2 with
1019      [ None ⇒ None ?
1020      | Some size ⇒
1021        let 〈def, destrs〉 ≝ fresh_regs def size in
1022        let lbl ≝ fresh_label def in
1023        match lbl with
1024        [ None ⇒ None ?
1025        | Some lbl ⇒
1026          match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
1027          [ None ⇒ None ?
1028          | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
1029          ]
1030        ]
1031      ]
1032    ]
1033  | _ ⇒
1034    let n ≝ length ? srcrs1 + length ? srcrs2 in
1035    match size_of_op2_ret n op2 with
1036    [ None ⇒ None ?
1037    | Some size ⇒
1038      let 〈def, destrs〉 ≝ fresh_regs def size in
1039      let lbl ≝ fresh_label def in
1040      match lbl with
1041      [ None ⇒ None ?
1042      | Some lbl ⇒
1043        match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
1044        [ None ⇒ None ?
1045        | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
1046        ]
1047      ]
1048    ]
1049  ].
1050
1051let rec addressing_pointer (mode: ?) (args: ?) (destr1: ?)
1052                           (destr2: ?) (start_lbl: label)
1053                           (dest_lbl: label) (def: rtl_internal_function) ≝
1054  let destrs ≝ [ destr1; destr2 ] in
1055  match mode with
1056  [ Aindexed off ⇒
1057    let srcr12 ≝ extract_singleton ? args in
1058    match srcr12 with
1059    [ None ⇒ None ?
1060    | Some srcr12 ⇒
1061      let srcr12 ≝ extract_pair ? srcr12 in
1062      match srcr12 with
1063      [ None ⇒ None ?
1064      | Some srcr12 ⇒
1065        let 〈srcr1, srcr2〉 ≝ srcr12 in
1066        let 〈def, tmpr〉 ≝ fresh_reg def in
1067        add_translates [
1068          adds_graph [
1069            rtl_st_int tmpr off start_lbl
1070          ];
1071          translate_op2 op_addp destrs [ srcr1 ; srcr2 ] [tmpr]
1072        ] start_lbl dest_lbl def
1073      ]
1074    ]
1075  | Aindexed2 ⇒
1076    let args_pair ≝ extract_pair ? args in
1077    match args_pair with
1078    [ None ⇒ None ?
1079    | Some args_pair ⇒
1080      let 〈lft, rgt〉 ≝ args_pair in
1081      let srcr1112 ≝ extract_pair ? lft in
1082      let srcr2 ≝ extract_singleton ? rgt in
1083      match srcr1112 with
1084      [ None ⇒
1085        let srcr2 ≝ extract_singleton ? rgt in
1086        let srcr1112 ≝ extract_pair ? lft in
1087        match srcr2 with
1088        [ None ⇒ None ?
1089        | Some srcr2 ⇒
1090          match srcr1112 with
1091          [ None ⇒ None ?
1092          | Some srcr1112 ⇒
1093            let 〈srcr11, srcr12〉 ≝ srcr1112 in
1094            translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
1095          ]
1096        ]
1097      | Some srcr1112 ⇒
1098        let 〈srcr11, srcr12〉 ≝ srcr1112 in
1099        match srcr2 with
1100        [ None ⇒ None ?
1101        | Some srcr2 ⇒
1102          translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
1103        ]
1104      ]
1105    ]
1106  | Aglobal x off ⇒
1107    let 〈def, tmpr〉 ≝ fresh_reg def in
1108    add_translates [
1109      adds_graph [
1110        rtl_st_int tmpr off start_lbl;
1111        rtl_st_addr destr1 destr2 x start_lbl
1112      ];
1113      translate_op2 op_addp destrs destrs [ tmpr ]
1114    ] start_lbl dest_lbl def
1115  | Abased x off ⇒
1116    let srcrs ≝ extract_singleton ? args in
1117    match srcrs with
1118    [ None ⇒ None ?
1119    | Some srcrs ⇒
1120      let 〈def, tmpr1〉 ≝ fresh_reg def in
1121      let 〈def, tmpr2〉 ≝ fresh_reg def in
1122      (* mode, args, destr1, destr2, start_lbl, dest_lbl, def *)
1123      (* addressing_pointer (Aglobal x off) [ ] tmpr1 tmpr2; *)
1124      let address_unfold ≝
1125        let 〈def, tmpr〉 ≝ fresh_reg def in
1126          add_translates [
1127            adds_graph [
1128              rtl_st_int tmpr off start_lbl;
1129              rtl_st_addr tmpr1 tmpr2 x start_lbl
1130           ];
1131            translate_op2 op_addp destrs destrs [ tmpr ]
1132         ]
1133      in
1134      add_translates [
1135        address_unfold;
1136        translate_op2 op_addp destrs [ tmpr1; tmpr2 ] srcrs
1137      ] start_lbl dest_lbl def
1138    ]
1139  | Ainstack off ⇒
1140    let 〈def, tmpr〉 ≝ fresh_reg def in
1141    add_translates [
1142      adds_graph [
1143        rtl_st_int tmpr off start_lbl;
1144        rtl_st_stack_addr destr1 destr2 start_lbl
1145      ];
1146      translate_op2 op_addp destrs destrs [ tmpr ]
1147    ] start_lbl dest_lbl def
1148  | _ ⇒ None ? (* wrong number of arguments *)
1149  ].
1150
1151definition translate_load ≝
1152  λq.
1153  λmode.
1154  λargs.
1155  λdestrs.
1156  λstart_lbl: label.
1157  λdest_lbl: label.
1158  λdef.
1159  match q with
1160  [ q_int b ⇒
1161    if eq_bv ? b (bitvector_of_nat ? 1) then
1162      match extract_singleton ? destrs with
1163      [ None ⇒ None ? (* error: size error in load *)
1164      | Some destr ⇒
1165        let 〈def, addr1〉 ≝ fresh_reg def in
1166        let 〈def, addr2〉 ≝ fresh_reg def in
1167          Some ? (add_translates [
1168            addressing_pointer mode args addr1 addr2;
1169            adds_graph [
1170              rtl_st_load destr addr1 addr2 start_lbl
1171            ]
1172          ] start_lbl dest_lbl def)
1173      ]
1174    else
1175      None ? (* error: size error in load *)
1176  | q_ptr ⇒
1177    match extract_pair ? destrs with
1178    [ None ⇒ None ? (* error: size error in load *)
1179    | Some destr12 ⇒
1180      let 〈destr1, destr2〉 ≝ destr12 in
1181      let 〈def, addr1〉 ≝ fresh_reg def in
1182      let 〈def, addr2〉 ≝ fresh_reg def in
1183      let addr ≝ [ addr1; addr2 ] in
1184      let 〈def, tmpr〉 ≝ fresh_reg def in
1185        Some ? (
1186          add_translates [
1187            addressing_pointer mode args addr1 addr2;
1188            adds_graph [
1189              rtl_st_load destr1 addr1 addr2 start_lbl;
1190              rtl_st_int tmpr (bitvector_of_nat ? 1) start_lbl
1191            ];
1192            translate_op2 op_addp addr addr [ tmpr ];
1193            adds_graph [
1194              rtl_st_load destr2 addr1 addr2 start_lbl
1195            ]
1196          ] start_lbl dest_lbl def
1197        )
1198    ]
1199  | _ ⇒ None ? (* error: size error in load *)
1200  ].
1201 
1202definition make_addr ≝
1203  λA: Type[0].
1204  λlst: list A.
1205  match lst with
1206  [ cons hd tl ⇒
1207    match tl with
1208    [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
1209    | _ ⇒ None ? (* do not use on these arguments *)
1210    ]
1211  | _ ⇒ None ? (* do not use on these arguments *)
1212  ].
1213 
1214definition translate_store_internal ≝
1215  λaddr.
1216  λtmp_addr.
1217  λtmpr.
1218  λstart_lbl.
1219  λdest_lbl.
1220  λtmp_addr1.
1221  λtmp_addr2.
1222  λtranslates_off.
1223  λsrcr.
1224    let 〈translates, off〉 ≝ translates_off in
1225    let translates ≝ translates @
1226      [ adds_graph [
1227          rtl_st_int tmpr off start_lbl
1228        ];
1229        translate_op2 op_addp tmp_addr addr [ tmpr ];
1230        adds_graph [
1231          rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
1232        ]
1233      ]
1234    in
1235    let 〈ignore, result〉 ≝ half_add ? off int_size in
1236      〈translates, result〉.
1237 
1238definition translate_store ≝
1239  λaddr.
1240  λsrcrs.
1241  λstart_lbl.
1242  λdest_lbl.
1243  λdef.
1244    let 〈def, tmp_addr〉 ≝ fresh_regs def (length ? addr) in
1245    match make_addr ? tmp_addr with
1246    [ None ⇒ None ?
1247    | Some tmp_addr12 ⇒
1248      let 〈tmp_addr1, tmp_addr2〉 ≝ tmp_addr12 in
1249      let 〈def, tmpr〉 ≝ fresh_reg def in
1250      let f ≝ translate_store_internal addr tmp_addr tmpr start_lbl dest_lbl tmp_addr1 tmp_addr2 in
1251      let 〈translates, ignore〉 ≝ foldl ? ? f 〈[], zero ?〉 srcrs in
1252        add_translates translates start_lbl dest_lbl def
1253    ].
1254
1255definition translate_stmt ≝
1256  λlenv.
1257  λlbl.
1258  λstmt.
1259  λdef.
1260  match stmt with
1261  [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
1262  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
1263  | St_cast destr cst lbl' ⇒
1264      translate_cst cst (find_local_env destr lenv) lbl lbl' def
1265  | _ ⇒ ?
1266  ].
1267
1268let translate_stmt lenv lbl stmt def = match stmt with
1269
1270  | RTLabs.St_skip lbl' ->
1271    add_graph lbl (RTL.St_skip lbl') def
1272
1273  | RTLabs.St_cost (cost_lbl, lbl') ->
1274    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
1275
1276  | RTLabs.St_cst (destr, cst, lbl') ->
1277    translate_cst cst (find_local_env destr lenv) lbl lbl' def
1278
1279  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
1280    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
1281      lbl lbl' def
1282
1283  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
1284    translate_op2 op2 (find_local_env destr lenv)
1285      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
1286
1287  | RTLabs.St_load (_, addr, destr, lbl') ->
1288    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
1289      lbl lbl' def
1290
1291  | RTLabs.St_store (_, addr, srcr, lbl') ->
1292    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
1293      lbl lbl' def
1294
1295  | RTLabs.St_call_id (f, args, None, _, lbl') ->
1296    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
1297
1298  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
1299    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
1300                                   find_local_env retr lenv, lbl')) def
1301
1302  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
1303    let (f1, f2) = find_and_addr f lenv in
1304    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
1305
1306  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
1307    let (f1, f2) = find_and_addr f lenv in
1308    add_graph lbl
1309      (RTL.St_call_ptr
1310         (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
1311
1312  | RTLabs.St_tailcall_id (f, args, _) ->
1313    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
1314
1315  | RTLabs.St_tailcall_ptr (f, args, _) ->
1316    let (f1, f2) = find_and_addr f lenv in
1317    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
1318
1319  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
1320    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
1321
1322  | RTLabs.St_jumptable _ ->
1323    error "Jump tables not supported yet."
1324
1325  | RTLabs.St_return None ->
1326    add_graph lbl (RTL.St_return []) def
1327
1328  | RTLabs.St_return (Some r) ->
1329    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
Note: See TracBrowser for help on using the repository browser.