 Timestamp:
 Apr 2, 2013, 1:48:08 PM (7 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r3065 r3066 513 513 ]. 514 514 515 definition is_code : region → bool ≝ λr.match r with [ Code ⇒ true  _ ⇒ false ]. 516 515 517 definition expand_pseudo_instruction: 516 518 ∀lookup_labels. … … 522 524 λpolicy: Word → bool. 523 525 λppc. 524 λlookup_datalabels:Identifier → Word.526 λlookup_datalabels:Identifier → region × Word. 525 527 λi. 526 528 match i with … … 539 541 [ LCALL address ] 540 542  Mov d trgt off ⇒ 541 let addr ≝ \fst (add_16_with_carry … (lookup_datalabels trgt) off false) in 543 let 〈r, addr〉 ≝ lookup_datalabels trgt in 544 let addr ≝ \fst (add_16_with_carry … addr off false) in 545 let addr ≝ if is_code r then sigma addr else addr in 542 546 match d with 543 547 [ inl _ ⇒ … … 664 668 let labels ≝ \fst (create_label_cost_map instr_list) in 665 669 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 666 let lookup_datalabels ≝ λx. lookup_def … (construct_datalabels preamble) x (sigma (lookup_labels x)) in 670 let lookup_datalabels ≝ λx. 671 match lookup ASMTag … (construct_datalabels preamble) x with 672 [ Some addr ⇒ 〈XData, addr〉 673  None ⇒ 〈Code, lookup_labels x〉 674 ] in 667 675 let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in 668 676 let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in … … 684 692 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels2 pi). 685 693 #lookup_labels #sigma #policy #ppc #pi #lookup_datalabels1 #lookup_datalabels2 686 cases pi // * [ #addr #Id #off % ] * #addr * @(subaddressing_mode_elim … addr) // 694 cases pi // * 695 [ #addr @(subaddressing_mode_elim … addr) 696  * #addr @(subaddressing_mode_elim … addr) [2,3: #arg ] * 697 ] #Id #off whd in ⊢ (??(???%)(???%)); 698 whd in match (expand_pseudo_instruction ??????) in ⊢ (??%%); 699 normalize nodelta 700 @pair_elim * #a #_ @pair_elim * #b #_ % 687 701 qed. 688 702 … … 812 826 normalize in ⊢ (?%?); // 813 827 5: #acc #dst1 #dst2 normalize in ⊢ (?%?); // 814 7: * [ #dptr #id #offset normalize in ⊢ (?%?); //] 815 * #dst @(subaddressing_mode_elim … dst) [2,3: #w] * #lbl #off 816 whd in match (assembly_1_pseudoinstruction ??????); 817 whd in match (expand_pseudo_instruction ??????); 818 lapply (vsplit bool 8 8 ?) * #high #low 819 normalize in ⊢ (?%?); // 828 7: * 829 [ #dst @(subaddressing_mode_elim … dst) 830  * #dst @(subaddressing_mode_elim … dst) [2,3: #w] * 831 ] #lbl #off 832 whd in match (assembly_1_pseudoinstruction ??????); 833 whd in match (expand_pseudo_instruction ??????); 834 normalize nodelta @pair_elim #a #b #_ 835 [*: lapply (vsplit bool 8 8 ?) * #high #low ] 836 normalize in ⊢ (?%?); // 820 837 ] 821 838 qed. … … 837 854 let datalabels ≝ construct_datalabels preamble in 838 855 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in 839 let lookup_datalabels ≝ λx.lookup_def … datalabels x (sigma (lookup_labels x)) in 856 let lookup_datalabels ≝ λx. 857 match lookup ASMTag … (construct_datalabels preamble) x with 858 [ Some addr ⇒ 〈XData, addr〉 859  None ⇒ 〈Code, lookup_labels x〉 860 ] in 840 861 ∀ppc. ∀ppc_ok:nat_of_bitvector … ppc < instr_list. 841 862 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc ppc_ok in … … 856 877 let datalabels ≝ construct_datalabels preamble in 857 878 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in 858 let lookup_datalabels ≝ λx.lookup_def … datalabels x (sigma (lookup_labels x)) in 879 let lookup_datalabels ≝ λx. 880 match lookup ASMTag … (construct_datalabels preamble) x with 881 [ Some addr ⇒ 〈XData, addr〉 882  None ⇒ 〈Code, lookup_labels x〉 883 ] in 859 884 let 〈next_pc,revcode〉 ≝ pi1 … ( 860 885 foldl_strong 
