[Ada] Volatile functions

This patch implements SPARK volatile functions described by the following
rules:

   A type is said to be effectively volatile if it is either a volatile
   type, an array type whose Volatile_Component aspect is True, or an
   array type whose component type is effectively volatile, a protected
   type, or a descendant of Ada.Synchronous_Task_Control.Suspension_Object.
   An effectively volatile object is a volatile object or an object of an
   effectively volatile type.

   The Boolean aspect Volatile_Function may be specified as part of
   the (explicit) initial declaration of a function. A function whose
   Volatile_Function aspect is True is said to be a volatile function.
   A protected function is also defined to be a volatile function.

   A subprogram whose Volatile_Function aspect is True shall not override an
   inherited primitive operation of a tagged type whose Volatile_Function
   aspect is False.

   A global_item of a nonvolatile function shall not denote either an
   effectively volatile object or an external state abstraction.

   A nonvolatile function shall not have a formal parameter (or result) of an
   effectively volatile type.

   Contrary to the general SPARK 2014 rule that expression evaluation cannot
   have side effects, a read of an effectively volatile object with the
   properties Async_Writers or Effective_Reads set to True is considered to
   have an effect when read. To reconcile this discrepancy, a name denoting
   such an object shall only occur in a non-interfering context. A name occurs
   in a non-interfering context if it is:

      the (protected) prefix of a name denoting a protected operation; or

      the return expression of a simple_return_statement which applies to a
      volatile function; or

      the initial value expression of the extended_return_object_declaration
      of an extended_return_statement which applies to a volatile function; or

The patch also changes the implementation of aspects/pragmas Async_Readers,
Async_Writers, Effective_Reads and Effective_Writes to remove their forward
referencing capabilities and require a static Boolean expression (if any).

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

--  volatile types.ads

with Ada.Synchronous_Task_Control; use Ada.Synchronous_Task_Control;

package Volatile_Types is
   type Vol_Typ_1 is null record with Volatile;
   type Vol_Typ_1_Ptr is access all Vol_Typ_1;

   type Vol_Typ_2 is array (1 .. 5) of Vol_Typ_1;

   type Vol_Typ_3 is array (1 .. 5) of Boolean with Volatile_Components;

   protected type Vol_Typ_4 is
      entry E;
      procedure P;
   end Vol_Typ_4;

   type Vol_Typ_5 is new Suspension_Object;
end Volatile_Types;

--  volatile types.adb

package body Volatile_Types is
   protected body Vol_Typ_4 is
      entry E when True is begin null; end E;
      procedure P is begin null; end P;
   end Vol_Typ_4;
end Volatile_Types;

--  lr712.ads

package LR712 is

   --  7.1.2 - The Boolean aspect Volatile_Function may be specified as part of
   --  the initial declaration of a function. Function whose Volatile_Function
   --  aspect is True is said to be a volatile function. A protected function
   --  is also defined to be a volatile function.

   function OK_1 return Boolean with Volatile_Function;              --  OK
   function OK_2 return Boolean is (True) with Volatile_Function;    --  OK
   function OK_3 return Boolean;
   pragma Volatile_Function;                                         --  OK

   function Error_1 return Boolean;
   function Error_2 return Boolean;
   function Error_3 return Boolean;
   function Error_4 return Boolean;
   function Error_4 return Boolean is (True)
     with Volatile_Function;                                         --  Error
   function Error_5 return Boolean
     with Volatile_Function => Junk;                                 --  Error
   function Error_6 return Boolean
     with Volatile_Function => "Junk";                               --  Error
   function Error_7 return Boolean;

   Obj : Integer := 1 with Volatile_Function;                        --  Error
end LR712;

--  lr712.adb

ckage body LR712 is
   function OK_1 return Boolean is begin return True; end OK_1;
   function OK_3 return Boolean is begin return True; end OK_3;

   function Error_1 return Boolean
     with Volatile_Function                                          --  Error
   is begin return True; end Error_1;
   function Error_2 return Boolean is (True) with Volatile_Function; --  Error
   function Error_3 return Boolean is separate;
   function Error_5 return Boolean is begin return True; end Error_5;
   function Error_6 return Boolean is begin return True; end Error_6;
   function Error_7 return Boolean is
      pragma Volatile_Function;                                      --  Error
   begin return True; end Error_7;
