Float Classification Functions

src/analyses/base.ml

@@ -2398,6 +2398,31 @@ struct
         | Some x -> assign ctx x (List.hd args)
         | None -> ctx.local
       end
+    (**Floating point classification and unary trigonometric functions defined in c99*)
+    | `Unknown (("__builtin_isfinite" | "__builtin_isinf" | "__builtin_isinf_sign" | "__builtin_isnan" | "__builtin_isnormal" | "__builtin_signbit") as name) ->
+      begin match args with
+        | [x] -> 
+          let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in
+          begin match eval_x with
+            | `Float float_x -> 
+              let result = 
+                begin match name with
+                  | "__builtin_isfinite" -> `Int (ID.cast_to IInt (FD.isfinite float_x))
+                  | "__builtin_isinf" | "__builtin_isinf_sign" -> `Int (ID.cast_to IInt (FD.isinf float_x))
+                  | "__builtin_isnan" -> `Int (ID.cast_to IInt (FD.isnan float_x))
+                  | "__builtin_isnormal" -> `Int (ID.cast_to IInt (FD.isnormal float_x))
+                  | "__builtin_signbit" -> `Int (ID.cast_to IInt (FD.signbit float_x))
+                  | _ -> failwith "impossible matching"
+                end 
+              in
+              begin match lv with
+                | Some lv_val -> set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) gs st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st lv_val) (Cilfacade.typeOfLval lv_val) result
+                | None -> st
+              end
+            | _ -> failwith ("non-floating-point argument in call to function "^name)
+          end
+        | _ -> failwith ("strange "^name^" arguments")
+      end
     (* handling thread creations *)
     | `ThreadCreate _ ->
       invalidate_ret_lv ctx.local (* actual results joined via threadspawn *)

src/cdomains/floatDomain.ml

@@ -30,6 +30,18 @@ module type FloatArith = sig
   (** Equal to: [x == y] *)
   val ne : t -> t -> IntDomain.IntDomTuple.t
   (** Not equal to: [x != y] *)
+
+  (** {unary functions returning int} *)
+  val isfinite : t -> IntDomain.IntDomTuple.t
+  (** __builtin_isfinite(x) *)
+  val isinf : t -> IntDomain.IntDomTuple.t
+  (** __builtin_isinf(x) *)
+  val isnan : t -> IntDomain.IntDomTuple.t
+  (** __builtin_isnan(x) *)
+  val isnormal : t -> IntDomain.IntDomTuple.t
+  (** __builtin_isnormal(x) *)
+  val signbit : t -> IntDomain.IntDomTuple.t
+  (** __builtin_signbit(x) *)
 end
 
 module type FloatDomainBase = sig
@@ -277,6 +289,42 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct
 
   let ne = eval_int_binop eval_ne
 
+  let true_nonZero_IInt = IntDomain.IntDomTuple.of_excl_list IInt [(Big_int_Z.big_int_of_int 0)]
+  let false_zero_IInt = IntDomain.IntDomTuple.of_int IInt (Big_int_Z.big_int_of_int 0)
+  let unknown_IInt = IntDomain.IntDomTuple.top_of IInt
+
+  let isfinite op =
+    match op with 
+    | Some v -> true_nonZero_IInt
+    | None -> unknown_IInt
+
+  let isinf op =
+    match op with 
+    | Some v -> false_zero_IInt
+    | None -> unknown_IInt
+
+  let isnan = isinf (**currently we cannot decide if we are NaN or +-inf; both are only in Top*)
+
+  let isnormal op =
+    match op with 
+    | Some (l, h) -> 
+      if l >= Float_t.smallest || h <= (Float_t.neg (Float_t.smallest)) then
+        true_nonZero_IInt
+      else if l > (Float_t.neg (Float_t.smallest)) && h < Float_t.smallest then
+        false_zero_IInt
+      else 
+        unknown_IInt
+    | None -> unknown_IInt
+
+  (**it seems strange not to return a explicit 1 for negative numbers, but in c99 signbit is defined as: *)
+  (**<<The signbit macro returns a nonzero value if and only if the sign of its argument value is negative.>> *)
+  let signbit op = 
+    match op with
+    | Some (_, h) when h < Float_t.zero -> true_nonZero_IInt
+    | Some (l, _) when l > Float_t.zero -> false_zero_IInt
+    | Some _ -> unknown_IInt (**any interval containing zero has to fall in this case, because we do not distinguish between 0. and -0. *)
+    | None -> unknown_IInt
+
 end
 
 module F64Interval = FloatIntervalImpl(CDouble)
