diff mbox series

[COMMITTED] ada: Fix expression pretty-printer for SPARK counterexamples

Message ID 20230523080749.1872946-1-poulhies@adacore.com
State New
Headers show
Series [COMMITTED] ada: Fix expression pretty-printer for SPARK counterexamples | expand

Commit Message

Marc Poulhiès May 23, 2023, 8:07 a.m. UTC
From: Piotr Trojanek <trojanek@adacore.com>

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 mbox series

Patch

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,