diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-10-03 16:13:07 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-10-03 16:13:07 +0200 |
| commit | b59eb881ad3fd72b8743fb48d90e2751dc996e77 (patch) | |
| tree | 0d596444e0801ea4af858abfaa88963f5624e40c /backend/Duplicateproof.v | |
| parent | 537857a59def9c9fb16035ac81c121b1ae176b66 (diff) | |
| download | compcert-kvx-b59eb881ad3fd72b8743fb48d90e2751dc996e77.tar.gz compcert-kvx-b59eb881ad3fd72b8743fb48d90e2751dc996e77.zip | |
Preparing the terrain for the rest of the instructions with one successor
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 22 |
1 files changed, 17 insertions, 5 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 3a6d6920..f3218f5f 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -51,15 +51,26 @@ Proof. + monadInv H0. destruct x0. eapply IHlb; assumption. Qed. -Lemma verify_is_copy_correct: - forall xf n n', +Inductive rtl_one_successor : node -> node -> instruction -> instruction -> Prop := + | inop_one_succ : forall n n', rtl_one_successor n n' (Inop n) (Inop n') + | iop_one_succ : forall op lr r n n', rtl_one_successor n n' (Iop op lr r n) (Iop op lr r n') + | iload_one_succ : forall m a lr r n n', rtl_one_successor n n' (Iload m a lr r n) (Iload m a lr r n') + | istore_one_succ : forall m a lr r n n', rtl_one_successor n n' (Istore m a lr r n) (Istore m a lr r n') + | icall_one_succ : forall s ri lr r n n', rtl_one_successor n n' (Icall s ri lr r n) (Icall s ri lr r n') + | ibuiltin_one_succ : forall ef lbr br n n', rtl_one_successor n n' (Ibuiltin ef lbr br n) (Ibuiltin ef lbr br n') +. + +Lemma verify_is_copy_correct_one: + forall xf n n' i i', verify_is_copy (fn_revmap xf) n n' = OK tt -> - match_inst (fun nn => (fn_revmap xf) ! nn) (Inop n) (Inop n'). + rtl_one_successor n n' i i' -> + match_inst (fun nn => (fn_revmap xf) ! nn) i i'. Proof. intros. unfold verify_is_copy in H. destruct (_ ! n') eqn:REVM; [|inversion H]. destruct (n ?= p) eqn:NP; try (inversion H; fail). clear H. eapply Pos.compare_eq in NP. subst. - constructor; eauto. + inv H0. + all: constructor; eauto. Qed. Lemma verify_match_inst_correct: @@ -70,7 +81,8 @@ Proof. intros. unfold verify_match_inst in H. destruct i; try (inversion H; fail). (* Inop *) - - destruct i'; try (inversion H; fail). monadInv H. eapply verify_is_copy_correct. destruct x. assumption. + - destruct i'; try (inversion H; fail). monadInv H. eapply verify_is_copy_correct_one. destruct x. eassumption. + constructor; eauto. Qed. Lemma verify_mapping_mn_correct: |