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.

1 files changed, 43 insertions, 8 deletions

diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index b215505b..4f530fde 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -44,9 +44,16 @@ 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
+  | SP_ref_caller
+  | SP_split_args
+
 let ilp32ll64 = {
   name = "ilp32ll64";
   char_signed = false;
@@ -76,7 +83,9 @@ let ilp32ll64 = {
   alignof_fun = None;
   bigendian = false;
   bitfields_msb_first = false;
-  struct_return_as_int = 0
+  supports_unaligned_accesses = false;
+  struct_return_as_int = 0;
+  struct_passing_style = SP_ref_callee
 }
 
 let i32lpll64 = {
@@ -108,7 +117,9 @@ let i32lpll64 = {
   alignof_fun = None;
   bigendian = false;
   bitfields_msb_first = false;
-  struct_return_as_int = 0
+  supports_unaligned_accesses = false;
+  struct_return_as_int = 0;
+  struct_passing_style = SP_ref_callee
 }
 
 let il32pll64 = {
@@ -140,7 +151,9 @@ let il32pll64 = {
   alignof_fun = None;
   bigendian = false;
   bitfields_msb_first = false;
-  struct_return_as_int = 0
+  supports_unaligned_accesses = false;
+  struct_return_as_int = 0;
+  struct_passing_style = SP_ref_callee
 }
 
 (* Canned configurations for some ABIs *)
@@ -149,9 +162,17 @@ let x86_32 =
   { ilp32ll64 with name = "x86_32";
                    char_signed = true;
                    alignof_longlong = 4; alignof_double = 4;
-                   sizeof_longdouble = 12; alignof_longdouble = 4 }
+                   sizeof_longdouble = 12; alignof_longdouble = 4;
+                   supports_unaligned_accesses = true;
+                   struct_passing_style = SP_split_args }
+
+let x86_32_macosx =
+  { x86_32 with sizeof_longdouble = 16; alignof_longdouble = 16;
+                struct_return_as_int = 8 }
+
 let x86_64 =
   { i32lpll64 with name = "x86_64"; char_signed = true }
+
 let win32 =
   { ilp32ll64 with name = "win32"; char_signed = true;
                    sizeof_wchar = 2; wchar_signed = false }
@@ -162,10 +183,14 @@ let ppc_32_bigendian =
   { ilp32ll64 with name = "powerpc";
                    bigendian = true;
                    bitfields_msb_first = true;
-                   struct_return_as_int = 8 }
+                   supports_unaligned_accesses = true;
+                   struct_return_as_int = 8;
+                   struct_passing_style = SP_ref_caller }
+
 let arm_littleendian =
   { ilp32ll64 with name = "arm";
-                   struct_return_as_int = 4 }
+                   struct_return_as_int = 4;
+                   struct_passing_style = SP_split_args }
 
 (* Add GCC extensions re: sizeof and alignof *)
 
@@ -173,6 +198,14 @@ let gcc_extensions c =
   { c with sizeof_void = Some 1; sizeof_fun = Some 1;
            alignof_void = Some 1; alignof_fun = Some 1 }
 
+(* Normalize configuration for use with the CompCert reference interpreter *)
+
+let compcert_interpreter c =
+  { c with sizeof_longdouble = 8; alignof_longdouble = 8;
+           supports_unaligned_accesses = false;
+           struct_return_as_int = 0;
+           struct_passing_style = SP_ref_callee }
+
 (* Undefined configuration *)
 
 let undef = {
@@ -204,7 +237,9 @@ let undef = {
   alignof_fun = None;
   bigendian = false;
   bitfields_msb_first = false;
-  struct_return_as_int = 0
+  supports_unaligned_accesses = false;
+  struct_return_as_int = 0;
+  struct_passing_style = SP_ref_callee
 }
 
 (* The current configuration.  Must be initialized before use. *)