From be43363d309cea62731e04ad10dddf3ecafcacd1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 11 Sep 2006 16:03:02 +0000 Subject: 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 --- cfrontend/Csem.v | 8 ++++---- cfrontend/Cshmgen.v | 19 ++++++++++--------- cfrontend/Cshmgenproof3.v | 26 ++++++++++---------------- cfrontend/Csyntax.v | 20 ++++++++++++-------- cfrontend/Ctyping.v | 13 +++++++++---- 5 files changed, 45 insertions(+), 41 deletions(-) (limited to 'cfrontend') 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. -- cgit