Patchwork [Ada] Handling of Invariant aspect on type completions

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 5, 2012, 2:32 p.m.
Message ID <20121005143220.GA11558@adacore.com>
Download mbox | patch
Permalink /patch/189499/
State New
Headers show

Comments

Arnaud Charlet - Oct. 5, 2012, 2:32 p.m.
This patch fixes the handling of type invariants when they are specified on
the completion of a private type, and when public expression functions return
a type with invariants.

Running the following:

   gnatmake -q -gnat12a main
   main

must yield:

   OK

---
with Ada.Assertions; use Ada.Assertions;
with Text_IO; use Text_IO;
with R; use R;
procedure Main is
    X : T;
begin
    X := Zero;
    Put_Line ("Invariant violated");
exception
   when Assertion_Error => Put_Line ("OK");
end Main;
---
package R is
    type T is private;;
    function Non_Null (X : T) return Boolean;
    function Zero return T;
private
    type T is new Integer with Type_Invariant => T /= 0;
    function Non_Null (X : T) return Boolean is (X /= 0);
    function Zero return T is (0);
end R;

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

2012-10-05  Ed Schonberg  <schonberg@adacore.com>

	* einfo.adb (Set_Invariant_Procedure, Set_Predicate_Function):
	chain properly subprograms on Subprograms_For_Type list.
	* sem_ch13.ads; (Build_Invariant_Procedure_Declaration): new
	procedure, to create declaration for invariant procedure
	independently of the construction of the body, so that it can
	be called within expression functions.
	* sem_ch13.adb (Build_Invariant_Procedure): code cleanup. The
	declaration may already have been generated at the point an
	explicit invariant aspect is encountered.
	* sem_prag.adb; (Analyze_Pragma, case Invariant): create declaration
	for invariant procedure.
	* sem_ch7.adb (Analyze_Package_Specification): clean up call to
	build invariant procedure.
	(Preserve_Full_Attributes): propagate information about invariants
	if they appear on a completion,

Patch

Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb	(revision 192066)
+++ sem_ch7.adb	(working copy)
@@ -28,6 +28,7 @@ 
 --  handling of private and full declarations, and the construction of dispatch
 --  tables for tagged types.
 
+with Aspects;  use Aspects;
 with Atree;    use Atree;
 with Debug;    use Debug;
 with Einfo;    use Einfo;
@@ -1387,7 +1388,21 @@ 
            and then Nkind (Parent (E)) = N_Full_Type_Declaration
            and then Has_Aspects (Parent (E))
          then
-            Build_Invariant_Procedure (E, N);
+            declare
+               ASN : Node_Id;
+            begin
+               ASN := First (Aspect_Specifications (Parent (E)));
+               while Present (ASN) loop
+                  if Chars (Identifier (ASN)) = Name_Invariant
+                    or else Chars (Identifier (ASN)) = Name_Type_Invariant
+                  then
+                     Build_Invariant_Procedure (E, N);
+                     exit;
+                  end if;
+
+                  Next (ASN);
+               end loop;
+            end;
          end if;
 
          Next_Entity (E);
@@ -2143,6 +2158,14 @@ 
 
          Set_Freeze_Node (Priv, Freeze_Node (Full));
 
+         --  Propagate information of type invariants, which may be specified
+         --  for the full view.
+
+         if Has_Invariants (Full) and not Has_Invariants (Priv) then
+            Set_Has_Invariants (Priv);
+            Set_Subprograms_For_Type (Priv, Subprograms_For_Type (Full));
+         end if;
+
          if Is_Tagged_Type (Priv)
            and then Is_Tagged_Type (Full)
            and then not Error_Posted (Full)
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 192066)
+++ einfo.adb	(working copy)
@@ -7113,6 +7113,7 @@ 
 
       S := Subprograms_For_Type (Id);
       Set_Subprograms_For_Type (Id, V);
+      Set_Subprograms_For_Type (V, S);
 
       while Present (S) loop
          if Has_Invariants (S) then
@@ -7121,8 +7122,6 @@ 
             S := Subprograms_For_Type (S);
          end if;
       end loop;
