From f7693b3d897b90fd3bc2533be002dc0bdcd9f6c2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 6 Oct 2012 15:46:47 +0000 Subject: Merge of branch seq-and-or. See Changelog for details. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgenproof.v | 577 ++++++++++++----------------------------------- 1 file changed, 146 insertions(+), 431 deletions(-) (limited to 'cfrontend/Cshmgenproof.v') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 6a02e1d0..51511b96 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -150,6 +150,19 @@ Proof. intros. functional inversion H; subst; simpl in H0; congruence. Qed. +Remark cast_to_bool_normalized: + forall ty1 ty2 chunk, + classify_cast ty1 ty2 = cast_case_f2bool \/ + classify_cast ty1 ty2 = cast_case_p2bool -> + access_mode ty2 = By_value chunk -> + chunk = Mint8unsigned. +Proof. + intros. destruct ty2; simpl in *; try discriminate. + destruct i; destruct ty1; intuition congruence. + destruct ty1; intuition discriminate. + destruct ty1; intuition discriminate. +Qed. + Lemma cast_result_normalized: forall chunk v1 ty1 ty2 v2, sem_cast v1 ty1 ty2 = Some v2 -> @@ -163,14 +176,10 @@ 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. + rewrite (cast_to_bool_normalized ty1 ty2 chunk); auto. red; auto. + rewrite (cast_to_bool_normalized ty1 ty2 chunk); auto. red; auto. + rewrite (cast_to_bool_normalized ty1 ty2 chunk); auto. destruct (Int.eq i Int.zero); red; auto. + rewrite (cast_to_bool_normalized ty1 ty2 chunk); auto. 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. @@ -376,6 +385,31 @@ Hint Resolve make_intconst_correct make_floatconst_correct eval_Eunop eval_Ebinop: cshm. Hint Extern 2 (@eq trace _ _) => traceEq: cshm. +Lemma make_cmp_ne_zero_correct: + forall e le m a n, + eval_expr ge e le m a (Vint n) -> + eval_expr ge e le m (make_cmp_ne_zero a) (Vint (if Int.eq n Int.zero then Int.zero else Int.one)). +Proof. + intros. + assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmp Cne) a (make_intconst Int.zero)) + (Vint (if Int.eq n Int.zero then Int.zero else Int.one))). + econstructor; eauto with cshm. simpl. unfold Val.cmp, Val.cmp_bool. + unfold Int.cmp. destruct (Int.eq n Int.zero); auto. + assert (CMP: forall ob, + Val.of_optbool ob = Vint n -> + n = (if Int.eq n Int.zero then Int.zero else Int.one)). + intros. destruct ob; simpl in H0; inv H0. destruct b; inv H2. + rewrite Int.eq_false. auto. apply Int.one_not_zero. + rewrite Int.eq_true. auto. + destruct a; simpl; auto. destruct b; auto. + inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. inv H6. unfold Val.cmp in H0. eauto. + inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. inv H6. unfold Val.cmp in H0. eauto. + inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. inv H6. unfold Val.cmp in H0. eauto. +Qed. + Lemma make_cast_int_correct: forall e le m a n sz si, eval_expr ge e le m a (Vint n) -> @@ -386,7 +420,7 @@ Proof. destruct si; eauto with cshm. destruct si; eauto with cshm. auto. - econstructor. eauto. simpl. destruct (Int.eq n Int.zero); auto. + apply make_cmp_ne_zero_correct; auto. Qed. Lemma make_cast_float_correct: @@ -418,14 +452,15 @@ Proof. rewrite H2. auto with cshm. (* float -> int *) rewrite H2. eauto with cshm. - (* 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. + (* pointer -> bool *) + rewrite H2. econstructor; eauto with cshm. + simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. destruct (Int.eq i Int.zero); reflexivity. + rewrite H2. econstructor; eauto with cshm. (* struct -> struct *) rewrite H2. auto. (* union -> union *) @@ -442,21 +477,20 @@ Lemma make_boolean_correct: eval_expr ge e le m (make_boolean a ty) vb /\ Val.bool_of_val vb b. Proof. - assert (VBI: forall n, Val.bool_of_val (Vint n) (negb (Int.eq n Int.zero))). - constructor. - 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. - exists (Val.of_bool (Float.cmp Cne f Float.zero)); split. - econstructor; eauto with cshm. - destruct (Float.cmp Cne f Float.zero); simpl; constructor. + intros. unfold make_boolean. unfold bool_val in H0. + destruct (classify_bool ty); destruct v; inv H0. +(* int *) + econstructor; split. apply make_cmp_ne_zero_correct with (n := i); auto. + destruct (Int.eq i Int.zero); simpl; constructor. +(* float *) + econstructor; split. econstructor; eauto with cshm. simpl. eauto. + unfold Val.cmpf, Val.cmpf_bool. simpl. rewrite <- Float.cmp_ne_eq. + destruct (Float.cmp Cne f Float.zero); constructor. +(* pointer *) + econstructor; split. econstructor; eauto with cshm. simpl. eauto. + unfold Val.cmpu, Val.cmpu_bool. simpl. + destruct (Int.eq i Int.zero); simpl; constructor. + exists Vtrue; split. econstructor; eauto with cshm. constructor. Qed. Lemma make_neg_correct: @@ -682,75 +716,26 @@ 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) -> - deref_loc ge ty m b ofs E0 v -> - type_is_volatile ty = false -> + deref_loc ty m b ofs v -> eval_expr ge e le m code v. Proof. - unfold make_load; intros until m; intros MKLOAD EVEXP DEREF NONVOL. + unfold make_load; intros until m; intros MKLOAD EVEXP DEREF. inv DEREF. - (* nonvolatile scalar *) + (* 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', + forall f dst src ty k e le m b ofs v 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' -> + assign_loc ty m b ofs v 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'). + step ge (State f (make_memcpy dst src ty) k e le m) E0 (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. @@ -763,44 +748,18 @@ Proof. Qed. Lemma make_store_correct: - forall addr ty rhs code e le m b ofs v t m' f k, + forall addr ty rhs code e le m b ofs v 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 -> - 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'). + assign_loc ty m b ofs v m' -> + step ge (State f code k e le m) E0 (State f Sskip k e le m'). Proof. - unfold make_store. intros until k; intros MKSTORE EV1 EV2 ASSIGN NONVOL. + unfold make_store. intros until k; intros MKSTORE EV1 EV2 ASSIGN. 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_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. @@ -859,31 +818,6 @@ Proof. 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 @@ -1013,7 +947,7 @@ Qed. Lemma bind_parameters_match: forall e m1 vars vals m2, - Csem.bind_parameters ge e m1 vars vals m2 -> + Clight.bind_parameters e m1 vars vals m2 -> forall te tvars, val_casted_list vals (type_of_params vars) -> match_env e te -> @@ -1026,10 +960,7 @@ Proof. (* inductive case *) simpl in H2. destruct H2. 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]. + inv H0. (* scalar case *) assert (vk = Vscalar chunk). exploit var_kind_by_value; eauto. congruence. subst vk. @@ -1038,8 +969,7 @@ Proof. eapply val_casted_normalized; eauto. assumption. apply IHbind_parameters; auto. - (* array case *) - inv H0; try congruence. + (* struct case *) 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. @@ -1050,6 +980,14 @@ Proof. apply IHbind_parameters; auto. Qed. +Lemma create_undef_temps_match: + forall temps, + create_undef_temps (List.map (@fst ident type) temps) = Clight.create_undef_temps temps. +Proof. + induction temps; simpl. auto. + destruct a as [id ty]. simpl. decEq. auto. +Qed. + (* ** Correctness of variable accessors *) (** Correctness of the code generated by [var_get]. *) @@ -1057,21 +995,15 @@ 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 -> - deref_loc ge ty m loc ofs E0 v -> + deref_loc ty m loc ofs v -> var_get id ty = OK code -> match_env e te -> eval_expr tge te le m code v. Proof. unfold var_get; intros. - destruct (access_mode ty) as [chunk| | | ]_eqn. + inv H0. (* access mode By_value *) - assert (Mem.loadv chunk m (Vptr loc ofs) = Some v). - inv H0. - congruence. - inv H5. simpl. congruence. - congruence. - congruence. - inv H1. inv H. + rewrite H3 in H1. inv H1. inv H. (* local variable *) exploit me_local; eauto. intros [vk [A B]]. assert (vk = Vscalar chunk). @@ -1088,8 +1020,7 @@ Proof. eauto. eauto. assumption. (* access mode By_reference *) - assert (v = Vptr loc ofs). inv H0; congruence. - inv H1. inv H. + rewrite H3 in H1. inv H1. inv H. (* local variable *) exploit me_local; eauto. intros [vk [A B]]. eapply eval_Eaddrof. @@ -1100,8 +1031,7 @@ Proof. 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. + rewrite H3 in H1. inv H1. inv H. (* local variable *) exploit me_local; eauto. intros [vk [A B]]. eapply eval_Eaddrof. @@ -1111,25 +1041,22 @@ Proof. eapply eval_Eaddrof. eapply eval_var_addr_global. auto. rewrite symbols_preserved. eauto. - (* access mode By_nothing *) - congruence. Qed. (** Correctness of the code generated by [var_set]. *) Lemma var_set_correct: - forall e le m id ty loc ofs v t m' code te rhs f k, + forall e le m id ty loc ofs v m' code te rhs f k, Clight.eval_lvalue ge e le m (Clight.Evar id ty) loc ofs -> val_casted v ty -> - assign_loc ge ty m loc ofs v t m' -> - type_is_volatile ty = false -> + assign_loc ty m loc ofs v m' -> 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) t (State f Sskip k te le m'). + step tge (State f code k te le m) E0 (State f Sskip k te le m'). Proof. - intros. unfold var_set in H3. - inversion H1; subst; rewrite H6 in H3; inv H3. + intros. unfold var_set in H2. + inversion H1; subst; rewrite H5 in H2; inv H2. (* scalar, non volatile *) inv H. (* local variable *) @@ -1148,9 +1075,7 @@ Proof. rewrite symbols_preserved. eauto. eauto. eauto. eapply val_casted_normalized; eauto. assumption. - (* scalar, volatile *) - congruence. - (* array *) + (* struct *) assert (eval_expr tge te le m (Eaddrof id) (Vptr loc ofs)). inv H. exploit me_local; eauto. intros [vk [A B]]. @@ -1158,7 +1083,7 @@ Proof. 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. + eapply make_memcpy_correct; eauto. Qed. (** * Proof of semantic preservation *) @@ -1216,11 +1141,6 @@ Proof. eapply transl_unop_correct; eauto. (* binop *) eapply transl_binop_correct; eauto. -(* condition *) - exploit make_boolean_correct. eapply H0; eauto. eauto. - intros [vb [EVAL BVAL]]. - eapply eval_Econdition; eauto. - destruct b; eapply make_cast_correct; eauto. (* cast *) eapply make_cast_correct; eauto. (* rvalue out of lvalue *) @@ -1229,7 +1149,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 deref_loc_preserved; eauto. + eapply make_load_correct; eauto. (* var local *) exploit (me_local _ _ MENV); eauto. intros [vk [A B]]. @@ -1263,10 +1183,10 @@ Lemma transl_lvalue_correct: Csharpminor.eval_expr tge te le m ta (Vptr b ofs). Proof (proj2 transl_expr_lvalue_correct). -Lemma transl_exprlist_correct: +Lemma transl_arglist_correct: forall al tyl vl, Clight.eval_exprlist ge e le m al tyl vl -> - forall tal, transl_exprlist al tyl = OK tal -> + forall tal, transl_arglist al tyl = OK tal -> Csharpminor.eval_exprlist tge te le m tal vl. Proof. induction 1; intros. @@ -1278,48 +1198,6 @@ Qed. End EXPR. -Lemma is_constant_bool_sound: - forall te le m a v ty b, - Csharpminor.eval_expr tge te le m a v -> - bool_val v ty = Some b -> - is_constant_bool a = Some b \/ is_constant_bool a = None. -Proof. - intros. unfold is_constant_bool. destruct a; auto. destruct c; auto. - left. decEq. inv H. simpl in H2. inv H2. functional inversion H0; auto. -Qed. - -Lemma exit_if_false_true: - forall a ts e le m v te f tk, - exit_if_false a = OK ts -> - Clight.eval_expr ge e le m a v -> - bool_val v (typeof a) = Some true -> - match_env e te -> - star step tge (State f ts tk te le m) E0 (State f Sskip tk te le m). -Proof. - intros. monadInv H. - exploit transl_expr_correct; eauto. intros EV. - exploit is_constant_bool_sound; eauto. intros [P | P]; rewrite P in EQ0; inv EQ0. - constructor. - exploit make_boolean_correct; eauto. intros [vb [EV' VB]]. - apply star_one. apply step_ifthenelse with (v := vb) (b := true); auto. -Qed. - -Lemma exit_if_false_false: - forall a ts e le m v te f tk, - exit_if_false a = OK ts -> - Clight.eval_expr ge e le m a v -> - bool_val v (typeof a) = Some false -> - match_env e te -> - star step tge (State f ts tk te le m) E0 (State f (Sexit 0) tk te le m). -Proof. - intros. monadInv H. - exploit transl_expr_correct; eauto. intros EV. - exploit is_constant_bool_sound; eauto. intros [P | P]; rewrite P in EQ0; inv EQ0. - constructor. - exploit make_boolean_correct; eauto. intros [vb [EV' VB]]. - apply star_one. apply step_ifthenelse with (v := vb) (b := false); auto. -Qed. - (** ** Semantic preservation for statements *) (** The simulation diagram for the translation of statements and functions @@ -1362,36 +1240,20 @@ Inductive match_cont: type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> P match_cont tyret nbrk ncnt (Clight.Kseq s k) (Kseq ts tk) - | match_Kwhile: forall tyret nbrk ncnt a s k ta ts tk, - exit_if_false a = OK ta -> - transl_statement tyret 1%nat 0%nat s = OK ts -> - match_cont tyret nbrk ncnt k tk -> - match_cont tyret 1%nat 0%nat - (Clight.Kwhile a s k) - (Kblock (Kseq (Sloop (Sseq ta (Sblock ts))) (Kblock tk))) - | match_Kdowhile: forall tyret nbrk ncnt a s k ta ts tk, - exit_if_false a = OK ta -> - transl_statement tyret 1%nat 0%nat s = OK ts -> + | match_Kloop1: forall tyret s1 s2 k ts1 ts2 nbrk ncnt tk, + transl_statement tyret 1%nat 0%nat s1 = OK ts1 -> + transl_statement tyret 0%nat (S ncnt) s2 = OK ts2 -> match_cont tyret nbrk ncnt k tk -> match_cont tyret 1%nat 0%nat - (Clight.Kdowhile a s k) - (Kblock (Kseq ta (Kseq (Sloop (Sseq (Sblock ts) ta)) (Kblock tk)))) - | match_Kfor2: forall tyret nbrk ncnt a2 a3 s k ta2 ta3 ts tk, - exit_if_false a2 = OK ta2 -> - transl_statement tyret 0%nat (S ncnt) a3 = OK ta3 -> - transl_statement tyret 1%nat 0%nat s = OK ts -> - match_cont tyret nbrk ncnt k tk -> - match_cont tyret 1%nat 0%nat - (Clight.Kfor2 a2 a3 s k) - (Kblock (Kseq ta3 (Kseq (Sloop (Sseq ta2 (Sseq (Sblock ts) ta3))) (Kblock tk)))) - | match_Kfor3: forall tyret nbrk ncnt a2 a3 s k ta2 ta3 ts tk, - exit_if_false a2 = OK ta2 -> - transl_statement tyret 0%nat (S ncnt) a3 = OK ta3 -> - transl_statement tyret 1%nat 0%nat s = OK ts -> + (Clight.Kloop1 s1 s2 k) + (Kblock (Kseq ts2 (Kseq (Sloop (Sseq (Sblock ts1) ts2)) (Kblock tk)))) + | match_Kloop2: forall tyret s1 s2 k ts1 ts2 nbrk ncnt tk, + transl_statement tyret 1%nat 0%nat s1 = OK ts1 -> + transl_statement tyret 0%nat (S ncnt) s2 = OK ts2 -> match_cont tyret nbrk ncnt k tk -> match_cont tyret 0%nat (S ncnt) - (Clight.Kfor3 a2 a3 s k) - (Kseq (Sloop (Sseq ta2 (Sseq (Sblock ts) ta3))) (Kblock tk)) + (Clight.Kloop2 s1 s2 k) + (Kseq (Sloop (Sseq (Sblock ts1) ts2)) (Kblock tk)) | match_Kswitch: forall tyret nbrk ncnt k tk, match_cont tyret nbrk ncnt k tk -> match_cont tyret 0%nat (S ncnt) @@ -1446,13 +1308,6 @@ Section FIND_LABEL. Variable lbl: label. Variable tyret: type. -Remark exit_if_false_no_label: - forall a s, exit_if_false a = OK s -> forall k, find_label lbl s k = None. -Proof. - intros. unfold exit_if_false in H. monadInv H. - destruct (is_constant_bool x). destruct b; inv EQ0; auto. inv EQ0; auto. -Qed. - Lemma transl_find_label: forall s nbrk ncnt k ts tk (TR: transl_statement tyret nbrk ncnt s = OK ts) @@ -1484,19 +1339,18 @@ Proof. (* skip *) auto. (* assign *) - 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. + simpl in TR. 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. + 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. +(* builtin *) + auto. (* seq *) exploit (transl_find_label s0 nbrk ncnt (Clight.Kseq s1 k)); eauto. constructor; eauto. destruct (Clight.find_label lbl s0 (Clight.Kseq s1 k)) as [[s' k'] | ]. @@ -1509,23 +1363,13 @@ Proof. intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]]. rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. intro. rewrite H. eapply transl_find_label; eauto. -(* while *) - rewrite (exit_if_false_no_label _ _ EQ). - eapply transl_find_label; eauto. econstructor; eauto. -(* dowhile *) - exploit (transl_find_label s0 1%nat 0%nat (Clight.Kdowhile e s0 k)); eauto. econstructor; eauto. - destruct (Clight.find_label lbl s0 (Kdowhile e s0 k)) as [[s' k'] | ]. - intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]]. - rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. - intro. rewrite H. eapply exit_if_false_no_label; eauto. -(* for *) - rewrite (exit_if_false_no_label _ _ EQ). - exploit (transl_find_label s1 1%nat 0%nat (Kfor2 e s0 s1 k)); eauto. econstructor; eauto. - destruct (Clight.find_label lbl s1 (Kfor2 e s0 s1 k)) as [[s' k'] | ]. +(* loop *) + exploit (transl_find_label s0 1%nat 0%nat (Kloop1 s0 s1 k)); eauto. econstructor; eauto. + destruct (Clight.find_label lbl s0 (Kloop1 s0 s1 k)) as [[s' k'] | ]. intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]]. rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. intro. rewrite H. - eapply transl_find_label; eauto. econstructor; eauto. + eapply transl_find_label; eauto. econstructor; eauto. (* break *) auto. (* continue *) @@ -1589,21 +1433,9 @@ Proof. induction 1; intros T1 MST; inv MST. (* assign *) - 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 *) + simpl in TR. destruct (is_variable a1) as []_eqn; monadInv TR. + (* a variable *) assert (SAME: ts' = ts /\ tk' = tk). inversion MTR. auto. subst ts. unfold var_set, make_memcpy in EQ0. destruct (access_mode (typeof a1)); congruence. @@ -1613,7 +1445,7 @@ Proof. 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. - (* Case 3: everything else *) + (* not a variable *) assert (SAME: ts' = ts /\ tk' = tk). inversion MTR. auto. subst ts. unfold make_store, make_memcpy in EQ2. destruct (access_mode (typeof a1)); congruence. @@ -1621,7 +1453,7 @@ Proof. econstructor; split. apply plus_one. eapply make_store_correct; eauto. eapply transl_lvalue_correct; eauto. eapply make_cast_correct; eauto. - eapply transl_expr_correct; eauto. eapply assign_loc_preserved; eauto. + eapply transl_expr_correct; eauto. eapply match_states_skip; eauto. (* set *) @@ -1629,17 +1461,6 @@ 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. @@ -1648,13 +1469,24 @@ Proof. econstructor; split. apply plus_one. econstructor; eauto. exploit transl_expr_correct; eauto. - exploit transl_exprlist_correct; eauto. + exploit transl_arglist_correct; eauto. eapply transl_fundef_sig1; eauto. rewrite H3. auto. econstructor; eauto. econstructor; eauto. simpl. auto. - eapply eval_exprlist_casted; eauto. + eapply eval_exprlist_casted; eauto. + +(* builtin *) + monadInv TR. inv MTR. + econstructor; split. + apply plus_one. econstructor. + eapply transl_arglist_correct; eauto. + eapply external_call_symbols_preserved_2; eauto. + exact symbols_preserved. + eexact (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). + eexact (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL). + eapply match_states_skip; eauto. (* seq *) monadInv TR. inv MTR. @@ -1690,33 +1522,17 @@ Proof. apply plus_one. apply step_ifthenelse with (v := v) (b := b); auto. destruct b; econstructor; eauto; constructor. -(* while false *) +(* loop *) monadInv TR. econstructor; split. eapply star_plus_trans. eapply match_transl_step; eauto. eapply plus_left. constructor. eapply star_left. constructor. - eapply star_trans. eapply exit_if_false_false; eauto. - eapply star_left. constructor. - eapply star_left. constructor. - apply star_one. constructor. - reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. traceEq. - eapply match_states_skip; eauto. - -(* while true *) - monadInv TR. - econstructor; split. - eapply star_plus_trans. eapply match_transl_step; eauto. - eapply plus_left. constructor. - eapply star_left. constructor. - eapply star_trans. eapply exit_if_false_true; eauto. - eapply star_left. constructor. apply star_one. constructor. - reflexivity. reflexivity. reflexivity. reflexivity. traceEq. - econstructor; eauto. constructor. - econstructor; eauto. + reflexivity. reflexivity. traceEq. + econstructor; eauto. constructor. econstructor; eauto. -(* skip or continue while *) +(* skip-or-continue loop *) assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). destruct H; subst x; monadInv TR; inv MTR; auto. destruct H0. inv MK. @@ -1724,126 +1540,32 @@ Proof. eapply plus_left. destruct H0; subst ts'; constructor. apply star_one. constructor. traceEq. - econstructor; eauto. - simpl. rewrite H8; simpl. rewrite H10; simpl. reflexivity. - constructor. + econstructor; eauto. constructor. econstructor; eauto. -(* break while *) +(* break loop1 *) monadInv TR. inv MTR. inv MK. econstructor; split. eapply plus_left. constructor. eapply star_left. constructor. - apply star_one. constructor. - reflexivity. traceEq. - eapply match_states_skip; eauto. - -(* dowhile *) - monadInv TR. - econstructor; split. - eapply star_plus_trans. eapply match_transl_step; eauto. - eapply plus_left. constructor. eapply star_left. constructor. apply star_one. constructor. reflexivity. reflexivity. traceEq. - econstructor; eauto. constructor. - econstructor; eauto. - -(* skip or continue dowhile false *) - assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). - destruct H; subst x; monadInv TR; inv MTR; auto. - destruct H2. inv MK. - econstructor; split. - eapply plus_left. destruct H2; subst ts'; constructor. - eapply star_left. constructor. - eapply star_trans. eapply exit_if_false_false; eauto. - eapply star_left. constructor. - apply star_one. constructor. - reflexivity. reflexivity. reflexivity. traceEq. eapply match_states_skip; eauto. -(* skip or continue dowhile true *) - assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). - destruct H; subst x; monadInv TR; inv MTR; auto. - destruct H2. inv MK. - econstructor; split. - eapply plus_left. destruct H2; subst ts'; constructor. - eapply star_left. constructor. - eapply star_trans. eapply exit_if_false_true; eauto. - apply star_one. constructor. - reflexivity. reflexivity. traceEq. - econstructor; eauto. - simpl. rewrite H10; simpl. rewrite H12; simpl. reflexivity. constructor. - -(* break dowhile *) +(* skip loop2 *) monadInv TR. inv MTR. inv MK. econstructor; split. - eapply plus_left. constructor. - eapply star_left. constructor. - eapply star_left. constructor. - apply star_one. constructor. - reflexivity. reflexivity. traceEq. - eapply match_states_skip; eauto. - -(* for false *) - monadInv TR. - econstructor; split. - eapply star_plus_trans. eapply match_transl_step; eauto. - eapply plus_left. constructor. - eapply star_left. constructor. - eapply star_trans. eapply exit_if_false_false; eauto. - eapply star_left. constructor. - eapply star_left. constructor. - apply star_one. constructor. - reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. - eapply match_states_skip; eauto. - -(* for true *) - monadInv TR. - econstructor; split. - eapply star_plus_trans. eapply match_transl_step; eauto. - eapply plus_left. constructor. - eapply star_left. constructor. - eapply star_trans. eapply exit_if_false_true; eauto. - eapply star_left. constructor. - eapply star_left. constructor. - apply star_one. constructor. - reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. - econstructor; eauto. constructor. + apply plus_one. constructor. econstructor; eauto. + simpl. rewrite H5; simpl. rewrite H7; simpl. eauto. + constructor. -(* skip or continue for2 *) - assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). - destruct H; subst x; monadInv TR; inv MTR; auto. - destruct H0. inv MK. - econstructor; split. - eapply plus_left. destruct H0; subst ts'; constructor. - apply star_one. constructor. reflexivity. - econstructor; eauto. constructor. - econstructor; eauto. - -(* break for2 *) +(* break loop2 *) monadInv TR. inv MTR. inv MK. econstructor; split. eapply plus_left. constructor. - eapply star_left. constructor. - eapply star_left. constructor. apply star_one. constructor. - reflexivity. reflexivity. traceEq. - eapply match_states_skip; eauto. - -(* skip for3 *) - monadInv TR. inv MTR. inv MK. - econstructor; split. - apply plus_one. constructor. - econstructor; eauto. - simpl. rewrite H6; simpl. rewrite H8; simpl. rewrite H9; simpl. reflexivity. - constructor. - -(* break for3 *) - monadInv TR. inv MTR. inv MK. - econstructor; split. - eapply plus_left. constructor. apply star_one. constructor. - econstructor; eauto. + traceEq. eapply match_states_skip; eauto. (* return none *) @@ -1858,10 +1580,6 @@ Proof. monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. -(* monadInv TRF. simpl. - unfold opttyp_of_type. destruct (Clight.fn_return f); try congruence. - inv H0. inv H3. inv H3. -*) eapply make_cast_correct. eapply transl_expr_correct; eauto. eauto. eapply match_env_free_blocks; eauto. econstructor; eauto. @@ -1930,6 +1648,7 @@ Proof. eapply transl_names_norepet; eauto. eexact C. eapply bind_parameters_match; eauto. simpl in TY. unfold type_of_function in TY. congruence. + simpl. rewrite (create_undef_temps_match (Clight.fn_temps f)). econstructor; eauto. unfold transl_function. rewrite EQ0; simpl. rewrite EQ; simpl. rewrite EQ1; auto. constructor. @@ -1953,10 +1672,6 @@ Proof. econstructor; split. apply plus_one. constructor. econstructor; eauto. simpl; reflexivity. constructor. - inv MK. - econstructor; split. - apply plus_one. constructor. - econstructor; eauto. simpl; reflexivity. constructor. Qed. Lemma transl_initial_states: -- cgit