[gcc r12-5733] [Ada] Enable expansion of dispatching equality for GNATprove

[gcc r12-5733] [Ada] Enable expansion of dispatching equality for GNATprove

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:eca89ac6e73026a8606e05e6f0486f963c02c4bc

commit r12-5733-geca89ac6e73026a8606e05e6f0486f963c02c4bc
Author: Piotr Trojanek <trojanek@adacore.com>
Date:   Mon Nov 22 19:01:33 2021 +0100

    [Ada] Enable expansion of dispatching equality for GNATprove
    
    gcc/ada/
    
            * exp_ch13.ads (Expand_N_Freeze_Entity): Add note about a SPARK
            twin.
            * exp_ch3.ads (Freeze_Type): Likewise.
            * exp_spark.adb (Expand_SPARK_N_Freeze_Entity): Mimic what is
            done in Freeze_Entity.
            (SPARK_Freeze_Type): Mimic what is done in Freeze_Type; add call
            to Make_Predefined_Primitive_Eq_Spec.

Diff:
---
 gcc/ada/exp_ch13.ads  |   3 +
 gcc/ada/exp_ch3.ads   |   3 +
 gcc/ada/exp_spark.adb | 289 +++++++++++++++++++++++++++++++++++++++++++++++---
 3 files changed, 280 insertions(+), 15 deletions(-)

diff --git a/gcc/ada/exp_ch13.ads b/gcc/ada/exp_ch13.ads
index 1c5301dca1d..f5dcfe097e2 100644
--- a/gcc/ada/exp_ch13.ads
+++ b/gcc/ada/exp_ch13.ads
@@ -32,6 +32,9 @@ package Exp_Ch13 is
    procedure Expand_N_Attribute_Definition_Clause  (N : Node_Id);
    procedure Expand_N_Free_Statement               (N : Node_Id);
    procedure Expand_N_Freeze_Entity                (N : Node_Id);
+   --  Note: for GNATprove we have a minimal variant of this routine in
+   --  Exp_SPARK.Expand_SPARK_N_Freeze_Entity. They need to be kept in sync.
+
    procedure Expand_N_Record_Representation_Clause (N : Node_Id);
 
 end Exp_Ch13;
diff --git a/gcc/ada/exp_ch3.ads b/gcc/ada/exp_ch3.ads
index 61595eba8bd..c7648e6f419 100644
--- a/gcc/ada/exp_ch3.ads
+++ b/gcc/ada/exp_ch3.ads
@@ -114,6 +114,9 @@ package Exp_Ch3 is
    --  delete the node if it is present just for front end purpose and we don't
    --  want Gigi to see the node. This function can't delete the node itself
    --  since it would confuse any remaining processing of the freeze node.
+   --
+   --  Note: for GNATprove we have a minimal variant of this routine in
+   --  Exp_SPARK.SPARK_Freeze_Type. They need to be kept in sync.
 
    function Get_Simple_Init_Val
      (Typ  : Entity_Id;
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index bce745b2690..84927f8509c 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -29,15 +29,22 @@ with Einfo;          use Einfo;
 with Einfo.Entities; use Einfo.Entities;
 with Einfo.Utils;    use Einfo.Utils;
 with Exp_Attr;
+with Exp_Ch3;
 with Exp_Ch4;
 with Exp_Ch5;        use Exp_Ch5;
 with Exp_Dbug;       use Exp_Dbug;
 with Exp_Util;       use Exp_Util;
+with Ghost;          use Ghost;
 with Namet;          use Namet;
 with Nlists;         use Nlists;
 with Nmake;          use Nmake;
+with Opt;            use Opt;
+with Restrict;       use Restrict;
+with Rident;         use Rident;
 with Rtsfind;        use Rtsfind;
 with Sem;            use Sem;
+with Sem_Aux;        use Sem_Aux;
+with Sem_Ch7;        use Sem_Ch7;
 with Sem_Ch8;        use Sem_Ch8;
 with Sem_Prag;       use Sem_Prag;
 with Sem_Res;        use Sem_Res;
@@ -62,8 +69,10 @@ package body Exp_SPARK is
    procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id);
    --  Perform delta-aggregate-specific expansion
 
