Changeset 3066
 Timestamp:
 Apr 2, 2013, 1:48:08 PM (6 years ago)
 Location:
 src
 Files:

 4 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). 
src/LIN/LINToASM.ma
r3051 r3066 360 360 361 361 record init_mutable : Type[0] ≝ 362 { virtual_dptr : Z363 ; actual_dptr : Z362 { virtual_dptr : Identifier × Z 363 ; actual_dptr : Identifier × Z 364 364 ; built_code : list (list labelled_instruction) 365 365 ; built_preamble : list (Identifier × Word) … … 371 371 match mut with 372 372 [ mk_init_mutable virt act acc1 acc2 ⇒ 373 let off ≝ virt  act in374 373 let pre ≝ 375 if eqZb off OZ then [ ] 376 else if eqZb off 1 then [ 〈None ?, Instruction (INC ? DPTR)〉 ] 377 else [ 〈None ?, Instruction (MOV ? (inl … (inl … (inr … 378 〈DPTR, DATA16 (bitvector_of_Z … virt)〉))))〉 ] in 374 if eq_identifier … (\fst virt) (\fst act) then 375 let off ≝ \snd virt  \snd act in 376 if eqZb off OZ then [ ] 377 else if eqZb off 1 then [ 〈None ?, Instruction (INC ? DPTR)〉 ] 378 else [ 〈None ?, Mov (inl … DPTR) (\fst virt) (bitvector_of_Z … (\snd virt))〉 ] 379 else [ 〈None ?, Mov (inl … DPTR) (\fst virt) (bitvector_of_Z … (\snd virt))〉 ] in 379 380 let post ≝ match by with 380 381 [ inl by ⇒ … … 384 385 〈None ?, Mov (inr ?? 〈ACC_A, \fst si_id〉) (\snd si_id) (bv_zero ?)〉 385 386 ] in 386 mk_init_mutable (Zsucc virt)virt387 mk_init_mutable 〈\fst virt, Zsucc (\snd virt)〉 virt 387 388 ((pre @ 388 389 [ post ; … … 415 416 return store_Identifier HIGH id (store_Identifier LOW id mut) 416 417  Init_space n ⇒ 417 return mk_init_mutable (n + virtual_dptr mut) (actual_dptr mut) 418 let 〈virt_id, virt_off〉 ≝ virtual_dptr mut in 419 return mk_init_mutable 〈virt_id, n + virt_off〉 (actual_dptr mut) 418 420 (built_code mut) (built_preamble mut) 419 421  Init_null ⇒ … … 429 431 let 〈id, reg, data〉 ≝ id_reg_data in 430 432 ! Id ← Identifier_of_ident … id ; 431 let mut ≝ mk_init_mutable (virtual_dptr mut) (actual_dptr mut) (built_code mut) 432 (* Paolo: this is what you intended Claudio: 433 (〈Id, bitvector_of_nat … (size_init_data_list … data)〉 :: built_preamble mut) in 434 however, if we do initialization here, we need to actually fix the addresses! 435 for now, I'll change lookup_datalabels... *) 436 (〈Id, bitvector_of_Z … (virtual_dptr mut)〉 :: built_preamble mut) in 433 let mut ≝ mk_init_mutable 〈Id, OZ〉 (actual_dptr … mut) (built_code mut) 434 (〈Id, bitvector_of_nat … (size_init_data_list … data)〉 :: built_preamble mut) in 437 435 foldl … do_store_init_data (return mut) data. 438 436 … … 448 446 ! main ← Identifier_of_ident … (prog_main … p) ; 449 447 ! u ← state_get … ; 450 (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature?*)451 let start_sp : Z ≝ (S (globals_stacksize … p))in452 let mut ≝ mk_init_mutable start_sp OZ[ ] [ ] in448 (* setting this as actual_dptr will force loading of the correct dptr *) 449 let dummy_dptr : Identifier × Z ≝ 〈an_identifier … one, 1〉 in 450 let mut ≝ mk_init_mutable dummy_dptr dummy_dptr [ ] [ ] in 453 451 ! globals_init ← foldl … do_store_global (return mut) (prog_vars … p) ; 454 let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … start_sp) in452 let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … ((S (globals_stacksize … p)))) in 455 453 let init_isp ≝ 456 454 (* initial stack pointer set to 2Fh in order to use addressable bits *)
Note: See TracChangeset
for help on using the changeset viewer.