From 3e0e136d88422f54684f0f950c33c516d3d31421 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 13 Feb 2020 18:02:03 +0100
Subject: [PATCH] [Eva] Subdivision: slightly changes the strategy to cut a
float interval in half.
If an interval contains positive and negative floating-point values, cuts the
interval at 0. Otherwise, uses the same strategy as before: cuts the interval
at the mathematical average of its bounds.
This strategy always reaches the maximal precision in one split on e*e squares,
which is the most common pattern for subdivisions.
In the tests, it decreases the precision on computations of e-e, where a split
at 0 is useless. However, this is not a common pattern in real codes.
---
.../abstract_interp/float_interval.ml | 28 ++++++++-------
tests/float/oracle/nonlin.1.res.oracle | 34 +++++++++---------
tests/float/oracle/nonlin.2.res.oracle | 28 +++++++--------
tests/float/oracle/nonlin.4.res.oracle | 36 +++++++++----------
tests/float/oracle/nonlin.5.res.oracle | 30 ++++++++--------
.../misc/oracle/widen_hints_float.res.oracle | 2 +-
6 files changed, 80 insertions(+), 78 deletions(-)
diff --git a/src/kernel_services/abstract_interp/float_interval.ml b/src/kernel_services/abstract_interp/float_interval.ml
index a881b716947..3e56c2698cf 100644
--- a/src/kernel_services/abstract_interp/float_interval.ml
+++ b/src/kernel_services/abstract_interp/float_interval.ml
@@ -1100,10 +1100,10 @@ module Make (F: Float_sig.S) = struct
Subdivision
------------------------------------------------------------------------ *)
- (* [avg] and [split] implement two different strategies for cutting a
+ (* [avg] and [balance] implement two different strategies for cutting a
floating-point interval in half: [avg] computes the mathematical average of
- the two bounds, while [split] balances the number of representable values
- of the given precision in each resulting intervals. *)
+ the two bounds, while [balance] balances the number of representable double
+ values in each resulting intervals. *)
(* Computes the average between two ocaml doubles. *)
let avg x y =
@@ -1112,20 +1112,22 @@ module Make (F: Float_sig.S) = struct
then fy +. (fx -. fy) /. 2.
else (fx +. fy) /. 2.
- (* assumption: [0. <= x <= y]. returns the median of the range [x..y]
+ (* Assumption: [0. <= x <= y]. Returns the median of the range [x..y]
in number of double values. *)
- let split_positive prec x y =
+ let _balance x y =
let ix = Int64.bits_of_float (F.to_float x) in
let iy = Int64.bits_of_float (F.to_float y) in
- let f = Int64.(float_of_bits (add ix (div (sub iy ix) 2L))) in
- F.of_float Near prec f
+ Int64.(float_of_bits (add ix (div (sub iy ix) 2L)))
- (* assumption: [x <= y] *)
- let _split prec x y =
+ (* Can be [avg] or [balance]. *)
+ let split_positive = avg
+
+ (* Assumption: [x <= y]. *)
+ let split x y =
match F.is_negative x, F.is_negative y with
- | false, false -> split_positive prec x y
- | true, true -> F.neg (split_positive prec (F.neg x) (F.neg y))
- | true, false -> Cst.neg_zero prec
+ | false, false -> split_positive x y
+ | true, true -> -. (split_positive (F.neg x) (F.neg y))
+ | true, false -> -0.
| false, true -> assert false
exception Can_not_subdiv = Abstract_interp.Can_not_subdiv
@@ -1149,7 +1151,7 @@ module Make (F: Float_sig.S) = struct
else if Cmp.equal (F.next_float prec b) e
then b, e
else
- let midpoint = avg b e in
+ let midpoint = split b e in
let midpoint = F.of_float Down prec midpoint in
let smidpoint =
if F.is_exact prec then F.next_float prec midpoint else midpoint
diff --git a/tests/float/oracle/nonlin.1.res.oracle b/tests/float/oracle/nonlin.1.res.oracle
index 3605d95496f..3a1506cfa7b 100644
--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -342,22 +342,22 @@
d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
[eva:final-states] Values at end of function norm:
Frama_C_entropy_source ∈ [--..--]
- v1 ∈ [-0x1.0133220000000p64 .. 0x1.bc16d60000000p59]
- v2 ∈ [-0x1.0133220000000p64 .. 0x1.bc16d60000000p59]
- square ∈ [-0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
- square2 ∈ [-0x1.a618a60000000p123 .. 0x1.fffffe0000000p127]
+ v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+ v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+ square ∈ [0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
+ square2 ∈ [0x0.0000000000000p0 .. 0x1.fffffe0000000p127]
[eva:final-states] Values at end of function other:
Frama_C_entropy_source ∈ [--..--]
- i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
+ i ∈ [-0x1.8effffffffff7p1 .. 0x1.8680000000000p1]
s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
- zf ∈ [-0x1.12ffffffffffep4 .. 0x1.12ffffffffffep4]
+ zf ∈ [-0x1.1bffffffffffcp4 .. 0x1.1bffffffffffcp4]
s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
- sq ∈ [-0x1.b37ffffffff34p-7 .. 0x1.3b10000000000p14]
- h ∈ [-0x1.38d8000000000p14 .. 0x1.3250000000034p-1]
- r ∈ [3..11]
+ sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+ h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dfffffffffep-2]
+ r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
x ∈ [1..42]
y ∈ {0; 1}
- z ∈ [-171874..171874]
+ z ∈ [-177499..177499]
rbits1 ∈ {0; 1; 2}
rbits2 ∈ {0; 1}
[eva:final-states] Values at end of function split_alarm:
@@ -367,7 +367,7 @@
Frama_C_entropy_source ∈ [--..--]
x_0 ∈ [-0x1.3880000000000p15 .. 0x1.3880000000000p15]
d_0 ∈ {0x1.3880000000000p13}
- square1 ∈ [-0x1.c1e15ac305198p-13 .. 0x1.3880000000000p13]
+ square1 ∈ [0x0.0000000000000p0 .. 0x1.3880000000000p13]
square2 ∈ [-0x1.fffffffffffffp1001 .. 0x1.fffffffffffffp1023]
square3 ∈ [-0x0.0000000000000p0 .. 0x1.2a05f20000000p31]
[eva:final-states] Values at end of function main:
@@ -378,15 +378,15 @@
r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffffffffffp2]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
- i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
+ i ∈ [-0x1.8effffffffff7p1 .. 0x1.8680000000000p1]
s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
- zf ∈ [-0x1.12ffffffffffep4 .. 0x1.12ffffffffffep4]
+ zf ∈ [-0x1.1bffffffffffcp4 .. 0x1.1bffffffffffcp4]
s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
- sq ∈ [-0x1.b37ffffffff34p-7 .. 0x1.3b10000000000p14]
- h ∈ [-0x1.38d8000000000p14 .. 0x1.3250000000034p-1]
- r ∈ [3..11]
+ sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+ h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dfffffffffep-2]
+ r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
x ∈ [1..42]
y ∈ {0; 1}
- z ∈ [-171874..171874]
+ z ∈ [-177499..177499]
rbits1 ∈ {0; 1; 2}
rbits2 ∈ {0; 1}
diff --git a/tests/float/oracle/nonlin.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index 3e52ec0cee5..2b0e030e86b 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -316,20 +316,20 @@
Frama_C_entropy_source ∈ [--..--]
v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
- square ∈ [-0x0.0000000000000p0 .. inf] ∪ {NaN}
+ square ∈ [0x0.0000000000000p0 .. inf] ∪ {NaN}
square2 ∈ [-inf .. inf] ∪ {NaN}
[eva:final-states] Values at end of function other:
Frama_C_entropy_source ∈ [--..--]
- i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
+ i ∈ [-0x1.8effffffffff7p1 .. 0x1.8680000000000p1]
s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
- zf ∈ [-0x1.12ffffffffffep4 .. 0x1.12ffffffffffep4]
+ zf ∈ [-0x1.1bffffffffffcp4 .. 0x1.1bffffffffffcp4]
s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
- sq ∈ [-0x1.b37ffffffff34p-7 .. 0x1.3b10000000000p14]
- h ∈ [-0x1.38d8000000000p14 .. 0x1.3250000000034p-1]
- r ∈ [3..11]
+ sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+ h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dfffffffffep-2]
+ r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
x ∈ [1..42]
y ∈ {0; 1}
- z ∈ [-171874..171874]
+ z ∈ [-177499..177499]
rbits1 ∈ {0; 1; 2}
rbits2 ∈ {0; 1}
[eva:final-states] Values at end of function split_alarm:
@@ -339,7 +339,7 @@
Frama_C_entropy_source ∈ [--..--]
x_0 ∈ [-0x1.3880000000000p15 .. 0x1.3880000000000p15]
d_0 ∈ {0x1.3880000000000p13}
- square1 ∈ [-0x1.c1e15ac305198p-13 .. 0x1.3880000000000p13]
+ square1 ∈ [0x0.0000000000000p0 .. 0x1.3880000000000p13]
square2 ∈ [-0x1.fffffffffffffp1014 .. inf] ∪ {NaN}
square3 ∈ [-0x0.0000000000000p0 .. 0x1.2a05f20000000p31]
[eva:final-states] Values at end of function main:
@@ -350,15 +350,15 @@
r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffffffffffp2]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
- i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
+ i ∈ [-0x1.8effffffffff7p1 .. 0x1.8680000000000p1]
s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
- zf ∈ [-0x1.12ffffffffffep4 .. 0x1.12ffffffffffep4]
+ zf ∈ [-0x1.1bffffffffffcp4 .. 0x1.1bffffffffffcp4]
s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
- sq ∈ [-0x1.b37ffffffff34p-7 .. 0x1.3b10000000000p14]
- h ∈ [-0x1.38d8000000000p14 .. 0x1.3250000000034p-1]
- r ∈ [3..11]
+ sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+ h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dfffffffffep-2]
+ r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
x ∈ [1..42]
y ∈ {0; 1}
- z ∈ [-171874..171874]
+ z ∈ [-177499..177499]
rbits1 ∈ {0; 1; 2}
rbits2 ∈ {0; 1}
diff --git a/tests/float/oracle/nonlin.4.res.oracle b/tests/float/oracle/nonlin.4.res.oracle
index 37f4cb97df6..d891c92adec 100644
--- a/tests/float/oracle/nonlin.4.res.oracle
+++ b/tests/float/oracle/nonlin.4.res.oracle
@@ -320,7 +320,7 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
- x0 ∈ [0..3224938487]
+ x0 ∈ [0..3225911288]
__retres ∈ {0; 1}
[eva:final-states] Values at end of function around_zeros:
Frama_C_entropy_source ∈ [--..--]
@@ -342,22 +342,22 @@
d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
[eva:final-states] Values at end of function norm:
Frama_C_entropy_source ∈ [--..--]
- v1 ∈ [-0x1.0133220000000p64 .. 0x1.bc16d60000000p59]
- v2 ∈ [-0x1.0133220000000p64 .. 0x1.bc16d60000000p59]
- square ∈ [-0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
- square2 ∈ [-0x1.a618a60000000p123 .. 0x1.fffffe0000000p127]
+ v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+ v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+ square ∈ [0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
+ square2 ∈ [0x0.0000000000000p0 .. 0x1.fffffe0000000p127]
[eva:final-states] Values at end of function other:
Frama_C_entropy_source ∈ [--..--]
- i ∈ [-0x1.714fee0000000p1 .. 0x1.71c0040000000p1]
+ i ∈ [-0x1.8efff00000000p1 .. 0x1.8680000000000p1]
s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
- zf ∈ [-0x1.12fffc0000000p4 .. 0x1.12fffc0000000p4]
+ zf ∈ [-0x1.1bfff80000000p4 .. 0x1.1bfff80000000p4]
s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
- sq ∈ [-0x1.b37e680000000p-7 .. 0x1.3b10000000000p14]
- h ∈ [-0x1.38d8000000000p14 .. 0x1.3250680000000p-1]
- r ∈ [3..11]
+ sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+ h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dffc0000000p-2]
+ r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
x ∈ [1..42]
y ∈ {0; 1}
- z ∈ [-171874..171874]
+ z ∈ [-177499..177499]
rbits1 ∈ {0; 1; 2}
rbits2 ∈ {0; 1}
[eva:final-states] Values at end of function split_alarm:
@@ -367,7 +367,7 @@
Frama_C_entropy_source ∈ [--..--]
x_0 ∈ [-0x1.3880000000000p15 .. 0x1.3880000000000p15]
d_0 ∈ {0x1.3880000000000p13}
- square1 ∈ [-0x1.c1e2e00000000p-13 .. 0x1.3880000000000p13]
+ square1 ∈ [0x0.0000000000000p0 .. 0x1.3880000000000p13]
square2 ∈ [-0x1.fffffe0000000p105 .. 0x1.fffffe0000000p127]
square3 ∈ [-0x0.0000000000000p0 .. 0x1.2a05f20000000p31]
[eva:final-states] Values at end of function main:
@@ -378,15 +378,15 @@
r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
- i ∈ [-0x1.714fee0000000p1 .. 0x1.71c0040000000p1]
+ i ∈ [-0x1.8efff00000000p1 .. 0x1.8680000000000p1]
s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
- zf ∈ [-0x1.12fffc0000000p4 .. 0x1.12fffc0000000p4]
+ zf ∈ [-0x1.1bfff80000000p4 .. 0x1.1bfff80000000p4]
s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
- sq ∈ [-0x1.b37e680000000p-7 .. 0x1.3b10000000000p14]
- h ∈ [-0x1.38d8000000000p14 .. 0x1.3250680000000p-1]
- r ∈ [3..11]
+ sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+ h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dffc0000000p-2]
+ r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
x ∈ [1..42]
y ∈ {0; 1}
- z ∈ [-171874..171874]
+ z ∈ [-177499..177499]
rbits1 ∈ {0; 1; 2}
rbits2 ∈ {0; 1}
diff --git a/tests/float/oracle/nonlin.5.res.oracle b/tests/float/oracle/nonlin.5.res.oracle
index 531c482e3f6..3a7da9b287e 100644
--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -292,7 +292,7 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
- x0 ∈ [0..3224938487]
+ x0 ∈ [0..3225911288]
__retres ∈ {0; 1}
[eva:final-states] Values at end of function around_zeros:
Frama_C_entropy_source ∈ [--..--]
@@ -316,20 +316,20 @@
Frama_C_entropy_source ∈ [--..--]
v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
- square ∈ [-0x0.0000000000000p0 .. inf] ∪ {NaN}
+ square ∈ [0x0.0000000000000p0 .. inf] ∪ {NaN}
square2 ∈ [-inf .. inf] ∪ {NaN}
[eva:final-states] Values at end of function other:
Frama_C_entropy_source ∈ [--..--]
- i ∈ [-0x1.714fee0000000p1 .. 0x1.71c0040000000p1]
+ i ∈ [-0x1.8efff00000000p1 .. 0x1.8680000000000p1]
s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
- zf ∈ [-0x1.12fffc0000000p4 .. 0x1.12fffc0000000p4]
+ zf ∈ [-0x1.1bfff80000000p4 .. 0x1.1bfff80000000p4]
s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
- sq ∈ [-0x1.b37e680000000p-7 .. 0x1.3b10000000000p14]
- h ∈ [-0x1.38d8000000000p14 .. 0x1.3250680000000p-1]
- r ∈ [3..11]
+ sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+ h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dffc0000000p-2]
+ r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
x ∈ [1..42]
y ∈ {0; 1}
- z ∈ [-171874..171874]
+ z ∈ [-177499..177499]
rbits1 ∈ {0; 1; 2}
rbits2 ∈ {0; 1}
[eva:final-states] Values at end of function split_alarm:
@@ -339,7 +339,7 @@
Frama_C_entropy_source ∈ [--..--]
x_0 ∈ [-0x1.3880000000000p15 .. 0x1.3880000000000p15]
d_0 ∈ {0x1.3880000000000p13}
- square1 ∈ [-0x1.c1e2e00000000p-13 .. 0x1.3880000000000p13]
+ square1 ∈ [0x0.0000000000000p0 .. 0x1.3880000000000p13]
square2 ∈ [-0x1.fffffe0000000p118 .. inf] ∪ {NaN}
square3 ∈ [-0x0.0000000000000p0 .. 0x1.2a05f20000000p31]
[eva:final-states] Values at end of function main:
@@ -350,15 +350,15 @@
r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2]
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
- i ∈ [-0x1.714fee0000000p1 .. 0x1.71c0040000000p1]
+ i ∈ [-0x1.8efff00000000p1 .. 0x1.8680000000000p1]
s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
- zf ∈ [-0x1.12fffc0000000p4 .. 0x1.12fffc0000000p4]
+ zf ∈ [-0x1.1bfff80000000p4 .. 0x1.1bfff80000000p4]
s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
- sq ∈ [-0x1.b37e680000000p-7 .. 0x1.3b10000000000p14]
- h ∈ [-0x1.38d8000000000p14 .. 0x1.3250680000000p-1]
- r ∈ [3..11]
+ sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+ h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dffc0000000p-2]
+ r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
x ∈ [1..42]
y ∈ {0; 1}
- z ∈ [-171874..171874]
+ z ∈ [-177499..177499]
rbits1 ∈ {0; 1; 2}
rbits2 ∈ {0; 1}
diff --git a/tests/misc/oracle/widen_hints_float.res.oracle b/tests/misc/oracle/widen_hints_float.res.oracle
index 087bdf14a4f..45e531fdbc4 100644
--- a/tests/misc/oracle/widen_hints_float.res.oracle
+++ b/tests/misc/oracle/widen_hints_float.res.oracle
@@ -145,7 +145,7 @@
Frama_C_entropy_source ∈ [--..--]
f1 ∈ [-0. .. 71.]
f2 ∈ [-80. .. 0.]
- f3 ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ f3 ∈ [-1.79769313486e+308 .. 10000000000.]
[eva:final-states] Values at end of function trigo:
Frama_C_entropy_source ∈ [--..--]
f1 ∈ [-1. .. 1.]
--
GitLab