Skip to content
Snippets Groups Projects
Commit 43b3e0f2 authored by David Bühler's avatar David Bühler
Browse files

Merge branch 'feature/martin/kernel/(post)dominators-using-interpreted-automata' into 'master' 

Compute (post)dominators analysis using interpreted automata

See merge request frama-c/frama-c!4647
parents 0cadd1ba 1b41e4e5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 317 additions and 937 deletions
src/kernel_services/analysis/dominators.ml
+ 228
− 244
View file @ 43b3e0f2
...@@ -20,261 +20,245 @@ ...@@ -20,261 +20,245 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
(** Computation of dominators. (* This module performs dataflow analysis using [Interpreted_automata] to
Based on "A Simple, Fast Dominance Algorithm" by K. D. Cooper et al. *) compute the domination/postdomination dependencies between statements of a
given function. *)
(* 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 *)
open Cil_types open Cil_types
(****************************************************************) let dkey = Kernel.dkey_dominators
module type DIRECTION = sig (* Datatype used to create a dot graph using analysis results. *)
(* Number of statements in the function. *) module StmtTbl = Cil_datatype.Stmt.Hashtbl
val nb_stmts: int
(* Conversion between statements and ordered statements. *) (* State type for our domain. *)
val to_ordered: stmt -> Ordered_stmt.ordered_stmt module StmtSet = Cil_datatype.Stmt.Hptset
val to_stmt: Ordered_stmt.ordered_stmt -> stmt
(* Iterates on all the statements, except the roots of the module DotGraph = Graph.Graphviz.Dot (
domination tree; in topological order for dominators, and reverse struct
topological order for the post-dominators. *) type t = string * (StmtSet.t StmtTbl.t)
val iter: (Ordered_stmt.ordered_stmt -> unit) -> unit 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), let iter_vertex f (_, graph) =
that will be the root of the dominator/post-dominator tree. *) StmtTbl.iter (fun stmt _ -> f stmt) graph
val root_stmt: Ordered_stmt.ordered_stmt;;
val is_further_from_root: let iter_edges_e f (_, graph) =
Ordered_stmt.ordered_stmt -> Ordered_stmt.ordered_stmt -> bool StmtTbl.iter (fun stmt -> StmtSet.iter (fun p -> f (p, stmt))) graph
(* List of all predecessors for the dominators, list of successors let graph_attributes (title, _) = [`Label title]
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
val name:string let default_vertex_attributes _g = [`Shape `Box; `Style `Filled]
end
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 let widen a b =
if StmtSet.subset a b then
(* Computes the smallest common dominator between two statements. *) Interpreted_automata.Fixpoint
let nearest_common_ancestor find_domtree ord1 ord2 = else
Kernel.debug ~dkey:Kernel.dkey_dominators "computing common ancestor %d %d" Interpreted_automata.Widening (join a b)
(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
;;
(* 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 end
let direction_dom kf = (* An analysis needs a name and a starting point. *)
let (stmt_to_ordered,ordered_to_stmt,_) = module type Analysis = sig
Ordered_stmt.get_conversion_tables kf val name : string
in (* May raise Kernel_function.No_Statement. *)
let to_stmt = Ordered_stmt.to_stmt ordered_to_stmt in val get_starting_stmt : kernel_function -> stmt
let module Dominator = struct include Interpreted_automata.DataflowAnalysis with type state = Domain.t
let to_ordered = Ordered_stmt.to_ordered stmt_to_ordered;; end
let to_stmt = to_stmt;;
let nb_stmts = Array.length ordered_to_stmt;; (* Main module, perform the analysis, store its results and provide ways to
let root_stmt = to_ordered (Kernel_function.find_first_stmt kf) access them. *)
(* Iterate on all statements, except the entry point. *) module Compute (Analysis : Analysis) = struct
let iter f =
for i = 0 to nb_stmts -1 do module Table =
if i != root_stmt Cil_state_builder.Stmt_hashtbl
then f i (StmtSet)
done;; (struct
let is_further_from_root p1 p2 = p1 > p2 let name = Analysis.name ^ "_table"
let preds s = List.map to_ordered (to_stmt s).Cil_types.preds let dependencies = [Ast.self]
let name = "dom" let size = 503
end end)
in
(module Dominator: DIRECTION) let compute kf =
;; match Table.find_opt (Analysis.get_starting_stmt kf) with
| exception Kernel_function.No_Statement ->
(* Fill the project table with the dominators of a given function. *) Kernel.warning "No statement in function %a: %s analysis cannot be done"
let store_dom domtree to_stmt = Kernel_function.pretty kf Analysis.name
Array.iteri( fun ord idom -> | Some _ ->
let idom = Option.map to_stmt idom in Kernel.feedback ~dkey "%s analysis already computed for function %a"
let stmt = to_stmt ord in Analysis.name Kernel_function.pretty kf
Kernel.debug ~dkey:Kernel.dkey_dominators "storing dom for %d: %s" | None ->
stmt.sid (match idom with None -> "self" | Some s ->string_of_int s.sid); match kf.fundec with
Dom_tree.add stmt idom | Definition (f, _) ->
) domtree Kernel.feedback ~dkey "computing %s analysis for function %a"
Analysis.name Kernel_function.pretty kf;
let compute_dom kf = (* Compute the analysis, initial state is empty. *)
let direction = direction_dom kf in let result = Analysis.fixpoint kf StmtSet.empty in
let module Dominator = (val direction: DIRECTION) in (* Fill table with all statements. *)
let module ComputeDom = Compute(Dominator) in List.iter (fun stmt -> Table.add stmt StmtSet.empty) f.sallstmts;
let domtree = ComputeDom.domtree () in (* A reachable statement always (post)dominates itself, so add it here. *)
store_dom domtree Dominator.to_stmt 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;
(* Note: The chosen semantics for postdominator is the following one: a Kernel.feedback ~dkey "%s analysis done for function %a"
post-dominates b if all the paths from b to the return statement Analysis.name Kernel_function.pretty kf
goes through a. (* [Analysis.get_starting_stmt] should fatal before this point. *)
| Declaration _ -> assert false
Statements on the paths that go only into infinite loop, or to
__no_return function, do not have any post dominator (they are set let find_kf stmt =
to None). try Kernel_function.find_englobing_kf stmt
with Not_found ->
This definition of post-dominator gives a single root to the Kernel.fatal "Statement %d is not part of a function" stmt.sid
post-domination tree, which is required by the Cooper algorithm
above. Beware that there are alternative, incompatible, definitions (* Generic function to get the set of (post)dominators of [stmt]. *)
to post-domination, e.g. saying that a post dominates b if all the let get stmt =
paths from b to any return statement or infinite loop go through match Table.find_opt stmt with
a. *) | None -> compute (find_kf stmt); Table.find stmt
(* TODO: | Some v -> v
- For each statement, associate its immediate post-dominator (if it
exists), and the list of sinks that dominates it (* Generic function to get the set of strict (post)dominators of [stmt]. *)
let get_strict stmt = get stmt |> StmtSet.remove stmt
- Attempt to find the post-dominator by intersection only if the
list of sinks of the points is the same. Otherwise, state that (* Generic function to test the (post)domination of 2 statements. *)
there is no immediate post-dominator, and that the point is let mem a b = get b |> StmtSet.mem a
dominated by the union of the lists of sinks of its successors.
*) (* Generic function to test the strict (post)domination of 2 statements. *)
let _compute_pdom kf = let mem_strict a b = get_strict b |> StmtSet.mem a
let (stmt_to_ordered,ordered_to_stmt,_) =
Ordered_stmt.get_conversion_tables kf (* The nearest common ancestor (resp. child) is the ancestor which is
in dominated (resp. postdominated) by all common ancestors, ie. the lowest
let module PostDominator = struct (resp. highest) ancestor in the domination tree. *)
let to_ordered = Ordered_stmt.to_ordered stmt_to_ordered;; let nearest stmtl =
let to_stmt = Ordered_stmt.to_stmt ordered_to_stmt;; (* Get the set of strict (post)doms for each statement and intersect them to
let nb_stmts = Array.length ordered_to_stmt;; keep the common ones. If one of them is unreachable, they do not
let root_stmt = to_ordered (Kernel_function.find_return kf) share a common ancestor/child. *)
let iter f = let common_set =
for i = nb_stmts -1 downto 0 do match stmtl with
if i != root_stmt | [] -> StmtSet.empty
then f i | stmt :: tail ->
done;; List.fold_left
let is_further_from_root p1 p2 = p1 < p2 (fun acc s -> StmtSet.inter acc (get_strict s))
let preds s = List.map to_ordered (to_stmt s).Cil_types.succs (get_strict stmt) tail
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)
in 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
src/kernel_services/analysis/dominators.mli
+ 82
− 14
View file @ 43b3e0f2
...@@ -20,22 +20,90 @@ ...@@ -20,22 +20,90 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
(** Computation of dominators. *) (** Module to perform dominators and postdominators analyses. This module was
open Cil_types;; completely redesigned and provides many new functions.
val get_idom: stmt -> stmt option A dominator [d] of [s] is a statement such that all paths from the entry
(** Immediate dominator of the statement. *) point of a function to [s] must go through [d].
val dominates: stmt -> stmt -> bool A postdominator [p] of [s] is a statement such that all paths from [s] to
(** [dominates a b] tells whether [a] dominates [b]. *) the return point of the function must go through [p].
val nearest_common_ancestor: stmt list -> stmt By definition, a statement always (post)dominates itself (except if it is
(** Finds the statement lowest in the function that dominates unreachable).
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. *)
(* An immediate (post)dominator (or i(post)dom) [d] is the unique
Local Variables: (post)dominator of [s] that strictly (post)dominates [s] but is
compile-command: "make -C ../../.." (post)dominated by all other (post)dominators of [s].
End:
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]. *)
src/plugins/eva/domains/taint_domain.ml
+ 1
− 4
View file @ 43b3e0f2
...@@ -168,12 +168,9 @@ module TransferTaint = struct ...@@ -168,12 +168,9 @@ module TransferTaint = struct
from the tainted assume that not go through [stmt], ie [stmt] is not a from the tainted assume that not go through [stmt], ie [stmt] is not a
postdominator for the tainted assume. *) postdominator for the tainted assume. *)
let filter_active_tainted_assumes stmt state = let filter_active_tainted_assumes stmt state =
let kf = Kernel_function.find_englobing_kf stmt in
let assume_stmts = let assume_stmts =
Stmt.Set.filter Stmt.Set.filter
(fun assume_stmt -> (fun assume_stmt -> not (Dominators.postdominates stmt assume_stmt))
not (Postdominators.is_postdominator kf
~opening:assume_stmt ~closing:stmt))
state.assume_stmts state.assume_stmts
in in
{ state with assume_stmts } { state with assume_stmts }
......
src/plugins/eva/dune
+ 1
− 2
View file @ 43b3e0f2
...@@ -28,7 +28,6 @@ ...@@ -28,7 +28,6 @@
(echo "EVA:" %{lib-available:frama-c-eva.core} "\n") (echo "EVA:" %{lib-available:frama-c-eva.core} "\n")
(echo " - ppx_deriving.eq:" %{lib-available:ppx_deriving.eq} "\n") (echo " - ppx_deriving.eq:" %{lib-available:ppx_deriving.eq} "\n")
(echo " - ppx_deriving.ord:" %{lib-available:ppx_deriving.ord} "\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 "Numerors:" %{lib-available:frama-c-eva.numerors.core} "\n")
(echo " - MLMPFR:" %{lib-available:mlmpfr} "\n") (echo " - MLMPFR:" %{lib-available:mlmpfr} "\n")
(echo "Apron domains:" %{lib-available:frama-c-eva.apron.core} "\n") (echo "Apron domains:" %{lib-available:frama-c-eva.apron.core} "\n")
...@@ -42,7 +41,7 @@ ...@@ -42,7 +41,7 @@
(optional) (optional)
(public_name frama-c-eva.core) (public_name frama-c-eva.core)
(flags -open Frama_c_kernel :standard -w -9) (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 landmarks))
(instrumentation (backend bisect_ppx)) (instrumentation (backend bisect_ppx))
(preprocess (pps ppx_deriving.eq ppx_deriving.ord))) (preprocess (pps ppx_deriving.eq ppx_deriving.ord)))
......
src/plugins/from/dune
+ 1
− 2
View file @ 43b3e0f2
...@@ -27,7 +27,6 @@ ...@@ -27,7 +27,6 @@
(echo "From:" %{lib-available:frama-c-from.core} "\n") (echo "From:" %{lib-available:frama-c-from.core} "\n")
(echo " - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n") (echo " - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
(echo " - Eva:" %{lib-available:frama-c-eva.core} "\n") (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
(echo " - Postdominators:" %{lib-available:frama-c-postdominators.core} "\n")
) )
) )
) )
...@@ -37,7 +36,7 @@ ...@@ -37,7 +36,7 @@
(optional) (optional)
(public_name frama-c-from.core) (public_name frama-c-from.core)
(flags -open Frama_c_kernel :standard -w -9) (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 landmarks))
(instrumentation (backend bisect_ppx)) (instrumentation (backend bisect_ppx))
) )
......
src/plugins/from/from_compute.ml
+ 1
− 2
View file @ 43b3e0f2
...@@ -477,12 +477,11 @@ struct ...@@ -477,12 +477,11 @@ struct
(* Eliminate additional variables originating from a control-flow branching (* Eliminate additional variables originating from a control-flow branching
statement closing at [s]. *) statement closing at [s]. *)
let eliminate_additional s data = let eliminate_additional s data =
let kf = Stack.top call_stack in
let map = data.additional_deps_table in let map = data.additional_deps_table in
let map' = let map' =
ZoneStmtMap.fold ZoneStmtMap.fold
(fun k _v acc_map -> (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 then ZoneStmtMap.remove k acc_map
else acc_map else acc_map
) map map ) map map
......
src/plugins/gui/help_manager.ml
+ 1
− 1
View file @ 43b3e0f2
...@@ -79,7 +79,7 @@ let show main_ui = ...@@ -79,7 +79,7 @@ let show main_ui =
let copyright (* should be automatically generated *) = let copyright (* should be automatically generated *) =
"\t © CEA and INRIA for the Frama-C kernel\n\ "\t © CEA and INRIA for the Frama-C kernel\n\
\t © CEA for the GUI and plug-ins constant propagation, from, inout, impact, \ \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\ semantic callgraph, slicing, sparecode, syntactic callgraph, users and value.\n\
\n\ \n\
See the particular header of each source file for details." See the particular header of each source file for details."
......
src/plugins/loop_analysis/region_analysis_stmt.ml
+ 1
− 0
View file @ 43b3e0f2
...@@ -100,6 +100,7 @@ struct ...@@ -100,6 +100,7 @@ struct
module DomTree = struct module DomTree = struct
let dominates = Dominators.dominates let dominates = Dominators.dominates
let domtree_postfix_iter f = let domtree_postfix_iter f =
(* Reverse the normal domtree. *) (* Reverse the normal domtree. *)
......
src/plugins/postdominators/compute.ml deleted 100644 → 0
+ 0
− 228
View file @ 0cadd1ba
(**************************************************************************)
(* *)
(* 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:
*)
src/plugins/postdominators/compute.mli deleted 100644 → 0
+ 0
− 41
View file @ 0cadd1ba
(**************************************************************************)
(* *)
(* 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
src/plugins/postdominators/dune deleted 100644 → 0
+ 0
− 42
View file @ 0cadd1ba
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 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)))
src/plugins/postdominators/dune-project deleted 100644 → 0
+ 0
− 25
View file @ 0cadd1ba
(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)
src/plugins/postdominators/frama-c-postdominators.opam deleted 100644 → 0
+ 0
− 0
View file @ 0cadd1ba
src/plugins/postdominators/postdominators.ml deleted 100644 → 0
+ 0
− 42
View file @ 0cadd1ba
(**************************************************************************)
(* *)
(* 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
src/plugins/postdominators/postdominators.mli deleted 100644 → 0
+ 0
− 43
View file @ 0cadd1ba
(**************************************************************************)
(* *)
(* 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]. *)
src/plugins/postdominators/postdominators_parameters.ml deleted 100644 → 0
+ 0
− 42
View file @ 0cadd1ba
(**************************************************************************)
(* *)
(* 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:
*)
src/plugins/postdominators/postdominators_parameters.mli deleted 100644 → 0
+ 0
− 32
View file @ 0cadd1ba
(**************************************************************************)
(* *)
(* 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:
*)
src/plugins/postdominators/print.ml deleted 100644 → 0
+ 0
− 148
View file @ 0cadd1ba
(**************************************************************************)
(* *)
(* 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:
*)
src/plugins/postdominators/print.mli deleted 100644 → 0
+ 0
− 23
View file @ 0cadd1ba
(**************************************************************************)
(* *)
(* 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
src/plugins/scope/datascope.ml
+ 1
− 2
View file @ 43b3e0f2
...@@ -537,8 +537,7 @@ let get_prop_scope_at_stmt ~warn kf stmt ?(proven=CA_Map.empty) annot = ...@@ -537,8 +537,7 @@ let get_prop_scope_at_stmt ~warn kf stmt ?(proven=CA_Map.empty) annot =
end; end;
let add ((acc_scope, acc_to_be_rm) as acc) s = match pre_state s with let add ((acc_scope, acc_to_be_rm) as acc) s = match pre_state s with
| State.SameVal -> | State.SameVal ->
if Dominators.dominates stmt s && not (Cil_datatype.Stmt.equal stmt s) if Dominators.strictly_dominates stmt s then
then
let acc_scope = add_s s acc_scope in 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 let acc_to_be_rm = check_stmt_annots (annot, stmt) s acc_to_be_rm in
(acc_scope, acc_to_be_rm) (acc_scope, acc_to_be_rm)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment