diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-27 16:57:20 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-27 16:57:20 +0100 |
commit | e096fa7aa6161e1f5a74001185eb3873a684c48d (patch) | |
tree | ca928bcb3f7b6b2237a626fbb1dbc1ce62b2e5d1 /cparser/Machine.ml | |
parent | f00b70b6a17fdfb4e8606df891f6becc8102ef12 (diff) | |
download | compcert-e096fa7aa6161e1f5a74001185eb3873a684c48d.tar.gz compcert-e096fa7aa6161e1f5a74001185eb3873a684c48d.zip |
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.
Diffstat (limited to 'cparser/Machine.ml')
-rw-r--r-- | cparser/Machine.ml | 51 |
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. *) |