source: Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml @ 619

Last change on this file since 619 was 619, checked in by ayache, 9 years ago

Update of D2.2 from Paris.

File size: 76.9 KB
Line 
1open BitVectors;;
2open Physical;;
3open ASM;;
4open IntelHex;;
5open Util;;
6open Parser;;
7
8exception Fetch_exception of string;;
9exception CodeTooLarge;;
10exception Halt;;
11
12type time = int;;
13type line = [ `P1 of byte
14            | `P3 of byte
15            | `SerialBuff of [ `Eight of byte | `Nine of BitVectors.bit * byte ]];;
16
17let string_of_line =
18  function
19  `P1 b ->
20    "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^
21      "P1 OUTPUT: " ^ hex_string_of_vect b ^ "\n" ^
22      "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n"
23    | `P3 b ->
24      "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^
25        "P2 OUTPUT: " ^ hex_string_of_vect b ^ "\n" ^
26        "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n"
27    | `SerialBuff (`Eight b) ->
28      "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^
29        "SERIAL 8b OUTPUT: " ^ string_of_vect b ^ "\n" ^
30        "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n"
31    | `SerialBuff (`Nine (b, b')) ->
32      "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^
33        "SERIAL 9b OUTPUT: " ^
34        (let i = int_of_vect b' in
35         if b then
36           string_of_int (128 + i)
37         else
38           string_of_int i) ^
39        "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n"
40
41(* In:  reception time, line of input, new continuation,
42   Out: transmission time, output line, expected duration until reply,
43        new continuation.
44*)
45
46type epsilon = int
47
48type continuation =
49  [`In of time * line * epsilon * continuation] option *
50    [`Out of (time -> line -> time * continuation)]
51
52let rec debug_continuation =
53  (Some (`In (1, (`SerialBuff (`Eight (vect_of_int 5 `Eight))), 0, debug_continuation))), `Out (
54    fun time line ->
55      (* let _ = prerr_endline <*> string_of_line $ line in *)
56      (time + 1),debug_continuation)
57   
58(* no differentiation between internal and external code memory *)
59type status =
60{
61  (* Memory *)
62  code_memory: Physical.WordMap.map;        (* can be reduced *)
63  low_internal_ram: Byte7Map.map;
64  high_internal_ram: Byte7Map.map;
65  external_ram: Physical.WordMap.map;
66
67  (* Program counter *)
68  pc: word;
69
70  (* SFRs *)
71  sp: byte;
72  dpl: byte;
73  dph: byte;
74  pcon: byte;
75  tcon: byte;
76  tmod: byte;
77  tl0: byte;
78  tl1: byte;
79  th0: byte;
80  th1: byte;
81  p1: byte;
82  scon: byte;
83  sbuf: byte;
84  ie: byte;
85  p3: byte;
86  ip: byte;
87  psw: byte;
88  acc: byte;
89  b: byte;
90  t2con: byte;   (* 8052 only *)
91  rcap2l: byte;  (* 8052 only *)
92  rcap2h: byte;  (* 8052 only *)
93  tl2: byte;     (* 8052 only *)
94  th2: byte;     (* 8052 only *)
95
96  (* Latches for the output lines *)
97  p1_latch: byte;
98  p3_latch: byte;
99
100  (* Fields for tracking the state of the processor. *)
101 
102  (* IO specific *)
103  previous_p1_val: bool;
104  previous_p3_val: bool;
105
106  serial_epsilon_out: epsilon option;
107  serial_epsilon_in: epsilon option;
108
109  io_epsilon: epsilon;
110
111  serial_v_in: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option;
112  serial_v_out: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option;
113
114  serial_k_out: continuation option;
115
116  io: continuation;
117  expected_out_time: [ `None | `Now | `At of time ];
118
119  (* Timer and clock specific *)
120  clock: time;
121  timer0: word;
122  timer1: word;
123  timer2: word;  (* can be missing *)
124
125  esi_running: bool;
126  t0i_running: bool;
127  t1i_running: bool;
128  e0i_running: bool;
129  e1i_running: bool;
130  es_running: bool;
131
132  exit_addr   : BitVectors.word;
133  cost_labels : string BitVectors.WordMap.t
134}
135
136(* Try to understand what DEC really does!!! *)
137(* Try to understand I/O *)
138let get_sfr status addr from_latch =
139  match int_of_vect addr with
140    (* I/O and timer ports *)
141      0x80 -> assert false (* P0 not modeled *)
142    | 0x90 ->
143      if from_latch then
144        status.p1_latch
145      else status.p1
146    | 0xA0 -> assert false (* P2 not modeled *)
147    | 0xB0 ->
148      if from_latch then
149        status.p3_latch
150      else status.p3
151    | 0x99 -> status.sbuf
152    | 0x8A -> status.tl0
153    | 0x8B -> status.tl1
154    | 0x8C -> status.th0
155    | 0x8D -> status.th1
156    | 0xC8 -> status.t2con
157    | 0xCA -> status.rcap2l
158    | 0xCB -> status.rcap2h
159    | 0xCC -> status.tl2
160    | 0xCD -> status.th2
161
162  (* control ports *)
163    | 0x87 -> status.pcon
164    | 0x88 -> status.tcon
165    | 0x89 -> status.tmod
166    | 0x98 -> status.scon
167    | 0xA8 -> status.ie
168    | 0xB8 -> status.ip
169     
170  (* registers *)
171    | 0x81 -> status.sp
172    | 0x82 -> status.dpl
173    | 0x83 -> status.dph
174    | 0xD0 -> status.psw
175    | 0xE0 -> status.acc
176    | 0xF0 -> status.b
177    | _ -> assert false
178;;
179
180(* Try to understand I/O *)
181let set_sfr status addr v =
182  match int_of_vect addr with
183    (* I/O and timer ports *)
184      0x80 -> assert false (* P0 not modeled *)
185    | 0x90 -> { status with p1 = v; p1_latch = v }
186    | 0xA0 -> assert false (* P2 not modeled *)
187    | 0xB0 -> { status with p3 = v; p3_latch = v }
188    | 0x99 ->
189      if status.expected_out_time = `None then
190        { status with sbuf = v; expected_out_time = `Now }
191      else
192        (* a real assert false: trying to initiate a transmission whilst one is still active *)
193        assert false
194    | 0x8A -> { status with tl0 = v }
195    | 0x8B -> { status with tl1 = v }
196    | 0x8C -> { status with th0 = v }
197    | 0x8D -> { status with th1 = v }
198    | 0xC8 -> { status with t2con = v }
199    | 0xCA -> { status with rcap2l = v }
200    | 0xCB -> { status with rcap2h = v }
201    | 0xCD -> { status with tl2 = v }
202    | 0xCE -> { status with th2 = v }
203
204    (* control ports *)
205    | 0x87 -> { status with pcon = v }
206    | 0x88 -> { status with tcon = v }
207    | 0x89 -> { status with tmod = v }
208    | 0x98 -> { status with scon = v }
209    | 0xA8 -> { status with ie = v }
210    | 0xB8 -> { status with ip = v }
211     
212    (* registers *)
213    | 0x81 -> { status with sp = v }
214    | 0x82 -> { status with dpl = v }
215    | 0x83 -> { status with dph = v }
216    | 0xD0 -> { status with psw = v }
217    | 0xE0 -> { status with acc = v }
218    | 0xF0 -> { status with b = v }
219    | _ -> assert false
220;;
221
222let initialize = {
223  code_memory = Physical.WordMap.empty;
224  low_internal_ram = Byte7Map.empty;
225  high_internal_ram = Byte7Map.empty;
226  external_ram = Physical.WordMap.empty;
227 
228  pc = zero `Sixteen;
229 
230  sp = vect_of_int 7 `Eight;
231  dpl = zero `Eight;
232  dph = zero `Eight;
233  pcon = zero `Eight;
234  tcon = zero `Eight;
235  tmod = zero `Eight;
236  tl0 = zero `Eight;
237  tl1 = zero `Eight;
238  th0 = zero `Eight;
239  th1 = zero `Eight;
240  p1 = zero `Eight;
241  p1_latch = zero `Eight;
242  scon = zero `Eight;
243  sbuf = zero `Eight;
244  ie = zero `Eight;
245  p3 = zero `Eight;
246  p3_latch = zero `Eight;
247  ip = zero `Eight;
248  psw = zero `Eight;
249  acc = zero `Eight;
250  b = zero `Eight;
251  t2con = zero `Eight;
252  rcap2l = zero `Eight;
253  rcap2h = zero `Eight;
254  tl2 = zero `Eight;
255  th2 = zero `Eight;
256
257  previous_p1_val = false;
258  previous_p3_val = false;
259
260  serial_v_in = None;
261  serial_v_out = None;
262  serial_epsilon_in = None;
263  serial_epsilon_out = None;
264  serial_k_out = None;
265
266  io_epsilon = 5;
267
268  clock = 0;
269  timer0 = zero `Sixteen;
270  timer1 = zero `Sixteen;
271  timer2 = zero `Sixteen;
272
273  expected_out_time = `None;
274
275  io = debug_continuation; (* a real assert false: unprepared for i/o *)
276
277  (* Initially no interrupts are executing *)
278  esi_running = false;
279  t0i_running = false;
280  t1i_running = false;
281  e0i_running = false;
282  e1i_running = false;
283  es_running = false;
284
285  exit_addr = BitVectors.zero `Sixteen;
286  cost_labels = BitVectors.WordMap.empty
287}
288
289let get_cy_flag status =
290  let (cy,_,_,_),(_,_,_,_) = bits_of_byte status.psw in cy
291let get_ac_flag status =
292  let (_,ac,_,_),(_,_,_,_) = bits_of_byte status.psw in ac
293let get_fo_flag status =
294  let (_,_,fo,_),(_,_,_,_) = bits_of_byte status.psw in fo
295let get_rs1_flag status =
296  let (_,_,_,rs1),(_,_,_,_) = bits_of_byte status.psw in rs1
297let get_rs0_flag status =
298  let (_,_,_,_),(rs0,_,_,_) = bits_of_byte status.psw in rs0
299let get_ov_flag status =
300  let (_,_,_,_),(_,ov,_,_) = bits_of_byte status.psw in ov
301let get_ud_flag status =
302  let (_,_,_,_),(_,_,ud,_) = bits_of_byte status.psw in ud
303let get_p_flag status =
304  let (_,_,_,_),(_,_,_,p) = bits_of_byte status.psw in p
305
306let get_address_of_register status (b1,b2,b3) =
307  let bu,_bl = from_byte status.psw in
308  let (_,_,rs1,rs0) = from_nibble bu in
309  let base =
310    match rs1,rs0 with
311        false,false -> 0x00
312      | false,true  -> 0x08
313      | true,false  -> 0x10
314      | true,true   -> 0x18
315  in
316  vect_of_int (base + int_of_vect (mk_nibble false b1 b2 b3)) `Seven
317;;
318
319let get_register status reg =
320  let addr = get_address_of_register status reg in
321  Byte7Map.find addr status.low_internal_ram
322;;
323
324let string_of_status status =   
325  let acc_str = (string_of_int <*> int_of_vect $ status.acc) ^ " (" ^ string_of_vect status.acc ^ ")" in
326  let b_str   = (string_of_int <*> int_of_vect $ status.b) ^ " (" ^ string_of_vect status.b ^ ")" in
327  let psw_str = (string_of_int <*> int_of_vect $ status.psw) ^ " (" ^ string_of_vect status.psw ^ ")" in
328  let sp_str  = (string_of_int <*> int_of_vect $ status.sp) ^ " (" ^ string_of_vect status.sp ^ ")" in
329  let ip_str  = (string_of_int <*> int_of_vect $ status.ip) ^ " (" ^ string_of_vect status.ip ^ ")" in
330  let pc_str  = (string_of_int <*> int_of_vect $ status.pc) ^ " (" ^ string_of_vect status.pc ^ ")" in
331  let dpl_str = (string_of_int <*> int_of_vect $ status.dpl) ^ " (" ^ string_of_vect status.dpl ^ ")" in
332  let dph_str = (string_of_int <*> int_of_vect $ status.dph) ^ " (" ^ string_of_vect status.dph ^ ")" in
333  let scn_str = (string_of_int <*> int_of_vect $ status.scon) ^ " (" ^ string_of_vect status.scon ^ ")" in
334  let sbf_str = (string_of_int <*> int_of_vect $ status.sbuf) ^ " (" ^ string_of_vect status.sbuf ^ ")" in
335  let tcn_str = (string_of_int <*> int_of_vect $ status.tcon) ^ " (" ^ string_of_vect status.tcon ^ ")" in
336  let tmd_str = (string_of_int <*> int_of_vect $ status.tmod) ^ " (" ^ string_of_vect status.tmod ^ ")" in
337  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
338  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
339  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
340  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
341  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
342  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
343  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
344  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
345    "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^
346    " Processor status:                               \n" ^
347    "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^
348    "   ACC : " ^ acc_str ^ "\n"                          ^
349    "   B   : " ^ b_str   ^ "\n"                          ^
350    "   PSW : " ^ psw_str ^ "\n"                          ^
351    "    with flags set as                            \n" ^
352    "     CY  : " ^ (string_of_bool <*> get_cy_flag $ status) ^ "\n" ^
353    "     AC  : " ^ (string_of_bool <*> get_ac_flag $ status) ^ "\n" ^
354    "     FO  : " ^ (string_of_bool <*> get_fo_flag $ status) ^ "\n" ^
355    "     RS1 : " ^ (string_of_bool <*> get_rs1_flag $ status) ^ "\n" ^
356    "     RS0 : " ^ (string_of_bool <*> get_rs0_flag $ status) ^ "\n" ^
357    "     OV  : " ^ (string_of_bool <*> get_ov_flag $ status) ^ "\n" ^
358    "     UD  : " ^ (string_of_bool <*> get_ud_flag $ status) ^ "\n" ^
359    "     P   : " ^ (string_of_bool <*> get_p_flag $ status) ^ "\n" ^
360    "   SP  : " ^ sp_str  ^ "\n"                          ^
361    "   IP  : " ^ ip_str  ^ "\n"                          ^
362    "   PC  : " ^ pc_str  ^ "\n"                          ^
363    "   DPL : " ^ dpl_str ^ "\n"                          ^
364    "   DPH : " ^ dph_str ^ "\n"                          ^
365    "   SCON: " ^ scn_str ^ "\n"                          ^
366    "   SBUF: " ^ sbf_str ^ "\n"                          ^
367    "   TMOD: " ^ tmd_str ^ "\n"                          ^
368    "   TCON: " ^ tcn_str ^ "\n"                          ^
369    "   Registers:                                    \n" ^
370    "    R0 : " ^ r0_str  ^ "\n"                          ^
371    "    R1 : " ^ r1_str  ^ "\n"                          ^
372    "    R2 : " ^ r2_str  ^ "\n"                          ^
373    "    R3 : " ^ r3_str  ^ "\n"                          ^
374    "    R4 : " ^ r4_str  ^ "\n"                          ^
375    "    R5 : " ^ r5_str  ^ "\n"                          ^
376    "    R6 : " ^ r6_str  ^ "\n"                          ^
377    "    R7 : " ^ r7_str  ^ "\n"                          ^
378    "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n"
379
380(* timings taken from SIEMENS *)
381
382let fetch pmem pc =
383  let next pc =
384    let _carry, res = half_add pc (vect_of_int 1 `Sixteen) in
385    res, Physical.WordMap.find pc pmem
386  in
387  let pc,instr = next pc in
388  let un, ln = from_byte instr in
389  let bits = (from_nibble un, from_nibble ln) in
390  match bits with
391      (a10,a9,a8,true),(false,false,false,true) ->
392        let pc,b1 = next pc in
393        `ACALL (`ADDR11 (mk_word11 a10 a9 a8 b1)), pc, 2
394    | (false,false,true,false),(true,r1,r2,r3) ->
395      `ADD (`A,`REG (r1,r2,r3)), pc, 1
396    | (false,false,true,false),(false,true,false,true) ->
397      let pc,b1 = next pc in
398      `ADD (`A,`DIRECT b1), pc, 1
399    | (false,false,true,false),(false,true,true,i1) ->
400      `ADD (`A,`INDIRECT i1), pc, 1
401    | (false,false,true,false),(false,true,false,false) ->
402      let pc,b1 = next pc in
403      `ADD (`A,`DATA b1), pc, 1
404    | (false,false,true,true),(true,r1,r2,r3) ->
405      `ADDC (`A,`REG (r1,r2,r3)), pc, 1
406    | (false,false,true,true),(false,true,false,true) ->
407      let pc,b1 = next pc in
408      `ADDC (`A,`DIRECT b1), pc, 1
409    | (false,false,true,true),(false,true,true,i1) ->
410      `ADDC (`A,`INDIRECT i1), pc, 1
411    | (false,false,true,true),(false,true,false,false) ->
412      let pc,b1 = next pc in
413      `ADDC (`A,`DATA b1), pc, 1
414    | (a10,a9,a8,false),(false,false,false,true) ->
415      let pc,b1 = next pc in
416      `AJMP (`ADDR11 (mk_word11 a10 a9 a8 b1)), pc, 2
417    | (false,true,false,true),(true,r1,r2,r3) ->
418      `ANL (`U1 (`A, `REG (r1,r2,r3))), pc, 1
419    | (false,true,false,true),(false,true,false,true) ->
420      let pc,b1 = next pc in
421      `ANL (`U1 (`A, `DIRECT b1)), pc, 1
422    | (false,true,false,true),(false,true,true,i1) ->
423      `ANL (`U1 (`A, `INDIRECT i1)), pc, 1
424    | (false,true,false,true),(false,true,false,false) ->
425      let pc,b1 = next pc in
426      `ANL (`U1 (`A, `DATA b1)), pc, 1
427    | (false,true,false,true),(false,false,true,false) ->
428      let pc,b1 = next pc in
429      `ANL (`U2 (`DIRECT b1,`A)), pc, 1
430    | (false,true,false,true),(false,false,true,true) ->
431      let pc,b1 = next pc in
432      let pc,b2 = next pc in
433      `ANL (`U2 (`DIRECT b1,`DATA b2)), pc, 2
434    | (true,false,false,false),(false,false,true,false) ->
435      let pc,b1 = next pc in
436      `ANL (`U3 (`C,`BIT b1)), pc, 2
437    | (true,false,true,true),(false,false,false,false) ->
438      let pc,b1 = next pc in
439      `ANL (`U3 (`C,`NBIT b1)), pc, 2
440    | (true,false,true,true),(false,true,false,true) ->
441      let pc,b1 = next pc in
442      let pc,b2 = next pc in
443      `CJNE (`U1 (`A, `DIRECT b1), `REL b2), pc, 2
444    | (true,false,true,true),(false,true,false,false) ->
445      let pc,b1 = next pc in
446      let pc,b2 = next pc in
447      `CJNE (`U1 (`A, `DATA b1), `REL b2), pc, 2
448    | (true,false,true,true),(true,r1,r2,r3) ->
449      let pc,b1 = next pc in
450      let pc,b2 = next pc in
451      `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2), pc, 2
452    | (true,false,true,true),(false,true,true,i1) ->
453      let pc,b1 = next pc in
454      let pc,b2 = next pc in
455      `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2), pc, 2
456    | (true,true,true,false),(false,true,false,false) ->
457      `CLR `A, pc, 1
458    | (true,true,false,false),(false,false,true,true) ->
459      `CLR `C, pc, 1
460    | (true,true,false,false),(false,false,true,false) ->
461      let pc,b1 = next pc in
462      `CLR (`BIT b1), pc, 1
463    | (true,true,true,true),(false,true,false,false) ->
464      `CPL `A, pc, 1
465    | (true,false,true,true),(false,false,true,true) ->
466      `CPL `C, pc, 1
467    | (true,false,true,true),(false,false,true,false) ->
468      let pc,b1 = next pc in
469      `CPL (`BIT b1), pc, 1
470    | (true,true,false,true),(false,true,false,false) ->
471      `DA `A, pc, 1
472    | (false,false,false,true),(false,true,false,false) ->
473      `DEC `A, pc, 1
474    | (false,false,false,true),(true,r1,r2,r3) ->
475      `DEC (`REG(r1,r2,r3)), pc, 1
476    | (false,false,false,true),(false,true,false,true) ->
477      let pc,b1 = next pc in
478      `DEC (`DIRECT b1), pc, 1
479    | (false,false,false,true),(false,true,true,i1) ->
480      `DEC (`INDIRECT i1), pc, 1
481    | (true,false,false,false),(false,true,false,false) ->
482      `DIV (`A, `B), pc, 4
483    | (true,true,false,true),(true,r1,r2,r3) ->
484      let pc,b1 = next pc in
485      `DJNZ (`REG(r1,r2,r3), `REL b1), pc, 2
486    | (true,true,false,true),(false,true,false,true) ->
487      let pc,b1 = next pc in
488      let pc,b2 = next pc in
489      `DJNZ (`DIRECT b1, `REL b2), pc, 2
490    | (false,false,false,false),(false,true,false,false) ->
491      `INC `A, pc, 1
492    | (false,false,false,false),(true,r1,r2,r3) ->
493      `INC (`REG(r1,r2,r3)), pc, 1
494    | (false,false,false,false),(false,true,false,true) ->
495      let pc,b1 = next pc in
496      `INC (`DIRECT b1), pc, 1
497    | (false,false,false,false),(false,true,true,i1) ->
498      `INC (`INDIRECT i1), pc, 1
499    | (true,false,true,false),(false,false,true,true) ->
500      `INC `DPTR, pc, 2
501    | (false,false,true,false),(false,false,false,false) ->
502      let pc,b1 = next pc in
503      let pc,b2 = next pc in
504      `JB (`BIT b1, `REL b2), pc, 2
505    | (false,false,false,true),(false,false,false,false) ->
506      let pc,b1 = next pc in
507      let pc,b2 = next pc in
508      `JBC (`BIT b1, `REL b2), pc, 2
509    | (false,true,false,false),(false,false,false,false) ->
510      let pc,b1 = next pc in
511      `JC (`REL b1), pc, 2
512    | (false,true,true,true),(false,false,true,true) ->
513      `JMP `IND_DPTR, pc, 2
514    | (false,false,true,true),(false,false,false,false) ->
515      let pc,b1 = next pc in
516      let pc,b2 = next pc in
517      `JNB (`BIT b1, `REL b2), pc, 2
518    | (false,true,false,true),(false,false,false,false) ->
519      let pc,b1 = next pc in
520      `JNC (`REL b1), pc, 2
521    | (false,true,true,true),(false,false,false,false) ->
522      let pc,b1 = next pc in
523      `JNZ (`REL b1), pc, 2
524    | (false,true,true,false),(false,false,false,false) ->
525      let pc,b1 = next pc in
526      `JZ (`REL b1), pc, 2
527    | (false,false,false,true),(false,false,true,false) ->
528      let pc,b1 = next pc in
529      let pc,b2 = next pc in
530      `LCALL (`ADDR16 (mk_word b1 b2)), pc, 2
531    | (false,false,false,false),(false,false,true,false) ->
532      let pc,b1 = next pc in
533      let pc,b2 = next pc in
534      `LJMP (`ADDR16 (mk_word b1 b2)), pc, 2
535   | (true,true,true,false),(true,r1,r2,r3) ->
536         `MOV (`U1 (`A, `REG(r1,r2,r3))), pc, 1
537   | (true,true,true,false),(false,true,false,true) ->
538       let pc,b1 = next pc in
539         `MOV (`U1 (`A, `DIRECT b1)), pc, 1
540   | (true,true,true,false),(false,true,true,i1) ->
541         `MOV (`U1 (`A, `INDIRECT i1)), pc, 1
542   | (false,true,true,true),(false,true,false,false) ->
543       let pc,b1 = next pc in
544         `MOV (`U1 (`A, `DATA b1)), pc, 1
545   | (true,true,true,true),(true,r1,r2,r3) ->
546         `MOV (`U2 (`REG(r1,r2,r3), `A)), pc, 1
547   | (true,false,true,false),(true,r1,r2,r3) ->
548       let pc,b1 = next pc in
549         `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))), pc, 2
550   | (false,true,true,true),(true,r1,r2,r3) ->
551       let pc,b1 = next pc in
552         `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))), pc, 1
553   | (true,true,true,true),(false,true,false,true) ->
554       let pc,b1 = next pc in
555         `MOV (`U3 (`DIRECT b1, `A)), pc, 1
556   | (true,false,false,false),(true,r1,r2,r3) ->
557       let pc,b1 = next pc in
558         `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))), pc, 2
559   | (true,false,false,false),(false,true,false,true) ->
560       let pc,b1 = next pc in
561       let pc,b2 = next pc in
562         `MOV (`U3 (`DIRECT b1, `DIRECT b2)), pc, 2
563   | (true,false,false,false),(false,true,true,i1) ->
564       let pc,b1 = next pc in
565         `MOV (`U3 (`DIRECT b1, `INDIRECT i1)), pc, 2
566   | (false,true,true,true),(false,true,false,true) ->
567       let pc,b1 = next pc in
568       let pc,b2 = next pc in
569         `MOV (`U3 (`DIRECT b1, `DATA b2)), pc, 3
570   | (true,true,true,true),(false,true,true,i1) ->
571         `MOV (`U2 (`INDIRECT i1, `A)), pc, 1
572   | (true,false,true,false),(false,true,true,i1) ->
573       let pc,b1 = next pc in
574         `MOV (`U2 (`INDIRECT i1, `DIRECT b1)), pc, 2
575   | (false,true,true,true),(false,true,true,i1) ->
576       let pc,b1 = next pc in
577         `MOV (`U2 (`INDIRECT i1, `DATA b1)), pc, 1
578   | (true,false,true,false),(false,false,true,false) ->
579       let pc,b1 = next pc in
580         `MOV (`U5 (`C, `BIT b1)), pc, 1
581   | (true,false,false,true),(false,false,true,false) ->
582       let pc,b1 = next pc in
583         `MOV (`U6 (`BIT b1, `C)), pc, 2
584   | (true,false,false,true),(false,false,false,false) ->
585       let pc,b1 = next pc in
586       let pc,b2 = next pc in
587         `MOV (`U4 (`DPTR, `DATA16(mk_word b1 b2))), pc, 2
588   | (true,false,false,true),(false,false,true,true) ->
589         `MOVC (`A, `A_DPTR), pc, 2
590   | (true,false,false,false),(false,false,true,true) ->
591         `MOVC (`A, `A_PC), pc, 2
592   | (true,true,true,false),(false,false,true,i1) ->
593         `MOVX (`U1 (`A, `EXT_INDIRECT i1)), pc, 2
594   | (true,true,true,false),(false,false,false,false) ->
595         `MOVX (`U1 (`A, `EXT_IND_DPTR)), pc, 2
596   | (true,true,true,true),(false,false,true,i1) ->
597         `MOVX (`U2 (`EXT_INDIRECT i1, `A)), pc, 2
598   | (true,true,true,true),(false,false,false,false) ->
599         `MOVX (`U2 (`EXT_IND_DPTR, `A)), pc, 2
600   | (true,false,true,false),(false,true,false,false) ->
601         `MUL(`A, `B), pc, 4
602   | (false,false,false,false),(false,false,false,false) ->
603         `NOP, pc, 1
604   | (false,true,false,false),(true,r1,r2,r3) ->
605         `ORL (`U1(`A, `REG(r1,r2,r3))), pc, 1
606   | (false,true,false,false),(false,true,false,true) ->
607       let pc,b1 = next pc in
608         `ORL (`U1(`A, `DIRECT b1)), pc, 1
609   | (false,true,false,false),(false,true,true,i1) ->
610         `ORL (`U1(`A, `INDIRECT i1)), pc, 1
611   | (false,true,false,false),(false,true,false,false) ->
612       let pc,b1 = next pc in
613         `ORL (`U1(`A, `DATA b1)), pc, 1
614   | (false,true,false,false),(false,false,true,false) ->
615       let pc,b1 = next pc in
616         `ORL (`U2(`DIRECT b1, `A)), pc, 1
617   | (false,true,false,false),(false,false,true,true) ->
618       let pc,b1 = next pc in
619       let pc,b2 = next pc in
620         `ORL (`U2 (`DIRECT b1, `DATA b2)), pc, 2
621   | (false,true,true,true),(false,false,true,false) ->
622       let pc,b1 = next pc in
623         `ORL (`U3 (`C, `BIT b1)), pc, 2
624   | (true,false,true,false),(false,false,false,false) ->
625       let pc,b1 = next pc in
626         `ORL (`U3 (`C, `NBIT b1)), pc, 2
627   | (true,true,false,true),(false,false,false,false) ->
628       let pc,b1 = next pc in
629         `POP (`DIRECT b1), pc, 2
630   | (true,true,false,false),(false,false,false,false) ->
631       let pc,b1 = next pc in
632         `PUSH (`DIRECT b1), pc, 2
633   | (false,false,true,false),(false,false,true,false) ->
634         `RET, pc, 2
635   | (false,false,true,true),(false,false,true,false) ->
636         `RETI, pc, 2
637   | (false,false,true,false),(false,false,true,true) ->
638         `RL `A, pc, 1
639   | (false,false,true,true),(false,false,true,true) ->
640         `RLC `A, pc, 1
641   | (false,false,false,false),(false,false,true,true) ->
642         `RR `A, pc, 1
643   | (false,false,false,true),(false,false,true,true) ->
644         `RRC `A, pc, 1
645   | (true,true,false,true),(false,false,true,true) ->
646         `SETB `C, pc, 1
647   | (true,true,false,true),(false,false,true,false) ->
648       let pc,b1 = next pc in
649         `SETB (`BIT b1), pc, 1
650   | (true,false,false,false),(false,false,false,false) ->
651       let pc,b1 = next pc in
652         `SJMP (`REL b1), pc, 2
653   | (true,false,false,true),(true,r1,r2,r3) ->
654       `SUBB (`A, `REG(r1,r2,r3)), pc, 1
655   | (true,false,false,true),(false,true,false,true) ->
656       let pc,b1 = next pc in
657         `SUBB (`A, `DIRECT b1), pc, 1
658   | (true,false,false,true),(false,true,true,i1) ->
659         `SUBB (`A, `INDIRECT i1), pc, 1
660   | (true,false,false,true),(false,true,false,false) ->
661       let pc,b1 = next pc in
662         `SUBB (`A, `DATA b1), pc, 1
663   | (true,true,false,false),(false,true,false,false) ->
664         `SWAP `A, pc, 1
665   | (true,true,false,false),(true,r1,r2,r3) ->
666         `XCH (`A, `REG(r1,r2,r3)), pc, 1
667   | (true,true,false,false),(false,true,false,true) ->
668       let pc,b1 = next pc in
669         `XCH (`A, `DIRECT b1), pc, 1
670   | (true,true,false,false),(false,true,true,i1) ->
671         `XCH (`A, `INDIRECT i1), pc, 1
672   | (true,true,false,true),(false,true,true,i1) ->
673         `XCHD(`A, `INDIRECT i1), pc, 1
674   | (false,true,true,false),(true,r1,r2,r3) ->
675         `XRL(`U1(`A, `REG(r1,r2,r3))), pc, 1
676   | (false,true,true,false),(false,true,false,true) ->
677       let pc,b1 = next pc in
678         `XRL(`U1(`A, `DIRECT b1)), pc, 1
679   | (false,true,true,false),(false,true,true,i1) ->
680         `XRL(`U1(`A, `INDIRECT i1)), pc, 1
681   | (false,true,true,false),(false,true,false,false) ->
682       let pc,b1 = next pc in
683         `XRL(`U1(`A, `DATA b1)), pc, 1
684   | (false,true,true,false),(false,false,true,false) ->
685       let pc,b1 = next pc in
686         `XRL(`U2(`DIRECT b1, `A)), pc, 1
687   | (false,true,true,false),(false,false,true,true) ->
688       let pc,b1 = next pc in
689       let pc,b2 = next pc in
690         `XRL(`U2(`DIRECT b1, `DATA b2)), pc, 2
691   | (true,false,true,false),(false,true,false,true) ->
692       (* undefined opcode *) assert false
693;;
694
695let assembly1 =
696 function
697    `ACALL (`ADDR11 w) ->
698      let (a10,a9,a8,b1) = from_word11 w in
699        [mk_byte_from_bits ((a10,a9,a8,true),(false,false,false,true)); b1]
700  | `ADD (`A,`REG (r1,r2,r3)) ->
701     [mk_byte_from_bits ((false,false,true,false),(true,r1,r2,r3))]
702  | `ADD (`A, `DIRECT b1) ->
703     [mk_byte_from_bits ((false,false,true,false),(false,true,false,true)); b1]
704  | `ADD (`A, `INDIRECT i1) ->
705     [mk_byte_from_bits ((false,false,true,false),(false,true,true,i1))]
706  | `ADD (`A, `DATA b1) ->
707     [mk_byte_from_bits ((false,false,true,false),(false,true,false,false)); b1]
708  | `ADDC (`A, `REG(r1,r2,r3)) ->
709     [mk_byte_from_bits ((false,false,true,true),(true,r1,r2,r3))]
710  | `ADDC (`A, `DIRECT b1) ->
711     [mk_byte_from_bits ((false,false,true,true),(false,true,false,true)); b1]
712  | `ADDC (`A,`INDIRECT i1) ->
713     [mk_byte_from_bits ((false,false,true,true),(false,true,true,i1))]
714  | `ADDC (`A,`DATA b1) ->
715     [mk_byte_from_bits ((false,false,true,true),(false,true,false,false)); b1]
716  | `AJMP (`ADDR11 w) ->
717     let (a10,a9,a8,b1) = from_word11 w in
718       [mk_byte_from_bits ((a10,a9,a8,false),(false,false,false,true)); b1]
719  | `ANL (`U1 (`A, `REG (r1,r2,r3))) ->
720     [mk_byte_from_bits ((false,true,false,true),(true,r1,r2,r3))]
721  | `ANL (`U1 (`A, `DIRECT b1)) ->
722     [mk_byte_from_bits ((false,true,false,true),(false,true,false,true)); b1]
723  | `ANL (`U1 (`A, `INDIRECT i1)) ->
724     [mk_byte_from_bits ((false,true,false,true),(false,true,true,i1))]
725  | `ANL (`U1 (`A, `DATA b1)) ->
726     [mk_byte_from_bits ((false,true,false,true),(false,true,false,false)); b1]
727  | `ANL (`U2 (`DIRECT b1,`A)) ->
728     [mk_byte_from_bits ((false,true,false,true),(false,false,true,false)); b1]
729  | `ANL (`U2 (`DIRECT b1,`DATA b2)) ->
730     [mk_byte_from_bits ((false,true,false,true),(false,false,true,true)); b1; b2]
731  | `ANL (`U3 (`C,`BIT b1)) ->
732     [mk_byte_from_bits ((true,false,false,false),(false,false,true,false)); b1]
733  | `ANL (`U3 (`C,`NBIT b1)) ->
734    [mk_byte_from_bits ((true,false,true,true),(false,false,false,false)); b1]
735  | `CJNE (`U1 (`A, `DIRECT b1), `REL b2) ->
736    [mk_byte_from_bits ((true,false,true,true),(false,true,false,true)); b1; b2]
737  | `CJNE (`U1 (`A, `DATA b1), `REL b2) ->
738    [mk_byte_from_bits ((true,false,true,true),(false,true,false,false)); b1; b2]
739  | `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2) ->
740    [mk_byte_from_bits ((true,false,true,true),(true,r1,r2,r3)); b1; b2]
741  | `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) ->
742    [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2]
743  | `CLR `A ->
744    [mk_byte_from_bits ((true,true,true,false),(false,true,false,false))]
745  | `CLR `C ->
746    [mk_byte_from_bits ((true,true,false,false),(false,false,true,true))]
747  | `CLR (`BIT b1) ->
748    [mk_byte_from_bits ((true,true,false,false),(false,false,true,false)); b1]
749  | `CPL `A ->
750    [mk_byte_from_bits ((true,true,true,true),(false,true,false,false))]
751  | `CPL `C ->
752    [mk_byte_from_bits ((true,false,true,true),(false,false,true,true))]
753  | `CPL (`BIT b1) ->
754    [mk_byte_from_bits ((true,false,true,true),(false,false,true,false)); b1]
755  | `DA `A ->
756    [mk_byte_from_bits ((true,true,false,true),(false,true,false,false))]
757  | `DEC `A ->
758    [mk_byte_from_bits ((false,false,false,true),(false,true,false,false))]
759  | `DEC (`REG(r1,r2,r3)) ->
760    [mk_byte_from_bits ((false,false,false,true),(true,r1,r2,r3))]
761  | `DEC (`DIRECT b1) ->
762    [mk_byte_from_bits ((false,false,false,true),(false,true,false,true)); b1]
763  | `DEC (`INDIRECT i1) ->
764    [mk_byte_from_bits ((false,false,false,true),(false,true,true,i1))]
765  | `DIV (`A, `B) ->
766    [mk_byte_from_bits ((true,false,false,false),(false,true,false,false))]
767  | `DJNZ (`REG(r1,r2,r3), `REL b1) ->
768    [mk_byte_from_bits ((true,true,false,true),(true,r1,r2,r3)); b1]
769  | `DJNZ (`DIRECT b1, `REL b2) ->
770    [mk_byte_from_bits ((true,true,false,true),(false,true,false,true)); b1; b2]
771  | `INC `A ->
772    [mk_byte_from_bits ((false,false,false,false),(false,true,false,false))]
773  | `INC (`REG(r1,r2,r3)) ->
774    [mk_byte_from_bits ((false,false,false,false),(true,r1,r2,r3))]
775  | `INC (`DIRECT b1) ->
776    [mk_byte_from_bits ((false,false,false,false),(false,true,false,true)); b1]
777  | `INC (`INDIRECT i1) ->
778    [mk_byte_from_bits ((false,false,false,false),(false,true,true,i1))]
779  | `INC `DPTR ->
780    [mk_byte_from_bits ((true,false,true,false),(false,false,true,true))]
781  | `JB (`BIT b1, `REL b2) ->
782    [mk_byte_from_bits ((false,false,true,false),(false,false,false,false)); b1; b2]
783  | `JBC (`BIT b1, `REL b2) ->
784    [mk_byte_from_bits ((false,false,false,true),(false,false,false,false)); b1; b2]
785  | `JC (`REL b1) ->
786    [mk_byte_from_bits ((false,true,false,false),(false,false,false,false)); b1]
787  | `JMP `IND_DPTR ->
788    [mk_byte_from_bits ((false,true,true,true),(false,false,true,true))]
789  | `JNB (`BIT b1, `REL b2) ->
790    [mk_byte_from_bits ((false,false,true,true),(false,false,false,false)); b1; b2]
791  | `JNC (`REL b1) ->
792    [mk_byte_from_bits ((false,true,false,true),(false,false,false,false)); b1]
793  | `JNZ (`REL b1) ->
794    [mk_byte_from_bits ((false,true,true,true),(false,false,false,false)); b1]
795  | `JZ (`REL b1) ->
796    [mk_byte_from_bits ((false,true,true,false),(false,false,false,false)); b1]
797  | `LCALL (`ADDR16 w) ->
798      let (b1,b2) = from_word w in
799        [mk_byte_from_bits ((false,false,false,true),(false,false,true,false)); b1; b2]
800  | `LJMP (`ADDR16 w) ->
801      let (b1,b2) = from_word w in
802        [mk_byte_from_bits ((false,false,false,false),(false,false,true,false)); b1; b2]
803  | `MOV (`U1 (`A, `REG(r1,r2,r3))) ->
804    [mk_byte_from_bits ((true,true,true,false),(true,r1,r2,r3))]
805  | `MOV (`U1 (`A, `DIRECT b1)) ->
806    [mk_byte_from_bits ((true,true,true,false),(false,true,false,true)); b1]
807  | `MOV (`U1 (`A, `INDIRECT i1)) ->
808    [mk_byte_from_bits ((true,true,true,false),(false,true,true,i1))]
809  | `MOV (`U1 (`A, `DATA b1)) ->
810    [mk_byte_from_bits ((false,true,true,true),(false,true,false,false)); b1]
811  | `MOV (`U2 (`REG(r1,r2,r3), `A)) ->
812    [mk_byte_from_bits ((true,true,true,true),(true,r1,r2,r3))]
813  | `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))) ->
814    [mk_byte_from_bits ((true,false,true,false),(true,r1,r2,r3)); b1]
815  | `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))) ->
816    [mk_byte_from_bits ((false,true,true,true),(true,r1,r2,r3)); b1]
817  | `MOV (`U3 (`DIRECT b1, `A)) ->
818    [mk_byte_from_bits ((true,true,true,true),(false,true,false,true)); b1]
819  | `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))) ->
820    [mk_byte_from_bits ((true,false,false,false),(true,r1,r2,r3)); b1]
821  | `MOV (`U3 (`DIRECT b1, `DIRECT b2)) ->
822    [mk_byte_from_bits ((true,false,false,false),(false,true,false,true)); b1; b2]
823  | `MOV (`U3 (`DIRECT b1, `INDIRECT i1)) ->
824    [mk_byte_from_bits ((true,false,false,false),(false,true,true,i1)); b1]
825  | `MOV (`U3 (`DIRECT b1, `DATA b2)) ->
826    [mk_byte_from_bits ((false,true,true,true),(false,true,false,true)); b1; b2]
827  | `MOV (`U2 (`INDIRECT i1, `A)) ->
828    [mk_byte_from_bits ((true,true,true,true),(false,true,true,i1))]
829  | `MOV (`U2 (`INDIRECT i1, `DIRECT b1)) ->
830    [mk_byte_from_bits ((true,false,true,false),(false,true,true,i1)); b1]
831  | `MOV (`U2 (`INDIRECT i1, `DATA b1)) ->
832    [mk_byte_from_bits ((false,true,true,true),(false,true,true,i1)); b1]
833  | `MOV (`U5 (`C, `BIT b1)) ->
834    [mk_byte_from_bits ((true,false,true,false),(false,false,true,false)); b1]
835  | `MOV (`U6 (`BIT b1, `C)) ->
836    [mk_byte_from_bits ((true,false,false,true),(false,false,true,false)); b1]
837  | `MOV (`U4 (`DPTR, `DATA16 w)) ->
838    let (b1,b2) = from_word w in
839      [mk_byte_from_bits ((true,false,false,true),(false,false,false,false)); b1; b2]
840  | `MOVC (`A, `A_DPTR) ->
841    [mk_byte_from_bits ((true,false,false,true),(false,false,true,true))]
842  | `MOVC (`A, `A_PC) ->
843    [mk_byte_from_bits ((true,false,false,false),(false,false,true,true))]
844  | `MOVX (`U1 (`A, `EXT_INDIRECT i1)) ->
845    [mk_byte_from_bits ((true,true,true,false),(false,false,true,i1))]
846  | `MOVX (`U1 (`A, `EXT_IND_DPTR)) ->
847    [mk_byte_from_bits ((true,true,true,false),(false,false,false,false))]
848  | `MOVX (`U2 (`EXT_INDIRECT i1, `A)) ->
849    [mk_byte_from_bits ((true,true,true,true),(false,false,true,i1))]
850  | `MOVX (`U2 (`EXT_IND_DPTR, `A)) ->
851    [mk_byte_from_bits ((true,true,true,true),(false,false,false,false))]
852  | `MUL(`A, `B) ->
853    [mk_byte_from_bits ((true,false,true,false),(false,true,false,false))]
854  | `NOP ->
855    [mk_byte_from_bits ((false,false,false,false),(false,false,false,false))]
856  | `ORL (`U1(`A, `REG(r1,r2,r3))) ->
857    [mk_byte_from_bits ((false,true,false,false),(true,r1,r2,r3))]
858  | `ORL (`U1(`A, `DIRECT b1)) ->
859    [mk_byte_from_bits ((false,true,false,false),(false,true,false,true)); b1]
860  | `ORL (`U1(`A, `INDIRECT i1)) ->
861    [mk_byte_from_bits ((false,true,false,false),(false,true,true,i1))]
862  | `ORL (`U1(`A, `DATA b1)) ->
863    [mk_byte_from_bits ((false,true,false,false),(false,true,false,false)); b1]
864  | `ORL (`U2(`DIRECT b1, `A)) ->
865    [mk_byte_from_bits ((false,true,false,false),(false,false,true,false)); b1]
866  | `ORL (`U2 (`DIRECT b1, `DATA b2)) ->
867    [mk_byte_from_bits ((false,true,false,false),(false,false,true,true)); b1; b2]
868  | `ORL (`U3 (`C, `BIT b1)) ->
869    [mk_byte_from_bits ((false,true,true,true),(false,false,true,false)); b1]
870  | `ORL (`U3 (`C, `NBIT b1)) ->
871    [mk_byte_from_bits ((true,false,true,false),(false,false,false,false)); b1]
872  | `POP (`DIRECT b1) ->
873    [mk_byte_from_bits ((true,true,false,true),(false,false,false,false)); b1]
874  | `PUSH (`DIRECT b1) ->
875    [mk_byte_from_bits ((true,true,false,false),(false,false,false,false)); b1]
876  | `RET ->
877    [mk_byte_from_bits ((false,false,true,false),(false,false,true,false))]
878  | `RETI ->
879    [mk_byte_from_bits ((false,false,true,true),(false,false,true,false))]
880  | `RL `A ->
881    [mk_byte_from_bits ((false,false,true,false),(false,false,true,true))]
882  | `RLC `A ->
883    [mk_byte_from_bits ((false,false,true,true),(false,false,true,true))]
884  | `RR `A ->
885    [mk_byte_from_bits ((false,false,false,false),(false,false,true,true))]
886  | `RRC `A ->
887    [mk_byte_from_bits ((false,false,false,true),(false,false,true,true))]
888  | `SETB `C ->
889    [mk_byte_from_bits ((true,true,false,true),(false,false,true,true))]
890  | `SETB (`BIT b1) ->
891    [mk_byte_from_bits ((true,true,false,true),(false,false,true,false)); b1]
892  | `SJMP (`REL b1) ->
893    [mk_byte_from_bits ((true,false,false,false),(false,false,false,false)); b1]
894  | `SUBB (`A, `REG(r1,r2,r3)) ->
895    [mk_byte_from_bits ((true,false,false,true),(true,r1,r2,r3))]
896  | `SUBB (`A, `DIRECT b1) ->
897    [mk_byte_from_bits ((true,false,false,true),(false,true,false,true)); b1]
898  | `SUBB (`A, `INDIRECT i1) ->
899    [mk_byte_from_bits ((true,false,false,true),(false,true,true,i1))]
900  | `SUBB (`A, `DATA b1) ->
901    [mk_byte_from_bits ((true,false,false,true),(false,true,false,false)); b1]
902  | `SWAP `A ->
903    [mk_byte_from_bits ((true,true,false,false),(false,true,false,false))]
904  | `XCH (`A, `REG(r1,r2,r3)) ->
905    [mk_byte_from_bits ((true,true,false,false),(true,r1,r2,r3))]
906  | `XCH (`A, `DIRECT b1) ->
907    [mk_byte_from_bits ((true,true,false,false),(false,true,false,true)); b1]
908  | `XCH (`A, `INDIRECT i1) ->
909    [mk_byte_from_bits ((true,true,false,false),(false,true,true,i1))]
910  | `XCHD(`A, `INDIRECT i1) ->
911    [mk_byte_from_bits ((true,true,false,true),(false,true,true,i1))]
912  | `XRL(`U1(`A, `REG(r1,r2,r3))) ->
913    [mk_byte_from_bits ((false,true,true,false),(true,r1,r2,r3))]
914  | `XRL(`U1(`A, `DIRECT b1)) ->
915    [mk_byte_from_bits ((false,true,true,false),(false,true,false,true)); b1]
916  | `XRL(`U1(`A, `INDIRECT i1)) ->
917    [mk_byte_from_bits ((false,true,true,false),(false,true,true,i1))]
918  | `XRL(`U1(`A, `DATA b1)) ->
919    [mk_byte_from_bits ((false,true,true,false),(false,true,false,false)); b1]
920  | `XRL(`U2(`DIRECT b1, `A)) ->
921    [mk_byte_from_bits ((false,true,true,false),(false,false,true,false)); b1]
922  | `XRL(`U2(`DIRECT b1, `DATA b2)) ->
923    [mk_byte_from_bits ((false,true,true,false),(false,false,true,true)); b1; b2]
924;;
925
926let load_code_memory = MiscPottier.foldi (fun i mem v -> Physical.WordMap.add (vect_of_int i `Sixteen) v mem) Physical.WordMap.empty
927
928let load_mem mem status = { status with code_memory = mem }
929let load l = load_mem (load_code_memory l)
930
931let assembly_jump addr_of =
932 function
933    `JC a1 -> `JC (addr_of a1)
934  | `JNC a1 -> `JNC (addr_of a1)
935  | `JB (a1,a2) -> `JB (a1,addr_of a2)
936  | `JNB (a1,a2) -> `JNB (a1,addr_of a2)
937  | `JBC (a1,a2) -> `JBC (a1,addr_of a2)
938  | `JZ a1 -> `JZ (addr_of a1)
939  | `JNZ a1 -> `JNZ (addr_of a1)
940  | `CJNE (a1,a2) -> `CJNE (a1,addr_of a2)
941  | `DJNZ (a1,a2) -> `DJNZ (a1,addr_of a2)
942;;
943
944let assembly p =
945 let datalabels,_ =
946  List.fold_left
947   (fun (datalabels,addr) (name,size) ->
948     let addr16 = vect_of_int addr `Sixteen in
949      StringTools.Map.add name addr16 datalabels, addr+size
950   ) (StringTools.Map.empty,0) p.ASM.ppreamble
951 in
952 let pc,exit_addr,labels,costs =
953  List.fold_left
954   (fun (pc,exit_addr,labels,costs) i ->
955     match i with
956        `Label s when s = p.ASM.pexit_label ->
957          pc, pc, StringTools.Map.add s pc labels, costs
958      | `Label s ->
959          pc, exit_addr, StringTools.Map.add s pc labels, costs
960      | `Cost s -> pc, exit_addr, labels, BitVectors.WordMap.add pc s costs
961      | `Mov (_,_) -> pc, exit_addr, labels, costs
962      | `Jmp _ 
963      | `Call _ ->
964        (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))),
965        exit_addr, labels, costs
966      (*CSC: very stupid: always expand to worst opcode *)
967      | `WithLabel i ->
968        let fake_addr _ = `REL (zero `Eight) in
969        let fake_jump = assembly_jump fake_addr i in
970        let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in
971        assert (fake_jump = i');
972        (snd (half_add pc pc'), exit_addr, labels, costs)
973      | #instruction as i ->
974        let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in
975         assert (i = i');
976         (snd (half_add pc pc'),exit_addr,labels, costs)
977   )
978    (BitVectors.zero `Sixteen,BitVectors.zero `Sixteen,
979     StringTools.Map.empty, BitVectors.WordMap.empty) p.ASM.pcode
980 in
981 let code =
982  List.flatten (List.map
983     (function
984        `Label _
985      | `Cost _ -> []
986      | `WithLabel i ->
987          let addr_of (`Label s) =
988           let addr = StringTools.Map.find s labels in
989            (* NOT IMPLEMENTED YET; NEEDS SMART ALGORITHM *)
990            `REL (assert false) (*addr*)
991          in
992           assembly1 (assembly_jump addr_of i)
993      | `Mov (`DPTR,s) ->
994          let addrr16 = StringTools.Map.find s datalabels in
995           assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16)))
996      | `Jmp s ->
997          let pc_offset = StringTools.Map.find s labels in
998            assembly1 (`LJMP (`ADDR16 pc_offset))
999      | `Call s ->
1000          let pc_offset = StringTools.Map.find s labels in
1001            assembly1 (`LCALL (`ADDR16 pc_offset ))
1002      | #instruction as i -> assembly1 i) p.ASM.pcode) in
1003 { ASM.code = code ; ASM.cost_labels = costs ;
1004   ASM.exit_addr = exit_addr ; ASM.has_main = p.ASM.phas_main }
1005;;
1006
1007let set_register status v reg =
1008  let addr = get_address_of_register status reg in
1009    { status with low_internal_ram =
1010        Byte7Map.add addr v status.low_internal_ram }
1011;;
1012
1013let get_arg_8 status from_latch = 
1014 function
1015    `DIRECT addr ->
1016       let n0, n1 = from_byte addr in
1017       (match from_nibble n0 with
1018          (false,r1,r2,r3) ->
1019            Byte7Map.find (mk_byte7 r1 r2 r3 n1) status.low_internal_ram
1020        | _ -> get_sfr status addr from_latch)
1021  | `INDIRECT b ->
1022       let (b1, b2) = from_byte (get_register status (false,false,b)) in
1023         (match (from_nibble b1, b2) with 
1024           (false,r1,r2,r3),b2 ->
1025             Byte7Map.find (mk_byte7 r1 r2 r3 b2) status.low_internal_ram
1026         | (true,r1,r2,r3),b2 ->
1027             Byte7Map.find (mk_byte7 r1 r2 r3 b2) status.high_internal_ram)
1028  | `REG (b1,b2,b3) -> get_register status (b1,b2,b3)
1029  | `A -> status.acc
1030  | `B -> status.b
1031  | `DATA b -> b
1032  | `A_DPTR ->
1033       let dpr = mk_word status.dph status.dpl in
1034       (* CSC: what is the right behaviour in case of overflow?
1035          assert false for now. Try to understand what DEC really does *)
1036       let cry,addr = half_add dpr (mk_word (vect_of_int 0 `Eight) status.acc) in
1037         Physical.WordMap.find addr status.external_ram
1038  | `A_PC ->
1039       (* CSC: what is the right behaviour in case of overflow?
1040          assert false for now *)
1041       let cry,addr = half_add status.pc (mk_word (vect_of_int 0 `Eight) status.acc) in
1042         Physical.WordMap.find addr status.external_ram
1043  | `EXT_INDIRECT b ->
1044         let addr = get_register status (false,false,b) in
1045           Physical.WordMap.find (mk_word (zero `Eight) addr) status.external_ram
1046  | `EXT_IND_DPTR ->
1047       let dpr = mk_word status.dph status.dpl in
1048         Physical.WordMap.find dpr status.external_ram
1049;;
1050
1051let get_arg_16 _status = function `DATA16 w -> w
1052
1053let get_arg_1 status from_latch =
1054  function
1055    `BIT addr
1056  | `NBIT addr as x ->
1057     let n1, n2 = from_byte addr in
1058     let res =
1059      (match from_nibble n1 with
1060         (false,r1,r2,r3) ->
1061           let addr = (int_of_vect (mk_byte7 r1 r2 r3 n2)) in
1062           let addr' = vect_of_int ((addr / 8) + 32) `Seven in
1063             get_bit (Byte7Map.find addr' status.low_internal_ram) (addr mod 8)
1064        | (true,r1,r2,r3) ->
1065            let addr = int_of_vect $ mk_byte7 r1 r2 r3 n2 in
1066            let div = addr / 8 in
1067            let rem = addr mod 8 in
1068              get_bit (get_sfr status (vect_of_int ((div * 8) + 128) `Eight) from_latch) rem)
1069    in (match x with `NBIT _ -> not res | _ -> res)
1070  | `C -> get_cy_flag status
1071
1072let set_arg_1 status v =
1073  function
1074    `BIT addr ->
1075      let n1, n2 = from_byte addr in
1076      (match from_nibble n1 with
1077         (false,r1,r2,r3) ->
1078           let addr = (int_of_vect (mk_byte7 r1 r2 r3 n2)) in
1079           let addr' = vect_of_int ((addr / 8) + 32) `Seven in
1080           let n_bit = set_bit (Byte7Map.find addr' status.low_internal_ram) (addr mod 8) v in
1081             { status with low_internal_ram = Byte7Map.add addr' n_bit status.low_internal_ram }
1082      | (true,r1,r2,r3) ->
1083            let addr = int_of_vect $ mk_byte7 r1 r2 r3 n2 in
1084            let div = addr / 8 in
1085            let rem = addr mod 8 in
1086            let addr' = vect_of_int ((div * 8) + 128) `Eight in
1087            let sfr = get_sfr status addr' true in (* are we reading from the latch here? *)
1088            let sfr' = set_bit sfr rem v in
1089              set_sfr status addr' sfr')
1090    | `C ->
1091       let (n1,n2) = from_byte status.psw in
1092       let (_,b2,b3,b4) = from_nibble n1 in
1093         { status with psw = (mk_byte (mk_nibble v b2 b3 b4) n2) }
1094
1095let set_arg_8 status v =
1096  function
1097  `DIRECT addr ->
1098    let (b1, b2) = from_byte addr in
1099    (match from_nibble b1 with
1100        (false,r1,r2,r3) ->
1101          { status with low_internal_ram =
1102              Byte7Map.add (mk_byte7 r1 r2 r3 b2) v status.low_internal_ram }
1103      | _ -> set_sfr status addr v)
1104    | `INDIRECT b ->
1105      let (b1, b2) = from_byte (get_register status (false,false,b)) in
1106      (match (from_nibble b1, b2) with 
1107          (false,r1,r2,r3),n1 ->
1108            { status with low_internal_ram =
1109                Byte7Map.add (mk_byte7 r1 r2 r3 n1) v status.low_internal_ram }
1110        | (true,r1,r2,r3),n1 ->
1111          { status with high_internal_ram =
1112              Byte7Map.add (mk_byte7 r1 r2 r3 n1) v status.high_internal_ram })
1113    | `REG (b1,b2,b3) ->
1114      set_register status v (b1,b2,b3)
1115    | `A -> { status with acc = v }
1116    | `B -> { status with b = v }
1117    | `EXT_IND_DPTR ->
1118      let dpr = mk_word status.dph status.dpl in
1119      { status with external_ram =
1120          Physical.WordMap.add dpr v status.external_ram }
1121    | `EXT_INDIRECT b ->
1122      let addr = get_register status (false,false,b) in
1123      { status with external_ram =
1124          Physical.WordMap.add (mk_word (zero `Eight) addr) v status.external_ram }
1125;;
1126
1127let set_arg_16 status wrd =
1128  function
1129  `DPTR ->
1130    let (dh, dl) = from_word wrd in
1131    { status with dph = dh; dpl = dl }
1132     
1133let set_flags status c ac ov =
1134  { status with psw =
1135      let bu,bl = from_byte status.psw in
1136      let (_c,oac,fo,rs1),(rs0,_ov,ud,p) = from_nibble bu, from_nibble bl in
1137      let ac = match ac with None -> oac | Some v -> v in
1138      mk_byte (mk_nibble c ac fo rs1) (mk_nibble rs0 ov ud p)
1139  }
1140;;
1141
1142let xor b1 b2 =
1143  if b1 = true && b2 = true then
1144    false
1145  else if b1 = false && b2 = false then
1146    false
1147  else true
1148;;
1149
1150let read_at_sp status =
1151  let n1,n2 = from_byte status.sp in
1152  let m,r1,r2,r3 = from_nibble n1 in
1153  Byte7Map.find (mk_byte7 r1 r2 r3 n2)
1154    (if m then status.low_internal_ram else status.high_internal_ram)
1155;;
1156
1157let write_at_sp status v =
1158  let n1,n2 = from_byte status.sp in
1159  match from_nibble n1 with
1160      true,r1,r2,r3 ->
1161        let memory =
1162          Byte7Map.add (mk_byte7 r1 r2 r3 n2) v status.low_internal_ram
1163        in
1164        { status with low_internal_ram = memory }
1165    | false,r1,r2,r3 ->
1166      let memory =
1167        Byte7Map.add (mk_byte7 r1 r2 r3 n2) v status.high_internal_ram
1168      in
1169      { status with high_internal_ram = memory }
1170;;
1171
1172let timer0 status b1 b2 ticks =
1173  let b = get_bit status.tcon 4 in
1174          (* Timer0 first *)
1175  (match b1,b2 with
1176      true,true ->
1177              (* Archaic 13 bit mode. *)
1178        if b then
1179          let res,_,_,_ = add8_with_c status.tl0 (vect_of_int ticks `Eight) false in
1180          let res = int_of_vect res in
1181          if res > 31 then
1182            let res = res mod 32 in
1183            let res',cy',ov',ac' = add8_with_c status.th0 (vect_of_int 1 `Eight) false in
1184            if ov' then
1185              let b = set_bit status.tcon 7 true in
1186              { status with tcon = b; th0 = res'; tl0 = vect_of_int res `Eight }
1187            else
1188              { status with th0 = res'; tl0 = vect_of_int res `Eight }
1189          else
1190            { status with tl0 = vect_of_int res `Eight }
1191        else
1192          status
1193    | false,false ->
1194              (* 8 bit split timer mode. *)
1195      let status = 
1196        (if b then
1197            let res,cy,ov,ac = add8_with_c status.tl0 (vect_of_int ticks `Eight) false in
1198            if ov then
1199              let b = set_bit status.tcon 5 true in
1200              { status with tcon = b; tl0 = res }
1201            else
1202              { status with tl0 = res }
1203         else
1204            status)
1205      in
1206      if get_bit status.tcon 6 then
1207        let res,cy,ov,ac = add8_with_c status.th0 (vect_of_int ticks `Eight) false in
1208        if ov then
1209          let b = set_bit status.tcon 7 true in
1210          { status with tcon = b; th0 = res }
1211        else
1212          { status with th0 = res }
1213      else
1214        status
1215    | false,true ->
1216             (* 16 bit timer mode. *)
1217      if b then
1218        let res,_,ov,_ = add16_with_c (mk_word status.th0 status.tl0) (vect_of_int ticks `Sixteen) false in
1219                if ov then
1220                  let b = set_bit status.tcon 5 true in
1221                  let new_th0,new_tl0 = from_word res in
1222                  { status with tcon = b; th0 = new_th0; tl0 = new_tl0 }
1223                else
1224                  let new_th0,new_tl0 = from_word res in
1225                  { status with th0 = new_th0; tl0 = new_tl0 }
1226      else
1227        status
1228    | true,false ->
1229              (* 8 bit single timer mode. *)
1230      if b then
1231        let res,_,ov,_ = add8_with_c status.tl0 (vect_of_int ticks `Eight) false in
1232        if ov then
1233          let b = set_bit status.tcon 5 true in
1234          { status with tcon = b; tl0 = status.th0; }
1235        else
1236          { status with tl0 = res }
1237      else
1238        status)
1239   
1240let timer1 status b3 b4 ticks =
1241  let b = get_bit status.tcon 4 in
1242  (match b3,b4 with
1243      true,true ->
1244        (* Archaic 13 bit mode. *)
1245        if b then
1246          let res,_,_,_ = add8_with_c status.tl1 (vect_of_int ticks `Eight) false in
1247          let res = int_of_vect res in
1248          if res > 31 then
1249            let res = res mod 32 in
1250            let res',cy',ov',ac' = add8_with_c status.th1 (vect_of_int 1 `Eight) false in
1251            if ov' then
1252              let b = set_bit status.tcon 7 true in
1253              { status with tcon = b; th1 = res'; tl1 = vect_of_int res `Eight }
1254            else
1255              { status with th1 = res'; tl0 = vect_of_int res `Eight }
1256          else
1257            { status with tl1 = vect_of_int res `Eight }
1258        else
1259          status
1260    | false,false ->
1261              (* 8 bit split timer mode. *)
1262      let status = 
1263        (if b then
1264            let res,cy,ov,ac = add8_with_c status.tl1 (vect_of_int ticks `Eight) false in
1265            if ov then
1266              let b = set_bit status.tcon 5 true in
1267                        { status with tcon = b; tl1 = res }
1268            else
1269              { status with tl1 = res }
1270         else
1271            status)
1272      in
1273      if get_bit status.tcon 6 then
1274        let res,cy,ov,ac = add8_with_c status.th1 (vect_of_int ticks `Eight) false in
1275        if ov then
1276          let b = set_bit status.tcon 7 true in
1277          { status with tcon = b; th1 = res }
1278        else
1279          { status with th1 = res }
1280      else
1281        status
1282    | false,true ->
1283             (* 16 bit timer mode. *)
1284      if b then
1285        let res,_,ov,_ = add16_with_c (mk_word status.th0 status.tl1) (vect_of_int ticks `Sixteen) false in
1286        if ov then
1287          let b = set_bit status.tcon 5 true in
1288          let new_th1,new_tl1 = from_word res in
1289          { status with tcon = b; th1 = new_th1; tl1 = new_tl1 }
1290        else
1291          let new_th1,new_tl1 = from_word res in
1292          { status with th1 = new_th1; tl1 = new_tl1 }
1293      else
1294        status
1295    | true,false ->
1296              (* 8 bit single timer mode. *)
1297      if b then
1298        let res,_,ov,_ = add8_with_c status.tl1 (vect_of_int ticks `Eight) false in
1299        if ov then
1300          let b = set_bit status.tcon 5 true in
1301          { status with tcon = b; tl1 = status.th1; }
1302        else
1303          { status with tl1 = res }
1304      else
1305        status)
1306;;
1307
1308let timers status ticks =
1309  (* DPM: Clock/Timer code follows. *)
1310  match bits_of_byte status.tmod with
1311    | (g1,c1,b1,b2),(g0,c0,b3,b4) ->
1312      let status =
1313        (if g0 then
1314            if get_bit status.p3 2 then
1315              if c0 then
1316                if status.previous_p1_val && not $ get_bit status.p3 4 then
1317                  timer0 status b1 b2 ticks
1318                else
1319                  status
1320              else
1321                timer0 status b1 b2 ticks
1322            else
1323              status
1324         else
1325            timer0 status b1 b2 ticks) in
1326      (* Timer 1 follows. *)
1327      let status =
1328        (if g1 then
1329            if get_bit status.p1 3 then
1330              if c1 then
1331                if status.previous_p3_val && not $ get_bit status.p3 5 then
1332                  timer1 status b3 b4 ticks
1333                else
1334                  status
1335              else
1336                timer1 status b3 b4 ticks
1337            else
1338              status
1339         else
1340            timer1 status b3 b4 ticks) in
1341      (* Timer 2 follows *)
1342      let status =
1343        (let (tf2,exf2,rclk,tclk),(exen2,tr2,ct2,cp2) = bits_of_byte status.t2con in
1344          (* Timer2 is enabled *)
1345         if tr2 then
1346            (* Counter/interval mode *)
1347           if ct2 && not cp2 then
1348             let word = mk_word status.th2 status.tl2 in
1349             let res,_,ov,_ = add16_with_c word (vect_of_int ticks `Sixteen) false in
1350             if ov then
1351               let new_th2 = status.rcap2h in
1352               let new_tl2 = status.rcap2l in
1353                  (* Overflow flag not set if either of the following flags are set *)
1354               if not rclk && not tclk then
1355                 let b = set_bit status.t2con 7 true in
1356                 { status with t2con = b;
1357                   th2 = new_th2;
1358                   tl2 = new_tl2 }
1359               else
1360                 { status with th2 = new_th2;
1361                   tl2 = new_tl2 }
1362             else
1363                (* Reload also signalled when a 1-0 transition is detected *)
1364               if status.previous_p1_val && not $ get_bit status.p1 1 then
1365                  (* In which case signal reload by setting T2CON.6 *)
1366                 let b = set_bit status.t2con 6 true in
1367                 { status with th2 = status.rcap2h;
1368                   tl2 = status.rcap2l;
1369                   t2con = b }
1370               else
1371                 let new_th2, new_tl2 = from_word res in
1372                 { status with th2 = new_th2;
1373                   tl2 = new_tl2 }
1374            (* Capture mode *)
1375           else if cp2 && exen2 then
1376              (* 1-0 transition detected *)
1377              (* DPM: look at this: is the timer still running throughout? *)
1378             if status.previous_p1_val && not $ get_bit status.p1 1 then
1379               status (* Implement clock here *)
1380             else
1381               status (* Implement clock here *)
1382           else
1383             status
1384           else
1385             status) in status
1386                     
1387;;
1388
1389let serial_port_input status in_cont =
1390      (* Serial port input *)
1391  match in_cont with
1392      Some (`In(time, line, epsilon, cont)) when get_bit status.scon 4 ->
1393        (let status =
1394           (match line with
1395               `P1 b ->
1396                 if status.clock >= time then
1397                   { status with p1 = b; p1_latch = b; }
1398                 else
1399                   status
1400             | `P3 b ->
1401               if status.clock >= time then
1402                 { status with p3 = b; p3_latch = b; }
1403               else
1404                 status
1405             | `SerialBuff (`Eight b) ->
1406               let sm0 = get_bit status.scon 7 in
1407               let sm1 = get_bit status.scon 6 in
1408               (match (sm0, sm1) with
1409                   (false, false) ->
1410                       (* Mode 0: shift register.  No delay. *)
1411                     if status.clock >= time then
1412                       { status with scon = set_bit status.scon 0 true;
1413                         io   = cont;
1414                         sbuf = b }
1415                     else
1416                       status
1417                 | (false, true) ->
1418                       (* Mode 1: 8-bit UART *)
1419                       (* Explanation: 8 bit asynchronous communication.  There's a delay (epsilon)
1420                          which needs taking care of.  If we're trying to communicate at the same time
1421                          an existing communication is occurring, we assert false (else clause of first
1422                          if). *)
1423                   if status.serial_epsilon_in = None && status.serial_v_in = None then
1424                     if status.clock >= time then
1425                           (* Waiting for nine bits, multiprocessor communication mode requires nine bits *)
1426                       if get_bit status.scon 5 then
1427                         assert false (* really: crash! *)
1428                       else
1429                         { status with serial_epsilon_in = Some (epsilon + time);
1430                           serial_v_in       = Some (`Eight b) }
1431                     else
1432                           (* Warning about incomplete case analysis here, but safe as we've already tested for
1433                              None. *)
1434                       let Some e = status.serial_epsilon_in in
1435                       let Some v = status.serial_v_in in
1436                       if status.clock >= e then
1437                         match v with
1438                             `Eight v' ->
1439                               { status with sbuf = v';
1440                                 serial_v_in = None;
1441                                 serial_epsilon_in = None;
1442                                 scon = set_bit status.scon 0 true;
1443                                 io = cont }
1444                           | _ -> assert false (* trying to read in 9 bits instead of 8 *)
1445                       else
1446                         status
1447                   else
1448                     assert false
1449                 | (true, false) | (true, true) ->
1450                   assert false (* only got eight bits on the line when in 9 bit mode *))
1451             | `SerialBuff (`Nine (b,b')) ->
1452               let sm0 = get_bit status.scon 7 in
1453               let sm1 = get_bit status.scon 6 in
1454               match(sm0, sm1) with
1455                   (false, false) | (false, true) -> assert false
1456                 | (true, false)  | (true, true) ->
1457                       (* Modes 2 and 3: 9-bit UART *)
1458                       (* Explanation: 9 bit asynchronous communication.  There's a delay (epsilon)
1459                          which needs taking care of.  If we're trying to communicate at the same time
1460                          an existing communication is occurring, we assert false (else claus of first
1461                          if). *)
1462                   if status.serial_epsilon_in = None && status.serial_v_in = None then
1463                     if status.clock >= time then
1464                           (* waiting for nine bits, multiprocessor communication mode requires nine bits *)
1465                       if get_bit status.scon 5 then
1466                         assert false (* really: crash! *)
1467                       else
1468                         { status with serial_epsilon_in = Some (epsilon + time);
1469                           serial_v_in       = Some (`Nine (b, b')) }
1470                     else
1471                           (* Warning about incomplete case analysis here, but safe as we've already tested for
1472                              None. *)
1473                       let Some e = status.serial_epsilon_in in
1474                       let Some v = status.serial_v_in in
1475                       if status.clock >= e then
1476                         match v with
1477                             `Nine (v, v') ->
1478                               let scon' = set_bit status.scon 0 true in
1479                               { status with sbuf = v';
1480                                 serial_v_in = None;
1481                                 serial_epsilon_in = None;
1482                                 scon = set_bit scon' 2 b;
1483                                 io = cont }
1484                           | _ -> assert false (* trying to read in 8 bits instead of 9 *)
1485                       else
1486                         status
1487                   else
1488                     assert false)
1489         in
1490         { status with io = cont })
1491    | _ -> status
1492;;
1493
1494let serial_port_output status out_cont =
1495  (* Serial port output *)
1496  (let status = { status with serial_epsilon_out = Some (status.clock + status.io_epsilon);
1497    serial_v_out = Some (`Eight status.sbuf);
1498    serial_k_out = Some (snd (out_cont (status.clock + status.io_epsilon) (`SerialBuff (`Eight status.sbuf)))) } in
1499   match status.serial_epsilon_out with
1500       Some s ->
1501         if status.clock >= s then
1502           match status.serial_k_out with
1503               None -> assert false (* correct? *)
1504             | Some k' -> { status with io   = k';
1505               scon = set_bit status.scon 1 true; }
1506         else
1507           status
1508     | _ -> assert false)
1509;;
1510
1511let external_serial_interrupt status esi =
1512  (* Interrupt enabled *)
1513  if esi then
1514    (* If we're already running, then fine (todo: check for *another* interrupt
1515       and add to a queue, or something? *)
1516    if status.t1i_running then
1517      status
1518    else
1519      (* If we should be running, but aren't... *)
1520      if false then
1521        assert false
1522      else
1523        status
1524  else
1525    status
1526;;
1527
1528let external0_interrupt status e0i =
1529  (* Interrupt enabled *)
1530  if e0i then
1531    (* If we're already running, then fine (todo: check for *another* interrupt
1532       and add to a queue, or something? *)
1533    if status.t1i_running then
1534      status
1535    else
1536      (* If we should be running, but aren't... *)
1537      if false then
1538        assert false
1539      else
1540        status
1541  else
1542    status
1543;;
1544
1545let external1_interrupt status e1i =
1546  (* Interrupt enabled *)
1547  if e1i then
1548    (* If we're already running, then fine (todo: check for *another* interrupt
1549       and add to a queue, or something? *)
1550    if status.t1i_running then
1551      status
1552    else
1553      (* If we should be running, but aren't... *)
1554      if false then
1555        assert false
1556      else
1557        status
1558  else
1559    status
1560;;
1561
1562let timer0_interrupt status t0i =
1563  (* Interrupt enabled *)
1564  if t0i then
1565    (* If we're already running, then fine (todo: check for *another* interrupt
1566       and add to a queue, or something? *)
1567    if status.t1i_running then
1568      status
1569    else
1570      (* If we should be running, but aren't... *)
1571      if false then
1572        assert false
1573      else
1574        status
1575  else
1576    status
1577;;
1578
1579let timer1_interrupt status t1i =
1580  (* Interrupt enabled *)
1581  if t1i then
1582    (* If we're already running, then fine (todo: check for *another* interrupt
1583       and add to a queue, or something? *)
1584    if status.t1i_running then
1585      status
1586    else
1587      (* If we should be running, but aren't... *)
1588      if false then
1589        assert false
1590      else
1591        status
1592  else
1593    status
1594;;
1595
1596let interrupts status =
1597  let (ea,_,_,es), (et1,ex1,et0,ex0) = bits_of_byte status.ie in
1598  let (_,_,_,ps), (pt1,px1,pt0,px0) = bits_of_byte status.ip in
1599    (* DPM: are interrupts enabled? *)
1600  if ea then
1601    match (ps,pt1,px1,pt0,px0) with
1602        _ -> assert false
1603  else
1604    status
1605;;
1606
1607let execute1 status =
1608  let instr,pc,ticks = fetch status.code_memory status.pc in
1609  let status = { status with clock = status.clock + ticks; pc = pc } in
1610  let status =
1611    (match instr with
1612        `ADD (`A,d1) ->
1613          let v,c,ac,ov =
1614            add8_with_c (get_arg_8 status false `A) (get_arg_8 status false d1) false
1615          in
1616          set_flags (set_arg_8 status v `A) c (Some ac) ov
1617      | `ADDC (`A,d1) ->
1618        let v,c,ac,ov =
1619          add8_with_c (get_arg_8 status false `A) (get_arg_8 status false d1) (get_cy_flag status)
1620        in
1621        set_flags (set_arg_8 status v `A) c (Some ac) ov
1622      | `SUBB (`A,d1) ->
1623        let v,c,ac,ov =
1624          subb8_with_c (get_arg_8 status false `A) (get_arg_8 status false d1) (get_cy_flag status)
1625        in
1626        set_flags (set_arg_8 status v `A) c (Some ac) ov
1627      | `INC `DPTR ->
1628        let cry, low_order_byte = half_add status.dpl (vect_of_int 1 `Eight) in
1629        let cry, high_order_byte = full_add status.dph (vect_of_int 0 `Eight) cry in
1630        { status with dpl = low_order_byte; dph = high_order_byte }
1631      | `INC ((`A | `REG _ | `DIRECT _ | `INDIRECT _) as d) ->
1632        let b = get_arg_8 status true d in
1633        let cry, res = half_add b (vect_of_int 1 `Eight) in
1634        set_arg_8 status res d
1635      | `DEC d ->
1636        let b = get_arg_8 status true d in
1637        let res,c,ac,ov = subb8_with_c b (vect_of_int 1 `Eight) false in
1638        set_arg_8 status res d
1639      | `MUL (`A,`B) ->
1640        let acc = int_of_vect status.acc in
1641        let b = int_of_vect status.b in
1642        let prod = acc * b in
1643        let ov = prod > 255 in
1644        let l = vect_of_int (prod  mod 256) `Eight in
1645        let h = vect_of_int (prod / 256) `Eight in
1646        let status = { status with acc = l ; b = h } in
1647         (* DPM: Carry flag is always cleared. *)
1648        set_flags status false None ov
1649      | `DIV (`A,`B) ->
1650        let acc = int_of_vect status.acc in
1651        let b = int_of_vect status.b in
1652        if b = 0 then
1653        (* CSC: ACC and B undefined! We leave them as they are. *)
1654          set_flags status false None true
1655        else
1656          let q = vect_of_int (acc / b) `Eight in
1657          let r = vect_of_int (acc mod b) `Eight in
1658          let status = { status with acc = q ; b = r } in
1659          set_flags status false None false
1660      | `DA `A ->
1661        let acc_upper_nibble, acc_lower_nibble = from_byte status.acc in
1662        if int_of_vect acc_lower_nibble > 9 or get_ac_flag status = true then
1663          let acc,cy,_,_ = add8_with_c status.acc (vect_of_int 6 `Eight) false in
1664          let acc_upper_nibble, acc_lower_nibble = from_byte acc in
1665          if int_of_vect acc_upper_nibble > 9 or cy = true then
1666            let cry,acc_upper_nibble = half_add acc_upper_nibble (vect_of_int 6 `Four) in
1667            let status = { status with acc = mk_byte acc_upper_nibble acc_lower_nibble } in
1668            set_flags status cry (Some (get_ac_flag status)) (get_ov_flag status)
1669          else
1670            status
1671        else
1672          status
1673      | `ANL (`U1(`A, ag)) ->
1674        let and_val = get_arg_8 status true `A -&- get_arg_8 status true ag in
1675        set_arg_8 status and_val `A
1676      | `ANL (`U2((`DIRECT d), ag)) ->
1677        let and_val = get_arg_8 status true (`DIRECT d) -&- get_arg_8 status true ag in
1678        set_arg_8 status and_val (`DIRECT d)
1679      | `ANL (`U3 (`C, b)) ->
1680        let and_val = get_cy_flag status && get_arg_1 status true b in
1681        set_flags status and_val None (get_ov_flag status)
1682      | `ORL (`U1(`A, ag)) ->
1683        let or_val = get_arg_8 status true `A -|- get_arg_8 status true ag in
1684        set_arg_8 status or_val `A
1685      | `ORL (`U2((`DIRECT d), ag)) ->
1686        let or_val = get_arg_8 status true (`DIRECT d) -|- get_arg_8 status true ag in
1687        set_arg_8 status or_val (`DIRECT d)
1688      | `ORL (`U3 (`C, b)) ->
1689        let or_val = get_cy_flag status || get_arg_1 status true b in
1690        set_flags status or_val None (get_ov_flag status)
1691      | `XRL (`U1(`A, ag)) ->
1692        let xor_val = get_arg_8 status true `A -^- get_arg_8 status true ag in
1693        set_arg_8 status xor_val `A
1694      | `XRL (`U2((`DIRECT d), ag)) ->
1695        let xor_val = get_arg_8 status true (`DIRECT d) -^- get_arg_8 status true ag in
1696        set_arg_8 status xor_val (`DIRECT d)
1697      | `CLR `A -> set_arg_8 status (zero `Eight) `A
1698      | `CLR `C -> set_arg_1 status false `C
1699      | `CLR ((`BIT _) as a) -> set_arg_1 status false a
1700      | `CPL `A -> { status with acc = complement status.acc }
1701      | `CPL `C -> set_arg_1 status (not $ get_arg_1 status true `C) `C
1702      | `CPL ((`BIT _) as b) -> set_arg_1 status (not $ get_arg_1 status true b) b
1703      | `RL `A -> { status with acc = rotate_left status.acc }
1704      | `RLC `A ->
1705        let old_cy = get_cy_flag status in
1706        let n1, n2 = from_byte status.acc in
1707        let (b1,b2,b3,b4),(b5,b6,b7,b8) = from_nibble n1, from_nibble n2 in
1708        let status = set_arg_1 status b1 `C in
1709        { status with acc = mk_byte (mk_nibble b2 b3 b4 b5) (mk_nibble b6 b7 b8 old_cy) }
1710      | `RR `A -> { status with acc = rotate_right status.acc }
1711      | `RRC `A ->
1712        let old_cy = get_cy_flag status in
1713        let n1, n2 = from_byte status.acc in
1714        let (b1,b2,b3,b4),(b5,b6,b7,b8) = from_nibble n1, from_nibble n2 in
1715        let status = set_arg_1 status b8 `C in
1716        { status with acc = mk_byte (mk_nibble old_cy b1 b2 b3) (mk_nibble b4 b5 b6 b7) }
1717      | `SWAP `A ->
1718        let (acc_nibble_upper, acc_nibble_lower) = from_byte status.acc in
1719        { status with acc = mk_byte acc_nibble_lower acc_nibble_upper }
1720      | `MOV(`U1(b1, b2)) -> set_arg_8 status (get_arg_8 status false b2) b1
1721      | `MOV(`U2(b1, b2)) -> set_arg_8 status (get_arg_8 status false b2) b1
1722      | `MOV(`U3(b1, b2)) -> set_arg_8 status (get_arg_8 status false b2) b1
1723      | `MOV(`U4(b1,b2)) -> set_arg_16 status (get_arg_16 status b2) b1
1724      | `MOV(`U5(b1,b2)) -> set_arg_1 status (get_arg_1 status false b2) b1
1725      | `MOV(`U6(b1,b2)) -> set_arg_1 status (get_arg_1 status false b2) b1
1726      | `MOVC (`A, `A_DPTR) ->
1727        let big_acc = mk_word (zero `Eight) status.acc in
1728        let dptr = mk_word status.dph status.dpl in
1729        let cry, addr = half_add dptr big_acc in
1730        let lookup = Physical.WordMap.find addr status.code_memory in
1731        { status with acc = lookup }
1732      | `MOVC (`A, `A_PC) ->
1733        let big_acc = mk_word (zero `Eight) status.acc in
1734        (* DPM: Under specified: does the carry from PC incrementation affect the *)
1735        (*      addition of the PC with the DPTR? At the moment, no.              *)
1736        let cry,inc_pc = half_add status.pc (vect_of_int 1 `Sixteen) in
1737        let status = { status with pc = inc_pc } in
1738        let cry,addr = half_add inc_pc big_acc in
1739        let lookup = Physical.WordMap.find addr status.code_memory in
1740        { status with acc = lookup }
1741      (* data transfer *)
1742      (* DPM: MOVX currently only implements the *copying* of data! *)
1743      | `MOVX (`U1 (a1, a2)) -> set_arg_8 status (get_arg_8 status false a2) a1
1744      | `MOVX (`U2 (a1, a2)) -> set_arg_8 status (get_arg_8 status false a2) a1
1745      | `SETB b -> set_arg_1 status true b
1746      | `PUSH a ->
1747       (* DPM: What happens if we overflow? *)
1748        let cry,new_sp = half_add status.sp (vect_of_int 1 `Eight) in
1749        let status = { status with sp = new_sp } in
1750        write_at_sp status (get_arg_8 status false a)
1751      | `POP (`DIRECT b) ->
1752        let contents = read_at_sp status in
1753        let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in
1754        let status = { status with sp = new_sp } in
1755        let status = set_arg_8 status contents (`DIRECT b) in
1756        status
1757      | `XCH(`A, arg) ->
1758        let old_arg = get_arg_8 status false arg in
1759        let old_acc = status.acc in
1760        let status = set_arg_8 status old_acc arg in
1761        { status with acc = old_arg }
1762      | `XCHD(`A, i) ->
1763        let acc_upper_nibble, acc_lower_nibble = from_byte $ get_arg_8 status false `A in
1764        let ind_upper_nibble, ind_lower_nibble = from_byte $ get_arg_8 status false i in
1765        let new_acc = mk_byte acc_upper_nibble ind_lower_nibble in
1766        let new_reg = mk_byte ind_upper_nibble acc_lower_nibble in
1767        let status = { status with acc = new_acc } in
1768        set_arg_8 status new_reg i
1769      (* program branching *)
1770      | `JC (`REL rel) ->
1771        if get_cy_flag status then
1772          let cry, new_pc = half_add status.pc (sign_extension rel) in
1773          { status with pc = new_pc }
1774        else
1775          status
1776      | `JNC (`REL rel) ->
1777        if not $ get_cy_flag status then
1778          let cry, new_pc = half_add status.pc (sign_extension rel) in
1779          { status with pc = new_pc }
1780        else
1781          status
1782      | `JB (b, (`REL rel)) ->
1783        if get_arg_1 status false b then
1784          let cry, new_pc = half_add status.pc (sign_extension rel) in
1785          { status with pc = new_pc }
1786        else
1787          status
1788      | `JNB (b, (`REL rel)) ->
1789        if not $ get_arg_1 status false b then
1790          let cry, new_pc = half_add status.pc (sign_extension rel) in
1791          { status with pc = new_pc }
1792        else
1793          status
1794      | `JBC (b, (`REL rel)) ->
1795        let status = set_arg_1 status false b in
1796        if get_arg_1 status false b then
1797          let cry, new_pc = half_add status.pc (sign_extension rel) in
1798          { status with pc = new_pc }
1799        else
1800          status
1801      | `RET ->
1802        (* DPM: What happens when we underflow? *)
1803        let high_bits = read_at_sp status in
1804        let new_sp,cy,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in
1805        let status = { status with sp = new_sp } in
1806        let low_bits = read_at_sp status in
1807        let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) cy in
1808        let status = { status with sp = new_sp } in
1809        { status with pc = mk_word high_bits low_bits }
1810      | `RETI ->
1811        let high_bits = read_at_sp status in
1812        let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in
1813        let status = { status with sp = new_sp } in
1814        let low_bits = read_at_sp status in
1815        let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in
1816        let status = { status with sp = new_sp } in
1817        { status with pc = mk_word high_bits low_bits }
1818      | `ACALL (`ADDR11 a) ->
1819        let cry, new_sp = half_add status.sp (vect_of_int 1 `Eight) in
1820        let status = { status with sp = new_sp } in
1821        let pc_upper_byte, pc_lower_byte = from_word status.pc in
1822        let status = write_at_sp status pc_lower_byte in
1823        let cry, new_sp = half_add status.sp (vect_of_int 1 `Eight) in
1824        let status = { status with sp = new_sp } in
1825        let status = write_at_sp status pc_upper_byte in
1826        let addr = addr16_of_addr11 status.pc a in
1827        { status with pc = addr }
1828      | `LCALL (`ADDR16 addr) ->
1829        let cry, new_sp = half_add status.sp (vect_of_int 1 `Eight) in
1830        let status = { status with sp = new_sp } in
1831        let pc_upper_byte, pc_lower_byte = from_word status.pc in
1832        let status = write_at_sp status pc_lower_byte in
1833        let cry, new_sp = half_add status.sp (vect_of_int 1 `Eight) in
1834        let status = { status with sp = new_sp } in
1835        let status = write_at_sp status pc_upper_byte in
1836        { status with pc = addr }
1837      | `AJMP (`ADDR11 a) ->
1838        let addr = addr16_of_addr11 status.pc a in
1839        { status with pc = addr }
1840      | `LJMP (`ADDR16 a) ->
1841        { status with pc = a }
1842      | `SJMP (`REL rel) ->
1843        let cry, new_pc = half_add status.pc (sign_extension rel) in
1844        { status with pc = new_pc }
1845      | `JMP `IND_DPTR ->
1846        let dptr = mk_word status.dph status.dpl in
1847        let big_acc = mk_word (zero `Eight) status.acc in
1848        let cry, jmp_addr = half_add big_acc dptr in
1849        let cry, new_pc = half_add status.pc jmp_addr in
1850        { status with pc = new_pc }
1851      | `JZ (`REL rel) ->
1852        if status.acc = zero `Eight then
1853          let cry, new_pc = half_add status.pc (sign_extension rel) in
1854          { status with pc = new_pc }
1855        else
1856          status
1857      | `JNZ (`REL rel) ->
1858        if status.acc <> zero `Eight then
1859          let cry, new_pc = half_add status.pc (sign_extension rel) in
1860          { status with pc = new_pc }
1861        else
1862          status
1863      | `CJNE ((`U1 (`A, ag)), `REL rel) ->
1864        let new_carry = status.acc < get_arg_8 status false ag in
1865        if get_arg_8 status false ag <> status.acc then
1866          let cry, new_pc = half_add status.pc (sign_extension rel) in
1867          let status = set_flags status new_carry None (get_ov_flag status) in
1868          { status with pc = new_pc;  }
1869        else
1870          set_flags status new_carry None (get_ov_flag status)
1871      | `CJNE ((`U2 (ag, `DATA d)), `REL rel) ->
1872        let new_carry = get_arg_8 status false ag < d in
1873        if get_arg_8 status false ag <> d then
1874          let cry, new_pc = half_add status.pc (sign_extension rel) in
1875          let status = { status with pc = new_pc } in
1876          set_flags status new_carry None (get_ov_flag status)
1877        else
1878          set_flags status new_carry None (get_ov_flag status)
1879      | `DJNZ (ag, (`REL rel)) ->
1880        let new_ag,_,_,_ = subb8_with_c (get_arg_8 status true ag) (vect_of_int 1 `Eight) false in
1881        let status = set_arg_8 status new_ag ag in
1882        if new_ag <> zero `Eight then
1883          let cry, new_pc = half_add status.pc (sign_extension rel) in
1884          { status with pc = new_pc }
1885        else
1886          status
1887      | `NOP -> status) in
1888  let status = timers status ticks in
1889  let in_cont, `Out out_cont = status.io in
1890  let status = serial_port_input status in_cont in
1891  let status = serial_port_output status out_cont in
1892  let status = interrupts status in
1893  { status with previous_p1_val = get_bit status.p3 4;
1894    previous_p3_val = get_bit status.p3 5 }
1895;;
1896
1897(*
1898OLD output routine:
1899           (* Serial port output, part one *)
1900           let status =
1901             (match status.expected_out_time with
1902               `At t when status.clock >= t ->
1903                 { status with scon = set_bit status.scon 1 true; expected_out_time = `None }
1904              | _ -> status) in
1905
1906             (if status.expected_out_time = `Now then
1907               if get_bit status.scon 7 then
1908                 let exp_time, new_cont = out_cont status.clock (`SerialBuff (`Nine ((get_bit status.scon 3), status.sbuf))) in
1909                   { status with expected_out_time = `At exp_time; io = new_cont }
1910               else
1911                 let exp_time, new_cont = out_cont status.clock (`SerialBuff (`Eight status.sbuf)) in
1912                   { status with expected_out_time = `At exp_time; io = new_cont }               
1913             else
1914               status) in
1915*)
1916
1917let rec execute f s =
1918  let cont =
1919    try f s; true
1920    with Halt -> false
1921  in
1922  if cont then execute f (execute1 s)
1923  else s
1924;;
1925
1926
1927let load_program p =
1928  let st = load p.ASM.code initialize in
1929  { st with exit_addr = p.ASM.exit_addr ; cost_labels = p.ASM.cost_labels }
1930
1931let observe_trace trace_ref st =
1932  let cost_label =
1933    if BitVectors.WordMap.mem st.pc st.cost_labels then
1934      [BitVectors.WordMap.find st.pc st.cost_labels]
1935    else [] in
1936  trace_ref := cost_label @ !trace_ref ;
1937  if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st
1938
1939let result st =
1940  let i = BitVectors.int_of_vect st.dpl in
1941  IntValue.Int8.of_int i
1942
1943let interpret print_result p =
1944  if p.ASM.has_main then
1945    let st = load_program p in
1946    let trace = ref [] in
1947    let callback = observe_trace trace in
1948    let st = execute callback st in
1949    let res = result st in
1950    if print_result then
1951      Printf.printf "8051: %s\n%!" (IntValue.Int8.to_string res) ;
1952    (res, List.rev !trace)
1953  else (IntValue.Int8.zero, [])
Note: See TracBrowser for help on using the repository browser.