Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2065 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

10 files changed, 84 insertions, 86 deletions

diff --git a/cparser/.depend b/cparser/.depend
index 63cd2cb1..0b38315a 100644
--- a/cparser/.depend
+++ b/cparser/.depend
@@ -46,8 +46,8 @@ Env.cmo: C.cmi Env.cmi
 Env.cmx: C.cmi Env.cmi
 GCC.cmo: Cutil.cmi C.cmi Builtins.cmi GCC.cmi
 GCC.cmx: Cutil.cmx C.cmi Builtins.cmx GCC.cmi
-Lexer.cmo: Parser.cmi Parse_aux.cmi Cabshelper.cmo Lexer.cmi
-Lexer.cmx: Parser.cmx Parse_aux.cmx Cabshelper.cmx Lexer.cmi
+Lexer.cmo: Parser.cmi Parse_aux.cmi Cabshelper.cmo Cabs.cmo Lexer.cmi
+Lexer.cmx: Parser.cmx Parse_aux.cmx Cabshelper.cmx Cabs.cmx Lexer.cmi
 Machine.cmo: Machine.cmi
 Machine.cmx: Machine.cmi
 Main.cmo: Parse.cmi GCC.cmi Cprint.cmi Builtins.cmi
diff --git a/cparser/C.mli b/cparser/C.mli
index 52f02c4b..8e73bc56 100644
--- a/cparser/C.mli
+++ b/cparser/C.mli
@@ -52,9 +52,16 @@ type fkind =
 
 (** Constants *)
 
+type float_cst = {
+  hex : bool;
+  intPart : string;
+  fracPart : string;
+  exp : string;
+}
+
 type constant =
   | CInt of int64 * ikind * string      (* as it appeared in the source *)
-  | CFloat of float * fkind * string    (* as it appeared in the source *)
+  | CFloat of float_cst * fkind
   | CStr of string
   | CWStr of int64 list
   | CEnum of ident * int64              (* enum tag, integer value *)
diff --git a/cparser/Cabs.ml b/cparser/Cabs.ml
index a2bb512c..23d3643c 100644
--- a/cparser/Cabs.ml
+++ b/cparser/Cabs.ml
@@ -267,9 +267,17 @@ and expression =
   | MEMBEROFPTR of expression * string
   | GNU_BODY of block
 
+and floatInfo = {
+  isHex_FI:bool;
+  integer_FI:string option;
+  fraction_FI:string option;
+  exponent_FI:string option;
+  suffix_FI:char option;
+}
+
 and constant =
   | CONST_INT of string   (* the textual representation *)
-  | CONST_FLOAT of string (* the textual representaton *)
+  | CONST_FLOAT of floatInfo
   | CONST_CHAR of int64 list
   | CONST_WCHAR of int64 list
   | CONST_STRING of string
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index 4fc01e5b..621fbbf7 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -51,27 +51,19 @@ let normalize_int n ik =
 
 (* Reduce n to the range of representable floats of the given kind *)
 
-let normalize_float f fk =
-  match fk with
-  | FFloat -> Int32.float_of_bits (Int32.bits_of_float f)
-  | FDouble -> f
-  | FLongDouble -> raise Notconst (* cannot accurately compute on this type *)
-
 type value =
   | I of int64
-  | F of float
   | S of string
   | WS of int64 list
 
 let boolean_value v =
   match v with
   | I n -> n <> 0L
-  | F n -> n <> 0.0
   | S _ | WS _ -> true
 
 let constant = function
   | CInt(v, ik, _) -> I (normalize_int v ik)
-  | CFloat(v, fk, _) -> F (normalize_float v fk)
+  | CFloat(v, fk) -> raise Notconst
   | CStr s -> S s
   | CWStr s -> WS s
   | CEnum(id, v) -> I v
@@ -87,22 +79,12 @@ let cast env ty_to ty_from v =
       if boolean_value v then I 1L else I 0L
   | TInt(ik, _), I n ->
       I(normalize_int n ik)
-  | TInt(ik, _), F n ->
-      I(normalize_int (Int64.of_float n) ik)
   | TInt(ik, _), (S _ | WS _) ->
       if sizeof_ikind ik >= !config.sizeof_ptr
       then v
       else raise Notconst
-  | TFloat(fk, _), F n ->
-      F(normalize_float n fk)
-  | TFloat(fk, _), I n ->
-      if is_signed env ty_from
-      then F(normalize_float (Int64.to_float n) fk)
-      else F(normalize_float (int64_unsigned_to_float n) fk)
   | TPtr(ty, _), I n ->
       I (normalize_int n ptr_t_ikind)
