mirror of
git://gcc.gnu.org/git/gcc.git
synced 2025-03-21 19:41:29 +08:00
[Ada] Expose part of ownership checking for use in GNATprove
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. 2019-08-14 Yannick Moy <moy@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. From-SVN: r274454
This commit is contained in:
Yannick Moy
Pierre-Marie de Rodat
parent
05b77088c0
commit
1384d88fa9
@ -1,3 +1,16 @@
|
||||
2019-08-14 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* 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.
|
||||
|
||||
2019-08-14 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* sem_spark.adb (Check_Old_Loop_Entry): New procedure to check
|
||||
|
||||
@ -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,35 +1443,6 @@ package body Sem_SPARK is
|
||||
when N_Object_Declaration =>
|
||||
Expr := Expression (Decl);
|
||||
|
||||
Check_Type (Target_Typ);
|
||||
|
||||
-- A declaration of a stand-alone object of an anonymous access
|
||||
-- type shall have an explicit initial value and shall occur
|
||||
-- immediately within a subprogram body, an entry body, or a
|
||||
-- block statement (SPARK RM 3.10(4)).
|
||||
|
||||
if Is_Anonymous_Access_Type (Target_Typ) then
|
||||
declare
|
||||
Scop : constant Entity_Id := Scope (Target);
|
||||
begin
|
||||
if not Is_Local_Context (Scop) then
|
||||
if Emit_Messages then
|
||||
Error_Msg_N
|
||||
("object of anonymous access type must be declared "
|
||||
& "immediately within a subprogram, entry or block "
|
||||
& "(SPARK RM 3.10(4))", Decl);
|
||||
end if;
|
||||
end if;
|
||||
end;
|
||||
|
||||
if No (Expr) then
|
||||
if Emit_Messages then
|
||||
Error_Msg_N ("object of anonymous access type must be "
|
||||
& "initialized (SPARK RM 3.10(4))", Decl);
|
||||
end if;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
if Present (Expr) then
|
||||
Check_Assignment (Target => Target,
|
||||
Expr => Expr);
|
||||
@ -1506,6 +1496,113 @@ package body Sem_SPARK is
|
||||
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
|
||||
-- immediately within a subprogram body, an entry body, or a
|
||||
-- block statement (SPARK RM 3.10(4)).
|
||||
|
||||
if Is_Anonymous_Access_Type (Target_Typ) then
|
||||
declare
|
||||
Scop : constant Entity_Id := Scope (Target);
|
||||
begin
|
||||
if not Is_Local_Context (Scop) then
|
||||
if Emit_Messages then
|
||||
Error_Msg_N
|
||||
("object of anonymous access type must be declared "
|
||||
& "immediately within a subprogram, entry or block "
|
||||
& "(SPARK RM 3.10(4))", Decl);
|
||||
end if;
|
||||
end if;
|
||||
end;
|
||||
|
||||
if No (Expr) then
|
||||
if Emit_Messages then
|
||||
Error_Msg_N ("object of anonymous access type must be "
|
||||
& "initialized (SPARK RM 3.10(4))", Decl);
|
||||
end if;
|
||||
end if;
|
||||
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_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 --
|
||||
----------------------
|
||||
|
||||
@ -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.
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user