checks.adb (Apply_Scalar_Range_Check): Analyze precisely conversions from float to integer in GNATprove mode.

2017-04-25  Yannick Moy  <moy@adacore.com>

	* checks.adb (Apply_Scalar_Range_Check): Analyze precisely
	conversions from float to integer in GNATprove mode.
	(Apply_Type_Conversion_Checks): Make sure in GNATprove mode
	to call Apply_Type_Conversion_Checks, so that range checks
	are properly positioned when needed on conversions, including
	when converting from float to integer.	(Determine_Range): In
	GNATprove mode, take into account the possibility of conversion
	from float to integer.
	* sem_res.adb (Resolve_Type_Conversion): Only enforce range
	check on conversions from fixed-point to integer, not anymore
	on conversions from floating-point to integer, when in GNATprove
	mode.

From-SVN: r247173

3 files changed, 97 insertions, 15 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3c9e1ac..0a7a782 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,20 @@
 2017-04-25  Yannick Moy  <moy@adacore.com>
 
+	* checks.adb (Apply_Scalar_Range_Check): Analyze precisely
+	conversions from float to integer in GNATprove mode.
+	(Apply_Type_Conversion_Checks): Make sure in GNATprove mode
+	to call Apply_Type_Conversion_Checks, so that range checks
+	are properly positioned when needed on conversions, including
+	when converting from float to integer.	(Determine_Range): In
+	GNATprove mode, take into account the possibility of conversion
+	from float to integer.
+	* sem_res.adb (Resolve_Type_Conversion): Only enforce range
+	check on conversions from fixed-point to integer, not anymore
+	on conversions from floating-point to integer, when in GNATprove
+	mode.
+
+2017-04-25  Yannick Moy  <moy@adacore.com>
+
 	* checks.adb (Determine_Range_R): Special case type conversions
 	from integer to float in order to get bounds in that case too.
 	* eval_fat.adb (Machine): Avoid issuing warnings in GNATprove
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index 9bf008b..a057cf3 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -2943,20 +2943,24 @@ package body Checks is
 
       --  The additional less-precise tests below catch these cases
 
+      --  In GNATprove_Mode, also deal with the case of a conversion from
+      --  floating-point to integer. It is only possible because analysis
+      --  in GNATprove rules out the possibility of a NaN or infinite value.
+
       --  Note: skip this if we are given a source_typ, since the point of
       --  supplying a Source_Typ is to stop us looking at the expression.
       --  We could sharpen this test to be out parameters only ???
 
       if Is_Discrete_Type (Target_Typ)
-        and then Is_Discrete_Type (Etype (Expr))
+        and then (Is_Discrete_Type (Etype (Expr))
+                   or else (GNATprove_Mode
+                             and then Is_Floating_Point_Type (Etype (Expr))))
         and then not Is_Unconstrained_Subscr_Ref
         and then No (Source_Typ)
       then
          declare
             Tlo : constant Node_Id := Type_Low_Bound  (Target_Typ);
             Thi : constant Node_Id := Type_High_Bound (Target_Typ);
-            Lo  : Uint;
-            Hi  : Uint;
 
          begin
             if Compile_Time_Known_Value (Tlo)
@@ -2965,6 +2969,8 @@ package body Checks is
                declare
                   Lov : constant Uint := Expr_Value (Tlo);
                   Hiv : constant Uint := Expr_Value (Thi);
+                  Lo  : Uint;
+                  Hi  : Uint;
 
                begin
                   --  If range is null, we for sure have a constraint error
@@ -2991,7 +2997,34 @@ package body Checks is
 
                   --  Otherwise determine range of value
 
