still buggy

2 files changed, 95 insertions, 56 deletions

diff --git a/backend/CSE2.v b/backend/CSE2.v
index 5b850cbb..07bde1ac 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -275,24 +275,6 @@ Definition forward_move (rel : RELATION.t) (x : reg) : reg :=
 Definition move (src dst : reg) (rel : RELATION.t) :=
   PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel).
 
-Definition oper1 (op: operation) (dst : reg) (args : list reg)
-           (rel : RELATION.t) :=
-  let rel' := kill_reg dst rel in
-  PTree.set dst (SOp op (List.map (forward_move rel') args)) rel'.
-
-Definition oper (op: operation) (dst : reg) (args : list reg)
-           (rel : RELATION.t) :=
-  if List.in_dec peq dst args
-  then kill_reg dst rel
-  else oper1 op dst args rel.
-
-Definition gen_oper (op: operation) (dst : reg) (args : list reg)
-           (rel : RELATION.t) :=
-  match op, args with
-  | Omove, src::nil => move src dst rel
-  | _, _ => oper op dst args rel
-  end.
-
 Definition find_op_fold op args (already : option reg) x sv :=
                 match already with
                 | Some found => already
@@ -309,6 +291,31 @@ Definition find_op_fold op args (already : option reg) x sv :=
 Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) :=
   PTree.fold (find_op_fold op args) rel None.
 
+Definition oper2 (op: operation) (dst : reg) (args : list reg)
+           (rel : RELATION.t) :=
+  let rel' := kill_reg dst rel in
+  PTree.set dst (SOp op (List.map (forward_move rel') args)) rel'.
+
+Definition oper1 (op: operation) (dst : reg) (args : list reg)
+           (rel : RELATION.t) :=
+  if List.in_dec peq dst args
+  then kill_reg dst rel
+  else oper2 op dst args rel.
+
+Definition oper (op: operation) (dst : reg) (args : list reg)
+           (rel : RELATION.t) :=
+  match find_op rel op args with
+  | Some r => move r dst rel
+  | None => oper1 op dst args rel
+  end.
+
+Definition gen_oper (op: operation) (dst : reg) (args : list reg)
+           (rel : RELATION.t) :=
+  match op, args with
+  | Omove, src::nil => move src dst rel
+  | _, _ => oper op dst args rel
+  end.
+
 (* NO LONGER NEEDED
 Fixpoint list_represents { X : Type } (l : list (positive*X)) (tr : PTree.t X) : Prop :=
   match l with
@@ -392,8 +399,9 @@ Definition transf_instr (fmap : option (PMap.t RB.t))
            (pc: node) (instr: instruction) :=
   match instr with
   | Iop op args dst s =>
-    match find_op_in_fmap fmap pc op args with
-    | None => Iop op (subst_args fmap pc args) dst s
+    let args' := subst_args fmap pc args in
+    match find_op_in_fmap fmap pc op args' with
+    | None => Iop op args' dst s
     | Some src => Iop Omove (src::nil) dst s
     end
   | Iload chunk addr args dst s =>
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 1d0a617a..47b60902 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -249,7 +249,7 @@ Proof.
   destruct s; simpl in *; destruct negb; simpl; congruence.
 Qed.
 
-Lemma oper1_sound :
+Lemma oper2_sound :
   forall rel : RELATION.t,
   forall op : operation,
   forall dst : reg,
@@ -259,12 +259,12 @@ Lemma oper1_sound :
     sem_rel rel rs ->
     not (In dst args) ->
     eval_operation genv sp op (rs ## args) m = Some v ->
-    sem_rel (oper1 op dst args rel) (rs # dst <- v).
+    sem_rel (oper2 op dst args rel) (rs # dst <- v).
 Proof.
   intros until v.
   intros REL NOT_IN EVAL x.
   pose proof (kill_reg_sound rel dst rs v REL x) as KILL.
-  unfold oper1.
+  unfold oper2.
   destruct (peq x dst).
   {
     subst x.
@@ -282,7 +282,7 @@ Proof.
   exact KILL.
 Qed.
 
-Lemma oper_sound :
+Lemma oper1_sound :
   forall rel : RELATION.t,
   forall op : operation,
   forall dst : reg,
@@ -291,45 +291,18 @@ Lemma oper_sound :
   forall v,
     sem_rel rel rs ->
     eval_operation genv sp op (rs ## args) m = Some v ->
-    sem_rel (oper op dst args rel) (rs # dst <- v).
+    sem_rel (oper1 op dst args rel) (rs # dst <- v).
 Proof.
   intros until v.
   intros REL EVAL.
-  unfold oper.
+  unfold oper1.
   destruct in_dec.
   {
     apply kill_reg_sound; auto. 
   }
-  apply oper1_sound; auto.
+  apply oper2_sound; auto.
 Qed.
 
-Lemma gen_oper_sound :
-  forall rel : RELATION.t,
-  forall op : operation,
-  forall dst : reg,
-  forall args: list reg,
-  forall rs : regset,
-  forall v,
-    sem_rel rel rs ->
-    eval_operation genv sp op (rs ## args) m = Some v ->
-    sem_rel (gen_oper op dst args rel) (rs # dst <- v).
-Proof.
-  intros until v.
-  intros REL EVAL.
-  unfold gen_oper.
-  destruct op.
-  { destruct args as [ | h0 t0].
-    apply oper_sound; auto.
-    destruct t0.
-    {
-      simpl in *.
-      replace v with (rs # h0) by congruence.
-      apply move_sound; auto.
-    }
-    apply oper_sound; auto.
-  }
-  all: apply oper_sound; auto.
-Qed.
 
 
 Lemma find_op_sound :
@@ -399,6 +372,59 @@ Proof.
   apply REC; auto.
 Qed.
 
+Lemma oper_sound :
+  forall rel : RELATION.t,
+  forall op : operation,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall v,
+    sem_rel rel rs ->
+    eval_operation genv sp op (rs ## args) m = Some v ->
+    sem_rel (oper op dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL EVAL.
+  unfold oper.
+  destruct find_op eqn:FIND.
+  {
+    assert (eval_operation genv sp op rs ## args m = Some rs # r).
+    {
+      apply (find_op_sound rel); trivial.
+    }
+    replace v with (rs # r) by congruence.
+    apply move_sound; auto.
+  }
+  apply oper1_sound; trivial.
+Qed.
+
+Lemma gen_oper_sound :
+  forall rel : RELATION.t,
+  forall op : operation,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall v,
+    sem_rel rel rs ->
+    eval_operation genv sp op (rs ## args) m = Some v ->
+    sem_rel (gen_oper op dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL EVAL.
+  unfold gen_oper.
+  destruct op.
+  { destruct args as [ | h0 t0].
+    apply oper_sound; auto.
+    destruct t0.
+    {
+      simpl in *.
+      replace v with (rs # h0) by congruence.
+      apply move_sound; auto.
+    }
+    apply oper_sound; auto.
+  }
+  all: apply oper_sound; auto.
+Qed.
 
 Lemma kill_reg_weaken:
   forall res mpc rs,
@@ -645,8 +671,13 @@ Proof.
     {
       eapply exec_Iop with (v := v); eauto.
       simpl.
-      rewrite find_op_sound with (rel := mpc) (src := r) in H0 by assumption.
-      assumption.
+      rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
+      {
+        rewrite MAP in H0.
+        rewrite find_op_sound with (rel := mpc) (src := r) in H0 by assumption.
+        assumption.
+      }
+      unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
     }
     constructor; eauto.
     unfold fmap_sem', fmap_sem in *.