source: src/RTLabs/RTLAbstoRTL.ma @ 1059

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

work from today, bit of a mess at the moment

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