Changeset 2015 for src/ASM/Assembly.ma

Timestamp:

Jun 4, 2012, 4:06:56 PM (8 years ago)

Author:

mulligan

Message:

Changes following a conversation with Jaap: as it stands computation of the length of machine code jump required to expand a pseudo relative jump was mismatched in his code and the assembler. The assembler assumed all lengths were computed from the start of the instruction, whereas Jaap's policies assumed that lengths were computed from the end. This has now been changed in the assembler, where the previous computation was incorrect. From the old point of view, it now appears that we can jump 129 forward and only 125 backward.

File:

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

src/ASM/Assembly.ma

@@ -418 +418 @@
 qed.
 
+(* 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.
+*)
 definition expand_relative_jump_internal:
  ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.
@@ -425 +430 @@
   λlookup_labels.λsigma.λlbl.λppc,i.
    let lookup_address ≝ sigma (lookup_labels lbl) in
-   let pc ≝ sigma ppc in
-   let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false 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 〈upper, lower〉 ≝ split ? 8 8 result in
    if eq_bv ? upper (zero 8) then