source: src/RTLabs/RTLAbstoRTL.ma @ 1285

Last change on this file since 1285 was 1285, checked in by mulligan, 8 years ago

more implementation on maps, final push to get rtl abs to rtl working

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