Patchwork [Ada] Cleanup invariant support

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 26, 2010, 1:12 p.m.
Message ID <20101026131251.GA26104@adacore.com>
Download mbox | patch
Permalink /patch/69248/
State New
Headers show

Comments

Arnaud Charlet - Oct. 26, 2010, 1:12 p.m.
There were quite a few problems with invariant aspect support which
are cleaned up by this patch. The most important change is that the
invariant procedure is now built at the end of the visible part,
rather than at the point of the full declaration, giving proper
visibility for the invariant expression. Also several cases where
an invariant procedure was not built when it should be are fixed.

The following tests are compiled with -gnata12 -gnatld7 -gnatj60
Previous to this patch, missinv1 and missinv2 compiled quietly,
and missinv3 did not raise an invariant error:

     1. pragma Ada_2012;
     2. procedure missinv1 is
     3.     package ip is
     4.        type r is private
     5.          with invariant => 127;
                                   |
        >>> expected type "Standard.Boolean"
            found type universal integer

     6.     private
     7.        type r is new integer;
     8.     end ip;
     9.     use ip;
    10.     rv : r;
    11. begin
    12.     null;
    13.     return;
    14. end missinv1;

     1. pragma Ada_2012;
     2. procedure missinv2 is
     3.     package ip is
     4.        type r is private
     5.          with invariant => r = 127;
                                     |
        >>> invalid operand types for operator "=", left
            operand has private type "r" defined at line 4,
            right operand has type universal integer

     6.     private
     7.        type r is new integer;
     8.     end ip;
     9.     use ip;
    10.     rv : r;
    11. begin
    12.     null;
    13.     return;
    14. end missinv2;

     1. pragma Ada_2012;
     2. procedure missinv3 is
     3.    package ip is
     4.       type r is private with
     5.         invariant => E127 (r);
     6.       function e127 (arg : r) return Boolean;
     7.
     8.    private
     9.       type r is new integer;
    10.    end ip;
    11.
    12.    package body ip is
    13.       function e127 (arg : r) return Boolean is
    14.       begin
    15.          return arg = 127;
    16.       end;
    17.    end ip;
    18.
    19.    use ip;
    20.    rv : r;
           |
        >>> warning: variable "rv" is never read and never
            assigned

    21.
    22. begin
    23.    null;
    24.    return;
    25. end missinv3;

The output from missinv3 is

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE :
 failed invariant from missinv3.adb:5

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

2010-10-26  Robert Dewar  <dewar@adacore.com>

	* sem_ch13.adb (Build_Invariant_Procedure): New calling sequence.
	(Build_Invariant_Procedure): Properly handle analysis of invariant
	expression with proper end-of-visible-decls visibility.
	* sem_ch13.ads (Build_Invariant_Procedure): Changed calling sequence.
	* sem_ch3.adb (Process_Full_View): Don't build invariant procedure
	(too late).
	(Analyze_Private_Extension_Declaration): Propagate invariant flags.
	* sem_ch7.adb (Analyze_Package_Specification): Build invariant
	procedures.

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 165957)
+++ sem_ch3.adb	(working copy)
@@ -3731,6 +3731,15 @@  package body Sem_Ch3 is
 
       Build_Derived_Record_Type (N, Parent_Type, T);
 
+      --  Propagate inherited invariant information. The new type has
+      --  invariants, if the parent type has inheritable invariants,
+      --  and these invariants can in turn be inherited.
+
+      if Has_Inheritable_Invariants (Parent_Type) then
+         Set_Has_Inheritable_Invariants (T);
+         Set_Has_Invariants (T);
+      end if;
+
       --  Ada 2005 (AI-443): Synchronized private extension or a rewritten
       --  synchronized formal derived type.
 
@@ -17439,58 +17448,15 @@  package body Sem_Ch3 is
          Set_Has_Specified_Stream_Output (Full_T);
       end if;
 
-      --  Deal with invariants
+      --  Propagate invariants to full type
 
-      if Has_Invariants (Full_T)
-           or else
-         Has_Invariants (Priv_T)
-      then
+      if Has_Invariants (Priv_T) then
          Set_Has_Invariants (Full_T);
-         Set_Has_Invariants (Priv_T);
+         Set_Invariant_Procedure (Full_T, Invariant_Procedure (Priv_T));
       end if;
 
-      if Has_Inheritable_Invariants (Full_T)
-           or else
-         Has_Inheritable_Invariants (Priv_T)
-      then
+      if Has_Inheritable_Invariants (Priv_T) then
          Set_Has_Inheritable_Invariants (Full_T);