@@ -342,9 +390,7 @@ module FloatIntervalImplLifted = struct
          however we could instead of crashing also return top_of some fkind to vaid this and nonetheless have no actual information about anything*)
       failwith "unsupported fkind" 
 
-  let neg = function 
-    | F32 x -> F32 (F1.neg x)
-    | F64 x -> F64 (F2.neg x)
+  let neg = lift (F1.neg, F2.neg)
   let add = lift2 (F1.add, F2.add)
   let sub = lift2 (F1.sub, F2.sub)
   let mul = lift2 (F1.mul, F2.mul)
@@ -355,6 +401,11 @@ module FloatIntervalImplLifted = struct
   let ge = lift2_cmp (F1.ge, F2.ge)
   let eq = lift2_cmp (F1.eq, F2.eq)
   let ne = lift2_cmp (F1.ne, F2.ne)
+  let isfinite = dispatch (F1.isfinite, F2.isfinite)
+  let isinf = dispatch (F1.isinf, F2.isinf)
+  let isnan = dispatch (F1.isnan, F2.isnan)
+  let isnormal = dispatch (F1.isnormal, F2.isnormal)
+  let signbit = dispatch (F1.signbit, F2.signbit)
 
   let bot_of fkind = dispatch_fkind fkind (F1.bot, F2.bot)
   let bot () = failwith "bot () is not implemented for FloatIntervalImplLifted."
@@ -441,14 +492,18 @@ module FloatDomTupleImpl = struct
 
   let mapp r = BatOption.map (r.fp (module F1))
 
-  let map r a = BatOption.(map (r.f1 (module F1)) a)
+  let map r a = BatOption.map (r.f1 (module F1)) a
   let map2 r xa ya = opt_map2 (r.f2 (module F1)) xa ya
   let map2p r xa ya = opt_map2 (r.f2p (module F1)) xa ya
 
   let map2int r xa ya =
     Option.map_default identity
       (IntDomain.IntDomTuple.top_of IBool) (opt_map2 (r.f2p (module F1)) xa ya)
 
+  let map1int r xa =
+    Option.map_default identity
+      (IntDomain.IntDomTuple.top_of IInt) (BatOption.map (r.fp (module F1)) xa)
+
   let ( %% ) f g x = f % g x
 
   let show x =
@@ -537,7 +592,7 @@ module FloatDomTupleImpl = struct
   let div =
     map2 { f2= (fun (type a) (module F : FloatDomain with type t = a) -> F.div); }
 
-  (* f2: binary ops which return an integer *)
+  (* f2p: binary ops which return an integer *)
   let lt =
     map2int { f2p= (fun (type a) (module F : FloatDomain with type t = a) -> F.lt); }
   let gt =
@@ -551,6 +606,18 @@ module FloatDomTupleImpl = struct
   let ne =
     map2int { f2p= (fun (type a) (module F : FloatDomain with type t = a) -> F.ne); }
 
