From be4d6e42dfa287b93b1a35ec820ab2a5aaf8c7ec Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 19 May 2013 09:54:40 +0000
Subject: Merge of the float32 branch: - added RTL type "Tsingle" -
 ABI-compatible passing of single-precision floats on ARM and x86

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/Asmgen.v | 36 +++++++++++++++++++++---------------
 1 file changed, 21 insertions(+), 15 deletions(-)

(limited to 'arm/Asmgen.v')

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 1ff28d9..d160b2d 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -419,27 +419,33 @@ Definition indexed_memory_access
 Definition loadind_int (base: ireg) (ofs: int) (dst: ireg) (k: code) :=
   indexed_memory_access (fun base n => Pldr dst base (SAimm n)) mk_immed_mem_word base ofs k.
 
-Definition loadind_float (base: ireg) (ofs: int) (dst: freg) (k: code) :=
-  indexed_memory_access (Pfldd dst) mk_immed_mem_float base ofs k.
-
 Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) :=
   match ty with
-  | Tint   => do r <- ireg_of dst; OK (loadind_int base ofs r k)
-  | Tfloat => do r <- freg_of dst; OK (loadind_float base ofs r k)
-  | Tlong => Error (msg "Asmgen.loadind")
+  | Tint =>
+      do r <- ireg_of dst; OK (loadind_int base ofs r k)
+  | Tfloat =>
+      do r <- freg_of dst;
+      OK (indexed_memory_access (Pfldd r) mk_immed_mem_float base ofs k)
+  | Tsingle =>
+      do r <- freg_of dst;
+      OK (indexed_memory_access (Pflds r) mk_immed_mem_float base ofs k)
+  | Tlong =>
+      Error (msg "Asmgen.loadind")
   end.
 
-Definition storeind_int (src: ireg) (base: ireg) (ofs: int) (k: code) :=
-  indexed_memory_access (fun base n => Pstr src base (SAimm n)) mk_immed_mem_word base ofs k.
-
-Definition storeind_float (src: freg) (base: ireg) (ofs: int) (k: code) :=
-  indexed_memory_access (Pfstd src) mk_immed_mem_float base ofs k.
-
 Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) :=
   match ty with
-  | Tint   => do r <- ireg_of src; OK (storeind_int r base ofs k)
-  | Tfloat => do r <- freg_of src; OK (storeind_float r base ofs k)
-  | Tlong => Error (msg "Asmgen.storeind")
+  | Tint =>
+      do r <- ireg_of src;
+      OK (indexed_memory_access (fun base n => Pstr r base (SAimm n)) mk_immed_mem_word base ofs k)
+  | Tfloat =>
+      do r <- freg_of src;
+      OK (indexed_memory_access (Pfstd r) mk_immed_mem_float base ofs k)
+  | Tsingle =>
+      do r <- freg_of src;
+      OK (indexed_memory_access (Pfsts r) mk_immed_mem_float base ofs k)
+  | Tlong =>
+      Error (msg "Asmgen.storeind")
   end.
 
 (** Translation of memory accesses *)
-- 
cgit v1.2.3