From 2ae79938bf17c1a190383e96056c30ee1b6109df Mon Sep 17 00:00:00 2001 From: FelixKrayer Date: Fri, 10 Jun 2022 19:01:07 +0200 Subject: [PATCH] implemented float classification functions from math.h --- src/analyses/base.ml | 25 ++++++ src/cdomains/floatDomain.ml | 77 +++++++++++++++++-- src/cdomains/floatDomain.mli | 12 +++ .../56-floats/06-library_functions.c | 51 ++++++++++++ 4 files changed, 160 insertions(+), 5 deletions(-) create mode 100644 tests/regression/56-floats/06-library_functions.c diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 15756b34ea..ed5d781402 100644 --- a/src/analyses/base.ml +++ b/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 *) diff --git a/src/cdomains/floatDomain.ml b/src/cdomains/floatDomain.ml index 3e958d0d07..1e22e8d9ec 100644 --- a/src/cdomains/floatDomain.ml +++ b/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: *) + (**<> *) + 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,7 +492,7 @@ 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 @@ -449,6 +500,10 @@ module FloatDomTupleImpl = struct 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 = diff --git a/src/cdomains/floatDomain.mli b/src/cdomains/floatDomain.mli index 8113928110..b8a4ec51dd 100644 --- a/src/cdomains/floatDomain.mli +++ b/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 diff --git a/tests/regression/56-floats/06-library_functions.c b/tests/regression/56-floats/06-library_functions.c new file mode 100644 index 0000000000..5d1e58432e --- /dev/null +++ b/tests/regression/56-floats/06-library_functions.c @@ -0,0 +1,51 @@ +// PARAM: --enable ana.float.interval --enable ana.int.interval +#include +#include +#include + +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 +}