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 /kvx/PostpassSchedulingproof.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 'kvx/PostpassSchedulingproof.v')
-rw-r--r-- | kvx/PostpassSchedulingproof.v | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/kvx/PostpassSchedulingproof.v b/kvx/PostpassSchedulingproof.v index c290387b..937b3be6 100644 --- a/kvx/PostpassSchedulingproof.v +++ b/kvx/PostpassSchedulingproof.v @@ -20,6 +20,7 @@ Require Import Asmblockgenproof0 Asmblockprops. Require Import PostpassScheduling. Require Import Asmblockgenproof. Require Import Axioms. +Require Import Lia. Local Open Scope error_monad_scope. @@ -93,12 +94,12 @@ Proof. rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id. assert (size bb = size a + size b). { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r. - repeat (rewrite Nat2Z.inj_add). omega. } + repeat (rewrite Nat2Z.inj_add). lia. } clear EXA H0 H1. rewrite H in EXEB. assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. } rewrite H0. rewrite <- pc_set_add; auto. - exploit size_positive. instantiate (1 := a). intro. omega. - exploit size_positive. instantiate (1 := b). intro. omega. + exploit size_positive. instantiate (1 := a). intro. lia. + exploit size_positive. instantiate (1 := b). intro. lia. Qed. Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) : @@ -140,7 +141,7 @@ Lemma transf_function_no_overflow: transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned. Proof. intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. - omega. + lia. Qed. Lemma symbols_preserved: @@ -224,7 +225,7 @@ Proof. + apply IHlbb in H. destruct H as (c & TAIL). exists c. enough (pos = pos - size a + size a) as ->. apply code_tail_S; auto. - omega. + lia. Qed. Lemma code_tail_head_app: @@ -291,7 +292,7 @@ Lemma verified_schedule_not_empty: verified_schedule bb = OK lbb -> lbb <> nil. Proof. intros. apply verified_schedule_size in H. - pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g. + pose (size_positive bb). assert (size_blocks lbb > 0) by lia. clear H g. destruct lbb; simpl in *; discriminate. Qed. @@ -356,7 +357,7 @@ Proof. induction tc. - intros. simpl in H. discriminate. - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL. - + inv H. assert (k = k') by omega. subst. reflexivity. + + inv H. assert (k = k') by lia. subst. reflexivity. + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto. Qed. |