This patch introduces a new aspect "Subprogram_Variant" with expressions that are meant to increase/decrease with each recursive call of the annotated subprogram. It is inspired by the existing pragma Loop_Variant, whose expressions are meant to increase/decrease with each iteration of the loop. Both of those annotations are primarily used by GNATprove to verify that subprograms and loops terminate, but GNAT does all the legality checks and expansion for the dynamic semantics.
The new aspect is processed in the following steps: 1. Translate aspect to a corresponding pragma, so that we can reuse the existing circuitry for similar aspects; in particular, we heavily mimic processing of aspect Contract_Cases, which appears to be the most similar one. 2. Validate placement of the pragma. 3. Analyse increase/decrease expressions, which might contain references to both the subprogram parameters and forward references to global objects (just like expressions of the aspects Pre/Post/Contract_Cases and Global/Depends, so analysis is delayed). 4. Build declarations of constant objects that capture values of the variant expressions at subprogram entry and a procedure that compares those constants with values of the corresponding expressions at a recursive call. 5. Add call to the above procedure at recursive calls of the subprogram. Steps 1-3 are needed for both GNAT and GNATprove (which requires increases/decreases expressions to be analyzed); steps 4-5 are only needed for GNAT to implement dynamics semantics. No existing GNAT functionality is affected by this new aspect. Tested on x86_64-pc-linux-gnu, committed on trunk 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.
patch.diff.gz
Description: application/gzip