[Ada] Support for new aspect Subprogram_Variant on recursive subprograms

gcc/ada/

	* aspects.ads: Introduce Subprogram_Variant aspect with the
	following properties: GNAT-specific, with mandatory expression,
	not a representation aspect, never delayed.
	* contracts.adb (Expand_Subprogram_Contract): Mention new aspect
	in the comment.
	(Add_Contract_Item): Support addition of pragma
	Subprogram_Variant to N_Contract node.
	(Analyze_Entry_Or_Subprogram_Contract): Mention new aspect in
	the comment; add pragma Subprogram_Variant to N_Contract node.
	(Build_Postconditions_Procedure): Adapt call to
	Insert_Before_First_Source_Declaration, which is now reused in
	expansion of new aspect.
	(Process_Contract_Cases_For): Also process Subprogram_Variant,
	which is stored in N_Contract node together with Contract_Cases.
	* contracts.ads (Analyze_Entry_Or_Subprogram_Contract): Mention
	new aspect in the comment.
	(Analyze_Entry_Or_Subprogram_Body_Contract): Likewise.
	* einfo.adb (Get_Pragma): Support retrieval of new pragma.
	* einfo.ads (Get_Pragma): Likewise.
	* exp_ch6.adb (Check_Subprogram_Variant): New routine for
	emitting call to check Subprogram_Variant expressions at run
	time.
	(Expand_Call_Helper): Check Subprogram_Variant expressions at
	recursive calls.
	* exp_prag.adb (Make_Op): Moved from expansion of pragma
	Loop_Variant to Exp_Util, so it is now reused for expansion of
	pragma Subprogram_Variant.
	(Process_Variant): Adapt call to Make_Op after moving it to
	Exp_Util.
	(Expand_Pragma_Subprogram_Variant): New routine.
	* exp_prag.ads (Expand_Pragma_Subprogram_Variant): Likewise.
	* exp_util.adb (Make_Variant_Comparison): Moved from Exp_Prag
	(see above).
	* exp_util.ads (Make_Variant_Comparison): Likewise.
	* inline.adb (Remove_Aspects_And_Pragmas): Handle aspect/pragma
	Subprogram_Variant just like similar contracts.
	* par-prag.adb (Prag): Likewise.
	* sem.adb (Insert_Before_First_Source_Declaration): Moved from
	Contracts (see above).
	* sem.ads (Insert_Before_First_Source_Declaration): Likewise.
	* sem_ch12.adb: Mention new aspect in the comment about
	"Implementation of Generic Contracts", just like similar aspects
	are mentioned there.
	* sem_ch13.adb (Insert_Pragma): Mention new aspect in the
	comment, because this routine is now used for Subprogram_Variant
	just like for other similar aspects.
	(Analyze_Aspect_Specifications): Mention new aspect in comments;
	it is handled just like aspect Contract_Cases.
	(Check_Aspect_At_Freeze_Point): Do not expect aspect
	Subprogram_Variant just like we don't expect aspect
	Contract_Cases.
	* sem_prag.adb (Ensure_Aggregate_Form): Now also used for pragma
	Subprogram_Variant, so update comment.
	(Analyze_Pragma): Add initial checks for pragma
	Subprogram_Variant.
	(Analyze_Subprogram_Variant_In_Decl_Part): New routine with
	secondary checks on the new pragma.
	(Sig_Flags): Handle references within pragma Subprogram_Variant
	expression just like references in similar pragma
	Contract_Cases.
	(Is_Valid_Assertion_Kind): Handle Subprogram_Variant just like
	other similar contracts.
	* sem_prag.ads (Analyze_Subprogram_Variant_In_Decl_Part): New
	routine.
	* sem_res.adb (Same_Or_Aliased_Subprograms): Moved to Sem_Util,
	so it can be reused for detection of recursive calls where
	Subprogram_Variant needs to be verified.
	* sem_util.adb (Is_Subprogram_Contract_Annotation): Handle new
	Subprogram_Variant annotation just like other similar
	annotations.
	(Same_Or_Aliased_Subprograms): Moved from Sem_Res (see above).
	* sem_util.ads (Is_Subprogram_Contract_Annotation): Mention new
	aspect in the comment.
	(Same_Or_Aliased_Subprograms): Moved from Sem_Res (see above).
	* sinfo.ads (N_Contract): Document handling of
	Subprogram_Variant.
	* snames.ads-tmpl: Add name for the internally generated
	procedure with checks for Subprogram_Variant expression, name
	for the new aspect and new pragma corresponding to aspect
	Subprogram_Variant.
This commit is contained in:
Piotr Trojanek 2020-07-13 12:42:18 +02:00 committed by Pierre-Marie de Rodat
parent 87eb6d2c2a
commit afa1ffd42c
23 changed files with 845 additions and 130 deletions

View File

@ -153,6 +153,7 @@ package Aspects is
Aspect_Storage_Size,
Aspect_Stream_Size,
Aspect_String_Literal,
Aspect_Subprogram_Variant, -- GNAT
Aspect_Suppress,
Aspect_Synchronization,
Aspect_Test_Case, -- GNAT
@ -426,6 +427,7 @@ package Aspects is
Aspect_Storage_Size => Expression,
Aspect_Stream_Size => Expression,
Aspect_String_Literal => Name,
Aspect_Subprogram_Variant => Expression,
Aspect_Suppress => Name,
Aspect_Synchronization => Name,
Aspect_Test_Case => Expression,
@ -526,6 +528,7 @@ package Aspects is
Aspect_Storage_Size => True,
Aspect_Stream_Size => True,
Aspect_String_Literal => False,
Aspect_Subprogram_Variant => False,
Aspect_Suppress => False,
Aspect_Synchronization => False,
Aspect_Test_Case => False,
@ -700,6 +703,7 @@ package Aspects is
Aspect_Storage_Size => Name_Storage_Size,
Aspect_Stream_Size => Name_Stream_Size,
Aspect_String_Literal => Name_String_Literal,
Aspect_Subprogram_Variant => Name_Subprogram_Variant,
Aspect_Suppress => Name_Suppress,
Aspect_Suppress_Debug_Info => Name_Suppress_Debug_Info,
Aspect_Suppress_Initialization => Name_Suppress_Initialization,
@ -955,6 +959,7 @@ package Aspects is
Aspect_Relaxed_Initialization => Never_Delay,
Aspect_SPARK_Mode => Never_Delay,
Aspect_Static => Never_Delay,
Aspect_Subprogram_Variant => Never_Delay,
Aspect_Synchronization => Never_Delay,
Aspect_Test_Case => Never_Delay,
Aspect_Unimplemented => Never_Delay,

