From 71c3681786e70c8d411e890f5da69a3741a4bd93 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 6 Feb 2020 18:10:34 +0100
Subject: [PATCH] [Eva] Subdivision: slightly changes the heuristic to stop
subdivisions.
Do not stop the subdivision if it can reduce the value of a sub-expression
*and* later subdivisions may improve the value of the complete expression
with this reduction.
If no other subdivision is planned, then stop the subdivision if it cannot
improve the value of the complete expression (as before).
---
.../value/engine/subdivided_evaluation.ml | 44 ++++++++++++++-----
tests/float/oracle/nonlin.1.res.oracle | 2 +-
tests/float/oracle/nonlin.2.res.oracle | 2 +-
tests/float/oracle/nonlin.4.res.oracle | 2 +-
tests/float/oracle/nonlin.5.res.oracle | 2 +-
tests/value/oracle/nonlin.res.oracle | 2 +-
6 files changed, 37 insertions(+), 17 deletions(-)
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index 3ab7878306e..57806d98601 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 3a1506cfa7b..3ddef66ef49 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 2b0e030e86b..ba81c19d44c 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 d891c92adec..2f06c2710cf 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 3a7da9b287e..a26018dc5a7 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 ca1b870962d..1783b2b8ca0 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]
--
GitLab