procyberian/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

ada: Allow No_Caching on volatile types

Browse source 
SPARK RM now allow the property No_Caching on volatile types, to
indicate that they should be considered volatile for compilation, but
not by GNATprove's analysis.

gcc/ada/

	* contracts.adb (Add_Contract_Item): Allow No_Caching on types.
	(Check_Type_Or_Object_External_Properties): Check No_Caching.
	Check that non-effectively volatile types does not contain an
	effectively volatile component (instead of just a volatile
	component).
	(Analyze_Object_Contract): Remove shared checking of No_Caching.
	* sem_prag.adb (Analyze_External_Property_In_Decl_Part): Adapt checking
	of No_Caching for types.
	(Analyze_Pragma): Allow No_Caching on types.
	* sem_util.adb (Has_Effectively_Volatile_Component): New query function.
	(Is_Effectively_Volatile): Type with Volatile and No_Caching is not
	effectively volatile.
	(No_Caching_Enabled): Remove assertion to apply to all entities.
	* sem_util.ads: Same.
This commit is contained in:
Yannick Moy 2022-11-25 17:16:06 +01:00 • committed by Marc Poulhiès
parent 7dc44f280e
commit 400d9fc1f0
4 changed files with 83 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
gcc/ada/contracts.adb
View file

@ -316,6 +316,7 @@ package body Contracts is
| Name_Async_Writers
| Name_Effective_Reads
| Name_Effective_Writes
| Name_No_Caching
or else (Ekind (Id) = E_Task_Type
and Prag_Nam in Name_Part_Of
| Name_Depends
@ -859,6 +860,7 @@ package body Contracts is
AW_Val : Boolean := False;
ER_Val : Boolean := False;
EW_Val : Boolean := False;
NC_Val : Boolean;
Seen : Boolean := False;
Prag : Node_Id;
Obj_Typ : Entity_Id;
@ -956,18 +958,25 @@ package body Contracts is
end if;
-- Verify the mutual interaction of the various external properties.
-- For variables for which No_Caching is enabled, it has been checked
-- already that only False values for other external properties are
-- allowed.
-- For types and variables for which No_Caching is enabled, it has been
-- checked already that only False values for other external properties
-- are allowed.
if Seen
and then (Ekind (Type_Or_Obj_Id) /= E_Variable
or else not No_Caching_Enabled (Type_Or_Obj_Id))
and then not No_Caching_Enabled (Type_Or_Obj_Id)
then
Check_External_Properties
(Type_Or_Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
end if;
-- Analyze the non-external volatility property No_Caching
Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_No_Caching);
if Present (Prag) then
Analyze_External_Property_In_Decl_Part (Prag, NC_Val);
end if;
-- The following checks are relevant only when SPARK_Mode is on, as
-- they are not standard Ada legality rules. Internally generated
-- temporaries are ignored, as well as return objects.
@ -1047,10 +1056,10 @@ package body Contracts is
if Is_Type_Id
and then not Is_Effectively_Volatile (Type_Or_Obj_Id)
and then Has_Volatile_Component (Type_Or_Obj_Id)
and then Has_Effectively_Volatile_Component (Type_Or_Obj_Id)
then
Error_Msg_N
("non-volatile type & cannot have volatile"
("non-volatile type & cannot have effectively volatile"
& " components",
Type_Or_Obj_Id);
end if;
@ -1076,7 +1085,6 @@ package body Contracts is
Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
-- Save the SPARK_Mode-related data to restore on exit
NC_Val : Boolean;
Items : Node_Id;
Prag : Node_Id;
Ref_Elmt : Elmt_Id;
@ -1118,14 +1126,6 @@ package body Contracts is
Check_Type_Or_Object_External_Properties (Type_Or_Obj_Id => Obj_Id);
-- Analyze the non-external volatility property No_Caching
Prag := Get_Pragma (Obj_Id, Pragma_No_Caching);
if Present (Prag) then
Analyze_External_Property_In_Decl_Part (Prag, NC_Val);
end if;
-- Constant-related checks
if Ekind (Obj_Id) = E_Constant then

47
gcc/ada/sem_prag.adb
View file

@ -2116,9 +2116,16 @@ package body Sem_Prag is
First (Pragma_Argument_Associations (N));
Obj_Decl : constant Node_Id := Find_Related_Context (N);
Obj_Id : constant Entity_Id := Defining_Entity (Obj_Decl);
Obj_Typ : Entity_Id;
Expr : Node_Id;
begin
if Is_Type (Obj_Id) then
Obj_Typ := Obj_Id;
else
Obj_Typ := Etype (Obj_Id);
end if;
-- Ensure that the Boolean expression (if present) is static. A missing
-- argument defaults the value to True (SPARK RM 7.1.2(5)).
@ -2153,9 +2160,7 @@ package body Sem_Prag is
if Prag_Id /= Pragma_No_Caching
and then not Is_Effectively_Volatile (Obj_Id)
then
if Ekind (Obj_Id) = E_Variable
and then No_Caching_Enabled (Obj_Id)
then
if No_Caching_Enabled (Obj_Id) then
if Expr_Val then -- Confirming value of False is allowed
SPARK_Msg_N
("illegal combination of external property % and property "
@ -2167,15 +2172,16 @@ package body Sem_Prag is
N);
end if;
-- Pragma No_Caching should only apply to volatile variables of
-- Pragma No_Caching should only apply to volatile types or variables of
-- a non-effectively volatile type (SPARK RM 7.1.2).
elsif Prag_Id = Pragma_No_Caching then
if Is_Effectively_Volatile (Etype (Obj_Id)) then
SPARK_Msg_N ("property % must not apply to an object of "
if Is_Effectively_Volatile (Obj_Typ) then
SPARK_Msg_N ("property % must not apply to a type or object of "
& "an effectively volatile type", N);
elsif not Is_Volatile (Obj_Id) then
SPARK_Msg_N ("property % must apply to a volatile object", N);
SPARK_Msg_N
("property % must apply to a volatile type or object", N);
end if;
end if;
@ -13484,22 +13490,19 @@ package body Sem_Prag is
Obj_Or_Type_Decl := Find_Related_Context (N, Do_Checks => True);
-- Pragma must apply to a object declaration or to a type
-- declaration (only the former in the No_Caching case).
-- Original_Node is necessary to account for untagged derived
-- types that are rewritten as subtypes of their
-- respective root types.
-- declaration. Original_Node is necessary to account for
-- untagged derived types that are rewritten as subtypes of
-- their respective root types.
if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration then
if Prag_Id = Pragma_No_Caching
or else Nkind (Original_Node (Obj_Or_Type_Decl)) not in
N_Full_Type_Declaration |
N_Private_Type_Declaration |
N_Formal_Type_Declaration |
N_Task_Type_Declaration |
N_Protected_Type_Declaration
then
Pragma_Misplaced;
end if;
if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration
and then Nkind (Original_Node (Obj_Or_Type_Decl)) not in
N_Full_Type_Declaration |
N_Private_Type_Declaration |
N_Formal_Type_Declaration |
N_Task_Type_Declaration |
N_Protected_Type_Declaration
then
Pragma_Misplaced;
end if;
Obj_Or_Type_Id := Defining_Entity (Obj_Or_Type_Decl);

37
gcc/ada/sem_util.adb
View file

@ -13530,6 +13530,36 @@ package body Sem_Util is
return Has_Undef_Ref;
end Has_Undefined_Reference;
----------------------------------------
-- Has_Effectively_Volatile_Component --
----------------------------------------
function Has_Effectively_Volatile_Component
(Typ : Entity_Id) return Boolean
is
Comp : Entity_Id;
begin
if Has_Volatile_Components (Typ) then
return True;
elsif Is_Array_Type (Typ) then
return Is_Effectively_Volatile (Component_Type (Typ));
elsif Is_Record_Type (Typ) then
Comp := First_Component (Typ);
while Present (Comp) loop
if Is_Effectively_Volatile (Etype (Comp)) then
return True;
end if;
Next_Component (Comp);
end loop;
end if;
return False;
end Has_Effectively_Volatile_Component;
----------------------------
-- Has_Volatile_Component --
----------------------------
@ -16663,9 +16693,11 @@ package body Sem_Util is
if Is_Type (Id) then
-- An arbitrary type is effectively volatile when it is subject to
-- pragma Atomic or Volatile.
-- pragma Atomic or Volatile, unless No_Caching is enabled.
if Is_Volatile (Id) then
if Is_Volatile (Id)
and then not No_Caching_Enabled (Id)
then
return True;
-- An array type is effectively volatile when it is subject to pragma
@ -24579,7 +24611,6 @@ package body Sem_Util is
------------------------
function No_Caching_Enabled (Id : Entity_Id) return Boolean is
pragma Assert (Ekind (Id) = E_Variable);
Prag : constant Node_Id := Get_Pragma (Id, Pragma_No_Caching);
Arg1 : Node_Id;

11
gcc/ada/sem_util.ads
View file

@ -1564,6 +1564,11 @@ package Sem_Util is
-- Given arbitrary expression Expr, determine whether it contains at
-- least one name whose entity is Any_Id.
function Has_Effectively_Volatile_Component
(Typ : Entity_Id) return Boolean;
-- Given arbitrary type Typ, determine whether it contains at least one
-- effectively volatile component.
function Has_Volatile_Component (Typ : Entity_Id) return Boolean;
-- Given arbitrary type Typ, determine whether it contains at least one
-- volatile component.
@ -2758,9 +2763,9 @@ package Sem_Util is
-- inline this procedural form, but not the functional form above.
function No_Caching_Enabled (Id : Entity_Id) return Boolean;
-- Given the entity of a variable, determine whether Id is subject to
-- volatility property No_Caching and if it is, the related expression
-- evaluates to True.
-- Given any entity Id, determine whether Id is subject to volatility
-- property No_Caching and if it is, the related expression evaluates
-- to True.
function No_Heap_Finalization (Typ : Entity_Id) return Boolean;
-- Determine whether type Typ is subject to pragma No_Heap_Finalization