View File

@ -69,8 +69,8 @@ package body Contracts is
procedure Expand_Subprogram_Contract (Body_Id : Entity_Id);
-- Expand the contracts of a subprogram body and its correspoding spec (if
-- any). This routine processes all [refined] pre- and postconditions as
-- well as Contract_Cases, invariants and predicates. Body_Id denotes the
-- entity of the subprogram body.
-- well as Contract_Cases, Subprogram_Variant, invariants and predicates.
-- Body_Id denotes the entity of the subprogram body.
-----------------------
-- Add_Contract_Item --
@ -200,7 +200,10 @@ package body Contracts is
then
Add_Classification;
elsif Prag_Nam in Name_Contract_Cases | Name_Test_Case then
elsif Prag_Nam in Name_Contract_Cases
| Name_Subprogram_Variant
| Name_Test_Case
then
Add_Contract_Test_Case;
elsif Prag_Nam in Name_Postcondition | Name_Precondition then
@ -550,8 +553,8 @@ package body Contracts is
end if;
-- Deal with preconditions, [refined] postconditions, Contract_Cases,
-- invariants and predicates associated with body and its spec. Do not
-- expand the contract of subprogram body stubs.
-- Subprogram_Variant, invariants and predicates associated with body
-- and its spec. Do not expand the contract of subprogram body stubs.
if Nkind (Body_Decl) = N_Subprogram_Body then
Expand_Subprogram_Contract (Body_Id);
@ -686,6 +689,10 @@ package body Contracts is
else
Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id);
end if;
elsif Prag_Nam = Name_Subprogram_Variant then
Analyze_Subprogram_Variant_In_Decl_Part (Prag);
else
pragma Assert (Prag_Nam = Name_Test_Case);
Analyze_Test_Case_In_Decl_Part (Prag);
@ -1941,49 +1948,6 @@ package body Contracts is
Stmts : List_Id;
Result : Entity_Id)
is
procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id);
-- Insert node Stmt before the first source declaration of the
-- related subprogram's body. If no such declaration exists, Stmt
-- becomes the last declaration.
--------------------------------------------
-- Insert_Before_First_Source_Declaration --
--------------------------------------------
procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is
Decls : constant List_Id := Declarations (Body_Decl);
Decl : Node_Id;
begin
-- Inspect the declarations of the related subprogram body looking
-- for the first source declaration.
if Present (Decls) then
Decl := First (Decls);
while Present (Decl) loop
if Comes_From_Source (Decl) then
Insert_Before (Decl, Stmt);
return;
end if;
Next (Decl);
end loop;
-- If we get there, then the subprogram body lacks any source
-- declarations. The body of _Postconditions now acts as the
-- last declaration.
Append (Stmt, Decls);
-- Ensure that the body has a declaration list
else
Set_Declarations (Body_Decl, New_List (Stmt));
end if;
end Insert_Before_First_Source_Declaration;
-- Local variables
Loc : constant Source_Ptr := Sloc (Body_Decl);
Params : List_Id := No_List;
Proc_Bod : Node_Id;
@ -1991,8 +1955,6 @@ package body Contracts is
Proc_Id : Entity_Id;
Proc_Spec : Node_Id;
-- Start of processing for Build_Postconditions_Procedure
begin
-- Nothing to do if there are no actions to check on exit
@ -2051,7 +2013,8 @@ package body Contracts is
-- order reference. The body of _Postconditions must be placed after
-- the declaration of Temp to preserve correct visibility.
Insert_Before_First_Source_Declaration (Proc_Decl);
Insert_Before_First_Source_Declaration
(Proc_Decl, Declarations (Body_Decl));
Analyze (Proc_Decl);
-- Set an explicit End_Label to override the sloc of the implicit
@ -2092,14 +2055,20 @@ package body Contracts is
if Present (Items) then
Prag := Contract_Test_Cases (Items);
while Present (Prag) loop
if Pragma_Name (Prag) = Name_Contract_Cases
and then Is_Checked (Prag)
then
if Is_Checked (Prag) then
if Pragma_Name (Prag) = Name_Contract_Cases then
Expand_Pragma_Contract_Cases
(CCs => Prag,
Subp_Id => Subp_Id,
Decls => Declarations (Body_Decl),
Stmts => Stmts);
elsif Pragma_Name (Prag) = Name_Subprogram_Variant then
Expand_Pragma_Subprogram_Variant
(Prag => Prag,
Subp_Id => Subp_Id,
Body_Decls => Declarations (Body_Decl));
end if;
end if;
Prag := Next_Pragma (Prag);

View File

@ -77,6 +77,7 @@ package Contracts is
-- Refined_Depends
-- Refined_Global
-- Refined_Post
-- Subprogram_Variant (stand alone subprogram body)
-- Test_Case (stand alone subprogram body)
procedure Analyze_Entry_Or_Subprogram_Contract
@ -91,6 +92,7 @@ package Contracts is
-- Global
-- Postcondition
-- Precondition
-- Subprogram_Variant
-- Test_Case
--
-- Freeze_Id is the entity of a [generic] package body or a [generic]

View File

@ -7660,10 +7660,11 @@ package body Einfo is
Id = Pragma_Refined_State or else
Id = Pragma_Volatile_Function;
-- Contract / test case pragmas
-- Contract / subprogram variant / test case pragmas
Is_CTC : constant Boolean :=
Id = Pragma_Contract_Cases or else
Id = Pragma_Subprogram_Variant or else
Id = Pragma_Test_Case;
-- Pre / postcondition pragmas

