Patchwork [Ada] Implement pragma Check_Float_Overflow

login
register
mail settings
Submitter Arnaud Charlet
Date Jan. 2, 2013, 10:04 a.m.
Message ID <20130102100436.GA8054@adacore.com>
Download mbox | patch
Permalink /patch/208986/
State New
Headers show

Comments

Arnaud Charlet - Jan. 2, 2013, 10:04 a.m.
On most targets, Machine_Overflows is false for built in floating-point
types, and unconstrained floating-point types like Float do not raise an
exception on overflow, instead they generate infinities or in some cases,
NaN's. Check_Float_Overflow is a configuration pragma that sets a mode in
which the result of all operators on unconstrained float values is checked
to make sure it is in the base range, and an exception is raised if not.
The switch -gnateF also sets Check_Float_Overflow mode.

The following program:

     1. with Text_IO; use Text_IO;
     2. procedure FptOV is
     3.    X : Float := Float'Last;
     4.    Y : Float;
     5.    subtype MF is Float range Float'Range;
     6.    XF : MF := MF'Last;
     7.    YF : MF;
     8. begin
     9.    begin
    10.       YF := XF + XF;
    11.    exception
    12.       when Constraint_Error =>
    13.          Put_Line ("exception for MF");
    14.    end;
    15.    begin
    16.       Y := X + X;
    17.    exception
    18.       when Constraint_Error =>
    19.          Put_Line ("exception for Float");
    20.    end;
    21. end FptOV;

With switch -gnateF generates

exception for MF
exception for Float

without this switch, it only generates

exception for MF.

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

2013-01-02  Robert Dewar  <dewar@adacore.com>

	* checks.adb (Apply_Scalar_Range_Check): Implement Check_Float_Overflow.
	* opt.ads, opt.adb: Handle flags Check_Float_Overflow[_Config].
	* par-prag.adb: Add dummy entry for pragma Check_Float_Overflow.
	* sem_prag.adb: Implement pragma Check_Float_Overflow.
	* snames.ads-tmpl: Add entries for pragma Check_Float_Overflow.
	* switch-c.adb: Recognize -gnateF switch.
	* tree_io.ads: Update ASIS version number.
	* gnat_rm.texi: Add documentation of pragma Check_Float_Overflow.

Patch

Index: checks.adb
===================================================================
--- checks.adb	(revision 194787)
+++ checks.adb	(working copy)
@@ -2692,15 +2692,24 @@ 
       Is_Unconstrained_Subscr_Ref :=
         Is_Subscr_Ref and then not Is_Constrained (Arr_Typ);
 
-      --  Always do a range check if the source type includes infinities and
-      --  the target type does not include infinities. We do not do this if
-      --  range checks are killed.
+      --  Special checks for floating-point type
 
-      if Is_Floating_Point_Type (S_Typ)
-        and then Has_Infinities (S_Typ)
-        and then not Has_Infinities (Target_Typ)
-      then
-         Enable_Range_Check (Expr);
+      if Is_Floating_Point_Type (S_Typ) then
+
+         --  Always do a range check if the source type includes infinities and
+         --  the target type does not include infinities. We do not do this if
+         --  range checks are killed.
+
+         if Has_Infinities (S_Typ)
+           and then not Has_Infinities (Target_Typ)
+         then
+            Enable_Range_Check (Expr);
+
+         --  Always do a range check for operators if option set
+
+         elsif Check_Float_Overflow and then Nkind (Expr) in N_Op then
+            Enable_Range_Check (Expr);
+         end if;
       end if;
 
       --  Return if we know expression is definitely in the range of the target
@@ -2780,15 +2789,14 @@ 
       --  only if this is not a conversion between integer and real types.
 
       if not Is_Unconstrained_Subscr_Ref
+        and then Is_Discrete_Type (S_Typ) = Is_Discrete_Type (Target_Typ)
         and then
