source: src/RTLabs/RTLAbstoRTL.ma @ 1287

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

about 3/4 of the way through rtlabs to rtl now

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