-         Set_Has_Inheritable_Invariants (Priv_T);
-      end if;
-
-      --  This is where we build the invariant procedure if needed
-
-      if Has_Invariants (Priv_T) then
-         declare
-            PDecl : Entity_Id;
-            PBody : Entity_Id;
-            Packg : constant Node_Id := Declaration_Node (Scope (Priv_T));
-
-         begin
-            Build_Invariant_Procedure (Full_T, PDecl, PBody);
-
-            --  Error defense, normally these should be set
-
-            if Present (PDecl) and then Present (PBody) then
-
-               --  Spec goes at the end of the public part of the package.
-               --  That's behind us, so we have to manually analyze the
-               --  inserted spec.
-
-               Append_To (Visible_Declarations (Packg), PDecl);
-               Analyze (PDecl);
-
-               --  Body goes at the end of the private part of the package.
-               --  That's ahead of us so it will get analyzed later on when
-               --  we come to it.
-
-               Append_To (Private_Declarations (Packg), PBody);
-
-               --  Copy Invariant procedure to private declaration
-
-               Set_Invariant_Procedure (Priv_T, Invariant_Procedure (Full_T));
-               Set_Has_Invariants (Priv_T);
-            end if;
-         end;
       end if;
 
       --  Propagate predicates to full type
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb	(revision 165952)
+++ sem_ch7.adb	(working copy)
@@ -1128,16 +1128,26 @@  package body Sem_Ch7 is
          Analyze_Declarations (Vis_Decls);
       end if;
 
-      --  Verify that incomplete types have received full declarations
+      --  Verify that incomplete types have received full declarations and
+      --  also build invariant procedures for any types with invariants.
 
       E := First_Entity (Id);
       while Present (E) loop
+
+         --  Check on incomplete types
+
          if Ekind (E) = E_Incomplete_Type
            and then No (Full_View (E))
          then
             Error_Msg_N ("no declaration in visible part for incomplete}", E);
          end if;
 
+         --  Build invariant procedures
+
+         if Is_Type (E) and then Has_Invariants (E) then
+            Build_Invariant_Procedure (E, N);
+         end if;
+
          Next_Entity (E);
       end loop;
 
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 165945)
+++ sem_ch13.adb	(working copy)
@@ -3549,15 +3549,16 @@  package body Sem_Ch13 is
    --     ...
    --  end typInvariant;
 
-   procedure Build_Invariant_Procedure
-     (Typ   : Entity_Id;
-      PDecl : out Node_Id;
-      PBody : out Node_Id)
-   is
+   procedure Build_Invariant_Procedure (Typ : Entity_Id; N : Node_Id) is
       Loc   : constant Source_Ptr := Sloc (Typ);
       Stmts : List_Id;
       Spec  : Node_Id;
       SId   : Entity_Id;
+      PDecl : Node_Id;
+      PBody : Node_Id;
+
+      Visible_Decls : constant List_Id := Visible_Declarations (N);
+      Private_Decls : constant List_Id := Private_Declarations (N);
 
       procedure Add_Invariants (T : Entity_Id; Inherit : Boolean);
       --  Appends statements to Stmts for any invariants in the rep item chain
@@ -3570,6 +3571,10 @@  package body Sem_Ch13 is
       Object_Name : constant Name_Id := New_Internal_Name ('I');
       --  Name for argument of invariant procedure
 
+      Object_Entity : constant Node_Id :=
+                        Make_Defining_Identifier (Loc, Object_Name);
+      --  The procedure declaration entity for the argument
+
       --------------------
       -- Add_Invariants --
       --------------------
@@ -3594,7 +3599,10 @@  package body Sem_Ch13 is
            new Replace_Type_References_Generic (Replace_Type_Reference);
          --  Traverse an expression replacing all occurrences of the subtype
          --  name with appropriate references to the object that is the formal
-         --  parameter of the predicate function.
+         --  parameter of the predicate function. Note that we must ensure
+         --  that the type and entity information is properly set in the
+         --  replacement node, since we will do a Preanalyze call of this
+         --  expression without proper visibility of the procedure argument.
 
          ----------------------------
          -- Replace_Type_Reference --
@@ -3616,12 +3624,15 @@  package body Sem_Ch13 is
                      Make_Identifier (Loc,
                        Chars => Object_Name)));
 
+               Set_Entity (Expression (N), Object_Entity);
+               Set_Etype  (Expression (N), Typ);
+
             --  Invariant, replace with obj
 
             else
-               Rewrite (N,
-                 Make_Identifier (Loc,
-                   Chars => Object_Name));
+               Rewrite (N, Make_Identifier (Loc, Chars => Object_Name));
+               Set_Entity (N, Object_Entity);
+               Set_Etype  (N, Typ);
             end if;
          end Replace_Type_Reference;
 
@@ -3668,13 +3679,20 @@  package body Sem_Ch13 is
 
                Replace_Type_References (Exp, Chars (T));
 
+               --  Now we need to preanalyze the expression to properly capture
+               --  the visibility in the visible part. The expression will not
+               --  be analyzed for real until the body is analyzed, but that is
+               --  at the end of the private part and has the wrong visibility.
+
+               Set_Parent (Exp, N);
+               Preanalyze_Spec_Expression (Exp, Standard_Boolean);
+
                --  Build first two arguments for Check pragma
 
                Assoc := New_List (
                  Make_Pragma_Argument_Association (Loc,
                     Expression =>
-                      Make_Identifier (Loc,
-                        Chars => Name_Invariant)),
+                      Make_Identifier (Loc, Chars => Name_Invariant)),
                   Make_Pragma_Argument_Association (Loc,
                     Expression => Exp));
 
