refining CSE3 nodes

1 files changed, 81 insertions, 14 deletions

diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index 8c83dc2e..6e190d35 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -14,7 +14,8 @@ open CSE3analysis
 open Maps
 open HashedSet
 open Camlcoq
-
+open Coqlib
+   
 let flatten_eq eq =
   ((P.to_int eq.eq_lhs), eq.eq_op, List.map P.to_int eq.eq_args);;
 
@@ -98,10 +99,72 @@ 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
+    Printf.fprintf chan "%d: %a\n\n" pc
       (pp_relation_b hints) (PMap.get (P.of_int pc) invariants)
   done
 
+module IntSet=Set.Make(struct type t=int let compare = ( - ) end);;
+
+let rec union_list prev = function
+  | [] -> prev
+  | h::t -> union_list (RB.lub prev h) t;;
+
+let rb_glb (x : RB.t) (y : RB.t) : RB.t =
+  match x, y with
+  | None, _ | _, None -> None
+  | (Some x'), (Some y') -> Some (RELATION.glb x' y');;
+
+let refine_invariants
+      (nodes : RTL.node list)
+      (entrypoint : RTL.node)
+      (successors : RTL.node -> RTL.node list)
+      (predecessors : RTL.node -> RTL.node list)
+      (tfr : RTL.node -> RB.t -> RB.t) (invariants0 : RB.t PMap.t) =
+  let todo = ref IntSet.empty
+  and invariants = ref invariants0 in  
+  let add_todo (pc : RTL.node) =
+    todo := IntSet.add (P.to_int pc) !todo in 
+  let update_node (pc : RTL.node) =
+    Printf.printf "updating node %d\n" (P.to_int pc);
+    if not (peq pc entrypoint)
+    then
+      let cur = PMap.get pc !invariants in
+      let nxt = union_list RB.bot
+                  (List.map
+                     (fun pred_pc->
+                       rb_glb cur
+                         (tfr pred_pc (PMap.get pred_pc !invariants)))
+                     (predecessors pc)) in
+      if not (RB.beq cur nxt)
+      then
+        begin
+          Printf.printf "refining CSE3 node %d\n" (P.to_int pc);
+          List.iter add_todo (successors pc)
+        end in
+  (List.iter add_todo nodes);
+  while not (IntSet.is_empty !todo) do
+    let nxt = IntSet.max_elt !todo in
+    todo := IntSet.remove nxt !todo;
+    update_node (P.of_int nxt)
+  done;
+  !invariants;;
+
+let get_default default x ptree =
+  match PTree.get x ptree with
+  | None -> default
+  | Some y -> y;;
+
+let refine_analysis ctx tenv
+      (f : RTL.coq_function) (invariants0 : RB.t PMap.t) =
+  let succ_map = RTL.successors_map f in
+  let succ_f x = get_default [] x succ_map in
+  let pred_map = Kildall.make_predecessors f.RTL.fn_code RTL.successors_instr in
+  let pred_f x = get_default [] x pred_map in
+  let tfr = apply_instr' ctx tenv f.RTL.fn_code in
+  refine_invariants
+    (List.map fst (PTree.elements f.RTL.fn_code))
+    f.RTL.fn_entrypoint succ_f pred_f tfr invariants0;;
+  
 let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
   let cur_eq_id = ref 0
   and cur_catalog = ref PTree.empty
@@ -113,6 +176,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 o = None then failwith "eq_find_oracle");
     (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);
@@ -161,21 +225,24 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
       pp_eq eq (pp_option pp_P) o);    
     o
   in
-  match
-    internal_analysis
-      { eq_catalog     = (fun eq_id -> PTree.get eq_id !cur_catalog);
-        eq_find_oracle = mutating_eq_find_oracle;
-        eq_rhs_oracle  = rhs_find_oracle ;
-        eq_kill_reg    = (fun reg -> PMap.get reg !cur_kill_reg);
-        eq_kill_mem    = (fun () -> !cur_kill_mem);
-        eq_moves       = (fun reg -> PMap.get reg !cur_moves)
-      } tenv f
+  let ctx = { eq_catalog     = (fun eq_id -> PTree.get eq_id !cur_catalog);
+              eq_find_oracle = mutating_eq_find_oracle;
+              eq_rhs_oracle  = rhs_find_oracle ;
+              eq_kill_reg    = (fun reg -> PMap.get reg !cur_kill_reg);
+              eq_kill_mem    = (fun () -> !cur_kill_mem);
+              eq_moves       = (fun reg -> PMap.get reg !cur_moves)
+            } in
+  match internal_analysis ctx tenv f
   with None -> failwith "CSE3analysisaux analysis failed, try re-running with -fno-cse3"
      | Some invariants ->
-        let hints = { hint_eq_catalog    = !cur_catalog;
+        let invariants' =
+          if ! Clflags.option_fcse3_refine
+          then refine_analysis ctx tenv f invariants
+          else invariants
+        and 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
+         then pp_results f invariants' hints stdout);
+        invariants', hints
 ;;