[264] | 1 | include "ASM.ma". |
---|
[410] | 2 | include "BitVectorTrie.ma". |
---|
[264] | 3 | |
---|
| 4 | ndefinition assembly1 ≝ |
---|
[293] | 5 | λi: instruction.match i with |
---|
[269] | 6 | [ ACALL addr ⇒ |
---|
[271] | 7 | match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with |
---|
| 8 | [ ADDR11 w ⇒ λ_. |
---|
[312] | 9 | let 〈v1,v2〉 ≝ split ? (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in |
---|
[272] | 10 | [ (v1 @@ [[true; false; false; false; true]]) ; v2 ] |
---|
[271] | 11 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 12 | | ADD addr1 addr2 ⇒ |
---|
| 13 | match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with |
---|
[316] | 14 | [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ] |
---|
[271] | 15 | | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ] |
---|
| 16 | | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ] |
---|
| 17 | | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ] |
---|
| 18 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
[282] | 19 | | ADDC addr1 addr2 ⇒ |
---|
| 20 | match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with |
---|
[316] | 21 | [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ] |
---|
[282] | 22 | | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ] |
---|
| 23 | | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ] |
---|
| 24 | | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ] |
---|
| 25 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
| 26 | | AJMP addr ⇒ |
---|
| 27 | match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with |
---|
| 28 | [ ADDR11 w ⇒ λ_. |
---|
[312] | 29 | let 〈v1,v2〉 ≝ split ? (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in |
---|
[282] | 30 | [ (v1 @@ [[false; false; false; false; true]]) ; v2 ] |
---|
| 31 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 32 | | ANL addrs ⇒ |
---|
| 33 | match addrs with |
---|
| 34 | [ Left addrs ⇒ match addrs with |
---|
| 35 | [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
| 36 | match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with |
---|
[316] | 37 | [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ] |
---|
[282] | 38 | | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ] |
---|
| 39 | | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ] |
---|
| 40 | | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ] |
---|
| 41 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
| 42 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
| 43 | let b1 ≝ |
---|
| 44 | match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with |
---|
| 45 | [ DIRECT b1 ⇒ λ_.b1 |
---|
| 46 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in |
---|
| 47 | match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with |
---|
| 48 | [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ] |
---|
| 49 | | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ] |
---|
| 50 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
| 51 | ] |
---|
[283] | 52 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
[282] | 53 | match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with |
---|
| 54 | [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ] |
---|
| 55 | | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ] |
---|
[283] | 56 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] |
---|
[284] | 57 | | CLR addr ⇒ |
---|
| 58 | match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with |
---|
| 59 | [ ACC_A ⇒ λ_. |
---|
| 60 | [ ([[true; true; true; false; false; true; false; false]]) ] |
---|
| 61 | | CARRY ⇒ λ_. |
---|
| 62 | [ ([[true; true; false; false; false; false; true; true]]) ] |
---|
| 63 | | BIT_ADDR b1 ⇒ λ_. |
---|
| 64 | [ ([[true; true; false; false; false; false; true; false]]) ; b1 ] |
---|
| 65 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 66 | | CPL addr ⇒ |
---|
| 67 | match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with |
---|
| 68 | [ ACC_A ⇒ λ_. |
---|
| 69 | [ ([[true; true; true; true; false; true; false; false]]) ] |
---|
| 70 | | CARRY ⇒ λ_. |
---|
| 71 | [ ([[true; false; true; true; false; false; true; true]]) ] |
---|
| 72 | | BIT_ADDR b1 ⇒ λ_. |
---|
| 73 | [ ([[true; false; true; true; false; false; true; false]]) ; b1 ] |
---|
| 74 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 75 | | DA addr ⇒ |
---|
| 76 | [ ([[true; true; false; true; false; true; false; false]]) ] |
---|
| 77 | | DEC addr ⇒ |
---|
| 78 | match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect]] x) → ? with |
---|
| 79 | [ ACC_A ⇒ λ_. |
---|
| 80 | [ ([[false; false; false; true; false; true; false; false]]) ] |
---|
[316] | 81 | | REGISTER r ⇒ λ_. |
---|
| 82 | [ ([[false; false; false; true; true]]) @@ r ] |
---|
[284] | 83 | | DIRECT b1 ⇒ λ_. |
---|
| 84 | [ ([[false; false; false; true; false; true; false; true]]); b1 ] |
---|
| 85 | | INDIRECT i1 ⇒ λ_. |
---|
| 86 | [ ([[false; false; false; true; false; true; true; i1]]) ] |
---|
| 87 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 88 | | DIV addr1 addr2 ⇒ |
---|
| 89 | [ ([[true;false;false;false;false;true;false;false]]) ] |
---|
[293] | 90 | | Jump j ⇒ |
---|
| 91 | match j with |
---|
| 92 | [ DJNZ addr1 addr2 ⇒ |
---|
| 93 | let b2 ≝ |
---|
| 94 | match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
| 95 | [ RELATIVE b2 ⇒ λ_. b2 |
---|
| 96 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in |
---|
| 97 | match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with |
---|
[316] | 98 | [ REGISTER r ⇒ λ_. |
---|
| 99 | [ ([[true; true; false; true; true]]) @@ r ; b2 ] |
---|
[293] | 100 | | DIRECT b1 ⇒ λ_. |
---|
| 101 | [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ] |
---|
| 102 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) |
---|
| 103 | | JC addr ⇒ |
---|
| 104 | match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
| 105 | [ RELATIVE b1 ⇒ λ_. |
---|
| 106 | [ ([[false; true; false; false; false; false; false; false]]); b1 ] |
---|
| 107 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 108 | | JNC addr ⇒ |
---|
| 109 | match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
| 110 | [ RELATIVE b1 ⇒ λ_. |
---|
| 111 | [ ([[false; true; false; true; false; false; false; false]]); b1 ] |
---|
| 112 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 113 | | JZ addr ⇒ |
---|
| 114 | match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
| 115 | [ RELATIVE b1 ⇒ λ_. |
---|
| 116 | [ ([[false; true; true; false; false; false; false; false]]); b1 ] |
---|
| 117 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 118 | | JNZ addr ⇒ |
---|
| 119 | match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
| 120 | [ RELATIVE b1 ⇒ λ_. |
---|
| 121 | [ ([[false; true; true; true; false; false; false; false]]); b1 ] |
---|
| 122 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 123 | | JB addr1 addr2 ⇒ |
---|
| 124 | let b2 ≝ |
---|
| 125 | match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
| 126 | [ RELATIVE b2 ⇒ λ_. b2 |
---|
| 127 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in |
---|
| 128 | match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with |
---|
| 129 | [ BIT_ADDR b1 ⇒ λ_. |
---|
| 130 | [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ] |
---|
| 131 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) |
---|
| 132 | | JNB addr1 addr2 ⇒ |
---|
| 133 | let b2 ≝ |
---|
| 134 | match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
| 135 | [ RELATIVE b2 ⇒ λ_. b2 |
---|
| 136 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in |
---|
| 137 | match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with |
---|
| 138 | [ BIT_ADDR b1 ⇒ λ_. |
---|
| 139 | [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ] |
---|
| 140 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) |
---|
| 141 | | JBC addr1 addr2 ⇒ |
---|
| 142 | let b2 ≝ |
---|
| 143 | match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
| 144 | [ RELATIVE b2 ⇒ λ_. b2 |
---|
| 145 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in |
---|
| 146 | match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with |
---|
| 147 | [ BIT_ADDR b1 ⇒ λ_. |
---|
| 148 | [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ] |
---|
| 149 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) |
---|
| 150 | | CJNE addrs addr3 ⇒ |
---|
| 151 | let b3 ≝ |
---|
| 152 | match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
| 153 | [ RELATIVE b3 ⇒ λ_. b3 |
---|
| 154 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in |
---|
| 155 | match addrs with |
---|
| 156 | [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
| 157 | match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with |
---|
| 158 | [ DIRECT b1 ⇒ λ_. |
---|
| 159 | [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ] |
---|
[296] | 160 | | DATA b1 ⇒ λ_. |
---|
[293] | 161 | [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ] |
---|
| 162 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
| 163 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
| 164 | let b2 ≝ |
---|
| 165 | match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with |
---|
| 166 | [ DATA b2 ⇒ λ_. b2 |
---|
| 167 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in |
---|
[308] | 168 | match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → List Byte with |
---|
[316] | 169 | [ REGISTER r⇒ λ_. |
---|
| 170 | [ ([[true; false; true; true; true]]) @@ r; b2; b3 ] |
---|
[308] | 171 | | INDIRECT i1 ⇒ λ_. |
---|
| 172 | [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ] |
---|
| 173 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) ]] |
---|
[297] | 174 | | INC addr ⇒ |
---|
| 175 | match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;dptr]] x) → ? with |
---|
| 176 | [ ACC_A ⇒ λ_. |
---|
| 177 | [ ([[false;false;false;false;false;true;false;false]]) ] |
---|
[316] | 178 | | REGISTER r ⇒ λ_. |
---|
| 179 | [ ([[false;false;false;false;true]]) @@ r ] |
---|
[297] | 180 | | DIRECT b1 ⇒ λ_. |
---|
| 181 | [ ([[false; false; false; false; false; true; false; true]]); b1 ] |
---|
| 182 | | INDIRECT i1 ⇒ λ_. |
---|
| 183 | [ ([[false; false; false; false; false; true; true; i1]]) ] |
---|
| 184 | | DPTR ⇒ λ_. |
---|
| 185 | [ ([[true;false;true;false;false;false;true;true]]) ] |
---|
| 186 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 187 | | JMP addr ⇒ |
---|
| 188 | [ ([[false;true;true;true;false;false;true;true]]) ] |
---|
| 189 | | LCALL addr ⇒ |
---|
| 190 | match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with |
---|
| 191 | [ ADDR16 w ⇒ λ_. |
---|
| 192 | let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in |
---|
| 193 | [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ] |
---|
| 194 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 195 | | LJMP addr ⇒ |
---|
| 196 | match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with |
---|
| 197 | [ ADDR16 w ⇒ λ_. |
---|
| 198 | let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in |
---|
| 199 | [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ] |
---|
| 200 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
[303] | 201 | | MOV addrs ⇒ |
---|
| 202 | match addrs with |
---|
| 203 | [ Left addrs ⇒ |
---|
| 204 | match addrs with |
---|
| 205 | [ Left addrs ⇒ |
---|
| 206 | match addrs with |
---|
| 207 | [ Left addrs ⇒ |
---|
| 208 | match addrs with |
---|
| 209 | [ Left addrs ⇒ |
---|
| 210 | match addrs with |
---|
| 211 | [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
[304] | 212 | match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with |
---|
[316] | 213 | [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ] |
---|
[304] | 214 | | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ] |
---|
| 215 | | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ] |
---|
| 216 | | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ] |
---|
| 217 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
[303] | 218 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
[306] | 219 | match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with |
---|
[316] | 220 | [ REGISTER r ⇒ λ_. |
---|
[306] | 221 | match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with |
---|
[316] | 222 | [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ] |
---|
| 223 | | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ] |
---|
| 224 | | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ] |
---|
[306] | 225 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
| 226 | | INDIRECT i1 ⇒ λ_. |
---|
| 227 | match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with |
---|
| 228 | [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ] |
---|
| 229 | | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ] |
---|
| 230 | | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ] |
---|
| 231 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
| 232 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)] |
---|
[309] | 233 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
[304] | 234 | let b1 ≝ |
---|
| 235 | match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with |
---|
| 236 | [ DIRECT b1 ⇒ λ_. b1 |
---|
| 237 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in |
---|
[306] | 238 | match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;data]] x) → ? with |
---|
| 239 | [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1] |
---|
[316] | 240 | | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ] |
---|
[306] | 241 | | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ] |
---|
| 242 | | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ] |
---|
[309] | 243 | | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ] |
---|
| 244 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] |
---|
[303] | 245 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
[304] | 246 | match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with |
---|
| 247 | [ DATA16 w ⇒ λ_. |
---|
| 248 | let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in |
---|
| 249 | [ ([[true;false;false;true;false;false;false;false]]); b1; b2] |
---|
| 250 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] |
---|
[303] | 251 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
[305] | 252 | match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with |
---|
| 253 | [ BIT_ADDR b1 ⇒ λ_. |
---|
| 254 | [ ([[true;false;true;false;false;false;true;false]]); b1 ] |
---|
| 255 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] |
---|
[303] | 256 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
[305] | 257 | match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with |
---|
| 258 | [ BIT_ADDR b1 ⇒ λ_. |
---|
| 259 | [ ([[true;false;false;true;false;false;true;false]]); b1 ] |
---|
| 260 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)] |
---|
[297] | 261 | | MOVC addr1 addr2 ⇒ |
---|
| 262 | match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with |
---|
| 263 | [ ACC_DPTR ⇒ λ_. |
---|
| 264 | [ ([[true;false;false;true;false;false;true;true]]) ] |
---|
| 265 | | ACC_PC ⇒ λ_. |
---|
| 266 | [ ([[true;false;false;false;false;false;true;true]]) ] |
---|
| 267 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
[301] | 268 | | MOVX addrs ⇒ |
---|
| 269 | match addrs with |
---|
| 270 | [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
| 271 | match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with |
---|
| 272 | [ EXT_INDIRECT i1 ⇒ λ_. |
---|
| 273 | [ ([[true;true;true;false;false;false;true;i1]]) ] |
---|
| 274 | | EXT_INDIRECT_DPTR ⇒ λ_. |
---|
| 275 | [ ([[true;true;true;false;false;false;false;false]]) ] |
---|
| 276 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
| 277 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
| 278 | match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with |
---|
| 279 | [ EXT_INDIRECT i1 ⇒ λ_. |
---|
| 280 | [ ([[true;true;true;true;false;false;true;i1]]) ] |
---|
| 281 | | EXT_INDIRECT_DPTR ⇒ λ_. |
---|
| 282 | [ ([[true;true;true;true;false;false;false;false]]) ] |
---|
| 283 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)] |
---|
[298] | 284 | | MUL addr1 addr2 ⇒ |
---|
| 285 | [ ([[true;false;true;false;false;true;false;false]]) ] |
---|
| 286 | | NOP ⇒ |
---|
| 287 | [ ([[false;false;false;false;false;false;false;false]]) ] |
---|
[302] | 288 | | ORL addrs ⇒ |
---|
| 289 | match addrs with |
---|
| 290 | [ Left addrs ⇒ |
---|
| 291 | match addrs with |
---|
| 292 | [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
| 293 | match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with |
---|
[316] | 294 | [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ] |
---|
[302] | 295 | | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ] |
---|
| 296 | | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ] |
---|
| 297 | | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ] |
---|
| 298 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
| 299 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
| 300 | let b1 ≝ |
---|
| 301 | match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with |
---|
| 302 | [ DIRECT b1 ⇒ λ_. b1 |
---|
| 303 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in |
---|
| 304 | match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with |
---|
| 305 | [ ACC_A ⇒ λ_. |
---|
| 306 | [ ([[false;true;false;false;false;false;true;false]]); b1 ] |
---|
| 307 | | DATA b2 ⇒ λ_. |
---|
| 308 | [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ] |
---|
| 309 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] |
---|
| 310 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
| 311 | match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with |
---|
| 312 | [ BIT_ADDR b1 ⇒ λ_. |
---|
| 313 | [ ([[false;true;true;true;false;false;true;false]]); b1 ] |
---|
| 314 | | N_BIT_ADDR b1 ⇒ λ_. |
---|
| 315 | [ ([[true;false;true;false;false;false;false;false]]); b1 ] |
---|
| 316 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] |
---|
[298] | 317 | | POP addr ⇒ |
---|
| 318 | match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with |
---|
| 319 | [ DIRECT b1 ⇒ λ_. |
---|
| 320 | [ ([[true;true;false;true;false;false;false;false]]) ; b1 ] |
---|
| 321 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 322 | | PUSH addr ⇒ |
---|
| 323 | match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with |
---|
| 324 | [ DIRECT b1 ⇒ λ_. |
---|
| 325 | [ ([[true;true;false;false;false;false;false;false]]) ; b1 ] |
---|
| 326 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 327 | | RET ⇒ |
---|
| 328 | [ ([[false;false;true;false;false;false;true;false]]) ] |
---|
| 329 | | RETI ⇒ |
---|
| 330 | [ ([[false;false;true;true;false;false;true;false]]) ] |
---|
| 331 | | RL addr ⇒ |
---|
| 332 | [ ([[false;false;true;false;false;false;true;true]]) ] |
---|
| 333 | | RLC addr ⇒ |
---|
| 334 | [ ([[false;false;true;true;false;false;true;true]]) ] |
---|
| 335 | | RR addr ⇒ |
---|
| 336 | [ ([[false;false;false;false;false;false;true;true]]) ] |
---|
| 337 | | RRC addr ⇒ |
---|
| 338 | [ ([[false;false;false;true;false;false;true;true]]) ] |
---|
| 339 | | SETB addr ⇒ |
---|
| 340 | match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with |
---|
| 341 | [ CARRY ⇒ λ_. |
---|
| 342 | [ ([[true;true;false;true;false;false;true;true]]) ] |
---|
| 343 | | BIT_ADDR b1 ⇒ λ_. |
---|
| 344 | [ ([[true;true;false;true;false;false;true;false]]); b1 ] |
---|
| 345 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
[299] | 346 | | SJMP addr ⇒ |
---|
| 347 | match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
| 348 | [ RELATIVE b1 ⇒ λ_. |
---|
| 349 | [ ([[true;false;false;false;false;false;false;false]]); b1 ] |
---|
| 350 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
| 351 | | SUBB addr1 addr2 ⇒ |
---|
| 352 | match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with |
---|
[316] | 353 | [ REGISTER r ⇒ λ_. |
---|
| 354 | [ ([[true;false;false;true;true]]) @@ r ] |
---|
[299] | 355 | | DIRECT b1 ⇒ λ_. |
---|
| 356 | [ ([[true;false;false;true;false;true;false;true]]); b1] |
---|
| 357 | | INDIRECT i1 ⇒ λ_. |
---|
| 358 | [ ([[true;false;false;true;false;true;true;i1]]) ] |
---|
| 359 | | DATA b1 ⇒ λ_. |
---|
| 360 | [ ([[true;false;false;true;false;true;false;false]]); b1] |
---|
| 361 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
| 362 | | SWAP addr ⇒ |
---|
| 363 | [ ([[true;true;false;false;false;true;false;false]]) ] |
---|
| 364 | | XCH addr1 addr2 ⇒ |
---|
| 365 | match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect]] x) → ? with |
---|
[316] | 366 | [ REGISTER r ⇒ λ_. |
---|
| 367 | [ ([[true;true;false;false;true]]) @@ r ] |
---|
[299] | 368 | | DIRECT b1 ⇒ λ_. |
---|
| 369 | [ ([[true;true;false;false;false;true;false;true]]); b1] |
---|
| 370 | | INDIRECT i1 ⇒ λ_. |
---|
| 371 | [ ([[true;true;false;false;false;true;true;i1]]) ] |
---|
| 372 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
| 373 | | XCHD addr1 addr2 ⇒ |
---|
| 374 | match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with |
---|
| 375 | [ INDIRECT i1 ⇒ λ_. |
---|
| 376 | [ ([[true;true;false;true;false;true;true;i1]]) ] |
---|
| 377 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
[300] | 378 | | XRL addrs ⇒ |
---|
| 379 | match addrs with |
---|
| 380 | [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
| 381 | match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with |
---|
[316] | 382 | [ REGISTER r ⇒ λ_. |
---|
| 383 | [ ([[false;true;true;false;true]]) @@ r ] |
---|
[300] | 384 | | DIRECT b1 ⇒ λ_. |
---|
| 385 | [ ([[false;true;true;false;false;true;false;true]]); b1] |
---|
| 386 | | INDIRECT i1 ⇒ λ_. |
---|
| 387 | [ ([[false;true;true;false;false;true;true;i1]]) ] |
---|
| 388 | | DATA b1 ⇒ λ_. |
---|
| 389 | [ ([[false;true;true;false;false;true;false;false]]); b1] |
---|
| 390 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
| 391 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
| 392 | let b1 ≝ |
---|
| 393 | match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with |
---|
| 394 | [ DIRECT b1 ⇒ λ_. b1 |
---|
| 395 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in |
---|
| 396 | match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with |
---|
| 397 | [ ACC_A ⇒ λ_. |
---|
| 398 | [ ([[false;true;true;false;false;false;true;false]]); b1 ] |
---|
| 399 | | DATA b2 ⇒ λ_. |
---|
| 400 | [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ] |
---|
[307] | 401 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]]. |
---|
[298] | 402 | |
---|
[410] | 403 | include "Arithmetic.ma". |
---|
| 404 | include "Fetch.ma". |
---|
| 405 | include "Status.ma". |
---|
| 406 | |
---|
[419] | 407 | ndefinition assembly_jump: ? → (jump ?) → (? → [[relative]]) → instruction ≝ |
---|
| 408 | λA: Type[0]. |
---|
| 409 | λj: jump A. |
---|
| 410 | λaddr_of: A → [[relative]]. |
---|
[410] | 411 | match j with |
---|
[419] | 412 | [ JC jmp ⇒ Jump [[relative]] (JC ? (addr_of jmp)) |
---|
| 413 | | JNC jmp ⇒ Jump ? (JNC ? (addr_of jmp)) |
---|
| 414 | | JZ jmp ⇒ Jump ? (JZ ? (addr_of jmp)) |
---|
| 415 | | JNZ jmp ⇒ Jump ? (JNZ ? (addr_of jmp)) |
---|
| 416 | | JB jmp jmp' ⇒ Jump ? (JB ? jmp (addr_of jmp')) |
---|
| 417 | | JNB jmp jmp' ⇒ Jump ? (JNB ? jmp (addr_of jmp')) |
---|
| 418 | | JBC jmp jmp' ⇒ Jump ? (JBC ? jmp (addr_of jmp')) |
---|
| 419 | | CJNE jmp jmp' ⇒ Jump ? (CJNE ? jmp (addr_of jmp')) |
---|
| 420 | | DJNZ jmp jmp' ⇒ Jump ? (DJNZ ? jmp (addr_of jmp')) |
---|
[410] | 421 | ]. |
---|
| 422 | |
---|
[419] | 423 | ndefinition address_of: BitVectorTrie (BitVector eight) eight → String → addressing_mode ≝ |
---|
| 424 | λmap: BitVectorTrie (BitVector eight) eight. |
---|
| 425 | λstring: String. |
---|
[418] | 426 | let address ≝ lookup … (bitvector_of_string … string) map (zero ?) in |
---|
| 427 | let address_bv ≝ nat_of_bitvector ? address in |
---|
| 428 | if less_than_b address_bv two_hundred_and_fifty_six then |
---|
| 429 | RELATIVE address |
---|
| 430 | else |
---|
| 431 | ?. |
---|
| 432 | nelim not_implemented. |
---|
| 433 | nqed. |
---|
| 434 | |
---|
[410] | 435 | ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie ? sixteen)) ≝ |
---|
| 436 | λp. |
---|
| 437 | let 〈preamble, instr_list〉 ≝ p in |
---|
| 438 | let 〈datalabels, ignore〉 ≝ |
---|
| 439 | fold_left ? ? ( |
---|
| 440 | λt. λpreamble. |
---|
| 441 | let 〈datalabels, addr〉 ≝ t in |
---|
| 442 | let 〈name, size〉 ≝ preamble in |
---|
| 443 | let addr_sixteen ≝ bitvector_of_nat sixteen addr in |
---|
[414] | 444 | 〈insert ? ? (bitvector_of_string ? name) addr_sixteen datalabels, addr + size〉) |
---|
[410] | 445 | 〈(Stub ? ?), Z〉 preamble in |
---|
| 446 | let 〈pc_labels, costs〉 ≝ |
---|
| 447 | fold_left ? ? ( |
---|
| 448 | λt. λi. |
---|
| 449 | let 〈pc_labels, costs〉 ≝ t in |
---|
| 450 | let 〈program_counter, labels〉 ≝ pc_labels in |
---|
| 451 | match i with |
---|
| 452 | [ Instruction instr ⇒ |
---|
| 453 | let code_memory ≝ load_code_memory (assembly1 instr) in |
---|
[414] | 454 | let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in |
---|
[410] | 455 | let 〈instr', program_counter'〉 ≝ instr_pc' in |
---|
| 456 | let program_counter_n' ≝ nat_of_bitvector ? program_counter' in |
---|
| 457 | 〈〈program_counter + program_counter_n', labels〉, costs〉 |
---|
| 458 | | Label label ⇒ |
---|
[419] | 459 | let program_counter_bv ≝ bitvector_of_nat ? program_counter in |
---|
| 460 | 〈〈program_counter, (insert ? ? (bitvector_of_string eight label) program_counter_bv labels)〉, costs〉 |
---|
[410] | 461 | | Cost cost ⇒ |
---|
[419] | 462 | let program_counter_bv ≝ bitvector_of_nat ? program_counter in |
---|
[410] | 463 | 〈pc_labels, (insert ? ? program_counter_bv cost costs)〉 |
---|
| 464 | | Jmp jmp ⇒ |
---|
| 465 | 〈〈program_counter + three, labels〉, costs〉 |
---|
| 466 | | Call call ⇒ |
---|
| 467 | 〈〈program_counter + three, labels〉, costs〉 |
---|
| 468 | | Mov dptr trgt ⇒ t |
---|
[419] | 469 | | WithLabel jmp ⇒ |
---|
[410] | 470 | let fake_addr ≝ RELATIVE (zero eight) in |
---|
[419] | 471 | let fake_jump ≝ assembly_jump ? jmp (λx. fake_addr) in |
---|
| 472 | let code_memory ≝ load_code_memory (assembly1 fake_jump) in |
---|
| 473 | let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in |
---|
[410] | 474 | let 〈instr', program_counter'〉 ≝ instr_pc' in |
---|
| 475 | let program_counter_n' ≝ nat_of_bitvector ? program_counter' in |
---|
[419] | 476 | 〈〈program_counter + program_counter_n', labels〉, costs〉 |
---|
[410] | 477 | ] |
---|
| 478 | ) 〈〈Z, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in |
---|
| 479 | let 〈program_counter, labels〉 ≝ pc_labels in |
---|
| 480 | if greater_than_b program_counter |
---|
| 481 | sixty_five_thousand_five_hundred_and_thirty_six then |
---|
| 482 | Nothing ? |
---|
| 483 | else |
---|
| 484 | let flat_list ≝ |
---|
| 485 | flatten ? ( |
---|
| 486 | map ? ? ( |
---|
| 487 | λi: labelled_instruction. |
---|
| 488 | match i with |
---|
| 489 | [ Cost cost ⇒ [ ] |
---|
| 490 | | Label label ⇒ [ ] |
---|
| 491 | | Call call ⇒ |
---|
| 492 | let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in |
---|
[419] | 493 | let pc_offset_pad ≝ (zero eight) @@ pc_offset in |
---|
| 494 | let address ≝ ADDR16 pc_offset_pad in |
---|
[414] | 495 | assembly1 (LCALL ? address) |
---|
| 496 | | Mov d trgt ⇒ |
---|
| 497 | let pc_offset ≝ lookup ? ? (bitvector_of_string ? trgt) datalabels (zero ?) in |
---|
| 498 | let address ≝ DATA16 pc_offset in |
---|
[418] | 499 | assembly1 (MOV ? (? ? ? ? 〈DPTR, address〉)) |
---|
| 500 | | Instruction instr ⇒ assembly1 instr |
---|
| 501 | | Jmp jmp ⇒ |
---|
[414] | 502 | let pc_offset ≝ lookup ? ? (bitvector_of_string ? jmp) labels (zero ?) in |
---|
[419] | 503 | let pc_offset_pad ≝ (zero eight) @@ pc_offset in |
---|
| 504 | let address ≝ ADDR16 pc_offset_pad in |
---|
[414] | 505 | assembly1 (LJMP ? address) |
---|
[419] | 506 | | WithLabel jmp ⇒ |
---|
| 507 | assembly1 (assembly_jump ? jmp (address_of labels)) |
---|
[410] | 508 | ] |
---|
| 509 | ) instr_list |
---|
| 510 | ) in |
---|
| 511 | Just ? 〈flat_list, costs〉. |
---|
| 512 | |
---|
[300] | 513 | (* |
---|
[307] | 514 | let load_code_memory = fold_lefti (fun i mem v -> WordMap.add (vect_of_int i `Sixteen) v mem) WordMap.empty |
---|
[264] | 515 | |
---|
[307] | 516 | let load_mem mem status = { status with code_memory = mem } |
---|
| 517 | let load l = load_mem (load_code_memory l) |
---|
[264] | 518 | |
---|
[307] | 519 | module StringMap = Map.Make(String);; |
---|
| 520 | module IntMap = Map.Make(struct type t = int let compare = compare end);; |
---|
[264] | 521 | |
---|
| 522 | |
---|
[307] | 523 | let assembly_jump addr_of = |
---|
| 524 | function |
---|
| 525 | `JC a1 -> `JC (addr_of a1) |
---|
| 526 | | `JNC a1 -> `JNC (addr_of a1) |
---|
| 527 | | `JB (a1,a2) -> `JB (a1,addr_of a2) |
---|
| 528 | | `JNB (a1,a2) -> `JNB (a1,addr_of a2) |
---|
| 529 | | `JBC (a1,a2) -> `JBC (a1,addr_of a2) |
---|
| 530 | | `JZ a1 -> `JZ (addr_of a1) |
---|
| 531 | | `JNZ a1 -> `JNZ (addr_of a1) |
---|
| 532 | | `CJNE (a1,a2) -> `CJNE (a1,addr_of a2) |
---|
| 533 | | `DJNZ (a1,a2) -> `DJNZ (a1,addr_of a2) |
---|
| 534 | ;; |
---|
[264] | 535 | |
---|
[307] | 536 | let assembly (preamble,l) = |
---|
| 537 | let datalabels,_ = |
---|
| 538 | List.fold_left |
---|
| 539 | (fun (datalabels,addr) (name,size) -> |
---|
| 540 | let addr16 = vect_of_int addr `Sixteen in |
---|
| 541 | StringMap.add name addr16 datalabels, addr+size |
---|
| 542 | ) (StringMap.empty,0) preamble |
---|
| 543 | in |
---|
| 544 | let pc,labels,costs = |
---|
| 545 | List.fold_left |
---|
| 546 | (fun (pc,labels,costs) i -> |
---|
| 547 | match i with |
---|
| 548 | `Label s -> pc, StringMap.add s pc labels, costs |
---|
| 549 | | `Cost s -> pc, labels, IntMap.add pc s costs |
---|
| 550 | | `Mov (_,_) -> pc, labels, costs |
---|
| 551 | | `Jmp _ |
---|
| 552 | | `Call _ -> pc + 3, labels, costs (*CSC: very stupid: always expand to worst opcode *) |
---|
| 553 | | `WithLabel i -> |
---|
| 554 | let fake_addr _ = `REL (zero `Eight) in |
---|
| 555 | let fake_jump = assembly_jump fake_addr i in |
---|
| 556 | let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in |
---|
| 557 | assert (fake_jump = i'); |
---|
| 558 | (pc + int_of_vect pc',labels, costs) |
---|
| 559 | | #instruction as i -> |
---|
| 560 | let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in |
---|
| 561 | assert (i = i'); |
---|
| 562 | (pc + int_of_vect pc',labels, costs) |
---|
| 563 | ) (0,StringMap.empty,IntMap.empty) l |
---|
| 564 | in |
---|
| 565 | if pc >= 65536 then |
---|
| 566 | raise CodeTooLarge |
---|
| 567 | else |
---|
| 568 | List.flatten (List.map |
---|
| 569 | (function |
---|
| 570 | `Label _ |
---|
| 571 | | `Cost _ -> [] |
---|
| 572 | | `WithLabel i -> |
---|
| 573 | let addr_of (`Label s) = |
---|
| 574 | let addr = StringMap.find s labels in |
---|
| 575 | (* NOT IMPLEMENTED YET; NEEDS SMART ALGORITHM *) |
---|
| 576 | assert (addr < 256); |
---|
| 577 | `REL (vect_of_int addr `Eight) |
---|
| 578 | in |
---|
| 579 | assembly1 (assembly_jump addr_of i) |
---|
| 580 | | `Mov (`DPTR,s) -> |
---|
| 581 | let addrr16 = StringMap.find s datalabels in |
---|
| 582 | assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16))) |
---|
| 583 | | `Jmp s -> |
---|
| 584 | let pc_offset = StringMap.find s labels in |
---|
| 585 | assembly1 (`LJMP (`ADDR16 (vect_of_int pc_offset `Sixteen))) |
---|
| 586 | | `Call s -> |
---|
| 587 | let pc_offset = StringMap.find s labels in |
---|
| 588 | assembly1 (`LCALL (`ADDR16 (vect_of_int pc_offset `Sixteen))) |
---|
| 589 | | #instruction as i -> assembly1 i) l), costs |
---|
| 590 | ;; |
---|
[304] | 591 | *) |
---|
[341] | 592 | |
---|
| 593 | ndefinition assembly: List instruction → List Byte ≝ |
---|
| 594 | fold_right … (λi,l. assembly1 i @ l) []. |
---|