From patchwork Tue Apr 23 09:06:55 2013 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 238811 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 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (Client CN "localhost", Issuer "www.qmailtoaster.com" (not verified)) by ozlabs.org (Postfix) with ESMTPS id CB6402C0142 for ; Tue, 23 Apr 2013 19:07:04 +1000 (EST) 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=Qr4hcDyEZFmMDI4MNK4TZcVssD916dMDrwmyc6v3s+x3+1sU+Q 8TR5No62pmapV7jUsi9tPxLGahF/2LDWew9a4QbAIHh9KpdM98colksyyPRHDu1i HNgupu55F+4UKEQiGbbmpFsejgqbz8OW0RFgKi2eZTYKp0lmsGJq6Cbvc= 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=3tkC0+mkPIlB5aGzFYBM783ya9o=; b=LTzNBdVJniBIOn69+4n6 XPedWljp7/4kmqXG23skV7lv/FQTm2cz1pYLntdhGKCNkpAidLsrP2VbTLHwHsi5 Dc3afK+kV7wSEg8UABbYNRaNSCP1qirNqRtISlRz12tbQZ+M9682879J88Hln2wk P5Yhr1+pfKRQMVHNve8w8os= Received: (qmail 16784 invoked by alias); 23 Apr 2013 09:06:58 -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 16769 invoked by uid 89); 23 Apr 2013 09:06:58 -0000 X-Spam-SWARE-Status: No, score=-1.8 required=5.0 tests=AWL, BAYES_00, RCVD_IN_HOSTKARMA_NO autolearn=ham version=3.3.1 Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.84/v0.84-167-ge50287c) with ESMTP; Tue, 23 Apr 2013 09:06:57 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id B88452E953; Tue, 23 Apr 2013 05:06:55 -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 lbq12bC+A10C; Tue, 23 Apr 2013 05:06:55 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 9882C2E94E; Tue, 23 Apr 2013 05:06:55 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 9821A3FF09; Tue, 23 Apr 2013 05:06:55 -0400 (EDT) Date: Tue, 23 Apr 2013 05:06:55 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Legality of self-referential outputs in aspect/pragma Depends Message-ID: <20130423090655.GA17651@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) X-Virus-Found: No This patch updates the analysis of aspect/pragma Depends to verify the legality of a self-referential output. ------------ -- Source -- ------------ -- semantics.ads package Semantics with Abstract_State => ((Input_State with Volatile, Input), (Output_State with Volatile, Output)) is Input_Var : Integer; -- in Mixed_Var : Integer; -- in out Output_Var : Integer; -- out procedure Error (Formal : out Integer) with Global => (Input => (Input_State, Input_Var), Output => (Output_State, Output_Var), In_Out => Mixed_Var), Depends => ((Formal, -- error Mixed_Var, -- ok, already in out Output_State, -- error Output_Var) -- error =>+ (Input_Var, Input_State, Mixed_Var)); end Semantics; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnat12 -gnatd.V semantics.ads semantics.ads:20:10: item "Formal" must have mode in out semantics.ads:22:10: item "Output_State" must have mode in out semantics.ads:23:10: item "Output_Var" must have mode in out Tested on x86_64-pc-linux-gnu, committed on trunk 2013-04-23 Hristian Kirtchev * sem_prag.adb (Analyze_Dependency_Clause): Update all calls to Analyze_Input_Output. (Analyze_Input_List): Update all calls to Analyze_Input_Output. (Analyze_Input_Output): Add formal parameter Self_Ref along with comment on its usage. Update all calls to Analyze_Input_Output. (Analyze_Pragma): Add new local variable Self_Ref to capture the presence of a self-referential dependency clause. Update all calls to Analyze_Input_Output. (Check_Mode): Add formal parameter Self_Ref along with comment on its usage. Verify the legality of a self-referential output. Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 198175) +++ sem_prag.adb (working copy) @@ -9346,10 +9346,14 @@ procedure Check_Mode (Item : Node_Id; Item_Id : Entity_Id; - Is_Input : Boolean); + Is_Input : Boolean; + Self_Ref : Boolean); -- Ensure that an item has a proper "in", "in out" or "out" mode -- depending on its function. If this is not the case, emit an - -- error. + -- error. Item and Item_Id denote the attributes of an item. Flag + -- Is_Input should be set when item comes from an input list. + -- Flag Self_Ref should be set when the item is an output and the + -- dependency clause has operator "+". procedure Check_Usage (Subp_List : Elist_Id; @@ -9382,16 +9386,19 @@ procedure Analyze_Input_Output (Item : Node_Id; Is_Input : Boolean; + Self_Ref : Boolean; Top_Level : Boolean; Seen : in out Elist_Id; Null_Seen : in out Boolean); -- Verify the legality of a single input or output item. Flag -- Is_Input should be set whenever Item is an input, False when - -- it denotes an output. Flag Top_Level should be set whenever - -- Item appears immediately within an input or output list. - -- Seen is a collection of all abstract states, variables and - -- formals processed so far. Flag Null_Seen denotes whether a - -- null input or output has been encountered. + -- it denotes an output. Flag Self_Ref should be set when the + -- item is an output and the dependency clause has a "+". Flag + -- Top_Level should be set whenever Item appears immediately + -- within an input or output list. Seen is a collection of all + -- abstract states, variables and formals processed so far. + -- Flag Null_Seen denotes whether a null input or output has + -- been encountered. ------------------------ -- Analyze_Input_List -- @@ -9421,6 +9428,7 @@ Analyze_Input_Output (Item => Input, Is_Input => True, + Self_Ref => False, Top_Level => False, Seen => Inputs_Seen, Null_Seen => Null_Input_Seen); @@ -9439,6 +9447,7 @@ Analyze_Input_Output (Item => Inputs, Is_Input => True, + Self_Ref => False, Top_Level => False, Seen => Inputs_Seen, Null_Seen => Null_Input_Seen); @@ -9462,6 +9471,7 @@ procedure Analyze_Input_Output (Item : Node_Id; Is_Input : Boolean; + Self_Ref : Boolean; Top_Level : Boolean; Seen : in out Elist_Id; Null_Seen : in out Boolean) @@ -9490,6 +9500,7 @@ Analyze_Input_Output (Item => Grouped, Is_Input => Is_Input, + Self_Ref => Self_Ref, Top_Level => False, Seen => Seen, Null_Seen => Null_Seen); @@ -9576,7 +9587,7 @@ -- Ensure that the item is of the correct mode -- depending on its function. - Check_Mode (Item, Item_Id, Is_Input); + Check_Mode (Item, Item_Id, Is_Input, Self_Ref); -- Detect multiple uses of the same state, variable -- or formal parameter. If this is not the case, @@ -9631,12 +9642,24 @@ -- Local variables - Inputs : Node_Id; - Output : Node_Id; + Inputs : Node_Id; + Output : Node_Id; + Self_Ref : Boolean; -- Start of processing for Analyze_Dependency_Clause begin + Inputs := Expression (Clause); + Self_Ref := False; + + -- An input list with a self-dependency appears as operator "+" + -- where the actuals inputs are the right operand. + + if Nkind (Inputs) = N_Op_Plus then + Inputs := Right_Opnd (Inputs); + Self_Ref := True; + end if; + -- Process the output_list of a dependency_clause Output := First (Choices (Clause)); @@ -9644,6 +9667,7 @@ Analyze_Input_Output (Item => Output, Is_Input => False, + Self_Ref => Self_Ref, Top_Level => True, Seen => Outputs_Seen, Null_Seen => Null_Output_Seen); @@ -9653,15 +9677,6 @@ -- Process the input_list of a dependency_clause - Inputs := Expression (Clause); - - -- An input list with a self-dependency appears as operator "+" - -- where the actuals inputs are the right operand. - - if Nkind (Inputs) = N_Op_Plus then - Inputs := Right_Opnd (Inputs); - end if; - Analyze_Input_List (Inputs); end Analyze_Dependency_Clause; @@ -9717,9 +9732,12 @@ procedure Check_Mode (Item : Node_Id; Item_Id : Entity_Id; - Is_Input : Boolean) + Is_Input : Boolean; + Self_Ref : Boolean) is begin + -- Input + if Is_Input then if Ekind (Item_Id) = E_Out_Parameter or else (Global_Seen @@ -9729,17 +9747,37 @@ ("item & must have mode in or in out", Item, Item_Id); end if; - -- Output + -- Self-referential output - else - if Ekind (Item_Id) = E_In_Parameter - or else - (Global_Seen - and then not Appears_In (Subp_Outputs, Item_Id)) - then + elsif Self_Ref then + + -- A self-referential state or variable must appear in both + -- input and output lists of a subprogram. + + if Ekind_In (Item_Id, E_Abstract_State, E_Variable) then + if Global_Seen + and then not Appears_In (Subp_Inputs, Item_Id) + then + Error_Msg_NE + ("item & must have mode in out", Item, Item_Id); + end if; + + -- Self-referential parameter + + elsif Ekind (Item_Id) /= E_In_Out_Parameter then Error_Msg_NE - ("item & must have mode out or in out", Item, Item_Id); + ("item & must have mode in out", Item, Item_Id); end if; + + -- Regular output + + elsif Ekind (Item_Id) = E_In_Parameter + or else + (Global_Seen + and then not Appears_In (Subp_Outputs, Item_Id)) + then + Error_Msg_NE + ("item & must have mode out or in out", Item, Item_Id); end if; end Check_Mode;