This patch provides the initial implementation of aspect Global. This construct
is intended for formal verification proofs.
The syntax of the aspect is as follows:
global_specification ::= (moded_global_list {, moded_global_list})
| global_list
| null
moded_global_list ::= mode_selector => global_list
global_list ::= global_item
| (global_item {, global_item})
mode_selector ::= Input | Output | In_Out | Contract_In
global_item ::= name
The semantics of the aspect are as follows:
A global_item of a subprogram shall be a stand alone variable object [that is,
it is not part of a larger object] or it shall be a state abstraction. Each
mode_selector shall occur at most once in a single Global aspect. A function
subprogram may not have a mode_selector of Output or In_Out in its Global
aspect. Global_items in the same Global aspect shall denote distinct entities.
A global item occurring in a Global aspect of a subprogram aspect specification
shall not have the same defining_identifier as a formal parameter of the
subprogram. A global item of mode in out or out shall not be a Volatile Input
state abstraction (see Abstract State Aspect). A global item of mode in or in
out shall not be a Volatile Output state abstraction.
This patch also corrects the timing of pragma Abstract_State analysis.
------------
-- Source --
------------
-- semantics.ads
package Semantics
with Abstract_State =>
((Input_State with Volatile, Input),
(Output_State with Volatile, Output))
is
type Composite is record
Comp : Integer;
end record;
Var : Composite;
type Composite_Array is array (1 .. 5) of Composite;
Arr : Composite_Array;
procedure Dummy_Proc;
procedure OK_1
with Global => (Var, Input_State);
procedure Error_1
with Global =>
(Var.Comp,
Arr (2),
Dummy_Proc);
procedure OK_2
with Global =>
(Input => (Var, Input_State),
Output => Arr);
procedure Error_2
with Global =>
(Input => Var,
Contract_In => Input_State,
Input => Arr);
function OK_3 return Boolean
with Global =>
(Input => Var,
Contract_In => Input_State);
function Error_3 return Boolean
with Global =>
(In_Out => Arr,
Output => Var);
procedure Error_4
with Global =>
(Input => Semantics.Var,
Output => Var);
function Error_5 (Formal : Boolean) return Boolean
with Global => Formal;
procedure Error_6
with Global => (In_Out => Input_State);
procedure Error_7
with Global => (Output => Input_State);
procedure Error_8
with Global => (In_Out => Output_State);
procedure Error_9
with Global => (Input => Output_State);
procedure Error_10
with Global => Output_State;
procedure OK_4
with Global => null;
procedure Error_11
with Global => (null, Var);
procedure Error_12
with Global => (Var, null, Arr);
procedure Error_13
with Global => (Var, null);
end Semantics;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnat12 -gnatd.V semantics.ads
semantics.ads:19:12: global item must denote variable or state
semantics.ads:20:09: global item must denote variable or state
semantics.ads:21:09: global item must denote variable or state
semantics.ads:30:09: duplicate global mode
semantics.ads:37:09: global mode "In_Out" not applicable to functions
semantics.ads:38:09: global mode "Output" not applicable to functions
semantics.ads:42:19: duplicate global item
semantics.ads:44:21: global item cannot reference formal parameter
semantics.ads:46:32: global item of mode In_Out or Output cannot reference
Volatile Input state
semantics.ads:48:32: global item of mode In_Out or Output cannot reference
Volatile Input state
semantics.ads:50:32: global item of mode In_Out or Input cannot reference
Volatile Output state
semantics.ads:52:31: global item of mode In_Out or Input cannot reference
Volatile Output state
semantics.ads:54:21: global item of mode In_Out or Input cannot reference
Volatile Output state
semantics.ads:58:22: cannot mix null and non-null global items
semantics.ads:60:27: cannot mix null and non-null global items
semantics.ads:62:27: cannot mix null and non-null global items
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-01-04 Hristian Kirtchev <[email protected]>
* aspects.adb, aspects.ads: Add Aspect_Global to all relevant tables.
* par-prag.adb: Add pragma Global to the list of pragmas that
do not need special processing by the parser.
* sem_ch13.adb (Analyze_Aspect_Specifications): Convert aspect
Global into a pragma without any form of legality checks. The
work is done by Analyze_Pragma. The aspect and pragma are both
marked as needing delayed processing. Insert the corresponding
pragma of aspect Abstract_State in the visible declarations of the
related package.
(Check_Aspect_At_Freeze_Point): Aspect Global
does not need processing even though it is marked as delayed.
Alphabetize the list on aspect names.
* sem_prag.adb: Add a value for pragma Global in table Sig_Flags.
(Analyze_Pragma): Add ??? comment about the grammar of pragma
Abstract_State. Move the error location from the pragma to the
state to improve the quality of error placement. Add legality
checks for pragma Global.
* snames.ads-tmpl Add the following specially recognized names
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 194888)
+++ sem_prag.adb (working copy)
@@ -789,6 +789,8 @@
procedure S14_Pragma;
-- Called for all pragmas defined for formal verification to check that
-- the S14_Extensions flag is set.
+ -- This name needs fixing ??? There is no such thing as an
+ -- "S14_Extensions" flag ???
function Is_Before_First_Decl
(Pragma_Node : Node_Id;
@@ -6644,6 +6646,8 @@
-- Abstract_State --
--------------------
+ -- ??? no formal grammar available yet
+
when Pragma_Abstract_State => Abstract_State : declare
Pack_Id : Entity_Id;
@@ -6824,7 +6828,7 @@
-- Any other attempt to declare a state is erroneous
else
- Error_Msg_N ("malformed abstract state declaration", N);
+ Error_Msg_N ("malformed abstract state declaration", State);
end if;
-- Do not generate a state abstraction entity if it was not
@@ -9946,6 +9950,362 @@
end if;
end Float_Representation;
+ ------------
+ -- Global --
+ ------------
+
+ -- ??? no formal grammar pragma available yet
+
+ when Pragma_Global => Global : declare
+ Subp_Id : Entity_Id;
+
+ Seen : Elist_Id := No_Elist;
+ -- A list containing the entities of all the items processed so
+ -- far. It plays a role in detecting distinct entities.
+
+ -- Flags used to verify the consistency of modes
+
+ Contract_Seen : Boolean := False;
+ In_Out_Seen : Boolean := False;
+ Input_Seen : Boolean := False;
+ Output_Seen : Boolean := False;
+
+ procedure Analyze_Global_List
+ (List : Node_Id;
+ Global_Mode : Name_Id := Name_Input);
+ -- Verify the legality of a single global list declaration.
+ -- Global_Mode denotes the current mode in effect.
+
+ -------------------------
+ -- Analyze_Global_List --
+ -------------------------
+
+ procedure Analyze_Global_List
+ (List : Node_Id;
+ Global_Mode : Name_Id := Name_Input)
+ is
+ procedure Analyze_Global_Item
+ (Item : Node_Id;
+ Global_Mode : Name_Id);
+ -- Verify the legality of a single global item declaration.
+ -- Global_Mode denotes the current mode in effect.
+
+ procedure Check_Duplicate_Mode
+ (Mode : Node_Id;
+ Status : in out Boolean);
+ -- Flag Status denotes whether a particular mode has been seen
+ -- while processing a global list. This routine verifies that
+ -- Mode is not a duplicate mode and sets the flag Status.
+
+ procedure Check_Mode_Restriction_In_Function (Mode : Node_Id);
+ -- Mode denotes either In_Out or Output. Depending on the kind
+ -- of the related subprogram, emit an error if those two modes
+ -- apply to a function.
+
+ -------------------------
+ -- Analyze_Global_Item --
+ -------------------------
+
+ procedure Analyze_Global_Item
+ (Item : Node_Id;
+ Global_Mode : Name_Id)
+ is
+ function Is_Duplicate_Item (Id : Entity_Id) return Boolean;
+ -- Determine whether Id has already been processed
+
+ -----------------------
+ -- Is_Duplicate_Item --
+ -----------------------
+
+ function Is_Duplicate_Item (Id : Entity_Id) return Boolean is
+ Item_Elmt : Elmt_Id;
+
+ begin
+ if Present (Seen) then
+ Item_Elmt := First_Elmt (Seen);
+ while Present (Item_Elmt) loop
+ if Node (Item_Elmt) = Id then
+ return True;
+ end if;
+
+ Next_Elmt (Item_Elmt);
+ end loop;
+ end if;
+
+ return False;
+ end Is_Duplicate_Item;
+
+ -- Local declarations
+
+ Id : Entity_Id;
+
+ -- Start of processing for Analyze_Global_Item
+
+ begin
+ -- Detect one of the following cases
+
+ -- with Global => (null, Name)
+ -- with Global => (Name_1, null, Name_2)
+ -- with Global => (Name, null)
+
+ if Nkind (Item) = N_Null then
+ Error_Msg_N
+ ("cannot mix null and non-null global items", Item);
+ return;
+ end if;
+
+ -- Ensure that the formal parameters are visible when
+ -- processing an item. This falls out of the general rule
+ -- of aspects pertaining to subprogram declarations.
+
+ Push_Scope (Subp_Id);
+ Install_Formals (Subp_Id);
+ Analyze (Item);
+ Pop_Scope;
+
+ if Is_Entity_Name (Item) then
+ Id := Entity (Item);
+
+ -- A global item cannot reference a formal parameter. Do
+ -- this check first to provide a better error diagnostic.
+
+ if Is_Formal (Id) then
+ Error_Msg_N
+ ("global item cannot reference formal parameter",
+ Item);
+ return;
+
+ -- The only legal references are those to abstract states
+ -- and variables.
+
+ elsif not Ekind_In (Entity (Item), E_Abstract_State,
+ E_Variable)
+ then
+ Error_Msg_N
+ ("global item must denote variable or state", Item);
+ return;
+ end if;
+
+ -- Some form of illegal construct masquerading as a name
+
+ else
+ Error_Msg_N
+ ("global item must denote variable or state", Item);
+ return;
+ end if;
+
+ -- The same entity might be referenced through various way.
+ -- Check the entity of the item rather than the item itself.
+
+ if Is_Duplicate_Item (Id) then
+ Error_Msg_N ("duplicate global item", Item);
+
+ -- Add the entity of the current item to the list of
+ -- processed items.
+
+ else
+ if No (Seen) then
+ Seen := New_Elmt_List;
+ end if;
+
+ Append_Elmt (Id, Seen);
+ end if;
+
+ if Ekind (Id) = E_Abstract_State
+ and then Is_Volatile_State (Id)
+ then
+ -- A global item of mode In_Out or Output cannot denote a
+ -- volatile Input state.
+
+ if Is_Input_State (Id)
+ and then (Global_Mode = Name_In_Out
+ or else
+ Global_Mode = Name_Output)
+ then
+ Error_Msg_N
+ ("global item of mode In_Out or Output cannot " &
+ "reference Volatile Input state", Item);
+
+ -- A global item of mode In_Out or Input cannot reference
+ -- a volatile Output state.
+
+ elsif Is_Output_State (Id)
+ and then (Global_Mode = Name_In_Out
+ or else
+ Global_Mode = Name_Input)
+ then
+ Error_Msg_N
+ ("global item of mode In_Out or Input cannot "
+ & "reference Volatile Output state", Item);
+ end if;
+ end if;
+ end Analyze_Global_Item;
+
+ --------------------------
+ -- Check_Duplicate_Mode --
+ --------------------------
+
+ procedure Check_Duplicate_Mode
+ (Mode : Node_Id;
+ Status : in out Boolean)
+ is
+ begin
+ if Status then
+ Error_Msg_N ("duplicate global mode", Mode);
+ end if;
+
+ Status := True;
+ end Check_Duplicate_Mode;
+
+ ----------------------------------------
+ -- Check_Mode_Restriction_In_Function --
+ ----------------------------------------
+
+ procedure Check_Mode_Restriction_In_Function (Mode : Node_Id) is
+ begin
+ if Ekind (Subp_Id) = E_Function then
+ Error_Msg_Name_1 := Chars (Mode);
+ Error_Msg_N
+ ("global mode % not applicable to functions", Mode);
+ end if;
+ end Check_Mode_Restriction_In_Function;
+
+ -- Local variables
+
+ Assoc : Node_Id;
+ Item : Node_Id;
+ Mode : Node_Id;
+
+ -- Start of processing for Analyze_Global_List
+
+ begin
+ -- Single global item declaration
+
+ if Nkind_In (List, N_Identifier, N_Selected_Component) then
+ Analyze_Global_Item (List, Global_Mode);
+
+ -- Simple global list or moded global list declaration
+
+ elsif Nkind (List) = N_Aggregate then
+
+ -- The declaration of a simple global list appear as a
+ -- collection of expressions.
+
+ if Present (Expressions (List)) then
+ if Present (Component_Associations (List)) then
+ Error_Msg_N
+ ("cannot mix moded and non-moded global lists",
+ List);
+ end if;
+
+ Item := First (Expressions (List));
+ while Present (Item) loop
+ Analyze_Global_Item (Item, Global_Mode);
+
+ Next (Item);
+ end loop;
+
+ -- The declaration of a moded global list appears as a
+ -- collection of component associations where individual
+ -- choices denote modes.
+
+ elsif Present (Component_Associations (List)) then
+ if Present (Expressions (List)) then
+ Error_Msg_N
+ ("cannot mix moded and non-moded global lists",
+ List);
+ end if;
+
+ Assoc := First (Component_Associations (List));
+ while Present (Assoc) loop
+ Mode := First (Choices (Assoc));
+
+ if Nkind (Mode) = N_Identifier then
+ if Chars (Mode) = Name_Contract_In then
+ Check_Duplicate_Mode (Mode, Contract_Seen);
+
+ elsif Chars (Mode) = Name_In_Out then
+ Check_Duplicate_Mode (Mode, In_Out_Seen);
+ Check_Mode_Restriction_In_Function (Mode);
+
+ elsif Chars (Mode) = Name_Input then
+ Check_Duplicate_Mode (Mode, Input_Seen);
+
+ elsif Chars (Mode) = Name_Output then
+ Check_Duplicate_Mode (Mode, Output_Seen);
+ Check_Mode_Restriction_In_Function (Mode);
+
+ else
+ Error_Msg_N ("invalid mode selector", Mode);
+ end if;
+
+ else
+ Error_Msg_N ("invalid mode selector", Mode);
+ end if;
+
+ -- Items in a moded list appear as a collection of
+ -- expressions. Reuse the existing machinery to
+ -- analyze them.
+
+ Analyze_Global_List
+ (List => Expression (Assoc),
+ Global_Mode => Chars (Mode));
+
+ Next (Assoc);
+ end loop;
+
+ -- Something went horribly wrong, we have a malformed tree
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Any other attempt to declare a global item is erroneous
+
+ else
+ Error_Msg_N ("malformed global list declaration", List);
+ end if;
+ end Analyze_Global_List;
+
+ -- Local variables
+
+ List : Node_Id;
+ Subp : Node_Id;
+
+ -- Start of processing for Global
+
+ begin
+ GNAT_Pragma;
+ S14_Pragma;
+ Check_Arg_Count (1);
+
+ -- Ensure the proper placement of the pragma. Global must be
+ -- associated with a subprogram declaration.
+
+ Subp := Parent (Corresponding_Aspect (N));
+
+ if Nkind (Subp) /= N_Subprogram_Declaration then
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Subp_Id := Defining_Unit_Name (Specification (Subp));
+ List := Expression (Arg1);
+
+ -- There is nothing to be done for a null global list
+
+ if Nkind (List) = N_Null then
+ null;
+
+ -- Analyze the various forms of global lists and items. Note that
+ -- some of these may be malformed in which case the analysis emits
+ -- error messages.
+
+ else
+ Analyze_Global_List (List);
+ end if;
+ end Global;
+
-----------
-- Ident --
-----------
@@ -16093,6 +16453,7 @@
Pragma_Fast_Math => -1,
Pragma_Finalize_Storage_Only => 0,
Pragma_Float_Representation => 0,
+ Pragma_Global => -1,
Pragma_Ident => -1,
Pragma_Implementation_Defined => -1,
Pragma_Implemented => -1,
Index: aspects.adb
===================================================================
--- aspects.adb (revision 194851)
+++ aspects.adb (working copy)
@@ -269,6 +269,7 @@
Aspect_External_Name => Aspect_External_Name,
Aspect_External_Tag => Aspect_External_Tag,
Aspect_Favor_Top_Level => Aspect_Favor_Top_Level,
+ Aspect_Global => Aspect_Global,
Aspect_Implicit_Dereference => Aspect_Implicit_Dereference,
Aspect_Import => Aspect_Import,
Aspect_Independent => Aspect_Independent,
Index: aspects.ads
===================================================================
--- aspects.ads (revision 194851)
+++ aspects.ads (working copy)
@@ -94,6 +94,7 @@
Aspect_Dynamic_Predicate,
Aspect_External_Name,
Aspect_External_Tag,
+ Aspect_Global, -- GNAT
Aspect_Implicit_Dereference,
Aspect_Input,
Aspect_Interrupt_Priority,
@@ -231,6 +232,7 @@
Aspect_Dimension => True,
Aspect_Dimension_System => True,
Aspect_Favor_Top_Level => True,
+ Aspect_Global => True,
Aspect_Inline_Always => True,
Aspect_Lock_Free => True,
Aspect_Object_Size => True,
@@ -327,6 +329,7 @@
Aspect_Dynamic_Predicate => Expression,
Aspect_External_Name => Expression,
Aspect_External_Tag => Expression,
+ Aspect_Global => Expression,
Aspect_Implicit_Dereference => Name,
Aspect_Input => Name,
Aspect_Interrupt_Priority => Expression,
@@ -404,6 +407,7 @@
Aspect_External_Tag => Name_External_Tag,
Aspect_Export => Name_Export,
Aspect_Favor_Top_Level => Name_Favor_Top_Level,
+ Aspect_Global => Name_Global,
Aspect_Implicit_Dereference => Name_Implicit_Dereference,
Aspect_Import => Name_Import,
Aspect_Independent => Name_Independent,
Index: par-prag.adb
===================================================================
--- par-prag.adb (revision 194851)
+++ par-prag.adb (working copy)
@@ -1156,6 +1156,7 @@
Pragma_Fast_Math |
Pragma_Finalize_Storage_Only |
Pragma_Float_Representation |
+ Pragma_Global |
Pragma_Ident |
Pragma_Implementation_Defined |
Pragma_Implemented |
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 194888)
+++ sem_ch13.adb (working copy)
@@ -1436,7 +1436,7 @@
-- Case 2d : Aspects that correspond to a pragma with one
-- argument.
- when Aspect_Abstract_State =>
+ when Aspect_Abstract_State =>
Aitem :=
Make_Pragma (Loc,
Pragma_Identifier =>
@@ -1447,11 +1447,24 @@
Delay_Required := False;
- when Aspect_Relative_Deadline =>
+ -- Aspect Global must be delayed because it can mention names
+ -- and benefit from the forward visibility rules applicable to
+ -- aspects of subprograms.
+
+ when Aspect_Global =>
Aitem :=
Make_Pragma (Loc,
+ Pragma_Identifier =>
+ Make_Identifier (Sloc (Id), Name_Global),
Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))));
+
+ when Aspect_Relative_Deadline =>
+ Aitem :=
+ Make_Pragma (Loc,
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
Expression => Relocate_Node (Expr))),
Pragma_Identifier =>
Make_Identifier (Sloc (Id), Name_Relative_Deadline));
@@ -1950,6 +1963,20 @@
Prepend (Aitem, Declarations (N));
+ -- Aspect Abstract_State produces implicit declarations for
+ -- all state abstraction entities it defines. To emulate
+ -- this behavior, insert the pragma at the start of the
+ -- visible declarations of the related package.
+
+ elsif Nam = Name_Abstract_State
+ and then Nkind (N) = N_Package_Declaration
+ then
+ if No (Visible_Declarations (Specification (N))) then
+ Set_Visible_Declarations (Specification (N), New_List);
+ end if;
+
+ Prepend (Aitem, Visible_Declarations (Specification (N)));
+
else
if No (Pragmas_After (Aux)) then
Set_Pragmas_After (Aux, New_List);
@@ -6887,33 +6914,33 @@
Library_Unit_Aspects =>
T := Standard_Boolean;
+ -- Aspects corresponding to attribute definition clauses
+
+ when Aspect_Address =>
+ T := RTE (RE_Address);
+
when Aspect_Attach_Handler =>
T := RTE (RE_Interrupt_ID);
+ when Aspect_Bit_Order | Aspect_Scalar_Storage_Order =>
+ T := RTE (RE_Bit_Order);
+
when Aspect_Convention =>
return;
- -- Default_Value is resolved with the type entity in question
+ when Aspect_CPU =>
+ T := RTE (RE_CPU_Range);
- when Aspect_Default_Value =>
- T := Entity (ASN);
-
-- Default_Component_Value is resolved with the component type
when Aspect_Default_Component_Value =>
T := Component_Type (Entity (ASN));
- -- Aspects corresponding to attribute definition clauses
+ -- Default_Value is resolved with the type entity in question
- when Aspect_Address =>
- T := RTE (RE_Address);
+ when Aspect_Default_Value =>
+ T := Entity (ASN);
- when Aspect_Bit_Order | Aspect_Scalar_Storage_Order =>
- T := RTE (RE_Bit_Order);
-
- when Aspect_CPU =>
- T := RTE (RE_CPU_Range);
-
when Aspect_Dispatching_Domain =>
T := RTE (RE_Dispatching_Domain);
@@ -6923,6 +6950,14 @@
when Aspect_External_Name =>
T := Standard_String;
+ -- Global is a delayed aspect because it may reference names that
+ -- have not been declared yet. There is no action to be taken with
+ -- respect to the aspect itself as the reference checking is done on
+ -- the corresponding pragma.
+
+ when Aspect_Global =>
+ return;
+
when Aspect_Link_Name =>
T := Standard_String;
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl (revision 194852)
+++ snames.ads-tmpl (working copy)
@@ -494,6 +494,7 @@
Name_Export_Valued_Procedure : constant Name_Id := N + $; -- GNAT
Name_External : constant Name_Id := N + $; -- GNAT
Name_Finalize_Storage_Only : constant Name_Id := N + $; -- GNAT
+ Name_Global : constant Name_Id := N + $; -- GNAT
Name_Ident : constant Name_Id := N + $; -- VMS
Name_Implementation_Defined : constant Name_Id := N + $; -- GNAT
Name_Implemented : constant Name_Id := N + $; -- Ada 12
@@ -673,6 +674,7 @@
Name_Code : constant Name_Id := N + $;
Name_Component : constant Name_Id := N + $;
Name_Component_Size_4 : constant Name_Id := N + $;
+ Name_Contract_In : constant Name_Id := N + $;
Name_Copy : constant Name_Id := N + $;
Name_D_Float : constant Name_Id := N + $;
Name_Decreases : constant Name_Id := N + $;
@@ -695,6 +697,7 @@
Name_GPL : constant Name_Id := N + $;
Name_IEEE_Float : constant Name_Id := N + $;
Name_Ignore : constant Name_Id := N + $;
+ Name_In_Out : constant Name_Id := N + $;
Name_Increases : constant Name_Id := N + $;
Name_Info : constant Name_Id := N + $;
Name_Integrity : constant Name_Id := N + $;
@@ -1771,6 +1774,7 @@
Pragma_Export_Valued_Procedure,
Pragma_External,
Pragma_Finalize_Storage_Only,
+ Pragma_Global,
Pragma_Ident,
Pragma_Implementation_Defined,
Pragma_Implemented,
