Commit e096fa7a authored by Xavier Leroy's avatar Xavier Leroy
Browse files

ABI compatibility for struct/union function arguments passed by value.

The passing of struct/union arguments by value implemented in the verified
part of CompCert is not compatible with the ARM, PowerPC and x86 ABI.
Here we enrich the StructReturn source-to-source emulation pass
so that it implements the calling conventions defined in these ABIs.

Plus: for x86, implement the returning of struct/union results by value
in a way compatible with the ABI.
parent f00b70b6
......@@ -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)
}
......@@ -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
......@@ -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. *)
......
......@@ -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
......@@ -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,