 Timestamp:
 Sep 23, 2011, 1:47:27 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1257 r1258 158 158 λsregs. 159 159 λdef. 160 let start_lbl ≝ joint_if_entry globals(ertl_params globals) def in161 let 〈tmp_lbl, nuniv〉 ≝ fresh_label ?def in162 match lookup ? ? (joint_if_code ?(ertl_params globals) def) start_lbl160 let start_lbl ≝ joint_if_entry … (ertl_params globals) def in 161 let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in 162 match lookup … (joint_if_code … (ertl_params globals) def) start_lbl 163 163 return λx. x ≠ None ? → ertl_internal_function globals with 164 164 [ None ⇒ λnone_absrd. ⊥ … … 184 184 185 185 definition save_return ≝ 186 λglobals. 186 187 λret_regs. 187 188 λstart_lbl: label. 188 189 λdest_lbl: label. 189 λdef: ertl_internal_function .190 let 〈def, tmpr〉 ≝ fresh_reg def in190 λdef: ertl_internal_function globals. 191 let 〈def, tmpr〉 ≝ fresh_reg … def in 191 192 match reduce_strong ? ? RegisterSTS ret_regs with 192 193 [ dp crl crl_proof ⇒ … … 195 196 let restl ≝ \snd (\fst crl) in 196 197 let restr ≝ \snd (\snd crl) in 197 let init_tmpr ≝ ertl_st_int tmpr (zero ?) start_lbl in198 let f_save ≝ λst. λr. ertl_st_set_hdw st rstart_lbl in198 let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int … tmpr (zero ?)) start_lbl in 199 let f_save ≝ λst. λr. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo r〉) start_lbl in 199 200 let saves ≝ map2 ? ? ? f_save commonl commonr crl_proof in 200 let f_default ≝ λst. ertl_st_set_hdw st tmprstart_lbl in201 let f_default ≝ λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo tmpr〉) start_lbl in 201 202 let defaults ≝ map ? ? f_default restl in 202 adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def203 adds_graph … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def 203 204 ]. 204 205 205 206 definition assign_result ≝ 206 λ start_lbl: label.207 λglobals.λstart_lbl: label. 207 208 match reduce_strong ? ? RegisterRets RegisterSTS with 208 209 [ dp crl crl_proof ⇒ 209 210 let commonl ≝ \fst (\fst crl) in 210 211 let commonr ≝ \fst (\snd crl) in 211 let f ≝ λret. λst. ertl_st_hdw_to_hdw ret ststart_lbl in212 let f ≝ λret. λst. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware ret, hardware st〉) start_lbl in 212 213 let insts ≝ map2 ? ? ? f commonl commonr crl_proof in 213 adds_graph insts start_lbl214 adds_graph … insts start_lbl 214 215 ]. 215 216 216 217 definition add_epilogue ≝ 218 λglobals. 217 219 λret_regs. 218 220 λsral. … … 220 222 λsregs. 221 223 λdef. 222 let start_lbl ≝ ertl_if_exitdef in223 let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in224 match lookup ? ? (ertl_if_graphdef) start_lbl225 return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ?with226 [ None ⇒ λnone_abs d. ?224 let start_lbl ≝ joint_if_exit … (ertl_params globals) def in 225 let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in 226 match lookup … (joint_if_code … (ertl_params globals) def) start_lbl 227 return λx. x ≠ None ? → ertl_internal_function globals with 228 [ None ⇒ λnone_absrd. ⊥ 227 229  Some last_stmt ⇒ λsome_prf. 228 230 let def ≝ 229 add_translates (230 [save_return ret_regs] @231 restore_hdws sregs @232 [adds_graph [233 ertl_st_push srahstart_lbl;234 ertl_st_push sralstart_lbl231 add_translates … ( 232 [save_return globals ret_regs] @ 233 restore_hdws … sregs @ 234 [adds_graph … [ 235 joint_st_sequential … (joint_instr_push … srah) start_lbl; 236 joint_st_sequential … (joint_instr_push … sral) start_lbl 235 237 ]] @ 236 [adds_graph [237 ertl_st_del_framestart_lbl238 [adds_graph … [ 239 joint_st_sequential … (joint_instr_extension … ertl_st_ext_del_frame) start_lbl 238 240 ]] @ 239 [assign_result ]241 [assign_result globals] 240 242 ) start_lbl tmp_lbl def 241 243 in 242 let def ≝ add_graphtmp_lbl last_stmt def in243 set_joint_if_exit … tmp_lbl def ?244 let def' ≝ add_graph … tmp_lbl last_stmt def in 245 set_joint_if_exit … tmp_lbl def' ? 244 246 ] ?. 245 cases not_implemented (* dep types here, bug in matita too! *) 247 [ cases start_lbl #x #H @H 248  cases (none_absrd) /2/ 249  cases daemon (* CSC: XXXXX *) 250 ] 246 251 qed. 247 252 248 definition allocate_regs_internal ≝ 249 λr: Register. 250 λdef_sregs. 251 let 〈def, sregs〉 ≝ def_sregs in 252 let 〈def, r'〉 ≝ fresh_reg def in 253 〈def, 〈r', r〉 :: sregs〉. 254 253 255 254 definition allocate_regs ≝ 255 λglobals. 256 256 λrs. 257 257 λsaved: rs_set rs. 258 258 λdef. 259 let allocate_regs_internal ≝ 260 λr: Register. 261 λdef_sregs. 262 let 〈def, sregs〉 ≝ def_sregs in 263 let 〈def, r'〉 ≝ fresh_reg globals def in 264 〈def, 〈r', r〉 :: sregs〉 265 in 259 266 rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉. 260 267 261 268 definition add_pro_and_epilogue ≝ 269 λglobals. 262 270 λparams. 263 271 λret_regs. 264 272 λdef. 265 match fresh_regs_strong def 2 with273 match fresh_regs_strong globals def 2 with 266 274 [ dp def_sra def_sra_proof ⇒ 267 275 let def ≝ \fst def_sra in … … 269 277 let sral ≝ nth_safe ? 0 sra ? in 270 278 let srah ≝ nth_safe ? 1 sra ? in 271 let 〈def, sregs〉 ≝ allocate_regs register_list_set RegisterCalleeSaved def in272 let def ≝ add_prologue params sral srah sregs def in273 let def ≝ add_epilogue ret_regs sral srah sregs def in279 let 〈def, sregs〉 ≝ allocate_regs … register_list_set RegisterCalleeSaved def in 280 let def ≝ add_prologue … params sral srah sregs def in 281 let def ≝ add_epilogue … ret_regs sral srah sregs def in 274 282 def 275 283 ]. 276 [1: >def_sra_proof // 277 2: >def_sra_proof // 278 ] 284 >def_sra_proof // 279 285 qed. 280 286 281 287 definition set_params_hdw ≝ 282 λ params.288 λglobals,params. 283 289 match params with 284 [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skipstart_lbl] start_lbl]290 [ nil ⇒ [ λstart_lbl. adds_graph … [joint_st_goto … start_lbl] start_lbl] 285 291  _ ⇒ 286 292 let l ≝ zip_pottier ? ? params RegisterParams in 287 restore_hdws l293 restore_hdws globals l 288 294 ]. 289 295
Note: See TracChangeset
for help on using the changeset viewer.