-                  Determine_Range (Expr, OK, Lo, Hi, Assume_Valid => True);
+                  if Is_Discrete_Type (Etype (Expr)) then
+                     Determine_Range (Expr, OK, Lo, Hi,
+                                      Assume_Valid => True);
+
+                  --  When converting a float to an integer type, determine the
+                  --  range in real first, and then convert the bounds using
+                  --  UR_To_Uint which correctly rounds away from zero when
+                  --  half way between two integers, as required by normal
+                  --  Ada 95 rounding semantics. It is only possible because
+                  --  analysis in GNATprove rules out the possibility of a NaN
+                  --  or infinite value.
+
+                  elsif GNATprove_Mode
+                    and then Is_Floating_Point_Type (Etype (Expr))
+                  then
+                     declare
+                        Lor : Ureal;
+                        Hir : Ureal;
+                     begin
+                        Determine_Range_R (Expr, OK, Lor, Hir,
+                                           Assume_Valid => True);
+
+                        if OK then
+                           Lo := UR_To_Uint (Lor);
+                           Hi := UR_To_Uint (Hir);
+                        end if;
+                     end;
+                  end if;
 
                   if OK then
 
@@ -3449,7 +3482,9 @@ package body Checks is
             if not Range_Checks_Suppressed (Target_Type)
               and then not Range_Checks_Suppressed (Expr_Type)
             then
-               if Float_To_Int then
+               if Float_To_Int
+                 and then not GNATprove_Mode
+               then
                   Apply_Float_Conversion_Check (Expr, Target_Type);
                else
                   Apply_Scalar_Range_Check
@@ -4688,11 +4723,39 @@ package body Checks is
 
             end case;
 
-         --  For type conversion from one discrete type to another, we can
-         --  refine the range using the converted value.
-
          when N_Type_Conversion =>
-            Determine_Range (Expression (N), OK1, Lor, Hir, Assume_Valid);
+
+            --  For type conversion from one discrete type to another, we can
+            --  refine the range using the converted value.
+
+            if Is_Discrete_Type (Etype (Expression (N))) then
+               Determine_Range (Expression (N), OK1, Lor, Hir, Assume_Valid);
+
+            --  When converting a float to an integer type, determine the range
+            --  in real first, and then convert the bounds using UR_To_Uint
+            --  which correctly rounds away from zero when half way between two
+            --  integers, as required by normal Ada 95 rounding semantics. It
+            --  is only possible because analysis in GNATprove rules out the
+            --  possibility of a NaN or infinite value.
+
+            elsif GNATprove_Mode
+              and then Is_Floating_Point_Type (Etype (Expression (N)))
+            then
+               declare
+                  Lor_Real, Hir_Real : Ureal;
+               begin
+                  Determine_Range_R (Expression (N), OK1, Lor_Real, Hir_Real,
+                                     Assume_Valid);
+
+                  if OK1 then
+                     Lor := UR_To_Uint (Lor_Real);
+                     Hir := UR_To_Uint (Hir_Real);
+                  end if;
+               end;
+
+            else
+               OK1 := False;
+            end if;
 
          --  Nothing special to do for all other expression kinds
 
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 5a0797e..70e0c28 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -11053,15 +11053,19 @@ package body Sem_Res is
          end if;
       end if;
 
-      --  If at this stage we have a real to integer conversion, make sure
-      --  that the Do_Range_Check flag is set, because such conversions in
-      --  general need a range check. We only need this if expansion is off
-      --  or we are in GNATProve mode.
+      --  If at this stage we have a real to integer conversion, make sure that
+      --  the Do_Range_Check flag is set, because such conversions in general
+      --  need a range check. We only need this if expansion is off, or we are
+      --  in GNATprove mode and the conversion if from fixed-point to integer
+      --  (as floating-point to integer conversions are now handled in
+      --  GNATprove mode).
 
       if Nkind (N) = N_Type_Conversion
-        and then (GNATprove_Mode or not Expander_Active)
+        and then not Expander_Active
         and then Is_Integer_Type (Target_Typ)
-        and then Is_Real_Type (Operand_Typ)
+        and then (Is_Real_Type (Operand_Typ)
+                   or else (GNATprove_Mode
+                             and then Is_Fixed_Point_Type (Operand_Typ)))
       then
          Set_Do_Range_Check (Operand);
       end if;