Changeset 2022

Timestamp:

Jun 7, 2012, 10:47:07 AM (5 years ago)

Author:

boender

Message:

• corrected jump calculation algorithm

File:

• src/ASM/Assembly.ma (modified) (5 diffs)

src/ASM/Assembly.ma

@@ -420 +420 @@
 (* XXX: pc_plus_sjmp_length used to be just sigma of ppc.  This is incorrect
         as relative lengths are computed from the *end* of the SJMP, not from
-        the beginning.  This caused a mismatch with Jaap's code which was
-        computing the lengths correctly, and has not been fixed.
+        the beginning.
 *)
 definition expand_relative_jump_internal:
@@ -430 +429 @@
   λlookup_labels.λsigma.λlbl.λppc,i.
    let lookup_address ≝ sigma (lookup_labels lbl) in
-   let pc_plus_sjmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
-   let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_sjmp_length lookup_address false in
+   let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
+   let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in
    let 〈upper, lower〉 ≝ split ? 8 8 result in
    if eq_bv ? upper (zero 8) then
@@ -537 +536 @@
   | Call call ⇒
     let 〈addr_5, resta〉 ≝ split ? 5 11 (sigma (lookup_labels call)) in
-    let pc ≝ sigma ppc in
+    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     let do_a_long ≝ policy ppc in
-    let 〈pc_5, restp〉 ≝ split ? 5 11 pc in
+    let 〈pc_5, restp〉 ≝ split ? 5 11 pc_plus_jmp_length in
     if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then
       let address ≝ ADDR11 resta in
@@ -551 +550 @@
   | Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr
   | Jmp jmp ⇒
-    let pc ≝ sigma ppc in
+    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     let do_a_long ≝ policy ppc in
     let lookup_address ≝ sigma (lookup_labels jmp) in
-    let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
+    let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in
     let 〈upper, lower〉 ≝ split ? 8 8 result in
     if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then
@@ -561 +560 @@
     else
       let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (lookup_labels jmp) in
-      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
+      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc_plus_jmp_length in
       if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then
         let address ≝ ADDR11 rest_addr in