* [Ada] Recognize HIDE directive in SPARK as special comment
@ 2011-08-02 15:21 Arnaud Charlet
0 siblings, 0 replies; only message in thread
From: Arnaud Charlet @ 2011-08-02 15:21 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
[-- Attachment #1: Type: text/plain, Size: 1870 bytes --]
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 <moy@adacore.com>
* 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.
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 18578 bytes --]
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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2011-08-02 15:21 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2011-08-02 15:21 [Ada] Recognize HIDE directive in SPARK as special comment Arnaud Charlet
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).