From: Gary Dismukes <dismu...@adacore.com>

GNAT was incorrectly implementing the Ada rules for resolving calls to
primitive functions within inherited class-wide pre- and postconditions,
as specified in RM22 6.1.1 (relating to AI12-0113).  Only function calls
that involve formals of the associated primitive subprogram should be
treated using the "(notional) formal derived type" rules.  In particular,
calls that are tag-indeterminate (for example, "F(G)") should not be mapped
to call the corresponding primitives of the derived type (they should still
call the primitives of the ancestor type).  The fix for this involves a new
predicate function that recursively traverses calls to determine the calls
that satisfy the criteria for mapping.  These changes also completely remove
the mapping of formals that was done in Contracts.Merge_Class_Conditions
(in Inherit_Condition), since the mapping will be done later anyway by
Build_Class_Wide_Expression, and the earlier mapping interferes with that.

Note: The utility function Sem_Util.Check_Parents is no longer called
after removal of the single call to it from contracts.adb, but it's being
retained (along with the generic subprograms in Atree that it depends on)
for possible use in VAST.

gcc/ada/ChangeLog:

        * contracts.adb (Inherit_Condition): Remove Assoc_List and its uses
        along with function Check_Condition, since mapping of formals will
        effectively be done in Build_Class_Wide_Expression (by Replace_Entity).
        * exp_util.adb (Replace_Entity): Only rewrite entity references in
        function calls that qualify according to the result of calling the
        new function Call_To_Parent_Dispatching_Op_Must_Be_Mapped.
        (Call_To_Parent_Dispatching_Op_Must_Be_Mapped): New function that
        determines whether a function call to a primitive of Par_Subp
        associated tagged type needs to be mapped (according to whether
        it has any actuals that reference controlling formals of the
        primitive).

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/contracts.adb | 103 ++++----------------------------------
 gcc/ada/exp_util.adb  | 113 +++++++++++++++++++++++++++++++++++++++++-
 2 files changed, 121 insertions(+), 95 deletions(-)

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 810458a7d9b..70e94874a23 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -4399,10 +4399,10 @@ package body Contracts is
          Seen    : Subprogram_List (Subps'Range) := (others => Empty);
 
          function Inherit_Condition
-           (Par_Subp : Entity_Id;
-            Subp     : Entity_Id) return Node_Id;
-         --  Inherit the class-wide condition from Par_Subp to Subp and adjust
-         --  all the references to formals in the inherited condition.
+           (Par_Subp : Entity_Id) return Node_Id;
+         --  Inherit the class-wide condition from Par_Subp. Simply makes
+         --  a copy of the condition in preparation for later mapping of
+         --  referenced formals and functions by Build_Class_Wide_Expression.
 
          procedure Merge_Conditions (From : Node_Id; Into : Node_Id);
          --  Merge two class-wide preconditions or postconditions (the former
@@ -4417,92 +4417,11 @@ package body Contracts is
          -----------------------
 
          function Inherit_Condition
-           (Par_Subp : Entity_Id;
-            Subp     : Entity_Id) return Node_Id
-         is
-            function Check_Condition (Expr : Node_Id) return Boolean;
-            --  Used in assertion to check that Expr has no reference to the
-            --  formals of Par_Subp.
-
-            ---------------------
-            -- Check_Condition --
-            ---------------------
-
-            function Check_Condition (Expr : Node_Id) return Boolean is
-               Par_Formal_Id : Entity_Id;
-
-               function Check_Entity (N : Node_Id) return Traverse_Result;
-               --  Check occurrence of Par_Formal_Id
-
-               ------------------
-               -- Check_Entity --
-               ------------------
-
-               function Check_Entity (N : Node_Id) return Traverse_Result is
-               begin
-                  if Nkind (N) = N_Identifier
-                    and then Present (Entity (N))
-                    and then Entity (N) = Par_Formal_Id
-                  then
-                     return Abandon;
-                  end if;
-
-                  return OK;
-               end Check_Entity;
-
-               function Check_Expression is new Traverse_Func (Check_Entity);
-
-            --  Start of processing for Check_Condition
-
-            begin
-               Par_Formal_Id := First_Formal (Par_Subp);
-
-               while Present (Par_Formal_Id) loop
-                  if Check_Expression (Expr) = Abandon then
-                     return False;
-                  end if;
-
-                  Next_Formal (Par_Formal_Id);
-               end loop;
-
-               return True;
-            end Check_Condition;
-
-            --  Local variables
-
-            Assoc_List     : constant Elist_Id := New_Elmt_List;
-            Par_Formal_Id  : Entity_Id := First_Formal (Par_Subp);
-            Subp_Formal_Id : Entity_Id := First_Formal (Subp);
-            New_Condition  : Node_Id;
-
+           (Par_Subp : Entity_Id) return Node_Id is
          begin
-            while Present (Par_Formal_Id) loop
-               Append_Elmt (Par_Formal_Id,  Assoc_List);
-               Append_Elmt (Subp_Formal_Id, Assoc_List);
-
-               Next_Formal (Par_Formal_Id);
-               Next_Formal (Subp_Formal_Id);
-            end loop;
-
-            --  Check that Parent field of all the nodes have their correct
-            --  decoration; required because otherwise mapped nodes with
-            --  wrong Parent field are left unmodified in the copied tree
-            --  and cause reporting wrong errors at later stages.
-
-            pragma Assert
-              (Check_Parents (Class_Condition (Kind, Par_Subp), Assoc_List));
-
-            New_Condition :=
+            return
               New_Copy_Tree
-                (Source => Class_Condition (Kind, Par_Subp),
-                 Map    => Assoc_List);
-
-            --  Ensure that the inherited condition has no reference to the
-            --  formals of the parent subprogram.
-
-            pragma Assert (Check_Condition (New_Condition));
-
-            return New_Condition;
+                (Source => Class_Condition (Kind, Par_Subp));
          end Inherit_Condition;
 
          ----------------------
@@ -4616,9 +4535,7 @@ package body Contracts is
                   Par_Prim        := Subp_Id;
                   Par_Iface_Prims := Covered_Interface_Primitives (Par_Prim);
 
-                  Cond := Inherit_Condition
-                            (Subp     => Spec_Id,
-                             Par_Subp => Subp_Id);
+                  Cond := Inherit_Condition (Par_Subp => Subp_Id);
 
                   if Present (Class_Cond) then
                      Merge_Conditions (Cond, Class_Cond);
@@ -4662,9 +4579,7 @@ package body Contracts is
                then
                   Seen (Index) := Subp_Id;
 
-                  Cond := Inherit_Condition
-                            (Subp     => Spec_Id,
-                             Par_Subp => Subp_Id);
+                  Cond := Inherit_Condition (Par_Subp => Subp_Id);
 
                   Check_Class_Condition
                     (Cond            => Cond,
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 028ee01873b..b76d387c5a5 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1523,7 +1523,118 @@ package body Exp_Util is
             New_E := Type_Map.Get (Entity (N));
 
             if Present (New_E) then
-               Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
+               declare
+
+                  Ctrl_Type : constant Entity_Id
+                    := Find_Dispatching_Type (Par_Subp);
+
+                  function Call_To_Parent_Dispatching_Op_Must_Be_Mapped
+                    (Call_Node : Node_Id) return Boolean;
+                  --  If Call_Node is a call to a primitive function F of the
+                  --  tagged type T associated with Par_Subp that either has
+                  --  any actuals that are controlling formals of Par_Subp,
+                  --  or else the call to F is an actual parameter of an
+                  --  enclosing call to a primitive of T that has any actuals
+                  --  that are controlling formals of Par_Subp (and recursively
+                  --  up the tree of enclosing function calls), returns True;
+                  --  otherwise returns False. Returning True implies that the
+                  --  call to F must be mapped to a call that instead targets
+                  --  the corresponding function F of the tagged type for which
+                  --  Subp is a primitive function.
+
+                  --------------------------------------------------
+                  -- Call_To_Parent_Dispatching_Op_Must_Be_Mapped --
+                  --------------------------------------------------
+
+                  function Call_To_Parent_Dispatching_Op_Must_Be_Mapped
+                    (Call_Node : Node_Id) return Boolean
+                  is
+                     pragma Assert (Nkind (Call_Node) = N_Function_Call);
+
+                     Actual           : Node_Id := First_Actual (Call_Node);
+                     Actual_Type      : Entity_Id;
+                     Actual_Or_Prefix : Node_Id;
+
+                  begin
+                     if Is_Entity_Name (Name (Call_Node))
+                       and then Is_Dispatching_Operation
+                                  (Entity (Name (Call_Node)))
+                       and then
+                            Is_Ancestor
+                              (Ctrl_Type,
+                               Find_Dispatching_Type
+                                 (Entity (Name (Call_Node))))
+                     then
+                        while Present (Actual) loop
+
+                           --  Account for 'Old and explicit dereferences,
+                           --  picking up the prefix object in those cases.
+
+                           if (Nkind (Actual) = N_Attribute_Reference
+                                and then Attribute_Name (Actual) = Name_Old)
+                             or else Nkind (Actual) = N_Explicit_Dereference
+                           then
+                              Actual_Or_Prefix := Prefix (Actual);
+                           else
+                              Actual_Or_Prefix := Actual;
+                           end if;
+
+                           Actual_Type := Etype (Actual);
+
+                           if Is_Anonymous_Access_Type (Actual_Type) then
+                              Actual_Type := Designated_Type (Actual_Type);
+                           end if;
+
+                           if Nkind (Actual_Or_Prefix)
+                                in N_Identifier
+                                 | N_Expanded_Name
+                                 | N_Operator_Symbol
+
+                             and then Is_Formal (Entity (Actual_Or_Prefix))
+
+                             and then Covers (Ctrl_Type, Actual_Type)
+                           then
+                              --  At least one actual is a formal parameter of
+                              --  Par_Subp with type Ctrl_Type.
+
+                              return True;
+                           end if;
+
+                           Next_Actual (Actual);
+                        end loop;
+
+                        if Nkind (Parent (Call_Node)) = N_Function_Call then
+                           return
+                             Call_To_Parent_Dispatching_Op_Must_Be_Mapped
+                               (Parent (Call_Node));
+                        end if;
+
+                        return False;
+
+                     else
+                        return False;
+                     end if;
+                  end Call_To_Parent_Dispatching_Op_Must_Be_Mapped;
+
+               begin
+                  --  If N's entity is in the map, then the entity is either
+                  --  a formal of the parent subprogram that should necessarily
+                  --  be mapped, or it's a function call's target entity that
+                  --  that should be mapped if the call involves any actuals
+                  --  that reference formals of the parent subprogram (or the
+                  --  function call is part of an enclosing call that similarly
+                  --  qualifies for mapping). Rewrite a node that references
+                  --  any such qualified entity to a new node referencing the
+                  --  corresponding entity associated with the derived type.
+
+                  if not Is_Subprogram (Entity (N))
+                    or else Nkind (Parent (N)) /= N_Function_Call
+                    or else
+                      Call_To_Parent_Dispatching_Op_Must_Be_Mapped (Parent (N))
+                  then
+                     Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
+                  end if;
+               end;
             end if;
 
             --  Update type of function call node, which should be the same as
-- 
2.43.0

Reply via email to