new CSE3

3 files changed, 107 insertions, 41 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 7316c9a9..cd7e3d84 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -282,12 +282,14 @@ Section OPERATIONS.
 
   Definition oper2 (dst : reg) (op: sym_op)(args : list reg)
            (rel : RELATION.t) : RELATION.t :=
-    let rel' := kill_reg dst rel in
     match eq_find {| eq_lhs := dst;
                      eq_op  := op;
                      eq_args:= args |} with
-    | Some id => PSet.add id rel'
-    | None => rel'
+    | Some id =>
+      if PSet.contains rel id
+      then rel
+      else PSet.add id (kill_reg dst rel)
+    | None => kill_reg dst rel
     end.
 
   Definition oper1 (dst : reg) (op: sym_op) (args : list reg)
@@ -307,12 +309,6 @@ Section OPERATIONS.
       | Some eq_id => PSet.add eq_id (kill_reg dst rel)
       | None => kill_reg dst rel
       end.
-
-  Definition is_trivial_sym_op sop :=
-    match sop with
-    | SOp op => is_trivial_op op
-    | SLoad _ _ => false
-    end.
   
   Definition oper (dst : reg) (op: sym_op) (args : list reg)
              (rel : RELATION.t) : RELATION.t :=
@@ -324,18 +320,18 @@ Section OPERATIONS.
       | _ => kill_reg dst rel
       end
     else
