From 9ab3738ae87a554fb742420b8c81ced4cd3c66c7 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 8 Sep 2020 13:56:01 +0200 Subject: Changed cc_varargs to an option type Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs. --- backend/Asmexpandaux.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend') diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml index 0530abe4..f7feb303 100644 --- a/backend/Asmexpandaux.ml +++ b/backend/Asmexpandaux.ml @@ -54,7 +54,7 @@ let get_current_function_args () = (!current_function).fn_sig.sig_args let is_current_function_variadic () = - (!current_function).fn_sig.sig_cc.cc_vararg + (!current_function).fn_sig.sig_cc.cc_vararg <> None let get_current_function_sig () = (!current_function).fn_sig -- cgit From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 18:22:00 +0200 Subject: Replace `omega` tactic with `lia` Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. --- backend/Allocproof.v | 6 +- backend/Asmgenproof0.v | 32 ++--- backend/Bounds.v | 8 +- backend/CSEproof.v | 58 ++++----- backend/CleanupLabelsproof.v | 2 +- backend/Cminor.v | 4 +- backend/CminorSel.v | 8 +- backend/Constpropproof.v | 4 +- backend/Conventions.v | 14 +-- backend/Deadcodeproof.v | 20 +-- backend/Inlining.v | 14 +-- backend/Inliningproof.v | 174 +++++++++++++------------- backend/Inliningspec.v | 110 ++++++++-------- backend/Linearizeproof.v | 8 +- backend/Locations.v | 20 +-- backend/NeedDomain.v | 90 ++++++------- backend/RTL.v | 42 +++---- backend/RTLgenproof.v | 2 +- backend/SelectDivproof.v | 186 +++++++++++++-------------- backend/Selectionproof.v | 18 +-- backend/SplitLongproof.v | 30 ++--- backend/Stackingproof.v | 26 ++-- backend/Tailcallproof.v | 52 ++++---- backend/Tunnelingproof.v | 8 +- backend/Unusedglobproof.v | 22 ++-- backend/ValueAnalysis.v | 22 ++-- backend/ValueDomain.v | 292 +++++++++++++++++++++---------------------- 27 files changed, 636 insertions(+), 636 deletions(-) (limited to 'backend') diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 51755912..3fdbacbe 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -548,7 +548,7 @@ Proof. unfold select_reg_l; intros. destruct H. red in H. congruence. rewrite Pos.leb_le in *. red in H. destruct H as [A | [A B]]. - red in A. zify; omega. + red in A. zify; lia. rewrite <- A; auto. Qed. @@ -560,7 +560,7 @@ Proof. unfold select_reg_h; intros. destruct H. red in H. congruence. rewrite Pos.leb_le in *. red in H. destruct H as [A | [A B]]. - red in A. zify; omega. + red in A. zify; lia. rewrite A; auto. Qed. @@ -568,7 +568,7 @@ Remark select_reg_charact: forall r q, select_reg_l r q = true /\ select_reg_h r q = true <-> ereg q = r. Proof. unfold select_reg_l, select_reg_h; intros; split. - rewrite ! Pos.leb_le. unfold reg; zify; omega. + rewrite ! Pos.leb_le. unfold reg; zify; lia. intros. rewrite H. rewrite ! Pos.leb_refl; auto. Qed. diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 3638c465..5e8acd6f 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -473,7 +473,7 @@ Inductive code_tail: Z -> code -> code -> Prop := Lemma code_tail_pos: forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0. Proof. - induction 1. omega. omega. + induction 1. lia. lia. Qed. Lemma find_instr_tail: @@ -484,8 +484,8 @@ Proof. induction c1; simpl; intros. inv H. destruct (zeq pos 0). subst pos. - inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. omegaContradiction. - inv H. congruence. replace (pos0 + 1 - 1) with pos0 by omega. + inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. extlia. + inv H. congruence. replace (pos0 + 1 - 1) with pos0 by lia. eauto. Qed. @@ -494,8 +494,8 @@ Remark code_tail_bounds_1: code_tail ofs fn c -> 0 <= ofs <= list_length_z fn. Proof. induction 1; intros; simpl. - generalize (list_length_z_pos c). omega. - rewrite list_length_z_cons. omega. + generalize (list_length_z_pos c). lia. + rewrite list_length_z_cons. lia. Qed. Remark code_tail_bounds_2: @@ -505,8 +505,8 @@ Proof. assert (forall ofs fn c, code_tail ofs fn c -> forall i c', c = i :: c' -> 0 <= ofs < list_length_z fn). induction 1; intros; simpl. - rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). omega. - rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). omega. + rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). lia. + rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). lia. eauto. Qed. @@ -531,7 +531,7 @@ Lemma code_tail_next_int: Proof. intros. rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_one. rewrite Ptrofs.unsigned_repr. apply code_tail_next with i; auto. - generalize (code_tail_bounds_2 _ _ _ _ H0). omega. + generalize (code_tail_bounds_2 _ _ _ _ H0). lia. Qed. (** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points @@ -654,7 +654,7 @@ Opaque transl_instr. exists (Ptrofs.repr ofs). red; intros. rewrite Ptrofs.unsigned_repr. congruence. exploit code_tail_bounds_1; eauto. - apply transf_function_len in TF. omega. + apply transf_function_len in TF. lia. + exists Ptrofs.zero; red; intros. congruence. Qed. @@ -663,7 +663,7 @@ End RETADDR_EXISTS. Remark code_tail_no_bigger: forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat. Proof. - induction 1; simpl; omega. + induction 1; simpl; lia. Qed. Remark code_tail_unique: @@ -671,8 +671,8 @@ Remark code_tail_unique: code_tail pos fn c -> code_tail pos' fn c -> pos = pos'. Proof. induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. + generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia. + generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia. f_equal. eauto. Qed. @@ -713,13 +713,13 @@ Proof. case (is_label lbl a). intro EQ; injection EQ; intro; subst c'. exists (pos + 1). split. auto. split. - replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. - rewrite list_length_z_cons. generalize (list_length_z_pos c). omega. + replace (pos + 1 - pos) with (0 + 1) by lia. constructor. constructor. + rewrite list_length_z_cons. generalize (list_length_z_pos c). lia. intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]]. exists pos'. split. auto. split. - replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega. + replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by lia. constructor. auto. - rewrite list_length_z_cons. omega. + rewrite list_length_z_cons. lia. Qed. (** Helper lemmas to reason about diff --git a/backend/Bounds.v b/backend/Bounds.v index fa695234..4231d861 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -163,7 +163,7 @@ Proof. intros until valu. unfold max_over_list. assert (forall l z, fold_left (fun x y => Z.max x (valu y)) l z >= z). induction l; simpl; intros. - omega. apply Zge_trans with (Z.max z (valu a)). + lia. apply Zge_trans with (Z.max z (valu a)). auto. apply Z.le_ge. apply Z.le_max_l. auto. Qed. @@ -307,7 +307,7 @@ Proof. let f := fold_left (fun x y => Z.max x (valu y)) c z in z <= f /\ (In x c -> valu x <= f)). induction c; simpl; intros. - split. omega. tauto. + split. lia. tauto. elim (IHc (Z.max z (valu a))); intros. split. apply Z.le_trans with (Z.max z (valu a)). apply Z.le_max_l. auto. intro H1; elim H1; intro. @@ -446,12 +446,12 @@ Lemma size_callee_save_area_rec_incr: Proof. Local Opaque mreg_type. induction l as [ | r l]; intros; simpl. -- omega. +- lia. - eapply Z.le_trans. 2: apply IHl. generalize (AST.typesize_pos (mreg_type r)); intros. apply Z.le_trans with (align ofs (AST.typesize (mreg_type r))). apply align_le; auto. - omega. + lia. Qed. Lemma size_callee_save_area_incr: diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 03c7ecfc..a2a1b461 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -128,9 +128,9 @@ Proof. exists valu2; splitall. + constructor; simpl; intros. * constructor; simpl; intros. - apply wf_equation_incr with (num_next n). eauto with cse. xomega. + apply wf_equation_incr with (num_next n). eauto with cse. extlia. rewrite PTree.gsspec in H0. destruct (peq r0 r). - inv H0; xomega. + inv H0; extlia. apply Plt_trans_succ; eauto with cse. rewrite PMap.gsspec in H0. destruct (peq v (num_next n)). replace r0 with r by (simpl in H0; intuition). rewrite PTree.gss. subst; auto. @@ -142,8 +142,8 @@ Proof. rewrite peq_false. eauto with cse. apply Plt_ne; eauto with cse. + unfold valu2. rewrite peq_true; auto. + auto. -+ xomega. -+ xomega. ++ extlia. ++ extlia. Qed. Lemma valnum_regs_holds: @@ -158,7 +158,7 @@ Lemma valnum_regs_holds: /\ Ple n.(num_next) n'.(num_next). Proof. induction rl; simpl; intros. -- inv H0. exists valu1; splitall; auto. red; auto. simpl; tauto. xomega. +- inv H0. exists valu1; splitall; auto. red; auto. simpl; tauto. extlia. - destruct (valnum_reg n a) as [n1 v1] eqn:V1. destruct (valnum_regs n1 rl) as [n2 vs] eqn:V2. inv H0. @@ -169,9 +169,9 @@ Proof. exists valu3; splitall. + auto. + simpl; f_equal; auto. rewrite R; auto. - + red; intros. transitivity (valu2 v); auto. apply R. xomega. - + simpl; intros. destruct H0; auto. subst v1; xomega. - + xomega. + + red; intros. transitivity (valu2 v); auto. apply R. extlia. + + simpl; intros. destruct H0; auto. subst v1; extlia. + + extlia. Qed. Lemma find_valnum_rhs_charact: @@ -327,11 +327,11 @@ Proof. { red; intros. unfold valu2. apply peq_false. apply Plt_ne; auto. } exists valu2; constructor; simpl; intros. + constructor; simpl; intros. - * destruct H3. inv H3. simpl; split. xomega. + * destruct H3. inv H3. simpl; split. extlia. red; intros. apply Plt_trans_succ; eauto. - apply wf_equation_incr with (num_next n). eauto with cse. xomega. + apply wf_equation_incr with (num_next n). eauto with cse. extlia. * rewrite PTree.gsspec in H3. destruct (peq r rd). - inv H3. xomega. + inv H3. extlia. apply Plt_trans_succ; eauto with cse. * apply update_reg_charact; eauto with cse. + destruct H3. inv H3. @@ -495,10 +495,10 @@ Lemma store_normalized_range_sound: Proof. intros. unfold Val.load_result; remember Archi.ptr64 as ptr64. destruct chunk; simpl in *; destruct v; auto. -- inv H. rewrite is_sgn_sign_ext in H4 by omega. rewrite H4; auto. -- inv H. rewrite is_uns_zero_ext in H4 by omega. rewrite H4; auto. -- inv H. rewrite is_sgn_sign_ext in H4 by omega. rewrite H4; auto. -- inv H. rewrite is_uns_zero_ext in H4 by omega. rewrite H4; auto. +- inv H. rewrite is_sgn_sign_ext in H4 by lia. rewrite H4; auto. +- inv H. rewrite is_uns_zero_ext in H4 by lia. rewrite H4; auto. +- inv H. rewrite is_sgn_sign_ext in H4 by lia. rewrite H4; auto. +- inv H. rewrite is_uns_zero_ext in H4 by lia. rewrite H4; auto. - destruct ptr64; auto. - destruct ptr64; auto. - destruct ptr64; auto. @@ -557,7 +557,7 @@ Proof. simpl. rewrite negb_false_iff in H8. eapply Mem.load_storebytes_other. eauto. - rewrite H6. rewrite Z2Nat.id by omega. + rewrite H6. rewrite Z2Nat.id by lia. eapply pdisjoint_sound. eauto. unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. erewrite <- regs_valnums_sound by eauto. eauto with va. @@ -578,39 +578,39 @@ Proof. set (n1 := i - ofs1). set (n2 := size_chunk chunk). set (n3 := sz - (n1 + n2)). - replace sz with (n1 + (n2 + n3)) in H by (unfold n3, n2, n1; omega). + replace sz with (n1 + (n2 + n3)) in H by (unfold n3, n2, n1; lia). exploit Mem.loadbytes_split; eauto. - unfold n1; omega. - unfold n3, n2, n1; omega. + unfold n1; lia. + unfold n3, n2, n1; lia. intros (bytes1 & bytes23 & LB1 & LB23 & EQ). clear H. exploit Mem.loadbytes_split; eauto. - unfold n2; omega. - unfold n3, n2, n1; omega. + unfold n2; lia. + unfold n3, n2, n1; lia. intros (bytes2 & bytes3 & LB2 & LB3 & EQ'). subst bytes23; subst bytes. exploit Mem.load_loadbytes; eauto. intros (bytes2' & A & B). assert (bytes2' = bytes2). - { replace (ofs1 + n1) with i in LB2 by (unfold n1; omega). unfold n2 in LB2. congruence. } + { replace (ofs1 + n1) with i in LB2 by (unfold n1; lia). unfold n2 in LB2. congruence. } subst bytes2'. exploit Mem.storebytes_split; eauto. intros (m1 & SB1 & SB23). clear H0. exploit Mem.storebytes_split; eauto. intros (m2 & SB2 & SB3). clear SB23. assert (L1: Z.of_nat (length bytes1) = n1). - { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n1; omega. } + { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n1; lia. } assert (L2: Z.of_nat (length bytes2) = n2). - { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n2; omega. } + { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n2; lia. } rewrite L1 in *. rewrite L2 in *. assert (LB': Mem.loadbytes m2 b2 (ofs2 + n1) n2 = Some bytes2). { rewrite <- L2. eapply Mem.loadbytes_storebytes_same; eauto. } assert (LB'': Mem.loadbytes m' b2 (ofs2 + n1) n2 = Some bytes2). { rewrite <- LB'. eapply Mem.loadbytes_storebytes_other; eauto. - unfold n2; omega. - right; left; omega. } + unfold n2; lia. + right; left; lia. } exploit Mem.load_valid_access; eauto. intros [P Q]. rewrite B. apply Mem.loadbytes_load. - replace (i + (ofs2 - ofs1)) with (ofs2 + n1) by (unfold n1; omega). + replace (i + (ofs2 - ofs1)) with (ofs2 + n1) by (unfold n1; lia). exact LB''. apply Z.divide_add_r; auto. Qed. @@ -655,9 +655,9 @@ Proof with (try discriminate). Mem.loadv chunk m (Vptr sp ofs) = Some v -> Mem.loadv chunk m' (Vptr sp (Ptrofs.repr j)) = Some v). { - simpl; intros. rewrite Ptrofs.unsigned_repr by omega. + simpl; intros. rewrite Ptrofs.unsigned_repr by lia. unfold j, delta. eapply load_memcpy; eauto. - apply Zmod_divide; auto. generalize (align_chunk_pos chunk); omega. + apply Zmod_divide; auto. generalize (align_chunk_pos chunk); lia. } inv H2. + inv H3. exploit eval_addressing_Ainstack_inv; eauto. intros [E1 E2]. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index e92be2b4..fb8e57b7 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -286,7 +286,7 @@ Proof. constructor. econstructor; eauto with coqlib. (* eliminated *) - right. split. simpl. omega. split. auto. econstructor; eauto with coqlib. + right. split. simpl. lia. split. auto. econstructor; eauto with coqlib. (* Lgoto *) left; econstructor; split. econstructor. eapply find_label_translated; eauto. red; auto. diff --git a/backend/Cminor.v b/backend/Cminor.v index 91a4c104..cf0ba314 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -588,7 +588,7 @@ Proof. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate vres2 k m2). econstructor; eauto. (* trace length *) - red; intros; inv H; simpl; try omega; eapply external_call_trace_length; eauto. + red; intros; inv H; simpl; try lia; eapply external_call_trace_length; eauto. Qed. (** This semantics is determinate. *) @@ -645,7 +645,7 @@ Proof. intros (A & B). split; intros; auto. apply B in H; destruct H; congruence. - (* single event *) - red; simpl. destruct 1; simpl; try omega; + red; simpl. destruct 1; simpl; try lia; eapply external_call_trace_length; eauto. - (* initial states *) inv H; inv H0. unfold ge0, ge1 in *. congruence. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 96cb8ae6..5cbdc249 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -522,9 +522,9 @@ Lemma insert_lenv_lookup1: nth_error le' n = Some v. Proof. induction 1; intros. - omegaContradiction. + extlia. destruct n; simpl; simpl in H0. auto. - apply IHinsert_lenv. auto. omega. + apply IHinsert_lenv. auto. lia. Qed. Lemma insert_lenv_lookup2: @@ -536,8 +536,8 @@ Lemma insert_lenv_lookup2: Proof. induction 1; intros. simpl. assumption. - simpl. destruct n. omegaContradiction. - apply IHinsert_lenv. exact H0. omega. + simpl. destruct n. extlia. + apply IHinsert_lenv. exact H0. lia. Qed. Lemma eval_lift_expr: diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index a5d08a0f..a3592c4d 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -364,7 +364,7 @@ Proof. - (* Inop, skipped over *) assert (s0 = pc') by congruence. subst s0. - right; exists n; split. omega. split. auto. + right; exists n; split. lia. split. auto. apply match_states_intro; auto. - (* Iop *) @@ -528,7 +528,7 @@ Opaque builtin_strength_reduction. - (* Icond, skipped over *) rewrite H1 in H; inv H. - right; exists n; split. omega. split. auto. + right; exists n; split. lia. split. auto. econstructor; eauto. - (* Ijumptable *) diff --git a/backend/Conventions.v b/backend/Conventions.v index 14ffb587..8910ee49 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -60,9 +60,9 @@ Remark fold_max_outgoing_above: forall l n, fold_left max_outgoing_2 l n >= n. Proof. assert (A: forall n l, max_outgoing_1 n l >= n). - { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } + { intros; unfold max_outgoing_1. destruct l as [_ | []]; extlia. } induction l; simpl; intros. - - omega. + - lia. - eapply Zge_trans. eauto. destruct a; simpl. apply A. eapply Zge_trans; eauto. Qed. @@ -80,14 +80,14 @@ Lemma loc_arguments_bounded: Proof. intros until ty. assert (A: forall n l, n <= max_outgoing_1 n l). - { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } + { intros; unfold max_outgoing_1. destruct l as [_ | []]; extlia. } assert (B: forall p n, In (S Outgoing ofs ty) (regs_of_rpair p) -> ofs + typesize ty <= max_outgoing_2 n p). { intros. destruct p; simpl in H; intuition; subst; simpl. - - xomega. - - eapply Z.le_trans. 2: apply A. xomega. - - xomega. } + - extlia. + - eapply Z.le_trans. 2: apply A. extlia. + - extlia. } assert (C: forall l n, In (S Outgoing ofs ty) (regs_of_rpairs l) -> ofs + typesize ty <= fold_left max_outgoing_2 l n). @@ -168,7 +168,7 @@ Proof. unfold loc_argument_acceptable. destruct l; intros. auto. destruct sl; try contradiction. destruct H1. generalize (loc_arguments_bounded _ _ _ H0). - generalize (typesize_pos ty). omega. + generalize (typesize_pos ty). lia. Qed. diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 2edc0395..7aa6ff88 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -67,7 +67,7 @@ Lemma mextends_agree: forall m1 m2 P, Mem.extends m1 m2 -> magree m1 m2 P. Proof. intros. destruct H. destruct mext_inj. constructor; intros. -- replace ofs with (ofs + 0) by omega. eapply mi_perm; eauto. auto. +- replace ofs with (ofs + 0) by lia. eapply mi_perm; eauto. auto. - eauto. - exploit mi_memval; eauto. unfold inject_id; eauto. rewrite Z.add_0_r. auto. @@ -99,15 +99,15 @@ Proof. induction n; intros; simpl. constructor. rewrite Nat2Z.inj_succ in H. constructor. - apply H. omega. - apply IHn. intros; apply H; omega. + apply H. lia. + apply IHn. intros; apply H; lia. } Local Transparent Mem.loadbytes. unfold Mem.loadbytes; intros. destruct H. destruct (Mem.range_perm_dec m1 b ofs (ofs + n) Cur Readable); inv H0. rewrite pred_dec_true. econstructor; split; eauto. apply GETN. intros. rewrite Z_to_nat_max in H. - assert (ofs <= i < ofs + n) by xomega. + assert (ofs <= i < ofs + n) by extlia. apply ma_memval0; auto. red; intros; eauto. Qed. @@ -146,11 +146,11 @@ Proof. (ZMap.get q (Mem.setN bytes2 p c2))). { induction 1; intros; simpl. - - apply H; auto. simpl. omega. + - apply H; auto. simpl. lia. - simpl length in H1; rewrite Nat2Z.inj_succ in H1. apply IHlist_forall2; auto. intros. rewrite ! ZMap.gsspec. destruct (ZIndexed.eq i p). auto. - apply H1; auto. unfold ZIndexed.t in *; omega. + apply H1; auto. unfold ZIndexed.t in *; lia. } intros. destruct (Mem.range_perm_storebytes m2 b ofs bytes2) as [m2' ST2]. @@ -211,8 +211,8 @@ Proof. - rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0). rewrite PMap.gsspec. destruct (peq b0 b). + subst b0. rewrite Mem.setN_outside. eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. - destruct (zlt ofs0 ofs); auto. destruct (zle (ofs + Z.of_nat (length bytes1)) ofs0); try omega. - elim (H1 ofs0). omega. auto. + destruct (zlt ofs0 ofs); auto. destruct (zle (ofs + Z.of_nat (length bytes1)) ofs0); try lia. + elim (H1 ofs0). lia. auto. + eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. - rewrite (Mem.nextblock_storebytes _ _ _ _ _ H0). eapply ma_nextblock; eauto. @@ -966,7 +966,7 @@ Ltac UseTransfer := intros. eapply nlive_remove; eauto. unfold adst, vanalyze; rewrite AN; eapply aaddr_arg_sound_1; eauto. erewrite Mem.loadbytes_length in H1 by eauto. - rewrite Z2Nat.id in H1 by omega. auto. + rewrite Z2Nat.id in H1 by lia. auto. eauto. intros (tm' & A & B). econstructor; split. @@ -993,7 +993,7 @@ Ltac UseTransfer := intros (bc & A & B & C). intros. eapply nlive_contains; eauto. erewrite Mem.loadbytes_length in H0 by eauto. - rewrite Z2Nat.id in H0 by omega. auto. + rewrite Z2Nat.id in H0 by lia. auto. + (* annot *) destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x2) as (ne1, nm1) eqn:TR. InvSoundState. diff --git a/backend/Inlining.v b/backend/Inlining.v index f7ee4166..7eb0f0fa 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -71,12 +71,12 @@ Inductive sincr (s1 s2: state) : Prop := Remark sincr_refl: forall s, sincr s s. Proof. - intros; constructor; xomega. + intros; constructor; extlia. Qed. Lemma sincr_trans: forall s1 s2 s3, sincr s1 s2 -> sincr s2 s3 -> sincr s1 s3. Proof. - intros. inv H; inv H0. constructor; xomega. + intros. inv H; inv H0. constructor; extlia. Qed. (** Dependently-typed state monad, ensuring that the final state is @@ -111,7 +111,7 @@ Program Definition set_instr (pc: node) (i: instruction): mon unit := (mkstate s.(st_nextreg) s.(st_nextnode) (PTree.set pc i s.(st_code)) s.(st_stksize)) _. Next Obligation. - intros; constructor; simpl; xomega. + intros; constructor; simpl; extlia. Qed. Program Definition add_instr (i: instruction): mon node := @@ -121,7 +121,7 @@ Program Definition add_instr (i: instruction): mon node := (mkstate s.(st_nextreg) (Pos.succ pc) (PTree.set pc i s.(st_code)) s.(st_stksize)) _. Next Obligation. - intros; constructor; simpl; xomega. + intros; constructor; simpl; extlia. Qed. Program Definition reserve_nodes (numnodes: positive): mon positive := @@ -130,7 +130,7 @@ Program Definition reserve_nodes (numnodes: positive): mon positive := (mkstate s.(st_nextreg) (Pos.add s.(st_nextnode) numnodes) s.(st_code) s.(st_stksize)) _. Next Obligation. - intros; constructor; simpl; xomega. + intros; constructor; simpl; extlia. Qed. Program Definition reserve_regs (numregs: positive): mon positive := @@ -139,7 +139,7 @@ Program Definition reserve_regs (numregs: positive): mon positive := (mkstate (Pos.add s.(st_nextreg) numregs) s.(st_nextnode) s.(st_code) s.(st_stksize)) _. Next Obligation. - intros; constructor; simpl; xomega. + intros; constructor; simpl; extlia. Qed. Program Definition request_stack (sz: Z): mon unit := @@ -148,7 +148,7 @@ Program Definition request_stack (sz: Z): mon unit := (mkstate s.(st_nextreg) s.(st_nextnode) s.(st_code) (Z.max s.(st_stksize) sz)) _. Next Obligation. - intros; constructor; simpl; xomega. + intros; constructor; simpl; extlia. Qed. Program Definition ptree_mfold {A: Type} (f: positive -> A -> mon unit) (t: PTree.t A): mon unit := diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index cc84b1cc..0434a4a4 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -67,21 +67,21 @@ Qed. Remark sreg_below_diff: forall ctx r r', Plt r' ctx.(dreg) -> sreg ctx r <> r'. Proof. - intros. zify. unfold sreg; rewrite shiftpos_eq. xomega. + intros. zify. unfold sreg; rewrite shiftpos_eq. extlia. Qed. Remark context_below_diff: forall ctx1 ctx2 r1 r2, context_below ctx1 ctx2 -> Ple r1 ctx1.(mreg) -> sreg ctx1 r1 <> sreg ctx2 r2. Proof. - intros. red in H. zify. unfold sreg; rewrite ! shiftpos_eq. xomega. + intros. red in H. zify. unfold sreg; rewrite ! shiftpos_eq. extlia. Qed. Remark context_below_lt: forall ctx1 ctx2 r, context_below ctx1 ctx2 -> Ple r ctx1.(mreg) -> Plt (sreg ctx1 r) ctx2.(dreg). Proof. intros. red in H. unfold Plt; zify. unfold sreg; rewrite shiftpos_eq. - xomega. + extlia. Qed. (* @@ -89,7 +89,7 @@ Remark context_below_le: forall ctx1 ctx2 r, context_below ctx1 ctx2 -> Ple r ctx1.(mreg) -> Ple (sreg ctx1 r) ctx2.(dreg). Proof. intros. red in H. unfold Ple; zify. unfold sreg; rewrite shiftpos_eq. - xomega. + extlia. Qed. *) @@ -105,7 +105,7 @@ Definition val_reg_charact (F: meminj) (ctx: context) (rs': regset) (v: val) (r: Remark Plt_Ple_dec: forall p q, {Plt p q} + {Ple q p}. Proof. - intros. destruct (plt p q). left; auto. right; xomega. + intros. destruct (plt p q). left; auto. right; extlia. Qed. Lemma agree_val_reg_gen: @@ -149,7 +149,7 @@ Proof. repeat rewrite Regmap.gsspec. destruct (peq r0 r). subst r0. rewrite peq_true. auto. rewrite peq_false. auto. apply shiftpos_diff; auto. - rewrite Regmap.gso. auto. xomega. + rewrite Regmap.gso. auto. extlia. Qed. Lemma agree_set_reg_undef: @@ -184,7 +184,7 @@ Proof. unfold agree_regs; intros. destruct H. split; intros. rewrite H0. auto. apply shiftpos_above. - eapply Pos.lt_le_trans. apply shiftpos_below. xomega. + eapply Pos.lt_le_trans. apply shiftpos_below. extlia. apply H1; auto. Qed. @@ -272,7 +272,7 @@ Lemma range_private_invariant: range_private F1 m1 m1' sp lo hi. Proof. intros; red; intros. exploit H; eauto. intros [A B]. split; auto. - intros; red; intros. exploit H0; eauto. omega. intros [P Q]. + intros; red; intros. exploit H0; eauto. lia. intros [P Q]. eelim B; eauto. Qed. @@ -293,12 +293,12 @@ Lemma range_private_alloc_left: range_private F1 m1 m' sp' (base + Z.max sz 0) hi. Proof. intros; red; intros. - exploit (H ofs). generalize (Z.le_max_r sz 0). omega. intros [A B]. + exploit (H ofs). generalize (Z.le_max_r sz 0). lia. intros [A B]. split; auto. intros; red; intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b sp); intros. subst b. rewrite H1 in H4; inv H4. - rewrite Zmax_spec in H3. destruct (zlt 0 sz); omega. + rewrite Zmax_spec in H3. destruct (zlt 0 sz); lia. rewrite H2 in H4; auto. eelim B; eauto. Qed. @@ -313,21 +313,21 @@ Proof. intros; red; intros. destruct (zlt ofs (base + Z.max sz 0)) as [z|z]. red; split. - replace ofs with ((ofs - base) + base) by omega. + replace ofs with ((ofs - base) + base) by lia. eapply Mem.perm_inject; eauto. eapply Mem.free_range_perm; eauto. - rewrite Zmax_spec in z. destruct (zlt 0 sz); omega. + rewrite Zmax_spec in z. destruct (zlt 0 sz); lia. intros; red; intros. destruct (eq_block b b0). subst b0. rewrite H1 in H4; inv H4. - eelim Mem.perm_free_2; eauto. rewrite Zmax_spec in z. destruct (zlt 0 sz); omega. + eelim Mem.perm_free_2; eauto. rewrite Zmax_spec in z. destruct (zlt 0 sz); lia. exploit Mem.mi_no_overlap; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.free_range_perm. eauto. - instantiate (1 := ofs - base). rewrite Zmax_spec in z. destruct (zlt 0 sz); omega. + instantiate (1 := ofs - base). rewrite Zmax_spec in z. destruct (zlt 0 sz); lia. eapply Mem.perm_free_3; eauto. - intros [A | A]. congruence. omega. + intros [A | A]. congruence. lia. - exploit (H ofs). omega. intros [A B]. split. auto. + exploit (H ofs). lia. intros [A B]. split. auto. intros; red; intros. eelim B; eauto. eapply Mem.perm_free_3; eauto. Qed. @@ -607,39 +607,39 @@ Proof. (* cons *) apply match_stacks_cons with (fenv := fenv) (ctx := ctx); auto. eapply match_stacks_inside_invariant; eauto. - intros; eapply INJ; eauto; xomega. - intros; eapply PERM1; eauto; xomega. - intros; eapply PERM2; eauto; xomega. - intros; eapply PERM3; eauto; xomega. + intros; eapply INJ; eauto; extlia. + intros; eapply PERM1; eauto; extlia. + intros; eapply PERM2; eauto; extlia. + intros; eapply PERM3; eauto; extlia. eapply agree_regs_incr; eauto. eapply range_private_invariant; eauto. (* untailcall *) apply match_stacks_untailcall with (ctx := ctx); auto. eapply match_stacks_inside_invariant; eauto. - intros; eapply INJ; eauto; xomega. - intros; eapply PERM1; eauto; xomega. - intros; eapply PERM2; eauto; xomega. - intros; eapply PERM3; eauto; xomega. + intros; eapply INJ; eauto; extlia. + intros; eapply PERM1; eauto; extlia. + intros; eapply PERM2; eauto; extlia. + intros; eapply PERM3; eauto; extlia. eapply range_private_invariant; eauto. induction 1; intros. (* base *) eapply match_stacks_inside_base; eauto. eapply match_stacks_invariant; eauto. - intros; eapply INJ; eauto; xomega. - intros; eapply PERM1; eauto; xomega. - intros; eapply PERM2; eauto; xomega. - intros; eapply PERM3; eauto; xomega. + intros; eapply INJ; eauto; extlia. + intros; eapply PERM1; eauto; extlia. + intros; eapply PERM2; eauto; extlia. + intros; eapply PERM3; eauto; extlia. (* inlined *) apply match_stacks_inside_inlined with (fenv := fenv) (ctx' := ctx'); auto. apply IHmatch_stacks_inside; auto. - intros. apply RS. red in BELOW. xomega. + intros. apply RS. red in BELOW. extlia. apply agree_regs_incr with F; auto. apply agree_regs_invariant with rs'; auto. - intros. apply RS. red in BELOW. xomega. + intros. apply RS. red in BELOW. extlia. eapply range_private_invariant; eauto. - intros. split. eapply INJ; eauto. xomega. eapply PERM1; eauto. xomega. - intros. eapply PERM2; eauto. xomega. + intros. split. eapply INJ; eauto. extlia. eapply PERM1; eauto. extlia. + intros. eapply PERM2; eauto. extlia. Qed. Lemma match_stacks_empty: @@ -668,7 +668,7 @@ Lemma match_stacks_inside_set_reg: match_stacks_inside F m m' stk stk' f' ctx sp' (rs'#(sreg ctx r) <- v). Proof. intros. eapply match_stacks_inside_invariant; eauto. - intros. apply Regmap.gso. zify. unfold sreg; rewrite shiftpos_eq. xomega. + intros. apply Regmap.gso. zify. unfold sreg; rewrite shiftpos_eq. extlia. Qed. Lemma match_stacks_inside_set_res: @@ -717,11 +717,11 @@ Proof. subst b1. rewrite H1 in H4. inv H4. eelim Plt_strict; eauto. (* inlined *) eapply match_stacks_inside_inlined; eauto. - eapply IHmatch_stacks_inside; eauto. destruct SBELOW. omega. + eapply IHmatch_stacks_inside; eauto. destruct SBELOW. lia. eapply agree_regs_incr; eauto. eapply range_private_invariant; eauto. intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b0 b); intros. - subst b0. rewrite H2 in H5; inv H5. elimtype False; xomega. + subst b0. rewrite H2 in H5; inv H5. elimtype False; extlia. rewrite H3 in H5; auto. Qed. @@ -753,25 +753,25 @@ Lemma min_alignment_sound: Proof. intros; red; intros. unfold min_alignment in H. assert (2 <= sz -> (2 | n)). intros. - destruct (zle sz 1). omegaContradiction. + destruct (zle sz 1). extlia. destruct (zle sz 2). auto. destruct (zle sz 4). apply Z.divide_trans with 4; auto. exists 2; auto. apply Z.divide_trans with 8; auto. exists 4; auto. assert (4 <= sz -> (4 | n)). intros. - destruct (zle sz 1). omegaContradiction. - destruct (zle sz 2). omegaContradiction. + destruct (zle sz 1). extlia. + destruct (zle sz 2). extlia. destruct (zle sz 4). auto. apply Z.divide_trans with 8; auto. exists 2; auto. assert (8 <= sz -> (8 | n)). intros. - destruct (zle sz 1). omegaContradiction. - destruct (zle sz 2). omegaContradiction. - destruct (zle sz 4). omegaContradiction. + destruct (zle sz 1). extlia. + destruct (zle sz 2). extlia. + destruct (zle sz 4). extlia. auto. destruct chunk; simpl in *; auto. apply Z.divide_1_l. apply Z.divide_1_l. - apply H2; omega. - apply H2; omega. + apply H2; lia. + apply H2; lia. Qed. (** Preservation by external calls *) @@ -803,19 +803,19 @@ Proof. inv MG. constructor; intros; eauto. destruct (F1 b1) as [[b2' delta']|] eqn:?. exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. eapply IMAGE; eauto. - exploit SEP; eauto. intros [A B]. elim B. red. xomega. + exploit SEP; eauto. intros [A B]. elim B. red. extlia. eapply match_stacks_cons; eauto. - eapply match_stacks_inside_extcall; eauto. xomega. + eapply match_stacks_inside_extcall; eauto. extlia. eapply agree_regs_incr; eauto. - eapply range_private_extcall; eauto. red; xomega. - intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega. + eapply range_private_extcall; eauto. red; extlia. + intros. apply SSZ2; auto. apply MAXPERM'; auto. red; extlia. eapply match_stacks_untailcall; eauto. - eapply match_stacks_inside_extcall; eauto. xomega. - eapply range_private_extcall; eauto. red; xomega. - intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega. + eapply match_stacks_inside_extcall; eauto. extlia. + eapply range_private_extcall; eauto. red; extlia. + intros. apply SSZ2; auto. apply MAXPERM'; auto. red; extlia. induction 1; intros. eapply match_stacks_inside_base; eauto. - eapply match_stacks_extcall; eauto. xomega. + eapply match_stacks_extcall; eauto. extlia. eapply match_stacks_inside_inlined; eauto. eapply agree_regs_incr; eauto. eapply range_private_extcall; eauto. @@ -829,7 +829,7 @@ Lemma align_unchanged: forall n amount, amount > 0 -> (amount | n) -> align n amount = n. Proof. intros. destruct H0 as [p EQ]. subst n. unfold align. decEq. - apply Zdiv_unique with (b := amount - 1). omega. omega. + apply Zdiv_unique with (b := amount - 1). lia. lia. Qed. Lemma match_stacks_inside_inlined_tailcall: @@ -849,10 +849,10 @@ Proof. (* inlined *) assert (dstk ctx <= dstk ctx'). rewrite H1. apply align_le. apply min_alignment_pos. eapply match_stacks_inside_inlined; eauto. - red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; omega. apply H3. inv H4. xomega. + red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; lia. apply H3. inv H4. extlia. congruence. - unfold context_below in *. xomega. - unfold context_stack_call in *. omega. + unfold context_below in *. extlia. + unfold context_stack_call in *. lia. Qed. (** ** Relating states *) @@ -1014,12 +1014,12 @@ Proof. + (* inlined *) assert (EQ: fd = Internal f0) by (eapply find_inlined_function; eauto). subst fd. - right; split. simpl; omega. split. auto. + right; split. simpl; lia. split. auto. econstructor; eauto. eapply match_stacks_inside_inlined; eauto. - red; intros. apply PRIV. inv H13. destruct H16. xomega. + red; intros. apply PRIV. inv H13. destruct H16. extlia. apply agree_val_regs_gen; auto. - red; intros; apply PRIV. destruct H16. omega. + red; intros; apply PRIV. destruct H16. lia. - (* tailcall *) exploit match_stacks_inside_globalenvs; eauto. intros [bound G]. @@ -1032,9 +1032,9 @@ Proof. assert (X: { m1' | Mem.free m'0 sp' 0 (fn_stacksize f') = Some m1'}). apply Mem.range_perm_free. red; intros. destruct (zlt ofs f.(fn_stacksize)). - replace ofs with (ofs + dstk ctx) by omega. eapply Mem.perm_inject; eauto. - eapply Mem.free_range_perm; eauto. omega. - inv FB. eapply range_private_perms; eauto. xomega. + replace ofs with (ofs + dstk ctx) by lia. eapply Mem.perm_inject; eauto. + eapply Mem.free_range_perm; eauto. lia. + inv FB. eapply range_private_perms; eauto. extlia. destruct X as [m1' FREE]. left; econstructor; split. eapply plus_one. eapply exec_Itailcall; eauto. @@ -1045,12 +1045,12 @@ Proof. intros. eapply Mem.perm_free_3; eauto. intros. eapply Mem.perm_free_1; eauto with ordered_type. intros. eapply Mem.perm_free_3; eauto. - erewrite Mem.nextblock_free; eauto. red in VB; xomega. + erewrite Mem.nextblock_free; eauto. red in VB; extlia. eapply agree_val_regs; eauto. eapply Mem.free_right_inject; eauto. eapply Mem.free_left_inject; eauto. (* show that no valid location points into the stack block being freed *) - intros. rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). omega. intros [P Q]. - eelim Q; eauto. replace (ofs + delta - delta) with ofs by omega. + intros. rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). lia. intros [P Q]. + eelim Q; eauto. replace (ofs + delta - delta) with ofs by lia. apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. + (* turned into a call *) left; econstructor; split. @@ -1065,7 +1065,7 @@ Proof. + (* inlined *) assert (EQ: fd = Internal f0) by (eapply find_inlined_function; eauto). subst fd. - right; split. simpl; omega. split. auto. + right; split. simpl; lia. split. auto. econstructor; eauto. eapply match_stacks_inside_inlined_tailcall; eauto. eapply match_stacks_inside_invariant; eauto. @@ -1074,7 +1074,7 @@ Proof. eapply Mem.free_left_inject; eauto. red; intros; apply PRIV'. assert (dstk ctx <= dstk ctx'). red in H14; rewrite H14. apply align_le. apply min_alignment_pos. - omega. + lia. - (* builtin *) exploit tr_funbody_inv; eauto. intros TR; inv TR. @@ -1124,10 +1124,10 @@ Proof. assert (X: { m1' | Mem.free m'0 sp' 0 (fn_stacksize f') = Some m1'}). apply Mem.range_perm_free. red; intros. destruct (zlt ofs f.(fn_stacksize)). - replace ofs with (ofs + dstk ctx) by omega. eapply Mem.perm_inject; eauto. - eapply Mem.free_range_perm; eauto. omega. + replace ofs with (ofs + dstk ctx) by lia. eapply Mem.perm_inject; eauto. + eapply Mem.free_range_perm; eauto. lia. inv FB. eapply range_private_perms; eauto. - generalize (Zmax_spec (fn_stacksize f) 0). destruct (zlt 0 (fn_stacksize f)); omega. + generalize (Zmax_spec (fn_stacksize f) 0). destruct (zlt 0 (fn_stacksize f)); lia. destruct X as [m1' FREE]. left; econstructor; split. eapply plus_one. eapply exec_Ireturn; eauto. @@ -1137,19 +1137,19 @@ Proof. intros. eapply Mem.perm_free_3; eauto. intros. eapply Mem.perm_free_1; eauto with ordered_type. intros. eapply Mem.perm_free_3; eauto. - erewrite Mem.nextblock_free; eauto. red in VB; xomega. + erewrite Mem.nextblock_free; eauto. red in VB; extlia. destruct or; simpl. apply agree_val_reg; auto. auto. eapply Mem.free_right_inject; eauto. eapply Mem.free_left_inject; eauto. (* show that no valid location points into the stack block being freed *) intros. inversion FB; subst. assert (PRIV': range_private F m' m'0 sp' (dstk ctx) f'.(fn_stacksize)). rewrite H8 in PRIV. eapply range_private_free_left; eauto. - rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). omega. intros [A B]. - eelim B; eauto. replace (ofs + delta - delta) with ofs by omega. + rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). lia. intros [A B]. + eelim B; eauto. replace (ofs + delta - delta) with ofs by lia. apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. + (* inlined *) - right. split. simpl. omega. split. auto. + right. split. simpl. lia. split. auto. econstructor; eauto. eapply match_stacks_inside_invariant; eauto. intros. eapply Mem.perm_free_3; eauto. @@ -1165,7 +1165,7 @@ Proof. { eapply tr_function_linkorder; eauto. } inversion TR; subst. exploit Mem.alloc_parallel_inject. eauto. eauto. apply Z.le_refl. - instantiate (1 := fn_stacksize f'). inv H1. xomega. + instantiate (1 := fn_stacksize f'). inv H1. extlia. intros [F' [m1' [sp' [A [B [C [D E]]]]]]]. left; econstructor; split. eapply plus_one. eapply exec_function_internal; eauto. @@ -1187,13 +1187,13 @@ Proof. rewrite H5. apply agree_regs_init_regs. eauto. auto. inv H1; auto. congruence. auto. eapply Mem.valid_new_block; eauto. red; intros. split. - eapply Mem.perm_alloc_2; eauto. inv H1; xomega. + eapply Mem.perm_alloc_2; eauto. inv H1; extlia. intros; red; intros. exploit Mem.perm_alloc_inv. eexact H. eauto. destruct (eq_block b stk); intros. - subst. rewrite D in H9; inv H9. inv H1; xomega. + subst. rewrite D in H9; inv H9. inv H1; extlia. rewrite E in H9; auto. eelim Mem.fresh_block_alloc. eexact A. eapply Mem.mi_mappedblocks; eauto. auto. - intros. exploit Mem.perm_alloc_inv; eauto. rewrite dec_eq_true. omega. + intros. exploit Mem.perm_alloc_inv; eauto. rewrite dec_eq_true. lia. - (* internal function, inlined *) inversion FB; subst. @@ -1203,19 +1203,19 @@ Proof. (* sp' is valid *) instantiate (1 := sp'). auto. (* offset is representable *) - instantiate (1 := dstk ctx). generalize (Z.le_max_r (fn_stacksize f) 0). omega. + instantiate (1 := dstk ctx). generalize (Z.le_max_r (fn_stacksize f) 0). lia. (* size of target block is representable *) - intros. right. exploit SSZ2; eauto with mem. inv FB; omega. + intros. right. exploit SSZ2; eauto with mem. inv FB; lia. (* we have full permissions on sp' at and above dstk ctx *) intros. apply Mem.perm_cur. apply Mem.perm_implies with Freeable; auto with mem. - eapply range_private_perms; eauto. xomega. + eapply range_private_perms; eauto. extlia. (* offset is aligned *) - replace (fn_stacksize f - 0) with (fn_stacksize f) by omega. + replace (fn_stacksize f - 0) with (fn_stacksize f) by lia. inv FB. apply min_alignment_sound; auto. (* nobody maps to (sp, dstk ctx...) *) - intros. exploit (PRIV (ofs + delta')); eauto. xomega. + intros. exploit (PRIV (ofs + delta')); eauto. extlia. intros [A B]. eelim B; eauto. - replace (ofs + delta' - delta') with ofs by omega. + replace (ofs + delta' - delta') with ofs by lia. apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. intros [F' [A [B [C D]]]]. exploit tr_moves_init_regs; eauto. intros [rs'' [P [Q R]]]. @@ -1224,7 +1224,7 @@ Proof. econstructor. eapply match_stacks_inside_alloc_left; eauto. eapply match_stacks_inside_invariant; eauto. - omega. + lia. eauto. auto. apply agree_regs_incr with F; auto. auto. auto. auto. @@ -1245,7 +1245,7 @@ Proof. eapply match_stacks_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto. intros; eapply external_call_max_perm; eauto. intros; eapply external_call_max_perm; eauto. - xomega. + extlia. eapply external_call_nextblock; eauto. auto. auto. @@ -1267,14 +1267,14 @@ Proof. eauto. auto. apply agree_set_reg; auto. auto. auto. auto. - red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; omega. apply PRIV; omega. + red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; lia. apply PRIV; lia. auto. auto. - (* return from inlined function *) inv MS0; try congruence. rewrite RET0 in RET; inv RET. unfold inline_return in AT. assert (PRIV': range_private F m m' sp' (dstk ctx' + mstk ctx') f'.(fn_stacksize)). - red; intros. destruct (zlt ofs (dstk ctx)). apply PAD. omega. apply PRIV. omega. + red; intros. destruct (zlt ofs (dstk ctx)). apply PAD. lia. apply PRIV. lia. destruct or. + (* with a result *) left; econstructor; split. diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index c345c942..477f883a 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -73,7 +73,7 @@ Qed. Lemma shiftpos_eq: forall x y, Zpos (shiftpos x y) = (Zpos x + Zpos y) - 1. Proof. intros. unfold shiftpos. zify. try rewrite Pos2Z.inj_sub. auto. - zify. omega. + zify. lia. Qed. Lemma shiftpos_inj: @@ -82,7 +82,7 @@ Proof. intros. assert (Zpos (shiftpos x n) = Zpos (shiftpos y n)) by congruence. rewrite ! shiftpos_eq in H0. - assert (Z.pos x = Z.pos y) by omega. + assert (Z.pos x = Z.pos y) by lia. congruence. Qed. @@ -95,25 +95,25 @@ Qed. Lemma shiftpos_above: forall x n, Ple n (shiftpos x n). Proof. - intros. unfold Ple; zify. rewrite shiftpos_eq. xomega. + intros. unfold Ple; zify. rewrite shiftpos_eq. extlia. Qed. Lemma shiftpos_not_below: forall x n, Plt (shiftpos x n) n -> False. Proof. - intros. generalize (shiftpos_above x n). xomega. + intros. generalize (shiftpos_above x n). extlia. Qed. Lemma shiftpos_below: forall x n, Plt (shiftpos x n) (Pos.add x n). Proof. - intros. unfold Plt; zify. rewrite shiftpos_eq. omega. + intros. unfold Plt; zify. rewrite shiftpos_eq. lia. Qed. Lemma shiftpos_le: forall x y n, Ple x y -> Ple (shiftpos x n) (shiftpos y n). Proof. - intros. unfold Ple in *; zify. rewrite ! shiftpos_eq. omega. + intros. unfold Ple in *; zify. rewrite ! shiftpos_eq. lia. Qed. @@ -219,9 +219,9 @@ Proof. induction srcs; simpl; intros. monadInv H. auto. destruct dsts; monadInv H. auto. - transitivity (st_code s0)!pc. eapply IHsrcs; eauto. monadInv EQ; simpl. xomega. + transitivity (st_code s0)!pc. eapply IHsrcs; eauto. monadInv EQ; simpl. extlia. monadInv EQ; simpl. apply PTree.gso. - inversion INCR0; simpl in *. xomega. + inversion INCR0; simpl in *. extlia. Qed. Lemma add_moves_spec: @@ -234,13 +234,13 @@ Proof. monadInv H. apply tr_moves_nil; auto. destruct dsts; monadInv H. apply tr_moves_nil; auto. apply tr_moves_cons with x. eapply IHsrcs; eauto. - intros. inversion INCR. apply H0; xomega. + intros. inversion INCR. apply H0; extlia. monadInv EQ. rewrite H0. erewrite add_moves_unchanged; eauto. simpl. apply PTree.gss. - simpl. xomega. - xomega. - inversion INCR; inversion INCR0; simpl in *; xomega. + simpl. extlia. + extlia. + inversion INCR; inversion INCR0; simpl in *; extlia. Qed. (** ** Relational specification of CFG expansion *) @@ -386,9 +386,9 @@ Proof. monadInv H. unfold inline_function in EQ. monadInv EQ. transitivity (s2.(st_code)!pc'). eauto. transitivity (s5.(st_code)!pc'). eapply add_moves_unchanged; eauto. - left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. xomega. + left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. extlia. transitivity (s4.(st_code)!pc'). eapply rec_unchanged; eauto. - simpl. monadInv EQ; simpl. monadInv EQ1; simpl. xomega. + simpl. monadInv EQ; simpl. monadInv EQ1; simpl. extlia. simpl. monadInv EQ1; simpl. auto. monadInv EQ; simpl. monadInv EQ1; simpl. auto. (* tailcall *) @@ -397,9 +397,9 @@ Proof. monadInv H. unfold inline_tail_function in EQ. monadInv EQ. transitivity (s2.(st_code)!pc'). eauto. transitivity (s5.(st_code)!pc'). eapply add_moves_unchanged; eauto. - left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. xomega. + left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. extlia. transitivity (s4.(st_code)!pc'). eapply rec_unchanged; eauto. - simpl. monadInv EQ; simpl. monadInv EQ1; simpl. xomega. + simpl. monadInv EQ; simpl. monadInv EQ1; simpl. extlia. simpl. monadInv EQ1; simpl. auto. monadInv EQ; simpl. monadInv EQ1; simpl. auto. (* return *) @@ -422,7 +422,7 @@ Proof. destruct a as [pc1 instr1]; simpl in *. monadInv H. inv H3. transitivity ((st_code s0)!pc). - eapply IHl; eauto. destruct INCR; xomega. destruct INCR; xomega. + eapply IHl; eauto. destruct INCR; extlia. destruct INCR; extlia. eapply expand_instr_unchanged; eauto. Qed. @@ -438,7 +438,7 @@ Proof. exploit ptree_mfold_spec; eauto. intros [INCR' ITER]. eapply iter_expand_instr_unchanged; eauto. subst s0; auto. - subst s0; simpl. xomega. + subst s0; simpl. extlia. red; intros. exploit list_in_map_inv; eauto. intros [pc1 [A B]]. subst pc. unfold spc in H1. eapply shiftpos_not_below; eauto. apply PTree.elements_keys_norepet. @@ -464,7 +464,7 @@ Remark min_alignment_pos: forall sz, min_alignment sz > 0. Proof. intros; unfold min_alignment. - destruct (zle sz 1). omega. destruct (zle sz 2). omega. destruct (zle sz 4); omega. + destruct (zle sz 1). lia. destruct (zle sz 2). lia. destruct (zle sz 4); lia. Qed. Ltac inv_incr := @@ -501,20 +501,20 @@ Proof. apply tr_call_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto. eapply BASE; eauto. eapply add_moves_spec; eauto. - intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. - xomega. xomega. + intros. rewrite S1. eapply set_instr_other; eauto. unfold node; extlia. + extlia. extlia. eapply rec_spec; eauto. red; intros. rewrite PTree.grspec in H. destruct (PTree.elt_eq id0 id); try discriminate. auto. - simpl. subst s2; simpl in *; xomega. - simpl. subst s3; simpl in *; xomega. - simpl. xomega. + simpl. subst s2; simpl in *; extlia. + simpl. subst s3; simpl in *; extlia. + simpl. extlia. simpl. apply align_divides. apply min_alignment_pos. - assert (dstk ctx + mstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega. - omega. + assert (dstk ctx + mstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. lia. + lia. intros. simpl in H. rewrite S1. - transitivity (s1.(st_code)!pc0). eapply set_instr_other; eauto. unfold node in *; xomega. - eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. - red; simpl. subst s2; simpl in *. xomega. + transitivity (s1.(st_code)!pc0). eapply set_instr_other; eauto. unfold node in *; extlia. + eapply add_moves_unchanged; eauto. unfold node in *; extlia. extlia. + red; simpl. subst s2; simpl in *. extlia. red; simpl. split. auto. apply align_le. apply min_alignment_pos. (* tailcall *) destruct (can_inline fe s1) as [|id f P Q]. @@ -532,20 +532,20 @@ Proof. apply tr_tailcall_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto. eapply BASE; eauto. eapply add_moves_spec; eauto. - intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. xomega. xomega. + intros. rewrite S1. eapply set_instr_other; eauto. unfold node; extlia. extlia. extlia. eapply rec_spec; eauto. red; intros. rewrite PTree.grspec in H. destruct (PTree.elt_eq id0 id); try discriminate. auto. - simpl. subst s3; simpl in *. subst s2; simpl in *. xomega. - simpl. subst s3; simpl in *; xomega. - simpl. xomega. + simpl. subst s3; simpl in *. subst s2; simpl in *. extlia. + simpl. subst s3; simpl in *; extlia. + simpl. extlia. simpl. apply align_divides. apply min_alignment_pos. - assert (dstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega. - omega. + assert (dstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. lia. + lia. intros. simpl in H. rewrite S1. - transitivity (s1.(st_code))!pc0. eapply set_instr_other; eauto. unfold node in *; xomega. - eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. + transitivity (s1.(st_code))!pc0. eapply set_instr_other; eauto. unfold node in *; extlia. + eapply add_moves_unchanged; eauto. unfold node in *; extlia. extlia. red; simpl. -subst s2; simpl in *; xomega. +subst s2; simpl in *; extlia. red; auto. (* builtin *) eapply tr_builtin; eauto. destruct b; eauto. @@ -577,31 +577,31 @@ Proof. destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. assert (A: Ple ctx.(dpc) s0.(st_nextnode)). assert (B: Plt (spc ctx pc) (st_nextnode s)) by eauto. - unfold spc in B. generalize (shiftpos_above pc (dpc ctx)). xomega. + unfold spc in B. generalize (shiftpos_above pc (dpc ctx)). extlia. destruct H9. inv H. (* same pc *) eapply expand_instr_spec; eauto. - omega. + lia. intros. transitivity ((st_code s')!pc'). - apply H7. auto. xomega. + apply H7. auto. extlia. eapply iter_expand_instr_unchanged; eauto. red; intros. rewrite list_map_compose in H9. exploit list_in_map_inv; eauto. intros [[pc0 instr0] [P Q]]. simpl in P. - assert (Plt (spc ctx pc0) (st_nextnode s)) by eauto. xomega. + assert (Plt (spc ctx pc0) (st_nextnode s)) by eauto. extlia. transitivity ((st_code s')!(spc ctx pc)). eapply H8; eauto. eapply iter_expand_instr_unchanged; eauto. - assert (Plt (spc ctx pc) (st_nextnode s)) by eauto. xomega. + assert (Plt (spc ctx pc) (st_nextnode s)) by eauto. extlia. red; intros. rewrite list_map_compose in H. exploit list_in_map_inv; eauto. intros [[pc0 instr0] [P Q]]. simpl in P. assert (pc = pc0) by (eapply shiftpos_inj; eauto). subst pc0. elim H12. change pc with (fst (pc, instr0)). apply List.in_map; auto. (* older pc *) inv_incr. eapply IHl; eauto. - intros. eapply Pos.lt_le_trans. eapply H2. right; eauto. xomega. + intros. eapply Pos.lt_le_trans. eapply H2. right; eauto. extlia. intros; eapply Ple_trans; eauto. - intros. apply H7; auto. xomega. + intros. apply H7; auto. extlia. Qed. Lemma expand_cfg_rec_spec: @@ -629,16 +629,16 @@ Proof. intros. assert (Ple pc0 (max_pc_function f)). eapply max_pc_function_sound. eapply PTree.elements_complete; eauto. - eapply Pos.lt_le_trans. apply shiftpos_below. subst s0; simpl; xomega. + eapply Pos.lt_le_trans. apply shiftpos_below. subst s0; simpl; extlia. subst s0; simpl; auto. - intros. apply H8; auto. subst s0; simpl in H11; xomega. + intros. apply H8; auto. subst s0; simpl in H11; extlia. intros. apply H8. apply shiftpos_above. assert (Ple pc0 (max_pc_function f)). eapply max_pc_function_sound. eapply PTree.elements_complete; eauto. - eapply Pos.lt_le_trans. apply shiftpos_below. inversion i; xomega. + eapply Pos.lt_le_trans. apply shiftpos_below. inversion i; extlia. apply PTree.elements_correct; auto. auto. auto. auto. - inversion INCR0. subst s0; simpl in STKSIZE; xomega. + inversion INCR0. subst s0; simpl in STKSIZE; extlia. Qed. End EXPAND_INSTR. @@ -721,12 +721,12 @@ Opaque initstate. apply funenv_program_compat. eapply expand_cfg_spec with (fe := fenv); eauto. red; auto. - unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. xomega. - unfold ctx; rewrite <- H0; rewrite <- H1; simpl. xomega. - simpl. xomega. + unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. extlia. + unfold ctx; rewrite <- H0; rewrite <- H1; simpl. extlia. + simpl. extlia. simpl. apply Z.divide_0_r. - simpl. omega. - simpl. omega. + simpl. lia. + simpl. lia. simpl. split; auto. destruct INCR2. destruct INCR1. destruct INCR0. destruct INCR. - simpl. change 0 with (st_stksize initstate). omega. + simpl. change 0 with (st_stksize initstate). lia. Qed. diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 10a3d8b2..b065238c 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -642,7 +642,7 @@ Proof. (* Lbranch *) assert ((reachable f)!!pc = true). apply REACH; simpl; auto. - right; split. simpl; omega. split. auto. simpl. econstructor; eauto. + right; split. simpl; lia. split. auto. simpl. econstructor; eauto. (* Lcond *) assert (REACH1: (reachable f)!!pc1 = true) by (apply REACH; simpl; auto). @@ -659,12 +659,12 @@ Proof. rewrite eval_negate_condition. rewrite H. auto. eauto. rewrite DC. econstructor; eauto. (* cond is false: branch is taken *) - right; split. simpl; omega. split. auto. rewrite <- DC. econstructor; eauto. + right; split. simpl; lia. split. auto. rewrite <- DC. econstructor; eauto. rewrite eval_negate_condition. rewrite H. auto. (* branch if cond is true *) destruct b. (* cond is true: branch is taken *) - right; split. simpl; omega. split. auto. econstructor; eauto. + right; split. simpl; lia. split. auto. econstructor; eauto. (* cond is false: no branch *) left; econstructor; split. apply plus_one. eapply exec_Lcond_false. eauto. eauto. @@ -673,7 +673,7 @@ Proof. (* Ljumptable *) assert (REACH': (reachable f)!!pc = true). apply REACH. simpl. eapply list_nth_z_in; eauto. - right; split. simpl; omega. split. auto. econstructor; eauto. + right; split. simpl; lia. split. auto. econstructor; eauto. (* Lreturn *) left; econstructor; split. diff --git a/backend/Locations.v b/backend/Locations.v index c437df5d..2a3ae1d7 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -157,7 +157,7 @@ Module Loc. forall l, ~(diff l l). Proof. destruct l; unfold diff; auto. - red; intros. destruct H; auto. generalize (typesize_pos ty); omega. + red; intros. destruct H; auto. generalize (typesize_pos ty); lia. Qed. Lemma diff_not_eq: @@ -184,7 +184,7 @@ Module Loc. left; auto. destruct (zle (pos0 + typesize ty0) pos). left; auto. - right; red; intros [P | [P | P]]. congruence. omega. omega. + right; red; intros [P | [P | P]]. congruence. lia. lia. left; auto. Defined. @@ -497,7 +497,7 @@ Module OrderedLoc <: OrderedType. destruct x. eelim Plt_strict; eauto. destruct H. eelim OrderedSlot.lt_not_eq; eauto. red; auto. - destruct H. destruct H0. omega. + destruct H. destruct H0. lia. destruct H0. eelim OrderedTyp.lt_not_eq; eauto. red; auto. Qed. Definition compare : forall x y : t, Compare lt eq x y. @@ -545,18 +545,18 @@ Module OrderedLoc <: OrderedType. { destruct H. apply not_eq_sym. apply Plt_ne; auto. apply Plt_ne; auto. } congruence. - assert (RANGE: forall ty, 1 <= typesize ty <= 2). - { intros; unfold typesize. destruct ty0; omega. } + { intros; unfold typesize. destruct ty0; lia. } destruct H. + destruct H. left. apply not_eq_sym. apply OrderedSlot.lt_not_eq; auto. destruct H. right. - destruct H0. right. generalize (RANGE ty'); omega. + destruct H0. right. generalize (RANGE ty'); lia. destruct H0. assert (ty' = Tint \/ ty' = Tsingle \/ ty' = Tany32). { unfold OrderedTyp.lt in H1. destruct ty'; auto; compute in H1; congruence. } - right. destruct H2 as [E|[E|E]]; subst ty'; simpl typesize; omega. + right. destruct H2 as [E|[E|E]]; subst ty'; simpl typesize; lia. + destruct H. left. apply OrderedSlot.lt_not_eq; auto. destruct H. right. - destruct H0. left; omega. + destruct H0. left; lia. destruct H0. exfalso. destruct ty'; compute in H1; congruence. Qed. @@ -572,14 +572,14 @@ Module OrderedLoc <: OrderedType. - destruct (OrderedSlot.compare sl sl'); auto. destruct H. contradiction. destruct H. - right; right; split; auto. left; omega. + right; right; split; auto. left; lia. left; right; split; auto. assert (EITHER: typesize ty' = 1 /\ OrderedTyp.lt ty' Tany64 \/ typesize ty' = 2). { destruct ty'; compute; auto. } destruct (zlt ofs' (ofs - 1)). left; auto. destruct EITHER as [[P Q] | P]. - right; split; auto. omega. - left; omega. + right; split; auto. lia. + left; lia. Qed. End OrderedLoc. diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index d9e9e025..d3c6ed75 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -240,9 +240,9 @@ Proof. destruct (zlt i (Int.unsigned n)). - auto. - generalize (Int.unsigned_range n); intros. - apply H. omega. rewrite Int.bits_shru by omega. - replace (i - Int.unsigned n + Int.unsigned n) with i by omega. - rewrite zlt_true by omega. auto. + apply H. lia. rewrite Int.bits_shru by lia. + replace (i - Int.unsigned n + Int.unsigned n) with i by lia. + rewrite zlt_true by lia. auto. Qed. Lemma iagree_shru: @@ -252,9 +252,9 @@ Proof. intros; red; intros. autorewrite with ints; auto. destruct (zlt (i + Int.unsigned n) Int.zwordsize). - generalize (Int.unsigned_range n); intros. - apply H. omega. rewrite Int.bits_shl by omega. - replace (i + Int.unsigned n - Int.unsigned n) with i by omega. - rewrite zlt_false by omega. auto. + apply H. lia. rewrite Int.bits_shl by lia. + replace (i + Int.unsigned n - Int.unsigned n) with i by lia. + rewrite zlt_false by lia. auto. - auto. Qed. @@ -266,7 +266,7 @@ Proof. intros; red; intros. rewrite <- H in H2. rewrite Int.bits_shru in H2 by auto. rewrite ! Int.bits_shr by auto. destruct (zlt (i + Int.unsigned n) Int.zwordsize). -- apply H0; auto. generalize (Int.unsigned_range n); omega. +- apply H0; auto. generalize (Int.unsigned_range n); lia. - discriminate. Qed. @@ -281,11 +281,11 @@ Proof. then i + Int.unsigned n else Int.zwordsize - 1). assert (0 <= j < Int.zwordsize). - { unfold j; destruct (zlt (i + Int.unsigned n) Int.zwordsize); omega. } + { unfold j; destruct (zlt (i + Int.unsigned n) Int.zwordsize); lia. } apply H; auto. autorewrite with ints; auto. apply orb_true_intro. unfold j; destruct (zlt (i + Int.unsigned n) Int.zwordsize). -- left. rewrite zlt_false by omega. - replace (i + Int.unsigned n - Int.unsigned n) with i by omega. +- left. rewrite zlt_false by lia. + replace (i + Int.unsigned n - Int.unsigned n) with i by lia. auto. - right. reflexivity. Qed. @@ -303,7 +303,7 @@ Proof. mod Int.zwordsize) with i. auto. apply eqmod_small_eq with Int.zwordsize; auto. apply eqmod_trans with ((i - Int.unsigned amount) + Int.unsigned amount). - apply eqmod_refl2; omega. + apply eqmod_refl2; lia. eapply eqmod_trans. 2: apply eqmod_mod; auto. apply eqmod_add. apply eqmod_mod; auto. @@ -330,12 +330,12 @@ Lemma eqmod_iagree: Proof. intros. set (p := Z.to_nat (Int.size m)). generalize (Int.size_range m); intros RANGE. - assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. omega. } + assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. lia. } rewrite EQ in H; rewrite <- two_power_nat_two_p in H. red; intros. rewrite ! Int.testbit_repr by auto. destruct (zlt i (Int.size m)). - eapply same_bits_eqmod; eauto. omega. - assert (Int.testbit m i = false) by (eapply Int.bits_size_2; omega). + eapply same_bits_eqmod; eauto. lia. + assert (Int.testbit m i = false) by (eapply Int.bits_size_2; lia). congruence. Qed. @@ -348,11 +348,11 @@ Lemma iagree_eqmod: Proof. intros. set (p := Z.to_nat (Int.size m)). generalize (Int.size_range m); intros RANGE. - assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. omega. } + assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. lia. } rewrite EQ; rewrite <- two_power_nat_two_p. - apply eqmod_same_bits. intros. apply H. omega. - unfold complete_mask. rewrite Int.bits_zero_ext by omega. - rewrite zlt_true by omega. rewrite Int.bits_mone by omega. auto. + apply eqmod_same_bits. intros. apply H. lia. + unfold complete_mask. rewrite Int.bits_zero_ext by lia. + rewrite zlt_true by lia. rewrite Int.bits_mone by lia. auto. Qed. Lemma complete_mask_idem: @@ -363,12 +363,12 @@ Proof. + assert (Int.unsigned m <> 0). { red; intros; elim n. rewrite <- (Int.repr_unsigned m). rewrite H; auto. } assert (0 < Int.size m). - { apply Zsize_pos'. generalize (Int.unsigned_range m); omega. } + { apply Zsize_pos'. generalize (Int.unsigned_range m); lia. } generalize (Int.size_range m); intros. f_equal. apply Int.bits_size_4. tauto. - rewrite Int.bits_zero_ext by omega. rewrite zlt_true by omega. - apply Int.bits_mone; omega. - intros. rewrite Int.bits_zero_ext by omega. apply zlt_false; omega. + rewrite Int.bits_zero_ext by lia. rewrite zlt_true by lia. + apply Int.bits_mone; lia. + intros. rewrite Int.bits_zero_ext by lia. apply zlt_false; lia. Qed. (** ** Abstract operations over value needs. *) @@ -676,12 +676,12 @@ Proof. destruct x; simpl in *. - auto. - unfold Val.zero_ext; InvAgree. - red; intros. autorewrite with ints; try omega. + red; intros. autorewrite with ints; try lia. destruct (zlt i1 n); auto. apply H; auto. - autorewrite with ints; try omega. rewrite zlt_true; auto. + autorewrite with ints; try lia. rewrite zlt_true; auto. - unfold Val.zero_ext; InvAgree; auto. apply Val.lessdef_same. f_equal. - Int.bit_solve; try omega. destruct (zlt i1 n); auto. apply H; auto. - autorewrite with ints; try omega. apply zlt_true; auto. + Int.bit_solve; try lia. destruct (zlt i1 n); auto. apply H; auto. + autorewrite with ints; try lia. apply zlt_true; auto. Qed. Definition sign_ext (n: Z) (x: nval) := @@ -700,25 +700,25 @@ Proof. unfold sign_ext; intros. destruct x; simpl in *. - auto. - unfold Val.sign_ext; InvAgree. - red; intros. autorewrite with ints; try omega. + red; intros. autorewrite with ints; try lia. set (j := if zlt i1 n then i1 else n - 1). assert (0 <= j < Int.zwordsize). - { unfold j; destruct (zlt i1 n); omega. } + { unfold j; destruct (zlt i1 n); lia. } apply H; auto. - autorewrite with ints; try omega. apply orb_true_intro. + autorewrite with ints; try lia. apply orb_true_intro. unfold j; destruct (zlt i1 n). left. rewrite zlt_true; auto. - right. rewrite Int.unsigned_repr. rewrite zlt_false by omega. - replace (n - 1 - (n - 1)) with 0 by omega. reflexivity. - generalize Int.wordsize_max_unsigned; omega. + right. rewrite Int.unsigned_repr. rewrite zlt_false by lia. + replace (n - 1 - (n - 1)) with 0 by lia. reflexivity. + generalize Int.wordsize_max_unsigned; lia. - unfold Val.sign_ext; InvAgree; auto. apply Val.lessdef_same. f_equal. - Int.bit_solve; try omega. + Int.bit_solve; try lia. set (j := if zlt i1 n then i1 else n - 1). assert (0 <= j < Int.zwordsize). - { unfold j; destruct (zlt i1 n); omega. } - apply H; auto. rewrite Int.bits_zero_ext; try omega. + { unfold j; destruct (zlt i1 n); lia. } + apply H; auto. rewrite Int.bits_zero_ext; try lia. rewrite zlt_true. apply Int.bits_mone; auto. - unfold j. destruct (zlt i1 n); omega. + unfold j. destruct (zlt i1 n); lia. Qed. (** The needs of a memory store concerning the value being stored. *) @@ -778,11 +778,11 @@ Proof. - apply sign_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 8). auto. compute; auto. - apply zero_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 8). - auto. omega. + auto. lia. - apply sign_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 16). auto. compute; auto. - apply zero_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 16). - auto. omega. + auto. lia. Qed. (** The needs of a comparison *) @@ -1014,9 +1014,9 @@ Proof. unfold zero_ext_redundant; intros. destruct x; try discriminate. - auto. - simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H. - red; intros; autorewrite with ints; try omega. + red; intros; autorewrite with ints; try lia. destruct (zlt i1 n). apply H0; auto. - rewrite Int.bits_zero_ext in H3 by omega. rewrite zlt_false in H3 by auto. discriminate. + rewrite Int.bits_zero_ext in H3 by lia. rewrite zlt_false in H3 by auto. discriminate. Qed. Definition sign_ext_redundant (n: Z) (x: nval) := @@ -1036,10 +1036,10 @@ Proof. unfold sign_ext_redundant; intros. destruct x; try discriminate. - auto. - simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H. - red; intros; autorewrite with ints; try omega. + red; intros; autorewrite with ints; try lia. destruct (zlt i1 n). apply H0; auto. rewrite Int.bits_or; auto. rewrite H3; auto. - rewrite Int.bits_zero_ext in H3 by omega. rewrite zlt_false in H3 by auto. discriminate. + rewrite Int.bits_zero_ext in H3 by lia. rewrite zlt_false in H3 by auto. discriminate. Qed. (** * Neededness for register environments *) @@ -1300,13 +1300,13 @@ Proof. split; simpl; auto; intros. rewrite PTree.gsspec in H6. destruct (peq id0 id). + inv H6. destruct H3. congruence. destruct gl!id as [iv0|] eqn:NG. - unfold iv'; rewrite ISet.In_add. intros [P|P]. omega. eelim GL; eauto. - unfold iv'; rewrite ISet.In_interval. omega. + unfold iv'; rewrite ISet.In_add. intros [P|P]. lia. eelim GL; eauto. + unfold iv'; rewrite ISet.In_interval. lia. + eauto. - (* Stk ofs *) split; simpl; auto; intros. destruct H3. elim H3. subst b'. eapply bc_stack; eauto. - rewrite ISet.In_add. intros [P|P]. omega. eapply STK; eauto. + rewrite ISet.In_add. intros [P|P]. lia. eapply STK; eauto. Qed. (** Test (conservatively) whether some locations in the range delimited diff --git a/backend/RTL.v b/backend/RTL.v index 9599a24a..a022f55a 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -352,7 +352,7 @@ Proof. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate s0 vres2 m2). econstructor; eauto. (* trace length *) - red; intros; inv H; simpl; try omega. + red; intros; inv H; simpl; try lia. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. Qed. @@ -450,8 +450,8 @@ Proof. rewrite PTree.gempty. congruence. (* inductive case *) intros. rewrite PTree.gsspec in H2. destruct (peq pc k). - inv H2. xomega. - apply Ple_trans with a. auto. xomega. + inv H2. extlia. + apply Ple_trans with a. auto. extlia. Qed. (** Maximum pseudo-register mentioned in a function. All results or arguments @@ -489,9 +489,9 @@ Proof. assert (X: forall l n, Ple m n -> Ple m (fold_left Pos.max l n)). { induction l; simpl; intros. auto. - apply IHl. xomega. } - destruct i; simpl; try (destruct s0); repeat (apply X); try xomega. - destruct o; xomega. + apply IHl. extlia. } + destruct i; simpl; try (destruct s0); repeat (apply X); try extlia. + destruct o; extlia. Qed. Remark max_reg_instr_def: @@ -499,12 +499,12 @@ Remark max_reg_instr_def: Proof. intros. assert (X: forall l n, Ple r n -> Ple r (fold_left Pos.max l n)). - { induction l; simpl; intros. xomega. apply IHl. xomega. } + { induction l; simpl; intros. extlia. apply IHl. extlia. } destruct i; simpl in *; inv H. -- apply X. xomega. -- apply X. xomega. -- destruct s0; apply X; xomega. -- destruct b; inv H1. apply X. simpl. xomega. +- apply X. extlia. +- apply X. extlia. +- destruct s0; apply X; extlia. +- destruct b; inv H1. apply X. simpl. extlia. Qed. Remark max_reg_instr_uses: @@ -514,14 +514,14 @@ Proof. assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)). { induction l; simpl; intros. tauto. - apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. } + apply IHl. destruct H0 as [[A|A]|A]. right; subst; extlia. auto. right; extlia. } destruct i; simpl in *; try (destruct s0); try (apply X; auto). - contradiction. -- destruct H. right; subst; xomega. auto. -- destruct H. right; subst; xomega. auto. -- destruct H. right; subst; xomega. auto. -- intuition. subst; xomega. -- destruct o; simpl in H; intuition. subst; xomega. +- destruct H. right; subst; extlia. auto. +- destruct H. right; subst; extlia. auto. +- destruct H. right; subst; extlia. auto. +- intuition. subst; extlia. +- destruct o; simpl in H; intuition. subst; extlia. Qed. Lemma max_reg_function_def: @@ -539,7 +539,7 @@ Proof. + inv H3. eapply max_reg_instr_def; eauto. + apply Ple_trans with a. auto. apply max_reg_instr_ge. } - unfold max_reg_function. xomega. + unfold max_reg_function. extlia. Qed. Lemma max_reg_function_use: @@ -557,7 +557,7 @@ Proof. + inv H3. eapply max_reg_instr_uses; eauto. + apply Ple_trans with a. auto. apply max_reg_instr_ge. } - unfold max_reg_function. xomega. + unfold max_reg_function. extlia. Qed. Lemma max_reg_function_params: @@ -567,8 +567,8 @@ Proof. assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)). { induction l; simpl; intros. tauto. - apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. } + apply IHl. destruct H0 as [[A|A]|A]. right; subst; extlia. auto. right; extlia. } assert (Y: Ple r (fold_left Pos.max f.(fn_params) 1%positive)). { apply X; auto. } - unfold max_reg_function. xomega. + unfold max_reg_function. extlia. Qed. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index b94ec22f..88f7fe53 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1145,7 +1145,7 @@ Proof. Qed. Ltac Lt_state := - apply lt_state_intro; simpl; try omega. + apply lt_state_intro; simpl; try lia. Lemma lt_state_wf: well_founded lt_state. diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index c57d3652..9d581ec9 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -44,55 +44,55 @@ Proof. set (r := n mod d). intro EUCL. assert (0 <= r <= d - 1). - unfold r. generalize (Z_mod_lt n d d_pos). omega. + unfold r. generalize (Z_mod_lt n d d_pos). lia. assert (0 <= m). apply Zmult_le_0_reg_r with d. auto. - exploit (two_p_gt_ZERO (N + l)). omega. omega. + exploit (two_p_gt_ZERO (N + l)). lia. lia. set (k := m * d - two_p (N + l)). assert (0 <= k <= two_p l). - unfold k; omega. + unfold k; lia. assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r). unfold k. rewrite EUCL. ring. assert (0 <= k * n). - apply Z.mul_nonneg_nonneg; omega. + apply Z.mul_nonneg_nonneg; lia. assert (k * n <= two_p (N + l) - two_p l). apply Z.le_trans with (two_p l * n). - apply Z.mul_le_mono_nonneg_r; omega. - replace (N + l) with (l + N) by omega. + apply Z.mul_le_mono_nonneg_r; lia. + replace (N + l) with (l + N) by lia. rewrite two_p_is_exp. replace (two_p l * two_p N - two_p l) with (two_p l * (two_p N - 1)) by ring. - apply Z.mul_le_mono_nonneg_l. omega. exploit (two_p_gt_ZERO l). omega. omega. - omega. omega. + apply Z.mul_le_mono_nonneg_l. lia. exploit (two_p_gt_ZERO l). lia. lia. + lia. lia. assert (0 <= two_p (N + l) * r). apply Z.mul_nonneg_nonneg. - exploit (two_p_gt_ZERO (N + l)). omega. omega. - omega. + exploit (two_p_gt_ZERO (N + l)). lia. lia. + lia. assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). replace (two_p (N + l) * d - two_p (N + l)) with (two_p (N + l) * (d - 1)) by ring. apply Z.mul_le_mono_nonneg_l. - omega. - exploit (two_p_gt_ZERO (N + l)). omega. omega. + lia. + exploit (two_p_gt_ZERO (N + l)). lia. lia. assert (0 <= m * n - two_p (N + l) * q). apply Zmult_le_reg_r with d. auto. - replace (0 * d) with 0 by ring. rewrite H2. omega. + replace (0 * d) with 0 by ring. rewrite H2. lia. assert (m * n - two_p (N + l) * q < two_p (N + l)). - apply Zmult_lt_reg_r with d. omega. + apply Zmult_lt_reg_r with d. lia. rewrite H2. apply Z.le_lt_trans with (two_p (N + l) * d - two_p l). - omega. - exploit (two_p_gt_ZERO l). omega. omega. + lia. + exploit (two_p_gt_ZERO l). lia. lia. symmetry. apply Zdiv_unique with (m * n - two_p (N + l) * q). - ring. omega. + ring. lia. Qed. Lemma Zdiv_unique_2: forall x y q, y > 0 -> 0 < y * q - x <= y -> Z.div x y = q - 1. Proof. intros. apply Zdiv_unique with (x - (q - 1) * y). ring. - replace ((q - 1) * y) with (y * q - y) by ring. omega. + replace ((q - 1) * y) with (y * q - y) by ring. lia. Qed. Lemma Zdiv_mul_opp: @@ -110,42 +110,42 @@ Proof. set (r := n mod d). intro EUCL. assert (0 <= r <= d - 1). - unfold r. generalize (Z_mod_lt n d d_pos). omega. + unfold r. generalize (Z_mod_lt n d d_pos). lia. assert (0 <= m). apply Zmult_le_0_reg_r with d. auto. - exploit (two_p_gt_ZERO (N + l)). omega. omega. + exploit (two_p_gt_ZERO (N + l)). lia. lia. cut (Z.div (- (m * n)) (two_p (N + l)) = -q - 1). - omega. + lia. apply Zdiv_unique_2. - apply two_p_gt_ZERO. omega. + apply two_p_gt_ZERO. lia. replace (two_p (N + l) * - q - - (m * n)) with (m * n - two_p (N + l) * q) by ring. set (k := m * d - two_p (N + l)). assert (0 < k <= two_p l). - unfold k; omega. + unfold k; lia. assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r). unfold k. rewrite EUCL. ring. split. - apply Zmult_lt_reg_r with d. omega. - replace (0 * d) with 0 by omega. + apply Zmult_lt_reg_r with d. lia. + replace (0 * d) with 0 by lia. rewrite H2. - assert (0 < k * n). apply Z.mul_pos_pos; omega. + assert (0 < k * n). apply Z.mul_pos_pos; lia. assert (0 <= two_p (N + l) * r). - apply Z.mul_nonneg_nonneg. exploit (two_p_gt_ZERO (N + l)); omega. omega. - omega. - apply Zmult_le_reg_r with d. omega. + apply Z.mul_nonneg_nonneg. exploit (two_p_gt_ZERO (N + l)); lia. lia. + lia. + apply Zmult_le_reg_r with d. lia. rewrite H2. assert (k * n <= two_p (N + l)). - rewrite Z.add_comm. rewrite two_p_is_exp; try omega. - apply Z.le_trans with (two_p l * n). apply Z.mul_le_mono_nonneg_r; omega. - apply Z.mul_le_mono_nonneg_l. omega. exploit (two_p_gt_ZERO l). omega. omega. + rewrite Z.add_comm. rewrite two_p_is_exp; try lia. + apply Z.le_trans with (two_p l * n). apply Z.mul_le_mono_nonneg_r; lia. + apply Z.mul_le_mono_nonneg_l. lia. exploit (two_p_gt_ZERO l). lia. lia. assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). replace (two_p (N + l) * d - two_p (N + l)) with (two_p (N + l) * (d - 1)) by ring. - apply Z.mul_le_mono_nonneg_l. exploit (two_p_gt_ZERO (N + l)). omega. omega. omega. - omega. + apply Z.mul_le_mono_nonneg_l. exploit (two_p_gt_ZERO (N + l)). lia. lia. lia. + lia. Qed. (** This is theorem 5.1 from Granlund and Montgomery, PLDI 1994. *) @@ -159,13 +159,13 @@ Lemma Zquot_mul: Z.quot n d = Z.div (m * n) (two_p (N + l)) + (if zlt n 0 then 1 else 0). Proof. intros. destruct (zlt n 0). - exploit (Zdiv_mul_opp m l H H0 (-n)). omega. + exploit (Zdiv_mul_opp m l H H0 (-n)). lia. replace (- - n) with n by ring. replace (Z.quot n d) with (- Z.quot (-n) d). - rewrite Zquot_Zdiv_pos by omega. omega. - rewrite Z.quot_opp_l by omega. ring. - rewrite Z.add_0_r. rewrite Zquot_Zdiv_pos by omega. - apply Zdiv_mul_pos; omega. + rewrite Zquot_Zdiv_pos by lia. lia. + rewrite Z.quot_opp_l by lia. ring. + rewrite Z.add_0_r. rewrite Zquot_Zdiv_pos by lia. + apply Zdiv_mul_pos; lia. Qed. End Z_DIV_MUL. @@ -194,11 +194,11 @@ Proof with (try discriminate). destruct (zlt p1 32)... intros EQ; inv EQ. split. auto. split. auto. intros. - replace (32 + p') with (31 + (p' + 1)) by omega. - apply Zquot_mul; try omega. - replace (31 + (p' + 1)) with (32 + p') by omega. omega. + replace (32 + p') with (31 + (p' + 1)) by lia. + apply Zquot_mul; try lia. + replace (31 + (p' + 1)) with (32 + p') by lia. lia. change (Int.min_signed <= n < Int.half_modulus). - unfold Int.max_signed in H. omega. + unfold Int.max_signed in H. lia. Qed. Lemma divu_mul_params_sound: @@ -223,7 +223,7 @@ Proof with (try discriminate). destruct (zlt p1 32)... intros EQ; inv EQ. split. auto. split. auto. intros. - apply Zdiv_mul_pos; try omega. assumption. + apply Zdiv_mul_pos; try lia. assumption. Qed. Lemma divs_mul_shift_gen: @@ -237,25 +237,25 @@ Proof. exploit divs_mul_params_sound; eauto. intros (A & B & C). split. auto. split. auto. unfold Int.divs. fold n; fold d. rewrite C by (apply Int.signed_range). - rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv. + rewrite two_p_is_exp by lia. rewrite <- Zdiv_Zdiv. rewrite Int.shru_lt_zero. unfold Int.add. apply Int.eqm_samerepr. apply Int.eqm_add. rewrite Int.shr_div_two_p. apply Int.eqm_unsigned_repr_r. apply Int.eqm_refl2. rewrite Int.unsigned_repr. f_equal. rewrite Int.signed_repr. rewrite Int.modulus_power. f_equal. ring. cut (Int.min_signed <= n * m / Int.modulus < Int.half_modulus). - unfold Int.max_signed; omega. - apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos. + unfold Int.max_signed; lia. + apply Zdiv_interval_1. generalize Int.min_signed_neg; lia. apply Int.half_modulus_pos. apply Int.modulus_pos. split. apply Z.le_trans with (Int.min_signed * m). - apply Z.mul_le_mono_nonpos_l. generalize Int.min_signed_neg; omega. omega. - apply Z.mul_le_mono_nonneg_r. omega. unfold n; generalize (Int.signed_range x); tauto. + apply Z.mul_le_mono_nonpos_l. generalize Int.min_signed_neg; lia. lia. + apply Z.mul_le_mono_nonneg_r. lia. unfold n; generalize (Int.signed_range x); tauto. apply Z.le_lt_trans with (Int.half_modulus * m). - apply Z.mul_le_mono_nonneg_r. tauto. generalize (Int.signed_range x); unfold n, Int.max_signed; omega. - apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto. - assert (32 < Int.max_unsigned) by (compute; auto). omega. + apply Z.mul_le_mono_nonneg_r. tauto. generalize (Int.signed_range x); unfold n, Int.max_signed; lia. + apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; lia. tauto. + assert (32 < Int.max_unsigned) by (compute; auto). lia. unfold Int.lt; fold n. rewrite Int.signed_zero. destruct (zlt n 0); apply Int.eqm_unsigned_repr. - 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. Theorem divs_mul_shift_1: @@ -269,7 +269,7 @@ Proof. intros. exploit divs_mul_shift_gen; eauto. instantiate (1 := x). intros (A & B & C). split. auto. rewrite C. unfold Int.mulhs. rewrite Int.signed_repr. auto. - generalize Int.min_signed_neg; unfold Int.max_signed; omega. + generalize Int.min_signed_neg; unfold Int.max_signed; lia. Qed. Theorem divs_mul_shift_2: @@ -305,18 +305,18 @@ Proof. split. auto. rewrite Int.shru_div_two_p. rewrite Int.unsigned_repr. unfold Int.divu, Int.mulhu. f_equal. rewrite C by apply Int.unsigned_range. - rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; omega). + rewrite two_p_is_exp by lia. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; lia). f_equal. rewrite (Int.unsigned_repr m). rewrite Int.unsigned_repr. f_equal. ring. cut (0 <= Int.unsigned x * m / Int.modulus < Int.modulus). - unfold Int.max_unsigned; omega. - apply Zdiv_interval_1. omega. compute; auto. compute; auto. - split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); omega. omega. + unfold Int.max_unsigned; lia. + apply Zdiv_interval_1. lia. compute; auto. compute; auto. + split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); lia. lia. apply Z.le_lt_trans with (Int.modulus * m). - apply Zmult_le_compat_r. generalize (Int.unsigned_range x); omega. omega. - apply Zmult_lt_compat_l. compute; auto. omega. - unfold Int.max_unsigned; omega. - assert (32 < Int.max_unsigned) by (compute; auto). omega. + apply Zmult_le_compat_r. generalize (Int.unsigned_range x); lia. lia. + apply Zmult_lt_compat_l. compute; auto. lia. + unfold Int.max_unsigned; lia. + assert (32 < Int.max_unsigned) by (compute; auto). lia. Qed. (** Same, for 64-bit integers *) @@ -343,11 +343,11 @@ Proof with (try discriminate). destruct (zlt p1 64)... intros EQ; inv EQ. split. auto. split. auto. intros. - replace (64 + p') with (63 + (p' + 1)) by omega. - apply Zquot_mul; try omega. - replace (63 + (p' + 1)) with (64 + p') by omega. omega. + replace (64 + p') with (63 + (p' + 1)) by lia. + apply Zquot_mul; try lia. + replace (63 + (p' + 1)) with (64 + p') by lia. lia. change (Int64.min_signed <= n < Int64.half_modulus). - unfold Int64.max_signed in H. omega. + unfold Int64.max_signed in H. lia. Qed. Lemma divlu_mul_params_sound: @@ -372,13 +372,13 @@ Proof with (try discriminate). destruct (zlt p1 64)... intros EQ; inv EQ. split. auto. split. auto. intros. - apply Zdiv_mul_pos; try omega. assumption. + apply Zdiv_mul_pos; try lia. assumption. Qed. Remark int64_shr'_div_two_p: forall x y, Int64.shr' x y = Int64.repr (Int64.signed x / two_p (Int.unsigned y)). Proof. - intros; unfold Int64.shr'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega. + intros; unfold Int64.shr'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); lia. Qed. Lemma divls_mul_shift_gen: @@ -392,25 +392,25 @@ Proof. exploit divls_mul_params_sound; eauto. intros (A & B & C). split. auto. split. auto. unfold Int64.divs. fold n; fold d. rewrite C by (apply Int64.signed_range). - rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv. + rewrite two_p_is_exp by lia. rewrite <- Zdiv_Zdiv. rewrite Int64.shru_lt_zero. unfold Int64.add. apply Int64.eqm_samerepr. apply Int64.eqm_add. rewrite int64_shr'_div_two_p. apply Int64.eqm_unsigned_repr_r. apply Int64.eqm_refl2. rewrite Int.unsigned_repr. f_equal. rewrite Int64.signed_repr. rewrite Int64.modulus_power. f_equal. ring. cut (Int64.min_signed <= n * m / Int64.modulus < Int64.half_modulus). - unfold Int64.max_signed; omega. - apply Zdiv_interval_1. generalize Int64.min_signed_neg; omega. apply Int64.half_modulus_pos. + unfold Int64.max_signed; lia. + apply Zdiv_interval_1. generalize Int64.min_signed_neg; lia. apply Int64.half_modulus_pos. apply Int64.modulus_pos. split. apply Z.le_trans with (Int64.min_signed * m). - apply Z.mul_le_mono_nonpos_l. generalize Int64.min_signed_neg; omega. omega. + apply Z.mul_le_mono_nonpos_l. generalize Int64.min_signed_neg; lia. lia. apply Z.mul_le_mono_nonneg_r. tauto. unfold n; generalize (Int64.signed_range x); tauto. apply Z.le_lt_trans with (Int64.half_modulus * m). - apply Zmult_le_compat_r. generalize (Int64.signed_range x); unfold n, Int64.max_signed; omega. tauto. - apply Zmult_lt_compat_l. generalize Int64.half_modulus_pos; omega. tauto. - assert (64 < Int.max_unsigned) by (compute; auto). omega. + apply Zmult_le_compat_r. generalize (Int64.signed_range x); unfold n, Int64.max_signed; lia. tauto. + apply Zmult_lt_compat_l. generalize Int64.half_modulus_pos; lia. tauto. + assert (64 < Int.max_unsigned) by (compute; auto). lia. unfold Int64.lt; fold n. rewrite Int64.signed_zero. destruct (zlt n 0); apply Int64.eqm_unsigned_repr. - 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. Theorem divls_mul_shift_1: @@ -424,7 +424,7 @@ Proof. intros. exploit divls_mul_shift_gen; eauto. instantiate (1 := x). intros (A & B & C). split. auto. rewrite C. unfold Int64.mulhs. rewrite Int64.signed_repr. auto. - generalize Int64.min_signed_neg; unfold Int64.max_signed; omega. + generalize Int64.min_signed_neg; unfold Int64.max_signed; lia. Qed. Theorem divls_mul_shift_2: @@ -453,7 +453,7 @@ Qed. Remark int64_shru'_div_two_p: forall x y, Int64.shru' x y = Int64.repr (Int64.unsigned x / two_p (Int.unsigned y)). Proof. - intros; unfold Int64.shru'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega. + intros; unfold Int64.shru'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); lia. Qed. Theorem divlu_mul_shift: @@ -466,18 +466,18 @@ Proof. split. auto. rewrite int64_shru'_div_two_p. rewrite Int.unsigned_repr. unfold Int64.divu, Int64.mulhu. f_equal. rewrite C by apply Int64.unsigned_range. - rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; omega). + rewrite two_p_is_exp by lia. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; lia). f_equal. rewrite (Int64.unsigned_repr m). rewrite Int64.unsigned_repr. f_equal. ring. cut (0 <= Int64.unsigned x * m / Int64.modulus < Int64.modulus). - unfold Int64.max_unsigned; omega. - apply Zdiv_interval_1. omega. compute; auto. compute; auto. - split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int64.unsigned_range x); omega. omega. + unfold Int64.max_unsigned; lia. + apply Zdiv_interval_1. lia. compute; auto. compute; auto. + split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int64.unsigned_range x); lia. lia. apply Z.le_lt_trans with (Int64.modulus * m). - apply Zmult_le_compat_r. generalize (Int64.unsigned_range x); omega. omega. - apply Zmult_lt_compat_l. compute; auto. omega. - unfold Int64.max_unsigned; omega. - assert (64 < Int.max_unsigned) by (compute; auto). omega. + apply Zmult_le_compat_r. generalize (Int64.unsigned_range x); lia. lia. + apply Zmult_lt_compat_l. compute; auto. lia. + unfold Int64.max_unsigned; lia. + assert (64 < Int.max_unsigned) by (compute; auto). lia. Qed. (** * Correctness of the smart constructors for division and modulus *) @@ -515,7 +515,7 @@ Proof. replace (Int.ltu (Int.repr p) Int.iwordsize) with true in Q. inv Q. rewrite B. auto. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true; auto. tauto. - assert (32 < Int.max_unsigned) by (compute; auto). omega. + assert (32 < Int.max_unsigned) by (compute; auto). lia. Qed. Theorem eval_divuimm: @@ -630,7 +630,7 @@ Proof. simpl in LD. inv LD. assert (RANGE: 0 <= p < 32 -> Int.ltu (Int.repr p) Int.iwordsize = true). { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto. - assert (32 < Int.max_unsigned) by (compute; auto). omega. } + assert (32 < Int.max_unsigned) by (compute; auto). lia. } destruct (zlt M Int.half_modulus). - exploit (divs_mul_shift_1 x); eauto. intros [A B]. exploit eval_shrimm. eexact X. instantiate (1 := Int.repr p). intros [v1 [Z LD]]. @@ -768,7 +768,7 @@ Proof. simpl in B1; inv B1. simpl in B2. replace (Int.ltu (Int.repr p) Int64.iwordsize') with true in B2. inv B2. rewrite B. assumption. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true; auto. tauto. - assert (64 < Int.max_unsigned) by (compute; auto). omega. + assert (64 < Int.max_unsigned) by (compute; auto). lia. Qed. Theorem eval_divlu: @@ -847,10 +847,10 @@ Proof. exploit eval_addl. auto. eexact A5. eexact A3. intros (v6 & A6 & B6). assert (RANGE: forall x, 0 <= x < 64 -> Int.ltu (Int.repr x) Int64.iwordsize' = true). { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto. - assert (64 < Int.max_unsigned) by (compute; auto). omega. } + assert (64 < Int.max_unsigned) by (compute; auto). lia. } simpl in B1; inv B1. simpl in B2; inv B2. - simpl in B3; rewrite RANGE in B3 by omega; inv B3. + simpl in B3; rewrite RANGE in B3 by lia; inv B3. destruct (zlt M Int64.half_modulus). - exploit (divls_mul_shift_1 x); eauto. intros [A B]. simpl in B5; rewrite RANGE in B5 by auto; inv B5. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 987926aa..4755ab79 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -531,7 +531,7 @@ Lemma sel_switch_correct: (XElet arg (sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int O t)) (switch_target i dfl cases). Proof. - intros. exploit validate_switch_correct; eauto. omega. intros [A B]. + intros. exploit validate_switch_correct; eauto. lia. intros [A B]. econstructor. eauto. eapply sel_switch_correct_rec; eauto. Qed. @@ -564,7 +564,7 @@ Proof. inv R. unfold Val.cmp in B. simpl in B. revert B. predSpec Int.eq Int.eq_spec n0 (Int.repr n); intros B; inv B. rewrite Int.unsigned_repr. unfold proj_sumbool; rewrite zeq_true; auto. - unfold Int.max_unsigned; omega. + unfold Int.max_unsigned; lia. unfold proj_sumbool; rewrite zeq_false; auto. red; intros; elim H1. rewrite <- (Int.repr_unsigned n0). congruence. - intros until n; intros EVAL R RANGE. @@ -573,7 +573,7 @@ Proof. inv R. unfold Val.cmpu in B. simpl in B. unfold Int.ltu in B. rewrite Int.unsigned_repr in B. destruct (zlt (Int.unsigned n0) n); inv B; auto. - unfold Int.max_unsigned; omega. + unfold Int.max_unsigned; lia. - intros until n; intros EVAL R RANGE. exploit eval_sub. eexact EVAL. apply (INTCONST (Int.repr n)). intros (vb & A & B). inv R. simpl in B. inv B. econstructor; split; eauto. @@ -581,7 +581,7 @@ Proof. with (Int.unsigned (Int.sub n0 (Int.repr n))). constructor. unfold Int.sub. rewrite Int.unsigned_repr_eq. f_equal. f_equal. - apply Int.unsigned_repr. unfold Int.max_unsigned; omega. + apply Int.unsigned_repr. unfold Int.max_unsigned; lia. - intros until i0; intros EVAL R. exists v; split; auto. inv R. rewrite Z.mod_small by (apply Int.unsigned_range). constructor. - constructor. @@ -599,12 +599,12 @@ Proof. eapply eval_cmpl. eexact EVAL. apply eval_longconst with (n := Int64.repr n). inv R. unfold Val.cmpl. simpl. f_equal; f_equal. unfold Int64.eq. rewrite Int64.unsigned_repr. destruct (zeq (Int64.unsigned n0) n); auto. - unfold Int64.max_unsigned; omega. + unfold Int64.max_unsigned; lia. - intros until n; intros EVAL R RANGE. eapply eval_cmplu; auto. eexact EVAL. apply eval_longconst with (n := Int64.repr n). inv R. unfold Val.cmplu. simpl. f_equal; f_equal. unfold Int64.ltu. rewrite Int64.unsigned_repr. destruct (zlt (Int64.unsigned n0) n); auto. - unfold Int64.max_unsigned; omega. + unfold Int64.max_unsigned; lia. - intros until n; intros EVAL R RANGE. exploit eval_subl; auto; try apply HF'. eexact EVAL. apply eval_longconst with (n := Int64.repr n). intros (vb & A & B). @@ -613,7 +613,7 @@ Proof. with (Int64.unsigned (Int64.sub n0 (Int64.repr n))). constructor. unfold Int64.sub. rewrite Int64.unsigned_repr_eq. f_equal. f_equal. - apply Int64.unsigned_repr. unfold Int64.max_unsigned; omega. + apply Int64.unsigned_repr. unfold Int64.max_unsigned; lia. - intros until i0; intros EVAL R. exploit eval_lowlong. eexact EVAL. intros (vb & A & B). inv R. simpl in B. inv B. econstructor; split; eauto. @@ -1295,7 +1295,7 @@ Proof. eapply match_cont_call with (cunit := cunit) (hf := hf); eauto. + (* turned into Sbuiltin *) intros EQ. subst fd. - right; left; split. simpl; omega. split; auto. econstructor; eauto. + right; left; split. simpl; lia. split; auto. econstructor; eauto. - (* Stailcall *) exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. erewrite <- stackspace_function_translated in P by eauto. @@ -1413,7 +1413,7 @@ Proof. apply plus_one; econstructor. econstructor; eauto. destruct optid; simpl; auto. apply set_var_lessdef; auto. - (* return of an external call turned into a Sbuiltin *) - right; left; split. simpl; omega. split. auto. econstructor; eauto. + right; left; split. simpl; lia. split. auto. econstructor; eauto. Qed. Lemma sel_initial_states: diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index 18c1f18d..1e50b1c2 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -335,7 +335,7 @@ Proof. fold (Int.testbit i i0). destruct (zlt i0 Int.zwordsize). auto. - rewrite Int.bits_zero. rewrite Int.bits_above by omega. auto. + rewrite Int.bits_zero. rewrite Int.bits_above by lia. auto. Qed. Theorem eval_longofint: unary_constructor_sound longofint Val.longofint. @@ -352,13 +352,13 @@ Proof. apply Int64.same_bits_eq; intros. rewrite Int64.testbit_repr by auto. rewrite Int64.bits_ofwords by auto. - rewrite Int.bits_signed by omega. + rewrite Int.bits_signed by lia. destruct (zlt i0 Int.zwordsize). auto. assert (Int64.zwordsize = 2 * Int.zwordsize) by reflexivity. - rewrite Int.bits_shr by omega. + rewrite Int.bits_shr by lia. change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1). - f_equal. destruct (zlt (i0 - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega. + f_equal. destruct (zlt (i0 - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); lia. Qed. Theorem eval_negl: unary_constructor_sound negl Val.negl. @@ -545,24 +545,24 @@ Proof. { red; intros. elim H. rewrite <- (Int.repr_unsigned n). rewrite H0. auto. } destruct (Int.ltu n Int.iwordsize) eqn:LT. exploit Int.ltu_iwordsize_inv; eauto. intros RANGE. - assert (0 <= Int.zwordsize - Int.unsigned n < Int.zwordsize) by omega. + assert (0 <= Int.zwordsize - Int.unsigned n < Int.zwordsize) by lia. apply A1. auto. auto. unfold Int.ltu, Int.sub. rewrite Int.unsigned_repr_wordsize. - rewrite Int.unsigned_repr. rewrite zlt_true; auto. omega. - generalize Int.wordsize_max_unsigned; omega. + rewrite Int.unsigned_repr. rewrite zlt_true; auto. lia. + generalize Int.wordsize_max_unsigned; lia. unfold Int.ltu. rewrite zlt_true; auto. change (Int.unsigned Int64.iwordsize') with 64. - change Int.zwordsize with 32 in RANGE. omega. + change Int.zwordsize with 32 in RANGE. lia. destruct (Int.ltu n Int64.iwordsize') eqn:LT'. exploit Int.ltu_inv; eauto. change (Int.unsigned Int64.iwordsize') with (Int.zwordsize * 2). intros RANGE. assert (Int.zwordsize <= Int.unsigned n). unfold Int.ltu in LT. rewrite Int.unsigned_repr_wordsize in LT. - destruct (zlt (Int.unsigned n) Int.zwordsize). discriminate. omega. + destruct (zlt (Int.unsigned n) Int.zwordsize). discriminate. lia. apply A2. tauto. unfold Int.ltu, Int.sub. rewrite Int.unsigned_repr_wordsize. - rewrite Int.unsigned_repr. rewrite zlt_true; auto. omega. - generalize Int.wordsize_max_unsigned; omega. + rewrite Int.unsigned_repr. rewrite zlt_true; auto. lia. + generalize Int.wordsize_max_unsigned; lia. auto. Qed. @@ -918,19 +918,19 @@ Proof. rewrite Int.bits_zero. rewrite Int.bits_or by auto. symmetry. apply orb_false_intro. transitivity (Int64.testbit (Int64.ofwords h l) (i + Int.zwordsize)). - rewrite Int64.bits_ofwords by omega. rewrite zlt_false by omega. f_equal; omega. + rewrite Int64.bits_ofwords by lia. rewrite zlt_false by lia. f_equal; lia. rewrite H0. apply Int64.bits_zero. transitivity (Int64.testbit (Int64.ofwords h l) i). - rewrite Int64.bits_ofwords by omega. rewrite zlt_true by omega. auto. + rewrite Int64.bits_ofwords by lia. rewrite zlt_true by lia. auto. rewrite H0. apply Int64.bits_zero. symmetry. apply Int.eq_false. red; intros; elim H0. apply Int64.same_bits_eq; intros. rewrite Int64.bits_zero. rewrite Int64.bits_ofwords by auto. destruct (zlt i Int.zwordsize). assert (Int.testbit (Int.or h l) i = false) by (rewrite H1; apply Int.bits_zero). - rewrite Int.bits_or in H3 by omega. exploit orb_false_elim; eauto. tauto. + rewrite Int.bits_or in H3 by lia. exploit orb_false_elim; eauto. tauto. assert (Int.testbit (Int.or h l) (i - Int.zwordsize) = false) by (rewrite H1; apply Int.bits_zero). - rewrite Int.bits_or in H3 by omega. exploit orb_false_elim; eauto. tauto. + rewrite Int.bits_or in H3 by lia. exploit orb_false_elim; eauto. tauto. Qed. Lemma eval_cmpl_eq_zero: diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index ffd9b227..7724c5d6 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -58,7 +58,7 @@ Lemma slot_outgoing_argument_valid: Proof. intros. exploit loc_arguments_acceptable_2; eauto. intros [A B]. unfold slot_valid. unfold proj_sumbool. - rewrite zle_true by omega. + rewrite zle_true by lia. rewrite pred_dec_true by auto. auto. Qed. @@ -126,7 +126,7 @@ Proof. destruct (wt_function f); simpl negb. destruct (zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f)))). intros; discriminate. - intros. unfold fe. unfold b. omega. + intros. unfold fe. unfold b. lia. intros; discriminate. Qed. @@ -200,7 +200,7 @@ Next Obligation. - exploit H4; eauto. intros (v & A & B). exists v; split; auto. eapply Mem.load_unchanged_on; eauto. simpl; intros. rewrite size_type_chunk, typesize_typesize in H8. - split; auto. omega. + split; auto. lia. Qed. Next Obligation. eauto with mem. @@ -215,7 +215,7 @@ Remark valid_access_location: Proof. intros; split. - red; intros. apply Mem.perm_implies with Freeable; auto with mem. - apply H0. rewrite size_type_chunk, typesize_typesize in H4. omega. + apply H0. rewrite size_type_chunk, typesize_typesize in H4. lia. - rewrite align_type_chunk. apply Z.divide_add_r. apply Z.divide_trans with 8; auto. exists (8 / (4 * typealign ty)); destruct ty; reflexivity. @@ -233,7 +233,7 @@ Proof. intros. destruct H as (D & E & F & G & H). exploit H; eauto. intros (v & U & V). exists v; split; auto. unfold load_stack; simpl. rewrite Ptrofs.add_zero_l, Ptrofs.unsigned_repr; auto. - unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). omega. + unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). lia. Qed. Lemma set_location: @@ -252,19 +252,19 @@ Proof. { red; intros; eauto with mem. } exists m'; split. - unfold store_stack; simpl. rewrite Ptrofs.add_zero_l, Ptrofs.unsigned_repr; eauto. - unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). omega. + unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). lia. - simpl. intuition auto. + unfold Locmap.set. destruct (Loc.eq (S sl ofs ty) (S sl ofs0 ty0)); [|destruct (Loc.diff_dec (S sl ofs ty) (S sl ofs0 ty0))]. * (* same location *) inv e. rename ofs0 into ofs. rename ty0 into ty. exists (Val.load_result (chunk_of_type ty) v'); split. - eapply Mem.load_store_similar_2; eauto. omega. + eapply Mem.load_store_similar_2; eauto. lia. apply Val.load_result_inject; auto. * (* different locations *) exploit H; eauto. intros (v0 & X & Y). exists v0; split; auto. rewrite <- X; eapply Mem.load_store_other; eauto. - destruct d. congruence. right. rewrite ! size_type_chunk, ! typesize_typesize. omega. + destruct d. congruence. right. rewrite ! size_type_chunk, ! typesize_typesize. lia. * (* overlapping locations *) destruct (Mem.valid_access_load m' (chunk_of_type ty0) sp (pos + 4 * ofs0)) as [v'' LOAD]. apply Mem.valid_access_implies with Writable; auto with mem. @@ -273,7 +273,7 @@ Proof. + apply (m_invar P) with m; auto. eapply Mem.store_unchanged_on; eauto. intros i; rewrite size_type_chunk, typesize_typesize. intros; red; intros. - eelim C; eauto. simpl. split; auto. omega. + eelim C; eauto. simpl. split; auto. lia. Qed. Lemma initial_locations: @@ -933,8 +933,8 @@ Local Opaque mreg_type. { unfold pos1. apply Z.divide_trans with sz. unfold sz; rewrite <- size_type_chunk. apply align_size_chunk_divides. apply align_divides; auto. } - apply range_drop_left with (mid := pos1) in SEP; [ | omega ]. - apply range_split with (mid := pos1 + sz) in SEP; [ | omega ]. + apply range_drop_left with (mid := pos1) in SEP; [ | lia ]. + apply range_split with (mid := pos1 + sz) in SEP; [ | lia ]. unfold sz at 1 in SEP. rewrite <- size_type_chunk in SEP. apply range_contains in SEP; auto. exploit (contains_set_stack (fun v' => Val.inject j (ls (R r)) v') (rs r)). @@ -1073,7 +1073,7 @@ Local Opaque b fe. instantiate (1 := fe_stack_data fe). tauto. reflexivity. instantiate (1 := fe_stack_data fe + bound_stack_data b). rewrite Z.max_comm. reflexivity. - generalize (bound_stack_data_pos b) size_no_overflow; omega. + generalize (bound_stack_data_pos b) size_no_overflow; lia. tauto. tauto. clear SEP. intros (j' & SEP & INCR & SAME). @@ -1607,7 +1607,7 @@ Proof. + simpl in SEP. unfold parent_sp. assert (slot_valid f Outgoing pos ty = true). { destruct H0. unfold slot_valid, proj_sumbool. - rewrite zle_true by omega. rewrite pred_dec_true by auto. reflexivity. } + rewrite zle_true by lia. rewrite pred_dec_true by auto. reflexivity. } assert (slot_within_bounds (function_bounds f) Outgoing pos ty) by eauto. exploit frame_get_outgoing; eauto. intros (v & A & B). exists v; split. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 9ec89553..7a5be5ed 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -47,11 +47,11 @@ Proof. intro f. assert (forall n pc, (return_measure_rec n f pc <= n)%nat). induction n; intros; simpl. - omega. - destruct (f!pc); try omega. - destruct i; try omega. - generalize (IHn n0). omega. - generalize (IHn n0). omega. + lia. + destruct (f!pc); try lia. + destruct i; try lia. + generalize (IHn n0). lia. + generalize (IHn n0). lia. intros. unfold return_measure. apply H. Qed. @@ -61,11 +61,11 @@ Remark return_measure_rec_incr: (return_measure_rec n1 f pc <= return_measure_rec n2 f pc)%nat. Proof. induction n1; intros; simpl. - omega. - destruct n2. omegaContradiction. assert (n1 <= n2)%nat by omega. - simpl. destruct f!pc; try omega. destruct i; try omega. - generalize (IHn1 n2 n H0). omega. - generalize (IHn1 n2 n H0). omega. + lia. + destruct n2. extlia. assert (n1 <= n2)%nat by lia. + simpl. destruct f!pc; try lia. destruct i; try lia. + generalize (IHn1 n2 n H0). lia. + generalize (IHn1 n2 n H0). lia. Qed. Lemma is_return_measure_rec: @@ -75,13 +75,13 @@ Lemma is_return_measure_rec: Proof. induction n; simpl; intros. congruence. - destruct n'. omegaContradiction. simpl. + destruct n'. extlia. simpl. destruct (fn_code f)!pc; try congruence. destruct i; try congruence. - decEq. apply IHn with r. auto. omega. + decEq. apply IHn with r. auto. lia. destruct (is_move_operation o l); try congruence. destruct (Reg.eq r r1); try congruence. - decEq. apply IHn with r0. auto. omega. + decEq. apply IHn with r0. auto. lia. Qed. (** ** Relational characterization of the code transformation *) @@ -117,22 +117,22 @@ Proof. generalize H. simpl. caseEq ((fn_code f)!pc); try congruence. intro i. caseEq i; try congruence. - intros s; intros. eapply is_return_nop; eauto. eapply IHn; eauto. omega. + intros s; intros. eapply is_return_nop; eauto. eapply IHn; eauto. lia. unfold return_measure. rewrite <- (is_return_measure_rec f (S n) niter pc rret); auto. rewrite <- (is_return_measure_rec f n niter s rret); auto. - simpl. rewrite H2. omega. omega. + simpl. rewrite H2. lia. lia. intros op args dst s EQ1 EQ2. caseEq (is_move_operation op args); try congruence. intros src IMO. destruct (Reg.eq rret src); try congruence. subst rret. intro. exploit is_move_operation_correct; eauto. intros [A B]. subst. - eapply is_return_move; eauto. eapply IHn; eauto. omega. + eapply is_return_move; eauto. eapply IHn; eauto. lia. unfold return_measure. rewrite <- (is_return_measure_rec f (S n) niter pc src); auto. rewrite <- (is_return_measure_rec f n niter s dst); auto. - simpl. rewrite EQ2. omega. omega. + simpl. rewrite EQ2. lia. lia. intros or EQ1 EQ2. destruct or; intros. assert (r = rret). eapply proj_sumbool_true; eauto. subst r. @@ -407,7 +407,7 @@ Proof. eapply exec_Inop; eauto. constructor; auto. - (* eliminated nop *) assert (s0 = pc') by congruence. subst s0. - right. split. simpl. omega. split. auto. + right. split. simpl. lia. split. auto. econstructor; eauto. - (* op *) @@ -421,7 +421,7 @@ Proof. econstructor; eauto. apply set_reg_lessdef; auto. - (* eliminated move *) rewrite H1 in H. clear H1. inv H. - right. split. simpl. omega. split. auto. + right. split. simpl. lia. split. auto. econstructor; eauto. simpl in H0. rewrite PMap.gss. congruence. - (* load *) @@ -455,13 +455,13 @@ Proof. + (* call turned tailcall *) assert ({ m'' | Mem.free m' sp0 0 (fn_stacksize (transf_function f)) = Some m''}). apply Mem.range_perm_free. rewrite stacksize_preserved. rewrite H7. - red; intros; omegaContradiction. + red; intros; extlia. destruct X as [m'' FREE]. left. exists (Callstate s' (transf_fundef fd) (rs'##args) m''); split. eapply exec_Itailcall; eauto. apply sig_preserved. constructor. eapply match_stackframes_tail; eauto. apply regs_lessdef_regs; auto. eapply Mem.free_right_extends; eauto. - rewrite stacksize_preserved. rewrite H7. intros. omegaContradiction. + rewrite stacksize_preserved. rewrite H7. intros. extlia. + (* call that remains a call *) left. exists (Callstate (Stackframe res (transf_function f) (Vptr sp0 Ptrofs.zero) pc' rs' :: s') (transf_fundef fd) (rs'##args) m'); split. @@ -514,22 +514,22 @@ Proof. - (* eliminated return None *) assert (or = None) by congruence. subst or. - right. split. simpl. omega. split. auto. + right. split. simpl. lia. split. auto. constructor. auto. simpl. constructor. eapply Mem.free_left_extends; eauto. - (* eliminated return Some *) assert (or = Some r) by congruence. subst or. - right. split. simpl. omega. split. auto. + right. split. simpl. lia. split. auto. constructor. auto. simpl. auto. eapply Mem.free_left_extends; eauto. - (* internal call *) exploit Mem.alloc_extends; eauto. - instantiate (1 := 0). omega. - instantiate (1 := fn_stacksize f). omega. + instantiate (1 := 0). lia. + instantiate (1 := fn_stacksize f). lia. intros [m'1 [ALLOC EXT]]. assert (fn_stacksize (transf_function f) = fn_stacksize f /\ fn_entrypoint (transf_function f) = fn_entrypoint f /\ @@ -559,7 +559,7 @@ Proof. right. split. unfold measure. simpl length. change (S (length s) * (niter + 2))%nat with ((niter + 2) + (length s) * (niter + 2))%nat. - generalize (return_measure_bounds (fn_code f) pc). omega. + generalize (return_measure_bounds (fn_code f) pc). lia. split. auto. econstructor; eauto. rewrite Regmap.gss. auto. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 4f95ac9b..c612995b 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -87,7 +87,7 @@ Proof. * (* The new instruction *) rewrite (U.repr_union_2 u pc s); auto. rewrite U.repr_union_3. unfold measure_edge. destruct (peq (U.repr u s) pc). auto. right. split. auto. - rewrite PC. rewrite peq_true. omega. + rewrite PC. rewrite peq_true. lia. * (* An old instruction *) assert (U.repr u pc' = pc' -> U.repr (U.union u pc s) pc' = pc'). @@ -96,7 +96,7 @@ Proof. intros [P | [P Q]]. left; auto. right. split. apply U.sameclass_union_2. auto. unfold measure_edge. destruct (peq (U.repr u s) pc). auto. - rewrite P. destruct (peq (U.repr u s0) pc). omega. auto. + rewrite P. destruct (peq (U.repr u s0) pc). lia. auto. Qed. Definition record_gotos' (f: function) := @@ -420,7 +420,7 @@ Proof. generalize (record_gotos_correct f pc). rewrite H. destruct bb; auto. destruct i; auto. intros [A | [B C]]. auto. - right. split. simpl. omega. + right. split. simpl. lia. split. auto. rewrite B. econstructor; eauto. @@ -487,7 +487,7 @@ Proof. eapply exec_Lbranch; eauto. fold (branch_target f pc). econstructor; eauto. - (* Lbranch (eliminated) *) - right; split. simpl. omega. split. auto. constructor; auto. + right; split. simpl. lia. split. auto. constructor; auto. - (* Lcond *) simpl tunneled_block. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 680daba7..3216ec50 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -982,7 +982,7 @@ Proof. intros. exploit G; eauto. intros [U V]. assert (Mem.valid_block m sp0) by (eapply Mem.valid_block_inject_1; eauto). assert (Mem.valid_block tm tsp) by (eapply Mem.valid_block_inject_2; eauto). - unfold Mem.valid_block in *; xomega. + unfold Mem.valid_block in *; extlia. apply set_res_inject; auto. apply regset_inject_incr with j; auto. - (* cond *) @@ -1036,7 +1036,7 @@ Proof. apply match_stacks_bound with (Mem.nextblock m) (Mem.nextblock tm). apply match_stacks_incr with j; auto. intros. exploit G; eauto. intros [P Q]. - unfold Mem.valid_block in *; xomega. + unfold Mem.valid_block in *; extlia. eapply external_call_nextblock; eauto. eapply external_call_nextblock; eauto. @@ -1063,7 +1063,7 @@ Proof. - apply IHl. unfold Genv.add_global, P; simpl. intros LT. apply Plt_succ_inv in LT. destruct LT. + rewrite PTree.gso. apply H; auto. apply Plt_ne; auto. + rewrite H0. rewrite PTree.gss. exists g1; auto. } - apply H. red; simpl; intros. exfalso; xomega. + apply H. red; simpl; intros. exfalso; extlia. Qed. *) @@ -1123,10 +1123,10 @@ Lemma Mem_getN_forall2: P (ZMap.get i c1) (ZMap.get i c2). Proof. induction n; simpl Mem.getN; intros. -- simpl in H1. omegaContradiction. +- simpl in H1. extlia. - inv H. rewrite Nat2Z.inj_succ in H1. destruct (zeq i p0). + congruence. -+ apply IHn with (p0 + 1); auto. omega. omega. ++ apply IHn with (p0 + 1); auto. lia. lia. Qed. Lemma init_mem_inj_1: @@ -1143,7 +1143,7 @@ Proof. + intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). apply Q1 in H0. destruct H0. subst. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. - apply P2. omega. + apply P2. lia. - exploit init_meminj_invert; eauto. intros (A & id & B & C). subst delta. apply Z.divide_0_r. - exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). @@ -1162,8 +1162,8 @@ Local Transparent Mem.loadbytes. rewrite Z.add_0_r. apply Mem_getN_forall2 with (p := 0) (n := Z.to_nat (init_data_list_size (gvar_init v))). rewrite H3, H4. apply bytes_of_init_inject. auto. - omega. - rewrite Z2Nat.id by (apply Z.ge_le; apply init_data_list_size_pos). omega. + lia. + rewrite Z2Nat.id by (apply Z.ge_le; apply init_data_list_size_pos). lia. Qed. Lemma init_mem_inj_2: @@ -1181,18 +1181,18 @@ Proof. exploit init_meminj_invert. eexact H1. intros (A2 & id2 & B2 & C2). destruct (ident_eq id1 id2). congruence. left; eapply Genv.global_addresses_distinct; eauto. - exploit init_meminj_invert; eauto. intros (A & id & B & C). subst delta. - split. omega. generalize (Ptrofs.unsigned_range_2 ofs). omega. + split. lia. generalize (Ptrofs.unsigned_range_2 ofs). lia. - exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). exploit (Genv.init_mem_characterization_gen p); eauto. exploit (Genv.init_mem_characterization_gen tp); eauto. destruct gd as [f|v]. + intros (P2 & Q2) (P1 & Q1). - apply Q2 in H0. destruct H0. subst. replace ofs with 0 by omega. + apply Q2 in H0. destruct H0. subst. replace ofs with 0 by lia. left; apply Mem.perm_cur; auto. + intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). apply Q2 in H0. destruct H0. subst. left. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. - apply P1. omega. + apply P1. lia. Qed. End INIT_MEM. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index b0ce019c..f7e4f0ed 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -544,8 +544,8 @@ Proof. eapply SM; auto. eapply mmatch_top; eauto. + (* below *) red; simpl; intros. rewrite NB. destruct (eq_block b sp). - subst b; rewrite SP; xomega. - exploit mmatch_below; eauto. xomega. + subst b; rewrite SP; extlia. + exploit mmatch_below; eauto. extlia. - (* unchanged *) simpl; intros. apply dec_eq_false. apply Plt_ne. auto. - (* values *) @@ -1147,11 +1147,11 @@ Proof. - constructor. - assert (Plt sp bound') by eauto with va. eapply sound_stack_public_call; eauto. apply IHsound_stack; intros. - apply INV. xomega. rewrite SAME; auto with ordered_type. xomega. auto. auto. + apply INV. extlia. rewrite SAME; auto with ordered_type. extlia. auto. auto. - assert (Plt sp bound') by eauto with va. eapply sound_stack_private_call; eauto. apply IHsound_stack; intros. - apply INV. xomega. rewrite SAME; auto with ordered_type. xomega. auto. auto. - apply bmatch_ext with m; auto. intros. apply INV. xomega. auto. auto. auto. + apply INV. extlia. rewrite SAME; auto with ordered_type. extlia. auto. auto. + apply bmatch_ext with m; auto. intros. apply INV. extlia. auto. auto. auto. Qed. Lemma sound_stack_inv: @@ -1210,8 +1210,8 @@ Lemma sound_stack_new_bound: Proof. intros. inv H. - constructor. -- eapply sound_stack_public_call with (bound' := bound'0); eauto. xomega. -- eapply sound_stack_private_call with (bound' := bound'0); eauto. xomega. +- eapply sound_stack_public_call with (bound' := bound'0); eauto. extlia. +- eapply sound_stack_private_call with (bound' := bound'0); eauto. extlia. Qed. Lemma sound_stack_exten: @@ -1224,12 +1224,12 @@ Proof. - constructor. - assert (Plt sp bound') by eauto with va. eapply sound_stack_public_call; eauto. - rewrite H0; auto. xomega. - intros. rewrite H0; auto. xomega. + rewrite H0; auto. extlia. + intros. rewrite H0; auto. extlia. - assert (Plt sp bound') by eauto with va. eapply sound_stack_private_call; eauto. - rewrite H0; auto. xomega. - intros. rewrite H0; auto. xomega. + rewrite H0; auto. extlia. + intros. rewrite H0; auto. extlia. Qed. (** ** Preservation of the semantic invariant by one step of execution *) diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index c132ce7c..45894bfc 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -45,10 +45,10 @@ Qed. Hint Extern 2 (_ = _) => congruence : va. Hint Extern 2 (_ <> _) => congruence : va. -Hint Extern 2 (_ < _) => xomega : va. -Hint Extern 2 (_ <= _) => xomega : va. -Hint Extern 2 (_ > _) => xomega : va. -Hint Extern 2 (_ >= _) => xomega : va. +Hint Extern 2 (_ < _) => extlia : va. +Hint Extern 2 (_ <= _) => extlia : va. +Hint Extern 2 (_ > _) => extlia : va. +Hint Extern 2 (_ >= _) => extlia : va. Section MATCH. @@ -595,17 +595,17 @@ Hint Extern 1 (vmatch _ _) => constructor : va. Lemma is_uns_mon: forall n1 n2 i, is_uns n1 i -> n1 <= n2 -> is_uns n2 i. Proof. - intros; red; intros. apply H; omega. + intros; red; intros. apply H; lia. Qed. Lemma is_sgn_mon: forall n1 n2 i, is_sgn n1 i -> n1 <= n2 -> is_sgn n2 i. Proof. - intros; red; intros. apply H; omega. + intros; red; intros. apply H; lia. Qed. Lemma is_uns_sgn: forall n1 n2 i, is_uns n1 i -> n1 < n2 -> is_sgn n2 i. Proof. - intros; red; intros. rewrite ! H by omega. auto. + intros; red; intros. rewrite ! H by lia. auto. Qed. Definition usize := Int.size. @@ -616,7 +616,7 @@ Lemma is_uns_usize: forall i, is_uns (usize i) i. Proof. unfold usize; intros; red; intros. - apply Int.bits_size_2. omega. + apply Int.bits_size_2. lia. Qed. Lemma is_sgn_ssize: @@ -628,10 +628,10 @@ Proof. rewrite <- (negb_involutive (Int.testbit i (Int.zwordsize - 1))). f_equal. generalize (Int.size_range (Int.not i)); intros RANGE. - rewrite <- ! Int.bits_not by omega. - rewrite ! Int.bits_size_2 by omega. + rewrite <- ! Int.bits_not by lia. + rewrite ! Int.bits_size_2 by lia. auto. -- rewrite ! Int.bits_size_2 by omega. +- rewrite ! Int.bits_size_2 by lia. auto. Qed. @@ -639,8 +639,8 @@ Lemma is_uns_zero_ext: forall n i, is_uns n i <-> Int.zero_ext n i = i. Proof. intros; split; intros. - Int.bit_solve. destruct (zlt i0 n); auto. symmetry; apply H; auto. omega. - rewrite <- H. red; intros. rewrite Int.bits_zero_ext by omega. rewrite zlt_false by omega. auto. + Int.bit_solve. destruct (zlt i0 n); auto. symmetry; apply H; auto. lia. + rewrite <- H. red; intros. rewrite Int.bits_zero_ext by lia. rewrite zlt_false by lia. auto. Qed. Lemma is_sgn_sign_ext: @@ -649,18 +649,18 @@ Proof. intros; split; intros. Int.bit_solve. destruct (zlt i0 n); auto. transitivity (Int.testbit i (Int.zwordsize - 1)). - apply H0; omega. symmetry; apply H0; omega. - rewrite <- H0. red; intros. rewrite ! Int.bits_sign_ext by omega. - f_equal. transitivity (n-1). destruct (zlt m n); omega. - destruct (zlt (Int.zwordsize - 1) n); omega. + apply H0; lia. symmetry; apply H0; lia. + rewrite <- H0. red; intros. rewrite ! Int.bits_sign_ext by lia. + f_equal. transitivity (n-1). destruct (zlt m n); lia. + destruct (zlt (Int.zwordsize - 1) n); lia. Qed. Lemma is_zero_ext_uns: forall i n m, is_uns m i \/ n <= m -> is_uns m (Int.zero_ext n i). Proof. - intros. red; intros. rewrite Int.bits_zero_ext by omega. - destruct (zlt m0 n); auto. destruct H. apply H; omega. omegaContradiction. + intros. red; intros. rewrite Int.bits_zero_ext by lia. + destruct (zlt m0 n); auto. destruct H. apply H; lia. extlia. Qed. Lemma is_zero_ext_sgn: @@ -668,9 +668,9 @@ Lemma is_zero_ext_sgn: n < m -> is_sgn m (Int.zero_ext n i). Proof. - intros. red; intros. rewrite ! Int.bits_zero_ext by omega. - transitivity false. apply zlt_false; omega. - symmetry; apply zlt_false; omega. + intros. red; intros. rewrite ! Int.bits_zero_ext by lia. + transitivity false. apply zlt_false; lia. + symmetry; apply zlt_false; lia. Qed. Lemma is_sign_ext_uns: @@ -679,8 +679,8 @@ Lemma is_sign_ext_uns: is_uns m i -> is_uns m (Int.sign_ext n i). Proof. - intros; red; intros. rewrite Int.bits_sign_ext by omega. - apply H0. destruct (zlt m0 n); omega. destruct (zlt m0 n); omega. + intros; red; intros. rewrite Int.bits_sign_ext by lia. + apply H0. destruct (zlt m0 n); lia. destruct (zlt m0 n); lia. Qed. Lemma is_sign_ext_sgn: @@ -690,9 +690,9 @@ Lemma is_sign_ext_sgn: Proof. intros. apply is_sgn_sign_ext; auto. destruct (zlt m n). destruct H1. apply is_sgn_sign_ext in H1; auto. - rewrite <- H1. rewrite (Int.sign_ext_widen i) by omega. apply Int.sign_ext_idem; auto. - omegaContradiction. - apply Int.sign_ext_widen; omega. + rewrite <- H1. rewrite (Int.sign_ext_widen i) by lia. apply Int.sign_ext_idem; auto. + extlia. + apply Int.sign_ext_widen; lia. Qed. Hint Resolve is_uns_mon is_sgn_mon is_uns_sgn is_uns_usize is_sgn_ssize : va. @@ -701,8 +701,8 @@ Lemma is_uns_1: forall n, is_uns 1 n -> n = Int.zero \/ n = Int.one. Proof. intros. destruct (Int.testbit n 0) eqn:B0; [right|left]; apply Int.same_bits_eq; intros. - rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; omega. - rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; omega. + rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; lia. + rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; lia. Qed. (** Tracking leakage of pointers through arithmetic operations. @@ -958,13 +958,13 @@ Hint Resolve vge_uns_uns' vge_uns_i' vge_sgn_sgn' vge_sgn_i' : va. Lemma usize_pos: forall n, 0 <= usize n. Proof. - unfold usize; intros. generalize (Int.size_range n); omega. + unfold usize; intros. generalize (Int.size_range n); lia. Qed. Lemma ssize_pos: forall n, 0 < ssize n. Proof. unfold ssize; intros. - generalize (Int.size_range (if Int.lt n Int.zero then Int.not n else n)); omega. + generalize (Int.size_range (if Int.lt n Int.zero then Int.not n else n)); lia. Qed. Lemma vge_lub_l: @@ -975,12 +975,12 @@ Proof. unfold vlub; destruct x, y; eauto using pge_lub_l with va. - predSpec Int.eq Int.eq_spec n n0. auto with va. destruct (Int.lt n Int.zero || Int.lt n0 Int.zero). - apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. - apply vge_uns_i'. generalize (usize_pos n); xomega. eauto with va. + apply vge_sgn_i'. generalize (ssize_pos n); extlia. eauto with va. + apply vge_uns_i'. generalize (usize_pos n); extlia. eauto with va. - destruct (Int.lt n Int.zero). - apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. - apply vge_uns_i'. generalize (usize_pos n); xomega. eauto with va. -- apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. + apply vge_sgn_i'. generalize (ssize_pos n); extlia. eauto with va. + apply vge_uns_i'. generalize (usize_pos n); extlia. eauto with va. +- apply vge_sgn_i'. generalize (ssize_pos n); extlia. eauto with va. - destruct (Int.lt n0 Int.zero). eapply vge_trans. apply vge_sgn_sgn'. apply vge_trans with (Sgn p (n + 1)); eauto with va. @@ -1269,12 +1269,12 @@ Proof. destruct (Int.ltu n Int.iwordsize) eqn:LTU; auto. exploit Int.ltu_inv; eauto. intros RANGE. inv H; auto with va. -- apply vmatch_uns'. red; intros. rewrite Int.bits_shl by omega. - destruct (zlt m (Int.unsigned n)). auto. apply H1; xomega. +- apply vmatch_uns'. red; intros. rewrite Int.bits_shl by lia. + destruct (zlt m (Int.unsigned n)). auto. apply H1; extlia. - apply vmatch_sgn'. red; intros. zify. - rewrite ! Int.bits_shl by omega. - rewrite ! zlt_false by omega. - rewrite H1 by omega. symmetry. rewrite H1 by omega. auto. + rewrite ! Int.bits_shl by lia. + rewrite ! zlt_false by lia. + rewrite H1 by lia. symmetry. rewrite H1 by lia. auto. - destruct v; constructor. Qed. @@ -1306,13 +1306,13 @@ Proof. assert (DEFAULT2: forall i, vmatch (Vint (Int.shru i n)) (uns (provenance x) (Int.zwordsize - Int.unsigned n))). { intros. apply vmatch_uns. red; intros. - rewrite Int.bits_shru by omega. apply zlt_false. omega. + rewrite Int.bits_shru by lia. apply zlt_false. lia. } inv H; auto with va. - apply vmatch_uns'. red; intros. zify. - rewrite Int.bits_shru by omega. + rewrite Int.bits_shru by lia. destruct (zlt (m + Int.unsigned n) Int.zwordsize); auto. - apply H1; omega. + apply H1; lia. - destruct v; constructor. Qed. @@ -1345,22 +1345,22 @@ Proof. assert (DEFAULT2: forall i, vmatch (Vint (Int.shr i n)) (sgn (provenance x) (Int.zwordsize - Int.unsigned n))). { intros. apply vmatch_sgn. red; intros. - rewrite ! Int.bits_shr by omega. f_equal. + rewrite ! Int.bits_shr by lia. f_equal. destruct (zlt (m + Int.unsigned n) Int.zwordsize); destruct (zlt (Int.zwordsize - 1 + Int.unsigned n) Int.zwordsize); - omega. + lia. } assert (SGN: forall q i p, is_sgn p i -> 0 < p -> vmatch (Vint (Int.shr i n)) (sgn q (p - Int.unsigned n))). { intros. apply vmatch_sgn'. red; intros. zify. - rewrite ! Int.bits_shr by omega. + rewrite ! Int.bits_shr by lia. transitivity (Int.testbit i (Int.zwordsize - 1)). destruct (zlt (m + Int.unsigned n) Int.zwordsize). - apply H0; omega. + apply H0; lia. auto. symmetry. destruct (zlt (Int.zwordsize - 1 + Int.unsigned n) Int.zwordsize). - apply H0; omega. + apply H0; lia. auto. } inv H; eauto with va. @@ -1418,12 +1418,12 @@ Proof. assert (UNS: forall i j n m, is_uns n i -> is_uns m j -> is_uns (Z.max n m) (Int.or i j)). { intros; red; intros. rewrite Int.bits_or by auto. - rewrite H by xomega. rewrite H0 by xomega. auto. + rewrite H by extlia. rewrite H0 by extlia. auto. } assert (SGN: forall i j n m, is_sgn n i -> is_sgn m j -> is_sgn (Z.max n m) (Int.or i j)). { - intros; red; intros. rewrite ! Int.bits_or by xomega. - rewrite H by xomega. rewrite H0 by xomega. auto. + intros; red; intros. rewrite ! Int.bits_or by extlia. + rewrite H by extlia. rewrite H0 by extlia. auto. } intros. unfold or, Val.or; inv H; eauto with va; inv H0; eauto with va. Qed. @@ -1443,12 +1443,12 @@ Proof. assert (UNS: forall i j n m, is_uns n i -> is_uns m j -> is_uns (Z.max n m) (Int.xor i j)). { intros; red; intros. rewrite Int.bits_xor by auto. - rewrite H by xomega. rewrite H0 by xomega. auto. + rewrite H by extlia. rewrite H0 by extlia. auto. } assert (SGN: forall i j n m, is_sgn n i -> is_sgn m j -> is_sgn (Z.max n m) (Int.xor i j)). { - intros; red; intros. rewrite ! Int.bits_xor by xomega. - rewrite H by xomega. rewrite H0 by xomega. auto. + intros; red; intros. rewrite ! Int.bits_xor by extlia. + rewrite H by extlia. rewrite H0 by extlia. auto. } intros. unfold xor, Val.xor; inv H; eauto with va; inv H0; eauto with va. Qed. @@ -1466,7 +1466,7 @@ Lemma notint_sound: Proof. assert (SGN: forall n i, is_sgn n i -> is_sgn n (Int.not i)). { - intros; red; intros. rewrite ! Int.bits_not by omega. + intros; red; intros. rewrite ! Int.bits_not by lia. f_equal. apply H; auto. } intros. unfold Val.notint, notint; inv H; eauto with va. @@ -1492,13 +1492,13 @@ Proof. inv H; auto with va. - apply vmatch_uns. red; intros. rewrite Int.bits_rol by auto. generalize (Int.unsigned_range n); intros. - rewrite Z.mod_small by omega. - apply H1. omega. omega. + rewrite Z.mod_small by lia. + apply H1. lia. lia. - destruct (zlt n0 Int.zwordsize); auto with va. - apply vmatch_sgn. red; intros. rewrite ! Int.bits_rol by omega. + apply vmatch_sgn. red; intros. rewrite ! Int.bits_rol by lia. generalize (Int.unsigned_range n); intros. - rewrite ! Z.mod_small by omega. - rewrite H1 by omega. symmetry. rewrite H1 by omega. auto. + rewrite ! Z.mod_small by lia. + rewrite H1 by lia. symmetry. rewrite H1 by lia. auto. - destruct (zlt n0 Int.zwordsize); auto with va. Qed. @@ -1674,8 +1674,8 @@ Proof. generalize (Int.unsigned_range_2 j); intros RANGE. assert (Int.unsigned j <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. } - exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD. - unfold Int.modu. rewrite Int.unsigned_repr. omega. omega. + exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). lia. intros MOD. + unfold Int.modu. rewrite Int.unsigned_repr. lia. lia. } intros. destruct v; destruct w; try discriminate; simpl in H1. destruct (Int.eq i0 Int.zero) eqn:Z; inv H1. @@ -2084,12 +2084,12 @@ Lemma zero_ext_sound: Proof. assert (DFL: forall nbits i, is_uns nbits (Int.zero_ext nbits i)). { - intros; red; intros. rewrite Int.bits_zero_ext by omega. apply zlt_false; auto. + intros; red; intros. rewrite Int.bits_zero_ext by lia. apply zlt_false; auto. } intros. inv H; simpl; auto with va. apply vmatch_uns. red; intros. zify. - rewrite Int.bits_zero_ext by omega. - destruct (zlt m nbits); auto. apply H1; omega. + rewrite Int.bits_zero_ext by lia. + destruct (zlt m nbits); auto. apply H1; lia. Qed. Definition sign_ext (nbits: Z) (v: aval) := @@ -2109,7 +2109,7 @@ Proof. intros. apply vmatch_sgn. apply is_sign_ext_sgn; auto with va. } intros. unfold sign_ext. destruct (zle nbits 0). -- destruct v; simpl; auto with va. constructor. omega. +- destruct v; simpl; auto with va. constructor. lia. rewrite Int.sign_ext_below by auto. red; intros; apply Int.bits_zero. - inv H; simpl; auto with va. + destruct (zlt n nbits); eauto with va. @@ -2514,26 +2514,26 @@ Proof. intros c [lo hi] x n; simpl; intros R. destruct c; unfold zcmp, proj_sumbool. - (* eq *) - destruct (zlt n lo). rewrite zeq_false by omega. constructor. - destruct (zlt hi n). rewrite zeq_false by omega. constructor. + destruct (zlt n lo). rewrite zeq_false by lia. constructor. + destruct (zlt hi n). rewrite zeq_false by lia. constructor. constructor. - (* ne *) constructor. - (* lt *) - destruct (zlt hi n). rewrite zlt_true by omega. constructor. - destruct (zle n lo). rewrite zlt_false by omega. constructor. + destruct (zlt hi n). rewrite zlt_true by lia. constructor. + destruct (zle n lo). rewrite zlt_false by lia. constructor. constructor. - (* le *) - destruct (zle hi n). rewrite zle_true by omega. constructor. - destruct (zlt n lo). rewrite zle_false by omega. constructor. + destruct (zle hi n). rewrite zle_true by lia. constructor. + destruct (zlt n lo). rewrite zle_false by lia. constructor. constructor. - (* gt *) - destruct (zlt n lo). rewrite zlt_true by omega. constructor. - destruct (zle hi n). rewrite zlt_false by omega. constructor. + destruct (zlt n lo). rewrite zlt_true by lia. constructor. + destruct (zle hi n). rewrite zlt_false by lia. constructor. constructor. - (* ge *) - destruct (zle n lo). rewrite zle_true by omega. constructor. - destruct (zlt hi n). rewrite zle_false by omega. constructor. + destruct (zle n lo). rewrite zle_true by lia. constructor. + destruct (zlt hi n). rewrite zle_false by lia. constructor. constructor. Qed. @@ -2567,10 +2567,10 @@ Lemma uintv_sound: forall n v, vmatch (Vint n) v -> fst (uintv v) <= Int.unsigned n <= snd (uintv v). Proof. intros. inv H; simpl; try (apply Int.unsigned_range_2). -- omega. +- lia. - destruct (zlt n0 Int.zwordsize); simpl. -+ rewrite is_uns_zero_ext in H2. rewrite <- H2. rewrite Int.zero_ext_mod by omega. - exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. omega. ++ rewrite is_uns_zero_ext in H2. rewrite <- H2. rewrite Int.zero_ext_mod by lia. + exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. lia. + apply Int.unsigned_range_2. Qed. @@ -2582,8 +2582,8 @@ Proof. intros. simpl. replace (Int.cmpu c n1 n2) with (zcmp c (Int.unsigned n1) (Int.unsigned n2)). apply zcmp_intv_sound; apply uintv_sound; auto. destruct c; simpl; auto. - unfold Int.ltu. destruct (zle (Int.unsigned n1) (Int.unsigned n2)); [rewrite zlt_false|rewrite zlt_true]; auto; omega. - unfold Int.ltu. destruct (zle (Int.unsigned n2) (Int.unsigned n1)); [rewrite zlt_false|rewrite zlt_true]; auto; omega. + unfold Int.ltu. destruct (zle (Int.unsigned n1) (Int.unsigned n2)); [rewrite zlt_false|rewrite zlt_true]; auto; lia. + unfold Int.ltu. destruct (zle (Int.unsigned n2) (Int.unsigned n1)); [rewrite zlt_false|rewrite zlt_true]; auto; lia. Qed. Lemma cmpu_intv_sound_2: @@ -2610,22 +2610,22 @@ Lemma sintv_sound: forall n v, vmatch (Vint n) v -> fst (sintv v) <= Int.signed n <= snd (sintv v). Proof. intros. inv H; simpl; try (apply Int.signed_range). -- omega. +- lia. - destruct (zlt n0 Int.zwordsize); simpl. + rewrite is_uns_zero_ext in H2. rewrite <- H2. - assert (Int.unsigned (Int.zero_ext n0 n) = Int.unsigned n mod two_p n0) by (apply Int.zero_ext_mod; omega). + assert (Int.unsigned (Int.zero_ext n0 n) = Int.unsigned n mod two_p n0) by (apply Int.zero_ext_mod; lia). exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. intros. replace (Int.signed (Int.zero_ext n0 n)) with (Int.unsigned (Int.zero_ext n0 n)). - rewrite H. omega. + rewrite H. lia. unfold Int.signed. rewrite zlt_true. auto. assert (two_p n0 <= Int.half_modulus). { change Int.half_modulus with (two_p (Int.zwordsize - 1)). - apply two_p_monotone. omega. } - omega. + apply two_p_monotone. lia. } + lia. + apply Int.signed_range. - destruct (zlt n0 (Int.zwordsize)); simpl. + rewrite is_sgn_sign_ext in H2 by auto. rewrite <- H2. - exploit (Int.sign_ext_range n0 n). omega. omega. + exploit (Int.sign_ext_range n0 n). lia. lia. + apply Int.signed_range. Qed. @@ -2637,8 +2637,8 @@ Proof. intros. simpl. replace (Int.cmp c n1 n2) with (zcmp c (Int.signed n1) (Int.signed n2)). apply zcmp_intv_sound; apply sintv_sound; auto. destruct c; simpl; rewrite ? Int.eq_signed; auto. - unfold Int.lt. destruct (zle (Int.signed n1) (Int.signed n2)); [rewrite zlt_false|rewrite zlt_true]; auto; omega. - unfold Int.lt. destruct (zle (Int.signed n2) (Int.signed n1)); [rewrite zlt_false|rewrite zlt_true]; auto; omega. + unfold Int.lt. destruct (zle (Int.signed n1) (Int.signed n2)); [rewrite zlt_false|rewrite zlt_true]; auto; lia. + unfold Int.lt. destruct (zle (Int.signed n2) (Int.signed n1)); [rewrite zlt_false|rewrite zlt_true]; auto; lia. Qed. Lemma cmp_intv_sound_2: @@ -2823,7 +2823,7 @@ Proof. assert (DEFAULT: vmatch (Val.of_optbool ob) (Uns Pbot 1)). { destruct ob; simpl; auto with va. - destruct b; constructor; try omega. + destruct b; constructor; try lia. change 1 with (usize Int.one). apply is_uns_usize. red; intros. apply Int.bits_zero. } @@ -2942,27 +2942,27 @@ Proof. - destruct (zlt n 8); constructor; auto with va. apply is_sign_ext_uns; auto. apply is_sign_ext_sgn; auto with va. -- constructor. xomega. apply is_zero_ext_uns. apply Z.min_case; auto with va. +- constructor. extlia. apply is_zero_ext_uns. apply Z.min_case; auto with va. - destruct (zlt n 16); constructor; auto with va. apply is_sign_ext_uns; auto. apply is_sign_ext_sgn; auto with va. -- constructor. xomega. apply is_zero_ext_uns. apply Z.min_case; auto with va. +- constructor. extlia. apply is_zero_ext_uns. apply Z.min_case; auto with va. - destruct (zlt n 8); auto with va. - destruct (zlt n 16); auto with va. -- constructor. xomega. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va. -- constructor. omega. apply is_zero_ext_uns; auto with va. -- constructor. xomega. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va. -- constructor. omega. apply is_zero_ext_uns; auto with va. +- constructor. extlia. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va. +- constructor. lia. apply is_zero_ext_uns; auto with va. +- constructor. extlia. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va. +- constructor. lia. apply is_zero_ext_uns; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. -- constructor. omega. apply is_sign_ext_sgn; auto with va. -- constructor. omega. apply is_zero_ext_uns; auto with va. -- constructor. omega. apply is_sign_ext_sgn; auto with va. -- constructor. omega. apply is_zero_ext_uns; auto with va. +- constructor. lia. apply is_sign_ext_sgn; auto with va. +- constructor. lia. apply is_zero_ext_uns; auto with va. +- constructor. lia. apply is_sign_ext_sgn; auto with va. +- constructor. lia. apply is_zero_ext_uns; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. @@ -2977,13 +2977,13 @@ Proof. intros. exploit Mem.load_cast; eauto. exploit Mem.load_type; eauto. destruct chunk; simpl; intros. - (* int8signed *) - rewrite H2. destruct v; simpl; constructor. omega. apply is_sign_ext_sgn; auto with va. + rewrite H2. destruct v; simpl; constructor. lia. apply is_sign_ext_sgn; auto with va. - (* int8unsigned *) - rewrite H2. destruct v; simpl; constructor. omega. apply is_zero_ext_uns; auto with va. + rewrite H2. destruct v; simpl; constructor. lia. apply is_zero_ext_uns; auto with va. - (* int16signed *) - rewrite H2. destruct v; simpl; constructor. omega. apply is_sign_ext_sgn; auto with va. + rewrite H2. destruct v; simpl; constructor. lia. apply is_sign_ext_sgn; auto with va. - (* int16unsigned *) - rewrite H2. destruct v; simpl; constructor. omega. apply is_zero_ext_uns; auto with va. + rewrite H2. destruct v; simpl; constructor. lia. apply is_zero_ext_uns; auto with va. - (* int32 *) auto. - (* int64 *) @@ -3025,9 +3025,9 @@ Proof with (auto using provenance_monotone with va). apply is_sign_ext_sgn... - constructor... apply is_zero_ext_uns... apply Z.min_case... - unfold provenance; destruct (va_strict tt)... -- destruct (zlt n1 8). rewrite zlt_true by omega... +- destruct (zlt n1 8). rewrite zlt_true by lia... destruct (zlt n2 8)... -- destruct (zlt n1 16). rewrite zlt_true by omega... +- destruct (zlt n1 16). rewrite zlt_true by lia... destruct (zlt n2 16)... - constructor... apply is_sign_ext_sgn... apply Z.min_case... - constructor... apply is_zero_ext_uns... @@ -3148,7 +3148,7 @@ Function inval_after (lo: Z) (hi: Z) (c: ZTree.t acontent) { wf (Zwf lo) hi } : then inval_after lo (hi - 1) (ZTree.remove hi c) else c. Proof. - intros; red; omega. + intros; red; lia. apply Zwf_well_founded. Qed. @@ -3163,7 +3163,7 @@ Function inval_before (hi: Z) (lo: Z) (c: ZTree.t acontent) { wf (Zwf_up hi) lo then inval_before hi (lo + 1) (inval_if hi lo c) else c. Proof. - intros; red; omega. + intros; red; lia. apply Zwf_up_well_founded. Qed. @@ -3201,7 +3201,7 @@ Remark loadbytes_load_ext: Proof. intros. exploit Mem.load_loadbytes; eauto. intros [bytes [A B]]. exploit Mem.load_valid_access; eauto. intros [C D]. - subst v. apply Mem.loadbytes_load; auto. apply H; auto. generalize (size_chunk_pos chunk); omega. + subst v. apply Mem.loadbytes_load; auto. apply H; auto. generalize (size_chunk_pos chunk); lia. Qed. Lemma smatch_ext: @@ -3212,7 +3212,7 @@ Lemma smatch_ext: Proof. intros. destruct H. split; intros. eapply H; eauto. eapply loadbytes_load_ext; eauto. - eapply H1; eauto. apply H0; eauto. omega. + eapply H1; eauto. apply H0; eauto. lia. Qed. Lemma smatch_inv: @@ -3247,19 +3247,19 @@ Proof. + rewrite (Mem.loadbytes_empty m b ofs sz) in LOAD by auto. inv LOAD. contradiction. + exploit (Mem.loadbytes_split m b ofs 1 (sz - 1) bytes). - replace (1 + (sz - 1)) with sz by omega. auto. - omega. - omega. + replace (1 + (sz - 1)) with sz by lia. auto. + lia. + lia. intros (bytes1 & bytes2 & LOAD1 & LOAD2 & CONCAT). subst bytes. exploit Mem.loadbytes_length. eexact LOAD1. change (Z.to_nat 1) with 1%nat. intros LENGTH1. rewrite in_app_iff in IN. destruct IN. * destruct bytes1; try discriminate. destruct bytes1; try discriminate. simpl in H. destruct H; try contradiction. subst m0. - exists ofs; split. omega. auto. - * exploit (REC (sz - 1)). red; omega. eexact LOAD2. auto. + exists ofs; split. lia. auto. + * exploit (REC (sz - 1)). red; lia. eexact LOAD2. auto. intros (ofs' & A & B). - exists ofs'; split. omega. auto. + exists ofs'; split. lia. auto. Qed. Lemma smatch_loadbytes: @@ -3285,13 +3285,13 @@ Proof. - apply Zwf_well_founded. - intros sz REC ofs bytes LOAD LOAD1 IN. exploit (Mem.loadbytes_split m b ofs 1 (sz - 1) bytes). - replace (1 + (sz - 1)) with sz by omega. auto. - omega. - omega. + replace (1 + (sz - 1)) with sz by lia. auto. + lia. + lia. intros (bytes1 & bytes2 & LOAD3 & LOAD4 & CONCAT). subst bytes. rewrite in_app_iff. destruct (zeq ofs ofs'). + subst ofs'. rewrite LOAD1 in LOAD3; inv LOAD3. left; simpl; auto. -+ right. eapply (REC (sz - 1)). red; omega. eexact LOAD4. auto. omega. ++ right. eapply (REC (sz - 1)). red; lia. eexact LOAD4. auto. lia. Qed. Lemma storebytes_provenance: @@ -3309,10 +3309,10 @@ Proof. destruct (eq_block b' b); auto. destruct (zle (ofs' + 1) ofs); auto. destruct (zle (ofs + Z.of_nat (length bytes)) ofs'); auto. - right. split. auto. omega. + right. split. auto. lia. } destruct EITHER as [A | (A & B)]. -- right. rewrite <- H0. symmetry. eapply Mem.loadbytes_storebytes_other; eauto. omega. +- right. rewrite <- H0. symmetry. eapply Mem.loadbytes_storebytes_other; eauto. lia. - subst b'. left. eapply loadbytes_provenance; eauto. eapply Mem.loadbytes_storebytes_same; eauto. @@ -3457,7 +3457,7 @@ Remark inval_after_outside: forall i lo hi c, i < lo \/ i > hi -> (inval_after lo hi c)##i = c##i. Proof. intros until c. functional induction (inval_after lo hi c); intros. - rewrite IHt by omega. apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; omega. + rewrite IHt by lia. apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; lia. auto. Qed. @@ -3468,18 +3468,18 @@ Remark inval_after_contents: Proof. intros until c. functional induction (inval_after lo hi c); intros. destruct (zeq i hi). - subst i. rewrite inval_after_outside in H by omega. rewrite ZTree.grs in H. discriminate. - exploit IHt; eauto. intros [A B]. rewrite ZTree.gro in A by auto. split. auto. omega. - split. auto. omega. + subst i. rewrite inval_after_outside in H by lia. rewrite ZTree.grs in H. discriminate. + exploit IHt; eauto. intros [A B]. rewrite ZTree.gro in A by auto. split. auto. lia. + split. auto. lia. Qed. Remark inval_before_outside: forall i hi lo c, i < lo \/ i >= hi -> (inval_before hi lo c)##i = c##i. Proof. intros until c. functional induction (inval_before hi lo c); intros. - rewrite IHt by omega. unfold inval_if. destruct (c##lo) as [[chunk av]|]; auto. + rewrite IHt by lia. unfold inval_if. destruct (c##lo) as [[chunk av]|]; auto. destruct (zle (lo + size_chunk chunk) hi); auto. - apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; omega. + apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; lia. auto. Qed. @@ -3490,21 +3490,21 @@ Remark inval_before_contents_1: Proof. intros until c. functional induction (inval_before hi lo c); intros. - destruct (zeq lo i). -+ subst i. rewrite inval_before_outside in H0 by omega. ++ subst i. rewrite inval_before_outside in H0 by lia. unfold inval_if in H0. destruct (c##lo) as [[chunk0 v0]|] eqn:C; try congruence. destruct (zle (lo + size_chunk chunk0) hi). rewrite C in H0; inv H0. auto. rewrite ZTree.grs in H0. congruence. -+ exploit IHt. omega. auto. intros [A B]; split; auto. ++ exploit IHt. lia. auto. intros [A B]; split; auto. unfold inval_if in A. destruct (c##lo) as [[chunk0 v0]|] eqn:C; auto. destruct (zle (lo + size_chunk chunk0) hi); auto. rewrite ZTree.gro in A; auto. -- omegaContradiction. +- extlia. Qed. Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8. Proof. - destruct chunk; simpl; omega. + destruct chunk; simpl; lia. Qed. Remark inval_before_contents: @@ -3513,12 +3513,12 @@ Remark inval_before_contents: c##j = Some (ACval chunk' av') /\ (j + size_chunk chunk' <= i \/ i <= j). Proof. intros. destruct (zlt j (i - 7)). - rewrite inval_before_outside in H by omega. - split. auto. left. generalize (max_size_chunk chunk'); omega. + rewrite inval_before_outside in H by lia. + split. auto. left. generalize (max_size_chunk chunk'); lia. destruct (zlt j i). - exploit inval_before_contents_1; eauto. omega. tauto. - rewrite inval_before_outside in H by omega. - split. auto. omega. + exploit inval_before_contents_1; eauto. lia. tauto. + rewrite inval_before_outside in H by lia. + split. auto. lia. Qed. Lemma ablock_store_contents: @@ -3534,7 +3534,7 @@ Proof. right. rewrite ZTree.gso in H by auto. exploit inval_before_contents; eauto. intros [A B]. exploit inval_after_contents; eauto. intros [C D]. - split. auto. omega. + split. auto. lia. Qed. Lemma chunk_compat_true: @@ -3604,7 +3604,7 @@ Proof. unfold ablock_storebytes; simpl; intros. exploit inval_before_contents; eauto. clear H. intros [A B]. exploit inval_after_contents; eauto. clear A. intros [C D]. - split. auto. xomega. + split. auto. extlia. Qed. Lemma ablock_storebytes_sound: @@ -3627,7 +3627,7 @@ Proof. exploit ablock_storebytes_contents; eauto. intros [A B]. assert (Mem.load chunk' m b ofs' = Some v'). { rewrite <- LOAD'; symmetry. eapply Mem.load_storebytes_other; eauto. - rewrite U. rewrite LENGTH. rewrite Z_to_nat_max. right; omega. } + rewrite U. rewrite LENGTH. rewrite Z_to_nat_max. right; lia. } exploit BM2; eauto. unfold ablock_load. rewrite A. rewrite COMPAT. auto. Qed. @@ -3755,7 +3755,7 @@ Proof. apply bmatch_inv with m; auto. + intros. eapply Mem.loadbytes_store_other; eauto. left. red; intros; subst b0. elim (C ofs). apply Mem.perm_cur_max. - apply P. generalize (size_chunk_pos chunk); omega. + apply P. generalize (size_chunk_pos chunk); lia. - intros; red; intros; elim (C ofs0). eauto with mem. Qed. @@ -4184,7 +4184,7 @@ Proof. - apply bmatch_ext with m; eauto with va. - apply smatch_ext with m; auto with va. - apply smatch_ext with m; auto with va. -- red; intros. exploit mmatch_below0; eauto. xomega. +- red; intros. exploit mmatch_below0; eauto. extlia. Qed. Lemma mmatch_free: @@ -4195,7 +4195,7 @@ Lemma mmatch_free: Proof. intros. apply mmatch_ext with m; auto. intros. eapply Mem.loadbytes_free_2; eauto. - erewrite <- Mem.nextblock_free by eauto. xomega. + erewrite <- Mem.nextblock_free by eauto. extlia. Qed. Lemma mmatch_top': @@ -4419,7 +4419,7 @@ Proof. { Local Transparent Mem.loadbytes. unfold Mem.loadbytes. rewrite pred_dec_true. reflexivity. - red; intros. replace ofs0 with ofs by omega. auto. + red; intros. replace ofs0 with ofs by lia. auto. } destruct mv; econstructor. destruct v; econstructor. apply inj_of_bc_valid. @@ -4440,7 +4440,7 @@ Proof. auto. - (* overflow *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - rewrite Z.add_0_r. split. omega. apply Ptrofs.unsigned_range_2. + rewrite Z.add_0_r. split. lia. apply Ptrofs.unsigned_range_2. - (* perm inv *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. rewrite Z.add_0_r in H2. auto. -- cgit From e16f5d1de08bb0c3ac561c2ea6a98f49ed8f49d5 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 15 Dec 2020 11:13:11 +0100 Subject: Revised correctness proof for record_goto We used to define an instrumented version record_goto' that also builds the measure f, prove it correct, then show equivalence with record_goto. The new proofs make do without the instrumented version. They prove strong existence of the measure, as in `{ f | branch_map_correct (record_goto fn) f}`. --- backend/Tunnelingproof.v | 97 +++++++++++++++--------------------------------- 1 file changed, 29 insertions(+), 68 deletions(-) (limited to 'backend') diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index c612995b..d514c16f 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -29,96 +29,59 @@ Qed. (** * Properties of the branch map computed using union-find. *) -(** A variant of [record_goto] that also incrementally computes a measure [f: node -> nat] - counting the number of [Lnop] instructions starting at a given [pc] that were eliminated. *) - Definition measure_edge (u: U.t) (pc s: node) (f: node -> nat) : node -> nat := fun x => if peq (U.repr u s) pc then f x else if peq (U.repr u x) pc then (f x + f s + 1)%nat else f x. -Definition record_goto' (uf: U.t * (node -> nat)) (pc: node) (b: bblock) : U.t * (node -> nat) := - match b with - | Lbranch s :: b' => let (u, f) := uf in (U.union u pc s, measure_edge u pc s f) - | _ => uf - end. - -Definition branch_map_correct (c: code) (uf: U.t * (node -> nat)): Prop := +Definition branch_map_correct (c: code) (u: U.t) (f: node -> nat): Prop := forall pc, match c!pc with | Some(Lbranch s :: b) => - U.repr (fst uf) pc = pc \/ (U.repr (fst uf) pc = U.repr (fst uf) s /\ snd uf s < snd uf pc)%nat + U.repr u pc = pc \/ (U.repr u pc = U.repr u s /\ f s < f pc)%nat | _ => - U.repr (fst uf) pc = pc + U.repr u pc = pc end. -Lemma record_gotos'_correct: - forall c, - branch_map_correct c (PTree.fold record_goto' c (U.empty, fun (x: node) => O)). +Lemma record_gotos_correct_1: + forall fn, { f | branch_map_correct fn.(fn_code) (record_gotos fn) f }. Proof. intros. - apply PTree_Properties.fold_rec with (P := fun c uf => branch_map_correct c uf). - -- (* extensionality *) - intros. red; intros. rewrite <- H. apply H0. + unfold record_gotos. apply PTree_Properties.fold_ind. - (* base case *) - red; intros; simpl. rewrite PTree.gempty. apply U.repr_empty. + intros m EMPTY. exists (fun _ => O). + red; intros. rewrite EMPTY. apply U.repr_empty. - (* inductive case *) - intros m uf pc bb; intros. destruct uf as [u f]. + intros m u pc bb GET1 GET2 [f BMC]. assert (PC: U.repr u pc = pc). - generalize (H1 pc). rewrite H. auto. - assert (record_goto' (u, f) pc bb = (u, f) - \/ exists s, exists bb', bb = Lbranch s :: bb' /\ record_goto' (u, f) pc bb = (U.union u pc s, measure_edge u pc s f)). - unfold record_goto'; simpl. destruct bb; auto. destruct i; auto. right. exists s; exists bb; auto. - destruct H2 as [B | [s [bb' [EQ B]]]]. - -+ (* u and f are unchanged *) - rewrite B. - red. intro pc'. simpl. rewrite PTree.gsspec. destruct (peq pc' pc). subst pc'. - destruct bb; auto. destruct i; auto. - apply H1. - -+ (* b is Lbranch s, u becomes union u pc s, f becomes measure_edge u pc s f *) - rewrite B. - red. intro pc'. simpl. rewrite PTree.gsspec. destruct (peq pc' pc). subst pc'. rewrite EQ. - -* (* The new instruction *) + { specialize (BMC pc). rewrite PTree.grs in BMC. auto. } + assert (DFL: { f | branch_map_correct m u f }). + { exists f. intros p. destruct (peq p pc). + - subst p. rewrite GET1. destruct bb as [ | [] bb ]; auto. + - specialize (BMC p). rewrite PTree.gro in BMC by auto. exact BMC. + } + unfold record_goto. destruct bb as [ | [] bb ]; auto. + exists (measure_edge u pc s f). intros p. destruct (peq p pc). ++ subst p. rewrite GET1. unfold measure_edge. rewrite (U.repr_union_2 u pc s); auto. rewrite U.repr_union_3. - unfold measure_edge. destruct (peq (U.repr u s) pc). auto. right. split. auto. - rewrite PC. rewrite peq_true. lia. - -* (* An old instruction *) - assert (U.repr u pc' = pc' -> U.repr (U.union u pc s) pc' = pc'). - { intro. rewrite <- H2 at 2. apply U.repr_union_1. congruence. } - generalize (H1 pc'). simpl. destruct (m!pc'); auto. destruct b; auto. destruct i; auto. - intros [P | [P Q]]. left; auto. right. - split. apply U.sameclass_union_2. auto. + destruct (peq (U.repr u s) pc); auto. rewrite PC, peq_true. right; split; auto. lia. ++ specialize (BMC p). rewrite PTree.gro in BMC by auto. + assert (U.repr u p = p -> U.repr (U.union u pc s) p = p). + { intro. rewrite <- H at 2. apply U.repr_union_1. congruence. } + destruct (m!p) as [ [ | [] b ] | ]; auto. + destruct BMC as [A | [A B]]. auto. + right; split. apply U.sameclass_union_2; auto. unfold measure_edge. destruct (peq (U.repr u s) pc). auto. - rewrite P. destruct (peq (U.repr u s0) pc). lia. auto. -Qed. - -Definition record_gotos' (f: function) := - PTree.fold record_goto' f.(fn_code) (U.empty, fun (x: node) => O). - -Lemma record_gotos_gotos': - forall f, fst (record_gotos' f) = record_gotos f. -Proof. - intros. unfold record_gotos', record_gotos. - repeat rewrite PTree.fold_spec. - generalize (PTree.elements (fn_code f)) (U.empty) (fun _ : node => O). - induction l; intros; simpl. - auto. - unfold record_goto' at 2. unfold record_goto at 2. - destruct (snd a). apply IHl. destruct i; apply IHl. + rewrite A. destruct (peq (U.repr u s0) pc); lia. Qed. Definition branch_target (f: function) (pc: node) : node := U.repr (record_gotos f) pc. Definition count_gotos (f: function) (pc: node) : nat := - snd (record_gotos' f) pc. + proj1_sig (record_gotos_correct_1 f) pc. Theorem record_gotos_correct: forall f pc, @@ -129,10 +92,8 @@ Theorem record_gotos_correct: | _ => branch_target f pc = pc end. Proof. - intros. - generalize (record_gotos'_correct f.(fn_code) pc). simpl. - fold (record_gotos' f). unfold branch_map_correct, branch_target, count_gotos. - rewrite record_gotos_gotos'. auto. + intros. unfold count_gotos. destruct (record_gotos_correct_1 f) as [m P]; simpl. + apply P. Qed. (** * Preservation of semantics *) -- cgit From 7f152e2f27d82f0d502ee919e1576edefcd44cf5 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 15 Dec 2020 19:29:29 +0100 Subject: Improve branch tunneling The previous branch tunneling was missing optimization opportunities introduced by the optimization of conditional branches. For example: L1: instr; branch L2 L2: if cond then branch L3 else branch L4 L3: branch L4 L4: ... was transformed into L1: instr; branch L2 L2: branch L4 L3: branch L4 L4: ... missing a tunneling opportunity (branch L2 -> branch L4). This commit improves branch tunneling so that the expected code is produced: L1: instr; branch L4 L2: branch L4 L3: branch L4 L4: ... To this end, additional equalities are introduced in the union-find data structure corresponding to optimizable conditional branches. In rare cases these additional equalities trigger new opportunities for optimizing conditional branches. Hence we iterate the analysis until no optimizable conditional branch remains. --- backend/Tunneling.v | 135 ++++++++++++++++++++----- backend/Tunnelingproof.v | 253 ++++++++++++++++++++++++++++++++++++++++------- 2 files changed, 328 insertions(+), 60 deletions(-) (limited to 'backend') diff --git a/backend/Tunneling.v b/backend/Tunneling.v index da1ce45a..265e06ba 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -12,6 +12,7 @@ (** Branch tunneling (optimization of branches to branches). *) +Require Import FunInd. Require Import Coqlib Maps UnionFind. Require Import AST. Require Import LTL. @@ -21,8 +22,8 @@ Require Import LTL. so that they jump directly to the end of the branch sequence. For example: << - L1: nop L2; L1: nop L3; - L2; nop L3; becomes L2: nop L3; + L1: branch L2; L1: branch L3; + L2; branch L3; becomes L2: branch L3; L3: instr; L3: instr; L4: if (cond) goto L1; L4: if (cond) goto L3; >> @@ -33,70 +34,156 @@ Require Import LTL. computations or useless moves), therefore there are more opportunities for tunneling after allocation than before. Symmetrically, prior tunneling helps linearization to produce - better code, e.g. by revealing that some [nop] instructions are - dead code (as the "nop L3" in the example above). + better code, e.g. by revealing that some [branch] instructions are + dead code (as the "branch L3" in the example above). *) (** The naive implementation of branch tunneling would replace any branch to a node [pc] by a branch to the node [branch_target f pc], defined as follows: << - branch_target f pc = branch_target f pc' if f(pc) = nop pc' + branch_target f pc = branch_target f pc' if f(pc) = branch pc' = pc otherwise >> However, this definition can fail to terminate if the program can contain loops consisting only of branches, as in << - L1: nop L1; + L1: branch L1; >> or -<< L1: nop L2; - L2: nop L1; +<< + L1: branch L2; + L2: branch L1; >> Coq warns us of this fact by not accepting the definition of [branch_target] above. - To handle this problem, we proceed in two passes. The first pass - populates a union-find data structure, adding equalities [pc = pc'] - for every instruction [pc: nop pc'] in the function. *) + To handle this problem, we proceed in two passes: + +- The first pass populates a union-find data structure, adding equalities + between PCs of blocks that are connected by branches and no other + computation. + +- The second pass rewrites the code, replacing every branch to a node [pc] + by a branch to the canonical representative of the equivalence class of [pc]. +*) + +(** * Construction of the union-find data structure *) Module U := UnionFind.UF(PTree). -Definition record_goto (uf: U.t) (pc: node) (b: bblock) : U.t := +(** We start populating the union-find data structure by adding + equalities [pc = pc'] for every block [pc: branch pc'] in the function. *) + +Definition record_branch (uf: U.t) (pc: node) (b: bblock) : U.t := match b with | Lbranch s :: _ => U.union uf pc s | _ => uf end. +Definition record_branches (f: LTL.function) : U.t := + PTree.fold record_branch f.(fn_code) U.empty. + +(** An additional optimization opportunity comes from conditional branches. + Consider a block [pc: cond ifso ifnot]. If the [ifso] case + and the [ifnot] case jump to the same block [pc'] + (modulo intermediate branches), the block can be simplified into + [pc: branch pc'], and the equality [pc = pc'] can be added to the + union-find data structure. *) + +(** In rare cases, the extra equation [pc = pc'] introduced by the + simplification of a conditional branch can trigger further simplifications + of other conditional branches. We therefore iterate the analysis + until no optimizable conditional branch remains. *) + +(** The code [c] (first component of the [st] triple) starts identical + to the code [fn.(fn_code)] of the current function, but each time + conditional branch at [pc] is optimized, we remove the block at + [pc] from the code [c]. This guarantees termination of the + iteration. *) + +Definition record_cond (st: code * U.t * bool) (pc: node) (b: bblock) : code * U.t * bool := + match b with + | Lcond cond args s1 s2 :: _ => + let '(c, u, _) := st in + if peq (U.repr u s1) (U.repr u s2) + then (PTree.remove pc c, U.union u pc s1, true) + else st + | _ => + st + end. + +Definition record_conds_1 (cu: code * U.t) : code * U.t * bool := + let (c, u) := cu in PTree.fold record_cond c (c, u, false). + +Definition measure_state (cu: code * U.t) : nat := + PTree_Properties.cardinal (fst cu). + +Function record_conds (cu: code * U.t) {measure measure_state cu} : U.t := + let (cu', changed) := record_conds_1 cu in + if changed then record_conds cu' else snd cu. +Proof. + intros [c0 u0] [c1 u1]. + set (P := fun (c: code) (s: code * U.t * bool) => + (forall pc, c!pc = None -> (fst (fst s))!pc = c0!pc) /\ + (PTree_Properties.cardinal (fst (fst s)) + + (if snd s then 1 else 0) + <= PTree_Properties.cardinal c0)%nat). + assert (A: P c0 (PTree.fold record_cond c0 (c0, u0, false))). + { apply PTree_Properties.fold_rec; unfold P. + - intros. destruct H0; split; auto. intros. rewrite <- H in H2. auto. + - simpl; split; intros. auto. simpl; lia. + - intros cd [[c u] changed] pc b NONE SOME [HR1 HR2]. simpl. split. + + intros p EQ. rewrite PTree.gsspec in EQ. destruct (peq p pc); try discriminate. + unfold record_cond. destruct b as [ | [] b ]; auto. + destruct (peq (U.repr u s1) (U.repr u s2)); auto. + simpl. rewrite PTree.gro by auto. auto. + + unfold record_cond. destruct b as [ | [] b ]; auto. + destruct (peq (U.repr u s1) (U.repr u s2)); auto. + simpl in *. + assert (SOME': c!pc = Some (Lcond cond args s1 s2 :: b)). + { rewrite HR1 by auto. auto. } + generalize (PTree_Properties.cardinal_remove SOME'). + destruct changed; lia. + } + unfold record_conds_1, measure_state; intros. + destruct A as [_ A]. rewrite teq in A. simpl in *. + lia. +Qed. + Definition record_gotos (f: LTL.function) : U.t := - PTree.fold record_goto f.(fn_code) U.empty. + record_conds (f.(fn_code), record_branches f). + +(** * Code transformation *) -(** The second pass rewrites all LTL instructions, replacing every +(** The code transformation rewrites all LTL instruction, replacing every successor [s] of every instruction by the canonical representative - of its equivalence class in the union-find data structure. *) + of its equivalence class in the union-find data structure. + Additionally, [Lcond] conditional branches are turned into [Lbranch] + unconditional branches whenever possible. *) -Definition tunnel_instr (uf: U.t) (i: instruction) : instruction := +Definition tunnel_instr (u: U.t) (i: instruction) : instruction := match i with - | Lbranch s => Lbranch (U.repr uf s) + | Lbranch s => Lbranch (U.repr u s) | Lcond cond args s1 s2 => - let s1' := U.repr uf s1 in let s2' := U.repr uf s2 in + let s1' := U.repr u s1 in let s2' := U.repr u s2 in if peq s1' s2' then Lbranch s1' else Lcond cond args s1' s2' - | Ljumptable arg tbl => Ljumptable arg (List.map (U.repr uf) tbl) + | Ljumptable arg tbl => Ljumptable arg (List.map (U.repr u) tbl) | _ => i end. -Definition tunnel_block (uf: U.t) (b: bblock) : bblock := - List.map (tunnel_instr uf) b. +Definition tunnel_block (u: U.t) (b: bblock) : bblock := + List.map (tunnel_instr u) b. Definition tunnel_function (f: LTL.function) : LTL.function := - let uf := record_gotos f in + let u := record_gotos f in mkfunction (fn_sig f) (fn_stacksize f) - (PTree.map1 (tunnel_block uf) (fn_code f)) - (U.repr uf (fn_entrypoint f)). + (PTree.map1 (tunnel_block u) (fn_code f)) + (U.repr u (fn_entrypoint f)). Definition tunnel_fundef (f: LTL.fundef) : LTL.fundef := transf_fundef tunnel_function f. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index d514c16f..68913fc9 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -12,6 +12,7 @@ (** Correctness proof for the branch tunneling optimization. *) +Require Import FunInd. Require Import Coqlib Maps UnionFind. Require Import AST Linking. Require Import Values Memory Events Globalenvs Smallstep. @@ -29,12 +30,21 @@ Qed. (** * Properties of the branch map computed using union-find. *) -Definition measure_edge (u: U.t) (pc s: node) (f: node -> nat) : node -> nat := +Section BRANCH_MAP_CORRECT. + +Variable fn: LTL.function. + +Definition measure_branch (u: U.t) (pc s: node) (f: node -> nat) : node -> nat := fun x => if peq (U.repr u s) pc then f x else if peq (U.repr u x) pc then (f x + f s + 1)%nat else f x. -Definition branch_map_correct (c: code) (u: U.t) (f: node -> nat): Prop := +Definition measure_cond (u: U.t) (pc s1 s2: node) (f: node -> nat) : node -> nat := + fun x => if peq (U.repr u s1) pc then f x + else if peq (U.repr u x) pc then (f x + Nat.max (f s1) (f s2) + 1)%nat + else f x. + +Definition branch_map_correct_1 (c: code) (u: U.t) (f: node -> nat): Prop := forall pc, match c!pc with | Some(Lbranch s :: b) => @@ -43,59 +53,209 @@ Definition branch_map_correct (c: code) (u: U.t) (f: node -> nat): Prop := U.repr u pc = pc end. -Lemma record_gotos_correct_1: - forall fn, { f | branch_map_correct fn.(fn_code) (record_gotos fn) f }. +Lemma record_branch_correct: + forall c u f pc b, + branch_map_correct_1 (PTree.remove pc c) u f -> + c!pc = Some b -> + { f' | branch_map_correct_1 c (record_branch u pc b) f' }. Proof. - intros. - unfold record_gotos. apply PTree_Properties.fold_ind. - -- (* base case *) - intros m EMPTY. exists (fun _ => O). - red; intros. rewrite EMPTY. apply U.repr_empty. - -- (* inductive case *) - intros m u pc bb GET1 GET2 [f BMC]. + intros c u f pc b BMC GET1. assert (PC: U.repr u pc = pc). { specialize (BMC pc). rewrite PTree.grs in BMC. auto. } - assert (DFL: { f | branch_map_correct m u f }). + assert (DFL: { f | branch_map_correct_1 c u f }). { exists f. intros p. destruct (peq p pc). - - subst p. rewrite GET1. destruct bb as [ | [] bb ]; auto. + - subst p. rewrite GET1. destruct b as [ | [] b ]; auto. - specialize (BMC p). rewrite PTree.gro in BMC by auto. exact BMC. } - unfold record_goto. destruct bb as [ | [] bb ]; auto. - exists (measure_edge u pc s f). intros p. destruct (peq p pc). -+ subst p. rewrite GET1. unfold measure_edge. + unfold record_branch. destruct b as [ | [] b ]; auto. + exists (measure_branch u pc s f). intros p. destruct (peq p pc). ++ subst p. rewrite GET1. unfold measure_branch. rewrite (U.repr_union_2 u pc s); auto. rewrite U.repr_union_3. destruct (peq (U.repr u s) pc); auto. rewrite PC, peq_true. right; split; auto. lia. + specialize (BMC p). rewrite PTree.gro in BMC by auto. assert (U.repr u p = p -> U.repr (U.union u pc s) p = p). { intro. rewrite <- H at 2. apply U.repr_union_1. congruence. } - destruct (m!p) as [ [ | [] b ] | ]; auto. + destruct (c!p) as [ [ | [] _ ] | ]; auto. destruct BMC as [A | [A B]]. auto. right; split. apply U.sameclass_union_2; auto. - unfold measure_edge. destruct (peq (U.repr u s) pc). auto. + unfold measure_branch. destruct (peq (U.repr u s) pc). auto. rewrite A. destruct (peq (U.repr u s0) pc); lia. Qed. -Definition branch_target (f: function) (pc: node) : node := - U.repr (record_gotos f) pc. +Lemma record_branches_correct: + { f | branch_map_correct_1 fn.(fn_code) (record_branches fn) f }. +Proof. + unfold record_branches. apply PTree_Properties.fold_ind. +- (* base case *) + intros m EMPTY. exists (fun _ => O). + red; intros. rewrite EMPTY. apply U.repr_empty. +- (* inductive case *) + intros m u pc bb GET1 GET2 [f BMC]. eapply record_branch_correct; eauto. +Qed. + +Definition branch_map_correct_2 (c: code) (u: U.t) (f: node -> nat): Prop := + forall pc, + match fn.(fn_code)!pc with + | Some(Lbranch s :: b) => + U.repr u pc = pc \/ (U.repr u pc = U.repr u s /\ f s < f pc)%nat + | Some(Lcond cond args s1 s2 :: b) => + U.repr u pc = pc \/ (c!pc = None /\ U.repr u pc = U.repr u s1 /\ U.repr u pc = U.repr u s2 /\ f s1 < f pc /\ f s2 < f pc)%nat + | _ => + U.repr u pc = pc + end. -Definition count_gotos (f: function) (pc: node) : nat := - proj1_sig (record_gotos_correct_1 f) pc. +Lemma record_cond_correct: + forall c u changed f pc b, + branch_map_correct_2 c u f -> + fn.(fn_code)!pc = Some b -> + c!pc <> None -> + let '(c1, u1, _) := record_cond (c, u, changed) pc b in + { f' | branch_map_correct_2 c1 u1 f' }. +Proof. + intros c u changed f pc b BMC GET1 GET2. + assert (DFL: { f' | branch_map_correct_2 c u f' }). + { exists f; auto. } + unfold record_cond. destruct b as [ | [] b ]; auto. + destruct (peq (U.repr u s1) (U.repr u s2)); auto. + exists (measure_cond u pc s1 s2 f). + assert (PC: U.repr u pc = pc). + { specialize (BMC pc). rewrite GET1 in BMC. intuition congruence. } + intro p. destruct (peq p pc). +- subst p. rewrite GET1. unfold measure_cond. + rewrite U.repr_union_2 by auto. rewrite <- e, PC, peq_true. + destruct (peq (U.repr u s1) pc); auto. + right; repeat split. + + apply PTree.grs. + + rewrite U.repr_union_3. auto. + + rewrite U.repr_union_1 by congruence. auto. + + lia. + + lia. +- assert (P: U.repr u p = p -> U.repr (U.union u pc s1) p = p). + { intros. rewrite U.repr_union_1 by congruence. auto. } + specialize (BMC p). destruct (fn_code fn)!p as [ [ | [] bb ] | ]; auto. + + destruct BMC as [A | (A & B)]; auto. right; split. + * apply U.sameclass_union_2; auto. + * unfold measure_cond. rewrite <- A. + destruct (peq (U.repr u s1) pc). auto. + destruct (peq (U.repr u p) pc); lia. + + destruct BMC as [A | (A & B & C & D & E)]; auto. right; split; [ | split; [ | split]]. + * rewrite PTree.gro by auto. auto. + * apply U.sameclass_union_2; auto. + * apply U.sameclass_union_2; auto. + * unfold measure_cond. rewrite <- B, <- C. + destruct (peq (U.repr u s1) pc). auto. + destruct (peq (U.repr u p) pc); lia. +Qed. + +Definition code_compat (c: code) : Prop := + forall pc b, c!pc = Some b -> fn.(fn_code)!pc = Some b. + +Definition code_invariant (c0 c1 c2: code) : Prop := + forall pc, c0!pc = None -> c1!pc = c2!pc. + +Lemma record_conds_1_correct: + forall c u f, + branch_map_correct_2 c u f -> + code_compat c -> + let '(c', u', _) := record_conds_1 (c, u) in + (code_compat c' * { f' | branch_map_correct_2 c' u' f' })%type. +Proof. + intros c0 u0 f0 BMC0 COMPAT0. + unfold record_conds_1. + set (x := PTree.fold record_cond c0 (c0, u0, false)). + set (P := fun (cd: code) (cuc: code * U.t * bool) => + (code_compat (fst (fst cuc)) * + code_invariant cd (fst (fst cuc)) c0 * + { f | branch_map_correct_2 (fst (fst cuc)) (snd (fst cuc)) f })%type). + assert (REC: P c0 x). + { unfold x; apply PTree_Properties.fold_ind. + - intros cd EMPTY. split; [split|]; simpl. + + auto. + + red; auto. + + exists f0; auto. + - intros cd [[c u] changed] pc b GET1 GET2 [[COMPAT INV] [f BMC]]. simpl in *. + split; [split|]. + + unfold record_cond; destruct b as [ | [] b]; simpl; auto. + destruct (peq (U.repr u s1) (U.repr u s2)); simpl; auto. + red; intros. rewrite PTree.grspec in H. destruct (PTree.elt_eq pc0 pc). discriminate. auto. + + assert (DFL: code_invariant cd c c0). + { intros p GET. apply INV. rewrite PTree.gro by congruence. auto. } + unfold record_cond; destruct b as [ | [] b]; simpl; auto. + destruct (peq (U.repr u s1) (U.repr u s2)); simpl; auto. + intros p GET. rewrite PTree.gro by congruence. apply INV. rewrite PTree.gro by congruence. auto. + + assert (GET3: c!pc = Some b). + { rewrite <- GET2. apply INV. apply PTree.grs. } + assert (X: fn.(fn_code)!pc = Some b) by auto. + assert (Y: c!pc <> None) by congruence. + generalize (record_cond_correct c u changed f pc b BMC X Y). + destruct (record_cond (c, u, changed) pc b) as [[c1 u1] changed1]; simpl. + auto. + } + destruct x as [[c1 u1] changed1]; destruct REC as [[COMPAT1 INV1] BMC1]; auto. +Qed. + +Definition branch_map_correct (u: U.t) (f: node -> nat): Prop := + forall pc, + match fn.(fn_code)!pc with + | Some(Lbranch s :: b) => + U.repr u pc = pc \/ (U.repr u pc = U.repr u s /\ f s < f pc)%nat + | Some(Lcond cond args s1 s2 :: b) => + U.repr u pc = pc \/ (U.repr u pc = U.repr u s1 /\ U.repr u pc = U.repr u s2 /\ f s1 < f pc /\ f s2 < f pc)%nat + | _ => + U.repr u pc = pc + end. + +Lemma record_conds_correct: + forall cu, + { f | branch_map_correct_2 (fst cu) (snd cu) f } -> + code_compat (fst cu) -> + { f | branch_map_correct (record_conds cu) f }. +Proof. + intros cu0. functional induction (record_conds cu0); intros. +- destruct cu as [c u], cu' as [c' u'], H as [f BMC]. + generalize (record_conds_1_correct c u f BMC H0). + rewrite e. intros [U V]. apply IHt; auto. +- destruct cu as [c u], H as [f BMC]. + exists f. intros pc. specialize (BMC pc); simpl in *. + destruct (fn_code fn)!pc as [ [ | [] b ] | ]; tauto. +Qed. + +Lemma record_gotos_correct_1: + { f | branch_map_correct (record_gotos fn) f }. +Proof. + apply record_conds_correct; simpl. +- destruct record_branches_correct as [f BMC]. + exists f. intros pc. specialize (BMC pc); simpl in *. + destruct (fn_code fn)!pc as [ [ | [] b ] | ]; auto. +- red; auto. +Qed. + +Definition branch_target (pc: node) : node := + U.repr (record_gotos fn) pc. + +Definition count_gotos (pc: node) : nat := + proj1_sig record_gotos_correct_1 pc. Theorem record_gotos_correct: - forall f pc, - match f.(fn_code)!pc with + forall pc, + match fn.(fn_code)!pc with | Some(Lbranch s :: b) => - branch_target f pc = pc \/ - (branch_target f pc = branch_target f s /\ count_gotos f s < count_gotos f pc)%nat - | _ => branch_target f pc = pc + branch_target pc = pc \/ + (branch_target pc = branch_target s /\ count_gotos s < count_gotos pc)%nat + | Some(Lcond cond args s1 s2 :: b) => + branch_target pc = pc \/ + (branch_target pc = branch_target s1 /\ branch_target pc = branch_target s2 + /\ count_gotos s1 < count_gotos pc /\ count_gotos s2 < count_gotos pc)%nat + | _ => + branch_target pc = pc end. Proof. - intros. unfold count_gotos. destruct (record_gotos_correct_1 f) as [m P]; simpl. + intros. unfold count_gotos. destruct record_gotos_correct_1 as [f P]; simpl. apply P. Qed. +End BRANCH_MAP_CORRECT. + (** * Preservation of semantics *) Section PRESERVATION. @@ -187,13 +347,21 @@ Inductive match_states: state -> state -> Prop := (MEM: Mem.extends m tm), match_states (Block s f sp bb ls m) (Block ts (tunnel_function f) sp (tunneled_block f bb) tls tm) - | match_states_interm: + | match_states_interm_branch: forall s f sp pc bb ls m ts tls tm (STK: list_forall2 match_stackframes s ts) (LS: locmap_lessdef ls tls) (MEM: Mem.extends m tm), match_states (Block s f sp (Lbranch pc :: bb) ls m) (State ts (tunnel_function f) sp (branch_target f pc) tls tm) + | match_states_interm_cond: + forall s f sp cond args pc1 pc2 bb ls m ts tls tm + (STK: list_forall2 match_stackframes s ts) + (LS: locmap_lessdef ls tls) + (MEM: Mem.extends m tm) + (SAME: branch_target f pc1 = branch_target f pc2), + match_states (Block s f sp (Lcond cond args pc1 pc2 :: bb) ls m) + (State ts (tunnel_function f) sp (branch_target f pc1) tls tm) | match_states_call: forall s f ls m ts tls tm (STK: list_forall2 match_stackframes s ts) @@ -346,6 +514,7 @@ Definition measure (st: state) : nat := match st with | State s f sp pc ls m => (count_gotos f pc * 2)%nat | Block s f sp (Lbranch pc :: _) ls m => (count_gotos f pc * 2 + 1)%nat + | Block s f sp (Lcond _ _ pc1 pc2 :: _) ls m => (Nat.max (count_gotos f pc1) (count_gotos f pc2) * 2 + 1)%nat | Block s f sp bb ls m => 0%nat | Callstate s f ls m => 0%nat | Returnstate s ls m => 0%nat @@ -380,10 +549,16 @@ Proof. generalize (record_gotos_correct f pc). rewrite H. destruct bb; auto. destruct i; auto. ++ (* Lbranch *) intros [A | [B C]]. auto. right. split. simpl. lia. split. auto. rewrite B. econstructor; eauto. ++ (* Lcond *) + intros [A | (B & C & D & E)]. auto. + right. split. simpl. lia. + split. auto. + rewrite B. econstructor; eauto. congruence. - (* Lop *) exploit eval_operation_lessdef. apply reglist_lessdef; eauto. eauto. eauto. @@ -450,18 +625,24 @@ Proof. - (* Lbranch (eliminated) *) right; split. simpl. lia. split. auto. constructor; auto. -- (* Lcond *) +- (* Lcond (preserved) *) simpl tunneled_block. set (s1 := U.repr (record_gotos f) pc1). set (s2 := U.repr (record_gotos f) pc2). destruct (peq s1 s2). + left; econstructor; split. - eapply exec_Lbranch. - destruct b. -* constructor; eauto using locmap_undef_regs_lessdef_1. -* rewrite e. constructor; eauto using locmap_undef_regs_lessdef_1. + eapply exec_Lbranch. + set (pc := if b then pc1 else pc2). + replace s1 with (branch_target f pc) by (unfold pc; destruct b; auto). + constructor; eauto using locmap_undef_regs_lessdef_1. + left; econstructor; split. eapply exec_Lcond; eauto. eapply eval_condition_lessdef; eauto using reglist_lessdef. destruct b; econstructor; eauto using locmap_undef_regs_lessdef. +- (* Lcond (eliminated) *) + right; split. simpl. destruct b; lia. + split. auto. + set (pc := if b then pc1 else pc2). + replace (branch_target f pc1) with (branch_target f pc) by (unfold pc; destruct b; auto). + econstructor; eauto. - (* Ljumptable *) assert (tls (R arg) = Vint n). -- cgit From fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jan 2021 15:44:09 +0100 Subject: Qualify `Hint` as `Global Hint` where appropriate This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`. --- backend/Asmgenproof0.v | 12 ++++++------ backend/CSEdomain.v | 4 ++-- backend/CminorSel.v | 4 ++-- backend/Cminortyping.v | 12 ++++++------ backend/Deadcodeproof.v | 2 +- backend/NeedDomain.v | 10 +++++----- backend/RTLgenproof.v | 4 ++-- backend/RTLgenspec.v | 48 ++++++++++++++++++++++++------------------------ backend/ValueAnalysis.v | 4 ++-- backend/ValueDomain.v | 20 ++++++++++---------- 10 files changed, 60 insertions(+), 60 deletions(-) (limited to 'backend') diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 5e8acd6f..85cee14f 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -31,7 +31,7 @@ Require Import Conventions. (** * Processor registers and register states *) -Hint Extern 2 (_ <> _) => congruence: asmgen. +Global Hint Extern 2 (_ <> _) => congruence: asmgen. Lemma ireg_of_eq: forall r r', ireg_of r = OK r' -> preg_of r = IR r'. @@ -56,7 +56,7 @@ Lemma preg_of_data: Proof. intros. destruct r; reflexivity. Qed. -Hint Resolve preg_of_data: asmgen. +Global Hint Resolve preg_of_data: asmgen. Lemma data_diff: forall r r', @@ -64,7 +64,7 @@ Lemma data_diff: Proof. congruence. Qed. -Hint Resolve data_diff: asmgen. +Global Hint Resolve data_diff: asmgen. Lemma preg_of_not_SP: forall r, preg_of r <> SP. @@ -78,7 +78,7 @@ Proof. intros. apply data_diff; auto with asmgen. Qed. -Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen. +Global Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen. Lemma nextinstr_pc: forall rs, (nextinstr rs)#PC = Val.offset_ptr rs#PC Ptrofs.one. @@ -746,7 +746,7 @@ Qed. Definition nolabel (i: instruction) := match i with Plabel _ => False | _ => True end. -Hint Extern 1 (nolabel _) => exact I : labels. +Global Hint Extern 1 (nolabel _) => exact I : labels. Lemma tail_nolabel_cons: forall i c k, @@ -757,7 +757,7 @@ Proof. intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction. Qed. -Hint Resolve tail_nolabel_refl: labels. +Global Hint Resolve tail_nolabel_refl: labels. Ltac TailNoLabel := eauto with labels; diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v index 9b1243c8..e96c4cd4 100644 --- a/backend/CSEdomain.v +++ b/backend/CSEdomain.v @@ -92,7 +92,7 @@ Record wf_numbering (n: numbering) : Prop := { In r (PMap.get v n.(num_val)) -> PTree.get r n.(num_reg) = Some v }. -Hint Resolve wf_num_eqs wf_num_reg wf_num_val: cse. +Global Hint Resolve wf_num_eqs wf_num_reg wf_num_val: cse. (** Satisfiability of numberings. A numbering holds in a concrete execution state if there exists a valuation assigning values to @@ -130,7 +130,7 @@ Record numbering_holds (valu: valuation) (ge: genv) (sp: val) n.(num_reg)!r = Some v -> rs#r = valu v }. -Hint Resolve num_holds_wf num_holds_eq num_holds_reg: cse. +Global Hint Resolve num_holds_wf num_holds_eq num_holds_reg: cse. Lemma empty_numbering_holds: forall valu ge sp rs m, diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 5cbdc249..f6f6e34d 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -464,7 +464,7 @@ Inductive final_state: state -> int -> Prop := Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). -Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr. +Global Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr. (** * Lifting of let-bound variables *) @@ -580,4 +580,4 @@ Proof. eexact H. apply insert_lenv_0. Qed. -Hint Resolve eval_lift: evalexpr. +Global Hint Resolve eval_lift: evalexpr. diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v index 92ec45f2..9f35fe35 100644 --- a/backend/Cminortyping.v +++ b/backend/Cminortyping.v @@ -290,7 +290,7 @@ Lemma expect_incr: forall te e t1 t2 e', Proof. unfold expect; intros. destruct (typ_eq t1 t2); inv H; auto. Qed. -Hint Resolve expect_incr: ty. +Global Hint Resolve expect_incr: ty. Lemma expect_sound: forall e t1 t2 e', expect e t1 t2 = OK e' -> t1 = t2. @@ -305,7 +305,7 @@ Proof. - destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty. - destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty. Qed. -Hint Resolve type_expr_incr: ty. +Global Hint Resolve type_expr_incr: ty. Lemma type_expr_sound: forall te a t e e', type_expr e a t = OK e' -> S.satisf te e' -> wt_expr te a t. @@ -325,7 +325,7 @@ Lemma type_exprlist_incr: forall te al tl e e', Proof. induction al; destruct tl; simpl; intros until e'; intros T SAT; monadInv T; eauto with ty. Qed. -Hint Resolve type_exprlist_incr: ty. +Global Hint Resolve type_exprlist_incr: ty. Lemma type_exprlist_sound: forall te al tl e e', type_exprlist e al tl = OK e' -> S.satisf te e' -> list_forall2 (wt_expr te) al tl. @@ -342,7 +342,7 @@ Proof. - destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty. - destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty. Qed. -Hint Resolve type_assign_incr: ty. +Global Hint Resolve type_assign_incr: ty. Lemma type_assign_sound: forall te id a e e', type_assign e id a = OK e' -> S.satisf te e' -> wt_expr te a (te id). @@ -362,7 +362,7 @@ Lemma opt_set_incr: forall te optid optty e e', Proof. unfold opt_set; intros. destruct optid, optty; try (monadInv H); eauto with ty. Qed. -Hint Resolve opt_set_incr: ty. +Global Hint Resolve opt_set_incr: ty. Lemma opt_set_sound: forall te optid sg e e', opt_set e optid (proj_sig_res sg) = OK e' -> S.satisf te e' -> @@ -379,7 +379,7 @@ Proof. induction s; simpl; intros e1 e2 T SAT; try (monadInv T); eauto with ty. - destruct tret, o; try (monadInv T); eauto with ty. Qed. -Hint Resolve type_stmt_incr: ty. +Global Hint Resolve type_stmt_incr: ty. Lemma type_stmt_sound: forall te tret s e e', type_stmt tret e s = OK e' -> S.satisf te e' -> wt_stmt te tret s. diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 7aa6ff88..7be12c69 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -358,7 +358,7 @@ Proof. intros. destruct ros; simpl in *. eapply add_need_all_eagree; eauto. auto. Qed. -Hint Resolve add_need_all_eagree add_need_all_lessdef +Global Hint Resolve add_need_all_eagree add_need_all_lessdef add_need_eagree add_need_vagree add_needs_all_eagree add_needs_all_lessdef add_needs_eagree add_needs_vagree diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index d3c6ed75..fc1ae16d 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -74,7 +74,7 @@ Proof. intros. simpl in H. auto. Qed. -Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na. +Global Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na. Inductive vagree_list: list val -> list val -> list nval -> Prop := | vagree_list_nil: forall nvl, @@ -100,7 +100,7 @@ Proof. destruct nvl; constructor; auto with na. Qed. -Hint Resolve lessdef_vagree_list vagree_lessdef_list: na. +Global Hint Resolve lessdef_vagree_list vagree_lessdef_list: na. (** ** Ordering and least upper bound between value needs *) @@ -116,8 +116,8 @@ Proof. destruct x; constructor; auto. Qed. -Hint Constructors nge: na. -Hint Resolve nge_refl: na. +Global Hint Constructors nge: na. +Global Hint Resolve nge_refl: na. Lemma nge_trans: forall x y, nge x y -> forall z, nge y z -> nge x z. Proof. @@ -1084,7 +1084,7 @@ Proof. intros. apply H. Qed. -Hint Resolve nreg_agree: na. +Global Hint Resolve nreg_agree: na. Lemma eagree_ge: forall e1 e2 ne ne', diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 88f7fe53..1602823f 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -165,7 +165,7 @@ Proof. subst r0; contradiction. apply Regmap.gso; auto. Qed. -Hint Resolve match_env_update_temp: rtlg. +Global Hint Resolve match_env_update_temp: rtlg. (** Matching between environments is preserved by simultaneous assignment to a Cminor local variable (in the Cminor environments) @@ -205,7 +205,7 @@ Proof. eapply match_env_update_temp; eauto. eapply match_env_update_var; eauto. Qed. -Hint Resolve match_env_update_dest: rtlg. +Global Hint Resolve match_env_update_dest: rtlg. (** A variant of [match_env_update_var] corresponding to the assignment of the result of a builtin. *) diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 72693f63..25f9954c 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -128,7 +128,7 @@ Ltac monadInv H := (** * Monotonicity properties of the state *) -Hint Resolve state_incr_refl: rtlg. +Global Hint Resolve state_incr_refl: rtlg. Lemma instr_at_incr: forall s1 s2 n i, @@ -137,7 +137,7 @@ Proof. intros. inv H. destruct (H3 n); congruence. Qed. -Hint Resolve instr_at_incr: rtlg. +Global Hint Resolve instr_at_incr: rtlg. (** The following tactic saturates the hypotheses with [state_incr] properties that follow by transitivity from @@ -174,14 +174,14 @@ Lemma valid_fresh_absurd: Proof. intros r s. unfold reg_valid, reg_fresh; case r; tauto. Qed. -Hint Resolve valid_fresh_absurd: rtlg. +Global Hint Resolve valid_fresh_absurd: rtlg. Lemma valid_fresh_different: forall r1 r2 s, reg_valid r1 s -> reg_fresh r2 s -> r1 <> r2. Proof. unfold not; intros. subst r2. eauto with rtlg. Qed. -Hint Resolve valid_fresh_different: rtlg. +Global Hint Resolve valid_fresh_different: rtlg. Lemma reg_valid_incr: forall r s1 s2, state_incr s1 s2 -> reg_valid r s1 -> reg_valid r s2. @@ -190,7 +190,7 @@ Proof. inversion INCR. unfold reg_valid. intros; apply Plt_Ple_trans with (st_nextreg s1); auto. Qed. -Hint Resolve reg_valid_incr: rtlg. +Global Hint Resolve reg_valid_incr: rtlg. Lemma reg_fresh_decr: forall r s1 s2, state_incr s1 s2 -> reg_fresh r s2 -> reg_fresh r s1. @@ -199,7 +199,7 @@ Proof. unfold reg_fresh; unfold not; intros. apply H4. apply Plt_Ple_trans with (st_nextreg s1); auto. Qed. -Hint Resolve reg_fresh_decr: rtlg. +Global Hint Resolve reg_fresh_decr: rtlg. (** Validity of a list of registers. *) @@ -211,7 +211,7 @@ Lemma regs_valid_nil: Proof. intros; red; intros. elim H. Qed. -Hint Resolve regs_valid_nil: rtlg. +Global Hint Resolve regs_valid_nil: rtlg. Lemma regs_valid_cons: forall r1 rl s, @@ -232,7 +232,7 @@ Lemma regs_valid_incr: Proof. unfold regs_valid; intros; eauto with rtlg. Qed. -Hint Resolve regs_valid_incr: rtlg. +Global Hint Resolve regs_valid_incr: rtlg. (** A register is ``in'' a mapping if it is associated with a Cminor local or let-bound variable. *) @@ -253,7 +253,7 @@ Lemma map_valid_incr: Proof. unfold map_valid; intros; eauto with rtlg. Qed. -Hint Resolve map_valid_incr: rtlg. +Global Hint Resolve map_valid_incr: rtlg. (** * Properties of basic operations over the state *) @@ -265,7 +265,7 @@ Lemma add_instr_at: Proof. intros. monadInv H. simpl. apply PTree.gss. Qed. -Hint Resolve add_instr_at: rtlg. +Global Hint Resolve add_instr_at: rtlg. (** Properties of [update_instr]. *) @@ -278,7 +278,7 @@ Proof. destruct (check_empty_node s1 n); try discriminate. inv H. simpl. apply PTree.gss. Qed. -Hint Resolve update_instr_at: rtlg. +Global Hint Resolve update_instr_at: rtlg. (** Properties of [new_reg]. *) @@ -289,7 +289,7 @@ Proof. intros. monadInv H. unfold reg_valid; simpl. apply Plt_succ. Qed. -Hint Resolve new_reg_valid: rtlg. +Global Hint Resolve new_reg_valid: rtlg. Lemma new_reg_fresh: forall s1 s2 r i, @@ -299,7 +299,7 @@ Proof. unfold reg_fresh; simpl. exact (Plt_strict _). Qed. -Hint Resolve new_reg_fresh: rtlg. +Global Hint Resolve new_reg_fresh: rtlg. Lemma new_reg_not_in_map: forall s1 s2 m r i, @@ -307,7 +307,7 @@ Lemma new_reg_not_in_map: Proof. unfold not; intros; eauto with rtlg. Qed. -Hint Resolve new_reg_not_in_map: rtlg. +Global Hint Resolve new_reg_not_in_map: rtlg. (** * Properties of operations over compilation environments *) @@ -330,7 +330,7 @@ Proof. intros. inv H0. left; exists name; auto. intros. inv H0. Qed. -Hint Resolve find_var_in_map: rtlg. +Global Hint Resolve find_var_in_map: rtlg. Lemma find_var_valid: forall s1 s2 map name r i, @@ -338,7 +338,7 @@ Lemma find_var_valid: Proof. eauto with rtlg. Qed. -Hint Resolve find_var_valid: rtlg. +Global Hint Resolve find_var_valid: rtlg. (** Properties of [find_letvar]. *) @@ -350,7 +350,7 @@ Proof. caseEq (nth_error (map_letvars map) idx); intros; monadInv H0. right; apply nth_error_in with idx; auto. Qed. -Hint Resolve find_letvar_in_map: rtlg. +Global Hint Resolve find_letvar_in_map: rtlg. Lemma find_letvar_valid: forall s1 s2 map idx r i, @@ -358,7 +358,7 @@ Lemma find_letvar_valid: Proof. eauto with rtlg. Qed. -Hint Resolve find_letvar_valid: rtlg. +Global Hint Resolve find_letvar_valid: rtlg. (** Properties of [add_var]. *) @@ -445,7 +445,7 @@ Proof. intros until r. unfold alloc_reg. case a; eauto with rtlg. Qed. -Hint Resolve alloc_reg_valid: rtlg. +Global Hint Resolve alloc_reg_valid: rtlg. Lemma alloc_reg_fresh_or_in_map: forall map a s r s' i, @@ -469,7 +469,7 @@ Proof. apply regs_valid_nil. apply regs_valid_cons. eauto with rtlg. eauto with rtlg. Qed. -Hint Resolve alloc_regs_valid: rtlg. +Global Hint Resolve alloc_regs_valid: rtlg. Lemma alloc_regs_fresh_or_in_map: forall map al s rl s' i, @@ -494,7 +494,7 @@ Proof. intros until r. unfold alloc_reg. case dest; eauto with rtlg. Qed. -Hint Resolve alloc_optreg_valid: rtlg. +Global Hint Resolve alloc_optreg_valid: rtlg. Lemma alloc_optreg_fresh_or_in_map: forall map dest s r s' i, @@ -609,7 +609,7 @@ Proof. apply regs_valid_cons; eauto with rtlg. Qed. -Hint Resolve new_reg_target_ok alloc_reg_target_ok +Global Hint Resolve new_reg_target_ok alloc_reg_target_ok alloc_regs_target_ok: rtlg. (** The following predicate is a variant of [target_reg_ok] used @@ -631,7 +631,7 @@ Lemma return_reg_ok_incr: Proof. induction 1; intros; econstructor; eauto with rtlg. Qed. -Hint Resolve return_reg_ok_incr: rtlg. +Global Hint Resolve return_reg_ok_incr: rtlg. Lemma new_reg_return_ok: forall s1 r s2 map sig i, @@ -676,7 +676,7 @@ Inductive reg_map_ok: mapping -> reg -> option ident -> Prop := map.(map_vars)!id = Some rd -> reg_map_ok map rd (Some id). -Hint Resolve reg_map_ok_novar: rtlg. +Global Hint Resolve reg_map_ok_novar: rtlg. (** [tr_expr c map pr expr ns nd rd optid] holds if the graph [c], between nodes [ns] and [nd], contains instructions that compute the diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index f7e4f0ed..ebf2c5ea 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -342,7 +342,7 @@ Proof. induction rl; simpl; intros. constructor. constructor; auto. apply areg_sound; auto. Qed. -Hint Resolve areg_sound aregs_sound: va. +Global Hint Resolve areg_sound aregs_sound: va. Lemma abuiltin_arg_sound: forall bc ge rs sp m ae rm am, @@ -1912,7 +1912,7 @@ Proof. - exact NOSTACK. Qed. -Hint Resolve areg_sound aregs_sound: va. +Global Hint Resolve areg_sound aregs_sound: va. (** * Interface with other optimizations *) diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 45894bfc..01f080ff 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -43,12 +43,12 @@ Proof. elim H. apply H0; auto. Qed. -Hint Extern 2 (_ = _) => congruence : va. -Hint Extern 2 (_ <> _) => congruence : va. -Hint Extern 2 (_ < _) => extlia : va. -Hint Extern 2 (_ <= _) => extlia : va. -Hint Extern 2 (_ > _) => extlia : va. -Hint Extern 2 (_ >= _) => extlia : va. +Global Hint Extern 2 (_ = _) => congruence : va. +Global Hint Extern 2 (_ <> _) => congruence : va. +Global Hint Extern 2 (_ < _) => extlia : va. +Global Hint Extern 2 (_ <= _) => extlia : va. +Global Hint Extern 2 (_ > _) => extlia : va. +Global Hint Extern 2 (_ >= _) => extlia : va. Section MATCH. @@ -4711,10 +4711,10 @@ Module VA <: SEMILATTICE. End VA. -Hint Constructors cmatch : va. -Hint Constructors pmatch: va. -Hint Constructors vmatch: va. -Hint Resolve cnot_sound symbol_address_sound +Global Hint Constructors cmatch : va. +Global Hint Constructors pmatch: va. +Global Hint Constructors vmatch: va. +Global Hint Resolve cnot_sound symbol_address_sound shl_sound shru_sound shr_sound and_sound or_sound xor_sound notint_sound ror_sound rolm_sound -- cgit From 30feb31c6d6e9235acad42ec5d09d14f3919cc36 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 30 Dec 2020 11:41:10 +0100 Subject: Introduce and use PrintAsmaux.variable_section This is a generalization of the previous PrintAsmaux.common_section function that - handles initialized variables in addition to uninitialized variables; - can be used for Section_const, not just for Section_data. --- backend/PrintAsmaux.ml | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) (limited to 'backend') diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index d31507ff..82621010 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -303,11 +303,16 @@ let print_version_and_options oc comment = fprintf oc " %s" Commandline.argv.(i) done; fprintf oc "\n" -(** Get the name of the common section if it is used otherwise the given section - name, with bss as default *) -let common_section ?(sec = ".bss") () = - if !Clflags.option_fcommon then - "COMM" - else - sec +(** Determine the name of the section to use for a variable. + [i] says whether the variable is initialized (true) or not (false). + [sec] is the name of the section to use if initialized or if + no other cases apply. + [bss] is the name of the section to use if uninitialized and + common declarations are not used. If not provided, [sec] is used. +*) + +let variable_section ~sec ?bss i = + if i then sec + else if !Clflags.option_fcommon then "COMM" + else match bss with None -> sec | Some b -> b -- cgit From ed89275cb820bb7ab283c51e461d852d1c8bec63 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 30 Dec 2020 11:00:22 +0100 Subject: Section handling: finer control of variable initialization Distinguish between: - uninitialized variables, which can go in COMM if supported - variables initialized with fixed, numeric quantities, which can go in a readonly section if "const" - variables initialized with symbol addresses which may need relocation, which cannot go in a readonly section even if "const", but can go in a special "const_data" section. Also: on macOS, use ".const" instead of ".literal8" for literals, as not all literals have size 8. --- backend/JsonAST.ml | 10 +++++++++- backend/PrintAsm.ml | 2 +- backend/PrintAsmaux.ml | 23 +++++++++++++++-------- 3 files changed, 25 insertions(+), 10 deletions(-) (limited to 'backend') diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml index 8905e252..d218e567 100644 --- a/backend/JsonAST.ml +++ b/backend/JsonAST.ml @@ -21,14 +21,22 @@ open Sections let pp_storage pp static = pp_jstring pp (if static then "Static" else "Extern") +let pp_init pp init = + pp_jstring pp + (match init with + | Uninit -> "Uninit" + | Init -> "Init" + | Init_reloc -> "Init_reloc") + let pp_section pp sec = let pp_simple name = pp_jsingle_object pp "Section Name" pp_jstring name and pp_complex name init = pp_jobject_start pp; pp_jmember ~first:true pp "Section Name" pp_jstring name; - pp_jmember pp "Init" pp_jbool init; + pp_jmember pp "Init" pp_init init; pp_jobject_end pp in + match sec with | Section_text -> pp_simple "Text" | Section_data init -> pp_complex "Data" init diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 155f5e55..22df68ae 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -121,7 +121,7 @@ module Printer(Target:TARGET) = let sec = match C2C.atom_sections name with | [s] -> s - | _ -> Section_data true + | _ -> Section_data Init and align = match C2C.atom_alignof name with | Some a -> a diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 82621010..7a692d20 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -305,14 +305,21 @@ let print_version_and_options oc comment = fprintf oc "\n" (** Determine the name of the section to use for a variable. - [i] says whether the variable is initialized (true) or not (false). - [sec] is the name of the section to use if initialized or if - no other cases apply. - [bss] is the name of the section to use if uninitialized and + - [i] is the initialization status of the variable. + - [sec] is the name of the section to use if initialized (with no + relocations) or if no other cases apply. + - [reloc] is the name of the section to use if initialized and + containing relocations. If not provided, [sec] is used. + - [bss] is the name of the section to use if uninitialized and common declarations are not used. If not provided, [sec] is used. *) -let variable_section ~sec ?bss i = - if i then sec - else if !Clflags.option_fcommon then "COMM" - else match bss with None -> sec | Some b -> b +let variable_section ~sec ?bss ?reloc i = + match i with + | Uninit -> + if !Clflags.option_fcommon + then "COMM" + else begin match bss with Some s -> s | None -> sec end + | Init -> sec + | Init_reloc -> + begin match reloc with Some s -> s | None -> sec end -- cgit From 014883f2f4cfc4fd64fe9aa5f561a971e2ed1345 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 19 Feb 2021 09:31:03 +0100 Subject: Fix regression on PowerPC / Diab On PowerPC/Diab, common declarations must not be used for small data sections. Add a `~common` option to `PrintAsmaux.variable_section` to control the use of common declarations. The default is whatever is specified on the command line using the `-fcommon` and `-fno-common` options. Use `~common:false` for `Section_small_data` on PowerPC / Diab. Note that on PowerPC/Linux, GCC uses common declarations for uninitialized variables in small data section, so we keep doing this in CompCert as well. --- backend/PrintAsmaux.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'backend') diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 7a692d20..e39ba8aa 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -312,12 +312,17 @@ let print_version_and_options oc comment = containing relocations. If not provided, [sec] is used. - [bss] is the name of the section to use if uninitialized and common declarations are not used. If not provided, [sec] is used. + - [common] says whether common declarations can be used for uninitialized + variables. It defaults to the status of the [-fcommon] / [-fno-common] + command-line option. Passing [~common:false] is needed when + common declarations cannot be used at all, for example in the context of + small data areas. *) -let variable_section ~sec ?bss ?reloc i = +let variable_section ~sec ?bss ?reloc ?(common = !Clflags.option_fcommon) i = match i with | Uninit -> - if !Clflags.option_fcommon + if common then "COMM" else begin match bss with Some s -> s | None -> sec end | Init -> sec -- cgit From 7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 29 Mar 2021 11:12:07 +0200 Subject: replacing omega with lia in some file --- backend/CSEproof.v | 2 +- backend/Injectproof.v | 8 ++++---- backend/ValueDomain.v | 5 +++-- 3 files changed, 8 insertions(+), 7 deletions(-) (limited to 'backend') diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 0716dad7..cf51f5a2 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -620,7 +620,7 @@ Proof. destruct a; simpl in H10; try discriminate; simpl; trivial. rewrite negb_false_iff in H8. eapply Mem.load_storebytes_other. eauto. - rewrite H6. rewrite Z2Nat.id by omega. + rewrite H6. rewrite Z2Nat.id by lia. eapply pdisjoint_sound. eauto. unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. erewrite <- regs_valnums_sound by eauto. eauto with va. diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 9e5ad6df..dd5e72f8 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -89,7 +89,7 @@ Qed. Obligation 2. Proof. simpl in BOUND. - omega. + lia. Qed. Program Definition bounded_nth_S_statement : Prop := @@ -104,14 +104,14 @@ Lemma bounded_nth_proof_irr : (BOUND1 BOUND2 : (k < List.length l)%nat), (bounded_nth k l BOUND1) = (bounded_nth k l BOUND2). Proof. - induction k; destruct l; simpl; intros; trivial; omega. + induction k; destruct l; simpl; intros; trivial; lia. Qed. Lemma bounded_nth_S : bounded_nth_S_statement. Proof. unfold bounded_nth_S_statement. induction k; destruct l; simpl; intros; trivial. - 1, 2: omega. + 1, 2: lia. apply bounded_nth_proof_irr. Qed. @@ -121,7 +121,7 @@ Lemma inject_list_injected: Some (inject_instr (bounded_nth k l BOUND) (Pos.succ (pos_add_nat pc k))). Proof. induction l; simpl; intros. - - omega. + - lia. - simpl. destruct k as [ | k]; simpl pos_add_nat. + simpl bounded_nth. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 0f895040..5a7cfc12 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -15,6 +15,7 @@ Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice. Require Import Compopts AST. Require Import Values Memory Globalenvs Builtins Events. Require Import Registers RTL. +Require Import Lia. (** The abstract domains for value analysis *) @@ -2822,8 +2823,8 @@ Proof. generalize (Int.unsigned_range_2 j); intros RANGE. assert (Int.unsigned j <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. } - exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD. - unfold Int.modu. rewrite Int.unsigned_repr. omega. omega. + exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). lia. intros MOD. + unfold Int.modu. rewrite Int.unsigned_repr. lia. lia. } intros until y. intros HX HY. -- cgit From 9faa0b9eb03e37facaf77366d703bb20f4af9461 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 28 Apr 2021 12:34:44 +0200 Subject: Heuristic counter update --- backend/Duplicateaux.ml | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) (limited to 'backend') diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index d55da64a..425947ce 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -48,13 +48,11 @@ let stats_nb_overpredict = ref 0 let wrong_opcode = ref 0 let wrong_return = ref 0 let wrong_loop2 = ref 0 -let wrong_loop = ref 0 let wrong_call = ref 0 let right_opcode = ref 0 let right_return = ref 0 let right_loop2 = ref 0 -let right_loop = ref 0 let right_call = ref 0 let reset_stats () = begin @@ -66,12 +64,10 @@ let reset_stats () = begin wrong_opcode := 0; wrong_return := 0; wrong_loop2 := 0; - wrong_loop := 0; wrong_call := 0; right_opcode := 0; right_return := 0; right_loop2 := 0; - right_loop := 0; right_call := 0; end @@ -85,11 +81,11 @@ let write_stats_oc () = match !stats_oc with | None -> () | Some oc -> begin - Printf.fprintf oc "%d %d %d %d %d %d %d %d %d %d %d %d %d %d %d\n" !stats_nb_total + Printf.fprintf oc "%d %d %d %d %d %d %d %d %d %d %d %d %d\n" !stats_nb_total !stats_nb_correct_predicts !stats_nb_mispredicts !stats_nb_missed_opportunities !stats_nb_overpredict - !wrong_opcode !wrong_return !wrong_loop2 !wrong_loop !wrong_call - !right_opcode !right_return !right_loop2 !right_loop !right_call + !wrong_opcode !wrong_return !wrong_loop2 !wrong_call + !right_opcode !right_return !right_loop2 !right_call ; close_out oc end @@ -417,7 +413,7 @@ let get_directions f code entrypoint = begin if stats_oc_recording () || not @@ has_some pred then (* debug "Analyzing %d.." (P.to_int n); *) let heuristics = [ do_opcode_heuristic; - do_return_heuristic; do_loop2_heuristic loop_info n; do_loop_heuristic; do_call_heuristic; + do_return_heuristic; do_loop2_heuristic loop_info n; (* do_loop_heuristic; *) do_call_heuristic; (* do_store_heuristic *) ] in let preferred = ref None in let current_heuristic = ref 0 in @@ -438,8 +434,7 @@ let get_directions f code entrypoint = begin | 0 -> incr wrong_opcode | 1 -> incr wrong_return | 2 -> incr wrong_loop2 - | 3 -> incr wrong_loop - | 4 -> incr wrong_call + | 3 -> incr wrong_call | _ -> failwith "Shouldn't happen" end | Some false, Some false @@ -448,8 +443,7 @@ let get_directions f code entrypoint = begin | 0 -> incr right_opcode | 1 -> incr right_return | 2 -> incr right_loop2 - | 3 -> incr right_loop - | 4 -> incr right_call + | 3 -> incr right_call | _ -> failwith "Shouldn't happen" end | _ -> () -- cgit From 8b649e6898afeb243a992ab81092c4fd431410d7 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 28 Apr 2021 12:44:30 +0200 Subject: Do not rotate if the CB was already at the end. --- backend/Duplicateaux.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'backend') diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index 425947ce..324acd99 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -1044,9 +1044,13 @@ let extract_upto_icond f code head = let rotate_inner_loop f code revmap iloop = let header = extract_upto_icond f code iloop.head in let limit = !Clflags.option_flooprotate in - if count_ignore_nops code header > limit then begin + let nb_duplicated = count_ignore_nops code header in + if nb_duplicated > limit then begin debug "Loop Rotate: too many nodes to duplicate (%d > %d)" (List.length header) limit; (code, revmap) + end else if nb_duplicated == count_ignore_nops code iloop.body then begin + debug "The conditional branch is already at the end! No need to rotate."; + (code, revmap) end else let (code2, revmap2, dupheader, fwmap) = clone code revmap header in let code' = ref code2 in -- cgit From 5a632954c85e8b2b5afea124e4fc83f39c5d3598 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 1 Jun 2021 14:37:07 +0200 Subject: [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend/C2C.ml --- backend/Cminor.v | 9 +++++---- backend/JsonAST.ml | 8 +++++++- backend/NeedDomain.v | 2 +- backend/PrintCminor.ml | 9 +++++---- 4 files changed, 18 insertions(+), 10 deletions(-) (limited to 'backend') diff --git a/backend/Cminor.v b/backend/Cminor.v index e585dc13..829adca0 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.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/backend/JsonAST.ml b/backend/JsonAST.ml index a55bfa0c..2e70aae7 100644 --- a/backend/JsonAST.ml +++ b/backend/JsonAST.ml @@ -114,11 +114,17 @@ let pp_program pp pp_inst prog = let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) -> match def with | Gfun (Internal f) -> + (* No assembly is generated for non static inline functions *) if not (atom_is_iso_inline_definition ident) then vars,(ident,f)::funs else vars,funs - | Gvar v -> (ident,v)::vars,funs + | Gvar v -> + (* No assembly is generated for variables without init *) + if v.gvar_init <> [] then + (ident,v)::vars,funs + else + vars, funs | _ -> vars,funs) ([],[]) prog.prog_defs in pp_jobject_start pp; pp_jmember ~first:true pp "Global Variables" (pp_jarray pp_vardef) prog_vars; diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index fc1ae16d..62b8ff90 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -737,7 +737,7 @@ Lemma store_argument_sound: Proof. intros. assert (UNDEF: list_forall2 memval_lessdef - (list_repeat (size_chunk_nat chunk) Undef) + (List.repeat Undef (size_chunk_nat chunk)) (encode_val chunk w)). { rewrite <- (encode_val_length chunk w). diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 051225a4..9ca0e3a0 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.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. *) (* *) (* *********************************************************************) -- cgit