In "symbol + ofs" addressing modes, limit the range of "ofs" in 64 bits

In 32-bit mode, a symbolic reference "symbol + ofs" (address of "symbol" plus "ofs" bytes) can always be resolved by the linker into a 32-bit quantity that fits the 32-bit displacement field of x86 addressing modes.

Not so in 64-bit mode: first, the displacement field is still 32 bits but the full address is 64 bits; second, the displacement is relative to the RIP instruction pointer.  In the "small code model" that CompCert uses for x86-64, excessively large offsets lead to link-time overflows of this 32-bit displacement field.

This commit addresses the issue by limiting the "ofs" part of "symbol + ofs" global addressing models to the range [-2^24, 2^24 - 1].  As explained in the AMD64 ELF ABI document, this is a safe range in the small code model, under the assumption that no global symbol is bigger than 2^24 bytes.  GCC seems to be using a wider range [-2^31, 2^24 - 1] but I'd rather be safe.

The limitation of the "ofs" offset is achieved by extending the mechanisms already present to ensure that "ofs" in "reg + ofs" indexed addressing modes fits in 32-bit signed:
- Op.addressing_valid checks that the "ofs" part of "symbol + ofs" addressing modes is in the correct interval;
- SelectOp.addressing turns invalid addressings into lea's + indexed addressings;
- Asmgen.normalize_addrmode_64 turns lea's with invalid addressings into simpler lea's + addq of the large offset.

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 *)
diff --git a/x86/Op.v b/x86/Op.v
index 02b04574..79c84ca2 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -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.