From 7998ccfd709b97f1a2306df4570365d58a5bb4b5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 12 Jan 2014 10:48:56 +0000 Subject: - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4. - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asm.v | 4 ++-- arm/Asmgen.v | 4 ++-- arm/PrintAsm.ml | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) (limited to 'arm') diff --git a/arm/Asm.v b/arm/Asm.v index 76e8196..69f6319 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -615,11 +615,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfcvtsd r1 r2 => Next (nextinstr (rs#r1 <- (Val.singleoffloat rs#r2))) m | Pfldd r1 r2 n => - exec_load Mfloat64al32 (Val.add rs#r2 (Vint n)) r1 rs m + exec_load Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m | Pflds r1 r2 n => exec_load Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m | Pfstd r1 r2 n => - exec_store Mfloat64al32 (Val.add rs#r2 (Vint n)) r1 rs m + exec_store Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m | Pfsts r1 r2 n => match exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m with | Next rs' m' => Next (rs'#FR6 <- Vundef) m' diff --git a/arm/Asmgen.v b/arm/Asmgen.v index b6cb2b3..fcc5061 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -542,7 +542,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) transl_memory_access_int Pldr mk_immed_mem_word dst addr args k | Mfloat32 => transl_memory_access_float Pflds mk_immed_mem_float dst addr args k - | Mfloat64 | Mfloat64al32 => + | Mfloat64 => transl_memory_access_float Pfldd mk_immed_mem_float dst addr args k | Mint64 => Error (msg "Asmgen.transl_load") @@ -563,7 +563,7 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) transl_memory_access_int Pstr mk_immed_mem_word src addr args k | Mfloat32 => transl_memory_access_float Pfsts mk_immed_mem_float src addr args k - | Mfloat64 | Mfloat64al32 => + | Mfloat64 => transl_memory_access_float Pfstd mk_immed_mem_float src addr args k | Mint64 => Error (msg "Asmgen.transl_store") diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 99dfa46..01b881f 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -350,7 +350,7 @@ let print_builtin_vload_common oc chunk args res = | Mfloat32, [IR addr], [FR res] -> fprintf oc " flds %a, [%a, #0]\n" freg_single res ireg addr; fprintf oc " fcvtds %a, %a\n" freg res freg_single res; 2 - | (Mfloat64 | Mfloat64al32), [IR addr], [FR res] -> + | Mfloat64, [IR addr], [FR res] -> fprintf oc " fldd %a, [%a, #0]\n" freg res ireg addr; 1 | _ -> assert false @@ -381,7 +381,7 @@ let print_builtin_vstore_common oc chunk args = | Mfloat32, [IR addr; FR src] -> fprintf oc " fcvtsd %a, %a\n" freg_single FR6 freg src; fprintf oc " fsts %a, [%a, #0]\n" freg_single FR6 ireg addr; 2 - | (Mfloat64 | Mfloat64al32), [IR addr; FR src] -> + | Mfloat64, [IR addr; FR src] -> fprintf oc " fstd %a, [%a, #0]\n" freg src ireg addr; 1 | _ -> assert false -- cgit v1.2.3