From patchwork Tue May 23 08:07:49 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Marc_Poulhi=C3=A8s?= X-Patchwork-Id: 1784942 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@legolas.ozlabs.org Authentication-Results: legolas.ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=8.43.85.97; helo=sourceware.org; envelope-from=gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: legolas.ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.a=rsa-sha256 header.s=default header.b=T5lxrkY9; dkim-atps=neutral Received: from sourceware.org (server2.sourceware.org [8.43.85.97]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature ECDSA (P-384) server-digest SHA384) (No client certificate requested) by legolas.ozlabs.org (Postfix) with ESMTPS id 4QQRnz4Fpsz2020 for ; Tue, 23 May 2023 18:10:31 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 80325388265C for ; Tue, 23 May 2023 08:10:29 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 80325388265C DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1684829429; bh=bZA2Ragdxxk7sZCvl5mcscFEly+v/W/uqZpw1mCUyW8=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=T5lxrkY9MFxK6u8wPm6DZVgZLn0+b49qGzFko3GEbL74U/cHmvm5Kt8jqYujo4sLD pjSPJYhPZeHP9/ygbLhqUnEHaT6c4BQHUf+rg0U5dE0VR6H2EnIovx+gNhxuATu72q yjD+QdwRbDGakbnFhMGJaYtjoo33vf5X+LmU1TW0= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x333.google.com (mail-wm1-x333.google.com [IPv6:2a00:1450:4864:20::333]) by sourceware.org (Postfix) with ESMTPS id DF306385700C for ; Tue, 23 May 2023 08:07:52 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org DF306385700C Received: by mail-wm1-x333.google.com with SMTP id 5b1f17b1804b1-3f427118644so69776115e9.0 for ; Tue, 23 May 2023 01:07:52 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1684829271; x=1687421271; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=bZA2Ragdxxk7sZCvl5mcscFEly+v/W/uqZpw1mCUyW8=; b=AICdO14Hvv6C8qXjP7y355WjtTRn1P/z/F5eSWQX5VRUjpjfbC61IU8GkJW7GzW2Ra K9NFWSm4w7EfIG/6DhegAi9tS9tLfFqy04txsN2D98e2RO8gF2/1+JxwaSA9VZ/Ul2eG zMWQwN//qSKU4F6D+R7o60h5yfejCJJk9MPfhfZSQh+nK6tn04BeZIOQguBJ+YLaPt+6 gTNMpeZMzIK8lEv6bBWapCg0vatvPmFWAI1p33APNMQf5sFr25zWHi7vm3UHXJOBnUiM vvUURecC8V6EtagZCH8qW5tZYBEYqYn/hzNXl26hHmJT0Sl1TmTjvdvi0XrxdS1CNcNV gVqw== X-Gm-Message-State: AC+VfDx/c1kTfNHcHVXxYe2J5MuqdA41LV1/qbrWYOcVWUmyaj1twohc Uk55scdsStt36W3bzq6+dnoza2uIpfnagHfI74PsrQ== X-Google-Smtp-Source: ACHHUZ4Eflq858Xv05NoSpJRgTE0fFLpCJqEHQocXmFCWmCGx02AJaowPWp1Ll05Ued1kEaZVwBcPg== X-Received: by 2002:a05:600c:2209:b0:3f6:2ae:230e with SMTP id z9-20020a05600c220900b003f602ae230emr5354722wml.3.1684829270629; Tue, 23 May 2023 01:07:50 -0700 (PDT) Received: from poulhies-Precision-5550.telnowedge.local (lmontsouris-659-1-24-67.w81-250.abo.wanadoo.fr. [81.250.175.67]) by smtp.gmail.com with ESMTPSA id q10-20020a1cf30a000000b003f423508c6bsm10611263wmq.44.2023.05.23.01.07.49 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 23 May 2023 01:07:50 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [COMMITTED] ada: Fix expression pretty-printer for SPARK counterexamples Date: Tue, 23 May 2023 10:07:49 +0200 Message-Id: <20230523080749.1872946-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.2 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: =?utf-8?q?Marc_Poulhi=C3=A8s_via_Gcc-patches?= From: =?utf-8?q?Marc_Poulhi=C3=A8s?= Reply-To: =?utf-8?q?Marc_Poulhi=C3=A8s?= Errors-To: gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org Sender: "Gcc-patches" From: Piotr Trojanek The expression pretty-printer that is used for SPARK counterexamples was essentially duplicating the logic of First_Node/Last_Node and First_Sloc/Last_Sloc routines. Now it simply reuses those routines. gcc/ada/ * errout.adb (Paren_Required): New subsidiary routine for better handling of parentheses in First_Node/Last_Node. (First_Sloc, Last_Sloc): Use Get_Source_File_Index to correctly handle generic instances and inlined subprograms; tune handling of parentheses; improve handling of literals. * pprint.adb (Expression_Image): Simplify using First_Sloc/Last_Sloc. * sem_ch6.adb (Analyze_Expression_Function): Remove parenthesis when relocating expression from expression function to simple return statement. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/errout.adb | 97 ++++++++++-- gcc/ada/pprint.adb | 377 ++++++-------------------------------------- gcc/ada/sem_ch6.adb | 7 + 3 files changed, 146 insertions(+), 335 deletions(-) diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb index a82aff5266b..0a36a1d7466 100644 --- a/gcc/ada/errout.adb +++ b/gcc/ada/errout.adb @@ -50,6 +50,7 @@ with Sinfo.Nodes; use Sinfo.Nodes; with Sinfo.Utils; use Sinfo.Utils; with Snames; use Snames; with Stand; use Stand; +with Stringt; use Stringt; with Stylesw; use Stylesw; with System.OS_Lib; with Uname; use Uname; @@ -139,6 +140,11 @@ package body Errout is -- indicates if there are errors attached to the line, which forces -- listing on, even in the presence of pragma List (Off). + function Paren_Required (N : Node_Id) return Boolean; + -- Subsidiary to First_Sloc and Last_Sloc. Returns True iff parentheses + -- around node N are required by the Ada syntax, e.g. when N is an + -- expression of a qualified expression. + procedure Set_Msg_Insertion_Column; -- Handle column number insertion (@ insertion character) @@ -1845,7 +1851,7 @@ package body Errout is ---------------- function First_Sloc (N : Node_Id) return Source_Ptr is - SI : constant Source_File_Index := Source_Index (Get_Source_Unit (N)); + SI : constant Source_File_Index := Get_Source_File_Index (Sloc (N)); SF : constant Source_Ptr := Source_First (SI); SL : constant Source_Ptr := Source_Last (SI); Src : constant Source_Buffer_Ptr := Source_Text (SI); @@ -1869,6 +1875,12 @@ package body Errout is -- values), but this is only for an error message so it is good enough. Node_Loop : loop + -- Include parentheses around the top node, except when they are + -- required by the syntax of the parent node. + + exit Node_Loop when F = N + and then Paren_Required (N); + Paren_Loop : for J in 1 .. Paren_Count (F) loop -- We don't look more than 12 characters behind the current @@ -1964,7 +1976,7 @@ package body Errout is --------------- function Last_Sloc (N : Node_Id) return Source_Ptr is - SI : constant Source_File_Index := Source_Index (Get_Source_Unit (N)); + SI : constant Source_File_Index := Get_Source_File_Index (Sloc (N)); SF : constant Source_Ptr := Source_First (SI); SL : constant Source_Ptr := Source_Last (SI); Src : constant Source_Buffer_Ptr := Source_Text (SI); @@ -1979,21 +1991,69 @@ package body Errout is return S; end if; - -- Skip past an identifier + -- For string and character literals simply forward the sloc by their + -- length including the closing quotes. Perhaps we should do something + -- special for multibyte characters, but this code is only used to emit + -- error messages, so it is not worth the effort. - while S in SF .. SL - 1 - and then Src (S + 1) - in - '0' .. '9' | 'a' .. 'z' | 'A' .. 'Z' | '.' | '_' - loop - S := S + 1; - end loop; + case Nkind (F) is + when N_String_Literal => + return S + Source_Ptr (String_Length (Strval (F))) + 1; + + when N_Character_Literal => + return S + 2; + + -- Skip past numeric literals, but they allow a wider set of + -- characters than keywords and identifiers. + + when N_Integer_Literal => + while S in SF .. SL - 1 + and then Src (S + 1) + in + '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_' | '#' | '+' | '-' + loop + S := S + 1; + end loop; + + when N_Real_Literal => + declare + Dot_Seen : Boolean := False; + begin + while S in SF .. SL - 1 + and then + (Src (S + 1) in '0' .. '9' + | 'a' .. 'f' | 'A' .. 'F' + | '_' | '#' | '+' | '-' + or else (Src (S + 1) = '.' and then not Dot_Seen)) + loop + Dot_Seen := Src (S + 1) = '.'; + S := S + 1; + end loop; + end; + + -- For other nodes simply skip past a keyword/identifier + + when others => + while S in SF .. SL - 1 + and then Src (S + 1) + in + '0' .. '9' | 'a' .. 'z' | 'A' .. 'Z' | '_' + loop + S := S + 1; + end loop; + end case; -- The following circuit attempts at crawling up the tree from the -- Last_Node, adjusting the Sloc value for any parentheses we know -- are present, similarly to what is done in First_Sloc. Node_Loop : loop + -- Include parentheses around the top node, except when they are + -- required by the syntax of the parent node. + + exit Node_Loop when F = N + and then Paren_Required (N); + Paren_Loop : for J in 1 .. Paren_Count (F) loop -- We don't look more than 12 characters after the current @@ -3298,6 +3358,23 @@ package body Errout is end if; end Output_Source_Line; + -------------------- + -- Paren_Required -- + -------------------- + + function Paren_Required (N : Node_Id) return Boolean is + begin + -- In a qualifed_expression the expression part needs to be enclosed in + -- parentheses. + + if Nkind (Parent (N)) = N_Qualified_Expression then + return N = Expression (Parent (N)); + + else + return False; + end if; + end Paren_Required; + ----------------------------- -- Remove_Warning_Messages -- ----------------------------- diff --git a/gcc/ada/pprint.adb b/gcc/ada/pprint.adb index 1b97630179b..8add10c8f22 100644 --- a/gcc/ada/pprint.adb +++ b/gcc/ada/pprint.adb @@ -652,11 +652,7 @@ package body Pprint is -- Local variables - Append_Paren : Natural := 0; - Left : Node_Id := Original_Node (Expr); - Right : Node_Id := Original_Node (Expr); - - Left_Sloc, Right_Sloc : Source_Ptr; + Left, Right : Source_Ptr; -- Start of processing for Expression_Image @@ -710,345 +706,76 @@ package body Pprint is -- Compute left (start) and right (end) slocs for the expression - loop - case Nkind (Left) is - when N_And_Then - | N_Binary_Op - | N_Membership_Test - | N_Or_Else - => - Left := Original_Node (Left_Opnd (Left)); - - when N_Attribute_Reference - | N_Expanded_Name - | N_Explicit_Dereference - | N_Indexed_Component - | N_Reference - | N_Selected_Component - | N_Slice - => - Left := Original_Node (Prefix (Left)); - - when N_Defining_Program_Unit_Name - | N_Designator - => - Left := Original_Node (Name (Left)); - - when N_Range => - Left := Original_Node (Low_Bound (Left)); - - when N_Qualified_Expression - | N_Type_Conversion - => - Left := Original_Node (Subtype_Mark (Left)); - - -- Examine parameters of function calls, because they might be - -- coming from rewriting of the prefix notation. - - when N_Function_Call => - declare - Param : Node_Id := First (Parameter_Associations (Left)); - begin - Left := Original_Node (Name (Left)); + Left := First_Sloc (Expr); + Right := Last_Sloc (Expr); - while Present (Param) loop - if Nkind (Param) /= N_Parameter_Association - and then Sloc (Original_Node (Param)) < Sloc (Left) - then - Left := Original_Node (Param); - end if; - Next (Param); - end loop; - end; + if Left > Right then + return Default; + end if; - -- For any other item, quit loop + declare + Scn : Source_Ptr := Left; + Src : constant not null Source_Buffer_Ptr := + Source_Text (Get_Source_File_Index (Scn)); + + Threshold : constant := 256; + Buffer : String (1 .. Natural (Right - Left + 1)); + Index : Natural := 0; + Skipping_Comment : Boolean := False; + Underscore : Boolean := False; + begin + while Scn <= Right loop + case Src (Scn) is - when others => - exit; - end case; - end loop; + -- Give up on non ASCII characters - loop - case Nkind (Right) is - when N_Membership_Test - | N_Op - | N_Short_Circuit - => - Right := Original_Node (Right_Opnd (Right)); + when Character'Val (128) .. Character'Last => + Index := 0; + exit; - when N_Attribute_Reference => - declare - Exprs : constant List_Id := Expressions (Right); - begin - if Present (Exprs) then - Right := Original_Node (Last (Expressions (Right))); - Append_Paren := Append_Paren + 1; - else - exit; + when ' ' + | ASCII.HT + => + if not Skipping_Comment and then not Underscore then + Underscore := True; + Index := Index + 1; + Buffer (Index) := ' '; end if; - end; - when N_Expanded_Name - | N_Selected_Component - => - Right := Original_Node (Selector_Name (Right)); - - when N_Qualified_Expression - | N_Type_Conversion - => - Right := Original_Node (Expression (Right)); - Append_Paren := Append_Paren + 1; - - when N_Unchecked_Type_Conversion => - Right := Original_Node (Expression (Right)); + -- CR/LF/FF is the end of any comment - when N_Designator => - Right := Original_Node (Identifier (Right)); + when ASCII.CR + | ASCII.FF + | ASCII.LF + => + Skipping_Comment := False; - when N_Defining_Program_Unit_Name => - Right := Original_Node (Defining_Identifier (Right)); + when others => + Underscore := False; - when N_Range_Constraint => - Right := Original_Node (Range_Expression (Right)); + if not Skipping_Comment then - when N_Range => - Right := Original_Node (High_Bound (Right)); - - when N_Parameter_Association => - Right := Original_Node (Explicit_Actual_Parameter (Right)); - - when N_Indexed_Component => - Right := Original_Node (Last (Expressions (Right))); - Append_Paren := Append_Paren + 1; - - when N_Function_Call => - declare - Has_Source_Param : Boolean := False; - -- True iff function call has a parameter coming from source - - Param : Node_Id; - - begin - -- Avoid source position confusion associated with - -- parameters for which Comes_From_Source is False. - - Param := First (Parameter_Associations (Right)); - while Present (Param) loop - if Comes_From_Source (Original_Node (Param)) then - if Nkind (Param) = N_Parameter_Association then - Right := - Original_Node (Explicit_Actual_Parameter (Param)); - else - Right := Original_Node (Param); - end if; - Has_Source_Param := True; - end if; + -- Ignore comment - Next (Param); - end loop; - - if Has_Source_Param then - Append_Paren := Append_Paren + 1; - else - Right := Original_Node (Name (Right)); - end if; - end; - - when N_Quantified_Expression => - Right := Original_Node (Condition (Right)); - Append_Paren := Append_Paren + 1; - - when N_Aggregate | N_Extension_Aggregate => - declare - Aggr : constant Node_Id := Right; - Sub : Node_Id; - - begin - Sub := First (Expressions (Aggr)); - while Present (Sub) loop - if Sloc (Sub) > Sloc (Right) then - Right := Original_Node (Sub); - end if; - - Next (Sub); - end loop; - - Sub := First (Component_Associations (Aggr)); - while Present (Sub) loop - if Box_Present (Sub) - and then Sloc (Original_Node (Sub)) > Sloc (Right) - then - Right := Original_Node (Sub); - elsif - Sloc (Original_Node (Expression (Sub))) > Sloc (Right) - then - Right := Original_Node (Expression (Sub)); + if Src (Scn) = '-' and then Src (Scn + 1) = '-' then + Skipping_Comment := True; + else + Index := Index + 1; + Buffer (Index) := Src (Scn); end if; - - Next (Sub); - end loop; - - exit when Right = Aggr - or else Nkind (Right) = N_Component_Association; - - Append_Paren := Append_Paren + 1; - end; - - when N_Slice => - Right := Original_Node (Discrete_Range (Right)); - Append_Paren := Append_Paren + 1; - - -- subtype_indication might appear inside allocator - - when N_Subtype_Indication => - Right := Original_Node (Constraint (Right)); - - when N_Index_Or_Discriminant_Constraint => - Right := Original_Node (Last (Constraints (Right))); - - when N_Raise_Expression => - declare - Exp : constant Node_Id := Expression (Right); - begin - if Present (Exp) then - Right := Original_Node (Exp); - else - Right := Original_Node (Name (Right)); - end if; - end; - - when N_If_Expression => - declare - Cond_Expr : constant Node_Id := First (Expressions (Right)); - Then_Expr : constant Node_Id := Next (Cond_Expr); - Else_Expr : constant Node_Id := Next (Then_Expr); - begin - -- The ELSE branch might be either missing or it might be - -- be a dummy TRUE that comes from the expansion. - - if Present (Else_Expr) - and then Comes_From_Source (Original_Node (Else_Expr)) - then - Right := Original_Node (Else_Expr); - else - Right := Original_Node (Then_Expr); end if; - end; - - when N_Allocator => - Right := Original_Node (Expression (Right)); - - when N_Discriminant_Association => - Right := Original_Node (Expression (Right)); - - -- For all other items, quit the loop - - when others => - exit; - end case; - end loop; - - -- We could just use Sinput.Sloc_Range, but we still need Append_Paren. - -- Make sure that we indeed got the left and right-most nodes. - - Sinput.Sloc_Range (Expr, Left_Sloc, Right_Sloc); + end case; - pragma Assert (Left_Sloc = Sloc (Left)); - pragma Assert (Right_Sloc = Sloc (Right)); + -- Give up on too long strings - declare - Scn : Source_Ptr := Left_Sloc; - End_Sloc : constant Source_Ptr := Right_Sloc; - Src : constant Source_Buffer_Ptr := - Source_Text (Get_Source_File_Index (Scn)); - - begin - if Scn > End_Sloc then - return Default; - end if; - - declare - Threshold : constant := 256; - Buffer : String (1 .. Natural (End_Sloc - Scn)); - Index : Natural := 0; - Skipping_Comment : Boolean := False; - Underscore : Boolean := False; - - begin - if Right /= Expr then - while Scn < End_Sloc loop - case Src (Scn) is - - -- Give up on non ASCII characters - - when Character'Val (128) .. Character'Last => - Append_Paren := 0; - Index := 0; - Right := Expr; - exit; - - when ' ' - | ASCII.HT - => - if not Skipping_Comment and then not Underscore then - Underscore := True; - Index := Index + 1; - Buffer (Index) := ' '; - end if; - - -- CR/LF/FF is the end of any comment - - when ASCII.CR - | ASCII.FF - | ASCII.LF - => - Skipping_Comment := False; - - when others => - Underscore := False; - - if not Skipping_Comment then - - -- Ignore comment - - if Src (Scn) = '-' and then Src (Scn + 1) = '-' then - Skipping_Comment := True; - - else - Index := Index + 1; - Buffer (Index) := Src (Scn); - end if; - end if; - end case; - - -- Give up on too long strings - - if Index >= Threshold then - return Buffer (1 .. Index) & "..."; - end if; - - Scn := Scn + 1; - end loop; + if Index >= Threshold then + return Buffer (1 .. Index) & "..."; end if; - if Index < 1 then - declare - S : constant String := Expr_Name (Right); - begin - if S = "..." then - return Default; - else - return S; - end if; - end; + Scn := Scn + 1; + end loop; - else - return - Buffer (1 .. Index) - & Expr_Name (Right, False) - & (1 .. Append_Paren => ')'); - end if; - end; + return Buffer (1 .. Index); end; end Expression_Image; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 0b374c2f01d..992688cf092 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -361,6 +361,13 @@ package body Sem_Ch6 is Ret := Make_Simple_Return_Statement (LocX, Expr); + -- Remove parens around the expression, so that if the expression will + -- appear without them when pretty-printed in error messages. + + if Paren_Count (Expr) > 0 then + Set_Paren_Count (Expr, Paren_Count (Expr) - 1); + end if; + New_Body := Make_Subprogram_Body (Loc, Specification => New_Spec,