Revu traitement des structures et unions recursives. Dans Cshmgen, meilleure compilation de exit_if_false.

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

5 files changed, 45 insertions, 41 deletions

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 5431697f..4cc85559 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -556,15 +556,15 @@ with eval_lvalue: env -> mem -> expr -> trace -> mem -> block -> int -> Prop :=
       sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) ->
       eval_lvalue e m (Expr (Eindex a1 a2) ty)
                   (t1 ** t2) m2 l ofs
- | eval_Efield_struct:   forall e m a t m1 l ofs fList i ty delta,
+ | eval_Efield_struct:   forall e m a t m1 l ofs id fList i ty delta,
       eval_lvalue e m a t m1 l ofs ->
-      typeof a = Tstruct fList ->
+      typeof a = Tstruct id fList ->
       field_offset i fList = Some delta ->
       eval_lvalue e m (Expr (Efield a i) ty)
                   t m1 l (Int.add ofs (Int.repr delta))
- | eval_Efield_union:   forall e m a t m1 l ofs fList i ty,
+ | eval_Efield_union:   forall e m a t m1 l ofs id fList i ty,
       eval_lvalue e m a t m1 l ofs ->
-      typeof a = Tunion fList ->
+      typeof a = Tunion id fList ->
       eval_lvalue e m (Expr (Efield a i) ty) 
                   t m1 l ofs
 
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 5585416b..aaec07d8 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -41,8 +41,9 @@ Definition var_kind_of_type (ty: type): option var_kind :=
   | Tpointer _ => Some(Vscalar Mint32)
   | Tarray _ _ => Some(Varray (Csyntax.sizeof ty))
   | Tfunction _ _ => None
-  | Tstruct fList => Some(Varray (Csyntax.sizeof ty))
-  | Tunion fList => Some(Varray (Csyntax.sizeof ty))
+  | Tstruct _ fList => Some(Varray (Csyntax.sizeof ty))
+  | Tunion _ fList => Some(Varray (Csyntax.sizeof ty))
+  | Tcomp_ptr _ => Some(Vscalar Mint32)
 end.
   
 (** ** Csharpminor constructors *)
@@ -359,13 +360,13 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr :=
       Some(make_intconst (Int.repr (Csyntax.sizeof ty)))
   | Expr (Csyntax.Efield b i) ty => 
       match typeof b with
-      | Tstruct fld =>
+      | Tstruct _ fld =>
           do tb <- transl_lvalue b;
           do ofs <- field_offset i fld;
           make_load
             (make_binop Oadd tb (make_intconst (Int.repr ofs)))
             ty
-      | Tunion fld =>
+      | Tunion _ fld =>
           do tb <- transl_lvalue b;
           make_load tb ty
       | _ => None
@@ -389,11 +390,11 @@ with transl_lvalue (a: Csyntax.expr) {struct a} : option expr :=
       make_add tb (typeof b) tc (typeof c)
   | Expr (Csyntax.Efield b i) ty => 
       match typeof b with
-      | Tstruct fld =>
+      | Tstruct _ fld =>
           do tb <- transl_lvalue b;
           do ofs <- field_offset i fld;
           Some (make_binop Oadd tb (make_intconst (Int.repr ofs)))
-      | Tunion fld =>
+      | Tunion _ fld =>
           transl_lvalue b
       | _ => None
       end
@@ -430,9 +431,9 @@ Definition is_variable (e: Csyntax.expr) : option ident :=
 Definition exit_if_false (e: Csyntax.expr) : option stmt :=
   do te <- transl_expr e;
   Some(Sifthenelse
-        (make_notbool te (typeof e))
-        (Sexit 0%nat)
-        Sskip).
+        (make_boolean te (typeof e))
+        Sskip
+        (Sexit 0%nat)).
 
 (* [transl_statement nbrk ncnt s] returns a Csharpminor statement
    that performs the same computations as the CabsCoq statement [s].
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index 5b4146bf..497286b3 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -725,11 +725,11 @@ Qed.
 
 Lemma transl_Efield_struct_correct:
        (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace)
-          (m1 : mem) (l : block) (ofs : int) (fList : fieldlist) (i : ident)
+          (m1 : mem) (l : block) (ofs : int) (id: ident) (fList : fieldlist) (i : ident)
           (ty : type) (delta : Z),
         eval_lvalue ge e m a t m1 l ofs ->
         eval_lvalue_prop e m a t m1 l ofs ->
-        typeof a = Tstruct fList ->
+        typeof a = Tstruct id fList ->
         field_offset i fList = Some delta ->
         eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 l
           (Int.add ofs (Int.repr delta))).
@@ -743,11 +743,11 @@ Qed.
 
 Lemma transl_Efield_union_correct:
        (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace)
