This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[Ada] Aspect Refined_Global


This patch provides the initial implementation of aspect/pragma Refined_Global.
This construct is intended for formal verification proofs.

The syntax of Refined_Global is as follows:

   pragma Refined_Global (GLOBAL_SPECIFICATION);

   GLOBAL_SPECIFICATION ::=
     null
     | GLOBAL_LIST
     | MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST}

     MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST

     MODE_SELECTOR ::= Input | Output | In_Out | Contract_In
     GLOBAL_LIST   ::= GLOBAL_ITEM | (GLOBAL_ITEM {, GLOBAL_ITEM})
     GLOBAL_ITEM   ::= NAME

The semantics of Refined_Global are as follows:

A Refined_Global 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, the declaration has a Global aspect which denotes a state
abstraction declared by the package and the refinement of the state abstraction
is visible.

A Refined_Global aspect specification shall refine the subprogram's Global
aspect as follows:

   For each global_item in the Global aspect which denotes a state abstraction
   whose non-null refinement is visible at the point of the Refined_Global
   aspect specification, the Refined_Global specification shall include one or
   more global_items which denote constituents of that state abstraction.

   For each global_item in the Global aspect which denotes a state abstraction
   whose null refinement is visible at the point of the Refined_Global aspect
   specification, shall be omitted, or if required by the syntax of a
   global_specification replaced by a null in the the Refined_Global aspect.

   For each global_item in the Global aspect which does not denote such a state
   abstraction, the Refined_Global specification shall include exactly one
   global_item which denotes the same entity as the global_item in the Global
   aspect.

   No other global_items shall be included in the Refined_Global aspect
   specification.

Global_items in the a Refined_Global aspect specification shall denote distinct
entities.

The mode of each global_item in a Refined_Global aspect shall match that of the
corresponding global_item in the Global aspect unless: the mode_selector
specified in the Global aspect is In_Out; the corresponding global_item of
Global aspect shall denote a state abstraction whose refinement is visible; and
the global_item in the Refined_Global aspect is a constituent of the state
abstraction.

For this special case when the mode_selector is In_Out, the Refined_Global
aspect may denote individual constituents of the state abstraction as Input,
Output, or In_Out (given that the constituent itself may have any of these
mode_selectors) so long as one or more of the following conditions are
satisfied:
 
   at least one of the constituents has a mode_selector of In_Out; or

   there is at least one of each of a constituent with a mode_selector of Input
   and of Output; or

   the Refined_Global aspect does not denote all of the constituents of the
   state abstraction and at least one of them has the mode_selector of Output.

If the Global aspect specification references a state abstraction with a
mode_selector of Output whose refinement is visible, then every constituent of
that state abstraction shall be referenced in the Refined_Global aspect
specification.

The legality rules for Global Aspects and External states described in Refined
External States 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
     with Global =>
            (Input  => (State_1, In_Var),
             In_Out => (State_2, In_Out_Var),
             Output => (State_3, Out_Var));

private
   Var_1 : Integer;
end Semantics;

--  semantics.adb

package body Semantics
  with Refined_State =>
         (State_1 => Var_1,
          State_2 => (Nested.State_4, Nested.Var_2),
          State_3 => Var_3)
is
   procedure OK
     with Refined_Global =>
            (Input  => (Var_1, In_Var),
             In_Out => (Nested.State_4, Nested.Var_2, In_Out_Var),
             Output => (Var_3, Out_Var)) is
   begin null; end OK;

   package Nested
     with Abstract_State => (State_4 with Part_Of => State_2)
   is
      Var_2 : Integer;
   end Nested;

   Var_3 : Integer;

   package body Nested
     with Refined_State => (State_4 => null)
   is end Nested;
end Semantics;

--  completions.ads

