Merge remote-tracking branch 'origin/kvx-work' into kvx-work-ssa

5 files changed, 109 insertions, 48 deletions

diff --git a/backend/CSE3.v b/backend/CSE3.v
index df1c2bfc..58e179e2 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -58,7 +58,7 @@ Definition transf_instr (fmap : PMap.t RB.t)
   match instr with
   | Iop op args dst s =>
     let args' := subst_args fmap pc args in
-    match (if is_trivial_op op then None else find_op_in_fmap fmap pc op args') with
+    match (if andb (negb (Compopts.optim_CSE3_trivial_ops tt)) (is_trivial_op op) then None else find_op_in_fmap fmap pc op args') with
     | None => Iop op args' dst s
     | Some src => Iop Omove (src::nil) dst s
     end
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index cd7e3d84..34df644e 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -227,29 +227,44 @@ Section OPERATIONS.
   Definition kill_mem (rel : RELATION.t) : RELATION.t :=
     PSet.subtract rel (eq_kill_mem ctx tt).
 
-  Definition pick_source (l : list reg) := (* todo: take min? *)
+  Definition reg_min (x y : reg) :=
+    if plt x y then x else y.
+  
+  Fixpoint reg_min_rec (l : list reg) (before : reg)  :=
+    match l with
+    | h::t => reg_min_rec t (reg_min before h)
+    | nil => before
+    end.
+
+  Definition pick_source (l : list reg) :=
     match l with
-    | h::t => Some h
+    | h::t => Some (reg_min_rec t h)
     | nil => None
     end.
-  
-  Definition forward_move (rel : RELATION.t)  (x : reg) : reg :=
-    match pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x))) with
-    | None => x
-    | Some eqno =>
+
+  Fixpoint get_sources (x : reg) eqs :=
+    match eqs with
+    | nil => nil
+    | eqno::others =>
       match eq_catalog ctx eqno with
       | Some eq =>
         if is_smove (eq_op eq) && peq x (eq_lhs eq)
         then
           match eq_args eq with
-          | src::nil => src
-          | _ => x
+          | src::nil => src :: (get_sources x others)
+          | _ => get_sources x others
           end
-        else x
-      | _ => x
+        else get_sources x others
+      | _ => get_sources x others
       end
     end.
-
+      
+  Definition forward_move (rel : RELATION.t)  (x : reg) : reg :=
+    match pick_source (get_sources x (PSet.elements (PSet.inter rel (eq_moves ctx x)))) with
+    | None => x
+    | Some src => src
+    end.
+  
   Definition forward_move_l (rel : RELATION.t) : list reg -> list reg :=
     List.map (forward_move rel).
 
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index ea4d37ca..12048010 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -478,6 +478,27 @@ Section SOUNDNESS.
     rewrite negb_true_iff in H.
     intuition.
   Qed.
+
+  Lemma reg_min_sound:
+    forall x y, (reg_min x y) = x \/ (reg_min x y) = y.
+  Proof.
+    intros; unfold reg_min.
+    destruct plt; auto.
+  Qed.
+  
+  Lemma reg_min_rec_sound :
+    forall (l : list reg) (before : reg),
+      In (reg_min_rec l before) l \/
+      reg_min_rec l before = before.
+  Proof.
+    induction l; cbn.
+    { auto. }
+    intro bef.
+    destruct (IHl (reg_min bef a)).
+    { auto. }
+    rewrite H.
+    destruct (reg_min_sound bef a); auto.
+  Qed.
     
   Lemma pick_source_sound :
     forall (l : list reg),
@@ -486,47 +507,71 @@ Section SOUNDNESS.
       | None => True
       end.
   Proof.
-    unfold pick_source.
-    destruct l; simpl; trivial.
-    left; trivial.
+    destruct l; cbn; trivial.
+    destruct (reg_min_rec_sound l r); auto.
   Qed.
-    
+
   Hint Resolve pick_source_sound : cse3.
 
