module Pdg: sig
.. end
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.
RaisesNot_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.
RaisesNot_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.
RaisesNot_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).
RaisesNot_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.
RaisesBottom
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
.
RaisesNot_found
if the given statement is unreachable.
Bottom
if given PDG is bottom.
Top
if the given pdg is top.
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)
RaisesNot_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.
RaisesNot_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.
RaisesNot_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
RaisesNot_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.
RaisesBottom
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.
RaisesNot_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.
RaisesNot_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.
RaisesNot_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).
RaisesBottom
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
RaisesNot_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
RaisesNot_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
RaisesNot_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.
RaisesNot_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
RaisesNot_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.
RaisesBottom
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.
RaisesBottom
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.
RaisesBottom
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.
RaisesBottom
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.
RaisesBottom
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).
RaisesBottom
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.
RaisesBottom
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.
RaisesBottom
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.
RaisesBottom
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.
RaisesBottom
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.
RaisesBottom
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.
RaisesBottom
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.
RaisesBottom
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
.
RaisesBottom
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
RaisesBottom
if given PDG is bottom.
Top
if the given pdg is top.
Pretty printing
: (t -> string -> unit) Pervasives.ref
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
.