Changeset 2015


Ignore:
Timestamp:
Jun 4, 2012, 4:06:56 PM (5 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2005 r2015  
    418418qed.
    419419
     420(* XXX: pc_plus_sjmp_length used to be just sigma of ppc.  This is incorrect
     421        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.
     424*)
    420425definition expand_relative_jump_internal:
    421426 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.
     
    425430  λlookup_labels.λsigma.λlbl.λppc,i.
    426431   let lookup_address ≝ sigma (lookup_labels lbl) in
    427    let pc ≝ sigma ppc in
    428    let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false 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
    429434   let 〈upper, lower〉 ≝ split ? 8 8 result in
    430435   if eq_bv ? upper (zero 8) then
Note: See TracChangeset for help on using the changeset viewer.