module Fct_slice:sig
..end
true
if the source function is called
(even indirectly via transitivity) from a Slice.t
.
This module deals with slice computation.
It computes a mapping between the PDG nodes and some marks
(see Fct_slice.FctMarks
),
and also manage interprocedural propagation (Fct_slice.CallInfo
).
Most high level function, named apply_xxx
,
like apply_change_call
, apply_missing_outputs
, ...,
correspond the actions defined in the
specification report.
Many functions are modifying the marks of a slice, so they can return a list of actions to be applied in order to deal with the propagation in the calls and callers.
Moreover, some function (named get_xxx_mark
) are provided to retrieve
the mark of the slice elements.
val is_src_fun_called : Cil_types.kernel_function -> bool
true
if the source function is called
(even indirectly via transitivity) from a Slice.t
.val is_src_fun_visible : Cil_types.kernel_function -> bool
true
if the source function is visible
(even indirectly via transitivity) from a Slice.t
.SlicingTypes.ExternalFunction
if the function has no source code,
because there cannot be any slice for it.SlicingTypes.NoPdg
when there is no PDG for the function.val make_new_ff : SlicingInternals.fct_info ->
bool -> SlicingInternals.fct_slice * SlicingInternals.criterion list
fct_info
.
If the function has some persistent selection, let's copy it in the new slice.
Notice that there can be at most one slice for the application entry point
(main), but we allow to have several slice for a library entry point.
SlicingTypes.NoPdg
(see new_slice
)build_actions
: (bool) is useful if the function has some persistent
selection : if the new slice marks will be modified just after that,
it is not useful to do examine_calls
, but if it is finished,
we must generate those actions to choose the calls.val merge_slices : SlicingInternals.fct_slice ->
SlicingInternals.fct_slice ->
SlicingInternals.fct_slice * SlicingInternals.criterion list
ff1
marks and ff2
marks. The result ff
is not called at the end of this action.
examine_calls
is called to generate the actions to choose the calls.val copy_slice : SlicingInternals.fct_slice -> SlicingInternals.fct_slice
val filter_already_in : SlicingInternals.fct_slice ->
SlicingInternals.fct_base_criterion -> SlicingInternals.fct_base_criterion
nodes_marks
are already in the slice or not.
nodes_marks
that are not already in.val apply_add_marks : SlicingInternals.fct_slice ->
SlicingInternals.fct_base_criterion -> SlicingInternals.criterion list
val add_marks_to_fi : SlicingInternals.fct_info ->
SlicingInternals.fct_base_criterion ->
bool ->
SlicingInternals.criterion list -> bool * SlicingInternals.criterion list
propagate=true
, also generates the actions to make every calls to this
function visible.val add_top_mark_to_fi : SlicingInternals.fct_info ->
SlicingInternals.pdg_mark ->
bool -> SlicingInternals.criterion list -> SlicingInternals.criterion list
val check_outputs_before_change_call : SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.fct_slice -> SlicingInternals.criterion list
change_call
to a function that doesn't
compute enough outputs, he can call check_outputs_before_change_call
in
order to build the action the add those outputs.val apply_change_call : SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.called_fct -> SlicingInternals.criterion list
f_to_call
is ok for this call, and if so,
change the function call and propagate missing marks in the inputs
if needed.
ChangeCallErr
if f_to_call
doesn't compute enough outputs.val apply_choose_call : SlicingInternals.fct_slice ->
Cil_types.stmt -> SlicingInternals.criterion list
choose_call
for the same call, and we want to do something only the first time.
Build an action change_call
to really call it.
If the chosen function doesn't compute enough output,
build an action to add outputs to it.
val apply_missing_inputs : SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.fct_base_criterion * bool -> SlicingInternals.criterion list
ff
calls a slice g
that needs more inputs than those computed by ff
.
The slicing level of ff
is used in order to know if we have to modify ff
or to call another function.val apply_missing_outputs : SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.fct_base_criterion ->
bool -> SlicingInternals.criterion list
ff
calls a slice g
that doesn't compute enough outputs for the call
.
The missing marks are output_marks
.
The slicing level has to be used to choose either to modify the called
function g
or to change it.val apply_examine_calls : SlicingInternals.fct_slice ->
SlicingInternals.pdg_mark PdgMarks.info_called_outputs ->
SlicingInternals.criterion list
val get_called_slice : SlicingInternals.fct_slice ->
Cil_types.stmt -> SlicingInternals.fct_slice option * bool
val get_node_mark : SlicingInternals.fct_slice -> PdgTypes.Node.t -> SlicingInternals.pdg_mark
val get_node_key_mark : SlicingInternals.fct_slice -> PdgIndex.Key.t -> SlicingInternals.pdg_mark
val get_top_input_mark : SlicingInternals.fct_info -> SlicingInternals.pdg_mark
val get_stmt_mark : SlicingInternals.fct_slice -> Cil_types.stmt -> SlicingInternals.pdg_mark
val get_label_mark : SlicingInternals.fct_slice ->
Cil_types.stmt -> Cil_types.label -> SlicingInternals.pdg_mark
val get_param_mark : SlicingInternals.fct_slice -> int -> SlicingInternals.pdg_mark
val get_local_var_mark : SlicingInternals.fct_slice -> Cil_types.varinfo -> SlicingInternals.pdg_mark
val get_input_loc_under_mark : SlicingInternals.fct_slice -> Locations.Zone.t -> SlicingInternals.pdg_mark
val get_mark_from_src_fun : Kernel_function.t -> SlicingInternals.pdg_mark
m
related to all statements of a source function kf
.
Property : is_bottom (get_from_func kf) = not (is_src_fun_called kf)
val merge_inputs_m1_mark : SlicingInternals.fct_slice -> SlicingInternals.pdg_mark
val clear_ff : SlicingInternals.fct_slice -> unit
ff
has to be removed. We have to check if it is not called
and to remove the called function in ff
.
SlicingTypes.CantRemoveCalledFf
if the slice is called.val print_ff_sig : Format.formatter -> SlicingInternals.fct_slice -> unit