CSE3 now runs on its own fixpoint iterator not based on Kildall.v

2 files changed, 3 insertions, 114 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 390f6d26..bcdebca7 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -509,12 +509,14 @@ Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: inva
              (fun pc' => relb_leb rel' (PMap.get pc' inv))
              (RTL.successors_instr instr)
          end).
+(* No longer used. Incompatible with transfer functions that yield a different result depending on the successor.
 
 Definition internal_analysis
   (tenv : typing_env)
   (f : RTL.function) : option invariants := DS.fixpoint
   (RTL.fn_code f) RTL.successors_instr
   (apply_instr' tenv (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top).
+*)
 End OPERATIONS.
 
 Record analysis_hints :=
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index 5ffa9222..b8f98b0d 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -230,99 +230,7 @@ let add_to_set_in_table table key item =
         | None -> PSet.empty
         | Some s -> s));;
   
-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
-  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
-  match internal_analysis ctx tenv f
-  with None -> failwith "CSE3analysisaux analysis failed, try re-running with -fno-cse3"
-     | Some invariants ->
-        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 preanalysis1 (tenv : typing_env) (f : RTL.coq_function) =
+let preanalysis (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
@@ -411,24 +319,3 @@ let preanalysis1 (tenv : typing_env) (f : RTL.coq_function) =
    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;;