ajouté Cond, tout passe

1 files changed, 134 insertions, 24 deletions

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.