Patchwork [Ada] Ada 2012 invariant checks on subcomponents

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

Comments

Arnaud Charlet - Oct. 1, 2012, 8:40 a.m.
If a record has a subvomponent whose type has a defined invariant, then there
must be a invariant check on that component whenever a value of the record type
is created or modified by a visible primitive operation of the type.

The command:

    gnatmake -q -gnat12 -gnata main
    main

must yield:

CHECK
CHECK
CHECK
CHECK
OK
CHECK
CHECK
CHECK
CHECK
CHECK
CHECK

---
with Text_IO; use Text_IO;
with Ada.Assertions; use Ada.Assertions;
with P;
procedure Main is
   V : P.R2; -- Check on the T default initialization? NOK
   Table : P.A2 (1..3);
begin
   begin
      P.P3 (Table);
   exception
      when Assertion_Error => Put_Line ("OK");
   end;
   P.Prim (V.V.V); -- Check on the T reference? OK
   P.P1 (V.V); -- Check on the part? NOK
   P.P2 (V); -- Check on the part? NOK
   declare
     Thing1 : P.R3 := P.F3 (True);
     Thing2 : P.R3 := P.F3 (False);
   begin
      null;
   end;
end Main;
--
package P is

   type T is private with Type_Invariant => Check (T);

   procedure Prim (V : in out T);

   function Check (V : in T) return Boolean;

   type R1 is record
      V : T;
   end record;

   type R2 is record
      V : R1;
   end record;

   type R3 (D : Boolean) is record
      V1 : T;
      case D is
         when True => V2 : T;
         when False => Zero : Integer := 0;
      end case;
   end record;

   type A2 is array (integer range <>) of T;
   procedure P1 (V : in out R1);

   procedure P2 (V : in out R2);
   procedure P3 (T : in out A2);
   function F3 (Yes: Boolean) return R3;

private
   type T is record
      Val : Integer := 17;
   end record;
