source: src/RTLabs/RTLAbstoRTL.ma @ 1307

Last change on this file since 1307 was 1307, checked in by mulligan, 9 years ago

adding translate_cst

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