source: src/RTLabs/RTLAbstoRTL.ma @ 1280

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

Some progress in the porting of RTLAbstoRTL to the joint syntax:

1) common code with RTLtoERTL factorized out in joint/TranslateUtils.ma
2) this required yet another refactoring of the parameters in Joint.ma
3) RTLtoERTL ported to the new parameters; LTLtoLIN and LINtoASM are

probably broken but easily fixable a.t.m. RTLAbstoRTL still in progress,
but the difficult part is almost done.

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