[Ada] Aspect Refined_Depends

[Arnaud Charlet <charlet at adacore dot com>]

This patch provides the initial implementation of aspect Refined_Depends along
with its pragma equivalent. This construct is intended for formal verification
purposes.

The syntax of the aspect/pragma is as follows:

   pragma Refined_Depends (DEPENDENCY_RELATION);

   DEPENDENCY_RELATION ::=
     null
     | DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE}

   DEPENDENCY_CLAUSE ::=
     OUTPUT_LIST =>[+] INPUT_LIST
     | NULL_DEPENDENCY_CLAUSE

   NULL_DEPENDENCY_CLAUSE ::= null => INPUT_LIST

   OUTPUT_LIST ::= OUTPUT | (OUTPUT {, OUTPUT})

   INPUT_LIST ::= null | INPUT | (INPUT {, INPUT})

   OUTPUT ::= name | FUNCTION_RESULT
   INPUT  ::= name

   where FUNCTION_RESULT is a function Result attribute_reference

The semantics of the aspect/pragma are as follows:

The static semantics are equivalent to those given for the Depends aspect in
Depends Aspect.

A Refined_Depends aspect shall be specified on a body_stub (if one is present)
or subprogram body if and only if it has a declaration in the visible part of
an enclosing package and the declaration has a Depends aspect which denotes a
state abstraction declared by the package and the refinement of the state
abstraction is visible.

A Refined_Depends aspect specification is, in effect, a copy of the
corresponding Depends aspect specification except that any references in the
Depends aspect to a state abstraction, whose refinement is visible at the point
of the Refined_Depends specification, are replaced with references to zero or
more direct or indirect constituents of that state abstraction. A
Refined_Depends aspect is defined by creating a new dependency_relation from
the original given in the Depends aspect as follows:

  A partially refined dependency relation is created by first copying, from the
Depends aspect, each output that is not state abstraction whose refinement is
visible at the point of the Refined_Depends aspect, along with its input_list,
to the partially refined dependency relation as an output denoting the same
entity with an input_list denoting the same entities as the original.
[The order of the outputs and the order of inputs within the input_list is
insignificant.]

  The partially refined dependency relation is then extended by replacing each
output in the Depends aspect that is a state abstraction, whose refinement is
visible at the point of the Refined_Depends, by zero or more outputs in the
partially refined dependency relation. It shall be zero only for a null
refinement, otherwise all of the outputs shall denote a constituent of the
state abstraction.

  If the output in the Depends_Aspect denotes a state abstraction which is not
also an input, then all of the constituents [for a non-null refinement] of the
state abstraction shall be denoted as outputs of the partially refined
dependency relation.

  These rules may, for each output in the Depends aspect, introduce more than
one output in the partially refined dependency relation. Each of these outputs
has an input_list that has zero or more of the inputs from the input_list of
the original output. The union of these inputs shall denote the same inputs
that appear in the input_list of the original output.

  If the Depends aspect has a null_dependency_clause, then the partially
refined dependency relation has a null_dependency_clause added with an
input_list denoting the same inputs as the original.

  The partially refined dependency relation is completed by replacing the
inputs which are state abstractions, whose refinements are visible at the point
of the Refined_Depends aspect, by zero or more inputs. It shall be zero only
for a null refinement, otherwise each of the inputs shall denote a constituent
of the state abstraction. The completed dependency relation is the
dependency_relation of the Refined_Depends aspect.

These rules result in omitting each state abstraction whose null refinement is
visible at the point of the Refined_Depends. If and only if required by the
syntax, the state abstraction shall be replaced by a null symbol rather than
being omitted.

No other outputs or inputs shall be included in the Refined_Depends aspect
specification. Outputs in the Refined_Depends aspect specification shall denote
distinct entities. Inputs in an input_list shall denote distinct entities.

