From patchwork Thu Sep 7 09:40:22 2017 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 810944 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (mailfrom) smtp.mailfrom=gcc.gnu.org (client-ip=209.132.180.131; helo=sourceware.org; envelope-from=gcc-patches-return-461671-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="DA/7oaYn"; dkim-atps=neutral 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 3xnwRv3zvHz9sNV for ; Thu, 7 Sep 2017 19:40:42 +1000 (AEST) 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=RA1qlg+Gtc5ImFPCWwfdJbWoid0VmqL0YQywAdhYnn6bl0wkX9 BBplsySknUxEq57/AsBD/J7f/d4Eh+LM+mCTb0G+64Re2cvvkfhbxt+v409klOWc 7pmsw3vh4mk2kBZAXvklowXU0FFrajFsWu96Se78Oq9T1KAgfbxFhx3qk= 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=6rfEjXefz0GlSomPBnLgp1n5AYM=; b=DA/7oaYnp57vZqATTPOs TeCnM/j21DWubtPp0EeQV7UOoW12xAxtWAfSW2ErZ1VUqfnBoM75PJbK7Q8HzDUK f3rBl6Nt8nG8XwaNvr5wfkPf9Mzoe16lp6qZkiWOMJqMLVD6CQoaRIyoGKVpIHjc 5gkVDU8N1P71BlazvB7a5pw= Received: (qmail 68485 invoked by alias); 7 Sep 2017 09:40:31 -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 67817 invoked by uid 89); 7 Sep 2017 09:40:30 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-11.1 required=5.0 tests=BAYES_00, GIT_PATCH_2, GIT_PATCH_3, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy= 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 ESMTP; Thu, 07 Sep 2017 09:40:24 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 8FA46561A2; Thu, 7 Sep 2017 05:40:22 -0400 (EDT) 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 ZtHsnv970AUw; Thu, 7 Sep 2017 05:40:22 -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 7B80256179; Thu, 7 Sep 2017 05:40:22 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4192) id 77B5E4FC; Thu, 7 Sep 2017 05:40:22 -0400 (EDT) Date: Thu, 7 Sep 2017 05:40:22 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Fix handling of ghost entity in predicate Message-ID: <20170907094022.GA93697@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) Ghost types are allowed to mention ghost entities in their predicate. Because Ghost is propagated from type to the generated predicate function, GNAT correctly identified valid from invalid cases, but this modification simplifies the reason for correction. Tested on x86_64-pc-linux-gnu, committed on trunk 2017-09-07 Yannick Moy * ghost.adb (Check_Ghost_Context): Do not err on ghost code inside predicate procedure. Check predicate pragma/aspect with Ghost entity. * exp_ch6.adb, par-ch6.adb, sem_ch13.adb, sem_prag.adb; Minor reformatting. Index: exp_ch6.adb =================================================================== --- exp_ch6.adb (revision 251835) +++ exp_ch6.adb (working copy) @@ -137,7 +137,8 @@ -- there are no tasks. function Caller_Known_Size - (Func_Call : Node_Id; Result_Subt : Entity_Id) return Boolean; + (Func_Call : Node_Id; + Result_Subt : Entity_Id) return Boolean; -- True if result subtype is definite, or has a size that does not require -- secondary stack usage (i.e. no variant part or components whose type -- depends on discriminants). In particular, untagged types with only @@ -837,11 +838,14 @@ ----------------------- function Caller_Known_Size - (Func_Call : Node_Id; Result_Subt : Entity_Id) return Boolean is + (Func_Call : Node_Id; + Result_Subt : Entity_Id) return Boolean + is begin - return (Is_Definite_Subtype (Underlying_Type (Result_Subt)) - and then No (Controlling_Argument (Func_Call))) - or else not Requires_Transient_Scope (Underlying_Type (Result_Subt)); + return + (Is_Definite_Subtype (Underlying_Type (Result_Subt)) + and then No (Controlling_Argument (Func_Call))) + or else not Requires_Transient_Scope (Underlying_Type (Result_Subt)); end Caller_Known_Size; -------------------------------- @@ -8081,7 +8085,8 @@ declare Definite : constant Boolean := - Caller_Known_Size (Func_Call, Result_Subt); + Caller_Known_Size (Func_Call, Result_Subt); + begin -- Create an access type designating the function's result subtype. -- We use the type of the original call because it may be a call to Index: ghost.adb =================================================================== --- ghost.adb (revision 251834) +++ ghost.adb (working copy) @@ -281,6 +281,13 @@ if Chars (Subp_Id) = Name_uPostconditions then return True; + -- The context is the internally built predicate function, + -- which is OK because the real check was done before the + -- predicate function was generated. + + elsif Is_Predicate_Function (Subp_Id) then + return True; + else Subp_Decl := Original_Node (Unit_Declaration_Node (Subp_Id)); @@ -362,10 +369,12 @@ return True; -- An assertion expression pragma is Ghost when it contains a - -- reference to a Ghost entity (SPARK RM 6.9(10)). + -- reference to a Ghost entity (SPARK RM 6.9(10)), except for + -- predicate pragmas (SPARK RM 6.9(11)). - elsif Assertion_Expression_Pragma (Prag_Id) then - + elsif Assertion_Expression_Pragma (Prag_Id) + and then Prag_Id /= Pragma_Predicate + then -- Ensure that the assertion policy and the Ghost policy are -- compatible (SPARK RM 6.9(18)). @@ -464,9 +473,16 @@ return True; -- A reference to a Ghost entity can appear within an aspect - -- specification (SPARK RM 6.9(10)). + -- specification (SPARK RM 6.9(10)). The precise checking will + -- occur when analyzing the corresponding pragma. We make an + -- exception for predicate aspects that only allow referencing + -- a Ghost entity when the corresponding type declaration is + -- Ghost (SPARK RM 6.9(11)). - elsif Nkind (Par) = N_Aspect_Specification then + elsif Nkind (Par) = N_Aspect_Specification + and then not Same_Aspect + (Get_Aspect_Id (Par), Aspect_Predicate) + then return True; elsif Is_OK_Declaration (Par) then Index: par-ch6.adb =================================================================== --- par-ch6.adb (revision 251835) +++ par-ch6.adb (working copy) @@ -855,13 +855,14 @@ if Is_Non_Empty_List (Aspects) then if Func then - Error_Msg ("aspect specifications must come after " - & "parenthesized expression", - Sloc (First (Aspects))); + Error_Msg + ("aspect specifications must come after " + & "parenthesized expression", + Sloc (First (Aspects))); else - Error_Msg ("aspect specifications must come after " - & "subprogram specification", - Sloc (First (Aspects))); + Error_Msg + ("aspect specifications must come after subprogram " + & "specification", Sloc (First (Aspects))); end if; end if; Index: sem_ch13.adb =================================================================== --- sem_ch13.adb (revision 251835) +++ sem_ch13.adb (working copy) @@ -12649,7 +12649,6 @@ -------------------------------- procedure Resolve_Aspect_Expressions (E : Entity_Id) is - function Resolve_Name (N : Node_Id) return Traverse_Result; -- Verify that all identifiers in the expression, with the exception -- of references to the current entity, denote visible entities. This @@ -12668,6 +12667,7 @@ function Resolve_Name (N : Node_Id) return Traverse_Result is Dummy : Traverse_Result; + begin if Nkind (N) = N_Selected_Component then if Nkind (Prefix (N)) = N_Identifier @@ -12700,6 +12700,8 @@ procedure Resolve_Aspect_Expression is new Traverse_Proc (Resolve_Name); + -- Local variables + ASN : Node_Id := First_Rep_Item (E); -- Start of processing for Resolve_Aspect_Expressions Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 251835) +++ sem_prag.adb (working copy) @@ -1205,126 +1205,173 @@ Item_Is_Output : out Boolean) is begin - Item_Is_Input := False; - Item_Is_Output := False; + case Ekind (Item_Id) is - -- Abstract states + -- Abstract states - if Ekind (Item_Id) = E_Abstract_State then + when E_Abstract_State => - -- When pragma Global is present, the mode of the state may be - -- further constrained by setting a more restrictive mode. + -- When pragma Global is present it determines the mode of + -- the abstract state. - if Global_Seen then - if Appears_In (Subp_Inputs, Item_Id) then - Item_Is_Input := True; - end if; + if Global_Seen then + Item_Is_Input := Appears_In (Subp_Inputs, Item_Id); + Item_Is_Output := Appears_In (Subp_Outputs, Item_Id); - if Appears_In (Subp_Outputs, Item_Id) then + -- Otherwise the state has a default IN OUT mode, because it + -- behaves as a variable. + + else + Item_Is_Input := True; Item_Is_Output := True; end if; - -- Otherwise the state has a default IN OUT mode + -- Constants and IN parameters - else - Item_Is_Input := True; - Item_Is_Output := True; - end if; + when E_Constant + | E_Generic_In_Parameter + | E_In_Parameter + | E_Loop_Parameter + => + -- When pragma Global is present it determines the mode + -- of constant objects as inputs (and such objects cannot + -- appear as outputs in the Global contract). - -- Constants + if Global_Seen then + Item_Is_Input := Appears_In (Subp_Inputs, Item_Id); + else + Item_Is_Input := True; + end if; - elsif Ekind_In (Item_Id, E_Constant, - E_Loop_Parameter) - then - Item_Is_Input := True; + Item_Is_Output := False; - -- Parameters + -- Variables and IN OUT parameters - elsif Ekind_In (Item_Id, E_Generic_In_Parameter, - E_In_Parameter) - then - Item_Is_Input := True; + when E_Generic_In_Out_Parameter + | E_In_Out_Parameter + | E_Variable + => + -- When pragma Global is present it determines the mode of + -- the object. - elsif Ekind_In (Item_Id, E_Generic_In_Out_Parameter, - E_In_Out_Parameter) - then - Item_Is_Input := True; - Item_Is_Output := True; + if Global_Seen then - elsif Ekind (Item_Id) = E_Out_Parameter then - if Scope (Item_Id) = Spec_Id then + -- A variable has mode IN when its type is unconstrained + -- or tagged because array bounds, discriminants or tags + -- can be read. - -- An OUT parameter of the related subprogram has mode IN - -- if its type is unconstrained or tagged because array - -- bounds, discriminants or tags can be read. + Item_Is_Input := + Appears_In (Subp_Inputs, Item_Id) + or else Is_Unconstrained_Or_Tagged_Item (Item_Id); - if Is_Unconstrained_Or_Tagged_Item (Item_Id) then - Item_Is_Input := True; + Item_Is_Output := Appears_In (Subp_Outputs, Item_Id); + + -- Otherwise the variable has a default IN OUT mode + + else + Item_Is_Input := True; + Item_Is_Output := True; end if; - Item_Is_Output := True; + when E_Out_Parameter => - -- An OUT parameter of an enclosing subprogram behaves as a - -- read-write variable in which case the mode is IN OUT. + -- An OUT parameter of the related subprogram; it cannot + -- appear in Global. - else - Item_Is_Input := True; - Item_Is_Output := True; - end if; + if Scope (Item_Id) = Spec_Id then - -- Protected types + -- The parameter has mode IN if its type is unconstrained + -- or tagged because array bounds, discriminants or tags + -- can be read. - elsif Ekind (Item_Id) = E_Protected_Type then + Item_Is_Input := + Is_Unconstrained_Or_Tagged_Item (Item_Id); - -- A protected type acts as a formal parameter of mode IN when - -- it applies to a protected function. + Item_Is_Output := True; - if Ekind (Spec_Id) = E_Function then - Item_Is_Input := True; + -- An OUT parameter of an enclosing subprogram; it can + -- appear in Global and behaves as a read-write variable. - -- Otherwise the protected type acts as a formal of mode IN OUT + else + -- When pragma Global is present it determines the mode + -- of the object. - else - Item_Is_Input := True; - Item_Is_Output := True; - end if; + if Global_Seen then - -- Task types + -- A variable has mode IN when its type is + -- unconstrained or tagged because array + -- bounds, discriminants or tags can be read. - elsif Ekind (Item_Id) = E_Task_Type then - Item_Is_Input := True; - Item_Is_Output := True; + Item_Is_Input := + Appears_In (Subp_Inputs, Item_Id) + or else Is_Unconstrained_Or_Tagged_Item (Item_Id); - -- Variable case + Item_Is_Output := Appears_In (Subp_Outputs, Item_Id); - else pragma Assert (Ekind (Item_Id) = E_Variable); + -- Otherwise the variable has a default IN OUT mode - -- When pragma Global is present, the mode of the variable may - -- be further constrained by setting a more restrictive mode. + else + Item_Is_Input := True; + Item_Is_Output := True; + end if; + end if; - if Global_Seen then + -- Protected types - -- A variable has mode IN when its type is unconstrained or - -- tagged because array bounds, discriminants or tags can be - -- read. + when E_Protected_Type => + if Global_Seen then - if Appears_In (Subp_Inputs, Item_Id) - or else Is_Unconstrained_Or_Tagged_Item (Item_Id) - then - Item_Is_Input := True; + -- A variable has mode IN when its type is unconstrained + -- or tagged because array bounds, discriminants or tags + -- can be read. + + Item_Is_Input := + Appears_In (Subp_Inputs, Item_Id) + or else Is_Unconstrained_Or_Tagged_Item (Item_Id); + + Item_Is_Output := Appears_In (Subp_Outputs, Item_Id); + + else + -- A protected type acts as a formal parameter of mode IN + -- when it applies to a protected function. + + if Ekind (Spec_Id) = E_Function then + Item_Is_Input := True; + Item_Is_Output := False; + + -- Otherwise the protected type acts as a formal of mode + -- IN OUT. + + else + Item_Is_Input := True; + Item_Is_Output := True; + end if; end if; - if Appears_In (Subp_Outputs, Item_Id) then + -- Task types + + when E_Task_Type => + + -- When pragma Global is present it determines the mode of + -- the object. + + if Global_Seen then + Item_Is_Input := + Appears_In (Subp_Inputs, Item_Id) + or else Is_Unconstrained_Or_Tagged_Item (Item_Id); + + Item_Is_Output := Appears_In (Subp_Outputs, Item_Id); + + -- Otherwise task types act as IN OUT parameters + + else + Item_Is_Input := True; Item_Is_Output := True; end if; - -- Otherwise the variable has a default IN OUT mode - - else - Item_Is_Input := True; - Item_Is_Output := True; - end if; - end if; + when others => + raise Program_Error; + end case; end Find_Role; ---------------- @@ -5069,7 +5116,7 @@ -- pragma is inserted in its declarative part. elsif From_Aspect_Specification (N) - and then Ent = Current_Scope + and then Ent = Current_Scope and then Nkind (Unit_Declaration_Node (Ent)) = N_Subprogram_Body then @@ -28300,7 +28347,7 @@ if Nkind (Clause) = N_Null then null; - -- A dependency cause appears as component association + -- A dependency clause appears as component association elsif Nkind (Clause) = N_Component_Association then Collect_Dependency_Item @@ -28424,21 +28471,15 @@ Subp_Decl := Unit_Declaration_Node (Subp_Id); Spec_Id := Unique_Defining_Entity (Subp_Decl); - -- Process all [generic] formal parameters + -- Process all formal parameters Formal := First_Entity (Spec_Id); while Present (Formal) loop - if Ekind_In (Formal, E_Generic_In_Parameter, - E_In_Out_Parameter, - E_In_Parameter) - then + if Ekind_In (Formal, E_In_Out_Parameter, E_In_Parameter) then Append_New_Elmt (Formal, Subp_Inputs); end if; - if Ekind_In (Formal, E_Generic_In_Out_Parameter, - E_In_Out_Parameter, - E_Out_Parameter) - then + if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then Append_New_Elmt (Formal, Subp_Outputs); -- Out parameters can act as inputs when the related type is