forward moves through CSE3 store

4 files changed, 11 insertions, 8 deletions

diff --git a/backend/CSE3.v b/backend/CSE3.v
index 352cc895..2203ad14 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -57,7 +57,7 @@ Definition transf_instr (fmap : PMap.t RB.t)
     | Some src => Iop Omove (src::nil) dst s
     end
   | Istore chunk addr args src s =>
-    Istore chunk addr (subst_args fmap pc args) src s
+    Istore chunk addr (subst_args fmap pc args) (subst_arg fmap pc src) s
   | Icall sig ros args dst s =>
     Icall sig ros (subst_args fmap pc args) dst s
   | Itailcall sig ros args =>
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index bc5d3244..d3d1c043 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -323,7 +323,7 @@ Section OPERATIONS.
              (chunk : memory_chunk) (addr: addressing) (args : list reg)
              (src : reg) (ty: typ)
              (rel : RELATION.t) : RELATION.t :=
-    store1 chunk addr (forward_move_l rel args) src ty rel.
+    store1 chunk addr (forward_move_l rel args) (forward_move rel src) ty rel.
 
   Definition kill_builtin_res res rel :=
     match res with
@@ -354,7 +354,7 @@ Section OPERATIONS.
   | Icond _ _ _ _ _
   | Ijumptable _ _ => Some rel
   | Istore chunk addr args src _ =>
-    Some (store chunk addr args src (tenv src) rel)
+    Some (store chunk addr args src (tenv (forward_move rel src)) rel)
   | Iop op args dst _ => Some (oper dst (SOp op) args rel)
   | Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel)
   | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel))
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index f4ec7a10..e1e9f6cc 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -848,14 +848,14 @@ Section SOUNDNESS.
   Qed.
   
   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 src) rel) rs m'.
+      sem_rel (store (ctx:=ctx) no chunk addr args src (tenv (forward_move (ctx:=ctx) rel src)) rel) rs m'.
   Proof.
     unfold store.
     intros until m'.
@@ -863,8 +863,8 @@ Section SOUNDNESS.
     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.
+    (* rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial.
+    assumption. *)
   Qed.
 
   Hint Resolve store_sound : cse3.
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 53872e62..ccbfd198 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -689,10 +689,13 @@ Proof.
 
   - (* Istore *)
     exists (State ts tf sp pc' rs m'). split.
-    + eapply exec_Istore with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption.
+    + eapply exec_Istore with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args))
+      (src := (subst_arg (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc src)) ; try eassumption.
       * TR_AT. reflexivity.
       * rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial.
         rewrite eval_addressing_preserved with (ge1 := ge) by exact symbols_preserved.
+        eassumption.
+      * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial.
         assumption.
     + econstructor; eauto.
       IND_STEP.