diff --git a/src/kernel_services/analysis/dominators.ml b/src/kernel_services/analysis/dominators.ml
index 8dc4629755e990d31dd5a5fc8e46af27c01a2568..bb04d918fa5a2e657e2d026e4d9ff9673d87cc07 100644
--- a/src/kernel_services/analysis/dominators.ml
+++ b/src/kernel_services/analysis/dominators.ml
@@ -20,261 +20,245 @@
(* *)
(**************************************************************************)
-(** Computation of dominators.
- Based on "A Simple, Fast Dominance Algorithm" by K. D. Cooper et al. *)
-
-(* A domination tree, represented as a map from a statement to its
- immediate dominator. The first statement in a function, and
- statically unreachable statements (that do not have idoms), are
- mapped to None. *)
-module Dom_tree = State_builder.Hashtbl
- (Cil_datatype.Stmt.Hashtbl)
- (Datatype.Option(Cil_datatype.Stmt))
- (struct
- let name = "Dominators.dom_tree"
- let dependencies = [ Ast.self ]
- let size = 197
- end)
-;;
-
-(** Compute dominator information for the statements in a function *)
+(* This module performs dataflow analysis using [Interpreted_automata] to
+ compute the domination/postdomination dependencies between statements of a
+ given function. *)
+
open Cil_types
-(****************************************************************)
+let dkey = Kernel.dkey_dominators
-module type DIRECTION = sig
- (* Number of statements in the function. *)
- val nb_stmts: int
+(* Datatype used to create a dot graph using analysis results. *)
+module StmtTbl = Cil_datatype.Stmt.Hashtbl
- (* Conversion between statements and ordered statements. *)
- val to_ordered: stmt -> Ordered_stmt.ordered_stmt
- val to_stmt: Ordered_stmt.ordered_stmt -> stmt
+(* State type for our domain. *)
+module StmtSet = Cil_datatype.Stmt.Hptset
- (* Iterates on all the statements, except the roots of the
- domination tree; in topological order for dominators, and reverse
- topological order for the post-dominators. *)
- val iter: (Ordered_stmt.ordered_stmt -> unit) -> unit
+module DotGraph = Graph.Graphviz.Dot (
+ struct
+ type t = string * (StmtSet.t StmtTbl.t)
+ module V = struct type t = stmt end
+ module E = struct
+ type t = (V.t * V.t)
+ let src = fst
+ let dst = snd
+ end
- (* Entry point (for dominators) or return (for post-dominators),
- that will be the root of the dominator/post-dominator tree. *)
- val root_stmt: Ordered_stmt.ordered_stmt;;
+ let iter_vertex f (_, graph) =
+ StmtTbl.iter (fun stmt _ -> f stmt) graph
- val is_further_from_root:
- Ordered_stmt.ordered_stmt -> Ordered_stmt.ordered_stmt -> bool
+ let iter_edges_e f (_, graph) =
+ StmtTbl.iter (fun stmt -> StmtSet.iter (fun p -> f (p, stmt))) graph
- (* List of all predecessors for the dominators, list of successors
- for the post-dominators (for the post-dominators, it can be seen
- as the predecessors in the reversed control flow graph that goes
- from the sinks to the entry point). *)
- val preds: Ordered_stmt.ordered_stmt -> Ordered_stmt.ordered_stmt list
+ let graph_attributes (title, _) = [`Label title]
- val name:string
-end
+ let default_vertex_attributes _g = [`Shape `Box; `Style `Filled]
+
+ let vertex_name stmt = string_of_int stmt.sid
+
+ let vertex_attributes stmt =
+ let txt = Format.asprintf "%a" Cil_printer.pp_stmt stmt in
+ [`Label txt]
+
+ let default_edge_attributes _g = []
+
+ let edge_attributes _s = []
+
+ let get_subgraph _v = None
+ end)
+
+(* Both analyses use this domain, which propagates all encountered statements
+ by adding them to the state. The [join] performs an intersection which is
+ enough to compute domination/postdomination. *)
+module Domain = struct
+ type t = StmtSet.t
+
+ let join = StmtSet.inter
-module Compute(D:DIRECTION) = struct
-
- (* Computes the smallest common dominator between two statements. *)
- let nearest_common_ancestor find_domtree ord1 ord2 =
- Kernel.debug ~dkey:Kernel.dkey_dominators "computing common ancestor %d %d"
- (D.to_stmt ord1).sid (D.to_stmt ord2).sid;
- let finger1 = ref ord1 in
- let finger2 = ref ord2 in
- while (!finger1 != !finger2) do (
- while ( D.is_further_from_root !finger1 !finger2) do
- finger1 := (match find_domtree !finger1 with
- | None -> assert false
- | Some x -> x)
- done;
- while ( D.is_further_from_root !finger2 !finger1) do
- finger2 := (match find_domtree !finger2 with
- | None -> assert false
- | Some x -> x)
- done;)
- done;
- !finger1
- ;;
-
- (* Note: None means either unprocessed, or that the statement has no
- predecessor or that all its ancestors are at None *)
- (* based on "A Simple, Fast Dominance Algorithm" by K.D. Cooper et al *)
- let domtree () =
- let domtree = Array.make D.nb_stmts None in
-
- (* Initialize the dataflow: for each root, add itself to its own
- set of dominators. *)
- domtree.(D.root_stmt) <- Some D.root_stmt;
- let changed = ref true in
- while !changed do
- changed := false;
- D.iter (fun b ->
- let ordered_preds = D.preds b in
- let processed_preds =
- let was_processed p = match domtree.(p) with
- | None -> false
- | Some(_) -> true
- in
- List.filter was_processed ordered_preds
- in
- match processed_preds with
- | [] -> () (* No predecessor (e.g. unreachable stmt): leave it to None.*)
- | first::rest ->
- let find i = domtree.(i) in
- let new_idom =
- List.fold_left (nearest_common_ancestor find) first rest
- in
- (match domtree.(b) with
- | Some(old_idom) when old_idom == new_idom -> ()
- | _ -> (domtree.(b) <- Some(new_idom); changed := true))
- );
- done;
- (* The roots are not _immediate_ dominators of themselves, so revert
- that now that the dataflow has finished. *)
- domtree.(D.root_stmt) <- None;
- domtree
- ;;
-
- let display domtree =
- Kernel.debug ~dkey:Kernel.dkey_dominators "Root is %d" (D.to_stmt 0).sid;
- Array.iteri (fun orig dest -> match dest with
- | Some(x) -> Kernel.debug ~dkey:Kernel.dkey_dominators "%s of %d is %d"
- D.name (D.to_stmt orig).sid (D.to_stmt x).sid
- | None -> Kernel.debug ~dkey:Kernel.dkey_dominators "no %s for %d"
- D.name (D.to_stmt orig).sid)
- domtree
- ;;
+ let widen a b =
+ if StmtSet.subset a b then
+ Interpreted_automata.Fixpoint
+ else
+ Interpreted_automata.Widening (join a b)
+ (* Trivial transfer function: add all visited statements to the current
+ state. *)
+ let transfer v _ state =
+ match v.Interpreted_automata.vertex_start_of with
+ | None -> Some state
+ | Some stmt -> Some (StmtSet.add stmt state)
end
-let direction_dom kf =
- let (stmt_to_ordered,ordered_to_stmt,_) =
- Ordered_stmt.get_conversion_tables kf
- in
- let to_stmt = Ordered_stmt.to_stmt ordered_to_stmt in
- let module Dominator = struct
- let to_ordered = Ordered_stmt.to_ordered stmt_to_ordered;;
- let to_stmt = to_stmt;;
- let nb_stmts = Array.length ordered_to_stmt;;
- let root_stmt = to_ordered (Kernel_function.find_first_stmt kf)
- (* Iterate on all statements, except the entry point. *)
- let iter f =
- for i = 0 to nb_stmts -1 do
- if i != root_stmt
- then f i
- done;;
- let is_further_from_root p1 p2 = p1 > p2
- let preds s = List.map to_ordered (to_stmt s).Cil_types.preds
- let name = "dom"
- end
- in
- (module Dominator: DIRECTION)
-;;
-
-(* Fill the project table with the dominators of a given function. *)
-let store_dom domtree to_stmt =
- Array.iteri( fun ord idom ->
- let idom = Option.map to_stmt idom in
- let stmt = to_stmt ord in
- Kernel.debug ~dkey:Kernel.dkey_dominators "storing dom for %d: %s"
- stmt.sid (match idom with None -> "self" | Some s ->string_of_int s.sid);
- Dom_tree.add stmt idom
- ) domtree
-
-let compute_dom kf =
- let direction = direction_dom kf in
- let module Dominator = (val direction: DIRECTION) in
- let module ComputeDom = Compute(Dominator) in
- let domtree = ComputeDom.domtree () in
- store_dom domtree Dominator.to_stmt
-;;
-
-(* Note: The chosen semantics for postdominator is the following one: a
- post-dominates b if all the paths from b to the return statement
- goes through a.
-
- Statements on the paths that go only into infinite loop, or to
- __no_return function, do not have any post dominator (they are set
- to None).
-
- This definition of post-dominator gives a single root to the
- post-domination tree, which is required by the Cooper algorithm
- above. Beware that there are alternative, incompatible, definitions
- to post-domination, e.g. saying that a post dominates b if all the
- paths from b to any return statement or infinite loop go through
- a. *)
-(* TODO:
- - For each statement, associate its immediate post-dominator (if it
- exists), and the list of sinks that dominates it
-
- - Attempt to find the post-dominator by intersection only if the
- list of sinks of the points is the same. Otherwise, state that
- there is no immediate post-dominator, and that the point is
- dominated by the union of the lists of sinks of its successors.
-*)
-let _compute_pdom kf =
- let (stmt_to_ordered,ordered_to_stmt,_) =
- Ordered_stmt.get_conversion_tables kf
- in
- let module PostDominator = struct
- let to_ordered = Ordered_stmt.to_ordered stmt_to_ordered;;
- let to_stmt = Ordered_stmt.to_stmt ordered_to_stmt;;
- let nb_stmts = Array.length ordered_to_stmt;;
- let root_stmt = to_ordered (Kernel_function.find_return kf)
- let iter f =
- for i = nb_stmts -1 downto 0 do
- if i != root_stmt
- then f i
- done;;
- let is_further_from_root p1 p2 = p1 < p2
- let preds s = List.map to_ordered (to_stmt s).Cil_types.succs
- let name = "postdom"
- end
- in
- let module ComputePDom = Compute(PostDominator) in
- let domtree = ComputePDom.domtree () in
- ComputePDom.display domtree
-;;
-
-(****************************************************************)
-(* For each statement we maintain a set of statements that dominate it *)
-
-(* Try to find the idom, and fill the table if not already computed. *)
-let get_idom s =
- try Dom_tree.find s
- with Not_found ->
- let kf = Kernel_function.find_englobing_kf s in
- let _ = (compute_dom kf) in
- try Dom_tree.find s
- with _ -> assert false
-;;
-
-(** Check whether one block dominates another. This assumes that the "idom"
- * field has been computed. *)
-let rec dominates (s1: stmt) (s2: stmt) =
- s1.sid = s2.sid ||
- match (get_idom s2) with
- | None -> false
- | Some s2idom -> dominates s1 s2idom
-
-let nearest_common_ancestor l =
- match l with
- | [] -> failwith ""
- | s :: _ ->
- let kf = Kernel_function.find_englobing_kf s in
- let direction = direction_dom kf in
- let module Dominator = (val direction: DIRECTION) in
- let module ComputeDom = Compute(Dominator) in
- (try ignore (Dom_tree.find s)
- with Not_found ->
- let domtree = ComputeDom.domtree () in
- store_dom domtree Dominator.to_stmt
- );
- let to_ordered = Dominator.to_ordered in
- let to_stmt = Dominator.to_stmt in
- let find i = Option.map to_ordered (Dom_tree.find (to_stmt i)) in
- let rec aux = function
- | [] -> assert false
- | [s] -> to_ordered s
- | s :: (_ :: _ as q) ->
- ComputeDom.nearest_common_ancestor find (to_ordered s) (aux q)
+(* An analysis needs a name and a starting point. *)
+module type Analysis = sig
+ val name : string
+ (* May raise Kernel_function.No_Statement. *)
+ val get_starting_stmt : kernel_function -> stmt
+ include Interpreted_automata.DataflowAnalysis with type state = Domain.t
+end
+
+(* Main module, perform the analysis, store its results and provide ways to
+ access them. *)
+module Compute (Analysis : Analysis) = struct
+
+ module Table =
+ Cil_state_builder.Stmt_hashtbl
+ (StmtSet)
+ (struct
+ let name = Analysis.name ^ "_table"
+ let dependencies = [Ast.self]
+ let size = 503
+ end)
+
+ let compute kf =
+ match Table.find_opt (Analysis.get_starting_stmt kf) with
+ | exception Kernel_function.No_Statement ->
+ Kernel.warning "No statement in function %a: %s analysis cannot be done"
+ Kernel_function.pretty kf Analysis.name
+ | Some _ ->
+ Kernel.feedback ~dkey "%s analysis already computed for function %a"
+ Analysis.name Kernel_function.pretty kf
+ | None ->
+ match kf.fundec with
+ | Definition (f, _) ->
+ Kernel.feedback ~dkey "computing %s analysis for function %a"
+ Analysis.name Kernel_function.pretty kf;
+ (* Compute the analysis, initial state is empty. *)
+ let result = Analysis.fixpoint kf StmtSet.empty in
+ (* Fill table with all statements. *)
+ List.iter (fun stmt -> Table.add stmt StmtSet.empty) f.sallstmts;
+ (* A reachable statement always (post)dominates itself, so add it here. *)
+ let add_in_table stmt set = Table.replace stmt (StmtSet.add stmt set) in
+ (* Update the table with analysis results. *)
+ Analysis.Result.iter_stmt add_in_table result;
+ Kernel.feedback ~dkey "%s analysis done for function %a"
+ Analysis.name Kernel_function.pretty kf
+ (* [Analysis.get_starting_stmt] should fatal before this point. *)
+ | Declaration _ -> assert false
+
+ let find_kf stmt =
+ try Kernel_function.find_englobing_kf stmt
+ with Not_found ->
+ Kernel.fatal "Statement %d is not part of a function" stmt.sid
+
+ (* Generic function to get the set of (post)dominators of [stmt]. *)
+ let get stmt =
+ match Table.find_opt stmt with
+ | None -> compute (find_kf stmt); Table.find stmt
+ | Some v -> v
+
+ (* Generic function to get the set of strict (post)dominators of [stmt]. *)
+ let get_strict stmt = get stmt |> StmtSet.remove stmt
+
+ (* Generic function to test the (post)domination of 2 statements. *)
+ let mem a b = get b |> StmtSet.mem a
+
+ (* Generic function to test the strict (post)domination of 2 statements. *)
+ let mem_strict a b = get_strict b |> StmtSet.mem a
+
+ (* The nearest common ancestor (resp. child) is the ancestor which is
+ dominated (resp. postdominated) by all common ancestors, ie. the lowest
+ (resp. highest) ancestor in the domination tree. *)
+ let nearest stmtl =
+ (* Get the set of strict (post)doms for each statement and intersect them to
+ keep the common ones. If one of them is unreachable, they do not
+ share a common ancestor/child. *)
+ let common_set =
+ match stmtl with
+ | [] -> StmtSet.empty
+ | stmt :: tail ->
+ List.fold_left
+ (fun acc s -> StmtSet.inter acc (get_strict s))
+ (get_strict stmt) tail
in
- Dominator.to_stmt (aux l)
+ (* Try to find a statement [s] in [common_set] which is (post)dominated by
+ all statements of the [common_set]. *)
+ let is_dom_by_all a = StmtSet.for_all (fun b -> mem b a) common_set in
+ List.find_opt is_dom_by_all (StmtSet.elements common_set)
+
+ let pretty fmt () =
+ let list = Table.to_seq () |> List.of_seq in
+ let pp_set fmt set =
+ Pretty_utils.pp_iter ~pre:"@[{" ~sep:",@," ~suf:"}@]"
+ StmtSet.iter (fun fmt stmt -> Format.pp_print_int fmt stmt.sid)
+ fmt set
+ in
+ Pretty_utils.pp_list ~pre:"@[<v>" ~sep:"@;" ~suf:"@]" ~empty:"Empty"
+ (fun fmt (s, set) -> Format.fprintf fmt "Stmt:%d -> %a" s.sid pp_set set)
+ fmt list
+
+ (* [s_set] are [s] (post)dominators, including [s]. We don't have to represent
+ the relation between [s] and [s], so [get_set] removes it. And because the
+ (post)domination relation is transitive, if [p] is in [s_set], we can
+ remove [p_set] from [s_set] in order to have a clearer graph. *)
+ let reduce graph s =
+ (* Union of all (post)dominators of [s] (post)dominators [s_set]. *)
+ let unions p acc = StmtTbl.find graph p |> StmtSet.union acc in
+ let s_set = StmtTbl.find graph s in
+ let p_sets = StmtSet.fold unions s_set StmtSet.empty in
+ let res = StmtSet.diff s_set p_sets in
+ StmtTbl.replace graph s res
+
+ let print_dot basename kf =
+ match kf.fundec with
+ | Definition (fct, _) ->
+ let graph = StmtTbl.create (List.length fct.sallstmts) in
+ let copy_in_graph stmt = get_strict stmt |> StmtTbl.replace graph stmt in
+ List.iter copy_in_graph fct.sallstmts;
+ List.iter (reduce graph) fct.sallstmts;
+ let name = Kernel_function.get_name kf in
+ let title = Format.sprintf "%s for function %s" Analysis.name name in
+ let filename = basename ^ "." ^ Kernel_function.get_name kf ^ ".dot" in
+ let file = open_out filename in
+ DotGraph.output_graph file (title, graph);
+ close_out file;
+ Kernel.result "%s: dot file generated in %s for function %a"
+ Analysis.name filename Kernel_function.pretty kf
+ | Declaration _ ->
+ Kernel.warning "cannot compute %s for function %a without body"
+ Analysis.name Kernel_function.pretty kf
+end
+
+(* ---------------------------------------------------------------------- *)
+(* --- Dominators --- *)
+(* ---------------------------------------------------------------------- *)
+
+module ForwardAnalysis = struct
+ include Interpreted_automata.ForwardAnalysis (Domain)
+ let name = "Dominators"
+ let get_starting_stmt kf = Kernel_function.find_first_stmt kf
+end
+
+module Dominators = Compute (ForwardAnalysis)
+
+let compute_dominators = Dominators.compute
+let get_dominators = Dominators.get
+let get_strict_dominators = Dominators.get_strict
+let dominates = Dominators.mem
+let strictly_dominates = Dominators.mem_strict
+let get_idom s = Dominators.nearest [s]
+let nearest_common_ancestor = Dominators.nearest
+let pretty_dominators = Dominators.pretty
+let print_dot_dominators = Dominators.print_dot
+
+(* ---------------------------------------------------------------------- *)
+(* --- Postdominators --- *)
+(* ---------------------------------------------------------------------- *)
+
+module BackwardAnalysis = struct
+ include Interpreted_automata.BackwardAnalysis (Domain)
+ let name = "PostDominators"
+ let get_starting_stmt kf = Kernel_function.find_return kf
+end
+
+module PostDominators = Compute (BackwardAnalysis)
+
+let compute_postdominators = PostDominators.compute
+let get_postdominators = PostDominators.get
+let get_strict_postdominators = PostDominators.get_strict
+let postdominates = PostDominators.mem
+let strictly_postdominates = PostDominators.mem_strict
+let get_ipostdom s = PostDominators.nearest [s]
+let nearest_common_child = PostDominators.nearest
+let pretty_postdominators = PostDominators.pretty
+let print_dot_postdominators = PostDominators.print_dot
diff --git a/src/kernel_services/analysis/dominators.mli b/src/kernel_services/analysis/dominators.mli
index 55a4e6129e3c7fdf69f9d6ca006f8161b291d0d7..449394b370df919babc60c39be1013611b72146a 100644
--- a/src/kernel_services/analysis/dominators.mli
+++ b/src/kernel_services/analysis/dominators.mli
@@ -20,22 +20,90 @@
(* *)
(**************************************************************************)
-(** Computation of dominators. *)
-open Cil_types;;
+(** Module to perform dominators and postdominators analyses. This module was
+ completely redesigned and provides many new functions.
-val get_idom: stmt -> stmt option
-(** Immediate dominator of the statement. *)
+ A dominator [d] of [s] is a statement such that all paths from the entry
+ point of a function to [s] must go through [d].
-val dominates: stmt -> stmt -> bool
-(** [dominates a b] tells whether [a] dominates [b]. *)
+ A postdominator [p] of [s] is a statement such that all paths from [s] to
+ the return point of the function must go through [p].
-val nearest_common_ancestor: stmt list -> stmt
-(** Finds the statement lowest in the function that dominates
- all the statements in the list passed as argument. The list must not
- be empty, and must contain statements that are all in the same function. *)
+ By definition, a statement always (post)dominates itself (except if it is
+ unreachable).
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
+ An immediate (post)dominator (or i(post)dom) [d] is the unique
+ (post)dominator of [s] that strictly (post)dominates [s] but is
+ (post)dominated by all other (post)dominators of [s].
+
+ A common ancestor (or child) of a list of statements is a (post)dominator
+ that (post)dominates all the statements
+
+ @since Frama-C+dev
+*)
+
+open Cil_types
+
+val compute_dominators : kernel_function -> unit
+(** Compute the Dominators analysis and register its result. *)
+
+val compute_postdominators : kernel_function -> unit
+(** Compute the Postdominators analysis and register its result. *)
+
+val get_dominators : stmt -> Cil_datatype.Stmt.Hptset.t
+(** Return the [set] of dominators of the given statement.
+ The empty set means the statement is unreachable. *)
+
+val get_postdominators : stmt -> Cil_datatype.Stmt.Hptset.t
+(** Return the [set] of postdominators of the given statement.
+ The empty set means the statement is unreachable. *)
+
+val get_strict_dominators : stmt -> Cil_datatype.Stmt.Hptset.t
+(** Same as [get_dominators] but exclude the statement itself. The empty set
+ means the statement is unreachable or is only dominated by itself. *)
+
+val get_strict_postdominators : stmt -> Cil_datatype.Stmt.Hptset.t
+(** Same as [get_postdominators] but exclude the statement itself. The empty set
+ means the statement is unreachable or is only post-dominated by itself. *)
+
+val dominates : stmt -> stmt -> bool
+(** [dominates a b] return [true] if [a] dominates [b]. *)
+
+val postdominates : stmt -> stmt -> bool
+(** [postdominates a b] return [true] if [a] postdominates [b]. *)
+
+val strictly_dominates : stmt -> stmt -> bool
+(** [strictly_dominates a b] return [true] if [a] strictly dominates [b]. *)
+
+val strictly_postdominates : stmt -> stmt -> bool
+(** [strictly_postdominates a b] return [true] if [a] strictly postdominates
+ [b]. *)
+
+val get_idom : stmt -> stmt option
+(** Return the immediate dominator of the given statement. *)
+
+val get_ipostdom : stmt -> stmt option
+(** Return the immediate postdominator of the given statement. *)
+
+val nearest_common_ancestor : stmt list -> stmt option
+(** Return the closest common ancestor of the given statement list.
+ @before Frama-C+dev previous implementation always returned a statement and
+ raised a failed assertion in case of unreachable statement.
*)
+
+val nearest_common_child : stmt list -> stmt option
+(** Return the closest common child of the given statement list. *)
+
+val pretty_dominators : Format.formatter -> unit -> unit
+(** Print the result of the domination analysis. Each statement is either
+ dominated by a set of statements, or [Top] if unreachable. *)
+
+val pretty_postdominators : Format.formatter -> unit -> unit
+(** Print the result of the postdomination analysis. Each statement is either
+ postdominated by a set of statements, or [Top] if unreachable. *)
+
+val print_dot_dominators : string -> kernel_function -> unit
+(** Print the domination graph in a file [basename.function_name.dot]. *)
+
+val print_dot_postdominators : string -> kernel_function -> unit
+(** Print the postdomination graph in a file [basename.function_name.dot]. *)
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index a6a9f9c33f1d6ac199a1f8acdf89798ff3a71d50..b08afe582914426698762bcaa24db2ea7efaf6c9 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -168,12 +168,9 @@ module TransferTaint = struct
from the tainted assume that not go through [stmt], ie [stmt] is not a
postdominator for the tainted assume. *)
let filter_active_tainted_assumes stmt state =
- let kf = Kernel_function.find_englobing_kf stmt in
let assume_stmts =
Stmt.Set.filter
- (fun assume_stmt ->
- not (Postdominators.is_postdominator kf
- ~opening:assume_stmt ~closing:stmt))
+ (fun assume_stmt -> not (Dominators.postdominates stmt assume_stmt))
state.assume_stmts
in
{ state with assume_stmts }
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index 56e7f073e57e6a8ff904701fcdfbac34b40d3b4f..784ba60c0b4191b86ad2329d7e74c9e5f8708df8 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -28,7 +28,6 @@
(echo "EVA:" %{lib-available:frama-c-eva.core} "\n")
(echo " - ppx_deriving.eq:" %{lib-available:ppx_deriving.eq} "\n")
(echo " - ppx_deriving.ord:" %{lib-available:ppx_deriving.ord} "\n")
- (echo " - Postdominators:" %{lib-available:frama-c-postdominators.core} "\n")
(echo "Numerors:" %{lib-available:frama-c-eva.numerors.core} "\n")
(echo " - MLMPFR:" %{lib-available:mlmpfr} "\n")
(echo "Apron domains:" %{lib-available:frama-c-eva.apron.core} "\n")
@@ -42,7 +41,7 @@
(optional)
(public_name frama-c-eva.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-server.core frama-c-postdominators.core)
+ (libraries frama-c.kernel frama-c-server.core)
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx))
(preprocess (pps ppx_deriving.eq ppx_deriving.ord)))
diff --git a/src/plugins/from/dune b/src/plugins/from/dune
index 1e769f239c2119877b6ab480a5229572e8426863..a47788602948d7a3f7a68e9cee93385fa4d4997b 100644
--- a/src/plugins/from/dune
+++ b/src/plugins/from/dune
@@ -27,7 +27,6 @@
(echo "From:" %{lib-available:frama-c-from.core} "\n")
(echo " - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
(echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
- (echo " - Postdominators:" %{lib-available:frama-c-postdominators.core} "\n")
)
)
)
@@ -37,7 +36,7 @@
(optional)
(public_name frama-c-from.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-callgraph.core frama-c-eva.core frama-c-postdominators.core)
+ (libraries frama-c.kernel frama-c-callgraph.core frama-c-eva.core)
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx))
)
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 14c0cc2acda9f71d51759577d6ebd76f5c95cfd0..9f4f3466bde40fdb604e181c97b2f3857248d5e0 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -477,12 +477,11 @@ struct
(* Eliminate additional variables originating from a control-flow branching
statement closing at [s]. *)
let eliminate_additional s data =
- let kf = Stack.top call_stack in
let map = data.additional_deps_table in
let map' =
ZoneStmtMap.fold
(fun k _v acc_map ->
- if Postdominators.is_postdominator kf ~opening:k ~closing:s
+ if Dominators.postdominates s k
then ZoneStmtMap.remove k acc_map
else acc_map
) map map
diff --git a/src/plugins/gui/help_manager.ml b/src/plugins/gui/help_manager.ml
index d5e9ba63a562c8a370e8128cfb8ccb994b5ad2d9..590c2bdf8a965e5abafb0b43ef65bb2602edc925 100644
--- a/src/plugins/gui/help_manager.ml
+++ b/src/plugins/gui/help_manager.ml
@@ -79,7 +79,7 @@ let show main_ui =
let copyright (* should be automatically generated *) =
"\t © CEA and INRIA for the Frama-C kernel\n\
\t © CEA for the GUI and plug-ins constant propagation, from, inout, impact, \
- metrics, occurrence pdg, postdominators, scope, security_slicing, \
+ metrics, occurrence pdg, scope, security_slicing, \
semantic callgraph, slicing, sparecode, syntactic callgraph, users and value.\n\
\n\
See the particular header of each source file for details."
diff --git a/src/plugins/loop_analysis/region_analysis_stmt.ml b/src/plugins/loop_analysis/region_analysis_stmt.ml
index e5d4380e2d1b8ba9edc628b56f396dabdde8989e..319d8e87659017f3d61890ac710d4575ef5fb547 100644
--- a/src/plugins/loop_analysis/region_analysis_stmt.ml
+++ b/src/plugins/loop_analysis/region_analysis_stmt.ml
@@ -100,6 +100,7 @@ struct
module DomTree = struct
let dominates = Dominators.dominates
+
let domtree_postfix_iter f =
(* Reverse the normal domtree. *)
diff --git a/src/plugins/postdominators/compute.ml b/src/plugins/postdominators/compute.ml
deleted file mode 100644
index 412f32507fee6f978b7e4b3feef22125a8d83ced..0000000000000000000000000000000000000000
--- a/src/plugins/postdominators/compute.ml
+++ /dev/null
@@ -1,228 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-open Cil_datatype
-
-include
- Plugin.Register
- (struct
- let name = "dominators"
- let shortname = "dominators"
- let help = "Compute postdominators of statements"
- end)
-
-module DomSet = struct
-
- type domset = Value of Stmt.Hptset.t | Top
-
- let inter a b = match a,b with
- | Top,Top -> Top
- | Value v, Top | Top, Value v -> Value v
- | Value v, Value v' -> Value (Stmt.Hptset.inter v v')
-
- let add v d = match d with
- | Top -> Top
- | Value d -> Value (Stmt.Hptset.add v d)
-
- let mem v = function
- | Top -> true
- | Value d -> Stmt.Hptset.mem v d
-
- let map f = function
- | Top -> Top
- | Value set -> Value (f set)
-
- include Datatype.Make
- (struct
- include Datatype.Serializable_undefined
- type t = domset
- let name = "dominator_set"
- let reprs = Top :: List.map (fun s -> Value s) Stmt.Hptset.reprs
- let structural_descr =
- Structural_descr.t_sum [| [| Stmt.Hptset.packed_descr |] |]
- let pretty fmt = function
- | Top -> Format.fprintf fmt "Top"
- | Value d ->
- Pretty_utils.pp_iter ~pre:"@[{" ~sep:",@," ~suf:"}@]"
- Stmt.Hptset.iter
- (fun fmt s -> Format.fprintf fmt "%d" s.sid)
- fmt d
- let equal a b = match a,b with
- | Top,Top -> true
- | Value _v, Top | Top, Value _v -> false
- | Value v, Value v' -> Stmt.Hptset.equal v v'
- let copy = map Cil_datatype.Stmt.Hptset.copy
- let mem_project = Datatype.never_any_project
- end)
-
-end
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-
-exception Top
-
-module type MakePostDomArg = sig
- val is_accessible: stmt -> bool
- (* Evaluation of an expression which is supposed to be the condition of an
- 'if'. The first boolean (resp. second) represents the possibility that
- the expression can be non-zero (resp. zero), ie. true (resp. false). *)
- val eval_cond: stmt -> exp -> bool * bool
-
- val dependencies: State.t list
- val name: string
-end
-
-module MakePostDom(X: MakePostDomArg) =
-struct
-
- module PostDom =
- Cil_state_builder.Stmt_hashtbl
- (DomSet)
- (struct
- let name = "postdominator." ^ X.name
- let dependencies = Ast.self :: X.dependencies
- let size = 503
- end)
-
- module PostComputer = struct
-
- let name = "postdominator"
- let debug = false
-
- type t = DomSet.t
- module StmtStartData = PostDom
-
- let pretty = DomSet.pretty
-
- let combineStmtStartData _stmt ~old new_ =
- if DomSet.equal old new_ then None else Some new_
-
- let combineSuccessors = DomSet.inter
-
- let doStmt stmt =
- Async.yield ();
- Postdominators_parameters.debug ~level:2 "doStmt: %d" stmt.sid;
- match stmt.skind with
- | Return _ -> Dataflow2.Done (DomSet.Value (Stmt.Hptset.singleton stmt))
- | _ -> Dataflow2.Post (fun data -> DomSet.add stmt data)
-
-
- let doInstr _ _ _ = Dataflow2.Default
-
- (* We make special tests for 'if' statements without a 'then' or
- 'else' branch. It can lead to better precision if we can evaluate
- the condition of the 'if' with always the same truth value *)
- let filterIf ifstmt next = match ifstmt.skind with
- | If (e, { bstmts = sthen :: _ }, { bstmts = [] }, _)
- when not (Stmt.equal sthen next) ->
- (* [next] is the syntactic successor of the 'if', ie the
- 'else' branch. If the condition is never false, then
- [sthen] postdominates [next]. We must not follow the edge
- from [ifstmt] to [next] *)
- snd (X.eval_cond ifstmt e)
-
- | If (e, { bstmts = [] }, { bstmts = selse :: _ }, _)
- when not (Stmt.equal selse next) ->
- (* dual case *)
- fst (X.eval_cond ifstmt e)
-
- | _ -> true
-
- let filterStmt pred next =
- X.is_accessible pred && filterIf pred next
-
-
- let funcExitData = DomSet.Value Stmt.Hptset.empty
-
- end
- module PostCompute = Dataflow2.Backwards(PostComputer)
-
- let compute kf =
- let return =
- try Kernel_function.find_return kf
- with Kernel_function.No_Statement ->
- Postdominators_parameters.abort
- "No return statement for a function with body %a"
- Kernel_function.pretty kf
- in
- try
- let _ = PostDom.find return in
- Postdominators_parameters.feedback ~level:2 "computed for function %a"
- Kernel_function.pretty kf
- with Not_found ->
- Postdominators_parameters.feedback ~level:2 "computing for function %a"
- Kernel_function.pretty kf;
- let f = kf.fundec in
- match f with
- | Definition (f,_) ->
- let stmts = f.sallstmts in
- List.iter (fun s -> PostDom.add s DomSet.Top) stmts;
- PostCompute.compute [return];
- Postdominators_parameters.feedback ~level:2 "done for function %a"
- Kernel_function.pretty kf
- | Declaration _ -> ()
-
- let get_stmt_postdominators f stmt =
- let do_it () = PostDom.find stmt in
- try do_it ()
- with Not_found -> compute f; do_it ()
-
- (** @raise Top when the statement postdominators
- * have not been computed ie neither the return statement is reachable,
- * nor the statement is in a natural loop. *)
- let stmt_postdominators f stmt =
- match get_stmt_postdominators f stmt with
- | DomSet.Value s ->
- Postdominators_parameters.debug ~level:1 "Postdom for %d are %a"
- stmt.sid Stmt.Hptset.pretty s;
- s
- | DomSet.Top -> raise Top
-
- let is_postdominator f ~opening ~closing =
- let open_postdominators = get_stmt_postdominators f opening in
- DomSet.mem closing open_postdominators
-
- let display () =
- let disp_all fmt =
- PostDom.iter
- (fun k v -> Format.fprintf fmt "Stmt:%d -> @[%a@]\n"
- k.sid PostComputer.pretty v)
- in Postdominators_parameters.result "%t" disp_all
-
-end
-
-module PostDomArg = struct
- let is_accessible _ = true
- let dependencies = []
- let name = "basic"
- let eval_cond _ _ = true, true
-end
-
-include MakePostDom (PostDomArg)
-let self = PostDom.self
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/postdominators/compute.mli b/src/plugins/postdominators/compute.mli
deleted file mode 100644
index 748beef0b5befe142b16cc1c5be3914cb17076a3..0000000000000000000000000000000000000000
--- a/src/plugins/postdominators/compute.mli
+++ /dev/null
@@ -1,41 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-
-exception Top
-(** Used for postdominators-related functions, when the
- postdominators of a statement cannot be computed. It means that
- there is no path from this statement to the function return. *)
-
-val compute: kernel_function -> unit
-
-val stmt_postdominators:
- kernel_function -> stmt -> Cil_datatype.Stmt.Hptset.t
-(** @raise Top (see above) *)
-
-val is_postdominator:
- kernel_function -> opening:stmt -> closing:stmt -> bool
-
-val display: unit -> unit
-
-val self: State.t
diff --git a/src/plugins/postdominators/dune b/src/plugins/postdominators/dune
deleted file mode 100644
index 421fca944bc2d73026038f7d29130d72774b1638..0000000000000000000000000000000000000000
--- a/src/plugins/postdominators/dune
+++ /dev/null
@@ -1,42 +0,0 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; ;;
-;; This file is part of Frama-C. ;;
-;; ;;
-;; Copyright (C) 2007-2024 ;;
-;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
-;; alternatives) ;;
-;; ;;
-;; you can redistribute it and/or modify it under the terms of the GNU ;;
-;; Lesser General Public License as published by the Free Software ;;
-;; Foundation, version 2.1. ;;
-;; ;;
-;; It is distributed in the hope that it will be useful, ;;
-;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
-;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
-;; GNU Lesser General Public License for more details. ;;
-;; ;;
-;; See the GNU Lesser General Public License version 2.1 ;;
-;; for more details (enclosed in the file licenses/LGPLv2.1). ;;
-;; ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(rule
- (alias frama-c-configure)
- (deps (universe))
- (action (progn
- (echo "Postdominators:" %{lib-available:frama-c-postdominators.core} "\n")
- )
- )
-)
-
-( library
- (name postdominators)
- (optional)
- (public_name frama-c-postdominators.core)
- (flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel)
- (instrumentation (backend landmarks))
- (instrumentation (backend bisect_ppx))
-)
-
-(plugin (optional) (name postdominators) (libraries frama-c-postdominators.core) (site (frama-c plugins)))
diff --git a/src/plugins/postdominators/dune-project b/src/plugins/postdominators/dune-project
deleted file mode 100644
index 1e31a2576fcd8d1781fb5f0acb3d25170369928a..0000000000000000000000000000000000000000
--- a/src/plugins/postdominators/dune-project
+++ /dev/null
@@ -1,25 +0,0 @@
-(lang dune 3.7)
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; ;;
-;; This file is part of Frama-C. ;;
-;; ;;
-;; Copyright (C) 2007-2024 ;;
-;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
-;; alternatives) ;;
-;; ;;
-;; you can redistribute it and/or modify it under the terms of the GNU ;;
-;; Lesser General Public License as published by the Free Software ;;
-;; Foundation, version 2.1. ;;
-;; ;;
-;; It is distributed in the hope that it will be useful, ;;
-;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
-;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
-;; GNU Lesser General Public License for more details. ;;
-;; ;;
-;; See the GNU Lesser General Public License version 2.1 ;;
-;; for more details (enclosed in the file licenses/LGPLv2.1). ;;
-;; ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(name frama-c-postdominators)
-(using dune_site 0.1)
diff --git a/src/plugins/postdominators/frama-c-postdominators.opam b/src/plugins/postdominators/frama-c-postdominators.opam
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/postdominators/postdominators.ml b/src/plugins/postdominators/postdominators.ml
deleted file mode 100644
index 2ebc1ad9268c9e9928d1672c77fa3a01b8a733f6..0000000000000000000000000000000000000000
--- a/src/plugins/postdominators/postdominators.ml
+++ /dev/null
@@ -1,42 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-include Compute
-
-let print_dot basename kf =
- let filename = basename ^ "." ^ Kernel_function.get_name kf ^ ".dot" in
- Print.build_dot filename kf;
- Postdominators_parameters.result "dot file generated in %s" filename
-
-let output () =
- let dot_postdom = Postdominators_parameters.DotPostdomBasename.get () in
- if dot_postdom <> "" then (
- Ast.compute ();
- Globals.Functions.iter (fun kf ->
- if Kernel_function.is_definition kf then
- print_dot dot_postdom kf)
- )
-
-let output, _ = State_builder.apply_once "Postdominators.Compute.output"
- [Compute.self] output
-
-let () = Boot.Main.extend output
diff --git a/src/plugins/postdominators/postdominators.mli b/src/plugins/postdominators/postdominators.mli
deleted file mode 100644
index a8786b4ba531903728c94deaaeb82595a9eb136a..0000000000000000000000000000000000000000
--- a/src/plugins/postdominators/postdominators.mli
+++ /dev/null
@@ -1,43 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-
-exception Top
-(** Used for postdominators-related functions, when the
- postdominators of a statement cannot be computed. It means that
- there is no path from this statement to the function return. *)
-
-val compute: kernel_function -> unit
-
-val stmt_postdominators:
- kernel_function -> stmt -> Cil_datatype.Stmt.Hptset.t
-(** @raise Top (see above) *)
-
-val is_postdominator:
- kernel_function -> opening:stmt -> closing:stmt -> bool
-
-val display: unit -> unit
-
-val print_dot : string -> kernel_function -> unit
-(** Print a representation of the postdominators in a dot file
- whose name is [basename.function_name.dot]. *)
diff --git a/src/plugins/postdominators/postdominators_parameters.ml b/src/plugins/postdominators/postdominators_parameters.ml
deleted file mode 100644
index 86b00634e808aaa74d8a21b2d9a393674f277b16..0000000000000000000000000000000000000000
--- a/src/plugins/postdominators/postdominators_parameters.ml
+++ /dev/null
@@ -1,42 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-include Plugin.Register
- (struct
- let name = "postdominators"
- let shortname = "postdominators"
- let help = "computing postdominators of statements"
- end)
-
-module DotPostdomBasename =
- Empty_string
- (struct
- let option_name = "-dot-postdom"
- let arg_name = "f"
- let help = "put the postdominators of function <f> in basename.f.dot"
- end)
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/postdominators/postdominators_parameters.mli b/src/plugins/postdominators/postdominators_parameters.mli
deleted file mode 100644
index 4e54382d36affe9be855bd01bb4107ecb88dff61..0000000000000000000000000000000000000000
--- a/src/plugins/postdominators/postdominators_parameters.mli
+++ /dev/null
@@ -1,32 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-include Plugin.General_services
-
-module DotPostdomBasename: Parameter_sig.String
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/postdominators/print.ml b/src/plugins/postdominators/print.ml
deleted file mode 100644
index 40534a9b8b9c1b6411d257dffbab7843f0ca9cd7..0000000000000000000000000000000000000000
--- a/src/plugins/postdominators/print.ml
+++ /dev/null
@@ -1,148 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-open Cil_datatype
-
-let pretty_stmt fmt s = Cil_printer.pp_stmt fmt s
-
-module Printer = struct
-
- type t = string * (Stmt.Hptset.t option Kinstr.Hashtbl.t)
- module V = struct
- type t = Cil_types.stmt * bool
- let pretty fmt v = pretty_stmt fmt v
- end
- module E = struct
- type t = (V.t * V.t)
- let src e = fst e
- let dst e = snd e
- end
-
- let iter_vertex f (_, graph) =
- let do_s ki postdom =
- let s = match ki with Kstmt s -> s | _ -> assert false in
- Postdominators_parameters.debug "iter_vertex %d : %a\n" s.sid V.pretty s;
- let has_postdom = match postdom with None -> false | _ -> true in
- f (s, has_postdom)
- in
- Kinstr.Hashtbl.iter do_s graph
-
- let iter_edges_e f (_, graph) =
- let do_s ki postdom =
- let s = match ki with Kstmt s -> s | _ -> assert false in
- match postdom with None -> ()
- | Some postdom ->
- let do_edge p = f ((s, true), (p, true)) in
- Stmt.Hptset.iter do_edge postdom
- in
- Kinstr.Hashtbl.iter do_s graph
-
-
- let vertex_name (s, _) = string_of_int s.sid
-
- let graph_attributes (title, _) = [`Label title]
-
- let default_vertex_attributes _g = [`Style `Filled]
- let default_edge_attributes _g = []
-
- let vertex_attributes (s, has_postdom) =
- let attrib = [] in
- let txt = Format.asprintf "%a" V.pretty s in
- let attrib = (`Label txt) :: attrib in
- let color = if has_postdom then 0x7FFFD4 else 0xFF0000 in
- let attrib = (`Shape `Box) :: attrib in
- let attrib = (`Fillcolor color) :: attrib in
- attrib
-
- let edge_attributes _s = []
-
- let get_subgraph _v = None
-end
-
-module PostdomGraph = Graph.Graphviz.Dot(Printer)
-
-let get_postdom kf graph s =
- try
- match Kinstr.Hashtbl.find graph (Kstmt s) with
- | None -> Stmt.Hptset.empty
- | Some l -> l
- with Not_found ->
- try
- let postdom = Compute.stmt_postdominators kf s in
- let postdom = Stmt.Hptset.remove s postdom in
- Postdominators_parameters.debug "postdom for %d:%a = %a\n"
- s.sid pretty_stmt s Stmt.Hptset.pretty postdom;
- Kinstr.Hashtbl.add graph (Kstmt s) (Some postdom); postdom
- with Compute.Top ->
- Kinstr.Hashtbl.add graph (Kstmt s) None;
- raise Compute.Top
-
-(** [s_postdom] are [s] postdominators, including [s].
- * We don't have to represent the relation between s and s.
- * And because the postdom relation is transitive, if [p] is in [s_postdom],
- * we can remove [p_postdom] from [s_postdom] in order to have a clearer graph.
-*)
-let reduce kf graph s =
- let remove p s_postdom =
- if Stmt.Hptset.mem p s_postdom
- then
- try
- let p_postdom = get_postdom kf graph p in
- let s_postdom = Stmt.Hptset.diff s_postdom p_postdom
- in s_postdom
- with Compute.Top -> assert false
- (* p postdom s -> cannot be top *)
- else s_postdom (* p has already been removed from s_postdom *)
- in
- try
- let postdom = get_postdom kf graph s in
- let postdom = Stmt.Hptset.fold remove postdom postdom in
- Postdominators_parameters.debug "new postdom for %d:%a = %a\n"
- s.sid pretty_stmt s Stmt.Hptset.pretty postdom;
- Kinstr.Hashtbl.replace graph (Kstmt s) (Some postdom)
- with Compute.Top ->
- ()
-
-let build_reduced_graph kf graph stmts =
- List.iter (reduce kf graph) stmts
-
-let build_dot filename kf =
- match kf.fundec with
- | Definition (fct, _) ->
- let stmts = fct.sallstmts in
- let graph = Kinstr.Hashtbl.create (List.length stmts) in
- let _ = build_reduced_graph kf graph stmts in
- let name = Kernel_function.get_name kf in
- let title = "Postdominators for function " ^ name in
- let file = open_out filename in
- PostdomGraph.output_graph file (title, graph);
- close_out file
- | Declaration _ ->
- Kernel.error "cannot compute for a function without body %a"
- Kernel_function.pretty kf
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/postdominators/print.mli b/src/plugins/postdominators/print.mli
deleted file mode 100644
index 95ea33441d9327a25a8634300dd49225e542b2dd..0000000000000000000000000000000000000000
--- a/src/plugins/postdominators/print.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-val build_dot: string -> Kernel_function.t -> unit
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index a65f14d60462aaa3428c9e69e27e3fbd6405af58..9715cdf49f62fe2e22101b3b8a2bc110260a59d1 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -537,8 +537,7 @@ let get_prop_scope_at_stmt ~warn kf stmt ?(proven=CA_Map.empty) annot =
end;
let add ((acc_scope, acc_to_be_rm) as acc) s = match pre_state s with
| State.SameVal ->
- if Dominators.dominates stmt s && not (Cil_datatype.Stmt.equal stmt s)
- then
+ if Dominators.strictly_dominates stmt s then
let acc_scope = add_s s acc_scope in
let acc_to_be_rm = check_stmt_annots (annot, stmt) s acc_to_be_rm in
(acc_scope, acc_to_be_rm)
diff --git a/tests/misc/oracle/dom_graph.f.dot b/tests/misc/oracle/dom_graph.f.dot
new file mode 100644
index 0000000000000000000000000000000000000000..ca126d8e69606de83dd763955586838d1244081d
--- /dev/null
+++ b/tests/misc/oracle/dom_graph.f.dot
@@ -0,0 +1,56 @@
+digraph G {
+ label="Dominators for function f";
+ node [shape=box, style="filled", ];
+ 1 [label="/* sid:1 */
+c = 12;", ];
+ 3 [label="/* sid:3 */
+if (c) {
+ /* sid:4 */
+ test: c = 42;
+ /* sid:5 */
+ goto test;
+}
+else {
+ /* sid:6 */
+ c = 12;
+ /* sid:53 */
+ {
+ /* sid:8 */
+ __retres = c;
+ /* sid:54 */
+ goto return_label;
+ }
+}",
+ ];
+ 4 [label="/* sid:4 */
+test: c = 42;", ];
+ 53 [label="/* sid:53 */
+{
+ /* sid:8 */
+ __retres = c;
+ /* sid:54 */
+ goto return_label;
+}",
+ ];
+ 5 [label="/* sid:5 */
+goto test;", ];
+ 54 [label="/* sid:54 */
+goto return_label;", ];
+ 6 [label="/* sid:6 */
+c = 12;", ];
+ 55 [label="/* sid:55 */
+return_label: return __retres;", ];
+ 8 [label="/* sid:8 */
+__retres = c;", ];
+
+
+ 1 -> 3;
+ 3 -> 4;
+ 6 -> 53;
+ 4 -> 5;
+ 8 -> 54;
+ 3 -> 6;
+ 54 -> 55;
+ 53 -> 8;
+
+ }
diff --git a/tests/misc/oracle/dom_graph.g.dot b/tests/misc/oracle/dom_graph.g.dot
new file mode 100644
index 0000000000000000000000000000000000000000..8d9ff3a679f7c9177486a7097ff2c4094561cfdd
--- /dev/null
+++ b/tests/misc/oracle/dom_graph.g.dot
@@ -0,0 +1,63 @@
+digraph G {
+ label="Dominators for function g";
+ node [shape=box, style="filled", ];
+ 16 [label="/* sid:16 */
+c = 12;", ];
+ 18 [label="/* sid:18 */
+__retres = c;", ];
+ 20 [label="/* sid:20 */
+__retres = c;", ];
+ 57 [label="/* sid:57 */
+{
+ /* sid:18 */
+ __retres = c;
+ /* sid:58 */
+ goto return_label;
+}",
+ ];
+ 58 [label="/* sid:58 */
+goto return_label;", ];
+ 10 [label="/* sid:10 */
+c = 12;", ];
+ 59 [label="/* sid:59 */
+return_label: return __retres;", ];
+ 12 [label="/* sid:12 */
+if (c) {
+ /* sid:13 */
+ goto test;
+ /* sid:14 */
+ c += 1;
+ /* sid:15 */
+ test: c = 42;
+}
+else {
+ /* sid:16 */
+ c = 12;
+ /* sid:57 */
+ {
+ /* sid:18 */
+ __retres = c;
+ /* sid:58 */
+ goto return_label;
+ }
+}",
+ ];
+ 13 [label="/* sid:13 */
+goto test;", ];
+ 14 [label="/* sid:14 */
+c += 1;", ];
+ 15 [label="/* sid:15 */
+test: c = 42;", ];
+
+
+ 12 -> 16;
+ 57 -> 18;
+ 15 -> 20;
+ 16 -> 57;
+ 18 -> 58;
+ 12 -> 59;
+ 10 -> 12;
+ 12 -> 13;
+ 13 -> 15;
+
+ }
diff --git a/tests/misc/oracle/dom_graph.h.dot b/tests/misc/oracle/dom_graph.h.dot
new file mode 100644
index 0000000000000000000000000000000000000000..2826acff315de2ec5020301ef387f3faa4f016dd
--- /dev/null
+++ b/tests/misc/oracle/dom_graph.h.dot
@@ -0,0 +1,113 @@
+digraph G {
+ label="Dominators for function h";
+ node [shape=box, style="filled", ];
+ 33 [label="/* sid:33 */
+j += 1;", ];
+ 34 [label="/* sid:34 */
+stop();", ];
+ 36 [label="/* sid:36 */
+return x;", ];
+ 22 [label="/* sid:22 */
+{
+ /* sid:23 */
+ int j = 0;
+ /* sid:24 */
+ while (1) {
+ /* sid:26 */
+ if (j < 10) {
+
+ }
+ else {
+ /* sid:27 */
+ break;
+ }
+ /* sid:28 */
+ {
+ /* sid:30 */
+ if (j % 2 == 0) {
+ /* sid:31 */
+ x += 1;
+ }
+ else {
+
+ }
+ }
+ /* sid:33 */
+ j += 1;
+ }
+}",
+ ];
+ 23 [label="/* sid:23 */
+int j = 0;", ];
+ 24 [label="/* sid:24 */
+while (1) {
+ /* sid:26 */
+ if (j < 10) {
+
+ }
+ else {
+ /* sid:27 */
+ break;
+ }
+ /* sid:28 */
+ {
+ /* sid:30 */
+ if (j % 2 == 0) {
+ /* sid:31 */
+ x += 1;
+ }
+ else {
+
+ }
+ }
+ /* sid:33 */
+ j += 1;
+}",
+ ];
+ 26 [label="/* sid:26 */
+if (j < 10) {
+
+}
+else {
+ /* sid:27 */
+ break;
+}",
+ ];
+ 27 [label="/* sid:27 */
+break;", ];
+ 28 [label="/* sid:28 */
+{
+ /* sid:30 */
+ if (j % 2 == 0) {
+ /* sid:31 */
+ x += 1;
+ }
+ else {
+
+ }
+}",
+ ];
+ 30 [label="/* sid:30 */
+if (j % 2 == 0) {
+ /* sid:31 */
+ x += 1;
+}
+else {
+
+}",
+ ];
+ 31 [label="/* sid:31 */
+x += 1;", ];
+
+
+ 30 -> 33;
+ 27 -> 34;
+ 22 -> 23;
+ 23 -> 24;
+ 24 -> 26;
+ 26 -> 27;
+ 26 -> 28;
+ 28 -> 30;
+ 30 -> 31;
+
+ }
diff --git a/tests/misc/oracle/dom_graph.i.dot b/tests/misc/oracle/dom_graph.i.dot
new file mode 100644
index 0000000000000000000000000000000000000000..9a4bece54956587ce9dae0bd4f0b35284a442c10
--- /dev/null
+++ b/tests/misc/oracle/dom_graph.i.dot
@@ -0,0 +1,76 @@
+digraph G {
+ label="Dominators for function i";
+ node [shape=box, style="filled", ];
+ 48 [label="/* sid:48 */
+{
+ /* sid:49 */
+ x += 1;
+ /* sid:50 */
+ loop: ;
+}",
+ ];
+ 49 [label="/* sid:49 */
+x += 1;", ];
+ 50 [label="/* sid:50 */
+loop: ;", ];
+ 38 [label="/* sid:38 */
+int x = 0;", ];
+ 40 [label="/* sid:40 */
+if (nondet) {
+ /* sid:41 */
+ goto loop;
+}
+else {
+
+}",
+ ];
+ 41 [label="/* sid:41 */
+goto loop;", ];
+ 43 [label="/* sid:43 */
+x = 1;", ];
+ 44 [label="/* sid:44 */
+while (1) {
+ /* sid:46 */
+ if (x < 10) {
+
+ }
+ else {
+ /* sid:47 */
+ break;
+ }
+ /* sid:48 */
+ {
+ /* sid:49 */
+ x += 1;
+ /* sid:50 */
+ loop: ;
+ }
+}",
+ ];
+ 62 [label="/* sid:62 */
+return;", ];
+ 46 [label="/* sid:46 */
+if (x < 10) {
+
+}
+else {
+ /* sid:47 */
+ break;
+}",
+ ];
+ 47 [label="/* sid:47 */
+break;", ];
+
+
+ 46 -> 48;
+ 48 -> 49;
+ 40 -> 50;
+ 38 -> 40;
+ 40 -> 41;
+ 40 -> 43;
+ 40 -> 44;
+ 47 -> 62;
+ 44 -> 46;
+ 46 -> 47;
+
+ }
diff --git a/tests/misc/oracle/postdom_graph.f.dot b/tests/misc/oracle/postdom_graph.f.dot
new file mode 100644
index 0000000000000000000000000000000000000000..07312345443505555321d09c6d7bca939a2c46b6
--- /dev/null
+++ b/tests/misc/oracle/postdom_graph.f.dot
@@ -0,0 +1,54 @@
+digraph G {
+ label="PostDominators for function f";
+ node [shape=box, style="filled", ];
+ 1 [label="/* sid:1 */
+c = 12;", ];
+ 3 [label="/* sid:3 */
+if (c) {
+ /* sid:4 */
+ test: c = 42;
+ /* sid:5 */
+ goto test;
+}
+else {
+ /* sid:6 */
+ c = 12;
+ /* sid:53 */
+ {
+ /* sid:8 */
+ __retres = c;
+ /* sid:54 */
+ goto return_label;
+ }
+}",
+ ];
+ 4 [label="/* sid:4 */
+test: c = 42;", ];
+ 53 [label="/* sid:53 */
+{
+ /* sid:8 */
+ __retres = c;
+ /* sid:54 */
+ goto return_label;
+}",
+ ];
+ 5 [label="/* sid:5 */
+goto test;", ];
+ 54 [label="/* sid:54 */
+goto return_label;", ];
+ 6 [label="/* sid:6 */
+c = 12;", ];
+ 55 [label="/* sid:55 */
+return_label: return __retres;", ];
+ 8 [label="/* sid:8 */
+__retres = c;", ];
+
+
+ 3 -> 1;
+ 6 -> 3;
+ 8 -> 53;
+ 55 -> 54;
+ 53 -> 6;
+ 54 -> 8;
+
+ }
diff --git a/tests/misc/oracle/postdom_graph.g.dot b/tests/misc/oracle/postdom_graph.g.dot
new file mode 100644
index 0000000000000000000000000000000000000000..b67c6c4a95ef21b02083a75cc6de251f36b93280
--- /dev/null
+++ b/tests/misc/oracle/postdom_graph.g.dot
@@ -0,0 +1,64 @@
+digraph G {
+ label="PostDominators for function g";
+ node [shape=box, style="filled", ];
+ 16 [label="/* sid:16 */
+c = 12;", ];
+ 18 [label="/* sid:18 */
+__retres = c;", ];
+ 20 [label="/* sid:20 */
+__retres = c;", ];
+ 57 [label="/* sid:57 */
+{
+ /* sid:18 */
+ __retres = c;
+ /* sid:58 */
+ goto return_label;
+}",
+ ];
+ 58 [label="/* sid:58 */
+goto return_label;", ];
+ 10 [label="/* sid:10 */
+c = 12;", ];
+ 59 [label="/* sid:59 */
+return_label: return __retres;", ];
+ 12 [label="/* sid:12 */
+if (c) {
+ /* sid:13 */
+ goto test;
+ /* sid:14 */
+ c += 1;
+ /* sid:15 */
+ test: c = 42;
+}
+else {
+ /* sid:16 */
+ c = 12;
+ /* sid:57 */
+ {
+ /* sid:18 */
+ __retres = c;
+ /* sid:58 */
+ goto return_label;
+ }
+}",
+ ];
+ 13 [label="/* sid:13 */
+goto test;", ];
+ 14 [label="/* sid:14 */
+c += 1;", ];
+ 15 [label="/* sid:15 */
+test: c = 42;", ];
+
+
+ 57 -> 16;
+ 58 -> 18;
+ 59 -> 20;
+ 18 -> 57;
+ 59 -> 58;
+ 12 -> 10;
+ 59 -> 12;
+ 15 -> 13;
+ 15 -> 14;
+ 20 -> 15;
+
+ }
diff --git a/tests/misc/oracle/postdom_graph.h.dot b/tests/misc/oracle/postdom_graph.h.dot
new file mode 100644
index 0000000000000000000000000000000000000000..0335859b42222119a397f5b135f16a7000b958d4
--- /dev/null
+++ b/tests/misc/oracle/postdom_graph.h.dot
@@ -0,0 +1,104 @@
+digraph G {
+ label="PostDominators for function h";
+ node [shape=box, style="filled", ];
+ 33 [label="/* sid:33 */
+j += 1;", ];
+ 34 [label="/* sid:34 */
+stop();", ];
+ 36 [label="/* sid:36 */
+return x;", ];
+ 22 [label="/* sid:22 */
+{
+ /* sid:23 */
+ int j = 0;
+ /* sid:24 */
+ while (1) {
+ /* sid:26 */
+ if (j < 10) {
+
+ }
+ else {
+ /* sid:27 */
+ break;
+ }
+ /* sid:28 */
+ {
+ /* sid:30 */
+ if (j % 2 == 0) {
+ /* sid:31 */
+ x += 1;
+ }
+ else {
+
+ }
+ }
+ /* sid:33 */
+ j += 1;
+ }
+}",
+ ];
+ 23 [label="/* sid:23 */
+int j = 0;", ];
+ 24 [label="/* sid:24 */
+while (1) {
+ /* sid:26 */
+ if (j < 10) {
+
+ }
+ else {
+ /* sid:27 */
+ break;
+ }
+ /* sid:28 */
+ {
+ /* sid:30 */
+ if (j % 2 == 0) {
+ /* sid:31 */
+ x += 1;
+ }
+ else {
+
+ }
+ }
+ /* sid:33 */
+ j += 1;
+}",
+ ];
+ 26 [label="/* sid:26 */
+if (j < 10) {
+
+}
+else {
+ /* sid:27 */
+ break;
+}",
+ ];
+ 27 [label="/* sid:27 */
+break;", ];
+ 28 [label="/* sid:28 */
+{
+ /* sid:30 */
+ if (j % 2 == 0) {
+ /* sid:31 */
+ x += 1;
+ }
+ else {
+
+ }
+}",
+ ];
+ 30 [label="/* sid:30 */
+if (j % 2 == 0) {
+ /* sid:31 */
+ x += 1;
+}
+else {
+
+}",
+ ];
+ 31 [label="/* sid:31 */
+x += 1;", ];
+
+
+
+ }
diff --git a/tests/misc/oracle/postdom_graph.i.dot b/tests/misc/oracle/postdom_graph.i.dot
new file mode 100644
index 0000000000000000000000000000000000000000..64c9cb923c32876d2623b6c6f46fb35effa107a6
--- /dev/null
+++ b/tests/misc/oracle/postdom_graph.i.dot
@@ -0,0 +1,76 @@
+digraph G {
+ label="PostDominators for function i";
+ node [shape=box, style="filled", ];
+ 48 [label="/* sid:48 */
+{
+ /* sid:49 */
+ x += 1;
+ /* sid:50 */
+ loop: ;
+}",
+ ];
+ 49 [label="/* sid:49 */
+x += 1;", ];
+ 50 [label="/* sid:50 */
+loop: ;", ];
+ 38 [label="/* sid:38 */
+int x = 0;", ];
+ 40 [label="/* sid:40 */
+if (nondet) {
+ /* sid:41 */
+ goto loop;
+}
+else {
+
+}",
+ ];
+ 41 [label="/* sid:41 */
+goto loop;", ];
+ 43 [label="/* sid:43 */
+x = 1;", ];
+ 44 [label="/* sid:44 */
+while (1) {
+ /* sid:46 */
+ if (x < 10) {
+
+ }
+ else {
+ /* sid:47 */
+ break;
+ }
+ /* sid:48 */
+ {
+ /* sid:49 */
+ x += 1;
+ /* sid:50 */
+ loop: ;
+ }
+}",
+ ];
+ 62 [label="/* sid:62 */
+return;", ];
+ 46 [label="/* sid:46 */
+if (x < 10) {
+
+}
+else {
+ /* sid:47 */
+ break;
+}",
+ ];
+ 47 [label="/* sid:47 */
+break;", ];
+
+
+ 49 -> 48;
+ 50 -> 49;
+ 44 -> 50;
+ 40 -> 38;
+ 44 -> 40;
+ 50 -> 41;
+ 44 -> 43;
+ 46 -> 44;
+ 47 -> 46;
+ 62 -> 47;
+
+ }
diff --git a/tests/misc/oracle/test_dominators.res.oracle b/tests/misc/oracle/test_dominators.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..76bebfc2cd6a1a86e8b1efd075dcf962409ffdde
--- /dev/null
+++ b/tests/misc/oracle/test_dominators.res.oracle
@@ -0,0 +1,257 @@
+[kernel] Parsing test_dominators.c (with preprocessing)
+
+Computing for function f:
+{
+ int __retres;
+ /* sid:1 */
+ c = 12;
+ /* sid:3 */
+ if (c) {
+ /* sid:4 */
+ test: c = 42;
+ /* sid:5 */
+ goto test;
+ }
+ else {
+ /* sid:6 */
+ c = 12;
+ /* sid:53 */
+ {
+ /* sid:8 */
+ __retres = c;
+ /* sid:54 */
+ goto return_label;
+ }
+ }
+ /* sid:55 */
+ return_label: return __retres;
+}
+[kernel] Dominators: dot file generated in dom_graph.f.dot for function f
+[kernel] PostDominators: dot file generated in postdom_graph.f.dot for function f
+Immediate dominators of f (sid, idom, ipostdom):
+ (1, none, 3), (3, 1, 6), (4, 3, none), (5, 4, none), (6, 3, 53),
+ (53, 6, 8), (8, 53, 54), (54, 8, 55), (55, 54, none)
+
+Computing for function g:
+{
+ int __retres;
+ /* sid:10 */
+ c = 12;
+ /* sid:12 */
+ if (c) {
+ /* sid:13 */
+ goto test;
+ /* sid:14 */
+ c += 1;
+ /* sid:15 */
+ test: c = 42;
+ }
+ else {
+ /* sid:16 */
+ c = 12;
+ /* sid:57 */
+ {
+ /* sid:18 */
+ __retres = c;
+ /* sid:58 */
+ goto return_label;
+ }
+ }
+ /* sid:20 */
+ __retres = c;
+ /* sid:59 */
+ return_label: return __retres;
+}
+[kernel] Dominators: dot file generated in dom_graph.g.dot for function g
+[kernel] PostDominators: dot file generated in postdom_graph.g.dot for function g
+Immediate dominators of g (sid, idom, ipostdom):
+ (10, none, 12), (12, 10, 59), (13, 12, 15), (14, none, 15), (15, 13, 20),
+ (16, 12, 57), (57, 16, 18), (18, 57, 58), (58, 18, 59), (20, 15, 59),
+ (59, 12, none)
+
+Computing for function h:
+{
+ /* sid:22 */
+ {
+ /* sid:23 */
+ int j = 0;
+ /* sid:24 */
+ while (1) {
+ /* sid:26 */
+ if (j < 10) {
+
+ }
+ else {
+ /* sid:27 */
+ break;
+ }
+ /* sid:28 */
+ {
+ /* sid:30 */
+ if (j % 2 == 0) {
+ /* sid:31 */
+ x += 1;
+ }
+ else {
+
+ }
+ }
+ /* sid:33 */
+ j += 1;
+ }
+ }
+ /* sid:34 */
+ stop();
+ /* sid:36 */
+ return x;
+}
+[kernel] Dominators: dot file generated in dom_graph.h.dot for function h
+[kernel] PostDominators: dot file generated in postdom_graph.h.dot for function h
+Immediate dominators of h (sid, idom, ipostdom):
+ (22, none, none), (23, 22, none), (24, 23, none), (26, 24, none),
+ (27, 26, none), (28, 26, none), (30, 28, none), (31, 30, none),
+ (33, 30, none), (34, 27, none), (36, none, none)
+
+Computing for function i:
+{
+ /* sid:38 */
+ int x = 0;
+ /* sid:40 */
+ if (nondet) {
+ /* sid:41 */
+ goto loop;
+ }
+ else {
+
+ }
+ /* sid:43 */
+ x = 1;
+ /* sid:44 */
+ while (1) {
+ /* sid:46 */
+ if (x < 10) {
+
+ }
+ else {
+ /* sid:47 */
+ break;
+ }
+ /* sid:48 */
+ {
+ /* sid:49 */
+ x += 1;
+ /* sid:50 */
+ loop: ;
+ }
+ }
+ /* sid:62 */
+ return;
+}
+[kernel] Dominators: dot file generated in dom_graph.i.dot for function i
+[kernel] PostDominators: dot file generated in postdom_graph.i.dot for function i
+Immediate dominators of i (sid, idom, ipostdom):
+ (38, none, 40), (40, 38, 44), (41, 40, 50), (43, 40, 44), (44, 40, 46),
+ (46, 44, 47), (47, 46, 62), (48, 46, 49), (49, 48, 50), (50, 40, 44),
+ (62, 47, none)
+
+Dominators analysis:
+ Stmt:1 -> {1}
+ Stmt:3 -> {1,3}
+ Stmt:4 -> {1,3,4}
+ Stmt:5 -> {1,3,4,5}
+ Stmt:6 -> {1,3,6}
+ Stmt:8 -> {1,3,6,8,53}
+ Stmt:10 -> {10}
+ Stmt:12 -> {10,12}
+ Stmt:13 -> {10,12,13}
+ Stmt:14 -> {}
+ Stmt:15 -> {10,12,13,15}
+ Stmt:16 -> {10,12,16}
+ Stmt:18 -> {10,12,16,18,57}
+ Stmt:20 -> {10,12,13,15,20}
+ Stmt:22 -> {22}
+ Stmt:23 -> {22,23}
+ Stmt:24 -> {22,23,24}
+ Stmt:26 -> {22,23,24,26}
+ Stmt:27 -> {22,23,24,26,27}
+ Stmt:28 -> {22,23,24,26,28}
+ Stmt:30 -> {22,23,24,26,28,30}
+ Stmt:31 -> {22,23,24,26,28,30,31}
+ Stmt:33 -> {22,23,24,26,28,30,33}
+ Stmt:34 -> {22,23,24,26,27,34}
+ Stmt:36 -> {}
+ Stmt:38 -> {38}
+ Stmt:40 -> {38,40}
+ Stmt:41 -> {38,40,41}
+ Stmt:43 -> {38,40,43}
+ Stmt:44 -> {38,40,44}
+ Stmt:46 -> {38,40,44,46}
+ Stmt:47 -> {38,40,44,46,47}
+ Stmt:48 -> {38,40,44,46,48}
+ Stmt:49 -> {38,40,44,46,48,49}
+ Stmt:50 -> {38,40,50}
+ Stmt:53 -> {1,3,6,53}
+ Stmt:54 -> {1,3,6,8,53,54}
+ Stmt:55 -> {1,3,6,8,53,54,55}
+ Stmt:57 -> {10,12,16,57}
+ Stmt:58 -> {10,12,16,18,57,58}
+ Stmt:59 -> {10,12,59}
+ Stmt:62 -> {38,40,44,46,47,62}
+
+Postominators analysis:
+ Stmt:1 -> {1,3,6,8,53,54,55}
+ Stmt:3 -> {3,6,8,53,54,55}
+ Stmt:4 -> {}
+ Stmt:5 -> {}
+ Stmt:6 -> {6,8,53,54,55}
+ Stmt:8 -> {8,54,55}
+ Stmt:10 -> {10,12,59}
+ Stmt:12 -> {12,59}
+ Stmt:13 -> {13,15,20,59}
+ Stmt:14 -> {14,15,20,59}
+ Stmt:15 -> {15,20,59}
+ Stmt:16 -> {16,18,57,58,59}
+ Stmt:18 -> {18,58,59}
+ Stmt:20 -> {20,59}
+ Stmt:22 -> {}
+ Stmt:23 -> {}
+ Stmt:24 -> {}
+ Stmt:26 -> {}
+ Stmt:27 -> {}
+ Stmt:28 -> {}
+ Stmt:30 -> {}
+ Stmt:31 -> {}
+ Stmt:33 -> {}
+ Stmt:34 -> {}
+ Stmt:36 -> {36}
+ Stmt:38 -> {38,40,44,46,47,62}
+ Stmt:40 -> {40,44,46,47,62}
+ Stmt:41 -> {41,44,46,47,50,62}
+ Stmt:43 -> {43,44,46,47,62}
+ Stmt:44 -> {44,46,47,62}
+ Stmt:46 -> {46,47,62}
+ Stmt:47 -> {47,62}
+ Stmt:48 -> {44,46,47,48,49,50,62}
+ Stmt:49 -> {44,46,47,49,50,62}
+ Stmt:50 -> {44,46,47,50,62}
+ Stmt:53 -> {8,53,54,55}
+ Stmt:54 -> {54,55}
+ Stmt:55 -> {55}
+ Stmt:57 -> {18,57,58,59}
+ Stmt:58 -> {58,59}
+ Stmt:59 -> {59}
+ Stmt:62 -> {62}
+
+Invalidate tables, which should now be empty
+
+Dominators analysis:
+ Empty
+
+Postominators analysis:
+ Empty
+
+Trigger some errors/warnings :
+[kernel] Failure: Statement -1 is not part of a function
+[kernel] Warning: No statement in function stop: Dominators analysis cannot be done
+[kernel] Warning: No statement in function stop: PostDominators analysis cannot be done
+[kernel] Warning: cannot compute Dominators for function stop without body
diff --git a/tests/misc/test_dominators.c b/tests/misc/test_dominators.c
new file mode 100644
index 0000000000000000000000000000000000000000..a461d101dce754b2061bc83fdf2bddc1a137e38f
--- /dev/null
+++ b/tests/misc/test_dominators.c
@@ -0,0 +1,54 @@
+/* run.config
+ MODULE: @PTEST_NAME@
+ LOG: postdom_graph.f.dot dom_graph.f.dot
+ LOG: postdom_graph.g.dot dom_graph.g.dot
+ LOG: postdom_graph.h.dot dom_graph.h.dot
+ LOG: postdom_graph.i.dot dom_graph.i.dot
+ OPT: -kernel-msg-key printer:sid -print-as-is
+*/
+
+void stop(void) __attribute__ ((noreturn)) ;
+
+int f (int c){
+ c = 12;
+ if (c) {
+ test: c = 42;
+ goto test;
+ }
+ else {
+ c = 12;
+ return c;
+ }
+}
+
+int g (int c){
+ c = 12;
+ if (c) {
+ goto test;
+ c++;
+ test: c = 42;
+ }
+ else {
+ c = 12;
+ return c;
+ }
+ return c;
+}
+
+int h(int x){
+ for (int j = 0; j < 10; j++){
+ if (j % 2 == 0) x++;
+ }
+ stop();
+ return x;
+}
+
+void i (int nondet) {
+ int x = 0;
+ if (nondet) goto loop;
+ x = 1;
+ while (x < 10) {
+ x++;
+ loop: ;
+ }
+}
diff --git a/tests/misc/test_dominators.ml b/tests/misc/test_dominators.ml
new file mode 100644
index 0000000000000000000000000000000000000000..eb26706d80b6a8578ae0d7e1d740e336c4250e21
--- /dev/null
+++ b/tests/misc/test_dominators.ml
@@ -0,0 +1,135 @@
+open Cil_types
+
+module StmtSet = Cil_datatype.Stmt.Hptset
+
+let get = function
+ | None -> "none"
+ | Some stmt -> string_of_int stmt.sid
+
+let pp_res =
+ Pretty_utils.pp_list ~pre:"(" ~sep:", " ~suf:")" Format.pp_print_string
+
+(** For each statement of [f], find its immediate dominator and postdominator
+ and print the triplets. *)
+let print_immediate f =
+ let res =
+ List.map (fun s ->
+ let dom = Dominators.get_idom s in
+ let postdom = Dominators.get_ipostdom s in
+ [string_of_int s.sid; get dom; get postdom]
+ ) f.sallstmts
+ in
+ Format.printf "@[<v2>Immediate dominators of %s (sid, idom, ipostdom):@;%a@]@;"
+ f.svar.vname
+ (Pretty_utils.pp_list ~pre:"@[" ~sep:",@ " ~suf:"@]" pp_res) res
+
+(* Make sure that the difference between (post)dominators and strict
+ (post)dominators of a statement [s] is equal to the singleton [s]. *)
+let test_strict f =
+ let test s dom strict_dom =
+ if StmtSet.is_empty dom
+ then assert (StmtSet.is_empty strict_dom)
+ else assert (StmtSet.diff dom strict_dom == StmtSet.singleton s)
+ in
+ List.iter (fun s ->
+ let dom = Dominators.get_dominators s in
+ let sdom = Dominators.get_strict_dominators s in
+ let postdom = Dominators.get_postdominators s in
+ let spostdom = Dominators.get_strict_postdominators s in
+ test s dom sdom;
+ test s postdom spostdom;
+ assert (Dominators.strictly_dominates s s = false);
+ assert (Dominators.strictly_postdominates s s = false)
+ ) f.sallstmts
+
+let test_nearest kf f =
+ (* Simple test for empty list coverage of nearest function. *)
+ assert (Dominators.nearest_common_ancestor [] = None);
+ assert (Dominators.nearest_common_child [] = None);
+
+ (* Since first and last statement do not have an ancestor/child,
+ common nearest for all statements should be empty. *)
+ assert (Dominators.nearest_common_ancestor f.sallstmts = None);
+ assert (Dominators.nearest_common_child f.sallstmts = None);
+
+ if List.length f.sallstmts > 1 then begin
+
+ let first = Kernel_function.find_first_stmt kf in
+ let last = Kernel_function.find_return kf in
+ let all_but_first = List.filter (fun s -> s != first) f.sallstmts in
+ let all_but_last = List.filter (fun s -> s != last) f.sallstmts in
+
+ (* Test that all statements (except the first one) have as common ancestor
+ the first statement of f, unless one of them is unreachable. *)
+ begin match Dominators.nearest_common_ancestor all_but_first with
+ | None -> (* At leats one statement is unreachable. *) ()
+ | Some ancestor -> assert (first == ancestor)
+ end;
+
+ (* Test that all statements (except the last one) have as common child
+ the return statement of f, unless one of them is unreachable. This test
+ supposes that frama-c's normalization removed all but one return statement.
+ *)
+ begin match Dominators.nearest_common_child all_but_last with
+ | None -> (* At leats one statement is unreachable. *) ()
+ | Some child -> assert (last == child)
+ end
+ end
+
+class visitPostDom = object(self)
+ inherit Visitor.frama_c_inplace
+
+ method! vfunc f =
+ let kf = Option.get (self#current_kf) in
+ Format.printf "@.@[<v>Computing for function %s:@;%a@?@;@?@]"
+ f.svar.vname Cil_printer.pp_block f.sbody;
+
+ Dominators.compute_dominators kf;
+ Dominators.print_dot_dominators "dom_graph" kf;
+
+ Dominators.compute_postdominators kf;
+ Dominators.print_dot_postdominators "postdom_graph" kf;
+
+ print_immediate f;
+ test_strict f;
+ test_nearest kf f;
+
+ SkipChildren
+end
+
+let cover_errors () =
+ Format.printf "Trigger some errors/warnings :@.";
+
+ (* Test when a statement is not in a function. *)
+ let loc = Cil_datatype.Location.unknown in
+ let skip = Cil_builder.Pure.(cil_stmt ~loc skip) in
+ try ignore (Dominators.get_postdominators skip) with Log.AbortFatal _ -> ();
+
+ let trigger kf =
+ match kf.fundec with
+ | Definition _ -> ()
+ | Declaration _ ->
+ (* Test Kernel_function.find_first_stmt on decl. *)
+ ignore @@ Dominators.compute_dominators kf;
+ (* Test Kernel_function.find_return on decl. *)
+ ignore @@ Dominators.compute_postdominators kf;
+ (* Test print_dot on decl. *)
+ ignore @@ Dominators.print_dot_dominators "tmp" kf
+ in
+ Globals.Functions.iter trigger
+
+let pretty () =
+ Format.printf "@.@[<v2>Dominators analysis:@;%a@]\n@."
+ Dominators.pretty_dominators ();
+ Format.printf "@[<v2>Postominators analysis:@;%a@]\n@."
+ Dominators.pretty_postdominators ()
+
+let startup () =
+ ignore (Cil.visitCilFileSameGlobals (new visitPostDom:>Cil.cilVisitor) (Ast.get ()));
+ pretty ();
+ Ast.mark_as_changed ();
+ Format.printf "Invalidate tables, which should now be empty\n";
+ pretty ();
+ cover_errors ()
+
+let () = Boot.Main.extend startup