source: src/RTLabs/RTLAbstoRTL.ma @ 1283

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

Bad programming practice removed: change_label is no longer required and
add_graph now takes function from label to statements in place of taking
statements containing a wrong label to be fixed.

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