module Compute_impact:sig
..end
Initial
module NS: Pdg_aux.NS
typenodes =
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 : |
|
pdg : |
|
zone : |
|
init : |
typetodolist =
todo NM.t
typeresult =
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 : |
(* |
nodes that are impacted, but that have not been
propagated yet.
| *) |
|
mutable 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 : |
(* |
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 : |
(* |
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 : |
(* |
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 : |
(* |
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 : |
(* |
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 for which the impact is
dismissed. Nodes that involve only those zones are skipped. Constant
after initialization
| *) |
|
mutable initial_nodes : |
(* |
Nodes that are part of the initial impact query, or directly
equivalent to those (corresponding nodes in a caller).
| *) |
|
mutable unimpacted_initial : |
(* |
Initial nodes (as defined above) that are not "self-impacting"
so far. Those nodes will not be part of the final results.
| *) |
|
mutable reason : |
(* |
Reasons why nodes in
result are marked as impacted. | *) |
|
compute_reason : |
(* |
compute the field
reason ; may be costly | *) |
val unimpacted_initial_by_kf : worklist -> KFM.key -> NS.t
val result_by_kf : worklist -> KFM.key -> NS.t
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
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
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
true
if the location in n
is contained in skip
, in which
case the node should be skipped entirelyval filter : worklist -> PdgTypes.Node.t * Locations.Zone.t -> bool
val add_to_reason : worklist ->
nsrc:Pdg_aux.node -> ndst:Pdg_aux.node -> Reason_graph.ReasonType.t -> unit
val add_to_do_aux : init:bool ->
worklist ->
Kernel_function.t -> PdgTypes.Pdg.t -> NM.key * Locations.Zone.t -> unit
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
todo
field, from a list of initial nodesval add_to_do_part_of_initial : worklist ->
Kernel_function.t -> PdgTypes.Pdg.t -> Pdg_aux.node -> unit
val add_to_do : worklist ->
Kernel_function.t -> Db.Pdg.t -> Pdg_aux.node -> unit
init = false
to add_to_do_aux
. We
define an alias insteadval intraprocedural_one_node : worklist ->
NM.key * Locations.Zone.t -> Kernel_function.t -> Db.Pdg.t -> unit
val add_downward_call : worklist ->
Kernel_function.t * Db.Pdg.t ->
Kernel_function.t * Db.Pdg.t -> Cil_datatype.Stmt.t -> unit
val downward_one_call_node : worklist ->
NM.key * Locations.Zone.t -> Kernel_function.t -> Db.Pdg.t -> unit
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
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
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
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
val initial_worklist : ?skip:Locations.Zone.t ->
?reason:bool -> Pdg_aux.node list -> KFM.key -> worklist
val initial_nodes : skip:Locations.Zone.t ->
Kernel_function.t -> Cil_types.stmt -> PdgTypes.Node.t list
val pick : worklist -> (NM.key * todo) option
val intraprocedural : worklist -> unit
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
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
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
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
val result_to_nodes : result -> nodes
val nodes_to_stmts : NS.t -> Cil_datatype.Stmt.Set.elt list
val stmts_impacted : ?skip:Locations.Zone.t ->
reason:bool ->
Kernel_function.t ->
Cil_datatype.Stmt.t list -> Cil_datatype.Stmt.Set.elt list
val nodes_impacted : ?skip:Locations.Zone.t ->
reason:bool -> KFM.key -> PdgTypes.Node.t list -> nodes
val impact_in_kf : result -> KFM.key -> NS.t
val skip_bases : Base.t list -> Locations.Zone.t
skip
field from a list of variablesval skip : unit -> Locations.Zone.t
skip
field from the -impact-skip
option
computed from the option -impact-skip