[Ada] Allow Refined_Global/Depends contracts with partial refinement

Arnaud Charlet charlet@adacore.com
Wed Oct 12 13:55:00 GMT 2016


Pragmas/aspects Refined_Global and Refined_Depends may be applied in
a scope where only partial refinement of abstract states is visible,
as defined in SPARK RM 7.2.4. In such a case, the partial refinement
should be used instead of the full refinement for checking the refined
contracts.

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

2016-10-12  Yannick Moy  <moy@adacore.com>

	* einfo.adb, einfo.ads (Has_Partial_Visible_Refinement): New flag
	in abtract states.
	(Has_Non_Null_Visible_Refinement): Return true for patial refinement.
	(Partial_Refinement_Constituents): New function returns the full or
	partial refinement constituents depending on scope.
	* sem_ch3.adb (Analyze_Declarations): Remove partial visible
	refinements when exiting the scope of a package spec or body
	and those partial refinements are not in scope afterwards.
	* sem_ch7.adb, sem_ch7.ads (Install_Partial_Declarations): Mark
	abstract states of parent units with partial refinement so that
	it is visible.
	* sem_prag.adb (Analyze_Part_Of_In_Decl_Part): Mark enclosing
	abstract state if any as having partial refinement in that scope.
	(Analyze_Refined_Global_In_Decl_Part): Check constituent usage
	based on full or partial refinement depending on scope.

-------------- next part --------------
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 241041)
+++ sem_ch3.adb	(working copy)
@@ -2178,10 +2178,17 @@
       --  case, add a proper spec if the body lacks one. The spec is inserted
       --  before Body_Decl and immediately analyzed.
 
+      procedure Remove_Partial_Visible_Refinements (Spec_Id : Entity_Id);
+      --  Spec_Id is the entity of a package that may define abstract states,
+      --  and in the case of a child unit, whose ancestors may define abstract
+      --  states. If the states have partial visible refinement, remove the
+      --  partial visibility of each constituent at the end of the package
+      --  spec and body declarations.
+
       procedure Remove_Visible_Refinements (Spec_Id : Entity_Id);
       --  Spec_Id is the entity of a package that may define abstract states.
       --  If the states have visible refinement, remove the visibility of each
-      --  constituent at the end of the package body declarations.
+      --  constituent at the end of the package body declaration.
 
       -----------------
       -- Adjust_Decl --
@@ -2335,6 +2342,29 @@
          Insert_Before_And_Analyze (Body_Decl, Decl);
       end Handle_Late_Controlled_Primitive;
 
+      ----------------------------------------
+      -- Remove_Partial_Visible_Refinements --
+      ----------------------------------------
+
+      procedure Remove_Partial_Visible_Refinements (Spec_Id : Entity_Id) is
+         State_Elmt : Elmt_Id;
+      begin
+         if Present (Abstract_States (Spec_Id)) then
+            State_Elmt := First_Elmt (Abstract_States (Spec_Id));
+            while Present (State_Elmt) loop
+               Set_Has_Partial_Visible_Refinement (Node (State_Elmt), False);
+               Next_Elmt (State_Elmt);
+            end loop;
+         end if;
+
+         --  For a child unit, also hide the partial state refinement from
+         --  ancestor packages.
+
+         if Is_Child_Unit (Spec_Id) then
+            Remove_Partial_Visible_Refinements (Scope (Spec_Id));
+         end if;
+      end Remove_Partial_Visible_Refinements;
+
       --------------------------------
       -- Remove_Visible_Refinements --
       --------------------------------
@@ -2576,6 +2606,15 @@
             --  restore the original state conditions.
 
             Remove_Visible_Refinements (Corresponding_Spec (Context));
+            Remove_Partial_Visible_Refinements (Corresponding_Spec (Context));
+
+         elsif Nkind (Context) = N_Package_Declaration then
+
+            --  Partial state refinements are visible up to the end of the
+            --  package spec declarations. Hide the partial state refinements
+            --  from visibility to restore the original state conditions.
+
+            Remove_Partial_Visible_Refinements (Corresponding_Spec (Context));
          end if;
 
          --  Verify that all abstract states found in any package declared in
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb	(revision 241024)
+++ sem_ch7.adb	(working copy)
@@ -2275,6 +2275,34 @@
          Next_Entity (Id);
       end loop;
 
