This patch implements the following rules concerning the refinement of external
abstract states:
* A state abstraction that is not specified as External shall not have
constituents which are External states.
* An External state abstraction shall have at least one constituent that is
External state, or shall have a null refinement.
* An External state abstraction shall have each of the properties set to True
which are True for any of its constituents.
* Refined_Global aspects must respect the rules related to external properties
of constituents which are external states given in External State and External
State - Variables.
------------
-- Source --
------------
-- semantics.ads
package Semantics
with Abstract_State =>
(State,
(AR_AW_ER_EW_State_1 with External),
(AR_AW_ER_EW_State_2 with External),
(AR_AW_ER_EW_State_3 with External),
(AR_EW_State with External => (Async_Readers, Effective_Writes)),
(AW_ER_State with External => (Async_Writers, Effective_Reads)))
is
procedure Proc
with Global => (Input => AW_ER_State);
end Semantics;
-- semantics.adb
package body Semantics
with Refined_State =>
(State =>
(Var_1, AR_1), -- error
AR_AW_ER_EW_State_1 =>
null, -- ok
AR_AW_ER_EW_State_2 =>
(Var_2_1, Var_2_2), -- error
AR_AW_ER_EW_State_3 =>
(AR_EW_3, AW_3), -- error
AR_EW_State =>
(AW_ER_4, AR_EW_4), -- error
AW_ER_State =>
AW_ER_5) -- ok
is
Var_1 : Integer := 1;
Var_2_1 : Integer := 2;
Var_2_2 : Integer := 3;
AR_1 : Integer := 4 with Volatile, Async_Readers;
AR_EW_3 : Integer := 5 with Volatile, Async_Readers, Effective_Writes;
AW_3 : Integer := 6 with Volatile, Async_Writers;
AR_EW_4 : Integer := 7 with Volatile, Async_Readers, Effective_Writes;
AW_ER_4 : Integer := 8 with Volatile, Async_Writers, Effective_Reads;
AW_ER_5 : Integer := 9 with Volatile, Async_Writers, Effective_Reads;
procedure Proc
with Refined_Global => (Input => AW_ER_5) -- error
is begin null; end Proc;
end Semantics;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c semantics.adb
semantics.adb:3:06: non-external state "State" cannot contain external
constituents in refinement (SPARK RM 7.2.8(1))
semantics.adb:7:06: external state "Ar_Aw_Er_Ew_State_2" requires at least one
external constituent or null refinement (SPARK RM 7.2.8(2))
semantics.adb:9:06: external state "Ar_Aw_Er_Ew_State_3" requires at least one
constituent with property "Effective_Reads" (SPARK RM 7.2.8(3))
semantics.adb:11:06: external state "Ar_Ew_State" lacks property
"Async_Writers" set by constituent "Aw_Er_4" (SPARK RM 7.2.8(3))
semantics.adb:27:39: volatile global item "AW_ER_5" with property
Effective_Reads must have mode In_Out or Output (SPARK RM 7.1.3(11))
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-01-27 Hristian Kirtchev <[email protected]>
* einfo.adb (Has_Option): Reimplemented.
* sem_prag.adb (Analyze_Refinement_Clause): Add global
variables AR_Constit, AW_Constit, ER_Constit, EW_Constit,
External_Constit_Seen and State. Add local variables Body_Ref,
Body_Ref_Elmt and Extra_State. Reimplement part of the logic to
avoid a cumbersome while pool. Verify the legality of an external
state and relevant properties.
(Check_External_Property): New routine.
(Check_Matching_State): Remove parameter profile
and update comment on usage.
(Collect_Constituent): Store the
relevant external property of a constituent.
* sem_util.adb (Async_Readers_Enabled): Update the call to
Has_Enabled_Property.
(Async_Writers_Enabled): Update the call to Has_Enabled_Property.
(Effective_Reads_Enabled): Update the call to Has_Enabled_Property.
(Effective_Writes_Enabled): Update the call to Has_Enabled_Property.
(Has_Enabled_Property): Rename formal parameter Extern to State_Id.
Update comment on usage. Reimplement the logic to recognize the various
formats of properties.
Index: einfo.adb
===================================================================
--- einfo.adb (revision 207138)
+++ einfo.adb (working copy)
@@ -589,10 +589,10 @@
-----------------------
function Has_Option
- (State : Entity_Id;
- Opt_Nam : Name_Id) return Boolean;
- -- Determine whether abstract state State has a particular option denoted
- -- by the name Opt_Nam.
+ (State_Id : Entity_Id;
+ Option_Nam : Name_Id) return Boolean;
+ -- Determine whether abstract state State_Id has particular option denoted
+ -- by the name Option_Nam.
---------------
-- Float_Rep --
@@ -609,33 +609,56 @@
----------------
function Has_Option
- (State : Entity_Id;
- Opt_Nam : Name_Id) return Boolean
+ (State_Id : Entity_Id;
+ Option_Nam : Name_Id) return Boolean
is
- Par : constant Node_Id := Parent (State);
- Opt : Node_Id;
+ Decl : constant Node_Id := Parent (State_Id);
+ Opt : Node_Id;
+ Opt_Nam : Node_Id;
begin
- pragma Assert (Ekind (State) = E_Abstract_State);
+ pragma Assert (Ekind (State_Id) = E_Abstract_State);
- -- States with options appear as extension aggregates in the tree
+ -- The declaration of abstract states with options appear as an
+ -- extension aggregate. If this is not the case, the option is not
+ -- available.
- if Nkind (Par) = N_Extension_Aggregate then
- if Opt_Nam = Name_Part_Of then
- return Present (Component_Associations (Par));
+ if Nkind (Decl) /= N_Extension_Aggregate then
+ return False;
+ end if;
- else
- Opt := First (Expressions (Par));
- while Present (Opt) loop
- if Chars (Opt) = Opt_Nam then
- return True;
- end if;
+ -- Simple options
- Next (Opt);
- end loop;
+ Opt := First (Expressions (Decl));
+ while Present (Opt) loop
+
+ -- Currently the only simple option allowed is External
+
+ if Nkind (Opt) = N_Identifier
+ and then Chars (Opt) = Name_External
+ and then Chars (Opt) = Option_Nam
+ then
+ return True;
end if;
- end if;
+ Next (Opt);
+ end loop;
+
+ -- Complex options with various specifiers
+
+ Opt := First (Component_Associations (Decl));
+ while Present (Opt) loop
+ Opt_Nam := First (Choices (Opt));
+
+ if Nkind (Opt_Nam) = N_Identifier
+ and then Chars (Opt_Nam) = Option_Nam
+ then
+ return True;
+ end if;
+
+ Next (Opt);
+ end loop;
+
return False;
end Has_Option;
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 207140)
+++ sem_prag.adb (working copy)
@@ -22214,25 +22214,45 @@
-------------------------------
procedure Analyze_Refinement_Clause (Clause : Node_Id) is
- State_Id : Entity_Id := Empty;
- -- The entity of the state being refined in the current clause
+ AR_Constit : Entity_Id := Empty;
+ AW_Constit : Entity_Id := Empty;
+ ER_Constit : Entity_Id := Empty;
+ EW_Constit : Entity_Id := Empty;
+ -- The entities of external constituents that contain one of the
+ -- following enabled properties: Async_Readers, Async_Writers,
+ -- Effective_Reads and Effective_Writes.
+ External_Constit_Seen : Boolean := False;
+ -- Flag used to mark when at least one external constituent is part
+ -- of the state refinement.
+
Non_Null_Seen : Boolean := False;
Null_Seen : Boolean := False;
-- Flags used to detect multiple uses of null in a single clause or a
-- mixture of null and non-null constituents.
+ State : Node_Id;
+ State_Id : Entity_Id;
+ -- The state being refined in the current clause
+
procedure Analyze_Constituent (Constit : Node_Id);
-- Perform full analysis of a single constituent
- procedure Check_Matching_State
- (State : Node_Id;
- State_Id : Entity_Id);
- -- Determine whether state State denoted by its name State_Id appears
- -- in Abstr_States. Emit an error when attempting to re-refine the
- -- state or when the state is not defined in the package declaration.
- -- Otherwise remove the state from Abstr_States.
+ procedure Check_External_Property
+ (Prop_Nam : Name_Id;
+ Enabled : Boolean;
+ Constit : Entity_Id);
+ -- Determine whether a property denoted by name Prop_Nam is present
+ -- in both the refined state and constituent Constit. Flag Enabled
+ -- should be set when the property applies to the refined state. If
+ -- this is not the case, emit an error message.
+ procedure Check_Matching_State;
+ -- Determine whether the state being refined appears in Abstr_States.
+ -- Emit an error when attempting to re-refine the state or when the
+ -- state is not defined in the package declaration. Otherwise remove
+ -- the state from Abstr_States.
+
-------------------------
-- Analyze_Constituent --
-------------------------
@@ -22276,6 +22296,29 @@
-- body declarations end (see routine Analyze_Declarations).
Set_Has_Visible_Refinement (State_Id);
+
+ -- When the constituent is external, save its relevant
+ -- property for further checks.
+
+ if Async_Readers_Enabled (Constit_Id) then
+ AR_Constit := Constit_Id;
+ External_Constit_Seen := True;
+ end if;
+
+ if Async_Writers_Enabled (Constit_Id) then
+ AW_Constit := Constit_Id;
+ External_Constit_Seen := True;
+ end if;
+
+ if Effective_Reads_Enabled (Constit_Id) then
+ ER_Constit := Constit_Id;
+ External_Constit_Seen := True;
+ end if;
+
+ if Effective_Writes_Enabled (Constit_Id) then
+ EW_Constit := Constit_Id;
+ External_Constit_Seen := True;
+ end if;
end Collect_Constituent;
-- Local variables
@@ -22426,14 +22469,44 @@
end if;
end Analyze_Constituent;
+ -----------------------------
+ -- Check_External_Property --
+ -----------------------------
+
+ procedure Check_External_Property
+ (Prop_Nam : Name_Id;
+ Enabled : Boolean;
+ Constit : Entity_Id)
+ is
+ begin
+ Error_Msg_Name_1 := Prop_Nam;
+
+ -- The property is enabled in the related Abstract_State pragma
+ -- that defines the state.
+
+ if Enabled then
+ if No (Constit) then
+ Error_Msg_NE
+ ("external state & requires at least one constituent with "
+ & "property % (SPARK RM 7.2.8(3))", State, State_Id);
+ end if;
+
+ -- The property is missing in the declaration of the state, but a
+ -- constituent is introducing it in the state refinement.
+
+ elsif Present (Constit) then
+ Error_Msg_Name_2 := Chars (Constit);
+ Error_Msg_NE
+ ("external state & lacks property % set by constituent % "
+ & "(SPARK RM 7.2.8(3))", State, State_Id);
+ end if;
+ end Check_External_Property;
+
--------------------------
-- Check_Matching_State --
--------------------------
- procedure Check_Matching_State
- (State : Node_Id;
- State_Id : Entity_Id)
- is
+ procedure Check_Matching_State is
State_Elmt : Elmt_Id;
begin
@@ -22478,8 +22551,10 @@
-- Local declarations
- Constit : Node_Id;
- State : Node_Id;
+ Body_Ref : Node_Id;
+ Body_Ref_Elmt : Elmt_Id;
+ Constit : Node_Id;
+ Extra_State : Node_Id;
-- Start of processing for Analyze_Refinement_Clause
@@ -22487,68 +22562,61 @@
-- Analyze the state name of a refinement clause
State := First (Choices (Clause));
- while Present (State) loop
- if Present (State_Id) then
- Error_Msg_N
- ("refinement clause cannot cover multiple states", State);
- else
- Analyze (State);
- Resolve_State (State);
+ Analyze (State);
+ Resolve_State (State);
- -- Ensure that the state name denotes a valid abstract state
- -- that is defined in the spec of the related package.
+ -- Ensure that the state name denotes a valid abstract state that is
+ -- defined in the spec of the related package.
- if Is_Entity_Name (State) then
- State_Id := Entity_Of (State);
+ if Is_Entity_Name (State) then
+ State_Id := Entity_Of (State);
- -- Catch any attempts to re-refine a state or refine a
- -- state that is not defined in the package declaration.
+ -- Catch any attempts to re-refine a state or refine a state that
+ -- is not defined in the package declaration.
- if Ekind (State_Id) = E_Abstract_State then
- Check_Matching_State (State, State_Id);
- else
- Error_Msg_NE
- ("& must denote an abstract state", State, State_Id);
- end if;
+ if Ekind (State_Id) = E_Abstract_State then
+ Check_Matching_State;
+ else
+ Error_Msg_NE
+ ("& must denote an abstract state", State, State_Id);
+ end if;
- -- A global item cannot denote a state abstraction whose
- -- refinement is visible, in other words a state abstraction
- -- cannot be named within its enclosing package's body other
- -- than in its refinement.
+ -- A global item cannot denote a state abstraction whose
+ -- refinement is visible, in other words a state abstraction
+ -- cannot be named within its enclosing package's body other than
+ -- in its refinement.
- if Has_Body_References (State_Id) then
- declare
- Ref : Node_Id;
- Ref_Elmt : Elmt_Id;
+ if Has_Body_References (State_Id) then
+ Body_Ref_Elmt := First_Elmt (Body_References (State_Id));
+ while Present (Body_Ref_Elmt) loop
+ Body_Ref := Node (Body_Ref_Elmt);
- begin
- Ref_Elmt := First_Elmt (Body_References (State_Id));
- while Present (Ref_Elmt) loop
- Ref := Node (Ref_Elmt);
+ Error_Msg_N
+ ("global reference to & not allowed (SPARK RM 6.1.4(8))",
+ Body_Ref);
+ Error_Msg_Sloc := Sloc (State);
+ Error_Msg_N ("\refinement of & is visible#", Body_Ref);
- Error_Msg_N
- ("global reference to & not allowed (SPARK RM "
- & "6.1.4(8))", Ref);
- Error_Msg_Sloc := Sloc (State);
- Error_Msg_N ("\refinement of & is visible#", Ref);
+ Next_Elmt (Body_Ref_Elmt);
+ end loop;
+ end if;
- Next_Elmt (Ref_Elmt);
- end loop;
- end;
- end if;
+ -- The state name is illegal
- -- The state name is illegal
+ else
+ Error_Msg_N ("malformed state name in refinement clause", State);
+ end if;
- else
- Error_Msg_N
- ("malformed state name in refinement clause", State);
- end if;
- end if;
+ -- A refinement clause may only refine one state at a time
- Next (State);
- end loop;
+ Extra_State := Next (State);
+ if Present (Extra_State) then
+ Error_Msg_N
+ ("refinement clause cannot cover multiple states", Extra_State);
+ end if;
+
-- Analyze all constituents of the refinement. Multiple constituents
-- appear as an aggregate.
@@ -22575,6 +22643,60 @@
else
Analyze_Constituent (Constit);
end if;
+
+ -- A refined external state is subject to special rules with respect
+ -- to its properties and constituents.
+
+ if Is_External_State (State_Id) then
+
+ -- The set of properties that all external constituents yield must
+ -- match that of the refined state. There are two cases to detect:
+ -- the refined state lacks a property or has an extra property.
+
+ if External_Constit_Seen then
+ Check_External_Property
+ (Prop_Nam => Name_Async_Readers,
+ Enabled => Async_Readers_Enabled (State_Id),
+ Constit => AR_Constit);
+
+ Check_External_Property
+ (Prop_Nam => Name_Async_Writers,
+ Enabled => Async_Writers_Enabled (State_Id),
+ Constit => AW_Constit);
+
+ Check_External_Property
+ (Prop_Nam => Name_Effective_Reads,
+ Enabled => Effective_Reads_Enabled (State_Id),
+ Constit => ER_Constit);
+
+ Check_External_Property
+ (Prop_Nam => Name_Effective_Writes,
+ Enabled => Effective_Writes_Enabled (State_Id),
+ Constit => EW_Constit);
+
+ -- An external state may be refined to null (SPARK RM 7.2.8(2))
+
+ elsif Null_Seen then
+ null;
+
+ -- The external state has constituents, but none of them are
+ -- external.
+
+ else
+ Error_Msg_NE
+ ("external state & requires at least one external "
+ & "constituent or null refinement (SPARK RM 7.2.8(2))",
+ State, State_Id);
+ end if;
+
+ -- When a refined state is not external, it should not have external
+ -- constituents.
+
+ elsif External_Constit_Seen then
+ Error_Msg_NE
+ ("non-external state & cannot contain external constituents in "
+ & "refinement (SPARK RM 7.2.8(1))", State, State_Id);
+ end if;
end Analyze_Refinement_Clause;
---------------------------
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 207141)
+++ sem_util.adb (working copy)
@@ -114,11 +114,11 @@
-- have a default.
function Has_Enabled_Property
- (Extern : Node_Id;
+ (State_Id : Node_Id;
Prop_Nam : Name_Id) return Boolean;
-- Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled.
- -- Given pragma External, determine whether it contains a property denoted
- -- by its name Prop_Nam and if it does, whether its expression is True.
+ -- Determine whether an abstract state denoted by its entity State_Id has
+ -- enabled property Prop_Name.
function Has_Null_Extension (T : Entity_Id) return Boolean;
-- T is a derived tagged type. Check whether the type extension is null.
@@ -560,10 +560,7 @@
function Async_Readers_Enabled (Id : Entity_Id) return Boolean is
begin
if Ekind (Id) = E_Abstract_State then
- return
- Has_Enabled_Property
- (Extern => Get_Pragma (Id, Pragma_External),
- Prop_Nam => Name_Async_Readers);
+ return Has_Enabled_Property (Id, Name_Async_Readers);
else pragma Assert (Ekind (Id) = E_Variable);
return Present (Get_Pragma (Id, Pragma_Async_Readers));
@@ -577,10 +574,7 @@
function Async_Writers_Enabled (Id : Entity_Id) return Boolean is
begin
if Ekind (Id) = E_Abstract_State then
- return
- Has_Enabled_Property
- (Extern => Get_Pragma (Id, Pragma_External),
- Prop_Nam => Name_Async_Writers);
+ return Has_Enabled_Property (Id, Name_Async_Writers);
else pragma Assert (Ekind (Id) = E_Variable);
return Present (Get_Pragma (Id, Pragma_Async_Writers));
@@ -4818,10 +4812,7 @@
function Effective_Reads_Enabled (Id : Entity_Id) return Boolean is
begin
if Ekind (Id) = E_Abstract_State then
- return
- Has_Enabled_Property
- (Extern => Get_Pragma (Id, Pragma_External),
- Prop_Nam => Name_Effective_Reads);
+ return Has_Enabled_Property (Id, Name_Effective_Reads);
else pragma Assert (Ekind (Id) = E_Variable);
return Present (Get_Pragma (Id, Pragma_Effective_Reads));
@@ -4835,10 +4826,7 @@
function Effective_Writes_Enabled (Id : Entity_Id) return Boolean is
begin
if Ekind (Id) = E_Abstract_State then
- return
- Has_Enabled_Property
- (Extern => Get_Pragma (Id, Pragma_External),
- Prop_Nam => Name_Effective_Writes);
+ return Has_Enabled_Property (Id, Name_Effective_Writes);
else pragma Assert (Ekind (Id) = E_Variable);
return Present (Get_Pragma (Id, Pragma_Effective_Writes));
@@ -7182,69 +7170,86 @@
--------------------------
function Has_Enabled_Property
- (Extern : Node_Id;
+ (State_Id : Node_Id;
Prop_Nam : Name_Id) return Boolean
is
- Prop : Node_Id;
- Props : Node_Id := Empty;
+ Decl : constant Node_Id := Parent (State_Id);
+ Opt : Node_Id;
+ Opt_Nam : Node_Id;
+ Prop : Node_Id;
+ Props : Node_Id;
begin
- -- The related abstract state or variable do not have an Extern pragma,
- -- the property in question cannot be set.
+ -- The declaration of an external abstract state appears as an extension
+ -- aggregate. If this is not the case, properties can never be set.
- if No (Extern) then
+ if Nkind (Decl) /= N_Extension_Aggregate then
return False;
-
- elsif Nkind (Extern) = N_Component_Association then
- Props := Expression (Extern);
end if;
- -- External state with properties
+ -- When External appears as a simple option, it automatically enables
+ -- all properties.
- if Present (Props) then
+ Opt := First (Expressions (Decl));
+ while Present (Opt) loop
+ if Nkind (Opt) = N_Identifier
+ and then Chars (Opt) = Name_External
+ then
+ return True;
+ end if;
- -- Multiple properties appear as an aggregate
+ Next (Opt);
+ end loop;
- if Nkind (Props) = N_Aggregate then
+ -- When External specifies particular properties, inspect those and
+ -- find the desired one (if any).
- -- Simple property form
+ Opt := First (Component_Associations (Decl));
+ while Present (Opt) loop
+ Opt_Nam := First (Choices (Opt));
- Prop := First (Expressions (Props));
- while Present (Prop) loop
- if Chars (Prop) = Prop_Nam then
- return True;
- end if;
+ if Nkind (Opt_Nam) = N_Identifier
+ and then Chars (Opt_Nam) = Name_External
+ then
+ Props := Expression (Opt);
- Next (Prop);
- end loop;
+ -- Multiple properties appear as an aggregate
- -- Property with expression form
+ if Nkind (Props) = N_Aggregate then
- Prop := First (Component_Associations (Props));
- while Present (Prop) loop
- if Chars (Prop) = Prop_Nam then
- return Is_True (Expr_Value (Expression (Prop)));
- end if;
+ -- Simple property form
- Next (Prop);
- end loop;
+ Prop := First (Expressions (Props));
+ while Present (Prop) loop
+ if Chars (Prop) = Prop_Nam then
+ return True;
+ end if;
- -- Pragma Extern contains properties, but not the one we want
+ Next (Prop);
+ end loop;
- return False;
+ -- Property with expression form
- -- Single property
+ Prop := First (Component_Associations (Props));
+ while Present (Prop) loop
+ if Chars (Prop) = Prop_Nam then
+ return Is_True (Expr_Value (Expression (Prop)));
+ end if;
- else
- return Chars (Prop) = Prop_Nam;
+ Next (Prop);
+ end loop;
+
+ -- Single property
+
+ else
+ return Chars (Prop) = Prop_Nam;
+ end if;
end if;
- -- An external state defined without any properties defaults all
- -- properties to True;
+ Next (Opt);
+ end loop;
- else
- return True;
- end if;
+ return False;
end Has_Enabled_Property;
--------------------
