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/Cshmgenproof.v | 519 +++++++++++++++++++++++++++++++---------------- 1 file changed, 344 insertions(+), 175 deletions(-) (limited to 'cfrontend/Cshmgenproof.v') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 0f7810d..1089b6b 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -32,27 +32,24 @@ Require Import Cshmgen. (** * Properties of operations over types *) -Remark type_of_chunk_of_type: - forall ty chunk, - chunk_of_type ty = OK chunk -> - type_of_chunk chunk = typ_of_type ty. +Remark type_of_kind_of_type: + forall t k, + var_kind_of_type t = OK k -> type_of_kind k = typ_of_type t. Proof. - intros. unfold chunk_of_type in H. destruct ty; simpl in H; try monadInv H. - destruct i; destruct s; monadInv H; reflexivity. - destruct f; monadInv H; reflexivity. - reflexivity. + intros. destruct t; try (monadInv H); auto. + destruct i; destruct s; monadInv H; auto. + destruct f; monadInv H; auto. Qed. Remark transl_params_types: forall p tp, - transl_params p = OK tp -> - map type_of_chunk (map param_chunk tp) = typlist_of_typelist (type_of_params p). + transl_vars p = OK tp -> + map type_of_kind (map variable_kind tp) = typlist_of_typelist (type_of_params p). Proof. induction p; simpl; intros. inv H. auto. - destruct a as [id ty]. generalize H; clear H. case_eq (chunk_of_type ty); intros. - monadInv H0. simpl. f_equal; auto. apply type_of_chunk_of_type; auto. - inv H0. + destruct a as [id ty]. destruct (var_kind_of_type ty) as []_eqn; monadInv H. + simpl. f_equal; auto. apply type_of_kind_of_type; auto. Qed. Lemma transl_fundef_sig1: @@ -93,13 +90,24 @@ Proof. destruct f; congruence. Qed. +Lemma var_kind_by_reference: + forall ty vk, + access_mode ty = By_reference \/ access_mode ty = By_copy -> + var_kind_of_type ty = OK vk -> + vk = Varray (Csyntax.sizeof ty) (Csyntax.alignof ty). +Proof. + intros ty vk; destruct ty; simpl; try intuition congruence. + destruct i; try congruence; destruct s; intuition congruence. + destruct f; intuition congruence. +Qed. + Lemma sizeof_var_kind_of_type: forall ty vk, var_kind_of_type ty = OK vk -> Csharpminor.sizeof vk = Csyntax.sizeof ty. Proof. intros ty vk. - assert (sizeof (Varray (Csyntax.sizeof ty)) = Csyntax.sizeof ty). + assert (sizeof (Varray (Csyntax.sizeof ty) (Csyntax.alignof ty)) = Csyntax.sizeof ty). simpl. rewrite Zmax_spec. apply zlt_false. generalize (Csyntax.sizeof_pos ty). omega. destruct ty; try (destruct i; try destruct s); try (destruct f); @@ -107,8 +115,8 @@ Proof. Qed. Remark cast_int_int_normalized: - forall sz si chunk n, - access_mode (Tint sz si) = By_value chunk -> + forall sz si a chunk n, + access_mode (Tint sz si a) = By_value chunk -> val_normalized (Vint (cast_int_int sz si n)) chunk. Proof. unfold access_mode, cast_int_int, val_normalized; intros. destruct sz. @@ -119,11 +127,12 @@ Proof. rewrite Int.sign_ext_idem; auto. compute; auto. rewrite Int.zero_ext_idem; auto. compute; auto. inv H. auto. + inv H. destruct (Int.eq n Int.zero); auto. Qed. Remark cast_float_float_normalized: - forall sz chunk n, - access_mode (Tfloat sz) = By_value chunk -> + forall sz a chunk n, + access_mode (Tfloat sz a) = By_value chunk -> val_normalized (Vfloat (cast_float_float sz n)) chunk. Proof. unfold access_mode, cast_float_float, val_normalized; intros. @@ -154,6 +163,16 @@ Proof. functional inversion H2; subst. eapply cast_float_float_normalized; eauto. functional inversion H2; subst. eapply cast_float_float_normalized; eauto. functional inversion H2; subst. eapply cast_int_int_normalized; eauto. + assert (chunk = Mint8unsigned). + functional inversion H2; subst; simpl in H0; try congruence. + subst chunk. destruct (Int.eq i Int.zero); red; auto. + assert (chunk = Mint8unsigned). + functional inversion H2; subst; simpl in H0; try congruence. + subst chunk. red; auto. + functional inversion H2; subst. simpl in H0. inv H0. red; auto. + functional inversion H2; subst. simpl in H0. inv H0. red; auto. + functional inversion H2; subst. simpl in H0. congruence. + functional inversion H2; subst. simpl in H0. congruence. functional inversion H5; subst. simpl in H0. congruence. Qed. @@ -213,14 +232,6 @@ Proof. inv H0. rewrite (IHl1 _ _ _ H H1). auto. Qed. -Lemma transl_params_names: - forall vars tvars, - transl_params vars = OK tvars -> - List.map param_name tvars = var_names vars. -Proof. - exact (map_partial_names _ _ chunk_of_type). -Qed. - Lemma transl_vars_names: forall vars tvars, transl_vars vars = OK tvars -> @@ -232,13 +243,13 @@ Qed. Lemma transl_names_norepet: forall params vars sg tparams tvars temps body, list_norepet (var_names params ++ var_names vars) -> - transl_params params = OK tparams -> + transl_vars params = OK tparams -> transl_vars vars = OK tvars -> let f := Csharpminor.mkfunction sg tparams tvars temps body in list_norepet (fn_params_names f ++ fn_vars_names f). Proof. - intros. unfold fn_params_names, fn_vars_names, f. simpl. - rewrite (transl_params_names _ _ H0). + intros. unfold fn_params_names, fn_vars_names; simpl. + rewrite (transl_vars_names _ _ H0). rewrite (transl_vars_names _ _ H1). auto. Qed. @@ -251,33 +262,15 @@ Proof. exact (map_partial_append _ _ var_kind_of_type). Qed. -Lemma transl_params_vars: - forall params tparams, - transl_params params = OK tparams -> - transl_vars params = - OK (List.map (fun id_chunk => (fst id_chunk, Vscalar (snd id_chunk))) tparams). -Proof. - induction params; intro tparams; simpl. - intros. inversion H. reflexivity. - destruct a as [id x]. - unfold chunk_of_type. caseEq (access_mode x); try congruence. - intros chunk AM. - caseEq (transl_params params); simpl; intros; try congruence. - inv H0. - rewrite (var_kind_by_value _ _ AM). - rewrite (IHparams _ H). reflexivity. -Qed. - Lemma transl_fn_variables: forall params vars sg tparams tvars temps body, - transl_params params = OK tparams -> + transl_vars params = OK tparams -> transl_vars vars = OK tvars -> let f := Csharpminor.mkfunction sg tparams tvars temps body in transl_vars (params ++ vars) = OK (fn_variables f). Proof. intros. - generalize (transl_params_vars _ _ H); intro. - rewrite (transl_vars_append _ _ _ _ H1 H0). + rewrite (transl_vars_append _ _ _ _ H H0). reflexivity. Qed. @@ -300,16 +293,20 @@ Lemma transl_expr_lvalue: (exists tb, transl_lvalue a = OK tb /\ make_load tb (typeof a) = OK ta). Proof. - intros. inversion H; subst; clear H; simpl in H0. + intros until ta; intros EVAL TR. inv EVAL. + (* var local *) left; exists id; exists ty; auto. + (* var global *) left; exists id; exists ty; auto. - monadInv H0. right. exists x; split; auto. - rewrite H2 in H0. monadInv H0. right. - exists (Ebinop Oadd x (make_intconst (Int.repr x0))). split; auto. - simpl. rewrite H2. rewrite EQ. rewrite EQ1. auto. - rewrite H2 in H0. monadInv H0. right. - exists x; split; auto. - simpl. rewrite H2. auto. + (* deref *) + monadInv TR. right. exists x; split; auto. + (* field struct *) + simpl in TR. rewrite H0 in TR. monadInv TR. + right. econstructor; split. simpl. rewrite H0. + rewrite EQ; rewrite EQ1; simpl; eauto. auto. + (* field union *) + simpl in TR. rewrite H0 in TR. monadInv TR. + right. econstructor; split. simpl. rewrite H0. rewrite EQ; simpl; eauto. auto. Qed. (** Properties of labeled statements *) @@ -389,6 +386,7 @@ Proof. destruct si; eauto with cshm. destruct si; eauto with cshm. auto. + econstructor. eauto. simpl. destruct (Int.eq n Int.zero); auto. Qed. Lemma make_cast_float_correct: @@ -420,7 +418,19 @@ Proof. rewrite H2. auto with cshm. (* float -> int *) rewrite H2. eauto with cshm. - (* void *) + (* int/pointer -> bool *) + rewrite H2. econstructor; eauto. simpl. destruct (Int.eq i Int.zero); auto. + rewrite H2. econstructor; eauto. + (* float -> bool *) + rewrite H2. econstructor; eauto with cshm. + simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq. rewrite H7; auto. + rewrite H2. econstructor; eauto with cshm. + simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq. rewrite H7; auto. + (* struct -> struct *) + rewrite H2. auto. + (* union -> union *) + rewrite H2. auto. + (* any -> void *) rewrite H5. auto. Qed. @@ -439,6 +449,10 @@ Proof. intros. functional inversion H0; subst; simpl. exists (Vint n); split; auto. exists (Vint n); split; auto. + exists (Vint n); split; auto. + exists (Vint n); split; auto. + exists (Vptr b0 ofs); split; auto. constructor. + exists (Vptr b0 ofs); split; auto. constructor. exists (Vptr b0 ofs); split; auto. constructor. exists (Vptr b0 ofs); split; auto. constructor. rewrite <- Float.cmp_ne_eq. @@ -670,31 +684,128 @@ Lemma make_load_correct: forall addr ty code b ofs v e le m, make_load addr ty = OK code -> eval_expr ge e le m addr (Vptr b ofs) -> - load_value_of_type ty m b ofs = Some v -> + deref_loc ge ty m b ofs E0 v -> + type_is_volatile ty = false -> eval_expr ge e le m code v. Proof. - unfold make_load, load_value_of_type. - intros until m; intros MKLOAD EVEXP LDVAL. - destruct (access_mode ty); inversion MKLOAD. - (* access_mode ty = By_value m *) - apply eval_Eload with (Vptr b ofs); auto. - (* access_mode ty = By_reference *) - subst code. inversion LDVAL. auto. + unfold make_load; intros until m; intros MKLOAD EVEXP DEREF NONVOL. + inv DEREF. + (* nonvolatile scalar *) + rewrite H in MKLOAD. inv MKLOAD. apply eval_Eload with (Vptr b ofs); auto. + (* volatile scalar *) + congruence. + (* by reference *) + rewrite H in MKLOAD. inv MKLOAD. auto. + (* by copy *) + rewrite H in MKLOAD. inv MKLOAD. auto. +Qed. + +Lemma make_vol_load_correct: + forall id addr ty code b ofs t v e le m f k, + make_vol_load id addr ty = OK code -> + eval_expr ge e le m addr (Vptr b ofs) -> + deref_loc ge ty m b ofs t v -> + type_is_volatile ty = true -> + step ge (State f code k e le m) t (State f Sskip k e (PTree.set id v le) m). +Proof. + unfold make_vol_load; intros until k; intros MKLOAD EVEXP DEREF VOL. + inv DEREF. + (* nonvolatile scalar *) + congruence. +(** + rewrite H in MKLOAD. inv MKLOAD. + change (PTree.set id v le) with (Cminor.set_optvar (Some id) v le). + econstructor. constructor. eauto. constructor. constructor; auto. constructor; auto. +*) + (* volatile scalar *) + rewrite H in MKLOAD. inv MKLOAD. + change (PTree.set id v le) with (Cminor.set_optvar (Some id) v le). + econstructor. constructor. eauto. constructor. constructor; auto. + (* by reference *) + rewrite H in MKLOAD. inv MKLOAD. constructor; auto. + (* by copy *) + rewrite H in MKLOAD. inv MKLOAD. constructor; auto. +Qed. + +Remark capped_alignof_divides: + forall ty n, + (alignof ty | n) -> (Zmin (alignof ty) 4 | n). +Proof. + intros. generalize (alignof_1248 ty). + intros [A|[A|[A|A]]]; rewrite A in *; auto. + apply Zdivides_trans with 8; auto. exists 2; auto. Qed. +Remark capped_alignof_124: + forall ty, + Zmin (alignof ty) 4 = 1 \/ Zmin (alignof ty) 4 = 2 \/ Zmin (alignof ty) 4 = 4. +Proof. + intros. generalize (alignof_1248 ty). + intros [A|[A|[A|A]]]; rewrite A; auto. +Qed. + +Lemma make_memcpy_correct: + forall f dst src ty k e le m b ofs v t m', + eval_expr ge e le m dst (Vptr b ofs) -> + eval_expr ge e le m src v -> + assign_loc ge ty m b ofs v t m' -> + access_mode ty = By_copy -> + step ge (State f (make_memcpy dst src ty) k e le m) t (State f Sskip k e le m'). +Proof. + intros. inv H1; try congruence. + unfold make_memcpy. change le with (set_optvar None Vundef le) at 2. + econstructor. + econstructor. eauto. econstructor. eauto. constructor. + econstructor; eauto. + apply capped_alignof_124. + apply sizeof_pos. + apply capped_alignof_divides. apply sizeof_alignof_compat. + apply capped_alignof_divides; auto. + apply capped_alignof_divides; auto. +Qed. + Lemma make_store_correct: - forall addr ty rhs code e le m b ofs v m' f k, + forall addr ty rhs code e le m b ofs v t m' f k, make_store addr ty rhs = OK code -> eval_expr ge e le m addr (Vptr b ofs) -> eval_expr ge e le m rhs v -> - store_value_of_type ty m b ofs v = Some m' -> - step ge (State f code k e le m) E0 (State f Sskip k e le m'). + assign_loc ge ty m b ofs v t m' -> + type_is_volatile ty = false -> + step ge (State f code k e le m) t (State f Sskip k e le m'). +Proof. + unfold make_store. intros until k; intros MKSTORE EV1 EV2 ASSIGN NONVOL. + inversion ASSIGN; subst. + (* nonvolatile scalar *) + rewrite H in MKSTORE; inv MKSTORE. + econstructor; eauto. + (* volatile scalar *) + congruence. + (* by copy *) + rewrite H in MKSTORE; inv MKSTORE. + eapply make_memcpy_correct; eauto. +Qed. + +Lemma make_vol_store_correct: + forall addr ty rhs code e le m b ofs v t m' f k, + make_vol_store addr ty rhs = OK code -> + eval_expr ge e le m addr (Vptr b ofs) -> + eval_expr ge e le m rhs v -> + assign_loc ge ty m b ofs v t m' -> + type_is_volatile ty = true -> + step ge (State f code k e le m) t (State f Sskip k e le m'). Proof. - unfold make_store, store_value_of_type. - intros until k; intros MKSTORE EV1 EV2 STVAL. - destruct (access_mode ty); inversion MKSTORE. - (* access_mode ty = By_value m *) - eapply step_store; eauto. + unfold make_vol_store. intros until k; intros MKSTORE EV1 EV2 ASSIGN VOL. + inversion ASSIGN; subst. + (* nonvolatile scalar *) + congruence. + (* volatile scalar *) + rewrite H in MKSTORE; inv MKSTORE. + change le with (Cminor.set_optvar None Vundef le) at 2. + econstructor. constructor. eauto. constructor. eauto. constructor. + constructor. auto. + (* by copy *) + rewrite H in MKSTORE; inv MKSTORE. + eapply make_memcpy_correct; eauto. Qed. End CONSTRUCTORS. @@ -732,6 +843,49 @@ Lemma var_info_translated: exists tv, Genv.find_var_info tge b = Some tv /\ transf_globvar transl_globvar v = OK tv. Proof (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). +Lemma var_info_rev_translated: + forall b tv, + Genv.find_var_info tge b = Some tv -> + exists v, Genv.find_var_info ge b = Some v /\ transf_globvar transl_globvar v = OK tv. +Proof (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL). + +Lemma block_is_volatile_preserved: + forall b, block_is_volatile tge b = block_is_volatile ge b. +Proof. + intros. unfold block_is_volatile. + destruct (Genv.find_var_info ge b) as []_eqn. + exploit var_info_translated; eauto. intros [tv [A B]]. rewrite A. + unfold transf_globvar in B. monadInv B. auto. + destruct (Genv.find_var_info tge b) as []_eqn. + exploit var_info_rev_translated; eauto. intros [tv [A B]]. congruence. + auto. +Qed. + +Lemma deref_loc_preserved: + forall ty m b ofs t v, + deref_loc ge ty m b ofs t v -> deref_loc tge ty m b ofs t v. +Proof. + intros. inv H. + eapply deref_loc_value; eauto. + eapply deref_loc_volatile; eauto. + eapply volatile_load_preserved with (ge1 := ge); auto. + exact symbols_preserved. exact block_is_volatile_preserved. + eapply deref_loc_reference; eauto. + eapply deref_loc_copy; eauto. +Qed. + +Lemma assign_loc_preserved: + forall ty m b ofs v t m', + assign_loc ge ty m b ofs v t m' -> assign_loc tge ty m b ofs v t m'. +Proof. + intros. inv H. + eapply assign_loc_value; eauto. + eapply assign_loc_volatile; eauto. + eapply volatile_store_preserved with (ge1 := ge); auto. + exact symbols_preserved. exact block_is_volatile_preserved. + eapply assign_loc_copy; eauto. +Qed. + (** * Matching between environments *) (** In this section, we define a matching relation between @@ -861,32 +1015,43 @@ Qed. Lemma bind_parameters_match: forall e m1 vars vals m2, - Csem.bind_parameters e m1 vars vals m2 -> + Csem.bind_parameters ge e m1 vars vals m2 -> forall te tvars, val_casted_list vals (type_of_params vars) -> match_env e te -> - transl_params vars = OK tvars -> - Csharpminor.bind_parameters te m1 tvars vals m2. + transl_vars vars = OK tvars -> + Csharpminor.bind_parameters tge te m1 tvars vals m2. Proof. induction 1; intros. (* base case *) monadInv H1. constructor. (* inductive case *) simpl in H2. destruct H2. - revert H4; simpl. - caseEq (chunk_of_type ty); simpl; [intros chunk CHK | congruence]. - caseEq (transl_params params); simpl; [intros tparams TPARAMS | congruence]. - intro EQ; inversion EQ; clear EQ; subst tvars. - generalize CHK. unfold chunk_of_type. - caseEq (access_mode ty); intros; try discriminate. - inversion CHK0; clear CHK0; subst m0. - unfold store_value_of_type in H0. rewrite H4 in H0. - apply bind_parameters_cons with b m1. - exploit me_local; eauto. intros [vk [A B]]. - exploit var_kind_by_value; eauto. congruence. + simpl in H4. destruct (var_kind_of_type ty) as [vk|]_eqn; monadInv H4. + assert (A: (exists chunk, access_mode ty = By_value chunk /\ Mem.store chunk m b 0 v1 = Some m1) + \/ access_mode ty = By_copy). + inv H0; auto; left; econstructor; split; eauto. inv H7. auto. + destruct A as [[chunk [MODE STORE]] | MODE]. + (* scalar case *) + assert (vk = Vscalar chunk). exploit var_kind_by_value; eauto. congruence. + subst vk. + apply bind_parameters_scalar with b m1. + exploit me_local; eauto. intros [vk [A B]]. congruence. eapply val_casted_normalized; eauto. assumption. apply IHbind_parameters; auto. + (* array case *) + inv H0; try congruence. + exploit var_kind_by_reference; eauto. intros; subst vk. + apply bind_parameters_array with b m1. + exploit me_local; eauto. intros [vk [A B]]. congruence. + econstructor; eauto. + apply capped_alignof_124. + apply sizeof_pos. + apply capped_alignof_divides. apply sizeof_alignof_compat. + apply capped_alignof_divides; auto. + apply capped_alignof_divides; auto. + apply IHbind_parameters; auto. Qed. (* ** Correctness of variable accessors *) @@ -896,16 +1061,21 @@ Qed. Lemma var_get_correct: forall e le m id ty loc ofs v code te, Clight.eval_lvalue ge e le m (Clight.Evar id ty) loc ofs -> - load_value_of_type ty m loc ofs = Some v -> + deref_loc ge ty m loc ofs E0 v -> var_get id ty = OK code -> match_env e te -> eval_expr tge te le m code v. Proof. - intros. revert H0 H1. unfold load_value_of_type, var_get. - case_eq (access_mode ty). + unfold var_get; intros. + destruct (access_mode ty) as [chunk| | | ]_eqn. (* access mode By_value *) - intros chunk ACC LOAD EQ. inv EQ. - inv H. + assert (Mem.loadv chunk m (Vptr loc ofs) = Some v). + inv H0. + congruence. + inv H5. simpl. congruence. + congruence. + congruence. + inv H1. inv H. (* local variable *) exploit me_local; eauto. intros [vk [A B]]. assert (vk = Vscalar chunk). @@ -922,7 +1092,20 @@ Proof. eauto. eauto. assumption. (* access mode By_reference *) - intros ACC EQ1 EQ2. inv EQ1; inv EQ2; inv H. + assert (v = Vptr loc ofs). inv H0; congruence. + inv H1. inv H. + (* local variable *) + exploit me_local; eauto. intros [vk [A B]]. + eapply eval_Eaddrof. + eapply eval_var_addr_local. eauto. + (* global variable *) + exploit match_env_globals; eauto. intros [A B]. + eapply eval_Eaddrof. + eapply eval_var_addr_global. auto. + rewrite symbols_preserved. eauto. + (* access mode By_copy *) + assert (v = Vptr loc ofs). inv H0; congruence. + inv H1. inv H. (* local variable *) exploit me_local; eauto. intros [vk [A B]]. eapply eval_Eaddrof. @@ -939,19 +1122,19 @@ Qed. (** Correctness of the code generated by [var_set]. *) Lemma var_set_correct: - forall e le m id ty loc ofs v m' code te rhs f k, + forall e le m id ty loc ofs v t m' code te rhs f k, Clight.eval_lvalue ge e le m (Clight.Evar id ty) loc ofs -> val_casted v ty -> - store_value_of_type ty m loc ofs v = Some m' -> + assign_loc ge ty m loc ofs v t m' -> + type_is_volatile ty = false -> var_set id ty rhs = OK code -> match_env e te -> eval_expr tge te le m rhs v -> - step tge (State f code k te le m) E0 (State f Sskip k te le m'). + step tge (State f code k te le m) t (State f Sskip k te le m'). Proof. - intros. revert H1 H2. unfold store_value_of_type, var_set. - caseEq (access_mode ty). - (* access mode By_value *) - intros chunk ACC STORE EQ. inv EQ. + intros. unfold var_set in H3. + inversion H1; subst; rewrite H6 in H3; inv H3. + (* scalar, non volatile *) inv H. (* local variable *) exploit me_local; eauto. intros [vk [A B]]. @@ -968,65 +1151,20 @@ Proof. econstructor. eapply eval_var_ref_global. auto. rewrite symbols_preserved. eauto. eauto. eauto. - eapply val_casted_normalized; eauto. assumption. - (* access mode By_reference *) - congruence. - (* access mode By_nothing *) + eapply val_casted_normalized; eauto. assumption. + (* scalar, volatile *) congruence. + (* array *) + assert (eval_expr tge te le m (Eaddrof id) (Vptr loc ofs)). + inv H. + exploit me_local; eauto. intros [vk [A B]]. + constructor. eapply eval_var_addr_local; eauto. + exploit match_env_globals; eauto. intros [A B]. + constructor. eapply eval_var_addr_global; eauto. + rewrite symbols_preserved. eauto. + eapply make_memcpy_correct; eauto. eapply assign_loc_preserved; eauto. Qed. -(**************************** -Lemma call_dest_correct: - forall e m lhs loc ofs optid te, - Csem.eval_lvalue ge e m lhs loc ofs -> - transl_lhs_call (Some lhs) = OK optid -> - match_env e te -> - exists id, - optid = Some id - /\ ofs = Int.zero - /\ match access_mode (typeof lhs) with - | By_value chunk => eval_var_ref tge te id loc chunk - | _ => True - end. -Proof. - intros. revert H0. simpl. caseEq (is_variable lhs); try congruence. - intros id ISV EQ. inv EQ. - exploit is_variable_correct; eauto. intro EQ. - rewrite EQ in H. clear EQ. - exists id. split; auto. - inv H. -(* local variable *) - split. auto. - exploit me_local; eauto. intros [vk [A B]]. - case_eq (access_mode (typeof lhs)); intros; auto. - assert (vk = Vscalar m0). - exploit var_kind_by_value; eauto. congruence. - subst vk. apply eval_var_ref_local; auto. -(* global variable *) - split. auto. - exploit match_env_globals; eauto. intros [A B]. - case_eq (access_mode (typeof lhs)); intros; auto. - exploit B; eauto. intros [gv [C D]]. - eapply eval_var_ref_global; eauto. - rewrite symbols_preserved. auto. -Qed. - -Lemma set_call_dest_correct: - forall ty m loc v m' e te id, - store_value_of_type ty m loc Int.zero v = Some m' -> - match access_mode ty with - | By_value chunk => eval_var_ref tge te id loc chunk - | _ => True - end -> - match_env e te -> - exec_opt_assign tge te m (Some id) v m'. -Proof. - intros. generalize H. unfold store_value_of_type. case_eq (access_mode ty); intros; try congruence. - rewrite H2 in H0. - constructor. econstructor. eauto. auto. -Qed. -**************************) - (** * Proof of semantic preservation *) (** ** Semantic preservation for expressions *) @@ -1097,7 +1235,7 @@ Proof. (* Case a is a variable *) subst a. eapply var_get_correct; eauto. (* Case a is another lvalue *) - eapply make_load_correct; eauto. + eapply make_load_correct; eauto. eapply deref_loc_preserved; eauto. (* var local *) exploit (me_local _ _ MENV); eauto. intros [vk [A B]]. @@ -1352,11 +1490,17 @@ Proof. (* skip *) auto. (* assign *) - simpl in TR. destruct (is_variable e); monadInv TR. - unfold var_set in EQ0. destruct (access_mode (typeof e)); inv EQ0. auto. - unfold make_store in EQ2. destruct (access_mode (typeof e)); inv EQ2. auto. + simpl in TR. destruct (type_is_volatile (typeof e)) as []_eqn. + monadInv TR. unfold make_vol_store, make_memcpy in EQ2. + destruct (access_mode (typeof e)); inv EQ2; auto. + destruct (is_variable e); monadInv TR. + unfold var_set, make_memcpy in EQ0. + destruct (access_mode (typeof e)); inv EQ0; auto. + unfold make_store, make_memcpy in EQ2. destruct (access_mode (typeof e)); inv EQ2; auto. (* set *) auto. +(* vol load *) + unfold make_vol_load in EQ0. destruct (access_mode (typeof e)); inv EQ0; auto. (* call *) simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto. (* seq *) @@ -1451,25 +1595,39 @@ Proof. induction 1; intros T1 MST; inv MST. (* assign *) - revert TR. simpl. case_eq (is_variable a1); intros; monadInv TR. - exploit is_variable_correct; eauto. intro EQ1. rewrite EQ1 in H. - assert (ts' = ts /\ tk' = tk). + simpl in TR. destruct (type_is_volatile (typeof a1)) as []_eqn. + (* Case 1: volatile *) + monadInv TR. + assert (SAME: ts' = ts /\ tk' = tk). + inversion MTR. auto. + subst ts. unfold make_vol_store, make_memcpy in EQ2. + destruct (access_mode (typeof a1)); congruence. + destruct SAME; subst ts' tk'. + econstructor; split. + apply plus_one. eapply make_vol_store_correct; eauto. + eapply transl_lvalue_correct; eauto. eapply make_cast_correct; eauto. + eapply transl_expr_correct; eauto. eapply assign_loc_preserved; eauto. + eapply match_states_skip; eauto. + (* Case 2: variable *) + destruct (is_variable a1) as []_eqn; monadInv TR. + assert (SAME: ts' = ts /\ tk' = tk). inversion MTR. auto. - subst ts. unfold var_set in EQ0. destruct (access_mode (typeof a1)); congruence. - destruct H4; subst ts' tk'. + subst ts. unfold var_set, make_memcpy in EQ0. destruct (access_mode (typeof a1)); congruence. + destruct SAME; subst ts' tk'. + exploit is_variable_correct; eauto. intro EQ1. rewrite EQ1 in H. econstructor; split. apply plus_one. eapply var_set_correct; eauto. exists v2; exists (typeof a2); auto. eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. eapply match_states_skip; eauto. - - assert (ts' = ts /\ tk' = tk). + (* Case 3: everything else *) + assert (SAME: ts' = ts /\ tk' = tk). inversion MTR. auto. - subst ts. unfold make_store in EQ2. destruct (access_mode (typeof a1)); congruence. - destruct H4; subst ts' tk'. + subst ts. unfold make_store, make_memcpy in EQ2. destruct (access_mode (typeof a1)); congruence. + destruct SAME; subst ts' tk'. econstructor; split. apply plus_one. eapply make_store_correct; eauto. - exploit transl_lvalue_correct; eauto. - eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. + eapply transl_lvalue_correct; eauto. eapply make_cast_correct; eauto. + eapply transl_expr_correct; eauto. eapply assign_loc_preserved; eauto. eapply match_states_skip; eauto. (* set *) @@ -1477,6 +1635,17 @@ Proof. apply plus_one. econstructor. eapply transl_expr_correct; eauto. eapply match_states_skip; eauto. +(* vol read *) + monadInv TR. + assert (SAME: ts' = ts /\ tk' = tk). + inversion MTR. auto. + subst ts. unfold make_vol_load in EQ0. destruct (access_mode (typeof a)); congruence. + destruct SAME; subst ts' tk'. + econstructor; split. + apply plus_one. eapply make_vol_load_correct; eauto. eapply transl_lvalue_correct; eauto. + eapply deref_loc_preserved; eauto. + eapply match_states_skip; eauto. + (* call *) revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence. intros targs tres CF TR. monadInv TR. inv MTR. @@ -1759,8 +1928,8 @@ Proof. monadInv TR. monadInv EQ. exploit match_cont_is_call_cont; eauto. intros [A B]. exploit match_env_alloc_variables; eauto. - apply match_env_empty. - apply transl_fn_variables. eauto. eauto. + apply match_env_empty. + eapply transl_fn_variables; eauto. intros [te1 [C D]]. econstructor; split. apply plus_one. econstructor. @@ -1806,7 +1975,7 @@ Proof. rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog). auto. symmetry. unfold transl_program in TRANSL. eapply transform_partial_program2_main; eauto. - assert (funsig tf = signature_of_type Tnil (Tint I32 Signed)). + assert (funsig tf = signature_of_type Tnil type_int32s). eapply transl_fundef_sig2; eauto. econstructor; split. econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto. -- cgit v1.2.3