From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 18:22:00 +0200 Subject: Replace `omega` tactic with `lia` Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. --- powerpc/Asm.v | 2 +- powerpc/Asmgenproof.v | 18 +++++++++--------- powerpc/Asmgenproof1.v | 46 +++++++++++++++++++++++----------------------- powerpc/ConstpropOpproof.v | 2 +- powerpc/Conventions1.v | 44 ++++++++++++++++++++++---------------------- powerpc/NeedOp.v | 4 ++-- powerpc/SelectLongproof.v | 6 +++--- powerpc/SelectOpproof.v | 4 ++-- powerpc/Stacklayout.v | 36 ++++++++++++++++++------------------ 9 files changed, 81 insertions(+), 81 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index d9901960..93bc31b8 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -1276,7 +1276,7 @@ Ltac Equalities := split. auto. intros. destruct B; auto. subst. auto. (* trace length *) red; intros. inv H; simpl. - omega. + lia. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. (* initial states *) diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index a1ae5855..23071756 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -69,7 +69,7 @@ Lemma transf_function_no_overflow: transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned. Proof. intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. - omega. + lia. Qed. Lemma exec_straight_exec: @@ -401,8 +401,8 @@ Proof. split. unfold goto_label. rewrite P. rewrite H1. auto. split. rewrite Pregmap.gss. constructor; auto. rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. - auto. omega. - generalize (transf_function_no_overflow _ _ H0). omega. + auto. lia. + generalize (transf_function_no_overflow _ _ H0). lia. intros. apply Pregmap.gso; auto. Qed. @@ -926,14 +926,14 @@ Local Transparent destroyed_by_jumptable. simpl const_low. rewrite ATLR. erewrite storev_offset_ptr by eexact P. auto. congruence. auto. auto. auto. left; exists (State rs5 m3'); split. - eapply exec_straight_steps_1; eauto. omega. constructor. + eapply exec_straight_steps_1; eauto. lia. constructor. econstructor; eauto. change (rs5 PC) with (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one) Ptrofs.one) Ptrofs.one). rewrite ATPC. simpl. constructor; eauto. - eapply code_tail_next_int. omega. - eapply code_tail_next_int. omega. - eapply code_tail_next_int. omega. - eapply code_tail_next_int. omega. + eapply code_tail_next_int. lia. + eapply code_tail_next_int. lia. + eapply code_tail_next_int. lia. + eapply code_tail_next_int. lia. constructor. unfold rs5, rs4, rs3, rs2. apply agree_nextinstr. apply agree_nextinstr. @@ -958,7 +958,7 @@ Local Transparent destroyed_by_jumptable. - (* return *) inv STACKS. simpl in *. - right. split. omega. split. auto. + right. split. lia. split. auto. rewrite <- ATPC in H5. econstructor; eauto. congruence. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 0442f7e8..14ca22f9 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -81,12 +81,12 @@ Proof. unfold Int.modu, Int.zero. decEq. change 0 with (0 mod 65536). change (Int.unsigned (Int.repr 65536)) with 65536. - apply eqmod_mod_eq. omega. + apply eqmod_mod_eq. lia. unfold x, low_s. eapply eqmod_trans. apply eqmod_divides with Int.modulus. unfold Int.sub. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. exists 65536. compute; auto. - replace 0 with (Int.unsigned n - Int.unsigned n) by omega. + replace 0 with (Int.unsigned n - Int.unsigned n) by lia. apply eqmod_sub. apply eqmod_refl. apply Int.eqmod_sign_ext'. compute; auto. rewrite H0 in H. rewrite Int.add_zero in H. @@ -543,7 +543,7 @@ Proof. - econstructor; split; [|split]. + apply exec_straight_one. simpl; eauto. auto. + Simpl. rewrite Int64.add_zero_l. rewrite H. unfold low64_s. - rewrite Int64.sign_ext_widen by omega. auto. + rewrite Int64.sign_ext_widen by lia. auto. + intros; Simpl. - econstructor; split; [|split]. + eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. @@ -551,16 +551,16 @@ Proof. apply Int64.same_bits_eq; intros. assert (Int64.zwordsize = 64) by auto. rewrite Int64.bits_or, Int64.bits_shl by auto. unfold low64_s, low64_u. - rewrite Int64.bits_zero_ext by omega. + rewrite Int64.bits_zero_ext by lia. change (Int64.unsigned (Int64.repr 16)) with 16. destruct (zlt i 16). - * rewrite Int64.bits_sign_ext by omega. rewrite zlt_true by omega. auto. - * rewrite ! Int64.bits_sign_ext by omega. rewrite orb_false_r. + * rewrite Int64.bits_sign_ext by lia. rewrite zlt_true by lia. auto. + * rewrite ! Int64.bits_sign_ext by lia. rewrite orb_false_r. destruct (zlt i 32). - ** rewrite zlt_true by omega. rewrite Int64.bits_shr by omega. + ** rewrite zlt_true by lia. rewrite Int64.bits_shr by lia. change (Int64.unsigned (Int64.repr 16)) with 16. - rewrite zlt_true by omega. f_equal; omega. - ** rewrite zlt_false by omega. rewrite Int64.bits_shr by omega. + rewrite zlt_true by lia. f_equal; lia. + ** rewrite zlt_false by lia. rewrite Int64.bits_shr by lia. change (Int64.unsigned (Int64.repr 16)) with 16. reflexivity. + intros; Simpl. @@ -605,11 +605,11 @@ Proof. rewrite Int64.bits_shl by auto. change (Int64.unsigned (Int64.repr 32)) with 32. destruct (zlt i 32); auto. - rewrite Int64.bits_sign_ext by omega. - rewrite zlt_true by omega. - unfold n2. rewrite Int64.bits_shru by omega. + rewrite Int64.bits_sign_ext by lia. + rewrite zlt_true by lia. + unfold n2. rewrite Int64.bits_shru by lia. change (Int64.unsigned (Int64.repr 32)) with 32. - rewrite zlt_true by omega. f_equal; omega. + rewrite zlt_true by lia. f_equal; lia. } assert (MI: forall i, 0 <= i < Int64.zwordsize -> Int64.testbit mi i = @@ -619,21 +619,21 @@ Proof. rewrite Int64.bits_shl by auto. change (Int64.unsigned (Int64.repr 16)) with 16. destruct (zlt i 16); auto. - unfold n1. rewrite Int64.bits_zero_ext by omega. - rewrite Int64.bits_shru by omega. + unfold n1. rewrite Int64.bits_zero_ext by lia. + rewrite Int64.bits_shru by lia. destruct (zlt i 32). - rewrite zlt_true by omega. + rewrite zlt_true by lia. change (Int64.unsigned (Int64.repr 16)) with 16. - rewrite zlt_true by omega. f_equal; omega. - rewrite zlt_false by omega. auto. + rewrite zlt_true by lia. f_equal; lia. + rewrite zlt_false by lia. auto. } assert (EQ: Int64.or (Int64.or hi mi) n0 = n). { apply Int64.same_bits_eq; intros. rewrite ! Int64.bits_or by auto. - unfold n0; rewrite Int64.bits_zero_ext by omega. + unfold n0; rewrite Int64.bits_zero_ext by lia. rewrite HI, MI by auto. destruct (zlt i 16). - rewrite zlt_true by omega. auto. + rewrite zlt_true by lia. auto. destruct (zlt i 32); rewrite ! orb_false_r; auto. } edestruct (loadimm64_32s_correct r n2) as (rs' & A & B & C). @@ -1180,7 +1180,7 @@ Local Transparent Int.repr. rewrite H2. apply Int.mkint_eq; reflexivity. rewrite Int.not_involutive in H3. congruence. - omega. + lia. Qed. Remark add_carry_ne0: @@ -1198,8 +1198,8 @@ Transparent Int.eq. rewrite Int.unsigned_zero. rewrite Int.unsigned_mone. unfold negb, Val.of_bool, Vtrue, Vfalse. destruct (zeq (Int.unsigned i) 0); decEq. - apply zlt_true. omega. - apply zlt_false. generalize (Int.unsigned_range i). omega. + apply zlt_true. lia. + apply zlt_false. generalize (Int.unsigned_range i). lia. Qed. Lemma transl_cond_op_correct: diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 8687b056..1dd2e0e4 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -374,7 +374,7 @@ Proof. Int.bit_solve. destruct (zlt i0 n0). replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)). rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. - rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. + rewrite <- EQ. rewrite Int.bits_zero_ext by lia. rewrite zlt_true by auto. rewrite Int.bits_not by auto. apply negb_involutive. rewrite H6 by auto. auto. econstructor; split; eauto. auto. diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 5c9cbd4f..045eb471 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -268,7 +268,7 @@ Remark loc_arguments_rec_charact: forall_rpair (loc_argument_charact ofs) p. Proof. assert (X: forall ofs1 ofs2 l, loc_argument_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } + { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact ofs1) p). { destruct p; simpl; intuition eauto. } Opaque list_nth_z. @@ -279,52 +279,52 @@ Opaque list_nth_z. destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H. subst. left. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. apply Z.divide_1_l. - eapply Y; eauto. omega. + subst. split. lia. apply Z.divide_1_l. + eapply Y; eauto. lia. - (* float *) - assert (ofs <= align ofs 2) by (apply align_le; omega). + assert (ofs <= align ofs 2) by (apply align_le; lia). destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. apply Z.divide_1_l. - eapply Y; eauto. omega. + subst. split. lia. apply Z.divide_1_l. + eapply Y; eauto. lia. - (* long *) - assert (ofs <= align ofs 2) by (apply align_le; omega). + assert (ofs <= align ofs 2) by (apply align_le; lia). set (ir' := align ir 2) in *. destruct (list_nth_z int_param_regs ir') as [r1|] eqn:E1. destruct (list_nth_z int_param_regs (ir' + 1)) as [r2|] eqn:E2. destruct H. subst; split; left; eapply list_nth_z_in; eauto. eapply IHtyl; eauto. destruct H. - subst. destruct Archi.ptr64; [split|split;split]; try omega. - apply align_divides; omega. apply Z.divide_1_l. apply Z.divide_1_l. - eapply Y; eauto. omega. + subst. destruct Archi.ptr64; [split|split;split]; try lia. + apply align_divides; lia. apply Z.divide_1_l. apply Z.divide_1_l. + eapply Y; eauto. lia. destruct H. - subst. destruct Archi.ptr64; [split|split;split]; try omega. - apply align_divides; omega. apply Z.divide_1_l. apply Z.divide_1_l. - eapply Y; eauto. omega. + subst. destruct Archi.ptr64; [split|split;split]; try lia. + apply align_divides; lia. apply Z.divide_1_l. apply Z.divide_1_l. + eapply Y; eauto. lia. - (* single *) - assert (ofs <= align ofs 1) by (apply align_le; omega). - assert (ofs <= align ofs 2) by (apply align_le; omega). + assert (ofs <= align ofs 1) by (apply align_le; lia). + assert (ofs <= align ofs 2) by (apply align_le; lia). destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. destruct Archi.single_passed_as_single; simpl; omega. + subst. split. destruct Archi.single_passed_as_single; simpl; lia. destruct Archi.single_passed_as_single; simpl; apply Z.divide_1_l. - eapply Y; eauto. destruct Archi.single_passed_as_single; simpl; omega. + eapply Y; eauto. destruct Archi.single_passed_as_single; simpl; lia. - (* any32 *) destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H. subst. left. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. apply Z.divide_1_l. - eapply Y; eauto. omega. + subst. split. lia. apply Z.divide_1_l. + eapply Y; eauto. lia. - (* float *) - assert (ofs <= align ofs 2) by (apply align_le; omega). + assert (ofs <= align ofs 2) by (apply align_le; lia). destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. apply Z.divide_1_l. - eapply Y; eauto. omega. + subst. split. lia. apply Z.divide_1_l. + eapply Y; eauto. lia. Qed. Lemma loc_arguments_acceptable: diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v index 74ee6b85..85dd9b2e 100644 --- a/powerpc/NeedOp.v +++ b/powerpc/NeedOp.v @@ -162,8 +162,8 @@ Lemma operation_is_redundant_sound: vagree v arg1' nv. Proof. intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst. -- apply sign_ext_redundant_sound; auto. omega. -- apply sign_ext_redundant_sound; auto. omega. +- apply sign_ext_redundant_sound; auto. lia. +- apply sign_ext_redundant_sound; auto. lia. - apply andimm_redundant_sound; auto. - apply orimm_redundant_sound; auto. - apply rolm_redundant_sound; auto. diff --git a/powerpc/SelectLongproof.v b/powerpc/SelectLongproof.v index f16c967e..ea14668f 100644 --- a/powerpc/SelectLongproof.v +++ b/powerpc/SelectLongproof.v @@ -221,15 +221,15 @@ Proof. change (Int64.unsigned Int64.iwordsize) with 64. f_equal. rewrite Int.unsigned_repr. - apply eqmod_mod_eq. omega. + apply eqmod_mod_eq. lia. apply eqmod_trans with a. apply eqmod_divides with Int.modulus. apply Int.eqm_sym. apply Int.eqm_unsigned_repr. exists (two_p (32-6)); auto. apply eqmod_divides with Int64.modulus. apply Int64.eqm_unsigned_repr. exists (two_p (64-6)); auto. - assert (0 <= Int.unsigned (Int.repr a) mod 64 < 64) by (apply Z_mod_lt; omega). + assert (0 <= Int.unsigned (Int.repr a) mod 64 < 64) by (apply Z_mod_lt; lia). assert (64 < Int.max_unsigned) by (compute; auto). - omega. + lia. - InvEval. TrivialExists. simpl. rewrite <- H. unfold Val.rolml; destruct v1; simpl; auto. unfold Int64.rolm. rewrite Int64.rol_and. rewrite Int64.and_assoc. auto. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 7b34ea89..73fadc46 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -805,7 +805,7 @@ Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). Proof. red; intros. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm; auto. omega. + rewrite Val.zero_ext_and. apply eval_andimm; auto. lia. Qed. Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16). @@ -818,7 +818,7 @@ Qed. Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16). Proof. red; intros. unfold cast16unsigned. - rewrite Val.zero_ext_and. apply eval_andimm; auto. omega. + rewrite Val.zero_ext_and. apply eval_andimm; auto. lia. Qed. Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat. diff --git a/powerpc/Stacklayout.v b/powerpc/Stacklayout.v index cb3806bd..32b11ad5 100644 --- a/powerpc/Stacklayout.v +++ b/powerpc/Stacklayout.v @@ -77,11 +77,11 @@ Local Opaque Z.add Z.mul sepconj range. set (ostkdata := align oendcs 8). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. unfold fe_ofs_arg. - assert (8 + 4 * b.(bound_outgoing) <= ol) by (apply align_le; omega). - assert (ol <= ora) by (unfold ora; omega). - assert (ora <= ocs) by (unfold ocs; omega). + assert (8 + 4 * b.(bound_outgoing) <= ol) by (apply align_le; lia). + assert (ol <= ora) by (unfold ora; lia). + assert (ora <= ocs) by (unfold ocs; lia). assert (ocs <= oendcs) by (apply size_callee_save_area_incr). - assert (oendcs <= ostkdata) by (apply align_le; omega). + assert (oendcs <= ostkdata) by (apply align_le; lia). (* Reorder as: back link outgoing @@ -90,12 +90,12 @@ Local Opaque Z.add Z.mul sepconj range. callee-save *) rewrite sep_swap3. (* Apply range_split and range_split2 repeatedly *) - apply range_drop_right with 8. omega. - apply range_split. omega. - apply range_split_2. fold ol; omega. omega. - apply range_split. omega. - apply range_split. omega. - apply range_drop_right with ostkdata. omega. + apply range_drop_right with 8. lia. + apply range_split. lia. + apply range_split_2. fold ol; lia. lia. + apply range_split. lia. + apply range_split. lia. + apply range_drop_right with ostkdata. lia. eapply sep_drop2. eexact H. Qed. @@ -112,12 +112,12 @@ Proof. set (ostkdata := align oendcs 8). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. unfold fe_ofs_arg. - assert (8 + 4 * b.(bound_outgoing) <= ol) by (apply align_le; omega). - assert (ol <= ora) by (unfold ora; omega). - assert (ora <= ocs) by (unfold ocs; omega). + assert (8 + 4 * b.(bound_outgoing) <= ol) by (apply align_le; lia). + assert (ol <= ora) by (unfold ora; lia). + assert (ora <= ocs) by (unfold ocs; lia). assert (ocs <= oendcs) by (apply size_callee_save_area_incr). - assert (oendcs <= ostkdata) by (apply align_le; omega). - split. omega. apply align_le. omega. + assert (oendcs <= ostkdata) by (apply align_le; lia). + split. lia. apply align_le. lia. Qed. Lemma frame_env_aligned: @@ -136,10 +136,10 @@ Proof. set (oendcs := size_callee_save_area b ocs). set (ostkdata := align oendcs 8). split. exists (fe_ofs_arg / 8); reflexivity. - split. apply align_divides; omega. - split. apply align_divides; omega. + split. apply align_divides; lia. + split. apply align_divides; lia. split. apply Z.divide_0_r. apply Z.divide_add_r. - apply Z.divide_trans with 8. exists 2; auto. apply align_divides; omega. + apply Z.divide_trans with 8. exists 2; auto. apply align_divides; lia. apply Z.divide_factor_l. Qed. -- cgit