source: src/RTLabs/RTLAbstoRTL.ma @ 1296

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

changes

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