From c28d06b86a1adac30659a42374a3bd2f624146d9 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 10 Mar 2022 10:50:40 +0100
Subject: [PATCH] [Slicing] extracts comments of the Slicing API from an older
db.ml
---
src/plugins/slicing/api.ml | 1 -
src/plugins/slicing/api.mli | 551 ++++++++++++++------------
src/plugins/slicing/slicingSelect.mli | 82 ++--
3 files changed, 349 insertions(+), 285 deletions(-)
diff --git a/src/plugins/slicing/api.ml b/src/plugins/slicing/api.ml
index 9300aec55d0..4f188601176 100644
--- a/src/plugins/slicing/api.ml
+++ b/src/plugins/slicing/api.ml
@@ -164,7 +164,6 @@ module Select = struct
let dyn_t = SlicingTypes.Sl_select.ty
type set = SlicingCmds.set
module S = Cil_datatype.Varinfo.Map.Make(SlicingTypes.Fct_user_crit)
- type selections = S.t
let dyn_set = S.ty
(** {2 Journalized selectors } *)
diff --git a/src/plugins/slicing/api.mli b/src/plugins/slicing/api.mli
index 126938a3411..bba2afb4077 100644
--- a/src/plugins/slicing/api.mli
+++ b/src/plugins/slicing/api.mli
@@ -21,62 +21,72 @@
(**************************************************************************)
(* ---------------------------------------------------------------------- *)
-(** Global data management *)
-
-val split_slice :
- SlicingInternals.fct_slice -> SlicingInternals.fct_slice list
-
-val merge_slices :
- SlicingInternals.fct_slice ->
- SlicingInternals.fct_slice -> replace:bool -> SlicingInternals.fct_slice
-
-val copy_slice : SlicingInternals.fct_slice -> SlicingInternals.fct_slice
-
-(* ---------------------------------------------------------------------- *)
-(** {1 Global setting } *)
+(** {1 Global setting.} *)
+(** Internal state of the slicing tool from project viewpoints. *)
val self : State.t
(* ---------------------------------------------------------------------- *)
(** {2 Functions with journalized side effects } *)
+(** Set the used slicing modes. *)
val set_modes :
?calls:SlicingParameters.Mode.Calls.t ->
?callers:SlicingParameters.Mode.Callers.t ->
?sliceUndef:SlicingParameters.Mode.SliceUndef.t ->
?keepAnnotations:SlicingParameters.Mode.KeepAnnotations.t -> unit -> unit
-
(* ---------------------------------------------------------------------- *)
-(** {1 Slicing project } *)
+(** {1 Slicing project management.} *)
module Project : sig
- (** {2 Values } *)
-
- val default_slice_names :
- Cil_types.kernel_function -> bool -> int -> string
-
(** {2 Functions with journalized side effects } *)
+ (** Init/reset a slicing project. *)
val reset_slicing : unit -> unit
+ (** Change the slicing level of this function
+ (see the [-slicing-level] option documentation to know the meaning of
+ the number)
+ @raise SlicingTypes.ExternalFunction if [kf] has no definition.
+ @raise SlicingTypes.WrongSlicingLevel if [n] is not valid. *)
+ val change_slicing_level : Cil_types.kernel_function -> int -> unit
+
+ (** Build a new [Db.Project.t] from all [Slice.t] of a project.
+ Can optionally specify how to name the sliced functions
+ by defining [f_slice_names].
+ [f_slice_names kf src_visi num_slice] has to return the name
+ of the exported functions based on the source function [kf].
+ - [src_visi] tells if the source function name is used
+ (if not, it can be used for a slice)
+ - [num_slice] gives the number of the slice to name.
+ The entry point function is only exported once :
+ it is VERY recommended to give to it its original name,
+ even if it is sliced. *)
val extract :
- ?f_slice_names:(Kernel_function.t -> bool -> int -> string) ->
+ ?f_slice_names:(Cil_types.kernel_function -> bool -> int -> string) ->
string -> Project.t
+ (** Print a representation of the slicing project (call graph)
+ in a dot file which name is the given string. *)
val print_dot : filename:string -> title:string -> unit
- val change_slicing_level : Kernel_function.t -> int -> unit
-
(** {2 No needs of Journalization} *)
- val is_directly_called_internal : Kernel_function.t -> bool
+ val default_slice_names : Cil_types.kernel_function -> bool -> int -> string
+ (** Return [true] iff the source function is called (even indirectly via
+ transitivity) from a [Slice.t]. *)
val is_called : Cil_types.kernel_function -> bool
- val has_persistent_selection : Kernel_function.t -> bool
+ (** Return [true] iff the source function has persistent selection *)
+ val has_persistent_selection : Cil_types.kernel_function -> bool
+
+ (** Return [true] if the source function is directly (even via pointer
+ function) called from a [Slice.t]. *)
+ val is_directly_called_internal : Cil_types.kernel_function -> bool
(** {2 Debug} *)
@@ -86,257 +96,330 @@ end
(* ---------------------------------------------------------------------- *)
-(** {1 Mark} *)
+(** {1 Access to slicing results.} *)
module Mark : sig
+ (** Abstract data type for mark value. *)
type t = SlicingTypes.sl_mark
- val dyn_t : SlicingTypes.Sl_mark.t Type.t
+
+ (** For dynamic type checking and journalization. *)
+ val dyn_t : t Type.t
(** {2 No needs of Journalization} *)
- val compare : SlicingTypes.sl_mark -> SlicingTypes.sl_mark -> int
+ (** To construct a mark such as
+ [(is_ctrl result, is_data result, isaddr result) = (~ctrl, ~data, ~addr)],
+ [(is_bottom result) = false] and
+ [(is_spare result) = not (~ctrl || ~data || ~addr)]. *)
+ val make : data:bool -> addr:bool -> ctrl:bool -> t
- val pretty : Format.formatter -> SlicingTypes.sl_mark -> unit
+ (** A total ordering function similar to the generic structural
+ comparison function [compare].
+ Can be used to build a map from [t] marks to, for example, colors for
+ the GUI. *)
+ val compare : t -> t -> int
- val make : data:bool -> addr:bool -> ctrl:bool -> SlicingTypes.sl_mark
+ (** [true] iff the mark is empty: it is the only case where the associated
+ element is invisible. *)
+ val is_bottom : t -> bool
- val is_bottom : SlicingTypes.sl_mark -> bool
+ (** Smallest visible mark. Usually used to mark element that need to be
+ visible for compilation purpose, not really for the selected computations.
+ That mark is related to transparent selection. *)
+ val is_spare : t -> bool
- val is_spare : SlicingTypes.sl_mark -> bool
+ (** The element is used to control the program point of a selected data. *)
+ val is_ctrl : t -> bool
- val is_ctrl : SlicingTypes.sl_mark -> bool
+ (** The element is used to compute selected data.
+ Notice that a mark can be [is_data] and/or [is_ctrl] and/or [is_addr]
+ at the same time. *)
+ val is_data : t -> bool
- val is_data : SlicingTypes.sl_mark -> bool
+ (** The element is used to compute the address of a selected data. *)
+ val is_addr : t -> bool
- val is_addr : SlicingTypes.sl_mark -> bool
+ (** 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) ] *)
+ val get_from_src_func : Cil_types.kernel_function -> t
- val get_from_src_func : Kernel_function.t -> SlicingInternals.pdg_mark
+ (** {2 Debug} *)
+
+ val pretty : Format.formatter -> t -> unit
end
(* ---------------------------------------------------------------------- *)
-(** {1 Selection} *)
+(** {1 Slicing selections.} *)
module Select : sig
+ (** Internal selection. *)
type t = SlicingTypes.sl_select
- val dyn_t : SlicingTypes.Sl_select.t Type.t
+ (** For dynamic type checking and journalization. *)
+ val dyn_t : t Type.t
+
+ (** Set of colored selections. *)
type set = SlicingCmds.set
- type selections = SlicingTypes.Fct_user_crit.t Cil_datatype.Varinfo.Map.t
+ (** For dynamic type checking and journalization. *)
+ val dyn_set : set Type.t
- val dyn_set : selections Type.t
+ (** {2 Selectors.} *)
- (** {2 Journalized selectors } *)
+ (** Empty selection. *)
+ val empty_selects : set
- val empty_selects : selections
+ (** {3 Statement selectors.} *)
+ (** To select a statement. *)
val select_stmt :
- selections -> spare:bool -> Cil_datatype.Stmt.t -> Kernel_function.t -> selections
+ set -> spare:bool -> Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
+ (** To select a statement reachability.
+ Note: add also a transparent selection on the whole statement. *)
val select_stmt_ctrl :
- selections -> spare:bool -> Cil_datatype.Stmt.t -> Kernel_function.t -> selections
-
+ set -> spare:bool -> Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
+
+ (** To select rw accesses to lvalues (given as string) related to a statement.
+ Variables of [~rd] and [~wr] string are bounded relatively to the whole
+ scope of the function.
+ The interpretation of the address of the lvalues is done just before the
+ execution of the statement [~eval].
+ The selection preserve the [~rd] and ~[wr] accesses contained into the
+ statement [ki].
+ Note: add also a transparent selection on the whole statement.
+ @modify Magnesium-20151001 argument [~scope] removed. *)
val select_stmt_lval_rw :
- selections ->
- SlicingTypes.Sl_mark.t ->
+ set ->
+ Mark.t ->
rd:Datatype.String.Set.t ->
wr:Datatype.String.Set.t ->
Cil_datatype.Stmt.t ->
- eval:Cil_datatype.Stmt.t -> Kernel_function.t -> selections
-
+ eval:Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
+
+ (** To select lvalues (given as string) related to a statement.
+ Variables of [lval_str] string are bounded relatively to the whole scope
+ of the function.
+ The interpretation of the address of the lvalue is done just before the
+ execution of the statement [~eval].
+ The selection preserve the value of these lvalues before or after (c.f.
+ boolean [~before]) the statement [ki].
+ Note: add also a transparent selection on the whole statement.
+ @modify Magnesium-20151001 argument [~scope] removed. *)
val select_stmt_lval :
- selections ->
- SlicingTypes.Sl_mark.t ->
+ set ->
+ Mark.t ->
Datatype.String.Set.t ->
before:bool ->
Cil_datatype.Stmt.t ->
- eval:Cil_datatype.Stmt.t -> Kernel_function.t -> selections
+ eval:Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
+ (** To select a zone value related to a statement.
+ Note: add also a transparent selection on the whole statement. *)
+ val select_stmt_zone :
+ set ->
+ Mark.t ->
+ Locations.Zone.t ->
+ before:bool ->
+ Cil_types.stmt -> Cil_types.kernel_function -> set
+
+ (** To select a predicate value related to a statement.
+ Note: add also a transparent selection on the whole statement. *)
+ val select_stmt_term :
+ set ->
+ Mark.t ->
+ Cil_types.term ->
+ Cil_types.stmt -> Cil_types.kernel_function -> set
+
+ (** To select a predicate value related to a statement.
+ Note: add also a transparent selection on the whole statement. *)
+ val select_stmt_pred :
+ set ->
+ Mark.t ->
+ Cil_types.predicate ->
+ Cil_types.stmt -> Cil_types.kernel_function -> set
+
+ (** To select the annotations related to a statement.
+ Note: add also a transparent selection on the whole statement. *)
+ val select_stmt_annot :
+ set ->
+ Mark.t ->
+ spare:bool ->
+ Cil_types.code_annotation ->
+ Cil_types.stmt -> Cil_types.kernel_function -> set
+
+ (** To select the annotations related to a statement.
+ Note: add also a transparent selection on the whole statement. *)
val select_stmt_annots :
- selections ->
- SlicingTypes.Sl_mark.t ->
+ set ->
+ Mark.t ->
spare:bool ->
threat:bool ->
user_assert:bool ->
slicing_pragma:bool ->
loop_inv:bool ->
- loop_var:bool -> Cil_datatype.Stmt.t -> Kernel_function.t -> selections
-
+ loop_var:bool -> Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
+
+ (** {3 Function selectors.} *)
+
+ (** To select rw accesses to lvalues (given as a string) related to a
+ function.
+ Variables of [~rd] and [~wr] string are bounded relatively to the whole
+ scope of the function.
+ The interpretation of the address of the lvalues is done just before the
+ execution of the statement [~eval].
+ The selection preserve the value of these lvalues into the whole project.
+ @modify Magnesium-20151001 argument [~scope] removed. *)
+ val select_func_lval_rw :
+ set -> Mark.t -> rd:Datatype.String.Set.t -> wr:Datatype.String.Set.t ->
+ eval:Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
+
+ (** To select lvalues (given as a string) related to a function.
+ Variables of [lval_str] string are bounded relatively to the scope of the
+ first statement of [kf].
+ The interpretation of the address of the lvalues is done just before the
+ execution of the first statement [kf].
+ The selection preserve the value of these lvalues before execution of the
+ return statement. *)
val select_func_lval :
- selections ->
- SlicingTypes.Sl_mark.t ->
- Datatype.String.Set.t -> Kernel_function.t -> selections
+ set -> Mark.t -> Datatype.String.Set.t -> Cil_types.kernel_function -> set
- val select_func_lval_rw :
- selections ->
- SlicingTypes.Sl_mark.t ->
- rd:Datatype.String.Set.t ->
- wr:Datatype.String.Set.t ->
- eval:Cil_datatype.Stmt.t -> Kernel_function.t -> selections
+ (** To select an output zone related to a function. *)
+ val select_func_zone :
+ set -> Mark.t -> Locations.Zone.t -> Cil_types.kernel_function -> set
- val select_func_return : selections -> spare:bool -> Kernel_function.t -> selections
+ (** To select the function result (returned value). *)
+ val select_func_return : set -> spare:bool -> Cil_types.kernel_function -> set
+ (** To select every calls to the given function, i.e. the call keeps its
+ semantics in the slice. *)
val select_func_calls_to :
- selections -> spare:bool -> Kernel_function.t -> selections
+ set -> spare:bool -> Cil_types.kernel_function -> set
+ (** To select every calls to the given function without the selection of its
+ inputs/outputs. *)
val select_func_calls_into :
- selections -> spare:bool -> Kernel_function.t -> selections
+ set -> spare:bool -> Cil_types.kernel_function -> set
+ (** To select the annotations related to a function. *)
val select_func_annots :
- selections ->
- SlicingTypes.Sl_mark.t ->
- spare:bool ->
- threat:bool ->
- user_assert:bool ->
- slicing_pragma:bool ->
- loop_inv:bool -> loop_var:bool -> Kernel_function.t -> selections
-
- val select_func_zone :
- SlicingCmds.set ->
- SlicingTypes.sl_mark ->
- Locations.Zone.t -> Cil_types.kernel_function -> SlicingCmds.set
-
- val select_stmt_term :
- SlicingCmds.set ->
- SlicingTypes.sl_mark ->
- Cil_types.term ->
- Cil_types.stmt -> Cil_types.kernel_function -> SlicingCmds.set
+ set -> Mark.t -> spare:bool -> threat:bool -> user_assert:bool ->
+ slicing_pragma:bool -> loop_inv:bool -> loop_var:bool ->
+ Cil_types.kernel_function -> set
- val select_stmt_pred :
- SlicingCmds.set ->
- SlicingTypes.sl_mark ->
- Cil_types.predicate ->
- Cil_types.stmt -> Cil_types.kernel_function -> SlicingCmds.set
-
- val select_stmt_annot :
- SlicingCmds.set ->
- SlicingTypes.sl_mark ->
- spare:bool ->
- Cil_types.code_annotation ->
- Cil_types.stmt -> Cil_types.kernel_function -> SlicingCmds.set
-
- val select_stmt_zone :
- SlicingCmds.set ->
- SlicingTypes.sl_mark ->
- Locations.Zone.t ->
- before:bool ->
- Cil_types.stmt -> Cil_types.kernel_function -> SlicingCmds.set
+ (** {3 Pdg selectors.} *)
val select_pdg_nodes :
- SlicingCmds.set ->
- SlicingTypes.sl_mark ->
- PdgTypes.Node.t list -> Cil_types.kernel_function -> SlicingCmds.set
+ set -> Mark.t -> PdgTypes.Node.t list -> Cil_types.kernel_function -> set
+
+ (** {3 Internal use only} *)
- val get_function : SlicingTypes.sl_select -> Cil_types.kernel_function
+ (** The function related to an internal selection. *)
+ val get_function : t -> Cil_types.kernel_function
- val merge_internal :
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ (** The function related to an internal selection. *)
+ val merge_internal : t -> t -> t
- val add_to_selects_internal :
- Cil_datatype.Varinfo.Map.key * SlicingInternals.fct_user_crit ->
- SlicingInternals.fct_user_crit Cil_datatype.Varinfo.Map.t ->
- SlicingInternals.fct_user_crit Cil_datatype.Varinfo.Map.t
+ val add_to_selects_internal : t -> set -> set
- val iter_selects_internal :
- (Cil_datatype.Varinfo.Map.key * 'a -> unit) ->
- 'a Cil_datatype.Varinfo.Map.t -> unit
+ val iter_selects_internal : (t -> unit) -> set -> unit
- val fold_selects_internal :
- ('a -> Cil_datatype.Varinfo.Map.key * 'b -> 'a) ->
- 'a -> 'b Cil_datatype.Varinfo.Map.t -> 'a
+ val fold_selects_internal : (('a -> t -> 'a) -> 'a -> set -> 'a)
+ (** Internally used to select a statement :
+ - if [is_ctrl_mark m],
+ propagate ctrl_mark on ctrl dependencies of the statement
+ - if [is_addr_mark m],
+ propagate addr_mark on addr dependencies of the statement
+ - if [is_data_mark m],
+ propagate data_mark on data dependencies of the statement
+ Marks the node with a spare_mark and propagate so that the dependencies
+ that were not selected yet will be marked spare.
+ When the statement is a call, its functional inputs/outputs are also
+ selected (The call is still selected even it has no output).
+ When the statement is a composed one (block, if, etc...),
+ all the sub-statements are selected.
+ @raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_stmt_internal :
- Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Cil_types.stmt ->
- SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ Cil_types.kernel_function -> ?select:t -> Cil_types.stmt -> Mark.t -> t
val select_label_internal :
- Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Cil_types.logic_label ->
- SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
-
+ Cil_types.kernel_function ->
+ ?select:t -> Cil_types.logic_label -> Mark.t -> t
+
+ (** Internally used to select a statement call without its
+ inputs/outputs so that it doesn't select the statements computing the
+ inputs of the called function as [select_stmt_internal] would do.
+ Raise [Invalid_argument] when the [stmt] isn't a call.
+ @raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_min_call_internal :
- Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Cil_types.stmt ->
- SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ Cil_types.kernel_function -> ?select:t -> Cil_types.stmt -> Mark.t -> t
+ (** Internally used to select a zone value at a program point.
+ @raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_stmt_zone_internal :
- Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Cil_types.stmt ->
- before:bool ->
- Locations.Zone.t ->
- SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
-
+ Cil_types.kernel_function ->
+ ?select:t ->
+ Cil_types.stmt -> before:bool -> Locations.Zone.t -> Mark.t -> t
+
+ (** Internally used to select a zone value at the beginning of a function.
+ For a defined function, it is similar to [select_stmt_zone_internal]
+ with the initial statement, but it can also be used for undefined
+ functions.
+ @raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_zone_at_entry_point_internal :
- Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Locations.Zone.t ->
- SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ Cil_types.kernel_function -> ?select:t -> Locations.Zone.t -> Mark.t -> t
+ (** Internally used to select a zone value at the end of a function.
+ For a defined function, it is similar to [select_stmt_zone_internal]
+ with the return statement, but it can also be used for undefined
+ functions.
+ @raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_zone_at_end_internal :
- Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Locations.Zone.t ->
- SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ Cil_types.kernel_function -> ?select:t -> Locations.Zone.t -> Mark.t -> t
+ (** Internally used to select the statements that modify the
+ given zone considered as in output.
+ Be careful that it is NOT the same as selecting the zone at the end!
+ The 'undef' zone is not propagated...
+ @raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_modified_output_zone_internal :
- Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Locations.Zone.t ->
- SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ Cil_types.kernel_function -> ?select:t -> Locations.Zone.t -> Mark.t -> t
+ (** Internally used to select a statement reachability :
+ Only propagate a ctrl_mark on the statement control dependencies.
+ @raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_stmt_ctrl_internal :
- Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Cil_types.stmt ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ Cil_types.kernel_function -> ?select:t -> Cil_types.stmt -> t
val select_entry_point_internal :
- Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ Cil_types.kernel_function -> ?select:t -> Mark.t -> t
val select_return_internal :
- Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ Cil_types.kernel_function -> ?select:t -> Mark.t -> t
val select_decl_var_internal :
- Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Cil_types.varinfo ->
- SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
-
+ Cil_types.kernel_function -> ?select:t -> Cil_types.varinfo -> Mark.t -> t
+
+ (** Internally used to select PDG nodes :
+ - if [is_ctrl_mark m],
+ propagate ctrl_mark on ctrl dependencies of the statement
+ - if [is_addr_mark m],
+ propagate addr_mark on addr dependencies of the statement
+ - if [is_data_mark m],
+ propagate data_mark on data dependencies of the statement
+ Marks the node with a spare_mark and propagate so that
+ the dependencies that were not selected yet will be marked spare. *)
val select_pdg_nodes_internal :
- Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- PdgTypes.Node.t list ->
- SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ Cil_types.kernel_function ->
+ ?select:t -> PdgTypes.Node.t list -> Mark.t -> t
(** {2 Debug} *)
- val pretty :
- Format.formatter ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
+ val pretty : Format.formatter -> t -> unit
end
@@ -346,61 +429,45 @@ end
module Slice : sig
type t = SlicingTypes.sl_fct_slice
- val dyn_t : SlicingTypes.Sl_fct_slice.t Type.t
+ val dyn_t : t Type.t
(** {2 Functions with journalized side effects } *)
- val create : Kernel_function.t -> SlicingTypes.Sl_fct_slice.t
+ val create : Cil_types.kernel_function -> t
- val remove : SlicingTypes.Sl_fct_slice.t -> unit
+ val remove : t -> unit
val remove_uncalled : unit -> unit
(** {2 No needs of Journalization} *)
- val get_all : Kernel_function.t -> SlicingInternals.fct_slice list
+ val get_all : Cil_types.kernel_function -> t list
- val get_function :
- SlicingInternals.fct_slice -> Cil_types.kernel_function
+ val get_function : t -> Cil_types.kernel_function
- val get_callers :
- SlicingInternals.fct_slice -> SlicingInternals.fct_slice list
+ val get_callers : t -> t list
- val get_called_slice :
- SlicingInternals.fct_slice ->
- Cil_types.stmt -> SlicingInternals.fct_slice option
+ val get_called_slice : t -> Cil_types.stmt -> t option
- val get_called_funcs :
- SlicingInternals.fct_slice ->
- Cil_types.stmt -> Kernel_function.Hptset.elt list
+ val get_called_funcs : t -> Cil_types.stmt -> Cil_types.kernel_function list
- val get_mark_from_stmt :
- SlicingInternals.fct_slice ->
- Cil_types.stmt -> SlicingInternals.pdg_mark
+ val get_mark_from_stmt : t -> Cil_types.stmt -> Mark.t
- val get_mark_from_label :
- SlicingInternals.fct_slice ->
- Cil_types.stmt -> Cil_types.label -> SlicingInternals.pdg_mark
+ val get_mark_from_label : t -> Cil_types.stmt -> Cil_types.label -> Mark.t
- val get_mark_from_local_var :
- SlicingInternals.fct_slice ->
- Cil_types.varinfo -> SlicingInternals.pdg_mark
+ val get_mark_from_local_var : t -> Cil_types.varinfo -> Mark.t
- val get_mark_from_formal :
- SlicingInternals.fct_slice ->
- Cil_datatype.Varinfo.t -> SlicingInternals.pdg_mark
+ val get_mark_from_formal : t -> Cil_datatype.Varinfo.t -> Mark.t
- val get_user_mark_from_inputs :
- SlicingInternals.fct_slice -> SlicingInternals.pdg_mark
+ val get_user_mark_from_inputs : t -> Mark.t
- val get_num_id : SlicingInternals.fct_slice -> int
+ val get_num_id : t -> int
- val from_num_id :
- Kernel_function.t -> int -> SlicingInternals.fct_slice
+ val from_num_id : Cil_types.kernel_function -> int -> t
(** {2 Debug} *)
- val pretty : Format.formatter -> SlicingInternals.fct_slice -> unit
+ val pretty : Format.formatter -> t -> unit
end
@@ -419,32 +486,22 @@ module Request : sig
val propagate_user_marks : unit -> unit
- val copy_slice :
- SlicingTypes.Sl_fct_slice.t -> SlicingTypes.Sl_fct_slice.t
+ val copy_slice : Slice.t -> Slice.t
- val split_slice :
- SlicingTypes.Sl_fct_slice.t -> SlicingTypes.Sl_fct_slice.t list
+ val split_slice : Slice.t -> Slice.t list
- val merge_slices :
- SlicingTypes.Sl_fct_slice.t ->
- SlicingTypes.Sl_fct_slice.t ->
- replace:bool -> SlicingTypes.Sl_fct_slice.t
+ val merge_slices : Slice.t -> Slice.t -> replace:bool -> Slice.t
- val add_call_slice :
- caller:SlicingTypes.Sl_fct_slice.t ->
- to_call:SlicingTypes.Sl_fct_slice.t -> unit
+ val add_call_slice : caller:Slice.t -> to_call:Slice.t -> unit
- val add_call_fun :
- caller:SlicingTypes.Sl_fct_slice.t ->
- to_call:Kernel_function.t -> unit
+ val add_call_fun : caller:Slice.t -> to_call:Cil_types.kernel_function -> unit
val add_call_min_fun :
- caller:SlicingTypes.Sl_fct_slice.t ->
- to_call:Kernel_function.t -> unit
+ caller:Slice.t -> to_call:Cil_types.kernel_function -> unit
- val add_selection : Select.selections -> unit
+ val add_selection : Select.set -> unit
- val add_persistent_selection : Select.selections -> unit
+ val add_persistent_selection : Select.set -> unit
val add_persistent_cmdline : unit -> unit
@@ -452,15 +509,23 @@ module Request : sig
val is_request_empty_internal : unit -> bool
- val add_slice_selection_internal :
- SlicingInternals.fct_slice ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
+ val add_slice_selection_internal : Slice.t -> Select.t -> unit
- val add_selection_internal :
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
+ val add_selection_internal : Select.t -> unit
(** {2 Debug} *)
val pretty : Format.formatter -> unit
end
+
+(* ---------------------------------------------------------------------- *)
+(** {1 Global data management} *)
+
+val split_slice : Slice.t -> Slice.t list
+
+val merge_slices : Slice.t -> Slice.t -> replace:bool -> Slice.t
+
+val copy_slice : Slice.t -> Slice.t
+
+(* -- end -------------------------------------------------------------- *)
diff --git a/src/plugins/slicing/slicingSelect.mli b/src/plugins/slicing/slicingSelect.mli
index e751a2cf45a..c139085e9da 100644
--- a/src/plugins/slicing/slicingSelect.mli
+++ b/src/plugins/slicing/slicingSelect.mli
@@ -24,14 +24,14 @@ val check_call : Cil_types.stmt -> bool -> Cil_types.stmt
val print_select :
Format.formatter ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
+ SlicingTypes.sl_select -> unit
val get_select_kf : Cil_types.varinfo * 'a -> Cil_types.kernel_function
val check_db_select :
Cil_datatype.Varinfo.t ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select ->
+ SlicingTypes.sl_select
val empty_db_select :
Kernel_function.t -> Cil_types.varinfo * SlicingInternals.fct_user_crit
@@ -43,30 +43,30 @@ val top_db_select :
val check_kf_db_select :
Kernel_function.t ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select ->
+ SlicingTypes.sl_select
val check_ff_db_select :
SlicingInternals.fct_slice ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ SlicingTypes.sl_select ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
val bottom_msg : Kernel_function.t -> unit
val basic_add_select :
Kernel_function.t ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ SlicingTypes.sl_select ->
PdgTypes.Node.t list ->
?undef:Locations.Zone.t option * SlicingTypes.sl_mark ->
SlicingActions.n_or_d_marks ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
val select_pdg_nodes :
Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ ?select:SlicingTypes.sl_select ->
PdgTypes.Node.t list ->
SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
val mk_select :
Db.Pdg.t ->
@@ -77,12 +77,12 @@ val mk_select :
val select_stmt_zone :
Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ ?select:SlicingTypes.sl_select ->
Cil_types.stmt ->
before:bool ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
(** this one is similar to [select_stmt_zone] with the return statement
* when the function is defined, but it can also be used for undefined functions. *)
@@ -90,91 +90,91 @@ val select_in_out_zone :
at_end:bool ->
use_undef:bool ->
Kernel_function.t ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ SlicingTypes.sl_select ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
val select_zone_at_end :
Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ ?select:SlicingTypes.sl_select ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
val select_modified_output_zone :
Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ ?select:SlicingTypes.sl_select ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
val select_zone_at_entry :
Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ ?select:SlicingTypes.sl_select ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
val stmt_nodes_to_select :
Db.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t list
val select_stmt_computation :
Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ ?select:SlicingTypes.sl_select ->
Cil_types.stmt ->
SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
val select_label :
Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ ?select:SlicingTypes.sl_select ->
Cil_types.logic_label ->
SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
(** marking a call node means that a [choose_call] will have to decide that to
* call according to the slicing-level, but anyway, the call will be visible.
*)
val select_minimal_call :
Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ ?select:SlicingTypes.sl_select ->
Cil_types.stmt ->
SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
val select_stmt_ctrl :
Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Cil_types.stmt -> Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ ?select:SlicingTypes.sl_select ->
+ Cil_types.stmt -> SlicingTypes.sl_select
val select_entry_point :
Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ ?select:SlicingTypes.sl_select ->
SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
val select_return :
Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ ?select:SlicingTypes.sl_select ->
SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
val select_decl_var :
Kernel_function.t ->
- ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ ?select:SlicingTypes.sl_select ->
Cil_types.varinfo ->
SlicingTypes.sl_mark ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select
val merge_select :
SlicingInternals.fct_user_crit ->
SlicingInternals.fct_user_crit -> SlicingInternals.fct_user_crit
val merge_db_select :
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+ SlicingTypes.sl_select ->
+ SlicingTypes.sl_select ->
+ SlicingTypes.sl_select
module Selections : sig
@@ -214,13 +214,13 @@ val call_min_f_in_caller :
val is_already_selected :
SlicingInternals.fct_slice ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> bool
+ SlicingTypes.sl_select -> bool
val add_ff_selection :
SlicingInternals.fct_slice ->
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
+ SlicingTypes.sl_select -> unit
(** add a persistent selection to the function.
* This might change its slicing level in order to call slices later on. *)
val add_fi_selection :
- Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
+ SlicingTypes.sl_select -> unit
--
GitLab