From 0f9018baabe8feeed19d8f7e14f8480e898b5a84 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 8 Dec 2020 19:56:28 +0100 Subject: CSE3 now runs on its own fixpoint iterator not based on Kildall.v --- backend/CSE3analysis.v | 2 + backend/CSE3analysisaux.ml | 115 +-------------------------------------------- 2 files changed, 3 insertions(+), 114 deletions(-) (limited to 'backend') 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;; -- cgit