View File

@ -8521,6 +8521,7 @@ package Einfo is
-- Refined_Global
-- Refined_Post
-- Refined_State
-- Subprogram_Variant
-- Test_Case
-- Volatile_Function

View File

@ -2800,6 +2800,10 @@ package body Exp_Ch6 is
-- though useless predicate checks will be generally removed by
-- back-end optimizations.
procedure Check_Subprogram_Variant;
-- Emit a call to the internally generated procedure with checks for
-- aspect Subprogrgram_Variant, if present and enabled.
function Inherited_From_Formal (S : Entity_Id) return Entity_Id;
-- Within an instance, a type derived from an untagged formal derived
-- type inherits from the original parent, not from the actual. The
@ -3058,6 +3062,37 @@ package body Exp_Ch6 is
end if;
end Can_Fold_Predicate_Call;
------------------------------
-- Check_Subprogram_Variant --
------------------------------
procedure Check_Subprogram_Variant is
Variant_Prag : constant Node_Id :=
Get_Pragma (Current_Scope, Pragma_Subprogram_Variant);
Variant_Proc : Entity_Id;
begin
if Present (Variant_Prag) and then Is_Checked (Variant_Prag) then
-- Analysis of the pragma rewrites its argument with a reference
-- to the internally generated procedure.
Variant_Proc :=
Entity
(Expression
(First
(Pragma_Argument_Associations (Variant_Prag))));
Insert_Action (Call_Node,
Make_Procedure_Call_Statement (Loc,
Name =>
New_Occurrence_Of (Variant_Proc, Loc),
Parameter_Associations =>
New_Copy_List (Parameter_Associations (Call_Node))));
end if;
end Check_Subprogram_Variant;
---------------------------
-- Inherited_From_Formal --
---------------------------
@ -4650,6 +4685,18 @@ package body Exp_Ch6 is
Expand_Actuals (Call_Node, Subp, Post_Call);
-- If it is a recursive call then call the internal procedure that
-- verifies Subprogram_Variant contract (if present and enabled).
-- Detecting calls to subprogram aliases is necessary for recursive
-- calls in instances of generic subprograms, where the renaming of
-- the current subprogram is called.
if Is_Subprogram (Subp)
and then Same_Or_Aliased_Subprograms (Subp, Current_Scope)
then
Check_Subprogram_Variant;
end if;
-- Verify that the actuals do not share storage. This check must be done
-- on the caller side rather that inside the subprogram to avoid issues
-- of parameter passing.

View File

