Changeset 2048


Ignore:
Timestamp:
Jun 12, 2012, 2:46:54 PM (5 years ago)
Author:
boender
Message:
  • factorised jump decisions
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2047 r2048  
    1414  | medium_jump: jump_length
    1515  | long_jump: jump_length.
     16 
     17(* Functions that define the conditions under which jumps are possible *)
     18definition short_jump_cond: Word → Word → (*pseudo_instruction →*)
     19  bool × (BitVector 8) ≝
     20  λpc_plus_jmp_length.λaddr.(*λinstr.*)
     21  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
     22  let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
     23    if get_index' ? 2 0 flags then
     24      〈eq_bv 8 upper [[true;true;true;true;true;true;true;true]], lower〉
     25    else
     26      〈eq_bv 8 upper (zero 8), zero 8〉.
     27 
     28definition medium_jump_cond: Word → Word → (*pseudo_instruction →*)
     29  bool × (BitVector 11) ≝
     30  λpc_plus_jmp_length.λaddr.(*λinstr.*)
     31  let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 addr in
     32  let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 pc_plus_jmp_length in
     33  〈eq_bv 5 fst_5_addr fst_5_pc, rest_addr〉.
    1634
    1735definition assembly_preinstruction ≝
     
    430448   let lookup_address ≝ sigma (lookup_labels lbl) in
    431449   let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    432    let 〈result, flags〉 ≝ sub_16_with_carry lookup_address pc_plus_jmp_length false in
    433    let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    434    if eq_bv ? upper (zero 8) then
    435      let address ≝ RELATIVE lower in
     450   let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     451   if sj_possible
     452   then
     453     let address ≝ RELATIVE disp in
    436454       [ RealInstruction (i address) ]
    437455   else
     
    535553  | Comment comment ⇒ [ ]
    536554  | Call call ⇒
    537     let 〈addr_5, resta〉 ≝ vsplit ? 5 11 (sigma (lookup_labels call)) in
    538555    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     556    let lookup_address ≝ sigma (lookup_labels call) in
     557    let 〈mj_possible, disp〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in
    539558    let do_a_long ≝ policy ppc in
    540     let 〈pc_5, restp〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in
    541     if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then
    542       let address ≝ ADDR11 resta in
     559    if mj_possible ∧ ¬ do_a_long then
     560      let address ≝ ADDR11 disp in
    543561        [ ACALL address ]
    544562    else
    545       let address ≝ ADDR16 (sigma (lookup_labels call)) in
     563      let address ≝ ADDR16 lookup_address in
    546564        [ LCALL address ]
    547565  | Mov d trgt ⇒
     
    553571    let do_a_long ≝ policy ppc in
    554572    let lookup_address ≝ sigma (lookup_labels jmp) in
    555     let 〈result, flags〉 ≝ sub_16_with_carry lookup_address pc_plus_jmp_length false in
    556     let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    557     if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then
    558       let address ≝ RELATIVE lower in
     573    let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     574    if sj_possible ∧ ¬ do_a_long then
     575      let address ≝ RELATIVE disp in
    559576        [ SJMP address ]
    560577    else
    561       let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (sigma (lookup_labels jmp)) in
    562       let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in
    563       if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then
    564         let address ≝ ADDR11 rest_addr in
     578      let 〈mj_possible, disp2〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in
     579      if mj_possible ∧ ¬ do_a_long then
     580        let address ≝ ADDR11 disp2 in
    565581          [ AJMP address ]
    566582      else   
  • 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.