From patchwork Tue Aug 2 15:21:29 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 107946 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]) by ozlabs.org (Postfix) with SMTP id 5B798B6F8F for ; Wed, 3 Aug 2011 01:21:52 +1000 (EST) Received: (qmail 3934 invoked by alias); 2 Aug 2011 15:21:50 -0000 Received: (qmail 3924 invoked by uid 22791); 2 Aug 2011 15:21:47 -0000 X-SWARE-Spam-Status: No, hits=-1.7 required=5.0 tests=AWL,BAYES_00,TW_TM X-Spam-Check-By: sourceware.org Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Tue, 02 Aug 2011 15:21:30 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 93BBE2BAB86; Tue, 2 Aug 2011 11:21:29 -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 eBiuQ9OdPzup; Tue, 2 Aug 2011 11:21:29 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 71ED52BAB7A; Tue, 2 Aug 2011 11:21:29 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 6F6563FEE8; Tue, 2 Aug 2011 11:21:29 -0400 (EDT) Date: Tue, 2 Aug 2011 11:21:29 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Recognize HIDE directive in SPARK as special comment Message-ID: <20110802152129.GA13862@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) 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 In SPARK, some parts of code that are ignored in the analysis can be "hidden", through the use of a HIDE directive formatted as a special comment. There is no benefit in detecting violations of SPARK restriction in such hidden parts, so we now recognize the HIDE directive from SPARK and do not report SPARK violations in these hidden parts, using ranges of source-locations to record hidden parts as is done for pragma Warnings (On|Off). Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-02 Yannick Moy * par-ch11.adb (P_Handled_Sequence_Of_Statements): mark a sequence of statements hidden in SPARK if preceded by the HIDE directive (Parse_Exception_Handlers): mark each exception handler in a sequence of exception handlers as hidden in SPARK if preceded by the HIDE directive * par-ch6.adb (P_Subprogram): mark a subprogram body hidden in SPARK if starting with the HIDE directive * par-ch7.adb (P_Package): mark a package body hidden in SPARK if starting with the HIDE directive; mark the declarations in a private part as hidden in SPARK if the private part starts with the HIDE directive * restrict.adb, restrict.ads (Set_Hidden_Part_In_SPARK): record a range of slocs as hidden in SPARK (Is_In_Hidden_Part_In_SPARK): new function which returns whether its argument node belongs to a part which is hidden in SPARK (Check_SPARK_Restriction): do not issue violations on nodes in hidden parts in SPARK; protect the possibly costly call to Is_In_Hidden_Part_In_SPARK by a check that the SPARK restriction is on * scans.ads (Token_Type): new value Tok_SPARK_Hide in enumeration * scng.adb (Accumulate_Token_Checksum_GNAT_6_3, Accumulate_Token_Checksum_GNAT_5_03): add case for new token Tok_SPARK_Hide. (Scan): recognize special comment starting with '#' and followed by SPARK keyword "hide" as a HIDE directive. Index: par-ch11.adb =================================================================== --- par-ch11.adb (revision 176998) +++ par-ch11.adb (working copy) @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2011, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -56,11 +56,28 @@ -- Error_Recovery : Cannot raise Error_Resync function P_Handled_Sequence_Of_Statements return Node_Id is - Handled_Stmt_Seq_Node : Node_Id; + Handled_Stmt_Seq_Node : Node_Id; + Seq_Is_Hidden_In_SPARK : Boolean; + Hidden_Region_Start : Source_Ptr; begin Handled_Stmt_Seq_Node := New_Node (N_Handled_Sequence_Of_Statements, Token_Ptr); + + -- In SPARK, a HIDE directive can be placed at the beginning of a + -- package initialization, thus hiding the sequence of statements (and + -- possible exception handlers) from SPARK tool-set. No violation of the + -- SPARK restriction should be issued on nodes in a hidden part, which + -- is obtained by marking such hidden parts. + + if Token = Tok_SPARK_Hide then + Seq_Is_Hidden_In_SPARK := True; + Hidden_Region_Start := Token_Ptr; + Scan; -- past HIDE directive + else + Seq_Is_Hidden_In_SPARK := False; + end if; + Set_Statements (Handled_Stmt_Seq_Node, P_Sequence_Of_Statements (SS_Extm_Sreq)); @@ -70,6 +87,10 @@ (Handled_Stmt_Seq_Node, Parse_Exception_Handlers); end if; + if Seq_Is_Hidden_In_SPARK then + Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr); + end if; + return Handled_Stmt_Seq_Node; end P_Handled_Sequence_Of_Statements; @@ -229,10 +250,26 @@ -- Error recovery: cannot raise Error_Resync function Parse_Exception_Handlers return List_Id is - Handler : Node_Id; - Handlers_List : List_Id; + Handler : Node_Id; + Handlers_List : List_Id; + Handler_Is_Hidden_In_SPARK : Boolean; + Hidden_Region_Start : Source_Ptr; begin + -- In SPARK, a HIDE directive can be placed at the beginning of a + -- sequence of exception handlers for a subprogram implementation, thus + -- hiding the exception handlers from SPARK tool-set. No violation of + -- the SPARK restriction should be issued on nodes in a hidden part, + -- which is obtained by marking such hidden parts. + + if Token = Tok_SPARK_Hide then + Handler_Is_Hidden_In_SPARK := True; + Hidden_Region_Start := Token_Ptr; + Scan; -- past HIDE directive + else + Handler_Is_Hidden_In_SPARK := False; + end if; + Handlers_List := New_List; P_Pragmas_Opt (Handlers_List); @@ -253,6 +290,10 @@ end loop; end if; + if Handler_Is_Hidden_In_SPARK then + Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr); + end if; + return Handlers_List; end Parse_Exception_Handlers; Index: scng.adb =================================================================== --- scng.adb (revision 176998) +++ scng.adb (working copy) @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2011, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -184,7 +184,7 @@ Tok_Separate | Tok_EOF | Tok_Semicolon | Tok_Arrow | Tok_Vertical_Bar | Tok_Dot_Dot | Tok_Project | Tok_Extends | Tok_External | Tok_External_As_List | Tok_Comment | - Tok_End_Of_Line | Tok_Special | No_Token => + Tok_End_Of_Line | Tok_Special | Tok_SPARK_Hide | No_Token => System.CRC32.Update (System.CRC32.CRC32 (Checksum), @@ -249,7 +249,7 @@ Tok_Separate | Tok_EOF | Tok_Semicolon | Tok_Arrow | Tok_Vertical_Bar | Tok_Dot_Dot | Tok_Project | Tok_Extends | Tok_External | Tok_External_As_List | Tok_Comment | - Tok_End_Of_Line | Tok_Special | No_Token => + Tok_End_Of_Line | Tok_Special | Tok_SPARK_Hide | No_Token => System.CRC32.Update (System.CRC32.CRC32 (Checksum), @@ -1761,6 +1761,42 @@ Token := Tok_Comment; return; end if; + + if Source (Start_Of_Comment) = '#' then + declare + Scan_SPARK_Ptr : Source_Ptr; + + begin + Scan_SPARK_Ptr := Start_Of_Comment + 1; + + -- Scan out blanks + + while Source (Scan_SPARK_Ptr) = ' ' + or else Source (Scan_SPARK_Ptr) = HT + loop + Scan_SPARK_Ptr := Scan_SPARK_Ptr + 1; + end loop; + + -- Recognize HIDE directive. SPARK input cannot be + -- encoded as wide characters, so only deal with + -- lower/upper case. + + if (Source (Scan_SPARK_Ptr) = 'h' + or else Source (Scan_SPARK_Ptr) = 'H') + and then (Source (Scan_SPARK_Ptr + 1) = 'i' + or else Source (Scan_SPARK_Ptr + 1) = 'I') + and then (Source (Scan_SPARK_Ptr + 2) = 'd' + or else Source (Scan_SPARK_Ptr + 2) = 'D') + and then (Source (Scan_SPARK_Ptr + 3) = 'e' + or else Source (Scan_SPARK_Ptr + 3) = 'E') + and then (Source (Scan_SPARK_Ptr + 4) = ' ' + or else Source (Scan_SPARK_Ptr + 4) = HT) + then + Token := Tok_SPARK_Hide; + return; + end if; + end; + end if; end if; end Minus_Case; Index: scans.ads =================================================================== --- scans.ads (revision 176998) +++ scans.ads (working copy) @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2011, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -213,6 +213,9 @@ -- characters '#', '$', '?', '@', '`', '\', '^', '~', or '_'. The -- character value itself is stored in Scans.Special_Character. + Tok_SPARK_Hide, + -- HIDE directive in SPARK + No_Token); -- No_Token is used for initializing Token values to indicate that -- no value has been set yet. Index: par-ch6.adb =================================================================== --- par-ch6.adb (revision 177125) +++ par-ch6.adb (working copy) @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2011, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -628,6 +628,9 @@ else Scan_Body_Or_Expression_Function : declare + Body_Is_Hidden_In_SPARK : Boolean; + Hidden_Region_Start : Source_Ptr; + function Likely_Expression_Function return Boolean; -- Returns True if we have a probable case of an expression -- function omitting the parentheses, if so, returns True @@ -770,7 +773,26 @@ Body_Node := New_Node (N_Subprogram_Body, Sloc (Specification_Node)); Set_Specification (Body_Node, Specification_Node); + + -- In SPARK, a HIDE directive can be placed at the beginning + -- of a subprogram implementation, thus hiding the + -- subprogram body from SPARK tool-set. No violation of the + -- SPARK restriction should be issued on nodes in a hidden + -- part, which is obtained by marking such hidden parts. + + if Token = Tok_SPARK_Hide then + Body_Is_Hidden_In_SPARK := True; + Hidden_Region_Start := Token_Ptr; + Scan; -- past HIDE directive + else + Body_Is_Hidden_In_SPARK := False; + end if; + Parse_Decls_Begin_End (Body_Node); + + if Body_Is_Hidden_In_SPARK then + Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr); + end if; end if; return Body_Node; Index: restrict.adb =================================================================== --- restrict.adb (revision 177177) +++ restrict.adb (working copy) @@ -119,6 +119,12 @@ begin if Force or else Comes_From_Source (N) then + if Restriction_Check_Required (SPARK) + and then Is_In_Hidden_Part_In_SPARK (Sloc (N)) + then + return; + end if; + -- Since the call to Restriction_Msg from Check_Restriction may set -- Error_Msg_Sloc to the location of the pragma restriction, save and -- restore the previous value of the global variable around the call. @@ -141,6 +147,12 @@ if Comes_From_Source (N) then + if Restriction_Check_Required (SPARK) + and then Is_In_Hidden_Part_In_SPARK (Sloc (N)) + then + return; + end if; + -- Since the call to Restriction_Msg from Check_Restriction may set -- Error_Msg_Sloc to the location of the pragma restriction, save and -- restore the previous value of the global variable around the call. @@ -548,6 +560,25 @@ return Not_A_Restriction_Id; end Get_Restriction_Id; + -------------------------------- + -- Is_In_Hidden_Part_In_SPARK -- + -------------------------------- + + function Is_In_Hidden_Part_In_SPARK (Loc : Source_Ptr) return Boolean is + begin + -- Loop through table of hidden ranges + + for J in SPARK_Hides.First .. SPARK_Hides.Last loop + if SPARK_Hides.Table (J).Start <= Loc + and then Loc <= SPARK_Hides.Table (J).Stop + then + return True; + end if; + end loop; + + return False; + end Is_In_Hidden_Part_In_SPARK; + ------------------------------- -- No_Exception_Handlers_Set -- ------------------------------- @@ -841,6 +872,17 @@ end Same_Unit; ------------------------------ + -- Set_Hidden_Part_In_SPARK -- + ------------------------------ + + procedure Set_Hidden_Part_In_SPARK (Loc1, Loc2 : Source_Ptr) is + begin + SPARK_Hides.Increment_Last; + SPARK_Hides.Table (SPARK_Hides.Last).Start := Loc1; + SPARK_Hides.Table (SPARK_Hides.Last).Stop := Loc2; + end Set_Hidden_Part_In_SPARK; + + ------------------------------ -- Set_Profile_Restrictions -- ------------------------------ Index: restrict.ads =================================================================== --- restrict.ads (revision 177175) +++ restrict.ads (working copy) @@ -174,6 +174,30 @@ Table_Increment => 200, Table_Name => "Name_No_Dependence"); + ------------------------------- + -- SPARK Restriction Control -- + ------------------------------- + + -- SPARK HIDE directives allow turning off SPARK restriction for a + -- specified region of code, and the following tables are the data + -- structures used to keep track of these regions. + + -- The table contains pairs of source locations, the first being the start + -- location for hidden region, and the second being the end location. + + type SPARK_Hide_Entry is record + Start : Source_Ptr; + Stop : Source_Ptr; + end record; + + package SPARK_Hides is new Table.Table ( + Table_Component_Type => SPARK_Hide_Entry, + Table_Index_Type => Natural, + Table_Low_Bound => 1, + Table_Initial => 100, + Table_Increment => 200, + Table_Name => "SPARK Hides"); + ----------------- -- Subprograms -- ----------------- @@ -289,6 +313,10 @@ -- identifier, and if so returns the corresponding Restriction_Id -- value, otherwise returns Not_A_Restriction_Id. + function Is_In_Hidden_Part_In_SPARK (Loc : Source_Ptr) return Boolean; + -- Determine if given location is covered by a hidden region range in the + -- SPARK hides table. + function No_Exception_Handlers_Set return Boolean; -- Test to see if current restrictions settings specify that no exception -- handlers are present. This function is called by Gigi when it needs to @@ -334,6 +362,9 @@ -- of individual Restrictions pragmas). Returns True only if all the -- required restrictions are set. + procedure Set_Hidden_Part_In_SPARK (Loc1, Loc2 : Source_Ptr); + -- Insert a new hidden region range in the SPARK hides table + procedure Set_Profile_Restrictions (P : Profile_Name; N : Node_Id; Index: par-ch7.adb =================================================================== --- par-ch7.adb (revision 177086) +++ par-ch7.adb (working copy) @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2011, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -110,6 +110,10 @@ -- Dummy node to attach aspect specifications to until we properly -- figure out where they eventually belong. + Body_Is_Hidden_In_SPARK : Boolean; + Private_Part_Is_Hidden_In_SPARK : Boolean; + Hidden_Region_Start : Source_Ptr; + begin Push_Scope_Stack; Scope.Table (Scope.Last).Etyp := E_Name; @@ -153,7 +157,26 @@ else Package_Node := New_Node (N_Package_Body, Package_Sloc); Set_Defining_Unit_Name (Package_Node, Name_Node); + + -- In SPARK, a HIDE directive can be placed at the beginning of a + -- package implementation, thus hiding the package body from SPARK + -- tool-set. No violation of the SPARK restriction should be + -- issued on nodes in a hidden part, which is obtained by marking + -- such hidden parts. + + if Token = Tok_SPARK_Hide then + Body_Is_Hidden_In_SPARK := True; + Hidden_Region_Start := Token_Ptr; + Scan; -- past HIDE directive + else + Body_Is_Hidden_In_SPARK := False; + end if; + Parse_Decls_Begin_End (Package_Node); + + if Body_Is_Hidden_In_SPARK then + Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr); + end if; end if; -- Cases other than Package_Body @@ -249,9 +272,28 @@ end if; Scan; -- past PRIVATE + + if Token = Tok_SPARK_Hide then + Private_Part_Is_Hidden_In_SPARK := True; + Hidden_Region_Start := Token_Ptr; + Scan; -- past HIDE directive + else + Private_Part_Is_Hidden_In_SPARK := False; + end if; + Set_Private_Declarations (Specification_Node, P_Basic_Declarative_Items); + -- In SPARK, a HIDE directive can be placed at the beginning + -- of a private part, thus hiding all declarations in the + -- private part from SPARK tool-set. No violation of the + -- SPARK restriction should be issued on nodes in a hidden + -- part, which is obtained by marking such hidden parts. + + if Private_Part_Is_Hidden_In_SPARK then + Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr); + end if; + -- Deal gracefully with multiple PRIVATE parts while Token = Tok_Private loop