From 3087fff2195a083eb8a733fe0ac1c76bc6b9f5cd Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 23 Nov 2023 14:15:00 +0100 Subject: [PATCH 1/6] better cos computation in case argument is neither inf nor nan --- src/analyses/base.ml | 36 ++++++++++++++++++++- src/analyses/tmpSpecial.ml | 63 ++++++++++++++++++++++++++++++++---- src/cdomains/floatDomain.ml | 25 +++++++++++--- src/cdomains/floatDomain.mli | 4 ++- src/domains/queries.ml | 8 ++++- 5 files changed, 122 insertions(+), 14 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 5b9a00313e..0312a8ad2b 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2355,6 +2355,40 @@ struct | _ -> failwith ("non-integer argument in call to function "^f.vname) end in + let apply_cos fk (float_fun : ?asPreciseAsConcrete:bool -> ?notInf_notNaN:bool -> FD.t -> FD.t) x = + let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in + begin match eval_x with + | Float float_x -> + let notInf_notNaN = match x with + | Lval (Var xvar, offs) -> ( + match ctx.ask (Q.TmpSpecialInv (xvar, Offset.Exp.of_cil offs)) with + | s when Q.MLInv.is_top s -> false + | s -> + let matchnan = function + | `Lifted LibraryDesc.Isnan _ -> true + | _ -> false in + let matchinf = function + | `Lifted LibraryDesc.Isnan _ -> true + | _ -> false in + let isFalse = function + | `Lifted expy -> ( + match ctx.ask (Q.EvalInt expy) with + | v when Queries.ID.is_bot v -> false + | v -> + match Queries.ID.to_bool v with + | Some b -> not b + | None -> false) + | _ -> false + in + let isNotNan = Q.MLInv.exists (fun (y, ml) -> matchnan ml && isFalse y) s in + let isNotInf = Q.MLInv.exists (fun (y, ml) -> matchinf ml && isFalse y) s in + isNotInf && isNotNan) + | _ -> false + in + float_fun ~notInf_notNaN (FD.cast_to fk float_x) + | _ -> failwith ("non-floating-point argument in call to function "^f.vname) + end + in let result:value = begin match fun_args with | Nan (fk, str) when Cil.isPointerType (Cilfacade.typeOf str) -> Float (FD.nan_of fk) @@ -2372,7 +2406,7 @@ struct | 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) + | Cos (fk, x) -> Float (apply_cos fk FD.cos x) | Sin (fk, x) -> Float (apply_unary fk FD.sin x) | Tan (fk, x) -> Float (apply_unary fk FD.tan x) | Isgreater (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.gt x y)) diff --git a/src/analyses/tmpSpecial.ml b/src/analyses/tmpSpecial.ml index 9ed6da7c60..eb78d18695 100644 --- a/src/analyses/tmpSpecial.ml +++ b/src/analyses/tmpSpecial.ml @@ -13,13 +13,29 @@ struct let name () = "tmpSpecial" module ML = LibraryDesc.MathLifted - module Deps = SetDomain.Reverse (SetDomain.ToppedSet (CilType.Exp) (struct let topname = "All" end)) + module Deps = SetDomain.ToppedSet (CilType.Exp) (struct let topname = "All" end) module MLDeps = Lattice.Prod (ML) (Deps) - module D = MapDomain.MapBot (Mval.Exp) (MLDeps) + + (* x maps to (mathf(arg), deps) arg if x = mathf(arg) *) + module MM = MapDomain.MapBot_LiftTop (Mval.Exp) (MLDeps) + + (* arg maps to (x, mathf(arg), deps) if x = mathf(arg) *) + module ExpFlat = Lattice.Flat (CilType.Exp) (Printable.DefaultNames) + module MInvEntry = Lattice.Prod3 (ExpFlat) (ML) (Deps) + module MInvEntrySet = SetDomain.Reverse (SetDomain.ToppedSet (MInvEntry) (struct let topname = "All" end)) + module MInv = MapDomain.MapBot_LiftTop (Mval.Exp) (MInvEntrySet) + + module D = Lattice.Prod (MM) (MInv) module C = Lattice.Unit let invalidate ask exp_w st = - D.filter (fun _ (ml, deps) -> (Deps.for_all (fun arg -> not (VarEq.may_change ask exp_w arg)) deps)) st + let depNotChanged = Deps.for_all (fun arg -> not (VarEq.may_change ask exp_w arg)) in + let invalidate1 m = MM.filter (fun _ (ml, deps) -> depNotChanged deps) m in + let invalidate2 m = MInv.map (fun es -> + match es with + | es when MInvEntrySet.is_bot es -> es + | es -> MInvEntrySet.filter (fun (_,_,deps) -> depNotChanged deps) es) m in + invalidate1 (fst st), invalidate2 (snd st) let context _ _ = () @@ -70,8 +86,30 @@ struct (* actually it would be necessary to check here, if one of the arguments is written by the call. However this is not the case for any of the math functions and no other functions are covered so far *) if List.exists (fun arg -> VarEq.may_change ask (mkAddrOf lv) arg) arglist then d - else - D.add (v, Offset.Exp.of_cil offs) ((ML.lift fun_args, Deps.of_list ((Lval lv)::arglist))) d + else ( + if M.tracing then M.trace "tmpSpecialInv" "build tmpSpecial Entry for Lval %s\n" v.vname; + let d1 = MM.add (v, Offset.Exp.of_cil offs) ((ML.lift fun_args, Deps.of_list ((Lval lv)::arglist))) (fst d) in + let castNeglectable t x = match fun_args with + | LibraryDesc.Isinf _ + | LibraryDesc.Isnan _ -> BaseDomain.VD.is_safe_cast t (Cilfacade.typeOfLval x) + | _ -> false + in + let build_inv_entry varg offsarg = + if M.tracing then M.trace "tmpSpecialInv" "build tmpSpecialInv Entry for Argument %s\n" varg.vname; + let key = (varg, Offset.Exp.of_cil offsarg) in + let newE = (`Lifted (Lval lv), ML.lift fun_args, Deps.of_list ((Lval lv)::arglist)) in + if M.tracing then M.trace "tmpSpecialInv" "newE (lv: %s, ml: %s)\n" v.vname (LibraryDesc.MathPrintable.show fun_args); + let combined = match MInv.find key (snd d) with + | `Top -> MInvEntrySet.singleton newE + | s -> MInvEntrySet.add newE s in + Some (key, combined) in + let pick_lval = function + | Lval (Var varg, offsarg) -> build_inv_entry varg offsarg + (* we store the relationship neglecting the cast only in case of upcasting and math functions being IsNan and IsInf *) + | CastE(t, Lval (Var varg, offsarg)) when castNeglectable t (Var varg, offsarg) -> build_inv_entry varg offsarg + | _ -> None in + let d2 = MInv.add_list (List.filter_map pick_lval arglist) (snd d) in + d1, d2) | _ -> d in @@ -82,9 +120,22 @@ struct let query ctx (type a) (q: a Queries.t) : a Queries.result = match q with - | TmpSpecial lv -> let ml = fst (D.find lv ctx.local) in + | TmpSpecial lv -> let ml = fst (MM.find lv (fst ctx.local)) in if ML.is_bot ml then Queries.Result.top q else ml + | TmpSpecialInv lv -> ( + if M.tracing then M.trace "tmpSpecialInv" "MInv.find lv: %s\n" (fst lv).vname; + match MInv.find lv (snd ctx.local) with + | `Top -> Queries.Result.top q + | es -> + let mlv = MInvEntrySet.fold (fun (v, ml, deps) acc -> Queries.MLInv.add (v,ml) acc) es (Queries.MLInv.empty ()) + |> Queries.MLInv.filter (fun (v,ml) -> + match ml, v with + | `Bot, _ -> false + | _, `Lifted exp -> true + | _ -> false) in + if Queries.MLInv.is_bot mlv then Queries.Result.top q + else mlv) | _ -> Queries.Result.top q let startstate v = D.bot () diff --git a/src/cdomains/floatDomain.ml b/src/cdomains/floatDomain.ml index 39d3744401..6849593eef 100644 --- a/src/cdomains/floatDomain.ml +++ b/src/cdomains/floatDomain.ml @@ -34,7 +34,7 @@ module type FloatArith = sig (** asin(x) *) val atan : t -> t (** atan(x) *) - val cos : t -> t + val cos : ?asPreciseAsConcrete:bool -> ?notInf_notNaN:bool -> t -> t (** cos(x) *) val sin : t -> t (** sin(x) *) @@ -791,7 +791,18 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let acos = eval_unop eval_acos let asin = eval_unop eval_asin let atan = eval_unop eval_atan - let cos = eval_unop eval_cos + let cos ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) op = + match op with + | Bot -> raise (ArithmeticOnFloatBot (Printf.sprintf "unop %s" (show op))) + (* TODO: cos should return NaN if argument is + or - infinity, fix this. *) + | Interval v -> eval_cos v + | PlusInfinity + | MinusInfinity + | NaN -> NaN + | Top -> + if asPreciseAsConcrete && notInf_notNaN then + eval_cos (Float_t.lower_bound, Float_t.upper_bound) + else top() let sin = eval_unop eval_sin let tan = eval_unop eval_tan let sqrt = eval_unop eval_sqrt @@ -907,7 +918,11 @@ module FloatIntervalImplLifted = struct let acos = lift (F1.acos, F2.acos) let asin = lift (F1.asin, F2.asin) let atan = lift (F1.atan, F2.atan) - let cos = lift (F1.cos, F2.cos) + let cos ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = function + | F32 a -> F32 (F1.cos ~asPreciseAsConcrete:true ~notInf_notNaN a) + | F64 a -> F64 (F2.cos ~asPreciseAsConcrete:true ~notInf_notNaN a) + | FLong a -> FLong (F2.cos ~notInf_notNaN a) + | FFloat128 a -> FFloat128 (F2.cos ~notInf_notNaN a) let sin = lift (F1.sin, F2.sin) let tan = lift (F1.tan, F2.tan) let sqrt = lift (F1.sqrt, F2.sqrt) @@ -1165,8 +1180,8 @@ module FloatDomTupleImpl = struct map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.asin); } let atan = map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.atan); } - let cos = - map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.cos); } + let cos ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = + map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.cos ~asPreciseAsConcrete ~notInf_notNaN); } let sin = map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.sin); } let tan = diff --git a/src/cdomains/floatDomain.mli b/src/cdomains/floatDomain.mli index d958e1ee81..e978d3772b 100644 --- a/src/cdomains/floatDomain.mli +++ b/src/cdomains/floatDomain.mli @@ -48,7 +48,7 @@ module type FloatArith = sig val atan : t -> t (** atan(x) *) - val cos : t -> t + val cos : ?asPreciseAsConcrete:bool -> ?notInf_notNaN:bool -> t -> t (** cos(x) *) val sin : t -> t @@ -63,8 +63,10 @@ module type FloatArith = sig (** {inversions of unary functions}*) val inv_ceil : ?asPreciseAsConcrete:bool -> t -> t (** (inv_ceil z -> x) if (z = ceil(x)) *) + val inv_floor : ?asPreciseAsConcrete:bool -> t -> t (** (inv_floor z -> x) if (z = floor(x)) *) + val inv_fabs : t -> t (** (inv_fabs z -> x) if (z = fabs(x)) *) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index b9fa28f5be..4824c5324b 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -16,6 +16,7 @@ module TC = WrapperFunctionAnalysis0.ThreadCreateUniqueCount module ThreadNodeLattice = Lattice.Prod (NFL) (TC) module ML = LibraryDesc.MathLifted +module MLInv = SetDomain.Reverse (SetDomain.ToppedSet (Lattice.Prod (Lattice.Flat (CilType.Exp) (Printable.DefaultNames)) (ML)) (struct let topname = "All" end)) module VI = Lattice.Flat (Basetype.Variables) (struct let top_name = "Unknown line" @@ -131,6 +132,7 @@ type _ t = | MustTermAllLoops: MustBool.t t | IsEverMultiThreaded: MayBool.t t | TmpSpecial: Mval.Exp.t -> ML.t t + | TmpSpecialInv: Mval.Exp.t -> MLInv.t t type 'a result = 'a @@ -200,6 +202,7 @@ struct | MustTermAllLoops -> (module MustBool) | IsEverMultiThreaded -> (module MayBool) | TmpSpecial _ -> (module ML) + | TmpSpecialInv _ -> (module MLInv) (** Get bottom result for query. *) let bot (type a) (q: a t): a result = @@ -268,6 +271,7 @@ struct | MustTermAllLoops -> MustBool.top () | IsEverMultiThreaded -> MayBool.top () | TmpSpecial _ -> ML.top () + | TmpSpecialInv _ -> MLInv.top () end (* The type any_query can't be directly defined in Any as t, @@ -332,7 +336,8 @@ struct | Any MustTermAllLoops -> 54 | Any IsEverMultiThreaded -> 55 | Any (TmpSpecial _) -> 56 - | Any (IsAllocVar _) -> 57 + | Any (TmpSpecialInv _) -> 57 + | Any (IsAllocVar _) -> 58 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -489,6 +494,7 @@ struct | Any MustTermAllLoops -> Pretty.dprintf "MustTermAllLoops" | Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded" | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv + | Any (TmpSpecialInv lv) -> Pretty.dprintf "TmpSpecialInv %a" Mval.Exp.pretty lv end let to_value_domain_ask (ask: ask) = From a7265c88442e83aa03645de411d2d672b8858b46 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 23 Nov 2023 14:17:01 +0100 Subject: [PATCH 2/6] fix headers in tests --- tests/regression/39-signed-overflows/07-abs-sqrt.c | 2 +- tests/regression/39-signed-overflows/08-labs.c | 2 ++ tests/regression/39-signed-overflows/09-labs-sqrt.c | 2 ++ 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/tests/regression/39-signed-overflows/07-abs-sqrt.c b/tests/regression/39-signed-overflows/07-abs-sqrt.c index 13ed863e51..346d68a76a 100644 --- a/tests/regression/39-signed-overflows/07-abs-sqrt.c +++ b/tests/regression/39-signed-overflows/07-abs-sqrt.c @@ -7,4 +7,4 @@ int main() { int result = data * data; //NOWARN } return 8; -} \ No newline at end of file +} diff --git a/tests/regression/39-signed-overflows/08-labs.c b/tests/regression/39-signed-overflows/08-labs.c index a9c6773d11..47052196a6 100644 --- a/tests/regression/39-signed-overflows/08-labs.c +++ b/tests/regression/39-signed-overflows/08-labs.c @@ -1,5 +1,7 @@ //PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial #include +#include + int main() { long data; if (data > (-0xffffffff - 1)) diff --git a/tests/regression/39-signed-overflows/09-labs-sqrt.c b/tests/regression/39-signed-overflows/09-labs-sqrt.c index 3a4b20a82b..346e2a1757 100644 --- a/tests/regression/39-signed-overflows/09-labs-sqrt.c +++ b/tests/regression/39-signed-overflows/09-labs-sqrt.c @@ -1,5 +1,7 @@ //PARAM: --enable ana.int.interval --enable ana.float.interval --set ana.activated[+] tmpSpecial +#include #include + int main() { int data; if (data > (-0x7fffffff - 1) && llabs(data) < (long)sqrt((double)0x7fffffff)) From fde7d4d222775151e6da44c2d3114417433dcea2 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 23 Nov 2023 14:26:20 +0100 Subject: [PATCH 3/6] add test case --- .../39-signed-overflows/11-cos-noninf-nonnan.c | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 tests/regression/39-signed-overflows/11-cos-noninf-nonnan.c diff --git a/tests/regression/39-signed-overflows/11-cos-noninf-nonnan.c b/tests/regression/39-signed-overflows/11-cos-noninf-nonnan.c new file mode 100644 index 0000000000..d3b7265ee3 --- /dev/null +++ b/tests/regression/39-signed-overflows/11-cos-noninf-nonnan.c @@ -0,0 +1,15 @@ +// PARAM: --enable ana.int.interval --enable ana.float.interval --set ana.activated[+] tmpSpecial --html + +#include + +int main() /* check_lower_bound */ +{ + float x; + + if(!(!__builtin_isnan (x) && !__builtin_isinf_sign (x))) abort(); + float y = cosf(x); + if(!(__builtin_isgreaterequal(y, -1.0f))) + __goblint_check(0); // NOWARN (unreachable) + return 0; + +} From 48d5f2a9be5c098954160e90554b2e134327b4a2 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 23 Nov 2023 14:43:19 +0100 Subject: [PATCH 4/6] fix test --- tests/regression/39-signed-overflows/11-cos-noninf-nonnan.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/39-signed-overflows/11-cos-noninf-nonnan.c b/tests/regression/39-signed-overflows/11-cos-noninf-nonnan.c index d3b7265ee3..006f13988d 100644 --- a/tests/regression/39-signed-overflows/11-cos-noninf-nonnan.c +++ b/tests/regression/39-signed-overflows/11-cos-noninf-nonnan.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval --enable ana.float.interval --set ana.activated[+] tmpSpecial --html +// PARAM: --enable ana.float.interval --set ana.activated[+] tmpSpecial #include From 0107ce94de3e96ebe61da5150d7646b7abd92f6d Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 23 Nov 2023 14:48:37 +0100 Subject: [PATCH 5/6] improve sin as well --- src/analyses/base.ml | 6 +++--- src/cdomains/floatDomain.ml | 25 ++++++++++++++++++++----- src/cdomains/floatDomain.mli | 2 +- 3 files changed, 24 insertions(+), 9 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 0312a8ad2b..f033df3bbe 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2355,7 +2355,7 @@ struct | _ -> failwith ("non-integer argument in call to function "^f.vname) end in - let apply_cos fk (float_fun : ?asPreciseAsConcrete:bool -> ?notInf_notNaN:bool -> FD.t -> FD.t) x = + let apply_better_trig fk (float_fun : ?asPreciseAsConcrete:bool -> ?notInf_notNaN:bool -> FD.t -> FD.t) x = let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in begin match eval_x with | Float float_x -> @@ -2406,8 +2406,8 @@ struct | 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_cos fk FD.cos x) - | Sin (fk, x) -> Float (apply_unary fk FD.sin x) + | Cos (fk, x) -> Float (apply_better_trig fk FD.cos x) + | Sin (fk, x) -> Float (apply_better_trig fk FD.sin x) | Tan (fk, x) -> Float (apply_unary fk FD.tan x) | Isgreater (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.gt x y)) | Isgreaterequal (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.ge x y)) diff --git a/src/cdomains/floatDomain.ml b/src/cdomains/floatDomain.ml index 6849593eef..4325bae2f1 100644 --- a/src/cdomains/floatDomain.ml +++ b/src/cdomains/floatDomain.ml @@ -36,7 +36,7 @@ module type FloatArith = sig (** atan(x) *) val cos : ?asPreciseAsConcrete:bool -> ?notInf_notNaN:bool -> t -> t (** cos(x) *) - val sin : t -> t + val sin : ?asPreciseAsConcrete:bool -> ?notInf_notNaN:bool -> t -> t (** sin(x) *) val tan : t -> t (** tan(x) *) @@ -803,7 +803,18 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct if asPreciseAsConcrete && notInf_notNaN then eval_cos (Float_t.lower_bound, Float_t.upper_bound) else top() - let sin = eval_unop eval_sin + let sin ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) op = + match op with + | Bot -> raise (ArithmeticOnFloatBot (Printf.sprintf "unop %s" (show op))) + (* TODO: sin should return NaN if argument is + or - infinity, fix this. *) + | Interval v -> eval_sin v + | PlusInfinity + | MinusInfinity + | NaN -> NaN + | Top -> + if asPreciseAsConcrete && notInf_notNaN then + eval_sin (Float_t.lower_bound, Float_t.upper_bound) + else top() let tan = eval_unop eval_tan let sqrt = eval_unop eval_sqrt @@ -923,7 +934,11 @@ module FloatIntervalImplLifted = struct | F64 a -> F64 (F2.cos ~asPreciseAsConcrete:true ~notInf_notNaN a) | FLong a -> FLong (F2.cos ~notInf_notNaN a) | FFloat128 a -> FFloat128 (F2.cos ~notInf_notNaN a) - let sin = lift (F1.sin, F2.sin) + let sin ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = function + | F32 a -> F32 (F1.sin ~asPreciseAsConcrete:true ~notInf_notNaN a) + | F64 a -> F64 (F2.sin ~asPreciseAsConcrete:true ~notInf_notNaN a) + | FLong a -> FLong (F2.sin ~notInf_notNaN a) + | FFloat128 a -> FFloat128 (F2.sin ~notInf_notNaN a) let tan = lift (F1.tan, F2.tan) let sqrt = lift (F1.sqrt, F2.sqrt) @@ -1182,8 +1197,8 @@ module FloatDomTupleImpl = struct map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.atan); } let cos ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.cos ~asPreciseAsConcrete ~notInf_notNaN); } - let sin = - map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.sin); } + let sin ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = + map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.sin ~asPreciseAsConcrete ~notInf_notNaN); } let tan = map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.tan); } let sqrt = diff --git a/src/cdomains/floatDomain.mli b/src/cdomains/floatDomain.mli index e978d3772b..24fe183734 100644 --- a/src/cdomains/floatDomain.mli +++ b/src/cdomains/floatDomain.mli @@ -51,7 +51,7 @@ module type FloatArith = sig val cos : ?asPreciseAsConcrete:bool -> ?notInf_notNaN:bool -> t -> t (** cos(x) *) - val sin : t -> t + val sin : ?asPreciseAsConcrete:bool -> ?notInf_notNaN:bool -> t -> t (** sin(x) *) val tan : t -> t From be4fdad0b0917e2d56328702a555353c5f104fd8 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 23 Nov 2023 14:51:59 +0100 Subject: [PATCH 6/6] add regression test for sin --- .../39-signed-overflows/12-sin-noninf-nonnan.c | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 tests/regression/39-signed-overflows/12-sin-noninf-nonnan.c diff --git a/tests/regression/39-signed-overflows/12-sin-noninf-nonnan.c b/tests/regression/39-signed-overflows/12-sin-noninf-nonnan.c new file mode 100644 index 0000000000..30a5f762be --- /dev/null +++ b/tests/regression/39-signed-overflows/12-sin-noninf-nonnan.c @@ -0,0 +1,15 @@ +// PARAM: --enable ana.float.interval --set ana.activated[+] tmpSpecial + +#include + +int main() /* check_lower_bound */ +{ + float x; + + if(!(!__builtin_isnan (x) && !__builtin_isinf_sign (x))) abort(); + float y = sinf(x); + if(!(__builtin_isgreaterequal(y, -1.0f))) + __goblint_check(0); // NOWARN (unreachable) + return 0; + +}