Skip to content

R
riscv-gcc-1
Commit a2119175 by Yannick Moy Committed by Pierre-Marie de Rodat
Options

[Ada] Adapt ownership checking in SPARK to traversal functions 

A traversal function, especially when implemented as an expression
function, may need to return an if-expression or case-expression, while
still respecting Legality Rule SPARK RM 3.10(5). This case is now
allowed in GNATprove.

There is no impact on compilation.

2019-07-22  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_spark.adb (Get_Root_Object, Is_Path_Expression,
	Is_Subpath_Expression): Add parameter Is_Traversal to adapt
	these functions to the case of paths returned from a traversal
	function.
	(Read_Indexes): Handle the case of an if-expression or
	case-expression.
	(Check_Statement): Check Emit_Messages only when issuing an
	error message. This is important as Emit_Messages may store the
	information that an error was detected.

From-SVN: r273693
parent 8113b0c7
Showing with 217 additions and 18 deletions
gcc/ada/ChangeLog
2019-07-22 Yannick Moy <moy@adacore.com>
* sem_spark.adb (Get_Root_Object, Is_Path_Expression,
Is_Subpath_Expression): Add parameter Is_Traversal to adapt
these functions to the case of paths returned from a traversal
function.
(Read_Indexes): Handle the case of an if-expression or
case-expression.
(Check_Statement): Check Emit_Messages only when issuing an
error message. This is important as Emit_Messages may store the
information that an error was detected.
2019-07-22 Eric Botcazou <ebotcazou@adacore.com>
* checks.adb (Apply_Type_Conversion_Checks): Do not set
......
gcc/ada/sem_spark.adb
......@@ -715,10 +715,14 @@ package body Sem_SPARK is
function Get_Root_Object
(Expr : Node_Id;
Through_Traversal : Boolean := True) return Entity_Id;
Through_Traversal : Boolean := True;
Is_Traversal : Boolean := False) return Entity_Id;
-- Return the root of the path expression Expr, or Empty for an allocator,
-- NULL, or a function call. Through_Traversal is True if it should follow
-- through calls to traversal functions.
-- through calls to traversal functions. Is_Traversal is True if this
-- corresponds to a value returned from a traversal function, which should
-- allow if-expressions and case-expressions that refer to the same root,
-- even if the paths are not the same in all branches.
generic
with procedure Handle_Parameter_Or_Global
......@@ -745,11 +749,19 @@ package body Sem_SPARK is
-- A procedure that is called when deep globals or aliased globals are used
-- without any global aspect.
function Is_Path_Expression (Expr : Node_Id) return Boolean;
-- Return whether Expr corresponds to a path
function Is_Path_Expression
(Expr : Node_Id;
Is_Traversal : Boolean := False) return Boolean;
-- Return whether Expr corresponds to a path. Is_Traversal is True if this
-- corresponds to a value returned from a traversal function, which should
-- allow if-expressions and case-expressions.
function Is_Subpath_Expression (Expr : Node_Id) return Boolean;
-- Return True if Expr can be part of a path expression
function Is_Subpath_Expression
(Expr : Node_Id;
Is_Traversal : Boolean := False) return Boolean;
-- Return True if Expr can be part of a path expression. Is_Traversal is
-- True if this corresponds to a value returned from a traversal function,
-- which should allow if-expressions and case-expressions.
function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean;
-- Determine if the candidate Prefix is indeed a prefix of Expr, or almost
......@@ -1749,6 +1761,31 @@ package body Sem_SPARK is
end loop;
end;
when N_If_Expression =>
declare
Cond : constant Node_Id := First (Expressions (Expr));
Then_Part : constant Node_Id := Next (Cond);
Else_Part : constant Node_Id := Next (Then_Part);
begin
Read_Expression (Cond);
Read_Indexes (Then_Part);
Read_Indexes (Else_Part);
end;
when N_Case_Expression =>
declare
Cases : constant List_Id := Alternatives (Expr);
Cur_Case : Node_Id := First (Cases);
begin
Read_Expression (Expression (Expr));
while Present (Cur_Case) loop
Read_Indexes (Expression (Cur_Case));
Next (Cur_Case);
end loop;
end;
when N_Attribute_Reference =>
pragma Assert
(Get_Attribute_Id (Attribute_Name (Expr)) =
......@@ -3115,14 +3152,14 @@ package body Sem_SPARK is
if Is_Anonymous_Access_Type (Return_Typ) then
pragma Assert (Is_Traversal_Function (Subp));
if Nkind (Expr) /= N_Null and then Emit_Messages then
if Nkind (Expr) /= N_Null then
declare
Expr_Root : constant Entity_Id :=
Get_Root_Object (Expr);
Get_Root_Object (Expr, Is_Traversal => True);
Param : constant Entity_Id :=
First_Formal (Subp);
begin
if Param /= Expr_Root then
if Param /= Expr_Root and then Emit_Messages then
Error_Msg_NE
("returned value must be rooted in "
& "traversed parameter & "
......@@ -3642,10 +3679,31 @@ package body Sem_SPARK is
function Get_Root_Object
(Expr : Node_Id;
Through_Traversal : Boolean := True) return Entity_Id
Through_Traversal : Boolean := True;
Is_Traversal : Boolean := False) return Entity_Id
is
function GRO (Expr : Node_Id) return Entity_Id;
-- Local wrapper on the actual function, to propagate the values of
-- optional parameters.
---------
-- GRO --
---------
function GRO (Expr : Node_Id) return Entity_Id is
begin
return Get_Root_Object (Expr, Through_Traversal, Is_Traversal);
end GRO;
Get_Root_Object : Boolean;
pragma Unmodified (Get_Root_Object);
-- Local variable to mask the name of function Get_Root_Object, to
-- prevent direct call. Instead GRO wrapper should be called.
-- Start of processing for Get_Root_Object
begin
if not Is_Subpath_Expression (Expr) then
if not Is_Subpath_Expression (Expr, Is_Traversal) then
if Emit_Messages then
Error_Msg_N ("name expected here for path", Expr);
end if;
......@@ -3663,7 +3721,7 @@ package body Sem_SPARK is
| N_Selected_Component
| N_Slice
=>
return Get_Root_Object (Prefix (Expr), Through_Traversal);
return GRO (Prefix (Expr));
-- There is no root object for an (extension) aggregate, allocator,
-- concat, or NULL.
......@@ -3684,7 +3742,7 @@ package body Sem_SPARK is
if Through_Traversal
and then Is_Traversal_Function_Call (Expr)
then
return Get_Root_Object (First_Actual (Expr), Through_Traversal);
return GRO (First_Actual (Expr));
else
return Empty;
end if;
......@@ -3693,7 +3751,7 @@ package body Sem_SPARK is
| N_Type_Conversion
| N_Unchecked_Type_Conversion
=>
return Get_Root_Object (Expression (Expr), Through_Traversal);
return GRO (Expression (Expr));
when N_Attribute_Reference =>
pragma Assert
......@@ -3706,6 +3764,69 @@ package body Sem_SPARK is
Attribute_Image);
return Empty;
when N_If_Expression =>
if Is_Traversal then
declare
Cond : constant Node_Id := First (Expressions (Expr));
Then_Part : constant Node_Id := Next (Cond);
Else_Part : constant Node_Id := Next (Then_Part);
Then_Root : constant Entity_Id := GRO (Then_Part);
Else_Root : constant Entity_Id := GRO (Else_Part);
begin
if Nkind (Then_Part) = N_Null then
return Else_Root;
elsif Nkind (Else_Part) = N_Null then
return Then_Part;
elsif Then_Root = Else_Root then
return Then_Root;
else
if Emit_Messages then
Error_Msg_N
("same name expected here in each branch", Expr);
end if;
return Empty;
end if;
end;
else
if Emit_Messages then
Error_Msg_N ("name expected here for path", Expr);
end if;
return Empty;
end if;
when N_Case_Expression =>
if Is_Traversal then
declare
Cases : constant List_Id := Alternatives (Expr);
Cur_Case : Node_Id := First (Cases);
Cur_Root : Entity_Id;
Common_Root : Entity_Id := Empty;
begin
while Present (Cur_Case) loop
Cur_Root := GRO (Expression (Cur_Case));
if Common_Root = Empty then
Common_Root := Cur_Root;
elsif Common_Root /= Cur_Root then
if Emit_Messages then
Error_Msg_N
("same name expected here in each branch", Expr);
end if;
return Empty;
end if;
Next (Cur_Case);
end loop;
return Common_Root;
end;
else
if Emit_Messages then
Error_Msg_N ("name expected here for path", Expr);
end if;
return Empty;
end if;
when others =>
raise Program_Error;
end case;
......@@ -3876,7 +3997,30 @@ package body Sem_SPARK is
-- Is_Path_Expression --
------------------------
function Is_Path_Expression (Expr : Node_Id) return Boolean is
function Is_Path_Expression
(Expr : Node_Id;
Is_Traversal : Boolean := False) return Boolean
is
function IPE (Expr : Node_Id) return Boolean;
-- Local wrapper on the actual function, to propagate the values of
-- optional parameter Is_Traversal.
---------
-- IPE --
---------
function IPE (Expr : Node_Id) return Boolean is
begin
return Is_Path_Expression (Expr, Is_Traversal);
end IPE;
Is_Path_Expression : Boolean;
pragma Unmodified (Is_Path_Expression);
-- Local variable to mask the name of function Is_Path_Expression, to
-- prevent direct call. Instead IPE wrapper should be called.
-- Start of processing for Is_Path_Expression
begin
case Nkind (Expr) is
when N_Expanded_Name
......@@ -3907,7 +4051,47 @@ package body Sem_SPARK is
| N_Type_Conversion
| N_Unchecked_Type_Conversion
=>
return Is_Path_Expression (Expression (Expr));
return IPE (Expression (Expr));
-- When returning from a traversal function, consider an
-- if-expression as a possible path expression.
when N_If_Expression =>
if Is_Traversal then
declare
Cond : constant Node_Id := First (Expressions (Expr));
Then_Part : constant Node_Id := Next (Cond);
Else_Part : constant Node_Id := Next (Then_Part);
begin
return IPE (Then_Part)
and then IPE (Else_Part);
end;
else
return False;
end if;
-- When returning from a traversal function, consider
-- a case-expression as a possible path expression.
when N_Case_Expression =>
if Is_Traversal then
declare
Cases : constant List_Id := Alternatives (Expr);
Cur_Case : Node_Id := First (Cases);
begin
while Present (Cur_Case) loop
if not IPE (Expression (Cur_Case)) then
return False;
end if;
Next (Cur_Case);
end loop;
return True;
end;
else
return False;
end if;
when others =>
return False;
......@@ -4033,9 +4217,12 @@ package body Sem_SPARK is
-- Is_Subpath_Expression --
---------------------------
function Is_Subpath_Expression (Expr : Node_Id) return Boolean is
function Is_Subpath_Expression
(Expr : Node_Id;
Is_Traversal : Boolean := False) return Boolean
is
begin
return Is_Path_Expression (Expr)
return Is_Path_Expression (Expr, Is_Traversal)
or else (Nkind (Expr) = N_Attribute_Reference
and then
(Get_Attribute_Id (Attribute_Name (Expr)) =
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment