diff options
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 155fedef..cd27a506 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -189,6 +189,22 @@ Proof. eassumption. Qed. +Hint Resolve get_kills_has_lhs : cse3. + +Lemma context_from_hints_get_kills_has_lhs : + forall hints lhs sop args j, + PTree.get j (hint_eq_catalog hints) = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + PSet.contains (eq_kill_reg (context_from_hints hints) lhs) j = true. +Proof. + intros; simpl. + eapply get_kills_has_lhs. + eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_lhs : cse3. + Lemma get_kills_has_arg : forall eqs lhs sop arg args j, PTree.get j eqs = Some {| eq_lhs := lhs; @@ -212,6 +228,21 @@ Qed. Hint Resolve get_kills_has_arg : cse3. +Lemma context_from_hints_get_kills_has_arg : + forall hints lhs sop arg args j, + PTree.get j (hint_eq_catalog hints) = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + In arg args -> + PSet.contains (eq_kill_reg (context_from_hints hints) arg) j = true. +Proof. + intros. + simpl. + eapply get_kills_has_arg; eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_arg : cse3. + Definition eq_involves (eq : equation) (i : reg) := i = (eq_lhs eq) \/ In i (eq_args eq). |