From 1ba76928e7365567ee4a8ae58c7cd84bbc596ceb Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 24 Jun 2022 16:05:56 +0200
Subject: [PATCH] [Pdg] removing Pdg from Db
---
src/kernel_services/plugin_entry_points/db.ml | 80 ----
.../plugin_entry_points/db.mli | 323 ----------------
src/plugins/impact/compute_impact.ml | 34 +-
src/plugins/impact/dune | 3 +-
src/plugins/impact/gui/dune | 2 +-
src/plugins/impact/gui/register_gui.ml | 7 +-
src/plugins/impact/pdg_aux.ml | 4 +-
src/plugins/impact/pdg_aux.mli | 11 +-
src/plugins/impact/reason_graph.ml | 2 +-
src/plugins/pdg/Pdg.ml | 5 +-
src/plugins/pdg/Pdg.mli | 5 +-
src/plugins/pdg/annot.ml | 8 +-
src/plugins/pdg/api.ml | 111 ++++++
src/plugins/pdg/api.mli | 350 ++++++++++++++++++
src/plugins/pdg/marks.ml | 14 +-
src/plugins/pdg/pdg_tbl.ml | 59 +++
src/plugins/pdg/pdg_tbl.mli | 44 +++
src/plugins/pdg/register.ml | 94 +----
src/plugins/postdominators/print.ml | 2 +-
src/plugins/scope/defs.ml | 28 +-
src/plugins/scope/dune | 3 +-
src/plugins/scope/zones.ml | 6 +-
src/plugins/security_slicing/components.ml | 78 ++--
src/plugins/security_slicing/dune | 3 +-
src/plugins/slicing/fct_slice.ml | 42 +--
src/plugins/slicing/printSlice.ml | 2 +-
src/plugins/slicing/slicingActions.ml | 10 +-
src/plugins/slicing/slicingActions.mli | 2 +-
src/plugins/slicing/slicingMacros.ml | 2 +-
src/plugins/slicing/slicingMacros.mli | 4 +-
src/plugins/slicing/slicingSelect.ml | 90 ++---
src/plugins/slicing/slicingSelect.mli | 4 +-
src/plugins/slicing/slicingState.ml | 2 +-
src/plugins/slicing/slicingTransform.ml | 20 +-
src/plugins/sparecode/globs.ml | 2 +-
src/plugins/sparecode/register.ml | 2 +-
src/plugins/sparecode/spare_marks.ml | 18 +-
src/plugins/sparecode/transform.ml | 2 +-
tests/pdg/dyn_dpds.ml | 16 +-
tests/pdg/sets.ml | 19 +-
tests/slicing/libSelect.ml | 2 +-
tests/slicing/min_call.ml | 8 +-
tests/slicing/select_by_annot.ml | 2 +-
tests/slicing/simple_intra_slice.ml | 2 +-
44 files changed, 801 insertions(+), 726 deletions(-)
create mode 100644 src/plugins/pdg/api.ml
create mode 100644 src/plugins/pdg/api.mli
create mode 100644 src/plugins/pdg/pdg_tbl.ml
create mode 100644 src/plugins/pdg/pdg_tbl.mli
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 64e5c108ab5..4d69ac1a7f4 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -708,86 +708,6 @@ module From = struct
end
end
-(* ************************************************************************* *)
-(** {2 PDG} *)
-(* ************************************************************************* *)
-
-module Pdg = struct
- type t = PdgTypes.Pdg.t
-
- type t_nodes_and_undef =
- ((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
-
- exception Top = PdgTypes.Pdg.Top
- exception Bottom = PdgTypes.Pdg.Bottom
-
- let self = ref State.dummy
-
- let get = mk_fun "Pdg.get"
-
- let from_same_fun pdg1 pdg2 =
- let kf1 = PdgTypes.Pdg.get_kf pdg1 in
- let kf2 = PdgTypes.Pdg.get_kf pdg2 in
- Kernel_function.equal kf1 kf2
-
- let node_key = mk_fun "Pdg.node_key"
-
- let find_decl_var_node = mk_fun "Pdg.find_decl_var_node"
- let find_input_node = mk_fun "Pdg.find_input_nodes"
- let find_ret_output_node = mk_fun "Pdg.find_ret_output_node"
- let find_output_nodes = mk_fun "Pdg.find_output_nodes"
- let find_all_inputs_nodes = mk_fun "Pdg.find_all_inputs_nodes"
- let find_stmt_and_blocks_nodes = mk_fun "Pdg.find_stmt_and_blocks_nodes"
- let find_simple_stmt_nodes = mk_fun "Pdg.find_simplestmt_nodes"
- let find_stmt_node = mk_fun "Pdg.find_stmt_node"
- let find_label_node = mk_fun "Pdg.find_label_node"
- let find_entry_point_node = mk_fun "Pdg.find_entry_point_node"
- let find_top_input_node = mk_fun "Pdg.find_top_input_node"
- let find_call_ctrl_node = mk_fun "Pdg.find_call_ctrl_node"
- let find_location_nodes_at_stmt = mk_fun "Pdg.find_location_nodes_at_stmt"
- let find_location_nodes_at_end = mk_fun "Pdg.find_location_nodes_at_end"
- let find_location_nodes_at_begin = mk_fun "Pdg.find_location_nodes_at_begin"
- let find_call_input_node = mk_fun "Pdg.find_call_input_node"
- let find_call_output_node = mk_fun "Pdg.find_call_output_node"
- let find_code_annot_nodes = mk_fun "Pdg.find_code_annot_nodes"
- let find_fun_precond_nodes = mk_fun "Pdg.find_fun_precond_nodes"
- let find_fun_postcond_nodes = mk_fun "Pdg.find_fun_postcond_nodes"
- let find_fun_variant_nodes = mk_fun "Pdg.find_fun_variant_nodes"
-
- let find_call_out_nodes_to_select = mk_fun "Pdg.find_call_out_nodes_to_select"
- let find_in_nodes_to_select_for_this_call =
- mk_fun "Pdg.find_in_nodes_to_select_for_this_call"
-
- let direct_dpds = mk_fun "Pdg.direct_dpds"
- let direct_ctrl_dpds = mk_fun "Pdg.direct_ctrl_dpds"
- let direct_data_dpds = mk_fun "Pdg.direct_data_dpds"
- let direct_addr_dpds = mk_fun "Pdg.direct_addr_dpds"
-
- let all_dpds = mk_fun "Pdg.all_dpds"
- let all_ctrl_dpds = mk_fun "Pdg.all_ctrl_dpds"
- let all_data_dpds = mk_fun "Pdg.all_data_dpds"
- let all_addr_dpds = mk_fun "Pdg.all_addr_dpds"
-
- let direct_uses = mk_fun "Pdg.direct_uses"
- let direct_ctrl_uses = mk_fun "Pdg.direct_ctrl_uses"
- let direct_data_uses = mk_fun "Pdg.direct_data_uses"
- let direct_addr_uses = mk_fun "Pdg.direct_addr_uses"
-
- let all_uses = mk_fun "Pdg.all_uses"
-
- let custom_related_nodes = mk_fun "Pdg.custom_related_nodes"
-
- let find_call_stmts = mk_fun "Pdg.find_call_stmts"
-
- let iter_nodes = mk_fun "Pdg.iter_nodes"
-
- let extract = mk_fun "Pdg.extract"
- let pretty = ref (fun ?bw:_ _ _ -> mk_labeled_fun "Pdg.pretty")
- let pretty_node = mk_fun "Pdg.pretty_node"
- let pretty_key = mk_fun "Pdg.pretty_key"
-
-end
-
(* ************************************************************************* *)
(** {2 Properties} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 905663fa636..62334a53e2e 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -844,329 +844,6 @@ module Security : sig
end
-(** Program Dependence Graph.
- @see <../pdg/index.html> PDG internal documentation. *)
-module Pdg : sig
-
- exception Bottom
- (** Raised by most function when the PDG is Bottom because we can hardly do
- nothing with it. It happens when the function is unreachable because we
- have no information about it. *)
-
- exception Top
- (** Raised by most function when the PDG is Top because we can hardly do
- nothing with it. It happens when we didn't manage to compute it, for
- instance for a variadic function. *)
-
- type t = PdgTypes.Pdg.t
- (** PDG type *)
-
- type t_nodes_and_undef =
- ((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
- (** type for the return value of many [find_xxx] functions when the
- answer can be a list of [(node, z_part)] and an [undef zone].
- For each node, [z_part] can specify which part of the node
- is used in terms of zone ([None] means all).
- *)
-
- val self : State.t ref
-
- (** {3 Getters} *)
-
- val get : (kernel_function -> t) ref
- (** Get the PDG of a function. Build it if it doesn't exist yet. *)
-
- val node_key : (PdgTypes.Node.t -> PdgIndex.Key.t) ref
-
- val from_same_fun : t -> t -> bool
-
- (** {3 Finding PDG nodes} *)
-
- val find_decl_var_node : (t -> Cil_types.varinfo -> PdgTypes.Node.t) ref
- (** Get the node corresponding the declaration of a local variable or a
- formal parameter.
- @raise Not_found if the variable is not declared in this function.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_ret_output_node : (t -> PdgTypes.Node.t) ref
- (** Get the node corresponding return stmt.
- @raise Not_found if the output state in unreachable
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_output_nodes :
- (t -> PdgIndex.Signature.out_key -> t_nodes_and_undef) ref
- (** Get the nodes corresponding to a call output key in the called pdg.
- @raise Not_found if the output state in unreachable
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_input_node : (t -> int -> PdgTypes.Node.t) ref
- (** Get the node corresponding to a given input (parameter).
- @raise Not_found if the number is not an input number.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_all_inputs_nodes : (t -> PdgTypes.Node.t list) ref
- (** Get the nodes corresponding to all inputs.
- {!node_key} can be used to know their numbers.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_stmt_node : (t -> Cil_types.stmt -> PdgTypes.Node.t) ref
- (** Get the node corresponding to the statement.
- It shouldn't be a call statement.
- See also {!find_simple_stmt_nodes} or {!find_call_stmts}.
- @raise Not_found if the given statement is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top.
- @raise PdgIndex.CallStatement if the given stmt is a function
- call. *)
-
-
- val find_simple_stmt_nodes : (t -> Cil_types.stmt -> PdgTypes.Node.t list) ref
- (** Get the nodes corresponding to the statement.
- It is usually composed of only one node (see {!find_stmt_node}),
- except for call statement.
- Be careful that for block statements, it only returns a node
- corresponding to the elementary stmt
- (see {!find_stmt_and_blocks_nodes} for more)
- @raise Not_found if the given statement is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_label_node : (t -> Cil_types.stmt -> Cil_types.label -> PdgTypes.Node.t) ref
- (** Get the node corresponding to the label.
- @raise Not_found if the given label is not in the PDG.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_stmt_and_blocks_nodes : (t -> Cil_types.stmt -> PdgTypes.Node.t list) ref
- (** Get the nodes corresponding to the statement like
- * {!find_simple_stmt_nodes} but also add the nodes of the enclosed
- * statements if [stmt] contains blocks.
- @raise Not_found if the given statement is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_top_input_node : (t -> PdgTypes.Node.t) ref
- (** @raise Not_found if there is no top input in the PDG.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_entry_point_node : (t -> PdgTypes.Node.t) ref
- (** Find the node that represent the entry point of the function, i.e. the
- higher level block.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_location_nodes_at_stmt :
- (t -> Cil_types.stmt -> before:bool -> Locations.Zone.t
- -> t_nodes_and_undef) ref
- (** Find the nodes that define the value of the location at the given
- program point. Also return a zone that might be undefined at that
- point.
- @raise Not_found if the given statement is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_location_nodes_at_end :
- (t -> Locations.Zone.t -> t_nodes_and_undef) ref
- (** Same than {!find_location_nodes_at_stmt} for the program point located
- at the end of the function.
- @raise Not_found if the output state is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_location_nodes_at_begin :
- (t -> Locations.Zone.t -> t_nodes_and_undef) ref
- (** Same than {!find_location_nodes_at_stmt} for the program point located
- at the beginning of the function.
- Notice that it can only find formal argument nodes.
- The remaining zone (implicit input) is returned as undef.
- @raise Not_found if the output state is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_call_stmts:
- (kernel_function -> caller:kernel_function -> Cil_types.stmt list) ref
- (** Find the call statements to the function (can maybe be somewhere
- else).
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_call_ctrl_node : (t -> Cil_types.stmt -> PdgTypes.Node.t) ref
- (** @raise Not_found if the call is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_call_input_node : (t -> Cil_types.stmt -> int -> PdgTypes.Node.t) ref
- (** @raise Not_found if the call is unreachable or has no such input.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_call_output_node : (t -> Cil_types.stmt -> PdgTypes.Node.t) ref
- (** @raise Not_found if the call is unreachable or has no output node.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_code_annot_nodes :
- (t -> Cil_types.stmt -> Cil_types.code_annotation ->
- PdgTypes.Node.t list * PdgTypes.Node.t list * (t_nodes_and_undef option)) ref
- (** The result is composed of three parts :
- - the first part of the result are the control dependencies nodes
- of the annotation,
- - the second part is the list of declaration nodes of the variables
- used in the annotation;
- - the third part is similar to [find_location_nodes_at_stmt] result
- but for all the locations needed by the annotation.
- When the third part is globally [None],
- it means that we were not able to compute this information.
- @raise Not_found if the statement is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_fun_precond_nodes :
- (t -> Cil_types.predicate -> PdgTypes.Node.t list * (t_nodes_and_undef option)) ref
- (** Similar to [find_code_annot_nodes] (no control dependencies nodes) *)
-
- val find_fun_postcond_nodes :
- (t -> Cil_types.predicate -> PdgTypes.Node.t list * (t_nodes_and_undef option)) ref
- (** Similar to [find_fun_precond_nodes] *)
-
- val find_fun_variant_nodes :
- (t -> Cil_types.term -> (PdgTypes.Node.t list * t_nodes_and_undef option)) ref
- (** Similar to [find_fun_precond_nodes] *)
-
- (** {3 Propagation}
- See also [Pdg.mli] for more function that cannot be here because
- they use polymorphic types.
- **)
-
- val find_call_out_nodes_to_select :
- (t -> PdgTypes.NodeSet.t -> t -> Cil_types.stmt -> PdgTypes.Node.t list) ref
- (** [find_call_out_nodes_to_select pdg_called called_selected_nodes
- pdg_caller call_stmt]
- @return the call outputs nodes [out] such that
- [find_output_nodes pdg_called out_key]
- intersects [called_selected_nodes]. *)
-
- val find_in_nodes_to_select_for_this_call :
- (t -> PdgTypes.NodeSet.t -> Cil_types.stmt -> t -> PdgTypes.Node.t list) ref
- (** [find_in_nodes_to_select_for_this_call
- pdg_caller caller_selected_nodes call_stmt pdg_called]
- @return the called input nodes such that the corresponding nodes
- in the caller intersect [caller_selected_nodes]
- @raise Not_found if the statement is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- (** {3 Dependencies} *)
-
- val direct_dpds : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Get the nodes to which the given node directly depend on.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_ctrl_dpds : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Similar to {!direct_dpds}, but for control dependencies only.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_data_dpds : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Similar to {!direct_dpds}, but for data dependencies only.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_addr_dpds : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Similar to {!direct_dpds}, but for address dependencies only.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val all_dpds : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) ref
- (** Transitive closure of {!direct_dpds} for all the given nodes.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val all_data_dpds : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) ref
- (** Gives the data dependencies of the given nodes, and recursively, all
- the dependencies of those nodes (regardless to their kind).
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val all_ctrl_dpds : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) ref
- (** Similar to {!all_data_dpds} for control dependencies.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val all_addr_dpds : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) ref
- (** Similar to {!all_data_dpds} for address dependencies.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_uses : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** build a list of all the nodes that have direct dependencies on the
- given node.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_ctrl_uses : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Similar to {!direct_uses}, but for control dependencies only.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_data_uses : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Similar to {!direct_uses}, but for data dependencies only.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_addr_uses : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Similar to {!direct_uses}, but for address dependencies only.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val all_uses : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) ref
- (** build a list of all the nodes that have dependencies (even indirect) on
- the given nodes.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val custom_related_nodes :
- ((PdgTypes.Node.t -> PdgTypes.Node.t list) -> PdgTypes.Node.t list -> PdgTypes.Node.t list) ref
- (** [custom_related_nodes get_dpds node_list] build a list, starting from
- the node in [node_list], and recursively add the nodes given by the
- function [get_dpds]. For this function to work well, it is important
- that [get_dpds n] returns a subset of the nodes directly related to
- [n], ie a subset of [direct_uses] U [direct_dpds].
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val iter_nodes : ((PdgTypes.Node.t -> unit) -> t -> unit) ref
- (** apply a given function to all the PDG nodes
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- (** {3 Pretty printing} *)
-
- val extract : (t -> string -> unit) ref
- (** Pretty print pdg into a dot file.
- @see <../pdg/index.html> PDG internal documentation. *)
-
- val pretty_node : (bool -> Format.formatter -> PdgTypes.Node.t -> unit) ref
- (** Pretty print information on a node : with [short=true], only the id
- of the node is printed.. *)
-
- val pretty_key : (Format.formatter -> PdgIndex.Key.t -> unit) ref
- (** Pretty print information on a node key *)
-
- val pretty : (?bw:bool -> Format.formatter -> t -> unit) ref
- (** For debugging... Pretty print pdg information.
- Print codependencies rather than dependencies if [bw=true]. *)
-
-end
-
-
(** Signature common to some Inout plugin options. The results of
the computations are available on a per function basis. *)
module type INOUTKF = sig
diff --git a/src/plugins/impact/compute_impact.ml b/src/plugins/impact/compute_impact.ml
index 1744f0a3e7d..f8d9abc1c11 100644
--- a/src/plugins/impact/compute_impact.ml
+++ b/src/plugins/impact/compute_impact.ml
@@ -166,7 +166,7 @@ let add_to_result wl n kf init =
(** return [true] if the location in [n] is contained in [skip], in which
case the node should be skipped entirely *)
let node_to_skip skip n =
- match !Db.Pdg.node_key n with
+ match Pdg.Api.node_key n with
| Key.SigKey (Signature.In (Signature.InImpl z))
| Key.SigKey (Signature.Out (Signature.OutLoc z))
| Key.SigCallKey (_, Signature.In (Signature.InImpl z))
@@ -179,7 +179,7 @@ let node_to_skip skip n =
the results *)
let filter wl (n, z) =
not (Locations.Zone.is_bottom z) &&
- match !Db.Pdg.node_key n with
+ match Pdg.Api.node_key n with
| Key.SigKey (Signature.In Signature.InCtrl) -> false
(* do not consider node [InCtrl]. YYY: find when this may happen *)
| Key.VarDecl _ -> false
@@ -320,7 +320,7 @@ let add_downward_call wl (caller_kf, pdg) (called_kf, called_pdg) stmt =
callee are directly in the worklist, and the call is registered in the
field [downward_calls]. *)
let downward_one_call_node wl (pnode, _ as node) caller_kf pdg =
- match !Db.Pdg.node_key pnode with
+ match Pdg.Api.node_key pnode with
| Key.SigKey (Signature.In Signature.InCtrl) (* never in the worklist *)
| Key.VarDecl _ (* never in the worklist *)
| Key.CallStmt _ (* pdg returns a SigCallKey instead *)
@@ -335,31 +335,31 @@ let downward_one_call_node wl (pnode, _ as node) caller_kf pdg =
let called_kfs = Eva.Results.callee stmt in
List.iter
(fun called_kf ->
- let called_pdg = !Db.Pdg.get called_kf in
+ let called_pdg = Pdg.Api.get called_kf in
let nodes_callee, pdg_ok =
Options.debug ~level:3 "%a: considering call to %a"
Pdg_aux.pretty_node node Kernel_function.pretty called_kf;
try
(match key with
| Signature.In (Signature.InNum n) ->
- (try [!Db.Pdg.find_input_node called_pdg n,
+ (try [Pdg.Api.find_input_node called_pdg n,
Locations.Zone.top]
with Not_found -> [])
| Signature.In Signature.InCtrl ->
- (try [!Db.Pdg.find_entry_point_node called_pdg,
+ (try [Pdg.Api.find_entry_point_node called_pdg,
Locations.Zone.top]
with Not_found -> [])
| Signature.In (Signature.InImpl _) -> assert false
| Signature.Out _ -> []
), true
with
- | Db.Pdg.Top ->
+ | Pdg.Api.Top ->
Options.warning
"no precise pdg for function %s. \n\
Ignoring this function in the analysis (potentially incorrect results)."
(Kernel_function.get_name called_kf);
[], false
- | Db.Pdg.Bottom ->
+ | Pdg.Api.Bottom ->
(*Function that fails or never returns immediately *)
[], false
| Not_found -> assert false
@@ -398,7 +398,7 @@ let downward_one_call_inputs wl kf_caller kf_callee (node, deps) =
(fun nsrc ->
add_to_reason wl ~nsrc ~ndst:node' InterproceduralDownward)
inter;
- add_to_do wl kf_callee (!Db.Pdg.get kf_callee) node';
+ add_to_do wl kf_callee (Pdg.Api.get kf_callee) node';
;;
(** Propagate impact for all calls registered in [downward_calls]. For each
@@ -447,10 +447,10 @@ let all_upward_callers wl kfs =
let todo =
if not (KFS.mem kf wl.callers) then (
Options.debug "Found caller %a" Kernel_function.pretty kf;
- let pdg_kf = !Db.Pdg.get kf in
+ let pdg_kf = Pdg.Api.get kf in
List.fold_left
(fun todo (caller, callsites) ->
- let pdg_caller = !Db.Pdg.get caller in
+ let pdg_caller = Pdg.Api.get caller in
List.iter (aux_call (caller, pdg_caller) (kf, pdg_kf)) callsites;
KFS.add caller todo
) todo (Eva.Results.callsites kf);
@@ -486,9 +486,9 @@ let upward_in_callers wl =
add_to_reason wl ~nsrc ~ndst:n InterproceduralUpward
) inter;
if init then
- add_to_do_part_of_initial wl caller (!Db.Pdg.get caller) n
+ add_to_do_part_of_initial wl caller (Pdg.Api.get caller) n
else
- add_to_do wl caller (!Db.Pdg.get caller) n
+ add_to_do wl caller (Pdg.Api.get caller) n
) (Lazy.force l)
in
KfKfCall.Map.iter aux wl.upward_calls;
@@ -522,7 +522,7 @@ let initial_worklist ?(skip=Locations.Zone.bottom) ?(reason=false) nodes kf =
}
in
(* Fill the [todo] field *)
- initial_to_do_list wl kf (!Db.Pdg.get kf) nodes;
+ initial_to_do_list wl kf (Pdg.Api.get kf) nodes;
let initial_callers =
if Options.Upward.get () then KFS.singleton kf else KFS.empty
in
@@ -536,10 +536,10 @@ let initial_worklist ?(skip=Locations.Zone.bottom) ?(reason=false) nodes kf =
callees of the call. *)
let initial_nodes ~skip kf stmt =
Options.debug ~level:3 "computing initial nodes for %d" stmt.sid;
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
if Eva.Results.is_reachable stmt then
try
- let all = !Db.Pdg.find_simple_stmt_nodes pdg stmt in
+ let all = Pdg.Api.find_simple_stmt_nodes pdg stmt in
let filter n = match PdgTypes.Node.elem_key n with
| Key.SigCallKey (_, Signature.In _) -> false
| _ -> not (node_to_skip skip n)
@@ -669,7 +669,7 @@ let result_to_nodes (res: result) : nodes =
(** Transform a set of PDG nodes into a set of statements *)
let nodes_to_stmts ns =
- let get_stmt node = Key.stmt (!Db.Pdg.node_key node) in
+ let get_stmt node = Key.stmt (Pdg.Api.node_key node) in
let set =
(* Do not generate a list immediately, some nodes would be duplicated *)
NS.fold
diff --git a/src/plugins/impact/dune b/src/plugins/impact/dune
index 734041fbd96..6bcede10dbb 100644
--- a/src/plugins/impact/dune
+++ b/src/plugins/impact/dune
@@ -28,6 +28,7 @@
(echo " - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
(echo " - Slicing:" %{lib-available:frama-c-slicing.core} "\n")
(echo " - Inout:" %{lib-available:frama-c-inout.core} "\n")
+ (echo " - Pdg:" %{lib-available:frama-c-pdg.core} "\n")
)
)
)
@@ -38,7 +39,7 @@
(optional)
(public_name frama-c-impact.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-slicing.core frama-c-callgraph.core frama-c-inout.core)
+ (libraries frama-c.kernel frama-c-pdg.core frama-c-slicing.core frama-c-callgraph.core frama-c-inout.core)
)
(plugin (optional) (name impact) (libraries frama-c-impact.core) (site (frama-c plugins)))
diff --git a/src/plugins/impact/gui/dune b/src/plugins/impact/gui/dune
index 39db9c604ef..e00946f6944 100644
--- a/src/plugins/impact/gui/dune
+++ b/src/plugins/impact/gui/dune
@@ -25,7 +25,7 @@
(public_name frama-c-impact.gui)
(optional)
(flags -open Frama_c_kernel -open Frama_c_gui -open Impact :standard -w -9)
- (libraries frama-c.kernel frama-c.gui frama-c-impact.core frama-c-slicing.core frama-c-callgraph.core)
+ (libraries frama-c.kernel frama-c.gui frama-c-pdg.core frama-c-impact.core frama-c-slicing.core frama-c-callgraph.core)
)
(plugin (optional) (name impact-gui) (libraries frama-c-impact.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/impact/gui/register_gui.ml b/src/plugins/impact/gui/register_gui.ml
index 5146cb4a509..bdbc771e13c 100644
--- a/src/plugins/impact/gui/register_gui.ml
+++ b/src/plugins/impact/gui/register_gui.ml
@@ -22,7 +22,6 @@
open Pretty_source
open Gtk_helper
-open Db
open Cil_types
module SelectedStmt = struct
@@ -43,7 +42,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:SelectedStmt.self
- [ !Db.Pdg.self ])
+ [ Pdg.Api.self ])
module Highlighted_stmt : sig
val add: Kernel_function.t -> stmt -> unit
@@ -232,7 +231,7 @@ let pp_impact_on_inputs (main_ui:Design.main_window_extension_points) kf =
let call, formals, zones =
Pdg_aux.NS.fold
(fun (node, z) (call, formals, zones as acc) ->
- match !Pdg.node_key node with
+ match Pdg.Api.node_key node with
| SigCallKey _ | CallStmt _ | Stmt _ | Label _ ->
acc (* Related to one stmt: skip *)
| VarDecl _ -> acc (* skip *)
@@ -268,7 +267,7 @@ let pp_impacted_call_outputs
let ret, zones =
Pdg_aux.NS.fold
(fun (node, z) (ret, zones as acc) ->
- match !Pdg.node_key node with
+ match Pdg.Api.node_key node with
| SigCallKey (stmt', key)
when Cil_datatype.Stmt.equal call_stmt stmt' ->
(match key with
diff --git a/src/plugins/impact/pdg_aux.ml b/src/plugins/impact/pdg_aux.ml
index 8513bcf2411..c36b4d651b9 100644
--- a/src/plugins/impact/pdg_aux.ml
+++ b/src/plugins/impact/pdg_aux.ml
@@ -159,7 +159,7 @@ let find_call_input_nodes pdg_caller call_stmt ?(z=Locations.Zone.top) in_key =
(* skip undef zone: any result different from None is due to calldeps or
some imprecision. *)
let nodes, _undef =
- !Db.Pdg.find_location_nodes_at_stmt
+ Pdg.Api.find_location_nodes_at_stmt
pdg_caller call_stmt ~before:true zone'
in
nodes
@@ -201,7 +201,7 @@ let all_call_out_nodes ~callee ~caller call_stmt =
in
let test_out acc (out_key, call_out_node) =
(* skip undef: any zone found undef is due to an imprecision or a bug*)
- let out_nodes, _ = !Db.Pdg.find_output_nodes callee out_key in
+ let out_nodes, _ = Pdg.Api.find_output_nodes callee out_key in
let out_nodes = node_list_to_set out_nodes in
(call_out_node, out_nodes) :: acc
in
diff --git a/src/plugins/impact/pdg_aux.mli b/src/plugins/impact/pdg_aux.mli
index 32e7f34d68c..fa3bcde2b5f 100644
--- a/src/plugins/impact/pdg_aux.mli
+++ b/src/plugins/impact/pdg_aux.mli
@@ -21,7 +21,6 @@
(**************************************************************************)
open Cil_types
-open PdgTypes
open Locations
(** Useful functions that are not directly accessible through the other
@@ -30,7 +29,7 @@ open Locations
(** Refinement of a PDG node: we add an indication of which zone is really
impacted *)
-type node = Node.t * Zone.t
+type node = PdgTypes.Node.t * Zone.t
val pretty_node: node Pretty_utils.formatter
@@ -53,9 +52,9 @@ module NS: sig
val inter: t -> t -> t
val diff: t -> t -> t
- val remove: Node.t -> t -> t
+ val remove: PdgTypes.Node.t -> t -> t
- val mem: Node.t -> t -> bool
+ val mem: PdgTypes.Node.t -> t -> bool
val mem': node -> t -> bool
val intersects: t -> t -> bool
val for_all': (node -> bool) -> t -> bool
@@ -76,7 +75,7 @@ type call_interface = (PdgTypes.Node.t * NS.t) list
of [callee]. Each input node in [callee] is returned with the set
of nodes that define it in [caller]. *)
val all_call_input_nodes:
- caller:Db.Pdg.t -> callee:kernel_function * Db.Pdg.t -> stmt ->
+ caller:Pdg.Api.t -> callee:kernel_function * Pdg.Api.t -> stmt ->
call_interface
(** [all_call_out_nodes ~callee ~caller stmt] find all the nodes of [callee]
@@ -84,4 +83,4 @@ val all_call_input_nodes:
that occurs at [stmt]. Each such out node is returned, with the set
of nodes that define it in [callee] *)
val all_call_out_nodes :
- callee:Db.Pdg.t -> caller:Db.Pdg.t -> stmt -> call_interface
+ callee:Pdg.Api.t -> caller:Pdg.Api.t -> stmt -> call_interface
diff --git a/src/plugins/impact/reason_graph.ml b/src/plugins/impact/reason_graph.ml
index eceba7800cf..f3242116b75 100644
--- a/src/plugins/impact/reason_graph.ml
+++ b/src/plugins/impact/reason_graph.ml
@@ -216,7 +216,7 @@ let print_dot_graph reason =
(* Very basic textual debugging function *)
let _print_reason reason =
- let pp_node = !Db.Pdg.pretty_node false in
+ let pp_node = Pdg.Api.pretty_node false in
let pp fmt (nsrc, ndst, reason) =
Format.fprintf fmt "@[<v 2>%a -> %a (%s)@]"
pp_node nsrc pp_node ndst
diff --git a/src/plugins/pdg/Pdg.ml b/src/plugins/pdg/Pdg.ml
index 40d3a563379..4838045256c 100644
--- a/src/plugins/pdg/Pdg.ml
+++ b/src/plugins/pdg/Pdg.ml
@@ -22,7 +22,6 @@
(** Program Dependences Graph. *)
-(** Functions for this plugin are registered through the [Db] module,
- the dynamic API, and the module Below. *)
-
module Register = Register
+
+module Api = Api
diff --git a/src/plugins/pdg/Pdg.mli b/src/plugins/pdg/Pdg.mli
index 2fcfa888531..1ba848dc619 100644
--- a/src/plugins/pdg/Pdg.mli
+++ b/src/plugins/pdg/Pdg.mli
@@ -22,7 +22,6 @@
(** Program Dependences Graph. *)
-(** Functions for this plugin are registered through the [Db] module,
- the dynamic API, and the module Below. *)
-
module Register : module type of Marks
+
+module Api : module type of Api
diff --git a/src/plugins/pdg/annot.ml b/src/plugins/pdg/annot.ml
index d76dc95c38d..00b327ff190 100644
--- a/src/plugins/pdg/annot.ml
+++ b/src/plugins/pdg/annot.ml
@@ -117,13 +117,13 @@ let find_code_annot_nodes pdg stmt annot =
let labels = decl_label_info.Db.Properties.Interp.To_zone.lbl in
let stmt_key = Key.stmt_key stmt in
let stmt_node = match stmt_key with
- | Key.Stmt _ -> !Db.Pdg.find_stmt_node pdg stmt
- | Key.CallStmt _ -> !Db.Pdg.find_call_ctrl_node pdg stmt
+ | Key.Stmt _ -> Sets.find_stmt_node pdg stmt
+ | Key.CallStmt _ -> Sets.find_call_ctrl_node pdg stmt
| _ -> assert false
in
- let ctrl_dpds = !Db.Pdg.direct_ctrl_dpds pdg stmt_node in
+ let ctrl_dpds = Sets.direct_ctrl_dpds pdg stmt_node in
let add_stmt_nodes s acc =
- try !Db.Pdg.find_stmt_and_blocks_nodes pdg s @ acc
+ try Sets.find_stmt_and_blocks_nodes pdg s @ acc
with Not_found -> acc
in
(* can safely ignore pragmas.ctrl
diff --git a/src/plugins/pdg/api.ml b/src/plugins/pdg/api.ml
new file mode 100644
index 00000000000..2dcc57f4a5c
--- /dev/null
+++ b/src/plugins/pdg/api.ml
@@ -0,0 +1,111 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+[@@@ warning "-32" ]
+
+type t = PdgTypes.Pdg.t
+
+type t_nodes_and_undef =
+ ((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
+
+exception Top = PdgTypes.Pdg.Top
+exception Bottom = PdgTypes.Pdg.Bottom
+
+(**************************************************************************)
+
+let self = Pdg_tbl.self
+let get = Pdg_tbl.get
+
+let node_key = PdgTypes.Node.elem_key
+
+let from_same_fun pdg1 pdg2 =
+ let kf1 = PdgTypes.Pdg.get_kf pdg1 in
+ let kf2 = PdgTypes.Pdg.get_kf pdg2 in
+ Kernel_function.equal kf1 kf2
+
+(**************************************************************************)
+let find_decl_var_node = Sets.find_decl_var_node
+let find_entry_point_node = Sets.find_entry_point_node
+let find_top_input_node = Sets.find_top_input_node
+let find_simple_stmt_nodes = Sets.find_simple_stmt_nodes
+let find_stmt_and_blocks_nodes = Sets.find_stmt_and_blocks_nodes
+let find_stmt_node = Sets.find_stmt_node
+let find_label_node = Sets.find_label_node
+let find_location_nodes_at_stmt = Sets.find_location_nodes_at_stmt
+let find_location_nodes_at_begin = Sets.find_location_nodes_at_begin
+let find_location_nodes_at_end = Sets.find_location_nodes_at_end
+let find_call_ctrl_node = Sets.find_call_ctrl_node
+let find_call_input_node = Sets.find_call_num_input_node
+let find_call_output_node = Sets.find_call_output_node
+let find_input_node = Sets.find_input_node
+let find_ret_output_node = Sets.find_output_node
+let find_output_nodes = Sets.find_output_nodes
+let find_all_inputs_nodes = Sets.find_all_input_nodes
+
+let find_call_stmts = Sets.find_call_stmts
+
+let find_code_annot_nodes = Annot.find_code_annot_nodes
+let find_fun_precond_nodes = Annot.find_fun_precond_nodes
+let find_fun_postcond_nodes = Annot.find_fun_postcond_nodes
+let find_fun_variant_nodes = Annot.find_fun_variant_nodes
+
+let find_call_out_nodes_to_select = Sets.find_call_out_nodes_to_select
+let find_in_nodes_to_select_for_this_call =
+ Sets.find_in_nodes_to_select_for_this_call
+
+(**************************************************************************)
+
+let direct_dpds = Sets.direct_dpds
+let direct_ctrl_dpds = Sets.direct_ctrl_dpds
+let direct_data_dpds = Sets.direct_data_dpds
+let direct_addr_dpds = Sets.direct_addr_dpds
+
+let all_dpds = Sets.find_nodes_all_dpds
+let all_ctrl_dpds = Sets.find_nodes_all_ctrl_dpds
+let all_data_dpds = Sets.find_nodes_all_data_dpds
+let all_addr_dpds = Sets.find_nodes_all_addr_dpds
+
+let direct_uses = Sets.direct_uses
+let direct_ctrl_uses = Sets.direct_ctrl_uses
+let direct_data_uses = Sets.direct_data_uses
+let direct_addr_uses = Sets.direct_addr_uses
+
+let all_uses = Sets.all_uses
+
+let custom_related_nodes = Sets.custom_related_nodes
+
+let iter_nodes = PdgTypes.Pdg.iter_nodes
+
+(**************************************************************************)
+
+
+let extract = Pdg_tbl.print_dot
+
+let pretty_node = Pdg_tbl.pretty_node
+let pretty_key = Pdg_tbl.pretty_key
+let pretty = Pdg_tbl.pretty
+
+(**************************************************************************)
+
+module Marks = Marks
+
+(**************************************************************************)
diff --git a/src/plugins/pdg/api.mli b/src/plugins/pdg/api.mli
new file mode 100644
index 00000000000..c0a8fcf858c
--- /dev/null
+++ b/src/plugins/pdg/api.mli
@@ -0,0 +1,350 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+type t = PdgTypes.Pdg.t
+(** Program Dependence Graph type *)
+
+type t_nodes_and_undef =
+ ((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
+(** type for the return value of many [find_xxx] functions when the
+ answer can be a list of [(node, z_part)] and an [undef zone].
+ For each node, [z_part] can specify which part of the node
+ is used in terms of zone ([None] means all). *)
+
+(**************************************************************************)
+
+exception Bottom
+(** Raised by most function when the PDG is Bottom because we can hardly do
+ nothing with it. It happens when the function is unreachable because we
+ have no information about it. *)
+
+exception Top
+(** Raised by most function when the PDG is Top because we can hardly do
+ nothing with it. It happens when we didn't manage to compute it, for
+ instance for a variadic function. *)
+
+(**************************************************************************)
+
+val self : State.t
+(** PDG depedency state *)
+
+(**************************************************************************)
+
+(** {3 Getters} *)
+
+val get : Cil_types.kernel_function -> t
+(** Get the PDG of a function. Build it if it doesn't exist yet. *)
+
+val node_key : PdgTypes.Node.t -> PdgIndex.Key.t
+
+val from_same_fun : t -> t -> bool
+
+(**************************************************************************)
+
+(** {Finding PDG nodes} *)
+
+val find_decl_var_node : t -> Cil_types.varinfo -> PdgTypes.Node.t
+(** Get the node corresponding the declaration of a local variable or a
+ formal parameter.
+ @raise Not_found if the variable is not declared in this function.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_ret_output_node : t -> PdgTypes.Node.t
+(** Get the node corresponding return stmt.
+ @raise Not_found if the output state in unreachable
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_output_nodes : t -> PdgIndex.Signature.out_key -> t_nodes_and_undef
+(** Get the nodes corresponding to a call output key in the called pdg.
+ @raise Not_found if the output state in unreachable
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_input_node : t -> int -> PdgTypes.Node.t
+(** Get the node corresponding to a given input (parameter).
+ @raise Not_found if the number is not an input number.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_all_inputs_nodes : t -> PdgTypes.Node.t list
+(** Get the nodes corresponding to all inputs.
+ {!node_key} can be used to know their numbers.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_stmt_node : t -> Cil_types.stmt -> PdgTypes.Node.t
+(** Get the node corresponding to the statement.
+ It shouldn't be a call statement.
+ See also {!find_simple_stmt_nodes} or {!find_call_stmts}.
+ @raise Not_found if the given statement is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top.
+ @raise PdgIndex.CallStatement if the given stmt is a function
+ call. *)
+
+
+val find_simple_stmt_nodes : t -> Cil_types.stmt -> PdgTypes.Node.t list
+(** Get the nodes corresponding to the statement.
+ It is usually composed of only one node (see {!find_stmt_node}),
+ except for call statement.
+ Be careful that for block statements, it only returns a node
+ corresponding to the elementary stmt
+ (see {!find_stmt_and_blocks_nodes} for more)
+ @raise Not_found if the given statement is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_label_node : t -> Cil_types.stmt -> Cil_types.label -> PdgTypes.Node.t
+(** Get the node corresponding to the label.
+ @raise Not_found if the given label is not in the PDG.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_stmt_and_blocks_nodes : t -> Cil_types.stmt -> PdgTypes.Node.t list
+(** Get the nodes corresponding to the statement like
+ {!find_simple_stmt_nodes} but also add the nodes of the enclosed
+ statements if [stmt] contains blocks.
+ @raise Not_found if the given statement is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_top_input_node : t -> PdgTypes.Node.t
+(** @raise Not_found if there is no top input in the PDG.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_entry_point_node : t -> PdgTypes.Node.t
+(** Find the node that represent the entry point of the function, i.e. the
+ higher level block.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_location_nodes_at_stmt : t -> Cil_types.stmt -> before:bool ->
+ Locations.Zone.t -> t_nodes_and_undef
+(** Find the nodes that define the value of the location at the given
+ program point. Also return a zone that might be undefined at that point.
+ @raise Not_found if the given statement is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_location_nodes_at_end : t -> Locations.Zone.t -> t_nodes_and_undef
+(** Same than {!find_location_nodes_at_stmt} for the program point located
+ at the end of the function.
+ @raise Not_found if the output state is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_location_nodes_at_begin : t -> Locations.Zone.t -> t_nodes_and_undef
+(** Same than {!find_location_nodes_at_stmt} for the program point located
+ at the beginning of the function.
+ Notice that it can only find formal argument nodes.
+ The remaining zone (implicit input) is returned as undef.
+ @raise Not_found if the output state is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_call_stmts : Cil_types.kernel_function ->
+ caller:Cil_types.kernel_function -> Cil_types.stmt list
+(** Find the call statements to the function (can maybe be somewhere
+ else).
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_call_ctrl_node : t -> Cil_types.stmt -> PdgTypes.Node.t
+(** @raise Not_found if the call is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_call_input_node : t -> Cil_types.stmt -> int -> PdgTypes.Node.t
+(** @raise Not_found if the call is unreachable or has no such input.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_call_output_node : t -> Cil_types.stmt -> PdgTypes.Node.t
+(** @raise Not_found if the call is unreachable or has no output node.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_code_annot_nodes : t -> Cil_types.stmt ->
+ Cil_types.code_annotation ->
+ PdgTypes.Node.t list * PdgTypes.Node.t list * (t_nodes_and_undef option)
+(** The result is composed of three parts :
+ - the first part of the result are the control dependencies nodes
+ of the annotation,
+ - the second part is the list of declaration nodes of the variables
+ used in the annotation;
+ - the third part is similar to [find_location_nodes_at_stmt] result
+ but for all the locations needed by the annotation.
+ When the third part is globally [None],
+ it means that we were not able to compute this information.
+ @raise Not_found if the statement is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_fun_precond_nodes : t -> Cil_types.predicate ->
+ PdgTypes.Node.t list * (t_nodes_and_undef option)
+(** Similar to [find_code_annot_nodes] (no control dependencies nodes) *)
+
+val find_fun_postcond_nodes : t -> Cil_types.predicate ->
+ PdgTypes.Node.t list * (t_nodes_and_undef option)
+(** Similar to [find_fun_precond_nodes] *)
+
+val find_fun_variant_nodes : t -> Cil_types.term ->
+ PdgTypes.Node.t list * (t_nodes_and_undef option)
+(** Similar to [find_fun_precond_nodes] *)
+
+(**************************************************************************)
+
+(** {3 Propagation}
+ See also [Pdg.mli] for more function that cannot be here because
+ they use polymorphic types. **)
+
+val find_call_out_nodes_to_select :
+ t -> PdgTypes.NodeSet.t -> t -> Cil_types.stmt -> PdgTypes.Node.t list
+(** [find_call_out_nodes_to_select pdg_called called_selected_nodes
+ pdg_caller call_stmt]
+ @return the call outputs nodes [out] such that
+ [find_output_nodes pdg_called out_key]
+ intersects [called_selected_nodes]. *)
+
+val find_in_nodes_to_select_for_this_call :
+ t -> PdgTypes.NodeSet.t -> Cil_types.stmt -> t -> PdgTypes.Node.t list
+(** [find_in_nodes_to_select_for_this_call
+ pdg_caller caller_selected_nodes call_stmt pdg_called]
+ @return the called input nodes such that the corresponding nodes
+ in the caller intersect [caller_selected_nodes]
+ @raise Not_found if the statement is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+(**************************************************************************)
+
+(** {3 Dependencies} *)
+
+val direct_dpds : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Get the nodes to which the given node directly depend on.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_ctrl_dpds : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Similar to {!direct_dpds}, but for control dependencies only.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_data_dpds : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Similar to {!direct_dpds}, but for data dependencies only.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_addr_dpds : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Similar to {!direct_dpds}, but for address dependencies only.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val all_dpds : t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
+(** Transitive closure of {!direct_dpds} for all the given nodes.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val all_data_dpds : t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
+(** Gives the data dependencies of the given nodes, and recursively, all
+ the dependencies of those nodes (regardless to their kind).
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val all_ctrl_dpds : t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
+(** Similar to {!all_data_dpds} for control dependencies.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val all_addr_dpds : t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
+(** Similar to {!all_data_dpds} for address dependencies.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_uses : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** build a list of all the nodes that have direct dependencies on the
+ given node.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_ctrl_uses : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Similar to {!direct_uses}, but for control dependencies only.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_data_uses : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Similar to {!direct_uses}, but for data dependencies only.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_addr_uses : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Similar to {!direct_uses}, but for address dependencies only.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val all_uses : t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
+(** build a list of all the nodes that have dependencies (even indirect) on
+ the given nodes.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val custom_related_nodes : (PdgTypes.Node.t -> PdgTypes.Node.t list) ->
+ PdgTypes.Node.t list -> PdgTypes.Node.t list
+(** [custom_related_nodes get_dpds node_list] build a list, starting from
+ the node in [node_list], and recursively add the nodes given by the
+ function [get_dpds]. For this function to work well, it is important
+ that [get_dpds n] returns a subset of the nodes directly related to
+ [n], ie a subset of [direct_uses] U [direct_dpds].
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val iter_nodes : (PdgTypes.Node.t -> unit) -> t -> unit
+(** apply a given function to all the PDG nodes
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+(**************************************************************************)
+
+(** {3 Printers} *)
+
+val extract : t -> string -> unit
+(** Pretty print pdg into a dot file. *)
+
+val pretty_node : bool -> Format.formatter -> PdgTypes.Node.t -> unit
+(** Pretty print information on a node : with [short=true], only the id
+ of the node is printed.. *)
+
+val pretty_key : Format.formatter -> PdgIndex.Key.t -> unit
+(** Pretty print information on a node key *)
+
+val pretty : ?bw:bool -> Format.formatter -> t -> unit
+(** For debugging... Pretty print pdg information.
+ Print codependencies rather than dependencies if [bw=true]. *)
+
+(**************************************************************************)
+
+module Marks : module type of Marks
+
+(**************************************************************************)
diff --git a/src/plugins/pdg/marks.ml b/src/plugins/pdg/marks.ml
index 272b5b1ad9f..520249051f0 100644
--- a/src/plugins/pdg/marks.ml
+++ b/src/plugins/pdg/marks.ml
@@ -36,12 +36,12 @@ let in_marks_to_caller pdg call m2m ?(rqs=[]) in_marks =
let build rqs (in_key, m) =
match in_key with
| Signature.InCtrl ->
- add_n_m rqs (!Db.Pdg.find_call_ctrl_node pdg call) None m
+ add_n_m rqs (Sets.find_call_ctrl_node pdg call) None m
| Signature.InNum in_num ->
- add_n_m rqs (!Db.Pdg.find_call_input_node pdg call in_num) None m
+ add_n_m rqs (Sets.find_call_num_input_node pdg call in_num) None m
| Signature.InImpl zone ->
let nodes, undef =
- !Db.Pdg.find_location_nodes_at_stmt pdg call ~before:true zone
+ Sets.find_location_nodes_at_stmt pdg call ~before:true zone
in
let rqs =
List.fold_left (fun acc (n,z) -> add_n_m acc n z m) rqs nodes in
@@ -64,10 +64,10 @@ let translate_in_marks pdg_called in_new_marks
in_marks_to_caller pdg call (m2m (Some call) pdg) ~rqs in_new_marks
in
let build rqs caller =
- let pdg_caller = !Db.Pdg.get caller in
+ let pdg_caller = Pdg_tbl.get caller in
let caller_rqs =
try
- let call_stmts = !Db.Pdg.find_call_stmts ~caller kf_called in
+ let call_stmts = Sets.find_call_stmts ~caller kf_called in
(* TODO : more intelligent merge ? *)
let rqs = List.fold_left (translate pdg_caller) [] call_stmts in
PdgMarks.SelList rqs
@@ -98,7 +98,7 @@ let call_out_marks_to_called called_pdg m2m ?(rqs=[]) out_marks =
let translate_out_mark _pdg m2m other_rqs (call, l) =
let add_list l_out_m rqs called_kf =
- let called_pdg = !Db.Pdg.get called_kf in
+ let called_pdg = Pdg_tbl.get called_kf in
let m2m = m2m (Some call) called_pdg in
try
let node_marks =
@@ -165,7 +165,7 @@ module F_Proj (C : PdgMarks.Config) :
let fct_var = Kernel_function.get_vi kf in
try Varinfo.Hashtbl.find proj fct_var
with Not_found ->
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg_tbl.get kf in
let info = F.create pdg in
Varinfo.Hashtbl.add proj fct_var info;
info
diff --git a/src/plugins/pdg/pdg_tbl.ml b/src/plugins/pdg/pdg_tbl.ml
new file mode 100644
index 00000000000..4961d4154bd
--- /dev/null
+++ b/src/plugins/pdg/pdg_tbl.ml
@@ -0,0 +1,59 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+type t = PdgTypes.Pdg.t
+
+(**************************************************************************)
+
+let compute = Build.compute_pdg
+
+module Tbl =
+ Kernel_function.Make_Table
+ (PdgTypes.Pdg)
+ (struct
+ let name = "Pdg.State"
+ let dependencies = [] (* postponed because !Db.From.self may
+ not exist yet *)
+ let size = 17
+ end)
+
+let self = Tbl.self
+let get = Tbl.memo compute
+
+(**************************************************************************)
+
+let pretty ?(bw=false) fmt pdg =
+ let kf = PdgTypes.Pdg.get_kf pdg in
+ Format.fprintf fmt "@[RESULT for %s:@]@\n@[ %a@]"
+ (Kernel_function.get_name kf) (PdgTypes.Pdg.pretty_bw ~bw) pdg
+
+let pretty_node short =
+ if short then PdgTypes.Node.pretty
+ else PdgTypes.Node.pretty_node
+
+let print_dot pdg filename =
+ PdgTypes.Pdg.build_dot filename pdg;
+ Pdg_parameters.feedback "dot file generated in %s" filename
+
+let pretty_key = PdgIndex.Key.pretty
+
+(**************************************************************************)
diff --git a/src/plugins/pdg/pdg_tbl.mli b/src/plugins/pdg/pdg_tbl.mli
new file mode 100644
index 00000000000..73bfa5d76ef
--- /dev/null
+++ b/src/plugins/pdg/pdg_tbl.mli
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+type t = PdgTypes.Pdg.t
+
+val self : State.t
+
+val get : Cil_types.kernel_function -> t
+(** Get the PDG of a function. Build it if it doesn't exist yet. *)
+
+(** {3 Pretty printing} *)
+
+val pretty_node : bool -> Format.formatter -> PdgTypes.Node.t -> unit
+(** Pretty print information on a node : with [short=true], only the id
+ of the node is printed.. *)
+
+val pretty_key : Format.formatter -> PdgIndex.Key.t -> unit
+(** Pretty print information on a node key *)
+
+val pretty : ?bw:bool -> Format.formatter -> t -> unit
+(** For debugging... Pretty print pdg information.
+ Print codependencies rather than dependencies if [bw=true]. *)
+
+val print_dot : t -> string -> unit
+(** Pretty print pdg into a dot file. *)
diff --git a/src/plugins/pdg/register.ml b/src/plugins/pdg/register.ml
index 4f707e7ffeb..ccce4b10491 100644
--- a/src/plugins/pdg/register.ml
+++ b/src/plugins/pdg/register.ml
@@ -20,104 +20,20 @@
(* *)
(**************************************************************************)
-let compute = Build.compute_pdg
-
-let pretty ?(bw=false) fmt pdg =
- let kf = PdgTypes.Pdg.get_kf pdg in
- Format.fprintf fmt "@[RESULT for %s:@]@\n@[ %a@]"
- (Kernel_function.get_name kf) (PdgTypes.Pdg.pretty_bw ~bw) pdg
-
-let pretty_node short =
- if short then PdgTypes.Node.pretty
- else PdgTypes.Node.pretty_node
-
-let print_dot pdg filename =
- PdgTypes.Pdg.build_dot filename pdg;
- Pdg_parameters.feedback "dot file generated in %s" filename
-
-module Tbl =
- Kernel_function.Make_Table
- (PdgTypes.Pdg)
- (struct
- let name = "Pdg.State"
- let dependencies = [] (* postponed because !Db.From.self may
- not exist yet *)
- let size = 17
- end)
let () =
Cmdline.run_after_extended_stage
(fun () ->
State_dependency_graph.add_codependencies
- ~onto:Tbl.self
+ ~onto:Pdg_tbl.self
[ !Db.From.self ])
-(** Register external functions into Db. *)
-let () =
- Db.Pdg.self := Tbl.self;
- Db.Pdg.get := Tbl.memo compute;
- Db.Pdg.node_key := PdgTypes.Node.elem_key;
-
- Db.Pdg.find_decl_var_node := Sets.find_decl_var_node;
- Db.Pdg.find_entry_point_node := Sets.find_entry_point_node;
- Db.Pdg.find_top_input_node := Sets.find_top_input_node;
- Db.Pdg.find_simple_stmt_nodes := Sets.find_simple_stmt_nodes;
- Db.Pdg.find_stmt_and_blocks_nodes := Sets.find_stmt_and_blocks_nodes;
- Db.Pdg.find_stmt_node := Sets.find_stmt_node;
- Db.Pdg.find_label_node := Sets.find_label_node;
- Db.Pdg.find_location_nodes_at_stmt := Sets.find_location_nodes_at_stmt;
- Db.Pdg.find_location_nodes_at_begin := Sets.find_location_nodes_at_begin;
- Db.Pdg.find_location_nodes_at_end := Sets.find_location_nodes_at_end;
- Db.Pdg.find_call_ctrl_node := Sets.find_call_ctrl_node;
- Db.Pdg.find_call_input_node := Sets.find_call_num_input_node;
- Db.Pdg.find_call_output_node := Sets.find_call_output_node;
- Db.Pdg.find_input_node := Sets.find_input_node;
- Db.Pdg.find_ret_output_node := Sets.find_output_node;
- Db.Pdg.find_output_nodes := Sets.find_output_nodes;
- Db.Pdg.find_all_inputs_nodes := Sets.find_all_input_nodes;
-
- Db.Pdg.find_call_stmts := Sets.find_call_stmts;
-
- Db.Pdg.find_code_annot_nodes := Annot.find_code_annot_nodes;
- Db.Pdg.find_fun_precond_nodes := Annot.find_fun_precond_nodes;
- Db.Pdg.find_fun_postcond_nodes := Annot.find_fun_postcond_nodes;
-
- Db.Pdg.find_call_out_nodes_to_select := Sets.find_call_out_nodes_to_select;
- Db.Pdg.find_in_nodes_to_select_for_this_call :=
- Sets.find_in_nodes_to_select_for_this_call;
-
- Db.Pdg.direct_dpds := Sets.direct_dpds;
- Db.Pdg.direct_ctrl_dpds := Sets.direct_ctrl_dpds;
- Db.Pdg.direct_data_dpds := Sets.direct_data_dpds;
- Db.Pdg.direct_addr_dpds := Sets.direct_addr_dpds;
-
- Db.Pdg.all_dpds := Sets.find_nodes_all_dpds;
- Db.Pdg.all_ctrl_dpds := Sets.find_nodes_all_ctrl_dpds;
- Db.Pdg.all_data_dpds := Sets.find_nodes_all_data_dpds;
- Db.Pdg.all_addr_dpds := Sets.find_nodes_all_addr_dpds;
-
- Db.Pdg.direct_uses := Sets.direct_uses;
- Db.Pdg.direct_ctrl_uses := Sets.direct_ctrl_uses;
- Db.Pdg.direct_data_uses := Sets.direct_data_uses;
- Db.Pdg.direct_addr_uses := Sets.direct_addr_uses;
-
- Db.Pdg.all_uses := Sets.all_uses;
-
- Db.Pdg.custom_related_nodes := Sets.custom_related_nodes;
-
- Db.Pdg.iter_nodes := PdgTypes.Pdg.iter_nodes;
-
- Db.Pdg.pretty := pretty ;
- Db.Pdg.pretty_node := pretty_node ;
- Db.Pdg.pretty_key := PdgIndex.Key.pretty;
- Db.Pdg.extract := print_dot
-
(* This module contains polymorphic functions : cannot be registered in Db.
Can be used through Pdg.Register instead (see Pdg.mli) *)
include Marks
let deps =
- [!Db.Pdg.self; Pdg_parameters.BuildAll.self; Pdg_parameters.BuildFct.self]
+ [Pdg_tbl.self; Pdg_parameters.BuildAll.self; Pdg_parameters.BuildFct.self]
let () = Pdg_parameters.BuildAll.set_output_dependencies deps
@@ -130,11 +46,11 @@ let compute () =
Eva.Analysis.compute ();
let do_kf_pdg kf =
if compute_for_kf kf then
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg_tbl.get kf in
let dot_basename = Pdg_parameters.DotBasename.get () in
if dot_basename <> "" then
let fname = Kernel_function.get_name kf in
- !Db.Pdg.extract pdg (dot_basename ^ "." ^ fname ^ ".dot")
+ Pdg_tbl.print_dot pdg (dot_basename ^ "." ^ fname ^ ".dot")
in
Callgraph.Uses.iter_in_rev_order do_kf_pdg;
let pp_sep fmt () = Format.pp_print_string fmt "," in
@@ -151,7 +67,7 @@ let output () =
let bw = Pdg_parameters.PrintBw.get () in
let do_kf_pdg kf =
if compute_for_kf kf then
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg_tbl.get kf in
let header fmt =
Format.fprintf fmt "PDG for %a" Kernel_function.pretty kf
in
diff --git a/src/plugins/postdominators/print.ml b/src/plugins/postdominators/print.ml
index 6ff5e94dd08..99549e4fb68 100644
--- a/src/plugins/postdominators/print.ml
+++ b/src/plugins/postdominators/print.ml
@@ -24,7 +24,7 @@ open Cil_types
open Cil_datatype
let pretty_stmt fmt s =
- let key = PdgIndex.Key.stmt_key s in !Db.Pdg.pretty_key fmt key
+ let key = PdgIndex.Key.stmt_key s in PdgIndex.Key.pretty fmt key
module Printer = struct
diff --git a/src/plugins/scope/defs.ml b/src/plugins/scope/defs.ml
index 2e7fbdbdf86..a73ef647869 100644
--- a/src/plugins/scope/defs.ml
+++ b/src/plugins/scope/defs.ml
@@ -60,19 +60,19 @@ let _pp_set prefix fmt =
let rec add_callee_nodes z acc nodes =
let new_nodes, acc = NSet.fold
(fun node acc2 ->
- match !Db.Pdg.node_key node with
+ match Pdg.Api.node_key node with
| PdgIndex.Key.SigCallKey (cid, PdgIndex.Signature.Out out_key) ->
let callees = Eva.Results.callee (PdgIndex.Key.call_from_id cid) in
List.fold_left (fun (new_nodes, acc) kf ->
- let callee_pdg = !Db.Pdg.get kf in
+ let callee_pdg = Pdg.Api.get kf in
let outputs = match out_key with
| PdgIndex.Signature.OutLoc out ->
(* [out] might be an over-approximation of the location
we are searching for. We refine the search if needed. *)
let z = Locations.Zone.narrow out z in
- fst (!Db.Pdg.find_location_nodes_at_end callee_pdg z)
+ fst (Pdg.Api.find_location_nodes_at_end callee_pdg z)
| PdgIndex.Signature.OutRet -> (* probably never occurs *)
- fst (!Db.Pdg.find_output_nodes callee_pdg out_key)
+ fst (Pdg.Api.find_output_nodes callee_pdg out_key)
in
let outputs = List.map fst outputs in
add_list_to_set outputs new_nodes, add_list_to_set outputs acc)
@@ -99,25 +99,25 @@ let rec add_caller_nodes z kf acc (undef, nodes) =
| None -> acc_undef, acc
| Some undef ->
let nodes_for_undef, undef' =
- !Db.Pdg.find_location_nodes_at_stmt pdg stmt ~before:true undef
+ Pdg.Api.find_location_nodes_at_stmt pdg stmt ~before:true undef
in
let acc_undef = join_undef acc_undef undef' in
let acc = add_list_to_set (List.map fst nodes_for_undef) acc in
acc_undef, acc
in
let add_call_input_nodes node (acc_undef, acc) =
- match !Db.Pdg.node_key node with
+ match Pdg.Api.node_key node with
| PdgIndex.Key.SigKey (PdgIndex.Signature.In in_key) ->
begin match in_key with
| PdgIndex.Signature.InCtrl ->
(* We only look for the values *)
acc_undef, acc
| PdgIndex.Signature.InNum n_param ->
- let n = !Db.Pdg.find_call_input_node pdg stmt n_param in
+ let n = Pdg.Api.find_call_input_node pdg stmt n_param in
acc_undef, NSet.add n acc
| PdgIndex.Signature.InImpl z' ->
let z = Locations.Zone.narrow z z' in
- let nodes, undef'= !Db.Pdg.find_location_nodes_at_stmt
+ let nodes, undef'= Pdg.Api.find_location_nodes_at_stmt
pdg stmt ~before:true z
in
let acc_undef = join_undef acc_undef undef' in
@@ -128,7 +128,7 @@ let rec add_caller_nodes z kf acc (undef, nodes) =
NSet.fold add_call_input_nodes nodes (acc_undef, acc)
in
let add_one_caller_nodes acc (kf, stmts) =
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let acc_undef, caller_nodes =
List.fold_left (add_one_call_nodes pdg) (None, NSet.empty) stmts
in add_caller_nodes z kf (NSet.union caller_nodes acc) (acc_undef, caller_nodes)
@@ -138,9 +138,9 @@ let compute_aux kf stmt zone =
debug1 "[Defs.compute] for %a at sid:%d in '%a'@."
Locations.Zone.pretty zone stmt.sid Kernel_function.pretty kf;
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let nodes, undef =
- !Db.Pdg.find_location_nodes_at_stmt pdg stmt ~before:true zone
+ Pdg.Api.find_location_nodes_at_stmt pdg stmt ~before:true zone
in
let nodes = add_list_to_set (List.map fst nodes) NSet.empty in
let nodes =
@@ -152,13 +152,13 @@ let compute_aux kf stmt zone =
else nodes
in
Some (nodes, undef)
- with Db.Pdg.Bottom | Db.Pdg.Top | Not_found ->
+ with Pdg.Api.Bottom | Pdg.Api.Top | Not_found ->
None
let compute kf stmt lval =
let extract (nodes, undef) =
let add_node node defs =
- match PdgIndex.Key.stmt (!Db.Pdg.node_key node) with
+ match PdgIndex.Key.stmt (Pdg.Api.node_key node) with
| None -> defs
| Some s -> Stmt.Hptset.add s defs
in
@@ -185,7 +185,7 @@ let compute_with_def_type_zone kf stmt zone =
let after = (direct || prev_d, indirect || pred_i) in
Stmt.Map.add stmt after acc
in
- match !Db.Pdg.node_key node with
+ match Pdg.Api.node_key node with
| PdgIndex.Key.Stmt s -> change s (true, false)
| PdgIndex.Key.CallStmt _ -> assert false
| PdgIndex.Key.SigCallKey (s, sign) ->
diff --git a/src/plugins/scope/dune b/src/plugins/scope/dune
index 95c81426d4f..82e4e62e600 100644
--- a/src/plugins/scope/dune
+++ b/src/plugins/scope/dune
@@ -27,6 +27,7 @@
(echo "Scope:" %{lib-available:frama-c-scope.core} "\n")
(echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
(echo " - Inout:" %{lib-available:frama-c-inout.core} "\n")
+ (echo " - Pdg:" %{lib-available:frama-c-pdg.core} "\n")
)
)
)
@@ -36,7 +37,7 @@
(optional)
(public_name frama-c-scope.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-eva.core frama-c-inout.core)
+ (libraries frama-c.kernel frama-c-eva.core frama-c-inout.core frama-c-pdg.core)
)
(plugin (optional) (name scope) (libraries frama-c-scope.core) (site (frama-c plugins)))
diff --git a/src/plugins/scope/zones.ml b/src/plugins/scope/zones.ml
index aa02df158d8..bc98607ed33 100644
--- a/src/plugins/scope/zones.ml
+++ b/src/plugins/scope/zones.ml
@@ -262,7 +262,7 @@ let compute_ctrl_info pdg ctrl_part used_stmts =
let module CtrlCompute = Dataflow2.Backwards(CtrlComputer) in
let seen = Stmt.Hashtbl.create 50 in
let rec add_node_ctrl_nodes new_stmts node =
- let ctrl_nodes = !Db.Pdg.direct_ctrl_dpds pdg node in
+ let ctrl_nodes = Pdg.Api.direct_ctrl_dpds pdg node in
List.fold_left add_ctrl_node new_stmts ctrl_nodes
and add_ctrl_node new_stmts ctrl_node =
debug2 "[zones] add ctrl node %a@." PdgTypes.Node.pretty ctrl_node;
@@ -287,7 +287,7 @@ let compute_ctrl_info pdg ctrl_part used_stmts =
if Stmt.Hashtbl.mem seen stmt then new_stmts
else begin
Stmt.Hashtbl.add seen stmt ();
- match !Db.Pdg.find_simple_stmt_nodes pdg stmt with
+ match Pdg.Api.find_simple_stmt_nodes pdg stmt with
| [] -> []
| n::_ -> add_node_ctrl_nodes new_stmts n
end
@@ -323,7 +323,7 @@ let compute kf stmt lval =
let used_stmts = DataComputer.get_and_reset_used_stmts () in
let all_used_stmts =
if used_stmts = [] then []
- else compute_ctrl_info (!Db.Pdg.get kf) ctrl_part used_stmts
+ else compute_ctrl_info (Pdg.Api.get kf) ctrl_part used_stmts
in
let all_used_stmts =
List.fold_left
diff --git a/src/plugins/security_slicing/components.ml b/src/plugins/security_slicing/components.ml
index 629fa05f383..1b76f3467bb 100644
--- a/src/plugins/security_slicing/components.ml
+++ b/src/plugins/security_slicing/components.ml
@@ -98,7 +98,7 @@ let search_security_requirements () =
open PdgIndex
-let get_node_stmt node = Key.stmt (!Db.Pdg.node_key node)
+let get_node_stmt node = Key.stmt (Pdg.Api.node_key node)
module NodeKf = Datatype.Pair(PdgTypes.Node)(Kernel_function)
@@ -246,26 +246,26 @@ module Todolist : sig
type todo = private
{ node: PdgTypes.Node.t;
kf: kernel_function;
- pdg: Db.Pdg.t;
+ pdg: Pdg.Api.t;
callstack_length: int;
from_deep: bool }
type t = todo list
- val mk_init: kernel_function -> Db.Pdg.t -> PdgTypes.Node.t list -> todo list
+ val mk_init: kernel_function -> Pdg.Api.t -> PdgTypes.Node.t list -> todo list
val add:
- PdgTypes.Node.t -> kernel_function -> Db.Pdg.t -> int -> bool -> t -> t
+ PdgTypes.Node.t -> kernel_function -> Pdg.Api.t -> int -> bool -> t -> t
end = struct
type todo =
{ node: PdgTypes.Node.t;
kf: kernel_function;
- pdg: Db.Pdg.t;
+ pdg: Pdg.Api.t;
callstack_length: int;
from_deep: bool }
type t = todo list
let add n kf pdg len fd list =
- match !Db.Pdg.node_key n with
+ match Pdg.Api.node_key n with
| Key.SigKey (Signature.In Signature.InCtrl) ->
(* do not consider node [InCtrl] *)
list
@@ -276,7 +276,7 @@ end = struct
list
| _ ->
Security_slicing_parameters.debug ~level:2 "adding node %a (in %s)"
- (!Db.Pdg.pretty_node false) n
+ (Pdg.Api.pretty_node false) n
(Kernel_function.get_name kf);
{ node = n; kf = kf; pdg = pdg;
callstack_length = len; from_deep = fd }
@@ -301,7 +301,7 @@ module Component = struct
| Forward of fwd_kind
type value =
- { pdg: Db.Pdg.t;
+ { pdg: Pdg.Api.t;
mutable callstack_length: int;
mutable direct: bool;
mutable indirect_backward: bool;
@@ -356,15 +356,15 @@ module Component = struct
(* do not consider address dependencies now (except for impact analysis):
just consider them during the last slicing pass
(for semantic preservation of pointers) *)
- let direct node = !Db.Pdg.direct_data_dpds pdg node in
+ let direct node = Pdg.Api.direct_data_dpds pdg node in
match kind with
| Direct -> direct node
- | Indirect_Backward -> direct node @ !Db.Pdg.direct_ctrl_dpds pdg node
+ | Indirect_Backward -> direct node @ Pdg.Api.direct_ctrl_dpds pdg node
| Forward Security ->
- !Db.Pdg.direct_data_uses pdg node @ !Db.Pdg.direct_ctrl_uses pdg node
+ Pdg.Api.direct_data_uses pdg node @ Pdg.Api.direct_ctrl_uses pdg node
| Forward Impact ->
- !Db.Pdg.direct_data_uses pdg node @ !Db.Pdg.direct_ctrl_uses pdg node
- @ !Db.Pdg.direct_addr_uses pdg node
+ Pdg.Api.direct_data_uses pdg node @ Pdg.Api.direct_ctrl_uses pdg node
+ @ Pdg.Api.direct_addr_uses pdg node
let search_input kind kf lazy_l =
try
@@ -378,18 +378,18 @@ module Component = struct
[]
let add_from_deep caller todo n =
- Todolist.add n caller (!Db.Pdg.get caller) 0 true todo
+ Todolist.add n caller (Pdg.Api.get caller) 0 true todo
let forward_caller kf node todolist =
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
List.fold_left
(fun todolist (caller, callsites) ->
(* foreach caller *)
List.fold_left
(fun todolist callsite ->
let nodes =
- !Db.Pdg.find_call_out_nodes_to_select
- pdg (PdgTypes.NodeSet.singleton node) (!Db.Pdg.get caller) callsite
+ Pdg.Api.find_call_out_nodes_to_select
+ pdg (PdgTypes.NodeSet.singleton node) (Pdg.Api.get caller) callsite
in
List.fold_left
(add_from_deep caller)
@@ -420,7 +420,7 @@ module Component = struct
end else begin
Security_slicing_parameters.debug
~level:2 "considering node %a (in %s)"
- (!Db.Pdg.pretty_node false) node
+ (Pdg.Api.pretty_node false) node
(Kernel_function.get_name kf);
(* intraprocedural related_nodes *)
let related_nodes = one_step_related_nodes kind pdg node in
@@ -448,7 +448,7 @@ module Component = struct
for zone %a@." (Kernel_function.get_name kf)
(Kernel_function.get_name caller)
Locations.Zone.pretty zone;*)
- let pdg_caller = !Db.Pdg.get caller in
+ let pdg_caller = Pdg.Api.get caller in
let do_call todolist callsite =
match kind with
| Direct | Indirect_Backward ->
@@ -465,13 +465,13 @@ module Component = struct
todolist
in
let todolist =
- match !Db.Pdg.node_key node with
+ match Pdg.Api.node_key node with
| Key.SigKey (Signature.In Signature.InCtrl) ->
assert false
| Key.SigKey (Signature.In (Signature.InImpl zone)) ->
let compute_nodes pdg_caller callsite =
let nodes, _undef_zone =
- !Db.Pdg.find_location_nodes_at_stmt
+ Pdg.Api.find_location_nodes_at_stmt
pdg_caller callsite ~before:true zone
(* TODO : use undef_zone (see FS#201)? *)
in
@@ -484,9 +484,9 @@ module Component = struct
let compute_nodes pdg_caller callsite =
[ match key with
| Signature.In (Signature.InNum n) ->
- !Db.Pdg.find_call_input_node pdg_caller callsite n
+ Pdg.Api.find_call_input_node pdg_caller callsite n
| Signature.Out Signature.OutRet ->
- !Db.Pdg.find_call_output_node pdg_caller callsite
+ Pdg.Api.find_call_output_node pdg_caller callsite
| Signature.In
(Signature.InCtrl | Signature.InImpl _)
| Signature.Out _ ->
@@ -511,14 +511,14 @@ module Component = struct
"[security] search inside %s (from %s)@."
(Kernel_function.get_name called_kf)
(Kernel_function.get_name kf);*)
- let called_pdg = !Db.Pdg.get called_kf in
+ let called_pdg = Pdg.Api.get called_kf in
let nodes =
try
match kind, key with
| (Direct | Indirect_Backward),
Signature.Out out_key ->
let nodes, _undef_zone =
- !Db.Pdg.find_output_nodes called_pdg out_key
+ Pdg.Api.find_output_nodes called_pdg out_key
(* TODO: use undef_zone (see FS#201) *)
in
let nodes =
@@ -527,28 +527,28 @@ module Component = struct
nodes
| _, Signature.In (Signature.InNum n) ->
search_input kind called_kf
- (lazy [!Db.Pdg.find_input_node called_pdg n])
+ (lazy [Pdg.Api.find_input_node called_pdg n])
| _, Signature.In Signature.InCtrl ->
search_input kind called_kf
(lazy
- [!Db.Pdg.find_entry_point_node called_pdg])
+ [Pdg.Api.find_entry_point_node called_pdg])
| _, Signature.In (Signature.InImpl _) ->
assert false
| Forward _, Signature.Out _ ->
[]
with
- | Db.Pdg.Top ->
+ | Pdg.Api.Top ->
Security_slicing_parameters.warning
"no precise pdg for function %s. \n\
Ignoring this function in the analysis (potentially incorrect results)."
(Kernel_function.get_name called_kf);
[]
- | Db.Pdg.Bottom | Not_found -> assert false
+ | Pdg.Api.Bottom | Not_found -> assert false
in
List.fold_left
(fun todo n ->
(*Format.printf "node %a inside %s@."
- (!Db.Pdg.pretty_node false) n
+ (Pdg.Api.pretty_node false) n
(Kernel_function.get_name called_kf);*)
Todolist.add
n called_kf called_pdg
@@ -584,16 +584,16 @@ module Component = struct
let from_stmt = List.fold_left
(fun s n -> PdgTypes.NodeSet.add n s)
PdgTypes.NodeSet.empty from_stmt in
- let called_pdg = !Db.Pdg.get called_kf in
+ let called_pdg = Pdg.Api.get called_kf in
let nodes =
try
- !Db.Pdg.find_in_nodes_to_select_for_this_call
+ Pdg.Api.find_in_nodes_to_select_for_this_call
pdg from_stmt stmt called_pdg
with
- | Db.Pdg.Top ->
+ | Pdg.Api.Top ->
(* warning already emitted in the previous fold *)
[]
- | Db.Pdg.Bottom | Not_found -> assert false
+ | Pdg.Api.Bottom | Not_found -> assert false
in
List.fold_left
(fun todo n ->
@@ -623,10 +623,10 @@ module Component = struct
let initial_nodes kf stmt =
Security_slicing_parameters.debug
~level:3 "computing initial nodes for %d" stmt.sid;
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let nodes =
if Eva.Results.is_reachable stmt then
- try !Db.Pdg.find_simple_stmt_nodes pdg stmt
+ try Pdg.Api.find_simple_stmt_nodes pdg stmt
with Not_found -> assert false
else begin
Security_slicing_parameters.debug
@@ -654,7 +654,7 @@ module Component = struct
nodes
in
res
- with Db.Pdg.Top | Db.Pdg.Bottom ->
+ with Pdg.Api.Top | Pdg.Api.Bottom ->
Security_slicing_parameters.warning "PDG is not manageable. skipping.";
M.empty
@@ -665,7 +665,7 @@ module Component = struct
Security_slicing_parameters.debug
"computing backward indirect component for %d" stmt.sid;
related_nodes_of_nodes Indirect_Backward res nodes
- with Db.Pdg.Top | Db.Pdg.Bottom ->
+ with Pdg.Api.Top | Pdg.Api.Bottom ->
Security_slicing_parameters.warning "PDG is not manageable. skipping.";
M.empty
@@ -855,7 +855,7 @@ let slice ctrl =
let slicing = !Slicing.Project.mk_project name in
let select (n, kf) sel =
Security_slicing_parameters.debug ~level:2 "selecting %a (of %s)"
- (!Db.Pdg.pretty_node false) n
+ (Pdg.Api.pretty_node false) n
(Kernel_function.get_name kf);
!Slicing.Select.select_pdg_nodes
sel
diff --git a/src/plugins/security_slicing/dune b/src/plugins/security_slicing/dune
index 91009d8a819..4e24b20cfd4 100644
--- a/src/plugins/security_slicing/dune
+++ b/src/plugins/security_slicing/dune
@@ -26,6 +26,7 @@
(action (progn
(echo "Security Slicing:" %{lib-available:frama-c-security_slicing.core} "\n")
(echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ (echo " - Pdg:" %{lib-available:frama-c-pdg.core} "\n")
)
)
)
@@ -35,7 +36,7 @@
(optional)
(public_name frama-c-security_slicing.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-eva.core)
+ (libraries frama-c.kernel frama-c-eva.core frama-c-pdg.core)
)
(plugin (optional) (name security_slicing) (libraries frama-c-security_slicing.core) (site (frama-c plugins)))
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index b470412386a..0a25e41fe18 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -356,7 +356,7 @@ end = struct
let merge ff1 ff2 =
let pdg1, fm1 = ff1.SlicingInternals.ff_marks in
let pdg2, fm2 = ff2.SlicingInternals.ff_marks in
- assert (Db.Pdg.from_same_fun pdg1 pdg2) ;
+ assert (Pdg.Api.from_same_fun pdg1 pdg2) ;
let merge_marks m1 m2 = SlicingMarks.merge_marks [m1; m2] in
let merge_call_info _c1 _c2 = None in
let fm = PdgIndex.FctIndex.merge fm1 fm2 merge_marks merge_call_info in
@@ -418,7 +418,7 @@ end = struct
let m2m s m =
let key = match s with
| PdgMarks.SelIn loc -> PdgIndex.Key.implicit_in_key loc
- | PdgMarks.SelNode (n,_z) -> !Db.Pdg.node_key n
+ | PdgMarks.SelNode (n,_z) -> Pdg.Api.node_key n
in
let old_m = get_mark old_marks key in
let add_mark =
@@ -436,7 +436,7 @@ end = struct
SlicingParameters.debug ~level:2
"[Fct_Slice.FctMarks.marks_for_caller_inputs] for %a : \
old=%a new=%a -> %a"
- !Db.Pdg.pretty_key key SlicingMarks.pretty_mark old_m
+ Pdg.Api.pretty_key key SlicingMarks.pretty_mark old_m
SlicingMarks.pretty_mark m
SlicingMarks.pretty_mark
(match new_m with None -> SlicingMarks.bottom_mark | Some m -> m);
@@ -467,7 +467,7 @@ end = struct
let pdg = SlicingMacros.get_ff_pdg ff_call in
let spare = SlicingMarks.mk_gen_spare in
let rec add2 marks n =
- match !Db.Pdg.node_key n with
+ match Pdg.Api.node_key n with
| PdgIndex.Key.SigCallKey (_, (PdgIndex.Signature.In _)) ->
marks
| PdgIndex.Key.SigCallKey (_, (PdgIndex.Signature.Out key)) ->
@@ -497,7 +497,7 @@ end = struct
* it has already been taken into account in the "from". *)
None
| PdgMarks.SelNode (n, _z_opt) ->
- let nkey = !Db.Pdg.node_key n in
+ let nkey = Pdg.Api.node_key n in
(*
let nkey = match z_opt with None -> nkey
| Some z -> match nkey with
@@ -516,7 +516,7 @@ end = struct
| _ -> (); false
in
SlicingParameters.debug ~level:2 "[Fct_Slice.FctMarks.check_called_marks] for %a : old=%a new=%a -> %a %s"
- !Db.Pdg.pretty_key nkey
+ Pdg.Api.pretty_key nkey
SlicingMarks.pretty_mark old_m
SlicingMarks.pretty_mark m
SlicingMarks.pretty_mark
@@ -532,7 +532,7 @@ end = struct
SlicingParameters.debug ~level:2 "[Fct_Slice.FctMarks.persistent_in_marks_to_prop] from %s" (SlicingMacros.fi_name fi);
let m2m _call _pdg_caller _n m =
(* SlicingParameters.debug ~level:2 " in_m2m %a in %s ?@."
- PdgIndex.Key.pretty (!Db.Pdg.node_key n) (SlicingMacros.pdg_name pdg_caller); *)
+ PdgIndex.Key.pretty (Pdg.Api.node_key n) (SlicingMacros.pdg_name pdg_caller); *)
SlicingMarks.missing_input_mark ~call:SlicingMarks.bottom_mark ~called:m
in
let pdg = SlicingMacros.get_fi_pdg fi in
@@ -546,13 +546,13 @@ end = struct
let nkey = match n with
| PdgMarks.SelNode (n, _z_opt) ->
(* TODO : something to do for z_opt ? *)
- !Db.Pdg.node_key n
+ Pdg.Api.node_key n
| PdgMarks.SelIn l -> PdgIndex.Key.implicit_in_key l
in
let oldm = get_mark fm nkey in
let newm = SlicingMarks.minus_marks m oldm in
(* Format.printf "get_new_marks for %a : old=%a new=%a -> %a@."
- !Db.Pdg.pretty_key nkey SlicingMarks.pretty_mark oldm
+ Pdg.Api.pretty_key nkey SlicingMarks.pretty_mark oldm
SlicingMarks.pretty_mark m SlicingMarks.pretty_mark newm; *)
if not (SlicingMarks.is_bottom_mark newm) then (n, newm)::acc else acc
in List.fold_left add_if_new [] nodes_marks
@@ -571,7 +571,7 @@ end = struct
let mark_spare_call_nodes ff call =
let pdg = SlicingMacros.get_ff_pdg ff in
- let nodes = !Db.Pdg.find_simple_stmt_nodes pdg call in
+ let nodes = Pdg.Api.find_simple_stmt_nodes pdg call in
mark_spare_nodes ff nodes
(** TODO :
@@ -587,8 +587,8 @@ end = struct
let rec check_in_params n params = match params with
| [] -> []
| _ :: params ->
- let node = !Db.Pdg.find_input_node pdg n in
- let dpds = !Db.Pdg.direct_dpds pdg node in
+ let node = Pdg.Api.find_input_node pdg n in
+ let dpds = Pdg.Api.direct_dpds pdg node in
let get_n_mark n = get_mark ff_marks (PdgTypes.Node.elem_key n) in
let dpds_marks = List.map get_n_mark dpds in
let m = SlicingMarks.inter_marks dpds_marks in
@@ -596,7 +596,7 @@ end = struct
if not (SlicingMarks.is_bottom_mark m) then begin
SlicingKernel.debug ~level:2
"[Fct_Slice.FctMarks.mark_visible_inputs] %a -> %a"
- (!Db.Pdg.pretty_node true) node SlicingMarks.pretty_mark m;
+ (Pdg.Api.pretty_node true) node SlicingMarks.pretty_mark m;
PdgMarks.add_node_to_select marks (node, None) m
end else
marks
@@ -609,15 +609,15 @@ end = struct
let mark_visible_output ff_marks =
let pdg, _ = ff_marks in
try
- let out_node = !Db.Pdg.find_ret_output_node pdg in
- let dpds = !Db.Pdg.direct_dpds pdg out_node in
+ let out_node = Pdg.Api.find_ret_output_node pdg in
+ let dpds = Pdg.Api.direct_dpds pdg out_node in
let get_n_mark n = get_mark ff_marks (PdgTypes.Node.elem_key n) in
let dpds_marks = List.map get_n_mark dpds in
let m = SlicingMarks.inter_marks dpds_marks in
if not (SlicingMarks.is_bottom_mark m) then begin
SlicingParameters.debug ~level:2
"[Fct_Slice.FctMarks.mark_visible_outputs] %a -> %a"
- (!Db.Pdg.pretty_node true) out_node SlicingMarks.pretty_mark m;
+ (Pdg.Api.pretty_node true) out_node SlicingMarks.pretty_mark m;
let select = PdgMarks.add_node_to_select [] (out_node, None) m in
let to_prop = mark_and_propagate ff_marks select in
assert (to_prop = PropMark.empty_to_prop); ()
@@ -634,10 +634,10 @@ end = struct
with PdgIndex.CallStatement -> assert false
with Not_found -> SlicingMarks.bottom_mark
in
- Format.fprintf fmt "%a : %a" (!Db.Pdg.pretty_node true) node
+ Format.fprintf fmt "%a : %a" (Pdg.Api.pretty_node true) node
SlicingMarks.pretty_mark m
in
- !Db.Pdg.iter_nodes print_node pdg
+ Pdg.Api.iter_nodes print_node pdg
let debug_marked_ff fmt ff =
Format.fprintf fmt "@[<hv>Print slice =@ %s@]" (SlicingMacros.ff_name ff);
@@ -663,7 +663,7 @@ let get_called_slice ff call =
let _pretty_node_marks fmt marks =
let print fmt (n, m) =
- (!Db.Pdg.pretty_node true) fmt n; SlicingMarks.pretty_mark fmt m
+ (Pdg.Api.pretty_node true) fmt n; SlicingMarks.pretty_mark fmt m
in
Format.fprintf fmt "%a" (fun fmt x -> List.iter (print fmt) x) marks
@@ -1000,7 +1000,7 @@ let get_call_in_nodes called_kf call_info called_in_zone =
let _, nodes, in_zone =
List.fold_left check_param (1, [], called_in_zone) param_list
in
- let impl_in_nodes, undef = !Db.Pdg.find_location_nodes_at_stmt
+ let impl_in_nodes, undef = Pdg.Api.find_location_nodes_at_stmt
pdg_caller call_stmt ~before:true in_zone
in (nodes @ impl_in_nodes), undef
@@ -1232,7 +1232,7 @@ let apply_missing_inputs ff call missing_inputs =
assert (not (SlicingMarks.is_bottom_mark m));
match sel with
| PdgMarks.SelNode (n, _)
- when (!Db.Pdg.node_key n = PdgIndex.Key.top_input) -> true
+ when (Pdg.Api.node_key n = PdgIndex.Key.top_input) -> true
| _ -> visible_top tl
in let is_top_visible = visible_top input_marks in
*)
diff --git a/src/plugins/slicing/printSlice.ml b/src/plugins/slicing/printSlice.ml
index faa275ee37b..1775db3293c 100644
--- a/src/plugins/slicing/printSlice.ml
+++ b/src/plugins/slicing/printSlice.ml
@@ -334,7 +334,7 @@ let build_dot_project filename title =
let print_fct_stmts fmt kf =
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
print_fct_from_pdg fmt pdg;
Format.pp_print_flush fmt ()
with Not_found -> ()
diff --git a/src/plugins/slicing/slicingActions.ml b/src/plugins/slicing/slicingActions.ml
index 3529e422015..8fd243d8a96 100644
--- a/src/plugins/slicing/slicingActions.ml
+++ b/src/plugins/slicing/slicingActions.ml
@@ -156,10 +156,10 @@ let mk_appli_select_calls fi = SlicingInternals.CrAppli (SlicingInternals.CaCall
let mk_crit_mark_calls fi_caller to_call mark =
let select = try
let caller = SlicingMacros.get_fi_kf fi_caller in
- let pdg_caller = !Db.Pdg.get caller in
- let call_stmts = !Db.Pdg.find_call_stmts ~caller to_call in
+ let pdg_caller = Pdg.Api.get caller in
+ let call_stmts = Pdg.Api.find_call_stmts ~caller to_call in
let stmt_mark stmt =
- let stmt_ctrl_node = !Db.Pdg.find_call_ctrl_node pdg_caller stmt in
+ let stmt_ctrl_node = Pdg.Api.find_call_ctrl_node pdg_caller stmt in
(PdgMarks.mk_select_node stmt_ctrl_node, mark)
in
let select = List.map stmt_mark call_stmts in
@@ -182,7 +182,7 @@ let mk_crit_add_output_marks ff select =
(*
let mk_crit_add_all_outputs_mark ff mark =
let pdg = SlicingMacros.get_ff_pdg ff in
- let nodes = !Db.Pdg.find_all_outputs_nodes pdg in
+ let nodes = Pdg.Api.find_all_outputs_nodes pdg in
let nd_m = build_simple_node_selection mark in
let select = mk_mark_nodes nodes nd_m in
mk_ff_user_crit ff select
@@ -206,7 +206,7 @@ let rec print_nd_and_mark_list fmt ndm_list =
print_nd_and_mark fmt x; print_nd_and_mark_list fmt ndm_list
let print_nodes fmt nodes =
- let print n = Format.fprintf fmt "%a " (!Db.Pdg.pretty_node true) n in
+ let print n = Format.fprintf fmt "%a " (Pdg.Api.pretty_node true) n in
List.iter print nodes
let print_node_mark fmt n z m =
diff --git a/src/plugins/slicing/slicingActions.mli b/src/plugins/slicing/slicingActions.mli
index 975252aaa93..314a61918cb 100644
--- a/src/plugins/slicing/slicingActions.mli
+++ b/src/plugins/slicing/slicingActions.mli
@@ -43,7 +43,7 @@ val build_node_and_dpds_selection :
?nd_marks:n_or_d_marks -> sl_mark -> n_or_d_marks
val translate_crit_to_select :
- Db.Pdg.t -> ?to_select:select ->
+ Pdg.Api.t -> ?to_select:select ->
((PdgTypes.Node.t * Locations.Zone.t option) list * n_or_d_marks) list
-> select
diff --git a/src/plugins/slicing/slicingMacros.ml b/src/plugins/slicing/slicingMacros.ml
index d221c7299c3..05df109b352 100644
--- a/src/plugins/slicing/slicingMacros.ml
+++ b/src/plugins/slicing/slicingMacros.ml
@@ -127,7 +127,7 @@ let get_pdg_kf pdg = PdgTypes.Pdg.get_kf pdg
(** {4 getting PDG} *)
-let get_fi_pdg fi = let kf = get_fi_kf fi in !Db.Pdg.get kf
+let get_fi_pdg fi = let kf = get_fi_kf fi in Pdg.Api.get kf
let get_ff_pdg ff = get_fi_pdg ff.SlicingInternals.ff_fct
diff --git a/src/plugins/slicing/slicingMacros.mli b/src/plugins/slicing/slicingMacros.mli
index 04e20ee753e..183aff57436 100644
--- a/src/plugins/slicing/slicingMacros.mli
+++ b/src/plugins/slicing/slicingMacros.mli
@@ -40,8 +40,8 @@ val ff_src_name : fct_slice -> string
val get_fi_kf : fct_info -> Cil_types.kernel_function
val get_ff_kf : fct_slice -> Cil_types.kernel_function
val get_pdg_kf : PdgTypes.Pdg.t -> Kernel_function.t
-val get_fi_pdg : fct_info -> Db.Pdg.t
-val get_ff_pdg : fct_slice -> Db.Pdg.t
+val get_fi_pdg : fct_info -> Pdg.Api.t
+val get_ff_pdg : fct_slice -> Pdg.Api.t
val ff_slicing_level : fct_slice -> level_option
val change_fi_slicing_level : fct_info -> level_option -> unit
val change_slicing_level : Kernel_function.t -> int -> unit
diff --git a/src/plugins/slicing/slicingSelect.ml b/src/plugins/slicing/slicingSelect.ml
index 25b922ab7f4..4b3c23c2913 100644
--- a/src/plugins/slicing/slicingSelect.ml
+++ b/src/plugins/slicing/slicingSelect.ml
@@ -72,7 +72,7 @@ let basic_add_select kf select nodes ?(undef) nd_marks =
match sel with
| SlicingInternals.CuTop _ -> select
| SlicingInternals.CuSelect sel ->
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let nodes =
List.map (fun n -> (n, None) (*TODO: add z_part ? *)) nodes in
(* let nd_marks = SlicingActions.build_node_and_dpds_selection mark in *)
@@ -89,7 +89,7 @@ let select_pdg_nodes kf ?(select=empty_db_select kf) nodes mark =
SlicingParameters.debug ~level:1 "[Register.select_pdg_nodes]" ;
let nd_marks = SlicingActions.build_node_and_dpds_selection mark in
try basic_add_select kf select nodes nd_marks
- with Db.Pdg.Top | Db.Pdg.Bottom ->
+ with Pdg.Api.Top | Pdg.Api.Bottom ->
assert false (* if we have node, we must have a pdg somewhere ! *)
let mk_select pdg sel nodes undef mark =
@@ -120,9 +120,9 @@ let select_stmt_zone kf ?(select=empty_db_select kf) stmt ~before loc mark =
| SlicingInternals.CuTop _ -> select
| SlicingInternals.CuSelect sel ->
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let nodes, undef =
- !Db.Pdg.find_location_nodes_at_stmt pdg stmt ~before loc in
+ Pdg.Api.find_location_nodes_at_stmt pdg stmt ~before loc in
let sel = mk_select pdg sel nodes undef mark in
(fvar, sel)
with
@@ -138,8 +138,8 @@ let select_stmt_zone kf ?(select=empty_db_select kf) stmt ~before loc mark =
(if before then "before" else "after") stmt.sid
Kernel_function.pretty kf;
select
- | Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; select
+ | Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; select
(** this one is similar to [select_stmt_zone] with the return statement
@@ -154,10 +154,10 @@ let select_in_out_zone ~at_end ~use_undef kf select loc mark =
| SlicingInternals.CuTop _ -> select
| SlicingInternals.CuSelect sel ->
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let find =
- if at_end then !Db.Pdg.find_location_nodes_at_end
- else !Db.Pdg.find_location_nodes_at_begin in
+ if at_end then Pdg.Api.find_location_nodes_at_end
+ else Pdg.Api.find_location_nodes_at_begin in
let nodes, undef = find pdg loc in
let undef = if use_undef then undef else None in
let sel = mk_select pdg sel nodes undef mark in
@@ -169,8 +169,8 @@ let select_in_out_zone ~at_end ~use_undef kf select loc mark =
Locations.Zone.pretty loc SlicingMarks.pretty_mark mark
(if at_end then "end" else "begin") Kernel_function.pretty kf;
select
- | Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; select
+ | Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; select
let select_zone_at_end kf ?(select=empty_db_select kf) loc mark =
select_in_out_zone ~at_end:true ~use_undef:true kf select loc mark
@@ -183,9 +183,9 @@ let select_zone_at_entry kf ?(select=empty_db_select kf) loc mark =
let stmt_nodes_to_select pdg stmt =
try
- let stmt_nodes = !Db.Pdg.find_stmt_and_blocks_nodes pdg stmt in
+ let stmt_nodes = Pdg.Api.find_stmt_and_blocks_nodes pdg stmt in
SlicingParameters.debug ~level:2 "[Register.stmt_nodes_to_select] results on stmt %d (%a)" stmt.sid
- (fun fmt l -> List.iter (!Db.Pdg.pretty_node true fmt) l)
+ (fun fmt l -> List.iter (Pdg.Api.pretty_node true fmt) l)
stmt_nodes;
stmt_nodes
with Not_found ->
@@ -203,23 +203,23 @@ let select_stmt_computation kf ?(select=empty_db_select kf) stmt mark =
end
else
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let stmt_nodes = stmt_nodes_to_select pdg stmt in
let nd_marks = SlicingActions.build_node_and_dpds_selection mark in
basic_add_select kf select stmt_nodes nd_marks
- with Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; select
+ with Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; select
let select_label kf ?(select=empty_db_select kf) label mark =
SlicingParameters.debug ~level:1 "[Register.select_label] on label "
(* Logic_label.pretty label *);
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let nodes =
let add_label_nodes l acc = match l with
| StmtLabel stmt ->
let add acc l =
- try !Db.Pdg.find_label_node pdg !stmt l :: acc
+ try Pdg.Api.find_label_node pdg !stmt l :: acc
with Not_found -> acc
in
List.fold_left add acc (!stmt).labels
@@ -230,8 +230,8 @@ let select_label kf ?(select=empty_db_select kf) label mark =
in
let nd_marks = SlicingActions.build_node_and_dpds_selection mark in
basic_add_select kf select nodes nd_marks
- with Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; select
+ with Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; select
(** marking a call node means that a [choose_call] will have to decide that to
* call according to the slicing-level, but anyway, the call will be visible.
@@ -239,42 +239,42 @@ let select_label kf ?(select=empty_db_select kf) label mark =
let select_minimal_call kf ?(select=empty_db_select kf) stmt m =
SlicingParameters.debug ~level:1 "[Register.select_minimal_call]";
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let call = check_call stmt true in
- let call_node = !Db.Pdg.find_call_ctrl_node pdg call in
+ let call_node = Pdg.Api.find_call_ctrl_node pdg call in
let nd_marks = SlicingActions.build_simple_node_selection m in
basic_add_select kf select [call_node] nd_marks
- with Db.Pdg.Top -> top_db_select kf m
- | Db.Pdg.Bottom -> bottom_msg kf; select
+ with Pdg.Api.Top -> top_db_select kf m
+ | Pdg.Api.Bottom -> bottom_msg kf; select
let select_stmt_ctrl kf ?(select=empty_db_select kf) stmt =
SlicingParameters.debug ~level:1 "[Register.select_stmt_ctrl] of sid:%d" stmt.sid;
let mark = SlicingMarks.mk_user_mark ~ctrl:true ~data:false ~addr:false in
try
- let pdg = !Db.Pdg.get kf in
- let stmt_nodes = !Db.Pdg.find_simple_stmt_nodes pdg stmt in
+ let pdg = Pdg.Api.get kf in
+ let stmt_nodes = Pdg.Api.find_simple_stmt_nodes pdg stmt in
let nd_marks = SlicingActions.build_ctrl_dpds_selection mark in
basic_add_select kf select stmt_nodes nd_marks
- with Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; empty_db_select kf
+ with Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; empty_db_select kf
let select_entry_point kf ?(select=empty_db_select kf) mark =
SlicingParameters.debug ~level:1 "[Register.select_entry_point] of %a"
Kernel_function.pretty kf;
try
- let pdg = !Db.Pdg.get kf in
- let node = !Db.Pdg.find_entry_point_node pdg in
+ let pdg = Pdg.Api.get kf in
+ let node = Pdg.Api.find_entry_point_node pdg in
let nd_marks = SlicingActions.build_simple_node_selection mark in
basic_add_select kf select [node] nd_marks
- with Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; empty_db_select kf
+ with Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; empty_db_select kf
let select_return kf ?(select=empty_db_select kf) mark =
SlicingParameters.debug ~level:1 "[Register.select_return] of %a"
Kernel_function.pretty kf;
try
- let pdg = !Db.Pdg.get kf in
- let node = !Db.Pdg.find_ret_output_node pdg in
+ let pdg = Pdg.Api.get kf in
+ let node = Pdg.Api.find_ret_output_node pdg in
let nd_marks = SlicingActions.build_simple_node_selection mark in
basic_add_select kf select [node] nd_marks
with
@@ -283,8 +283,8 @@ let select_return kf ?(select=empty_db_select kf) mark =
"@[Nothing to select for return stmt of %a@]"
Kernel_function.pretty kf;
select
- | Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; empty_db_select kf
+ | Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; empty_db_select kf
let select_decl_var kf ?(select=empty_db_select kf) vi mark =
SlicingParameters.debug ~level:1 "[Register.select_decl_var] of %s in %a@."
@@ -292,8 +292,8 @@ let select_decl_var kf ?(select=empty_db_select kf) vi mark =
if vi.Cil_types.vglob (* no slicing request on globals *)
then select
else try
- let pdg = !Db.Pdg.get kf in
- let node = !Db.Pdg.find_decl_var_node pdg vi in
+ let pdg = Pdg.Api.get kf in
+ let node = Pdg.Api.find_decl_var_node pdg vi in
let nd_marks = SlicingActions.build_simple_node_selection mark in
basic_add_select kf select [node] nd_marks
with
@@ -302,8 +302,8 @@ let select_decl_var kf ?(select=empty_db_select kf) vi mark =
"@[Nothing to select for %s declarationin %a@]"
vi.Cil_types.vname Kernel_function.pretty kf;
select
- | Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; empty_db_select kf
+ | Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; empty_db_select kf
let merge_select select1 select2 =
@@ -351,7 +351,7 @@ let add_crit_ff_change_call ff_caller call f_to_call =
let call_ff_in_caller ~caller ~to_call =
let kf_caller = SlicingMacros.get_ff_kf caller in
let kf_to_call = SlicingMacros.get_ff_kf to_call in
- let call_stmts = !Db.Pdg.find_call_stmts ~caller:kf_caller kf_to_call in
+ let call_stmts = Pdg.Api.find_call_stmts ~caller:kf_caller kf_to_call in
let ff_to_call = SlicingInternals.CallSlice to_call in
let add_change_call stmt =
add_crit_ff_change_call caller stmt ff_to_call ;
@@ -367,7 +367,7 @@ let call_fsrc_in_caller ~caller ~to_call =
let kf_caller = SlicingMacros.get_ff_kf caller in
let fi_to_call = SlicingMacros.get_kf_fi to_call in
let kf_to_call = SlicingMacros.get_fi_kf fi_to_call in
- let call_stmts = !Db.Pdg.find_call_stmts ~caller:kf_caller kf_to_call in
+ let call_stmts = Pdg.Api.find_call_stmts ~caller:kf_caller kf_to_call in
let add_change_call stmt =
add_crit_ff_change_call caller stmt (SlicingInternals.CallSrc (Some fi_to_call))
in List.iter add_change_call call_stmts
@@ -375,9 +375,9 @@ let call_fsrc_in_caller ~caller ~to_call =
let call_min_f_in_caller ~caller ~to_call =
let kf_caller = SlicingMacros.get_ff_kf caller in
let pdg = SlicingMacros.get_ff_pdg caller in
- let call_stmts = !Db.Pdg.find_call_stmts ~caller:kf_caller to_call in
+ let call_stmts = Pdg.Api.find_call_stmts ~caller:kf_caller to_call in
let call_nodes =
- List.map (fun call -> (!Db.Pdg.find_call_ctrl_node pdg call),None)
+ List.map (fun call -> (Pdg.Api.find_call_ctrl_node pdg call),None)
call_stmts in
let m = SlicingMarks.mk_user_spare in
let nd_marks = SlicingActions.build_simple_node_selection m in
@@ -389,7 +389,7 @@ let is_already_selected ff db_select =
match select with
| SlicingInternals.CuTop _ -> assert false
| SlicingInternals.CuSelect to_select ->
- (* let pdg = !Db.Pdg.get (Globals.Functions.get fvar) in *)
+ (* let pdg = Pdg.Api.get (Globals.Functions.get fvar) in *)
let new_marks = Fct_slice.filter_already_in ff to_select in
let ok = if new_marks = [] then true else false in
if ok then
diff --git a/src/plugins/slicing/slicingSelect.mli b/src/plugins/slicing/slicingSelect.mli
index c139085e9da..6f682ad2735 100644
--- a/src/plugins/slicing/slicingSelect.mli
+++ b/src/plugins/slicing/slicingSelect.mli
@@ -69,7 +69,7 @@ val select_pdg_nodes :
SlicingTypes.sl_select
val mk_select :
- Db.Pdg.t ->
+ Pdg.Api.t ->
SlicingActions.select ->
(PdgTypes.Node.t * Locations.Zone.t option) list ->
Locations.Zone.t option ->
@@ -117,7 +117,7 @@ val select_zone_at_entry :
SlicingTypes.sl_select
val stmt_nodes_to_select :
- Db.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t list
+ Pdg.Api.t -> Cil_types.stmt -> PdgTypes.Node.t list
val select_stmt_computation :
Kernel_function.t ->
diff --git a/src/plugins/slicing/slicingState.ml b/src/plugins/slicing/slicingState.ml
index b51f528fe8b..28991d80642 100644
--- a/src/plugins/slicing/slicingState.ml
+++ b/src/plugins/slicing/slicingState.ml
@@ -34,7 +34,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:self
- [ !Db.Pdg.self; !Db.Inputs.self_external; !Db.Outputs.self_external ])
+ [ Pdg.Api.self; !Db.Inputs.self_external; !Db.Outputs.self_external ])
let get () =
try P.get ()
diff --git a/src/plugins/slicing/slicingTransform.ml b/src/plugins/slicing/slicingTransform.ml
index 5d7b4d1c528..f142150160d 100644
--- a/src/plugins/slicing/slicingTransform.ml
+++ b/src/plugins/slicing/slicingTransform.ml
@@ -138,7 +138,7 @@ module Visibility (SliceName : sig
begin
SlicingParameters.debug ~level:3
"[SlicingTransform.Visibility.all_nodes_visible] node %a invisible"
- (!Db.Pdg.pretty_node true) n;
+ (Pdg.Api.pretty_node true) n;
false
end
else visi
@@ -173,7 +173,7 @@ module Visibility (SliceName : sig
SlicingParameters.debug ~level:2
"[SlicingTransform.Visibility.data_nodes_visible]@\n\
node %a invisible"
- (!Db.Pdg.pretty_node true) n;
+ (Pdg.Api.pretty_node true) n;
false
end
else visi
@@ -242,10 +242,10 @@ module Visibility (SliceName : sig
| Iproto -> false
| Iff {slice = ff} ->
let kf = SlicingMacros.get_ff_kf ff in
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
try
let ctrl_nodes, decl_nodes, data_info =
- !Db.Pdg.find_code_annot_nodes pdg stmt annot
+ Pdg.Api.find_code_annot_nodes pdg stmt annot
in
let data_visible = data_nodes_visible ff (decl_nodes, data_info) in
let visible = ((all_nodes_visible ff ctrl_nodes) && data_visible) in
@@ -276,9 +276,9 @@ module Visibility (SliceName : sig
| Iproto -> true
| Iff {slice = ff} ->
let kf = SlicingMacros.get_ff_kf ff in
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
try
- let nodes = !Db.Pdg.find_fun_precond_nodes pdg p in
+ let nodes = Pdg.Api.find_fun_precond_nodes pdg p in
data_nodes_visible ff nodes
with NoDataInfo ->
all_logic_var_visible ff p
@@ -296,9 +296,9 @@ module Visibility (SliceName : sig
| Iproto -> true
| Iff {slice = ff} ->
let kf = SlicingMacros.get_ff_kf ff in
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
try
- let nodes = !Db.Pdg.find_fun_postcond_nodes pdg p in
+ let nodes = Pdg.Api.find_fun_postcond_nodes pdg p in
data_nodes_visible ff nodes
with NoDataInfo -> all_logic_var_visible ff p
@@ -316,9 +316,9 @@ module Visibility (SliceName : sig
| Iproto -> true
| Iff {slice = ff} ->
let kf = SlicingMacros.get_ff_kf ff in
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
try
- let nodes = !Db.Pdg.find_fun_variant_nodes pdg v in
+ let nodes = Pdg.Api.find_fun_variant_nodes pdg v in
data_nodes_visible ff nodes
with NoDataInfo -> all_logic_var_visible_term ff v
in SlicingParameters.debug ~level:2 "[SlicingTransform.Visibility.fun_variant_visible] -> %s"
diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml
index 860f24fa634..7db1fca385b 100644
--- a/src/plugins/sparecode/globs.ml
+++ b/src/plugins/sparecode/globs.ml
@@ -160,7 +160,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:Result.self
- [ !Db.Pdg.self; !Db.Outputs.self_external ])
+ [ Pdg.Api.self; !Db.Outputs.self_external ])
let rm_unused_decl =
Result.memo
diff --git a/src/plugins/sparecode/register.ml b/src/plugins/sparecode/register.ml
index b684d758b6b..3ac3e1d4ccb 100644
--- a/src/plugins/sparecode/register.ml
+++ b/src/plugins/sparecode/register.ml
@@ -43,7 +43,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:Result.self
- [ !Db.Pdg.self; !Db.Outputs.self_external ])
+ [ Pdg.Api.self; !Db.Outputs.self_external ])
module P = Sparecode_params
diff --git a/src/plugins/sparecode/spare_marks.ml b/src/plugins/sparecode/spare_marks.ml
index 2f0c83674a9..314e896c662 100644
--- a/src/plugins/sparecode/spare_marks.ml
+++ b/src/plugins/sparecode/spare_marks.ml
@@ -25,7 +25,7 @@ let fatal fmt = Sparecode_params.fatal fmt
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(** The project is composed of [FctIndex] marked with [BoolMark]
- * to be used by [Pdg.Register.F_Proj], and another table to store if a function
+ * to be used by [Pdg.Api.Marks.F_Proj], and another table to store if a function
* is visible (useful for Top PDG). *)
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
@@ -122,7 +122,7 @@ module Config = struct
end
-module ProjBoolMarks = Pdg.Register.F_Proj (Config)
+module ProjBoolMarks = Pdg.Api.Marks.F_Proj (Config)
type proj = ProjBoolMarks.t * unit KfTopVisi.t
type fct = ProjBoolMarks.fct
@@ -172,7 +172,7 @@ let rec add_pdg_selection to_select pdg sel_mark = match to_select with
| [] ->
let l = match sel_mark with None -> [] | Some m -> [m] in [(pdg, l)]
| (p, ln) :: tl ->
- if Db.Pdg.from_same_fun p pdg
+ if Pdg.Api.from_same_fun p pdg
then
let ln = match sel_mark with None -> ln
| Some sel_mark -> sel_mark::ln
@@ -273,7 +273,7 @@ let rec process_call_inputs proj =
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
let select_entry_point proj _kf pdg =
- let ctrl = !Db.Pdg.find_entry_point_node pdg in
+ let ctrl = Pdg.Api.find_entry_point_node pdg in
let to_select = add_node_to_select true [] None ctrl in
select_pdg_elements proj pdg to_select
@@ -281,9 +281,9 @@ let select_all_outputs proj kf pdg =
let outputs = !Db.Outputs.get_external kf in
debug 1 "@[selecting output zones %a@]" Locations.Zone.pretty outputs;
try
- let nodes, undef = !Db.Pdg.find_location_nodes_at_end pdg outputs in
+ let nodes, undef = Pdg.Api.find_location_nodes_at_end pdg outputs in
let nodes =
- try ((!Db.Pdg.find_ret_output_node pdg),None) :: nodes
+ try ((Pdg.Api.find_ret_output_node pdg),None) :: nodes
with Not_found -> nodes
in
let nodes_and_co = ([], [], Some (nodes, undef)) in
@@ -308,7 +308,7 @@ class annot_visitor ~filter pdg = object (self)
let stmt = Option.get self#current_stmt in
debug 1 "selecting annotation : %a @."
Printer.pp_code_annotation annot;
- let info = !Db.Pdg.find_code_annot_nodes pdg stmt annot in
+ let info = Pdg.Api.find_code_annot_nodes pdg stmt annot in
to_select <- add_nodes_and_undef_to_select true info to_select
with
Not_found -> () (* unreachable *)
@@ -322,7 +322,7 @@ end
let select_annotations ~select_annot ~select_slice_pragma proj =
let visit_fun kf =
debug 1 "look for annotations in function %a@." Kernel_function.pretty kf;
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
if PdgTypes.Pdg.is_top pdg then debug 1 "pdg top: skip annotations"
else if PdgTypes.Pdg.is_bottom pdg
then debug 1 "pdg bottom: skip annotations"
@@ -357,7 +357,7 @@ let select_useful_things ~select_annot ~select_slice_pragma kf_entry =
assert (!call_in_to_check = []);
debug 1 "selecting function %a outputs and entry point@."
Kernel_function.pretty kf_entry;
- let pdg = !Db.Pdg.get kf_entry in
+ let pdg = Pdg.Api.get kf_entry in
if PdgTypes.Pdg.is_top pdg
then KfTopVisi.set proj kf_entry
else if PdgTypes.Pdg.is_bottom pdg
diff --git a/src/plugins/sparecode/transform.ml b/src/plugins/sparecode/transform.ml
index e2280ec81b2..b22d74c35c0 100644
--- a/src/plugins/sparecode/transform.ml
+++ b/src/plugins/sparecode/transform.ml
@@ -41,7 +41,7 @@ module BoolInfo = struct
| Some fm -> Spare_marks.key_visible fm key
in
Sparecode_params.debug ~level:3 "%s : %a -> %b"
- txt !Db.Pdg.pretty_key key visible;
+ txt Pdg.Api.pretty_key key visible;
visible
let param_visible (fm,_) n =
diff --git a/tests/pdg/dyn_dpds.ml b/tests/pdg/dyn_dpds.ml
index 716e5067f6a..4907cf29314 100644
--- a/tests/pdg/dyn_dpds.ml
+++ b/tests/pdg/dyn_dpds.ml
@@ -21,29 +21,29 @@ let main _ =
File.pretty_ast ();
Kernel.Debug.set memo_debug ;
let kf = Globals.Functions.find_def_by_name "main" in
- let pdg = !Db.Pdg.get kf in
- Format.printf "%a@." (!Db.Pdg.pretty ~bw:false) pdg;
- !Db.Pdg.extract pdg "dyn_dpds_0.dot";
+ let pdg = Pdg.Api.get kf in
+ Format.printf "%a@." (Pdg.Api.pretty ~bw:false) pdg;
+ Pdg.Api.extract pdg "dyn_dpds_0.dot";
let assert_sid = 5 in (* assert ( *p>G) *)
let assert_stmt, kf = Kernel_function.find_from_sid assert_sid in
let _assert_node =
- match !Db.Pdg.find_simple_stmt_nodes pdg assert_stmt with
+ match Pdg.Api.find_simple_stmt_nodes pdg assert_stmt with
| n::[] -> n | _ -> assert false
in
let star_p = get_zones "*p" (assert_stmt, kf) in
let data_nodes, undef =
- !Db.Pdg.find_location_nodes_at_stmt pdg assert_stmt ~before:true star_p
+ Pdg.Api.find_location_nodes_at_stmt pdg assert_stmt ~before:true star_p
in
assert (undef = None);
let g_zone = get_zones "G" (assert_stmt, kf) in
let g_nodes, undef =
- !Db.Pdg.find_location_nodes_at_stmt pdg assert_stmt ~before:true g_zone
+ Pdg.Api.find_location_nodes_at_stmt pdg assert_stmt ~before:true g_zone
in
let _data_nodes = g_nodes @ data_nodes in
let undef = match undef with None -> assert false | Some z -> z in
Format.printf "Warning : cannot select %a in this function...@\n"
Locations.Zone.pretty undef;
- Format.printf "%a@." (!Db.Pdg.pretty ~bw:false) pdg;
- !Db.Pdg.extract pdg "dyn_dpds_1.dot"
+ Format.printf "%a@." (Pdg.Api.pretty ~bw:false) pdg;
+ Pdg.Api.extract pdg "dyn_dpds_1.dot"
let () = Db.Main.extend main
diff --git a/tests/pdg/sets.ml b/tests/pdg/sets.ml
index f9759901253..8ebb56e106c 100644
--- a/tests/pdg/sets.ml
+++ b/tests/pdg/sets.ml
@@ -1,15 +1,14 @@
-open Db;;
open Cil_types;;
let pp_nodes msg nodes =
Kernel.result "%s" msg ;
- List.iter (fun n -> Kernel.result "%a" (!Pdg.pretty_node false) n) nodes;;
+ List.iter (fun n -> Kernel.result "%a" (Pdg.Api.pretty_node false) n) nodes;;
exception Find of varinfo;;
let main _ =
let f = Globals.Functions.find_by_name "f" in
- let pdg = !Pdg.get f in
+ let pdg = Pdg.Api.get f in
(* Uncomment to retrieve sid *)
(*Kernel.Debug.set 1;;
@@ -17,8 +16,8 @@ let main _ =
*)
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
let stmt_1 = fst (Kernel_function.find_from_sid 1) in (* y = 0 *)
- let node = !Pdg.find_stmt_node pdg stmt_1 in
- let nodes = !Pdg.all_uses pdg [node] in
+ let node = Pdg.Api.find_stmt_node pdg stmt_1 in
+ let nodes = Pdg.Api.all_uses pdg [node] in
pp_nodes "Test [all_uses] stmt1" nodes;
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
@@ -32,7 +31,7 @@ let main _ =
let y_zone = Locations.(enumerate_valid_bits Read (loc_of_varinfo y)) in
let y_at_11_nodes, undef = (* y=5 *)
- !Pdg.find_location_nodes_at_stmt
+ Pdg.Api.find_location_nodes_at_stmt
pdg (fst (Kernel_function.find_from_sid 11)) ~before:false y_zone
in
@@ -41,15 +40,15 @@ let main _ =
let () = pp_nodes "Test [find_location_nodes_at_stmt] y@11" y_at_11_nodes in
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let nodes = !Pdg.all_dpds pdg y_at_11_nodes in
+ let nodes = Pdg.Api.all_dpds pdg y_at_11_nodes in
let () = pp_nodes "Test [all_dpds] y@11" nodes in
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let nodes = !Pdg.all_uses pdg y_at_11_nodes in
+ let nodes = Pdg.Api.all_uses pdg y_at_11_nodes in
let () = pp_nodes "Test [all_uses] y@11" nodes in
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
let all_related_nodes pdg =
- let all n = (!Pdg.direct_uses pdg n) @ (!Pdg.direct_dpds pdg n) in
- !Pdg.custom_related_nodes all
+ let all n = (Pdg.Api.direct_uses pdg n) @ (Pdg.Api.direct_dpds pdg n) in
+ Pdg.Api.custom_related_nodes all
in
let nodes = all_related_nodes pdg y_at_11_nodes in
pp_nodes "Test [all_related_nodes] y@11" nodes
diff --git a/tests/slicing/libSelect.ml b/tests/slicing/libSelect.ml
index fae01cc8b50..8fed3fdca1f 100644
--- a/tests/slicing/libSelect.ml
+++ b/tests/slicing/libSelect.ml
@@ -29,7 +29,7 @@ let print_stmt kf =
Slicing.PrintSlice.print_fct_stmts fmt kf
(* print PDG (for debugging purposes) *)
-let print_pdg kf = !Db.Pdg.pretty fmt (!Db.Pdg.get kf) ;;
+let print_pdg kf = Pdg.Api.pretty fmt (Pdg.Api.get kf) ;;
let print_ff ff = Slicing.Api.Slice.pretty fmt ff
diff --git a/tests/slicing/min_call.ml b/tests/slicing/min_call.ml
index ebb0e3e8983..80fbe7ad125 100644
--- a/tests/slicing/min_call.ml
+++ b/tests/slicing/min_call.ml
@@ -31,8 +31,8 @@ let main _ =
* the call to [send_bis] is visible as wished. *)
Slicing.Api.Project.reset_slicing ();
- (*let pdg_k = !Db.Pdg.get kf_k;;*)
- let calls = !Db.Pdg.find_call_stmts ~caller:kf_k(*pdg_k*) kf_send_bis in
+ (*let pdg_k = Pdg.Api.get kf_k;;*)
+ let calls = Pdg.Api.find_call_stmts ~caller:kf_k(*pdg_k*) kf_send_bis in
let sb_call = match calls with c::[] -> c | _ -> assert false in
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let select = Slicing.Api.Select.select_stmt_internal kf_k sb_call mark in
@@ -52,8 +52,8 @@ let main _ =
* But as [send_bis] is an undefined function, this makes no difference.
*)
Slicing.Api.Project.reset_slicing ();
- (*let pdg_k = !Db.Pdg.get kf_k;;*)
- let calls = !Db.Pdg.find_call_stmts (*pdg_k*)~caller:kf_k kf_send_bis in
+ (*let pdg_k = Pdg.Api.get kf_k;;*)
+ let calls = Pdg.Api.find_call_stmts (*pdg_k*)~caller:kf_k kf_send_bis in
let sb_call = match calls with c::[] -> c | _ -> assert false in
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let select = Slicing.Api.Select.select_min_call_internal kf_k sb_call mark in
diff --git a/tests/slicing/select_by_annot.ml b/tests/slicing/select_by_annot.ml
index c3dec000e62..39e3e6d67a0 100644
--- a/tests/slicing/select_by_annot.ml
+++ b/tests/slicing/select_by_annot.ml
@@ -7,7 +7,7 @@ open LibSelect;;
let main _ =
Slicing.Api.Project.reset_slicing ();
- let pretty_pdg fmt kf = !Db.Pdg.pretty fmt (!Db.Pdg.get kf) in
+ let pretty_pdg fmt kf = Pdg.Api.pretty fmt (Pdg.Api.get kf) in
let add_annot kf =
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let select = Slicing.Api.Select.empty_selects in
diff --git a/tests/slicing/simple_intra_slice.ml b/tests/slicing/simple_intra_slice.ml
index f9e17c3b87c..7a7e189a1c9 100644
--- a/tests/slicing/simple_intra_slice.ml
+++ b/tests/slicing/simple_intra_slice.ml
@@ -7,7 +7,7 @@ include LibSelect;;
let main _ =
Slicing.Api.Project.reset_slicing ();
- let pretty_pdg fmt kf = !Db.Pdg.pretty fmt (!Db.Pdg.get kf) in
+ let pretty_pdg fmt kf = Pdg.Api.pretty fmt (Pdg.Api.get kf) in
let apply_all_actions = Slicing.Api.Request.apply_all_internal in
let print_slice = Slicing.Api.Slice.pretty in
let print_fct_stmts kf =
--
GitLab