From 9ab3738ae87a554fb742420b8c81ced4cd3c66c7 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 8 Sep 2020 13:56:01 +0200 Subject: Changed cc_varargs to an option type Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs. --- powerpc/Asmexpand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index cb6a659f..fcd7c426 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -830,7 +830,7 @@ let expand_builtin_inline name args res = function is unprototyped. *) let set_cr6 sg = - if sg.sig_cc.cc_vararg || sg.sig_cc.cc_unproto then begin + if (sg.sig_cc.cc_vararg <> None) || sg.sig_cc.cc_unproto then begin if List.exists (function Tfloat | Tsingle -> true | _ -> false) sg.sig_args then emit (Pcreqv(CRbit_6, CRbit_6, CRbit_6)) else emit (Pcrxor(CRbit_6, CRbit_6, CRbit_6)) -- cgit 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 From 522285d1163523b02a1972b99d71c08552cd9c7b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 13 Jan 2021 14:51:36 +0100 Subject: Replace `omega` tactic with `lia`, continued Follow-up to aba0e740f --- powerpc/SelectOpproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 73fadc46..adac6c34 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -856,7 +856,7 @@ Proof. simpl; rewrite Heqo; simpl; eauto. constructor. simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned. auto. assert (Int.modulus < Int64.max_unsigned) by (compute; auto). - generalize (Int.unsigned_range n). omega. + generalize (Int.unsigned_range n). lia. - set (im := Int.repr Int.half_modulus). set (fm := Float.of_intu im). assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)). -- cgit From 15f354788a954635b44b3d2fae1057f67006509e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 15 Jan 2021 10:34:05 +0100 Subject: PowerPC: wrong computation of the position of the first vararg argument In function Asmexpand.next_arg_locations: If 7 integer parameter passing registers have been used already, and the next fixed arguments are Tlong then Tint, the Tlong argument was correctly analyzed as being passed on the stack, but the Tint argument was incorrectly analyzed as being passed in the 8th register. --- powerpc/Asmexpand.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index fcd7c426..df712b9d 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -388,8 +388,9 @@ let rec next_arg_locations ir fr ofs = function then next_arg_locations ir (fr + 1) ofs l else next_arg_locations ir fr (align ofs 8 + 8) l | Tlong :: l -> - if ir < 7 - then next_arg_locations (align ir 2 + 2) fr ofs l + let ir = align ir 2 in + if ir < 8 + then next_arg_locations (ir + 2) fr ofs l else next_arg_locations ir fr (align ofs 8 + 8) l let expand_builtin_va_start r = -- cgit From 478ece46d8323ea182ded96a531309becf7445bb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 16 Jan 2021 15:27:02 +0100 Subject: Support re-normalization of function parameters at function entry This is complementary to 28f235806 Some ABIs leave more flexibility concerning function parameters than CompCert expects. For instance, the AArch64/ELF ABI allow the caller of a function to leave unspecified the "padding bits" of function parameters. As an example, a parameter of type "unsigned char" may not have zeros in bits 8 to 63, but may have any bits there. When the caller is compiled by CompCert, it normalizes argument values to the parameter types before the call, so padding bits are always correct w.r.t. the type of the argument. This is no longer guaranteed in interoperability scenarios, when the caller is not compiled by CompCert. This commit adds a general mechanism to insert "re-normalization" conversions on the parameters of a function, at function entry. This is controlled by the platform-dependent function Convention1.return_value_needs_normalization. The semantic preservation proof is still conducted against the CompCert model, where the argument values of functions are already normalized. What the proof shows is that the extra conversions have no effect in this case. In future work we could relax the CompCert model, allowing functions to pass arguments that are not normalized. --- powerpc/Conventions1.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 045eb471..56beffe8 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -349,8 +349,9 @@ Proof. reflexivity. Qed. -(** ** Normalization of function results *) +(** ** Normalization of function results and parameters *) (** No normalization needed. *) Definition return_value_needs_normalization (t: rettype) := false. +Definition parameter_needs_normalization (t: rettype) := false. -- cgit From fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jan 2021 15:44:09 +0100 Subject: Qualify `Hint` as `Global Hint` where appropriate This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`. --- powerpc/Asmgenproof1.v | 14 +++++++------- powerpc/Conventions1.v | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 14ca22f9..89514d62 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -132,7 +132,7 @@ Lemma important_diff: Proof. congruence. Qed. -Hint Resolve important_diff: asmgen. +Global Hint Resolve important_diff: asmgen. Lemma important_data_preg_1: forall r, data_preg r = true -> important_preg r = true. @@ -146,7 +146,7 @@ Proof. intros. destruct (data_preg r) eqn:E; auto. apply important_data_preg_1 in E. congruence. Qed. -Hint Resolve important_data_preg_1 important_data_preg_2: asmgen. +Global Hint Resolve important_data_preg_1 important_data_preg_2: asmgen. Lemma nextinstr_inv2: forall r rs, important_preg r = true -> (nextinstr rs)#r = rs#r. @@ -166,7 +166,7 @@ Lemma gpr_or_zero_zero: Proof. intros. reflexivity. Qed. -Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: asmgen. +Global Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: asmgen. Lemma gpr_or_zero_l_not_zero: forall rs r, r <> GPR0 -> gpr_or_zero_l rs r = rs#r. @@ -178,21 +178,21 @@ Lemma gpr_or_zero_l_zero: Proof. intros. reflexivity. Qed. -Hint Resolve gpr_or_zero_l_not_zero gpr_or_zero_l_zero: asmgen. +Global Hint Resolve gpr_or_zero_l_not_zero gpr_or_zero_l_zero: asmgen. Lemma ireg_of_not_GPR0: forall m r, ireg_of m = OK r -> IR r <> IR GPR0. Proof. intros. erewrite <- ireg_of_eq; eauto with asmgen. Qed. -Hint Resolve ireg_of_not_GPR0: asmgen. +Global Hint Resolve ireg_of_not_GPR0: asmgen. Lemma ireg_of_not_GPR0': forall m r, ireg_of m = OK r -> r <> GPR0. Proof. intros. generalize (ireg_of_not_GPR0 _ _ H). congruence. Qed. -Hint Resolve ireg_of_not_GPR0': asmgen. +Global Hint Resolve ireg_of_not_GPR0': asmgen. (** Useful properties of the LR register *) @@ -208,7 +208,7 @@ Proof. intros. rewrite preg_notin_charact. intros. apply preg_of_not_LR. Qed. -Hint Resolve preg_of_not_LR preg_notin_LR: asmgen. +Global Hint Resolve preg_of_not_LR preg_notin_LR: asmgen. (** Useful simplification tactic *) diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 56beffe8..f05e77df 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -341,7 +341,7 @@ Proof. unfold forall_rpair; destruct p; intuition auto. Qed. -Hint Resolve loc_arguments_acceptable: locs. +Global Hint Resolve loc_arguments_acceptable: locs. Lemma loc_arguments_main: loc_arguments signature_main = nil. -- cgit From 30feb31c6d6e9235acad42ec5d09d14f3919cc36 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 30 Dec 2020 11:41:10 +0100 Subject: Introduce and use PrintAsmaux.variable_section This is a generalization of the previous PrintAsmaux.common_section function that - handles initialized variables in addition to uninitialized variables; - can be used for Section_const, not just for Section_data. --- powerpc/TargetPrinter.ml | 22 ++++++++-------------- 1 file changed, 8 insertions(+), 14 deletions(-) (limited to 'powerpc') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 43d2447d..cf00e659 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -118,22 +118,16 @@ module Linux_System : SYSTEM = let name_of_section = function | Section_text -> ".text" | Section_data i -> - if i then - ".data" - else - common_section ~sec:".section .bss" () + variable_section ~sec:".data" ~bss:".section .bss" i | Section_small_data i -> - if i then - ".section .sdata,\"aw\",@progbits" - else - common_section ~sec:".section .sbss,\"aw\",@nobits" () + variable_section + ~sec:".section .sdata,\"aw\",@progbits" + ~bss:".section .sbss,\"aw\",@nobits" + i | Section_const i -> - if i || (not !Clflags.option_fcommon) then ".rodata" else "COMM" + variable_section ~sec:".rodata" i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then - ".section .sdata2,\"a\",@progbits" - else - "COMM" + variable_section ~sec:".section .sdata2,\"a\",@progbits" i | Section_string -> ".rodata" | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" | Section_jumptable -> ".text" @@ -218,7 +212,7 @@ module Diab_System : SYSTEM = let name_of_section = function | Section_text -> ".text" - | Section_data i -> if i then ".data" else common_section () + | Section_data i -> variable_section ~sec:".data" ~bss:".bss" i | Section_small_data i -> if i then ".sdata" else ".sbss" | Section_const _ -> ".text" | Section_small_const _ -> ".sdata2" -- cgit From ed89275cb820bb7ab283c51e461d852d1c8bec63 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 30 Dec 2020 11:00:22 +0100 Subject: Section handling: finer control of variable initialization Distinguish between: - uninitialized variables, which can go in COMM if supported - variables initialized with fixed, numeric quantities, which can go in a readonly section if "const" - variables initialized with symbol addresses which may need relocation, which cannot go in a readonly section even if "const", but can go in a special "const_data" section. Also: on macOS, use ".const" instead of ".literal8" for literals, as not all literals have size 8. --- powerpc/TargetPrinter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index cf00e659..e32348a3 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -213,7 +213,7 @@ module Diab_System : SYSTEM = let name_of_section = function | Section_text -> ".text" | Section_data i -> variable_section ~sec:".data" ~bss:".bss" i - | Section_small_data i -> if i then ".sdata" else ".sbss" + | Section_small_data i -> variable_section ~sec:".sdata" ~bss:".sbss" i | Section_const _ -> ".text" | Section_small_const _ -> ".sdata2" | Section_string -> ".text" -- cgit From 014883f2f4cfc4fd64fe9aa5f561a971e2ed1345 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 19 Feb 2021 09:31:03 +0100 Subject: Fix regression on PowerPC / Diab On PowerPC/Diab, common declarations must not be used for small data sections. Add a `~common` option to `PrintAsmaux.variable_section` to control the use of common declarations. The default is whatever is specified on the command line using the `-fcommon` and `-fno-common` options. Use `~common:false` for `Section_small_data` on PowerPC / Diab. Note that on PowerPC/Linux, GCC uses common declarations for uninitialized variables in small data section, so we keep doing this in CompCert as well. --- powerpc/TargetPrinter.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'powerpc') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index e32348a3..52d30e33 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -212,8 +212,10 @@ module Diab_System : SYSTEM = let name_of_section = function | Section_text -> ".text" - | Section_data i -> variable_section ~sec:".data" ~bss:".bss" i - | Section_small_data i -> variable_section ~sec:".sdata" ~bss:".sbss" i + | Section_data i -> + variable_section ~sec:".data" ~bss:".bss" i + | Section_small_data i -> + variable_section ~sec:".sdata" ~bss:".sbss" ~common:false i | Section_const _ -> ".text" | Section_small_const _ -> ".sdata2" | Section_string -> ".text" -- cgit