-           Is_Discrete_Type (S_Typ) = Is_Discrete_Type (Target_Typ)
-        and then
           (In_Subrange_Of (S_Typ, Target_Typ, Fixed_Int)
              or else
                Is_In_Range (Expr, Target_Typ,
                             Assume_Valid => True,
-                            Fixed_Int => Fixed_Int,
-                            Int_Real  => Int_Real))
+                            Fixed_Int    => Fixed_Int,
+                            Int_Real     => Int_Real))
       then
          return;
 
@@ -2800,12 +2808,18 @@ 
          Bad_Value;
          return;
 
+      --  Floating-point case
       --  In the floating-point case, we only do range checks if the type is
       --  constrained. We definitely do NOT want range checks for unconstrained
       --  types, since we want to have infinities
 
       elsif Is_Floating_Point_Type (S_Typ) then
-         if Is_Constrained (S_Typ) then
+
+      --  Normally, we only do range checks if the type is constrained. We do
+      --  NOT want range checks for unconstrained types, since we want to have
+      --  infinities. Override this decision in Check_Float_Overflow mode.
+
+         if Is_Constrained (S_Typ) or else Check_Float_Overflow then
             Enable_Range_Check (Expr);
          end if;
 
@@ -5650,22 +5664,24 @@ 
       --  First special case, if the source type is already within the range
       --  of the target type, then no check is needed (probably we should have
       --  stopped Do_Range_Check from being set in the first place, but better
-      --  late than later in preventing junk code!
+      --  late than never in preventing junk code!
 
-      --  We do NOT apply this if the source node is a literal, since in this
-      --  case the literal has already been labeled as having the subtype of
-      --  the target.
+      if In_Subrange_Of (Source_Type, Target_Type)
 
-      if In_Subrange_Of (Source_Type, Target_Type)
+        --  We do NOT apply this if the source node is a literal, since in this
+        --  case the literal has already been labeled as having the subtype of
+        --  the target.
+
         and then not
-          (Nkind (N) = N_Integer_Literal
+          (Nkind_In (N, N_Integer_Literal, N_Real_Literal, N_Character_Literal)
              or else
-           Nkind (N) = N_Real_Literal
-             or else
-           Nkind (N) = N_Character_Literal
-             or else
-           (Is_Entity_Name (N)
-              and then Ekind (Entity (N)) = E_Enumeration_Literal))
+               (Is_Entity_Name (N)
+                 and then Ekind (Entity (N)) = E_Enumeration_Literal))
+
+        --  Also do not apply this for floating-point if Check_Float_Overflow
+
+        and then not
+          (Is_Floating_Point_Type (Source_Type) and Check_Float_Overflow)
       then
          return;
       end if;
@@ -5675,9 +5691,7 @@ 
       --  reference). Such a double evaluation is always a potential source
       --  of inefficiency, and is functionally incorrect in the volatile case.
 
-      if not Is_Entity_Name (N)
-        or else Treat_As_Volatile (Entity (N))
-      then
+      if not Is_Entity_Name (N) or else Treat_As_Volatile (Entity (N)) then
          Force_Evaluation (N);
       end if;
 
Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi	(revision 194776)
+++ gnat_rm.texi	(working copy)
@@ -111,6 +111,7 @@ 
 * Pragma Ast_Entry::
 * Pragma C_Pass_By_Copy::
 * Pragma Check::
+* Pragma Check_Float_Overflow::
 * Pragma Check_Name::
 * Pragma Check_Policy::
 * Pragma Comment::
@@ -850,6 +851,7 @@ 
 * Pragma Ast_Entry::
 * Pragma C_Pass_By_Copy::
 * Pragma Check::
+* Pragma Check_Float_Overflow::
 * Pragma Check_Name::
 * Pragma Check_Policy::
 * Pragma Comment::
@@ -1402,6 +1404,58 @@ 
 be activated either by the command line option @option{-gnata}, which turns on
 all checks, or individually controlled using pragma @code{Check_Policy}.
 
