diff options
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 433 |
1 files changed, 322 insertions, 111 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index b298ea65..d53cf604 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -127,22 +127,35 @@ Proof. Qed. Hint Resolve add_ilist_j_adds: cse3. -Definition xlget_kills (eqs : list (eq_id * equation)) (m : Regmap.t PSet.t) : +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) => - 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 := + 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) (p : positive * equation) => - if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a) + (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)) (m : PSet.t) : PSet.t := +Definition xlget_store_kills (eqs : list (positive * equation_or_condition)) + (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) + (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 : @@ -152,7 +165,8 @@ Lemma xlget_kills_monotone : Proof. induction eqs; simpl; trivial. intros. - auto with cse3. + 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. @@ -164,9 +178,10 @@ Lemma xlget_mem_kills_monotone : Proof. induction eqs; simpl; trivial. intros. - destruct eq_depends_on_mem. + destruct a as [id eq_cond]; cbn. + destruct eq_cond_depends_on_mem. - apply IHeqs. - destruct (peq (fst a) j). + destruct (peq id j). + subst j. apply PSet.gadds. + rewrite PSet.gaddo by congruence. trivial. @@ -182,9 +197,10 @@ Lemma xlget_store_kills_monotone : Proof. induction eqs; simpl; trivial. intros. - destruct eq_depends_on_store. + destruct a as [id eq_cond]; cbn. + destruct eq_cond_depends_on_store. - apply IHeqs. - destruct (peq (fst a) j). + destruct (peq id j). + subst j. apply PSet.gadds. + rewrite PSet.gaddo by congruence. trivial. @@ -195,9 +211,7 @@ Hint Resolve xlget_store_kills_monotone : cse3. Lemma xlget_kills_has_lhs : forall eqs m lhs sop args j, - In (j, {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |}) eqs -> + In (j, (Equ lhs sop args)) eqs -> PSet.contains (Regmap.get lhs (xlget_kills eqs m)) j = true. Proof. induction eqs; simpl. @@ -212,9 +226,7 @@ Hint Resolve xlget_kills_has_lhs : cse3. Lemma xlget_kills_has_arg : forall eqs m lhs sop arg args j, - In (j, {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |}) eqs -> + In (j, (Equ lhs sop args)) eqs -> In arg args -> PSet.contains (Regmap.get arg (xlget_kills eqs m)) j = true. Proof. @@ -229,20 +241,38 @@ 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 {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> + 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) => - add_i_j (eq_lhs (snd p)) (fst p) - (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills. + (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. @@ -252,9 +282,7 @@ 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 {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> + 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. @@ -266,9 +294,7 @@ 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 {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> + PTree.get j eqs = Some (Equ lhs sop args) -> In arg args -> PSet.contains (Regmap.get arg (get_reg_kills eqs)) j = true. Proof. @@ -276,9 +302,12 @@ Proof. intros. rewrite PTree.fold_spec. change (fold_left - (fun (a : Regmap.t PSet.t) (p : positive * equation) => - add_i_j (eq_lhs (snd p)) (fst p) - (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills. + (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. @@ -289,9 +318,7 @@ 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 {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> + 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. @@ -302,10 +329,47 @@ 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_depends_on_mem eq = true -> + eq_cond_depends_on_mem eq = true -> PSet.contains (xlget_mem_kills eqs m) j = true. Proof. induction eqs; simpl. @@ -326,17 +390,16 @@ 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_depends_on_mem eq = true -> + 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) => - if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a) - (PTree.elements eqs) PSet.empty) - with (xlget_mem_kills (PTree.elements eqs) PSet.empty). + (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. @@ -346,7 +409,7 @@ 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_depends_on_mem eq = true -> + eq_cond_depends_on_mem eq = true -> PSet.contains (eq_kill_mem (context_from_hints hints) tt) j = true. Proof. intros. @@ -359,7 +422,7 @@ 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 -> + eq_cond_depends_on_store eq = true -> PSet.contains (xlget_store_kills eqs m) j = true. Proof. induction eqs; simpl. @@ -380,17 +443,16 @@ 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 -> + 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) => - 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). + (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. @@ -400,7 +462,7 @@ 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 -> + eq_cond_depends_on_store eq = true -> PSet.contains (eq_kill_store (context_from_hints hints) tt) j = true. Proof. intros. @@ -410,8 +472,12 @@ 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). +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}. @@ -440,8 +506,11 @@ Section SOUNDNESS. end end. - Definition sem_eq (eq : equation) (rs : regset) (m : mem) := - sem_rhs (eq_op eq) (eq_args eq) rs m (rs # (eq_lhs eq)). + 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, @@ -475,16 +544,19 @@ Section SOUNDNESS. Hypothesis ctx_kill_reg_has_lhs : forall lhs sop args j, - eq_catalog ctx j = Some {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> + 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 {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> + 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. @@ -492,13 +564,13 @@ Section SOUNDNESS. Hypothesis ctx_kill_mem_has_depends_on_mem : forall eq j, eq_catalog ctx j = Some eq -> - eq_depends_on_mem eq = true -> + 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_depends_on_store eq = true -> + eq_cond_depends_on_store eq = true -> PSet.contains (eq_kill_store ctx tt) j = true. Theorem kill_reg_sound : @@ -510,8 +582,8 @@ Section SOUNDNESS. intros until v. intros REL i eq. specialize REL with (i := i) (eq0 := eq). - destruct eq as [lhs sop args]; simpl. - specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i). + 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. @@ -539,6 +611,24 @@ Section SOUNDNESS. 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. @@ -552,14 +642,20 @@ Section SOUNDNESS. intros until dst. intros REL i eq. specialize REL with (i := i) (eq0 := eq). - destruct eq as [lhs sop args]; simpl. - specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i). + 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 : @@ -590,9 +686,11 @@ Section SOUNDNESS. destruct (eq_catalog ctx r) as [eq | ] eqn:CATALOG. 2: reflexivity. specialize REL with (i := r) (eq0 := eq). - destruct (is_smove (eq_op eq)) as [MOVE | ]. + destruct eq as [lhs sop args | cond args]; cbn in *; trivial. + destruct (is_smove sop) as [MOVE | ]. 2: reflexivity. - destruct (peq x (eq_lhs eq)). + rewrite MOVE in *; cbn in *. + destruct (peq x lhs). 2: reflexivity. simpl. subst x. @@ -600,9 +698,8 @@ Section SOUNDNESS. rewrite PSet.ginter in ELEMENT. rewrite andb_true_iff in ELEMENT. unfold sem_eq in REL. - rewrite MOVE in REL. simpl in REL. - destruct (eq_args eq) as [ | h t]. + destruct args as [ | h t]. reflexivity. destruct t. 2: reflexivity. @@ -637,22 +734,30 @@ Section SOUNDNESS. rewrite PSet.gsubtract in SUBTRACT. rewrite andb_true_iff in SUBTRACT. intuition. - destruct (eq_op eq) as [op | chunk addr] eqn:OP. + 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). - unfold eq_depends_on_mem in ctx_kill_mem_has_depends_on_mem. - rewrite OP in ctx_kill_mem_has_depends_on_mem. + 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). - destruct eq as [lhs op args]; simpl in *. - rewrite OP in ctx_kill_mem_has_depends_on_mem. + rewrite EQ in ctx_kill_mem_has_depends_on_mem. rewrite negb_true_iff in H0. - rewrite OP in CATALOG. 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. @@ -691,17 +796,19 @@ Section SOUNDNESS. rewrite PSet.gsubtract in SUBTRACT. rewrite andb_true_iff in SUBTRACT. intuition. - destruct (eq_op eq) as [op | chunk addr] eqn:OP. + 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). - destruct eq as [lhs op args]; simpl in *. - rewrite OP in ctx_kill_store_has_depends_on_store. + rewrite EQ in ctx_kill_store_has_depends_on_store. rewrite negb_true_iff in H0. - rewrite OP in CATALOG. intuition. congruence. + * rewrite cond_valid_pointer_eq with (m2 := m). + assumption. + eapply store_preserves_validity; eauto. Qed. Hint Resolve kill_store_sound : cse3. @@ -724,6 +831,22 @@ Section SOUNDNESS. 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 -> @@ -742,9 +865,11 @@ Section SOUNDNESS. destruct (eq_catalog ctx src') as [eq | ] eqn:CATALOG. 2: discriminate. specialize REL with (i := src') (eq0 := eq). - destruct (eq_dec_sym_op sop (eq_op 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 eq)). + destruct (eq_dec_args args eq_args). 2: discriminate. simpl in FIND. intuition congruence. @@ -794,17 +919,14 @@ Section SOUNDNESS. sem_rel rel rs m -> sem_rhs sop args rs m v -> ~ In dst args -> - eq_find (ctx := ctx) no - {| eq_lhs := dst; - eq_op := sop; - eq_args:= args |} = Some eqno -> + 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 := {| eq_lhs := dst; eq_op := sop; eq_args := args |}) in CATALOG by exact FIND. + rewrite eq_find_sound with (no := no) (eq0 := Equ dst sop args) in CATALOG by exact FIND. clear FIND. inv CATALOG. unfold sem_eq. @@ -862,7 +984,7 @@ Section SOUNDNESS. unfold oper2. intros until v. intros REL NOTIN RHS. - pose proof (eq_find_sound no {| eq_lhs := dst; eq_op := sop; eq_args := args |}) as EQ_FIND_SOUND. + 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). @@ -881,14 +1003,16 @@ Section SOUNDNESS. } intros INi. destruct (PSet.contains rel e) eqn:CONTAINSe. - { pose proof (REL e {| eq_lhs := dst; eq_op := sop; eq_args := args |} CONTAINSe H) as RELe. + { pose proof (REL e (Equ dst sop args) CONTAINSe H) as RELe. pose proof (REL i eq CONTAINS INi) as RELi. - unfold sem_eq in *. - cbn in RELe. - replace v with (rs # dst) by (eapply sem_rhs_det; eassumption). - rewrite Regmap.gsident. - apply sem_rhs_idem_write. - assumption. + 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. @@ -919,13 +1043,17 @@ Section SOUNDNESS. unfold sem_rel, sem_eq, sem_rhs in *. intros. specialize REL with (i:=i) (eq0:=eq). - rewrite Regmap.gsident. - replace ((rs # r <- (rs # r)) ## (eq_args eq)) with - (rs ## (eq_args 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 : @@ -943,7 +1071,7 @@ Section SOUNDNESS. { subst dst. apply rel_idem_replace; auto. } - pose proof (eq_find_sound no {| eq_lhs := dst; eq_op := SOp Omove; eq_args := src :: nil |}) as EQ_FIND_SOUND. + 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). @@ -1023,10 +1151,10 @@ Section SOUNDNESS. rewrite CATALOG in CONTAINS. unfold sem_rel in REL. specialize REL with (i := i) (eq0 := eq). - destruct eq; simpl in *. - unfold sem_eq in *. + destruct eq as [eq_lhs eq_sop eq_args | eq_cond eq_args]; simpl in *. + * unfold sem_eq in *. simpl in *. - destruct eq_op as [op' | chunk' addr']; simpl. + destruct eq_sop as [op' | chunk' addr']; simpl. - rewrite op_valid_pointer_eq with (m2 := m). + cbn in *. apply REL; auto. @@ -1039,6 +1167,9 @@ Section SOUNDNESS. + 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. @@ -1076,7 +1207,7 @@ Section SOUNDNESS. intros i eq CONTAINS CATALOG. destruct (peq i eq_id). { subst i. - rewrite eq_find_sound with (no:=no) (eq0:={| eq_lhs := src; eq_op := SLoad chunk addr; eq_args := args |}) in CATALOG; trivial. + rewrite eq_find_sound with (no:=no) (eq0:=Equ src (SLoad chunk addr) args) in CATALOG; trivial. inv CATALOG. unfold sem_eq. simpl. @@ -1157,6 +1288,79 @@ Section SOUNDNESS. 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. + destruct (Compopts.optim_CSE3_conditions tt). + { + 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. + } + exact REL. + Qed. + + (* Section INDUCTIVENESS. Variable fn : RTL.function. Variable tenv : typing_env. @@ -1167,7 +1371,10 @@ Section SOUNDNESS. PTree.get pc (fn_code fn) = Some instr -> In pc' (successors_instr instr) -> RB.ge (PMap.get pc' inv) - (apply_instr' (ctx:=ctx) tenv (fn_code fn) pc (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'. @@ -1186,11 +1393,14 @@ Section SOUNDNESS. pose proof (ALL INSTR) as AT_PC. destruct (inv # pc). 2: apply RB.ge_bot. - rewrite List.forallb_forall in AT_PC. unfold apply_instr'. rewrite INSTR. - apply relb_leb_correct. - auto. + destruct apply_instr. + { (* same *) + rewrite List.forallb_forall in AT_PC. + apply relb_leb_correct. + auto. + } Qed. Lemma checked_is_inductive_entry: @@ -1211,4 +1421,5 @@ Section SOUNDNESS. End INDUCTIVENESS. Hint Resolve checked_is_inductive_allstep checked_is_inductive_entry : cse3. + *) End SOUNDNESS. |