diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-02-09 14:29:18 +0100 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-02-12 14:38:59 +0100 |
commit | 26a4436b9d1b6916d67ee35d00a7120603a3bc9c (patch) | |
tree | ee3b643431a6ee6ad487e3ad8b611c920371fdd5 /x86/Asmgenproof1.v | |
parent | 81bcef3f62b7283910f898cdc89eaf5c836ded6a (diff) | |
download | compcert-kvx-26a4436b9d1b6916d67ee35d00a7120603a3bc9c.tar.gz compcert-kvx-26a4436b9d1b6916d67ee35d00a7120603a3bc9c.zip |
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.
Diffstat (limited to 'x86/Asmgenproof1.v')
-rw-r--r-- | x86/Asmgenproof1.v | 9 |
1 files changed, 7 insertions, 2 deletions
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 *) |