[Ada] Indicator Part_Of

This patch implements indicator Part_Of (aspect, pragma and option forms). This
feature is intended for formal verification purposes.

The syntax of the aspect form is as follows:

   with Part_Of => ABSTRACT_STATE

   ABSTRACT_STATE ::= name

The semantics of this feature are as follows:

1. A Part_Of indicator is a Part_Of option of a state abstraction declaration
in an Abstract_State aspect, a Part_Of aspect specification applied to a
variable declaration or a Part_Of specification aspect applied to a generic
package instantiation. The Part_Of indicator shall denote the encapsulating
state abstraction of which the declaration is a constituent.

2. A variable declared immediately within the private part of a given package
or a variable or state abstraction that is part of the visible state of a
package that is declared immediately within the private part of the given
package shall have its Part_Of indicator specified; the Part_Of indicator shall
denote a state abstraction declared by the given package.

3. A variable or state abstraction which is part of the visible state of a
private child unit (or a public descendant thereof) shall have its Part_Of
indicator specified; the Part_Of indicator shall denote a state abstraction
declared by either the parent unit of the private unit or by a public
descendant of that parent unit.

4. Part_Of aspect specification for a package instantiation applies to each
part of the visible state of the instantiation. More specifically, explicitly
specifying the Part_Of aspect of a package instantiation implicitly specifies
the Part_Of aspect of each part of the visible state of that instantiation. The
legality rules for such an implicit specification are the same as for an
explicit specification.

5. No other declarations shall have a Part_Of indicator.

6. The refinement of a state abstraction denoted in a Part_Of indicator shall
denote as constituents all of the declarations that have a Part_Of indicator
denoting the state abstraction.

7. A state abstraction and a constituent (direct or indirect) thereof shall not
both be denoted in one Global, Depends, Initializes, Refined_Global or
Refined_Depends aspect specification. The denotation must be consistent between
the Global and Depends or between Refined_Global and Refined_Depends aspects of
a single subprogram.

------------
-- Source --
------------

--  simple_gen.ads

generic
package Simple_Gen is
   Var_1 : Integer := 1;

   package Visible_Nested is
      Var_2 : Integer := 2;
   end Visible_Nested;
end Simple_Gen;

--  illegal_constituents.ads

with Simple_Gen;

package Illegal_Constituents
  with Abstract_State => (State, Aux_State)
is
private
   Var_1 : Integer := 1 with Part_Of => State;

   package Private_Nested
     with Abstract_State =>
       (Private_Nested_State with Part_Of => State)
   is
      Var_2 : Integer := 2 with Part_Of => State;
   end Private_Nested;

   package Private_Inst is new Simple_Gen with Part_Of => Aux_State;
end Illegal_Constituents;

--  illegal_constituents.adb

with Illegal_Constituents.Private_Child;

package body Illegal_Constituents
  with Refined_State =>
    (State =>
       (Var_1,
        Private_Nested.Var_2,
        Private_Inst.Var_1,
        Private_Inst.Visible_Nested.Var_2,

        Body_Nested.Body_Nested_State,
        Body_Nested.Var_4,
        Body_Inst.Var_1,

        Illegal_Constituents.Private_Child.Private_Child_State,
        Illegal_Constituents.Private_Child.Var_5,
        Illegal_Constituents.Private_Child.Visible_Nested.Visible_Nested_State,
        Illegal_Constituents.Private_Child.Visible_Inst.Visible_Nested.Var_2),

     Aux_State =>
        null)
is
   Var_3 : Integer := 3;

   package body Private_Nested
     with Refined_State => (Private_Nested_State => null)
   is end Private_Nested;

   package Body_Nested
     with Abstract_State => Body_Nested_State
   is
      Var_4 : Integer := 4;
   end Body_Nested;

   package body Body_Nested
     with Refined_State => (Body_Nested_State => null)
   is end Body_Nested;

   package Body_Inst is new Simple_Gen;
end Illegal_Constituents;

--  illegal_constituents-private_child.ads

private package Illegal_Constituents.Private_Child
  with Abstract_State =>
    (Private_Child_State with Part_Of => State)
is
   Var_5 : Integer := 5 with Part_Of => Aux_State;

   package Visible_Nested
     with Abstract_State =>
       (Visible_Nested_State with Part_Of => State)
   is
      Var_6 : Integer := 6 with Part_Of => State;
   end Visible_Nested;

   package Visible_Inst is new Simple_Gen with Part_Of => State;
end Illegal_Constituents.Private_Child;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c illegal_constituents.adb
llegal_constituents.adb:3:14: body of package "Illegal_Constituents" has unused
  hidden states
illegal_constituents.adb:3:14:   variable "Var_3" defined at line 23
illegal_constituents.adb:3:14:   variable "Var_2" defined at simple_gen.ads:6,
  instance at line 39
