New implementation of class-wide pre/postconditions that relies on helpers to move the corresponding runtime checks to the caller side. This implementation also adds indirect call wrappers and dispatch table wrappers that facilitate combining class-wide conditions with access-to-subprogram types with preconditions (AI12-0220), and provides full support for inheriting body but overriding preconditions or postconditions (AI12-0195).
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* contracts.ads (Make_Class_Precondition_Subps): New subprogram.
(Merge_Class_Conditions): New subprogram.
(Process_Class_Conditions_At_Freeze_Point): New subprogram.
* contracts.adb (Check_Class_Condition): New subprogram.
(Set_Class_Condition): New subprogram.
(Analyze_Contracts): Remove code analyzing class-wide-clone
subprogram since it is no longer built.
(Process_Spec_Postconditions): Avoid processing twice seen
subprograms.
(Process_Preconditions): Simplify its functionality to
non-class-wide preconditions.
(Process_Preconditions_For): No action needed for wrappers and
helpers.
(Make_Class_Precondition_Subps): New subprogram.
(Process_Class_Conditions_At_Freeze_Point): New subprogram.
(Merge_Class_Conditions): New subprogram.
* exp_ch6.ads (Install_Class_Preconditions_Check): New
subprogram.
* exp_ch6.adb (Expand_Call_Helper): Install class-wide
preconditions check on dispatching primitives that have or
inherit class-wide preconditions.
(Freeze_Subprogram): Remove code for null procedures with
preconditions.
(Install_Class_Preconditions_Check): New subprogram.
* exp_util.ads (Build_Class_Wide_Expression): Lower the
complexity of this subprogram; out-mode formal Needs_Wrapper
since this functionality is now provided by a new subprogram.
(Get_Mapped_Entity): New subprogram.
(Map_Formals): New subprogram.
* exp_util.adb (Build_Class_Wide_Expression): Lower the
complexity of this subprogram. Its previous functionality is now
provided by subprograms Needs_Wrapper and Check_Class_Condition.
(Add_Parent_DICs): Map the overridden primitive to the
overriding one.
(Get_Mapped_Entity): New subprogram.
(Map_Formals): New subprogram.
(Update_Primitives_Mapping): Adding assertion.
* freeze.ads (Check_Inherited_Conditions): Subprogram made
public with added formal to support late overriding.
* freeze.adb (Check_Inherited_Conditions): New implementation;
builds the dispatch table wrapper required for class-wide
pre/postconditions; added support for late overriding.
(Needs_Wrapper): New subprogram.
* sem.ads (Inside_Class_Condition_Preanalysis): New global
variable.
* sem_disp.ads (Covered_Interface_Primitives): New subprogram.
* sem_disp.adb (Covered_Interface_Primitives): New subprogram.
(Check_Dispatching_Context): Skip checking context of
dispatching calls during preanalysis of class-wide conditions
since at that stage the expression is not installed yet on its
definite context.
(Check_Dispatching_Call): Skip checking 6.1.1(18.2/5) by
AI12-0412 on helpers and wrappers internally built for
supporting class-wide conditions; for late-overriding
subprograms call Check_Inherited_Conditions to build the
dispatch-table wrapper (if required).
(Propagate_Tag): Adding call to
Install_Class_Preconditions_Check.
* sem_util.ads (Build_Class_Wide_Clone_Body): Removed.
(Build_Class_Wide_Clone_Call): Removed.
(Build_Class_Wide_Clone_Decl): Removed.
(Class_Condition): New subprogram.
(Nearest_Class_Condition_Subprogram): New subprogram.
* sem_util.adb (Build_Class_Wide_Clone_Body): Removed.
(Build_Class_Wide_Clone_Call): Removed.
(Build_Class_Wide_Clone_Decl): Removed.
(Class_Condition): New subprogram.
(Nearest_Class_Condition_Subprogram): New subprogram.
(Eligible_For_Conditional_Evaluation): No need to evaluate
class-wide conditions during preanalysis since the expression is
not installed on its definite context.
* einfo.ads (Class_Wide_Clone): Removed.
(Class_Postconditions): New attribute.
(Class_Preconditions): New attribute.
(Class_Preconditions_Subprogram): New attribute.
(Dynamic_Call_Helper): New attribute.
(Ignored_Class_Postconditions): New attribute.
(Ignored_Class_Preconditions): New attribute.
(Indirect_Call_Wrapper): New attribute.
(Is_Dispatch_Table_Wrapper): New attribute.
(Static_Call_Helper): New attribute.
* exp_attr.adb (Expand_N_Attribute_Reference): When the prefix
is of an access-to-subprogram type that has class-wide
preconditions and an indirect-call wrapper of such subprogram is
available, replace the prefix by the wrapper.
* exp_ch3.adb (Build_Class_Condition_Subprograms): New
subprogram.
(Register_Dispatch_Table_Wrappers): New subprogram.
* exp_disp.adb (Build_Class_Wide_Check): Removed; class-wide
precondition checks now rely on internally built helpers.
* sem_ch13.adb (Analyze_Aspect_Specifications): Set initial
value of attributes Class_Preconditions, Class_Postconditions,
Ignored_Class_Preconditions and Ignored_Class_Postconditions.
These values are later updated with the full pre/postcondition
by Merge_Class_Conditions.
(Freeze_Entity_Checks): Call
Process_Class_Conditions_At_Freeze_Point.
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Remove code
building the body of the class-wide clone subprogram since it is
no longer required.
(Install_Entity): Adding assertion.
* sem_prag.adb (Analyze_Pre_Post_Condition_In_Decl_Part): Remove
code building and analyzing the class-wide clone subprogram; no
longer required.
(Build_Pragma_Check_Equivalent): Adjust call to
Build_Class_Wide_Expression since the formal named Needs_Wrapper
has been removed.
* sem_attr.adb (Analyze_Attribute_Old_Result): Skip processing
these attributes during preanalysis of class-wide conditions
since at that stage the expression is not installed yet on its
definite context.
* sem_res.adb (Resolve_Actuals): Skip applying RM 3.9.2(9/1) and
SPARK RM 6.1.7(3) on actuals of internal helpers and wrappers
built to support class-wide preconditions.
* sem_ch5.adb (Process_Bounds): Do not generate a constant
declaration for the bounds when we are preanalyzing a class-wide
condition.
(Analyze_Loop_Parameter_Specification): Handle preanalysis of
quantified expression placed in the outermost expression of a
class-wide condition.
* ghost.adb (Check_Ghost_Context): No check required during
preanalysis of class-wide conditions.
* gen_il-fields.ads (Opt_Field_Enum): Adding
Class_Postconditions, Class_Preconditions,
Class_Preconditions_Subprogram, Dynamic_Call_Helper,
Ignored_Class_Postconditions, Ignored_Class_Preconditions,
Indirect_Call_Wrapper, Is_Dispatch_Table_Wrapper,
Static_Call_Helper.
* gen_il-gen-gen_entities.adb (Is_Dispatch_Table_Wrapper):
Adding semantic flag Is_Dispatch_Table_Wrapper; removing
semantic field Class_Wide_Clone; adding semantic fields for
Class_Postconditions, Class_Preconditions,
Class_Preconditions_Subprogram, Dynamic_Call_Helper,
Ignored_Class_Postconditions, Indirect_Call_Wrapper,
Ignored_Class_Preconditions, and Static_Call_Helper.
patch.diff.gz
Description: application/gzip
