Commit 60a38ae1 by Hristian Kirtchev Committed by Pierre-Marie de Rodat

[Ada] Failure to detect trivial infinite recursion

This patch reimplements the detection of trivial infinite recursion to
remove the implicit assumptions concenring the structure and contents of
the enclosing subprogram statements.

------------
-- Source --
------------

--  infinite.adb

procedure Infinite with SPARK_Mode is
   function Func_1 (Val : Integer) return Integer;
   function Func_2 (Val : Integer) return Integer;
   function Func_3 (Val : Integer) return Integer;
   function Func_4 (Val : Integer) return Integer;
   function Func_5 (Val : Integer) return Integer;
   function Func_6 (Val : Integer) return Integer;
   function Func_7 (Val : Integer) return Integer;
   function Func_8 (Val_1 : Integer; Val_2 : Integer) return Integer;
   procedure Proc_1 (Val : Integer);

   function Func_1 (Val : Integer) return Integer is
   begin
      return Func_1 (Val);                                           --  WARN
   end Func_1;

   function Func_2 (Val : Integer) return Integer is
   begin
      return Func_2 (123);                                           --  none
   end Func_2;

   function Func_3 (Val : Integer) return Integer is
      Temp : Integer;
   begin
      Temp := Func_3 (Val);                                          --  WARN
      return Temp;
   end Func_3;

   function Func_4 (Val : Integer) return Integer is
      Temp : Integer;
   begin
      Temp := Func_4 (123);                                          --  none
      return Temp;
   end Func_4;

   function Func_5 (Val : Integer) return Integer is
   begin
      Proc_1 (Val);
      return Func_5 (Val);                                           --  none
   end Func_5;

   function Func_6 (Val : Integer) return Integer is
   begin
      Proc_1 (Val);
      return Func_6 (123);                                           --  none
   end Func_6;

   function Func_7 (Val : Integer) return Integer is
   begin
      raise Program_Error;
      return Func_7 (Val);                                           --  none
   end Func_7;

   function Func_8 (Val_1 : Integer; Val_2 : Integer) return Integer is
   begin
      return Func_8 (Val_1, 123);                                    --  none
   end Func_8;

   procedure Proc_1 (Val : Integer) is
   begin
      Proc_1 (Val);                                                  --  WARN
   end Proc_1;

begin null; end Infinite;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c infinite.adb
infinite.adb:14:14: infinite recursion
infinite.adb:14:14: Storage_Error would have been raised at run time
infinite.adb:25:15: infinite recursion
infinite.adb:25:15: Storage_Error would have been raised at run time
infinite.adb:61:07: infinite recursion
infinite.adb:61:07: Storage_Error would have been raised at run time

2019-07-05  Hristian Kirtchev  <kirtchev@adacore.com>

gcc/ada/

	* sem_res.adb (Check_Infinite_Recursion): Reimplemented.
	(Enclosing_Declaration_Or_Statement,
	Invoked_With_Different_Arguments, Is_Conditional_Statement,
	Is_Control_Flow_Statement, Is_Immediately_Within_Body,
	Is_Raise_Idiom, Is_Raise_Statement, Is_Sole_Statement,
	Preceded_By_Control_Flow_Statement,
	Within_Conditional_Statement): New routines.

