 Timestamp:
 May 23, 2011, 6:12:51 PM (9 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r820 r825 410 410 qed. 411 411 412 definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 413 λp. 414 let 〈preamble, instr_list〉 ≝ p in 415 let 〈datalabels, ignore〉 ≝ 416 foldl ((BitVectorTrie Identifier 16) × nat) ? ( 417 λt. λpreamble. 418 let 〈datalabels, addr〉 ≝ t in 419 let 〈name, size〉 ≝ preamble in 420 let addr_16 ≝ bitvector_of_nat 16 addr in 421 〈insert ? ? name addr_16 datalabels, addr + size〉) 422 〈(Stub ? ?), 0〉 preamble in 423 let 〈labels,pc_costs〉 ≝ 424 foldl ((BitVectorTrie ? ?) × (nat × (BitVectorTrie ? ?))) ? ( 425 λt. λi. 426 let 〈label, i〉 ≝ i in 427 let 〈labels, pc_costs〉 ≝ t in 428 let 〈program_counter, costs〉 ≝ pc_costs in 429 let labels ≝ match label with 430 [ None ⇒ labels 431  Some label ⇒ 432 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 433 insert ? ? label program_counter_bv labels 434 ] in 435 〈labels, 412 definition assembly_expansion ≝ 413 λi. 414 λcosts: BitVectorTrie Identifier 16. 415 λprogram_counter: nat. 436 416 match i with 437 417 [ Instruction instr ⇒ … … 449 429  Call call ⇒ 450 430 〈program_counter + 3, costs〉 451  Mov dptr trgt ⇒ pc_costs 452 ]〉 431  Mov dptr trgt ⇒ 〈program_counter, costs〉 432 ]. 433 434 definition assembly_1_pseudoinstruction ≝ 435 λlookup_labels. 436 λlookup_datalabels. 437 λaddress_of. 438 λi: labelled_instruction. 439 match \snd i with 440 [ Cost cost ⇒ [ ] 441  Comment comment ⇒ [ ] 442  Call call ⇒ 443 let address ≝ ADDR16 (lookup_labels call) in 444 assembly1 (LCALL address) 445  Mov d trgt ⇒ 446 let address ≝ DATA16 (lookup_datalabels trgt) in 447 assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉)))) 448  Instruction instr ⇒ assembly_preinstruction ? address_of instr 449  Jmp jmp ⇒ 450 let address ≝ ADDR16 (lookup_labels jmp) in 451 assembly1 (LJMP address) 452 (*  WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels)) 453 *) 454 ]. 455 @ I 456 qed. 457 458 definition construct_datalabels ≝ 459 λpreamble. 460 \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? ( 461 λt. λpreamble. 462 let 〈datalabels, addr〉 ≝ t in 463 let 〈name, size〉 ≝ preamble in 464 let addr_16 ≝ bitvector_of_nat 16 addr in 465 〈insert ? ? name addr_16 datalabels, addr + size〉) 466 〈(Stub ? ?), 0〉 preamble). 467 468 definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 469 λp. 470 let 〈preamble, instr_list〉 ≝ p in 471 let datalabels ≝ construct_datalabels preamble in 472 let 〈labels,pc_costs〉 ≝ 473 foldl ((BitVectorTrie ? ?) × (nat × (BitVectorTrie ? ?))) ? ( 474 λt. λi. 475 let 〈label, i〉 ≝ i in 476 let 〈labels, pc_costs〉 ≝ t in 477 let 〈program_counter, costs〉 ≝ pc_costs in 478 let labels ≝ match label with 479 [ None ⇒ labels 480  Some label ⇒ 481 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 482 insert ? ? label program_counter_bv labels 483 ] in 484 〈labels, assembly_expansion i costs program_counter〉 453 485 ) 〈(Stub ? ?), 〈0,(Stub ? ?)〉〉 instr_list in 454 486 let 〈program_counter, costs〉 ≝ pc_costs in … … 456 488 None ? 457 489 else 458 let flat_list ≝ 459 flatten ? ( 460 map ? ? ( 461 λi: labelled_instruction. 462 match \snd i with 463 [ Cost cost ⇒ [ ] 464  Comment comment ⇒ [ ] 465  Call call ⇒ 466 let pc_offset ≝ lookup ? ? call labels (zero ?) in 467 let address ≝ ADDR16 pc_offset in 468 assembly1 (LCALL address) 469  Mov d trgt ⇒ 470 let pc_offset ≝ lookup ? ? trgt datalabels (zero ?) in 471 let address ≝ DATA16 pc_offset in 472 assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉)))) 473  Instruction instr ⇒ assembly_preinstruction ? (address_of labels) instr 474  Jmp jmp ⇒ 475 let pc_offset ≝ lookup ? ? jmp labels (zero ?) in 476 let address ≝ ADDR16 pc_offset in 477 assembly1 (LJMP address) 478 (*  WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels)) 479 *) 480 ] 481 ) instr_list 482 ) in 490 let flat_list ≝ flatten ? ( 491 map ? ? ( 492 assembly_1_pseudoinstruction ( 493 λx. lookup ? ? x labels (zero ?)) 494 (λx. lookup ? ? x datalabels (zero ?)) 495 (address_of labels)) instr_list) in 483 496 Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉. 497 (* 484 498 [2,3,4,5,6: 485 499 normalize; %; … … 495 509 ] 496 510 ] 497 qed. 511 qed. *) 498 512 499 513 definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 
