diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-06 23:47:28 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-06 23:47:28 +0100 |
| commit | 45e1539974db9c84d3e6466ac9c5f92afb1b08c6 (patch) | |
| tree | 2896cc93208966d51c70223779b5e2148211dbbf /backend/CSE3analysis.v | |
| parent | 5e6f8c2bc49dd2a27eb6886033e6687fb13030fd (diff) | |
| download | compcert-kvx-45e1539974db9c84d3e6466ac9c5f92afb1b08c6.tar.gz compcert-kvx-45e1539974db9c84d3e6466ac9c5f92afb1b08c6.zip | |
xlkills
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 64ddad11..34633cfc 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -186,7 +186,27 @@ Proof. - eapply IHeqs. eassumption. Qed. Hint Resolve xlget_kills_has_lhs : cse3. - + + +Lemma xlget_kills_has_arg : + forall eqs m lhs sop arg args j, + In (j, {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |}) eqs -> + In arg args -> + PSet.contains (Regmap.get arg (xlget_kills eqs m)) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros until j. + intros HEAD_TAIL ARG. + destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl. + - auto with cse3. + - eapply IHeqs; eassumption. +Qed. + +Hint Resolve xlget_kills_has_arg : cse3. + (* Lemma xget_kills_monotone : forall eqs m i j, |