+  (* fp: unary functions which return an integer *)
+  let isfinite =
+    map1int { fp= (fun (type a) (module F : FloatDomain with type t = a) -> F.isfinite); }
+  let isinf =
+    map1int { fp= (fun (type a) (module F : FloatDomain with type t = a) -> F.isinf); }
+  let isnan =
+    map1int { fp= (fun (type a) (module F : FloatDomain with type t = a) -> F.isnan); }
+  let isnormal =
+    map1int { fp= (fun (type a) (module F : FloatDomain with type t = a) -> F.isnormal); }
+  let signbit =
+    map1int { fp= (fun (type a) (module F : FloatDomain with type t = a) -> F.signbit); }
+
   let pretty_diff () (x, y) = dprintf "%a instead of %a" pretty x pretty y
 
   let printXml f x =

src/cdomains/floatDomain.mli

@@ -28,6 +28,18 @@ module type FloatArith = sig
   (** Equal to: [x == y] *)
   val ne : t -> t -> IntDomain.IntDomTuple.t
   (** Not equal to: [x != y] *)
+
+  (** {unary functions returning int} *)
+  val isfinite : t -> IntDomain.IntDomTuple.t
+  (** __builtin_isfinite(x) *)
+  val isinf : t -> IntDomain.IntDomTuple.t
+  (** __builtin_isinf(x) *)
+  val isnan : t -> IntDomain.IntDomTuple.t
+  (** __builtin_isnan(x) *)
+  val isnormal : t -> IntDomain.IntDomTuple.t
+  (** __builtin_isnormal(x) *)
+  val signbit : t -> IntDomain.IntDomTuple.t
+  (** __builtin_signbit(x) *)
 end
 
 module type FloatDomainBase = sig

tests/regression/56-floats/06-library_functions.c

@@ -0,0 +1,51 @@
+// PARAM: --enable ana.float.interval --enable ana.int.interval
+#include <assert.h>
+#include <math.h>
+#include <float.h>
+
+int main() {
+    double dbl_min = 2.2250738585072014e-308;
+    double inf = 1. / 0.;
+    double nan = 0. / 0.;
+
+    //__buitin_isfinite(x):
+    assert(__builtin_isfinite(1.0)); //SUCCESS!
+    assert(__builtin_isfinite(inf)); //UNKNOWN
+    assert(__builtin_isfinite(nan)); //UNKNOWN
+
+    //__buitin_isinf(x):
+    assert(__builtin_isinf(1.0)); //FAIL!
+    assert(__builtin_isinf(inf)); //UNKNOWN
+    assert(__builtin_isinf(nan)); //UNKNOWN
+
+    //__buitin_isinf_sign(x):
+    assert(__builtin_isinf_sign(1.0)); //FAIL!
+    assert(__builtin_isinf_sign(inf)); //UNKNOWN
+    assert(__builtin_isinf_sign(- inf)); //UNKNOWN
+    assert(__builtin_isinf_sign(nan)); //UNKNOWN
+
+    //__buitin_isnan(x):
+    assert(__builtin_isnan(1.0)); //FAIL!
+    assert(__builtin_isnan(inf)); //UNKNOWN
+    assert(__builtin_isnan(nan)); //UNKNOWN
+
+    //__buitin_isnormal(x):
+    assert(__builtin_isnormal(dbl_min)); //SUCCESS!
+    assert(__builtin_isnormal(0.0)); //FAIL!
+    assert(__builtin_isnormal(dbl_min / 2)); //FAIL!
+    assert(__builtin_isnormal(inf)); //UNKNOWN
+    assert(__builtin_isnormal(nan)); //UNKNOWN
+
+    //__buitin_signbit(x):
+    assert(__builtin_signbit(1.0)); //FAIL!
+    assert(__builtin_signbit(-1.0)); //SUCCESS!
+    assert(__builtin_signbit(0.0)); //UNKNOWN
+    assert(__builtin_signbit(inf)); //UNKNOWN
+    assert(__builtin_signbit(- inf)); //UNKNOWN
+    assert(__builtin_signbit(nan)); //UNKNOWN
+
+    //unimplemented math.h function, should not invalidate globals:
+    cos(0.1); //NOWARN
+    j0(0.1); //NOWARN
+    ldexp(0.1, 1); //NOWARN
+}