From patchwork Thu Nov 12 11:35:37 2015 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 543315 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 02C2E1413F0 for ; Thu, 12 Nov 2015 22:35:48 +1100 (AEDT) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b=NoeJ62wf; dkim-atps=neutral DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=nSs/mejIpEzXX1wh5i22VaakiAhrUwKJU+D5dQdSrZmmkrIDqT iem3H09bq8kYdI4XEYDrJ/LoXy9xgcXQm/IS23fOeMlmthuXC2O01PKBtNjvKrYe oi7SFBh1qFkU20Wso916iFo1m46gKx06Kz/VMdFhxEssXRP6t8X/cUHj8= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=pr5H8BJAu54l6MqyHNbD2ZxxDz0=; b=NoeJ62wf6Mm7cXKGnIyW 7LLOzuL4hVKiCOp7OEATRqx0WNR/Zty3u0d2k3k58CP4wiGgCFlErjvL/VRS2Vz2 tCYI/ekGli+R2JAPZs9xQvpVkdlbhJ5YoMUOZOAkGSZzGbFHyDSX0clfNwJC95A0 zqt5vkAJeWZ5kRJ7WUTEW+w= Received: (qmail 127250 invoked by alias); 12 Nov 2015 11:35:41 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org Received: (qmail 125258 invoked by uid 89); 12 Nov 2015 11:35:40 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=1.9 required=5.0 tests=BAYES_50, KAM_ASCII_DIVIDERS, KAM_LAZY_DOMAIN_SECURITY, RCVD_IN_DNSWL_LOW autolearn=no version=3.3.2 X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with (AES256-SHA encrypted) ESMTPS; Thu, 12 Nov 2015 11:35:39 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 2F18329954; Thu, 12 Nov 2015 06:35:37 -0500 (EST) 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 Uqy3m1c1RaaV; Thu, 12 Nov 2015 06:35:37 -0500 (EST) 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 1B46D2994C; Thu, 12 Nov 2015 06:35:37 -0500 (EST) Received: by tron.gnat.com (Postfix, from userid 4192) id 156BD1A5; Thu, 12 Nov 2015 06:35:37 -0500 (EST) Date: Thu, 12 Nov 2015 06:35:37 -0500 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Missing detection of elaboration dependency Message-ID: <20151112113537.GA24105@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) This patch modifies the elaboration circuitry to detect an issue in SPARK where an object in package P of a private type in package T subject to pragma Default_Initial_Condition is default initialized and package P lacks Elaborate_All (T). ------------ -- Source -- ------------ -- pack.ads package Pack with SPARK_Mode is type Elab_Typ is private with Default_Initial_Condition => Get_Val (Elab_Typ) = Expect_Val; type False_Typ is private with Default_Initial_Condition => False; type True_Typ is private with Default_Initial_Condition => True; function Expect_Val return Integer; function Get_Val (Obj : Elab_Typ) return Integer; private type Elab_Typ is record Comp : Integer; end record; type False_Typ is null record; type True_Typ is null record; end Pack; -- pack.adb package body Pack with SPARK_Mode is function Expect_Val return Integer is begin return 1234; end Expect_Val; function Get_Val (Obj : Elab_Typ) return Integer is begin return Obj.Comp; end Get_Val; end Pack; -- main_pack.ads with Pack; use Pack; package Main_Pack with SPARK_Mode is Obj_1 : Elab_Typ; Obj_2 : False_Typ; Obj_3 : True_Typ; end Main_Pack; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnata main_pack.ads main_pack.ads:4:04: call to Default_Initial_Condition during elaboration in SPARK main_pack.ads:4:04: Elaborate_All pragma required for "Pack" Tested on x86_64-pc-linux-gnu, committed on trunk 2015-11-12 Hristian Kirtchev * sem_elab.adb (Check_A_Call): Add new variable Is_DIC_Proc. Report elaboration issue in SPARK concerning calls to source subprograms or nontrivial Default_Initial_Condition procedures. Add specialized error message to avoid outputting the internal name of the Default_Initial_Condition procedure. * sem_util.ads, sem_util.adb (Is_Non_Trivial_Default_Init_Cond_Procedure): New routine. Index: sem_util.adb =================================================================== --- sem_util.adb (revision 230235) +++ sem_util.adb (working copy) @@ -12362,12 +12362,50 @@ end if; end Is_Local_Variable_Reference; + ------------------------------------------------ + -- Is_Non_Trivial_Default_Init_Cond_Procedure -- + ------------------------------------------------ + + function Is_Non_Trivial_Default_Init_Cond_Procedure + (Id : Entity_Id) return Boolean + is + Body_Decl : Node_Id; + Stmt : Node_Id; + + begin + if Ekind (Id) = E_Procedure + and then Is_Default_Init_Cond_Procedure (Id) + then + Body_Decl := + Unit_Declaration_Node + (Corresponding_Body (Unit_Declaration_Node (Id))); + + -- The body of the Default_Initial_Condition procedure must contain + -- at least one statement, otherwise the generation of the subprogram + -- body failed. + + pragma Assert (Present (Handled_Statement_Sequence (Body_Decl))); + + -- To qualify as non-trivial, the first statement of the procedure + -- must be a check in the form of an if statement. If the original + -- Default_Initial_Condition expression was folded, then the first + -- statement is not a check. + + Stmt := First (Statements (Handled_Statement_Sequence (Body_Decl))); + + return + Nkind (Stmt) = N_If_Statement + and then Nkind (Original_Node (Stmt)) = N_Pragma; + end if; + + return False; + end Is_Non_Trivial_Default_Init_Cond_Procedure; + ------------------------- -- Is_Object_Reference -- ------------------------- function Is_Object_Reference (N : Node_Id) return Boolean is - function Is_Internally_Generated_Renaming (N : Node_Id) return Boolean; -- Determine whether N is the name of an internally-generated renaming Index: sem_util.ads =================================================================== --- sem_util.ads (revision 230223) +++ sem_util.ads (working copy) @@ -1433,6 +1433,12 @@ -- parameter of the current enclosing subprogram. -- Why are OUT parameters not considered here ??? + function Is_Non_Trivial_Default_Init_Cond_Procedure + (Id : Entity_Id) return Boolean; + -- Determine whether entity Id denotes the procedure which verifies the + -- assertion expression of pragma Default_Initial_Condition and if it does, + -- the encapsulated expression is non-trivial. + function Is_Object_Reference (N : Node_Id) return Boolean; -- Determines if the tree referenced by N represents an object. Both -- variable and constant objects return True (compare Is_Variable). Index: sem_elab.adb =================================================================== --- sem_elab.adb (revision 230223) +++ sem_elab.adb (working copy) @@ -597,6 +597,11 @@ -- non-visible unit. This is the scope that is to be investigated to -- see whether an elaboration check is required. + Is_DIC_Proc : Boolean := False; + -- Flag set when the call denotes the Default_Initial_Condition + -- procedure of a private type which wraps a non-trivila assertion + -- expression. + Issue_In_SPARK : Boolean; -- Flag set when a source entity is called during elaboration in SPARK @@ -966,8 +971,17 @@ return; end if; - Issue_In_SPARK := SPARK_Mode = On and Comes_From_Source (Ent); + Is_DIC_Proc := Is_Non_Trivial_Default_Init_Cond_Procedure (Ent); + -- Elaboration issues in SPARK are reported only for source constructs + -- and for non-trivial Default_Initial_Condition procedures. The latter + -- must be checked because the default initialization of an object of a + -- private type triggers the evaluation of the Default_Initial_Condition + -- expression which in turn may have side effects. + + Issue_In_SPARK := + SPARK_Mode = On and (Comes_From_Source (Ent) or Is_DIC_Proc); + -- Now check if an Elaborate_All (or dynamic check) is needed if not Suppress_Elaboration_Warnings (Ent) @@ -1016,8 +1030,21 @@ Ent); elsif Issue_In_SPARK then - Error_Msg_NE ("call to & during elaboration in SPARK", N, Ent); + -- Emit a specialized error message when the elaboration of an + -- object of a private type evaluates the expression of pragma + -- Default_Initial_Condition. This prevents the internal name + -- of the procedure from appearing in the error message. + + if Is_DIC_Proc then + Error_Msg_N + ("call to Default_Initial_Condition during elaboration in " + & "SPARK", N); + else + Error_Msg_NE + ("call to & during elaboration in SPARK", N, Ent); + end if; + else Elab_Warning ("call to & may raise Program_Error?l?",