Patchwork [Ada] Hidden state detection

login
register
mail settings
Submitter Arnaud Charlet
Date April 25, 2013, 10:29 a.m.
Message ID <20130425102905.GA9820@adacore.com>
Download mbox | patch
Permalink /patch/239468/
State New
Headers show

Comments

Arnaud Charlet - April 25, 2013, 10:29 a.m.
This patch adds machinery to catch illegal object or state declarations that
introduce a hidden state within a package subject to a null abstract state.

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

--  gen.ads

generic
   type Data_Type is private;

package Gen is
   Visible_Obj : Data_Type;

private
   Private_Obj : Data_Type;

end Gen;

--  semantics.ads

with Gen;

package Semantics
   with Abstract_State => null
is
   pragma Elaborate_Body;

   OK_1 : Integer;  --  in visible declarations

   package Visible_Instance is new Gen (Integer);
   --  Visible_Obj is ok
   --  Private_Obj is an error

   package Visible_Nested
      with Abstract_State => Error_1  --  introduces state
   is
      OK_2 : Integer;  --  in visible declarations of a visible package
   private
      Error_2 : Integer;  --  in private part regardless of visibility
   end Visible_Nested;

private
   Error_3 : Integer;  --  in private part

   package Private_Instance is new Gen (Integer);
   --  Visible_Obj is an error
   --  Private_Obj is an error

   package Private_Nested
      with Abstract_State => Error_4  --  introduces state
   is
      Error_5 : Integer;  --  in visible declarations but in private part
   private
      Error_6 : Integer;  --  in private part
   end Private_Nested;
end Semantics;

--  semantics.adb

package body Semantics is
   Error_7 : Integer;  --  in body

   package Body_Instance is new Gen (Integer);
   --  Visible_Obj is an error
   --  Private_Obj is an error

   package Body_Nested
     with Abstract_State => Error_8  --  introduces state
   is
      Error_9 : Integer;  --  in visible declarations but in body
      procedure Proc;
   private
      Error_10 : Integer;  --  in private part
   end Body_Nested;

   package body Body_Nested is
      Error_11 : Integer;  --  in body

      procedure Proc is
         OK_3 : Integer;  --  nested in subprogram

         package Proc_Instance is new Gen (Integer);
         --  Visible_Obj is ok
         --  Private_Obj is ok

         package Proc_Nested
           with Abstract_State => OK_4  --  nested in subprogram
         is
            OK_5 : Integer;  --  nested in subprogram
         private
            OK_6 : Integer;  --  nested in subprogram
         end Proc_Nested;
      begin
         null;
      end Proc;
   end Body_Nested;
end Semantics;

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

$ gcc -c -gnat12 -gnatd.V semantics.adb
semantics.adb:2:04: cannot introduce hidden state "Error_7"
semantics.adb:2:04: package "Semantics" has null abstract state
semantics.adb:4:04: instantiation error at gen.ads:5
semantics.adb:4:04: cannot introduce hidden state "Visible_Obj"
semantics.adb:4:04: package "Semantics" has null abstract state
semantics.adb:4:04: instantiation error at gen.ads:8
semantics.adb:4:04: cannot introduce hidden state "Private_Obj"
semantics.adb:4:04: package "Semantics" has null abstract state
semantics.adb:9:29: cannot introduce hidden state "Error_8"
semantics.adb:9:29: package "Semantics" has null abstract state
semantics.adb:11:07: cannot introduce hidden state "Error_9"
semantics.adb:11:07: package "Semantics" has null abstract state
semantics.adb:14:07: cannot introduce hidden state "Error_10"
semantics.adb:14:07: package "Semantics" has null abstract state
semantics.adb:18:07: cannot introduce hidden state "Error_11"
semantics.adb:18:07: package "Semantics" has null abstract state
semantics.ads:10:04: instantiation error at gen.ads:8
semantics.ads:10:04: cannot introduce hidden state "Private_Obj"
semantics.ads:10:04: package "Semantics" has null abstract state
semantics.ads:15:30: cannot introduce hidden state "Error_1"
semantics.ads:15:30: package "Semantics" has null abstract state
semantics.ads:19:07: cannot introduce hidden state "Error_2"
semantics.ads:19:07: package "Semantics" has null abstract state
semantics.ads:23:04: cannot introduce hidden state "Error_3"
semantics.ads:23:04: package "Semantics" has null abstract state
semantics.ads:25:04: instantiation error at gen.ads:5
semantics.ads:25:04: cannot introduce hidden state "Visible_Obj"
semantics.ads:25:04: package "Semantics" has null abstract state
semantics.ads:25:04: instantiation error at gen.ads:8
semantics.ads:25:04: cannot introduce hidden state "Private_Obj"
semantics.ads:25:04: package "Semantics" has null abstract state
semantics.ads:30:30: cannot introduce hidden state "Error_4"
semantics.ads:30:30: package "Semantics" has null abstract state
semantics.ads:32:07: cannot introduce hidden state "Error_5"
semantics.ads:32:07: package "Semantics" has null abstract state
semantics.ads:34:07: cannot introduce hidden state "Error_6"
semantics.ads:34:07: package "Semantics" has null abstract state

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

