From 26a4436b9d1b6916d67ee35d00a7120603a3bc9c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 9 Feb 2018 14:29:18 +0100 Subject: 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. --- x86/Op.v | 26 +++++++++++++++++++++----- 1 file changed, 21 insertions(+), 5 deletions(-) (limited to 'x86/Op.v') 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. -- cgit