[Ada] Refined external states

Arnaud Charlet charlet@adacore.com
Mon Jan 27 16:50:00 GMT 2014


This patch implements the following rules concerning the refinement of external
abstract states:

* A state abstraction that is not specified as External shall not have
constituents which are External states.

* An External state abstraction shall have at least one constituent that is
External state, or shall have a null refinement.

* An External state abstraction shall have each of the properties set to True
which are True for any of its constituents.

* Refined_Global aspects must respect the rules related to external properties
of constituents which are external states given in External State and External
State - Variables.

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

--  semantics.ads

package Semantics
  with Abstract_State =>
    (State,
    (AR_AW_ER_EW_State_1 with External),
    (AR_AW_ER_EW_State_2 with External),
    (AR_AW_ER_EW_State_3 with External),
    (AR_EW_State         with External => (Async_Readers, Effective_Writes)),
    (AW_ER_State         with External => (Async_Writers, Effective_Reads)))
is
   procedure Proc
     with Global => (Input => AW_ER_State);
end Semantics;

--  semantics.adb

package body Semantics
  with Refined_State =>
    (State =>
       (Var_1, AR_1),       --  error
     AR_AW_ER_EW_State_1 =>
        null,               --  ok
     AR_AW_ER_EW_State_2 =>
       (Var_2_1, Var_2_2),  --  error
     AR_AW_ER_EW_State_3 =>
       (AR_EW_3, AW_3),     --  error
     AR_EW_State =>
       (AW_ER_4, AR_EW_4),  --  error
     AW_ER_State =>
        AW_ER_5)            --  ok
is
   Var_1   : Integer := 1;
   Var_2_1 : Integer := 2;
   Var_2_2 : Integer := 3;
   AR_1    : Integer := 4 with Volatile, Async_Readers;
   AR_EW_3 : Integer := 5 with Volatile, Async_Readers, Effective_Writes;
   AW_3    : Integer := 6 with Volatile, Async_Writers;
   AR_EW_4 : Integer := 7 with Volatile, Async_Readers, Effective_Writes;
   AW_ER_4 : Integer := 8 with Volatile, Async_Writers, Effective_Reads;
   AW_ER_5 : Integer := 9 with Volatile, Async_Writers, Effective_Reads;

   procedure Proc
     with Refined_Global => (Input => AW_ER_5)  --  error
   is begin null; end Proc;
end Semantics;

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

$ gcc -c semantics.adb
semantics.adb:3:06: non-external state "State" cannot contain external
  constituents in refinement (SPARK RM 7.2.8(1))
semantics.adb:7:06: external state "Ar_Aw_Er_Ew_State_2" requires at least one
  external constituent or null refinement (SPARK RM 7.2.8(2))
semantics.adb:9:06: external state "Ar_Aw_Er_Ew_State_3" requires at least one
  constituent with property "Effective_Reads" (SPARK RM 7.2.8(3))
semantics.adb:11:06: external state "Ar_Ew_State" lacks property
  "Async_Writers" set by constituent "Aw_Er_4" (SPARK RM 7.2.8(3))
semantics.adb:27:39: volatile global item "AW_ER_5" with property
  Effective_Reads must have mode In_Out or Output (SPARK RM 7.1.3(11))

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

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

	* einfo.adb (Has_Option): Reimplemented.
	* sem_prag.adb (Analyze_Refinement_Clause): Add global
	variables AR_Constit, AW_Constit, ER_Constit, EW_Constit,
	External_Constit_Seen and State. Add local variables Body_Ref,
	Body_Ref_Elmt and Extra_State. Reimplement part of the logic to
	avoid a cumbersome while pool. Verify the legality of an external
	state and relevant properties.
	(Check_External_Property): New routine.
	(Check_Matching_State): Remove parameter profile
	and update comment on usage.
	(Collect_Constituent): Store the
	relevant external property of a constituent.
	* sem_util.adb (Async_Readers_Enabled): Update the call to
	Has_Enabled_Property.
	(Async_Writers_Enabled): Update the call to Has_Enabled_Property.
	(Effective_Reads_Enabled): Update the call to Has_Enabled_Property.
	(Effective_Writes_Enabled): Update the call to Has_Enabled_Property.
	(Has_Enabled_Property): Rename formal parameter Extern to State_Id.
	Update comment on usage. Reimplement the logic to recognize the various
	formats of properties.

