public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-234] [Ada] Accept Structural in aspect Subprogram_Variant and pragma Loop_Variant
@ 2022-05-10 8:21 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-05-10 8:21 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:d89d9ecceb541ca824f7fb5f57f747a31c7ce9a5
commit r13-234-gd89d9ecceb541ca824f7fb5f57f747a31c7ce9a5
Author: Claire Dross <dross@adacore.com>
Date: Fri Jan 21 10:42:49 2022 +0100
[Ada] Accept Structural in aspect Subprogram_Variant and pragma Loop_Variant
Add a new form of variants to ensure termination of loops or recursive
subprograms. Structural variants correspond to objects which designate a
part of the data-structure they used to designate in the previous loop
iteration or recursive call. They only imply termination if the
data-structure is acyclic, which is the case in SPARK but not in Ada in
general. The fact that these variants are correct is only verified
formally by the proof tool and not by the compiler or dynamically at
execution like other forms of variants.
gcc/ada/
* snames.ads-tmpl: Add "Structural" as a name.
* sem_prag.adb: (Analyze_Pragma): Accept modifier "Structural"
in pragmas Loop_Variant and Subprogram_Variant. Check that items
associated to Structural occur alone in the pragma associations.
(Analyze_Subprogram_Variant_In_Decl_Part): Idem.
* exp_prag.adb (Expand_Pragma_Loop_Variant): Discard structural
variants.
(Expand_Pragma_Subprogram_Variant): Idem.
gcc/testsuite/
* gnat.dg/loopvar.adb: Update expected error message.
Diff:
---
gcc/ada/exp_prag.adb | 25 ++++++++++------
gcc/ada/sem_prag.adb | 61 +++++++++++++++++++++++++++++----------
gcc/ada/snames.ads-tmpl | 1 +
gcc/testsuite/gnat.dg/loopvar.adb | 2 +-
4 files changed, 64 insertions(+), 25 deletions(-)
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index 0fe8bfffdb2..bf2d29744c4 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -2694,10 +2694,15 @@ package body Exp_Prag is
-- If pragma is not enabled, rewrite as Null statement. If pragma is
-- disabled, it has already been rewritten as a Null statement.
--
- -- Likewise, do this in CodePeer mode, because the expanded code is too
+ -- Likewise, ignore structural variants for execution.
+ --
+ -- Also do this in CodePeer mode, because the expanded code is too
-- complicated for CodePeer to analyse.
- if Is_Ignored (N) or else CodePeer_Mode then
+ if Is_Ignored (N)
+ or else Chars (Last_Var) = Name_Structural
+ or else CodePeer_Mode
+ then
Rewrite (N, Make_Null_Statement (Loc));
Analyze (N);
return;
@@ -3058,10 +3063,12 @@ package body Exp_Prag is
Loc : constant Source_Ptr := Sloc (Prag);
- Aggr : Node_Id;
+ Aggr : constant Node_Id :=
+ Expression (First (Pragma_Argument_Associations (Prag)));
Formal_Map : Elist_Id;
Last : Node_Id;
- Last_Variant : Node_Id;
+ Last_Variant : constant Node_Id :=
+ Nlists.Last (Component_Associations (Aggr));
Proc_Bod : Node_Id;
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
@@ -3069,14 +3076,15 @@ package body Exp_Prag is
Variant : Node_Id;
begin
- -- Do nothing if pragma is not present or is disabled
+ -- Do nothing if pragma is not present or is disabled.
+ -- Also ignore structural variants for execution.
- if Is_Ignored (Prag) then
+ if Is_Ignored (Prag)
+ or else Chars (Nlists.Last (Choices (Last_Variant))) = Name_Structural
+ then
return;
end if;
- Aggr := Expression (First (Pragma_Argument_Associations (Prag)));
-
-- The expansion of Subprogram Variant is quite distributed as it
-- produces various statements to capture and compare the arguments.
-- To preserve the original context, set the Is_Assertion_Expr flag.
@@ -3115,7 +3123,6 @@ package body Exp_Prag is
Last := Proc_Decl;
Curr_Decls := New_List;
- Last_Variant := Nlists.Last (Component_Associations (Aggr));
Variant := First (Component_Associations (Aggr));
while Present (Variant) loop
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 9ef3a06d929..57a74db53ba 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -19423,7 +19423,8 @@ package body Sem_Prag is
if Chars (Variant) = No_Name then
Error_Pragma_Arg_Ident ("expect name `Increases`", Variant);
- elsif Chars (Variant) not in Name_Decreases | Name_Increases
+ elsif Chars (Variant) not in
+ Name_Decreases | Name_Increases | Name_Structural
then
declare
Name : String := Get_Name_String (Chars (Variant));
@@ -19448,11 +19449,24 @@ package body Sem_Prag is
Error_Pragma_Arg_Ident
("expect name `Decreases`", Variant);
+ elsif Name'Length >= 4
+ and then Name (1 .. 4) = "stru"
+ then
+ Error_Pragma_Arg_Ident
+ ("expect name `Structural`", Variant);
+
else
Error_Pragma_Arg_Ident
- ("expect name `Increases` or `Decreases`", Variant);
+ ("expect name `Increases`, `Decreases`,"
+ & " or `Structural`", Variant);
end if;
end;
+
+ elsif Chars (Variant) = Name_Structural
+ and then List_Length (Pragma_Argument_Associations (N)) > 1
+ then
+ Error_Pragma_Arg_Ident
+ ("Structural variant shall be the only variant", Variant);
end if;
-- Preanalyze_Assert_Expression, but without enforcing any of
@@ -19460,9 +19474,12 @@ package body Sem_Prag is
Preanalyze_Assert_Expression (Expression (Variant));
- -- Expression of a discrete type is allowed
+ -- Expression of a discrete type is allowed. Nothing to
+ -- check for structural variants.
- if Is_Discrete_Type (Etype (Expression (Variant))) then
+ if Chars (Variant) = Name_Structural
+ or else Is_Discrete_Type (Etype (Expression (Variant)))
+ then
null;
-- Expression of a Big_Integer type (or its ghost variant) is
@@ -24227,13 +24244,16 @@ package body Sem_Prag is
-- Subprogram_Variant --
------------------------
- -- pragma Subprogram_Variant ( SUBPROGRAM_VARIANT_ITEM
- -- {, SUBPROGRAM_VARIANT_ITEM } );
-
- -- SUBPROGRAM_VARIANT_ITEM ::=
- -- CHANGE_DIRECTION => discrete_EXPRESSION
+ -- pragma Subprogram_Variant ( SUBPROGRAM_VARIANT_LIST );
- -- CHANGE_DIRECTION ::= Increases | Decreases
+ -- SUBPROGRAM_VARIANT_LIST ::= STRUCTURAL_SUBPROGRAM_VARIANT_ITEM
+ -- | NUMERIC_SUBPROGRAM_VARIANT_ITEMS
+ -- NUMERIC_SUBPROGRAM_VARIANT_ITEMS ::=
+ -- NUMERIC_SUBPROGRAM_VARIANT_ITEM
+ -- {, NUMERIC_SUBPROGRAM_VARIANT_ITEM}
+ -- NUMERIC_SUBPROGRAM_VARIANT_ITEM ::= CHANGE_DIRECTION => EXPRESSION
+ -- STRUCTURAL_SUBPROGRAM_VARIANT_ITEM ::= Structural => EXPRESSION
+ -- CHANGE_DIRECTION ::= Increases | Decreases
-- Characteristics:
@@ -29435,9 +29455,9 @@ package body Sem_Prag is
-- Check placement of OTHERS if available (SPARK RM 6.1.3(1))
if Nkind (Direction) = N_Identifier then
- if Chars (Direction) /= Name_Decreases
- and then
- Chars (Direction) /= Name_Increases
+ if Chars (Direction) not in Name_Decreases
+ | Name_Increases
+ | Name_Structural
then
Error_Msg_N ("wrong direction", Direction);
end if;
@@ -29452,9 +29472,12 @@ package body Sem_Prag is
Preanalyze_Assert_Expression (Expr);
- -- Expression of a discrete type is allowed
+ -- Expression of a discrete type is allowed. Nothing more to check
+ -- for structural variants.
- if Is_Discrete_Type (Etype (Expr)) then
+ if Is_Discrete_Type (Etype (Expr))
+ or else Chars (Direction) = Name_Structural
+ then
null;
-- Expression of a Big_Integer type (or its ghost variant) is only
@@ -29561,6 +29584,14 @@ package body Sem_Prag is
Variant := First (Component_Associations (Variants));
while Present (Variant) loop
Analyze_Variant (Variant);
+
+ if Chars (First (Choices (Variant))) = Name_Structural
+ and then List_Length (Component_Associations (Variants)) > 1
+ then
+ Error_Msg_N
+ ("Structural variant shall be the only variant", Variant);
+ end if;
+
Next (Variant);
end loop;
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index fa7ac8a9dfb..5f7d6b7687b 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -875,6 +875,7 @@ package Snames is
Name_Static : constant Name_Id := N + $;
Name_Stack_Size : constant Name_Id := N + $;
Name_Strict : constant Name_Id := N + $;
+ Name_Structural : constant Name_Id := N + $;
Name_Subunit_File_Name : constant Name_Id := N + $;
Name_Suppressible : constant Name_Id := N + $;
Name_Synchronous : constant Name_Id := N + $;
diff --git a/gcc/testsuite/gnat.dg/loopvar.adb b/gcc/testsuite/gnat.dg/loopvar.adb
index f85402adc1d..e98d20d310d 100644
--- a/gcc/testsuite/gnat.dg/loopvar.adb
+++ b/gcc/testsuite/gnat.dg/loopvar.adb
@@ -9,7 +9,7 @@ begin
pragma Loop_Variant (J + 1); -- { dg-error "expect name \"Increases\"" }
pragma Loop_Variant (incr => -J + 1); -- { dg-error "expect name \"Increases\"" }
pragma Loop_Variant (decr => -J + 1); -- { dg-error "expect name \"Decreases\"" }
- pragma Loop_Variant (foof => -J + 1); -- { dg-error "expect name \"Increases\" or \"Decreases\"" }
+ pragma Loop_Variant (foof => -J + 1); -- { dg-error "expect name \"Increases\", \"Decreases\", or \"Structural\"" }
J := J + 2;
end loop;
end Loopvar;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-05-10 8:21 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-05-10 8:21 [gcc r13-234] [Ada] Accept Structural in aspect Subprogram_Variant and pragma Loop_Variant Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).