From b8174c837ecd50d8b218c234ea5a2f98b5416300 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 12 Apr 2019 14:38:22 +0200
Subject: [PATCH] [Eva] Comments and simplifies the interface of
partitioning_index.
---
.../value/engine/partitioning_index.ml | 32 -------------------
.../value/engine/partitioning_index.mli | 27 +++++++++-------
2 files changed, 15 insertions(+), 44 deletions(-)
diff --git a/src/plugins/value/engine/partitioning_index.ml b/src/plugins/value/engine/partitioning_index.ml
index c40be57a5bc..08a2f449cf0 100644
--- a/src/plugins/value/engine/partitioning_index.ml
+++ b/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
diff --git a/src/plugins/value/engine/partitioning_index.mli b/src/plugins/value/engine/partitioning_index.mli
index 4ecc2ee21ff..b4488a2eef7 100644
--- a/src/plugins/value/engine/partitioning_index.mli
+++ b/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:
--
GitLab