diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-05 18:21:46 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-05 18:21:46 +0100 |
commit | 5e2b2d9a6c85a2ed90eda0fe630a218e8b437c5f (patch) | |
tree | 1e74a15034fe762df2b44289b1cb7d1ccac31a99 /backend/CSE3analysis.v | |
parent | 746b4cd3895462be7959389ef39696294177e465 (diff) | |
download | compcert-kvx-5e2b2d9a6c85a2ed90eda0fe630a218e8b437c5f.tar.gz compcert-kvx-5e2b2d9a6c85a2ed90eda0fe630a218e8b437c5f.zip |
just the analysis
Diffstat (limited to 'backend/CSE3analysis.v')
-rw-r--r-- | backend/CSE3analysis.v | 81 |
1 files changed, 81 insertions, 0 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v new file mode 100644 index 00000000..06de1b08 --- /dev/null +++ b/backend/CSE3analysis.v @@ -0,0 +1,81 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps CSE2deps. +Require Import HashedSet. + +Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. + Definition t := PSet.t. + Definition eq (x : t) (y : t) := x = y. + + Lemma eq_refl: forall x, eq x x. + Proof. + unfold eq. trivial. + Qed. + + Lemma eq_sym: forall x y, eq x y -> eq y x. + Proof. + unfold eq. congruence. + Qed. + + Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Proof. + unfold eq. congruence. + Qed. + + Definition beq (x y : t) := if PSet.eq x y then true else false. + + Lemma beq_correct: forall x y, beq x y = true -> eq x y. + Proof. + unfold beq. + intros. + destruct PSet.eq; congruence. + Qed. + + Definition ge (x y : t) := (PSet.is_subset x y) = true. + + Lemma ge_refl: forall x y, eq x y -> ge x y. + Proof. + unfold eq, ge. + intros. + subst y. + apply PSet.is_subset_spec. + trivial. + Qed. + + Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Proof. + unfold ge. + intros. + rewrite PSet.is_subset_spec in *. + intuition. + Qed. + + Definition lub := PSet.inter. + + Lemma ge_lub_left: forall x y, ge (lub x y) x. + Proof. + unfold ge, lub. + intros. + apply PSet.is_subset_spec. + intro. + rewrite PSet.ginter. + rewrite andb_true_iff. + intuition. + Qed. + + Lemma ge_lub_right: forall x y, ge (lub x y) y. + Proof. + unfold ge, lub. + intros. + apply PSet.is_subset_spec. + intro. + rewrite PSet.ginter. + rewrite andb_true_iff. + intuition. + Qed. +End RELATION. + +Module RB := ADD_BOTTOM(RELATION). +Module DS := Dataflow_Solver(RB)(NodeSetForward). + +Definition totoro := RELATION.lub. |