diff mbox

[Ada] Issue with SPARK aspects and generics

Message ID 20140220134838.GA30666@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Feb. 20, 2014, 1:48 p.m. UTC 
This patch corrects the propagation of various SPARK aspects from a generic
template to an instance.

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

--  values.ads

package Values is
   In_1 : Integer := 1234;
end Values;

--  gen.ads

with Values; use Values;

generic
package Gen
  with Abstract_State    =>  State,
       Initializes       =>  Out_1,
       Initial_Condition => (Out_1 = 5678)
is
   Out_1 : Integer := 5678;

   procedure Proc (In_2 : Integer; Out_2 : out Integer)
     with Global  => (Input  => In_1,
                      In_Out => State,
                      Output => Out_1),
          Depends => ((Out_1, Out_2, State) => (In_1, In_2, State));
end Gen;

--  gen.adb

package body Gen
  with Refined_State => (State => (In_3, Out_3))
is
   In_3  : Integer := 1;
   Out_3 : Integer := 2;

   procedure Proc (In_2 : Integer; Out_2 : out Integer)
     with Refined_Global  => (Input  => (In_1,  In_3),
                              Output => (Out_1, Out_3)),
          Refined_Depends => ((Out_1, Out_2, Out_3) => (In_1, In_2, In_3))
   is begin null; end Proc;
end Gen;

--  inst.ads

with Gen;

package Inst is new Gen;

-----------------
-- Compilation --
-----------------

$ gcc -c inst.ads

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

2014-02-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb (Exchange_Aspects): New routine.
	* aspects.ads (Exchange_Aspects): New routine.
	* atree.adb (Rewrite): Do not check whether the save node has
	aspects as it never will, instead check the node about to be clobbered.
	* einfo.adb (Write_Field25_Name): Abstract_States can appear in
	entities of generic packages.
	* sem_ch6.adb (Analyze_Expression_Function): Fix the parent
	pointer of an aspect specification list after rewriting takes place.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Swap the aspect
	specifications of the generic template and the copy used for analysis.
	* sem_ch12.adb (Analyze_Generic_Package_Declaration): Swap
	the aspect specifications of the generic template and the
	copy used for analysis.
	(Analyze_Package_Instantiation): Propagate the aspect specifications
	from the generic template to the instantiation.
	(Build_Instance_Compilation_Unit_Nodes): Propagate the aspect
	specifications from the generic template to the instantiation.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Handle aspects
	Abstract_State, Initializes and Initial_Condition when they
	apply to a package instantiation.
diff mbox

Patch

Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb	(revision 207879)
+++ sem_ch7.adb	(working copy)
@@ -327,6 +327,11 @@ 
          New_N := Copy_Generic_Node (N, Empty, Instantiating => False);
          Rewrite (N, New_N);
 
+         --  Once the contents of the generic copy and the template are
+         --  swapped, do the same for their respective aspect specifications.
+
+         Exchange_Aspects (N, New_N);
+
          --  Update Body_Id to point to the copied node for the remainder of
          --  the processing.
 
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 207879)
+++ einfo.adb	(working copy)
@@ -9290,7 +9290,8 @@ 
    procedure Write_Field25_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
-         when E_Package                                    =>
+         when E_Generic_Package                            |
+              E_Package                                    =>
             Write_Str ("Abstract_States");
 
          when E_Variable                                   =>
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb	(revision 207942)
+++ sem_ch12.adb	(working copy)
@@ -3019,6 +3019,11 @@ 
       New_N := Copy_Generic_Node (N, Empty, Instantiating => False);
       Set_Parent_Spec (New_N, Save_Parent);
       Rewrite (N, New_N);
+
+      --  Once the contents of the generic copy and the template are swapped,
+      --  do the same for their respective aspect specifications.
+
+      Exchange_Aspects (N, New_N);
       Id := Defining_Entity (N);
       Generate_Definition (Id);
 
@@ -3088,7 +3093,6 @@ 
             Check_References (Id);
          end if;
       end if;
-
    end Analyze_Generic_Package_Declaration;
 
    --------------------------------------------
@@ -3598,7 +3602,7 @@ 
            Make_Package_Renaming_Declaration (Loc,
              Defining_Unit_Name =>
                Make_Defining_Identifier (Loc, Chars (Gen_Unit)),
-             Name => New_Occurrence_Of (Act_Decl_Id, Loc));
+             Name               => New_Occurrence_Of (Act_Decl_Id, Loc));
 
          Append (Unit_Renaming, Renaming_List);
 
