diff mbox series

[COMMITTED] ada: Move splitting of pre/post aspect expressions to expansion

Message ID 20240513083632.165835-1-poulhies@adacore.com
State New
Headers show
Series [COMMITTED] ada: Move splitting of pre/post aspect expressions to expansion | expand

Commit Message

Marc Poulhiès May 13, 2024, 8:36 a.m. UTC
From: Piotr Trojanek <trojanek@adacore.com>

We split expressions of pre/post aspects into individual conjuncts and
emit messages with their precise location when they fail at runtime.

This was done when processing the aspects and caused inefficiency when
the original expression had to be recovered to detects uses of 'Old that
changed in Ada 2022. This patch moves splitting to expansion.

Conceptually, splitting in expansion is easy, but we need to take care
of locations for inherited pre/post contracts. Previously the location
string was generated while splitting the aspect into pragmas and then
it was manipulated when inheriting the pragmas. Now the location string
is built when installing the Pre'Class check and when splitting the
expression in expansion.

gcc/ada/

	* exp_ch6.adb (Append_Message): Build the location string from
	scratch and not rely on the one produced while splitting the
	aspect into pragmas.
	* exp_prag.adb (Expand_Pragma_Check): Split pre/post checks in
	expansion.
	* sem_ch13.adb (Analyze_Aspect_Specification): Don't split
	pre/post expressions into conjuncts; don't add message with
	location to the corresponding pragma.
	* sem_prag.adb (Build_Pragma_Check_Equivalent): Inherited
	pragmas no longer have messages that would need to be updated.
	* sinput.adb (Build_Location_String): Adjust to keep previous
	messages while using with inherited pragmas.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/exp_ch6.adb  |  45 +++----
 gcc/ada/exp_prag.adb | 279 +++++++++++++++++++++++++++++--------------
 gcc/ada/sem_ch13.adb |  52 --------
 gcc/ada/sem_prag.adb |  18 ---
 gcc/ada/sinput.adb   |  21 +++-
 5 files changed, 224 insertions(+), 191 deletions(-)
diff mbox series

Patch

diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 1ed83255a6d..97be99d6661 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -78,7 +78,6 @@  with Sinfo.Utils;    use Sinfo.Utils;
 with Sinput;         use Sinput;
 with Snames;         use Snames;
 with Stand;          use Stand;
-with Stringt;        use Stringt;
 with Tbuild;         use Tbuild;
 with Uintp;          use Uintp;
 with Validsw;        use Validsw;
@@ -7677,47 +7676,37 @@  package body Exp_Ch6 is
            (Id       : Entity_Id;
             Is_First : in out Boolean)
          is
-            Prag   : constant Node_Id := Get_Class_Wide_Pragma (Id,
-                                         Pragma_Precondition);
-            Msg    : Node_Id;
-            Str_Id : String_Id;
+            Prag : constant Node_Id :=
+              Get_Class_Wide_Pragma (Id, Pragma_Precondition);
 
          begin
             if No (Prag) or else Is_Ignored (Prag) then
                return;
             end if;
 
-            Msg    := Expression (Last (Pragma_Argument_Associations (Prag)));
-            Str_Id := Strval (Msg);
-
             if Is_First then
                Is_First := False;
 
-               Append (Global_Name_Buffer, Strval (Msg));
-
-               if Id /= Subp_Id
-                 and then Name_Buffer (1 .. 19) = "failed precondition"
-               then
-                  Insert_Str_In_Name_Buffer ("inherited ", 8);
+               if Id /= Subp_Id then
+                  Append
+                    (Global_Name_Buffer, "failed inherited precondition ");
+               else
+                  Append (Global_Name_Buffer, "failed precondition ");
                end if;
 
             else
-               declare
-                  Str      : constant String := To_String (Str_Id);
-                  From_Idx : Integer;
+               Append (Global_Name_Buffer, ASCII.LF);
+               Append (Global_Name_Buffer, "  or ");
 
-               begin
-                  Append (Global_Name_Buffer, ASCII.LF);
-                  Append (Global_Name_Buffer, "  or ");
-
-                  From_Idx := Name_Len;
-                  Append (Global_Name_Buffer, Str_Id);
-
-                  if Str (1 .. 19) = "failed precondition" then
-                     Insert_Str_In_Name_Buffer ("inherited ", From_Idx + 8);
-                  end if;
-               end;
+               Append (Global_Name_Buffer, "failed inherited precondition ");
             end if;