-------------- next part --------------
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 207138)
+++ einfo.adb	(working copy)
@@ -589,10 +589,10 @@
    -----------------------
 
    function Has_Option
-     (State   : Entity_Id;
-      Opt_Nam : Name_Id) return Boolean;
-   --  Determine whether abstract state State has a particular option denoted
-   --  by the name Opt_Nam.
+     (State_Id   : Entity_Id;
+      Option_Nam : Name_Id) return Boolean;
+   --  Determine whether abstract state State_Id has particular option denoted
+   --  by the name Option_Nam.
 
    ---------------
    -- Float_Rep --
@@ -609,33 +609,56 @@
    ----------------
 
    function Has_Option
-     (State   : Entity_Id;
-      Opt_Nam : Name_Id) return Boolean
+     (State_Id   : Entity_Id;
+      Option_Nam : Name_Id) return Boolean
    is
-      Par : constant Node_Id := Parent (State);
-      Opt : Node_Id;
+      Decl    : constant Node_Id := Parent (State_Id);
+      Opt     : Node_Id;
+      Opt_Nam : Node_Id;
 
    begin
-      pragma Assert (Ekind (State) = E_Abstract_State);
+      pragma Assert (Ekind (State_Id) = E_Abstract_State);
 
-      --  States with options appear as extension aggregates in the tree
+      --  The declaration of abstract states with options appear as an
+      --  extension aggregate. If this is not the case, the option is not
+      --  available.
 
-      if Nkind (Par) = N_Extension_Aggregate then
-         if Opt_Nam = Name_Part_Of then
-            return Present (Component_Associations (Par));
+      if Nkind (Decl) /= N_Extension_Aggregate then
+         return False;
+      end if;
 
-         else
-            Opt := First (Expressions (Par));
-            while Present (Opt) loop
-               if Chars (Opt) = Opt_Nam then
-                  return True;
-               end if;
+      --  Simple options
 
-               Next (Opt);
-            end loop;
+      Opt := First (Expressions (Decl));
+      while Present (Opt) loop
+
+         --  Currently the only simple option allowed is External
+
+         if Nkind (Opt) = N_Identifier
+           and then Chars (Opt) = Name_External
+           and then Chars (Opt) = Option_Nam
+         then
+            return True;
          end if;
-      end if;
 
+         Next (Opt);
+      end loop;
+
+      --  Complex options with various specifiers
+
+      Opt := First (Component_Associations (Decl));
+      while Present (Opt) loop
+         Opt_Nam := First (Choices (Opt));
+
+         if Nkind (Opt_Nam) = N_Identifier
+           and then Chars (Opt_Nam) = Option_Nam
+         then
+            return True;
+         end if;
+
+         Next (Opt);
+      end loop;
+
       return False;
    end Has_Option;
 
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 207140)
+++ sem_prag.adb	(working copy)
@@ -22214,25 +22214,45 @@
       -------------------------------
 
       procedure Analyze_Refinement_Clause (Clause : Node_Id) is
-         State_Id : Entity_Id := Empty;
-         --  The entity of the state being refined in the current clause
+         AR_Constit : Entity_Id := Empty;
+         AW_Constit : Entity_Id := Empty;
+         ER_Constit : Entity_Id := Empty;
+         EW_Constit : Entity_Id := Empty;
+         --  The entities of external constituents that contain one of the
+         --  following enabled properties: Async_Readers, Async_Writers,
+         --  Effective_Reads and Effective_Writes.
 
+         External_Constit_Seen : Boolean := False;
+         --  Flag used to mark when at least one external constituent is part
+         --  of the state refinement.
+
          Non_Null_Seen : Boolean := False;
          Null_Seen     : Boolean := False;
          --  Flags used to detect multiple uses of null in a single clause or a
          --  mixture of null and non-null constituents.
 
