source: src/RTLabs/RTLAbstoRTL.ma @ 1047

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

more work from today

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