[Ada] Pragma Default_Initial_Condition and tagged types

This patch reimplements pragma Default_Initial_Condition. When the pragma is
inherited from a parent tagged type, the assertion expression of the pragma is
subject to class-wide pre/postcondition-like semantics. This means that any
function calls to primitives of the parent type are replaced by calls to the
overriding primitives of the derived type.

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

--  dic_aspects.ads

package DIC_Aspects is

   ------------------------------------
   --  Derivation without overriding --
   ------------------------------------

   type Par_1 is tagged private
     with Default_Initial_Condition => A (Par_1);

   function A (Obj : Par_1) return Boolean;

   type Deriv_1 is new Par_1 with private;
   --  DIC calls: A (Par_1)

   --------------------------------
   -- Derivation with overriding --
   --------------------------------

   type Par_2 is tagged private
     with Default_Initial_Condition => B (Par_2);

   function B (Obj : Par_2) return Boolean;

   type Deriv_2 is new Par_2 with private;
   --  DIC calls: B (Deriv_2)

   function B (Obj : Deriv_2) return Boolean;

   ------------------------------------
   -- Derivation with DIC overriding --
   ------------------------------------

   type Par_3 is tagged private
     with Default_Initial_Condition => C (Par_3);

   function C (Obj : Par_3) return Boolean;

   type Deriv_3 is new Par_3 with private
     with Default_Initial_Condition => D (Deriv_3);
   --  DIC calls: D (Deriv_3)

   function D (Obj : Deriv_3) return Boolean;

   ------------------------------------------------
   -- Derivation with overriding, DIC overriding --
   ------------------------------------------------

   type Par_4 is tagged private
     with Default_Initial_Condition => E (Par_4);

   function E (Obj : Par_4) return Boolean;

   type Deriv_4 is new Par_4 with private
     with Default_Initial_Condition => E (Deriv_4);
   --  DIC calls: E (Deriv_4)

   function E (Obj : Deriv_4) return Boolean;

   ----------------------------------------
   -- Derivation with partial overriding --
   ----------------------------------------

   type Par_5 is tagged private
     with Default_Initial_Condition => F (Par_5) and G (Par_5);

   function F (Obj : Par_5) return Boolean;
   function G (Obj : Par_5) return Boolean;

   type Deriv_5 is new Par_5 with private;
   --  DIC calls: F (Deriv_5), G (Par_5)

   function F (Obj : Deriv_5) return Boolean;

   -------------------------------------------
   --  Hidden derivation without overriding --
   -------------------------------------------

   type Par_6 is tagged private
     with Default_Initial_Condition => H (Par_6);

   function H (Obj : Par_6) return Boolean;

   type Deriv_6 is tagged private;
   --  DIC calls: H (Par_6)

   ---------------------------------------
   -- Hidden derivation with overriding --
   ---------------------------------------

   type Par_7 is tagged private
     with Default_Initial_Condition => I (Par_7);

   function I (Obj : Par_7) return Boolean;

   type Deriv_7 is tagged private;
   --  DIC calls: I (Deriv_7)

   -----------------------------------------------
   -- Hidden derivation with partial overriding --
   -----------------------------------------------

   type Par_8 is tagged private
     with Default_Initial_Condition => J (Par_8) and K (Par_8) and L (Par_8);

   function J (Obj : Par_8) return Boolean;
   function K (Obj : Par_8) return Boolean;
   function L (Obj : Par_8) return Boolean;

   type Deriv_8 is tagged private;
   --  DIC calls: J (Deriv_8), K (Deriv_8), L (Par_8)

   function J (Obj : Deriv_8) return Boolean;

   -----------------------------------
   -- Long chain without overriding --
   -----------------------------------

   type Deriv_9 is new Deriv_1 with private;
   --  DIC calls: A (Par_1)

   --------------------------------
   -- Long chain with overriding --
   --------------------------------

   type Deriv_10 is new Deriv_2 with private;
   --  DIC calls: B (Deriv_2)

   -----------
   -- Mix 1 --
   -----------

   type Typ_1 is tagged private
     with Default_Initial_Condition =>
            M (Typ_1) and N (Typ_1) and O (Typ_1) and P (Typ_1) and Q (Typ_1);

   function M (Obj : Typ_1) return Boolean;
   function N (Obj : Typ_1) return Boolean;
   function O (Obj : Typ_1) return Boolean;
   function P (Obj : Typ_1) return Boolean;
   function Q (Obj : Typ_1) return Boolean;

   type Typ_2 is new Typ_1 with private;
   --  DIC calls: M (Typ_2), N (Typ_2), O (Typ_1), P (Typ_1), Q (Typ_1)

   function M (Obj : Typ_2) return Boolean;

   type Typ_3 is new Typ_2 with private;
   --  DIC calls: M (Typ_2), N (Typ_2), O (Typ_3), P (Typ_3), Q (Typ_1)

   function O (Obj : Typ_3) return Boolean;

