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 <kirtc...@adacore.com> * 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,