Clight: ajout Econdition, suppression Eindex.

caml/PrintCsyntax.ml: afficher les formes a[b] et a->fld.



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

6 files changed, 146 insertions, 37 deletions

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 5e4f4e3..2213912 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -564,6 +564,16 @@ Inductive eval_expr: expr -> val -> Prop :=
       eval_expr a2 v2 ->
       sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v ->
       eval_expr (Expr (Ebinop op a1 a2) ty) v
+  | eval_Econdition_true: forall a1 a2 a3 ty v1 v2,
+      eval_expr a1 v1 ->
+      is_true v1 (typeof a1) ->
+      eval_expr a2 v2 ->
+      eval_expr (Expr (Econdition a1 a2 a3) ty) v2
+  | eval_Econdition_false: forall a1 a2 a3 ty v1 v3,
+      eval_expr a1 v1 ->
+      is_false v1 (typeof a1) ->
+      eval_expr a3 v3 ->
+      eval_expr (Expr (Econdition a1 a2 a3) ty) v3
   | eval_Eorbool_1: forall a1 a2 ty v1,
       eval_expr a1 v1 ->
       is_true v1 (typeof a1) ->
@@ -604,11 +614,6 @@ with eval_lvalue: expr -> block -> int -> Prop :=
   | eval_Ederef: forall a ty l ofs,
       eval_expr a (Vptr l ofs) ->
       eval_lvalue (Expr (Ederef a) ty) l ofs
-  | eval_Eindex: forall a1 a2 ty v1 v2 l ofs,
-      eval_expr a1 v1 ->
-      eval_expr a2 v2 ->
-      sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) ->
-      eval_lvalue (Expr (Eindex a1 a2) ty) l ofs
  | eval_Efield_struct:   forall a i ty l ofs id fList delta,
       eval_lvalue a l ofs ->
       typeof a = Tstruct id fList ->
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 20eb17f..64a58ad 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -383,11 +383,11 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : res expr :=
   | Expr (Csyntax.Ecast ty b) _ =>
       do tb <- transl_expr b;
       OK (make_cast (typeof b) ty tb)
-  | Expr (Csyntax.Eindex b c) ty =>
+  | Expr (Csyntax.Econdition b c d) _ =>
       do tb <- transl_expr b;
       do tc <- transl_expr c;
-      do ts <- make_add tb (typeof b) tc (typeof c);
-      make_load ts ty
+      do td <- transl_expr d;
+      OK(Econdition (make_boolean tb (typeof b)) tc td)
   | Expr (Csyntax.Eandbool b c) _ =>
       do tb <- transl_expr b;
       do tc <- transl_expr c;
@@ -425,10 +425,6 @@ with transl_lvalue (a: Csyntax.expr) {struct a} : res expr :=
       OK (Eaddrof id)
   | Expr (Csyntax.Ederef b) _ =>
       transl_expr b
-  | Expr (Csyntax.Eindex b c) _ =>
-      do tb <- transl_expr b;
-      do tc <- transl_expr c;
-      make_add tb (typeof b) tc (typeof c)
   | Expr (Csyntax.Efield b i) ty => 
       match typeof b with
       | Tstruct _ fld =>
diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v
index 87cdb21..2c010cb 100644
--- a/cfrontend/Cshmgenproof1.v
+++ b/cfrontend/Cshmgenproof1.v
@@ -197,9 +197,7 @@ Proof.
   intros. inversion H; subst; clear H; simpl in H0.
   left; exists id; auto.
   left; exists id; auto.
-  monadInv H0. right. exists x; split; auto. 
-  simpl. monadInv H0. right. exists x1; split; auto. 
-  simpl. rewrite EQ; rewrite EQ1. simpl. auto.
+  monadInv H0. right. exists x; split; auto.
   rewrite H4 in H0. monadInv H0. right.  
   exists (Ebinop Oadd x (make_intconst (Int.repr x0))). split; auto.
   simpl. rewrite H4. rewrite EQ. rewrite EQ1. auto.
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index a25c5b8..75dbc14 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -482,7 +482,7 @@ Definition eval_exprlist_prop (al: list Csyntax.expr) (vl: list val) : Prop :=
     (TR: transl_exprlist al = OK tal),
   Csharpminor.eval_exprlist tprog te m tal vl.
 
-(* Check (eval_expr_ind2 ge e m eval_expr_prop eval_lvalue_prop).*)
+(* Check (eval_expr_ind2 ge e m eval_expr_prop eval_lvalue_prop). *)
 
 Lemma transl_Econst_int_correct:
   forall (i : int) (ty : type),
@@ -565,6 +565,38 @@ Proof.
   eapply transl_binop_correct; eauto. 
 Qed.
 
