Skip to content

R
riscv-gcc-1
Commit d8ee014f by Yannick Moy Committed by Arnaud Charlet
Options

checks.adb (Apply_Scalar_Range_Check): Analyze precisely conversions from float… 

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
parent 3c77943e
Showing with 94 additions and 12 deletions
gcc/ada/ChangeLog
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
......
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,12 +4723,40 @@ package body Checks is
end case;
when N_Type_Conversion =>
-- For type conversion from one discrete type to another, we can
-- refine the range using the converted value.
when N_Type_Conversion =>
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
when others =>
......
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;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment