Changeset 2022


Ignore:
Timestamp:
Jun 7, 2012, 10:47:07 AM (5 years ago)
Author:
boender
Message:
  • corrected jump calculation algorithm
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2021 r2022  
    420420(* XXX: pc_plus_sjmp_length used to be just sigma of ppc.  This is incorrect
    421421        as relative lengths are computed from the *end* of the SJMP, not from
    422         the beginning.  This caused a mismatch with Jaap's code which was
    423         computing the lengths correctly, and has not been fixed.
     422        the beginning.
    424423*)
    425424definition expand_relative_jump_internal:
     
    430429  λlookup_labels.λsigma.λlbl.λppc,i.
    431430   let lookup_address ≝ sigma (lookup_labels lbl) in
    432    let pc_plus_sjmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    433    let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_sjmp_length lookup_address false in
     431   let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     432   let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in
    434433   let 〈upper, lower〉 ≝ split ? 8 8 result in
    435434   if eq_bv ? upper (zero 8) then
     
    537536  | Call call ⇒
    538537    let 〈addr_5, resta〉 ≝ split ? 5 11 (sigma (lookup_labels call)) in
    539     let pc ≝ sigma ppc in
     538    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    540539    let do_a_long ≝ policy ppc in
    541     let 〈pc_5, restp〉 ≝ split ? 5 11 pc in
     540    let 〈pc_5, restp〉 ≝ split ? 5 11 pc_plus_jmp_length in
    542541    if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then
    543542      let address ≝ ADDR11 resta in
     
    551550  | Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr
    552551  | Jmp jmp ⇒
    553     let pc ≝ sigma ppc in
     552    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    554553    let do_a_long ≝ policy ppc in
    555554    let lookup_address ≝ sigma (lookup_labels jmp) in
    556     let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
     555    let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in
    557556    let 〈upper, lower〉 ≝ split ? 8 8 result in
    558557    if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then
     
    561560    else
    562561      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (lookup_labels jmp) in
    563       let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
     562      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc_plus_jmp_length in
    564563      if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then
    565564        let address ≝ ADDR11 rest_addr in
Note: See TracChangeset for help on using the changeset viewer.