source: src/RTLabs/RTLAbstoRTL.ma @ 1281

Last change on this file since 1281 was 1281, checked in by sacerdot, 8 years ago

Porting of all transformation to the joint syntax practically completed.
Some functions remain to be ported in RTLAbstoRTL, but it is just repetitive
coding.

File size: 37.0 KB
Line 
1include "RTLabs/syntax.ma".
2include "RTL/RTL.ma".
3include "common/AssocList.ma".
4include "common/FrontEndOps.ma".
5include "common/Graphs.ma".
6include "joint/TranslateUtils.ma".
7
8let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
9  match n with
10  [ O ⇒ 〈[],runiverse〉
11  | S n' ⇒
12     let 〈r,runiverse〉 ≝ fresh … runiverse in
13     let 〈res,runiverse〉 ≝ register_freshes runiverse n' in
14      〈r::res,runiverse〉 ].
15
16definition choose_rest ≝
17  λA: Type[0].
18  λleft, right: list A.
19  λprfl: 0 < |left|.
20  λprfr: 0 < |right|.
21  match left return λx. 0 < |x| → list A with
22  [ nil ⇒ λnil_prf.
23    match right return λx. 0 < |x| → list A with
24    [ nil ⇒ λnil_nil_absrd. ?
25    | _ ⇒ λnil_cons_prf. right
26    ] prfr
27  | _ ⇒ λcons_prf. right
28  ] prfl.
29  normalize in nil_prf;
30  cases(not_le_Sn_O 0)
31  #HYP
32  cases(HYP nil_prf)
33qed.
34
35definition complete_regs ≝
36  λglobals.
37  λdef.
38  λsrcrs1.
39  λsrcrs2.
40  if leb (length … srcrs2) (length … srcrs1) then
41   let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs1) (length ? srcrs2)) in
42    〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
43  else
44   let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs2) (length ? srcrs1)) in
45    〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
46
47lemma complete_regs_length:
48  ∀globals,def,left,right.
49   |\fst (\fst (complete_regs globals def left right))| = |\snd (\fst (complete_regs globals def left right))|.
50 #globals #def #left #right
51 whd in match complete_regs normalize nodelta
52 @leb_elim normalize nodelta #H
53 [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right)))
54 | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)))]
55 cases (fresh_regs ????) #def' #fresh normalize >append_length
56 generalize in match H -H;
57 generalize in match (length … left) generalize in match (length … right) generalize in match (length … fresh)
58 [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H) -H #H #E >E >commutative_plus
59         <plus_minus_m_m /2/ ]
60qed.
61
62definition size_of_sig_type ≝
63  λsig.
64  match sig with
65  [ ASTint isize sign ⇒
66    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
67      isize' ÷ (nat_of_bitvector ? int_size)
68  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
69  | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
70  ].
71  cases not_implemented;
72qed.
73
74inductive register_type: Type[0] ≝
75  | register_int: register → register_type
76  | register_ptr: register → register → register_type.
77
78definition local_env ≝ BitVectorTrie (list register) 16.
79
80definition mem_local_env : register → local_env → bool ≝
81  λr. member … (word_of_identifier … r).
82
83definition add_local_env : register → list register → local_env → local_env ≝
84  λr. insert … (word_of_identifier … r).
85
86definition find_local_env : register → local_env → list register ≝
87  λr: register.λbvt. lookup … (word_of_identifier … r) bvt [].
88
89definition initialize_local_env_internal ≝
90  λlenv_runiverse.
91  λr_sig.
92  let 〈lenv,runiverse〉 ≝ lenv_runiverse in
93  let 〈r, sig〉 ≝ r_sig in
94  let size ≝ size_of_sig_type sig in
95  let 〈rs,runiverse〉 ≝ register_freshes runiverse size in
96    〈add_local_env r rs lenv,runiverse〉.
97
98definition initialize_local_env ≝
99  λruniverse.
100  λregisters.
101  λresult.
102  let registers ≝ registers @
103    match result with
104    [ None ⇒ [ ]
105    | Some rt ⇒ [ rt ]
106    ]
107  in
108    foldl ? ? initialize_local_env_internal 〈Stub …,runiverse〉 registers.
109
110definition map_list_local_env_internal ≝
111  λlenv,res,r. res @ (find_local_env r lenv).
112   
113definition map_list_local_env ≝
114  λlenv,regs. foldl … (map_list_local_env_internal lenv) [ ] regs.
115
116definition make_addr ≝
117  λA.
118  λlst: list A.
119  λprf: 2 ≤ length A lst.
120  match lst return λx. 2 ≤ |x| → A × A with
121  [ nil ⇒ λlst_nil_prf. ?
122  | cons hd tl ⇒ λprf.
123    match tl return λx. 1 ≤ |x| → A × A with
124    [ nil ⇒ λtl_nil_prf. ?
125    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
126    ] ?
127  ] prf.
128  [1: normalize in lst_nil_prf;
129      cases(not_le_Sn_O 1);
130      #HYP cases(HYP lst_nil_prf)
131  |2: normalize in prf;
132      @le_S_S_to_le
133      assumption
134  |3: normalize in tl_nil_prf;
135      cases(not_le_Sn_O 0)
136      #HYP cases(HYP tl_nil_prf)]
137qed.
138
139definition find_and_addr ≝
140  λr,lenv. make_addr ? (find_local_env r lenv).
141
142definition rtl_args ≝
143  λregs_list,lenv. flatten … (map … (λr. find_local_env r lenv) regs_list).
144
145definition translate_cst_int_internal ≝
146  λglobals,dest_lbl,r,i. joint_st_sequential rtl_params_ globals (joint_instr_int … r i) dest_lbl.
147
148(*CSC: XXXXX *)
149axiom translate_cst:
150  ∀globals.
151  ∀cst: constant.
152  ∀destrs: list register.
153  ∀start_lbl: label.
154  ∀dest_lbl: label.
155  ∀def: rtl_internal_function globals.
156    rtl_internal_function globals.
157
158definition translate_move_internal ≝
159  λglobals.
160  λstart_lbl: label.
161  λdestr: register.
162  λsrcr: register.
163    joint_st_sequential rtl_params_ globals (joint_instr_move … 〈destr,srcr〉) start_lbl.
164
165definition translate_move ≝
166  λglobals.
167  λdestrs: list register.
168  λsrcrs: list register.
169  λstart_lbl: label.
170    match reduce_strong register register destrs srcrs with
171    [ dp crl_crr len_proof ⇒
172      let commonl ≝ \fst (\fst crl_crr) in
173      let commonr ≝ \fst (\snd crl_crr) in
174      let restl ≝ \snd (\fst crl_crr) in
175      let restr ≝ \snd (\snd crl_crr) in
176      let f_common ≝ translate_move_internal globals start_lbl in
177      let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in
178      let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
179        add_translates … [ translate1 ; translate2 ] start_lbl
180    ].
181    @len_proof
182qed.
183
184let rec make
185  (A: Type[0]) (elt: A) (n: nat) on n ≝
186  match n with
187  [ O ⇒ [ ]
188  | S n' ⇒ elt :: make A elt n'
189  ].
190 
191lemma make_length:
192  ∀A: Type[0].
193  ∀elt: A.
194  ∀n: nat.
195    n = length ? (make A elt n).
196  #A #ELT #N
197  elim N
198  [ normalize %
199  | #N #IH
200    normalize <IH %
201  ]
202qed.
203
204definition translate_cast_unsigned ≝
205  λglobals.
206  λdestrs.
207  λstart_lbl.
208  λdest_lbl.
209  λdef: joint_internal_function … (rtl_params globals).
210  let 〈def, tmp_zero〉 ≝ fresh_reg … def in
211  let zeros ≝ make … tmp_zero (length … destrs) in
212    add_translates … [
213      adds_graph rtl_params1 … [
214        joint_st_sequential rtl_params_ … (joint_instr_int rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl
215        ];
216      translate_move globals destrs zeros
217    ] start_lbl dest_lbl def.
218
219(*
220definition translate_cast_signed ≝
221  λglobals.
222  λdestrs.
223  λsrcr.
224  λstart_lbl.
225  λdest_lbl.
226  λdef.
227  let 〈def, tmp_128〉 ≝ fresh_reg … def in
228  let 〈def, tmp_255〉 ≝ fresh_reg … def in
229  let 〈def, tmpr〉 ≝ fresh_reg … def in
230  let 〈def, dummy〉 ≝ fresh_reg … def in
231  let insts ≝ [
232    rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl;
233    rtl_st_op2 And tmpr tmp_128 srcr start_lbl;
234    rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl;
235    rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl;
236    rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl
237  ] in
238  let srcrs ≝ make … tmpr (length … destrs) in
239    add_translates … [
240      adds_graph … insts;
241      translate_move destrs srcrs
242    ] start_lbl dest_lbl def.
243
244definition translate_cast ≝
245  λsrc_size.
246  λsrc_sign.
247  λdest_size.
248  λdestrs.
249  λsrcrs.
250  match |srcrs| return λx. |srcrs| = x → ? with
251  [ O ⇒ λzero_prf. adds_graph [ ]
252  | S n' ⇒ λsucc_prf.
253    if ltb dest_size src_size then
254      translate_move destrs srcrs
255    else
256      match reduce_strong register register destrs srcrs with
257      [ dp crl len_proof ⇒
258        let commonl ≝ \fst (\fst crl) in
259        let commonr ≝ \fst (\snd crl) in
260        let restl ≝ \snd (\fst crl) in
261        let restr ≝ \snd (\snd crl) in
262        let insts_common ≝ translate_move commonl commonr in
263        let sign_reg ≝ last_safe ? srcrs ? in
264        let insts_sign ≝
265          match src_sign with
266          [ Unsigned ⇒ translate_cast_unsigned restl
267          | Signed ⇒ translate_cast_signed restl sign_reg
268          ]
269        in
270          add_translates [ insts_common; insts_sign ]
271      ]
272  ] (refl ? (|srcrs|)).
273  >succ_prf //
274qed.
275
276definition translate_negint ≝
277  λdestrs.
278  λsrcrs.
279  λstart_lbl.
280  λdest_lbl.
281  λdef.
282  λprf: | destrs | = | srcrs |. (* assert in caml code *)
283  let 〈def, tmpr〉 ≝ fresh_reg def in
284  let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
285  let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in
286  let insts_init ≝ [
287    rtl_st_set_carry start_lbl;
288    rtl_st_int tmpr (zero ?) start_lbl
289  ] in
290  let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lbl in
291  let insts_add ≝ map … f_add destrs in
292    adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
293
294definition translate_notbool ≝
295  λdestrs.
296  λsrcrs.
297  λstart_lbl.
298  λdest_lbl.
299  λdef.
300  match destrs with
301  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
302  | cons destr destrs ⇒
303    let 〈def, tmpr〉 ≝ fresh_reg def in
304    let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in
305    let save_srcrs ≝ translate_move tmp_srcrs srcrs in
306    let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lbl in
307    let f ≝ λtmp_srcr. [
308      rtl_st_clear_carry start_lbl;
309      rtl_st_int tmpr (zero ?) start_lbl;
310      rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl;
311      rtl_st_int tmpr (zero ?) start_lbl;
312      rtl_st_op2 Addc tmpr tmpr tmpr start_lbl;
313      rtl_st_op2 Xor destr destr tmpr start_lbl
314    ] in
315    let insts ≝ init_destr :: (flatten ? (map … f tmp_srcrs)) in
316    let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in
317      add_translates [
318        save_srcrs; adds_graph insts; epilogue
319      ] start_lbl dest_lbl def
320  ].
321
322(* TODO: examine this properly.  This is a change from the O'caml code due
323   to us dropping the explicit use of a cast destination size field.  We
324   instead infer the size of the cast's destination from the context.  Is
325   this correct?
326*)
327definition translate_op1 ≝
328  λop1: unary_operation.
329  λdestrs: list register.
330  λsrcrs: list register.
331  λprf: |destrs| = |srcrs|.
332  λstart_lbl: label.
333  λdest_lbl: label.
334  λdef: rtl_internal_function.
335  match op1 with
336  [ Ocastint src_sign src_size ⇒
337    let dest_size ≝ |destrs| * 8 in
338    let src_size ≝ bitsize_of_intsize src_size in
339      translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
340  | Onegint ⇒
341      translate_negint destrs srcrs start_lbl dest_lbl def prf
342  | Onotbool ⇒
343      translate_notbool destrs srcrs start_lbl dest_lbl def
344  | Onotint ⇒
345    let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
346    let l ≝ map2 … f destrs srcrs prf in
347      adds_graph l start_lbl dest_lbl def
348  | Optrofint r ⇒
349      translate_move destrs srcrs start_lbl dest_lbl def
350  | Ointofptr r ⇒
351      translate_move destrs srcrs start_lbl dest_lbl def
352  | Oid ⇒
353      translate_move destrs srcrs start_lbl dest_lbl def
354  | _ ⇒ ? (* float operations implemented in runtime *)
355  ].
356  cases not_implemented
357qed.
358 
359definition translate_op ≝
360  λop.
361  λdestrs.
362  λsrcrs1.
363  λsrcrs2.
364  λstart_lbl.
365  λdest_lbl.
366  λdef.
367  match reduce_strong register register srcrs1 srcrs2 with
368  [ dp reduced first_reduced_proof ⇒
369    let srcrsl_common ≝ \fst (\fst reduced) in
370    let srcrsr_common ≝ \fst (\snd reduced) in
371    let srcrsl_rest ≝ \snd (\fst reduced) in
372    let srcrsr_rest ≝ \snd (\snd reduced) in
373    let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ? in
374    match reduce_strong register register destrs srcrsl_common with
375    [ dp reduced second_reduced_proof ⇒
376      let destrs_common ≝ \fst (\fst reduced) in
377      let destrs_rest ≝ \snd (\fst reduced) in
378      match reduce_strong register register destrs_rest srcrs_rest with
379      [ dp reduced third_reduced_proof ⇒
380        let destrs_cted ≝ \fst (\fst reduced) in
381        let destrs_rest ≝ \snd (\fst reduced) in
382        let srcrs_cted ≝ \fst (\snd reduced) in
383        let 〈def, tmpr〉 ≝ fresh_reg def in
384        let insts_init ≝ [
385          rtl_st_clear_carry start_lbl;
386          rtl_st_int tmpr (zero ?) start_lbl
387        ] in
388        let f_add ≝ λdestr. λsrcr1. λsrcr2. rtl_st_op2 op destr srcr1 srcr2 start_lbl in
389        let insts_add ≝ map3 … f_add destrs_common srcrsl_common srcrsr_common ? ? in
390        let f_add_cted ≝ λdestr. λsrcr. rtl_st_op2 op destr srcr tmpr start_lbl in
391        let insts_add_cted ≝ map2 ? ? ? f_add_cted destrs_cted srcrs_cted ? in
392        let f_rest ≝ λdestr. rtl_st_op2 op destr tmpr tmpr start_lbl in
393        let insts_rest ≝ map … f_rest destrs_rest in
394          adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
395      ]
396    ]
397  ].
398  [1: @third_reduced_proof
399  |3: @first_reduced_proof
400  |*: cases daemon (* TODO *)
401  ]
402qed.
403
404let rec translate_mul1
405  (dummy: register) (tmpr: register) (destrs: list register)
406  (srcrs1: list register) (srcr2: register) (start_lbl: label)
407    on srcrs1 ≝
408  match destrs with
409  [ nil ⇒ adds_graph [ rtl_st_skip start_lbl ] start_lbl
410  | cons destr tl ⇒
411    match tl with
412    [ nil ⇒
413      match srcrs1 with
414      [ nil ⇒
415        adds_graph [
416          rtl_st_int tmpr (zero ?) start_lbl;
417          rtl_st_op2 Addc destr destr tmpr start_lbl
418        ] start_lbl
419      | cons srcr1 tl' ⇒
420        adds_graph [
421          rtl_st_opaccs Mul tmpr dummy srcr2 srcr1 start_lbl;
422          rtl_st_op2 Addc destr destr tmpr start_lbl
423        ] start_lbl
424      ]
425    | cons destr2 destrs ⇒
426      match srcrs1 with
427      [ nil ⇒
428        add_translates [
429          adds_graph [
430            rtl_st_int tmpr (zero ?) start_lbl;
431            rtl_st_op2 Addc destr destr tmpr start_lbl;
432            rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
433          ];
434          translate_cst (Ointconst I8 (zero ?)) destrs
435        ] start_lbl
436      | cons srcr1 srcrs1 ⇒
437        match destrs with
438        [ nil ⇒
439          add_translates [
440            adds_graph [
441              rtl_st_int tmpr (zero ?) start_lbl;
442              rtl_st_op2 Addc destr destr tmpr start_lbl;
443              rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
444            ];
445            translate_cst (Ointconst I8 (zero ?)) destrs
446          ] start_lbl
447        | cons destr2 destrs ⇒
448          add_translates [
449            adds_graph [
450              rtl_st_opaccs Mul tmpr destr2 srcr2 srcr1 start_lbl;
451              rtl_st_op2 Addc destr destr tmpr start_lbl
452            ];
453            translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2
454          ] start_lbl
455        ]
456      ]
457    ]
458  ].
459
460definition translate_muli ≝
461  λdummy: register.
462  λtmpr: register.
463  λdestrs: list register.
464  λtmp_destrs: list register.
465  λsrcrs1: list register.
466  λdummy_lbl: label.
467  λi: nat.
468  λi_prf.
469  λtranslates: list ?.
470  λsrcr2i: register.
471  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split ? tmp_destrs i i_prf in
472  let tmp_destrs2' ≝
473    match tmp_destrs2 with
474    [ nil ⇒ [ ]
475    | cons tmp_destr2 tmp_destrs2 ⇒ [
476        adds_graph [
477          rtl_st_clear_carry dummy_lbl;
478          rtl_st_int tmp_destr2 (zero ?) dummy_lbl
479        ];
480        translate_mul1 dummy tmpr tmp_destrs2 srcrs1 srcr2i;
481        translate_cst (Ointconst I8 (zero ?)) tmp_destrs1;
482        adds_graph [
483          rtl_st_clear_carry dummy_lbl
484        ];
485        translate_op Addc destrs destrs tmp_destrs
486      ]
487    ]
488  in
489    translates @ tmp_destrs2'.
490
491axiom translate_mul:
492  ∀destrs: list register.
493  ∀srcrs1: list register.
494  ∀srcrs2: list register.
495  ∀start_lbl: label.
496  ∀dest_lbl: label.
497  ∀def: rtl_internal_function.
498    rtl_internal_function.
499
500(*
501definition translate_mul ≝
502  λdestrs: list register.
503  λsrcrs1: list register.
504  λsrcrs2: list register.
505  λstart_lbl: label.
506  λdest_lbl: label.
507  λdef: rtl_internal_function.
508  let 〈def, dummy〉 ≝ fresh_reg def in
509  let 〈def, tmpr〉 ≝ fresh_reg def in
510  let 〈def, tmp_destrs〉 ≝ fresh_regs def (|destrs|) in
511  let 〈def, fresh_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
512  let 〈def, fresh_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
513  let insts_init ≝ [
514    translate_move fresh_srcrs1 srcrs1;
515    translate_move fresh_srcrs2 srcrs2;
516    translate_cst (Ointconst I8 (zero ?)) destrs
517  ]
518  in
519  let f ≝ λi. translate_muli dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in
520  let insts_mul ≝ foldi ? ? [ ] srcrs2 in ?. [5: check insts_init.
521    add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
522*)
523
524definition translate_divumodu8 ≝
525  λorder: bool.
526  λdestrs: list register.
527  λsrcr1: register.
528  λsrcr2: register.
529  λstart_lbl: label.
530  λdest_lbl: label.
531  λdef: rtl_internal_function.
532  match destrs with
533  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
534  | cons destr destrs ⇒
535    let 〈def, dummy〉 ≝ fresh_reg def in
536    let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉 | _ ⇒ 〈dummy, destr〉 ] in
537    let inst_div ≝ adds_graph [
538      rtl_st_opaccs DivuModu destr1 destr2 srcr1 srcr2 start_lbl
539    ]
540    in
541    let insts_rest ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
542      add_translates [ inst_div; insts_rest ] start_lbl dest_lbl def
543  ].
544
545definition translate_ne: ? → ? → ? → ? → ? → ? → rtl_internal_function ≝
546  λdestrs: list register.
547  λsrcrs1: list register.
548  λsrcrs2: list register.
549  λstart_lbl: label.
550  λdest_lbl: label.
551  λdef: rtl_internal_function.
552  match destrs with
553  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
554  | cons destr destrs ⇒
555    let 〈def, tmpr〉 ≝ fresh_reg def in
556    let 〈def, tmp_zero〉 ≝ fresh_reg def in
557    let 〈def, tmp_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
558    let save_srcrs1 ≝ translate_move tmp_srcrs1 srcrs1 in
559    let 〈def, tmp_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
560    let save_srcrs2 ≝ translate_move tmp_srcrs2 srcrs2 in
561    match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
562    [ dp crl their_proof ⇒
563      let commonl ≝ \fst (\fst crl) in
564      let commonr ≝ \fst (\snd crl) in
565      let restl ≝ \snd (\snd crl) in
566      let restr ≝ \snd (\snd crl) in
567      let rest ≝ choose_rest ? restl restr ? ? in
568      let inits ≝ [
569        rtl_st_int destr (zero ?) start_lbl;
570        rtl_st_int tmp_zero (zero ?) start_lbl
571      ]
572      in
573      let f_common ≝ λtmp_srcr1. λtmp_srcr2. [
574        rtl_st_clear_carry start_lbl;
575        rtl_st_op2 Sub tmpr tmp_srcr1 tmp_srcr2 start_lbl;
576        rtl_st_op2 Or destr destr tmpr start_lbl
577      ]
578      in
579      let insts_common ≝ flatten ? (map2 … f_common commonl commonr ?) in
580      let f_rest ≝ λtmp_srcr. [
581        rtl_st_clear_carry start_lbl;
582        rtl_st_op2 Sub tmpr tmp_zero tmp_srcr start_lbl;
583        rtl_st_op2 Or destr destr tmpr start_lbl
584      ]
585      in
586      let insts_rest ≝ flatten ? (map ? ? f_rest rest) in
587      let insts ≝ inits @ insts_common @ insts_rest in
588      let epilogue ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
589        add_translates [
590          save_srcrs1; save_srcrs2; adds_graph insts; epilogue
591        ] start_lbl dest_lbl def
592    ]
593  ].
594  [1: @their_proof
595  |*: cases not_implemented (* choose rest requires non-emptiness proofs but
596                               these appear impossible to obtain, similar proof
597                               to above *)
598  ]
599qed.
600
601definition translate_eq_reg ≝
602  λtmp_zero: register.
603  λtmp_one: register.
604  λtmpr1: register.
605  λtmpr2: register.
606  λdestr: register.
607  λdummy_lbl: label.
608  λsrcr12: register × register.
609  let 〈srcr1, srcr2〉 ≝ srcr12 in
610  [ rtl_st_clear_carry dummy_lbl;
611    rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
612    rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
613    rtl_st_op2 Sub tmpr2 srcr2 srcr1 dummy_lbl;
614    rtl_st_op2 Addc tmpr2 tmp_zero tmp_zero dummy_lbl;
615    rtl_st_op2 Or tmpr1 tmpr1 tmpr2 dummy_lbl;
616    rtl_st_op2 Xor tmpr1 tmpr1 tmp_one dummy_lbl;
617    rtl_st_op2 And destr destr tmpr1 dummy_lbl ].
618
619definition translate_eq_list ≝
620  λtmp_zero: register.
621  λtmp_one: register.
622  λtmpr1: register.
623  λtmpr2: register.
624  λdestr: register.
625  λleq: list (register × register).
626  λdummy_lbl: label.
627  let f ≝ translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
628    (rtl_st_int destr (bitvector_of_nat ? 1) dummy_lbl) ::
629      flatten ? (map ? ? f leq).
630
631definition translate_atom ≝
632  λtmp_zero: register.
633  λtmp_one: register.
634  λtmpr1: register.
635  λtmpr2: register.
636  λtmpr3: register.
637  λdestr: register.
638  λdummy_lbl: label.
639  λleq: list (register × register).
640  λsrcr1: register.
641  λsrcr2: register.
642    translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
643    [ rtl_st_clear_carry dummy_lbl;
644      rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
645      rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
646      rtl_st_op2 And tmpr3 tmpr3 tmpr1 dummy_lbl;
647      rtl_st_op2 Or destr destr tmpr3 dummy_lbl ].
648
649definition translate_lt_main ≝
650  λtmp_zero: register.
651  λtmp_one: register.
652  λtmpr1: register.
653  λtmpr2: register.
654  λtmpr3: register.
655  λdestr: register.
656  λdummy_lbl: label.
657  λsrcrs1: list register.
658  λsrcrs2: list register.
659  λproof: |srcrs1| = |srcrs2|.
660  let f ≝ λinsts_leq. λsrcr1. λsrcr2.
661    let 〈insts, leq〉 ≝ insts_leq in
662    let added_insts ≝ translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
663      〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉
664  in
665    \fst (fold_left2 ? ? ? f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).
666
667definition fresh_regs_strong:
668  rtl_internal_function → ∀n: nat. Σfresh: rtl_internal_function × (list register). |\snd fresh| = n ≝
669  λdef.
670  λn.
671    fresh_regs def n.
672  @fresh_regs_length
673qed.
674
675definition complete_regs_strong:
676  rtl_internal_function → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
677  λdef.
678  λleft.
679  λright.
680    complete_regs def left right.
681  @complete_regs_length
682qed.
683
684definition translate_lt ≝
685  λdestrs: list register.
686  λprf_destrs: lt 0 (|destrs|).
687  λsrcrs1: list register.
688  λsrcrs2: list register.
689  λstart_lbl: label.
690  λdest_lbl: label.
691  λdef: rtl_internal_function.
692  match destrs with
693  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
694  | _ ⇒
695    match fresh_regs_strong def (|destrs|) with
696    [ dp def_tmp_destrs tmp_destrs_proof ⇒
697      let def ≝ \fst def_tmp_destrs in
698      let tmp_destrs ≝ \snd def_tmp_destrs in
699      let tmp_destr ≝ hd_safe ? tmp_destrs ? in
700      let 〈def, tmp_zero〉 ≝ fresh_reg def in
701      let 〈def, tmp_one〉 ≝ fresh_reg def in
702      let 〈def, tmpr1〉 ≝ fresh_reg def in
703      let 〈def, tmpr2〉 ≝ fresh_reg def in
704      let 〈def, tmpr3〉 ≝ fresh_reg def in
705      match complete_regs_strong def srcrs1 srcrs2 with
706      [ dp srcrs12_added srcrs12_proof ⇒
707        let srcrs1 ≝ \fst (\fst srcrs12_added) in
708        let srcrs2 ≝ \snd (\fst srcrs12_added) in
709        let added ≝ \snd srcrs12_added in
710        let srcrs1' ≝ rev ? srcrs1 in
711        let srcrs2' ≝ rev ? srcrs2 in
712        let insts_init ≝ [
713          translate_cst (Ointconst I8 (zero ?)) tmp_destrs;
714          translate_cst (Ointconst I8 (zero ?)) added;
715          adds_graph [
716            rtl_st_int tmp_zero (zero ?) start_lbl;
717            rtl_st_int tmp_one (bitvector_of_nat ? 1) start_lbl
718          ]
719        ]
720        in
721        let insts_main ≝
722          translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
723          let insts_main ≝ [ adds_graph insts_main ] in
724          let insts_exit ≝ [ translate_move destrs tmp_destrs ] in
725            add_translates (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
726      ]
727    ]
728  ].
729  [2: >tmp_destrs_proof @prf_destrs
730  |1: normalize nodelta
731      generalize in match srcrs12_proof
732      #HYP >rev_length >rev_length @HYP
733  ]
734qed.
735
736definition add_128_to_last ≝
737  λtmp_128: register.
738  λrs.
739  λprf: 0 < |rs|.
740  λstart_lbl: label.
741  match rs with
742  [ nil ⇒ adds_graph [ ] start_lbl
743  | _ ⇒
744    let r ≝ last_safe ? rs prf in
745      adds_graph [
746        rtl_st_op2 Add r r tmp_128 start_lbl
747      ] start_lbl
748  ].
749
750definition translate_lts ≝
751  λdestrs: list register.
752  λdestrs_prf: lt 0 (|destrs|).
753  λsrcrs1: list register.
754  λsrcrs2: list register.
755  λsrcrs1_lt_prf: 0 < |srcrs1|.
756  λsrcrs2_lt_prf: 0 < |srcrs2|.
757  λstart_lbl: label.
758  λdest_lbl: label.
759  λdef: rtl_internal_function.
760  match fresh_regs_strong def (|srcrs1|) with
761  [ dp def_tmp_srcrs1 srcrs1_prf ⇒
762    let def ≝ \fst def_tmp_srcrs1 in
763    let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
764    match fresh_regs_strong def (|srcrs2|) with
765    [ dp def_tmp_srcrs2 srcrs2_prf ⇒
766      let def ≝ \fst def_tmp_srcrs2 in
767      let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
768      let 〈def, tmp_128〉 ≝ fresh_reg def in
769        add_translates [
770          translate_move tmp_srcrs1 srcrs1;
771          translate_move tmp_srcrs2 srcrs2;
772          adds_graph [
773            rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl
774          ];
775          add_128_to_last tmp_128 tmp_srcrs1 ?;
776          add_128_to_last tmp_128 tmp_srcrs2 ?;
777          translate_lt destrs destrs_prf tmp_srcrs1 tmp_srcrs2
778        ] start_lbl dest_lbl def
779    ]
780  ].
781  [1: >srcrs1_prf @srcrs1_lt_prf
782  |2: >srcrs2_prf @srcrs2_lt_prf
783  ]
784qed.
785
786definition translate_op2 ≝
787  λop2.
788  λdestrs: list register.
789  λdestrs_prf: lt 0 (|destrs|).
790  λsrcrs1: list register.
791  λsrcrs2: list register.
792  λsrcrs1_prf: lt 0 (|srcrs1|). (* can this be relaxed? i think it can
793                                   but we need more dep. typ. in modu/divu
794                                   cases *)
795  λsrcrs2_prf: lt 0 (|srcrs2|).
796  λstart_lbl: label.
797  λdest_lbl: label.
798  λdef: rtl_internal_function.
799  match op2 with
800  [ Oadd ⇒
801    translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
802  | Oaddp ⇒
803    translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
804  | Osub ⇒
805    translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
806  | Osubpi ⇒
807    translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
808  | Osubpp sz ⇒
809    translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
810  | Omul ⇒
811    translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def
812  | Odivu ⇒
813    match srcrs1 return λx. 0 < |x| → rtl_internal_function with
814    [ cons hd tl ⇒ λcons_prf.
815      match tl with
816      [ nil ⇒ translate_divumodu8 true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
817      | _ ⇒ ? (* not implemented *)
818      ]
819    | nil ⇒ λnil_absrd. ?
820    ] srcrs1_prf
821  | Omodu ⇒
822    match srcrs1 return λx. 0 < |x| → rtl_internal_function with
823    [ cons hd tl ⇒ λcons_prf.
824      match tl with
825      [ nil ⇒ translate_divumodu8 false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
826      | _ ⇒ ? (* not implemented *)
827      ]
828    | nil ⇒ λnil_absrd. ?
829    ] srcrs1_prf
830  | Oand ⇒
831    translate_op And destrs srcrs1 srcrs2 start_lbl dest_lbl def
832  | Oor ⇒
833    translate_op Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
834  | Oxor ⇒
835    translate_op Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
836  | Ocmp c ⇒
837    match c with
838    [ Ceq ⇒
839      add_translates [
840        translate_ne destrs srcrs1 srcrs2;
841        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
842      ] start_lbl dest_lbl def
843    | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
844    | Clt ⇒ translate_lts destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def
845    | Cgt ⇒ translate_lts destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def
846    | Cle ⇒
847      add_translates [
848        translate_lts destrs destrs_prf srcrs2 srcrs1 ? ?;
849        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
850      ] start_lbl dest_lbl def
851    | Cge ⇒
852      add_translates [
853        translate_lts destrs destrs_prf srcrs1 srcrs2 ? ?;
854        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
855      ] start_lbl dest_lbl def
856    ]
857  | Ocmpu c ⇒
858    match c with
859    [ Ceq ⇒
860      add_translates [
861        translate_ne destrs srcrs1 srcrs2;
862        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
863      ] start_lbl dest_lbl def
864    | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
865    | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
866    | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
867    | Cle ⇒
868      add_translates [
869        translate_lt destrs destrs_prf srcrs2 srcrs1;
870        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
871      ] start_lbl dest_lbl def
872    | Cge ⇒
873      add_translates [
874        translate_lt destrs destrs_prf srcrs1 srcrs2;
875        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
876      ] start_lbl dest_lbl def
877    ]
878  | Ocmpp c ⇒
879    match c with
880    [ Ceq ⇒
881      add_translates [
882        translate_ne destrs srcrs1 srcrs2;
883        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
884      ] start_lbl dest_lbl def
885    | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
886    | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
887    | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
888    | Cle ⇒
889      add_translates [
890        translate_lt destrs destrs_prf srcrs2 srcrs1;
891        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
892      ] start_lbl dest_lbl def
893    | Cge ⇒
894      add_translates [
895        translate_lt destrs destrs_prf srcrs1 srcrs2;
896        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
897      ] start_lbl dest_lbl def
898    ]
899  | _ ⇒ ? (* assert false, implemented in run time or float op *)
900  ].
901  [ 2,6: normalize in nil_absrd;
902         cases(not_le_Sn_O 0)
903         #HYP cases(HYP nil_absrd)
904  | 3,7,12,17,13,15,18,19,20,21,14,16:
905         assumption
906  | *:   cases not_implemented (* yes, really *)
907  ]
908qed.
909
910definition translate_cond ≝
911  λsrcrs: list register.
912  λstart_lbl: label.
913  λlbl_true: label.
914  λlbl_false: label.
915  λdef: rtl_internal_function.
916  let 〈def, tmpr〉 ≝ fresh_reg def in
917  let 〈def, tmp_lbl〉 ≝ fresh_label def in
918  let init ≝ rtl_st_int tmpr (zero ?) start_lbl in
919  let f ≝ λsrcr. rtl_st_op2 Or tmpr tmpr srcr start_lbl in
920  let def ≝ adds_graph (init :: (map … f srcrs)) start_lbl tmp_lbl def in
921    add_graph tmp_lbl (rtl_st_cond tmpr lbl_true lbl_false) def. 
922
923definition translate_load ≝
924  λaddr.
925  λaddr_prf: 2 ≤ |addr|.
926  λdestrs: list register.
927  λstart_lbl: label.
928  λdest_lbl: label.
929  λdef: rtl_internal_function.
930  match fresh_regs_strong def (|addr|) with
931  [ dp def_save_addr save_addr_prf ⇒
932    let def ≝ \fst def_save_addr in
933    let save_addr ≝ \snd def_save_addr in
934    match fresh_regs_strong def (|addr|) with
935    [ dp def_tmp_addr tmp_addr_prf ⇒
936      let def ≝ \fst def_tmp_addr in
937      let tmp_addr ≝ \snd def_tmp_addr in
938      let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
939      let 〈def, tmpr〉 ≝ fresh_reg def in
940      let insts_save_addr ≝ translate_move save_addr addr in
941      let f ≝ λtranslates_off. λr.
942        let 〈translates, off〉 ≝ translates_off in
943        let translates ≝ translates @ [
944          adds_graph [
945            rtl_st_int tmpr off start_lbl
946          ];
947          translate_op2 Oaddp tmp_addr ? save_addr [tmpr] ? ?;
948          adds_graph [
949            rtl_st_load r tmp_addr1 tmp_addr2 dest_lbl
950          ]
951        ]
952        in
953        let 〈carry, result〉 ≝ half_add ? off int_size in
954          〈translates, result〉
955      in
956      let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], (zero ?)〉 destrs in
957        add_translates (insts_save_addr :: translates) start_lbl dest_lbl def
958    ]
959  ].
960  [1: normalize //
961  |2: >save_addr_prf normalize
962      @(transitive_le 1 2 (|addr|)) //
963  |3: >tmp_addr_prf normalize
964      @(transitive_le 1 2 (|addr|)) //
965  |*: >tmp_addr_prf assumption
966  ]
967qed.
968
969definition translate_store ≝
970  λaddr.
971  λaddr_prf: 2 ≤ |addr|.
972  λsrcrs: list register.
973  λstart_lbl: label.
974  λdest_lbl: label.
975  λdef: rtl_internal_function.
976  match fresh_regs_strong def (|addr|) with
977  [ dp def_tmp_addr tmp_addr_prf ⇒
978    let def ≝ \fst def_tmp_addr in
979    let tmp_addr ≝ \snd def_tmp_addr in
980    let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
981    let 〈def, tmpr〉 ≝ fresh_reg def in
982    let f ≝ λtranslate_off. λsrcr.
983      let 〈translates, off〉 ≝ translate_off in
984      let translates ≝ translates @ [
985        adds_graph [
986          rtl_st_int tmpr off start_lbl
987        ];
988        translate_op2 Oaddp tmp_addr ? addr [tmpr] ? ?;
989        adds_graph [
990          rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
991        ]
992      ]
993      in
994        let 〈carry, result〉 ≝ half_add ? off int_size in
995          〈translates, result〉
996    in
997    let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], zero ?〉 srcrs in
998      add_translates translates start_lbl dest_lbl def
999  ].
1000  [1: normalize //
1001  |2: >tmp_addr_prf normalize
1002      @(transitive_le 1 2 (|addr|)) //
1003  |3: >tmp_addr_prf normalize
1004      @(transitive_le 1 2 (|addr|)) //
1005  |*: >tmp_addr_prf assumption
1006  ]
1007qed.
1008*)
1009
1010definition translate_stmt ≝
1011  λglobals.
1012  λlenv: local_env.
1013  λlbl: label.
1014  λstmt.
1015  λdef: joint_internal_function … (rtl_params globals).
1016  match stmt with
1017  [ St_skip lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def
1018  | _ ⇒ ? ].
1019(*
1020  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
1021  | St_const destr cst lbl' ⇒
1022    translate_cst cst (find_local_env destr lenv) lbl lbl' def
1023  | St_op1 op1 destr srcr lbl' ⇒
1024    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) ? lbl lbl' def
1025  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
1026    translate_op2 op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
1027  | St_load ignore addr destr lbl' ⇒
1028    translate_load (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
1029  | St_store ignore addr srcr lbl' ⇒
1030    translate_store (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
1031  | St_call_id f args retr lbl' ⇒
1032    match retr with
1033    [ Some retr ⇒
1034      add_graph lbl (rtl_st_call_id f (rtl_args args lenv) (find_local_env retr lenv) lbl') def
1035    | None ⇒ add_graph lbl (rtl_st_call_id f (rtl_args args lenv) [ ] lbl') def
1036    ]
1037  | St_call_ptr f args retr lbl' ⇒
1038    match retr with
1039    [ None ⇒
1040      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1041        add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) [ ] lbl') def
1042    | Some retr ⇒
1043      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1044        add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv) lbl') def
1045    ]
1046  | St_tailcall_id f args ⇒
1047    add_graph lbl (rtl_st_tailcall_id f (rtl_args args lenv)) def
1048  | St_tailcall_ptr f args ⇒
1049    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1050      add_graph lbl (rtl_st_tailcall_ptr f1 f2 (rtl_args args lenv)) def
1051  | St_cond r lbl_true lbl_false ⇒
1052    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
1053  | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
1054  | St_return ⇒ add_graph lbl rtl_st_return def
1055  ].
1056  [10: cases not_implemented (* jtable case *)
1057  |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *)
1058  ]
1059*) cases daemon
1060qed.
1061
1062(* XXX: we use a "hack" here to circumvent the proof obligations required to
1063   create res, an empty internal_function record.  we insert into our graph
1064   the start and end nodes to ensure that they are in, and place dummy
1065   skip instructions at these nodes. *)
1066definition translate_internal ≝
1067  λglobals,def.
1068  let runiverse ≝ f_reggen def in
1069  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
1070    (f_params def @ f_locals def) (f_result def) in
1071  let params ≝ map_list_local_env lenv (map ? ? \fst (f_params def)) in
1072  let locals ≝ map_list_local_env lenv (map ? ? \fst (f_locals def)) in
1073  let result ≝
1074    match (f_result def) with
1075    [ None ⇒ [ ]
1076    | Some r_typ ⇒
1077      let 〈r, typ〉 ≝ r_typ in
1078        find_local_env r lenv
1079    ]
1080  in
1081  let luniverse' ≝ f_labgen def in
1082  let runiverse' ≝ runiverse in
1083  let result' ≝ result in
1084  let params' ≝ params in
1085  let locals' ≝ locals in
1086  let stack_size' ≝ f_stacksize def in
1087  let entry' ≝ f_entry def in
1088  let exit' ≝ f_exit def in
1089  let graph' ≝ add … (empty_map ? ?) entry' (joint_st_goto … entry') in
1090  let graph' ≝ add … graph' exit' (joint_st_goto … exit') in
1091  let res ≝
1092    mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
1093     locals' stack_size' graph' ? ? in
1094    foldi … (translate_stmt … lenv) (f_graph def) res.
1095[ % [@entry' | @graph_add_lookup @graph_add]
1096| % [@exit'  | @graph_add]]
1097qed.
1098
1099(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
1100  because of CompCert heritage *)
1101definition rtlabs_to_rtl : RTLabs_program → rtl_program ≝
1102 λp. transform_program ??? p (transf_fundef … (translate_internal (prog_var_names …))).
Note: See TracBrowser for help on using the repository browser.