@@ -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;
@@ -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;
@@ -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;