[Ada] Variable assignments and reads in SPARK elaboration code

This patch reimplements the treatment of variable assignments and reads within
SPARK elaboration code. The changes are as follows:

1) Diagnostics of variable assignments in elaboration code are now based on the
   rules in effect (either Ada or SPARK).

2) Variable assignments in Ada elaboration code are considered problematic
   when a variable declared at the library level of a package spec without
   pragma Elaborate_Body lacks initialization, and the elaboration code of
   the corresponding package body initializes it. The compiler continues to
   emit a warning suggesting pragma Elaborate_Body on the package spec.

3) Variable assignments in SPARK elaboration code are considered problematic
   when a variable declared at the library level of a package spec without
   pragma Elaborate_Body is initialized, and the elaboration code of the
   corresponding package body further modifies the variable. The compiler
   emits an error on the missing Elaborate_Body.

4) A read of an external variable now imposes an Elaborate requirement on the
   unit performing the read, unless the variable is initialied, or the spec of
   the external unit carries pragma Elaborate_Body.

------------
-- Source --
------------

--  c1_pack.ads

with S1_Pack; use S1_Pack;

package C1_Pack with SPARK_Mode is
   Local : constant Integer := Var;                        --  needs Elaborate

   function Reference_Var return Boolean;
end C1_Pack;

--  c1_pack.adb

package body C1_Pack with SPARK_Mode is
   function Reference_Var return Boolean is
      procedure Read (Formal : Integer) is
      begin
         null;
      end Read;

      procedure Read_Write (Formal : in out Integer) is
      begin
         Formal := Formal + 1;
      end Read_Write;

      procedure Write (Formal : out Integer) is
      begin
         Formal := 123;
      end Write;

      Local : Integer;

   begin
      Read (Var);                                          --  needs Elaborate
      Read_Write (Var);                                    --  needs Elaborate
      Local := Var;                                        --  needs Elaborate

      Write (Var);                                         --  OK
      Var := 234;                                          --  OK

      return True;
   end Reference_Var;

   Ref : constant Boolean := Reference_Var;
end C1_Pack;

--  c2_pack.ads

with S2_Pack; use S2_Pack;

package C2_Pack with SPARK_Mode is
   Local : constant Integer := Var;                        --  OK

   function Reference_Var return Boolean;
end C2_Pack;

--  c2_pack.adb

package body C2_Pack with SPARK_Mode is
   function Reference_Var return Boolean is
      procedure Read (Formal : Integer) is
      begin
         null;
      end Read;

      procedure Read_Write (Formal : in out Integer) is
      begin
         Formal := Formal + 1;
      end Read_Write;

      procedure Write (Formal : out Integer) is
      begin
         Formal := 123;
      end Write;

      Local : Integer;

   begin
      Read (Var);                                          --  OK
      Read_Write (Var);                                    --  OK
      Local := Var;                                        --  OK

      Write (Var);                                         --  OK
      Var := 234;                                          --  OK

      return True;
   end Reference_Var;

   Ref : constant Boolean := Reference_Var;
end C2_Pack;

--  c3_pack.ads

with S3_Pack; use S3_Pack;
pragma Elaborate (S3_Pack);

package C3_Pack with SPARK_Mode is
   Local : constant Integer := Var;                        --  OK

   function Reference_Var return Boolean;
end C3_Pack;

--  c3_pack.adb

package body C3_Pack with SPARK_Mode is
   function Reference_Var return Boolean is
      procedure Read (Formal : Integer) is
      begin
         null;
      end Read;

      procedure Read_Write (Formal : in out Integer) is
      begin
         Formal := Formal + 1;
      end Read_Write;

      procedure Write (Formal : out Integer) is
      begin
         Formal := 123;
      end Write;

      Local : Integer;

   begin
      Read (Var);                                          --  OK
      Read_Write (Var);                                    --  OK
      Local := Var;                                        --  OK

      Write (Var);                                         --  OK
      Var := 234;                                          --  OK

      return True;
   end Reference_Var;

   Ref : constant Boolean := Reference_Var;
end C3_Pack;

