Module Fct_slice

module Fct_slice: sig .. end

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 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

Manage the information related to a function call in a slice.

module FctMarks: sig .. end

FctMarks manages the mapping between a function elements and their marks.

xxx

val get_called_slice : SlicingInternals.fct_slice ->
       Cil_types.stmt -> SlicingInternals.fct_slice option * bool

Inform about the called slice or else calls to source functions.

xxx

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

Examine the call statements after the modification of 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

build a new empty slice in the given 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.
Raises

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.

Adding marks

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

quite internal function that only computes the marks. Dont't use it alone because it doesn't take care of the calls and so on. See 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

main function to build or modify a slice.
Returns a list of the filters to add to the worklist.

val filter_already_in : SlicingInternals.fct_slice ->
       SlicingTypes.sl_mark PdgMarks.select -> SlicingTypes.sl_mark PdgMarks.select

a function that doesn't modify anything but test if the nodes_marks are already in the slice or not.
Returns the 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

when the user adds persistent marks to a function, he might want to propagate them to the callers, but, anyway, we don't want to propagate persistent marks to the calls for the same reason (if we mark 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

add the marks to the persistent marks to be used when new slices will be created. The actions to add the marks to the existing slices are generated in slicingProject. If it is the first persistent selection for this function, and 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

Choosing the function to call

val add_change_call_action : SlicingInternals.fct_slice ->
       Cil_types.stmt ->
       CallInfo.t ->
       SlicingInternals.called_fct ->
       SlicingInternals.criterion list -> SlicingInternals.criterion list

Build a new action ChangeCall (if needed)

val choose_precise_slice : SlicingInternals.fct_info ->
       CallInfo.t ->
       SlicingInternals.fct_slice * SlicingInternals.criterion list

choose among the already computed slice if there is a function that computes just enough outputs (what ever their marks are). If not, create a new one

val choose_f_to_call : SlicingInternals.fct_info option ->
       CallInfo.t ->
       SlicingInternals.called_fct * SlicingInternals.criterion list

choose the function to call according to the slicing level of the function to call

val check_called_outputs : CallInfo.call_id ->
       SlicingInternals.fct_slice ->
       SlicingInternals.criterion list -> SlicingInternals.criterion list

we are about to call 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 the function (slice or source) to call according to the slicing level of the called function. Does nothing if there is already a called function : this is useful because we can sometime generate several 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.

Calls input/output marks

val modif_call_inputs : SlicingInternals.fct_slice ->
       'a -> SlicingTypes.sl_mark PdgMarks.select -> FctMarks.to_prop

propagate the 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 callers

val 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.

Changing the function to call

val apply_change_call : SlicingInternals.project ->
       SlicingInternals.fct_slice ->
       Cil_types.stmt ->
       SlicingInternals.called_fct -> SlicingInternals.criterion list

check if f_to_call is ok for this call, and if so, change the function call and propagate missing marks in the inputs if needed.
Raises 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

When the user wants to make a 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.

Merge, remove, ...

val merge_slices : SlicingInternals.fct_slice ->
       SlicingInternals.fct_slice ->
       SlicingInternals.fct_slice * SlicingInternals.criterion list

Build a new slice which marks are a join between 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.
Raises SlicingTypes.CantRemoveCalledFf if the slice is called.

Getting the slice marks

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

Getting the source function marks

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

The 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)

Printing

(see also PrintSlice)

val print_ff_sig : Format.formatter -> SlicingInternals.fct_slice -> unit