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/Asmgen.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'x86/Asmgen.v') 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 -- cgit