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.

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

Improve trigonometric abstractions #1272

Closed
wants to merge 7 commits into from
Closed
Show file tree
Hide file tree
Changes from 6 commits
Commits
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
38 changes: 36 additions & 2 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2355,6 +2355,40 @@ struct
| _ -> failwith ("non-integer argument in call to function "^f.vname)
end
in
let apply_better_trig fk (float_fun : ?asPreciseAsConcrete:bool -> ?notInf_notNaN:bool -> FD.t -> FD.t) x =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the type annotation needed, it looks a bit clunky.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Possibly, because the type inference of optional arguments is not principal: https://dev.realworldocaml.org/variables-and-functions.html#inference-of-labeled-and-optional-arguments.

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
Comment on lines +2448 to +2449
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
let matchinf = function
| `Lifted LibraryDesc.Isnan _ -> true
let matchinf = function
| `Lifted LibraryDesc.Isinf _ -> 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)
Comment on lines +2456 to +2458
Copy link
Member

@michael-schwarz michael-schwarz Nov 23, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
match Queries.ID.to_bool v with
| Some b -> not b
| None -> false)
Queries.ID.to_bool v = Some 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)
Comment on lines +2461 to +2463
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Might make sense to restructure so the lookup for isNotInf doesn't always happen.

| _ -> 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)
Expand All @@ -2372,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_unary 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))
Expand Down
63 changes: 57 additions & 6 deletions src/analyses/tmpSpecial.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Have you tried this type:

module MInvEntry = Printable.Prod3 (CilType.Exp) (LibraryDesc.MathPrintable) (SetDomain.Make(CilType.Exp))

Might make it easier on the inside to give up on the lattice structure that is unused anyway.

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 _ _ = ()

Expand Down Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think some parens are unneeded here...

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also Deps.of_list ((Lval lv)::arglist)) is constructed twice here.

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
Expand All @@ -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
Comment on lines +131 to +136
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This way of doing looks as if it may be in a figure of speech potentially trying to achieve the goal in a way that might be described as roundabout. You might want to do the filtering right in place. 😉

if Queries.MLInv.is_bot mlv then Queries.Result.top q
else mlv)
| _ -> Queries.Result.top q

let startstate v = D.bot ()
Expand Down
50 changes: 40 additions & 10 deletions src/cdomains/floatDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -34,9 +34,9 @@ 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
val sin : ?asPreciseAsConcrete:bool -> ?notInf_notNaN:bool -> t -> t
(** sin(x) *)
val tan : t -> t
(** tan(x) *)
Expand Down Expand Up @@ -791,8 +791,30 @@ 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 sin = eval_unop eval_sin
let cos ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) op =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems like we should be able to get some reuse here for sin and cos.

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 ?(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

Expand Down Expand Up @@ -907,8 +929,16 @@ 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 sin = lift (F1.sin, F2.sin)
let cos ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = function
Copy link
Member

@michael-schwarz michael-schwarz Nov 23, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
let cos ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = function
let cos ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) = function

BoolDomain.MustBool.top () is false.

| 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 ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = function
Copy link
Member

@michael-schwarz michael-schwarz Nov 23, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
let sin ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) = function
let sin ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) = 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)

Expand Down Expand Up @@ -1165,10 +1195,10 @@ 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 sin =
map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.sin); }
let cos ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
let cos ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) =
let cos ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) =

map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.cos ~asPreciseAsConcrete ~notInf_notNaN); }
let sin ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
let sin ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) ?(notInf_notNaN=BoolDomain.MustBool.top ()) =
let sin ?(asPreciseAsConcrete=false) ?(notInf_notNaN=false) =

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 =
Expand Down
6 changes: 4 additions & 2 deletions src/cdomains/floatDomain.mli
Original file line number Diff line number Diff line change
Expand Up @@ -48,10 +48,10 @@ 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
val sin : ?asPreciseAsConcrete:bool -> ?notInf_notNaN:bool -> t -> t
(** sin(x) *)

val tan : t -> t
Expand All @@ -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)) *)

Expand Down
8 changes: 7 additions & 1 deletion src/domains/queries.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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) =
Expand Down
2 changes: 1 addition & 1 deletion tests/regression/39-signed-overflows/07-abs-sqrt.c
Original file line number Diff line number Diff line change
Expand Up @@ -7,4 +7,4 @@ int main() {
int result = data * data; //NOWARN
}
return 8;
}
}
2 changes: 2 additions & 0 deletions tests/regression/39-signed-overflows/08-labs.c
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial
#include<stdlib.h>
#include<math.h>

int main() {
long data;
if (data > (-0xffffffff - 1))
Expand Down
2 changes: 2 additions & 0 deletions tests/regression/39-signed-overflows/09-labs-sqrt.c
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
//PARAM: --enable ana.int.interval --enable ana.float.interval --set ana.activated[+] tmpSpecial
#include<stdlib.h>
#include<math.h>

int main() {
int data;
if (data > (-0x7fffffff - 1) && llabs(data) < (long)sqrt((double)0x7fffffff))
Expand Down
15 changes: 15 additions & 0 deletions tests/regression/39-signed-overflows/11-cos-noninf-nonnan.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// PARAM: --enable ana.float.interval --set ana.activated[+] tmpSpecial

#include <math.h>

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;

}
15 changes: 15 additions & 0 deletions tests/regression/39-signed-overflows/12-sin-noninf-nonnan.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// PARAM: --enable ana.float.interval --set ana.activated[+] tmpSpecial

#include <math.h>

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;

}
Loading