-          (m1 : mem) (l : block) (ofs : int) (fList : fieldlist) (i : ident)
+          (m1 : mem) (l : block) (ofs : int) (id: ident) (fList : fieldlist) (i : ident)
           (ty : type),
         eval_lvalue ge e m a t m1 l ofs ->
         eval_lvalue_prop e m a t m1 l ofs ->
-        typeof a = Tunion fList ->
+        typeof a = Tunion id fList ->
         eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 l ofs).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. 
@@ -925,13 +925,9 @@ Lemma exit_if_false_true:
   exec_stmt tprog te m1 ts t m2 Out_normal.
 Proof.
   intros. monadInv H. rewrite <- H5. 
-  eapply exec_Sifthenelse_false with (v1 := Vfalse).
-  eapply make_notbool_correct with (va := v); eauto.
-  inversion H3; subst; simpl; auto.
-  rewrite Int.eq_false; auto.
-  rewrite Int.eq_false; auto.
-  rewrite Float.eq_zero_false; auto.
-  simpl; auto.
+  exploit make_boolean_correct_true. eapply H0; eauto. eauto.
+  intros [vb [EVAL ISTRUE]].
+  eapply exec_Sifthenelse_true with (v1 := vb); eauto. 
   constructor. traceEq.
 Qed.
  
@@ -945,11 +941,9 @@ Lemma exit_if_false_false:
   exec_stmt tprog te m1 ts t m2 (Out_exit 0).
 Proof.
   intros. monadInv H. rewrite <- H5. 
-  eapply exec_Sifthenelse_true with (v1 := Vtrue).
-  eapply make_notbool_correct with (va := v); eauto.
-  inversion H3; subst; simpl; auto.
-  rewrite Float.eq_zero_true; auto.
-  simpl; apply Int.one_not_zero.
+  exploit make_boolean_correct_false. eapply H0; eauto. eauto.
+  intros [vb [EVAL ISFALSE]].
+  eapply exec_Sifthenelse_false with (v1 := vb); eauto. 
   constructor. traceEq.
 Qed.
 
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 979d0bca..f9463e65 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -29,8 +29,9 @@ Inductive type : Set :=
   | Tpointer: type -> type
   | Tarray: type -> Z -> type
   | Tfunction: typelist -> type -> type
-  | Tstruct: fieldlist -> type
-  | Tunion: fieldlist -> type
+  | Tstruct: ident -> fieldlist -> type
+  | Tunion: ident ->fieldlist -> type
+  | Tcomp_ptr: ident -> type
 
 with typelist : Set :=
   | Tnil: typelist
@@ -164,8 +165,9 @@ Fixpoint alignof (t: type) : Z :=
   | Tpointer _ => 4
   | Tarray t' n => alignof t'
   | Tfunction _ _ => 1
-  | Tstruct fld => alignof_fields fld
-  | Tunion fld => alignof_fields fld
+  | Tstruct _ fld => alignof_fields fld
+  | Tunion _ fld => alignof_fields fld
+  | Tcomp_ptr _ => 4
   end
 
 with alignof_fields (f: fieldlist) : Z :=
@@ -208,8 +210,9 @@ Fixpoint sizeof (t: type) : Z :=
   | Tpointer _ => 4
   | Tarray t' n => sizeof t' * Zmax 1 n
   | Tfunction _ _ => 1
-  | Tstruct fld => align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
-  | Tunion fld => align (Zmax 1 (sizeof_union fld)) (alignof t)
+  | Tstruct _ fld => align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
+  | Tunion _ fld => align (Zmax 1 (sizeof_union fld)) (alignof t)
+  | Tcomp_ptr _ => 4
   end
 
 with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z :=
@@ -285,8 +288,9 @@ Definition access_mode (ty: type) : mode :=
   | Tpointer _ => By_value Mint32
   | Tarray _ _ => By_reference
   | Tfunction _ _ => By_reference
-  | Tstruct fList => By_nothing
-  | Tunion fList => By_nothing
+  | Tstruct _ fList => By_nothing
+  | Tunion _ fList => By_nothing
+  | Tcomp_ptr _ => By_value Mint32
 end.
 
 (** Classification of arithmetic operations and comparisons *)
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 797033dc..0795e1b2 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -190,8 +190,12 @@ Fixpoint eq_type (t1 t2: type) {struct t1}: bool :=
       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
+  | 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
 
@@ -239,8 +243,9 @@ Proof.
   decEq; auto.
   TrueInv. decEq; auto.
   TrueInv. decEq; auto.
-  decEq; auto.
-  decEq; auto.
+  TrueInv. subst i0. decEq; auto.
+  TrueInv. subst i0. decEq; auto.
+  TrueInv. congruence.
   auto.
   TrueInv. decEq; auto.
   auto.