source: src/RTLabs/RTLabsToRTL.ma @ 1331

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

some changes, but i now have two contradictory proof obligations.

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