aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--cfrontend/C2C.ml50
-rwxr-xr-xconfigure36
-rw-r--r--cparser/Cutil.ml80
-rw-r--r--cparser/Cutil.mli9
-rw-r--r--cparser/Machine.ml30
-rw-r--r--cparser/Machine.mli12
-rw-r--r--cparser/StructReturn.ml435
-rw-r--r--cparser/Unblock.ml2
-rw-r--r--driver/Clflags.ml2
-rw-r--r--driver/Configuration.ml27
-rw-r--r--driver/Configuration.mli55
-rw-r--r--driver/Driver.ml32
-rw-r--r--ia32/TargetPrinter.ml19
-rw-r--r--runtime/arm/vararg.S12
-rw-r--r--runtime/ia32/vararg.S12
-rw-r--r--runtime/powerpc/vararg.s7
-rw-r--r--test/regression/Makefile9
-rw-r--r--test/regression/Results/interop190
-rw-r--r--test/regression/Results/varargs24
-rw-r--r--test/regression/interop1.c286
-rw-r--r--test/regression/varargs2.c16
22 files changed, 1115 insertions, 112 deletions
diff --git a/Makefile b/Makefile
index 6fd8d2a6..820908b0 100644
--- a/Makefile
+++ b/Makefile
@@ -203,6 +203,8 @@ compcert.ini: Makefile.config VERSION
echo "system=$(SYSTEM)"; \
echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \
echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \
+ echo "struct_passing_style=$(STRUCT_PASSING)"; \
+ echo "struct_return_style=$(STRUCT_RETURN)"; \
version=`cat VERSION`; \
echo version=$$version) \
> compcert.ini
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 2b9a54a4..4cb4ded6 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -199,6 +199,10 @@ let builtins_generic = {
(TFloat(FDouble, []),
[TPtr(TVoid [], [])],
false);
+ "__compcert_va_composite",
+ (TPtr(TVoid [], []),
+ [TPtr(TVoid [], []); TInt(IUInt, [])],
+ false);
(* Helper functions for int64 arithmetic *)
"__i64_dtos",
(TInt(ILongLong, []),
@@ -381,26 +385,46 @@ let va_list_ptr e =
| Evalof(e', _) -> Eaddrof(e', Tpointer(typeof e, noattr))
| _ -> error "bad use of a va_list object"; e
-let make_builtin_va_arg env ty e =
- let (helper, ty_ret) =
- match ty with
- | Tint _ | Tpointer _ ->
- ("__compcert_va_int32", Tint(I32, Unsigned, noattr))
- | Tlong _ ->
- ("__compcert_va_int64", Tlong(Unsigned, noattr))
- | Tfloat _ ->
- ("__compcert_va_float64", Tfloat(F64, noattr))
- | _ ->
- unsupported "va_arg at this type";
- ("", Tvoid) in
+let make_builtin_va_arg_by_val helper ty ty_ret arg =
let ty_fun =
Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, cc_default) in
Ecast
(Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun),
- Econs(va_list_ptr e, Enil),
+ Econs(va_list_ptr arg, Enil),
ty_ret),
ty)
+let make_builtin_va_arg_by_ref helper ty arg =
+ let ty_fun =
+ Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil),
+ Tpointer(Tvoid, noattr), cc_default) in
+ let ty_ptr =
+ Tpointer(ty, noattr) in
+ let call =
+ Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun),
+ Econs(va_list_ptr arg,
+ Econs(Esizeof(ty, Tint(I32, Unsigned, noattr)), Enil)),
+ Tpointer(Tvoid, noattr)) in
+ Evalof(Ederef(Ecast(call, ty_ptr), ty), ty)
+
+let make_builtin_va_arg env ty e =
+ match ty with
+ | Tint _ | Tpointer _ ->
+ make_builtin_va_arg_by_val
+ "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e
+ | Tlong _ ->
+ make_builtin_va_arg_by_val
+ "__compcert_va_int64" ty (Tlong(Unsigned, noattr)) e
+ | Tfloat _ ->
+ make_builtin_va_arg_by_val
+ "__compcert_va_float64" ty (Tfloat(F64, noattr)) e
+ | Tstruct _ | Tunion _ ->
+ make_builtin_va_arg_by_ref
+ "__compcert_va_composite" ty e
+ | _ ->
+ unsupported "va_arg at this type";
+ Eval(Vint(coqint_of_camlint 0l), type_int32s)
+
(** ** Translation functions *)
(** Constants *)
diff --git a/configure b/configure
index f9591c0b..53d43832 100755
--- a/configure
+++ b/configure
@@ -79,12 +79,19 @@ done
cchecklink=false
casmruntime=""
asm_supports_cfi=""
+struct_passing=""
+struct_return=""
case "$target" in
powerpc-linux|ppc-linux|powerpc-eabi|ppc-eabi)
arch="powerpc"
model="standard"
abi="eabi"
+ struct_passing="ref-caller"
+ case "$target" in
+ *-linux) struct_return="ref";;
+ *-eabi) struct_return="int1-8";;
+ esac
system="linux"
cc="${toolprefix}gcc"
cprepro="${toolprefix}gcc -U__GNUC__ -E"
@@ -97,6 +104,8 @@ case "$target" in
arch="powerpc"
model="standard"
abi="eabi"
+ struct_passing="ref-caller"
+ struct_return="int1-8"
system="diab"
cc="${toolprefix}dcc"
cprepro="${toolprefix}dcc -E"
@@ -125,6 +134,8 @@ case "$target" in
echo "$usage" 1>&2
exit 2;;
esac
+ struct_passing="ints"
+ struct_return="int1-4"
system="linux"
cc="${toolprefix}gcc"
cprepro="${toolprefix}gcc -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E"
@@ -135,6 +146,8 @@ case "$target" in
arch="ia32"
model="sse2"
abi="standard"
+ struct_passing="ints"
+ struct_return="ref"
system="linux"
cc="${toolprefix}gcc -m32"
cprepro="${toolprefix}gcc -m32 -U__GNUC__ -E"
@@ -145,6 +158,8 @@ case "$target" in
arch="ia32"
model="sse2"
abi="standard"
+ struct_passing="ints"
+ struct_return="int1248" # to check!
system="bsd"
cc="${toolprefix}gcc -m32"
cprepro="${toolprefix}gcc -m32 -U__GNUC__ -E"
@@ -154,7 +169,9 @@ case "$target" in
ia32-macosx)
arch="ia32"
model="sse2"
- abi="standard"
+ abi="macosx"
+ struct_passing="ints"
+ struct_return="int1248"
system="macosx"
cc="${toolprefix}gcc -arch i386"
cprepro="${toolprefix}gcc -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' -E"
@@ -170,6 +187,8 @@ case "$target" in
arch="ia32"
model="sse2"
abi="standard"
+ struct_passing="ints"
+ struct_return="ref"
system="cygwin"
cc="${toolprefix}gcc -m32"
cprepro="${toolprefix}gcc -m32 -U__GNUC__ -E"
@@ -326,6 +345,8 @@ cat >> Makefile.config <<EOF
ARCH=$arch
MODEL=$model
ABI=$abi
+STRUCT_PASSING=$struct_passing
+STRUCT_RETURN=$struct_return
SYSTEM=$system
CC=$cc
CPREPRO=$cprepro
@@ -362,9 +383,19 @@ MODEL=
# ABI=standard # for IA32
ABI=
+# Default calling conventions for passing structs and unions by value
+# See options -fstruct-passing=<style> and -fstruct-return=<style>
+# in the CompCert user's manual
+STRUCT_PASSING=ref_callee
+# STRUCT_PASSING=ref_caller
+# STRUCT_PASSING=ints
+STRUCT_RETURN=ref
+# STRUCT_RETURN=int1248
+# STRUCT_RETURN=int1-4
+# STRUCT_RETURN=int1-8
+
# Target operating system and development environment
# Possible choices for PowerPC:
-# SYSTEM=macosx
# SYSTEM=linux
# SYSTEM=diab
# Possible choices for ARM:
@@ -425,6 +456,7 @@ CompCert configuration:
Target architecture........... $arch
Hardware model................ $model
Application binary interface.. $abi
+ Composite passing conventions. arguments: $struct_passing, return values: $struct_return
OS and development env........ $system
C compiler.................... $cc
C preprocessor................ $cprepro
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 9e7f102e..4d6d2137 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -834,9 +834,23 @@ let nullconst = ecast (TPtr(TVoid [], [])) (intconst 0L IInt)
let eassign e1 e2 = { edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp }
-(* Construct a "," expression *)
+(* Construct a "," expression. Reassociate to the left so that
+ it prints more nicely. *)
-let ecomma e1 e2 = { edesc = EBinop(Ocomma, e1, e2, e2.etyp); etyp = e2.etyp }
+let rec ecomma e1 e2 =
+ match e2.edesc with
+ | EBinop(Ocomma, e2', e2'', _) ->
+ ecomma (ecomma e1 e2') e2''
+ | _ ->
+ { edesc = EBinop(Ocomma, e1, e2, e2.etyp); etyp = e2.etyp }
+
+(* Construct a cascade of "," expressions.
+ Associate to the left so that it prints more nicely. *)
+
+let ecommalist el e =
+ match el with
+ | [] -> e
+ | e1 :: el -> ecomma (List.fold_left ecomma e1 el) e
(* Construct an address-of expression. Can be applied not just to
an l-value but also to a sequence or a conditional of l-values. *)
@@ -910,3 +924,65 @@ let rec default_init env ty =
end
| _ ->
assert false
+
+(* Substitution of variables by expressions *)
+
+let rec subst_expr phi e =
+ match e.edesc with
+ | EConst _ | ESizeof _ | EAlignof _ -> e
+ | EVar x ->
+ begin try IdentMap.find x phi with Not_found -> e end
+ | EUnop(op, e1) ->
+ { e with edesc = EUnop(op, subst_expr phi e1) }
+ | EBinop(op, e1, e2, ty) ->
+ { e with edesc = EBinop(op, subst_expr phi e1, subst_expr phi e2, ty) }
+ | EConditional(e1, e2, e3) ->
+ { e with edesc =
+ EConditional(subst_expr phi e1, subst_expr phi e2, subst_expr phi e3) }
+ | ECast(ty, e1) ->
+ { e with edesc = ECast(ty, subst_expr phi e1) }
+ | ECompound(ty, i) ->
+ { e with edesc = ECompound(ty, subst_init phi i) }
+ | ECall(e1, el) ->
+ { e with edesc = ECall(subst_expr phi e1, List.map (subst_expr phi) el) }
+
+and subst_init phi = function
+ | Init_single e -> Init_single (subst_expr phi e)
+ | Init_array il -> Init_array (List.map (subst_init phi) il)
+ | Init_struct(name, fl) ->
+ Init_struct(name, List.map (fun (f,i) -> (f, subst_init phi i)) fl)
+ | Init_union(name, f, i) ->
+ Init_union(name, f, subst_init phi i)
+
+let subst_decl phi (sto, name, ty, optinit) =
+ (sto, name, ty,
+ match optinit with None -> None | Some i -> Some (subst_init phi i))
+
+let rec subst_stmt phi s =
+ { s with sdesc =
+ match s.sdesc with
+ | Sskip
+ | Sbreak
+ | Scontinue
+ | Sgoto _
+ | Sasm _ -> s.sdesc
+ | Sdo e -> Sdo (subst_expr phi e)
+ | Sseq(s1, s2) -> Sseq (subst_stmt phi s1, subst_stmt phi s2)
+ | Sif(e, s1, s2) ->
+ Sif (subst_expr phi e, subst_stmt phi s1, subst_stmt phi s2)
+ | Swhile(e, s1) -> Swhile (subst_expr phi e, subst_stmt phi s1)
+ | Sdowhile(s1, e) -> Sdowhile (subst_stmt phi s1, subst_expr phi e)
+ | Sfor(s1, e, s2, s3) ->
+ Sfor (subst_stmt phi s1, subst_expr phi e,
+ subst_stmt phi s2, subst_stmt phi s3)
+ | Sswitch(e, s1) -> Sswitch (subst_expr phi e, subst_stmt phi s1)
+ | Slabeled(l, s1) -> Slabeled (l, subst_stmt phi s1)
+ | Sreturn None -> s.sdesc
+ | Sreturn (Some e) -> Sreturn (Some (subst_expr phi e))
+ | Sblock sl -> Sblock (List.map (subst_stmt phi) sl)
+ | Sdecl d -> Sdecl (subst_decl phi d)
+ }
+
+
+
+
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index b90dc897..deee9f08 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -210,6 +210,8 @@ val eassign : exp -> exp -> exp
(* Expression for [e1 = e2] *)
val ecomma : exp -> exp -> exp
(* Expression for [e1, e2] *)
+val ecommalist : exp list -> exp -> exp
+ (* Expression for [e1, ..., eN, e] *)
val sskip: stmt
(* The [skip] statement. No location. *)
val sseq : location -> stmt -> stmt -> stmt
@@ -232,3 +234,10 @@ val formatloc: Format.formatter -> location -> unit
val default_init: Env.t -> typ -> init
(* Return a default initializer for the given type
(with zero numbers, null pointers, etc). *)
+
+(* Substitution of variables by expressions *)
+
+val subst_expr: exp IdentMap.t -> exp -> exp
+val subst_init: exp IdentMap.t -> init -> init
+val subst_decl: exp IdentMap.t -> decl -> decl
+val subst_stmt: exp IdentMap.t -> stmt -> stmt
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index b215505b..bd6489fd 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -44,7 +44,7 @@ type t = {
alignof_fun: int option;
bigendian: bool;
bitfields_msb_first: bool;
- struct_return_as_int: int
+ supports_unaligned_accesses: bool
}
let ilp32ll64 = {
@@ -76,7 +76,7 @@ let ilp32ll64 = {
alignof_fun = None;
bigendian = false;
bitfields_msb_first = false;
- struct_return_as_int = 0
+ supports_unaligned_accesses = false
}
let i32lpll64 = {
@@ -108,7 +108,7 @@ let i32lpll64 = {
alignof_fun = None;
bigendian = false;
bitfields_msb_first = false;
- struct_return_as_int = 0
+ supports_unaligned_accesses = false
}
let il32pll64 = {
@@ -140,7 +140,7 @@ let il32pll64 = {
alignof_fun = None;
bigendian = false;
bitfields_msb_first = false;
- struct_return_as_int = 0
+ supports_unaligned_accesses = false
}
(* Canned configurations for some ABIs *)
@@ -149,9 +149,15 @@ 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 }
+
+let x86_32_macosx =
+ { x86_32 with sizeof_longdouble = 16; alignof_longdouble = 16 }
+
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 +168,10 @@ let ppc_32_bigendian =
{ ilp32ll64 with name = "powerpc";
bigendian = true;
bitfields_msb_first = true;
- struct_return_as_int = 8 }
+ supports_unaligned_accesses = true }
+
let arm_littleendian =
- { ilp32ll64 with name = "arm";
- struct_return_as_int = 4 }
+ { ilp32ll64 with name = "arm" }
(* Add GCC extensions re: sizeof and alignof *)
@@ -173,6 +179,12 @@ 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 }
+
(* Undefined configuration *)
let undef = {
@@ -204,7 +216,7 @@ let undef = {
alignof_fun = None;
bigendian = false;
bitfields_msb_first = false;
- struct_return_as_int = 0
+ supports_unaligned_accesses = false
}
(* The current configuration. Must be initialized before use. *)
diff --git a/cparser/Machine.mli b/cparser/Machine.mli
index b544711f..fb7321f9 100644
--- a/cparser/Machine.mli
+++ b/cparser/Machine.mli
@@ -44,13 +44,20 @@ type t = {
alignof_fun: int option;
bigendian: bool;
bitfields_msb_first: bool;
- struct_return_as_int: int
+ supports_unaligned_accesses: bool
}
+(* The current configuration *)
+
+val config : t ref
+
+(* Canned configurations *)
+
val ilp32ll64 : t
val i32lpll64 : t
val il32pll64 : t
val x86_32 : t
+val x86_32_macosx : t
val x86_64 : t
val win32 : t
val win64 : t
@@ -58,5 +65,4 @@ val ppc_32_bigendian : t
val arm_littleendian : t
val gcc_extensions : t -> t
-
-val config : t ref
+val compcert_interpreter : t -> t
diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml
index 228cc530..8bfc6954 100644
--- a/cparser/StructReturn.ml
+++ b/cparser/StructReturn.ml
@@ -13,37 +13,198 @@
(* *)
(* *********************************************************************)
-(* Eliminate structs and unions being returned by value as function results *)
+(* Eliminate structs and unions that are
+ - returned by value as function results
+ - passed by value as function parameters. *)
open Machine
+open Configuration
open C
open Cutil
open Transform
+let struct_return_style = ref SR_ref
+let struct_passing_style = ref SP_ref_callee
+
(* Classification of function return types. *)
type return_kind =
| Ret_scalar (**r a scalar type, returned as usual *)
| Ret_ref (**r a composite type, returned by reference *)
- | Ret_value of typ (**r a small composite type, returned as an integer *)
+ | Ret_value of typ * int * int
+ (**r a small composite type, returned as an integer
+ (type, size, alignment) *)
let classify_return env ty =
if is_composite_type env ty then begin
- match sizeof env ty with
- | None -> Ret_ref (* should not happen *)
- | Some sz ->
- if (!config).struct_return_as_int >= 4 && sz <= 4 then
- Ret_value (TInt(IUInt, []))
- else if (!config).struct_return_as_int >= 8 && sz <= 8 then
- Ret_value (TInt(IULongLong, []))
- else Ret_ref
+ match sizeof env ty, alignof env ty with
+ | Some sz, Some al ->
+ begin match !struct_return_style with
+ | SR_int1248 when sz = 1 || sz = 2 || sz = 4 ->
+ Ret_value (TInt(IUInt, []), sz, al)
+ | SR_int1248 when sz = 8 ->
+ Ret_value (TInt(IULongLong, []), sz, al)
+ | (SR_int1to4 | SR_int1to8) when sz <= 4 ->
+ Ret_value (TInt(IUInt, []), sz, al)
+ | SR_int1to8 when sz > 4 && sz <= 8 ->
+ Ret_value (TInt(IULongLong, []), sz, al)
+ | _ ->
+ Ret_ref
+ end
+ | _, _ ->
+ Ret_ref (* should not happen *)
end else
Ret_scalar
-(* Rewriting of function types.
+(* Classification of function parameter types. *)
+
+type param_kind =
+ | Param_unchanged (**r passed as is *)
+ | Param_ref_caller (**r passed by reference to a copy taken by the caller *)
+ | Param_flattened of int * int * int (**r passed as N integer arguments *)
+ (**r (N, size, alignment) *)
+
+let classify_param env ty =
+ if is_composite_type env ty then begin
+ match !struct_passing_style with
+ | SP_ref_callee -> Param_unchanged
+ | SP_ref_caller -> Param_ref_caller
+ | _ ->
+ match sizeof env ty, alignof env ty with
+ | Some sz, Some al ->
+ Param_flattened ((sz + 3) / 4, sz, al)
+ | _, _ ->
+ Param_unchanged (* should not happen *)
+ end else
+ Param_unchanged
+
+(* Return the list [f 0; f 1; ...; f (n-1)] *)
+
+let list_map_n f n =
+ let rec map i = if i >= n then [] else f i :: map (i + 1)
+ in map 0
+
+(* Declaring and accessing buffers (arrays of int) *)
+
+let uchar = TInt(IUChar, [])
+let ushort = TInt(IUShort, [])
+let uint = TInt(IUInt, [])
+let ulonglong = TInt(IULongLong, [])
+let ucharptr = TPtr(uchar, [])
+let ushortptr = TPtr(ushort, [])
+let uintptr = TPtr(uint, [])
+let ulonglongptr = TPtr(ulonglong, [])
+
+let ty_buffer n =
+ TArray(uint, Some (Int64.of_int n), [])
+
+let ebuffer_index base idx =
+ { edesc = EBinop(Oindex, base, intconst (Int64.of_int idx) IInt, uintptr);
+ etyp = uint }
+
+let attr_structret = [Attr("__structreturn", [])]
+
+(* Expression constructor functions *)
+
+let ereinterpret ty e =
+ { edesc = EUnop(Oderef, ecast (TPtr(ty, [])) (eaddrof e)); etyp = ty }
+
+let or2 a b = { edesc = EBinop(Oor, a, b, uint); etyp = uint }
+let or3 a b c = or2 (or2 a b) c
+let or4 a b c d = or2 (or2 (or2 a b) c) d
+
+let lshift a nbytes =
+ if nbytes = 0 then a else
+ { edesc = EBinop(Oshl, a, intconst (Int64.of_int (nbytes * 8)) IInt, uint);
+ etyp = uint }
+
+let offsetptr base ofs =
+ if ofs = 0 then base else
+ { edesc = EBinop(Oadd, base, intconst (Int64.of_int ofs) IInt, ucharptr);
+ etyp = ucharptr }
+
+let load1 base ofs shift_le shift_be =
+ let shift = if (!config).bigendian then shift_be else shift_le in
+ let a = offsetptr base ofs in
+ lshift { edesc = EUnop(Oderef, a); etyp = uchar } shift
+
+let load2 base ofs shift_le shift_be =
+ let shift = if (!config).bigendian then shift_be else shift_le in
+ let a = ecast ushortptr (offsetptr base ofs) in
+ lshift { edesc = EUnop(Oderef, a); etyp = ushort } shift
+
+let load4 base ofs =
+ let a = ecast uintptr (offsetptr base ofs) in
+ { edesc = EUnop(Oderef, a); etyp = uint }
+
+let load8 base ofs =
+ let a = ecast ulonglongptr (offsetptr base ofs) in
+ { edesc = EUnop(Oderef, a); etyp = ulonglong }
+
+let lshift_ll a nbytes =
+ let a = ecast ulonglong a in
+ if nbytes = 0 then a else
+ { edesc = EBinop(Oshl, a, intconst (Int64.of_int (nbytes * 8)) IInt, ulonglong);
+ etyp = ulonglong }
+
+let or2_ll a b = { edesc = EBinop(Oor, a, b, uint); etyp = ulonglong }
+
+(* Loading a memory area as one or several integers. *)
+
+let load_word base ofs sz al =
+ match sz with
+ | 0 -> intconst 0L IInt
+ | 1 -> load1 base ofs 0 3
+ | 2 -> if al >= 2 || (!config).supports_unaligned_accesses then
+ load2 base ofs 0 2
+ else
+ or2 (load1 base ofs 0 3)
+ (load1 base (ofs + 1) 1 2)
+ | 3 -> if al >= 2 || (!config).supports_unaligned_accesses then
+ or2 (load2 base ofs 0 2)
+ (load1 base (ofs + 2) 2 1)
+ else
+ or3 (load1 base ofs 0 3)
+ (load1 base (ofs + 1) 1 2)
+ (load1 base (ofs + 2) 2 1)
+ | 4 -> if al >= 4 || (!config).supports_unaligned_accesses then
+ load4 base ofs
+ else if al >= 2 then
+ or2 (load2 base ofs 0 2)
+ (load2 base (ofs + 2) 2 0)
+ else
+ or4 (load1 base ofs 0 3)
+ (load1 base (ofs + 1) 1 2)
+ (load1 base (ofs + 2) 2 1)
+ (load1 base (ofs + 3) 3 0)
+ | _ -> assert false
+
+
+let rec load_words base ofs sz al =
+ if ofs >= sz then []
+ else if ofs + 4 >= sz then [load_word base ofs (sz - ofs) al]
+ else load_word base ofs 4 al :: load_words base (ofs + 4) sz al
+
+let load_result base sz al =
+ assert (sz <= 8);
+ if sz <= 4 then
+ load_word base 0 sz al
+ else if sz = 8 && (al >= 8 || (!config).supports_unaligned_accesses) then
+ load8 base 0
+ else begin
+ let (shift1, shift2) = if (!config).bigendian then (4, 0) else (0, 4) in
+ or2_ll (lshift_ll (load_word base 0 4 al) shift1)
+ (lshift_ll (load_word base 4 (sz - 4) al) shift2)
+ end
+
+(* Rewriting of function types. For the return type:
return kind scalar -> no change
return kind ref -> return type void + add 1st parameter struct s *
return kind value(t) -> return type t.
+ For the parameters:
+ param unchanged -> no change
+ param_ref_caller -> turn into a pointer
+ param_flattened N -> turn into N parameters of type "int"
Try to preserve original typedef names when no change.
*)
@@ -51,22 +212,25 @@ let rec transf_type env t =
match unroll env t with
| TFun(tres, None, vararg, attr) ->
let tres' = transf_type env tres in
- let tres'' =
- match classify_return env tres with
- | Ret_scalar -> tres'
- | Ret_ref -> TVoid []
- | Ret_value ty -> ty in
- TFun(tres'', None, vararg, attr)
+ begin match classify_return env tres with
+ | Ret_scalar ->
+ TFun(tres', None, vararg, attr)
+ | Ret_ref ->
+ TFun(TVoid [], None, vararg, add_attributes attr attr_structret)
+ | Ret_value(ty, sz, al) ->
+ TFun(ty, None, vararg, attr)
+ end
| TFun(tres, Some args, vararg, attr) ->
- let args' = List.map (transf_funarg env) args in
+ let args' = transf_funargs env args in
let tres' = transf_type env tres in
begin match classify_return env tres with
| Ret_scalar ->
TFun(tres', Some args', vararg, attr)
| Ret_ref ->
let res = Env.fresh_ident "_res" in
- TFun(TVoid [], Some((res, TPtr(tres', [])) :: args'), vararg, attr)
- | Ret_value ty ->
+ TFun(TVoid [], Some((res, TPtr(tres', [])) :: args'), vararg,
+ add_attributes attr attr_structret)
+ | Ret_value(ty, sz, al) ->
TFun(ty, Some args', vararg, attr)
end
| TPtr(t1, attr) ->
@@ -77,12 +241,28 @@ let rec transf_type env t =
if t1' = t1 then t else TArray(transf_type env t1, sz, attr)
| _ -> t
-and transf_funarg env (id, t) = (id, transf_type env t)
+and transf_funargs env = function
+ | [] -> []
+ | (id, t) :: args ->
+ let t' = transf_type env t in
+ let args' = transf_funargs env args in
+ match classify_param env t with
+ | Param_unchanged ->
+ (id, t') :: args'
+ | Param_ref_caller ->
+ (id, TPtr(t', [])) :: args'
+ | Param_flattened(n, sz, al) ->
+ list_map_n (fun _ -> (Env.fresh_ident id.name, uint)) n
+ @ args'
(* Expressions: transform calls + rewrite the types *)
-let ereinterpret ty e =
- { edesc = EUnop(Oderef, ecast (TPtr(ty, [])) (eaddrof e)); etyp = ty }
+let rec translates_to_extended_lvalue arg =
+ is_lvalue arg ||
+ (match arg.edesc with
+ | ECall _ -> true
+ | EBinop(Ocomma, a, b, _) -> translates_to_extended_lvalue b
+ | _ -> false)
let rec transf_expr env ctx e =
let newty = transf_type env e.etyp in
@@ -98,7 +278,7 @@ let rec transf_expr env ctx e =
| EUnop(op, e1) ->
{edesc = EUnop(op, transf_expr env Val e1); etyp = newty}
| EBinop(Oassign, lhs, {edesc = ECall(fn, args); etyp = ty}, _) ->
- transf_call env ctx (Some lhs) fn args ty
+ transf_call env ctx (Some (transf_expr env Val lhs)) fn args ty
| EBinop(Ocomma, e1, e2, ty) ->
ecomma (transf_expr env Effects e1) (transf_expr env ctx e2)
| EBinop(op, e1, e2, ty) ->
@@ -133,48 +313,92 @@ let rec transf_expr env ctx e =
and transf_call env ctx opt_lhs fn args ty =
let ty' = transf_type env ty in
let fn' = transf_expr env Val fn in
- let args' = List.map (transf_expr env Val) args in
+ let (assignments, args') = transf_arguments env args in
let opt_eassign e =
match opt_lhs with
| None -> e
- | Some lhs -> eassign (transf_expr env Val lhs) e in
+ | Some lhs -> eassign lhs e in
match fn with
| {edesc = EVar {name = "__builtin_va_arg"}} ->
(* Do not transform the call in this case *)
opt_eassign {edesc = ECall(fn, args'); etyp = ty}
| _ ->
- match classify_return env ty with
- | Ret_scalar ->
- opt_eassign {edesc = ECall(fn', args'); etyp = ty'}
- | Ret_ref ->
- begin match ctx, opt_lhs with
- | Effects, None ->
- let tmp = new_temp ~name:"_res" ty in
- {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []}
- | Effects, Some lhs ->
- let lhs' = transf_expr env Val lhs in
- {edesc = ECall(fn', eaddrof lhs' :: args'); etyp = TVoid []}
- | Val, None ->
- let tmp = new_temp ~name:"_res" ty in
- ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []}
- tmp
- | Val, Some lhs ->
- let lhs' = transf_expr env Val lhs in
- let tmp = new_temp ~name:"_res" ty in
- ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []}
- (eassign lhs' tmp)
- end
- | Ret_value ty_ret ->
- let ecall = {edesc = ECall(fn', args'); etyp = ty_ret} in
- begin match ctx, opt_lhs with
- | Effects, None ->
- ecall
- | _, _ ->
- let tmp = new_temp ~name:"_res" ty_ret in
- opt_eassign
- (ecomma (eassign tmp ecall)
- (ereinterpret ty' tmp))
- end
+ let call =
+ match classify_return env ty with
+ | Ret_scalar ->
+ opt_eassign {edesc = ECall(fn', args'); etyp = ty'}
+ | Ret_ref ->
+ begin match ctx, opt_lhs with
+ | Effects, None ->
+ let tmp = new_temp ~name:"_res" ty in
+ {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []}
+ | Effects, Some lhs ->
+ {edesc = ECall(fn', eaddrof lhs :: args'); etyp = TVoid []}
+ | Val, None ->
+ let tmp = new_temp ~name:"_res" ty in
+ ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []}
+ tmp
+ | Val, Some lhs ->
+ let tmp = new_temp ~name:"_res" ty in
+ ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []}
+ (eassign lhs tmp)
+ end
+ | Ret_value(ty_ret, sz, al) ->
+ let ecall = {edesc = ECall(fn', args'); etyp = ty_ret} in
+ begin match ctx, opt_lhs with
+ | Effects, None ->
+ ecall
+ | _, _ ->
+ let tmp = new_temp ~name:"_res" ty_ret in
+ opt_eassign
+ (ecomma (eassign tmp ecall)
+ (ereinterpret ty' tmp))
+ end
+ in ecommalist assignments call
+
+(* Function argument of ref_caller kind: take a copy and pass pointer to copy
+ arg ---> newtemp = arg ... &newtemp
+ Function argument of flattened(N) kind: load and pass as integers
+ either using an intermediate array
+ arg ---> ( * ((ty * ) temparray) = arg ...
+ temparray[0], ...,, temparray[N-1]
+ or by using loadwords:
+ arg ---> addr = &(arg) ... loadwords addr ...
+*)
+
+and transf_arguments env args =
+ match args with
+ | [] -> ([], [])
+ | arg :: args ->
+ let (assignments, args') = transf_arguments env args in
+ match classify_param env arg.etyp with
+ | Param_unchanged ->
+ let arg' = transf_expr env Val arg in
+ (assignments, arg' :: args')
+ | Param_ref_caller ->
+ let ty' = transf_type env arg.etyp in
+ let tmp = new_temp ~name:"_arg" ty' in
+ (transf_assign env tmp arg :: assignments,
+ eaddrof tmp :: args')
+ | Param_flattened(n, sz, al) ->
+ let ty' = transf_type env arg.etyp in
+ if translates_to_extended_lvalue arg then begin
+ let tmp = new_temp ~name:"_arg" ucharptr in
+ (eassign tmp (ecast ucharptr (eaddrof (transf_expr env Val arg)))
+ :: assignments,
+ load_words tmp 0 sz al @ args')
+ end else begin
+ let tmp = new_temp ~name:"_arg" (ty_buffer n) in
+ (transf_assign env (ereinterpret ty' tmp) arg :: assignments,
+ list_map_n (ebuffer_index tmp) n @ args')
+ end
+
+and transf_assign env lhs e =
+ match e.edesc with
+ | ECall(fn, args) ->
+ transf_call env Effects (Some lhs) fn args e.etyp
+ | _ ->
+ eassign lhs (transf_expr env Val e)
(* Initializers *)
@@ -204,6 +428,7 @@ let transf_expr ctx e = transf_expr env ctx e in
return kind scalar -> return e
return kind ref -> _res = x; return
return kind value ty -> *((struct s * )_res) = x; return _res
+ or addr = &x; return loadresult(addr)
*)
let rec transf_stmt s =
@@ -240,10 +465,18 @@ let rec transf_stmt s =
sseq s.sloc
(sassign s.sloc dst e')
{sdesc = Sreturn None; sloc = s.sloc}
- | Ret_value ty, Some dst ->
- sseq s.sloc
- (sassign s.sloc (ereinterpret e'.etyp dst) e')
- {sdesc = Sreturn (Some dst); sloc = s.sloc}
+ | Ret_value(ty, sz, al), None ->
+ if translates_to_extended_lvalue e then begin
+ let tmp = new_temp ~name:"_res" ucharptr in
+ sseq s.sloc
+ (sassign s.sloc tmp (ecast ucharptr (eaddrof e')))
+ {sdesc = Sreturn (Some (load_result tmp sz al)); sloc = s.sloc}
+ end else begin
+ let dst = new_temp ~name:"_res" ty in
+ sseq s.sloc
+ (sassign s.sloc (ereinterpret e'.etyp dst) e')
+ {sdesc = Sreturn (Some dst); sloc = s.sloc}
+ end
| _, _ ->
assert false
end
@@ -256,29 +489,77 @@ let rec transf_stmt s =
in
transf_stmt body
+(* Binding arguments to parameters. Returns a triple:
+ - parameter list
+ - actions to perform at the beginning of the function
+ - substitution to apply to the function body
+*)
+
+let rec transf_funparams loc env params =
+ match params with
+ | [] ->
+ ([], sskip, IdentMap.empty)
+ | (x, tx) :: params ->
+ let tx' = transf_type env tx in
+ let (params', actions, subst) = transf_funparams loc env params in
+ match classify_param env tx with
+ | Param_unchanged ->
+ ((x, tx') :: params',
+ actions,
+ subst)
+ | Param_ref_caller ->
+ let tpx = TPtr(tx', []) in
+ let ex = { edesc = EVar x; etyp = tpx } in
+ let estarx = { edesc = EUnop(Oderef, ex); etyp = tx' } in
+ ((x, tpx) :: params',
+ actions,
+ IdentMap.add x estarx subst)
+ | Param_flattened(n, sz, al) ->
+ let y = new_temp ~name:x.name (ty_buffer n) in
+ let yparts = list_map_n (fun _ -> Env.fresh_ident x.name) n in
+ let assign_part e p act =
+ sseq loc (sassign loc e {edesc = EVar p; etyp = uint}) act in
+ (List.map (fun p -> (p, uint)) yparts @ params',
+ List.fold_right2 assign_part
+ (list_map_n (ebuffer_index y) n)
+ yparts
+ actions,
+ IdentMap.add x (ereinterpret tx' y) subst)
+
let transf_fundef env f =
reset_temps();
let ret = transf_type env f.fd_ret in
- let params =
- List.map (fun (id, ty) -> (id, transf_type env ty)) f.fd_params in
- let (ret1, params1, body1) =
+ let (params, actions, subst) =
+ transf_funparams f.fd_body.sloc env f.fd_params in
+ let locals =
+ List.map (fun d -> transf_decl env (subst_decl subst d)) f.fd_locals in
+ let (attr1, ret1, params1, body1) =
match classify_return env f.fd_ret with
| Ret_scalar ->
- (ret, params, transf_funbody env f.fd_body None)
+ (f.fd_attrib,
+ ret,
+ params,
+ transf_funbody env (subst_stmt subst f.fd_body) None)
| Ret_ref ->
let vres = Env.fresh_ident "_res" in
let tres = TPtr(ret, []) in
let eres = {edesc = EVar vres; etyp = tres} in
let eeres = {edesc = EUnop(Oderef, eres); etyp = ret} in
- (TVoid [],
+ (add_attributes f.fd_attrib attr_structret,
+ TVoid [],
(vres, tres) :: params,
- transf_funbody env f.fd_body (Some eeres))
- | Ret_value ty ->
- let eres = new_temp ~name:"_res" ty in
- (ty, params, transf_funbody env f.fd_body (Some eres)) in
+ transf_funbody env (subst_stmt subst f.fd_body) (Some eeres))
+ | Ret_value(ty, sz, al) ->
+ (f.fd_attrib,
+ ty,
+ params,
+ transf_funbody env (subst_stmt subst f.fd_body) None) in
let temps = get_temps() in
- {f with fd_ret = ret1; fd_params = params1;
- fd_locals = f.fd_locals @ temps; fd_body = body1}
+ {f with fd_attrib = attr1;
+ fd_ret = ret1;
+ fd_params = params1;
+ fd_locals = locals @ temps;
+ fd_body = sseq f.fd_body.sloc actions body1}
(* Composites *)
@@ -288,6 +569,14 @@ let transf_composite env su id attr fl =
(* Entry point *)
let program p =
+ struct_passing_style :=
+ if !Clflags.option_interp
+ then SP_ref_callee
+ else !Clflags.option_fstruct_passing_style;
+ struct_return_style :=
+ if !Clflags.option_interp
+ then SR_ref
+ else !Clflags.option_fstruct_return_style;
Transform.program
~decl:transf_decl
~fundef:transf_fundef
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index 405986f3..4013db9b 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -149,7 +149,7 @@ let rec expand_expr islocal env e =
| ECall(e1, el) ->
{edesc = ECall(expand e1, List.map expand el); etyp = e.etyp}
in
- let e' = expand e in add_inits_expr !inits e'
+ let e' = expand e in ecommalist !inits e'
(* Elimination of compound literals within an initializer. *)
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 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 d22dd77c..ad7cf61e 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -265,6 +265,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;
@@ -409,6 +410,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]
@@ -550,7 +555,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 *)
@@ -607,7 +633,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;
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 888a7e72..c00dfc57 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -801,8 +801,10 @@ module Target(System: SYSTEM):TARGET =
| Pjmp_l(l) ->
fprintf oc " jmp %a\n" label (transl_label l)
| Pjmp_s(f, sg) ->
+ assert (not sg.sig_cc.cc_structret);
fprintf oc " jmp %a\n" symbol f
| Pjmp_r(r, sg) ->
+ assert (not sg.sig_cc.cc_structret);
fprintf oc " jmp *%a\n" ireg r
| Pjcc(c, l) ->
let l = transl_label l in
@@ -818,12 +820,21 @@ module Target(System: SYSTEM):TARGET =
fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r;
jumptables := (l, tbl) :: !jumptables
| Pcall_s(f, sg) ->
- fprintf oc " call %a\n" symbol f
+ fprintf oc " call %a\n" symbol f;
+ if sg.sig_cc.cc_structret then
+ fprintf oc " pushl %%eax\n"
| Pcall_r(r, sg) ->
- fprintf oc " call *%a\n" ireg r
+ fprintf oc " call *%a\n" ireg r;
+ if sg.sig_cc.cc_structret then
+ fprintf oc " pushl %%eax\n"
| Pret ->
- fprintf oc " ret\n"
- (** Pseudo-instructions *)
+ if (!current_function_sig).sig_cc.cc_structret then begin
+ fprintf oc " movl 0(%%esp), %%eax\n";
+ fprintf oc " ret $4\n"
+ end else begin
+ fprintf oc " ret\n"
+ end
+ (** Pseudo-instructions *)
| Plabel(l) ->
fprintf oc "%a:\n" label (transl_label l)
| Pallocframe(sz, ofs_ra, ofs_link) ->
diff --git a/runtime/arm/vararg.S b/runtime/arm/vararg.S
index ae06e361..5e319b8b 100644
--- a/runtime/arm/vararg.S
+++ b/runtime/arm/vararg.S
@@ -75,3 +75,15 @@ FUNCTION(__compcert_va_float64)
#endif
bx lr
ENDFUNCTION(__compcert_va_float64)
+
+FUNCTION(__compcert_va_composite)
+ @ r0 = ap parameter
+ @ r1 = size of the composite, in bytes
+ ldr r2, [r0, #0] @ r2 = pointer to next argument
+ ADD r3, r2, r1 @ advance by size
+ ADD r3, r3, #3 @ 4-align
+ BIC r3, r3, #3
+ str r3, [r0, #0] @ update ap
+ mov r0, r2 @ result is pointer to composite in stack
+ bx lr
+ENDFUNCTION(__compcert_va_composite)
diff --git a/runtime/ia32/vararg.S b/runtime/ia32/vararg.S
index ec55a454..78666c70 100644
--- a/runtime/ia32/vararg.S
+++ b/runtime/ia32/vararg.S
@@ -67,3 +67,15 @@ FUNCTION(__compcert_va_float64)
movl %edx, 0(%ecx)
ret
ENDFUNCTION(__compcert_va_float64)
+
+FUNCTION(__compcert_va_composite)
+ movl 4(%esp), %ecx // %ecx = ap parameter
+ movl 8(%esp), %edx // %edx = size of composite in bytes
+ movl 0(%ecx), %eax // %eax = current argument pointer
+ leal 3(%eax, %edx), %edx // advance by size
+ andl $0xfffffffc, %edx // and round up to multiple of 4
+ movl %edx, 0(%ecx) // update argument pointer
+ ret
+ENDFUNCTION(__compcert_va_composite)
+
+
diff --git a/runtime/powerpc/vararg.s b/runtime/powerpc/vararg.s
index 16681c1c..8d7e62c8 100644
--- a/runtime/powerpc/vararg.s
+++ b/runtime/powerpc/vararg.s
@@ -128,6 +128,13 @@ __compcert_va_float64:
.type __compcert_va_float64, @function
.size __compcert_va_float64, .-__compcert_va_int64
+ .balign 16
+ .globl __compcert_va_composite
+__compcert_va_composite:
+ b __compcert_va_int32
+ .type __compcert_va_composite, @function
+ .size __compcert_va_composite, .-__compcert_va_composite
+
# Save integer and FP registers at beginning of vararg function
.balign 16
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 5c601211..206670b5 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -17,7 +17,7 @@ TESTS=int32 int64 floats floats-basics \
volatile1 volatile2 volatile3 \
funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \
sizeof1 sizeof2 binops bool for1 switch switch2 compound \
- decl1
+ decl1 interop1
# Can run, but only in compiled mode, and have reference output in Results
@@ -45,6 +45,13 @@ all: $(TESTS:%=%.compcert) $(TESTS_COMP:%=%.compcert) $(TESTS_DIFF:%=%.compcert)
all_s: $(TESTS:%=%.s) $(TESTS_COMP:%=%.s) $(TESTS_DIFF:%=%.s) $(EXTRAS:%=%.s)
+interop1.compcert: interop1.c $(CCOMP)
+ $(CC) -DCC_SIDE -c -o interop1n.o interop1.c
+ $(CCOMP) $(CCOMPFLAGS) -DCOMPCERT_SIDE -o interop1.compcert interop1.c interop1n.o $(LIBS)
+
+interop1.s: interop1.c $(CCOMP)
+ $(CCOMP) $(CCOMPFLAGS) -S interop1.c
+
%.compcert: %.c $(CCOMP)
$(CCOMP) $(CCOMPFLAGS) -o $*.compcert $*.c $(LIBS)
diff --git a/test/regression/Results/interop1 b/test/regression/Results/interop1
new file mode 100644
index 00000000..990dfe9d
--- /dev/null
+++ b/test/regression/Results/interop1
@@ -0,0 +1,90 @@
+--- CompCert calling native:
+s1: { a = 'a' }
+s2: { a = 'a', b = 'b' }
+s3: { a = 'a', b = 'b', c = ' c' }
+s4: { a = 'a', b = 'b', c = ' c', d = 'd' }
+s5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' }
+s6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' }
+s7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' }
+s8: "Hello world!"
+t1: { a = 123 }
+t2: { a = 123, b = 456 }
+t3: { a = 123, b = 456, c = 789 }
+t4: { a = 123, b = 456, c = 789, d = -111 }
+t5: { a = 123, b = 456, c = 789, d = -999, e = 'x' }
+u1: { a = 12 }
+u2: { a = 12, b = -34 }
+u3: { a = 12, b = 34, c = -56 }
+u4: { a = 12, b = 34, c = 56, d = -78 }
+u5: { a = 1234, b = 'u' }
+u6: { a = 55555, b = 666 }
+u7: { a = -10001, b = -789, c = 'z' }
+u8: { a = 'x', b = 12345 }
+after ms4, x = { 's', 'a', 'm', 'e' }
+after mu4, x = { a = { 11, 22, 33, 44 } }
+rs1: { a = 'a' }
+rs2: { a = 'a', b = 'b' }
+rs3: { a = 'a', b = 'b', c = ' c' }
+rs4: { a = 'a', b = 'b', c = ' c', d = 'd' }
+rs5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' }
+rs6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' }
+rs7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' }
+rs8: "Hello world!"
+rt1: { a = 123 }
+rt2: { a = 123, b = 456 }
+rt3: { a = 123, b = 456, c = 789 }
+rt4: { a = 123, b = 456, c = 789, d = -111 }
+rt5: { a = 123, b = 456, c = 789, d = -999, e = 'x' }
+ru1: { a = 12 }
+ru2: { a = 12, b = -34 }
+ru3: { a = 12, b = 34, c = -56 }
+ru4: { a = 12, b = 34, c = 56, d = -78 }
+ru5: { a = 1234, b = 'u' }
+ru6: { a = 55555, b = 666 }
+ru7: { a = -10001, b = -789, c = 'z' }
+ru8: { a = 'x', b = 12345 }
+--- native calling CompCert:
+s1: { a = 'a' }
+s2: { a = 'a', b = 'b' }
+s3: { a = 'a', b = 'b', c = ' c' }
+s4: { a = 'a', b = 'b', c = ' c', d = 'd' }
+s5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' }
+s6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' }
+s7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' }
+s8: "Hello world!"
+t1: { a = 123 }
+t2: { a = 123, b = 456 }
+t3: { a = 123, b = 456, c = 789 }
+t4: { a = 123, b = 456, c = 789, d = -111 }
+t5: { a = 123, b = 456, c = 789, d = -999, e = 'x' }
+u1: { a = 12 }
+u2: { a = 12, b = -34 }
+u3: { a = 12, b = 34, c = -56 }
+u4: { a = 12, b = 34, c = 56, d = -78 }
+u5: { a = 1234, b = 'u' }
+u6: { a = 55555, b = 666 }
+u7: { a = -10001, b = -789, c = 'z' }
+u8: { a = 'x', b = 12345 }
+after ms4, x = { 's', 'a', 'm', 'e' }
+after mu4, x = { a = { 11, 22, 33, 44 } }
+rs1: { a = 'a' }
+rs2: { a = 'a', b = 'b' }
+rs3: { a = 'a', b = 'b', c = ' c' }
+rs4: { a = 'a', b = 'b', c = ' c', d = 'd' }
+rs5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' }
+rs6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' }
+rs7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' }
+rs8: "Hello world!"
+rt1: { a = 123 }
+rt2: { a = 123, b = 456 }
+rt3: { a = 123, b = 456, c = 789 }
+rt4: { a = 123, b = 456, c = 789, d = -111 }
+rt5: { a = 123, b = 456, c = 789, d = -999, e = 'x' }
+ru1: { a = 12 }
+ru2: { a = 12, b = -34 }
+ru3: { a = 12, b = 34, c = -56 }
+ru4: { a = 12, b = 34, c = 56, d = -78 }
+ru5: { a = 1234, b = 'u' }
+ru6: { a = 55555, b = 666 }
+ru7: { a = -10001, b = -789, c = 'z' }
+ru8: { a = 'x', b = 12345 }
diff --git a/test/regression/Results/varargs2 b/test/regression/Results/varargs2
index f954927e..96ee9d63 100644
--- a/test/regression/Results/varargs2
+++ b/test/regression/Results/varargs2
@@ -2,7 +2,9 @@ An int: 42
A long long: 123456789012345
A string: Hello world
A double: 3.141592654
-A mixture: x & Hello, world! & 42 & 123456789012345 & 3.141592654 & 2.718281746
+A small struct: x12
+A bigger struct: (123,456,789)
+A mixture: x & Hello, world! & y2 & 42 & 123456789012345 & 3.141592654 & 2.718281746
Twice: -1 1.23
Twice: -1 1.23
With va_copy: -1 1.23
diff --git a/test/regression/interop1.c b/test/regression/interop1.c
new file mode 100644
index 00000000..a39f449c
--- /dev/null
+++ b/test/regression/interop1.c
@@ -0,0 +1,286 @@
+#if defined(COMPCERT_SIDE)
+#define US(x) compcert_##x
+#define THEM(x) native_##x
+#elif defined(CC_SIDE)
+#define US(x) native_##x
+#define THEM(x) compcert_##x
+#else
+#define US(x) x
+#define THEM(x) x
+#endif
+
+#include <stdio.h>
+
+/* Alignment 1 */
+
+struct S1 { char a; };
+static struct S1 init_S1 = { 'a' };
+#define print_S1(x) printf("{ a = '%c' }\n", x.a)
+
+struct S2 { char a, b; };
+static struct S2 init_S2 = { 'a', 'b' };
+#define print_S2(x) printf("{ a = '%c', b = '%c' }\n", x.a, x.b)
+
+struct S3 { char a, b, c; };
+static struct S3 init_S3 = { 'a', 'b', 'c' };
+#define print_S3(x) \
+ printf("{ a = '%c', b = '%c', c = ' %c' }\n", x.a, x.b, x.c)
+
+struct S4 { char a, b, c, d; };
+static struct S4 init_S4 = { 'a', 'b', 'c', 'd' };
+#define print_S4(x) \
+ printf("{ a = '%c', b = '%c', c = ' %c', d = '%c' }\n", \
+ x.a, x.b, x.c, x.d);
+
+struct S5 { char a, b, c, d, e; };
+static struct S5 init_S5 = { 'a', 'b', 'c', 'd', 'e' };
+#define print_S5(x) \
+ printf("{ a = '%c', b = '%c', c = ' %c', d = '%c', e = '%c' }\n", \
+ x.a, x.b, x.c, x.d, x.e)
+
+struct S6 { char a, b, c, d, e, f; };
+static struct S6 init_S6 = { 'a', 'b', 'c', 'd', 'e', 'f' };
+#define print_S6(x) \
+ printf("{ a = '%c', b = '%c', c = ' %c', d = '%c', e = '%c', f = '%c' }\n", \
+ x.a, x.b, x.c, x.d, x.e, x.f)
+
+struct S7 { char a, b, c, d, e, f, g; };
+static struct S7 init_S7 = { 'a', 'b', 'c', 'd', 'e', 'f', 'g' };
+#define print_S7(x) \
+ printf("{ a = '%c', b = '%c', c = ' %c', d = '%c', e = '%c', f = '%c', g = '%c' }\n", \
+ x.a, x.b, x.c, x.d, x.e, x.f, x.g)
+
+struct S8 { char a[32]; };
+static struct S8 init_S8 = { "Hello world!" };
+/* Do not use printf("%s") to avoid undefined behavior in the
+ reference interpreter */
+#define print_S8(x) \
+ { char * p; \
+ printf("\""); \
+ for (p = x.a; *p != 0; p++) printf("%c", *p); \
+ printf("\"\n"); \
+ }
+
+/* Alignment 2 */
+
+struct T1 { short a; };
+static struct T1 init_T1 = { 123 };
+#define print_T1(x) printf("{ a = %d }\n", x.a)
+
+struct T2 { short a, b; };
+static struct T2 init_T2 = { 123, 456 };
+#define print_T2(x) printf("{ a = %d, b = %d }\n", x.a, x.b)
+
+struct T3 { short a, b, c; };
+static struct T3 init_T3 = { 123, 456, 789 };
+#define print_T3(x) printf("{ a = %d, b = %d, c = %d }\n", x.a, x.b, x.c)
+
+struct T4 { short a, b, c, d; };
+static struct T4 init_T4 = { 123, 456, 789, -111 };
+#define print_T4(x) \
+ printf("{ a = %d, b = %d, c = %d, d = %d }\n", x.a, x.b, x.c, x.d)
+
+struct T5 { short a, b, c, d; char e; };
+static struct T5 init_T5 = { 123, 456, 789, -999, 'x' };
+#define print_T5(x) \
+ printf("{ a = %d, b = %d, c = %d, d = %d, e = '%c' }\n", \
+ x.a, x.b, x.c, x.d, x.e)
+
+/* Alignment >= 4 */
+
+struct U1 { int a; };
+static struct U1 init_U1 = { 12 };
+#define print_U1(x) printf("{ a = %d }\n", x.a)
+
+struct U2 { int a, b; };
+static struct U2 init_U2 = { 12, -34 };
+#define print_U2(x) printf("{ a = %d, b = %d }\n", x.a, x.b)
+
+struct U3 { int a, b, c; };
+static struct U3 init_U3 = { 12, 34, -56};
+#define print_U3(x) printf("{ a = %d, b = %d, c = %d }\n", x.a, x.b, x.c)
+
+struct U4 { int a, b, c, d; };
+static struct U4 init_U4 = { 12, 34, 56, -78 };
+#define print_U4(x) \
+ printf("{ a = %d, b = %d, c = %d, d = %d }\n", x.a, x.b, x.c, x.d)
+
+struct U5 { int a; char b; };
+static struct U5 init_U5 = { 1234, 'u' };
+#define print_U5(x) \
+ printf("{ a = %d, b = '%c' }\n", x.a, x.b)
+
+struct U6 { int a; short b; };
+static struct U6 init_U6 = { 55555, 666 };
+#define print_U6(x) \
+ printf("{ a = %d, b = %d }\n", x.a, x.b)
+
+struct U7 { int a; short b; char c; };
+static struct U7 init_U7 = { -10001, -789, 'z' };
+#define print_U7(x) \
+ printf("{ a = %d, b = %d, c = '%c' }\n", x.a, x.b, x.c)
+
+struct U8 { char a; int b; };
+static struct U8 init_U8 = { 'x', 12345 };
+#define print_U8(x) \
+ printf("{ a = '%c', b = %d }\n", x.a, x.b)
+
+/* Struct passing */
+
+#define PRINT(name,ty,print) \
+extern void THEM(name) (struct ty x); \
+void US(name) (struct ty x) { print(x); }
+
+PRINT(s1,S1,print_S1)
+PRINT(s2,S2,print_S2)
+PRINT(s3,S3,print_S3)
+PRINT(s4,S4,print_S4)
+PRINT(s5,S5,print_S5)
+PRINT(s6,S6,print_S6)
+PRINT(s7,S7,print_S7)
+PRINT(s8,S8,print_S8)
+PRINT(t1,T1,print_T1)
+PRINT(t2,T2,print_T2)
+PRINT(t3,T3,print_T3)
+PRINT(t4,T4,print_T4)
+PRINT(t5,T5,print_T5)
+PRINT(u1,U1,print_U1)
+PRINT(u2,U2,print_U2)
+PRINT(u3,U3,print_U3)
+PRINT(u4,U4,print_U4)
+PRINT(u5,U5,print_U5)
+PRINT(u6,U6,print_U6)
+PRINT(u7,U7,print_U7)
+PRINT(u8,U8,print_U8)
+
+/* Struct passing with modification in the callee */
+
+extern void THEM (ms4) (struct S4 x);
+void US (ms4) (struct S4 x)
+{
+ x.a += 1; x.d -= 1;
+}
+
+extern void THEM (mu4) (struct U4 x);
+void US (mu4) (struct U4 x)
+{
+ x.a = 1; x.b = 2;
+}
+
+/* Struct return */
+
+#define RETURN(name,ty,init) \
+extern struct ty THEM(name)(void); \
+struct ty US(name)(void) { return init; }
+
+RETURN(rs1,S1,init_S1)
+RETURN(rs2,S2,init_S2)
+RETURN(rs3,S3,init_S3)
+RETURN(rs4,S4,init_S4)
+RETURN(rs5,S5,init_S5)
+RETURN(rs6,S6,init_S6)
+RETURN(rs7,S7,init_S7)
+RETURN(rs8,S8,init_S8)
+RETURN(rt1,T1,init_T1)
+RETURN(rt2,T2,init_T2)
+RETURN(rt3,T3,init_T3)
+RETURN(rt4,T4,init_T4)
+RETURN(rt5,T5,init_T5)
+RETURN(ru1,U1,init_U1)
+RETURN(ru2,U2,init_U2)
+RETURN(ru3,U3,init_U3)
+RETURN(ru4,U4,init_U4)
+RETURN(ru5,U5,init_U5)
+RETURN(ru6,U6,init_U6)
+RETURN(ru7,U7,init_U7)
+RETURN(ru8,U8,init_U8)
+
+/* Test function, calling the functions compiled by the other compiler */
+
+#define CALLPRINT(name,ty,init) \
+ printf(#name": "); THEM(name)(init);
+
+#define CALLRETURN(name,ty,print) \
+ { struct ty x = THEM(name)(); \
+ printf(#name": "); print(x); }
+
+extern void THEM(test) (void);
+void US(test) (void)
+{
+ CALLPRINT(s1,S1,init_S1)
+ CALLPRINT(s2,S2,init_S2)
+ CALLPRINT(s3,S3,init_S3)
+ CALLPRINT(s4,S4,init_S4)
+ CALLPRINT(s5,S5,init_S5)
+ CALLPRINT(s6,S6,init_S6)
+ CALLPRINT(s7,S7,init_S7)
+ CALLPRINT(s8,S8,init_S8)
+ CALLPRINT(t1,T1,init_T1)
+ CALLPRINT(t2,T2,init_T2)
+ CALLPRINT(t3,T3,init_T3)
+ CALLPRINT(t4,T4,init_T4)
+ CALLPRINT(t5,T5,init_T5)
+ CALLPRINT(u1,U1,init_U1)
+ CALLPRINT(u2,U2,init_U2)
+ CALLPRINT(u3,U3,init_U3)
+ CALLPRINT(u4,U4,init_U4)
+ CALLPRINT(u5,U5,init_U5)
+ CALLPRINT(u6,U6,init_U6)
+ CALLPRINT(u7,U7,init_U7)
+ CALLPRINT(u8,U8,init_U8)
+
+ { struct S4 x = { 's', 'a', 'm', 'e' };
+ THEM(ms4)(x);
+ printf("after ms4, x = { '%c', '%c', '%c', '%c' }\n", x.a, x.b, x.c, x.d); }
+ { struct U4 x = { 11, 22, 33, 44 };
+ THEM(mu4)(x);
+ printf("after mu4, x = { a = { %d, %d, %d, %d } }\n", x.a, x.b, x.c, x.d); }
+
+ CALLRETURN(rs1,S1,print_S1)
+ CALLRETURN(rs2,S2,print_S2)
+ CALLRETURN(rs3,S3,print_S3)
+ CALLRETURN(rs4,S4,print_S4)
+ CALLRETURN(rs5,S5,print_S5)
+ CALLRETURN(rs6,S6,print_S6)
+ CALLRETURN(rs7,S7,print_S7)
+ CALLRETURN(rs8,S8,print_S8)
+ CALLRETURN(rt1,T1,print_T1)
+ CALLRETURN(rt2,T2,print_T2)
+ CALLRETURN(rt3,T3,print_T3)
+ CALLRETURN(rt4,T4,print_T4)
+ CALLRETURN(rt5,T5,print_T5)
+ CALLRETURN(ru1,U1,print_U1)
+ CALLRETURN(ru2,U2,print_U2)
+ CALLRETURN(ru3,U3,print_U3)
+ CALLRETURN(ru4,U4,print_U4)
+ CALLRETURN(ru5,U5,print_U5)
+ CALLRETURN(ru6,U6,print_U6)
+ CALLRETURN(ru7,U7,print_U7)
+ CALLRETURN(ru8,U8,print_U8)
+}
+
+#if defined(COMPCERT_SIDE)
+
+int main()
+{
+ printf("--- CompCert calling native:\n");
+ compcert_test();
+ printf("--- native calling CompCert:\n");
+ native_test();
+ return 0;
+}
+
+#elif !defined(CC_SIDE)
+
+int main()
+{
+ printf("--- CompCert calling native:\n");
+ test();
+ printf("--- native calling CompCert:\n");
+ test();
+ return 0;
+}
+
+#endif
+
+
diff --git a/test/regression/varargs2.c b/test/regression/varargs2.c
index 6c091d8b..b96d1940 100644
--- a/test/regression/varargs2.c
+++ b/test/regression/varargs2.c
@@ -1,6 +1,9 @@
#include <stdarg.h>
#include <stdio.h>
+struct Y { char kind; unsigned char num; };
+struct Z { int x, y, z; };
+
void minivprintf(const char * fmt, va_list ap)
{
char c;
@@ -32,6 +35,14 @@ void minivprintf(const char * fmt, va_list ap)
case 'f':
printf("%.10g", (float) va_arg(ap, double));
break;
+ case 'y':
+ { struct Y s = va_arg(ap, struct Y);
+ printf("%c%d", s.kind, s.num);
+ break; }
+ case 'z':
+ { struct Z s = va_arg(ap, struct Z);
+ printf("(%d,%d,%d)", s.x, s.y, s.z);
+ break; }
default:
puts("<bad format>");
return;
@@ -111,9 +122,12 @@ int main()
miniprintf("A long long: %l\n", 123456789012345LL);
miniprintf("A string: %s\n", "Hello world");
miniprintf("A double: %e\n", 3.141592654);
- miniprintf("A mixture: %c & %s & %d & %l & %e & %f\n",
+ miniprintf("A small struct: %y\n", (struct Y) { 'x', 12 });
+ miniprintf("A bigger struct: %z\n", (struct Z) { 123, 456, 789 });
+ miniprintf("A mixture: %c & %s & %y & %d & %l & %e & %f\n",
'x',
"Hello, world!",
+ (struct Y) { 'y', 2 },
42,
123456789012345LL,
3.141592654,
generated by cgit (git 2.34.1) at 2024-06-29 01:44:31 +0000