-      if is_trivial_sym_op op
-      then kill_reg dst rel
-      else
-        let args' := forward_move_l rel args in
-        match rhs_find op args' rel with
-        | Some r =>
-          if Compopts.optim_CSE3_glb tt
-          then RELATION.glb (move r dst rel)
-                            (oper1 dst op args' rel)
-          else oper1 dst op args' rel
-        | None => oper1 dst op args' rel
-        end.
+      let args' := forward_move_l rel args in
+      match rhs_find op args' rel with
+      | Some r =>
+        if Compopts.optim_CSE3_glb tt
+        then RELATION.glb (move r dst rel)
+                          (RELATION.glb (oper1 dst op args' rel)
+                                        (oper1 dst op args rel))
+        else RELATION.glb (oper1 dst op args' rel)
+                          (oper1 dst op args rel)
+      | None => RELATION.glb (oper1 dst op args' rel)
+                             (oper1 dst op args rel)
+      end.
   
   Definition clever_kill_store
              (chunk : memory_chunk) (addr: addressing) (args : list reg)
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index 3990b765..8c83dc2e 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -39,12 +39,12 @@ let print_reg channel i =
 let print_eq channel (lhs, sop, args) =
   match sop with
   | SOp op ->
-     Printf.printf "%a = %a\n" print_reg lhs (PrintOp.print_operation print_reg) (op, args)
+     Printf.printf "%a = %a" print_reg lhs (PrintOp.print_operation print_reg) (op, args)
   | SLoad(chunk, addr) ->
-     Printf.printf "%a = %s @ %a\n" print_reg lhs (string_of_chunk chunk)
+     Printf.printf "%a = %s @ %a" print_reg lhs (string_of_chunk chunk)
        (PrintOp.print_addressing print_reg) (addr, args);;
 
-let pp_set oc s =
+let pp_intset oc s =
   Printf.fprintf oc "{ ";
   List.iter (fun i -> Printf.fprintf oc "%d; " (P.to_int i)) (PSet.elements s);
   Printf.fprintf oc "}";;
@@ -70,6 +70,38 @@ let pp_option pp oc = function
 let is_trivial eq =
   (eq.eq_op = SOp Op.Omove) && (eq.eq_args = [eq.eq_lhs]);;
 
+let rec pp_list separator pp_item chan = function
+  | [] -> ()
+  | [h] -> pp_item chan h
+  | h::t ->
+     pp_item chan h;
+     output_string chan separator;
+     pp_list separator pp_item chan t;;
+
+let pp_set separator pp_item chan s =
+  pp_list separator pp_item chan (PSet.elements s);;
+
+let pp_equation hints chan x =
+  match PTree.get x hints.hint_eq_catalog with
+  | None -> output_string chan "???"
+  | Some eq ->
+     print_eq chan  (P.to_int eq.eq_lhs, eq.eq_op, List.map P.to_int eq.eq_args);;
+
+let pp_relation hints chan rel =
+  pp_set "; " (pp_equation hints) chan rel;;
+
+let pp_relation_b hints chan = function
+  | None -> output_string chan "bot"
+  | Some rel -> pp_relation hints chan rel;;
+
+let pp_results f (invariants : RB.t PMap.t) hints chan =
+  let max_pc = P.to_int (RTL.max_pc_function f) in
+  for pc=max_pc downto 1
+  do
+    Printf.fprintf chan "%d: %a\n" pc
+      (pp_relation_b hints) (PMap.get (P.of_int pc) invariants)
+  done
+
 let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
   let cur_eq_id = ref 0
   and cur_catalog = ref PTree.empty
@@ -81,7 +113,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
   let eq_find_oracle node eq =
     assert (not (is_trivial eq));
     let o = Hashtbl.find_opt eq_table (flatten_eq eq) in
-    (if !Clflags.option_debug_compcert > 1
+    (if !Clflags.option_debug_compcert > 5
      then Printf.printf "@%d: eq_find %a -> %a\n" (P.to_int node)
             pp_eq eq (pp_option pp_P) o);
     o
@@ -90,9 +122,9 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
       match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with
       | None -> PSet.empty
       | Some s -> s in
-    (if !Clflags.option_debug_compcert > 1
+    (if !Clflags.option_debug_compcert > 5
      then Printf.printf "@%d: rhs_find %a = %a\n"
-            (P.to_int node) pp_rhs (sop, args) pp_set o);
+            (P.to_int node) pp_rhs (sop, args) pp_intset o);
     o in
   let mutating_eq_find_oracle node eq : P.t option =
     let (flat_eq_lhs, flat_eq_op, flat_eq_args) as flat_eq = flatten_eq eq in
@@ -124,7 +156,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
          Some coq_id
        end
     in
-    (if !Clflags.option_debug_compcert > 1
+    (if !Clflags.option_debug_compcert > 5
      then Printf.printf "@%d: mutating_eq_find %a -> %a\n" (P.to_int node)
       pp_eq eq (pp_option pp_P) o);    
     o
@@ -140,7 +172,10 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
       } tenv f
   with None -> failwith "CSE3analysisaux analysis failed, try re-running with -fno-cse3"
      | Some invariants ->
-        invariants,
-        { hint_eq_catalog    = !cur_catalog;
-          hint_eq_find_oracle= eq_find_oracle;
-          hint_eq_rhs_oracle = rhs_find_oracle };;
+        let hints = { hint_eq_catalog    = !cur_catalog;
+                      hint_eq_find_oracle= eq_find_oracle;
+                      hint_eq_rhs_oracle = rhs_find_oracle } in
+        (if !Clflags.option_debug_compcert > 1
+         then pp_results f invariants hints stdout);
+        invariants, hints
+;;
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 66b199cc..ea4d37ca 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -699,6 +699,28 @@ Section SOUNDNESS.
       + congruence.
   Qed.
 
+
+  Lemma arglist_idem_write:
+    forall { A : Type} args (rs : Regmap.t A) dst,
+      (rs # dst <- (rs # dst)) ## args = rs ## args.
+  Proof.
+    induction args; trivial.
+    intros. cbn.
+    f_equal; trivial.
+    apply Regmap.gsident.
+  Qed.
+  
+  Lemma sem_rhs_idem_write:
+    forall sop args rs dst m v,
+      sem_rhs sop args rs m v ->
+      sem_rhs sop args (rs # dst <- (rs # dst)) m v.
+  Proof.
+    intros.
+    unfold sem_rhs in *.
+    rewrite arglist_idem_write.
+    assumption.
+  Qed.
+  
   Theorem oper2_sound:
     forall no dst sop args rel rs m v,
       sem_rel rel rs m ->
@@ -726,6 +748,17 @@ Section SOUNDNESS.
       rewrite Regmap.gss.
       apply sem_rhs_depends_on_args_only; auto.
     }
+    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 i eq CONTAINS INi) as RELi.
+      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.
+      assumption.
+    }
     rewrite PSet.gaddo in CONTAINS by congruence.
     apply (kill_reg_sound rel rs m dst v REL i eq); auto.
   Qed.
@@ -821,11 +854,7 @@ 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.
@@ -833,12 +862,18 @@ Section SOUNDNESS.
              2: eassumption.
              rewrite <- (sem_rhs_det SOUND RHS).
              apply move_sound; auto.
+          ** apply sem_rel_glb; split.
+             *** apply oper1_sound; auto.
+                 apply forward_move_rhs_sound; auto.
+             *** apply oper1_sound; auto.
+        * apply sem_rel_glb; split.
           ** 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 oper1_sound; auto.
+      + apply sem_rel_glb; split.
+        * apply oper1_sound; auto.
+          apply forward_move_rhs_sound; auto.
+        * apply oper1_sound; auto.
   Qed.
 
   Hint Resolve oper_sound : cse3.