[The above rules may be viewed from the perspective of checking the consistency
of a Refined_Depends aspect with its corresponding Depends aspect. In this
view, each input in the Refined_Depends aspect that is a constituent of a state
abstraction, whose refinement is visible at the point of the Refined_Depends
aspect, is replaced by its representative state abstraction with duplicate
inputs removed.

Each output in the Refined_Depends aspect, which is a constituent of the same
state abstraction whose refinement is visible at the point of the
Refined_Depends aspect, is merged along with its input_list into a single
dependency_clause whose output denotes the state abstraction and input_list is
the union of all of the inputs from the original input_lists.]

The rules for Depends Aspect also apply.

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

--  semantics.ads

package Semantics
  with Abstract_State =>
         ((State_1 with External, Input_Only),
           State_2,
          (State_3 with External, Output_Only))
is
   In_Var     : Integer;
   In_Out_Var : Integer;
   Out_Var    : Integer;

   procedure OK_1
     (Formal_1 : in     Integer;
      Formal_2 : in out Integer;
      Formal_3 : out    Integer)
   --  Input  set : Formal_1, Formal_2, In_Var, In_Out_Var,  State_1, State_2
   --  Output set : Formal_2, Formal_3, In_Out_Var, Out_Var, State_2, State_3
   with Global =>
          (Input  => (State_1, In_Var),
           In_Out => (State_2, In_Out_Var),
           Output => (State_3, Out_Var)),
        Depends =>
          ((Formal_2, In_Out_Var, State_2) => (Formal_1, In_Var, State_1),
           (Formal_3, Out_Var, State_3) => (Formal_2, In_Out_Var, State_2));

   procedure OK_2
     (Formal_1 : in     Integer;
      Formal_2 : in out Integer;
      Formal_3 : out    Integer)
   --  Input  set : Formal_1, Formal_2, In_Var, In_Out_Var
   --  Output set : Formal_2, Formal_3, In_Out_Var, Out_Var
   with Global =>
          (Input  => In_Var,
           In_Out => In_Out_Var,
           Output => Out_Var),
        Depends =>
          ((Formal_2, Formal_3, In_Out_Var) => Formal_1,
            Out_Var => (Formal_2, In_Var, In_Out_Var));

private
   Var_2 : Integer;

   package In_Private_Part
     with Abstract_State => (State_7 with Part_Of => State_1)
   is
      Var_3 : Integer;
   private
      Var_4 : Integer;
   end In_Private_Part;
end Semantics;

--  semantics.adb

package body Semantics
  with Refined_State =>
         (State_1 => (Var_2, In_Private_Part.State_7),
          State_2 => (In_Private_Part.Var_3, In_Body.State_8),
          State_3 => (In_Body.Var_6, Var_8))
is
   procedure OK_1
     (Formal_1 : in     Integer;
      Formal_2 : in out Integer;
      Formal_3 : out    Integer)
   --  Input set:
   --    Formal_1
   --    Formal_2
   --    In_Var
   --    In_Out_Var
   --    Var_2 ---------------------+-- State_1
   --    In_Private_Part.State_7 --/
   --    In_Private_Part.Var_3 -----+-- State_2
   --    In_Body.State_8 ----------/

   --  Output set:
   --    Formal_2
   --    Formal_3
   --    In_Out_Var
   --    Out_Var
   --    In_Private_Part.Var_3 -----+-- State_2
   --    In_Body.State_8 ----------/
   --    In_Body.Var_6 -------------+-- State_3
   --    Var_8 --------------------/

   with Refined_Global =>
          (Input  => (Var_2, In_Private_Part.State_7, In_Var),
           In_Out => (In_Private_Part.Var_3, In_Body.State_8, In_Out_Var),
           Output => (In_Body.Var_6, Var_8, Out_Var)),
        Refined_Depends =>
          ((Formal_2,
            In_Out_Var,
            In_Private_Part.Var_3,
            In_Body.State_8) =>
              (Formal_1,
               In_Var,
               Var_2,
               In_Private_Part.State_7),

           (Formal_3,
            Out_Var,
            In_Body.Var_6,
            Var_8) =>
              (Formal_2,
               In_Out_Var,
               In_Private_Part.Var_3,
               In_Body.State_8)) is
   begin null; end OK_1;

   procedure OK_2
     (Formal_1 : in     Integer;
      Formal_2 : in out Integer;
      Formal_3 : out    Integer)
   is begin null; end OK_2;

   package In_Body
     with Abstract_State => (State_8 with Part_Of => State_2)
   is
      Var_6 : Integer;
   private
      Var_7 : Integer;
   end In_Body;

   package body In_Private_Part
     with Refined_State => (State_7 => Var_4)
   is end In_Private_Part;

   package body In_Body
     with Refined_State => (State_8 => Var_7)
   is end In_Body;

   Var_8 : Integer;
