Commit 9ab3738a authored by Bernhard Schommer's avatar Bernhard Schommer Committed by Xavier Leroy
Browse files

Changed cc_varargs to an option type

Instead of being a simple boolean we now use an option type to record
the number of fixed (non-vararg) arguments.  Hence, `None` means
not vararg, and `Some n` means `n` fixed arguments followed with varargs.
parent a138b43c
......@@ -545,7 +545,7 @@ module FixupHF = struct
end
let fixup_arguments dir sg =
if sg.sig_cc.cc_vararg then
if sg.sig_cc.cc_vararg <> None then
FixupEABI.fixup_arguments dir sg
else begin
let act = fixup_actions (Array.make 16 false) 0 sg.sig_args in
......@@ -555,7 +555,7 @@ module FixupHF = struct
end
let fixup_result dir sg =
if sg.sig_cc.cc_vararg then
if sg.sig_cc.cc_vararg <> None then
FixupEABI.fixup_result dir sg
end
......
......@@ -54,7 +54,7 @@ let get_current_function_args () =
(!current_function).fn_sig.sig_args
let is_current_function_variadic () =
(!current_function).fn_sig.sig_cc.cc_vararg
(!current_function).fn_sig.sig_cc.cc_vararg <> None
let get_current_function_sig () =
(!current_function).fn_sig
......
......@@ -552,10 +552,16 @@ let convertAttr a =
let n = Cutil.alignas_attribute a in
if n > 0 then Some (N.of_int (log2 n)) else None }
let convertCallconv va unproto attr =
let convertCallconv _tres targs va attr =
let vararg =
match targs with
| None -> None
| Some tl -> if va then Some (Z.of_uint (List.length tl)) else None in
let sr =
Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in
{ AST.cc_vararg = va; cc_unproto = unproto; cc_structret = sr <> [] }
{ AST.cc_vararg = vararg;
AST.cc_unproto = (targs = None);
AST.cc_structret = (sr <> []) }
(** Types *)
......@@ -623,7 +629,7 @@ let rec convertTyp env t =
| Some tl -> convertParams env tl
end,
convertTyp env tres,
convertCallconv va (targs = None) a)
convertCallconv tres targs va a)
| C.TNamed _ ->
convertTyp env (Cutil.unroll env t)
| C.TStruct(id, a) ->
......@@ -989,7 +995,7 @@ let rec convertExpr env e =
and tres = convertTyp env e.etyp in
let sg =
signature_of_type targs tres
{ AST.cc_vararg = true; cc_unproto = false; cc_structret = false} in
{ AST.cc_vararg = Some (coqint_of_camlint 1l); cc_unproto = false; cc_structret = false} in
Ebuiltin( AST.EF_external(coqstring_of_camlstring "printf", sg),
targs, convertExprList env args, tres)
......@@ -1256,7 +1262,8 @@ let convertFundef loc env fd =
a_loc = loc };
(id', AST.Gfun(Ctypes.Internal
{fn_return = ret;
fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib;
fn_callconv = convertCallconv fd.fd_ret (Some fd.fd_params)
fd.fd_vararg fd.fd_attrib;
fn_params = params;
fn_vars = vars;
fn_body = body'}))
......
......@@ -94,6 +94,7 @@ Proof.
decide equality.
decide equality.
decide equality.
decide equality.
Defined.
Opaque type_eq typelist_eq.
......
......@@ -170,7 +170,7 @@ Definition floatsize_eq: forall (x y: floatsize), {x=y} + {x<>y}.
Proof. decide equality. Defined.
Definition callconv_combine (cc1 cc2: calling_convention) : res calling_convention :=
if bool_eq cc1.(cc_vararg) cc2.(cc_vararg) then
if option_eq Z.eq_dec cc1.(cc_vararg) cc2.(cc_vararg) then
OK {| cc_vararg := cc1.(cc_vararg);
cc_unproto := cc1.(cc_unproto) && cc2.(cc_unproto);
cc_structret := cc1.(cc_structret) |}
......
......@@ -111,8 +111,8 @@ let rec name_cdecl id ty =
| Tnil ->
if first then
Buffer.add_string b
(if cconv.cc_vararg then "..." else "void")
else if cconv.cc_vararg then
(if cconv.cc_vararg <> None then "..." else "void")
else if cconv.cc_vararg <> None then
Buffer.add_string b ", ..."
else
()
......@@ -400,11 +400,11 @@ let name_function_parameters name_param fun_name params cconv =
Buffer.add_char b '(';
begin match params with
| [] ->
Buffer.add_string b (if cconv.cc_vararg then "..." else "void")
Buffer.add_string b (if cconv.cc_vararg <> None then "..." else "void")
| _ ->
let rec add_params first = function
| [] ->
if cconv.cc_vararg then Buffer.add_string b ",..."
if cconv.cc_vararg <> None then Buffer.add_string b ",..."
| (id, ty) :: rem ->
if not first then Buffer.add_string b ", ";
Buffer.add_string b (name_cdecl (name_param id) ty);
......
......@@ -122,17 +122,17 @@ These signatures are used in particular to determine appropriate
calling conventions for the function. *)
Record calling_convention : Type := mkcallconv {
cc_vararg: bool; (**r variable-arity function *)
cc_unproto: bool; (**r old-style unprototyped function *)
cc_structret: bool (**r function returning a struct *)
cc_vararg: option Z; (**r variable-arity function (+ number of fixed args) *)
cc_unproto: bool; (**r old-style unprototyped function *)
cc_structret: bool (**r function returning a struct *)
}.
Definition cc_default :=
{| cc_vararg := false; cc_unproto := false; cc_structret := false |}.
{| cc_vararg := None; cc_unproto := false; cc_structret := false |}.
Definition calling_convention_eq (x y: calling_convention) : {x=y} + {x<>y}.
Proof.
decide equality; apply bool_dec.
decide equality; try (apply bool_dec). decide equality; apply Z.eq_dec.
Defined.
Global Opaque calling_convention_eq.
......
......@@ -216,8 +216,8 @@ and typlist p = function
and callconv p cc =
if cc = cc_default
then fprintf p "cc_default"
else fprintf p "{|cc_vararg:=%b; cc_unproto:=%b; cc_structret:=%b|}"
cc.cc_vararg cc.cc_unproto cc.cc_structret
else fprintf p "{|cc_vararg:=%a; cc_unproto:=%b; cc_structret:=%b|}"
(print_option coqZ) cc.cc_vararg cc.cc_unproto cc.cc_structret
(* External functions *)
......
......@@ -830,7 +830,7 @@ let expand_builtin_inline name args res =
function is unprototyped. *)
let set_cr6 sg =
if sg.sig_cc.cc_vararg || sg.sig_cc.cc_unproto then begin
if (sg.sig_cc.cc_vararg <> None) || sg.sig_cc.cc_unproto then begin
if List.exists (function Tfloat | Tsingle -> true | _ -> false) sg.sig_args
then emit (Pcreqv(CRbit_6, CRbit_6, CRbit_6))
else emit (Pcrxor(CRbit_6, CRbit_6, CRbit_6))
......
......@@ -100,7 +100,7 @@ let rec fixup_variadic_call ri rf tyl =
end
let fixup_call sg =
if sg.sig_cc.cc_vararg then fixup_variadic_call 0 0 sg.sig_args
if (sg.sig_cc.cc_vararg <> None) then fixup_variadic_call 0 0 sg.sig_args
(* Handling of annotations *)
......@@ -588,7 +588,7 @@ let expand_instruction instr =
| Pallocframe (sz, ofs) ->
let sg = get_current_function_sig() in
emit (Pmv (X30, X2));
if sg.sig_cc.cc_vararg then begin
if (sg.sig_cc.cc_vararg <> None) then begin
let n = arguments_size sg in
let extra_sz = if n >= 8 then 0 else align ((8 - n) * wordsize) 16 in
let full_sz = Z.add sz (Z.of_uint extra_sz) in
......@@ -606,7 +606,7 @@ let expand_instruction instr =
| Pfreeframe (sz, ofs) ->
let sg = get_current_function_sig() in
let extra_sz =
if sg.sig_cc.cc_vararg then begin
if (sg.sig_cc.cc_vararg <> None) then begin
let n = arguments_size sg in
if n >= 8 then 0 else align ((8 - n) * wordsize) 16
end else 0 in
......
......@@ -281,7 +281,8 @@ Fixpoint loc_arguments_rec (va: bool)
when calling a function with signature [s]. *)
Definition loc_arguments (s: signature) : list (rpair loc) :=
loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0 0.
let va := match s.(sig_cc).(cc_vararg) with Some _ => true | None => false end in
loc_arguments_rec va s.(sig_args) 0 0 0.
(** Argument locations are either non-temporary registers or [Outgoing]
stack slots at nonnegative offsets. *)
......
......@@ -500,7 +500,7 @@ let expand_builtin_inline name args res =
unprototyped. *)
let fixup_funcall_elf64 sg =
if sg.sig_cc.cc_vararg || sg.sig_cc.cc_unproto then begin
if sg.sig_cc.cc_vararg <> None || sg.sig_cc.cc_unproto then begin
let (ir, fr, ofs) = next_arg_locations 0 0 0 sg.sig_args in
emit (Pmovl_ri (RAX, coqint_of_camlint (Int32.of_int fr)))
end
......@@ -521,7 +521,7 @@ let rec copy_fregs_to_iregs args fr ir =
()
let fixup_funcall_win64 sg =
if sg.sig_cc.cc_vararg then
if sg.sig_cc.cc_vararg <> None then
copy_fregs_to_iregs sg.sig_args [XMM0; XMM1; XMM2; XMM3] [RCX; RDX; R8; R9]
let fixup_funcall sg =
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment