Commit fbdff974 authored by xleroy's avatar xleroy
Browse files

Revert suppression of __builtin_{read,write}_reversed for x86 and ARM,

for compatibility with earlier CompCert versions.
But don't use them in PackedStructs.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2216 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent e1fc4beb
......@@ -31,7 +31,16 @@ let builtins = {
(TInt(IUInt, []), [TInt(IUInt, [])], false);
(* Float arithmetic *)
"__builtin_fsqrt",
(TFloat(FDouble, []), [TFloat(FDouble, [])], false)
(TFloat(FDouble, []), [TFloat(FDouble, [])], false);
(* Memory accesses *)
"__builtin_read16_reversed",
(TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false);
"__builtin_read32_reversed",
(TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false);
"__builtin_write16_reversed",
(TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
"__builtin_write32_reversed",
(TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
]
}
......@@ -388,6 +388,19 @@ let print_builtin_inline oc name args res =
end else begin
fprintf oc " umull %a, %a, %a, %a\n" ireg rl ireg rh ireg a ireg b; 1
end
(* Memory accesses *)
| "__builtin_read16_reversed", [IR a1], [IR res] ->
fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg a1;
fprintf oc " rev16 %a, %a\n" ireg res ireg res; 2
| "__builtin_read32_reversed", [IR a1], [IR res] ->
fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg a1;
fprintf oc " rev %a, %a\n" ireg res ireg res; 2
| "__builtin_write16_reversed", [IR a1; IR a2], _ ->
fprintf oc " rev16 %a, %a\n" ireg IR14 ireg a2;
fprintf oc " strh %a, [%a, #0]\n" ireg IR14 ireg a1; 2
| "__builtin_write32_reversed", [IR a1; IR a2], _ ->
fprintf oc " rev %a, %a\n" ireg IR14 ireg a2;
fprintf oc " str %a, [%a, #0]\n" ireg IR14 ireg a1; 2
(* Catch-all *)
| _ ->
invalid_arg ("unrecognized builtin " ^ name)
......
......@@ -16,6 +16,7 @@
(* Machine-dependent aspects *)
type t = {
name: string;
char_signed: bool;
sizeof_ptr: int;
sizeof_short: int;
......@@ -45,6 +46,7 @@ type t = {
}
let ilp32ll64 = {
name = "ilp32ll64";
char_signed = false;
sizeof_ptr = 4;
sizeof_short = 2;
......@@ -74,6 +76,7 @@ let ilp32ll64 = {
}
let i32lpll64 = {
name = "i32lpll64";
char_signed = false;
sizeof_ptr = 8;
sizeof_short = 2;
......@@ -103,6 +106,7 @@ let i32lpll64 = {
}
let il32pll64 = {
name = "il32pll64";
char_signed = false;
sizeof_ptr = 8;
sizeof_short = 2;
......@@ -133,11 +137,15 @@ let il32pll64 = {
(* Canned configurations for some ABIs *)
let x86_32 = { ilp32ll64 with char_signed = true }
let x86_64 = { i32lpll64 with char_signed = true }
let win64 = { il32pll64 with char_signed = true }
let ppc_32_bigendian = { ilp32ll64 with bigendian = true; bitfields_msb_first = true }
let arm_littleendian = ilp32ll64
let x86_32 =
{ ilp32ll64 with char_signed = true; name = "x86_32" }
let x86_64 =
{ i32lpll64 with char_signed = true; name = "x86_64" }
let win64 =
{ il32pll64 with char_signed = true; name = "x86_64" }
let ppc_32_bigendian =
{ ilp32ll64 with bigendian = true; bitfields_msb_first = true; name = "powerpc" }
let arm_littleendian = { ilp32ll64 with name = "arm" }
(* Add GCC extensions re: sizeof and alignof *)
......
......@@ -16,6 +16,7 @@
(* Machine-dependent aspects *)
type t = {
name: string;
char_signed: bool;
sizeof_ptr: int;
sizeof_short: int;
......
......@@ -197,25 +197,31 @@ let arrow_packed_field base pf ty =
(* (ty) __builtin_readNN_reversed(&lval)
or (ty) __builtin_bswapNN(lval) *)
let use_reversed =
match !Machine.config.Machine.name with
| "powerpc" -> true
| _ -> false
let bswap_read loc env lval =
let ty = lval.etyp in
let (bsize, aty) = accessor_type loc env ty in
assert (bsize = 16 || bsize = 32);
try
let (id, fty) =
lookup_function loc env (sprintf "__builtin_read%d_reversed" bsize) in
let fn = {edesc = EVar id; etyp = fty} in
let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lval)] in
let call = {edesc = ECall(fn, args); etyp = aty} in
ecast_opt env ty call
with Env.Error _ ->
try
let (id, fty) =
lookup_function loc env (sprintf "__builtin_bswap%d" bsize) in
let fn = {edesc = EVar id; etyp = fty} in
let args = [ecast_opt env aty lval] in
let call = {edesc = ECall(fn, args); etyp = aty} in
ecast_opt env ty call
if use_reversed then begin
let (id, fty) =
lookup_function loc env (sprintf "__builtin_read%d_reversed" bsize) in
let fn = {edesc = EVar id; etyp = fty} in
let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lval)] in
let call = {edesc = ECall(fn, args); etyp = aty} in
ecast_opt env ty call
end else begin
let (id, fty) =
lookup_function loc env (sprintf "__builtin_bswap%d" bsize) in
let fn = {edesc = EVar id; etyp = fty} in
let args = [ecast_opt env aty lval] in
let call = {edesc = ECall(fn, args); etyp = aty} in
ecast_opt env ty call
end
with Env.Error msg ->
fatal_error "%a: Error: %s" formatloc loc (Env.error_message msg)
......@@ -228,20 +234,21 @@ let bswap_write loc env lhs rhs =
accessor_type loc env ty in
assert (bsize = 16 || bsize = 32);
try
let (id, fty) =
lookup_function loc env (sprintf "__builtin_write%d_reversed" bsize) in
let fn = {edesc = EVar id; etyp = fty} in
let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lhs);
ecast_opt env aty rhs] in
{edesc = ECall(fn, args); etyp = TVoid[]}
with Env.Error _ ->
try
let (id, fty) =
lookup_function loc env (sprintf "__builtin_bswap%d" bsize) in
let fn = {edesc = EVar id; etyp = fty} in
let args = [ecast_opt env aty rhs] in
let call = {edesc = ECall(fn, args); etyp = aty} in
eassign lhs (ecast_opt env ty call)
if use_reversed then begin
let (id, fty) =
lookup_function loc env (sprintf "__builtin_write%d_reversed" bsize) in
let fn = {edesc = EVar id; etyp = fty} in
let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lhs);
ecast_opt env aty rhs] in
{edesc = ECall(fn, args); etyp = TVoid[]}
end else begin
let (id, fty) =
lookup_function loc env (sprintf "__builtin_bswap%d" bsize) in
let fn = {edesc = EVar id; etyp = fty} in
let args = [ecast_opt env aty rhs] in
let call = {edesc = ECall(fn, args); etyp = aty} in
eassign lhs (ecast_opt env ty call)
end
with Env.Error msg ->
fatal_error "%a: Error: %s" formatloc loc (Env.error_message msg)
......
......@@ -33,6 +33,15 @@ let builtins = {
"__builtin_fmax",
(TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
"__builtin_fmin",
(TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false)
(TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
(* Memory accesses *)
"__builtin_read16_reversed",
(TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false);
"__builtin_read32_reversed",
(TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false);
"__builtin_write16_reversed",
(TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
"__builtin_write32_reversed",
(TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
]
}
......@@ -101,6 +101,11 @@ Definition destroyed_by_cond (cond: condition): list mreg :=
Definition destroyed_by_jumptable: list mreg :=
nil.
Local Open Scope string_scope.
Definition builtin_write16_reversed := ident_of_string "__builtin_write16_reversed".
Definition builtin_write32_reversed := ident_of_string "__builtin_write32_reversed".
Definition destroyed_by_builtin (ef: external_function): list mreg :=
match ef with
| EF_memcpy sz al =>
......@@ -109,6 +114,10 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
| EF_vstore Mfloat32 => X7 :: nil
| EF_vstore_global (Mint8unsigned|Mint8signed) _ _ => AX :: nil
| EF_vstore_global Mfloat32 _ _ => X7 :: nil
| EF_builtin id sg =>
if ident_eq id builtin_write16_reversed
|| ident_eq id builtin_write32_reversed
then CX :: DX :: nil else nil
| _ => nil
end.
......@@ -131,8 +140,6 @@ Definition mregs_for_operation (op: operation): list (option mreg) * option mreg
| _ => (nil, None)
end.
Local Open Scope string_scope.
Definition builtin_negl := ident_of_string "__builtin_negl".
Definition builtin_addl := ident_of_string "__builtin_addl".
Definition builtin_subl := ident_of_string "__builtin_subl".
......
......@@ -442,6 +442,25 @@ let print_builtin_inline oc name args res =
| "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
assert (a = EAX && b = EDX && rh = EDX && rl = EAX);
fprintf oc " mull %a\n" ireg EDX
(* Memory accesses *)
| "__builtin_read16_reversed", [IR a1], [IR res] ->
fprintf oc " movzwl 0(%a), %a\n" ireg a1 ireg res;
fprintf oc " rolw $8, %a\n" ireg16 res
| "__builtin_read32_reversed", [IR a1], [IR res] ->
fprintf oc " movl 0(%a), %a\n" ireg a1 ireg res;
fprintf oc " bswap %a\n" ireg res
| "__builtin_write16_reversed", [IR a1; IR a2], _ ->
let tmp = if a1 = ECX then EDX else ECX in
if a2 <> tmp then
fprintf oc " movl %a, %a\n" ireg a2 ireg tmp;
fprintf oc " xchg %a, %a\n" ireg8 tmp high_ireg8 tmp;
fprintf oc " movw %a, 0(%a)\n" ireg16 tmp ireg a1
| "__builtin_write32_reversed", [IR a1; IR a2], _ ->
let tmp = if a1 = ECX then EDX else ECX in
if a2 <> tmp then
fprintf oc " movl %a, %a\n" ireg a2 ireg tmp;
fprintf oc " bswap %a\n" ireg tmp;
fprintf oc " movl %a, 0(%a)\n" ireg tmp ireg a1
(* Catch-all *)
| _ ->
invalid_arg ("unrecognized builtin " ^ name)
......
......@@ -2,3 +2,7 @@ bswap(12345678) = 78563412
bswap16(1234) = 3412
cntlz(12345678) = 3
fsqrt(3.141590) = 1.772453
read_16_rev = 3412
read_32_rev = efbeadde
after write_16_rev: 9a78
after write_32_rev: 78563412
......@@ -3,3 +3,7 @@ bswap16(1234) = 3412
fsqrt(3.141590) = 1.772453
fmin(3.141590, 2.718000) = 2.718000
fmax(3.141590, 2.718000) = 3.141590
read_16_rev = 3412
read_32_rev = efbeadde
after write_16_rev: 9a78
after write_32_rev: 78563412
......@@ -14,6 +14,13 @@ int main(int argc, char ** argv)
printf("cntlz(%x) = %d\n", x, __builtin_cntlz(x));
printf("fsqrt(%f) = %f\n", a, __builtin_fsqrt(a));
printf ("read_16_rev = %x\n", __builtin_read16_reversed(&s));
printf ("read_32_rev = %x\n", __builtin_read32_reversed(&y));
__builtin_write16_reversed(&s, 0x789A);
printf ("after write_16_rev: %x\n", s);
__builtin_write32_reversed(&y, 0x12345678);
printf ("after write_32_rev: %x\n", y);
return 0;
}
......
......@@ -5,6 +5,7 @@
int main(int argc, char ** argv)
{
unsigned int x = 0x12345678;
unsigned int y = 0xDEADBEEF;
double a = 3.14159;
double b = 2.718;
unsigned short s = 0x1234;
......@@ -16,6 +17,13 @@ int main(int argc, char ** argv)
printf("fmin(%f, %f) = %f\n", a, b, __builtin_fmin(a, b));
printf("fmax(%f, %f) = %f\n", a, b, __builtin_fmax(a, b));
printf ("read_16_rev = %x\n", __builtin_read16_reversed(&s));
printf ("read_32_rev = %x\n", __builtin_read32_reversed(&y));
__builtin_write16_reversed(&s, 0x789A);
printf ("after write_16_rev: %x\n", s);
__builtin_write32_reversed(&y, 0x12345678);
printf ("after write_32_rev: %x\n", y);
return 0;
}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment