From a15858a0a8fcea82db02fe8c9bd2ed912210419f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 18 Aug 2010 09:06:55 +0000 Subject: Merge of branches/full-expr-4: - Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Ctyping.v | 459 ---------------------------------------------------- 1 file changed, 459 deletions(-) delete mode 100644 cfrontend/Ctyping.v (limited to 'cfrontend/Ctyping.v') diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v deleted file mode 100644 index 8e089f16..00000000 --- a/cfrontend/Ctyping.v +++ /dev/null @@ -1,459 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** * Typing constraints on C programs *) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Csyntax. - -(** ** Typing rules *) - -(** We now define a simple, incomplete type system for the Clight language. - This ``type system'' is very coarse: we check only the typing properties - that matter for the translation to be correct. Essentially, - we need to check that the types attached to variable references - match the declaration types for those variables. *) - -(** A typing environment maps variable names to their types. *) - -Definition typenv := PTree.t type. - -Section TYPING. - -Variable env: typenv. - -Inductive wt_expr: expr -> Prop := - | wt_Econst_int: forall i ty, - wt_expr (Expr (Econst_int i) ty) - | wt_Econst_float: forall f ty, - wt_expr (Expr (Econst_float f) ty) - | wt_Evar: forall id ty, - env!id = Some ty -> - wt_expr (Expr (Evar id) ty) - | wt_Ederef: forall e ty, - wt_expr e -> - wt_expr (Expr (Ederef e) ty) - | wt_Eaddrof: forall e ty, - wt_expr e -> - wt_expr (Expr (Eaddrof e) ty) - | wt_Eunop: forall op e ty, - wt_expr e -> - wt_expr (Expr (Eunop op e) ty) - | wt_Ebinop: forall op e1 e2 ty, - wt_expr e1 -> wt_expr e2 -> - wt_expr (Expr (Ebinop op e1 e2) ty) - | wt_Ecast: forall e ty ty', - wt_expr e -> - wt_expr (Expr (Ecast ty' e) ty) - | wt_Econdition: forall e1 e2 e3 ty, - wt_expr e1 -> wt_expr e2 -> wt_expr e3 -> - wt_expr (Expr (Econdition e1 e2 e3) ty) - | wt_Eandbool: forall e1 e2 ty, - wt_expr e1 -> wt_expr e2 -> - wt_expr (Expr (Eandbool e1 e2) ty) - | wt_Eorbool: forall e1 e2 ty, - wt_expr e1 -> wt_expr e2 -> - wt_expr (Expr (Eorbool e1 e2) ty) - | wt_Esizeof: forall ty' ty, - wt_expr (Expr (Esizeof ty') ty) - | wt_Efield: forall e id ty, - wt_expr e -> - wt_expr (Expr (Efield e id) ty). - -Inductive wt_optexpr: option expr -> Prop := - | wt_Enone: - wt_optexpr None - | wt_Esome: forall e, - wt_expr e -> - wt_optexpr (Some e). - -Inductive wt_exprlist: list expr -> Prop := - | wt_Enil: - wt_exprlist nil - | wt_Econs: forall e el, - wt_expr e -> wt_exprlist el -> wt_exprlist (e :: el). - -Inductive wt_stmt: statement -> Prop := - | wt_Sskip: - wt_stmt Sskip - | wt_Sassign: forall e1 e2, - wt_expr e1 -> wt_expr e2 -> - wt_stmt (Sassign e1 e2) - | wt_Scall: forall lhs e1 el, - wt_optexpr lhs -> - wt_expr e1 -> - wt_exprlist el -> - wt_stmt (Scall lhs e1 el) - | wt_Ssequence: forall s1 s2, - wt_stmt s1 -> wt_stmt s2 -> - wt_stmt (Ssequence s1 s2) - | wt_Sifthenelse: forall e s1 s2, - wt_expr e -> wt_stmt s1 -> wt_stmt s2 -> - wt_stmt (Sifthenelse e s1 s2) - | wt_Swhile: forall e s, - wt_expr e -> wt_stmt s -> - wt_stmt (Swhile e s) - | wt_Sdowhile: forall e s, - wt_expr e -> wt_stmt s -> - wt_stmt (Sdowhile e s) - | wt_Sfor: forall e s1 s2 s3, - wt_expr e -> wt_stmt s1 -> wt_stmt s2 -> wt_stmt s3 -> - wt_stmt (Sfor s1 e s2 s3) - | wt_Sbreak: - wt_stmt Sbreak - | wt_Scontinue: - wt_stmt Scontinue - | wt_Sreturn: forall opte, - wt_optexpr opte -> - wt_stmt (Sreturn opte) - | wt_Sswitch: forall e sl, - wt_expr e -> wt_lblstmts sl -> - wt_stmt (Sswitch e sl) - | wt_Slabel: forall lbl s, - wt_stmt s -> - wt_stmt (Slabel lbl s) - | wt_Sgoto: forall lbl, - wt_stmt (Sgoto lbl) - -with wt_lblstmts: labeled_statements -> Prop := - | wt_LSdefault: forall s, - wt_stmt s -> - wt_lblstmts (LSdefault s) - | wt_LScase: forall n s sl, - wt_stmt s -> wt_lblstmts sl -> - wt_lblstmts (LScase n s sl). - -End TYPING. - -Definition add_var (env: typenv) (id_ty: ident * type) : typenv := - PTree.set (fst id_ty) (snd id_ty) env. - -Definition add_vars (env: typenv) (vars: list(ident * type)) : typenv := - List.fold_left add_var vars env. - -Definition var_names (vars: list(ident * type)) : list ident := - List.map (@fst ident type) vars. - -Inductive wt_function: typenv -> function -> Prop := - | wt_function_intro: forall env f, - list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> - wt_stmt (add_vars env (f.(fn_params) ++ f.(fn_vars))) f.(fn_body) -> - wt_function env f. - -Inductive wt_fundef: typenv -> fundef -> Prop := - | wt_fundef_Internal: forall env f, - wt_function env f -> - wt_fundef env (Internal f) - | wt_fundef_External: forall env ef args res, - (ef_sig ef).(sig_args) = typlist_of_typelist args -> - (ef_sig ef).(sig_res) = opttyp_of_type res -> - wt_fundef env (External ef args res). - -Definition add_global_var - (env: typenv) (id_v: ident * globvar type) : typenv := - PTree.set (fst id_v) (gvar_info (snd id_v)) env. - -Definition add_global_vars - (env: typenv) (vars: list(ident * globvar type)) : typenv := - List.fold_left add_global_var vars env. - -Definition add_global_fun - (env: typenv) (id_fd: ident * fundef) : typenv := - PTree.set (fst id_fd) (type_of_fundef (snd id_fd)) env. - -Definition add_global_funs - (env: typenv) (funs: list(ident * fundef)) : typenv := - List.fold_left add_global_fun funs env. - -Definition global_typenv (p: program) := - add_global_vars (add_global_funs (PTree.empty type) p.(prog_funct)) p.(prog_vars). - -Record wt_program (p: program) : Prop := mk_wt_program { - wt_program_funct: - forall id fd, - In (id, fd) p.(prog_funct) -> - wt_fundef (global_typenv p) fd; - wt_program_main: - forall fd, - In (p.(prog_main), fd) p.(prog_funct) -> - exists targs, type_of_fundef fd = Tfunction targs (Tint I32 Signed) -}. - -(* ** Type-checking algorithm *) - -(** We now define and prove correct a type-checking algorithm - for the type system defined above. *) - -Lemma eq_signedness: forall (s1 s2: signedness), {s1=s2} + {s1<>s2}. -Proof. decide equality. Qed. - -Lemma eq_intsize: forall (s1 s2: intsize), {s1=s2} + {s1<>s2}. -Proof. decide equality. Qed. - -Lemma eq_floatsize: forall (s1 s2: floatsize), {s1=s2} + {s1<>s2}. -Proof. decide equality. Qed. - -Fixpoint eq_type (t1 t2: type) {struct t1}: bool := - match t1, t2 with - | Tvoid, Tvoid => true - | Tint sz1 sg1, Tint sz2 sg2 => - if eq_intsize sz1 sz2 - then if eq_signedness sg1 sg2 then true else false - else false - | Tfloat sz1, Tfloat sz2 => - if eq_floatsize sz1 sz2 then true else false - | Tpointer u1, Tpointer u2 => eq_type u1 u2 - | Tarray u1 sz1, Tarray u2 sz2 => - eq_type u1 u2 && if zeq sz1 sz2 then true else false - | Tfunction args1 res1, Tfunction args2 res2 => - eq_typelist args1 args2 && eq_type res1 res2 - | Tstruct id1 f1, Tstruct id2 f2 => - if ident_eq id1 id2 then eq_fieldlist f1 f2 else false - | Tunion id1 f1, Tunion id2 f2 => - if ident_eq id1 id2 then eq_fieldlist f1 f2 else false - | Tcomp_ptr id1, Tcomp_ptr id2 => - if ident_eq id1 id2 then true else false - | _, _ => false - end - -with eq_typelist (t1 t2: typelist) {struct t1} : bool := - match t1, t2 with - | Tnil, Tnil => true - | Tcons u1 r1, Tcons u2 r2 => eq_type u1 u2 && eq_typelist r1 r2 - | _, _ => false - end - -with eq_fieldlist (f1 f2: fieldlist) {struct f1} : bool := - match f1, f2 with - | Fnil, Fnil => true - | Fcons id1 t1 r1, Fcons id2 t2 r2 => - if ident_eq id1 id2 - then eq_type t1 t2 && eq_fieldlist r1 r2 - else false - | _, _ => false - end. - -Ltac TrueInv := - match goal with - | [ H: ((if ?x then ?y else false) = true) |- _ ] => - destruct x; [TrueInv | discriminate] - | [ H: (?x && ?y = true) |- _ ] => - elim (andb_prop _ _ H); clear H; intros; TrueInv - | _ => - idtac - end. - -Scheme type_ind_3 := Induction for type Sort Prop - with typelist_ind_3 := Induction for typelist Sort Prop - with fieldlist_ind_3 := Induction for fieldlist Sort Prop. - -Lemma eq_type_correct: - forall t1 t2, eq_type t1 t2 = true -> t1 = t2. -Proof. - apply (type_ind_3 (fun t1 => forall t2, eq_type t1 t2 = true -> t1 = t2) - (fun t1 => forall t2, eq_typelist t1 t2 = true -> t1 = t2) - (fun t1 => forall t2, eq_fieldlist t1 t2 = true -> t1 = t2)); - intros; destruct t2; simpl in *; try discriminate. - auto. - TrueInv. congruence. - TrueInv. congruence. - decEq; auto. - TrueInv. decEq; auto. - TrueInv. decEq; auto. - TrueInv. subst i0. decEq; auto. - TrueInv. subst i0. decEq; auto. - TrueInv. congruence. - auto. - TrueInv. decEq; auto. - auto. - TrueInv. decEq; auto. -Qed. - -Section TYPECHECKING. - -Variable env: typenv. - -Fixpoint typecheck_expr (a: Csyntax.expr) {struct a} : bool := - match a with - | Expr ad aty => typecheck_exprdescr ad aty - end - -with typecheck_exprdescr (a: Csyntax.expr_descr) (ty: type) {struct a} : bool := - match a with - | Csyntax.Econst_int n => true - | Csyntax.Econst_float n => true - | Csyntax.Evar id => - match env!id with - | None => false - | Some ty' => eq_type ty ty' - end - | Csyntax.Ederef b => typecheck_expr b - | Csyntax.Eaddrof b => typecheck_expr b - | Csyntax.Eunop op b => typecheck_expr b - | Csyntax.Ebinop op b c => typecheck_expr b && typecheck_expr c - | Csyntax.Ecast ty b => typecheck_expr b - | Csyntax.Econdition b c d => typecheck_expr b && typecheck_expr c && typecheck_expr d - | Csyntax.Eandbool b c => typecheck_expr b && typecheck_expr c - | Csyntax.Eorbool b c => typecheck_expr b && typecheck_expr c - | Csyntax.Esizeof ty => true - | Csyntax.Efield b i => typecheck_expr b - end. - -Fixpoint typecheck_exprlist (al: list Csyntax.expr): bool := - match al with - | nil => true - | a1 :: a2 => typecheck_expr a1 && typecheck_exprlist a2 - end. - -Definition typecheck_optexpr (opta: option Csyntax.expr): bool := - match opta with - | None => true - | Some a => typecheck_expr a - end. - -Scheme expr_ind_2 := Induction for expr Sort Prop - with expr_descr_ind_2 := Induction for expr_descr Sort Prop. - -Lemma typecheck_expr_correct: - forall a, typecheck_expr a = true -> wt_expr env a. -Proof. - apply (expr_ind_2 (fun a => typecheck_expr a = true -> wt_expr env a) - (fun a => forall ty, typecheck_exprdescr a ty = true -> wt_expr env (Expr a ty))); - simpl; intros; TrueInv; try constructor; auto. - destruct (env!i). decEq; symmetry; apply eq_type_correct; auto. - discriminate. -Qed. - -Lemma typecheck_exprlist_correct: - forall a, typecheck_exprlist a = true -> wt_exprlist env a. -Proof. - induction a; simpl; intros. - constructor. - TrueInv. constructor; auto. apply typecheck_expr_correct; auto. -Qed. - -Lemma typecheck_optexpr_correct: - forall a, typecheck_optexpr a = true -> wt_optexpr env a. -Proof. - destruct a; simpl; intros. - constructor. apply typecheck_expr_correct; auto. - constructor. -Qed. - -Fixpoint typecheck_stmt (s: Csyntax.statement) {struct s} : bool := - match s with - | Csyntax.Sskip => true - | Csyntax.Sassign b c => typecheck_expr b && typecheck_expr c - | Csyntax.Scall a b cl => typecheck_optexpr a && typecheck_expr b && typecheck_exprlist cl - | Csyntax.Ssequence s1 s2 => typecheck_stmt s1 && typecheck_stmt s2 - | Csyntax.Sifthenelse e s1 s2 => - typecheck_expr e && typecheck_stmt s1 && typecheck_stmt s2 - | Csyntax.Swhile e s1 => typecheck_expr e && typecheck_stmt s1 - | Csyntax.Sdowhile e s1 => typecheck_expr e && typecheck_stmt s1 - | Csyntax.Sfor e1 e2 e3 s1 => - typecheck_stmt e1 && typecheck_expr e2 && - typecheck_stmt e3 && typecheck_stmt s1 - | Csyntax.Sbreak => true - | Csyntax.Scontinue => true - | Csyntax.Sreturn (Some e) => typecheck_expr e - | Csyntax.Sreturn None => true - | Csyntax.Sswitch e sl => typecheck_expr e && typecheck_lblstmts sl - | Csyntax.Slabel lbl s => typecheck_stmt s - | Csyntax.Sgoto lbl => true - end - -with typecheck_lblstmts (sl: labeled_statements) {struct sl}: bool := - match sl with - | LSdefault s => typecheck_stmt s - | LScase _ s rem => typecheck_stmt s && typecheck_lblstmts rem - end. - -Scheme stmt_ind_2 := Induction for statement Sort Prop - with lblstmts_ind_2 := Induction for labeled_statements Sort Prop. - -Lemma typecheck_stmt_correct: - forall s, typecheck_stmt s = true -> wt_stmt env s. -Proof. - generalize typecheck_expr_correct; intro. - generalize typecheck_exprlist_correct; intro. - generalize typecheck_optexpr_correct; intro. - apply (stmt_ind_2 (fun s => typecheck_stmt s = true -> wt_stmt env s) - (fun s => typecheck_lblstmts s = true -> wt_lblstmts env s)); - simpl; intros; TrueInv; constructor; auto. -Qed. - -End TYPECHECKING. - -Definition typecheck_function (env: typenv) (f: function) : bool := - if list_norepet_dec ident_eq - (var_names f.(fn_params) ++ var_names f.(fn_vars)) - then typecheck_stmt (add_vars env (f.(fn_params) ++ f.(fn_vars))) - f.(fn_body) - else false. - -Lemma typecheck_function_correct: - forall env f, typecheck_function env f = true -> wt_function env f. -Proof. - unfold typecheck_function; intros; TrueInv. - constructor. auto. apply typecheck_stmt_correct; auto. -Qed. - -Definition typecheck_fundef (main: ident) (env: typenv) (id_fd: ident * fundef) : bool := - let (id, fd) := id_fd in - match fd with - | Internal f => - typecheck_function env f - | External ef targs tres => - let s := ef_sig ef in - list_eq_dec typ_eq s.(sig_args) (typlist_of_typelist targs) - && opt_typ_eq s.(sig_res) (opttyp_of_type tres) - end && - if ident_eq id main - then match type_of_fundef fd with - | Tfunction targs tres => eq_type tres (Tint I32 Signed) - | _ => false - end - else true. - -Lemma typecheck_fundef_correct: - forall main env id fd, - typecheck_fundef main env (id, fd) = true -> - wt_fundef env fd /\ - (id = main -> - exists targs, type_of_fundef fd = Tfunction targs (Tint I32 Signed)). -Proof. - intros. unfold typecheck_fundef in H; TrueInv. - split. - destruct fd. - constructor. apply typecheck_function_correct; auto. - TrueInv. constructor; eapply proj_sumbool_true; eauto. - intro. destruct (ident_eq id main). - destruct (type_of_fundef fd); try discriminate. - exists t; decEq; auto. apply eq_type_correct; auto. - congruence. -Qed. - -Definition typecheck_program (p: program) : bool := - List.forallb (typecheck_fundef p.(prog_main) (global_typenv p)) - p.(prog_funct). - -Lemma typecheck_program_correct: - forall p, typecheck_program p = true -> wt_program p. -Proof. - unfold typecheck_program; intros. - rewrite List.forallb_forall in H. - constructor; intros. - exploit typecheck_fundef_correct; eauto. tauto. - exploit typecheck_fundef_correct; eauto. tauto. -Qed. -- cgit