module SlicingInternals:sig
..end
type
level_option =
| |
DontSlice |
(* |
don't build slice for the function :
ie. always call the source function.
| *) |
| |
DontSliceButComputeMarks |
(* |
don't slice the called functions,
but compute the marks for them
| *) |
| |
MinNbSlice |
(* |
try to use existing slices, create at most one
| *) |
| |
MaxNbSlice |
(* |
most precise slices
(but merge slices with the same visibility,
even if they don't have the same marks)
| *) |
DontSlice
function).type
mark =
| |
Cav of |
| |
Spare |
val compare_mark : mark -> mark -> int
type
pdg_mark = {
|
m1 : |
|
m2 : |
val pdg_mark_packed_descr : Structural_descr.pack
val compare_pdg_mark : pdg_mark -> pdg_mark -> int
type
fct_info = {
|
fi_kf : |
|||
|
fi_def : |
|||
|
fi_project : |
|||
|
mutable fi_top : |
(* |
indicates if the function is maked top (=> src visible)
| *) |
|
mutable fi_level_option : |
(* |
level of specialisation for this function
| *) |
|
mutable fi_init_marks : |
(* |
the marks that must be in every slices of that function
| *) |
|
mutable fi_slices : |
(* |
the list of the slices already computed for this function.
| *) |
|
mutable fi_next_ff_num : |
(* |
the number to assign to the next slice.
| *) |
|
mutable f_called_by : |
(* |
calls in slices that call source fct
| *) |
typecalled_by =
(fct_slice * Cil_types.stmt) list
type
fct_slice = {
|
ff_fct : |
|
ff_id : |
|
mutable ff_marks : |
|
mutable ff_called_by : |
type
fct_id =
| |
FctSrc of |
(* |
source function
| *) |
| |
FctSliced of |
(* |
sliced function
| *) |
type
called_fct =
| |
CallSrc of |
(* |
call the source function (might be unknown if the call uses pointer)
| *) |
| |
CallSlice of |
typecall_info =
called_fct option
typemarks_index =
(pdg_mark, call_info) PdgIndex.FctIndex.t
typeff_marks =
PdgTypes.Pdg.t * marks_index
type
project = {
|
name : |
|
application : |
|
functions : |
|
mutable actions : |
type
appli_criterion =
| |
CaGlobalData of |
(* |
select all that is necessary to compute the given location.
| *) |
| |
CaCall of |
(* |
select all that is necessary to call the given function.
Its application generates requests to add persistent selection
to all the function callers.
| *) |
| |
CaOther |
typefct_base_criterion =
pdg_mark PdgMarks.select
typeloc_point =
Cil_types.stmt * Locations.Zone.t * bool
SlicingInternals.fct_user_crit
)type
node_or_dpds =
| |
CwNode |
| |
CwAddrDpds |
| |
CwDataDpds |
| |
CwCtrlDpds |
type
fct_user_crit =
| |
CuSelect of |
|||
| |
CuTop of |
(* |
the function has probably no PDG,
but we nonetheless give a mark to propagate
| *) |
type
fct_crit =
| |
CcUserMark of |
(* |
add marks to a slice
| *) |
| |
CcChooseCall of |
(* |
have to choose what function to call here.
| *) |
| |
CcChangeCall of |
(* |
call the
called_fct for the given call Cil_types.stmt | *) |
| |
CcMissingOutputs of |
(* |
this call is affected to a function that doesn't compute enough
outputs : we will have to choose between adding outputs to that slice,
or call another one. The boolean tells if the modifications would
change the visibility of some outputs.
| *) |
| |
CcMissingInputs of |
(* |
the function calls a slice that has been modified :
and doesn't compute not enough inputs.
We will have to choose between adding marks to this function,
and call another slice.
The boolean tells if the modifications would
change the visibility of some inputs.
| *) |
| |
CcPropagate of |
(* |
simply propagate the given marks
| *) |
| |
CcExamineCalls of |
type
fct_criterion = {
|
cf_fct : |
(* |
Identification of the RESULT of this filter.
When it a a slice, it might be an existing slice that will be modified,
or a new one will be created during application.
When it is the source function, it means what the criterion has to be
applied on each existing slice, and stored into the inititial marks of
the function.
| *) |
|
cf_info : |
type
criterion =
| |
CrAppli of |
| |
CrFct of |
val dummy_pdg_mark : pdg_mark
val dummy_project : project
val dummy_fct_info : fct_info
val dummy_marks_index : (pdg_mark, call_info) PdgIndex.FctIndex.t
val dummy_ff_marks : PdgTypes.Pdg.t *
(pdg_mark, call_info) PdgIndex.FctIndex.t
val dummy_fct_slice : fct_slice
val dummy_fct_user_crit : fct_user_crit