diff options
| -rw-r--r-- | backend/CSE3analysis.v | 13 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 78 | ||||
| -rw-r--r-- | lib/HashedSet.v | 2 |
3 files changed, 89 insertions, 4 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 257149b5..485b6067 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -88,7 +88,7 @@ Record equation := eq_op : sym_op; eq_args : list reg }. -Definition eq_id := positive. +Definition eq_id := node. Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) := Regmap.set i (PSet.add j (Regmap.get i m)) m. @@ -103,4 +103,15 @@ Definition get_kills (eqs : PTree.t equation) : (add_ilist_j (eq_args eq) eqno already)) eqs (PMap.init PSet.empty). +Record eq_context := mkeqcontext + { eq_catalog : node -> option equation; + eq_kills : reg -> PSet.t }. + +Section OPERATIONS. + Context {ctx : eq_context}. + + Definition kill_reg (r : reg) (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kills ctx r). +End OPERATIONS. + Definition totoro := RELATION.lub. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index af42a2e8..d3681398 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -9,6 +9,24 @@ Require Import Registers Op RTL. Require Import CSE3analysis CSE2deps CSE2depsproof HashedSet. Require Import Lia. +Lemma subst_args_notin : + forall (rs : regset) dst v args, + ~ In dst args -> + (rs # dst <- v) ## args = rs ## args. +Proof. + induction args; simpl; trivial. + intro NOTIN. + destruct (peq a dst). + { + subst a. + intuition congruence. + } + rewrite Regmap.gso by congruence. + f_equal. + apply IHargs. + intuition congruence. +Qed. + Lemma add_i_j_adds : forall i j m, PSet.contains (Regmap.get i (add_i_j i j m)) j = true. Proof. @@ -159,7 +177,7 @@ Section SOUNDNESS. Variable genv: Genv.t F V. Variable sp : val. - Variable eq_catalog : PTree.t equation. + Context {ctx : eq_context}. Definition sem_eq (eq : equation) (rs : regset) (m : mem) := match eq_op eq with @@ -183,6 +201,62 @@ Section SOUNDNESS. Definition sem_rel (rel : RELATION.t) (rs : regset) (m : mem) := forall i eq, PSet.contains rel i = true -> - PTree.get i eq_catalog = Some eq -> + eq_catalog ctx i = Some eq -> sem_eq eq rs m. + + Hypothesis ctx_kills_has_lhs : + forall lhs sop args j, + eq_catalog ctx j = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + PSet.contains (eq_kills ctx lhs) j = true. + + Hypothesis ctx_kills_has_arg : + forall lhs sop args j, + eq_catalog ctx j = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + forall arg, + In arg args -> + PSet.contains (eq_kills ctx arg) j = true. + + Theorem kill_reg_sound : + forall rel rs m dst v, + (sem_rel rel rs m) -> + (sem_rel (kill_reg (ctx:=ctx) dst rel) (rs#dst <- v) m). + Proof. + unfold sem_rel, sem_eq, kill_reg. + intros until v. + intros REL i eq. + specialize REL with (i := i) (eq0 := eq). + destruct eq as [lhs sop args]; simpl. + specialize ctx_kills_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i). + specialize ctx_kills_has_arg with (lhs := lhs) (sop := sop) (args := args) (j := i) (arg := dst). + intuition. + rewrite PSet.gsubtract in H. + rewrite andb_true_iff in H. + rewrite negb_true_iff in H. + intuition. + simpl in *. + assert ({In dst args} + {~In dst args}) as IN_ARGS. + { + apply List.in_dec. + apply peq. + } + destruct IN_ARGS as [IN_ARGS | NOTIN_ARGS]. + { intuition. + congruence. + } + destruct (peq dst lhs). + { + congruence. + } + rewrite subst_args_notin by assumption. + destruct sop. + - destruct (eval_operation genv sp o rs ## args m) as [ev | ]; trivial. + rewrite Regmap.gso by congruence. + assumption. + - rewrite Regmap.gso by congruence. + assumption. + Qed. End SOUNDNESS. diff --git a/lib/HashedSet.v b/lib/HashedSet.v index 5b4faeaa..bd9cd9c0 100644 --- a/lib/HashedSet.v +++ b/lib/HashedSet.v @@ -52,7 +52,7 @@ Proof. destruct b; reflexivity. Qed. -Hint Rewrite orb_false_r andb_false_r andb_true_r orb_true_r orb_idem andb_idem andb_negb_false: pset. +Hint Rewrite orb_false_r andb_false_r andb_true_r orb_true_r orb_idem andb_idem andb_negb_false : pset. Module PSet_internals. Inductive pset : Type := |