Changeset 2048 for src/ASM/Assembly.ma


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/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   
Note: See TracChangeset for help on using the changeset viewer.