From a9cdb059e17583f178dba879475fdf70604d9473 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 11 Feb 2021 09:47:47 +0100
Subject: [PATCH] [libc] math.h: adds behaviors for NaN and infinite cases in
exp specifications.
---
share/libc/math.h | 58 +++++++++++-
tests/float/oracle/builtins.res.oracle | 48 +++++++---
tests/float/oracle/math_builtins.res.oracle | 97 +++++++++++++++------
tests/float/oracle/sqrt.0.res.oracle | 2 +
tests/float/oracle/sqrt.1.res.oracle | 2 +
5 files changed, 161 insertions(+), 46 deletions(-)
diff --git a/share/libc/math.h b/share/libc/math.h
index 84751ea44f6..566406dfae8 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -515,19 +515,69 @@ extern double tanh(double x);
extern float tanhf(float x);
extern long double tanhl(long double x);
-/*@ requires finite_arg: \is_finite(x);
- requires finite_domain: x <= 0x1.62e42fefa39efp+9;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes domain_arg: x >= -0x1.74910d52d3051p9 && x <= 0x1.62e42fefa39efp+9;
assigns \result \from x;
ensures res_finite: \is_finite(\result);
ensures positive_result: \result > 0.;
+ behavior overflow:
+ assumes overflow_arg: \is_finite(x) && x > 0x1.62e42fefa39efp+9;
+ ensures infinite_res: \is_plus_infinity(\result);
+ ensures errno_set: errno == ERANGE;
+ behavior plus_infinity:
+ assumes plus_infinity_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinity_result: \is_plus_infinity(\result);
+ behavior underflow:
+ assumes underflow_arg: \is_finite(x) && x < -0x1.74910d52d3051p9;
+ ensures zero_res: \result == 0.;
+ ensures errno_set: errno == ERANGE;
+ behavior minus_infinity:
+ assumes plus_infinity_arg: \is_minus_infinity(x);
+ assigns \result \from x;
+ ensures zero_result: \is_finite(\result) && \result == 0.;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double exp(double x);
-/*@ requires finite_arg: \is_finite(x);
- requires res_finite: x <= 0x1.62e42ep+6;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes domain_arg: x >= -0x1.9fe368p6 && x <= 0x1.62e42ep+6;
assigns \result \from x;
ensures res_finite: \is_finite(\result);
ensures positive_result: \result > 0.;
+ behavior overflow:
+ assumes overflow_arg: \is_finite(x) && x > 0x1.62e42ep+6;
+ ensures infinite_res: \is_plus_infinity(\result);
+ ensures errno_set: errno == ERANGE;
+ behavior plus_infinity:
+ assumes plus_infinity_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinity_result: \is_plus_infinity(\result);
+ behavior underflow:
+ assumes underflow_arg: \is_finite(x) && x < -0x1.9fe368p6;
+ ensures zero_res: \result == 0.;
+ ensures errno_set: errno == ERANGE;
+ behavior minus_infinity:
+ assumes plus_infinity_arg: \is_minus_infinity(x);
+ assigns \result \from x;
+ ensures zero_result: \is_finite(\result) && \result == 0.;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float expf(float x);
diff --git a/tests/float/oracle/builtins.res.oracle b/tests/float/oracle/builtins.res.oracle
index 66f30707d32..e6023b3d1ca 100644
--- a/tests/float/oracle/builtins.res.oracle
+++ b/tests/float/oracle/builtins.res.oracle
@@ -99,30 +99,46 @@
function log10: precondition 'arg_positive' got status invalid.
[eva] tests/float/builtins.c:85: Call to builtin exp
[eva] tests/float/builtins.c:85:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
[eva] tests/float/builtins.c:85:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+[eva] tests/float/builtins.c:85:
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/builtins.c:88: Call to builtin exp
[eva] tests/float/builtins.c:88:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+[eva] tests/float/builtins.c:88:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/builtins.c:88:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/builtins.c:91: Call to builtin exp
[eva] tests/float/builtins.c:91:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+[eva] tests/float/builtins.c:91:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/builtins.c:91:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva:alarm] tests/float/builtins.c:94: Warning: assertion got status unknown.
[eva] tests/float/builtins.c:95: Call to builtin exp
-[eva] tests/float/builtins.c:95:
- function exp: precondition 'finite_arg' got status valid.
[eva:alarm] tests/float/builtins.c:95: Warning:
- function exp: precondition 'finite_domain' got status unknown.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status unknown.
+[eva] tests/float/builtins.c:95:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+[eva] tests/float/builtins.c:95:
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/builtins.c:98: Call to builtin exp
-[eva] tests/float/builtins.c:98:
- function exp: precondition 'finite_arg' got status valid.
[eva:alarm] tests/float/builtins.c:98: Warning:
- function exp: precondition 'finite_domain' got status invalid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status invalid.
+[eva] tests/float/builtins.c:98:
+ function exp: no state left, precondition ¬(plus_infinity_arg:
+ \is_plus_infinity(x)) got status valid.
+[eva] tests/float/builtins.c:98:
+ function exp: no state left, precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/builtins.c:102: Call to builtin log
[eva] tests/float/builtins.c:102:
function log: precondition 'finite_arg' got status valid.
@@ -131,9 +147,12 @@
[eva] tests/float/builtins.c:103: assertion got status valid.
[eva] tests/float/builtins.c:104: Call to builtin exp
[eva] tests/float/builtins.c:104:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+[eva] tests/float/builtins.c:104:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/builtins.c:104:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva:alarm] tests/float/builtins.c:107: Warning:
pointer downcast. assert (unsigned int)(&d) ≤ 2147483647;
[eva:alarm] tests/float/builtins.c:107: Warning:
@@ -155,6 +174,7 @@
assertion 'Eva,initialization' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main_log_exp:
+ __fc_errno ∈ [--..--]
l1 ∈ {0} or UNINITIALIZED
l2 ∈ {1.00063188031} or UNINITIALIZED
l3 ∈ {1.09861228867} or UNINITIALIZED
diff --git a/tests/float/oracle/math_builtins.res.oracle b/tests/float/oracle/math_builtins.res.oracle
index 6d134f9df1d..8d5f7927ba8 100644
--- a/tests/float/oracle/math_builtins.res.oracle
+++ b/tests/float/oracle/math_builtins.res.oracle
@@ -1213,39 +1213,58 @@
[eva] tests/float/math_builtins.c:516:
Call to builtin Frama_C_exp for function exp
[eva] tests/float/math_builtins.c:516:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
[eva] tests/float/math_builtins.c:516:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+[eva] tests/float/math_builtins.c:516:
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:517:
Call to builtin Frama_C_exp for function exp
[eva] tests/float/math_builtins.c:517:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+[eva] tests/float/math_builtins.c:517:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/math_builtins.c:517:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:518:
Call to builtin Frama_C_exp for function exp
[eva] tests/float/math_builtins.c:518:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
[eva] tests/float/math_builtins.c:518:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+[eva] tests/float/math_builtins.c:518:
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:519:
Call to builtin Frama_C_exp for function exp
[eva] tests/float/math_builtins.c:519:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+[eva] tests/float/math_builtins.c:519:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/math_builtins.c:519:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:520:
Call to builtin Frama_C_exp for function exp
[eva] tests/float/math_builtins.c:520:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
[eva] tests/float/math_builtins.c:520:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+[eva] tests/float/math_builtins.c:520:
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:521:
Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:521:
- function exp: precondition 'finite_arg' got status valid.
[eva:alarm] tests/float/math_builtins.c:521: Warning:
- function exp: precondition 'finite_domain' got status invalid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status invalid.
+[eva] tests/float/math_builtins.c:521:
+ function exp: no state left, precondition ¬(plus_infinity_arg:
+ \is_plus_infinity(x)) got status valid.
+[eva] tests/float/math_builtins.c:521:
+ function exp: no state left, precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] Recording results for test_exp_det
[eva] Done for function test_exp_det
[eva] computing for function test_log_det <- main.
@@ -1782,33 +1801,48 @@
[eva] tests/float/math_builtins.c:525:
Call to builtin Frama_C_expf for function expf
[eva] tests/float/math_builtins.c:525:
- function expf: precondition 'finite_arg' got status valid.
+ function expf: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
[eva] tests/float/math_builtins.c:525:
- function expf: precondition 'res_finite' got status valid.
+ function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+[eva] tests/float/math_builtins.c:525:
+ function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:526:
Call to builtin Frama_C_expf for function expf
[eva] tests/float/math_builtins.c:526:
- function expf: precondition 'finite_arg' got status valid.
+ function expf: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
+[eva] tests/float/math_builtins.c:526:
+ function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/math_builtins.c:526:
- function expf: precondition 'res_finite' got status valid.
+ function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:527:
Call to builtin Frama_C_expf for function expf
[eva] tests/float/math_builtins.c:527:
- function expf: precondition 'finite_arg' got status valid.
+ function expf: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
[eva] tests/float/math_builtins.c:527:
- function expf: precondition 'res_finite' got status valid.
+ function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+[eva] tests/float/math_builtins.c:527:
+ function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:528:
Call to builtin Frama_C_expf for function expf
[eva] tests/float/math_builtins.c:528:
- function expf: precondition 'finite_arg' got status valid.
+ function expf: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
+[eva] tests/float/math_builtins.c:528:
+ function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/math_builtins.c:528:
- function expf: precondition 'res_finite' got status valid.
+ function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:529:
Call to builtin Frama_C_expf for function expf
[eva] tests/float/math_builtins.c:529:
- function expf: precondition 'finite_arg' got status valid.
+ function expf: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
[eva] tests/float/math_builtins.c:529:
- function expf: precondition 'res_finite' got status valid.
+ function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+[eva] tests/float/math_builtins.c:529:
+ function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] Recording results for test_expf_det
[eva] Done for function test_expf_det
[eva] computing for function test_logf_det <- main.
@@ -2455,12 +2489,14 @@
d ∈ {1.3824840787361052*2^-96}
f32__f ∈ {1.382483*2^-96}
[eva:final-states] Values at end of function test_exp_det:
+ __fc_errno ∈ [--..--]
a ∈ {1.7094457008275896*2^60}
b ∈ {1.0826822658929016*2^-3}
c ∈ {1.0000000000000000}
d ∈ {1.0000000000000000}
e ∈ {1.4715177646857693*2^-2}
[eva:final-states] Values at end of function test_expf_det:
+ __fc_errno ∈ [--..--]
f32__a ∈ {1.709445*2^60}
f32__b ∈ {1.082682*2^-3}
f32__c ∈ {1.000000}
@@ -2706,6 +2742,7 @@
f32__e ∈ {-0.000000}
f32__f ∈ {-1.000000}
[eva:final-states] Values at end of function main:
+ __fc_errno ∈ [--..--]
__retres ∈ {0}
[from] Computing for function double_interval
[from] Done for function double_interval
@@ -2876,8 +2913,10 @@
[from] Function double_interval:
\result FROM min; max; nondet
[from] Function exp:
+ __fc_errno FROM x
\result FROM x
[from] Function expf:
+ __fc_errno FROM x
\result FROM x
[from] Function floor:
\result FROM x
@@ -2930,9 +2969,9 @@
[from] Function test_diff_pow_powf:
NO EFFECTS
[from] Function test_exp_det:
- NO EFFECTS
+ __fc_errno FROM \nothing
[from] Function test_expf_det:
- NO EFFECTS
+ __fc_errno FROM \nothing
[from] Function test_floor:
NO EFFECTS
[from] Function test_floor_det:
@@ -2996,6 +3035,7 @@
[from] Function test_truncf_det:
NO EFFECTS
[from] Function main:
+ __fc_errno FROM \nothing
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function double_interval:
@@ -3050,11 +3090,11 @@
[inout] Inputs for function test_diff_pow_powf:
\nothing
[inout] Out (internal) for function test_exp_det:
- a; b; c; d; e
+ __fc_errno; a; b; c; d; e
[inout] Inputs for function test_exp_det:
nondet
[inout] Out (internal) for function test_expf_det:
- f32__a; f32__b; f32__c; f32__d; f32__e
+ __fc_errno; f32__a; f32__b; f32__c; f32__d; f32__e
[inout] Inputs for function test_expf_det:
\nothing
[inout] Out (internal) for function test_floor:
@@ -3180,10 +3220,11 @@
[inout] Inputs for function test_truncf_det:
\nothing
[inout] Out (internal) for function main:
- __retres
+ __fc_errno; __retres
[inout] Inputs for function main:
nondet; any_double; any_float
/* Generated by Frama-C */
+#include "errno.h"
#include "math.h"
static int volatile nondet;
static double volatile any_double;
diff --git a/tests/float/oracle/sqrt.0.res.oracle b/tests/float/oracle/sqrt.0.res.oracle
index fecf923ed14..ae53efbab13 100644
--- a/tests/float/oracle/sqrt.0.res.oracle
+++ b/tests/float/oracle/sqrt.0.res.oracle
@@ -14,6 +14,7 @@
[eva] tests/float/sqrt.c:19:
Frama_C_dump_each:
# Cvalue domain:
+ __fc_errno ∈ [--..--]
k ∈ UNINITIALIZED
i ∈ {-0.}
j ∈ {-0.}
@@ -24,6 +25,7 @@
[eva] tests/float/sqrt.c:23:
Frama_C_dump_each:
# Cvalue domain:
+ __fc_errno ∈ [--..--]
k ∈ UNINITIALIZED
i ∈ {-0.}
j ∈ {-0.}
diff --git a/tests/float/oracle/sqrt.1.res.oracle b/tests/float/oracle/sqrt.1.res.oracle
index 6478e72b4c4..75d3c6a1725 100644
--- a/tests/float/oracle/sqrt.1.res.oracle
+++ b/tests/float/oracle/sqrt.1.res.oracle
@@ -14,6 +14,7 @@
[eva] tests/float/sqrt.c:19:
Frama_C_dump_each:
# Cvalue domain:
+ __fc_errno ∈ [--..--]
k ∈ UNINITIALIZED
i ∈ {-0.}
j ∈ {-0.}
@@ -24,6 +25,7 @@
[eva] tests/float/sqrt.c:23:
Frama_C_dump_each:
# Cvalue domain:
+ __fc_errno ∈ [--..--]
k ∈ UNINITIALIZED
i ∈ {-0.}
j ∈ {-0.}
--
GitLab