open BitVectors;; open Physical;; open ASM;; open IntelHex;; open Util;; open Parser;; exception Fetch_exception of string;; exception CodeTooLarge;; exception Halt;; let extract = function | Some a -> a | None -> raise (Failure "ASMInterpret.extract") type time = int;; type line = [ `P1 of byte | `P3 of byte | `SerialBuff of [ `Eight of byte | `Nine of BitVectors.bit * byte ]];; let string_of_line = function `P1 b -> "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^ "P1 OUTPUT: " ^ hex_string_of_vect b ^ "\n" ^ "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" | `P3 b -> "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^ "P2 OUTPUT: " ^ hex_string_of_vect b ^ "\n" ^ "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" | `SerialBuff (`Eight b) -> "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^ "SERIAL 8b OUTPUT: " ^ string_of_vect b ^ "\n" ^ "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" | `SerialBuff (`Nine (b, b')) -> "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^ "SERIAL 9b OUTPUT: " ^ (let i = int_of_vect b' in if b then string_of_int (128 + i) else string_of_int i) ^ "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" (* In: reception time, line of input, new continuation, Out: transmission time, output line, expected duration until reply, new continuation. *) type epsilon = int type continuation = [`In of time * line * epsilon * continuation] option * [`Out of (time -> line -> time * continuation)] let rec debug_continuation = (Some (`In (1, (`SerialBuff (`Eight (vect_of_int 5 `Eight))), 0, debug_continuation))), `Out ( fun time line -> (* let _ = prerr_endline <*> string_of_line $ line in *) (time + 1),debug_continuation) (* no differentiation between internal and external code memory *) type status = { (* Memory *) code_memory: Physical.WordMap.map; (* can be reduced *) low_internal_ram: Byte7Map.map; high_internal_ram: Byte7Map.map; external_ram: Physical.WordMap.map; (* Program counter *) pc: word; (* SFRs *) sp: byte; dpl: byte; dph: byte; pcon: byte; tcon: byte; tmod: byte; tl0: byte; tl1: byte; th0: byte; th1: byte; p1: byte; scon: byte; sbuf: byte; ie: byte; p3: byte; ip: byte; psw: byte; acc: byte; b: byte; t2con: byte; (* 8052 only *) rcap2l: byte; (* 8052 only *) rcap2h: byte; (* 8052 only *) tl2: byte; (* 8052 only *) th2: byte; (* 8052 only *) (* Latches for the output lines *) p1_latch: byte; p3_latch: byte; (* Fields for tracking the state of the processor. *) (* IO specific *) previous_p1_val: bool; previous_p3_val: bool; serial_epsilon_out: epsilon option; serial_epsilon_in: epsilon option; io_epsilon: epsilon; serial_v_in: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option; serial_v_out: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option; serial_k_out: continuation option; io: continuation; expected_out_time: [ `None | `Now | `At of time ]; (* Timer and clock specific *) clock: time; timer0: word; timer1: word; timer2: word; (* can be missing *) esi_running: bool; t0i_running: bool; t1i_running: bool; e0i_running: bool; e1i_running: bool; es_running: bool; exit_addr : BitVectors.word; cost_labels : string BitVectors.WordMap.t } (* Try to understand what DEC really does!!! *) (* Try to understand I/O *) let get_sfr status addr from_latch = match int_of_vect addr with (* I/O and timer ports *) 0x80 -> assert false (* P0 not modeled *) | 0x90 -> if from_latch then status.p1_latch else status.p1 | 0xA0 -> assert false (* P2 not modeled *) | 0xB0 -> if from_latch then status.p3_latch else status.p3 | 0x99 -> status.sbuf | 0x8A -> status.tl0 | 0x8B -> status.tl1 | 0x8C -> status.th0 | 0x8D -> status.th1 | 0xC8 -> status.t2con | 0xCA -> status.rcap2l | 0xCB -> status.rcap2h | 0xCC -> status.tl2 | 0xCD -> status.th2 (* control ports *) | 0x87 -> status.pcon | 0x88 -> status.tcon | 0x89 -> status.tmod | 0x98 -> status.scon | 0xA8 -> status.ie | 0xB8 -> status.ip (* registers *) | 0x81 -> status.sp | 0x82 -> status.dpl | 0x83 -> status.dph | 0xD0 -> status.psw | 0xE0 -> status.acc | 0xF0 -> status.b | _ -> assert false ;; (* Try to understand I/O *) let set_sfr status addr v = match int_of_vect addr with (* I/O and timer ports *) 0x80 -> assert false (* P0 not modeled *) | 0x90 -> { status with p1 = v; p1_latch = v } | 0xA0 -> assert false (* P2 not modeled *) | 0xB0 -> { status with p3 = v; p3_latch = v } | 0x99 -> if status.expected_out_time = `None then { status with sbuf = v; expected_out_time = `Now } else (* a real assert false: trying to initiate a transmission whilst one is still active *) assert false | 0x8A -> { status with tl0 = v } | 0x8B -> { status with tl1 = v } | 0x8C -> { status with th0 = v } | 0x8D -> { status with th1 = v } | 0xC8 -> { status with t2con = v } | 0xCA -> { status with rcap2l = v } | 0xCB -> { status with rcap2h = v } | 0xCD -> { status with tl2 = v } | 0xCE -> { status with th2 = v } (* control ports *) | 0x87 -> { status with pcon = v } | 0x88 -> { status with tcon = v } | 0x89 -> { status with tmod = v } | 0x98 -> { status with scon = v } | 0xA8 -> { status with ie = v } | 0xB8 -> { status with ip = v } (* registers *) | 0x81 -> { status with sp = v } | 0x82 -> { status with dpl = v } | 0x83 -> { status with dph = v } | 0xD0 -> { status with psw = v } | 0xE0 -> { status with acc = v } | 0xF0 -> { status with b = v } | _ -> assert false ;; let initialize = { code_memory = Physical.WordMap.empty; low_internal_ram = Byte7Map.empty; high_internal_ram = Byte7Map.empty; external_ram = Physical.WordMap.empty; pc = zero `Sixteen; sp = vect_of_int 7 `Eight; dpl = zero `Eight; dph = zero `Eight; pcon = zero `Eight; tcon = zero `Eight; tmod = zero `Eight; tl0 = zero `Eight; tl1 = zero `Eight; th0 = zero `Eight; th1 = zero `Eight; p1 = zero `Eight; p1_latch = zero `Eight; scon = zero `Eight; sbuf = zero `Eight; ie = zero `Eight; p3 = zero `Eight; p3_latch = zero `Eight; ip = zero `Eight; psw = zero `Eight; acc = zero `Eight; b = zero `Eight; t2con = zero `Eight; rcap2l = zero `Eight; rcap2h = zero `Eight; tl2 = zero `Eight; th2 = zero `Eight; previous_p1_val = false; previous_p3_val = false; serial_v_in = None; serial_v_out = None; serial_epsilon_in = None; serial_epsilon_out = None; serial_k_out = None; io_epsilon = 5; clock = 0; timer0 = zero `Sixteen; timer1 = zero `Sixteen; timer2 = zero `Sixteen; expected_out_time = `None; io = debug_continuation; (* a real assert false: unprepared for i/o *) (* Initially no interrupts are executing *) esi_running = false; t0i_running = false; t1i_running = false; e0i_running = false; e1i_running = false; es_running = false; exit_addr = BitVectors.zero `Sixteen; cost_labels = BitVectors.WordMap.empty } let get_cy_flag status = let (cy,_,_,_),(_,_,_,_) = bits_of_byte status.psw in cy let get_ac_flag status = let (_,ac,_,_),(_,_,_,_) = bits_of_byte status.psw in ac let get_fo_flag status = let (_,_,fo,_),(_,_,_,_) = bits_of_byte status.psw in fo let get_rs1_flag status = let (_,_,_,rs1),(_,_,_,_) = bits_of_byte status.psw in rs1 let get_rs0_flag status = let (_,_,_,_),(rs0,_,_,_) = bits_of_byte status.psw in rs0 let get_ov_flag status = let (_,_,_,_),(_,ov,_,_) = bits_of_byte status.psw in ov let get_ud_flag status = let (_,_,_,_),(_,_,ud,_) = bits_of_byte status.psw in ud let get_p_flag status = let (_,_,_,_),(_,_,_,p) = bits_of_byte status.psw in p let get_address_of_register status (b1,b2,b3) = let bu,_bl = from_byte status.psw in let (_,_,rs1,rs0) = from_nibble bu in let base = match rs1,rs0 with false,false -> 0x00 | false,true -> 0x08 | true,false -> 0x10 | true,true -> 0x18 in vect_of_int (base + int_of_vect (mk_nibble false b1 b2 b3)) `Seven ;; let get_register status reg = let addr = get_address_of_register status reg in Byte7Map.find addr status.low_internal_ram ;; let string_of_status status = let acc_str = (string_of_int <*> int_of_vect $ status.acc) ^ " (" ^ string_of_vect status.acc ^ ")" in let b_str = (string_of_int <*> int_of_vect $ status.b) ^ " (" ^ string_of_vect status.b ^ ")" in let psw_str = (string_of_int <*> int_of_vect $ status.psw) ^ " (" ^ string_of_vect status.psw ^ ")" in let sp_str = (string_of_int <*> int_of_vect $ status.sp) ^ " (" ^ string_of_vect status.sp ^ ")" in let ip_str = (string_of_int <*> int_of_vect $ status.ip) ^ " (" ^ string_of_vect status.ip ^ ")" in let pc_str = (string_of_int <*> int_of_vect $ status.pc) ^ " (" ^ string_of_vect status.pc ^ ")" in let dpl_str = (string_of_int <*> int_of_vect $ status.dpl) ^ " (" ^ string_of_vect status.dpl ^ ")" in let dph_str = (string_of_int <*> int_of_vect $ status.dph) ^ " (" ^ string_of_vect status.dph ^ ")" in let scn_str = (string_of_int <*> int_of_vect $ status.scon) ^ " (" ^ string_of_vect status.scon ^ ")" in let sbf_str = (string_of_int <*> int_of_vect $ status.sbuf) ^ " (" ^ string_of_vect status.sbuf ^ ")" in let tcn_str = (string_of_int <*> int_of_vect $ status.tcon) ^ " (" ^ string_of_vect status.tcon ^ ")" in let tmd_str = (string_of_int <*> int_of_vect $ status.tmod) ^ " (" ^ string_of_vect status.tmod ^ ")" in let r0_str = (string_of_int <*> int_of_vect $ get_register status (false, false, false)) ^ " (" ^ (string_of_vect $ get_register status (false, false, false)) ^ ")" in let r1_str = (string_of_int <*> int_of_vect $ get_register status (false, false, true)) ^ " (" ^ (string_of_vect $ get_register status (false, false, true)) ^ ")" in let r2_str = (string_of_int <*> int_of_vect $ get_register status (false, true, false)) ^ " (" ^ (string_of_vect $ get_register status (false, true, false)) ^ ")" in let r3_str = (string_of_int <*> int_of_vect $ get_register status (false, true, true)) ^ " (" ^ (string_of_vect $ get_register status (false, true, true)) ^ ")" in let r4_str = (string_of_int <*> int_of_vect $ get_register status (true, false, false)) ^ " (" ^ (string_of_vect $ get_register status (true, false, false)) ^ ")" in let r5_str = (string_of_int <*> int_of_vect $ get_register status (true, false, true)) ^ " (" ^ (string_of_vect $ get_register status (true, false, true)) ^ ")" in let r6_str = (string_of_int <*> int_of_vect $ get_register status (true, true, false)) ^ " (" ^ (string_of_vect $ get_register status (true, true, false)) ^ ")" in let r7_str = (string_of_int <*> int_of_vect $ get_register status (true, true, true)) ^ " (" ^ (string_of_vect $ get_register status (true, true, true)) ^ ")" in "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^ " Processor status: \n" ^ "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^ " ACC : " ^ acc_str ^ "\n" ^ " B : " ^ b_str ^ "\n" ^ " PSW : " ^ psw_str ^ "\n" ^ " with flags set as \n" ^ " CY : " ^ (string_of_bool <*> get_cy_flag $ status) ^ "\n" ^ " AC : " ^ (string_of_bool <*> get_ac_flag $ status) ^ "\n" ^ " FO : " ^ (string_of_bool <*> get_fo_flag $ status) ^ "\n" ^ " RS1 : " ^ (string_of_bool <*> get_rs1_flag $ status) ^ "\n" ^ " RS0 : " ^ (string_of_bool <*> get_rs0_flag $ status) ^ "\n" ^ " OV : " ^ (string_of_bool <*> get_ov_flag $ status) ^ "\n" ^ " UD : " ^ (string_of_bool <*> get_ud_flag $ status) ^ "\n" ^ " P : " ^ (string_of_bool <*> get_p_flag $ status) ^ "\n" ^ " SP : " ^ sp_str ^ "\n" ^ " IP : " ^ ip_str ^ "\n" ^ " PC : " ^ pc_str ^ "\n" ^ " DPL : " ^ dpl_str ^ "\n" ^ " DPH : " ^ dph_str ^ "\n" ^ " SCON: " ^ scn_str ^ "\n" ^ " SBUF: " ^ sbf_str ^ "\n" ^ " TMOD: " ^ tmd_str ^ "\n" ^ " TCON: " ^ tcn_str ^ "\n" ^ " Registers: \n" ^ " R0 : " ^ r0_str ^ "\n" ^ " R1 : " ^ r1_str ^ "\n" ^ " R2 : " ^ r2_str ^ "\n" ^ " R3 : " ^ r3_str ^ "\n" ^ " R4 : " ^ r4_str ^ "\n" ^ " R5 : " ^ r5_str ^ "\n" ^ " R6 : " ^ r6_str ^ "\n" ^ " R7 : " ^ r7_str ^ "\n" ^ "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" (* timings taken from SIEMENS *) let fetch pmem pc = let next pc = let _carry, res = half_add pc (vect_of_int 1 `Sixteen) in res, Physical.WordMap.find pc pmem in let pc,instr = next pc in let un, ln = from_byte instr in let bits = (from_nibble un, from_nibble ln) in match bits with (a10,a9,a8,true),(false,false,false,true) -> let pc,b1 = next pc in `ACALL (`ADDR11 (mk_word11 a10 a9 a8 b1)), pc, 2 | (false,false,true,false),(true,r1,r2,r3) -> `ADD (`A,`REG (r1,r2,r3)), pc, 1 | (false,false,true,false),(false,true,false,true) -> let pc,b1 = next pc in `ADD (`A,`DIRECT b1), pc, 1 | (false,false,true,false),(false,true,true,i1) -> `ADD (`A,`INDIRECT i1), pc, 1 | (false,false,true,false),(false,true,false,false) -> let pc,b1 = next pc in `ADD (`A,`DATA b1), pc, 1 | (false,false,true,true),(true,r1,r2,r3) -> `ADDC (`A,`REG (r1,r2,r3)), pc, 1 | (false,false,true,true),(false,true,false,true) -> let pc,b1 = next pc in `ADDC (`A,`DIRECT b1), pc, 1 | (false,false,true,true),(false,true,true,i1) -> `ADDC (`A,`INDIRECT i1), pc, 1 | (false,false,true,true),(false,true,false,false) -> let pc,b1 = next pc in `ADDC (`A,`DATA b1), pc, 1 | (a10,a9,a8,false),(false,false,false,true) -> let pc,b1 = next pc in `AJMP (`ADDR11 (mk_word11 a10 a9 a8 b1)), pc, 2 | (false,true,false,true),(true,r1,r2,r3) -> `ANL (`U1 (`A, `REG (r1,r2,r3))), pc, 1 | (false,true,false,true),(false,true,false,true) -> let pc,b1 = next pc in `ANL (`U1 (`A, `DIRECT b1)), pc, 1 | (false,true,false,true),(false,true,true,i1) -> `ANL (`U1 (`A, `INDIRECT i1)), pc, 1 | (false,true,false,true),(false,true,false,false) -> let pc,b1 = next pc in `ANL (`U1 (`A, `DATA b1)), pc, 1 | (false,true,false,true),(false,false,true,false) -> let pc,b1 = next pc in `ANL (`U2 (`DIRECT b1,`A)), pc, 1 | (false,true,false,true),(false,false,true,true) -> let pc,b1 = next pc in let pc,b2 = next pc in `ANL (`U2 (`DIRECT b1,`DATA b2)), pc, 2 | (true,false,false,false),(false,false,true,false) -> let pc,b1 = next pc in `ANL (`U3 (`C,`BIT b1)), pc, 2 | (true,false,true,true),(false,false,false,false) -> let pc,b1 = next pc in `ANL (`U3 (`C,`NBIT b1)), pc, 2 | (true,false,true,true),(false,true,false,true) -> let pc,b1 = next pc in let pc,b2 = next pc in `CJNE (`U1 (`A, `DIRECT b1), `REL b2), pc, 2 | (true,false,true,true),(false,true,false,false) -> let pc,b1 = next pc in let pc,b2 = next pc in `CJNE (`U1 (`A, `DATA b1), `REL b2), pc, 2 | (true,false,true,true),(true,r1,r2,r3) -> let pc,b1 = next pc in let pc,b2 = next pc in `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2), pc, 2 | (true,false,true,true),(false,true,true,i1) -> let pc,b1 = next pc in let pc,b2 = next pc in `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2), pc, 2 | (true,true,true,false),(false,true,false,false) -> `CLR `A, pc, 1 | (true,true,false,false),(false,false,true,true) -> `CLR `C, pc, 1 | (true,true,false,false),(false,false,true,false) -> let pc,b1 = next pc in `CLR (`BIT b1), pc, 1 | (true,true,true,true),(false,true,false,false) -> `CPL `A, pc, 1 | (true,false,true,true),(false,false,true,true) -> `CPL `C, pc, 1 | (true,false,true,true),(false,false,true,false) -> let pc,b1 = next pc in `CPL (`BIT b1), pc, 1 | (true,true,false,true),(false,true,false,false) -> `DA `A, pc, 1 | (false,false,false,true),(false,true,false,false) -> `DEC `A, pc, 1 | (false,false,false,true),(true,r1,r2,r3) -> `DEC (`REG(r1,r2,r3)), pc, 1 | (false,false,false,true),(false,true,false,true) -> let pc,b1 = next pc in `DEC (`DIRECT b1), pc, 1 | (false,false,false,true),(false,true,true,i1) -> `DEC (`INDIRECT i1), pc, 1 | (true,false,false,false),(false,true,false,false) -> `DIV (`A, `B), pc, 4 | (true,true,false,true),(true,r1,r2,r3) -> let pc,b1 = next pc in `DJNZ (`REG(r1,r2,r3), `REL b1), pc, 2 | (true,true,false,true),(false,true,false,true) -> let pc,b1 = next pc in let pc,b2 = next pc in `DJNZ (`DIRECT b1, `REL b2), pc, 2 | (false,false,false,false),(false,true,false,false) -> `INC `A, pc, 1 | (false,false,false,false),(true,r1,r2,r3) -> `INC (`REG(r1,r2,r3)), pc, 1 | (false,false,false,false),(false,true,false,true) -> let pc,b1 = next pc in `INC (`DIRECT b1), pc, 1 | (false,false,false,false),(false,true,true,i1) -> `INC (`INDIRECT i1), pc, 1 | (true,false,true,false),(false,false,true,true) -> `INC `DPTR, pc, 2 | (false,false,true,false),(false,false,false,false) -> let pc,b1 = next pc in let pc,b2 = next pc in `JB (`BIT b1, `REL b2), pc, 2 | (false,false,false,true),(false,false,false,false) -> let pc,b1 = next pc in let pc,b2 = next pc in `JBC (`BIT b1, `REL b2), pc, 2 | (false,true,false,false),(false,false,false,false) -> let pc,b1 = next pc in `JC (`REL b1), pc, 2 | (false,true,true,true),(false,false,true,true) -> `JMP `IND_DPTR, pc, 2 | (false,false,true,true),(false,false,false,false) -> let pc,b1 = next pc in let pc,b2 = next pc in `JNB (`BIT b1, `REL b2), pc, 2 | (false,true,false,true),(false,false,false,false) -> let pc,b1 = next pc in `JNC (`REL b1), pc, 2 | (false,true,true,true),(false,false,false,false) -> let pc,b1 = next pc in `JNZ (`REL b1), pc, 2 | (false,true,true,false),(false,false,false,false) -> let pc,b1 = next pc in `JZ (`REL b1), pc, 2 | (false,false,false,true),(false,false,true,false) -> let pc,b1 = next pc in let pc,b2 = next pc in `LCALL (`ADDR16 (mk_word b1 b2)), pc, 2 | (false,false,false,false),(false,false,true,false) -> let pc,b1 = next pc in let pc,b2 = next pc in `LJMP (`ADDR16 (mk_word b1 b2)), pc, 2 | (true,true,true,false),(true,r1,r2,r3) -> `MOV (`U1 (`A, `REG(r1,r2,r3))), pc, 1 | (true,true,true,false),(false,true,false,true) -> let pc,b1 = next pc in `MOV (`U1 (`A, `DIRECT b1)), pc, 1 | (true,true,true,false),(false,true,true,i1) -> `MOV (`U1 (`A, `INDIRECT i1)), pc, 1 | (false,true,true,true),(false,true,false,false) -> let pc,b1 = next pc in `MOV (`U1 (`A, `DATA b1)), pc, 1 | (true,true,true,true),(true,r1,r2,r3) -> `MOV (`U2 (`REG(r1,r2,r3), `A)), pc, 1 | (true,false,true,false),(true,r1,r2,r3) -> let pc,b1 = next pc in `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))), pc, 2 | (false,true,true,true),(true,r1,r2,r3) -> let pc,b1 = next pc in `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))), pc, 1 | (true,true,true,true),(false,true,false,true) -> let pc,b1 = next pc in `MOV (`U3 (`DIRECT b1, `A)), pc, 1 | (true,false,false,false),(true,r1,r2,r3) -> let pc,b1 = next pc in `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))), pc, 2 | (true,false,false,false),(false,true,false,true) -> let pc,b1 = next pc in let pc,b2 = next pc in `MOV (`U3 (`DIRECT b1, `DIRECT b2)), pc, 2 | (true,false,false,false),(false,true,true,i1) -> let pc,b1 = next pc in `MOV (`U3 (`DIRECT b1, `INDIRECT i1)), pc, 2 | (false,true,true,true),(false,true,false,true) -> let pc,b1 = next pc in let pc,b2 = next pc in `MOV (`U3 (`DIRECT b1, `DATA b2)), pc, 3 | (true,true,true,true),(false,true,true,i1) -> `MOV (`U2 (`INDIRECT i1, `A)), pc, 1 | (true,false,true,false),(false,true,true,i1) -> let pc,b1 = next pc in `MOV (`U2 (`INDIRECT i1, `DIRECT b1)), pc, 2 | (false,true,true,true),(false,true,true,i1) -> let pc,b1 = next pc in `MOV (`U2 (`INDIRECT i1, `DATA b1)), pc, 1 | (true,false,true,false),(false,false,true,false) -> let pc,b1 = next pc in `MOV (`U5 (`C, `BIT b1)), pc, 1 | (true,false,false,true),(false,false,true,false) -> let pc,b1 = next pc in `MOV (`U6 (`BIT b1, `C)), pc, 2 | (true,false,false,true),(false,false,false,false) -> let pc,b1 = next pc in let pc,b2 = next pc in `MOV (`U4 (`DPTR, `DATA16(mk_word b1 b2))), pc, 2 | (true,false,false,true),(false,false,true,true) -> `MOVC (`A, `A_DPTR), pc, 2 | (true,false,false,false),(false,false,true,true) -> `MOVC (`A, `A_PC), pc, 2 | (true,true,true,false),(false,false,true,i1) -> `MOVX (`U1 (`A, `EXT_INDIRECT i1)), pc, 2 | (true,true,true,false),(false,false,false,false) -> `MOVX (`U1 (`A, `EXT_IND_DPTR)), pc, 2 | (true,true,true,true),(false,false,true,i1) -> `MOVX (`U2 (`EXT_INDIRECT i1, `A)), pc, 2 | (true,true,true,true),(false,false,false,false) -> `MOVX (`U2 (`EXT_IND_DPTR, `A)), pc, 2 | (true,false,true,false),(false,true,false,false) -> `MUL(`A, `B), pc, 4 | (false,false,false,false),(false,false,false,false) -> `NOP, pc, 1 | (false,true,false,false),(true,r1,r2,r3) -> `ORL (`U1(`A, `REG(r1,r2,r3))), pc, 1 | (false,true,false,false),(false,true,false,true) -> let pc,b1 = next pc in `ORL (`U1(`A, `DIRECT b1)), pc, 1 | (false,true,false,false),(false,true,true,i1) -> `ORL (`U1(`A, `INDIRECT i1)), pc, 1 | (false,true,false,false),(false,true,false,false) -> let pc,b1 = next pc in `ORL (`U1(`A, `DATA b1)), pc, 1 | (false,true,false,false),(false,false,true,false) -> let pc,b1 = next pc in `ORL (`U2(`DIRECT b1, `A)), pc, 1 | (false,true,false,false),(false,false,true,true) -> let pc,b1 = next pc in let pc,b2 = next pc in `ORL (`U2 (`DIRECT b1, `DATA b2)), pc, 2 | (false,true,true,true),(false,false,true,false) -> let pc,b1 = next pc in `ORL (`U3 (`C, `BIT b1)), pc, 2 | (true,false,true,false),(false,false,false,false) -> let pc,b1 = next pc in `ORL (`U3 (`C, `NBIT b1)), pc, 2 | (true,true,false,true),(false,false,false,false) -> let pc,b1 = next pc in `POP (`DIRECT b1), pc, 2 | (true,true,false,false),(false,false,false,false) -> let pc,b1 = next pc in `PUSH (`DIRECT b1), pc, 2 | (false,false,true,false),(false,false,true,false) -> `RET, pc, 2 | (false,false,true,true),(false,false,true,false) -> `RETI, pc, 2 | (false,false,true,false),(false,false,true,true) -> `RL `A, pc, 1 | (false,false,true,true),(false,false,true,true) -> `RLC `A, pc, 1 | (false,false,false,false),(false,false,true,true) -> `RR `A, pc, 1 | (false,false,false,true),(false,false,true,true) -> `RRC `A, pc, 1 | (true,true,false,true),(false,false,true,true) -> `SETB `C, pc, 1 | (true,true,false,true),(false,false,true,false) -> let pc,b1 = next pc in `SETB (`BIT b1), pc, 1 | (true,false,false,false),(false,false,false,false) -> let pc,b1 = next pc in `SJMP (`REL b1), pc, 2 | (true,false,false,true),(true,r1,r2,r3) -> `SUBB (`A, `REG(r1,r2,r3)), pc, 1 | (true,false,false,true),(false,true,false,true) -> let pc,b1 = next pc in `SUBB (`A, `DIRECT b1), pc, 1 | (true,false,false,true),(false,true,true,i1) -> `SUBB (`A, `INDIRECT i1), pc, 1 | (true,false,false,true),(false,true,false,false) -> let pc,b1 = next pc in `SUBB (`A, `DATA b1), pc, 1 | (true,true,false,false),(false,true,false,false) -> `SWAP `A, pc, 1 | (true,true,false,false),(true,r1,r2,r3) -> `XCH (`A, `REG(r1,r2,r3)), pc, 1 | (true,true,false,false),(false,true,false,true) -> let pc,b1 = next pc in `XCH (`A, `DIRECT b1), pc, 1 | (true,true,false,false),(false,true,true,i1) -> `XCH (`A, `INDIRECT i1), pc, 1 | (true,true,false,true),(false,true,true,i1) -> `XCHD(`A, `INDIRECT i1), pc, 1 | (false,true,true,false),(true,r1,r2,r3) -> `XRL(`U1(`A, `REG(r1,r2,r3))), pc, 1 | (false,true,true,false),(false,true,false,true) -> let pc,b1 = next pc in `XRL(`U1(`A, `DIRECT b1)), pc, 1 | (false,true,true,false),(false,true,true,i1) -> `XRL(`U1(`A, `INDIRECT i1)), pc, 1 | (false,true,true,false),(false,true,false,false) -> let pc,b1 = next pc in `XRL(`U1(`A, `DATA b1)), pc, 1 | (false,true,true,false),(false,false,true,false) -> let pc,b1 = next pc in `XRL(`U2(`DIRECT b1, `A)), pc, 1 | (false,true,true,false),(false,false,true,true) -> let pc,b1 = next pc in let pc,b2 = next pc in `XRL(`U2(`DIRECT b1, `DATA b2)), pc, 2 | (true,false,true,false),(false,true,false,true) -> (* undefined opcode *) assert false ;; let assembly1 = function `ACALL (`ADDR11 w) -> let (a10,a9,a8,b1) = from_word11 w in [mk_byte_from_bits ((a10,a9,a8,true),(false,false,false,true)); b1] | `ADD (`A,`REG (r1,r2,r3)) -> [mk_byte_from_bits ((false,false,true,false),(true,r1,r2,r3))] | `ADD (`A, `DIRECT b1) -> [mk_byte_from_bits ((false,false,true,false),(false,true,false,true)); b1] | `ADD (`A, `INDIRECT i1) -> [mk_byte_from_bits ((false,false,true,false),(false,true,true,i1))] | `ADD (`A, `DATA b1) -> [mk_byte_from_bits ((false,false,true,false),(false,true,false,false)); b1] | `ADDC (`A, `REG(r1,r2,r3)) -> [mk_byte_from_bits ((false,false,true,true),(true,r1,r2,r3))] | `ADDC (`A, `DIRECT b1) -> [mk_byte_from_bits ((false,false,true,true),(false,true,false,true)); b1] | `ADDC (`A,`INDIRECT i1) -> [mk_byte_from_bits ((false,false,true,true),(false,true,true,i1))] | `ADDC (`A,`DATA b1) -> [mk_byte_from_bits ((false,false,true,true),(false,true,false,false)); b1] | `AJMP (`ADDR11 w) -> let (a10,a9,a8,b1) = from_word11 w in [mk_byte_from_bits ((a10,a9,a8,false),(false,false,false,true)); b1] | `ANL (`U1 (`A, `REG (r1,r2,r3))) -> [mk_byte_from_bits ((false,true,false,true),(true,r1,r2,r3))] | `ANL (`U1 (`A, `DIRECT b1)) -> [mk_byte_from_bits ((false,true,false,true),(false,true,false,true)); b1] | `ANL (`U1 (`A, `INDIRECT i1)) -> [mk_byte_from_bits ((false,true,false,true),(false,true,true,i1))] | `ANL (`U1 (`A, `DATA b1)) -> [mk_byte_from_bits ((false,true,false,true),(false,true,false,false)); b1] | `ANL (`U2 (`DIRECT b1,`A)) -> [mk_byte_from_bits ((false,true,false,true),(false,false,true,false)); b1] | `ANL (`U2 (`DIRECT b1,`DATA b2)) -> [mk_byte_from_bits ((false,true,false,true),(false,false,true,true)); b1; b2] | `ANL (`U3 (`C,`BIT b1)) -> [mk_byte_from_bits ((true,false,false,false),(false,false,true,false)); b1] | `ANL (`U3 (`C,`NBIT b1)) -> [mk_byte_from_bits ((true,false,true,true),(false,false,false,false)); b1] | `CJNE (`U1 (`A, `DIRECT b1), `REL b2) -> [mk_byte_from_bits ((true,false,true,true),(false,true,false,true)); b1; b2] | `CJNE (`U1 (`A, `DATA b1), `REL b2) -> [mk_byte_from_bits ((true,false,true,true),(false,true,false,false)); b1; b2] | `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2) -> [mk_byte_from_bits ((true,false,true,true),(true,r1,r2,r3)); b1; b2] | `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) -> [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2] | `CLR `A -> [mk_byte_from_bits ((true,true,true,false),(false,true,false,false))] | `CLR `C -> [mk_byte_from_bits ((true,true,false,false),(false,false,true,true))] | `CLR (`BIT b1) -> [mk_byte_from_bits ((true,true,false,false),(false,false,true,false)); b1] | `CPL `A -> [mk_byte_from_bits ((true,true,true,true),(false,true,false,false))] | `CPL `C -> [mk_byte_from_bits ((true,false,true,true),(false,false,true,true))] | `CPL (`BIT b1) -> [mk_byte_from_bits ((true,false,true,true),(false,false,true,false)); b1] | `DA `A -> [mk_byte_from_bits ((true,true,false,true),(false,true,false,false))] | `DEC `A -> [mk_byte_from_bits ((false,false,false,true),(false,true,false,false))] | `DEC (`REG(r1,r2,r3)) -> [mk_byte_from_bits ((false,false,false,true),(true,r1,r2,r3))] | `DEC (`DIRECT b1) -> [mk_byte_from_bits ((false,false,false,true),(false,true,false,true)); b1] | `DEC (`INDIRECT i1) -> [mk_byte_from_bits ((false,false,false,true),(false,true,true,i1))] | `DIV (`A, `B) -> [mk_byte_from_bits ((true,false,false,false),(false,true,false,false))] | `DJNZ (`REG(r1,r2,r3), `REL b1) -> [mk_byte_from_bits ((true,true,false,true),(true,r1,r2,r3)); b1] | `DJNZ (`DIRECT b1, `REL b2) -> [mk_byte_from_bits ((true,true,false,true),(false,true,false,true)); b1; b2] | `INC `A -> [mk_byte_from_bits ((false,false,false,false),(false,true,false,false))] | `INC (`REG(r1,r2,r3)) -> [mk_byte_from_bits ((false,false,false,false),(true,r1,r2,r3))] | `INC (`DIRECT b1) -> [mk_byte_from_bits ((false,false,false,false),(false,true,false,true)); b1] | `INC (`INDIRECT i1) -> [mk_byte_from_bits ((false,false,false,false),(false,true,true,i1))] | `INC `DPTR -> [mk_byte_from_bits ((true,false,true,false),(false,false,true,true))] | `JB (`BIT b1, `REL b2) -> [mk_byte_from_bits ((false,false,true,false),(false,false,false,false)); b1; b2] | `JBC (`BIT b1, `REL b2) -> [mk_byte_from_bits ((false,false,false,true),(false,false,false,false)); b1; b2] | `JC (`REL b1) -> [mk_byte_from_bits ((false,true,false,false),(false,false,false,false)); b1] | `JMP `IND_DPTR -> [mk_byte_from_bits ((false,true,true,true),(false,false,true,true))] | `JNB (`BIT b1, `REL b2) -> [mk_byte_from_bits ((false,false,true,true),(false,false,false,false)); b1; b2] | `JNC (`REL b1) -> [mk_byte_from_bits ((false,true,false,true),(false,false,false,false)); b1] | `JNZ (`REL b1) -> [mk_byte_from_bits ((false,true,true,true),(false,false,false,false)); b1] | `JZ (`REL b1) -> [mk_byte_from_bits ((false,true,true,false),(false,false,false,false)); b1] | `LCALL (`ADDR16 w) -> let (b1,b2) = from_word w in [mk_byte_from_bits ((false,false,false,true),(false,false,true,false)); b1; b2] | `LJMP (`ADDR16 w) -> let (b1,b2) = from_word w in [mk_byte_from_bits ((false,false,false,false),(false,false,true,false)); b1; b2] | `MOV (`U1 (`A, `REG(r1,r2,r3))) -> [mk_byte_from_bits ((true,true,true,false),(true,r1,r2,r3))] | `MOV (`U1 (`A, `DIRECT b1)) -> [mk_byte_from_bits ((true,true,true,false),(false,true,false,true)); b1] | `MOV (`U1 (`A, `INDIRECT i1)) -> [mk_byte_from_bits ((true,true,true,false),(false,true,true,i1))] | `MOV (`U1 (`A, `DATA b1)) -> [mk_byte_from_bits ((false,true,true,true),(false,true,false,false)); b1] | `MOV (`U2 (`REG(r1,r2,r3), `A)) -> [mk_byte_from_bits ((true,true,true,true),(true,r1,r2,r3))] | `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))) -> [mk_byte_from_bits ((true,false,true,false),(true,r1,r2,r3)); b1] | `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))) -> [mk_byte_from_bits ((false,true,true,true),(true,r1,r2,r3)); b1] | `MOV (`U3 (`DIRECT b1, `A)) -> [mk_byte_from_bits ((true,true,true,true),(false,true,false,true)); b1] | `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))) -> [mk_byte_from_bits ((true,false,false,false),(true,r1,r2,r3)); b1] | `MOV (`U3 (`DIRECT b1, `DIRECT b2)) -> [mk_byte_from_bits ((true,false,false,false),(false,true,false,true)); b1; b2] | `MOV (`U3 (`DIRECT b1, `INDIRECT i1)) -> [mk_byte_from_bits ((true,false,false,false),(false,true,true,i1)); b1] | `MOV (`U3 (`DIRECT b1, `DATA b2)) -> [mk_byte_from_bits ((false,true,true,true),(false,true,false,true)); b1; b2] | `MOV (`U2 (`INDIRECT i1, `A)) -> [mk_byte_from_bits ((true,true,true,true),(false,true,true,i1))] | `MOV (`U2 (`INDIRECT i1, `DIRECT b1)) -> [mk_byte_from_bits ((true,false,true,false),(false,true,true,i1)); b1] | `MOV (`U2 (`INDIRECT i1, `DATA b1)) -> [mk_byte_from_bits ((false,true,true,true),(false,true,true,i1)); b1] | `MOV (`U5 (`C, `BIT b1)) -> [mk_byte_from_bits ((true,false,true,false),(false,false,true,false)); b1] | `MOV (`U6 (`BIT b1, `C)) -> [mk_byte_from_bits ((true,false,false,true),(false,false,true,false)); b1] | `MOV (`U4 (`DPTR, `DATA16 w)) -> let (b1,b2) = from_word w in [mk_byte_from_bits ((true,false,false,true),(false,false,false,false)); b1; b2] | `MOVC (`A, `A_DPTR) -> [mk_byte_from_bits ((true,false,false,true),(false,false,true,true))] | `MOVC (`A, `A_PC) -> [mk_byte_from_bits ((true,false,false,false),(false,false,true,true))] | `MOVX (`U1 (`A, `EXT_INDIRECT i1)) -> [mk_byte_from_bits ((true,true,true,false),(false,false,true,i1))] | `MOVX (`U1 (`A, `EXT_IND_DPTR)) -> [mk_byte_from_bits ((true,true,true,false),(false,false,false,false))] | `MOVX (`U2 (`EXT_INDIRECT i1, `A)) -> [mk_byte_from_bits ((true,true,true,true),(false,false,true,i1))] | `MOVX (`U2 (`EXT_IND_DPTR, `A)) -> [mk_byte_from_bits ((true,true,true,true),(false,false,false,false))] | `MUL(`A, `B) -> [mk_byte_from_bits ((true,false,true,false),(false,true,false,false))] | `NOP -> [mk_byte_from_bits ((false,false,false,false),(false,false,false,false))] | `ORL (`U1(`A, `REG(r1,r2,r3))) -> [mk_byte_from_bits ((false,true,false,false),(true,r1,r2,r3))] | `ORL (`U1(`A, `DIRECT b1)) -> [mk_byte_from_bits ((false,true,false,false),(false,true,false,true)); b1] | `ORL (`U1(`A, `INDIRECT i1)) -> [mk_byte_from_bits ((false,true,false,false),(false,true,true,i1))] | `ORL (`U1(`A, `DATA b1)) -> [mk_byte_from_bits ((false,true,false,false),(false,true,false,false)); b1] | `ORL (`U2(`DIRECT b1, `A)) -> [mk_byte_from_bits ((false,true,false,false),(false,false,true,false)); b1] | `ORL (`U2 (`DIRECT b1, `DATA b2)) -> [mk_byte_from_bits ((false,true,false,false),(false,false,true,true)); b1; b2] | `ORL (`U3 (`C, `BIT b1)) -> [mk_byte_from_bits ((false,true,true,true),(false,false,true,false)); b1] | `ORL (`U3 (`C, `NBIT b1)) -> [mk_byte_from_bits ((true,false,true,false),(false,false,false,false)); b1] | `POP (`DIRECT b1) -> [mk_byte_from_bits ((true,true,false,true),(false,false,false,false)); b1] | `PUSH (`DIRECT b1) -> [mk_byte_from_bits ((true,true,false,false),(false,false,false,false)); b1] | `RET -> [mk_byte_from_bits ((false,false,true,false),(false,false,true,false))] | `RETI -> [mk_byte_from_bits ((false,false,true,true),(false,false,true,false))] | `RL `A -> [mk_byte_from_bits ((false,false,true,false),(false,false,true,true))] | `RLC `A -> [mk_byte_from_bits ((false,false,true,true),(false,false,true,true))] | `RR `A -> [mk_byte_from_bits ((false,false,false,false),(false,false,true,true))] | `RRC `A -> [mk_byte_from_bits ((false,false,false,true),(false,false,true,true))] | `SETB `C -> [mk_byte_from_bits ((true,true,false,true),(false,false,true,true))] | `SETB (`BIT b1) -> [mk_byte_from_bits ((true,true,false,true),(false,false,true,false)); b1] | `SJMP (`REL b1) -> [mk_byte_from_bits ((true,false,false,false),(false,false,false,false)); b1] | `SUBB (`A, `REG(r1,r2,r3)) -> [mk_byte_from_bits ((true,false,false,true),(true,r1,r2,r3))] | `SUBB (`A, `DIRECT b1) -> [mk_byte_from_bits ((true,false,false,true),(false,true,false,true)); b1] | `SUBB (`A, `INDIRECT i1) -> [mk_byte_from_bits ((true,false,false,true),(false,true,true,i1))] | `SUBB (`A, `DATA b1) -> [mk_byte_from_bits ((true,false,false,true),(false,true,false,false)); b1] | `SWAP `A -> [mk_byte_from_bits ((true,true,false,false),(false,true,false,false))] | `XCH (`A, `REG(r1,r2,r3)) -> [mk_byte_from_bits ((true,true,false,false),(true,r1,r2,r3))] | `XCH (`A, `DIRECT b1) -> [mk_byte_from_bits ((true,true,false,false),(false,true,false,true)); b1] | `XCH (`A, `INDIRECT i1) -> [mk_byte_from_bits ((true,true,false,false),(false,true,true,i1))] | `XCHD(`A, `INDIRECT i1) -> [mk_byte_from_bits ((true,true,false,true),(false,true,true,i1))] | `XRL(`U1(`A, `REG(r1,r2,r3))) -> [mk_byte_from_bits ((false,true,true,false),(true,r1,r2,r3))] | `XRL(`U1(`A, `DIRECT b1)) -> [mk_byte_from_bits ((false,true,true,false),(false,true,false,true)); b1] | `XRL(`U1(`A, `INDIRECT i1)) -> [mk_byte_from_bits ((false,true,true,false),(false,true,true,i1))] | `XRL(`U1(`A, `DATA b1)) -> [mk_byte_from_bits ((false,true,true,false),(false,true,false,false)); b1] | `XRL(`U2(`DIRECT b1, `A)) -> [mk_byte_from_bits ((false,true,true,false),(false,false,true,false)); b1] | `XRL(`U2(`DIRECT b1, `DATA b2)) -> [mk_byte_from_bits ((false,true,true,false),(false,false,true,true)); b1; b2] ;; let load_code_memory = MiscPottier.foldi (fun i mem v -> Physical.WordMap.add (vect_of_int i `Sixteen) v mem) Physical.WordMap.empty let load_mem mem status = { status with code_memory = mem } let load l = load_mem (load_code_memory l) let assembly_jump addr_of = function `JC a1 -> `JC (addr_of a1) | `JNC a1 -> `JNC (addr_of a1) | `JB (a1,a2) -> `JB (a1,addr_of a2) | `JNB (a1,a2) -> `JNB (a1,addr_of a2) | `JBC (a1,a2) -> `JBC (a1,addr_of a2) | `JZ a1 -> `JZ (addr_of a1) | `JNZ a1 -> `JNZ (addr_of a1) | `CJNE (a1,a2) -> `CJNE (a1,addr_of a2) | `DJNZ (a1,a2) -> `DJNZ (a1,addr_of a2) ;; let assembly p = let datalabels,_ = List.fold_left (fun (datalabels,addr) (name,size) -> let addr16 = vect_of_int addr `Sixteen in StringTools.Map.add name addr16 datalabels, addr+size ) (StringTools.Map.empty,0) p.ASM.ppreamble in let pc,exit_addr,labels,costs = List.fold_left (fun (pc,exit_addr,labels,costs) i -> match i with `Label s when s = p.ASM.pexit_label -> pc, pc, StringTools.Map.add s pc labels, costs | `Label s -> pc, exit_addr, StringTools.Map.add s pc labels, costs | `Cost s -> pc, exit_addr, labels, BitVectors.WordMap.add pc s costs | `Mov (_,_) -> (snd (half_add pc (vect_of_int 3 `Sixteen))), exit_addr, labels, costs | `Jmp _ | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), exit_addr, labels, costs (*CSC: very stupid: always expand to worst opcode *) | `WithLabel i -> let fake_addr _ = `REL (zero `Eight) in let fake_jump = assembly_jump fake_addr i in let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in assert (fake_jump = i'); let pc' = snd (half_add pc' (vect_of_int 5 `Sixteen)) in (snd (half_add pc pc'), exit_addr, labels, costs) | #instruction as i -> let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in assert (i = i'); (snd (half_add pc pc'),exit_addr,labels, costs) ) (BitVectors.zero `Sixteen,BitVectors.zero `Sixteen, StringTools.Map.empty, BitVectors.WordMap.empty) p.ASM.pcode in let code = List.flatten (List.map (function `Label _ | `Cost _ -> [] | `WithLabel i -> (* We need to expand a conditional jump to a label to a machine language conditional jump. Suppose we have: JC label This should be expanded to: JC 2 -- size of a short jump SJMP 3 -- size of a long jump LJMP offset -- offset = position of label in code And, for ever label appearing after the location of the jump in code memory, we must increment by 5, as we added two new instructions. *) let to_ljmp = `REL (vect_of_int 2 `Eight) in (* let offset = 5 in *) let jmp_address, translated_jump = match i with `JC (`Label a) -> let address = StringTools.Map.find a labels in let reconstructed = `JC to_ljmp in address, reconstructed | `JNC (`Label a) -> let address = StringTools.Map.find a labels in let reconstructed = `JNC to_ljmp in address, reconstructed | `JB (b, `Label a) -> let address = StringTools.Map.find a labels in let reconstructed = `JB (b, to_ljmp) in address, reconstructed | `JNB (b, `Label a) -> let address = StringTools.Map.find a labels in let reconstructed = `JNB (b, to_ljmp) in address, reconstructed | `JBC (b, `Label a) -> let address = StringTools.Map.find a labels in let reconstructed = `JBC (b, to_ljmp) in address, reconstructed | `JZ (`Label a) -> let address = StringTools.Map.find a labels in let reconstructed = `JZ (to_ljmp) in address, reconstructed | `JNZ (`Label a) -> let address = StringTools.Map.find a labels in let reconstructed = `JNZ (to_ljmp) in address, reconstructed | `CJNE (args, `Label a) -> let address = StringTools.Map.find a labels in let reconstructed = `CJNE (args, to_ljmp) in address, reconstructed | `DJNZ (args, `Label a) -> let address = StringTools.Map.find a labels in let reconstructed = `DJNZ (args, to_ljmp) in address, reconstructed in let sjmp, jmp = `SJMP (`REL (vect_of_int 3 `Eight)), `LJMP (`ADDR16 jmp_address) in let translation = [ translated_jump; sjmp; jmp ] in List.flatten (List.map assembly1 translation) | `Mov (`DPTR,s) -> (* let addr16 = StringTools.Map.find s datalabels in *) let addrr16 = try StringTools.Map.find s datalabels with Not_found -> StringTools.Map.find s labels in assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16))) | `Jmp s -> let pc_offset = StringTools.Map.find s labels in assembly1 (`LJMP (`ADDR16 pc_offset)) | `Call s -> let pc_offset = StringTools.Map.find s labels in assembly1 (`LCALL (`ADDR16 pc_offset )) | #instruction as i -> assembly1 i) p.ASM.pcode) in { ASM.code = code ; ASM.cost_labels = costs ; ASM.labels = StringTools.Map.empty ; ASM.exit_addr = exit_addr ; ASM.has_main = p.ASM.phas_main } ;; let set_register status v reg = let addr = get_address_of_register status reg in { status with low_internal_ram = Byte7Map.add addr v status.low_internal_ram } ;; let get_arg_8 status from_latch = function `DIRECT addr -> let n0, n1 = from_byte addr in (match from_nibble n0 with (false,r1,r2,r3) -> Byte7Map.find (mk_byte7 r1 r2 r3 n1) status.low_internal_ram | _ -> get_sfr status addr from_latch) | `INDIRECT b -> let (b1, b2) = from_byte (get_register status (false,false,b)) in (match (from_nibble b1, b2) with (false,r1,r2,r3),b2 -> Byte7Map.find (mk_byte7 r1 r2 r3 b2) status.low_internal_ram | (true,r1,r2,r3),b2 -> Byte7Map.find (mk_byte7 r1 r2 r3 b2) status.high_internal_ram) | `REG (b1,b2,b3) -> get_register status (b1,b2,b3) | `A -> status.acc | `B -> status.b | `DATA b -> b | `A_DPTR -> let dpr = mk_word status.dph status.dpl in (* CSC: what is the right behaviour in case of overflow? assert false for now. Try to understand what DEC really does *) let cry,addr = half_add dpr (mk_word (vect_of_int 0 `Eight) status.acc) in Physical.WordMap.find addr status.external_ram | `A_PC -> (* CSC: what is the right behaviour in case of overflow? assert false for now *) let cry,addr = half_add status.pc (mk_word (vect_of_int 0 `Eight) status.acc) in Physical.WordMap.find addr status.external_ram | `EXT_INDIRECT b -> let addr = get_register status (false,false,b) in Physical.WordMap.find (mk_word (zero `Eight) addr) status.external_ram | `EXT_IND_DPTR -> let dpr = mk_word status.dph status.dpl in Physical.WordMap.find dpr status.external_ram ;; let get_arg_16 _status = function `DATA16 w -> w let get_arg_1 status from_latch = function `BIT addr | `NBIT addr as x -> let n1, n2 = from_byte addr in let res = (match from_nibble n1 with (false,r1,r2,r3) -> let addr = (int_of_vect (mk_byte7 r1 r2 r3 n2)) in let addr' = vect_of_int ((addr / 8) + 32) `Seven in get_bit (Byte7Map.find addr' status.low_internal_ram) (addr mod 8) | (true,r1,r2,r3) -> let addr = int_of_vect $ mk_byte7 r1 r2 r3 n2 in let div = addr / 8 in let rem = addr mod 8 in get_bit (get_sfr status (vect_of_int ((div * 8) + 128) `Eight) from_latch) rem) in (match x with `NBIT _ -> not res | _ -> res) | `C -> get_cy_flag status let set_arg_1 status v = function `BIT addr -> let n1, n2 = from_byte addr in (match from_nibble n1 with (false,r1,r2,r3) -> let addr = (int_of_vect (mk_byte7 r1 r2 r3 n2)) in let addr' = vect_of_int ((addr / 8) + 32) `Seven in let n_bit = set_bit (Byte7Map.find addr' status.low_internal_ram) (addr mod 8) v in { status with low_internal_ram = Byte7Map.add addr' n_bit status.low_internal_ram } | (true,r1,r2,r3) -> let addr = int_of_vect $ mk_byte7 r1 r2 r3 n2 in let div = addr / 8 in let rem = addr mod 8 in let addr' = vect_of_int ((div * 8) + 128) `Eight in let sfr = get_sfr status addr' true in (* are we reading from the latch here? *) let sfr' = set_bit sfr rem v in set_sfr status addr' sfr') | `C -> let (n1,n2) = from_byte status.psw in let (_,b2,b3,b4) = from_nibble n1 in { status with psw = (mk_byte (mk_nibble v b2 b3 b4) n2) } let set_arg_8 status v = function `DIRECT addr -> let (b1, b2) = from_byte addr in (match from_nibble b1 with (false,r1,r2,r3) -> { status with low_internal_ram = Byte7Map.add (mk_byte7 r1 r2 r3 b2) v status.low_internal_ram } | _ -> set_sfr status addr v) | `INDIRECT b -> let (b1, b2) = from_byte (get_register status (false,false,b)) in (match (from_nibble b1, b2) with (false,r1,r2,r3),n1 -> { status with low_internal_ram = Byte7Map.add (mk_byte7 r1 r2 r3 n1) v status.low_internal_ram } | (true,r1,r2,r3),n1 -> { status with high_internal_ram = Byte7Map.add (mk_byte7 r1 r2 r3 n1) v status.high_internal_ram }) | `REG (b1,b2,b3) -> set_register status v (b1,b2,b3) | `A -> { status with acc = v } | `B -> { status with b = v } | `EXT_IND_DPTR -> let dpr = mk_word status.dph status.dpl in { status with external_ram = Physical.WordMap.add dpr v status.external_ram } | `EXT_INDIRECT b -> let addr = get_register status (false,false,b) in { status with external_ram = Physical.WordMap.add (mk_word (zero `Eight) addr) v status.external_ram } ;; let set_arg_16 status wrd = function `DPTR -> let (dh, dl) = from_word wrd in { status with dph = dh; dpl = dl } let set_flags status c ac ov = { status with psw = let bu,bl = from_byte status.psw in let (_c,oac,fo,rs1),(rs0,_ov,ud,p) = from_nibble bu, from_nibble bl in let ac = match ac with None -> oac | Some v -> v in mk_byte (mk_nibble c ac fo rs1) (mk_nibble rs0 ov ud p) } ;; let xor b1 b2 = if b1 = true && b2 = true then false else if b1 = false && b2 = false then false else true ;; let read_at_sp status = let n1,n2 = from_byte status.sp in let m,r1,r2,r3 = from_nibble n1 in Byte7Map.find (mk_byte7 r1 r2 r3 n2) (if m then status.low_internal_ram else status.high_internal_ram) ;; let write_at_sp status v = let n1,n2 = from_byte status.sp in match from_nibble n1 with true,r1,r2,r3 -> let memory = Byte7Map.add (mk_byte7 r1 r2 r3 n2) v status.low_internal_ram in { status with low_internal_ram = memory } | false,r1,r2,r3 -> let memory = Byte7Map.add (mk_byte7 r1 r2 r3 n2) v status.high_internal_ram in { status with high_internal_ram = memory } ;; let timer0 status b1 b2 ticks = let b = get_bit status.tcon 4 in (* Timer0 first *) (match b1,b2 with true,true -> (* Archaic 13 bit mode. *) if b then let res,_,_,_ = add8_with_c status.tl0 (vect_of_int ticks `Eight) false in let res = int_of_vect res in if res > 31 then let res = res mod 32 in let res',cy',ov',ac' = add8_with_c status.th0 (vect_of_int 1 `Eight) false in if ov' then let b = set_bit status.tcon 7 true in { status with tcon = b; th0 = res'; tl0 = vect_of_int res `Eight } else { status with th0 = res'; tl0 = vect_of_int res `Eight } else { status with tl0 = vect_of_int res `Eight } else status | false,false -> (* 8 bit split timer mode. *) let status = (if b then let res,cy,ov,ac = add8_with_c status.tl0 (vect_of_int ticks `Eight) false in if ov then let b = set_bit status.tcon 5 true in { status with tcon = b; tl0 = res } else { status with tl0 = res } else status) in if get_bit status.tcon 6 then let res,cy,ov,ac = add8_with_c status.th0 (vect_of_int ticks `Eight) false in if ov then let b = set_bit status.tcon 7 true in { status with tcon = b; th0 = res } else { status with th0 = res } else status | false,true -> (* 16 bit timer mode. *) if b then let res,_,ov,_ = add16_with_c (mk_word status.th0 status.tl0) (vect_of_int ticks `Sixteen) false in if ov then let b = set_bit status.tcon 5 true in let new_th0,new_tl0 = from_word res in { status with tcon = b; th0 = new_th0; tl0 = new_tl0 } else let new_th0,new_tl0 = from_word res in { status with th0 = new_th0; tl0 = new_tl0 } else status | true,false -> (* 8 bit single timer mode. *) if b then let res,_,ov,_ = add8_with_c status.tl0 (vect_of_int ticks `Eight) false in if ov then let b = set_bit status.tcon 5 true in { status with tcon = b; tl0 = status.th0; } else { status with tl0 = res } else status) let timer1 status b3 b4 ticks = let b = get_bit status.tcon 4 in (match b3,b4 with true,true -> (* Archaic 13 bit mode. *) if b then let res,_,_,_ = add8_with_c status.tl1 (vect_of_int ticks `Eight) false in let res = int_of_vect res in if res > 31 then let res = res mod 32 in let res',cy',ov',ac' = add8_with_c status.th1 (vect_of_int 1 `Eight) false in if ov' then let b = set_bit status.tcon 7 true in { status with tcon = b; th1 = res'; tl1 = vect_of_int res `Eight } else { status with th1 = res'; tl0 = vect_of_int res `Eight } else { status with tl1 = vect_of_int res `Eight } else status | false,false -> (* 8 bit split timer mode. *) let status = (if b then let res,cy,ov,ac = add8_with_c status.tl1 (vect_of_int ticks `Eight) false in if ov then let b = set_bit status.tcon 5 true in { status with tcon = b; tl1 = res } else { status with tl1 = res } else status) in if get_bit status.tcon 6 then let res,cy,ov,ac = add8_with_c status.th1 (vect_of_int ticks `Eight) false in if ov then let b = set_bit status.tcon 7 true in { status with tcon = b; th1 = res } else { status with th1 = res } else status | false,true -> (* 16 bit timer mode. *) if b then let res,_,ov,_ = add16_with_c (mk_word status.th0 status.tl1) (vect_of_int ticks `Sixteen) false in if ov then let b = set_bit status.tcon 5 true in let new_th1,new_tl1 = from_word res in { status with tcon = b; th1 = new_th1; tl1 = new_tl1 } else let new_th1,new_tl1 = from_word res in { status with th1 = new_th1; tl1 = new_tl1 } else status | true,false -> (* 8 bit single timer mode. *) if b then let res,_,ov,_ = add8_with_c status.tl1 (vect_of_int ticks `Eight) false in if ov then let b = set_bit status.tcon 5 true in { status with tcon = b; tl1 = status.th1; } else { status with tl1 = res } else status) ;; let timers status ticks = (* DPM: Clock/Timer code follows. *) match bits_of_byte status.tmod with | (g1,c1,b1,b2),(g0,c0,b3,b4) -> let status = (if g0 then if get_bit status.p3 2 then if c0 then if status.previous_p1_val && not $ get_bit status.p3 4 then timer0 status b1 b2 ticks else status else timer0 status b1 b2 ticks else status else timer0 status b1 b2 ticks) in (* Timer 1 follows. *) let status = (if g1 then if get_bit status.p1 3 then if c1 then if status.previous_p3_val && not $ get_bit status.p3 5 then timer1 status b3 b4 ticks else status else timer1 status b3 b4 ticks else status else timer1 status b3 b4 ticks) in (* Timer 2 follows *) let status = (let (tf2,exf2,rclk,tclk),(exen2,tr2,ct2,cp2) = bits_of_byte status.t2con in (* Timer2 is enabled *) if tr2 then (* Counter/interval mode *) if ct2 && not cp2 then let word = mk_word status.th2 status.tl2 in let res,_,ov,_ = add16_with_c word (vect_of_int ticks `Sixteen) false in if ov then let new_th2 = status.rcap2h in let new_tl2 = status.rcap2l in (* Overflow flag not set if either of the following flags are set *) if not rclk && not tclk then let b = set_bit status.t2con 7 true in { status with t2con = b; th2 = new_th2; tl2 = new_tl2 } else { status with th2 = new_th2; tl2 = new_tl2 } else (* Reload also signalled when a 1-0 transition is detected *) if status.previous_p1_val && not $ get_bit status.p1 1 then (* In which case signal reload by setting T2CON.6 *) let b = set_bit status.t2con 6 true in { status with th2 = status.rcap2h; tl2 = status.rcap2l; t2con = b } else let new_th2, new_tl2 = from_word res in { status with th2 = new_th2; tl2 = new_tl2 } (* Capture mode *) else if cp2 && exen2 then (* 1-0 transition detected *) (* DPM: look at this: is the timer still running throughout? *) if status.previous_p1_val && not $ get_bit status.p1 1 then status (* Implement clock here *) else status (* Implement clock here *) else status else status) in status ;; let serial_port_input status in_cont = (* Serial port input *) match in_cont with Some (`In(time, line, epsilon, cont)) when get_bit status.scon 4 -> (let status = (match line with `P1 b -> if status.clock >= time then { status with p1 = b; p1_latch = b; } else status | `P3 b -> if status.clock >= time then { status with p3 = b; p3_latch = b; } else status | `SerialBuff (`Eight b) -> let sm0 = get_bit status.scon 7 in let sm1 = get_bit status.scon 6 in (match (sm0, sm1) with (false, false) -> (* Mode 0: shift register. No delay. *) if status.clock >= time then { status with scon = set_bit status.scon 0 true; io = cont; sbuf = b } else status | (false, true) -> (* Mode 1: 8-bit UART *) (* Explanation: 8 bit asynchronous communication. There's a delay (epsilon) which needs taking care of. If we're trying to communicate at the same time an existing communication is occurring, we assert false (else clause of first if). *) if status.serial_epsilon_in = None && status.serial_v_in = None then if status.clock >= time then (* Waiting for nine bits, multiprocessor communication mode requires nine bits *) if get_bit status.scon 5 then assert false (* really: crash! *) else { status with serial_epsilon_in = Some (epsilon + time); serial_v_in = Some (`Eight b) } else (* Warning about incomplete case analysis here, but safe as we've already tested for None. *) let e = extract status.serial_epsilon_in in let v = extract status.serial_v_in in if status.clock >= e then match v with `Eight v' -> { status with sbuf = v'; serial_v_in = None; serial_epsilon_in = None; scon = set_bit status.scon 0 true; io = cont } | _ -> assert false (* trying to read in 9 bits instead of 8 *) else status else assert false | (true, false) | (true, true) -> assert false (* only got eight bits on the line when in 9 bit mode *)) | `SerialBuff (`Nine (b,b')) -> let sm0 = get_bit status.scon 7 in let sm1 = get_bit status.scon 6 in match(sm0, sm1) with (false, false) | (false, true) -> assert false | (true, false) | (true, true) -> (* Modes 2 and 3: 9-bit UART *) (* Explanation: 9 bit asynchronous communication. There's a delay (epsilon) which needs taking care of. If we're trying to communicate at the same time an existing communication is occurring, we assert false (else claus of first if). *) if status.serial_epsilon_in = None && status.serial_v_in = None then if status.clock >= time then (* waiting for nine bits, multiprocessor communication mode requires nine bits *) if get_bit status.scon 5 then assert false (* really: crash! *) else { status with serial_epsilon_in = Some (epsilon + time); serial_v_in = Some (`Nine (b, b')) } else (* Warning about incomplete case analysis here, but safe as we've already tested for None. *) let e = extract status.serial_epsilon_in in let v = extract status.serial_v_in in if status.clock >= e then match v with `Nine (v, v') -> let scon' = set_bit status.scon 0 true in { status with sbuf = v'; serial_v_in = None; serial_epsilon_in = None; scon = set_bit scon' 2 b; io = cont } | _ -> assert false (* trying to read in 8 bits instead of 9 *) else status else assert false) in { status with io = cont }) | _ -> status ;; let serial_port_output status out_cont = (* Serial port output *) (let status = { status with serial_epsilon_out = Some (status.clock + status.io_epsilon); serial_v_out = Some (`Eight status.sbuf); serial_k_out = Some (snd (out_cont (status.clock + status.io_epsilon) (`SerialBuff (`Eight status.sbuf)))) } in match status.serial_epsilon_out with Some s -> if status.clock >= s then match status.serial_k_out with None -> assert false (* correct? *) | Some k' -> { status with io = k'; scon = set_bit status.scon 1 true; } else status | _ -> assert false) ;; let external_serial_interrupt status esi = (* Interrupt enabled *) if esi then (* If we're already running, then fine (todo: check for *another* interrupt and add to a queue, or something? *) if status.t1i_running then status else (* If we should be running, but aren't... *) if false then assert false else status else status ;; let external0_interrupt status e0i = (* Interrupt enabled *) if e0i then (* If we're already running, then fine (todo: check for *another* interrupt and add to a queue, or something? *) if status.t1i_running then status else (* If we should be running, but aren't... *) if false then assert false else status else status ;; let external1_interrupt status e1i = (* Interrupt enabled *) if e1i then (* If we're already running, then fine (todo: check for *another* interrupt and add to a queue, or something? *) if status.t1i_running then status else (* If we should be running, but aren't... *) if false then assert false else status else status ;; let timer0_interrupt status t0i = (* Interrupt enabled *) if t0i then (* If we're already running, then fine (todo: check for *another* interrupt and add to a queue, or something? *) if status.t1i_running then status else (* If we should be running, but aren't... *) if false then assert false else status else status ;; let timer1_interrupt status t1i = (* Interrupt enabled *) if t1i then (* If we're already running, then fine (todo: check for *another* interrupt and add to a queue, or something? *) if status.t1i_running then status else (* If we should be running, but aren't... *) if false then assert false else status else status ;; let interrupts status = let (ea,_,_,es), (et1,ex1,et0,ex0) = bits_of_byte status.ie in let (_,_,_,ps), (pt1,px1,pt0,px0) = bits_of_byte status.ip in (* DPM: are interrupts enabled? *) if ea then match (ps,pt1,px1,pt0,px0) with _ -> assert false else status ;; let execute1 status = let instr,pc,ticks = fetch status.code_memory status.pc in let status = { status with clock = status.clock + ticks; pc = pc } in let status = (match instr with `ADD (`A,d1) -> let v,c,ac,ov = add8_with_c (get_arg_8 status false `A) (get_arg_8 status false d1) false in set_flags (set_arg_8 status v `A) c (Some ac) ov | `ADDC (`A,d1) -> let v,c,ac,ov = add8_with_c (get_arg_8 status false `A) (get_arg_8 status false d1) (get_cy_flag status) in set_flags (set_arg_8 status v `A) c (Some ac) ov | `SUBB (`A,d1) -> let v,c,ac,ov = subb8_with_c (get_arg_8 status false `A) (get_arg_8 status false d1) (get_cy_flag status) in set_flags (set_arg_8 status v `A) c (Some ac) ov | `INC `DPTR -> let cry, low_order_byte = half_add status.dpl (vect_of_int 1 `Eight) in let cry, high_order_byte = full_add status.dph (vect_of_int 0 `Eight) cry in { status with dpl = low_order_byte; dph = high_order_byte } | `INC ((`A | `REG _ | `DIRECT _ | `INDIRECT _) as d) -> let b = get_arg_8 status true d in let cry, res = half_add b (vect_of_int 1 `Eight) in set_arg_8 status res d | `DEC d -> let b = get_arg_8 status true d in let res,c,ac,ov = subb8_with_c b (vect_of_int 1 `Eight) false in set_arg_8 status res d | `MUL (`A,`B) -> let acc = int_of_vect status.acc in let b = int_of_vect status.b in let prod = acc * b in let ov = prod > 255 in let l = vect_of_int (prod mod 256) `Eight in let h = vect_of_int (prod / 256) `Eight in let status = { status with acc = l ; b = h } in (* DPM: Carry flag is always cleared. *) set_flags status false None ov | `DIV (`A,`B) -> let acc = int_of_vect status.acc in let b = int_of_vect status.b in if b = 0 then (* CSC: ACC and B undefined! We leave them as they are. *) set_flags status false None true else let q = vect_of_int (acc / b) `Eight in let r = vect_of_int (acc mod b) `Eight in let status = { status with acc = q ; b = r } in set_flags status false None false | `DA `A -> let acc_upper_nibble, acc_lower_nibble = from_byte status.acc in if int_of_vect acc_lower_nibble > 9 or get_ac_flag status = true then let acc,cy,_,_ = add8_with_c status.acc (vect_of_int 6 `Eight) false in let acc_upper_nibble, acc_lower_nibble = from_byte acc in if int_of_vect acc_upper_nibble > 9 or cy = true then let cry,acc_upper_nibble = half_add acc_upper_nibble (vect_of_int 6 `Four) in let status = { status with acc = mk_byte acc_upper_nibble acc_lower_nibble } in set_flags status cry (Some (get_ac_flag status)) (get_ov_flag status) else status else status | `ANL (`U1(`A, ag)) -> let and_val = get_arg_8 status true `A -&- get_arg_8 status true ag in set_arg_8 status and_val `A | `ANL (`U2((`DIRECT d), ag)) -> let and_val = get_arg_8 status true (`DIRECT d) -&- get_arg_8 status true ag in set_arg_8 status and_val (`DIRECT d) | `ANL (`U3 (`C, b)) -> let and_val = get_cy_flag status && get_arg_1 status true b in set_flags status and_val None (get_ov_flag status) | `ORL (`U1(`A, ag)) -> let or_val = get_arg_8 status true `A -|- get_arg_8 status true ag in set_arg_8 status or_val `A | `ORL (`U2((`DIRECT d), ag)) -> let or_val = get_arg_8 status true (`DIRECT d) -|- get_arg_8 status true ag in set_arg_8 status or_val (`DIRECT d) | `ORL (`U3 (`C, b)) -> let or_val = get_cy_flag status || get_arg_1 status true b in set_flags status or_val None (get_ov_flag status) | `XRL (`U1(`A, ag)) -> let xor_val = get_arg_8 status true `A -^- get_arg_8 status true ag in set_arg_8 status xor_val `A | `XRL (`U2((`DIRECT d), ag)) -> let xor_val = get_arg_8 status true (`DIRECT d) -^- get_arg_8 status true ag in set_arg_8 status xor_val (`DIRECT d) | `CLR `A -> set_arg_8 status (zero `Eight) `A | `CLR `C -> set_arg_1 status false `C | `CLR ((`BIT _) as a) -> set_arg_1 status false a | `CPL `A -> { status with acc = complement status.acc } | `CPL `C -> set_arg_1 status (not $ get_arg_1 status true `C) `C | `CPL ((`BIT _) as b) -> set_arg_1 status (not $ get_arg_1 status true b) b | `RL `A -> { status with acc = rotate_left status.acc } | `RLC `A -> let old_cy = get_cy_flag status in let n1, n2 = from_byte status.acc in let (b1,b2,b3,b4),(b5,b6,b7,b8) = from_nibble n1, from_nibble n2 in let status = set_arg_1 status b1 `C in { status with acc = mk_byte (mk_nibble b2 b3 b4 b5) (mk_nibble b6 b7 b8 old_cy) } | `RR `A -> { status with acc = rotate_right status.acc } | `RRC `A -> let old_cy = get_cy_flag status in let n1, n2 = from_byte status.acc in let (b1,b2,b3,b4),(b5,b6,b7,b8) = from_nibble n1, from_nibble n2 in let status = set_arg_1 status b8 `C in { status with acc = mk_byte (mk_nibble old_cy b1 b2 b3) (mk_nibble b4 b5 b6 b7) } | `SWAP `A -> let (acc_nibble_upper, acc_nibble_lower) = from_byte status.acc in { status with acc = mk_byte acc_nibble_lower acc_nibble_upper } | `MOV(`U1(b1, b2)) -> set_arg_8 status (get_arg_8 status false b2) b1 | `MOV(`U2(b1, b2)) -> set_arg_8 status (get_arg_8 status false b2) b1 | `MOV(`U3(b1, b2)) -> set_arg_8 status (get_arg_8 status false b2) b1 | `MOV(`U4(b1,b2)) -> set_arg_16 status (get_arg_16 status b2) b1 | `MOV(`U5(b1,b2)) -> set_arg_1 status (get_arg_1 status false b2) b1 | `MOV(`U6(b1,b2)) -> set_arg_1 status (get_arg_1 status false b2) b1 | `MOVC (`A, `A_DPTR) -> let big_acc = mk_word (zero `Eight) status.acc in let dptr = mk_word status.dph status.dpl in let cry, addr = half_add dptr big_acc in let lookup = Physical.WordMap.find addr status.code_memory in { status with acc = lookup } | `MOVC (`A, `A_PC) -> let big_acc = mk_word (zero `Eight) status.acc in (* DPM: Under specified: does the carry from PC incrementation affect the *) (* addition of the PC with the DPTR? At the moment, no. *) let cry,inc_pc = half_add status.pc (vect_of_int 1 `Sixteen) in let status = { status with pc = inc_pc } in let cry,addr = half_add inc_pc big_acc in let lookup = Physical.WordMap.find addr status.code_memory in { status with acc = lookup } (* data transfer *) (* DPM: MOVX currently only implements the *copying* of data! *) | `MOVX (`U1 (a1, a2)) -> set_arg_8 status (get_arg_8 status false a2) a1 | `MOVX (`U2 (a1, a2)) -> set_arg_8 status (get_arg_8 status false a2) a1 | `SETB b -> set_arg_1 status true b | `PUSH a -> (* DPM: What happens if we overflow? *) let cry,new_sp = half_add status.sp (vect_of_int 1 `Eight) in let status = { status with sp = new_sp } in write_at_sp status (get_arg_8 status false a) | `POP (`DIRECT b) -> let contents = read_at_sp status in let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in let status = { status with sp = new_sp } in let status = set_arg_8 status contents (`DIRECT b) in status | `XCH(`A, arg) -> let old_arg = get_arg_8 status false arg in let old_acc = status.acc in let status = set_arg_8 status old_acc arg in { status with acc = old_arg } | `XCHD(`A, i) -> let acc_upper_nibble, acc_lower_nibble = from_byte $ get_arg_8 status false `A in let ind_upper_nibble, ind_lower_nibble = from_byte $ get_arg_8 status false i in let new_acc = mk_byte acc_upper_nibble ind_lower_nibble in let new_reg = mk_byte ind_upper_nibble acc_lower_nibble in let status = { status with acc = new_acc } in set_arg_8 status new_reg i (* program branching *) | `JC (`REL rel) -> if get_cy_flag status then let cry, new_pc = half_add status.pc (sign_extension rel) in { status with pc = new_pc } else status | `JNC (`REL rel) -> if not $ get_cy_flag status then let cry, new_pc = half_add status.pc (sign_extension rel) in { status with pc = new_pc } else status | `JB (b, (`REL rel)) -> if get_arg_1 status false b then let cry, new_pc = half_add status.pc (sign_extension rel) in { status with pc = new_pc } else status | `JNB (b, (`REL rel)) -> if not $ get_arg_1 status false b then let cry, new_pc = half_add status.pc (sign_extension rel) in { status with pc = new_pc } else status | `JBC (b, (`REL rel)) -> let status = set_arg_1 status false b in if get_arg_1 status false b then let cry, new_pc = half_add status.pc (sign_extension rel) in { status with pc = new_pc } else status | `RET -> (* DPM: What happens when we underflow? *) let high_bits = read_at_sp status in let new_sp,cy,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in let status = { status with sp = new_sp } in let low_bits = read_at_sp status in let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) cy in let status = { status with sp = new_sp } in { status with pc = mk_word high_bits low_bits } | `RETI -> let high_bits = read_at_sp status in let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in let status = { status with sp = new_sp } in let low_bits = read_at_sp status in let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in let status = { status with sp = new_sp } in { status with pc = mk_word high_bits low_bits } | `ACALL (`ADDR11 a) -> let cry, new_sp = half_add status.sp (vect_of_int 1 `Eight) in let status = { status with sp = new_sp } in let pc_upper_byte, pc_lower_byte = from_word status.pc in let status = write_at_sp status pc_lower_byte in let cry, new_sp = half_add status.sp (vect_of_int 1 `Eight) in let status = { status with sp = new_sp } in let status = write_at_sp status pc_upper_byte in let addr = addr16_of_addr11 status.pc a in { status with pc = addr } | `LCALL (`ADDR16 addr) -> let cry, new_sp = half_add status.sp (vect_of_int 1 `Eight) in let status = { status with sp = new_sp } in let pc_upper_byte, pc_lower_byte = from_word status.pc in let status = write_at_sp status pc_lower_byte in let cry, new_sp = half_add status.sp (vect_of_int 1 `Eight) in let status = { status with sp = new_sp } in let status = write_at_sp status pc_upper_byte in { status with pc = addr } | `AJMP (`ADDR11 a) -> let addr = addr16_of_addr11 status.pc a in { status with pc = addr } | `LJMP (`ADDR16 a) -> { status with pc = a } | `SJMP (`REL rel) -> let cry, new_pc = half_add status.pc (sign_extension rel) in { status with pc = new_pc } | `JMP `IND_DPTR -> let dptr = mk_word status.dph status.dpl in let big_acc = mk_word (zero `Eight) status.acc in let cry, jmp_addr = half_add big_acc dptr in let cry, new_pc = half_add status.pc jmp_addr in { status with pc = new_pc } | `JZ (`REL rel) -> if status.acc = zero `Eight then let cry, new_pc = half_add status.pc (sign_extension rel) in { status with pc = new_pc } else status | `JNZ (`REL rel) -> if status.acc <> zero `Eight then let cry, new_pc = half_add status.pc (sign_extension rel) in { status with pc = new_pc } else status | `CJNE ((`U1 (`A, ag)), `REL rel) -> let new_carry = status.acc < get_arg_8 status false ag in if get_arg_8 status false ag <> status.acc then let cry, new_pc = half_add status.pc (sign_extension rel) in let status = set_flags status new_carry None (get_ov_flag status) in { status with pc = new_pc; } else set_flags status new_carry None (get_ov_flag status) | `CJNE ((`U2 (ag, `DATA d)), `REL rel) -> let new_carry = get_arg_8 status false ag < d in if get_arg_8 status false ag <> d then let cry, new_pc = half_add status.pc (sign_extension rel) in let status = { status with pc = new_pc } in set_flags status new_carry None (get_ov_flag status) else set_flags status new_carry None (get_ov_flag status) | `DJNZ (ag, (`REL rel)) -> let new_ag,_,_,_ = subb8_with_c (get_arg_8 status true ag) (vect_of_int 1 `Eight) false in let status = set_arg_8 status new_ag ag in if new_ag <> zero `Eight then let cry, new_pc = half_add status.pc (sign_extension rel) in { status with pc = new_pc } else status | `NOP -> status) in let status = timers status ticks in let in_cont, `Out out_cont = status.io in let status = serial_port_input status in_cont in let status = serial_port_output status out_cont in let status = interrupts status in { status with previous_p1_val = get_bit status.p3 4; previous_p3_val = get_bit status.p3 5 } ;; (* OLD output routine: (* Serial port output, part one *) let status = (match status.expected_out_time with `At t when status.clock >= t -> { status with scon = set_bit status.scon 1 true; expected_out_time = `None } | _ -> status) in (if status.expected_out_time = `Now then if get_bit status.scon 7 then let exp_time, new_cont = out_cont status.clock (`SerialBuff (`Nine ((get_bit status.scon 3), status.sbuf))) in { status with expected_out_time = `At exp_time; io = new_cont } else let exp_time, new_cont = out_cont status.clock (`SerialBuff (`Eight status.sbuf)) in { status with expected_out_time = `At exp_time; io = new_cont } else status) in *) let rec execute f s = let cont = try f s; true with Halt -> false in if cont then execute f (execute1 s) else s ;; let load_program p = let st = load p.ASM.code initialize in { st with exit_addr = p.ASM.exit_addr ; cost_labels = p.ASM.cost_labels } let observe_trace trace_ref st = let cost_label = if BitVectors.WordMap.mem st.pc st.cost_labels then [BitVectors.WordMap.find st.pc st.cost_labels] else [] in trace_ref := cost_label @ !trace_ref ; if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st let result st = let dpl = st.dpl in let dpr = st.dph in let addr i = BitVectors.vect_of_int i `Seven in let get_ireg i = Physical.Byte7Map.find (addr i) st.low_internal_ram in let r00 = get_ireg 0 in let r01 = get_ireg 1 in let is = [dpl ; dpr ; r00 ; r01] in let f i = IntValue.Int32.of_int (BitVectors.int_of_vect i) in IntValue.Int32.merge (List.map f is) let interpret debug p = Printf.printf "*** 8051 interpret ***\n%!" ; if p.ASM.has_main then let st = load_program p in let trace = ref [] in let callback = observe_trace trace in let st = execute callback st in let res = result st in if debug then Printf.printf "Result = %s\n%!" (IntValue.Int32.to_string res) ; (res, List.rev !trace) else (IntValue.Int32.zero, []) let size_of_instr instr = let exit_lbl = "exit" in let p = { ASM.ppreamble = [] ; ASM.pexit_label = exit_lbl ; ASM.pcode = [instr ; `Label exit_lbl] ; ASM.phas_main = false } in let p = assembly p in let status = load_program p in let addr_zero = BitVectors.vect_of_int 0 `Sixteen in let (_, size, _) = fetch status.code_memory addr_zero in BitVectors.int_of_vect size let size_of_instrs instrs = let f res instr = res + (size_of_instr instr) in List.fold_left f 0 instrs