+@node Pragma Check_Float_Overflow
+@unnumberedsec Pragma Check_Float_Overflow
+@cindex Floating-point overflow
+@findex Check_Float_Overflow
+@noindent
+Syntax:
+@smallexample @c ada
+pragma Check_Float_Overflow;
+@end smallexample
+
+@noindent
+In Ada, the predefined floating-point types (@code{Short_Float},
+@code{Float}, @code{Long_Float}, @code{Long_Long_Float}) are
+defined as being unconstrained. This means that even though they
+have well defined base ranges, there is no requirement that an
+overflow exception be raised when the result of an operation is
+outside this base range. This definition accomodates the notion
+of infinities in IEEE floating-point, and corresponds to the
+efficient execution mode on most machines. GNAT will not raise
+overflow exceptions on these machines, instead it will generate
+infinities and NaN's as defined in the IEEE standard.
+
+Although the generation of infinities is efficient, it is not
+always desirable, and it is often the case that it would be
+preferable to check for overflows, even if this resulted in
+substantially less efficient code. This can be accomplished
+by defining your own float subtypes, and indeed such types
+can have the same base range as in:
+
+@smallexample @c ada
+subtype My_Float is Float range Float'Range;
+@end smallexample
+
+@noindent
+In this example, @code{My_Float} has the same range as
+@code{Float} but it is constrained, so operations on
+@code{My_Float} values will be checked for overflow
+against this range.
+
+However, it is often convenient to avoid the need to
+define your own floating-point types, and instead use
+the standard predefined types. The @code{Check_Float_Overflow}
+configuration pragma achieves that. If a unit is compiled
+subject to this configuration pragma, then all operations
+on predefined floating-point types will be treated as
+though those types were constrained and overflow checks
+will be generated, resulting in a @code{Constraint_Error}
+exception if the result is out of range.
+
+This mode can also be set by use of the compiler
+switch @option{-gnateF}.
+
 @node Pragma Check_Name
 @unnumberedsec Pragma Check_Name
 @cindex Defining check names
Index: opt.adb
===================================================================
--- opt.adb	(revision 194776)
+++ opt.adb	(working copy)
@@ -57,6 +57,7 @@ 
       Ada_Version_Explicit_Config           := Ada_Version_Explicit;
       Assertions_Enabled_Config             := Assertions_Enabled;
       Assume_No_Invalid_Values_Config       := Assume_No_Invalid_Values;
+      Check_Float_Overflow_Config           := Check_Float_Overflow;
       Check_Policy_List_Config              := Check_Policy_List;
       Debug_Pragmas_Disabled_Config         := Debug_Pragmas_Disabled;
       Debug_Pragmas_Enabled_Config          := Debug_Pragmas_Enabled;
@@ -91,6 +92,7 @@ 
       Ada_Version_Explicit           := Save.Ada_Version_Explicit;
       Assertions_Enabled             := Save.Assertions_Enabled;
       Assume_No_Invalid_Values       := Save.Assume_No_Invalid_Values;
+      Check_Float_Overflow           := Save.Check_Float_Overflow;
       Check_Policy_List              := Save.Check_Policy_List;
       Debug_Pragmas_Disabled         := Save.Debug_Pragmas_Disabled;
       Debug_Pragmas_Enabled          := Save.Debug_Pragmas_Enabled;
@@ -127,6 +129,7 @@ 
       Save.Ada_Version_Explicit           := Ada_Version_Explicit;
       Save.Assertions_Enabled             := Assertions_Enabled;
       Save.Assume_No_Invalid_Values       := Assume_No_Invalid_Values;
+      Save.Check_Float_Overflow           := Check_Float_Overflow;
       Save.Check_Policy_List              := Check_Policy_List;
       Save.Debug_Pragmas_Disabled         := Debug_Pragmas_Disabled;
       Save.Debug_Pragmas_Enabled          := Debug_Pragmas_Enabled;
@@ -198,6 +201,7 @@ 
          Ada_Version_Explicit        := Ada_Version_Explicit_Config;
          Assertions_Enabled          := Assertions_Enabled_Config;
          Assume_No_Invalid_Values    := Assume_No_Invalid_Values_Config;
