* [Ada] Failure to detect trivial infinite recursion
@ 2019-07-05 7:08 Pierre-Marie de Rodat
0 siblings, 0 replies; 2+ messages in thread
From: Pierre-Marie de Rodat @ 2019-07-05 7:08 UTC (permalink / raw)
To: gcc-patches; +Cc: Hristian Kirtchev
[-- Attachment #1: Type: text/plain, Size: 3230 bytes --]
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
Tested on x86_64-pc-linux-gnu, committed on trunk
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.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 19318 bytes --]
--- gcc/ada/sem_res.adb
+++ gcc/ada/sem_res.adb
@@ -111,8 +111,8 @@ package body Sem_Res is
Pref : Node_Id);
-- Check that the type of the prefix of a dereference is not incomplete
- function Check_Infinite_Recursion (N : Node_Id) return Boolean;
- -- Given a call node, N, which is known to occur immediately within the
+ function Check_Infinite_Recursion (Call : Node_Id) return Boolean;
+ -- Given a call node, Call, which is known to occur immediately within the
-- subprogram being called, determines whether it is a detectable case of
-- an infinite recursion, and if so, outputs appropriate messages. Returns
-- True if an infinite recursion is detected, and False otherwise.
@@ -695,164 +695,406 @@ package body Sem_Res is
-- Check_Infinite_Recursion --
------------------------------
- function Check_Infinite_Recursion (N : Node_Id) return Boolean is
- P : Node_Id;
- C : Node_Id;
+ function Check_Infinite_Recursion (Call : Node_Id) return Boolean is
+ function Enclosing_Declaration_Or_Statement (N : Node_Id) return Node_Id;
+ -- Return the nearest enclosing declaration or statement that houses
+ -- arbitrary node N.
- function Same_Argument_List return Boolean;
- -- Check whether list of actuals is identical to list of formals of
- -- called function (which is also the enclosing scope).
+ function Invoked_With_Different_Arguments (N : Node_Id) return Boolean;
+ -- Determine whether call N invokes the related enclosing subprogram
+ -- with actuals that differ from the subprogram's formals.
- ------------------------
- -- Same_Argument_List --
- ------------------------
+ function Is_Conditional_Statement (N : Node_Id) return Boolean;
+ -- 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
- A : Node_Id;
- F : Entity_Id;
- Subp : Entity_Id;
+ function Is_Raise_Statement (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes a raise statement
+
+ 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
- if not Is_Entity_Name (Name (N)) then
- return False;
- else
- Subp := Entity (Name (N));
- end if;
+ Par := N;
+ while Present (Par) loop
+ if Is_Declaration (Par) or else Is_Statement (Par) then
+ return Par;
- F := First_Formal (Subp);
- A := First_Actual (N);
- while Present (F) and then Present (A) loop
- if not Is_Entity_Name (A) or else Entity (A) /= F then
- return False;
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Par) then
+ exit;
end if;
- Next_Actual (A);
- Next_Formal (F);
+ Par := Parent (Par);
end loop;
- return True;
- end Same_Argument_List;
+ return N;
+ end Enclosing_Declaration_Or_Statement;
- -- Start of processing for Check_Infinite_Recursion
+ --------------------------------------
+ -- Invoked_With_Different_Arguments --
+ --------------------------------------
- begin
- -- Special case, if this is a procedure call and is a call to the
- -- current procedure with the same argument list, then this is for
- -- sure an infinite recursion and we insert a call to raise SE.
+ function Invoked_With_Different_Arguments (N : Node_Id) return Boolean is
+ Subp : constant Entity_Id := Entity (Name (N));
- if Is_List_Member (N)
- and then List_Length (List_Containing (N)) = 1
- and then Same_Argument_List
- then
- declare
- P : constant Node_Id := Parent (N);
- begin
- if Nkind (P) = N_Handled_Sequence_Of_Statements
- and then Nkind (Parent (P)) = N_Subprogram_Body
- and then Is_Empty_List (Declarations (Parent (P)))
+ Actual : Node_Id;
+ Formal : Entity_Id;
+
+ begin
+ -- Determine whether the formals of the invoked subprogram are not
+ -- used as actuals in the call.
+
+ Actual := First_Actual (Call);
+ Formal := First_Formal (Subp);
+ 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
- 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;
end if;
- end;
- end if;
- -- If not that special case, search up tree, quitting if we reach a
- -- construct (e.g. a conditional) that tells us that this is not a
- -- case for an infinite recursion warning.
+ Next_Actual (Actual);
+ Next_Formal (Formal);
+ end loop;
- C := N;
- loop
- P := Parent (C);
+ return False;
+ end Invoked_With_Different_Arguments;
- -- If no parent, then we were not inside a subprogram, this can for
- -- example happen when processing certain pragmas in a spec. Just
- -- return False in this case.
+ ------------------------------
+ -- Is_Conditional_Statement --
+ ------------------------------
- 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;
+
+ -- 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 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,
- N_Case_Expression,
- N_Case_Statement,
- N_If_Expression,
- N_If_Statement)
- then
- return False;
+ --------------------
+ -- Is_Raise_Idiom --
+ --------------------
- elsif Nkind (P) = N_Handled_Sequence_Of_Statements
- and then C /= First (Statements (P))
- then
- -- 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.
+ function Is_Raise_Idiom (N : Node_Id) return Boolean is
+ Raise_Stmt : Node_Id;
+ Stmt : Node_Id;
- -- Furthermore, this corresponds to a common idiom:
+ begin
+ if Is_Immediately_Within_Body (N) then
- -- function F (L : Thing) return Boolean is
- -- begin
- -- raise Program_Error;
- -- return F (L);
- -- end F;
+ -- Assume that no raise statement has been seen yet
- -- for generating a stub function
+ Raise_Stmt := Empty;
- if Nkind (Parent (N)) = N_Simple_Return_Statement
- and then Same_Argument_List
- then
- exit when not Is_List_Member (Parent (N));
+ -- Examine the statements preceding the input node, skipping
+ -- internally-generated constructs.
- -- OK, return statement is in a statement list, look for raise
+ Stmt := Prev (N);
+ while Present (Stmt) loop
- declare
- Nod : Node_Id;
+ -- Multiple raise statements violate the idiom
- begin
- -- Skip past N_Freeze_Entity nodes generated by expansion
+ if Is_Raise_Statement (Stmt) then
+ if Present (Raise_Stmt) then
+ return False;
+ end if;
- Nod := Prev (Parent (N));
- while Present (Nod)
- and then Nkind (Nod) = N_Freeze_Entity
- loop
- Prev (Nod);
- end loop;
+ Raise_Stmt := Stmt;
- -- If no raise statement, give warning. We look at the
- -- original node, because in the case of "raise ... with
- -- ...", the node has been transformed into a call.
+ elsif Comes_From_Source (Stmt) then
+ exit;
+ end if;
- exit when Nkind (Original_Node (Nod)) /= N_Raise_Statement
- and then
- (Nkind (Nod) not in N_Raise_xxx_Error
- or else Present (Condition (Nod)));
- end;
- end if;
+ Stmt := Prev (Stmt);
+ end loop;
- 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
- C := P;
+ return
+ Present (Raise_Stmt) and then Is_Sole_Statement (Raise_Stmt);
end if;
- end loop;
- Error_Msg_Warn := SPARK_Mode /= On;
- Error_Msg_N ("!possible infinite recursion<<", N);
- Error_Msg_N ("\!??Storage_Error ]<<", N);
+ return False;
+ end Is_Raise_Idiom;
+
+ ------------------------
+ -- 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;
end Check_Infinite_Recursion;
^ permalink raw reply [flat|nested] 2+ messages in thread
* [Ada] Failure to detect trivial infinite recursion
@ 2019-07-05 7:08 Pierre-Marie de Rodat
0 siblings, 0 replies; 2+ messages in thread
From: Pierre-Marie de Rodat @ 2019-07-05 7:08 UTC (permalink / raw)
To: gcc-patches; +Cc: Hristian Kirtchev
[-- Attachment #1: Type: text/plain, Size: 507 bytes --]
This patch includes delay statements in the set of control flow
statements since their expressions may have side effects, which in turn
may affect an infinite recursion.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-07-05 Hristian Kirtchev <kirtchev@adacore.com>
gcc/ada/
* sem_res.adb (Is_Control_Flow_Statement): Delay statements
contain an expression, which in turn may have side effects and
affect the infinite recursion. As a result, delay statements
should not be treated specially.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 1035 bytes --]
--- gcc/ada/sem_res.adb
+++ gcc/ada/sem_res.adb
@@ -816,19 +816,11 @@ package body Sem_Res is
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.
+ -- It is assumed that all statements may affect the control flow in
+ -- some way. A raise statement may be expanded into a non-statement
+ -- node.
- if Nkind (N) in N_Delay_Statement then
- 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;
+ return Is_Statement (N) or else Is_Raise_Statement (N);
end Is_Control_Flow_Statement;
--------------------------------
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2019-07-05 7:08 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-07-05 7:08 [Ada] Failure to detect trivial infinite recursion Pierre-Marie de Rodat
-- strict thread matches above, loose matches on Subject: below --
2019-07-05 7:08 Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).