source: src/RTLabs/RTLAbstoRTL.ma @ 1062

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

separated jmeq and coercions from foldstuff.ma in order to fix the ongoing mess in util.ma surrounding reduce_strong

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