From 61cbcef3628999d214d5a1b4b2f5cfd8a905b85d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 9 Jan 2019 13:39:36 +0100
Subject: [PATCH] [Eva] Uses the period (instead of delay) to postpone the
widening of nested loops.
Also adds some comments.
---
src/plugins/value/engine/basic_partitioning.ml | 2 +-
src/plugins/value/engine/legacy_partitioning.ml | 3 ++-
src/plugins/value/engine/loop_partitioning.ml | 4 +++-
src/plugins/value/engine/partitioned_dataflow.ml | 4 +++-
src/plugins/value/engine/state_partitioning.mli | 5 +++++
5 files changed, 14 insertions(+), 4 deletions(-)
diff --git a/src/plugins/value/engine/basic_partitioning.ml b/src/plugins/value/engine/basic_partitioning.ml
index ca14677cc57..ae99cfef5dc 100644
--- a/src/plugins/value/engine/basic_partitioning.ml
+++ b/src/plugins/value/engine/basic_partitioning.ml
@@ -183,7 +183,7 @@ struct
w.widening_counter <- widening_delay
let reset_widening_counter (w : widening) : unit =
- w.widening_counter <- widening_delay
+ w.widening_counter <- max w.widening_counter (widening_period - 1)
(* Operators *)
diff --git a/src/plugins/value/engine/legacy_partitioning.ml b/src/plugins/value/engine/legacy_partitioning.ml
index 29552b96f66..bee9eba706b 100644
--- a/src/plugins/value/engine/legacy_partitioning.ml
+++ b/src/plugins/value/engine/legacy_partitioning.ml
@@ -141,7 +141,8 @@ struct
w.previous_state <- `Bottom;
w.widening_counter <- widening_delay
- let reset_widening_counter w = w.widening_counter <- widening_delay
+ let reset_widening_counter w =
+ w.widening_counter <- max w.widening_counter (widening_period - 1)
(* Operators *)
diff --git a/src/plugins/value/engine/loop_partitioning.ml b/src/plugins/value/engine/loop_partitioning.ml
index 3036e5bd5a3..a6700d0c890 100644
--- a/src/plugins/value/engine/loop_partitioning.ml
+++ b/src/plugins/value/engine/loop_partitioning.ml
@@ -360,7 +360,9 @@ struct
Tree.iter reset w.widening_tree
let reset_widening_counter (w : widening) : unit =
- let reset w = w.widening_counter <- widening_delay in
+ let reset w =
+ w.widening_counter <- max w.widening_counter (widening_period - 1)
+ in
Tree.iter reset w.widening_tree
(* Operators *)
diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml
index 8a7d4a1be7d..aa0be86c0bb 100644
--- a/src/plugins/value/engine/partitioned_dataflow.ml
+++ b/src/plugins/value/engine/partitioned_dataflow.ml
@@ -623,7 +623,9 @@ module Make_Dataflow
| Wto.Node v ->
ignore (process_vertex v)
| Wto.Component (v, w) as component ->
- (* Reset the component if hierachical_convergence is set *)
+ (* Reset the component if hierachical_convergence is set.
+ Otherwise, only resets the widening counter for this component. This
+ is especially useful for nested loops. *)
if hierachical_convergence
then reset_component (v :: Wto.flatten w)
else Partition.reset_widening_counter (get_vertex_widening v);
diff --git a/src/plugins/value/engine/state_partitioning.mli b/src/plugins/value/engine/state_partitioning.mli
index a7b54408b6a..a76253bb3b3 100644
--- a/src/plugins/value/engine/state_partitioning.mli
+++ b/src/plugins/value/engine/state_partitioning.mli
@@ -90,6 +90,11 @@ sig
val reset_propagation : propagation -> unit
val reset_shadow : shadow -> 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
--
GitLab