+Lemma transl_Econdition_true_correct:
+  forall (a1 a2 a3 : Csyntax.expr) (ty : type) (v1 v2 : val),
+  Csem.eval_expr ge e m a1 v1 ->
+  eval_expr_prop a1 v1 ->
+  is_true v1 (typeof a1) ->
+  Csem.eval_expr ge e m a2 v2 ->
+  eval_expr_prop a2 v2 ->
+  eval_expr_prop (Expr (Csyntax.Econdition a1 a2 a3) ty) v2.
+Proof.
+  intros; red; intros. inv WT. monadInv TR. 
+  exploit make_boolean_correct_true. eapply H0; eauto. eauto.
+  intros [vb [EVAL ISTRUE]].
+  eapply eval_Econdition; eauto. apply Val.bool_of_true_val; eauto.
+  simpl. eauto. 
+Qed.
+
+Lemma transl_Econdition_false_correct:
+  forall (a1 a2 a3 : Csyntax.expr) (ty : type) (v1 v3 : val),
+  Csem.eval_expr ge e m a1 v1 ->
+  eval_expr_prop a1 v1 ->
+  is_false v1 (typeof a1) ->
+  Csem.eval_expr ge e m a3 v3 ->
+  eval_expr_prop a3 v3 ->
+  eval_expr_prop (Expr (Csyntax.Econdition a1 a2 a3) ty) v3.
+Proof.
+  intros; red; intros. inv WT. monadInv TR. 
+  exploit make_boolean_correct_false. eapply H0; eauto. eauto.
+  intros [vb [EVAL ISTRUE]].
+  eapply eval_Econdition; eauto. apply Val.bool_of_false_val; eauto.
+  simpl. eauto. 
+Qed.
+
 Lemma transl_Eorbool_1_correct:
   forall (a1 a2 : Csyntax.expr) (ty : type) (v1 : val),
   Csem.eval_expr ge e m a1 v1 ->
@@ -681,20 +713,6 @@ Proof.
   eauto.
 Qed.
 
-Lemma transl_Eindex_correct:
-  forall (a1 a2 : Csyntax.expr) (ty : type) (v1 v2 : val) (l : block)
-         (ofs : int),
-  Csem.eval_expr ge e m a1 v1 ->
-  eval_expr_prop a1 v1 ->
-  Csem.eval_expr ge e m a2 v2 ->
-  eval_expr_prop a2 v2 ->
-  sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) ->
-  eval_lvalue_prop (Expr (Eindex a1 a2) ty) l ofs.
-Proof.
-  intros; red; intros. inversion WT; clear WT; subst. simpl in TR. monadInv TR.
-  eapply (make_add_correct tprog); eauto. 
-Qed.
-
 Lemma transl_Efield_struct_correct:
   forall (a : Csyntax.expr) (i : ident) (ty : type) (l : block)
          (ofs : int) (id : ident) (fList : fieldlist) (delta : Z),
@@ -736,6 +754,8 @@ Proof
          transl_Esizeof_correct
          transl_Eunop_correct
          transl_Ebinop_correct
+         transl_Econdition_true_correct
+         transl_Econdition_false_correct
          transl_Eorbool_1_correct
          transl_Eorbool_2_correct
          transl_Eandbool_1_correct
@@ -744,7 +764,6 @@ Proof
          transl_Evar_local_correct
          transl_Evar_global_correct
          transl_Ederef_correct
-         transl_Eindex_correct
          transl_Efield_struct_correct
          transl_Efield_union_correct).
 
@@ -761,6 +780,8 @@ Proof
          transl_Esizeof_correct
          transl_Eunop_correct
          transl_Ebinop_correct
+         transl_Econdition_true_correct
+         transl_Econdition_false_correct
          transl_Eorbool_1_correct
          transl_Eorbool_2_correct
          transl_Eandbool_1_correct
@@ -769,7 +790,6 @@ Proof
          transl_Evar_local_correct
          transl_Evar_global_correct
          transl_Ederef_correct
-         transl_Eindex_correct
          transl_Efield_struct_correct
          transl_Efield_union_correct).
 
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index ee1b861..ac79047 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -150,7 +150,7 @@ with expr_descr : Set :=
   | Eunop: unary_operation -> expr -> expr_descr  (**r unary operation *)
   | Ebinop: binary_operation -> expr -> expr -> expr_descr (**r binary operation *)
   | Ecast: type -> expr -> expr_descr   (**r type cast ([(ty) e]) *)
-  | Eindex: expr -> expr -> expr_descr  (**r array indexing ([e1[e2]]) *)
+  | Econdition: expr -> expr -> expr -> expr_descr (**r conditional ([e1 ? e2 : e3]) *)
   | Eandbool: expr -> expr -> expr_descr (**r sequential and ([&&]) *)
   | Eorbool: expr -> expr -> expr_descr (**r sequential or ([||]) *)
   | Esizeof: type -> expr_descr         (**r size of a type *)