+
+            Append (Global_Name_Buffer, "from " &
+              Build_Location_String
+                (Sloc
+                  (First_Node
+                     (Expression
+                        (First (Pragma_Argument_Associations (Prag)))))));
          end Append_Message;
 
          --  Local variables
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index 78490dcbf45..a9379025a6b 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -284,24 +284,6 @@  package body Exp_Prag is
    --------------------------
 
    procedure Expand_Pragma_Check (N : Node_Id) is
-      Cond : constant Node_Id := Arg_N (N, 2);
-      Nam  : constant Name_Id := Chars (Arg_N (N, 1));
-      Msg  : Node_Id;
-
-      Loc : constant Source_Ptr := Sloc (First_Node (Cond));
-      --  Source location used in the case of a failed assertion: point to the
-      --  failing condition, not Loc. Note that the source location of the
-      --  expression is not usually the best choice here, because it points to
-      --  the location of the topmost tree node, which may be an operator in
-      --  the middle of the source text of the expression. For example, it gets
-      --  located on the last AND keyword in a chain of boolean expressions
-      --  AND'ed together. It is best to put the message on the first character
-      --  of the condition, which is the effect of the First_Node call here.
-      --  This source location is used to build the default exception message,
-      --  and also as the sloc of the call to the runtime subprogram raising
-      --  Assert_Failure, so that coverage analysis tools can relate the
-      --  call to the failed check.
-
       procedure Replace_Discriminals_Of_Protected_Op (Expr : Node_Id);
       --  Discriminants of the enclosing protected object may be referenced
       --  in the expression of a precondition of a protected operation.
@@ -315,6 +297,94 @@  package body Exp_Prag is
       --  analyzed earlier, before the creation of the discriminal renaming
       --  declarations that are added to the subprogram body.
 
+      function Make_Failure_Message
+        (Nam  : Name_Id;
+         Cond : Node_Id)
+         return Node_Id;
+      --  Build node with a string literal of a message for check Nam with
+      --  condition Cond failing at runtime.
+
+      --------------------------
+      -- Make_Failure_Message --
+      --------------------------
+
+      function Make_Failure_Message
+        (Nam  : Name_Id;
+         Cond : Node_Id)
+         return Node_Id
+      is
+         Loc     : constant Source_Ptr := Sloc (First_Node (Cond));
+         Loc_Str : constant String := Build_Location_String (Loc);
+
+      begin
+         Name_Len := 0;
+
+         --  For Assert, we just use the location
+
+         if Nam = Name_Assert then
+            null;
+
+         --  For predicate, we generate the string "predicate failed at yyy".
+         --  We prefer all lower case for predicate.
+
+         elsif Nam = Name_Predicate then
+            Add_Str_To_Name_Buffer ("predicate failed at ");
+
+         --  For special case of Precondition/Postcondition the string is
+         --  "failed xx from yy" where xx is precondition/postcondition in all
+         --  lower case. The reason for this different wording is that the
+         --  failure is not at the point of occurrence of the pragma, unlike
+         --  the other Check cases.
+
+         elsif Nam in Name_Pre
+                    | Name_Precondition
+                    | Name_Post
+                    | Name_Postcondition
+         then
+            Add_Str_To_Name_Buffer ("failed ");
+
+            --  Enhance information for inherited pragmas
+
+            if Comes_From_Inherited_Pragma (Loc) then
+               Add_Str_To_Name_Buffer ("inherited ");
+            end if;
+
+            if Nam = Name_Pre then
+               Get_Name_String_And_Append (Name_Precondition);
+            elsif Nam = Name_Post then
+               Get_Name_String_And_Append (Name_Postcondition);
+            else
+               Get_Name_String_And_Append (Nam);
+            end if;
+
+            Add_Str_To_Name_Buffer (" from ");
+
+         --  For special case of Invariant, the string is "failed invariant
+         --  from yy", to be consistent with the string that is generated for
+         --  the aspect case (the code later on checks for this specific string
+         --  to modify it in some cases, so this is functionally important).
+
+         elsif Nam = Name_Invariant then
+            Add_Str_To_Name_Buffer ("failed invariant from ");
+
+         --  For all other checks, the string is "xxx failed at yyy"
+         --  where xxx is the check name with appropriate casing.
+
+         else
+            Get_Name_String (Nam);
+            Set_Casing (Identifier_Casing (Source_Index (Current_Sem_Unit)));
+            Add_Str_To_Name_Buffer (" failed at ");
+         end if;
+
+         --  In all cases, add location string
+
+         Add_Str_To_Name_Buffer (Loc_Str);
+
+         --  Build the message
+
+         return Make_String_Literal (Loc, Name_Buffer (1 .. Name_Len));
+      end Make_Failure_Message;
+
       ------------------------------------------
       -- Replace_Discriminals_Of_Protected_Op --
       ------------------------------------------