src/ASM/Interpret.ma
r3064 r3066 186 186  _ ⇒ λother: False. ⊥ 187 187 ] (subaddressing_modein … addr) 188  JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)188  JMP acc_dptr ⇒ λinstr_refl. 189 189 let s ≝ add_ticks1 s in 190 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 191 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 192 let jmp_addr : Word ≝ add … big_acc dptr in 190 let jmp_addr ≝ get_arg_16 … s acc_dptr in 193 191 set_program_counter … s jmp_addr 194 192  NOP ⇒ λinstr_refl. … … 612 610  _ ⇒ λother: False. ⊥ 613 611 ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr)) 614  JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)612  JMP acc_dptr ⇒ λinstr_refl. 615 613 let s ≝ add_ticks1 s in 616 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 617 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 618 let jmp_addr ≝ add … big_acc dptr in 619 let new_pc : Word ≝ add … (program_counter … s) jmp_addr in (* JHM: type annotation *) 620 set_program_counter … s new_pc 614 let jmp_addr ≝ get_arg_16 … s acc_dptr in 615 set_program_counter … s jmp_addr 621 616  NOP ⇒ λinstr_refl. 622 617 let s ≝ add_ticks2 s in … … 960 955 program_counter_set_8051_sfr,program_counter_set_arg_1/ 961 956 try (% @I) try (@or_introl % @I) try (@or_intror % @I) // 957 normalize nodelta 958 @(subaddressing_mode_elim … arg2) #w whd in match (get_arg_16 ????); 959 %1 arg2 960 @(subaddressing_mode_elim … arg1) 961 whd in match (set_arg_16 ?????); 962 whd in match (set_arg_16' ?????); 963 @vsplit_elim #vh #vl #_ normalize nodelta % 962 964 qed. 963 965 
src/ASM/Status.ma
r3056 r3066 756 756 qed. 757 757 758 759 definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ data16]] → Word ≝758 definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → 759 [[ data16 ; acc_dptr ]] → Word ≝ 760 760 λm, cm, s, a. 761 match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with761 match a return λx. bool_to_Prop (is_in ? [[ data16 ; acc_dptr ]] x) → ? with 762 762 [ DATA16 d ⇒ λ_:True. d 763  _ ⇒ λK. 764 match K in False with 765 [ 766 ] 763  ACC_DPTR ⇒ λ_:True. 764 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 765 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 766 add … big_acc dptr 767  _ ⇒ Ⓧ 767 768 ] (subaddressing_modein … a). 768 769 … … 1028 1029 qed. 1029 1030 1030 (* probably to be changed *) 1031 definition construct_datalabels: list (Identifier × Word) → ? ≝ 1032 foldl (identifier_map ASMTag Word) ? (λdatalabels,preamble. 1033 let 〈name, addr〉 ≝ preamble in 1034 add ? ? datalabels name addr) (empty_map …). 1035 (* 1031 definition construct_datalabels: list (Identifier × Word) → 1032 identifier_map ASMTag Word ≝ 1033 λthe_preamble. 1034 \fst (foldl ((identifier_map ASMTag Word) × Word) ? (λt,preamble. 1036 1035 let 〈datalabels, addr〉 ≝ t in 1037 1036 let 〈name, size〉 ≝ preamble in 1038 let 〈 carry, sum〉 ≝ half_add … addr size in1039 〈add ? ? datalabels name addr, sum〉)1040 〈empty_map …, zero 16〉 (the_preamble)).1041 *) 1037 let 〈addr, carry〉 ≝ sub_16_with_carry addr size false in 1038 〈add ?? datalabels name addr, addr〉) 1039 (* mcu8051ide disallows XDATA access at 1, bug or feature? *) 1040 〈empty_map …, maximum …〉 the_preamble).
Note: See TracChangeset
for help on using the changeset viewer.