diff mbox

[Ada] Reimplementation of type invariants

Message ID 20160620123207.GA29705@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet June 20, 2016, 12:32 p.m. UTC
This patch prevents the insertion of the invariant procedure declaration and
body when the context is a generic unit. This ensures that generated code does
not permiate the template.

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

--  tester.ads

package Tester is
   type Type_Id is
     (Ext_1_Id,
      Ext_1_FV_Id,
      Ext_2_Id,
      Ext_3_Id,
      Ext_4_Id,
      Ext_4_FV_Id,
      Ext_5_Id,
      Ext_6_Id,
      Ext_6_FV_Id,
      Ext_7_Id,
      Ext_8_Id,
      Iface_1_Id,
      Iface_2_Id,
      Iface_3_Id,
      Iface_4_Id,
      Par_1_Id,
      Par_2_FV_Id,
      Par_3_Id,
      Par_4_Id,
      Par_4_FV_Id,
      Prot_1_FV_Id,
      Prot_2_Id,
      Prot_3_Id,
      Prot_3_FV_Id,
      Synch_1_Id,
      Synch_2_Id,
      Tag_1_Id,
      Tag_2_Id,
      Tag_3_Id,
      Tag_4_Id,
      Tag_4_FV_Id,
      Tag_5_Id,
      Tag_6_Id,
      Tag_7_Id,
      Tag_8_Id,
      Tag_9_Id,
      Tag_10_Id,
      Tag_11_Id,
      Tag_12_Id,
      Tag_13_Id,
      Tag_14_Id,
      Tag_15_Id,
      Tag_15_FV_Id,
      Tag_16_Id,
      Tag_17_Id,
      Tag_18_Id,
      Tag_19_Id,
      Tag_20_Id,
      Tag_20_FV_Id,
      Tag_21_Id,
      Tag_22_Id,
      Tag_23_Id,
      Tag_24_Id,
      Tag_24_FV_Id,
      Tag_25_Id,
      Tag_26_Id,
      Tag_27_Id,
      Tag_28_Id,
      Task_1_Id,
      Task_2_Id,
      Task_2_FV_Id,
      Untag_1_Id,
      Untag_2_Id,
      Untag_3_Id,
      Untag_4_Id,
      Untag_5_Id,
      Untag_6_Id,
      Untag_7_Id,
      Untag_8_Id,
      Untag_9_Id);

   type Results is array (Type_Id) of Boolean;

   function Mark (Typ : Type_Id) return Boolean;
   --  Mark the result for a particular type as verified. The function always
   --  returns True.

   procedure Reset_Results;
   --  Reset the internally kept result state

   procedure Test_Results (Test_Id : String; Exp : Results);
   --  Ensure that the internally kept result state agrees with expected
   --  results Exp. Emit an error if this is not the case.
end Tester;

--  tester.adb

with Ada.Text_IO; use Ada.Text_IO;

