Improve trigonometric abstractions

src/analyses/base.ml

@@ -877,9 +877,9 @@ struct
       | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~ctx st (Const (CStr (x,e))) (* TODO safe? *)
       | CastE  (t, exp) ->
         (let v = eval_rv ~ctx st exp in
-         try 
+         try
            VD.cast ~torg:(Cilfacade.typeOf exp) t v
-         with Cilfacade.TypeOfError _  -> 
+         with Cilfacade.TypeOfError _  ->
            VD.cast t v)
       | SizeOf _
       | Real _
@@ -2433,6 +2433,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 =
+        let eval_x = eval_rv ~ctx 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)
@@ -2450,8 +2484,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))

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)
+  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 ()

src/cdomain/value/cdomains/floatDomain.ml

@@ -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) *)
@@ -803,8 +803,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 =
+    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
 
@@ -919,8 +941,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
+    | 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
+    | 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)
 
@@ -1177,10 +1207,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 ()) =
+    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 ()) =
+    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 =

src/cdomain/value/cdomains/floatDomain.mli

@@ -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
@@ -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)) *)
 

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)) (ML)) (struct let topname = "All" end))
 
 module VI = Lattice.Flat (Basetype.Variables)
 
@@ -126,6 +127,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
 
@@ -195,6 +197,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 =
@@ -263,6 +266,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,
@@ -327,7 +331,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
@@ -484,6 +489,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) =

tests/regression/39-signed-overflows/07-abs-sqrt.c

@@ -7,4 +7,4 @@ int main() {
         int result = data * data; //NOWARN
     }
     return 8;
-}
+}

tests/regression/39-signed-overflows/08-labs.c

@@ -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))

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<stdlib.h>
 #include<math.h>
+
 int main() {
     int data;
     if (data > (-0x7fffffff - 1) && llabs(data) < (long)sqrt((double)0x7fffffff))

tests/regression/39-signed-overflows/11-cos-noninf-nonnan.c

@@ -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;
+
+}

tests/regression/39-signed-overflows/12-sin-noninf-nonnan.c

@@ -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;
+
+}