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/Cstrategy.v | 625 +++++++++++++++++++++++++++++++++++--------------- 1 file changed, 441 insertions(+), 184 deletions(-) (limited to 'cfrontend/Cstrategy.v') diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 8b66ef9..e088c26 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -49,9 +49,9 @@ Fixpoint simple (a: expr) : Prop := | Eloc _ _ _ => True | Evar _ _ => True | Ederef r _ => simple r - | Efield l1 _ _ => simple l1 + | Efield r _ _ => simple r | Eval _ _ => True - | Evalof l _ => simple l + | Evalof l _ => simple l /\ type_is_volatile (typeof l) = false | Eaddrof l _ => simple l | Eunop _ r1 _ => simple r1 | Ebinop _ r1 r2 _ => simple r1 /\ simple r2 @@ -93,22 +93,22 @@ 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, eval_simple_rvalue (Eval v ty) v | 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 -> + ty = typeof l -> type_is_volatile ty = false -> + 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 -> @@ -151,7 +151,7 @@ Inductive leftcontext: kind -> kind -> (expr -> expr) -> Prop := | lctx_deref: forall k C ty, leftcontext k RV C -> leftcontext k LV (fun x => Ederef (C x) ty) | lctx_field: forall k C f ty, - leftcontext k LV C -> leftcontext k LV (fun x => Efield (C x) f ty) + leftcontext k RV C -> leftcontext k LV (fun x => Efield (C x) f ty) | lctx_rvalof: forall k C ty, leftcontext k LV C -> leftcontext k RV (fun x => Evalof (C x) ty) | lctx_addrof: forall k C ty, @@ -222,6 +222,14 @@ Inductive estep: state -> trace -> state -> Prop := estep (ExprState f r k e m) E0 (ExprState f (Eval v ty) k e m) + | step_rvalof_volatile: forall f C l ty k e m b ofs t v, + leftcontext RV RV C -> + eval_simple_lvalue e m l b ofs -> + deref_loc ge ty m b ofs t v -> + ty = typeof l -> type_is_volatile ty = true -> + estep (ExprState f (C (Evalof l ty)) k e m) + t (ExprState f (C (Eval v ty)) k e m) + | step_condition: forall f C r1 r2 r3 ty k e m v b, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> @@ -229,38 +237,73 @@ Inductive estep: state -> trace -> state -> Prop := estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m) E0 (ExprState f (C (Eparen (if b then r2 else r3) ty)) k e m) - | step_assign: forall f C l r ty k e m b ofs v v' m', + | step_assign: forall f C l r ty k e m b ofs v v' t m', leftcontext RV RV C -> eval_simple_lvalue e m l b ofs -> eval_simple_rvalue e m r v -> sem_cast v (typeof r) (typeof l) = Some v' -> - store_value_of_type (typeof l) m b ofs v' = Some m' -> + assign_loc ge (typeof l) m b ofs v' t m' -> ty = typeof l -> estep (ExprState f (C (Eassign l r ty)) k e m) - E0 (ExprState f (C (Eval v' ty)) k e m') + t (ExprState f (C (Eval v' ty)) k e m') - | step_assignop: forall f C op l r tyres ty k e m b ofs v1 v2 v3 v4 m', + | step_assignop: forall f C op l r tyres ty k e m b ofs v1 v2 v3 v4 t1 t2 m' t, leftcontext RV RV C -> eval_simple_lvalue e m l b ofs -> - load_value_of_type (typeof l) m b ofs = Some v1 -> + deref_loc ge (typeof l) m b ofs t1 v1 -> eval_simple_rvalue e m r v2 -> sem_binary_operation op v1 (typeof l) v2 (typeof r) m = Some v3 -> sem_cast v3 tyres (typeof l) = Some v4 -> - store_value_of_type (typeof l) m b ofs v4 = Some m' -> + assign_loc ge (typeof l) m b ofs v4 t2 m' -> ty = typeof l -> + t = t1 ** t2 -> estep (ExprState f (C (Eassignop op l r tyres ty)) k e m) - E0 (ExprState f (C (Eval v4 ty)) k e m') + t (ExprState f (C (Eval v4 ty)) k e m') - | step_postincr: forall f C id l ty k e m b ofs v1 v2 v3 m', + | step_assignop_stuck: forall f C op l r tyres ty k e m b ofs v1 v2 t, leftcontext RV RV C -> eval_simple_lvalue e m l b ofs -> - load_value_of_type ty m b ofs = Some v1 -> + deref_loc ge (typeof l) m b ofs t v1 -> + eval_simple_rvalue e m r v2 -> + match sem_binary_operation op v1 (typeof l) v2 (typeof r) m with + | None => True + | Some v3 => + match sem_cast v3 tyres (typeof l) with + | None => True + | Some v4 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v4 t2 m') + end + end -> + ty = typeof l -> + estep (ExprState f (C (Eassignop op l r tyres ty)) k e m) + t Stuckstate + + | step_postincr: forall f C id l ty k e m b ofs v1 v2 v3 t1 t2 m' t, + leftcontext RV RV C -> + eval_simple_lvalue e m l b ofs -> + deref_loc ge ty m b ofs t1 v1 -> sem_incrdecr id v1 ty = Some v2 -> sem_cast v2 (typeconv ty) ty = Some v3 -> - store_value_of_type ty m b ofs v3 = Some m' -> + assign_loc ge ty m b ofs v3 t2 m' -> + ty = typeof l -> + t = t1 ** t2 -> + estep (ExprState f (C (Epostincr id l ty)) k e m) + t (ExprState f (C (Eval v1 ty)) k e m') + + | step_postincr_stuck: forall f C id l ty k e m b ofs v1 t, + leftcontext RV RV C -> + eval_simple_lvalue e m l b ofs -> + deref_loc ge ty m b ofs t v1 -> + match sem_incrdecr id v1 ty with + | None => True + | Some v2 => + match sem_cast v2 (typeconv ty) ty with + | None => True + | Some v3 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v3 t2 m') + end + end -> ty = typeof l -> estep (ExprState f (C (Epostincr id l ty)) k e m) - E0 (ExprState f (C (Eval v1 ty)) k e m') + t Stuckstate | step_comma: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> @@ -326,53 +369,37 @@ Proof. Qed. Lemma star_safe: - forall s1 s2 s3, - safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> star Csem.step ge s2 E0 s3) -> - star Csem.step ge s1 E0 s3. + forall s1 s2 t s3, + safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> star Csem.step ge s2 t s3) -> + star Csem.step ge s1 t s3. Proof. intros. eapply star_trans; eauto. apply H1. eapply safe_steps; eauto. auto. Qed. Lemma plus_safe: - forall s1 s2 s3, - safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> plus Csem.step ge s2 E0 s3) -> - plus Csem.step ge s1 E0 s3. + forall s1 s2 t s3, + safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> plus Csem.step ge s2 t s3) -> + plus Csem.step ge s1 t s3. Proof. intros. eapply star_plus_trans; eauto. apply H1. eapply safe_steps; eauto. auto. Qed. -Remark not_stuck_val: - forall e v ty m, - not_stuck ge e (Eval v ty) m. -Proof. - intros; red; intros. inv H; try congruence. subst e'. constructor. -Qed. - -Lemma safe_not_stuck: - forall f a k e m, - safe (ExprState f a k e m) -> - not_stuck ge e a m. -Proof. - intros. exploit H. apply star_refl. intros [[r FIN] | [t [s' STEP]]]. - inv FIN. - inv STEP. - inv H0; auto; apply not_stuck_val. - inv H0; apply not_stuck_val. -Qed. - -Hint Resolve safe_not_stuck. +Require Import Classical. -Lemma safe_not_imm_stuck: - forall k C f a K e m, - safe (ExprState f (C a) K e m) -> - context k RV C -> - not_imm_stuck ge e k a m. +Lemma safe_imm_safe: + forall f C a k e m K, + safe (ExprState f (C a) k e m) -> + context K RV C -> + imm_safe ge e K a m. Proof. - intros. exploit safe_not_stuck; eauto. + intros. destruct (classic (imm_safe ge e K a m)); auto. + destruct (H Stuckstate). + apply star_one. left. econstructor; eauto. + destruct H2 as [r F]. inv F. + destruct H2 as [t [s' S]]. inv S. inv H2. inv H2. Qed. -(** Simple, non-stuck expressions are well-formed with respect to - l-values and r-values. *) +(** Safe expressions are well-formed with respect to l-values and r-values. *) Definition expr_kind (a: expr) : kind := match a with @@ -390,7 +417,7 @@ Proof. Qed. Lemma rred_kind: - forall a m a' m', rred a m a' m' -> expr_kind a = RV. + forall a m t a' m', rred ge a m t a' m' -> expr_kind a = RV. Proof. induction 1; auto. Qed. @@ -407,8 +434,8 @@ Proof. induction 1; intros; simpl; auto. Qed. -Lemma not_imm_stuck_kind: - forall e k a m, not_imm_stuck ge e k a m -> expr_kind a = k. +Lemma imm_safe_kind: + forall e k a m, imm_safe ge e k a m -> expr_kind a = k. Proof. induction 1. auto. @@ -424,10 +451,10 @@ Lemma safe_expr_kind: safe (ExprState f (C a) k e m) -> expr_kind a = from. Proof. - intros. eapply not_imm_stuck_kind. eapply safe_not_imm_stuck; eauto. + intros. eapply imm_safe_kind. eapply safe_imm_safe; eauto. Qed. -(** Painful inversion lemmas on particular states that are not stuck. *) +(** Painful inversion lemmas on particular states that are safe. *) Section INVERSION_LEMMAS. @@ -449,15 +476,16 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := \/ (e!x = None /\ Genv.find_symbol ge x = Some b /\ type_of_global ge b = Some ty) | Ederef (Eval v ty1) ty => exists b, exists ofs, v = Vptr b ofs - | Efield (Eloc b ofs ty1) f ty => + | Efield (Eval v ty1) f ty => + exists b, exists ofs, v = Vptr b ofs /\ match ty1 with - | Tstruct _ fList => exists delta, field_offset f fList = Errors.OK delta - | Tunion _ _ => True + | Tstruct _ fList _ => exists delta, field_offset f fList = Errors.OK delta + | Tunion _ _ _ => True | _ => False end | Eval v ty => False | Evalof (Eloc b ofs ty') ty => - ty' = ty /\ exists v, load_value_of_type ty m b ofs = Some v + ty' = ty /\ exists t, exists v, deref_loc ge ty m b ofs t v | Eunop op (Eval v1 ty1) ty => exists v, sem_unary_operation op v1 ty1 = Some v | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => @@ -467,22 +495,16 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Econdition (Eval v1 ty1) r1 r2 ty => exists b, bool_val v1 ty1 = Some b | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty => - exists v, exists m', - ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ store_value_of_type ty1 m b ofs v = Some m' + exists v, exists m', exists t, + ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m' | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty => - exists v1, exists v, exists v', exists m', - ty = ty1 - /\ load_value_of_type ty1 m b ofs = Some v1 - /\ sem_binary_operation op v1 ty1 v2 ty2 m = Some v - /\ sem_cast v tyres ty1 = Some v' - /\ store_value_of_type ty1 m b ofs v' = Some m' + exists t, exists v1, + ty = ty1 + /\ deref_loc ge ty1 m b ofs t v1 | Epostincr id (Eloc b ofs ty1) ty => - exists v1, exists v2, exists v3, exists m', + exists t, exists v1, ty = ty1 - /\ load_value_of_type ty m b ofs = Some v1 - /\ sem_incrdecr id v1 ty = Some v2 - /\ sem_cast v2 (typeconv ty) ty = Some v3 - /\ store_value_of_type ty m b ofs v3 = Some m' + /\ deref_loc ge ty m b ofs t v1 | Ecomma (Eval v ty1) r2 ty => typeof r2 = ty | Eparen (Eval v1 ty1) ty => @@ -504,21 +526,22 @@ Proof. exists b; auto. exists b; auto. exists b; exists ofs; auto. - exists delta; auto. + exists b; exists ofs; split; auto. exists delta; auto. + exists b; exists ofs; auto. Qed. Lemma rred_invert: - forall r m r' m', rred r m r' m' -> invert_expr_prop r m. + forall r m t r' m', rred ge r m t r' m' -> invert_expr_prop r m. Proof. induction 1; red; auto. - split; auto; exists v; auto. + split; auto; exists t; exists v; auto. exists v; auto. exists v; auto. exists v; auto. exists b; auto. - exists v; exists m'; auto. - exists v1; exists v; exists v'; exists m'; auto. - exists v1; exists v2; exists v3; exists m'; auto. + exists v; exists m'; exists t; auto. + exists t; exists v1; auto. + exists t; exists v1; auto. exists v; auto. Qed. @@ -569,9 +592,9 @@ Proof. red; intros. destruct e1; auto. elim (H0 a m); auto. Qed. -Lemma not_imm_stuck_inv: +Lemma imm_safe_inv: forall k a m, - not_imm_stuck ge e k a m -> + imm_safe ge e k a m -> match a with | Eloc _ _ _ => True | Eval _ _ => True @@ -603,7 +626,7 @@ Lemma safe_inv: | _ => invert_expr_prop a m end. Proof. - intros. eapply not_imm_stuck_inv; eauto. eapply safe_not_imm_stuck; eauto. + intros. eapply imm_safe_inv; eauto. eapply safe_imm_safe; eauto. Qed. End INVERSION_LEMMAS. @@ -619,16 +642,16 @@ Variable m: mem. Lemma eval_simple_steps: (forall a v, eval_simple_rvalue e m a v -> - forall C, context RV RV C -> safe (ExprState f (C a) k e m) -> + forall C, context RV RV C -> star Csem.step ge (ExprState f (C a) k e m) E0 (ExprState f (C (Eval v (typeof a))) k e m)) /\ (forall a b ofs, eval_simple_lvalue e m a b ofs -> - forall C, context LV RV C -> safe (ExprState f (C a) k e m) -> + forall C, context LV RV C -> star Csem.step ge (ExprState f (C a) k e m) E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m)). Proof. -Ltac Steps REC C' := eapply star_safe; eauto; [apply (REC C'); eauto | intros]. +Ltac Steps REC C' := eapply star_trans; [apply (REC C'); eauto | idtac | simpl; reflexivity]. Ltac FinishR := apply star_one; left; apply step_rred; eauto; simpl; try (econstructor; eauto; fail). Ltac FinishL := apply star_one; left; apply step_lred; eauto; simpl; try (econstructor; eauto; fail). @@ -665,14 +688,14 @@ Qed. Lemma eval_simple_rvalue_steps: forall a v, eval_simple_rvalue e m a v -> - forall C, context RV RV C -> safe (ExprState f (C a) k e m) -> + forall C, context RV RV C -> star Csem.step ge (ExprState f (C a) k e m) E0 (ExprState f (C (Eval v (typeof a))) k e m). Proof (proj1 eval_simple_steps). Lemma eval_simple_lvalue_steps: forall a b ofs, eval_simple_lvalue e m a b ofs -> - forall C, context LV RV C -> safe (ExprState f (C a) k e m) -> + forall C, context LV RV C -> star Csem.step ge (ExprState f (C a) k e m) E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m). Proof (proj2 eval_simple_steps). @@ -727,14 +750,16 @@ Ltac StepR REC C' a := exists b; exists Int.zero. intuition. apply esl_var_local; auto. apply esl_var_global; auto. (* field *) - StepL IHa (fun x => C(Efield x f0 ty)) a. - exploit safe_inv. eexact SAFE0. eauto. simpl. case_eq (typeof a); intros; try contradiction. - destruct H0 as [delta OFS]. exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto. + StepR IHa (fun x => C(Efield x f0 ty)) a. + exploit safe_inv. eexact SAFE0. eauto. simpl. + intros [b [ofs [EQ TY]]]. subst v. destruct (typeof a) as []_eqn; try contradiction. + destruct TY as [delta OFS]. exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto. exists b; exists ofs; econstructor; eauto. (* valof *) - StepL IHa (fun x => C(Evalof x ty)) a. - exploit safe_inv. eexact SAFE0. eauto. simpl. intros [TY [v LOAD]]. - exists v; econstructor; eauto. + destruct S. StepL IHa (fun x => C(Evalof x ty)) a. + exploit safe_inv. eexact SAFE0. eauto. simpl. intros [TY [t [v LOAD]]]. + assert (t = E0). inv LOAD; auto. congruence. subst t. + exists v; econstructor; eauto. congruence. (* deref *) StepR IHa (fun x => C(Ederef x ty)) a. exploit safe_inv. eexact SAFE0. eauto. simpl. intros [b [ofs EQ]]. @@ -875,7 +900,7 @@ Hint Resolve contextlist'_head contextlist'_tail. Lemma eval_simple_list_steps: forall rl vl, eval_simple_list' rl vl -> - forall C, contextlist' C -> safe (ExprState f (C rl) k e m) -> + forall C, contextlist' C -> star Csem.step ge (ExprState f (C rl) k e m) E0 (ExprState f (C (rval_list vl rl)) k e m). Proof. @@ -883,9 +908,10 @@ Proof. (* nil *) apply star_refl. (* cons *) - eapply star_safe. eauto. + eapply star_trans. eapply eval_simple_rvalue_steps with (C := fun x => C(Econs x rl)); eauto. - intros. apply IHeval_simple_list' with (C := fun x => C(Econs (Eval v (typeof r)) x)); auto. + apply IHeval_simple_list' with (C := fun x => C(Econs (Eval v (typeof r)) x)); auto. + auto. Qed. Lemma simple_list_can_eval: @@ -926,7 +952,8 @@ Variable m: mem. Definition simple_side_effect (r: expr) : Prop := match r with - | Econdition r1 r2 r3 ty => simple r1 + | Evalof l _ => simple l /\ type_is_volatile (typeof l) = true + | Econdition r1 r2 r3 _ => simple r1 | Eassign l1 r2 _ => simple l1 /\ simple r2 | Eassignop _ l1 r2 _ _ => simple l1 /\ simple r2 | Epostincr _ l1 _ => simple l1 @@ -964,9 +991,11 @@ Ltac Base := right; exists (fun x => x); econstructor; split; [eauto | simpl; auto]. (* field *) - Kind. Rec H LV C (fun x => Efield x f0 ty). + Kind. Rec H RV C (fun x => Efield x f0 ty). (* rvalof *) Kind. Rec H LV C (fun x => Evalof x ty). + destruct (type_is_volatile (typeof l)) as []_eqn. + Base. auto. (* deref *) Kind. Rec H RV C (fun x => Ederef x ty). (* addrof *) @@ -1020,95 +1049,185 @@ End DECOMPOSITION. Lemma estep_simulation: forall S t S', - estep S t S' -> safe S -> plus Csem.step ge S t S'. + estep S t S' -> plus Csem.step ge S t S'. Proof. intros. inv H. (* simple *) exploit eval_simple_rvalue_steps; eauto. simpl; intros STEPS. - exploit star_inv; eauto. intros [[EQ1 EQ2] | A]; auto. - inversion EQ1. rewrite <- H3 in H2; contradiction. + exploit star_inv; eauto. intros [[EQ1 EQ2] | A]; eauto. + inversion EQ1. rewrite <- H2 in H1; contradiction. +(* valof volatile *) + eapply plus_right. + eapply eval_simple_lvalue_steps with (C := fun x => C(Evalof x (typeof l))); eauto. + left. apply step_rred; eauto. econstructor; eauto. auto. (* condition *) - eapply plus_safe; eauto. + eapply plus_right. eapply eval_simple_rvalue_steps with (C := fun x => C(Econdition x r2 r3 ty)); eauto. - intros. apply plus_one. left; apply step_rred; eauto. constructor; auto. + left; apply step_rred; eauto. constructor; auto. auto. (* assign *) - eapply plus_safe; eauto. + eapply star_plus_trans. eapply eval_simple_lvalue_steps with (C := fun x => C(Eassign x r (typeof l))); eauto. - intros. eapply plus_safe; eauto. + eapply plus_right. eapply eval_simple_rvalue_steps with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. - intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto. + left; apply step_rred; eauto. econstructor; eauto. + reflexivity. auto. (* assignop *) - eapply plus_safe; eauto. + eapply star_plus_trans. eapply eval_simple_lvalue_steps with (C := fun x => C(Eassignop op x r tyres (typeof l))); eauto. - intros. eapply plus_safe; eauto. + eapply star_plus_trans. eapply eval_simple_rvalue_steps with (C := fun x => C(Eassignop op (Eloc b ofs (typeof l)) x tyres (typeof l))); eauto. - intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto. + eapply plus_left. + left; apply step_rred; auto. econstructor; eauto. + eapply star_left. + left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. econstructor; eauto. + apply star_one. + left; apply step_rred; auto. econstructor; eauto. + reflexivity. reflexivity. reflexivity. traceEq. +(* assignop stuck *) + eapply star_plus_trans. + eapply eval_simple_lvalue_steps with (C := fun x => C(Eassignop op x r tyres (typeof l))); eauto. + eapply star_plus_trans. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eassignop op (Eloc b ofs (typeof l)) x tyres (typeof l))); eauto. + eapply plus_left. + left; apply step_rred; auto. econstructor; eauto. + destruct (sem_binary_operation op v1 (typeof l) v2 (typeof r) m) as [v3|]_eqn. + eapply star_left. + left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. econstructor; eauto. + apply star_one. + left; eapply step_stuck; eauto. + red; intros. exploit imm_safe_inv; eauto. simpl. intros [v4' [m' [t' [A [B D]]]]]. + rewrite B in H4. eelim H4; eauto. + reflexivity. + apply star_one. + left; eapply step_stuck with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. + red; intros. exploit imm_safe_inv; eauto. simpl. intros [v3 A]. congruence. + reflexivity. + reflexivity. traceEq. (* postincr *) - eapply plus_safe; eauto. + eapply star_plus_trans. + eapply eval_simple_lvalue_steps with (C := fun x => C(Epostincr id x (typeof l))); eauto. + eapply plus_left. + left; apply step_rred; auto. econstructor; eauto. + eapply star_left. + left; apply step_rred with (C := fun x => C (Ecomma (Eassign (Eloc b ofs (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto. + econstructor. instantiate (1 := v2). destruct id; assumption. + eapply star_left. + left; apply step_rred with (C := fun x => C (Ecomma x (Eval v1 (typeof l)) (typeof l))); eauto. + econstructor; eauto. + apply star_one. + left; apply step_rred; auto. econstructor; eauto. + reflexivity. reflexivity. reflexivity. traceEq. +(* postincr stuck *) + eapply star_plus_trans. eapply eval_simple_lvalue_steps with (C := fun x => C(Epostincr id x (typeof l))); eauto. - intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto. + eapply plus_left. + left; apply step_rred; auto. econstructor; eauto. + set (op := match id with Incr => Oadd | Decr => Osub end). + assert (SEM: sem_binary_operation op v1 (typeof l) (Vint Int.one) type_int32s m = + sem_incrdecr id v1 (typeof l)). + destruct id; auto. + destruct (sem_incrdecr id v1 (typeof l)) as [v2|]. + eapply star_left. + left; apply step_rred with (C := fun x => C (Ecomma (Eassign (Eloc b ofs (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto. + econstructor; eauto. + apply star_one. + left; eapply step_stuck with (C := fun x => C (Ecomma x (Eval v1 (typeof l)) (typeof l))); eauto. + red; intros. exploit imm_safe_inv; eauto. simpl. intros [v3 [m' [t' [A [B D]]]]]. + rewrite B in H3. eelim H3; eauto. + reflexivity. + apply star_one. + left; eapply step_stuck with (C := fun x => C (Ecomma (Eassign (Eloc b ofs (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto. + red; intros. exploit imm_safe_inv; eauto. simpl. intros [v2 A]. congruence. + reflexivity. + traceEq. (* comma *) - eapply plus_safe; eauto. + eapply plus_right. eapply eval_simple_rvalue_steps with (C := fun x => C(Ecomma x r2 (typeof r2))); eauto. - intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto. + left; apply step_rred; eauto. econstructor; eauto. auto. (* paren *) - eapply plus_safe; eauto. + eapply plus_right; eauto. eapply eval_simple_rvalue_steps with (C := fun x => C(Eparen x ty)); eauto. - intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto. + left; apply step_rred; eauto. econstructor; eauto. auto. (* call *) exploit eval_simple_list_implies; eauto. intros [vl' [A B]]. - eapply plus_safe; eauto. + eapply star_plus_trans. eapply eval_simple_rvalue_steps with (C := fun x => C(Ecall x rargs ty)); eauto. - intros. eapply plus_safe; eauto. + eapply plus_right. eapply eval_simple_list_steps with (C := fun x => C(Ecall (Eval vf (typeof rf)) x ty)); eauto. eapply contextlist'_intro with (rl0 := Enil); auto. - intros. apply plus_one; left; apply Csem.step_call; eauto. - econstructor; eauto. + left; apply Csem.step_call; eauto. econstructor; eauto. + traceEq. auto. Qed. Lemma can_estep: forall f a k e m, safe (ExprState f a k e m) -> match a with Eval _ _ => False | _ => True end -> - exists S, estep (ExprState f a k e m) E0 S. + exists t, exists S, estep (ExprState f a k e m) t S. Proof. intros. destruct (decompose_topexpr f k e m a H) as [A | [C [b [P [Q R]]]]]. (* simple expr *) exploit (simple_can_eval f k e m a RV (fun x => x)); auto. intros [v P]. - econstructor; eapply step_expr; eauto. + econstructor; econstructor; eapply step_expr; eauto. (* side effect *) clear H0. subst a. red in Q. destruct b; try contradiction. +(* valof volatile *) + destruct Q. + exploit (simple_can_eval_lval f k e m b (fun x => C(Evalof x ty))); eauto. + intros [b1 [ofs [E1 S1]]]. + exploit safe_inv. eexact S1. eauto. simpl. intros [A [t [v B]]]. + econstructor; econstructor; eapply step_rvalof_volatile; eauto. congruence. (* condition *) exploit (simple_can_eval_rval f k e m b1 (fun x => C(Econdition x b2 b3 ty))); eauto. intros [v1 [E1 S1]]. exploit safe_inv. eexact S1. eauto. simpl. intros [b BV]. - econstructor. eapply step_condition; eauto. + econstructor; econstructor. eapply step_condition; eauto. (* assign *) destruct Q. exploit (simple_can_eval_lval f k e m b1 (fun x => C(Eassign x b2 ty))); eauto. intros [b [ofs [E1 S1]]]. exploit (simple_can_eval_rval f k e m b2 (fun x => C(Eassign (Eloc b ofs (typeof b1)) x ty))); eauto. intros [v [E2 S2]]. - exploit safe_inv. eexact S2. eauto. simpl. intros [v' [m' [A [B D]]]]. - econstructor; eapply step_assign; eauto. + exploit safe_inv. eexact S2. eauto. simpl. intros [v' [m' [t [A [B D]]]]]. + econstructor; econstructor; eapply step_assign; eauto. (* assignop *) destruct Q. exploit (simple_can_eval_lval f k e m b1 (fun x => C(Eassignop op x b2 tyres ty))); eauto. intros [b [ofs [E1 S1]]]. exploit (simple_can_eval_rval f k e m b2 (fun x => C(Eassignop op (Eloc b ofs (typeof b1)) x tyres ty))); eauto. intros [v [E2 S2]]. - exploit safe_inv. eexact S2. eauto. simpl. intros [v1 [v2 [v3 [m' [A [B [D [E F]]]]]]]]. - econstructor; eapply step_assignop; eauto. + exploit safe_inv. eexact S2. eauto. simpl. intros [t1 [v1 [A B]]]. + destruct (sem_binary_operation op v1 (typeof b1) v (typeof b2) m) as [v3|]_eqn. + destruct (sem_cast v3 tyres (typeof b1)) as [v4|]_eqn. + destruct (classic (exists t2, exists m', assign_loc ge (typeof b1) m b ofs v4 t2 m')). + destruct H2 as [t2 [m' D]]. + econstructor; econstructor; eapply step_assignop; eauto. + econstructor; econstructor; eapply step_assignop_stuck; eauto. + rewrite Heqo. rewrite Heqo0. intros; red; intros. elim H2. exists t2; exists m'; auto. + econstructor; econstructor; eapply step_assignop_stuck; eauto. + rewrite Heqo. rewrite Heqo0. auto. + econstructor; econstructor; eapply step_assignop_stuck; eauto. + rewrite Heqo. auto. (* postincr *) exploit (simple_can_eval_lval f k e m b (fun x => C(Epostincr id x ty))); eauto. intros [b1 [ofs [E1 S1]]]. - exploit safe_inv. eexact S1. eauto. simpl. intros [v1 [v2 [v3 [m' [A [B [D [E F]]]]]]]]. - econstructor; eapply step_postincr; eauto. + exploit safe_inv. eexact S1. eauto. simpl. intros [t [v1 [A B]]]. + destruct (sem_incrdecr id v1 ty) as [v2|]_eqn. + destruct (sem_cast v2 (typeconv ty) ty) as [v3|]_eqn. + destruct (classic (exists t2, exists m', assign_loc ge ty m b1 ofs v3 t2 m')). + destruct H0 as [t2 [m' D]]. + econstructor; econstructor; eapply step_postincr; eauto. + econstructor; econstructor; eapply step_postincr_stuck; eauto. + rewrite Heqo. rewrite Heqo0. intros; red; intros. elim H0. exists t2; exists m'; congruence. + econstructor; econstructor; eapply step_postincr_stuck; eauto. + rewrite Heqo. rewrite Heqo0. auto. + econstructor; econstructor; eapply step_postincr_stuck; eauto. + rewrite Heqo. auto. (* comma *) exploit (simple_can_eval_rval f k e m b1 (fun x => C(Ecomma x b2 ty))); eauto. intros [v1 [E1 S1]]. exploit safe_inv. eexact S1. eauto. simpl. intros EQ. - econstructor; eapply step_comma; eauto. + econstructor; econstructor; eapply step_comma; eauto. (* call *) destruct Q. exploit (simple_can_eval_rval f k e m b (fun x => C(Ecall x rargs ty))); eauto. @@ -1122,19 +1241,19 @@ Proof. apply (eval_simple_list_steps f k e m rargs vl E2 C'); auto. simpl. intros X. exploit X. eapply rval_list_all_values. intros [tyargs [tyres [fd [vargs [P [Q [U V]]]]]]]. - econstructor; eapply step_call; eauto. eapply can_eval_simple_list; eauto. + econstructor; econstructor; eapply step_call; eauto. eapply can_eval_simple_list; eauto. (* paren *) exploit (simple_can_eval_rval f k e m b (fun x => C(Eparen x ty))); eauto. intros [v1 [E1 S1]]. exploit safe_inv. eexact S1. eauto. simpl. intros [v CAST]. - econstructor; eapply step_paren; eauto. + econstructor; econstructor; eapply step_paren; eauto. Qed. (** Simulation for all states *) Theorem step_simulation: forall S1 t S2, - step S1 t S2 -> safe S1 -> plus Csem.step ge S1 t S2. + step S1 t S2 -> plus Csem.step ge S1 t S2. Proof. intros. inv H. apply estep_simulation; auto. @@ -1150,16 +1269,19 @@ Proof. auto. right. destruct STEP. (* 2. Expression step. *) - assert (exists S', estep S E0 S'). + assert (exists t, exists S', estep S t S'). inv H0. (* lred *) - eapply can_estep; eauto. inv H3; auto. + eapply can_estep; eauto. inv H2; auto. (* rred *) - eapply can_estep; eauto. inv H3; auto. inv H1; auto. + eapply can_estep; eauto. inv H2; auto. inv H1; auto. (* callred *) - eapply can_estep; eauto. inv H3; auto. inv H1; auto. - destruct H1 as [S'' ESTEP]. - exists E0; exists S''; left; auto. + eapply can_estep; eauto. inv H2; auto. inv H1; auto. + (* stuck *) + exploit (H Stuckstate). apply star_one. left. econstructor; eauto. + intros [[r F] | [t [S' R]]]. inv F. inv R. inv H0. inv H0. + destruct H1 as [t' [S'' ESTEP]]. + exists t'; exists S''; left; auto. (* 3. Other step. *) exists t; exists S'; right; auto. Qed. @@ -1173,22 +1295,145 @@ Definition semantics (p: program) := (** This semantics is receptive to changes in events. *) -Lemma semantics_receptive: - forall p, receptive (semantics p). +Remark deref_loc_trace: + forall F V (ge: Genv.t F V) ty m b ofs t v, + deref_loc ge ty m b ofs t v -> + match t with nil => True | ev :: nil => True | _ => False end. +Proof. + intros. inv H; simpl; auto. inv H2; simpl; auto. +Qed. + +Remark deref_loc_receptive: + forall F V (ge: Genv.t F V) ty m b ofs ev1 t1 v ev2, + deref_loc ge ty m b ofs (ev1 :: t1) v -> + match_traces ge (ev1 :: nil) (ev2 :: nil) -> + t1 = nil /\ exists v', deref_loc ge ty m b ofs (ev2 :: nil) v'. +Proof. + intros. + assert (t1 = nil). exploit deref_loc_trace; eauto. destruct t1; simpl; tauto. + inv H. exploit volatile_load_receptive; eauto. intros [v' A]. + split; auto; exists v'; econstructor; eauto. +Qed. + +Remark assign_loc_trace: + forall F V (ge: Genv.t F V) ty m b ofs t v m', + assign_loc ge ty m b ofs v t m' -> + match t with nil => True | ev :: nil => output_event ev | _ => False end. +Proof. + intros. inv H; simpl; auto. inv H2; simpl; auto. +Qed. + +Remark assign_loc_receptive: + forall F V (ge: Genv.t F V) ty m b ofs ev1 t1 v m' ev2, + assign_loc ge ty m b ofs v (ev1 :: t1) m' -> + match_traces ge (ev1 :: nil) (ev2 :: nil) -> + ev1 :: t1 = ev2 :: nil. +Proof. + intros. + assert (t1 = nil). exploit assign_loc_trace; eauto. destruct t1; simpl; tauto. + inv H. eapply volatile_store_receptive; eauto. +Qed. + +Lemma semantics_strongly_receptive: + forall p, strongly_receptive (semantics p). Proof. intros. constructor; simpl; intros. (* receptiveness *) - assert (t1 = E0 -> exists s2, step (Genv.globalenv p) s t2 s2). - intros. subst. inv H0. exists s1; auto. inversion H; subst. - inv H2; auto. - inv H2; auto. + inv H1. + (* valof volatile *) + exploit deref_loc_receptive; eauto. intros [A [v' B]]. + econstructor; econstructor. left; eapply step_rvalof_volatile; eauto. + (* assign *) + exploit assign_loc_receptive; eauto. intro EQ; rewrite EQ in H. + econstructor; econstructor; eauto. + (* assignop *) + destruct t0 as [ | ev0 t0]; simpl in H10. + subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H. + econstructor; econstructor; eauto. + inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0. + destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|]_eqn. + destruct (sem_cast v3' tyres (typeof l)) as [v4'|]_eqn. + destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v4' t2' m'')). + destruct H1 as [t2' [m'' P]]. + econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. + econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. + rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t0; exists m'0; auto. + econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. + rewrite Heqo; rewrite Heqo0; auto. + econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. + rewrite Heqo; auto. + (* assignop stuck *) + exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1. + destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|]_eqn. + destruct (sem_cast v3' tyres (typeof l)) as [v4'|]_eqn. + destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v4' t2' m'')). + destruct H1 as [t2' [m'' P]]. + econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. + econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. + rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t2; exists m'; auto. + econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. + rewrite Heqo; rewrite Heqo0; auto. + econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. + rewrite Heqo; auto. + (* postincr *) + destruct t0 as [ | ev0 t0]; simpl in H9. + subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H. + econstructor; econstructor; eauto. + inv H9. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0. + destruct (sem_incrdecr id v1' (typeof l)) as [v2'|]_eqn. + destruct (sem_cast v2' (typeconv (typeof l)) (typeof l)) as [v3'|]_eqn. + destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v3' t2' m'')). + destruct H1 as [t2' [m'' P]]. + econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. + econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. + rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t0; exists m'0; auto. + econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. + rewrite Heqo; rewrite Heqo0; auto. + econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. + rewrite Heqo; auto. + (* postincr stuck *) + exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1. + destruct (sem_incrdecr id v1' (typeof l)) as [v2'|]_eqn. + destruct (sem_cast v2' (typeconv (typeof l)) (typeof l)) as [v3'|]_eqn. + destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v3' t2' m'')). + destruct H1 as [t2' [m'' P]]. + econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. + econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. + rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t2; exists m'; auto. + econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. + rewrite Heqo; rewrite Heqo0; auto. + econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. + rewrite Heqo; auto. + (* external calls *) + inv H1. + exploit external_call_trace_length; eauto. destruct t1; simpl; intros. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. - exists (Returnstate vres2 k m2). right; econstructor; eauto. -(* trace length *) - inv H. - inv H0; simpl; omega. - inv H0; simpl; try omega. eapply external_call_trace_length; eauto. + exists (Returnstate vres2 k m2); exists E0; right; econstructor; eauto. + omegaContradiction. +(* well-behaved traces *) + red; intros. inv H; inv H0; simpl; auto. + (* valof volatile *) + exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto. + (* assign *) + exploit assign_loc_trace; eauto. destruct t; auto. destruct t; simpl; tauto. + (* assignop *) + exploit deref_loc_trace; eauto. exploit assign_loc_trace; eauto. + destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. + destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. + tauto. + (* assignop stuck *) + exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto. + (* postincr *) + exploit deref_loc_trace; eauto. exploit assign_loc_trace; eauto. + destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. + destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. + tauto. + (* postincr stuck *) + exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto. + (* external calls *) + exploit external_call_trace_length; eauto. + destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction. Qed. (** The main simulation result. *) @@ -1200,8 +1445,6 @@ Proof. apply backward_simulation_plus with (match_states := fun (S1 S2: state) => S1 = S2); simpl. (* symbols *) auto. -(* trace length *) - intros. eapply sr_traces. apply semantics_receptive. simpl. eauto. (* initial states exist *) intros. exists s1; auto. (* initial states match *) @@ -1269,11 +1512,19 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := | eval_var: forall e m x ty, eval_expr e m LV (Evar x ty) E0 m (Evar x ty) | eval_field: forall e m a t m' a' f ty, - eval_expr e m LV a t m' a' -> + eval_expr e m RV a t m' a' -> eval_expr e m LV (Efield a f ty) t m' (Efield a' f ty) | eval_valof: forall e m a t m' a' ty, + type_is_volatile (typeof a) = false -> eval_expr e m LV a t m' a' -> eval_expr e m RV (Evalof a ty) t m' (Evalof a' ty) + | eval_valof_volatile: forall e m a t1 m' a' ty b ofs t2 v, + type_is_volatile (typeof a) = true -> + eval_expr e m LV a t1 m' a' -> + eval_simple_lvalue ge e m' a' b ofs -> + deref_loc ge (typeof a) m' b ofs t2 v -> + ty = typeof a -> + eval_expr e m RV (Evalof a ty) (t1 ** t2) m' (Eval v ty) | eval_deref: forall e m a t m' a' ty, eval_expr e m RV a t m' a' -> eval_expr e m LV (Ederef a ty) t m' (Ederef a' ty) @@ -1297,34 +1548,34 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty) | eval_sizeof: forall e m ty' ty, eval_expr e m RV (Esizeof ty' ty) E0 m (Esizeof ty' ty) - | eval_assign: forall e m l r ty t1 m1 l' t2 m2 r' b ofs v v' m3, + | eval_assign: forall e m l r ty t1 m1 l' t2 m2 r' b ofs v v' t3 m3, eval_expr e m LV l t1 m1 l' -> eval_expr e m1 RV r t2 m2 r' -> eval_simple_lvalue ge e m2 l' b ofs -> eval_simple_rvalue ge e m2 r' v -> sem_cast v (typeof r) (typeof l) = Some v' -> - store_value_of_type (typeof l) m2 b ofs v' = Some m3 -> + assign_loc ge (typeof l) m2 b ofs v' t3 m3 -> ty = typeof l -> - eval_expr e m RV (Eassign l r ty) (t1**t2) m3 (Eval v' ty) + eval_expr e m RV (Eassign l r ty) (t1**t2**t3) m3 (Eval v' ty) | eval_assignop: forall e m op l r tyres ty t1 m1 l' t2 m2 r' b ofs - v1 v2 v3 v4 m3, + v1 v2 v3 v4 t3 t4 m3, eval_expr e m LV l t1 m1 l' -> eval_expr e m1 RV r t2 m2 r' -> eval_simple_lvalue ge e m2 l' b ofs -> - load_value_of_type (typeof l) m2 b ofs = Some v1 -> + deref_loc ge (typeof l) m2 b ofs t3 v1 -> eval_simple_rvalue ge e m2 r' v2 -> sem_binary_operation op v1 (typeof l) v2 (typeof r) m2 = Some v3 -> sem_cast v3 tyres (typeof l) = Some v4 -> - store_value_of_type (typeof l) m2 b ofs v4 = Some m3 -> + assign_loc ge (typeof l) m2 b ofs v4 t4 m3 -> ty = typeof l -> - eval_expr e m RV (Eassignop op l r tyres ty) (t1**t2) m3 (Eval v4 ty) - | eval_postincr: forall e m id l ty t m1 l' b ofs v1 v2 v3 m2, - eval_expr e m LV l t m1 l' -> + eval_expr e m RV (Eassignop op l r tyres ty) (t1**t2**t3**t4) m3 (Eval v4 ty) + | eval_postincr: forall e m id l ty t1 m1 l' b ofs v1 v2 v3 m2 t2 t3, + eval_expr e m LV l t1 m1 l' -> eval_simple_lvalue ge e m1 l' b ofs -> - load_value_of_type ty m1 b ofs = Some v1 -> + deref_loc ge ty m1 b ofs t2 v1 -> sem_incrdecr id v1 ty = Some v2 -> sem_cast v2 (typeconv ty) ty = Some v3 -> - store_value_of_type ty m1 b ofs v3 = Some m2 -> + assign_loc ge ty m1 b ofs v3 t3 m2 -> ty = typeof l -> - eval_expr e m RV (Epostincr id l ty) t m2 (Eval v1 ty) + eval_expr e m RV (Epostincr id l ty) (t1**t2**t3) m2 (Eval v1 ty) | eval_comma: forall e m r1 r2 ty t1 m1 r1' v1 t2 m2 r2', eval_expr e m RV r1 t1 m1 r1' -> eval_simple_rvalue ge e m1 r1' v1 -> @@ -1472,7 +1723,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := | eval_funcall_internal: forall m f vargs t e m1 m2 m3 out vres m4, list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> - bind_parameters e m1 f.(fn_params) vargs m2 -> + bind_parameters ge e m1 f.(fn_params) vargs m2 -> exec_stmt e m2 f.(fn_body) t m3 out -> outcome_result_value out f.(fn_return) vres -> Mem.free_list m3 (blocks_of_env e) = Some m4 -> @@ -1497,7 +1748,7 @@ Combined Scheme bigstep_induction from CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := | evalinf_field: forall e m a t f ty, - evalinf_expr e m LV a t -> + evalinf_expr e m RV a t -> evalinf_expr e m LV (Efield a f ty) t | evalinf_valof: forall e m a t ty, evalinf_expr e m LV a t -> @@ -1677,7 +1928,7 @@ with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop := | evalinf_funcall_internal: forall m f vargs t e m1 m2, list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> - bind_parameters e m1 f.(fn_params) vargs m2 -> + bind_parameters ge e m1 f.(fn_params) vargs m2 -> execinf_stmt e m2 f.(fn_body) t -> evalinf_funcall m (Internal f) vargs t. @@ -1780,9 +2031,16 @@ Proof. eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. simpl; intuition; eauto. (* valof *) - exploit (H0 (fun x => C(Evalof x ty))). + exploit (H1 (fun x => C(Evalof x ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. - simpl; intuition; eauto. + simpl; intuition; eauto. congruence. +(* valof volatile *) + exploit (H1 (fun x => C(Evalof x ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + simpl; intuition. + eapply star_right. eexact D. + left. eapply step_rvalof_volatile; eauto. rewrite H4; eauto. congruence. congruence. + traceEq. (* deref *) exploit (H0 (fun x => C(Ederef x ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. @@ -1825,7 +2083,7 @@ Proof. simpl; intuition. eapply star_trans. eexact D. eapply star_right. eexact G. - left. eapply step_assign; eauto. congruence. congruence. congruence. + left. eapply step_assign; eauto. congruence. rewrite B; eauto. congruence. reflexivity. traceEq. (* assignop *) exploit (H0 (fun x => C(Eassignop op x r tyres ty))). @@ -1836,7 +2094,7 @@ Proof. eapply star_trans. eexact D. eapply star_right. eexact G. left. eapply step_assignop; eauto. - rewrite B; eauto. rewrite B; rewrite F; eauto. congruence. congruence. congruence. + rewrite B; eauto. rewrite B; rewrite F; eauto. congruence. rewrite B; eauto. congruence. reflexivity. traceEq. (* postincr *) exploit (H0 (fun x => C(Epostincr id x ty))). @@ -2113,16 +2371,15 @@ Proof. (* Out_normal *) assert (fn_return f = Tvoid /\ vres = Vundef). destruct (fn_return f); auto || contradiction. - destruct H7. subst vres. right; apply step_skip_call; auto. + destruct H7 as [P Q]. subst vres. right; eapply step_skip_call; eauto. (* Out_return None *) assert (fn_return f = Tvoid /\ vres = Vundef). destruct (fn_return f); auto || contradiction. - destruct H8. subst vres. + destruct H8 as [P Q]. subst vres. rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7. right; apply step_return_0; auto. (* Out_return Some *) - destruct H4. - rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7. + destruct H4. rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7. right; eapply step_return_2; eauto. reflexivity. traceEq. @@ -2510,7 +2767,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - type_of_fundef f = Tfunction Tnil (Tint I32 Signed) -> + type_of_fundef f = Tfunction Tnil type_int32s -> eval_funcall ge m0 f nil t m1 (Vint r) -> bigstep_program_terminates p t r. @@ -2520,7 +2777,7 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - type_of_fundef f = Tfunction Tnil (Tint I32 Signed) -> + type_of_fundef f = Tfunction Tnil type_int32s -> evalinf_funcall ge m0 f nil t -> bigstep_program_diverges p t. -- cgit v1.2.3