Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10

1 files changed, 23 insertions, 13 deletions

diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index e2c556c7..f81b9165 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -39,11 +39,6 @@ let _16z = Z.of_sint 16
 
 let stack_alignment () = 16
 
-(* Pseudo instructions for 32/64 bit compatibility *)
-
-let _Plea (r, addr) =
-  if Archi.ptr64 then Pleaq (r, addr) else Pleal (r, addr)
-
 (* SP adjustment to allocate or free a stack frame. *)
 
 let align n a =
@@ -109,6 +104,21 @@ 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))
 
+(* A "leaq" instruction that does not overflow *)
+
+let emit_leaq r addr =
+  match Asmgen.normalize_addrmode_64 addr with
+  | (addr, None) ->
+      emit (Pleaq (r, addr))
+  | (addr, Some delta) ->
+      emit (Pleaq (r, addr));
+      emit (Paddq_ri (r, delta))
+
+(* Pseudo "lea" instruction for 32/64 bit compatibility *)
+
+let emit_lea r addr =
+  if Archi.ptr64 then emit_leaq r addr else emit (Pleal (r, addr))
+
 (* Translate a builtin argument into an addressing mode *)
 
 let addressing_of_builtin_arg = function
@@ -150,8 +160,8 @@ let expand_builtin_memcpy_small sz al src dst =
   copy (addressing_of_builtin_arg src) (addressing_of_builtin_arg dst) sz
 
 let expand_builtin_memcpy_big sz al src dst =
-  if src <> BA (IR RSI) then emit (_Plea (RSI, addressing_of_builtin_arg src));
-  if dst <> BA (IR RDI) then emit (_Plea (RDI, addressing_of_builtin_arg dst));
+  if src <> BA (IR RSI) then emit_lea RSI (addressing_of_builtin_arg src);
+  if dst <> BA (IR RDI) then emit_lea RDI (addressing_of_builtin_arg dst);
   (* TODO: movsq? *)
   emit (Pmovl_ri (RCX,coqint_of_camlint (Int32.of_int (sz / 4))));
   emit Prep_movsl;
@@ -289,9 +299,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_leaq RAX (linear_addr 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_leaq RAX (linear_addr RSP (Z.of_uint64 reg_save_area));
   emit (Pmovq_mr (linear_addr r _16z, RAX))
 
 let expand_builtin_va_start_win64 r =
@@ -302,7 +312,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_leaq RAX (linear_addr RSP (Z.of_uint64 ofs));
   emit (Pmovq_mr (linear_addr r _0z, RAX))
 
 (* FMA operations *)
@@ -552,7 +562,7 @@ let expand_instruction instr =
        (* 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_leaq RAX addr1;
        emit (Pmovq_mr (addr2, RAX));
        current_function_stacksize := Int64.of_int (sz + 8)
      end else if Archi.ptr64 then begin
@@ -563,7 +573,7 @@ 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_leaq R10 (linear_addr RSP (Z.of_uint save_regs));
          emit (Pcall_s (intern_string "__compcert_va_saveregs",
                         {sig_args = []; sig_res = Tvoid; sig_cc = cc_default}))
        end;
@@ -571,7 +581,7 @@ let expand_instruction instr =
        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_leaq RAX addr1;
        emit (Pmovq_mr (addr2, RAX));
        current_function_stacksize := Int64.of_int fullsz
      end else begin