From d65de28407ab7893efb82e8f30f432a8f14610f6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 19 Oct 2018 10:36:51 +0200
Subject: [PATCH] [Eva] Improves widenings on nested loops.
On nested loops, for each iteration of the outer loop, postpone the widening of
the inner loop of [delay] iterations, [delay] being set by -eva-widening-delay.
Example:
while (i < n) {
j = 0;
while (j < 100) { j++; }
i++;
}
On such nested loops, the fixpoint of the inner loop is independent from the
outer loop.
At the first iteration of the outer loop, a fixpoint is reached for the inner
loop. For other iterations of the outer loop, only one iteration of the inner
loop is needed to reach a new fixpoint, by only updating the variables modified
by the outer loop (i here). Avoiding widening during this one iteration is
crucial for precision, as the widening of the inner loop would widen the
variable i, leading to an overflow alarm at i++.
---
src/plugins/value/engine/basic_partitioning.ml | 3 +++
src/plugins/value/engine/legacy_partitioning.ml | 2 ++
src/plugins/value/engine/loop_partitioning.ml | 4 ++++
src/plugins/value/engine/partitioned_dataflow.ml | 5 +++--
src/plugins/value/engine/state_partitioning.mli | 1 +
5 files changed, 13 insertions(+), 2 deletions(-)
diff --git a/src/plugins/value/engine/basic_partitioning.ml b/src/plugins/value/engine/basic_partitioning.ml
index a2ee7cd2334..ca14677cc57 100644
--- a/src/plugins/value/engine/basic_partitioning.ml
+++ b/src/plugins/value/engine/basic_partitioning.ml
@@ -182,6 +182,9 @@ struct
w.previous_state <- `Bottom;
w.widening_counter <- widening_delay
+ let reset_widening_counter (w : widening) : unit =
+ w.widening_counter <- widening_delay
+
(* Operators *)
let clear_propagation (p : propagation) : unit =
diff --git a/src/plugins/value/engine/legacy_partitioning.ml b/src/plugins/value/engine/legacy_partitioning.ml
index 119ce80be5b..29552b96f66 100644
--- a/src/plugins/value/engine/legacy_partitioning.ml
+++ b/src/plugins/value/engine/legacy_partitioning.ml
@@ -141,6 +141,8 @@ struct
w.previous_state <- `Bottom;
w.widening_counter <- widening_delay
+ let reset_widening_counter w = w.widening_counter <- widening_delay
+
(* Operators *)
let clear_propagation (p : propagation) : unit =
diff --git a/src/plugins/value/engine/loop_partitioning.ml b/src/plugins/value/engine/loop_partitioning.ml
index eda3d98eadd..3036e5bd5a3 100644
--- a/src/plugins/value/engine/loop_partitioning.ml
+++ b/src/plugins/value/engine/loop_partitioning.ml
@@ -359,6 +359,10 @@ struct
in
Tree.iter reset w.widening_tree
+ let reset_widening_counter (w : widening) : unit =
+ let reset w = w.widening_counter <- widening_delay in
+ Tree.iter reset w.widening_tree
+
(* Operators *)
let clear_propagation (p : propagation) : unit =
diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml
index 24468248e01..8a7d4a1be7d 100644
--- a/src/plugins/value/engine/partitioned_dataflow.ml
+++ b/src/plugins/value/engine/partitioned_dataflow.ml
@@ -624,8 +624,9 @@ module Make_Dataflow
ignore (process_vertex v)
| Wto.Component (v, w) as component ->
(* Reset the component if hierachical_convergence is set *)
- if hierachical_convergence then
- reset_component (v :: Wto.flatten w);
+ if hierachical_convergence
+ then reset_component (v :: Wto.flatten w)
+ else Partition.reset_widening_counter (get_vertex_widening v);
(* Iterate until convergence *)
let iteration_count = ref 0 in
while
diff --git a/src/plugins/value/engine/state_partitioning.mli b/src/plugins/value/engine/state_partitioning.mli
index 50932afe1d8..a7b54408b6a 100644
--- a/src/plugins/value/engine/state_partitioning.mli
+++ b/src/plugins/value/engine/state_partitioning.mli
@@ -90,6 +90,7 @@ sig
val reset_propagation : propagation -> unit
val reset_shadow : shadow -> unit
val reset_widening : widening -> unit
+ val reset_widening_counter : widening -> unit
(* --- Partition transfer functions --- *)
--
GitLab