+         State    : Node_Id;
+         State_Id : Entity_Id;
+         --  The state being refined in the current clause
+
          procedure Analyze_Constituent (Constit : Node_Id);
          --  Perform full analysis of a single constituent
 
-         procedure Check_Matching_State
-           (State    : Node_Id;
-            State_Id : Entity_Id);
-         --  Determine whether state State denoted by its name State_Id appears
-         --  in Abstr_States. Emit an error when attempting to re-refine the
-         --  state or when the state is not defined in the package declaration.
-         --  Otherwise remove the state from Abstr_States.
+         procedure Check_External_Property
+           (Prop_Nam : Name_Id;
+            Enabled  : Boolean;
+            Constit  : Entity_Id);
+         --  Determine whether a property denoted by name Prop_Nam is present
+         --  in both the refined state and constituent Constit. Flag Enabled
+         --  should be set when the property applies to the refined state. If
+         --  this is not the case, emit an error message.
 
+         procedure Check_Matching_State;
+         --  Determine whether the state being refined appears in Abstr_States.
+         --  Emit an error when attempting to re-refine the state or when the
+         --  state is not defined in the package declaration. Otherwise remove
+         --  the state from Abstr_States.
+
          -------------------------
          -- Analyze_Constituent --
          -------------------------
@@ -22276,6 +22296,29 @@
                   --  body declarations end (see routine Analyze_Declarations).
 
                   Set_Has_Visible_Refinement (State_Id);
+
+                  --  When the constituent is external, save its relevant
+                  --  property for further checks.
+
+                  if Async_Readers_Enabled (Constit_Id) then
+                     AR_Constit := Constit_Id;
+                     External_Constit_Seen := True;
+                  end if;
+
+                  if Async_Writers_Enabled (Constit_Id) then
+                     AW_Constit := Constit_Id;
+                     External_Constit_Seen := True;
+                  end if;
+
+                  if Effective_Reads_Enabled (Constit_Id) then
+                     ER_Constit := Constit_Id;
+                     External_Constit_Seen := True;
+                  end if;
+
+                  if Effective_Writes_Enabled (Constit_Id) then
+                     EW_Constit := Constit_Id;
+                     External_Constit_Seen := True;
+                  end if;
                end Collect_Constituent;
 
                --  Local variables
@@ -22426,14 +22469,44 @@
             end if;
          end Analyze_Constituent;
 
+         -----------------------------
+         -- Check_External_Property --
+         -----------------------------
+
+         procedure Check_External_Property
+           (Prop_Nam : Name_Id;
+            Enabled  : Boolean;
+            Constit  : Entity_Id)
+         is
+         begin
+            Error_Msg_Name_1 := Prop_Nam;
+
+            --  The property is enabled in the related Abstract_State pragma
+            --  that defines the state.
+
+            if Enabled then
+               if No (Constit) then
+                  Error_Msg_NE
+                    ("external state & requires at least one constituent with "
+                     & "property % (SPARK RM 7.2.8(3))", State, State_Id);
+               end if;
+
+            --  The property is missing in the declaration of the state, but a
+            --  constituent is introducing it in the state refinement.
+
+            elsif Present (Constit) then
+               Error_Msg_Name_2 := Chars (Constit);
+               Error_Msg_NE
+                 ("external state & lacks property % set by constituent % "
+                  & "(SPARK RM 7.2.8(3))", State, State_Id);
+            end if;
+         end Check_External_Property;
+
          --------------------------
          -- Check_Matching_State --
          --------------------------
 
-         procedure Check_Matching_State
-           (State    : Node_Id;
-            State_Id : Entity_Id)
-         is
+         procedure Check_Matching_State is
             State_Elmt : Elmt_Id;
 
          begin
@@ -22478,8 +22551,10 @@
 
          --  Local declarations
 
-         Constit : Node_Id;
-         State   : Node_Id;
+         Body_Ref      : Node_Id;
+         Body_Ref_Elmt : Elmt_Id;
+         Constit       : Node_Id;
+         Extra_State   : Node_Id;
 
       --  Start of processing for Analyze_Refinement_Clause
 
@@ -22487,68 +22562,61 @@
          --  Analyze the state name of a refinement clause
 
          State := First (Choices (Clause));
