From e096fa7aa6161e1f5a74001185eb3873a684c48d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 27 Jan 2015 16:57:20 +0100 Subject: ABI compatibility for struct/union function arguments passed by value. The passing of struct/union arguments by value implemented in the verified part of CompCert is not compatible with the ARM, PowerPC and x86 ABI. Here we enrich the StructReturn source-to-source emulation pass so that it implements the calling conventions defined in these ABIs. Plus: for x86, implement the returning of struct/union results by value in a way compatible with the ABI. --- cparser/Machine.mli | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) (limited to 'cparser/Machine.mli') diff --git a/cparser/Machine.mli b/cparser/Machine.mli index b544711f..0fd8431f 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -44,13 +44,27 @@ type t = { alignof_fun: int option; bigendian: bool; bitfields_msb_first: bool; - struct_return_as_int: int + supports_unaligned_accesses: bool; + struct_return_as_int: int; + struct_passing_style: struct_passing_style } +and struct_passing_style = + | SP_ref_callee (* by reference, callee takes copy *) + | SP_ref_caller (* by reference, caller takes copy *) + | SP_split_args (* by value, as a sequence of ints *) + +(* The current configuration *) + +val config : t ref + +(* Canned configurations *) + val ilp32ll64 : t val i32lpll64 : t val il32pll64 : t val x86_32 : t +val x86_32_macosx : t val x86_64 : t val win32 : t val win64 : t @@ -58,5 +72,4 @@ val ppc_32_bigendian : t val arm_littleendian : t val gcc_extensions : t -> t - -val config : t ref +val compcert_interpreter : t -> t -- cgit From 67e8b783c7e794d995675a332f118533e6a9b14a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 14 Mar 2015 10:31:02 +0100 Subject: Improve performance and configurability for the StructReturn pass. configure: special ABI value for IA32/MacOSX and PowerPC/Linux cparser/Machine: special config for PowerPC/Linux cparser/StructReturn: generate better code for return-as-int driver/Clflags, driver/Driver: add options -fstruct-return= and -fstruct-passing= to simplify testing --- cparser/Machine.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'cparser/Machine.mli') diff --git a/cparser/Machine.mli b/cparser/Machine.mli index 0fd8431f..76cea879 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -69,6 +69,7 @@ val x86_64 : t val win32 : t val win64 : t val ppc_32_bigendian : t +val ppc_32_bigendian_linux : t val arm_littleendian : t val gcc_extensions : t -> t -- cgit From cbf8434e44ebd6bc05022d1fbe0400267520184f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 20 Mar 2015 11:25:30 +0100 Subject: Improvements in the StructReturn transformation (ABI conformance for passing composites). - Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD. - Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions. - More comprehensive interoperability test in regression/interop1.c. --- cparser/Machine.mli | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) (limited to 'cparser/Machine.mli') diff --git a/cparser/Machine.mli b/cparser/Machine.mli index 76cea879..fb7321f9 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -44,16 +44,9 @@ type t = { alignof_fun: int option; bigendian: bool; bitfields_msb_first: bool; - supports_unaligned_accesses: bool; - struct_return_as_int: int; - struct_passing_style: struct_passing_style + supports_unaligned_accesses: bool } -and struct_passing_style = - | SP_ref_callee (* by reference, callee takes copy *) - | SP_ref_caller (* by reference, caller takes copy *) - | SP_split_args (* by value, as a sequence of ints *) - (* The current configuration *) val config : t ref @@ -69,7 +62,6 @@ val x86_64 : t val win32 : t val win64 : t val ppc_32_bigendian : t -val ppc_32_bigendian_linux : t val arm_littleendian : t val gcc_extensions : t -> t -- cgit