-  | TPtr(ty, _), F n ->
-      if n = 0.0 then I 0L else raise Notconst
   | TPtr(ty, _), (S _ | WS _) ->
       v
   | _, _ ->
@@ -112,9 +94,7 @@ let unop env op tyres ty v =
   let res =
    match op, tyres, v with
    | Ominus, TInt _, I n -> I (Int64.neg n)
-   | Ominus, TFloat _, F n -> F (-. n)
    | Oplus, TInt _, I n -> I n
-   | Oplus, TFloat _, F n -> F n
    | Olognot, _, _ -> if boolean_value v then I 0L else I 1L
    | Onot, _, I n -> I (Int64.lognot n)
    | _ -> raise Notconst
@@ -128,8 +108,6 @@ let comparison env direction ptraction tyop ty1 v1 ty2 v2 =
         if is_signed env tyop
         then direction (compare n1 n2) 0
         else direction (int64_unsigned_compare n1 n2) 0 (* including pointers *)
-    | F n1, F n2 ->
-        direction (compare n1 n2) 0
     | (S _ | WS _), I 0L ->
         begin match ptraction with None -> raise Notconst | Some b -> b end
     | I 0L, (S _ | WS _) ->
@@ -147,7 +125,6 @@ let binop env op tyop tyres ty1 v1 ty2 v2 =
         if is_arith_type env ty1 && is_arith_type env ty2 then begin
           match cast env tyop ty1 v1, cast env tyop ty2 v2 with
           | I n1, I n2 -> I (Int64.add n1 n2)
-          | F n1, F n2 -> F (n1 +. n2)
           | _, _ -> raise Notconst
         end else
           raise Notconst
@@ -155,14 +132,12 @@ let binop env op tyop tyres ty1 v1 ty2 v2 =
         if is_arith_type env ty1 && is_arith_type env ty2 then begin
           match cast env tyop ty1 v1, cast env tyop ty2 v2 with
           | I n1, I n2 -> I (Int64.sub n1 n2)
-          | F n1, F n2 -> F (n1 -. n2)
           | _, _ -> raise Notconst
         end else
           raise Notconst
     | Omul ->
         begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with
           | I n1, I n2 -> I (Int64.mul n1 n2)
-          | F n1, F n2 -> F (n1 *. n2)
           | _, _ -> raise Notconst
         end
     | Odiv ->
@@ -171,7 +146,6 @@ let binop env op tyop tyres ty1 v1 ty2 v2 =
               if n2 = 0L then raise Notconst else
               if is_signed env tyop then I (Int64.div n1 n2)
               else I (int64_unsigned_div n1 n2)
-          | F n1, F n2 -> F (n1 /. n2)
           | _, _ -> raise Notconst
         end
     | Omod ->
@@ -261,6 +235,7 @@ let rec expr env e =
       if boolean_value (expr env e1)
       then cast env e.etyp e2.etyp (expr env e2)
       else cast env e.etyp e3.etyp (expr env e3)
+  (* | ECast(TInt (_, _), EConst (CFloat (_, _))) -> TODO *)
   | ECast(ty, e1) ->
       cast env ty e1.etyp (expr env e1)
   | ECall _ ->
@@ -277,7 +252,6 @@ let constant_expr env ty e =
   try
     match unroll env ty, cast env ty e.etyp (expr env e) with
     | TInt(ik, _), I n -> Some(CInt(n, ik, ""))
-    | TFloat(fk, _), F n -> Some(CFloat(n, fk, ""))
     | TPtr(_, _), I 0L -> Some(CInt(0L, IInt, ""))
     | TPtr(_, _), S s -> Some(CStr s)
     | TPtr(_, _), WS s -> Some(CWStr s)
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 2924c3d4..2548f3b9 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -45,16 +45,16 @@ let const pp = function
         | IUInt -> fprintf pp "U"
         | _ -> ()
       end
-  | CFloat(v, fk, s) ->
-      if s <> "" then
-        fprintf pp "%s" s
-      else begin
-        fprintf pp "%.18g" v;
-        match fk with
-        | FFloat -> fprintf pp "F"
-        | FLongDouble -> fprintf pp "L"
-        | _ -> ()
-      end
+  | CFloat(v, fk) ->
+    if v.hex then
+      fprintf pp "0x%s.%sP%s" v.intPart v.fracPart v.exp
+    else
+      fprintf pp "%s.%sE%s" v.intPart v.fracPart v.exp;
+    begin match fk with
+      | FFloat -> fprintf pp "F"
+      | FLongDouble -> fprintf pp "L"
+      | FDouble -> ()
+    end
   | CStr s ->
       fprintf pp "\"";
       for i = 0 to String.length s - 1 do
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 4856c01d..d84b9c9b 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -625,7 +625,7 @@ let enum_ikind = IInt
 
 let type_of_constant = function
   | CInt(_, ik, _) -> TInt(ik, [])
