Module Db.Pdg

module Pdg: sig .. end

Program Dependence Graph.


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.

val find_ret_output_node : (t -> PdgTypes.Node.t) Pervasives.ref

Get the node corresponding return stmt.

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.

val find_input_node : (t -> int -> PdgTypes.Node.t) Pervasives.ref

Get the node corresponding to a given input (parameter).

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.

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.

val find_simple_stmt_nodes : (t -> Cil_types.stmt -> PdgTypes.Node.t list) Pervasives.ref

Get the nodes corresponding to the statement. It is usually composed of only one node (see Db.Pdg.find_stmt_node), except for call statement. Be careful that for block statements, it only returns a node corresponding to the elementary stmt (see Db.Pdg.find_stmt_and_blocks_nodes for more)

val find_label_node : (t -> Cil_types.stmt -> Cil_types.label -> PdgTypes.Node.t)
Pervasives.ref

Get the node corresponding to the label.

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.

val find_top_input_node : (t -> PdgTypes.Node.t) Pervasives.ref
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.

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.

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.

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.

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).

val find_call_ctrl_node : (t -> Cil_types.stmt -> PdgTypes.Node.t) Pervasives.ref
val find_call_input_node : (t -> Cil_types.stmt -> int -> PdgTypes.Node.t) Pervasives.ref
val find_call_output_node : (t -> Cil_types.stmt -> PdgTypes.Node.t) Pervasives.ref
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 :

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

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

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.

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.

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.

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.

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.

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).

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.

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.

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.

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.

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.

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.

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.

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.

val iter_nodes : ((PdgTypes.Node.t -> unit) -> t -> unit) Pervasives.ref

apply a given function to all the PDG nodes

Pretty printing

val extract : (t -> string -> unit) Pervasives.ref

Pretty print pdg into a dot file.

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.