Changeset 936 for src/ASM/Interpret.ma
 Timestamp:
 Jun 10, 2011, 4:20:47 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r928 r936 159 159 include alias "ASM/BitVectorTrie.ma". 160 160 161 definition execute_1_preinstruction: ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝ 161 definition execute_1_preinstruction: 162 ∀ticks: nat × nat. 163 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝ 164 λticks. 162 165 λA, M: Type[0]. 163 166 λaddr_of: A → (PreStatus M) → Word. 164 167 λinstr: preinstruction A. 165 168 λs: PreStatus M. 169 let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in 170 let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in 166 171 match instr with 167 172 [ ADD addr1 addr2 ⇒ 173 let s ≝ add_ticks1 s in 168 174 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1) 169 175 (get_arg_8 ? s false addr2) false in … … 174 180 set_flags ? s cy_flag (Some Bit ac_flag) ov_flag 175 181  ADDC addr1 addr2 ⇒ 182 let s ≝ add_ticks1 s in 176 183 let old_cy_flag ≝ get_cy_flag ? s in 177 184 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1) … … 183 190 set_flags ? s cy_flag (Some Bit ac_flag) ov_flag 184 191  SUBB addr1 addr2 ⇒ 192 let s ≝ add_ticks1 s in 185 193 let old_cy_flag ≝ get_cy_flag ? s in 186 194 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1) … … 192 200 set_flags ? s cy_flag (Some Bit ac_flag) ov_flag 193 201  ANL addr ⇒ 202 let s ≝ add_ticks1 s in 194 203 match addr with 195 204 [ inl l ⇒ … … 210 219 ] 211 220  ORL addr ⇒ 221 let s ≝ add_ticks1 s in 212 222 match addr with 213 223 [ inl l ⇒ … … 228 238 ] 229 239  XRL addr ⇒ 240 let s ≝ add_ticks1 s in 230 241 match addr with 231 242 [ inl l' ⇒ … … 239 250 ] 240 251  INC addr ⇒ 252 let s ≝ add_ticks1 s in 241 253 match addr return λx. bool_to_Prop (is_in … [[ acc_a; 242 254 registr; … … 264 276 ] (subaddressing_modein … addr) 265 277  DEC addr ⇒ 278 let s ≝ add_ticks1 s in 266 279 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in 267 280 set_arg_8 ? s addr result 268 281  MUL addr1 addr2 ⇒ 282 let s ≝ add_ticks1 s in 269 283 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in 270 284 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in … … 276 290 set_8051_sfr ? s SFR_ACC_B high 277 291  DIV addr1 addr2 ⇒ 292 let s ≝ add_ticks1 s in 278 293 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in 279 294 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in … … 288 303 ] 289 304  DA addr ⇒ 305 let s ≝ add_ticks1 s in 290 306 let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in 291 307 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then … … 303 319 s 304 320  CLR addr ⇒ 321 let s ≝ add_ticks1 s in 305 322 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 306 323 [ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8) … … 310 327 ] (subaddressing_modein … addr) 311 328  CPL addr ⇒ 329 let s ≝ add_ticks1 s in 312 330 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 313 331 [ ACC_A ⇒ λacc_a: True. … … 325 343  _ ⇒ λother: False. ? 326 344 ] (subaddressing_modein … addr) 327  SETB b ⇒ set_arg_1 ? s b false 345  SETB b ⇒ 346 let s ≝ add_ticks1 s in 347 set_arg_1 ? s b false 328 348  RL _ ⇒ (* DPM: always ACC_A *) 349 let s ≝ add_ticks1 s in 329 350 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 330 351 let new_acc ≝ rotate_left … 1 old_acc in 331 352 set_8051_sfr ? s SFR_ACC_A new_acc 332 353  RR _ ⇒ (* DPM: always ACC_A *) 354 let s ≝ add_ticks1 s in 333 355 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 334 356 let new_acc ≝ rotate_right … 1 old_acc in 335 357 set_8051_sfr ? s SFR_ACC_A new_acc 336 358  RLC _ ⇒ (* DPM: always ACC_A *) 359 let s ≝ add_ticks1 s in 337 360 let old_cy_flag ≝ get_cy_flag ? s in 338 361 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in … … 342 365 set_8051_sfr ? s SFR_ACC_A new_acc 343 366  RRC _ ⇒ (* DPM: always ACC_A *) 367 let s ≝ add_ticks1 s in 344 368 let old_cy_flag ≝ get_cy_flag ? s in 345 369 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in … … 349 373 set_8051_sfr ? s SFR_ACC_A new_acc 350 374  SWAP _ ⇒ (* DPM: always ACC_A *) 375 let s ≝ add_ticks1 s in 351 376 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 352 377 let 〈nu,nl〉 ≝ split ? 4 4 old_acc in … … 354 379 set_8051_sfr ? s SFR_ACC_A new_acc 355 380  PUSH addr ⇒ 381 let s ≝ add_ticks1 s in 356 382 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with 357 383 [ DIRECT d ⇒ λdirect: True. … … 362 388 ] (subaddressing_modein … addr) 363 389  POP addr ⇒ 390 let s ≝ add_ticks1 s in 364 391 let contents ≝ read_at_stack_pointer ? s in 365 392 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in … … 367 394 set_arg_8 ? s addr contents 368 395  XCH addr1 addr2 ⇒ 396 let s ≝ add_ticks1 s in 369 397 let old_addr ≝ get_arg_8 ? s false addr2 in 370 398 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in … … 372 400 set_arg_8 ? s addr2 old_acc 373 401  XCHD addr1 addr2 ⇒ 402 let s ≝ add_ticks1 s in 374 403 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in 375 404 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in … … 379 408 set_arg_8 ? s addr2 new_arg 380 409  RET ⇒ 410 let s ≝ add_ticks1 s in 381 411 let high_bits ≝ read_at_stack_pointer ? s in 382 412 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in … … 388 418 set_program_counter ? s new_pc 389 419  RETI ⇒ 420 let s ≝ add_ticks1 s in 390 421 let high_bits ≝ read_at_stack_pointer ? s in 391 422 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in … … 397 428 set_program_counter ? s new_pc 398 429  MOVX addr ⇒ 430 let s ≝ add_ticks1 s in 399 431 (* DPM: only copies  doesn't affect I/O *) 400 432 match addr with … … 407 439 ] 408 440  MOV addr ⇒ 441 let s ≝ add_ticks1 s in 409 442 match addr with 410 443 [ inl l ⇒ … … 441 474  JC addr ⇒ 442 475 if get_cy_flag ? s then 443 set_program_counter ? s (addr_of addr s) 476 let s ≝ add_ticks1 s in 477 set_program_counter ? s (addr_of addr s) 444 478 else 479 let s ≝ add_ticks2 s in 445 480 s 446 481  JNC addr ⇒ 447 482 if ¬(get_cy_flag ? s) then 448 set_program_counter ? s (addr_of addr s) 483 let s ≝ add_ticks1 s in 484 set_program_counter ? s (addr_of addr s) 449 485 else 486 let s ≝ add_ticks2 s in 450 487 s 451 488  JB addr1 addr2 ⇒ 452 489 if get_arg_1 ? s addr1 false then 453 set_program_counter ? s (addr_of addr2 s) 490 let s ≝ add_ticks1 s in 491 set_program_counter ? s (addr_of addr2 s) 454 492 else 493 let s ≝ add_ticks2 s in 455 494 s 456 495  JNB addr1 addr2 ⇒ 457 496 if ¬(get_arg_1 ? s addr1 false) then 458 set_program_counter ? s (addr_of addr2 s) 497 let s ≝ add_ticks1 s in 498 set_program_counter ? s (addr_of addr2 s) 459 499 else 500 let s ≝ add_ticks2 s in 460 501 s 461 502  JBC addr1 addr2 ⇒ 462 503 let s ≝ set_arg_1 ? s addr1 false in 463 504 if get_arg_1 ? s addr1 false then 464 set_program_counter ? s (addr_of addr2 s) 505 let s ≝ add_ticks1 s in 506 set_program_counter ? s (addr_of addr2 s) 465 507 else 508 let s ≝ add_ticks2 s in 466 509 s 467 510  JZ addr ⇒ 468 511 if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then 469 set_program_counter ? s (addr_of addr s) 512 let s ≝ add_ticks1 s in 513 set_program_counter ? s (addr_of addr s) 470 514 else 515 let s ≝ add_ticks2 s in 471 516 s 472 517  JNZ addr ⇒ 473 518 if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then 474 set_program_counter ? s (addr_of addr s) 519 let s ≝ add_ticks1 s in 520 set_program_counter ? s (addr_of addr s) 475 521 else 522 let s ≝ add_ticks2 s in 476 523 s 477 524  CJNE addr1 addr2 ⇒ … … 482 529 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in 483 530 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then 531 let s ≝ add_ticks1 s in 484 532 let s ≝ set_program_counter ? s (addr_of addr2 s) in 485 533 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 486 534 else 535 let s ≝ add_ticks2 s in 487 536 (set_flags ? s new_cy (None ?) (get_ov_flag ? s)) 488 537  inr r' ⇒ … … 491 540 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in 492 541 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then 542 let s ≝ add_ticks1 s in 493 543 let s ≝ set_program_counter ? s (addr_of addr2 s) in 494 544 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 495 545 else 546 let s ≝ add_ticks2 s in 496 547 (set_flags ? s new_cy (None ?) (get_ov_flag ? s)) 497 548 ] … … 500 551 let s ≝ set_arg_8 ? s addr1 result in 501 552 if ¬(eq_bv ? result (zero 8)) then 502 set_program_counter ? s (addr_of addr2 s) 553 let s ≝ add_ticks1 s in 554 set_program_counter ? s (addr_of addr2 s) 503 555 else 556 let s ≝ add_ticks2 s in 504 557 s 505  NOP ⇒ s 558  NOP ⇒ 559 let s ≝ add_ticks2 s in 560 s 506 561 ]. 507 562 try assumption … … 517 572 let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in 518 573 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 519 let s ≝ set_clock ? s (clock ? s + ticks) in520 574 let s ≝ set_program_counter ? s pc in 521 575 let s ≝ 522 576 match instr with 523 [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] ?577 [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ? 524 578 (λx. λs. 525 579 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with … … 528 582 ] (subaddressing_modein … x)) instr s 529 583  ACALL addr ⇒ 584 let s ≝ set_clock ? s (ticks + clock ? s) in 530 585 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 531 586 [ ADDR11 a ⇒ λaddr11: True. … … 544 599 ] (subaddressing_modein … addr) 545 600  LCALL addr ⇒ 601 let s ≝ set_clock ? s (ticks + clock ? s) in 546 602 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 547 603 [ ADDR16 a ⇒ λaddr16: True. … … 557 613 ] (subaddressing_modein … addr) 558 614  MOVC addr1 addr2 ⇒ 615 let s ≝ set_clock ? s (ticks + clock ? s) in 559 616 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with 560 617 [ ACC_DPTR ⇒ λacc_dptr: True. … … 576 633 ] (subaddressing_modein … addr2) 577 634  JMP _ ⇒ (* DPM: always indirect_dptr *) 635 let s ≝ set_clock ? s (ticks + clock ? s) in 578 636 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 579 637 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in … … 582 640 set_program_counter ? s new_pc 583 641  LJMP addr ⇒ 642 let s ≝ set_clock ? s (ticks + clock ? s) in 584 643 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 585 644 [ ADDR16 a ⇒ λaddr16: True. … … 588 647 ] (subaddressing_modein … addr) 589 648  SJMP addr ⇒ 649 let s ≝ set_clock ? s (ticks + clock ? s) in 590 650 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 591 651 [ RELATIVE r ⇒ λrelative: True. … … 595 655 ] (subaddressing_modein … addr) 596 656  AJMP addr ⇒ 657 let s ≝ set_clock ? s (ticks + clock ? s) in 597 658 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 598 659 [ ADDR11 a ⇒ λaddr11: True. … … 666 727 address_of_word_labels_code_mem (\snd (code_memory ? ps)) id. 667 728 668 definition execute_1_pseudo_instruction: (Word → nat ) → PseudoStatus → PseudoStatus ≝729 definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝ 669 730 λticks_of. 670 731 λs. 671 732 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in 672 733 let ticks ≝ ticks_of (program_counter ? s) in 673 let s ≝ set_clock ? s (clock ? s + ticks) in674 734 let s ≝ set_program_counter ? s pc in 675 735 let s ≝ 676 736 match instr with 677 [ Instruction instr ⇒ execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s 678  Comment cmt ⇒ s 737 [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s 738  Comment cmt ⇒ 739 let s ≝ set_clock ? s (\fst ticks + clock ? s) in 740 s 679 741  Cost cst ⇒ s 680  Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp) 742  Jmp jmp ⇒ 743 let s ≝ set_clock ? s (\fst ticks + clock ? s) in 744 set_program_counter ? s (address_of_word_labels s jmp) 681 745  Call call ⇒ 746 let s ≝ set_clock ? s (\fst ticks + clock ? s) in 682 747 let a ≝ address_of_word_labels s call in 683 748 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in … … 690 755 set_program_counter ? s a 691 756  Mov dptr ident ⇒ 757 let s ≝ set_clock ? s (\fst ticks + clock ? s) in 692 758 let preamble ≝ \fst (code_memory ? s) in 693 759 let data_labels ≝ construct_datalabels preamble in … … 706 772 ]. 707 773 708 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat ) (s: PseudoStatus) on n: PseudoStatus ≝774 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝ 709 775 match n with 710 776 [ O ⇒ s
Note: See TracChangeset
for help on using the changeset viewer.