end LR712;

--  lr712-error_3.adb

separate (LR712)

function Error_3 return Boolean
  with Volatile_Function                                             --  Error
is begin return True; end Error_3;

--  lr71215.ads

package LR71215 is

   --  7.1.2(15) - A subprogram whose Volatile_Function aspect is True shall
   --  not override an inherited primitive operation of a tagged type whose
   --  Volatile_Function aspect is False.

   type Parent_Type is tagged null record;
   function Func_1 (Obj : Parent_Type) return Boolean;
   function Func_2 (Obj : Parent_Type) return Boolean
     with Volatile_Function;

   type Child_Type is new Parent_Type with null record;
   function Func_1 (Obj : Child_Type) return Boolean
     with Volatile_Function;                                         --  Error
   function Func_2 (Obj : Child_Type) return Boolean;                --  OK
end LR71215;

--  lr7138.ads

with Volatile_Types; use Volatile_Types;

package LR7138
  with SPARK_Mode,
       Abstract_State => (External_State with External)
is
   --  71.3(8) - A global_item of a nonvolatile function shall not denote
   --  either an effectively volatile object or an external state abstraction.

   Obj_1 : Vol_Typ_1 with Async_Readers;
   Obj_2 : Vol_Typ_2 with Async_Readers;
   Obj_3 : Vol_Typ_3 with Async_Readers;
   Obj_4 : Vol_Typ_4 with Async_Readers;
   Obj_5 : Vol_Typ_5 with Async_Readers;

   function OK return Boolean
     with Global =>
            (Input =>
              (External_State, Obj_1, Obj_2, Obj_3, Obj_4, Obj_5)),  --  all OK
          Volatile_Function;

   function Error return Boolean
     with Global => (Input => (External_State,                       --  Error
                               Obj_1,                                --  Error
                               Obj_2,                                --  Error
                               Obj_3,                                --  Error
                               Obj_4,                                --  Error
                               Obj_5));                              --  Error
end LR7138;

--  lr7139.ads

with Volatile_Types; use Volatile_Types;

package LR7139 with SPARK_Mode is

   --  7.1.3(9) - A nonvolatile function shall not have a formal parameter (or
   --  result) of an effectively volatile type.

   function OK_1 return Vol_Typ_1 with Volatile_Function;            --  OK
   function OK_2 return Vol_Typ_2 with Volatile_Function;            --  OK
   function OK_3 return Vol_Typ_3 with Volatile_Function;            --  OK
   function OK_4 return Vol_Typ_4 with Volatile_Function;            --  OK
   function OK_5 return Vol_Typ_5 with Volatile_Function;            --  OK
   function OK_6
     (Formal_1 : Vol_Typ_1;                                          --  OK
      Formal_2 : Vol_Typ_2;                                          --  OK
      Formal_3 : Vol_Typ_3;                                          --  OK
      Formal_4 : Vol_Typ_4;                                          --  OK
      Formal_5 : Vol_Typ_5) return Boolean                           --  OK
   with Volatile_Function;

   function Error_1 return Vol_Typ_1;                                --  Error
   function Error_2 return Vol_Typ_2;                                --  Error
   function Error_3 return Vol_Typ_3;                                --  Error
   function Error_4 return Vol_Typ_4;                                --  Error
   function Error_5 return Vol_Typ_5;                                --  Error
   function Error_6
     (Formal_1 : Vol_Typ_1;                                          --  Error
      Formal_2 : Vol_Typ_2;                                          --  Error
      Formal_3 : Vol_Typ_3;                                          --  Error
      Formal_4 : Vol_Typ_4;                                          --  Error
      Formal_5 : Vol_Typ_5) return Boolean;                          --  Error
end LR7139;

--  lr71312.ads

