[Ada] Preparatory work for solving exponentiation problem
Arnaud Charlet
charlet@adacore.com
Tue May 26 10:35:00 GMT 2015
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.
-------------- next part --------------
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;
More information about the Gcc-patches
mailing list