Patchwork [Ada] Additional invariant checks on composite types

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 1, 2012, 8:49 a.m.
Message ID <20121001084927.GA9662@adacore.com>
Download mbox | patch
Permalink /patch/188244/
State New
Headers show

Comments

Arnaud Charlet - Oct. 1, 2012, 8:49 a.m.
If a composite type has a declared invariant, and some of its compoents are of
types that have their own invariants, the invariant checks on those compoents
must be added to the invariant checks for the enclosing type.

The command;

   gnatmake -q -gnat12 -gnata test_bars
   test_bars

must yield:

   chart invariant violation detected
   value invariant violation detected

with Ada.Assertions; use Ada.Assertions;
with Bars; use Bars;
with Text_IO; use Text_IO;
procedure Test_Bars is
   B : Bar_chart := Bare_Bar (5);
   D : Data (1 .. 5) := (20, 20, 20, 20, 19);
begin
   begin
      Assemble (D, B);
   exception
      when Assertion_Error => Put_Line ("chart invariant violation detected");
   end;

   declare
      D : Data (1 .. 5) := (30, 30, 30, 30, -20);
   begin
      Assemble (D, B);
   exception
      when Assertion_Error => Put_Line ("value invariant violation detected");
   end;
end;
---
package Bars is
   type Value is private
     with Invariant => Legal (Value);

   type Bar_Chart (<>) is private
     with Invariant => Complete (Bar_Chart);

   type Data is array (positive range <>) of Integer;

   function Legal (It : Value) return Boolean;
   function Complete (It : Bar_Chart) return Boolean;
   function Bare_Bar (N : Positive) return Bar_Chart;
   procedure Assemble (From : Data; Result : out Bar_Chart);
private
   type Value is new Integer;
   type Bar_Chart is array (positive range <>) of Value;
end;
--- 
package body  Bars is
   --  type Value is private
   --    with Invariant => Legal (Value);

   --  type Bar_Chart is private
   --    with Invariant => Complete (Bar_Chart);

   function Legal (It : Value) return Boolean is
   begin
      return It >= 0 and It <= 100;
   end;

   function Complete (It : Bar_Chart) return Boolean is
      Total : Value := 0;
   begin
      for B of It loop Total := Total + B; end loop;
      return Total = 100;
   end;
      
   function Bare_Bar (N : Positive) return Bar_Chart is
      Result : Bar_Chart (1 .. N) := (100, others => 0);
   begin
      return Result;
   end;
      
   
   procedure Assemble (From : Data; Result : out Bar_Chart) is
   begin
      for J in From'range loop
         Result (J) := Value (From (J));
      end loop;
   end;
end;

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

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

	* exp_ch3.ads (Build_Array_Invariant_Proc): moved to body.
	* exp_ch3.adb (Build_Array_Invariant_Proc,
	Build_Record_Invariant_Proc): transform into functions.
	(Insert_Component_Invariant_Checks): for composite types that have
	components with specified invariants, build a checking procedure,
	and make into the invariant procedure of the composite type,
	or incorporate it into the user- defined invariant procedure if
	one has been created.
	* sem_ch3.adb (Array_Type_Declaration): Checking for invariants
	on the component type is defered to the expander.

Patch

Index: exp_ch3.adb
===================================================================
--- exp_ch3.adb	(revision 191902)
+++ exp_ch3.adb	(working copy)
@@ -88,6 +88,22 @@ 
    --  used for attachment of any actions required in its construction.
    --  It also supplies the source location used for the procedure.
 
+   function Build_Array_Invariant_Proc
+     (A_Type : Entity_Id;
+      Nod    : Node_Id) return Node_Id;
+   --  If the component of type of array type has invariants, build procedure
+   --  that checks invariant on all components of the array. Ada 2012 specifies
+   --  that an invariant on some type T must be applied to in-out parameters
+   --  and return values that include a part of type T. If the array type has
+   --  an otherwise specified invariant, the component check procedure is
+   --  called from within the user-specified invariant. Otherwise this becomes
+   --  the invariant procedure for the array type.
+
+   function Build_Record_Invariant_Proc
+     (R_Type : Entity_Id;
+      Nod    : Node_Id) return Node_Id;
+   --  Ditto for record types.
+
    function Build_Discriminant_Formals
      (Rec_Id : Entity_Id;
       Use_Dl : Boolean) return List_Id;