+         Check_Float_Overflow        := Check_Float_Overflow_Config;
          Check_Policy_List           := Check_Policy_List_Config;
          Debug_Pragmas_Disabled      := Debug_Pragmas_Disabled_Config;
          Debug_Pragmas_Enabled       := Debug_Pragmas_Enabled_Config;
@@ -255,6 +259,7 @@ 
       Tree_Read_Int  (Assertions_Enabled_Config_Val);
       Tree_Read_Bool (All_Errors_Mode);
       Tree_Read_Bool (Assertions_Enabled);
+      Tree_Read_Bool (Check_Float_Overflow);
       Tree_Read_Int  (Int (Check_Policy_List));
       Tree_Read_Bool (Debug_Pragmas_Disabled);
       Tree_Read_Bool (Debug_Pragmas_Enabled);
@@ -321,6 +326,7 @@ 
       Tree_Write_Int  (Boolean'Pos (Assertions_Enabled_Config));
       Tree_Write_Bool (All_Errors_Mode);
       Tree_Write_Bool (Assertions_Enabled);
+      Tree_Write_Bool (Check_Float_Overflow);
       Tree_Write_Int  (Int (Check_Policy_List));
       Tree_Write_Bool (Debug_Pragmas_Disabled);
       Tree_Write_Bool (Debug_Pragmas_Enabled);
Index: opt.ads
===================================================================
--- opt.ads	(revision 194787)
+++ opt.ads	(working copy)
@@ -276,6 +276,13 @@ 
    --  Set to True to detect whether subprogram parameters and function results
    --  alias the same object(s).
 
+   Check_Float_Overflow : Boolean := False;
+   --  GNAT
+   --  Set to True to check that operations on predefined unconstrained float
+   --  types (e.g. Float, Long_Float) do not overflow and generate infinities
+   --  or invalid values. Set by the Check_Float_Overflow pragma, or by use
+   --  of the -gnateo switch.
+
    Check_Object_Consistency : Boolean := False;
    --  GNATBIND, GNATMAKE
    --  Set to True to check whether every object file is consistent with
@@ -556,8 +563,7 @@ 
    Extensions_Allowed : Boolean := False;
    --  GNAT
    --  Set to True by switch -gnatX if GNAT specific language extensions
-   --  are allowed. For example, the use of 'Constrained with objects of
-   --  generic types is a GNAT extension.
+   --  are allowed. Currently there are no such defined extensions.
 
    type External_Casing_Type is (
      As_Is,       -- External names cased as they appear in the Ada source
@@ -1021,7 +1027,7 @@ 
    Object_Path_File_Name : String_Ptr := null;
    --  GNAT2WHY
    --  Path of the temporary file that contains a list of object directories
-   --  passed by -gnateO=<obj_pat_file>.
+   --  passed by -gnateO=<obj_path_file>.
 
    One_Compilation_Per_Obj_Dir : Boolean := False;
    --  GNATMAKE, GPRBUILD
@@ -1726,6 +1732,13 @@ 
    --  -gnatB, and possibly modified by the use of the configuration pragma
    --  Assume_No_Invalid_Values.
 
+   Check_Float_Overflow_Config : Boolean;
+   --  GNAT
+   --  Set to True to check that operations on predefined unconstrained float
+   --  types (e.g. Float, Long_Float) do not overflow and generate infinities
+   --  or invalid values. Set by the Check_Float_Overflow pragma, or by use
+   --  of the -gnateo switch.
+
    Check_Policy_List_Config : Node_Id;
    --  GNAT
    --  This points to the list of N_Pragma nodes for Check_Policy pragmas
@@ -1981,6 +1994,7 @@ 
       Ada_Version_Explicit           : Ada_Version_Type;
       Assertions_Enabled             : Boolean;
       Assume_No_Invalid_Values       : Boolean;
+      Check_Float_Overflow           : Boolean;
       Check_Policy_List              : Node_Id;
       Debug_Pragmas_Disabled         : Boolean;
       Debug_Pragmas_Enabled          : Boolean;
Index: par-prag.adb
===================================================================
--- par-prag.adb	(revision 194776)
+++ par-prag.adb	(working copy)
@@ -1106,6 +1106,7 @@ 
            Pragma_Attach_Handler                 |
            Pragma_Attribute_Definition           |
            Pragma_Check                          |
+           Pragma_Check_Float_Overflow           |
            Pragma_Check_Name                     |
            Pragma_Check_Policy                   |
            Pragma_CIL_Constructor                |
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 194786)
+++ sem_prag.adb	(working copy)
@@ -7560,6 +7560,18 @@ 
             end if;
          end Check;
 
+         --------------------------
+         -- Check_Float_Overflow --
+         --------------------------
+
+         --  pragma Check_Float_Overflow;
+
+         when Pragma_Check_Float_Overflow =>
+            GNAT_Pragma;
+            Check_Valid_Configuration_Pragma;
+            Check_Arg_Count (0);
+            Check_Float_Overflow := True;
+
          ----------------
          -- Check_Name --
          ----------------
@@ -15740,6 +15752,7 @@ 
       Pragma_Atomic_Components              =>  0,
       Pragma_Attach_Handler                 => -1,
       Pragma_Check                          => 99,
+      Pragma_Check_Float_Overflow           =>  0,
       Pragma_Check_Name                     =>  0,
       Pragma_Check_Policy                   =>  0,
       Pragma_CIL_Constructor                => -1,
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 194776)
+++ snames.ads-tmpl	(working copy)
@@ -366,6 +366,7 @@ 
    Name_Assume_No_Invalid_Values       : constant Name_Id := N + $; -- GNAT
    Name_Attribute_Definition           : constant Name_Id := N + $; -- GNAT
    Name_C_Pass_By_Copy                 : constant Name_Id := N + $; -- GNAT
