From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-wr1-x435.google.com (mail-wr1-x435.google.com [IPv6:2a00:1450:4864:20::435]) by sourceware.org (Postfix) with ESMTPS id ADDAD3836004 for ; Tue, 10 May 2022 08:21:02 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org ADDAD3836004 Received: by mail-wr1-x435.google.com with SMTP id e2so22655001wrh.7 for ; Tue, 10 May 2022 01:21:02 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=WdTkMwgi5ihN+M+K9Ify5JH91WT4R4eH+uKE9rdt91o=; b=kftQL8IbMgLIMSjbFHdpExF3i1mVvccVKQPkxQGaylv7YrPEZz7+a4RI8giroh1qJ6 SG+TnddCdPGxfoBUANicitMAUh4JofoF/avv9/S0epjK0pie9oe/15B4RVixyeRscfGm HbJez7SyfavXhb12ojMfvjmnzvhlnDT0Lvk9Y+C+yD3cAP1hVqtWZmbz3YvRM5f8ulbr VBT4bLAqibtDGNCe2goTq6HTV4c7snILnUQ3p52I+YlAb2LRRSqeMS+EeCVb77LtKCcY fld7dLWIPNWQ7v5xLzHw9LnEBkiTzi1U/QqNVM2CvFRDgWWxhsZHf70Ew6TI2NZN3F78 IZzg== X-Gm-Message-State: AOAM532NNsrOB+Zrp3nHywCWepAVeZfmEj0XuZWv249iswtaFyV5VfE5 S3enhVXvhhHEsfFSUu3LHllzYvPGURlgVA== X-Google-Smtp-Source: ABdhPJxAH4qAU5IBtcIxc0b3zolzXXRiRoM+o0GSuM/xcZB7CrGJygqb6QDY6ZZ5q7PkRHYyzsUZPA== X-Received: by 2002:adf:f00d:0:b0:20c:d4d4:2b79 with SMTP id j13-20020adff00d000000b0020cd4d42b79mr3001810wro.552.1652170861532; Tue, 10 May 2022 01:21:01 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id d8-20020a1c7308000000b003942a244f50sm1799527wmb.41.2022.05.10.01.21.00 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 10 May 2022 01:21:01 -0700 (PDT) Date: Tue, 10 May 2022 08:21:00 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Claire Dross Subject: [Ada] Accept Structural in aspect Subprogram_Variant and pragma Loop_Variant Message-ID: <20220510082100.GA3029091@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="sm4nu43k4a2Rpi4c" Content-Disposition: inline X-Spam-Status: No, score=-13.2 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 10 May 2022 08:21:05 -0000 --sm4nu43k4a2Rpi4c Content-Type: text/plain; charset=us-ascii Content-Disposition: inline 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. Tested on x86_64-pc-linux-gnu, committed on trunk 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. --sm4nu43k4a2Rpi4c Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb --- 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 --- 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 --- 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 --- 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; --sm4nu43k4a2Rpi4c--