diff options
Diffstat (limited to 'x86')
-rw-r--r-- | x86/Asmgen.v | 9 | ||||
-rw-r--r-- | x86/Asmgenproof1.v | 9 | ||||
-rw-r--r-- | x86/Op.v | 26 |
3 files changed, 33 insertions, 11 deletions
diff --git a/x86/Asmgen.v b/x86/Asmgen.v index a627881b..dedbfbe6 100644 --- a/x86/Asmgen.v +++ b/x86/Asmgen.v @@ -153,12 +153,13 @@ Definition normalize_addrmode_32 (a: addrmode) := Definition normalize_addrmode_64 (a: addrmode) := match a with | Addrmode base ofs (inl n) => - let n' := Int.signed (Int.repr n) in - if zeq n' n + if Op.offset_in_range n then (a, None) else (Addrmode base ofs (inl _ 0), Some (Int64.repr n)) - | Addrmode base ofs (inr _) => - (a, None) + | Addrmode base ofs (inr (id, delta)) => + if Op.ptroffset_in_range delta || negb Archi.ptr64 + then (a, None) + else (Addrmode base ofs (inr _ (id, Ptrofs.zero)), Some (Ptrofs.to_int64 delta)) end. (** Floating-point comparison. We swap the operands in some cases diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v index aade95d2..86a5218a 100644 --- a/x86/Asmgenproof1.v +++ b/x86/Asmgenproof1.v @@ -495,9 +495,14 @@ Lemma normalize_addrmode_64_correct: | (am', Some delta) => Val.addl (eval_addrmode64 ge am' rs) (Vlong delta) end. Proof. - intros; destruct am as [base ofs [n|r]]; simpl; auto. - destruct (zeq (Int.signed (Int.repr n)) n); simpl; auto. + intros; destruct am as [base ofs [n|[id delta]]]; simpl. +- destruct (offset_in_range n); auto; simpl. rewrite ! Val.addl_assoc. apply f_equal. apply f_equal. simpl. rewrite Int64.add_zero_l; auto. +- destruct (ptroffset_in_range delta); auto. + destruct Archi.ptr64 eqn:SF; auto; simpl. + rewrite ! Val.addl_assoc. apply f_equal. apply f_equal. + rewrite <- Genv.shift_symbol_address_64 by auto. + f_equal. rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto. Qed. (** Processor conditions and comparisons *) @@ -201,9 +201,25 @@ Global Opaque eq_condition eq_addressing eq_operation. mode is valid, i.e. that the offsets are in range. The check always succeeds in 32-bit mode because offsets are always 32-bit integers and are normalized as 32-bit signed integers - during code generation (see [Asmgen.normalize_addrmode_32]). *) + during code generation (see [Asmgen.normalize_addrmode_32]). -Definition offset_in_range (n: Z) : bool := zle Int.min_signed n && zle n Int.max_signed. + Moreover, in 64-bit mode, we use RIP-relative addressing for + access to globals. (This is the "small code model" from the + x86_64 ELF ABI.) Thus, for addressing global variables, + the offset from the variable plus the RIP-relative offset + must fit in 32 bits. The "small code model" guarantees that + this will fit if the offset is between [-2^24] and [2^24-1], + under the assumption that no global variable is bigger than + [2^24] bytes. *) + +Definition offset_in_range (n: Z) : bool := + zle Int.min_signed n && zle n Int.max_signed. + +Definition ptroffset_min := -16777216. (**r [-2^24] *) +Definition ptroffset_max := 16777215. (**r [2^24 - 1] *) + +Definition ptroffset_in_range (n: ptrofs) : bool := + let n := Ptrofs.signed n in zle ptroffset_min n && zle n ptroffset_max. Definition addressing_valid (a: addressing) : bool := if Archi.ptr64 then @@ -212,9 +228,9 @@ Definition addressing_valid (a: addressing) : bool := | Aindexed2 n => offset_in_range n | Ascaled sc ofs => offset_in_range ofs | Aindexed2scaled sc ofs => offset_in_range ofs - | Aglobal s ofs => true - | Abased s ofs => true - | Abasedscaled sc s ofs => true + | Aglobal s ofs => ptroffset_in_range ofs + | Abased s ofs => ptroffset_in_range ofs + | Abasedscaled sc s ofs => ptroffset_in_range ofs | Ainstack ofs => offset_in_range (Ptrofs.signed ofs) end else true. |