@@ -3616,6 +3620,14 @@ 
            Make_Package_Declaration (Loc,
              Specification => Act_Spec);
 
+         --  Propagate the aspect specifications from the package declaration
+         --  template to the instantiated version of the package declaration.
+
+         if Has_Aspects (Act_Tree) then
+            Set_Aspect_Specifications (Act_Decl,
+              New_Copy_List_Tree (Aspect_Specifications (Act_Tree)));
+         end if;
+
          --  Save the instantiation node, for subsequent instantiation of the
          --  body, if there is one and we are generating code for the current
          --  unit. Mark unit as having a body (avoids premature error message).
@@ -5007,7 +5019,7 @@ 
           Unit           => Act_Decl,
           Aux_Decls_Node => Make_Compilation_Unit_Aux (Sloc (N)));
 
-      Set_Parent_Spec   (Act_Decl, Parent_Spec (N));
+      Set_Parent_Spec (Act_Decl, Parent_Spec (N));
 
       --  The new compilation unit is linked to its body, but both share the
       --  same file, so we do not set Body_Required on the new unit so as not
@@ -5018,6 +5030,15 @@ 
       --  compilation unit of the instance, since this is the main unit.
 
       Rewrite (N, Act_Body);
+
+      --  Propagate the aspect specifications from the package body template to
+      --  the instantiated version of the package body.
+
+      if Has_Aspects (Act_Body) then
+         Set_Aspect_Specifications
+           (N, New_Copy_List_Tree (Aspect_Specifications (Act_Body)));
+      end if;
+
       Body_Cunit := Parent (N);
 
       --  The two compilation unit nodes are linked by the Library_Unit field
Index: aspects.adb
===================================================================
--- aspects.adb	(revision 207881)
+++ aspects.adb	(working copy)
@@ -174,6 +174,31 @@ 
       return True;
    end Aspects_On_Body_Or_Stub_OK;
 
+   ----------------------
+   -- Exchange_Aspects --
+   ----------------------
+
+   procedure Exchange_Aspects (N1 : Node_Id; N2 : Node_Id) is
+   begin
+      pragma Assert
+        (Permits_Aspect_Specifications (N1)
+           and then Permits_Aspect_Specifications (N2));
+
+      --  Perform the exchange only when both nodes have lists to be swapped
+
+      if Has_Aspects (N1) and then Has_Aspects (N2) then
+         declare
+            L1 : constant List_Id := Aspect_Specifications (N1);
+            L2 : constant List_Id := Aspect_Specifications (N2);
+         begin
+            Set_Parent (L1, N2);
+            Set_Parent (L2, N1);
+            Aspect_Specifications_Hash_Table.Set (N1, L2);
+            Aspect_Specifications_Hash_Table.Set (N2, L1);
+         end;
+      end if;
+   end Exchange_Aspects;
+
    -----------------
    -- Find_Aspect --
    -----------------
Index: aspects.ads
===================================================================
--- aspects.ads	(revision 207881)
+++ aspects.ads	(working copy)
@@ -786,6 +786,11 @@ 
    --  N denotes a body [stub] with aspects. Determine whether all aspects of N
    --  are allowed to appear on a body [stub].
 
+   procedure Exchange_Aspects (N1 : Node_Id; N2 : Node_Id);
+   --  Exchange the aspect specifications of two nodes. If either node lacks an
+   --  aspect specification list, the routine has no effect. It is assumed that
+   --  both nodes can support aspects.
+
    function Find_Aspect (Id : Entity_Id; A : Aspect_Id) return Node_Id;
    --  Find the aspect specification of aspect A associated with entity I.
    --  Return Empty if Id does not have the requested aspect.
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 207942)
+++ sem_ch6.adb	(working copy)
@@ -374,6 +374,13 @@ 
          Generate_Reference (Prev, Defining_Entity (N), 'b', Force => True);
          Rewrite (N, New_Body);
 
+         --  Correct the parent pointer of the aspect specification list to
+         --  reference the rewritten node.
+
+         if Has_Aspects (N) then
+            Set_Parent (Aspect_Specifications (N), N);
+         end if;
+
          --  Propagate any pragmas that apply to the expression function to the
          --  proper body when the expression function acts as a completion.
          --  Aspects are automatically transfered because of node rewriting.
@@ -429,6 +436,14 @@ 
            Make_Subprogram_Declaration (Loc, Specification => Spec);
 
          Rewrite (N, New_Decl);
+
+         --  Correct the parent pointer of the aspect specification list to
+         --  reference the rewritten node.
+
+         if Has_Aspects (N) then
+            Set_Parent (Aspect_Specifications (N), N);
+         end if;
+
          Analyze (N);
          Set_Is_Inlined (Defining_Entity (New_Decl));
 
