aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2018-08-20 10:22:35 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2018-08-20 10:22:35 +0200
commit6fc89e5c8c4a8f98ef0a4a03c00994bbfb146431 (patch)
tree27fd2d801607ee940e5254869c775f3662b4088b
parentec8d93afc8875dcf7dfeb982eab255f150a91074 (diff)
downloadcompcert-6fc89e5c8c4a8f98ef0a4a03c00994bbfb146431.tar.gz
compcert-6fc89e5c8c4a8f98ef0a4a03c00994bbfb146431.zip
Add sizeof_reg and new Machine configurations (#129)
Since the size of integer registers is not identical to the size of pointers for the ppc64 and e5500 model the check for register pairs in ExtendedAsm does not work correctly. In order to avoid this a new field sizeof_intreg is introduced in the Machine configuration which describes the size of integer registers. New configurations for the ppc64 and e5500 model are added and used. Bug 24273
-rw-r--r--cparser/ExtendedAsm.ml2
-rw-r--r--cparser/Machine.ml14
-rw-r--r--cparser/Machine.mli4
-rw-r--r--driver/Frontend.ml10
4 files changed, 25 insertions, 5 deletions
diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml
index 8b694ac4..257e9cf7 100644
--- a/cparser/ExtendedAsm.ml
+++ b/cparser/ExtendedAsm.ml
@@ -73,7 +73,7 @@ let set_label_const lbl pos n subst =
let is_reg_pair env ty =
match unroll env ty with
- | TInt(ik, _) -> sizeof_ikind ik > !config.sizeof_ptr
+ | TInt(ik, _) -> sizeof_ikind ik > !config.sizeof_intreg
| _ -> false
(* Transform the input operands:
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index 4d1e7588..089f2483 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -44,6 +44,7 @@ type t = {
wchar_signed: bool;
sizeof_size_t: int;
sizeof_ptrdiff_t: int;
+ sizeof_intreg: int;
alignof_ptr: int;
alignof_short: int;
alignof_int: int;
@@ -78,6 +79,7 @@ let ilp32ll64 = {
wchar_signed = true;
sizeof_size_t = 4;
sizeof_ptrdiff_t = 4;
+ sizeof_intreg = 4;
alignof_ptr = 4;
alignof_short = 2;
alignof_int = 4;
@@ -112,6 +114,7 @@ let i32lpll64 = {
wchar_signed = true;
sizeof_size_t = 8;
sizeof_ptrdiff_t = 8;
+ sizeof_intreg = 8;
alignof_ptr = 8;
alignof_short = 2;
alignof_int = 4;
@@ -146,6 +149,7 @@ let il32pll64 = {
wchar_signed = true;
sizeof_size_t = 8;
sizeof_ptrdiff_t = 8;
+ sizeof_intreg = 8;
alignof_ptr = 8;
alignof_short = 2;
alignof_int = 4;
@@ -202,11 +206,20 @@ let ppc_32_bigendian =
struct_passing_style = SP_ref_caller;
struct_return_style = SR_int1to8; }
+let ppc_32_r64_bigendian =
+ { ppc_32_bigendian with sizeof_intreg = 8;}
+
let ppc_32_diab_bigendian =
{ ppc_32_bigendian with sizeof_wchar = 2; wchar_signed = false }
+let ppc_32_r64_diab_bigendian =
+ { ppc_32_diab_bigendian with sizeof_intreg = 8;}
+
let ppc_32_linux_bigendian = {ppc_32_bigendian with struct_return_style = SR_ref;}
+let ppc_32_r64_linux_bigendian =
+ { ppc_32_linux_bigendian with sizeof_intreg = 8;}
+
let arm_littleendian =
{ ilp32ll64 with name = "arm"; struct_passing_style = SP_split_args;
struct_return_style = SR_int1to4;}
@@ -254,6 +267,7 @@ let undef = {
wchar_signed = true;
sizeof_size_t = 0;
sizeof_ptrdiff_t = 0;
+ sizeof_intreg = 0;
alignof_ptr = 0;
alignof_short = 0;
alignof_int = 0;
diff --git a/cparser/Machine.mli b/cparser/Machine.mli
index 53c13b52..8971e2a3 100644
--- a/cparser/Machine.mli
+++ b/cparser/Machine.mli
@@ -43,6 +43,7 @@ type t = {
wchar_signed: bool;
sizeof_size_t: int;
sizeof_ptrdiff_t: int;
+ sizeof_intreg: int;
alignof_ptr: int;
alignof_short: int;
alignof_int: int;
@@ -78,6 +79,9 @@ val win64 : t
val ppc_32_bigendian : t
val ppc_32_diab_bigendian : t
val ppc_32_linux_bigendian : t
+val ppc_32_r64_bigendian : t
+val ppc_32_r64_diab_bigendian : t
+val ppc_32_r64_linux_bigendian : t
val arm_littleendian : t
val arm_bigendian : t
val rv32 : t
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index e5b51c1f..88b47854 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -73,10 +73,12 @@ let parse_c_file sourcename ifile =
let init () =
Machine.config:=
begin match Configuration.arch with
- | "powerpc" -> if Configuration.gnu_toolchain
- then if Configuration.abi = "linux"
- then Machine.ppc_32_linux_bigendian
- else Machine.ppc_32_bigendian
+ | "powerpc" -> if Configuration.model = "e5500" || Configuration.model = "ppc64"
+ then if Configuration.abi = "linux" then Machine.ppc_32_r64_linux_bigendian
+ else if Configuration.gnu_toolchain then Machine.ppc_32_r64_bigendian
+ else Machine.ppc_32_r64_diab_bigendian
+ else if Configuration.abi = "linux" then Machine.ppc_32_linux_bigendian
+ else if Configuration.gnu_toolchain then Machine.ppc_32_bigendian
else Machine.ppc_32_diab_bigendian
| "arm" -> if Configuration.is_big_endian
then Machine.arm_bigendian