diff --git a/src/plugins/value/engine/basic_partitioning.ml b/src/plugins/value/engine/basic_partitioning.ml index ca14677cc57a45b07e9da67418bb96f2b03cf5dc..ae99cfef5dc0c0e3fa85292ba024326b7ccbfa92 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 29552b96f667365380db7a0b632cf597c01085bd..bee9eba706bbe1df282416ca133e6ad35c265c87 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 3036e5bd5a397dda9ee62c14deeb7d967c63fcc7..a6700d0c89021b88247c4f6f692926140260bc04 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 8a7d4a1be7da52c943e88bffcef343ddc54d4f6a..aa0be86c0bb64f3d80441a05509ce8adab7a4037 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 a7b54408b6a3f910d4d6984577e18c8fcc386810..a76253bb3b3c35a6ecffcdfc75cdd2c1a269bd30 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