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