package Completions is
   package Input_State_Checks
     with Abstract_State => (Input_State with External, Input_Only)
   is
      procedure Input_Proc
        with Global => (Input => Input_State);
   private
      Var_1 : Integer;
   end Input_State_Checks;

   package In_Out_State_Checks
     with Abstract_State => In_Out_State
   is
      procedure In_Out_Proc_1
        with Global => (In_Out => In_Out_State);
      procedure In_Out_Proc_2
        with Global => (In_Out => In_Out_State);
      procedure In_Out_Proc_3
        with Global => (In_Out => In_Out_State);
      procedure In_Out_Proc_4
        with Global => (In_Out => In_Out_State);
      procedure In_Out_Proc_5
        with Global => (In_Out => In_Out_State);
   private
      Var_1 : Integer;
   end In_Out_State_Checks;

   package Output_State_Checks
     with Abstract_State => (Output_State with External, Output_Only)
   is
      procedure Output_Proc_1
        with Global => (Output => Output_State);
      procedure Output_Proc_2
        with Global => (Output => Output_State);
   private
      Var_1 : Integer;
   end Output_State_Checks;
end Completions;

--  completions.adb

package body Completions is
   package body Input_State_Checks
     with Refined_State => (Input_State => (Var_1, Var_2, Var_3))
   is
      Var_2 : Integer;
      Var_3 : Integer;

      procedure Input_Proc
        with Refined_Global => (Input  => (Var_1, Var_3),  --  OK
                                In_Out => Var_2)           --  illegal
      is begin null; end Input_Proc;
   end Input_State_Checks;

   package body In_Out_State_Checks
     with Refined_State => (In_Out_State => (Var_1, Var_2, Var_3))
   is
      Var_2 : Integer;
      Var_3 : Integer;

      procedure In_Out_Proc_1
        with Refined_Global => (In_Out => Var_1)  --  OK
      is begin null; end In_Out_Proc_1;

      procedure In_Out_Proc_2
        with Refined_Global => (Input  => Var_1,  --  OK
                                Output => Var_2)  --  OK
      is begin null; end In_Out_Proc_2;

      procedure In_Out_Proc_3
       with Refined_Global => (Output => Var_3)  --  OK
      is begin null; end In_Out_Proc_3;

      procedure In_Out_Proc_4
        with Refined_Global => (Input => (Var_1))  --  illegal
      is begin null; end In_Out_Proc_4;

      procedure In_Out_Proc_5
        with Refined_Global => (Output => (Var_1, Var_2, Var_3)) --  illegal
      is begin null; end In_Out_Proc_5;
   end In_Out_State_Checks;

   package body Output_State_Checks
     with Refined_State => (Output_State => (Var_1, Var_2, Var_3))
   is
      Var_2 : Integer;
      Var_3 : Integer;

      procedure Output_Proc_1
        with Refined_Global => (Output => (Var_1, Var_3))  --  illegal
      is begin null; end Output_Proc_1;

      procedure Output_Proc_2
        with Refined_Global => (Input  => Var_1,           --  illegal
                                Output => (Var_2, Var_3))  --  OK
      is begin null; end Output_Proc_2;
   end Output_State_Checks;
end Completions;

--  inconsistencies.ads

package Inconsistencies
  with Abstract_State => State
is
   Var_1 : Integer;
   Var_2 : Integer;
   Extra : Integer;

   procedure Mismatched_Items
     with Global => (Input  => Var_1,
                     In_Out => State,
                     Output => Var_2);
private
   Var_3 : Integer;
end Inconsistencies;

--  inconsistencies.adb

package body Inconsistencies
  with Refined_State => (State => (Var_3, Var_4))
is
   Var_4 : Integer;

   procedure Mismatched_Items
     with Refined_Global => (Input  => Var_2,
                             In_Out => (Var_4, Extra),
                             Output => Var_1)
   is begin null; end Mismatched_Items;
end Inconsistencies;

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

$ gcc -c -gnat12 -gnatd.V -gnatws semantics.adb
$ gcc -c -gnat12 -gnatd.V completions.adb
$ gcc -c -gnat12 -gnatd.V inconsistencies.adb
completions.adb:9:14: constituent "Var_2" of state "Input_State" must have mode
  Input in global refinement
