From 90723a44d14bfac014043bde4bfefcf9de09bd16 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 8 Apr 2019 11:08:14 +0200
Subject: [PATCH] [Eva] Moves the signature from state_partitioning into
trace_partitioning.
Removes state_partitioning.mli.
Since there is only one implementation of state_partitioning signature, there is
no need to keep this separate file.
---
Makefile | 1 -
src/plugins/value/engine/partition.mli | 2 +-
.../value/engine/partitioning_parameters.ml | 3 +-
.../value/engine/partitioning_parameters.mli | 13 +-
.../value/engine/state_partitioning.mli | 143 ------------------
.../value/engine/trace_partitioning.ml | 10 +-
.../value/engine/trace_partitioning.mli | 98 +++++++++++-
7 files changed, 115 insertions(+), 155 deletions(-)
delete mode 100644 src/plugins/value/engine/state_partitioning.mli
diff --git a/Makefile b/Makefile
index 411ebb702e9..9f7c9a8ba71 100644
--- a/Makefile
+++ b/Makefile
@@ -923,7 +923,6 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
engine/initialization \
engine/compute_functions engine/analysis register
PLUGIN_CMI:= values/abstract_value values/abstract_location \
- engine/state_partitioning \
domains/abstract_domain domains/simpler_domains
PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen
diff --git a/src/plugins/value/engine/partition.mli b/src/plugins/value/engine/partition.mli
index 6e5c2be9533..672c0cb458b 100644
--- a/src/plugins/value/engine/partition.mli
+++ b/src/plugins/value/engine/partition.mli
@@ -55,7 +55,7 @@
of keys.
*)
-type branch = int
+type branch = int (* Junction branch id in the control flow *)
module ExpMap = Cil_datatype.ExpStructEq.Map
diff --git a/src/plugins/value/engine/partitioning_parameters.ml b/src/plugins/value/engine/partitioning_parameters.ml
index 3cd62544005..100803fa8c3 100644
--- a/src/plugins/value/engine/partitioning_parameters.ml
+++ b/src/plugins/value/engine/partitioning_parameters.ml
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-open State_partitioning
open Value_parameters
open Partitioning_annots
open Cil_types
@@ -30,7 +29,7 @@ let is_loop s = match s.skind with Loop _ -> true | _ -> false
let warn ?(current = true) = Kernel.warning ~once:true ~current
-module Make (Kf : Kf) : Parameters =
+module Make (Kf : sig val kf: kernel_function end) =
struct
let kf = Kf.kf
diff --git a/src/plugins/value/engine/partitioning_parameters.mli b/src/plugins/value/engine/partitioning_parameters.mli
index 57acfb7caab..df2f76e600b 100644
--- a/src/plugins/value/engine/partitioning_parameters.mli
+++ b/src/plugins/value/engine/partitioning_parameters.mli
@@ -20,4 +20,15 @@
(* *)
(**************************************************************************)
-module Make (Kf : State_partitioning.Kf) : State_partitioning.Parameters
+open Cil_types
+
+module Make (Kf : sig val kf: kernel_function end) : sig
+ val widening_delay : int
+ val widening_period : int
+ val slevel : stmt -> int
+ val merge : stmt -> bool
+ val unroll : stmt -> Partition.unroll_limit
+ val history_size : int
+ val universal_splits : Partition.action list
+ val flow_actions : stmt -> Partition.action list
+end
diff --git a/src/plugins/value/engine/state_partitioning.mli b/src/plugins/value/engine/state_partitioning.mli
deleted file mode 100644
index d5b8df9227e..00000000000
--- a/src/plugins/value/engine/state_partitioning.mli
+++ /dev/null
@@ -1,143 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2019 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Bottom.Type
-
-type branch = Partition.branch (* Junction branch id in the control flow *)
-type loop = Cil_types.stmt (* Loop head id *)
-
-module type Kf =
-sig
- val kf : Cil_types.kernel_function
-end
-
-module type Parameters =
-sig
- val widening_delay : int
- val widening_period : int
- val slevel : Cil_types.stmt -> int
- val merge : Cil_types.stmt -> bool
- val unroll : loop -> Partition.unroll_limit
- val history_size : int
- val universal_splits : Partition.action list
- val flow_actions : Cil_types.stmt -> Partition.action list
-end
-
-module type Partition =
-sig
- type state (** The states being partitioned *)
- type store (** The storage of all states ever met at a control point *)
- type flow (** A set of states which are currently propagated *)
- type tank (** An organized temporary accumulation of flows *)
- type widening (** Widening informations *)
-
- (* --- Constructors --- *)
-
- val empty_store : stmt:Cil_types.stmt option -> store
- val empty_flow : unit -> flow
- val empty_tank : unit -> tank
- val empty_widening : stmt:Cil_types.stmt option -> widening
-
- (** Build the initial tank for the entry point of a function. *)
- val initial_tank : state list -> tank
-
- (* --- Pretty printing --- *)
-
- val pretty_store : Format.formatter -> store -> unit
- val pretty_flow : Format.formatter -> flow -> unit
-
- (* --- Accessors --- *)
-
- val expanded : store -> state list
- val smashed : store -> state or_bottom
- val contents : flow -> state list
- val is_empty_store : store -> bool
- val is_empty_flow : flow -> bool
- val is_empty_tank : tank -> bool
- val store_size : store -> int
- val flow_size : flow -> int
- val tank_size : tank -> int
-
- (* --- Reset state (for hierchical convergence) --- *)
-
- (* These functions reset the part of the state of the analysis which has
- been obtained after a widening. *)
- val reset_store : store -> unit
- val reset_flow : flow -> unit
- val reset_tank : tank -> unit
- val reset_widening : widening -> unit
-
- (** Resets (or just delays) the widening counter. Used on nested loops, to
- postpone the widening of the inner loop when iterating on the outer
- loops. This is especially useful when the inner loop fixpoint does not
- depend on the outer loop. *)
- val reset_widening_counter : widening -> unit
-
- (* --- Partition transfer functions --- *)
-
- val enter_loop : flow -> loop -> unit
- val leave_loop : flow -> loop -> unit
- val next_loop_iteration : flow -> loop -> unit
- val split_return : flow -> Cil_types.exp option -> unit
-
- (* --- Operators --- *)
-
- (** Remove all states from the tank, leaving it empty as if it was just
- created by [empty_tank] *)
- val drain : tank -> flow
-
- (** Fill the states of the flow into the tank, modifying [into] inplace but
- letting the flow unchanged *)
- val fill: into:tank -> flow -> unit
-
- (** Apply a transfer function to all the states of a propagation. *)
- val transfer : (state -> state list) -> flow -> unit
-
- (** Join all incoming propagations into the given store. This function returns
- a set of states which still need to be propagated past the store.
-
- If a state from the propagations is included in another state which has
- already been propagated, it may be removed from the output propagation.
- Likewise, if a state from a propagation is included in a state from
- another propagation of the list (coming from another edge or iteration),
- it may also be removed.
-
- This function also interprets partitioning annotations at the store
- vertex (slevel, splits, merges, ...) which will generally change the
- current partitioning. *)
- val join : (branch * flow) list -> store -> flow
-
- (** Widen a flow. The widening object keeps track of the previous widenings
- and previous propagated states to ensure termination. The result is true
- when it is correct to end the propagation here, i.e. when the flow
- object is only containng states which are included into already propagated
- states. *)
- val widen : widening -> flow -> bool
-end
-
-module type Domain = Partitioning.Domain
-
-module type Partitioning = functor
- (Abstract : Abstractions.Eva)
- (Transfer : Transfer_stmt.S with type state = Abstract.Dom.t)
- (Kf : Kf) ->
- Partition with type state = Abstract.Dom.t
diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml
index 3e529ae6435..b9aef2190db 100644
--- a/src/plugins/value/engine/trace_partitioning.ml
+++ b/src/plugins/value/engine/trace_partitioning.ml
@@ -22,14 +22,12 @@
open Cil_types
open Bottom.Type
-open State_partitioning
open Partition
-
module Make
(Abstract: Abstractions.Eva)
(Transfer : Transfer_stmt.S with type state = Abstract.Dom.t)
- (Kf : Kf) =
+ (Kf : sig val kf: kernel_function end) =
struct
module Parameters = Partitioning_parameters.Make (Kf)
@@ -152,13 +150,13 @@ struct
let transfer_action p action =
p.flow_states <- Flow.transfer_keys p.flow_states action
- let enter_loop (p : flow) (i : loop) : unit =
+ let enter_loop (p : flow) (i : stmt) : unit =
transfer_action p (Enter_loop (unroll i))
- let leave_loop (p : flow) (_i : loop) : unit =
+ let leave_loop (p : flow) (_i : stmt) : unit =
transfer_action p Leave_loop
- let next_loop_iteration (p : flow) (_i : loop) : unit =
+ let next_loop_iteration (p : flow) (_i : stmt) : unit =
transfer_action p Incr_loop
let empty_rationing = new_rationing ~limit:0 ~merge:false
diff --git a/src/plugins/value/engine/trace_partitioning.mli b/src/plugins/value/engine/trace_partitioning.mli
index 9006e977b10..dd9dfaadeec 100644
--- a/src/plugins/value/engine/trace_partitioning.mli
+++ b/src/plugins/value/engine/trace_partitioning.mli
@@ -20,4 +20,100 @@
(* *)
(**************************************************************************)
-module Make : State_partitioning.Partitioning
+open Bottom.Type
+
+module Make
+ (Abstract : Abstractions.Eva)
+ (Transfer : Transfer_stmt.S with type state = Abstract.Dom.t)
+ (Kf : sig val kf: Cil_types.kernel_function end) :
+sig
+ type state = Abstract.Dom.t (** The states being partitioned *)
+ type store (** The storage of all states ever met at a control point *)
+ type flow (** A set of states which are currently propagated *)
+ type tank (** An organized temporary accumulation of flows *)
+ type widening (** Widening informations *)
+
+ (* --- Constructors --- *)
+
+ val empty_store : stmt:Cil_types.stmt option -> store
+ val empty_flow : unit -> flow
+ val empty_tank : unit -> tank
+ val empty_widening : stmt:Cil_types.stmt option -> widening
+
+ (** Build the initial tank for the entry point of a function. *)
+ val initial_tank : state list -> tank
+
+ (* --- Pretty printing --- *)
+
+ val pretty_store : Format.formatter -> store -> unit
+ val pretty_flow : Format.formatter -> flow -> unit
+
+ (* --- Accessors --- *)
+
+ val expanded : store -> state list
+ val smashed : store -> state or_bottom
+ val contents : flow -> state list
+ val is_empty_store : store -> bool
+ val is_empty_flow : flow -> bool
+ val is_empty_tank : tank -> bool
+ val store_size : store -> int
+ val flow_size : flow -> int
+ val tank_size : tank -> int
+
+ (* --- Reset state (for hierchical convergence) --- *)
+
+ (* These functions reset the part of the state of the analysis which has
+ been obtained after a widening. *)
+ val reset_store : store -> unit
+ val reset_flow : flow -> unit
+ val reset_tank : tank -> unit
+ val reset_widening : widening -> unit
+
+ (** Resets (or just delays) the widening counter. Used on nested loops, to
+ postpone the widening of the inner loop when iterating on the outer
+ loops. This is especially useful when the inner loop fixpoint does not
+ depend on the outer loop. *)
+ val reset_widening_counter : widening -> unit
+
+ (* --- Partition transfer functions --- *)
+
+ val enter_loop : flow -> Cil_types.stmt -> unit
+ val leave_loop : flow -> Cil_types.stmt -> unit
+ val next_loop_iteration : flow -> Cil_types.stmt -> unit
+ val split_return : flow -> Cil_types.exp option -> unit
+
+ (* --- Operators --- *)
+
+ (** Remove all states from the tank, leaving it empty as if it was just
+ created by [empty_tank] *)
+ val drain : tank -> flow
+
+ (** Fill the states of the flow into the tank, modifying [into] inplace but
+ letting the flow unchanged *)
+ val fill : into:tank -> flow -> unit
+
+ (** Apply a transfer function to all the states of a propagation. *)
+ val transfer : (state -> state list) -> flow -> unit
+
+ (** Join all incoming propagations into the given store. This function returns
+ a set of states which still need to be propagated past the store.
+
+ If a state from the propagations is included in another state which has
+ already been propagated, it may be removed from the output propagation.
+ Likewise, if a state from a propagation is included in a state from
+ another propagation of the list (coming from another edge or iteration),
+ it may also be removed.
+
+ This function also interprets partitioning annotations at the store
+ vertex (slevel, splits, merges, ...) which will generally change the
+ current partitioning. *)
+ val join : (Partition.branch * flow) list -> store -> flow
+
+ (** Widen a flow. The widening object keeps track of the previous widenings
+ and previous propagated states to ensure termination. The result is true
+ when it is correct to end the propagation here, i.e. when the flow
+ object is only containng states which are included into already propagated
+ states. *)
+ val widen : widening -> flow -> bool
+
+end
--
GitLab