diff mbox

[Ada] Missing type invariant check on view conversion

Message ID 20170112132431.GA125129@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Jan. 12, 2017, 1:24 p.m. UTC 
This patch corrects an issue with "out" or "in out" arguments producing wrong
code when the argument is view converted. According to RM 7.3.2 (11-14)
invariant checks of intermediate types must be preformed in the order of the
parent to the child (skipping the parent) after the subprogram. With this
patch the appropriate calls to invariant checksare inserted after the
subprogram during expansion.

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

--  invariants.ads

package Invariants is

   -------------
   -- Testing --
   -------------

   type Type_Id is
     (Tag_1_Id,
      Tag_1_FV_Id,
      Tag_2_Id,
      Tag_2_FV_Id,
      Tag_3_Id,
      Tag_4_Id,
      Tag_4_FV_Id,
      Tag_5_Id,
      Tag_5_FV_Id,
      Tag_6_Id,
      Tag_7_Id,
      Iface_1_Id,
      Iface_2_Id,
      Iface_3_Id,
      Iface_4_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.

   ----------------
   -- Interfaces --
   ----------------

   type Iface_1 is interface
     with Type_Invariant'Class => Mark (Iface_1_Id);

   type Iface_2 is interface
     with Type_Invariant'Class => Mark (Iface_2_Id);

   type Iface_3 is interface and Iface_1 and Iface_2;

   type Iface_4 is interface and Iface_3
     with Type_Invariant'Class => Mark (Iface_4_Id);

   ------------------
   -- Tagged types --
   ------------------

   type Tag_1 is tagged private
     with Type_Invariant'Class => Mark (Tag_1_Id);

   type Tag_2 is new Tag_1 and Iface_1 and Iface_4 with private;

   type Tag_3 is new Tag_2 and Iface_2 and Iface_3 with private
     with Type_Invariant => Mark (Tag_3_Id);

   type Tag_4 is new Tag_3 and Iface_4 with private
     with Type_Invariant'Class => Mark (Tag_4_Id);

   type Tag_5 is tagged private;

   type Tag_6 is new Tag_5 with private
     with Type_Invariant => Mark (Tag_6_Id);

   type Tag_7 is new Tag_6 with private
     with Type_Invariant'Class => Mark (Tag_7_Id);

private

   type Tag_1 is tagged null record
     with Type_Invariant => Mark (Tag_1_FV_Id);
   --  own:         Tag_1_Id, Tag_1_FV_Id
   --  inheritable: Tag_1_Id

   type Tag_2 is new Tag_1 and Iface_1 and Iface_4 with null record
     with Type_Invariant => Mark (Tag_2_FV_Id);
   --  own:       Tag_2_FV_Id
   --  inherited: Tag_1_Id, Iface_1_Id, Iface_2_Id, Iface_4_Id

   type Tag_3 is new Tag_2 and Iface_2 and Iface_3 with null record;
   --  own:       Tag_3_Id
   --  inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_1_Id

   type Tag_4 is new Tag_3 and Iface_4 with null record
     with Type_Invariant => Mark (Tag_4_FV_Id);
   --  own:         Tag_4_Id, Tag_4_FV_Id
   --  inheritable: Tag_4_Id
   --  inherited  : Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_1_Id

   type Tag_5 is tagged null record
     with Type_Invariant => Mark (Tag_5_FV_Id);
   --  own: Tag_5_FV_Id

   type Tag_6 is new Tag_5 with null record;
   --  own: Tag_6_Id

   type Tag_7 is new Tag_6 with null record;
   --  own: Tag_7_Id

end Invariants;

--  invariants.adb

with Ada.Text_IO; use Ada.Text_IO;

package body Invariants is

   State : Results;

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

   function Mark (Typ : Type_Id) return Boolean is
   begin
      State (Typ) := True;
      Put_Line ("     Check: " & Typ'Img);
      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 Invariants;

--  fail.adb

procedure Fail is

   package Derived is

      type T is tagged private;
      type D is new T with private;
      type E is new D with private;

      procedure Create (X : out T);

   private

      type T is tagged record
         C : Integer;
      end record;

      type D is new T with null record
        with Type_Invariant => D.C /= 0;

      type E is new D with null record;

   end Derived;

   package body Derived is

      procedure Create (X : out T) is
      begin
         X.C := 0;
      end Create;

   end Derived;

   X : Derived.E;

begin
   Derived.Create (Derived.T(X)); --  ERROR
end Fail;

--  pass.adb

with Invariants; use Invariants;

procedure Pass is

begin
   Reset_Results;
   declare
      Obj : Tag_2;
      procedure Call_Tag_1 (Item : out Tag_1) is
      begin
        null;
      end;
   begin
      Call_Tag_1 (Tag_1 (Obj));
      Test_Results ("Tag_2", (Tag_1_Id    => True,
                              Tag_2_FV_Id => True,
                              Iface_1_Id  => True,
                              Iface_2_Id  => True,
                              Iface_4_Id  => True,
                              others      => False));    --  OK
   end;

   Reset_Results;
   declare
      Obj : Tag_3;
      procedure Call_Tag_2 (Item : out Tag_2) is
      begin
        null;
      end;
   begin
      Call_Tag_2 (Tag_2 (Obj));
      Test_Results ("Tag_3", (Tag_1_Id    => True,
                              Tag_3_Id    => True,
                              Iface_1_Id  => True,
                              Iface_2_Id  => True,
                              Iface_4_Id  => True,
                              others      => False));    --  OK
   end;

   Reset_Results;
   declare
      Obj : Tag_4;
      procedure Call_Tag_2 (Item : out Tag_2) is
      begin
        null;
      end;
   begin
      Call_Tag_2 (Tag_2 (Obj));
      Test_Results ("Tag_4", (Tag_1_Id    => True,
                              Tag_3_Id    => True,
                              Tag_4_Id    => True,
                              Tag_4_FV_Id => True,
                              Iface_1_Id  => True,
                              Iface_2_Id  => True,
                              Iface_4_Id  => True,
                              others      => False));    --  OK
   end;

   Reset_Results;
   declare
      Obj : Tag_6;
      procedure Call_Tag_5 (Item : out Tag_5) is
      begin
        null;
      end;
   begin
      Call_Tag_5 (Tag_5 (Obj));
      Test_Results ("Tag_6", (Tag_6_Id => True,
                              others   => False));       --  OK
   end;

   Reset_Results;
   declare
      Obj : Tag_7;
      procedure Call_Tag_5 (Item : out Tag_5) is
      begin
        null;
      end;
   begin
      Call_Tag_5 (Tag_5 (Tag_6 (Obj)));
      Test_Results ("Tag_7", (Tag_6_Id => True,
                              Tag_7_Id => True,
                              others   => False));       --  OK
   end;

   Reset_Results;
   declare
      Obj : Tag_4;
      procedure Call_Tag_1 (Item : out Tag_1) is
      begin
         null;
      end;
   begin
      Call_Tag_1 (Tag_1 (Obj));
      Test_Results ("Tag_4 #2", (Tag_1_Id    => True,
                                 Tag_2_FV_Id => True,
                                 Tag_3_Id    => True,
                                 Tag_4_Id    => True,
                                 Tag_4_FV_Id => True,
                                 Iface_1_Id  => True,
                                 Iface_2_Id  => True,
                                 Iface_4_Id  => True,
                                 others      => False)); -- OK
   end;
end Pass;

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

$ gnatmake -q -gnata -gnatws pass.adb
$ pass
$ gnatmake -q -gnata -gnatws fail.adb
$ fail
     Check: TAG_2_FV_ID
     Check: TAG_1_ID
     Check: IFACE_1_ID
     Check: IFACE_2_ID
     Check: IFACE_4_ID
     Check: TAG_2_FV_ID
     Check: TAG_1_ID
     Check: IFACE_1_ID
     Check: IFACE_2_ID
     Check: IFACE_4_ID
Tag_2: OK
     Check: TAG_3_ID
     Check: TAG_1_ID
     Check: IFACE_1_ID
     Check: IFACE_2_ID
     Check: IFACE_4_ID
     Check: TAG_3_ID
     Check: TAG_1_ID
     Check: IFACE_1_ID
     Check: IFACE_2_ID
     Check: IFACE_4_ID
Tag_3: OK
     Check: TAG_4_ID
     Check: TAG_4_FV_ID
     Check: TAG_1_ID
     Check: IFACE_1_ID
     Check: IFACE_2_ID
     Check: IFACE_4_ID
     Check: TAG_3_ID
     Check: TAG_1_ID
     Check: IFACE_1_ID
     Check: IFACE_2_ID
     Check: IFACE_4_ID
     Check: TAG_4_ID
     Check: TAG_4_FV_ID
     Check: TAG_1_ID
     Check: IFACE_1_ID
     Check: IFACE_2_ID
     Check: IFACE_4_ID
Tag_4: OK
     Check: TAG_6_ID
     Check: TAG_6_ID
Tag_6: OK
     Check: TAG_7_ID
     Check: TAG_6_ID
     Check: TAG_6_ID
     Check: TAG_7_ID
Tag_7: OK
     Check: TAG_4_ID
     Check: TAG_4_FV_ID
     Check: TAG_1_ID
     Check: IFACE_1_ID
     Check: IFACE_2_ID
     Check: IFACE_4_ID
     Check: TAG_2_FV_ID
     Check: TAG_1_ID
     Check: IFACE_1_ID
     Check: IFACE_2_ID
     Check: IFACE_4_ID
     Check: TAG_3_ID
     Check: TAG_1_ID
     Check: IFACE_1_ID
     Check: IFACE_2_ID
     Check: IFACE_4_ID
     Check: TAG_4_ID
     Check: TAG_4_FV_ID
     Check: TAG_1_ID
     Check: IFACE_1_ID
     Check: IFACE_2_ID
     Check: IFACE_4_ID
Tag_4 #2: OK

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed invariant from fail.adb:18

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

2017-01-12  Justin Squirek  <squirek@adacore.com>

	* exp_ch6.adb (Check_View_Conversion): Created this function
	to properly chain calls to check type invariants that may be
	present in a subprogram call after the subprogram.
	(Expand_Call): Add a conditional to identify when a view conversion
	needs to be checked.
	* nlists.adb, nlists.ads (Prepend_New): New routine.
	(Prepend_New_To): New routine.
diff mbox

Patch

Index: nlists.adb
===================================================================
--- nlists.adb	(revision 244350)
+++ nlists.adb	(working copy)
@@ -1158,6 +1158,28 @@ 
       Prepend_List (List, To);
    end Prepend_List_To;
 
+   -----------------
+   -- Prepend_New --
+   -----------------
+
+   procedure Prepend_New (Node : Node_Or_Entity_Id; To : in out List_Id) is
+   begin
+      if No (To) then
+         To := New_List;
+      end if;
+
+      Prepend (Node, To);
+   end Prepend_New;
+
+   --------------------
+   -- Prepend_New_To --
+   --------------------
+
+   procedure Prepend_New_To (To : in out List_Id; Node : Node_Or_Entity_Id) is
+   begin
+      Prepend_New (Node, To);
+   end Prepend_New_To;
+
    ----------------
    -- Prepend_To --
    ----------------
Index: nlists.ads
===================================================================
--- nlists.ads	(revision 244350)
+++ nlists.ads	(working copy)
@@ -289,12 +289,6 @@ 
    --  node list. An attempt to prepend an error node is ignored without
    --  complaint and the list is unchanged.
 
-   procedure Prepend_To
-     (To   : List_Id;
-      Node : Node_Or_Entity_Id);
-   pragma Inline (Prepend_To);
-   --  Like Prepend, but arguments are the other way round
-
    procedure Prepend_List
      (List : List_Id;
       To   : List_Id);
@@ -307,6 +301,22 @@ 
    pragma Inline (Prepend_List_To);
    --  Like Prepend_List, but arguments are the other way round
 
+   procedure Prepend_New (Node : Node_Or_Entity_Id; To : in out List_Id);
+   pragma Inline (Append_New);
+   --  Prepends Node at the end of node list To. If To is non-existent list, a
+   --  list is created. Node must be a non-empty node that is not already a
+   --  member of a node list, and To must be a node list.
+
+   procedure Prepend_New_To (To : in out List_Id; Node : Node_Or_Entity_Id);
+   pragma Inline (Append_New_To);
+   --  Like Prepend_New, but the arguments are in reverse order
+
+   procedure Prepend_To
+     (To   : List_Id;
+      Node : Node_Or_Entity_Id);
+   pragma Inline (Prepend_To);
+   --  Like Prepend, but arguments are the other way round
+
    procedure Remove (Node : Node_Or_Entity_Id);
    --  Removes Node, which must be a node that is a member of a node list,
    --  from this node list. The contents of Node are not otherwise affected.
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb	(revision 244353)
+++ exp_ch6.adb	(working copy)
@@ -2264,6 +2264,11 @@ 
       --  expression for the value of the actual, EF is the entity for the
       --  extra formal.
 
+      procedure Check_View_Conversion (Formal : Entity_Id; Actual : Node_Id);
+      --  Adds Invariant checks for every intermediate type between
+      --  the range of a view converted argument to its ancestor (from
+      --  parent to child).
+
       function Inherited_From_Formal (S : Entity_Id) return Entity_Id;
       --  Within an instance, a type derived from an untagged formal derived
       --  type inherits from the original parent, not from the actual. The
@@ -2351,6 +2356,57 @@ 
       end Add_Extra_Actual;
 
       ---------------------------
+      -- Check_View_Conversion --
+      ---------------------------
+
+      procedure Check_View_Conversion (Formal : Entity_Id; Actual : Node_Id) is
+         Arg        : Entity_Id;
+         Curr_Typ   : Entity_Id := Empty;
+         Inv_Checks : List_Id;
+         Par_Typ    : Entity_Id;
+
+      begin
+         Inv_Checks := No_List;
+
+         --  Extract actual object for type conversions
+
+         Arg := Actual;
+         while Nkind (Arg) = N_Type_Conversion loop
+            Arg := Expression (Arg);
+         end loop;
+
+         --  Move up the derivation chain starting with the type of the
+         --  the formal parameter down to the type of the actual object.
+
+         Par_Typ := Etype (Arg);
+         while Par_Typ /= Etype (Formal) and Par_Typ /= Curr_Typ loop
+            Curr_Typ := Par_Typ;
+            if Has_Invariants (Curr_Typ)
+              and then Present (Invariant_Procedure (Curr_Typ))
+            then
+               --  Verify the invariate of the current type. Generate:
+               --    Invariant_Check_Curr_Typ (Curr_Typ (Arg));
+
+               Prepend_New_To (Inv_Checks,
+                 Make_Procedure_Call_Statement (Loc,
+                   Name                   =>
+                     New_Occurrence_Of
+                       (Invariant_Procedure (Curr_Typ), Loc),
+                   Parameter_Associations => New_List (
+                     Make_Type_Conversion (Loc,
+                       Subtype_Mark => New_Occurrence_Of (Curr_Typ, Loc),
+                       Expression   => New_Copy_Tree (Arg)))));
+            end if;
+
+            Par_Typ := Base_Type (Etype (Curr_Typ));
+         end loop;
+
+         if not Is_Empty_List (Inv_Checks) then
+            Insert_Actions_After (N, Inv_Checks);
+         end if;
+      end Check_View_Conversion;
+
+      ---------------------------
       -- Inherited_From_Formal --
       ---------------------------
 
@@ -3233,6 +3289,17 @@ 
                 Duplicate_Subexpr_Move_Checks (Actual)));
          end if;
 
+         --  Invariant checks are performed for every intermediate type between
+         --  the range of a view converted argument to its ancestor (from
+         --  parent to child) if it is passed as an "out" or "in out" parameter
+         --  after executing the call (RM 7.3.2 (11-14)).
+
+         if Ekind (Formal) /= E_In_Parameter
+           and then Nkind (Actual) = N_Type_Conversion
+         then
+            Check_View_Conversion (Formal, Actual);
+         end if;
+
          --  This label is required when skipping extra actual generation for
          --  Unchecked_Union parameters.