| 1 | include "LTL/LTL.ma". |
|---|
| 2 | include "ERTLptr/Interference.ma". |
|---|
| 3 | include "ASM/Arithmetic.ma". |
|---|
| 4 | include "joint/TranslateUtils.ma". |
|---|
| 5 | |
|---|
| 6 | (* Note: translation is complicated by having to preserve the carry bit and |
|---|
| 7 | wanting to do it with as less boilerplate as possible. It could be somewhat |
|---|
| 8 | simplified if constant and copy propagation was to be done after this pass: |
|---|
| 9 | those optimisations would take care of the boilerplate for us.*) |
|---|
| 10 | |
|---|
| 11 | coercion Reg_to_dec : ∀r:Register.decision ≝ decision_colour on _r : Register to decision. |
|---|
| 12 | |
|---|
| 13 | inductive arg_decision : Type[0] ≝ |
|---|
| 14 | | arg_decision_colour : Register → arg_decision |
|---|
| 15 | | arg_decision_spill : ℕ → arg_decision |
|---|
| 16 | | arg_decision_imm : Byte → arg_decision. |
|---|
| 17 | |
|---|
| 18 | coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision. |
|---|
| 19 | |
|---|
| 20 | (* Paolo: I'm changing the following: before, spilled registers were |
|---|
| 21 | assigned stack addresses going from SP + #frame_size - #stack_params |
|---|
| 22 | excluded down to SP included. I am turning it upside down, so that |
|---|
| 23 | the offset does not need the stack size to be computed *) |
|---|
| 24 | |
|---|
| 25 | definition preserve_carry_bit : |
|---|
| 26 | ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝ |
|---|
| 27 | λglobals,do_it,steps. |
|---|
| 28 | if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps. |
|---|
| 29 | |
|---|
| 30 | (* for notation *) |
|---|
| 31 | definition A ≝ it. |
|---|
| 32 | |
|---|
| 33 | coercion beval_of_byte : ∀b : Byte.beval ≝ BVByte on _b : Byte to beval. |
|---|
| 34 | |
|---|
| 35 | (* spill should be byte-based from the start *) |
|---|
| 36 | definition set_dp_by_offset : |
|---|
| 37 | ∀globals.nat → list (joint_seq LTL globals) ≝ |
|---|
| 38 | λglobals,off. |
|---|
| 39 | [ A ← byte_of_nat off |
|---|
| 40 | ; A ← A .Add. RegisterSPL |
|---|
| 41 | ; RegisterDPL ← A |
|---|
| 42 | ; A ← zero_byte |
|---|
| 43 | ; A ← A .Addc. RegisterSPH |
|---|
| 44 | ; RegisterDPH ← A |
|---|
| 45 | ]. |
|---|
| 46 | |
|---|
| 47 | definition get_stack: |
|---|
| 48 | ∀globals.nat → Register → nat → list (joint_seq LTL globals) ≝ |
|---|
| 49 | λglobals,localss,r,off. |
|---|
| 50 | let off ≝ localss + off in |
|---|
| 51 | set_dp_by_offset ? off @ |
|---|
| 52 | [ LOAD … A it it ] @ |
|---|
| 53 | if eq_Register r RegisterA then [ ] else [ r ← A ]. |
|---|
| 54 | |
|---|
| 55 | definition set_stack_not_a : |
|---|
| 56 | ∀globals.nat → nat → Register → list (joint_seq LTL globals) ≝ |
|---|
| 57 | λglobals,localss,off,r. |
|---|
| 58 | let off ≝ localss + off in |
|---|
| 59 | set_dp_by_offset ? off @ |
|---|
| 60 | [ A ← r |
|---|
| 61 | ; STORE … it it A ]. |
|---|
| 62 | |
|---|
| 63 | definition set_stack_a : |
|---|
| 64 | ∀globals.nat → nat → list (joint_seq LTL globals) ≝ |
|---|
| 65 | λglobals,localss,off. |
|---|
| 66 | [ RegisterST1 ← A ] @ |
|---|
| 67 | set_stack_not_a ? localss off RegisterST1. |
|---|
| 68 | |
|---|
| 69 | definition set_stack : |
|---|
| 70 | ∀globals.nat → nat → Register → list (joint_seq LTL globals) ≝ |
|---|
| 71 | λglobals,localss,off,r. |
|---|
| 72 | if eq_Register r RegisterA then |
|---|
| 73 | set_stack_a ? localss off |
|---|
| 74 | else |
|---|
| 75 | set_stack_not_a ? localss off r. |
|---|
| 76 | |
|---|
| 77 | definition set_stack_int : |
|---|
| 78 | ∀globals.nat → nat → Byte → list (joint_seq LTL globals) ≝ |
|---|
| 79 | λglobals,localss,off,int. |
|---|
| 80 | let off ≝ localss + off in |
|---|
| 81 | set_dp_by_offset ? off @ |
|---|
| 82 | [ A ← int |
|---|
| 83 | ; STORE … it it A ]. |
|---|
| 84 | |
|---|
| 85 | definition move : |
|---|
| 86 | ∀globals.nat → bool → decision → arg_decision → list (joint_seq LTL globals) ≝ |
|---|
| 87 | λglobals,localss,carry_lives_after,dst,src. |
|---|
| 88 | match dst with |
|---|
| 89 | [ decision_colour dstr ⇒ |
|---|
| 90 | match src with |
|---|
| 91 | [ arg_decision_colour srcr ⇒ |
|---|
| 92 | if eq_Register dstr srcr then [ ] else |
|---|
| 93 | if eq_Register dstr RegisterA then [ A ← srcr ] else |
|---|
| 94 | if eq_Register srcr RegisterA then [ dstr ← A ] else |
|---|
| 95 | [ A ← srcr ; dstr ← A] |
|---|
| 96 | | arg_decision_spill srco ⇒ |
|---|
| 97 | preserve_carry_bit ? carry_lives_after |
|---|
| 98 | (get_stack ? localss dstr srco) |
|---|
| 99 | | arg_decision_imm int ⇒ |
|---|
| 100 | [ A ← int ] @ |
|---|
| 101 | if eq_Register dstr RegisterA then [ ] else |
|---|
| 102 | [ dstr ← A ] |
|---|
| 103 | ] |
|---|
| 104 | | decision_spill dsto ⇒ |
|---|
| 105 | match src with |
|---|
| 106 | [ arg_decision_colour srcr ⇒ |
|---|
| 107 | preserve_carry_bit ? carry_lives_after |
|---|
| 108 | (set_stack ? localss dsto srcr) |
|---|
| 109 | | arg_decision_spill srco ⇒ |
|---|
| 110 | if eqb srco dsto then [ ] else |
|---|
| 111 | preserve_carry_bit ? carry_lives_after |
|---|
| 112 | (get_stack ? localss RegisterA srco @ |
|---|
| 113 | set_stack ? localss dsto RegisterA) |
|---|
| 114 | | arg_decision_imm int ⇒ |
|---|
| 115 | preserve_carry_bit ? carry_lives_after |
|---|
| 116 | (set_stack_int ? localss dsto int) |
|---|
| 117 | ] |
|---|
| 118 | ]. |
|---|
| 119 | |
|---|
| 120 | definition arg_is_spilled : arg_decision → bool ≝ |
|---|
| 121 | λx.match x with [ arg_decision_spill _ ⇒ true | _ ⇒ false ]. |
|---|
| 122 | definition is_spilled : decision → bool ≝ |
|---|
| 123 | λx.match x with [ decision_spill _ ⇒ true | _ ⇒ false ]. |
|---|
| 124 | |
|---|
| 125 | definition newframe : |
|---|
| 126 | ∀globals.ℕ → list (joint_seq LTL globals) ≝ |
|---|
| 127 | λglobals,stack_sz. |
|---|
| 128 | [ CLEAR_CARRY … |
|---|
| 129 | ; A ← RegisterSPL |
|---|
| 130 | ; A ← A .Sub. byte_of_nat stack_sz |
|---|
| 131 | ; RegisterSPL ← A |
|---|
| 132 | ; A ← RegisterSPH |
|---|
| 133 | ; A ← A .Sub. zero_byte |
|---|
| 134 | ; RegisterSPH ← A |
|---|
| 135 | ]. |
|---|
| 136 | |
|---|
| 137 | definition delframe : |
|---|
| 138 | ∀globals.ℕ → list (joint_seq LTL globals) ≝ |
|---|
| 139 | λglobals,stack_sz. |
|---|
| 140 | [ A ← RegisterSPL |
|---|
| 141 | ; A ← A .Add. byte_of_nat stack_sz |
|---|
| 142 | ; RegisterSPL ← A |
|---|
| 143 | ; A ← RegisterSPH |
|---|
| 144 | ; A ← A .Addc. zero_byte |
|---|
| 145 | ; RegisterSPH ← A |
|---|
| 146 | ]. |
|---|
| 147 | |
|---|
| 148 | definition commutative : Op2 → bool ≝ |
|---|
| 149 | λop.match op with |
|---|
| 150 | [ Add ⇒ true |
|---|
| 151 | | Addc ⇒ true |
|---|
| 152 | | Or ⇒ true |
|---|
| 153 | | Xor ⇒ true |
|---|
| 154 | | And ⇒ true |
|---|
| 155 | | _ ⇒ false |
|---|
| 156 | ]. |
|---|
| 157 | |
|---|
| 158 | definition uses_carry : Op2 → bool ≝ |
|---|
| 159 | λop.match op with |
|---|
| 160 | [ Addc ⇒ true |
|---|
| 161 | | Sub ⇒ true |
|---|
| 162 | | _ ⇒ false |
|---|
| 163 | ]. |
|---|
| 164 | |
|---|
| 165 | definition sets_carry : Op2 → bool ≝ |
|---|
| 166 | λop.match op with |
|---|
| 167 | [ Add ⇒ true |
|---|
| 168 | | Addc ⇒ true |
|---|
| 169 | | Sub ⇒ true |
|---|
| 170 | | _ ⇒ false |
|---|
| 171 | ]. |
|---|
| 172 | |
|---|
| 173 | definition translate_op2 : |
|---|
| 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. |
|---|
| 176 | (* this won't preserve the carry bit if op does not set it: left to next function *) |
|---|
| 177 | (* if op uses carry bit (⇒ it sets it too) it must be preserved before the op *) |
|---|
| 178 | (preserve_carry_bit ? |
|---|
| 179 | (uses_carry op ∧ (arg_is_spilled arg1 ∨ arg_is_spilled arg2)) |
|---|
| 180 | (move ? localss false RegisterB arg2 @ |
|---|
| 181 | move ? localss false RegisterA arg1) @ |
|---|
| 182 | [ A ← A .op. RegisterB ] @ |
|---|
| 183 | (* it op sets the carry bit and it is needed afterwards it must be preserved here *) |
|---|
| 184 | move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA). |
|---|
| 185 | |
|---|
| 186 | definition translate_op2_smart : |
|---|
| 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. |
|---|
| 189 | (* if op does not set carry bit (⇒ it does not use it either) then it must be |
|---|
| 190 | preserved *) |
|---|
| 191 | preserve_carry_bit ? |
|---|
| 192 | (¬sets_carry op ∧ carry_lives_after ∧ |
|---|
| 193 | (arg_is_spilled arg1 ∨ arg_is_spilled arg2 ∨ is_spilled dst)) |
|---|
| 194 | (match arg2 with |
|---|
| 195 | [ arg_decision_colour arg2r ⇒ |
|---|
| 196 | move ? localss (uses_carry op) RegisterA arg1 @ |
|---|
| 197 | [ A ← A .op. arg2r ] @ |
|---|
| 198 | move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA |
|---|
| 199 | | arg_decision_imm arg2i ⇒ |
|---|
| 200 | move ? localss (uses_carry op) RegisterA arg1 @ |
|---|
| 201 | [ A ← A .op. arg2i ] @ |
|---|
| 202 | move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA |
|---|
| 203 | | _ ⇒ |
|---|
| 204 | if commutative op then |
|---|
| 205 | match arg1 with |
|---|
| 206 | [ arg_decision_colour arg1r ⇒ |
|---|
| 207 | move ? localss (uses_carry op) RegisterA arg2 @ |
|---|
| 208 | [ A ← A .op. arg1r ] @ |
|---|
| 209 | move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA |
|---|
| 210 | | arg_decision_imm arg1i ⇒ |
|---|
| 211 | move ? localss (uses_carry op) RegisterA arg2 @ |
|---|
| 212 | [ A ← A .op. arg1i ] @ |
|---|
| 213 | move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA |
|---|
| 214 | | _ ⇒ |
|---|
| 215 | translate_op2 ? localss carry_lives_after op dst arg1 arg2 |
|---|
| 216 | ] |
|---|
| 217 | else |
|---|
| 218 | translate_op2 ? localss carry_lives_after op dst arg1 arg2 |
|---|
| 219 | ]). |
|---|
| 220 | |
|---|
| 221 | definition dec_to_arg_dec : decision → arg_decision ≝ |
|---|
| 222 | λd.match d with |
|---|
| 223 | [ decision_colour r ⇒ arg_decision_colour r |
|---|
| 224 | | decision_spill n ⇒ arg_decision_spill n |
|---|
| 225 | ]. |
|---|
| 226 | |
|---|
| 227 | coercion dec_arg_dec : ∀d:decision.arg_decision ≝ dec_to_arg_dec on _d : decision to arg_decision. |
|---|
| 228 | |
|---|
| 229 | definition translate_op1 : |
|---|
| 230 | ∀globals.nat → bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝ |
|---|
| 231 | λglobals,localss,carry_lives_after,op,dst,arg. |
|---|
| 232 | let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in |
|---|
| 233 | preserve_carry_bit ? preserve_carry |
|---|
| 234 | (move ? localss false RegisterA arg @ |
|---|
| 235 | OP1 … op it it :: |
|---|
| 236 | move ? localss false dst RegisterA). |
|---|
| 237 | |
|---|
| 238 | definition translate_opaccs : |
|---|
| 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. |
|---|
| 241 | (* OPACCS always has dead carry bit and sets it to zero *) |
|---|
| 242 | move ? localss false RegisterB arg2 @ |
|---|
| 243 | move ? localss false RegisterA arg1 @ |
|---|
| 244 | OPACCS … op it it it it :: |
|---|
| 245 | move ? localss false dst1 RegisterA @ |
|---|
| 246 | move ? localss false dst2 RegisterB @ |
|---|
| 247 | if carry_lives_after ∧ (is_spilled dst1 ∨ is_spilled dst2) then |
|---|
| 248 | [CLEAR_CARRY ??] |
|---|
| 249 | else [ ]. |
|---|
| 250 | |
|---|
| 251 | (* does not preserve carry bit *) |
|---|
| 252 | definition move_to_dp : |
|---|
| 253 | ∀globals.nat → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ |
|---|
| 254 | λglobals,localss,arg1,arg2. |
|---|
| 255 | if ¬arg_is_spilled arg1 then |
|---|
| 256 | move ? localss false RegisterDPH arg2 @ |
|---|
| 257 | (* does not change dph because arg1 is not spilled *) |
|---|
| 258 | move ? localss false RegisterDPL arg1 |
|---|
| 259 | else if ¬arg_is_spilled arg2 then |
|---|
| 260 | move ? localss false RegisterDPL arg1 @ |
|---|
| 261 | (* does not change dpl because arg2 is not spilled *) |
|---|
| 262 | move ? localss false RegisterDPH arg2 |
|---|
| 263 | else |
|---|
| 264 | (* using B as temporary, as moving spilled registers tampers with DPTR *) |
|---|
| 265 | move ? localss false RegisterB arg1 @ |
|---|
| 266 | move ? localss false RegisterDPH arg2 @ |
|---|
| 267 | move ? localss false RegisterDPL RegisterB. |
|---|
| 268 | |
|---|
| 269 | definition translate_store : |
|---|
| 270 | ∀globals.nat → bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ |
|---|
| 271 | λglobals,localss,carry_lives_after,addr1,addr2,src. |
|---|
| 272 | (* requires src != RegisterA and RegisterB *) |
|---|
| 273 | preserve_carry_bit ? (carry_lives_after ∧ |
|---|
| 274 | (arg_is_spilled addr1 ∨ arg_is_spilled addr1 ∨ arg_is_spilled src)) |
|---|
| 275 | (let move_to_dptr ≝ move_to_dp ? localss addr1 addr2 in |
|---|
| 276 | (if arg_is_spilled src then |
|---|
| 277 | move ? localss false RegisterST0 src @ |
|---|
| 278 | move_to_dptr @ |
|---|
| 279 | [ A ← RegisterST0] |
|---|
| 280 | else move_to_dptr) @ |
|---|
| 281 | [STORE … it it A]). |
|---|
| 282 | |
|---|
| 283 | definition translate_load : |
|---|
| 284 | ∀globals.nat → bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ |
|---|
| 285 | λglobals,localss,carry_lives_after,dst,addr1,addr2. |
|---|
| 286 | preserve_carry_bit ? (carry_lives_after ∧ |
|---|
| 287 | (is_spilled dst ∨ arg_is_spilled addr1 ∨ arg_is_spilled addr1)) |
|---|
| 288 | (move_to_dp ? localss addr1 addr2 @ |
|---|
| 289 | [ LOAD … A it it ] @ |
|---|
| 290 | move ? localss false dst RegisterA). |
|---|
| 291 | |
|---|
| 292 | definition translate_address : |
|---|
| 293 | ∀globals.nat → bool → ∀i.i ∈ globals → decision → decision → |
|---|
| 294 | list (joint_seq LTL globals) ≝ |
|---|
| 295 | λglobals,localss,carry_lives_after,id,prf,addr1,addr2. |
|---|
| 296 | preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2)) |
|---|
| 297 | (ADDRESS LTL ? id prf it it :: |
|---|
| 298 | move ? localss false addr1 RegisterDPL @ |
|---|
| 299 | move ? localss false addr2 RegisterDPH). |
|---|
| 300 | |
|---|
| 301 | definition translate_low_address : |
|---|
| 302 | ∀globals.nat → bool → decision → label → |
|---|
| 303 | list (joint_seq LTL globals) ≝ |
|---|
| 304 | λglobals,localss,carry_lives_after,dst,lbl. |
|---|
| 305 | match dst return λ_.list (joint_seq LTL globals) with |
|---|
| 306 | [ decision_colour r ⇒ [LOW_ADDRESS r lbl] |
|---|
| 307 | | _ ⇒ |
|---|
| 308 | LOW_ADDRESS RegisterA lbl :: move ? localss carry_lives_after dst RegisterA |
|---|
| 309 | ]. |
|---|
| 310 | |
|---|
| 311 | definition translate_high_address : |
|---|
| 312 | ∀globals.nat → bool → decision → label → |
|---|
| 313 | list (joint_seq LTL globals) ≝ |
|---|
| 314 | λglobals,localss,carry_lives_after,dst,lbl. |
|---|
| 315 | match dst return λ_.list (joint_seq LTL globals) with |
|---|
| 316 | [ decision_colour r ⇒ [HIGH_ADDRESS r lbl] |
|---|
| 317 | | _ ⇒ |
|---|
| 318 | HIGH_ADDRESS RegisterA lbl :: move ? localss carry_lives_after dst RegisterA |
|---|
| 319 | ]. |
|---|
| 320 | |
|---|
| 321 | definition translate_step: |
|---|
| 322 | ∀globals.nat → ∀after : valuation register_lattice. |
|---|
| 323 | coloured_graph after → |
|---|
| 324 | ℕ → label → joint_step ERTLptr globals → bind_step_block LTL globals ≝ |
|---|
| 325 | λglobals,localss,after,grph,stack_sz,lbl,s. |
|---|
| 326 | bret … ( |
|---|
| 327 | let lookup ≝ λr.colouring … grph (inl … r) in |
|---|
| 328 | let lookup_arg ≝ λa.match a with |
|---|
| 329 | [ Reg r ⇒ lookup r |
|---|
| 330 | | Imm b ⇒ arg_decision_imm b |
|---|
| 331 | ] in |
|---|
| 332 | let carry_lives_after ≝ hlives RegisterCarry (after lbl) in |
|---|
| 333 | let move ≝ move globals localss carry_lives_after in |
|---|
| 334 | if eliminable_step … (after lbl) s then ([ ] : step_block LTL globals) else |
|---|
| 335 | match s with |
|---|
| 336 | [ step_seq s' ⇒ |
|---|
| 337 | match s' return λ_.step_block LTL globals with |
|---|
| 338 | [ COMMENT c ⇒ [COMMENT … c] |
|---|
| 339 | | POP r ⇒ |
|---|
| 340 | POP … A :: |
|---|
| 341 | move (lookup r) RegisterA |
|---|
| 342 | | PUSH a ⇒ |
|---|
| 343 | move RegisterA (lookup_arg a) @ |
|---|
| 344 | [ PUSH … A ] |
|---|
| 345 | | STORE addr1 addr2 srcr ⇒ |
|---|
| 346 | translate_store ? localss carry_lives_after |
|---|
| 347 | (lookup_arg addr1) |
|---|
| 348 | (lookup_arg addr2) |
|---|
| 349 | (lookup_arg srcr) |
|---|
| 350 | | LOAD dstr addr1 addr2 ⇒ |
|---|
| 351 | translate_load ? localss carry_lives_after |
|---|
| 352 | (lookup dstr) |
|---|
| 353 | (lookup_arg addr1) |
|---|
| 354 | (lookup_arg addr2) |
|---|
| 355 | | CLEAR_CARRY ⇒ [CLEAR_CARRY ??] |
|---|
| 356 | | SET_CARRY ⇒ [SET_CARRY ??] |
|---|
| 357 | | OP2 op dst arg1 arg2 ⇒ |
|---|
| 358 | translate_op2_smart ? localss carry_lives_after op |
|---|
| 359 | (lookup dst) |
|---|
| 360 | (lookup_arg arg1) |
|---|
| 361 | (lookup_arg arg2) |
|---|
| 362 | | OP1 op dst arg ⇒ |
|---|
| 363 | translate_op1 ? localss carry_lives_after op |
|---|
| 364 | (lookup dst) |
|---|
| 365 | (lookup arg) |
|---|
| 366 | | MOVE pair_regs ⇒ |
|---|
| 367 | let lookup_move_dst ≝ λx.match x return λ_.decision with |
|---|
| 368 | [ PSD r ⇒ lookup r |
|---|
| 369 | | HDW r ⇒ r |
|---|
| 370 | ] in |
|---|
| 371 | let dst ≝ lookup_move_dst (\fst pair_regs) in |
|---|
| 372 | let src ≝ |
|---|
| 373 | match \snd pair_regs return λ_.arg_decision with |
|---|
| 374 | [ Reg r ⇒ lookup_move_dst r |
|---|
| 375 | | Imm b ⇒ arg_decision_imm b |
|---|
| 376 | ] in |
|---|
| 377 | move dst src |
|---|
| 378 | | ADDRESS lbl prf dpl dph ⇒ |
|---|
| 379 | translate_address ? localss carry_lives_after |
|---|
| 380 | lbl prf (lookup dpl) (lookup dph) |
|---|
| 381 | | OPACCS op dst1 dst2 arg1 arg2 ⇒ |
|---|
| 382 | translate_opaccs ? localss carry_lives_after op |
|---|
| 383 | (lookup dst1) (lookup dst2) |
|---|
| 384 | (lookup_arg arg1) (lookup_arg arg2) |
|---|
| 385 | | extension_seq ext ⇒ |
|---|
| 386 | match ext with |
|---|
| 387 | [ ertlptr_ertl ext' ⇒ |
|---|
| 388 | match ext' with |
|---|
| 389 | [ ertl_new_frame ⇒ newframe ? stack_sz |
|---|
| 390 | | ertl_del_frame ⇒ delframe ? stack_sz |
|---|
| 391 | | ertl_frame_size r ⇒ |
|---|
| 392 | move (lookup r) (arg_decision_imm (byte_of_nat stack_sz)) |
|---|
| 393 | ] |
|---|
| 394 | | LOW_ADDRESS r1 l ⇒ |
|---|
| 395 | translate_low_address ? localss carry_lives_after (lookup r1) l |
|---|
| 396 | | HIGH_ADDRESS r1 l ⇒ |
|---|
| 397 | translate_high_address ? localss carry_lives_after (lookup r1) l |
|---|
| 398 | ] |
|---|
| 399 | ] |
|---|
| 400 | | COST_LABEL cost_lbl ⇒ 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉 |
|---|
| 401 | | COND r ltrue ⇒ |
|---|
| 402 | 〈add_dummy_variance … (move RegisterA (lookup r)),λ_.COND … it ltrue, [ ]〉 |
|---|
| 403 | | CALL f n_args _ ⇒ |
|---|
| 404 | match f with |
|---|
| 405 | [ inl f ⇒ |
|---|
| 406 | 〈[ ],λ_.CALL LTL ? (inl … f) n_args it, [ ]〉 |
|---|
| 407 | | inr dp ⇒ |
|---|
| 408 | let 〈dpl, dph〉 ≝ dp in |
|---|
| 409 | 〈add_dummy_variance … (move_to_dp ? localss (lookup_arg dpl) (lookup_arg dph)), |
|---|
| 410 | λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉 |
|---|
| 411 | ] |
|---|
| 412 | ]). |
|---|
| 413 | |
|---|
| 414 | definition translate_fin_step: |
|---|
| 415 | ∀globals.label → joint_fin_step ERTLptr → bind_fin_block LTL globals ≝ |
|---|
| 416 | λglobals,lbl,s. |
|---|
| 417 | bret … (〈[ ], |
|---|
| 418 | match s with |
|---|
| 419 | [ RETURN ⇒ RETURN ? |
|---|
| 420 | | GOTO l ⇒ GOTO ? l |
|---|
| 421 | | TAILCALL abs _ _ ⇒ Ⓧabs |
|---|
| 422 | ]〉). |
|---|
| 423 | |
|---|
| 424 | definition translate_data : |
|---|
| 425 | fixpoint_computer → coloured_graph_computer → |
|---|
| 426 | ∀globals. |
|---|
| 427 | joint_closed_internal_function ERTLptr globals → |
|---|
| 428 | bind_new register (b_graph_translate_data ERTLptr LTL globals) ≝ |
|---|
| 429 | λthe_fixpoint,build,globals,int_fun. |
|---|
| 430 | (* colour registers *) |
|---|
| 431 | let after ≝ analyse_liveness the_fixpoint globals int_fun in |
|---|
| 432 | let coloured_graph ≝ build … int_fun after in |
|---|
| 433 | (* compute new stack size *) |
|---|
| 434 | let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in |
|---|
| 435 | bret … |
|---|
| 436 | (mk_b_graph_translate_data ERTLptr LTL globals |
|---|
| 437 | (* init_ret ≝ *) it |
|---|
| 438 | (* init_params ≝ *) it |
|---|
| 439 | (* init_stack_size ≝ *) stack_sz |
|---|
| 440 | (* added_prologue ≝ *) [ ] |
|---|
| 441 | (* new_regs ≝ *) [ ] |
|---|
| 442 | (* f_step ≝ *) (translate_step ? (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz) |
|---|
| 443 | (* f_fin ≝ *) (translate_fin_step globals) |
|---|
| 444 | ????). |
|---|
| 445 | @hide_prf |
|---|
| 446 | [ |
|---|
| 447 | | #l #c % ] |
|---|
| 448 | cases daemon (* TODO *) |
|---|
| 449 | qed. |
|---|
| 450 | |
|---|
| 451 | (* Paolo: does it really have sense to do here the first stack address computation, |
|---|
| 452 | when it is an info easily available from any program in the back end? |
|---|
| 453 | Also, is it really 2^16 - |globals|, or should there also be a -1? *) |
|---|
| 454 | definition ertlptr_to_ltl: |
|---|
| 455 | fixpoint_computer → coloured_graph_computer → ertlptr_program → |
|---|
| 456 | ltl_program × stack_cost_model × nat ≝ |
|---|
| 457 | λthe_fixpoint,build,pr. |
|---|
| 458 | let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in |
|---|
| 459 | 〈ltlprog, stack_cost … ltlprog, 2^16 - globals_stacksize … ltlprog〉. |
|---|
| 460 | % |
|---|
| 461 | qed. |
|---|
