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.
typet =
PdgTypes.Pdg.t
PDG type
typet_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
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
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.
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.
Not_found
if the output state in unreachableBottom
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.
Not_found
if the output state in unreachableBottom
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).
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.
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
.
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 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)
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.
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.
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
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.
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.
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.
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.
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).
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
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
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
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 :
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.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
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
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
Not_found
if the statement is unreachable.Bottom
if given PDG is bottom.Top
if the given pdg is top.caller_selected_nodes
val direct_dpds : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref
Get the nodes to which the given node directly depend on.
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.
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.
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.
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.
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).
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.
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.
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.
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.
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.
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.
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.
Bottom
if given PDG is bottom.Top
if the given pdg is top.((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
.
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
Bottom
if given PDG is bottom.Top
if the given pdg is top.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
.