Support INFINITY and NAN

  Add \plus_infinity, \minus_infinity, \NaN
  Support in EVA

share/libc/math.h

@@ -37,10 +37,6 @@ typedef double double_t;
 #define MATH_ERRNO	1
 #define MATH_ERREXCEPT	2
 
-#define HUGE_VAL  0x1.0p2047
-#define HUGE_VALF 0x1.0p255f
-#define HUGE_VALL 0x1.0p32767L
-
 /* The constants below are not part of C99/C11 but they are defined in POSIX */
 #define M_E 0x1.5bf0a8b145769p1         /* e          */
 #define M_LOG2E 0x1.71547652b82fep0     /* log_2 e    */
@@ -755,6 +751,37 @@ extern int __finite(double d);
 #  define isfinite(x) \
      (sizeof (x) == sizeof (float) ? __finitef (x) : __finite (x))
 
+//The (integer x) argument is just here because a function without argument is
+//applied differently in ACSL and C
+
+/*@
+
+  logic float __fc_infinity(integer x) = \plus_infinity;
+  logic float __fc_nan(integer x) = \NaN;
+
+  @*/
+
+/*@
+  ensures \eq_float(\result,\plus_infinity);
+  assigns \result \from \nothing;
+  @*/
+extern const float __fc_infinity(int x);
+
+/*@
+  ensures \is_NaN(\result);
+  assigns \result \from \nothing;
+  @*/
+extern const float __fc_nan();
+
+
+#define INFINITY __fc_infinity(0)
+#define NAN __fc_nan(0)
+
+#define HUGE_VALF INFINITY
+#define HUGE_VAL  ((double)INFINITY)
+#define HUGE_VALL ((long double)INFINITY)
+
+
 __END_DECLS
 
 __POP_FC_STDLIB

src/kernel_internals/typing/logic_builtin.ml

@@ -285,6 +285,9 @@ let init =
                ["m",  rounding_mode; "x", Lreal], float_type;
             "\\round_double", [], 
                ["m", rounding_mode ; "x", Lreal], double_type;
+            "\\plus_infinity", [], [], float_type;
+            "\\minus_infinity", [], [], float_type;
+            "\\NaN", [], [], float_type;
             (*"\\round_quad", [], 
                ["m",  rounding_mode; "x", Lreal], long_double_type;*)
 

src/kernel_services/abstract_interp/float_interval.ml

@@ -223,7 +223,7 @@ module Make (F: Float_sig.S) = struct
   let pos_zero prec = singleton (Cst.pos_zero prec)
   let one prec = singleton (F.of_float Near prec 1.)
   let pos_infinity prec = singleton (Cst.pos_infinity prec)
-  let _neg_infinity prec = singleton (Cst.neg_infinity prec)
+  let neg_infinity prec = singleton (Cst.neg_infinity prec)
 
   let minus_one_one prec ~nan =
     FRange.inject ~nan (F.of_float Near prec (-1.)) (F.of_float Near prec 1.)
@@ -420,6 +420,20 @@ 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_pos_infinity = function
+    | FRange.NaN -> Comp.False
+    | FRange.Itv (b, e, _) ->
+      if not (Cmp.is_pos_infinity e) then Comp.False
+      else if not (Cmp.is_pos_infinity b) then Comp.Unknown
+      else Comp.True
+
+  let is_neg_infinity = function
+    | FRange.NaN -> Comp.False
+    | FRange.Itv (b, e, _) ->
+      if not (Cmp.is_neg_infinity b) then Comp.False
+      else if not (Cmp.is_neg_infinity e) then Comp.Unknown
+      else Comp.True
+
   let is_finite = function
     | FRange.NaN -> Comp.False
     | FRange.Itv (b, e, nan) ->
@@ -441,6 +455,11 @@ module Make (F: Float_sig.S) = struct
     | FRange.NaN -> `Bottom
     | FRange.Itv (b, e, _) -> `Value (FRange.inject ~nan:false b e)
 
