Changeset 2808 for src/ERTLptr
 Timestamp:
 Mar 7, 2013, 6:03:18 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLptrToLTL.ma
r2806 r2808 46 46 47 47 definition get_stack: 48 ∀globals.Register → nat → list (joint_seq LTL globals) ≝ 49 λglobals,r,off. 48 ∀globals.nat → Register → nat → list (joint_seq LTL globals) ≝ 49 λglobals,localss,r,off. 50 let off ≝ localss + off in 50 51 set_dp_by_offset ? off @ 51 52 [ LOAD … A it it ] @ … … 53 54 54 55 definition set_stack_not_a : 55 ∀globals.nat → Register → list (joint_seq LTL globals) ≝ 56 λglobals,off,r. 56 ∀globals.nat → nat → Register → list (joint_seq LTL globals) ≝ 57 λglobals,localss,off,r. 58 let off ≝ localss + off in 57 59 set_dp_by_offset ? off @ 58 60 [ A ← r … … 60 62 61 63 definition set_stack_a : 62 ∀globals.nat → list (joint_seq LTL globals) ≝63 λglobals, off.64 ∀globals.nat → nat → list (joint_seq LTL globals) ≝ 65 λglobals,localss,off. 64 66 [ RegisterST1 ← A ] @ 65 set_stack_not_a ? off RegisterST1.67 set_stack_not_a ? localss off RegisterST1. 66 68 67 69 definition set_stack : 68 ∀globals.nat → Register → list (joint_seq LTL globals) ≝69 λglobals, off,r.70 ∀globals.nat → nat → Register → list (joint_seq LTL globals) ≝ 71 λglobals,localss,off,r. 70 72 if eq_Register r RegisterA then 71 set_stack_a ? off73 set_stack_a ? localss off 72 74 else 73 set_stack_not_a ? off r.75 set_stack_not_a ? localss off r. 74 76 75 77 definition set_stack_int : 76 ∀globals.nat → Byte → list (joint_seq LTL globals) ≝ 77 λglobals,off,int. 78 ∀globals.nat → nat → Byte → list (joint_seq LTL globals) ≝ 79 λglobals,localss,off,int. 80 let off ≝ localss + off in 78 81 set_dp_by_offset ? off @ 79 82 [ A ← int … … 81 84 82 85 definition move : 83 ∀globals. bool → decision → arg_decision → list (joint_seq LTL globals) ≝84 λglobals, carry_lives_after,dst,src.86 ∀globals.nat → bool → decision → arg_decision → list (joint_seq LTL globals) ≝ 87 λglobals,localss,carry_lives_after,dst,src. 85 88 match dst with 86 89 [ decision_colour dstr ⇒ … … 93 96  arg_decision_spill srco ⇒ 94 97 preserve_carry_bit ? carry_lives_after 95 (get_stack ? dstr srco)98 (get_stack ? localss dstr srco) 96 99  arg_decision_imm int ⇒ 97 100 [ A ← int ] @ … … 103 106 [ arg_decision_colour srcr ⇒ 104 107 preserve_carry_bit ? carry_lives_after 105 (set_stack ? dsto srcr)108 (set_stack ? localss dsto srcr) 106 109  arg_decision_spill srco ⇒ 107 110 if eqb srco dsto then [ ] else 108 111 preserve_carry_bit ? carry_lives_after 109 (get_stack ? RegisterA srco @110 set_stack ? dsto RegisterA)112 (get_stack ? localss RegisterA srco @ 113 set_stack ? localss dsto RegisterA) 111 114  arg_decision_imm int ⇒ 112 115 preserve_carry_bit ? carry_lives_after 113 (set_stack_int ? dsto int)116 (set_stack_int ? localss dsto int) 114 117 ] 115 118 ]. … … 169 172 170 173 definition translate_op2 : 171 ∀globals. bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝172 λglobals, carry_lives_after,op,dst,arg1,arg2.174 ∀globals.nat → bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 175 λglobals,localss,carry_lives_after,op,dst,arg1,arg2. 173 176 (* this won't preserve the carry bit if op does not set it: left to next function *) 174 177 (* if op uses carry bit (⇒ it sets it too) it must be preserved before the op *) 175 178 (preserve_carry_bit ? 176 179 (uses_carry op ∧ (arg_is_spilled arg1 ∨ arg_is_spilled arg2)) 177 (move ? false RegisterB arg2 @178 move ? false RegisterA arg1) @180 (move ? localss false RegisterB arg2 @ 181 move ? localss false RegisterA arg1) @ 179 182 [ A ← A .op. RegisterB ] @ 180 183 (* it op sets the carry bit and it is needed afterwards it must be preserved here *) 181 move ? (sets_carry op ∧ carry_lives_after) dst RegisterA).184 move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA). 182 185 183 186 definition translate_op2_smart : 184 ∀globals. bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝185 λglobals, carry_lives_after,op,dst,arg1,arg2.187 ∀globals.nat → bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 188 λglobals,localss,carry_lives_after,op,dst,arg1,arg2. 186 189 (* if op does not set carry bit (⇒ it does not use it either) then it must be 187 190 preserved *) … … 191 194 (match arg2 with 192 195 [ arg_decision_colour arg2r ⇒ 193 move ? (uses_carry op) RegisterA arg1 @196 move ? localss (uses_carry op) RegisterA arg1 @ 194 197 [ A ← A .op. arg2r ] @ 195 move ? (sets_carry op ∧ carry_lives_after) dst RegisterA198 move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA 196 199  arg_decision_imm arg2i ⇒ 197 move ? (uses_carry op) RegisterA arg1 @200 move ? localss (uses_carry op) RegisterA arg1 @ 198 201 [ A ← A .op. arg2i ] @ 199 move ? (sets_carry op ∧ carry_lives_after) dst RegisterA202 move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA 200 203  _ ⇒ 201 204 if commutative op then 202 205 match arg1 with 203 206 [ arg_decision_colour arg1r ⇒ 204 move ? (uses_carry op) RegisterA arg2 @207 move ? localss (uses_carry op) RegisterA arg2 @ 205 208 [ A ← A .op. arg1r ] @ 206 move ? (sets_carry op ∧ carry_lives_after) dst RegisterA209 move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA 207 210  arg_decision_imm arg1i ⇒ 208 move ? (uses_carry op) RegisterA arg2 @211 move ? localss (uses_carry op) RegisterA arg2 @ 209 212 [ A ← A .op. arg1i ] @ 210 move ? (sets_carry op ∧ carry_lives_after) dst RegisterA213 move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA 211 214  _ ⇒ 212 translate_op2 ? carry_lives_after op dst arg1 arg2215 translate_op2 ? localss carry_lives_after op dst arg1 arg2 213 216 ] 214 217 else 215 translate_op2 ? carry_lives_after op dst arg1 arg2218 translate_op2 ? localss carry_lives_after op dst arg1 arg2 216 219 ]). 217 220 … … 225 228 226 229 definition translate_op1 : 227 ∀globals. bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝228 λglobals, carry_lives_after,op,dst,arg.230 ∀globals.nat → bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝ 231 λglobals,localss,carry_lives_after,op,dst,arg. 229 232 let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in 230 233 preserve_carry_bit ? preserve_carry 231 (move ? false RegisterA arg @234 (move ? localss false RegisterA arg @ 232 235 OP1 … op it it :: 233 move ? false dst RegisterA).236 move ? localss false dst RegisterA). 234 237 235 238 definition translate_opaccs : 236 ∀globals. bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝237 λglobals, carry_lives_after,op,dst1,dst2,arg1,arg2.239 ∀globals.nat → bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 240 λglobals,localss,carry_lives_after,op,dst1,dst2,arg1,arg2. 238 241 (* OPACCS always has dead carry bit and sets it to zero *) 239 move ? false RegisterB arg2 @240 move ? false RegisterA arg1 @242 move ? localss false RegisterB arg2 @ 243 move ? localss false RegisterA arg1 @ 241 244 OPACCS … op it it it it :: 242 move ? false dst1 RegisterA @243 move ? false dst2 RegisterB @245 move ? localss false dst1 RegisterA @ 246 move ? localss false dst2 RegisterB @ 244 247 if carry_lives_after ∧ (is_spilled dst1 ∨ is_spilled dst2) then 245 248 [CLEAR_CARRY ??] … … 248 251 (* does not preserve carry bit *) 249 252 definition move_to_dp : 250 ∀globals. arg_decision → arg_decision → list (joint_seq LTL globals) ≝251 λglobals, arg1,arg2.253 ∀globals.nat → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 254 λglobals,localss,arg1,arg2. 252 255 if ¬arg_is_spilled arg1 then 253 move ? false RegisterDPH arg2 @256 move ? localss false RegisterDPH arg2 @ 254 257 (* does not change dph because arg1 is not spilled *) 255 move ? false RegisterDPL arg1258 move ? localss false RegisterDPL arg1 256 259 else if ¬arg_is_spilled arg2 then 257 move ? false RegisterDPL arg1 @260 move ? localss false RegisterDPL arg1 @ 258 261 (* does not change dpl because arg2 is not spilled *) 259 move ? false RegisterDPH arg2262 move ? localss false RegisterDPH arg2 260 263 else 261 264 (* using B as temporary, as moving spilled registers tampers with DPTR *) 262 move ? false RegisterB arg1 @263 move ? false RegisterDPH arg2 @264 move ? false RegisterDPL RegisterB.265 move ? localss false RegisterB arg1 @ 266 move ? localss false RegisterDPH arg2 @ 267 move ? localss false RegisterDPL RegisterB. 265 268 266 269 definition translate_store : 267 ∀globals. bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝268 λglobals, carry_lives_after,addr1,addr2,src.270 ∀globals.nat → bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 271 λglobals,localss,carry_lives_after,addr1,addr2,src. 269 272 (* requires src != RegisterA and RegisterB *) 270 273 preserve_carry_bit ? (carry_lives_after ∧ 271 274 (arg_is_spilled addr1 ∨ arg_is_spilled addr1 ∨ arg_is_spilled src)) 272 (let move_to_dptr ≝ move_to_dp ? addr1 addr2 in275 (let move_to_dptr ≝ move_to_dp ? localss addr1 addr2 in 273 276 (if arg_is_spilled src then 274 move ? false RegisterST0 src @277 move ? localss false RegisterST0 src @ 275 278 move_to_dptr @ 276 279 [ A ← RegisterST0] … … 279 282 280 283 definition translate_load : 281 ∀globals. bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝282 λglobals, carry_lives_after,dst,addr1,addr2.284 ∀globals.nat → bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 285 λglobals,localss,carry_lives_after,dst,addr1,addr2. 283 286 preserve_carry_bit ? (carry_lives_after ∧ 284 287 (is_spilled dst ∨ arg_is_spilled addr1 ∨ arg_is_spilled addr1)) 285 (move_to_dp ? addr1 addr2 @288 (move_to_dp ? localss addr1 addr2 @ 286 289 [ LOAD … A it it ] @ 287 move ? false dst RegisterA).290 move ? localss false dst RegisterA). 288 291 289 292 definition translate_address : 290 ∀globals. bool → ∀i.i ∈ globals → decision → decision →293 ∀globals.nat → bool → ∀i.i ∈ globals → decision → decision → 291 294 list (joint_seq LTL globals) ≝ 292 λglobals, carry_lives_after,id,prf,addr1,addr2.295 λglobals,localss,carry_lives_after,id,prf,addr1,addr2. 293 296 preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2)) 294 297 (ADDRESS LTL ? id prf it it :: 295 move ? false addr1 RegisterDPL @296 move ? false addr2 RegisterDPH).298 move ? localss false addr1 RegisterDPL @ 299 move ? localss false addr2 RegisterDPH). 297 300 298 301 definition translate_low_address : 299 ∀globals. bool → decision → label →302 ∀globals.nat → bool → decision → label → 300 303 list (joint_seq LTL globals) ≝ 301 λglobals, carry_lives_after,dst,lbl.304 λglobals,localss,carry_lives_after,dst,lbl. 302 305 match dst return λ_.list (joint_seq LTL globals) with 303 306 [ decision_colour r ⇒ [LOW_ADDRESS r lbl] 304 307  _ ⇒ 305 LOW_ADDRESS RegisterA lbl :: move ? carry_lives_after dst RegisterA308 LOW_ADDRESS RegisterA lbl :: move ? localss carry_lives_after dst RegisterA 306 309 ]. 307 310 308 311 definition translate_high_address : 309 ∀globals. bool → decision → label →312 ∀globals.nat → bool → decision → label → 310 313 list (joint_seq LTL globals) ≝ 311 λglobals, carry_lives_after,dst,lbl.314 λglobals,localss,carry_lives_after,dst,lbl. 312 315 match dst return λ_.list (joint_seq LTL globals) with 313 316 [ decision_colour r ⇒ [HIGH_ADDRESS r lbl] 314 317  _ ⇒ 315 HIGH_ADDRESS RegisterA lbl :: move ? carry_lives_after dst RegisterA318 HIGH_ADDRESS RegisterA lbl :: move ? localss carry_lives_after dst RegisterA 316 319 ]. 317 320 318 321 definition translate_step: 319 ∀globals. ∀after : valuation register_lattice.322 ∀globals.nat → ∀after : valuation register_lattice. 320 323 coloured_graph after → 321 324 ℕ → label → joint_step ERTLptr globals → bind_step_block LTL globals ≝ 322 λglobals, after,grph,stack_sz,lbl,s.325 λglobals,localss,after,grph,stack_sz,lbl,s. 323 326 bret … ( 324 327 let lookup ≝ λr.colouring … grph (inl … r) in … … 328 331 ] in 329 332 let carry_lives_after ≝ hlives RegisterCarry (after lbl) in 330 let move ≝ move globals carry_lives_after in333 let move ≝ move globals localss carry_lives_after in 331 334 match s with 332 335 [ step_seq s' ⇒ … … 340 343 [ PUSH … A ] 341 344  STORE addr1 addr2 srcr ⇒ 342 translate_store ? carry_lives_after345 translate_store ? localss carry_lives_after 343 346 (lookup_arg addr1) 344 347 (lookup_arg addr2) 345 348 (lookup_arg srcr) 346 349  LOAD dstr addr1 addr2 ⇒ 347 translate_load ? carry_lives_after350 translate_load ? localss carry_lives_after 348 351 (lookup dstr) 349 352 (lookup_arg addr1) … … 352 355  SET_CARRY ⇒ [CLEAR_CARRY ??] 353 356  OP2 op dst arg1 arg2 ⇒ 354 translate_op2_smart ? carry_lives_after op357 translate_op2_smart ? localss carry_lives_after op 355 358 (lookup dst) 356 359 (lookup_arg arg1) 357 360 (lookup_arg arg2) 358 361  OP1 op dst arg ⇒ 359 translate_op1 ? carry_lives_after op362 translate_op1 ? localss carry_lives_after op 360 363 (lookup dst) 361 364 (lookup arg) … … 373 376 move dst src 374 377  ADDRESS lbl prf dpl dph ⇒ 375 translate_address ? carry_lives_after378 translate_address ? localss carry_lives_after 376 379 lbl prf (lookup dpl) (lookup dph) 377 380  OPACCS op dst1 dst2 arg1 arg2 ⇒ 378 translate_opaccs ? carry_lives_after op381 translate_opaccs ? localss carry_lives_after op 379 382 (lookup dst1) (lookup dst2) 380 383 (lookup_arg arg1) (lookup_arg arg2) … … 389 392 ] 390 393  LOW_ADDRESS r1 l ⇒ 391 translate_low_address ? carry_lives_after (lookup r1) l394 translate_low_address ? localss carry_lives_after (lookup r1) l 392 395  HIGH_ADDRESS r1 l ⇒ 393 translate_high_address ? carry_lives_after (lookup r1) l396 translate_high_address ? localss carry_lives_after (lookup r1) l 394 397 ] 395 398 ] … … 403 406  inr dp ⇒ 404 407 let 〈dpl, dph〉 ≝ dp in 405 〈add_dummy_variance … (move_to_dp …(lookup_arg dpl) (lookup_arg dph)),408 〈add_dummy_variance … (move_to_dp ? localss (lookup_arg dpl) (lookup_arg dph)), 406 409 λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉 407 410 ] … … 436 439 (* added_prologue ≝ *) [ ] 437 440 (* new_regs ≝ *) [ ] 438 (* f_step ≝ *) (translate_step … coloured_graph stack_sz)441 (* f_step ≝ *) (translate_step ? (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz) 439 442 (* f_fin ≝ *) (translate_fin_step globals) 440 443 ????).
Note: See TracChangeset
for help on using the changeset viewer.