module Fct_slice:sig
..end
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 retreive
the mark of the slice elements.
Raises
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.module CallInfo:sig
..end
module FctMarks:sig
..end
FctMarks
manages the mapping between a function elements and their
marks.
val get_called_slice : SlicingInternals.fct_slice ->
Cil_types.stmt -> SlicingInternals.fct_slice option * bool
val _pretty_node_marks : Format.formatter -> (PdgTypes.Node.t * SlicingTypes.sl_mark) list -> unit
val check_outputs : CallInfo.call_id ->
SlicingInternals.fct_slice ->
bool -> SlicingTypes.sl_mark PdgMarks.select * bool
val check_ff_called : SlicingInternals.fct_slice ->
Cil_types.stmt ->
(Cil_types.stmt * (PdgIndex.Signature.out_key * SlicingTypes.sl_mark) list)
list -> SlicingInternals.fct_slice -> SlicingInternals.criterion option
ff
marks have changed : check if the call to ff_called
is still ok.val examine_calls : SlicingInternals.fct_slice ->
(Cil_types.stmt * (PdgIndex.Signature.out_key * SlicingTypes.sl_mark) list)
list -> SlicingInternals.criterion list
ff
marks.
If one node is visible we have to choose which function to call,
or to check if it is ok is something is called already.
Returns a list of actions if needed.
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
)
when there is no PDG for the function.
SlicingTypes.ExternalFunction
if the function has no source code,
because there cannot be any slice for it.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 copy_slice : SlicingInternals.fct_slice -> SlicingInternals.fct_slice
val add_missing_inputs_actions : SlicingInternals.fct_slice ->
(SlicingInternals.fct_slice * Cil_datatype.Stmt.t) list ->
FctMarks.to_prop ->
SlicingInternals.criterion list -> SlicingInternals.criterion list
ff
marks have just been modified :
check if the calls
to ff
compute enough inputs,
and create MissingInputs
actions if not.val after_marks_modifications : SlicingInternals.fct_slice ->
FctMarks.to_prop -> SlicingInternals.criterion list
ff
marks have been modified : we have to check if the calls and the
callers are ok. Create new actions if there is something to do.
Notice that the action creations are independent from the options.
They will by used during the applications.
val apply_examine_calls : SlicingInternals.fct_slice ->
(Cil_types.stmt * (PdgIndex.Signature.out_key * SlicingTypes.sl_mark) list)
list -> SlicingInternals.criterion list
val add_marks : FctMarks.t ->
SlicingTypes.sl_mark PdgMarks.select -> FctMarks.to_prop
apply_add_marks
or add_marks_to_fi
for higher level functions.val apply_add_marks : SlicingInternals.fct_slice ->
SlicingTypes.sl_mark PdgMarks.select -> SlicingInternals.criterion list
val filter_already_in : SlicingInternals.fct_slice ->
SlicingTypes.sl_mark PdgMarks.select -> SlicingTypes.sl_mark PdgMarks.select
nodes_marks
are already in the slice or not.
nodes_marks
that are not already in.val prop_persistant_marks : SlicingInternals.project ->
SlicingInternals.fct_info ->
FctMarks.to_prop ->
SlicingInternals.criterion list -> SlicingInternals.criterion list
x = g ();
in f
, we don't necessarily want
all versions of g
to have a visible return
for instance).
val add_marks_to_fi : SlicingInternals.project ->
SlicingInternals.fct_info ->
SlicingTypes.sl_mark PdgMarks.select ->
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 ->
SlicingTypes.sl_mark ->
bool -> SlicingInternals.criterion list -> SlicingInternals.criterion list
val add_change_call_action : SlicingInternals.fct_slice ->
Cil_types.stmt ->
CallInfo.t ->
SlicingInternals.called_fct ->
SlicingInternals.criterion list -> SlicingInternals.criterion list
ChangeCall
(if needed)val choose_precise_slice : SlicingInternals.fct_info ->
CallInfo.t ->
SlicingInternals.fct_slice * SlicingInternals.criterion list
val choose_f_to_call : SlicingInternals.fct_info option ->
CallInfo.t ->
SlicingInternals.called_fct * SlicingInternals.criterion list
val check_called_outputs : CallInfo.call_id ->
SlicingInternals.fct_slice ->
SlicingInternals.criterion list -> SlicingInternals.criterion list
ff
for sig_call
: let's first add some more output
marks in ff
if needed.val apply_choose_call : SlicingInternals.project ->
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 modif_call_inputs : SlicingInternals.fct_slice ->
'a -> SlicingTypes.sl_mark PdgMarks.select -> FctMarks.to_prop
input_marks
in the inputs of call
in ff
.val apply_modif_call_inputs : SlicingInternals.fct_slice ->
'a ->
SlicingTypes.sl_mark PdgMarks.select * 'b -> SlicingInternals.criterion list
modif_call_inputs
and then, check the calls and the callersval apply_missing_inputs : SlicingInternals.project ->
SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingTypes.sl_mark PdgMarks.select * 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.project ->
SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingTypes.sl_mark PdgMarks.select ->
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_change_call : SlicingInternals.project ->
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 enought outputs.val check_outputs_before_change_call : 'a ->
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 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 clear_ff : SlicingInternals.project -> 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 get_node_key_mark : SlicingInternals.fct_slice -> PdgIndex.Key.t -> SlicingTypes.sl_mark
val get_node_mark : SlicingInternals.fct_slice -> PdgTypes.Node.t -> SlicingTypes.sl_mark
val get_local_var_mark : SlicingInternals.fct_slice -> Cil_types.varinfo -> SlicingTypes.sl_mark
val get_param_mark : SlicingInternals.fct_slice -> int -> SlicingTypes.sl_mark
val get_label_mark : SlicingInternals.fct_slice ->
Cil_types.stmt -> Cil_types.label -> SlicingTypes.sl_mark
val get_stmt_mark : SlicingInternals.fct_slice -> Cil_types.stmt -> SlicingTypes.sl_mark
val get_top_input_mark : SlicingInternals.fct_info -> SlicingTypes.sl_mark
val merge_inputs_m1_mark : SlicingInternals.fct_slice -> SlicingTypes.sl_mark
val get_input_loc_under_mark : SlicingInternals.fct_slice -> Locations.Zone.t -> SlicingTypes.sl_mark
exception StopMerging
val merge_fun_callers : ('a -> Kernel_function.t -> 'b list) ->
('b -> 'c) ->
('c -> 'd -> 'd) -> ('d -> bool) -> 'd -> 'a -> Kernel_function.t -> 'd
val get_mark_from_src_fun : Db.Slicing.Project.t -> Kernel_function.t -> SlicingTypes.sl_mark
m
related to all statements of a source function kf
.
Property : is_bottom (get_from_func proj kf) = not (Project.is_called proj kf)
PrintSlice
)val print_ff_sig : Format.formatter -> SlicingInternals.fct_slice -> unit