From a5caf8c1e292ad92a3a040c8cc55ba1a1e5dd80b Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Wed, 29 May 2024 17:13:20 +0200
Subject: [PATCH] [e-acsl] fix typing problem when using rationals
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
The occurrence of rationals in the following logic function lead to an
assertion failure in Interval_utils.extract_ival, which was only defined
for non-integer arguments.
/*@
logic integer signum(â„ x) =
x > 0. ? 1 : x < 0. ? -1 : 0;
*/
Regression test added: src/plugins/e-acsl/tests/arith/sign_rational.c
---
src/plugins/e-acsl/src/analyses/interval.ml | 41 +++--
src/plugins/e-acsl/src/analyses/interval.mli | 2 +-
.../e-acsl/src/code_generator/quantif.ml | 26 +--
.../src/code_generator/translate_ats.ml | 7 +-
.../e-acsl/src/libraries/interval_utils.ml | 4 +-
.../e-acsl/src/libraries/interval_utils.mli | 4 +-
.../tests/arith/oracle/gen_sign_rational.c | 149 ++++++++++++++++++
.../arith/oracle/sign_rational.res.oracle | 4 +
.../e-acsl/tests/arith/sign_rational.c | 15 ++
9 files changed, 215 insertions(+), 37 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/arith/oracle/gen_sign_rational.c
create mode 100644 src/plugins/e-acsl/tests/arith/oracle/sign_rational.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/sign_rational.c
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index d43be59cca8..ed2bd6ff624 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -658,11 +658,11 @@ and compute_logic_env_if_branches logic_env t =
let get_res = Error.map (fun x -> x) in
let ival v = infer ~force:false ~logic_env v in
let add_ub logic_env x v =
- let max = Ival.max_int (Error.map extract_ival (ival v)) in
+ let max = Option.bind (Error.map extract_ival @@ ival v) Ival.max_int in
Logic_env.refine logic_env x (Ival (Ival.inject_range None max))
in
let add_lb logic_env x v =
- let min = Ival.min_int (Error.map extract_ival (ival v)) in
+ let min = Option.bind (Error.map extract_ival @@ ival v) Ival.min_int in
Logic_env.refine logic_env x (Ival (Ival.inject_range min None))
in
let add_eq logic_env x v = Logic_env.refine logic_env x (get_res (ival v)) in
@@ -748,22 +748,29 @@ and infer_bound_variable ~loc ~logic_env (t1, lv, t2) =
let i = meet i ity in
(* We can now update the bounds in the preprocessed form
that come from the meet of the two intervals *)
- let min, max = Misc.finite_min_and_max (extract_ival i) in
- let t1 = Logic_const.tint ~loc min in
- let t2 = Logic_const.tint ~loc max in
- t1, t2, i
- end else
+ match extract_ival i with
+ | None -> t1, t2, i
+ | Some ival ->
+ let min, max = Misc.finite_min_and_max ival in
+ let t1 = Logic_const.tint ~loc min in
+ let t2 = Logic_const.tint ~loc max in
+ t1, t2, i
+ end
+ else
(* case 3 *)
- let min, max = Misc.finite_min_and_max (extract_ival ity) in
- let guard_lower = Logic_const.tint ~loc min in
- let guard_upper = Logic_const.tint ~loc max in
- let lv_term = Logic_const.tvar ~loc lv in
- let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
- let guard_upper = Logic_const.prel ~loc (Rlt, lv_term, guard_upper) in
- let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
- ignore (infer_predicate ~logic_env guard);
- Bound_variables.add_guard_for_small_type lv guard;
- t1, t2, i
+ match extract_ival ity with
+ | None -> t1, t2, i
+ | Some ival ->
+ let min, max = Misc.finite_min_and_max ival in
+ let guard_lower = Logic_const.tint ~loc min in
+ let guard_upper = Logic_const.tint ~loc max in
+ let lv_term = Logic_const.tvar ~loc lv in
+ let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
+ let guard_upper = Logic_const.prel ~loc (Rlt, lv_term, guard_upper) in
+ let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
+ ignore (infer_predicate ~logic_env guard);
+ Bound_variables.add_guard_for_small_type lv guard;
+ t1, t2, i
in
ignore (infer ~force:false ~logic_env t1);
ignore (infer ~force:false ~logic_env t2);
diff --git a/src/plugins/e-acsl/src/analyses/interval.mli b/src/plugins/e-acsl/src/analyses/interval.mli
index 1cbc7492730..aeb9bd4f89e 100644
--- a/src/plugins/e-acsl/src/analyses/interval.mli
+++ b/src/plugins/e-acsl/src/analyses/interval.mli
@@ -81,7 +81,7 @@ val joins_from_profile: profile:Profile.t -> term list -> t
val joins: logic_env:Logic_env.t -> term list -> t
val join_plus_one: profile:Profile.t -> term -> term -> t
-val get_ival: logic_env:Logic_env.t -> term -> Ival.t
+val get_ival: logic_env:Logic_env.t -> term -> Ival.t option
(*****************************************************************************)
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index a851389f548..2c8346eb5d1 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -48,17 +48,21 @@ let rec has_empty_quantif_with_false_negative ~logic_env = function
(* case 2 *)
false
| (t1, _, t2) :: guards ->
- let lower_bound, _ = Ival.min_and_max (Interval.get_ival ~logic_env t1) in
- let _, upper_bound = Ival.min_and_max (Interval.get_ival ~logic_env t2) in
- begin
- match lower_bound, upper_bound with
- | Some lower_bound, Some upper_bound ->
- let res = lower_bound >= upper_bound in
- res (* case 1 *) ||
- has_empty_quantif_with_false_negative guards ~logic_env
- | None, _ | _, None ->
- has_empty_quantif_with_false_negative guards ~logic_env
- end
+ let bounds =
+ let open Option.Operators in
+ let* ival1 = Interval.get_ival ~logic_env t1 in
+ let* ival2 = Interval.get_ival ~logic_env t2 in
+ let* lower_bound = fst @@ Ival.min_and_max ival1 in
+ let* upper_bound = snd @@ Ival.min_and_max ival2 in
+ Some (lower_bound, upper_bound)
+ in
+ match bounds with
+ | Some (lower_bound, upper_bound) ->
+ let res = lower_bound >= upper_bound in
+ res (* case 1 *) ||
+ has_empty_quantif_with_false_negative guards ~logic_env
+ | None ->
+ has_empty_quantif_with_false_negative guards ~logic_env
let () =
Labels.has_empty_quantif_ref :=
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index 961e4a5bae7..8575b160506 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -136,10 +136,9 @@ let rec sizes_and_shifts_from_quantifs ~loc ~logic_env kf lscope sizes_and_shift
beneficial. In particular, though we may allocate more memory than
needed, the number of reads/writes into it is the same in both cases.
Conclusion: over-approximate [t_size] *)
- let t_size = match Ival.min_and_max iv with
- | _, Some max ->
- Logic_const.tint ~loc max
- | _, None ->
+ let t_size = match Option.map Ival.min_and_max iv with
+ | Some (_, Some max) -> Logic_const.tint ~loc max
+ | _ ->
Error.not_yet
"\\at on purely logic variables and with quantifier that uses \
too complex bound (E-ACSL cannot infer a finite upper bound to it)"
diff --git a/src/plugins/e-acsl/src/libraries/interval_utils.ml b/src/plugins/e-acsl/src/libraries/interval_utils.ml
index 41c50a29fcb..2b3a66396cf 100644
--- a/src/plugins/e-acsl/src/libraries/interval_utils.ml
+++ b/src/plugins/e-acsl/src/libraries/interval_utils.ml
@@ -218,8 +218,8 @@ let is_singleton_int = function
(* ********************************************************************* *)
let extract_ival = function
- | Ival iv -> iv
- | Float _ | Rational | Real | Nan -> assert false
+ | Ival iv -> Some iv
+ | _ -> None
let bottom = Ival Ival.bottom
let top_ival = Ival (Ival.inject_range None None)
diff --git a/src/plugins/e-acsl/src/libraries/interval_utils.mli b/src/plugins/e-acsl/src/libraries/interval_utils.mli
index 90c57989716..042d4e16871 100644
--- a/src/plugins/e-acsl/src/libraries/interval_utils.mli
+++ b/src/plugins/e-acsl/src/libraries/interval_utils.mli
@@ -47,8 +47,8 @@ val lift_unop : (Ival.t -> Ival.t) -> ival -> ival
val lift_arith_binop : (Ival.t -> Ival.t -> Ival.t) -> ival -> ival -> ival
(** Lift a binary operation on [IVal.t] to the type [ival] *)
-(** assume [Ival _] as argument *)
-val extract_ival : ival -> Ival.t
+(** @return [Some ival] if argument is [Ival ival] *)
+val extract_ival : ival -> Ival.t option
val ival_of_ikind: ikind -> Ival.t
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_sign_rational.c b/src/plugins/e-acsl/tests/arith/oracle/gen_sign_rational.c
new file mode 100644
index 00000000000..1fa5198a816
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_sign_rational.c
@@ -0,0 +1,149 @@
+/* Generated by Frama-C */
+#include "pthread.h"
+#include "sched.h"
+#include "signal.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "time.h"
+extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+/*@ logic integer signum(real x) = x > 0.? 1: (x < 0.? -1: 0);
+
+*/
+int __gen_e_acsl_signum_5(double x);
+
+int __gen_e_acsl_signum(double x);
+
+int __gen_e_acsl_signum_3(__e_acsl_mpq_t x);
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ {
+ int __gen_e_acsl_signum_2;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __gen_e_acsl_signum_2 = __gen_e_acsl_signum(3.);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"signum(3.0)",0,
+ __gen_e_acsl_signum_2);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Assertion";
+ __gen_e_acsl_assert_data.pred_txt = "signum(3.0) > 0";
+ __gen_e_acsl_assert_data.file = "sign_rational.c";
+ __gen_e_acsl_assert_data.fct = "main";
+ __gen_e_acsl_assert_data.line = 11;
+ __e_acsl_assert(__gen_e_acsl_signum_2 > 0,& __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ }
+ /*@ assert signum(3.0) > 0; */ ;
+ {
+ __e_acsl_mpq_t __gen_e_acsl_;
+ __e_acsl_mpq_t __gen_e_acsl__2;
+ __e_acsl_mpq_t __gen_e_acsl_sub;
+ int __gen_e_acsl_signum_4;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
+ {.values = (void *)0};
+ __gmpq_init(__gen_e_acsl_);
+ __gmpq_set_d(__gen_e_acsl_,0.);
+ __gmpq_init(__gen_e_acsl__2);
+ __gmpq_set_d(__gen_e_acsl__2,3.);
+ __gmpq_init(__gen_e_acsl_sub);
+ __gmpq_sub(__gen_e_acsl_sub,(__e_acsl_mpq_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__2));
+ __gen_e_acsl_signum_4 = __gen_e_acsl_signum_3(__gen_e_acsl_sub);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+ "signum(0.0 - 3.0)",0,__gen_e_acsl_signum_4);
+ __gen_e_acsl_assert_data_2.blocking = 1;
+ __gen_e_acsl_assert_data_2.kind = "Assertion";
+ __gen_e_acsl_assert_data_2.pred_txt = "signum(0.0 - 3.0) < 0";
+ __gen_e_acsl_assert_data_2.file = "sign_rational.c";
+ __gen_e_acsl_assert_data_2.fct = "main";
+ __gen_e_acsl_assert_data_2.line = 12;
+ __e_acsl_assert(__gen_e_acsl_signum_4 < 0,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
+ __gmpq_clear(__gen_e_acsl_);
+ __gmpq_clear(__gen_e_acsl__2);
+ __gmpq_clear(__gen_e_acsl_sub);
+ }
+ /*@ assert signum(0.0 - 3.0) < 0; */ ;
+ {
+ int __gen_e_acsl_signum_6;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
+ {.values = (void *)0};
+ __gen_e_acsl_signum_6 = __gen_e_acsl_signum_5(0.);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"signum(0.0)",
+ 0,__gen_e_acsl_signum_6);
+ __gen_e_acsl_assert_data_3.blocking = 1;
+ __gen_e_acsl_assert_data_3.kind = "Assertion";
+ __gen_e_acsl_assert_data_3.pred_txt = "signum(0.0) == 0";
+ __gen_e_acsl_assert_data_3.file = "sign_rational.c";
+ __gen_e_acsl_assert_data_3.fct = "main";
+ __gen_e_acsl_assert_data_3.line = 13;
+ __e_acsl_assert(__gen_e_acsl_signum_6 == 0,& __gen_e_acsl_assert_data_3);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
+ }
+ /*@ assert signum(0.0) == 0; */ ;
+ __retres = 0;
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+/*@ assigns \result;
+ assigns \result \from x; */
+int __gen_e_acsl_signum_5(double x)
+{
+ int __gen_e_acsl_if_6;
+ if (x > 0.) __gen_e_acsl_if_6 = 1;
+ else {
+ int __gen_e_acsl_if_5;
+ if (x < 0.) __gen_e_acsl_if_5 = -1; else __gen_e_acsl_if_5 = 0;
+ __gen_e_acsl_if_6 = __gen_e_acsl_if_5;
+ }
+ return __gen_e_acsl_if_6;
+}
+
+/*@ assigns \result;
+ assigns \result \from x; */
+int __gen_e_acsl_signum(double x)
+{
+ int __gen_e_acsl_if_2;
+ if (x > 0.) __gen_e_acsl_if_2 = 1;
+ else {
+ int __gen_e_acsl_if;
+ if (x < 0.) __gen_e_acsl_if = -1; else __gen_e_acsl_if = 0;
+ __gen_e_acsl_if_2 = __gen_e_acsl_if;
+ }
+ return __gen_e_acsl_if_2;
+}
+
+/*@ assigns \result;
+ assigns \result \from *((__e_acsl_mpq_struct *)x); */
+int __gen_e_acsl_signum_3(__e_acsl_mpq_t x)
+{
+ __e_acsl_mpq_t __gen_e_acsl__3;
+ int __gen_e_acsl_gt;
+ int __gen_e_acsl_if_4;
+ __gmpq_init(__gen_e_acsl__3);
+ __gmpq_set_d(__gen_e_acsl__3,0.);
+ __gen_e_acsl_gt = __gmpq_cmp((__e_acsl_mpq_struct const *)(x),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__3));
+ if (__gen_e_acsl_gt > 0) __gen_e_acsl_if_4 = 1;
+ else {
+ __e_acsl_mpq_t __gen_e_acsl__4;
+ int __gen_e_acsl_lt;
+ int __gen_e_acsl_if_3;
+ __gmpq_init(__gen_e_acsl__4);
+ __gmpq_set_d(__gen_e_acsl__4,0.);
+ __gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(x),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__4));
+ if (__gen_e_acsl_lt < 0) __gen_e_acsl_if_3 = -1;
+ else __gen_e_acsl_if_3 = 0;
+ __gen_e_acsl_if_4 = __gen_e_acsl_if_3;
+ __gmpq_clear(__gen_e_acsl__4);
+ }
+ __gmpq_clear(__gen_e_acsl__3);
+ return __gen_e_acsl_if_4;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/arith/oracle/sign_rational.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/sign_rational.res.oracle
new file mode 100644
index 00000000000..1d33ef8c2a9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle/sign_rational.res.oracle
@@ -0,0 +1,4 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] sign_rational.c:12: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/sign_rational.c b/src/plugins/e-acsl/tests/arith/sign_rational.c
new file mode 100644
index 00000000000..34a823fb832
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/sign_rational.c
@@ -0,0 +1,15 @@
+/* run.config
+ COMMENT: a logic function defined over rationals
+*/
+
+/*@
+ logic integer signum(â„ x) =
+ x > 0. ? 1 : x < 0. ? -1 : 0;
+*/
+
+int main() {
+ /*@ assert signum(3.0) > 0; */
+ /*@ assert signum(0.0-3.0) < 0; */
+ /*@ assert signum(0.0) ≡ 0; */
+ return 0;
+}
--
GitLab