Changeset 1572 for Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml
 Timestamp:
 Nov 28, 2011, 3:13:14 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml
r1568 r1572 33 33 open I8051 34 34 35 36 type argument = 37  AColor of I8051.register 38  ASpill of AST.immediate 39  AImm of AST.immediate 40 41 let lookup_as_arg r = match lookup r with 42  Spill k > ASpill k 43  Color r > AColor r 44 45 let lookup_arg = function 46  RTL.Imm k > AImm k 47  RTL.Reg r > lookup_as_arg r 48 35 49 let adjust off = locals  (off + I8051.int_size) 36 50 37 let get_stack r off l = 38 let off = adjust off in 39 let l = generate (LTL.St_from_acc (r, l)) in 40 let l = generate (LTL.St_load l) in 41 let l = generate (LTL.St_from_acc (I8051.dph, l)) in 42 let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in 43 let l = generate (LTL.St_int (I8051.a, 0, l)) in 44 let l = generate (LTL.St_from_acc (I8051.dpl, l)) in 45 let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in 46 LTL.St_int (I8051.a, off, l) 47 48 let set_stack_preamble off l = 51 (* sideeffects : dpl, dph, a *) 52 let move_sp_to_dptr off l = 49 53 let off = adjust off in 50 54 let l = generate (LTL.St_from_acc (I8051.dph, l)) in … … 55 59 LTL.St_int (I8051.a, off, l) 56 60 57 let set_stack off r l = 61 62 (* sideeffects : dpl, dph, a *) 63 let get_stack r off l = 64 let l = 65 if I8051.eq_reg r I8051.a then l else generate (LTL.St_from_acc (r, l)) in 66 let l = generate (LTL.St_load l) in 67 move_sp_to_dptr off l 68 69 (* sideeffects : dpl, dph, a *) 70 let set_stack_not_a off r l = 58 71 let l = generate (LTL.St_store l) in 59 72 let l = generate (LTL.St_to_acc (r, l)) in 60 set_stack_preamble off l 61 73 move_sp_to_dptr off l 74 75 (* sideeffects : dpl, dph, sst *) 76 let set_stack_a off l = 77 let l = generate (LTL.St_store l) in 78 let l = generate (set_stack_not_a off I8051.sst l) in 79 LTL.St_from_acc (I8051.st0, l) 80 81 (* sideeffects : dpl, dph, st0 if r = a, a if r != a *) 82 let set_stack off r = 83 if I8051.eq_reg r I8051.a then set_stack_a off else 84 set_stack_not_a off r 85 86 (* sideeffects : dpl, dph, a *) 62 87 let set_stack_int off k l = 63 88 let l = generate (LTL.St_store l) in 64 89 let l = generate (LTL.St_int (I8051.a, k, l)) in 65 set_stack_preamble off l 66 67 (* let write (r : Register.t) (l : Label.t) : (I8051.register * Label.t) = *) 68 (* match lookup r with *) 69 70 (*  Color hwr > *) 71 (* (\* Pseudoregister [r] has been mapped to hardware register *) 72 (* [hwr]. Just write into [hwr] and branch to [l]. *\) *) 73 (* (hwr, l) *) 74 75 (*  Spill off > *) 76 (* (\* Pseudoregister [r] has been mapped to offset [off] in the local zone *) 77 (* of the stack. Then, write into [sst] (never allocated) and transfer *) 78 (* control to an instruction that copies [sst] in the designated *) 79 (* location of the stack before branching to [l]. *\) *) 80 (* (I8051.sst, generate (set_stack off I8051.sst l)) *) 81 82 83 (* let read (r : Register.t) (stmt : I8051.register > LTL.statement) = *) 84 (* match lookup r with *) 85 (*  Color hwr > *) 86 (* (\* Pseudoregister [r] has been mapped to hardware register [hwr]. Just *) 87 (* generate statement [stmt] with a reference to register [hwr]. *\) *) 88 (* generate (stmt hwr) *) 89 90 (*  Spill off > *) 91 (* (\* Pseudoregister [r] has been mapped to offset [off] in the local zone *) 92 (* of the stack. Issue a statement that copies the designated area in *) 93 (* the stack into the temporary unallocatable hardware register [sst], *) 94 (* then generate statement [stmt] with a reference to register *) 95 (* [sst]. *\) *) 96 (* let temphwr = I8051.sst in *) 97 (* let l = generate (stmt temphwr) in *) 98 (* generate (get_stack temphwr off l) *) 99 100 101 let move (dest : decision) (src : decision) l = 102 match dest, src with 103 104 (* Both pseudoregisters are translated to hardware registers. Issue move 105 statements, or no statement at all if both pseudoregisters reside in 106 the same hardware register. *) 107  Color desthwr, Color sourcehwr when I8051.eq_reg desthwr sourcehwr > 108 LTL.St_skip l 109  Color desthwr, Color sourcehwr when I8051.eq_reg desthwr I8051.a > 110 LTL.St_to_acc (sourcehwr, l) 111  Color desthwr, Color sourcehwr when I8051.eq_reg sourcehwr I8051.a > 112 LTL.St_from_acc (desthwr, l) 113  Color desthwr, Color sourcehwr > 114 let l = generate (LTL.St_from_acc (desthwr, l)) in 115 LTL.St_to_acc (sourcehwr, l) 116 117 (* One pseudoregister is translated to a hardware register, while the 118 other is spilled. Issue a single stack access instruction. *) 119  Color desthwr, Spill off > get_stack desthwr off l 120  Spill off, Color sourcehwr > set_stack off sourcehwr l 121 122 (* Both pseudoregisters are spilled. Combine the previous two cases. Of 123 course, if the two pseudoregisters have been spilled into the same 124 stack slot, there is nothing to do. *) 125  Spill off1, Spill off2 when off1 = off2 > 126 LTL.St_skip l 127  Spill off1, Spill off2 > 128 let temphwr = I8051.sst in 129 let l = generate (set_stack off1 temphwr l) in 130 get_stack temphwr off2 l 131 90 move_sp_to_dptr off l 91 92 93 (* sideeffects : (dpl, dph, a) if dest spilled *) 132 94 let move_int (dest : decision) (k : int) l = 133 95 match dest with … … 135 97  Spill off > set_stack_int off k l 136 98 137 let op2 op (dest : decision) (src1 : decision) (src2 : decision) l = 138 let l = generate (move dest (Color I8051.a) l) in 99 (* sideeffects : none if dest = src, a if both colored, 100 (dpl, dph, a) if src spilled or src imm and dest spilled, 101 (dpl, dph, a, sst) if dest spilled *) 102 let move (dest : decision) (src : argument) l = 103 match dest, src with 104  _, AImm k > move_int dest k l 105 (* Both pseudoregisters are translated to hardware registers. Issue move 106 statements, or no statement at all if both pseudoregisters reside in 107 the same hardware register. *) 108  Color desthwr, AColor sourcehwr 109 when I8051.eq_reg desthwr sourcehwr > 110 LTL.St_skip l 111  Color desthwr, AColor sourcehwr 112 when I8051.eq_reg desthwr I8051.a > 113 LTL.St_to_acc (sourcehwr, l) 114  Color desthwr, AColor sourcehwr 115 when I8051.eq_reg sourcehwr I8051.a > 116 LTL.St_from_acc (desthwr, l) 117  Color desthwr, AColor sourcehwr > 118 let l = generate (LTL.St_from_acc (desthwr, l)) in 119 LTL.St_to_acc (sourcehwr, l) 120 121 (* One pseudoregister is translated to a hardware register, while the 122 other is spilled. Issue a single stack access instruction. *) 123  Color desthwr, ASpill off > get_stack desthwr off l 124  Spill off, AColor sourcehwr > set_stack off sourcehwr l 125 126 (* Both pseudoregisters are spilled. Combine the previous two cases. Of 127 course, if the two pseudoregisters have been spilled into the same 128 stack slot, there is nothing to do. *) 129  Spill off1, ASpill off2 when off1 = off2 > 130 LTL.St_skip l 131  Spill off1, ASpill off2 > 132 let l = generate (set_stack_a off1 l) in 133 get_stack I8051.a off2 l 134 135 (* sideeffects (dpl, dph) if either spilled, (dpl, dph, b) if both *) 136 let op2 op (dest : decision) (src1 : argument) (src2 : argument) l = 137 let l = generate (move dest (AColor I8051.a) l) in 139 138 match op, src1, src2 with 140  _, _, Color src2hwr > 139  _, _, AImm k > 140 let l = generate (LTL.St_op2 (op, LTL.Imm k, l)) in 141 move (Color I8051.a) src1 l 142 (* if op is commutative, we can do as above if first is hwr *) 143  (Add  Addc  And  Or  Xor), AImm k, _ > 144 let l = generate (LTL.St_op2 (op, LTL.Imm k, l)) in 145 move (Color I8051.a) src2 l 146  _, _, AColor src2hwr > 141 147 let l = generate (LTL.St_op2 (op, LTL.Reg src2hwr, l)) in 142 148 move (Color I8051.a) src1 l 143 (* if op is commutative, we can do as above if first is hwr *) 144  (Add  Addc  And  Or  Xor), Color src1hwr, _ > 149  (Add  Addc  And  Or  Xor), AColor src1hwr, _ > 145 150 let l = generate (LTL.St_op2 (op, LTL.Reg src1hwr, l)) in 146 151 move (Color I8051.a) src2 l 147 (* otherwise we have to use b *) 148  _ > 152  _, _, _ > 149 153 let l = generate (LTL.St_op2 (op, LTL.Reg I8051.b, l)) in 150 154 let l = generate (move (Color I8051.a) src1 l) in 151 155 move (Color I8051.b) src2 l 152 156 153 let move_to_dptr (addr1 : decision) (addr2 : decision) l = 157 (* sideeffects : a, b if both spilled *) 158 let move_to_dptr (addr1 : argument) (addr2 : argument) l = 154 159 match addr1, addr2 with 155  Color _, _ > 160  ASpill _, ASpill _ > 161 let l = generate (move (Color I8051.dph) (AColor I8051.b) l) in 162 let l = generate (move (Color I8051.dpl) addr1 l) in 163 move (Color I8051.b) addr2 l 164  (AColor _  AImm _) , _ > 156 165 (* the following does not change dph, as addr1 is hwr *) 157 166 let l = generate (move (Color I8051.dpl) addr1 l) in 158 167 move (Color I8051.dph) addr2 l 159  _, Color _>160 (* the following does not change dp h, as addr1is hwr *)168  _, (AColor _  AImm _) > 169 (* the following does not change dpl, as addr2 is hwr *) 161 170 let l = generate (move (Color I8051.dph) addr2 l) in 162 171 move (Color I8051.dpl) addr1 l 163  _ > 164 let l = generate (move (Color I8051.dph) (Color I8051.b) l) in 165 let l = generate (move (Color I8051.dpl) addr1 l) in 166 move (Color I8051.b) addr2 l 167 168 let store addr1 addr2 srcr l = 172 173 (* sideeffects : dpl, dph, b if both addr spilled, 174 st0 if srcr = a or srcr spilled, a if srcrs != a *) 175 let store (addr1 : argument) (addr2 : argument) (srcr : argument) l = 169 176 let l = generate (LTL.St_store l) in 170 177 match srcr with 171  Color _ > 172 let l = generate (move (Color I8051.a) srcr l) in 178  AColor r when I8051.eq_reg r a > 179 let l = generate (LTL.St_to_acc (I8051.st0, l)) in 180 let l = generate (move_to_dptr addr1 addr2 l) in 181 LTL.St_from_acc (I8051.st0, l) 182  AColor r > 183 let l = generate (LTL.St_to_acc (r, l)) in 173 184 move_to_dptr addr1 addr2 l 174  _ > 185  AImm k > 186 let l = generate (LTL.St_int (I8051.a, k, l)) in 187 move_to_dptr addr1 addr2 l 188  ASpill _ > 175 189 let l = generate (LTL.St_to_acc (I8051.st0, l)) in 176 190 let l = generate (move_to_dptr addr1 addr2 l) in … … 227 241 228 242  ERTL.St_get_hdw (destr, sourcehwr, l) > 229 move (lookup destr) (Color sourcehwr) l 230 231  ERTL.St_set_hdw (desthwr, RTL.Reg sourcer, l) > 232 move (Color desthwr) (lookup sourcer) l 233 234  ERTL.St_set_hdw (desthwr, RTL.Imm k, l) > 235 move_int (Color desthwr) k l 243 move (lookup destr) (AColor sourcehwr) l 244 245  ERTL.St_set_hdw (desthwr, sourcer, l) > 246 move (Color desthwr) (lookup_arg sourcer) l 236 247 237 248  ERTL.St_hdw_to_hdw (r1, r2, l) > 238 move (Color r1) ( Color r2) l249 move (Color r1) (AColor r2) l 239 250 240 251  ERTL.St_newframe l > … … 248 259 249 260  ERTL.St_pop (r, l) > 250 let l = generate (move (lookup r) ( Color I8051.a) l) in261 let l = generate (move (lookup r) (AColor I8051.a) l) in 251 262 LTL.St_pop l 252 263 253 264  ERTL.St_push (r, l) > 254 265 let l = generate (LTL.St_push l) in 255 move (Color I8051.a) (lookup r) l266 move (Color I8051.a) (lookup_arg r) l 256 267 257 268  ERTL.St_addrH (r, x, l) > 258 let l = generate (move (lookup r) ( Color I8051.dph) l) in269 let l = generate (move (lookup r) (AColor I8051.dph) l) in 259 270 LTL.St_addr (x, l) 260 271 261 272  ERTL.St_addrL (r, x, l) > 262 let l = generate (move (lookup r) ( Color I8051.dpl) l) in273 let l = generate (move (lookup r) (AColor I8051.dpl) l) in 263 274 LTL.St_addr (x, l) 264 275 265  ERTL.St_move (r, RTL.Imm i, l) > 266 move_int (lookup r) i l 267 268  ERTL.St_move (r1, RTL.Reg r2, l) > 269 move (lookup r1) (lookup r2) l 276  ERTL.St_move (r, a, l) > 277 move (lookup r) (lookup_arg a) l 270 278 271 279  ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) > 272 let l = generate (move (lookup destr) ( Color I8051.a) l) in280 let l = generate (move (lookup destr) (AColor I8051.a) l) in 273 281 let l = generate (LTL.St_opaccs (opaccs, l)) in 274 let l = generate (move (Color I8051.a) (lookupsrcr1) l) in275 move (Color I8051.b) (lookup srcr2) l282 let l = generate (move (Color I8051.a) (lookup_arg srcr1) l) in 283 move (Color I8051.b) (lookup_arg srcr2) l 276 284 277 285  ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) > 278 let l = generate (move (lookup destr) ( Color I8051.b) l) in286 let l = generate (move (lookup destr) (AColor I8051.b) l) in 279 287 let l = generate (LTL.St_opaccs (opaccs, l)) in 280 let l = generate (move (Color I8051.a) (lookup srcr1) l) in281 move (Color I8051.b) (lookup srcr2) l288 let l = generate (move (Color I8051.a) (lookup_arg srcr1) l) in 289 move (Color I8051.b) (lookup_arg srcr2) l 282 290 283 291  ERTL.St_op1 (op1, destr, srcr, l) > 284 let l = generate (move (lookup destr) ( Color I8051.a) l) in292 let l = generate (move (lookup destr) (AColor I8051.a) l) in 285 293 let l = generate (LTL.St_op1 (op1, l)) in 286 move (Color I8051.a) (lookup srcr) l 287 288  ERTL.St_op2 (op, destr, srcr1, RTL.Reg srcr2, l) > 289 op2 op (lookup destr) (lookup srcr1) (lookup srcr2) l 290 291  ERTL.St_op2 (op2, destr, srcr1, RTL.Imm k, l) > 292 let l = generate (move (lookup destr) (Color I8051.a) l) in 293 let l = generate (LTL.St_op2 (op2, LTL.Imm k, l)) in 294 move (Color I8051.a) (lookup srcr1) l 294 move (Color I8051.a) (lookup_as_arg srcr) l 295 296  ERTL.St_op2 (op, destr, arg1, arg2, l) > 297 op2 op (lookup destr) (lookup_arg arg1) (lookup_arg arg2) l 295 298 296 299  ERTL.St_clear_carry l > … … 300 303 LTL.St_set_carry l 301 304 302 (* act differently on hardware registers? if at least one of303 the address bytes is hdw use of st0 can be avoided. And in304 case of nonhdw, the read could actually target a register305 directly *)306 305  ERTL.St_load (destr, addr1, addr2, l) > 307 let l = generate (move (lookup destr) ( Color I8051.a) l) in306 let l = generate (move (lookup destr) (AColor I8051.a) l) in 308 307 let l = generate (LTL.St_load l) in 309 move_to_dptr (lookup addr1) (lookupaddr2) l308 move_to_dptr (lookup_arg addr1) (lookup_arg addr2) l 310 309 311 310  ERTL.St_store (addr1, addr2, srcr, l) > 312 store (lookup addr1) (lookup addr2) (lookupsrcr) l311 store (lookup_arg addr1) (lookup_arg addr2) (lookup_arg srcr) l 313 312 314 313  ERTL.St_call_id (f, _, l) > … … 317 316  ERTL.St_call_ptr (f1, f2, _, l) > 318 317 let l = generate (LTL.St_call_ptr l) in 319 move_to_dptr (lookup f1) (lookupf2) l318 move_to_dptr (lookup_as_arg f1) (lookup_as_arg f2) l 320 319 321 320  ERTL.St_cond (srcr, lbl_true, lbl_false) > 322 321 let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in 323 move (Color I8051.a) (lookup srcr) l322 move (Color I8051.a) (lookup_as_arg srcr) l 324 323 325 324  ERTL.St_return _ >
Note: See TracChangeset
for help on using the changeset viewer.