diff options
-rw-r--r-- | cfrontend/Cshmgenproof.v | 116 | ||||
-rw-r--r-- | ia32/Asmgenproof1.v | 40 | ||||
-rw-r--r-- | ia32/SelectLongproof.v | 87 |
3 files changed, 121 insertions, 122 deletions
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 3a35b87e..4f8632f2 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -37,7 +37,7 @@ Lemma transf_program_match: forall p tp, transl_program p = OK tp -> match_prog p tp. Proof. unfold transl_program; intros. - eapply match_transform_partial_program2. + eapply match_transform_partial_program2. eexact H. - intros. destruct f; simpl in H0. + monadInv H0. constructor; auto. @@ -109,7 +109,7 @@ Lemma transl_alignof_blockcopy: Proof. intros. destruct H. unfold sizeof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0. - split. + split. - symmetry. apply Ctypes.sizeof_stable; auto. - revert C. induction t; simpl; auto; destruct (prog_comp_env cunit)!i as [co|] eqn:X; try discriminate; erewrite H1 by eauto; auto. @@ -119,10 +119,10 @@ Lemma field_offset_stable: forall (cunit prog: Clight.program) id co f, linkorder cunit prog -> cunit.(prog_comp_env)!id = Some co -> - prog.(prog_comp_env)!id = Some co /\ + prog.(prog_comp_env)!id = Some co /\ field_offset prog.(prog_comp_env) f (co_members co) = field_offset cunit.(prog_comp_env) f (co_members co). Proof. - intros. + intros. assert (C: composite_consistent cunit.(prog_comp_env) co). { apply build_composite_env_consistent with cunit.(prog_types) id; auto. apply prog_comp_env_eq. } @@ -134,7 +134,7 @@ Proof. rewrite ! (alignof_stable _ _ A) by auto. rewrite ! (sizeof_stable _ _ A) by auto. destruct (ident_eq f f1); eauto. -Qed. +Qed. (** * Properties of the translation functions *) @@ -329,7 +329,7 @@ Lemma make_cmpu_ne_zero_correct_ptr: Mem.weak_valid_pointer m b (Ptrofs.unsigned i) = true -> eval_expr ge e le m (make_cmpu_ne_zero a) Vone. Proof. - intros. + intros. assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero)) Vone). { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. unfold Mem.weak_valid_pointer in H1. rewrite H0, H1. @@ -343,8 +343,8 @@ Proof. - inv H; eelim OF_OPTBOOL; eauto. - inv H; eelim OF_OPTBOOL; eauto. - inv H; eelim OF_OPTBOOL; eauto. -- inv H; eelim OF_BOOL; eauto. -- inv H; eelim OF_BOOL; eauto. +- inv H; eelim OF_BOOL; eauto. +- inv H; eelim OF_BOOL; eauto. Qed. Lemma make_cast_int_correct: @@ -365,7 +365,7 @@ Lemma make_longofint_correct: eval_expr ge e le m a (Vint n) -> eval_expr ge e le m (make_longofint a si) (Vlong (cast_int_long si n)). Proof. - intros. unfold make_longofint, cast_int_long. destruct si; eauto with cshm. + intros. unfold make_longofint, cast_int_long. destruct si; eauto with cshm. Qed. Hint Resolve make_cast_int_correct make_longofint_correct: cshm. @@ -448,13 +448,13 @@ Proof. econstructor; split. apply make_cmpu_ne_zero_correct with (n := i); auto. destruct (Int.eq i Int.zero); simpl; constructor. - (* ptr 32 bits *) - exists Vone; split. eapply make_cmpu_ne_zero_correct_ptr; eauto. constructor. + exists Vone; split. eapply make_cmpu_ne_zero_correct_ptr; eauto. constructor. - (* long *) econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmplu. simpl. eauto. destruct (Int64.eq i Int64.zero); simpl; constructor. - (* ptr 64 bits *) - exists Vone; split. - econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. + exists Vone; split. + econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. unfold Mem.weak_valid_pointer in Heqb0. rewrite Heqb0, Heqb1, Int64.eq_true. reflexivity. constructor. - (* float *) @@ -501,21 +501,21 @@ Lemma make_notbool_correct: Proof. unfold sem_notbool, bool_val, make_notbool; intros until m; intros SEM MAKE EV1. destruct (classify_bool tya); inv MAKE; destruct va; simpl in SEM; InvEval. -- econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. +- econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. destruct (Int.eq i Int.zero); auto. - destruct Archi.ptr64 eqn:SF; inv SEM. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0. - econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. + econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int.eq_true. auto. -- econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu. +- econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu. destruct (Int64.eq i Int64.zero); auto. - destruct Archi.ptr64 eqn:SF; inv SEM. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0. - econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. + econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int64.eq_true. auto. -- econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. +- econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. destruct (Float.cmp Ceq f Float.zero); auto. -- econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool. +- econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool. destruct (Float32.cmp Ceq f Float32.zero); auto. Qed. @@ -633,7 +633,7 @@ Lemma ptrofs_mul_32: Archi.ptr64 = false -> Ptrofs.of_int (Int.mul (Int.repr n) i) = Ptrofs.mul (Ptrofs.repr n) (ptrofs_of_int si i). Proof. - intros. apply Ptrofs.eqm_samerepr. + intros. apply Ptrofs.eqm_samerepr. eapply Ptrofs.eqm_trans; [ | apply Ptrofs.eqm_mult ]. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. apply Ptrofs.eqm_unsigned_repr_r. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. @@ -646,11 +646,11 @@ Lemma ptrofs_mul_32_64: Archi.ptr64 = false -> Ptrofs.of_int (Int.mul (Int.repr n) (Int64.loword i)) = Ptrofs.mul (Ptrofs.repr n) (Ptrofs.of_int64 i). Proof. - intros. apply Ptrofs.eqm_samerepr. + intros. apply Ptrofs.eqm_samerepr. eapply Ptrofs.eqm_trans; [ | apply Ptrofs.eqm_mult ]. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. apply Ptrofs.eqm_unsigned_repr_r. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. - unfold Ptrofs.of_int64. apply Ptrofs.eqm_unsigned_repr_r. + unfold Ptrofs.of_int64. apply Ptrofs.eqm_unsigned_repr_r. unfold Int64.loword. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. Qed. *) @@ -663,20 +663,20 @@ Proof. - destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. econstructor; eauto with cshm. - simpl. rewrite SF. do 3 f_equal. + simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)). { destruct si; simpl; apply Ptrofs.agree64_repr; auto. } auto with ptrofs. + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. - econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal. + econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs). auto with ptrofs. - destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. econstructor; eauto with cshm. - simpl. rewrite SF. do 3 f_equal. auto with ptrofs. + simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs. + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. - econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal. + econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto). auto with ptrofs. - eapply make_binarith_correct; eauto; intros; auto. @@ -690,17 +690,17 @@ Proof. - destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. econstructor; eauto with cshm. - simpl. rewrite SF. do 3 f_equal. + simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)). { destruct si; simpl; apply Ptrofs.agree64_repr; auto. } auto with ptrofs. + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. - econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal. + econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs). auto with ptrofs. -- rewrite (transl_sizeof _ _ _ _ LINK EQ) in EQ0. clear EQ. +- rewrite (transl_sizeof _ _ _ _ LINK EQ) in EQ0. clear EQ. set (sz := Ctypes.sizeof (prog_comp_env prog) ty) in *. - destruct va; InvEval; destruct vb; InvEval. + destruct va; InvEval; destruct vb; InvEval. destruct (eq_block b0 b1); try discriminate. destruct (zlt 0 sz); try discriminate. destruct (zle sz Ptrofs.max_signed); simpl in SEM; inv SEM. @@ -709,37 +709,37 @@ Proof. destruct Archi.ptr64 eqn:SF; inversion EQ0; clear EQ0; subst c. + assert (E: Int64.signed (Int64.repr sz) = sz). { apply Int64.signed_repr. - replace Int64.max_signed with Ptrofs.max_signed. + replace Int64.max_signed with Ptrofs.max_signed. generalize Int64.min_signed_neg; omega. unfold Ptrofs.max_signed, Ptrofs.half_modulus; rewrite Ptrofs.modulus_eq64 by auto. reflexivity. } econstructor; eauto with cshm. - rewrite SF, dec_eq_true. simpl. + rewrite SF, dec_eq_true. simpl. predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.zero. rewrite H in E; rewrite Int64.signed_zero in E; omegaContradiction. predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.mone. rewrite H0 in E; rewrite Int64.signed_mone in E; omegaContradiction. - rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. do 2 f_equal. - symmetry. auto with ptrofs. + rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal. + apply f_equal. symmetry. auto with ptrofs. + assert (E: Int.signed (Int.repr sz) = sz). { apply Int.signed_repr. - replace Int.max_signed with Ptrofs.max_signed. + replace Int.max_signed with Ptrofs.max_signed. generalize Int.min_signed_neg; omega. - unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. rewrite SF. reflexivity. + unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. rewrite SF. reflexivity. } - econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl. + econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl. 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; simpl. unfold Vptrofs; rewrite SF. do 2 f_equal. + rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal. apply f_equal. symmetry. auto with ptrofs. - destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. econstructor; eauto with cshm. - simpl. rewrite SF. do 3 f_equal. + simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs. + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. - econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal. + econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto). auto with ptrofs. - eapply make_binarith_correct; eauto; intros; auto. @@ -867,7 +867,7 @@ Proof. unfold cmp_ptr, make_cmp_ptr; intros. destruct Archi.ptr64. - econstructor; eauto. -- econstructor; eauto. simpl. unfold Val.cmpu. +- econstructor; eauto. simpl. unfold Val.cmpu. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bo|]; inv H. auto. Qed. @@ -880,15 +880,15 @@ Proof. - unfold make_longofint. destruct si. + replace (Ptrofs.to_int64 (Ptrofs.of_ints i)) with (Int64.repr (Int.signed i)). eauto with cshm. - apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. + apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. + replace (Ptrofs.to_int64 (Ptrofs.of_intu i)) with (Int64.repr (Int.unsigned i)). eauto with cshm. - apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. + apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. - destruct si. + replace (Ptrofs.to_int (Ptrofs.of_ints i)) with i. auto. - symmetry. auto with ptrofs. + symmetry. auto with ptrofs. + replace (Ptrofs.to_int (Ptrofs.of_intu i)) with i. auto. - symmetry. auto with ptrofs. + symmetry. auto with ptrofs. Qed. Remark make_ptrofs_of_int64_correct: @@ -899,7 +899,7 @@ Proof. intros. unfold Vptrofs. destruct Archi.ptr64 eqn:SF. - replace (Ptrofs.to_int64 (Ptrofs.of_int64 i)) with i. auto. symmetry. auto with ptrofs. -- econstructor; eauto. simpl. do 2 f_equal. +- econstructor; eauto. simpl. apply f_equal. apply f_equal. apply Int.eqm_samerepr. rewrite Ptrofs.eqm32 by auto. apply Ptrofs.eqm_unsigned_repr. Qed. @@ -983,7 +983,7 @@ Lemma make_memcpy_correct: step ge (State f s k e le m) E0 (State f Sskip k e le m'). Proof. intros. inv H1; try congruence. - monadInv H3. + monadInv H3. exploit transl_alignof_blockcopy. eexact LINK. eauto. intros [A B]. rewrite A, B. change le with (set_optvar None Vundef le) at 2. econstructor. @@ -1131,8 +1131,8 @@ Lemma match_env_alloc_variables: Proof. induction 2; simpl; intros. - inv H0. exists te1; split. constructor. auto. -- monadInv H2. monadInv EQ. simpl in *. - exploit transl_sizeof. eexact H. eauto. intros SZ; rewrite SZ. +- monadInv H2. monadInv EQ. simpl in *. + exploit transl_sizeof. eexact H. eauto. intros SZ; rewrite SZ. exploit (IHalloc_variables x0 (PTree.set id (b1, Ctypes.sizeof ge ty) te1)). auto. constructor. @@ -1254,7 +1254,7 @@ Proof. - (* deref *) simpl in TR. eauto. - (* field struct *) - unfold make_field_access in EQ0. rewrite H1 in EQ0. + unfold make_field_access in EQ0. rewrite H1 in EQ0. destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; monadInv EQ0. exploit field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B]. rewrite <- B in EQ1. @@ -1262,9 +1262,9 @@ Proof. subst x0. destruct Archi.ptr64 eqn:SF. + eapply eval_Ebinop; eauto using make_longconst_correct. - simpl. rewrite SF. do 3 f_equal. auto with ptrofs. + simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs. + eapply eval_Ebinop; eauto using make_intconst_correct. - simpl. rewrite SF. do 3 f_equal. auto with ptrofs. + simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs. - (* field union *) unfold make_field_access in EQ0; rewrite H1 in EQ0; monadInv EQ0. auto. @@ -1570,7 +1570,7 @@ Proof. rewrite H in CF. simpl in CF. inv CF. econstructor; split. apply plus_one. econstructor; eauto. - eapply transl_expr_correct with (cunit := cu); eauto. + eapply transl_expr_correct with (cunit := cu); eauto. eapply transl_arglist_correct with (cunit := cu); eauto. erewrite typlist_of_arglist_eq by eauto. eapply transl_fundef_sig1; eauto. @@ -1739,7 +1739,7 @@ Proof. econstructor; eauto. constructor. - (* internal function *) - inv H. inv TR. monadInv H5. + inv H. inv TR. monadInv H5. exploit match_cont_is_call_cont; eauto. intros [A B]. exploit match_env_alloc_variables; eauto. apply match_env_empty. @@ -1749,7 +1749,7 @@ Proof. simpl. erewrite transl_vars_names by eauto. assumption. simpl. assumption. simpl. assumption. - simpl; eauto. + simpl; eauto. simpl. rewrite create_undef_temps_match. eapply bind_parameter_temps_match; eauto. simpl. econstructor; eauto. unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto. @@ -1809,7 +1809,7 @@ End CORRECTNESS. Instance TransfCshmgenLink : TransfLink match_prog. Proof. red; intros. destruct (link_linkorder _ _ _ H) as (LO1 & LO2). - generalize H. + generalize H. Local Transparent Ctypes.Linker_program. simpl; unfold link_program. destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate. @@ -1819,15 +1819,15 @@ Local Transparent Ctypes.Linker_program. (prog_comp_env_eq p2) EQ) as (env & P & Q). intros E. eapply Linking.link_match_program; eauto. -- intros. +- intros. Local Transparent Linker_fundef Linking.Linker_fundef. - inv H3; inv H4; simpl in H2. + inv H3; inv H4; simpl in H2. + discriminate. + destruct ef; inv H2. econstructor; split. simpl; eauto. left; constructor; auto. + destruct ef; inv H2. econstructor; split. simpl; eauto. right; constructor; auto. + destruct (external_function_eq ef ef0 && typelist_eq args args0 && type_eq res res0 && calling_convention_eq cc cc0) eqn:E'; inv H2. - InvBooleans. subst ef0. econstructor; split. + InvBooleans. subst ef0. econstructor; split. simpl; rewrite dec_eq_true; eauto. left; constructor. congruence. - intros. exists tt. auto. diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 99d0680d..4effe7c9 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -142,7 +142,7 @@ Proof. || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone) eqn:OK; try (intuition discriminate). intros _. - InvBooleans. + InvBooleans. exists (Int.shr i (Int.repr 31)), i, i0, (Int.divs i i0), (Int.mods i i0); intuition auto. rewrite Int.shr_lt_zero. apply Int.divmods2_divs_mods. red; intros; subst i0; rewrite Int.eq_true in H; discriminate. @@ -182,7 +182,7 @@ Proof. || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone) eqn:OK; try (intuition discriminate). intros _. - InvBooleans. + InvBooleans. exists (Int64.shr i (Int64.repr 63)), i, i0, (Int64.divs i i0), (Int64.mods i i0); intuition auto. rewrite Int64.shr_lt_zero. apply Int64.divmods2_divs_mods. red; intros; subst i0; rewrite Int64.eq_true in H; discriminate. @@ -314,7 +314,7 @@ Proof. unfold mk_storebyte; intros. destruct (Archi.ptr64 || low_ireg r) eqn:E. (* low reg *) - monadInv H. econstructor; split. apply exec_straight_one. + monadInv H. econstructor; split. apply exec_straight_one. simpl. unfold exec_store. rewrite H0. eauto. auto. intros; Simplifs. (* high reg *) @@ -333,7 +333,7 @@ Proof. replace (Val.add (eval_addrmode32 ge addr rs1) (Vint Int.zero)) with (eval_addrmode ge addr rs1). rewrite H0. eauto. - unfold eval_addrmode in *; rewrite H1 in *. + unfold eval_addrmode in *; rewrite H1 in *. destruct (eval_addrmode32 ge addr rs1); simpl in H0; try discriminate. simpl. rewrite H1. rewrite Ptrofs.add_zero; auto. auto. auto. auto. @@ -358,10 +358,10 @@ Remark eval_addrmode_indexed: match rs#base with Vptr _ _ => True | _ => False end -> eval_addrmode ge (Addrmode (Some base) None (inl _ (Ptrofs.unsigned ofs))) rs = Val.offset_ptr rs#base ofs. Proof. - intros. destruct (rs#base) eqn:BASE; try contradiction. + intros. destruct (rs#base) eqn:BASE; try contradiction. intros; unfold eval_addrmode; destruct Archi.ptr64 eqn:SF; simpl; rewrite BASE; simpl; rewrite SF; simpl. -- do 2 f_equal. rewrite Int64.add_zero_l. rewrite <- (Ptrofs.repr_unsigned ofs) at 2. auto with ptrofs. -- do 2 f_equal. rewrite Int.add_zero_l. rewrite <- (Ptrofs.repr_unsigned ofs) at 2. auto with ptrofs. +- apply f_equal. apply f_equal. rewrite Int64.add_zero_l. rewrite <- (Ptrofs.repr_unsigned ofs) at 2. auto with ptrofs. +- apply f_equal. apply f_equal. rewrite Int.add_zero_l. rewrite <- (Ptrofs.repr_unsigned ofs) at 2. auto with ptrofs. Qed. Ltac loadind_correct_solve := @@ -420,7 +420,7 @@ Lemma transl_addressing_mode_32_correct: Proof. assert (A: forall id ofs, Archi.ptr64 = false -> Val.add (Vint Int.zero) (Genv.symbol_address ge id ofs) = Genv.symbol_address ge id ofs). - { intros. unfold Val.add; rewrite H. unfold Genv.symbol_address. + { intros. unfold Val.add; rewrite H. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id); auto. rewrite Ptrofs.add_zero; auto. } assert (C: forall v i, Val.lessdef (Val.mul v (Vint (Int.repr i))) @@ -440,7 +440,7 @@ Proof. - destruct Archi.ptr64 eqn:SF; inv H2. erewrite ireg_of_eq by eauto. rewrite Val.add_permut. rewrite Val.add_commut. apply Val.add_lessdef; auto. rewrite A; auto. - destruct Archi.ptr64 eqn:SF; inv H2. simpl. - destruct (rs RSP); simpl; auto; rewrite SF. + destruct (rs RSP); simpl; auto; rewrite SF. rewrite Int.add_zero_l. apply Val.lessdef_same; f_equal; f_equal. symmetry. transitivity (Ptrofs.repr (Ptrofs.signed i)). auto with ptrofs. auto with ints. Qed. @@ -453,7 +453,7 @@ Lemma transl_addressing_mode_64_correct: Proof. assert (A: forall id ofs, Archi.ptr64 = true -> Val.addl (Vlong Int64.zero) (Genv.symbol_address ge id ofs) = Genv.symbol_address ge id ofs). - { intros. unfold Val.addl; rewrite H. unfold Genv.symbol_address. + { intros. unfold Val.addl; rewrite H. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id); auto. rewrite Ptrofs.add_zero; auto. } assert (C: forall v i, Val.lessdef (Val.mull v (Vlong (Int64.repr i))) @@ -469,7 +469,7 @@ Proof. - apply Val.addl_lessdef; auto. apply Val.addl_lessdef; auto. - destruct Archi.ptr64 eqn:SF; inv H2. rewrite ! A by auto. auto. - destruct Archi.ptr64 eqn:SF; inv H2. simpl. - destruct (rs RSP); simpl; auto; rewrite SF. + destruct (rs RSP); simpl; auto; rewrite SF. rewrite Int64.add_zero_l. apply Val.lessdef_same; f_equal; f_equal. symmetry. transitivity (Ptrofs.repr (Ptrofs.signed i)). auto with ptrofs. auto with ints. Qed. @@ -480,7 +480,7 @@ Lemma transl_addressing_mode_correct: eval_addressing ge (rs RSP) addr (List.map rs (List.map preg_of args)) = Some v -> Val.lessdef v (eval_addrmode ge am rs). Proof. - unfold eval_addressing, eval_addrmode; intros. destruct Archi.ptr64. + unfold eval_addressing, eval_addrmode; intros. destruct Archi.ptr64. eapply transl_addressing_mode_64_correct; eauto. eapply transl_addressing_mode_32_correct; eauto. Qed. @@ -492,16 +492,16 @@ Proof. Qed. Lemma normalize_addrmode_64_correct: - forall am rs, + forall am rs, eval_addrmode64 ge am rs = match normalize_addrmode_64 am with | (am', None) => eval_addrmode64 ge am' rs | (am', Some delta) => Val.addl (eval_addrmode64 ge am' rs) (Vlong delta) end. Proof. - intros; destruct am as [base ofs [n|r]]; simpl; auto. + intros; destruct am as [base ofs [n|r]]; simpl; auto. destruct (zeq (Int.signed (Int.repr n)) n); simpl; auto. - rewrite ! Val.addl_assoc. do 2 f_equal. simpl. rewrite Int64.add_zero_l; auto. + rewrite ! Val.addl_assoc. apply f_equal. apply f_equal. simpl. rewrite Int64.add_zero_l; auto. Qed. (** Processor conditions and comparisons *) @@ -657,7 +657,7 @@ Proof. intros. generalize (compare_longs_spec rs v1 v2 m). set (rs' := nextinstr (compare_longs v1 v2 rs m)). intros [A [B [C [D E]]]]. - unfold eval_testcond. rewrite A; rewrite B. + unfold eval_testcond. rewrite A; rewrite B. destruct v1; destruct v2; simpl in H; inv H. - (* int int *) destruct c; simpl; auto. @@ -1365,11 +1365,11 @@ Transparent destroyed_by_op. (* leal *) exploit transl_addressing_mode_64_correct; eauto. intros EA. generalize (normalize_addrmode_64_correct x rs). destruct (normalize_addrmode_64 x) as [am' [delta|]]; intros EV. - econstructor; split. eapply exec_straight_two. - simpl. reflexivity. simpl. reflexivity. auto. auto. + econstructor; split. eapply exec_straight_two. + simpl. reflexivity. simpl. reflexivity. auto. auto. split. rewrite nextinstr_nf_inv by auto. rewrite Pregmap.gss. rewrite nextinstr_inv by auto with asmgen. rewrite Pregmap.gss. rewrite <- EV; auto. - intros; Simplifs. + intros; Simplifs. TranslOp. rewrite nextinstr_inv; auto with asmgen. rewrite Pregmap.gss; auto. rewrite <- EV; auto. (* intoffloat *) apply SAME. TranslOp. rewrite H0; auto. @@ -1475,5 +1475,3 @@ Proof. Qed. End CONSTRUCTORS. - - diff --git a/ia32/SelectLongproof.v b/ia32/SelectLongproof.v index fced9a07..4cd15fd3 100644 --- a/ia32/SelectLongproof.v +++ b/ia32/SelectLongproof.v @@ -64,7 +64,7 @@ Proof. unfold longconst; intros; destruct Archi.splitlong. apply SplitLongproof.eval_longconst. EvalOp. -Qed. +Qed. Lemma is_longconst_sound_1: forall a n, is_longconst a = Some n -> a = Eop (Olongconst n) Enil. @@ -83,46 +83,46 @@ Theorem eval_intoflong: unary_constructor_sound intoflong Val.loword. Proof. unfold intoflong; destruct Archi.splitlong. apply SplitLongproof.eval_intoflong. red; intros. destruct (is_longconst a) as [n|] eqn:C. -- TrivialExists. simpl. erewrite (is_longconst_sound x) by eauto. auto. -- TrivialExists. -Qed. +- TrivialExists. simpl. erewrite (is_longconst_sound x) by eauto. auto. +- TrivialExists. +Qed. Theorem eval_longofintu: unary_constructor_sound longofintu Val.longofintu. Proof. unfold longofintu; destruct Archi.splitlong. apply SplitLongproof.eval_longofintu. red; intros. destruct (is_intconst a) as [n|] eqn:C. -- econstructor; split. apply eval_longconst. +- econstructor; split. apply eval_longconst. exploit is_intconst_sound; eauto. intros; subst x. auto. -- TrivialExists. -Qed. +- TrivialExists. +Qed. Theorem eval_longofint: unary_constructor_sound longofint Val.longofint. Proof. unfold longofint; destruct Archi.splitlong. apply SplitLongproof.eval_longofint. red; intros. destruct (is_intconst a) as [n|] eqn:C. -- econstructor; split. apply eval_longconst. +- econstructor; split. apply eval_longconst. exploit is_intconst_sound; eauto. intros; subst x. auto. -- TrivialExists. -Qed. +- TrivialExists. +Qed. Theorem eval_notl: unary_constructor_sound notl Val.notl. Proof. unfold notl; destruct Archi.splitlong. apply SplitLongproof.eval_notl. - red; intros. destruct (notl_match a). + red; intros. destruct (notl_match a). - InvEval. econstructor; split. apply eval_longconst. auto. - InvEval. subst. exists v1; split; auto. destruct v1; simpl; auto. rewrite Int64.not_involutive; auto. -- TrivialExists. -Qed. +- TrivialExists. +Qed. Theorem eval_andlimm: forall n, unary_constructor_sound (andlimm n) (fun v => Val.andl v (Vlong n)). Proof. - unfold andlimm; intros; red; intros. + unfold andlimm; intros; red; intros. predSpec Int64.eq Int64.eq_spec n Int64.zero. - exists (Vlong Int64.zero); split. apply eval_longconst. - subst. destruct x; simpl; auto. rewrite Int64.and_zero; auto. + exists (Vlong Int64.zero); split. apply eval_longconst. + subst. destruct x; simpl; auto. rewrite Int64.and_zero; auto. predSpec Int64.eq Int64.eq_spec n Int64.mone. exists x; split. assumption. - subst. destruct x; simpl; auto. rewrite Int64.and_mone; auto. + subst. destruct x; simpl; auto. rewrite Int64.and_mone; auto. destruct (andlimm_match a); InvEval; subst. - econstructor; split. apply eval_longconst. simpl. rewrite Int64.and_commut; auto. - TrivialExists. simpl. rewrite Val.andl_assoc. rewrite Int64.and_commut; auto. @@ -131,7 +131,7 @@ Qed. Theorem eval_andl: binary_constructor_sound andl Val.andl. Proof. - unfold andl; destruct Archi.splitlong. apply SplitLongproof.eval_andl. + unfold andl; destruct Archi.splitlong. apply SplitLongproof.eval_andl. red; intros. destruct (andl_match a b). - InvEval. rewrite Val.andl_commut. apply eval_andlimm; auto. - InvEval. apply eval_andlimm; auto. @@ -140,7 +140,7 @@ Qed. Theorem eval_orlimm: forall n, unary_constructor_sound (orlimm n) (fun v => Val.orl v (Vlong n)). Proof. - unfold orlimm; intros; red; intros. + unfold orlimm; intros; red; intros. predSpec Int64.eq Int64.eq_spec n Int64.zero. exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.or_zero; auto. predSpec Int64.eq Int64.eq_spec n Int64.mone. @@ -153,7 +153,7 @@ Qed. Theorem eval_orl: binary_constructor_sound orl Val.orl. Proof. - unfold orl; destruct Archi.splitlong. apply SplitLongproof.eval_orl. + unfold orl; destruct Archi.splitlong. apply SplitLongproof.eval_orl. red; intros. assert (DEFAULT: exists v, eval_expr ge sp e m le (Eop Oorl (a:::b:::Enil)) v /\ Val.lessdef (Val.orl x y) v) by TrivialExists. assert (ROR: forall v n1 n2, @@ -180,23 +180,24 @@ Qed. Theorem eval_xorlimm: forall n, unary_constructor_sound (xorlimm n) (fun v => Val.xorl v (Vlong n)). Proof. - unfold xorlimm; intros; red; intros. + unfold xorlimm; intros; red; intros. predSpec Int64.eq Int64.eq_spec n Int64.zero. exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.xor_zero; auto. predSpec Int64.eq Int64.eq_spec n Int64.mone. replace (Val.xorl x (Vlong n)) with (Val.notl x). apply eval_notl; auto. - subst n. destruct x; simpl; auto. + subst n. destruct x; simpl; auto. destruct (xorlimm_match a); InvEval; subst. - econstructor; split. apply eval_longconst. simpl. rewrite Int64.xor_commut; auto. - TrivialExists. simpl. rewrite Val.xorl_assoc. rewrite Int64.xor_commut; auto. - TrivialExists. simpl. destruct v1; simpl; auto. unfold Int64.not. - rewrite Int64.xor_assoc. do 3 f_equal. apply Int64.xor_commut. + rewrite Int64.xor_assoc. apply f_equal. apply f_equal. apply f_equal. + apply Int64.xor_commut. - TrivialExists. Qed. Theorem eval_xorl: binary_constructor_sound xorl Val.xorl. Proof. - unfold xorl; destruct Archi.splitlong. apply SplitLongproof.eval_xorl. + unfold xorl; destruct Archi.splitlong. apply SplitLongproof.eval_xorl. red; intros. destruct (xorl_match a b). - InvEval. rewrite Val.xorl_commut. apply eval_xorlimm; auto. - InvEval. apply eval_xorlimm; auto. @@ -305,19 +306,19 @@ Theorem eval_negl: unary_constructor_sound negl Val.negl. Proof. unfold negl. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_negl; auto. red; intros. destruct (is_longconst a) as [n|] eqn:C. -- exploit is_longconst_sound; eauto. intros EQ; subst x. +- exploit is_longconst_sound; eauto. intros EQ; subst x. econstructor; split. apply eval_longconst. auto. - TrivialExists. -Qed. +Qed. Theorem eval_addlimm: forall n, unary_constructor_sound (addlimm n) (fun v => Val.addl v (Vlong n)). Proof. - unfold addlimm; intros; red; intros. + unfold addlimm; intros; red; intros. predSpec Int64.eq Int64.eq_spec n Int64.zero. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int64.add_zero; auto. - destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto. + destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto. destruct (addlimm_match a); InvEval. - econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto. - inv H. simpl in H6. TrivialExists. simpl. @@ -332,10 +333,10 @@ Proof. assert (B: forall id ofs n, Archi.ptr64 = true -> Genv.symbol_address ge id (Ptrofs.add ofs (Ptrofs.repr n)) = Val.addl (Genv.symbol_address ge id ofs) (Vlong (Int64.repr n))). - { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int64 (Int64.repr n)) by auto with ptrofs. + { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int64 (Int64.repr n)) by auto with ptrofs. apply Genv.shift_symbol_address_64; auto. } unfold addl. destruct Archi.splitlong eqn:SL. - apply SplitLongproof.eval_addl. apply Archi.splitlong_ptr32; auto. + apply SplitLongproof.eval_addl. apply Archi.splitlong_ptr32; auto. red; intros; destruct (addl_match a b); InvEval. - rewrite Val.addl_commut. apply eval_addlimm; auto. - apply eval_addlimm; auto. @@ -373,7 +374,7 @@ Qed. Theorem eval_mullimm_base: forall n, unary_constructor_sound (mullimm_base n) (fun v => Val.mull v (Vlong n)). Proof. - intros; unfold mullimm_base. red; intros. + intros; unfold mullimm_base. red; intros. generalize (Int64.one_bits'_decomp n); intros D. destruct (Int64.one_bits' n) as [ | i [ | j [ | ? ? ]]] eqn:B. - TrivialExists. @@ -416,7 +417,7 @@ Proof. rewrite (Int64.mul_commut n). auto. destruct Archi.ptr64; auto. - apply eval_mullimm_base; auto. -Qed. +Qed. Theorem eval_mull: binary_constructor_sound mull Val.mull. Proof. @@ -442,28 +443,28 @@ Proof. Qed. Theorem eval_divls_base: partial_binary_constructor_sound divls_base Val.divls. -Proof. +Proof. unfold divls_base; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_divls_base; eauto. TrivialExists. Qed. Theorem eval_modls_base: partial_binary_constructor_sound modls_base Val.modls. -Proof. +Proof. unfold modls_base; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_modls_base; eauto. TrivialExists. Qed. - + Theorem eval_divlu_base: partial_binary_constructor_sound divlu_base Val.divlu. -Proof. +Proof. unfold divlu_base; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_divlu_base; eauto. TrivialExists. Qed. Theorem eval_modlu_base: partial_binary_constructor_sound modlu_base Val.modlu. -Proof. +Proof. unfold modlu_base; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_modlu_base; eauto. TrivialExists. @@ -476,7 +477,7 @@ Theorem eval_cmplu: Val.cmplu (Mem.valid_pointer m) c x y = Some v -> eval_expr ge sp e m le (cmplu c a b) v. Proof. - unfold cmplu; intros. destruct Archi.splitlong eqn:SL. + unfold cmplu; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_cmplu; eauto. apply Archi.splitlong_ptr32; auto. unfold Val.cmplu in H1. destruct (Val.cmplu_bool (Mem.valid_pointer m) c x y) as [vb|] eqn:C; simpl in H1; inv H1. @@ -497,7 +498,7 @@ Theorem eval_cmpl: Val.cmpl c x y = Some v -> eval_expr ge sp e m le (cmpl c a b) v. Proof. - unfold cmpl; intros. destruct Archi.splitlong eqn:SL. + unfold cmpl; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_cmpl; eauto. unfold Val.cmpl in H1. destruct (Val.cmpl_bool c x y) as [vb|] eqn:C; simpl in H1; inv H1. @@ -516,27 +517,27 @@ Proof. unfold longoffloat; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longoffloat; eauto. TrivialExists. -Qed. +Qed. Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong. Proof. unfold floatoflong; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_floatoflong; eauto. TrivialExists. -Qed. +Qed. Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle. Proof. unfold longofsingle; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longofsingle; eauto. TrivialExists. -Qed. +Qed. Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong. Proof. unfold singleoflong; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_singleoflong; eauto. TrivialExists. -Qed. +Qed. End CMCONSTR. |