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. --- driver/Driver.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 5d4c2f9c..31d5096b 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -241,6 +241,7 @@ let process_c_file sourcename = let preproname = Filename.temp_file "compcert" ".i" in preprocess sourcename preproname; if !option_interp then begin + Machine.config := Machine.compcert_interpreter !Machine.config; let csyntax = parse_c_file sourcename preproname in safe_remove preproname; Interp.execute csyntax; @@ -583,7 +584,9 @@ let _ = begin match Configuration.arch with | "powerpc" -> Machine.ppc_32_bigendian | "arm" -> Machine.arm_littleendian - | "ia32" -> Machine.x86_32 + | "ia32" -> if Configuration.system = "macosx" + then Machine.x86_32_macosx + else Machine.x86_32 | _ -> assert false end; Builtins.set C2C.builtins; -- 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 --- driver/Driver.ml | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 31d5096b..1af66f2c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -386,6 +386,10 @@ Language support options (use -fno- to turn off -f) : -fbitfields Emulate bit fields in structs [off] -flongdouble Treat 'long double' as 'double' [off] -fstruct-return Emulate returning structs and unions by value [off] + -fstruct-return= + Set the calling conventions used to return structs by value + -fstruct-passing= + Set the calling conventions used to pass structs by value -fvararg-calls Support calls to variable-argument functions [on] -funprototyped Support calls to old-style functions without prototypes [on] -fpacked-structs Emulate packed structs [off] @@ -527,7 +531,25 @@ let cmdline_actions = Exact "-quiet", Self (fun _ -> Interp.trace := 0); Exact "-trace", Self (fun _ -> Interp.trace := 2); Exact "-random", Self (fun _ -> Interp.mode := Interp.Random); - Exact "-all", Self (fun _ -> Interp.mode := Interp.All) + Exact "-all", Self (fun _ -> Interp.mode := Interp.All); +(* Special -f options *) + Exact "-fstruct-passing=ref-callee", + Self (fun _ -> option_fstruct_passing_style := Some Machine.SP_ref_callee); + Exact "-fstruct-passing=ref-caller", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_passing_style := Some Machine.SP_ref_caller); + Exact "-fstruct-passing=ints", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_passing_style := Some Machine.SP_split_args); + Exact "-fstruct-return=ref", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_return_style := Some 0); + Exact "-fstruct-return=int4", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_return_style := Some 4); + Exact "-fstruct-return=int8", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_return_style := Some 8) ] (* -f options: come in -f and -fno- variants *) (* Language support options *) @@ -582,9 +604,11 @@ let _ = Printexc.record_backtrace true; Machine.config := begin match Configuration.arch with - | "powerpc" -> Machine.ppc_32_bigendian + | "powerpc" -> if Configuration.abi = "linux" + then Machine.ppc_32_bigendian_linux + else Machine.ppc_32_bigendian | "arm" -> Machine.arm_littleendian - | "ia32" -> if Configuration.system = "macosx" + | "ia32" -> if Configuration.abi = "macosx" then Machine.x86_32_macosx else Machine.x86_32 | _ -> assert false -- 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. --- driver/Driver.ml | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index e3ad4549..ad7cf61e 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -558,22 +558,25 @@ let cmdline_actions = Exact "-all", Self (fun _ -> Interp.mode := Interp.All); (* Special -f options *) Exact "-fstruct-passing=ref-callee", - Self (fun _ -> option_fstruct_passing_style := Some Machine.SP_ref_callee); + Self (fun _ -> option_fstruct_passing_style := Configuration.SP_ref_callee); Exact "-fstruct-passing=ref-caller", Self (fun _ -> option_fstruct_return := true; - option_fstruct_passing_style := Some Machine.SP_ref_caller); + option_fstruct_passing_style := Configuration.SP_ref_caller); Exact "-fstruct-passing=ints", Self (fun _ -> option_fstruct_return := true; - option_fstruct_passing_style := Some Machine.SP_split_args); + option_fstruct_passing_style := Configuration.SP_split_args); Exact "-fstruct-return=ref", Self (fun _ -> option_fstruct_return := true; - option_fstruct_return_style := Some 0); - Exact "-fstruct-return=int4", + option_fstruct_return_style := Configuration.SR_ref); + Exact "-fstruct-return=int1248", Self (fun _ -> option_fstruct_return := true; - option_fstruct_return_style := Some 4); - Exact "-fstruct-return=int8", + option_fstruct_return_style := Configuration.SR_int1248); + Exact "-fstruct-return=int1-4", Self (fun _ -> option_fstruct_return := true; - option_fstruct_return_style := Some 8) + option_fstruct_return_style := Configuration.SR_int1to4); + Exact "-fstruct-return=int1-8", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_return_style := Configuration.SR_int1to8) ] (* -f options: come in -f and -fno- variants *) (* Language support options *) @@ -628,9 +631,7 @@ let _ = Printexc.record_backtrace true; Machine.config := begin match Configuration.arch with - | "powerpc" -> if Configuration.abi = "linux" - then Machine.ppc_32_bigendian_linux - else Machine.ppc_32_bigendian + | "powerpc" -> Machine.ppc_32_bigendian | "arm" -> Machine.arm_littleendian | "ia32" -> if Configuration.abi = "macosx" then Machine.x86_32_macosx -- cgit