+  Theorem get_sources_sound :
+    forall l src rs m x,
+    (forall i eq,
+      In i l ->
+      eq_catalog ctx i = Some eq ->
+      sem_eq eq rs m) ->
+      (In src (get_sources (ctx := ctx) x l)) ->
+      rs # src = rs # x.
+  Proof.
+    induction l; cbn; intros until x; intros SEM IN.
+    contradiction.
+    destruct (eq_catalog ctx a) eqn:CATALOG.
+    2: eauto using IHl; fail.
+    pose proof (SEM a e) as SEMeq.
+    destruct e; cbn in *.
+    destruct (is_smove eq_op && peq x eq_lhs) eqn:CORRECT.
+    2: eauto using IHl; fail.
+    destruct eq_args.
+    eauto using IHl; fail.
+    destruct eq_args.
+    2: eauto using IHl; fail.
+    cbn in IN.
+    destruct IN.
+    2: eauto using IHl; fail.
+    rewrite andb_true_iff in CORRECT.
+    intuition.
+    destruct (peq x eq_lhs).
+    2: discriminate.
+    subst eq_lhs.
+    destruct (is_smove eq_op).
+    2: discriminate.
+    subst eq_op.
+    subst src.
+    cbn in H2.
+    symmetry.
+    assumption.
+  Qed.
+    
   Theorem forward_move_sound :
     forall rel rs m x,
       (sem_rel rel rs m) ->
       rs # (forward_move (ctx := ctx) rel x) = rs # x.
   Proof.
-    unfold sem_rel, forward_move.
-    intros until x.
-    intro REL.
-    pose proof (pick_source_sound (PSet.elements (PSet.inter rel (eq_moves ctx x)))) as ELEMENT.
-    destruct (pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x)))).
-    2: reflexivity.
-    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 | ].
-    2: reflexivity.
-    destruct (peq x (eq_lhs eq)).
+    unfold forward_move.
+    intros until x; intros REL.
+    pose proof (pick_source_sound (get_sources (ctx := ctx) x (PSet.elements (PSet.inter rel (eq_moves ctx x))))) as PICK.
+    destruct pick_source.
     2: reflexivity.
-    simpl.
-    subst x.
-    rewrite PSet.elements_spec in ELEMENT.
-    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].
-    reflexivity.
-    destruct t.
-    2: reflexivity.
-    simpl in REL.
-    intuition congruence.
+    apply get_sources_sound with (l := (PSet.elements (PSet.inter rel (eq_moves ctx x)))) (m:=m).
+    2: assumption.
+    intros i eq IN CATALOG.
+    rewrite PSet.elements_spec in IN.
+    rewrite PSet.ginter in IN.
+    rewrite andb_true_iff in IN.
+    destruct IN.
+    unfold sem_rel in REL.
+    apply REL with (i:=i); assumption.
   Qed.
-
+  
   Hint Resolve forward_move_sound : cse3.
 
   Theorem forward_move_l_sound :
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 3fbc9912..a0361746 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -63,7 +63,7 @@ Proof.
     destruct rel as [rel | ]; simpl; intros.
     2: contradiction.
     eapply forward_move_sound; eauto.
-  Qed.
+Qed.
 
   Lemma forward_move_l_b_sound :
     forall rel rs m x,
@@ -447,7 +447,6 @@ Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 -> 
   forall S1', match_states S1 S1' ->
               exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
-Proof.
   induction 1; intros S1' MS; inv MS.
   - (* Inop *)
     exists (State ts tf sp pc' rs m). split.
@@ -463,12 +462,12 @@ Proof.
       destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
       pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SOp op)
                 (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
-      * destruct (if is_trivial_op op
+      * destruct (if (negb (Compopts.optim_CSE3_trivial_ops tt) && is_trivial_op op)
                then None
                else
                 rhs_find pc (SOp op)
                   (subst_args (fst (preanalysis tenv f)) pc args) t) eqn:FIND.
-        ** destruct (is_trivial_op op). discriminate.
+        ** destruct (negb (Compopts.optim_CSE3_trivial_ops tt) && is_trivial_op op). discriminate.
            apply exec_Iop with (op := Omove) (args := r :: nil).
            TR_AT.
            subst instr'.
diff --git a/extraction/extraction.v b/extraction/extraction.v
index e4f052ee..34a09330 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -127,6 +127,8 @@ Extract Constant Compopts.optim_CSE3_across_merges =>
   "fun _ -> !Clflags.option_fcse3_across_merges".
 Extract Constant Compopts.optim_CSE3_glb =>
   "fun _ -> !Clflags.option_fcse3_glb".
+Extract Constant Compopts.optim_CSE3_trivial_ops =>
+  "fun _ -> !Clflags.option_fcse3_trivial_ops".
 Extract Constant Compopts.optim_move_loop_invariants =>
   "fun _ -> !Clflags.option_fmove_loop_invariants".