Module Db.Pdg

module Pdg: sig .. end
Program Dependence Graph.
See also PDG internal documentation.

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 Pervasives.ref

Getters


val get : (Cil_types.kernel_function -> t) Pervasives.ref
Get the PDG of a function. Build it if it doesn't exist yet.
val node_key : (PdgTypes.Node.t -> PdgIndex.Key.t) Pervasives.ref
val from_same_fun : t -> t -> bool

Finding PDG nodes


val find_decl_var_node : (t -> Cil_types.varinfo -> PdgTypes.Node.t) Pervasives.ref
Get the node corresponding the declaration of a local variable or a formal parameter.
Raises
val find_ret_output_node : (t -> PdgTypes.Node.t) Pervasives.ref
Get the node corresponding return stmt.
Raises
val find_output_nodes : (t -> PdgIndex.Signature.out_key -> t_nodes_and_undef)
Pervasives.ref
Get the nodes corresponding to a call output key in the called pdg.
Raises
val find_input_node : (t -> int -> PdgTypes.Node.t) Pervasives.ref
Get the node corresponding to a given input (parameter).
Raises
val find_all_inputs_nodes : (t -> PdgTypes.Node.t list) Pervasives.ref
Get the nodes corresponding to all inputs. Db.Pdg.node_key can be used to know their numbers.
Raises
val find_stmt_node : (t -> Cil_types.stmt -> PdgTypes.Node.t) Pervasives.ref
Get the node corresponding to the statement. It shouldn't be a call statement. See also Db.Pdg.find_simple_stmt_nodes or Db.Pdg.find_call_stmts.
Raises
val find_simple_stmt_nodes : (t -> Cil_types.stmt -> PdgTypes.Node.t list) Pervasives.ref
Get the nodes corresponding to the statement. It is usualy composed of only one node (see Db.Pdg.find_stmt_node), except for call statement. Be careful that for block statements, it only retuns a node corresponding to the elementary stmt (see Db.Pdg.find_stmt_and_blocks_nodes for more)
Raises
val find_label_node : (t -> Cil_types.stmt -> Cil_types.label -> PdgTypes.Node.t)
Pervasives.ref
Get the node corresponding to the label.
Raises
val find_stmt_and_blocks_nodes : (t -> Cil_types.stmt -> PdgTypes.Node.t list) Pervasives.ref
Get the nodes corresponding to the statement like Db.Pdg.find_simple_stmt_nodes but also add the nodes of the enclosed statements if stmt contains blocks.
Raises
val find_top_input_node : (t -> PdgTypes.Node.t) Pervasives.ref
Raises
val find_entry_point_node : (t -> PdgTypes.Node.t) Pervasives.ref
Find the node that represent the entry point of the function, i.e. the higher level block.
Raises
val find_location_nodes_at_stmt : (t ->
Cil_types.stmt ->
before:bool -> Locations.Zone.t -> t_nodes_and_undef)
Pervasives.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.
Raises
val find_location_nodes_at_end : (t -> Locations.Zone.t -> t_nodes_and_undef) Pervasives.ref
Same than Db.Pdg.find_location_nodes_at_stmt for the program point located at the end of the function.
Raises
val find_location_nodes_at_begin : (t -> Locations.Zone.t -> t_nodes_and_undef) Pervasives.ref
Same than Db.Pdg.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.
Raises
val find_call_stmts : (Cil_types.kernel_function ->
caller:Cil_types.kernel_function -> Cil_types.stmt list)
Pervasives.ref
Find the call statements to the function (can maybe be somewhere else).
Raises
val find_call_ctrl_node : (t -> Cil_types.stmt -> PdgTypes.Node.t) Pervasives.ref
Raises
val find_call_input_node : (t -> Cil_types.stmt -> int -> PdgTypes.Node.t) Pervasives.ref
Raises
val find_call_output_node : (t -> Cil_types.stmt -> PdgTypes.Node.t) Pervasives.ref
Raises
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)
Pervasives.ref
The result is composed of three parts :
Raises
val find_fun_precond_nodes : (t ->
Cil_types.predicate ->
PdgTypes.Node.t list * t_nodes_and_undef option)
Pervasives.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)
Pervasives.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)
Pervasives.ref
Similar to find_fun_precond_nodes

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)
Pervasives.ref
find_call_out_nodes_to_select pdg_called called_selected_nodes pdg_caller call_stmt
Returns 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)
Pervasives.ref
find_in_nodes_to_select_for_this_call pdg_caller caller_selected_nodes call_stmt pdg_called
Raises Returns the called input nodes such that the corresponding nodes in the caller intersect caller_selected_nodes

Dependencies


val direct_dpds : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref
Get the nodes to which the given node directly depend on.
Raises
val direct_ctrl_dpds : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref
Similar to Db.Pdg.direct_dpds, but for control dependencies only.
Raises
val direct_data_dpds : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref
Similar to Db.Pdg.direct_dpds, but for data dependencies only.
Raises
val direct_addr_dpds : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref
Similar to Db.Pdg.direct_dpds, but for address dependencies only.
Raises
val all_dpds : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) Pervasives.ref
Transitive closure of Db.Pdg.direct_dpds for all the given nodes.
Raises
val all_data_dpds : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) Pervasives.ref
Gives the data dependencies of the given nodes, and recursively, all the dependencies of those nodes (regardless to their kind).
Raises
val all_ctrl_dpds : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) Pervasives.ref
Similar to Db.Pdg.all_data_dpds for control dependencies.
Raises
val all_addr_dpds : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) Pervasives.ref
Similar to Db.Pdg.all_data_dpds for address dependencies.
Raises
val direct_uses : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref
build a list of all the nodes that have direct dependencies on the given node.
Raises
val direct_ctrl_uses : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref
Similar to Db.Pdg.direct_uses, but for control dependencies only.
Raises
val direct_data_uses : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref
Similar to Db.Pdg.direct_uses, but for data dependencies only.
Raises
val direct_addr_uses : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref
Similar to Db.Pdg.direct_uses, but for address dependencies only.
Raises
val all_uses : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) Pervasives.ref
build a list of all the nodes that have dependencies (even indirect) on the given nodes.
Raises
val custom_related_nodes : ((PdgTypes.Node.t -> PdgTypes.Node.t list) ->
PdgTypes.Node.t list -> PdgTypes.Node.t list)
Pervasives.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.
Raises
val iter_nodes : ((PdgTypes.Node.t -> unit) -> t -> unit) Pervasives.ref
apply a given function to all the PDG nodes
Raises

Pretty printing


val extract : (t -> string -> unit) Pervasives.ref
Pretty print pdg into a dot file.
See also PDG internal documentation.
val pretty_node : (bool -> Format.formatter -> PdgTypes.Node.t -> unit) Pervasives.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) Pervasives.ref
Pretty print information on a node key
val pretty : (?bw:bool -> Format.formatter -> t -> unit) Pervasives.ref
For debugging... Pretty print pdg information. Print codependencies rather than dependencies if bw=true.