end Semantics;

-----------------
-- Compilation --
-----------------

$ gcc -c -gnat12 -gnatd.V semantics.adb

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

2013-10-14  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Add processing
	for pragma Refined_State.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Refined_Depends.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
	Use Find_Related_Subprogram_Or_Body to find the related
	context. Use the current scope when determining whether to
	ensure proper visibility.
	(Analyze_Depends_In_Decl_Part):
	Add local variable Spec_Id. Update the comment on usage of
	Subp_Id. Use Find_Related_Subprogram_Or_Body to find the
	related context. Extract the corresponding spec of the body
	(if any). Use the current scope when determining when to
	ensure proper visibility.
	(Analyze_Global_In_Decl_Part):
	Add local variable Spec_Id. Update the comment on usage of
	Subp_Id. Use Find_Related_Subprogram_Or_Body to find the
	related context. Extract the corresponding spec of the body
	(if any). Use the current scope when determining when to
	ensure proper visibility.
	(Analyze_Global_Item): Use the
	entity of the subprogram spec when performing formal parameter
	checks. Perform state-related checks.
	(Analyze_Input_Output):
	Use Is_Attribute_Result to detect 'Result. Query the
	entity of a subprogram spec when verifying the prefix of
	'Result. Perform state-related checks.	(Analyze_Pragma):
	Merge the analysis of Refined_Depends and Refined_Global.
	(Analyze_Refined_Depends_In_Decl_Part): Provide implemenation.
	(Analyze_Refined_Global_In_Decl_Part): Move state-related checks
	to the body of Analyze_Global_In_Decl_Part. Rename local constant
	List to Items.	(Analyze_Refined_Pragma): Remove circuitry to
	find the proper context, use Find_Related_Subprogram_Or_Body
	instead.
	(Check_Function_Return): Query the entity of
	the subprogram spec when verifying the use of 'Result.
	(Check_In_Out_States, Check_Input_States, Check_Output_States):
	Avoid using Has_Null_Refinement to detect a state with
	a non-null refinement, use the Refinement_Constituents
	list instead.
	(Check_Matching_Constituent): Remove initialization code.
	(Check_Mode_Restriction_In_Function): Use the entity of the subprogram
	spec when verifying mode usage in functions.
	(Collect_Global_Items): New routine.
	(Collect_Subprogram_Inputs_Outputs): Add local
	variable Spec_Id. Add circuitry for bodies-as-specs. Use
	pragma Refined_Global when collecting for a body.
	(Create_Or_Modify_Clause): Use the location of the
	clause. Rename local variable Clause to New_Clause to avoid
	confusion and update all occurrences.  Use Is_Attribute_Result
	to detect 'Result.
	(Find_Related_Subprogram): Removed.
	(Find_Related_Subprogram_Or_Body): New routine.
	(Is_Part_Of): Move routine to top level.
	(Normalize_Clause): Update the
	comment on usage. The routine can now normalize a clause with
	multiple outputs by splitting it.
	(Collect_Global_Items):
	Rename local constant List to Items. Remove the check for
	a null list.
	(Requires_Profile_Installation): Removed.
	(Split_Multiple_Outputs): New routine.
	* sem_prag.ads: Update the comments on usage of various
	pragma-related analysis routines.
	* sem_util.adb (Contains_Refined_State): The routine can now
	process pragma [Refined_]Depends.
	(Has_Refined_State): Removed.
	(Has_State_In_Dependency): New routine.
	(Has_State_In_Global): New routine.
	(Is_Attribute_Result): New routine.
	* sem_util.ads (Is_Attribute_Result): New routine.

Attachment: difs
Description: Text document