diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-10-07 17:06:06 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-10-07 17:06:06 +0200 |
commit | cb7d444a5a97626a794f2167c2a4bc4d51f4ed67 (patch) | |
tree | ea436e9752befd8b1fba3080e0badb330fc361e2 | |
parent | 5ffa8534d09272e5f44c51193e74cffdbc2b043c (diff) | |
download | compcert-kvx-cb7d444a5a97626a794f2167c2a4bc4d51f4ed67.tar.gz compcert-kvx-cb7d444a5a97626a794f2167c2a4bc4d51f4ed67.zip |
Finished Duplicate proof.
-rw-r--r-- | backend/Duplicate.v | 19 | ||||
-rw-r--r-- | backend/Duplicateproof.v | 75 |
2 files changed, 58 insertions, 36 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 0f3c2ba9..d1458bd4 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -45,6 +45,17 @@ Definition verify_is_copy revmap n n' := | Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end end. +Fixpoint verify_is_copy_list revmap ln ln' := + match ln with + | n::ln => match ln' with + | n'::ln' => do u <- verify_is_copy revmap n n'; + verify_is_copy_list revmap ln ln' + | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end + | nil => match ln' with + | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'") + | nil => OK tt end + end. + Lemma product_eq {A B: Type} : (forall (a b: A), {a=b} + {a<>b}) -> (forall (c d: B), {c=d} + {c<>d}) -> @@ -152,12 +163,18 @@ Definition verify_match_inst revmap inst tinst := else Error (msg "Different cond in Icond") | _ => Error (msg "verify_match_inst Icond") end + | Ijumptable r ln => match tinst with + | Ijumptable r' ln' => + do u <- verify_is_copy_list revmap ln ln'; + if (Pos.eq_dec r r') then OK tt + else Error (msg "Different r in Ijumptable") + | _ => Error (msg "verify_match_inst Ijumptable") end + | Ireturn or => match tinst with | Ireturn or' => if (option_eq Pos.eq_dec or or') then OK tt else Error (msg "Different or in Ireturn") | _ => Error (msg "verify_match_inst Ireturn") end - | _ => Error(msg "not implemented") end. Definition verify_mapping_mn f xf (m: positive*positive) := diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index ba1fecc1..54dd6196 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -51,26 +51,26 @@ Proof. + monadInv H0. destruct x0. eapply IHlb; assumption. Qed. -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', +Lemma verify_is_copy_correct: + forall xf n n', verify_is_copy (fn_revmap xf) n n' = OK tt -> - rtl_one_successor n n' i i' -> - match_inst (fun nn => (fn_revmap xf) ! nn) i i'. + (fn_revmap xf) ! n' = Some n. 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. + destruct (n ?= n0) eqn:NP; try (inversion H; fail). eapply Pos.compare_eq in NP. subst. - inv H0. - all: constructor; eauto. + reflexivity. +Qed. + +Lemma verify_is_copy_list_correct: + forall xf ln ln', + verify_is_copy_list (fn_revmap xf) ln ln' = OK tt -> + list_forall2 (fun n n' => (fn_revmap xf) ! n' = Some n) ln ln'. +Proof. + induction ln. + - intros. destruct ln'; monadInv H. constructor. + - intros. destruct ln'; monadInv H. destruct x. apply verify_is_copy_correct in EQ. + eapply IHln in EQ0. constructor; assumption. Qed. Lemma verify_match_inst_correct: @@ -81,39 +81,40 @@ 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_one. destruct x. eassumption. + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. constructor; eauto. (* Iop *) - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. destruct (eq_operation _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst. - eapply verify_is_copy_correct_one. destruct x. eassumption. - constructor. + constructor. assumption. (* Iload *) - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. destruct (chunk_eq _ _); try discriminate. destruct (eq_addressing _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst. - eapply verify_is_copy_correct_one. destruct x. eassumption. - constructor. + constructor. assumption. (* Istore *) - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. destruct (chunk_eq _ _); try discriminate. destruct (eq_addressing _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst. - eapply verify_is_copy_correct_one. destruct x. eassumption. - constructor. + constructor. assumption. (* Icall *) - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. destruct (signature_eq _ _); try discriminate. destruct (product_eq _ _ _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. - destruct (Pos.eq_dec _ _); try discriminate. - eapply verify_is_copy_correct_one. destruct x. eassumption. subst. - constructor. + destruct (Pos.eq_dec _ _); try discriminate. subst. + constructor. assumption. (* Itailcall *) - destruct i'; try (inversion H; fail). destruct (signature_eq _ _); try discriminate. @@ -122,26 +123,30 @@ Proof. constructor. (* Ibuiltin *) - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. destruct (external_function_eq _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. - destruct (builtin_res_eq_pos _ _); try discriminate. - eapply verify_is_copy_correct_one. destruct x. eassumption. subst. - constructor. + destruct (builtin_res_eq_pos _ _); try discriminate. subst. + constructor. assumption. (* Icond *) - destruct i'; try (inversion H; fail). monadInv H. - unfold verify_is_copy in EQ, EQ1. - destruct (_ ! n1) eqn:REVM; [|inversion EQ]. - destruct (n ?= p) eqn:NP; try (inversion EQ; fail). eapply Pos.compare_eq in NP. subst. inv EQ. - destruct (_ ! n2) eqn:REVMM; [|inversion EQ1]. - destruct (n0 ?= p0) eqn:NP0; try (inversion EQ1; fail). eapply Pos.compare_eq in NP0. subst. inv EQ1. + destruct x. eapply verify_is_copy_correct in EQ. + destruct x0. eapply verify_is_copy_correct in EQ1. destruct (condition_eq _ _); try discriminate. - destruct (list_eq_dec _ _ _); try discriminate. subst. constructor; assumption. + destruct (list_eq_dec _ _ _); try discriminate. subst. + constructor; assumption. +(* Ijumptable *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_list_correct in EQ. + destruct (Pos.eq_dec _ _); try discriminate. subst. + constructor. assumption. (* Ireturn *) - destruct i'; try (inversion H; fail). destruct (option_eq _ _ _); try discriminate. subst. clear H. constructor. Qed. + Lemma verify_mapping_mn_correct: forall mp n n' i f xf tc, mp ! n' = Some n -> |