From 5e2b2d9a6c85a2ed90eda0fe630a218e8b437c5f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 5 Mar 2020 18:21:46 +0100 Subject: just the analysis --- Makefile | 2 +- backend/CSE3.v | 78 ----------------------------------------------- backend/CSE3analysis.v | 81 +++++++++++++++++++++++++++++++++++++++++++++++++ extraction/extraction.v | 4 +-- 4 files changed, 84 insertions(+), 81 deletions(-) delete mode 100644 backend/CSE3.v create mode 100644 backend/CSE3analysis.v diff --git a/Makefile b/Makefile index e51bdb8a..dc368c66 100644 --- a/Makefile +++ b/Makefile @@ -89,7 +89,7 @@ BACKEND=\ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ CSE2deps.v CSE2depsproof.v \ CSE2.v CSE2proof.v \ - CSE3.v \ + CSE3analysis.v \ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ diff --git a/backend/CSE3.v b/backend/CSE3.v deleted file mode 100644 index 0ac56b36..00000000 --- a/backend/CSE3.v +++ /dev/null @@ -1,78 +0,0 @@ -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. - -Definition totoro := RELATION.lub. 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. diff --git a/extraction/extraction.v b/extraction/extraction.v index a258d4d8..ea30e7c2 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -36,7 +36,7 @@ Require Parser. Require Initializers. Require Asmaux. -Require CSE3. (* FIXME *) +Require CSE3analysis. (* FIXME *) (* Standard lib *) Require Import ExtrOcamlBasic. @@ -188,7 +188,7 @@ Set Extraction AccessOpaque. Cd "extraction". Separate Extraction - CSE3.totoro (* FIXME *) + CSE3analysis.totoro (* FIXME *) Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env -- cgit