@@ -3705,8 +3723,7 @@  package body Sem_Ch13 is
                Append_To (Stmts,
                  Make_Pragma (Loc,
                    Pragma_Identifier            =>
-                     Make_Identifier (Loc,
-                       Chars => Name_Check),
+                     Make_Identifier (Loc, Chars => Name_Check),
                    Pragma_Argument_Associations => Assoc));
 
                --  If Inherited case and option enabled, output info msg. Note
@@ -3731,6 +3748,7 @@  package body Sem_Ch13 is
       Stmts := No_List;
       PDecl := Empty;
       PBody := Empty;
+      Set_Etype (Object_Entity, Typ);
 
       --  Add invariants for the current type
 
@@ -3766,7 +3784,6 @@  package body Sem_Ch13 is
 
          --  Build procedure declaration
 
-         pragma Assert (Has_Invariants (Typ));
          SId :=
            Make_Defining_Identifier (Loc,
              Chars => New_External_Name (Chars (Typ), "Invariant"));
@@ -3778,15 +3795,10 @@  package body Sem_Ch13 is
              Defining_Unit_Name       => SId,
              Parameter_Specifications => New_List (
                Make_Parameter_Specification (Loc,
-                 Defining_Identifier =>
-                   Make_Defining_Identifier (Loc,
-                     Chars => Object_Name),
-                 Parameter_Type =>
-                   New_Occurrence_Of (Typ, Loc))));
+                 Defining_Identifier => Object_Entity,
+                 Parameter_Type      => New_Occurrence_Of (Typ, Loc))));
 
-         PDecl :=
-           Make_Subprogram_Declaration (Loc,
-             Specification => Spec);
+         PDecl := Make_Subprogram_Declaration (Loc, Specification => Spec);
 
          --  Build procedure body
 
@@ -3812,6 +3824,27 @@  package body Sem_Ch13 is
              Handled_Statement_Sequence =>
                Make_Handled_Sequence_Of_Statements (Loc,
                  Statements => Stmts));
+
+         --  Insert procedure declaration and spec at the appropriate points.
+         --  Skip this if there are no private declarations (that's an error
+         --  that will be diagnosed elsewhere, and there is no point in having
+         --  an invariant procedure set if the full declaration is missing).
+
+         if Present (Private_Decls) then
+
+            --  The spec goes at the end of visible declarations, but they have
+            --  already been analyzed, so we need to explicitly do the analyze.
+
+            Append_To (Visible_Decls, PDecl);
+            Analyze (PDecl);
+
+            --  The body goes at the end of the private declarations, which we
+            --  have not analyzed yet, so we do not need to perform an explicit
+            --  analyze call. We skip this if there are no private declarations
+            --  (this is an error that will be caught elsewhere);
+
+            Append_To (Private_Decls, PBody);
+         end if;
       end if;
    end Build_Invariant_Procedure;
 
Index: sem_ch13.ads
===================================================================
--- sem_ch13.ads	(revision 165935)
+++ sem_ch13.ads	(working copy)
@@ -52,17 +52,16 @@  package Sem_Ch13 is
    --  order is specified and there is at least one component clause. Adjusts
    --  component positions according to either Ada 95 or Ada 2005 (AI-133).
 
-   procedure Build_Invariant_Procedure
-     (Typ   : Entity_Id;
-      PDecl : out Node_Id;
-      PBody : out Node_Id);
-   --  If Typ has Invariants (indicated by Has_Invariants being set for Typ,
-   --  indicating the presence of pragma Invariant entries on the rep chain,
-   --  note that Invariant aspects are converted to pragma Invariant), then
-   --  this procedure builds the spec and body for the corresponding Invariant
-   --  procedure, returning themn in PDecl and PBody. Invariant_Procedure is
-   --  set for Typ. In some error situations no procedure is built, in which
-   --  case PDecl/PBody are empty on return.
+   procedure Build_Invariant_Procedure (Typ : Entity_Id; N : Node_Id);
+   --  Typ is a private type with invariants (indicated by Has_Invariants being
+   --  set for Typ, indicating the presence of pragma Invariant entries on the
+   --  rep chain, note that Invariant aspects have already been converted to
+   --  pragma Invariant), then this procedure builds the spec and body for the
+   --  corresponding Invariant procedure, inserting them at appropriate points
+   --  in the package specification N. Invariant_Procedure is set for Typ. Note
+   --  that this procedure is called at the end of processing the declarations
+   --  in the visible part (i.e. the right point for visibility analysis of
+   --  the invariant expression).
 
    procedure Check_Record_Representation_Clause (N : Node_Id);
    --  This procedure completes the analysis of a record representation clause