package body Tester is
   State : Results;

   ----------
   -- Mark --
   ----------

   function Mark (Typ : Type_Id) return Boolean is
   begin
      State (Typ) := True;
      return True;
   end Mark;

   -------------------
   -- Reset_Results --
   -------------------

   procedure Reset_Results is
   begin
      State := (others => False);
   end Reset_Results;

   ------------------
   -- Test_Results --
   ------------------

   procedure Test_Results (Test_Id : String; Exp : Results) is
      Exp_Val   : Boolean;
      Posted    : Boolean := False;
      State_Val : Boolean;

   begin
      for Index in Results'Range loop
         Exp_Val   := Exp (Index);
         State_Val := State (Index);

         if State_Val /= Exp_Val then
            if not Posted then
               Posted := True;
               Put_Line (Test_Id & ": ERROR");
            end if;

            Put_Line ("  Expected: " & Exp_Val'Img & " for " & Index'Img);
            Put_Line ("  Got:      " & State_Val'Img);
         end if;
      end loop;

      if not Posted then
         Put_Line (Test_Id & ": OK");
      end if;
   end Test_Results;
end Tester;

--  gen_invariants.ads

with Tester; use Tester;

generic
package Gen_Invariants is
   type Untag_1 is private
     with Type_Invariant => Mark (Untag_1_Id);

private
   type Untag_1 is null record;

   Obj_1 : Untag_1;
end Gen_Invariants;

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

$ gcc -c -gnata -gnatDG gen_invariants.ads
$ grep "Invariant" gen_invariants.ads.dg

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

2016-06-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch7.adb (Build_Invariant_Procedure_Body):
	Always install the scope of the invariant procedure
	in order to produce better error messages. Do not
	insert the body when the context is a generic unit.
	(Build_Invariant_Procedure_Declaration): Perform minimal
	decoration of the invariant procedure and its formal parameter
	in case they are not analyzed.	Do not insert the declaration
	when the context is a generic unit.
diff mbox

Patch

Index: exp_ch7.adb
===================================================================
--- exp_ch7.adb	(revision 237598)
+++ exp_ch7.adb	(working copy)
@@ -4622,7 +4622,16 @@ 
 
       Set_Ghost_Mode_From_Entity (Work_Typ);
 
+      --  Emulate the environment of the invariant procedure by installing
+      --  its scope and formal parameters. Note that this is not need, but
+      --  having the scope of the invariant procedure installed helps with
+      --  the detection of invariant-related errors.
+
+      Push_Scope (Proc_Id);
+      Install_Formals (Proc_Id);
+
       Obj_Id := First_Formal (Proc_Id);
+      pragma Assert (Present (Obj_Id));
 
       --  The "partial" invariant procedure verifies the invariants of the
       --  partial view only.
@@ -4631,14 +4640,6 @@ 
          pragma Assert (Present (Priv_Typ));
          Freeze_Typ := Priv_Typ;
 
-         --  Emulate the environment of the invariant procedure by installing
-         --  its scope and formal parameters. Note that this is not need, but
-         --  having the scope of the invariant procedure installed helps with
-         --  the detection of invariant-related errors.
-
-         Push_Scope (Proc_Id);
-         Install_Formals (Proc_Id);
-
          Add_Type_Invariants
            (Priv_Typ => Priv_Typ,
             Full_Typ => Empty,
@@ -4646,8 +4647,6 @@ 
             Obj_Id   => Obj_Id,
             Checks   => Stmts);
 
-         End_Scope;
-
       --  Otherwise the "full" invariant procedure verifies the invariants of
       --  the full view, all array or record components, as well as class-wide
       --  invariants inherited from parent types or interfaces. In addition, it
@@ -4744,6 +4743,8 @@ 
          Add_Interface_Invariants (Full_Typ, Obj_Id, Stmts);
       end if;
 
+      End_Scope;
+
       --  At this point there should be at least one invariant check. If this
       --  is not the case, then the invariant-related flags were not properly
       --  set, or there is a missing invariant procedure on one of the array
@@ -4759,6 +4760,12 @@ 
          Stmts := New_List (Make_Null_Statement (Loc));
       end if;
 
+      --  Generate:
+      --    procedure <Work_Typ>[Partial_]Invariant (_object : <Work_Typ>) is
+      --    begin
+      --       <Stmts>
+      --    end <Work_Typ>[Partial_]Invariant;
+
       Proc_Body :=
         Make_Subprogram_Body (Loc,
           Specification                =>
@@ -4769,16 +4776,30 @@ 
                 Statements => Stmts));
       Proc_Body_Id := Defining_Entity (Proc_Body);
 
+      --  Perform minor decoration in case the body is not analyzed
+
       Set_Ekind (Proc_Body_Id, E_Subprogram_Body);
       Set_Etype (Proc_Body_Id, Standard_Void_Type);
-      Set_Scope (Proc_Body_Id, Scope (Typ));
+      Set_Scope (Proc_Body_Id, Current_Scope);
 
       --  Link both spec and body to avoid generating duplicates
 
       Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
       Set_Corresponding_Spec (Proc_Body, Proc_Id);
 
