From patchwork Sat Oct 14 17:08:27 2017 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 825842 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (mailfrom) smtp.mailfrom=gcc.gnu.org (client-ip=209.132.180.131; helo=sourceware.org; envelope-from=gcc-patches-return-464223-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="HvT8hPZZ"; dkim-atps=neutral Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 3yDrdj6Mv0z9t2l for ; Sun, 15 Oct 2017 04:08:41 +1100 (AEDT) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=O5PaJaUwk09QSGGi5UqvthlLctEaORu1UigH2Bt0VKD7y8Tc64 uLRFbBxF6givTneLe4o6TyBfrENOvLYytGXt8qpRQn0M36NvjsrZ4Uan9oWvJIIP m08oIFLwFWlyUY0ZN1P2QYdxONfD0IFSHIh7DZ6cNqj9YD/fc4En8Yqu0= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=CaLEes28CoDQhya35lqaRWyc6t0=; b=HvT8hPZZJZ+G2CVWcEkl H2LLw80MO0yxUcaJeQqhKDyiEJcvjMaBgzyMy6e2CSQ3AriReaUeypamV57/sUBU VoO7m4wB5Z+fvYN5Vgt2sple+VDFtUX8s+c6+QQzfqW0diggeHCX/I1qmHi0QBqn wAvB4X/iMGeP/RX49KDf2O8= Received: (qmail 72580 invoked by alias); 14 Oct 2017 17:08:31 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org Received: (qmail 72562 invoked by uid 89); 14 Oct 2017 17:08:31 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-15.7 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_1, GIT_PATCH_2, GIT_PATCH_3, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy=dw, ds, factors, fulfilled X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Sat, 14 Oct 2017 17:08:28 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 6648756121; Sat, 14 Oct 2017 13:08:27 -0400 (EDT) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id oV+tAuxW5ANz; Sat, 14 Oct 2017 13:08:27 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 53EFB56079; Sat, 14 Oct 2017 13:08:27 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 52DFC319; Sat, 14 Oct 2017 13:08:27 -0400 (EDT) Date: Sat, 14 Oct 2017 13:08:27 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Activation/suppression of SPARK elaboration rules Message-ID: <20171014170827.GA123125@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes This patch utilizes compilation switch -gnatd.v to enforce the SPARK rules for elaboration in SPARK code. The affected scenarios are calls and instantiations. If the switch is active, the ABE mechanism will verify that the scenarios have fulfilled their Elaborate[_All] requirements. Otherwise the static model of the ABE mechanism will install implicit Elaborate[_All] pragmas to meet these requirements. ------------ -- Source -- ------------ -- server.ads package Server with SPARK_Mode is generic procedure Gen_Proc; generic package Gen_Pack is procedure Proc; end Gen_Pack; function Func return Boolean; end Server; -- server.adb with Ada.Text_IO; use Ada.Text_IO; package body Server with SPARK_Mode is procedure Gen_Proc is begin Put_Line ("Gen_Proc"); end Gen_Proc; package body Gen_Pack is procedure Proc is begin Put_Line ("Proc"); end Proc; end Gen_Pack; function Func return Boolean is begin Put_Line ("Func"); return True; end Func; end Server; -- client.ads with Server; package Client with SPARK_Mode is procedure Inst_Proc is new Server.Gen_Proc; package Inst_Pack is new Server.Gen_Pack; Val : constant Boolean := Server.Func; end Client; ---------------------------- -- Compilation and output -- ---------------------------- $ echo "Ignore SPARK rules" $ gcc -c client.ads $ echo "Apply SPARK rules" $ gcc -c client.ads -gnatd.v Ignore SPARK rules Apply SPARK rules client.ads:4:04: instantiation of "Gen_Proc" during elaboration in SPARK client.ads:4:04: unit "Client" requires pragma "Elaborate_All" for "Server" client.ads:4:04: spec of unit "Client" elaborated client.ads:4:04: procedure "Gen_Proc" instantiated as "Inst_Proc" at line 4 client.ads:5:04: instantiation of "Gen_Pack" during elaboration in SPARK client.ads:5:04: unit "Client" requires pragma "Elaborate" for "Server" client.ads:5:04: spec of unit "Client" elaborated client.ads:5:04: package "Gen_Pack" instantiated as "Inst_Pack" at line 5 client.ads:7:36: call to "Func" during elaboration in SPARK client.ads:7:36: unit "Client" requires pragma "Elaborate_All" for "Server" client.ads:7:36: spec of unit "Client" elaborated client.ads:7:36: function "Func" called at line 7 Tested on x86_64-pc-linux-gnu, committed on trunk 2017-10-14 Hristian Kirtchev * debug.adb: Switch -gnatd.v and associated flag are now used to enforce the SPARK rules for elaboration in SPARK code. * sem_elab.adb: Describe switch -gnatd.v. (Process_Call): Verify the SPARK rules only when -gnatd.v is in effect. (Process_Instantiation): Verify the SPARK rules only when -gnatd.v is in effect. (Process_Variable_Assignment): Clarify why variable assignments are processed reglardless of whether -gnatd.v is in effect. * doc/gnat_ugn/elaboration_order_handling_in_gnat.rst: Update the sections on elaboration code and compilation switches. * gnat_ugn.texi: Regenerate. Index: doc/gnat_ugn/elaboration_order_handling_in_gnat.rst =================================================================== --- doc/gnat_ugn/elaboration_order_handling_in_gnat.rst (revision 253753) +++ doc/gnat_ugn/elaboration_order_handling_in_gnat.rst (working copy) @@ -133,9 +133,44 @@ ================= The sequence by which the elaboration code of all units within a partition is -executed is referred to as **elaboration order**. The elaboration order depends -on the following factors: +executed is referred to as **elaboration order**. +Within a single unit, elaboration code is executed in sequential order. + +:: + + package body Client is + Result : ... := Server.Func; + + procedure Proc is + package Inst is new Server.Gen; + begin + Inst.Eval (Result); + end Proc; + begin + Proc; + end Client; + +In the example above, the elaboration order within package body ``Client`` is +as follows: + +1. The object declaration of ``Result`` is elaborated. + + * Function ``Server.Func`` is invoked. + +2. The subprogram body of ``Proc`` is elaborated. + +3. Procedure ``Proc`` is invoked. + + * Generic unit ``Server.Gen`` is instantiated as ``Inst``. + + * Instance ``Inst`` is elaborated. + + * Procedure ``Inst.Eval`` is invoked. + +The elaboration order of all units within a partition depends on the following +factors: + * |withed| units * purity of units @@ -571,7 +606,7 @@ a partition is elaboration code. GNAT performs very few diagnostics and generates run-time checks to verify the elaboration order of a program. This behavior is identical to that specified by the Ada Reference Manual. The - dynamic model is enabled with compilation switch :switch:`-gnatE`. + dynamic model is enabled with compiler switch :switch:`-gnatE`. .. index:: Static elaboration model @@ -860,7 +895,7 @@ The SPARK model is identical to the static model in its handling of internal targets. The SPARK model, however, requires explicit ``Elaborate`` or ``Elaborate_All`` pragmas to be present in the program when a target is -external, and emits hard errors instead of warnings: +external, and compiler switch :switch:`-gnatd.v` is in effect. :: @@ -987,7 +1022,7 @@ * *Switch to more permissive elaboration model* If the compilation was performed using the static model, enable the dynamic - model with compilation switch :switch:`-gnatE`. GNAT will no longer generate + model with compiler switch :switch:`-gnatE`. GNAT will no longer generate implicit ``Elaborate`` and ``Elaborate_All`` pragmas, resulting in a behavior identical to that specified by the Ada Reference Manual. The binder will generate an executable program that may or may not raise ``Program_Error``, @@ -1504,6 +1539,17 @@ When this switch is in effect, GNAT will ignore ``'Access`` of an entry, operator, or subprogram when the static model is in effect. +.. index:: -gnatd.v (gnat) + +:switch:`-gnatd.v` + Enforce SPARK elaboration rules in SPARK code + + When this switch is in effect, GNAT will enforce the SPARK rules of + elaboration as defined in the SPARK Reference Manual, section 7.7. As a + result, constructs which violate the SPARK elaboration rules are no longer + accepted, even if GNAT is able to statically ensure that these constructs + will not lead to ABE problems. + .. index:: -gnatd.y (gnat) :switch:`-gnatd.y` @@ -1558,7 +1604,7 @@ - *SPARK model* GNAT will indicate how an elaboration requirement is met by the context of - a unit. + a unit. This diagnostic requires compiler switch :switch:`-gnatd.v`. :: @@ -1612,8 +1658,8 @@ elaboration order, then apart from possible cases involing dispatching calls and access-to-subprogram types, the program is free of elaboration errors. If it is important for the program to be portable to compilers other than GNAT, -then the programmer should use compilation switch :switch:`-gnatel` and -consider the messages about missing or implicitly created ``Elaborate`` and +then the programmer should use compiler switch :switch:`-gnatel` and consider +the messages about missing or implicitly created ``Elaborate`` and ``Elaborate_All`` pragmas. If the binder reports an elaboration circularity, the programmer has several Index: sem_elab.adb =================================================================== --- sem_elab.adb (revision 253756) +++ sem_elab.adb (working copy) @@ -361,6 +361,13 @@ -- entries, operators, and subprograms. As a result, the scenarios -- are not recorder or processed. -- + -- -gnatd.v enforce SPARK elaboration rules in SPARK code + -- + -- The ABE mechanism applies some of the SPARK elaboration rules + -- defined in the SPARK reference manual, chapter 7.7. Note that + -- certain rules are always enforced, regardless of whether the + -- switch is active. + -- -- -gnatd.y disable implicit pragma Elaborate_All on task bodies -- -- The ABE mechanism does not generate implicit Elaborate_All when @@ -6891,16 +6898,18 @@ elsif Is_Up_Level_Target (Target_Attrs.Spec_Decl) then return; - -- The SPARK rules are in effect + -- The SPARK rules are verified only when -gnatd.v (enforce SPARK + -- elaboration rules in SPARK code) is in effect. - elsif SPARK_Rules_On then + elsif SPARK_Rules_On and Debug_Flag_Dot_V then Process_Call_SPARK (Call => Call, Call_Attrs => Call_Attrs, Target_Id => Target_Id, Target_Attrs => Target_Attrs); - -- Otherwise the Ada rules are in effect + -- Otherwise the Ada rules are in effect, or SPARK code is allowed to + -- violate the SPARK rules. else Process_Call_Ada @@ -7459,9 +7468,10 @@ elsif Is_Up_Level_Target (Gen_Attrs.Spec_Decl) then return; - -- The SPARK rules are in effect + -- The SPARK rules are verified only when -gnatd.v (enforce SPARK + -- elaboration rules in SPARK code) is in effect. - elsif SPARK_Rules_On then + elsif SPARK_Rules_On and Debug_Flag_Dot_V then Process_Instantiation_SPARK (Exp_Inst => Exp_Inst, Inst => Inst, @@ -7469,7 +7479,8 @@ Gen_Id => Gen_Id, Gen_Attrs => Gen_Attrs); - -- Otherwise the Ada rules are in effect + -- Otherwise the Ada rules are in effect, or SPARK code is allowed to + -- violate the SPARK rules. else Process_Instantiation_Ada @@ -7869,7 +7880,10 @@ In_SPARK => SPARK_Rules_On); end if; - -- The SPARK rules are in effect + -- The SPARK rules are in effect. These rules are applied regardless of + -- whether -gnatd.v (enforce SPARK elaboration rules in SPARK code) is + -- in effect because the static model cannot ensure safe assignment of + -- variables. if SPARK_Rules_On then Process_Variable_Assignment_SPARK Index: debug.adb =================================================================== --- debug.adb (revision 253753) +++ debug.adb (working copy) @@ -112,7 +112,7 @@ -- d.s Strict secondary stack management -- d.t Disable static allocation of library level dispatch tables -- d.u Enable Modify_Tree_For_C (update tree for c) - -- d.v + -- d.v Enforce SPARK elaboration rules in SPARK code -- d.w Do not check for infinite loops -- d.x No exception handlers -- d.y Disable implicit pragma Elaborate_All on task bodies @@ -600,6 +600,13 @@ -- d.u Sets Modify_Tree_For_C mode in which tree is modified to make it -- easier to generate code using a C compiler. + -- d.v This flag enforces the elaboration rules defined in the SPARK + -- Reference Manual, chapter 7.7, to all SPARK code within a unit. As + -- a result, constructs which violate the rules in chapter 7.7 are no + -- longer accepted, even if the implementation is able to statically + -- ensure that accepting these constructs does not introduce the + -- possibility of failing an elaboration check. + -- d.w This flag turns off the scanning of loops to detect possible -- infinite loops. Index: gnat_ugn.texi =================================================================== --- gnat_ugn.texi (revision 253753) +++ gnat_ugn.texi (working copy) @@ -21,7 +21,7 @@ @copying @quotation -GNAT User's Guide for Native Platforms , Oct 09, 2017 +GNAT User's Guide for Native Platforms , Oct 14, 2017 AdaCore @@ -27187,13 +27187,67 @@ The sequence by which the elaboration code of all units within a partition is -executed is referred to as @strong{elaboration order}. The elaboration order depends -on the following factors: +executed is referred to as @strong{elaboration order}. +Within a single unit, elaboration code is executed in sequential order. +@example +package body Client is + Result : ... := Server.Func; + + procedure Proc is + package Inst is new Server.Gen; + begin + Inst.Eval (Result); + end Proc; +begin + Proc; +end Client; +@end example + +In the example above, the elaboration order within package body @code{Client} is +as follows: + + +@enumerate + +@item +The object declaration of @code{Result} is elaborated. + + @itemize * @item +Function @code{Server.Func} is invoked. +@end itemize + +@item +The subprogram body of @code{Proc} is elaborated. + +@item +Procedure @code{Proc} is invoked. + + +@itemize * + +@item +Generic unit @code{Server.Gen} is instantiated as @code{Inst}. + +@item +Instance @code{Inst} is elaborated. + +@item +Procedure @code{Inst.Eval} is invoked. +@end itemize +@end enumerate + +The elaboration order of all units within a partition depends on the following +factors: + + +@itemize * + +@item @emph{with}ed units @item @@ -27689,7 +27743,7 @@ a partition is elaboration code. GNAT performs very few diagnostics and generates run-time checks to verify the elaboration order of a program. This behavior is identical to that specified by the Ada Reference Manual. The -dynamic model is enabled with compilation switch @code{-gnatE}. +dynamic model is enabled with compiler switch @code{-gnatE}. @end itemize @geindex Static elaboration model @@ -28001,7 +28055,7 @@ The SPARK model is identical to the static model in its handling of internal targets. The SPARK model, however, requires explicit @code{Elaborate} or @code{Elaborate_All} pragmas to be present in the program when a target is -external, and emits hard errors instead of warnings: +external, and compiler switch @code{-gnatd.v} is in effect. @example 1. with Server; @@ -28146,7 +28200,7 @@ @emph{Switch to more permissive elaboration model} If the compilation was performed using the static model, enable the dynamic -model with compilation switch @code{-gnatE}. GNAT will no longer generate +model with compiler switch @code{-gnatE}. GNAT will no longer generate implicit @code{Elaborate} and @code{Elaborate_All} pragmas, resulting in a behavior identical to that specified by the Ada Reference Manual. The binder will generate an executable program that may or may not raise @code{Program_Error}, @@ -28711,6 +28765,22 @@ operator, or subprogram when the static model is in effect. @end table +@geindex -gnatd.v (gnat) + + +@table @asis + +@item @code{-gnatd.v} + +Enforce SPARK elaboration rules in SPARK code + +When this switch is in effect, GNAT will enforce the SPARK rules of +elaboration as defined in the SPARK Reference Manual, section 7.7. As a +result, constructs which violate the SPARK elaboration rules are no longer +accepted, even if GNAT is able to statically ensure that these constructs +will not lead to ABE problems. +@end table + @geindex -gnatd.y (gnat) @@ -28785,7 +28855,7 @@ @emph{SPARK model} GNAT will indicate how an elaboration requirement is met by the context of -a unit. +a unit. This diagnostic requires compiler switch @code{-gnatd.v}. @example 1. with Server; pragma Elaborate_All (Server); @@ -28846,8 +28916,8 @@ elaboration order, then apart from possible cases involing dispatching calls and access-to-subprogram types, the program is free of elaboration errors. If it is important for the program to be portable to compilers other than GNAT, -then the programmer should use compilation switch @code{-gnatel} and -consider the messages about missing or implicitly created @code{Elaborate} and +then the programmer should use compiler switch @code{-gnatel} and consider +the messages about missing or implicitly created @code{Elaborate} and @code{Elaborate_All} pragmas. If the binder reports an elaboration circularity, the programmer has several