@ -2321,32 +2321,6 @@ package body Exp_Prag is
---------------------
procedure Process_Variant (Variant : Node_Id; Is_Last : Boolean) is
function Make_Op
(Loc : Source_Ptr;
Curr_Val : Node_Id;
Old_Val : Node_Id) return Node_Id;
-- Generate a comparison between Curr_Val and Old_Val depending on
-- the change mode (Increases / Decreases) of the variant.
-------------
-- Make_Op --
-------------
function Make_Op
(Loc : Source_Ptr;
Curr_Val : Node_Id;
Old_Val : Node_Id) return Node_Id
is
begin
if Chars (Variant) = Name_Increases then
return Make_Op_Gt (Loc, Curr_Val, Old_Val);
else pragma Assert (Chars (Variant) = Name_Decreases);
return Make_Op_Lt (Loc, Curr_Val, Old_Val);
end if;
end Make_Op;
-- Local variables
Expr : constant Node_Id := Expression (Variant);
Expr_Typ : constant Entity_Id := Etype (Expr);
Loc : constant Source_Ptr := Sloc (Expr);
@ -2355,8 +2329,6 @@ package body Exp_Prag is
Old_Id : Entity_Id;
Prag : Node_Id;
-- Start of processing for Process_Variant
begin
-- All temporaries generated in this routine must be inserted before
-- the related loop statement. Ensure that the proper scope is on the
@ -2467,7 +2439,8 @@ package body Exp_Prag is
Expression => Make_Identifier (Loc, Name_Loop_Variant)),
Make_Pragma_Argument_Association (Loc,
Expression =>
Make_Op (Loc,
Make_Variant_Comparison (Loc,
Mode => Chars (Variant),
Curr_Val => New_Occurrence_Of (Curr_Id, Loc),
Old_Val => New_Occurrence_Of (Old_Id, Loc)))));
@ -2650,6 +2623,338 @@ package body Exp_Prag is
end if;
end Expand_Pragma_Relative_Deadline;
--------------------------------------
-- Expand_Pragma_Subprogram_Variant --
--------------------------------------
-- Aspect Subprogram_Variant is expanded in the following manner:
-- Original code
-- procedure Proc (Param : T) with
-- with Variant (Increases => Incr_Expr,
-- Decreases => Decr_Expr)
-- <declarations>
-- is
-- <source statements>
-- Proc (New_Param_Value);
-- end Proc;
-- Expanded code
-- procedure Proc (Param : T) is
-- Old_Incr : constant <type of Incr_Expr> := <Incr_Expr>;
-- Old_Decr : constant <type of Decr_Expr> := <Decr_Expr> ;
--
-- procedure Variants (Param : T);
--
-- procedure Variants (Param : T) is
-- Curr_Incr : constant <type of Incr_Expr> := <Incr_Expr>;
-- Curr_Decr : constant <type of Decr_Expr> := <Decr_Expr>;
-- begin
-- if Curr_Incr /= Old_Incr then
-- pragma Check (Variant, Curr_Incr > Old_Incr);
-- else
-- pragma Check (Variant, Curr_Decr < Old_Decr);
-- end if;
-- end Variants;
--
-- <declarations>
-- begin
-- <source statements>
-- Variants (New_Param_Value);
-- Proc (New_Param_Value);
-- end Proc;
procedure Expand_Pragma_Subprogram_Variant
(Prag : Node_Id;
Subp_Id : Node_Id;
Body_Decls : List_Id)
is
Curr_Decls : List_Id;
If_Stmt : Node_Id := Empty;
function Formal_Param_Map
(Old_Subp : Entity_Id;
New_Subp : Entity_Id) return Elist_Id;
-- Given two subprogram entities Old_Subp and New_Subp with the same
-- number of formal parameters return a list of the form:
--
-- old formal 1
-- new formal 1
-- old formal 2
-- new formal 2
-- ...
--
-- as required by New_Copy_Tree to replace references to formal
-- parameters of Old_Subp with references to formal parameters of
-- New_Subp.
procedure Process_Variant
(Variant : Node_Id;
Formal_Map : Elist_Id;
Prev_Decl : in out Node_Id;
Is_Last : Boolean);
-- Process a single increasing / decreasing termination variant given by
-- a component association Variant. Formal_Map is a list of formal
-- parameters of the annotated subprogram and of the internal procedure
-- that verifies the variant in the format required by New_Copy_Tree.
-- The Old_... object created by this routine will be appended after
-- Prev_Decl and is stored in this parameter for a next call to this
-- routine. Is_Last is True when there are no more variants to process.
----------------------
-- Formal_Param_Map --
----------------------
function Formal_Param_Map
(Old_Subp : Entity_Id;
New_Subp : Entity_Id) return Elist_Id
is
Old_Formal : Entity_Id := First_Formal (Old_Subp);
New_Formal : Entity_Id := First_Formal (New_Subp);
Param_Map : Elist_Id;
begin
if Present (Old_Formal) then
Param_Map := New_Elmt_List;
while Present (Old_Formal) and then Present (New_Formal) loop
Append_Elmt (Old_Formal, Param_Map);
Append_Elmt (New_Formal, Param_Map);
Next_Formal (Old_Formal);
Next_Formal (New_Formal);
end loop;
return Param_Map;
else
return No_Elist;
end if;
end Formal_Param_Map;
---------------------
-- Process_Variant --
---------------------
procedure Process_Variant
(Variant : Node_Id;
Formal_Map : Elist_Id;
Prev_Decl : in out Node_Id;
Is_Last : Boolean)
is
Expr : constant Node_Id := Expression (Variant);
Expr_Typ : constant Entity_Id := Etype (Expr);
Loc : constant Source_Ptr := Sloc (Expr);
Old_Id : Entity_Id;
Old_Decl : Node_Id;
Curr_Id : Entity_Id;
Curr_Decl : Node_Id;
Prag : Node_Id;
begin
-- Create temporaries that store the old values of the associated
-- expression.
-- Generate:
-- Old : constant <type of Expr> := <Expr>;
Old_Id := Make_Temporary (Loc, 'P');
Old_Decl :=
Make_Object_Declaration (Loc,
Defining_Identifier => Old_Id,
Constant_Present => True,
Object_Definition => New_Occurrence_Of (Expr_Typ, Loc),
Expression => New_Copy_Tree (Expr));
Insert_After_And_Analyze (Prev_Decl, Old_Decl);
Prev_Decl := Old_Decl;
-- Generate:
-- Curr : constant <type of Expr> := <Expr>;
Curr_Id := Make_Temporary (Loc, 'C');
Curr_Decl :=
Make_Object_Declaration (Loc,
Defining_Identifier => Curr_Id,
Constant_Present => True,
Object_Definition => New_Occurrence_Of (Expr_Typ, Loc),
Expression =>
New_Copy_Tree (Expr, Map => Formal_Map));
Append (Curr_Decl, Curr_Decls);
-- Generate:
-- pragma Check (Variant, Curr <|> Old);
Prag :=
Make_Pragma (Loc,
Chars => Name_Check,
Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
Expression =>
Make_Identifier (Loc,
Name_Subprogram_Variant)),
Make_Pragma_Argument_Association (Loc,
Expression =>
Make_Variant_Comparison (Loc,
Mode => Chars (First (Choices (Variant))),
Curr_Val => New_Occurrence_Of (Curr_Id, Loc),
Old_Val => New_Occurrence_Of (Old_Id, Loc)))));
-- Generate:
-- if Curr /= Old then
-- <Prag>;
if No (If_Stmt) then
-- When there is just one termination variant, do not compare
-- the old and current value for equality, just check the
-- pragma.
if Is_Last then
If_Stmt := Prag;
else
If_Stmt :=
Make_If_Statement (Loc,
Condition =>
Make_Op_Ne (Loc,
Left_Opnd => New_Occurrence_Of (Curr_Id, Loc),
Right_Opnd => New_Occurrence_Of (Old_Id, Loc)),
Then_Statements => New_List (Prag));
end if;
-- Generate:
-- else
-- <Prag>;
-- end if;
elsif Is_Last then
Set_Else_Statements (If_Stmt, New_List (Prag));
-- Generate:
-- elsif Curr /= Old then
-- <Prag>;
else
if Elsif_Parts (If_Stmt) = No_List then
Set_Elsif_Parts (If_Stmt, New_List);
end if;
Append_To (Elsif_Parts (If_Stmt),
Make_Elsif_Part (Loc,
Condition =>
Make_Op_Ne (Loc,
Left_Opnd => New_Occurrence_Of (Curr_Id, Loc),
Right_Opnd => New_Occurrence_Of (Old_Id, Loc)),
Then_Statements => New_List (Prag)));
end if;
end Process_Variant;
-- Local variables
Loc : constant Source_Ptr := Sloc (Prag);
Aggr : Node_Id;
Formal_Map : Elist_Id;
Last : Node_Id;
Last_Variant : Node_Id;
Proc_Bod : Node_Id;
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
Proc_Spec : Node_Id;
Variant : Node_Id;
begin
-- Do nothing if pragma is not present or is disabled
if Is_Ignored (Prag) then
return;
end if;
Aggr := Expression (First (Pragma_Argument_Associations (Prag)));
-- The expansion of Subprogram Variant is quite distributed as it
-- produces various statements to capture and compare the arguments.
-- To preserve the original context, set the Is_Assertion_Expr flag.
-- This aids the Ghost legality checks when verifying the placement
-- of a reference to a Ghost entity.
In_Assertion_Expr := In_Assertion_Expr + 1;
-- Create declaration of the procedure that compares values of the
-- variant expressions captured at the start of subprogram with their
-- values at the recursive call of the subprogram.
Proc_Id := Make_Defining_Identifier (Loc, Name_uVariants);
Proc_Spec :=
Make_Procedure_Specification
(Loc,
Defining_Unit_Name => Proc_Id,
Parameter_Specifications => Copy_Parameter_List (Subp_Id));
Proc_Decl :=
Make_Subprogram_Declaration (Loc, Proc_Spec);
Insert_Before_First_Source_Declaration (Proc_Decl, Body_Decls);
Analyze (Proc_Decl);
-- Create a mapping between formals of the annotated subprogram (which
-- are used to compute values of the variant expression at the start of
-- subprogram) and formals of the internal procedure (which are used to
-- compute values of of the variant expression at the recursive call).
Formal_Map :=
Formal_Param_Map (Old_Subp => Subp_Id, New_Subp => Proc_Id);
-- Process invidual increasing / decreasing variants
Last := Proc_Decl;
Curr_Decls := New_List;
Last_Variant := Nlists.Last (Component_Associations (Aggr));
Variant := First (Component_Associations (Aggr));
while Present (Variant) loop
Process_Variant
(Variant => Variant,
Formal_Map => Formal_Map,
Prev_Decl => Last,
Is_Last => Variant = Last_Variant);
Next (Variant);
end loop;
-- Create a subprogram body with declarations of objects that capture
-- the current values of variant expressions at a recursive call and an
-- if-then-else statement that compares current with old values.
Proc_Bod :=
Make_Subprogram_Body (Loc,
Specification =>
Copy_Subprogram_Spec (Proc_Spec),
Declarations => Curr_Decls,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
Statements => New_List (If_Stmt),
End_Label => Make_Identifier (Loc, Chars (Proc_Id))));
Insert_After_And_Analyze (Last, Proc_Bod);
-- Restore assertion context
In_Assertion_Expr := In_Assertion_Expr - 1;
-- Rewrite the aspect expression, which is no longer needed, with
-- a reference to the procedure that has just been created. We will
-- generate a call to this procedure at each recursive call of the
-- subprogram that has been annotated with Subprogram_Variant.
Rewrite (Aggr, New_Occurrence_Of (Proc_Id, Loc));
end Expand_Pragma_Subprogram_Variant;
-------------------------------------------
-- Expand_Pragma_Suppress_Initialization --
-------------------------------------------