2013-04-25  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb (Abstract_States): The attribute now applies to
	generic packages.
	* sem_ch3.adb (Analyze_Object_Declaration): Check whether an
	object declaration introduces an illegal hidden state.
	* sem_prag.adb (Analyze_Abstract_State): Check whether a state
	declaration introduces an illegal hidden state.
	* sem_util.ads, sem_util.adb (Check_No_Hidden_State): New routine.

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 198286)
+++ sem_ch3.adb	(working copy)
@@ -3720,6 +3720,13 @@ 
       end if;
 
       Analyze_Dimension (N);
+
+      --  Verify whether the object declaration introduces an illegal hidden
+      --  state within a package subject to a null abstract state.
+
+      if Formal_Extensions and then Ekind (Id) = E_Variable then
+         Check_No_Hidden_State (Id);
+      end if;
    end Analyze_Object_Declaration;
 
    ---------------------------
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 198286)
+++ einfo.adb	(working copy)
@@ -666,7 +666,7 @@ 
 
    function Abstract_States (Id : E) return L is
    begin
-      pragma Assert (Ekind (Id) = E_Package);
+      pragma Assert (Ekind_In (Id, E_Generic_Package, E_Package));
       return Elist25 (Id);
    end Abstract_States;
 
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 198275)
+++ sem_prag.adb	(working copy)
@@ -8518,6 +8518,13 @@ 
                   Pop_Scope;
                end if;
 
+               --  Verify whether the state introduces an illegal hidden state
+               --  within a package subject to a null abstract state.
+
+               if Formal_Extensions then
+                  Check_No_Hidden_State (Id);
+               end if;
+
                --  Associate the state with its related package
 
                if No (Abstract_States (Pack_Id)) then
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 198284)
+++ sem_util.adb	(working copy)
@@ -2125,6 +2125,98 @@ 
       end if;
    end Check_Nested_Access;
 
