Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

add fabs and builtins inf/nan #40

Merged
merged 1 commit into from
Jul 15, 2022
Merged

add fabs and builtins inf/nan #40

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 20 additions & 16 deletions src/analyses/base.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
17 changes: 10 additions & 7 deletions src/analyses/libraryDesc.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand Down
66 changes: 38 additions & 28 deletions src/analyses/libraryFunctions.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
11 changes: 11 additions & 0 deletions src/cdomains/floatDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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) ->
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 =
Expand Down
2 changes: 2 additions & 0 deletions src/cdomains/floatDomain.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions src/cdomains/floatOps/floatOps.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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"
Expand Down
1 change: 1 addition & 0 deletions src/cdomains/floatOps/floatOps.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 8 additions & 2 deletions tests/regression/57-floats/06-library_functions.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down