dik@cwi.nl (Dik T. Winter) (03/05/88)
Attached you will find a program that will verify the correctness of
the values returned by floating point type attributes. This program
was written within the framework of the Ada Europe Numerics Working
Group, and I thank the group members for there input and advise.
Attributes are crucial when an attempt is made to write a portable
problem. And it is, of course, essential that the values returned
are correct. But even with my current, limited, knowledge I know
that for every floating point type attribute there is at least one
compiler system that returns the wrong value! And only a minority (2)
of the compiler systems tested so far (9) return (apparently) correct
values in all cases. But I know from other sources that one of these
2 compilers gives wrong results in a number of other cases, and the
other compiler gives wrong results when a port to a different machine
is used.
It is clear that a program for the verification of the attributes
would be appropriate in the validation suite. The problem is that
validation programs should be portable to all machines and compilers,
however weird they are. But this program relies on some properties
of the hardware, and I do not know of a method to avoid this.
The most important property this program requires is that multiplication
of a positive floating point number by the machine radix either yields
an overflown result (which might have exponent wrap-around) or the
correct result. I know of at least one binary machine where multiplication
of a floating point number by two might loose precision (though there is
not yet an Ada compiler on it). So this program will fail on that
machine without any doubt.
As it is not feasible to put this program in the validation suite, I
intend to have this program put to as wide a public as possible.
I would appreciate if you, when you compile and execute this program,
would mail the results to me. My addresses are in the header page
of the output. Also feel free to communicate any problems or errors
you encounter with the program, so that I am able to adjust the program
accordingly (no program is perfect).
dik t. winter, cwi, amsterdam, nederland
Internet: dik@cwi.nl
Bitnet : dik@mcvax (this is a nickname, do NOT use hamcwi6, it will fail)
UUCP : ....uunet!dik@cwi.nl (or something like that)
------------
-- AENWG 15.8
-- Copyright (C) 1988 Dik T. Winter, CWI, Amsterdam
-- This program may be freely distributed, but not be sold.
--
-- Verify-attributes version 1.3
--
-- To adjust to the true type to be tested see the program at the end.
-- This implementation tests FLOAT.
generic
USER_DEFINED : BOOLEAN;
type FLOAT_TYPE is digits <>;
procedure VERIFY_ATTRIBUTES;
with TEXT_IO;
use TEXT_IO;
procedure VERIFY_ATTRIBUTES is
--
-- This procedure is intended to verify the attributes of floating-
-- point types. First the machine characteristics are determined.
-- This is done according to an algorithm due to M. Malcolm,
-- CACM 15 (1972), pp. 949-951, incorporating some improvements
-- suggested by M. Gentleman and S. Marovich, CACM 17 (1974),
-- pp. 276-277. The version given here forces storing of intermediate
-- results to memory using tasks. Even if procedures are used to
-- do this the compiler might optimise it away; it is difficult to
-- see how a compiler might optimise the tasks away. Forced storing
-- into memory is needed on machines where the register size exceeds
-- memory word size. For part implementations of Ada not having tasks
-- they might be elided, unless long registers are used. In the last
-- case there is (apparently) no possibility to obtain the true values.
--
-- After the machine characteristics are calculated the attributes of
-- the floating-point type given are verified (including model
-- arithmetic but the last only in part).
--
-- History:
--
-- Version 1.0: June 6, 1987, original version.
-- Distributed as AENWG 13.9
--
-- Version 1.1: October 1, 1987.
-- Distributed as AENWG 14.2
-- Corrects:
-- Output format
-- Check for rounding
-- Calculation of improved SAFE_EMAX
--
-- Version 1.2: December, 1987.
-- Corrects:
-- Calculation of SAFE_EMAX if attribute too large
-- Some minor corrections
-- Check attributes for user defined types
--
-- Version 1.3: February 16, 1988.
-- Distributed as AENWG 15.8
-- Distributed through INFO-ADA mailing list and Usenet
-- comp.lang.ada newsgroup
-- Enhanced:
-- Allows for floating point implementation where
-- overflow results in wrap-around
--
-- Author: Dik T. Winter,
-- Centrum voor Wiskunde en Informatica,
-- Amsterdam
--
-- Users of this version are kindly requested to send (preferably by
-- e-mail) the output to the author, after filling in the blanks.
--
package FLOAT_IO is new TEXT_IO.FLOAT_IO (FLOAT_TYPE);
package INTEGER_IO is new TEXT_IO.INTEGER_IO (INTEGER);
use FLOAT_IO, INTEGER_IO;
ERRORS : BOOLEAN := FALSE;
FATAL_ERRORS : BOOLEAN := FALSE;
OVERFLOW_ERROR : INTEGER := 0;
ATT_DIGITS : INTEGER;
MAX_DIGITS : INTEGER;
MANTISSA : INTEGER;
EPSILON : FLOAT_TYPE;
EMAX : INTEGER;
REQUIRED_EMAX : INTEGER;
SMALL : FLOAT_TYPE;
LARGE : FLOAT_TYPE;
SAFE_DIGITS : INTEGER;
SAFE_EMAX : INTEGER;
SAFE_V_EMAX : INTEGER;
SAFE_SMALL : FLOAT_TYPE;
SAFE_V_SMALL : FLOAT_TYPE;
SAFE_SMALL_1 : FLOAT_TYPE;
SAFE_LARGE : FLOAT_TYPE;
SAFE_V_LARGE : FLOAT_TYPE;
SAFE_VERY_EMAX : INTEGER;
SAFE_VERY_EMIN : INTEGER;
SAFE_VERY_SMALL : FLOAT_TYPE;
SAFE_VERY_LARGE : FLOAT_TYPE;
MAX_MANTISSA : INTEGER;
MACHINE_RADIX : INTEGER;
MACHINE_MANTISSA : INTEGER;
MACHINE_ROUNDS : BOOLEAN;
MACHINE_EMAX : INTEGER;
MACHINE_EMIN : INTEGER;
MACHINE_VERY_EMIN : INTEGER;
MACHINE_LARGE : FLOAT_TYPE;
MACHINE_SMALL : FLOAT_TYPE;
MACHINE_VERY_SMALL : FLOAT_TYPE;
MACHINE_OVERFLOWS : BOOLEAN;
BIT_MULTIPLIER : INTEGER;
REQUIRED_MANTISSA : INTEGER;
-- temporaries
A : FLOAT_TYPE;
B : FLOAT_TYPE;
BETA : FLOAT_TYPE;
BETAM1 : FLOAT_TYPE;
BETAINV : FLOAT_TYPE;
C : FLOAT_TYPE;
C_PLUS : FLOAT_TYPE;
C_MINUS : FLOAT_TYPE;
D : FLOAT_TYPE;
E : FLOAT_TYPE;
K : INTEGER;
MODEL_ONEMINUSEPS : FLOAT_TYPE;
ONEMINUSEPS : FLOAT_TYPE;
SAFE_MODEL_ONEMINUSEPS : FLOAT_TYPE;
-- the following constant should work up to digits 100 at least
DIGITS_MULTIPLIER : constant := 3.32193;
-- force storing in memory
-- if the Ada implementation under investigation does not implement
-- tasks, this task may be omitted and the procedure hereafter
-- has to be changed.
task USE_MEMORY is
entry STORE (F : FLOAT_TYPE);
entry FETCH (F : out FLOAT_TYPE);
end USE_MEMORY;
task body USE_MEMORY is
MEMORY : FLOAT_TYPE;
begin
loop
select
accept STORE (F : FLOAT_TYPE) do
MEMORY := F;
end STORE;
or
accept FETCH (F : out FLOAT_TYPE) do
F := MEMORY;
end FETCH;
or
terminate;
end select;
end loop;
end USE_MEMORY;
-- if the task is omitted the body should be changed to the
-- single statement:
-- return F;
-- However, an optimizing compiler might optimize it away.
--
function THROUGH_MEMORY (F : FLOAT_TYPE) return FLOAT_TYPE is
FF : FLOAT_TYPE;
begin
USE_MEMORY.STORE (F);
USE_MEMORY.FETCH (FF);
return FF;
end THROUGH_MEMORY;
-- output floating point number. format is first with hexadecimal
-- mantissa and base MACHINE_RADIX exponent, followed by decimal
-- format. if the latter gives *EXCEPTION* an error might be present
-- in the standard output routines.
procedure PUT_FLOAT (F : FLOAT_TYPE) is
EXP : INTEGER;
MANT : FLOAT_TYPE;
SYMBOLS : STRING (1 .. 16) := "0123456789abcdef";
DIG : INTEGER;
ACCU : INTEGER := 0;
BITS_IN_ACCU : INTEGER := 0;
FACTOR : INTEGER := 1;
begin
MANT := abs F;
EXP := 0;
if F < 0.0 then
PUT ("-");
end if;
if F = 0.0 then
PUT ("0.0");
else
while MANT >= 1.0 loop
MANT := MANT * BETAINV;
EXP := EXP + 1;
end loop;
while MANT < BETAINV loop
MANT := MANT * BETA;
EXP := EXP - 1;
end loop;
if MANT = BETAINV then
-- take care for machines with inexact comparison.
declare
A, B : FLOAT_TYPE;
begin
A := MANT * BETA;
B := A - 0.5;
if B /= 0.5 then
-- comparison is inexact
EXP := EXP + 1;
MANT := A;
end if;
end;
end if;
PUT ("16#0.");
while MANT /= 0.0 loop
MANT := MANT * BETA;
DIG := INTEGER (MANT);
if FLOAT_TYPE (DIG) > MANT then
DIG := DIG - 1;
end if;
if DIG >= MACHINE_RADIX then
DIG := MACHINE_RADIX - 1;
end if;
ACCU := ACCU * MACHINE_RADIX + DIG;
BITS_IN_ACCU := BITS_IN_ACCU + BIT_MULTIPLIER;
FACTOR := FACTOR * MACHINE_RADIX;
MANT := MANT - FLOAT_TYPE (DIG);
if BITS_IN_ACCU >= 4 then
FACTOR := FACTOR / 16;
DIG := ACCU / FACTOR;
ACCU := ACCU - DIG * FACTOR;
BITS_IN_ACCU := BITS_IN_ACCU - 4;
PUT (SYMBOLS (DIG + 1));
end if;
end loop;
if ACCU /= 0 then
for I in BITS_IN_ACCU + 1 .. 4 loop
ACCU := ACCU * 2;
end loop;
PUT (SYMBOLS (ACCU + 1));
end if;
PUT ("#*");
PUT (MACHINE_RADIX, 0);
PUT ("**");
PUT (EXP, 0);
end if;
PUT (" (");
begin
PUT (F);
exception
when others =>
PUT ("*EXCEPTION*");
end;
PUT (")");
end PUT_FLOAT;
function MULTIPLIER (RADIX : INTEGER) return INTEGER is
-- Given RADIX return the number of bits in radix
L_RADIX : INTEGER := RADIX;
O_RADIX : INTEGER;
VALUE : INTEGER := 0;
begin
case RADIX is
when 2 => return 1;
when 4 => return 2;
when 8 => return 3;
when 16 => return 4;
when others =>
loop
O_RADIX := L_RADIX;
L_RADIX := L_RADIX / 2;
exit when L_RADIX * 2 /= O_RADIX;
VALUE := VALUE + 1;
if L_RADIX = 1 then
return VALUE;
end if;
end loop;
PUT ("Something weird is happening, the machine radix is not a");
NEW_LINE;
PUT ("power of 2. This might play havoc with model arithmetic");
NEW_LINE;
PUT ("We must be very careful there.");
NEW_LINE;
return 0;
end case;
end MULTIPLIER;
begin
NEW_PAGE;
-- determine MACHINE_RADIX
-- first multiply A by 2 until miltiplication is inexact when 1 is
-- added to it (i.e. A becomes the smallest power of two such that
-- addition of 1 is thrown away).
A := 1.0;
while (THROUGH_MEMORY (A + 1.0) - A) - 1.0 = 0.0 loop
A := A + A;
end loop;
-- find the smallest power of 2 (B) such that addition of B to A
-- increases A.
B := 1.0;
while THROUGH_MEMORY (A + B) - A = 0.0 loop
B := B + B;
end loop;
MACHINE_RADIX := INTEGER (THROUGH_MEMORY (A + B) - A);
BIT_MULTIPLIER := MULTIPLIER (MACHINE_RADIX);
-- determine MACHINE_MANTISSA
BETA := FLOAT_TYPE (MACHINE_RADIX);
BETAINV := 1.0 / BETA;
BETAM1 := BETA - 1.0;
MACHINE_MANTISSA := 0;
B := 1.0;
while (THROUGH_MEMORY (B + 1.0) - B) - 1.0 = 0.0 loop
B := B * BETA;
MACHINE_MANTISSA := MACHINE_MANTISSA + 1;
end loop;
-- determine MACHINE_ROUNDS
-- we can get away with division by two because MACHINE_RADIX has to
-- be even (even a power of 2).
E := B;
C := BETA * 0.5;
D := BETA;
for I in 1 .. MACHINE_MANTISSA loop
D := D * BETAINV;
end loop;
-- C is half the difference of B and the next higher number; C + D is the
-- number next above C while C - D is the number next below D.
-- we cannot check rounding with C itself, because this may round either
-- way.
C_PLUS := C + D;
C_MINUS := C - D;
-- if MACHINE_RADIX is 2 we can stuff one more bit in C_MINUS
if MACHINE_RADIX = 2 then
C_MINUS := C_MINUS + D * 0.5;
end if;
MACHINE_ROUNDS := FALSE;
if THROUGH_MEMORY (E + C_PLUS) - E /= 0.0 then
MACHINE_ROUNDS := TRUE;
end if;
if THROUGH_MEMORY (E + C_MINUS) - E /= 0.0 then
MACHINE_ROUNDS := FALSE;
end if;
-- determine MACHINE_LARGE, MACHINE_SMALL, MACHINE_VERY_SMALL,
-- MACHINE_EMAX, MACHINE_EMIN and MACHINE_VERY_EMIN.
-- MACHINE_SMALL (and the associated MACHINE_EMIN) is the
-- smallest hardware number with full precision, numbers
-- between MACHINE_VERY_SMALL and MACHINE_SMALL have less
-- precision (gradual underflow).
ONEMINUSEPS := 0.0;
A := BETAM1;
for I in 1 .. MACHINE_MANTISSA loop
A := A * BETAINV;
ONEMINUSEPS := ONEMINUSEPS + A;
end loop;
A := ONEMINUSEPS;
MACHINE_EMAX := 0;
MACHINE_OVERFLOWS := FALSE;
loop
begin
MACHINE_LARGE := A;
A := THROUGH_MEMORY (A * BETA);
exit when A * BETAINV /= MACHINE_LARGE or A <= MACHINE_LARGE;
MACHINE_EMAX := MACHINE_EMAX + 1;
exception
when NUMERIC_ERROR =>
MACHINE_OVERFLOWS := TRUE;
exit;
when CONSTRAINT_ERROR =>
PUT ("Overflow raises CONSTRAINT_ERROR.");
ERRORS := TRUE;
NEW_LINE;
MACHINE_OVERFLOWS := TRUE;
exit;
when others =>
PUT ("Catching overflow but it was not NUMERIC_ERROR that was raised.");
NEW_LINE;
ERRORS := TRUE;
MACHINE_OVERFLOWS := TRUE;
exit;
end;
end loop;
MACHINE_EMIN := 0;
A := ONEMINUSEPS;
MACHINE_SMALL := BETAINV;
loop
begin
B := A;
A := THROUGH_MEMORY (A * BETAINV);
exit when A * BETA /= B;
MACHINE_EMIN := MACHINE_EMIN - 1;
MACHINE_SMALL := MACHINE_SMALL * BETAINV;
exception
when others =>
PUT ("Apparently underflow raises an (illegal) exception.");
NEW_LINE;
ERRORS := TRUE;
exit;
end;
end loop;
A := MACHINE_SMALL;
MACHINE_VERY_EMIN := MACHINE_EMIN;
loop
begin
MACHINE_VERY_SMALL := A;
A := THROUGH_MEMORY (A * BETAINV);
exit when A >= MACHINE_VERY_SMALL or A = 0.0;
MACHINE_VERY_EMIN := MACHINE_VERY_EMIN - 1;
exception
when others =>
PUT ("Apparently underflow raises an (illegal) exception.");
NEW_LINE;
ERRORS := TRUE;
exit;
end;
end loop;
-- Now we have the machine characteristics and can compare to the
-- attributes. First with the MACHINE attributes.
PUT ("MACHINE_RADIX is ");
PUT (MACHINE_RADIX, 0);
if FLOAT_TYPE'MACHINE_RADIX /= MACHINE_RADIX then
PUT (" but the attribute gives ");
PUT (FLOAT_TYPE'MACHINE_RADIX, 0);
ERRORS := TRUE;
end if;
NEW_LINE;
PUT ("MACHINE_MANTISSA is ");
PUT (MACHINE_MANTISSA, 0);
if FLOAT_TYPE'MACHINE_MANTISSA /= MACHINE_MANTISSA then
PUT (" but the attribute gives ");
PUT (FLOAT_TYPE'MACHINE_MANTISSA, 0);
ERRORS := TRUE;
if MULTIPLIER (FLOAT_TYPE'MACHINE_RADIX) *
FLOAT_TYPE'MACHINE_MANTISSA =
BIT_MULTIPLIER * MACHINE_MANTISSA then
NEW_LINE;
PUT ("But it fits with the wrong value of MACHINE_RADIX");
end if;
end if;
NEW_LINE;
PUT ("MACHINE_EMAX is ");
PUT (MACHINE_EMAX, 0);
if FLOAT_TYPE'MACHINE_EMAX /= MACHINE_EMAX then
PUT (" but the attribute gives ");
PUT (FLOAT_TYPE'MACHINE_EMAX, 0);
ERRORS := TRUE;
end if;
NEW_LINE;
PUT ("MACHINE_EMIN is ");
PUT (MACHINE_EMIN, 0);
if FLOAT_TYPE'MACHINE_EMIN /= MACHINE_VERY_EMIN then
if FLOAT_TYPE'MACHINE_EMIN /= MACHINE_EMIN then
PUT (" but the attribute gives ");
PUT (FLOAT_TYPE'MACHINE_EMIN, 0);
ERRORS := TRUE;
else
PUT (" apparently not the smallest number was used;");
NEW_LINE;
PUT (" as the attribute gives ");
PUT (FLOAT_TYPE'MACHINE_EMIN, 0);
end if;
end if;
NEW_LINE;
-- Give also pseudo attributes
if MACHINE_EMIN /= MACHINE_VERY_EMIN then
PUT ("'MACHINE_VERY_EMIN' is ");
PUT (MACHINE_VERY_EMIN, 0);
NEW_LINE;
end if;
PUT ("'MACHINE_LARGE' is ");
PUT_FLOAT (MACHINE_LARGE);
NEW_LINE;
PUT ("'MACHINE_SMALL' is ");
PUT_FLOAT (MACHINE_SMALL);
NEW_LINE;
if MACHINE_SMALL /= MACHINE_VERY_SMALL then
PUT ("'MACHINE_VERY_SMALL' is ");
PUT_FLOAT (MACHINE_VERY_SMALL);
NEW_LINE;
end if;
PUT ("MACHINE_ROUNDS is ");
if MACHINE_ROUNDS then
PUT ("TRUE");
else
PUT ("FALSE");
end if;
if MACHINE_ROUNDS /= FLOAT_TYPE'MACHINE_ROUNDS then
-- rounding is not properly defined, does it mean the nearest
-- harware number?
PUT (" but the attribute does not agree");
NEW_LINE;
if MACHINE_ROUNDS then
PUT ("probably not checked thoroughly enough.");
else
PUT ("(another interpretation?).");
if THROUGH_MEMORY (E + C_PLUS) - E = 0.0 then
NEW_LINE;
PUT_FLOAT (E);
PUT (" + ");
PUT_FLOAT (C_PLUS);
PUT (" = ");
NEW_LINE;
PUT (" ");
PUT_FLOAT (E);
NEW_LINE;
PUT ("should be ");
PUT_FLOAT (E + BETA);
end if;
if THROUGH_MEMORY (E + C_MINUS) - E /= 0.0 then
NEW_LINE;
PUT_FLOAT (E);
PUT (" + ");
PUT_FLOAT (C_MINUS);
PUT (" = ");
NEW_LINE;
PUT (" ");
PUT_FLOAT (E + C_MINUS);
NEW_LINE;
PUT ("should be ");
PUT_FLOAT (E);
end if;
end if;
end if;
NEW_LINE;
PUT ("MACHINE_OVERFLOWS is ");
if MACHINE_OVERFLOWS then
PUT ("TRUE");
else
PUT ("FALSE");
end if;
if MACHINE_OVERFLOWS /= FLOAT_TYPE'MACHINE_OVERFLOWS then
if MACHINE_OVERFLOWS then
-- might have that the system uses the strict interpretation of
-- MACHINE_OVERFLOWS and hence is not allowed to return FALSE.
PUT (" the attribute says no, perhaps a stricter interpretation.");
else
PUT (" the attribute says yes; clearly wrong.");
ERRORS := TRUE;
end if;
end if;
NEW_LINE;
-- Now check the other attributes
-- Cater for wobbling precision
MAX_MANTISSA := (MACHINE_MANTISSA - 1) * BIT_MULTIPLIER + 1;
ATT_DIGITS := FLOAT_TYPE'DIGITS;
A := FLOAT_TYPE (ATT_DIGITS) * DIGITS_MULTIPLIER + 1.0;
REQUIRED_MANTISSA := INTEGER (A);
if FLOAT_TYPE (REQUIRED_MANTISSA) < A then
REQUIRED_MANTISSA := REQUIRED_MANTISSA + 1;
end if;
MANTISSA := REQUIRED_MANTISSA;
REQUIRED_EMAX := REQUIRED_MANTISSA * 4;
EMAX := REQUIRED_EMAX;
MAX_DIGITS := ATT_DIGITS;
PUT ("DIGITS gives ");
PUT (ATT_DIGITS, 0);
NEW_LINE;
-- check egainst MACHINE_MANTISSA
if REQUIRED_MANTISSA > MAX_MANTISSA then
if BIT_MULTIPLIER /= 0 then
PUT ("The mantissa requirements are more than the hardware gives;");
NEW_LINE;
ERRORS := TRUE;
FATAL_ERRORS := TRUE;
while REQUIRED_MANTISSA > MAX_MANTISSA loop
MAX_DIGITS := MAX_DIGITS - 1;
A := FLOAT_TYPE (MAX_DIGITS) * DIGITS_MULTIPLIER + 1.0;
REQUIRED_MANTISSA := INTEGER (A);
if FLOAT_TYPE (REQUIRED_MANTISSA) < A then
REQUIRED_MANTISSA := REQUIRED_MANTISSA + 1;
end if;
end loop;
REQUIRED_EMAX := REQUIRED_MANTISSA * 4;
else
PUT ("This cannot be verified.");
NEW_LINE;
end if;
elsif REQUIRED_MANTISSA < MAX_MANTISSA then
-- MACHINE_MANTISSA would probably allow more
A := FLOAT_TYPE (ATT_DIGITS + 1) * DIGITS_MULTIPLIER + 1.0;
K := INTEGER (A);
if FLOAT_TYPE (K) < A then
K := K + 1;
end if;
if K <= MAX_MANTISSA then
PUT ("Apparently DIGITS is limited by declaration or due to exponent");
PUT (" limitations.");
NEW_LINE;
end if;
end if;
-- check against exponent range
if REQUIRED_EMAX > MACHINE_EMAX * BIT_MULTIPLIER or
REQUIRED_EMAX > -MACHINE_EMIN * BIT_MULTIPLIER then
if BIT_MULTIPLIER /= 0 then
ERRORS := TRUE;
FATAL_ERRORS := TRUE;
PUT ("The exponent requirements are more than the hardware gives.");
NEW_LINE;
if MAX_DIGITS /= ATT_DIGITS then
PUT ("Even after adjustment for mantissa limitations!");
NEW_LINE;
end if;
while REQUIRED_EMAX > MACHINE_EMAX * BIT_MULTIPLIER or
REQUIRED_EMAX > -MACHINE_EMIN * BIT_MULTIPLIER loop
MAX_DIGITS := MAX_DIGITS - 1;
A := FLOAT_TYPE (MAX_DIGITS) * DIGITS_MULTIPLIER + 1.0;
REQUIRED_MANTISSA := INTEGER (A);
if FLOAT_TYPE (REQUIRED_MANTISSA) < A then
REQUIRED_MANTISSA := REQUIRED_MANTISSA + 1;
end if;
REQUIRED_EMAX := REQUIRED_MANTISSA * 4;
end loop;
end if;
end if;
if ATT_DIGITS /= MAX_DIGITS then
-- this is what the hardware allows
PUT ("DIGITS should not be larger than ");
PUT (MAX_DIGITS, 0);
NEW_LINE;
end if;
PUT ("MANTISSA is ");
PUT (MANTISSA, 0);
if ATT_DIGITS /= MAX_DIGITS then
PUT (" but with proper DIGITS value it is ");
PUT (REQUIRED_MANTISSA, 0);
end if;
if FLOAT_TYPE'MANTISSA /= MANTISSA then
ERRORS := TRUE;
FATAL_ERRORS := TRUE;
PUT (" the attribute gives ");
PUT (FLOAT_TYPE'MANTISSA, 0);
if FLOAT_TYPE'MANTISSA = REQUIRED_MANTISSA then
PUT (" that fits the proper value of DIGITS!");
end if;
MANTISSA := FLOAT_TYPE'MANTISSA;
EMAX := MANTISSA * 4;
end if;
NEW_LINE;
PUT ("EMAX is ");
PUT (REQUIRED_EMAX, 0);
if REQUIRED_EMAX /= FLOAT_TYPE'EMAX then
ERRORS := TRUE;
FATAL_ERRORS := TRUE;
PUT (" the attribute gives ");
PUT (FLOAT_TYPE'EMAX, 0);
if EMAX = FLOAT_TYPE'EMAX then
PUT ("; that fits other attributes.");
end if;
end if;
NEW_LINE;
if FATAL_ERRORS then
PUT ("Due to the preceeding errors the remainder may be faulty");
NEW_LINE;
PUT ("when comparing to attributes.");
NEW_LINE;
PUT ("This is because the attributes might match earlier wrong");
NEW_LINE;
PUT ("attributes.");
NEW_LINE;
MANTISSA := REQUIRED_MANTISSA;
EMAX := REQUIRED_EMAX;
ATT_DIGITS := MAX_DIGITS;
end if;
-- now calculate LARGE and SMALL
-- (cross your fingers you will not get exceptions here.)
MODEL_ONEMINUSEPS := 0.0;
A := 1.0;
for I in 1 .. MANTISSA loop
A := A * 0.5;
MODEL_ONEMINUSEPS := MODEL_ONEMINUSEPS + A;
end loop;
LARGE := MODEL_ONEMINUSEPS;
for I in 1 .. EMAX loop
LARGE := LARGE * 2.0;
end loop;
PUT ("LARGE is ");
PUT_FLOAT (LARGE);
if LARGE /= FLOAT_TYPE'LARGE then
PUT (" but the attribute gives ");
PUT_FLOAT (FLOAT_TYPE'LARGE);
ERRORS := TRUE;
end if;
NEW_LINE;
SMALL := 0.5;
for I in 1 .. EMAX loop
SMALL := SMALL * 0.5;
end loop;
PUT ("SMALL is ");
PUT_FLOAT (SMALL);
if SMALL /= FLOAT_TYPE'SMALL then
PUT (" but the attribute gives ");
PUT_FLOAT (FLOAT_TYPE'SMALL);
ERRORS := TRUE;
end if;
NEW_LINE;
EPSILON := 1.0;
for I in 2 .. MANTISSA loop
EPSILON := EPSILON * 0.5;
end loop;
PUT ("EPSILON is ");
PUT_FLOAT (EPSILON);
if EPSILON /= FLOAT_TYPE'EPSILON then
PUT (" but the attribute gives ");
PUT_FLOAT (FLOAT_TYPE'EPSILON);
ERRORS := TRUE;
end if;
NEW_LINE;
-- SAFE_DIGITS should be FLOAT_TYPE'BASE'DIGITS
-- Assume either a predefined type or a user defined type of the form
-- type USER_TYPE is digits <N>;
SAFE_DIGITS := FLOAT_TYPE'BASE'DIGITS;
if SAFE_DIGITS /= ATT_DIGITS then
if not USER_DEFINED then
PUT ("Although this is a predefined type, the attributes of the");
NEW_LINE;
PUT ("base type do not match!");
NEW_LINE;
ERRORS := TRUE;
end if;
SAFE_MODEL_ONEMINUSEPS := 0.0;
A := 1.0;
for I in 1 .. FLOAT_TYPE'BASE'MANTISSA loop
A := A * 0.5;
SAFE_MODEL_ONEMINUSEPS := SAFE_MODEL_ONEMINUSEPS + A;
end loop;
else
SAFE_MODEL_ONEMINUSEPS := MODEL_ONEMINUSEPS;
if USER_DEFINED then
PUT ("Although this is a user defined type, the attributes of the");
NEW_LINE;
PUT ("base type appear to match the attributes of this type.");
NEW_LINE;
PUT ("Probably there is a predefined type with the specified number");
PUT (" of digits.");
NEW_LINE;
PUT ("But it is more likely that the system is wrong.");
NEW_LINE;
ERRORS := TRUE;
end if;
end if;
SAFE_EMAX := FLOAT_TYPE'SAFE_EMAX;
PUT ("SAFE_EMAX gives ");
PUT (SAFE_EMAX, 0);
-- checking SAFE attributes; note: the range must be symmetric!
SAFE_LARGE := SAFE_MODEL_ONEMINUSEPS;
SAFE_SMALL_1 := SAFE_MODEL_ONEMINUSEPS;
for I in 1 .. SAFE_EMAX loop
begin
A := THROUGH_MEMORY (SAFE_LARGE * 2.0);
B := THROUGH_MEMORY (SAFE_SMALL_1 * 0.5);
if SAFE_LARGE * 2.0 /= A or SAFE_SMALL_1 * 0.5 /= B then
PUT (" detected lack of model arithmetic within given range.");
NEW_LINE;
PUT ("SAFE_EMAX has been adjusted to ");
SAFE_EMAX := I - 1;
PUT (SAFE_EMAX, 0);
ERRORS := TRUE;
exit;
end if;
SAFE_LARGE := A;
SAFE_SMALL_1 := B;
exception
when NUMERIC_ERROR =>
PUT (" caught NUMERIC_ERROR during verification.");
NEW_LINE;
PUT ("SAFE_EMAX has been adjusted to ");
SAFE_EMAX := I - 1;
PUT (SAFE_EMAX, 0);
ERRORS := TRUE;
exit;
when CONSTRAINT_ERROR =>
PUT (" caught CONSTRAINT_ERROR during verification.");
NEW_LINE;
PUT ("SAFE_EMAX has been adjusted to ");
SAFE_EMAX := I - 1;
PUT (SAFE_EMAX, 0);
ERRORS := TRUE;
exit;
when others =>
PUT (" caught some strange exception during verification.");
NEW_LINE;
PUT ("SAFE_EMAX has been adjusted to ");
SAFE_EMAX := I - 1;
PUT (SAFE_EMAX, 0);
ERRORS := TRUE;
exit;
end;
end loop;
NEW_LINE;
SAFE_SMALL := 0.5;
for I in 1 .. SAFE_EMAX loop
SAFE_SMALL := SAFE_SMALL * 0.5;
end loop;
PUT ("SAFE_LARGE is ");
PUT_FLOAT (SAFE_LARGE);
if SAFE_LARGE /= FLOAT_TYPE'SAFE_LARGE then
PUT (" the attribute gives ");
PUT_FLOAT (FLOAT_TYPE'SAFE_LARGE);
ERRORS := TRUE;
end if;
NEW_LINE;
PUT ("SAFE_SMALL is ");
PUT_FLOAT (SAFE_SMALL);
if SAFE_SMALL /= FLOAT_TYPE'SAFE_SMALL then
PUT (" the attribute gives ");
PUT_FLOAT (FLOAT_TYPE'SAFE_SMALL);
ERRORS := TRUE;
end if;
NEW_LINE;
if FLOAT_TYPE'SAFE_EMAX /= FLOAT_TYPE'BASE'SAFE_EMAX or
FLOAT_TYPE'SAFE_LARGE /= FLOAT_TYPE'BASE'SAFE_LARGE or
FLOAT_TYPE'SAFE_SMALL /= FLOAT_TYPE'BASE'SAFE_SMALL then
PUT ("SAFE_EMAX, SAFE_LARGE and/or SAFE_SMALL does not match the");
NEW_LINE;
PUT ("corresponding attribute of the base type.");
NEW_LINE;
ERRORS := TRUE;
end if;
SAFE_V_LARGE := SAFE_LARGE;
SAFE_V_SMALL := SAFE_SMALL;
SAFE_V_EMAX := SAFE_EMAX;
if SAFE_EMAX = FLOAT_TYPE'SAFE_EMAX then
A := SAFE_LARGE;
B := SAFE_SMALL_1;
loop
begin
SAFE_V_LARGE := A;
SAFE_SMALL_1 := B;
A := THROUGH_MEMORY (A * 2.0);
B := THROUGH_MEMORY (B * 0.5);
exit when A * 0.5 /= SAFE_V_LARGE or B * 2.0 /= SAFE_SMALL_1;
SAFE_V_EMAX := SAFE_V_EMAX + 1;
SAFE_V_SMALL := SAFE_V_SMALL * 0.5;
exception
when NUMERIC_ERROR =>
exit;
when CONSTRAINT_ERROR =>
PUT ("Caught unexpected CONSTRAINT_ERROR.");
NEW_LINE;
exit;
when others =>
PUT ("Caught some strange exception.");
NEW_LINE;
ERRORS := TRUE;
exit;
end;
end loop;
if SAFE_V_EMAX /= FLOAT_TYPE'SAFE_EMAX then
PUT ("SAFE_EMAX is probably too pessimistic, the following values");
PUT (" might be better:");
NEW_LINE;
PUT ("SAFE_EMAX could be ");
PUT (SAFE_V_EMAX, 0);
NEW_LINE;
PUT ("SAFE_LARGE could be ");
PUT_FLOAT (SAFE_V_LARGE);
NEW_LINE;
PUT ("SAFE_SMALL could be ");
PUT_FLOAT (SAFE_V_SMALL);
NEW_LINE;
end if;
end if;
A := SAFE_V_LARGE;
SAFE_VERY_EMAX := SAFE_V_EMAX;
loop
begin
SAFE_VERY_LARGE := A;
A := THROUGH_MEMORY (A * 2.0);
exit when A * 0.5 /= SAFE_VERY_LARGE;
SAFE_VERY_EMAX := SAFE_VERY_EMAX + 1;
exception
when NUMERIC_ERROR =>
exit;
when CONSTRAINT_ERROR =>
PUT ("Caught unexpected CONSTRAINT_ERROR.");
NEW_LINE;
exit;
when others =>
PUT ("Caught some strange exception.");
NEW_LINE;
ERRORS := TRUE;
exit;
end;
end loop;
B := SAFE_SMALL_1;
SAFE_VERY_SMALL := SAFE_V_SMALL;
SAFE_VERY_EMIN := - SAFE_V_EMAX;
loop
begin
SAFE_SMALL_1 := B;
B := THROUGH_MEMORY (B * 0.5);
exit when B * 2.0 /= SAFE_SMALL_1;
SAFE_VERY_EMIN := SAFE_VERY_EMIN - 1;
SAFE_VERY_SMALL := SAFE_VERY_SMALL * 0.5;
exception
when others =>
PUT ("Caught some strange exception.");
NEW_LINE;
ERRORS := TRUE;
exit;
end;
end loop;
if SAFE_V_EMAX /= SAFE_VERY_EMAX or SAFE_V_EMAX /= - SAFE_VERY_EMIN then
PUT ("The safe exponent range ought to be asymmetric with:");
NEW_LINE;
PUT ("SAFE_EMAX is ");
PUT (SAFE_VERY_EMAX, 0);
NEW_LINE;
PUT ("SAFE_EMIN is ");
PUT (SAFE_VERY_EMIN, 0);
NEW_LINE;
PUT ("SAFE_LARGE is ");
PUT_FLOAT (SAFE_VERY_LARGE);
NEW_LINE;
PUT ("SAFE_SMALL is ");
PUT_FLOAT (SAFE_VERY_SMALL);
NEW_LINE;
end if;
if FLOAT_TYPE'MACHINE_OVERFLOWS and MACHINE_OVERFLOWS then
PUT ("Verifying strictness of overflow interpretations.");
NEW_LINE;
begin
begin
B := EPSILON * 0.5 * 0.5;
for I in 1 .. SAFE_EMAX loop
B := B * 2.0;
end loop;
A := SAFE_LARGE + B;
OVERFLOW_ERROR := 1;
A := SAFE_LARGE * 2.0;
OVERFLOW_ERROR := 2;
for I in SAFE_EMAX + 1 .. SAFE_V_EMAX loop
B := B * 2.0;
end loop;
A := SAFE_V_LARGE + B;
OVERFLOW_ERROR := 3;
A := SAFE_V_LARGE * 2.0;
OVERFLOW_ERROR := 4;
for I in SAFE_V_EMAX + 1 .. SAFE_VERY_EMAX loop
B := B * 2.0;
end loop;
A := SAFE_VERY_LARGE + B;
OVERFLOW_ERROR := 3;
A := SAFE_VERY_LARGE * 2.0;
OVERFLOW_ERROR := 4;
raise NUMERIC_ERROR;
exception
when NUMERIC_ERROR =>
raise;
when others =>
PUT ("Wrong exception raised on overflow.");
NEW_LINE;
raise NUMERIC_ERROR;
end;
exception
when others =>
case OVERFLOW_ERROR is
when 0 =>
PUT ("MACHINE_OVERFLOWS appears to be according to LRM 4.5.7(7).");
when 1 =>
PUT ("MACHINE_OVERFLOWS is not according to LRM 4.5.7(7)");
NEW_LINE;
PUT ("Overflow occurs for numbers slightly larger than");
PUT (" SAFE_LARGE.");
when 2 =>
PUT ("If the recalculated SAFE attributes are used,");
NEW_LINE;
PUT ("MACHINE_OVERFLOWS appears to be according to LRM 4.5.7(7).");
when 3 =>
PUT ("MACHINE_OVERFLOWS is not according to LRM 4.5.7(7)");
NEW_LINE;
PUT ("for the recalculated SAFE attributes.");
if SAFE_V_EMAX /= SAFE_VERY_EMAX then
NEW_LINE;
PUT ("But the asymmetric attributes help.");
end if;
when 4 =>
PUT ("If the asymmetric SAFE attributes are used,");
NEW_LINE;
PUT ("MACHINE_OVERFLOWS appears to be according to LRM 4.5.7(7).");
when 5 =>
PUT ("Even if the asymmetric attributes are used,");
NEW_LINE;
PUT ("MACHINE_OVERFLOWS is not according to LRM 4.5.7(7)");
when 6 =>
PUT ("Cannot get an overflow exception with SAFE attributes,");
NEW_LINE;
PUT ("even not with the asymmetric ones.");
NEW_LINE;
PUT ("SAFE_LARGE * 2.0 does not overflow!");
when others =>
PUT ("This cannot happen!");
end case;
NEW_LINE;
end;
end if;
if ERRORS then
PUT ("It appears that some attributes are invalid.");
NEW_LINE;
else
PUT ("No erroneous attributes were found");
if SAFE_EMAX /= FLOAT_TYPE'SAFE_EMAX then
PUT ("; but SAFE_EMAX requires further verification");
end if;
PUT (".");
NEW_LINE;
end if;
PUT ("This concludes the verification.");
NEW_LINE;
exception
when NUMERIC_ERROR =>
PUT ("Caught NUMERIC_ERROR in an unexpected place.");
NEW_LINE;
PUT ("Verification has to be abandoned.");
NEW_LINE;
return;
when others =>
PUT ("Caught some exception in an unexpected place.");
NEW_LINE;
PUT ("Verification has to be abandoned.");
NEW_LINE;
return;
end VERIFY_ATTRIBUTES;
with TEXT_IO;
use TEXT_IO;
procedure HEADER is
begin
NEW_PAGE;
PUT ("VERIFY Version 1.3");
NEW_LINE;
PUT ("Floating point attribute verifyer.");
NEW_LINE;
NEW_LINE;
PUT ("Please send this output to the author after filling in the blanks.");
NEW_LINE;
PUT ("E-mail is preferred.");
NEW_LINE;
NEW_LINE;
PUT ("E-mail: dik@cwi.nl");
NEW_LINE;
PUT ("Bitnet/EARN: dik@mcvax");
NEW_LINE;
PUT ("ARPA: dik%cwi.nl@uunet.uu.net");
NEW_LINE;
PUT ("Surface mail:");
NEW_LINE;
PUT (" Dik T. Winter");
NEW_LINE;
PUT (" Centrum voor Wiskunde en Informatica");
NEW_LINE;
PUT (" Kruislaan 413");
NEW_LINE;
PUT (" 1098 SJ Amsterdam");
NEW_LINE;
PUT (" Nederland");
NEW_LINE;
NEW_LINE;
PUT ("Please fill in the following blanks:");
NEW_LINE;
PUT ("Machine (manufacturer/type):");
NEW_LINE;
PUT ("Model:");
NEW_LINE;
PUT ("Hardware floating-point?");
NEW_LINE;
PUT ("If a separate processor, which one?");
NEW_LINE;
NEW_LINE;
PUT ("Compiler manifacturer:");
NEW_LINE;
PUT ("Version (be as complete as possible):");
NEW_LINE;
end HEADER;
with VERIFY_ATTRIBUTES, HEADER, TEXT_IO;
use TEXT_IO;
procedure PROGRAM is
-- change the following lines to reflect the actual type to be tested.
-- these line must be either of the form:
-- type FLOAT_TO_TEST is new <predefined type>;
-- or of the form:
-- type USER_TYPEs digits <N>;
-- in the latter case the program assumes that the attributes of the
-- predefined types are verified (and correct!).
-- the first parameter to VERIFY_ATTRIBUTES is TRUE for
-- user defined types
type FLOAT_TO_TEST is new FLOAT;
type USER_TYPE is digits (FLOAT'DIGITS - 1);
procedure VF_P is new VERIFY_ATTRIBUTES (USER_DEFINED => FALSE,
FLOAT_TYPE => FLOAT_TO_TEST);
procedure VF_U is new VERIFY_ATTRIBUTES (USER_DEFINED => TRUE,
FLOAT_TYPE => USER_TYPE);
begin
HEADER;
NEW_PAGE;
PUT ("Checking predefined type.");
NEW_LINE;
VF_P;
NEW_PAGE;
PUT ("Checking user defined type.");
NEW_LINE;
VF_U;
end PROGRAM;
--
dik t. winter, cwi, amsterdam, nederland
INTERNET : dik@cwi.nl
BITNET/EARN: dik@mcvax