+   ---------------------------
+   -- Check_No_Hidden_State --
+   ---------------------------
+
+   procedure Check_No_Hidden_State (Id : Entity_Id) is
+      function Has_Null_Abstract_State (Pkg : Entity_Id) return Boolean;
+      --  Determine whether the entity of a package denoted by Pkg has a null
+      --  abstract state.
+
+      -----------------------------
+      -- Has_Null_Abstract_State --
+      -----------------------------
+
+      function Has_Null_Abstract_State (Pkg : Entity_Id) return Boolean is
+         States : constant Elist_Id := Abstract_States (Pkg);
+
+      begin
+         --  Check the first available state of the related package. A null
+         --  abstract state always appears as the sole element of the state
+         --  list.
+
+         return
+           Present (States)
+             and then Is_Null_State (Node (First_Elmt (States)));
+      end Has_Null_Abstract_State;
+
+      --  Local variables
+
+      Context     : Entity_Id := Empty;
+      Not_Visible : Boolean   := False;
+      Scop        : Entity_Id;
+
+   --  Start of processing for Check_No_Hidden_State
+
+   begin
+      pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
+
+      --  Find the proper context where the object or state appears
+
+      Scop := Scope (Id);
+      while Present (Scop) loop
+         Context := Scop;
+
+         --  Keep track of the context's visibility
+
+         Not_Visible := Not_Visible or else In_Private_Part (Context);
+
+         --  Prevent the search from going too far
+
+         if Context = Standard_Standard then
+            return;
+
+         --  Objects and states that appear immediately within a subprogram or
+         --  inside a construct nested within a subprogram do not introduce a
+         --  hidden state. They behave as local variable declarations.
+
+         elsif Is_Subprogram (Context) then
+            return;
+
+         --  When examining a package body, use the entity of the spec as it
+         --  carries the abstract state declarations.
+
+         elsif Ekind (Context) = E_Package_Body then
+            Context := Spec_Entity (Context);
+         end if;
+
+         --  Stop the traversal when a package subject to a null abstract state
+         --  has been found.
+
+         if Ekind_In (Context, E_Generic_Package, E_Package)
+           and then Has_Null_Abstract_State (Context)
+         then
+            exit;
+         end if;
+
+         Scop := Scope (Scop);
+      end loop;
+
+      --  At this point we know that there is at least one package with a null
+      --  abstract state in visibility. Emit an error message unconditionally
+      --  if the entity being processed is a state because the placement of the
+      --  related package is irrelevant. This is not the case for objects as
+      --  the intermediate context matters.
+
+      if Present (Context)
+        and then (Ekind (Id) = E_Abstract_State or else Not_Visible)
+      then
+         Error_Msg_N ("cannot introduce hidden state &", Id);
+         Error_Msg_NE ("\package & has null abstract state", Id, Context);
+      end if;
+   end Check_No_Hidden_State;
+
    ------------------------------------------
    -- Check_Potentially_Blocking_Operation --
    ------------------------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 198283)
+++ sem_util.ads	(working copy)
@@ -168,14 +168,14 @@ 
    --  the compilation unit, and install it in the Elaboration_Entity field
    --  of Spec_Id, the entity for the compilation unit.
 
-      procedure Build_Explicit_Dereference
-        (Expr : Node_Id;
-         Disc : Entity_Id);
-      --  AI05-139: Names with implicit dereference. If the expression N is a
-      --  reference type and the context imposes the corresponding designated
-      --  type, convert N into N.Disc.all. Such expressions are always over-
-      --  loaded with both interpretations, and the dereference interpretation
-      --  carries the name of the reference discriminant.
+   procedure Build_Explicit_Dereference
+     (Expr : Node_Id;
+      Disc : Entity_Id);
+   --  AI05-139: Names with implicit dereference. If the expression N is a
+   --  reference type and the context imposes the corresponding designated
+   --  type, convert N into N.Disc.all. Such expressions are always over-
+   --  loaded with both interpretations, and the dereference interpretation
+   --  carries the name of the reference discriminant.
 
    function Cannot_Raise_Constraint_Error (Expr : Node_Id) return Boolean;
    --  Returns True if the expression cannot possibly raise Constraint_Error.
@@ -231,6 +231,10 @@ 
    --  is accessed inside a nested procedure, and set Has_Up_Level_Access flag
    --  accordingly. This is currently only enabled for VM_Target /= No_VM.
 
+   procedure Check_No_Hidden_State (Id : Entity_Id);
+   --  Determine whether object or state Id introduces a hidden state. If this
+   --  is the case, emit an error.
+
    procedure Check_Potentially_Blocking_Operation (N : Node_Id);
    --  N is one of the statement forms that is a potentially blocking
    --  operation. If it appears within a protected action, emit warning.