diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-08-17 11:33:24 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-08-17 11:33:24 +0000 |
commit | 9096c5c513aba868970a3e792fd5237d74547c05 (patch) | |
tree | 32b4217ea8391937b642c1df1d703b72c3385339 | |
parent | 3b24f0e0404de0c2c5b1cf64d5a5d6059cd604b6 (diff) | |
download | compcert-9096c5c513aba868970a3e792fd5237d74547c05.tar.gz compcert-9096c5c513aba868970a3e792fd5237d74547c05.zip |
Wrong usage of temps in builtin_volatile_write.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2030 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r-- | ia32/PrintAsm.ml | 19 |
1 files changed, 7 insertions, 12 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index b473464d..d6de2d1b 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -385,27 +385,21 @@ let print_builtin_vload_global oc chunk id ofs args res = (Addrmode(None, None, Coq_inr(id,ofs))) res; fprintf oc "%s end builtin __builtin_volatile_read\n" comment -let print_builtin_vstore_common oc chunk addr src = +let print_builtin_vstore_common oc chunk addr src tmp = match chunk, src with | (Mint8signed | Mint8unsigned), IR src -> if Asmgen.low_ireg src then fprintf oc " movb %a, %a\n" ireg8 src addressing addr else begin - fprintf oc " movl %a, %%ecx\n" ireg src; - fprintf oc " movb %%cl, %a\n" addressing addr + fprintf oc " movl %a, %a\n" ireg src ireg tmp; + fprintf oc " movb %a, %a\n" ireg8 tmp addressing addr end | (Mint16signed | Mint16unsigned), IR src -> - if Asmgen.low_ireg src then - fprintf oc " movw %a, %a\n" ireg16 src addressing addr - else begin - fprintf oc " movl %a, %%ecx\n" ireg src; - fprintf oc " movw %%cx, %a\n" addressing addr - end + fprintf oc " movw %a, %a\n" ireg16 src addressing addr | Mint32, IR src -> fprintf oc " movl %a, %a\n" ireg src addressing addr | Mfloat32, FR src -> - fprintf oc " cvtsd2ss %a, %%xmm7\n" freg src; - fprintf oc " movss %%xmm7, %a\n" addressing addr + fprintf oc " cvtsd2ss %a, %a\n" freg src addressing addr | (Mfloat64 | Mfloat64al32), FR src -> fprintf oc " movsd %a, %a\n" freg src addressing addr | _ -> @@ -417,6 +411,7 @@ let print_builtin_vstore oc chunk args = | [IR addr; src] -> print_builtin_vstore_common oc chunk (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src + (if addr = ECX then EDX else ECD) | _ -> assert false end; @@ -427,7 +422,7 @@ let print_builtin_vstore_global oc chunk id ofs args = begin match args with | [src] -> print_builtin_vstore_common oc chunk - (Addrmode(None, None, Coq_inr(id,ofs))) src + (Addrmode(None, None, Coq_inr(id,ofs))) src EDX | _ -> assert false end; |