source: src/RTLabs/RTLAbstoRTL.ma @ 1053

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

changes

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