From a100edde18de43cf933c0d53467e196541436e13 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 2 Dec 2020 19:00:21 +0100 Subject: start checking for bugs --- backend/CSE3analysisaux.ml | 117 ++++++++++++++++++++++++++++++++++++++++++++- driver/Clflags.ml | 2 +- 2 files changed, 116 insertions(+), 3 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;; diff --git a/driver/Clflags.ml b/driver/Clflags.ml index bc8a7925..8286f4f3 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -34,7 +34,7 @@ let option_fcse3_across_calls = ref false let option_fcse3_across_merges = ref true let option_fcse3_glb = ref true let option_fcse3_trivial_ops = ref false -let option_fcse3_refine = ref true +let option_fcse3_refine = ref false (* DM *) let option_fredundancy = ref true (** Options relative to superblock scheduling *) -- cgit