illegal_constituents.adb:5:06: state "State" has unused Part_Of constituents
illegal_constituents.adb:5:06:   abstract state "Private_Nested_State" defined
  at illegal_constituents.ads:10
illegal_constituents.adb:5:06:   variable "Var_6" defined at
  illegal_constituents-private_child.ads:11
illegal_constituents.adb:5:06:   variable "Var_1" defined at simple_gen.ads:3,
  instance at illegal_constituents-private_child.ads:14
illegal_constituents.adb:8:21: "Var_1" cannot act as constituent of state
  "State"
illegal_constituents.adb:8:21: Part_Of indicator specifies "Aux_State" as
  encapsulating state
illegal_constituents.adb:9:36: "Var_2" cannot act as constituent of state
  "State"
illegal_constituents.adb:9:36: Part_Of indicator specifies "Aux_State" as
  encapsulating state
illegal_constituents.adb:16:43: "Var_5" cannot act as constituent of state
  "State"
illegal_constituents.adb:16:43: Part_Of indicator specifies "Aux_State" as
  encapsulating state
illegal_constituents.adb:20:06: state "Aux_State" has unused Part_Of
  constituents
illegal_constituents.adb:20:06:   variable "Var_1" defined at simple_gen.ads:3,
  instance at illegal_constituents.ads:16
illegal_constituents.adb:20:06:   variable "Var_2" defined at simple_gen.ads:6,
  instance at illegal_constituents.ads:16
