diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
commit | af16cdae6d58033cc8aa06bca330f98b96ba12f2 (patch) | |
tree | 4985e9ae8fa0d580bbf95a198edeca4f0bd6ff46 /backend/RTL.v | |
parent | 21c979fce33b068ce4b86e67d3d866b203411c6c (diff) | |
parent | 02b169b444c435b8d1aacf54969dd7de57317a5c (diff) | |
download | compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.tar.gz compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.zip |
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
Diffstat (limited to 'backend/RTL.v')
-rw-r--r-- | backend/RTL.v | 42 |
1 files changed, 21 insertions, 21 deletions
diff --git a/backend/RTL.v b/backend/RTL.v index dec59ca2..31b5cf99 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -367,7 +367,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. @@ -465,8 +465,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 @@ -504,9 +504,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: @@ -514,12 +514,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: @@ -529,14 +529,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: @@ -554,7 +554,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: @@ -572,7 +572,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: @@ -582,8 +582,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. |