[Eva] New builtin for the trigonometric function atan.

src/kernel_services/abstract_interp/fc_float.ml

@@ -224,4 +224,5 @@ let cos round = generate Floating_point.cosf cos round
 let sin round = generate Floating_point.sinf sin round
 let acos round = generate Floating_point.acosf acos round
 let asin round = generate Floating_point.asinf asin round
+let atan round = generate Floating_point.atanf atan round
 let atan2 round = generate Floating_point.atan2f atan2 round

src/kernel_services/abstract_interp/float_interval.ml

@@ -1028,6 +1028,9 @@ module Make (F: Float_sig.S) = struct
   let acos = acos_asin ~acos:true
   let asin = acos_asin ~acos:false
 
+  let atan prec t =
+    t >>: approx F.atan prec
+
   let atan2 prec x y =
     (x, y) >>% fun ~nan (b1, e1) (b2, e2) ->
     let op = F.atan2 Near prec in

src/kernel_services/abstract_interp/float_interval_sig.mli

@@ -142,6 +142,7 @@ module type S = sig
   val sin: prec -> t -> t
   val acos: prec -> t -> t
   val asin: prec -> t -> t
+  val atan: prec -> t -> t
   val atan2: prec -> t -> t -> t
 
   val backward_add:

src/kernel_services/abstract_interp/float_sig.mli

@@ -121,5 +121,6 @@ module type S = sig
   val sin: round -> prec -> t -> t
   val acos: round -> prec -> t -> t
   val asin: round -> prec -> t -> t
+  val atan: round -> prec -> t -> t
   val atan2: round -> prec -> t -> t -> t
 end

src/libraries/utils/c_bindings.c

@@ -148,6 +148,13 @@ value c_asinf(value x)
   return caml_copy_double(res);
 }
 
+value c_atanf(value x)
+{
+  float f = Double_val(x);
+  volatile float res = atanf(f); // see remarks above
+  return caml_copy_double(res);
+}
+
 value c_atan2f(value x, value y)
 {
   float fx = Double_val(x);

src/libraries/utils/floating_point.ml

@@ -428,6 +428,7 @@ external cosf: float -> float = "c_cosf"
 external sinf: float -> float = "c_sinf"
 external acosf: float -> float = "c_acosf"
 external asinf: float -> float = "c_asinf"
+external atanf: float -> float = "c_atanf"
 external atan2f: float -> float -> float = "c_atan2f"
 
 

src/libraries/utils/floating_point.mli

@@ -112,6 +112,7 @@ external cosf: float -> float = "c_cosf"
 external sinf: float -> float = "c_sinf"
 external acosf: float -> float = "c_acosf"
 external asinf: float -> float = "c_asinf"
+external atanf: float -> float = "c_atanf"
 external atan2f: float -> float -> float = "c_atan2f"
 
 

src/plugins/value/domains/cvalue/builtins_float.ml

@@ -123,6 +123,7 @@ let () =
   register_arity1 "sin" Cil_types.FDouble sin;
   register_arity1 "acos" Cil_types.FDouble acos;
   register_arity1 "asin" Cil_types.FDouble asin;
+  register_arity1 "atan" Cil_types.FDouble atan;
   register_arity1 "log" Cil_types.FDouble log;
   register_arity1 "log10" Cil_types.FDouble log10;
   register_arity1 "exp" Cil_types.FDouble exp;
@@ -136,6 +137,7 @@ let () =
   register_arity1 "sinf" Cil_types.FFloat sin;
   register_arity1 "acosf" Cil_types.FFloat acos;
   register_arity1 "asinf" Cil_types.FFloat asin;
+  register_arity1 "atanf" Cil_types.FFloat atan;
   register_arity1 "logf" Cil_types.FFloat log;
   register_arity1 "log10f" Cil_types.FFloat log10;
   register_arity1 "expf" Cil_types.FFloat exp;

tests/libc/oracle/math_h.res.oracle

@@ -29,98 +29,60 @@
   infinity ∈ {inf}
   fp_ilogb0 ∈ {-2147483648.}
   fp_ilogbnan ∈ {-2147483648.}
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
-[eva] using specification for function atan
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva:alarm] tests/libc/math_h.c:45: Warning: 
   function atan: precondition 'finite_arg' got status unknown.
-[eva] Done for function atan
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
-[eva] using specification for function atanf
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva:alarm] tests/libc/math_h.c:46: Warning: 
   function atanf: precondition 'finite_arg' got status unknown.
-[eva] Done for function atanf
 [eva] computing for function atanl <- main.
   Called from tests/libc/math_h.c:47.
 [eva] using specification for function atanl
@@ -309,24 +271,24 @@
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
-  atan_pi ∈ [-1.571 .. 1.571]
-  atan_half_pi ∈ [-1.571 .. 1.571]
-  atan_e ∈ [-1.571 .. 1.571]
-  atan_zero ∈ [-1.571 .. 1.571]
-  atan_minus_zero ∈ [-1.571 .. 1.571]
-  atan_one ∈ [-1.571 .. 1.571]
-  atan_minus_one ∈ [-1.571 .. 1.571]
-  atan_large ∈ [-1.571 .. 1.571]
-  atan_top ∈ [-1.571 .. 1.571]
-  atanf_f_pi ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_f_half_pi ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_f_e ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_zero ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_minus_zero ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_one ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_minus_one ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_large ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_f_top ∈ [-1.57099997997 .. 1.57099997997]
+  atan_pi ∈ {1.26262725568}
+  atan_half_pi ∈ {1.00388482185}
+  atan_e ∈ {1.21828290502}
+  atan_zero ∈ {0}
+  atan_minus_zero ∈ {-0.}
+  atan_one ∈ {0.785398163397}
+  atan_minus_one ∈ {-0.785398163397}
+  atan_large ∈ {1.57079632679}
+  atan_top ∈ [-1.57079632679 .. 1.57079632679] ∪ {NaN}
+  atanf_f_pi ∈ {1.262627244}
+  atanf_f_half_pi ∈ {1.00388479233}
+  atanf_f_e ∈ {1.218282938}
+  atanf_zero ∈ {0}
+  atanf_minus_zero ∈ {-0.}
+  atanf_one ∈ {0.785398185253}
+  atanf_minus_one ∈ {-0.785398185253}
+  atanf_large ∈ {1.57079637051}
+  atanf_f_top ∈ [-1.57079637051 .. 1.57079637051] ∪ {NaN}
   atanl_ld_pi ∈ [-inf .. inf]
   atanl_ld_half_pi ∈ [-inf .. inf]
   atanl_ld_e ∈ [-inf .. inf]