src/ASM/AssemblyProof.ma
r823 r825 2 2 include "ASM/Interpret.ma". 3 3 4 let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word) 5 (encoding: list Byte) on encoding: Prop ≝ 6 match encoding with 7 [ nil ⇒ final_pc = pc 8  cons hd tl ⇒ 9 let 〈new_pc, byte〉 ≝ next code_memory pc in 10 hd = byte ∧ encoding_check code_memory new_pc final_pc tl 11 ]. 12 13 definition invariant: 14 ∀sigma: Word → Word. ∀assembly_program: pseudo_assembly_program. 15 ∀code_mem: BitVectorTrie Byte 16. Prop ≝ 16 λsigma. 17 λpseudo_assembly_program. 18 λcode_mem. 19 ∀pc: Word. 20 let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in 21 let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in 22 let address_of ≝ ? in 23 let labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in 24 let datalabels ≝ λx. sigma (lookup ? ? x (construct_datalabels preamble) (zero ?)) in 25 let pre_assembled ≝ assembly_1_pseudoinstruction labels datalabels address_of 〈None ?, pre_instr〉 in 26 encoding_check code_mem pc (sigma pre_new_pc) pre_assembled. 27 cases not_implemented 28 qed. 
src/ASM/Interpret.ma
r822 r825 632 632 qed. 633 633 634 definition fetch_pseudo_instruction: PseudoStatus → Word → (Word → nat) → ((pseudo_instruction × Word) × nat) ≝635 λ ps: PseudoStatus.634 definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝ 635 λcode_mem. 636 636 λpc: Word. 637 λticks_of: Word → nat. 638 let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … (code_memory ? ps) ? in 637 let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … code_mem ? in 639 638 let 〈flags, new_pc〉 ≝ half_add ? pc (bitvector_of_nat ? 1) in 640 〈 〈instr, new_pc〉, ticks_ofpc〉.639 〈instr, new_pc〉. 641 640 cases not_implemented. 642 641 qed. … … 668 667 ]. 669 668 669 definition address_of_word_labels_code_mem ≝ 670 λcode_mem. 671 λid: Identifier. 672 bitvector_of_nat 16 (index_of ? (address_of_word_labels_internal id) code_mem). 673 670 674 definition address_of_word_labels ≝ 671 675 λps: PseudoStatus. 672 676 λid: Identifier. 673 bitvector_of_nat 16 (index_of ? (address_of_word_labels_internal id) (code_memory ? ps)).677 address_of_word_labels_code_mem (code_memory ? ps) id. 674 678 675 679 definition execute_1_pseudo_instruction: (Word → nat) → PseudoStatus → PseudoStatus ≝ 676 680 λticks_of. 677 681 λs. 678 let 〈instr _pc, ticks〉 ≝ fetch_pseudo_instruction s (program_counter ? s) ticks_ofin679 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉in682 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (code_memory ? s) (program_counter ? s) in 683 let ticks ≝ ticks_of (program_counter ? s) in 680 684 let s ≝ set_clock ? s (clock ? s + ticks) in 681 685 let s ≝ set_program_counter ? s pc in
Note: See TracChangeset
for help on using the changeset viewer.