end P;
---
with Ada.Text_IO; use Ada.Text_IO;
package body P is

   -----------
   -- Check --
   -----------

   function Check (V : in T) return Boolean is
   begin
      Put_Line ("CHECK");
      return V.Val = 17;
   end Check;

   procedure Prim (V : in out T) is
   begin
      null;
   end Prim;

   procedure P1 (V : in out R1) is
   begin
      null;
   end P1;

   procedure P2 (V : in out R2) is
   begin
      null;
   end P2;

   procedure P3 (T : in out A2) is
   begin
      T (T'Last).Val := 18;
      null;
   end P3;

   function F3 (Yes : Boolean) return R3 is
      Result : R3 (Yes);
   begin
      return Result;
   end;
end P;

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

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

	* exp_ch3.adb (Build_Record_Invariant_Proc): new procedure to
	generate a checking procedure for record types that may have
	components whose types have type invariants declared.

Patch

Index: exp_ch3.adb
===================================================================
--- exp_ch3.adb	(revision 191894)
+++ exp_ch3.adb	(working copy)
@@ -118,6 +118,10 @@ 
    --  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
@@ -3611,6 +3615,174 @@ 
       end if;
    end Build_Record_Init_Proc;
 
+   --------------------------------
+   -- Build_Record_Invariant_Proc --
+   --------------------------------
+
+   procedure Build_Record_Invariant_Proc (R_Type : Entity_Id; Nod : Node_Id) is
+      Loc : constant Source_Ptr := Sloc (Nod);
+
+      Object_Name : constant Name_Id := New_Internal_Name ('I');
+      --  Name for argument of invariant procedure
+
+      Object_Entity : constant Node_Id :=
+                        Make_Defining_Identifier (Loc, Object_Name);
+      --  The procedure declaration entity for the argument
+
+      Invariant_Found : Boolean;
+      --  Set if any component needs an invariant check.
+
+      Proc_Id   : Entity_Id;
+      Proc_Body : Node_Id;
+      Stmts     : List_Id;
+      Type_Def  : Node_Id;
+
+      function Build_Invariant_Checks (Comp_List : Node_Id) return List_Id;
+      --  Recursive procedure that generates a list of checks for components
+      --  that need it, and recurses through variant parts when present.
+
+      function Build_Component_Invariant_Call (Comp : Entity_Id)
+      return Node_Id;
+      --  Build call to invariant procedure for a record component.
+
+      ------------------------------------
+      -- Build_Component_Invariant_Call --
+      ------------------------------------
+
+      function Build_Component_Invariant_Call (Comp : Entity_Id)
+      return Node_Id
+      is
+         Sel_Comp : Node_Id;
+
+      begin
+         Invariant_Found := True;
+         Sel_Comp :=
+           Make_Selected_Component (Loc,
+             Prefix      => New_Occurrence_Of (Object_Entity, Loc),
+             Selector_Name => New_Occurrence_Of (Comp, Loc));
+
+         return
+           Make_Procedure_Call_Statement (Loc,
+             Name                   =>
+               New_Occurrence_Of
+                 (Invariant_Procedure (Etype (Comp)), Loc),
+             Parameter_Associations => New_List (Sel_Comp));
+      end Build_Component_Invariant_Call;
+
+      ----------------------------
+      -- Build_Invariant_Checks --
+      ----------------------------
+
+      function Build_Invariant_Checks (Comp_List : Node_Id) return List_Id is
+         Decl     : Node_Id;
+         Id       : Entity_Id;
+         Stmts    : List_Id;
+
+      begin
+         Stmts := New_List;
+         Decl := First_Non_Pragma (Component_Items (Comp_List));
+
+         while Present (Decl) loop
+            if Nkind (Decl) = N_Component_Declaration then
+               Id  := Defining_Identifier (Decl);
+               if Has_Invariants (Etype (Id)) then
+                  Append_To (Stmts, Build_Component_Invariant_Call (Id));
+               end if;
+            end if;
+
+            Next (Decl);
+         end loop;
+
+         if Present (Variant_Part (Comp_List)) then
+            declare
+               Variant_Alts  : constant List_Id := New_List;
+               Var_Loc       : Source_Ptr;
+               Variant       : Node_Id;
+               Variant_Stmts : List_Id;
+
+            begin
+               Variant :=
+                 First_Non_Pragma (Variants (Variant_Part (Comp_List)));
+               while Present (Variant) loop
+                  Variant_Stmts :=
+                    Build_Invariant_Checks (Component_List (Variant));
+                  Var_Loc := Sloc (Variant);
+                  Append_To (Variant_Alts,
+                    Make_Case_Statement_Alternative (Var_Loc,
+                      Discrete_Choices =>
+                        New_Copy_List (Discrete_Choices (Variant)),
+                      Statements => Variant_Stmts));
+
+                  Next_Non_Pragma (Variant);
+               end loop;
+
+               --  The expression in the case statement is the reference to
+               --  the discriminant of the target object.
+
+               Append_To (Stmts,
+                 Make_Case_Statement (Var_Loc,
+                   Expression =>
+                     Make_Selected_Component (Var_Loc,
+                      Prefix => New_Occurrence_Of (Object_Entity, Var_Loc),
+                      Selector_Name => New_Occurrence_Of
+                        (Entity
+                          (Name (Variant_Part (Comp_List))), Var_Loc)),
+                      Alternatives => Variant_Alts));
+            end;
+         end if;
+
+         return Stmts;
+      end Build_Invariant_Checks;
+
+   begin
+      Invariant_Found := False;
+      Type_Def := Type_Definition (Parent (R_Type));
+      if Nkind (Type_Def) = N_Record_Definition
+        and then  not Null_Present (Type_Def)
+      then
+         Stmts :=
+           Build_Invariant_Checks (Component_List (Type_Def));
+      else
+         return;
+      end if;
+
+      if not Invariant_Found then
+         return;
+      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,
+          Specification =>
+            Make_Procedure_Specification (Loc,
+              Defining_Unit_Name       => Proc_Id,
+              Parameter_Specifications => New_List (
+                Make_Parameter_Specification (Loc,
+                  Defining_Identifier => Object_Entity,
+                  Parameter_Type      => New_Occurrence_Of (R_Type, Loc)))),
+
+          Declarations               => Empty_List,
+          Handled_Statement_Sequence =>
+            Make_Handled_Sequence_Of_Statements (Loc,
+              Statements => Stmts));
+
+      Set_Ekind          (Proc_Id, E_Procedure);
+      Set_Is_Public      (Proc_Id, Is_Public (R_Type));
+      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);
+   end Build_Record_Invariant_Proc;
+
    ----------------------------
    -- Build_Slice_Assignment --
    ----------------------------
@@ -6637,6 +6809,10 @@ 
             end loop;
          end;
       end if;
+
+      if not Has_Invariants (Def_Id) then
+         Build_Record_Invariant_Proc (Def_Id, N);
+      end if;
    end Expand_Freeze_Record_Type;
 
    ------------------------------