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] Support for aspect Refined_State


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

The syntax of the aspect/pragma is as follows:

   pragma Refined_State (REFINEMENT_LIST);

   REFINEMENT_LIST ::=
     REFINEMENT_CLAUSE
     | (REFINEMENT_CLAUSE {, REFINEMENT_CLAUSE})

   REFINEMENT_CLAUSE ::= state_NAME => CONSTITUENT_LIST

   CONSTITUENT_LIST ::=
     null
     | CONSTITUENT
     | (CONSTITUENT {, CONSTITUENT})

   CONSTITUENT ::= object_NAME | state_NAME

The semantics of the aspect/pragma are as follows:

A Refined_State aspect may only appear in the aspect_specification of a
package_body. [The use of package_body rather than package body allows this
aspect to be specified for generic package bodies.]

If a package_specification has a non-null Abstract_State aspect its body shall
have a Refined_State aspect.

If a package_specification does not have an Abstract_State aspect, then the
corresponding package_body shall not have a Refined_State aspect.

A Refined_State Aspect of a package_body has visibility extended to the
declarative_part of the body.

Each constituent is either a variable or a state abstraction.

An object which is a constituent shall be an entire object.

Each abstract_state_name declared in the package specification shall be denoted
as the state_name of a refinement_clause in the Refined_State aspect of the
body of the package.

Every entity of the hidden state of a package shall be denoted as a constituent
of exactly one abstract_state_name in the Refined_State aspect of the package
and shall not be denoted more than once. [These constituents are either
variables declared in the private part or body of the package, or the
declarations from the visible part of nested packages declared immediately
therein.]

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

--  semantics.ads

package Semantics
  with Abstract_State =>
         ((Refinement_State_1 with External, Input_Only),
          (Refinement_State_2 with External, Output_Only),
          (Refinement_State_3 with Non_Volatile),
          (Refinement_State_4 with Non_Volatile))  --  not refined
is
   procedure Enforce_Body;

   Var_1 : Integer;

   package In_Visible_Part
     with Abstract_State =>
            (State_1 with External, Input_Only)
   is
      Var_2 : Integer;
   private
      Var_3 : Integer;
   end In_Visible_Part;

   package Has_AS_No_RS
     with Abstract_State =>
            (Has_AS_No_RS_State with Non_Volatile)
   is end Has_AS_No_RS;

   package Null_AS_No_RS
     with Abstract_State => null
   is end Null_AS_No_RS;

   package No_AS_Has_RS
     with Abstract_State =>
            (No_AS_Has_RS_State with Non_Volatile)
   is end No_AS_Has_RS;

private
   Var_4   : Integer;
   Extra_1 : Integer;  --  hidden state not used

   package In_Private_Part
     with Abstract_State =>
            (State_2 with External, Output_Only)
   is
      Var_5 : Integer;
   private
      Var_6 : Integer;
   end In_Private_Part;
end Semantics;

--  semantics.adb

package body Semantics
  with Refined_State =>
         (Refinement_State_1 =>
            (Var_1,                    --  not a hidden state
             In_Visible_Part.State_1,  --  not a hidden state
             In_Visible_Part.Var_2,    --  not a hidden state
             In_Visible_Part.Var_3),   --  not a hidden state

          Refinement_State_2 =>
            (Var_4,
             In_Private_Part.State_2,
             In_Private_Part.Var_5,
             In_Private_Part.Var_6,     --  not a hidden state
             In_Private_Part.State_2),  --  duplicate use of hidden state

          Refinement_State_3 =>
            (Var_7,
             In_Body.State_3,
             In_Body.Var_8,
             In_Body.Var_9,  --  not a hidden state
             Var_7),         --  duplicate use of hidden state

          Refinement_State_2 => null,  --  duplicate refinement

          In_Visible_Part.State_1 => null)  --  not a valid abstract state of
                                            --  package Semantics
is
   procedure Enforce_Body is begin null; end Enforce_Body;

   package body In_Visible_Part
     with Refined_State => (State_1 => Var_3)
   is end In_Visible_Part;

   package body Has_AS_No_RS is end Has_AS_No_RS;  --  requires refinement

   package body Null_AS_No_RS is end Null_AS_No_RS;

   package body No_AS_Has_RS
     with Refined_State => (No_AS_Has_RS_State => null)  --  useless
   is end No_AS_Has_RS;                                  --  refinement

   package body In_Private_Part
     with Refined_State => (State_2 => Var_6)
   is end In_Private_Part;

   Var_7 : Integer;

   package In_Body
     with Abstract_State =>
            (State_3 with Non_Volatile)
   is
      Var_8   : Integer;
      Extra_2 : Integer;  --  hidden state not used
   private
      Var_9 : Integer;
   end In_Body;

   package body In_Body
     with Refined_State => (State_3 => Var_9)
   is end In_Body;