-         while Present (State) loop
-            if Present (State_Id) then
-               Error_Msg_N
-                 ("refinement clause cannot cover multiple states", State);
 
-            else
-               Analyze       (State);
-               Resolve_State (State);
+         Analyze       (State);
+         Resolve_State (State);
 
-               --  Ensure that the state name denotes a valid abstract state
-               --  that is defined in the spec of the related package.
+         --  Ensure that the state name denotes a valid abstract state that is
+         --  defined in the spec of the related package.
 
-               if Is_Entity_Name (State) then
-                  State_Id := Entity_Of (State);
+         if Is_Entity_Name (State) then
+            State_Id := Entity_Of (State);
 
-                  --  Catch any attempts to re-refine a state or refine a
-                  --  state that is not defined in the package declaration.
+            --  Catch any attempts to re-refine a state or refine a state that
+            --  is not defined in the package declaration.
 
-                  if Ekind (State_Id) = E_Abstract_State then
-                     Check_Matching_State (State, State_Id);
-                  else
-                     Error_Msg_NE
-                       ("& must denote an abstract state", State, State_Id);
-                  end if;
+            if Ekind (State_Id) = E_Abstract_State then
+               Check_Matching_State;
+            else
+               Error_Msg_NE
+                 ("& must denote an abstract state", State, State_Id);
+            end if;
 
-                  --  A global item cannot denote a state abstraction whose
-                  --  refinement is visible, in other words a state abstraction
-                  --  cannot be named within its enclosing package's body other
-                  --  than in its refinement.
+            --  A global item cannot denote a state abstraction whose
+            --  refinement is visible, in other words a state abstraction
+            --  cannot be named within its enclosing package's body other than
+            --  in its refinement.
 
-                  if Has_Body_References (State_Id) then
-                     declare
-                        Ref      : Node_Id;
-                        Ref_Elmt : Elmt_Id;
+            if Has_Body_References (State_Id) then
+               Body_Ref_Elmt := First_Elmt (Body_References (State_Id));
+               while Present (Body_Ref_Elmt) loop
+                  Body_Ref := Node (Body_Ref_Elmt);
 
-                     begin
-                        Ref_Elmt := First_Elmt (Body_References (State_Id));
-                        while Present (Ref_Elmt) loop
-                           Ref := Node (Ref_Elmt);
+                  Error_Msg_N
+                    ("global reference to & not allowed (SPARK RM 6.1.4(8))",
+                     Body_Ref);
+                  Error_Msg_Sloc := Sloc (State);
+                  Error_Msg_N ("\refinement of & is visible#", Body_Ref);
 
-                           Error_Msg_N
-                             ("global reference to & not allowed (SPARK RM "
-                              & "6.1.4(8))", Ref);
-                           Error_Msg_Sloc := Sloc (State);
-                           Error_Msg_N ("\refinement of & is visible#", Ref);
+                  Next_Elmt (Body_Ref_Elmt);
+               end loop;
+            end if;
 
-                           Next_Elmt (Ref_Elmt);
-                        end loop;
-                     end;
-                  end if;
+            --  The state name is illegal
 
-               --  The state name is illegal
+         else
+            Error_Msg_N ("malformed state name in refinement clause", State);
+         end if;
 
-               else
-                  Error_Msg_N
-                    ("malformed state name in refinement clause", State);
-               end if;
-            end if;
+         --  A refinement clause may only refine one state at a time
 
-            Next (State);
-         end loop;
+         Extra_State := Next (State);
 
+         if Present (Extra_State) then
+            Error_Msg_N
+              ("refinement clause cannot cover multiple states", Extra_State);
+         end if;
+
          --  Analyze all constituents of the refinement. Multiple constituents
          --  appear as an aggregate.
 
@@ -22575,6 +22643,60 @@
          else
             Analyze_Constituent (Constit);
          end if;
