Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Protect against overflows in leaq N(src), dst #407

Merged
merged 1 commit into from
Aug 27, 2021
Merged

Protect against overflows in leaq N(src), dst #407

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 17 additions & 12 deletions x86/Asmexpand.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,15 @@ let offset_addressing (Addrmode(base, ofs, cst)) delta =
let linear_addr reg ofs = Addrmode(Some reg, None, Coq_inl ofs)
let global_addr id ofs = Addrmode(None, None, Coq_inr(id, ofs))

(* Emit a 64-bit immediate add [dst <- src + imm]. *)

let emit_addimm64 dst src imm =
if Op.offset_in_range imm then
emit (Pleaq(dst, linear_addr src imm))
else begin
emit (Pmov_rr(dst, src)); emit (Paddq_ri(dst, Integers.Int64.repr imm))
end

(* Translate a builtin argument into an addressing mode *)

let addressing_of_builtin_arg = function
Expand Down Expand Up @@ -289,9 +298,9 @@ let expand_builtin_va_start_elf64 r =
emit (Pmovl_mr (linear_addr r _0z, RAX));
emit (Pmovl_ri (RAX, coqint_of_camlint fp_offset));
emit (Pmovl_mr (linear_addr r _4z, RAX));
emit (Pleaq (RAX, linear_addr RSP (Z.of_uint64 overflow_arg_area)));
emit_addimm64 RAX RSP (Z.of_uint64 overflow_arg_area);
emit (Pmovq_mr (linear_addr r _8z, RAX));
emit (Pleaq (RAX, linear_addr RSP (Z.of_uint64 reg_save_area)));
emit_addimm64 RAX RSP (Z.of_uint64 reg_save_area);
emit (Pmovq_mr (linear_addr r _16z, RAX))

let expand_builtin_va_start_win64 r =
Expand All @@ -302,7 +311,7 @@ let expand_builtin_va_start_win64 r =
let ofs =
Int64.(add !current_function_stacksize
(mul 8L (of_int num_args))) in
emit (Pleaq (RAX, linear_addr RSP (Z.of_uint64 ofs)));
emit_addimm64 RAX RSP (Z.of_uint64 ofs);
emit (Pmovq_mr (linear_addr r _0z, RAX))

(* FMA operations *)
Expand Down Expand Up @@ -550,10 +559,8 @@ let expand_instruction instr =
emit (Psubl_ri (RSP, sz'));
emit (Pcfi_adjust sz');
(* Stack chaining *)
let addr1 = linear_addr RSP (Z.of_uint (sz + 8)) in
let addr2 = linear_addr RSP ofs_link in
emit (Pleaq (RAX,addr1));
emit (Pmovq_mr (addr2, RAX));
emit_addimm64 RAX RSP (Z.of_uint (sz + 8));
emit (Pmovq_mr (linear_addr RSP ofs_link, RAX));
current_function_stacksize := Int64.of_int (sz + 8)
end else if Archi.ptr64 then begin
let (sz, save_regs) = sp_adjustment_elf64 sz in
Expand All @@ -563,16 +570,14 @@ let expand_instruction instr =
emit (Pcfi_adjust sz');
if save_regs >= 0 then begin
(* Save the registers *)
emit (Pleaq (R10, linear_addr RSP (Z.of_uint save_regs)));
emit_addimm64 R10 RSP (Z.of_uint save_regs);
emit (Pcall_s (intern_string "__compcert_va_saveregs",
{sig_args = []; sig_res = Tvoid; sig_cc = cc_default}))
end;
(* Stack chaining *)
let fullsz = sz + 8 in
let addr1 = linear_addr RSP (Z.of_uint fullsz) in
let addr2 = linear_addr RSP ofs_link in
emit (Pleaq (RAX, addr1));
emit (Pmovq_mr (addr2, RAX));
emit_addimm64 RAX RSP (Z.of_uint fullsz);
emit (Pmovq_mr (linear_addr RSP ofs_link, RAX));
current_function_stacksize := Int64.of_int fullsz
end else begin
let sz = sp_adjustment_32 sz in
Expand Down