@@ -118,10 +134,6 @@ 
    --  Build record initialization procedure. N is the type declaration
    --  node, and Rec_Ent is the corresponding entity for the record type.
 
-   procedure Build_Record_Invariant_Proc (R_Type : Entity_Id; Nod : Node_Id);
-   --  If the record type has components whose types have invariant, build
-   --  an invariant procedure for the record type itself.
-
    procedure Build_Slice_Assignment (Typ : Entity_Id);
    --  Build assignment procedure for one-dimensional arrays of controlled
    --  types. Other array and slice assignments are expanded in-line, but
@@ -184,6 +196,14 @@ 
    --  Treat user-defined stream operations as renaming_as_body if the
    --  subprogram they rename is not frozen when the type is frozen.
 
+   procedure Insert_Component_Invariant_Checks
+     (N   : Node_Id;
+     Typ  : Entity_Id;
+     Proc : Node_Id);
+   --  If a composite type has invariants and also has components with defined
+   --  invariants. the component invariant procedure is inserted into the user-
+   --  defined invariant procedure and added to the checks to be performed.
+
    procedure Initialization_Warning (E : Entity_Id);
    --  If static elaboration of the package is requested, indicate
    --  when a type does meet the conditions for static initialization. If
@@ -788,7 +808,10 @@ 
    -- Build_Array_Invariant_Proc --
    --------------------------------
 
-   procedure Build_Array_Invariant_Proc (A_Type : Entity_Id; Nod : Node_Id) is
+   function Build_Array_Invariant_Proc
+     (A_Type : Entity_Id;
+      Nod    : Node_Id) return Node_Id
+   is
       Loc : constant Source_Ptr := Sloc (Nod);
 
       Object_Name : constant Name_Id := New_Internal_Name ('I');
@@ -882,9 +905,7 @@ 
 
       Proc_Id :=
         Make_Defining_Identifier (Loc,
-           Chars => New_External_Name (Chars (A_Type), "Invariant"));
-      Set_Has_Invariants (Proc_Id);
-      Set_Invariant_Procedure (A_Type, Proc_Id);
+           Chars => New_External_Name (Chars (A_Type), "CInvariant"));
 
       Body_Stmts := Check_One_Dimension (1);
 
@@ -912,10 +933,7 @@ 
          Set_Debug_Info_Off (Proc_Id);
       end if;
 
-      --  The procedure body is placed after the freeze node for the type.
-
-      Insert_After (Nod, Proc_Body);
-      Analyze (Proc_Body);
+      return Proc_Body;
    end Build_Array_Invariant_Proc;
 
    --------------------------------
@@ -3619,7 +3637,10 @@ 
    -- Build_Record_Invariant_Proc --
    --------------------------------
 
-   procedure Build_Record_Invariant_Proc (R_Type : Entity_Id; Nod : Node_Id) is
+   function Build_Record_Invariant_Proc
+     (R_Type : Entity_Id;
+      Nod    : Node_Id) return Node_Id
+   is
       Loc : constant Source_Ptr := Sloc (Nod);
 
       Object_Name : constant Name_Id := New_Internal_Name ('I');
@@ -3745,19 +3766,16 @@ 
       then
          Stmts := Build_Invariant_Checks (Component_List (Type_Def));
       else
-         return;
+         return Empty;
       end if;
 
       if not Invariant_Found then
-         return;
+         return Empty;
       end if;
 
       Proc_Id :=
         Make_Defining_Identifier (Loc,
            Chars => New_External_Name (Chars (R_Type), "Invariant"));