@@ -383,6 +453,26 @@  package body Exp_Prag is
          Replace_Discriminant_References (Expr);
       end Replace_Discriminals_Of_Protected_Op;
 
+      --  Local variables
+
+      Cond : constant Node_Id := Arg_N (N, 2);
+      Nam  : constant Name_Id := Chars (Arg_N (N, 1));
+      Msg  : Node_Id;
+
+      Loc : constant Source_Ptr := Sloc (First_Node (Cond));
+      --  Source location used in the case of a failed assertion: point to the
+      --  failing condition, not Loc. Note that the source location of the
+      --  expression is not usually the best choice here, because it points to
+      --  the location of the topmost tree node, which may be an operator in
+      --  the middle of the source text of the expression. For example, it gets
+      --  located on the last AND keyword in a chain of boolean expressions
+      --  AND'ed together. It is best to put the message on the first character
+      --  of the condition, which is the effect of the First_Node call here.
+      --  This source location is used to build the default exception message,
+      --  and also as the sloc of the call to the runtime subprogram raising
+      --  Assert_Failure, so that coverage analysis tools can relate the
+      --  call to the failed check.
+
    --  Start of processing for Expand_Pragma_Check
 
    begin
@@ -469,71 +559,6 @@  package body Exp_Prag is
       --  Case where we call the procedure
 
       else
-         --  If we have a message given, use it
-
-         if Present (Arg_N (N, 3)) then
-            Msg := Get_Pragma_Arg (Arg_N (N, 3));
-
-         --  Here we have no string, so prepare one
-
-         else
-            declare
-               Loc_Str : constant String := Build_Location_String (Loc);
-
-            begin
-               Name_Len := 0;
-
-               --  For Assert, we just use the location
-
-               if Nam = Name_Assert then
-                  null;
-
-               --  For predicate, we generate the string "predicate failed at
-               --  yyy". We prefer all lower case for predicate.
-
-               elsif Nam = Name_Predicate then
-                  Add_Str_To_Name_Buffer ("predicate failed at ");
-
-               --  For special case of Precondition/Postcondition the string is
-               --  "failed xx from yy" where xx is precondition/postcondition
-               --  in all lower case. The reason for this different wording is
-               --  that the failure is not at the point of occurrence of the
-               --  pragma, unlike the other Check cases.
-
-               elsif Nam in Name_Precondition | Name_Postcondition then
-                  Get_Name_String (Nam);
-                  Insert_Str_In_Name_Buffer ("failed ", 1);
-                  Add_Str_To_Name_Buffer (" from ");
-
-               --  For special case of Invariant, the string is "failed
-               --  invariant from yy", to be consistent with the string that is
-               --  generated for the aspect case (the code later on checks for
-               --  this specific string to modify it in some cases, so this is
-               --  functionally important).
-
-               elsif Nam = Name_Invariant then
-                  Add_Str_To_Name_Buffer ("failed invariant from ");
-
-               --  For all other checks, the string is "xxx failed at yyy"
-               --  where xxx is the check name with appropriate casing.
-
-               else
-                  Get_Name_String (Nam);
-                  Set_Casing
-                    (Identifier_Casing (Source_Index (Current_Sem_Unit)));
-                  Add_Str_To_Name_Buffer (" failed at ");
-               end if;
-
-               --  In all cases, add location string
-
-               Add_Str_To_Name_Buffer (Loc_Str);
-
-               --  Build the message
-
-               Msg := Make_String_Literal (Loc, Name_Buffer (1 .. Name_Len));
-            end;
-         end if;
-
          --  For a precondition, replace references to discriminants of a
          --  protected type with the local discriminals.
 
@@ -546,16 +571,86 @@  package body Exp_Prag is
 
          --  Now rewrite as an if statement
 
