From db6261488e4e53e4ac09ec9db50ea2e4a1859377 Mon Sep 17 00:00:00 2001 From: Ed Schonberg Date: Fri, 5 Jul 2019 07:02:03 +0000 Subject: [PATCH] [Ada] Compiler abort on a dynamic predicate used in a precondition This patch suppresses the generation of a predicate check when the expression is a formal IN parameter of a subprogram S. If the check is being applied to the actual in a call, the call is either in the body of S, or in an aspect specfication for S, e.g. a precondition, In both cases the check is redundant bevause it will be applied on any call to S. In the second case the expansion of the predicate check may lead to out-of-scope references the the formal. 2019-07-05 Ed Schonberg gcc/ada/ * checks.adb (Apply_Predicate_Check): Except within the subprogram body that defines the formal, do not apply predicate check on a formal IN parameter: such a check is redundant and its expansion can lead to out-of-scope references when it is originates in a function call in a precondition, gcc/testsuite/ * gnat.dg/predicate7.adb, gnat.dg/predicate7.ads, gnat.dg/predicate7_pkg.ads: New testcase. From-SVN: r273106 --- gcc/ada/ChangeLog | 8 ++++++++ gcc/ada/checks.adb | 35 ++++++++++++++++++++++++++++++++ gcc/testsuite/ChangeLog | 5 +++++ gcc/testsuite/gnat.dg/predicate7.adb | 6 ++++++ gcc/testsuite/gnat.dg/predicate7.ads | 13 ++++++++++++ gcc/testsuite/gnat.dg/predicate7_pkg.ads | 3 +++ 6 files changed, 70 insertions(+) create mode 100644 gcc/testsuite/gnat.dg/predicate7.adb create mode 100644 gcc/testsuite/gnat.dg/predicate7.ads create mode 100644 gcc/testsuite/gnat.dg/predicate7_pkg.ads diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6f22a1a..b1b98f2 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,11 @@ +2019-07-05 Ed Schonberg + + * checks.adb (Apply_Predicate_Check): Except within the + subprogram body that defines the formal, do not apply predicate + check on a formal IN parameter: such a check is redundant and + its expansion can lead to out-of-scope references when it is + originates in a function call in a precondition, + 2019-07-05 Yannick Moy * sem_res.adb (Resolve_Call): Cannot inline in quantified diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 33fb27e..8176f85 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -2707,6 +2707,41 @@ package body Checks is -- Here for normal case of predicate active else + -- If the expression is an IN parameter, the predicate will have + -- been applied at the point of call. An additional check would + -- be redundant, or will lead to out-of-scope references if the + -- call appears within an aspect specification for a precondition. + + -- However, if the reference is within the body of the subprogram + -- that declares the formal, the predicate can safely be applied, + -- which may be necessary for a nested call whose formal has a + -- different predicate. + + if Is_Entity_Name (N) + and then Ekind (Entity (N)) = E_In_Parameter + then + declare + In_Body : Boolean := False; + P : Node_Id := Parent (N); + + begin + while Present (P) loop + if Nkind (P) = N_Subprogram_Body + and then Corresponding_Spec (P) = Scope (Entity (N)) + then + In_Body := True; + exit; + end if; + + P := Parent (P); + end loop; + + if not In_Body then + return; + end if; + end; + end if; + -- If the type has a static predicate and the expression is known -- at compile time, see if the expression satisfies the predicate. diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index 30b2d1f..d5905f0 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,8 @@ +2019-07-05 Ed Schonberg + + * gnat.dg/predicate7.adb, gnat.dg/predicate7.ads, + gnat.dg/predicate7_pkg.ads: New testcase. + 2019-07-04 Jakub Jelinek PR middle-end/78884 diff --git a/gcc/testsuite/gnat.dg/predicate7.adb b/gcc/testsuite/gnat.dg/predicate7.adb new file mode 100644 index 0000000..119c190 --- /dev/null +++ b/gcc/testsuite/gnat.dg/predicate7.adb @@ -0,0 +1,6 @@ +-- { dg-do compile } +-- { dg-options "-gnata" } + +package body Predicate7 is + procedure Foo is null; +end; diff --git a/gcc/testsuite/gnat.dg/predicate7.ads b/gcc/testsuite/gnat.dg/predicate7.ads new file mode 100644 index 0000000..598e2b0 --- /dev/null +++ b/gcc/testsuite/gnat.dg/predicate7.ads @@ -0,0 +1,13 @@ +with Predicate7_Pkg; use Predicate7_Pkg; + +package Predicate7 is + function Always_True (I : My_Int) return Boolean; + + function Identity (I : My_Int ) return Integer with Pre => Always_True (I); + + procedure Foo; + +private + function Identity (I : My_Int ) return Integer is (I); + function Always_True (I : My_Int) return Boolean is (True); +end; diff --git a/gcc/testsuite/gnat.dg/predicate7_pkg.ads b/gcc/testsuite/gnat.dg/predicate7_pkg.ads new file mode 100644 index 0000000..b90419e --- /dev/null +++ b/gcc/testsuite/gnat.dg/predicate7_pkg.ads @@ -0,0 +1,3 @@ +package Predicate7_Pkg is + subtype My_Int is Integer with Dynamic_Predicate => My_Int /= 0; +end Predicate7_Pkg; -- 2.7.4