Changeset 2713 for src/ASM


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

PolicyFront?.ma repaired

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2653 r2713  
    121121  | RET ⇒ inr … (RET ?)
    122122  | RETI ⇒ inr … (RETI ?)
    123   | NOP ⇒ inr … (RealInstruction (NOP ?))
     123  | NOP ⇒ inr … (NOP ?)
     124  | JMP dst ⇒ inr … (RealInstruction (JMP ? dst))
    124125  ].
    125126
     
    147148     [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))]
    148149  | Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr
     150  | Jnz acc dst1 dst2 ⇒
     151      [ RealInstruction (JNZ … (RELATIVE (bitvector_of_nat ? 3)));
     152        LJMP (ADDR16 (zero ?));
     153        LJMP (ADDR16 (zero ?)) ]
     154  | MovSuccessor dst ws lbl ⇒
     155     let v ≝ DATA (zero …) in
     156     match dst return λx. bool_to_Prop (is_in ? [[acc_a;direct;registr]] x) → ? with
     157     [ ACC_A ⇒ λ_.
     158        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈
     159ACC_A, v〉))))))]
     160     | DIRECT b1 ⇒ λ_.
     161        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT b1, v〉)))))]
     162     | REGISTER r ⇒ λ_.
     163        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈
     164REGISTER r, v〉))))))]
     165     | _ ⇒ λK. match K in False with [ ] ] (subaddressing_modein … dst)
    149166  | Jmp jmp ⇒
    150167    match jmp_len with
     
    587604   @(subaddressing_mode_elim … a1) #w
    588605   #EQ normalize in EQ; destruct(EQ)
    589   |2,3,6: #x [3: #y] #H cases H
    590   |4,5: #id #_ cases a cases b #H try % normalize in H; destruct(H)
     606  |2,3,8: #x [3: #y] #H cases H
     607  |4,7: #id #_ cases a cases b #H try % normalize in H; destruct(H)
     608  |5,6: #x #y #z #H normalize in H; cases H
    591609 ]
    592610qed.
     
    595613  instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i.
    596614 #a #b #i cases i
    597  [2,3,6: #x [3: #y] #H cases H
    598  |4,5: #id #_ cases a cases b @leb_true_to_le / by refl/
     615 [2,3,8: #x [3: #y] #H cases H
     616 |4,7: #id #_ cases a cases b @leb_true_to_le / by refl/
    599617 |1: #pi cases pi
    600618    try (#x #y #H) try (#x #H) try (#H) cases H
     
    603621    cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try %
    604622    @(subaddressing_mode_elim … a1) #w %
     623 |5,6: #x #y #z #H cases H
    605624 ]
    606625qed.
     
    640659              try (#x #id #Hnth_eq #Hsafe) try (#id #Hnth_eq #Hsafe) try (#Hnth_eq #Hsafe)
    641660              try % lapply Hsafe -Hsafe lapply Hnth_eq -Hnth_eq lapply id -id
    642           |2,3,6: #x [3: #y] normalize nodelta #Hnth_eq #_ %]
     661          |2,3,5,8: #x [3: #y #z | 4: #y] normalize nodelta #_ #_ %
     662          |6: #x #y #z normalize nodelta #_ #_ @pair_elim #w1 #w2 #_
     663              @(subaddressing_mode_elim … x) try #k % ]
    643664            #id lapply (Hpc_equal i (le_S_to_le … Hi))
    644665            lapply (Hpc_equal (S i) Hi)
     
    751772  ¬is_jump i → ∀j1,j2.instruction_size_jmplen j1 i = instruction_size_jmplen j2 i.
    752773 #i cases i
    753  [2,3,6: #x [3: #y] #Hj #j1 #j2 %
    754  |4,5: #x #Hi cases Hi
     774 [2,3,8: #x [3: #y] #Hj #j1 #j2 %
     775 |5,6: #x #y #z #_ #j1 #j2 %
     776 |4,7: #x #Hi cases Hi
    755777 |1: #pi cases pi try (#x #y #Hj #j1 #j2) try (#y #Hj #j1 #j2) try (#Hj #j1 #j2)
    756778     try % cases Hj ]
Note: See TracChangeset for help on using the changeset viewer.