module SlicingInternals:sig
..end
Internals type definitions should be hidden to the outside world, but it is not really possible to have abstract types since Slicing has to use Db.Slicing functions...
Internals type definitions should be hidden to the outside world, but it is not really possible to have abstract types since Slicing has to use Db.Slicing functions...
type
level_option =
| |
DontSlice |
(* | don't build slice for the function : ie. always call the source function. 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 don't slice the called functions, but compute the marks for them | *) |
| |
MinNbSlice |
(* | try to use existing slices, create at most one 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) most precise slices (but merge slices with the same visibility, even if they don't have the same marks) | *) |
associate a level to each function in order to control how it will be
specialized. This is only a hint used when the tool has to make a choice,
but it doesn't forbid to the user to do whatever he wants
(like building slices for a DontSlice
function).
associate a level to each function in order to control how it will be
specialized. This is only a hint used when the tool has to make a choice,
but it doesn't forbid to the user to do whatever he wants
(like building slices for a DontSlice
function).
type
mark =
| |
Cav of |
| |
Spare |
Kinds of elementary marks.
Kinds of elementary marks.
val compare_mark : mark -> mark -> int
type
pdg_mark = {
|
m1 : |
|
m2 : |
}
Each PDG element has 2 marks to deal with interprocedural propagation
Each PDG element has 2 marks to deal with interprocedural propagation
val pdg_mark_packed_descr : Structural_descr.pack
val compare_pdg_mark : pdg_mark -> pdg_mark -> int
type
fct_info = {
|
fi_kf : |
|||
|
fi_def : |
|||
|
mutable fi_top : |
(* | indicates if the function is marked top (=> src visible) indicates if the function is marked top (=> src visible) | *) |
|
mutable fi_level_option : |
(* | level of specialisation for this function level of specialisation for this function | *) |
|
mutable fi_init_marks : |
(* | the marks that must be in every slices of that function the marks that must be in every slices of that function | *) |
|
mutable fi_slices : |
(* | the list of the slices already computed for this function. the list of the slices already computed for this function. | *) |
|
mutable fi_next_ff_num : |
(* | the number to assign to the next slice. the number to assign to the next slice. | *) |
|
mutable f_called_by : |
(* | calls in slices that call source fct calls in slices that call source fct | *) |
}
Type for all the informations related to any function, even if we don't have its definition.
Type for all the informations related to any function, even if we don't have its definition.
typecalled_by =
(fct_slice * Cil_types.stmt) list
to represent where a function is called.
to represent where a function is called.
type
fct_slice = {
|
ff_fct : |
|
ff_id : |
|
mutable ff_marks : |
|
mutable ff_called_by : |
}
Function slice : created as soon as there is a criterion to compute it, even if the slice itself hasn't been computed yet.
Function slice : created as soon as there is a criterion to compute it, even if the slice itself hasn't been computed yet.
type
fct_id =
| |
FctSrc of |
(* | source function source function | *) |
| |
FctSliced of |
(* | sliced function sliced function | *) |
fct_id
is used to identify either a source function or a sliced one.
fct_id
is used to identify either a source function or a sliced one.
type
called_fct =
| |
CallSrc of |
(* | call the source function (might be unknown if the call uses pointer) call the source function (might be unknown if the call uses pointer) | *) |
| |
CallSlice of |
typecall_info =
called_fct option
information about a call in a slice which gives the function to call
information about a call in a slice which gives the function to call
typemarks_index =
(pdg_mark, call_info) PdgIndex.FctIndex.t
main part of a slice = mapping between the function elements and information about them in the slice.
main part of a slice = mapping between the function elements and information about them in the slice.
typeff_marks =
PdgTypes.Pdg.t * marks_index
type
project = {
|
functions : |
|
mutable actions : |
}
type
appli_criterion =
| |
CaGlobalData of |
(* | select all that is necessary to compute the given location. 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. select all that is necessary to call the given function. Its application generates requests to add persistent selection to all the function callers. | *) |
| |
CaOther |
Slicing criterion at the application level.
When applied, they are translated into fct_criterion
Slicing criterion at the application level.
When applied, they are translated into fct_criterion
typefct_base_criterion =
pdg_mark PdgMarks.select
Base criterion for the functions. These are the only one that can really generate function slices. All the other criteria are translated in more basic ones. Note that to build such a base criterion, the PDG has to be already computed.
Base criterion for the functions. These are the only one that can really generate function slices. All the other criteria are translated in more basic ones. Note that to build such a base criterion, the PDG has to be already computed.
typeloc_point =
Cil_types.stmt * Locations.Zone.t * bool
Used to identify a location (zone) at a given program point. The boolean tell if the point is before (true) or after the statement
Used to identify a location (zone) at a given program point. The boolean tell if the point is before (true) or after the statement
type
node_or_dpds =
| |
CwNode |
| |
CwAddrDpds |
| |
CwDataDpds |
| |
CwCtrlDpds |
node_or_dpds
tells how we want to select nodes,
or some of their dependencies (see SlicingInternals.fct_user_crit
).
node_or_dpds
tells how we want to select nodes,
or some of their dependencies (see SlicingInternals.fct_user_crit
).
type
fct_user_crit =
| |
CuSelect of |
|||
| |
CuTop of |
(* | the function has probably no PDG, but we nonetheless give a mark to propagate the function has probably no PDG, but we nonetheless give a mark to propagate | *) |
Tells which marks we want to put in the slice of a function
Tells which marks we want to put in the slice of a function
type
fct_crit =
| |
CcUserMark of |
(* | add marks to a slice add marks to a slice | *) |
| |
CcChooseCall of |
(* | have to choose what function to call here. have to choose what function to call here. | *) |
| |
CcChangeCall of |
(* | call the call the | *) |
| |
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. 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. 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 simply propagate the given marks | *) |
| |
CcExamineCalls of |
kinds of actions that can be apply to a function
kinds of actions that can be apply to a function
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 initial marks of the function. 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 initial marks of the function. | *) |
|
cf_info : |
}
Slicing criterion for a function.
Slicing criterion for a function.
type
criterion =
| |
CrAppli of |
| |
CrFct of |
A slicing criterion is either an application level criterion, or a function level one.
A slicing criterion is either an application level criterion, or a function level one.
val dummy_pdg_mark : pdg_mark
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
val dummy_project : project
The whole project.
The whole project.