[Ada] Prevent inlining inside condition of while loop in GNATprove

2019-12-13  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_res.adb (Resolve_Call): Prevent inlining inside while loop
	conditions.
	* sem_util.adb, sem_util.ads (In_While_Loop_Condition): New
	query function.

From-SVN: r279347

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 209a2d452ec7e0717c5bed150655b8cfd3d141fa..b5834a9de147607184faee3aa32a394bdfa0c8c1 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+2019-12-13  Yannick Moy  <moy@adacore.com>
+
+       * sem_res.adb (Resolve_Call): Prevent inlining inside while loop
+       conditions.
+       * sem_util.adb, sem_util.ads (In_While_Loop_Condition): New
+       query function.
+
 2019-12-13  Bob Duff  <duff@adacore.com>
 
        * impunit.ads: Add Ada_202X_Unit.

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 0bdbc25ff0fd2e8d3ff64401dac09ee24df2045e..11b531610e06b60b6ca59457a0a945322d71e80d 100644 (file)
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7172,6 +7172,14 @@ package body Sem_Res is
                     ("cannot inline & (in potentially unevaluated context)?",
                      N, Nam_UA);
 
+               --  Calls cannot be inlined inside the conditions of while
+               --  loops, as this would create complex actions inside
+               --  the condition, that are not handled by GNATprove.
+
+               elsif In_While_Loop_Condition (N) then
+                  Cannot_Inline
+                    ("cannot inline & (in while loop condition)?", N, Nam_UA);
+
                --  Do not inline calls which would possibly lead to missing a
                --  type conversion check on an input parameter.
 

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index ea87a3a33520dd187edd18daa6897a01345109e7..03ce7c0327af51c94ce66df2e426d029160f0b56 100644 (file)
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -12855,6 +12855,30 @@ package body Sem_Util is
         and then not In_Private_Part (Scope_Id);
    end In_Visible_Part;
 
+   -----------------------------
+   -- In_While_Loop_Condition --
+   -----------------------------
+
+   function In_While_Loop_Condition (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
+           and then Prev = Condition (P)
+         then
+            return True;
+         else
+            Prev := P;
+            P := Parent (P);
+         end if;
+      end loop;
+   end In_While_Loop_Condition;
+
    --------------------------------
    -- Incomplete_Or_Partial_View --
    --------------------------------

diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index ace843ed34eb761ae2cff1a7873ae84ccb7f63e0..ea963deb44962f462f029f929901d38859303d06 100644 (file)
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1446,6 +1446,9 @@ package Sem_Util is
    --  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