From patchwork Thu Jul 16 09:20:51 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 1330091 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=8.43.85.97; helo=sourceware.org; envelope-from=gcc-patches-bounces@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dmarc=none (p=none dis=none) header.from=adacore.com Received: from sourceware.org (server2.sourceware.org [8.43.85.97]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 4B6pf96BCLz9sT6 for ; Thu, 16 Jul 2020 19:21:21 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 72D1C388C01A; Thu, 16 Jul 2020 09:20:57 +0000 (GMT) X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from rock.gnat.com (rock.gnat.com [IPv6:2620:20:4000:0:a9e:1ff:fe9b:1d1]) by sourceware.org (Postfix) with ESMTP id 8858D3857C51 for ; Thu, 16 Jul 2020 09:20:51 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.3.2 sourceware.org 8858D3857C51 Authentication-Results: sourceware.org; dmarc=none (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=derodat@adacore.com Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 476FF56079; Thu, 16 Jul 2020 05:20:51 -0400 (EDT) X-Virus-Scanned: Debian amavisd-new at gnat.com Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id 3El7BwY0rZxU; Thu, 16 Jul 2020 05:20:51 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [IPv6:2620:20:4000:0:46a8:42ff:fe0e:e294]) by rock.gnat.com (Postfix) with ESMTP id 31C0B56074; Thu, 16 Jul 2020 05:20:51 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 2A4A812D; Thu, 16 Jul 2020 05:20:51 -0400 (EDT) Date: Thu, 16 Jul 2020 05:20:51 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Subject: [Ada] AI12-0042: Type invariant checking rules Message-ID: <20200716092051.GA146371@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-Spam-Status: No, score=-8.5 required=5.0 tests=BAYES_00, GIT_PATCH_0, KAM_ASCII_DIVIDERS, KAM_DMARC_STATUS, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=ham autolearn_force=no version=3.4.2 X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) 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: , Cc: Gary Dismukes Errors-To: gcc-patches-bounces@gcc.gnu.org Sender: "Gcc-patches" AI12-0042 specifies a couple of new rules for type invariants. The first is that when a type extension inherits a nonabstract subprogram that is a private operation of an ancestor type that has a class-wide invariant and the parent subprogram is visible at that point, the subprogram must be overridden. The second is the addition of a requirement to perform an invariant check on a conversion from a specific tagged expression to a class-wide type T'Class whose root type imposes a type invariant, when the conversion occurs within the immediate scope of T (checking the invariant on the part of the conversion expression that is of type T). Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_ch4.adb (Expand_N_Type_Conversion): Handle the case of applying an invariant check for a conversion to a class-wide type whose root type has a type invariant, when the conversion appears within the immediate scope of the type and the expression is of a specific tagged type. * sem_ch3.adb (Is_Private_Primitive): New function to determine whether a primitive subprogram is a private operation. (Check_Abstract_Overriding): Enforce the restriction imposed by AI12-0042 of requiring overriding of an inherited nonabstract private operation when the ancestor has a class-wide type invariant and the ancestor's private operation is visible. (Derive_Subprogram): Set Requires_Overriding on a subprogram inherited from a visible private operation of an ancestor to which a Type_Invariant'Class expression applies. 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 @@ -11951,6 +11951,39 @@ package body Exp_Ch4 is Remove_Side_Effects (N); Insert_Action (N, Make_Invariant_Call (Duplicate_Subexpr (N))); goto Done; + + -- AI12-0042: For a view conversion to a class-wide type occurring + -- within the immediate scope of T, from a specific type that is + -- a descendant of T (including T itself), an invariant check is + -- performed on the part of the object that is of type T. (We don't + -- need to explicitly check for the operand type being a descendant, + -- just that it's a specific type, because the conversion would be + -- illegal if it's specific and not a descendant -- downward conversion + -- is not allowed). + + elsif Is_Class_Wide_Type (Target_Type) + and then not Is_Class_Wide_Type (Etype (Expression (N))) + and then Present (Invariant_Procedure (Root_Type (Target_Type))) + and then Comes_From_Source (N) + and then Within_Scope (Find_Enclosing_Scope (N), Scope (Target_Type)) + then + Remove_Side_Effects (N); + + -- Perform the invariant check on a conversion to the class-wide + -- type's root type. + + declare + Root_Conv : constant Node_Id := + Make_Type_Conversion (Loc, + Subtype_Mark => + New_Occurrence_Of (Root_Type (Target_Type), Loc), + Expression => Duplicate_Subexpr (Expression (N))); + begin + Set_Etype (Root_Conv, Root_Type (Target_Type)); + + Insert_Action (N, Make_Invariant_Call (Root_Conv)); + goto Done; + end; end if; -- Here if we may need to expand conversion diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -579,6 +579,12 @@ package body Sem_Ch3 is -- Extensions_Visible with value False and has at least one controlling -- parameter of mode OUT. + function Is_Private_Primitive (Prim : Entity_Id) return Boolean; + -- Subsidiary to Check_Abstract_Overriding and Derive_Subprogram. + -- When applied to a primitive subprogram Prim, returns True if Prim is + -- declared as a private operation within a package or generic package, + -- and returns False otherwise. + function Is_Valid_Constraint_Kind (T_Kind : Type_Kind; Constraint_Kind : Node_Kind) return Boolean; @@ -10754,6 +10760,32 @@ package body Sem_Ch3 is elsif Present (Interface_Alias (Subp)) then null; + -- AI12-0042: Test for rule in 7.3.2(6.1/4), that requires overriding + -- of a visible private primitive inherited from an ancestor with + -- the aspect Type_Invariant'Class, unless the inherited primitive + -- is abstract. (The test for the extension occurring in a different + -- scope than the ancestor is to avoid requiring overriding when + -- extending in the same scope, because the inherited primitive will + -- also be private in that case, which looks like an unhelpful + -- restriction that may break reasonable code, though the rule + -- appears to apply in the same-scope case as well???) + + elsif not Is_Abstract_Subprogram (Subp) + and then not Comes_From_Source (Subp) -- An inherited subprogram + and then Requires_Overriding (Subp) + and then Present (Alias_Subp) + and then Has_Invariants (Etype (T)) + and then Present (Get_Pragma (Etype (T), Pragma_Invariant)) + and then Class_Present (Get_Pragma (Etype (T), Pragma_Invariant)) + and then Is_Private_Primitive (Alias_Subp) + and then Scope (Subp) /= Scope (Alias_Subp) + then + Error_Msg_NE + ("inherited private primitive & must be overridden", T, Subp); + Error_Msg_N + ("\because ancestor type has 'Type_'Invariant''Class " & + "(RM 7.3.2(6.1))", T); + elsif (Is_Abstract_Subprogram (Subp) or else Requires_Overriding (Subp) or else @@ -15676,6 +15708,9 @@ package body Sem_Ch3 is -- Ada 2005 (AI-228): Calculate the "require overriding" and "abstract" -- properties of the subprogram, as defined in RM-3.9.3(4/2-6/2). + -- Ada 202x (AI12-0042): Similarly, set those properties for + -- implementing the rule of RM 7.3.2(6.1/4). + -- A subprogram subject to pragma Extensions_Visible with value False -- requires overriding if the subprogram has at least one controlling -- OUT parameter (SPARK RM 6.1.7(6)). @@ -15692,7 +15727,23 @@ package body Sem_Ch3 is Derived_Type and then not Is_Null_Extension (Derived_Type)) or else (Comes_From_Source (Alias (New_Subp)) - and then Is_EVF_Procedure (Alias (New_Subp)))) + and then Is_EVF_Procedure (Alias (New_Subp))) + + -- AI12-0042: Set Requires_Overriding when a type extension + -- inherits a private operation that is visible at the + -- point of extension (Has_Private_Ancestor is False) from + -- an ancestor that has Type_Invariant'Class. + + or else + (not Has_Private_Ancestor (Derived_Type) + and then Has_Invariants (Parent_Type) + and then + Present (Get_Pragma (Parent_Type, Pragma_Invariant)) + and then + Class_Present + (Get_Pragma (Parent_Type, Pragma_Invariant)) + and then Is_Private_Primitive (Parent_Subp))) + and then No (Actual_Subp) then if not Is_Tagged_Type (Derived_Type) @@ -18727,6 +18778,29 @@ package body Sem_Ch3 is end if; end Is_Null_Extension; + -------------------------- + -- Is_Private_Primitive -- + -------------------------- + + function Is_Private_Primitive (Prim : Entity_Id) return Boolean is + Prim_Scope : constant Entity_Id := Scope (Prim); + Priv_Entity : Entity_Id; + begin + if Is_Package_Or_Generic_Package (Prim_Scope) then + Priv_Entity := First_Private_Entity (Prim_Scope); + + while Present (Priv_Entity) loop + if Priv_Entity = Prim then + return True; + end if; + + Next_Entity (Priv_Entity); + end loop; + end if; + + return False; + end Is_Private_Primitive; + ------------------------------ -- Is_Valid_Constraint_Kind -- ------------------------------