aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--cparser/Cutil.ml70
-rw-r--r--cparser/Cutil.mli9
-rw-r--r--cparser/Machine.ml51
-rw-r--r--cparser/Machine.mli19
-rw-r--r--cparser/StructReturn.ml338
-rw-r--r--cparser/Unblock.ml2
-rw-r--r--driver/Driver.ml5
-rw-r--r--driver/Interp.ml6
-rw-r--r--ia32/PrintAsm.ml17
-rw-r--r--test/regression/Makefile9
-rw-r--r--test/regression/Results/interop162
-rw-r--r--test/regression/interop1.c285
12 files changed, 799 insertions, 74 deletions
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 9e7f102e..986c70a2 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -838,6 +838,14 @@ let eassign e1 e2 = { edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp }
let ecomma e1 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 +918,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..4f530fde 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -44,9 +44,16 @@ type t = {
alignof_fun: int option;
bigendian: bool;
bitfields_msb_first: bool;
- struct_return_as_int: int
+ supports_unaligned_accesses: bool;
+ struct_return_as_int: int;
+ struct_passing_style: struct_passing_style
}
+and struct_passing_style =
+ | SP_ref_callee
+ | SP_ref_caller
+ | SP_split_args
+
let ilp32ll64 = {
name = "ilp32ll64";
char_signed = false;
@@ -76,7 +83,9 @@ let ilp32ll64 = {
alignof_fun = None;
bigendian = false;
bitfields_msb_first = false;
- struct_return_as_int = 0
+ supports_unaligned_accesses = false;
+ struct_return_as_int = 0;
+ struct_passing_style = SP_ref_callee
}
let i32lpll64 = {
@@ -108,7 +117,9 @@ let i32lpll64 = {
alignof_fun = None;
bigendian = false;
bitfields_msb_first = false;
- struct_return_as_int = 0
+ supports_unaligned_accesses = false;
+ struct_return_as_int = 0;
+ struct_passing_style = SP_ref_callee
}
let il32pll64 = {
@@ -140,7 +151,9 @@ let il32pll64 = {
alignof_fun = None;
bigendian = false;
bitfields_msb_first = false;
- struct_return_as_int = 0
+ supports_unaligned_accesses = false;
+ struct_return_as_int = 0;
+ struct_passing_style = SP_ref_callee
}
(* Canned configurations for some ABIs *)
@@ -149,9 +162,17 @@ 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;
+ struct_passing_style = SP_split_args }
+
+let x86_32_macosx =
+ { x86_32 with sizeof_longdouble = 16; alignof_longdouble = 16;
+ struct_return_as_int = 8 }
+
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 +183,14 @@ let ppc_32_bigendian =
{ ilp32ll64 with name = "powerpc";
bigendian = true;
bitfields_msb_first = true;
- struct_return_as_int = 8 }
+ supports_unaligned_accesses = true;
+ struct_return_as_int = 8;
+ struct_passing_style = SP_ref_caller }
+
let arm_littleendian =
{ ilp32ll64 with name = "arm";
- struct_return_as_int = 4 }
+ struct_return_as_int = 4;
+ struct_passing_style = SP_split_args }
(* Add GCC extensions re: sizeof and alignof *)
@@ -173,6 +198,14 @@ 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;
+ struct_return_as_int = 0;
+ struct_passing_style = SP_ref_callee }
+
(* Undefined configuration *)
let undef = {
@@ -204,7 +237,9 @@ let undef = {
alignof_fun = None;
bigendian = false;
bitfields_msb_first = false;
- struct_return_as_int = 0
+ supports_unaligned_accesses = false;
+ struct_return_as_int = 0;
+ struct_passing_style = SP_ref_callee
}
(* The current configuration. Must be initialized before use. *)
diff --git a/cparser/Machine.mli b/cparser/Machine.mli
index b544711f..0fd8431f 100644
--- a/cparser/Machine.mli
+++ b/cparser/Machine.mli
@@ -44,13 +44,27 @@ type t = {
alignof_fun: int option;
bigendian: bool;
bitfields_msb_first: bool;
- struct_return_as_int: int
+ supports_unaligned_accesses: bool;
+ struct_return_as_int: int;
+ struct_passing_style: struct_passing_style
}
+and 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 *)
+
+(* 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 +72,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..81f3425c 100644
--- a/cparser/StructReturn.ml
+++ b/cparser/StructReturn.ml
@@ -13,7 +13,9 @@
(* *)
(* *********************************************************************)
-(* 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 C
@@ -40,10 +42,124 @@ let classify_return env ty =
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 (!config).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 ucharptr = TPtr(uchar, [])
+let ushortptr = TPtr(ushort, [])
+let uintptr = TPtr(uint, [])
+
+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 ereinterpret ty e =
+ { edesc = EUnop(Oderef, ecast (TPtr(ty, [])) (eaddrof e)); etyp = ty }
+
+let attr_structret = [Attr("__structreturn", [])]
+
+(* Expression constructor functions *)
+
+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 =
+ { 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 rec load_words base ofs sz al =
+ if ofs + 4 <= sz then
+ (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))
+ :: load_words base (ofs + 4) sz al
+ else if ofs + 3 = sz then
+ [ 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) ]
+ else if ofs + 2 = sz then
+ [ 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) ]
+ else if ofs + 1 = sz then
+ [ load1 base ofs 0 3 ]
+ else
+ []
+
+(* 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,21 +167,24 @@ 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 ->
+ 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)
+ TFun(TVoid [], Some((res, TPtr(tres', [])) :: args'), vararg,
+ add_attributes attr attr_structret)
| Ret_value ty ->
TFun(ty, Some args', vararg, attr)
end
@@ -77,12 +196,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 +233,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 +268,88 @@ 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 ->
+ 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: copy to array and pass array elts
+ arg ---> (*((ty *) temparray) = arg ...
+ temparray[0], ...,, temparray[N-1]
+*)
+
+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 (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 *)
@@ -256,29 +431,78 @@ 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))
+ transf_funbody env (subst_stmt subst 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
+ (f.fd_attrib,
+ ty,
+ params,
+ transf_funbody env (subst_stmt subst f.fd_body) (Some eres)) 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 *)
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/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;
diff --git a/driver/Interp.ml b/driver/Interp.ml
index ab22cebb..57f252b0 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -380,6 +380,7 @@ 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 =
@@ -399,6 +400,7 @@ 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
@@ -406,8 +408,12 @@ 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
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index b0ef0180..2ffd5600 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -844,8 +844,10 @@ let print_instruction oc = function
| 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
@@ -861,11 +863,20 @@ let print_instruction oc = function
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"
+ 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)
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..34ec8e6b
--- /dev/null
+++ b/test/regression/Results/interop1
@@ -0,0 +1,62 @@
+--- CompCert calling native:
+s1 = { a = 'a' }
+s2 = { a = 'x', b = 'y' }
+s3 = { a = 'a', b = 'b', c = ' c' }
+s4 = { a = 'p', b = 'q', c = ' r', d = 's' }
+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 = 12 }
+t2 = { a = 34, b = 56 }
+t3 = { a = -1, b = -2, c = -3 }
+t4 = { a = 11, b = 22, c = 33, d = 44 }
+t4 = { a = 1, b = 2, c = 3, d = 4, e = 'x' }
+u1 = { a = 12345678 }
+u2 = { a = 1, b = -1 }
+u3 = { a = -1, b = -2, c = -3 }
+u4 = { a = 4, b = 3, c = 2, d = 1 }
+u5 = { a = 123, b = 'z' }
+u6 = { a = -12345678, b = 555 }
+u7 = { a = 111111111, b = 2222, c = 'a' }
+u8 = { a = 'u', b = 8 }
+u9 = { a = 3.14159, b = -2.718 }
+rs1 = { a = 'a' }
+rs2 = { a = 'a', b = 'b' }
+rs3 = { a = 'a', b = 'b', c = 'c' }
+rs4 = { a = 'a', b = 'b', c = 'c', d = 'd' }
+rs8 = { "Lorem ipsum" }
+ru2 = { a = 12, b = -34 }
+ru6 = { a = 12345678, b = -9999 }
+ru9 = { a = 0.123400, b = -5678.900000 }
+--- native calling CompCert:
+s1 = { a = 'a' }
+s2 = { a = 'x', b = 'y' }
+s3 = { a = 'a', b = 'b', c = ' c' }
+s4 = { a = 'p', b = 'q', c = ' r', d = 's' }
+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 = 12 }
+t2 = { a = 34, b = 56 }
+t3 = { a = -1, b = -2, c = -3 }
+t4 = { a = 11, b = 22, c = 33, d = 44 }
+t4 = { a = 1, b = 2, c = 3, d = 4, e = 'x' }
+u1 = { a = 12345678 }
+u2 = { a = 1, b = -1 }
+u3 = { a = -1, b = -2, c = -3 }
+u4 = { a = 4, b = 3, c = 2, d = 1 }
+u5 = { a = 123, b = 'z' }
+u6 = { a = -12345678, b = 555 }
+u7 = { a = 111111111, b = 2222, c = 'a' }
+u8 = { a = 'u', b = 8 }
+u9 = { a = 3.14159, b = -2.718 }
+rs1 = { a = 'a' }
+rs2 = { a = 'a', b = 'b' }
+rs3 = { a = 'a', b = 'b', c = 'c' }
+rs4 = { a = 'a', b = 'b', c = 'c', d = 'd' }
+rs8 = { "Lorem ipsum" }
+ru2 = { a = 12, b = -34 }
+ru6 = { a = 12345678, b = -9999 }
+ru9 = { a = 0.123400, b = -5678.900000 }
diff --git a/test/regression/interop1.c b/test/regression/interop1.c
new file mode 100644
index 00000000..325eb574
--- /dev/null
+++ b/test/regression/interop1.c
@@ -0,0 +1,285 @@
+#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; };
+struct S2 { char a, b; };
+struct S3 { char a, b, c; };
+struct S4 { char a, b, c, d; };
+struct S5 { char a, b, c, d, e; };
+struct S6 { char a, b, c, d, e, f; };
+struct S7 { char a, b, c, d, e, f, g; };
+struct S8 { char a[32]; };
+
+/* Alignment 2 */
+struct T1 { short a; };
+struct T2 { short a, b; };
+struct T3 { short a, b, c; };
+struct T4 { short a, b, c, d; };
+struct T5 { short a, b, c, d; char e; };
+
+/* Alignment >= 4 */
+struct U1 { int a; };
+struct U2 { int a, b; };
+struct U3 { int a, b, c; };
+struct U4 { int a, b, c, d; };
+struct U5 { int a; char b; };
+struct U6 { int a; short b; };
+struct U7 { int a; short b; char c; };
+struct U8 { char a; int b; };
+struct U9 { double a, b; };
+
+/* Struct passing */
+
+extern void THEM(s1) (struct S1 x);
+void US(s1) (struct S1 x)
+{
+ printf("s1 = { a = '%c' }\n", x.a);
+}
+
+extern void THEM(s2) (struct S2 x);
+void US(s2) (struct S2 x)
+{
+ printf("s2 = { a = '%c', b = '%c' }\n", x.a, x.b);
+}
+
+extern void THEM(s3) (struct S3 x);
+void US(s3) (struct S3 x)
+{
+ printf("s3 = { a = '%c', b = '%c', c = ' %c' }\n", x.a, x.b, x.c);
+}
+
+extern void THEM(s4) (struct S4 x);
+void US(s4) (struct S4 x)
+{
+ printf("s4 = { a = '%c', b = '%c', c = ' %c', d = '%c' }\n",
+ x.a, x.b, x.c, x.d);
+}
+
+extern void THEM(s5) (struct S5 x);
+void US(s5) (struct S5 x)
+{
+ printf("s5 = { a = '%c', b = '%c', c = ' %c', d = '%c', e = '%c' }\n",
+ x.a, x.b, x.c, x.d, x.e);
+}
+
+extern void THEM(s6) (struct S6 x);
+void US(s6) (struct S6 x)
+{
+ printf("s6 = { 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);
+}
+
+extern void THEM(s7) (struct S7 x);
+void US(s7) (struct S7 x)
+{
+ printf("s7 = { 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);
+}
+
+extern void THEM(s8) (struct S8 x);
+void US(s8) (struct S8 x)
+{
+ printf("s8 = \"%s\"\n", x.a);
+}
+
+extern void THEM(t1) (struct T1 x);
+void US(t1) (struct T1 x)
+{
+ printf("t1 = { a = %d }\n", x.a);
+}
+
+extern void THEM(t2) (struct T2 x);
+void US(t2) (struct T2 x)
+{
+ printf("t2 = { a = %d, b = %d }\n", x.a, x.b);
+}
+
+extern void THEM(t3) (struct T3 x);
+void US(t3) (struct T3 x)
+{
+ printf("t3 = { a = %d, b = %d, c = %d }\n", x.a, x.b, x.c);
+}
+
+extern void THEM(t4) (struct T4 x);
+void US(t4) (struct T4 x)
+{
+ printf("t4 = { a = %d, b = %d, c = %d, d = %d }\n", x.a, x.b, x.c, x.d);
+}
+
+extern void THEM(t5) (struct T5 x);
+void US(t5) (struct T5 x)
+{
+ printf("t4 = { a = %d, b = %d, c = %d, d = %d, e = '%c' }\n",
+ x.a, x.b, x.c, x.d, x.e);
+}
+
+extern void THEM(u1) (struct U1 x);
+void US(u1) (struct U1 x)
+{
+ printf("u1 = { a = %d }\n", x.a);
+}
+
+extern void THEM(u2) (struct U2 x);
+void US(u2) (struct U2 x)
+{
+ printf("u2 = { a = %d, b = %d }\n", x.a, x.b);
+}
+
+extern void THEM(u3) (struct U3 x);
+void US(u3) (struct U3 x)
+{
+ printf("u3 = { a = %d, b = %d, c = %d }\n", x.a, x.b, x.c);
+}
+
+extern void THEM(u4) (struct U4 x);
+void US(u4) (struct U4 x)
+{
+ printf("u4 = { a = %d, b = %d, c = %d, d = %d }\n", x.a, x.b, x.c, x.d);
+}
+
+extern void THEM(u5) (struct U5 x);
+void US(u5) (struct U5 x)
+{
+ printf("u5 = { a = %d, b = '%c' }\n", x.a, x.b);
+}
+
+extern void THEM(u6) (struct U6 x);
+void US(u6) (struct U6 x)
+{
+ printf("u6 = { a = %d, b = %d }\n", x.a, x.b);
+}
+
+extern void THEM(u7) (struct U7 x);
+void US(u7) (struct U7 x)
+{
+ printf("u7 = { a = %d, b = %d, c = '%c' }\n", x.a, x.b, x.c);
+}
+
+extern void THEM(u8) (struct U8 x);
+void US(u8) (struct U8 x)
+{
+ printf("u8 = { a = '%c', b = %d }\n", x.a, x.b);
+}
+
+extern void THEM(u9) (struct U9 x);
+void US(u9) (struct U9 x)
+{
+ printf("u9 = { a = %g, b = %g }\n", x.a, x.b);
+}
+
+/* Struct return */
+
+extern struct S1 THEM(rs1) (void);
+struct S1 US(rs1) (void)
+{ return (struct S1){ 'a' }; }
+
+extern struct S2 THEM(rs2) (void);
+struct S2 US(rs2) (void)
+{ return (struct S2){ 'a', 'b' }; }
+
+extern struct S3 THEM(rs3) (void);
+struct S3 US(rs3) (void)
+{ return (struct S3){ 'a', 'b', 'c' }; }
+
+extern struct S4 THEM(rs4) (void);
+struct S4 US(rs4) (void)
+{ return (struct S4){ 'a', 'b', 'c', 'd' }; }
+
+extern struct S8 THEM(rs8) (void);
+struct S8 US(rs8) (void)
+{ return (struct S8){ "Lorem ipsum" }; }
+
+extern struct U2 THEM(ru2) (void);
+struct U2 US(ru2) (void)
+{ return (struct U2){ 12, -34 }; }
+
+extern struct U6 THEM(ru6) (void);
+struct U6 US(ru6) (void)
+{ return (struct U6){ 12345678, -9999 }; }
+
+extern struct U9 THEM(ru9) (void);
+struct U9 US(ru9) (void)
+{ return (struct U9){ 0.1234, -5678.9 }; }
+
+/* Test function, calling the functions compiled by the other compiler */
+
+extern void THEM(test) (void);
+void US(test) (void)
+{
+ THEM(s1)((struct S1) {'a'});
+ THEM(s2)((struct S2) {'x', 'y'});
+ THEM(s3)((struct S3) {'a', 'b', 'c'});
+ THEM(s4)((struct S4) {'p', 'q', 'r', 's'});
+ THEM(s5)((struct S5) {'a', 'b', 'c', 'd', 'e'});
+ THEM(s6)((struct S6) {'a', 'b', 'c', 'd', 'e', 'f'});
+ THEM(s7)((struct S7) {'a', 'b', 'c', 'd', 'e', 'f', 'g'});
+ THEM(s8)((struct S8) { "Hello, world!" });
+ THEM(t1)((struct T1) { 12 });
+ THEM(t2)((struct T2) { 34, 56 });
+ THEM(t3)((struct T3) { -1, -2, -3});
+ THEM(t4)((struct T4) { 11, 22, 33, 44} );
+ THEM(t5)((struct T5) { 1, 2, 3, 4, 'x'});
+ THEM(u1)((struct U1) { 12345678 } );
+ THEM(u2)((struct U2) { 1, -1});
+ THEM(u3)((struct U3) { -1, -2, -3 });
+ THEM(u4)((struct U4) { 4, 3, 2, 1 });
+ THEM(u5)((struct U5) { 123, 'z' });
+ THEM(u6)((struct U6) { -12345678, 555 });
+ THEM(u7)((struct U7) { 111111111, 2222, 'a' });
+ THEM(u8)((struct U8) { 'u', 8 });
+ THEM(u9)((struct U9) { 3.14159, -2.718 });
+ { struct S1 x = THEM(rs1)();
+ printf("rs1 = { a = '%c' }\n", x.a); }
+ { struct S2 x = THEM(rs2)();
+ printf("rs2 = { a = '%c', b = '%c' }\n", x.a, x.b); }
+ { struct S3 x = THEM(rs3)();
+ printf("rs3 = { a = '%c', b = '%c', c = '%c' }\n", x.a, x.b, x.c); }
+ { struct S4 x = THEM(rs4)();
+ printf("rs4 = { a = '%c', b = '%c', c = '%c', d = '%c' }\n",
+ x.a, x.b, x.c, x.d); }
+ { struct S8 x = THEM(rs8)();
+ printf("rs8 = { \"%s\" }\n", x.a); }
+ { struct U2 x = THEM(ru2)();
+ printf("ru2 = { a = %d, b = %d }\n", x.a, x.b); }
+ { struct U6 x = THEM(ru6)();
+ printf("ru6 = { a = %d, b = %d }\n", x.a, x.b); }
+ { struct U9 x = THEM(ru9)();
+ printf("ru9 = { a = %f, b = %f }\n", x.a, x.b); }
+}
+
+#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
+
+
generated by cgit (git 2.34.1) at 2024-06-12 02:42:45 +0000