-   procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id);
-   --  Build the DIC procedure of a type when needed, if not already done
+   procedure Expand_SPARK_N_Freeze_Entity (N : Node_Id);
+   --  Do a minimal expansion of freeze entities required by GNATprove. It is
+   --  a subset of what is done for GNAT in Exp_Ch13.Expand_N_Freeze_Entity.
+   --  Those two routines should be kept in sync.
 
    procedure Expand_SPARK_N_Loop_Statement (N : Node_Id);
    --  Perform loop-statement-specific expansion
@@ -80,6 +89,20 @@ package body Exp_SPARK is
    procedure Expand_SPARK_Delta_Or_Update (Typ : Entity_Id; Aggr : Node_Id);
    --  Common expansion for attribute Update and delta aggregates
 
+   procedure SPARK_Freeze_Type (N : Node_Id);
+   --  Do a minimal type freezing required by GNATprove. It is a subset of what
+   --  is done for GNAT in Exp_Ch3.Freeze_Type. Those two routines should be
+   --  kept in sync.
+   --
+   --  Currently in freezing we build the spec of dispatching equality. This
+   --  spec is needed to properly resolve references to the equality operator.
+   --  The body is not needed, because proof knows how to directly synthesize a
+   --  logical meaning for it. Also, for tagged types with extension the
+   --  expanded body would compare the _parent component, which is
+   --  intentionally not generated in the GNATprove mode.
+   --
+   --  We build the DIC procedure body here as well.
+
    ------------------
    -- Expand_SPARK --
    ------------------
@@ -140,8 +163,12 @@ package body Exp_SPARK is
             Expand_SPARK_N_Op_Ne (N);
 
          when N_Freeze_Entity =>
+            --  Currently we only expand type freeze entities, so ignore other
+            --  freeze entites, because it is expensive to create a suitable
+            --  freezing environment.
+
             if Is_Type (Entity (N)) then
-               Expand_SPARK_N_Freeze_Type (Entity (N));
+               Expand_SPARK_N_Freeze_Entity (N);
             end if;
 
          --  In SPARK mode, no other constructs require expansion
@@ -350,23 +377,176 @@ package body Exp_SPARK is
       end if;
    end Expand_SPARK_Delta_Or_Update;
 
-   --------------------------------
-   -- Expand_SPARK_N_Freeze_Type --
-   --------------------------------
+   ----------------------------------
+   -- Expand_SPARK_N_Freeze_Entity --
+   ----------------------------------
+
+   procedure Expand_SPARK_N_Freeze_Entity (N : Entity_Id) is
+      E : constant Entity_Id := Entity (N);
+
+      Action         : Node_Id;
+      E_Scope        : Entity_Id;
+      In_Other_Scope : Boolean;
+      In_Outer_Scope : Boolean;
 
-   procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id) is
    begin
-      --  When a DIC is inherited by a tagged type, it may need to be
-      --  specialized to the descendant type, hence build a separate DIC
-      --  procedure for it as done during regular expansion for compilation.
+      --  Here E is a type or a subprogram
 
-      if Has_DIC (E) and then Is_Tagged_Type (E) then
-         --  Why is this needed for DIC, but not for other aspects (such as
-         --  Type_Invariant)???
+      E_Scope := Scope (E);
+
+      --  This is an error protection against previous errors
+
+      if No (E_Scope) then
+         Check_Error_Detected;
+         return;
+      end if;
+
+      --  The entity may be a subtype declared for a constrained record
+      --  component, in which case the relevant scope is the scope of
+      --  the record. This happens for class-wide subtypes created for
+      --  a constrained type extension with inherited discriminants.
+
+      if Is_Type (E_Scope)
+        and then not Is_Concurrent_Type (E_Scope)
+      then
+         E_Scope := Scope (E_Scope);
+
+      --  The entity may be a subtype declared for an iterator
+
+      elsif Ekind (E_Scope) = E_Loop then
+         E_Scope := Scope (E_Scope);
+      end if;
+
+      --  If we are freezing entities defined in protected types, they belong
+      --  in the enclosing scope, given that the original type has been
+      --  expanded away. The same is true for entities in task types, in
+      --  particular the parameter records of entries (Entities in bodies are
+      --  all frozen within the body). If we are in the task body, this is a
+      --  proper scope. If we are within a subprogram body, the proper scope
+      --  is the corresponding spec. This may happen for itypes generated in
+      --  the bodies of protected operations.
+
+      if Ekind (E_Scope) = E_Protected_Type
+        or else (Ekind (E_Scope) = E_Task_Type
+                  and then not Has_Completion (E_Scope))
+      then
+         E_Scope := Scope (E_Scope);
 
