diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
commit | af16cdae6d58033cc8aa06bca330f98b96ba12f2 (patch) | |
tree | 4985e9ae8fa0d580bbf95a198edeca4f0bd6ff46 /common | |
parent | 21c979fce33b068ce4b86e67d3d866b203411c6c (diff) | |
parent | 02b169b444c435b8d1aacf54969dd7de57317a5c (diff) | |
download | compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.tar.gz compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.zip |
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
Diffstat (limited to 'common')
-rw-r--r-- | common/AST.v | 25 | ||||
-rw-r--r-- | common/Behaviors.v | 9 | ||||
-rw-r--r-- | common/Builtins.v | 9 | ||||
-rw-r--r-- | common/Builtins0.v | 14 | ||||
-rw-r--r-- | common/Determinism.v | 9 | ||||
-rw-r--r-- | common/Errors.v | 9 | ||||
-rw-r--r-- | common/Events.v | 68 | ||||
-rw-r--r-- | common/Globalenvs.v | 93 | ||||
-rw-r--r-- | common/Linking.v | 11 | ||||
-rw-r--r-- | common/Memdata.v | 92 | ||||
-rw-r--r-- | common/Memory.v | 349 | ||||
-rw-r--r-- | common/Memtype.v | 11 | ||||
-rw-r--r-- | common/PrintAST.ml | 9 | ||||
-rw-r--r-- | common/Sections.ml | 79 | ||||
-rw-r--r-- | common/Sections.mli | 25 | ||||
-rw-r--r-- | common/Separation.v | 79 | ||||
-rw-r--r-- | common/Smallstep.v | 29 | ||||
-rw-r--r-- | common/Subtyping.v | 65 | ||||
-rw-r--r-- | common/Switch.v | 47 | ||||
-rw-r--r-- | common/Switchaux.ml | 9 | ||||
-rw-r--r-- | common/Unityping.v | 31 | ||||
-rw-r--r-- | common/Values.v | 66 |
22 files changed, 598 insertions, 540 deletions
diff --git a/common/AST.v b/common/AST.v index 979db4b9..868364cd 100644 --- a/common/AST.v +++ b/common/AST.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -61,7 +62,7 @@ Definition typesize (ty: typ) : Z := end. Lemma typesize_pos: forall ty, typesize ty > 0. -Proof. destruct ty; simpl; omega. Qed. +Proof. destruct ty; simpl; lia. Qed. Lemma typesize_Tptr: typesize Tptr = if Archi.ptr64 then 8 else 4. Proof. unfold Tptr; destruct Archi.ptr64; auto. Qed. @@ -122,17 +123,17 @@ These signatures are used in particular to determine appropriate calling conventions for the function. *) Record calling_convention : Type := mkcallconv { - cc_vararg: bool; (**r variable-arity function *) - cc_unproto: bool; (**r old-style unprototyped function *) - cc_structret: bool (**r function returning a struct *) + cc_vararg: option Z; (**r variable-arity function (+ number of fixed args) *) + cc_unproto: bool; (**r old-style unprototyped function *) + cc_structret: bool (**r function returning a struct *) }. Definition cc_default := - {| cc_vararg := false; cc_unproto := false; cc_structret := false |}. + {| cc_vararg := None; cc_unproto := false; cc_structret := false |}. Definition calling_convention_eq (x y: calling_convention) : {x=y} + {x<>y}. Proof. - decide equality; apply bool_dec. + decide equality; try (apply bool_dec). decide equality; apply Z.eq_dec. Defined. Global Opaque calling_convention_eq. @@ -275,13 +276,13 @@ Fixpoint init_data_list_size (il: list init_data) {struct il} : Z := Lemma init_data_size_pos: forall i, init_data_size i >= 0. Proof. - destruct i; simpl; try xomega. destruct Archi.ptr64; omega. + destruct i; simpl; try extlia. destruct Archi.ptr64; lia. Qed. Lemma init_data_list_size_pos: forall il, init_data_list_size il >= 0. Proof. - induction il; simpl. omega. generalize (init_data_size_pos a); omega. + induction il; simpl. lia. generalize (init_data_size_pos a); lia. Qed. (** Information attached to global variables. *) diff --git a/common/Behaviors.v b/common/Behaviors.v index 92bd708f..023b33e2 100644 --- a/common/Behaviors.v +++ b/common/Behaviors.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/common/Builtins.v b/common/Builtins.v index 476b541e..facff726 100644 --- a/common/Builtins.v +++ b/common/Builtins.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/common/Builtins0.v b/common/Builtins0.v index d84c9112..384dde1e 100644 --- a/common/Builtins0.v +++ b/common/Builtins0.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -341,6 +342,7 @@ Inductive standard_builtin : Type := | BI_i16_bswap | BI_i32_bswap | BI_i64_bswap + | BI_unreachable | BI_i64_umulh | BI_i64_smulh | BI_i64_sdiv @@ -376,6 +378,7 @@ Definition standard_builtin_table : list (string * standard_builtin) := :: ("__builtin_bswap", BI_i32_bswap) :: ("__builtin_bswap32", BI_i32_bswap) :: ("__builtin_bswap64", BI_i64_bswap) + :: ("__builtin_unreachable", BI_unreachable) :: ("__compcert_i64_umulh", BI_i64_umulh) :: ("__compcert_i64_smulh", BI_i64_smulh) :: ("__compcert_i64_sdiv", BI_i64_sdiv) @@ -414,6 +417,8 @@ Definition standard_builtin_sig (b: standard_builtin) : signature := mksignature (Tlong :: nil) Tlong cc_default | BI_i16_bswap => mksignature (Tint :: nil) Tint cc_default + | BI_unreachable => + mksignature nil Tvoid cc_default | BI_i64_shl | BI_i64_shr | BI_i64_sar => mksignature (Tlong :: Tint :: nil) Tlong cc_default | BI_i64_dtos | BI_i64_dtou => @@ -448,6 +453,7 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig | BI_i64_bswap => mkbuiltin_n1t Tlong Tlong (fun n => Int64.repr (decode_int (List.rev (encode_int 8%nat (Int64.unsigned n))))) + | BI_unreachable => mkbuiltin Tvoid (fun vargs => None) _ _ | BI_i64_umulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu | BI_i64_smulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs | BI_i64_sdiv => mkbuiltin_v2p Tlong Val.divls _ _ diff --git a/common/Determinism.v b/common/Determinism.v index 7fa01c2d..c8c90782 100644 --- a/common/Determinism.v +++ b/common/Determinism.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/common/Errors.v b/common/Errors.v index 6807735a..bf72f12b 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/common/Events.v b/common/Events.v index 033e2e03..360da52f 100644 --- a/common/Events.v +++ b/common/Events.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -25,6 +26,7 @@ Require Import Values. Require Import Memory. Require Import Globalenvs. Require Import Builtins. +Require Import Lia. (** * Events and traces *) @@ -798,7 +800,7 @@ Proof. exists f; exists v'; exists m1'; intuition. constructor; auto. red; intros. congruence. (* trace length *) -- inv H; inv H0; simpl; omega. +- inv H; inv H0; simpl; lia. (* receptive *) - inv H. exploit volatile_load_receptive; eauto. intros [v2 A]. exists v2; exists m1; constructor; auto. @@ -925,7 +927,7 @@ Proof. eelim H3; eauto. exploit Mem.store_valid_access_3. eexact H0. intros [X Y]. apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. - apply X. omega. + apply X. lia. Qed. Lemma volatile_store_receptive: @@ -960,7 +962,7 @@ Proof. exploit volatile_store_inject; eauto. intros [m2' [A [B [C D]]]]. exists f; exists Vundef; exists m2'; intuition. constructor; auto. red; intros; congruence. (* trace length *) -- inv H; inv H0; simpl; omega. +- inv H; inv H0; simpl; lia. (* receptive *) - assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto. subst t2; exists vres1; exists m1; auto. @@ -1042,7 +1044,7 @@ Proof. subst b1. rewrite C in H2. inv H2. eauto with mem. rewrite D in H2 by auto. congruence. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. @@ -1122,21 +1124,21 @@ Proof. exploit Mem.address_inject; eauto. apply Mem.perm_implies with Freeable; auto with mem. apply P. instantiate (1 := lo). - generalize (size_chunk_pos Mptr); omega. + generalize (size_chunk_pos Mptr); lia. intro EQ. exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D). exists f, Vundef, m2'; split. apply extcall_free_sem_ptr with (sz := sz) (m' := m2'). - rewrite EQ. rewrite <- A. f_equal. omega. + rewrite EQ. rewrite <- A. f_equal. lia. auto. auto. - rewrite ! EQ. rewrite <- C. f_equal; omega. + rewrite ! EQ. rewrite <- C. f_equal; lia. split. auto. split. auto. split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence. split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach. intros. red; intros. eelim H2; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - apply P. omega. + apply P. lia. split. auto. red; intros. congruence. + inv H2. inv H6. replace v' with Vnullptr. @@ -1145,7 +1147,7 @@ Proof. red; intros; congruence. unfold Vnullptr in *; destruct Archi.ptr64; inv H4; auto. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - assert (t1 = t2) by (inv H; inv H0; auto). subst t2. exists vres1; exists m1; auto. @@ -1217,23 +1219,23 @@ Proof. destruct (zeq sz 0). + (* special case sz = 0 *) assert (bytes = nil). - { exploit (Mem.loadbytes_empty m1 bsrc (Ptrofs.unsigned osrc) sz). omega. congruence. } + { exploit (Mem.loadbytes_empty m1 bsrc (Ptrofs.unsigned osrc) sz). lia. congruence. } subst. destruct (Mem.range_perm_storebytes m1' b0 (Ptrofs.unsigned (Ptrofs.add odst (Ptrofs.repr delta0))) nil) as [m2' SB]. - simpl. red; intros; omegaContradiction. + simpl. red; intros; extlia. exists f, Vundef, m2'. split. econstructor; eauto. - intros; omegaContradiction. - intros; omegaContradiction. - right; omega. - apply Mem.loadbytes_empty. omega. + intros; extlia. + intros; extlia. + right; lia. + apply Mem.loadbytes_empty. lia. split. auto. split. eapply Mem.storebytes_empty_inject; eauto. split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros. congruence. split. eapply Mem.storebytes_unchanged_on; eauto. - simpl; intros; omegaContradiction. + simpl; intros; extlia. split. apply inject_incr_refl. red; intros; congruence. + (* general case sz > 0 *) @@ -1243,11 +1245,11 @@ Proof. assert (RPDST: Mem.range_perm m1 bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sz) Cur Nonempty). replace sz with (Z.of_nat (length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. - rewrite LEN. apply Z2Nat.id. omega. + rewrite LEN. apply Z2Nat.id. lia. assert (PSRC: Mem.perm m1 bsrc (Ptrofs.unsigned osrc) Cur Nonempty). - apply RPSRC. omega. + apply RPSRC. lia. assert (PDST: Mem.perm m1 bdst (Ptrofs.unsigned odst) Cur Nonempty). - apply RPDST. omega. + apply RPDST. lia. exploit Mem.address_inject. eauto. eexact PSRC. eauto. intros EQ1. exploit Mem.address_inject. eauto. eexact PDST. eauto. intros EQ2. exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]]. @@ -1258,7 +1260,7 @@ Proof. intros; eapply Mem.aligned_area_inject with (m := m1); eauto. eapply Mem.disjoint_or_equal_inject with (m := m1); eauto. apply Mem.range_perm_max with Cur; auto. - apply Mem.range_perm_max with Cur; auto. omega. + apply Mem.range_perm_max with Cur; auto. lia. split. constructor. split. auto. split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros. @@ -1268,11 +1270,11 @@ Proof. apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. eapply Mem.storebytes_range_perm; eauto. erewrite list_forall2_length; eauto. - omega. + lia. split. apply inject_incr_refl. red; intros; congruence. - (* trace length *) - intros; inv H. simpl; omega. + intros; inv H. simpl; lia. - (* receptive *) intros. assert (t1 = t2). inv H; inv H0; auto. subst t2. @@ -1318,7 +1320,7 @@ Proof. eapply eventval_list_match_inject; eauto. red; intros; congruence. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. exists vres1; exists m1; congruence. @@ -1363,7 +1365,7 @@ Proof. eapply eventval_match_inject; eauto. red; intros; congruence. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. @@ -1409,7 +1411,7 @@ Proof. econstructor; eauto. red; intros; congruence. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - inv H; inv H0. exists Vundef, m1; constructor. (* determ *) @@ -1443,7 +1445,7 @@ Proof. econstructor; eauto. red; intros; congruence. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - inv H; inv H0. exists Vundef, m1; constructor. (* determ *) @@ -1497,7 +1499,7 @@ Proof. constructor; auto. red; intros; congruence. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - inv H; inv H0. exists vres1, m1; constructor; auto. (* determ *) @@ -1623,7 +1625,7 @@ Proof. intros. destruct (plt (Mem.nextblock m2) (Mem.nextblock m1)). exploit external_call_valid_block; eauto. intros. eelim Plt_strict; eauto. - unfold Plt, Ple in *; zify; omega. + unfold Plt, Ple in *; zify; lia. Qed. (** Special case of [external_call_mem_inject_gen] (for backward compatibility) *) @@ -1738,7 +1740,7 @@ Qed. End EVAL_BUILTIN_ARG. -Hint Constructors eval_builtin_arg: barg. +Global Hint Constructors eval_builtin_arg: barg. (** Invariance by change of global environment. *) diff --git a/common/Globalenvs.v b/common/Globalenvs.v index d37fbd46..4c9e7889 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -55,7 +56,7 @@ Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option me | None => None end. Proof. - intros. red. omega. + intros. red. lia. apply Zwf_well_founded. Qed. @@ -849,8 +850,8 @@ Proof. intros until n. functional induction (store_zeros m b p n); intros. - inv H; apply Mem.unchanged_on_refl. - apply Mem.unchanged_on_trans with m'. -+ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. omega. -+ apply IHo; auto. intros; apply H0; omega. ++ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. lia. ++ apply IHo; auto. intros; apply H0; lia. - discriminate. Qed. @@ -879,7 +880,7 @@ Proof. - destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence. apply Mem.unchanged_on_trans with m1. eapply store_init_data_unchanged; eauto. intros; apply H0; tauto. - eapply IHil; eauto. intros; apply H0. generalize (init_data_size_pos a); omega. + eapply IHil; eauto. intros; apply H0. generalize (init_data_size_pos a); lia. Qed. (** Properties related to [loadbytes] *) @@ -887,7 +888,7 @@ Qed. Definition readbytes_as_zero (m: mem) (b: block) (ofs len: Z) : Prop := forall p n, ofs <= p -> p + Z.of_nat n <= ofs + len -> - Mem.loadbytes m b p (Z.of_nat n) = Some (list_repeat n (Byte Byte.zero)). + Mem.loadbytes m b p (Z.of_nat n) = Some (List.repeat (Byte Byte.zero) n). Lemma store_zeros_loadbytes: forall m b p n m', @@ -895,24 +896,24 @@ Lemma store_zeros_loadbytes: readbytes_as_zero m' b p n. Proof. intros until n; functional induction (store_zeros m b p n); red; intros. -- destruct n0. simpl. apply Mem.loadbytes_empty. omega. - rewrite Nat2Z.inj_succ in H1. omegaContradiction. +- destruct n0. simpl. apply Mem.loadbytes_empty. lia. + rewrite Nat2Z.inj_succ in H1. extlia. - destruct (zeq p0 p). - + subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. omega. + + subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. lia. rewrite Nat2Z.inj_succ in H1. rewrite Nat2Z.inj_succ. - replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by omega. - change (list_repeat (S n0) (Byte Byte.zero)) - with ((Byte Byte.zero :: nil) ++ list_repeat n0 (Byte Byte.zero)). + replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by lia. + change (List.repeat (Byte Byte.zero) (S n0)) + with ((Byte Byte.zero :: nil) ++ List.repeat (Byte Byte.zero) n0). apply Mem.loadbytes_concat. eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 = p). - eapply store_zeros_unchanged; eauto. intros; omega. - intros; omega. + eapply store_zeros_unchanged; eauto. intros; lia. + intros; lia. replace (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero). change 1 with (size_chunk Mint8unsigned). eapply Mem.loadbytes_store_same; eauto. unfold encode_val; unfold encode_int; unfold rev_if_be; destruct Archi.big_endian; reflexivity. - eapply IHo; eauto. omega. omega. omega. omega. - + eapply IHo; eauto. omega. omega. + eapply IHo; eauto. lia. lia. lia. lia. + + eapply IHo; eauto. lia. lia. - discriminate. Qed. @@ -924,11 +925,11 @@ Definition bytes_of_init_data (i: init_data): list memval := | Init_int64 n => inj_bytes (encode_int 8%nat (Int64.unsigned n)) | Init_float32 n => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n))) | Init_float64 n => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n))) - | Init_space n => list_repeat (Z.to_nat n) (Byte Byte.zero) + | Init_space n => List.repeat (Byte Byte.zero) (Z.to_nat n) | Init_addrof id ofs => match find_symbol ge id with | Some b => inj_value (if Archi.ptr64 then Q64 else Q32) (Vptr b ofs) - | None => list_repeat (if Archi.ptr64 then 8%nat else 4%nat) Undef + | None => List.repeat Undef (if Archi.ptr64 then 8%nat else 4%nat) end end. @@ -947,8 +948,8 @@ Proof. intros; destruct i; simpl in H; try apply (Mem.loadbytes_store_same _ _ _ _ _ _ H). - inv H. simpl. assert (EQ: Z.of_nat (Z.to_nat z) = Z.max z 0). - { destruct (zle 0 z). rewrite Z2Nat.id; xomega. destruct z; try discriminate. simpl. xomega. } - rewrite <- EQ. apply H0. omega. simpl. omega. + { destruct (zle 0 z). rewrite Z2Nat.id; extlia. destruct z; try discriminate. simpl. extlia. } + rewrite <- EQ. apply H0. lia. simpl. lia. - rewrite init_data_size_addrof. simpl. destruct (find_symbol ge i) as [b'|]; try discriminate. rewrite (Mem.loadbytes_store_same _ _ _ _ _ _ H). @@ -968,23 +969,23 @@ Lemma store_init_data_list_loadbytes: Mem.loadbytes m' b p (init_data_list_size il) = Some (bytes_of_init_data_list il). Proof. induction il as [ | i1 il]; simpl; intros. -- apply Mem.loadbytes_empty. omega. +- apply Mem.loadbytes_empty. lia. - generalize (init_data_size_pos i1) (init_data_list_size_pos il); intros P1 PL. destruct (store_init_data m b p i1) as [m1|] eqn:S; try discriminate. apply Mem.loadbytes_concat. eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 < p + init_data_size i1). eapply store_init_data_list_unchanged; eauto. - intros; omega. - intros; omega. + intros; lia. + intros; lia. eapply store_init_data_loadbytes; eauto. - red; intros; apply H0. omega. omega. + red; intros; apply H0. lia. lia. apply IHil with m1; auto. red; intros. eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => p + init_data_size i1 <= ofs1). eapply store_init_data_unchanged; eauto. - intros; omega. - intros; omega. - apply H0. omega. omega. + intros; lia. + intros; lia. + apply H0. lia. lia. auto. auto. Qed. @@ -1011,7 +1012,7 @@ Remark read_as_zero_unchanged: read_as_zero m' b ofs len. Proof. intros; red; intros. eapply Mem.load_unchanged_on; eauto. - intros; apply H1. omega. + intros; apply H1. lia. Qed. Lemma store_zeros_read_as_zero: @@ -1020,7 +1021,7 @@ Lemma store_zeros_read_as_zero: read_as_zero m' b p n. Proof. intros; red; intros. - transitivity (Some(decode_val chunk (list_repeat (size_chunk_nat chunk) (Byte Byte.zero)))). + transitivity (Some(decode_val chunk (List.repeat (Byte Byte.zero) (size_chunk_nat chunk)))). apply Mem.loadbytes_load; auto. rewrite size_chunk_conv. eapply store_zeros_loadbytes; eauto. rewrite <- size_chunk_conv; auto. f_equal. destruct chunk; unfold decode_val; unfold decode_int; unfold rev_if_be; destruct Archi.big_endian; reflexivity. @@ -1068,7 +1069,7 @@ Proof. { intros. eapply Mem.load_unchanged_on with (P := fun b' ofs' => ofs' < p + size_chunk chunk). - eapply store_init_data_list_unchanged; eauto. intros; omega. + eapply store_init_data_list_unchanged; eauto. intros; lia. intros; tauto. eapply Mem.load_store_same; eauto. } @@ -1078,10 +1079,10 @@ Proof. exploit IHil; eauto. set (P := fun (b': block) ofs' => p + init_data_size a <= ofs'). apply read_as_zero_unchanged with (m := m) (P := P). - red; intros; apply H0; auto. generalize (init_data_size_pos a); omega. omega. + red; intros; apply H0; auto. generalize (init_data_size_pos a); lia. lia. eapply store_init_data_unchanged with (P := P); eauto. - intros; unfold P. omega. - intros; unfold P. omega. + intros; unfold P. lia. + intros; unfold P. lia. intro D. destruct a; simpl in Heqo. + split; auto. eapply (A Mint8unsigned (Vint i)); eauto. @@ -1093,10 +1094,10 @@ Proof. + split; auto. set (P := fun (b': block) ofs' => ofs' < p + init_data_size (Init_space z)). inv Heqo. apply read_as_zero_unchanged with (m := m1) (P := P). - red; intros. apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega. + red; intros. apply H0; auto. simpl. generalize (init_data_list_size_pos il); extlia. eapply store_init_data_list_unchanged; eauto. - intros; unfold P. omega. - intros; unfold P. simpl; xomega. + intros; unfold P. lia. + intros; unfold P. simpl; extlia. + rewrite init_data_size_addrof in *. split; auto. destruct (find_symbol ge i); try congruence. @@ -1195,11 +1196,11 @@ Proof. * destruct (Mem.alloc m 0 1) as [m1 b] eqn:ALLOC. exploit Mem.alloc_result; eauto. intros RES. rewrite H, <- RES. split. - eapply Mem.perm_drop_1; eauto. omega. + eapply Mem.perm_drop_1; eauto. lia. intros. assert (0 <= ofs < 1). { eapply Mem.perm_alloc_3; eauto. eapply Mem.perm_drop_4; eauto. } exploit Mem.perm_drop_2; eauto. intros ORD. - split. omega. inv ORD; auto. + split. lia. inv ORD; auto. * set (init := gvar_init v) in *. set (sz := init_data_list_size init) in *. destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?. @@ -1442,7 +1443,7 @@ Proof. exploit alloc_global_neutral; eauto. assert (Ple (Pos.succ (Mem.nextblock m)) (Mem.nextblock m')). { rewrite EQ. apply advance_next_le. } - unfold Plt, Ple in *; zify; omega. + unfold Plt, Ple in *; zify; lia. Qed. End INITMEM_INJ. @@ -1563,9 +1564,9 @@ Lemma store_zeros_exists: Proof. intros until n. functional induction (store_zeros m b p n); intros PERM. - exists m; auto. -- apply IHo. red; intros. eapply Mem.perm_store_1; eauto. apply PERM. omega. +- apply IHo. red; intros. eapply Mem.perm_store_1; eauto. apply PERM. lia. - destruct (Mem.valid_access_store m Mint8unsigned b p Vzero) as (m' & STORE). - split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. omega. + split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. lia. simpl. apply Z.divide_1_l. congruence. Qed. @@ -1603,10 +1604,10 @@ Proof. - exists m; auto. - destruct H0. destruct (@store_init_data_exists m b p i1) as (m1 & S1); eauto. - red; intros. apply H. generalize (init_data_list_size_pos il); omega. + red; intros. apply H. generalize (init_data_list_size_pos il); lia. rewrite S1. apply IHil; eauto. - red; intros. erewrite <- store_init_data_perm by eauto. apply H. generalize (init_data_size_pos i1); omega. + red; intros. erewrite <- store_init_data_perm by eauto. apply H. generalize (init_data_size_pos i1); lia. Qed. Lemma alloc_global_exists: diff --git a/common/Linking.v b/common/Linking.v index ec828ea4..089f4fd2 100644 --- a/common/Linking.v +++ b/common/Linking.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -123,7 +124,7 @@ Defined. Next Obligation. inv H; inv H0; constructor; auto. congruence. - simpl. generalize (init_data_list_size_pos z). xomega. + simpl. generalize (init_data_list_size_pos z). extlia. Defined. Next Obligation. revert H; unfold link_varinit. diff --git a/common/Memdata.v b/common/Memdata.v index a09b90f5..c80b3754 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -7,10 +7,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -23,6 +24,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. +Require Import Lia. (** * Properties of memory chunks *) @@ -48,13 +50,13 @@ Definition largest_size_chunk := 8. Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8. Proof. - destruct chunk; simpl; omega. + destruct chunk; simpl; lia. Qed. Lemma size_chunk_pos: forall chunk, size_chunk chunk > 0. Proof. - intros. destruct chunk; simpl; omega. + intros. destruct chunk; simpl; lia. Qed. Definition size_chunk_nat (chunk: memory_chunk) : nat := @@ -72,7 +74,7 @@ Proof. intros. generalize (size_chunk_pos chunk). rewrite size_chunk_conv. destruct (size_chunk_nat chunk). - simpl; intros; omegaContradiction. + simpl; intros; extlia. intros; exists n; auto. Qed. @@ -108,7 +110,7 @@ Definition align_chunk (chunk: memory_chunk) : Z := Lemma align_chunk_pos: forall chunk, align_chunk chunk > 0. Proof. - intro. destruct chunk; simpl; omega. + intro. destruct chunk; simpl; lia. Qed. Lemma align_chunk_Mptr: align_chunk Mptr = if Archi.ptr64 then 8 else 4. @@ -127,7 +129,7 @@ Lemma align_le_divides: align_chunk chunk1 <= align_chunk chunk2 -> (align_chunk chunk1 | align_chunk chunk2). Proof. intros. destruct chunk1; destruct chunk2; simpl in *; - solve [ omegaContradiction + solve [ extlia | apply Z.divide_refl | exists 2; reflexivity | exists 4; reflexivity @@ -223,12 +225,12 @@ Proof. simpl. rewrite Zmod_1_r. auto. Opaque Byte.wordsize. rewrite Nat2Z.inj_succ. simpl. - replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega. - rewrite two_p_is_exp; try omega. + replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by lia. + rewrite two_p_is_exp; try lia. rewrite Zmod_recombine. rewrite IHn. rewrite Z.add_comm. change (Byte.unsigned (Byte.repr x)) with (Byte.Z_mod_modulus x). rewrite Byte.Z_mod_modulus_eq. reflexivity. - apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega. + apply two_p_gt_ZERO. lia. apply two_p_gt_ZERO. lia. Qed. Lemma rev_if_be_involutive: @@ -287,15 +289,15 @@ Proof. intros; simpl; auto. intros until y. rewrite Nat2Z.inj_succ. - replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega. - rewrite two_p_is_exp; try omega. + replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by lia. + rewrite two_p_is_exp; try lia. intro EQM. simpl; decEq. apply Byte.eqm_samerepr. red. eapply eqmod_divides; eauto. apply Z.divide_factor_r. apply IHn. destruct EQM as [k EQ]. exists k. rewrite EQ. - rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. omega. + rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. lia. Qed. Lemma encode_int_8_mod: @@ -378,14 +380,14 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval := | Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat (Int.unsigned n)) | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat (Int.unsigned n)) | Vint n, Mint32 => inj_bytes (encode_int 4%nat (Int.unsigned n)) - | Vptr b ofs, Mint32 => if Archi.ptr64 then list_repeat 4%nat Undef else inj_value Q32 v + | Vptr b ofs, Mint32 => if Archi.ptr64 then List.repeat Undef 4%nat else inj_value Q32 v | Vlong n, Mint64 => inj_bytes (encode_int 8%nat (Int64.unsigned n)) - | Vptr b ofs, Mint64 => if Archi.ptr64 then inj_value Q64 v else list_repeat 8%nat Undef + | Vptr b ofs, Mint64 => if Archi.ptr64 then inj_value Q64 v else List.repeat Undef 8%nat | Vsingle n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n))) | Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n))) | _, Many32 => inj_value Q32 v | _, Many64 => inj_value Q64 v - | _, _ => list_repeat (size_chunk_nat chunk) Undef + | _, _ => List.repeat Undef (size_chunk_nat chunk) end. Definition decode_val (chunk: memory_chunk) (vl: list memval) : val := @@ -524,9 +526,9 @@ Ltac solve_decode_encode_val_general := | |- context [ Int.repr(decode_int (encode_int 2 (Int.unsigned _))) ] => rewrite decode_encode_int_2 | |- context [ Int.repr(decode_int (encode_int 4 (Int.unsigned _))) ] => rewrite decode_encode_int_4 | |- context [ Int64.repr(decode_int (encode_int 8 (Int64.unsigned _))) ] => rewrite decode_encode_int_8 - | |- Vint (Int.sign_ext _ (Int.sign_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_idem; omega - | |- Vint (Int.zero_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.zero_ext_idem; omega - | |- Vint (Int.sign_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_zero_ext; omega + | |- Vint (Int.sign_ext _ (Int.sign_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_idem; lia + | |- Vint (Int.zero_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.zero_ext_idem; lia + | |- Vint (Int.sign_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_zero_ext; lia end. Lemma decode_encode_val_general: @@ -550,7 +552,7 @@ Lemma decode_encode_val_similar: v2 = Val.load_result chunk2 v1. Proof. intros until v2; intros TY SZ DE. - destruct chunk1; destruct chunk2; simpl in TY; try discriminate; simpl in SZ; try omegaContradiction; + destruct chunk1; destruct chunk2; simpl in TY; try discriminate; simpl in SZ; try extlia; destruct v1; auto. Qed. @@ -560,7 +562,7 @@ Lemma decode_val_rettype: Proof. intros. unfold decode_val. destruct (proj_bytes cl). -- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by omega; auto. +- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by lia; auto. - Local Opaque Val.load_result. destruct chunk; simpl; (exact I || apply Val.load_result_type || destruct Archi.ptr64; (exact I || apply Val.load_result_type)). @@ -660,7 +662,7 @@ Proof. exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q). { induction n; simpl; intros. contradiction. destruct H0. - exists n; split; auto. omega. apply IHn; auto. omega. + exists n; split; auto. lia. apply IHn; auto. lia. } assert (B: forall q, q = quantity_chunk chunk -> @@ -670,7 +672,7 @@ Proof. Local Transparent inj_value. intros. unfold inj_value. destruct (size_quantity_nat_pos q) as [sz' EQ']. rewrite EQ'. simpl. constructor; auto. - intros; eapply A; eauto. omega. + intros; eapply A; eauto. lia. } assert (C: forall bl, match v with Vint _ => True | Vlong _ => True | Vfloat _ => True | Vsingle _ => True | _ => False end -> @@ -681,10 +683,10 @@ Local Transparent inj_value. constructor; auto. unfold inj_bytes; intros. exploit list_in_map_inv; eauto. intros (b & P & Q); exists b; auto. } - assert (D: shape_encoding chunk v (list_repeat (size_chunk_nat chunk) Undef)). + assert (D: shape_encoding chunk v (List.repeat Undef (size_chunk_nat chunk))). { intros. rewrite EQ; simpl; constructor; auto. - intros. eapply in_list_repeat; eauto. + intros. eapply repeat_spec; eauto. } generalize (encode_val_length chunk v). intros LEN. unfold encode_val; unfold encode_val in LEN; @@ -726,8 +728,8 @@ Proof. induction n; destruct mvs; simpl; intros; try discriminate. contradiction. destruct m; try discriminate. InvBooleans. apply beq_nat_true in H4. subst. - destruct H0. subst mv. exists n0; split; auto. omega. - eapply IHn; eauto. omega. + destruct H0. subst mv. exists n0; split; auto. lia. + eapply IHn; eauto. lia. } assert (U: forall mvs, shape_decoding chunk mvs (Val.load_result chunk Vundef)). { @@ -747,7 +749,7 @@ Proof. simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto. destruct H0 as [E|[E|[E|E]]]; subst chunk; destruct q; auto || discriminate. congruence. - intros. eapply B; eauto. omega. + intros. eapply B; eauto. lia. } unfold decode_val. destruct (proj_bytes (mv1 :: mvl)) as [bl|] eqn:PB. @@ -889,21 +891,21 @@ Qed. Lemma repeat_Undef_inject_any: forall f vl, - list_forall2 (memval_inject f) (list_repeat (length vl) Undef) vl. + list_forall2 (memval_inject f) (List.repeat Undef (length vl)) vl. Proof. induction vl; simpl; constructor; auto. constructor. Qed. Lemma repeat_Undef_inject_encode_val: forall f chunk v, - list_forall2 (memval_inject f) (list_repeat (size_chunk_nat chunk) Undef) (encode_val chunk v). + list_forall2 (memval_inject f) (List.repeat Undef (size_chunk_nat chunk)) (encode_val chunk v). Proof. intros. rewrite <- (encode_val_length chunk v). apply repeat_Undef_inject_any. Qed. Lemma repeat_Undef_inject_self: forall f n, - list_forall2 (memval_inject f) (list_repeat n Undef) (list_repeat n Undef). + list_forall2 (memval_inject f) (List.repeat Undef n) (List.repeat Undef n). Proof. induction n; simpl; constructor; auto. constructor. Qed. @@ -922,7 +924,7 @@ Theorem encode_val_inject: Val.inject f v1 v2 -> list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2). Proof. -Local Opaque list_repeat. +Local Opaque List.repeat. intros. inversion H; subst; simpl; destruct chunk; auto using inj_bytes_inject, inj_value_inject, repeat_Undef_inject_self, repeat_Undef_inject_encode_val. - destruct Archi.ptr64; auto using inj_value_inject, repeat_Undef_inject_self. @@ -962,22 +964,22 @@ Proof. induction l1; simpl int_of_bytes; intros. simpl. ring. simpl length. rewrite Nat2Z.inj_succ. - replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z.of_nat (length l1) * 8 + 8) by omega. + replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z.of_nat (length l1) * 8 + 8) by lia. rewrite two_p_is_exp. change (two_p 8) with 256. rewrite IHl1. ring. - omega. omega. + lia. lia. Qed. Lemma int_of_bytes_range: forall l, 0 <= int_of_bytes l < two_p (Z.of_nat (length l) * 8). Proof. induction l; intros. - simpl. omega. + simpl. lia. simpl length. rewrite Nat2Z.inj_succ. - replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by omega. + replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by lia. rewrite two_p_is_exp. change (two_p 8) with 256. simpl int_of_bytes. generalize (Byte.unsigned_range a). - change Byte.modulus with 256. omega. - omega. omega. + change Byte.modulus with 256. lia. + lia. lia. Qed. Lemma length_proj_bytes: @@ -1021,7 +1023,7 @@ Proof. intros. apply Int.unsigned_repr. generalize (int_of_bytes_range l). rewrite H2. change (two_p (Z.of_nat 4 * 8)) with (Int.max_unsigned + 1). - omega. + lia. apply Val.lessdef_same. unfold decode_int, rev_if_be. destruct Archi.big_endian; rewrite B1; rewrite B2. + rewrite <- (rev_length b1) in L1. @@ -1043,18 +1045,18 @@ Lemma bytes_of_int_append: bytes_of_int n1 x1 ++ bytes_of_int n2 x2. Proof. induction n1; intros. -- simpl in *. f_equal. omega. +- simpl in *. f_equal. lia. - assert (E: two_p (Z.of_nat (S n1) * 8) = two_p (Z.of_nat n1 * 8) * 256). { rewrite Nat2Z.inj_succ. change 256 with (two_p 8). rewrite <- two_p_is_exp. - f_equal. omega. omega. omega. + f_equal. lia. lia. lia. } rewrite E in *. simpl. f_equal. apply Byte.eqm_samerepr. exists (x2 * two_p (Z.of_nat n1 * 8)). change Byte.modulus with 256. ring. rewrite Z.mul_assoc. rewrite Z_div_plus. apply IHn1. - apply Zdiv_interval_1. omega. apply two_p_gt_ZERO; omega. omega. - assumption. omega. + apply Zdiv_interval_1. lia. apply two_p_gt_ZERO; lia. lia. + assumption. lia. Qed. Lemma bytes_of_int64: diff --git a/common/Memory.v b/common/Memory.v index 65f36966..bf8ca083 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -9,10 +9,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -212,11 +213,11 @@ Proof. induction lo using (well_founded_induction_type (Zwf_up_well_founded hi)). destruct (zlt lo hi). destruct (perm_dec m b lo k p). - destruct (H (lo + 1)). red. omega. - left; red; intros. destruct (zeq lo ofs). congruence. apply r. omega. - right; red; intros. elim n. red; intros; apply H0; omega. - right; red; intros. elim n. apply H0. omega. - left; red; intros. omegaContradiction. + destruct (H (lo + 1)). red. lia. + left; red; intros. destruct (zeq lo ofs). congruence. apply r. lia. + right; red; intros. elim n. red; intros; apply H0; lia. + right; red; intros. elim n. apply H0. lia. + left; red; intros. extlia. Defined. (** [valid_access m chunk b ofs p] holds if a memory access @@ -257,7 +258,7 @@ Theorem valid_access_valid_block: Proof. intros. destruct H. assert (perm m b ofs Cur Nonempty). - apply H. generalize (size_chunk_pos chunk). omega. + apply H. generalize (size_chunk_pos chunk). lia. eauto with mem. Qed. @@ -268,7 +269,7 @@ Lemma valid_access_perm: valid_access m chunk b ofs p -> perm m b ofs k p. Proof. - intros. destruct H. apply perm_cur. apply H. generalize (size_chunk_pos chunk). omega. + intros. destruct H. apply perm_cur. apply H. generalize (size_chunk_pos chunk). lia. Qed. Lemma valid_access_compat: @@ -314,9 +315,9 @@ Theorem valid_pointer_valid_access: Proof. intros. rewrite valid_pointer_nonempty_perm. split; intros. - split. simpl; red; intros. replace ofs0 with ofs by omega. auto. + split. simpl; red; intros. replace ofs0 with ofs by lia. auto. simpl. apply Z.divide_1_l. - destruct H. apply H. simpl. omega. + destruct H. apply H. simpl. lia. Qed. (** C allows pointers one past the last element of an array. These are not @@ -486,8 +487,8 @@ Proof. auto. simpl length in H. rewrite Nat2Z.inj_succ in H. transitivity (ZMap.get q (ZMap.set p a c)). - apply IHvl. intros. apply H. omega. - apply ZMap.gso. apply not_eq_sym. apply H. omega. + apply IHvl. intros. apply H. lia. + apply ZMap.gso. apply not_eq_sym. apply H. lia. Qed. Remark setN_outside: @@ -496,7 +497,7 @@ Remark setN_outside: ZMap.get q (setN vl p c) = ZMap.get q c. Proof. intros. apply setN_other. - intros. omega. + intros. lia. Qed. Remark getN_setN_same: @@ -506,7 +507,7 @@ Proof. induction vl; intros; simpl. auto. decEq. - rewrite setN_outside. apply ZMap.gss. omega. + rewrite setN_outside. apply ZMap.gss. lia. apply IHvl. Qed. @@ -516,7 +517,7 @@ Remark getN_exten: getN n p c1 = getN n p c2. Proof. induction n; intros. auto. rewrite Nat2Z.inj_succ in H. simpl. decEq. - apply H. omega. apply IHn. intros. apply H. omega. + apply H. lia. apply IHn. intros. apply H. lia. Qed. Remark getN_setN_disjoint: @@ -682,7 +683,7 @@ Qed. Theorem valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p. Proof. intros. red; intros. elim (perm_empty b ofs Cur p). apply H. - generalize (size_chunk_pos chunk); omega. + generalize (size_chunk_pos chunk); lia. Qed. (** ** Properties related to [load] *) @@ -847,7 +848,7 @@ Theorem loadbytes_empty: n <= 0 -> loadbytes m b ofs n = Some nil. Proof. intros. unfold loadbytes. rewrite pred_dec_true. rewrite Z_to_nat_neg; auto. - red; intros. omegaContradiction. + red; intros. extlia. Qed. Lemma getN_concat: @@ -855,9 +856,9 @@ Lemma getN_concat: getN (n1 + n2)%nat p c = getN n1 p c ++ getN n2 (p + Z.of_nat n1) c. Proof. induction n1; intros. - simpl. decEq. omega. + simpl. decEq. lia. rewrite Nat2Z.inj_succ. simpl. decEq. - replace (p + Z.succ (Z.of_nat n1)) with ((p + 1) + Z.of_nat n1) by omega. + replace (p + Z.succ (Z.of_nat n1)) with ((p + 1) + Z.of_nat n1) by lia. auto. Qed. @@ -871,12 +872,12 @@ Proof. unfold loadbytes; intros. destruct (range_perm_dec m b ofs (ofs + n1) Cur Readable); try congruence. destruct (range_perm_dec m b (ofs + n1) (ofs + n1 + n2) Cur Readable); try congruence. - rewrite pred_dec_true. rewrite Z2Nat.inj_add by omega. - rewrite getN_concat. rewrite Z2Nat.id by omega. + rewrite pred_dec_true. rewrite Z2Nat.inj_add by lia. + rewrite getN_concat. rewrite Z2Nat.id by lia. congruence. red; intros. - assert (ofs0 < ofs + n1 \/ ofs0 >= ofs + n1) by omega. - destruct H4. apply r; omega. apply r0; omega. + assert (ofs0 < ofs + n1 \/ ofs0 >= ofs + n1) by lia. + destruct H4. apply r; lia. apply r0; lia. Qed. Theorem loadbytes_split: @@ -891,13 +892,13 @@ Proof. unfold loadbytes; intros. destruct (range_perm_dec m b ofs (ofs + (n1 + n2)) Cur Readable); try congruence. - rewrite Z2Nat.inj_add in H by omega. rewrite getN_concat in H. - rewrite Z2Nat.id in H by omega. + rewrite Z2Nat.inj_add in H by lia. rewrite getN_concat in H. + rewrite Z2Nat.id in H by lia. repeat rewrite pred_dec_true. econstructor; econstructor. split. reflexivity. split. reflexivity. congruence. - red; intros; apply r; omega. - red; intros; apply r; omega. + red; intros; apply r; lia. + red; intros; apply r; lia. Qed. Theorem load_rep: @@ -917,13 +918,13 @@ Proof. revert ofs H; induction n; intros; simpl; auto. f_equal. rewrite Nat2Z.inj_succ in H. - replace ofs with (ofs+0) by omega. - apply H; omega. + replace ofs with (ofs+0) by lia. + apply H; lia. apply IHn. intros. rewrite <- Z.add_assoc. apply H. - rewrite Nat2Z.inj_succ. omega. + rewrite Nat2Z.inj_succ. lia. Qed. Theorem load_int64_split: @@ -938,7 +939,7 @@ Proof. exploit load_valid_access; eauto. intros [A B]. simpl in *. exploit load_loadbytes. eexact H. simpl. intros [bytes [LB EQ]]. change 8 with (4 + 4) in LB. - exploit loadbytes_split. eexact LB. omega. omega. + exploit loadbytes_split. eexact LB. lia. lia. intros (bytes1 & bytes2 & LB1 & LB2 & APP). change 4 with (size_chunk Mint32) in LB1. exploit loadbytes_load. eexact LB1. @@ -970,11 +971,11 @@ Proof. change (Int.unsigned (Int.repr 4)) with 4. apply Ptrofs.unsigned_repr. exploit (Zdivide_interval (Ptrofs.unsigned i) Ptrofs.modulus 8). - omega. apply Ptrofs.unsigned_range. auto. + lia. apply Ptrofs.unsigned_range. auto. exists (two_p (Ptrofs.zwordsize - 3)). unfold Ptrofs.modulus, Ptrofs.zwordsize, Ptrofs.wordsize. unfold Wordsize_Ptrofs.wordsize. destruct Archi.ptr64; reflexivity. - unfold Ptrofs.max_unsigned. omega. + unfold Ptrofs.max_unsigned. lia. Qed. Theorem loadv_int64_split: @@ -1131,7 +1132,7 @@ Qed. Theorem load_store_same: load chunk m2 b ofs = Some (Val.load_result chunk v). Proof. - apply load_store_similar_2; auto. omega. + apply load_store_similar_2; auto. lia. Qed. Theorem load_store_other: @@ -1183,9 +1184,9 @@ Proof. destruct H. congruence. destruct (zle n 0) as [z | n0]. rewrite (Z_to_nat_neg _ z). auto. - destruct H. omegaContradiction. + destruct H. extlia. apply getN_setN_outside. rewrite encode_val_length. rewrite <- size_chunk_conv. - rewrite Z2Nat.id. auto. omega. + rewrite Z2Nat.id. auto. lia. auto. red; intros. eauto with mem. rewrite pred_dec_false. auto. @@ -1198,11 +1199,11 @@ Lemma setN_in: In (ZMap.get q (setN vl p c)) vl. Proof. induction vl; intros. - simpl in H. omegaContradiction. + simpl in H. extlia. simpl length in H. rewrite Nat2Z.inj_succ in H. simpl. destruct (zeq p q). subst q. rewrite setN_outside. rewrite ZMap.gss. - auto with coqlib. omega. - right. apply IHvl. omega. + auto with coqlib. lia. + right. apply IHvl. lia. Qed. Lemma getN_in: @@ -1211,10 +1212,10 @@ Lemma getN_in: In (ZMap.get q c) (getN n p c). Proof. induction n; intros. - simpl in H; omegaContradiction. + simpl in H; extlia. rewrite Nat2Z.inj_succ in H. simpl. destruct (zeq p q). subst q. auto. - right. apply IHn. omega. + right. apply IHn. lia. Qed. End STORE. @@ -1363,28 +1364,28 @@ Proof. split. rewrite V', SIZE'. apply decode_val_shape. destruct (zeq ofs' ofs). - subst ofs'. left; split. auto. unfold c'. simpl. - rewrite setN_outside by omega. apply ZMap.gss. + rewrite setN_outside by lia. apply ZMap.gss. - right. destruct (zlt ofs ofs'). (* If ofs < ofs': the load reads (at ofs') a continuation byte from the write. ofs ofs' ofs+|chunk| [-------------------] write [-------------------] read *) -+ left; split. omega. unfold c'. simpl. apply setN_in. ++ left; split. lia. unfold c'. simpl. apply setN_in. assert (Z.of_nat (length (mv1 :: mvl)) = size_chunk chunk). { rewrite <- ENC; rewrite encode_val_length. rewrite size_chunk_conv; auto. } - simpl length in H3. rewrite Nat2Z.inj_succ in H3. omega. + simpl length in H3. rewrite Nat2Z.inj_succ in H3. lia. (* If ofs > ofs': the load reads (at ofs) the first byte from the write. ofs' ofs ofs'+|chunk'| [-------------------] write [----------------] read *) -+ right; split. omega. replace mv1 with (ZMap.get ofs c'). ++ right; split. lia. replace mv1 with (ZMap.get ofs c'). apply getN_in. assert (size_chunk chunk' = Z.succ (Z.of_nat sz')). { rewrite size_chunk_conv. rewrite SIZE'. rewrite Nat2Z.inj_succ; auto. } - omega. - unfold c'. simpl. rewrite setN_outside by omega. apply ZMap.gss. + lia. + unfold c'. simpl. rewrite setN_outside by lia. apply ZMap.gss. Qed. Definition compat_pointer_chunks (chunk1 chunk2: memory_chunk) : Prop := @@ -1471,10 +1472,10 @@ Theorem load_store_pointer_mismatch: Proof. intros. exploit load_store_overlap; eauto. - generalize (size_chunk_pos chunk'); omega. - generalize (size_chunk_pos chunk); omega. + generalize (size_chunk_pos chunk'); lia. + generalize (size_chunk_pos chunk); lia. intros (mv1 & mvl & mv1' & mvl' & ENC & DEC & CASES). - destruct CASES as [(A & B) | [(A & B) | (A & B)]]; try omegaContradiction. + destruct CASES as [(A & B) | [(A & B) | (A & B)]]; try extlia. inv ENC; inv DEC; auto. - elim H1. apply compat_pointer_chunks_true; auto. - contradiction. @@ -1496,8 +1497,8 @@ Proof. destruct (valid_access_dec m chunk1 b ofs Writable); destruct (valid_access_dec m chunk2 b ofs Writable); auto. f_equal. apply mkmem_ext; auto. congruence. - elim n. apply valid_access_compat with chunk1; auto. omega. - elim n. apply valid_access_compat with chunk2; auto. omega. + elim n. apply valid_access_compat with chunk1; auto. lia. + elim n. apply valid_access_compat with chunk2; auto. lia. Qed. Theorem store_signed_unsigned_8: @@ -1543,7 +1544,7 @@ Proof. destruct (valid_access_dec m Mfloat64 b ofs Writable); try discriminate. destruct (valid_access_dec m Mfloat64al32 b ofs Writable). rewrite <- H. f_equal. apply mkmem_ext; auto. - elim n. apply valid_access_compat with Mfloat64; auto. simpl; omega. + elim n. apply valid_access_compat with Mfloat64; auto. simpl; lia. Qed. Theorem storev_float64al32: @@ -1706,7 +1707,7 @@ Proof. rewrite pred_dec_true. rewrite storebytes_mem_contents. decEq. rewrite PMap.gsspec. destruct (peq b' b). subst b'. - apply getN_setN_disjoint. rewrite Z2Nat.id by omega. intuition congruence. + apply getN_setN_disjoint. rewrite Z2Nat.id by lia. intuition congruence. auto. red; auto with mem. apply pred_dec_false. @@ -1751,8 +1752,8 @@ Lemma setN_concat: setN (bytes1 ++ bytes2) ofs c = setN bytes2 (ofs + Z.of_nat (length bytes1)) (setN bytes1 ofs c). Proof. induction bytes1; intros. - simpl. decEq. omega. - simpl length. rewrite Nat2Z.inj_succ. simpl. rewrite IHbytes1. decEq. omega. + simpl. decEq. lia. + simpl length. rewrite Nat2Z.inj_succ. simpl. rewrite IHbytes1. decEq. lia. Qed. Theorem storebytes_concat: @@ -1771,8 +1772,8 @@ Proof. elim n. rewrite app_length. rewrite Nat2Z.inj_add. red; intros. destruct (zlt ofs0 (ofs + Z.of_nat(length bytes1))). - apply r. omega. - eapply perm_storebytes_2; eauto. apply r0. omega. + apply r. lia. + eapply perm_storebytes_2; eauto. apply r0. lia. Qed. Theorem storebytes_split: @@ -1785,10 +1786,10 @@ Proof. intros. destruct (range_perm_storebytes m b ofs bytes1) as [m1 ST1]. red; intros. exploit storebytes_range_perm; eauto. rewrite app_length. - rewrite Nat2Z.inj_add. omega. + rewrite Nat2Z.inj_add. lia. destruct (range_perm_storebytes m1 b (ofs + Z.of_nat (length bytes1)) bytes2) as [m2' ST2]. red; intros. eapply perm_storebytes_1; eauto. exploit storebytes_range_perm. - eexact H. instantiate (1 := ofs0). rewrite app_length. rewrite Nat2Z.inj_add. omega. + eexact H. instantiate (1 := ofs0). rewrite app_length. rewrite Nat2Z.inj_add. lia. auto. assert (Some m2 = Some m2'). rewrite <- H. eapply storebytes_concat; eauto. @@ -1896,7 +1897,7 @@ Theorem perm_alloc_2: Proof. unfold perm; intros. injection ALLOC; intros. rewrite <- H1; simpl. subst b. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. - rewrite zlt_true. simpl. auto with mem. omega. omega. + rewrite zlt_true. simpl. auto with mem. lia. lia. Qed. Theorem perm_alloc_inv: @@ -1940,7 +1941,7 @@ Theorem valid_access_alloc_same: valid_access m2 chunk b ofs Freeable. Proof. intros. constructor; auto with mem. - red; intros. apply perm_alloc_2. omega. + red; intros. apply perm_alloc_2. lia. Qed. Local Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem. @@ -1955,11 +1956,11 @@ Proof. intros. inv H. generalize (size_chunk_pos chunk); intro. destruct (eq_block b' b). subst b'. - assert (perm m2 b ofs Cur p). apply H0. omega. - assert (perm m2 b (ofs + size_chunk chunk - 1) Cur p). apply H0. omega. + assert (perm m2 b ofs Cur p). apply H0. lia. + assert (perm m2 b (ofs + size_chunk chunk - 1) Cur p). apply H0. lia. exploit perm_alloc_inv. eexact H2. rewrite dec_eq_true. intro. exploit perm_alloc_inv. eexact H3. rewrite dec_eq_true. intro. - intuition omega. + intuition lia. split; auto. red; intros. exploit perm_alloc_inv. apply H0. eauto. rewrite dec_eq_false; auto. Qed. @@ -2006,7 +2007,7 @@ Theorem load_alloc_same': Proof. intros. assert (exists v, load chunk m2 b ofs = Some v). apply valid_access_load. constructor; auto. - red; intros. eapply perm_implies. apply perm_alloc_2. omega. auto with mem. + red; intros. eapply perm_implies. apply perm_alloc_2. lia. auto with mem. destruct H2 as [v LOAD]. rewrite LOAD. decEq. eapply load_alloc_same; eauto. Qed. @@ -2116,7 +2117,7 @@ Theorem perm_free_2: Proof. intros. rewrite free_result. unfold perm, unchecked_free; simpl. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. - simpl. tauto. omega. omega. + simpl. tauto. lia. lia. Qed. Theorem perm_free_3: @@ -2149,7 +2150,7 @@ Theorem valid_access_free_1: Proof. intros. inv H. constructor; auto with mem. red; intros. eapply perm_free_1; eauto. - destruct (zlt lo hi). intuition. right. omega. + destruct (zlt lo hi). intuition. right. lia. Qed. Theorem valid_access_free_2: @@ -2161,9 +2162,9 @@ Proof. generalize (size_chunk_pos chunk); intros. destruct (zlt ofs lo). elim (perm_free_2 lo Cur p). - omega. apply H3. omega. + lia. apply H3. lia. elim (perm_free_2 ofs Cur p). - omega. apply H3. omega. + lia. apply H3. lia. Qed. Theorem valid_access_free_inv_1: @@ -2189,7 +2190,7 @@ Proof. destruct (zlt lo hi); auto. destruct (zle (ofs + size_chunk chunk) lo); auto. destruct (zle hi ofs); auto. - elim (valid_access_free_2 chunk ofs p); auto. omega. + elim (valid_access_free_2 chunk ofs p); auto. lia. Qed. Theorem load_free: @@ -2227,7 +2228,7 @@ Proof. red; intros. eapply perm_free_3; eauto. rewrite pred_dec_false; auto. red; intros. elim n0; red; intros. - eapply perm_free_1; eauto. destruct H; auto. right; omega. + eapply perm_free_1; eauto. destruct H; auto. right; lia. Qed. Theorem loadbytes_free_2: @@ -2297,7 +2298,7 @@ Proof. unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. unfold perm. simpl. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. simpl. constructor. - omega. omega. + lia. lia. Qed. Theorem perm_drop_2: @@ -2307,7 +2308,7 @@ Proof. unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. revert H0. unfold perm; simpl. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. simpl. auto. - omega. omega. + lia. lia. Qed. Theorem perm_drop_3: @@ -2317,7 +2318,7 @@ Proof. unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. unfold perm; simpl. rewrite PMap.gsspec. destruct (peq b' b). subst b'. unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi). - byContradiction. intuition omega. + byContradiction. intuition lia. auto. auto. auto. Qed. @@ -2343,7 +2344,7 @@ Proof. destruct (eq_block b' b). subst b'. destruct (zlt ofs0 lo). eapply perm_drop_3; eauto. destruct (zle hi ofs0). eapply perm_drop_3; eauto. - apply perm_implies with p. eapply perm_drop_1; eauto. omega. + apply perm_implies with p. eapply perm_drop_1; eauto. lia. generalize (size_chunk_pos chunk); intros. intuition. eapply perm_drop_3; eauto. Qed. @@ -2385,7 +2386,7 @@ Proof. destruct (eq_block b' b). subst b'. destruct (zlt ofs0 lo). eapply perm_drop_3; eauto. destruct (zle hi ofs0). eapply perm_drop_3; eauto. - apply perm_implies with p. eapply perm_drop_1; eauto. omega. intuition. + apply perm_implies with p. eapply perm_drop_1; eauto. lia. intuition. eapply perm_drop_3; eauto. rewrite pred_dec_false; eauto. red; intros; elim n0; red; intros. @@ -2443,8 +2444,8 @@ Lemma range_perm_inj: range_perm m2 b2 (lo + delta) (hi + delta) k p. Proof. intros; red; intros. - replace ofs with ((ofs - delta) + delta) by omega. - eapply perm_inj; eauto. apply H0. omega. + replace ofs with ((ofs - delta) + delta) by lia. + eapply perm_inj; eauto. apply H0. lia. Qed. Lemma valid_access_inj: @@ -2456,7 +2457,7 @@ Lemma valid_access_inj: Proof. intros. destruct H1 as [A B]. constructor. replace (ofs + delta + size_chunk chunk) - with ((ofs + size_chunk chunk) + delta) by omega. + with ((ofs + size_chunk chunk) + delta) by lia. eapply range_perm_inj; eauto. apply Z.divide_add_r; auto. eapply mi_align; eauto with mem. Qed. @@ -2478,9 +2479,9 @@ Proof. rewrite Nat2Z.inj_succ in H1. constructor. eapply mi_memval; eauto. - apply H1. omega. - replace (ofs + delta + 1) with ((ofs + 1) + delta) by omega. - apply IHn. red; intros; apply H1; omega. + apply H1. lia. + replace (ofs + delta + 1) with ((ofs + 1) + delta) by lia. + apply IHn. red; intros; apply H1; lia. Qed. Lemma load_inj: @@ -2511,11 +2512,11 @@ Proof. destruct (range_perm_dec m1 b1 ofs (ofs + len) Cur Readable); inv H0. exists (getN (Z.to_nat len) (ofs + delta) (m2.(mem_contents)#b2)). split. apply pred_dec_true. - replace (ofs + delta + len) with ((ofs + len) + delta) by omega. + replace (ofs + delta + len) with ((ofs + len) + delta) by lia. eapply range_perm_inj; eauto with mem. apply getN_inj; auto. - destruct (zle 0 len). rewrite Z2Nat.id by omega. auto. - rewrite Z_to_nat_neg by omega. simpl. red; intros; omegaContradiction. + destruct (zle 0 len). rewrite Z2Nat.id by lia. auto. + rewrite Z_to_nat_neg by lia. simpl. red; intros; extlia. Qed. (** Preservation of stores. *) @@ -2530,11 +2531,11 @@ Lemma setN_inj: Proof. induction 1; intros; simpl. auto. - replace (p + delta + 1) with ((p + 1) + delta) by omega. + replace (p + delta + 1) with ((p + 1) + delta) by lia. apply IHlist_forall2; auto. intros. rewrite ZMap.gsspec at 1. destruct (ZIndexed.eq q0 p). subst q0. rewrite ZMap.gss. auto. - rewrite ZMap.gso. auto. unfold ZIndexed.t in *. omega. + rewrite ZMap.gso. auto. unfold ZIndexed.t in *. lia. Qed. Definition meminj_no_overlap (f: meminj) (m: mem) : Prop := @@ -2589,8 +2590,8 @@ Proof. assert (b2 <> b2 \/ ofs0 + delta0 <> (r - delta) + delta). eapply H1; eauto. eauto 6 with mem. exploit store_valid_access_3. eexact H0. intros [A B]. - eapply perm_implies. apply perm_cur_max. apply A. omega. auto with mem. - destruct H8. congruence. omega. + eapply perm_implies. apply perm_cur_max. apply A. lia. auto with mem. + destruct H8. congruence. lia. (* block <> b1, block <> b2 *) eapply mi_memval; eauto. eauto with mem. Qed. @@ -2637,8 +2638,8 @@ Proof. rewrite setN_outside. auto. rewrite encode_val_length. rewrite <- size_chunk_conv. destruct (zlt (ofs0 + delta) ofs); auto. - destruct (zle (ofs + size_chunk chunk) (ofs0 + delta)). omega. - byContradiction. eapply H0; eauto. omega. + destruct (zle (ofs + size_chunk chunk) (ofs0 + delta)). lia. + byContradiction. eapply H0; eauto. lia. eauto with mem. Qed. @@ -2659,7 +2660,7 @@ Proof. with ((ofs + Z.of_nat (length bytes1)) + delta). eapply range_perm_inj; eauto with mem. eapply storebytes_range_perm; eauto. - rewrite (list_forall2_length H3). omega. + rewrite (list_forall2_length H3). lia. destruct (range_perm_storebytes _ _ _ _ H4) as [n2 STORE]. exists n2; split. eauto. constructor. @@ -2690,9 +2691,9 @@ Proof. eapply H1; eauto 6 with mem. exploit storebytes_range_perm. eexact H0. instantiate (1 := r - delta). - rewrite (list_forall2_length H3). omega. + rewrite (list_forall2_length H3). lia. eauto 6 with mem. - destruct H9. congruence. omega. + destruct H9. congruence. lia. (* block <> b1, block <> b2 *) eauto. Qed. @@ -2739,8 +2740,8 @@ Proof. rewrite PMap.gsspec. destruct (peq b2 b). subst b2. rewrite setN_outside. auto. destruct (zlt (ofs0 + delta) ofs); auto. - destruct (zle (ofs + Z.of_nat (length bytes2)) (ofs0 + delta)). omega. - byContradiction. eapply H0; eauto. omega. + destruct (zle (ofs + Z.of_nat (length bytes2)) (ofs0 + delta)). lia. + byContradiction. eapply H0; eauto. lia. eauto with mem. Qed. @@ -2837,10 +2838,10 @@ Proof. intros. destruct (eq_block b0 b1). subst b0. assert (delta0 = delta) by congruence. subst delta0. assert (lo <= ofs < hi). - { eapply perm_alloc_3; eauto. apply H6. generalize (size_chunk_pos chunk); omega. } + { eapply perm_alloc_3; eauto. apply H6. generalize (size_chunk_pos chunk); lia. } assert (lo <= ofs + size_chunk chunk - 1 < hi). - { eapply perm_alloc_3; eauto. apply H6. generalize (size_chunk_pos chunk); omega. } - apply H2. omega. + { eapply perm_alloc_3; eauto. apply H6. generalize (size_chunk_pos chunk); lia. } + apply H2. lia. eapply mi_align0 with (ofs := ofs) (p := p); eauto. red; intros. eapply perm_alloc_4; eauto. (* mem_contents *) @@ -2885,7 +2886,7 @@ Proof. intros. eapply perm_free_1; eauto. destruct (eq_block b2 b); auto. subst b. right. assert (~ (lo <= ofs + delta < hi)). red; intros; eapply H1; eauto. - omega. + lia. constructor. (* perm *) auto. @@ -2930,8 +2931,8 @@ Proof. intros. assert ({ m2' | drop_perm m2 b2 (lo + delta) (hi + delta) p = Some m2' }). apply range_perm_drop_2. red; intros. - replace ofs with ((ofs - delta) + delta) by omega. - eapply perm_inj; eauto. eapply range_perm_drop_1; eauto. omega. + replace ofs with ((ofs - delta) + delta) by lia. + eapply perm_inj; eauto. eapply range_perm_drop_1; eauto. lia. destruct X as [m2' DROP]. exists m2'; split; auto. inv H. constructor. @@ -2945,9 +2946,9 @@ Proof. destruct (zlt (ofs + delta0) (lo + delta0)). eapply perm_drop_3; eauto. destruct (zle (hi + delta0) (ofs + delta0)). eapply perm_drop_3; eauto. assert (perm_order p p0). - eapply perm_drop_2. eexact H0. instantiate (1 := ofs). omega. eauto. + eapply perm_drop_2. eexact H0. instantiate (1 := ofs). lia. eauto. apply perm_implies with p; auto. - eapply perm_drop_1. eauto. omega. + eapply perm_drop_1. eauto. lia. (* b1 <> b0 *) eapply perm_drop_3; eauto. destruct (eq_block b3 b2); auto. @@ -2956,7 +2957,7 @@ Proof. exploit H1; eauto. instantiate (1 := ofs + delta0 - delta). apply perm_cur_max. apply perm_implies with Freeable. - eapply range_perm_drop_1; eauto. omega. auto with mem. + eapply range_perm_drop_1; eauto. lia. auto with mem. eapply perm_drop_4; eauto. eapply perm_max. apply perm_implies with p0. eauto. eauto with mem. intuition. @@ -2987,7 +2988,7 @@ Proof. destruct (eq_block b2 b); auto. subst b2. right. destruct (zlt (ofs + delta) lo); auto. destruct (zle hi (ofs + delta)); auto. - byContradiction. exploit H1; eauto. omega. + byContradiction. exploit H1; eauto. lia. (* align *) eapply mi_align0; eauto. (* contents *) @@ -3020,9 +3021,9 @@ Theorem extends_refl: forall m, extends m m. Proof. intros. constructor. auto. constructor. - intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. auto. + intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by lia. auto. intros. unfold inject_id in H; inv H. apply Z.divide_0_r. - intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. + intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by lia. apply memval_lessdef_refl. tauto. Qed. @@ -3035,7 +3036,7 @@ Theorem load_extends: Proof. intros. inv H. exploit load_inj; eauto. unfold inject_id; reflexivity. intros [v2 [A B]]. exists v2; split. - replace (ofs + 0) with ofs in A by omega. auto. + replace (ofs + 0) with ofs in A by lia. auto. rewrite val_inject_id in B. auto. Qed. @@ -3059,7 +3060,7 @@ Theorem loadbytes_extends: /\ list_forall2 memval_lessdef bytes1 bytes2. Proof. intros. inv H. - replace ofs with (ofs + 0) by omega. eapply loadbytes_inj; eauto. + replace ofs with (ofs + 0) by lia. eapply loadbytes_inj; eauto. Qed. Theorem store_within_extends: @@ -3078,7 +3079,7 @@ Proof. rewrite val_inject_id. eauto. intros [m2' [A B]]. exists m2'; split. - replace (ofs + 0) with ofs in A by omega. auto. + replace (ofs + 0) with ofs in A by lia. auto. constructor; auto. rewrite (nextblock_store _ _ _ _ _ _ H0). rewrite (nextblock_store _ _ _ _ _ _ A). @@ -3096,7 +3097,7 @@ Proof. intros. inversion H. constructor. rewrite (nextblock_store _ _ _ _ _ _ H0). auto. eapply store_outside_inj; eauto. - unfold inject_id; intros. inv H2. eapply H1; eauto. omega. + unfold inject_id; intros. inv H2. eapply H1; eauto. lia. intros. eauto using perm_store_2. Qed. @@ -3130,7 +3131,7 @@ Proof. unfold inject_id; reflexivity. intros [m2' [A B]]. exists m2'; split. - replace (ofs + 0) with ofs in A by omega. auto. + replace (ofs + 0) with ofs in A by lia. auto. constructor; auto. rewrite (nextblock_storebytes _ _ _ _ _ H0). rewrite (nextblock_storebytes _ _ _ _ _ A). @@ -3148,7 +3149,7 @@ Proof. intros. inversion H. constructor. rewrite (nextblock_storebytes _ _ _ _ _ H0). auto. eapply storebytes_outside_inj; eauto. - unfold inject_id; intros. inv H2. eapply H1; eauto. omega. + unfold inject_id; intros. inv H2. eapply H1; eauto. lia. intros. eauto using perm_storebytes_2. Qed. @@ -3180,12 +3181,12 @@ Proof. intros. eapply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. - omega. + lia. intros. eapply perm_alloc_inv in H; eauto. generalize (perm_alloc_inv _ _ _ _ _ H0 b0 ofs Max Nonempty); intros PERM. destruct (eq_block b0 b). subst b0. - assert (EITHER: lo1 <= ofs < hi1 \/ ~(lo1 <= ofs < hi1)) by omega. + assert (EITHER: lo1 <= ofs < hi1 \/ ~(lo1 <= ofs < hi1)) by lia. destruct EITHER. left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. right; tauto. @@ -3217,7 +3218,7 @@ Proof. intros. inv H. constructor. rewrite (nextblock_free _ _ _ _ _ H0). auto. eapply free_right_inj; eauto. - unfold inject_id; intros. inv H. eapply H1; eauto. omega. + unfold inject_id; intros. inv H. eapply H1; eauto. lia. intros. eauto using perm_free_3. Qed. @@ -3232,7 +3233,7 @@ Proof. intros. inversion H. assert ({ m2': mem | free m2 b lo hi = Some m2' }). apply range_perm_free. red; intros. - replace ofs with (ofs + 0) by omega. + replace ofs with (ofs + 0) by lia. eapply perm_inj with (b1 := b); eauto. eapply free_range_perm; eauto. destruct X as [m2' FREE]. exists m2'; split; auto. @@ -3242,7 +3243,7 @@ Proof. eapply free_right_inj with (m1 := m1'); eauto. eapply free_left_inj; eauto. unfold inject_id; intros. inv H1. - eapply perm_free_2. eexact H0. instantiate (1 := ofs); omega. eauto. + eapply perm_free_2. eexact H0. instantiate (1 := ofs); lia. eauto. intros. exploit mext_perm_inv0; eauto using perm_free_3. intros [A|A]. eapply perm_free_inv in A; eauto. destruct A as [[A B]|A]; auto. subst b0. right; eapply perm_free_2; eauto. @@ -3261,7 +3262,7 @@ Theorem perm_extends: forall m1 m2 b ofs k p, extends m1 m2 -> perm m1 b ofs k p -> perm m2 b ofs k p. Proof. - intros. inv H. replace ofs with (ofs + 0) by omega. + intros. inv H. replace ofs with (ofs + 0) by lia. eapply perm_inj; eauto. Qed. @@ -3276,7 +3277,7 @@ Theorem valid_access_extends: forall m1 m2 chunk b ofs p, extends m1 m2 -> valid_access m1 chunk b ofs p -> valid_access m2 chunk b ofs p. Proof. - intros. inv H. replace ofs with (ofs + 0) by omega. + intros. inv H. replace ofs with (ofs + 0) by lia. eapply valid_access_inj; eauto. auto. Qed. @@ -3421,7 +3422,7 @@ Theorem weak_valid_pointer_inject: weak_valid_pointer m2 b2 (ofs + delta) = true. Proof. intros until 2. unfold weak_valid_pointer. rewrite !orb_true_iff. - replace (ofs + delta - 1) with ((ofs - 1) + delta) by omega. + replace (ofs + delta - 1) with ((ofs - 1) + delta) by lia. intros []; eauto using valid_pointer_inject. Qed. @@ -3439,8 +3440,8 @@ Proof. assert (perm m1 b1 (Ptrofs.unsigned ofs1) Max Nonempty) by eauto with mem. exploit mi_representable; eauto. intros [A B]. assert (0 <= delta <= Ptrofs.max_unsigned). - generalize (Ptrofs.unsigned_range ofs1). omega. - unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; omega. + generalize (Ptrofs.unsigned_range ofs1). lia. + unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; lia. Qed. Lemma address_inject': @@ -3451,7 +3452,7 @@ Lemma address_inject': Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta. Proof. intros. destruct H0. eapply address_inject; eauto. - apply H0. generalize (size_chunk_pos chunk). omega. + apply H0. generalize (size_chunk_pos chunk). lia. Qed. Theorem weak_valid_pointer_inject_no_overflow: @@ -3466,7 +3467,7 @@ Proof. exploit mi_representable; eauto. destruct H0; eauto with mem. intros [A B]. pose proof (Ptrofs.unsigned_range ofs). - rewrite Ptrofs.unsigned_repr; omega. + rewrite Ptrofs.unsigned_repr; lia. Qed. Theorem valid_pointer_inject_no_overflow: @@ -3506,7 +3507,7 @@ Proof. exploit mi_representable; eauto. destruct H0; eauto with mem. intros [A B]. pose proof (Ptrofs.unsigned_range ofs). - unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; auto; omega. + unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; auto; lia. Qed. Theorem inject_no_overlap: @@ -3541,8 +3542,8 @@ Proof. rewrite (address_inject' _ _ _ _ _ _ _ _ H H2 H4). inv H1. simpl in H5. inv H2. simpl in H1. eapply mi_no_overlap; eauto. - apply perm_cur_max. apply (H5 (Ptrofs.unsigned ofs1)). omega. - apply perm_cur_max. apply (H1 (Ptrofs.unsigned ofs2)). omega. + apply perm_cur_max. apply (H5 (Ptrofs.unsigned ofs1)). lia. + apply perm_cur_max. apply (H1 (Ptrofs.unsigned ofs2)). lia. Qed. Theorem disjoint_or_equal_inject: @@ -3561,16 +3562,16 @@ Proof. intros. destruct (eq_block b1 b2). assert (b1' = b2') by congruence. assert (delta1 = delta2) by congruence. subst. - destruct H5. congruence. right. destruct H5. left; congruence. right. omega. + destruct H5. congruence. right. destruct H5. left; congruence. right. lia. destruct (eq_block b1' b2'); auto. subst. right. right. set (i1 := (ofs1 + delta1, ofs1 + delta1 + sz)). set (i2 := (ofs2 + delta2, ofs2 + delta2 + sz)). change (snd i1 <= fst i2 \/ snd i2 <= fst i1). - apply Intv.range_disjoint'; simpl; try omega. + apply Intv.range_disjoint'; simpl; try lia. unfold Intv.disjoint, Intv.In; simpl; intros. red; intros. exploit mi_no_overlap; eauto. - instantiate (1 := x - delta1). apply H2. omega. - instantiate (1 := x - delta2). apply H3. omega. + instantiate (1 := x - delta1). apply H2. lia. + instantiate (1 := x - delta2). apply H3. lia. intuition. Qed. @@ -3585,9 +3586,9 @@ Theorem aligned_area_inject: (al | ofs + delta). Proof. intros. - assert (P: al > 0) by omega. - assert (Q: Z.abs al <= Z.abs sz). apply Zdivide_bounds; auto. omega. - rewrite Z.abs_eq in Q; try omega. rewrite Z.abs_eq in Q; try omega. + assert (P: al > 0) by lia. + assert (Q: Z.abs al <= Z.abs sz). apply Zdivide_bounds; auto. lia. + rewrite Z.abs_eq in Q; try lia. rewrite Z.abs_eq in Q; try lia. assert (R: exists chunk, al = align_chunk chunk /\ al = size_chunk chunk). destruct H0. subst; exists Mint8unsigned; auto. destruct H0. subst; exists Mint16unsigned; auto. @@ -3595,7 +3596,7 @@ Proof. subst; exists Mint64; auto. destruct R as [chunk [A B]]. assert (valid_access m chunk b ofs Nonempty). - split. red; intros; apply H3. omega. congruence. + split. red; intros; apply H3. lia. congruence. exploit valid_access_inject; eauto. intros [C D]. congruence. Qed. @@ -3952,7 +3953,7 @@ Proof. unfold f'; intros. destruct (eq_block b0 b1). inversion H8. subst b0 b3 delta0. elim (fresh_block_alloc _ _ _ _ _ H0). - eapply perm_valid_block with (ofs := ofs). apply H9. generalize (size_chunk_pos chunk); omega. + eapply perm_valid_block with (ofs := ofs). apply H9. generalize (size_chunk_pos chunk); lia. eauto. unfold f'; intros. destruct (eq_block b0 b1). inversion H8. subst b0 b3 delta0. @@ -3975,10 +3976,10 @@ Proof. congruence. inversion H10; subst b0 b1' delta1. destruct (eq_block b2 b2'); auto. subst b2'. right; red; intros. - eapply H6; eauto. omega. + eapply H6; eauto. lia. inversion H11; subst b3 b2' delta2. destruct (eq_block b1' b2); auto. subst b1'. right; red; intros. - eapply H6; eauto. omega. + eapply H6; eauto. lia. eauto. (* representable *) unfold f'; intros. @@ -3986,16 +3987,16 @@ Proof. subst. injection H9; intros; subst b' delta0. destruct H10. exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto. - generalize (Ptrofs.unsigned_range_2 ofs). omega. + generalize (Ptrofs.unsigned_range_2 ofs). lia. exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto. - generalize (Ptrofs.unsigned_range_2 ofs). omega. + generalize (Ptrofs.unsigned_range_2 ofs). lia. eapply mi_representable0; try eassumption. destruct H10; eauto using perm_alloc_4. (* perm inv *) intros. unfold f' in H9; destruct (eq_block b0 b1). inversion H9; clear H9; subst b0 b3 delta0. - assert (EITHER: lo <= ofs < hi \/ ~(lo <= ofs < hi)) by omega. + assert (EITHER: lo <= ofs < hi \/ ~(lo <= ofs < hi)) by lia. destruct EITHER. left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. right; intros A. eapply perm_alloc_inv in A; eauto. rewrite dec_eq_true in A. tauto. @@ -4026,10 +4027,10 @@ Proof. eapply alloc_right_inject; eauto. eauto. instantiate (1 := b2). eauto with mem. - instantiate (1 := 0). unfold Ptrofs.max_unsigned. generalize Ptrofs.modulus_pos; omega. + instantiate (1 := 0). unfold Ptrofs.max_unsigned. generalize Ptrofs.modulus_pos; lia. auto. intros. apply perm_implies with Freeable; auto with mem. - eapply perm_alloc_2; eauto. omega. + eapply perm_alloc_2; eauto. lia. red; intros. apply Z.divide_0_r. intros. apply (valid_not_valid_diff m2 b2 b2); eauto with mem. intros [f' [A [B [C D]]]]. @@ -4152,13 +4153,13 @@ Proof. simpl; rewrite H0; auto. intros. destruct (eq_block b1 b). subst b1. rewrite H1 in H2; inv H2. - exists lo, hi; split; auto with coqlib. omega. + exists lo, hi; split; auto with coqlib. lia. exploit mi_no_overlap. eexact H. eexact n. eauto. eauto. eapply perm_max. eapply perm_implies. eauto. auto with mem. instantiate (1 := ofs + delta0 - delta). apply perm_cur_max. apply perm_implies with Freeable; auto with mem. - eapply free_range_perm; eauto. omega. - intros [A|A]. congruence. omega. + eapply free_range_perm; eauto. lia. + intros [A|A]. congruence. lia. Qed. Lemma drop_outside_inject: forall f m1 m2 b lo hi p m2', @@ -4185,7 +4186,7 @@ Proof. (* perm *) destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. destruct (f' b') as [[b'' delta''] |] eqn:?; inv H. - replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by omega. + replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by lia. eauto. (* align *) destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. @@ -4193,12 +4194,12 @@ Proof. apply Z.divide_add_r. eapply mi_align0; eauto. eapply mi_align1 with (ofs := ofs + delta') (p := p); eauto. - red; intros. replace ofs0 with ((ofs0 - delta') + delta') by omega. - eapply mi_perm0; eauto. apply H0. omega. + red; intros. replace ofs0 with ((ofs0 - delta') + delta') by lia. + eapply mi_perm0; eauto. apply H0. lia. (* memval *) destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. destruct (f' b') as [[b'' delta''] |] eqn:?; inv H. - replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by omega. + replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by lia. eapply memval_inject_compose; eauto. Qed. @@ -4227,11 +4228,11 @@ Proof. exploit mi_no_overlap0; eauto. intros A. destruct (eq_block b1x b2x). subst b1x. destruct A. congruence. - assert (delta1y = delta2y) by congruence. right; omega. + assert (delta1y = delta2y) by congruence. right; lia. exploit mi_no_overlap1. eauto. eauto. eauto. eapply perm_inj. eauto. eexact H2. eauto. eapply perm_inj. eauto. eexact H3. eauto. - intuition omega. + intuition lia. (* representable *) intros. destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate. @@ -4243,15 +4244,15 @@ Proof. exploit mi_representable1. eauto. instantiate (1 := ofs'). rewrite H. replace (Ptrofs.unsigned ofs + delta1 - 1) with - ((Ptrofs.unsigned ofs - 1) + delta1) by omega. + ((Ptrofs.unsigned ofs - 1) + delta1) by lia. destruct H0; eauto using perm_inj. - rewrite H. omega. + rewrite H. lia. (* perm inv *) intros. destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. destruct (f' b') as [[b'' delta''] |] eqn:?; try discriminate. inversion H; clear H; subst b'' delta. - replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') in H0 by omega. + replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') in H0 by lia. exploit mi_perm_inv1; eauto. intros [A|A]. eapply mi_perm_inv0; eauto. right; red; intros. elim A. eapply perm_inj; eauto. @@ -4303,7 +4304,7 @@ Proof. (* inj *) replace f with (compose_meminj f inject_id). eapply mem_inj_compose; eauto. apply extensionality; intros. unfold compose_meminj, inject_id. - destruct (f x) as [[y delta] | ]; auto. decEq. decEq. omega. + destruct (f x) as [[y delta] | ]; auto. decEq. decEq. lia. (* unmapped *) eauto. (* mapped *) @@ -4368,7 +4369,7 @@ Proof. apply flat_inj_no_overlap. (* range *) unfold flat_inj; intros. - destruct (plt b (nextblock m)); inv H0. generalize (Ptrofs.unsigned_range_2 ofs); omega. + destruct (plt b (nextblock m)); inv H0. generalize (Ptrofs.unsigned_range_2 ofs); lia. (* perm inv *) unfold flat_inj; intros. destruct (plt b1 (nextblock m)); inv H0. @@ -4381,7 +4382,7 @@ Proof. intros; red; constructor. (* perm *) unfold flat_inj; intros. destruct (plt b1 thr); inv H. - replace (ofs + 0) with ofs by omega; auto. + replace (ofs + 0) with ofs by lia; auto. (* align *) unfold flat_inj; intros. destruct (plt b1 thr); inv H. apply Z.divide_0_r. (* mem_contents *) @@ -4401,7 +4402,7 @@ Proof. red. intros. apply Z.divide_0_r. intros. apply perm_implies with Freeable; auto with mem. - eapply perm_alloc_2; eauto. omega. + eapply perm_alloc_2; eauto. lia. unfold flat_inj. apply pred_dec_true. rewrite (alloc_result _ _ _ _ _ H). auto. Qed. @@ -4417,7 +4418,7 @@ Proof. intros; red. exploit store_mapped_inj. eauto. eauto. apply flat_inj_no_overlap. unfold flat_inj. apply pred_dec_true; auto. eauto. - replace (ofs + 0) with ofs by omega. + replace (ofs + 0) with ofs by lia. intros [m'' [A B]]. congruence. Qed. @@ -4464,7 +4465,7 @@ Lemma valid_block_unchanged_on: forall m m' b, unchanged_on m m' -> valid_block m b -> valid_block m' b. Proof. - unfold valid_block; intros. apply unchanged_on_nextblock in H. xomega. + unfold valid_block; intros. apply unchanged_on_nextblock in H. extlia. Qed. Lemma perm_unchanged_on: @@ -4507,7 +4508,7 @@ Proof. + unfold loadbytes. destruct H. destruct (range_perm_dec m b ofs (ofs + n) Cur Readable). rewrite pred_dec_true. f_equal. - apply getN_exten. intros. rewrite Z2Nat.id in H by omega. + apply getN_exten. intros. rewrite Z2Nat.id in H by lia. apply unchanged_on_contents0; auto. red; intros. apply unchanged_on_perm0; auto. rewrite pred_dec_false. auto. @@ -4525,7 +4526,7 @@ Proof. destruct (zle n 0). + erewrite loadbytes_empty in * by assumption. auto. + rewrite <- H1. apply loadbytes_unchanged_on_1; auto. - exploit loadbytes_range_perm; eauto. instantiate (1 := ofs). omega. + exploit loadbytes_range_perm; eauto. instantiate (1 := ofs). lia. intros. eauto with mem. Qed. @@ -4568,7 +4569,7 @@ Proof. rewrite encode_val_length. rewrite <- size_chunk_conv. destruct (zlt ofs0 ofs); auto. destruct (zlt ofs0 (ofs + size_chunk chunk)); auto. - elim (H0 ofs0). omega. auto. + elim (H0 ofs0). lia. auto. Qed. Lemma storebytes_unchanged_on: @@ -4584,7 +4585,7 @@ Proof. destruct (peq b0 b); auto. subst b0. apply setN_outside. destruct (zlt ofs0 ofs); auto. destruct (zlt ofs0 (ofs + Z.of_nat (length bytes))); auto. - elim (H0 ofs0). omega. auto. + elim (H0 ofs0). lia. auto. Qed. Lemma alloc_unchanged_on: @@ -4613,7 +4614,7 @@ Proof. - split; intros. eapply perm_free_1; eauto. destruct (eq_block b0 b); auto. destruct (zlt ofs lo); auto. destruct (zle hi ofs); auto. - subst b0. elim (H0 ofs). omega. auto. + subst b0. elim (H0 ofs). lia. auto. eapply perm_free_3; eauto. - unfold free in H. destruct (range_perm_dec m b lo hi Cur Freeable); inv H. simpl. auto. @@ -4631,7 +4632,7 @@ Proof. destruct (eq_block b0 b); auto. subst b0. assert (~ (lo <= ofs < hi)). { red; intros; eelim H0; eauto. } - right; omega. + right; lia. eapply perm_drop_4; eauto. - unfold drop_perm in H. destruct (range_perm_dec m b lo hi Cur Freeable); inv H; simpl. auto. @@ -4658,7 +4659,7 @@ Notation mem := Mem.mem. Global Opaque Mem.alloc Mem.free Mem.store Mem.load Mem.storebytes Mem.loadbytes. -Hint Resolve +Global Hint Resolve Mem.valid_not_valid_diff Mem.perm_implies Mem.perm_cur diff --git a/common/Memtype.v b/common/Memtype.v index ca9c6f1f..b8ad1a6b 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -60,7 +61,7 @@ Inductive perm_order: permission -> permission -> Prop := | perm_W_R: perm_order Writable Readable | perm_any_N: forall p, perm_order p Nonempty. -Hint Constructors perm_order: mem. +Global Hint Constructors perm_order: mem. Lemma perm_order_trans: forall p1 p2 p3, perm_order p1 p2 -> perm_order p2 p3 -> perm_order p1 p3. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 38bbfa47..c33cb2dc 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/common/Sections.ml b/common/Sections.ml index ea0b6dbc..c256628e 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -6,22 +6,27 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) (* Handling of linker sections *) +type initialized = + | Uninit (* uninitialized data area *) + | Init (* initialized with fixed, non-relocatable data *) + | Init_reloc (* initialized with relocatable data (symbol addresses) *) + type section_name = | Section_text - | Section_data of bool (* true = init data, false = uninit data *) - * bool (* thread local? *) - | Section_small_data of bool - | Section_const of bool - | Section_small_const of bool + | Section_data of initialized * bool (* true = thread local ? *) + | Section_small_data of initialized + | Section_const of initialized + | Section_small_const of initialized | Section_string | Section_literal | Section_jumptable @@ -41,6 +46,7 @@ type access_mode = type section_info = { sec_name_init: section_name; + sec_name_init_reloc: section_name; sec_name_uninit: section_name; sec_writable: bool; sec_executable: bool; @@ -48,8 +54,9 @@ type section_info = { } let default_section_info = { - sec_name_init = Section_data (true, false); - sec_name_uninit = Section_data (false, false); + sec_name_init = Section_data (Init, false); + sec_name_init_reloc = Section_data (Init_reloc, false); + sec_name_uninit = Section_data (Uninit, false); sec_writable = true; sec_executable = false; sec_access = Access_default @@ -60,46 +67,55 @@ let default_section_info = { let builtin_sections = [ "CODE", {sec_name_init = Section_text; + sec_name_init_reloc = Section_text; sec_name_uninit = Section_text; sec_writable = false; sec_executable = true; sec_access = Access_default}; "DATA", - {sec_name_init = Section_data (true, false); - sec_name_uninit = Section_data (false, false); + {sec_name_init = Section_data (Init, false); + sec_name_init_reloc = Section_data (Init_reloc, false); + sec_name_uninit = Section_data (Uninit, false); sec_writable = true; sec_executable = false; sec_access = Access_default}; "TDATA", - {sec_name_init = Section_data (true, true); - sec_name_uninit = Section_data (false, true); + {sec_name_init = Section_data (Init, true); + sec_name_init_reloc = Section_data (Init_reloc, true); + sec_name_uninit = Section_data (Uninit, true); sec_writable = true; sec_executable = false; sec_access = Access_default}; "SDATA", - {sec_name_init = Section_small_data true; - sec_name_uninit = Section_small_data false; + {sec_name_init = Section_small_data Init; + sec_name_init_reloc = Section_small_data Init_reloc; + sec_name_uninit = Section_small_data Uninit; sec_writable = true; sec_executable = false; sec_access = Access_near}; "CONST", - {sec_name_init = Section_const true; - sec_name_uninit = Section_const false; + {sec_name_init = Section_const Init; + sec_name_init_reloc = Section_const Init_reloc; + sec_name_uninit = Section_const Uninit; sec_writable = false; sec_executable = false; sec_access = Access_default}; "SCONST", - {sec_name_init = Section_small_const true; - sec_name_uninit = Section_small_const false; + {sec_name_init = Section_small_const Init; + sec_name_init_reloc = Section_small_const Init_reloc; + sec_name_uninit = Section_small_const Uninit; sec_writable = false; sec_executable = false; sec_access = Access_near}; "STRING", {sec_name_init = Section_string; + sec_name_init_reloc = Section_string; sec_name_uninit = Section_string; sec_writable = false; sec_executable = false; sec_access = Access_default}; "LITERAL", {sec_name_init = Section_literal; + sec_name_init_reloc = Section_literal; sec_name_uninit = Section_literal; sec_writable = false; sec_executable = false; sec_access = Access_default}; "JUMPTABLE", {sec_name_init = Section_jumptable; + sec_name_init_reloc = Section_jumptable; sec_name_uninit = Section_jumptable; sec_writable = false; sec_executable = false; sec_access = Access_default} @@ -134,15 +150,19 @@ let define_section name ?iname ?uname ?writable ?executable ?access () = match executable with Some b -> b | None -> si.sec_executable and access = match access with Some b -> b | None -> si.sec_access in - let iname = + let i = match iname with Some s -> Section_user(s, writable, executable) | None -> si.sec_name_init in - let uname = + let ir = + match iname with Some s -> Section_user(s, writable, executable) + | None -> si.sec_name_init_reloc in + let u = match uname with Some s -> Section_user(s, writable, executable) | None -> si.sec_name_uninit in let new_si = - { sec_name_init = iname; - sec_name_uninit = uname; + { sec_name_init = i; + sec_name_init_reloc = ir; + sec_name_uninit = u; sec_writable = writable; sec_executable = executable; sec_access = access } in @@ -162,7 +182,7 @@ let use_section_for id name = let gcc_section name readonly exec = let sn = Section_user(name, not readonly, exec) in - { sec_name_init = sn; sec_name_uninit = sn; + { sec_name_init = sn; sec_name_init_reloc = sn; sec_name_uninit = sn; sec_writable = not readonly; sec_executable = exec; sec_access = Access_default } @@ -206,7 +226,12 @@ let for_variable env loc id ty init thrl = Hashtbl.find current_section_table name with Not_found -> assert false in - ((if init then si.sec_name_init else si.sec_name_uninit), si.sec_access) + let secname = + match init with + | Uninit -> si.sec_name_uninit + | Init -> si.sec_name_init + | Init_reloc -> si.sec_name_init_reloc in + (secname, si.sec_access) (* Determine sections for a function definition *) diff --git a/common/Sections.mli b/common/Sections.mli index 00c06c20..6d1d9c69 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -6,23 +6,28 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) (* Handling of linker sections *) +type initialized = + | Uninit (* uninitialized data area *) + | Init (* initialized with fixed, non-relocatable data *) + | Init_reloc (* initialized with relocatable data (symbol addresses) *) + type section_name = | Section_text - | Section_data of bool (* true = init data, false = uninit data *) - * bool (* thread local? *) - | Section_small_data of bool - | Section_const of bool - | Section_small_const of bool + | Section_data of initialized * bool (* true = thread local? *) + | Section_small_data of initialized + | Section_const of initialized + | Section_small_const of initialized | Section_string | Section_literal | Section_jumptable @@ -47,7 +52,7 @@ val define_section: -> ?writable:bool -> ?executable:bool -> ?access:access_mode -> unit -> unit val use_section_for: AST.ident -> string -> bool -val for_variable: Env.t -> C.location -> AST.ident -> C.typ -> bool -> bool -> +val for_variable: Env.t -> C.location -> AST.ident -> C.typ -> initialized -> bool -> section_name * access_mode val for_function: Env.t -> C.location -> AST.ident -> C.attributes -> section_name list val for_stringlit: unit -> section_name diff --git a/common/Separation.v b/common/Separation.v index 27065d1f..f41d94c3 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -113,7 +114,7 @@ Proof. intros P Q [[A B] [C D]]. split; auto. Qed. -Hint Resolve massert_imp_refl massert_eqv_refl : core. +Global Hint Resolve massert_imp_refl massert_eqv_refl : core. (** * Separating conjunction *) @@ -355,12 +356,12 @@ Proof. intros. rewrite <- sep_assoc. eapply sep_imp; eauto. split; simpl; intros. - intuition auto. -+ omega. -+ apply H5; omega. -+ omega. -+ apply H5; omega. -+ red; simpl; intros; omega. -- intuition omega. ++ lia. ++ apply H5; lia. ++ lia. ++ apply H5; lia. ++ red; simpl; intros; lia. +- intuition lia. Qed. Lemma range_drop_left: @@ -392,12 +393,12 @@ Proof. assert (mid <= align mid al) by (apply align_le; auto). split; simpl; intros. - intuition auto. -+ omega. -+ apply H7; omega. -+ omega. -+ apply H7; omega. -+ red; simpl; intros; omega. -- intuition omega. ++ lia. ++ apply H7; lia. ++ lia. ++ apply H7; lia. ++ red; simpl; intros; lia. +- intuition lia. Qed. Lemma range_preserved: @@ -493,7 +494,7 @@ Proof. split; [|split]. - assert (Mem.valid_access m chunk b ofs Freeable). { split; auto. red; auto. } - split. generalize (size_chunk_pos chunk). unfold Ptrofs.max_unsigned. omega. + split. generalize (size_chunk_pos chunk). unfold Ptrofs.max_unsigned. lia. split. auto. + destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD]. eauto with mem. @@ -616,7 +617,7 @@ Next Obligation. assert (IMG: forall b1 b2 delta ofs k p, j b1 = Some (b2, delta) -> Mem.perm m0 b1 ofs k p -> img b2 (ofs + delta)). { intros. red. exists b1, delta; split; auto. - replace (ofs + delta - delta) with ofs by omega. + replace (ofs + delta - delta) with ofs by lia. eauto with mem. } destruct H. constructor. - destruct mi_inj. constructor; intros. @@ -668,7 +669,7 @@ Proof. intros; red; intros. eelim C; eauto. simpl. exists b1, delta; split; auto. destruct VALID as [V1 V2]. apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. - apply V1. omega. + apply V1. lia. - red; simpl; intros. destruct H1 as (b0 & delta0 & U & V). eelim C; eauto. simpl. exists b0, delta0; eauto with mem. Qed. @@ -690,7 +691,7 @@ Lemma alloc_parallel_rule: /\ (forall b, b <> b1 -> j' b = j b). Proof. intros until delta; intros SEP ALLOC1 ALLOC2 ALIGN LO HI RANGE1 RANGE2 RANGE3. - assert (RANGE4: lo <= hi) by xomega. + assert (RANGE4: lo <= hi) by extlia. assert (FRESH1: ~Mem.valid_block m1 b1) by (eapply Mem.fresh_block_alloc; eauto). assert (FRESH2: ~Mem.valid_block m2 b2) by (eapply Mem.fresh_block_alloc; eauto). destruct SEP as (INJ & SP & DISJ). simpl in INJ. @@ -698,10 +699,10 @@ Proof. - eapply Mem.alloc_right_inject; eauto. - eexact ALLOC1. - instantiate (1 := b2). eauto with mem. -- instantiate (1 := delta). xomega. -- intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). omega. +- instantiate (1 := delta). extlia. +- intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). lia. - intros. apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. xomega. + eapply Mem.perm_alloc_2; eauto. extlia. - red; intros. apply Z.divide_trans with 8; auto. exists (8 / align_chunk chunk). destruct chunk; reflexivity. - intros. elim FRESH2. eapply Mem.valid_block_inject_2; eauto. @@ -709,19 +710,19 @@ Proof. exists j'; split; auto. rewrite <- ! sep_assoc. split; [|split]. -+ simpl. intuition auto; try (unfold Ptrofs.max_unsigned in *; omega). ++ simpl. intuition auto; try (unfold Ptrofs.max_unsigned in *; lia). * apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. omega. + eapply Mem.perm_alloc_2; eauto. lia. * apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. omega. -* red; simpl; intros. destruct H1, H2. omega. + eapply Mem.perm_alloc_2; eauto. lia. +* red; simpl; intros. destruct H1, H2. lia. * red; simpl; intros. assert (b = b2) by tauto. subst b. assert (0 <= ofs < lo \/ hi <= ofs < sz2) by tauto. clear H1. destruct H2 as (b0 & delta0 & D & E). eapply Mem.perm_alloc_inv in E; eauto. destruct (eq_block b0 b1). - subst b0. rewrite J2 in D. inversion D; clear D; subst delta0. xomega. + subst b0. rewrite J2 in D. inversion D; clear D; subst delta0. extlia. rewrite J3 in D by auto. elim FRESH2. eapply Mem.valid_block_inject_2; eauto. + apply (m_invar P) with m2; auto. eapply Mem.alloc_unchanged_on; eauto. + red; simpl; intros. @@ -753,11 +754,11 @@ Proof. simpl in E. assert (PERM: Mem.range_perm m2 b2 0 sz2 Cur Freeable). { red; intros. - destruct (zlt ofs lo). apply J; omega. - destruct (zle hi ofs). apply K; omega. - replace ofs with ((ofs - delta) + delta) by omega. + destruct (zlt ofs lo). apply J; lia. + destruct (zle hi ofs). apply K; lia. + replace ofs with ((ofs - delta) + delta) by lia. eapply Mem.perm_inject; eauto. - eapply Mem.free_range_perm; eauto. xomega. + eapply Mem.free_range_perm; eauto. extlia. } destruct (Mem.range_perm_free _ _ _ _ PERM) as [m2' FREE]. exists m2'; split; auto. split; [|split]. @@ -768,16 +769,16 @@ Proof. destruct (zle hi (ofs + delta0)). intuition auto. destruct (eq_block b0 b1). * subst b0. rewrite H1 in H; inversion H; clear H; subst delta0. - eelim (Mem.perm_free_2 m1); eauto. xomega. + eelim (Mem.perm_free_2 m1); eauto. extlia. * exploit Mem.mi_no_overlap; eauto. apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. eapply Mem.perm_free_3; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. eapply (Mem.free_range_perm m1); eauto. - instantiate (1 := ofs + delta0 - delta). xomega. - intros [X|X]. congruence. omega. + instantiate (1 := ofs + delta0 - delta). extlia. + intros [X|X]. congruence. lia. + simpl. exists b0, delta0; split; auto. - replace (ofs + delta0 - delta0) with ofs by omega. + replace (ofs + delta0 - delta0) with ofs by lia. apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. eapply Mem.perm_free_3; eauto. - apply (m_invar P) with m2; auto. @@ -787,7 +788,7 @@ Proof. destruct (zle hi i). intuition auto. right; exists b1, delta; split; auto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.free_range_perm; eauto. xomega. + eapply Mem.free_range_perm; eauto. extlia. - red; simpl; intros. eelim C; eauto. simpl. right. destruct H as (b0 & delta0 & U & V). exists b0, delta0; split; auto. @@ -870,7 +871,7 @@ Proof. exists j', vres2, m2'; intuition auto. split; [|split]. - exact INJ'. -- apply m_invar with (m0 := m2). +- apply (m_invar _ m2). + apply globalenv_inject_incr with j m1; auto. + eapply Mem.unchanged_on_implies; eauto. intros; red; intros; red; intros. diff --git a/common/Smallstep.v b/common/Smallstep.v index 27ad0a2d..f337ba3c 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -893,8 +894,8 @@ Proof. exploit (sd_traces DET). eexact H3. intros L2. assert (t1 = t0 /\ t2 = t3). destruct t1. inv MT. auto. - destruct t1; simpl in L1; try omegaContradiction. - destruct t0. inv MT. destruct t0; simpl in L2; try omegaContradiction. + destruct t1; simpl in L1; try extlia. + destruct t0. inv MT. destruct t0; simpl in L2; try extlia. simpl in H5. split. congruence. congruence. destruct H1; subst. assert (s2 = s4) by (eapply sd_determ_2; eauto). subst s4. @@ -974,7 +975,7 @@ Proof. destruct C as [P | [P Q]]; auto using lex_ord_left. + exploit sd_determ_3. eauto. eexact A. eauto. intros [P Q]; subst t s1'0. exists (i, n), s2; split; auto. - right; split. apply star_refl. apply lex_ord_right. omega. + right; split. apply star_refl. apply lex_ord_right. lia. - exact public_preserved. Qed. @@ -1256,7 +1257,7 @@ Proof. subst t. assert (EITHER: t1 = E0 \/ t2 = E0). unfold Eapp in H2; rewrite app_length in H2. - destruct t1; auto. destruct t2; auto. simpl in H2; omegaContradiction. + destruct t1; auto. destruct t2; auto. simpl in H2; extlia. destruct EITHER; subst. exploit IHstar; eauto. intros [s2x [s2y [A [B C]]]]. exists s2x; exists s2y; intuition. eapply star_left; eauto. @@ -1305,7 +1306,7 @@ Proof. - (* 1 L2 makes one or several transitions *) assert (EITHER: t = E0 \/ (length t = 1)%nat). { exploit L3_single_events; eauto. - destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction. } + destruct t; auto. destruct t; auto. simpl. intros. extlia. } destruct EITHER. + (* 1.1 these are silent transitions *) subst t. exploit (bsim_E0_plus S12); eauto. @@ -1473,7 +1474,7 @@ Remark not_silent_length: forall t1 t2, (length (t1 ** t2) <= 1)%nat -> t1 = E0 \/ t2 = E0. Proof. unfold Eapp, E0; intros. rewrite app_length in H. - destruct t1; destruct t2; auto. simpl in H. omegaContradiction. + destruct t1; destruct t2; auto. simpl in H. extlia. Qed. Lemma f2b_determinacy_inv: @@ -1622,7 +1623,7 @@ Proof. intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]]. + (* 2.1 L2 makes a silent transition: remain in "before" state *) subst. simpl in *. exists (F2BI_before n0); exists s1; split. - right; split. apply star_refl. constructor. omega. + right; split. apply star_refl. constructor. lia. econstructor; eauto. eapply star_right; eauto. + (* 2.2 L2 make a non-silent transition *) exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ]. @@ -1650,7 +1651,7 @@ Proof. exploit f2b_determinacy_inv. eexact H2. eexact STEP2. intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]]. subst. exists (F2BI_after n); exists s1; split. - right; split. apply star_refl. constructor; omega. + right; split. apply star_refl. constructor; lia. eapply f2b_match_after'; eauto. congruence. Qed. @@ -1763,7 +1764,7 @@ Proof. destruct IHstar as [s2x [A B]]. exists s2x; split; auto. eapply plus_left. eauto. apply plus_star; eauto. auto. destruct t1. simpl in *. subst t. exists s2; split; auto. apply plus_one; auto. - simpl in LEN. omegaContradiction. + simpl in LEN. extlia. Qed. Lemma ffs_simulation: @@ -1955,7 +1956,7 @@ Proof. assert (t2 = ev :: nil). inv H1; simpl in H0; tauto. subst t2. exists (t, s0). constructor; auto. simpl; auto. (* single-event *) - red. intros. inv H0; simpl; omega. + red. intros. inv H0; simpl; lia. Qed. (** * Connections with big-step semantics *) diff --git a/common/Subtyping.v b/common/Subtyping.v index 26b282e0..8e5d9361 100644 --- a/common/Subtyping.v +++ b/common/Subtyping.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -222,7 +223,7 @@ Definition weight_bounds (ob: option bounds) : nat := Lemma weight_bounds_1: forall lo hi s, weight_bounds (Some (B lo hi s)) < weight_bounds None. Proof. - intros; simpl. generalize (T.weight_range hi); omega. + intros; simpl. generalize (T.weight_range hi); lia. Qed. Lemma weight_bounds_2: @@ -233,8 +234,8 @@ Proof. intros; simpl. generalize (T.weight_sub _ _ s1) (T.weight_sub _ _ s2) (T.weight_sub _ _ H) (T.weight_sub _ _ H0); intros. destruct H1. - assert (T.weight lo2 < T.weight lo1) by (apply T.weight_sub_strict; auto). omega. - assert (T.weight hi1 < T.weight hi2) by (apply T.weight_sub_strict; auto). omega. + assert (T.weight lo2 < T.weight lo1) by (apply T.weight_sub_strict; auto). lia. + assert (T.weight hi1 < T.weight hi2) by (apply T.weight_sub_strict; auto). lia. Qed. Hint Resolve T.sub_refl: ty. @@ -250,11 +251,11 @@ Lemma weight_type_move: Proof. unfold type_move; intros. destruct (peq r1 r2). - inv H. split; auto. split; intros. omega. discriminate. + inv H. split; auto. split; intros. lia. discriminate. destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1; destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2. - destruct (T.sub_dec hi1 lo2). - inv H. split; auto. split; intros. omega. discriminate. + inv H. split; auto. split; intros. lia. discriminate. destruct (T.sub_dec lo1 hi2); try discriminate. set (lo2' := T.lub lo1 lo2) in *. set (hi1' := T.glb hi1 hi2) in *. @@ -264,45 +265,45 @@ Proof. set (b2 := B lo2' hi2 (T.lub_min lo1 lo2 hi2 s s2)) in *. Local Opaque weight_bounds. destruct (T.eq lo2 lo2'); destruct (T.eq hi1 hi1'); inversion H; clear H; subst changed e'; simpl. -+ split; auto. split; intros. omega. discriminate. ++ split; auto. split; intros. lia. discriminate. + assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1))) by (apply weight_bounds_2; auto with ty). split; auto. split; intros. - rewrite PTree.gsspec. destruct (peq r r1). subst r. rewrite E1. omega. omega. - rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega. + rewrite PTree.gsspec. destruct (peq r r1). subst r. rewrite E1. lia. lia. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. lia. + assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2))) by (apply weight_bounds_2; auto with ty). split; auto. split; intros. - rewrite PTree.gsspec. destruct (peq r r2). subst r. rewrite E2. omega. omega. - rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega. + rewrite PTree.gsspec. destruct (peq r r2). subst r. rewrite E2. lia. lia. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. lia. + assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1))) by (apply weight_bounds_2; auto with ty). assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2))) by (apply weight_bounds_2; auto with ty). split; auto. split; intros. rewrite ! PTree.gsspec. - destruct (peq r r2). subst r. rewrite E2. omega. - destruct (peq r r1). subst r. rewrite E1. omega. - omega. - rewrite PTree.gss. rewrite PTree.gso by auto. rewrite PTree.gss. omega. + destruct (peq r r2). subst r. rewrite E2. lia. + destruct (peq r r1). subst r. rewrite E1. lia. + lia. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite PTree.gss. lia. - set (b2 := B lo1 (T.high_bound lo1) (T.high_bound_sub lo1)) in *. assert (weight_bounds (Some b2) < weight_bounds None) by (apply weight_bounds_1). inv H; simpl. split. destruct (T.sub_dec hi1 lo1); auto. split; intros. - rewrite PTree.gsspec. destruct (peq r r2). subst r; rewrite E2; omega. omega. - rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega. + rewrite PTree.gsspec. destruct (peq r r2). subst r; rewrite E2; lia. lia. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. lia. - set (b1 := B (T.low_bound hi2) hi2 (T.low_bound_sub hi2)) in *. assert (weight_bounds (Some b1) < weight_bounds None) by (apply weight_bounds_1). inv H; simpl. split. destruct (T.sub_dec hi2 lo2); auto. split; intros. - rewrite PTree.gsspec. destruct (peq r r1). subst r; rewrite E1; omega. omega. - rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega. + rewrite PTree.gsspec. destruct (peq r r1). subst r; rewrite E1; lia. lia. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. lia. -- inv H. split; auto. simpl; split; intros. omega. congruence. +- inv H. split; auto. simpl; split; intros. lia. congruence. Qed. Definition weight_constraints (b: PTree.t bounds) (cstr: list constraint) : nat := @@ -312,7 +313,7 @@ Remark weight_constraints_tighter: forall b1 b2, (forall r, weight_bounds b1!r <= weight_bounds b2!r) -> forall q, weight_constraints b1 q <= weight_constraints b2 q. Proof. - induction q; simpl. omega. generalize (H (fst a)) (H (snd a)); omega. + induction q; simpl. lia. generalize (H (fst a)) (H (snd a)); lia. Qed. Lemma weight_solve_rec: @@ -323,8 +324,8 @@ Lemma weight_solve_rec: <= weight_constraints e.(te_typ) e.(te_sub) + weight_constraints e.(te_typ) q. Proof. induction q; simpl; intros. -- inv H. split. intros; omega. replace (changed' && negb changed') with false. - omega. destruct changed'; auto. +- inv H. split. intros; lia. replace (changed' && negb changed') with false. + lia. destruct changed'; auto. - destruct a as [r1 r2]; monadInv H; simpl. rename x into changed1. rename x0 into e1. exploit weight_type_move; eauto. intros [A [B C]]. @@ -336,7 +337,7 @@ Proof. assert (Q: weight_constraints (te_typ e1) (te_sub e1) <= weight_constraints (te_typ e1) (te_sub e) + weight_bounds (te_typ e1)!r1 + weight_bounds (te_typ e1)!r2). - { destruct A as [Q|Q]; rewrite Q. omega. simpl. omega. } + { destruct A as [Q|Q]; rewrite Q. lia. simpl. lia. } assert (R: weight_constraints (te_typ e1) q <= weight_constraints (te_typ e) q) by (apply weight_constraints_tighter; auto). set (ch1 := if changed' && negb (changed || changed1) then 1 else 0) in *. @@ -344,11 +345,11 @@ Proof. destruct changed1. assert (ch2 <= ch1 + 1). { unfold ch2, ch1. rewrite orb_true_r. simpl. rewrite andb_false_r. - destruct (changed' && negb changed); omega. } - exploit C; eauto. omega. + destruct (changed' && negb changed); lia. } + exploit C; eauto. lia. assert (ch2 <= ch1). - { unfold ch2, ch1. rewrite orb_false_r. omega. } - generalize (B r1) (B r2); omega. + { unfold ch2, ch1. rewrite orb_false_r. lia. } + generalize (B r1) (B r2); lia. Qed. Definition weight_typenv (e: typenv) : nat := @@ -364,7 +365,7 @@ Function solve_constraints (e: typenv) {measure weight_typenv e}: res typenv := end. Proof. intros. exploit weight_solve_rec; eauto. simpl. intros [A B]. - unfold weight_typenv. omega. + unfold weight_typenv. lia. Qed. Definition typassign := positive -> T.t. diff --git a/common/Switch.v b/common/Switch.v index 5a6d4c63..b9aeed96 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -235,8 +236,8 @@ Proof. destruct (split_lt n cases) as [lc rc] eqn:SEQ. rewrite (IHcases lc rc) by auto. destruct (zlt key n); intros EQ; inv EQ; simpl. -+ destruct (zeq v key). rewrite zlt_true by omega. auto. auto. -+ destruct (zeq v key). rewrite zlt_false by omega. auto. auto. ++ destruct (zeq v key). rewrite zlt_true by lia. auto. auto. ++ destruct (zeq v key). rewrite zlt_false by lia. auto. auto. Qed. Lemma split_between_prop: @@ -269,12 +270,12 @@ Lemma validate_jumptable_correct_rec: list_nth_z tbl v = Some(ZMap.get (base + v) cases). Proof. induction tbl; simpl; intros. -- unfold list_length_z in H0. simpl in H0. omegaContradiction. +- unfold list_length_z in H0. simpl in H0. extlia. - InvBooleans. rewrite list_length_z_cons in H0. apply beq_nat_true in H1. destruct (zeq v 0). - + replace (base + v) with base by omega. congruence. - + replace (base + v) with (Z.succ base + Z.pred v) by omega. - apply IHtbl. auto. omega. + + replace (base + v) with base by lia. congruence. + + replace (base + v) with (Z.succ base + Z.pred v) by lia. + apply IHtbl. auto. lia. Qed. Lemma validate_jumptable_correct: @@ -288,12 +289,12 @@ Lemma validate_jumptable_correct: Proof. intros. rewrite (validate_jumptable_correct_rec cases tbl ofs); auto. -- f_equal. f_equal. rewrite Z.mod_small. omega. - destruct (zle ofs v). omega. +- f_equal. f_equal. rewrite Z.mod_small. lia. + destruct (zle ofs v). lia. assert (M: ((v - ofs) + 1 * modulus) mod modulus = (v - ofs) + modulus). - { rewrite Z.mod_small. omega. omega. } - rewrite Z_mod_plus in M by auto. rewrite M in H0. omega. -- generalize (Z_mod_lt (v - ofs) modulus modulus_pos). omega. + { rewrite Z.mod_small. lia. lia. } + rewrite Z_mod_plus in M by auto. rewrite M in H0. lia. +- generalize (Z_mod_lt (v - ofs) modulus modulus_pos). lia. Qed. Lemma validate_correct_rec: @@ -309,7 +310,7 @@ Proof. destruct cases as [ | [key1 act1] cases1]; intros. + apply beq_nat_true in H. subst act. reflexivity. + InvBooleans. apply beq_nat_true in H2. subst. simpl. - destruct (zeq v hi). auto. omegaContradiction. + destruct (zeq v hi). auto. extlia. - (* eq node *) destruct (split_eq key cases) as [optact others] eqn:EQ. intros. destruct optact as [act1|]; InvBooleans; try discriminate. @@ -319,19 +320,19 @@ Proof. + congruence. + eapply IHt; eauto. unfold refine_low_bound, refine_high_bound. split. - destruct (zeq key lo); omega. - destruct (zeq key hi); omega. + destruct (zeq key lo); lia. + destruct (zeq key hi); lia. - (* lt node *) destruct (split_lt key cases) as [lcases rcases] eqn:EQ; intros; InvBooleans. rewrite (split_lt_prop v default _ _ _ _ EQ). destruct (zlt v key). - eapply IHt1. eauto. omega. - eapply IHt2. eauto. omega. + eapply IHt1. eauto. lia. + eapply IHt2. eauto. lia. - (* jumptable node *) destruct (split_between default ofs sz cases) as [ins outs] eqn:EQ; intros; InvBooleans. rewrite (split_between_prop v _ _ _ _ _ _ EQ). - assert (0 <= (v - ofs) mod modulus < modulus) by (apply Z_mod_lt; omega). + assert (0 <= (v - ofs) mod modulus < modulus) by (apply Z_mod_lt; lia). destruct (zlt ((v - ofs) mod modulus) sz). - rewrite Z.mod_small by omega. eapply validate_jumptable_correct; eauto. + rewrite Z.mod_small by lia. eapply validate_jumptable_correct; eauto. eapply IHt; eauto. Qed. @@ -346,7 +347,7 @@ Theorem validate_switch_correct: Proof. unfold validate_switch, table_tree_agree; split. eapply validate_wf; eauto. - intros; eapply validate_correct_rec; eauto. omega. + intros; eapply validate_correct_rec; eauto. lia. Qed. End COMPTREE. diff --git a/common/Switchaux.ml b/common/Switchaux.ml index 1744a932..eb1ab8bc 100644 --- a/common/Switchaux.ml +++ b/common/Switchaux.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/common/Unityping.v b/common/Unityping.v index 28bcfb5c..1089b359 100644 --- a/common/Unityping.v +++ b/common/Unityping.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -126,12 +127,12 @@ Lemma length_move: length e'.(te_equ) + (if changed then 1 else 0) <= S(length e.(te_equ)). Proof. unfold move; intros. - destruct (peq r1 r2). inv H. omega. + destruct (peq r1 r2). inv H. lia. destruct e.(te_typ)!r1 as [ty1|]; destruct e.(te_typ)!r2 as [ty2|]; inv H; simpl. - destruct (T.eq ty1 ty2); inv H1. omega. - omega. - omega. - omega. + destruct (T.eq ty1 ty2); inv H1. lia. + lia. + lia. + lia. Qed. Lemma length_solve_rec: @@ -140,14 +141,14 @@ Lemma length_solve_rec: length e'.(te_equ) + (if ch' && negb ch then 1 else 0) <= length e.(te_equ) + length q. Proof. induction q; simpl; intros. -- inv H. replace (ch' && negb ch') with false. omega. destruct ch'; auto. +- inv H. replace (ch' && negb ch') with false. lia. destruct ch'; auto. - destruct a as [r1 r2]; monadInv H. rename x0 into e0. rename x into ch0. exploit IHq; eauto. intros A. exploit length_move; eauto. intros B. set (X := (if ch' && negb (ch || ch0) then 1 else 0)) in *. set (Y := (if ch0 then 1 else 0)) in *. set (Z := (if ch' && negb ch then 1 else 0)) in *. - cut (Z <= X + Y). intros. omega. + cut (Z <= X + Y). intros. lia. unfold X, Y, Z. destruct ch'; destruct ch; destruct ch0; simpl; auto. Qed. @@ -164,7 +165,7 @@ Function solve_constraints (e: typenv) {measure weight_typenv e}: res typenv := end. Proof. intros. exploit length_solve_rec; eauto. simpl. intros. - unfold weight_typenv. omega. + unfold weight_typenv. lia. Qed. Definition typassign := positive -> T.t. @@ -199,7 +200,7 @@ Proof. apply A. rewrite PTree.gso by congruence. auto. Qed. -Hint Resolve set_incr: ty. +Global Hint Resolve set_incr: ty. Lemma set_sound: forall te x ty e e', set e x ty = OK e' -> satisf te e' -> te x = ty. @@ -216,7 +217,7 @@ Proof. induction xl; destruct tyl; simpl; intros; monadInv H; eauto with ty. Qed. -Hint Resolve set_list_incr: ty. +Global Hint Resolve set_list_incr: ty. Lemma set_list_sound: forall te xl tyl e e', set_list e xl tyl = OK e' -> satisf te e' -> map te xl = tyl. @@ -242,7 +243,7 @@ Proof. - inv H; simpl in *; split; auto. Qed. -Hint Resolve move_incr: ty. +Global Hint Resolve move_incr: ty. Lemma move_sound: forall te e r1 r2 e' changed, diff --git a/common/Values.v b/common/Values.v index 5d32e54e..9353366d 100644 --- a/common/Values.v +++ b/common/Values.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -20,6 +21,7 @@ Require Import Coqlib. Require Import AST. Require Import Integers. Require Import Floats. +Require Import Lia. Definition block : Type := positive. Definition eq_block := peq. @@ -1045,10 +1047,10 @@ Lemma load_result_rettype: forall chunk v, has_rettype (load_result chunk v) (rettype_of_chunk chunk). Proof. intros. unfold has_rettype; destruct chunk; destruct v; simpl; auto. -- rewrite Int.sign_ext_idem by omega; auto. -- rewrite Int.zero_ext_idem by omega; auto. -- rewrite Int.sign_ext_idem by omega; auto. -- rewrite Int.zero_ext_idem by omega; auto. +- rewrite Int.sign_ext_idem by lia; auto. +- rewrite Int.zero_ext_idem by lia; auto. +- rewrite Int.sign_ext_idem by lia; auto. +- rewrite Int.zero_ext_idem by lia; auto. - destruct Archi.ptr64 eqn:SF; simpl; auto. - destruct Archi.ptr64 eqn:SF; simpl; auto. - destruct Archi.ptr64 eqn:SF; simpl; auto. @@ -1074,14 +1076,14 @@ Theorem cast8unsigned_and: forall x, zero_ext 8 x = and x (Vint(Int.repr 255)). Proof. destruct x; simpl; auto. decEq. - change 255 with (two_p 8 - 1). apply Int.zero_ext_and. omega. + change 255 with (two_p 8 - 1). apply Int.zero_ext_and. lia. Qed. Theorem cast16unsigned_and: forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)). Proof. destruct x; simpl; auto. decEq. - change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. omega. + change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. lia. Qed. Theorem bool_of_val_of_bool: @@ -1318,7 +1320,7 @@ Proof. unfold divs. rewrite Int.eq_false; try discriminate. simpl. rewrite (Int.eq_false Int.one Int.mone); try discriminate. rewrite andb_false_intro2; auto. f_equal. f_equal. - rewrite Int.divs_one; auto. replace Int.zwordsize with 32; auto. omega. + rewrite Int.divs_one; auto. replace Int.zwordsize with 32; auto. lia. Qed. Theorem divu_pow2: @@ -1445,7 +1447,7 @@ Proof. destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1. exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros. assert (Int.ltu i0 Int.iwordsize = true). - unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. + unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. lia. simpl. rewrite H0. simpl. decEq. rewrite Int.shrx_carry; auto. Qed. @@ -1460,7 +1462,7 @@ Proof. destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1. exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros. assert (Int.ltu i0 Int.iwordsize = true). - unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. + unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. lia. exists i; exists i0; intuition. rewrite Int.shrx_shr; auto. destruct (Int.lt i Int.zero); simpl; rewrite H0; auto. Qed. @@ -1483,12 +1485,12 @@ Proof. replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl. replace (Int.ltu n Int.iwordsize) with true. f_equal; apply Int.shrx_shr_2; assumption. - symmetry; apply zlt_true. change (Int.unsigned n < 32); omega. + symmetry; apply zlt_true. change (Int.unsigned n < 32); lia. symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32. assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } rewrite Int.unsigned_repr. - change (Int.unsigned Int.iwordsize) with 32; omega. - assert (32 < Int.max_unsigned) by reflexivity. omega. + change (Int.unsigned Int.iwordsize) with 32; lia. + assert (32 < Int.max_unsigned) by reflexivity. lia. Qed. Theorem shrx1_shr: @@ -1535,14 +1537,14 @@ Proof. replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl. replace (Int.ltu n Int.iwordsize) with true. f_equal; apply Int.shrx_shr_2; assumption. - symmetry; apply zlt_true. change (Int.unsigned n < 32); omega. + symmetry; apply zlt_true. change (Int.unsigned n < 32); lia. symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32. assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } rewrite Int.unsigned_repr. - change (Int.unsigned Int.iwordsize) with 32; omega. - assert (32 < Int.max_unsigned) by reflexivity. omega. + change (Int.unsigned Int.iwordsize) with 32; lia. + assert (32 < Int.max_unsigned) by reflexivity. lia. Qed. Theorem or_rolm: @@ -1732,7 +1734,7 @@ Proof. rewrite (Int64.eq_false Int64.one Int64.mone); try discriminate. rewrite andb_false_intro2; auto. simpl. f_equal. f_equal. apply Int64.divs_one. - replace Int64.zwordsize with 64; auto. omega. + replace Int64.zwordsize with 64; auto. lia. Qed. Theorem divlu_pow2: @@ -1775,7 +1777,7 @@ Proof. destruct (Int.ltu i0 (Int.repr 63)) eqn:?; inv H1. exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 63)) with 63. intros. assert (Int.ltu i0 Int64.iwordsize' = true). - unfold Int.ltu. apply zlt_true. change (Int.unsigned Int64.iwordsize') with 64. omega. + unfold Int.ltu. apply zlt_true. change (Int.unsigned Int64.iwordsize') with 64. lia. simpl. rewrite H0. simpl. decEq. rewrite Int64.shrx'_carry; auto. Qed. @@ -1796,12 +1798,12 @@ Proof. replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl. replace (Int.ltu n Int64.iwordsize') with true. f_equal; apply Int64.shrx'_shr_2; assumption. - symmetry; apply zlt_true. change (Int.unsigned n < 64); omega. + symmetry; apply zlt_true. change (Int.unsigned n < 64); lia. symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64. assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } rewrite Int.unsigned_repr. - change (Int.unsigned Int64.iwordsize') with 64; omega. - assert (64 < Int.max_unsigned) by reflexivity. omega. + change (Int.unsigned Int64.iwordsize') with 64; lia. + assert (64 < Int.max_unsigned) by reflexivity. lia. Qed. Theorem shrxl1_shrl: @@ -1848,12 +1850,12 @@ simpl. change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl. replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl. replace (Int.ltu n Int64.iwordsize') with true. f_equal; apply Int64.shrx'_shr_2; assumption. - symmetry; apply zlt_true. change (Int.unsigned n < 64); omega. + symmetry; apply zlt_true. change (Int.unsigned n < 64); lia. symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64. assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } rewrite Int.unsigned_repr. - change (Int.unsigned Int64.iwordsize') with 64; omega. - assert (64 < Int.max_unsigned) by reflexivity. omega. + change (Int.unsigned Int64.iwordsize') with 64; lia. + assert (64 < Int.max_unsigned) by reflexivity. lia. Qed. Theorem negate_cmp_bool: @@ -2127,7 +2129,7 @@ Inductive lessdef_list: list val -> list val -> Prop := lessdef v1 v2 -> lessdef_list vl1 vl2 -> lessdef_list (v1 :: vl1) (v2 :: vl2). -Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons : core. +Global Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons : core. Lemma lessdef_list_inv: forall vl1 vl2, lessdef_list vl1 vl2 -> vl1 = vl2 \/ In Vundef vl1. @@ -2352,7 +2354,7 @@ Inductive inject (mi: meminj): val -> val -> Prop := | val_inject_undef: forall v, inject mi Vundef v. -Hint Constructors inject : core. +Global Hint Constructors inject : core. Inductive inject_list (mi: meminj): list val -> list val-> Prop:= | inject_list_nil : @@ -2361,7 +2363,7 @@ Inductive inject_list (mi: meminj): list val -> list val-> Prop:= inject mi v v' -> inject_list mi vl vl'-> inject_list mi (v :: vl) (v' :: vl'). -Hint Resolve inject_list_nil inject_list_cons : core. +Global Hint Resolve inject_list_nil inject_list_cons : core. Lemma inject_ptrofs: forall mi i, inject mi (Vptrofs i) (Vptrofs i). @@ -2369,7 +2371,7 @@ Proof. unfold Vptrofs; intros. destruct Archi.ptr64; auto. Qed. -Hint Resolve inject_ptrofs : core. +Global Hint Resolve inject_ptrofs : core. Section VAL_INJ_OPS. @@ -2721,7 +2723,7 @@ Proof. constructor. eapply val_inject_incr; eauto. auto. Qed. -Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr : core. +Global Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr : core. Lemma val_inject_lessdef: forall v1 v2, Val.lessdef v1 v2 <-> Val.inject (fun b => Some(b, 0)) v1 v2. |