refixcse3

1 files changed, 24 insertions, 18 deletions

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 07a58f23..1e5b88c3 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -853,24 +853,24 @@ Section SOUNDNESS.
       subst.
       rewrite <- (forward_move_sound rel rs m r) by auto.
       apply move_sound; auto.
-    - destruct (is_trivial_sym_op sop).
-      {
-        apply kill_reg_sound; auto.
-      }
-      destruct rhs_find as [src |] eqn:RHS_FIND.
+    - destruct rhs_find as [src |] eqn:RHS_FIND.
       + destruct (Compopts.optim_CSE3_glb tt).
         * apply sem_rel_glb; split.
-          ** pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND.
-             eapply forward_move_rhs_sound in RHS.
-             2: eassumption.
+          ** pose proof (rhs_find_sound no sop args rel src rs m REL RHS_FIND) as SOUND.                                                                    
              rewrite <- (sem_rhs_det SOUND RHS).
              apply move_sound; auto.
+          ** apply sem_rel_glb; split.
+             *** apply oper1_sound; auto.
+             *** apply oper1_sound; auto.
+                 apply forward_move_rhs_sound; auto.
+        * apply sem_rel_glb; split.
+          ** apply oper1_sound; auto.
           ** apply oper1_sound; auto.
              apply forward_move_rhs_sound; auto.
-        * ** apply oper1_sound; auto.
-             apply forward_move_rhs_sound; auto.
-      + apply oper1_sound; auto.
-        apply forward_move_rhs_sound; auto.
+      + apply sem_rel_glb; split.
+        * apply oper1_sound; auto.
+        * apply oper1_sound; auto.
+          apply forward_move_rhs_sound; auto.
   Qed.
 
   Hint Resolve oper_sound : cse3.
@@ -959,22 +959,28 @@ Section SOUNDNESS.
   
   Hint Resolve store1_sound : cse3.
     
+    
   Theorem store_sound:
     forall no chunk addr args a src rel tenv rs m m',
       sem_rel rel rs m ->
       wt_regset tenv rs ->
       eval_addressing genv sp addr (rs ## args) = Some a ->
       Mem.storev chunk m a (rs#src) = Some m' ->
-      sem_rel (store (ctx:=ctx) no chunk addr args src (tenv (forward_move (ctx:=ctx) rel src)) rel) rs m'.
+      sem_rel (store (ctx:=ctx) no tenv chunk addr args src rel) rs m'.
   Proof.
     unfold store.
     intros until m'.
     intros REL WT ADDR STORE.
-    rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial.
-    rewrite <- forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial.
-    apply store1_sound with (a := a) (m := m); trivial.
-    (* rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial.
-    assumption. *)
+    apply sem_rel_glb; split.
+    - apply sem_rel_glb; split.
+      * apply store1_sound with (a := a) (m := m); trivial.
+      * rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial.
+        apply store1_sound with (a := a) (m := m); trivial.
+    - rewrite <- forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial.
+      apply sem_rel_glb; split.
+      * apply store1_sound with (a := a) (m := m); trivial.
+      * rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial.
+        apply store1_sound with (a := a) (m := m); trivial.
   Qed.
 
   Hint Resolve store_sound : cse3.