+      --  An abstract state is partially refined when it has at least one
+      --  Part_Of constituent. Since these constituents are being installed
+      --  into visibility, update the partial refinement status of any state
+      --  defined in the associated package, subject to at least one Part_Of
+      --  constituent.
+
+      if Ekind_In (P, E_Generic_Package, E_Package) then
+         declare
+            States     : constant Elist_Id := Abstract_States (P);
+            State_Elmt : Elmt_Id;
+            State_Id   : Entity_Id;
+
+         begin
+            if Present (States) then
+               State_Elmt := First_Elmt (States);
+               while Present (State_Elmt) loop
+                  State_Id := Node (State_Elmt);
+
+                  if Present (Part_Of_Constituents (State_Id)) then
+                     Set_Has_Partial_Visible_Refinement (State_Id);
+                  end if;
+
+                  Next_Elmt (State_Elmt);
+               end loop;
+            end if;
+         end;
+      end if;
+
       --  Indicate that the private part is currently visible, so it can be
       --  properly reset on exit.
 
Index: sem_ch7.ads
===================================================================
--- sem_ch7.ads	(revision 241024)
+++ sem_ch7.ads	(working copy)
@@ -46,10 +46,10 @@
    --  On entrance to a package body, make declarations in package spec
    --  immediately visible.
    --
-   --  When compiling the body of a package,  both routines are called in
+   --  When compiling the body of a package, both routines are called in
    --  succession. When compiling the body of a child package, the call
    --  to Install_Private_Declaration is immediate for private children,
-   --  but is deferred until the compilation of the  private part of the
+   --  but is deferred until the compilation of the private part of the
    --  child for public child packages.
 
    function Unit_Requires_Body
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 241024)
+++ einfo.adb	(working copy)
@@ -610,8 +610,8 @@
    --    Is_Actual_Subtype               Flag293
    --    Has_Pragma_Unused               Flag294
    --    Is_Ignored_Transient            Flag295
+   --    Has_Partial_Visible_Refinement  Flag296
 
-   --    (unused)                        Flag296
    --    (unused)                        Flag297
    --    (unused)                        Flag298
    --    (unused)                        Flag299
@@ -1682,6 +1682,12 @@
       return Flag232 (Id);
    end Has_Own_Invariants;
 
+   function Has_Partial_Visible_Refinement (Id : E) return B is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      return Flag296 (Id);
+   end Has_Partial_Visible_Refinement;
+
    function Has_Per_Object_Constraint (Id : E) return B is
    begin
       return Flag154 (Id);
@@ -4698,6 +4704,12 @@
       Set_Flag232 (Id, V);
    end Set_Has_Own_Invariants;
 
+   procedure Set_Has_Partial_Visible_Refinement (Id : E; V : B := True) is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      Set_Flag296 (Id, V);
+   end Set_Has_Partial_Visible_Refinement;
+
    procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True) is
    begin
       Set_Flag154 (Id, V);
@@ -7485,13 +7497,14 @@
       pragma Assert (Ekind (Id) = E_Abstract_State);
       Constits := Refinement_Constituents (Id);
 
-      --  For a refinement to be non-null, the first constituent must be
-      --  anything other than null.
+      --  A partial refinement is always non-null. For a full refinement to be
+      --  non-null, the first constituent must be anything other than null.
 
       return
-        Has_Visible_Refinement (Id)
-          and then Present (Constits)
-          and then Nkind (Node (First_Elmt (Constits))) /= N_Null;
+        Has_Partial_Visible_Refinement (Id)
+          or else (Has_Visible_Refinement (Id)
+                    and then Present (Constits)
+                    and then Nkind (Node (First_Elmt (Constits))) /= N_Null);
    end Has_Non_Null_Visible_Refinement;
 
    -----------------------------
@@ -8370,6 +8383,29 @@
       return Empty;
    end Partial_Invariant_Procedure;
 
+   -------------------------------------
+   -- Partial_Refinement_Constituents --
+   -------------------------------------
+
+   function Partial_Refinement_Constituents (Id : E) return L is
+      Constits : Elist_Id;
+
+   begin
+      --  "Refinement" is a concept applicable only to abstract states
+
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      Constits := Refinement_Constituents (Id);
+
+      --  A refinement may be partially visible when objects declared in the
+      --  private part of a package are subject to a Part_Of indicator.
+
+      if No (Constits) then
+         Constits := Part_Of_Constituents (Id);
+      end if;
+
+      return Constits;
+   end Partial_Refinement_Constituents;
+
    ------------------------
    -- Predicate_Function --
    ------------------------
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 241024)
+++ einfo.ads	(working copy)
@@ -1812,6 +1812,14 @@
 --       one invariant of its own. The flag is also set on the full view of a
 --       private extension or a private type for completeness.
 
