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 <squi...@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.
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.
