From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- cfrontend/Cshmgenproof.v | 340 +++++++++++++++++++++++------------------------ 1 file changed, 170 insertions(+), 170 deletions(-) (limited to 'cfrontend/Cshmgenproof.v') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index c69d0c0a..e25e21c9 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -45,8 +45,8 @@ Lemma transl_fundef_sig1: classify_fun (type_of_fundef f) = fun_case_f args res cc -> funsig tf = signature_of_type args res cc. Proof. - intros. destruct f; simpl in *. - monadInv H. monadInv EQ. simpl. inversion H0. + intros. destruct f; simpl in *. + monadInv H. monadInv EQ. simpl. inversion H0. unfold signature_of_function, signature_of_type. f_equal. apply transl_params_types. destruct (signature_eq (ef_sig e) (signature_of_type t t0 c)); inv H. @@ -81,9 +81,9 @@ Proof. (* deref *) monadInv TR. exists x; auto. (* field struct *) - monadInv TR. exists x0; split; auto. simpl; rewrite EQ; auto. + monadInv TR. exists x0; split; auto. simpl; rewrite EQ; auto. (* field union *) - monadInv TR. exists x0; split; auto. simpl; rewrite EQ; auto. + monadInv TR. exists x0; split; auto. simpl; rewrite EQ; auto. Qed. (** Properties of labeled statements *) @@ -98,7 +98,7 @@ Proof. transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl -> transl_lbl_stmt ce tyret nbrk ncnt (Clight.select_switch_default sl) = OK (select_switch_default tsl)). { - induction sl; simpl; intros. + induction sl; simpl; intros. inv H; auto. monadInv H. simpl. destruct o; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto. } @@ -114,16 +114,16 @@ Proof. end). { induction sl; simpl; intros. - inv H; auto. + inv H; auto. monadInv H; simpl. destruct o. destruct (zeq z n). econstructor; split; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto. apply IHsl; auto. apply IHsl; auto. } - intros. specialize (CASE _ _ H). unfold Clight.select_switch, select_switch. - destruct (Clight.select_switch_case n sl) as [sl'|]. + intros. specialize (CASE _ _ H). unfold Clight.select_switch, select_switch. + destruct (Clight.select_switch_case n sl) as [sl'|]. destruct CASE as [tsl' [P Q]]. rewrite P, Q. auto. - rewrite CASE. auto. + rewrite CASE. auto. Qed. Lemma transl_lbl_stmt_2: @@ -132,7 +132,7 @@ Lemma transl_lbl_stmt_2: transl_statement ce tyret nbrk ncnt (seq_of_labeled_statement sl) = OK (seq_of_lbl_stmt tsl). Proof. induction sl; intros. - monadInv H. auto. + monadInv H. auto. monadInv H. simpl. rewrite EQ; simpl. rewrite (IHsl _ EQ1). simpl. auto. Qed. @@ -147,28 +147,28 @@ Lemma make_intconst_correct: forall n e le m, eval_expr ge e le m (make_intconst n) (Vint n). Proof. - intros. unfold make_intconst. econstructor. reflexivity. + intros. unfold make_intconst. econstructor. reflexivity. Qed. Lemma make_floatconst_correct: forall n e le m, eval_expr ge e le m (make_floatconst n) (Vfloat n). Proof. - intros. unfold make_floatconst. econstructor. reflexivity. + intros. unfold make_floatconst. econstructor. reflexivity. Qed. Lemma make_singleconst_correct: forall n e le m, eval_expr ge e le m (make_singleconst n) (Vsingle n). Proof. - intros. unfold make_singleconst. econstructor. reflexivity. + intros. unfold make_singleconst. econstructor. reflexivity. Qed. Lemma make_longconst_correct: forall n e le m, eval_expr ge e le m (make_longconst n) (Vlong n). Proof. - intros. unfold make_floatconst. econstructor. reflexivity. + intros. unfold make_floatconst. econstructor. reflexivity. Qed. Lemma make_singleoffloat_correct: @@ -193,7 +193,7 @@ Lemma make_floatofint_correct: eval_expr ge e le m (make_floatofint a sg) (Vfloat(cast_int_float sg n)). Proof. intros. unfold make_floatofint, cast_int_float. - destruct sg; econstructor; eauto. + destruct sg; econstructor; eauto. Qed. Hint Resolve make_intconst_correct make_floatconst_correct make_longconst_correct @@ -207,33 +207,33 @@ Lemma make_cmp_ne_zero_correct: 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. + 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. + 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. + 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. + 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. + 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. + 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. + inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. unfold Val.cmpfs in H6. - destruct (Val.cmpfs_bool c v1 v2) as [[]|]; inv H6; reflexivity. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. + destruct (Val.cmpfs_bool c v1 v2) as [[]|]; inv H6; reflexivity. + inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. unfold Val.cmpl in H6. - destruct (Val.cmpl_bool c v1 v2) as [[]|]; inv H6; reflexivity. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. + destruct (Val.cmpl_bool c v1 v2) as [[]|]; inv H6; reflexivity. + inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. unfold Val.cmplu in H6. - destruct (Val.cmplu_bool c v1 v2) as [[]|]; inv H6; reflexivity. + destruct (Val.cmplu_bool c v1 v2) as [[]|]; inv H6; reflexivity. Qed. Lemma make_cast_int_correct: @@ -241,7 +241,7 @@ Lemma make_cast_int_correct: eval_expr ge e le m a (Vint n) -> eval_expr ge e le m (make_cast_int a sz si) (Vint (cast_int_int sz si n)). Proof. - intros. unfold make_cast_int, cast_int_int. + intros. unfold make_cast_int, cast_int_int. destruct sz. destruct si; eauto with cshm. destruct si; eauto with cshm. @@ -261,15 +261,15 @@ Proof. intros. unfold make_cast, sem_cast in *; destruct (classify_cast ty1 ty2); inv H; destruct v; inv H1; eauto with cshm. (* single -> int *) - unfold make_singleofint, cast_int_float. destruct si1; eauto with cshm. + unfold make_singleofint, cast_int_float. destruct si1; eauto with cshm. (* float -> int *) destruct (cast_float_int si2 f) as [i|] eqn:E; inv H2. - apply make_cast_int_correct. + apply make_cast_int_correct. unfold cast_float_int in E. unfold make_intoffloat. destruct si2; econstructor; eauto; simpl; rewrite E; auto. (* single -> int *) destruct (cast_single_int si2 f) as [i|] eqn:E; inv H2. - apply make_cast_int_correct. + apply make_cast_int_correct. unfold cast_single_int in E. unfold make_intofsingle. destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto. (* long -> int *) @@ -316,36 +316,36 @@ Lemma make_boolean_correct: eval_expr ge e le m (make_boolean a ty) vb /\ Val.bool_of_val vb b. Proof. - intros. unfold make_boolean. unfold bool_val in H0. + 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. + 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. + 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. (* single *) - econstructor; split. econstructor; eauto with cshm. simpl. eauto. - unfold Val.cmpfs, Val.cmpfs_bool. simpl. rewrite <- Float32.cmp_ne_eq. - destruct (Float32.cmp Cne f Float32.zero); constructor. + econstructor; split. econstructor; eauto with cshm. simpl. eauto. + unfold Val.cmpfs, Val.cmpfs_bool. simpl. rewrite <- Float32.cmp_ne_eq. + destruct (Float32.cmp Cne f Float32.zero); constructor. (* pointer *) - econstructor; split. econstructor; eauto with cshm. simpl. eauto. + econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpu, Val.cmpu_bool. simpl. destruct (Int.eq i Int.zero); simpl; constructor. econstructor; split. econstructor; eauto with cshm. simpl. eauto. destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i)) eqn:V; inv H2. unfold Val.cmpu, Val.cmpu_bool. simpl. - unfold Mem.weak_valid_pointer in V; rewrite V. constructor. + unfold Mem.weak_valid_pointer in V; rewrite V. constructor. (* long *) - econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. - destruct (Int64.eq i Int64.zero); simpl; constructor. + econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. + destruct (Int64.eq i Int64.zero); simpl; constructor. Qed. Lemma make_neg_correct: forall a tya c va v e le m, sem_neg va tya = Some v -> - make_neg a tya = OK c -> + make_neg a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. @@ -356,21 +356,21 @@ Qed. Lemma make_absfloat_correct: forall a tya c va v e le m, sem_absfloat va tya = Some v -> - make_absfloat a tya = OK c -> + make_absfloat a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. unfold sem_absfloat, make_absfloat; intros until m; intros SEM MAKE EV1; destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm. unfold make_floatoflong, cast_long_float. destruct s. - econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto. - econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto. + econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto. + econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto. Qed. Lemma make_notbool_correct: forall a tya c va v e le m, sem_notbool va tya m = Some v -> - make_notbool a tya = OK c -> + make_notbool a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. @@ -378,13 +378,13 @@ Proof. destruct (classify_bool tya); inv MAKE; destruct va; inv SEM; eauto with cshm. destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:V; inv H0. econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. - unfold Mem.weak_valid_pointer in V; rewrite V. auto. + unfold Mem.weak_valid_pointer in V; rewrite V. auto. Qed. Lemma make_notint_correct: forall a tya c va v e le m, sem_notint va tya = Some v -> - make_notint a tya = OK c -> + make_notint a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. @@ -397,7 +397,7 @@ Definition binary_constructor_correct (sem: val -> type -> val -> type -> option val): Prop := forall a tya b tyb c va vb v e le m, sem va tya vb tyb = Some v -> - make a tya b tyb = OK c -> + make a tya b tyb = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m b vb -> eval_expr ge e le m c v. @@ -438,9 +438,9 @@ Proof. exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. -- destruct s; inv H0; econstructor; eauto with cshm. +- destruct s; inv H0; econstructor; eauto with cshm. rewrite iop_ok; auto. rewrite iopu_ok; auto. -- destruct s; inv H0; econstructor; eauto with cshm. +- destruct s; inv H0; econstructor; eauto with cshm. rewrite lop_ok; auto. rewrite lopu_ok; auto. - erewrite <- fop_ok in SEM; eauto with cshm. - erewrite <- sop_ok in SEM; eauto with cshm. @@ -461,9 +461,9 @@ Proof. exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. -- destruct s; inv H0; econstructor; eauto with cshm. +- destruct s; inv H0; econstructor; eauto with cshm. rewrite iop_ok; auto. rewrite iopu_ok; auto. -- destruct s; inv H0; econstructor; eauto with cshm. +- destruct s; inv H0; econstructor; eauto with cshm. rewrite lop_ok; auto. rewrite lopu_ok; auto. Qed. @@ -492,17 +492,17 @@ Proof. - destruct va; try discriminate; destruct vb; inv SEM. destruct (eq_block b0 b1); try discriminate. set (sz := sizeof ce ty) in *. - destruct (zlt 0 sz); try discriminate. + destruct (zlt 0 sz); try discriminate. destruct (zle sz Int.max_signed); simpl in H0; inv H0. - econstructor; eauto with cshm. - rewrite dec_eq_true; simpl. - assert (E: Int.signed (Int.repr sz) = sz). + econstructor; eauto with cshm. + rewrite dec_eq_true; simpl. + assert (E: Int.signed (Int.repr sz) = sz). { apply Int.signed_repr. generalize Int.min_signed_neg; omega. } predSpec Int.eq Int.eq_spec (Int.repr sz) Int.zero. rewrite H in E; rewrite Int.signed_zero in E; omegaContradiction. predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone. rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction. - rewrite andb_false_r; auto. + rewrite andb_false_r; auto. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - eapply make_binarith_correct; eauto; intros; auto. Qed. @@ -546,10 +546,10 @@ Remark small_shift_amount_1: Int.ltu (Int64.loword i) Int64.iwordsize' = true /\ Int64.unsigned i = Int.unsigned (Int64.loword i). Proof. - intros. apply Int64.ltu_inv in H. comput (Int64.unsigned Int64.iwordsize). + intros. apply Int64.ltu_inv in H. comput (Int64.unsigned Int64.iwordsize). assert (Int64.unsigned i = Int.unsigned (Int64.loword i)). { - unfold Int64.loword. rewrite Int.unsigned_repr; auto. + unfold Int64.loword. rewrite Int.unsigned_repr; auto. comput Int.max_unsigned; omega. } split; auto. unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto. @@ -563,7 +563,7 @@ Proof. intros. apply Int64.ltu_inv in H. comput (Int64.unsigned (Int64.repr 32)). assert (Int64.unsigned i = Int.unsigned (Int64.loword i)). { - unfold Int64.loword. rewrite Int.unsigned_repr; auto. + unfold Int64.loword. rewrite Int.unsigned_repr; auto. comput Int.max_unsigned; omega. } unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto. @@ -574,7 +574,7 @@ Lemma small_shift_amount_3: Int.ltu i Int64.iwordsize' = true -> Int64.unsigned (Int64.repr (Int.unsigned i)) = Int.unsigned i. Proof. - intros. apply Int.ltu_inv in H. comput (Int.unsigned Int64.iwordsize'). + intros. apply Int.ltu_inv in H. comput (Int.unsigned Int64.iwordsize'). apply Int64.unsigned_repr. comput Int64.max_unsigned; omega. Qed. @@ -588,12 +588,12 @@ Proof. econstructor; eauto. simpl; rewrite E; auto. - destruct (Int64.ltu i0 Int64.iwordsize) eqn:E; inv SEM. exploit small_shift_amount_1; eauto. intros [A B]. - econstructor; eauto with cshm. simpl. rewrite A. + econstructor; eauto with cshm. simpl. rewrite A. f_equal; f_equal. unfold Int64.shl', Int64.shl. rewrite B; auto. - destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM. - econstructor; eauto with cshm. simpl. rewrite small_shift_amount_2; auto. -- destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM. - econstructor; eauto with cshm. simpl. rewrite E. + econstructor; eauto with cshm. simpl. rewrite small_shift_amount_2; auto. +- destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM. + econstructor; eauto with cshm. simpl. rewrite E. unfold Int64.shl', Int64.shl. rewrite small_shift_amount_3; auto. Qed. @@ -612,9 +612,9 @@ Proof. unfold Int64.shr', Int64.shr; rewrite B; auto. unfold Int64.shru', Int64.shru; rewrite B; auto. - destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM. - destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite small_shift_amount_2; auto. + destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite small_shift_amount_2; auto. - destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM. - destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite E. + destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite E. unfold Int64.shr', Int64.shr; rewrite small_shift_amount_3; auto. unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto. Qed. @@ -622,7 +622,7 @@ Qed. Lemma make_cmp_correct: forall cmp a tya b tyb c va vb v e le m, sem_cmp cmp va tya vb tyb m = Some v -> - make_cmp cmp a tya b tyb = OK c -> + make_cmp cmp a tya b tyb = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m b vb -> eval_expr ge e le m c v. @@ -632,38 +632,38 @@ Proof. - inv MAKE. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; simpl in SEM; inv SEM. econstructor; eauto. simpl. unfold Val.cmpu. rewrite E. auto. -- inv MAKE. destruct vb; try discriminate. +- inv MAKE. destruct vb; try discriminate. set (vb := Vint (Int.repr (Int64.unsigned i))) in *. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; simpl in SEM; inv SEM. - econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with vb. + econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with vb. unfold Val.cmpu. rewrite E. auto. -- inv MAKE. destruct va; try discriminate. +- inv MAKE. destruct va; try discriminate. set (va := Vint (Int.repr (Int64.unsigned i))) in *. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; simpl in SEM; inv SEM. - econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with va. + econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with va. unfold Val.cmpu. rewrite E. auto. - eapply make_binarith_correct; eauto; intros; auto. Qed. Lemma transl_unop_correct: - forall op a tya c va v e le m, + forall op a tya c va v e le m, transl_unop op a tya = OK c -> sem_unary_operation op va tya m = Some v -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. intros. destruct op; simpl in *. - eapply make_notbool_correct; eauto. - eapply make_notint_correct; eauto. + eapply make_notbool_correct; eauto. + eapply make_notint_correct; eauto. eapply make_neg_correct; eauto. eapply make_absfloat_correct; eauto. Qed. Lemma transl_binop_correct: forall op a tya b tyb c va vb v e le m, - transl_binop ce op a tya b tyb = OK c -> + transl_binop ce op a tya b tyb = OK c -> sem_binary_operation ce op va tya vb tyb m = Some v -> eval_expr ge e le m a va -> eval_expr ge e le m b vb -> @@ -686,7 +686,7 @@ Proof. eapply make_cmp_correct; eauto. eapply make_cmp_correct; eauto. eapply make_cmp_correct; eauto. -Qed. +Qed. Lemma make_load_correct: forall addr ty code b ofs v e le m, @@ -696,7 +696,7 @@ Lemma make_load_correct: eval_expr ge e le m code v. Proof. unfold make_load; intros until m; intros MKLOAD EVEXP DEREF. - inv DEREF. + inv DEREF. (* scalar *) rewrite H in MKLOAD. inv MKLOAD. apply eval_Eload with (Vptr b ofs); auto. (* by reference *) @@ -713,16 +713,16 @@ Lemma make_memcpy_correct: access_mode ty = By_copy -> step ge (State f (make_memcpy ce 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. + 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. + econstructor. eauto. econstructor. eauto. constructor. + econstructor; eauto. apply alignof_blockcopy_1248. apply sizeof_pos. apply sizeof_alignof_blockcopy_compat. Qed. - + Lemma make_store_correct: forall addr ty rhs code e le m b ofs v m' f k, make_store ce addr ty rhs = OK code -> @@ -735,10 +735,10 @@ Proof. inversion ASSIGN; subst. (* nonvolatile scalar *) rewrite H in MKSTORE; inv MKSTORE. - econstructor; eauto. + econstructor; eauto. (* by copy *) - rewrite H in MKSTORE; inv MKSTORE. - eapply make_memcpy_correct; eauto. + rewrite H in MKSTORE; inv MKSTORE. + eapply make_memcpy_correct; eauto. Qed. End CONSTRUCTORS. @@ -813,19 +813,19 @@ Proof. match x, y with | (b1, ty), (b2, sz) => b2 = b1 /\ sz = sizeof ge ty end). - assert (list_forall2 + assert (list_forall2 (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y)) (PTree.elements e) (PTree.elements te)). apply PTree.elements_canonical_order. intros id [b ty] GET. exists (b, sizeof ge ty); split. eapply me_local; eauto. red; auto. intros id [b sz] GET. exploit me_local_inv; eauto. intros [ty EQ]. - exploit me_local; eauto. intros EQ1. + exploit me_local; eauto. intros EQ1. exists (b, ty); split. auto. red; split; congruence. unfold blocks_of_env, Clight.blocks_of_env. - generalize H0. induction 1. auto. + generalize H0. induction 1. auto. simpl. f_equal; auto. - unfold block_of_binding, Clight.block_of_binding. + unfold block_of_binding, Clight.block_of_binding. destruct a1 as [id1 [blk1 ty1]]. destruct b1 as [id2 [blk2 sz2]]. simpl in *. destruct H1 as [A [B C]]. congruence. Qed. @@ -867,19 +867,19 @@ Proof. constructor. (* me_local *) intros until ty0. repeat rewrite PTree.gsspec. - destruct (peq id0 id); intros. congruence. eapply me_local; eauto. + destruct (peq id0 id); intros. congruence. eapply me_local; eauto. (* me_local_inv *) - intros until sz. repeat rewrite PTree.gsspec. - destruct (peq id0 id); intros. exists ty; congruence. eapply me_local_inv; eauto. + intros until sz. repeat rewrite PTree.gsspec. + destruct (peq id0 id); intros. exists ty; congruence. eapply me_local_inv; eauto. intros [te2 [ALLOC MENV]]. exists te2; split. econstructor; eauto. auto. -Qed. +Qed. Lemma create_undef_temps_match: forall temps, create_undef_temps (map fst temps) = Clight.create_undef_temps temps. Proof. - induction temps; simpl. auto. + induction temps; simpl. auto. destruct a as [id ty]. simpl. decEq. auto. Qed. @@ -889,8 +889,8 @@ Lemma bind_parameter_temps_match: bind_parameters (map fst vars) vals le1 = Some le2. Proof. induction vars; simpl; intros. - destruct vals; inv H. auto. - destruct a as [id ty]. destruct vals; try discriminate. auto. + destruct vals; inv H. auto. + destruct a as [id ty]. destruct vals; try discriminate. auto. Qed. (** * Proof of semantic preservation *) @@ -909,9 +909,9 @@ Qed. >> Left: evaluation of r-value expression [a] in Clight. Right: evaluation of its translation [ta] in Csharpminor. - Top (precondition): matching between environments [e], [te], + Top (precondition): matching between environments [e], [te], plus well-typedness of expression [a]. - Bottom (postcondition): the result values [v] + Bottom (postcondition): the result values [v] are identical in both evaluations. We state these diagrams as the following properties, parameterized @@ -947,7 +947,7 @@ Proof. (* temp var *) constructor; auto. (* addrof *) - simpl in TR. auto. + simpl in TR. auto. (* unop *) eapply transl_unop_correct; eauto. (* binop *) @@ -960,21 +960,21 @@ Proof. apply make_intconst_correct. (* rvalue out of lvalue *) exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]]. - eapply make_load_correct; eauto. + eapply make_load_correct; eauto. (* var local *) exploit (me_local _ _ MENV); eauto. intros EQ. econstructor. eapply eval_var_addr_local. eauto. (* var global *) - econstructor. eapply eval_var_addr_global. + econstructor. eapply eval_var_addr_global. eapply match_env_globals; eauto. rewrite symbols_preserved. auto. (* deref *) - simpl in TR. eauto. + simpl in TR. eauto. (* field struct *) change (prog_comp_env prog) with (genv_cenv ge) in EQ0. unfold make_field_access in EQ0; rewrite H1, H2 in EQ0; monadInv EQ0. eapply eval_Ebinop; eauto. - apply make_intconst_correct. + apply make_intconst_correct. simpl. congruence. (* field union *) unfold make_field_access in EQ0; rewrite H1 in EQ0; monadInv EQ0. @@ -1003,8 +1003,8 @@ Lemma transl_arglist_correct: Proof. induction 1; intros. monadInv H. constructor. - monadInv H2. constructor. - eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. auto. + monadInv H2. constructor. + eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. auto. Qed. Lemma typlist_of_arglist_eq: @@ -1026,9 +1026,9 @@ End EXPR. << I S1 ------- R1 - | | + | | t | + | t - v v + v v S2 ------- R2 I I >> @@ -1047,8 +1047,8 @@ Lemma match_transl_step: match_transl (Sblock ts) tk ts' tk' -> star step tge (State f ts' tk' te le m) E0 (State f ts (Kblock tk) te le m). Proof. - intros. inv H. - apply star_one. constructor. + intros. inv H. + apply star_one. constructor. apply star_refl. Qed. @@ -1084,7 +1084,7 @@ Inductive match_cont: type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> P transl_function ge f = OK tf -> match_env e te -> match_cont (Clight.fn_return f) nbrk' ncnt' k tk -> - match_cont tyret nbrk ncnt + match_cont tyret nbrk ncnt (Clight.Kcall id f e le k) (Kcall id tf te le tk). @@ -1107,7 +1107,7 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop := match_states (Clight.Callstate fd args k m) (Callstate tfd args tk m) | match_returnstate: - forall res k m tk + forall res k m tk (MK: match_cont Tvoid 0%nat 0%nat k tk), match_states (Clight.Returnstate res k m) (Returnstate res tk m). @@ -1119,7 +1119,7 @@ Remark match_states_skip: match_cont (Clight.fn_return f) nbrk ncnt k tk -> match_states (Clight.State f Clight.Sskip k e le m) (State tf Sskip tk te le m). Proof. - intros. econstructor; eauto. simpl; reflexivity. constructor. + intros. econstructor; eauto. simpl; reflexivity. constructor. Qed. (** Commutation between label resolution and compilation *) @@ -1168,13 +1168,13 @@ Proof. (* builtin *) auto. (* seq *) - exploit (transl_find_label s0 nbrk ncnt (Clight.Kseq s1 k)); eauto. constructor; eauto. + 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'] | ]. 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. (* ifthenelse *) - exploit (transl_find_label s0); eauto. + exploit (transl_find_label s0); eauto. destruct (Clight.find_label lbl s0 k) as [[s' k'] | ]. intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]]. rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. @@ -1185,20 +1185,20 @@ 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. econstructor; eauto. + eapply transl_find_label; eauto. econstructor; eauto. (* break *) auto. (* continue *) auto. (* return *) - simpl in TR. destruct o; monadInv TR. auto. auto. + simpl in TR. destruct o; monadInv TR. auto. auto. (* switch *) assert (exists b, ts = Sblock (Sswitch b x x0)). { destruct (classify_switch (typeof e)); inv EQ2; econstructor; eauto. } destruct H as [b EQ3]; rewrite EQ3; simpl. - eapply transl_find_label_ls with (k := Clight.Kswitch k); eauto. econstructor; eauto. + eapply transl_find_label_ls with (k := Clight.Kswitch k); eauto. econstructor; eauto. (* label *) - destruct (ident_eq lbl l). + destruct (ident_eq lbl l). exists x; exists tk; exists nbrk; exists ncnt; auto. eapply transl_find_label; eauto. (* goto *) @@ -1208,7 +1208,7 @@ Proof. (* nil *) auto. (* cons *) - exploit (transl_find_label s nbrk ncnt (Clight.Kseq (seq_of_labeled_statement l) k)); eauto. + exploit (transl_find_label s nbrk ncnt (Clight.Kseq (seq_of_labeled_statement l) k)); eauto. econstructor; eauto. apply transl_lbl_stmt_2; eauto. destruct (Clight.find_label lbl s (Clight.Kseq (seq_of_labeled_statement l) k)) as [[s' k'] | ]. intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]]. @@ -1228,7 +1228,7 @@ Lemma match_cont_call_cont: Proof. induction 1; simpl; auto. constructor. - econstructor; eauto. + econstructor; eauto. Qed. Lemma match_cont_is_call_cont: @@ -1254,41 +1254,41 @@ Proof. (* assign *) monadInv TR. assert (SAME: ts' = ts /\ tk' = tk). - inversion MTR. auto. + inversion MTR. auto. subst ts. unfold make_store, make_memcpy in EQ3. destruct (access_mode (typeof a1)); congruence. destruct SAME; subst ts' tk'. 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 transl_expr_correct; eauto. eapply match_states_skip; eauto. (* set *) monadInv TR. inv MTR. econstructor; split. - apply plus_one. econstructor. eapply transl_expr_correct; eauto. + apply plus_one. econstructor. eapply transl_expr_correct; eauto. eapply match_states_skip; eauto. (* call *) revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence. - intros targs tres cc CF TR. monadInv TR. inv MTR. + intros targs tres cc CF TR. monadInv TR. inv MTR. exploit functions_translated; eauto. intros [tfd [FIND TFD]]. rewrite H in CF. simpl in CF. inv CF. econstructor; split. - apply plus_one. econstructor; eauto. + apply plus_one. econstructor; eauto. exploit transl_expr_correct; eauto. exploit transl_arglist_correct; eauto. - erewrite typlist_of_arglist_eq by eauto. + erewrite typlist_of_arglist_eq by eauto. eapply transl_fundef_sig1; eauto. rewrite H3. auto. - econstructor; eauto. + econstructor; eauto. econstructor; eauto. simpl. auto. (* builtin *) - monadInv TR. inv MTR. + monadInv TR. inv MTR. econstructor; split. - apply plus_one. econstructor. - eapply transl_arglist_correct; eauto. + apply plus_one. econstructor. + eapply transl_arglist_correct; eauto. eapply external_call_symbols_preserved_gen with (ge1 := ge). exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. eauto. eapply match_states_skip; eauto. @@ -1296,31 +1296,31 @@ Proof. (* seq *) monadInv TR. inv MTR. econstructor; split. - apply plus_one. constructor. - econstructor; eauto. constructor. + apply plus_one. constructor. + econstructor; eauto. constructor. econstructor; eauto. (* skip seq *) monadInv TR. inv MTR. inv MK. econstructor; split. - apply plus_one. apply step_skip_seq. + apply plus_one. apply step_skip_seq. econstructor; eauto. constructor. (* continue seq *) monadInv TR. inv MTR. inv MK. econstructor; split. - apply plus_one. constructor. + apply plus_one. constructor. econstructor; eauto. simpl. reflexivity. constructor. (* break seq *) monadInv TR. inv MTR. inv MK. econstructor; split. - apply plus_one. constructor. + apply plus_one. constructor. econstructor; eauto. simpl. reflexivity. constructor. (* ifthenelse *) monadInv TR. inv MTR. - exploit make_boolean_correct; eauto. + exploit make_boolean_correct; eauto. exploit transl_expr_correct; eauto. intros [v [A B]]. econstructor; split. @@ -1330,12 +1330,12 @@ Proof. (* loop *) monadInv TR. econstructor; split. - eapply star_plus_trans. eapply match_transl_step; eauto. - eapply plus_left. constructor. + 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. + econstructor; eauto. constructor. econstructor; eauto. (* skip-or-continue loop *) assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). @@ -1345,7 +1345,7 @@ Proof. eapply plus_left. destruct H0; subst ts'. 2:constructor. constructor. apply star_one. constructor. traceEq. - econstructor; eauto. constructor. econstructor; eauto. + econstructor; eauto. constructor. econstructor; eauto. (* break loop1 *) monadInv TR. inv MTR. inv MK. @@ -1362,9 +1362,9 @@ Proof. econstructor; split. apply plus_one. constructor. econstructor; eauto. -Local Opaque ge. - simpl. rewrite H5; simpl. rewrite H7; simpl. eauto. - constructor. +Local Opaque ge. + simpl. rewrite H5; simpl. rewrite H7; simpl. eauto. + constructor. (* break loop2 *) monadInv TR. inv MTR. inv MK. @@ -1375,21 +1375,21 @@ Local Opaque ge. eapply match_states_skip; eauto. (* return none *) - monadInv TR. inv MTR. + monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. - eapply match_env_free_blocks; eauto. + eapply match_env_free_blocks; eauto. econstructor; eauto. - eapply match_cont_call_cont. eauto. + eapply match_cont_call_cont. eauto. (* return some *) - monadInv TR. inv MTR. + monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. eapply match_env_free_blocks; eauto. econstructor; eauto. - eapply match_cont_call_cont. eauto. + eapply match_cont_call_cont. eauto. (* skip call *) monadInv TR. inv MTR. @@ -1405,13 +1405,13 @@ Local Opaque ge. { unfold sem_switch_arg in H0. destruct (classify_switch (typeof a)); inv EQ2; econstructor; split; eauto; destruct v; inv H0; constructor. } - destruct E as (b & A & B). subst ts. + destruct E as (b & A & B). subst ts. exploit transl_expr_correct; eauto. intro EV. econstructor; split. eapply star_plus_trans. eapply match_transl_step; eauto. - apply plus_one. econstructor; eauto. traceEq. + apply plus_one. econstructor; eauto. traceEq. econstructor; eauto. - apply transl_lbl_stmt_2. apply transl_lbl_stmt_1. eauto. + apply transl_lbl_stmt_2. apply transl_lbl_stmt_1. eauto. constructor. econstructor. eauto. @@ -1427,29 +1427,29 @@ Local Opaque ge. (* continue switch *) monadInv TR. inv MTR. inv MK. econstructor; split. - apply plus_one. constructor. + apply plus_one. constructor. econstructor; eauto. simpl. reflexivity. constructor. (* label *) - monadInv TR. inv MTR. + monadInv TR. inv MTR. econstructor; split. - apply plus_one. constructor. + apply plus_one. constructor. econstructor; eauto. constructor. (* goto *) monadInv TR. inv MTR. generalize TRF. unfold transl_function. intro TRF'. monadInv TRF'. exploit (transl_find_label lbl). eexact EQ. eapply match_cont_call_cont. eauto. - rewrite H. + rewrite H. intros [ts' [tk'' [nbrk' [ncnt' [A [B C]]]]]]. econstructor; split. - apply plus_one. constructor. simpl. eexact A. + apply plus_one. constructor. simpl. eexact A. econstructor; eauto. constructor. (* internal function *) inv H. monadInv TR. monadInv EQ. exploit match_cont_is_call_cont; eauto. intros [A B]. - exploit match_env_alloc_variables; eauto. + exploit match_env_alloc_variables; eauto. apply match_env_empty. intros [te1 [C D]]. econstructor; split. @@ -1464,17 +1464,17 @@ Local Opaque ge. constructor. (* external function *) - simpl in TR. + simpl in TR. destruct (signature_eq (ef_sig ef) (signature_of_type targs tres cconv)); inv TR. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. - apply plus_one. constructor. eauto. + apply plus_one. constructor. eauto. eapply external_call_symbols_preserved_gen with (ge1 := ge). exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. eauto. econstructor; eauto. (* returnstate *) - inv MK. + inv MK. econstructor; split. apply plus_one. constructor. econstructor; eauto. simpl; reflexivity. constructor. @@ -1492,10 +1492,10 @@ Proof. change (prog_main prog) with (AST.prog_main (program_of_program prog)). eapply transform_partial_program2_main; eauto. assert (funsig tf = signature_of_type Tnil type_int32s cc_default). - eapply transl_fundef_sig2; eauto. + eapply transl_fundef_sig2; eauto. econstructor; split. - econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto. - econstructor; eauto. constructor; auto. exact I. + econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto. + econstructor; eauto. constructor; auto. exact I. Qed. Lemma transl_final_states: -- cgit