From d09c509f8d1bd8335ebedbe260320bb43c5a2723 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 26 Nov 2020 15:11:15 +0100 Subject: ajouté Cond, tout passe MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- backend/CSE3analysisproof.v | 158 +++++++++++++++++++++++++++++++++++++------- 1 file changed, 134 insertions(+), 24 deletions(-) (limited to 'backend/CSE3analysisproof.v') diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 5fcaa048..228fec93 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -135,6 +135,7 @@ Definition xlget_kills (eqs : list (eq_id * equation_or_condition)) | 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)) @@ -165,8 +166,7 @@ Proof. induction eqs; simpl; trivial. intros. destruct a as [id eq_cond]; cbn. - destruct eq_cond as [eq_lhs eq_sop eq_args]. - auto with cse3. + destruct eq_cond as [eq_lhs eq_sop eq_args | eq_cond eq_args]; auto with cse3. Qed. Hint Resolve xlget_kills_monotone : cse3. @@ -241,6 +241,23 @@ 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) -> @@ -253,7 +270,8 @@ Proof. (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) + 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. @@ -287,7 +305,8 @@ Proof. (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) + 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. @@ -310,6 +329,43 @@ 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 -> @@ -420,6 +476,7 @@ 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. @@ -452,6 +509,7 @@ Section SOUNDNESS. 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) := @@ -496,6 +554,13 @@ Section SOUNDNESS. 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 -> @@ -517,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. @@ -546,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. @@ -559,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 : @@ -597,7 +686,7 @@ Section SOUNDNESS. destruct (eq_catalog ctx r) as [eq | ] eqn:CATALOG. 2: reflexivity. specialize REL with (i := r) (eq0 := eq). - destruct eq as [lhs sop args]; cbn in *. (* TODO *) + destruct eq as [lhs sop args | cond args]; cbn in *; trivial. destruct (is_smove sop) as [MOVE | ]. 2: reflexivity. rewrite MOVE in *; cbn in *. @@ -645,8 +734,8 @@ Section SOUNDNESS. rewrite PSet.gsubtract in SUBTRACT. rewrite andb_true_iff in SUBTRACT. intuition. - destruct eq as [lhs sop args] eqn:EQ. - destruct sop 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). rewrite EQ in ctx_kill_mem_has_depends_on_mem. unfold eq_cond_depends_on_mem in ctx_kill_mem_has_depends_on_mem. @@ -660,6 +749,15 @@ Section SOUNDNESS. 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. @@ -698,8 +796,8 @@ Section SOUNDNESS. rewrite PSet.gsubtract in SUBTRACT. rewrite andb_true_iff in SUBTRACT. intuition. - destruct eq as [lhs sop args] eqn:EQ. - destruct sop 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. @@ -708,6 +806,9 @@ Section SOUNDNESS. 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. @@ -748,7 +849,8 @@ Section SOUNDNESS. 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] eqn: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). @@ -887,12 +989,14 @@ Section SOUNDNESS. 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]; cbn in *. - unfold sem_eq in *. - 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. @@ -923,14 +1027,17 @@ Section SOUNDNESS. unfold sem_rel, sem_eq, sem_rhs in *. intros. specialize REL with (i:=i) (eq0:=eq). - destruct eq as [lhs sop args] eqn:EQ. - rewrite Regmap.gsident. + 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 : @@ -1028,8 +1135,8 @@ Section SOUNDNESS. 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]; 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_sop as [op' | chunk' addr']; simpl. - rewrite op_valid_pointer_eq with (m2 := m). @@ -1044,6 +1151,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. -- cgit