package LR71312 with SPARK_Mode is

   --  7.1.3(12) - Contrary to the general SPARK 2014 rule that expression
   --  evaluation cannot have side effects, a read of an effectively volatile
   --  object with the properties Async_Writers or Effective_Reads set to True
   --  is considered to have an effect when read. To reconcile this discrepancy
   --  a name denoting such an object shall only occur in a non-interfering
   --  context. A name occurs in a non-interfering context if it is:

   --    the (protected) prefix of a name denoting a protected operation

   --    the return expression of a simple_return_statement which applies to a
   --    volatile function

   --    the initial value expression of the extended_return_object_declaration
   --    of an extended_return_statement which applies to a volatile function

   function OK_1 return Integer with Volatile_Function;
   function OK_2 return Integer with Volatile_Function;
   procedure OK_3;

   function Error_1 return Integer;
   function Error_2 return Integer;
   procedure Error_3;
end LR71312;

--  lr71312.adb

with Volatile_Types; use Volatile_Types;

package body LR71312 with SPARK_Mode is
   Obj_1 : Integer with Async_Writers, Volatile;
   Obj_2 : Vol_Typ_4;

   function OK_1 return Integer is
   begin
      return Obj_1;                                                  --  OK
   end OK_1;

   function OK_2 return Integer is
   begin
      return Result : Integer := Obj_1;                              --  OK
   end OK_2;

   procedure OK_3 is
   begin
      Obj_2.E;                                                       --  OK
      Obj_2.P;                                                       --  OK
   end OK_3;

   function Error_1 return Integer is
   begin
      return Obj_1;                                                  --  Error
   end Error_1;

   function Error_2 return Integer is
   begin
      return Result : Integer := Obj_1;                              --  Error
   end Error_2;

   procedure Error_3 is
   begin
      if Obj_2 in Vol_Typ_4 then                                     --  Error
         null;
      end if;
   end Error_3;
end LR71312;

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

$ gcc -c lr712.adb
$ gcc -c lr71215.ads
$ gcc -c lr7138.ads
$ gcc -c lr7139.ads
$ gcc -c lr71312.adb
lr712.adb:6:11: aspect specification must appear in subprogram declaration
lr712.adb:8:51: aspect specification must appear in subprogram declaration
lr712.adb:13:07: incorrect placement of pragma "VOLATILE_FUNCTION"
lr712.ads:18:11: aspect specification must appear in subprogram declaration
lr712.ads:20:32: "Junk" is undefined
lr712.ads:22:32: expected type "Standard.Boolean"
lr712.ads:22:32: found a string type
lr712.ads:25:28: incorrect placement of aspect "VOLATILE_FUNCTION"
lr712-error_3.adb:4:08: aspect specification must appear in subprogram
  declaration
lr71215.ads:13:13: incompatible volatile function values in effect
lr71215.ads:13:13: "Func_1" declared at line 8 with Volatile_Function value
  "False"
lr71215.ads:13:13: overridden at line 13 with Volatile_Function value "True"
lr7138.ads:23:32: external state "External_State" cannot act as global item of
  nonvolatile function
lr7138.ads:24:32: volatile object "Obj_1" cannot act as global item of a
  function
lr7138.ads:25:32: volatile object "Obj_2" cannot act as global item of a
  function
lr7138.ads:26:32: volatile object "Obj_3" cannot act as global item of a
  function
lr7138.ads:27:32: volatile object "Obj_4" cannot act as global item of a
  function
lr7138.ads:28:32: volatile object "Obj_5" cannot act as global item of a
  function
lr7139.ads:21:13: nonvolatile function "Error_1" cannot have a volatile return
  type
lr7139.ads:22:13: nonvolatile function "Error_2" cannot have a volatile return
  type
lr7139.ads:23:13: nonvolatile function "Error_3" cannot have a volatile return
  type
lr7139.ads:24:13: nonvolatile function "Error_4" cannot have a volatile return
  type
lr7139.ads:25:13: nonvolatile function "Error_5" cannot have a volatile return
  type
lr7139.ads:27:07: nonvolatile function "Error_6" cannot have a volatile
  parameter
lr7139.ads:28:07: nonvolatile function "Error_6" cannot have a volatile
  parameter
lr7139.ads:29:07: nonvolatile function "Error_6" cannot have a volatile
  parameter
lr7139.ads:30:07: nonvolatile function "Error_6" cannot have a volatile
  parameter
lr7139.ads:31:07: nonvolatile function "Error_6" cannot have a volatile
  parameter
lr71312.adb:25:14: volatile object cannot appear in this context (SPARK RM
  7.1.3(12))
