Changeset 1568 for Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml
 Timestamp:
 Nov 25, 2011, 7:43:39 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml
r1542 r1568 40 40 let l = generate (LTL.St_load l) in 41 41 let l = generate (LTL.St_from_acc (I8051.dph, l)) in 42 let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in42 let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in 43 43 let l = generate (LTL.St_int (I8051.a, 0, l)) in 44 44 let l = generate (LTL.St_from_acc (I8051.dpl, l)) in 45 let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in45 let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in 46 46 LTL.St_int (I8051.a, off, l) 47 47 48 let set_stack_preamble off l = 49 let off = adjust off in 50 let l = generate (LTL.St_from_acc (I8051.dph, l)) in 51 let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in 52 let l = generate (LTL.St_int (I8051.a, 0, l)) in 53 let l = generate (LTL.St_from_acc (I8051.dpl, l)) in 54 let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in 55 LTL.St_int (I8051.a, off, l) 56 48 57 let set_stack off r l = 49 let off = adjust off in50 58 let l = generate (LTL.St_store l) in 51 59 let l = generate (LTL.St_to_acc (r, l)) in 52 let l = generate (LTL.St_from_acc (I8051.dph, l)) in 53 let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in 54 let l = generate (LTL.St_int (I8051.a, 0, l)) in 55 let l = generate (LTL.St_from_acc (I8051.dpl, l)) in 56 let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in 57 LTL.St_int (I8051.a, off, l) 58 59 60 let write (r : Register.t) (l : Label.t) : (I8051.register * Label.t) = 61 match lookup r with 62 63  Color hwr > 64 (* Pseudoregister [r] has been mapped to hardware register 65 [hwr]. Just write into [hwr] and branch to [l]. *) 66 (hwr, l) 67 68  Spill off > 69 (* Pseudoregister [r] has been mapped to offset [off] in the local zone 70 of the stack. Then, write into [sst] (never allocated) and transfer 71 control to an instruction that copies [sst] in the designated 72 location of the stack before branching to [l]. *) 73 (I8051.sst, generate (set_stack off I8051.sst l)) 74 75 76 let read (r : Register.t) (stmt : I8051.register > LTL.statement) = 77 match lookup r with 78  Color hwr > 79 (* Pseudoregister [r] has been mapped to hardware register [hwr]. Just 80 generate statement [stmt] with a reference to register [hwr]. *) 81 generate (stmt hwr) 82 83  Spill off > 84 (* Pseudoregister [r] has been mapped to offset [off] in the local zone 85 of the stack. Issue a statement that copies the designated area in 86 the stack into the temporary unallocatable hardware register [sst], 87 then generate statement [stmt] with a reference to register 88 [sst]. *) 89 let temphwr = I8051.sst in 90 let l = generate (stmt temphwr) in 91 generate (get_stack temphwr off l) 60 set_stack_preamble off l 61 62 let set_stack_int off k l = 63 let l = generate (LTL.St_store l) in 64 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) *) 92 99 93 100 … … 100 107  Color desthwr, Color sourcehwr when I8051.eq_reg desthwr sourcehwr > 101 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) 102 113  Color desthwr, Color sourcehwr > 103 114 let l = generate (LTL.St_from_acc (desthwr, l)) in … … 119 130 get_stack temphwr off2 l 120 131 132 let move_int (dest : decision) (k : int) l = 133 match dest with 134  Color desthwr > LTL.St_int (desthwr, k, l) 135  Spill off > set_stack_int off k l 136 137 let op2 op (dest : decision) (src1 : decision) (src2 : decision) l = 138 let l = generate (move dest (Color I8051.a) l) in 139 match op, src1, src2 with 140  _, _, Color src2hwr > 141 let l = generate (LTL.St_op2 (op, LTL.Reg src2hwr, l)) in 142 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, _ > 145 let l = generate (LTL.St_op2 (op, LTL.Reg src1hwr, l)) in 146 move (Color I8051.a) src2 l 147 (* otherwise we have to use b *) 148  _ > 149 let l = generate (LTL.St_op2 (op, LTL.Reg I8051.b, l)) in 150 let l = generate (move (Color I8051.a) src1 l) in 151 move (Color I8051.b) src2 l 152 153 let move_to_dptr (addr1 : decision) (addr2 : decision) l = 154 match addr1, addr2 with 155  Color _, _ > 156 (* the following does not change dph, as addr1 is hwr *) 157 let l = generate (move (Color I8051.dpl) addr1 l) in 158 move (Color I8051.dph) addr2 l 159  _, Color _ > 160 (* the following does not change dph, as addr1 is hwr *) 161 let l = generate (move (Color I8051.dph) addr2 l) in 162 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 = 169 let l = generate (LTL.St_store l) in 170 match srcr with 171  Color _ > 172 let l = generate (move (Color I8051.a) srcr l) in 173 move_to_dptr addr1 addr2 l 174  _ > 175 let l = generate (LTL.St_to_acc (I8051.st0, l)) in 176 let l = generate (move_to_dptr addr1 addr2 l) in 177 move (Color I8051.st0) srcr l 121 178 122 179 let newframe l = … … 124 181 else 125 182 let l = generate (LTL.St_from_acc (I8051.sph, l)) in 126 let l = generate (LTL.St_op2 (I8051.Sub, I8051.dph, l)) in 127 let l = generate (LTL.St_int (I8051.dph, 0, l)) in 183 let l = generate (LTL.St_op2 (I8051.Sub, LTL.Imm 0, l)) in 128 184 let l = generate (LTL.St_to_acc (I8051.sph, l)) in 129 185 let l = generate (LTL.St_from_acc (I8051.spl, l)) in 130 let l = generate (LTL.St_op2 (I8051.Sub, I8051.dpl, l)) in186 let l = generate (LTL.St_op2 (I8051.Sub, LTL.Imm stacksize, l)) in 131 187 let l = generate (LTL.St_clear_carry l) in 132 let l = generate (LTL.St_int (I8051.dpl, stacksize, l)) in133 188 LTL.St_to_acc (I8051.spl, l) 134 189 … … 137 192 else 138 193 let l = generate (LTL.St_from_acc (I8051.sph, l)) in 139 let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in194 let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in 140 195 let l = generate (LTL.St_int (I8051.a, 0, l)) in 141 196 let l = generate (LTL.St_from_acc (I8051.spl, l)) in 142 let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in143 LTL.St_ int (I8051.a, stacksize, l)197 let l = generate (LTL.St_op2 (I8051.Add, LTL.Imm stacksize, l)) in 198 LTL.St_to_acc (I8051.spl, l) 144 199 145 200 … … 174 229 move (lookup destr) (Color sourcehwr) l 175 230 176  ERTL.St_set_hdw (desthwr, sourcer, l) >231  ERTL.St_set_hdw (desthwr, RTL.Reg sourcer, l) > 177 232 move (Color desthwr) (lookup sourcer) l 178 233 234  ERTL.St_set_hdw (desthwr, RTL.Imm k, l) > 235 move_int (Color desthwr) k l 236 179 237  ERTL.St_hdw_to_hdw (r1, r2, l) > 180 let l = generate (LTL.St_from_acc (r1, l)) in 181 LTL.St_to_acc (r2, l) 238 move (Color r1) (Color r2) l 182 239 183 240  ERTL.St_newframe l > … … 188 245 189 246  ERTL.St_framesize (r, l) > 190 let (hdw, l) = write r l in 191 LTL.St_int (hdw, stacksize, l) 247 move_int (lookup r) stacksize l 192 248 193 249  ERTL.St_pop (r, l) > 194 let (hdw, l) = write r l in 195 let l = generate (LTL.St_from_acc (hdw, l)) in 250 let l = generate (move (lookup r) (Color I8051.a) l) in 196 251 LTL.St_pop l 197 252 198 253  ERTL.St_push (r, l) > 199 254 let l = generate (LTL.St_push l) in 200 let l = read r (fun hdw > LTL.St_to_acc (hdw, l)) in 201 LTL.St_skip l 255 move (Color I8051.a) (lookup r) l 202 256 203 257  ERTL.St_addrH (r, x, l) > 204 let (hdw, l) = write r l in 205 let l = generate (LTL.St_from_acc (hdw, l)) in 206 let l = generate (LTL.St_to_acc (I8051.dph, l)) in 258 let l = generate (move (lookup r) (Color I8051.dph) l) in 207 259 LTL.St_addr (x, l) 208 260 209 261  ERTL.St_addrL (r, x, l) > 210 let (hdw, l) = write r l in 211 let l = generate (LTL.St_from_acc (hdw, l)) in 212 let l = generate (LTL.St_to_acc (I8051.dpl, l)) in 262 let l = generate (move (lookup r) (Color I8051.dpl) l) in 213 263 LTL.St_addr (x, l) 214 264 215  ERTL.St_int (r, i, l) > 216 let (hdw, l) = write r l in 217 LTL.St_int (hdw, i, l) 218 219  ERTL.St_move (r1, r2, l) > 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) > 220 269 move (lookup r1) (lookup r2) l 221 270 222 271  ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) > 223 let (hdw, l) = write destr l in 224 let l = generate (LTL.St_from_acc (hdw, l)) in 272 let l = generate (move (lookup destr) (Color I8051.a) l) in 225 273 let l = generate (LTL.St_opaccs (opaccs, l)) in 226 let l = read srcr1 (fun hdw > LTL.St_to_acc (hdw, l)) in 227 let l = generate (LTL.St_from_acc (I8051.b, l)) in 228 let l = read srcr2 (fun hdw > LTL.St_to_acc (hdw, l)) in 229 LTL.St_skip l 274 let l = generate (move (Color I8051.a) (lookup srcr1) l) in 275 move (Color I8051.b) (lookup srcr2) l 230 276 231 277  ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) > 232 let (hdw, l) = write destr l in 233 let l = generate (LTL.St_from_acc (hdw, l)) in 234 let l = generate (LTL.St_to_acc (I8051.b, l)) in 278 let l = generate (move (lookup destr) (Color I8051.b) l) in 235 279 let l = generate (LTL.St_opaccs (opaccs, l)) in 236 let l = read srcr1 (fun hdw > LTL.St_to_acc (hdw, l)) in 237 let l = generate (LTL.St_from_acc (I8051.b, l)) in 238 let l = read srcr2 (fun hdw > LTL.St_to_acc (hdw, l)) in 239 LTL.St_skip l 280 let l = generate (move (Color I8051.a) (lookup srcr1) l) in 281 move (Color I8051.b) (lookup srcr2) l 240 282 241 283  ERTL.St_op1 (op1, destr, srcr, l) > 242 let (hdw, l) = write destr l in 243 let l = generate (LTL.St_from_acc (hdw, l)) in 284 let l = generate (move (lookup destr) (Color I8051.a) l) in 244 285 let l = generate (LTL.St_op1 (op1, l)) in 245 let l = read srcr (fun hdw > LTL.St_to_acc (hdw, l)) in 246 LTL.St_skip l 247 248  ERTL.St_op2 (op2, destr, srcr1, srcr2, l) > 249 let (hdw, l) = write destr l in 250 let l = generate (LTL.St_from_acc (hdw, l)) in 251 let l = generate (LTL.St_op2 (op2, I8051.b, l)) in 252 let l = read srcr1 (fun hdw > LTL.St_to_acc (hdw, l)) in 253 let l = generate (LTL.St_from_acc (I8051.b, l)) in 254 let l = read srcr2 (fun hdw > LTL.St_to_acc (hdw, l)) in 255 LTL.St_skip l 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 256 295 257 296  ERTL.St_clear_carry l > … … 261 300 LTL.St_set_carry l 262 301 302 (* act differently on hardware registers? if at least one of 303 the address bytes is hdw use of st0 can be avoided. And in 304 case of nonhdw, the read could actually target a register 305 directly *) 263 306  ERTL.St_load (destr, addr1, addr2, l) > 264 let (hdw, l) = write destr l in 265 let l = generate (LTL.St_from_acc (hdw, l)) in 266 let l = generate (LTL.St_load l) in 267 let l = generate (LTL.St_from_acc (I8051.dph, l)) in 268 let l = generate (LTL.St_to_acc (I8051.st0, l)) in 269 let l = generate (LTL.St_from_acc (I8051.dpl, l)) in 270 let l = read addr1 (fun hdw > LTL.St_to_acc (hdw, l)) in 271 let l = generate (LTL.St_from_acc (I8051.st0, l)) in 272 let l = read addr2 (fun hdw > LTL.St_to_acc (hdw, l)) in 273 LTL.St_skip l 307 let l = generate (move (lookup destr) (Color I8051.a) l) in 308 let l = generate (LTL.St_load l) in 309 move_to_dptr (lookup addr1) (lookup addr2) l 274 310 275 311  ERTL.St_store (addr1, addr2, srcr, l) > 276 let l = generate (LTL.St_store l) in 277 let l = generate (LTL.St_to_acc (I8051.st1, l)) in 278 let l = generate (LTL.St_from_acc (I8051.dph, l)) in 279 let l = generate (LTL.St_to_acc (I8051.st0, l)) in 280 let l = generate (LTL.St_from_acc (I8051.dpl, l)) in 281 let l = read addr1 (fun hdw > LTL.St_to_acc (hdw, l)) in 282 let l = generate (LTL.St_from_acc (I8051.st0, l)) in 283 let l = read addr2 (fun hdw > LTL.St_to_acc (hdw, l)) in 284 let l = generate (LTL.St_from_acc (I8051.st1, l)) in 285 let l = read srcr (fun hdw > LTL.St_to_acc (hdw, l)) in 286 LTL.St_skip l 312 store (lookup addr1) (lookup addr2) (lookup srcr) l 287 313 288 314  ERTL.St_call_id (f, _, l) > … … 291 317  ERTL.St_call_ptr (f1, f2, _, l) > 292 318 let l = generate (LTL.St_call_ptr l) in 293 let l = generate (LTL.St_from_acc (I8051.dph, l)) in 294 let l = generate (LTL.St_to_acc (I8051.st0, l)) in 295 let l = generate (LTL.St_from_acc (I8051.dpl, l)) in 296 let l = read f1 (fun hdw > LTL.St_to_acc (hdw, l)) in 297 let l = generate (LTL.St_from_acc (I8051.st0, l)) in 298 let l = read f2 (fun hdw > LTL.St_to_acc (hdw, l)) in 299 LTL.St_skip l 319 move_to_dptr (lookup f1) (lookup f2) l 300 320 301 321  ERTL.St_cond (srcr, lbl_true, lbl_false) > 302 322 let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in 303 let l = read srcr (fun hdw > LTL.St_to_acc (hdw, l)) in 304 LTL.St_skip l 323 move (Color I8051.a) (lookup srcr) l 305 324 306 325  ERTL.St_return _ >
Note: See TracChangeset
for help on using the changeset viewer.