passage à Equ

1 files changed, 100 insertions, 95 deletions

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index b298ea65..5fcaa048 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -127,22 +127,34 @@ 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)
+    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,6 +164,8 @@ Lemma xlget_kills_monotone :
 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.
 Qed.
 
@@ -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.
@@ -231,18 +243,18 @@ Hint Resolve xlget_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)
+        end))  with xlget_kills.
   eapply xlget_kills_has_lhs.
   apply PTree.elements_correct.
   eassumption.
@@ -252,9 +264,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 +276,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 +284,11 @@ 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)
+        end)) with xlget_kills.
   eapply xlget_kills_has_arg.
   - apply PTree.elements_correct.
     eassumption.
@@ -289,9 +299,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.
@@ -305,7 +313,7 @@ Hint Resolve context_from_hints_get_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 +334,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 +353,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 +366,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 +387,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 +406,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 +416,11 @@ 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
+  end.
 
 Section SOUNDNESS.
   Context {F V : Type}.
@@ -440,8 +449,10 @@ 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)
+    end.
 
   Definition sem_rel (rel : RELATION.t) (rs : regset) (m : mem) :=
     forall i eq,
@@ -475,16 +486,12 @@ 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.
@@ -492,13 +499,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 :
@@ -590,9 +597,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]; cbn in *. (* TODO *)
+    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 +609,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,20 +645,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] 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.
   Qed.
@@ -691,15 +698,14 @@ 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] 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.
   Qed.
@@ -742,9 +748,10 @@ 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] eqn:EQ.
+    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 +801,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 +866,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,10 +885,10 @@ 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.
+      destruct eq as [eq_lhs eq_sop eq_args]; cbn in *.
       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.
@@ -919,9 +923,10 @@ 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.
-    replace ((rs # r <- (rs # r)) ## (eq_args eq)) with
-        (rs ## (eq_args eq)).
+    replace ((rs # r <- (rs # r)) ## args) with
+        (rs ## args).
     { apply REL; auto. }
     apply list_map_exten.
     intros.
@@ -943,7 +948,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 +1028,10 @@ Section SOUNDNESS.
     rewrite CATALOG in CONTAINS.
     unfold sem_rel in REL.
     specialize REL with (i := i) (eq0 := eq).
-    destruct eq; simpl in *.
+    destruct eq as [eq_lhs eq_sop 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.
@@ -1076,7 +1081,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.