__builtin_memcpy_aligned for large blocks

aarch64/Asmexpand.ml

@@ -37,6 +37,9 @@ let _m1 = Z.of_sint (-1)
 let expand_loadimm32 (dst: ireg) n =
   List.iter emit (Asmgen.loadimm32 dst n [])
 
+let expand_loadimm64 (dst: ireg) n =
+  List.iter emit (Asmgen.loadimm64 dst n [])
+
 let expand_addimm64 (dst: iregsp) (src: iregsp) n =
   List.iter emit (Asmgen.addimm64 dst src n [])
 
@@ -229,39 +232,39 @@ let memcpy_big_arg arg tmp =
   | _ -> assert false
 
 let expand_builtin_memcpy_big sz al src dst =
-  assert (sz >= 16);
+  assert Z.(ge sz _16 && lt sz (shl _1 64));
   memcpy_big_arg src X30;
   memcpy_big_arg dst X14;
   let lbl = new_label () in
-  expand_loadimm32 X15 (Z.of_uint (sz / 16));
+  expand_loadimm64 X15 (Z.div sz _16);
   emit (Plabel lbl);
   emit (Pldp(X16, X17, ADpostincr(RR1 X30, _16)));
   emit (Pstp(X16, X17, ADpostincr(RR1 X14, _16)));
   emit (Psubimm(W, RR1 X15, RR1 X15, _1));
   emit (Pcbnz(W, X15, lbl));
-  if sz mod 16 >= 8 then begin
+  if Z.(ge (modulo sz _16) _8) then begin
     emit (Pldrx(X16, ADpostincr(RR1 X30, _8)));
     emit (Pstrx(X16, ADpostincr(RR1 X14, _8)))
   end;
-  if sz mod 8 >= 4 then begin
+  if Z.(ge (modulo sz _8) _4) then begin
     emit (Pldrw(X16, ADpostincr(RR1 X30, _4)));
     emit (Pstrw(X16, ADpostincr(RR1 X14, _4)))
   end;
-  if sz mod 4 >= 2 then begin
+  if Z.(ge (modulo sz _4) _2) then begin
     emit (Pldrh(W, X16, ADpostincr(RR1 X30, _2)));
     emit (Pstrh(X16, ADpostincr(RR1 X14, _2)))
   end;
-  if sz mod 2 >= 1 then begin
+  if Z.(ge (modulo sz _2) _1) then begin
     emit (Pldrb(W, X16, ADpostincr(RR1 X30, _1)));
     emit (Pstrb(X16, ADpostincr(RR1 X14, _1)))
   end
 
-let expand_builtin_memcpy  sz al args =
+let expand_builtin_memcpy sz al args =
   let (dst, src) =
     match args with [d; s] -> (d, s) | _ -> assert false in
-  if sz < 64
-  then expand_builtin_memcpy_small sz al src dst
-  else expand_builtin_memcpy_big sz al src dst
+  if Z.(lt sz (of_sint 64))
+  then expand_builtin_memcpy_small (Z.to_int sz) (Z.to_int al) src dst
+  else expand_builtin_memcpy_big sz (Z.to_int al) src dst
 
 (* Handling of volatile reads and writes *)
 
@@ -530,7 +533,7 @@ let expand_instruction instr =
      | EF_annot_val (kind,txt,targ) ->
         expand_annot_val kind txt targ args res
      | EF_memcpy(sz, al) ->
-        expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args
+        expand_builtin_memcpy sz al args
      | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
         emit instr
      | _ ->

arm/Asmexpand.ml

@@ -131,33 +131,33 @@ let memcpy_big_arg arg tmp =
       assert false
 
 let expand_builtin_memcpy_big sz al src dst =
-  assert (sz >= al);
-  assert (sz mod al = 0);
+  assert Z.(eq (modulo sz (of_uint al)) _0);
+  assert Z.(gt sz _0 && lt sz (shl _1 32));
   let (s, d) =
     if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in
   memcpy_big_arg src s;
   memcpy_big_arg dst d;
   let (load, store, chunksize) =
     if al >= 4 then
-      (Pldr_p (IR12,s,SOimm _4), Pstr_p (IR12,d,SOimm _4) , 4)
+      (Pldr_p (IR12,s,SOimm _4), Pstr_p (IR12,d,SOimm _4) , _4)
     else if al = 2 then
-       (Pldrh_p (IR12,s,SOimm _2), Pstrh_p (IR12,d,SOimm _2), 2)
+       (Pldrh_p (IR12,s,SOimm _2), Pstrh_p (IR12,d,SOimm _2), _2)
     else
