[Ada] Valid postconditions incorrectly rejected.

Message ID 20211011133949.GA1519117@adacore.com
State New
Headers show
  • [Ada] Valid postconditions incorrectly rejected.
Related show

Commit Message

Aldy Hernandez via Gcc-patches Oct. 11, 2021, 1:39 p.m.
For users, 'Old attribute references are only allowed within
postcondition expressions. Internally, the FE may build trees that
transiently (before some subsequent transformation) violate these rules;
this is ok, but these violations were being incorrectly flagged in some
cases. Fix this problem.

The customer's example for this ticket also demonstrates a second
problem.  Exp_Util.Insert_Actions was willing to take an action (e.g.,
the constraint check for an array indexing expression) that contains a
reference to the loop parameter of a
N_Iterated_Component/Element_Association and insert it in the tree
somewhere above that node, so that the reference ends up outside of the
scope of the declaration it refers to. This leads to a bugbox failure
(gigi is understandably unhappy with the resulting malformed tree). Fix
this too.

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


	* sem_attr.adb (Analyze_Attribute_Old_Result): Permit an
	attribute reference inside a compiler-generated _Postconditions
	procedure. In this case, Subp_Decl is assigned the declaration
	of the enclosing subprogram.
	* exp_util.adb (Insert_Actions): When climbing up the tree
	looking for an insertion point, do not climb past an
	N_Iterated_Component/Element_Association, since this could
	result in inserting a reference to a loop parameter at a
	location outside of the scope of that loop parameter. On the
	other hand, be careful to preserve existing behavior in the case
	of an N_Component_Association node.


diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -7619,8 +7619,18 @@  package body Exp_Util is
                | N_Iterated_Component_Association
                | N_Iterated_Element_Association
-               if Nkind (Parent (P)) = N_Aggregate
-                 and then Present (Loop_Actions (P))
+               if Nkind (Parent (P)) in N_Aggregate | N_Delta_Aggregate
+                 --  We must not climb up out of an N_Iterated_xxx_Association
+                 --  because the actions might contain references to the loop
+                 --  parameter. But it turns out that setting the Loop_Actions
+                 --  attribute in the case of an N_Component_Association
+                 --  when the attribute was not already set can lead to
+                 --  (as yet not understood) bugboxes (gcc failures that are
+                 --  presumably due to malformed trees). So we don't do that.
+                 and then (Nkind (P) /= N_Component_Association
+                            or else Present (Loop_Actions (P)))
                   if Is_Empty_List (Loop_Actions (P)) then
                      Set_Loop_Actions (P, Ins_Actions);

diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -1413,6 +1413,15 @@  package body Sem_Attr is
             end if;
+         --  'Old attribute reference ok in a _Postconditions procedure
+         elsif Nkind (Prag) = N_Subprogram_Body
+           and then not Comes_From_Source (Prag)
+           and then Nkind (Corresponding_Spec (Prag)) = N_Defining_Identifier
+           and then Chars (Corresponding_Spec (Prag)) = Name_uPostconditions
+         then
+            null;
          --  Otherwise the placement of the attribute is illegal
@@ -1424,6 +1433,15 @@  package body Sem_Attr is
          if Nkind (Prag) = N_Aspect_Specification then
             Subp_Decl := Parent (Prag);
+         elsif Nkind (Prag) = N_Subprogram_Body then
+            declare
+               Enclosing_Scope : constant Node_Id :=
+                 Scope (Corresponding_Spec (Prag));
+            begin
+               pragma Assert (Postconditions_Proc (Enclosing_Scope)
+                               = Corresponding_Spec (Prag));
+               Subp_Decl := Parent (Parent (Enclosing_Scope));
+            end;
             Subp_Decl := Find_Related_Declaration_Or_Body (Prag);
          end if;