Changeset 3078


Ignore:
Timestamp:
Apr 3, 2013, 3:01:54 PM (4 years ago)
Author:
tranquil
Message:

fixed change of Mov

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2771 r3078  
    640640 [ <plus_n_O #_ @le_n
    641641 | -n #n <plus_n_Sm #Hind #H @(transitive_le ??? (Hind (le_S_to_le … H)))
    642    lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (λx.zero 16) (i+n) H)
    643    lapply (refl ? (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)))
    644    cases (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)) in ⊢ (???% → %);
    645    [ normalize nodelta #_ #abs cases abs
    646    | #x cases x -x #pc #jl #EQ normalize nodelta
    647      lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)))
    648      cases (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)) in ⊢ (???% → %);
    649      [ normalize nodelta #_ #abs cases abs
    650      | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hcomp
     642   lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (λx.〈XData, bv_zero 16〉) (i+n) H)
     643   inversion (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol))
     644   [ normalize nodelta #_ *
     645   | * #pc #jl #EQ normalize nodelta
     646     inversion (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol))
     647     [ normalize nodelta #_ *
     648     | * #Spc #Sjl #SEQ normalize nodelta #Hcomp
    651649       >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    652650       >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hcomp @le_plus_n_r
  • src/ASM/PolicyFront.ma

    r3039 r3078  
    661661              try % lapply Hsafe -Hsafe lapply Hnth_eq -Hnth_eq lapply id -id
    662662          |2,3,5: #x [3: #y #z | 4: #y] normalize nodelta #_ #_ %
    663           |7: * [ #x normalize nodelta #y #z #_ #_ % ]
    664             * #x @(subaddressing_mode_elim … x) [2,3: #y] * #lbl #off
    665             normalize nodelta #_ #_ lapply (vsplit ? 8 8 ?) * #w1 #w2 % ]
     663          |7: *
     664            [ #x @(subaddressing_mode_elim … x)
     665            | * #x  @(subaddressing_mode_elim … x) [2,3: #y] *
     666            ] normalize nodelta #lbl #off #_ #_
     667            @pair_elim * #addr normalize nodelta #_ %
     668          ]
    666669            #id lapply (Hpc_equal i (le_S_to_le … Hi))
    667670            lapply (Hpc_equal (S i) Hi)
Note: See TracChangeset for help on using the changeset viewer.