improve sin as well

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

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 =

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