@@ -331,6 +331,16 @@ Proof.
   generalize (align_le pos (alignof t) (alignof_pos t)). omega.
 Qed.
 
+Lemma sizeof_struct_incr:
+  forall fld pos, pos <= sizeof_struct fld pos.
+Proof.
+  induction fld; intros; simpl. omega. 
+  eapply Zle_trans. 2: apply IHfld.
+  apply Zle_trans with (align pos (alignof t)). 
+  apply align_le. apply alignof_pos. 
+  assert (sizeof t > 0) by apply sizeof_pos. omega.
+Qed.
+
 (** Byte offset for a field in a struct or union.
   Field are laid out consecutively, and padding is inserted
   to align each field to the natural alignment for its type. *)
@@ -350,6 +360,86 @@ Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
 Definition field_offset (id: ident) (fld: fieldlist) : res Z :=
   field_offset_rec id fld 0.
 
+Fixpoint field_type (id: ident) (fld: fieldlist) {struct fld} : res type :=
+  match fld with
+  | Fnil => Error (MSG "Unknown field " :: CTX id :: nil)
+  | Fcons id' t fld' => if ident_eq id id' then OK t else field_type id fld'
+  end.
+
+(** Some sanity checks about field offsets.  First, field offsets are 
+  within the range of acceptable offsets. *)
+
+Remark field_offset_rec_in_range:
+  forall id ofs ty fld pos,
+  field_offset_rec id fld pos = OK ofs -> field_type id fld = OK ty ->
+  pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos.
+Proof.
+  intros until ty. induction fld; simpl.
+  congruence.
+  destruct (ident_eq id i); intros.
+  inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr.
+  exploit IHfld; eauto. intros [A B]. split; auto. 
+  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)).
+  apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega. 
+Qed.
+
+Lemma field_offset_in_range:
+  forall id fld ofs ty,
+  field_offset id fld = OK ofs -> field_type id fld = OK ty ->
+  0 <= ofs /\ ofs + sizeof ty <= sizeof_struct fld 0.
+Proof.
+  intros. eapply field_offset_rec_in_range. unfold field_offset in H; eauto. eauto.
+Qed.
+
+(** Second, two distinct fields do not overlap *)
+
+Lemma field_offset_no_overlap:
+  forall id1 ofs1 ty1 id2 ofs2 ty2 fld,
+  field_offset id1 fld = OK ofs1 -> field_type id1 fld = OK ty1 ->
+  field_offset id2 fld = OK ofs2 -> field_type id2 fld = OK ty2 ->
+  id1 <> id2 ->
+  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1.
+Proof.
+  intros until ty2. intros fld0 A B C D NEQ.
+  assert (forall fld pos,
+  field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 ->
+  field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 ->
+  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1).
+  induction fld; intro pos; simpl. congruence.
+  destruct (ident_eq id1 i); destruct (ident_eq id2 i).
+  congruence. 
+  subst i. intros. inv H; inv H0.
+  exploit field_offset_rec_in_range; eauto. tauto. 
+  subst i. intros. inv H1; inv H2.
+  exploit field_offset_rec_in_range; eauto. tauto. 
+  intros. eapply IHfld; eauto.
+
+  apply H with fld0 0; auto.
+Qed.
+
+(** Third, if a struct is a prefix of another, the offsets of fields
+  in common is the same. *)
+
+Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist :=
+  match fld1 with
+  | Fnil => fld2
+  | Fcons id ty fld => Fcons id ty (fieldlist_app fld fld2)
+  end.
+
+Lemma field_offset_prefix:
+  forall id ofs fld2 fld1,
+  field_offset id fld1 = OK ofs ->
+  field_offset id (fieldlist_app fld1 fld2) = OK ofs.
+Proof.
+  intros until fld2.
+  assert (forall fld1 pos, 
+    field_offset_rec id fld1 pos = OK ofs ->
+    field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs).
+  induction fld1; intros pos; simpl. congruence.
+  destruct (ident_eq id i); auto.
+  intros. unfold field_offset; auto. 
+Qed.
+
 (** The [access_mode] function describes how a variable of the given
 type must be accessed:
 - [By_value ch]: access by value, i.e. by loading from the address
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index b4dd290..c03552c 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -56,9 +56,9 @@ Inductive wt_expr: expr -> Prop :=
   | 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_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)
@@ -296,7 +296,7 @@ with typecheck_exprdescr (a: Csyntax.expr_descr) (ty: type) {struct a} : bool :=
   | 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.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