source: src/RTLabs/RTLAbstoRTL.ma @ 1052

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

removed offsets after reading cerco mailing list

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