diff options
-rw-r--r-- | backend/CSE3analysisaux.ml | 36 |
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 |