diff options
| -rw-r--r-- | backend/Duplicate.v | 17 | ||||
| -rw-r--r-- | backend/Duplicateproof.v | 9 | ||||
| -rw-r--r-- | lib/Integers.v | 5 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 6 |
4 files changed, 37 insertions, 0 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 24fb8e78..0f3c2ba9 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -69,6 +69,7 @@ Global Opaque builtin_res_eq_pos. 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'; @@ -80,6 +81,7 @@ Definition verify_match_inst revmap inst tinst := else Error (msg "Different lr in Iop") else Error(msg "Different operations in Iop") | _ => Error(msg "verify_match_inst Inop") end + | Iload m a lr r n => match tinst with | Iload m' a' lr' r' n' => do u <- verify_is_copy revmap n n'; @@ -92,6 +94,7 @@ Definition verify_match_inst revmap inst tinst := else Error (msg "Different addressing in Iload") else Error (msg "Different mchunk in Iload") | _ => Error (msg "verify_match_inst Iload") end + | Istore m a lr r n => match tinst with | Istore m' a' lr' r' n' => do u <- verify_is_copy revmap n n'; @@ -104,6 +107,7 @@ Definition verify_match_inst revmap inst tinst := else Error (msg "Different addressing in Istore") else Error (msg "Different mchunk in Istore") | _ => Error (msg "verify_match_inst Istore") end + | Icall s ri lr r n => match tinst with | Icall s' ri' lr' r' n' => do u <- verify_is_copy revmap n n'; @@ -116,6 +120,7 @@ Definition verify_match_inst revmap inst tinst := else Error (msg "Different ri in Icall") else Error (msg "Different signatures in Icall") | _ => Error (msg "verify_match_inst Icall") end + | Itailcall s ri lr => match tinst with | Itailcall s' ri' lr' => if (signature_eq s s') then @@ -125,6 +130,7 @@ Definition verify_match_inst revmap inst tinst := else Error (msg "Different ri in Itailcall") else Error (msg "Different signatures in Itailcall") | _ => Error (msg "verify_match_inst Itailcall") end + | Ibuiltin ef lbar brr n => match tinst with | Ibuiltin ef' lbar' brr' n' => do u <- verify_is_copy revmap n n'; @@ -135,6 +141,17 @@ Definition verify_match_inst revmap inst tinst := else Error (msg "Different lbar in Ibuiltin") else Error (msg "Different ef in Ibuiltin") | _ => Error (msg "verify_match_inst Ibuiltin") end + + | Icond cond lr n1 n2 => match tinst with + | Icond cond' lr' n1' n2' => + do u1 <- verify_is_copy revmap n1 n1'; + do u2 <- verify_is_copy revmap n2 n2'; + if (condition_eq cond cond') then + if (list_eq_dec Pos.eq_dec lr lr') then OK tt + else Error (msg "Different lr in Icond") + else Error (msg "Different cond in Icond") + | _ => Error (msg "verify_match_inst Icond") end + | Ireturn or => match tinst with | Ireturn or' => if (option_eq Pos.eq_dec or or') then OK tt diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index aa605bea..ba1fecc1 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -127,6 +127,15 @@ Proof. destruct (builtin_res_eq_pos _ _); try discriminate. eapply verify_is_copy_correct_one. destruct x. eassumption. subst. constructor. +(* 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 (condition_eq _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. subst. constructor; assumption. (* Ireturn *) - destruct i'; try (inversion H; fail). destruct (option_eq _ _ _); try discriminate. subst. clear H. diff --git a/lib/Integers.v b/lib/Integers.v index 9c6fcf1d..08a416c1 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -29,6 +29,11 @@ Inductive comparison : Type := | Cgt : comparison (**r greater than *) | Cge : comparison. (**r greater than or equal *) +Definition comparison_eq: forall (x y: comparison), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + Definition negate_comparison (c: comparison): comparison := match c with | Ceq => Cne diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index f9a774e8..ce9a5dcd 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -51,6 +51,12 @@ Inductive condition : Type := | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) | Cnotcompfs (c: comparison). (**r negation of a floating-point comparison *) +Definition condition_eq: forall (x y: condition), {x = y} + {x <> y}. +Proof. + generalize comparison_eq int_eq int64_eq. + decide equality. +Defined. + Inductive condition0 : Type := | Ccomp0 (c: comparison) (**r signed integer comparison with 0 *) | Ccompu0 (c: comparison) (**r unsigned integer comparison with 0 *) |