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

Not_found if the variable is not declared in this function.
Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Get the node corresponding return stmt.
Raises

Not_found if the ouptut state in unreachable
Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Not_found if the ouptut state in unreachable
Bottom if given PDG is bottom.
Top if the given pdg is top.

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

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

Not_found if the number is not an input number.
Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Not_found if the given statement is unreachable.
Bottom if given PDG is bottom.
Top if the given pdg is top.
PdgIndex.CallStatement if the given stmt is a function call.

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

Not_found if the given statement is unreachable.
Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Get the node corresponding to the label.
Raises

Not_found if the given label is not in the PDG.
Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Not_found if the given statement is unreachable.
Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Raises

Not_found if there is no top input in the PDG.
Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
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)
       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

Not_found if the given statement is unreachable.
Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Not_found if the output state is unreachable.
Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Not_found if the output state is unreachable.
Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Raises

Not_found if the call is unreachable.
Bottom if given PDG is bottom.
Top if the given pdg is top.

val find_call_input_node : (t -> Cil_types.stmt -> int -> PdgTypes.Node.t) Pervasives.ref

Raises

Not_found if the call is unreachable or has no such input.
Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Raises

Not_found if the call is unreachable or has no output node.
Bottom if given PDG is bottom.
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)
       Pervasives.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.

Raises

Not_found if the statement is unreachable.
Bottom if given PDG is bottom.
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)
       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

Not_found if the statement is unreachable.
Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

Bottom if given PDG is bottom.
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)
       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

Bottom if given PDG is bottom.
Top if the given pdg is top.

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

apply a given function to all the PDG nodes
Raises

Bottom if given PDG is bottom.
Top if the given pdg is top.

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.