[gcc r13-195] [Ada] Prevent inlining-for-proof for calls inside ELSIF condition

[gcc r13-195] [Ada] Prevent inlining-for-proof for calls inside ELSIF condition

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:785b1b5d43be6bbbf38d8c8dc40d6d0c991cf99b

commit r13-195-g785b1b5d43be6bbbf38d8c8dc40d6d0c991cf99b
Author: Piotr Trojanek <trojanek@adacore.com>
Date:   Fri Jan 14 18:43:53 2022 +0100

    [Ada] Prevent inlining-for-proof for calls inside ELSIF condition
    
    In GNATprove we don't want inlining-for-proof to expand subprogram
    bodies into actions attached to nodes. These actions are attached either
    to expressions or to statements.
    
    For expressions, we prevented inlining by Is_Potentially_Unevaluated.
    For statements, we prevented inlining by In_While_Loop_Condition, but
    forgot about actions attached to ELSIF condition.
    
    There are no other expression or statements nodes where actions could be
    attached, so this fix is exhaustive.
    
    gcc/ada/
    
            * sem_util.ads (In_Statement_Condition_With_Actions): Renamed
            from In_While_Loop_Condition; move to fit the alphabetic order.
            * sem_util.adb (In_Statement_Condition_With_Actions): Detect
            Elsif condition; stop search on other statements; prevent search
            from going too far; move to fit the alphabetic order.
            * sem_res.adb (Resolve_Call): Adapt caller.

Diff:
---
 gcc/ada/sem_res.adb  |  2 +-
 gcc/ada/sem_util.adb | 65 +++++++++++++++++++++++++++++++++-------------------
 gcc/ada/sem_util.ads | 10 +++++---
 3 files changed, 49 insertions(+), 28 deletions(-)

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index f5c8b10456e..1c686cd3e06 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7346,7 +7346,7 @@ package body Sem_Res is
                --  loops, as this would create complex actions inside
                --  the condition, that are not handled by GNATprove.
 
-               elsif In_While_Loop_Condition (N) then
+               elsif In_Statement_Condition_With_Actions (N) then
                   Cannot_Inline
                     ("cannot inline & (in while loop condition)?", N, Nam_UA);
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 86bd296faa5..1fc2c617afa 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -14986,41 +14986,58 @@ package body Sem_Util is
       return False;
    end In_Return_Value;
 
-   ---------------------
-   -- In_Visible_Part --
-   ---------------------
-
-   function In_Visible_Part (Scope_Id : Entity_Id) return Boolean is
-   begin
-      return Is_Package_Or_Generic_Package (Scope_Id)
-        and then In_Open_Scopes (Scope_Id)
-        and then not In_Package_Body (Scope_Id)
-        and then not In_Private_Part (Scope_Id);
-   end In_Visible_Part;
-
-   -----------------------------
-   -- In_While_Loop_Condition --
-   -----------------------------
+   -----------------------------------------
+   -- In_Statement_Condition_With_Actions --
+   -----------------------------------------
 
-   function In_While_Loop_Condition (N : Node_Id) return Boolean is
+   function In_Statement_Condition_With_Actions (N : Node_Id) return Boolean is
       Prev : Node_Id := N;
       P    : Node_Id := Parent (N);
       --  P and Prev will be used for traversing the AST, while maintaining an
       --  invariant that P = Parent (Prev).
    begin
-      loop
-         if No (P) then
-            return False;
-         elsif Nkind (P) = N_Iteration_Scheme
+      while Present (P) loop
+         if Nkind (P) = N_Iteration_Scheme
            and then Prev = Condition (P)
          then
             return True;
-         else
-            Prev := P;
-            P := Parent (P);
+
+         elsif Nkind (P) = N_Elsif_Part
+           and then Prev = Condition (P)
+         then
+            return True;
+
+         --  No point in going beyond statements
+
+         elsif Nkind (N) in N_Statement_Other_Than_Procedure_Call
+                          | N_Procedure_Call_Statement
+         then
+            exit;
+
+         --  Prevent the search from going too far
+
+         elsif Is_Body_Or_Package_Declaration (P) then
+            exit;
          end if;
+
+         Prev := P;
+         P := Parent (P);
       end loop;
-   end In_While_Loop_Condition;
+
+      return False;
+   end In_Statement_Condition_With_Actions;
+
+   ---------------------
+   -- In_Visible_Part --
+   ---------------------
+
+   function In_Visible_Part (Scope_Id : Entity_Id) return Boolean is
+   begin
+      return Is_Package_Or_Generic_Package (Scope_Id)
+        and then In_Open_Scopes (Scope_Id)
+        and then not In_Package_Body (Scope_Id)
+        and then not In_Private_Part (Scope_Id);
+   end In_Visible_Part;
 
    --------------------------------
    -- Incomplete_Or_Partial_View --
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index e5dee96b7f4..78fc347464e 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1723,14 +1723,18 @@ package Sem_Util is
    --  This version is more efficient than calling the single root version of
    --  Is_Subtree twice.
 
+   function In_Statement_Condition_With_Actions (N : Node_Id) return Boolean;
+   --  Returns true if the expression N occurs within the condition of a
+   --  statement node with actions. Subsidiary to inlining for GNATprove, where
+   --  inlining of function calls in such expressions would expand the called
+   --  body into actions list of the condition node. GNATprove cannot yet cope
+   --  with such a complex AST.
+
    function In_Visible_Part (Scope_Id : Entity_Id) return Boolean;
    --  Determine whether a declaration occurs within the visible part of a
    --  package specification. The package must be on the scope stack, and the
    --  corresponding private part must not.
 
-   function In_While_Loop_Condition (N : Node_Id) return Boolean;
-   --  Returns true if the expression N occurs within the condition of a while
-
    function Incomplete_Or_Partial_View (Id : Entity_Id) return Entity_Id;
    --  Given the entity of a constant or a type, retrieve the incomplete or
    --  partial view of the same entity. Note that Id may not have a partial