From 25b9b003178002360d666919f2e49e7f5f4a36e2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Feb 2012 19:14:14 +0000 Subject: Merge of the "volatile" branch: - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Initializersproof.v | 89 +++++++++++++++++++++++-------------------- 1 file changed, 48 insertions(+), 41 deletions(-) (limited to 'cfrontend/Initializersproof.v') diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 6563a352..4d287bcc 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -86,14 +86,14 @@ Inductive eval_simple_lvalue: expr -> block -> int -> Prop := | esl_deref: forall r ty b ofs, eval_simple_rvalue r (Vptr b ofs) -> eval_simple_lvalue (Ederef r ty) b ofs - | esl_field_struct: forall l f ty b ofs id fList delta, - eval_simple_lvalue l b ofs -> - typeof l = Tstruct id fList -> field_offset f fList = OK delta -> - eval_simple_lvalue (Efield l f ty) b (Int.add ofs (Int.repr delta)) - | esl_field_union: forall l f ty b ofs id fList, - eval_simple_lvalue l b ofs -> - typeof l = Tunion id fList -> - eval_simple_lvalue (Efield l f ty) b ofs + | esl_field_struct: forall r f ty b ofs id fList a delta, + eval_simple_rvalue r (Vptr b ofs) -> + typeof r = Tstruct id fList a -> field_offset f fList = OK delta -> + eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta)) + | esl_field_union: forall r f ty b ofs id fList a, + eval_simple_rvalue r (Vptr b ofs) -> + typeof r = Tunion id fList a -> + eval_simple_lvalue (Efield r f ty) b ofs with eval_simple_rvalue: expr -> val -> Prop := | esr_val: forall v ty, @@ -101,7 +101,7 @@ with eval_simple_rvalue: expr -> val -> Prop := | esr_rvalof: forall b ofs l ty v, eval_simple_lvalue l b ofs -> ty = typeof l -> - load_value_of_type ty m b ofs = Some v -> + deref_loc ge ty m b ofs E0 v -> eval_simple_rvalue (Evalof l ty) v | esr_addrof: forall b ofs l ty, eval_simple_lvalue l b ofs -> @@ -166,17 +166,17 @@ Proof. Qed. Lemma rred_simple: - forall r m r' m', rred r m r' m' -> simple r -> simple r'. + forall r m t r' m', rred ge r m t r' m' -> simple r -> simple r'. Proof. induction 1; simpl; intuition. destruct b; auto. Qed. Lemma rred_compat: - forall e r m r' m', rred r m r' m' -> + forall e r m r' m', rred ge r m E0 r' m' -> simple r -> m = m' /\ compat_eval RV e r r' m. Proof. - induction 1; simpl; intro SIMP; try contradiction; split; auto; split; auto; intros vx EV. + intros until m'; intros RED SIMP. inv RED; simpl in SIMP; try contradiction; split; auto; split; auto; intros vx EV. inv EV. econstructor. constructor. auto. auto. inv EV. econstructor. constructor. inv EV. econstructor; eauto. constructor. @@ -227,12 +227,12 @@ Qed. Lemma simple_context_2: forall a a', simple a' -> forall from to C, context from to C -> simple (C a) -> simple (C a'). Proof. - induction 2; simpl; tauto. + induction 2; simpl; try tauto. Qed. Lemma compat_eval_steps: - forall f r e m w r' m', - star step ge (ExprState f r Kstop e m) w (ExprState f r' Kstop e m') -> + forall f r e m r' m', + star step ge (ExprState f r Kstop e m) E0 (ExprState f r' Kstop e m') -> simple r -> m' = m /\ compat_eval RV e r r' m. Proof. @@ -240,10 +240,10 @@ Proof. (* base case *) split. auto. red; auto. (* inductive case *) - destruct H. + destruct (app_eq_nil t1 t2); auto. subst. inv H. (* expression step *) assert (X: exists r1, s2 = ExprState f r1 Kstop e m /\ compat_eval RV e r r1 m /\ simple r1). - inv H. + inv H3. (* lred *) assert (S: simple a) by (eapply simple_context_1; eauto). exploit lred_compat; eauto. intros [A B]. subst m'0. @@ -258,17 +258,19 @@ Proof. eapply simple_context_2; eauto. eapply rred_simple; eauto. (* callred *) assert (S: simple a) by (eapply simple_context_1; eauto). - inv H10; simpl in S; contradiction. + inv H9; simpl in S; contradiction. + (* stuckred *) + inv H2. destruct H; inv H. destruct X as [r1 [A [B C]]]. subst s2. exploit IHstar; eauto. intros [D E]. split. auto. destruct B; destruct E. split. congruence. auto. (* statement steps *) - inv H. + inv H3. Qed. Theorem eval_simple_steps: - forall f r e m w v ty m', - star step ge (ExprState f r Kstop e m) w (ExprState f (Eval v ty) Kstop e m') -> + forall f r e m v ty m', + star step ge (ExprState f r Kstop e m) E0 (ExprState f (Eval v ty) Kstop e m') -> simple r -> m' = m /\ ty = typeof r /\ eval_simple_rvalue e m r v. Proof. @@ -406,6 +408,12 @@ Proof. rewrite H2 in H. inv H0. inv H. constructor. rewrite H2 in H. inv H0. inv H. constructor. rewrite H2 in H. inv H0. destruct (cast_float_int si2 f); inv H. inv H7. constructor. + rewrite H2 in H. inv H0. inv H. constructor. + rewrite H2 in H. inv H0. inv H. constructor. + rewrite H2 in H. inv H0. inv H. rewrite H7. constructor. + rewrite H2 in H. inv H0. inv H. rewrite H7. constructor. + rewrite H2 in H. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. auto. + rewrite H2 in H. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. auto. rewrite H5 in H. inv H. auto. Qed. @@ -437,8 +445,7 @@ Proof. (* val *) destruct v; monadInv CV; constructor. (* rval *) - unfold load_value_of_type in H1. destruct (access_mode ty); try congruence. inv H1. - eauto. + inv H1; rewrite H2 in CV; try congruence. eauto. (* addrof *) eauto. (* unop *) @@ -468,10 +475,10 @@ Proof. (* deref *) eauto. (* field struct *) - rewrite H0 in CV. monadInv CV. exploit IHeval_simple_lvalue; eauto. intro MV. inv MV. + rewrite H0 in CV. monadInv CV. exploit constval_rvalue; eauto. intro MV. inv MV. simpl. replace x with delta by congruence. constructor. auto. (* field union *) - rewrite H0 in CV. auto. + rewrite H0 in CV. eauto. Qed. Lemma constval_simple: @@ -487,8 +494,8 @@ Qed. (** Soundness of [constval] with respect to the reduction semantics. *) Theorem constval_steps: - forall f r m w v v' ty m', - star step ge (ExprState f r Kstop empty_env m) w (ExprState f (Eval v' ty) Kstop empty_env m') -> + forall f r m v v' ty m', + star step ge (ExprState f r Kstop empty_env m) E0 (ExprState f (Eval v' ty) Kstop empty_env m') -> constval r = OK v -> m' = m /\ ty = typeof r /\ match_val v v'. Proof. @@ -501,9 +508,9 @@ Qed. (** Soundness for single initializers. *) Theorem transl_init_single_steps: - forall ty a data f m w v1 ty1 m' v chunk b ofs m'', + forall ty a data f m v1 ty1 m' v chunk b ofs m'', transl_init_single ty a = OK data -> - star step ge (ExprState f a Kstop empty_env m) w (ExprState f (Eval v1 ty1) Kstop empty_env m') -> + star step ge (ExprState f a Kstop empty_env m) E0 (ExprState f (Eval v1 ty1) Kstop empty_env m') -> sem_cast v1 ty1 ty = Some v -> access_mode ty = By_value chunk -> Mem.store chunk m' b ofs v = Some m'' -> @@ -583,9 +590,9 @@ Proof. Qed. Remark sizeof_struct_eq: - forall id fl, + forall id fl a, fl <> Fnil -> - sizeof (Tstruct id fl) = align (sizeof_struct fl 0) (alignof (Tstruct id fl)). + sizeof (Tstruct id fl a) = align (sizeof_struct fl 0) (alignof (Tstruct id fl a)). Proof. intros. simpl. f_equal. rewrite Zmax_spec. apply zlt_false. destruct fl. congruence. simpl. @@ -595,9 +602,9 @@ Proof. Qed. Remark sizeof_union_eq: - forall id fl, + forall id fl a, fl <> Fnil -> - sizeof (Tunion id fl) = align (sizeof_union fl) (alignof (Tunion id fl)). + sizeof (Tunion id fl a) = align (sizeof_union fl) (alignof (Tunion id fl a)). Proof. intros. simpl. f_equal. rewrite Zmax_spec. apply zlt_false. destruct fl. congruence. simpl. @@ -705,15 +712,15 @@ Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := access_mode ty = By_value chunk -> Mem.store chunk m' b ofs v = Some m'' -> exec_init m b ofs ty (Init_single a) m'' - | exec_init_compound_array: forall m b ofs ty sz il m', + | exec_init_compound_array: forall m b ofs ty sz a il m', exec_init_array m b ofs ty sz il m' -> - exec_init m b ofs (Tarray ty sz) (Init_compound il) m' - | exec_init_compound_struct: forall m b ofs id fl il m', - exec_init_list m b ofs (fields_of_struct id (Tstruct id fl) fl 0) il m' -> - exec_init m b ofs (Tstruct id fl) (Init_compound il) m' - | exec_init_compound_union: forall m b ofs id id1 ty1 fl i m', - exec_init m b ofs (unroll_composite id (Tunion id (Fcons id1 ty1 fl)) ty1) i m' -> - exec_init m b ofs (Tunion id (Fcons id1 ty1 fl)) (Init_compound (Init_cons i Init_nil)) m' + exec_init m b ofs (Tarray ty sz a) (Init_compound il) m' + | exec_init_compound_struct: forall m b ofs id fl a il m', + exec_init_list m b ofs (fields_of_struct id (Tstruct id fl a) fl 0) il m' -> + exec_init m b ofs (Tstruct id fl a) (Init_compound il) m' + | exec_init_compound_union: forall m b ofs id id1 ty1 fl a i m', + exec_init m b ofs (unroll_composite id (Tunion id (Fcons id1 ty1 fl) a) ty1) i m' -> + exec_init m b ofs (Tunion id (Fcons id1 ty1 fl) a) (Init_compound (Init_cons i Init_nil)) m' with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem -> Prop := | exec_init_array_nil: forall m b ofs ty, -- cgit