From e577151d02b9e73e2aa985f0254f5a2f060d3e54 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Fri, 27 Mar 2020 23:39:03 +0100 Subject: [PATCH] [Ada] Support aspect Relaxed_Initialization and attribute Initialized 2020-06-15 Piotr Trojanek gcc/ada/ * aspects.ads (Aspect_Id): Add Aspect_Relaxed_Initialization. (Implementation_Defined_Aspect): Add new aspect. (Aspect_Argument): Add new aspect with Optional_Expression argument. (Is_Representation_Aspect): Add new aspect as a non-representation one. (Aspect_Names): Add name for the new aspect. (Aspect_Delay): Add new aspect as a non-delayed one. * sem_ch3.adb: Minor reformatting. * einfo.ads, einfo.adb (Is_Relaxed_Initialization_State): New query; reuses existing code for querying abstract state options. * exp_attr.adb (Expand_N_Attribute_Reference): For now ignore attribute 'Initialized. * sem_attr.adb (Analyze_Attribute_Old_Result): Allow attribute 'Result to be used in the aspect Relaxed_Initialization expression. (Analyze_Attribute): Analyze attribute 'Initialized; based on existing code for attribute 'Valid_Scalars. (Eval_Attribute): Do not expect attribute 'Initialized, just like attribute 'Valid_Scalars is not expected. * sem_ch13.adb (Analyze_Aspect_Relaxed_Initialization): New routine. (Analyze_Aspect_Specifications): Analyze new aspect in a dedicated routine. (Check_Aspect_At_Freeze_Point): Do not expect new aspect. * sem_prag.adb (Analyze_Abstract_State): Support option Relaxed_Initialization on abstract states. * sem_util.ads, sem_util.adb (Has_Relaxed_Initialization): New query for the GNATprove backend. * snames.ads-tmpl (Snames): Add Name_Ids for the new aspect and attribute; add an Attribute_Id for the new attribute. --- gcc/ada/aspects.ads | 6 ++ gcc/ada/einfo.adb | 15 ++++ gcc/ada/einfo.ads | 6 ++ gcc/ada/exp_attr.adb | 19 +++++ gcc/ada/sem_attr.adb | 30 +++++++ gcc/ada/sem_ch13.adb | 183 ++++++++++++++++++++++++++++++++++++++++ gcc/ada/sem_ch3.adb | 2 +- gcc/ada/sem_prag.adb | 27 +++--- gcc/ada/sem_util.adb | 117 +++++++++++++++++++++++++ gcc/ada/sem_util.ads | 5 ++ gcc/ada/snames.ads-tmpl | 3 + 11 files changed, 402 insertions(+), 11 deletions(-) diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 82bf5ca54b9..383a52869d3 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -138,6 +138,7 @@ package Aspects is Aspect_Refined_Post, -- GNAT Aspect_Refined_State, -- GNAT Aspect_Relative_Deadline, + Aspect_Relaxed_Initialization, -- GNAT Aspect_Scalar_Storage_Order, -- GNAT Aspect_Secondary_Stack_Size, -- GNAT Aspect_Simple_Storage_Pool, -- GNAT @@ -261,6 +262,7 @@ package Aspects is Aspect_Persistent_BSS => True, Aspect_Predicate => True, Aspect_Pure_Function => True, + Aspect_Relaxed_Initialization => True, Aspect_Remote_Access_Type => True, Aspect_Scalar_Storage_Order => True, Aspect_Secondary_Stack_Size => True, @@ -400,6 +402,7 @@ package Aspects is Aspect_Refined_Post => Expression, Aspect_Refined_State => Expression, Aspect_Relative_Deadline => Expression, + Aspect_Relaxed_Initialization => Optional_Expression, Aspect_Scalar_Storage_Order => Expression, Aspect_Secondary_Stack_Size => Expression, Aspect_Simple_Storage_Pool => Name, @@ -493,6 +496,7 @@ package Aspects is Aspect_Refined_Post => False, Aspect_Refined_State => False, Aspect_Relative_Deadline => False, + Aspect_Relaxed_Initialization => False, Aspect_Scalar_Storage_Order => True, Aspect_Secondary_Stack_Size => True, Aspect_Simple_Storage_Pool => True, @@ -651,6 +655,7 @@ package Aspects is Aspect_Refined_Post => Name_Refined_Post, Aspect_Refined_State => Name_Refined_State, Aspect_Relative_Deadline => Name_Relative_Deadline, + Aspect_Relaxed_Initialization => Name_Relaxed_Initialization, Aspect_Remote_Access_Type => Name_Remote_Access_Type, Aspect_Remote_Call_Interface => Name_Remote_Call_Interface, Aspect_Remote_Types => Name_Remote_Types, @@ -912,6 +917,7 @@ package Aspects is Aspect_Refined_Global => Never_Delay, Aspect_Refined_Post => Never_Delay, Aspect_Refined_State => Never_Delay, + Aspect_Relaxed_Initialization => Never_Delay, Aspect_SPARK_Mode => Never_Delay, Aspect_Synchronization => Never_Delay, Aspect_Test_Case => Never_Delay, diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 2456fc15e8f..eb6ae1728a0 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -8249,6 +8249,21 @@ package body Einfo is and then Is_Protected_Type (Corresponding_Concurrent_Type (Id)); end Is_Protected_Record_Type; + ------------------------------------- + -- Is_Relaxed_Initialization_State -- + ------------------------------------- + + function Is_Relaxed_Initialization_State (Id : E) return B is + begin + -- To qualify, the abstract state must appear with simple option + -- "Relaxed_Initialization" (??? add reference to SPARK RM once the + -- Relaxed_Initialization aspect is described there). + + return + Ekind (Id) = E_Abstract_State + and then Has_Option (Id, Name_Relaxed_Initialization); + end Is_Relaxed_Initialization_State; + -------------------------------- -- Is_Standard_Character_Type -- -------------------------------- diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index a1cfd7d37ce..346a15eac5b 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -3184,6 +3184,10 @@ package Einfo is -- Applies to all entities, true for record types and subtypes, -- includes class-wide types and subtypes (which are also records). +-- Is_Relaxed_Initialization_State (synthesized) +-- Applies to all entities, true for abstract states that are subject to +-- option Relaxed_Initialization. + -- Is_Remote_Call_Interface (Flag62) -- Defined in all entities. Set in E_Package and E_Generic_Package -- entities to which a pragma Remote_Call_Interface is applied, and @@ -5832,6 +5836,7 @@ package Einfo is -- Has_Null_Visible_Refinement (synth) -- Is_External_State (synth) -- Is_Null_State (synth) + -- Is_Relaxed_Initialization_State (synth) -- Is_Synchronized_State (synth) -- Partial_Refinement_Constituents (synth) @@ -7669,6 +7674,7 @@ package Einfo is function Is_Protected_Component (Id : E) return B; function Is_Protected_Interface (Id : E) return B; function Is_Protected_Record_Type (Id : E) return B; + function Is_Relaxed_Initialization_State (Id : E) return B; function Is_Standard_Character_Type (Id : E) return B; function Is_Standard_String_Type (Id : E) return B; function Is_String_Type (Id : E) return B; diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb index 182ce1554bc..08bea2b531a 100644 --- a/gcc/ada/exp_attr.adb +++ b/gcc/ada/exp_attr.adb @@ -3737,6 +3737,25 @@ package body Exp_Attr is when Attribute_Img => Exp_Imgv.Expand_Image_Attribute (N); + ----------------- + -- Initialized -- + ----------------- + + -- For execution, we could either implement an approximation of this + -- aspect, or use Valid_Scalars as a first approximation. For now we do + -- the latter. + + when Attribute_Initialized => + Rewrite + (N, + Make_Attribute_Reference + (Sloc => Loc, + Prefix => Pref, + Attribute_Name => Name_Valid_Scalars, + Expressions => Exprs)); + + Analyze_And_Resolve (N); + ----------- -- Input -- ----------- diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 801c4457ed6..2bb24a29aab 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -1324,6 +1324,15 @@ package body Sem_Attr is then null; + -- Attribute 'Result is allowed to appear in aspect + -- Relaxed_Initialization (??? add reference to SPARK RM once this + -- attribute is described there). + + elsif Prag_Nam = Name_Relaxed_Initialization + and then Aname = Name_Result + then + null; + elsif Nam_In (Prag_Nam, Name_Post, Name_Post_Class, Name_Postcondition, @@ -4146,6 +4155,26 @@ package body Sem_Attr is when Attribute_Img => Analyze_Image_Attribute (Standard_String); + ----------------- + -- Initialized -- + ----------------- + + when Attribute_Initialized => + Check_E0; + + if Comes_From_Source (N) then + + -- A similar attribute Valid_Scalars can be prefixed with + -- references to both functions and objects, but this attribute + -- can be only prefixed with references to objects. + + if not Is_Object_Reference (P) then + Error_Attr_P ("prefix of % attribute must be object"); + end if; + end if; + + Set_Etype (N, Standard_Boolean); + ----------- -- Input -- ----------- @@ -10231,6 +10260,7 @@ package body Sem_Attr is | Attribute_First_Bit | Attribute_Img | Attribute_Input + | Attribute_Initialized | Attribute_Last_Bit | Attribute_Library_Level | Attribute_Maximum_Alignment diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 0f23cbb7930..503fd150032 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1708,6 +1708,9 @@ package body Sem_Ch13 is procedure Analyze_Aspect_Implicit_Dereference; -- Perform analysis of the Implicit_Dereference aspects + procedure Analyze_Aspect_Relaxed_Initialization; + -- Perform analysis of aspect Relaxed_Initialization + procedure Make_Aitem_Pragma (Pragma_Argument_Associations : List_Id; Pragma_Name : Name_Id); @@ -2040,6 +2043,179 @@ package body Sem_Ch13 is end Analyze_Aspect_Implicit_Dereference; + ------------------------------------------- + -- Analyze_Aspect_Relaxed_Initialization -- + ------------------------------------------- + + procedure Analyze_Aspect_Relaxed_Initialization is + procedure Analyze_Relaxed_Parameter + (Subp_Id : Entity_Id; + Param : Node_Id; + Seen : in out Elist_Id); + -- Analyze parameter that appears in the expression of the + -- aspect Relaxed_Initialization. + + ------------------------------- + -- Analyze_Relaxed_Parameter -- + ------------------------------- + + procedure Analyze_Relaxed_Parameter + (Subp_Id : Entity_Id; + Param : Node_Id; + Seen : in out Elist_Id) + is + begin + -- The relaxed parameter is a formal parameter + + if Nkind_In (Param, N_Identifier, N_Expanded_Name) then + Analyze (Param); + + declare + Item : constant Entity_Id := Entity (Param); + begin + -- It must be a formal of the analyzed subprogram + + if Scope (Item) = Subp_Id then + + pragma Assert (Is_Formal (Item)); + + -- Detect duplicated items + + if Contains (Seen, Item) then + Error_Msg_N ("duplicate aspect % item", Param); + else + Append_New_Elmt (Item, Seen); + end if; + else + Error_Msg_N ("illegal aspect % item", Param); + end if; + end; + + -- The relaxed parameter is the function's Result attribute + + elsif Is_Attribute_Result (Param) then + Analyze (Param); + + declare + Pref : constant Node_Id := Prefix (Param); + begin + if Present (Pref) + and then + Nkind_In (Pref, N_Identifier, N_Expanded_Name) + and then + Entity (Pref) = Subp_Id + then + -- Detect duplicated items + + if Contains (Seen, Subp_Id) then + Error_Msg_N ("duplicate aspect % item", Param); + else + Append_New_Elmt (Entity (Pref), Seen); + end if; + + else + Error_Msg_N ("illegal aspect % item", Param); + end if; + end; + else + Error_Msg_N ("illegal aspect % item", Param); + end if; + end Analyze_Relaxed_Parameter; + + -- Local variables + + Seen : Elist_Id := No_Elist; + -- Items that appear in the relaxed initialization aspect + -- expression of a subprogram; for detecting duplicates. + + -- Start of processing for Analyze_Aspect_Relaxed_Initialization + + begin + -- Set name of the aspect for error messages + Error_Msg_Name_1 := Nam; + + -- Annotation of a type; no aspect expression is allowed + -- ??? Once the exact rule for this aspect is ready, we will + -- likely reject concurrent types, etc., so let's keep the code + -- for types and variable separate. + + if Is_First_Subtype (E) then + if Present (Expr) then + Error_Msg_N ("illegal aspect % expression", Expr); + end if; + + -- Annotation of a variable; no aspect expression is allowed + + elsif Ekind (E) = E_Variable then + if Present (Expr) then + Error_Msg_N ("illegal aspect % expression", Expr); + end if; + + -- Annotation of a subprogram; aspect expression is required + + elsif Is_Subprogram (E) then + if Present (Expr) then + + -- Subprogram and its formal parameters must be visible + -- when analyzing the aspect expression. + + pragma Assert (not In_Open_Scopes (E)); + + Push_Scope (E); + + if Is_Generic_Subprogram (E) then + Install_Generic_Formals (E); + else + Install_Formals (E); + end if; + + -- Aspect expression is either an aggregate with list of + -- parameters (and possibly the Result attribute for a + -- function). + + if Nkind (Expr) = N_Aggregate then + + -- Component associations are not allowed in the + -- aspect expression aggregate. + + if Present (Component_Associations (Expr)) then + Error_Msg_N ("illegal aspect % expression", Expr); + else + declare + Param : Node_Id := First (Expressions (Expr)); + + begin + while Present (Param) loop + Analyze_Relaxed_Parameter (E, Param, Seen); + Next (Param); + end loop; + end; + end if; + + -- Mark the aggregate expression itself as analyzed; + -- its subexpressions were marked when they themselves + -- were analyzed. + + Set_Analyzed (Expr); + + -- Otherwise, it is a single name of a subprogram + -- parameter (or possibly the Result attribute for + -- a function). + + else + Analyze_Relaxed_Parameter (E, Expr, Seen); + end if; + + End_Scope; + else + Error_Msg_N ("missing expression for aspect %", N); + end if; + + else + Error_Msg_N ("inappropriate entity for aspect %", E); + end if; + end Analyze_Aspect_Relaxed_Initialization; + ----------------------- -- Make_Aitem_Pragma -- ----------------------- @@ -3332,6 +3508,12 @@ package body Sem_Ch13 is end; end if; + -- Relaxed_Initialization + + when Aspect_Relaxed_Initialization => + Analyze_Aspect_Relaxed_Initialization; + goto Continue; + -- Secondary_Stack_Size -- Aspect Secondary_Stack_Size needs to be converted into a @@ -9942,6 +10124,7 @@ package body Sem_Ch13 is | Aspect_Refined_Global | Aspect_Refined_Post | Aspect_Refined_State + | Aspect_Relaxed_Initialization | Aspect_SPARK_Mode | Aspect_Test_Case | Aspect_Unimplemented diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 2e9a3d0758c..2431b260e67 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2814,7 +2814,7 @@ package body Sem_Ch3 is if Present (L) then Context := Parent (L); - -- Certain contract annocations have forward visibility semantics and + -- Certain contract annotations have forward visibility semantics and -- must be analyzed after all declarative items have been processed. -- This timing ensures that entities referenced by such contracts are -- visible. diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index a7356c749cc..2b63617b42c 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -11798,7 +11798,7 @@ package body Sem_Prag is -- SIMPLE_OPTION -- | NAME_VALUE_OPTION - -- SIMPLE_OPTION ::= Ghost | Synchronous + -- SIMPLE_OPTION ::= Ghost | Relaxed_Initialization | Synchronous -- NAME_VALUE_OPTION ::= -- Part_Of => ABSTRACT_STATE @@ -11868,15 +11868,16 @@ package body Sem_Prag is is -- Flags used to verify the consistency of options - AR_Seen : Boolean := False; - AW_Seen : Boolean := False; - ER_Seen : Boolean := False; - EW_Seen : Boolean := False; - External_Seen : Boolean := False; - Ghost_Seen : Boolean := False; - Others_Seen : Boolean := False; - Part_Of_Seen : Boolean := False; - Synchronous_Seen : Boolean := False; + AR_Seen : Boolean := False; + AW_Seen : Boolean := False; + ER_Seen : Boolean := False; + EW_Seen : Boolean := False; + External_Seen : Boolean := False; + Ghost_Seen : Boolean := False; + Others_Seen : Boolean := False; + Part_Of_Seen : Boolean := False; + Relaxed_Initialization_Seen : Boolean := False; + Synchronous_Seen : Boolean := False; -- Flags used to store the static value of all external states' -- expressions. @@ -12357,6 +12358,12 @@ package body Sem_Prag is Check_Duplicate_Option (Opt, Synchronous_Seen); Check_Ghost_Synchronous; + -- Relaxed_Initialization + + elsif Chars (Opt) = Name_Relaxed_Initialization then + Check_Duplicate_Option + (Opt, Relaxed_Initialization_Seen); + -- Option Part_Of without an encapsulating state is -- illegal (SPARK RM 7.1.4(8)). diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index a1bf0ae5b2d..9f97f7dfb4f 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -12424,6 +12424,123 @@ package body Sem_Util is end if; end Has_Private_Component; + -------------------------------- + -- Has_Relaxed_Initialization -- + -------------------------------- + + function Has_Relaxed_Initialization (E : Entity_Id) return Boolean is + + function Denotes_Relaxed_Parameter + (Expr : Node_Id; + Param : Entity_Id) + return Boolean; + -- Returns True iff expression Expr denotes a formal parameter or + -- function Param (through its attribute Result). + + ------------------------------- + -- Denotes_Relaxed_Parameter -- + ------------------------------- + + function Denotes_Relaxed_Parameter + (Expr : Node_Id; + Param : Entity_Id) + return Boolean + is + begin + if Nkind_In (Expr, N_Identifier, N_Expanded_Name) then + return Entity (Expr) = Param; + else + pragma Assert (Is_Attribute_Result (Expr)); + return Entity (Prefix (Expr)) = Param; + end if; + end Denotes_Relaxed_Parameter; + + -- Start of processing for Has_Relaxed_Initialization + + begin + -- When analyzing, we checked all syntax legality rules for the aspect + -- Relaxed_Initialization, but didn't store the property anywhere (e.g. + -- as an Einfo flag). To query the property we look directly at the AST, + -- but now without any syntactic checks. + + case Ekind (E) is + -- Abstract states have option Relaxed_Initialization + + when E_Abstract_State => + return Is_Relaxed_Initialization_State (E); + + -- Variables have this aspect attached directly + + when E_Variable => + return Has_Aspect (E, Aspect_Relaxed_Initialization); + + -- Types have this aspect attached directly (though we only allow it + -- to be specified for the first subtype). + + when Type_Kind => + pragma Assert (Is_First_Subtype (E)); + return Has_Aspect (E, Aspect_Relaxed_Initialization); + + -- Formal parameters and functions have the Relaxed_Initialization + -- aspect attached to the subprogram entity and must be listed in + -- the aspect expression. + + when Formal_Kind + | E_Function + => + declare + Subp_Id : Entity_Id; + Aspect_Expr : Node_Id; + Param_Expr : Node_Id; + + begin + if Is_Formal (E) then + Subp_Id := Scope (E); + else + Subp_Id := E; + end if; + + if Has_Aspect (Subp_Id, Aspect_Relaxed_Initialization) then + Aspect_Expr := + Find_Value_Of_Aspect (E, Aspect_Relaxed_Initialization); + + -- Aspect expression is either an aggregate, e.g.: + -- + -- function F (X : Integer) return Integer + -- with Relaxed_Initialization => (X, F'Result); + + if Nkind (Aspect_Expr) = N_Aggregate then + + Param_Expr := First (Expressions (Aspect_Expr)); + + while Present (Param_Expr) loop + if Denotes_Relaxed_Parameter (Param_Expr, E) then + return True; + end if; + + Next (Param_Expr); + end loop; + + return False; + + -- or it is a single identifier, e.g.: + -- + -- function F (X : Integer) return Integer + -- with Relaxed_Initialization => X; + + else + return Denotes_Relaxed_Parameter (Aspect_Expr, E); + end if; + else + return False; + end if; + end; + + when others => + raise Program_Error; + end case; + end Has_Relaxed_Initialization; + ---------------------- -- Has_Signed_Zeros -- ---------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index a6d913935da..5aac8b8dc80 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1380,6 +1380,11 @@ package Sem_Util is -- Check if a type has a (sub)component of a private type that has not -- yet received a full declaration. + function Has_Relaxed_Initialization (E : Entity_Id) return Boolean; + -- Returns True iff entity E, which can be either a type, a variable, an + -- abstract state or a function, is subject to the Relaxed_Initialization + -- aspect. + function Has_Signed_Zeros (E : Entity_Id) return Boolean; -- Determines if the floating-point type E supports signed zeros. -- Returns False if E is not a floating-point type. diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 871178814f4..8d6ba414da3 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -148,6 +148,7 @@ package Snames is Name_Dimension_System : constant Name_Id := N + $; Name_Disable_Controlled : constant Name_Id := N + $; Name_Dynamic_Predicate : constant Name_Id := N + $; + Name_Relaxed_Initialization : constant Name_Id := N + $; Name_Static_Predicate : constant Name_Id := N + $; Name_Synchronization : constant Name_Id := N + $; Name_Unimplemented : constant Name_Id := N + $; @@ -953,6 +954,7 @@ package Snames is Name_Has_Tagged_Values : constant Name_Id := N + $; -- GNAT Name_Identity : constant Name_Id := N + $; Name_Implicit_Dereference : constant Name_Id := N + $; -- GNAT + Name_Initialized : constant Name_Id := N + $; -- GNAT Name_Integer_Value : constant Name_Id := N + $; -- GNAT Name_Invalid_Value : constant Name_Id := N + $; -- GNAT Name_Iterator_Element : constant Name_Id := N + $; -- GNAT @@ -1636,6 +1638,7 @@ package Snames is Attribute_Has_Tagged_Values, Attribute_Identity, Attribute_Implicit_Dereference, + Attribute_Initialized, Attribute_Integer_Value, Attribute_Invalid_Value, Attribute_Iterator_Element, -- 2.30.2