From ec6d00d94bcb1a0adc5c698367634b5e2f370c6e Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 27 Sep 2008 08:57:55 +0000 Subject: 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 --- cfrontend/Csem.v | 15 +++++--- cfrontend/Cshmgen.v | 10 ++---- cfrontend/Cshmgenproof1.v | 4 +-- cfrontend/Cshmgenproof3.v | 54 +++++++++++++++++++--------- cfrontend/Csyntax.v | 92 ++++++++++++++++++++++++++++++++++++++++++++++- cfrontend/Ctyping.v | 8 ++--- 6 files changed, 146 insertions(+), 37 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 5e4f4e37..22139127 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 20eb17f4..64a58ad0 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 87cdb21d..2c010cb4 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 a25c5b8b..75dbc145 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 ee1b8617..ac790470 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 b4dd2904..c03552c6 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 -- cgit