1 | open BitVectors;; |
---|
2 | open ASM;; |
---|
3 | |
---|
4 | let hex_string_of_vect v = |
---|
5 | "[[" ^ String.concat ";" (List.map string_of_bool (Obj.magic v)) ^ "]]" |
---|
6 | ;; |
---|
7 | |
---|
8 | let pp_arg = |
---|
9 | function |
---|
10 | `A -> "ACC_A" |
---|
11 | | `B -> "ACC_B" |
---|
12 | | `C -> "CARRY" |
---|
13 | | `DPTR -> "DPTR" |
---|
14 | | `ADDR11 x -> "ADDR11 " ^ hex_string_of_vect x |
---|
15 | | `ADDR16 x -> "ADDR16 " ^ hex_string_of_vect x |
---|
16 | | `DATA x -> "DATA " ^ hex_string_of_vect x |
---|
17 | | `DATA16 x -> "DATA16 " ^ hex_string_of_vect x |
---|
18 | | `BIT x -> "BIT_ADDR " ^ hex_string_of_vect (x: byte) |
---|
19 | | `NBIT x -> "N_BIT_ADDR " ^ hex_string_of_vect (x: byte) |
---|
20 | | `REG (r1, r2, r3) -> "REGISTER " ^ hex_string_of_vect (Obj.magic [r1;r2;r3]) |
---|
21 | | `REL x -> "RELATIVE " ^ hex_string_of_vect x |
---|
22 | | `A_DPTR -> "ACC_DPTR" |
---|
23 | | `A_PC -> "ACC_PC" |
---|
24 | | `DIRECT x -> "DIRECT " ^ hex_string_of_vect (x: byte) |
---|
25 | | `EXT_INDIRECT x -> "EXT_INDIRECT " ^ string_of_bool x |
---|
26 | | `EXT_IND_DPTR -> "EXT_INDIRECT_DPTR" |
---|
27 | (* DPM: weird: this seems to be reversed in mcu8051ide: change made. *) |
---|
28 | | `INDIRECT x -> "INDIRECT " ^ string_of_bool x |
---|
29 | | `IND_DPTR -> "INDIRECT_DPTR" |
---|
30 | | `Label s -> s |
---|
31 | ;; |
---|
32 | |
---|
33 | let pp_arg a = "(" ^ pp_arg a ^ ")";; |
---|
34 | |
---|
35 | let pp_jump = |
---|
36 | function |
---|
37 | `CJNE (`U1 (a1,a2),a3) -> "CJNE … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉) " ^ pp_arg a3 |
---|
38 | | `CJNE (`U2 (a1,a2),a3) -> "CJNE … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉) " ^ pp_arg a3 |
---|
39 | | `DJNZ (a1,a2) -> "DJNZ … " ^ pp_arg a1 ^ " " ^ pp_arg a2 |
---|
40 | | `JB (a1,a2) -> "JB … " ^ pp_arg a1 ^ " " ^ pp_arg a2 |
---|
41 | | `JBC (a1,a2) -> "JBC … " ^ pp_arg a1 ^ " " ^ pp_arg a2 |
---|
42 | | `JC a1 -> "JC … " ^ pp_arg a1 |
---|
43 | | `JNB (a1,a2) -> "JNB … " ^ pp_arg a1 ^ " " ^ pp_arg a2 |
---|
44 | | `JNC a1 -> "JNC … " ^ pp_arg a1 |
---|
45 | | `JNZ a1 -> "JNZ … " ^ pp_arg a1 |
---|
46 | | `JZ a1 -> "JZ … " ^ pp_arg a1 |
---|
47 | |
---|
48 | let pp_jump j = |
---|
49 | "Jump … (" ^ pp_jump j ^ ")" |
---|
50 | ;; |
---|
51 | |
---|
52 | let pp_matita_instruction = |
---|
53 | function |
---|
54 | `Label l -> l ^ ":" |
---|
55 | | `Cost l -> l ^ ":" |
---|
56 | | `Jmp j -> "Jump " ^ j |
---|
57 | | `Call j -> "Call " ^ j |
---|
58 | | `WithLabel i -> pp_jump i |
---|
59 | | (#jump as i) -> pp_jump i |
---|
60 | | `Mov (a1,a2) -> "MOV … " ^ pp_arg a1 ^ " " ^ a2 |
---|
61 | | `ACALL a1 -> "ACALL … " ^ pp_arg a1 |
---|
62 | | `ADD (a1,a2) -> "ADD … " ^ pp_arg a1 ^ " " ^ pp_arg a2 |
---|
63 | | `ADDC (a1,a2) -> "ADDC … " ^ pp_arg a1 ^ " " ^ pp_arg a2 |
---|
64 | | `AJMP a1 -> "AJMP … " ^ pp_arg a1 |
---|
65 | | `ANL (`U1 (a1,a2)) -> "ANL … (Left … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))" |
---|
66 | | `ANL (`U2 (a1,a2)) -> "ANL … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))" |
---|
67 | | `ANL (`U3 (a1,a2)) -> "ANL … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)" |
---|
68 | | `CLR a1 -> "CLR … " ^ pp_arg a1 |
---|
69 | | `CPL a1 -> "CPL … " ^ pp_arg a1 |
---|
70 | | `DA a1 -> "DA … " ^ pp_arg a1 |
---|
71 | | `DEC a1 -> "DEC … " ^ pp_arg a1 |
---|
72 | | `DIV (a1,a2) -> "DIV … " ^ pp_arg a1 ^ " " ^ pp_arg a2 |
---|
73 | | `INC a1 -> "INC … " ^ pp_arg a1 |
---|
74 | | `JMP a1 -> "JMP … " ^ pp_arg a1 |
---|
75 | | `LCALL a1 -> "LCALL … " ^ pp_arg a1 |
---|
76 | | `LJMP a1 -> "LJMP … " ^ pp_arg a1 |
---|
77 | | `MOV (`U1 (a1,a2)) -> "MOV … (Left … (Left … (Left … (Left … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)))))" |
---|
78 | | `MOV (`U2 (a1,a2)) -> "MOV … (Left … (Left … (Left … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)))))" |
---|
79 | | `MOV (`U3 (a1,a2)) -> "MOV … (Left … (Left … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))))" |
---|
80 | | `MOV (`U4 (a1,a2)) -> "MOV … (Left … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)))" |
---|
81 | | `MOV (`U5 (a1,a2)) -> "MOV … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))" |
---|
82 | | `MOV (`U6 (a1,a2)) -> "MOV … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)" |
---|
83 | | `MOVC (a1,a2) -> "MOVC … " ^ pp_arg a1 ^ " " ^ pp_arg a2 |
---|
84 | | `MOVX (`U1 (a1,a2)) -> "MOVX … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)" |
---|
85 | | `MOVX (`U2 (a1,a2)) -> "MOVX … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)" |
---|
86 | | `MUL(a1, a2) -> "MUL … " ^ pp_arg a1 ^ " " ^ pp_arg a2 |
---|
87 | | `NOP -> "NOP … " |
---|
88 | | `ORL (`U1 (a1,a2)) -> "ORL … (Left … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))" |
---|
89 | | `ORL (`U2 (a1,a2)) -> "ORL … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))" |
---|
90 | | `ORL (`U3 (a1,a2)) -> "ORL … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)" |
---|
91 | | `POP a1 -> "POP … " ^ pp_arg a1 |
---|
92 | | `PUSH a1 -> "PUSH … " ^ pp_arg a1 |
---|
93 | | `RET -> "RET … " |
---|
94 | | `RETI -> "RETI … " |
---|
95 | | `RL a1 -> "RL … " ^ pp_arg a1 |
---|
96 | | `RLC a1 -> "RLC … " ^ pp_arg a1 |
---|
97 | | `RR a1 -> "RR … " ^ pp_arg a1 |
---|
98 | | `RRC a1 -> "RRC … " ^ pp_arg a1 |
---|
99 | | `SETB a1 -> "SETB … " ^ pp_arg a1 |
---|
100 | | `SJMP a1 -> "SJMP … " ^ pp_arg a1 |
---|
101 | | `SUBB (a1,a2) -> "SUBB … " ^ pp_arg a1 ^ " " ^ pp_arg a2 |
---|
102 | | `SWAP a1 -> "SWAP … " ^ pp_arg a1 |
---|
103 | | `XCH (a1,a2) -> "XCH … " ^ pp_arg a1 ^ " " ^ pp_arg a2 |
---|
104 | | `XCHD(a1,a2) -> "XCHD … " ^ pp_arg a1 ^ " " ^ pp_arg a2 |
---|
105 | | `XRL (`U1 (a1,a2)) -> "XRL … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)" |
---|
106 | | `XRL (`U2 (a1,a2)) -> "XRL … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)" |
---|