Commit c1ffa08a by Julien Signoles

### [typing] improve precision for floats

parent 64410979
 ... ... @@ -120,14 +120,42 @@ let lift_unop f = function | Rational | Real | Nan as i -> i let lift_binop ~safe_float f i1 i2 = match i1, i2 with | Ival iv, i when Ival.is_bottom iv -> i | i, Ival iv when Ival.is_bottom iv -> i | Ival i1, Ival i2 -> Ival (f i1 i2) | Float(k1, _), Float(k2, _) when safe_float -> let k = if Stdlib.compare k1 k2 >= 0 then k1 else k2 in Float(k, None (* lost value, if any before *)) | Ival iv, Float(k, _) | Float(k, _), Ival iv -> if safe_float then match Ival.min_and_max iv with | None, None -> (* unbounded integers *) Rational | Some min, Some max -> (* if the interval of integers fits into the float types, then return this float type; otherwise return Rational *) (try let to_float n = Int64.to_float (Integer.to_int64 n) in let mini, maxi = to_float min, to_float max in let minf, maxf = match k with | FFloat -> Floating_point.most_negative_single_precision_float, Floating_point.max_single_precision_float | FDouble -> -. Float.max_float, Float.max_float | FLongDouble -> raise Exit in if mini >= minf && maxi <= maxf then Float(k, None) else Rational with Z.Overflow | Exit -> Rational) | None, Some _ | Some _, None -> assert false else Rational (* sound over-approximation *) | (Ival _ | Float _ | Rational), (Float _ | Rational) | (Float _ | Rational), Ival _ -> (* any binary operator over a float or a rational generates a rational *) | Rational, Ival _ -> Rational | (Ival _ | Float _ | Rational | Real), Real | Real, (Ival _ | Float _ | Rational) -> ... ... @@ -336,7 +364,7 @@ end = struct let (_, p as named_p) = extract_profile ~infer old_profile t in try let old_i = LF.Hashtbl.find named_profiles named_p in if is_included i old_i then true, p, old_i if is_included i old_i then true, p, old_i (* fixpoint reached *) else begin let j = join i old_i in LF.Hashtbl.replace named_profiles named_p j; ... ...
 ... ... @@ -64,9 +64,10 @@ int main (void) { k(9); double d = 2.0; /*@ assert f2(d) > 0; */ ; // not yet supported /* double d = 2.0; */ /* /\*@ assert f2(d) > 0; *\/ ; */ /* /\*@ assert p_notyet(27); *\/ ; */ /* /\*@ assert f_notyet(27) == 27; *\/ ; */ }
 ... ... @@ -28,4 +28,14 @@ function __e_acsl_assert: precondition got status unknown. [eva:alarm] tests/gmp/functions.c:49: Warning: function __e_acsl_assert: precondition got status unknown. [eva] using specification for function __gmpq_init [eva] using specification for function __gmpq_set_str [eva] using specification for function __gmpq_set_d [eva] using specification for function __gmpq_div [eva] using specification for function __gmpq_get_d [eva] using specification for function __gmpq_clear [eva:alarm] tests/gmp/functions.c:68: Warning: non-finite double value. assert \is_finite(__gen_e_acsl__10); [eva:alarm] tests/gmp/functions.c:68: Warning: function __e_acsl_assert: precondition got status unknown. [eva] done for function main
 ... ... @@ -47,4 +47,14 @@ function __e_acsl_assert: precondition got status unknown. [eva:alarm] tests/gmp/functions.c:25: Warning: function __e_acsl_assert: precondition got status unknown. [eva] using specification for function __gmpq_init [eva] using specification for function __gmpq_set_str [eva] using specification for function __gmpq_set_d [eva] using specification for function __gmpq_div [eva] using specification for function __gmpq_get_d [eva] using specification for function __gmpq_clear [eva:alarm] tests/gmp/functions.c:68: Warning: non-finite double value. assert \is_finite(__gen_e_acsl__15); [eva:alarm] tests/gmp/functions.c:68: Warning: function __e_acsl_assert: precondition got status unknown. [eva] done for function main
 ... ... @@ -74,6 +74,8 @@ int glob = 5; */ /*@ logic double f2(double x) = (double)(1 / x); */ double __gen_e_acsl_f2(double x); /*@ predicate p_notyet{L}(ℤ x) = x > 0; */ /*@ logic ℤ f_notyet{L}(ℤ x) = x; ... ... @@ -203,6 +205,14 @@ int main(void) (char *)"main",(char *)"t2(t1(m)) == 17",63); } __gen_e_acsl_k(9); double d = 2.0; /*@ assert f2(d) > 0; */ { double __gen_e_acsl_f2_2; __gen_e_acsl_f2_2 = __gen_e_acsl_f2(d); __e_acsl_assert(__gen_e_acsl_f2_2 > 0.,(char *)"Assertion", (char *)"main",(char *)"f2(d) > 0",68); } __retres = 0; return __retres; } ... ... @@ -230,6 +240,27 @@ int __gen_e_acsl_g_hidden(int x) return x; } double __gen_e_acsl_f2(double x) { __e_acsl_mpq_t __gen_e_acsl__8; __e_acsl_mpq_t __gen_e_acsl__9; __e_acsl_mpq_t __gen_e_acsl_div; double __gen_e_acsl__10; __gmpq_init(__gen_e_acsl__8); __gmpq_set_str(__gen_e_acsl__8,"1",10); __gmpq_init(__gen_e_acsl__9); __gmpq_set_d(__gen_e_acsl__9,x); __gmpq_init(__gen_e_acsl_div); __gmpq_div(__gen_e_acsl_div,(__e_acsl_mpq_struct const *)(__gen_e_acsl__8), (__e_acsl_mpq_struct const *)(__gen_e_acsl__9)); __gen_e_acsl__10 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div)); __gmpq_clear(__gen_e_acsl__8); __gmpq_clear(__gen_e_acsl__9); __gmpq_clear(__gen_e_acsl_div); /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__10); */ return __gen_e_acsl__10; } int __gen_e_acsl_g(int x) { int __gen_e_acsl_g_hidden_2; ... ...
 ... ... @@ -72,6 +72,8 @@ int glob = 5; */ /*@ logic double f2(double x) = (double)(1 / x); */ double __gen_e_acsl_f2(double x); /*@ predicate p_notyet{L}(ℤ x) = x > 0; */ /*@ logic ℤ f_notyet{L}(ℤ x) = x; ... ... @@ -249,6 +251,14 @@ int main(void) __gmpz_clear(__gen_e_acsl__12); } __gen_e_acsl_k(9); double d = 2.0; /*@ assert f2(d) > 0; */ { double __gen_e_acsl_f2_2; __gen_e_acsl_f2_2 = __gen_e_acsl_f2(d); __e_acsl_assert(__gen_e_acsl_f2_2 > 0.,(char *)"Assertion", (char *)"main",(char *)"f2(d) > 0",68); } __retres = 0; return __retres; } ... ... @@ -276,6 +286,28 @@ int __gen_e_acsl_g_hidden(int x) return x; } double __gen_e_acsl_f2(double x) { __e_acsl_mpq_t __gen_e_acsl__13; __e_acsl_mpq_t __gen_e_acsl__14; __e_acsl_mpq_t __gen_e_acsl_div; double __gen_e_acsl__15; __gmpq_init(__gen_e_acsl__13); __gmpq_set_str(__gen_e_acsl__13,"1",10); __gmpq_init(__gen_e_acsl__14); __gmpq_set_d(__gen_e_acsl__14,x); __gmpq_init(__gen_e_acsl_div); __gmpq_div(__gen_e_acsl_div, (__e_acsl_mpq_struct const *)(__gen_e_acsl__13), (__e_acsl_mpq_struct const *)(__gen_e_acsl__14)); __gen_e_acsl__15 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div)); __gmpq_clear(__gen_e_acsl__13); __gmpq_clear(__gen_e_acsl__14); __gmpq_clear(__gen_e_acsl_div); /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__15); */ return __gen_e_acsl__15; } int __gen_e_acsl_g(int x) { int __gen_e_acsl_g_hidden_2; ... ...