diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
index 2fc410f59d4a1a98fa508ce5dcf8d8428655a427..b6ef39a67856b8c00985e4a92dc62e4be686179c 100644
--- a/.git-blame-ignore-revs
+++ b/.git-blame-ignore-revs
@@ -39,3 +39,4 @@ aef808e15e4dcc02dcee7004add8530083d33474
6ead6d862f1960e6baca64d335b811c954cf8430
7955ef2039b2010cc30b88da7a47d4f07e298042
8353ff71c9958169cf27c589b678f183cca63a9c
+fe98b40c209dbe13fdc2069e26c42d4062fda3f0
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 64e5c108ab5c3840e18f335d49f175bf582864d0..4d69ac1a7f47a72f2d819c48e4655f08e40f7fa6 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 905663fa636b56df38e8b0fbcbeda93483098aac..62334a53e2eda38fd43e4b647ac20c2b526507ff 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 1744f0a3e7da3f56490a759d998ecd28957c7be2..9f1379f3ec9104f0e9c23927c726ed55e9f30ce6 100644
--- a/src/plugins/impact/compute_impact.ml
+++ b/src/plugins/impact/compute_impact.ml
@@ -22,7 +22,10 @@
open Cil_types
open Cil_datatype
+
+open Pdg_types
open PdgIndex
+
open Reason_graph
(** Computation of the PDG nodes that are impacted by the "execution"
@@ -166,7 +169,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 +182,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 +323,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 +338,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 +401,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 +450,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 +489,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 +525,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 +539,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 +672,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/compute_impact.mli b/src/plugins/impact/compute_impact.mli
index 64307dc66281a1879dd0e7332ef9748ce058813c..74831f03df77459e0b84f0b5a17f7c2154dd3c43 100644
--- a/src/plugins/impact/compute_impact.mli
+++ b/src/plugins/impact/compute_impact.mli
@@ -22,6 +22,8 @@
open Cil_types
+open Pdg_types
+
type nodes = Pdg_aux.NS.t
type result = nodes Kernel_function.Map.t
diff --git a/src/plugins/impact/dune b/src/plugins/impact/dune
index 734041fbd969ca0f0697b1d757282f93c417c8d7..6bcede10dbbcfd1333725c7a55c804e15abbe9ae 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 39db9c604eff13ccd99f1853b7a7061a4f6e8c89..e00946f69448800bdd05a5e35f6bbf859a7e19ec 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 5146cb4a509f753a2e4ef66c8eac70c68377cf11..1bd988cb199607a31a287fa4df715fb8916fa52b 100644
--- a/src/plugins/impact/gui/register_gui.ml
+++ b/src/plugins/impact/gui/register_gui.ml
@@ -22,8 +22,8 @@
open Pretty_source
open Gtk_helper
-open Db
open Cil_types
+open Pdg_types
module SelectedStmt = struct
include State_builder.Option_ref
@@ -43,7 +43,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 +232,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 +268,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 8513bcf24116c76db8f094446ad837068f527f2e..0a3b4acb21ed47d3e6ab5e15869955fd91164b06 100644
--- a/src/plugins/impact/pdg_aux.ml
+++ b/src/plugins/impact/pdg_aux.ml
@@ -20,12 +20,12 @@
(* *)
(**************************************************************************)
+open Pdg_types
open PdgIndex
open Locations
type node = PdgTypes.Node.t * Zone.t
-
module NS = struct
include Hptmap.Make
(PdgTypes.Node)
@@ -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 32e7f34d68c3decd9bc4b30df0046734c05d5012..f07aca633a1ca26345642e911cf4567fa5d6a3fb 100644
--- a/src/plugins/impact/pdg_aux.mli
+++ b/src/plugins/impact/pdg_aux.mli
@@ -21,16 +21,17 @@
(**************************************************************************)
open Cil_types
-open PdgTypes
open Locations
+open Pdg_types
+
(** Useful functions that are not directly accessible through the other
Pdg modules. *)
(** 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 +54,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 +77,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 +85,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 eceba7800cf411e23e0689b306edd741f1ef07cb..eb8452ccdd367b01b77d582fb0b6571ea7bbb209 100644
--- a/src/plugins/impact/reason_graph.ml
+++ b/src/plugins/impact/reason_graph.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
module NodeSet = PdgTypes.NodeSet
@@ -216,7 +218,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/impact/reason_graph.mli b/src/plugins/impact/reason_graph.mli
index d0f03c55694e1a5d10439b237934cd69bce29d10..ccdbd733b2207e905a3d7054b204fcea8a674433 100644
--- a/src/plugins/impact/reason_graph.mli
+++ b/src/plugins/impact/reason_graph.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
(** Why is a node impacted. The reasons will be given as [n is impacted
by the effect of [n'], and the impact is of type reason]. *)
type reason_type =
diff --git a/src/plugins/impact/register.ml b/src/plugins/impact/register.ml
index 6dfc46429bd86b280c90ba5418fb0e552a2314bb..e9b09ca1784c2b9f1d8e547f27209b48f3284003 100644
--- a/src/plugins/impact/register.ml
+++ b/src/plugins/impact/register.ml
@@ -23,6 +23,8 @@
open Cil_types
open Cil_datatype
+open Pdg_types
+
let rec pp_stmt fmt s = match s.skind with
| Instr _ | Return _ | Goto _ | Break _ | Continue _ | TryFinally _
| TryExcept _ | Throw _ | TryCatch _ ->
diff --git a/src/plugins/impact/register.mli b/src/plugins/impact/register.mli
index a426a0bb2b23bc8422b0ec2a2b818d0834729721..7cdc3c047533c1b1c7e33408488ce820ba5bff83 100644
--- a/src/plugins/impact/register.mli
+++ b/src/plugins/impact/register.mli
@@ -22,6 +22,8 @@
open Cil_types
+open Pdg_types
+
val compute_pragmas: (unit -> stmt list)
(** Compute the impact analysis from the impact pragma in the program.
Print and slice the results according to the parameters -impact-print
diff --git a/src/plugins/pdg/Pdg.ml b/src/plugins/pdg/Pdg.ml
index 40d3a5633796cc24cd35e6286651003365ec1568..2472224ae4c3981e0e6720ab359d8b6f8ea034a6 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 Api = Api
-module Register = Register
+module Marks = Marks
diff --git a/src/plugins/pdg/Pdg.mli b/src/plugins/pdg/Pdg.mli
index 2fcfa88853137ba80dbddf902f353d2bbc5ac1fb..aaaefb329d90b35ec8a6078cf2d3cd5d767ca2d1 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 Api : module type of Api
-module Register : module type of Marks
+module Marks : module type of Marks
diff --git a/src/plugins/pdg/annot.ml b/src/plugins/pdg/annot.ml
index d76dc95c38da8546bce3569b83ddcadbb3fbfa54..09c37fa94373490d0eb7133f4c09be10d36bccec 100644
--- a/src/plugins/pdg/annot.ml
+++ b/src/plugins/pdg/annot.ml
@@ -22,6 +22,8 @@
open Cil_types
open Cil_datatype
+
+open Pdg_types
open PdgIndex
type data_info = ((PdgTypes.Node.t * Locations.Zone.t option) list
@@ -117,13 +119,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/annot.mli b/src/plugins/pdg/annot.mli
index 8aa296375843ddb909c61cba30f6b76014ea6c3e..c46dd70667d8e4df934d0843732858f3694fa267 100644
--- a/src/plugins/pdg/annot.mli
+++ b/src/plugins/pdg/annot.mli
@@ -24,6 +24,8 @@
@raise Kernel_function.No_Definition on annotations for function declarations.
*)
+open Pdg_types
+
(** [data_info] is composed of [(node,z_part) list, undef_loc)]
* and correspond to data dependencies nodes.
* Can be None if we don't know how to compute them.
diff --git a/src/plugins/pdg/api.ml b/src/plugins/pdg/api.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0024018d796890a4136e964dcbc48c9d1ee97ec7
--- /dev/null
+++ b/src/plugins/pdg/api.ml
@@ -0,0 +1,113 @@
+(**************************************************************************)
+(* *)
+(* 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" ]
+
+open Pdg_types
+
+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 0000000000000000000000000000000000000000..6094779cec4e5920a5575b27b90613eae0deaf66
--- /dev/null
+++ b/src/plugins/pdg/api.mli
@@ -0,0 +1,352 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Pdg_types
+
+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/build.ml b/src/plugins/pdg/build.ml
index 256f3d9f9980db347853fa0fcef8ed3ab51deb27..34dfb781a9acc918cf7bbffb2cd0f28718053bbd 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -31,6 +31,8 @@
{!module: Build.Computer} below).
*)
+open Pdg_types
+
let dkey = Pdg_parameters.register_category "build"
let debug fmt = Pdg_parameters.debug ~dkey fmt
let debug2 fmt = Pdg_parameters.debug ~dkey fmt ~level:2
diff --git a/src/plugins/pdg/build.mli b/src/plugins/pdg/build.mli
index 583fdbc47301200ea659df06ad1ba628c46044f9..6e134517409b423d3a2dab2e50cfa49f4f2a20a1 100644
--- a/src/plugins/pdg/build.mli
+++ b/src/plugins/pdg/build.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
val compute_pdg : Cil_types.kernel_function -> PdgTypes.Pdg.t
(*
diff --git a/src/plugins/pdg/dune b/src/plugins/pdg/dune
index 09b16b196070e41eb98cc7c8d813def69334e81c..1465f8006ad853303f300d99eb456d30638e8444 100644
--- a/src/plugins/pdg/dune
+++ b/src/plugins/pdg/dune
@@ -25,6 +25,7 @@
(deps (universe))
(action (progn
(echo "PDG:" %{lib-available:frama-c-pdg.core} "\n")
+ (echo " - Pdg-Types:" %{lib-available:frama-c-pdg-types.core} "\n")
(echo " - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
(echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
(echo " - From:" %{lib-available:frama-c-from.core} "\n")
@@ -37,7 +38,7 @@
(optional)
(public_name frama-c-pdg.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-callgraph.core frama-c-from.core frama-c-eva.core)
+ (libraries frama-c.kernel frama-c-pdg-types.core frama-c-callgraph.core frama-c-from.core frama-c-eva.core)
)
(plugin (optional) (name pdg) (libraries frama-c-pdg.core) (site (frama-c plugins)))
diff --git a/src/plugins/pdg/marks.ml b/src/plugins/pdg/marks.ml
index 272b5b1ad9fe0928b90ed766e1c06a0345f5afcc..6330ce5fb40bb8dfbe87e315f1ed4c2639b905d1 100644
--- a/src/plugins/pdg/marks.ml
+++ b/src/plugins/pdg/marks.ml
@@ -20,9 +20,11 @@
(* *)
(**************************************************************************)
-open PdgIndex
open Cil_datatype
+open Pdg_types
+open PdgIndex
+
(** compute the marks to propagate in the caller nodes from the marks of
* a function inputs [in_marks].
*)
@@ -36,12 +38,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 +66,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 +100,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 +167,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/marks.mli b/src/plugins/pdg/marks.mli
index 55a303293f931a46d482ff89bc32e84d1ad9666d..846aeae6adace9a638d1fbda719eff249dec6731 100644
--- a/src/plugins/pdg/marks.mli
+++ b/src/plugins/pdg/marks.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
open PdgMarks
(** [in_marks_to_caller] translate the input information part returned by
diff --git a/src/plugins/pdg/pdg_state.ml b/src/plugins/pdg/pdg_state.ml
index 276f231efbe10bc51e0dd8891540a12b56feb943..b5c081a3438d810f876fa6b30fe4f949be98804e 100644
--- a/src/plugins/pdg/pdg_state.ml
+++ b/src/plugins/pdg/pdg_state.ml
@@ -29,6 +29,8 @@
let dkey = Pdg_parameters.register_category "state"
module P = Pdg_parameters
+
+open Pdg_types
open PdgTypes
exception Cannot_fold
diff --git a/src/plugins/pdg/pdg_state.mli b/src/plugins/pdg/pdg_state.mli
index a108bd99666eca31c374ce242e6a9c50e1a7134b..72f8297b41a2e8f42130aca2aed6dbe160cb99ce 100644
--- a/src/plugins/pdg/pdg_state.mli
+++ b/src/plugins/pdg/pdg_state.mli
@@ -22,6 +22,8 @@
exception Cannot_fold
+open Pdg_types
+
open PdgTypes
(** Types data_state and Node.t come froms this module *)
diff --git a/src/plugins/pdg/pdg_tbl.ml b/src/plugins/pdg/pdg_tbl.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5603732213786a2cc7020bd13272323edd35081c
--- /dev/null
+++ b/src/plugins/pdg/pdg_tbl.ml
@@ -0,0 +1,61 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Pdg_types
+
+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 0000000000000000000000000000000000000000..541731a591138e8f100578e57827682b488da976
--- /dev/null
+++ b/src/plugins/pdg/pdg_tbl.mli
@@ -0,0 +1,46 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Pdg_types
+
+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/pdg_types/Pdg_types.ml b/src/plugins/pdg/pdg_types/Pdg_types.ml
new file mode 100644
index 0000000000000000000000000000000000000000..a27209b47941a8551ffbe793be5f98d714307ea5
--- /dev/null
+++ b/src/plugins/pdg/pdg_types/Pdg_types.ml
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module PdgIndex = PdgIndex
+module PdgMarks = PdgMarks
+module PdgTypes = PdgTypes
diff --git a/src/plugins/pdg/pdg_types/Pdg_types.mli b/src/plugins/pdg/pdg_types/Pdg_types.mli
new file mode 100644
index 0000000000000000000000000000000000000000..edc3a0fd49034f42631a26719c9338ac75e292ce
--- /dev/null
+++ b/src/plugins/pdg/pdg_types/Pdg_types.mli
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module PdgIndex: module type of PdgIndex
+module PdgMarks: module type of PdgMarks
+module PdgTypes: module type of PdgTypes
+
+(**************************************************************************)
diff --git a/src/plugins/pdg/pdg_types/dune b/src/plugins/pdg/pdg_types/dune
new file mode 100644
index 0000000000000000000000000000000000000000..722fae390011c23904d8646cfcfbd7e30f6c06e4
--- /dev/null
+++ b/src/plugins/pdg/pdg_types/dune
@@ -0,0 +1,40 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; 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). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Pdg-Types:" %{lib-available:frama-c-pdg.types.core} "\n")
+ )
+ )
+)
+
+( library
+ (name Pdg_types)
+ (optional)
+ (public_name frama-c-pdg.types.core)
+ (flags -open Frama_c_kernel :standard -w -9)
+ (libraries frama-c.kernel)
+)
+
+(plugin (optional) (name pdg-types) (libraries frama-c-pdg.types.core) (site (frama-c plugins)))
diff --git a/src/plugins/pdg/pdg_types/frama-c-pdg-types.opam b/src/plugins/pdg/pdg_types/frama-c-pdg-types.opam
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/kernel_externals/pdg_types/pdgIndex.ml b/src/plugins/pdg/pdg_types/pdgIndex.ml
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgIndex.ml
rename to src/plugins/pdg/pdg_types/pdgIndex.ml
diff --git a/src/kernel_externals/pdg_types/pdgIndex.mli b/src/plugins/pdg/pdg_types/pdgIndex.mli
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgIndex.mli
rename to src/plugins/pdg/pdg_types/pdgIndex.mli
diff --git a/src/kernel_externals/pdg_types/pdgMarks.ml b/src/plugins/pdg/pdg_types/pdgMarks.ml
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgMarks.ml
rename to src/plugins/pdg/pdg_types/pdgMarks.ml
diff --git a/src/kernel_externals/pdg_types/pdgMarks.mli b/src/plugins/pdg/pdg_types/pdgMarks.mli
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgMarks.mli
rename to src/plugins/pdg/pdg_types/pdgMarks.mli
diff --git a/src/kernel_externals/pdg_types/pdgTypes.ml b/src/plugins/pdg/pdg_types/pdgTypes.ml
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgTypes.ml
rename to src/plugins/pdg/pdg_types/pdgTypes.ml
diff --git a/src/kernel_externals/pdg_types/pdgTypes.mli b/src/plugins/pdg/pdg_types/pdgTypes.mli
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgTypes.mli
rename to src/plugins/pdg/pdg_types/pdgTypes.mli
diff --git a/src/plugins/pdg/register.ml b/src/plugins/pdg/register.ml
index 4f707e7ffeb43572c405893f74411acb98b2b560..8217fb8ccc0794e95ec2b72c7178730c50fa990c 100644
--- a/src/plugins/pdg/register.ml
+++ b/src/plugins/pdg/register.ml
@@ -20,104 +20,18 @@
(* *)
(**************************************************************************)
-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
+open Pdg_types
-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 +44,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 +65,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/pdg/register.mli b/src/plugins/pdg/register.mli
index a99bfbabb26f9923ead07b600345bf705b0b6757..a7f49285d2960e715b6059dcd0fbfc316c2c6360 100644
--- a/src/plugins/pdg/register.mli
+++ b/src/plugins/pdg/register.mli
@@ -20,4 +20,4 @@
(* *)
(**************************************************************************)
-include module type of Marks
+(* empty *)
diff --git a/src/plugins/pdg/sets.ml b/src/plugins/pdg/sets.ml
index 275477477b083ab80dca3d0e8df4ae8a95a30e96..846b30c2540db37082090965d0a76a07d422b553 100644
--- a/src/plugins/pdg/sets.ml
+++ b/src/plugins/pdg/sets.ml
@@ -23,6 +23,8 @@
(** Provides function to extract information from the PDG. *)
open Cil_types
+
+open Pdg_types
open PdgIndex
type nodes_and_undef =
diff --git a/src/plugins/pdg/sets.mli b/src/plugins/pdg/sets.mli
index a416d993e6975611bf9612afb1c25d71a28ee41d..27c12193321a174aad89fcd0e57f19643b355c6d 100644
--- a/src/plugins/pdg/sets.mli
+++ b/src/plugins/pdg/sets.mli
@@ -23,6 +23,7 @@
(** PDG (program dependence graph) access functions. *)
open Cil_types
+open Pdg_types
type nodes_and_undef =
(PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option
diff --git a/src/plugins/postdominators/dune b/src/plugins/postdominators/dune
index da173221feddee9605ea27c2754b1cc1f1329343..7b84cb8f931afdbf83851d235a4bcfa6abbd3085 100644
--- a/src/plugins/postdominators/dune
+++ b/src/plugins/postdominators/dune
@@ -25,6 +25,7 @@
(deps (universe))
(action (progn
(echo "Postdominators:" %{lib-available:frama-c-postdominators.core} "\n")
+ (echo " - Pdg-Types:" %{lib-available:frama-c-pdg.types.core} "\n")
(echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
)
)
@@ -35,7 +36,7 @@
(optional)
(public_name frama-c-postdominators.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-eva.core)
+ (libraries frama-c.kernel frama-c-pdg.types.core frama-c-eva.core)
)
(plugin (optional) (name postdominators) (libraries frama-c-postdominators.core) (site (frama-c plugins)))
diff --git a/src/plugins/postdominators/print.ml b/src/plugins/postdominators/print.ml
index 6ff5e94dd085ea9bafddbe2bd0a0f78f66928221..560c6965ce4f43f2a2b87e5e42cdcc93743b106e 100644
--- a/src/plugins/postdominators/print.ml
+++ b/src/plugins/postdominators/print.ml
@@ -23,8 +23,8 @@
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 pretty_stmt fmt s = let open Pdg_types in
+ 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 2e7fbdbdf8694c5424314143013f4681865576b5..b7783e9f5e508440367136109324a5fb629805e9 100644
--- a/src/plugins/scope/defs.ml
+++ b/src/plugins/scope/defs.ml
@@ -27,6 +27,8 @@
open Cil_datatype
open Cil_types
+open Pdg_types
+
let debug1 fmt = Datascope.R.debug ~level:1 fmt
module Interproc =
@@ -60,19 +62,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 +101,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 +130,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 +140,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 +154,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 +187,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 95c81426d4f4e3e8411ac1a494d109152f432b38..82e4e62e6002f60ee6ee6b9267438cf6dd4e304e 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 aa02df158d8b3d246e59e501748f8fdf5dd3ae08..ba308e499fa2110d4aef18bbe2f29c18c890d9e8 100644
--- a/src/plugins/scope/zones.ml
+++ b/src/plugins/scope/zones.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
module R = Datascope.R
let debug1 fmt = R.debug ~level:1 fmt
let debug2 fmt = R.debug ~level:2 fmt
@@ -262,7 +264,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 +289,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 +325,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 629fa05f3835588deac0848a4d24514a7f93b89f..e28a649eb889d5ade1e2af1bf5e0072e8607ad8b 100644
--- a/src/plugins/security_slicing/components.ml
+++ b/src/plugins/security_slicing/components.ml
@@ -23,6 +23,8 @@
open Cil_types
open Cil_datatype
+open Pdg_types
+
(* ************************************************************************* *)
(** {2 Searching security annotations} *)
(* ************************************************************************* *)
@@ -98,7 +100,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 +248,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 +278,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 +303,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 +358,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 +380,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 +422,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 +450,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 +467,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 +486,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 +513,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 +529,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 +586,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 +625,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 +656,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 +667,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 +857,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 91009d8a81921bc390fd8964c6fdd617c764c233..4e24b20cfd4e2c6103fd71897dc204be5fe01bcb 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/api.mli b/src/plugins/slicing/api.mli
index 2a0af61952fbb5e2b4ef8ed5550aed059a351773..c1b4b19a0d97e6391031f0fb39fb5ac64367937a 100644
--- a/src/plugins/slicing/api.mli
+++ b/src/plugins/slicing/api.mli
@@ -306,6 +306,8 @@ module Select : sig
(** {3 Pdg selectors.} *)
+ open Pdg_types
+
val select_pdg_nodes :
set -> Mark.t -> PdgTypes.Node.t list -> Cil_types.kernel_function -> set
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index b470412386a2539a15b5fd3c3b3fb857fa5de024..43be72e63ec8990bfab89552dde3857cebd463e6 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -41,6 +41,7 @@
(**/**)
open Cil_types
+open Pdg_types
(**/**)
(* Look at (only once) the callers of [kf] ([kf] included). *)
@@ -356,7 +357,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 +419,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 +437,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);
@@ -452,7 +453,7 @@ end = struct
None
in
let new_input_marks =
- Pdg.Register.in_marks_to_caller pdg_caller call m2m in_info in
+ Pdg.Marks.in_marks_to_caller pdg_caller call m2m in_info in
new_input_marks, !new_input
let marks_for_call_outputs (_, out_info) = out_info
@@ -467,7 +468,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 +498,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 +517,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
@@ -524,7 +525,7 @@ end = struct
(if new_out then "(new out)" else "");
m_opt
in let new_called_marks =
- Pdg.Register.call_out_marks_to_called ff_pdg m2m new_call_marks
+ Pdg.Marks.call_out_marks_to_called ff_pdg m2m new_call_marks
in new_called_marks, !new_output
let persistent_in_marks_to_prop fi to_prop =
@@ -532,12 +533,12 @@ 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
let pdg_node_marks =
- Pdg.Register.translate_in_marks pdg ~m2m in_info [] in
+ Pdg.Marks.translate_in_marks pdg ~m2m in_info [] in
pdg_node_marks
let get_new_marks ff nodes_marks =
@@ -546,13 +547,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 +572,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 +588,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 +597,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 +610,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 +635,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 +664,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 +1001,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 +1233,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/fct_slice.mli b/src/plugins/slicing/fct_slice.mli
index 6ea3a114edbdc847d41731dc0d04e4ec1dd20157..a6dd86470f6aa83f972912dad981089fbfeb2468 100644
--- a/src/plugins/slicing/fct_slice.mli
+++ b/src/plugins/slicing/fct_slice.mli
@@ -23,6 +23,8 @@
open SlicingInternals
open Cil_types
+open Pdg_types
+
(** Return [true] if the source function is called
* (even indirectly via transitivity) from a [Slice.t]. *)
val is_src_fun_called :
diff --git a/src/plugins/slicing/printSlice.ml b/src/plugins/slicing/printSlice.ml
index faa275ee37bf95e7489066f89220042821c4e219..535e841b34be8791091c1f102f0074fafb09fa86 100644
--- a/src/plugins/slicing/printSlice.ml
+++ b/src/plugins/slicing/printSlice.ml
@@ -26,6 +26,8 @@
open Cil_types
+open Pdg_types
+
(**/**)
let find_sub_stmts st = match st.skind with
@@ -334,7 +336,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/printSlice.mli b/src/plugins/slicing/printSlice.mli
index dbf55bac1d788e64a6a64727a937478b5402a153..f3ad3570b12b39cc771b39339d2277b03384d5ba 100644
--- a/src/plugins/slicing/printSlice.mli
+++ b/src/plugins/slicing/printSlice.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
val print_fct_from_pdg :
Format.formatter ->
?ff:SlicingInternals.fct_slice -> PdgTypes.Pdg.t -> unit
diff --git a/src/plugins/slicing/slicingActions.ml b/src/plugins/slicing/slicingActions.ml
index 3529e42201527f028e136480bc7018d6c08d738a..0f8410e0446c633e8f855b3425c5993cfa613999 100644
--- a/src/plugins/slicing/slicingActions.ml
+++ b/src/plugins/slicing/slicingActions.ml
@@ -27,6 +27,8 @@
(**/**)
+open Pdg_types
+
type select = SlicingTypes.sl_mark PdgMarks.select
type n_or_d_marks = (SlicingInternals.node_or_dpds * SlicingInternals.pdg_mark) list
@@ -156,10 +158,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 +184,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 +208,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 975252aaa930ef6d2fe39aa93fe626a20a5c655a..081e5bbb6822e1adb85919bfc86037cb7b9a62f6 100644
--- a/src/plugins/slicing/slicingActions.mli
+++ b/src/plugins/slicing/slicingActions.mli
@@ -22,6 +22,9 @@
open SlicingTypes
open Cil_types
+
+open Pdg_types
+
open SlicingInternals
type select = sl_mark PdgMarks.select
@@ -43,7 +46,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/slicingCmds.mli b/src/plugins/slicing/slicingCmds.mli
index a54c67ba31adc7806433769f1d1ca5cb56d70666..693aa337f1c05aa23fbf27b9680e3a132ab2c66b 100644
--- a/src/plugins/slicing/slicingCmds.mli
+++ b/src/plugins/slicing/slicingCmds.mli
@@ -22,6 +22,8 @@
open Cil_types
+open Pdg_types
+
(* TODO: This .mli exists mainly to avoid problems with 'make -j'. This API
is too vast and must be simplified. For example, functions should not
receive variables as names (ie. strings) but directly as zones, possibly
diff --git a/src/plugins/slicing/slicingInternals.ml b/src/plugins/slicing/slicingInternals.ml
index 4169f6937d3d208c157d24e958faf9d96b4aea93..df18b5d589c2cbff6be1b02017156f92ce4478fa 100644
--- a/src/plugins/slicing/slicingInternals.ml
+++ b/src/plugins/slicing/slicingInternals.ml
@@ -27,6 +27,8 @@
open Cil_datatype
+open Pdg_types
+
(** {3 About options} *)
(** associate a level to each function in order to control how it will be
diff --git a/src/plugins/slicing/slicingInternals.mli b/src/plugins/slicing/slicingInternals.mli
index 0e6dc51a49ccfd353bbe3d0e3c6729e68a48eb96..2c7de6f72a77653826a563428b842f379e2d204c 100644
--- a/src/plugins/slicing/slicingInternals.mli
+++ b/src/plugins/slicing/slicingInternals.mli
@@ -27,6 +27,8 @@
open Cil_datatype
+open Pdg_types
+
(** {3 About options} *)
(** associate a level to each function in order to control how it will be
diff --git a/src/plugins/slicing/slicingMacros.ml b/src/plugins/slicing/slicingMacros.ml
index d221c7299c34279593def3da2e49322dd59c3e88..56dc2b438bd9b2024a9d642932e6aef85e96230b 100644
--- a/src/plugins/slicing/slicingMacros.ml
+++ b/src/plugins/slicing/slicingMacros.ml
@@ -28,6 +28,8 @@
open Cil_types
+open Pdg_types
+
(**/**)
(** {2 Options} *)
@@ -127,7 +129,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 04e20ee753e5287e06af6884d83120043d6c562b..427b60450b8ccffe98994cb4c62dac41866746a0 100644
--- a/src/plugins/slicing/slicingMacros.mli
+++ b/src/plugins/slicing/slicingMacros.mli
@@ -24,6 +24,8 @@
functions below should be inlined, as there is no good reason to treat
those types as semi-private *)
+open Pdg_types
+
open SlicingInternals
val str_level_option : level_option -> string
@@ -40,8 +42,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/slicingMarks.ml b/src/plugins/slicing/slicingMarks.ml
index d32603122c23f6479a4139c1d7f4194016ba25ca..77e2c60002dc6e95b15e94a4df90e970610dc68b 100644
--- a/src/plugins/slicing/slicingMarks.ml
+++ b/src/plugins/slicing/slicingMarks.ml
@@ -22,6 +22,8 @@
(** Everything related with the marks. Mainly quite low level function. *)
+open Pdg_types
+
(**/**)
let debug = false
diff --git a/src/plugins/slicing/slicingMarks.mli b/src/plugins/slicing/slicingMarks.mli
index d398c3967fdaec9c47b1e2aa9a4cbd5fc79a47af..fd4505c96de75d7990f83b99007cd56f8c7f1894 100644
--- a/src/plugins/slicing/slicingMarks.mli
+++ b/src/plugins/slicing/slicingMarks.mli
@@ -22,6 +22,8 @@
open SlicingTypes
+open Pdg_types
+
val bottom_mark : sl_mark
val mk_user_mark : data:bool -> addr:bool -> ctrl:bool -> sl_mark
diff --git a/src/plugins/slicing/slicingProject.ml b/src/plugins/slicing/slicingProject.ml
index 27cca02339737ad74f510c4dfec8679ccc6b8a34..70ee325043535f43c8ae87624cf22f940addbc75 100644
--- a/src/plugins/slicing/slicingProject.ml
+++ b/src/plugins/slicing/slicingProject.ml
@@ -24,6 +24,8 @@
(**/**)
+open Pdg_types
+
module T = SlicingInternals
module M = SlicingMacros
diff --git a/src/plugins/slicing/slicingSelect.ml b/src/plugins/slicing/slicingSelect.ml
index 25b922ab7f417778765b40c4bc8eeb43efc48ae6..cf279d65247463b02cf17fc8c0155f90ea46b625 100644
--- a/src/plugins/slicing/slicingSelect.ml
+++ b/src/plugins/slicing/slicingSelect.ml
@@ -23,6 +23,8 @@
open Cil_types
open Cil_datatype
+open Pdg_types
+
(* ---------------------------------------------------------------------- *)
(** {1 For internal use} *)
@@ -72,7 +74,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 +91,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 +122,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 +140,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 +156,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 +171,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 +185,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 +205,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 +232,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 +241,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 +285,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 +294,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 +304,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 +353,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 +369,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 +377,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 +391,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 c139085e9da9b6f5dd0b7925a88397f5e229405c..f68618af4ab69e2871793680ace383a3a673be89 100644
--- a/src/plugins/slicing/slicingSelect.mli
+++ b/src/plugins/slicing/slicingSelect.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
val check_call : Cil_types.stmt -> bool -> Cil_types.stmt
val print_select :
@@ -69,7 +71,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 +119,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 b51f528fe8b7d7427b7fa06fd95ecb42f94040ca..28991d806423a6408dc7202d49476160cb0c7373 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 5d7b4d1c5282e14d1fcfe0777d92e5d020051606..2915223eec08c36ed39b517038169b951525e899 100644
--- a/src/plugins/slicing/slicingTransform.ml
+++ b/src/plugins/slicing/slicingTransform.ml
@@ -26,6 +26,8 @@
open Cil_types
open Cil
+open Pdg_types
+
(**/**)
module Visibility (SliceName : sig
@@ -138,7 +140,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 +175,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 +244,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 +278,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 +298,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 +318,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/slicing/slicingTypes.ml b/src/plugins/slicing/slicingTypes.ml
index 343d08a8f13a70053957f7cbb3de2133a0394a8c..e370df2269d2401259075c7ed22268b86ea5f6a2 100644
--- a/src/plugins/slicing/slicingTypes.ml
+++ b/src/plugins/slicing/slicingTypes.ml
@@ -22,6 +22,8 @@
(** Slicing module types. *)
+open Pdg_types
+
exception Slicing_Internal_Error of string
exception ChangeCallErr of string
exception PtrCallExpr
diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml
index 860f24fa634864535634f4222a038748df3e161c..7db1fca385b380e152d9e8889c5e2af06be6a8e9 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 b684d758b6bc1fcc216d63385568821a4f334c92..3ac3e1d4ccbea47722282482cdfd82e826cba46f 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 2f0c83674a97d3f143b99a5c84ed36342cbb6ae6..bc433062ccc8929f0be579864f7878a07a6f8cee 100644
--- a/src/plugins/sparecode/spare_marks.ml
+++ b/src/plugins/sparecode/spare_marks.ml
@@ -20,12 +20,14 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
let debug n format = Sparecode_params.debug ~level:n format
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 +124,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 +174,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 +275,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 +283,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 +310,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 +324,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 +359,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/spare_marks.mli b/src/plugins/sparecode/spare_marks.mli
index 92a003570b041fa3cf7509dbaa3efff0b6dae067..d6e60878d7c11c498afe8e03592bf2a2331fb8ff 100644
--- a/src/plugins/sparecode/spare_marks.mli
+++ b/src/plugins/sparecode/spare_marks.mli
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Pdg_types
type proj
type fct
diff --git a/src/plugins/sparecode/transform.ml b/src/plugins/sparecode/transform.ml
index e2280ec81b2c4ad240ddcd1902c29356572e55d9..0e3ae5a6f1b496506585981e777937a9a7ef387a 100644
--- a/src/plugins/sparecode/transform.ml
+++ b/src/plugins/sparecode/transform.ml
@@ -23,6 +23,8 @@
open Cil_types
open Cil
+open Pdg_types
+
module BoolInfo = struct
type proj = Spare_marks.proj
type fct = Spare_marks.fct option * Kernel_function.t
@@ -41,7 +43,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/src/plugins/wp/tests/wp_bts/bts_1586.i b/src/plugins/wp/tests/wp_bts/bts_1586.i
index dab7fc01fe3489960e604ec1a582048561820a0e..510137770e7c34d8dcec9e29899e910519cbaa7e 100644
--- a/src/plugins/wp/tests/wp_bts/bts_1586.i
+++ b/src/plugins/wp/tests/wp_bts/bts_1586.i
@@ -1,54 +1,54 @@
-
-/*@ behavior Bizarre:
- assumes x;
- ensures TRANS: x ==> \result==1 ;
- */
-int compute_bizarre(int x)
-{
- if (x)
- return 1;
- else
- return 2;
-}
-
-/*@ behavior Normal:
- assumes x;
- ensures TRANS: x <==> \result==1 ;
- */
-int compute_normal(int x)
-{
- if (x)
- return 1;
- else
- return 2;
-}
-
-int main_bizarre_KO(int x)
-{
- int trans = compute_bizarre(x);
-
- switch(trans) {
- case 0:
- //@ assert FALSE: \false;
- return -1;
- break;
- default:
- return -1;
- break;
- }
-}
-
-int main_normal_KO(int x)
-{
- int trans = compute_normal(x);
-
- switch(trans) {
- case 0:
- //@ assert FALSE: \false;
- return -1;
- break;
- default:
- return -1;
- break;
- }
-}
+
+/*@ behavior Bizarre:
+ assumes x;
+ ensures TRANS: x ==> \result==1 ;
+ */
+int compute_bizarre(int x)
+{
+ if (x)
+ return 1;
+ else
+ return 2;
+}
+
+/*@ behavior Normal:
+ assumes x;
+ ensures TRANS: x <==> \result==1 ;
+ */
+int compute_normal(int x)
+{
+ if (x)
+ return 1;
+ else
+ return 2;
+}
+
+int main_bizarre_KO(int x)
+{
+ int trans = compute_bizarre(x);
+
+ switch(trans) {
+ case 0:
+ //@ assert FALSE: \false;
+ return -1;
+ break;
+ default:
+ return -1;
+ break;
+ }
+}
+
+int main_normal_KO(int x)
+{
+ int trans = compute_normal(x);
+
+ switch(trans) {
+ case 0:
+ //@ assert FALSE: \false;
+ return -1;
+ break;
+ default:
+ return -1;
+ break;
+ }
+}
diff --git a/src/plugins/wp/tests/wp_bts/ergo_typecheck.i b/src/plugins/wp/tests/wp_bts/ergo_typecheck.i
index 27786043f20fd6d2e90613e767fd3de0deed156c..3a05b9220dd03e2b1b1444e202df0a8a79ab2978 100644
--- a/src/plugins/wp/tests/wp_bts/ergo_typecheck.i
+++ b/src/plugins/wp/tests/wp_bts/ergo_typecheck.i
@@ -1,44 +1,44 @@
-typedef struct
-{
- unsigned int a[2];
- unsigned int b[2];
- unsigned int c;
-} my_type;
-
-my_type var = {0};
-
-/*@
- @ ensures var_divded : var == {\old(var) \with
- @ .a = {\old(var.a) \with
- @ [0] = (unsigned int) 0,
- @ [1] = (unsigned int) 1},
- @ .b = {\old(var.b) \with
- @ [0] = (unsigned int)(\old(var.b[0]) + 1),
- @ [1] = (unsigned int)(\old(var.b[1]) + 2)},
- @ .c = (unsigned int) 5
- @ };
- @
- @ ensures var_inline : var == {\old(var) \with
- @ .a[0] = (unsigned int) 0,
- @ .a[1] = (unsigned int) 1,
- @ .b[0] = (unsigned int)(\old(var.b[0]) + 1),
- @ .b[1] = (unsigned int)(\old(var.b[1]) + 2),
- @ .c = (unsigned int) 5
- @ };
- @
- @ ensures var_unit0 : var.a[0] == 0;
- @ ensures var_unit1 : var.a[1] == 1;
- @ ensures var_unit2 : var.b[0] == (unsigned int)(\old(var.b[0]) + 1);
- @ ensures var_unit3 : var.b[1] == (unsigned int)(\old(var.b[1]) + 2);
- @ ensures var_unit4 : var.c == 5;
- @ assigns var;
- @
- */
-void f()
-{
- var.a[0] = 0u;
- var.a[1] = 1u;
- var.b[0] ++;
- var.b[1] += 2;
- var.c = 5u;
-}
+typedef struct
+{
+ unsigned int a[2];
+ unsigned int b[2];
+ unsigned int c;
+} my_type;
+
+my_type var = {0};
+
+/*@
+ @ ensures var_divded : var == {\old(var) \with
+ @ .a = {\old(var.a) \with
+ @ [0] = (unsigned int) 0,
+ @ [1] = (unsigned int) 1},
+ @ .b = {\old(var.b) \with
+ @ [0] = (unsigned int)(\old(var.b[0]) + 1),
+ @ [1] = (unsigned int)(\old(var.b[1]) + 2)},
+ @ .c = (unsigned int) 5
+ @ };
+ @
+ @ ensures var_inline : var == {\old(var) \with
+ @ .a[0] = (unsigned int) 0,
+ @ .a[1] = (unsigned int) 1,
+ @ .b[0] = (unsigned int)(\old(var.b[0]) + 1),
+ @ .b[1] = (unsigned int)(\old(var.b[1]) + 2),
+ @ .c = (unsigned int) 5
+ @ };
+ @
+ @ ensures var_unit0 : var.a[0] == 0;
+ @ ensures var_unit1 : var.a[1] == 1;
+ @ ensures var_unit2 : var.b[0] == (unsigned int)(\old(var.b[0]) + 1);
+ @ ensures var_unit3 : var.b[1] == (unsigned int)(\old(var.b[1]) + 2);
+ @ ensures var_unit4 : var.c == 5;
+ @ assigns var;
+ @
+ */
+void f()
+{
+ var.a[0] = 0u;
+ var.a[1] = 1u;
+ var.b[0] ++;
+ var.b[1] += 2;
+ var.c = 5u;
+}
diff --git a/tests/pdg/dyn_dpds.ml b/tests/pdg/dyn_dpds.ml
index 716e5067f6a276524b036e8efe28dd061dd235ab..4907cf29314c0d98ef989c991d66b70567bc1493 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 f9759901253978aef39e3675d91663df60b7587e..23c627b3a5bb207fb6a40a3d1ec5fcd793dfbe3e 100644
--- a/tests/pdg/sets.ml
+++ b/tests/pdg/sets.ml
@@ -1,58 +1,57 @@
-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;;
-
-exception Find of varinfo;;
-
-let main _ =
- let f = Globals.Functions.find_by_name "f" in
- let pdg = !Pdg.get f in
-
- (* Uncomment to retrieve sid *)
- (*Kernel.Debug.set 1;;
- Format.eprintf "@[%a@]@." Printer.pp_global (Kernel_function.get_global f);;
- *)
- (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- 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
- pp_nodes "Test [all_uses] stmt1" nodes;
-
- (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let y =
- try
- Globals.Vars.iter (fun v _ -> if v.vname = "y" then raise (Find v));
- assert false
- with Find v ->
- v
- in
-
- 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 (fst (Kernel_function.find_from_sid 11)) ~before:false y_zone
- in
-
- assert (undef = None);
- let y_at_11_nodes = List.map (fun (n,_z) -> n) y_at_11_nodes in
-
- 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 () = pp_nodes "Test [all_dpds] y@11" nodes in
- (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let nodes = !Pdg.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
- in
- let nodes = all_related_nodes pdg y_at_11_nodes in
- pp_nodes "Test [all_related_nodes] y@11" nodes
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-
-let () = Db.Main.extend main
+open Cil_types;;
+
+let pp_nodes msg nodes =
+ Kernel.result "%s" msg ;
+ 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.Api.get f in
+
+ (* Uncomment to retrieve sid *)
+ (*Kernel.Debug.set 1;;
+ Format.eprintf "@[%a@]@." Printer.pp_global (Kernel_function.get_global f);;
+ *)
+ (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+ let stmt_1 = fst (Kernel_function.find_from_sid 1) in (* y = 0 *)
+ 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;
+
+ (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+ let y =
+ try
+ Globals.Vars.iter (fun v _ -> if v.vname = "y" then raise (Find v));
+ assert false
+ with Find v ->
+ v
+ in
+
+ let y_zone = Locations.(enumerate_valid_bits Read (loc_of_varinfo y)) in
+ let y_at_11_nodes, undef = (* y=5 *)
+ Pdg.Api.find_location_nodes_at_stmt
+ pdg (fst (Kernel_function.find_from_sid 11)) ~before:false y_zone
+ in
+
+ assert (undef = None);
+ let y_at_11_nodes = List.map (fun (n,_z) -> n) y_at_11_nodes in
+
+ let () = pp_nodes "Test [find_location_nodes_at_stmt] y@11" 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.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.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
+(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+
+let () = Db.Main.extend main
diff --git a/tests/slicing/libSelect.ml b/tests/slicing/libSelect.ml
index fae01cc8b503d8b9ea25207c7d62c2617596d3aa..8fed3fdca1f1de30f97a13a1bb3d6d358a5197d9 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 ebb0e3e8983bf0c210980e6700575ac75ff6f5ab..80fbe7ad12575a7cf978e0441508b3fec992676d 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 c3dec000e6239395812460cca35e5dd40299bcda..39e3e6d67a0bbda7190384523b629ca7b7ba20b9 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 f9e17c3b87c76683424ec6fc3679609606e3beac..7a7e189a1c90ae91ae2a9165430481ed0d3d05d7 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 =
diff --git a/tests/spec/const_ptr_bts1729.i b/tests/spec/const_ptr_bts1729.i
index e2231335e0454d2586897f1552b3eac698e88e87..cb6ef2c2f0fe442b5bcd69f4714ec14f65cd0c73 100644
--- a/tests/spec/const_ptr_bts1729.i
+++ b/tests/spec/const_ptr_bts1729.i
@@ -1,4 +1,4 @@
-
-static void elem_size(void) {
- //@ assert \valid_read((char const * const *)0);
-}
+
+static void elem_size(void) {
+ //@ assert \valid_read((char const * const *)0);
+}
diff --git a/tests/syntax/copy_visitor_bts_1073_bis.ml b/tests/syntax/copy_visitor_bts_1073_bis.ml
index d26b1010abf5ca0abdc6ed8c1f089c43bc39291c..7f6abc845200d0eceff40365c3c812cd702b3632 100644
--- a/tests/syntax/copy_visitor_bts_1073_bis.ml
+++ b/tests/syntax/copy_visitor_bts_1073_bis.ml
@@ -1,55 +1,55 @@
-(*============================================================================*)
-module P = Plugin.Register
- (struct
- let name = "Testing plugin"
- let shortname = "test"
- let help = "Just to test Filter..."
- end)
-module Opt = P.False
- (struct
- let option_name = "-test"
- let help = "switch the plug-in on"
- end)
-(*============================================================================*)
-module Visi = struct
- exception EraseAssigns
- exception EraseAllocation
+(*============================================================================*)
+module P = Plugin.Register
+ (struct
+ let name = "Testing plugin"
+ let shortname = "test"
+ let help = "Just to test Filter..."
+ end)
+module Opt = P.False
+ (struct
+ let option_name = "-test"
+ let help = "switch the plug-in on"
+ end)
+(*============================================================================*)
+module Visi = struct
+ exception EraseAssigns
+ exception EraseAllocation
- type fct = unit
- type proj = unit
+ type fct = unit
+ type proj = unit
- let fct_name vf _fi = vf.Cil_types.vname
- let fct_info () _ = [ () ]
- let param_visible _ _ = true
- let body_visible _fi = true
- let loc_var_visible _ _ = true
- let inst_visible _ _ = true
- let label_visible _ _ _ = true
- let annotation_visible _ _ _ = true
- let fun_precond_visible _ _ = true
- let fun_postcond_visible _ _ = true
- let fun_variant_visible _ _ = true
- let fun_frees_visible _ _ = true
- let fun_allocates_visible _ _ = true
- let fun_assign_visible _ _ = true
- let fun_deps_visible _ _ = true
- let called_info _ _ = None
- let res_call_visible _ _ = true
- let result_visible _ _ = true
- let cond_edge_visible _ _ = true, true
-end
-(*============================================================================*)
-let main () =
- if Opt.get () then
- begin
- let _ast = Ast.get () in
- P.feedback "start compute";
- let new_proj_name = "filtered" in
- let module Transform = Filter.F (Visi) in
- let new_prj = Transform.build_cil_file new_proj_name () in
- Project.on new_prj Opt.clear ();
- P.feedback "exported in new project : %s" new_proj_name
- end
+ let fct_name vf _fi = vf.Cil_types.vname
+ let fct_info () _ = [ () ]
+ let param_visible _ _ = true
+ let body_visible _fi = true
+ let loc_var_visible _ _ = true
+ let inst_visible _ _ = true
+ let label_visible _ _ _ = true
+ let annotation_visible _ _ _ = true
+ let fun_precond_visible _ _ = true
+ let fun_postcond_visible _ _ = true
+ let fun_variant_visible _ _ = true
+ let fun_frees_visible _ _ = true
+ let fun_allocates_visible _ _ = true
+ let fun_assign_visible _ _ = true
+ let fun_deps_visible _ _ = true
+ let called_info _ _ = None
+ let res_call_visible _ _ = true
+ let result_visible _ _ = true
+ let cond_edge_visible _ _ = true, true
+end
+(*============================================================================*)
+let main () =
+ if Opt.get () then
+ begin
+ let _ast = Ast.get () in
+ P.feedback "start compute";
+ let new_proj_name = "filtered" in
+ let module Transform = Filter.F (Visi) in
+ let new_prj = Transform.build_cil_file new_proj_name () in
+ Project.on new_prj Opt.clear ();
+ P.feedback "exported in new project : %s" new_proj_name
+ end
-let () = Db.Main.extend main
-(*============================================================================*)
+let () = Db.Main.extend main
+(*============================================================================*)
diff --git a/tests/syntax/duplicated_global_bts1129.i b/tests/syntax/duplicated_global_bts1129.i
index b95f7dfed63c40ac468c5af75edf3b4f1d7ef84b..b8ac93ff233a19e3dcd95c1d12e7297ff4c9668e 100644
--- a/tests/syntax/duplicated_global_bts1129.i
+++ b/tests/syntax/duplicated_global_bts1129.i
@@ -1,7 +1,7 @@
-void f(int* x);
-
-void f(int* x) { *x++; }
-
-int X;
-//@ ensures X==1;
-void f(int* x);
+void f(int* x);
+
+void f(int* x) { *x++; }
+
+int X;
+//@ ensures X==1;
+void f(int* x);