-  | CFloat(_, fk, _) -> TFloat(fk, [])
+  | CFloat(_, fk) -> TFloat(fk, [])
   | CStr _ -> TPtr(TInt(IChar, []), [])          (* XXX or array? const? *)
   | CWStr _ -> TPtr(TInt(wchar_ikind, []), [])   (* XXX or array? const? *)
   | CEnum(_, _) -> TInt(IInt, [])
@@ -708,10 +708,11 @@ let valid_cast env tfrom tto =
 let intconst v ik =
   { edesc = EConst(CInt(v, ik, "")); etyp = TInt(ik, []) }
 
-(* Construct a float constant *)
+(* Construct the 0 float constant of double type *)
 
-let floatconst v fk =
-  { edesc = EConst(CFloat(v, fk, "")); etyp = TFloat(fk, []) }
+let floatconst0 =
+  { edesc = EConst(CFloat({hex=false; intPart="0"; fracPart="0"; exp="0"}, FDouble));
+    etyp = TFloat(FDouble, []) }
 
 (* Construct the literal "0" with void * type *)
 
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 3c39b99a..64881178 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -165,8 +165,8 @@ val fundef_typ: fundef -> typ
 
 val intconst : int64 -> ikind -> exp
   (* Build expression for given integer constant. *)
-val floatconst : float -> fkind -> exp
-  (* Build expression for given float constant. *)
+val floatconst0 : exp
+  (* Build expression for (double)0. *)
 val nullconst : exp
   (* Expression for [(void * ) 0] *)
 val eaddrof : exp -> exp
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 2473cf20..0e7b5492 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -200,20 +200,19 @@ let elab_int_constant loc s0 =
   in
   (v, ty)
 
-let elab_float_constant loc s0 =
-  let s = String.uppercase s0 in
-  (* Determine type and chop suffix *)
-  let (s, ty) =
-    if has_suffix s "L" then
-      (chop_last s 1, FLongDouble)
-    else if has_suffix s "F" then
-      (chop_last s 1, FFloat)
-    else
-      (s, FDouble) in
-  (* Convert to Caml float - XXX loss of precision for long double *)
-  let v =
-    try float_of_string s
-    with Failure _ -> error loc "bad float literal '%s'" s0; 0.0 in
+let elab_float_constant loc f =
+  let ty = match f.suffix_FI with
+    | Some 'l' | Some 'L' -> FLongDouble
+    | Some 'f' | Some 'F' -> FFloat
+    | None -> FDouble
+    | _ -> assert false (* The lexer should not accept anything else. *)
+  in
+  let v = {
+    hex=f.isHex_FI;
+    intPart=begin match f.integer_FI with Some s -> s | None -> "0" end;
+    fracPart=begin match f.fraction_FI with Some s -> s | None -> "0" end;
+    exp=begin match f.exponent_FI with Some s -> s | None -> "0" end }
+  in
   (v, ty)
 
 let elab_char_constant loc sz cl =
@@ -238,9 +237,9 @@ let elab_constant loc = function
   | CONST_INT s ->
       let (v, ik) = elab_int_constant loc s in
       CInt(v, ik, s)
-  | CONST_FLOAT s ->
-      let (v, fk) = elab_float_constant loc s in
-      CFloat(v, fk, s)
+  | CONST_FLOAT f ->
+      let (v, fk) = elab_float_constant loc f in
+      CFloat(v, fk)
   | CONST_CHAR cl ->
       let (v, ik) = elab_char_constant loc 1 cl in
       CInt(v, ik, "")
@@ -1386,7 +1385,7 @@ let rec elab_init loc env ty ile =
       | (NO_INIT :: ile1) | ([] as ile1) ->
           begin match unroll env ty with
           | TInt _   -> (Init_single (intconst 0L IInt), ile1)
-          | TFloat _ -> (Init_single (floatconst 0.0 FDouble), ile1)
+          | TFloat _ -> (Init_single floatconst0, ile1)
           | TPtr _   -> (Init_single nullconst, ile1)
           | _        -> assert false
           end
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index 424252e7..0820e4e7 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -365,9 +365,8 @@ let letter = ['a'- 'z' 'A'-'Z']
 
 let usuffix = ['u' 'U']
 let lsuffix = "l"|"L"|"ll"|"LL"
-let intsuffix = lsuffix | usuffix | usuffix lsuffix | lsuffix usuffix 
+let intsuffix = lsuffix | usuffix | usuffix lsuffix | lsuffix usuffix
               | usuffix ? "i64"
