Ignore:
Timestamp:
Jun 12, 2012, 2:46:54 PM (8 years ago)
Author:
boender
Message:
  • factorised jump decisions
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2047 r2048  
    324324  then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
    325325  else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
    326   let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
    327   let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    328   if eq_bv ? upper (zero 8)
     326  let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
     327  if sj_possible
    329328  then short_jump
    330329  else long_jump.
     
    336335  let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
    337336  let paddr ≝ lookup_def ? ? labels lbl 0 in
    338   let addr ≝
    339     if leb ppc paddr (* forward jump *)
     337  let addr ≝ bitvector_of_nat ?
     338    (if leb ppc paddr (* forward jump *)
    340339    then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)
    341340            + added
    342     else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in
    343   let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (bitvector_of_nat ? addr) in
    344   let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in
    345   if eq_bv ? fst_5_addr fst_5_pc
     341    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
     342  let 〈mj_possible, disp〉 ≝ medium_jump_cond pc_plus_jmp_length addr in   
     343  if mj_possible
    346344  then medium_jump
    347345  else long_jump.
     
    356354  then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
    357355  else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
    358   let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
    359   let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    360   if eq_bv ? upper (zero 8)
     356  let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
     357  if sj_possible
    361358  then short_jump
    362359  else select_call_length labels old_sigma inc_sigma added ppc lbl.
     
    644641definition policy_equal ≝
    645642  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
    646   (* \fst p1 = \fst p2 ∧ *)
    647   (∀n:ℕ.n < |program| →
    648     let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in
    649     let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in
    650     \snd pc1 = \snd pc2).
     643  (∀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〉).
    651646   
    652647definition nec_plus_ultra ≝
     
    745740qed.
    746741
    747 (* (Intermediate) policy safety *)
    748 definition short_jump_cond: Word → Word → pseudo_instruction → Prop ≝
    749   λpc_plus_jmp_length.λaddr.λinstr.
    750   let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
    751   let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    752     if flags then
    753       eq_bv 8 upper [[true;true;true;true;true;true;true;true]] = true
    754     else
    755       eq_bv 8 upper (zero 8) = true.
    756 
    757 definition medium_jump_cond: Word → Word → pseudo_instruction → Prop ≝
    758   λpc_plus_jmp_length.λaddr.λinstr.
    759   let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 addr in
    760   let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 pc_plus_jmp_length in
    761   eq_bv 5 fst_5_addr fst_5_pc = true.
    762  
    763 definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
    764  λprogram.λlabels.λsigma.
     742definition policy_safe: list labelled_instruction → label_map → ℕ → ppc_pc_map → ppc_pc_map → Prop ≝
     743 λprogram.λlabels.λadded.λold_sigma.λsigma.
    765744 ∀i.i < |program| →
    766745 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉 in
     
    769748 ∀dest.is_jump_to instr dest →
    770749   let paddr ≝ lookup_def … labels dest 0 in
    771    let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,short_jump〉)) in
     750   let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump *)
     751   then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
     752   else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,short_jump〉)) in
    772753   match j with
    773    [ short_jump ⇒ short_jump_cond pc_plus_jmp_length addr instr ∧ ¬is_call instr
    774    | medium_jump ⇒  medium_jump_cond pc_plus_jmp_length addr instr ∧
    775        ¬short_jump_cond pc_plus_jmp_length addr instr ∧ ¬is_relative_jump instr
    776    | long_jump   ⇒ ¬short_jump_cond pc_plus_jmp_length addr instr ∧
    777        ¬medium_jump_cond pc_plus_jmp_length addr instr
     754   [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧
     755      ¬is_call instr
     756   | medium_jump ⇒  \fst (medium_jump_cond pc_plus_jmp_length addr) = true ∧
     757       \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
     758       ¬is_relative_jump instr
     759   | long_jump   ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
     760       \fst (medium_jump_cond pc_plus_jmp_length addr) = false
    778761   ].
    779762
Note: See TracChangeset for help on using the changeset viewer.