* [Ada] Aspect Abstract_State
@ 2013-01-03 13:07 Arnaud Charlet
0 siblings, 0 replies; only message in thread
From: Arnaud Charlet @ 2013-01-03 13:07 UTC (permalink / raw)
To: gcc-patches; +Cc: Hristian Kirtchev
[-- Attachment #1: Type: text/plain, Size: 6356 bytes --]
This patch provides the initial implementation of aspect Abstract_State. This
construct is intended for formal verification proofs.
The syntax of the aspect is as follows:
abstract_state_list ::=
null
| state_name_with_properties
| (state_name_with_properties { , state_name_with_properties } )
state_name_with_properties ::=
state_name
| ( state_name with property_list )
property_list ::= property { , property }
property ::= simple_property
| name_value_property
simple_property ::= identifier
name_value_property ::= identifier => expression
state_name ::= defining_identifier
The semantics of the aspect are as follows:
The identifier of a simple_property shall be Volatile, Input, or Output. There
shall be at most one occurrence of the identifiers Volatile, Input and Output
in a single property_list. If a property_list includes Volatile, then it shall
also include exactly one of Input or Output. If a property_list includes either
Input or Output, then it shall also include Volatile. The identifier of a
name_value_property shall be Integrity. If a property_list includes Integrity
then it shall be the final property in the list.
Each state_name occurring in an Abstract_State aspect specification for a given
package P introduces an implicit declaration of a state abstraction entity.
This implicit declaration occurs at the beginning of the visible part of P.
This implicit declaration requires completion.
A state abstraction shall only be named in contexts where this is explicitly
permitted (e.g., as part of a Globals aspect specification), but this is not a
name resolution rule. Thus, the declaration of a state abstraction has the same
visibility as any other declaration. A state abstraction is not an object; it
does not have a type. The completion of a state abstraction declared in a
package aspect_specification can only be provided as part of a Refined_State
aspect specification within the body of the package.
A null abstract_state_list specifies that a package contains no hidden state or
variables declared in its visible_part.
A variable declared in the visible_part of a package implicitly declares a
state abstraction entity with the same identifier as the defining_identifier of
the variable. The variable declaration acts as the completion of the state
abstraction. The implicitly declared state abstraction is only visible in a
limited view of the package.
A volatile state abstraction is one declared with a property list which
includes the Volatile property, and either Input or Output. A Volatile Input or
Output state abstraction represents a sequence of state changes brought about
by reading or writing successive values to or from a volatile variable.
------------
-- Source --
------------
-- semantics.ads
package Semantics is
package OK_1
with Abstract_State => null
is end OK_1;
package OK_2
with Abstract_State =>
(S_1,
(S_2 with Volatile, Input, Integrity => 1),
(S_3 with Output, Volatile, Integrity => 2))
is end OK_2;
package Error_1
with Abstract_State =>
(S_1,
S_1, -- duplicate state name
123, -- junk state name
(123 with Input, Volatile), -- junk state name
(S_2 with Junk_Name), -- junk property
(S_3 with Input, Input), -- duplicate property
(S_4 with Input), -- no Volatile
(S_5 with Output), -- no Volatile
(S_6 with Volatile), -- neither Input nor Output
(S_7 with Volatile, Input, Output), -- can't have Input and Output
(S_8 with Integrity => Junk_Value), -- has to be integer literal
null) -- can't have null or any of the above
is end Error_1;
end Semantics;
-----------------
-- Compilation --
-----------------
$ gcc -c -gnatc -gnat12 -gnatd.V semantics.ads
semantics.ads:14:11: malformed abstract state declaration
semantics.ads:16:09: "S_1" conflicts with declaration at line 15
semantics.ads:18:09: state name must be an identifier
semantics.ads:19:18: invalid state property
semantics.ads:20:25: duplicate state property
semantics.ads:21:08: properties Input and Output require Volatile
semantics.ads:22:08: properties Input and Output require Volatile
semantics.ads:23:08: property Volatile requires exactly one Input or Output
semantics.ads:24:08: property Volatile requires exactly one Input or Output
semantics.ads:25:31: integrity level must be an integer literal
semantics.ads:26:08: package "Error_1" has non-null abstract state
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-01-03 Hristian Kirtchev <kirtchev@adacore.com>
* aspects.adb, aspects.ads: Add Aspect_Abstract_State to all the
relevant tables.
* einfo.ads, einfo.adb: Add Integrity_Level and Refined_State to
the description of fields (Abstract_States): New routine.
(Integrity_Level): New routine.
(Has_Property): New routine.
(Is_Input_State): New routine.
(Is_Null_State): New routine.
(Is_Output_State): New routine.
(Is_Volatile_State): New routine.
(Refined_State): New routine.
(Set_Abstract_States): New routine.
(Set_Integrity_Level): New routine.
(Set_Refined_State): New routine.
(Write_Field8_Name): Add proper output for E_Abstract_State.
(Write_Field9_Name): Add proper output for E_Abstract_State.
(Write_Field25_Name): Add proper output for E_Package.
* lib-xref.ads: Add new letter for an abstract state.
* par-prag.adb: Add pragma Abstract_State to the list of pragma
that do not need special processing by the parser.
* sem_ch13.adb (Analyze_Aspect_Specifications): Convert
aspect Abstract_State into a pragma without any form
of legality checks. The work is done by Analyze_Pragma.
(Check_Aspect_At_Freeze_Point): Aspect Abstract_State does not
require delayed analysis.
* sem_prag.adb: Add a value for pragma Abstract_State in table
Sig_Flags.
(Analyze_Pragma): Add legality checks for pragma
Abstract_State. Analysis of individual states introduces a state
abstraction entity into the visibility chain.
* snames.ads-tmpl: Add new names for abstract state and
integrity. Add new pragma id for abstract state.
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 40108 bytes --]
Index: einfo.adb
===================================================================
--- einfo.adb (revision 194847)
+++ einfo.adb (working copy)
@@ -76,6 +76,7 @@
-- Associated_Node_For_Itype Node8
-- Dependent_Instances Elist8
-- Hiding_Loop_Variable Node8
+ -- Integrity_Level Uint8
-- Mechanism Uint8 (but returns Mechanism_Type)
-- Normalized_First_Bit Uint8
-- Postcondition_Proc Node8
@@ -84,6 +85,7 @@
-- Class_Wide_Type Node9
-- Current_Value Node9
+ -- Refined_State Node9
-- Renaming_Map Uint9
-- Direct_Primitive_Operations Elist10
@@ -535,6 +537,12 @@
-- Local subprograms --
-----------------------
+ function Has_Property
+ (State : Entity_Id;
+ Prop_Nam : Name_Id) return Boolean;
+ -- Determine whether abstract state State has a particular property denoted
+ -- by the name Prop_Nam.
+
function Rep_Clause (Id : E; Rep_Name : Name_Id) return N;
-- Returns the attribute definition clause for Id whose name is Rep_Name.
-- Returns Empty if no matching attribute definition clause found for Id.
@@ -549,6 +557,41 @@
return F'Val (UI_To_Int (Uint10 (Base_Type (Id))));
end Float_Rep;
+ ------------------
+ -- Has_Property --
+ ------------------
+
+ function Has_Property
+ (State : Entity_Id;
+ Prop_Nam : Name_Id) return Boolean
+ is
+ Par : constant Node_Id := Parent (State);
+ Prop : Node_Id;
+
+ begin
+ pragma Assert (Ekind (State) = E_Abstract_State);
+
+ -- States with properties appear as extension aggregates in the tree
+
+ if Nkind (Par) = N_Extension_Aggregate then
+ if Prop_Nam = Name_Integrity then
+ return Present (Component_Associations (Par));
+
+ else
+ Prop := First (Expressions (Par));
+ while Present (Prop) loop
+ if Chars (Prop) = Prop_Nam then
+ return True;
+ end if;
+
+ Next (Prop);
+ end loop;
+ end if;
+ end if;
+
+ return False;
+ end Has_Property;
+
----------------
-- Rep_Clause --
----------------
@@ -575,6 +618,12 @@
-- Attribute Access Functions --
--------------------------------
+ function Abstract_States (Id : E) return L is
+ begin
+ pragma Assert (Ekind (Id) = E_Package);
+ return Elist25 (Id);
+ end Abstract_States;
+
function Accept_Address (Id : E) return L is
begin
return Elist21 (Id);
@@ -1662,6 +1711,12 @@
return Node28 (Id);
end Initialization_Statements;
+ function Integrity_Level (Id : E) return U is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ return Uint8 (Id);
+ end Integrity_Level;
+
function Inner_Instances (Id : E) return L is
begin
return Elist23 (Id);
@@ -2534,6 +2589,12 @@
return Flag227 (Id);
end Referenced_As_Out_Parameter;
+ function Refined_State (Id : E) return E is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ return Node9 (Id);
+ end Refined_State;
+
function Register_Exception_Call (Id : E) return N is
begin
pragma Assert (Ekind (Id) = E_Exception);
@@ -3084,6 +3145,12 @@
-- it is possible to add assertions that specifically include the E_Void
-- possibility, but in some cases, we just omit the assertions.
+ procedure Set_Abstract_States (Id : E; V : L) is
+ begin
+ pragma Assert (Ekind (Id) = E_Package);
+ Set_Elist25 (Id, V);
+ end Set_Abstract_States;
+
procedure Set_Accept_Address (Id : E; V : L) is
begin
Set_Elist21 (Id, V);
@@ -4200,6 +4267,12 @@
Set_Node28 (Id, V);
end Set_Initialization_Statements;
+ procedure Set_Integrity_Level (Id : E; V : Uint) is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ Set_Uint8 (Id, V);
+ end Set_Integrity_Level;
+
procedure Set_Inner_Instances (Id : E; V : L) is
begin
Set_Elist23 (Id, V);
@@ -5110,6 +5183,12 @@
Set_Flag227 (Id, V);
end Set_Referenced_As_Out_Parameter;
+ procedure Set_Refined_State (Id : E; V : E) is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ Set_Node9 (Id, V);
+ end Set_Refined_State;
+
procedure Set_Register_Exception_Call (Id : E; V : N) is
begin
pragma Assert (Ekind (Id) = E_Exception);
@@ -6364,6 +6443,37 @@
and then Chars (Id) = Name_uFinalizer;
end Is_Finalizer;
+ --------------------
+ -- Is_Input_State --
+ --------------------
+
+ function Is_Input_State (Id : E) return B is
+ begin
+ return
+ Ekind (Id) = E_Abstract_State and then Has_Property (Id, Name_Input);
+ end Is_Input_State;
+
+ -------------------
+ -- Is_Null_State --
+ -------------------
+
+ function Is_Null_State (Id : E) return B is
+ begin
+ return
+ Ekind (Id) = E_Abstract_State
+ and then Nkind (Parent (Id)) = N_Null;
+ end Is_Null_State;
+
+ ---------------------
+ -- Is_Output_State --
+ ---------------------
+
+ function Is_Output_State (Id : E) return B is
+ begin
+ return
+ Ekind (Id) = E_Abstract_State and then Has_Property (Id, Name_Output);
+ end Is_Output_State;
+
-----------------------------------
-- Is_Package_Or_Generic_Package --
-----------------------------------
@@ -6376,33 +6486,6 @@
Ekind (Id) = E_Generic_Package;
end Is_Package_Or_Generic_Package;
- ------------------------
- -- Predicate_Function --
- ------------------------
-
- function Predicate_Function (Id : E) return E is
- S : Entity_Id;
-
- begin
- pragma Assert (Is_Type (Id));
-
- if No (Subprograms_For_Type (Id)) then
- return Empty;
-
- else
- S := Subprograms_For_Type (Id);
- while Present (S) loop
- if Has_Predicates (S) then
- return S;
- else
- S := Subprograms_For_Type (S);
- end if;
- end loop;
-
- return Empty;
- end if;
- end Predicate_Function;
-
---------------
-- Is_Prival --
---------------
@@ -6534,6 +6617,17 @@
and then Is_Task_Type (Corresponding_Concurrent_Type (Id));
end Is_Task_Record_Type;
+ -----------------------
+ -- Is_Volatile_State --
+ -----------------------
+
+ function Is_Volatile_State (Id : E) return B is
+ begin
+ return
+ Ekind (Id) = E_Abstract_State
+ and then Has_Property (Id, Name_Volatile);
+ end Is_Volatile_State;
+
------------------------
-- Is_Wrapper_Package --
------------------------
@@ -6917,6 +7011,33 @@
return Ekind (Id);
end Parameter_Mode;
+ ------------------------
+ -- Predicate_Function --
+ ------------------------
+
+ function Predicate_Function (Id : E) return E is
+ S : Entity_Id;
+
+ begin
+ pragma Assert (Is_Type (Id));
+
+ if No (Subprograms_For_Type (Id)) then
+ return Empty;
+
+ else
+ S := Subprograms_For_Type (Id);
+ while Present (S) loop
+ if Has_Predicates (S) then
+ return S;
+ else
+ S := Subprograms_For_Type (S);
+ end if;
+ end loop;
+
+ return Empty;
+ end if;
+ end Predicate_Function;
+
-------------------------
-- Present_In_Rep_Item --
-------------------------
@@ -7835,6 +7956,9 @@
when E_Variable =>
Write_Str ("Hiding_Loop_Variable");
+ when E_Abstract_State =>
+ Write_Str ("Integrity_Level");
+
when Formal_Kind |
E_Function |
E_Subprogram_Body =>
@@ -7868,6 +7992,9 @@
when Object_Kind =>
Write_Str ("Current_Value");
+ when E_Abstract_State =>
+ Write_Str ("Refined_State");
+
when E_Function |
E_Generic_Function |
E_Generic_Package |
@@ -8594,6 +8721,9 @@
procedure Write_Field25_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
+ when E_Package =>
+ Write_Str ("Abstract_States");
+
when E_Variable =>
Write_Str ("Debug_Renaming_Link");
Index: einfo.ads
===================================================================
--- einfo.ads (revision 194847)
+++ einfo.ads (working copy)
@@ -327,6 +327,10 @@
-- type, and if assertions are enabled, an attempt to set the attribute on a
-- subtype will raise an assert error.
+-- Abstract_States (Elist25)
+-- Defined for E_Package entities. Contains a list of all the abstract
+-- states declared by the related package.
+
-- Accept_Address (Elist21)
-- Defined in entries. If an accept has a statement sequence, then an
-- address variable is created, which is used to hold the address of the
@@ -1907,18 +1911,6 @@
-- that we still have a concrete type. For entities other than types,
-- returns the entity unchanged.
--- Interface_Alias (Node25)
--- Defined in subprograms that cover a primitive operation of an abstract
--- interface type. Can be set only if the Is_Hidden flag is also set,
--- since such entities are always hidden. Points to its associated
--- interface subprogram. It is used to register the subprogram in
--- secondary dispatch table of the interface (Ada 2005: AI-251).
-
--- Interfaces (Elist25)
--- Defined in record types and subtypes. List of abstract interfaces
--- implemented by a tagged type that are not already implemented by the
--- ancestors (Ada 2005: AI-251).
-
-- In_Package_Body (Flag48)
-- Defined in package entities. Set on the entity that denotes the
-- package (the defining occurrence of the package declaration) while
@@ -1943,6 +1935,18 @@
-- instantiated within the given generic. Used to diagnose circular
-- instantiations.
+-- Integrity_Level (Uint8)
+-- Defined for E_Abstract_State entities. Contains the numerical value of
+-- the integrity level state property. A value of Uint_0 designates a non
+-- existent integrity.
+
+-- Interface_Alias (Node25)
+-- Defined in subprograms that cover a primitive operation of an abstract
+-- interface type. Can be set only if the Is_Hidden flag is also set,
+-- since such entities are always hidden. Points to its associated
+-- interface subprogram. It is used to register the subprogram in
+-- secondary dispatch table of the interface (Ada 2005: AI-251).
+
-- Interface_Name (Node21)
-- Defined in constants, variables, exceptions, functions, procedures,
-- packages, components (JGNAT only), discriminants (JGNAT only), and
@@ -1967,6 +1971,11 @@
-- External_Name of the imported Java field (which is generally needed,
-- because Java names are case sensitive).
+-- Interfaces (Elist25)
+-- Defined in record types and subtypes. List of abstract interfaces
+-- implemented by a tagged type that are not already implemented by the
+-- ancestors (Ada 2005: AI-251).
+
-- Invariant_Procedure (synthesized)
-- Defined in types and subtypes. Set for private types if one or more
-- Invariant, or Invariant'Class, or inherited Invariant'Class aspects
@@ -2329,6 +2338,10 @@
-- inherited by their instances. It is also set on the body entities
-- of inlined subprograms. See also Has_Pragma_Inline.
+-- Is_Input_State (synthesized)
+-- Applies to all entities, true for abstract states that are subject to
+-- property Input.
+
-- Is_Instantiated (Flag126)
-- Defined in generic packages and generic subprograms. Set if the unit
-- is instantiated from somewhere in the extended main source unit. This
@@ -2523,6 +2536,10 @@
-- but there is no need to call such procedures within a compilation
-- unit, and this flag is used to suppress such calls.
+-- Is_Null_State (synthesized)
+-- Applies to all entities, true for an abstract state declared with
+-- keyword null.
+
-- Is_Numeric_Type (synthesized)
-- Applies to all entities, true for all numeric types and subtypes
-- (integer, fixed, float).
@@ -2550,6 +2567,10 @@
-- Applies to all entities, true for ordinary fixed point types and
-- subtypes.
+-- Is_Output_State (synthesized)
+-- Applies to all entities, true for abstract states that are subject to
+-- property Output.
+
-- Is_Package_Or_Generic_Package (synthesized)
-- Applies to all entities. True for packages and generic packages.
-- False for all other entities.
@@ -2895,6 +2916,10 @@
-- optimizations on volatile objects should test Treat_As_Volatile
-- rather than testing this flag.
+-- Is_Volatile_State (synthesized)
+-- Applies to all entities, true for abstract states that are subject to
+-- property Volatile.
+
-- Is_Wrapper_Package (synthesized)
-- Defined in package entities. Indicates that the package has been
-- created as a wrapper for a subprogram instantiation.
@@ -3441,6 +3466,10 @@
-- we have a separate warning for variables that are only assigned and
-- never read, and out parameters are a special case.
+-- Refined_State (Node9)
+-- Defined in E_Abstract_State entities. Contains the entity of the
+-- abstract state completion which is usually foung in package bodies.
+
-- Register_Exception_Call (Node20)
-- Defined in exception entities. When an exception is declared,
-- a call is expanded to Register_Exception. This field points to
@@ -4400,11 +4429,16 @@
-- A task body. This entity serves almost no function, since all
-- semantic analysis uses the protected entity (E_Task_Type).
- E_Subprogram_Body
+ E_Subprogram_Body,
-- A subprogram body. Used when a subprogram has a separate declaration
-- to represent the entity for the body. This entity serves almost no
-- function, since all semantic analysis uses the subprogram entity
-- for the declaration (E_Function or E_Procedure).
+
+ E_Abstract_State
+ -- A state abstraction. Used to designate entities introduced by aspect
+ -- or pragma Abstract_State. The entity carries the various properties
+ -- of the state.
);
for Entity_Kind'Size use 8;
@@ -4972,6 +5006,14 @@
-- Applicable attributes by entity kind --
------------------------------------------
+ -- E_Abstract_State
+ -- Integrity_Level (Uint8)
+ -- Refined_State (Node9)
+ -- Is_Input_State (synth)
+ -- Is_Null_State (synth)
+ -- Is_Output_State (synth)
+ -- Is_Volatile_State (synth)
+
-- E_Access_Protected_Subprogram_Type
-- Equivalent_Type (Node18)
-- Directly_Designated_Type (Node20)
@@ -5480,8 +5522,9 @@
-- Inner_Instances (Elist23) (generic case only)
-- Limited_View (Node23) (non-generic/instance)
-- Finalizer (Node24) (non-generic case only)
+ -- Abstract_States (Elist25)
+ -- Package_Instantiation (Node26)
-- Current_Use_Clause (Node27)
- -- Package_Instantiation (Node26)
-- Delay_Subprogram_Descriptors (Flag50)
-- Body_Needed_For_SAL (Flag40)
-- Discard_Names (Flag88)
@@ -6040,6 +6083,7 @@
-- section contains the functions used to obtain attribute values which
-- correspond to values in fields or flags in the entity itself.
+ function Abstract_States (Id : E) return L;
function Accept_Address (Id : E) return L;
function Access_Disp_Table (Id : E) return L;
function Actual_Subtype (Id : E) return E;
@@ -6226,6 +6270,7 @@
function In_Private_Part (Id : E) return B;
function In_Use (Id : E) return B;
function Initialization_Statements (Id : E) return N;
+ function Integrity_Level (Id : E) return U;
function Inner_Instances (Id : E) return L;
function Interface_Alias (Id : E) return E;
function Interface_Name (Id : E) return N;
@@ -6380,6 +6425,7 @@
function Referenced (Id : E) return B;
function Referenced_As_LHS (Id : E) return B;
function Referenced_As_Out_Parameter (Id : E) return B;
+ function Refined_State (Id : E) return E;
function Register_Exception_Call (Id : E) return N;
function Related_Array_Object (Id : E) return E;
function Related_Expression (Id : E) return N;
@@ -6524,6 +6570,9 @@
function Is_Discriminal (Id : E) return B;
function Is_Dynamic_Scope (Id : E) return B;
function Is_Finalizer (Id : E) return B;
+ function Is_Input_State (Id : E) return B;
+ function Is_Null_State (Id : E) return B;
+ function Is_Output_State (Id : E) return B;
function Is_Package_Or_Generic_Package (Id : E) return B;
function Is_Prival (Id : E) return B;
function Is_Protected_Component (Id : E) return B;
@@ -6534,6 +6583,7 @@
function Is_Synchronized_Interface (Id : E) return B;
function Is_Task_Interface (Id : E) return B;
function Is_Task_Record_Type (Id : E) return B;
+ function Is_Volatile_State (Id : E) return B;
function Is_Wrapper_Package (Id : E) return B;
function Last_Formal (Id : E) return E;
function Machine_Emax_Value (Id : E) return U;
@@ -6634,6 +6684,7 @@
-- Attribute Set Procedures --
------------------------------
+ procedure Set_Abstract_States (Id : E; V : L);
procedure Set_Accept_Address (Id : E; V : L);
procedure Set_Access_Disp_Table (Id : E; V : L);
procedure Set_Actual_Subtype (Id : E; V : E);
@@ -6819,6 +6870,7 @@
procedure Set_In_Private_Part (Id : E; V : B := True);
procedure Set_In_Use (Id : E; V : B := True);
procedure Set_Initialization_Statements (Id : E; V : N);
+ procedure Set_Integrity_Level (Id : E; V : U);
procedure Set_Inner_Instances (Id : E; V : L);
procedure Set_Interface_Alias (Id : E; V : E);
procedure Set_Interface_Name (Id : E; V : N);
@@ -6979,6 +7031,7 @@
procedure Set_Referenced (Id : E; V : B := True);
procedure Set_Referenced_As_LHS (Id : E; V : B := True);
procedure Set_Referenced_As_Out_Parameter (Id : E; V : B := True);
+ procedure Set_Refined_State (Id : E; V : E);
procedure Set_Register_Exception_Call (Id : E; V : N);
procedure Set_Related_Array_Object (Id : E; V : E);
procedure Set_Related_Expression (Id : E; V : N);
@@ -7317,6 +7370,7 @@
-- subprograms meeting the requirements documented in the section on
-- XEINFO may be referenced in this section.
+ pragma Inline (Abstract_States);
pragma Inline (Accept_Address);
pragma Inline (Access_Disp_Table);
pragma Inline (Actual_Subtype);
@@ -7499,6 +7553,7 @@
pragma Inline (In_Package_Body);
pragma Inline (In_Private_Part);
pragma Inline (In_Use);
+ pragma Inline (Integrity_Level);
pragma Inline (Inner_Instances);
pragma Inline (Interface_Alias);
pragma Inline (Interface_Name);
@@ -7702,6 +7757,7 @@
pragma Inline (Referenced);
pragma Inline (Referenced_As_LHS);
pragma Inline (Referenced_As_Out_Parameter);
+ pragma Inline (Refined_State);
pragma Inline (Register_Exception_Call);
pragma Inline (Related_Array_Object);
pragma Inline (Related_Expression);
@@ -7766,6 +7822,7 @@
pragma Inline (Init_Esize);
pragma Inline (Init_RM_Size);
+ pragma Inline (Set_Abstract_States);
pragma Inline (Set_Accept_Address);
pragma Inline (Set_Access_Disp_Table);
pragma Inline (Set_Actual_Subtype);
@@ -7947,6 +8004,7 @@
pragma Inline (Set_In_Private_Part);
pragma Inline (Set_In_Use);
pragma Inline (Set_Inner_Instances);
+ pragma Inline (Set_Integrity_Level);
pragma Inline (Set_Interface_Alias);
pragma Inline (Set_Interface_Name);
pragma Inline (Set_Interfaces);
@@ -8106,6 +8164,7 @@
pragma Inline (Set_Referenced);
pragma Inline (Set_Referenced_As_LHS);
pragma Inline (Set_Referenced_As_Out_Parameter);
+ pragma Inline (Set_Refined_State);
pragma Inline (Set_Register_Exception_Call);
pragma Inline (Set_Related_Array_Object);
pragma Inline (Set_Related_Expression);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 194841)
+++ sem_prag.adb (working copy)
@@ -6640,6 +6640,280 @@
Pragma_Misplaced;
end if;
+ --------------------
+ -- Abstract_State --
+ --------------------
+
+ when Pragma_Abstract_State => Abstract_State : declare
+ Pack_Id : Entity_Id;
+
+ -- Flags used to verify the consistency of states
+
+ Non_Null_Seen : Boolean := False;
+ Null_Seen : Boolean := False;
+
+ procedure Analyze_Abstract_State (State : Node_Id);
+ -- Verify the legality of a single state declaration. Create and
+ -- decorate a state abstraction entity and introduce it into the
+ -- visibility chain.
+
+ ----------------------------
+ -- Analyze_Abstract_State --
+ ----------------------------
+
+ procedure Analyze_Abstract_State (State : Node_Id) is
+ procedure Check_Duplicate_Property
+ (Prop : Node_Id;
+ Status : in out Boolean);
+ -- Flag Status denotes whether a particular property has been
+ -- seen while processing a state. This routine verifies that
+ -- Prop is not a duplicate property and sets the flag Status.
+
+ ------------------------------
+ -- Check_Duplicate_Property --
+ ------------------------------
+
+ procedure Check_Duplicate_Property
+ (Prop : Node_Id;
+ Status : in out Boolean)
+ is
+ begin
+ if Status then
+ Error_Msg_N ("duplicate state property", Prop);
+ end if;
+
+ Status := True;
+ end Check_Duplicate_Property;
+
+ -- Local variables
+
+ Errors : constant Nat := Serious_Errors_Detected;
+ Loc : constant Source_Ptr := Sloc (State);
+ Assoc : Node_Id;
+ Id : Entity_Id;
+ Is_Null : Boolean := False;
+ Level : Uint := Uint_0;
+ Name : Name_Id;
+ Prop : Node_Id;
+
+ -- Flags used to verify the consistency of properties
+
+ Input_Seen : Boolean := False;
+ Integrity_Seen : Boolean := False;
+ Output_Seen : Boolean := False;
+ Volatile_Seen : Boolean := False;
+
+ -- Start of processing for Analyze_Abstract_State
+
+ begin
+ -- A package with a null abstract state is not allowed to
+ -- declare additional states.
+
+ if Null_Seen then
+ Error_Msg_Name_1 := Chars (Pack_Id);
+ Error_Msg_N ("package % has null abstract state", State);
+
+ -- Null states appear as internally generated entities
+
+ elsif Nkind (State) = N_Null then
+ Name := New_Internal_Name ('S');
+ Is_Null := True;
+ Null_Seen := True;
+
+ -- Catch a case where a null state appears in a list of
+ -- non-null states.
+
+ if Non_Null_Seen then
+ Error_Msg_Name_1 := Chars (Pack_Id);
+ Error_Msg_N
+ ("package % has non-null abstract state", State);
+ end if;
+
+ -- Simple state declaration
+
+ elsif Nkind (State) = N_Identifier then
+ Name := Chars (State);
+ Non_Null_Seen := True;
+
+ -- State declaration with various properties. This construct
+ -- appears as an extension aggregate in the tree.
+
+ elsif Nkind (State) = N_Extension_Aggregate then
+ if Nkind (Ancestor_Part (State)) = N_Identifier then
+ Name := Chars (Ancestor_Part (State));
+ Non_Null_Seen := True;
+ else
+ Error_Msg_N
+ ("state name must be an identifier",
+ Ancestor_Part (State));
+ end if;
+
+ -- Process properties Input, Output and Volatile. Ensure
+ -- that none of them appear more than once.
+
+ Prop := First (Expressions (State));
+ while Present (Prop) loop
+ if Nkind (Prop) = N_Identifier then
+ if Chars (Prop) = Name_Input then
+ Check_Duplicate_Property (Prop, Input_Seen);
+ elsif Chars (Prop) = Name_Output then
+ Check_Duplicate_Property (Prop, Output_Seen);
+ elsif Chars (Prop) = Name_Volatile then
+ Check_Duplicate_Property (Prop, Volatile_Seen);
+ else
+ Error_Msg_N ("invalid state property", Prop);
+ end if;
+ else
+ Error_Msg_N ("invalid state property", Prop);
+ end if;
+
+ Next (Prop);
+ end loop;
+
+ -- Volatile requires exactly one Input or Output
+
+ if Volatile_Seen
+ and then
+ ((Input_Seen and then Output_Seen) -- both
+ or else
+ (not Input_Seen and then not Output_Seen)) -- none
+ then
+ Error_Msg_N
+ ("property Volatile requires exactly one Input or " &
+ "Output", State);
+ end if;
+
+ -- Either Input or Output require Volatile
+
+ if (Input_Seen or else Output_Seen)
+ and then not Volatile_Seen
+ then
+ Error_Msg_N
+ ("properties Input and Output require Volatile", State);
+ end if;
+
+ -- State property Integrity appears as a component
+ -- association.
+
+ Assoc := First (Component_Associations (State));
+ while Present (Assoc) loop
+ Prop := First (Choices (Assoc));
+ while Present (Prop) loop
+ if Nkind (Prop) = N_Identifier
+ and then Chars (Prop) = Name_Integrity
+ then
+ Check_Duplicate_Property (Prop, Integrity_Seen);
+ else
+ Error_Msg_N ("invalid state property", Prop);
+ end if;
+
+ Next (Prop);
+ end loop;
+
+ if Nkind (Expression (Assoc)) = N_Integer_Literal then
+ Level := Intval (Expression (Assoc));
+ else
+ Error_Msg_N
+ ("integrity level must be an integer literal",
+ Expression (Assoc));
+ end if;
+
+ Next (Assoc);
+ end loop;
+
+ -- Any other attempt to declare a state is erroneous
+
+ else
+ Error_Msg_N ("malformed abstract state declaration", N);
+ end if;
+
+ -- Do not generate a state abstraction entity if it was not
+ -- properly declared.
+
+ if Serious_Errors_Detected > Errors then
+ return;
+ end if;
+
+ -- The generated state abstraction reuses the same characters
+ -- from the original state declaration. Decorate the entity.
+
+ Id := Make_Defining_Identifier (Loc, New_External_Name (Name));
+ Set_Comes_From_Source (Id, not Is_Null);
+ Set_Parent (Id, State);
+ Set_Ekind (Id, E_Abstract_State);
+ Set_Etype (Id, Standard_Void_Type);
+ Set_Integrity_Level (Id, Level);
+ Set_Refined_State (Id, Empty);
+
+ -- Every non-null state must be nameable and resolvable the
+ -- same way a constant is.
+
+ if not Is_Null then
+ Push_Scope (Pack_Id);
+ Enter_Name (Id);
+ Pop_Scope;
+ end if;
+
+ -- Associate the state with its related package
+
+ if No (Abstract_States (Pack_Id)) then
+ Set_Abstract_States (Pack_Id, New_Elmt_List);
+ end if;
+
+ Append_Elmt (Id, Abstract_States (Pack_Id));
+ end Analyze_Abstract_State;
+
+ -- Local variables
+
+ Par : Node_Id;
+ State : Node_Id;
+
+ -- Start of processing for Abstract_State
+
+ begin
+ GNAT_Pragma;
+ S14_Pragma;
+ Check_Arg_Count (1);
+
+ -- Ensure the proper placement of the pragma. Abstract states must
+ -- be associated with a package declaration.
+
+ if From_Aspect_Specification (N) then
+ Par := Parent (Corresponding_Aspect (N));
+ else
+ Par := Parent (Parent (N));
+ end if;
+
+ if Nkind (Par) = N_Compilation_Unit then
+ Par := Unit (Par);
+ end if;
+
+ if Nkind (Par) /= N_Package_Declaration then
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Pack_Id := Defining_Unit_Name (Specification (Par));
+ State := Expression (Arg1);
+
+ -- Multiple abstract states appear as an aggregate
+
+ if Nkind (State) = N_Aggregate then
+ State := First (Expressions (State));
+ while Present (State) loop
+ Analyze_Abstract_State (State);
+
+ Next (State);
+ end loop;
+
+ -- Various forms of a single abstract state. Note that these may
+ -- include malformed state declarations.
+
+ else
+ Analyze_Abstract_State (State);
+ end if;
+ end Abstract_State;
+
------------
-- Ada_83 --
------------
@@ -15748,6 +16022,7 @@
Sig_Flags : constant array (Pragma_Id) of Int :=
(Pragma_AST_Entry => -1,
Pragma_Abort_Defer => -1,
+ Pragma_Abstract_State => -1,
Pragma_Ada_83 => -1,
Pragma_Ada_95 => -1,
Pragma_Ada_05 => -1,
Index: aspects.adb
===================================================================
--- aspects.adb (revision 194841)
+++ aspects.adb (working copy)
@@ -238,6 +238,7 @@
Canonical_Aspect : constant array (Aspect_Id) of Aspect_Id :=
(No_Aspect => No_Aspect,
+ Aspect_Abstract_State => Aspect_Abstract_State,
Aspect_Ada_2005 => Aspect_Ada_2005,
Aspect_Ada_2012 => Aspect_Ada_2005,
Aspect_Address => Aspect_Address,
Index: aspects.ads
===================================================================
--- aspects.ads (revision 194841)
+++ aspects.ads (working copy)
@@ -74,6 +74,7 @@
type Aspect_Id is
(No_Aspect, -- Dummy entry for no aspect
+ Aspect_Abstract_State, -- GNAT
Aspect_Address,
Aspect_Alignment,
Aspect_Attach_Handler,
@@ -221,7 +222,8 @@
-- The following array identifies all implementation defined aspects
Impl_Defined_Aspects : constant array (Aspect_Id) of Boolean :=
- (Aspect_Ada_2005 => True,
+ (Aspect_Abstract_State => True,
+ Aspect_Ada_2005 => True,
Aspect_Ada_2012 => True,
Aspect_Compiler_Unit => True,
Aspect_Contract_Case => True,
@@ -305,6 +307,7 @@
Aspect_Argument : constant array (Aspect_Id) of Aspect_Expression :=
(No_Aspect => Optional,
+ Aspect_Abstract_State => Expression,
Aspect_Address => Expression,
Aspect_Alignment => Expression,
Aspect_Attach_Handler => Expression,
@@ -370,6 +373,7 @@
Aspect_Names : constant array (Aspect_Id) of Name_Id := (
No_Aspect => No_Name,
+ Aspect_Abstract_State => Name_Abstract_State,
Aspect_Ada_2005 => Name_Ada_2005,
Aspect_Ada_2012 => Name_Ada_2012,
Aspect_Address => Name_Address,
Index: par-prag.adb
===================================================================
--- par-prag.adb (revision 194841)
+++ par-prag.adb (working copy)
@@ -1092,6 +1092,7 @@
-- entirely in Sem_Prag, and no further checking is done by Par.
when Pragma_Abort_Defer |
+ Pragma_Abstract_State |
Pragma_Assertion_Policy |
Pragma_Assume |
Pragma_Assume_No_Invalid_Values |
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 194849)
+++ sem_ch13.adb (working copy)
@@ -1434,13 +1434,23 @@
-- Case 2d : Aspects that correspond to a pragma with one
-- argument.
+ when Aspect_Abstract_State =>
+ Aitem :=
+ Make_Pragma (Loc,
+ Pragma_Identifier =>
+ Make_Identifier (Sloc (Id), Name_Abstract_State),
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))));
+
+ Delay_Required := False;
+
when Aspect_Relative_Deadline =>
Aitem :=
Make_Pragma (Loc,
- Pragma_Argument_Associations =>
- New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
Pragma_Identifier =>
Make_Identifier (Sloc (Id), Name_Relative_Deadline));
@@ -6961,9 +6971,10 @@
Aspect_Type_Invariant =>
T := Standard_Boolean;
- -- Here is the list of aspects that don't require delay analysis.
+ -- Here is the list of aspects that don't require delay analysis
- when Aspect_Contract_Case |
+ when Aspect_Abstract_State |
+ Aspect_Contract_Case |
Aspect_Contract_Cases |
Aspect_Dimension |
Aspect_Dimension_System |
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl (revision 194841)
+++ snames.ads-tmpl (working copy)
@@ -446,6 +446,7 @@
-- Remaining pragma names
Name_Abort_Defer : constant Name_Id := N + $; -- GNAT
+ Name_Abstract_State : constant Name_Id := N + $; -- GNAT
Name_All_Calls_Remote : constant Name_Id := N + $;
-- Note: AST_Entry is not in this list because its name matches the name of
@@ -696,6 +697,7 @@
Name_Ignore : constant Name_Id := N + $;
Name_Increases : constant Name_Id := N + $;
Name_Info : constant Name_Id := N + $;
+ Name_Integrity : constant Name_Id := N + $;
Name_Internal : constant Name_Id := N + $;
Name_Link_Name : constant Name_Id := N + $;
Name_Lowercase : constant Name_Id := N + $;
@@ -1731,6 +1733,7 @@
-- Remaining (non-configuration) pragmas
Pragma_Abort_Defer,
+ Pragma_Abstract_State,
Pragma_All_Calls_Remote,
Pragma_Assert,
Pragma_Assert_And_Cut,
Index: lib-xref.ads
===================================================================
--- lib-xref.ads (revision 194841)
+++ lib-xref.ads (working copy)
@@ -531,8 +531,13 @@
E_Protected_Object => ' ',
E_Protected_Body => ' ',
E_Task_Body => ' ',
- E_Subprogram_Body => ' ');
+ E_Subprogram_Body => ' ',
+ -- ??? The following letter is added for completion, proper design and
+ -- implementation of abstract state cross-referencing to follow.
+
+ E_Abstract_State => ' ');
+
-- The following table is for information purposes. It shows the use of
-- each character appearing as an entity type.
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2013-01-03 13:07 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2013-01-03 13:07 [Ada] Aspect Abstract_State 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).