-                
 
 let hexprefix = '0' ['x' 'X']
 
@@ -375,21 +374,19 @@ let intnum = decdigit+ intsuffix?
 let octnum = '0' octdigit+ intsuffix?
 let hexnum = hexprefix hexdigit+ intsuffix?
 
-let exponent = ['e' 'E']['+' '-']? decdigit+
-let fraction  = '.' decdigit+
-let decfloat = (intnum? fraction)
-	      |(intnum exponent)
-	      |(intnum? fraction exponent)
-	      | (intnum '.') 
-              | (intnum '.' exponent) 
-
-let hexfraction = hexdigit* '.' hexdigit+ | hexdigit+
-let binexponent = ['p' 'P'] ['+' '-']? decdigit+
-let hexfloat = hexprefix hexfraction binexponent
-             | hexprefix hexdigit+   binexponent
-
-let floatsuffix = ['f' 'F' 'l' 'L']
-let floatnum = (decfloat | hexfloat) floatsuffix?
+let floating_suffix = ['f' 'F' 'l' 'L'] as suffix
+let exponent_part = ['e' 'E']((['+' '-']? decdigit+) as expo)
+let fractional_constant = ((decdigit+ as intpart)? '.' (decdigit+ as frac))
+	                 |((decdigit+ as intpart)  '.')
+let decimal_floating_constant =
+   (fractional_constant exponent_part? floating_suffix?)
+  |((decdigit+ as intpart) exponent_part floating_suffix?)
+let binary_exponent_part =  ['p' 'P']((['+' '-']? decdigit+) as expo)
+let hexadecimal_fractional_constant = ((hexdigit+ as intpart)? '.' (hexdigit+ as frac))
+                                     |((hexdigit+ as intpart) '.')
+let hexadecimal_floating_constant =
+   (hexprefix hexadecimal_fractional_constant binary_exponent_part floating_suffix?)
+  |(hexprefix (hexdigit+ as intpart) binary_exponent_part floating_suffix?)
 
 let ident = (letter|'_'|'$')(letter|decdigit|'_'|'$')* 
 let blank = [' ' '\t' '\012' '\r']+
@@ -425,7 +422,20 @@ rule initial =
                                           CST_STRING (str lexbuf, currentLoc lexbuf) }
 |		"L\""			{ (* weimer: wchar_t string literal *)
                                           CST_WSTRING(str lexbuf, currentLoc lexbuf) }
-|		floatnum		{CST_FLOAT (Lexing.lexeme lexbuf, currentLoc lexbuf)}
+|               decimal_floating_constant
+                                        {CST_FLOAT ({Cabs.isHex_FI = false;
+						     Cabs.integer_FI = intpart;
+						     Cabs.fraction_FI = frac;
+						     Cabs.exponent_FI = expo;
+						     Cabs.suffix_FI = suffix},
+                                                    currentLoc lexbuf)}
+|               hexadecimal_floating_constant
+                                        {CST_FLOAT ({Cabs.isHex_FI = true;
+						     Cabs.integer_FI = intpart;
+						     Cabs.fraction_FI = frac;
+						     Cabs.exponent_FI = Some expo;
+						     Cabs.suffix_FI = suffix},
+                                                    currentLoc lexbuf)}
 |		hexnum			{CST_INT (Lexing.lexeme lexbuf, currentLoc lexbuf)}
 |		octnum			{CST_INT (Lexing.lexeme lexbuf, currentLoc lexbuf)}
 |		intnum			{CST_INT (Lexing.lexeme lexbuf, currentLoc lexbuf)}
diff --git a/cparser/Parser.mly b/cparser/Parser.mly
index 0eebb84a..83b1984c 100644
--- a/cparser/Parser.mly
+++ b/cparser/Parser.mly
@@ -199,14 +199,13 @@ let transformOffsetOf (speclist, dtype) member =
   let sizeofType = [SpecType Tunsigned], JUSTBASE in
   let resultExpr = CAST (sizeofType, SINGLE_INIT addrExpr) in
   resultExpr
-
 %}
 
 %token <string * Cabs.cabsloc> IDENT
 %token <int64 list * Cabs.cabsloc> CST_CHAR
 %token <int64 list * Cabs.cabsloc> CST_WCHAR
 %token <string * Cabs.cabsloc> CST_INT
-%token <string * Cabs.cabsloc> CST_FLOAT
+%token <Cabs.floatInfo * Cabs.cabsloc> CST_FLOAT
 %token <string * Cabs.cabsloc> NAMED_TYPE
 
 /* Each character is its own list element, and the terminating nul is not