When reorganizing the mechanism which evaluates relational operators and
potentially folds them, the "General case" in routine Eval_Relational_Op
was put into an ELSE branch. This was subtly wrong, because it must be
executed unless the special case in the THEN branch exits with a RETURN
statement.
This patch restores the original behaviour of Eval_Relational_Op, so
that the relational operator is always folded when its operators are
static. This behaviour is asserted in Rewrite_Comparison, which is
called as part of the expansion (without this patch this assertion was
failing).
Finally, to satisfy this assertion we need to re-enable evaluation
within assertion expression, which was dubiously disabled for GNATprove.
(But this can be investigated separately).
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* exp_ch4.adb (Rewrite_Comparison): Add assertion to confirm
that evaluation folds comparisons with static operands; when
folding comparison with non-static operands, the resulting
literal is non-static.
* sem_eval.adb (Eval_Relational_Op): Refactor nested IF
statement for the special case in the THEN branch; move code for
the "general case" out of the ELSE branch.
* sem_res.adb (Resolve_Comparison_Op): Only apply a dubious
special-case for GNATprove in the GNATprove_Mode.diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -14962,6 +14962,14 @@ package body Exp_Ch4 is
return;
end if;
+ -- If both operands are static, then the comparison has been already
+ -- folded in evaluation.
+
+ pragma Assert
+ (not Is_Static_Expression (Left_Opnd (N))
+ or else
+ not Is_Static_Expression (Right_Opnd (N)));
+
-- Determine the potential outcome of the comparison assuming that the
-- operands are valid and emit a warning when the comparison evaluates
-- to True or False only in the presence of invalid values.
@@ -14977,7 +14985,8 @@ package body Exp_Ch4 is
True_Result => True_Result,
False_Result => False_Result);
- -- The outcome is a decisive False or True, rewrite the operator
+ -- The outcome is a decisive False or True, rewrite the operator into a
+ -- non-static literal.
if False_Result or True_Result then
Rewrite (N,
@@ -14985,6 +14994,7 @@ package body Exp_Ch4 is
New_Occurrence_Of (Boolean_Literals (True_Result), Sloc (N))));
Analyze_And_Resolve (N, Typ);
+ Set_Is_Static_Expression (N, False);
Warn_On_Known_Condition (N);
end if;
end Rewrite_Comparison;
diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb
--- a/gcc/ada/sem_eval.adb
+++ b/gcc/ada/sem_eval.adb
@@ -3731,83 +3731,81 @@ package body Sem_Eval is
Raises_Constraint_Error (Right)
then
return;
+ end if;
-- OK, we have the case where we may be able to do this fold
- else
- Left_Len := Static_Length (Left);
- Right_Len := Static_Length (Right);
+ Left_Len := Static_Length (Left);
+ Right_Len := Static_Length (Right);
- if Left_Len /= Uint_Minus_1
- and then Right_Len /= Uint_Minus_1
- and then Left_Len /= Right_Len
- then
- -- AI12-0201: comparison of string is static in Ada 202x
+ if Left_Len /= Uint_Minus_1
+ and then Right_Len /= Uint_Minus_1
+ and then Left_Len /= Right_Len
+ then
+ -- AI12-0201: comparison of string is static in Ada 202x
- Fold_Uint
- (N,
- Test (Nkind (N) = N_Op_Ne),
- Static => Ada_Version >= Ada_2020
- and then Is_String_Type (Left_Typ));
- Warn_On_Known_Condition (N);
- return;
- end if;
+ Fold_Uint
+ (N,
+ Test (Nkind (N) = N_Op_Ne),
+ Static => Ada_Version >= Ada_2020
+ and then Is_String_Type (Left_Typ));
+ Warn_On_Known_Condition (N);
+ return;
end if;
+ end if;
-- General case
- else
- -- Initialize the value of Is_Static_Expression. The value of Fold
- -- returned by Test_Expression_Is_Foldable is not needed since, even
- -- when some operand is a variable, we can still perform the static
- -- evaluation of the expression in some cases (for example, for a
- -- variable of a subtype of Integer we statically know that any value
- -- stored in such variable is smaller than Integer'Last).
-
- Test_Expression_Is_Foldable
- (N, Left, Right, Is_Static_Expression, Fold);
-
- -- Comparisons of scalars can give static results.
- -- In addition starting with Ada 202x (AI12-0201), comparison of
- -- strings can also give static results, and as noted above, we also
- -- allow for earlier Ada versions internally generated equality and
- -- inequality for strings.
- -- ??? The Comes_From_Source test below isn't correct and will accept
- -- some cases that are illegal in Ada 2012. and before. Now that
- -- Ada 202x has relaxed the rules, this doesn't really matter.
-
- if Is_String_Type (Left_Typ) then
- if Ada_Version < Ada_2020
- and then (Comes_From_Source (N)
- or else Nkind (N) not in N_Op_Eq | N_Op_Ne)
- then
- Is_Static_Expression := False;
- Set_Is_Static_Expression (N, False);
- end if;
+ -- Initialize the value of Is_Static_Expression. The value of Fold
+ -- returned by Test_Expression_Is_Foldable is not needed since, even
+ -- when some operand is a variable, we can still perform the static
+ -- evaluation of the expression in some cases (for example, for a
+ -- variable of a subtype of Integer we statically know that any value
+ -- stored in such variable is smaller than Integer'Last).
- elsif not Is_Scalar_Type (Left_Typ) then
+ Test_Expression_Is_Foldable
+ (N, Left, Right, Is_Static_Expression, Fold);
+
+ -- Comparisons of scalars can give static results.
+ -- In addition starting with Ada 202x (AI12-0201), comparison of strings
+ -- can also give static results, and as noted above, we also allow for
+ -- earlier Ada versions internally generated equality and inequality for
+ -- strings.
+ -- ??? The Comes_From_Source test below isn't correct and will accept
+ -- some cases that are illegal in Ada 2012. and before. Now that Ada
+ -- 202x has relaxed the rules, this doesn't really matter.
+
+ if Is_String_Type (Left_Typ) then
+ if Ada_Version < Ada_2020
+ and then (Comes_From_Source (N)
+ or else Nkind (N) not in N_Op_Eq | N_Op_Ne)
+ then
Is_Static_Expression := False;
Set_Is_Static_Expression (N, False);
end if;
- -- For operators on universal numeric types called as functions with
- -- an explicit scope, determine appropriate specific numeric type,
- -- and diagnose possible ambiguity.
+ elsif not Is_Scalar_Type (Left_Typ) then
+ Is_Static_Expression := False;
+ Set_Is_Static_Expression (N, False);
+ end if;
- if Is_Universal_Numeric_Type (Left_Typ)
- and then
- Is_Universal_Numeric_Type (Right_Typ)
- then
- Op_Typ := Find_Universal_Operator_Type (N);
- end if;
+ -- For operators on universal numeric types called as functions with an
+ -- explicit scope, determine appropriate specific numeric type, and
+ -- diagnose possible ambiguity.
- -- Attempt to fold the relational operator
+ if Is_Universal_Numeric_Type (Left_Typ)
+ and then
+ Is_Universal_Numeric_Type (Right_Typ)
+ then
+ Op_Typ := Find_Universal_Operator_Type (N);
+ end if;
- if Is_Static_Expression and then Is_Real_Type (Left_Typ) then
- Fold_Static_Real_Op;
- else
- Fold_General_Op (Is_Static_Expression);
- end if;
+ -- Attempt to fold the relational operator
+
+ if Is_Static_Expression and then Is_Real_Type (Left_Typ) then
+ Fold_Static_Real_Op;
+ else
+ Fold_General_Op (Is_Static_Expression);
end if;
-- For the case of a folded relational operator on a specific numeric
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7458,14 +7458,17 @@ package body Sem_Res is
Analyze_Dimension (N);
-- Evaluate the relation (note we do this after the above check since
- -- this Eval call may change N to True/False. Skip this evaluation
+ -- this Eval call may change N to True/False). Skip this evaluation
-- inside assertions, in order to keep assertions as written by users
-- for tools that rely on these, e.g. GNATprove for loop invariants.
-- Except evaluation is still performed even inside assertions for
-- comparisons between values of universal type, which are useless
-- for static analysis tools, and not supported even by GNATprove.
+ -- ??? It is suspicious to disable evaluation only for comparison
+ -- operators and not, let's say, for calls to static functions.
- if In_Assertion_Expr = 0
+ if not GNATprove_Mode
+ or else In_Assertion_Expr = 0
or else (Is_Universal_Numeric_Type (Etype (L))
and then
Is_Universal_Numeric_Type (Etype (R)))
