From: Yannick Moy <moy@adacore.com>
Date: Fri, 13 Dec 2019 09:03:56 +0000 (+0000)
Subject: [Ada] Prevent inlining inside condition of while loop in GNATprove
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2e3795d016a7263c82a4f64a7204f416d12a72da;p=gcc.git

[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 209a2d452ec..b5834a9de14 100644
--- 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 0bdbc25ff0f..11b531610e0 100644
--- 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 ea87a3a3352..03ce7c0327a 100644
--- 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 ace843ed34e..ea963deb449 100644
--- 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