start checking for bugs

1 files changed, 115 insertions, 2 deletions

diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index 39490d79..5ffa9222 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -151,7 +151,9 @@ let compute_invariants
         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
+        then (
+          invariants := PMap.set next_pc next !invariants;
+          add_todo next_pc)) (successors pc) in
   add_todo entrypoint;
   while not (IntSet.is_empty !todo) do
     let nxt = IntSet.max_elt !todo in
@@ -228,7 +230,7 @@ let add_to_set_in_table table key item =
         | None -> PSet.empty
         | Some s -> s));;
   
-let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
+let preanalysis0 (tenv : typing_env) (f : RTL.coq_function) =
   let cur_eq_id = ref 0
   and cur_catalog = ref PTree.empty
   and eq_table = Hashtbl.create 100
@@ -319,3 +321,114 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
          then pp_results f invariants' hints stdout);
         invariants', hints
 ;;
+  
+let preanalysis1 (tenv : typing_env) (f : RTL.coq_function) =
+  let cur_eq_id = ref 0
+  and cur_catalog = ref PTree.empty
+  and eq_table = Hashtbl.create 100
+  and rhs_table = Hashtbl.create 100
+  and cur_kill_reg = ref (PMap.init PSet.empty)
+  and cur_kill_mem = ref PSet.empty
+  and cur_kill_store = ref PSet.empty
+  and cur_moves = ref (PMap.init PSet.empty) in
+  let eq_find_oracle node eq =
+    assert (not (is_trivial eq));
+    let o = Hashtbl.find_opt eq_table (flatten_eq eq) in
+    (* FIXME (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);
+    o
+  and rhs_find_oracle node sop args =
+    let o =
+      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 > 5
+     then Printf.printf "@%d: rhs_find %a = %a\n"
+            (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 = flatten_eq eq in
+    let o =
+    match Hashtbl.find_opt eq_table flat_eq with
+    | Some x ->
+       Some x
+    | None ->
+       (* TODO print_eq stderr flat_eq; *)
+       incr cur_eq_id;
+       let id = !cur_eq_id in
+       let coq_id = P.of_int id in
+       begin
+         Hashtbl.add eq_table flat_eq coq_id;
+         (cur_catalog := PTree.set coq_id eq !cur_catalog);
+         (match flat_eq with
+          | Flat_equ(flat_eq_lhs, flat_eq_op, flat_eq_args) ->
+             add_to_set_in_table rhs_table
+               (flat_eq_op, flat_eq_args) coq_id
+          | Flat_cond(flat_eq_cond, flat_eq_args) -> ());
+         (match eq with
+          | Equ(lhs, sop, args) ->
+             List.iter
+               (fun reg -> imp_add_i_j cur_kill_reg reg coq_id)
+               (lhs :: args);
+             (match sop, args with
+              | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves lhs coq_id
+              | _, _ -> ())
+          | Cond(cond, args) ->
+             List.iter
+               (fun reg -> imp_add_i_j cur_kill_reg reg coq_id) args
+         );
+         (if eq_cond_depends_on_mem eq
+          then cur_kill_mem := PSet.add coq_id !cur_kill_mem);
+         (if eq_cond_depends_on_store eq
+          then cur_kill_store := PSet.add coq_id !cur_kill_store);
+         Some coq_id
+       end
+    in
+    (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
+  in
+  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_kill_store  = (fun () -> !cur_kill_store);
+              eq_moves       = (fun reg -> PMap.get reg !cur_moves)
+            } in
+  let invariants = initial_analysis ctx tenv f in
+  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
+;;
+
+let check_same_invariants max_pc invariants0 invariants1 =
+  for pc=1 to max_pc
+  do
+    let p_pc = P.of_int pc in
+    if not (RB.beq (PMap.get p_pc invariants0)
+                   (PMap.get p_pc invariants1))
+    then failwith (Printf.sprintf "check_same_invariants at %d" pc)
+  done;;
+
+let check_same_catalog catalog0 catalog1 =
+  if not (PTree.beq eq_dec_equation catalog0 catalog1)
+  then failwith "catalogs not equal";;
+
+let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
+  let invariants0, hints0 = preanalysis0 tenv f
+  and invariants1, hints1 = preanalysis1 tenv f in
+  check_same_invariants (P.to_int (RTL.max_pc_function f))
+    invariants0 invariants1;
+  check_same_catalog hints0.hint_eq_catalog hints1.hint_eq_catalog;
+  invariants1, hints1;;