Changeset 820
 Timestamp:
 May 20, 2011, 6:09:00 PM (9 years ago)
 Location:
 src/ASM
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASM.ma
r757 r820 112 112 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?. 113 113 114 inductive jump (A: Type[0]): Type[0] ≝115 JC: A → jump A116  JNC: A → jump A117  JB: [[bit_addr]] → A → jump A118  JNB: [[bit_addr]] → A → jump A119  JBC: [[bit_addr]] → A → jump A120  JZ: A → jump A121  JNZ: A → jump A122  CJNE:123 [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → jump A124  DJNZ: [[registr ; direct]] → A → jump A.125 126 114 inductive preinstruction (A: Type[0]) : Type[0] ≝ 127 115 ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A … … 134 122  DA: [[acc_a]] → preinstruction A 135 123 124 (* conditional jumps *) 125  JC: A → preinstruction A 126  JNC: A → preinstruction A 127  JB: [[bit_addr]] → A → preinstruction A 128  JNB: [[bit_addr]] → A → preinstruction A 129  JBC: [[bit_addr]] → A → preinstruction A 130  JZ: A → preinstruction A 131  JNZ: A → preinstruction A 132  CJNE: 133 [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A 134  DJNZ: [[registr ; direct]] → A → preinstruction A 136 135 (* logical operations *) 137 136  ANL: … … 162 161 [[carry]] × [[bit_addr]] ⊎ 163 162 [[bit_addr]] × [[carry]] → preinstruction A 164  MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → preinstruction A165 163  MOVX: 166 164 [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎ … … 173 171 174 172 (* program branching *) 175  Jump: jump A → preinstruction A176  ACALL: [[addr11]] → preinstruction A177  LCALL: [[addr16]] → preinstruction A178 173  RET: preinstruction A 179 174  RETI: preinstruction A 180  AJMP: [[addr11]] → preinstruction A181  LJMP: [[addr16]] → preinstruction A182  SJMP: [[relative]] → preinstruction A183  JMP: [[indirect_dptr]] → preinstruction A184 175  NOP: preinstruction A. 185 176 186 definition instruction ≝ preinstruction [[relative]]. 177 inductive instruction: Type[0] ≝ 178  ACALL: [[addr11]] → instruction 179  LCALL: [[addr16]] → instruction 180  AJMP: [[addr11]] → instruction 181  LJMP: [[addr16]] → instruction 182  SJMP: [[relative]] → instruction 183  JMP: [[indirect_dptr]] → instruction 184  MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction 185  RealInstruction: preinstruction [[ relative ]] → instruction. 186 187 coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝ 188 RealInstruction on _p: preinstruction ? to instruction. 187 189 188 190 inductive pseudo_instruction: Type[0] ≝ 189 Instruction: instruction → pseudo_instruction 190  Comment: String → pseudo_instruction 191  Cost: Identifier → pseudo_instruction 192  Jmp: Identifier → pseudo_instruction 193  Call: Identifier → pseudo_instruction 194  Mov: [[dptr]] → Identifier → pseudo_instruction 195  WithLabel: jump Identifier → pseudo_instruction. 191  Instruction: preinstruction Identifier → pseudo_instruction 192  Comment: String → pseudo_instruction 193  Cost: Identifier → pseudo_instruction 194  Jmp: Identifier → pseudo_instruction 195  Call: Identifier → pseudo_instruction 196  Mov: [[dptr]] → Identifier → pseudo_instruction. 196 197 197 198 definition labelled_instruction ≝ option Identifier × pseudo_instruction. 198 199 199 definition preamble ≝ list (Identifier × nat). 200 201 definition assembly_program ≝ preamble × (list labelled_instruction).200 definition assembly_program ≝ list instruction. 201 definition pseudo_assembly_program ≝ preamble × (list labelled_instruction). 
src/ASM/Assembly.ma
r757 r820 5 5 include "ASM/Status.ma". 6 6 7 definition assembly1 ≝ 8 λi: instruction. 9 match i with 10 [ ACALL addr ⇒ 11 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 12 [ ADDR11 w ⇒ λ_. 13 let 〈v1,v2〉 ≝ split ? 3 8 w in 14 [ (v1 @@ [[true; false; false; false; true]]) ; v2 ] 15  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 16  ADD addr1 addr2 ⇒ 7 definition assembly_preinstruction ≝ 8 λA: Type[0]. 9 λaddr_of: A → Byte. (* relative *) 10 λpre: preinstruction A. 11 match pre with 12 [ ADD addr1 addr2 ⇒ 17 13 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with 18 14 [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ] … … 28 24  DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ] 29 25  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 30  AJMP addr ⇒31 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with32 [ ADDR11 w ⇒ λ_.33 let 〈v1,v2〉 ≝ split ? 3 8 w in34 [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]35  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)36 26  ANL addrs ⇒ 37 27 match addrs with … … 90 80 [ ([[false; false; false; true; false; true; true; i1]]) ] 91 81  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 92  DIV addr1 addr2 ⇒ 93 [ ([[true;false;false;false;false;true;false;false]]) ] 94  Jump j ⇒ 95 match j with 96 [ DJNZ addr1 addr2 ⇒ 97 let b2 ≝ 98 match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 99 [ RELATIVE b2 ⇒ λ_. b2 100  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 82  DJNZ addr1 addr2 ⇒ 83 let b2 ≝ addr_of addr2 in 101 84 match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with 102 85 [ REGISTER r ⇒ λ_. … … 106 89  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 107 90  JC addr ⇒ 108 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 109 [ RELATIVE b1 ⇒ λ_. 110 [ ([[false; true; false; false; false; false; false; false]]); b1 ] 111  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 91 let b1 ≝ addr_of addr in 92 [ ([[false; true; false; false; false; false; false; false]]); b1 ] 112 93  JNC addr ⇒ 113 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 114 [ RELATIVE b1 ⇒ λ_. 115 [ ([[false; true; false; true; false; false; false; false]]); b1 ] 116  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 94 let b1 ≝ addr_of addr in 95 [ ([[false; true; false; true; false; false; false; false]]); b1 ] 117 96  JZ addr ⇒ 118 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 119 [ RELATIVE b1 ⇒ λ_. 120 [ ([[false; true; true; false; false; false; false; false]]); b1 ] 121  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 97 let b1 ≝ addr_of addr in 98 [ ([[false; true; true; false; false; false; false; false]]); b1 ] 122 99  JNZ addr ⇒ 123 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 124 [ RELATIVE b1 ⇒ λ_. 125 [ ([[false; true; true; true; false; false; false; false]]); b1 ] 126  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 100 let b1 ≝ addr_of addr in 101 [ ([[false; true; true; true; false; false; false; false]]); b1 ] 127 102  JB addr1 addr2 ⇒ 128 let b2 ≝ 129 match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 130 [ RELATIVE b2 ⇒ λ_. b2 131  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 103 let b2 ≝ addr_of addr2 in 132 104 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 133 105 [ BIT_ADDR b1 ⇒ λ_. … … 135 107  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 136 108  JNB addr1 addr2 ⇒ 137 let b2 ≝ 138 match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 139 [ RELATIVE b2 ⇒ λ_. b2 140  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 109 let b2 ≝ addr_of addr2 in 141 110 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 142 111 [ BIT_ADDR b1 ⇒ λ_. … … 144 113  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 145 114  JBC addr1 addr2 ⇒ 146 let b2 ≝ 147 match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 148 [ RELATIVE b2 ⇒ λ_. b2 149  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 115 let b2 ≝ addr_of addr2 in 150 116 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 151 117 [ BIT_ADDR b1 ⇒ λ_. … … 153 119  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 154 120  CJNE addrs addr3 ⇒ 155 let b3 ≝ 156 match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 157 [ RELATIVE b3 ⇒ λ_. b3 158  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in 121 let b3 ≝ addr_of addr3 in 159 122 match addrs with 160 123 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in … … 171 134  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 172 135 match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with 173 [ REGISTER r ⇒ λ_.136 [ REGISTER r ⇒ λ_. 174 137 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ] 175 138  INDIRECT i1 ⇒ λ_. 176 139 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ] 177  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) ]] 140  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 141 ] 142  DIV addr1 addr2 ⇒ 143 [ ([[true;false;false;false;false;true;false;false]]) ] 178 144  INC addr ⇒ 179 145 match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with … … 188 154  DPTR ⇒ λ_. 189 155 [ ([[true;false;true;false;false;false;true;true]]) ] 190  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)191  JMP addr ⇒192 [ ([[false;true;true;true;false;false;true;true]]) ]193  LCALL addr ⇒194 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with195 [ ADDR16 w ⇒ λ_.196 let 〈b1,b2〉 ≝ split ? 8 8 w in197 [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]198  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)199  LJMP addr ⇒200 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with201 [ ADDR16 w ⇒ λ_.202 let 〈b1,b2〉 ≝ split ? 8 8 w in203 [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]204 156  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 205 157  MOV addrs ⇒ … … 263 215 [ ([[true;false;false;true;false;false;true;false]]); b1 ] 264 216  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)] 265  MOVC addr1 addr2 ⇒266 match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with267 [ ACC_DPTR ⇒ λ_.268 [ ([[true;false;false;true;false;false;true;true]]) ]269  ACC_PC ⇒ λ_.270 [ ([[true;false;false;false;false;false;true;true]]) ]271  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)272 217  MOVX addrs ⇒ 273 218 match addrs with … … 348 293 [ ([[true;true;false;true;false;false;true;false]]); b1 ] 349 294  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 350  SJMP addr ⇒351 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with352 [ RELATIVE b1 ⇒ λ_.353 [ ([[true;false;false;false;false;false;false;false]]); b1 ]354  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)355 295  SUBB addr1 addr2 ⇒ 356 296 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with … … 403 343  DATA b2 ⇒ λ_. 404 344 [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ] 405  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]]. 406 407 definition assembly_jump: (jump Identifier) → (Identifier → [[relative]]) → instruction ≝ 408 λj: jump Identifier. 409 λaddr_of: Identifier → [[relative]]. 410 match j with 411 [ JC jmp ⇒ Jump ? (JC ? (addr_of jmp)) 412  JNC jmp ⇒ Jump ? (JNC ? (addr_of jmp)) 413  JZ jmp ⇒ Jump ? (JZ ? (addr_of jmp)) 414  JNZ jmp ⇒ Jump ? (JNZ ? (addr_of jmp)) 415  JB jmp jmp' ⇒ Jump ? (JB ? jmp (addr_of jmp')) 416  JNB jmp jmp' ⇒ Jump ? (JNB ? jmp (addr_of jmp')) 417  JBC jmp jmp' ⇒ Jump ? (JBC ? jmp (addr_of jmp')) 418  CJNE jmp jmp' ⇒ Jump ? (CJNE ? jmp (addr_of jmp')) 419  DJNZ jmp jmp' ⇒ Jump ? (DJNZ ? jmp (addr_of jmp')) 420 ]. 345  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 346 ]. 421 347 422 definition address_of: BitVectorTrie Word 16 → Identifier → addressing_mode ≝ 348 definition assembly1 ≝ 349 λi: instruction. 350 match i with 351 [ ACALL addr ⇒ 352 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 353 [ ADDR11 w ⇒ λ_. 354 let 〈v1,v2〉 ≝ split ? 3 8 w in 355 [ (v1 @@ [[true; false; false; false; true]]) ; v2 ] 356  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 357  AJMP addr ⇒ 358 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 359 [ ADDR11 w ⇒ λ_. 360 let 〈v1,v2〉 ≝ split ? 3 8 w in 361 [ (v1 @@ [[false; false; false; false; true]]) ; v2 ] 362  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 363  JMP adptr ⇒ 364 [ ([[false;true;true;true;false;false;true;true]]) ] 365  LCALL addr ⇒ 366 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 367 [ ADDR16 w ⇒ λ_. 368 let 〈b1,b2〉 ≝ split ? 8 8 w in 369 [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ] 370  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 371  LJMP addr ⇒ 372 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 373 [ ADDR16 w ⇒ λ_. 374 let 〈b1,b2〉 ≝ split ? 8 8 w in 375 [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ] 376  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 377  MOVC addr1 addr2 ⇒ 378 match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with 379 [ ACC_DPTR ⇒ λ_. 380 [ ([[true;false;false;true;false;false;true;true]]) ] 381  ACC_PC ⇒ λ_. 382 [ ([[true;false;false;false;false;false;true;true]]) ] 383  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 384  SJMP addr ⇒ 385 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 386 [ RELATIVE b1 ⇒ λ_. 387 [ ([[true;false;false;false;false;false;false;false]]); b1 ] 388  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 389  RealInstruction instr ⇒ 390 assembly_preinstruction [[ relative ]] 391 (λx. 392 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with 393 [ RELATIVE r ⇒ λ_. r 394  _ ⇒ λabsd. ⊥ 395 ] (subaddressing_modein … x)) instr 396 ]. 397 cases absd 398 qed. 399 400 definition address_of: BitVectorTrie Word 16 → Identifier → Byte ≝ 423 401 λmap. 424 402 λid: Identifier. … … 426 404 let 〈high, low〉 ≝ split ? 8 8 address in 427 405 if eq_bv ? high (zero ?) then 428 RELATIVElow406 low 429 407 else 430 408 ?. … … 432 410 qed. 433 411 434 definition assembly: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝412 definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 435 413 λp. 436 414 let 〈preamble, instr_list〉 ≝ p in … … 458 436 match i with 459 437 [ Instruction instr ⇒ 460 let code_memory ≝ load_code_memory (assembly 1instr) in438 let code_memory ≝ load_code_memory (assembly_preinstruction Identifier (λx. zero 8) instr) in 461 439 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in 462 440 let 〈instr', program_counter'〉 ≝ instr_pc' in … … 472 450 〈program_counter + 3, costs〉 473 451  Mov dptr trgt ⇒ pc_costs 474  WithLabel jmp ⇒475 let fake_addr ≝ RELATIVE (zero 8) in476 let fake_jump ≝ assembly_jump jmp (λx: Identifier. fake_addr) in477 let code_memory ≝ load_code_memory (assembly1 fake_jump) in478 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in479 let 〈instr', program_counter'〉 ≝ instr_pc' in480 let program_counter_n' ≝ nat_of_bitvector 16 program_counter' in481 〈program_counter + program_counter_n', costs〉482 452 ]〉 483 453 ) 〈(Stub ? ?), 〈0,(Stub ? ?)〉〉 instr_list in … … 496 466 let pc_offset ≝ lookup ? ? call labels (zero ?) in 497 467 let address ≝ ADDR16 pc_offset in 498 assembly1 (LCALL ?address)468 assembly1 (LCALL address) 499 469  Mov d trgt ⇒ 500 470 let pc_offset ≝ lookup ? ? trgt datalabels (zero ?) in 501 471 let address ≝ DATA16 pc_offset in 502 472 assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉)))) 503  Instruction instr ⇒ assembly 1instr473  Instruction instr ⇒ assembly_preinstruction ? (address_of labels) instr 504 474  Jmp jmp ⇒ 505 475 let pc_offset ≝ lookup ? ? jmp labels (zero ?) in 506 476 let address ≝ ADDR16 pc_offset in 507 assembly1 (LJMP ? address) 508  WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels)) 477 assembly1 (LJMP address) 478 (*  WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels)) 479 *) 509 480 ] 510 481 ) instr_list … … 514 485 normalize; %; 515 486  whd in ⊢ (? (? ? ? %)); 516 cases (split bool 8 8 (lookup Word 16 c0labels (zero 16)))487 cases (split bool 8 8 (lookup Word 16 trgt labels (zero 16))) 517 488 # high 518 489 # low … … 526 497 qed. 527 498 528 definition assembly_unlabelled_program: list instruction→ option (list Byte × (BitVectorTrie Identifier 16)) ≝499 definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 529 500 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉). 530 501 
src/ASM/Fetch.ma
r712 r820 20 20 let 〈b,v〉 ≝ head … v in if b then 21 21 let 〈b,v〉 ≝ head … v in if b then 22 〈〈 MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉))))), pc〉, 1〉23 else 24 let 〈b,v〉≝ head … v in if b then 25 let 〈b,v〉≝ head … v in if b then 26 〈〈 MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉))))), pc〉, 1〉27 else 28 let 〈b,v〉≝ head … v in if b then 29 let 〈pc,b1〉≝ next pmem pc in 〈〈 MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉)))), pc〉, 1〉22 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉 23 else 24 let 〈b,v〉≝ head … v in if b then 25 let 〈b,v〉≝ head … v in if b then 26 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉 27 else 28 let 〈b,v〉≝ head … v in if b then 29 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉 30 30 else 31 31 〈〈CPL … ACC_A, pc〉, 1〉 32 32 else 33 33 let 〈b,v〉≝ head … v in if b then 34 〈〈 MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉), pc〉, 2〉34 〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉 35 35 else 36 36 let 〈b,v〉≝ head … v in if b then 37 37 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 38 38 else 39 〈〈 MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉), pc〉, 2〉40 else 41 let 〈b,v〉≝ head … v in if b then 42 〈〈 MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉))))), pc〉, 1〉43 else 44 let 〈b,v〉≝ head … v in if b then 45 let 〈b,v〉≝ head … v in if b then 46 〈〈 MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))))), pc〉, 1〉47 else 48 let 〈b,v〉≝ head … v in if b then 49 let 〈pc,b1〉≝ next pmem pc in 〈〈 MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉))))), pc〉, 1〉50 else 51 〈〈 CLR … ACC_A, pc〉, 1〉52 else 53 let 〈b,v〉≝ head … v in if b then 54 〈〈 MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉), pc〉, 2〉39 〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉 40 else 41 let 〈b,v〉≝ head … v in if b then 42 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉 43 else 44 let 〈b,v〉≝ head … v in if b then 45 let 〈b,v〉≝ head … v in if b then 46 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉 47 else 48 let 〈b,v〉≝ head … v in if b then 49 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉 50 else 51 〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉 52 else 53 let 〈b,v〉≝ head … v in if b then 54 〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉 55 55 else 56 56 let 〈b,v〉≝ head … v in if b then 57 57 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 58 58 else 59 〈〈 MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉), pc〉, 2〉59 〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉 60 60 else 61 61 let 〈b,v〉≝ head … v in if b then 62 62 let 〈b,v〉≝ head … v in if b then 63 let 〈pc,b1〉≝ next pmem pc in 〈〈 Jump [[relative]](DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉64 else 65 let 〈b,v〉≝ head … v in if b then 66 let 〈b,v〉≝ head … v in if b then 67 〈〈 XCHD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉68 else 69 let 〈b,v〉≝ head … v in if b then 70 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 Jump [[relative]](DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉71 else 72 〈〈 DA … ACC_A, pc〉, 1〉73 else 74 let 〈b,v〉≝ head … v in if b then 75 let 〈b,v〉≝ head … v in if b then 76 〈〈 SETB … CARRY, pc〉, 1〉77 else 78 let 〈pc,b1〉≝ next pmem pc in 〈〈 SETB … (BIT_ADDR b1), pc〉, 1〉63 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉 64 else 65 let 〈b,v〉≝ head … v in if b then 66 let 〈b,v〉≝ head … v in if b then 67 〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉 68 else 69 let 〈b,v〉≝ head … v in if b then 70 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉 71 else 72 〈〈RealInstruction (DA … ACC_A), pc〉, 1〉 73 else 74 let 〈b,v〉≝ head … v in if b then 75 let 〈b,v〉≝ head … v in if b then 76 〈〈RealInstruction (SETB … CARRY), pc〉, 1〉 77 else 78 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉 79 79 else 80 80 let 〈b,v〉≝ head … v in if b then 81 81 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 82 82 else 83 let 〈pc,b1〉≝ next pmem pc in 〈〈 POP … (DIRECT b1), pc〉, 2〉84 else 85 let 〈b,v〉≝ head … v in if b then 86 〈〈 XCH … ACC_A (REGISTER v), pc〉, 1〉87 else 88 let 〈b,v〉≝ head … v in if b then 89 let 〈b,v〉≝ head … v in if b then 90 〈〈 XCH … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉91 else 92 let 〈b,v〉≝ head … v in if b then 93 let 〈pc,b1〉≝ next pmem pc in 〈〈 XCH … ACC_A (DIRECT b1), pc〉, 1〉94 else 95 〈〈 SWAP … ACC_A, pc〉, 1〉96 else 97 let 〈b,v〉≝ head … v in if b then 98 let 〈b,v〉≝ head … v in if b then 99 〈〈 CLR … CARRY, pc〉, 1〉100 else 101 let 〈pc,b1〉≝ next pmem pc in 〈〈 CLR … (BIT_ADDR b1), pc〉, 1〉83 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉 84 else 85 let 〈b,v〉≝ head … v in if b then 86 〈〈RealInstruction (XCH … ACC_A (REGISTER v)), pc〉, 1〉 87 else 88 let 〈b,v〉≝ head … v in if b then 89 let 〈b,v〉≝ head … v in if b then 90 〈〈RealInstruction (XCH … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉 91 else 92 let 〈b,v〉≝ head … v in if b then 93 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉 94 else 95 〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉 96 else 97 let 〈b,v〉≝ head … v in if b then 98 let 〈b,v〉≝ head … v in if b then 99 〈〈RealInstruction (CLR … CARRY), pc〉, 1〉 100 else 101 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉 102 102 else 103 103 let 〈b,v〉≝ head … v in if b then 104 104 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 105 105 else 106 let 〈pc,b1〉≝ next pmem pc in 〈〈 PUSH … (DIRECT b1), pc〉, 2〉106 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉 107 107 else 108 108 let 〈b,v〉≝ head … v in if b then 109 109 let 〈b,v〉≝ head … v in if b then 110 110 let 〈b,v〉≝ head … v in if b then 111 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 Jump [[relative]](CJNE … (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉112 else 113 let 〈b,v〉≝ head … v in if b then 114 let 〈b,v〉≝ head … v in if b then 115 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 Jump [[relative]](CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉116 else 117 let 〈b,v〉≝ head … v in if b then 118 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 Jump [[relative]](CJNE … (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉119 else 120 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 Jump [[relative]](CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉121 else 122 let 〈b,v〉≝ head … v in if b then 123 let 〈b,v〉≝ head … v in if b then 124 〈〈 CPL … CARRY, pc〉, 1〉125 else 126 let 〈pc,b1〉≝ next pmem pc in 〈〈 CPL … (BIT_ADDR b1), pc〉, 1〉111 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE … (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 112 else 113 let 〈b,v〉≝ head … v in if b then 114 let 〈b,v〉≝ head … v in if b then 115 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉 116 else 117 let 〈b,v〉≝ head … v in if b then 118 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉 119 else 120 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 121 else 122 let 〈b,v〉≝ head … v in if b then 123 let 〈b,v〉≝ head … v in if b then 124 〈〈RealInstruction (CPL … CARRY), pc〉, 1〉 125 else 126 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉 127 127 else 128 128 let 〈b,v〉≝ head … v in if b then 129 129 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 130 130 else 131 let 〈pc,b1〉≝ next pmem pc in 〈〈 ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉132 else 133 let 〈b,v〉≝ head … v in if b then 134 let 〈pc,b1〉≝ next pmem pc in 〈〈 MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉))))), pc〉, 2〉135 else 136 let 〈b,v〉≝ head … v in if b then 137 let 〈b,v〉≝ head … v in if b then 138 let 〈pc,b1〉≝ next pmem pc in 〈〈 MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉))))), pc〉, 2〉139 else 140 〈〈 MUL … ACC_A ACC_B, pc〉, 4〉141 else 142 let 〈b,v〉≝ head … v in if b then 143 let 〈b,v〉≝ head … v in if b then 144 〈〈 INC … DPTR, pc〉, 2〉145 else 146 let 〈pc,b1〉≝ next pmem pc in 〈〈 MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 1〉131 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉 132 else 133 let 〈b,v〉≝ head … v in if b then 134 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉 135 else 136 let 〈b,v〉≝ head … v in if b then 137 let 〈b,v〉≝ head … v in if b then 138 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉 139 else 140 〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉 141 else 142 let 〈b,v〉≝ head … v in if b then 143 let 〈b,v〉≝ head … v in if b then 144 〈〈RealInstruction (INC … DPTR), pc〉, 2〉 145 else 146 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉 147 147 else 148 148 let 〈b,v〉≝ head … v in if b then 149 149 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 150 150 else 151 let 〈pc,b1〉≝ next pmem pc in 〈〈 ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉151 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉 152 152 else 153 153 let 〈b,v〉≝ head … v in if b then 154 154 let 〈b,v〉≝ head … v in if b then 155 〈〈 SUBB … ACC_A (REGISTER v), pc〉, 1〉156 else 157 let 〈b,v〉≝ head … v in if b then 158 let 〈b,v〉≝ head … v in if b then 159 〈〈 SUBB … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉160 else 161 let 〈b,v〉≝ head … v in if b then 162 let 〈pc,b1〉≝ next pmem pc in 〈〈 SUBB … ACC_A (DIRECT b1), pc〉, 1〉163 else 164 let 〈pc,b1〉≝ next pmem pc in 〈〈 SUBB … ACC_A (DATA b1), pc〉, 1〉155 〈〈RealInstruction (SUBB … ACC_A (REGISTER v)), pc〉, 1〉 156 else 157 let 〈b,v〉≝ head … v in if b then 158 let 〈b,v〉≝ head … v in if b then 159 〈〈RealInstruction (SUBB … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉 160 else 161 let 〈b,v〉≝ head … v in if b then 162 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉 163 else 164 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉 165 165 else 166 166 let 〈b,v〉≝ head … v in if b then … … 168 168 〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉 169 169 else 170 let 〈pc,b1〉≝ next pmem pc in 〈〈 MOV … (inr … 〈BIT_ADDR b1,CARRY〉), pc〉, 2〉170 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉 171 171 else 172 172 let 〈b,v〉≝ head … v in if b then 173 173 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 174 174 else 175 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉))), pc〉, 2〉176 else 177 let 〈b,v〉≝ head … v in if b then 178 let 〈pc,b1〉≝ next pmem pc in 〈〈 MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉)))), pc〉, 2〉179 else 180 let 〈b,v〉≝ head … v in if b then 181 let 〈b,v〉≝ head … v in if b then 182 let 〈pc,b1〉≝ next pmem pc in 〈〈 MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉)))), pc〉, 2〉183 else 184 let 〈b,v〉≝ head … v in if b then 185 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉)))), pc〉, 2〉186 else 187 〈〈 DIV … ACC_A ACC_B, pc〉, 4〉175 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉 176 else 177 let 〈b,v〉≝ head … v in if b then 178 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉 179 else 180 let 〈b,v〉≝ head … v in if b then 181 let 〈b,v〉≝ head … v in if b then 182 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉 183 else 184 let 〈b,v〉≝ head … v in if b then 185 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉 186 else 187 〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉 188 188 else 189 189 let 〈b,v〉≝ head … v in if b then … … 191 191 〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉 192 192 else 193 let 〈pc,b1〉≝ next pmem pc in 〈〈 ANL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉193 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉 194 194 else 195 195 let 〈b,v〉≝ head … v in if b then … … 202 202 let 〈b,v〉≝ head … v in if b then 203 203 let 〈b,v〉≝ head … v in if b then 204 let 〈pc,b1〉≝ next pmem pc in 〈〈 MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉))))), pc〉, 1〉205 else 206 let 〈b,v〉≝ head … v in if b then 207 let 〈b,v〉≝ head … v in if b then 208 let 〈pc,b1〉≝ next pmem pc in 〈〈 MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉))))), pc〉, 1〉209 else 210 let 〈b,v〉≝ head … v in if b then 211 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉)))), pc〉, 3〉212 else 213 let 〈pc,b1〉≝ next pmem pc in 〈〈 MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉))))), pc〉, 1〉204 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉 205 else 206 let 〈b,v〉≝ head … v in if b then 207 let 〈b,v〉≝ head … v in if b then 208 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉 209 else 210 let 〈b,v〉≝ head … v in if b then 211 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉 212 else 213 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉 214 214 else 215 215 let 〈b,v〉≝ head … v in if b then … … 217 217 〈〈JMP … INDIRECT_DPTR, pc〉, 2〉 218 218 else 219 let 〈pc,b1〉≝ next pmem pc in 〈〈 ORL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉219 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉 220 220 else 221 221 let 〈b,v〉≝ head … v in if b then 222 222 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 223 223 else 224 let 〈pc,b1〉≝ next pmem pc in 〈〈 Jump [[relative]](JNZ … (RELATIVE b1)), pc〉, 2〉225 else 226 let 〈b,v〉≝ head … v in if b then 227 〈〈 XRL … (inl … 〈ACC_A,REGISTER v〉), pc〉, 1〉228 else 229 let 〈b,v〉≝ head … v in if b then 230 let 〈b,v〉≝ head … v in if b then 231 〈〈 XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉), pc〉, 1〉232 else 233 let 〈b,v〉≝ head … v in if b then 234 let 〈pc,b1〉≝ next pmem pc in 〈〈 XRL … (inl … 〈ACC_A,DIRECT b1〉), pc〉, 1〉235 else 236 let 〈pc,b1〉≝ next pmem pc in 〈〈 XRL … (inl … 〈ACC_A,DATA b1〉), pc〉, 1〉237 else 238 let 〈b,v〉≝ head … v in if b then 239 let 〈b,v〉≝ head … v in if b then 240 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 XRL … (inr … 〈DIRECT b1,DATA b2〉), pc〉, 2〉241 else 242 let 〈pc,b1〉≝ next pmem pc in 〈〈 XRL … (inr … 〈DIRECT b1,ACC_A〉), pc〉, 1〉224 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉 225 else 226 let 〈b,v〉≝ head … v in if b then 227 〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉 228 else 229 let 〈b,v〉≝ head … v in if b then 230 let 〈b,v〉≝ head … v in if b then 231 〈〈RealInstruction (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉 232 else 233 let 〈b,v〉≝ head … v in if b then 234 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉 235 else 236 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉 237 else 238 let 〈b,v〉≝ head … v in if b then 239 let 〈b,v〉≝ head … v in if b then 240 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉 241 else 242 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉 243 243 else 244 244 let 〈b,v〉≝ head … v in if b then 245 245 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 246 246 else 247 let 〈pc,b1〉≝ next pmem pc in 〈〈 Jump [[relative]](JZ … (RELATIVE b1)), pc〉, 2〉247 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉 248 248 else 249 249 let 〈b,v〉≝ head … v in if b then 250 250 let 〈b,v〉≝ head … v in if b then 251 〈〈 ANL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉252 else 253 let 〈b,v〉≝ head … v in if b then 254 let 〈b,v〉≝ head … v in if b then 255 〈〈 ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉256 else 257 let 〈b,v〉≝ head … v in if b then 258 let 〈pc,b1〉≝ next pmem pc in 〈〈 ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉259 else 260 let 〈pc,b1〉≝ next pmem pc in 〈〈 ANL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉261 else 262 let 〈b,v〉≝ head … v in if b then 263 let 〈b,v〉≝ head … v in if b then 264 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉265 else 266 let 〈pc,b1〉≝ next pmem pc in 〈〈 ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉251 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉 252 else 253 let 〈b,v〉≝ head … v in if b then 254 let 〈b,v〉≝ head … v in if b then 255 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉 256 else 257 let 〈b,v〉≝ head … v in if b then 258 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉 259 else 260 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉 261 else 262 let 〈b,v〉≝ head … v in if b then 263 let 〈b,v〉≝ head … v in if b then 264 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉 265 else 266 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉 267 267 else 268 268 let 〈b,v〉≝ head … v in if b then 269 269 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 270 270 else 271 let 〈pc,b1〉≝ next pmem pc in 〈〈 Jump [[relative]](JNC … (RELATIVE b1)), pc〉, 2〉272 else 273 let 〈b,v〉≝ head … v in if b then 274 〈〈 ORL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉275 else 276 let 〈b,v〉≝ head … v in if b then 277 let 〈b,v〉≝ head … v in if b then 278 〈〈 ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉279 else 280 let 〈b,v〉≝ head … v in if b then 281 let 〈pc,b1〉≝ next pmem pc in 〈〈 ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉282 else 283 let 〈pc,b1〉≝ next pmem pc in 〈〈 ORL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉284 else 285 let 〈b,v〉≝ head … v in if b then 286 let 〈b,v〉≝ head … v in if b then 287 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉288 else 289 let 〈pc,b1〉≝ next pmem pc in 〈〈 ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉271 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉 272 else 273 let 〈b,v〉≝ head … v in if b then 274 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉 275 else 276 let 〈b,v〉≝ head … v in if b then 277 let 〈b,v〉≝ head … v in if b then 278 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉 279 else 280 let 〈b,v〉≝ head … v in if b then 281 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉 282 else 283 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉 284 else 285 let 〈b,v〉≝ head … v in if b then 286 let 〈b,v〉≝ head … v in if b then 287 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉 288 else 289 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉 290 290 else 291 291 let 〈b,v〉≝ head … v in if b then 292 292 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 293 293 else 294 let 〈pc,b1〉≝ next pmem pc in 〈〈 Jump [[relative]](JC … (RELATIVE b1)), pc〉, 2〉294 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉 295 295 else 296 296 let 〈b,v〉≝ head … v in if b then 297 297 let 〈b,v〉≝ head … v in if b then 298 298 let 〈b,v〉≝ head … v in if b then 299 〈〈 ADDC … ACC_A (REGISTER v), pc〉, 1〉300 else 301 let 〈b,v〉≝ head … v in if b then 302 let 〈b,v〉≝ head … v in if b then 303 〈〈 ADDC … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉304 else 305 let 〈b,v〉≝ head … v in if b then 306 let 〈pc,b1〉≝ next pmem pc in 〈〈 ADDC … ACC_A (DIRECT b1), pc〉, 1〉307 else 308 let 〈pc,b1〉≝ next pmem pc in 〈〈 ADDC … ACC_A (DATA b1), pc〉, 1〉309 else 310 let 〈b,v〉≝ head … v in if b then 311 let 〈b,v〉≝ head … v in if b then 312 〈〈R LC … ACC_A, pc〉, 1〉313 else 314 〈〈R ETI …, pc〉, 2〉299 〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉 300 else 301 let 〈b,v〉≝ head … v in if b then 302 let 〈b,v〉≝ head … v in if b then 303 〈〈RealInstruction (ADDC … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉 304 else 305 let 〈b,v〉≝ head … v in if b then 306 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉 307 else 308 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉 309 else 310 let 〈b,v〉≝ head … v in if b then 311 let 〈b,v〉≝ head … v in if b then 312 〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉 313 else 314 〈〈RealInstruction (RETI …), pc〉, 2〉 315 315 else 316 316 let 〈b,v〉≝ head … v in if b then 317 317 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 318 318 else 319 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 Jump [[relative]](JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉320 else 321 let 〈b,v〉≝ head … v in if b then 322 〈〈 ADD … ACC_A (REGISTER v), pc〉, 1〉323 else 324 let 〈b,v〉≝ head … v in if b then 325 let 〈b,v〉≝ head … v in if b then 326 〈〈 ADD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉327 else 328 let 〈b,v〉≝ head … v in if b then 329 let 〈pc,b1〉≝ next pmem pc in 〈〈 ADD … ACC_A (DIRECT b1), pc〉, 1〉330 else 331 let 〈pc,b1〉≝ next pmem pc in 〈〈 ADD … ACC_A (DATA b1), pc〉, 1〉332 else 333 let 〈b,v〉≝ head … v in if b then 334 let 〈b,v〉≝ head … v in if b then 335 〈〈R L … ACC_A, pc〉, 1〉336 else 337 〈〈R ET …, pc〉, 2〉319 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 320 else 321 let 〈b,v〉≝ head … v in if b then 322 〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉 323 else 324 let 〈b,v〉≝ head … v in if b then 325 let 〈b,v〉≝ head … v in if b then 326 〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉 327 else 328 let 〈b,v〉≝ head … v in if b then 329 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉 330 else 331 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉 332 else 333 let 〈b,v〉≝ head … v in if b then 334 let 〈b,v〉≝ head … v in if b then 335 〈〈RealInstruction (RL … ACC_A), pc〉, 1〉 336 else 337 〈〈RealInstruction (RET …), pc〉, 2〉 338 338 else 339 339 let 〈b,v〉≝ head … v in if b then 340 340 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 341 341 else 342 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 Jump [[relative]](JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉342 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 343 343 else 344 344 let 〈b,v〉≝ head … v in if b then 345 345 let 〈b,v〉≝ head … v in if b then 346 〈〈 DEC … (REGISTER v), pc〉, 1〉347 else 348 let 〈b,v〉≝ head … v in if b then 349 let 〈b,v〉≝ head … v in if b then 350 〈〈 DEC … (INDIRECT (from_singl … v)), pc〉, 1〉351 else 352 let 〈b,v〉≝ head … v in if b then 353 let 〈pc,b1〉≝ next pmem pc in 〈〈 DEC … (DIRECT b1), pc〉, 1〉354 else 355 〈〈 DEC … ACC_A, pc〉, 1〉356 else 357 let 〈b,v〉≝ head … v in if b then 358 let 〈b,v〉≝ head … v in if b then 359 〈〈R RC … ACC_A, pc〉, 1〉346 〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉 347 else 348 let 〈b,v〉≝ head … v in if b then 349 let 〈b,v〉≝ head … v in if b then 350 〈〈RealInstruction (DEC … (INDIRECT (from_singl … v))), pc〉, 1〉 351 else 352 let 〈b,v〉≝ head … v in if b then 353 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉 354 else 355 〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉 356 else 357 let 〈b,v〉≝ head … v in if b then 358 let 〈b,v〉≝ head … v in if b then 359 〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉 360 360 else 361 361 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉 … … 364 364 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 365 365 else 366 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 Jump [[relative]](JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉367 else 368 let 〈b,v〉≝ head … v in if b then 369 〈〈 INC … (REGISTER v), pc〉, 1〉370 else 371 let 〈b,v〉≝ head … v in if b then 372 let 〈b,v〉≝ head … v in if b then 373 〈〈 INC … (INDIRECT (from_singl … v)), pc〉, 1〉374 else 375 let 〈b,v〉≝ head … v in if b then 376 let 〈pc,b1〉≝ next pmem pc in 〈〈 INC … (DIRECT b1), pc〉, 1〉377 else 378 〈〈 INC … ACC_A, pc〉, 1〉379 else 380 let 〈b,v〉≝ head … v in if b then 381 let 〈b,v〉≝ head … v in if b then 382 〈〈R R … ACC_A, pc〉, 1〉366 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 367 else 368 let 〈b,v〉≝ head … v in if b then 369 〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉 370 else 371 let 〈b,v〉≝ head … v in if b then 372 let 〈b,v〉≝ head … v in if b then 373 〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉 374 else 375 let 〈b,v〉≝ head … v in if b then 376 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉 377 else 378 〈〈RealInstruction (INC … ACC_A), pc〉, 1〉 379 else 380 let 〈b,v〉≝ head … v in if b then 381 let 〈b,v〉≝ head … v in if b then 382 〈〈RealInstruction (RR … ACC_A), pc〉, 1〉 383 383 else 384 384 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉 … … 387 387 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 388 388 else 389 〈〈 NOP …, pc〉, 1〉.389 〈〈RealInstruction (NOP …), pc〉, 1〉. 390 390 %. 391 391 qed. 
src/ASM/Interpret.ma
r757 r820 158 158 include alias "ASM/BitVectorTrie.ma". 159 159 160 definition execute_1: Status → Status ≝ 160 definition execute_1_preinstruction: ∀A: Type[0]. (A → Byte) → preinstruction A → Status → Status ≝ 161 λA: Type[0]. 162 λaddr_of: A → Byte. 163 λinstr: preinstruction A. 161 164 λs: Status. 162 let 〈instr_pc, ticks〉 ≝ fetch (code_memory s) (program_counter s) in 163 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 164 let s ≝ set_clock s (clock s + ticks) in 165 let s ≝ set_program_counter s pc in 166 let s ≝ 167 match instr with 165 match instr with 168 166 [ ADD addr1 addr2 ⇒ 169 167 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1) … … 397 395 let new_pc ≝ high_bits @@ low_bits in 398 396 set_program_counter s new_pc 399  JMP _ ⇒ (* DPM: always indirect_dptr *)400 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in401 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in402 let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in403 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in404 set_program_counter s new_pc405  LJMP addr ⇒406 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with407 [ ADDR16 a ⇒ λaddr16: True.408 set_program_counter s a409  _ ⇒ λother: False. ⊥410 ] (subaddressing_modein … addr)411  SJMP addr ⇒412 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with413 [ RELATIVE r ⇒ λrelative: True.414 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in415 set_program_counter s new_pc416  _ ⇒ λother: False. ⊥417 ] (subaddressing_modein … addr)418  AJMP addr ⇒419 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with420 [ ADDR11 a ⇒ λaddr11: True.421 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in422 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in423 let bit ≝ get_index' ? O ? nl in424 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in425 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in426 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in427 set_program_counter s new_pc428  _ ⇒ λother: False. ⊥429 ] (subaddressing_modein … addr)430 397  MOVX addr ⇒ 431 398 (* DPM: only copies  doesn't affect I/O *) … … 471 438 set_arg_1 s addr1 (get_arg_1 s addr2 false) 472 439 ] 473  LCALL addr ⇒ 474 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 475 [ ADDR16 a ⇒ λaddr16: True. 476 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 477 let s ≝ set_8051_sfr s SFR_SP new_sp in 478 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 479 let s ≝ write_at_stack_pointer s pc_bl in 480 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 481 let s ≝ set_8051_sfr s SFR_SP new_sp in 482 let s ≝ write_at_stack_pointer s pc_bu in 483 set_program_counter s a 484  _ ⇒ λother: False. ⊥ 485 ] (subaddressing_modein … addr) 486  ACALL addr ⇒ 487 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 488 [ ADDR11 a ⇒ λaddr11: True. 489 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 490 let s ≝ set_8051_sfr s SFR_SP new_sp in 491 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 492 let s ≝ write_at_stack_pointer s pc_bl in 493 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 494 let s ≝ set_8051_sfr s SFR_SP new_sp in 495 let s ≝ write_at_stack_pointer s pc_bu in 496 let 〈thr, eig〉 ≝ split ? 3 8 a in 497 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 498 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 499 set_program_counter s new_addr 500  _ ⇒ λother: False. ⊥ 501 ] (subaddressing_modein … addr) 502  Jump j ⇒ 503 match j with 504 [ JC addr ⇒ 505 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 506 [ RELATIVE r ⇒ λrel: True. 440  JC addr ⇒ 441 let r ≝ addr_of addr in 507 442 if get_cy_flag s then 508 443 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in … … 510 445 else 511 446 s 512  _ ⇒ λother: False. ⊥513 ] (subaddressing_modein … addr)514 447  JNC addr ⇒ 515 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 516 [ RELATIVE r ⇒ λrel: True. 448 let r ≝ addr_of addr in 517 449 if ¬(get_cy_flag s) then 518 450 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in … … 520 452 else 521 453 s 522  _ ⇒ λother: False. ⊥523 ] (subaddressing_modein … addr)524 454  JB addr1 addr2 ⇒ 525 match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 526 [ RELATIVE r ⇒ λrel: True. 455 let r ≝ addr_of addr2 in 527 456 if get_arg_1 s addr1 false then 528 457 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in … … 530 459 else 531 460 s 532  _ ⇒ λother: False. ⊥533 ] (subaddressing_modein … addr2)534 461  JNB addr1 addr2 ⇒ 535 match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 536 [ RELATIVE r ⇒ λrel: True. 462 let r ≝ addr_of addr2 in 537 463 if ¬(get_arg_1 s addr1 false) then 538 464 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in … … 540 466 else 541 467 s 542  _ ⇒ λother: False. ⊥543 ] (subaddressing_modein … addr2)544 468  JBC addr1 addr2 ⇒ 545 match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 546 [ RELATIVE r ⇒ λrel: True. 469 let r ≝ addr_of addr2 in 547 470 let s ≝ set_arg_1 s addr1 false in 548 471 if get_arg_1 s addr1 false then … … 551 474 else 552 475 s 553  _ ⇒ λother: False. ⊥554 ] (subaddressing_modein … addr2)555 476  JZ addr ⇒ 556 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 557 [ RELATIVE r ⇒ λrel: True. 477 let r ≝ addr_of addr in 558 478 if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then 559 479 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in … … 561 481 else 562 482 s 563  _ ⇒ λother: False. ⊥564 ] (subaddressing_modein … addr)565 483  JNZ addr ⇒ 566 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 567 [ RELATIVE r ⇒ λrel: True. 484 let r ≝ addr_of addr in 568 485 if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then 569 486 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in … … 571 488 else 572 489 s 573  _ ⇒ λother: False. ⊥574 ] (subaddressing_modein … addr)575 490  CJNE addr1 addr2 ⇒ 576 match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 577 [ RELATIVE r ⇒ λrelative: True. 491 let r ≝ addr_of addr2 in 578 492 match addr1 with 579 493 [ inl l ⇒ … … 598 512 (set_flags s new_cy (None ?) (get_ov_flag s)) 599 513 ] 600  _ ⇒ λother: False. ⊥601 ] (subaddressing_modein … addr2)602 514  DJNZ addr1 addr2 ⇒ 603 match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 604 [ RELATIVE r ⇒ λrel: True. 605 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in 606 let s ≝ set_arg_8 s addr1 result in 607 if ¬(eq_bv ? result (zero 8)) then 608 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in 609 set_program_counter s new_pc 610 else 611 s 612  _ ⇒ λother: False. ⊥ 613 ] (subaddressing_modein … addr2) 614 ] 515 let r ≝ addr_of addr2 in 516 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in 517 let s ≝ set_arg_8 s addr1 result in 518 if ¬(eq_bv ? result (zero 8)) then 519 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in 520 set_program_counter s new_pc 521 else 522 s 523  NOP ⇒ s 524 ]. 525 try assumption 526 try ( 527 normalize 528 repeat (@ (le_S_S)) 529 @ (le_O_n) 530 ) 531 try ( 532 @ (execute_1_technical … (subaddressing_modein …)) 533 @ I 534 ) 535 try ( 536 normalize 537 @ I 538 ) 539 qed. 540 541 definition execute_1: Status → Status ≝ 542 λs: Status. 543 let 〈instr_pc, ticks〉 ≝ fetch (code_memory s) (program_counter s) in 544 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 545 let s ≝ set_clock s (clock s + ticks) in 546 let s ≝ set_program_counter s pc in 547 let s ≝ 548 match instr with 549 [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] 550 (λx. 551 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with 552 [ RELATIVE r ⇒ λ_. r 553  _ ⇒ λabsd. ⊥ 554 ] (subaddressing_modein … x)) instr s 555  ACALL addr ⇒ 556 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 557 [ ADDR11 a ⇒ λaddr11: True. 558 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 559 let s ≝ set_8051_sfr s SFR_SP new_sp in 560 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 561 let s ≝ write_at_stack_pointer s pc_bl in 562 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 563 let s ≝ set_8051_sfr s SFR_SP new_sp in 564 let s ≝ write_at_stack_pointer s pc_bu in 565 let 〈thr, eig〉 ≝ split ? 3 8 a in 566 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 567 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 568 set_program_counter s new_addr 569  _ ⇒ λother: False. ⊥ 570 ] (subaddressing_modein … addr) 571  LCALL addr ⇒ 572 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 573 [ ADDR16 a ⇒ λaddr16: True. 574 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 575 let s ≝ set_8051_sfr s SFR_SP new_sp in 576 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 577 let s ≝ write_at_stack_pointer s pc_bl in 578 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 579 let s ≝ set_8051_sfr s SFR_SP new_sp in 580 let s ≝ write_at_stack_pointer s pc_bu in 581 set_program_counter s a 582  _ ⇒ λother: False. ⊥ 583 ] (subaddressing_modein … addr) 615 584  MOVC addr1 addr2 ⇒ 616 585 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with … … 632 601  _ ⇒ λother: False. ⊥ 633 602 ] (subaddressing_modein … addr2) 634  NOP ⇒ s 635 ] 603  JMP _ ⇒ (* DPM: always indirect_dptr *) 604 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 605 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in 606 let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in 607 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in 608 set_program_counter s new_pc 609  LJMP addr ⇒ 610 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 611 [ ADDR16 a ⇒ λaddr16: True. 612 set_program_counter s a 613  _ ⇒ λother: False. ⊥ 614 ] (subaddressing_modein … addr) 615  SJMP addr ⇒ 616 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 617 [ RELATIVE r ⇒ λrelative: True. 618 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in 619 set_program_counter s new_pc 620  _ ⇒ λother: False. ⊥ 621 ] (subaddressing_modein … addr) 622  AJMP addr ⇒ 623 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 624 [ ADDR11 a ⇒ λaddr11: True. 625 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 626 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 627 let bit ≝ get_index' ? O ? nl in 628 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 629 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 630 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in 631 set_program_counter s new_pc 632  _ ⇒ λother: False. ⊥ 633 ] (subaddressing_modein … addr) 634 ] 636 635 in 637 636 s. … … 652 651 qed. 653 652 653 axiom fetch_pseudo_instruction: 654 ∀p: list labelled_instruction. 655 ∀pc: Word. 656 (pseudo_instruction × Word) × nat. 657 658 axiom address_of_labels: Identifier → Byte. 659 axiom address_of_word_labels: Identifier → Word. 660 661 definition execute_1_pseudo_instruction: pseudo_assembly_program → Status → Status ≝ 662 λp. 663 λs. 664 let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction (\snd p) (program_counter s) in 665 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 666 let s ≝ set_clock s (clock s + ticks) in 667 let s ≝ set_program_counter s pc in 668 let s ≝ 669 match instr with 670 [ Instruction instr ⇒ execute_1_preinstruction ? address_of_labels instr s 671  Comment cmt ⇒ s 672  Cost cst ⇒ s 673  Jmp jmp ⇒ set_program_counter s (address_of_word_labels jmp) 674  Call call ⇒ 675 let a ≝ address_of_word_labels call in 676 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 677 let s ≝ set_8051_sfr s SFR_SP new_sp in 678 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 679 let s ≝ write_at_stack_pointer s pc_bl in 680 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 681 let s ≝ set_8051_sfr s SFR_SP new_sp in 682 let s ≝ write_at_stack_pointer s pc_bu in 683 set_program_counter s a 684  Mov dptr ident ⇒ set_arg_16 s (get_arg_16 s (DATA16 (address_of_word_labels ident))) dptr 685 ] 686 in 687 s. 688 normalize 689 @ I 690 qed. 691 654 692 let rec execute (n: nat) (s: Status) on n: Status ≝ 655 693 match n with … … 657 695  S o ⇒ execute o (execute_1 s) 658 696 ]. 697 698 let rec execute_pseudo_instruction (n: nat) (p: pseudo_assembly_program) (s: Status) on n: Status ≝ 699 match n with 700 [ O ⇒ s 701  S o ⇒ execute_pseudo_instruction o p (execute_1_pseudo_instruction p s) 702 ].
Note: See TracChangeset
for help on using the changeset viewer.