View File

@ -49,4 +49,15 @@ package Exp_Prag is
-- applies to package Pack_Id. N denotes the related package spec or
-- body.
procedure Expand_Pragma_Subprogram_Variant
(Prag : Node_Id;
Subp_Id : Entity_Id;
Body_Decls : List_Id);
-- Given pragma Subprogram_Variant Prag, create the circuitry needed
-- to evaluate variant expressions at the subprogram entry and at the
-- recursive call. Subp_Id is the related subprogram for which the pragma
-- applies and Body_Decls are its body declarations. On exit, the argument
-- of Prag is replaced with a reference to procedure with checks for the
-- variant expressions.
end Exp_Prag;

View File

@ -9930,6 +9930,24 @@ package body Exp_Util is
Constraints => List_Constr));
end Make_Subtype_From_Expr;
-----------------------------
-- Make_Variant_Comparison --
-----------------------------
function Make_Variant_Comparison
(Loc : Source_Ptr;
Mode : Name_Id;
Curr_Val : Node_Id;
Old_Val : Node_Id) return Node_Id
is
begin
if Mode = Name_Increases then
return Make_Op_Gt (Loc, Curr_Val, Old_Val);
else pragma Assert (Mode = Name_Decreases);
return Make_Op_Lt (Loc, Curr_Val, Old_Val);
end if;
end Make_Variant_Comparison;
---------------
-- Map_Types --
---------------

View File

@ -910,6 +910,15 @@ package Exp_Util is
-- wide type. Set Related_Id to request an external name for the subtype
-- rather than an internal temporary.
function Make_Variant_Comparison
(Loc : Source_Ptr;
Mode : Name_Id;
Curr_Val : Node_Id;
Old_Val : Node_Id) return Node_Id;
-- Subsidiary to the expansion of pragmas Loop_Variant and
-- Subprogram_Variant. Generate a comparison between Curr_Val and Old_Val
-- depending on the variant mode (Increases / Decreases).
procedure Map_Types (Parent_Type : Entity_Id; Derived_Type : Entity_Id);
-- Establish the following mapping between the attributes of tagged parent
-- type Parent_Type and tagged derived type Derived_Type.

View File

@ -317,6 +317,7 @@ package body Inline is
-- Refined_Global
-- Refined_Depends
-- Refined_Post
-- Subprogram_Variant
-- Test_Case
-- Unmodified
-- Unreferenced
@ -5119,6 +5120,7 @@ package body Inline is
| Name_Refined_Global
| Name_Refined_Depends
| Name_Refined_Post
| Name_Subprogram_Variant
| Name_Test_Case
| Name_Unmodified
| Name_Unreferenced

View File

@ -1496,6 +1496,7 @@ begin
| Pragma_Storage_Unit
| Pragma_Stream_Convert
| Pragma_Subtitle
| Pragma_Subprogram_Variant
| Pragma_Suppress
| Pragma_Suppress_Debug_Info
| Pragma_Suppress_Exception_Locations

View File

