diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index 3ab7878306eaa3f8abb5ed4e234a11b1a79f4ffa..57806d98601a89e71b58b76c3ee291bea7225090 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -639,12 +639,14 @@ module Make
(* Subdivision of the evaluation of the expression [expr], according to the
values of a list of lvalues [lvals], in the state [state].
[subexpr] is the smallest subexpression of [expr] containing all
- occurrences of the lvalues in [lvals]. At the end of the subdivision, we
- reduce the final value of [expr], [subexpr], and of the lvalues in [lvals].
+ occurrences of the lvalues in [lvals].
[valuation] is the result of the evaluation of [expr] without subdivision.
- This function returns the alarms and the valuation resulting from the
- subdivided evaluation. *)
- let subdivide_lvals context valuation subdivnb expr subexpr lvals =
+ The subdivision is stopped after [subdivnb] splits, or as soon as they can
+ no longer improve the precision of the value computed for [expr].
+ The function returns the alarms and the valuation resulting from the
+ subdivided evaluation. In the resulting valuation, the values of [expr],
+ [subexpr] and of the lvalues in [lvals] have been reduced. *)
+ let subdivide_lvals context valuation subdivnb ~expr ~subexpr lvals =
let Hypotheses.L variables = Hypotheses.from_list lvals in
(* Split function for the subvalues of [lvals]. *)
let split = make_split valuation variables in
@@ -742,13 +744,15 @@ module Make
(* List of non-linear subexpressions [subexpr], with the lvalues that
appear multiple times in [subexpr], candidates for the subdivision. *)
let vars = compute_non_linear expr in
+ (* Compute necessary information about the lvalues to be subdivided.
+ Also remove lvalues with pointer or singleton values. *)
+ let make_info = make_info_list context initial_valuation in
+ let vars_info = List.map (fun (e, lvals) -> e, make_info lvals) vars in
+ let vars_info = List.filter (fun (_, infos) -> infos <> []) vars_info in
let rec subdivide_subexpr vars valuation result alarms =
match vars with
| [] -> `Value (valuation, result), alarms
- | (subexpr, lvals) :: tail ->
- (* Retrieve necessary information about the lvalues.
- Also remove lvalues with pointer or singleton values. *)
- let lvals_info = make_info_list context initial_valuation lvals in
+ | (subexpr, lvals_info) :: tail ->
match lvals_info with
| [] -> subdivide_subexpr tail valuation result alarms
| _ ->
@@ -767,10 +771,26 @@ module Make
Value_parameters.result ~current:true ~once:true ~dkey
"subdividing on %a"
(Pretty_utils.pp_list ~sep:", " Printer.pp_lval) lvals;
- subdivide_lvals context valuation subdivnb expr subexpr lvals_info
- >>> subdivide_subexpr tail
+ let subdivide =
+ subdivide_lvals context valuation subdivnb lvals_info
+ in
+ (* If there are no other variables to subdivide, stops the
+ subdivision as soon as they can no longer improve the value
+ of the final expression [expr]. *)
+ if tail = []
+ then subdivide ~expr ~subexpr
+ else
+ (* Otherwise, later subdivisions on other sub-expressions may
+ improve the value of [expr] thanks to a reduction of [subexpr],
+ even if this reduction has not directly improved the value of
+ [expr]. Thus, stop the subdivisions according to [subexpr]
+ instead of [expr]. Use [~expr:subexpr], then evaluate [expr]
+ with the reduced valuation, then continue to subdivide. *)
+ subdivide ~expr:subexpr ~subexpr >>> fun valuation _ _ ->
+ Eva.evaluate context valuation expr >>>
+ subdivide_subexpr tail
in
- subdivide_subexpr vars valuation result alarms
+ subdivide_subexpr vars_info valuation result alarms
let evaluate context valuation ~subdivnb expr =
if subdivnb = 0 || not activated
diff --git a/tests/float/oracle/nonlin.1.res.oracle b/tests/float/oracle/nonlin.1.res.oracle
index 3a1506cfa7bae0a013c33b2f8ac41af58f2b66cf..3ddef66ef496f7061b9f8444af849b2b4bd1bafb 100644
--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -342,7 +342,7 @@
d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
[eva:final-states] Values at end of function norm:
Frama_C_entropy_source ∈ [--..--]
- v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+ v1 ∈ [-0x1.0f0cde0000000p64 .. 0x1.bc16d60000000p59]
v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
square ∈ [0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
square2 ∈ [0x0.0000000000000p0 .. 0x1.fffffe0000000p127]
diff --git a/tests/float/oracle/nonlin.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index 2b0e030e86b354257dc29606a9413e9e8dcd4744..ba81c19d44c306730614d89d500ccdb7fde507a5 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -317,7 +317,7 @@
v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
square ∈ [0x0.0000000000000p0 .. inf] ∪ {NaN}
- square2 ∈ [-inf .. inf] ∪ {NaN}
+ square2 ∈ [0x0.0000000000000p0 .. inf]
[eva:final-states] Values at end of function other:
Frama_C_entropy_source ∈ [--..--]
i ∈ [-0x1.8effffffffff7p1 .. 0x1.8680000000000p1]
diff --git a/tests/float/oracle/nonlin.4.res.oracle b/tests/float/oracle/nonlin.4.res.oracle
index d891c92adecec0773a0a204be2e8ade3147c4753..2f06c2710cf66d8592b8fdae363e0a41589b4481 100644
--- a/tests/float/oracle/nonlin.4.res.oracle
+++ b/tests/float/oracle/nonlin.4.res.oracle
@@ -342,7 +342,7 @@
d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
[eva:final-states] Values at end of function norm:
Frama_C_entropy_source ∈ [--..--]
- v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+ v1 ∈ [-0x1.0f0cde0000000p64 .. 0x1.bc16d60000000p59]
v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
square ∈ [0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
square2 ∈ [0x0.0000000000000p0 .. 0x1.fffffe0000000p127]
diff --git a/tests/float/oracle/nonlin.5.res.oracle b/tests/float/oracle/nonlin.5.res.oracle
index 3a7da9b287ed6d48a6065ed1689ff2f9760e1681..a26018dc5a7b1e8f6e79c7f951bc2d4b1e746db0 100644
--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -317,7 +317,7 @@
v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
square ∈ [0x0.0000000000000p0 .. inf] ∪ {NaN}
- square2 ∈ [-inf .. inf] ∪ {NaN}
+ square2 ∈ [0x0.0000000000000p0 .. inf]
[eva:final-states] Values at end of function other:
Frama_C_entropy_source ∈ [--..--]
i ∈ [-0x1.8efff00000000p1 .. 0x1.8680000000000p1]
diff --git a/tests/value/oracle/nonlin.res.oracle b/tests/value/oracle/nonlin.res.oracle
index ca1b870962dc9a89c3d58e9d29bea23a70cbdfec..1783b2b8ca0f5b2892b7b555733d4c107057dd16 100644
--- a/tests/value/oracle/nonlin.res.oracle
+++ b/tests/value/oracle/nonlin.res.oracle
@@ -198,7 +198,7 @@
y ∈ [-10..10]
z ∈ [-10..10]
norm ∈ [0..200]
- mult ∈ [-10000..10000]
+ mult ∈ [0..10000]
zero ∈ [-26..26]
square ∈ [-48..400]
square2 ∈ [-48..400]