summaryrefslogtreecommitdiff
path: root/cfrontend
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend')
-rw-r--r--cfrontend/C2C.ml132
-rw-r--r--cfrontend/Cexec.v22
-rw-r--r--cfrontend/Clight.v19
-rw-r--r--cfrontend/ClightBigstep.v20
-rw-r--r--cfrontend/Cop.v16
-rw-r--r--cfrontend/Csem.v12
-rw-r--r--cfrontend/Csharpminor.v2
-rw-r--r--cfrontend/Cshmgen.v35
-rw-r--r--cfrontend/Cshmgenproof.v43
-rw-r--r--cfrontend/Cstrategy.v36
-rw-r--r--cfrontend/Csyntax.v7
-rw-r--r--cfrontend/Ctypes.v36
-rw-r--r--cfrontend/Initializersproof.v2
-rw-r--r--cfrontend/PrintClight.ml10
-rw-r--r--cfrontend/PrintCsyntax.ml50
-rw-r--r--cfrontend/SimplExpr.v5
-rw-r--r--cfrontend/SimplExprproof.v6
-rw-r--r--cfrontend/SimplExprspec.v5
-rw-r--r--cfrontend/SimplLocals.v3
-rw-r--r--cfrontend/SimplLocalsproof.v4
20 files changed, 230 insertions, 235 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index f12efa3..4cac92c 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -143,39 +143,6 @@ let globals_for_strings globs =
(fun s id l -> global_for_string s id :: l)
stringTable globs
-(** ** Declaration of special external functions *)
-
-let special_externals_table : (string, fundef) Hashtbl.t = Hashtbl.create 47
-
-let register_special_external name ef targs tres =
- if not (Hashtbl.mem special_externals_table name) then
- Hashtbl.add special_externals_table name (External(ef, targs, tres))
-
-let declare_special_externals k =
- Hashtbl.fold
- (fun name fd k -> (intern_string name, Gfun fd) :: k)
- special_externals_table k
-
-(** ** Handling of stubs for variadic functions *)
-
-let register_stub_function name tres targs =
- let rec letters_of_type = function
- | Tnil -> []
- | Tcons(Tfloat _, tl) -> "f" :: letters_of_type tl
- | Tcons(Tlong _, tl) -> "l" :: letters_of_type tl
- | Tcons(_, tl) -> "i" :: letters_of_type tl in
- let rec types_of_types = function
- | Tnil -> Tnil
- | Tcons(Tfloat _, tl) -> Tcons(Tfloat(F64, noattr), types_of_types tl)
- | Tcons(Tlong _, tl) -> Tcons(Tlong(Signed, noattr), types_of_types tl)
- | Tcons(_, tl) -> Tcons(Tpointer(Tvoid, noattr), types_of_types tl) in
- let stub_name =
- name ^ "$" ^ String.concat "" (letters_of_type targs) in
- let targs = types_of_types targs in
- let ef = EF_external(intern_string stub_name, signature_of_type targs tres) in
- register_special_external stub_name ef targs tres;
- (stub_name, Tfunction (targs, tres))
-
(** ** Handling of inlined memcpy functions *)
let make_builtin_memcpy args =
@@ -230,11 +197,16 @@ let mergeTypAttr ty a2 =
| Tlong(sg, a1) -> Tlong(sg, mergeAttr a1 a2)
| Tpointer(ty', a1) -> Tpointer(ty', mergeAttr a1 a2)
| Tarray(ty', sz, a1) -> Tarray(ty', sz, mergeAttr a1 a2)
- | Tfunction(targs, tres) -> ty
+ | Tfunction(targs, tres, cc) -> ty
| Tstruct(id, fld, a1) -> Tstruct(id, fld, mergeAttr a1 a2)
| Tunion(id, fld, a1) -> Tunion(id, fld, mergeAttr a1 a2)
| Tcomp_ptr(id, a1) -> Tcomp_ptr(id, mergeAttr a1 a2)
+let convertCallconv va attr =
+ let sr =
+ Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in
+ { cc_vararg = va; cc_structret = sr <> [] }
+
(** Types *)
let convertIkind = function
@@ -293,14 +265,15 @@ let convertTyp env t =
| C.TArray(ty, Some sz, a) ->
Tarray(convertTyp seen ty, convertInt sz, convertAttr a)
| C.TFun(tres, targs, va, a) ->
- if va then unsupported "variadic function type";
+ (* if va then unsupported "variadic function type"; *)
if Cutil.is_composite_type env tres then
unsupported "return type is a struct or union";
Tfunction(begin match targs with
| None -> (*warning "un-prototyped function type";*) Tnil
| Some tl -> convertParams seen tl
end,
- convertTyp seen tres)
+ convertTyp seen tres,
+ convertCallconv va a)
| C.TNamed _ ->
assert false
| C.TStruct(id, a) ->
@@ -347,9 +320,20 @@ let convertTyp env t =
in convertTyp [] t
+(*
let rec convertTypList env = function
| [] -> Tnil
| t1 :: tl -> Tcons(convertTyp env t1, convertTypList env tl)
+*)
+
+let rec convertTypArgs env tl el =
+ match tl, el with
+ | _, [] -> Tnil
+ | [], e1 :: el ->
+ Tcons(convertTyp env (Cutil.default_argument_conversion env e1.etyp),
+ convertTypArgs env [] el)
+ | (id, t1) :: tl, e1 :: el ->
+ Tcons(convertTyp env t1, convertTypArgs env tl el)
let cacheCompositeDef env su id attr flds =
let ty =
@@ -358,12 +342,6 @@ let cacheCompositeDef env su id attr flds =
| C.Union -> C.TUnion(id, attr) in
Hashtbl.add compositeCache id (convertTyp env ty)
-let rec projFunType env ty =
- match Cutil.unroll env ty with
- | TFun(res, args, vararg, attr) -> Some(res, args, vararg)
- | TPtr(ty', attr) -> projFunType env ty'
- | _ -> None
-
let string_of_type ty =
let b = Buffer.create 20 in
let fb = Format.formatter_of_buffer b in
@@ -544,10 +522,7 @@ let rec convertExpr env e =
| C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) ->
begin match args with
| {edesc = C.EConst(CStr txt)} :: args1 ->
- let targs1 =
- convertTypList env
- (List.map (fun e -> Cutil.default_argument_conversion env e.etyp)
- args1) in
+ let targs1 = convertTypArgs env [] args1 in
Ebuiltin(
EF_annot(intern_string txt,
List.map (fun t -> AA_arg t) (typlist_of_typelist targs1)),
@@ -575,36 +550,19 @@ let rec convertExpr env e =
| C.ECall({edesc = C.EVar {name = "__builtin_fabs"}}, [arg]) ->
Eunop(Oabsfloat, convertExpr env arg, ty)
+ | C.ECall({edesc = C.EVar {name = "printf"}}, args)
+ when !Clflags.option_interp ->
+ let targs =
+ convertTypArgs env [] args in
+ let sg =
+ signature_of_type targs ty {cc_vararg = true; cc_structret = false} in
+ Ebuiltin(EF_external(intern_string "printf", sg),
+ targs, convertExprList env args, ty)
+
| C.ECall(fn, args) ->
if not (supported_return_type env e.etyp) then
unsupported ("function returning a result of type " ^ string_of_type e.etyp);
- match projFunType env fn.etyp with
- | None ->
- error "wrong type for function part of a call"; ezero
- | Some(tres, targs, false) ->
- (* Non-variadic function *)
- if targs = None then
- unsupported "call to non-prototyped function";
- Ecall(convertExpr env fn, convertExprList env args, ty)
- | Some(tres, targs, true) ->
- (* Variadic function: generate a call to a stub function with
- the appropriate number and types of arguments. Works only if
- the function expression e is a global variable. *)
- let fun_name =
- match fn with
- | {edesc = C.EVar id} when !Clflags.option_fvararg_calls ->
- (*warning "emulating call to variadic function"; *)
- id.name
- | _ ->
- unsupported "call to variadic function";
- "<error>" in
- let targs = convertTypList env (List.map (fun e -> e.etyp) args) in
- let tres = convertTyp env tres in
- let (stub_fun_name, stub_fun_typ) =
- register_stub_function fun_name tres targs in
- Ecall(Evalof(Evar(intern_string stub_fun_name, stub_fun_typ),
- stub_fun_typ),
- convertExprList env args, ty)
+ Ecall(convertExpr env fn, convertExprList env args, ty)
and convertLvalue env e =
let ty = convertTyp env e.etyp in
@@ -787,25 +745,28 @@ let convertFundef loc env fd =
a_access = Sections.Access_default;
a_inline = fd.fd_inline;
a_loc = loc };
- (id', Gfun(Internal {fn_return = ret; fn_params = params;
- fn_vars = vars; fn_body = body'}))
+ (id', Gfun(Internal {fn_return = ret;
+ fn_callconv = convertCallconv fd.fd_vararg fd.fd_attrib;
+ fn_params = params;
+ fn_vars = vars;
+ fn_body = body'}))
(** External function declaration *)
let convertFundecl env (sto, id, ty, optinit) =
- let (args, res) =
+ let (args, res, cconv) =
match convertTyp env ty with
- | Tfunction(args, res) -> (args, res)
+ | Tfunction(args, res, cconv) -> (args, res, cconv)
| _ -> assert false in
let id' = intern_string id.name in
- let sg = signature_of_type args res in
+ let sg = signature_of_type args res cconv in
let ef =
if id.name = "malloc" then EF_malloc else
if id.name = "free" then EF_free else
if List.mem_assoc id.name builtins.functions
then EF_builtin(id', sg)
else EF_external(id', sg) in
- (id', Gfun(External(ef, args, res)))
+ (id', Gfun(External(ef, args, res, cconv)))
(** Initializers *)
@@ -894,16 +855,13 @@ let rec convertGlobdecls env res gl =
match g.gdesc with
| C.Gdecl((sto, id, ty, optinit) as d) ->
(* Prototyped functions become external declarations.
- Variadic functions are skipped.
Other types become variable declarations. *)
begin match Cutil.unroll env ty with
- | TFun(_, Some _, false, _) ->
+ | TFun(_, Some _, _, _) ->
convertGlobdecls env (convertFundecl env d :: res) gl'
- | TFun(_, None, false, _) ->
+ | TFun(_, None, _, _) ->
unsupported ("'" ^ id.name ^ "' is declared without a function prototype");
convertGlobdecls env res gl'
- | TFun(_, _, true, _) ->
- convertGlobdecls env res gl'
| _ ->
convertGlobdecls env (convertGlobvar g.gloc env d :: res) gl'
end
@@ -1002,15 +960,13 @@ let convertProgram p =
Hashtbl.clear decl_atom;
Hashtbl.clear stringTable;
Hashtbl.clear compositeCache;
- Hashtbl.clear special_externals_table;
let p = Builtins.declarations() @ p in
try
let gl1 = convertGlobdecls (translEnv Env.empty p) [] (cleanupGlobals p) in
- let gl2 = declare_special_externals gl1 in
- let gl3 = globals_for_strings gl2 in
+ let gl2 = globals_for_strings gl1 in
if !numErrors > 0
then None
- else Some { AST.prog_defs = gl3;
+ else Some { AST.prog_defs = gl2;
AST.prog_main = intern_string "main" }
with Env.Error msg ->
error (Env.error_message msg); None
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 79dd26f..9593afd 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -887,10 +887,10 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
match is_val r1, is_val_list rargs with
| Some(vf, tyf), Some vtl =>
match classify_fun tyf with
- | fun_case_f tyargs tyres =>
+ | fun_case_f tyargs tyres cconv =>
do fd <- Genv.find_funct ge vf;
do vargs <- sem_cast_arguments vtl tyargs;
- check type_eq (type_of_fundef fd) (Tfunction tyargs tyres);
+ check type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv);
topred (Callred fd vargs ty m)
| _ => stuck
end
@@ -1020,14 +1020,14 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
exists v, sem_cast v1 ty1 ty = Some v
| Ecall (Eval vf tyf) rargs ty =>
exprlist_all_values rargs ->
- exists tyargs, exists tyres, exists fd, exists vl,
- classify_fun tyf = fun_case_f tyargs tyres
+ exists tyargs tyres cconv fd vl,
+ classify_fun tyf = fun_case_f tyargs tyres cconv
/\ Genv.find_funct ge vf = Some fd
/\ cast_arguments rargs tyargs vl
- /\ type_of_fundef fd = Tfunction tyargs tyres
+ /\ type_of_fundef fd = Tfunction tyargs tyres cconv
| Ebuiltin ef tyargs rargs ty =>
exprlist_all_values rargs ->
- exists vargs, exists t, exists vres, exists m', exists w',
+ exists vargs t vres m' w',
cast_arguments rargs tyargs vargs
/\ external_call ef ge vargs m t vres m'
/\ possible_trace w t w'
@@ -1069,7 +1069,7 @@ Lemma callred_invert:
invert_expr_prop r m.
Proof.
intros. inv H. simpl.
- intros. exists tyargs; exists tyres; exists fd; exists args; auto.
+ intros. exists tyargs, tyres, cconv, fd, args; auto.
Qed.
Scheme context_ind2 := Minimality for context Sort Prop
@@ -1513,10 +1513,10 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
destruct (is_val_list rargs) as [vtl | ] eqn:?.
rewrite (is_val_inv _ _ _ Heqo). exploit is_val_list_all_values; eauto. intros ALLVAL.
(* top *)
- destruct (classify_fun tyf) as [tyargs tyres|] eqn:?...
+ destruct (classify_fun tyf) as [tyargs tyres cconv|] eqn:?...
destruct (Genv.find_funct ge vf) as [fd|] eqn:?...
destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?...
- destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres))...
+ destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv))...
apply topred_ok; auto. red. split; auto. eapply red_Ecall; eauto.
eapply sem_cast_arguments_sound; eauto.
apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence.
@@ -2049,7 +2049,7 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
let (e,m1) := do_alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) in
do m2 <- sem_bind_parameters w e m1 f.(fn_params) vargs;
ret (State f f.(fn_body) k e m2)
- | Callstate (External ef _ _) vargs k m =>
+ | Callstate (External ef _ _ _) vargs k m =>
match do_external ef w vargs m with
| None => nil
| Some(w',t,v,m') => (t, Returnstate v k m') :: nil
@@ -2215,7 +2215,7 @@ Definition do_initial_state (p: program): option (genv * state) :=
do m0 <- Genv.init_mem p;
do b <- Genv.find_symbol ge p.(prog_main);
do f <- Genv.find_funct_ptr ge b;
- check (type_eq (type_of_fundef f) (Tfunction Tnil type_int32s));
+ check (type_eq (type_of_fundef f) (Tfunction Tnil type_int32s cc_default));
Some (ge, Callstate f nil Kstop m0).
Definition at_final_state (S: state): option int :=
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 137decc..f402ac2 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -132,6 +132,7 @@ Definition Sfor (s1: statement) (e2: expr) (s3: statement) (s4: statement) :=
Record function : Type := mkfunction {
fn_return: type;
+ fn_callconv: calling_convention;
fn_params: list (ident * type);
fn_vars: list (ident * type);
fn_temps: list (ident * type);
@@ -146,17 +147,17 @@ Definition var_names (vars: list(ident * type)) : list ident :=
Inductive fundef : Type :=
| Internal: function -> fundef
- | External: external_function -> typelist -> type -> fundef.
+ | External: external_function -> typelist -> type -> calling_convention -> fundef.
(** The type of a function definition. *)
Definition type_of_function (f: function) : type :=
- Tfunction (type_of_params (fn_params f)) (fn_return f).
+ Tfunction (type_of_params (fn_params f)) (fn_return f) (fn_callconv f).
Definition type_of_fundef (f: fundef) : type :=
match f with
| Internal fd => type_of_function fd
- | External id args res => Tfunction args res
+ | External id args res cc => Tfunction args res cc
end.
(** ** Programs *)
@@ -556,12 +557,12 @@ Inductive step: state -> trace -> state -> Prop :=
step (State f (Sset id a) k e le m)
E0 (State f Sskip k e (PTree.set id v le) m)
- | step_call: forall f optid a al k e le m tyargs tyres vf vargs fd,
- classify_fun (typeof a) = fun_case_f tyargs tyres ->
+ | step_call: forall f optid a al k e le m tyargs tyres cconv vf vargs fd,
+ classify_fun (typeof a) = fun_case_f tyargs tyres cconv ->
eval_expr e le m a vf ->
eval_exprlist e le m al tyargs vargs ->
Genv.find_funct ge vf = Some fd ->
- type_of_fundef fd = Tfunction tyargs tyres ->
+ type_of_fundef fd = Tfunction tyargs tyres cconv ->
step (State f (Scall optid a al) k e le m)
E0 (Callstate fd vargs (Kcall optid f e le k) m)
@@ -649,9 +650,9 @@ Inductive step: state -> trace -> state -> Prop :=
step (Callstate (Internal f) vargs k m)
E0 (State f f.(fn_body) k e le m1)
- | step_external_function: forall ef targs tres vargs k m vres t m',
+ | step_external_function: forall ef targs tres cconv vargs k m vres t m',
external_call ef ge vargs m t vres m' ->
- step (Callstate (External ef targs tres) vargs k m)
+ step (Callstate (External ef targs tres cconv) vargs k m)
t (Returnstate vres k m')
| step_returnstate: forall v optid f e le k m,
@@ -671,7 +672,7 @@ Inductive initial_state (p: program): state -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- type_of_fundef f = Tfunction Tnil type_int32s ->
+ type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
initial_state p (Callstate f nil Kstop m0).
(** A final state is a [Returnstate] with an empty continuation. *)
diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v
index 4d10c62..f7a0e18 100644
--- a/cfrontend/ClightBigstep.v
+++ b/cfrontend/ClightBigstep.v
@@ -89,12 +89,12 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env ->
eval_expr ge e le m a v ->
exec_stmt e le m (Sset id a)
E0 (PTree.set id v le) m Out_normal
- | exec_Scall: forall e le m optid a al tyargs tyres vf vargs f t m' vres,
- classify_fun (typeof a) = fun_case_f tyargs tyres ->
+ | exec_Scall: forall e le m optid a al tyargs tyres cconv vf vargs f t m' vres,
+ classify_fun (typeof a) = fun_case_f tyargs tyres cconv ->
eval_expr ge e le m a vf ->
eval_exprlist ge e le m al tyargs vargs ->
Genv.find_funct ge vf = Some f ->
- type_of_fundef f = Tfunction tyargs tyres ->
+ type_of_fundef f = Tfunction tyargs tyres cconv ->
eval_funcall m f vargs t m' vres ->
exec_stmt e le m (Scall optid a al)
t (set_opttemp optid vres le) m' Out_normal
@@ -170,9 +170,9 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
outcome_result_value out f.(fn_return) vres ->
Mem.free_list m3 (blocks_of_env e) = Some m4 ->
eval_funcall m (Internal f) vargs t m4 vres
- | eval_funcall_external: forall m ef targs tres vargs t vres m',
+ | eval_funcall_external: forall m ef targs tres cconv vargs t vres m',
external_call ef ge vargs m t vres m' ->
- eval_funcall m (External ef targs tres) vargs t m' vres.
+ eval_funcall m (External ef targs tres cconv) vargs t m' vres.
Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop.
@@ -186,12 +186,12 @@ Combined Scheme exec_stmt_funcall_ind from exec_stmt_ind2, eval_funcall_ind2.
trace of observable events performed during the execution. *)
CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Prop :=
- | execinf_Scall: forall e le m optid a al vf tyargs tyres vargs f t,
- classify_fun (typeof a) = fun_case_f tyargs tyres ->
+ | execinf_Scall: forall e le m optid a al vf tyargs tyres cconv vargs f t,
+ classify_fun (typeof a) = fun_case_f tyargs tyres cconv ->
eval_expr ge e le m a vf ->
eval_exprlist ge e le m al tyargs vargs ->
Genv.find_funct ge vf = Some f ->
- type_of_fundef f = Tfunction tyargs tyres ->
+ type_of_fundef f = Tfunction tyargs tyres cconv ->
evalinf_funcall m f vargs t ->
execinf_stmt e le m (Scall optid a al) t
| execinf_Sseq_1: forall e le m s1 s2 t,
@@ -246,7 +246,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- type_of_fundef f = Tfunction Tnil type_int32s ->
+ type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
eval_funcall ge m0 f nil t m1 (Vint r) ->
bigstep_program_terminates p t r.
@@ -256,7 +256,7 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- type_of_fundef f = Tfunction Tnil type_int32s ->
+ type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
evalinf_funcall ge m0 f nil t ->
bigstep_program_diverges p t.
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 31643a9..fec540b 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -92,14 +92,14 @@ Inductive classify_cast_cases : Type :=
Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
match tto, tfrom with
- | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral
+ | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
| Tint IBool _ _, Tfloat _ _ => cast_case_f2bool
- | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_p2bool
+ | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool
| Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2
| Tint sz2 si2 _, Tfloat sz1 _ => cast_case_f2i sz2 si2
| Tfloat sz2 _, Tfloat sz1 _ => cast_case_f2f sz2
| Tfloat sz2 _, Tint sz1 si1 _ => cast_case_i2f si1 sz2
- | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral
+ | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
| Tlong _ _, Tlong _ _ => cast_case_l2l
| Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1
| Tint IBool _ _, Tlong _ _ => cast_case_l2bool
@@ -107,7 +107,7 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
| Tlong si2 _, Tfloat sz1 _ => cast_case_f2l si2
| Tfloat sz2 _, Tlong si1 _ => cast_case_l2f si1 sz2
| (Tpointer _ _ | Tcomp_ptr _ _), Tlong _ _ => cast_case_l2i I32 Unsigned
- | Tlong si2 _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_i2l si2
+ | Tlong si2 _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2
| Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2
| Tunion id2 fld2 _, Tunion id1 fld1 _ => cast_case_union id1 fld1 id2 fld2
| Tvoid, _ => cast_case_void
@@ -326,7 +326,7 @@ Proof.
assert (A: classify_bool t =
match t with
| Tint _ _ _ => bool_case_i
- | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ => bool_case_p
+ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p
| Tfloat _ _ => bool_case_f
| Tlong _ _ => bool_case_l
| _ => bool_default
@@ -833,13 +833,13 @@ Definition sem_cmp (c:comparison)
(** ** Function applications *)
Inductive classify_fun_cases : Type:=
- | fun_case_f (targs: typelist) (tres: type) (**r (pointer to) function *)
+ | fun_case_f (targs: typelist) (tres: type) (cc: calling_convention) (**r (pointer to) function *)
| fun_default.
Definition classify_fun (ty: type) :=
match ty with
- | Tfunction args res => fun_case_f args res
- | Tpointer (Tfunction args res) _ => fun_case_f args res
+ | Tfunction args res cc => fun_case_f args res cc
+ | Tpointer (Tfunction args res cc) _ => fun_case_f args res cc
| _ => fun_default
end.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index be3ee4b..2eedbd8 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -322,11 +322,11 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
(More exactly, identification of function calls that can reduce.) *)
Inductive callred: expr -> fundef -> list val -> type -> Prop :=
- | red_Ecall: forall vf tyf tyargs tyres el ty fd vargs,
+ | red_Ecall: forall vf tyf tyargs tyres cconv el ty fd vargs,
Genv.find_funct ge vf = Some fd ->
cast_arguments el tyargs vargs ->
- type_of_fundef fd = Tfunction tyargs tyres ->
- classify_fun tyf = fun_case_f tyargs tyres ->
+ type_of_fundef fd = Tfunction tyargs tyres cconv ->
+ classify_fun tyf = fun_case_f tyargs tyres cconv ->
callred (Ecall (Eval vf tyf) el ty)
fd vargs ty.
@@ -754,9 +754,9 @@ Inductive sstep: state -> trace -> state -> Prop :=
sstep (Callstate (Internal f) vargs k m)
E0 (State f f.(fn_body) k e m2)
- | step_external_function: forall ef targs tres vargs k m vres t m',
+ | step_external_function: forall ef targs tres cc vargs k m vres t m',
external_call ef ge vargs m t vres m' ->
- sstep (Callstate (External ef targs tres) vargs k m)
+ sstep (Callstate (External ef targs tres cc) vargs k m)
t (Returnstate vres k m')
| step_returnstate: forall v f e C ty k m,
@@ -781,7 +781,7 @@ Inductive initial_state (p: program): state -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- type_of_fundef f = Tfunction Tnil type_int32s ->
+ type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
initial_state p (Callstate f nil Kstop m0).
(** A final state is a [Returnstate] with an empty continuation. *)
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 6ae33a6..4b2e915 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -475,7 +475,7 @@ Inductive initial_state (p: program): state -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- funsig f = mksignature nil (Some Tint) ->
+ funsig f = signature_main ->
initial_state p (Callstate f nil Kstop m0).
(** A final state is a [Returnstate] with an empty continuation. *)
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 0ed008f..1380695 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -443,10 +443,28 @@ Fixpoint transl_arglist (al: list Clight.expr) (tyl: typelist)
do ta1' <- make_cast (typeof a1) ty1 ta1;
do ta2 <- transl_arglist a2 ty2;
OK (ta1' :: ta2)
+ | a1 :: a2, Tnil =>
+ (* Tolerance for calls to K&R or variadic functions *)
+ do ta1 <- transl_expr a1;
+ do ta2 <- transl_arglist a2 Tnil;
+ OK (ta1 :: ta2)
| _, _ =>
Error(msg "Cshmgen.transl_arglist: arity mismatch")
end.
+(** Compute the argument signature that corresponds to a function application. *)
+
+Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: typelist)
+ {struct al}: list AST.typ :=
+ match al, tyl with
+ | nil, _ => nil
+ | a1 :: a2, Tcons ty1 ty2 =>
+ typ_of_type ty1 :: typlist_of_arglist a2 ty2
+ | a1 :: a2, Tnil =>
+ (* Tolerance for calls to K&R or variadic functions *)
+ typ_of_type_default (typeof a1) :: typlist_of_arglist a2 Tnil
+ end.
+
(** * Translation of statements *)
(** [transl_statement nbrk ncnt s] returns a Csharpminor statement
@@ -487,10 +505,13 @@ Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat)
OK(Sset x tb)
| Clight.Scall x b cl =>
match classify_fun (typeof b) with
- | fun_case_f args res =>
+ | fun_case_f args res cconv =>
do tb <- transl_expr b;
do tcl <- transl_arglist cl args;
- OK(Scall x (signature_of_type args res) tb tcl)
+ OK(Scall x {| sig_args := typlist_of_arglist cl args;
+ sig_res := opttyp_of_type res;
+ sig_cc := cconv |}
+ tb tcl)
| _ => Error(msg "Cshmgen.transl_stmt(call)")
end
| Clight.Sbuiltin x ef tyargs bl =>
@@ -547,8 +568,9 @@ with transl_lbl_stmt (tyret: type) (nbrk ncnt: nat)
Definition transl_var (v: ident * type) := (fst v, sizeof (snd v)).
Definition signature_of_function (f: Clight.function) :=
- mksignature (map typ_of_type (map snd (Clight.fn_params f)))
- (opttyp_of_type (Clight.fn_return f)).
+ {| sig_args := map typ_of_type (map snd (Clight.fn_params f));
+ sig_res := opttyp_of_type (Clight.fn_return f);
+ sig_cc := Clight.fn_callconv f |}.
Definition transl_function (f: Clight.function) : res function :=
do tbody <- transl_statement f.(Clight.fn_return) 1%nat 0%nat (Clight.fn_body f);
@@ -563,9 +585,8 @@ Definition transl_fundef (f: Clight.fundef) : res fundef :=
match f with
| Clight.Internal g =>
do tg <- transl_function g; OK(AST.Internal tg)
- | Clight.External ef args res =>
- if list_typ_eq (sig_args (ef_sig ef)) (typlist_of_typelist args)
- && opt_typ_eq (sig_res (ef_sig ef)) (opttyp_of_type res)
+ | Clight.External ef args res cconv =>
+ if signature_eq (ef_sig ef) (signature_of_type args res cconv)
then OK(AST.External ef)
else Error(msg "Cshmgen.transl_fundef: wrong external signature")
end.
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 220d907..d6e881e 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -40,28 +40,24 @@ Proof.
Qed.
Lemma transl_fundef_sig1:
- forall f tf args res,
+ forall f tf args res cc,
transl_fundef f = OK tf ->
- classify_fun (type_of_fundef f) = fun_case_f args res ->
- funsig tf = signature_of_type args res.
+ classify_fun (type_of_fundef f) = fun_case_f args res cc ->
+ funsig tf = signature_of_type args res cc.
Proof.
intros. destruct f; simpl in *.
monadInv H. monadInv EQ. simpl. inversion H0.
unfold signature_of_function, signature_of_type.
f_equal. apply transl_params_types.
- destruct (list_typ_eq (sig_args (ef_sig e)) (typlist_of_typelist t)); simpl in H.
- destruct (opt_typ_eq (sig_res (ef_sig e)) (opttyp_of_type t0)); simpl in H.
- inv H. simpl. destruct (ef_sig e); simpl in *. inv H0.
- unfold signature_of_type. auto.
- congruence.
- congruence.
+ destruct (signature_eq (ef_sig e) (signature_of_type t t0 c)); inv H.
+ simpl. congruence.
Qed.
Lemma transl_fundef_sig2:
- forall f tf args res,
+ forall f tf args res cc,
transl_fundef f = OK tf ->
- type_of_fundef f = Tfunction args res ->
- funsig tf = signature_of_type args res.
+ type_of_fundef f = Tfunction args res cc ->
+ funsig tf = signature_of_type args res cc.
Proof.
intros. eapply transl_fundef_sig1; eauto.
rewrite H0; reflexivity.
@@ -982,6 +978,16 @@ Proof.
eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. auto.
Qed.
+Lemma typlist_of_arglist_eq:
+ forall al tyl vl,
+ Clight.eval_exprlist ge e le m al tyl vl ->
+ typlist_of_arglist al tyl = typlist_of_typelist tyl.
+Proof.
+ induction 1; simpl.
+ auto.
+ f_equal; auto.
+Qed.
+
End EXPR.
(** ** Semantic preservation for statements *)
@@ -1064,11 +1070,11 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop :=
match_states (Clight.State f s k e le m)
(State tf ts' tk' te le m)
| match_callstate:
- forall fd args k m tfd tk targs tres
+ forall fd args k m tfd tk targs tres cconv
(TR: transl_fundef fd = OK tfd)
(MK: match_cont Tvoid 0%nat 0%nat k tk)
(ISCC: Clight.is_call_cont k)
- (TY: type_of_fundef fd = Tfunction targs tres),
+ (TY: type_of_fundef fd = Tfunction targs tres cconv),
match_states (Clight.Callstate fd args k m)
(Callstate tfd args tk m)
| match_returnstate:
@@ -1232,13 +1238,14 @@ Proof.
(* call *)
revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence.
- intros targs tres CF TR. monadInv TR. inv MTR.
+ intros targs tres cc CF TR. monadInv TR. inv MTR.
exploit functions_translated; eauto. intros [tfd [FIND TFD]].
rewrite H in CF. simpl in CF. inv CF.
econstructor; split.
apply plus_one. econstructor; eauto.
exploit transl_expr_correct; eauto.
exploit transl_arglist_correct; eauto.
+ erewrite typlist_of_arglist_eq by eauto.
eapply transl_fundef_sig1; eauto.
rewrite H3. auto.
econstructor; eauto.
@@ -1422,9 +1429,7 @@ Proof.
(* external function *)
simpl in TR.
- destruct (list_typ_eq (sig_args (ef_sig ef)) (typlist_of_typelist targs) &&
- opt_typ_eq (sig_res (ef_sig ef)) (opttyp_of_type tres));
- monadInv TR.
+ destruct (signature_eq (ef_sig ef) (signature_of_type targs tres cconv)); inv TR.
exploit match_cont_is_call_cont; eauto. intros [A B].
econstructor; split.
apply plus_one. constructor. eauto.
@@ -1451,7 +1456,7 @@ Proof.
rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog).
auto. symmetry. unfold transl_program in TRANSL.
eapply transform_partial_program2_main; eauto.
- assert (funsig tf = signature_of_type Tnil type_int32s).
+ assert (funsig tf = signature_of_type Tnil type_int32s cc_default).
eapply transl_fundef_sig2; eauto.
econstructor; split.
econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto.
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 7988dfa..b1fbebe 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -359,13 +359,13 @@ Inductive estep: state -> trace -> state -> Prop :=
estep (ExprState f (C (Eparen r ty)) k e m)
E0 (ExprState f (C (Eval v ty)) k e m)
- | step_call: forall f C rf rargs ty k e m targs tres vf vargs fd,
+ | step_call: forall f C rf rargs ty k e m targs tres cconv vf vargs fd,
leftcontext RV RV C ->
- classify_fun (typeof rf) = fun_case_f targs tres ->
+ classify_fun (typeof rf) = fun_case_f targs tres cconv ->
eval_simple_rvalue e m rf vf ->
eval_simple_list e m rargs targs vargs ->
Genv.find_funct ge vf = Some fd ->
- type_of_fundef fd = Tfunction targs tres ->
+ type_of_fundef fd = Tfunction targs tres cconv ->
estep (ExprState f (C (Ecall rf rargs ty)) k e m)
E0 (Callstate fd vargs (Kcall f e C ty k) m)
@@ -562,11 +562,11 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
exists v, sem_cast v1 ty1 ty = Some v
| Ecall (Eval vf tyf) rargs ty =>
exprlist_all_values rargs ->
- exists tyargs, exists tyres, exists fd, exists vl,
- classify_fun tyf = fun_case_f tyargs tyres
+ exists tyargs tyres cconv fd vl,
+ classify_fun tyf = fun_case_f tyargs tyres cconv
/\ Genv.find_funct ge vf = Some fd
/\ cast_arguments rargs tyargs vl
- /\ type_of_fundef fd = Tfunction tyargs tyres
+ /\ type_of_fundef fd = Tfunction tyargs tyres cconv
| Ebuiltin ef tyargs rargs ty =>
exprlist_all_values rargs ->
exists vargs, exists t, exists vres, exists m',
@@ -610,7 +610,7 @@ Lemma callred_invert:
invert_expr_prop r m.
Proof.
intros. inv H. simpl.
- intros. exists tyargs; exists tyres; exists fd; exists args; auto.
+ intros. exists tyargs, tyres, cconv, fd, args; auto.
Qed.
Scheme context_ind2 := Minimality for context Sort Prop
@@ -1369,7 +1369,7 @@ Proof.
eapply safe_steps. eexact S1.
apply (eval_simple_list_steps f k e m rargs vl E2 C'); auto.
simpl. intros X. exploit X. eapply rval_list_all_values.
- intros [tyargs [tyres [fd [vargs [P [Q [U V]]]]]]].
+ intros [tyargs [tyres [cconv [fd [vargs [P [Q [U V]]]]]]]].
econstructor; econstructor; eapply step_call; eauto. eapply can_eval_simple_list; eauto.
(* builtin *)
pose (C' := fun x => C(Ebuiltin ef tyargs x ty)).
@@ -1756,13 +1756,13 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
ty = typeof r2 ->
eval_expr e m RV (Ecomma r1 r2 ty) (t1**t2) m2 r2'
| eval_call: forall e m rf rargs ty t1 m1 rf' t2 m2 rargs' vf vargs
- targs tres fd t3 m3 vres,
+ targs tres cconv fd t3 m3 vres,
eval_expr e m RV rf t1 m1 rf' -> eval_exprlist e m1 rargs t2 m2 rargs' ->
eval_simple_rvalue ge e m2 rf' vf ->
eval_simple_list ge e m2 rargs' targs vargs ->
- classify_fun (typeof rf) = fun_case_f targs tres ->
+ classify_fun (typeof rf) = fun_case_f targs tres cconv ->
Genv.find_funct ge vf = Some fd ->
- type_of_fundef fd = Tfunction targs tres ->
+ type_of_fundef fd = Tfunction targs tres cconv ->
eval_funcall m2 fd vargs t3 m3 vres ->
eval_expr e m RV (Ecall rf rargs ty) (t1**t2**t3) m3 (Eval vres ty)
@@ -1901,9 +1901,9 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
outcome_result_value out f.(fn_return) vres ->
Mem.free_list m3 (blocks_of_env e) = Some m4 ->
eval_funcall m (Internal f) vargs t m4 vres
- | eval_funcall_external: forall m ef targs tres vargs t vres m',
+ | eval_funcall_external: forall m ef targs tres cconv vargs t vres m',
external_call ef ge vargs m t vres m' ->
- eval_funcall m (External ef targs tres) vargs t m' vres.
+ eval_funcall m (External ef targs tres cconv) vargs t m' vres.
Scheme eval_expression_ind5 := Minimality for eval_expression Sort Prop
with eval_expr_ind5 := Minimality for eval_expr Sort Prop
@@ -1999,13 +1999,13 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop :=
evalinf_exprlist e m1 a2 t2 ->
evalinf_expr e m RV (Ecall a1 a2 ty) (t1 *** t2)
| evalinf_call: forall e m rf rargs ty t1 m1 rf' t2 m2 rargs' vf vargs
- targs tres fd t3,
+ targs tres cconv fd t3,
eval_expr e m RV rf t1 m1 rf' -> eval_exprlist e m1 rargs t2 m2 rargs' ->
eval_simple_rvalue ge e m2 rf' vf ->
eval_simple_list ge e m2 rargs' targs vargs ->
- classify_fun (typeof rf) = fun_case_f targs tres ->
+ classify_fun (typeof rf) = fun_case_f targs tres cconv ->
Genv.find_funct ge vf = Some fd ->
- type_of_fundef fd = Tfunction targs tres ->
+ type_of_fundef fd = Tfunction targs tres cconv ->
evalinf_funcall m2 fd vargs t3 ->
evalinf_expr e m RV (Ecall rf rargs ty) (t1***t2***t3)
@@ -3034,7 +3034,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- type_of_fundef f = Tfunction Tnil type_int32s ->
+ type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
eval_funcall ge m0 f nil t m1 (Vint r) ->
bigstep_program_terminates p t r.
@@ -3044,7 +3044,7 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- type_of_fundef f = Tfunction Tnil type_int32s ->
+ type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
evalinf_funcall ge m0 f nil t ->
bigstep_program_diverges p t.
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 8b98556..ea1bd86 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -177,6 +177,7 @@ with labeled_statements : Type := (**r cases of a [switch] *)
Record function : Type := mkfunction {
fn_return: type;
+ fn_callconv: calling_convention;
fn_params: list (ident * type);
fn_vars: list (ident * type);
fn_body: statement
@@ -190,17 +191,17 @@ Definition var_names (vars: list(ident * type)) : list ident :=
Inductive fundef : Type :=
| Internal: function -> fundef
- | External: external_function -> typelist -> type -> fundef.
+ | External: external_function -> typelist -> type -> calling_convention -> fundef.
(** The type of a function definition. *)
Definition type_of_function (f: function) : type :=
- Tfunction (type_of_params (fn_params f)) (fn_return f).
+ Tfunction (type_of_params (fn_params f)) (fn_return f) (fn_callconv f).
Definition type_of_fundef (f: fundef) : type :=
match f with
| Internal fd => type_of_function fd
- | External id args res => Tfunction args res
+ | External id args res cc => Tfunction args res cc
end.
(** ** Programs *)
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index c9ef996..2b409ab 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -97,7 +97,7 @@ Inductive type : Type :=
| Tfloat: floatsize -> attr -> type (**r floating-point types *)
| Tpointer: type -> attr -> type (**r pointer types ([*ty]) *)
| Tarray: type -> Z -> attr -> type (**r array types ([ty[len]]) *)
- | Tfunction: typelist -> type -> type (**r function types *)
+ | Tfunction: typelist -> type -> calling_convention -> type (**r function types *)
| Tstruct: ident -> fieldlist -> attr -> type (**r struct types *)
| Tunion: ident -> fieldlist -> attr -> type (**r union types *)
| Tcomp_ptr: ident -> attr -> type (**r pointer to named struct or union *)
@@ -119,11 +119,11 @@ Proof.
assert (forall (x y: floatsize), {x=y} + {x<>y}) by decide equality.
assert (forall (x y: attr), {x=y} + {x<>y}).
{ decide equality. decide equality. apply N.eq_dec. apply bool_dec. }
- generalize ident_eq zeq. intros E1 E2.
+ generalize ident_eq zeq bool_dec. intros E1 E2 E3.
decide equality.
decide equality.
- generalize ident_eq. intros E1.
decide equality.
+ generalize ident_eq. intros E1. decide equality.
Defined.
Opaque type_eq typelist_eq fieldlist_eq.
@@ -138,7 +138,7 @@ Definition attr_of_type (ty: type) :=
| Tfloat sz a => a
| Tpointer elt a => a
| Tarray elt sz a => a
- | Tfunction args res => noattr
+ | Tfunction args res cc => noattr
| Tstruct id fld a => a
| Tunion id fld a => a
| Tcomp_ptr id a => a
@@ -154,7 +154,7 @@ Definition typeconv (ty: type) : type :=
match ty with
| Tint (I8 | I16 | IBool) _ a => Tint I32 Signed a
| Tarray t sz a => Tpointer t a
- | Tfunction _ _ => Tpointer ty noattr
+ | Tfunction _ _ _ => Tpointer ty noattr
| _ => ty
end.
@@ -177,7 +177,7 @@ Fixpoint alignof (t: type) : Z :=
| Tfloat F64 _ => 8
| Tpointer _ _ => 4
| Tarray t' _ _ => alignof t'
- | Tfunction _ _ => 1
+ | Tfunction _ _ _ => 1
| Tstruct _ fld _ => alignof_fields fld
| Tunion _ fld _ => alignof_fields fld
| Tcomp_ptr _ _ => 4
@@ -252,7 +252,7 @@ Fixpoint sizeof (t: type) : Z :=
| Tfloat F64 _ => 8
| Tpointer _ _ => 4
| Tarray t' n _ => sizeof t' * Zmax 1 n
- | Tfunction _ _ => 1
+ | Tfunction _ _ _ => 1
| Tstruct _ fld _ => align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
| Tunion _ fld _ => align (Zmax 1 (sizeof_union fld)) (alignof t)
| Tcomp_ptr _ _ => 4
@@ -302,7 +302,7 @@ Fixpoint naturally_aligned (t: type) : Prop :=
attr_alignas a = None
| Tarray t' _ a =>
attr_alignas a = None /\ naturally_aligned t'
- | Tvoid | Tfunction _ _ | Tstruct _ _ _ | Tunion _ _ _ =>
+ | Tvoid | Tfunction _ _ _ | Tstruct _ _ _ | Tunion _ _ _ =>
True
end.
@@ -478,7 +478,7 @@ Definition access_mode (ty: type) : mode :=
| Tvoid => By_nothing
| Tpointer _ _ => By_value Mint32
| Tarray _ _ _ => By_reference
- | Tfunction _ _ => By_reference
+ | Tfunction _ _ _ => By_reference
| Tstruct _ _ _ => By_copy
| Tunion _ _ _ => By_copy
| Tcomp_ptr _ _ => By_nothing
@@ -510,7 +510,7 @@ Fixpoint unroll_composite (ty: type) : type :=
| Tfloat _ _ => ty
| Tpointer t1 a => Tpointer (unroll_composite t1) a
| Tarray t1 sz a => Tarray (unroll_composite t1) sz a
- | Tfunction t1 t2 => Tfunction (unroll_composite_list t1) (unroll_composite t2)
+ | Tfunction t1 t2 a => Tfunction (unroll_composite_list t1) (unroll_composite t2) a
| Tstruct id fld a => if ident_eq id cid then ty else Tstruct id (unroll_composite_fields fld) a
| Tunion id fld a => if ident_eq id cid then ty else Tunion id (unroll_composite_fields fld) a
| Tcomp_ptr id a => if ident_eq id cid then Tpointer comp a else ty
@@ -586,7 +586,7 @@ Fixpoint alignof_blockcopy (t: type) : Z :=
| Tfloat F64 _ => 8
| Tpointer _ _ => 4
| Tarray t' _ _ => alignof_blockcopy t'
- | Tfunction _ _ => 1
+ | Tfunction _ _ _ => 1
| Tstruct _ fld _ => Zmin 8 (alignof t)
| Tunion _ fld _ => Zmin 8 (alignof t)
| Tcomp_ptr _ _ => 4
@@ -681,5 +681,15 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
| Tcons hd tl => typ_of_type hd :: typlist_of_typelist tl
end.
-Definition signature_of_type (args: typelist) (res: type) : signature :=
- mksignature (typlist_of_typelist args) (opttyp_of_type res).
+Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature :=
+ mksignature (typlist_of_typelist args) (opttyp_of_type res) cc.
+
+(** Like [typ_of_type], but apply default argument promotion. *)
+
+Definition typ_of_type_default (t: type) : AST.typ :=
+ match t with
+ | Tfloat _ _ => AST.Tfloat
+ | Tlong _ _ => AST.Tlong
+ | _ => AST.Tint
+ end.
+
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 5db4718..b6fc728 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -680,7 +680,7 @@ Qed.
(** A semantics for general initializers *)
-Definition dummy_function := mkfunction Tvoid nil nil Sskip.
+Definition dummy_function := mkfunction Tvoid cc_default nil nil Sskip.
Fixpoint fields_of_struct (id: ident) (ty: type) (fl: fieldlist) (pos: Z) : list (Z * type) :=
match fl with
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 78ab7fc..376707a 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -229,7 +229,7 @@ and print_stmt_for p s =
let print_function p id f =
fprintf p "%s@ "
(name_cdecl (name_function_parameters (extern_atom id)
- f.fn_params)
+ f.fn_params f.fn_callconv)
f.fn_return);
fprintf p "@[<v 2>{@ ";
List.iter
@@ -245,10 +245,10 @@ let print_function p id f =
let print_fundef p id fd =
match fd with
- | External(EF_external(_,_), args, res) ->
+ | External(EF_external(_,_), args, res, cconv) ->
fprintf p "extern %s;@ @ "
- (name_cdecl (extern_atom id) (Tfunction(args, res)))
- | External(_, _, _) ->
+ (name_cdecl (extern_atom id) (Tfunction(args, res, cconv)))
+ | External(_, _, _, _) ->
()
| Internal f ->
print_function p id f
@@ -309,7 +309,7 @@ let collect_function f =
let collect_globdef (id, gd) =
match gd with
- | Gfun(External(_, args, res)) -> collect_type_list args; collect_type res
+ | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res
| Gfun(Internal f) -> collect_function f
| Gvar v -> collect_type v.gvar_info
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 4db8976..758323e 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -88,11 +88,6 @@ let attributes a =
let name_optid id =
if id = "" then "" else " " ^ id
-(*
-let parenthesize_if_pointer id =
- if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
-*)
-
let rec name_cdecl id ty =
match ty with
| Tvoid ->
@@ -111,24 +106,26 @@ let rec name_cdecl id ty =
name_cdecl id' t
| Tarray(t, n, a) ->
name_cdecl (sprintf "%s[%ld]" id (camlint_of_coqint n)) t
- | Tfunction(args, res) ->
+ | Tfunction(args, res, cconv) ->
let b = Buffer.create 20 in
if id = ""
then Buffer.add_string b "(*)"
else Buffer.add_string b id;
Buffer.add_char b '(';
- begin match args with
+ let rec add_args first = function
| Tnil ->
- Buffer.add_string b "void"
- | _ ->
- let rec add_args first = function
- | Tnil -> ()
- | Tcons(t1, tl) ->
- if not first then Buffer.add_string b ", ";
- Buffer.add_string b (name_cdecl "" t1);
- add_args false tl in
- add_args true args
- end;
+ if first then
+ Buffer.add_string b
+ (if cconv.cc_vararg then "..." else "void")
+ else if cconv.cc_vararg then
+ Buffer.add_string b ", ..."
+ else
+ ()
+ | Tcons(t1, tl) ->
+ if not first then Buffer.add_string b ", ";
+ Buffer.add_string b (name_cdecl "" t1);
+ add_args false tl in
+ add_args true args;
Buffer.add_char b ')';
name_cdecl (Buffer.contents b) res
| Tstruct(name, fld, a) ->
@@ -351,16 +348,17 @@ and print_stmt_for p s =
| _ ->
fprintf p "({ %a })" print_stmt s
-let name_function_parameters fun_name params =
+let name_function_parameters fun_name params cconv =
let b = Buffer.create 20 in
Buffer.add_string b fun_name;
Buffer.add_char b '(';
begin match params with
| [] ->
- Buffer.add_string b "void"
+ Buffer.add_string b (if cconv.cc_vararg then "..." else "void")
| _ ->
let rec add_params first = function
- | [] -> ()
+ | [] ->
+ if cconv.cc_vararg then Buffer.add_string b "..."
| (id, ty) :: rem ->
if not first then Buffer.add_string b ", ";
Buffer.add_string b (name_cdecl (extern_atom id) ty);
@@ -373,7 +371,7 @@ let name_function_parameters fun_name params =
let print_function p id f =
fprintf p "%s@ "
(name_cdecl (name_function_parameters (extern_atom id)
- f.fn_params)
+ f.fn_params f.fn_callconv)
f.fn_return);
fprintf p "@[<v 2>{@ ";
List.iter
@@ -385,10 +383,10 @@ let print_function p id f =
let print_fundef p id fd =
match fd with
- | External(EF_external(_,_), args, res) ->
+ | External(EF_external(_,_), args, res, cconv) ->
fprintf p "extern %s;@ @ "
- (name_cdecl (extern_atom id) (Tfunction(args, res)))
- | External(_, _, _) ->
+ (name_cdecl (extern_atom id) (Tfunction(args, res, cconv)))
+ | External(_, _, _, _) ->
()
| Internal f ->
print_function p id f
@@ -474,7 +472,7 @@ let rec collect_type = function
| Tlong _ -> ()
| Tpointer(t, _) -> collect_type t
| Tarray(t, _, _) -> collect_type t
- | Tfunction(args, res) -> collect_type_list args; collect_type res
+ | Tfunction(args, res, _) -> collect_type_list args; collect_type res
| Tstruct(id, fld, _) | Tunion(id, fld, _) ->
let s = extern_atom id in
if not (StructUnion.mem s !struct_unions) then begin
@@ -552,7 +550,7 @@ let collect_function f =
let collect_globdef (id, gd) =
match gd with
- | Gfun(External(_, args, res)) -> collect_type_list args; collect_type res
+ | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res
| Gfun(Internal f) -> collect_function f
| Gvar v -> collect_type v.gvar_info
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 1ead0ae..01f304e 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -504,6 +504,7 @@ Definition transl_function (f: Csyntax.function) : mon function :=
do temps <- get_trail;
ret (mkfunction
f.(Csyntax.fn_return)
+ f.(Csyntax.fn_callconv)
f.(Csyntax.fn_params)
f.(Csyntax.fn_vars)
temps
@@ -513,8 +514,8 @@ Definition transl_fundef (fd: Csyntax.fundef) : mon fundef :=
match fd with
| Csyntax.Internal f =>
do tf <- transl_function f; ret (Internal tf)
- | Csyntax.External ef targs tres =>
- ret (External ef targs tres)
+ | Csyntax.External ef targs tres cconv =>
+ ret (External ef targs tres cconv)
end.
Local Open Scope error_monad_scope.
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index b3c861e..9134e11 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -2166,9 +2166,9 @@ Proof.
inv H7. inversion H3; subst.
econstructor; split.
left; apply plus_one. eapply step_internal_function. econstructor.
- rewrite H5; rewrite H6; auto.
- rewrite H5; rewrite H6. eapply alloc_variables_preserved; eauto.
- rewrite H5. eapply bind_parameters_preserved; eauto.
+ rewrite H6; rewrite H7; auto.
+ rewrite H6; rewrite H7. eapply alloc_variables_preserved; eauto.
+ rewrite H6. eapply bind_parameters_preserved; eauto.
eauto.
constructor; auto.
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 9dfa42e..3dae7ab 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -1090,6 +1090,7 @@ Inductive tr_function: Csyntax.function -> Clight.function -> Prop :=
| tr_function_intro: forall f tf,
tr_stmt f.(Csyntax.fn_body) tf.(fn_body) ->
fn_return tf = Csyntax.fn_return f ->
+ fn_callconv tf = Csyntax.fn_callconv f ->
fn_params tf = Csyntax.fn_params f ->
fn_vars tf = Csyntax.fn_vars f ->
tr_function f tf.
@@ -1098,8 +1099,8 @@ Inductive tr_fundef: Csyntax.fundef -> Clight.fundef -> Prop :=
| tr_internal: forall f tf,
tr_function f tf ->
tr_fundef (Csyntax.Internal f) (Clight.Internal tf)
- | tr_external: forall ef targs tres,
- tr_fundef (Csyntax.External ef targs tres) (External ef targs tres).
+ | tr_external: forall ef targs tres cconv,
+ tr_fundef (Csyntax.External ef targs tres cconv) (External ef targs tres cconv).
Lemma transl_function_spec:
forall f tf g g' i,
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index 95ff9ed..2956508 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -229,6 +229,7 @@ Definition transf_function (f: function) : res function :=
assertion (list_disjoint_dec ident_eq (var_names f.(fn_params)) (var_names f.(fn_temps)));
do body' <- simpl_stmt cenv f.(fn_body);
OK {| fn_return := f.(fn_return);
+ fn_callconv := f.(fn_callconv);
fn_params := f.(fn_params);
fn_vars := remove_lifted cenv (f.(fn_params) ++ f.(fn_vars));
fn_temps := add_lifted cenv f.(fn_vars) f.(fn_temps);
@@ -239,7 +240,7 @@ Definition transf_function (f: function) : res function :=
Definition transf_fundef (fd: fundef) : res fundef :=
match fd with
| Internal f => do tf <- transf_function f; OK (Internal tf)
- | External ef targs tres => OK (External ef targs tres)
+ | External ef targs tres cconv => OK (External ef targs tres cconv)
end.
Definition transf_program (p: program) : res program :=
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 552c991..ae98130 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -1710,12 +1710,12 @@ Inductive match_states: state -> state -> Prop :=
match_states (State f s k e le m)
(State tf ts tk te tle tm)
| match_call_state:
- forall fd vargs k m tfd tvargs tk tm j targs tres
+ forall fd vargs k m tfd tvargs tk tm j targs tres cconv
(TRFD: transf_fundef fd = OK tfd)
(MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm))
(MINJ: Mem.inject j m tm)
(AINJ: val_list_inject j vargs tvargs)
- (FUNTY: type_of_fundef fd = Tfunction targs tres)
+ (FUNTY: type_of_fundef fd = Tfunction targs tres cconv)
(ANORM: val_casted_list vargs targs),
match_states (Callstate fd vargs k m)
(Callstate tfd tvargs tk tm)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 03:45:59 +0000