illegal_constituents.adb:20:06:   variable "Var_5" defined at
  illegal_constituents-private_child.ads:5

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-01-29  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb Add an entry for aspect Part_Of in table
	Canonical_Aspect.
	* aspects.ads Add an entry for aspect Part_Of in tables Aspect_Id,
	Aspect_Argument, Aspect_Names and Aspect_Delay.
	* atree.h Define Elist9.
	* atree.adb (Elist9): New routine.
	(Set_Elist9): New routine.
	* atree.ads (Elist9): New routine.
	(Set_Elist9): New routine.
	* einfo.adb Add Part_Of_Constituents and Encapsulating_State to
	the list of node usage.  Remove Refined_State from the list of
	node usage.
	(Encapsulating_State): New routine.
	(Get_Pragma):
	Handle pragma Part_Of; (Part_Of_Constituents): New routine.
	(Refined_State): Removed.
	(Set_Encapsulating_State): New routine.
	(Set_Part_Of_Constituents): New routine.
	(Set_Refined_State): Removed.
	(Write_Field9_Name): Add an entry
	for Part_Of_Constituents (Write_Field10_Name): Add an entry for
	Encapsulating_State. Remove the entry for Refined_State.
	* einfo.ads Add new attributes Encapsulating_State
	and Part_Of_Constituents alond with their usage in
	entities. Remove attribute Refined_State along with its
	usage in entities.
	(Encapsulating_State): New routine and
	pragma Inline.	(Get_Pragma): Update the comment on usage.
	(Part_Of_Constituents): New routine and pragma Inline.
	(Refined_State): Removed along with pragma Inline.
	(Set_Encapsulating_State): New routine and pragma Inline.
	(Set_Part_Of_Constituents): New routine and pragma Inline.
	(Set_Refined_State): Removed along with pragma Inline.
	* par-prag.adb Pragma Part_Of does not need any special processing
	by the parser.
	* sem_ch3.adb (Analyze_Declarations): Remove local variables
	Body_Id and Prag. Call separate routines to analyze the
	contract of a package [body].
	(Analyze_Object_Contract):
	Update the comment on usage. Remove local variables
	Items and Nam. Use Get_Pragma rather than traversing the
	classification list.  Verify whether the lack of indicator
	Part_Of agrees with the placement of the variable in state space.
	(Analyze_Object_Declaration): Initialize the encapsulating state
	of a variable.	(Requires_State_Refinement): Moved to sem_util.
	* sem_ch7.adb (Analyze_Package_Body_Contract): New routine.
	(Analyze_Package_Contract): New routine.
	* sem_ch7.ads (Analyze_Package_Body_Contract): New routine.
	(Analyze_Package_Contract): New routine.
	* sem_ch10.adb (Decorate_State): Initialize the encapsulating
	state and Part_Of constituents.
	* sem_ch13.adb (Analyze_Aspect_Specifications):
	Add processing for aspect Part_Of. Update all
	calls to Decorate_Delayed_Aspect_And_Pragma.
	(Check_Aspect_At_Freeze_Point): Aspect Part_Of does
	not need any special processing at freeze time.
	(Decorate_Delayed_Aspect_And_Pragma): Renamed to
	Decorate_Aspect_And_Pragma.  Add formal parameter Delayed and
	update the associated comment.
	* sem_prag.adb Add an entry for pragma Part_Of in table Sig_Flags.
	(Analyze_Abstract_State): Add new global variable State_Id. Remove
	local constants Errors and Loc. Remove local variables Is_Null
	and State_Nam. Create the entity of the abstract state on the
	spot, before all remaining checks are performed. Verify that a
	missing Part_Of option agrees with the placement of the abstract
	state within the state space.
	(Analyze_Depends_In_Decl_Part):
	Add new global variables Constits_Seen and States_Seen. Check
	that a state and a corresponding constituent do not appear
	in pragma [Refined_]Depends.
	(Analyze_Global_In_Decl_Part):
	Add new global variables Constits_Seen and States_Seen. Check
	that a state and a corresponding constituent do not appear
	in pragma [Refined_]Global.
	(Analyze_Global_Item):
	Remove the now obsolete code that deals with Part_Of.
	Add the entity of the global item to the list of processed
	items.	(Analyze_Initializes_In_Decl_Part): Add new global
	variables Constits_Seen and States_Seen. Check that a state
	and a corresponding constituent do not appear in pragma
	Initializes.
	(Analyze_Initialization_Item): Add the entity
	of the initialization item to the list of processed items.
	(Analyze_Input_Item): Add the entity of the initialization
	item to the list of processed items.
	(Analyze_Input_Output):
	Remove the now obsolete code that deals with Part_Of.  Add the
	entity of the input/output to the list of processed items.
	(Analyze_Part_Of): New routine.
	(Analyze_Part_Of_Option): Remove
	local constant Par_State. Add local constant Encaps and local
	variables Encaps_Id and Legal. Use Analyze_Part of to analyze
	the option. Turn the related state into a Part_Of constituent
	if the option is legal.
	(Analyze_Pragma): Add processing
	for pragma Part_Of.
	(Analyze_Refined_State_In_Decl_Part):
	Remove global constants Pack_Body and Spec_Id. Remove
	global variables Abstr_States and Hidden_States. Add new
	global variables Available_States, Body_Id, Body_States and
	Spec_Id. Add new local constant Body_Decl. Reimplement the
	logic that extracts the states available for refinement from
	the related package and the body hidden states of the said
	package.
	(Analyze_Refinement_Clause): Add local variable Part_Of_Constits.
	(Check_Applicable_Policy): Alphabetize body.
	(Check_Dependency_Clause): Replace Refined_State
	with Encapsulating_State.
	(Check_Matching_Constituent):
	Reimplement the logic that determines whether an item is a valid
	/ invalid constituent of the current refined state. Return when
	a construct does not denote a valid abstract state. Extract the
	list of Part_Of constituents for further analysis. Check that all
	Part_Of constituents of a state have been used in its refinement.
	(Check_Matching_State): Update the comment on usage. Operate
	on the list of available states.
	(Check_Missing_Part_Of): New routine.
	(Check_Refined_Global_Item): Replace Refined_State
	with Encapsulating_State.
	(Check_State_And_Constituent_Use): New routine.
	(Create_Abstract_State): New routine.
	(Is_Matching_Input): Replace Refined_State with Encapsulating_State.
	(Is_Part_Of): Removed.
	(Collect_Body_States): New routine.
	(Collect_Constituent): Replace Refined_State with Encapsulating_State.
	(Collect_Hidden_States): Removed.
	(Report_Unrefined_States): Change the profile of the procedure along
	with the comment on usage.
	(Report_Unused_Constituents): New routine.
	(Report_Unused_Hidden_States): Removed.
	(Report_Unused_States): New routine.
	* sem_prag.ads (Check_Missing_Part_Of): New routine.
	* sem_util.adb (Add_Contract_Item): Pragma Part_Of can now
	appear in the classification pragmas of a package instantiation
	or a variable.
	(Find_Placement_In_State_Space): New routine.
	(Is_Child): Removed.
	(Is_Child_Or_Sibling): Remove formal
	parameter Private_Child. Remove the private child checks.
	(Requires_State_Refinement): Moved from sem_ch3.
	* sem_util.ads Add new type State_Space_Kind along with
	comment on its usage and values.
	(Add_Contract_Item): Update the comment on usage.
	(Find_Body_Discriminal): Alphabetize spec.
	(Find_Placement_In_State_Space): New routine.
	(Is_Child_Or_Sibling): Remove formal parameter Private_Child
	and update the comment on usage.
	(Requires_State_Refinement): Moved from sem_ch3.
	* sinfo.ads: Update the documentation of N_Contract.
	* snames.ads-tmpl The predefined name for Part_Of is now used
	to denote a pragma. Add Pragma_Id for Part_Of.

[Ada] Indicator Part_Of

Commit Message

Patch