[Kernel] Fix erroneous parsing of hexadecimal floats

The parser used to always assign the [lower], [nearest] and [upper]
to the same constant for any hexadecimal float. Which is obviously
wrong.

It is fixed by using [float_of_string] and rounding modes to compute
upper and lower bounds.

src/libraries/floating_point/floating_point.c

@@ -147,25 +147,6 @@ value float_is_negative(value v) {
   return (Val_int((int)((uv.i) >> 63)));
 }
 
-// Some compilers apply the C90 standard strictly and do not prototype
-// strtof() although it is available in the C library.
-float strtof(const char *, char **);
-
-// Convert a string into a single precision float.
-value single_precision_of_string(value str) {
-  const char *s = (const char *)str;
-  const char *s_end = s + caml_string_length(str);
-  char *end;
-  float f = strtof(s, &end);
-  char last = tolower(*end);
-  // Because strtof does not consider optional floating-point suffixes
-  // (f, F, l, L), we have to test if they are the cause of the
-  // difference, and if so, ignore it.
-  if (end != s_end && (end + 1 != s_end || (last != 'f' && last != 'l')))
-    caml_failwith("single_precision_of_string");
-  return to_ocaml(f);
-}
-
 value frama_c_round(value frama_c_prec, value num) {
   switch (decode_precision(frama_c_prec)) {
   case Single:

src/libraries/floating_point/floating_point.ml

@@ -41,7 +41,6 @@ type 'f t =
 
 
 external change_format : 'f format -> float -> float = "frama_c_change_format"
-external single_of_string : string -> float = "single_precision_of_string"
 external set_rounding_mode : rounding -> unit = "frama_c_set_round_mode" [@@noalloc]
 external get_rounding_mode : unit -> rounding = "frama_c_get_round_mode" [@@noalloc]
 
@@ -477,14 +476,20 @@ let normalize integral fractional exponent format =
 let is_hexadecimal s =
   Stdlib.(String.length s >= 2 && s.[0] = '0' && (s.[1] = 'X' || s.[1] = 'x'))
 
-let parse_hexadecimal (type f) ~(format : f format) s : f parsed_float option =
+let parse_hexadecimal (type f) ~(format : f format) s =
   let open Option.Operators in
-  let constant f = { lower = f ; nearest = f ; upper = f ; format } in
-  let single s = single_of_string s |> single in
-  match format with
-  | Long   -> let+ n = float_of_string_opt s in constant (long n)
-  | Double -> let+ n = float_of_string_opt s in constant (double n)
-  | Single -> try Some (single s |> constant) with Failure _ -> None
+  let current  = get_rounding_mode () in
+  set_rounding_mode Nearest_even ;
+  let* nearest = float_of_string_opt s in
+  let  nearest = represents ~float:nearest ~in_format:format in
+  set_rounding_mode Downward ;
+  let* lower   = float_of_string_opt s in
+  let  lower   = represents ~float:lower   ~in_format:format in
+  set_rounding_mode Upward ;
+  let* upper   = float_of_string_opt s in
+  let  upper   = represents ~float:upper   ~in_format:format in
+  set_rounding_mode current ;
+  Some { lower ; nearest ; upper ; format }
 
 
 

src/libraries/floating_point/floating_point.mli

@@ -103,7 +103,7 @@ val single : float -> single t
 val double : float -> double t
 
 (** Returns a typed long precision float. *)
-val long : float -> long   t
+val long : float -> long t
 
 (** Build a typed float of the given format given an OCaml 64-bits
     floating point number. *)

tests/float/oracle/parse.res.oracle

@@ -3,6 +3,8 @@
   Floating-point constant 0.00000000000000000000000000000000000000001e310 is not represented exactly. Will use 0x1.83a99c3ec7eb0p893.
 [kernel:parser:decimal-float] parse.i:30: Warning: 
   Floating-point constant 0.0000001E9999999999999999999 is not represented exactly. Will use inf.
+[kernel:parser:decimal-float] parse.i:36: Warning: 
+  Floating-point constant 0x1p32767L is not represented exactly. Will use inf.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
@@ -15,23 +17,19 @@
 [eva:alarm] parse.i:30: Warning: 
   non-finite double value.
   assert \is_finite((double)0.0000001E9999999999999999999);
-[eva] parse.i:36: Warning: 
-  cannot parse floating-point constant, returning imprecise result
 [eva:alarm] parse.i:36: Warning: 
   non-finite long double value. assert \is_finite(0x1p32767L);
 [eva:alarm] parse.i:37: Warning: 
   non-finite long double value. assert \is_finite(l);
 [eva:alarm] parse.i:37: Warning: 
   non-finite long double value. assert \is_finite(l);
-[eva:alarm] parse.i:37: Warning: 
-  overflow in conversion from floating-point to integer.
-  assert -2147483649 < l;
 [eva:alarm] parse.i:37: Warning: 
   overflow in conversion from floating-point to integer. assert l < 2147483648;
 [eva] Recording results for main
 [eva] Done for function main
 [eva] parse.i:30: assertion 'Eva,is_nan_or_infinite' got final status invalid.
 [eva] parse.i:36: assertion 'Eva,is_nan_or_infinite' got final status invalid.
+[eva] parse.i:37: assertion 'Eva,float_to_int' got final status invalid.
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   __retres ∈ {0}

tests/rte/oracle/finite_float.res.oracle

 [kernel] Parsing finite_float.c (with preprocessing)
+[kernel:parser:decimal-float] finite_float.c:8: Warning: 
+  Floating-point constant 0x1p10000 is not represented exactly. Will use inf.
+  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [rte:annot] annotating function main
 /* Generated by Frama-C */
 #include "errno.h"