-         Build_DIC_Procedure_Body (E);
+      elsif Ekind (E_Scope) = E_Subprogram_Body then
+         E_Scope := Corresponding_Spec (Unit_Declaration_Node (E_Scope));
       end if;
-   end Expand_SPARK_N_Freeze_Type;
+
+      --  If the scope of the entity is in open scopes, it is the current one
+      --  or an enclosing one, including a loop, a block, or a subprogram.
+
+      if In_Open_Scopes (E_Scope) then
+         In_Other_Scope := False;
+         In_Outer_Scope := E_Scope /= Current_Scope;
+
+      --  Otherwise it is a local package or a different compilation unit
+
+      else
+         In_Other_Scope := True;
+         In_Outer_Scope := False;
+      end if;
+
+      --  If the entity being frozen is defined in a scope that is not
+      --  currently on the scope stack, we must establish the proper
+      --  visibility before freezing the entity and related subprograms.
+
+      if In_Other_Scope then
+         Push_Scope (E_Scope);
+
+         --  Finalizers are little odd in terms of freezing. The spec of the
+         --  procedure appears in the declarations while the body appears in
+         --  the statement part of a single construct. Since the finalizer must
+         --  be called by the At_End handler of the construct, the spec is
+         --  manually frozen right after its declaration. The only side effect
+         --  of this action appears in contexts where the construct is not in
+         --  its final resting place. These contexts are:
+
+         --    * Entry bodies - The declarations and statements are moved to
+         --      the procedure equivalen of the entry.
+         --    * Protected subprograms - The declarations and statements are
+         --      moved to the non-protected version of the subprogram.
+         --    * Task bodies - The declarations and statements are moved to the
+         --      task body procedure.
+         --    * Blocks that will be rewritten as subprograms when unnesting
+         --      is in effect.
+
+         --  Visible declarations do not need to be installed in these three
+         --  cases since it does not make semantic sense to do so. All entities
+         --  referenced by a finalizer are visible and already resolved, plus
+         --  the enclosing scope may not have visible declarations at all.
+
+         if Ekind (E) = E_Procedure
+           and then Is_Finalizer (E)
+           and then
+             (Is_Entry (E_Scope)
+                or else (Is_Subprogram (E_Scope)
+                          and then Is_Protected_Type (Scope (E_Scope)))
+                or else Is_Task_Type (E_Scope)
+                or else Ekind (E_Scope) = E_Block)
+         then
+            null;
+         else
+            Install_Visible_Declarations (E_Scope);
+         end if;
+
+         if Is_Concurrent_Type (E_Scope)
+           or else Is_Package_Or_Generic_Package (E_Scope)
+         then
+            Install_Private_Declarations (E_Scope);
+         end if;
+
+      --  If the entity is in an outer scope, then that scope needs to
+      --  temporarily become the current scope so that operations created
+      --  during type freezing will be declared in the right scope and
+      --  can properly override any corresponding inherited operations.
+
+      elsif In_Outer_Scope then
+         Push_Scope (E_Scope);
+      end if;
+
+      --  Remember that we are processing a freezing entity and its freezing
+      --  nodes. This flag (non-zero = set) is used to avoid the need of
+      --  climbing through the tree while processing the freezing actions (ie.
+      --  to avoid generating spurious warnings or to avoid killing constant
+      --  indications while processing the code associated with freezing
+      --  actions). We use a counter to deal with nesting.
+
+      Inside_Freezing_Actions := Inside_Freezing_Actions + 1;
+
+      --  Currently only types require freezing in SPARK
+
+      SPARK_Freeze_Type (N);
+
+      --  Analyze actions in freeze node, if any
+
+      Action := First (Actions (N));
+      while Present (Action) loop
+         Analyze (Action);
+         Next (Action);
+      end loop;
+
+      --  Pop scope if we installed one for the analysis
+
+      if In_Other_Scope then
+         if Ekind (Current_Scope) = E_Package then
+            End_Package_Scope (E_Scope);
+         else
+            End_Scope;
+         end if;
+
+      elsif In_Outer_Scope then
+         Pop_Scope;
+      end if;
+
+      --  Restore previous value of the nesting-level counter that records
+      --  whether we are inside a (possibly nested) call to this procedure.
+
+      Inside_Freezing_Actions := Inside_Freezing_Actions - 1;
+   end Expand_SPARK_N_Freeze_Entity;
 
    ----------------------------------------
    -- Expand_SPARK_N_Attribute_Reference --
