From aa2f48d2e6710bcc0e4d0404f6bb05149a8a8427 Mon Sep 17 00:00:00 2001 From: charlet Date: Fri, 13 Mar 2015 13:28:15 +0000 Subject: [PATCH] 2015-03-13 Claire Dross * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not inline subprograms with unconstrained record parameters containing Itype declarations. * sinfo.ads Document GNATprove assumption that type should match in the AST. * sem_ch6.adb (Analyze_Subprogram_Body_Contract): Do not check for Refined_Depends and Refined_Globals contracts as they are optional. 2015-03-13 Ed Schonberg * sem_ch12.adb (Instantiate_Type): For a floating-point type, capture dimension info if any, because the generated subtype declaration does not come from source and will not process dimensions. * sem_dim,adb (Analyze_Dimension_Extension_Or_Record_Aggregate): Do not analyze expressions with an initialization procedure because aggregates will have been checked at the point of record declaration. 2015-03-13 Robert Dewar * aspects.ads, aspects.adb: Add entries for aspect Unimplemented. * einfo.ads, einfo.adb (Is_Unimplemented): New flag. * sem_ch13.adb: Add dummy entry for aspect Unimplemented. * snames.ads-tmpl: Add entry for Name_Unimplemented. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@221420 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/ChangeLog | 28 +++++++++++++++++ gcc/ada/aspects.adb | 3 +- gcc/ada/aspects.ads | 6 +++- gcc/ada/einfo.adb | 13 +++++++- gcc/ada/einfo.ads | 16 ++++++++-- gcc/ada/inline.adb | 83 ++++++++++++++++++++++++++++++++++++++++++++++++- gcc/ada/sem_ch12.adb | 8 +++++ gcc/ada/sem_ch13.adb | 5 ++- gcc/ada/sem_ch6.adb | 32 ------------------- gcc/ada/sem_dim.adb | 12 +++++-- gcc/ada/sinfo.ads | 11 +++++++ gcc/ada/snames.ads-tmpl | 1 + 12 files changed, 176 insertions(+), 42 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 3b96147..c3a79af 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,31 @@ +2015-03-13 Claire Dross + + * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not inline + subprograms with unconstrained record parameters containing + Itype declarations. + * sinfo.ads Document GNATprove assumption that type should match + in the AST. + * sem_ch6.adb (Analyze_Subprogram_Body_Contract): + Do not check for Refined_Depends and Refined_Globals contracts + as they are optional. + +2015-03-13 Ed Schonberg + + * sem_ch12.adb (Instantiate_Type): For a floating-point type, + capture dimension info if any, because the generated subtype + declaration does not come from source and will not process dimensions. + * sem_dim,adb (Analyze_Dimension_Extension_Or_Record_Aggregate): + Do not analyze expressions with an initialization procedure + because aggregates will have been checked at the point of record + declaration. + +2015-03-13 Robert Dewar + + * aspects.ads, aspects.adb: Add entries for aspect Unimplemented. + * einfo.ads, einfo.adb (Is_Unimplemented): New flag. + * sem_ch13.adb: Add dummy entry for aspect Unimplemented. + * snames.ads-tmpl: Add entry for Name_Unimplemented. + 2015-03-13 Gary Dismukes * style.adb (Missing_Overriding): Apply the diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index 19e49b5..bef432f 100644 --- a/gcc/ada/aspects.adb +++ b/gcc/ada/aspects.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2010-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 2010-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -595,6 +595,7 @@ package body Aspects is Aspect_Thread_Local_Storage => Aspect_Thread_Local_Storage, Aspect_Type_Invariant => Aspect_Invariant, Aspect_Unchecked_Union => Aspect_Unchecked_Union, + Aspect_Unimplemented => Aspect_Unimplemented, Aspect_Universal_Aliasing => Aspect_Universal_Aliasing, Aspect_Universal_Data => Aspect_Universal_Data, Aspect_Unmodified => Aspect_Unmodified, diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 0e01beb..049efae 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2010-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 2010-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -140,6 +140,7 @@ package Aspects is Aspect_Synchronization, Aspect_Test_Case, -- GNAT Aspect_Type_Invariant, + Aspect_Unimplemented, -- GNAT Aspect_Unsuppress, Aspect_Value_Size, -- GNAT Aspect_Variable_Indexing, @@ -369,6 +370,7 @@ package Aspects is Aspect_Synchronization => Name, Aspect_Test_Case => Expression, Aspect_Type_Invariant => Expression, + Aspect_Unimplemented => Optional_Expression, Aspect_Unsuppress => Name, Aspect_Value_Size => Expression, Aspect_Variable_Indexing => Name, @@ -490,6 +492,7 @@ package Aspects is Aspect_Test_Case => Name_Test_Case, Aspect_Type_Invariant => Name_Type_Invariant, Aspect_Unchecked_Union => Name_Unchecked_Union, + Aspect_Unimplemented => Name_Unimplemented, Aspect_Universal_Aliasing => Name_Universal_Aliasing, Aspect_Universal_Data => Name_Universal_Data, Aspect_Unmodified => Name_Unmodified, @@ -717,6 +720,7 @@ package Aspects is Aspect_SPARK_Mode => Never_Delay, Aspect_Synchronization => Never_Delay, Aspect_Test_Case => Never_Delay, + Aspect_Unimplemented => Never_Delay, Aspect_Warnings => Never_Delay, Aspect_Alignment => Rep_Aspect, diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 70dc46f..e215df9 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -584,8 +584,8 @@ package body Einfo is -- Is_Static_Type Flag281 -- Has_Nested_Subprogram Flag282 -- Uplevel_Reference_Noted Flag283 + -- Is_Unimplemented Flag284 - -- (unused) Flag284 -- (unused) Flag285 -- (unused) Flag286 -- (unused) Flag287 @@ -2456,6 +2456,11 @@ package body Einfo is return Flag246 (Id); end Is_Underlying_Record_View; + function Is_Unimplemented (Id : E) return B is + begin + return Flag284 (Id); + end Is_Unimplemented; + function Is_Unsigned_Type (Id : E) return B is begin pragma Assert (Is_Type (Id)); @@ -5398,6 +5403,11 @@ package body Einfo is Set_Flag246 (Id, V); end Set_Is_Underlying_Record_View; + procedure Set_Is_Unimplemented (Id : E; V : B := True) is + begin + Set_Flag284 (Id, V); + end Set_Is_Unimplemented; + procedure Set_Is_Unsigned_Type (Id : E; V : B := True) is begin pragma Assert (Is_Discrete_Or_Fixed_Point_Type (Id)); @@ -8767,6 +8777,7 @@ package body Einfo is W ("Is_True_Constant", Flag163 (Id)); W ("Is_Unchecked_Union", Flag117 (Id)); W ("Is_Underlying_Record_View", Flag246 (Id)); + W ("Is_Unimplemented", Flag284 (Id)); W ("Is_Unsigned_Type", Flag144 (Id)); W ("Is_Valued_Procedure", Flag127 (Id)); W ("Is_Visible_Formal", Flag206 (Id)); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index cd92063..81a77f9 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -2745,8 +2745,8 @@ package Einfo is -- including generic formal parameters. -- Is_Obsolescent (Flag153) --- Defined in all entities. Set for any entity for which a valid pragma --- Obsolescent applies. +-- Defined in all entities. Set for any entity to which a valid pragma +-- or aspect Obsolescent applies. -- Is_Only_Out_Parameter (Flag226) -- Defined in formal parameter entities. Set if this parameter is the @@ -3090,6 +3090,10 @@ package Einfo is -- as its corresponding record type, but whose parent is the full view -- of the parent in the original type extension. +-- Is_Unimplemented (Flag284) +-- Defined in all entities. Set for any entity to which a valid pragma +-- or aspect Unimplemented applies. + -- Is_Unsigned_Type (Flag144) -- Defined in all types, but can be set only for discrete and fixed-point -- type and subtype entities. This flag is only valid if the entity is @@ -5299,6 +5303,7 @@ package Einfo is -- Is_Thunk (Flag225) -- Is_Trivial_Subprogram (Flag235) -- Is_Unchecked_Union (Flag117) + -- Is_Unimplemented (Flag284) -- Is_Visible_Formal (Flag206) -- Kill_Elaboration_Checks (Flag32) -- Kill_Range_Checks (Flag33) @@ -5784,6 +5789,7 @@ package Einfo is -- SPARK_Pragma (Node32) -- Linker_Section_Pragma (Node33) -- Contract (Node34) + -- Import_Pragma (Node35) (non-generic case only) -- Body_Needed_For_SAL (Flag40) -- Contains_Ignored_Ghost_Code (Flag279) -- Default_Expressions_Processed (Flag108) @@ -5951,6 +5957,7 @@ package Einfo is -- Subprograms_For_Type (Node29) -- Linker_Section_Pragma (Node33) -- Contract (Node34) + -- Import_Pragma (Node35) -- Has_Invariants (Flag232) -- Is_Machine_Code_Subprogram (Flag137) -- Is_Pure (Flag44) @@ -6089,6 +6096,7 @@ package Einfo is -- SPARK_Pragma (Node32) -- Linker_Section_Pragma (Node33) -- Contract (Node34) + -- Import_Pragma (Node35) (non-generic case only) -- Body_Needed_For_SAL (Flag40) -- Contains_Ignored_Ghost_Code (Flag279) -- Delay_Cleanups (Flag114) @@ -6894,6 +6902,7 @@ package Einfo is function Is_True_Constant (Id : E) return B; function Is_Unchecked_Union (Id : E) return B; function Is_Underlying_Record_View (Id : E) return B; + function Is_Unimplemented (Id : E) return B; function Is_Unsigned_Type (Id : E) return B; function Is_Valued_Procedure (Id : E) return B; function Is_Visible_Formal (Id : E) return B; @@ -7548,6 +7557,7 @@ package Einfo is procedure Set_Is_True_Constant (Id : E; V : B := True); procedure Set_Is_Unchecked_Union (Id : E; V : B := True); procedure Set_Is_Underlying_Record_View (Id : E; V : B := True); + procedure Set_Is_Unimplemented (Id : E; V : B := True); procedure Set_Is_Unsigned_Type (Id : E; V : B := True); procedure Set_Is_Valued_Procedure (Id : E; V : B := True); procedure Set_Is_Visible_Formal (Id : E; V : B := True); @@ -8352,6 +8362,7 @@ package Einfo is pragma Inline (Is_Type); pragma Inline (Is_Unchecked_Union); pragma Inline (Is_Underlying_Record_View); + pragma Inline (Is_Unimplemented); pragma Inline (Is_Unsigned_Type); pragma Inline (Is_Valued_Procedure); pragma Inline (Is_Visible_Formal); @@ -8807,6 +8818,7 @@ package Einfo is pragma Inline (Set_Is_True_Constant); pragma Inline (Set_Is_Unchecked_Union); pragma Inline (Set_Is_Underlying_Record_View); + pragma Inline (Set_Is_Unimplemented); pragma Inline (Set_Is_Unsigned_Type); pragma Inline (Set_Is_Valued_Procedure); pragma Inline (Set_Is_Visible_Formal); diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 9a60bef..7db46cf 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1335,6 +1335,11 @@ package body Inline is (Spec_Id : Entity_Id; Body_Id : Entity_Id) return Boolean is + function Has_Parameter_With_Discriminant_Dependent_Fields + (Id : Entity_Id) return Boolean; + -- Returns true if the subprogram as parameters of an unconstrained + -- record types with fields whose types depend on a discriminant. + function Has_Some_Contract (Id : Entity_Id) return Boolean; -- Returns True if subprogram Id has any contract (Pre, Post, Global, -- Depends, etc.) @@ -1351,6 +1356,73 @@ package body Inline is -- Returns True if subprogram Id was defined originally as an expression -- function. + ------------------------------------------------------ + -- Has_Parameter_With_Discriminant_Dependent_Fields -- + ------------------------------------------------------ + + function Has_Parameter_With_Discriminant_Dependent_Fields + (Id : Entity_Id) return Boolean + is + E : Entity_Id := Id; + Spec : Node_Id := Parent (E); + + begin + -- Get the specification of the subprogram. Go through alias if + -- needed. + + if Nkind (Spec) = N_Defining_Program_Unit_Name then + Spec := Parent (Spec); + end if; + + while Nkind (Spec) not in N_Subprogram_Specification loop + pragma Assert (Present (Alias (E))); + E := Alias (E); + Spec := Parent (E); + + if Nkind (Spec) = N_Defining_Program_Unit_Name then + Spec := Parent (Spec); + end if; + end loop; + + declare + Params : constant List_Id := Parameter_Specifications (Spec); + Param : Node_Id; + Param_Ty : Entity_Id; + + begin + if Is_Non_Empty_List (Params) then + Param := First (Params); + while Present (Param) loop + Param_Ty := Etype (Defining_Identifier (Param)); + + -- If the parameter is an unconstrained record, check if + -- it has components whose types depend on a discriminant. + + if Is_Record_Type (Param_Ty) + and then not Is_Constrained (Param_Ty) + then + declare + Comp : Node_Id := First_Component (Param_Ty); + + begin + while Present (Comp) loop + if Has_Discriminant_Dependent_Constraint (Comp) then + return True; + end if; + + Comp := Next_Component (Comp); + end loop; + end; + end if; + + Param := Next (Param); + end loop; + end if; + end; + + return False; + end Has_Parameter_With_Discriminant_Dependent_Fields; + ----------------------- -- Has_Some_Contract -- ----------------------- @@ -1497,11 +1569,20 @@ package body Inline is elsif Instantiation_Location (Sloc (Id)) /= No_Location then return False; - -- Don't inline predicate functions (treated specially by GNATprove) + -- Do not inline predicate functions (treated specially by GNATprove) elsif Is_Predicate_Function (Id) then return False; + -- Do not inline subprograms with a parameter of an unconstrained + -- record type if it has discrimiant dependent fields. Indeed, with + -- such parameters, the frontend cannot always ensure type compliance + -- in record component accesses (in particular with records containing + -- packed arrays). + + elsif Has_Parameter_With_Discriminant_Dependent_Fields (Id) then + return False; + -- Otherwise, this is a subprogram declared inside the private part of a -- package, or inside a package body, or locally in a subprogram, and it -- does not have any contract. Inline it. diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 424c118..0fa7817 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -12456,6 +12456,14 @@ package body Sem_Ch12 is end; end if; + -- For a floating-point type, capture dimension info if any, because + -- the generated subtype declaration does not come from source and + -- will not process dimensions. + + if Is_Floating_Point_Type (Act_T) then + Copy_Dimensions (Act_T, Subt); + end if; + return Decl_Nodes; end Instantiate_Type; diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 5883e4c..fc23010 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1642,6 +1642,8 @@ package body Sem_Ch13 is -- Processing based on specific aspect case A_Id is + when Aspect_Unimplemented => + null; -- ??? temp for now -- No_Aspect should be impossible @@ -9024,7 +9026,8 @@ package body Sem_Ch13 is Aspect_Refined_Post | Aspect_Refined_State | Aspect_SPARK_Mode | - Aspect_Test_Case => + Aspect_Test_Case | + Aspect_Unimplemented => raise Program_Error; end case; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 929b1c9..2f9e1f5 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -2203,22 +2203,6 @@ package body Sem_Ch6 is if Present (Ref_Global) then Analyze_Refined_Global_In_Decl_Part (Ref_Global); - - -- When the corresponding Global pragma references a state with - -- visible refinement, the body requires Refined_Global. Such a - -- refinement is not required when SPARK checks are suppressed. - - else - Prag := Get_Pragma (Spec_Id, Pragma_Global); - - if SPARK_Mode /= Off - and then Present (Prag) - and then Contains_Refined_State (Prag) - then - Error_Msg_NE - ("body of subprogram& requires global refinement", - Body_Decl, Spec_Id); - end if; end if; -- Refined_Depends must be analyzed after Refined_Global in order to @@ -2226,22 +2210,6 @@ package body Sem_Ch6 is if Present (Ref_Depends) then Analyze_Refined_Depends_In_Decl_Part (Ref_Depends); - - -- When the corresponding Depends pragma references a state with - -- visible refinement, the body requires Refined_Depends. Such a - -- refinement is not required when SPARK checks are suppressed. - - else - Prag := Get_Pragma (Spec_Id, Pragma_Depends); - - if SPARK_Mode /= Off - and then Present (Prag) - and then Contains_Refined_State (Prag) - then - Error_Msg_NE - ("body of subprogram& requires dependance refinement", - Body_Decl, Spec_Id); - end if; end if; end Analyze_Completion_Contract; diff --git a/gcc/ada/sem_dim.adb b/gcc/ada/sem_dim.adb index 37d2f7a..1f98027 100644 --- a/gcc/ada/sem_dim.adb +++ b/gcc/ada/sem_dim.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2011-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 2011-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -27,6 +27,7 @@ with Aspects; use Aspects; with Atree; use Atree; with Einfo; use Einfo; with Errout; use Errout; +with Exp_Util; use Exp_Util; with Lib; use Lib; with Namet; use Namet; with Nlists; use Nlists; @@ -1792,9 +1793,14 @@ package body Sem_Dim is begin -- Aspect is an Ada 2012 feature. Note that there is no need to check - -- dimensions for aggregates that don't come from source. + -- dimensions for aggregates that don't come from source, or if we are + -- within an initialization procedure, whose expressions have been + -- checked at the point of record declaration. - if Ada_Version < Ada_2012 or else not Comes_From_Source (N) then + if Ada_Version < Ada_2012 + or else not Comes_From_Source (N) + or else Inside_Init_Proc + then return; end if; diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 3dc9311..5f057f2 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -617,6 +617,17 @@ package Sinfo is -- checks on empty ranges, which typically appear in deactivated -- code in a particular configuration). + -- 6. Subtypes should match in the AST, even after a generic is + -- instantiated. In particular, GNATprove relies on the fact that, + -- on a selected component, the type of the selected component is + -- the type of the corresponding component in the prefix of the + -- selected component. + -- + -- Note that, in some cases, we know that this rule is broken by the + -- frontend. In particular, if the selected component is a packed + -- array depending on a discriminant of a unconstrained formal object + -- parameter of a generic. + ----------------------- -- Check Flag Fields -- ----------------------- diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 6e1aec8..3781cfc 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -144,6 +144,7 @@ package Snames is Name_Dynamic_Predicate : constant Name_Id := N + $; Name_Static_Predicate : constant Name_Id := N + $; Name_Synchronization : constant Name_Id := N + $; + Name_Unimplemented : constant Name_Id := N + $; -- Some special names used by the expander. Note that the lower case u's -- at the start of these names get translated to extra underscores. These -- 2.7.4