-
-      Set_Subprograms_For_Type (Id, V);
    end Set_Invariant_Procedure;
 
    ----------------------------
@@ -7137,6 +7136,7 @@ 
 
       S := Subprograms_For_Type (Id);
       Set_Subprograms_For_Type (Id, V);
+      Set_Subprograms_For_Type (V, S);
 
       while Present (S) loop
          if Has_Predicates (S) then
@@ -7145,8 +7145,6 @@ 
             S := Subprograms_For_Type (S);
          end if;
       end loop;
-
-      Set_Subprograms_For_Type (Id, V);
    end Set_Predicate_Function;
 
    -----------------
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 192124)
+++ sem_prag.adb	(working copy)
@@ -10329,6 +10329,7 @@ 
          when Pragma_Invariant => Invariant : declare
             Type_Id : Node_Id;
             Typ     : Entity_Id;
+            PDecl   : Node_Id;
 
             Discard : Boolean;
             pragma Unreferenced (Discard);
@@ -10380,8 +10381,13 @@ 
 
             --  Note that the type has at least one invariant, and also that
             --  it has inheritable invariants if we have Invariant'Class.
+            --  Build the corresponding invariant procedure declaration, so
+            --  that calls to it can be generated before the body is built
+            --  (for example wihin an expression function).
 
-            Set_Has_Invariants (Typ);
+            PDecl := Build_Invariant_Procedure_Declaration (Typ);
+            Insert_After (N, PDecl);
+            Analyze (PDecl);
 
             if Class_Present (N) then
                Set_Has_Inheritable_Invariants (Typ);
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 192066)
+++ sem_ch13.adb	(working copy)
@@ -4902,6 +4902,48 @@ 
       end if;
    end Analyze_Record_Representation_Clause;
 
+   -------------------------------------------
+   -- Build_Invariant_Procedure_Declaration --
+   -------------------------------------------
+
+   function Build_Invariant_Procedure_Declaration
+     (Typ : Entity_Id) return Node_Id
+   is
+      Loc           : constant Source_Ptr := Sloc (Typ);
+      Object_Entity : constant Entity_Id :=
+        Make_Defining_Identifier (Loc, New_Internal_Name ('I'));
+      Spec          : Node_Id;
+      SId           : Entity_Id;
+
+   begin
+      Set_Etype (Object_Entity, Typ);
+
+      --  Check for duplicate definiations.
+
+      if Has_Invariants (Typ)
+        and then Present (Invariant_Procedure (Typ))
+      then
+         return Empty;
+      end if;
+
+      SId := Make_Defining_Identifier (Loc,
+         Chars => New_External_Name (Chars (Typ), "Invariant"));
+      Set_Has_Invariants (SId);
+      Set_Has_Invariants (Typ);
+      Set_Ekind (SId, E_Procedure);
+      Set_Invariant_Procedure (Typ, SId);
+
+      Spec :=
+        Make_Procedure_Specification (Loc,
+          Defining_Unit_Name       => SId,
+          Parameter_Specifications => New_List (
+            Make_Parameter_Specification (Loc,
+              Defining_Identifier => Object_Entity,
+              Parameter_Type      => New_Occurrence_Of (Typ, Loc))));
+
+      return Make_Subprogram_Declaration (Loc, Specification => Spec);
+   end Build_Invariant_Procedure_Declaration;
+
    -------------------------------
    -- Build_Invariant_Procedure --
    -------------------------------
@@ -4936,12 +4978,11 @@ 
       --  "inherited" to the exception message and generating an informational
       --  message about the inheritance of an invariant.
 
-      Object_Name : constant Name_Id := New_Internal_Name ('I');
+      Object_Name : Name_Id;
       --  Name for argument of invariant procedure
 
-      Object_Entity : constant Node_Id :=
-                        Make_Defining_Identifier (Loc, Object_Name);
-      --  The procedure declaration entity for the argument
+      Object_Entity : Node_Id;
+      --  The entity of the formal for the procedure
 
       --------------------
       -- Add_Invariants --
