diff mbox series

[Ada] Enable expansion of dispatching equality for GNATprove

Message ID 20211202162852.GA2159459@adacore.com
State Committed
Headers show
Series [Ada] Enable expansion of dispatching equality for GNATprove | expand

Commit Message

Pierre-Marie de Rodat Dec. 2, 2021, 4:28 p.m. UTC
For GNAT the dispatching equality is generated in expansion of freezing
nodes. For GNATprove this expansion needs to be specifically enabled and
must occur in a carefully setup context.

Previously type freezing for GNATprove only involved building of the DIC
procedure, which didn't require much context. Now freezing also involves
the dispatching equality, which must be analyzed in a full context with
a proper visibility (as otherwise the generated equality will duplicate
the one created when a type is derived).

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

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 mbox series

Patch

diff --git a/gcc/ada/exp_ch13.ads b/gcc/ada/exp_ch13.ads
--- 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
--- 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
--- 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;