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. --- arm/Asmexpand.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm') diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index f4e79a37..15cbebec 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -545,7 +545,7 @@ module FixupHF = struct end let fixup_arguments dir sg = - if sg.sig_cc.cc_vararg then + if sg.sig_cc.cc_vararg <> None then FixupEABI.fixup_arguments dir sg else begin let act = fixup_actions (Array.make 16 false) 0 sg.sig_args in @@ -555,7 +555,7 @@ module FixupHF = struct end let fixup_result dir sg = - if sg.sig_cc.cc_vararg then + if sg.sig_cc.cc_vararg <> None then FixupEABI.fixup_result dir sg end -- 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`. --- arm/Asm.v | 2 +- arm/Asmgenproof.v | 20 ++++++++--------- arm/Asmgenproof1.v | 26 +++++++++++----------- arm/ConstpropOpproof.v | 2 +- arm/Conventions1.v | 60 +++++++++++++++++++++++++------------------------- arm/NeedOp.v | 4 ++-- arm/Op.v | 6 ++--- arm/SelectOpproof.v | 4 ++-- arm/Stacklayout.v | 36 +++++++++++++++--------------- 9 files changed, 80 insertions(+), 80 deletions(-) (limited to 'arm') diff --git a/arm/Asm.v b/arm/Asm.v index 293df274..8c902074 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -1004,7 +1004,7 @@ Ltac Equalities := split. auto. intros. destruct B; auto. subst. auto. (* trace length *) red; intros; inv H; simpl. - omega. + lia. inv H3; eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. (* initial states *) diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index f60f4b48..93e0c6c2 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -68,7 +68,7 @@ Lemma transf_function_no_overflow: forall f tf, transf_function f = OK tf -> list_length_z (fn_code tf) <= Ptrofs.max_unsigned. Proof. - intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0. omega. + intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0. lia. Qed. Lemma exec_straight_exec: @@ -122,13 +122,13 @@ Proof. case (is_label lbl a). intro EQ; injection EQ; intro; subst c'. exists (pos + 1). split. auto. split. - replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. - rewrite list_length_z_cons. generalize (list_length_z_pos c). omega. + replace (pos + 1 - pos) with (0 + 1) by lia. constructor. constructor. + rewrite list_length_z_cons. generalize (list_length_z_pos c). lia. intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]]. exists pos'. split. auto. split. - replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega. + replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by lia. constructor. auto. - rewrite list_length_z_cons. omega. + rewrite list_length_z_cons. lia. Qed. (** The following lemmas show that the translation from Mach to ARM @@ -378,8 +378,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. @@ -903,11 +903,11 @@ Opaque loadind. simpl; reflexivity. reflexivity. } (* After the function prologue is the code for the function body *) - exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor. + exploit exec_straight_steps_2; eauto using functions_transl. lia. constructor. intros (ofsbody & U & V). (* Conclusions *) left; exists (State rs4 m3'); split. - eapply exec_straight_steps_1; eauto. omega. constructor. + eapply exec_straight_steps_1; eauto. lia. constructor. econstructor; eauto. rewrite U. econstructor; eauto. apply agree_nextinstr. apply agree_undef_regs2 with rs2. @@ -934,7 +934,7 @@ Opaque loadind. - (* return *) inv STACKS. simpl in *. - right. split. omega. split. auto. + right. split. lia. split. auto. rewrite <- ATPC in H5. econstructor; eauto. congruence. Qed. diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 807e069d..fce9d4a6 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -352,15 +352,15 @@ Proof. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. econstructor; split. eapply exec_straight_two. simpl; reflexivity. simpl; reflexivity. auto. auto. - split; intros; Simpl. simpl. f_equal. rewrite Int.zero_ext_and by omega. + split; intros; Simpl. simpl. f_equal. rewrite Int.zero_ext_and by lia. rewrite Int.and_assoc. change 65535 with (two_p 16 - 1). rewrite Int.and_idem. apply Int.same_bits_eq; intros. rewrite Int.bits_or, Int.bits_and, Int.bits_shl, Int.testbit_repr by auto. - rewrite Ztestbit_two_p_m1 by omega. change (Int.unsigned (Int.repr 16)) with 16. + rewrite Ztestbit_two_p_m1 by lia. change (Int.unsigned (Int.repr 16)) with 16. destruct (zlt i 16). rewrite andb_true_r, orb_false_r; auto. - rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega. - change (Int.unsigned (Int.repr 16)) with 16. rewrite zlt_true by omega. f_equal; omega. + rewrite andb_false_r; simpl. rewrite Int.bits_shru by lia. + change (Int.unsigned (Int.repr 16)) with 16. rewrite zlt_true by lia. f_equal; lia. } destruct (Nat.leb l1 l2). { (* mov - orr* *) @@ -696,10 +696,10 @@ Lemma int_not_lt: Proof. intros. unfold Int.lt. rewrite int_signed_eq. unfold proj_sumbool. destruct (zlt (Int.signed y) (Int.signed x)). - rewrite zlt_false. rewrite zeq_false. auto. omega. omega. + rewrite zlt_false. rewrite zeq_false. auto. lia. lia. destruct (zeq (Int.signed x) (Int.signed y)). - rewrite zlt_false. auto. omega. - rewrite zlt_true. auto. omega. + rewrite zlt_false. auto. lia. + rewrite zlt_true. auto. lia. Qed. Lemma int_lt_not: @@ -713,10 +713,10 @@ Lemma int_not_ltu: Proof. intros. unfold Int.ltu, Int.eq. destruct (zlt (Int.unsigned y) (Int.unsigned x)). - rewrite zlt_false. rewrite zeq_false. auto. omega. omega. + rewrite zlt_false. rewrite zeq_false. auto. lia. lia. destruct (zeq (Int.unsigned x) (Int.unsigned y)). - rewrite zlt_false. auto. omega. - rewrite zlt_true. auto. omega. + rewrite zlt_false. auto. lia. + rewrite zlt_true. auto. lia. Qed. Lemma int_ltu_not: @@ -1279,16 +1279,16 @@ Local Transparent destroyed_by_op. rewrite Int.unsigned_repr. apply zlt_true. assert (Int.unsigned i <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned i). rewrite H1; reflexivity. } - omega. + lia. change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0. - generalize Int.wordsize_max_unsigned; omega. + generalize Int.wordsize_max_unsigned; lia. } assert (LTU'': Int.ltu i Int.iwordsize = true). { generalize (Int.ltu_inv _ _ LTU). intros. unfold Int.ltu. rewrite Int.unsigned_repr_wordsize. apply zlt_true. change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0. - omega. + lia. } set (j := Int.sub Int.iwordsize i) in *. set (rs1 := nextinstr_nf (rs#IR14 <- (Val.shr (Vint i0) (Vint (Int.repr 31))))). diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index a4f5c29c..cd0afb7a 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -451,7 +451,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/arm/Conventions1.v b/arm/Conventions1.v index fe49a781..3bd2b553 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -309,7 +309,7 @@ Remark loc_arguments_hf_charact: In p (loc_arguments_hf tyl ir fr ofs) -> 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. } induction tyl; simpl loc_arguments_hf; intros. @@ -319,40 +319,40 @@ Proof. destruct (zlt ir 4); destruct H. subst. apply ireg_param_caller_save. eapply IHtyl; eauto. - subst. split; [omega | auto]. - eapply Y; eauto. omega. + subst. split; [lia | auto]. + eapply Y; eauto. lia. - (* float *) destruct (zlt fr 8); destruct H. subst. apply freg_param_caller_save. eapply IHtyl; eauto. - subst. split. apply Z.le_ge. apply align_le. omega. auto. - eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; omega. omega. + subst. split. apply Z.le_ge. apply align_le. lia. auto. + eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; lia. lia. - (* long *) set (ir' := align ir 2) in *. - assert (ofs <= align ofs 2) by (apply align_le; omega). + assert (ofs <= align ofs 2) by (apply align_le; lia). destruct (zlt ir' 4). destruct H. subst p. split; apply ireg_param_caller_save. eapply IHtyl; eauto. - destruct H. subst p. split; destruct Archi.big_endian; (split; [ omega | auto ]). - eapply Y. eapply IHtyl; eauto. omega. + destruct H. subst p. split; destruct Archi.big_endian; (split; [ lia | auto ]). + eapply Y. eapply IHtyl; eauto. lia. - (* single *) destruct (zlt fr 8); destruct H. subst. apply freg_param_caller_save. eapply IHtyl; eauto. - subst. split; [omega|auto]. - eapply Y; eauto. omega. + subst. split; [lia|auto]. + eapply Y; eauto. lia. - (* any32 *) destruct (zlt ir 4); destruct H. subst. apply ireg_param_caller_save. eapply IHtyl; eauto. - subst. split; [omega | auto]. - eapply Y; eauto. omega. + subst. split; [lia | auto]. + eapply Y; eauto. lia. - (* any64 *) destruct (zlt fr 8); destruct H. subst. apply freg_param_caller_save. eapply IHtyl; eauto. - subst. split. apply Z.le_ge. apply align_le. omega. auto. - eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; omega. omega. + subst. split. apply Z.le_ge. apply align_le. lia. auto. + eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; lia. lia. Qed. Remark loc_arguments_sf_charact: @@ -360,7 +360,7 @@ Remark loc_arguments_sf_charact: In p (loc_arguments_sf tyl ofs) -> forall_rpair (loc_argument_charact (Z.max 0 ofs)) p. Proof. assert (X: forall ofs1 ofs2 l, loc_argument_charact (Z.max 0 ofs2) l -> ofs1 <= ofs2 -> loc_argument_charact (Z.max 0 ofs1) l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition xomega. } + { destruct l; simpl; intros; auto. destruct sl; auto. intuition extlia. } assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact (Z.max 0 ofs2)) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact (Z.max 0 ofs1)) p). { destruct p; simpl; intuition eauto. } induction tyl; simpl loc_arguments_sf; intros. @@ -370,44 +370,44 @@ Proof. destruct H. destruct (zlt ofs 0); subst p. apply ireg_param_caller_save. - split; [xomega|auto]. - eapply Y; eauto. omega. + split; [extlia|auto]. + eapply Y; eauto. lia. - (* float *) set (ofs' := align ofs 2) in *. - assert (ofs <= ofs') by (apply align_le; omega). + assert (ofs <= ofs') by (apply align_le; lia). destruct H. destruct (zlt ofs' 0); subst p. apply freg_param_caller_save. - split; [xomega|auto]. - eapply Y. eapply IHtyl; eauto. omega. + split; [extlia|auto]. + eapply Y. eapply IHtyl; eauto. lia. - (* long *) set (ofs' := align ofs 2) in *. - assert (ofs <= ofs') by (apply align_le; omega). + assert (ofs <= ofs') by (apply align_le; lia). destruct H. destruct (zlt ofs' 0); subst p. split; apply ireg_param_caller_save. - split; destruct Archi.big_endian; (split; [xomega|auto]). - eapply Y. eapply IHtyl; eauto. omega. + split; destruct Archi.big_endian; (split; [extlia|auto]). + eapply Y. eapply IHtyl; eauto. lia. - (* single *) destruct H. destruct (zlt ofs 0); subst p. apply freg_param_caller_save. - split; [xomega|auto]. - eapply Y; eauto. omega. + split; [extlia|auto]. + eapply Y; eauto. lia. - (* any32 *) destruct H. destruct (zlt ofs 0); subst p. apply ireg_param_caller_save. - split; [xomega|auto]. - eapply Y; eauto. omega. + split; [extlia|auto]. + eapply Y; eauto. lia. - (* any64 *) set (ofs' := align ofs 2) in *. - assert (ofs <= ofs') by (apply align_le; omega). + assert (ofs <= ofs') by (apply align_le; lia). destruct H. destruct (zlt ofs' 0); subst p. apply freg_param_caller_save. - split; [xomega|auto]. - eapply Y. eapply IHtyl; eauto. omega. + split; [extlia|auto]. + eapply Y. eapply IHtyl; eauto. lia. Qed. Lemma loc_arguments_acceptable: diff --git a/arm/NeedOp.v b/arm/NeedOp.v index c70c7e40..23e8f047 100644 --- a/arm/NeedOp.v +++ b/arm/NeedOp.v @@ -198,8 +198,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. Qed. diff --git a/arm/Op.v b/arm/Op.v index cc90e043..4739ef2e 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -527,10 +527,10 @@ End SOUNDNESS. Program Definition mk_shift_amount (n: int) : shift_amount := {| s_amount := Int.modu n Int.iwordsize; s_range := _ |}. Next Obligation. - assert (0 <= Z.modulo (Int.unsigned n) 32 < 32). apply Z_mod_lt. omega. + assert (0 <= Z.modulo (Int.unsigned n) 32 < 32). apply Z_mod_lt. lia. unfold Int.ltu, Int.modu. change (Int.unsigned Int.iwordsize) with 32. - rewrite Int.unsigned_repr. apply zlt_true. omega. - assert (32 < Int.max_unsigned). compute; auto. omega. + rewrite Int.unsigned_repr. apply zlt_true. lia. + assert (32 < Int.max_unsigned). compute; auto. lia. Qed. Lemma mk_shift_amount_eq: diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index 70f8f191..bd9f01b1 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -754,7 +754,7 @@ Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. omega. + rewrite Val.zero_ext_and. apply eval_andimm. lia. Qed. Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16). @@ -767,7 +767,7 @@ Qed. Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. omega. + rewrite Val.zero_ext_and. apply eval_andimm. lia. Qed. Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat. diff --git a/arm/Stacklayout.v b/arm/Stacklayout.v index 462d83ad..f6e01e0c 100644 --- a/arm/Stacklayout.v +++ b/arm/Stacklayout.v @@ -72,12 +72,12 @@ Local Opaque Z.add Z.mul sepconj range. set (ocs := ol + 4 * b.(bound_local)); set (ostkdata := align (size_callee_save_area b ocs) 8). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= olink) by (unfold olink; omega). - assert (olink <= ora) by (unfold ora; omega). - assert (ora + 4 <= ol) by (apply align_le; omega). - assert (ol + 4 * b.(bound_local) <= ocs) by (unfold ocs; omega). + assert (0 <= olink) by (unfold olink; lia). + assert (olink <= ora) by (unfold ora; lia). + assert (ora + 4 <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= ocs) by (unfold ocs; lia). assert (ocs <= size_callee_save_area b ocs) by apply size_callee_save_area_incr. - assert (size_callee_save_area b ocs <= ostkdata) by (apply align_le; omega). + assert (size_callee_save_area b ocs <= ostkdata) by (apply align_le; lia). (* Reorder as: outgoing back link @@ -89,11 +89,11 @@ Local Opaque Z.add Z.mul sepconj range. rewrite sep_swap34. (* Apply range_split and range_split2 repeatedly *) unfold fe_ofs_arg. - apply range_split. omega. - apply range_split. omega. - apply range_split_2. fold ol; omega. omega. - apply range_split. omega. - apply range_drop_right with ostkdata. omega. + apply range_split. lia. + apply range_split. lia. + apply range_split_2. fold ol; lia. lia. + apply range_split. lia. + apply range_drop_right with ostkdata. lia. eapply sep_drop2. eexact H. Qed. @@ -109,13 +109,13 @@ Proof. set (ocs := ol + 4 * b.(bound_local)); set (ostkdata := align (size_callee_save_area b ocs) 8). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= olink) by (unfold olink; omega). - assert (olink <= ora) by (unfold ora; omega). - assert (ora + 4 <= ol) by (apply align_le; omega). - assert (ol + 4 * b.(bound_local) <= ocs) by (unfold ocs; omega). + assert (0 <= olink) by (unfold olink; lia). + assert (olink <= ora) by (unfold ora; lia). + assert (ora + 4 <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= ocs) by (unfold ocs; lia). assert (ocs <= size_callee_save_area b ocs) by apply size_callee_save_area_incr. - assert (size_callee_save_area b ocs <= ostkdata) by (apply align_le; omega). - split. omega. apply align_le; omega. + assert (size_callee_save_area b ocs <= ostkdata) by (apply align_le; lia). + split. lia. apply align_le; lia. Qed. Lemma frame_env_aligned: @@ -134,7 +134,7 @@ Proof. set (ocs := ol + 4 * b.(bound_local)); set (ostkdata := align (size_callee_save_area b ocs) 8). split. apply Z.divide_0_r. - split. apply align_divides; omega. - split. apply align_divides; omega. + split. apply align_divides; lia. + split. apply align_divides; lia. unfold ora, olink; auto using Z.divide_mul_l, Z.divide_add_r, Z.divide_refl. Qed. -- 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. --- arm/Conventions1.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'arm') diff --git a/arm/Conventions1.v b/arm/Conventions1.v index 3bd2b553..b94ce9ef 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -436,8 +436,9 @@ Proof. destruct Archi.abi; 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`. --- arm/Asmgenproof1.v | 6 +++--- arm/Conventions1.v | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'arm') diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index fce9d4a6..b94964a0 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -40,14 +40,14 @@ Lemma ireg_of_not_R14: Proof. intros. erewrite <- ireg_of_eq; eauto with asmgen. Qed. -Hint Resolve ireg_of_not_R14: asmgen. +Global Hint Resolve ireg_of_not_R14: asmgen. Lemma ireg_of_not_R14': forall m r, ireg_of m = OK r -> r <> IR14. Proof. intros. generalize (ireg_of_not_R14 _ _ H). congruence. Qed. -Hint Resolve ireg_of_not_R14': asmgen. +Global Hint Resolve ireg_of_not_R14': asmgen. (** [undef_flags] and [nextinstr_nf] *) @@ -75,7 +75,7 @@ Proof. intros; red; intros; subst; discriminate. Qed. -Hint Resolve data_if_preg if_preg_not_PC: asmgen. +Global Hint Resolve data_if_preg if_preg_not_PC: asmgen. Lemma nextinstr_nf_inv: forall r rs, if_preg r = true -> (nextinstr_nf rs)#r = rs#r. diff --git a/arm/Conventions1.v b/arm/Conventions1.v index b94ce9ef..0ddd882f 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -427,7 +427,7 @@ Proof. destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; 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. --- arm/TargetPrinter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 03e06a65..43dac44a 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -148,9 +148,9 @@ struct let name_of_section = function | Section_text -> ".text" | Section_data i | Section_small_data i -> - if i then ".data" else common_section () + variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" + variable_section ~sec:".section .rodata" i | Section_string -> ".section .rodata" | Section_literal -> ".text" | Section_jumptable -> ".text" -- cgit