From-SVN: r273116
parent 43fa58c2
2019-07-05 Hristian Kirtchev <kirtchev@adacore.com>
* sem_res.adb (Check_Infinite_Recursion): Reimplemented.
(Enclosing_Declaration_Or_Statement,
Invoked_With_Different_Arguments, Is_Conditional_Statement,
Is_Control_Flow_Statement, Is_Immediately_Within_Body,
Is_Raise_Idiom, Is_Raise_Statement, Is_Sole_Statement,
Preceded_By_Control_Flow_Statement,
Within_Conditional_Statement): New routines.
2019-07-05 Javier Miranda <miranda@adacore.com> 2019-07-05 Javier Miranda <miranda@adacore.com>
* exp_ch4.adb (Expand_N_Type_Conversion): Do not apply an * exp_ch4.adb (Expand_N_Type_Conversion): Do not apply an
......
...@@ -111,8 +111,8 @@ package body Sem_Res is ...@@ -111,8 +111,8 @@ package body Sem_Res is
Pref : Node_Id); Pref : Node_Id);
-- Check that the type of the prefix of a dereference is not incomplete -- Check that the type of the prefix of a dereference is not incomplete
function Check_Infinite_Recursion (N : Node_Id) return Boolean; function Check_Infinite_Recursion (Call : Node_Id) return Boolean;
-- Given a call node, N, which is known to occur immediately within the -- Given a call node, Call, which is known to occur immediately within the
-- subprogram being called, determines whether it is a detectable case of -- subprogram being called, determines whether it is a detectable case of
-- an infinite recursion, and if so, outputs appropriate messages. Returns -- an infinite recursion, and if so, outputs appropriate messages. Returns
-- True if an infinite recursion is detected, and False otherwise. -- True if an infinite recursion is detected, and False otherwise.
...@@ -695,164 +695,406 @@ package body Sem_Res is ...@@ -695,164 +695,406 @@ package body Sem_Res is
-- Check_Infinite_Recursion -- -- Check_Infinite_Recursion --
------------------------------ ------------------------------
function Check_Infinite_Recursion (N : Node_Id) return Boolean is function Check_Infinite_Recursion (Call : Node_Id) return Boolean is
P : Node_Id; function Enclosing_Declaration_Or_Statement (N : Node_Id) return Node_Id;
C : Node_Id; -- Return the nearest enclosing declaration or statement that houses
-- arbitrary node N.
function Same_Argument_List return Boolean; function Invoked_With_Different_Arguments (N : Node_Id) return Boolean;
-- Check whether list of actuals is identical to list of formals of -- Determine whether call N invokes the related enclosing subprogram
-- called function (which is also the enclosing scope). -- with actuals that differ from the subprogram's formals.
------------------------ function Is_Conditional_Statement (N : Node_Id) return Boolean;
-- Same_Argument_List -- -- Determine whether arbitrary node N denotes a conditional construct
------------------------
function Is_Control_Flow_Statement (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N denotes a control flow statement
-- or a construct that may contains such a statement.
function Is_Immediately_Within_Body (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N appears immediately within the
-- statements of an entry or subprogram body.
function Is_Raise_Idiom (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N appears immediately within the
-- body of an entry or subprogram, and is preceded by a single raise
-- statement.
function Same_Argument_List return Boolean is function Is_Raise_Statement (N : Node_Id) return Boolean;
A : Node_Id; -- Determine whether arbitrary node N denotes a raise statement
F : Entity_Id;
Subp : Entity_Id; function Is_Sole_Statement (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N is the sole source statement in
-- the body of the enclosing subprogram.
function Preceded_By_Control_Flow_Statement (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N is preceded by a control flow
-- statement.
function Within_Conditional_Statement (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N appears within a conditional
-- construct.
----------------------------------------
-- Enclosing_Declaration_Or_Statement --
----------------------------------------
function Enclosing_Declaration_Or_Statement
(N : Node_Id) return Node_Id
is
Par : Node_Id;
begin begin
if not Is_Entity_Name (Name (N)) then Par := N;
return False; while Present (Par) loop
else if Is_Declaration (Par) or else Is_Statement (Par) then
Subp := Entity (Name (N)); return Par;
end if;
F := First_Formal (Subp); -- Prevent the search from going too far
A := First_Actual (N);
while Present (F) and then Present (A) loop elsif Is_Body_Or_Package_Declaration (Par) then
if not Is_Entity_Name (A) or else Entity (A) /= F then exit;
return False;
end if; end if;
Next_Actual (A); Par := Parent (Par);
Next_Formal (F);
end loop; end loop;
return True; return N;
end Same_Argument_List; end Enclosing_Declaration_Or_Statement;
-- Start of processing for Check_Infinite_Recursion --------------------------------------
-- Invoked_With_Different_Arguments --
--------------------------------------
begin function Invoked_With_Different_Arguments (N : Node_Id) return Boolean is
-- Special case, if this is a procedure call and is a call to the Subp : constant Entity_Id := Entity (Name (N));
-- current procedure with the same argument list, then this is for
-- sure an infinite recursion and we insert a call to raise SE.
if Is_List_Member (N) Actual : Node_Id;
and then List_Length (List_Containing (N)) = 1 Formal : Entity_Id;
and then Same_Argument_List
then begin
declare -- Determine whether the formals of the invoked subprogram are not
P : constant Node_Id := Parent (N); -- used as actuals in the call.
begin
if Nkind (P) = N_Handled_Sequence_Of_Statements Actual := First_Actual (Call);
and then Nkind (Parent (P)) = N_Subprogram_Body Formal := First_Formal (Subp);
and then Is_Empty_List (Declarations (Parent (P))) while Present (Actual) and then Present (Formal) loop
-- The current actual does not match the current formal
if not (Is_Entity_Name (Actual)
and then Entity (Actual) = Formal)
then then
Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("!infinite recursion<<", N);
Error_Msg_N ("\!Storage_Error [<<", N);
Insert_Action (N,
Make_Raise_Storage_Error (Sloc (N),
Reason => SE_Infinite_Recursion));
return True; return True;
end if; end if;
end;
end if;
-- If not that special case, search up tree, quitting if we reach a Next_Actual (Actual);
-- construct (e.g. a conditional) that tells us that this is not a Next_Formal (Formal);
-- case for an infinite recursion warning. end loop;
C := N; return False;
loop end Invoked_With_Different_Arguments;
P := Parent (C);
-- If no parent, then we were not inside a subprogram, this can for ------------------------------
-- example happen when processing certain pragmas in a spec. Just -- Is_Conditional_Statement --
-- return False in this case. ------------------------------
if No (P) then function Is_Conditional_Statement (N : Node_Id) return Boolean is
begin
return
Nkind_In (N, N_And_Then,
N_Case_Expression,
N_Case_Statement,
N_If_Expression,
N_If_Statement,
N_Or_Else);
end Is_Conditional_Statement;
-------------------------------
-- Is_Control_Flow_Statement --
-------------------------------
function Is_Control_Flow_Statement (N : Node_Id) return Boolean is
begin
-- Delay statements do not affect the control flow because they
-- simply postpone the execution of all subsequent statements.
if Nkind (N) in N_Delay_Statement then
return False; return False;
-- Otherwise it is assumed that all other statements may affect the
-- control flow in some way. A raise statement may be expanded into
-- a non-statement node.
else
return Is_Statement (N) or else Is_Raise_Statement (N);
end if; end if;
end Is_Control_Flow_Statement;
-- Done if we get to subprogram body, this is definitely an infinite --------------------------------
-- recursion case if we did not find anything to stop us. -- Is_Immediately_Within_Body --
--------------------------------
exit when Nkind (P) = N_Subprogram_Body; function Is_Immediately_Within_Body (N : Node_Id) return Boolean is
HSS : constant Node_Id := Parent (N);
-- If appearing in conditional, result is false begin
return
Nkind (HSS) = N_Handled_Sequence_Of_Statements
and then Nkind_In (Parent (HSS), N_Entry_Body, N_Subprogram_Body)
and then Is_List_Member (N)
and then List_Containing (N) = Statements (HSS);
end Is_Immediately_Within_Body;
if Nkind_In (P, N_Or_Else, --------------------
N_And_Then, -- Is_Raise_Idiom --
N_Case_Expression, --------------------
N_Case_Statement,
N_If_Expression,
N_If_Statement)
then
return False;
elsif Nkind (P) = N_Handled_Sequence_Of_Statements function Is_Raise_Idiom (N : Node_Id) return Boolean is
and then C /= First (Statements (P)) Raise_Stmt : Node_Id;
then Stmt : Node_Id;
-- If the call is the expression of a return statement and the
-- actuals are identical to the formals, it's worth a warning.
-- However, we skip this if there is an immediately preceding
-- raise statement, since the call is never executed.
-- Furthermore, this corresponds to a common idiom: begin
if Is_Immediately_Within_Body (N) then
-- function F (L : Thing) return Boolean is -- Assume that no raise statement has been seen yet
-- begin
-- raise Program_Error;
-- return F (L);
-- end F;
-- for generating a stub function Raise_Stmt := Empty;
if Nkind (Parent (N)) = N_Simple_Return_Statement -- Examine the statements preceding the input node, skipping
and then Same_Argument_List -- internally-generated constructs.
then
exit when not Is_List_Member (Parent (N));
-- OK, return statement is in a statement list, look for raise Stmt := Prev (N);
while Present (Stmt) loop
declare -- Multiple raise statements violate the idiom
Nod : Node_Id;
begin if Is_Raise_Statement (Stmt) then
-- Skip past N_Freeze_Entity nodes generated by expansion if Present (Raise_Stmt) then
return False;
end if;
Nod := Prev (Parent (N)); Raise_Stmt := Stmt;
while Present (Nod)
and then Nkind (Nod) = N_Freeze_Entity
loop
Prev (Nod);
end loop;
-- If no raise statement, give warning. We look at the elsif Comes_From_Source (Stmt) then
-- original node, because in the case of "raise ... with exit;
-- ...", the node has been transformed into a call. end if;
exit when Nkind (Original_Node (Nod)) /= N_Raise_Statement Stmt := Prev (Stmt);
and then end loop;
(Nkind (Nod) not in N_Raise_xxx_Error
or else Present (Condition (Nod)));
end;
end if;
return False; -- At this point the node must be preceded by a raise statement,
-- and the raise statement has to be the sole statement within
-- the enclosing entry or subprogram body.
else return
C := P; Present (Raise_Stmt) and then Is_Sole_Statement (Raise_Stmt);
end if; end if;
end loop;
Error_Msg_Warn := SPARK_Mode /= On; return False;
Error_Msg_N ("!possible infinite recursion<<", N); end Is_Raise_Idiom;
Error_Msg_N ("\!??Storage_Error ]<<", N);
------------------------
-- Is_Raise_Statement --
------------------------
function Is_Raise_Statement (N : Node_Id) return Boolean is
begin
-- A raise statement may be transfomed into a Raise_xxx_Error node
return
Nkind (N) = N_Raise_Statement
or else Nkind (N) in N_Raise_xxx_Error;
end Is_Raise_Statement;
-----------------------
-- Is_Sole_Statement --
-----------------------
function Is_Sole_Statement (N : Node_Id) return Boolean is
Stmt : Node_Id;
begin
-- The input node appears within the statements of an entry or
-- subprogram body. Examine the statements preceding the node.
if Is_Immediately_Within_Body (N) then
Stmt := Prev (N);
while Present (Stmt) loop
-- The statement is preceded by another statement or a source
-- construct. This indicates that the node does not appear by
-- itself.
if Is_Control_Flow_Statement (Stmt)
or else Comes_From_Source (Stmt)
then
return False;
end if;
Stmt := Prev (Stmt);
end loop;
return True;
end if;
-- The input node is within a construct nested inside the entry or
-- subprogram body.
return False;
end Is_Sole_Statement;
----------------------------------------
-- Preceded_By_Control_Flow_Statement --
----------------------------------------
function Preceded_By_Control_Flow_Statement
(N : Node_Id) return Boolean
is
Stmt : Node_Id;
begin
if Is_List_Member (N) then
Stmt := Prev (N);
-- Examine the statements preceding the input node
while Present (Stmt) loop
if Is_Control_Flow_Statement (Stmt) then
return True;
end if;
Stmt := Prev (Stmt);
end loop;
return False;
end if;
-- Assume that the node is part of some control flow statement
return True;
end Preceded_By_Control_Flow_Statement;
----------------------------------
-- Within_Conditional_Statement --
----------------------------------
function Within_Conditional_Statement (N : Node_Id) return Boolean is
Stmt : Node_Id;
begin
Stmt := Parent (N);
while Present (Stmt) loop
if Is_Conditional_Statement (Stmt) then
return True;
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Stmt) then
exit;
end if;
Stmt := Parent (Stmt);
end loop;
return False;
end Within_Conditional_Statement;
-- Local variables
Call_Context : constant Node_Id :=
Enclosing_Declaration_Or_Statement (Call);
-- Start of processing for Check_Infinite_Recursion
begin
-- The call is assumed to be safe when the enclosing subprogram is
-- invoked with actuals other than its formals.
--
-- procedure Proc (F1 : ...; F2 : ...; ...; FN : ...) is
-- begin
-- ...
-- Proc (A1, A2, ..., AN);
-- ...
-- end Proc;
if Invoked_With_Different_Arguments (Call) then
return False;
-- The call is assumed to be safe when the invocation of the enclosing
-- subprogram depends on a conditional statement.
--
-- procedure Proc (F1 : ...; F2 : ...; ...; FN : ...) is
-- begin
-- ...
-- if Some_Condition then
-- Proc (F1, F2, ..., FN);
-- end if;
-- ...
-- end Proc;
elsif Within_Conditional_Statement (Call) then
return False;
-- The context of the call is assumed to be safe when the invocation of
-- the enclosing subprogram is preceded by some control flow statement.
--
-- procedure Proc (F1 : ...; F2 : ...; ...; FN : ...) is
-- begin
-- ...
-- if Some_Condition then
-- ...
-- end if;
-- ...
-- Proc (F1, F2, ..., FN);
-- ...
-- end Proc;
elsif Preceded_By_Control_Flow_Statement (Call_Context) then
return False;
-- Detect an idiom where the context of the call is preceded by a single
-- raise statement.
--
-- procedure Proc (F1 : ...; F2 : ...; ...; FN : ...) is
-- begin
-- raise ...;
-- Proc (F1, F2, ..., FN);
-- end Proc;
elsif Is_Raise_Idiom (Call_Context) then
return False;
end if;
-- At this point it is certain that infinite recursion will take place
-- as long as the call is executed. Detect a case where the context of
-- the call is the sole source statement within the subprogram body.
--
-- procedure Proc (F1 : ...; F2 : ...; ...; FN : ...) is
-- begin
-- Proc (F1, F2, ..., FN);
-- end Proc;
--
-- Install an explicit raise to prevent the infinite recursion.
if Is_Sole_Statement (Call_Context) then
Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("!infinite recursion<<", Call);
Error_Msg_N ("\!Storage_Error [<<", Call);
Insert_Action (Call,
Make_Raise_Storage_Error (Sloc (Call),
Reason => SE_Infinite_Recursion));
-- Otherwise infinite recursion could take place, considering other flow
-- control constructs such as gotos, exit statements, etc.
else
Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("!possible infinite recursion<<", Call);
Error_Msg_N ("\!??Storage_Error ]<<", Call);
end if;
return True; return True;
end Check_Infinite_Recursion; end Check_Infinite_Recursion;
......
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