From 9fa07ffc930cff3da321024df2508554dbe7465e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 6 Jan 2021 14:11:27 +0100
Subject: [PATCH] [wp] Fixes dispatch of sqrt in real mode
---
src/plugins/wp/Cfloat.ml | 15 +++++++----
.../wp_acsl/oracle/sqrt_builtins.0.res.oracle | 22 ++++++++++++++++
.../wp_acsl/oracle/sqrt_builtins.1.res.oracle | 22 ++++++++++++++++
.../oracle_qualif/sqrt_builtins.0.res.oracle | 14 ++++++++++
.../oracle_qualif/sqrt_builtins.1.res.oracle | 14 ++++++++++
src/plugins/wp/tests/wp_acsl/sqrt_builtins.i | 26 +++++++++++++++++++
6 files changed, 108 insertions(+), 5 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.0.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.1.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.0.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.1.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/sqrt_builtins.i
diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 04ccb8f8151..27904b61625 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -405,12 +405,17 @@ let () = Context.register
(* --- Models --- *)
(* -------------------------------------------------------------------------- *)
-let register_c_acsl_builtin name lfun ft =
+let hack_sqrt_builtin ft =
+ let choose xs =
+ match Context.get model with
+ | Real -> F.e_fun ~result:t_real Cmath.f_sqrt xs
+ | Float -> F.e_fun ~result:(ftau ft) (f_sqrt ft) xs
+ in
let name = match ft with
- | Float32 -> name ^ "f"
- | Float64 -> name
+ | Float32 -> "sqrtf"
+ | Float64 -> "sqrt"
in
- LogicBuiltins.add_builtin name [F ft] (lfun ft)
+ LogicBuiltins.hack name choose
let () =
let open LogicBuiltins in
@@ -418,7 +423,7 @@ let () =
add_builtin "\\model" [F ft] (f_model ft) ;
add_builtin "\\delta" [F ft] (f_delta ft) ;
add_builtin "\\epsilon" [F ft] (f_epsilon ft) ;
- register_c_acsl_builtin "sqrt" f_sqrt ft
+ hack_sqrt_builtin ft
in
register_builtin Float32 ;
register_builtin Float64
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.0.res.oracle
new file mode 100644
index 00000000000..546f84fc336
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.0.res.oracle
@@ -0,0 +1,22 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/sqrt_builtins.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function test_sqrt
+------------------------------------------------------------
+
+Goal Assertion 'KO' (file tests/wp_acsl/sqrt_builtins.i, line 25):
+Assume { (* Call 'sqrt' *) Have: .0 <= of_f64(sqrt_f64(q)). }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function test_sqrtf
+------------------------------------------------------------
+
+Goal Assertion 'KO' (file tests/wp_acsl/sqrt_builtins.i, line 16):
+Assume { (* Call 'sqrtf' *) Have: .0 <= of_f32(sqrt_f32(q)). }
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.1.res.oracle
new file mode 100644
index 00000000000..21bd47ad8f8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.1.res.oracle
@@ -0,0 +1,22 @@
+# frama-c -wp -wp-model 'Typed (Real)' [...]
+[kernel] Parsing tests/wp_acsl/sqrt_builtins.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function test_sqrt
+------------------------------------------------------------
+
+Goal Assertion 'KO' (file tests/wp_acsl/sqrt_builtins.i, line 25):
+Assume { (* Call 'sqrt' *) Have: .0 <= sqrt(q). }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function test_sqrtf
+------------------------------------------------------------
+
+Goal Assertion 'KO' (file tests/wp_acsl/sqrt_builtins.i, line 16):
+Assume { (* Call 'sqrtf' *) Have: .0 <= sqrt(q). }
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.0.res.oracle
new file mode 100644
index 00000000000..93fd64a1995
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.0.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/sqrt_builtins.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] [Alt-Ergo] Goal typed_test_sqrtf_assert_KO : Unsuccess
+[wp] [Alt-Ergo] Goal typed_test_sqrt_assert_KO : Unsuccess
+[wp] Proved goals: 0 / 2
+ Alt-Ergo: 0 (unsuccess: 2)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ test_sqrtf - - 1 0.0%
+ test_sqrt - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.1.res.oracle
new file mode 100644
index 00000000000..bd5e2fe0f92
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.1.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp -wp-model 'Typed (Real)' [...]
+[kernel] Parsing tests/wp_acsl/sqrt_builtins.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] [Alt-Ergo] Goal typed_real_test_sqrtf_assert_KO : Unsuccess
+[wp] [Alt-Ergo] Goal typed_real_test_sqrt_assert_KO : Unsuccess
+[wp] Proved goals: 0 / 2
+ Alt-Ergo: 0 (unsuccess: 2)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ test_sqrtf - - 1 0.0%
+ test_sqrt - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/sqrt_builtins.i b/src/plugins/wp/tests/wp_acsl/sqrt_builtins.i
new file mode 100644
index 00000000000..a19b233d84f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/sqrt_builtins.i
@@ -0,0 +1,26 @@
+/* run.config
+ OPT:
+ OPT: -wp-model real
+*/
+/* run.config_qualif
+ OPT:
+ OPT: -wp-model real
+*/
+
+/*@ assigns \nothing;
+ ensures -0. <= sqrtf(x); */
+void sqrtf(float x);
+
+void test_sqrtf(float q){
+ sqrtf(q);
+ /*@ assert KO: \false; */
+}
+
+/*@ assigns \nothing;
+ ensures -0. <= sqrt(x); */
+void sqrt(double x);
+
+void test_sqrt(double q){
+ sqrt(q);
+ /*@ assert KO: \false; */
+}
--
GitLab