@ -1193,6 +1193,38 @@ package body Sem is
end if;
end Insert_Before_And_Analyze;
--------------------------------------------
-- Insert_Before_First_Source_Declaration --
--------------------------------------------
procedure Insert_Before_First_Source_Declaration
(Stmt : Node_Id;
Decls : List_Id)
is
Decl : Node_Id;
begin
-- Inspect the declarations of the related subprogram body looking for
-- the first source declaration.
pragma Assert (Present (Decls));
Decl := First (Decls);
while Present (Decl) loop
if Comes_From_Source (Decl) then
Insert_Before (Decl, Stmt);
return;
end if;
Next (Decl);
end loop;
-- If we get there, then the subprogram body lacks any source
-- declarations. The body of _Postconditions now acts as the
-- last declaration.
Append (Stmt, Decls);
end Insert_Before_First_Source_Declaration;
-----------------------------------
-- Insert_List_After_And_Analyze --
-----------------------------------

View File

@ -671,6 +671,13 @@ package Sem is
-- Suppress argument is present, then the analysis is done with the
-- specified check suppressed (can be All_Checks to suppress all checks).
procedure Insert_Before_First_Source_Declaration
(Stmt : Node_Id;
Decls : List_Id);
-- Insert node Stmt before the first source declaration of the related
-- subprogram's body. If no such declaration exists, Stmt becomes the last
-- declaration.
function External_Ref_In_Generic (E : Entity_Id) return Boolean;
-- Return True if we are in the context of a generic and E is
-- external (more global) to it.

View File

@ -270,6 +270,7 @@ package body Sem_Ch12 is
-- Refined_Depends
-- Refined_Global
-- Refined_Post
-- Subprogram_Variant
-- Test_Case
-- Most package contract annotations utilize forward references to classify

View File

@ -1544,6 +1544,7 @@ package body Sem_Ch13 is
-- Refined_Global
-- Refined_State
-- SPARK_Mode
-- Subprogram_Variant
-- Warnings
-- Insert pragma Prag such that it mimics the placement of a source
-- pragma of the same kind. Flag Is_Generic should be set when the
@ -1764,10 +1765,10 @@ package body Sem_Ch13 is
-- analyzed right now.
-- Note that there is a special handling for Pre, Post, Test_Case,
-- Contract_Cases aspects. In these cases, we do not have to worry
-- about delay issues, since the pragmas themselves deal with delay
-- of visibility for the expression analysis. Thus, we just insert
-- the pragma after the node N.
-- Contract_Cases and Subprogram_Variant aspects. In these cases, we do
-- not have to worry about delay issues, since the pragmas themselves
-- deal with delay of visibility for the expression analysis. Thus, we
-- just insert the pragma after the node N.
-- Loop through aspects
@ -4192,8 +4193,8 @@ package body Sem_Ch13 is
-- Case 4: Aspects requiring special handling
-- Pre/Post/Test_Case/Contract_Cases whose corresponding
-- pragmas take care of the delay.
-- Pre/Post/Test_Case/Contract_Cases/Subprogram_Variant whose
-- corresponding pragmas take care of the delay.
-- Pre/Post
@ -4402,6 +4403,19 @@ package body Sem_Ch13 is
Insert_Pragma (Aitem);
goto Continue;
-- Subprogram_Variant
when Aspect_Subprogram_Variant =>
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
Expression => Relocate_Node (Expr))),
Pragma_Name => Nam);
Decorate (Aspect, Aitem);
Insert_Pragma (Aitem);
goto Continue;
-- Case 5: Special handling for aspects with an optional
-- boolean argument.
@ -10855,6 +10869,7 @@ package body Sem_Ch13 is
| Aspect_Refined_State
| Aspect_Relaxed_Initialization
| Aspect_SPARK_Mode
| Aspect_Subprogram_Variant
| Aspect_Test_Case
| Aspect_Unimplemented
| Aspect_Volatile_Function

View File