+--    Has_Partial_Visible_Refinement (Flag296)
+--       Defined in E_Abstract_State entities. Set when a state has at least
+--       one refinement constituent subject to indicator Part_Of, and analysis
+--       is in the region between the declaration of the first constituent for
+--       this abstract state (in the private part of the package) and the end
+--       of the package spec or body with visibility over this private part
+--       (which includes the package itself and its child packages).
+
 --    Has_Per_Object_Constraint (Flag154)
 --       Defined in E_Component entities. Set if the subtype of the component
 --       has a per object constraint. Per object constraints result from the
@@ -3780,6 +3788,11 @@
 --       Note: the reason this is marked as a synthesized attribute is that the
 --       way this is stored is as an element of the Subprograms_For_Type field.
 
+--    Partial_Refinement_Constituents (synthesized)
+--       Present in abstract state entities. Contains the constituents that
+--       refine the state in its private part, in other words, all the hidden
+--       states that indicate this abstract state in a Part_Of aspect/pragma.
+
 --    Partial_View_Has_Unknown_Discr (Flag280)
 --       Present in all types. Set to Indicate that the partial view of a type
 --       has unknown discriminants. A default initialization of an object of
@@ -5619,6 +5632,7 @@
    --    Non_Limited_View                    (Node19)
    --    Encapsulating_State                 (Node32)
    --    From_Limited_With                   (Flag159)
+   --    Has_Partial_Visible_Refinement      (Flag296)
    --    Has_Visible_Refinement              (Flag263)
    --    Has_Non_Limited_View                (synth)
    --    Has_Non_Null_Visible_Refinement     (synth)
@@ -5626,6 +5640,7 @@
    --    Is_External_State                   (synth)
    --    Is_Null_State                       (synth)
    --    Is_Synchronized_State               (synth)
+   --    Partial_Refinement_Constituents     (synth)
 
    --  E_Access_Protected_Subprogram_Type
    --    Equivalent_Type                     (Node18)
@@ -6977,6 +6992,7 @@
    function Has_Object_Size_Clause              (Id : E) return B;
    function Has_Out_Or_In_Out_Parameter         (Id : E) return B;
    function Has_Own_Invariants                  (Id : E) return B;
+   function Has_Partial_Visible_Refinement      (Id : E) return B;
    function Has_Per_Object_Constraint           (Id : E) return B;
    function Has_Pragma_Controlled               (Id : E) return B;
    function Has_Pragma_Elaborate_Body           (Id : E) return B;
@@ -7412,6 +7428,7 @@
    function Number_Entries                      (Id : E) return Nat;
    function Number_Formals                      (Id : E) return Pos;
    function Parameter_Mode                      (Id : E) return Formal_Kind;
+   function Partial_Refinement_Constituents     (Id : E) return L;
    function Primitive_Operations                (Id : E) return L;
    function Root_Type                           (Id : E) return E;
    function Safe_Emax_Value                     (Id : E) return U;
@@ -7652,6 +7669,7 @@
    procedure Set_Has_Object_Size_Clause          (Id : E; V : B := True);
    procedure Set_Has_Out_Or_In_Out_Parameter     (Id : E; V : B := True);
    procedure Set_Has_Own_Invariants              (Id : E; V : B := True);
+   procedure Set_Has_Partial_Visible_Refinement  (Id : E; V : B := True);
    procedure Set_Has_Per_Object_Constraint       (Id : E; V : B := True);
    procedure Set_Has_Pragma_Controlled           (Id : E; V : B := True);
    procedure Set_Has_Pragma_Elaborate_Body       (Id : E; V : B := True);
@@ -8444,6 +8462,7 @@
    pragma Inline (Has_Object_Size_Clause);
    pragma Inline (Has_Out_Or_In_Out_Parameter);
    pragma Inline (Has_Own_Invariants);
+   pragma Inline (Has_Partial_Visible_Refinement);
    pragma Inline (Has_Per_Object_Constraint);
    pragma Inline (Has_Pragma_Controlled);
    pragma Inline (Has_Pragma_Elaborate_Body);
@@ -8959,6 +8978,7 @@
    pragma Inline (Set_Has_Object_Size_Clause);
    pragma Inline (Set_Has_Out_Or_In_Out_Parameter);
    pragma Inline (Set_Has_Own_Invariants);
