Changeset 2286 for src/RTL/RTLToERTL.ma
 Timestamp:
 Aug 2, 2012, 3:18:11 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLToERTL.ma
r2103 r2286 7 7 include alias "basics/lists/list.ma". 8 8 9 definition save_hdws ≝ 10 λglobals,l. 9 definition ertl_fresh_reg: 10 ∀globals.freshT ERTL globals register ≝ 11 λglobals,def. 12 let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in 13 〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉. 14 15 definition save_hdws : 16 ∀globals.list (register×Register) → list (joint_seq ERTL globals) ≝ 17 λglobals. 11 18 let save_hdws_internal ≝ 12 λdestr_srcr.λstart_lbl. 13 let 〈destr, srcr〉 ≝ destr_srcr in 14 adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈pseudo destr,hardware srcr〉) ] start_lbl 15 in 16 map ? ? save_hdws_internal l. 17 18 definition restore_hdws ≝ 19 λglobals,l. 19 λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in 20 map ?? save_hdws_internal. 21 22 definition restore_hdws : 23 ∀globals.list (psd_argument×Register) → list (joint_seq ERTL globals) ≝ 24 λglobals. 20 25 let restore_hdws_internal ≝ 21 λsrcr_destr: register × Register. 22 λstart_lbl: label. 23 let 〈srcr, destr〉 ≝ srcr_destr in 24 adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈hardware destr, pseudo srcr〉) ] start_lbl 25 in 26 map ? ? restore_hdws_internal l. 27 28 definition get_params_hdw ≝ 29 λglobals. 30 λparams: list register. 31 match params with 32 [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … ] start_lbl] 33  _ ⇒ 34 let l ≝ zip_pottier ? ? params RegisterParams in 35 save_hdws globals l ]. 36 37 definition get_param_stack ≝ 38 λglobals. 39 λoff: nat. 40 λdestr. 41 λstart_lbl, dest_lbl: label. 42 λdef. 43 let 〈def, addr1〉 ≝ fresh_reg … def in 44 let 〈def, addr2〉 ≝ fresh_reg … def in 45 let 〈def, tmpr〉 ≝ fresh_reg … def in 46 let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in 47 adds_graph ertl_params1 globals [ 48 sequential ertl_params_ … (extension … (ertl_st_ext_frame_size addr1)); 49 sequential ertl_params_ … (INT … tmpr int_offset); 50 sequential ertl_params_ … (OP2 … Sub addr1 addr1 tmpr); 51 sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉); 52 sequential ertl_params_ … (OP2 … Add addr1 addr1 tmpr); 53 sequential ertl_params_ … (INT … addr2 (bitvector_of_nat 8 0)); 54 sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉); 55 sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr); 56 sequential ertl_params_ … (LOAD … destr addr1 addr2) 57 ] start_lbl dest_lbl def. 58 59 definition get_params_stack ≝ 60 λglobals,params. 61 match params with 62 [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl ] 63  _ ⇒ mapi ? ? (get_param_stack globals) params ]. 26 λdestr_srcr:psd_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in 27 map ? ? restore_hdws_internal. 28 29 definition get_params_hdw : 30 ∀globals.list register → list (joint_seq ERTL globals) ≝ 31 λglobals,params. 32 save_hdws … (zip_pottier … params RegisterParams). 33 34 definition get_param_stack : 35 ∀globals.register → register → register → 36 list (joint_seq ERTL globals) ≝ 37 λglobals,addr1,addr2,destr. 38 (* liveness analysis will erase the last useless ops *) 39 [ LOAD ?? destr addr1 addr2 ; 40 addr1 ← addr1 .Add. (int_size : Byte) ; 41 addr2 ← addr2 .Addc. zero_byte 42 ]. 43 44 definition get_params_stack : 45 ∀globals.list register → 46 bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝ 47 λglobals,params. 48 νtmpr,addr1,addr2 in 49 let params_length_byte : Byte ≝ bitvector_of_nat ? (params) in 50 [ (ertl_frame_size tmpr : joint_seq ??) ; 51 CLEAR_CARRY ?? ; 52 tmpr ← tmpr .Sub. params_length_byte ; (* will be constant later *) 53 PSD addr1 ← HDW RegisterSPL ; 54 PSD addr2 ← HDW RegisterSPH ; 55 addr1 ← addr1 .Add. tmpr ; 56 addr2 ← addr2 .Addc. zero_byte ] @ 57 flatten … (map ?? (get_param_stack globals addr1 addr2) params). 64 58 65 59 definition get_params ≝ … … 67 61 let n ≝ min (length … params) (length … RegisterParams) in 68 62 let 〈hdw_params, stack_params〉 ≝ list_split … n params in 69 let hdw_params ≝ get_params_hdw globals hdw_params in 70 hdw_params @ (get_params_stack … stack_params). 71 72 definition add_prologue ≝ 73 λglobals. 74 λparams: list register. 75 λsral. 76 λsrah. 77 λsregs. 78 λdef. 79 let start_lbl ≝ joint_if_entry … (ertl_params globals) def in 80 let 〈tmp_lbl, def〉 ≝ fresh_label … def in 81 match lookup … (joint_if_code … def) start_lbl 82 return λx. x ≠ None ? → ertl_internal_function globals with 83 [ None ⇒ λnone_absrd. ⊥ 84  Some last_stmt ⇒ λsome_prf. 85 let def ≝ 86 add_translates … 87 ((adds_graph ertl_params1 … [ 88 sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame) 89 ]) :: 90 (adds_graph ertl_params1 … [ 91 sequential ertl_params_ … (POP … sral); 92 sequential ertl_params_ … (POP … srah) 93 ]) :: 94 (save_hdws … sregs) @ 95 (get_params … params)) 96 start_lbl tmp_lbl def 97 in 98 add_graph … tmp_lbl last_stmt def 99 ] ?. 100 [ cases start_lbl #x #H cases daemon (* @H *) (*CSC: XXXX, no Russell *) 101  cases (none_absrd) /2/ ] 102 qed. 103 104 definition save_return ≝ 105 λglobals. 106 λret_regs. 107 λstart_lbl: label. 108 λdest_lbl: label. 109 λdef: ertl_internal_function globals. 110 let 〈def, tmpr〉 ≝ fresh_reg … def in 63 get_params_hdw globals hdw_params @@ get_params_stack … stack_params. 64 65 definition prologue : 66 ∀globals.list register → register → register → list (register×Register) → 67 bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝ 68 λglobals,params,sral,srah,sregs. 69 [ (ertl_new_frame : joint_seq ??) ; 70 POP … sral ; 71 POP … srah 72 ] @@ save_hdws … sregs @@ get_params … params. 73 74 definition save_return : 75 ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝ 76 λglobals,ret_regs. 111 77 match reduce_strong ? ? RegisterSTS ret_regs with 112 78 [ mk_Sig crl crl_proof ⇒ … … 114 80 let commonr ≝ \fst (\snd crl) in 115 81 let restl ≝ \snd (\fst crl) in 116 let restr ≝ \snd (\snd crl) in 117 let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) in 118 let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) in 119 let saves ≝ map2 … f_save commonl commonr crl_proof in 120 let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) in 121 let defaults ≝ map … f_default restl in 122 adds_graph ertl_params1 ? (init_tmpr :: saves @ defaults) start_lbl dest_lbl def 123 ]. 124 125 definition assign_result ≝ 126 λglobals.λstart_lbl: label. 127 match reduce_strong ? ? RegisterRets RegisterSTS with 82 (* let restr ≝ \snd (\snd crl) in *) 83 map2 … (λst.λr : psd_argument.HDW st ← r) commonl commonr crl_proof @ 84 map … (λst.HDW st ← zero_byte) restl 85 ]. 86 87 definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝ 88 λglobals. 89 match reduce_strong ?? RegisterRets RegisterSTS with 128 90 [ mk_Sig crl crl_proof ⇒ 129 91 let commonl ≝ \fst (\fst crl) in 130 92 let commonr ≝ \fst (\snd crl) in 131 let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) in 132 let insts ≝ map2 ? ? ? f commonl commonr crl_proof in 133 adds_graph ertl_params1 … insts start_lbl 134 ]. 135 136 definition add_epilogue ≝ 137 λglobals. 138 λret_regs. 139 λsral. 140 λsrah. 141 λsregs. 142 λdef. 143 let start_lbl ≝ joint_if_exit … (ertl_params globals) def in 144 let 〈tmp_lbl, def〉 ≝ fresh_label … def in 145 match lookup … (joint_if_code … def) start_lbl 146 return λx. x ≠ None ? → ertl_internal_function globals with 147 [ None ⇒ λnone_absrd. ⊥ 148  Some last_stmt ⇒ λsome_prf. 149 let def ≝ 150 add_translates ertl_params1 … ( 151 [save_return globals ret_regs] @ 152 restore_hdws … sregs @ 153 [adds_graph ertl_params1 … [ 154 sequential ertl_params_ … (PUSH … srah); 155 sequential ertl_params_ … (PUSH … sral) 156 ]] @ 157 [adds_graph ertl_params1 … [ 158 sequential ertl_params_ … (extension … ertl_st_ext_del_frame) 159 ]] @ 160 [assign_result globals] 161 ) start_lbl tmp_lbl def 162 in 163 let def' ≝ add_graph … tmp_lbl last_stmt def in 164 set_joint_if_exit … tmp_lbl def' ? 165 ] ?. 166 [ cases start_lbl #x #H cases daemon (* @H *) (* CSC: XXXX *) 167  cases (none_absrd) /2/ 168  cases daemon (* CSC: XXXXX *) 169 ] 170 qed. 171 172 173 definition allocate_regs ≝ 174 λglobals. 175 λrs. 176 λsaved: rs_set rs. 177 λdef. 93 map2 … (λret,st.HDW ret ← HDW st) commonl commonr crl_proof 94 ]. 95 96 definition epilogue : 97 ∀globals.list register → register → register → list (register × Register) → 98 list (joint_seq ERTL globals) ≝ 99 λglobals,ret_regs,sral,srah,sregs. 100 save_return … (map … (Reg ?) ret_regs) @ 101 restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @ 102 [ PUSH ERTL ? srah ; 103 PUSH … sral ; 104 ertl_del_frame ] @ 105 assign_result globals. 106 107 definition allocate_regs : 108 ∀globals,rs.rs_set rs → 109 freshT ERTL globals (list (register×Register)) ≝ 110 λglobals,rs,saved,def. 178 111 let allocate_regs_internal ≝ 179 112 λr: Register. 180 113 λdef_sregs. 181 let 〈def, sregs〉 ≝ def_sregs in 182 let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in 183 〈def, 〈r', r〉 :: sregs〉 184 in 185 rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉. 186 187 definition add_pro_and_epilogue ≝ 188 λglobals. 189 λparams. 190 λret_regs. 191 λdef. 192 match fresh_regs_strong … globals def 2 with 193 [ mk_Sig def_sra def_sra_proof ⇒ 194 let def ≝ \fst def_sra in 195 let sra ≝ \snd def_sra in 196 let sral ≝ nth_safe ? 0 sra ? in 197 let srah ≝ nth_safe ? 1 sra ? in 198 let 〈def, sregs〉 ≝ allocate_regs … register_list_set RegisterCalleeSaved def in 199 let def ≝ add_prologue … params sral srah sregs def in 200 let def ≝ add_epilogue … ret_regs sral srah sregs def in 201 def 202 ]. 203 >def_sra_proof // 204 qed. 205 206 definition set_params_hdw ≝ 207 λglobals,params. 208 match params with 209 [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl] 210  _ ⇒ 211 let l ≝ zip_pottier ? ? params RegisterParams in 212 restore_hdws globals l 213 ]. 214 215 definition set_param_stack ≝ 216 λglobals. 217 λoff. 218 λsrcr. 219 λstart_lbl: label. 220 λdest_lbl: label. 221 λdef: ertl_internal_function globals. 222 let 〈def, addr1〉 ≝ fresh_reg … def in 223 let 〈def, addr2〉 ≝ fresh_reg … def in 224 let 〈def, tmpr〉 ≝ fresh_reg … def in 225 let 〈ignore, int_off〉 ≝ half_add ? off int_size in 226 adds_graph ertl_params1 … [ 227 sequential ertl_params_ … (INT … addr1 int_off); 228 sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉); 229 sequential ertl_params_ … (CLEAR_CARRY …); 230 sequential ertl_params_ … (OP2 … Sub addr1 tmpr addr1); 231 sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉); 232 sequential ertl_params_ … (INT … addr2 (zero ?)); 233 sequential ertl_params_ … (OP2 … Sub addr2 tmpr addr2); 234 sequential ertl_params_ … (STORE … addr1 addr2 srcr) 235 ] start_lbl dest_lbl def. 236 237 definition set_params_stack ≝ 238 λglobals,params. 239 match params with 240 [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO …] start_lbl] 241  _ ⇒ 242 let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in 243 mapi ? ? f params]. 114 let 〈def, r'〉 ≝ ertl_fresh_reg … (\fst def_sregs) in 115 〈def, 〈r', r〉::\snd def_sregs〉 in 116 rs_fold ?? allocate_regs_internal saved 〈def, [ ]〉. 117 118 definition add_pro_and_epilogue : 119 ∀globals.list register → list register → 120 joint_internal_function ERTL globals → 121 joint_internal_function ERTL globals ≝ 122 λglobals,params,ret_regs,def. 123 let start_lbl ≝ joint_if_entry … def in 124 let end_lbl ≝ joint_if_exit … def in 125 state_run … def ( 126 ! sral ← ertl_fresh_reg … ; 127 ! srah ← ertl_fresh_reg … ; 128 ! sregs ← allocate_regs … register_list_set RegisterCalleeSaved ; 129 ! prologue' ← bcompile … (ertl_fresh_reg …) (prologue … params sral srah sregs) ; 130 let epilogue' ≝ epilogue … ret_regs sral srah sregs in 131 ! def' ← state_get … ; 132 let def'' ≝ insert_prologue … prologue' def' in 133 return insert_epilogue … epilogue' def'' 134 ). 135 136 definition set_params_hdw : 137 ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝ 138 λglobals,params. 139 restore_hdws globals (zip_pottier ? ? params RegisterParams). 140 141 (* Paolo: The following can probably be done way more efficiently with INC DPTR *) 142 143 definition set_param_stack : 144 ∀globals.register → register → psd_argument → 145 list (joint_seq ERTL globals) ≝ 146 λglobals,addr1,addr2,arg. 147 [ STORE … addr1 addr2 arg ; 148 addr1 ← addr1 .Add. (int_size : Byte) ; 149 addr2 ← addr2 .Addc. zero_byte 150 ]. 151 152 definition set_params_stack : 153 ∀globals.list psd_argument → bind_new (localsT ERTL) ? ≝ 154 λglobals,params. 155 νaddr1,addr2 in 156 let params_length_byte : Byte ≝ bitvector_of_nat ? (params) in 157 [ PSD addr1 ← HDW RegisterSPL ; 158 PSD addr2 ← HDW RegisterSPH ; 159 CLEAR_CARRY ?? ; 160 addr1 ← addr1 .Sub. params_length_byte ; 161 addr2 ← addr2 .Sub. zero_byte 162 ] @ 163 flatten … (map … (set_param_stack globals addr1 addr2) params). 244 164 245 165 definition set_params ≝ … … 249 169 let hdw_params ≝ \fst hdw_stack_params in 250 170 let stack_params ≝ \snd hdw_stack_params in 251 set_params_hdw globals hdw_params @ set_params_stack globals stack_params. 252 253 definition fetch_result ≝ 254 λglobals. 255 λret_regs. 256 λstart_lbl: label. 257 match reduce_strong ? ? RegisterSTS RegisterRets with 258 [ mk_Sig crl first_crl_proof ⇒ 171 set_params_hdw globals hdw_params @@ set_params_stack globals stack_params. 172 173 definition fetch_result : 174 ∀globals.list register → list (joint_seq ERTL globals) ≝ 175 λglobals,ret_regs. 176 match reduce_strong ?? RegisterSTS RegisterRets with 177 [ mk_Sig crl crl_proof ⇒ 259 178 let commonl ≝ \fst (\fst crl) in 260 179 let commonr ≝ \fst (\snd crl) in 261 let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) in 262 let saves ≝ map2 ? ? ? f_save commonl commonr ? in 263 match reduce_strong ? ? ret_regs RegisterSTS with 264 [ mk_Sig crl second_crl_proof ⇒ 180 map2 … (λst,r.HDW st ← HDW r) commonl commonr crl_proof @ 181 match reduce_strong ?? ret_regs RegisterSTS with 182 [ mk_Sig crl crl_proof ⇒ 265 183 let commonl ≝ \fst (\fst crl) in 266 184 let commonr ≝ \fst (\snd crl) in 267 let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) in 268 let restores ≝ map2 ? ? ? f_restore commonl commonr ? in 269 adds_graph ertl_params1 … (saves @ restores) start_lbl]]. 270 [@second_crl_proof  @first_crl_proof] 271 qed. 272 273 definition translate_call_id ≝ 274 λglobals,f. 275 λargs. 276 λret_regs. 277 λstart_lbl. 278 λdest_lbl. 279 λdef. 280 let nb_args ≝ args in 281 add_translates ertl_params1 globals ( 282 set_params … args @ [ 283 adds_graph ertl_params1 … [ sequential ertl_params_ … (CALL_ID … f nb_args it) ]; 284 fetch_result … ret_regs 185 map2 … (λret,st.PSD ret ← HDW st) commonl commonr crl_proof 186 ] 187 ]. 188 189 definition translate_step : 190 ∀globals.label → joint_step RTL_ntc globals → 191 bind_seq_block ERTL globals (joint_step ERTL globals) ≝ 192 λglobals.λ_.λs. 193 match s return λ_.bind_seq_block ?? (joint_step ??) with 194 [ step_seq s ⇒ 195 match s return λ_.bind_seq_block ?? (joint_step ??) with 196 [ PUSH _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *) 197  POP _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *) 198  MOVE rs ⇒ PSD (\fst rs) ← \snd rs 199  COST_LABEL lbl ⇒ 200 COST_LABEL … lbl 201  ADDRESS x prf r1 r2 ⇒ 202 ADDRESS ERTL ? x prf r1 r2 203  OPACCS op destr1 destr2 srcr1 srcr2 ⇒ 204 OPACCS ERTL ? op destr1 destr2 srcr1 srcr2 205  OP1 op1 destr srcr ⇒ 206 OP1 ERTL ? op1 destr srcr 207  OP2 op2 destr srcr1 srcr2 ⇒ 208 OP2 ERTL ? op2 destr srcr1 srcr2 209  CLEAR_CARRY ⇒ 210 CLEAR_CARRY … 211  SET_CARRY ⇒ 212 SET_CARRY … 213  LOAD destr addr1 addr2 ⇒ 214 LOAD ERTL ? destr addr1 addr2 215  STORE addr1 addr2 srcr ⇒ 216 STORE ERTL ? addr1 addr2 srcr 217  COMMENT msg ⇒ 218 COMMENT … msg 219  extension_seq ext ⇒ 220 match ext with 221 [ rtl_stack_address addr1 addr2 ⇒ 222 [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ] 285 223 ] 286 ) start_lbl dest_lbl def. 287 288 definition translate_stmt : 289 ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals 290 ≝ 291 λglobals. 292 λlbl. 293 λstmt. 294 λdef. 295 match stmt with 296 [ GOTO lbl' ⇒ add_graph … lbl (GOTO … lbl') def 297  RETURN ⇒ add_graph … lbl (RETURN …) def 298  sequential seq lbl' ⇒ 299 match seq with 300 [ PUSH _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *) 301  POP _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *) 302  CALL_ID f args ret_regs ⇒ 303 translate_call_id … f args ret_regs lbl lbl' def 304  MOVE rs ⇒ 305 let 〈r1,r2〉 ≝ rs in 306 let rs ≝ 〈pseudo r1, pseudo r2〉 in 307 add_graph ertl_params1 ? lbl (sequential … (MOVE … rs) lbl') def 308  extension ext ⇒ 309 match ext with 310 [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *) 311  rtlntc_st_ext_stack_address r1 r2 ⇒ 312 adds_graph ertl_params1 … [ 313 sequential ertl_params_ … (MOVE … 〈pseudo r1, hardware RegisterSPL〉); 314 sequential ertl_params_ … (MOVE … 〈pseudo r2, hardware RegisterSPH〉) 315 ] lbl lbl' def] 316 (*CSC: everything is just copied to retype it from now on; 317 the problem is call_id that takes different parameters, but that is patternmatched 318 above. It could be made nicer at the cost of making all the rest of the code uglier *) 319  COST_LABEL cost_lbl ⇒ add_graph ertl_params1 … lbl (sequential … (COST_LABEL … cost_lbl) lbl') def 320  ADDRESS x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (sequential … (ADDRESS … x prf r1 r2) lbl') def 321  INT r i ⇒ add_graph ertl_params1 … lbl (sequential … (INT … r i) lbl') def 322  OPACCS op destr1 destr2 srcr1 srcr2 ⇒ 323 add_graph ertl_params1 … lbl (sequential … (OPACCS … op destr1 destr2 srcr1 srcr2) lbl') def 324  OP1 op1 destr srcr ⇒ 325 add_graph ertl_params1 … lbl (sequential … (OP1 … op1 destr srcr) lbl') def 326  OP2 op2 destr srcr1 srcr2 ⇒ 327 add_graph ertl_params1 … lbl (sequential … (OP2 … op2 destr srcr1 srcr2) lbl') def 328  CLEAR_CARRY ⇒ 329 add_graph ertl_params1 … lbl (sequential … (CLEAR_CARRY …) lbl') def 330  SET_CARRY ⇒ 331 add_graph ertl_params1 … lbl (sequential … (SET_CARRY …) lbl') def 332  LOAD destr addr1 addr2 ⇒ 333 add_graph ertl_params1 … lbl (sequential … (LOAD … destr addr1 addr2) lbl') def 334  STORE addr1 addr2 srcr ⇒ 335 add_graph ertl_params1 … lbl (sequential … (STORE … addr1 addr2 srcr) lbl') def 336  COND srcr lbl_true ⇒ 337 add_graph ertl_params1 … lbl (sequential … (COND … srcr lbl_true) lbl') def 338  COMMENT msg ⇒ 339 add_graph ertl_params1 … lbl (sequential … (COMMENT … msg) lbl') def 340 ]]. 341 @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *) 342 qed. 224  CALL_ID f args ret_regs ⇒ 225 set_params ? args @@ 226 CALL_ID ERTL ? f (args) it ::: 227 fetch_result ? ret_regs 228  extension_call c ⇒ 229 match c with 230 [ rtl_call_ptr f1 f2 args dest ⇒ 231 ? 232 ] 233 ] 234  COND r ltrue ⇒ 235 COND ERTL ? r ltrue 236 ]. cases daemon (* pointer call to be ported yet *) qed. 237 238 definition translate_fin_step : 239 ∀globals.label → joint_fin_step RTL_ntc → 240 bind_seq_block ERTL globals (joint_fin_step ERTL) ≝ 241 λglobals.λ_.λs. 242 match s with 243 [ GOTO lbl' ⇒ GOTO … lbl' 244  RETURN ⇒ RETURN ? 245  tailcall abs ⇒ match abs in void with [ ] 246 ]. 343 247 344 248 (* hack with empty graphs used here *) 345 definition translate_funct_internal ≝ 346 λglobals.λdef:rtlntc_internal_function globals. 249 definition translate_funct : 250 ∀globals.joint_internal_function RTL_ntc globals → 251 joint_internal_function ERTL globals ≝ 252 λglobals,def. 347 253 let nb_params ≝ joint_if_params ?? def in 348 254 let added_stacksize ≝ max 0 (minus nb_params (RegisterParams)) in 349 255 let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in 350 let entry' ≝ joint_if_entry … def in 351 let exit' ≝ joint_if_exit … def in 352 let graph' ≝ add ? ? (empty_map ? ?) entry' (GOTO … entry') in 353 let graph' ≝ add ? ? graph' exit' (GOTO … exit') in 354 let def' ≝ 355 mk_joint_internal_function globals (ertl_params globals) 356 (joint_if_luniverse … def) (joint_if_runiverse … def) (joint_if_result … def) (*CSC: different from OCaml code where joint_if_result is unit*) 256 let entry' ≝ pi1 … (joint_if_entry … def) in 257 let exit' ≝ pi1 … (joint_if_exit … def) in 258 let def' ≝ init_graph_if ERTL globals 259 (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *) 357 260 nb_params new_locals ((joint_if_stacksize … def) + added_stacksize) 358 graph' ? ?in359 let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in360 add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.361 whd in match ertl_params; (* CSC: Matita's bug here; not enough/too much reduction 362 makes the next application fail. Why? *)363 % 364 [ @entry'  @graph_add_lookup @graph_add365  @exit'  @graph_add ]366 qed. 367 261 entry' exit' in 262 let def'' ≝ b_graph_translate … 263 (ertl_fresh_reg …) 264 def' 265 (translate_step globals) 266 (translate_fin_step globals) 267 def in 268 add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'. 269 270 (* removing this because of how insert_prologue is now defined 368 271 definition generate ≝ 369 272 λglobals. 370 273 λstmt. 371 λdef: joint_internal_function … (ertl_params globals).274 λdef: joint_internal_function globals ERTL. 372 275 let 〈entry, def〉 ≝ fresh_label … def in 373 276 let graph ≝ add … (joint_if_code … def) entry stmt in 374 set_joint_if_graph … ( ertl_paramsglobals) graph def ??.277 set_joint_if_graph … (ERTL globals) graph def ??. 375 278 [ (*% [ @entry  @graph_add ]*) cases daemon (*CSC: XXX *) 376 279  (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL  @graph_add_lookup @LBL_PRF … … 392 295 match inst with 393 296 [ COST_LABEL cost_lbl ⇒ 394 〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉297 〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉 395 298  _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ] 396 299  RETURN ⇒ 〈None …, def〉 … … 407 310 match cost_label with 408 311 [ None ⇒ def 409  Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def312  Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def 410 313 ]. 411 314 412 315 definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)). 316 *) 413 317 414 318 definition rtl_to_ertl : rtl_program → ertl_program ≝
Note: See TracChangeset
for help on using the changeset viewer.