 Timestamp:
 Feb 22, 2013, 6:45:10 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2705 r2707 559 559 [ LJMP address ] 560 560  Jnz acc tgt1 tgt2 ⇒ 561 561 let lookup_address1 ≝ sigma (lookup_labels tgt1) in 562 let lookup_address2 ≝ sigma (lookup_labels tgt2) in 563 (*CSC: we inefficiently use always LJMPs; the policy could 564 choose two SJMPs instead *) 565 [ RealInstruction (JNZ … (RELATIVE (bitvector_of_nat ? 3))); 566 LJMP (ADDR16 lookup_address2); 567 LJMP (ADDR16 lookup_address1) ] 568  MovSuccessor dst ws lbl ⇒ 569 let addr ≝ lookup_labels lbl in 570 let 〈high, low〉 ≝ vsplit ? 8 8 addr in 571 let v ≝ DATA match ws with [ HIGH ⇒ high  LOW ⇒ low ] in 572 match dst return λx. bool_to_Prop (is_in ? [[acc_a;direct;registr]] x) → ? with 573 [ ACC_A ⇒ λ_. 574 [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, v〉))))))] 575  DIRECT b1 ⇒ λ_. 576 [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT b1, v〉)))))] 577  REGISTER r ⇒ λ_. 578 [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, v〉))))))]  _ ⇒ λK. match K in False with [ ] ] (subaddressing_modein … dst) 562 579 ]. 563 %580 try % 564 581 qed. 565 582 … … 774 791 [2: @pair_elim #x #y #_ cases (?∧?)] 775 792 normalize in ⊢ (?%?); // 776  #label whd in match (assembly_1_pseudoinstruction ??????);793 7: #label whd in match (assembly_1_pseudoinstruction ??????); 777 794 whd in match (expand_pseudo_instruction ??????); 778 795 @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_ 779 796 normalize in ⊢ (?%?); // 780  #dptr #id normalize in ⊢ (?%?); // 797 8: #dptr #id normalize in ⊢ (?%?); // 798 5: #acc #dst1 #dst2 normalize in ⊢ (?%?); // 799 6: #dst #ws #lbl whd in match (assembly_1_pseudoinstruction ??????); 800 whd in match (expand_pseudo_instruction ??????); 801 @pair_elim #high #low #EQ @(subaddressing_mode_elim … dst) 802 normalize nodelta [2,3: #w] normalize in ⊢ (?%?); // 781 803 ] 782 804 qed.
Note: See TracChangeset
for help on using the changeset viewer.