-      Append_Freeze_Action (Freeze_Typ, Proc_Body);
+      --  The body should not be inserted into the tree when the context is a
+      --  generic unit because it is not part of the template. Note that the
+      --  body must still be generated in order to resolve the invariants.
+
+      if Inside_A_Generic then
+         null;
+
+      --  Otherwise the body is part of the freezing actions of the type
+
+      else
+         Append_Freeze_Action (Freeze_Typ, Proc_Body);
+      end if;
+
       Ghost_Mode := Save_Ghost_Mode;
    end Build_Invariant_Procedure_Body;
 
@@ -4794,8 +4815,10 @@ 
 
       Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
 
-      Proc_Id  : Entity_Id;
-      Typ_Decl : Node_Id;
+      Proc_Decl : Node_Id;
+      Proc_Id   : Entity_Id;
+      Proc_Nam  : Name_Id;
+      Typ_Decl  : Node_Id;
 
       CRec_Typ : Entity_Id;
       --  The corresponding record type of Full_Typ
@@ -4869,24 +4892,27 @@ 
       --  procedure.
 
       if Partial_Invariant then
-         Proc_Id :=
-           Make_Defining_Identifier (Loc,
-             Chars =>
-               New_External_Name (Chars (Work_Typ), "Partial_Invariant"));
+         Proc_Nam := New_External_Name (Chars (Work_Typ), "Partial_Invariant");
 
-         Set_Ekind (Proc_Id, E_Procedure);
-         Set_Is_Partial_Invariant_Procedure (Proc_Id);
-         Set_Partial_Invariant_Procedure (Work_Typ, Proc_Id);
-
       --  Otherwise the caller requests the declaration of the "full" invariant
       --  procedure.
 
       else
-         Proc_Id :=
-           Make_Defining_Identifier (Loc,
-             Chars => New_External_Name (Chars (Work_Typ), "Invariant"));
+         Proc_Nam := New_External_Name (Chars (Work_Typ), "Invariant");
+      end if;
 
-         Set_Ekind (Proc_Id, E_Procedure);
+      Proc_Id := Make_Defining_Identifier (Loc, Chars => Proc_Nam);
+
+      --  Perform minor decoration in case the declaration is not analyzed
+
+      Set_Ekind (Proc_Id, E_Procedure);
+      Set_Etype (Proc_Id, Standard_Void_Type);
+      Set_Scope (Proc_Id, Current_Scope);
+
+      if Partial_Invariant then
+         Set_Is_Partial_Invariant_Procedure (Proc_Id);
+         Set_Partial_Invariant_Procedure (Work_Typ, Proc_Id);
+      else
          Set_Is_Invariant_Procedure (Proc_Id);
          Set_Invariant_Procedure (Work_Typ, Proc_Id);
       end if;
@@ -4938,12 +4964,19 @@ 
       --  of the current type instance.
 
       Obj_Id := Make_Defining_Identifier (Loc, Chars => Name_uObject);
+
+      --  Perform minor decoration in case the declaration is not analyzed
+
       Set_Ekind (Obj_Id, E_In_Parameter);
+      Set_Etype (Obj_Id, Work_Typ);
+      Set_Scope (Obj_Id, Proc_Id);
 
+      Set_First_Entity (Proc_Id, Obj_Id);
+
       --  Generate:
       --    procedure <Work_Typ>[Partial_]Invariant (_object : <Work_Typ>);
 
-      Insert_After_And_Analyze (Typ_Decl,
+      Proc_Decl :=
         Make_Subprogram_Declaration (Loc,
           Specification =>
             Make_Procedure_Specification (Loc,
@@ -4952,8 +4985,21 @@ 
                 Make_Parameter_Specification (Loc,
                   Defining_Identifier => Obj_Id,
                   Parameter_Type      =>
-                    New_Occurrence_Of (Work_Typ, Loc))))));
+                    New_Occurrence_Of (Work_Typ, Loc)))));
 
+      --  The declaration should not be inserted into the tree when the context
+      --  is a generic unit because it is not part of the template.
+
+      if Inside_A_Generic then
+         null;
+
+      --  Otherwise insert the declaration
+
+      else
+         pragma Assert (Present (Typ_Decl));
+         Insert_After_And_Analyze (Typ_Decl, Proc_Decl);
+      end if;
+
       Ghost_Mode := Save_Ghost_Mode;
    end Build_Invariant_Procedure_Declaration;