--  c4_pack.ads

with S4_Pack; use S4_Pack;
pragma Elaborate (S4_Pack);

package C4_Pack with SPARK_Mode is
   Local : constant Integer := Var;                        --  OK

   function Reference_Var return Boolean;
end C4_Pack;

--  c4_pack.adb

package body C4_Pack with SPARK_Mode is
   function Reference_Var return Boolean is
      procedure Read (Formal : Integer) is
      begin
         null;
      end Read;

      procedure Read_Write (Formal : in out Integer) is
      begin
         Formal := Formal + 1;
      end Read_Write;

      procedure Write (Formal : out Integer) is
      begin
         Formal := 123;
      end Write;

      Local : Integer;

   begin
      Read (Var);                                          --  OK
      Read_Write (Var);                                    --  OK
      Local := Var;                                        --  OK

      Write (Var);                                         --  OK
      Var := 234;                                          --  OK

      return True;
   end Reference_Var;

   Ref : constant Boolean := Reference_Var;
end C4_Pack;

--  s1_pack.ads

package S1_Pack with SPARK_Mode is
   Var : Integer;

   function Init_Var return Boolean;
end S1_Pack;

--  s1_pack.adb

package body S1_Pack with SPARK_Mode is
   function Init_Var return Boolean is
   begin
      Var := 1;                                            --  OK
      return True;
   end Init_Var;

   Init : constant Boolean := Init_Var;
begin
   Var := 2;                                               --  OK
end S1_Pack;

--  s2_pack.ads

package S2_Pack with SPARK_Mode is
   pragma Elaborate_Body;
   Var : Integer;

   function Init_Var return Boolean;
end S2_Pack;

--  s2_pack.adb

package body S2_Pack with SPARK_Mode is
   function Init_Var return Boolean is
   begin
      Var := 1;                                            --  OK
      return True;
   end Init_Var;

   Init : constant Boolean := Init_Var;
begin
   Var := 2;                                               --  OK
end S2_Pack;

--  s3_pack.ads

package S3_Pack with SPARK_Mode is
   Var : Integer := 0;

   function Init_Var return Boolean;
end S3_Pack;

--  s3_pack.adb

package body S3_Pack with SPARK_Mode is
   function Init_Var return Boolean is
   begin
      Var := 1;                                            --  needs Elab_Body
      return True;
   end Init_Var;

   Init : constant Boolean := Init_Var;
begin
   Var := 2;                                               --  needs Elab_Body
end S3_Pack;

--  s4_pack.ads

package S4_Pack with SPARK_Mode is
   pragma Elaborate_Body;
   Var : Integer := 0;

   function Init_Var return Boolean;
end S4_Pack;

--  s4_pack.adb

package body S4_Pack with SPARK_Mode is
   function Init_Var return Boolean is
   begin
      Var := 1;                                            --  OK
      return True;
   end Init_Var;

   Init : constant Boolean := Init_Var;
begin
   Var := 2;                                               --  OK
end S4_Pack;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c s1_pack.adb
$ gcc -c s2_pack.adb
$ gcc -c s3_pack.adb
$ gcc -c s4_pack.adb
$ gcc -c c1_pack.adb
$ gcc -c c2_pack.adb
$ gcc -c c3_pack.adb
$ gcc -c c4_pack.adb
s3_pack.adb:4:11: variable "Var" modified by elaboration code in package body
s3_pack.adb:4:11: add pragma "Elaborate_Body" to spec "S3_Pack" to ensure full
  initialization
s3_pack.adb:4:11:   body of unit "S3_Pack" elaborated
s3_pack.adb:4:11:   function "Init_Var" called at line 8
s3_pack.adb:4:11:   variable "Var" assigned at line 4
s3_pack.adb:10:08: variable "Var" modified by elaboration code in package body
s3_pack.adb:10:08: add pragma "Elaborate_Body" to spec "S3_Pack" to ensure full
  initialization
