8 exception Fetch_exception of string;;
9 exception CodeTooLarge;;
12 let extract = function
14 | None -> raise (Failure "ASMInterpret.extract")
17 type line = [ `P1 of byte
19 | `SerialBuff of [ `Eight of byte | `Nine of BitVectors.bit * byte ]];;
24 "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^
25 "P1 OUTPUT: " ^ hex_string_of_vect b ^ "\n" ^
26 "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n"
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
40 string_of_int (128 + i)
43 "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n"
45 (* In: reception time, line of input, new continuation,
46 Out: transmission time, output line, expected duration until reply,
53 [`In of time * line * epsilon * continuation] option *
54 [`Out of (time -> line -> time * continuation)]
56 let rec debug_continuation =
57 (Some (`In (1, (`SerialBuff (`Eight (vect_of_int 5 `Eight))), 0, debug_continuation))), `Out (
59 (* let _ = prerr_endline <*> string_of_line $ line in *)
60 (time + 1),debug_continuation)
62 (* no differentiation between internal and external code 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;
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 *)
100 (* Latches for the output lines *)
104 (* Fields for tracking the state of the processor. *)
107 previous_p1_val: bool;
108 previous_p3_val: bool;
110 serial_epsilon_out: epsilon option;
111 serial_epsilon_in: epsilon option;
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;
118 serial_k_out: continuation option;
121 expected_out_time: [ `None | `Now | `At of time ];
123 (* Timer and clock specific *)
127 timer2: word; (* can be missing *)
136 exit_addr : BitVectors.word;
137 cost_labels : string BitVectors.WordMap.t
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 *)
150 | 0xA0 -> assert false (* P2 not modeled *)
155 | 0x99 -> status.sbuf
160 | 0xC8 -> status.t2con
161 | 0xCA -> status.rcap2l
162 | 0xCB -> status.rcap2h
167 | 0x87 -> status.pcon
168 | 0x88 -> status.tcon
169 | 0x89 -> status.tmod
170 | 0x98 -> status.scon
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 }
193 if status.expected_out_time = `None then
194 { status with sbuf = v; expected_out_time = `Now }
196 (* a real assert false: trying to initiate a transmission whilst one is still active *)
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 }
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 }
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 }
227 code_memory = Physical.WordMap.empty;
228 low_internal_ram = Byte7Map.empty;
229 high_internal_ram = Byte7Map.empty;
230 external_ram = Physical.WordMap.empty;
234 sp = vect_of_int 7 `Eight;
245 p1_latch = zero `Eight;
250 p3_latch = zero `Eight;
256 rcap2l = zero `Eight;
257 rcap2h = zero `Eight;
261 previous_p1_val = false;
262 previous_p3_val = false;
266 serial_epsilon_in = None;
267 serial_epsilon_out = None;
273 timer0 = zero `Sixteen;
274 timer1 = zero `Sixteen;
275 timer2 = zero `Sixteen;
277 expected_out_time = `None;
279 io = debug_continuation; (* a real assert false: unprepared for i/o *)
281 (* Initially no interrupts are executing *)
289 exit_addr = BitVectors.zero `Sixteen;
290 cost_labels = BitVectors.WordMap.empty
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
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
320 vect_of_int (base + int_of_vect (mk_nibble false b1 b2 b3)) `Seven
323 let get_register status reg =
324 let addr = get_address_of_register status reg in
325 Byte7Map.find addr status.low_internal_ram
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" ^
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"
384 (* timings taken from SIEMENS *)
388 let _carry, res = half_add pc (vect_of_int 1 `Sixteen) in
389 res, Physical.WordMap.find pc pmem
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
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) ->
462 | (true,true,false,false),(false,false,true,true) ->
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) ->
469 | (true,false,true,true),(false,false,true,true) ->
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) ->
476 | (false,false,false,true),(false,true,false,false) ->
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) ->
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) ->
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) ->
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
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
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) ->
606 | (false,false,false,false),(false,false,false,false) ->
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) ->
639 | (false,false,true,true),(false,false,true,false) ->
641 | (false,false,true,false),(false,false,true,true) ->
643 | (false,false,true,true),(false,false,true,true) ->
645 | (false,false,false,false),(false,false,true,true) ->
647 | (false,false,false,true),(false,false,true,true) ->
649 | (true,true,false,true),(false,false,true,true) ->
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) ->
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
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]
748 [mk_byte_from_bits ((true,true,true,false),(false,true,false,false))]
750 [mk_byte_from_bits ((true,true,false,false),(false,false,true,true))]
752 [mk_byte_from_bits ((true,true,false,false),(false,false,true,false)); b1]
754 [mk_byte_from_bits ((true,true,true,true),(false,true,false,false))]
756 [mk_byte_from_bits ((true,false,true,true),(false,false,true,true))]
758 [mk_byte_from_bits ((true,false,true,true),(false,false,true,false)); b1]
760 [mk_byte_from_bits ((true,true,false,true),(false,true,false,false))]
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))]
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]
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))]
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]
790 [mk_byte_from_bits ((false,true,false,false),(false,false,false,false)); b1]
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]
796 [mk_byte_from_bits ((false,true,false,true),(false,false,false,false)); b1]
798 [mk_byte_from_bits ((false,true,true,true),(false,false,false,false)); 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))]
857 [mk_byte_from_bits ((true,false,true,false),(false,true,false,false))]
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]
881 [mk_byte_from_bits ((false,false,true,false),(false,false,true,false))]
883 [mk_byte_from_bits ((false,false,true,true),(false,false,true,false))]
885 [mk_byte_from_bits ((false,false,true,false),(false,false,true,true))]
887 [mk_byte_from_bits ((false,false,true,true),(false,false,true,true))]
889 [mk_byte_from_bits ((false,false,false,false),(false,false,true,true))]
891 [mk_byte_from_bits ((false,false,false,true),(false,false,true,true))]
893 [mk_byte_from_bits ((true,true,false,true),(false,false,true,true))]
895 [mk_byte_from_bits ((true,true,false,true),(false,false,true,false)); 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]
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]
930 let load_code_memory = MiscPottier.foldi (fun i mem v -> Physical.WordMap.add (vect_of_int i `Sixteen) v mem) Physical.WordMap.empty
932 let load_mem mem status = { status with code_memory = mem }
933 let load l = load_mem (load_code_memory l)
935 let assembly_jump addr_of =
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)
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
956 let pc,exit_addr,labels,costs =
958 (fun (pc,exit_addr,labels,costs) i ->
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
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 *)
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
977 (snd (half_add pc pc'),exit_addr,labels, costs)
979 (BitVectors.zero `Sixteen,BitVectors.zero `Sixteen,
980 StringTools.Map.empty, BitVectors.WordMap.empty) p.ASM.pcode
983 List.flatten (List.map
988 (* We need to expand a conditional jump to a label to a machine language
989 conditional jump. Suppose we have:
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 =
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
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
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)
1042 (* let addr16 = StringTools.Map.find s datalabels in *)
1044 try StringTools.Map.find s datalabels
1045 with Not_found -> StringTools.Map.find s labels in
1046 assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16)))
1048 let pc_offset = StringTools.Map.find s labels in
1049 assembly1 (`LJMP (`ADDR16 pc_offset))
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 }
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 }
1065 let get_arg_8 status from_latch =
1068 let n0, n1 = from_byte addr in
1069 (match from_nibble n0 with
1071 Byte7Map.find (mk_byte7 r1 r2 r3 n1) status.low_internal_ram
1072 | _ -> get_sfr status addr from_latch)
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)
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
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
1099 let dpr = mk_word status.dph status.dpl in
1100 Physical.WordMap.find dpr status.external_ram
1103 let get_arg_16 _status = function `DATA16 w -> w
1105 let get_arg_1 status from_latch =
1108 | `NBIT addr as x ->
1109 let n1, n2 = from_byte addr in
1111 (match from_nibble n1 with
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
1124 let set_arg_1 status v =
1127 let n1, n2 = from_byte addr in
1128 (match from_nibble n1 with
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')
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) }
1147 let set_arg_8 status v =
1150 let (b1, b2) = from_byte addr in
1151 (match from_nibble b1 with
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)
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 }
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 }
1179 let set_arg_16 status wrd =
1182 let (dh, dl) = from_word wrd in
1183 { status with dph = dh; dpl = dl }
1185 let set_flags status c ac ov =
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)
1195 if b1 = true && b2 = true then
1197 else if b1 = false && b2 = false then
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)
1209 let write_at_sp status v =
1210 let n1,n2 = from_byte status.sp in
1211 match from_nibble n1 with
1214 Byte7Map.add (mk_byte7 r1 r2 r3 n2) v status.low_internal_ram
1216 { status with low_internal_ram = memory }
1219 Byte7Map.add (mk_byte7 r1 r2 r3 n2) v status.high_internal_ram
1221 { status with high_internal_ram = memory }
1224 let timer0 status b1 b2 ticks =
1225 let b = get_bit status.tcon 4 in
1229 (* Archaic 13 bit mode. *)
1231 let res,_,_,_ = add8_with_c status.tl0 (vect_of_int ticks `Eight) false in
1232 let res = int_of_vect res in
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
1237 let b = set_bit status.tcon 7 true in
1238 { status with tcon = b; th0 = res'; tl0 = vect_of_int res `Eight }
1240 { status with th0 = res'; tl0 = vect_of_int res `Eight }
1242 { status with tl0 = vect_of_int res `Eight }
1246 (* 8 bit split timer mode. *)
1249 let res,cy,ov,ac = add8_with_c status.tl0 (vect_of_int ticks `Eight) false in
1251 let b = set_bit status.tcon 5 true in
1252 { status with tcon = b; tl0 = res }
1254 { status with tl0 = res }
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
1261 let b = set_bit status.tcon 7 true in
1262 { status with tcon = b; th0 = res }
1264 { status with th0 = res }
1268 (* 16 bit timer mode. *)
1270 let res,_,ov,_ = add16_with_c (mk_word status.th0 status.tl0) (vect_of_int ticks `Sixteen) false in
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 }
1276 let new_th0,new_tl0 = from_word res in
1277 { status with th0 = new_th0; tl0 = new_tl0 }
1281 (* 8 bit single timer mode. *)
1283 let res,_,ov,_ = add8_with_c status.tl0 (vect_of_int ticks `Eight) false in
1285 let b = set_bit status.tcon 5 true in
1286 { status with tcon = b; tl0 = status.th0; }
1288 { status with tl0 = res }
1292 let timer1 status b3 b4 ticks =
1293 let b = get_bit status.tcon 4 in
1296 (* Archaic 13 bit mode. *)
1298 let res,_,_,_ = add8_with_c status.tl1 (vect_of_int ticks `Eight) false in
1299 let res = int_of_vect res in
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
1304 let b = set_bit status.tcon 7 true in
1305 { status with tcon = b; th1 = res'; tl1 = vect_of_int res `Eight }
1307 { status with th1 = res'; tl0 = vect_of_int res `Eight }
1309 { status with tl1 = vect_of_int res `Eight }
1313 (* 8 bit split timer mode. *)
1316 let res,cy,ov,ac = add8_with_c status.tl1 (vect_of_int ticks `Eight) false in
1318 let b = set_bit status.tcon 5 true in
1319 { status with tcon = b; tl1 = res }
1321 { status with tl1 = res }
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
1328 let b = set_bit status.tcon 7 true in
1329 { status with tcon = b; th1 = res }
1331 { status with th1 = res }
1335 (* 16 bit timer mode. *)
1337 let res,_,ov,_ = add16_with_c (mk_word status.th0 status.tl1) (vect_of_int ticks `Sixteen) false in
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 }
1343 let new_th1,new_tl1 = from_word res in
1344 { status with th1 = new_th1; tl1 = new_tl1 }
1348 (* 8 bit single timer mode. *)
1350 let res,_,ov,_ = add8_with_c status.tl1 (vect_of_int ticks `Eight) false in
1352 let b = set_bit status.tcon 5 true in
1353 { status with tcon = b; tl1 = status.th1; }
1355 { status with tl1 = res }
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) ->
1366 if get_bit status.p3 2 then
1368 if status.previous_p1_val && not $ get_bit status.p3 4 then
1369 timer0 status b1 b2 ticks
1373 timer0 status b1 b2 ticks
1377 timer0 status b1 b2 ticks) in
1378 (* Timer 1 follows. *)
1381 if get_bit status.p1 3 then
1383 if status.previous_p3_val && not $ get_bit status.p3 5 then
1384 timer1 status b3 b4 ticks
1388 timer1 status b3 b4 ticks
1392 timer1 status b3 b4 ticks) in
1393 (* Timer 2 follows *)
1395 (let (tf2,exf2,rclk,tclk),(exen2,tr2,ct2,cp2) = bits_of_byte status.t2con in
1396 (* Timer2 is enabled *)
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
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;
1412 { status with th2 = new_th2;
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;
1423 let new_th2, new_tl2 = from_word res in
1424 { status with th2 = new_th2;
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 *)
1433 status (* Implement clock here *)
1441 let serial_port_input status in_cont =
1442 (* Serial port input *)
1444 Some (`In(time, line, epsilon, cont)) when get_bit status.scon 4 ->
1448 if status.clock >= time then
1449 { status with p1 = b; p1_latch = b; }
1453 if status.clock >= time then
1454 { status with p3 = b; p3_latch = b; }
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
1462 (* Mode 0: shift register. No delay. *)
1463 if status.clock >= time then
1464 { status with scon = set_bit status.scon 0 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
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! *)
1481 { status with serial_epsilon_in = Some (epsilon + time);
1482 serial_v_in = Some (`Eight b) }
1484 (* Warning about incomplete case analysis here, but safe as we've already tested for
1486 let e = extract status.serial_epsilon_in in
1487 let v = extract status.serial_v_in in
1488 if status.clock >= e then
1491 { status with sbuf = v';
1493 serial_epsilon_in = None;
1494 scon = set_bit status.scon 0 true;
1496 | _ -> assert false (* trying to read in 9 bits instead of 8 *)
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
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! *)
1520 { status with serial_epsilon_in = Some (epsilon + time);
1521 serial_v_in = Some (`Nine (b, b')) }
1523 (* Warning about incomplete case analysis here, but safe as we've already tested for
1525 let e = extract status.serial_epsilon_in in
1526 let v = extract status.serial_v_in in
1527 if status.clock >= e then
1530 let scon' = set_bit status.scon 0 true in
1531 { status with sbuf = v';
1533 serial_epsilon_in = None;
1534 scon = set_bit scon' 2 b;
1536 | _ -> assert false (* trying to read in 8 bits instead of 9 *)
1542 { status with io = cont })
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
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; }
1560 | _ -> assert false)
1563 let external_serial_interrupt status esi =
1564 (* Interrupt enabled *)
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
1571 (* If we should be running, but aren't... *)
1580 let external0_interrupt status e0i =
1581 (* Interrupt enabled *)
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
1588 (* If we should be running, but aren't... *)
1597 let external1_interrupt status e1i =
1598 (* Interrupt enabled *)
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
1605 (* If we should be running, but aren't... *)
1614 let timer0_interrupt status t0i =
1615 (* Interrupt enabled *)
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
1622 (* If we should be running, but aren't... *)
1631 let timer1_interrupt status t1i =
1632 (* Interrupt enabled *)
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
1639 (* If we should be running, but aren't... *)
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? *)
1653 match (ps,pt1,px1,pt0,px0) with
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
1666 add8_with_c (get_arg_8 status false `A) (get_arg_8 status false d1) false
1668 set_flags (set_arg_8 status v `A) c (Some ac) ov
1671 add8_with_c (get_arg_8 status false `A) (get_arg_8 status false d1) (get_cy_flag status)
1673 set_flags (set_arg_8 status v `A) c (Some ac) ov
1676 subb8_with_c (get_arg_8 status false `A) (get_arg_8 status false d1) (get_cy_flag status)
1678 set_flags (set_arg_8 status v `A) c (Some ac) ov
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
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
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
1702 let acc = int_of_vect status.acc in
1703 let b = int_of_vect status.b in
1705 (* CSC: ACC and B undefined! We leave them as they are. *)
1706 set_flags status false None true
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
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)
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 }
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 }
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) }
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 }
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
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
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 }
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 *)
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 }
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 }
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 }
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 }
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 }
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 }
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 }
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 }
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 }
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 }
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; }
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)
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 }
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 }
1951 (* Serial port output, part one *)
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 }
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 }
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 }
1969 let rec execute f s =
1974 if cont then execute f (execute1 s)
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 }
1983 let observe_trace trace_ref st =
1985 if BitVectors.WordMap.mem st.pc st.cost_labels then
1986 [BitVectors.WordMap.find st.pc st.cost_labels]
1988 trace_ref := cost_label @ !trace_ref ;
1989 if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st
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)
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
2011 Printf.printf "Result = %s\n%!" (IntValue.Int32.to_string res) ;
2012 (res, List.rev !trace)
2013 else (IntValue.Int32.zero, [])
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
2026 let size_of_instrs instrs =
2027 let f res instr = res + (size_of_instr instr) in
2028 List.fold_left f 0 instrs