-       (Pldrb_p (IR12,s,SOimm _1), Pstrb_p (IR12,d,SOimm _1), 1) in
-  expand_movimm IR14 (coqint_of_camlint (Int32.of_int (sz / chunksize)));
+       (Pldrb_p (IR12,s,SOimm _1), Pstrb_p (IR12,d,SOimm _1), _1) in
+  expand_movimm IR14 Z.(div sz chunksize);
   let lbl = new_label () in
   emit (Plabel lbl);
   emit load;
   emit (Psubs (IR14,IR14,SOimm _1));
   emit store;
   emit (Pbne lbl)
 
-let expand_builtin_memcpy  sz al args =
+let expand_builtin_memcpy sz al args =
   let (dst, src) =
     match args with [d; s] -> (d, s) | _ -> assert false in
-  if sz <= 32
-  then expand_builtin_memcpy_small sz al src dst
-  else expand_builtin_memcpy_big sz al src dst
+  if Z.(le sz _32)
+  then expand_builtin_memcpy_small (Z.to_int sz) (Z.to_int al) src dst
+  else expand_builtin_memcpy_big sz (Z.to_int al) src dst
 
 (* Handling of volatile reads and writes *)
 
@@ -623,8 +623,7 @@ let expand_instruction instr =
 	   | EF_annot_val (kind,txt,targ) ->
 	      expand_annot_val kind txt targ args res
 	   | EF_memcpy(sz, al) ->
-	      expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz))
-		(Int32.to_int (camlint_of_coqint al)) args
+              expand_builtin_memcpy sz al args
 	   | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
               emit instr
 	   | _ ->

cfrontend/C2C.ml

@@ -343,8 +343,10 @@ let make_builtin_memcpy args =
         error "alignment argument of '__builtin_memcpy_aligned' must be a power of 2";
       if not (Z.eq (Z.modulo sz1 al1) Z.zero) then
         error "alignment argument of '__builtin_memcpy_aligned' must be a divisor of the size";
