===================================================================
@@ -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;
===================================================================
@@ -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;
---------------------------
===================================================================
@@ -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;
--------------------
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 <kirtchev@adacore.com> * 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.