completions.adb:34:14: global refinement of state "In_Out_State" redefines the
  mode of its constituents
completions.adb:38:14: global refinement of state "In_Out_State" redefines the
  mode of its constituents
completions.adb:49:14: constituent "Var_2" of state "Output_State" must have
  mode Output in global refinement
completions.adb:53:14: constituent "Var_1" of state "Output_State" must have
  mode Output in global refinement
inconsistencies.adb:7:40: global item "Var_2" has inconsistent modes
inconsistencies.adb:7:40:   expected mode "Input"
inconsistencies.adb:7:40:   found mode "Output"
inconsistencies.adb:8:48: extra global item "Extra"
inconsistencies.adb:9:40: global item "Var_1" has inconsistent modes
inconsistencies.adb:9:40:   expected mode "Output"
inconsistencies.adb:9:40:   found mode "Input"

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

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

	* einfo.adb: Add node/list usage for Refined_State
	and Refinement_Constituents.
	(Get_Pragma): Update the
	initialization of Is_CDG to include Refined_Global and
	Refined_Depends. Rename constant Delayed to In_Contract and update
	all of its occurrences.
	(Is_Non_Volatile_State): New routine.
	(Is_Volatile_State): Removed.
	(Refined_State): New routine.
	(Refinement_Constituents): New routine.
	(Set_Refined_State): New routine.
	(Set_Refinement_Constituents): New routine.
	(Write_Field8_Name): Add output for Refinement_Constituents.
	(Write_Field10_Name): Add output for Refined_State.
	* einfo.ads: Add new synthesized attribute Is_Non_Volatile_State.
	Remove synthesized attribute Is_Volatile_State.  Add new
	attributes Refined_State and Refinement_Constituents along with
	usage in nodes.
	(Get_Pragma): Update the comment on usage.
	(Is_Non_Volatile_State): New routine.
	(Is_Volatile_State): Removed.
	(Refined_State): New routine and pragma Inline.
	(Refinement_Constituents): New routine and pragma Inline.
	(Set_Refined_State): New routine and pragma Inline.
	(Set_Refinement_Constituents): New routine and pragma Inline.
	* elists.ads, elists.adb (Clone): Removed.
	(New_Copy_Elist): New routine.
	(Remove): New routine.
	* sem_ch3.adb (Analyze_Declarations): Use Defining_Entity
	to get the entity of the subprogram [body].
	(Analyze_Object_Declaration): Add initialization for
	Refined_State.
	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Add processing
	for Refined_Global and Refined_Depends. Emit an error when
	the body requires Refined_Global, but the aspect/pragma is
	not present.
	* sem_ch6.ads (Analyze_Subprogram_Body_Contract): Change
	procedure signature and add comment on usage.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Refined_Global.
	* sem_prag.adb (Analyze_Abstract_State): Add initialization
	of attributes Refined_State and Refinement_Constituents.
	(Analyze_Depends_In_Decl_Part, Analyze_Global_In_Decl_Part,
	Analyze_Contract_Cases_In_Decl_Part): Remove local
	constant Arg1.
	(Analyze_Pragma): Add processing for pragma
	Refined_Global. The analysis of Refined_Post and Refined_Pre
	has been merged. Update an error message in the processing of
	pragma Refined_State.
	(Analyze_Refined_Global_In_Decl_Part): Provide implementation.
	(Analyze_Refined_Pragma): New routine.
	(Analyze_Refined_Pre_Post_Condition): Removed.
	(Analyze_Refined_State_In_Decl_Part): Update the call to Clone.
	(Analyze_Refinement_Clause): Make State_Id visible to all
	nested subprogram.
	(Check_Matching_Constituent): Establish
	a relation between a refined state and its constituent.
	(Collect_Hidden_States_In_Decls): Remove ??? comment. Look at
	the entity of the object declaration to establish its kind.
	* sem_util.adb: Alphabetize with and use clauses.
	(Contains_Refined_State): New routine.
	* sem_util.ads (Contains_Refined_State): New routine.

Attachment: difs
Description: Text document


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]