+
+         --  A refined external state is subject to special rules with respect
+         --  to its properties and constituents.
+
+         if Is_External_State (State_Id) then
+
+            --  The set of properties that all external constituents yield must
+            --  match that of the refined state. There are two cases to detect:
+            --  the refined state lacks a property or has an extra property.
+
+            if External_Constit_Seen then
+               Check_External_Property
+                 (Prop_Nam => Name_Async_Readers,
+                  Enabled  => Async_Readers_Enabled (State_Id),
+                  Constit  => AR_Constit);
+
+               Check_External_Property
+                 (Prop_Nam => Name_Async_Writers,
+                  Enabled  => Async_Writers_Enabled (State_Id),
+                  Constit  => AW_Constit);
+
+               Check_External_Property
+                 (Prop_Nam => Name_Effective_Reads,
+                  Enabled  => Effective_Reads_Enabled (State_Id),
+                  Constit  => ER_Constit);
+
+               Check_External_Property
+                 (Prop_Nam => Name_Effective_Writes,
+                  Enabled  => Effective_Writes_Enabled (State_Id),
+                  Constit  => EW_Constit);
+
+            --  An external state may be refined to null (SPARK RM 7.2.8(2))
+
+            elsif Null_Seen then
+               null;
+
+            --  The external state has constituents, but none of them are
+            --  external.
+
+            else
+               Error_Msg_NE
+                 ("external state & requires at least one external "
+                  & "constituent or null refinement (SPARK RM 7.2.8(2))",
+                  State, State_Id);
+            end if;
+
+         --  When a refined state is not external, it should not have external
+         --  constituents.
+
+         elsif External_Constit_Seen then
+            Error_Msg_NE
+              ("non-external state & cannot contain external constituents in "
+               & "refinement (SPARK RM 7.2.8(1))", State, State_Id);
+         end if;
       end Analyze_Refinement_Clause;
 
       ---------------------------
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 207141)
+++ sem_util.adb	(working copy)
@@ -114,11 +114,11 @@
    --  have a default.
 
    function Has_Enabled_Property
