[Eva] Comments and simplifies the interface of partitioning_index.

src/plugins/value/engine/partitioning_index.ml

@@ -20,34 +20,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Eval
-
 module type Domain = sig
   include Abstract_domain.Lattice
   include Datatype.S_with_collections with type t = state
   include Abstract_domain.Interface with type t := state
 end
 
-module type S = sig
-  type state
-  type t
-
-  val empty: unit -> t
-  val add : state -> t -> bool
-  val merge_set_return_new: state list -> t -> state list
-  val join: t -> state or_bottom
-  val to_list: t -> state list
-  val pretty : Format.formatter -> t -> unit
-end
-
-
 (** Partition of the abstract states, computed for each node by the
     dataflow analysis. *)
 module Make
     (Domain : Domain)
 = struct
 
-  type state = Domain.t
   module Index = Hashtbl.Make (Cvalue_domain.Subpart)
 
   type t = {
@@ -59,10 +43,6 @@ module Make
   let sentinel = Index.create 1
   let empty () = { states = sentinel ; prefix = None ; others = [] }
 
-  let fold f {states; others} acc =
-    let acc = Index.fold (fun _k s acc -> f s acc) states acc in
-    List.fold_left (fun acc s -> f s acc) acc others
-
   (* Optimizations relying on specific features of the cvalue domain. *)
 
   let distinct_subpart = match Domain.get Cvalue_domain.key with
@@ -113,18 +93,6 @@ module Make
         then false
         else (Index.add states prefix state; true)
 
-  let merge_set_return_new states partition =
-    let f acc state =
-      let added = add state partition in
-      if added then state :: acc else acc
-    in
-    List.fold_left f [] states
-
-  let join partition =
-    fold (fun v acc -> Bottom.join Domain.join (`Value v) acc) partition `Bottom
-
-  let to_list p = Index.fold (fun _k v a -> v :: a) p.states p.others
-
   let iter f { states; others } =
     Index.iter (fun _k v -> f v) states;
     List.iter f others

src/plugins/value/engine/partitioning_index.mli

@@ -20,7 +20,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Eval
+(** A partitioning index is a collection of states optimized to determine
+    if a new state is included in one of the states it contains — in a more
+    efficient way than to test the inclusion with all stored states.
+    Such an index is used to keep track of all the states already propagated
+    through a control point, and to rule out new incoming states included in
+    previous ones.
+
+    Partitioning index relies on an heuristics on the cvalue domain,
+    and is very inefficient without it. *)
 
 module type Domain = sig
   include Abstract_domain.Lattice
@@ -28,25 +36,20 @@ module type Domain = sig
   include Abstract_domain.Interface with type t := state
 end
 
-module type S = sig
-  type state
+module Make (Domain: Domain) : sig
   type t
 
+  (** Creates an empty index. *)
   val empty: unit -> t
 
-  val add : state -> t -> bool
-  val merge_set_return_new: state list -> t -> state list
-  val join: t -> state or_bottom
-
-  val to_list: t -> state list
+  (** Adds a state into an index. Returns true if the state did not belong to
+      the index (and has indeed been added), and false if the index already
+      contained the state. *)
+  val add : Domain.t -> t -> bool
 
   val pretty : Format.formatter -> t -> unit
 end
 
-module Make
-    (Domain: Domain)
-  : S with type state = Domain.t
-
 
 (*
 Local Variables: