Use VFD regs to implement 64-bit mem-mem copies in builtin_memcpy_false.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2616 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 10 insertions, 5 deletions

diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index 1689c77..ffa441b 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -29,7 +29,7 @@ Require Archi.
 -- Callee-save registers, whose value is preserved across a function call.
 -- Caller-save registers that can be modified during a function call.
 
-  We follow the PowerPC application binary interface (ABI) in our choice
+  We follow the ARM application binary interface (EABI) in our choice
   of callee- and caller-save registers.
 *)
 
diff --git a/arm/Machregs.v b/arm/Machregs.v
index 791ccbb..f373b43 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -97,7 +97,7 @@ Definition destroyed_by_jumptable: list mreg :=
 
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
-  | EF_memcpy sz al => if zle sz 32 then nil else R2 :: R3 :: R12 :: nil
+  | EF_memcpy sz al => if zle sz 32 then F7 :: nil else R2 :: R3 :: R12 :: nil
   | _ => nil
   end.
 
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 5c2833f..dfe6bfc 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -368,16 +368,21 @@ let print_annot_val oc txt args res =
   | [IR src], [IR dst] ->
       if dst = src then 0 else (fprintf oc "	mov	%a, %a\n" ireg dst ireg src; 1)
   | [FR src], [FR dst] ->
-      if dst = src then 0 else (fprintf oc "	fcpyd	%a, %a\n" freg dst freg src; 1)
+      if dst = src then 0 else (fprintf oc "	vmov.f64	%a, %a\n" freg dst freg src; 1)
   | _, _ -> assert false
 
 (* Handling of memcpy *)
 
-(* The ARM has strict alignment constraints. *)
+(* The ARM has strict alignment constraints for 2 and 4 byte accesses.
+   8-byte accesses must be 4-aligned. *)
 
 let print_builtin_memcpy_small oc sz al src dst =
   let rec copy ofs sz ninstr =
-    if sz >= 4 && al >= 4 then begin
+    if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin
+      fprintf oc "	vldr	%a, [%a, #%d]\n" freg FR7 ireg src ofs;
+      fprintf oc "	vstr	%a, [%a, #%d]\n" freg FR7 ireg dst ofs;
+      copy (ofs + 8) (sz - 8) (ninstr + 2)
+    end else if sz >= 4 && al >= 4 then begin
       fprintf oc "	ldr	%a, [%a, #%d]\n" ireg IR14 ireg src ofs;
       fprintf oc "	str	%a, [%a, #%d]\n" ireg IR14 ireg dst ofs;
       copy (ofs + 4) (sz - 4) (ninstr + 2)