+   pragma Inline (Set_Has_Partial_Visible_Refinement);
    pragma Inline (Set_Has_Per_Object_Constraint);
    pragma Inline (Set_Has_Pragma_Controlled);
    pragma Inline (Set_Has_Pragma_Elaborate_Body);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 241041)
+++ sem_prag.adb	(working copy)
@@ -3410,6 +3410,13 @@
 
          Append_Elmt (Var_Id, Constits);
          Set_Encapsulating_State (Var_Id, Encap_Id);
+
+         --  A Part_Of constituent partially refines an abstract state. This
+         --  property does not apply to protected or task units.
+
+         if Ekind (Encap_Id) = E_Abstract_State then
+            Set_Has_Partial_Visible_Refinement (Encap_Id);
+         end if;
       end if;
 
       --  Emit a clarification message when the encapsulator is undefined,
@@ -18717,7 +18724,7 @@
 
             Add_Contract_Item (N, Item_Id);
 
-            --  A variable may act as consituent of a single concurrent type
+            --  A variable may act as constituent of a single concurrent type
             --  which in turn could be declared after the variable. Due to this
             --  discrepancy, the full analysis of indicator Part_Of is delayed
             --  until the end of the enclosing declarative region (see routine
@@ -24051,7 +24058,7 @@
 
          procedure Check_Constituent_Usage (State_Id : Entity_Id) is
             Constits     : constant Elist_Id :=
-                             Refinement_Constituents (State_Id);
+                             Partial_Refinement_Constituents (State_Id);
             Constit_Elmt : Elmt_Id;
             Constit_Id   : Entity_Id;
             Posted       : Boolean := False;
@@ -24614,7 +24621,7 @@
 
          procedure Check_Constituent_Usage (State_Id : Entity_Id) is
             Constits      : constant Elist_Id :=
-                              Refinement_Constituents (State_Id);
+                              Partial_Refinement_Constituents (State_Id);
             Constit_Elmt  : Elmt_Id;
             Constit_Id    : Entity_Id;
             Has_Missing   : Boolean := False;
@@ -24753,7 +24760,7 @@
 
          procedure Check_Constituent_Usage (State_Id : Entity_Id) is
             Constits     : constant Elist_Id :=
-                             Refinement_Constituents (State_Id);
+                             Partial_Refinement_Constituents (State_Id);
             Constit_Elmt : Elmt_Id;
             Constit_Id   : Entity_Id;
             In_Seen      : Boolean := False;
@@ -24853,7 +24860,7 @@
 
          procedure Check_Constituent_Usage (State_Id : Entity_Id) is
             Constits     : constant Elist_Id :=
-                             Refinement_Constituents (State_Id);
+                             Partial_Refinement_Constituents (State_Id);
             Constit_Elmt : Elmt_Id;
             Constit_Id   : Entity_Id;
             Posted       : Boolean := False;
@@ -24952,7 +24959,7 @@
 
          procedure Check_Constituent_Usage (State_Id : Entity_Id) is
             Constits      : constant Elist_Id :=
-                              Refinement_Constituents (State_Id);
+                              Partial_Refinement_Constituents (State_Id);
             Constit_Elmt  : Elmt_Id;
             Constit_Id    : Entity_Id;
             Proof_In_Seen : Boolean := False;
@@ -25083,7 +25090,10 @@
 
             if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
              and then Present (Encapsulating_State (Item_Id))
-             and then Has_Visible_Refinement (Encapsulating_State (Item_Id))
+             and then
+               (Has_Visible_Refinement (Encapsulating_State (Item_Id))
+                  or else
+                Has_Partial_Visible_Refinement (Encapsulating_State (Item_Id)))
              and then Contains (States, Encapsulating_State (Item_Id))
             then
                if Global_Mode = Name_Input then
@@ -25438,10 +25448,10 @@
       --  Non-instance case
 
       else
-         --  The corresponding Global pragma must mention at least one state
-         --  witha visible refinement at the point Refined_Global is processed.
-         --  States with null refinements need Refined_Global pragma
-         --  (SPARK RM 7.2.4(2)).
+         --  The corresponding Global pragma must mention at least one
+         --  state with a visible refinement at the point Refined_Global
+         --  is processed. States with null refinements need Refined_Global
+         --  pragma (SPARK RM 7.2.4(2)).
 
          if not Has_In_State
            and then not Has_In_Out_State


More information about the Gcc-patches mailing list