@ -4070,10 +4070,10 @@ package body Sem_Prag is
procedure Ensure_Aggregate_Form (Arg : Node_Id);
-- Subsidiary routine to the processing of pragmas Abstract_State,
-- Contract_Cases, Depends, Global, Initializes, Refined_Depends,
-- Refined_Global and Refined_State. Transform argument Arg into
-- an aggregate if not one already. N_Null is never transformed.
-- Arg may denote an aspect specification or a pragma argument
-- association.
-- Refined_Global, Refined_State and Subprogram_Variant. Transform
-- argument Arg into an aggregate if not one already. N_Null is never
-- transformed. Arg may denote an aspect specification or a pragma
-- argument association.
procedure Error_Pragma (Msg : String);
pragma No_Return (Error_Pragma);
@ -23898,6 +23898,139 @@ package body Sem_Prag is
end if;
end Style_Checks;
------------------------
-- Subprogram_Variant --
------------------------
-- pragma Subprogram_Variant ( SUBPROGRAM_VARIANT_ITEM
-- {, SUBPROGRAM_VARIANT_ITEM } );
-- SUBPROGRAM_VARIANT_ITEM ::=
-- CHANGE_DIRECTION => discrete_EXPRESSION
-- CHANGE_DIRECTION ::= Increases | Decreases
-- Characteristics:
-- * Analysis - The annotation undergoes initial checks to verify
-- the legal placement and context. Secondary checks preanalyze the
-- expressions in:
-- Analyze_Subprogram_Variant_In_Decl_Part
-- * Expansion - The annotation is expanded during the expansion of
-- the related subprogram [body] contract as performed in:
-- Expand_Subprogram_Contract
-- * Template - The annotation utilizes the generic template of the
-- related subprogram [body] when it is:
-- aspect on subprogram declaration
-- aspect on stand-alone subprogram body
-- pragma on stand-alone subprogram body
-- The annotation must prepare its own template when it is:
-- pragma on subprogram declaration
-- * Globals - Capture of global references must occur after full
-- analysis.
-- * Instance - The annotation is instantiated automatically when
-- the related generic subprogram [body] is instantiated except for
-- the "pragma on subprogram declaration" case. In that scenario
-- the annotation must instantiate itself.
when Pragma_Subprogram_Variant => Subprogram_Variant : declare
Spec_Id : Entity_Id;
Subp_Decl : Node_Id;
Subp_Spec : Node_Id;
begin
GNAT_Pragma;
Check_No_Identifiers;
Check_Arg_Count (1);
-- Ensure the proper placement of the pragma. Subprogram_Variant
-- must be associated with a subprogram declaration or a body that
-- acts as a spec.
Subp_Decl :=
Find_Related_Declaration_Or_Body (N, Do_Checks => True);
-- Generic subprogram
if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
null;
-- Body acts as spec
elsif Nkind (Subp_Decl) = N_Subprogram_Body
and then No (Corresponding_Spec (Subp_Decl))
then
null;
-- Body stub acts as spec
elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
and then No (Corresponding_Spec_Of_Stub (Subp_Decl))
then
null;
-- Subprogram
elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
Subp_Spec := Specification (Subp_Decl);
-- Pragma Subprogram_Variant is forbidden on null procedures,
-- as this may lead to potential ambiguities in behavior when
-- interface null procedures are involved. Also, it just
-- wouldn't make sense, because null procedure is not
-- recursive.
if Nkind (Subp_Spec) = N_Procedure_Specification
and then Null_Present (Subp_Spec)
then
Error_Msg_N (Fix_Error
("pragma % cannot apply to null procedure"), N);
return;
end if;
else
Pragma_Misplaced;
return;
end if;
Spec_Id := Unique_Defining_Entity (Subp_Decl);
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
Mark_Ghost_Pragma (N, Spec_Id);
Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
-- Chain the pragma on the contract for further processing by
-- Analyze_Contract_Cases_In_Decl_Part.
Add_Contract_Item (N, Defining_Entity (Subp_Decl));
-- Fully analyze the pragma when it appears inside a subprogram
-- body because it cannot benefit from forward references.
if Nkind (Subp_Decl) in N_Subprogram_Body
| N_Subprogram_Body_Stub
then
-- The legality checks of pragma Subprogram_Variant are
-- affected by the SPARK mode in effect and the volatility
-- of the context. Analyze all pragmas in a specific order.
Analyze_If_Present (Pragma_SPARK_Mode);
Analyze_If_Present (Pragma_Volatile_Function);
Analyze_Subprogram_Variant_In_Decl_Part (N);
end if;
end Subprogram_Variant;
--------------
-- Subtitle --
--------------
@ -28918,6 +29051,152 @@ package body Sem_Prag is
Set_Is_Analyzed_Pragma (N);
end Analyze_Refined_State_In_Decl_Part;
---------------------------------------------
-- Analyze_Subprogram_Variant_In_Decl_Part --
---------------------------------------------
-- WARNING: This routine manages Ghost regions. Return statements must be
-- replaced by gotos which jump to the end of the routine and restore the
-- Ghost mode.
procedure Analyze_Subprogram_Variant_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty)
is
Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
procedure Analyze_Variant (Variant : Node_Id);
-- Verify the legality of a single contract case
---------------------
-- Analyze_Variant --
---------------------
procedure Analyze_Variant (Variant : Node_Id) is
Direction : Node_Id;
Expr : Node_Id;
Errors : Nat;
Extra_Direction : Node_Id;
begin
if Nkind (Variant) /= N_Component_Association then
Error_Msg_N ("wrong syntax in subprogram variant", Variant);
return;
end if;
Direction := First (Choices (Variant));
Expr := Expression (Variant);
-- Each variant must have exactly one direction
Extra_Direction := Next (Direction);
if Present (Extra_Direction) then
Error_Msg_N
("subprogram variant case must have exactly one direction",
Extra_Direction);
end if;
-- Check placement of OTHERS if available (SPARK RM 6.1.3(1))
if Nkind (Direction) = N_Identifier then
if Chars (Direction) /= Name_Decreases
and then
Chars (Direction) /= Name_Increases
then
Error_Msg_N ("wrong direction", Direction);
end if;
else
Error_Msg_N ("wrong syntax", Direction);
end if;
Errors := Serious_Errors_Detected;
Preanalyze_Assert_Expression (Expr, Any_Discrete);
-- Emit a clarification message when the variant expression
-- contains at least one undefined reference, possibly due
-- to contract freezing.
if Errors /= Serious_Errors_Detected
and then Present (Freeze_Id)
and then Has_Undefined_Reference (Expr)
then
Contract_Freeze_Error (Spec_Id, Freeze_Id);
end if;
end Analyze_Variant;
-- Local variables
Variants : constant Node_Id := Expression (Get_Argument (N, Spec_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
Variant : Node_Id;
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Subprogram_Variant_In_Decl_Part
begin
-- Do not analyze the pragma multiple times
if Is_Analyzed_Pragma (N) then
return;
end if;
-- Set the Ghost mode in effect from the pragma. Due to the delayed
-- analysis of the pragma, the Ghost mode at point of declaration and
-- point of analysis may not necessarily be the same. Use the mode in
-- effect at the point of declaration.
Set_Ghost_Mode (N);
-- Single and multiple contract cases must appear in aggregate form. If
-- this is not the case, then either the parser of the analysis of the
-- pragma failed to produce an aggregate.
pragma Assert (Nkind (Variants) = N_Aggregate);
if Present (Component_Associations (Variants)) then
-- Ensure that the formal parameters are visible when analyzing all
-- clauses. This falls out of the general rule of aspects pertaining
-- to subprogram declarations.
if not In_Open_Scopes (Spec_Id) then
Restore_Scope := True;
Push_Scope (Spec_Id);
if Is_Generic_Subprogram (Spec_Id) then
Install_Generic_Formals (Spec_Id);
else
Install_Formals (Spec_Id);
end if;
end if;
Variant := First (Component_Associations (Variants));
while Present (Variant) loop
Analyze_Variant (Variant);
Next (Variant);
end loop;
if Restore_Scope then
End_Scope;
end if;
-- Otherwise the pragma is illegal
else
Error_Msg_N ("wrong syntax for subprogram variant", N);
end if;
Set_Is_Analyzed_Pragma (N);
Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Analyze_Subprogram_Variant_In_Decl_Part;
------------------------------------
-- Analyze_Test_Case_In_Decl_Part --
------------------------------------
@ -30983,6 +31262,7 @@ package body Sem_Prag is
Pragma_Storage_Unit => 0,
Pragma_Stream_Convert => 0,
Pragma_Style_Checks => 0,
Pragma_Subprogram_Variant => -1,
Pragma_Subtitle => 0,
Pragma_Suppress => 0,
Pragma_Suppress_All => 0,
@ -31274,6 +31554,7 @@ package body Sem_Prag is
| Name_Predicate
| Name_Refined_Post
| Name_Statement_Assertions
| Name_Subprogram_Variant
=>
return True;

View File

@ -265,6 +265,13 @@ package Sem_Prag is
-- the entity of [generic] package body or [generic] subprogram body which
-- caused "freezing" of the related contract where the pragma resides.
procedure Analyze_Subprogram_Variant_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty);
-- Perform full analysis of delayed pragma Subprogram_Variant. Freeze_Id is
-- the entity of [generic] package body or [generic] subprogram body which
-- caused "freezing" of the related contract where the pragma resides.
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id);
-- Perform preanalysis of pragma Test_Case

