This patch implements the following SPARK rule from 6.1.4:
The Depends and Refined_Depends aspect of a task unit T need not mention
this implicit parameter; an implicit specification of "T => T" is assumed,
although this may be confirmed explicitly.
------------
-- Source --
------------
-- implicit_tasks.ads
package Implicit_Tasks with
SPARK_Mode,
Abstract_State => State
is
-- Single tasks
task OK_1 with
Global => (Input => State),
Depends => (null => State); -- OK
task OK_2 with
Global => (Output => State),
Depends => ((State, OK_2) => OK_2); -- OK
task Error_1 with
Global => (Output => State),
Depends => (State => Error_1); -- Error
task Error_2 with
Global => (In_Out => State),
Depends => ((State, Error_2) => State); -- Error
-- Task types
task type OK_3 with
Global => (Input => State),
Depends => (null => State); -- OK
task type OK_4 with
Global => (Output => State),
Depends => ((State, OK_4) => OK_4); -- OK
task type Error_3 with
Global => (Output => State),
Depends => (State => Error_3); -- Error
task type Error_4 with
Global => (In_Out => State),
Depends => ((State, Error_4) => State); -- Error
-- Task types with definitions
task type OK_5 with
Global => (Input => State),
Depends => (null => State) -- OK
is end OK_5;
task type OK_6 with
Global => (Output => State),
Depends => ((State, OK_6) => OK_6) -- OK
is end OK_6;
task type Error_5 with
Global => (Output => State),
Depends => (State => Error_5) -- Error
is end Error_5;
task type Error_6 with
Global => (In_Out => State),
Depends => ((State, Error_6) => State) -- Error
is end Error_6;
end Implicit_Tasks;
-- implicit_tasks.adb
package body Implicit_Tasks with
SPARK_Mode,
Refined_State => (State => Var)
is
Var : Integer := 1;
task body OK_1 with
Refined_Global => (Input => Var),
Refined_Depends => (null => Var) -- OK
is begin null; end OK_1;
task body OK_2 with
Refined_Global => (Output => Var),
Refined_Depends => ((Var, OK_2) => OK_2) -- OK
is begin null; end OK_2;
task body Error_1 with
Refined_Global => (Output => Var),
Refined_Depends => (Var => Error_1) -- Error
is begin null; end Error_1;
task body Error_2 with
Refined_Global => (In_Out => Var),
Refined_Depends => ((Var, Error_2) => Var) -- Error
is begin null; end Error_2;
task body OK_3 with
Refined_Global => (Input => Var),
Refined_Depends => (null => Var) -- OK
is begin null; end OK_3;
task body OK_4 with
Refined_Global => (Output => Var),
Refined_Depends => ((Var, OK_4) => OK_4) -- OK
is begin null; end OK_4;
task body Error_3 with
Refined_Global => (Output => Var),
Refined_Depends => (Var => Error_3) -- Error
is begin null; end Error_3;
task body Error_4 with
Refined_Global => (In_Out => Var),
Refined_Depends => ((Var, Error_4) => Var) -- Error
is begin null; end Error_4;
task body OK_5 with
Refined_Global => (Input => Var),
Refined_Depends => (null => Var) -- OK
is begin null; end OK_5;
task body OK_6 with
Refined_Global => (Output => Var),
Refined_Depends => ((Var, OK_6) => OK_6) -- OK
is begin null; end OK_6;
task body Error_5 with
Refined_Global => (Output => Var),
Refined_Depends => (Var => Error_5) -- Error
is begin null; end Error_5;
task body Error_6 with
Refined_Global => (In_Out => Var),
Refined_Depends => ((Var, Error_6) => Var) -- Error
is begin null; end Error_6;
end Implicit_Tasks;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c implicit_tasks.adb
implicit_tasks.adb:19:06: current instance of task type "Error_1" is missing
from output dependence list
implicit_tasks.adb:24:06: current instance of task type "Error_2" is missing
from input dependence list
implicit_tasks.adb:39:06: current instance of task type "Error_3" is missing
from output dependence list
implicit_tasks.adb:44:06: current instance of task type "Error_4" is missing
from input dependence list
implicit_tasks.adb:59:06: current instance of task type "Error_5" is missing
from output dependence list
implicit_tasks.adb:64:06: current instance of task type "Error_6" is missing
from input dependence list
implicit_tasks.ads:17:06: current instance of task type "Error_1" is missing
from output dependence list
implicit_tasks.ads:21:06: current instance of task type "Error_2" is missing
from input dependence list
implicit_tasks.ads:35:06: current instance of task type "Error_3" is missing
from output dependence list
implicit_tasks.ads:39:06: current instance of task type "Error_4" is missing
from input dependence list
implicit_tasks.ads:55:06: current instance of task type "Error_5" is missing
from output dependence list
implicit_tasks.ads:60:06: current instance of task type "Error_6" is missing
from input dependence list
Tested on x86_64-pc-linux-gnu, committed on trunk
2016-04-18 Hristian Kirtchev <kirtc...@adacore.com>
* sem_prag.adb (Analyze_Depends_In_Decl_Part):
Add global variables Task_Input_Seen and Task_Output_Seen.
(Analyze_Global_Item): Detect an illegal use of the current
instance of a single protected/task type in a global annotation.
(Analyze_Input_Output): Inputs and output related to the current
instance of a task unit are now tracked.
(Check_Usage): Require
the presence of the current instance of a task unit only when
one input/output is available. (Current_Task_Instance_Seen):
New routine.
(Is_CCT_Instance): New parameter profile. Update
the comment on usage. The routine now properly recognizes several
cases related to single protected/task types.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 235100)
+++ sem_prag.adb (working copy)
@@ -245,10 +245,13 @@
-- Determine whether dependency clause Clause is surrounded by extra
-- parentheses. If this is the case, issue an error message.
- function Is_CCT_Instance (Ref : Node_Id) return Boolean;
+ function Is_CCT_Instance
+ (Ref_Id : Entity_Id;
+ Context_Id : Entity_Id) return Boolean;
-- Subsidiary to the analysis of pragmas [Refined_]Depends and [Refined_]
- -- Global. Determine whether reference Ref denotes the current instance of
- -- a concurrent type.
+ -- Global. Determine whether entity Ref_Id denotes the current instance of
+ -- a concurrent type. Context_Id denotes the associated context where the
+ -- pragma appears.
function Is_Unconstrained_Or_Tagged_Item (Item : Entity_Id) return Boolean;
-- Subsidiary to Collect_Subprogram_Inputs_Outputs and the analysis of
@@ -559,6 +562,10 @@
-- Two lists containing the full set of inputs and output of the related
-- subprograms. Note that these lists contain both nodes and entities.
+ Task_Input_Seen : Boolean := False;
+ Task_Output_Seen : Boolean := False;
+ -- Flags used to track the implicit dependence of a task unit on itself
+
procedure Add_Item_To_Name_Buffer (Item_Id : Entity_Id);
-- Subsidiary routine to Check_Role and Check_Usage. Add the item kind
-- to the name buffer. The individual kinds are as follows:
@@ -590,7 +597,7 @@
Item_Id : Entity_Id;
Is_Input : Boolean;
Self_Ref : Boolean);
- -- Ensure that an item fulfils its designated input and/or output role
+ -- Ensure that an item fulfills its designated input and/or output role
-- as specified by pragma Global (if any) or the enclosing context. If
-- this is not the case, emit an error. Item and Item_Id denote the
-- attributes of an item. Flag Is_Input should be set when item comes
@@ -763,10 +770,31 @@
Null_Seen : in out Boolean;
Non_Null_Seen : in out Boolean)
is
+ procedure Current_Task_Instance_Seen;
+ -- Set the appropriate global flag when the current instance of a
+ -- task unit is encountered.
+
+ --------------------------------
+ -- Current_Task_Instance_Seen --
+ --------------------------------
+
+ procedure Current_Task_Instance_Seen is
+ begin
+ if Is_Input then
+ Task_Input_Seen := True;
+ else
+ Task_Output_Seen := True;
+ end if;
+ end Current_Task_Instance_Seen;
+
+ -- Local variables
+
Is_Output : constant Boolean := not Is_Input;
Grouped : Node_Id;
Item_Id : Entity_Id;
+ -- Start of processing for Analyze_Input_Output
+
begin
-- Multiple input or output items appear as an aggregate
@@ -899,18 +927,45 @@
Ekind_In (Item_Id, E_Abstract_State, E_Variable)
then
- -- The item denotes a concurrent type, but it is not the
- -- current instance of an enclosing concurrent type.
+ -- The item denotes a concurrent type. Note that single
+ -- protected/task types are not considered here because
+ -- they behave as objects in the context of pragma
+ -- [Refined_]Depends.
- if Ekind_In (Item_Id, E_Protected_Type, E_Task_Type)
- and then not Is_CCT_Instance (Item)
+ if Ekind_In (Item_Id, E_Protected_Type, E_Task_Type) then
+
+ -- This use is legal as long as the concurrent type is
+ -- the current instance of an enclosing type.
+
+ if Is_CCT_Instance (Item_Id, Spec_Id) then
+
+ -- The dependence of a task unit on itself is
+ -- implicit and may or may not be explicitly
+ -- specified (SPARK RM 6.1.4).
+
+ if Ekind (Item_Id) = E_Task_Type then
+ Current_Task_Instance_Seen;
+ end if;
+
+ -- Otherwise this is not the current instance
+
+ else
+ SPARK_Msg_N
+ ("invalid use of subtype mark in dependency "
+ & "relation", Item);
+ end if;
+
+ -- The dependency of a task unit on itself is implicit
+ -- and may or may not be explicitly specified
+ -- (SPARK RM 6.1.4).
+
+ elsif Is_Single_Task_Object (Item_Id)
+ and then Is_CCT_Instance (Item_Id, Spec_Id)
then
- SPARK_Msg_N
- ("invalid use of subtype mark in dependency "
- & "relation", Item);
+ Current_Task_Instance_Seen;
end if;
- -- Ensure that the item fulfils its role as input and/or
+ -- Ensure that the item fulfills its role as input and/or
-- output as specified by pragma Global or the enclosing
-- context.
@@ -1427,14 +1482,31 @@
if Present (Item_Id)
and then not Contains (Used_Items, Item_Id)
then
- -- The current instance of a concurrent type behaves as a
- -- formal parameter (SPARK RM 6.1.4).
+ if Is_Formal (Item_Id) then
+ Usage_Error (Item_Id);
- if Is_Formal (Item_Id)
- or else Ekind_In (Item_Id, E_Protected_Type, E_Task_Type)
+ -- The current instance of a protected type behaves as a formal
+ -- parameter (SPARK RM 6.1.4).
+
+ elsif Ekind (Item_Id) = E_Protected_Type
+ or else Is_Single_Protected_Object (Item_Id)
then
Usage_Error (Item_Id);
+ -- The current instance of a task type behaves as a formal
+ -- parameter (SPARK RM 6.1.4).
+
+ elsif Ekind (Item_Id) = E_Task_Type
+ or else Is_Single_Task_Object (Item_Id)
+ then
+ -- The dependence of a task unit on itself is implicit and
+ -- may or may not be explicitly specified (SPARK RM 6.1.4).
+ -- Emit an error if only one input/output is present.
+
+ if Task_Input_Seen /= Task_Output_Seen then
+ Usage_Error (Item_Id);
+ end if;
+
-- States and global objects are not used properly only when
-- the subprogram is subject to pragma Global.
@@ -2036,20 +2108,18 @@
end if;
-- A global item may denote a concurrent type as long as it is
- -- the current instance of an enclosing concurrent type
+ -- the current instance of an enclosing protected or task type
-- (SPARK RM 6.1.4).
elsif Ekind_In (Item_Id, E_Protected_Type, E_Task_Type) then
- if Is_CCT_Instance (Item) then
+ if Is_CCT_Instance (Item_Id, Spec_Id) then
-- Pragma [Refined_]Global associated with a protected
-- subprogram cannot mention the current instance of a
-- protected type because the instance behaves as a
-- formal parameter.
- if Ekind (Item_Id) = E_Protected_Type
- and then Scope (Spec_Id) = Item_Id
- then
+ if Ekind (Item_Id) = E_Protected_Type then
Error_Msg_Name_1 := Chars (Item_Id);
SPARK_Msg_NE
(Fix_Msg (Spec_Id, "global item of subprogram & "
@@ -2061,9 +2131,7 @@
-- cannot mention the current instance of a task type
-- because the instance behaves as a formal parameter.
- elsif Ekind (Item_Id) = E_Task_Type
- and then Spec_Id = Item_Id
- then
+ else pragma Assert (Ekind (Item_Id) = E_Task_Type);
Error_Msg_Name_1 := Chars (Item_Id);
SPARK_Msg_NE
(Fix_Msg (Spec_Id, "global item of subprogram & "
@@ -2081,6 +2149,39 @@
return;
end if;
+ -- A global item may denote the anonymous object created for a
+ -- single protected/task type as long as the current instance
+ -- is the same single type (SPARK RM 6.1.4).
+
+ elsif Is_Single_Concurrent_Object (Item_Id)
+ and then Is_CCT_Instance (Item_Id, Spec_Id)
+ then
+ -- Pragma [Refined_]Global associated with a protected
+ -- subprogram cannot mention the current instance of a
+ -- protected type because the instance behaves as a formal
+ -- parameter.
+
+ if Is_Single_Protected_Object (Item_Id) then
+ Error_Msg_Name_1 := Chars (Item_Id);
+ SPARK_Msg_NE
+ (Fix_Msg (Spec_Id, "global item of subprogram & cannot "
+ & "reference current instance of protected type %"),
+ Item, Spec_Id);
+ return;
+
+ -- Pragma [Refined_]Global associated with a task type
+ -- cannot mention the current instance of a task type
+ -- because the instance behaves as a formal parameter.
+
+ else pragma Assert (Is_Single_Task_Object (Item_Id));
+ Error_Msg_Name_1 := Chars (Item_Id);
+ SPARK_Msg_NE
+ (Fix_Msg (Spec_Id, "global item of subprogram & cannot "
+ & "reference current instance of task type %"),
+ Item, Spec_Id);
+ return;
+ end if;
+
-- A formal object may act as a global item inside a generic
elsif Is_Formal_Object (Item_Id) then
@@ -27455,24 +27556,56 @@
-- Is_CCT_Instance --
---------------------
- function Is_CCT_Instance (Ref : Node_Id) return Boolean is
- Ref_Id : constant Entity_Id := Entity (Ref);
- S : Entity_Id;
+ function Is_CCT_Instance
+ (Ref_Id : Entity_Id;
+ Context_Id : Entity_Id) return Boolean
+ is
+ S : Entity_Id;
+ Typ : Entity_Id;
begin
- -- Climb the scope chain looking for an enclosing concurrent type that
- -- matches the referenced entity.
+ -- When the reference denotes a single protected type, the context is
+ -- either a protected subprogram or its body.
- S := Current_Scope;
- while Present (S) and then S /= Standard_Standard loop
- if Ekind_In (S, E_Protected_Type, E_Task_Type) and then S = Ref_Id
- then
- return True;
+ if Is_Single_Protected_Object (Ref_Id) then
+ Typ := Scope (Context_Id);
+
+ return
+ Ekind (Typ) = E_Protected_Type
+ and then Present (Anonymous_Object (Typ))
+ and then Anonymous_Object (Typ) = Ref_Id;
+
+ -- When the reference denotes a single task type, the context is either
+ -- the same type or if inside the body, the anonymous task type.
+
+ elsif Is_Single_Task_Object (Ref_Id) then
+ if Ekind (Context_Id) = E_Task_Type then
+ return
+ Present (Anonymous_Object (Context_Id))
+ and then Anonymous_Object (Context_Id) = Ref_Id;
+ else
+ return Ref_Id = Context_Id;
end if;
- S := Scope (S);
- end loop;
+ -- Otherwise the reference denotes a protected or a task type. Climb the
+ -- scope chain looking for an enclosing concurrent type that matches the
+ -- referenced entity.
+ else
+ pragma Assert (Ekind_In (Ref_Id, E_Protected_Type, E_Task_Type));
+
+ S := Current_Scope;
+ while Present (S) and then S /= Standard_Standard loop
+ if Ekind_In (S, E_Protected_Type, E_Task_Type)
+ and then S = Ref_Id
+ then
+ return True;
+ end if;
+
+ S := Scope (S);
+ end loop;
+ end if;
+
return False;
end Is_CCT_Instance;