+      (* Clamp alignment to 8, the largest alignment supported by CompCert *)
+      let al2 = Z.min al1 (Z.of_uint 8) in
       (* Issue #28: must decay array types to pointer types *)
-      Ebuiltin(AST.EF_memcpy(sz1, al1),
+      Ebuiltin(AST.EF_memcpy(sz1, al2),
                [typeconv(typeof dst); typeconv(typeof src)],
                Econs(dst, Econs(src, Enil)), Tvoid)
   | _ ->

lib/Camlcoq.ml

@@ -181,6 +181,9 @@ module Z = struct
   let compare x y = match Z.compare x y with Lt -> -1 | Eq -> 0 | Gt -> 1
   let max = Z.max
   let min = Z.min
+  let logor = Z.coq_lor
+  let logand = Z.coq_land
+  let logxor = Z.coq_lxor
 
   let to_int = function
   | Z0 -> 0
@@ -255,6 +258,9 @@ module Z = struct
   let is_power2 x =
     gt x zero && eq (Z.coq_land x (pred x)) zero
 
+  let shl x n = Z.shiftl x (of_uint n)
+  let shr x n = Z.shiftr x (of_uint n)
+
   let (+) = add
   let (-) = sub
   let ( * ) = mul

powerpc/Asmexpand.ml

@@ -152,9 +152,9 @@ let memcpy_big_arg arg tmp =
   | _ ->
       assert false
 
-let expand_builtin_memcpy_big sz al src dst =
-  assert (sz >= 4);
-  emit_loadimm GPR0 (Z.of_uint (sz / 4));
+let expand_builtin_memcpy_big sz src dst =
+  assert Z.(ge sz _4 && lt sz (shl _1 32));
+  emit_loadimm GPR0 (Z.div sz _4);
   emit (Pmtctr GPR0);
   let (s, d) =
     if dst <> BA (IR GPR11) then (GPR11, GPR12) else (GPR12, GPR11) in
@@ -166,7 +166,7 @@ let expand_builtin_memcpy_big sz al src dst =
   emit (Pstwu(GPR0, Cint _4, d));
   emit (Pbdnz lbl);
   (* s and d lag behind by 4 bytes *)
-  match sz land 3 with
+  match Z.(to_int (modulo sz _4)) with
   | 1 -> emit (Plbz(GPR0, Cint _4, s));
          emit (Pstb(GPR0, Cint _4, d))
   | 2 -> emit (Plhz(GPR0, Cint _4, s));
@@ -180,11 +180,14 @@ let expand_builtin_memcpy_big sz al src dst =
 let expand_builtin_memcpy sz al args =
   let (dst, src) =
     match args with [d; s] -> (d, s) | _ -> assert false in
-  if sz <= (if !Clflags.option_ffpu && al >= 4
-            then if !Clflags.option_Osize then 35 else 51
-	    else if !Clflags.option_Osize then 19 else 27)
-  then expand_builtin_memcpy_small sz al src dst
-  else expand_builtin_memcpy_big sz al src dst
+  let al = Z.to_int al in
+  let threshold =
+    if !Clflags.option_ffpu && al >= 4
+    then if !Clflags.option_Osize then 35 else 51
+    else if !Clflags.option_Osize then 19 else 27 in
+  if Z.(le sz (of_uint threshold))
+  then expand_builtin_memcpy_small (Z.to_int sz) al src dst
+  else expand_builtin_memcpy_big sz src dst
 
 (* Handling of volatile reads and writes *)
 
@@ -988,7 +991,7 @@ let expand_instruction instr =
       | EF_vstore chunk ->
           expand_builtin_vstore chunk args
       | EF_memcpy(sz, al) ->
-          expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args
+          expand_builtin_memcpy sz al args
       | EF_annot_val(kind,txt, targ) ->
           expand_annot_val kind txt targ args res
       | EF_annot _ | EF_debug _ | EF_inline_asm _ ->

riscV/Asmexpand.ml

@@ -46,6 +46,8 @@ let align n a = (n + a - 1) land (-a)
 
 let expand_loadimm32 dst n =
   List.iter emit (Asmgen.loadimm32 dst n [])
+let expand_loadimm64 dst n =
+  List.iter emit (Asmgen.loadimm64 dst n [])
 let expand_addptrofs dst src n =
   List.iter emit (Asmgen.addptrofs dst src n [])
 let expand_storeind_ptr src base ofs =
@@ -216,41 +218,40 @@ let memcpy_big_arg sz arg tmp =
       assert false
 
 let expand_builtin_memcpy_big sz al src dst =
-  assert (sz >= al);
-  assert (sz mod al = 0);
+  assert Z.(eq (modulo sz (of_uint al)) _0);
+  assert (Z.gt sz _0 && Z.lt sz (Z.shl _1 (wordsize * 8)));
   let (s, d) =
     if dst <> BA (IR X5) then (X5, X6) else (X6, X5) in
   memcpy_big_arg sz src s;
   memcpy_big_arg sz dst d;
   (* Use X7 as loop count, X31 and F0 as ld/st temporaries. *)
   let (load, store, chunksize) =
     if Archi.ptr64 && al >= 8 then
-      (Pld (X31, s, Ofsimm _0), Psd (X31, d, Ofsimm _0), 8)
+      (Pld (X31, s, Ofsimm _0), Psd (X31, d, Ofsimm _0), _8)
     else if !Clflags.option_ffpu && al >= 8 then
-      (Pfld (F0, s, Ofsimm _0), Pfsd (F0, d, Ofsimm _0), 8)
+      (Pfld (F0, s, Ofsimm _0), Pfsd (F0, d, Ofsimm _0), _8)
     else if al >= 4 then
-      (Plw (X31, s, Ofsimm _0), Psw (X31, d, Ofsimm _0), 4)
+      (Plw (X31, s, Ofsimm _0), Psw (X31, d, Ofsimm _0), _4)
     else if al = 2 then
-      (Plh (X31, s, Ofsimm _0), Psh (X31, d, Ofsimm _0), 2)
+      (Plh (X31, s, Ofsimm _0), Psh (X31, d, Ofsimm _0), _2)
     else
-      (Plb (X31, s, Ofsimm _0), Psb (X31, d, Ofsimm _0), 1) in
-  expand_loadimm32 X7 (Z.of_uint (sz / chunksize));
-  let delta = Z.of_uint chunksize in
+      (Plb (X31, s, Ofsimm _0), Psb (X31, d, Ofsimm _0), _1) in
+  expand_loadimm64 X7 Z.(div sz chunksize);
   let lbl = new_label () in
   emit (Plabel lbl);
   emit load;
-  expand_addptrofs s s delta;
+  expand_addptrofs s s chunksize;
   emit (Paddiw(X7, X X7, _m1));
   emit store;
-  expand_addptrofs d d delta;
+  expand_addptrofs d d chunksize;
   emit (Pbnew (X X7, X0, lbl))
 
-let expand_builtin_memcpy  sz al args =
+let expand_builtin_memcpy sz al args =
   let (dst, src) =
     match args with [d; s] -> (d, s) | _ -> assert false in
-  if sz <= 32
-  then expand_builtin_memcpy_small sz al src dst
-  else expand_builtin_memcpy_big sz al src dst
+  if Z.(le sz (of_uint 32))
+  then expand_builtin_memcpy_small (Z.to_int sz) (Z.to_int al) src dst
+  else expand_builtin_memcpy_big sz (Z.to_int al) src dst
 
 (* Handling of volatile reads and writes *)
 
@@ -773,7 +774,7 @@ let expand_instruction instr =
      | EF_annot_val (kind,txt,targ) ->
         expand_annot_val kind txt targ args res
      | EF_memcpy(sz, al) ->
-        expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args
+        expand_builtin_memcpy sz al args
      | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
         emit instr
      | _ ->

x86/Asm.v

@@ -286,6 +286,7 @@ Inductive instruction: Type :=
   | Pmovsw
   | Pmovw_rm (rd: ireg) (ad: addrmode)
   | Pnop
+  | Prep_movsb
   | Prep_movsl
   | Psbbl_rr (rd: ireg) (r2: ireg)
   | Psqrtsd (rd: freg) (r1: freg)
@@ -1009,6 +1010,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pmovsw
   | Pmovw_rm _ _
   | Pnop
+  | Prep_movsb
   | Prep_movsl
   | Psbbl_rr _ _
   | Psqrtsd _ _

x86/Asmexpand.ml

@@ -131,10 +131,10 @@ let addressing_of_builtin_arg = function
 
 (* Handling of memcpy *)
 
-(* Unaligned memory accesses are quite fast on IA32, so use large
+(* Unaligned memory accesses are quite fast on x86, so use large
    memory accesses regardless of alignment. *)
 
-let expand_builtin_memcpy_small sz al src dst =
+let expand_builtin_memcpy_small sz src dst =
   let rec copy src dst sz =
     if sz >= 8 && Archi.ptr64 then begin
 	emit (Pmovq_rm (RCX, src));
@@ -159,20 +159,28 @@ let expand_builtin_memcpy_small sz al src dst =
       end in
   copy (addressing_of_builtin_arg src) (addressing_of_builtin_arg dst) sz
 
-let expand_builtin_memcpy_big sz al src dst =
+let expand_builtin_memcpy_big sz src 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;
-  if sz mod 4 >= 2 then emit Pmovsw;
-  if sz mod 2 >= 1 then emit Pmovsb
+  if Archi.ptr64 then begin
+    (* Recent x86-64 processors optimize [rep movsb] specially *)
+    assert Z.(lt sz (shl _1z 64));
+    emit (Pmovq_ri (RCX, sz));
+    emit Prep_movsb
+  end else begin
+    (* For older processors, [rep movsl] is better *)
+    assert Z.(lt sz (Z.shl _1z 32));
+    emit (Pmovl_ri (RCX, Z.div sz _4z));
+    emit Prep_movsl;
+    if Z.(ge (modulo sz _4z) _2z) then emit Pmovsw;
+    if Z.(ge (modulo sz _2z) _1z) then emit Pmovsb
+  end
 
 let expand_builtin_memcpy sz al args =
   let (dst, src) = match args with [d; s] -> (d, s) | _ -> assert false in
-  if sz <= 32
-  then expand_builtin_memcpy_small sz al src dst
-  else expand_builtin_memcpy_big sz al src dst
+  if Z.(le sz (of_sint 32))
+  then expand_builtin_memcpy_small (Z.to_int sz) src dst
+  else expand_builtin_memcpy_big sz src dst
 
 (* Handling of volatile reads and writes *)
 
@@ -603,7 +611,7 @@ let expand_instruction instr =
        | EF_vstore chunk ->
           expand_builtin_vstore chunk args
        | EF_memcpy(sz, al) ->
-          expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args
+          expand_builtin_memcpy sz al args
        | EF_annot_val(kind,txt, targ) ->
           expand_annot_val kind txt targ args res
        | EF_annot _ | EF_debug _ | EF_inline_asm _ ->

x86/TargetPrinter.ml

@@ -845,6 +845,8 @@ module Target(System: SYSTEM):TARGET =
           fprintf oc "	movw	%a, %a\n" addressing a ireg16 rd
       | Pnop ->
           fprintf oc "	nop\n"
+      | Prep_movsb ->
+	 fprintf oc "	rep	movsb\n"
       | Prep_movsl ->
 	 fprintf oc "	rep	movsl\n"
       | Psbbl_rr (res,a1) ->