GNATprove needs to be able to call a subset of the ownership legality
rules from marking. This is provided by a new function
Sem_SPARK.Is_Legal.
There is no impact on compilation.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-08-14 Yannick Moy <m...@adacore.com>
gcc/ada/
* sem_spark.adb, sem_spark.ads (Is_Legal): New function exposed
for use in GNATprove, to test legality rules not related to
permissions.
(Check_Declaration_Legality): Extract the part of
Check_Declaration that checks rules not related to permissions.
(Check_Declaration): Call the new Check_Declaration_Legality.
(Check_Type_Legality): Rename of Check_Type. Introduce
parameters to force or not checking, and update a flag detecting
illegalities.
(Check_Node): Ignore attribute references in statement position.--- gcc/ada/sem_spark.adb
+++ gcc/ada/sem_spark.adb
@@ -637,6 +637,14 @@ package body Sem_SPARK is
procedure Check_Declaration (Decl : Node_Id);
+ procedure Check_Declaration_Legality
+ (Decl : Node_Id;
+ Force : Boolean;
+ Legal : in out Boolean);
+ -- Check the legality of declaration Decl regarding rules not related to
+ -- permissions. Update Legal to False if a rule is violated. Issue an
+ -- error message if Force is True and Emit_Messages returns True.
+
procedure Check_Expression (Expr : Node_Id; Mode : Extended_Checking_Mode);
pragma Precondition (Nkind_In (Expr, N_Index_Or_Discriminant_Constraint,
N_Range_Constraint,
@@ -686,7 +694,10 @@ package body Sem_SPARK is
procedure Check_Statement (Stmt : Node_Id);
- procedure Check_Type (Typ : Entity_Id);
+ procedure Check_Type_Legality
+ (Typ : Entity_Id;
+ Force : Boolean;
+ Legal : in out Boolean);
-- Check that type Typ is either not deep, or that it is an observing or
-- owning type according to SPARK RM 3.10
@@ -1138,11 +1149,12 @@ package body Sem_SPARK is
Expr_Root : Entity_Id;
Perm : Perm_Kind;
Status : Error_Status;
+ Dummy : Boolean := True;
-- Start of processing for Check_Assignment
begin
- Check_Type (Target_Typ);
+ Check_Type_Legality (Target_Typ, Force => True, Legal => Dummy);
if Is_Anonymous_Access_Type (Target_Typ) then
Check_Source_Of_Borrow_Or_Observe (Expr, Status);
@@ -1410,11 +1422,18 @@ package body Sem_SPARK is
Target : constant Entity_Id := Defining_Identifier (Decl);
Target_Typ : constant Node_Id := Etype (Target);
Expr : Node_Id;
+ Dummy : Boolean := True;
begin
+ -- Start with legality rules not related to permissions
+
+ Check_Declaration_Legality (Decl, Force => True, Legal => Dummy);
+
+ -- Now check permission-related legality rules
+
case N_Declaration'(Nkind (Decl)) is
when N_Full_Type_Declaration =>
- Check_Type (Target);
+ null;
-- ??? What about component declarations with defaults.
@@ -1424,7 +1443,105 @@ package body Sem_SPARK is
when N_Object_Declaration =>
Expr := Expression (Decl);
- Check_Type (Target_Typ);
+ if Present (Expr) then
+ Check_Assignment (Target => Target,
+ Expr => Expr);
+ end if;
+
+ if Is_Deep (Target_Typ) then
+ declare
+ Tree : constant Perm_Tree_Access :=
+ new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => True,
+ Explanation => Decl,
+ Permission => Read_Write,
+ Children_Permission => Read_Write));
+ begin
+ Set (Current_Perm_Env, Target, Tree);
+ end;
+ end if;
+
+ when N_Iterator_Specification =>
+ null;
+
+ when N_Loop_Parameter_Specification =>
+ null;
+
+ -- Checking should not be called directly on these nodes
+
+ when N_Function_Specification
+ | N_Entry_Declaration
+ | N_Procedure_Specification
+ | N_Component_Declaration
+ =>
+ raise Program_Error;
+
+ -- Ignored constructs for pointer checking
+
+ when N_Formal_Object_Declaration
+ | N_Formal_Type_Declaration
+ | N_Incomplete_Type_Declaration
+ | N_Private_Extension_Declaration
+ | N_Private_Type_Declaration
+ | N_Protected_Type_Declaration
+ =>
+ null;
+
+ -- The following nodes are rewritten by semantic analysis
+
+ when N_Expression_Function =>
+ raise Program_Error;
+ end case;
+ end Check_Declaration;
+
+ --------------------------------
+ -- Check_Declaration_Legality --
+ --------------------------------
+
+ procedure Check_Declaration_Legality
+ (Decl : Node_Id;
+ Force : Boolean;
+ Legal : in out Boolean)
+ is
+ function Original_Emit_Messages return Boolean renames Emit_Messages;
+
+ function Emit_Messages return Boolean;
+ -- Local wrapper around generic formal parameter Emit_Messages, to
+ -- check the value of parameter Force before calling the original
+ -- Emit_Messages, and setting Legal to False.
+
+ -------------------
+ -- Emit_Messages --
+ -------------------
+
+ function Emit_Messages return Boolean is
+ begin
+ Legal := False;
+ return Force and then Original_Emit_Messages;
+ end Emit_Messages;
+
+ -- Local variables
+
+ Target : constant Entity_Id := Defining_Identifier (Decl);
+ Target_Typ : constant Node_Id := Etype (Target);
+ Expr : Node_Id;
+
+ -- Start of processing for Check_Declaration_Legality
+
+ begin
+ case N_Declaration'(Nkind (Decl)) is
+ when N_Full_Type_Declaration =>
+ Check_Type_Legality (Target, Force, Legal);
+
+ when N_Subtype_Declaration =>
+ null;
+
+ when N_Object_Declaration =>
+ Expr := Expression (Decl);
+
+ Check_Type_Legality (Target_Typ, Force, Legal);
-- A declaration of a stand-alone object of an anonymous access
-- type shall have an explicit initial value and shall occur
@@ -1453,26 +1570,6 @@ package body Sem_SPARK is
end if;
end if;
- if Present (Expr) then
- Check_Assignment (Target => Target,
- Expr => Expr);
- end if;
-
- if Is_Deep (Target_Typ) then
- declare
- Tree : constant Perm_Tree_Access :=
- new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => True,
- Explanation => Decl,
- Permission => Read_Write,
- Children_Permission => Read_Write));
- begin
- Set (Current_Perm_Env, Target, Tree);
- end;
- end if;
-
when N_Iterator_Specification =>
null;
@@ -1504,7 +1601,7 @@ package body Sem_SPARK is
when N_Expression_Function =>
raise Program_Error;
end case;
- end Check_Declaration;
+ end Check_Declaration_Legality;
----------------------
-- Check_Expression --
@@ -2668,6 +2765,12 @@ package body Sem_SPARK is
when N_Subprogram_Declaration =>
Check_Subprogram_Contract (N);
+ -- Attribute references in statement position are not supported in
+ -- SPARK and will be rejected by GNATprove.
+
+ when N_Attribute_Reference =>
+ null;
+
-- Ignored constructs for pointer checking
when N_Abstract_Subprogram_Declaration
@@ -3503,13 +3606,38 @@ package body Sem_SPARK is
end case;
end Check_Statement;
- ----------------
- -- Check_Type --
- ----------------
+ -------------------------
+ -- Check_Type_Legality --
+ -------------------------
+
+ procedure Check_Type_Legality
+ (Typ : Entity_Id;
+ Force : Boolean;
+ Legal : in out Boolean)
+ is
+ function Original_Emit_Messages return Boolean renames Emit_Messages;
+
+ function Emit_Messages return Boolean;
+ -- Local wrapper around generic formal parameter Emit_Messages, to
+ -- check the value of parameter Force before calling the original
+ -- Emit_Messages, and setting Legal to False.
+
+ -------------------
+ -- Emit_Messages --
+ -------------------
+
+ function Emit_Messages return Boolean is
+ begin
+ Legal := False;
+ return Force and then Original_Emit_Messages;
+ end Emit_Messages;
+
+ -- Local variables
- procedure Check_Type (Typ : Entity_Id) is
Check_Typ : constant Entity_Id := Retysp (Typ);
+ -- Start of processing for Check_Type_Legality
+
begin
case Type_Kind'(Ekind (Check_Typ)) is
when Access_Kind =>
@@ -3519,7 +3647,7 @@ package body Sem_SPARK is
=>
null;
when E_Access_Subtype =>
- Check_Type (Base_Type (Check_Typ));
+ Check_Type_Legality (Base_Type (Check_Typ), Force, Legal);
when E_Access_Attribute_Type =>
if Emit_Messages then
Error_Msg_N ("access attribute not allowed in SPARK",
@@ -3546,7 +3674,7 @@ package body Sem_SPARK is
when E_Array_Type
| E_Array_Subtype
=>
- Check_Type (Component_Type (Check_Typ));
+ Check_Type_Legality (Component_Type (Check_Typ), Force, Legal);
when Record_Kind =>
if Is_Deep (Check_Typ)
@@ -3569,7 +3697,7 @@ package body Sem_SPARK is
-- Ignore components which are not visible in SPARK
if Component_Is_Visible_In_SPARK (Comp) then
- Check_Type (Etype (Comp));
+ Check_Type_Legality (Etype (Comp), Force, Legal);
end if;
Next_Component_Or_Discriminant (Comp);
end loop;
@@ -3595,7 +3723,7 @@ package body Sem_SPARK is
=>
null;
end case;
- end Check_Type;
+ end Check_Type_Legality;
--------------
-- Get_Expl --
@@ -4141,6 +4269,24 @@ package body Sem_SPARK is
end case;
end Is_Deep;
+ --------------
+ -- Is_Legal --
+ --------------
+
+ function Is_Legal (N : Node_Id) return Boolean is
+ Legal : Boolean := True;
+
+ begin
+ case Nkind (N) is
+ when N_Declaration =>
+ Check_Declaration_Legality (N, Force => False, Legal => Legal);
+ when others =>
+ null;
+ end case;
+
+ return Legal;
+ end Is_Legal;
+
----------------------
-- Is_Local_Context --
----------------------
--- gcc/ada/sem_spark.ads
+++ gcc/ada/sem_spark.ads
@@ -152,6 +152,12 @@ generic
package Sem_SPARK is
+ function Is_Legal (N : Node_Id) return Boolean;
+ -- Test the legality of a node wrt ownership-checking rules. This does not
+ -- check rules related to the validity of permissions associated with paths
+ -- from objects, so that it can be called from GNATprove on code of library
+ -- units analyzed in SPARK_Mode Auto.
+
procedure Check_Safe_Pointers (N : Node_Id);
-- The entry point of this package. It analyzes a node and reports errors
-- when there are violations of ownership rules.
