Merge branch 'master' into dwarf

Conflicts:
	Makefile
	driver/Driver.ml

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;