private
   type Par_1 is tagged null record;
   type Par_2 is tagged null record;
   type Par_3 is tagged null record;
   type Par_4 is tagged null record;
   type Par_5 is tagged null record;
   type Par_6 is tagged null record;
   type Par_7 is tagged null record;
   type Par_8 is tagged null record;

   type Deriv_1 is new Par_1 with null record;
   type Deriv_2 is new Par_2 with null record;
   type Deriv_3 is new Par_3 with null record;
   type Deriv_4 is new Par_4 with null record;
   type Deriv_5 is new Par_5 with null record;

   type Deriv_6 is new Par_6 with null record;
   type Deriv_7 is new Par_7 with null record;

   function I (Obj : Deriv_7) return Boolean;

   type Deriv_8 is new Par_8 with null record;

   function K (Obj : Deriv_8) return Boolean;

   type Deriv_9 is new Deriv_1 with null record;
   type Deriv_10 is new Deriv_2 with null record;

   type Typ_1 is tagged null record;
   type Typ_2 is new Typ_1 with null record;

   function N (Obj : Typ_2) return Boolean;

   type Typ_3 is new Typ_2 with null record;

   function P (Obj : Typ_3) return Boolean;
end DIC_Aspects;

--  dic_aspects.adb

with Tester; use Tester;

package body DIC_Aspects is
   function A (Obj : Par_1) return Boolean is
   begin
      Mark (Par_1_Id);
      return True;
   end A;

   function B (Obj : Par_2) return Boolean is
   begin
      Mark (Par_2_Id);
      return True;
   end B;

   function B (Obj : Deriv_2) return Boolean is
   begin
      Mark (Deriv_2_Id);
      return True;
   end B;

   function C (Obj : Par_3) return Boolean is
   begin
      Mark (Par_3_Id);
      return True;
   end C;

   function D (Obj : Deriv_3) return Boolean is
   begin
      Mark (Deriv_3_Id);
      return True;
   end D;

   function E (Obj : Par_4) return Boolean is
   begin
      Mark (Par_4_Id);
      return True;
   end E;

   function E (Obj : Deriv_4) return Boolean is
   begin
      Mark (Deriv_4_Id);
      return True;
   end E;

   function F (Obj : Par_5) return Boolean is
   begin
      Mark (Par_5_Id);
      return True;
   end F;

   function F (Obj : Deriv_5) return Boolean is
   begin
      Mark (Deriv_5_Id);
      return True;
   end F;

   function G (Obj : Par_5) return Boolean is
   begin
      Mark (Par_5_Id);
      return True;
   end G;

   function H (Obj : Par_6) return Boolean is
   begin
      Mark (Par_6_Id);
      return True;
   end H;

   function I (Obj : Par_7) return Boolean is
   begin
      Mark (Par_7_Id);
      return True;
   end I;

   function I (Obj : Deriv_7) return Boolean is
   begin
      Mark (Deriv_7_Id);
      return True;
   end I;

   function J (Obj : Par_8) return Boolean is
   begin
      Mark (Par_8_Id);
      return True;
   end J;

   function J (Obj : Deriv_8) return Boolean is
   begin
      Mark (Deriv_8_Id);
      return True;
   end J;

   function K (Obj : Par_8) return Boolean is
   begin
      Mark (Par_8_Id);
      return True;
   end K;

   function K (Obj : Deriv_8) return Boolean is
   begin
      Mark (Deriv_8_Id);
      return True;
   end K;

   function L (Obj : Par_8) return Boolean is
   begin
      Mark (Par_8_Id);
      return True;
   end L;

   function M (Obj : Typ_1) return Boolean is
   begin
      Mark (Typ_1_Id);
      return True;
   end M;

   function M (Obj : Typ_2) return Boolean is
   begin
      Mark (Typ_2_Id);
      return True;
   end M;

   function N (Obj : Typ_1) return Boolean is
   begin
      Mark (Typ_1_Id);
      return True;
   end N;

   function N (Obj : Typ_2) return Boolean is
   begin
      Mark (Typ_2_Id);
      return True;
   end N;

   function O (Obj : Typ_1) return Boolean is
   begin
      Mark (Typ_1_Id);
      return True;
   end O;

   function O (Obj : Typ_3) return Boolean is
   begin
      Mark (Typ_3_Id);
      return True;
   end O;

   function P (Obj : Typ_1) return Boolean is
   begin
      Mark (Typ_1_Id);
      return True;
   end P;

   function P (Obj : Typ_3) return Boolean is
   begin
      Mark (Typ_3_Id);
      return True;
   end P;

   function Q (Obj : Typ_1) return Boolean is
   begin
      Mark (Typ_1_Id);
      return True;
   end Q;
