source: src/RTLabs/RTLAbstoRTL.ma @ 1050

Last change on this file since 1050 was 1050, checked in by mulligan, 10 years ago

adding dependent types to map datastructure to remove all option types. some changes to rtlabs to rtl translation pass.

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