diff options
| -rw-r--r-- | backend/Duplicate.v | 14 | ||||
| -rw-r--r-- | backend/Duplicateproof.v | 7 |
2 files changed, 20 insertions, 1 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index ce6c436f..a96d0826 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -2,7 +2,7 @@ structures *) Require Import AST RTL Maps Globalenvs. -Require Import Coqlib Errors. +Require Import Coqlib Errors Op. Local Open Scope error_monad_scope. Local Open Scope positive_scope. @@ -45,9 +45,21 @@ 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. + Definition verify_match_inst revmap inst tinst := match inst with | Inop n => match tinst with Inop n' => do u <- verify_is_copy revmap n n'; OK tt | _ => Error(msg "verify_match_inst Inop") end + | Iop op lr r n => match tinst with + Iop op' lr' r' n' => + do u <- verify_is_copy revmap n n'; + if (eq_operation op op') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then + OK tt + else Error (msg "Different r in Iop") + else Error (msg "Different lr in Iop") + else Error(msg "Different operations in Iop") + | _ => Error(msg "verify_match_inst Inop") end | _ => Error(msg "not implemented") end. diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index f3218f5f..d8ca9cd1 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -83,6 +83,13 @@ Proof. (* Inop *) - destruct i'; try (inversion H; fail). monadInv H. eapply verify_is_copy_correct_one. destruct x. eassumption. constructor; eauto. +(* Iop *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct (eq_operation _ _) eqn:EQO; try discriminate. + destruct (list_eq_dec _ _ _) eqn:LEQ; try discriminate. + destruct (Pos.eq_dec _ _) eqn:POS; try discriminate. clear EQ0. subst. + eapply verify_is_copy_correct_one. destruct x. eassumption. + constructor. Qed. Lemma verify_mapping_mn_correct: |