Module Sets

module Sets: sig .. end
Provides function to extract information from the PDG.

PDG (program dependence graph) access functions.


type nodes_and_undef = (PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option 
val get_init_state : PdgTypes.Pdg.t -> PdgTypes.data_state
val get_last_state : PdgTypes.Pdg.t -> PdgTypes.data_state
Raises Not_found when no last state (strange !)
val get_stmt_state : PdgTypes.Pdg.t -> Cil_types.stmt -> PdgTypes.data_state
Raises Not_found for unreachable stmt
val find_node : PdgTypes.Pdg.t -> PdgIndex.Key.t -> PdgTypes.Node.t
val find_simple_stmt_nodes : PdgTypes.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t list
notice that there can be several nodes if the statement is a call. For If, Switch, ... the node represent only the condition (see find_stmt_nodes below).
val add_stmt_nodes : PdgTypes.Pdg.t ->
PdgTypes.Node.t list -> Cil_types.stmt -> PdgTypes.Node.t list
val find_stmt_and_blocks_nodes : PdgTypes.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t list
notice that there can be several nodes if the statement is a call. If the stmt is a composed instruction (block, etc), all the nodes of the enclosed statements are considered.
val find_stmt_node : PdgTypes.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t
val find_entry_point_node : PdgTypes.Pdg.t -> PdgTypes.Node.t
val find_top_input_node : PdgTypes.Pdg.t -> PdgTypes.Node.t
val find_loc_nodes : PdgTypes.Pdg.t ->
PdgTypes.data_state ->
Locations.Zone.t ->
(PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option
val find_location_nodes_at_stmt : PdgTypes.Pdg.t ->
Cil_types.stmt ->
before:bool ->
Locations.Zone.t ->
(PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option
val find_location_nodes_at_end : PdgTypes.Pdg.t ->
Locations.Zone.t ->
(PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option
val find_location_nodes_at_begin : PdgTypes.Pdg.t ->
Locations.Zone.t ->
(PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option
val find_label_node : PdgTypes.Pdg.t -> Cil_types.stmt -> Cil_types.label -> PdgTypes.Node.t
val find_decl_var_node : PdgTypes.Pdg.t -> Cil_types.varinfo -> PdgTypes.Node.t
val find_output_node : PdgTypes.Pdg.t -> PdgTypes.Node.t
val find_input_node : PdgTypes.Pdg.t -> int -> PdgTypes.Node.t
val find_all_input_nodes : PdgTypes.Pdg.t -> PdgTypes.Node.t list
val find_call_input_nodes : PdgTypes.Pdg.t ->
Cil_types.stmt ->
PdgIndex.Signature.in_key ->
(PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option
val find_call_ctrl_node : PdgTypes.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t
val find_call_num_input_node : PdgTypes.Pdg.t -> Cil_types.stmt -> int -> PdgTypes.Node.t
val find_call_output_node : PdgTypes.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t
val find_output_nodes : PdgTypes.Pdg.t ->
PdgIndex.Signature.out_key ->
(PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option
val find_call_stmts : Cil_types.kernel_function -> caller:Kernel_function.t -> Cil_types.stmt list

Build sets of nodes

This parts groups the functions that build sets from the pdg. Made to answer user questions rather that to build slice marks, because efficient marking doesn't need to build this sets. However, it might be useful to prove that it is the same...

val add_node_in_list : PdgTypes.Node.t -> PdgTypes.Node.t list -> PdgTypes.Node.t list * bool
add the node in the list if it is not already in.
val add_node_and_custom_dpds : (PdgTypes.Node.t -> PdgTypes.Node.t list) ->
PdgTypes.Node.t list -> PdgTypes.Node.t -> PdgTypes.Node.t list
add the node to the list. It it wasn't already in the list, recursively call the same function on the successors or/and predecessors according to the flags.
val add_nodes_and_custom_dpds : (PdgTypes.Node.t -> PdgTypes.Node.t list) ->
PdgTypes.Node.t list -> PdgTypes.Node.t list -> PdgTypes.Node.t list
val custom_related_nodes : (PdgTypes.Node.t -> PdgTypes.Node.t list) ->
PdgTypes.Node.t list -> PdgTypes.Node.t list
val filter_nodes : ('a * 'b) list -> 'a list
we ignore z_part for the moment. TODO ?

Backward

build sets of the dependencies of given nodes
val direct_dpds : PdgTypes.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list
gives the list of nodes that the given node depends on, without looking at the kind of dependency.

direct dependencies only: This means the nodes that have an edge to the given node.

val direct_x_dpds : PdgTypes.Dpd.td -> PdgTypes.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list
gives the list of nodes that the given node depends on, with a given kind of dependency.
val direct_data_dpds : PdgTypes.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list
val direct_ctrl_dpds : PdgTypes.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list
val direct_addr_dpds : PdgTypes.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list

accumulates in node_list the results of add_node_and_dpds_or_codpds for all the nodes
val find_nodes_all_x_dpds : PdgTypes.Dpd.td ->
PdgTypes.Pdg.t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
val find_nodes_all_dpds : PdgTypes.Pdg.t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
val find_nodes_all_data_dpds : PdgTypes.Pdg.t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
val find_nodes_all_ctrl_dpds : PdgTypes.Pdg.t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
val find_nodes_all_addr_dpds : PdgTypes.Pdg.t -> PdgTypes.Node.t list -> PdgTypes.Node.t list

Forward

build sets of the nodes that depend on given nodes
val direct_uses : PdgTypes.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list
Returns the list of nodes that directly depend on the given node
val direct_x_uses : PdgTypes.Dpd.td -> PdgTypes.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list
val direct_data_uses : PdgTypes.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list
val direct_ctrl_uses : PdgTypes.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list
val direct_addr_uses : PdgTypes.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list
val all_uses : PdgTypes.Pdg.t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
Returns a list containing all the nodes that depend on the given nodes.

Others


val find_call_out_nodes_to_select : PdgTypes.Pdg.t ->
PdgTypes.NodeSet.t ->
PdgTypes.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t list
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 : PdgTypes.Pdg.t ->
PdgTypes.NodeSet.t ->
Cil_types.stmt -> PdgTypes.Pdg.t -> PdgTypes.Node.t list