add fabs and builtin inf/nan (#40)

Dudeldu · Jul 15, 2022 · d660e4e · d660e4e
1 parent 8c9769c
commit d660e4e
Show file tree

Hide file tree

Showing 8 changed files with 93 additions and 53 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -2590,35 +2590,39 @@ struct
       end
     (**Floating point classification and trigonometric functions defined in c99*)
     | Math { fun_args; }, _ ->
-      let apply_unary float_fun x =
+      let apply_unary fk float_fun x =
         let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in
         begin match eval_x with
-          | `Float float_x -> float_fun float_x
+          | `Float float_x -> float_fun (FD.cast_to fk float_x)
           | _ -> failwith ("non-floating-point argument in call to function "^f.vname)
         end
       in
-      let apply_binary float_fun x y =
+      let apply_binary fk float_fun x y =
         let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in
         let eval_y = eval_rv (Analyses.ask_of_ctx ctx) gs st y in
         begin match eval_x, eval_y with
-          | `Float float_x, `Float float_y -> float_fun float_x float_y
+          | `Float float_x, `Float float_y -> float_fun (FD.cast_to fk float_x) (FD.cast_to fk float_y)
           | _ -> failwith ("non-floating-point argument in call to function "^f.vname)
         end
       in
       let result =
         begin match fun_args with
-          | Isfinite x -> `Int (ID.cast_to IInt (apply_unary FD.isfinite x))
-          | Isinf x -> `Int (ID.cast_to IInt (apply_unary FD.isinf x))
-          | Isnan x -> `Int (ID.cast_to IInt (apply_unary FD.isnan x))
-          | Isnormal x -> `Int (ID.cast_to IInt (apply_unary FD.isnormal x))
-          | Signbit x -> `Int (ID.cast_to IInt (apply_unary FD.signbit x))
-          | Acos x -> `Float (apply_unary FD.acos x)
-          | Asin x -> `Float (apply_unary FD.asin x)
-          | Atan x -> `Float (apply_unary FD.atan x)
-          | Atan2 (y, x) -> `Float (apply_binary (fun y' x' -> FD.atan (FD.div y' x')) y x)
-          | Cos x -> `Float (apply_unary FD.cos x)
-          | Sin x -> `Float (apply_unary FD.sin x)
-          | Tan x -> `Float (apply_unary FD.tan x)
+          | Nan (fk, str) when Cil.isPointerType (Cilfacade.typeOf str) -> `Float (FD.top_of fk)
+          | Nan _ -> failwith ("non-pointer argument in call to function "^f.vname)
+          | Inf fk -> `Float (FD.top_of fk)
+          | Isfinite x -> `Int (ID.cast_to IInt (apply_unary FDouble FD.isfinite x))
+          | Isinf x -> `Int (ID.cast_to IInt (apply_unary FDouble FD.isinf x))
+          | Isnan x -> `Int (ID.cast_to IInt (apply_unary FDouble FD.isnan x))
+          | Isnormal x -> `Int (ID.cast_to IInt (apply_unary FDouble FD.isnormal x))
+          | Signbit x -> `Int (ID.cast_to IInt (apply_unary FDouble FD.signbit x))
+          | Fabs (fk, x) -> `Float (apply_unary fk FD.fabs x)
+          | Acos (fk, x) -> `Float (apply_unary fk FD.acos x)
+          | Asin (fk, x) -> `Float (apply_unary fk FD.asin x)
+          | Atan (fk, x) -> `Float (apply_unary fk FD.atan x)
+          | Atan2 (fk, y, x) -> `Float (apply_binary fk (fun y' x' -> FD.atan (FD.div y' x')) y x)
+          | Cos (fk, x) -> `Float (apply_unary fk FD.cos x)
+          | Sin (fk, x) -> `Float (apply_unary fk FD.sin x)
+          | Tan (fk, x) -> `Float (apply_unary fk FD.tan x)
         end
       in
       begin match lv with

diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
@@ -12,18 +12,21 @@ struct
 end
 
 type math =
+  | Nan of (Cil.fkind * Cil.exp)
+  | Inf of Cil.fkind
   | Isfinite of Cil.exp
   | Isinf of Cil.exp
   | Isnan of Cil.exp
   | Isnormal of Cil.exp
   | Signbit of Cil.exp
-  | Acos of Cil.exp
-  | Asin of Cil.exp
-  | Atan of Cil.exp
-  | Atan2 of (Cil.exp * Cil.exp)
-  | Cos of Cil.exp
-  | Sin of Cil.exp
-  | Tan of Cil.exp
+  | Fabs of (Cil.fkind * Cil.exp)
+  | Acos of (Cil.fkind * Cil.exp)
+  | Asin of (Cil.fkind * Cil.exp)
+  | Atan of (Cil.fkind * Cil.exp)
+  | Atan2 of (Cil.fkind * Cil.exp * Cil.exp)
+  | Cos of (Cil.fkind * Cil.exp)
+  | Sin of (Cil.fkind * Cil.exp)
+  | Tan of (Cil.fkind * Cil.exp)
 
 (** Type of special function, or {!Unknown}. *)
 (* Use inline record if not single {!Cil.exp} argument. *)

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
@@ -63,40 +63,50 @@ let zstd_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
 (** math functions.
     Functions and builtin versions of function and macros defined in math.h. *)
 let math_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
+    ("__builtin_nan", special [__ "str" []] @@ fun str -> Math { fun_args = (Nan (FDouble, str)) });
+    ("__builtin_nanf", special [__ "str" []] @@ fun str -> Math { fun_args = (Nan (FFloat, str)) });
+    ("__builtin_nanl", special [__ "str" []] @@ fun str -> Math { fun_args = (Nan (FLongDouble, str)) });
+    ("__builtin_inf", special [] @@ Math { fun_args = Inf FDouble});
+    ("__builtin_inff", special [] @@ Math { fun_args = Inf FFloat});
+    ("__builtin_infl", special [] @@ Math { fun_args = Inf FLongDouble});
     ("__builtin_isfinite", special [__ "x" []] @@ fun x -> Math { fun_args = (Isfinite x) });
     ("__builtin_isinf", special [__ "x" []] @@ fun x -> Math { fun_args = (Isinf x) });
     ("__builtin_isinf_sign", special [__ "x" []] @@ fun x -> Math { fun_args = (Isinf x) });
     ("__builtin_isnan", special [__ "x" []] @@ fun x -> Math { fun_args = (Isnan x) });
     ("__builtin_isnormal", special [__ "x" []] @@ fun x -> Math { fun_args = (Isnormal x) });
     ("__builtin_signbit", special [__ "x" []] @@ fun x -> Math { fun_args = (Signbit x) });
-    ("__builtin_acos", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos x) });
-    ("acos", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos x) });
-    ("acosf", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos x) });
-    ("acosl", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos x) });
-    ("__builtin_asin", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin x) });
-    ("asin", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin x) });
-    ("asinf", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin x) });
-    ("asinl", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin x) });
-    ("__builtin_atan", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan x) });
-    ("atan", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan x) });
-    ("atanf", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan x) });
-    ("atanl", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan x) });
-    ("__builtin_atan2", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (y, x)) });
-    ("atan2", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (y, x)) });
-    ("atan2l", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (y, x)) });
-    ("atan2f", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (y, x)) });
-    ("__builtin_cos", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos x) });
-    ("cos", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos x) });
-    ("cosf", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos x) });
-    ("cosl", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos x) });
-    ("__builtin_sin", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin x) });
-    ("sin", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin x) });
-    ("sinf", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin x) });
-    ("sinl", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin x) });
-    ("__builtin_tan", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan x) });
-    ("tan", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan x) });
-    ("tanf", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan x) });
-    ("tanl", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan x) });
+    ("__builtin_fabs", special [__ "x" []] @@ fun x -> Math { fun_args = (Fabs (FDouble, x)) });
+    ("fabs", special [__ "x" []] @@ fun x -> Math { fun_args = (Fabs (FDouble, x)) });
+    ("fabsf", special [__ "x" []] @@ fun x -> Math { fun_args = (Fabs (FFloat, x)) });
+    ("fabsl", special [__ "x" []] @@ fun x -> Math { fun_args = (Fabs (FLongDouble, x)) });
+    ("__builtin_acos", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos (FDouble, x)) });
+    ("acos", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos (FDouble, x)) });
+    ("acosf", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos (FFloat, x)) });
+    ("acosl", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos (FLongDouble, x)) });
+    ("__builtin_asin", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin (FDouble, x)) });
+    ("asin", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin (FDouble, x)) });
+    ("asinf", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin (FFloat, x)) });
+    ("asinl", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin (FLongDouble, x)) });
+    ("__builtin_atan", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan (FDouble, x)) });
+    ("atan", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan (FDouble, x)) });
+    ("atanf", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan (FFloat, x)) });
+    ("atanl", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan (FLongDouble, x)) });
+    ("__builtin_atan2", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (FDouble, y, x)) });
+    ("atan2", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (FDouble, y, x)) });
+    ("atan2f", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (FFloat, y, x)) });
+    ("atan2l", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (FLongDouble, y, x)) });
+    ("__builtin_cos", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos (FDouble, x)) });
+    ("cos", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos (FDouble, x)) });
+    ("cosf", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos (FFloat, x)) });
+    ("cosl", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos (FLongDouble, x)) });
+    ("__builtin_sin", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin (FDouble, x)) });
+    ("sin", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin (FDouble, x)) });
+    ("sinf", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin (FFloat, x)) });
+    ("sinl", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin (FLongDouble, x)) });
+    ("__builtin_tan", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FDouble, x)) });
+    ("tan", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FDouble, x)) });
+    ("tanf", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FFloat, x)) });
+    ("tanl", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FLongDouble, x)) });
   ]
 
 (* TODO: allow selecting which lists to use *)

diff --git a/src/cdomains/floatDomain.ml b/src/cdomains/floatDomain.ml
@@ -20,6 +20,8 @@ module type FloatArith = sig
   (** Division: [x / y] *)
 
   (** {unary functions} *)
+  val fabs : t -> t
+  (** fabs(x) *)
   val acos : t -> t
   (** acos(x) *)
   val asin : t -> t
@@ -408,6 +410,11 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct
   (**This Constant overapproximates pi to use as bounds for the return values of trigonometric functions *)
   let overapprox_pi = 3.1416
 
+  let eval_fabs = function
+    | (l, h) when l > Float_t.zero -> Interval (l, h)
+    | (l, h) when h < Float_t.zero -> neg (Interval (l, h))
+    | (l, h) -> Interval (Float_t.zero, max (Float_t.fabs l) (Float_t.fabs h))
+
   let eval_acos = function
     | (l, h) when l = h && l = Float_t.of_float Nearest 1. -> of_const 0. (*acos(1) = 0*)
     | (l, h) ->
@@ -444,6 +451,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct
   let isnormal = eval_unop unknown_IInt eval_isnormal
   let signbit = eval_unop unknown_IInt eval_signbit
 
+  let fabs = eval_unop (top ()) eval_fabs
   let acos = eval_unop (top ()) eval_acos
   let asin = eval_unop (top ()) eval_asin
   let atan = eval_unop (top ()) eval_atan
@@ -535,6 +543,7 @@ module FloatIntervalImplLifted = struct
       failwith "unsupported fkind"
 
   let neg = lift (F1.neg, F2.neg)
+  let fabs = lift (F1.fabs, F2.fabs)
   let acos = lift (F1.acos, F2.acos)
   let asin = lift (F1.asin, F2.asin)
   let atan = lift (F1.atan, F2.atan)
@@ -738,6 +747,8 @@ module FloatDomTupleImpl = struct
   let neg =
     map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.neg); }
   (* f1: unary functions *)
+  let fabs =
+    map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.fabs); }
   let acos =
     map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.acos); }
   let asin =

diff --git a/src/cdomains/floatDomain.mli b/src/cdomains/floatDomain.mli
@@ -18,6 +18,8 @@ module type FloatArith = sig
   (** Division: [x / y] *)
 
   (** {unary functions} *)
+  val fabs : t -> t
+  (** fabs(x) *)
   val acos : t -> t
   (** acos(x) *)
   val asin : t -> t

diff --git a/src/cdomains/floatOps/floatOps.ml b/src/cdomains/floatOps/floatOps.ml
@@ -28,6 +28,7 @@ module type CFloatType = sig
   val to_string: t -> string
 
   val neg: t -> t
+  val fabs: t -> t
   val add: round_mode -> t -> t -> t
   val sub: round_mode -> t -> t -> t
   val mul: round_mode -> t -> t -> t
@@ -64,6 +65,7 @@ module CDouble = struct
   let to_string = Float.to_string
 
   let neg = Float.neg
+  let fabs = Float.abs
   external add: round_mode -> t -> t -> t = "add_double"
   external sub: round_mode -> t -> t -> t = "sub_double"
   external mul: round_mode -> t -> t -> t = "mul_double"
@@ -94,6 +96,7 @@ module CFloat = struct
   let to_string = Float.to_string
 
   let neg = Float.neg
+  let fabs = Float.abs
   external add: round_mode -> t -> t -> t = "add_float"
   external sub: round_mode -> t -> t -> t = "sub_float"
   external mul: round_mode -> t -> t -> t = "mul_float"

diff --git a/src/cdomains/floatOps/floatOps.mli b/src/cdomains/floatOps/floatOps.mli
@@ -29,6 +29,7 @@ module type CFloatType = sig
 
 
   val neg: t -> t
+  val fabs: t -> t
   val add: round_mode -> t -> t -> t
   val sub: round_mode -> t -> t -> t
   val mul: round_mode -> t -> t -> t

diff --git a/tests/regression/57-floats/06-library_functions.c b/tests/regression/57-floats/06-library_functions.c
@@ -6,8 +6,8 @@
 int main()
 {
     double dbl_min = 2.2250738585072014e-308;
-    double inf = 1. / 0.;
-    double nan = 0. / 0.;
+    double inf = __builtin_inf();
+    double nan = __builtin_nan("");
 
     //__buitin_isfinite(x):
     assert(__builtin_isfinite(1.0)); // SUCCESS
@@ -45,6 +45,12 @@ int main()
     assert(__builtin_signbit(-inf)); // UNKNOWN
     assert(__builtin_signbit(nan));  // UNKNOWN
 
+    // fabs(x):
+    assert(4. == fabs(-4.));         // SUCCESS
+    assert(0. <= fabs(cos(0.1)));    // SUCCESS
+    assert(0. <= fabs(-inf));        // UNKNOWN
+    assert(0. <= fabs(nan));         // UNKNOWN
+
     double greater_than_pi = 3.142;
     // acos(x):
     assert((0. <= acos(0.1)) && (acos(0.1) <= greater_than_pi)); // SUCCESS