@@ -5140,8 +5181,30 @@ 
       Stmts := No_List;
       PDecl := Empty;
       PBody := Empty;
-      Set_Etype (Object_Entity, Typ);
+      SId   := Empty;
 
+      --  If the aspect specification exists for some view of the type, the
+      --  declaration for the procedure has been created.
+
+      if Has_Invariants (Typ) then
+         SId := Invariant_Procedure (Typ);
+      end if;
+
+      if Present (SId) then
+         PDecl := Unit_Declaration_Node (SId);
+
+      else
+         PDecl := Build_Invariant_Procedure_Declaration (Typ);
+      end if;
+
+      --  Recover formal of procedure, for use in the calls to invariant
+      --  functions (including inherited ones).
+
+      Object_Entity :=
+        Defining_Identifier
+          (First (Parameter_Specifications (Specification (PDecl))));
+      Object_Name := Chars (Object_Entity);
+
       --  Add invariants for the current type
 
       Add_Invariants (Typ, Inherit => False);
@@ -5174,39 +5237,8 @@ 
 
       if Stmts /= No_List then
 
-         --  Build procedure declaration
+         Spec  := Copy_Separate_Tree (Specification (PDecl));
 
-         SId :=
-           Make_Defining_Identifier (Loc,
-             Chars => New_External_Name (Chars (Typ), "Invariant"));
-         Set_Has_Invariants (SId);
-         Set_Invariant_Procedure (Typ, SId);
-
-         Spec :=
-           Make_Procedure_Specification (Loc,
-             Defining_Unit_Name       => SId,
-             Parameter_Specifications => New_List (
-               Make_Parameter_Specification (Loc,
-                 Defining_Identifier => Object_Entity,
-                 Parameter_Type      => New_Occurrence_Of (Typ, Loc))));
-
-         PDecl := Make_Subprogram_Declaration (Loc, Specification => Spec);
-
-         --  Build procedure body
-
-         SId :=
-           Make_Defining_Identifier (Loc,
-             Chars => New_External_Name (Chars (Typ), "Invariant"));
-
-         Spec :=
-           Make_Procedure_Specification (Loc,
-             Defining_Unit_Name       => SId,
-             Parameter_Specifications => New_List (
-               Make_Parameter_Specification (Loc,
-                 Defining_Identifier =>
-                   Make_Defining_Identifier (Loc, Object_Name),
-                 Parameter_Type => New_Occurrence_Of (Typ, Loc))));
-
          PBody :=
            Make_Subprogram_Body (Loc,
              Specification              => Spec,
@@ -5216,14 +5248,18 @@ 
                  Statements => Stmts));
 
          --  Insert procedure declaration and spec at the appropriate points.
+         --  If declaration is already analyzed, it was processed by the
+         --  generated pragma.
 
          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);
+            if not Analyzed (PDecl) then
+               Append_To (Visible_Decls, PDecl);
+               Analyze (PDecl);
+            end if;
 
             --  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
@@ -5523,6 +5559,7 @@ 
            Make_Defining_Identifier (Loc,
              Chars => New_External_Name (Chars (Typ), "Predicate"));
          Set_Has_Predicates (SId);
+         Set_Ekind (SId, E_Function);
          Set_Predicate_Function (Typ, SId);
 
          --  The predicate function is shared between views of a type.
Index: sem_ch13.ads
===================================================================
--- sem_ch13.ads	(revision 192066)
+++ sem_ch13.ads	(working copy)
@@ -46,6 +46,14 @@ 
    --  order is specified and there is at least one component clause. Adjusts
    --  component positions according to either Ada 95 or Ada 2005 (AI-133).
 
+   function Build_Invariant_Procedure_Declaration
+     (Typ : Entity_Id) return Node_Id;
+   --  If a type declaration has a specified invariant aspect, build the
+   --  declaration for the procedure at once, so that calls to it can be
+   --  generated before the body of the invariant procedure is built. This
+   --  is needed in the presence of public expression functions that return
+   --  the type in question.
+
    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