Ignore:
Timestamp:
Jun 13, 2012, 3:44:20 PM (8 years ago)
Author:
boender
Message:
  • updated Policy to work better
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2048 r2059  
    128128  ppc_pc_map → Prop ≝
    129129 λprogram.λop.λp.
    130  ∀i.i < |program| →
     130 ∀i.i |program| →
    131131   let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in
    132132   let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in
    133133     (*opc ≤ pc ∧*) jmpleq oj j.
    134 
     134     
    135135(* this is the instruction size as determined by the jump length given *)
    136136definition expand_relative_jump_internal_unsafe:
     
    639639qed.
    640640
    641 definition policy_equal ≝
     641(* NOTE: we only compare the first elements here because otherwise the
     642 * added = 0 → policy_equal property of jump_expansion_step doesn't hold:
     643 * if we have not added anything to the pc, we only know the PC hasn't changed,
     644 * there might still have been a short/medium jump change *)
     645definition policy_pc_equal ≝
    642646  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
    643647  (∀n:ℕ.n ≤ |program| →
    644     bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 =
    645     bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉).
     648    \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) =
     649    \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)).
     650
     651definition policy_jump_equal ≝
     652  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
     653  (∀n:ℕ.n < |program| →
     654    \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) =
     655    \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)).
    646656   
    647657definition nec_plus_ultra ≝
Note: See TracChangeset for help on using the changeset viewer.