Previous  Up  Next

Module Compute_impact

module Compute_impact: sig .. end
Computation of the PDG nodes that are impacted by the "execution" of some initial PDG nodes. This is implemented as a forward inter-procedural analysis on top of the PDG plugin.

Initial


Computation of the PDG nodes that are impacted by the "execution" of some initial PDG nodes. This is implemented as a forward inter-procedural analysis on top of the PDG plugin.
module NS: Pdg_aux.NS
type nodes = NS.t 
module NM: PdgTypes.Node.Map
module KFS: Kernel_function.Hptset
module KFM: Kernel_function.Map
val kfmns_find_default : KFM.key ->
       NS.t KFM.t -> NS.t
type todo = {
   kf : Cil_types.kernel_function;
   pdg : PdgTypes.Pdg.t;
   zone : Locations.Zone.t;
   init : bool;
} 
type todolist = todo NM.t 
type result = nodes KFM.t 
module KfKfCall: Datatype.Triple_with_collections(Kernel_function)(Kernel_function)(Cil_datatype.Stmt)(sig


val module_name : string
end)
type worklist = {
   mutable todo : todolist; (*nodes that are impacted, but that have not been propagated yet.*)
   mutable result : result; (*impacted nodes. This field only grows. An invariant is that nodes in todolist are not already in result, except with differing init fields.*)
   mutable downward_calls : Pdg_aux.call_interface KfKfCall.Map.t; (*calls for which an input may be impacted. If so, we must compute the impact within the called function. For each call, we associate to each PDG input of the callee the nodes that define the input in the caller. The contents of this field grow.*)
   mutable callers : KFS.t; (*all the callers of the functions in which the initial nodes are located. Constant after initialization, used to initialize upward_calls below.*)
   mutable upward_calls : Pdg_aux.call_interface Lazy.t KfKfCall.Map.t; (*calls for which an output may be impacted. If so, we must compute the impact after the call in the caller (which is part of the callers field by construction). For each output node at the call point in the caller, associate all the nodes of the callee that define this output. The field is lazy: if the impact "dies" before before reaching the call, we may avoid a costly computation. Constant once initialized.*)
   mutable fun_changed_downward : KFS.t; (*Functions in which a new pdg node has been found since the last iteration. The impact on downward calls with those callers will have to be computed again.*)
   mutable fun_changed_upward : KFS.t; (*Functions in which a new pdg node has been found. The impact on upward calls to those callees will have to be computed again.*)
   mutable skip : Locations.Zone.t; (*Locations for which the impact is dismissed. Nodes that involve only those zones are skipped. Constant after initialization*)
   mutable initial_nodes : nodes KFM.t; (*Nodes that are part of the initial impact query, or directly equivalent to those (corresponding nodes in a caller).*)
   mutable unimpacted_initial : nodes KFM.t; (*Initial nodes (as defined above) that are not "self-impacting" so far. Those nodes will not be part of the final results.*)
   mutable reason : Reason_graph.reason_graph; (*Reasons why nodes in result are marked as impacted.*)
   compute_reason : bool; (*compute the field reason; may be costly*)
}
Worklist maintained by the plugin to build its results
val unimpacted_initial_by_kf : worklist -> KFM.key -> NS.t
Extract the node of the kf that are only part of the initial impact
val result_by_kf : worklist -> KFM.key -> NS.t
Extract the current results for a given function
val result_to_node_origin : result -> Reason_graph.nodes_origin
val initial_to_node_set : nodes KFM.t -> NS.t
val remove_from_unimpacted_initial : worklist ->
       KFM.key -> PdgTypes.Node.t * Locations.Zone.t -> unit
Mark that n comes from an indirect impact, ie. remove it from the set of initial nodes that are not impacted.
val add_to_result : worklist ->
       Pdg_aux.node -> KFM.key -> bool -> unit
Add a node to the sets of impacted nodes. Update the various fields of the worklist that need it. init indicates that the node is added only because it belongs to the set of initial nodes.
val node_to_skip : Locations.Zone.t -> PdgTypes.Node.t -> bool
return true if the location in n is contained in skip, in which case the node should be skipped entirely
val filter : worklist -> PdgTypes.Node.t * Locations.Zone.t -> bool
Auxiliary function, used to refuse some nodes that should not go in the results
val add_to_reason : worklist ->
       nsrc:Pdg_aux.node -> ndst:Pdg_aux.node -> Reason_graph.ReasonType.t -> unit
Add a new edge in the graph explaining the results
val add_to_do_aux : init:bool ->
       worklist ->
       Kernel_function.t ->
       PdgTypes.Pdg.t -> NM.key * Locations.Zone.t -> unit
Add some nodes to the todo field of the worklist, while enforcing some invariants. Some kind of pdg nodes must not appear in it, plus the nodes must not be in result already.
val initial_to_do_list : worklist ->
       Kernel_function.t ->
       PdgTypes.Pdg.t -> (NM.key * Locations.Zone.t) list -> unit
Build the initial value of the todo field, from a list of initial nodes
val add_to_do_part_of_initial : worklist ->
       Kernel_function.t -> PdgTypes.Pdg.t -> Pdg_aux.node -> unit
Mark a new node as impacted, and simultaneouly mark that it is equivalent to nodes that are all initial nodes
val add_to_do : worklist ->
       Kernel_function.t -> Db.Pdg.t -> Pdg_aux.node -> unit
