From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 7871) id 161513857B8E; Thu, 14 Sep 2023 12:45:35 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 161513857B8E DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1694695535; bh=D07rfBZb9Oc3/kc9UV5jwRJ0pMh69y7c4Y4nZNG+lg0=; h=From:To:Subject:Date:From; b=DHOx8xlnD4dHu8XgCzZp98Bm2/4A7yM/B23zeZb1bT8cxeaUTJZNGVyhbjreHg8yV Om02MHo54Hk7GrauFEcBjR5U4Ua3N7SXpj2m2EqIMx+uzGeH8wwKAE8bfX5NprK81Q f9djH4CknGd5rDGz451P2Q4TWUc/ltu9WyEqP5Eo= MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Marc Poulhi?s To: gcc-cvs@gcc.gnu.org Subject: [gcc r14-3989] ada: Improve detection of deactivated code for warnings with -gnatwt X-Act-Checkin: gcc X-Git-Author: Yannick Moy X-Git-Refname: refs/heads/master X-Git-Oldrev: fa16e3229499f4c7c5375bd1bc4b713fb1d2e30e X-Git-Newrev: 8517317ce8e9fbea0b4c7a8f87a86d07d95dc8c7 Message-Id: <20230914124535.161513857B8E@sourceware.org> Date: Thu, 14 Sep 2023 12:45:35 +0000 (GMT) List-Id: https://gcc.gnu.org/g:8517317ce8e9fbea0b4c7a8f87a86d07d95dc8c7 commit r14-3989-g8517317ce8e9fbea0b4c7a8f87a86d07d95dc8c7 Author: Yannick Moy Date: Fri Aug 4 15:01:28 2023 +0200 ada: Improve detection of deactivated code for warnings with -gnatwt Switch -gnatwt is used in GNAT to track deleted code. It can be emitted by GNAT on code that is intentionally deactivated for a given configuration. The current test to suppress spurious warnings is not complex enough to detect all such cases. Now improved, by using the same test as used in GNATprove to suppress warnings related to a "statically disabled condition which evaluates to a given value", as described in SPARK UG 7.3.2. gcc/ada/ * exp_util.adb (Is_Statically_Disabled): New function to detect a "statically disabled condition which evaluates to a given value", as described in SPARK UG 7.3.2. (Kill_Dead_Code): Call the new function Is_Statically_Disabled for conditions of if statements. * exp_util.ads (Is_Statically_Disabled): New function spec. Diff: --- gcc/ada/exp_util.adb | 159 ++++++++++++++++++++++++++++++++++++++++++++++++--- gcc/ada/exp_util.ads | 17 ++++++ 2 files changed, 167 insertions(+), 9 deletions(-) diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 5cfadc5245e..b2542d4ae59 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -30,7 +30,6 @@ with Checks; use Checks; with Debug; use Debug; with Einfo; use Einfo; with Einfo.Entities; use Einfo.Entities; -with Einfo.Utils; use Einfo.Utils; with Elists; use Elists; with Errout; use Errout; with Exp_Aggr; use Exp_Aggr; @@ -9401,6 +9400,135 @@ package body Exp_Util is and then Has_Controlling_Result (Id); end Is_Secondary_Stack_Thunk; + ---------------------------- + -- Is_Statically_Disabled -- + ---------------------------- + + function Is_Statically_Disabled + (N : Node_Id; + Value : Boolean; + Include_Valid : Boolean) + return Boolean + is + function Is_Discrete_Literal (N : Node_Id) return Boolean; + -- Returns whether N is an integer, character or enumeration literal + + ------------------------- + -- Is_Discrete_Literal -- + ------------------------- + + function Is_Discrete_Literal (N : Node_Id) return Boolean is + (Nkind (N) in N_Integer_Literal | N_Character_Literal + or else (Nkind (N) in N_Identifier | N_Expanded_Name + and then Ekind (Entity (N)) = E_Enumeration_Literal)); + + Expr_N : constant Node_Id := + (if Is_Static_Expression (N) + and then Entity (N) in Standard_True | Standard_False + and then Is_Rewrite_Substitution (N) + then Original_Node (N) + else N); + + -- Start of processing for Is_Statically_Disabled + + begin + -- A "statically disabled" condition which evaluates to Value is either: + + case Nkind (Expr_N) is + + -- an AND or AND THEN operator when: + -- - Value is True and both operands are statically disabled + -- conditions evaluated to True. + -- - Value is False and at least one operand is a statically disabled + -- condition evaluated to False. + + when N_Op_And | N_And_Then => + return + (if Value then + (Is_Statically_Disabled + (Left_Opnd (Expr_N), Value, Include_Valid) + and then Is_Statically_Disabled + (Right_Opnd (Expr_N), Value, Include_Valid)) + else + (Is_Statically_Disabled + (Left_Opnd (Expr_N), Value, Include_Valid) + or else Is_Statically_Disabled + (Right_Opnd (Expr_N), Value, Include_Valid))); + + -- an OR or OR ELSE operator when: + -- - Value is True and at least one operand is a statically disabled + -- condition evaluated to True. + -- - Value is False and both operands are statically disabled + -- conditions evaluated to False. + + when N_Op_Or | N_Or_Else => + return + (if Value then + (Is_Statically_Disabled + (Left_Opnd (Expr_N), Value, Include_Valid) + or else Is_Statically_Disabled + (Right_Opnd (Expr_N), Value, Include_Valid)) + else + (Is_Statically_Disabled + (Left_Opnd (Expr_N), Value, Include_Valid) + and then Is_Statically_Disabled + (Right_Opnd (Expr_N), Value, Include_Valid))); + + -- a NOT operator when the right operand is a statically disabled + -- condition evaluated to the negation of Value. + + when N_Op_Not => + return Is_Statically_Disabled + (Right_Opnd (Expr_N), not Value, Include_Valid); + + -- a static constant when it is of a boolean type with aspect + -- Warnings Off. + + when N_Identifier | N_Expanded_Name => + return Is_Static_Expression (Expr_N) + and then Value = Is_True (Expr_Value (Expr_N)) + and then Ekind (Entity (Expr_N)) = E_Constant + and then Has_Warnings_Off (Entity (Expr_N)); + + -- a relational_operator where one operand is a static constant with + -- aspect Warnings Off and the other operand is a literal of the + -- corresponding type. + + when N_Op_Compare => + declare + Left : constant Node_Id := Left_Opnd (Expr_N); + Right : constant Node_Id := Right_Opnd (Expr_N); + begin + return + Is_Static_Expression (N) + and then Value = Is_True (Expr_Value (N)) + and then + ((Is_Discrete_Literal (Right) + and then Nkind (Left) in N_Identifier + | N_Expanded_Name + and then Ekind (Entity (Left)) = E_Constant + and then Has_Warnings_Off (Entity (Left))) + or else + (Is_Discrete_Literal (Left) + and then Nkind (Right) in N_Identifier + | N_Expanded_Name + and then Ekind (Entity (Right)) = E_Constant + and then Has_Warnings_Off (Entity (Right)))); + end; + + -- a reference to 'Valid or 'Valid_Scalar if Include_Valid is True + + when N_Attribute_Reference => + return Include_Valid + and then Get_Attribute_Id (Attribute_Name (Expr_N)) in + Attribute_Valid | Attribute_Valid_Scalars + and then Value; + + when others => + return False; + end case; + end Is_Statically_Disabled; + -------------------------------- -- Is_Uninitialized_Aggregate -- -------------------------------- @@ -9577,8 +9705,11 @@ package body Exp_Util is -- if/case statement and either -- a) we are in an instance and the condition/selector -- has a statically known value; or - -- b) the condition/selector is a simple identifier and - -- warnings off is set for this identifier. + -- b) the selector of a case statement is a simple identifier + -- and warnings off is set for this identifier; or + -- c) the condition of an if statement is a "statically + -- disabled" condition which evaluates to False as described + -- in section 7.3.2 of SPARK User's Guide. -- Dead code is common and reasonable in instances, so we don't -- want a warning in that case. @@ -9587,19 +9718,29 @@ package body Exp_Util is begin if Nkind (Parent (N)) = N_If_Statement then C := Condition (Parent (N)); + + if Is_Statically_Disabled + (C, Value => False, Include_Valid => False) + then + W := False; + end if; + elsif Nkind (Parent (N)) = N_Case_Statement_Alternative then C := Expression (Parent (Parent (N))); - end if; - if Present (C) then - if (In_Instance and Compile_Time_Known_Value (C)) - or else (Nkind (C) = N_Identifier - and then Present (Entity (C)) - and then Has_Warnings_Off (Entity (C))) + if Nkind (C) = N_Identifier + and then Present (Entity (C)) + and then Has_Warnings_Off (Entity (C)) then W := False; end if; end if; + + if Present (C) + and then (In_Instance and Compile_Time_Known_Value (C)) + then + W := False; + end if; end; -- Generate warning if not suppressed diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads index 65bb9203009..95ea4403c5d 100644 --- a/gcc/ada/exp_util.ads +++ b/gcc/ada/exp_util.ads @@ -25,6 +25,7 @@ -- Package containing utility procedures used throughout the expander +with Einfo.Utils; use Einfo.Utils; with Exp_Tss; use Exp_Tss; with Namet; use Namet; with Rtsfind; use Rtsfind; @@ -856,6 +857,22 @@ package Exp_Util is -- WARNING: There is a matching C declaration of this subprogram in fe.h + function Is_Statically_Disabled + (N : Node_Id; + Value : Boolean; + Include_Valid : Boolean) + return Boolean + with Pre => Nkind (N) in N_Subexpr and then Is_Boolean_Type (Etype (N)); + -- Returns whether N is a "statically disabled" condition which evaluates + -- to Value, as described in section 7.3.2 of SPARK User's Guide. + -- + -- If Include_Valid is True, a reference to 'Valid or 'Valid_Scalar is + -- considered as disabled for Value=True, which is useful in GNATprove, as + -- proof considers that these attributes always return the value True. In + -- general, Include_Valid is set to True in the proof phase of GNATprove, + -- as 'Valid is assumed to always evaluate to True, but not in the flow + -- analysis phase of GNATprove, which does not make this assumption. + function Is_Untagged_Derivation (T : Entity_Id) return Boolean; -- Returns true if type T is not tagged and is a derived type, -- or is a private type whose completion is such a type.