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

1 files changed, 0 insertions, 459 deletions

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.