-         Rewrite (N,
-           Make_If_Statement (Loc,
-             Condition       => Make_Op_Not (Loc, Right_Opnd => Cond),
-             Then_Statements => New_List (
-               Make_Procedure_Call_Statement (Loc,
-                 Name                   =>
-                   New_Occurrence_Of (RTE (RE_Raise_Assert_Failure), Loc),
-                 Parameter_Associations => New_List (Relocate_Node (Msg))))));
+         declare
+            function Make_Elsif_Check (Conj : Node_Id) return Node_Id;
+            --  Create an elsif part that checks a conjunct expression Conj and
+            --  emits a message with the exact location when the check fails.
 
-         Set_Comes_From_Check_Or_Contract (N);
+            ----------------------
+            -- Make_Elsif_Check --
+            ----------------------
+
+            function Make_Elsif_Check (Conj : Node_Id) return Node_Id is
+            begin
+               return
+                 Make_Elsif_Part (Loc,
+                   Condition       =>
+                     Make_Op_Not (Loc,
+                       Relocate_Node (Conj)),
+                   Then_Statements =>
+                     New_List (
+                       Make_Procedure_Call_Statement (Loc,
+                         Name                   =>
+                           New_Occurrence_Of
+                             (RTE (RE_Raise_Assert_Failure), Loc),
+                       Parameter_Associations =>
+                         New_List (
+                           Make_Failure_Message (Nam, Conj)))));
+            end Make_Elsif_Check;
+
+            Conjunct : Node_Id := Cond;
+            Elsifs   : List_Id := No_List;
+
+         begin
+            --  If we have a message given, use it
+
+            if Present (Arg_N (N, 3)) then
+               Msg := Get_Pragma_Arg (Arg_N (N, 3));
+
+            --  If check is for a Pre/Post expression of the form "A and then
+            --  B", then we split condition into separate conjuncts with
+            --  messages pointing to their exact locations, i.e.:
+            --
+            --    if not A then
+            --       Raise_Assert_Failure ("failed pre/post from [sloc of A]");
+            --    elsif not B then then
+            --       Raise_Assert_Failure ("failed pre/post from [sloc of B]");
+            --    end if;
+            --
+            --  This makes it easier to debug a failed complex contract.
+
+            else
+               if Nam in Name_Pre
+                       | Name_Precondition
+                       | Name_Post
+                       | Name_Postcondition
+               then
+                  while Nkind (Conjunct) = N_And_Then loop
+                     Prepend_New_To (Elsifs,
+                       Make_Elsif_Check (Right_Opnd (Conjunct)));
+                     Conjunct := Left_Opnd (Conjunct);
+                  end loop;
+               end if;
+
+               Msg := Make_Failure_Message (Nam, Conjunct);
+            end if;
+
+            Rewrite (N,
+              Make_If_Statement (Loc,
+                Condition       =>
+                  Make_Op_Not (Loc, Relocate_Node (Conjunct)),
+                Then_Statements =>
+                  New_List (
+                    Make_Procedure_Call_Statement (Loc,
+                      Name                   =>
+                        New_Occurrence_Of
+                          (RTE (RE_Raise_Assert_Failure), Loc),
+                    Parameter_Associations =>
+                      New_List (Msg))),
+                Elsif_Parts     => Elsifs));
+
+            Set_Comes_From_Check_Or_Contract (N);
+         end;
       end if;
 
       Analyze (N);
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index f3212f25dcc..efbc67f3c5d 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -4436,44 +4436,6 @@  package body Sem_Ch13 is
                      end if;
                   end if;
 
-                  --  If the expressions is of the form A and then B, then
-                  --  we generate separate Pre/Post aspects for the separate
-                  --  clauses. Since we allow multiple pragmas, there is no
-                  --  problem in allowing multiple Pre/Post aspects internally.
-                  --  These should be treated in reverse order (B first and
-                  --  A second) since they are later inserted just after N in
-                  --  the order they are treated. This way, the pragma for A
-                  --  ends up preceding the pragma for B, which may have an
-                  --  importance for the error raised (either constraint error
-                  --  or precondition error).
-
-                  --  We do not do this for Pre'Class, since we have to put
-                  --  these conditions together in a complex OR expression.
-
-                  --  We don't do this in GNATprove mode, because it brings no
-                  --  benefit for proof and causes annoyance for flow analysis,
-                  --  which prefers to be as close to the original source code
-                  --  as possible. Also we don't do this when analyzing generic
-                  --  units since it causes spurious visibility errors in the
-                  --  preanalysis of instantiations.
-
-                  if not GNATprove_Mode
-                    and then (Pname = Name_Postcondition
-                               or else not Class_Present (Aspect))
-                    and then not Inside_A_Generic
-                  then
-                     while Nkind (Expr) = N_And_Then loop
-                        Insert_After (Aspect,
-                          Make_Aspect_Specification (Sloc (Left_Opnd (Expr)),
-                            Identifier    => Identifier (Aspect),
-                            Expression    => Relocate_Node (Left_Opnd (Expr)),
-                            Class_Present => Class_Present (Aspect),
-                            Split_PPC     => True));
-                        Rewrite (Expr, Relocate_Node (Right_Opnd (Expr)));
-                        Eloc := Sloc (Expr);
-                     end loop;
-                  end if;
-
                   --  Build the precondition/postcondition pragma
 
                   Aitem := Make_Aitem_Pragma
