diff options
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Clflags.ml | 2 | ||||
-rw-r--r-- | driver/Configuration.ml | 27 | ||||
-rw-r--r-- | driver/Configuration.mli | 57 | ||||
-rw-r--r-- | driver/Driver.ml | 32 |
4 files changed, 116 insertions, 2 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index ead27b36..8899c2b0 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -17,6 +17,8 @@ let linker_options = ref ([]: string list) let assembler_options = ref ([]: string list) let option_flongdouble = ref false let option_fstruct_return = ref false +let option_fstruct_return_style = ref Configuration.struct_return_style +let option_fstruct_passing_style = ref Configuration.struct_passing_style let option_fbitfields = ref false let option_fvararg_calls = ref true let option_funprototyped = ref true diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 48c31767..2cea2b80 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -100,3 +100,30 @@ let advanced_debug = | v -> bad_config "advanced_debug" [v] let version = get_config_string "version" + +type 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 *) + +type struct_return_style = + | SR_int1248 (* return by content if size is 1, 2, 4 or 8 bytes *) + | SR_int1to4 (* return by content if size is <= 4 *) + | SR_int1to8 (* return by content if size is <= 8 *) + | SR_ref (* always return by assignment to a reference + given as extra argument *) + +let struct_passing_style = + match get_config_string "struct_passing_style" with + | "ref-callee" -> SP_ref_callee + | "ref-caller" -> SP_ref_caller + | "ints" -> SP_split_args + | v -> bad_config "struct_passing_style" [v] + +let struct_return_style = + match get_config_string "struct_return_style" with + | "int1248" -> SR_int1248 + | "int1-4" -> SR_int1to4 + | "int1-8" -> SR_int1to8 + | "ref" -> SR_ref + | v -> bad_config "struct_return_style" [v] diff --git a/driver/Configuration.mli b/driver/Configuration.mli new file mode 100644 index 00000000..20c45518 --- /dev/null +++ b/driver/Configuration.mli @@ -0,0 +1,57 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +val arch: string + (** Target architecture *) +val model: string + (** Sub-model for this architecture *) +val abi: string + (** ABI to use *) +val system: string + (** Flavor of operating system that runs CompCert *) + +val prepro: string list + (** How to invoke the external preprocessor *) +val asm: string list + (** How to invoke the external assembler *) +val linker: string list + (** How to invoke the external linker *) +val asm_supports_cfi: bool + (** True if the assembler supports Call Frame Information *) +val stdlib_path: string + (** Path to CompCert's library *) +val has_runtime_lib: bool + (** True if CompCert's library is available. *) +val advanced_debug: bool + (** True if advanced debug is implement for the Target *) + +val version: string + (** CompCert version string *) + +type 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 *) + +type struct_return_style = + | SR_int1248 (* return by content if size is 1, 2, 4 or 8 bytes *) + | SR_int1to4 (* return by content if size is <= 4 *) + | SR_int1to8 (* return by content if size is <= 8 *) + | SR_ref (* always return by assignment to a reference + given as extra argument *) + +val struct_passing_style: struct_passing_style + (** Calling conventions to use for passing structs and unions as + first-class values *) +val struct_return_style: struct_return_style + (** Calling conventions to use for returning structs and unions as + first-class values *) diff --git a/driver/Driver.ml b/driver/Driver.ml index 1191982d..d225ec4f 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -266,6 +266,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; @@ -410,6 +411,10 @@ Language support options (use -fno-<opt> to turn off -f<opt>) : -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=<convention> + Set the calling conventions used to return structs by value + -fstruct-passing=<convention> + 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] @@ -551,7 +556,28 @@ 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 := Configuration.SP_ref_callee); + Exact "-fstruct-passing=ref-caller", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_passing_style := Configuration.SP_ref_caller); + Exact "-fstruct-passing=ints", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_passing_style := Configuration.SP_split_args); + Exact "-fstruct-return=ref", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_return_style := Configuration.SR_ref); + Exact "-fstruct-return=int1248", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_return_style := Configuration.SR_int1248); + Exact "-fstruct-return=int1-4", + Self (fun _ -> option_fstruct_return := true; + 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 *) @@ -608,7 +634,9 @@ let _ = begin match Configuration.arch with | "powerpc" -> Machine.ppc_32_bigendian | "arm" -> Machine.arm_littleendian - | "ia32" -> Machine.x86_32 + | "ia32" -> if Configuration.abi = "macosx" + then Machine.x86_32_macosx + else Machine.x86_32 | _ -> assert false end; Builtins.set C2C.builtins; |