end DIC_Aspects;

--  tester.ads

package Tester is
   type Type_Id is
     (Deriv_1_Id,
      Deriv_2_Id,
      Deriv_3_Id,
      Deriv_4_Id,
      Deriv_5_Id,
      Deriv_6_Id,
      Deriv_7_Id,
      Deriv_8_Id,
      Deriv_9_Id,
      Deriv_10_Id,
      Par_1_Id,
      Par_2_Id,
      Par_3_Id,
      Par_4_Id,
      Par_5_Id,
      Par_6_Id,
      Par_7_Id,
      Par_8_Id,
      Typ_1_Id,
      Typ_2_Id,
      Typ_3_Id);

   type Results is array (Type_Id) of Natural;

   procedure Mark (Typ : Type_Id);
   --  Mark the result for a particular type as verified

   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 --
   ----------

   procedure Mark (Typ : Type_Id) is
   begin
      State (Typ) := State (Typ) + 1;
   end Mark;

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

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

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

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

   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 ("  " & Index'Img);
            Put_Line ("    Expected:" & Exp_Val'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;

--  dic_main.adb

with DIC_Aspects; use DIC_Aspects;
with Tester;      use Tester;

procedure DIC_Main is
begin
   Reset_Results;
   declare
      Obj : Deriv_1;
   begin
      Test_Results ("Deriv_1", (Par_1_Id => 1,
                                others   => 0));
   end;

   Reset_Results;
   declare
      Obj : Deriv_2;
   begin
      Test_Results ("Deriv_2", (Deriv_2_Id => 1,
                                others     => 0));
   end;

   Reset_Results;
   declare
      Obj : Deriv_3;
   begin
      Test_Results ("Deriv_3", (Deriv_3_Id => 1,
                                others     => 0));
   end;

   Reset_Results;
   declare
      Obj : Deriv_4;
   begin
      Test_Results ("Deriv_4", (Deriv_4_Id => 1,
                                others     => 0));
   end;

   Reset_Results;
   declare
      Obj : Deriv_5;
   begin
      Test_Results ("Deriv_5", (Deriv_5_Id => 1,
                                Par_5_Id   => 1,
                                others     => 0));
   end;

   Reset_Results;
   declare
      Obj : Deriv_6;
   begin
      Test_Results ("Deriv_6", (Par_6_Id => 1,
                                others   => 0));
   end;

   Reset_Results;
   declare
      Obj : Deriv_7;
   begin
      Test_Results ("Deriv_7", (Deriv_7_Id => 1,
                                others     => 0));
   end;

   Reset_Results;
   declare
      Obj : Deriv_8;
   begin
      Test_Results ("Deriv_8", (Deriv_8_Id => 2,
                                Par_8_Id   => 1,
                                others     => 0));
   end;

   Reset_Results;
   declare
      Obj : Deriv_9;
   begin
      Test_Results ("Deriv_9", (Par_1_Id => 1,
                                others   => 0));
   end;

   Reset_Results;
   declare
      Obj : Deriv_10;
   begin
      Test_Results ("Deriv_10", (Deriv_2_Id => 1,
                                 others     => 0));
   end;

   Reset_Results;
   declare
      Obj : Par_1;
   begin
      Test_Results ("Par_1", (Par_1_Id => 1,
                              others   => 0));
   end;

   Reset_Results;
   declare
      Obj : Par_2;
   begin
      Test_Results ("Par_2", (Par_2_Id => 1,
                              others   => 0));
   end;

   Reset_Results;
   declare
      Obj : Par_3;
   begin
      Test_Results ("Par_3", (Par_3_Id => 1,
                              others   => 0));
   end;

   Reset_Results;
   declare
      Obj : Par_4;
   begin
      Test_Results ("Par_4", (Par_4_Id => 1,
                              others   => 0));
   end;

   Reset_Results;
   declare
      Obj : Par_5;
   begin
      Test_Results ("Par_5", (Par_5_Id => 2,
                              others   => 0));
   end;

   Reset_Results;
   declare
      Obj : Par_6;
   begin
      Test_Results ("Par_6", (Par_6_Id => 1,
                              others   => 0));
   end;

   Reset_Results;
   declare
      Obj : Par_7;
   begin
      Test_Results ("Par_7", (Par_7_Id => 1,
                              others   => 0));
   end;

   Reset_Results;
   declare
      Obj : Par_8;
   begin
      Test_Results ("Par_8", (Par_8_Id => 3,
                              others   => 0));
   end;

   Reset_Results;
   declare
      Obj : Typ_1;
   begin
      Test_Results ("Typ_1", (Typ_1_Id => 5,
                              others   => 0));
   end;

   Reset_Results;
   declare
      Obj : Typ_2;
   begin
      Test_Results ("Typ_2", (Typ_1_Id => 3,
                              Typ_2_Id => 2,
                              others   => 0));
   end;

   Reset_Results;
   declare
      Obj : Typ_3;
   begin
      Test_Results ("Typ_3", (Typ_1_Id => 1,
                              Typ_2_Id => 2,
                              Typ_3_Id => 2,
                              others   => 0));
   end;
end DIC_Main;

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

$ gnatmake -q -gnata dic_main.adb
$ ./dic_main
Deriv_1: OK
Deriv_2: OK
Deriv_3: OK
Deriv_4: OK
Deriv_5: OK
Deriv_6: OK
Deriv_7: OK
Deriv_8: OK
Deriv_9: OK
Deriv_10: OK
Par_1: OK
Par_2: OK
Par_3: OK
Par_4: OK
Par_5: OK
Par_6: OK
Par_7: OK
Par_8: OK
Typ_1: OK
Typ_2: OK
Typ_3: OK

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

2017-01-09  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.ads, einfo.adb: Remove uses of flags Has_Default_Init_Cond,
	Is_Default_Init_Cond_Procedure, and
	Has_Inherited_Default_Init_Cond.  Add uses of flags
	Has_Own_DIC, Is_DIC_Procedure, and Has_Inherited_DIC.
	(Default_Init_Cond_Procedure): Removed.
	(DIC_Procedure): New routine.
	(Has_Default_Init_Cond): Removed.
	(Has_DIC): New routine.
	(Has_Inheritable_Invariants): The attribute applies to the base type.
	(Has_Inherited_Default_Init_Cond): Removed.
	(Has_Inherited_DIC): New routine.
	(Has_Inherited_Invariants): The attribute applies to the base type.
	(Has_Own_DIC): New routine.
	(Has_Own_Invariants): The attribute applies to the base type.
	(Is_Default_Init_Cond_Procedure): Removed.
	(Is_DIC_Procedure): New routine.
	(Set_Default_Init_Cond_Procedure): Removed.
	(Set_DIC_Procedure): New routine.
	(Set_Has_Default_Init_Cond): Removed.
	(Set_Has_Inheritable_Invariants): The attribute applies
	to the base type.
	(Set_Has_Inherited_Default_Init_Cond): Removed.
	(Set_Has_Inherited_DIC): New routine.
	(Set_Has_Inherited_Invariants): The attribute applies to the base type.
	(Set_Has_Own_DIC): New routine.
	(Set_Has_Own_Invariants): The attribute applies to the base type.
	(Set_Is_Default_Init_Cond_Procedure): Removed.
	(Set_Is_DIC_Procedure): New routine.
	(Write_Entity_Flags): Update the output of all flags related to
	default initial condition.
	* exp_ch3.adb (Expand_N_Object_Declaration): Update the generation
	of the call to the DIC procedure.
	(Freeze_Type): Generate the body of the DIC procedure.
	* exp_ch7.adb (Build_Invariant_Procedure_Body): Replace
	all occurrences of Create_Append with Append_New_To. Do
	not generate an invariant procedure for a class-wide type.
	The generated body acts as a freeze action of the working type.
	(Build_Invariant_Procedure_Declaration): Do not generate an
	invariant procedure for a class-wide type.
	(Create_Append): Removed.
	* exp_util.adb: Add with and use clauses for Sem_Ch3, sem_ch6,
	sem_Ch12, Sem_Disp, and GNAT.HTable. Move the handling of
	class-wide pre/postcondition description and data structures from
	Sem_Prag.
	(Build_Class_Wide_Expression): Moved from Sem_Prag.
	(Build_DIC_Call): New routine.
	(Build_DIC_Procedure_Body): New routine.
	(Build_DIC_Procedure_Declaration): New routine.
	(Entity_Hash): Moved from Sem_Prag.
	(Find_DIC_Type): New routine.
	(Update_Primitives_Mapping): Reimplemented.
	(Update_Primitives_Mapping_Of_Types): New routine.
	* exp_util.ads (Build_Class_Wide_Expression): Moved from Sem_Prag.
	(Build_DIC_Call): New routine.
	(Build_DIC_Procedure_Body): New routine.
	(Build_DIC_Procedure_Declaration): New routine.
	(Update_Primitives_Mapping): Moved from Sem_Prag.
	(Update_Primitives_Mapping_Of_Types): New routine.
	* nlists.adb (Append_New): New routine.
	(Append_New_To): New routine.
	* nlists.ads (Append_New): New routine.
	(Append_New_To): New routine.
	* sem_ch3.adb (Analyze_Declarations): Do not generate the bodies
	of DIC procedures here. This is now done at the end of the
	visible declarations, private declarations, and at the freeze
	point of a type.
	(Analyze_Private_Extension_Declaration):
	A private extension inherits the DIC pragma of a parent type.
	(Analyze_Subtype_Declaration): No need to propagate invariant
	attributes to a subtype as those apply to the base type.
	(Build_Derived_Record_Type): No need to inherit invariants here
	as this is now done in Build_Derived_Type.
	(Build_Derived_Type): Inherit both the DIC pragma and invariants from
	a parent type.
	(Process_Full_View): Update the propagation of DIC attributes.
	(Propagate_Default_Init_Cond_Attributes): Removed.
	* sem_ch7.adb Add with and use clauses for Exp_Util.
	(Analyze_Package_Specification): Create the body of the DIC
	procedure at the end of the visible and private declarations.
	(Preserve_Full_Attributes): Propagate DIC attributes.
	* sem_ch9.adb (Analyze_Protected_Type_Declaration): Propagate
	DIC attributes.
	(Analyze_Task_Type_Declaration): Propagate DIC attributes.
	* sem_elab.adb (Check_A_Call): Update the call to
	Is_Nontrivial_Default_Init_Cond_Procedure.
	* sem_prag.adb Remove the with and use clauses for
	GNAT.HTable. Move the handling of class- wide pre/postcondition
	description and data structures to Exp_Util.
	(Analyze_Pragma): Create the declaration of the DIC procedure. There
	is no need to propagate invariant-related attributes at this point
	as this is done in Build_Invariant_Procedure_Declaration.
	(Build_Class_Wide_Expression): Moved to Exp_Util.
	(Entity_Hash): Moved to Exp_Util.
	(Update_Primitives_Mapping): Moved to Exp_Util.
	* sem_prag.ads (Build_Class_Wide_Expression): Moved to Exp_Util.
	(Update_Primitives_Mapping): Moved to Exp_Util.
	* sem_util.adb: Remove with and use clauses for Ghost
	and Sem_Ch13.
	(Build_Default_Init_Cond_Call): Removed.
	(Build_Default_Init_Cond_Procedure_Bodies): Removed.
	(Build_Default_Init_Cond_Procedure_Declaration): Removed.
	(Get_Views): Reimplemented.
	(Has_Full_Default_Initialization): Reimplement the section on DIC.
	(Inherit_Default_Init_Cond_Procedure): Removed.
	(Is_Nontrivial_Default_Init_Cond_Procedure): Removed.
	(Is_Nontrivial_DIC_Procedure): New routine.
	(Is_Verifiable_DIC_Pragma): New routine.
	(Propagate_DIC_Attributes): New routine.
	* sem_util.ads (Build_Default_Init_Cond_Call): Removed.
	(Build_Default_Init_Cond_Procedure_Bodies): Removed.
	(Build_Default_Init_Cond_Procedure_Declaration): Removed.
	(Inherit_Default_Init_Cond_Procedure): Removed.
	(Is_Nontrivial_Default_Init_Cond_Procedure): Removed.
	(Is_Nontrivial_DIC_Procedure): New routine.
	(Is_Verifiable_DIC_Pragma): New routine.
	(Propagate_DIC_Attributes): New routine.
	* sem_warn.adb (Is_OK_Fully_Initialized): Reimplement the section
	on DIC.
	* sinfo.ads, sinfo.adb: Add new attribute Expression_Copy along with
	usage in nodes.
	(Expression_Copy): New routine along with pragma Inline.
	(Set_Expression_Copy): New routine along with pragma Inline.

[Ada] Pragma Default_Initial_Condition and tagged types

Commit Message

Patch