Changeset 2707 for src/ASM


Ignore:
Timestamp:
Feb 22, 2013, 6:45:10 PM (7 years ago)
Author:
sacerdot
Message:

Assembly repaired.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2705 r2707  
    559559        [ LJMP address ]
    560560  | 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)
    562579  ].
    563   %
     580  try %
    564581qed.
    565582 
     
    774791  [2: @pair_elim #x #y #_ cases (?∧?)]
    775792  normalize in ⊢ (?%?); //
    776 | #label whd in match (assembly_1_pseudoinstruction ??????);
     793|7: #label whd in match (assembly_1_pseudoinstruction ??????);
    777794  whd in match (expand_pseudo_instruction ??????);
    778795  @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
    779796  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 ⊢ (?%?); //
    781803]
    782804qed.
Note: See TracChangeset for help on using the changeset viewer.