-     (Extern   : Node_Id;
+     (State_Id : Node_Id;
       Prop_Nam : Name_Id) return Boolean;
    --  Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled.
-   --  Given pragma External, determine whether it contains a property denoted
-   --  by its name Prop_Nam and if it does, whether its expression is True.
+   --  Determine whether an abstract state denoted by its entity State_Id has
+   --  enabled property Prop_Name.
 
    function Has_Null_Extension (T : Entity_Id) return Boolean;
    --  T is a derived tagged type. Check whether the type extension is null.
@@ -560,10 +560,7 @@
    function Async_Readers_Enabled (Id : Entity_Id) return Boolean is
    begin
       if Ekind (Id) = E_Abstract_State then
-         return
-           Has_Enabled_Property
-             (Extern   => Get_Pragma (Id, Pragma_External),
-              Prop_Nam => Name_Async_Readers);
+         return Has_Enabled_Property (Id, Name_Async_Readers);
 
       else pragma Assert (Ekind (Id) = E_Variable);
          return Present (Get_Pragma (Id, Pragma_Async_Readers));
@@ -577,10 +574,7 @@
    function Async_Writers_Enabled (Id : Entity_Id) return Boolean is
    begin
       if Ekind (Id) = E_Abstract_State then
-         return
-           Has_Enabled_Property
-             (Extern   => Get_Pragma (Id, Pragma_External),
-              Prop_Nam => Name_Async_Writers);
+         return Has_Enabled_Property (Id, Name_Async_Writers);
 
       else pragma Assert (Ekind (Id) = E_Variable);
          return Present (Get_Pragma (Id, Pragma_Async_Writers));
@@ -4818,10 +4812,7 @@
    function Effective_Reads_Enabled (Id : Entity_Id) return Boolean is
    begin
       if Ekind (Id) = E_Abstract_State then
-         return
-           Has_Enabled_Property
-             (Extern   => Get_Pragma (Id, Pragma_External),
-              Prop_Nam => Name_Effective_Reads);
+         return Has_Enabled_Property (Id, Name_Effective_Reads);
 
       else pragma Assert (Ekind (Id) = E_Variable);
          return Present (Get_Pragma (Id, Pragma_Effective_Reads));
@@ -4835,10 +4826,7 @@
    function Effective_Writes_Enabled (Id : Entity_Id) return Boolean is
    begin
       if Ekind (Id) = E_Abstract_State then
-         return
-           Has_Enabled_Property
-             (Extern   => Get_Pragma (Id, Pragma_External),
-              Prop_Nam => Name_Effective_Writes);
+         return Has_Enabled_Property (Id, Name_Effective_Writes);
 
       else pragma Assert (Ekind (Id) = E_Variable);
          return Present (Get_Pragma (Id, Pragma_Effective_Writes));
@@ -7182,69 +7170,86 @@
    --------------------------
 
    function Has_Enabled_Property
-     (Extern   : Node_Id;
+     (State_Id : Node_Id;
       Prop_Nam : Name_Id) return Boolean
    is
-      Prop  : Node_Id;
-      Props : Node_Id := Empty;
+      Decl    : constant Node_Id := Parent (State_Id);
+      Opt     : Node_Id;
+      Opt_Nam : Node_Id;
+      Prop    : Node_Id;
+      Props   : Node_Id;
 
    begin
-      --  The related abstract state or variable do not have an Extern pragma,
-      --  the property in question cannot be set.
+      --  The declaration of an external abstract state appears as an extension
+      --  aggregate. If this is not the case, properties can never be set.
 
-      if No (Extern) then
+      if Nkind (Decl) /= N_Extension_Aggregate then
          return False;
-
-      elsif Nkind (Extern) = N_Component_Association then
-         Props := Expression (Extern);
       end if;
 
-      --  External state with properties
+      --  When External appears as a simple option, it automatically enables
+      --  all properties.
 
-      if Present (Props) then
+      Opt := First (Expressions (Decl));
+      while Present (Opt) loop
+         if Nkind (Opt) = N_Identifier
+           and then Chars (Opt) = Name_External
+         then
+            return True;
+         end if;
 
-         --  Multiple properties appear as an aggregate
+         Next (Opt);
+      end loop;
 
-         if Nkind (Props) = N_Aggregate then
+      --  When External specifies particular properties, inspect those and
+      --  find the desired one (if any).
 
-            --  Simple property form
+      Opt := First (Component_Associations (Decl));
+      while Present (Opt) loop
+         Opt_Nam := First (Choices (Opt));
 
-            Prop := First (Expressions (Props));
-            while Present (Prop) loop
-               if Chars (Prop) = Prop_Nam then
-                  return True;
-               end if;
+         if Nkind (Opt_Nam) = N_Identifier
+           and then Chars (Opt_Nam) = Name_External
+         then
+            Props := Expression (Opt);
 
-               Next (Prop);
-            end loop;
+            --  Multiple properties appear as an aggregate
 
-            --  Property with expression form
+            if Nkind (Props) = N_Aggregate then
 
-            Prop := First (Component_Associations (Props));
-            while Present (Prop) loop
-               if Chars (Prop) = Prop_Nam then
-                  return Is_True (Expr_Value (Expression (Prop)));
-               end if;
+               --  Simple property form
 
-               Next (Prop);
-            end loop;
+               Prop := First (Expressions (Props));
+               while Present (Prop) loop
+                  if Chars (Prop) = Prop_Nam then
+                     return True;
+                  end if;
 
-            --  Pragma Extern contains properties, but not the one we want
+                  Next (Prop);
+               end loop;
 
-            return False;
+               --  Property with expression form
 
-         --  Single property
+               Prop := First (Component_Associations (Props));
+               while Present (Prop) loop
+                  if Chars (Prop) = Prop_Nam then
+                     return Is_True (Expr_Value (Expression (Prop)));
+                  end if;
 
-         else
-            return Chars (Prop) = Prop_Nam;
+                  Next (Prop);
+               end loop;
+
+            --  Single property
+
+            else
+               return Chars (Prop) = Prop_Nam;
+            end if;
          end if;
 
-      --  An external state defined without any properties defaults all
-      --  properties to True;
+         Next (Opt);
+      end loop;
 
-      else
-         return True;
-      end if;
+      return False;
    end Has_Enabled_Property;
 
    --------------------


More information about the Gcc-patches mailing list