source: src/RTLabs/RTLAbstoRTL.ma @ 1050

Last change on this file since 1050 was 1050, checked in by mulligan, 9 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.