-      Set_Has_Invariants (Proc_Id);
-      Set_Has_Invariants (R_Type);
-      Set_Invariant_Procedure (R_Type, Proc_Id);
 
       Proc_Body :=
         Make_Subprogram_Body (Loc,
@@ -3779,10 +3797,9 @@ 
       Set_Is_Internal    (Proc_Id);
       Set_Has_Completion (Proc_Id);
 
-      --  The procedure body is placed after the freeze node for the type.
-
-      Insert_After (Nod, Proc_Body);
-      Analyze (Proc_Body);
+      return Proc_Body;
+      --  Insert_After (Nod, Proc_Body);
+      --  Analyze (Proc_Body);
    end Build_Record_Invariant_Proc;
 
    ----------------------------
@@ -5843,7 +5860,11 @@ 
       end if;
 
       if Has_Invariants (Component_Type (Base)) then
-         Build_Array_Invariant_Proc (Base, N);
+
+         --  Generate component invariant checking procedure.
+
+         Insert_Component_Invariant_Checks
+           (N, Base, Build_Array_Invariant_Proc (Base, N));
       end if;
    end Expand_Freeze_Array_Type;
 
@@ -6812,9 +6833,11 @@ 
          end;
       end if;
 
-      if not Has_Invariants (Def_Id) then
-         Build_Record_Invariant_Proc (Def_Id, N);
-      end if;
+      --  Check whether individual components have a defined invariant,
+      --  and add the corresponding component invariant checks.
+
+      Insert_Component_Invariant_Checks
+        (N, Def_Id, Build_Record_Invariant_Proc (Def_Id, N));
    end Expand_Freeze_Record_Type;
 
    ------------------------------
@@ -7579,6 +7602,63 @@ 
       return Is_RTU (S1, System) or else Is_RTU (S1, Ada);
    end In_Runtime;
 
+   ---------------------------------------
+   -- Insert_Component_Invariant_Checks --
+   ---------------------------------------
+
+   procedure Insert_Component_Invariant_Checks
+     (N   : Node_Id;
+     Typ  : Entity_Id;
+     Proc : Node_Id)
+   is
+      Loc     : constant Source_Ptr := Sloc (Typ);
+      Proc_Id : Entity_Id;
+
+   begin
+      if Present (Proc) then
+         Proc_Id := Defining_Entity (Proc);
+
+         if not Has_Invariants (Typ) then
+            Set_Has_Invariants (Typ);
+            Set_Has_Invariants (Proc_Id);
+            Set_Invariant_Procedure (Typ, Proc_Id);
+            Insert_After (N, Proc);
+            Analyze (Proc);
+
+         else
+
+            --  Find already created invariant body, insert body of component
+            --  invariant proc in it, and add call after other checks.
+
+            declare
+               Bod : Node_Id;
+               Inv_Id : constant Entity_Id := Invariant_Procedure (Typ);
+               Call   : constant Node_Id :=
+                 Make_Procedure_Call_Statement (Loc,
+                   Name => New_Occurrence_Of (Proc_Id, Loc),
+                   Parameter_Associations =>
+                     New_List
+                       (New_Reference_To (First_Formal (Inv_Id), Loc)));
+
+            begin
+
+               --  The invariant  body has not been analyzed yet, so we do a
+               --  sequential search forward, and retrieve it by name.
+
+               Bod := Next (N);
+               while Present (Bod) loop
+                  exit when Nkind (Bod) = N_Subprogram_Body
+                    and then Chars (Defining_Entity (Bod)) = Chars (Inv_Id);
+                  Next (Bod);
+               end loop;
+
+               Append_To (Declarations (Bod), Proc);
+               Append_To (Statements (Handled_Statement_Sequence (Bod)), Call);
+            end;
+         end if;
+      end if;
+   end Insert_Component_Invariant_Checks;
+
    ----------------------------
    -- Initialization_Warning --
    ----------------------------
Index: exp_ch3.ads
===================================================================
--- exp_ch3.ads	(revision 191888)
+++ exp_ch3.ads	(working copy)
@@ -46,12 +46,6 @@ 
    procedure Expand_Record_Extension (T : Entity_Id; Def : Node_Id);
    --  Add a field _parent in the extension part of the record
 
-   procedure Build_Array_Invariant_Proc (A_Type : Entity_Id; Nod : Node_Id);
-   --  If the component of type of array type has invariants, build procedure
-   --  that checks invariant on all components of the array. Ada 2012 specifies
-   --  that an invariant on some type T must be applied to in-out parameters
-   --  and return values that include a part of type T.
-
    procedure Build_Discr_Checking_Funcs (N : Node_Id);
    --  Builds function which checks whether the component name is consistent
    --  with the current discriminants. N is the full type declaration node,
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 191898)
+++ sem_ch3.adb	(working copy)
@@ -4974,12 +4974,9 @@ 
             Subtype_Indication (Component_Def));
       end if;
 
-      --  Ada 2012: if the element type has invariants we must create an
-      --  invariant procedure for the array type as well.
-
-      if Has_Invariants (Element_Type) then
-         Set_Has_Invariants (T);
-      end if;
+      --  There may be an invariant declared for the component type, but
+      --  the construction of the component invariant checking procedure
+      --  takes place during expansion.
    end Array_Type_Declaration;
 
    ------------------------------------------------------