Changeset 1568 for Deliverables
- Timestamp:
- Nov 25, 2011, 7:43:39 PM (8 years ago)
- Location:
- Deliverables/D2.2/8051/src
- Files:
-
- 29 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml
r1542 r1568 1007 1007 memory, we must increment by 5, as we added two new instructions. *) 1008 1008 let to_ljmp = `REL (vect_of_int 2 `Eight) in 1009 let offset = 5 in1009 (* let offset = 5 in *) 1010 1010 let jmp_address, translated_jump = 1011 1011 match i with … … 1452 1452 ;; 1453 1453 1454 let unopt = function Some x -> x | None -> invalid_arg "None" 1455 1454 1456 let serial_port_input status in_cont = 1455 1457 (* Serial port input *) … … 1495 1497 serial_v_in = Some (`Eight b) } 1496 1498 else 1497 (* Warning about incomplete case analysis here, but safe as we've already tested for 1498 None. *) 1499 let Some e = status.serial_epsilon_in in 1500 let Some v = status.serial_v_in in 1499 (* safe as we've already tested for None. *) 1500 let e = unopt status.serial_epsilon_in in 1501 let v = unopt status.serial_v_in in 1501 1502 if status.clock >= e then 1502 1503 match v with … … 1534 1535 serial_v_in = Some (`Nine (b, b')) } 1535 1536 else 1536 (* Warning about incomplete case analysis here, but safe as we've already tested for 1537 None. *) 1538 let Some e = status.serial_epsilon_in in 1539 let Some v = status.serial_v_in in 1537 (* safe as we've already tested for None. *) 1538 let e = unopt status.serial_epsilon_in in 1539 let v = unopt status.serial_v_in in 1540 1540 if status.clock >= e then 1541 1541 match v with -
Deliverables/D2.2/8051/src/ASM/I8051.ml
r1488 r1568 11 11 | Cmpl 12 12 | Inc 13 (* | Dec *) 14 | Rl 13 15 14 16 type op2 = … … 27 29 | Cmpl -> "cmpl" 28 30 | Inc -> "inc" 31 | Rl -> "rotl" 29 32 30 33 let print_op2 = function … … 57 60 | Cmpl -> Val.cmpl 58 61 | Inc -> Val.succ 62 | Rl -> Val.rotl 59 63 60 64 let op2 carry op2 v1 v2 = match op2 with -
Deliverables/D2.2/8051/src/ASM/I8051.mli
r1488 r1568 9 9 | Cmpl 10 10 | Inc 11 (* | Dec *) 12 | Rl 11 13 12 14 type op2 = -
Deliverables/D2.2/8051/src/ERTL/ERTL.mli
r1542 r1568 38 38 type registers = Register.t list 39 39 40 type argument = RTL.argument 41 40 42 type statement = 41 43 … … 63 65 are the destination hardware register, the source pseudo register, and the 64 66 label of the next statement. *) 65 | St_set_hdw of I8051.register * Register.t * Label.t67 | St_set_hdw of I8051.register * argument * Label.t 66 68 67 69 (* Assign the content of a hardware register to a hardware … … 101 103 | St_addrL of Register.t * AST.ident * Label.t 102 104 103 (* Assign an integer constant to a register. Parameters are the destination104 register, the integer and the label of the next statement.*)105 | St_int of Register.t * int * Label.t105 (* (\* Assign an integer constant to a register. Parameters are the destination *) 106 (* register, the integer and the label of the next statement. *\) *) 107 (* | St_int of Register.t * int * Label.t *) 106 108 107 109 (* Move the content of a register to another. Parameters are the destination 108 110 register, the source register, and the label of the next statement. *) 109 | St_move of Register.t * Register.t * Label.t111 | St_move of Register.t * argument * Label.t 110 112 111 113 (* Apply a binary operation that will later be translated in an operation on … … 127 129 (* Apply a binary operation. Parameters are the operation, the destination 128 130 register, the source registers, and the label of the next statement. *) 129 | St_op2 of I8051.op2 * Register.t * Register.t * Register.t * Label.t131 | St_op2 of I8051.op2 * Register.t * Register.t * argument * Label.t 130 132 131 133 (* Set the carry flag to zero. Parameter is the label of the next -
Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml
r1542 r1568 158 158 else error ("Unknown local register " ^ (Register.print r) ^ ".") 159 159 160 let get_arg a st = match a with 161 | RTL.Imm i -> Val.of_int i 162 | RTL.Reg r -> get_reg (Psd r) st 163 160 164 let push st v = 161 165 let mem = Mem.store st.mem chunk st.isp v in … … 282 286 283 287 | ERTL.St_set_hdw (destr, srcr, lbl) -> 284 let st = add_reg (Hdw destr) (get_ reg (Psd srcr)st) st in288 let st = add_reg (Hdw destr) (get_arg srcr st) st in 285 289 next_pc st lbl 286 290 … … 328 332 next_pc st lbl 329 333 330 | ERTL.St_ int (r,i, lbl) ->334 | ERTL.St_move (r, RTL.Imm i, lbl) -> 331 335 let st = add_reg (Psd r) (Val.of_int i) st in 332 336 next_pc st lbl 333 337 334 | ERTL.St_move (destr, srcr, lbl) ->338 | ERTL.St_move (destr, RTL.Reg srcr, lbl) -> 335 339 let st = add_reg (Psd destr) (get_reg (Psd srcr) st) st in 336 340 next_pc st lbl … … 361 365 Eval.op2 st.carry op2 362 366 (get_reg (Psd srcr1) st) 363 (get_ reg (Psd srcr2)st) in367 (get_arg srcr2 st) in 364 368 let st = change_carry st carry in 365 369 let st = add_reg (Psd destr) v st in -
Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml
r1542 r1568 37 37 let print_result rl = print_reg_list "[" "]" " ; " Register.print rl 38 38 39 let print_arg = function 40 | RTL.Imm i -> string_of_int i 41 | RTL.Reg r -> Register.print r 39 42 40 43 let print_statement = function … … 54 57 | ERTL.St_set_hdw (r1, r2, lbl) -> 55 58 Printf.sprintf "move %s, %s --> %s" 56 (I8051.print_register r1) ( Register.printr2) lbl59 (I8051.print_register r1) (print_arg r2) lbl 57 60 | ERTL.St_hdw_to_hdw (r1, r2, lbl) -> 58 61 Printf.sprintf "move %s, %s --> %s" … … 72 75 | ERTL.St_addrL (dstr, id, lbl) -> 73 76 Printf.sprintf "addrL %s, %s --> %s" (Register.print dstr) id lbl 74 | ERTL.St_int (dstr, i, lbl) ->75 Printf.sprintf "imm %s, %d --> %s" (Register.print dstr) i lbl77 (* | ERTL.St_int (dstr, i, lbl) -> *) 78 (* Printf.sprintf "imm %s, %d --> %s" (Register.print dstr) i lbl *) 76 79 | ERTL.St_move (dstr, srcr, lbl) -> 77 80 Printf.sprintf "move %s, %s --> %s" 78 (Register.print dstr) ( Register.printsrcr) lbl81 (Register.print dstr) (print_arg srcr) lbl 79 82 | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl) -> 80 83 Printf.sprintf "%sA %s, %s, %s --> %s" … … 102 105 (Register.print dstr) 103 106 (Register.print srcr1) 104 ( Register.printsrcr2)107 (print_arg srcr2) 105 108 lbl 106 109 | ERTL.St_clear_carry lbl -> -
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 (* Pseudo-register [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 (* Pseudo-register [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 (* Pseudo-register [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 (* Pseudo-register [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 (* (\* Pseudo-register [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 (* (\* Pseudo-register [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 (* (\* Pseudo-register [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 (* (\* Pseudo-register [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 non-hdw, 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 _ -> -
Deliverables/D2.2/8051/src/ERTL/build.ml
r486 r1568 70 70 let exceptions = 71 71 match stmt with 72 | St_move (_, sourcer, _)73 | St_set_hdw (_, sourcer, _) ->72 | St_move (_, RTL.Reg sourcer, _) 73 | St_set_hdw (_, RTL.Reg sourcer, _) -> 74 74 Liveness.L.psingleton sourcer 75 75 | St_get_hdw (_, sourcehwr, _) -> … … 103 103 let graph = 104 104 match stmt with 105 | St_move (r1, r2, _) ->105 | St_move (r1, RTL.Reg r2, _) -> 106 106 mkppp graph r1 r2 107 107 | St_get_hdw (r, hwr, _) 108 | St_set_hdw (hwr, r, _) ->108 | St_set_hdw (hwr, RTL.Reg r, _) -> 109 109 mkpph graph r hwr 110 110 | _ -> -
Deliverables/D2.2/8051/src/ERTL/liveness.ml
r1542 r1568 30 30 | St_addrH (_, _, l) 31 31 | St_addrL (_, _, l) 32 | St_int (_, _, l)32 (* | St_int (_, _, l) *) 33 33 | St_move (_, _, l) 34 34 | St_opaccsA (_, _, _, _, l) … … 112 112 | St_framesize (r, _) 113 113 | St_pop (r, _) 114 | St_int (r, _, _)114 (* | St_int (r, _, _) *) 115 115 | St_addrH (r, _, _) 116 116 | St_addrL (r, _, _) … … 154 154 | St_addrH _ 155 155 | St_addrL _ 156 | St_int _156 (* | St_int _ *) 157 157 | St_clear_carry _ 158 | St_set_carry _ -> 158 | St_set_carry _ 159 | St_set_hdw (_, RTL.Imm _, _) 160 | St_move (_, RTL.Imm _, _) -> 159 161 L.bottom 160 162 | St_call_id (_, nparams, _) -> … … 169 171 | St_hdw_to_hdw (_, r, _) -> 170 172 L.hsingleton r 171 | St_set_hdw (_, r, _) 173 | St_op2 (I8051.Addc, _, r1, RTL.Reg r2, _) -> 174 L.join (L.join (L.psingleton r1) (L.psingleton r2)) 175 (L.hsingleton I8051.carry) 176 | St_op2 (I8051.Addc, _, r1, RTL.Imm _, _) -> 177 L.join (L.psingleton r1) (L.hsingleton I8051.carry) 178 | St_set_hdw (_, RTL.Reg r, _) 172 179 | St_push (r, _) 173 | St_move (_, r, _)180 | St_move (_, RTL.Reg r, _) 174 181 | St_op1 (_, _, r, _) 182 | St_op2 (_, _, r, RTL.Imm _, _) 175 183 | St_cond (r, _, _) -> 176 184 L.psingleton r 177 | St_op2 (I8051.Addc, _, r1, r2, _) ->178 L.join (L.join (L.psingleton r1) (L.psingleton r2))179 (L.hsingleton I8051.carry)180 185 | St_opaccsA (_, _, r1, r2, _) 181 186 | St_opaccsB (_, _, r1, r2, _) 182 | St_op2 (_, _, r1, r2, _)187 | St_op2 (_, _, r1, RTL.Reg r2, _) 183 188 | St_load (_, r1, r2, _) -> 184 189 L.join (L.psingleton r1) (L.psingleton r2) … … 187 192 | St_newframe _ 188 193 | St_delframe _ -> 189 L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph) 194 L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph) 190 195 | St_return _ -> 191 196 Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved ret_regs … … 224 229 | St_get_hdw (r, _, l) 225 230 | St_framesize (r, l) 226 | St_int (r, _, l)231 (* | St_int (r, _, l) *) 227 232 | St_addrH (r, _, l) 228 233 | St_addrL (r, _, l) -
Deliverables/D2.2/8051/src/ERTL/uses.ml
r1542 r1568 23 23 | St_ind_inc _ 24 24 | St_hdw_to_hdw _ 25 | St_set_hdw (_, RTL.Imm _, _) 25 26 | St_newframe _ 26 27 | St_delframe _ … … 31 32 uses 32 33 | St_get_hdw (r, _, _) 33 | St_set_hdw (_, r, _)34 | St_set_hdw (_, RTL.Reg r, _) 34 35 | St_framesize (r, _) 35 36 | St_pop (r, _) 36 37 | St_push (r, _) 37 | St_ int (r,_, _)38 | St_move (r, RTL.Imm _, _) 38 39 | St_addrH (r, _, _) 39 40 | St_addrL (r, _, _) 40 41 | St_cond (r, _, _) -> 41 42 count r uses 42 | St_move (r1, r2, _)43 | St_move (r1, RTL.Reg r2, _) 43 44 | St_op1 (_, r1, r2, _) 45 | St_op2 (_, r1, r2, RTL.Imm _, _) 44 46 | St_call_ptr (r1, r2, _, _) -> 45 47 count r1 (count r2 uses) 46 48 | St_opaccsA (_, r1, r2, r3, _) 47 49 | St_opaccsB (_, r1, r2, r3, _) 48 | St_op2 (_, r1, r2, r3, _)50 | St_op2 (_, r1, r2, RTL.Reg r3, _) 49 51 | St_load (r1, r2, r3, _) 50 52 | St_store (r1, r2, r3, _) -> -
Deliverables/D2.2/8051/src/LIN/LIN.mli
r1542 r1568 1 1 2 2 (** This module defines the abstract syntax tree of [LIN]. *) 3 4 type argument = LTL.argument 3 5 4 6 (** Compared to LTL where functions were graphs, the functions of a LIN program … … 55 57 (* Apply a binary operation on the A accumulator. Parameters are the 56 58 operation, and the other source register. *) 57 | St_op2 of I8051.op2 * I8051.register59 | St_op2 of I8051.op2 * argument 58 60 59 61 (* Set the carry flag to zero. *) -
Deliverables/D2.2/8051/src/LIN/LINInterpret.ml
r1542 r1568 96 96 else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".") 97 97 98 let get_arg a st = match a with 99 | LTL.Imm i -> Val.of_int i 100 | LTL.Reg r -> get_reg r st 101 98 102 let push st v = 99 103 let mem = Mem.store st.mem chunk st.isp v in … … 262 266 263 267 | LIN.St_op2 (op2, srcr) -> 264 let (v, carry) = 265 266 267 (get_reg srcr st) in268 let (v, carry) = 269 Eval.op2 st.carry op2 270 (get_reg I8051.a st) 271 (get_arg srcr st) in 268 272 let st = change_carry st carry in 269 273 let st = add_reg I8051.a v st in -
Deliverables/D2.2/8051/src/LIN/LINPrinter.ml
r1542 r1568 19 19 let print_a = print_reg I8051.a 20 20 21 let print_arg = function 22 | LTL.Imm i -> string_of_int i 23 | LTL.Reg r -> print_reg r 21 24 22 25 let print_statement = function … … 51 54 | LIN.St_op2 (op2, srcr) -> 52 55 Printf.sprintf "%s %s, %s" 53 (I8051.print_op2 op2) print_a (print_ reg srcr)56 (I8051.print_op2 op2) print_a (print_arg srcr) 54 57 | LIN.St_clear_carry -> "clear CARRY" 55 58 | LIN.St_set_carry -> "set CARRY" -
Deliverables/D2.2/8051/src/LIN/LINToASM.ml
r1542 r1568 55 55 let byte_of_int i = vect_of_int i `Eight 56 56 let data_of_int i = `DATA (byte_of_int i) 57 let reg_or_data = function 58 | LTL.Imm k -> data_of_int k 59 | LTL.Reg r -> I8051.reg_addr r 57 60 let data16_of_int i = `DATA16 (vect_of_int i `Sixteen) 58 61 let acc_addr = I8051.reg_addr I8051.a … … 95 98 | LIN.St_op1 I8051.Inc -> 96 99 [`INC `A] 97 | LIN.St_op2 (I8051.Add, r) -> 98 [`ADD (`A, I8051.reg_addr r)] 99 | LIN.St_op2 (I8051.Addc, r) -> 100 [`ADDC (`A, I8051.reg_addr r)] 101 | LIN.St_op2 (I8051.Sub, r) -> 102 [`SUBB (`A, I8051.reg_addr r)] 100 | LIN.St_op1 I8051.Rl -> 101 [`RL `A] 102 | LIN.St_op2 (I8051.Add, a) -> 103 [`ADD (`A, reg_or_data a)] 104 | LIN.St_op2 (I8051.Addc, a) -> 105 [`ADDC (`A, reg_or_data a)] 106 | LIN.St_op2 (I8051.Sub, a) -> 107 [`SUBB (`A, reg_or_data a)] 103 108 | LIN.St_op2 (I8051.And, r) -> 104 [`ANL (`U1 (`A, I8051.reg_addrr))]109 [`ANL (`U1 (`A, reg_or_data r))] 105 110 | LIN.St_op2 (I8051.Or, r) -> 106 [`ORL (`U1 (`A, I8051.reg_addrr))]111 [`ORL (`U1 (`A, reg_or_data r))] 107 112 | LIN.St_op2 (I8051.Xor, r) -> 108 [`XRL (`U1 (`A, I8051.reg_addrr))]113 [`XRL (`U1 (`A, reg_or_data r))] 109 114 | LIN.St_clear_carry -> 110 115 [`CLR `C] -
Deliverables/D2.2/8051/src/LTL/LTL.mli
r1542 r1568 7 7 algorithm. Actually, this coloring algorithm relies on the result of a 8 8 liveness analysis that will also allow to remove dead code. *) 9 10 type argument = 11 | Reg of I8051.register 12 | Imm of int 9 13 10 14 type statement = … … 58 62 59 63 (* Apply a binary operation on the A accumulator. Parameters are the 60 operation, the other source register, and the label of the next64 operation, the other argument, and the label of the next 61 65 statement. *) 62 | St_op2 of I8051.op2 * I8051.register* Label.t66 | St_op2 of I8051.op2 * argument * Label.t 63 67 64 68 (* Set the carry flag to zero. Parameter is the label of the next -
Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml
r1542 r1568 123 123 else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".") 124 124 125 let get_arg a st = match a with 126 | LTL.Imm i -> Val.of_int i 127 | LTL.Reg r -> get_reg r st 128 125 129 let push st v = 126 130 let mem = Mem.store st.mem chunk st.isp v in … … 294 298 Eval.op2 st.carry op2 295 299 (get_reg I8051.a st) 296 (get_ reg srcr st) in300 (get_arg srcr st) in 297 301 let st = change_carry st carry in 298 302 let st = add_reg I8051.a v st in -
Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml
r1542 r1568 18 18 19 19 let print_a = print_reg I8051.a 20 21 let print_arg = function 22 | LTL.Imm i -> string_of_int i 23 | LTL.Reg r -> print_reg r 20 24 21 25 … … 50 54 | LTL.St_op2 (op2, srcr, lbl) -> 51 55 Printf.sprintf "%s %s, %s --> %s" 52 (I8051.print_op2 op2) print_a (print_ reg srcr) lbl56 (I8051.print_op2 op2) print_a (print_arg srcr) lbl 53 57 | LTL.St_clear_carry lbl -> 54 58 Printf.sprintf "clear CARRY --> %s" lbl -
Deliverables/D2.2/8051/src/RTL/RTL.mli
r1542 r1568 9 9 type registers = Register.t list 10 10 11 (* arguments to certain operations: either registers or immediate args *) 12 type argument = 13 | Reg of Register.t 14 | Imm of int 15 11 16 type statement = 12 17 … … 17 22 | St_cost of CostLabel.t * Label.t 18 23 19 (* Reset to 0 a loop index *) 24 (* Reset to 0 a loop index *) 20 25 | St_ind_0 of CostLabel.index * Label.t 21 26 … … 32 37 | St_stackaddr of Register.t * Register.t * Label.t 33 38 34 (* Assign an integer constant to a register. Parameters are the destination35 register, the integer and the label of the next statement.*)36 | St_int of Register.t * int * Label.t39 (* (\* Assign an integer constant to a register. Parameters are the destination *) 40 (* register, the integer and the label of the next statement. *\) *) 41 (* | St_int of Register.t * int * Label.t *) 37 42 38 43 (* Move the content of a register to another. Parameters are the destination 39 register, the source register, and the label of the next statement. *)40 | St_move of Register.t * Register.t * Label.t44 register, the source argument, and the label of the next statement. *) 45 | St_move of Register.t * argument * Label.t 41 46 42 47 (* Apply a binary operation that will later be translated in an operation on … … 52 57 53 58 (* Apply a binary operation. Parameters are the operation, the destination 54 register, the source registers, and the label of the next statement. *)55 | St_op2 of I8051.op2 * Register.t * Register.t * Register.t * Label.t59 register, the source arguments, and the label of the next statement. *) 60 | St_op2 of I8051.op2 * Register.t * Register.t * argument * Label.t 56 61 57 62 (* Set the carry flag to zero. Parameter is the label of the next -
Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml
r1542 r1568 89 89 if Register.Map.mem r lenv then Register.Map.find r lenv 90 90 else error ("Unknown local register \"" ^ (Register.print r) ^ "\".") 91 92 let get_local_arg_value (lenv : local_env) : RTL.argument -> Val.t = function 93 | RTL.Reg r -> get_local_value lenv r 94 | RTL.Imm i -> Val.of_int i 95 91 96 let get_arg_values lenv args = List.map (get_local_value lenv) args 92 97 … … 159 164 assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2] sp 160 165 161 | RTL.St_int (r, i, lbl) ->162 assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i] 166 (* | RTL.St_int (r, i, lbl) -> *) 167 (* assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i] *) 163 168 164 169 | RTL.St_move (destr, srcr, lbl) -> 165 170 assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] 166 [get_local_ value lenv srcr]171 [get_local_arg_value lenv srcr] 167 172 168 173 | RTL.St_opaccs (opaccs, destr1, destr2, srcr1, srcr2, lbl) -> … … 182 187 Eval.op2 carry op2 183 188 (get_local_value lenv srcr1) 184 (get_local_ value lenv srcr2) in189 (get_local_arg_value lenv srcr2) in 185 190 assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v] 186 191 -
Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml
r1542 r1568 16 16 17 17 let print_reg = Register.print 18 19 let print_arg = function 20 | RTL.Reg r -> print_reg r 21 | RTL.Imm i -> string_of_int i 18 22 19 23 let reg_set_to_list rs = … … 44 48 | RTL.St_cost (cost_lbl, lbl) -> 45 49 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 46 Printf.sprintf " emit %s --> %s" cost_lbl lbl50 Printf.sprintf "_emit %s --> %s" cost_lbl lbl 47 51 | RTL.St_ind_0 (i, lbl) -> 48 Printf.sprintf " index %d --> %s" i lbl52 Printf.sprintf "_index %d --> %s" i lbl 49 53 | RTL.St_ind_inc (i, lbl) -> 50 Printf.sprintf " increment %d --> %s" i lbl54 Printf.sprintf "_increment %d --> %s" i lbl 51 55 | RTL.St_addr (dstr1, dstr2, id, lbl) -> 52 Printf.sprintf " imm(%s, %s), %s --> %s"56 Printf.sprintf "move (%s, %s), %s --> %s" 53 57 (print_reg dstr1) (print_reg dstr2) id lbl 54 58 | RTL.St_stackaddr (dstr1, dstr2, lbl) -> 55 Printf.sprintf " imm(%s, %s), STACK --> %s"59 Printf.sprintf "move (%s, %s), STACK --> %s" 56 60 (print_reg dstr1) (print_reg dstr2) lbl 57 | RTL.St_int (dstr, i, lbl) ->58 Printf.sprintf "imm %s, %d --> %s" (print_reg dstr) i lbl61 (* | RTL.St_int (dstr, i, lbl) -> *) 62 (* Printf.sprintf "imm %s, %d --> %s" (print_reg dstr) i lbl *) 59 63 | RTL.St_move (dstr, srcr, lbl) -> 60 64 Printf.sprintf "move %s, %s --> %s" 61 (print_reg dstr) (print_ reg srcr) lbl65 (print_reg dstr) (print_arg srcr) lbl 62 66 | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl) -> 63 67 Printf.sprintf "%s (%s, %s) %s, %s --> %s" … … 76 80 (print_reg dstr) 77 81 (print_reg srcr1) 78 (print_ reg srcr2)82 (print_arg srcr2) 79 83 lbl 80 84 | RTL.St_clear_carry lbl -> -
Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml
r1542 r1568 34 34 | ERTL.St_addrH (r, id, _) -> ERTL.St_addrH (r, id, lbl) 35 35 | ERTL.St_addrL (r, id, _) -> ERTL.St_addrL (r, id, lbl) 36 | ERTL.St_int (r, i, _) -> ERTL.St_int (r, i, lbl) 37 | ERTL.St_move (r1, r2, _) -> ERTL.St_move (r1, r2, lbl) 36 | ERTL.St_move (r1, a, _) -> ERTL.St_move (r1, a, lbl) 38 37 | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, _) -> 39 38 ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl) … … 102 101 let restore_hdws l = 103 102 let f (destr, srcr) start_lbl = 104 adds_graph [ERTL.St_set_hdw (destr, srcr, start_lbl)] start_lbl in103 adds_graph [ERTL.St_set_hdw (destr, RTL.Reg srcr, start_lbl)] start_lbl in 105 104 List.map f (List.map (fun (x, y) -> (y, x)) l) 106 105 … … 118 117 adds_graph 119 118 [ERTL.St_framesize (addr1, start_lbl) ; 120 ERTL.St_ int (tmpr, off+I8051.int_size, start_lbl) ;121 ERTL.St_op2 (I8051.Sub, addr1, addr1, tmpr,start_lbl) ;119 ERTL.St_op2 (I8051.Sub, addr1, addr1, RTL.Imm (off+I8051.int_size), 120 start_lbl) ; 122 121 ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ; 123 ERTL.St_op2 (I8051.Add, addr1, addr1, tmpr, start_lbl) ; 124 ERTL.St_int (addr2, 0, start_lbl) ; 122 ERTL.St_op2 (I8051.Add, addr1, addr1, RTL.Reg tmpr, start_lbl) ; 125 123 ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ; 126 ERTL.St_op2 (I8051.Addc, addr2, addr2, tmpr, start_lbl) ;124 ERTL.St_op2 (I8051.Addc, addr2, tmpr, RTL.Imm 0, start_lbl) ; 127 125 ERTL.St_load (destr, addr1, addr2, start_lbl)] 128 126 start_lbl dest_lbl def … … 176 174 177 175 let save_return ret_regs start_lbl dest_lbl def = 178 let (def, tmpr) = fresh_reg def in179 176 let ((common1, rest1), (common2, _)) = 180 177 MiscPottier.reduce I8051.sts ret_regs in 181 let init_tmpr = ERTL.St_int (tmpr, 0, start_lbl) in 182 let f_save st r = ERTL.St_set_hdw (st, r, start_lbl) in 178 let f_save st r = ERTL.St_set_hdw (st, RTL.Reg r, start_lbl) in 183 179 let saves = List.map2 f_save common1 common2 in 184 let f_default st = ERTL.St_set_hdw (st, tmpr, start_lbl) in180 let f_default st = ERTL.St_set_hdw (st, RTL.Imm 0, start_lbl) in 185 181 let defaults = List.map f_default rest1 in 186 adds_graph ( init_tmpr ::saves @ defaults) start_lbl dest_lbl def182 adds_graph (saves @ defaults) start_lbl dest_lbl def 187 183 188 184 let assign_result start_lbl = … … 252 248 let (def, tmpr) = fresh_reg def in 253 249 adds_graph 254 [ERTL.St_int (addr1, off+I8051.int_size, start_lbl) ; 255 ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ; 250 [ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ; 256 251 ERTL.St_clear_carry start_lbl ; 257 ERTL.St_op2 (I8051.Sub, addr1, tmpr, addr1, start_lbl) ; 252 ERTL.St_op2 (I8051.Sub, addr1, tmpr, RTL.Imm (off+I8051.int_size), 253 start_lbl) ; 258 254 ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ; 259 ERTL.St_int (addr2, 0, start_lbl) ; 260 ERTL.St_op2 (I8051.Sub, addr2, tmpr, addr2, start_lbl) ; 255 ERTL.St_op2 (I8051.Sub, addr2, tmpr, RTL.Imm 0, start_lbl) ; 261 256 ERTL.St_store (addr1, addr2, srcr, start_lbl)] 262 257 start_lbl dest_lbl def … … 338 333 lbl lbl' def 339 334 340 | RTL.St_int (r, i, lbl') ->341 add_graph lbl (ERTL.St_int (r, i, lbl')) def335 (* | RTL.St_int (r, i, lbl') -> *) 336 (* add_graph lbl (ERTL.St_int (r, i, lbl')) def *) 342 337 343 338 | RTL.St_move (r1, r2, lbl') -> … … 444 439 | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl) 445 440 | ERTL.St_pop (_, lbl) | ERTL.St_push (_, lbl) | ERTL.St_addrH (_, _, lbl) 446 | ERTL.St_addrL (_, _, lbl) | ERTL.St_int (_, _, lbl)441 | ERTL.St_addrL (_, _, lbl) (* | ERTL.St_int (_, _, lbl) *) 447 442 | ERTL.St_move (_, _, lbl) | ERTL.St_opaccsA (_, _, _, _, lbl) 448 443 | ERTL.St_opaccsB (_, _, _, _, lbl) -
Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli
r1542 r1568 11 11 12 12 13 (* arguments to certain operations: either registers or immediate args *) 13 14 type argument = 14 15 | Reg of Register.t -
Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml
r1542 r1568 168 168 lbl 169 169 | RTLabs.St_load (q, addr, destr, lbl) -> 170 Printf.sprintf "%s := *(%s)%s --> %s"170 Printf.sprintf "%s := (%s) *%s --> %s" 171 171 (print_reg destr) 172 172 (Memory.string_of_quantity q) … … 174 174 lbl 175 175 | RTLabs.St_store (q, addr, srcr, lbl) -> 176 Printf.sprintf "*(%s)%s := %s --> %s" 176 Printf.sprintf "*%s := (%s)%s --> %s" 177 (print_arg addr) 177 178 (Memory.string_of_quantity q) 178 (print_arg addr)179 179 (print_arg srcr) 180 180 lbl … … 216 216 (Primitive.print_sig sg) 217 217 | RTLabs.St_cond (r, lbl_true, lbl_false) -> 218 Printf.sprintf " %s? --> %s,%s"218 Printf.sprintf "if %s --> %s else --> %s" 219 219 (print_reg r) 220 220 lbl_true -
Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml
r1542 r1568 97 97 | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl) 98 98 | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl) 99 | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl)99 (* | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl) *) 100 100 | RTL.St_move (r1, r2, _) -> RTL.St_move (r1, r2, lbl) 101 101 | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, _) -> … … 204 204 let module M = IntValue.Make (struct let size = size end) in 205 205 let is = List.map M.to_int (M.break (M.of_int i) size) in 206 let f r i = RTL.St_ int (r,i, dest_lbl) in206 let f r i = RTL.St_move (r, RTL.Imm i, dest_lbl) in 207 207 let l = List.map2 f destrs is in 208 208 adds_graph l start_lbl dest_lbl def … … 229 229 let rec translate_move destrs srcrs start_lbl = 230 230 let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in 231 let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in231 let f_common destr srcr = RTL.St_move (destr, RTL.Reg srcr, start_lbl) in 232 232 let translates1 = adds_graph (List.map2 f_common common1 common2) in 233 233 let translates2 = translate_cst (AST.Cst_int 0) rest1 in 234 234 add_translates [translates1 ; translates2] start_lbl 235 235 236 let rec translate_imm destrs vals start_lbl = 237 let ((common1, rest1), (common2, _)) = MiscPottier.reduce destrs vals in 238 let f_common destr srcr = RTL.St_move (destr, RTL.Imm srcr, start_lbl) in 239 let translates1 = adds_graph (List.map2 f_common common1 common2) in 240 let translates2 = translate_cst (AST.Cst_int 0) rest1 in 241 add_translates [translates1 ; translates2] start_lbl 242 236 243 237 244 let translate_cast_unsigned destrs start_lbl dest_lbl def = 238 let (def, tmp_zero) = fresh_reg def in 239 let zeros = MiscPottier.make tmp_zero (List.length destrs) in 240 add_translates 241 [adds_graph [RTL.St_int (tmp_zero, 0, start_lbl)] ; 242 translate_move destrs zeros] 243 start_lbl dest_lbl def 245 translate_cst (AST.Cst_int 0) destrs start_lbl dest_lbl def 244 246 245 247 let translate_cast_signed destrs srcr start_lbl dest_lbl def = 246 let (def, tmp_128) = fresh_reg def in247 let (def, tmp_255) = fresh_reg def in248 248 let (def, tmpr) = fresh_reg def in 249 let (def, dummy) = fresh_reg def in250 249 let insts = 251 [RTL.St_int (tmp_128, 128, start_lbl) ; 252 RTL.St_op2 (I8051.And, tmpr, tmp_128, srcr, start_lbl) ; 253 RTL.St_opaccs (I8051.DivuModu, tmpr, dummy, tmpr, tmp_128, start_lbl) ; 254 RTL.St_int (tmp_255, 255, start_lbl) ; 255 RTL.St_opaccs (I8051.Mul, tmpr, dummy, tmpr, tmp_255, start_lbl)] in 250 (* this sets tmpr to 0xFF if s is neg, 0x00 o.w. Done like that: 251 byte in tmpr if srcr is: neg | pos 252 tmpr ← srcr | 127 11...1 | 01...1 253 tmpr ← tmpr <rot< 1 1...11 | 1...10 254 tmpr ← INC tmpr 0....0 | 1....1 255 tmpr ← CPL tmpr 1....1 | 0....0 256 257 *) 258 [RTL.St_op2 (I8051.Or, tmpr, srcr, RTL.Imm 127, start_lbl) ; 259 RTL.St_op1 (I8051.Rl, tmpr, tmpr, start_lbl) ; 260 RTL.St_op1 (I8051.Inc, tmpr, tmpr, start_lbl) ; 261 RTL.St_op1 (I8051.Cmpl, tmpr, tmpr, start_lbl) ] in 256 262 let srcrs = MiscPottier.make tmpr (List.length destrs) in 257 263 add_translates [adds_graph insts ; translate_move destrs srcrs] … … 273 279 274 280 let translate_negint destrs srcrs start_lbl dest_lbl def = 275 assert (List.length destrs = List.length srcrs) ; 276 let (def, tmpr) = fresh_reg def in 281 assert (List.length destrs = List.length srcrs && List.length destrs > 0) ; 277 282 let f_cmpl destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in 278 283 let insts_cmpl = List.map2 f_cmpl destrs srcrs in 279 let insts_init = 280 [RTL.St_set_carry start_lbl ; 281 RTL.St_int (tmpr, 0, start_lbl)] in 282 let f_add destr = RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl) in 283 let insts_add = List.map f_add destrs in 284 adds_graph (insts_cmpl @ insts_init @ insts_add) 284 let first, rest = List.hd destrs, List.tl destrs in 285 let inst_init = 286 RTL.St_op2 (I8051.Add, first, first, RTL.Imm 0, start_lbl) in 287 let f_add destr = 288 RTL.St_op2 (I8051.Addc, destr, destr, RTL.Imm 0, start_lbl) in 289 let insts_add = List.map f_add rest in 290 adds_graph (insts_cmpl @ inst_init :: insts_add) 285 291 start_lbl dest_lbl def 286 292 287 293 288 let translate_notbool destrs srcrs start_lbl dest_lbl def = match destrs with 289 | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def 290 | destr :: destrs -> 291 let (def, tmpr) = fresh_reg def in 292 let (def, tmp_srcrs) = fresh_regs def (List.length srcrs) in 293 let save_srcrs = translate_move tmp_srcrs srcrs in 294 let init_destr = RTL.St_int (destr, 1, start_lbl) in 295 let f tmp_srcr = 296 [RTL.St_clear_carry start_lbl ; 297 RTL.St_int (tmpr, 0, start_lbl) ; 298 RTL.St_op2 (I8051.Sub, tmpr, tmpr, tmp_srcr, start_lbl) ; 299 RTL.St_int (tmpr, 0, start_lbl) ; 300 RTL.St_op2 (I8051.Addc, tmpr, tmpr, tmpr, start_lbl) ; 301 RTL.St_op2 (I8051.Xor, destr, destr, tmpr, start_lbl)] in 302 let insts = init_destr :: (List.flatten (List.map f tmp_srcrs)) in 303 let epilogue = translate_cst (AST.Cst_int 0) destrs in 304 add_translates [save_srcrs ; adds_graph insts ; epilogue] 305 start_lbl dest_lbl def 294 let translate_notbool destrs srcrs start_lbl dest_lbl def = 295 match destrs,srcrs with 296 | [], _ -> adds_graph [] start_lbl dest_lbl def 297 | destr :: destrs, srcr :: srcrs -> 298 let (def, tmpr) = fresh_reg def in 299 let init_destr = RTL.St_move (destr, RTL.Reg srcr, start_lbl) in 300 let f r = 301 RTL.St_op2 (I8051.Or, destr, destr, RTL.Reg r, start_lbl) in 302 let big_or = List.map f srcrs in 303 let finalize_destr = 304 [RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ; 305 RTL.St_clear_carry start_lbl ; 306 RTL.St_op2 (I8051.Sub, tmpr, tmpr, RTL.Reg destr, start_lbl) ; 307 (* carry bit is set iff destr is non-zero iff destrs was non-zero *) 308 RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ; 309 RTL.St_op2 (I8051.Addc, destr, tmpr, RTL.Reg tmpr, start_lbl) ; 310 (* destr = carry bit = bigor of old destrs *) 311 RTL.St_op2 (I8051.Xor, destr, destr, RTL.Imm 1, start_lbl)] in 312 let epilogue = translate_cst (AST.Cst_int 0) destrs in 313 add_translates [adds_graph (init_destr :: big_or @ finalize_destr) ; 314 epilogue] 315 start_lbl dest_lbl def 316 | destr :: destrs, [] -> 317 translate_cst (AST.Cst_int 1) destrs start_lbl dest_lbl def 306 318 307 319 … … 336 348 MiscPottier.reduce destrs_rest srcrs_rest in 337 349 let (def, tmpr) = fresh_reg def in 338 let insts_init = 339 [RTL.St_clear_carry start_lbl ; 340 RTL.St_int (tmpr, 0, start_lbl)] in 350 let carry_init = match op with 351 | I8051.Addc | I8051.Sub -> 352 (* depend on carry bit *) 353 [RTL.St_clear_carry start_lbl] 354 | I8051.Add -> assert false (* should not call with add, not correct *) 355 | _ -> [] in 356 let inst_init = RTL.St_move (tmpr, RTL.Imm 0, start_lbl) :: carry_init in 341 357 let f_add destr srcr1 srcr2 = 342 RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in358 RTL.St_op2 (op, destr, srcr1, RTL.Reg srcr2, start_lbl) in 343 359 let insts_add = 344 360 MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in 345 361 let f_add_cted destr srcr = 346 RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in362 RTL.St_op2 (op, destr, srcr, RTL.Reg tmpr, start_lbl) in 347 363 let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in 348 364 let f_rest destr = 349 RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in365 RTL.St_op2 (op, destr, tmpr, RTL.Reg tmpr, start_lbl) in 350 366 let insts_rest = List.map f_rest destrs_rest in 351 adds_graph (inst s_init @ insts_add @ insts_add_cted @ insts_rest)367 adds_graph (inst_init @ insts_add @ insts_add_cted @ insts_rest) 352 368 start_lbl dest_lbl def 353 369 … … 357 373 | [], _ -> adds_graph [RTL.St_skip start_lbl] start_lbl 358 374 | [destr], [] -> 359 adds_graph [RTL.St_int (tmpr, 0, start_lbl) ; 360 RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)] 375 adds_graph [RTL.St_op2 (I8051.Addc, destr, destr, RTL.Imm 0, start_lbl)] 361 376 start_lbl 362 377 | destr1 :: destr2 :: destrs, [] -> 363 378 add_translates 364 [adds_graph [RTL.St_int (tmpr, 0, start_lbl) ; 365 RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl) ; 366 RTL.St_op2 (I8051.Addc, destr2, tmpr, tmpr, start_lbl)] ; 379 [adds_graph 380 [RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ; 381 RTL.St_op2 (I8051.Addc, destr1, destr1, RTL.Imm 0, start_lbl) ; 382 RTL.St_op2 (I8051.Addc, destr2, tmpr, RTL.Imm 0, start_lbl)] ; 367 383 translate_cst (AST.Cst_int 0) destrs] 368 384 start_lbl … … 370 386 adds_graph 371 387 [RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ; 372 RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)]388 RTL.St_op2 (I8051.Addc, destr, destr, RTL.Reg tmpr, start_lbl)] 373 389 start_lbl 374 390 | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 -> … … 377 393 [RTL.St_opaccs 378 394 (I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ; 379 RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl)] ;395 RTL.St_op2 (I8051.Addc, destr1, destr1, RTL.Reg tmpr, start_lbl)] ; 380 396 translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2] 381 397 start_lbl … … 389 405 | tmp_destr2 :: tmp_destrs2 -> 390 406 [adds_graph [RTL.St_clear_carry dummy_lbl ; 391 RTL.St_ int (tmp_destr2,0, dummy_lbl)] ;407 RTL.St_move (tmp_destr2, RTL.Imm 0, dummy_lbl)] ; 392 408 translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ; 393 409 translate_cst (AST.Cst_int 0) tmp_destrs1 ; 394 adds_graph [RTL.St_clear_carry dummy_lbl] ;395 410 translate_op I8051.Addc destrs destrs tmp_destrs]) 396 411 … … 422 437 add_translates [inst_div ; insts_rest] start_lbl dest_lbl def 423 438 424 425 439 let translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def = 426 440 match destrs with 427 | [] -> add _graph start_lbl (RTL.St_skip dest_lbl)def441 | [] -> adds_graph [] start_lbl dest_lbl def 428 442 | destr :: destrs -> 429 443 let (def, tmpr) = fresh_reg def in 430 let (def, tmp_zero) = fresh_reg def in431 let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in432 let save_srcrs1 = translate_move tmp_srcrs1 srcrs1 in433 let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in434 let save_srcrs2 = translate_move tmp_srcrs2 srcrs2 in435 444 let ((common1, rest1), (common2, rest2)) = 436 MiscPottier.reduce tmp_srcrs1 tmp_srcrs2 in445 MiscPottier.reduce srcrs1 srcrs2 in 437 446 let rest = choose_rest rest1 rest2 in 438 let inits = 439 [RTL.St_int (destr, 0, start_lbl) ; 440 RTL.St_int (tmp_zero, 0, start_lbl)] in 441 let f_common tmp_srcr1 tmp_srcr2 = 442 [RTL.St_clear_carry start_lbl ; 443 RTL.St_op2 (I8051.Sub, tmpr, tmp_srcr1, tmp_srcr2, start_lbl) ; 444 RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in 445 let insts_common = List.flatten (List.map2 f_common common1 common2) in 447 let firsts = match common1, common2 with 448 | c1hd :: c1tl, c2hd :: c2tl -> 449 let init = 450 RTL.St_op2 (I8051.Xor, destr, c1hd, RTL.Reg c2hd, start_lbl) in 451 let f_common tmp_srcr1 tmp_srcr2 = 452 [RTL.St_op2 (I8051.Xor, tmpr, tmp_srcr1, 453 RTL.Reg tmp_srcr2, start_lbl) ; 454 RTL.St_op2 (I8051.Or, destr, destr, RTL.Reg tmpr, start_lbl)] in 455 let insts_common = List.flatten (List.map2 f_common c1tl c2tl) in 456 init :: insts_common 457 | [], [] -> 458 [RTL.St_move (destr, RTL.Imm 0, start_lbl)] 459 (* common1 and common2 have the same length *) 460 | _ -> assert false in 446 461 let f_rest tmp_srcr = 447 [RTL.St_clear_carry start_lbl ; 448 RTL.St_op2 (I8051.Sub, tmpr, tmp_zero, tmp_srcr, start_lbl) ; 449 RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in 450 let insts_rest = List.flatten (List.map f_rest rest) in 451 let insts = inits @ insts_common @ insts_rest in 462 RTL.St_op2 (I8051.Xor, destr, destr, RTL.Reg tmp_srcr, start_lbl) in 463 let insts_rest = List.map f_rest rest in 464 let insts = firsts @ insts_rest in 452 465 let epilogue = translate_cst (AST.Cst_int 0) destrs in 453 add_translates [save_srcrs1 ; save_srcrs2 ; adds_graph insts ; epilogue] 454 start_lbl dest_lbl def 455 456 457 let translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl 458 (srcr1, srcr2) = 459 [RTL.St_clear_carry dummy_lbl ; 460 RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ; 461 RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ; 462 RTL.St_op2 (I8051.Sub, tmpr2, srcr2, srcr1, dummy_lbl) ; 463 RTL.St_op2 (I8051.Addc, tmpr2, tmp_zero, tmp_zero, dummy_lbl) ; 464 RTL.St_op2 (I8051.Or, tmpr1, tmpr1, tmpr2, dummy_lbl) ; 465 RTL.St_op2 (I8051.Xor, tmpr1, tmpr1, tmp_one, dummy_lbl) ; 466 RTL.St_op2 (I8051.And, destr, destr, tmpr1, dummy_lbl)] 467 468 let translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 destr leq dummy_lbl = 469 let f = translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in 470 (RTL.St_int (destr, 1, dummy_lbl)) :: (List.flatten (List.map f leq)) 471 472 let translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq 473 srcr1 srcr2 = 474 (translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl) @ 475 [RTL.St_clear_carry dummy_lbl ; 476 RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ; 477 RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ; 478 RTL.St_op2 (I8051.And, tmpr3, tmpr3, tmpr1, dummy_lbl) ; 479 RTL.St_op2 (I8051.Or, destr, destr, tmpr3, dummy_lbl)] 480 481 let translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl 482 srcrs1 srcrs2 = 483 let f (insts, leq) srcr1 srcr2 = 484 let added_insts = 485 translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq 486 srcr1 srcr2 in 487 (insts @ added_insts, leq @ [(srcr1, srcr2)]) in 488 fst (List.fold_left2 f ([], []) srcrs1 srcrs2) 489 490 let translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def = 466 add_translates [ adds_graph insts ; epilogue] start_lbl dest_lbl def 467 468 (* this requires destrs to be either 0 or 1 to be truly correct 469 to be used after translations that ensure this *) 470 let translate_toggle_bool destrs start_lbl = 491 471 match destrs with 492 | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def 493 | _ -> 494 let (def, tmp_destrs) = fresh_regs def (List.length destrs) in 495 let tmp_destr = List.hd tmp_destrs in 496 let (def, tmp_zero) = fresh_reg def in 497 let (def, tmp_one) = fresh_reg def in 498 let (def, tmpr1) = fresh_reg def in 499 let (def, tmpr2) = fresh_reg def in 500 let (def, tmpr3) = fresh_reg def in 501 let (srcrs1, srcrs2, added) = complete_regs def srcrs1 srcrs2 in 502 let srcrs1 = List.rev srcrs1 in 503 let srcrs2 = List.rev srcrs2 in 504 let insts_init = 505 [translate_cst (AST.Cst_int 0) tmp_destrs ; 506 translate_cst (AST.Cst_int 0) added ; 507 adds_graph [RTL.St_int (tmp_zero, 0, start_lbl) ; 508 RTL.St_int (tmp_one, 1, start_lbl)]] in 509 let insts_main = 510 translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl 511 srcrs1 srcrs2 in 512 let insts_main = [adds_graph insts_main] in 513 let insts_exit = [translate_move destrs tmp_destrs] in 514 add_translates (insts_init @ insts_main @ insts_exit ) 515 start_lbl dest_lbl def 516 517 518 let add_128_to_last tmp_128 rs start_lbl = match rs with 519 | [] -> adds_graph [] start_lbl 520 | _ -> 521 let r = MiscPottier.last rs in 522 adds_graph [RTL.St_op2 (I8051.Add, r, r, tmp_128, start_lbl)] start_lbl 523 472 | [] -> adds_graph [] start_lbl 473 | destr :: _ -> 474 adds_graph [RTL.St_op1 (I8051.Cmpl, destr, destr, start_lbl)] start_lbl 475 476 477 478 (* let translate_eq_reg tmp_zero tmpr destr dummy_lbl *) 479 (* (srcr1, srcr2) = *) 480 (* [RTL.St_op2 (I8051.Xor, tmpr, srcr1, srcr2, dummy_lbl) ; *) 481 (* (\* now tmpr = 0 iff srcr1 = srcr2 *\) *) 482 (* RTL.St_clear_carry dummy_lbl ; *) 483 (* RTL.St_op2 (I8051.Sub, tmpr, tmp_zero, tmpr, dummy_lbl) ; *) 484 (* (\* now carry bit = (old tmpr is not zero) = (srcr1 != srcr2) *\) *) 485 (* RTL.St_op2 (I8051.Addc, tmpr, tmp_zero, tmp_zero, dummy_lbl) ; *) 486 (* (\* now tmpr = old carry bit = (srcr1 != srcr2) *\) *) 487 (* RTL.St_op1 (I8051.Cpl, tmpr, tmpr, dummy_lbl)] *) 488 489 (* let translate_eq_list tmp_zero tmpr destr leq dummy_lbl = match leq with *) 490 (* | leqhd :: leqtl -> *) 491 (* let init = translate_eq_reg tmp_zero destr dummy_lbl leqhd in *) 492 (* let f p = translate_eq_reg tmp_zero tmpr destr dummy_lbl p @ *) 493 (* [RTL.St_op2 (I8051.And, destr, destr, tmpr1, dummy_lbl)] in *) 494 (* init @ List.flatten (List.map f leqtl) *) 495 (* | _ -> [RTL.St_move (destr, RTL.Imm 1, dummy_lbl)] *) 496 497 (* let translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq *) 498 (* srcr1 srcr2 = *) 499 (* (translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl) @ *) 500 (* [RTL.St_clear_carry dummy_lbl ; *) 501 (* RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ; *) 502 (* RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ; *) 503 (* RTL.St_op2 (I8051.And, tmpr3, tmpr3, tmpr1, dummy_lbl) ; *) 504 (* RTL.St_op2 (I8051.Or, destr, destr, tmpr3, dummy_lbl)] *) 505 506 (* let translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl *) 507 (* srcrs1 srcrs2 = *) 508 (* let f (insts, leq) srcr1 srcr2 = *) 509 (* let added_insts = *) 510 (* translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq *) 511 (* srcr1 srcr2 in *) 512 (* (insts @ added_insts, leq @ [(srcr1, srcr2)]) in *) 513 (* fst (List.fold_left2 f ([], []) srcrs1 srcrs2) *) 514 515 (* let translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def = *) 516 (* match destrs with *) 517 (* | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def *) 518 (* | _ -> *) 519 (* let (def, tmp_destrs) = fresh_regs def (List.length destrs) in *) 520 (* let tmp_destr = List.hd tmp_destrs in *) 521 (* let (def, tmp_zero) = fresh_reg def in *) 522 (* let (def, tmp_one) = fresh_reg def in *) 523 (* let (def, tmpr1) = fresh_reg def in *) 524 (* let (def, tmpr2) = fresh_reg def in *) 525 (* let (def, tmpr3) = fresh_reg def in *) 526 (* let (srcrs1, srcrs2, added) = complete_regs def srcrs1 srcrs2 in *) 527 (* let srcrs1 = List.rev srcrs1 in *) 528 (* let srcrs2 = List.rev srcrs2 in *) 529 (* let insts_init = *) 530 (* [translate_cst (AST.Cst_int 0) tmp_destrs ; *) 531 (* translate_cst (AST.Cst_int 0) added ; *) 532 (* adds_graph [RTL.St_int (tmp_zero, 0, start_lbl) ; *) 533 (* RTL.St_int (tmp_one, 1, start_lbl)]] in *) 534 (* let insts_main = *) 535 (* translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl *) 536 (* srcrs1 srcrs2 in *) 537 (* let insts_main = [adds_graph insts_main] in *) 538 (* let insts_exit = [translate_move destrs tmp_destrs] in *) 539 (* add_translates (insts_init @ insts_main @ insts_exit ) *) 540 (* start_lbl dest_lbl def *) 541 542 let rec pad_with p l1 l2 = match l1, l2 with 543 | [], [] -> ([], []) 544 | x :: xs, y :: ys -> 545 let (xs', ys') = pad_with p xs ys in 546 (x :: xs', y :: ys') 547 | [], _ -> (MiscPottier.make p (List.length l2), l2) 548 | _, [] -> (l1, MiscPottier.make p (List.length l1)) 549 550 let translate_ltu desrtrs srcrs1 srcrs2 start_lbl dest_lbl def = 551 match desrtrs with 552 | [] -> adds_graph [] start_lbl dest_lbl def 553 | destr :: destrs -> 554 let (def, tmpr_zero) = fresh_reg def in 555 let (srcrs1, srcrs2) = pad_with tmpr_zero srcrs1 srcrs2 in 556 let init = 557 [RTL.St_move (tmpr_zero, RTL.Imm 0, start_lbl) ; 558 RTL.St_clear_carry start_lbl] in 559 let f srcr1 srcr2 = 560 RTL.St_op2 (I8051.Sub, destr, srcr1, RTL.Reg srcr2, start_lbl) in 561 (* not interested in result, just the carry bit 562 the following is safe even if destrs = srcrsi *) 563 let iter_sub = List.map2 f srcrs1 srcrs2 in 564 let extract_carry = 565 [RTL.St_op2 (I8051.Addc, destr, tmpr_zero, 566 RTL.Reg tmpr_zero, start_lbl)] in 567 let epilogue = translate_cst (AST.Cst_int 0) destrs in 568 add_translates [adds_graph (init @ iter_sub @ extract_carry); 569 epilogue] start_lbl dest_lbl def 570 571 let rec add_128_to_last 572 (tmp_128 : Register.t) 573 (last_subst : Register.t) 574 (rs : Register.t list) 575 (dummy_lbl : Label.t) = match rs with 576 | [] -> ([], adds_graph []) 577 | [last] -> 578 let insts = 579 [RTL.St_move (last_subst, RTL.Reg last, dummy_lbl) ; 580 RTL.St_op2 (I8051.Add, last_subst, last_subst, 581 RTL.Reg tmp_128, dummy_lbl)] in 582 ([last_subst], adds_graph insts) 583 | hd :: tail -> 584 let (tail', trans) = add_128_to_last tmp_128 last_subst tail dummy_lbl in 585 (hd :: tail', trans) 586 587 (* what happens if srcrs1 and srcrs2 have different length? seems to me 588 128 is added at the wrong place then *) 524 589 let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def = 525 let (def, tmp_ srcrs1) = fresh_regs def (List.length srcrs1)in526 let (def, tmp_ srcrs2) = fresh_regs def (List.length srcrs2)in590 let (def, tmp_last_srcr1) = fresh_reg def in 591 let (def, tmp_last_srcr2) = fresh_reg def in 527 592 let (def, tmp_128) = fresh_reg def in 593 (* I save just the last registers *) 594 let (srcrs1, add_128_to_srcrs1) = 595 add_128_to_last tmp_128 tmp_last_srcr1 srcrs1 start_lbl in 596 let (srcrs2, add_128_to_srcrs2) = 597 add_128_to_last tmp_128 tmp_last_srcr2 srcrs2 start_lbl in 528 598 add_translates 529 [translate_move tmp_srcrs1 srcrs1 ; 530 translate_move tmp_srcrs2 srcrs2 ; 531 adds_graph [RTL.St_int (tmp_128, 128, start_lbl)] ; 532 add_128_to_last tmp_128 tmp_srcrs1 ; 533 add_128_to_last tmp_128 tmp_srcrs2 ; 534 translate_lt destrs tmp_srcrs1 tmp_srcrs2] 599 [adds_graph [RTL.St_move (tmp_128, RTL.Imm 128, start_lbl)] ; 600 add_128_to_srcrs1; 601 add_128_to_srcrs2; 602 translate_ltu destrs srcrs1 srcrs2] 535 603 start_lbl dest_lbl def 536 604 537 605 538 let rectranslate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =606 let translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def = 539 607 match op2 with 540 608 … … 569 637 | AST.Op_cmpp AST.Cmp_eq -> 570 638 add_translates 571 [translate_op2 (AST.Op_cmpu AST.Cmp_ne) destrs srcrs1 srcrs2 ; 572 translate_op1 AST.Op_notbool destrs destrs] 573 start_lbl dest_lbl def 639 [translate_ne destrs srcrs1 srcrs2 ; 640 translate_toggle_bool destrs] start_lbl dest_lbl def 574 641 575 642 | AST.Op_cmp AST.Cmp_ne … … 582 649 583 650 | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt -> 584 translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def651 translate_ltu destrs srcrs1 srcrs2 start_lbl dest_lbl def 585 652 586 653 | AST.Op_cmp AST.Cmp_le -> 587 654 add_translates 588 [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs2 srcrs1 ; 589 translate_op1 AST.Op_notbool destrs destrs] 590 start_lbl dest_lbl def 591 592 | AST.Op_cmpu AST.Cmp_le -> 655 [translate_lts destrs srcrs2 srcrs1 ; 656 translate_toggle_bool destrs] start_lbl dest_lbl def 657 658 | AST.Op_cmpu AST.Cmp_le | AST.Op_cmpp AST.Cmp_le -> 593 659 add_translates 594 [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs2 srcrs1 ; 595 translate_op1 AST.Op_notbool destrs destrs] 596 start_lbl dest_lbl def 597 598 | AST.Op_cmpp AST.Cmp_le -> 599 add_translates 600 [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs2 srcrs1 ; 601 translate_op1 AST.Op_notbool destrs destrs] 602 start_lbl dest_lbl def 660 [translate_ltu destrs srcrs2 srcrs1 ; 661 translate_toggle_bool destrs] start_lbl dest_lbl def 603 662 604 663 | AST.Op_cmp AST.Cmp_gt -> 605 translate_op2 (AST.Op_cmp AST.Cmp_lt) 606 destrs srcrs2 srcrs1 start_lbl dest_lbl def 607 608 | AST.Op_cmpu AST.Cmp_gt -> 609 translate_op2 (AST.Op_cmpu AST.Cmp_lt) 610 destrs srcrs2 srcrs1 start_lbl dest_lbl def 611 612 | AST.Op_cmpp AST.Cmp_gt -> 613 translate_op2 (AST.Op_cmpp AST.Cmp_lt) 614 destrs srcrs2 srcrs1 start_lbl dest_lbl def 664 translate_lts destrs srcrs2 srcrs1 start_lbl dest_lbl def 665 666 | AST.Op_cmpu AST.Cmp_gt | AST.Op_cmpp AST.Cmp_gt -> 667 translate_ltu destrs srcrs2 srcrs1 start_lbl dest_lbl def 615 668 616 669 | AST.Op_cmp AST.Cmp_ge -> 617 670 add_translates 618 [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs1 srcrs2 ; 619 translate_op1 AST.Op_notbool destrs destrs] 620 start_lbl dest_lbl def 621 622 | AST.Op_cmpu AST.Cmp_ge -> 671 [translate_lts destrs srcrs1 srcrs2 ; 672 translate_toggle_bool destrs] start_lbl dest_lbl def 673 674 | AST.Op_cmpu AST.Cmp_ge | AST.Op_cmpp AST.Cmp_ge -> 623 675 add_translates 624 [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ; 625 translate_op1 AST.Op_notbool destrs destrs] 626 start_lbl dest_lbl def 627 628 | AST.Op_cmpp AST.Cmp_ge -> 629 add_translates 630 [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ; 631 translate_op1 AST.Op_notbool destrs destrs] 632 start_lbl dest_lbl def 676 [translate_ltu destrs srcrs1 srcrs2 ; 677 translate_toggle_bool destrs] start_lbl dest_lbl def 633 678 634 679 | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl … … 639 684 640 685 let translate_cond srcrs start_lbl lbl_true lbl_false def = 641 let (def, tmpr) = fresh_reg def in 642 let tmp_lbl = fresh_label def in 643 let init = RTL.St_int (tmpr, 0, start_lbl) in 644 let f srcr = RTL.St_op2 (I8051.Or, tmpr, tmpr, srcr, start_lbl) in 645 let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in 646 add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def 686 match srcrs with 687 | [] -> add_graph start_lbl (RTL.St_skip lbl_false) def 688 | srcr :: srcrs -> 689 let (def, tmpr) = fresh_reg def in 690 let tmp_lbl = fresh_label def in 691 let init = RTL.St_move (tmpr, RTL.Reg srcr, start_lbl) in 692 let f srcr = RTL.St_op2 (I8051.Or, tmpr, tmpr, RTL.Reg srcr, start_lbl) in 693 let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in 694 add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def 647 695 648 696 … … 656 704 let translates = 657 705 translates @ 658 [adds_graph [RTL.St_ int (tmpr,off, start_lbl)] ;706 [adds_graph [RTL.St_move (tmpr, RTL.Imm off, start_lbl)] ; 659 707 translate_op2 AST.Op_addp tmp_addr save_addr [tmpr] ; 660 708 adds_graph [RTL.St_load (r, tmp_addr1, tmp_addr2, dest_lbl)]] in … … 671 719 let translates = 672 720 translates @ 673 [adds_graph [RTL.St_ int (tmpr,off, start_lbl)] ;721 [adds_graph [RTL.St_move (tmpr, RTL.Imm off, start_lbl)] ; 674 722 translate_op2 AST.Op_addp tmp_addr addr [tmpr] ; 675 723 adds_graph [RTL.St_store (tmp_addr1, tmp_addr2, srcr, dest_lbl)]] in … … 747 795 | RTLabs.St_return (Some r) -> 748 796 add_graph lbl (RTL.St_return (find_local_env r lenv)) def 749 797 750 798 | _ -> assert false (*not possible because of previous removal of immediates*) 751 799 -
Deliverables/D2.2/8051/src/common/intValue.ml
r818 r1568 66 66 val logxor : t -> t -> t 67 67 val shl : t -> t -> t 68 val rotl : t -> t 68 69 val shr : t -> t -> t 69 70 val shrl : t -> t -> t … … 176 177 let pow = power_int_positive_big_int 2 (cast b) in 177 178 cast (mult_big_int a pow) 179 180 let rotl a = 181 if ge_big_int a half_bound then 182 cast (add_big_int (mult_big_int a two) one) 183 else 184 cast (mult_big_int a two) 178 185 179 186 let shr a b = -
Deliverables/D2.2/8051/src/common/intValue.mli
r818 r1568 62 62 val logxor : t -> t -> t 63 63 val shl : t -> t -> t 64 val rotl : t -> t 64 65 val shr : t -> t -> t 65 66 val shrl : t -> t -> t -
Deliverables/D2.2/8051/src/common/memory.ml
r818 r1568 8 8 9 9 let error_prefix = "Memory" 10 let error s = Error.global_error error_prefix s10 let error s = invalid_arg (error_prefix ^ s) 11 11 12 12 -
Deliverables/D2.2/8051/src/common/value.ml
r818 r1568 113 113 val xor : t -> t -> t 114 114 val shl : t -> t -> t 115 val rotl : t -> t 115 116 val shr : t -> t -> t 116 117 val shru : t -> t -> t … … 376 377 let xor = binary_int_op ValInt.logxor 377 378 let shl = binary_int_op ValInt.shl 379 let rotl = unary_int_op ValInt.rotl 378 380 let shr = binary_int_op ValInt.shr 379 381 let shru = binary_int_op ValInt.shrl -
Deliverables/D2.2/8051/src/common/value.mli
r818 r1568 105 105 val xor : t -> t -> t 106 106 val shl : t -> t -> t 107 val rotl : t -> t 107 108 val shr : t -> t -> t 108 109 val shru : t -> t -> t
Note: See TracChangeset
for help on using the changeset viewer.