Index: atree.adb
===================================================================
--- atree.adb	(revision 207879)
+++ atree.adb	(working copy)
@@ -1870,8 +1870,7 @@ 
          --  Both the old and new copies of the node will share the same list
          --  of aspect specifications if aspect specifications are present.
 
-         if Has_Aspects (Sav_Node) then
-            Set_Has_Aspects (Sav_Node, False);
+         if Old_Has_Aspects then
             Set_Aspect_Specifications
               (Sav_Node, Aspect_Specifications (Old_Node));
          end if;
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 207942)
+++ sem_ch13.adb	(working copy)
@@ -2008,13 +2008,22 @@ 
                --  immediately.
 
                when Aspect_Abstract_State => Abstract_State : declare
-                  Decls : List_Id;
+                  Context : Node_Id := N;
+                  Decls   : List_Id;
 
                begin
-                  if Nkind_In (N, N_Generic_Package_Declaration,
-                                  N_Package_Declaration)
+                  --  When aspect Abstract_State appears on a generic package,
+                  --  it is propageted to the package instance. The context in
+                  --  this case is the instance spec.
+
+                  if Nkind (Context) = N_Package_Instantiation then
+                     Context := Instance_Spec (Context);
+                  end if;
+
+                  if Nkind_In (Context, N_Generic_Package_Declaration,
+                                        N_Package_Declaration)
                   then
-                     Decls := Visible_Declarations (Specification (N));
+                     Decls := Visible_Declarations (Specification (Context));
 
                      Make_Aitem_Pragma
                        (Pragma_Argument_Associations => New_List (
@@ -2025,7 +2034,7 @@ 
 
                      if No (Decls) then
                         Decls := New_List;
-                        Set_Visible_Declarations (N, Decls);
+                        Set_Visible_Declarations (Context, Decls);
                      end if;
 
                      Prepend_To (Decls, Aitem);
@@ -2084,13 +2093,22 @@ 
                --  it must be evaluated at the end of the said declarations.
 
                when Aspect_Initial_Condition => Initial_Condition : declare
-                  Decls : List_Id;
+                  Context : Node_Id := N;
+                  Decls   : List_Id;
 
                begin
-                  if Nkind_In (N, N_Generic_Package_Declaration,
-                                  N_Package_Declaration)
+                  --  When aspect Abstract_State appears on a generic package,
+                  --  it is propageted to the package instance. The context in
+                  --  this case is the instance spec.
+
+                  if Nkind (Context) = N_Package_Instantiation then
+                     Context := Instance_Spec (Context);
+                  end if;
+
+                  if Nkind_In (Context, N_Generic_Package_Declaration,
+                                        N_Package_Declaration)
                   then
-                     Decls := Visible_Declarations (Specification (N));
+                     Decls := Visible_Declarations (Specification (Context));
 
                      Make_Aitem_Pragma
                        (Pragma_Argument_Associations => New_List (
@@ -2104,7 +2122,7 @@ 
 
                      if No (Decls) then
                         Decls := New_List;
-                        Set_Visible_Declarations (N, Decls);
+                        Set_Visible_Declarations (Context, Decls);
                      end if;
 
                      Prepend_To (Decls, Aitem);
@@ -2125,13 +2143,22 @@ 
                --  said declarations.
 
                when Aspect_Initializes => Initializes : declare
-                  Decls : List_Id;
+                  Context : Node_Id := N;
+                  Decls   : List_Id;
 
                begin
-                  if Nkind_In (N, N_Generic_Package_Declaration,
-                                  N_Package_Declaration)
+                  --  When aspect Abstract_State appears on a generic package,
+                  --  it is propageted to the package instance. The context in
+                  --  this case is the instance spec.
+
+                  if Nkind (Context) = N_Package_Instantiation then
+                     Context := Instance_Spec (Context);
+                  end if;
+
+                  if Nkind_In (Context, N_Generic_Package_Declaration,
+                                        N_Package_Declaration)
                   then
-                     Decls := Visible_Declarations (Specification (N));
+                     Decls := Visible_Declarations (Specification (Context));
 
                      Make_Aitem_Pragma
                        (Pragma_Argument_Associations => New_List (
@@ -2144,7 +2171,7 @@ 
 
                      if No (Decls) then
                         Decls := New_List;
-                        Set_Visible_Declarations (N, Decls);
+                        Set_Visible_Declarations (Context, Decls);
                      end if;
 
                      Prepend_To (Decls, Aitem);