lr71312.adb:30:34: volatile object cannot appear in this context (SPARK RM
  7.1.3(12))
lr71312.adb:35:10: volatile object cannot appear in this context (SPARK RM
  7.1.3(12))

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

2015-10-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb Add aspect Volatile_Function to table
	Canonical_Aspect.
	* aspect.ads Add aspect Volatile_Function to tables
	Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names
	and Implementation_Defined_Aspect.  Aspects Async_Readers,
	Async_Writers, Effective_Reads and Effective_Writes are no
	longer Boolean.
	* einfo.adb (Get_Pragma): Add an entry for pragma
	Volatile_Function.
	* par-prag.adb (Prag): Pragma Volatile_Function does not need
	special processing by the parser.
	* rtsfind.ads Add an entry for Ada.Synchronous_Task_Control in
	table RTU_Id. Add an entry for Suspension_Object in table RE_Id.
	* sem_ch3.adb Fix SPARK RM references.
	(Analyze_Object_Contract): Update the error guard.
	* sem_ch5.adb Fix SPARK RM references.
	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Ensure
	that a non-volatile function does not contain an effectively
	volatile parameter.
	(Analyze_Subprogram_Contract): Ensure
	that a non-volatile function does not contain an effectively
	volatile parameter.
	* sem_ch12.adb (Instantiate_Object): Remove the reference to
	the SPARK RM from the error message.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add
	processing for aspects Async_Readers, Async_Writers,
	Effective_Reads, Effective_Writes and Volatile_Function.
	(Check_Aspect_At_Freeze_Point): Aspects Async_Readers,
	Async_Writers, Effective_Reads, Effective_Writes and
	Volatile_Function do not need special processing at the freeze
	point.
	* sem_prag.adb Add an entry for pragma Volatile_Function in
	table Sig_Flags.
	(Analyze_External_Property_In_Decl_Part):
	Reimplemented as Async_Readers, Async_Writers, Effective_Reads
	and Effective_Writes are no longer Boolean pragmas.
	(Analyze_Global_Item): An external state or effectively
	volatile object cannot appear as an item in pragma
	[Refined_]Global.
	(Analyze_Pragma): Change the implementation
	of Async_Readers, Async_Writers, Effective_Reads and
	Effective_Writes as these are no longer Boolean pragmas.
	Use routine Check_Static_Boolean_Expression to verify the
	optional Boolean expression of Async_Readers, Async_Writers,
	Constant_After_Elaboration, Effective_Reads, Effective_Writes,
	Extensions_Visible and Volatile_Function.  Add processing for
	pragma Volatile_Function.
	(Check_Static_Boolean_Expression): New routine.
	(Find_Related_Context): Update the comment on usage.
	(Is_Enabled_Pragma): New routine.
	* sem_prag.ads (Is_Enabled_Pragma): New routine.
	* sem_res.adb Fix SPARK RM references.
	(Is_OK_Volatile_Context): Add detection for return statements.
	(Resolve_Actuals): Remove the check concerning an effectively volatile
	OUT actual parameter as this is now done by the SPARK flow analyzer.
	(Resolve_Entity_Name): Remove the check concerning an effectively
	volatile OUT formal parameter as this is now done by the SPARK
	flow analyzer.	(Within_Volatile_Function): New routine.
	* sem_util.adb (Add_Contract_Item): Add processing for pragma
	Volatile_Function.
	(Check_Nonvolatile_Function_Profile): New routine.
	(Is_Descendant_Of_Suspension_Object): New routine.
	(Is_Effectively_Volatile): Protected types and descendants of
	Suspension_Object are now treated as effectively volatile.
	(Is_Enabled): The optional Boolean expression of pragmas
	Async_Readers, Async_Writers, Effective_Reads and Effective_Writes
	now appears as the first argument.
	(Is_Volatile_Function): New routine.
	* sem_util.ads Add SPARK RM references.
	(Add_Contract_Item): Update the comment on usage.
	(Check_Nonvolatile_Function_Profile): New routine.
	(Is_Effectively_Volatile): Update the comment on usage.
	(Is_Volatile_Function): New routine.
	* snames.ads-tmpl Add a predefined name and pragma id for
	Volatile_Function.

[Ada] Volatile functions

Commit Message

Patch