@@ -4483,20 +4445,6 @@  package body Sem_Ch13 is
                          Expression => Relocate_Expression (Expr))),
                        Pragma_Name                => Pname);
 
-                  --  Add message unless exception messages are suppressed
-
-                  if not Opt.Exception_Locations_Suppressed then
-                     Append_To (Pragma_Argument_Associations (Aitem),
-                       Make_Pragma_Argument_Association (Eloc,
-                         Chars      => Name_Message,
-                         Expression =>
-                           Make_String_Literal (Eloc,
-                             Strval => "failed "
-                                       & Get_Name_String (Pname)
-                                       & " from "
-                                       & Build_Location_String (Eloc))));
-                  end if;
-
                   Set_Is_Delayed_Aspect (Aspect);
 
                   --  For Pre/Post cases, insert immediately after the entity
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 9e0e41c3dad..b26054e336b 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -30845,7 +30845,6 @@  package body Sem_Prag is
       Loc        : constant Source_Ptr := Sloc (Prag);
       Prag_Nam   : constant Name_Id    := Pragma_Name (Prag);
       Check_Prag : Node_Id;
-      Msg_Arg    : Node_Id;
       Nam        : Name_Id;
 
    --  Start of processing for Build_Pragma_Check_Equivalent
@@ -30930,23 +30929,6 @@  package body Sem_Prag is
              Expression => Make_Identifier (Loc, Nam)));
       end if;
 
-      --  Update the error message when the pragma is inherited
-
-      if Present (Inher_Id) then
-         Msg_Arg := Last (Pragma_Argument_Associations (Check_Prag));
-
-         if Chars (Msg_Arg) = Name_Message then
-            String_To_Name_Buffer (Strval (Expression (Msg_Arg)));
-
-            --  Insert "inherited" to improve the error message
-
-            if Name_Buffer (1 .. 8) = "failed p" then
-               Insert_Str_In_Name_Buffer ("inherited ", 8);
-               Set_Strval (Expression (Msg_Arg), String_From_Name_Buffer);
-            end if;
-         end if;
-      end if;
-
       return Check_Prag;
    end Build_Pragma_Check_Equivalent;
 
diff --git a/gcc/ada/sinput.adb b/gcc/ada/sinput.adb
index ae86f1f5bd9..8538a06654e 100644
--- a/gcc/ada/sinput.adb
+++ b/gcc/ada/sinput.adb
@@ -244,9 +244,28 @@  package body Sinput is
          Append (Buf, ':');
          Append (Buf, Nat (Get_Logical_Line_Number (Ptr)));
 
+         --  For inherited pragmas, the location will be appended to a messsage
+         --  that already says "inherited"; also, we are not interested where
+         --  the pragma has been inherited. Progress directly to instantiation
+         --  locations.
+
+         if Comes_From_Inherited_Pragma (Ptr) then
+            Ptr := Instantiation_Location (Ptr);
+         end if;
+
          Ptr := Instantiation_Location (Ptr);
          exit when Ptr = No_Location;
-         Append (Buf, " instantiated at ");
+
+         --  Make sure that we don't mention "instantiated" when in fact the
+         --  location comes from other mechanisms.
+
+         pragma Assert (not Comes_From_Inherited_Pragma (Ptr));
+
+         if Comes_From_Inlined_Body (Ptr) then
+            Append (Buf, " inlined at ");
+         else
+            Append (Buf, " instantiated at ");
+         end if;
       end loop;
    end Build_Location_String;