Fusion de la branche "traces":

- Ajout de traces d'evenements d'E/S dans les semantiques
- Ajout constructions switch et allocation dynamique
- Initialisation des variables globales
- Portage Coq 8.1 beta
Debut d'integration du front-end C:
- Traduction Clight -> Csharpminor dans cfrontend/
- Modifications de Csharpminor et Globalenvs en consequence.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 420 insertions, 0 deletions

diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
new file mode 100644
index 00000000..8b2f90f2
--- /dev/null
+++ b/cfrontend/Ctyping.v
@@ -0,0 +1,420 @@
+(** * Type well-formedness of C programs *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Csyntax.
+
+(** ** Typing rules *)
+
+(** 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. *)
+
+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_Eindex: forall e1 e2 ty,
+     wt_expr e1 -> wt_expr e2 ->
+     wt_expr (Expr (Eindex e1 e2) ty)
+  | wt_Ecall: forall e1 el ty,
+     wt_expr e1 ->
+     wt_exprlist el ->
+     wt_expr (Expr (Ecall e1 el) 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)
+
+with wt_exprlist: exprlist -> Prop :=
+  | wt_Enil:
+     wt_exprlist Enil
+  | wt_Econs: forall e el,
+     wt_expr e -> wt_exprlist el -> wt_exprlist (Econs e el).
+
+Inductive wt_stmt: statement -> Prop :=
+  | wt_Sskip:
+     wt_stmt Sskip
+  | wt_Sexpr: forall e,
+     wt_expr e ->
+     wt_stmt (Sexpr e)
+  | wt_Sassign: forall e1 e2,
+     wt_expr e1 -> wt_expr e2 ->
+     wt_stmt (Sassign e1 e2)
+  | 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_some: forall e,
+     wt_expr e ->
+     wt_stmt (Sreturn (Some e))
+  | wt_Sreturn_none:
+     wt_stmt (Sreturn None)
+  | wt_Sswitch: forall e sl,
+     wt_expr e -> wt_lblstmts sl ->
+     wt_stmt (Sswitch e sl)
+
+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 id args res,
+      wt_fundef env (External id args res).
+
+Definition add_global_var
+     (env: typenv) (id_ty_init: ident * type * list init_data) : typenv :=
+  match id_ty_init with (id, ty, init) => PTree.set id ty env end.
+
+Definition add_global_vars
+     (env: typenv) (vars: list(ident * type * list init_data)) : 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_defs).
+
+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) ->
+    type_of_fundef fd = Tfunction Tnil (Tint I32 Signed)
+}.
+
+(** ** Type-checking algorithm *)
+
+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 f1, Tstruct f2 => eq_fieldlist f1 f2
+  | Tunion f1, Tunion f2 => eq_fieldlist f1 f2
+  | _, _ => 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.
+  decEq; auto.
+  decEq; auto.
+  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.Eindex b c => typecheck_expr b && typecheck_expr c
+  | Csyntax.Ecall b cl => typecheck_expr b && typecheck_exprlist cl
+  | 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
+
+with typecheck_exprlist (al: Csyntax.exprlist): bool :=
+  match al with
+  | Csyntax.Enil => true
+  | Csyntax.Econs a1 a2 => typecheck_expr a1 && typecheck_exprlist a2
+  end.
+
+Scheme expr_ind_3 := Induction for expr Sort Prop
+  with expr_descr_ind_3 := Induction for expr_descr Sort Prop
+  with exprlist_ind_3 := Induction for exprlist Sort Prop.
+
+Lemma typecheck_expr_correct:
+  forall a, typecheck_expr a = true -> wt_expr env a.
+Proof.
+  apply (expr_ind_3 (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))
+                    (fun a => typecheck_exprlist a = true -> wt_exprlist env a));
+  simpl; intros; TrueInv.
+  auto.
+  constructor.
+  constructor.
+  constructor. destruct (env!i). decEq; symmetry; apply eq_type_correct; auto.
+  discriminate.
+  constructor; auto.
+  constructor; auto.
+  constructor; auto.
+  constructor; auto.
+  constructor; auto.
+  constructor; auto.
+  constructor; auto.
+  constructor; auto.
+  constructor; auto.
+  auto.
+  constructor; auto.
+  constructor; auto.
+  constructor.
+  constructor; auto.
+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.
+
+Fixpoint typecheck_stmt (s: Csyntax.statement) {struct s} : bool :=
+  match s with
+  | Csyntax.Sskip => true
+  | Csyntax.Sexpr e => typecheck_expr e
+  | Csyntax.Sassign b c => typecheck_expr b && typecheck_expr c
+  | 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
+  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.
+  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; try constructor; auto.
+  destruct o; 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 _ _ _ => true
+  end &&
+  if ident_eq id main
+  then eq_type (type_of_fundef fd) (Tfunction Tnil (Tint I32 Signed))
+  else true.
+
+Lemma typecheck_fundef_correct:
+  forall main env id fd,
+  typecheck_fundef main env (id, fd) = true ->
+  wt_fundef env fd /\
+  (id = main -> type_of_fundef fd = Tfunction Tnil (Tint I32 Signed)).
+Proof.
+  intros. unfold typecheck_fundef in H; TrueInv.
+  split. 
+    destruct fd.
+    constructor. apply typecheck_function_correct; auto. 
+    constructor.
+  intro. destruct (ident_eq id main). 
+  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.