source: src/RTLabs/RTLAbstoRTL.ma @ 1057

Last change on this file since 1057 was 1057, checked in by mulligan, 9 years ago

changes from today

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