attempt at initial analysis

1 files changed, 35 insertions, 1 deletions

diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index ab8cbeed..39490d79 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -134,6 +134,32 @@ let rb_glb (x : RB.t) (y : RB.t) : RB.t =
   | None, _ | _, None -> None
   | (Some x'), (Some y') -> Some (RELATION.glb x' y');;
 
+let compute_invariants
+      (nodes : RTL.node list)
+      (entrypoint : RTL.node)
+      (successors : RTL.node -> RTL.node list)
+      (tfr : RTL.node -> RB.t -> RB.t) =
+  let todo = ref IntSet.empty
+  and invariants = ref (PMap.set entrypoint (Some RELATION.top) (PMap.init RB.bot)) in  
+  let add_todo (pc : RTL.node) =
+    todo := IntSet.add (P.to_int pc) !todo in 
+  let update_node (pc : RTL.node) =
+    (if !Clflags.option_debug_compcert > 9
+     then Printf.printf "UP updating node %d\n" (P.to_int pc));
+    let cur = PMap.get pc !invariants in
+    List.iter (fun next_pc ->
+        let previous = PMap.get next_pc !invariants in
+        let next = RB.lub previous (tfr pc cur) in
+        if not (RB.beq previous next)
+        then add_todo next_pc) (successors pc) in
+  add_todo entrypoint;
+  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 refine_invariants
       (nodes : RTL.node list)
       (entrypoint : RTL.node)
@@ -146,7 +172,7 @@ let refine_invariants
     todo := IntSet.add (P.to_int pc) !todo in 
   let update_node (pc : RTL.node) =
     (if !Clflags.option_debug_compcert > 9
-     then Printf.printf "updating node %d\n" (P.to_int pc));
+     then Printf.printf "DOWN updating node %d\n" (P.to_int pc));
     if not (peq pc entrypoint)
     then
       let cur = PMap.get pc !invariants in
@@ -176,6 +202,14 @@ let get_default default x ptree =
   | None -> default
   | Some y -> y;;
 
+let initial_analysis ctx tenv (f : RTL.coq_function) =
+  let succ_map = RTL.successors_map f in
+  let succ_f x = get_default [] x succ_map in
+  let tfr = apply_instr' ctx tenv f.RTL.fn_code in
+  compute_invariants
+    (List.map fst (PTree.elements f.RTL.fn_code))
+    f.RTL.fn_entrypoint succ_f tfr;;
+
 let refine_analysis ctx tenv
       (f : RTL.coq_function) (invariants0 : RB.t PMap.t) =
   let succ_map = RTL.successors_map f in