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.

5 files changed, 96 insertions, 19 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index c90ff1a9..8899c2b0 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -17,8 +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 (None: int option)
-let option_fstruct_passing_style = ref (None: Machine.struct_passing_style option)
+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 0012dc0c..237085de 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -94,3 +94,30 @@ let asm_supports_cfi =
   | v -> bad_config "asm_supports_cfi" [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..875bd692
--- /dev/null
+++ b/driver/Configuration.mli
@@ -0,0 +1,55 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 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 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
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 3ad0df8a..2725dbfe 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -366,7 +366,6 @@ let do_printf m fmt args =
 
 let (>>=) opt f = match opt with None -> None | Some arg -> f arg
 
-(*
 (* Like eventval_of_val, but accepts static globals as well *)
 
 let convert_external_arg ge v t =
@@ -386,7 +385,6 @@ let rec convert_external_args ge vl tl =
       convert_external_arg ge v1 t1 >>= fun e1 ->
       convert_external_args ge vl tl >>= fun el -> Some (e1 :: el)
   | _, _ -> None
-*)
 
 let do_external_function id sg ge w args m =
   match extern_atom id, args with
@@ -394,12 +392,8 @@ let do_external_function id sg ge w args m =
       extract_string m b ofs >>= fun fmt ->
       print_string (do_printf m fmt args');
       flush stdout;
-      Some(((w, [Event_syscall(id, [], EVint Int.zero)]), Vint Int.zero), m)
-(*
       convert_external_args ge args sg.sig_args >>= fun eargs ->
       Some(((w, [Event_syscall(id, eargs, EVint Int.zero)]), Vint Int.zero), m)
-*)
-
   | _ ->
       None