diff mbox

[Ada] Preparatory work for solving exponentiation problem

Message ID 20150526103154.GA27874@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet May 26, 2015, 10:31 a.m. UTC 
Previously, A**B could give different results for float and
long float depending on whether B was a small static constant
in the range 2..4 or a variable with the same value. Although
both values are valid, this discrepancy is undesirable, both
for general use and in particular for formal analysis by e.g.
codepeer or SPARK.

This checkin is a first step to solving this problem, but it
is not complete yet, corresponding changes in exp_ch4.adb
are required.

So no test yet

Tested on x86_64-pc-linux-gnu, committed on trunk

2015-05-26  Robert Dewar  <dewar@adacore.com>

	* rtsfind.ads: Add entries for RE_Exn[_Long]_Float.
	* s-exnllf.adb (Exn_Float): New function.
	(Exn_Long_Float): New function.
	(Exn_Long_Long_Float): Rewritten interface.
	(Exp): New name for what used to be Exn_Long_Long_Float.
	* s-exnllf.ads (Exn_Float): New function.
	(Exn_Long_Float): New function.
diff mbox

Patch

Index: rtsfind.ads
===================================================================
--- rtsfind.ads	(revision 223661)
+++ rtsfind.ads	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -863,6 +863,8 @@ 
 
      RE_Exn_Integer,                     -- System.Exn_Int
 
+     RE_Exn_Float,                       -- System.Exn_LLF
+     RE_Exn_Long_Float,                  -- System.Exn_LLF
      RE_Exn_Long_Long_Float,             -- System.Exn_LLF
 
      RE_Exn_Long_Long_Integer,           -- System.Exn_LLI
@@ -2098,6 +2100,8 @@ 
 
      RE_Exn_Integer                      => System_Exn_Int,
 
+     RE_Exn_Float                        => System_Exn_LLF,
+     RE_Exn_Long_Float                   => System_Exn_LLF,
      RE_Exn_Long_Long_Float              => System_Exn_LLF,
 
      RE_Exn_Long_Long_Integer            => System_Exn_LLI,
Index: s-exnllf.adb
===================================================================
--- s-exnllf.adb	(revision 223661)
+++ s-exnllf.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -29,8 +29,76 @@ 
 --                                                                          --
 ------------------------------------------------------------------------------
 
+--  Note: the reason for treating exponents in the range 0 .. 4 specially is
+--  to ensure identical results to the static inline expansion in the case of
+--  a compile time known exponent in this range. The use of Float'Machine and
+--  Long_Float'Machine is to avoid unwanted extra precision in the results.
+
 package body System.Exn_LLF is
 
+   function Exp
+     (Left  : Long_Long_Float;
+      Right : Integer) return Long_Long_Float;
+   --  Common routine used if Right not in 0 .. 4
+
+   ---------------
+   -- Exn_Float --
+   ---------------
+
+   function Exn_Float
+     (Left  : Float;
+      Right : Integer) return Float
+   is
+      Temp : Float;
+   begin
+      case Right is
+         when 0 =>
+            return 1.0;
+         when 1 =>
+            return Left;
+         when 2 =>
+            return Float'Machine (Left * Left);
+         when 3 =>
+            return Float'Machine (Left * Left * Left);
+         when 4 =>
+            Temp := Float'Machine (Left * Left);
+            return Float'Machine (Temp * Temp);
+         when others =>
+            return
+              Float'Machine
+                (Float (Exp (Long_Long_Float (Left), Right)));
+      end case;
+   end Exn_Float;
+
+   --------------------
+   -- Exn_Long_Float --
+   --------------------
+
+   function Exn_Long_Float
+     (Left  : Long_Float;
+      Right : Integer) return Long_Float
+   is
+      Temp : Long_Float;
+   begin
+      case Right is
+         when 0 =>
+            return 1.0;
+         when 1 =>
+            return Left;
+         when 2 =>
+            return Long_Float'Machine (Left * Left);
+         when 3 =>
+            return Long_Float'Machine (Left * Left * Left);
+         when 4 =>
+            Temp := Long_Float'Machine (Left * Left);
+            return Long_Float'Machine (Temp * Temp);
+         when others =>
+            return
+              Long_Float'Machine
+                (Long_Float (Exp (Long_Long_Float (Left), Right)));
+      end case;
+   end Exn_Long_Float;
+
    -------------------------
    -- Exn_Long_Long_Float --
    -------------------------
@@ -39,6 +107,33 @@ 
      (Left  : Long_Long_Float;
       Right : Integer) return Long_Long_Float
    is
+      Temp : Long_Long_Float;
+   begin
+      case Right is
+         when 0 =>
+            return 1.0;
+         when 1 =>
+            return Left;
+         when 2 =>
+            return Left * Left;
+         when 3 =>
+            return Left * Left * Left;
+         when 4 =>
+            Temp := Left * Left;
+            return Temp * Temp;
+         when others =>
+            return Exp (Left, Right);
+      end case;
+   end Exn_Long_Long_Float;
+
+   ---------
+   -- Exp --
+   ---------
+
+   function Exp
+     (Left  : Long_Long_Float;
+      Right : Integer) return Long_Long_Float
+   is
       Result : Long_Long_Float := 1.0;
       Factor : Long_Long_Float := Left;
       Exp    : Integer := Right;
@@ -91,6 +186,6 @@ 
             return 1.0 / Result;
          end;
       end if;
-   end Exn_Long_Long_Float;
+   end Exp;
 
 end System.Exn_LLF;
Index: s-exnllf.ads
===================================================================
--- s-exnllf.ads	(revision 223661)
+++ s-exnllf.ads	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -29,11 +29,19 @@ 
 --                                                                          --
 ------------------------------------------------------------------------------
 
---  Long_Long_Float exponentiation (checks off)
+--  [Long_[Long_]]Float exponentiation (checks off)
 
 package System.Exn_LLF is
    pragma Pure;
 
+   function Exn_Float
+     (Left  : Float;
+      Right : Integer) return Float;
+
+   function Exn_Long_Float
+     (Left  : Long_Float;
+      Right : Integer) return Long_Float;
+
    function Exn_Long_Long_Float
      (Left  : Long_Long_Float;
       Right : Integer) return Long_Long_Float;