s3_pack.adb:10:08:   body of unit "S3_Pack" elaborated
s3_pack.adb:10:08:   variable "Var" assigned at line 10
c1_pack.adb:21:13: read of variable "Var" during elaboration in SPARK
c1_pack.adb:21:13: unit "C1_Pack" requires pragma "Elaborate" for "S1_Pack"
c1_pack.adb:21:13:   body of unit "C1_Pack" elaborated
c1_pack.adb:21:13:   function "Reference_Var" called at line 31
c1_pack.adb:21:13:   variable "Var" read at line 21
c1_pack.adb:22:19: read of variable "Var" during elaboration in SPARK
c1_pack.adb:22:19: unit "C1_Pack" requires pragma "Elaborate" for "S1_Pack"
c1_pack.adb:22:19:   body of unit "C1_Pack" elaborated
c1_pack.adb:22:19:   function "Reference_Var" called at line 31
c1_pack.adb:22:19:   variable "Var" read at line 22
c1_pack.adb:23:16: read of variable "Var" during elaboration in SPARK
c1_pack.adb:23:16: unit "C1_Pack" requires pragma "Elaborate" for "S1_Pack"
c1_pack.adb:23:16:   body of unit "C1_Pack" elaborated
c1_pack.adb:23:16:   function "Reference_Var" called at line 31
c1_pack.adb:23:16:   variable "Var" read at line 23
c1_pack.ads:4:32: read of variable "Var" during elaboration in SPARK
c1_pack.ads:4:32: unit "C1_Pack" requires pragma "Elaborate" for "S1_Pack"
c1_pack.ads:4:32:   spec of unit "C1_Pack" elaborated
c1_pack.ads:4:32:   variable "Var" read at line 4

Tested on x86_64-pc-linux-gnu, committed on trunk

2017-10-14  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_elab.adb (Ensure_Dynamic_Prior_Elaboration): Renamed to
	Ensure_Prior_Elaboration_Dynamic for consistency reasons.
	(Ensure_Static_Prior_Elaboration): Renamed to
	Ensure_Prior_Elaboration_Static for consistency reasons.
	(Info_Variable_Reference): Renamed to Info_Variable_Read in order to
	reflect its new purpose.
	(Is_Initialized): New routine.
	(Is_Suitable_Variable_Reference): Renamed to Is_Suitable_Variable_Read
	in order to reflect its new purpose.
	(Is_Variable_Read): New routine.
	(Output_Variable_Reference): Renamed to Output_Variable_Read in order
	to reflect its new purpose.
	(Process_Variable_Assignment): This routine now acts as a top level
	dispatcher for variable assignments.
	(Process_Variable_Assignment_Ada): New routine.
	(Process_Variable_Assignment_SPARK): New routine.
	(Process_Variable_Reference): Renamed to Process_Variable_Read in order
	to reflects its new purpose. A reference to a variable is now suitable
	for ABE processing only when it is a read. The logic in the routine now
	reflects the latest SPARK elaboration rules.

Message ID	20171014164750.GA103148@adacore.com
State	New
Headers	show Return-Path: <gcc-patches-return-464217-incoming=patchwork.ozlabs.org@gcc.gnu.org> 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=qTLOdammcn71qd4oqPAbgRr1L/KTfaR/Uxj4HL3wEJ6Lj5UQb/ 9Yt49YKbXZKOYHeMyqEwcOnlP97BzAw9w+FoxZ9kiL0kgXYE059QC/CF2YHWgUpb XXPyEbIrxaDHWnLQDe5x1+WdkO39OZqfi4PQJmitDIqIVsEnKZdTjeoJk= Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk Sender: gcc-patches-owner@gcc.gnu.org Date: Sat, 14 Oct 2017 12:47:50 -0400 From: Pierre-Marie de Rodat <derodat@adacore.com> To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev <kirtchev@adacore.com> Subject: [Ada] Variable assignments and reads in SPARK elaboration code Message-ID: <20171014164750.GA103148@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="y0ulUmNC+osPPQO6" Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12)
Series	[Ada] Variable assignments and reads in SPARK elaboration code \| expand [Ada] Variable assignments and reads in SPARK elaboration code

[Ada] Variable assignments and reads in SPARK elaboration code

Commit Message

Patch