diff options
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 1421 |
1 files changed, 1421 insertions, 0 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v new file mode 100644 index 00000000..523b52df --- /dev/null +++ b/backend/CSE3analysisproof.v @@ -0,0 +1,1421 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE3analysis CSE2deps CSE2depsproof HashedSet. +Require Import RTLtyping. +Require Import Lia. + +Lemma rel_leb_correct: + forall x x', + rel_leb x x' = true <-> RELATION.ge x' x. +Proof. + unfold rel_leb, RELATION.ge. + split; auto. +Qed. + +Hint Resolve rel_leb_correct : cse3. + +Lemma relb_leb_correct: + forall x x', + relb_leb x x' = true <-> RB.ge x' x. +Proof. + unfold relb_leb, RB.ge. + destruct x; destruct x'; split; trivial; try contradiction; discriminate. +Qed. + +Hint Resolve relb_leb_correct : cse3. + +Theorem loadv_storev_really_same: + forall chunk: memory_chunk, + forall m1: mem, + forall addr v: val, + forall m2: mem, + forall ty : typ, + forall TYPE: Val.has_type v ty, + forall STORE: Mem.storev chunk m1 addr v = Some m2, + forall COMPATIBLE: loadv_storev_compatible_type chunk ty = true, + Mem.loadv chunk m2 addr = Some v. +Proof. + intros. + rewrite Mem.loadv_storev_same with (m1:=m1) (v:=v) by assumption. + f_equal. + destruct chunk; destruct ty; try discriminate. + all: destruct v; trivial; try contradiction. + all: unfold Val.load_result, Val.has_type in *. + all: destruct Archi.ptr64; trivial; discriminate. +Qed. + +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. + intros. + unfold add_i_j. + rewrite Regmap.gss. + auto with pset. +Qed. +Hint Resolve add_i_j_adds: cse3. + +Lemma add_i_j_monotone : forall i j i' j' m, + PSet.contains (Regmap.get i' m) j' = true -> + PSet.contains (Regmap.get i' (add_i_j i j m)) j' = true. +Proof. + intros. + unfold add_i_j. + destruct (peq i i'). + - subst i'. + rewrite Regmap.gss. + destruct (peq j j'). + + subst j'. + apply PSet.gadds. + + eauto with pset. + - rewrite Regmap.gso. + assumption. + congruence. +Qed. + +Hint Resolve add_i_j_monotone: cse3. + +Lemma add_ilist_j_monotone : forall ilist j i' j' m, + PSet.contains (Regmap.get i' m) j' = true -> + PSet.contains (Regmap.get i' (add_ilist_j ilist j m)) j' = true. +Proof. + induction ilist; simpl; intros until m; intro CONTAINS; auto with cse3. +Qed. +Hint Resolve add_ilist_j_monotone: cse3. + +Lemma add_ilist_j_adds : forall ilist j m, + forall i, In i ilist -> + PSet.contains (Regmap.get i (add_ilist_j ilist j m)) j = true. +Proof. + induction ilist; simpl; intros until i; intro IN. + contradiction. + destruct IN as [HEAD | TAIL]; subst; auto with cse3. +Qed. +Hint Resolve add_ilist_j_adds: cse3. + +Definition xlget_kills (eqs : list (eq_id * equation_or_condition)) + (m : Regmap.t PSet.t) : + Regmap.t PSet.t := + List.fold_left (fun already (item : eq_id * equation_or_condition) => + match snd item with + | Equ lhs sop args => + add_i_j lhs (fst item) + (add_ilist_j args (fst item) already) + | Cond cond args => add_ilist_j args (fst item) already + end) eqs m. + +Definition xlget_mem_kills (eqs : list (positive * equation_or_condition)) + (m : PSet.t) : PSet.t := +(fold_left + (fun (a : PSet.t) (item : positive * equation_or_condition) => + if eq_cond_depends_on_mem (snd item) + then PSet.add (fst item) a + else a + ) + eqs m). + +Definition xlget_store_kills (eqs : list (positive * equation_or_condition)) + (m : PSet.t) : PSet.t := +(fold_left + (fun (a : PSet.t) (item : positive * equation_or_condition) => + if eq_cond_depends_on_store (snd item) + then PSet.add (fst item) a + else a + ) + eqs m). + +Lemma xlget_kills_monotone : + forall eqs m i j, + PSet.contains (Regmap.get i m) j = true -> + PSet.contains (Regmap.get i (xlget_kills eqs m)) j = true. +Proof. + induction eqs; simpl; trivial. + intros. + destruct a as [id eq_cond]; cbn. + destruct eq_cond as [eq_lhs eq_sop eq_args | eq_cond eq_args]; auto with cse3. +Qed. + +Hint Resolve xlget_kills_monotone : cse3. + +Lemma xlget_mem_kills_monotone : + forall eqs m j, + PSet.contains m j = true -> + PSet.contains (xlget_mem_kills eqs m) j = true. +Proof. + induction eqs; simpl; trivial. + intros. + destruct a as [id eq_cond]; cbn. + destruct eq_cond_depends_on_mem. + - apply IHeqs. + destruct (peq id j). + + subst j. apply PSet.gadds. + + rewrite PSet.gaddo by congruence. + trivial. + - auto. +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 a as [id eq_cond]; cbn. + destruct eq_cond_depends_on_store. + - apply IHeqs. + destruct (peq id 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, (Equ lhs sop args)) eqs -> + PSet.contains (Regmap.get lhs (xlget_kills eqs m)) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros until j. + intro HEAD_TAIL. + destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl. + - auto with cse3. + - 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, (Equ lhs sop 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 xlget_cond_kills_has_arg : + forall eqs m cond arg args j, + In (j, (Cond cond 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_cond_kills_has_arg : cse3. + +Lemma get_kills_has_lhs : + forall eqs lhs sop args j, + PTree.get j eqs = Some (Equ lhs sop args) -> + PSet.contains (Regmap.get lhs (get_reg_kills eqs)) j = true. +Proof. + unfold get_reg_kills. + intros. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : Regmap.t PSet.t) (p : positive * equation_or_condition) => + match snd p with + | Equ lhs0 _ args0 => + add_i_j lhs0 (fst p) (add_ilist_j args0 (fst p) a) + | Cond _ args0 => add_ilist_j args0 (fst p) a + end)) with xlget_kills. + eapply xlget_kills_has_lhs. + apply PTree.elements_correct. + eassumption. +Qed. + +Hint Resolve get_kills_has_lhs : cse3. + +Lemma context_from_hints_get_kills_has_lhs : + forall hints lhs sop args j, + PTree.get j (hint_eq_catalog hints) = Some (Equ lhs sop args) -> + PSet.contains (eq_kill_reg (context_from_hints hints) lhs) j = true. +Proof. + intros; simpl. + eapply get_kills_has_lhs. + eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_lhs : cse3. + +Lemma get_kills_has_arg : + forall eqs lhs sop arg args j, + PTree.get j eqs = Some (Equ lhs sop args) -> + In arg args -> + PSet.contains (Regmap.get arg (get_reg_kills eqs)) j = true. +Proof. + unfold get_reg_kills. + intros. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : Regmap.t PSet.t) (p : positive * equation_or_condition) => + match snd p with + | Equ lhs0 _ args0 => + add_i_j lhs0 (fst p) (add_ilist_j args0 (fst p) a) + | Cond _ args0 => add_ilist_j args0 (fst p) a + end)) with xlget_kills. + eapply xlget_kills_has_arg. + - apply PTree.elements_correct. + eassumption. + - assumption. +Qed. + +Hint Resolve get_kills_has_arg : cse3. + +Lemma context_from_hints_get_kills_has_arg : + forall hints lhs sop arg args j, + PTree.get j (hint_eq_catalog hints) = Some (Equ lhs sop args) -> + In arg args -> + PSet.contains (eq_kill_reg (context_from_hints hints) arg) j = true. +Proof. + intros. + simpl. + eapply get_kills_has_arg; eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_arg : cse3. + +Lemma get_cond_kills_has_arg : + forall eqs cond arg args j, + PTree.get j eqs = Some (Cond cond args) -> + In arg args -> + PSet.contains (Regmap.get arg (get_reg_kills eqs)) j = true. +Proof. + unfold get_reg_kills. + intros. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : Regmap.t PSet.t) (p : positive * equation_or_condition) => + match snd p with + | Equ lhs0 _ args0 => + add_i_j lhs0 (fst p) (add_ilist_j args0 (fst p) a) + | Cond _ args0 => add_ilist_j args0 (fst p) a + end)) with xlget_kills. + eapply xlget_cond_kills_has_arg. + - apply PTree.elements_correct. + eassumption. + - assumption. +Qed. + +Hint Resolve get_cond_kills_has_arg : cse3. + +Lemma context_from_hints_get_cond_kills_has_arg : + forall hints cond arg args j, + PTree.get j (hint_eq_catalog hints) = Some (Cond cond args) -> + In arg args -> + PSet.contains (eq_kill_reg (context_from_hints hints) arg) j = true. +Proof. + intros. + simpl. + eapply get_cond_kills_has_arg; eassumption. +Qed. + +Hint Resolve context_from_hints_get_cond_kills_has_arg : cse3. + +Lemma xlget_kills_has_eq_depends_on_mem : + forall eqs eq j m, + In (j, eq) eqs -> + eq_cond_depends_on_mem eq = true -> + PSet.contains (xlget_mem_kills eqs m) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros. + destruct H. + { subst a. + simpl. + rewrite H0. + apply xlget_mem_kills_monotone. + apply PSet.gadds. + } + eauto. +Qed. + +Hint Resolve xlget_kills_has_eq_depends_on_mem : cse3. + +Lemma get_kills_has_eq_depends_on_mem : + forall eqs eq j, + PTree.get j eqs = Some eq -> + eq_cond_depends_on_mem eq = true -> + PSet.contains (get_mem_kills eqs) j = true. +Proof. + intros. + unfold get_mem_kills. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : PSet.t) (p : positive * equation_or_condition) => + if eq_cond_depends_on_mem (snd p) then PSet.add (fst p) a else a)) + with xlget_mem_kills. + eapply xlget_kills_has_eq_depends_on_mem. + apply PTree.elements_correct. + eassumption. + trivial. +Qed. + +Lemma context_from_hints_get_kills_has_eq_depends_on_mem : + forall hints eq j, + PTree.get j (hint_eq_catalog hints) = Some eq -> + eq_cond_depends_on_mem eq = true -> + PSet.contains (eq_kill_mem (context_from_hints hints) tt) j = true. +Proof. + intros. + simpl. + eapply get_kills_has_eq_depends_on_mem; eassumption. +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_cond_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_cond_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_or_condition) => + if eq_cond_depends_on_store (snd p) then PSet.add (fst p) a else a)) + with xlget_store_kills. + 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_cond_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_or_condition) (i : reg) := + match eq with + | Equ lhs sop args => + i = lhs \/ In i args + | Cond cond args => In i args + end. + +Section SOUNDNESS. + Context {F V : Type}. + Context {genv: Genv.t F V}. + Context {sp : val}. + + Context {ctx : eq_context}. + + Definition sem_rhs (sop : sym_op) (args : list reg) + (rs : regset) (m : mem) (v' : val) := + match sop with + | SOp op => + match eval_operation genv sp op (rs ## args) m with + | Some v => v' = v + | None => False + end + | SLoad chunk addr => + match + match eval_addressing genv sp addr (rs ## args) with + | Some a => Mem.loadv chunk m a + | None => None + end + with + | Some dat => v' = dat + | None => v' = Vundef + end + end. + + Definition sem_eq (eq : equation_or_condition) (rs : regset) (m : mem) := + match eq with + | Equ lhs sop args => sem_rhs sop args rs m (rs # lhs) + | Cond cond args => eval_condition cond (rs ## args) m = Some true + end. + + Definition sem_rel (rel : RELATION.t) (rs : regset) (m : mem) := + forall i eq, + PSet.contains rel i = true -> + eq_catalog ctx i = Some eq -> + sem_eq eq rs m. + + Lemma sem_rel_glb: + forall rel1 rel2 rs m, + (sem_rel (RELATION.glb rel1 rel2) rs m) <-> + ((sem_rel rel1 rs m) /\ + (sem_rel rel2 rs m)). + Proof. + intros. + unfold sem_rel, RELATION.glb. + split. + - intro IMPLIES. + split; + intros i eq CONTAINS; + specialize IMPLIES with (i:=i) (eq0:=eq); + rewrite PSet.gunion in IMPLIES; + rewrite orb_true_iff in IMPLIES; + intuition. + - intros (IMPLIES1 & IMPLIES2) i eq. + rewrite PSet.gunion. + rewrite orb_true_iff. + specialize IMPLIES1 with (i:=i) (eq0:=eq). + specialize IMPLIES2 with (i:=i) (eq0:=eq). + intuition. + Qed. + + Hypothesis ctx_kill_reg_has_lhs : + forall lhs sop args j, + eq_catalog ctx j = Some (Equ lhs sop args) -> + PSet.contains (eq_kill_reg ctx lhs) j = true. + + Hypothesis ctx_kill_reg_has_arg : + forall lhs sop args j, + eq_catalog ctx j = Some (Equ lhs sop args) -> + forall arg, + In arg args -> + PSet.contains (eq_kill_reg ctx arg) j = true. + + Hypothesis ctx_cond_kill_reg_has_arg : + forall cond args j, + eq_catalog ctx j = Some (Cond cond args) -> + forall arg, + In arg args -> + PSet.contains (eq_kill_reg ctx arg) j = true. + + Hypothesis ctx_kill_mem_has_depends_on_mem : + forall eq j, + eq_catalog ctx j = Some eq -> + eq_cond_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_cond_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) -> + (sem_rel (kill_reg (ctx:=ctx) dst rel) (rs#dst <- v) m). + Proof. + unfold sem_rel, sem_eq, sem_rhs, kill_reg. + intros until v. + intros REL i eq. + specialize REL with (i := i) (eq0 := eq). + destruct eq as [lhs sop args | cond args]; simpl. + * specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i). + specialize ctx_kill_reg_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. + * specialize ctx_cond_kill_reg_has_arg with (cond := cond) (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. + } + rewrite subst_args_notin by assumption. + assumption. + Qed. + + Hint Resolve kill_reg_sound : cse3. + + Theorem kill_reg_sound2 : + forall rel rs m dst, + (sem_rel rel rs m) -> + (sem_rel (kill_reg (ctx:=ctx) dst rel) rs m). + Proof. + unfold sem_rel, sem_eq, sem_rhs, kill_reg. + intros until dst. + intros REL i eq. + specialize REL with (i := i) (eq0 := eq). + destruct eq as [lhs sop args | cond args]; simpl. + * specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i). + specialize ctx_kill_reg_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. + * specialize ctx_cond_kill_reg_has_arg with (cond := cond) (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. + Qed. + + Lemma pick_source_sound : + forall (l : list reg), + match pick_source l with + | Some x => In x l + | None => True + end. + Proof. + unfold pick_source. + destruct l; simpl; trivial. + left; trivial. + Qed. + + Hint Resolve pick_source_sound : cse3. + + Theorem forward_move_sound : + forall rel rs m x, + (sem_rel rel rs m) -> + rs # (forward_move (ctx := ctx) rel x) = rs # x. + Proof. + unfold sem_rel, forward_move. + intros until x. + intro REL. + pose proof (pick_source_sound (PSet.elements (PSet.inter rel (eq_moves ctx x)))) as ELEMENT. + destruct (pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x)))). + 2: reflexivity. + destruct (eq_catalog ctx r) as [eq | ] eqn:CATALOG. + 2: reflexivity. + specialize REL with (i := r) (eq0 := eq). + destruct eq as [lhs sop args | cond args]; cbn in *; trivial. + destruct (is_smove sop) as [MOVE | ]. + 2: reflexivity. + rewrite MOVE in *; cbn in *. + destruct (peq x lhs). + 2: reflexivity. + simpl. + subst x. + rewrite PSet.elements_spec in ELEMENT. + rewrite PSet.ginter in ELEMENT. + rewrite andb_true_iff in ELEMENT. + unfold sem_eq in REL. + simpl in REL. + destruct args as [ | h t]. + reflexivity. + destruct t. + 2: reflexivity. + simpl in REL. + intuition congruence. + Qed. + + Hint Resolve forward_move_sound : cse3. + + Theorem forward_move_l_sound : + forall rel rs m l, + (sem_rel rel rs m) -> + rs ## (forward_move_l (ctx := ctx) rel l) = rs ## l. + Proof. + induction l; simpl; intros; trivial. + erewrite forward_move_sound by eassumption. + intuition congruence. + Qed. + + Hint Resolve forward_move_l_sound : cse3. + + Theorem kill_mem_sound : + forall rel rs m m', + (sem_rel rel rs m) -> + (sem_rel (kill_mem (ctx:=ctx) rel) rs m'). + Proof. + unfold sem_rel, sem_eq, sem_rhs, kill_mem. + intros until m'. + intros REL 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 as [lhs sop args | cond args] eqn:EQ. + * destruct sop as [op | chunk addr] eqn:OP. + - specialize ctx_kill_mem_has_depends_on_mem with (eq0 := eq) (j := i). + rewrite EQ in ctx_kill_mem_has_depends_on_mem. + unfold eq_cond_depends_on_mem in ctx_kill_mem_has_depends_on_mem. + rewrite (op_depends_on_memory_correct genv sp op) with (m2 := m). + assumption. + destruct (op_depends_on_memory op) in *; trivial. + rewrite ctx_kill_mem_has_depends_on_mem in H0; trivial. + discriminate H0. + - specialize ctx_kill_mem_has_depends_on_mem with (eq0 := eq) (j := i). + rewrite EQ in ctx_kill_mem_has_depends_on_mem. + rewrite negb_true_iff in H0. + intuition. + congruence. + * specialize ctx_kill_mem_has_depends_on_mem with (eq0 := eq) (j := i). + rewrite EQ in ctx_kill_mem_has_depends_on_mem. + unfold eq_cond_depends_on_mem in ctx_kill_mem_has_depends_on_mem. + rewrite (cond_depends_on_memory_correct cond) with (m2 := m). + assumption. + destruct (cond_depends_on_memory cond) in *; trivial. + rewrite negb_true_iff in H0. + intuition. + congruence. + Qed. + + 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 as [lhs sop args | cond args] eqn:EQ. + * destruct sop 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). + rewrite EQ in ctx_kill_store_has_depends_on_store. + rewrite negb_true_iff in H0. + intuition. + congruence. + * rewrite cond_valid_pointer_eq with (m2 := m). + assumption. + eapply store_preserves_validity; eauto. + Qed. + + Hint Resolve kill_store_sound : cse3. + + Theorem eq_find_sound: + forall no eq id, + eq_find (ctx := ctx) no eq = Some id -> + eq_catalog ctx id = Some eq. + Proof. + unfold eq_find. + intros. + destruct (eq_find_oracle ctx no eq) as [ id' | ]. + 2: discriminate. + destruct (eq_catalog ctx id') as [eq' |] eqn:CATALOG. + 2: discriminate. + destruct (eq_dec_equation eq eq'). + 2: discriminate. + congruence. + Qed. + + Hint Resolve eq_find_sound : cse3. + + Theorem is_condition_present_sound : + forall node rel cond args rs m + (REL : sem_rel rel rs m) + (COND : (is_condition_present (ctx := ctx) node rel cond args) = true), + (eval_condition cond (rs ## args) m) = Some true. + Proof. + unfold sem_rel, is_condition_present. + intros. + destruct eq_find as [i |] eqn:FIND. + 2: discriminate. + pose proof (eq_find_sound node (Cond cond args) i FIND) as CATALOG. + exact (REL i (Cond cond args) COND CATALOG). + Qed. + + Hint Resolve is_condition_present_sound : cse3. + + Theorem rhs_find_sound: + forall no sop args rel src rs m, + sem_rel rel rs m -> + rhs_find (ctx := ctx) no sop args rel = Some src -> + sem_rhs sop args rs m (rs # src). + Proof. + unfold rhs_find, sem_rel, sem_eq. + intros until m. + intros REL FIND. + pose proof (pick_source_sound (PSet.elements (PSet.inter (eq_rhs_oracle ctx no sop args) rel))) as SOURCE. + destruct (pick_source (PSet.elements (PSet.inter (eq_rhs_oracle ctx no sop args) rel))) as [ src' | ]. + 2: discriminate. + rewrite PSet.elements_spec in SOURCE. + rewrite PSet.ginter in SOURCE. + rewrite andb_true_iff in SOURCE. + destruct (eq_catalog ctx src') as [eq | ] eqn:CATALOG. + 2: discriminate. + specialize REL with (i := src') (eq0 := eq). + destruct eq as [eq_lhs eq_sop eq_args | eq_cond eq_args] eqn:EQ. + 2: discriminate. + destruct (eq_dec_sym_op sop eq_sop). + 2: discriminate. + destruct (eq_dec_args args eq_args). + 2: discriminate. + simpl in FIND. + intuition congruence. + Qed. + + Hint Resolve rhs_find_sound : cse3. + + Theorem forward_move_rhs_sound : + forall sop args rel rs m v, + (sem_rel rel rs m) -> + (sem_rhs sop args rs m v) -> + (sem_rhs sop (forward_move_l (ctx := ctx) rel args) rs m v). + Proof. + intros until v. + intros REL RHS. + destruct sop; simpl in *. + all: erewrite forward_move_l_sound by eassumption; assumption. + Qed. + + Hint Resolve forward_move_rhs_sound : cse3. + + Lemma arg_not_replaced: + forall (rs : regset) dst v args, + ~ In dst args -> + (rs # dst <- v) ## args = rs ## args. + Proof. + induction args; simpl; trivial. + intuition. + f_equal; trivial. + apply Regmap.gso; congruence. + Qed. + + Lemma sem_rhs_depends_on_args_only: + forall sop args rs dst m v, + sem_rhs sop args rs m v -> + ~ In dst args -> + sem_rhs sop args (rs # dst <- v) m v. + Proof. + unfold sem_rhs. + intros. + rewrite arg_not_replaced by assumption. + assumption. + Qed. + + Lemma replace_sound: + forall no eqno dst sop args rel rs m v, + sem_rel rel rs m -> + sem_rhs sop args rs m v -> + ~ In dst args -> + eq_find (ctx := ctx) no (Equ dst sop args) = Some eqno -> + sem_rel (PSet.add eqno (kill_reg (ctx := ctx) dst rel)) (rs # dst <- v) m. + Proof. + intros until v. + intros REL RHS NOTIN FIND i eq CONTAINS CATALOG. + destruct (peq i eqno). + - subst i. + rewrite eq_find_sound with (no := no) (eq0 := Equ dst sop args) in CATALOG by exact FIND. + clear FIND. + inv CATALOG. + unfold sem_eq. + simpl in *. + rewrite Regmap.gss. + apply sem_rhs_depends_on_args_only; auto. + - rewrite PSet.gaddo in CONTAINS by congruence. + eapply kill_reg_sound; eauto. + Qed. + + Lemma sem_rhs_det: + forall {sop} {args} {rs} {m} {v} {v'}, + sem_rhs sop args rs m v -> + sem_rhs sop args rs m v' -> + v = v'. + Proof. + intros until v'. intro SEMv. + destruct sop; simpl in *. + - destruct eval_operation. + congruence. + contradiction. + - destruct eval_addressing. + + destruct Mem.loadv; congruence. + + congruence. + Qed. + + Lemma arglist_idem_write: + forall { A : Type} args (rs : Regmap.t A) dst, + (rs # dst <- (rs # dst)) ## args = rs ## args. + Proof. + induction args; trivial. + intros. cbn. + f_equal; trivial. + apply Regmap.gsident. + Qed. + + Lemma sem_rhs_idem_write: + forall sop args rs dst m v, + sem_rhs sop args rs m v -> + sem_rhs sop args (rs # dst <- (rs # dst)) m v. + Proof. + intros. + unfold sem_rhs in *. + rewrite arglist_idem_write. + assumption. + Qed. + + Theorem oper2_sound: + forall no dst sop args rel rs m v, + sem_rel rel rs m -> + not (In dst args) -> + sem_rhs sop args rs m v -> + sem_rel (oper2 (ctx := ctx) no dst sop args rel) (rs # dst <- v) m. + Proof. + unfold oper2. + intros until v. + intros REL NOTIN RHS. + pose proof (eq_find_sound no (Equ dst sop args)) as EQ_FIND_SOUND. + destruct eq_find. + 2: auto with cse3; fail. + specialize EQ_FIND_SOUND with (id := e). + intuition. + intros i eq CONTAINS. + destruct (peq i e). + { subst i. + rewrite H. + clear H. + intro Z. + inv Z. + unfold sem_eq. + simpl. + rewrite Regmap.gss. + apply sem_rhs_depends_on_args_only; auto. + } + intros INi. + destruct (PSet.contains rel e) eqn:CONTAINSe. + { pose proof (REL e (Equ dst sop args) CONTAINSe H) as RELe. + pose proof (REL i eq CONTAINS INi) as RELi. + destruct eq as [eq_lhs eq_sop eq_args | eq_cond eq_args]; cbn in *. + - replace v with (rs # dst) by (eapply sem_rhs_det; eassumption). + rewrite Regmap.gsident. + apply sem_rhs_idem_write. + assumption. + - replace v with (rs # dst) by (eapply sem_rhs_det; eassumption). + rewrite arglist_idem_write. + assumption. + } + rewrite PSet.gaddo in CONTAINS by congruence. + apply (kill_reg_sound rel rs m dst v REL i eq); auto. + Qed. + + Hint Resolve oper2_sound : cse3. + + Theorem oper1_sound: + forall no dst sop args rel rs m v, + sem_rel rel rs m -> + sem_rhs sop args rs m v -> + sem_rel (oper1 (ctx := ctx) no dst sop args rel) (rs # dst <- v) m. + Proof. + intros. + unfold oper1. + destruct in_dec; auto with cse3. + Qed. + + Hint Resolve oper1_sound : cse3. + + Lemma rel_idem_replace: + forall rel rs r m, + sem_rel rel rs m -> + sem_rel rel rs # r <- (rs # r) m. + Proof. + intros until m. + intro REL. + unfold sem_rel, sem_eq, sem_rhs in *. + intros. + specialize REL with (i:=i) (eq0:=eq). + destruct eq as [lhs sop args | cond args] eqn:EQ. + * rewrite Regmap.gsident. + replace ((rs # r <- (rs # r)) ## args) with + (rs ## args). + { apply REL; auto. } + apply list_map_exten. + intros. + apply Regmap.gsident. + (* TODO simplify? *) + * rewrite arglist_idem_write. + auto. + Qed. + + Lemma move_sound : + forall no : node, + forall rel : RELATION.t, + forall src dst : reg, + forall rs m, + sem_rel rel rs m -> + sem_rel (move (ctx:=ctx) no src dst rel) (rs # dst <- (rs # src)) m. + Proof. + unfold move. + intros until m. + intro REL. + destruct (peq src dst). + { subst dst. + apply rel_idem_replace; auto. + } + pose proof (eq_find_sound no (Equ dst (SOp Omove) (src::nil))) as EQ_FIND_SOUND. + destruct eq_find. + - intros i eq CONTAINS. + destruct (peq i e). + + subst i. + rewrite (EQ_FIND_SOUND e) by trivial. + intro Z. + inv Z. + unfold sem_eq. + simpl. + destruct (peq src dst). + * subst dst. + reflexivity. + * rewrite Regmap.gss. + rewrite Regmap.gso by congruence. + reflexivity. + + intros. + rewrite PSet.gaddo in CONTAINS by congruence. + apply (kill_reg_sound rel rs m dst (rs # src) REL i); auto. + - apply kill_reg_sound; auto. + Qed. + + Hint Resolve move_sound : cse3. + + Theorem oper_sound: + forall no dst sop args rel rs m v, + sem_rel rel rs m -> + sem_rhs sop args rs m v -> + sem_rel (oper (ctx := ctx) no dst sop args rel) (rs # dst <- v) m. + Proof. + intros until v. + intros REL RHS. + unfold oper. + destruct (is_smove sop). + - subst. + simpl in RHS. + destruct args. contradiction. + destruct args. 2: contradiction. + cbn in *. + subst. + rewrite <- (forward_move_sound rel rs m r) by auto. + apply move_sound; auto. + - destruct rhs_find as [src |] eqn:RHS_FIND. + + destruct (Compopts.optim_CSE3_glb tt). + * apply sem_rel_glb; split. + ** pose proof (rhs_find_sound no sop args rel src rs m REL RHS_FIND) as SOUND. + rewrite <- (sem_rhs_det SOUND RHS). + apply move_sound; auto. + ** apply sem_rel_glb; split. + *** apply oper1_sound; auto. + *** apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + * apply sem_rel_glb; split. + ** apply oper1_sound; auto. + ** apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + + apply sem_rel_glb; split. + * apply oper1_sound; auto. + * apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + Qed. + + Hint Resolve oper_sound : cse3. + + + Theorem clever_kill_store_sound: + forall chunk addr args a src rel rs m m', + sem_rel rel rs m -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs # src) = Some m' -> + sem_rel (clever_kill_store (ctx:=ctx) chunk addr args src rel) rs m'. + Proof. + unfold clever_kill_store. + intros until m'. intros REL ADDR STORE i eq CONTAINS CATALOG. + autorewrite with pset in CONTAINS. + destruct (PSet.contains rel i) eqn:RELi; simpl in CONTAINS. + 2: discriminate. + rewrite CATALOG in CONTAINS. + unfold sem_rel in REL. + specialize REL with (i := i) (eq0 := eq). + destruct eq as [eq_lhs eq_sop eq_args | eq_cond eq_args]; simpl in *. + * unfold sem_eq in *. + simpl in *. + destruct eq_sop as [op' | chunk' addr']; simpl. + - rewrite op_valid_pointer_eq with (m2 := m). + + cbn in *. + apply REL; auto. + + eapply store_preserves_validity; eauto. + - simpl in REL. + 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'. + + erewrite may_overlap_sound with (chunk:=chunk) (addr:=addr) (args:=args) (chunk':=chunk') (addr':=addr') (args':=eq_args); try eassumption. + apply REL; auto. + + apply REL; auto. + * rewrite cond_valid_pointer_eq with (m2 := m). + auto. + eapply store_preserves_validity; eauto. + Qed. + + Hint Resolve clever_kill_store_sound : cse3. + + Theorem store2_sound: + forall chunk addr args a src rel rs m m', + sem_rel rel rs m -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs # src) = Some m' -> + sem_rel (store2 (ctx:=ctx) chunk addr args src rel) rs m'. + Proof. + unfold store2. + intros. + destruct (Compopts.optim_CSE3_alias_analysis tt); eauto with cse3. + Qed. + + Hint Resolve store2_sound : cse3. + + Theorem store1_sound: + forall no chunk addr args a src rel tenv rs m m', + sem_rel rel rs m -> + wt_regset tenv rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs#src) = Some m' -> + sem_rel (store1 (ctx:=ctx) no chunk addr args src (tenv src) rel) rs m'. + Proof. + unfold store1. + intros until m'. + intros REL WT ADDR STORE. + assert (sem_rel (store2 (ctx:=ctx) chunk addr args src rel) rs m') as REL' by eauto with cse3. + destruct loadv_storev_compatible_type eqn:COMPATIBLE. + 2: auto; fail. + destruct eq_find as [eq_id | ] eqn:FIND. + 2: auto; fail. + intros i eq CONTAINS CATALOG. + destruct (peq i eq_id). + { subst i. + rewrite eq_find_sound with (no:=no) (eq0:=Equ src (SLoad chunk addr) args) in CATALOG; trivial. + inv CATALOG. + unfold sem_eq. + simpl. + rewrite ADDR. + rewrite loadv_storev_really_same with (m1:=m) (v:=rs#src) (ty:=(tenv src)); trivial. + } + unfold sem_rel in REL'. + rewrite PSet.gaddo in CONTAINS by congruence. + eauto. + Qed. + + Hint Resolve store1_sound : cse3. + + + Theorem store_sound: + forall no chunk addr args a src rel tenv rs m m', + sem_rel rel rs m -> + wt_regset tenv rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs#src) = Some m' -> + sem_rel (store (ctx:=ctx) no tenv chunk addr args src rel) rs m'. + Proof. + unfold store. + intros until m'. + intros REL WT ADDR STORE. + apply sem_rel_glb; split. + - apply sem_rel_glb; split. + * apply store1_sound with (a := a) (m := m); trivial. + * rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial. + apply store1_sound with (a := a) (m := m); trivial. + - rewrite <- forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. + apply sem_rel_glb; split. + * apply store1_sound with (a := a) (m := m); trivial. + * rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial. + apply store1_sound with (a := a) (m := m); trivial. + Qed. + + Hint Resolve store_sound : cse3. + + Lemma kill_builtin_res_sound: + forall res (m : mem) (rs : regset) vres (rel : RELATION.t) + (REL : sem_rel rel rs m), + (sem_rel (kill_builtin_res (ctx:=ctx) res rel) + (regmap_setres res vres rs) m). + Proof. + destruct res; simpl; intros; trivial. + apply kill_reg_sound; trivial. + Qed. + + Hint Resolve kill_builtin_res_sound : cse3. + + Lemma top_sound: + forall rs m, (sem_rel RELATION.top rs m). + Proof. + unfold RELATION.top, sem_rel. + intros. + rewrite PSet.gempty in H. + discriminate. + Qed. + + Hint Resolve top_sound : cse3. + + Lemma external_call_sound: + forall ge ef (rel : RELATION.t) (m m' : mem) (rs : regset) vargs t vres + (REL : sem_rel rel rs m) + (CALL : external_call ef ge vargs m t vres m'), + sem_rel (apply_external_call (ctx:=ctx) ef rel) rs m'. + Proof. + destruct ef; intros; simpl in *. + all: eauto using kill_mem_sound. + all: unfold builtin_or_external_sem in *. + 1, 2, 3, 5, 6: destruct (Compopts.optim_CSE3_across_calls tt). + all: eauto using kill_mem_sound, top_sound. + 1, 2, 3: destruct (Builtins.lookup_builtin_function name sg). + all: eauto using kill_mem_sound, top_sound. + all: inv CALL; eauto using kill_mem_sound. + Qed. + + Hint Resolve external_call_sound : cse3. + + + Definition sem_rel_b (rel : RB.t) (rs : regset) (m : mem) := + match rel with + | None => False + | Some rel => sem_rel rel rs m + end. + + Lemma apply_cond1_sound : + forall pc cond args rel rs m + (COND : (eval_condition cond (rs ## args) m) = Some true) + (REL : (sem_rel rel rs m)), + (sem_rel_b (apply_cond1 (ctx:=ctx) pc cond args rel) rs m). + Proof. + intros. + unfold apply_cond1. + destruct eq_find as [eq_id | ] eqn:FIND; cbn. + 2: assumption. + destruct PSet.contains eqn:CONTAINS. + { + pose proof (eq_find_sound pc (Cond (negate_condition cond) args) eq_id FIND) as FIND_SOUND. + unfold sem_rel in REL. + pose proof (REL eq_id (Cond (negate_condition cond) args) CONTAINS FIND_SOUND) as REL_id. + cbn in REL_id. + rewrite eval_negate_condition in REL_id. + rewrite COND in REL_id. + discriminate. + } + exact REL. + Qed. + + Lemma apply_cond0_sound : + forall pc cond args rel rs m + (COND : (eval_condition cond (rs ## args) m) = Some true) + (REL : (sem_rel rel rs m)), + (sem_rel (apply_cond0 (ctx:=ctx) pc cond args rel) rs m). + Proof. + intros. + unfold apply_cond0. + destruct eq_find as [eq_id | ] eqn:FIND; cbn. + 2: assumption. + pose proof (eq_find_sound pc (Cond cond args) eq_id FIND) as FIND_SOUND. + intros eq_id' eq' CONTAINS CATALOG. + destruct (peq eq_id eq_id'). + { subst eq_id'. + unfold sem_eq. + rewrite FIND_SOUND in CATALOG. + inv CATALOG. + assumption. + } + rewrite PSet.gaddo in CONTAINS by assumption. + unfold sem_rel in REL. + eapply REL; eassumption. + Qed. + + Lemma apply_cond_sound : + forall pc cond args rel rs m + (COND : (eval_condition cond (rs ## args) m) = Some true) + (REL : (sem_rel rel rs m)), + (sem_rel_b (apply_cond (ctx:=ctx) pc cond args rel) rs m). + Proof. + unfold apply_cond. + intros. + pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1. + destruct apply_cond1 eqn:COND1. + { apply apply_cond0_sound; auto. } + exact SOUND1. + Qed. + + (* + Section INDUCTIVENESS. + Variable fn : RTL.function. + Variable tenv : typing_env. + Variable inv: invariants. + + Definition is_inductive_step (pc pc' : node) := + forall instr, + PTree.get pc (fn_code fn) = Some instr -> + In pc' (successors_instr instr) -> + RB.ge (PMap.get pc' inv) + (match apply_instr' (ctx:=ctx) tenv (fn_code fn) pc + (PMap.get pc inv) with + | Abst_same rel' => rel' + end). + + Definition is_inductive_allstep := + forall pc pc', is_inductive_step pc pc'. + + Lemma checked_is_inductive_allstep: + (check_inductiveness (ctx:=ctx) fn tenv inv) = true -> + is_inductive_allstep. + Proof. + unfold check_inductiveness, is_inductive_allstep, is_inductive_step. + rewrite andb_true_iff. + rewrite PTree_Properties.for_all_correct. + intros (ENTRYPOINT & ALL). + intros until instr. + intros INSTR IN_SUCC. + specialize ALL with (x := pc) (a := instr). + pose proof (ALL INSTR) as AT_PC. + destruct (inv # pc). + 2: apply RB.ge_bot. + unfold apply_instr'. + rewrite INSTR. + destruct apply_instr. + { (* same *) + rewrite List.forallb_forall in AT_PC. + apply relb_leb_correct. + auto. + } + Qed. + + Lemma checked_is_inductive_entry: + (check_inductiveness (ctx:=ctx) fn tenv inv) = true -> + inv # (fn_entrypoint fn) = Some RELATION.top. + Proof. + unfold check_inductiveness, is_inductive_allstep, is_inductive_step. + rewrite andb_true_iff. + intros (ENTRYPOINT & ALL). + apply RB.beq_correct in ENTRYPOINT. + unfold RB.eq, RELATION.eq in ENTRYPOINT. + destruct (inv # (fn_entrypoint fn)) as [rel | ]. + 2: contradiction. + f_equal. + symmetry. + assumption. + Qed. + End INDUCTIVENESS. + + Hint Resolve checked_is_inductive_allstep checked_is_inductive_entry : cse3. + *) +End SOUNDNESS. |