end Semantics;

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

$ gcc -c -gnat12 -gnatd.V semantics.adb
semantics.adb:2:08: package "Semantics" has unused hidden states
semantics.adb:2:08:   variable "Extra_1" defined at semantics.ads:37
semantics.adb:2:08:   variable "Extra_2" defined at line 53
semantics.adb:4:14: cannot use "Var_1" in refinement, constituent is not a
  hidden state of package "Semantics"
semantics.adb:5:29: cannot use "State_1" in refinement, constituent is not a
  hidden state of package "Semantics"
semantics.adb:6:29: cannot use "Var_2" in refinement, constituent is not a
  hidden state of package "Semantics"
semantics.adb:7:29: "Var_3" is not a visible entity of "In_Visible_Part"
semantics.adb:13:29: "Var_6" is not a visible entity of "In_Private_Part"
semantics.adb:14:29: duplicate use of constituent "State_2"
semantics.adb:20:21: "Var_9" is not a visible entity of "In_Body"
semantics.adb:21:14: duplicate use of constituent "Var_7"
semantics.adb:23:11: duplicate refinement of state "Refinement_State_2"
semantics.adb:25:26: cannot refine state, "State_1" is not defined in package
  "Semantics"
semantics.adb:34:04: package "Has_AS_No_RS" requires state refinement
semantics.ads:6:11: abstract state "Refinement_State_4" must be refined

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

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

	* aspects.adb: Add an entry in table Canonical_Aspect for
	Refined_State.
	* aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument,
	Aspect_Names and Aspect_Delay for Refined_State.
	* einfo.adb: Add with and use clauses for Elists.
	Remove Refined_State from the list of node usage.
	Add Refined_State_Pragma to the list of node usage.
	(Has_Null_Abstract_State): New routine.
	(Refined_State): Removed.
	(Refined_State_Pragma): New routine.
	(Set_Refined_State): Removed.
	(Set_Refined_State_Pragma): New routine.
	(Write_Field8_Name): Add output for Refined_State_Pragma.
	(Write_Field9_Name): Remove the output for Refined_State.
	* einfo.ads: Add new synthesized attribute Has_Null_Abstract_State
	along with usage in nodes.  Remove attribute Refined_State along
	with usage in nodes.  Add new attribute Refined_State_Pragma along
	with usage in nodes.
	(Has_Null_Abstract_State): New routine.
	(Refined_State): Removed.
	(Refined_State_Pragma): New routine.
	(Set_Refined_State): Removed.
	(Set_Refined_State_Pragma): New routine.
	* elists.adb (Clone): New routine.
	* elists.ads (Clone): New routine.
	* par-prag.adb: Add Refined_State to the pragmas that do not
	require special processing by the parser.
	* sem_ch3.adb: Add with and use clause for Sem_Prag.
	(Analyze_Declarations): Add local variables Body_Id, Context and
	Spec_Id. Add processing for delayed aspect/pragma Refined_State.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Update the
	handling of aspect Abstract_State.  Add processing for aspect
	Refined_State. Remove the bizzare insertion policy for aspect
	Abstract_State.
	(Check_Aspect_At_Freeze_Point): Add an entry for Refined_State.
	* sem_prag.adb: Add an entry to table Sig_Flags
	for pragma Refined_State.
	(Add_Item): Update the
	comment on usage. The inserted items need not be unique.
	(Analyze_Contract_Cases_In_Decl_Part): Rename variable Restore to
	Restore_Scope and update all its occurrences.
	(Analyze_Pragma):
	Update the handling of pragma Abstract_State. Add processing for
	pragma Refined_State.
	(Analyze_Pre_Post_Condition_In_Decl_Part):
	Rename variable Restore to Restore_Scope and update all its
	occurrences.
	(Analyze_Refined_State_In_Decl_Part): New routine.
	* sem_prag.ads (Analyze_Refined_State_In_Decl_Part): New routine.
	* snames.ads-tmpl: Add new predefined name for Refined_State. Add
	new Pragma_Id for Refined_State.

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]