From ccd32410c534b94b52ba505a70a47e75768186ee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 11 May 2021 10:37:14 +0200
Subject: [PATCH] [Eva] Adds support for ACSL predicate is_infinite.
Adds functions [is_infinite] and [backward_is_infinite] in float_interval.
---
.../abstract_interp/float_interval.ml | 20 +++++++++++++++++++
.../abstract_interp/float_interval_sig.mli | 2 ++
src/plugins/value/legacy/eval_terms.ml | 4 ++++
3 files changed, 26 insertions(+)
diff --git a/src/kernel_services/abstract_interp/float_interval.ml b/src/kernel_services/abstract_interp/float_interval.ml
index 7e733d4faa6..316b5b9b46b 100644
--- a/src/kernel_services/abstract_interp/float_interval.ml
+++ b/src/kernel_services/abstract_interp/float_interval.ml
@@ -421,6 +421,13 @@ module Make (F: Float_sig.S) = struct
| FRange.NaN -> Comp.False
| FRange.Itv (_b, _e, nan) -> if nan then Comp.Unknown else Comp.True
+ let is_infinite = function
+ | FRange.NaN -> Comp.False
+ | FRange.Itv (b, e, nan) ->
+ if F.is_infinite b || F.is_infinite e
+ then if Cmp.equal b e && not nan then Comp.True else Comp.Unknown
+ else Comp.False
+
let is_finite = function
| FRange.NaN -> Comp.False
| FRange.Itv (b, e, nan) ->
@@ -444,6 +451,19 @@ module Make (F: Float_sig.S) = struct
| FRange.Itv (b, e, true) ->
if positive then `Value nan else `Value (FRange.inject ~nan:false b e)
+ let backward_is_infinite ~positive prec = function
+ | FRange.NaN as v -> if positive then `Bottom else `Value v
+ | FRange.Itv (b, e, nan) as f ->
+ if positive
+ then
+ match F.is_infinite b, F.is_infinite e with
+ | true, true -> `Value (if nan then FRange.inject ~nan:false b e else f)
+ | true, false -> `Value (FRange.inject ~nan:false b b)
+ | false, true -> `Value (FRange.inject ~nan:false e e)
+ | false, false -> `Bottom
+ else
+ narrow (FRange.add_nan (top_finite prec)) f
+
let backward_is_finite ~positive prec = function
| FRange.NaN as v -> if positive then `Bottom else `Value v
| FRange.Itv (b, e, nan) as f ->
diff --git a/src/kernel_services/abstract_interp/float_interval_sig.mli b/src/kernel_services/abstract_interp/float_interval_sig.mli
index e105e4b09b5..1ea3e2fcfa2 100644
--- a/src/kernel_services/abstract_interp/float_interval_sig.mli
+++ b/src/kernel_services/abstract_interp/float_interval_sig.mli
@@ -90,8 +90,10 @@ module type S = sig
val is_negative: t -> Abstract_interp.Comp.result
val is_finite: t -> Abstract_interp.Comp.result
+ val is_infinite: t -> Abstract_interp.Comp.result
val is_not_nan: t -> Abstract_interp.Comp.result
val backward_is_finite: positive:bool -> prec -> t -> t or_bottom
+ val backward_is_infinite: positive:bool -> prec -> t -> t or_bottom
val backward_is_nan: positive:bool -> t -> t or_bottom
(** [has_greater_min_bound f1 f2] returns 1 if the interval [f1] has a better
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 2ae8f263be7..bc8883d793f 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -737,6 +737,7 @@ let known_logic_funs = [
let known_predicates = [
"\\warning", ACSL;
"\\is_finite", ACSL;
+ "\\is_infinite", ACSL;
"\\is_plus_infinity", ACSL;
"\\is_minus_infinity", ACSL;
"\\is_NaN", ACSL;
@@ -2036,6 +2037,8 @@ let reduce_by_known_papp ~alarm_mode env positive li _labels args =
match li.l_var_info.lv_name, args with
| "\\is_finite", [arg] ->
reduce_float (Fval.backward_is_finite ~positive) arg
+ | "\\is_infinite", [arg] ->
+ reduce_float (Fval.backward_is_infinite ~positive) arg
| "\\is_plus_infinity", [arg] ->
reduce_float (reduce_by_infinity ~pos:true) arg
| "\\is_minus_infinity", [arg] ->
@@ -2555,6 +2558,7 @@ and eval_predicate env pred =
in
match li.l_var_info.lv_name, args with
| "\\is_finite", [arg] -> unary_float Fval.is_finite arg
+ | "\\is_infinite", [arg] -> unary_float Fval.is_infinite arg
| "\\is_plus_infinity", [arg] ->
let pos_inf = Fval.pos_infinity Float_sig.Single in
unary_float (fun f -> Fval.forward_comp Comp.Eq f pos_inf) arg
--
GitLab