+   Name_Check_Float_Overflow           : constant Name_Id := N + $; -- GNAT
    Name_Check_Name                     : constant Name_Id := N + $; -- GNAT
    Name_Check_Policy                   : constant Name_Id := N + $; -- GNAT
    Name_Compile_Time_Error             : constant Name_Id := N + $; -- GNAT
@@ -1665,6 +1666,7 @@ 
       Pragma_Assume_No_Invalid_Values,
       Pragma_Attribute_Definition,
       Pragma_C_Pass_By_Copy,
+      Pragma_Check_Float_Overflow,
       Pragma_Check_Name,
       Pragma_Check_Policy,
       Pragma_Compile_Time_Error,
Index: switch-c.adb
===================================================================
--- switch-c.adb	(revision 194776)
+++ switch-c.adb	(working copy)
@@ -514,6 +514,12 @@ 
                      Ptr := Ptr + 1;
                      Full_Path_Name_For_Brief_Errors := True;
 
+                  --  -gnateF (Check_Float_Overflow)
+
+                  when 'F' =>
+                     Ptr := Ptr + 1;
+                     Check_Float_Overflow := True;
+
                   --  -gnateG (save preprocessor output)
 
                   when 'G' =>
Index: tree_io.ads
===================================================================
--- tree_io.ads	(revision 194776)
+++ tree_io.ads	(working copy)
@@ -47,7 +47,7 @@ 
    Tree_Format_Error : exception;
    --  Raised if a format error is detected in the input file
 
-   ASIS_Version_Number : constant := 29;
+   ASIS_Version_Number : constant := 30;
    --  ASIS Version. This is used to check for consistency between the compiler
    --  used to generate trees and an ASIS application that is reading the
    --  trees. It must be incremented whenever a change is made to the tree
@@ -58,6 +58,7 @@ 
    --  28  Changes in Snames
    --  29  Changes in Sem_Ch3 (tree copying in case of discriminant constraint
    --      for concurrent types).
+   --  30  Add Check_Float_Overflow boolean to tree file
 
    procedure Tree_Read_Initialize (Desc : File_Descriptor);
    --  Called to initialize reading of a tree file. This call must be made