Changeset 1241 for src/ERTL/ERTLToLTL.ma
 Timestamp:
 Sep 21, 2011, 5:28:06 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1232 r1241 3 3 include "ERTL/spill.ma". 4 4 include "ERTL/build.ma". 5 include "ERTL/uses.ma". 5 6 include "ERTL/Interference.ma". 6 7 include "ASM/Arithmetic.ma". … … 78 79 λglobals. 79 80 λint_fun. 80 colour_locals + (joint_if_stacksize globals ertl_params (ertl_sem_params_ globals)int_fun).81 colour_locals + (joint_if_stacksize ertl_params globals int_fun). 81 82 82 83 definition stacksize ≝ 83 84 λglobals. 84 85 λint_fun. 85 colour_locals + (joint_if_stacksize globals ertl_params (ertl_sem_params_ globals)int_fun).86 colour_locals + (joint_if_stacksize ertl_params globals int_fun). 86 87 87 88 definition adjust_off ≝ … … 103 104 λl. 104 105 let off ≝ adjust_off globals int_fun off in 105 let luniv ≝ joint_if_luniverse globals …int_fun in106 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 106 107 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in 107 108 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in … … 123 124 λl. 124 125 let off ≝ adjust_off globals int_fun off in 125 let luniv ≝ joint_if_luniverse globals …int_fun in126 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 126 127 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in 127 128 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in … … 147 148 〈RegisterSST, l, graph, luniv〉 148 149  decision_colour hwr ⇒ 149 let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun in150 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 150 151 〈hwr, l, graph, luniv〉 151 152 ]. … … 160 161 λstmt. 161 162 match lookup valuation coloured_graph (inl … r) with 162 [ decision_colour hwr ⇒ generate globals (joint_if_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun) graph (stmt hwr)163 [ decision_colour hwr ⇒ generate globals (joint_if_luniverse ertl_params globals int_fun) graph (stmt hwr) 163 164  decision_spill off ⇒ 164 165 let temphwr ≝ RegisterSST in 165 let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse globals …int_fun) graph (stmt temphwr) in166 let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse ertl_params globals int_fun) graph (stmt temphwr) in 166 167 let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l in 167 168 generate globals luniv graph stmt … … 179 180 match src with 180 181 [ decision_colour src_hwr ⇒ 181 let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun in182 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 182 183 if eq_Register dest_hwr src_hwr then 183 184 〈joint_st_goto … globals l, graph, luniv〉 … … 191 192 [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l 192 193  decision_spill src_off ⇒ 193 let luniv ≝ joint_if_luniverse globals …int_fun in194 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 194 195 if eq_nat dest_off src_off then 195 196 〈joint_st_goto … globals l, graph, luniv〉 … … 208 209 λl: label. 209 210 if eq_nat (stacksize globals int_fun) 0 then 210 〈joint_st_goto ltl_params globals l, graph, (joint_if_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun)〉211 〈joint_st_goto ltl_params globals l, graph, (joint_if_luniverse ertl_params globals int_fun)〉 211 212 else 212 let luniv ≝ joint_if_luniverse globals …int_fun in213 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 213 214 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in 214 215 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in … … 227 228 λl. 228 229 if eq_nat (stacksize globals int_fun) 0 then 229 〈joint_st_goto ltl_params globals l, graph, joint_if_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun〉230 〈joint_st_goto ltl_params globals l, graph, joint_if_luniverse ertl_params globals int_fun〉 230 231 else 231 let luniv ≝ joint_if_luniverse globals …int_fun in232 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 232 233 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in 233 234 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in … … 246 247 match stmt with 247 248 [ joint_st_sequential seq l ⇒ 248 let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun in249 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 249 250 match seq with 250 251 [ joint_instr_comment c ⇒ … … 258 259  joint_instr_push r ⇒ 259 260 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in 260 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in261 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 261 262 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 262 263 〈joint_st_goto ltl_params globals l, graph, luniv〉 263 264  joint_instr_cond srcr lbl_true ⇒ 264 265 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in 265 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in266 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 266 267 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 267 268 〈joint_st_goto ltl_params globals l, graph, luniv〉 … … 273 274 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in 274 275 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 275 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in276 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 276 277 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 277 278 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in 278 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in279 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 279 280 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 280 281 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in … … 288 289 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in 289 290 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 290 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in291 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 291 292 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 292 293 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in 293 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in294 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 294 295 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 295 296 〈joint_st_goto ltl_params globals l, graph, luniv〉 … … 300 301 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 301 302 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in 302 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in303 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 303 304 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 304 305 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 305 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in306 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 306 307 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 307 308 〈joint_st_goto ltl_params globals l, graph, luniv〉 … … 310 311 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 311 312 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in 312 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in313 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 313 314 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 314 315 〈joint_st_goto ltl_params globals l, graph, luniv〉 … … 320 321 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 321 322 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in 322 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in323 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 323 324 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 324 325 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 325 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in326 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 326 327 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 327 328 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in 328 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in329 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 329 330 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l in 330 331 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 331 332 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in 332 333 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in 333 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in334 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 334 335 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 335 336 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 336 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in337 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 337 338 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 338 339 〈joint_st_goto ltl_params globals l, graph, luniv〉 … … 359 360 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in 360 361 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in 361 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in362 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 362 363 let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l in 363 364 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in … … 365 366 〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉 366 367 ] 367  joint_st_return ⇒ 〈joint_st_return … globals, graph, joint_if_luniverse globals …int_fun〉368  joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, joint_if_luniverse globals …int_fun〉368  joint_st_return ⇒ 〈joint_st_return … globals, graph, joint_if_luniverse ertl_params globals int_fun〉 369  joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, joint_if_luniverse ertl_params globals int_fun〉 369 370  joint_st_extension ext ⇒ 370 371 match ext with … … 380 381 λglobals. 381 382 λint_fun. 382 383 let uses ≝ examine_internal globals int_fun in ?. 383 384 384 385 definition translate_funct ≝
Note: See TracChangeset
for help on using the changeset viewer.