source: src/RTLabs/RTLAbstoRTL.ma @ 1066

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

changes from today

File size: 72.3 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
75axiom fresh_regs_length:
76  ∀def: rtl_internal_function.
77  ∀n: nat.
78    |(\snd (fresh_regs def n))| = n.
79   
80definition addr_regs ≝
81  λregs.
82  match regs with
83  [ cons hd tl ⇒
84    match tl with
85    [ cons hd' tl' ⇒ Some (register × register) 〈hd, hd'〉
86    | nil          ⇒ None (register × register)
87    ]
88  | nil ⇒ None (register × register) (* registers are not an address *)
89  ].
90
91let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
92  match n with
93  [ O ⇒ [ ]
94  | S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n')
95  ].
96
97definition choose_rest ≝
98  λA: Type[0].
99  λleft, right: list A.
100  λprfl: 0 < |left|.
101  λprfr: 0 < |right|.
102  match left return λx. 0 < |x| → list A with
103  [ nil ⇒ λnil_prf.
104    match right return λx. 0 < |x| → list A with
105    [ nil ⇒ λnil_nil_absrd. ?
106    | _ ⇒ λnil_cons_prf. right
107    ] prfr
108  | _ ⇒ λcons_prf. right
109  ] prfl.
110  normalize in nil_prf;
111  cases(not_le_Sn_O 0)
112  #HYP
113  cases(HYP nil_prf)
114qed.
115
116definition complete_regs ≝
117  λdef.
118  λsrcrs1.
119  λsrcrs2.
120  let nb_added ≝ abs ((length ? srcrs1) - (length ? srcrs2)) in
121  let 〈def, added_regs〉 ≝ fresh_regs def nb_added in
122    if gtb nb_added 0 then
123      〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
124    else
125      〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
126
127(* obvious, but proof doesn't look easy! *)
128axiom complete_regs_length:
129  ∀def.
130  ∀left.
131  ∀right.
132    |\fst (\fst (complete_regs def left right))| = |\snd (\fst (complete_regs def left right))|.
133
134definition size_of_sig_type ≝
135  λsig.
136  match sig with
137  [ ASTint isize sign ⇒
138    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
139      isize' ÷ (nat_of_bitvector ? int_size)
140  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
141  | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
142  ].
143  cases not_implemented;
144qed.
145
146inductive register_type: Type[0] ≝
147  | register_int: register → register_type
148  | register_ptr: register → register → register_type.
149
150definition local_env ≝ BitVectorTrie (list register).
151
152definition mem_local_env ≝
153  λr: register.
154  match r with
155  [ an_identifier w ⇒ member (list register) 16 w
156  ].
157
158definition add_local_env ≝
159  λr: register.
160  match r with
161  [ an_identifier w ⇒ insert (list register) 16 w
162  ].
163
164definition find_local_env ≝
165  λr: register.
166  λbvt.
167  match r with
168  [ an_identifier w ⇒ lookup (list register) 16 w bvt [ ]
169  ].
170
171definition initialize_local_env_internal ≝
172  λruniverse.
173  λlenv.
174  λr_sig.
175  let 〈r, sig〉 ≝ r_sig in
176  let size ≝ size_of_sig_type sig in
177  let rs ≝ register_freshes runiverse size in
178    add_local_env r rs lenv.
179
180definition initialize_local_env ≝
181  λruniverse.
182  λregisters.
183  λresult.
184  let registers ≝ registers @
185    match result with
186    [ None ⇒ [ ]
187    | Some rt ⇒ [ rt ]
188    ]
189  in
190    foldl ? ? (initialize_local_env_internal runiverse) (Stub …) registers.
191 
192definition map_list_local_env_internal ≝
193  λlenv.
194  λres.
195  λr.
196    res @ (find_local_env r lenv).
197   
198definition map_list_local_env ≝
199  λlenv.
200  λregs.
201    foldl ? ? (map_list_local_env_internal lenv) [ ] regs.
202
203definition make_addr ≝
204  λA.
205  λlst: list A.
206  λprf: 2 ≤ length A lst.
207  match lst return λx. 2 ≤ |x| → A × A with
208  [ nil ⇒ λlst_nil_prf. ?
209  | cons hd tl ⇒ λprf.
210    match tl return λx. 1 ≤ |x| → A × A with
211    [ nil ⇒ λtl_nil_prf. ?
212    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
213    ] ?
214  ] prf.
215  [1: normalize in lst_nil_prf;
216      cases(not_le_Sn_O 1);
217      #HYP cases(HYP lst_nil_prf)
218  |2: normalize in prf;
219      @le_S_S_to_le
220      assumption
221  |3: normalize in tl_nil_prf;
222      cases(not_le_Sn_O 0)
223      #HYP cases(HYP tl_nil_prf)
224  ]
225qed.
226
227definition find_and_addr ≝
228  λr.
229  λlenv.
230    make_addr ? (find_local_env r lenv).
231
232definition rtl_args ≝
233  λregs_list.
234  λlenv.
235    flatten ? (map ? ? (
236      λr. find_local_env r lenv) regs_list).
237
238definition change_label ≝
239  λlbl.
240  λstmt: rtl_statement.
241  match stmt with
242  [ rtl_st_skip _ ⇒ rtl_st_skip lbl
243  | rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl
244  | rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl
245  | rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl
246  | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
247  | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
248  | rtl_st_opaccs opaccs d s1 s2 s3 _ ⇒ rtl_st_opaccs opaccs d s1 s2 s3 lbl
249  | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
250  | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
251  | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl
252  | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl
253  | rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl
254  | rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl
255  | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a
256  | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
257  | rtl_st_cond r l1 l2 ⇒ rtl_st_cond r l1 l2
258  | rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl
259  | rtl_st_set_carry l ⇒ rtl_st_set_carry lbl
260  | rtl_st_return r ⇒ rtl_st_return r
261  ].
262
263(* Ack! Should generating a fresh label ever fail?  This seems to be a side-effect
264   of implementing everything as a bitvector, which is bounded.  If we implemented
265   labels as unbounded nats then this function will never fail.
266*)
267(* Fixed with changes to label generation.
268*)
269let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝
270  match stmt_list with
271  [ nil ⇒ def
272  | cons hd tl ⇒
273    match tl with
274    [ nil ⇒ add_graph start_lbl (change_label dest_lbl hd) def
275    | cons hd' tl' ⇒
276      let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
277      let stmt ≝ change_label tmp_lbl hd in
278      let def ≝ add_graph start_lbl stmt new_def in
279        adds_graph tl tmp_lbl dest_lbl new_def
280    ]
281  ].
282
283let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
284                       (def: ?) on translate_list ≝
285  match translate_list with
286  [ nil ⇒ def
287  | cons hd tl ⇒
288    match tl with
289    [ nil ⇒ hd start_lbl dest_lbl def
290    | cons hd' tl' ⇒
291      let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
292      let applied ≝ hd start_lbl tmp_lbl new_def in
293        add_translates tl tmp_lbl dest_lbl applied
294    ]
295  ].
296
297definition translate_cst_int_internal ≝
298  λdest_lbl.
299  λr.
300  λi.
301    rtl_st_int r i dest_lbl.
302
303axiom translate_cst:
304  ∀cst: constant.
305  ∀destrs: list register.
306  ∀start_lbl: label.
307  ∀dest_lbl: label.
308  ∀def: rtl_internal_function.
309    rtl_internal_function.
310
311definition translate_move_internal ≝
312  λstart_lbl: label.
313  λdestr: register.
314  λsrcr: register.
315    rtl_st_move destr srcr start_lbl.
316
317definition translate_move ≝
318  λdestrs: list register.
319  λsrcrs: list register.
320  λstart_lbl: label.
321    match reduce_strong register destrs srcrs with
322    [ dp crl_crr len_proof ⇒
323      let commonl ≝ \fst (\fst crl_crr) in
324      let commonr ≝ \fst (\snd crl_crr) in
325      let restl ≝ \snd (\fst crl_crr) in
326      let restr ≝ \snd (\snd crl_crr) in
327      let f_common ≝ translate_move_internal start_lbl in
328      let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
329      let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
330        add_translates [ translate1 ; translate2 ] start_lbl
331    ].
332    @len_proof
333qed.
334
335let rec make
336  (A: Type[0]) (elt: A) (n: nat) on n ≝
337  match n with
338  [ O ⇒ [ ]
339  | S n' ⇒ elt :: make A elt n'
340  ].
341 
342lemma make_length:
343  ∀A: Type[0].
344  ∀elt: A.
345  ∀n: nat.
346    n = length ? (make A elt n).
347  #A #ELT #N
348  elim N
349  [ normalize %
350  | #N #IH
351    normalize <IH %
352  ]
353qed.
354
355definition translate_cast_unsigned ≝
356  λdestrs.
357  λstart_lbl.
358  λdest_lbl.
359  λdef.
360  let 〈def, tmp_zero〉 ≝ fresh_reg def in
361  let zeros ≝ make ? tmp_zero (length ? destrs) in
362    add_translates [
363      adds_graph [
364        rtl_st_int tmp_zero (bitvector_of_nat ? 0) start_lbl
365        ];
366      translate_move destrs zeros
367    ] start_lbl dest_lbl def.
368
369definition translate_cast_signed ≝
370  λdestrs.
371  λsrcr.
372  λstart_lbl.
373  λdest_lbl.
374  λdef.
375  let 〈def, tmp_128〉 ≝ fresh_reg def in
376  let 〈def, tmp_255〉 ≝ fresh_reg def in
377  let 〈def, tmpr〉 ≝ fresh_reg def in
378  let 〈def, dummy〉 ≝ fresh_reg def in
379  let insts ≝ [
380    rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl;
381    rtl_st_op2 And tmpr tmp_128 srcr start_lbl;
382    rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl;
383    rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl;
384    rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl
385  ] in
386  let srcrs ≝ make ? tmpr (length ? destrs) in
387    add_translates [
388      adds_graph insts;
389      translate_move destrs srcrs
390    ] start_lbl dest_lbl def.
391
392definition translate_cast ≝
393  λsrc_size.
394  λsrc_sign.
395  λdest_size.
396  λdestrs.
397  λsrcrs.
398  match |srcrs| return λx. |srcrs| = x → ? with
399  [ O ⇒ λzero_prf. adds_graph [ ]
400  | S n' ⇒ λsucc_prf.
401    if ltb dest_size src_size then
402      translate_move destrs srcrs
403    else
404      match reduce_strong ? destrs srcrs with
405      [ dp crl len_proof ⇒
406        let commonl ≝ \fst (\fst crl) in
407        let commonr ≝ \fst (\snd crl) in
408        let restl ≝ \snd (\fst crl) in
409        let restr ≝ \snd (\snd crl) in
410        let insts_common ≝ translate_move commonl commonr in
411        let sign_reg ≝ last_safe ? srcrs ? in
412        let insts_sign ≝
413          match src_sign with
414          [ Unsigned ⇒ translate_cast_unsigned restl
415          | Signed ⇒ translate_cast_signed restl sign_reg
416          ]
417        in
418          add_translates [ insts_common; insts_sign ]
419      ]
420  ] (refl ? (|srcrs|)).
421  >succ_prf //
422qed.
423
424definition translate_negint ≝
425  λdestrs.
426  λsrcrs.
427  λstart_lbl.
428  λdest_lbl.
429  λdef.
430  λprf: | destrs | = | srcrs |. (* assert in caml code *)
431  let 〈def, tmpr〉 ≝ fresh_reg def in
432  let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
433  let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in
434  let insts_init ≝ [
435    rtl_st_set_carry start_lbl;
436    rtl_st_int tmpr (zero ?) start_lbl
437  ] in
438  let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lbl in
439  let insts_add ≝ map … f_add destrs in
440    adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
441
442definition translate_notbool ≝
443  λdestrs.
444  λsrcrs.
445  λstart_lbl.
446  λdest_lbl.
447  λdef.
448  match destrs with
449  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
450  | cons destr destrs ⇒
451    let 〈def, tmpr〉 ≝ fresh_reg def in
452    let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in
453    let save_srcrs ≝ translate_move tmp_srcrs srcrs in
454    let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lbl in
455    let f ≝ λtmp_srcr. [
456      rtl_st_clear_carry start_lbl;
457      rtl_st_int tmpr (zero ?) start_lbl;
458      rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl;
459      rtl_st_int tmpr (zero ?) start_lbl;
460      rtl_st_op2 Addc tmpr tmpr tmpr start_lbl;
461      rtl_st_op2 Xor destr destr tmpr start_lbl
462    ] in
463    let insts ≝ init_destr :: (flatten ? (map … f tmp_srcrs)) in
464    let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in
465      add_translates [
466        save_srcrs; adds_graph insts; epilogue
467      ] start_lbl dest_lbl def
468  ].
469
470(* TODO: examine this properly.  This is a change from the O'caml code due
471   to us dropping the explicit use of a cast destination size field.  We
472   instead infer the size of the cast's destination from the context.  Is
473   this correct?
474*)
475definition translate_op1 ≝
476  λop1: unary_operation.
477  λdestrs: list register.
478  λsrcrs: list register.
479  λprf: |destrs| = |srcrs|.
480  λstart_lbl: label.
481  λdest_lbl: label.
482  λdef: rtl_internal_function.
483  match op1 with
484  [ Ocastint src_sign src_size ⇒
485    let dest_size ≝ |destrs| * 8 in
486    let src_size ≝ bitsize_of_intsize src_size in
487      translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
488  | Onegint ⇒
489      translate_negint destrs srcrs start_lbl dest_lbl def prf
490  | Onotbool ⇒
491      translate_notbool destrs srcrs start_lbl dest_lbl def
492  | Onotint ⇒
493    let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
494    let l ≝ map2 … f destrs srcrs prf in
495      adds_graph l start_lbl dest_lbl def
496  | Optrofint r ⇒
497      translate_move destrs srcrs start_lbl dest_lbl def
498  | Ointofptr r ⇒
499      translate_move destrs srcrs start_lbl dest_lbl def
500  | Oid ⇒
501      translate_move destrs srcrs start_lbl dest_lbl def
502  | _ ⇒ ? (* float operations implemented in runtime *)
503  ].
504  cases not_implemented
505qed.
506 
507definition translate_op ≝
508  λop.
509  λdestrs.
510  λsrcrs1.
511  λsrcrs2.
512  λstart_lbl.
513  λdest_lbl.
514  λdef.
515  match reduce_strong ? srcrs1 srcrs2 with
516  [ dp reduced first_reduced_proof ⇒
517    let srcrsl_common ≝ \fst (\fst reduced) in
518    let srcrsr_common ≝ \fst (\snd reduced) in
519    let srcrsl_rest ≝ \snd (\fst reduced) in
520    let srcrsr_rest ≝ \snd (\snd reduced) in
521    let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ? in
522    match reduce_strong ? destrs srcrsl_common with
523    [ dp reduced second_reduced_proof ⇒
524      let destrs_common ≝ \fst (\fst reduced) in
525      let destrs_rest ≝ \snd (\fst reduced) in
526      match reduce_strong ? destrs_rest srcrs_rest with
527      [ dp reduced third_reduced_proof ⇒
528        let destrs_cted ≝ \fst (\fst reduced) in
529        let destrs_rest ≝ \snd (\fst reduced) in
530        let srcrs_cted ≝ \fst (\snd reduced) in
531        let 〈def, tmpr〉 ≝ fresh_reg def in
532        let insts_init ≝ [
533          rtl_st_clear_carry start_lbl;
534          rtl_st_int tmpr (zero ?) start_lbl
535        ] in
536        let f_add ≝ λdestr. λsrcr1. λsrcr2. rtl_st_op2 op destr srcr1 srcr2 start_lbl in
537        let insts_add ≝ map3 … f_add destrs_common srcrsl_common srcrsr_common ? ? in
538        let f_add_cted ≝ λdestr. λsrcr. rtl_st_op2 op destr srcr tmpr start_lbl in
539        let insts_add_cted ≝ map2 ? ? ? f_add_cted destrs_cted srcrs_cted ? in
540        let f_rest ≝ λdestr. rtl_st_op2 op destr tmpr tmpr start_lbl in
541        let insts_rest ≝ map … f_rest destrs_rest in
542          adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
543      ]
544    ]
545  ].
546  [1: @third_reduced_proof
547  |3: @first_reduced_proof
548  |*: cases daemon (* TODO *)
549  ]
550qed.
551
552let rec translate_mul1
553  (dummy: register) (tmpr: register) (destrs: list register)
554  (srcrs1: list register) (srcr2: register) (start_lbl: label)
555    on srcrs1 ≝
556  match destrs with
557  [ nil ⇒ adds_graph [ rtl_st_skip start_lbl ] start_lbl
558  | cons destr tl ⇒
559    match tl with
560    [ nil ⇒
561      match srcrs1 with
562      [ nil ⇒
563        adds_graph [
564          rtl_st_int tmpr (zero ?) start_lbl;
565          rtl_st_op2 Addc destr destr tmpr start_lbl
566        ] start_lbl
567      | cons srcr1 tl' ⇒
568        adds_graph [
569          rtl_st_opaccs Mul tmpr dummy srcr2 srcr1 start_lbl;
570          rtl_st_op2 Addc destr destr tmpr start_lbl
571        ] start_lbl
572      ]
573    | cons destr2 destrs ⇒
574      match srcrs1 with
575      [ nil ⇒
576        add_translates [
577          adds_graph [
578            rtl_st_int tmpr (zero ?) start_lbl;
579            rtl_st_op2 Addc destr destr tmpr start_lbl;
580            rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
581          ];
582          translate_cst (Ointconst I8 (zero ?)) destrs
583        ] start_lbl
584      | cons srcr1 srcrs1 ⇒
585        match destrs with
586        [ nil ⇒
587          add_translates [
588            adds_graph [
589              rtl_st_int tmpr (zero ?) start_lbl;
590              rtl_st_op2 Addc destr destr tmpr start_lbl;
591              rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
592            ];
593            translate_cst (Ointconst I8 (zero ?)) destrs
594          ] start_lbl
595        | cons destr2 destrs ⇒
596          add_translates [
597            adds_graph [
598              rtl_st_opaccs Mul tmpr destr2 srcr2 srcr1 start_lbl;
599              rtl_st_op2 Addc destr destr tmpr start_lbl
600            ];
601            translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2
602          ] start_lbl
603        ]
604      ]
605    ]
606  ].
607
608definition translate_muli ≝
609  λdummy: register.
610  λtmpr: register.
611  λdestrs: list register.
612  λtmp_destrs: list register.
613  λsrcrs1: list register.
614  λdummy_lbl: label.
615  λi: nat.
616  λi_prf.
617  λtranslates: list ?.
618  λsrcr2i: register.
619  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split ? tmp_destrs i i_prf in
620  let tmp_destrs2' ≝
621    match tmp_destrs2 with
622    [ nil ⇒ [ ]
623    | cons tmp_destr2 tmp_destrs2 ⇒ [
624        adds_graph [
625          rtl_st_clear_carry dummy_lbl;
626          rtl_st_int tmp_destr2 (zero ?) dummy_lbl
627        ];
628        translate_mul1 dummy tmpr tmp_destrs2 srcrs1 srcr2i;
629        translate_cst (Ointconst I8 (zero ?)) tmp_destrs1;
630        adds_graph [
631          rtl_st_clear_carry dummy_lbl
632        ];
633        translate_op Addc destrs destrs tmp_destrs
634      ]
635    ]
636  in
637    translates @ tmp_destrs2'.
638
639axiom translate_mul:
640  ∀destrs: list register.
641  ∀srcrs1: list register.
642  ∀srcrs2: list register.
643  ∀start_lbl: label.
644  ∀dest_lbl: label.
645  ∀def: rtl_internal_function.
646    rtl_internal_function.
647
648(*
649definition translate_mul ≝
650  λdestrs: list register.
651  λsrcrs1: list register.
652  λsrcrs2: list register.
653  λstart_lbl: label.
654  λdest_lbl: label.
655  λdef: rtl_internal_function.
656  let 〈def, dummy〉 ≝ fresh_reg def in
657  let 〈def, tmpr〉 ≝ fresh_reg def in
658  let 〈def, tmp_destrs〉 ≝ fresh_regs def (|destrs|) in
659  let 〈def, fresh_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
660  let 〈def, fresh_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
661  let insts_init ≝ [
662    translate_move fresh_srcrs1 srcrs1;
663    translate_move fresh_srcrs2 srcrs2;
664    translate_cst (Ointconst I8 (zero ?)) destrs
665  ]
666  in
667  let f ≝ λi. translate_muli dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in
668  let insts_mul ≝ foldi ? ? [ ] srcrs2 in ?. [5: check insts_init.
669    add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
670*)
671
672definition translate_divumodu8 ≝
673  λorder: bool.
674  λdestrs: list register.
675  λsrcr1: register.
676  λsrcr2: register.
677  λstart_lbl: label.
678  λdest_lbl: label.
679  λdef: rtl_internal_function.
680  match destrs with
681  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
682  | cons destr destrs ⇒
683    let 〈def, dummy〉 ≝ fresh_reg def in
684    let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉 | _ ⇒ 〈dummy, destr〉 ] in
685    let inst_div ≝ adds_graph [
686      rtl_st_opaccs DivuModu destr1 destr2 srcr1 srcr2 start_lbl
687    ]
688    in
689    let insts_rest ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
690      add_translates [ inst_div; insts_rest ] start_lbl dest_lbl def
691  ].
692
693definition translate_ne: ? → ? → ? → ? → ? → ? → rtl_internal_function ≝
694  λdestrs: list register.
695  λsrcrs1: list register.
696  λsrcrs2: list register.
697  λstart_lbl: label.
698  λdest_lbl: label.
699  λdef: rtl_internal_function.
700  match destrs with
701  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
702  | cons destr destrs ⇒
703    let 〈def, tmpr〉 ≝ fresh_reg def in
704    let 〈def, tmp_zero〉 ≝ fresh_reg def in
705    let 〈def, tmp_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
706    let save_srcrs1 ≝ translate_move tmp_srcrs1 srcrs1 in
707    let 〈def, tmp_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
708    let save_srcrs2 ≝ translate_move tmp_srcrs2 srcrs2 in
709    match reduce_strong ? tmp_srcrs1 tmp_srcrs2 with
710    [ dp crl their_proof ⇒
711      let commonl ≝ \fst (\fst crl) in
712      let commonr ≝ \fst (\snd crl) in
713      let restl ≝ \snd (\snd crl) in
714      let restr ≝ \snd (\snd crl) in
715      let rest ≝ choose_rest ? restl restr ? ? in
716      let inits ≝ [
717        rtl_st_int destr (zero ?) start_lbl;
718        rtl_st_int tmp_zero (zero ?) start_lbl
719      ]
720      in
721      let f_common ≝ λtmp_srcr1. λtmp_srcr2. [
722        rtl_st_clear_carry start_lbl;
723        rtl_st_op2 Sub tmpr tmp_srcr1 tmp_srcr2 start_lbl;
724        rtl_st_op2 Or destr destr tmpr start_lbl
725      ]
726      in
727      let insts_common ≝ flatten ? (map2 … f_common commonl commonr ?) in
728      let f_rest ≝ λtmp_srcr. [
729        rtl_st_clear_carry start_lbl;
730        rtl_st_op2 Sub tmpr tmp_zero tmp_srcr start_lbl;
731        rtl_st_op2 Or destr destr tmpr start_lbl
732      ]
733      in
734      let insts_rest ≝ flatten ? (map ? ? f_rest rest) in
735      let insts ≝ inits @ insts_common @ insts_rest in
736      let epilogue ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
737        add_translates [
738          save_srcrs1; save_srcrs2; adds_graph insts; epilogue
739        ] start_lbl dest_lbl def
740    ]
741  ].
742  [1: @their_proof
743  |*: cases not_implemented (* choose rest requires non-emptiness proofs but
744                               these appear impossible to obtain, similar proof
745                               to above *)
746  ]
747qed.
748
749definition translate_eq_reg ≝
750  λtmp_zero: register.
751  λtmp_one: register.
752  λtmpr1: register.
753  λtmpr2: register.
754  λdestr: register.
755  λdummy_lbl: label.
756  λsrcr12: register × register.
757  let 〈srcr1, srcr2〉 ≝ srcr12 in
758  [ rtl_st_clear_carry dummy_lbl;
759    rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
760    rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
761    rtl_st_op2 Sub tmpr2 srcr2 srcr1 dummy_lbl;
762    rtl_st_op2 Addc tmpr2 tmp_zero tmp_zero dummy_lbl;
763    rtl_st_op2 Or tmpr1 tmpr1 tmpr2 dummy_lbl;
764    rtl_st_op2 Xor tmpr1 tmpr1 tmp_one dummy_lbl;
765    rtl_st_op2 And destr destr tmpr1 dummy_lbl ].
766
767definition translate_eq_list ≝
768  λtmp_zero: register.
769  λtmp_one: register.
770  λtmpr1: register.
771  λtmpr2: register.
772  λdestr: register.
773  λleq: list (register × register).
774  λdummy_lbl: label.
775  let f ≝ translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
776    (rtl_st_int destr (bitvector_of_nat ? 1) dummy_lbl) ::
777      flatten ? (map ? ? f leq).
778
779definition translate_atom ≝
780  λtmp_zero: register.
781  λtmp_one: register.
782  λtmpr1: register.
783  λtmpr2: register.
784  λtmpr3: register.
785  λdestr: register.
786  λdummy_lbl: label.
787  λleq: list (register × register).
788  λsrcr1: register.
789  λsrcr2: register.
790    translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
791    [ rtl_st_clear_carry dummy_lbl;
792      rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
793      rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
794      rtl_st_op2 And tmpr3 tmpr3 tmpr1 dummy_lbl;
795      rtl_st_op2 Or destr destr tmpr3 dummy_lbl ].
796
797definition translate_lt_main ≝
798  λtmp_zero: register.
799  λtmp_one: register.
800  λtmpr1: register.
801  λtmpr2: register.
802  λtmpr3: register.
803  λdestr: register.
804  λdummy_lbl: label.
805  λsrcrs1: list register.
806  λsrcrs2: list register.
807  λproof: |srcrs1| = |srcrs2|.
808  let f ≝ λinsts_leq. λsrcr1. λsrcr2.
809    let 〈insts, leq〉 ≝ insts_leq in
810    let added_insts ≝ translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
811      〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉
812  in
813    \fst (fold_left2 ? ? ? f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).
814
815definition fresh_regs_strong:
816  rtl_internal_function → ∀n: nat. Σfresh: rtl_internal_function × (list register). |\snd fresh| = n ≝
817  λdef.
818  λn.
819    fresh_regs def n.
820  @fresh_regs_length
821qed.
822
823definition complete_regs_strong:
824  rtl_internal_function → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
825  λdef.
826  λleft.
827  λright.
828    complete_regs def left right.
829  @complete_regs_length
830qed.
831
832definition translate_lt ≝
833  λdestrs: list register.
834  λprf_destrs: lt 0 (|destrs|).
835  λsrcrs1: list register.
836  λsrcrs2: list register.
837  λstart_lbl: label.
838  λdest_lbl: label.
839  λdef: rtl_internal_function.
840  match destrs with
841  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
842  | _ ⇒
843    match fresh_regs_strong def (|destrs|) with
844    [ dp def_tmp_destrs tmp_destrs_proof ⇒
845      let def ≝ \fst def_tmp_destrs in
846      let tmp_destrs ≝ \snd def_tmp_destrs in
847      let tmp_destr ≝ hd_safe ? tmp_destrs ? in
848      let 〈def, tmp_zero〉 ≝ fresh_reg def in
849      let 〈def, tmp_one〉 ≝ fresh_reg def in
850      let 〈def, tmpr1〉 ≝ fresh_reg def in
851      let 〈def, tmpr2〉 ≝ fresh_reg def in
852      let 〈def, tmpr3〉 ≝ fresh_reg def in
853      match complete_regs_strong def srcrs1 srcrs2 with
854      [ dp srcrs12_added srcrs12_proof ⇒
855        let srcrs1 ≝ \fst (\fst srcrs12_added) in
856        let srcrs2 ≝ \snd (\fst srcrs12_added) in
857        let added ≝ \snd srcrs12_added in
858        let srcrs1' ≝ rev ? srcrs1 in
859        let srcrs2' ≝ rev ? srcrs2 in
860        let insts_init ≝ [
861          translate_cst (Ointconst I8 (zero ?)) tmp_destrs;
862          translate_cst (Ointconst I8 (zero ?)) added;
863          adds_graph [
864            rtl_st_int tmp_zero (zero ?) start_lbl;
865            rtl_st_int tmp_one (bitvector_of_nat ? 1) start_lbl
866          ]
867        ]
868        in
869        let insts_main ≝
870          translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
871          let insts_main ≝ [ adds_graph insts_main ] in
872          let insts_exit ≝ [ translate_move destrs tmp_destrs ] in
873            add_translates (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
874      ]
875    ]
876  ].
877  [2: >tmp_destrs_proof @prf_destrs
878  |1: normalize nodelta
879      generalize in match srcrs12_proof
880      #HYP >rev_length >rev_length @HYP
881  ]
882qed.
883
884definition add_128_to_last ≝
885  λtmp_128: register.
886  λrs.
887  λprf: 0 < |rs|.
888  λstart_lbl: label.
889  match rs with
890  [ nil ⇒ adds_graph [ ] start_lbl
891  | _ ⇒
892    let r ≝ last_safe ? rs prf in
893      adds_graph [
894        rtl_st_op2 Add r r tmp_128 start_lbl
895      ] start_lbl
896  ].
897
898definition translate_lts ≝
899  λdestrs: list register.
900  λdestrs_prf: lt 0 (|destrs|).
901  λsrcrs1: list register.
902  λsrcrs2: list register.
903  λsrcrs1_lt_prf: 0 < |srcrs1|.
904  λsrcrs2_lt_prf: 0 < |srcrs2|.
905  λstart_lbl: label.
906  λdest_lbl: label.
907  λdef: rtl_internal_function.
908  match fresh_regs_strong def (|srcrs1|) with
909  [ dp def_tmp_srcrs1 srcrs1_prf ⇒
910    let def ≝ \fst def_tmp_srcrs1 in
911    let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
912    match fresh_regs_strong def (|srcrs2|) with
913    [ dp def_tmp_srcrs2 srcrs2_prf ⇒
914      let def ≝ \fst def_tmp_srcrs2 in
915      let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
916      let 〈def, tmp_128〉 ≝ fresh_reg def in
917        add_translates [
918          translate_move tmp_srcrs1 srcrs1;
919          translate_move tmp_srcrs2 srcrs2;
920          adds_graph [
921            rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl
922          ];
923          add_128_to_last tmp_128 tmp_srcrs1 ?;
924          add_128_to_last tmp_128 tmp_srcrs2 ?;
925          translate_lt destrs destrs_prf tmp_srcrs1 tmp_srcrs2
926        ] start_lbl dest_lbl def
927    ]
928  ].
929  [1: >srcrs1_prf @srcrs1_lt_prf
930  |2: >srcrs2_prf @srcrs2_lt_prf
931  ]
932qed.
933
934definition translate_op2 ≝
935  λop2.
936  λdestrs: list register.
937  λdestrs_prf: lt 0 (|destrs|).
938  λsrcrs1: list register.
939  λsrcrs2: list register.
940  λsrcrs1_prf: lt 0 (|srcrs1|). (* can this be relaxed? i think it can
941                                   but we need more dep. typ. in modu/divu
942                                   cases *)
943  λsrcrs2_prf: lt 0 (|srcrs2|).
944  λstart_lbl: label.
945  λdest_lbl: label.
946  λdef: rtl_internal_function.
947  match op2 with
948  [ Oadd ⇒
949    translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
950  | Oaddp ⇒
951    translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
952  | Osub ⇒
953    translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
954  | Osubpi ⇒
955    translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
956  | Osubpp sz ⇒
957    translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
958  | Omul ⇒
959    translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def
960  | Odivu ⇒
961    match srcrs1 return λx. 0 < |x| → rtl_internal_function with
962    [ cons hd tl ⇒ λcons_prf.
963      match tl with
964      [ nil ⇒ translate_divumodu8 true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
965      | _ ⇒ ? (* not implemented *)
966      ]
967    | nil ⇒ λnil_absrd. ?
968    ] srcrs1_prf
969  | Omodu ⇒
970    match srcrs1 return λx. 0 < |x| → rtl_internal_function with
971    [ cons hd tl ⇒ λcons_prf.
972      match tl with
973      [ nil ⇒ translate_divumodu8 false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
974      | _ ⇒ ? (* not implemented *)
975      ]
976    | nil ⇒ λnil_absrd. ?
977    ] srcrs1_prf
978  | Oand ⇒
979    translate_op And destrs srcrs1 srcrs2 start_lbl dest_lbl def
980  | Oor ⇒
981    translate_op Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
982  | Oxor ⇒
983    translate_op Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
984  | Ocmp c ⇒
985    match c with
986    [ Ceq ⇒
987      add_translates [
988        translate_ne destrs srcrs1 srcrs2;
989        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
990      ] start_lbl dest_lbl def
991    | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
992    | Clt ⇒ translate_lts destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def
993    | Cgt ⇒ translate_lts destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def
994    | Cle ⇒
995      add_translates [
996        translate_lts destrs destrs_prf srcrs2 srcrs1 ? ?;
997        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
998      ] start_lbl dest_lbl def
999    | Cge ⇒
1000      add_translates [
1001        translate_lts destrs destrs_prf srcrs1 srcrs2 ? ?;
1002        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1003      ] start_lbl dest_lbl def
1004    ]
1005  | Ocmpu c ⇒
1006    match c with
1007    [ Ceq ⇒
1008      add_translates [
1009        translate_ne destrs srcrs1 srcrs2;
1010        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1011      ] start_lbl dest_lbl def
1012    | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
1013    | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
1014    | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
1015    | Cle ⇒
1016      add_translates [
1017        translate_lt destrs destrs_prf srcrs2 srcrs1;
1018        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1019      ] start_lbl dest_lbl def
1020    | Cge ⇒
1021      add_translates [
1022        translate_lt destrs destrs_prf srcrs1 srcrs2;
1023        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1024      ] start_lbl dest_lbl def
1025    ]
1026  | Ocmpp c ⇒
1027    match c with
1028    [ Ceq ⇒
1029      add_translates [
1030        translate_ne destrs srcrs1 srcrs2;
1031        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1032      ] start_lbl dest_lbl def
1033    | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
1034    | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
1035    | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
1036    | Cle ⇒
1037      add_translates [
1038        translate_lt destrs destrs_prf srcrs2 srcrs1;
1039        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1040      ] start_lbl dest_lbl def
1041    | Cge ⇒
1042      add_translates [
1043        translate_lt destrs destrs_prf srcrs1 srcrs2;
1044        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1045      ] start_lbl dest_lbl def
1046    ]
1047  | _ ⇒ ? (* assert false, implemented in run time or float op *)
1048  ].
1049  [ 2,6: normalize in nil_absrd;
1050         cases(not_le_Sn_O 0)
1051         #HYP cases(HYP nil_absrd)
1052  | 3,7,12,17,13,15,18,19,20,21,14,16:
1053         assumption
1054  | *:   cases not_implemented (* yes, really *)
1055  ]
1056qed.
1057
1058definition translate_cond ≝
1059  λsrcrs: list register.
1060  λstart_lbl: label.
1061  λlbl_true: label.
1062  λlbl_false: label.
1063  λdef: rtl_internal_function.
1064  let 〈def, tmpr〉 ≝ fresh_reg def in
1065  let 〈def, tmp_lbl〉 ≝ fresh_label def in
1066  let init ≝ rtl_st_int tmpr (zero ?) start_lbl in
1067  let f ≝ λsrcr. rtl_st_op2 Or tmpr tmpr srcr start_lbl in
1068  let def ≝ adds_graph (init :: (map … f srcrs)) start_lbl tmp_lbl def in
1069    add_graph tmp_lbl (rtl_st_cond tmpr lbl_true lbl_false) def. 
1070
1071definition translate_load ≝
1072  λaddr.
1073  λaddr_prf: 2 ≤ |addr|.
1074  λdestrs: list register.
1075  λstart_lbl: label.
1076  λdest_lbl: label.
1077  λdef: rtl_internal_function.
1078  match fresh_regs_strong def (|addr|) with
1079  [ dp def_save_addr save_addr_prf ⇒
1080    let def ≝ \fst def_save_addr in
1081    let save_addr ≝ \snd def_save_addr in
1082    match fresh_regs_strong def (|addr|) with
1083    [ dp def_tmp_addr tmp_addr_prf ⇒
1084      let def ≝ \fst def_tmp_addr in
1085      let tmp_addr ≝ \snd def_tmp_addr in
1086      let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
1087      let 〈def, tmpr〉 ≝ fresh_reg def in
1088      let insts_save_addr ≝ translate_move save_addr addr in
1089      let f ≝ λtranslates_off. λr.
1090        let 〈translates, off〉 ≝ translates_off in
1091        let translates ≝ translates @ [
1092          adds_graph [
1093            rtl_st_int tmpr off start_lbl
1094          ];
1095          translate_op2 Oaddp tmp_addr ? save_addr [tmpr] ? ?;
1096          adds_graph [
1097            rtl_st_load r tmp_addr1 tmp_addr2 dest_lbl
1098          ]
1099        ]
1100        in
1101        let 〈carry, result〉 ≝ half_add ? off int_size in
1102          〈translates, result〉
1103      in
1104      let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], (zero ?)〉 destrs in
1105        add_translates (insts_save_addr :: translates) start_lbl dest_lbl def
1106    ]
1107  ].
1108  [1: normalize //
1109  |2: >save_addr_prf normalize
1110      @(transitive_le 1 2 (|addr|)) //
1111  |3: >tmp_addr_prf normalize
1112      @(transitive_le 1 2 (|addr|)) //
1113  |*: >tmp_addr_prf assumption
1114  ]
1115qed.
1116
1117definition translate_store ≝
1118  λaddr.
1119  λaddr_prf: 2 ≤ |addr|.
1120  λsrcrs: list register.
1121  λstart_lbl: label.
1122  λdest_lbl: label.
1123  λdef: rtl_internal_function.
1124  match fresh_regs_strong def (|addr|) with
1125  [ dp def_tmp_addr tmp_addr_prf ⇒
1126    let def ≝ \fst def_tmp_addr in
1127    let tmp_addr ≝ \snd def_tmp_addr in
1128    let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
1129    let 〈def, tmpr〉 ≝ fresh_reg def in
1130    let f ≝ λtranslate_off. λsrcr.
1131      let 〈translates, off〉 ≝ translate_off in
1132      let translates ≝ translates @ [
1133        adds_graph [
1134          rtl_st_int tmpr off start_lbl
1135        ];
1136        translate_op2 Oaddp tmp_addr ? addr [tmpr] ? ?;
1137        adds_graph [
1138          rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
1139        ]
1140      ]
1141      in
1142        let 〈carry, result〉 ≝ half_add ? off int_size in
1143          〈translates, result〉
1144    in
1145    let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], zero ?〉 srcrs in
1146      add_translates translates start_lbl dest_lbl def
1147  ].
1148  [1: normalize //
1149  |2: >tmp_addr_prf normalize
1150      @(transitive_le 1 2 (|addr|)) //
1151  |3: >tmp_addr_prf normalize
1152      @(transitive_le 1 2 (|addr|)) //
1153  |*: >tmp_addr_prf assumption
1154  ]
1155qed.
1156
1157definition translate_stmt ≝
1158  λlenv.
1159  λlbl: label.
1160  λstmt.
1161  λdef: rtl_internal_function.
1162  match stmt with
1163  [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
1164  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
1165  | St_const destr cst lbl' ⇒
1166    translate_cst cst (find_local_env destr lenv) lbl lbl' def
1167  | St_op1 op1 destr srcr lbl' ⇒
1168    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) ? lbl lbl' def
1169  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
1170    translate_op2 op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
1171  | St_load ignore addr destr lbl' ⇒
1172    translate_load (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
1173  | St_store ignore addr srcr lbl' ⇒
1174    translate_store (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
1175  | St_call_id f args retr lbl' ⇒
1176    match retr with
1177    [ Some retr ⇒
1178      add_graph lbl (rtl_st_call_id f (rtl_args args lenv) (find_local_env retr lenv) lbl') def
1179    | None ⇒ add_graph lbl (rtl_st_call_id f (rtl_args args lenv) [ ] lbl') def
1180    ]
1181  | St_call_ptr f args retr lbl' ⇒
1182    match retr with
1183    [ None ⇒
1184      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1185        add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) [ ] lbl') def
1186    | Some retr ⇒
1187      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1188        add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv) lbl') def
1189    ]
1190  | St_tailcall_id f args ⇒
1191    add_graph lbl (rtl_st_tailcall_id f (rtl_args args lenv)) def
1192  | St_tailcall_ptr f args ⇒
1193    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1194      add_graph lbl (rtl_st_tailcall_ptr f1 f2 (rtl_args args lenv)) def
1195  | St_cond r lbl_true lbl_false ⇒
1196    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
1197  | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
1198  | St_return r ⇒
1199    match r with
1200    [ None ⇒ add_graph lbl (rtl_st_return [ ]) def
1201    | Some r ⇒ add_graph lbl (rtl_st_return (find_local_env r lenv)) def
1202    ]
1203  | _ ⇒ ?
1204  ].
1205
1206let translate_stmt lenv lbl stmt def = match stmt with
1207
1208  | RTLabs.St_skip lbl' ->
1209    add_graph lbl (RTL.St_skip lbl') def
1210
1211  | RTLabs.St_cost (cost_lbl, lbl') ->
1212    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
1213
1214  | RTLabs.St_cst (destr, cst, lbl') ->
1215    translate_cst cst (find_local_env destr lenv) lbl lbl' def
1216
1217  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
1218    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
1219      lbl lbl' def
1220
1221  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
1222    translate_op2 op2 (find_local_env destr lenv)
1223      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
1224
1225  | RTLabs.St_load (_, addr, destr, lbl') ->
1226    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
1227      lbl lbl' def
1228
1229  | RTLabs.St_store (_, addr, srcr, lbl') ->
1230    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
1231      lbl lbl' def
1232
1233  | RTLabs.St_call_id (f, args, None, _, lbl') ->
1234    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
1235
1236  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
1237    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
1238                                   find_local_env retr lenv, lbl')) def
1239
1240  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
1241    let (f1, f2) = find_and_addr f lenv in
1242    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
1243
1244  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
1245    let (f1, f2) = find_and_addr f lenv in
1246    add_graph lbl
1247      (RTL.St_call_ptr
1248         (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
1249
1250  | RTLabs.St_tailcall_id (f, args, _) ->
1251    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
1252
1253  | RTLabs.St_tailcall_ptr (f, args, _) ->
1254    let (f1, f2) = find_and_addr f lenv in
1255    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
1256
1257  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
1258    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
1259
1260  | RTLabs.St_jumptable _ ->
1261    error "Jump tables not supported yet."
1262
1263  | RTLabs.St_return None ->
1264    add_graph lbl (RTL.St_return []) def
1265
1266  | RTLabs.St_return (Some r) ->
1267    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
1268
1269definition filter_and_to_list_local_env_internal ≝
1270  λlenv.
1271  λl.
1272  λr.
1273  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
1274  [ Some entry ⇒
1275    match entry with
1276    [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ])
1277    | register_int r ⇒ (l @ [ r ])
1278    ]
1279  | None       ⇒ [ ] (* dpm: should this be none? *)
1280  ].
1281
1282definition filter_and_to_list_local_env ≝
1283  λlenv.
1284  λregisters.
1285    foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers.
1286
1287definition list_of_register_type ≝
1288  λrt.
1289  match rt with
1290  [ register_ptr r1 r2 ⇒ [ r1; r2 ]
1291  | register_int r ⇒ [ r ]
1292  ].
1293
1294definition find_and_list ≝
1295  λr.
1296  λlenv.
1297  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
1298  [ None      ⇒ [ ] (* dpm: should this be none? *)
1299  | Some lkup ⇒ list_of_register_type lkup
1300  ].
1301
1302definition find_and_list_args ≝
1303  λargs.
1304  λlenv.
1305    map ? ? (λr. find_and_list r lenv) args.
1306 
1307(* dpm: horrendous, use dependent types.
1308  length destr = length srcrs *)
1309let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label)
1310                       (dest_lbl: label) (def: ?) ≝
1311  match destrs with
1312  [ nil ⇒
1313    match srcrs with
1314    [ nil        ⇒ Some ? def
1315    | cons hd tl ⇒ None ?
1316    ]
1317  | cons hd tl ⇒
1318    match srcrs with
1319    [ nil        ⇒ None ?
1320    | cons hd' tl' ⇒
1321      match tl with
1322      [ nil            ⇒
1323        match tl' with
1324        (* one element lists *)
1325        [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def)
1326        | cons hd'' tl'' ⇒ None ?
1327        ]
1328      | cons hd'' tl'' ⇒
1329        match tl' with
1330        [ nil ⇒ None ?
1331        (* multielement lists *)
1332        | cons hd''' tl''' ⇒
1333          let tmp_lbl ≝ fresh_label def in
1334          match tmp_lbl with
1335          [ None ⇒ None ?
1336          | Some tmp_lbl ⇒
1337            let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in
1338              translate_move tl tl' tmp_lbl dest_lbl def
1339          ]
1340        ]
1341      ]
1342    ]
1343  ].
1344
1345definition extract_singleton ≝
1346  λA: Type[0].
1347  λl: list A.
1348  match l with
1349  [ nil ⇒ None ?
1350  | cons hd tl ⇒
1351    match tl with
1352    [ nil ⇒ Some ? hd
1353    | cons hd tl ⇒ None ?
1354    ]
1355  ].
1356
1357definition extract_pair ≝
1358  λA: Type[0].
1359  λl: list A.
1360  match l with
1361  [ nil ⇒ None ?
1362  | cons hd tl ⇒
1363    match tl with
1364    [ nil ⇒ None ?
1365    | cons hd' tl' ⇒
1366      match tl' with
1367      [ nil ⇒ Some ? 〈hd, hd'〉
1368      | cons hd'' tl'' ⇒ None ?
1369      ]
1370    ]
1371  ].
1372
1373definition translate_op1 ≝
1374  λop1.
1375  λdestrs.
1376  λsrcrs.
1377  λstart_lbl.
1378  λdest_lbl.
1379  λdef.
1380  match op1 with
1381  [ op_cast8_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1382  | op_cast8_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1383  | op_cast16_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1384  | op_cast16_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1385  | op_neg_int ⇒
1386    let dstr ≝ extract_singleton ? destrs in
1387    let srcr ≝ extract_singleton ? srcrs in
1388    match dstr with
1389    [ None ⇒ None ?
1390    | Some dstr ⇒
1391      match srcr with
1392      [ None ⇒ None ?
1393      | Some srcr ⇒
1394        adds_graph [
1395          rtl_st_op1 Cmpl dstr srcr start_lbl;
1396          rtl_st_op1 Inc dstr dstr start_lbl
1397        ] start_lbl dest_lbl def
1398      ]
1399    ]
1400  | op_not_int ⇒
1401    let dstr ≝ extract_singleton ? destrs in
1402    let srcr ≝ extract_singleton ? srcrs in
1403    match dstr with
1404    [ None ⇒ None ?
1405    | Some dstr ⇒
1406      match srcr with
1407      [ None ⇒ None ?
1408      | Some srcr ⇒
1409        adds_graph [
1410          rtl_st_op1 Cmpl dstr srcr start_lbl
1411        ] start_lbl dest_lbl def
1412      ]
1413    ]
1414  | op_id ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1415  | op_ptr_of_int ⇒
1416    let destr12 ≝ extract_pair ? destrs in
1417    let srcr ≝ extract_singleton ? srcrs in
1418    match destr12 with
1419    [ None ⇒ None ?
1420    | Some destr12 ⇒
1421      let 〈destr1, destr2〉 ≝ destr12 in
1422      match srcr with
1423      [ None ⇒ None ?
1424      | Some srcr ⇒
1425        adds_graph [
1426          rtl_st_move destr1 srcr dest_lbl;
1427          rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl
1428        ] start_lbl dest_lbl def
1429      ]
1430    ]
1431  | op_int_of_ptr ⇒
1432    let destr ≝ extract_singleton ? destrs in
1433    match destr with
1434    [ None ⇒ None ?
1435    | Some destr ⇒
1436      match srcrs with
1437      [ nil ⇒ None ?
1438      | cons srcr tl ⇒
1439        Some ? (add_graph start_lbl (rtl_st_move destr srcr dest_lbl) def)
1440      ]
1441    ]
1442  | op_not_bool ⇒
1443    let destr ≝ extract_singleton ? destrs in
1444    let srcrs ≝ extract_singleton ? srcrs in
1445    match destr with
1446    [ None ⇒ None ?
1447    | Some destr ⇒
1448      match srcrs with
1449      [ None ⇒ None ?
1450      | Some srcr ⇒
1451        let 〈def, tmpr〉 ≝ fresh_reg def in
1452        adds_graph [
1453          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
1454          rtl_st_clear_carry start_lbl;
1455          rtl_st_op2 Sub destr tmpr srcr start_lbl;
1456          rtl_st_int destr (bitvector_of_nat ? 0) dest_lbl;
1457          rtl_st_op2 Addc destr destr destr start_lbl;
1458          rtl_st_int tmpr (bitvector_of_nat ? 1) dest_lbl;
1459          rtl_st_op2 Xor destr destr tmpr start_lbl
1460        ] start_lbl dest_lbl def
1461      ]
1462    ]
1463  | _ ⇒ None ? (* error float *)
1464  ].
1465
1466definition translate_condptr ≝
1467  λr1.
1468  λr2.
1469  λstart_lbl: label.
1470  λlbl_true: label.
1471  λlbl_false: label.
1472  λdef.
1473  let 〈def, tmpr〉 ≝ fresh_reg def in
1474    adds_graph [
1475      rtl_st_op2 Or tmpr r1 r2 start_lbl;
1476      rtl_st_cond_acc tmpr lbl_true lbl_false
1477    ] start_lbl start_lbl def.
1478   
1479   
1480
1481(*
1482let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?)
1483                      (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝
1484  match op2 with
1485  [ op_add ⇒
1486    let destr ≝ extract_singleton ? destrs in
1487    let srcr1 ≝ extract_singleton ? srcrs1 in
1488    let srcr2 ≝ extract_singleton ? srcrs2 in
1489    match destr with
1490    [ None ⇒ None ?
1491    | Some destr ⇒
1492      match srcr1 with
1493      [ None ⇒ None ?
1494      | Some srcr1 ⇒
1495        match srcr2 with
1496        [ None ⇒ None ?
1497        | Some srcr2 ⇒
1498          adds_graph [
1499            rtl_st_op2 Add destr srcr1 srcr2 start_lbl
1500          ] start_lbl dest_lbl def
1501        ]
1502      ]
1503    ]
1504  | op_sub ⇒
1505    let destr ≝ extract_singleton ? destrs in
1506    let srcr1 ≝ extract_singleton ? srcrs1 in
1507    let srcr2 ≝ extract_singleton ? srcrs2 in
1508    match destr with
1509    [ None ⇒ None ?
1510    | Some destr ⇒
1511      match srcr1 with
1512      [ None ⇒ None ?
1513      | Some srcr1 ⇒
1514        match srcr2 with
1515        [ None ⇒ None ?
1516        | Some srcr2 ⇒
1517          adds_graph [
1518            rtl_st_clear_carry start_lbl;
1519            rtl_st_op2 Sub destr srcr1 srcr2 start_lbl
1520          ] start_lbl dest_lbl def
1521        ]
1522      ]
1523    ]
1524  | op_mul ⇒
1525    let destr ≝ extract_singleton ? destrs in
1526    let srcr1 ≝ extract_singleton ? srcrs1 in
1527    let srcr2 ≝ extract_singleton ? srcrs2 in
1528    match destr with
1529    [ None ⇒ None ?
1530    | Some destr ⇒
1531      match srcr1 with
1532      [ None ⇒ None ?
1533      | Some srcr1 ⇒
1534        match srcr2 with
1535        [ None ⇒ None ?
1536        | Some srcr2 ⇒
1537          adds_graph [
1538            rtl_st_opaccs Mul destr srcr1 srcr2 start_lbl
1539          ] start_lbl dest_lbl def
1540        ]
1541      ]
1542    ]
1543  | op_div ⇒ None ? (* signed div not supported *)
1544  | op_divu ⇒
1545    let destr ≝ extract_singleton ? destrs in
1546    let srcr1 ≝ extract_singleton ? srcrs1 in
1547    let srcr2 ≝ extract_singleton ? srcrs2 in
1548    match destr with
1549    [ None ⇒ None ?
1550    | Some destr ⇒
1551      match srcr1 with
1552      [ None ⇒ None ?
1553      | Some srcr1 ⇒
1554        match srcr2 with
1555        [ None ⇒ None ?
1556        | Some srcr2 ⇒
1557          adds_graph [
1558            rtl_st_opaccs Divu destr srcr1 srcr2 start_lbl
1559          ] start_lbl dest_lbl def
1560        ]
1561      ]
1562    ]
1563  | op_modu ⇒
1564    let destr ≝ extract_singleton ? destrs in
1565    let srcr1 ≝ extract_singleton ? srcrs1 in
1566    let srcr2 ≝ extract_singleton ? srcrs2 in
1567    match destr with
1568    [ None ⇒ None ?
1569    | Some destr ⇒
1570      match srcr1 with
1571      [ None ⇒ None ?
1572      | Some srcr1 ⇒
1573        match srcr2 with
1574        [ None ⇒ None ?
1575        | Some srcr2 ⇒
1576          adds_graph [
1577            rtl_st_opaccs Modu destr srcr1 srcr2 start_lbl
1578          ] start_lbl dest_lbl def
1579        ]
1580      ]
1581    ]
1582  | op_mod ⇒ None ? (* signed mod not supported *)
1583  | op_and ⇒
1584    let destr ≝ extract_singleton ? destrs in
1585    let srcr1 ≝ extract_singleton ? srcrs1 in
1586    let srcr2 ≝ extract_singleton ? srcrs2 in
1587    match destr with
1588    [ None ⇒ None ?
1589    | Some destr ⇒
1590      match srcr1 with
1591      [ None ⇒ None ?
1592      | Some srcr1 ⇒
1593        match srcr2 with
1594        [ None ⇒ None ?
1595        | Some srcr2 ⇒
1596          adds_graph [
1597            rtl_st_op2 And destr srcr1 srcr2 start_lbl
1598          ] start_lbl dest_lbl def
1599        ]
1600      ]
1601    ]
1602  | op_or ⇒
1603    let destr ≝ extract_singleton ? destrs in
1604    let srcr1 ≝ extract_singleton ? srcrs1 in
1605    let srcr2 ≝ extract_singleton ? srcrs2 in
1606    match destr with
1607    [ None ⇒ None ?
1608    | Some destr ⇒
1609      match srcr1 with
1610      [ None ⇒ None ?
1611      | Some srcr1 ⇒
1612        match srcr2 with
1613        [ None ⇒ None ?
1614        | Some srcr2 ⇒
1615          adds_graph [
1616            rtl_st_op2 Or destr srcr1 srcr2 start_lbl
1617          ] start_lbl dest_lbl def
1618        ]
1619      ]
1620    ]
1621  | op_xor ⇒
1622    let destr ≝ extract_singleton ? destrs in
1623    let srcr1 ≝ extract_singleton ? srcrs1 in
1624    let srcr2 ≝ extract_singleton ? srcrs2 in
1625    match destr with
1626    [ None ⇒ None ?
1627    | Some destr ⇒
1628      match srcr1 with
1629      [ None ⇒ None ?
1630      | Some srcr1 ⇒
1631        match srcr2 with
1632        [ None ⇒ None ?
1633        | Some srcr2 ⇒
1634          adds_graph [
1635            rtl_st_op2 Xor destr srcr1 srcr2 start_lbl
1636          ] start_lbl dest_lbl def
1637        ]
1638      ]
1639    ]
1640  | op_shru ⇒ None ? (* shifts not supported *)
1641  | op_shr ⇒ None ?
1642  | op_shl ⇒ None ?
1643  | op_addf ⇒ None ? (* floats not supported *)
1644  | op_subf ⇒ None ?
1645  | op_mulf ⇒ None ?
1646  | op_divf ⇒ None ?
1647  | op_cmpf _ ⇒ None ?
1648  | op_addp ⇒
1649    let destr12 ≝ extract_pair ? destrs in
1650    match destr12 with
1651    [ None         ⇒ None ?
1652    | Some destr12 ⇒
1653      let 〈destr1, destr2〉 ≝ destr12 in
1654      let srcr12 ≝ extract_pair ? srcrs1 in
1655      match srcr12 with
1656      [ None ⇒
1657        let srcr2 ≝ extract_singleton ? srcrs1 in
1658        match srcr2 with
1659        [ None ⇒ None ?
1660        | Some srcr2 ⇒
1661          let srcr12 ≝ extract_pair ? srcrs2 in
1662          match srcr12 with
1663          [ None ⇒ None ?
1664          | Some srcr12 ⇒
1665            let 〈srcr11, srcr12〉 ≝ srcr12 in
1666            let 〈def, tmpr1〉 ≝ fresh_reg def in
1667            let 〈def, tmpr2〉 ≝ fresh_reg def in
1668              adds_graph [
1669                rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
1670                rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
1671                rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
1672                rtl_st_move destr1 tmpr1 start_lbl
1673              ] start_lbl dest_lbl def
1674          ]
1675        ]
1676      | Some srcr12 ⇒
1677        let 〈srcr11, srcr12〉 ≝ srcr12 in
1678        let srcr2 ≝ extract_singleton ? srcrs2 in
1679        match srcr2 with
1680        [ None       ⇒ None ?
1681        | Some srcr2 ⇒
1682          let 〈def, tmpr1〉 ≝ fresh_reg def in
1683          let 〈def, tmpr2〉 ≝ fresh_reg def in
1684            adds_graph [
1685              rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
1686              rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
1687              rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
1688              rtl_st_move destr1 tmpr1 start_lbl
1689            ] start_lbl dest_lbl def
1690        ]
1691      ]
1692    ]
1693  | op_subp ⇒
1694    let destr ≝ extract_singleton ? destrs in
1695    match destr with
1696    [ None ⇒
1697      let destr12 ≝ extract_pair ? destrs in
1698      match destr12 with
1699      [ None ⇒ None ?
1700      | Some destr12 ⇒
1701        let 〈destr1, destr2〉 ≝ destr12 in
1702        let srcr12 ≝ extract_pair ? srcrs1 in
1703        match srcr12 with
1704        [ None ⇒ None ?
1705        | Some srcr12 ⇒
1706          let 〈srcr11, srcr12〉 ≝ srcr12 in
1707          let srcr2 ≝ extract_singleton ? srcrs2 in
1708          match srcr2 with
1709          [ None ⇒ None ?
1710          | Some srcr2 ⇒
1711            adds_graph [
1712              rtl_st_clear_carry start_lbl;
1713              rtl_st_op2 Sub destr1 srcr11 srcr2 start_lbl;
1714              rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl;
1715              rtl_st_op2 Sub destr2 srcr12 destr2 start_lbl
1716            ] start_lbl dest_lbl def
1717          ]
1718        ]
1719      ]
1720    | Some destr ⇒
1721      match srcrs1 with
1722      [ nil ⇒ None ?
1723      | cons srcr1 tl ⇒
1724        match srcrs2 with
1725        [ nil ⇒ None ?
1726        | cons srcr2 tl' ⇒
1727          let 〈def, tmpr1〉 ≝ fresh_reg def in
1728          let 〈def, tmpr2〉 ≝ fresh_reg def in
1729            adds_graph [
1730              rtl_st_op1 Cmpl tmpr1 srcr2 start_lbl;
1731              rtl_st_int tmpr2 (bitvector_of_nat ? 1) start_lbl;
1732              rtl_st_op2 Add tmpr1 tmpr1 tmpr2 start_lbl;
1733              rtl_st_op2 Add destr srcr1 tmpr1 start_lbl
1734            ] start_lbl dest_lbl def
1735        ]
1736      ]
1737    ]
1738  | op_cmp cmp ⇒
1739    match cmp with
1740    [ Compare_Equal ⇒
1741      add_translates [
1742        translate_op2 op_sub destrs srcrs1 srcrs2;
1743        translate_op1 op_not_bool destrs destrs
1744      ] start_lbl dest_lbl def
1745    | Compare_NotEqual ⇒
1746      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
1747    | _ ⇒ None ?
1748    ]
1749  | op_cmpu cmp ⇒
1750    match cmp with
1751    [ Compare_Equal ⇒
1752      add_translates [
1753        translate_op2 op_sub destrs srcrs1 srcrs2;
1754        translate_op1 op_not_bool destrs destrs
1755      ] start_lbl dest_lbl def
1756    | Compare_NotEqual ⇒
1757      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
1758    | Compare
1759    | _ ⇒ None ?
1760    ]
1761  | _ ⇒ ?
1762  ].
1763
1764    | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
1765      let (def, tmpr) = fresh_reg def in
1766      adds_graph
1767        [RTL.St_clear_carry start_lbl ;
1768         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
1769         RTL.St_int (destr, 0, start_lbl) ;
1770         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
1771        start_lbl dest_lbl def
1772
1773    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
1774      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
1775        destrs srcrs2 srcrs1 start_lbl dest_lbl def
1776
1777    | AST.Op_cmpu AST.Cmp_le, _, _, _ ->
1778      add_translates
1779        [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ;
1780         translate_op1 AST.Op_notbool destrs destrs]
1781        start_lbl dest_lbl def
1782
1783    | AST.Op_cmpu AST.Cmp_ge, _, _, _ ->
1784      add_translates
1785        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
1786         translate_op1 AST.Op_notbool destrs destrs]
1787        start_lbl dest_lbl def
1788
1789    | AST.Op_cmp cmp, _, _, _ ->
1790      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
1791      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
1792      add_translates
1793        [translate_cst (AST.Cst_int 128) tmprs1 ;
1794         translate_cst (AST.Cst_int 128) tmprs2 ;
1795         translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ;
1796         translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ;
1797         translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2]
1798        start_lbl dest_lbl def
1799
1800    | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
1801      let (def, tmpr) = fresh_reg def in
1802      add_translates
1803        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ;
1804         translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ;
1805         translate_op2 AST.Op_or [destr] [destr] [tmpr] ;
1806         adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ;
1807         translate_op2 AST.Op_xor [destr] [destr] [tmpr]]
1808        start_lbl dest_lbl def
1809
1810    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
1811      let (def, tmpr1) = fresh_reg def in
1812      let (def, tmpr2) = fresh_reg def in
1813      add_translates
1814        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
1815         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
1816         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
1817         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
1818         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
1819        start_lbl dest_lbl def
1820
1821    | AST.Op_cmpp AST.Cmp_gt, _, _, _ ->
1822      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
1823        destrs srcrs2 srcrs1 start_lbl dest_lbl def
1824
1825    | AST.Op_cmpp AST.Cmp_le, _, _, _ ->
1826      add_translates
1827        [translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ;
1828         translate_op1 AST.Op_notbool destrs destrs]
1829        start_lbl dest_lbl def
1830
1831    | AST.Op_cmpp AST.Cmp_ge, _, _, _ ->
1832      add_translates
1833        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
1834         translate_op1 AST.Op_notbool destrs destrs]
1835        start_lbl dest_lbl def
1836
1837    | _ -> assert false (* wrong number of arguments *)
1838*)
1839
1840definition translate_condcst ≝
1841  λcst.
1842  λstart_lbl: label.
1843  λlbl_true: label.
1844  λlbl_false: label.
1845  λdef.
1846  match cst with
1847  [ cast_int i ⇒
1848    let 〈def, tmpr〉 ≝ fresh_reg def in
1849    adds_graph [
1850      rtl_st_int tmpr i start_lbl;
1851      rtl_st_cond_acc tmpr lbl_true lbl_false
1852    ] start_lbl start_lbl def
1853  | cast_addr_symbol x ⇒
1854    let 〈def, r1〉 ≝ fresh_reg def in
1855    let 〈def, r2〉 ≝ fresh_reg def in
1856    let lbl ≝ fresh_label def in
1857    match lbl with
1858    [ None ⇒ None ?
1859    | Some lbl ⇒
1860      let def ≝ add_graph start_lbl (rtl_st_addr r1 r2 x lbl) def in
1861        translate_condptr r1 r2 lbl lbl_true lbl_false def
1862    ]
1863  | cast_stack_offset off ⇒
1864    let 〈def, r1〉 ≝ fresh_reg def in
1865    let 〈def, r2〉 ≝ fresh_reg def in
1866    let tmp_lbl ≝ fresh_label def in
1867    match tmp_lbl with
1868    [ None ⇒ None ?
1869    | Some tmp_lbl ⇒
1870      let def ≝ translate_cst (cast_stack_offset off) [r1; r2] start_lbl tmp_lbl def in
1871      match def with
1872      [ None ⇒ None ?
1873      | Some def ⇒ translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def
1874      ]
1875    ]
1876  | cast_float f ⇒ None ? (* error_float *)
1877  ].
1878
1879definition size_of_op1_ret ≝
1880  λop.
1881  match op with
1882  [ op_cast8_unsigned ⇒ Some ? 1
1883  | op_cast8_signed ⇒ Some ? 1
1884  | op_cast16_unsigned ⇒ Some ? 1
1885  | op_cast16_signed ⇒ Some ? 1
1886  | op_neg_int ⇒ Some ? 1
1887  | op_not_int ⇒ Some ? 1
1888  | op_int_of_ptr ⇒ Some ? 1
1889  | op_ptr_of_int ⇒ Some ? 2
1890  | op_id ⇒ None ? (* invalid_argument *)
1891  | _ ⇒ None ? (* error_float *)
1892  ].
1893
1894definition translate_cond1 ≝
1895  λop1.
1896  λsrcrs: list register.
1897  λstart_lbl: label.
1898  λlbl_true: label.
1899  λlbl_false: label.
1900  λdef.
1901  match op1 with
1902  [ op_id ⇒
1903    let srcr ≝ extract_singleton ? srcrs in
1904    match srcr with
1905    [ None ⇒
1906      let srcr12 ≝ extract_pair ? srcrs in
1907      match srcr12 with
1908      [ None ⇒ None ?
1909      | Some srcr12 ⇒
1910        let 〈srcr1, srcr2〉 ≝ srcr12 in
1911          translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def
1912      ]
1913    | Some srcr ⇒
1914      adds_graph [
1915        rtl_st_cond_acc srcr lbl_true lbl_false
1916      ] start_lbl start_lbl def
1917    ]
1918  | _     ⇒
1919    let size ≝ size_of_op1_ret op1 in
1920    match size with
1921    [ None ⇒ None ?
1922    | Some size ⇒
1923      let 〈def, destrs〉 ≝ fresh_regs def size in
1924      let lbl ≝ fresh_label def in
1925      match lbl with
1926      [ None ⇒ None ?
1927      | Some lbl ⇒
1928        let def ≝ translate_op1 op1 destrs srcrs start_lbl lbl def in
1929        match def with
1930        [ None ⇒ None ?
1931        | Some def ⇒
1932          let destr ≝ extract_singleton ? destrs in
1933          match destr with
1934          [ None ⇒
1935            let destr12 ≝ extract_pair ? destrs in
1936            match destr12 with
1937            [ None ⇒ None ?
1938            | Some destr12 ⇒
1939              let 〈destr1, destr2〉 ≝ destr12 in
1940                translate_condptr destr1 destr2 start_lbl lbl_true lbl_false def
1941            ]
1942          | Some destr ⇒
1943            adds_graph [
1944              rtl_st_cond_acc destr lbl_true lbl_false
1945            ] start_lbl start_lbl def
1946          ]
1947        ]
1948      ]
1949    ]
1950  ].
1951
1952definition size_of_op2_ret ≝
1953  λn: nat.
1954  λop2.
1955  match op2 with
1956  [ op_add ⇒ Some ? 1
1957  | op_sub ⇒ Some ? 1
1958  | op_mul ⇒ Some ? 1
1959  | op_div ⇒ Some ? 1
1960  | op_divu ⇒ Some ? 1
1961  | op_mod ⇒ Some ? 1
1962  | op_modu ⇒ Some ? 1
1963  | op_and ⇒ Some ? 1
1964  | op_or ⇒ Some ? 1
1965  | op_xor ⇒ Some ? 1
1966  | op_shl ⇒ Some ? 1
1967  | op_shr ⇒ Some ? 1
1968  | op_shru ⇒ Some ? 1
1969  | op_cmp _ ⇒ Some ? 1
1970  | op_cmpu _ ⇒ Some ? 1
1971  | op_cmpp _ ⇒ Some ? 1
1972  | op_addp ⇒ Some ? 2
1973  | op_subp ⇒
1974    if eq_nat n 4 then
1975      Some ? 1
1976    else
1977      Some ? 2
1978  | _ ⇒ None ? (* error_float *)
1979  ].
1980
1981axiom translate_op2:
1982  op2 → list register → list register → list register → label → label → rtl_internal_function → option rtl_internal_function.
1983
1984definition translate_cond2 ≝
1985  λop2.
1986  λsrcrs1: list register.
1987  λsrcrs2: list register.
1988  λstart_lbl: label.
1989  λlbl_true: label.
1990  λlbl_false: label.
1991  λdef.
1992  match op2 with
1993  [ op_cmp cmp ⇒
1994    match cmp with
1995    [ Compare_Equal ⇒
1996      let srcr1 ≝ extract_singleton ? srcrs1 in
1997      match srcr1 with
1998      [ None ⇒ None ?
1999      | Some srcr1 ⇒
2000        let srcr2 ≝ extract_singleton ? srcrs2 in
2001        match srcr2 with
2002        [ None ⇒ None ?
2003        | Some srcr2 ⇒
2004          let 〈def, tmpr〉 ≝ fresh_reg def in
2005          adds_graph [
2006            rtl_st_clear_carry start_lbl;
2007            rtl_st_op2 Sub tmpr srcr1 srcr2 start_lbl;
2008            rtl_st_cond_acc tmpr lbl_false lbl_true
2009          ] start_lbl start_lbl def
2010        ]
2011      ]
2012    | _ ⇒
2013      let n ≝ length ? srcrs1 + length ? srcrs2 in
2014      match size_of_op2_ret n op2 with
2015      [ None ⇒ None ?
2016      | Some size ⇒
2017        let 〈def, destrs〉 ≝ fresh_regs def size in
2018        let lbl ≝ fresh_label def in
2019        match lbl with
2020        [ None ⇒ None ?
2021        | Some lbl ⇒
2022          match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
2023          [ None ⇒ None ?
2024          | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
2025          ]
2026        ]
2027      ]
2028    ]
2029  | _ ⇒
2030    let n ≝ length ? srcrs1 + length ? srcrs2 in
2031    match size_of_op2_ret n op2 with
2032    [ None ⇒ None ?
2033    | Some size ⇒
2034      let 〈def, destrs〉 ≝ fresh_regs def size in
2035      let lbl ≝ fresh_label def in
2036      match lbl with
2037      [ None ⇒ None ?
2038      | Some lbl ⇒
2039        match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
2040        [ None ⇒ None ?
2041        | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
2042        ]
2043      ]
2044    ]
2045  ].
2046
2047let rec addressing_pointer (mode: ?) (args: ?) (destr1: ?)
2048                           (destr2: ?) (start_lbl: label)
2049                           (dest_lbl: label) (def: rtl_internal_function) ≝
2050  let destrs ≝ [ destr1; destr2 ] in
2051  match mode with
2052  [ Aindexed off ⇒
2053    let srcr12 ≝ extract_singleton ? args in
2054    match srcr12 with
2055    [ None ⇒ None ?
2056    | Some srcr12 ⇒
2057      let srcr12 ≝ extract_pair ? srcr12 in
2058      match srcr12 with
2059      [ None ⇒ None ?
2060      | Some srcr12 ⇒
2061        let 〈srcr1, srcr2〉 ≝ srcr12 in
2062        let 〈def, tmpr〉 ≝ fresh_reg def in
2063        add_translates [
2064          adds_graph [
2065            rtl_st_int tmpr off start_lbl
2066          ];
2067          translate_op2 op_addp destrs [ srcr1 ; srcr2 ] [tmpr]
2068        ] start_lbl dest_lbl def
2069      ]
2070    ]
2071  | Aindexed2 ⇒
2072    let args_pair ≝ extract_pair ? args in
2073    match args_pair with
2074    [ None ⇒ None ?
2075    | Some args_pair ⇒
2076      let 〈lft, rgt〉 ≝ args_pair in
2077      let srcr1112 ≝ extract_pair ? lft in
2078      let srcr2 ≝ extract_singleton ? rgt in
2079      match srcr1112 with
2080      [ None ⇒
2081        let srcr2 ≝ extract_singleton ? rgt in
2082        let srcr1112 ≝ extract_pair ? lft in
2083        match srcr2 with
2084        [ None ⇒ None ?
2085        | Some srcr2 ⇒
2086          match srcr1112 with
2087          [ None ⇒ None ?
2088          | Some srcr1112 ⇒
2089            let 〈srcr11, srcr12〉 ≝ srcr1112 in
2090            translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
2091          ]
2092        ]
2093      | Some srcr1112 ⇒
2094        let 〈srcr11, srcr12〉 ≝ srcr1112 in
2095        match srcr2 with
2096        [ None ⇒ None ?
2097        | Some srcr2 ⇒
2098          translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
2099        ]
2100      ]
2101    ]
2102  | Aglobal x off ⇒
2103    let 〈def, tmpr〉 ≝ fresh_reg def in
2104    add_translates [
2105      adds_graph [
2106        rtl_st_int tmpr off start_lbl;
2107        rtl_st_addr destr1 destr2 x start_lbl
2108      ];
2109      translate_op2 op_addp destrs destrs [ tmpr ]
2110    ] start_lbl dest_lbl def
2111  | Abased x off ⇒
2112    let srcrs ≝ extract_singleton ? args in
2113    match srcrs with
2114    [ None ⇒ None ?
2115    | Some srcrs ⇒
2116      let 〈def, tmpr1〉 ≝ fresh_reg def in
2117      let 〈def, tmpr2〉 ≝ fresh_reg def in
2118      (* mode, args, destr1, destr2, start_lbl, dest_lbl, def *)
2119      (* addressing_pointer (Aglobal x off) [ ] tmpr1 tmpr2; *)
2120      let address_unfold ≝
2121        let 〈def, tmpr〉 ≝ fresh_reg def in
2122          add_translates [
2123            adds_graph [
2124              rtl_st_int tmpr off start_lbl;
2125              rtl_st_addr tmpr1 tmpr2 x start_lbl
2126           ];
2127            translate_op2 op_addp destrs destrs [ tmpr ]
2128         ]
2129      in
2130      add_translates [
2131        address_unfold;
2132        translate_op2 op_addp destrs [ tmpr1; tmpr2 ] srcrs
2133      ] start_lbl dest_lbl def
2134    ]
2135  | Ainstack off ⇒
2136    let 〈def, tmpr〉 ≝ fresh_reg def in
2137    add_translates [
2138      adds_graph [
2139        rtl_st_int tmpr off start_lbl;
2140        rtl_st_stack_addr destr1 destr2 start_lbl
2141      ];
2142      translate_op2 op_addp destrs destrs [ tmpr ]
2143    ] start_lbl dest_lbl def
2144  | _ ⇒ None ? (* wrong number of arguments *)
2145  ].
2146
2147definition translate_load ≝
2148  λq.
2149  λmode.
2150  λargs.
2151  λdestrs.
2152  λstart_lbl: label.
2153  λdest_lbl: label.
2154  λdef.
2155  match q with
2156  [ q_int b ⇒
2157    if eq_bv ? b (bitvector_of_nat ? 1) then
2158      match extract_singleton ? destrs with
2159      [ None ⇒ None ? (* error: size error in load *)
2160      | Some destr ⇒
2161        let 〈def, addr1〉 ≝ fresh_reg def in
2162        let 〈def, addr2〉 ≝ fresh_reg def in
2163          Some ? (add_translates [
2164            addressing_pointer mode args addr1 addr2;
2165            adds_graph [
2166              rtl_st_load destr addr1 addr2 start_lbl
2167            ]
2168          ] start_lbl dest_lbl def)
2169      ]
2170    else
2171      None ? (* error: size error in load *)
2172  | q_ptr ⇒
2173    match extract_pair ? destrs with
2174    [ None ⇒ None ? (* error: size error in load *)
2175    | Some destr12 ⇒
2176      let 〈destr1, destr2〉 ≝ destr12 in
2177      let 〈def, addr1〉 ≝ fresh_reg def in
2178      let 〈def, addr2〉 ≝ fresh_reg def in
2179      let addr ≝ [ addr1; addr2 ] in
2180      let 〈def, tmpr〉 ≝ fresh_reg def in
2181        Some ? (
2182          add_translates [
2183            addressing_pointer mode args addr1 addr2;
2184            adds_graph [
2185              rtl_st_load destr1 addr1 addr2 start_lbl;
2186              rtl_st_int tmpr (bitvector_of_nat ? 1) start_lbl
2187            ];
2188            translate_op2 op_addp addr addr [ tmpr ];
2189            adds_graph [
2190              rtl_st_load destr2 addr1 addr2 start_lbl
2191            ]
2192          ] start_lbl dest_lbl def
2193        )
2194    ]
2195  | _ ⇒ None ? (* error: size error in load *)
2196  ].
2197 
2198definition make_addr ≝
2199  λA: Type[0].
2200  λlst: list A.
2201  match lst with
2202  [ cons hd tl ⇒
2203    match tl with
2204    [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
2205    | _ ⇒ None ? (* do not use on these arguments *)
2206    ]
2207  | _ ⇒ None ? (* do not use on these arguments *)
2208  ].
2209 
2210definition translate_store_internal ≝
2211  λaddr.
2212  λtmp_addr.
2213  λtmpr.
2214  λstart_lbl.
2215  λdest_lbl.
2216  λtmp_addr1.
2217  λtmp_addr2.
2218  λtranslates_off.
2219  λsrcr.
2220    let 〈translates, off〉 ≝ translates_off in
2221    let translates ≝ translates @
2222      [ adds_graph [
2223          rtl_st_int tmpr off start_lbl
2224        ];
2225        translate_op2 op_addp tmp_addr addr [ tmpr ];
2226        adds_graph [
2227          rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
2228        ]
2229      ]
2230    in
2231    let 〈ignore, result〉 ≝ half_add ? off int_size in
2232      〈translates, result〉.
2233 
2234definition translate_store ≝
2235  λaddr.
2236  λsrcrs.
2237  λstart_lbl.
2238  λdest_lbl.
2239  λdef.
2240    let 〈def, tmp_addr〉 ≝ fresh_regs def (length ? addr) in
2241    match make_addr ? tmp_addr with
2242    [ None ⇒ None ?
2243    | Some tmp_addr12 ⇒
2244      let 〈tmp_addr1, tmp_addr2〉 ≝ tmp_addr12 in
2245      let 〈def, tmpr〉 ≝ fresh_reg def in
2246      let f ≝ translate_store_internal addr tmp_addr tmpr start_lbl dest_lbl tmp_addr1 tmp_addr2 in
2247      let 〈translates, ignore〉 ≝ foldl ? ? f 〈[], zero ?〉 srcrs in
2248        add_translates translates start_lbl dest_lbl def
2249    ].
2250
2251definition translate_stmt ≝
2252  λlenv.
2253  λlbl.
2254  λstmt.
2255  λdef.
2256  match stmt with
2257  [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
2258  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
2259  | St_cast destr cst lbl' ⇒
2260      translate_cst cst (find_local_env destr lenv) lbl lbl' def
2261  | _ ⇒ ?
2262  ].
2263
2264let translate_stmt lenv lbl stmt def = match stmt with
2265
2266  | RTLabs.St_skip lbl' ->
2267    add_graph lbl (RTL.St_skip lbl') def
2268
2269  | RTLabs.St_cost (cost_lbl, lbl') ->
2270    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
2271
2272  | RTLabs.St_cst (destr, cst, lbl') ->
2273    translate_cst cst (find_local_env destr lenv) lbl lbl' def
2274
2275  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
2276    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
2277      lbl lbl' def
2278
2279  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
2280    translate_op2 op2 (find_local_env destr lenv)
2281      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
2282
2283  | RTLabs.St_load (_, addr, destr, lbl') ->
2284    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
2285      lbl lbl' def
2286
2287  | RTLabs.St_store (_, addr, srcr, lbl') ->
2288    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
2289      lbl lbl' def
2290
2291  | RTLabs.St_call_id (f, args, None, _, lbl') ->
2292    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
2293
2294  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
2295    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
2296                                   find_local_env retr lenv, lbl')) def
2297
2298  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
2299    let (f1, f2) = find_and_addr f lenv in
2300    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
2301
2302  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
2303    let (f1, f2) = find_and_addr f lenv in
2304    add_graph lbl
2305      (RTL.St_call_ptr
2306         (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
2307
2308  | RTLabs.St_tailcall_id (f, args, _) ->
2309    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
2310
2311  | RTLabs.St_tailcall_ptr (f, args, _) ->
2312    let (f1, f2) = find_and_addr f lenv in
2313    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
2314
2315  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
2316    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
2317
2318  | RTLabs.St_jumptable _ ->
2319    error "Jump tables not supported yet."
2320
2321  | RTLabs.St_return None ->
2322    add_graph lbl (RTL.St_return []) def
2323
2324  | RTLabs.St_return (Some r) ->
2325    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
Note: See TracBrowser for help on using the repository browser.