From now on, most functions will pass init = false to add_to_do_aux. We define an alias instead
val intraprocedural_one_node : worklist ->
       NM.key * Locations.Zone.t ->
       Kernel_function.t -> Db.Pdg.t -> unit
Purely intra-procedural propagation from one impacted node. Just follow the PDG once, for all kind of dependencies.
val add_downward_call : worklist ->
       Kernel_function.t * Db.Pdg.t ->
       Kernel_function.t * Db.Pdg.t -> Cil_datatype.Stmt.t -> unit
Add a downward call to the worklist the first time it is encountered. This functions implicitly caches the mapping from the PDG nodes of the caller to the ones of the callee, as this information is expensive to compute
val downward_one_call_node : worklist ->
       NM.key * Locations.Zone.t ->
       Kernel_function.t -> Db.Pdg.t -> unit
Propagate impact from node node if it corresponds to a call statement. This is a partially inter-procedural propagation: some nodes of the callee are directly in the worklist, and the call is registered in the field downward_calls.
val zone_restrict : NS.t -> Locations.Zone.t
val downward_one_call_inputs : worklist ->
       KFM.key ->
       Kernel_function.t -> PdgTypes.Node.t * NS.t -> unit
Propagate impact for one call registered in downward_calls. If the set of impacted nodes in the caller intersect the nodes deps that define the input node of the call, add node to the impacted nodes.
val downward_calls_inputs : worklist -> unit
Propagate impact for all calls registered in downward_calls. For each caller, if new impacted nodes have been found, try to propagate the call. Then, zero out the list of functions that must be considered again.
val all_upward_callers : worklist -> KFS.t -> unit
Fill out the field upward_calls of the worklist. This is done by visiting (transitively) all the callers of functions in kfs, and registering all the calls found this way. The callers found are added to the field callers. For each find, we find the nodes of the callee that define a given output in the caller using Pdg_aux.all_call_out_nodes. kfs must be all the functions containing the initial nodes of the analysis.
val upward_in_callers : worklist -> unit
Upward propagation in all the callers. For all upward-registered calls, find if new impacted nodes have been found in the callee. If so, check if they intersect with the nodes of the callee defining the output. Then, mark the (caller) output node as impacted. At the end, zero out the list of function that must be examined again.
val initial_worklist : ?skip:Locations.Zone.t ->
       ?reason:bool ->
       Pdg_aux.node list -> KFM.key -> worklist
Compute the initial state of the worklist.
val initial_nodes : skip:Locations.Zone.t ->
       Kernel_function.t -> Cil_types.stmt -> PdgTypes.Node.t list
To compute the impact of a statement, find the initial PDG nodes that must be put in the worklist. The only subtlety consists in skipping input nodes on statements that are calls; otherwise, we would get an impact in the callees of the call.
val pick : worklist ->
       (NM.key * todo) option
Choose one node to process in the todo list, if one remains
val intraprocedural : worklist -> unit
Empty the todo field of the worklist by applying as many basic steps as possible: intra-procedural steps, plus basic inter-procedural steps on downward calls.
val something_to_do : worklist -> bool
val fixpoint : worklist -> unit
Make the worklist reach a fixpoint, by propagating all possible source of impact as much as possible. Due to the way calls are treated (by intersecting new impacted nodes with constant sets of nodes), it is more efficient to saturate the field result before calling downward_calls_inputs and upward_in_callers. We also make sure all downward propagation is done before starting upward propagation.
val remove_unimpacted : 'a ->
       NS.t option ->
       NS.t option -> NS.t option
val impact : ?skip:Locations.Zone.t ->
       ?reason:bool ->
       Pdg_aux.node list ->
       KFM.key ->
       NS.t KFM.t *
       nodes KFM.t *
       nodes KFM.t * Reason_graph.reason_graph
Impact of a set of nodes. Once the worklist has reached its fixpoint, remove the initial nodes that are not self-impacting from the result, and return this result.
val nodes_impacted_by_nodes : ?skip:Locations.Zone.t ->
       ?restrict:Locations.Zone.t ->
       ?reason:bool ->
       KFM.key ->
       PdgTypes.Node.t list ->
       NS.t KFM.t *
       nodes KFM.t * Reason_graph.reason
Impact of a list of PDG nodes coming from the same function
val nodes_impacted_by_stmts : ?skip:Locations.Zone.t ->
       ?restrict:Locations.Zone.t ->
       ?reason:bool ->
       Kernel_function.t ->
       Cil_datatype.Stmt.t list ->
       NS.t KFM.t *
       nodes KFM.t * Reason_graph.reason
Impact of a list stmts coming from the same function
val result_to_nodes : result -> nodes
Transform the result of an analysis into a set of PDG nodes
val nodes_to_stmts : NS.t -> Cil_datatype.Stmt.Set.elt list
Transform a set of PDG nodes into a set of statements
val stmts_impacted : ?skip:Locations.Zone.t ->
       reason:bool ->
       Kernel_function.t ->
       Cil_datatype.Stmt.t list -> Cil_datatype.Stmt.Set.elt list
Impact of a list of statements as a set of statements
val nodes_impacted : ?skip:Locations.Zone.t ->
       reason:bool ->
       KFM.key -> PdgTypes.Node.t list -> nodes
Impact of a list of PDG nodes as a set of nodes
val impact_in_kf : result -> KFM.key -> NS.t
Nodes impacted in a given function
val skip_bases : Base.t list -> Locations.Zone.t
Computation of the skip field from a list of variables
val skip : unit -> Locations.Zone.t
Computation of the skip field from the -impact-skip option

computed from the option -impact-skip