From patchwork Wed Jun 17 08:16:11 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: 1311020 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=2620:52:3:1:0:246e:9693:128c; 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 [IPv6:2620:52:3:1:0:246e:9693:128c]) (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 49mybr2CK1z9sSf for ; Wed, 17 Jun 2020 18:17:28 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 69E2B389041E; Wed, 17 Jun 2020 08:16:22 +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 [205.232.38.15]) by sourceware.org (Postfix) with ESMTP id 6ABB43890405 for ; Wed, 17 Jun 2020 08:16:13 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.3.2 sourceware.org 6ABB43890405 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 2DA2D116139; Wed, 17 Jun 2020 04:16:11 -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 imF0mgVnNVtp; Wed, 17 Jun 2020 04:16:11 -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 1B4E0117EC0; Wed, 17 Jun 2020 04:16:11 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 1A68FA9; Wed, 17 Jun 2020 04:16:11 -0400 (EDT) Date: Wed, 17 Jun 2020 04:16:11 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Subject: [Ada] Support aspect Relaxed_Initialization on private types and constants Message-ID: <20200617081611.GA55400@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-Spam-Status: No, score=-3.1 required=5.0 tests=BAYES_00, 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: Piotr Trojanek Errors-To: gcc-patches-bounces@gcc.gnu.org Sender: "Gcc-patches" Aspect Relaxed_Initialization can now be attached to private types and deferred constants, but only to their private views. This is similar to the spirit of SPARK RM 6.9(9) for ghost aspect, which says: "[This rule is to ensure that the ghostliness of a visible entity can be determined without having to look into the private part of the enclosing package.]" Note: implementation of this rule for Ghost aspect appears to be slightly wrong. We require Ghost aspect to be repeated on a full view that completes a private type, but only for record types. Tested on x86_64-pc-linux-gnu, committed on trunk 2020-06-17 Piotr Trojanek gcc/ada/ * einfo.adb (Is_Relaxed_Initialization_State): Add reference to SPARK RM. * sem_attr.adb (Analyze_Attribute_Old_Result): Likewise. * sem_ch13.adb (Analyze_Aspect_Relaxed_Initialization): Reject aspect on completions of private types and deferred constants. * sem_util.ads, sem_util.adb (Has_Relaxed_Initialization): Adjust comments; support queries for constants. --- gcc/ada/einfo.adb +++ gcc/ada/einfo.adb @@ -8256,8 +8256,7 @@ package body Einfo is function Is_Relaxed_Initialization_State (Id : E) return B is begin -- To qualify, the abstract state must appear with simple option - -- "Relaxed_Initialization" (??? add reference to SPARK RM once the - -- Relaxed_Initialization aspect is described there). + -- "Relaxed_Initialization" (SPARK RM 6.10). return Ekind (Id) = E_Abstract_State --- gcc/ada/sem_attr.adb +++ gcc/ada/sem_attr.adb @@ -1333,8 +1333,7 @@ package body Sem_Attr is null; -- Attribute 'Result is allowed to appear in aspect - -- Relaxed_Initialization (??? add reference to SPARK RM once this - -- attribute is described there). + -- Relaxed_Initialization (SPARK RM 6.10). elsif Prag_Nam = Name_Relaxed_Initialization and then Aname = Name_Result --- gcc/ada/sem_ch13.adb +++ gcc/ada/sem_ch13.adb @@ -2216,19 +2216,37 @@ package body Sem_Ch13 is -- Will be set to True if we need to restore the scope table -- after analyzing the aspect expression. + Prev_Id : Entity_Id; + -- Start of processing for Analyze_Aspect_Relaxed_Initialization begin -- Set name of the aspect for error messages Error_Msg_Name_1 := Nam; - -- Annotation of a type; no aspect expression is allowed + -- Annotation of a type; no aspect expression is allowed. + -- For a private type, the aspect must be attached to the + -- partial view. + -- -- ??? Once the exact rule for this aspect is ready, we will -- likely reject concurrent types, etc., so let's keep the code -- for types and variable separate. if Is_First_Subtype (E) then - if Present (Expr) then + Prev_Id := Incomplete_Or_Partial_View (E); + if Present (Prev_Id) then + + -- Aspect may appear on the full view of an incomplete + -- type because the incomplete declaration cannot have + -- any aspects. + + if Ekind (Prev_Id) = E_Incomplete_Type then + null; + else + Error_Msg_N ("aspect % must apply to partial view", N); + end if; + + elsif Present (Expr) then Error_Msg_N ("illegal aspect % expression", Expr); end if; @@ -2239,6 +2257,19 @@ package body Sem_Ch13 is Error_Msg_N ("illegal aspect % expression", Expr); end if; + -- Annotation of a constant; no aspect expression is allowed. + -- For a deferred constant, the aspect must be attached to the + -- partial view. + + elsif Ekind (E) = E_Constant then + if Present (Incomplete_Or_Partial_View (E)) then + Error_Msg_N + ("aspect % must apply to deferred constant", N); + + elsif Present (Expr) then + Error_Msg_N ("illegal aspect % expression", Expr); + end if; + -- Annotation of a subprogram; aspect expression is required elsif Is_Subprogram (E) then --- gcc/ada/sem_util.adb +++ gcc/ada/sem_util.adb @@ -12495,13 +12495,20 @@ package body Sem_Util is when E_Abstract_State => return Is_Relaxed_Initialization_State (E); + -- Constants have this aspect attached directly; for deferred + -- constants, the aspect is attached to the partial view. + + when E_Constant => + return Has_Aspect (E, Aspect_Relaxed_Initialization); + -- Variables have this aspect attached directly when E_Variable => return Has_Aspect (E, Aspect_Relaxed_Initialization); -- Types have this aspect attached directly (though we only allow it - -- to be specified for the first subtype). + -- to be specified for the first subtype). For private types, the + -- aspect is attached to the partial view. when Type_Kind => pragma Assert (Is_First_Subtype (E)); --- gcc/ada/sem_util.ads +++ gcc/ada/sem_util.ads @@ -1382,9 +1382,10 @@ package Sem_Util is -- yet received a full declaration. function Has_Relaxed_Initialization (E : Entity_Id) return Boolean; - -- Returns True iff entity E, which can be either a type, a variable, an - -- abstract state or a function, is subject to the Relaxed_Initialization - -- aspect. + -- Returns True iff entity E is subject to the Relaxed_Initialization + -- aspect. Entity E can be either type, variable, constant, function, + -- or abstract state. For private types and deferred constants E should + -- be the private view, because aspect can only be attached there. function Has_Signed_Zeros (E : Entity_Id) return Boolean; -- Determines if the floating-point type E supports signed zeros.