+  let backward_is_nan = function
+    | FRange.Itv (_, _, false) -> `Bottom
+    | FRange.Itv (_, _, true)
+    | FRange.NaN -> `Value nan
+
   let backward_is_finite prec = function
     | FRange.NaN -> `Bottom
     | FRange.Itv (b, e, _) as f ->

src/kernel_services/abstract_interp/float_interval_sig.mli

@@ -47,6 +47,10 @@ module type S = sig
   (** The NaN singleton *)
   val nan: t
 
+  (** The infinities singleton *)
+  val pos_infinity: prec -> t
+  val neg_infinity: prec -> t
+
   (** [inject ~nan b e] creates the floating-point interval [b..e], plus NaN
       if [nan] is true. [b] and [e] must be ordered, and not NaN. They can be
       infinite. *)
@@ -87,8 +91,11 @@ module type S = sig
 
   val is_finite: t -> Abstract_interp.Comp.result
   val is_not_nan: t -> Abstract_interp.Comp.result
+  val is_pos_infinity: t -> Abstract_interp.Comp.result
+  val is_neg_infinity: t -> Abstract_interp.Comp.result
   val backward_is_finite: prec -> t -> t or_bottom
   val backward_is_not_nan: t -> t or_bottom
+  val backward_is_nan: t -> t or_bottom
 
   (** [has_greater_min_bound f1 f2] returns 1 if the interval [f1] has a better
       minimum bound (i.e. greater) than the interval [f2]. *)

src/plugins/value/legacy/eval_terms.ml

@@ -633,6 +633,9 @@ let known_logic_funs = [
   "\\sign", ACSL;
   "\\min", ACSL;
   "\\max", ACSL;
+  "\\plus_infinity", ACSL;
+  "\\minus_infinity", ACSL;
+  "\\NaN", ACSL;
 ]
 let known_predicates = [
   "\\warning", ACSL;
@@ -745,6 +748,16 @@ let rec eval_term ~alarm_mode env t =
   (* Special case for the constants \pi and \e. *)
   | TLval (TVar {lv_name = "\\pi"}, _) -> ereal (V.inject_float Fval.pi)
   | TLval (TVar {lv_name = "\\e"}, _)  -> ereal (V.inject_float Fval.e)
+  | TLval (TVar {lv_name = "\\plus_infinity"}, _) ->
+    let v = Cvalue.V.inject_float (Fval.pos_infinity Float_sig.Single) in
+    { etype = Cil.floatType; eunder = v; eover = v; ldeps = empty_logic_deps }
+  | TLval (TVar {lv_name = "\\minus_infinity"}, _) ->
+    let v = Cvalue.V.inject_float (Fval.neg_infinity Float_sig.Single) in
+    { etype = Cil.floatType; eunder = v; eover = v; ldeps = empty_logic_deps }
+  | TLval (TVar {lv_name = "\\NaN"}, _) ->
+    let v = Cvalue.V.inject_float Fval.nan in
+    { etype = Cil.floatType; eunder = v; eover = v; ldeps = empty_logic_deps }
+
   | TLval _ ->
     let lval = eval_tlval ~alarm_mode env t in
     let typ = lval.etype in
@@ -1220,6 +1233,7 @@ and eval_tif : 'a. (alarm_mode:_ -> _ -> _ -> 'a eval_result) -> ('a -> 'a -> 'a
     | false, false -> assert false (* a logic alarm would have been raised*)
 
 (* if you add something here, update known_logic_funs above also *)
+(* Constants are directly in eval_terms *)
 and eval_known_logic_function ~alarm_mode env li labels args =
   let lvi = li.l_var_info in
   match lvi.lv_name, li.l_type, labels, args with
@@ -1271,7 +1285,6 @@ and eval_known_logic_function ~alarm_mode env li labels args =
   | "\\max", Some Lreal, _, [t1; t2] ->
     let backward = Cvalue.V.backward_comp_float_left_true Comp.Ge Fval.Real in
     eval_extremum Cil.doubleType backward ~alarm_mode env t1 t2
-
   | _ -> assert false
 
 and eval_float_builtin_arity2  ~alarm_mode env name arg1 arg2 =
@@ -1694,6 +1707,7 @@ let reduce_by_left_relation ~alarm_mode env positive tl rel tr =
     let debug = false in
     if debug then Format.printf "#Left term %a@." Printer.pp_term tl;
     let typ_loc, locs = eval_term_as_exact_locs ~alarm_mode env tl in
+    if debug then Format.printf "HERE@.";
     let reduce = Eval_op.backward_comp_left_from_type typ_loc in
     let rtl = eval_term ~alarm_mode env tr in
     let cond_v = rtl.eover in
@@ -1747,40 +1761,40 @@ let rec reduce_by_relation ~alarm_mode env positive t1 rel t2 =
    May raise LogicEvalError or Not_an_exact_loc, when no reduction can be done,
    and Reduce_to_bottom, in which case the reduction leads to bottom. *)
 let reduce_by_known_papp ~alarm_mode env positive li _labels args =
-  match positive, li.l_var_info.lv_name, args with
-  | true, "\\is_finite", [arg]
-  | false, "\\is_NaN", [arg] -> begin
-      let fval_reduce =
-        (* positive is true for is_finite, false for is_NaN. *)
-        if positive
-        then Fval.backward_is_finite
-        else (fun _fkind -> Fval.backward_is_not_nan)
-      in
-      try
-        let alarm_mode = alarm_reduce_mode () in
-        let typ_loc, locs = eval_term_as_exact_locs ~alarm_mode env arg in
-        let aux loc env =
-          let state = env_current_state env in
-          let v = find_or_alarm ~alarm_mode state loc in
-          let v =  Cvalue_forward.reinterpret typ_loc v in
-          let v = match Cil.unrollType typ_loc with
-            | TFloat (fkind,_) -> begin
-                let v = Cvalue.V.project_float v in
-                let kind = Fval.kind fkind in
-                match fval_reduce kind v with
-                | `Value f -> V.inject_float f
-                | `Bottom -> V.bottom
-              end
-            | _ -> (* Better safe than sorry, we may have e.g. en int location
-                      here *)
-              raise Not_an_exact_loc
-          in
-          let state' = Cvalue.Model.reduce_previous_binding state loc v in
-          overwrite_current_state env state'
+  let reduce_float fval_reduce arg =
+    try
+      let alarm_mode = alarm_reduce_mode () in
+      let typ_loc, locs = eval_term_as_exact_locs ~alarm_mode env arg in
+      let aux loc env =
+        let state = env_current_state env in
+        let v = find_or_alarm ~alarm_mode state loc in
+        let v =  Cvalue_forward.reinterpret typ_loc v in
+        let v = match Cil.unrollType typ_loc with
+          | TFloat (fkind,_) -> begin
+              let v = Cvalue.V.project_float v in
+              let kind = Fval.kind fkind in
+              match fval_reduce kind v with
+              | `Value f -> V.inject_float f
+              | `Bottom -> V.bottom
+            end
+          | _ -> (* Better safe than sorry, we may have e.g. en int location
+                    here *)
+            raise Not_an_exact_loc
         in
-        Eval_op.apply_on_all_locs aux locs env
-      with Cvalue.V.Not_based_on_null -> env
-    end
+        let state' = Cvalue.Model.reduce_previous_binding state loc v in
+        overwrite_current_state env state'
+      in
+      Eval_op.apply_on_all_locs aux locs env
+    with LogicEvalError _ | Not_an_exact_loc | Cvalue.V.Not_based_on_null ->
+      env
+  in
+  match positive, li.l_var_info.lv_name, args with
+  | true, "\\is_finite", [arg] ->
+    reduce_float Fval.backward_is_finite arg
+  | false, "\\is_NaN", [arg] ->
+    reduce_float (fun _fkind -> Fval.backward_is_not_nan) arg
+  | true, "\\is_NaN", [arg] ->
+    reduce_float (fun _fkind -> Fval.backward_is_nan) arg
   | _ , ("\\eq_float" | "\\eq_double"), [t1;t2] ->
     reduce_by_relation ~alarm_mode env positive t1 Req t2
   | _ , ("\\ne_float" | "\\ne_double"), [t1;t2] ->
@@ -2289,6 +2303,8 @@ and eval_predicate env pred =
           Value_parameters.abort
             "Wrong argument: \\warning expects a constant string"
       end
+    | "\\is_plus_infinity", [arg] -> unary_float Fval.is_pos_infinity arg
+    | "\\is_minus_infinity", [arg] -> unary_float Fval.is_neg_infinity arg
     | "\\subset", [argl;argr] -> begin
         try
           let l = eval_term ~alarm_mode env argl in

tests/value/INFINITY_NAN.c

+/* run.config*
+  STDOPT: +"-warn-special-float none"
+*/
+
+#include <math.h>
+
+int main1(){
+  float infinity_f = INFINITY;
+  Frama_C_show_each(infinity_f);
+  /*@ assert \eq_float(infinity_f,INFINITY); @*/
+  double infinity_d = HUGE_VAL;
+  if(infinity_f == infinity_d) {
+    return 1;
+  } else {
+    /*@ assert \false; @*/
+    return 0;
+  }
+}
+
+
+volatile float nondet;
+
+int main2(){
+  float nan_f = nondet;
+  Frama_C_show_each(nan_f);
+  /*@ assert \is_NaN(nan_f); @*/
+  double infinity_d = HUGE_VAL;
+  if(nan_f == infinity_d) {
+    /*@ assert \false; @*/
+    return 0;
+  } else {
+    return 1;
+  }
+}
+
+
+int main(){
+  return (main1 () && main2 ());
+}

tests/value/oracle/INFINITY_NAN.res.oracle

+[eva] Warning: Unknown message key summary
+[kernel] Parsing tests/value/INFINITY_NAN.c (with preprocessing)
+[kernel] tests/value/INFINITY_NAN.c:8: Failure: Cannot resolve variable INFINITY
+[kernel] User Error: stopping on file "tests/value/INFINITY_NAN.c" that has errors. Add
+  '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.