diff options
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 143 |
1 files changed, 137 insertions, 6 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 1e5b88c3..b298ea65 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -133,13 +133,18 @@ Definition xlget_kills (eqs : list (eq_id * equation)) (m : Regmap.t PSet.t) : add_i_j (eq_lhs (snd item)) (fst item) (add_ilist_j (eq_args (snd item)) (fst item) already)) eqs m. - Definition xlget_mem_kills (eqs : list (positive * equation)) (m : PSet.t) : PSet.t := (fold_left (fun (a : PSet.t) (p : positive * equation) => if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a) eqs m). +Definition xlget_store_kills (eqs : list (positive * equation)) (m : PSet.t) : PSet.t := +(fold_left + (fun (a : PSet.t) (p : positive * equation) => + if eq_depends_on_store (snd p) then PSet.add (fst p) a else a) + eqs m). + Lemma xlget_kills_monotone : forall eqs m i j, PSet.contains (Regmap.get i m) j = true -> @@ -170,6 +175,24 @@ Qed. Hint Resolve xlget_mem_kills_monotone : cse3. +Lemma xlget_store_kills_monotone : + forall eqs m j, + PSet.contains m j = true -> + PSet.contains (xlget_store_kills eqs m) j = true. +Proof. + induction eqs; simpl; trivial. + intros. + destruct eq_depends_on_store. + - apply IHeqs. + destruct (peq (fst a) j). + + subst j. apply PSet.gadds. + + rewrite PSet.gaddo by congruence. + trivial. + - auto. +Qed. + +Hint Resolve xlget_store_kills_monotone : cse3. + Lemma xlget_kills_has_lhs : forall eqs m lhs sop args j, In (j, {| eq_lhs := lhs; @@ -333,6 +356,60 @@ Qed. Hint Resolve context_from_hints_get_kills_has_eq_depends_on_mem : cse3. +Lemma xlget_kills_has_eq_depends_on_store : + forall eqs eq j m, + In (j, eq) eqs -> + eq_depends_on_store eq = true -> + PSet.contains (xlget_store_kills eqs m) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros. + destruct H. + { subst a. + simpl. + rewrite H0. + apply xlget_store_kills_monotone. + apply PSet.gadds. + } + eauto. +Qed. + +Hint Resolve xlget_kills_has_eq_depends_on_store : cse3. + +Lemma get_kills_has_eq_depends_on_store : + forall eqs eq j, + PTree.get j eqs = Some eq -> + eq_depends_on_store eq = true -> + PSet.contains (get_store_kills eqs) j = true. +Proof. + intros. + unfold get_store_kills. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : PSet.t) (p : positive * equation) => + if eq_depends_on_store (snd p) then PSet.add (fst p) a else a) + (PTree.elements eqs) PSet.empty) + with (xlget_store_kills (PTree.elements eqs) PSet.empty). + eapply xlget_kills_has_eq_depends_on_store. + apply PTree.elements_correct. + eassumption. + trivial. +Qed. + +Lemma context_from_hints_get_kills_has_eq_depends_on_store : + forall hints eq j, + PTree.get j (hint_eq_catalog hints) = Some eq -> + eq_depends_on_store eq = true -> + PSet.contains (eq_kill_store (context_from_hints hints) tt) j = true. +Proof. + intros. + simpl. + eapply get_kills_has_eq_depends_on_store; eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_eq_depends_on_store : cse3. + Definition eq_involves (eq : equation) (i : reg) := i = (eq_lhs eq) \/ In i (eq_args eq). @@ -418,6 +495,12 @@ Section SOUNDNESS. eq_depends_on_mem eq = true -> PSet.contains (eq_kill_mem ctx tt) j = true. + Hypothesis ctx_kill_store_has_depends_on_store : + forall eq j, + eq_catalog ctx j = Some eq -> + eq_depends_on_store eq = true -> + PSet.contains (eq_kill_store ctx tt) j = true. + Theorem kill_reg_sound : forall rel rs m dst v, (sem_rel rel rs m) -> @@ -574,6 +657,55 @@ Section SOUNDNESS. Hint Resolve kill_mem_sound : cse3. + (* TODO: shouldn't this already be proved somewhere else? *) + Lemma store_preserves_validity: + forall m m' wchunk a v + (STORE : Mem.storev wchunk m a v = Some m') + (b : block) (z : Z), + Mem.valid_pointer m' b z = Mem.valid_pointer m b z. + Proof. + unfold Mem.storev. + intros. + destruct a; try discriminate. + Local Transparent Mem.store. + unfold Mem.store in STORE. + destruct Mem.valid_access_dec in STORE. + 2: discriminate. + inv STORE. + reflexivity. + Qed. + + Hint Resolve store_preserves_validity : cse3. + + Theorem kill_store_sound : + forall rel rs m m' wchunk a v, + (sem_rel rel rs m) -> + (Mem.storev wchunk m a v = Some m') -> + (sem_rel (kill_store (ctx:=ctx) rel) rs m'). + Proof. + unfold sem_rel, sem_eq, sem_rhs, kill_store. + intros until v. + intros REL STORE i eq. + specialize REL with (i := i) (eq0 := eq). + intros SUBTRACT CATALOG. + rewrite PSet.gsubtract in SUBTRACT. + rewrite andb_true_iff in SUBTRACT. + intuition. + destruct (eq_op eq) as [op | chunk addr] eqn:OP. + - rewrite op_valid_pointer_eq with (m2 := m). + assumption. + eapply store_preserves_validity; eauto. + - specialize ctx_kill_store_has_depends_on_store with (eq0 := eq) (j := i). + destruct eq as [lhs op args]; simpl in *. + rewrite OP in ctx_kill_store_has_depends_on_store. + rewrite negb_true_iff in H0. + rewrite OP in CATALOG. + intuition. + congruence. + Qed. + + Hint Resolve kill_store_sound : cse3. + Theorem eq_find_sound: forall no eq id, eq_find (ctx := ctx) no eq = Some id -> @@ -895,13 +1027,12 @@ Section SOUNDNESS. unfold sem_eq in *. simpl in *. destruct eq_op as [op' | chunk' addr']; simpl. - - destruct (op_depends_on_memory op') eqn:DEPENDS. - + erewrite ctx_kill_mem_has_depends_on_mem in CONTAINS by eauto. - discriminate. - + rewrite op_depends_on_memory_correct with (m2:=m); trivial. + - rewrite op_valid_pointer_eq with (m2 := m). + + cbn in *. apply REL; auto. + + eapply store_preserves_validity; eauto. - simpl in REL. - erewrite ctx_kill_mem_has_depends_on_mem in CONTAINS by eauto. + erewrite ctx_kill_store_has_depends_on_store in CONTAINS by eauto. simpl in CONTAINS. rewrite negb_true_iff in CONTAINS. destruct (eval_addressing genv sp addr' rs ## eq_args) as [a'|] eqn:ADDR'. |