source: src/RTLabs/RTLAbstoRTL.ma @ 1067

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

more smaller changes

File size: 71.4 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  λret: register. (* change from o'caml code, this is taken from func. record *)
1160  λlbl: label.
1161  λstmt.
1162  λdef: rtl_internal_function.
1163  match stmt with
1164  [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
1165  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
1166  | St_const destr cst lbl' ⇒
1167    translate_cst cst (find_local_env destr lenv) lbl lbl' def
1168  | St_op1 op1 destr srcr lbl' ⇒
1169    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) ? lbl lbl' def
1170  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
1171    translate_op2 op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
1172  | St_load ignore addr destr lbl' ⇒
1173    translate_load (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
1174  | St_store ignore addr srcr lbl' ⇒
1175    translate_store (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
1176  | St_call_id f args retr lbl' ⇒
1177    match retr with
1178    [ Some retr ⇒
1179      add_graph lbl (rtl_st_call_id f (rtl_args args lenv) (find_local_env retr lenv) lbl') def
1180    | None ⇒ add_graph lbl (rtl_st_call_id f (rtl_args args lenv) [ ] lbl') def
1181    ]
1182  | St_call_ptr f args retr lbl' ⇒
1183    match retr with
1184    [ None ⇒
1185      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1186        add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) [ ] lbl') def
1187    | Some retr ⇒
1188      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1189        add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv) lbl') def
1190    ]
1191  | St_tailcall_id f args ⇒
1192    add_graph lbl (rtl_st_tailcall_id f (rtl_args args lenv)) def
1193  | St_tailcall_ptr f args ⇒
1194    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1195      add_graph lbl (rtl_st_tailcall_ptr f1 f2 (rtl_args args lenv)) def
1196  | St_cond r lbl_true lbl_false ⇒
1197    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
1198  | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
1199  | St_return ⇒ add_graph lbl (rtl_st_return (find_local_env ret lenv)) def
1200  ].
1201  [10: cases not_implemented (* jtable case *)
1202  |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *)
1203  ]
1204qed.
1205
1206definition translate_internal ≝
1207  λdef.
1208  let runiverse ≝ f_reggen def in
1209  let lenv ≝ initialize_local_env runiverse
1210    (f_params def @ f_locals def) (f_result def) in ?.
1211
1212let translate_internal def =
1213  let runiverse = def.RTLabs.f_runiverse in
1214  let lenv =
1215    initialize_local_env runiverse
1216      (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in
1217  let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
1218  let params = map_list_local_env lenv (List.map fst def.RTLabs.f_params) in
1219  let locals = map_list_local_env lenv (List.map fst def.RTLabs.f_locals) in
1220  let locals = set_of_list locals in
1221  let result = match def.RTLabs.f_result with
1222    | None -> []
1223    | Some (r, _) -> find_local_env r lenv in
1224  let res =
1225    { RTL.f_luniverse = def.RTLabs.f_luniverse ;
1226      RTL.f_runiverse = runiverse ;
1227      RTL.f_result    = result ;
1228      RTL.f_params    = params ;
1229      RTL.f_locals    = locals ;
1230      RTL.f_stacksize = concrete_size def.RTLabs.f_stacksize ;
1231      RTL.f_graph     = Label.Map.empty ;
1232      RTL.f_entry     = def.RTLabs.f_entry ;
1233      RTL.f_exit      = def.RTLabs.f_exit } in
1234  Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res
1235
1236definition filter_and_to_list_local_env_internal ≝
1237  λlenv.
1238  λl.
1239  λr.
1240  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
1241  [ Some entry ⇒
1242    match entry with
1243    [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ])
1244    | register_int r ⇒ (l @ [ r ])
1245    ]
1246  | None       ⇒ [ ] (* dpm: should this be none? *)
1247  ].
1248
1249definition filter_and_to_list_local_env ≝
1250  λlenv.
1251  λregisters.
1252    foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers.
1253
1254definition list_of_register_type ≝
1255  λrt.
1256  match rt with
1257  [ register_ptr r1 r2 ⇒ [ r1; r2 ]
1258  | register_int r ⇒ [ r ]
1259  ].
1260
1261definition find_and_list ≝
1262  λr.
1263  λlenv.
1264  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
1265  [ None      ⇒ [ ] (* dpm: should this be none? *)
1266  | Some lkup ⇒ list_of_register_type lkup
1267  ].
1268
1269definition find_and_list_args ≝
1270  λargs.
1271  λlenv.
1272    map ? ? (λr. find_and_list r lenv) args.
1273 
1274(* dpm: horrendous, use dependent types.
1275  length destr = length srcrs *)
1276let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label)
1277                       (dest_lbl: label) (def: ?) ≝
1278  match destrs with
1279  [ nil ⇒
1280    match srcrs with
1281    [ nil        ⇒ Some ? def
1282    | cons hd tl ⇒ None ?
1283    ]
1284  | cons hd tl ⇒
1285    match srcrs with
1286    [ nil        ⇒ None ?
1287    | cons hd' tl' ⇒
1288      match tl with
1289      [ nil            ⇒
1290        match tl' with
1291        (* one element lists *)
1292        [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def)
1293        | cons hd'' tl'' ⇒ None ?
1294        ]
1295      | cons hd'' tl'' ⇒
1296        match tl' with
1297        [ nil ⇒ None ?
1298        (* multielement lists *)
1299        | cons hd''' tl''' ⇒
1300          let tmp_lbl ≝ fresh_label def in
1301          match tmp_lbl with
1302          [ None ⇒ None ?
1303          | Some tmp_lbl ⇒
1304            let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in
1305              translate_move tl tl' tmp_lbl dest_lbl def
1306          ]
1307        ]
1308      ]
1309    ]
1310  ].
1311
1312definition extract_singleton ≝
1313  λA: Type[0].
1314  λl: list A.
1315  match l with
1316  [ nil ⇒ None ?
1317  | cons hd tl ⇒
1318    match tl with
1319    [ nil ⇒ Some ? hd
1320    | cons hd tl ⇒ None ?
1321    ]
1322  ].
1323
1324definition extract_pair ≝
1325  λA: Type[0].
1326  λl: list A.
1327  match l with
1328  [ nil ⇒ None ?
1329  | cons hd tl ⇒
1330    match tl with
1331    [ nil ⇒ None ?
1332    | cons hd' tl' ⇒
1333      match tl' with
1334      [ nil ⇒ Some ? 〈hd, hd'〉
1335      | cons hd'' tl'' ⇒ None ?
1336      ]
1337    ]
1338  ].
1339
1340definition translate_op1 ≝
1341  λop1.
1342  λdestrs.
1343  λsrcrs.
1344  λstart_lbl.
1345  λdest_lbl.
1346  λdef.
1347  match op1 with
1348  [ op_cast8_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1349  | op_cast8_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1350  | op_cast16_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1351  | op_cast16_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1352  | op_neg_int ⇒
1353    let dstr ≝ extract_singleton ? destrs in
1354    let srcr ≝ extract_singleton ? srcrs in
1355    match dstr with
1356    [ None ⇒ None ?
1357    | Some dstr ⇒
1358      match srcr with
1359      [ None ⇒ None ?
1360      | Some srcr ⇒
1361        adds_graph [
1362          rtl_st_op1 Cmpl dstr srcr start_lbl;
1363          rtl_st_op1 Inc dstr dstr start_lbl
1364        ] start_lbl dest_lbl def
1365      ]
1366    ]
1367  | op_not_int ⇒
1368    let dstr ≝ extract_singleton ? destrs in
1369    let srcr ≝ extract_singleton ? srcrs in
1370    match dstr with
1371    [ None ⇒ None ?
1372    | Some dstr ⇒
1373      match srcr with
1374      [ None ⇒ None ?
1375      | Some srcr ⇒
1376        adds_graph [
1377          rtl_st_op1 Cmpl dstr srcr start_lbl
1378        ] start_lbl dest_lbl def
1379      ]
1380    ]
1381  | op_id ⇒ translate_move destrs srcrs start_lbl dest_lbl def
1382  | op_ptr_of_int ⇒
1383    let destr12 ≝ extract_pair ? destrs in
1384    let srcr ≝ extract_singleton ? srcrs in
1385    match destr12 with
1386    [ None ⇒ None ?
1387    | Some destr12 ⇒
1388      let 〈destr1, destr2〉 ≝ destr12 in
1389      match srcr with
1390      [ None ⇒ None ?
1391      | Some srcr ⇒
1392        adds_graph [
1393          rtl_st_move destr1 srcr dest_lbl;
1394          rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl
1395        ] start_lbl dest_lbl def
1396      ]
1397    ]
1398  | op_int_of_ptr ⇒
1399    let destr ≝ extract_singleton ? destrs in
1400    match destr with
1401    [ None ⇒ None ?
1402    | Some destr ⇒
1403      match srcrs with
1404      [ nil ⇒ None ?
1405      | cons srcr tl ⇒
1406        Some ? (add_graph start_lbl (rtl_st_move destr srcr dest_lbl) def)
1407      ]
1408    ]
1409  | op_not_bool ⇒
1410    let destr ≝ extract_singleton ? destrs in
1411    let srcrs ≝ extract_singleton ? srcrs in
1412    match destr with
1413    [ None ⇒ None ?
1414    | Some destr ⇒
1415      match srcrs with
1416      [ None ⇒ None ?
1417      | Some srcr ⇒
1418        let 〈def, tmpr〉 ≝ fresh_reg def in
1419        adds_graph [
1420          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
1421          rtl_st_clear_carry start_lbl;
1422          rtl_st_op2 Sub destr tmpr srcr start_lbl;
1423          rtl_st_int destr (bitvector_of_nat ? 0) dest_lbl;
1424          rtl_st_op2 Addc destr destr destr start_lbl;
1425          rtl_st_int tmpr (bitvector_of_nat ? 1) dest_lbl;
1426          rtl_st_op2 Xor destr destr tmpr start_lbl
1427        ] start_lbl dest_lbl def
1428      ]
1429    ]
1430  | _ ⇒ None ? (* error float *)
1431  ].
1432
1433definition translate_condptr ≝
1434  λr1.
1435  λr2.
1436  λstart_lbl: label.
1437  λlbl_true: label.
1438  λlbl_false: label.
1439  λdef.
1440  let 〈def, tmpr〉 ≝ fresh_reg def in
1441    adds_graph [
1442      rtl_st_op2 Or tmpr r1 r2 start_lbl;
1443      rtl_st_cond_acc tmpr lbl_true lbl_false
1444    ] start_lbl start_lbl def.
1445   
1446   
1447
1448(*
1449let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?)
1450                      (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝
1451  match op2 with
1452  [ op_add ⇒
1453    let destr ≝ extract_singleton ? destrs in
1454    let srcr1 ≝ extract_singleton ? srcrs1 in
1455    let srcr2 ≝ extract_singleton ? srcrs2 in
1456    match destr with
1457    [ None ⇒ None ?
1458    | Some destr ⇒
1459      match srcr1 with
1460      [ None ⇒ None ?
1461      | Some srcr1 ⇒
1462        match srcr2 with
1463        [ None ⇒ None ?
1464        | Some srcr2 ⇒
1465          adds_graph [
1466            rtl_st_op2 Add destr srcr1 srcr2 start_lbl
1467          ] start_lbl dest_lbl def
1468        ]
1469      ]
1470    ]
1471  | op_sub ⇒
1472    let destr ≝ extract_singleton ? destrs in
1473    let srcr1 ≝ extract_singleton ? srcrs1 in
1474    let srcr2 ≝ extract_singleton ? srcrs2 in
1475    match destr with
1476    [ None ⇒ None ?
1477    | Some destr ⇒
1478      match srcr1 with
1479      [ None ⇒ None ?
1480      | Some srcr1 ⇒
1481        match srcr2 with
1482        [ None ⇒ None ?
1483        | Some srcr2 ⇒
1484          adds_graph [
1485            rtl_st_clear_carry start_lbl;
1486            rtl_st_op2 Sub destr srcr1 srcr2 start_lbl
1487          ] start_lbl dest_lbl def
1488        ]
1489      ]
1490    ]
1491  | op_mul ⇒
1492    let destr ≝ extract_singleton ? destrs in
1493    let srcr1 ≝ extract_singleton ? srcrs1 in
1494    let srcr2 ≝ extract_singleton ? srcrs2 in
1495    match destr with
1496    [ None ⇒ None ?
1497    | Some destr ⇒
1498      match srcr1 with
1499      [ None ⇒ None ?
1500      | Some srcr1 ⇒
1501        match srcr2 with
1502        [ None ⇒ None ?
1503        | Some srcr2 ⇒
1504          adds_graph [
1505            rtl_st_opaccs Mul destr srcr1 srcr2 start_lbl
1506          ] start_lbl dest_lbl def
1507        ]
1508      ]
1509    ]
1510  | op_div ⇒ None ? (* signed div not supported *)
1511  | op_divu ⇒
1512    let destr ≝ extract_singleton ? destrs in
1513    let srcr1 ≝ extract_singleton ? srcrs1 in
1514    let srcr2 ≝ extract_singleton ? srcrs2 in
1515    match destr with
1516    [ None ⇒ None ?
1517    | Some destr ⇒
1518      match srcr1 with
1519      [ None ⇒ None ?
1520      | Some srcr1 ⇒
1521        match srcr2 with
1522        [ None ⇒ None ?
1523        | Some srcr2 ⇒
1524          adds_graph [
1525            rtl_st_opaccs Divu destr srcr1 srcr2 start_lbl
1526          ] start_lbl dest_lbl def
1527        ]
1528      ]
1529    ]
1530  | op_modu ⇒
1531    let destr ≝ extract_singleton ? destrs in
1532    let srcr1 ≝ extract_singleton ? srcrs1 in
1533    let srcr2 ≝ extract_singleton ? srcrs2 in
1534    match destr with
1535    [ None ⇒ None ?
1536    | Some destr ⇒
1537      match srcr1 with
1538      [ None ⇒ None ?
1539      | Some srcr1 ⇒
1540        match srcr2 with
1541        [ None ⇒ None ?
1542        | Some srcr2 ⇒
1543          adds_graph [
1544            rtl_st_opaccs Modu destr srcr1 srcr2 start_lbl
1545          ] start_lbl dest_lbl def
1546        ]
1547      ]
1548    ]
1549  | op_mod ⇒ None ? (* signed mod not supported *)
1550  | op_and ⇒
1551    let destr ≝ extract_singleton ? destrs in
1552    let srcr1 ≝ extract_singleton ? srcrs1 in
1553    let srcr2 ≝ extract_singleton ? srcrs2 in
1554    match destr with
1555    [ None ⇒ None ?
1556    | Some destr ⇒
1557      match srcr1 with
1558      [ None ⇒ None ?
1559      | Some srcr1 ⇒
1560        match srcr2 with
1561        [ None ⇒ None ?
1562        | Some srcr2 ⇒
1563          adds_graph [
1564            rtl_st_op2 And destr srcr1 srcr2 start_lbl
1565          ] start_lbl dest_lbl def
1566        ]
1567      ]
1568    ]
1569  | op_or ⇒
1570    let destr ≝ extract_singleton ? destrs in
1571    let srcr1 ≝ extract_singleton ? srcrs1 in
1572    let srcr2 ≝ extract_singleton ? srcrs2 in
1573    match destr with
1574    [ None ⇒ None ?
1575    | Some destr ⇒
1576      match srcr1 with
1577      [ None ⇒ None ?
1578      | Some srcr1 ⇒
1579        match srcr2 with
1580        [ None ⇒ None ?
1581        | Some srcr2 ⇒
1582          adds_graph [
1583            rtl_st_op2 Or destr srcr1 srcr2 start_lbl
1584          ] start_lbl dest_lbl def
1585        ]
1586      ]
1587    ]
1588  | op_xor ⇒
1589    let destr ≝ extract_singleton ? destrs in
1590    let srcr1 ≝ extract_singleton ? srcrs1 in
1591    let srcr2 ≝ extract_singleton ? srcrs2 in
1592    match destr with
1593    [ None ⇒ None ?
1594    | Some destr ⇒
1595      match srcr1 with
1596      [ None ⇒ None ?
1597      | Some srcr1 ⇒
1598        match srcr2 with
1599        [ None ⇒ None ?
1600        | Some srcr2 ⇒
1601          adds_graph [
1602            rtl_st_op2 Xor destr srcr1 srcr2 start_lbl
1603          ] start_lbl dest_lbl def
1604        ]
1605      ]
1606    ]
1607  | op_shru ⇒ None ? (* shifts not supported *)
1608  | op_shr ⇒ None ?
1609  | op_shl ⇒ None ?
1610  | op_addf ⇒ None ? (* floats not supported *)
1611  | op_subf ⇒ None ?
1612  | op_mulf ⇒ None ?
1613  | op_divf ⇒ None ?
1614  | op_cmpf _ ⇒ None ?
1615  | op_addp ⇒
1616    let destr12 ≝ extract_pair ? destrs in
1617    match destr12 with
1618    [ None         ⇒ None ?
1619    | Some destr12 ⇒
1620      let 〈destr1, destr2〉 ≝ destr12 in
1621      let srcr12 ≝ extract_pair ? srcrs1 in
1622      match srcr12 with
1623      [ None ⇒
1624        let srcr2 ≝ extract_singleton ? srcrs1 in
1625        match srcr2 with
1626        [ None ⇒ None ?
1627        | Some srcr2 ⇒
1628          let srcr12 ≝ extract_pair ? srcrs2 in
1629          match srcr12 with
1630          [ None ⇒ None ?
1631          | Some srcr12 ⇒
1632            let 〈srcr11, srcr12〉 ≝ srcr12 in
1633            let 〈def, tmpr1〉 ≝ fresh_reg def in
1634            let 〈def, tmpr2〉 ≝ fresh_reg def in
1635              adds_graph [
1636                rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
1637                rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
1638                rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
1639                rtl_st_move destr1 tmpr1 start_lbl
1640              ] start_lbl dest_lbl def
1641          ]
1642        ]
1643      | Some srcr12 ⇒
1644        let 〈srcr11, srcr12〉 ≝ srcr12 in
1645        let srcr2 ≝ extract_singleton ? srcrs2 in
1646        match srcr2 with
1647        [ None       ⇒ None ?
1648        | Some srcr2 ⇒
1649          let 〈def, tmpr1〉 ≝ fresh_reg def in
1650          let 〈def, tmpr2〉 ≝ fresh_reg def in
1651            adds_graph [
1652              rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
1653              rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
1654              rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
1655              rtl_st_move destr1 tmpr1 start_lbl
1656            ] start_lbl dest_lbl def
1657        ]
1658      ]
1659    ]
1660  | op_subp ⇒
1661    let destr ≝ extract_singleton ? destrs in
1662    match destr with
1663    [ None ⇒
1664      let destr12 ≝ extract_pair ? destrs in
1665      match destr12 with
1666      [ None ⇒ None ?
1667      | Some destr12 ⇒
1668        let 〈destr1, destr2〉 ≝ destr12 in
1669        let srcr12 ≝ extract_pair ? srcrs1 in
1670        match srcr12 with
1671        [ None ⇒ None ?
1672        | Some srcr12 ⇒
1673          let 〈srcr11, srcr12〉 ≝ srcr12 in
1674          let srcr2 ≝ extract_singleton ? srcrs2 in
1675          match srcr2 with
1676          [ None ⇒ None ?
1677          | Some srcr2 ⇒
1678            adds_graph [
1679              rtl_st_clear_carry start_lbl;
1680              rtl_st_op2 Sub destr1 srcr11 srcr2 start_lbl;
1681              rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl;
1682              rtl_st_op2 Sub destr2 srcr12 destr2 start_lbl
1683            ] start_lbl dest_lbl def
1684          ]
1685        ]
1686      ]
1687    | Some destr ⇒
1688      match srcrs1 with
1689      [ nil ⇒ None ?
1690      | cons srcr1 tl ⇒
1691        match srcrs2 with
1692        [ nil ⇒ None ?
1693        | cons srcr2 tl' ⇒
1694          let 〈def, tmpr1〉 ≝ fresh_reg def in
1695          let 〈def, tmpr2〉 ≝ fresh_reg def in
1696            adds_graph [
1697              rtl_st_op1 Cmpl tmpr1 srcr2 start_lbl;
1698              rtl_st_int tmpr2 (bitvector_of_nat ? 1) start_lbl;
1699              rtl_st_op2 Add tmpr1 tmpr1 tmpr2 start_lbl;
1700              rtl_st_op2 Add destr srcr1 tmpr1 start_lbl
1701            ] start_lbl dest_lbl def
1702        ]
1703      ]
1704    ]
1705  | op_cmp cmp ⇒
1706    match cmp with
1707    [ Compare_Equal ⇒
1708      add_translates [
1709        translate_op2 op_sub destrs srcrs1 srcrs2;
1710        translate_op1 op_not_bool destrs destrs
1711      ] start_lbl dest_lbl def
1712    | Compare_NotEqual ⇒
1713      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
1714    | _ ⇒ None ?
1715    ]
1716  | op_cmpu cmp ⇒
1717    match cmp with
1718    [ Compare_Equal ⇒
1719      add_translates [
1720        translate_op2 op_sub destrs srcrs1 srcrs2;
1721        translate_op1 op_not_bool destrs destrs
1722      ] start_lbl dest_lbl def
1723    | Compare_NotEqual ⇒
1724      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
1725    | Compare
1726    | _ ⇒ None ?
1727    ]
1728  | _ ⇒ ?
1729  ].
1730
1731    | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
1732      let (def, tmpr) = fresh_reg def in
1733      adds_graph
1734        [RTL.St_clear_carry start_lbl ;
1735         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
1736         RTL.St_int (destr, 0, start_lbl) ;
1737         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
1738        start_lbl dest_lbl def
1739
1740    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
1741      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
1742        destrs srcrs2 srcrs1 start_lbl dest_lbl def
1743
1744    | AST.Op_cmpu AST.Cmp_le, _, _, _ ->
1745      add_translates
1746        [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ;
1747         translate_op1 AST.Op_notbool destrs destrs]
1748        start_lbl dest_lbl def
1749
1750    | AST.Op_cmpu AST.Cmp_ge, _, _, _ ->
1751      add_translates
1752        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
1753         translate_op1 AST.Op_notbool destrs destrs]
1754        start_lbl dest_lbl def
1755
1756    | AST.Op_cmp cmp, _, _, _ ->
1757      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
1758      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
1759      add_translates
1760        [translate_cst (AST.Cst_int 128) tmprs1 ;
1761         translate_cst (AST.Cst_int 128) tmprs2 ;
1762         translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ;
1763         translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ;
1764         translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2]
1765        start_lbl dest_lbl def
1766
1767    | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
1768      let (def, tmpr) = fresh_reg def in
1769      add_translates
1770        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ;
1771         translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ;
1772         translate_op2 AST.Op_or [destr] [destr] [tmpr] ;
1773         adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ;
1774         translate_op2 AST.Op_xor [destr] [destr] [tmpr]]
1775        start_lbl dest_lbl def
1776
1777    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
1778      let (def, tmpr1) = fresh_reg def in
1779      let (def, tmpr2) = fresh_reg def in
1780      add_translates
1781        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
1782         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
1783         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
1784         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
1785         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
1786        start_lbl dest_lbl def
1787
1788    | AST.Op_cmpp AST.Cmp_gt, _, _, _ ->
1789      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
1790        destrs srcrs2 srcrs1 start_lbl dest_lbl def
1791
1792    | AST.Op_cmpp AST.Cmp_le, _, _, _ ->
1793      add_translates
1794        [translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ;
1795         translate_op1 AST.Op_notbool destrs destrs]
1796        start_lbl dest_lbl def
1797
1798    | AST.Op_cmpp AST.Cmp_ge, _, _, _ ->
1799      add_translates
1800        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
1801         translate_op1 AST.Op_notbool destrs destrs]
1802        start_lbl dest_lbl def
1803
1804    | _ -> assert false (* wrong number of arguments *)
1805*)
1806
1807definition translate_condcst ≝
1808  λcst.
1809  λstart_lbl: label.
1810  λlbl_true: label.
1811  λlbl_false: label.
1812  λdef.
1813  match cst with
1814  [ cast_int i ⇒
1815    let 〈def, tmpr〉 ≝ fresh_reg def in
1816    adds_graph [
1817      rtl_st_int tmpr i start_lbl;
1818      rtl_st_cond_acc tmpr lbl_true lbl_false
1819    ] start_lbl start_lbl def
1820  | cast_addr_symbol x ⇒
1821    let 〈def, r1〉 ≝ fresh_reg def in
1822    let 〈def, r2〉 ≝ fresh_reg def in
1823    let lbl ≝ fresh_label def in
1824    match lbl with
1825    [ None ⇒ None ?
1826    | Some lbl ⇒
1827      let def ≝ add_graph start_lbl (rtl_st_addr r1 r2 x lbl) def in
1828        translate_condptr r1 r2 lbl lbl_true lbl_false def
1829    ]
1830  | cast_stack_offset off ⇒
1831    let 〈def, r1〉 ≝ fresh_reg def in
1832    let 〈def, r2〉 ≝ fresh_reg def in
1833    let tmp_lbl ≝ fresh_label def in
1834    match tmp_lbl with
1835    [ None ⇒ None ?
1836    | Some tmp_lbl ⇒
1837      let def ≝ translate_cst (cast_stack_offset off) [r1; r2] start_lbl tmp_lbl def in
1838      match def with
1839      [ None ⇒ None ?
1840      | Some def ⇒ translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def
1841      ]
1842    ]
1843  | cast_float f ⇒ None ? (* error_float *)
1844  ].
1845
1846definition size_of_op1_ret ≝
1847  λop.
1848  match op with
1849  [ op_cast8_unsigned ⇒ Some ? 1
1850  | op_cast8_signed ⇒ Some ? 1
1851  | op_cast16_unsigned ⇒ Some ? 1
1852  | op_cast16_signed ⇒ Some ? 1
1853  | op_neg_int ⇒ Some ? 1
1854  | op_not_int ⇒ Some ? 1
1855  | op_int_of_ptr ⇒ Some ? 1
1856  | op_ptr_of_int ⇒ Some ? 2
1857  | op_id ⇒ None ? (* invalid_argument *)
1858  | _ ⇒ None ? (* error_float *)
1859  ].
1860
1861definition translate_cond1 ≝
1862  λop1.
1863  λsrcrs: list register.
1864  λstart_lbl: label.
1865  λlbl_true: label.
1866  λlbl_false: label.
1867  λdef.
1868  match op1 with
1869  [ op_id ⇒
1870    let srcr ≝ extract_singleton ? srcrs in
1871    match srcr with
1872    [ None ⇒
1873      let srcr12 ≝ extract_pair ? srcrs in
1874      match srcr12 with
1875      [ None ⇒ None ?
1876      | Some srcr12 ⇒
1877        let 〈srcr1, srcr2〉 ≝ srcr12 in
1878          translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def
1879      ]
1880    | Some srcr ⇒
1881      adds_graph [
1882        rtl_st_cond_acc srcr lbl_true lbl_false
1883      ] start_lbl start_lbl def
1884    ]
1885  | _     ⇒
1886    let size ≝ size_of_op1_ret op1 in
1887    match size with
1888    [ None ⇒ None ?
1889    | Some size ⇒
1890      let 〈def, destrs〉 ≝ fresh_regs def size in
1891      let lbl ≝ fresh_label def in
1892      match lbl with
1893      [ None ⇒ None ?
1894      | Some lbl ⇒
1895        let def ≝ translate_op1 op1 destrs srcrs start_lbl lbl def in
1896        match def with
1897        [ None ⇒ None ?
1898        | Some def ⇒
1899          let destr ≝ extract_singleton ? destrs in
1900          match destr with
1901          [ None ⇒
1902            let destr12 ≝ extract_pair ? destrs in
1903            match destr12 with
1904            [ None ⇒ None ?
1905            | Some destr12 ⇒
1906              let 〈destr1, destr2〉 ≝ destr12 in
1907                translate_condptr destr1 destr2 start_lbl lbl_true lbl_false def
1908            ]
1909          | Some destr ⇒
1910            adds_graph [
1911              rtl_st_cond_acc destr lbl_true lbl_false
1912            ] start_lbl start_lbl def
1913          ]
1914        ]
1915      ]
1916    ]
1917  ].
1918
1919definition size_of_op2_ret ≝
1920  λn: nat.
1921  λop2.
1922  match op2 with
1923  [ op_add ⇒ Some ? 1
1924  | op_sub ⇒ Some ? 1
1925  | op_mul ⇒ Some ? 1
1926  | op_div ⇒ Some ? 1
1927  | op_divu ⇒ Some ? 1
1928  | op_mod ⇒ Some ? 1
1929  | op_modu ⇒ Some ? 1
1930  | op_and ⇒ Some ? 1
1931  | op_or ⇒ Some ? 1
1932  | op_xor ⇒ Some ? 1
1933  | op_shl ⇒ Some ? 1
1934  | op_shr ⇒ Some ? 1
1935  | op_shru ⇒ Some ? 1
1936  | op_cmp _ ⇒ Some ? 1
1937  | op_cmpu _ ⇒ Some ? 1
1938  | op_cmpp _ ⇒ Some ? 1
1939  | op_addp ⇒ Some ? 2
1940  | op_subp ⇒
1941    if eq_nat n 4 then
1942      Some ? 1
1943    else
1944      Some ? 2
1945  | _ ⇒ None ? (* error_float *)
1946  ].
1947
1948axiom translate_op2:
1949  op2 → list register → list register → list register → label → label → rtl_internal_function → option rtl_internal_function.
1950
1951definition translate_cond2 ≝
1952  λop2.
1953  λsrcrs1: list register.
1954  λsrcrs2: list register.
1955  λstart_lbl: label.
1956  λlbl_true: label.
1957  λlbl_false: label.
1958  λdef.
1959  match op2 with
1960  [ op_cmp cmp ⇒
1961    match cmp with
1962    [ Compare_Equal ⇒
1963      let srcr1 ≝ extract_singleton ? srcrs1 in
1964      match srcr1 with
1965      [ None ⇒ None ?
1966      | Some srcr1 ⇒
1967        let srcr2 ≝ extract_singleton ? srcrs2 in
1968        match srcr2 with
1969        [ None ⇒ None ?
1970        | Some srcr2 ⇒
1971          let 〈def, tmpr〉 ≝ fresh_reg def in
1972          adds_graph [
1973            rtl_st_clear_carry start_lbl;
1974            rtl_st_op2 Sub tmpr srcr1 srcr2 start_lbl;
1975            rtl_st_cond_acc tmpr lbl_false lbl_true
1976          ] start_lbl start_lbl def
1977        ]
1978      ]
1979    | _ ⇒
1980      let n ≝ length ? srcrs1 + length ? srcrs2 in
1981      match size_of_op2_ret n op2 with
1982      [ None ⇒ None ?
1983      | Some size ⇒
1984        let 〈def, destrs〉 ≝ fresh_regs def size in
1985        let lbl ≝ fresh_label def in
1986        match lbl with
1987        [ None ⇒ None ?
1988        | Some lbl ⇒
1989          match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
1990          [ None ⇒ None ?
1991          | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
1992          ]
1993        ]
1994      ]
1995    ]
1996  | _ ⇒
1997    let n ≝ length ? srcrs1 + length ? srcrs2 in
1998    match size_of_op2_ret n op2 with
1999    [ None ⇒ None ?
2000    | Some size ⇒
2001      let 〈def, destrs〉 ≝ fresh_regs def size in
2002      let lbl ≝ fresh_label def in
2003      match lbl with
2004      [ None ⇒ None ?
2005      | Some lbl ⇒
2006        match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
2007        [ None ⇒ None ?
2008        | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
2009        ]
2010      ]
2011    ]
2012  ].
2013
2014let rec addressing_pointer (mode: ?) (args: ?) (destr1: ?)
2015                           (destr2: ?) (start_lbl: label)
2016                           (dest_lbl: label) (def: rtl_internal_function) ≝
2017  let destrs ≝ [ destr1; destr2 ] in
2018  match mode with
2019  [ Aindexed off ⇒
2020    let srcr12 ≝ extract_singleton ? args in
2021    match srcr12 with
2022    [ None ⇒ None ?
2023    | Some srcr12 ⇒
2024      let srcr12 ≝ extract_pair ? srcr12 in
2025      match srcr12 with
2026      [ None ⇒ None ?
2027      | Some srcr12 ⇒
2028        let 〈srcr1, srcr2〉 ≝ srcr12 in
2029        let 〈def, tmpr〉 ≝ fresh_reg def in
2030        add_translates [
2031          adds_graph [
2032            rtl_st_int tmpr off start_lbl
2033          ];
2034          translate_op2 op_addp destrs [ srcr1 ; srcr2 ] [tmpr]
2035        ] start_lbl dest_lbl def
2036      ]
2037    ]
2038  | Aindexed2 ⇒
2039    let args_pair ≝ extract_pair ? args in
2040    match args_pair with
2041    [ None ⇒ None ?
2042    | Some args_pair ⇒
2043      let 〈lft, rgt〉 ≝ args_pair in
2044      let srcr1112 ≝ extract_pair ? lft in
2045      let srcr2 ≝ extract_singleton ? rgt in
2046      match srcr1112 with
2047      [ None ⇒
2048        let srcr2 ≝ extract_singleton ? rgt in
2049        let srcr1112 ≝ extract_pair ? lft in
2050        match srcr2 with
2051        [ None ⇒ None ?
2052        | Some srcr2 ⇒
2053          match srcr1112 with
2054          [ None ⇒ None ?
2055          | Some srcr1112 ⇒
2056            let 〈srcr11, srcr12〉 ≝ srcr1112 in
2057            translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
2058          ]
2059        ]
2060      | Some srcr1112 ⇒
2061        let 〈srcr11, srcr12〉 ≝ srcr1112 in
2062        match srcr2 with
2063        [ None ⇒ None ?
2064        | Some srcr2 ⇒
2065          translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
2066        ]
2067      ]
2068    ]
2069  | Aglobal x off ⇒
2070    let 〈def, tmpr〉 ≝ fresh_reg def in
2071    add_translates [
2072      adds_graph [
2073        rtl_st_int tmpr off start_lbl;
2074        rtl_st_addr destr1 destr2 x start_lbl
2075      ];
2076      translate_op2 op_addp destrs destrs [ tmpr ]
2077    ] start_lbl dest_lbl def
2078  | Abased x off ⇒
2079    let srcrs ≝ extract_singleton ? args in
2080    match srcrs with
2081    [ None ⇒ None ?
2082    | Some srcrs ⇒
2083      let 〈def, tmpr1〉 ≝ fresh_reg def in
2084      let 〈def, tmpr2〉 ≝ fresh_reg def in
2085      (* mode, args, destr1, destr2, start_lbl, dest_lbl, def *)
2086      (* addressing_pointer (Aglobal x off) [ ] tmpr1 tmpr2; *)
2087      let address_unfold ≝
2088        let 〈def, tmpr〉 ≝ fresh_reg def in
2089          add_translates [
2090            adds_graph [
2091              rtl_st_int tmpr off start_lbl;
2092              rtl_st_addr tmpr1 tmpr2 x start_lbl
2093           ];
2094            translate_op2 op_addp destrs destrs [ tmpr ]
2095         ]
2096      in
2097      add_translates [
2098        address_unfold;
2099        translate_op2 op_addp destrs [ tmpr1; tmpr2 ] srcrs
2100      ] start_lbl dest_lbl def
2101    ]
2102  | Ainstack 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_stack_addr destr1 destr2 start_lbl
2108      ];
2109      translate_op2 op_addp destrs destrs [ tmpr ]
2110    ] start_lbl dest_lbl def
2111  | _ ⇒ None ? (* wrong number of arguments *)
2112  ].
2113
2114definition translate_load ≝
2115  λq.
2116  λmode.
2117  λargs.
2118  λdestrs.
2119  λstart_lbl: label.
2120  λdest_lbl: label.
2121  λdef.
2122  match q with
2123  [ q_int b ⇒
2124    if eq_bv ? b (bitvector_of_nat ? 1) then
2125      match extract_singleton ? destrs with
2126      [ None ⇒ None ? (* error: size error in load *)
2127      | Some destr ⇒
2128        let 〈def, addr1〉 ≝ fresh_reg def in
2129        let 〈def, addr2〉 ≝ fresh_reg def in
2130          Some ? (add_translates [
2131            addressing_pointer mode args addr1 addr2;
2132            adds_graph [
2133              rtl_st_load destr addr1 addr2 start_lbl
2134            ]
2135          ] start_lbl dest_lbl def)
2136      ]
2137    else
2138      None ? (* error: size error in load *)
2139  | q_ptr ⇒
2140    match extract_pair ? destrs with
2141    [ None ⇒ None ? (* error: size error in load *)
2142    | Some destr12 ⇒
2143      let 〈destr1, destr2〉 ≝ destr12 in
2144      let 〈def, addr1〉 ≝ fresh_reg def in
2145      let 〈def, addr2〉 ≝ fresh_reg def in
2146      let addr ≝ [ addr1; addr2 ] in
2147      let 〈def, tmpr〉 ≝ fresh_reg def in
2148        Some ? (
2149          add_translates [
2150            addressing_pointer mode args addr1 addr2;
2151            adds_graph [
2152              rtl_st_load destr1 addr1 addr2 start_lbl;
2153              rtl_st_int tmpr (bitvector_of_nat ? 1) start_lbl
2154            ];
2155            translate_op2 op_addp addr addr [ tmpr ];
2156            adds_graph [
2157              rtl_st_load destr2 addr1 addr2 start_lbl
2158            ]
2159          ] start_lbl dest_lbl def
2160        )
2161    ]
2162  | _ ⇒ None ? (* error: size error in load *)
2163  ].
2164 
2165definition make_addr ≝
2166  λA: Type[0].
2167  λlst: list A.
2168  match lst with
2169  [ cons hd tl ⇒
2170    match tl with
2171    [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
2172    | _ ⇒ None ? (* do not use on these arguments *)
2173    ]
2174  | _ ⇒ None ? (* do not use on these arguments *)
2175  ].
2176 
2177definition translate_store_internal ≝
2178  λaddr.
2179  λtmp_addr.
2180  λtmpr.
2181  λstart_lbl.
2182  λdest_lbl.
2183  λtmp_addr1.
2184  λtmp_addr2.
2185  λtranslates_off.
2186  λsrcr.
2187    let 〈translates, off〉 ≝ translates_off in
2188    let translates ≝ translates @
2189      [ adds_graph [
2190          rtl_st_int tmpr off start_lbl
2191        ];
2192        translate_op2 op_addp tmp_addr addr [ tmpr ];
2193        adds_graph [
2194          rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
2195        ]
2196      ]
2197    in
2198    let 〈ignore, result〉 ≝ half_add ? off int_size in
2199      〈translates, result〉.
2200 
2201definition translate_store ≝
2202  λaddr.
2203  λsrcrs.
2204  λstart_lbl.
2205  λdest_lbl.
2206  λdef.
2207    let 〈def, tmp_addr〉 ≝ fresh_regs def (length ? addr) in
2208    match make_addr ? tmp_addr with
2209    [ None ⇒ None ?
2210    | Some tmp_addr12 ⇒
2211      let 〈tmp_addr1, tmp_addr2〉 ≝ tmp_addr12 in
2212      let 〈def, tmpr〉 ≝ fresh_reg def in
2213      let f ≝ translate_store_internal addr tmp_addr tmpr start_lbl dest_lbl tmp_addr1 tmp_addr2 in
2214      let 〈translates, ignore〉 ≝ foldl ? ? f 〈[], zero ?〉 srcrs in
2215        add_translates translates start_lbl dest_lbl def
2216    ].
2217
2218definition translate_stmt ≝
2219  λlenv.
2220  λlbl.
2221  λstmt.
2222  λdef.
2223  match stmt with
2224  [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
2225  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
2226  | St_cast destr cst lbl' ⇒
2227      translate_cst cst (find_local_env destr lenv) lbl lbl' def
2228  | _ ⇒ ?
2229  ].
2230
2231let translate_stmt lenv lbl stmt def = match stmt with
2232
2233  | RTLabs.St_skip lbl' ->
2234    add_graph lbl (RTL.St_skip lbl') def
2235
2236  | RTLabs.St_cost (cost_lbl, lbl') ->
2237    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
2238
2239  | RTLabs.St_cst (destr, cst, lbl') ->
2240    translate_cst cst (find_local_env destr lenv) lbl lbl' def
2241
2242  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
2243    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
2244      lbl lbl' def
2245
2246  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
2247    translate_op2 op2 (find_local_env destr lenv)
2248      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
2249
2250  | RTLabs.St_load (_, addr, destr, lbl') ->
2251    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
2252      lbl lbl' def
2253
2254  | RTLabs.St_store (_, addr, srcr, lbl') ->
2255    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
2256      lbl lbl' def
2257
2258  | RTLabs.St_call_id (f, args, None, _, lbl') ->
2259    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
2260
2261  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
2262    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
2263                                   find_local_env retr lenv, lbl')) def
2264
2265  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
2266    let (f1, f2) = find_and_addr f lenv in
2267    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
2268
2269  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
2270    let (f1, f2) = find_and_addr f lenv in
2271    add_graph lbl
2272      (RTL.St_call_ptr
2273         (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
2274
2275  | RTLabs.St_tailcall_id (f, args, _) ->
2276    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
2277
2278  | RTLabs.St_tailcall_ptr (f, args, _) ->
2279    let (f1, f2) = find_and_addr f lenv in
2280    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
2281
2282  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
2283    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
2284
2285  | RTLabs.St_jumptable _ ->
2286    error "Jump tables not supported yet."
2287
2288  | RTLabs.St_return None ->
2289    add_graph lbl (RTL.St_return []) def
2290
2291  | RTLabs.St_return (Some r) ->
2292    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
Note: See TracBrowser for help on using the repository browser.