diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-21 18:22:00 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-12-29 15:29:56 +0100 |
commit | aba0e740f25ffa5c338dfa76cab71144802cebc2 (patch) | |
tree | 746115009aa60b802a2b5369a5106a2e971eb22f /riscV/Stacklayout.v | |
parent | 2e202e2b17cc3ae909628b7b3ae0b8ede3117d82 (diff) | |
download | compcert-aba0e740f25ffa5c338dfa76cab71144802cebc2.tar.gz compcert-aba0e740f25ffa5c338dfa76cab71144802cebc2.zip |
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`.
Diffstat (limited to 'riscV/Stacklayout.v')
-rw-r--r-- | riscV/Stacklayout.v | 50 |
1 files changed, 25 insertions, 25 deletions
diff --git a/riscV/Stacklayout.v b/riscV/Stacklayout.v index d0c6a526..25f02aab 100644 --- a/riscV/Stacklayout.v +++ b/riscV/Stacklayout.v @@ -68,15 +68,15 @@ Local Opaque Z.add Z.mul sepconj range. set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= 4 * b.(bound_outgoing)) by omega. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). - assert (olink + w <= oretaddr) by (unfold oretaddr; omega). - assert (oretaddr + w <= ocs) by (unfold ocs; omega). + assert (0 <= 4 * b.(bound_outgoing)) by lia. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (olink + w <= oretaddr) by (unfold oretaddr; lia). + assert (oretaddr + w <= 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 <= ol) by (apply align_le; omega). - assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). + assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= 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_swap45. (* Apply range_split and range_split2 repeatedly *) unfold fe_ofs_arg. - apply range_split_2. fold olink; omega. omega. - apply range_split. omega. - apply range_split. omega. - apply range_split_2. fold ol. omega. omega. - apply range_drop_right with ostkdata. omega. + apply range_split_2. fold olink; lia. lia. + apply range_split. lia. + apply range_split. lia. + apply range_split_2. fold ol. lia. lia. + apply range_drop_right with ostkdata. lia. eapply sep_drop2. eexact H. Qed. @@ -109,16 +109,16 @@ Proof. set (ocs := oretaddr + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= 4 * b.(bound_outgoing)) by omega. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). - assert (olink + w <= oretaddr) by (unfold oretaddr; omega). - assert (oretaddr + w <= ocs) by (unfold ocs; omega). + assert (0 <= 4 * b.(bound_outgoing)) by lia. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (olink + w <= oretaddr) by (unfold oretaddr; lia). + assert (oretaddr + w <= 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 <= ol) by (apply align_le; omega). - assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). - split. omega. apply align_le. omega. + assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia). + split. lia. apply align_le. lia. Qed. Lemma frame_env_aligned: @@ -137,11 +137,11 @@ Proof. set (ocs := oretaddr + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto). split. apply Z.divide_0_r. - split. apply align_divides; omega. - split. apply align_divides; omega. - split. apply align_divides; omega. - apply Z.divide_add_r. apply align_divides; omega. apply Z.divide_refl. + split. apply align_divides; lia. + split. apply align_divides; lia. + split. apply align_divides; lia. + apply Z.divide_add_r. apply align_divides; lia. apply Z.divide_refl. Qed. |