View File

@ -6124,27 +6124,6 @@ package body Sem_Res is
------------------
procedure Resolve_Call (N : Node_Id; Typ : Entity_Id) is
function Same_Or_Aliased_Subprograms
(S : Entity_Id;
E : Entity_Id) return Boolean;
-- Returns True if the subprogram entity S is the same as E or else
-- S is an alias of E.
---------------------------------
-- Same_Or_Aliased_Subprograms --
---------------------------------
function Same_Or_Aliased_Subprograms
(S : Entity_Id;
E : Entity_Id) return Boolean
is
Subp_Alias : constant Entity_Id := Alias (S);
begin
return S = E or else (Present (Subp_Alias) and then Subp_Alias = E);
end Same_Or_Aliased_Subprograms;
-- Local variables
Loc : constant Source_Ptr := Sloc (N);
Subp : constant Node_Id := Name (N);
Body_Id : Entity_Id;
@ -6157,8 +6136,6 @@ package body Sem_Res is
Rtype : Entity_Id;
Scop : Entity_Id;
-- Start of processing for Resolve_Call
begin
-- Preserve relevant elaboration-related attributes of the context which
-- are no longer available or very expensive to recompute once analysis,

View File

@ -19037,6 +19037,7 @@ package body Sem_Util is
or else Nam = Name_Refined_Depends
or else Nam = Name_Refined_Global
or else Nam = Name_Refined_Post
or else Nam = Name_Subprogram_Variant
or else Nam = Name_Test_Case;
end Is_Subprogram_Contract_Annotation;
@ -26242,6 +26243,19 @@ package body Sem_Util is
end if;
end Same_Object;
---------------------------------
-- Same_Or_Aliased_Subprograms --
---------------------------------
function Same_Or_Aliased_Subprograms
(S : Entity_Id;
E : Entity_Id) return Boolean
is
Subp_Alias : constant Entity_Id := Alias (S);
begin
return S = E or else (Present (Subp_Alias) and then Subp_Alias = E);
end Same_Or_Aliased_Subprograms;
---------------
-- Same_Type --
---------------

View File

@ -2148,6 +2148,7 @@ package Sem_Util is
-- Refined_Depends
-- Refined_Global
-- Refined_Post
-- Subprogram_Variant
-- Test_Case
function Is_Subprogram_Stub_Without_Prior_Declaration
@ -2824,6 +2825,12 @@ package Sem_Util is
-- mean that different objects are designated, just that this could not
-- be reliably determined at compile time.
function Same_Or_Aliased_Subprograms
(S : Entity_Id;
E : Entity_Id) return Boolean;
-- Returns True if the subprogram entity S is the same as E or else S is an
-- alias of E.
function Same_Type (T1, T2 : Entity_Id) return Boolean;
-- Determines if T1 and T2 represent exactly the same type. Two types
-- are the same if they are identical, or if one is an unconstrained

View File

@ -7945,8 +7945,8 @@ package Sinfo is
-- operation) are also in this list.
-- Contract_Test_Cases contains a collection of pragmas that correspond
-- to aspects/pragmas Contract_Cases and Test_Case. The ordering in the
-- list is in LIFO fashion.
-- to aspects/pragmas Contract_Cases, Test_Case and Subprogram_Variant.
-- The ordering in the list is in LIFO fashion.
-- Classifications contains pragmas that either declare, categorize, or
-- establish dependencies between subprogram or package inputs and

View File

@ -196,6 +196,7 @@ package Snames is
Name_uTask_Name : constant Name_Id := N + $;
Name_uTrace_Sp : constant Name_Id := N + $;
Name_uType_Invariant : constant Name_Id := N + $;
Name_uVariants : constant Name_Id := N + $;
-- Names of predefined primitives used in the expansion of dispatching
-- requeue and select statements, Abort, 'Callable and 'Terminated.
@ -668,6 +669,7 @@ package Snames is
Name_Source_Reference : constant Name_Id := N + $; -- GNAT
Name_Static_Elaboration_Desired : constant Name_Id := N + $; -- GNAT
Name_Stream_Convert : constant Name_Id := N + $; -- GNAT
Name_Subprogram_Variant : constant Name_Id := N + $; -- GNAT
Name_Subtitle : constant Name_Id := N + $; -- GNAT
Name_Suppress_All : constant Name_Id := N + $; -- GNAT
Name_Suppress_Debug_Info : constant Name_Id := N + $; -- GNAT
@ -2102,6 +2104,7 @@ package Snames is
Pragma_Source_Reference,
Pragma_Static_Elaboration_Desired,
Pragma_Stream_Convert,
Pragma_Subprogram_Variant,
Pragma_Subtitle,
Pragma_Suppress_All,
Pragma_Suppress_Debug_Info,