From: Johannes Kanig Date: Mon, 17 Aug 2020 00:41:10 +0000 (+0900) Subject: [Ada] GNATprove: remove support for external axiomatizations X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=955886d1a2c75d16b41df1c97d04387bd7436dab;p=gcc.git [Ada] GNATprove: remove support for external axiomatizations gcc/ada/ * exp_util.adb, exp_util.ads (Containing_Package_With_Ext_Axioms, Has_Annotate_Pragma_For_External_Axiomatizations): Removed. * sem_ch8.adb (Analyze_Subprogram_Renaming): Removed code related to external axiomatizations. * einfo.ads (Is_Generic_Actual_Subprogram): Removed comment about external axiomatization. --- diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index da9b49fa5ad..bb5ab07790e 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -2655,10 +2655,6 @@ package Einfo is -- Used to generate constraint checks on calls to these subprograms, even -- within an instance of a predefined run-time unit, in which checks -- are otherwise suppressed. --- --- The flag is also set on the entity of the expression function created --- within an instance, for a function that has external axiomatization, --- for use in GNATprove mode. -- Is_Generic_Actual_Type (Flag94) -- Defined in all type and subtype entities. Set in the subtype diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 2b05d8acff8..6b474d80f82 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -4615,60 +4615,6 @@ package body Exp_Util is end if; end Component_May_Be_Bit_Aligned; - ---------------------------------------- - -- Containing_Package_With_Ext_Axioms -- - ---------------------------------------- - - function Containing_Package_With_Ext_Axioms - (E : Entity_Id) return Entity_Id - is - begin - -- E is the package or generic package which is externally axiomatized - - if Is_Package_Or_Generic_Package (E) - and then Has_Annotate_Pragma_For_External_Axiomatization (E) - then - return E; - end if; - - -- If E's scope is axiomatized, E is axiomatized - - if Present (Scope (E)) then - declare - First_Ax_Parent_Scope : constant Entity_Id := - Containing_Package_With_Ext_Axioms (Scope (E)); - begin - if Present (First_Ax_Parent_Scope) then - return First_Ax_Parent_Scope; - end if; - end; - end if; - - -- Otherwise, if E is a package instance, it is axiomatized if the - -- corresponding generic package is axiomatized. - - if Ekind (E) = E_Package then - declare - Par : constant Node_Id := Parent (E); - Decl : Node_Id; - - begin - if Nkind (Par) = N_Defining_Program_Unit_Name then - Decl := Parent (Par); - else - Decl := Par; - end if; - - if Present (Generic_Parent (Decl)) then - return - Containing_Package_With_Ext_Axioms (Generic_Parent (Decl)); - end if; - end; - end if; - - return Empty; - end Containing_Package_With_Ext_Axioms; - ------------------------------- -- Convert_To_Actual_Subtype -- ------------------------------- @@ -6653,122 +6599,6 @@ package body Exp_Util is end if; end Has_Access_Constraint; - ----------------------------------------------------- - -- Has_Annotate_Pragma_For_External_Axiomatization -- - ----------------------------------------------------- - - function Has_Annotate_Pragma_For_External_Axiomatization - (E : Entity_Id) return Boolean - is - function Is_Annotate_Pragma_For_External_Axiomatization - (N : Node_Id) return Boolean; - -- Returns whether N is - -- pragma Annotate (GNATprove, External_Axiomatization); - - ---------------------------------------------------- - -- Is_Annotate_Pragma_For_External_Axiomatization -- - ---------------------------------------------------- - - -- The general form of pragma Annotate is - - -- pragma Annotate (IDENTIFIER [, IDENTIFIER {, ARG}]); - -- ARG ::= NAME | EXPRESSION - - -- The first two arguments are by convention intended to refer to an - -- external tool and a tool-specific function. These arguments are - -- not analyzed. - - -- The following is used to annotate a package specification which - -- GNATprove should treat specially, because the axiomatization of - -- this unit is given by the user instead of being automatically - -- generated. - - -- pragma Annotate (GNATprove, External_Axiomatization); - - function Is_Annotate_Pragma_For_External_Axiomatization - (N : Node_Id) return Boolean - is - Name_GNATprove : constant String := - "gnatprove"; - Name_External_Axiomatization : constant String := - "external_axiomatization"; - -- Special names - - begin - if Nkind (N) = N_Pragma - and then Get_Pragma_Id (N) = Pragma_Annotate - and then List_Length (Pragma_Argument_Associations (N)) = 2 - then - declare - Arg1 : constant Node_Id := - First (Pragma_Argument_Associations (N)); - Arg2 : constant Node_Id := Next (Arg1); - Nam1 : Name_Id; - Nam2 : Name_Id; - - begin - -- Fill in Name_Buffer with Name_GNATprove first, and then with - -- Name_External_Axiomatization so that Name_Find returns the - -- corresponding name. This takes care of all possible casings. - - Name_Len := 0; - Add_Str_To_Name_Buffer (Name_GNATprove); - Nam1 := Name_Find; - - Name_Len := 0; - Add_Str_To_Name_Buffer (Name_External_Axiomatization); - Nam2 := Name_Find; - - return Chars (Get_Pragma_Arg (Arg1)) = Nam1 - and then - Chars (Get_Pragma_Arg (Arg2)) = Nam2; - end; - - else - return False; - end if; - end Is_Annotate_Pragma_For_External_Axiomatization; - - -- Local variables - - Decl : Node_Id; - Vis_Decls : List_Id; - N : Node_Id; - - -- Start of processing for Has_Annotate_Pragma_For_External_Axiomatization - - begin - if Nkind (Parent (E)) = N_Defining_Program_Unit_Name then - Decl := Parent (Parent (E)); - else - Decl := Parent (E); - end if; - - Vis_Decls := Visible_Declarations (Decl); - - N := First (Vis_Decls); - while Present (N) loop - - -- Skip declarations generated by the frontend. Skip all pragmas - -- that are not the desired Annotate pragma. Stop the search on - -- the first non-pragma source declaration. - - if Comes_From_Source (N) then - if Nkind (N) = N_Pragma then - if Is_Annotate_Pragma_For_External_Axiomatization (N) then - return True; - end if; - else - return False; - end if; - end if; - - Next (N); - end loop; - - return False; - end Has_Annotate_Pragma_For_External_Axiomatization; - -------------------- -- Homonym_Number -- -------------------- diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads index cb288bd0c0e..37eb86fba00 100644 --- a/gcc/ada/exp_util.ads +++ b/gcc/ada/exp_util.ads @@ -427,11 +427,6 @@ package Exp_Util is -- for trouble using this function and, if so, the assignment is expanded -- component-wise, which the back end is required to handle correctly. - function Containing_Package_With_Ext_Axioms - (E : Entity_Id) return Entity_Id; - -- Returns the package entity with an external axiomatization containing E, - -- if any, or Empty if none. - procedure Convert_To_Actual_Subtype (Exp : Node_Id); -- The Etype of an expression is the nominal type of the expression, -- not the actual subtype. Often these are the same, but not always. @@ -730,12 +725,6 @@ package Exp_Util is function Has_Access_Constraint (E : Entity_Id) return Boolean; -- Given object or type E, determine if a discriminant is of an access type - function Has_Annotate_Pragma_For_External_Axiomatization - (E : Entity_Id) return Boolean; - -- Returns whether E is a package entity, for which the initial list of - -- pragmas at the start of the package declaration contains - -- pragma Annotate (GNATprove, External_Axiomatization); - function Homonym_Number (Subp : Entity_Id) return Pos; -- Here subp is the entity for a subprogram. This routine returns the -- homonym number used to disambiguate overloaded subprograms in the same diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index 3bdce445ffa..35c6f60d75d 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -3005,16 +3005,7 @@ package body Sem_Ch8 is -- Check whether the renaming is for a defaulted actual subprogram -- with a class-wide actual. - -- The class-wide wrapper is not needed in GNATprove_Mode and there - -- is an external axiomatization on the package. - - if CW_Actual - and then Box_Present (Inst_Node) - and then not - (GNATprove_Mode - and then - Present (Containing_Package_With_Ext_Axioms (Formal_Spec))) - then + if CW_Actual and then Box_Present (Inst_Node) then Build_Class_Wide_Wrapper (New_S, Old_S); elsif Is_Entity_Name (Nam) @@ -3874,29 +3865,6 @@ package body Sem_Ch8 is Ada_Version_Pragma := Save_AVP; Ada_Version_Explicit := Save_AV_Exp; - -- In GNATprove mode, the renamings of actual subprograms are replaced - -- with wrapper functions that make it easier to propagate axioms to the - -- points of call within an instance. Wrappers are generated if formal - -- subprogram is subject to axiomatization. - - -- The types in the wrapper profiles are obtained from (instances of) - -- the types of the formal subprogram. - - if Is_Actual - and then GNATprove_Mode - and then Present (Containing_Package_With_Ext_Axioms (Formal_Spec)) - and then not Inside_A_Generic - then - if Ekind (Old_S) = E_Function then - Rewrite (N, Build_Function_Wrapper (Formal_Spec, Old_S)); - Analyze (N); - - elsif Ekind (Old_S) = E_Operator then - Rewrite (N, Build_Operator_Wrapper (Formal_Spec, Old_S)); - Analyze (N); - end if; - end if; - -- Check if we are looking at an Ada 2012 defaulted formal subprogram -- and mark any use_package_clauses that affect the visibility of the -- implicit generic actual.