@@ -705,4 +885,83 @@ package body Exp_SPARK is
       end if;
    end Expand_SPARK_Potential_Renaming;
 
+   -----------------------
+   -- SPARK_Freeze_Type --
+   -----------------------
+
+   procedure SPARK_Freeze_Type (N : Entity_Id) is
+      Typ : constant Entity_Id := Entity (N);
+
+      Renamed_Eq : Node_Id;
+      --  Defining unit name for the predefined equality function in the case
+      --  where the type has a primitive operation that is a renaming of
+      --  predefined equality (but only if there is also an overriding
+      --  user-defined equality function). Used to pass this entity from
+      --  Make_Predefined_Primitive_Specs to Predefined_Primitive_Bodies.
+
+      Decl        : Node_Id;
+      Eq_Spec     : Node_Id := Empty;
+      Predef_List : List_Id;
+
+      Saved_GM  : constant Ghost_Mode_Type := Ghost_Mode;
+      Saved_IGR : constant Node_Id         := Ignored_Ghost_Region;
+      --  Save the Ghost-related attributes to restore on exit
+
+   begin
+      --  The type being frozen may be subject to pragma Ghost. Set the mode
+      --  now to ensure that any nodes generated during freezing are properly
+      --  marked as Ghost.
+
+      Set_Ghost_Mode (Typ);
+
+      --  When a DIC is inherited by a tagged type, it may need to be
+      --  specialized to the descendant type, hence build a separate DIC
+      --  procedure for it as done during regular expansion for compilation.
+
+      if Has_DIC (Typ) and then Is_Tagged_Type (Typ) then
+         --  Why is this needed for DIC, but not for other aspects (such as
+         --  Type_Invariant)???
+
+         Build_DIC_Procedure_Body (Typ);
+      end if;
+
+      if Ekind (Typ) = E_Record_Type
+        and then Is_Tagged_Type (Typ)
+        and then not Is_Interface (Typ)
+        and then not Is_Limited_Type (Typ)
+      then
+         if Is_CPP_Class (Root_Type (Typ))
+           and then Convention (Typ) = Convention_CPP
+         then
+            null;
+
+         --  Do not add the spec of the predefined primitives if we are
+         --  compiling under restriction No_Dispatching_Calls.
+
+         elsif not Restriction_Active (No_Dispatching_Calls) then
+            Set_Is_Frozen (Typ, False);
+
+            Predef_List := New_List;
+            Exp_Ch3.Make_Predefined_Primitive_Eq_Spec
+              (Typ, Predef_List, Renamed_Eq);
+            Eq_Spec := First (Predef_List);
+            Insert_List_Before_And_Analyze (N, Predef_List);
+
+            Set_Is_Frozen (Typ);
+
+            --  Remove link from the parent list to the spec and body of
+            --  the dispatching equality, but keep the link in the opposite
+            --  direction, to allow up-traversal of the AST.
+
+            if Present (Eq_Spec) then
+               Decl := Parent (Eq_Spec);
+               Remove (Eq_Spec);
+               Set_Parent (Eq_Spec, Decl);
+            end if;
+         end if;
+      end if;
+
+      Restore_Ghost_Region (Saved_GM, Saved_IGR);
+   end SPARK_Freeze_Type;
+
 end Exp_SPARK;