[m-rev.] for review: fix yet another termination analysis bug
Julien Fischer
juliensf at students.cs.mu.OZ.AU
Mon Dec 15 14:35:35 AEDT 2003
Estimated hours taken: 10
Branches: main
Fix a bug in the termination analysis that causes a software error
during pass 2. This is due to a sanity check failing.
The bug in pass 1 occurred when the analyser detected a call to a procedure
that had an infinite change constant. If the call affected the size
of any of the variables in the caller then the analyser marked it as an
error and aborted the remainder of pass 1. Any other procedures in the
SCC were not checked and their change constant was set to infinite.
The analyser did not (correctly) consider a infinite change constant to be a
fatal error, ie. one that would result in nontermination, so it ran pass 2.
However, since the remainder of the SCC had not been analysed during pass 1
it had not been determined if any of those procedures made calls to
procedures that had been marked as nonterminating. Pass 2 assumes the
opposite, namely that any SCC that is analysing will contain no calls
to procedures that have been marked as nonterminating since pass 1
should have detected this.
This diff fixes that problem by checking the remainder of the SCC for
nonterminating calls if the usual pass 1 is aborted.
compiler/term_pass1.m:
Make sure that all of the SCC is checked for calls to nonterminating
procedures when the analysis is abandoned due to a non-fatal error.
Add a comment about why this is necessary.
Add an end_module declaration.
compiler/term_pass2.m:
Document some assumptions that this module makes.
compiler/term_traversal:
Fix some formatting.
tests/term/Mmakefile:
tests/term/Mercury.options:
tests/term/inf_const_bug.m:
tests/term/inf_const_bug.trans_opt_exp
Add a new test case.
Julien.
Index: compiler/term_pass1.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_pass1.m,v
retrieving revision 1.13
diff -u -r1.13 term_pass1.m
--- compiler/term_pass1.m 5 Nov 2003 03:17:44 -0000 1.13
+++ compiler/term_pass1.m 15 Dec 2003 03:22:46 -0000
@@ -56,13 +56,14 @@
:- import_module check_hlds__type_util.
:- import_module hlds__hlds_data.
:- import_module hlds__hlds_goal.
+:- import_module hlds__error_util.
:- import_module parse_tree__prog_data.
:- import_module transform_hlds__lp.
:- import_module transform_hlds__term_errors.
:- import_module transform_hlds__term_traversal.
:- import_module int, float, char, string, bool, set, bag, map.
-:- import_module term, varset, require.
+:- import_module string, term, varset, require.
%-----------------------------------------------------------------------------%
@@ -169,27 +170,35 @@
list(term_errors__error)::in, list(term_errors__error)::out) is det.
find_arg_sizes_in_scc_pass([], _, _, OutputSupplierMap, Paths, SubsetErrors,
- Result, TermErrors, TermErrors) :-
+ Result, !TermErrors) :-
Result = ok(Paths, OutputSupplierMap, SubsetErrors).
find_arg_sizes_in_scc_pass([PPId | PPIds], Module, PassInfo,
OutputSupplierMap0, Paths0, SubsetErrors0, Result,
- TermErrors0, TermErrors) :-
+ !TermErrors) :-
find_arg_sizes_pred(PPId, Module, PassInfo, OutputSupplierMap0,
- Result1, TermErrors1),
- list__append(TermErrors0, TermErrors1, TermErrors2),
+ Result1, ProcTermErrors),
+ list__append(!.TermErrors, ProcTermErrors, !:TermErrors),
PassInfo = pass_info(_, MaxErrors, _),
- list__take_upto(MaxErrors, TermErrors2, TermErrors3),
+ list__take_upto(MaxErrors, !TermErrors),
(
Result1 = error(_),
- Result = Result1,
- TermErrors = TermErrors3
+ Result = Result1,
+ % The error does not necessarily mean that this
+ % SCC is nonterminating. We need to check that
+ % the remainder of this SCC does not make any
+ % nonterminating calls otherwise we might get
+ % a software error during pass 2.
+ % (See below for details).
+ list__foldl(check_proc_non_term_calls(Module), PPIds, [],
+ OtherTermErrors),
+ list__append(OtherTermErrors, !TermErrors)
;
Result1 = ok(Paths1, OutputSupplierMap1, SubsetErrors1),
list__append(Paths0, Paths1, Paths),
list__append(SubsetErrors0, SubsetErrors1, SubsetErrors),
find_arg_sizes_in_scc_pass(PPIds, Module, PassInfo,
OutputSupplierMap1, Paths, SubsetErrors, Result,
- TermErrors3, TermErrors)
+ !TermErrors)
).
%-----------------------------------------------------------------------------%
@@ -262,8 +271,107 @@
update_output_suppliers(Args, ActiveVars,
OutputSuppliers0, OutputSuppliers).
-%-----------------------------------------------------------------------------%
-%-----------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+%
+% Check if a procedure makes any nonterminating calls.
+%
+
+% We only use this if we have detected an error at some point during the
+% argument size analysis. The idea is to quickly analyse a procedure and
+% see if it does anything that would prevent us from running pass 2.
+% We cannot run pass 2 if the procedure contains any calls to nonterminating
+% procedures lower down the call-graph (see term_pass2.m for details).
+
+:- pred check_proc_non_term_calls(module_info::in, pred_proc_id::in,
+ list(term_errors__error)::in, list(term_errors__error)::out) is det.
+
+check_proc_non_term_calls(Module, PPId, !Errors) :-
+ module_info_pred_proc_info(Module, PPId, _, ProcInfo),
+ proc_info_goal(ProcInfo, Goal),
+ proc_info_vartypes(ProcInfo, VarTypes),
+ check_goal_non_term_calls(Module, PPId, VarTypes, Goal, !Errors).
+
+:- pred check_goal_non_term_calls(module_info::in,
+ pred_proc_id::in, vartypes::in, hlds_goal::in,
+ list(term_errors__error)::in, list(term_errors__error)::out) is det.
+
+check_goal_non_term_calls(Module, PPId, VarTypes, GoalExpr - GoalInfo,
+ !Errors) :-
+ check_goal_expr_non_term_calls(Module, PPId, VarTypes, GoalExpr,
+ GoalInfo, !Errors).
+
+:- pred check_goal_expr_non_term_calls(module_info::in, pred_proc_id::in,
+ vartypes::in, hlds_goal_expr::in, hlds_goal_info::in,
+ list(term_errors__error)::in, list(term_errors__error)::out) is det.
+
+check_goal_expr_non_term_calls(Module, PPId, VarTypes, conj(Goals), _,
+ !Errors):-
+ list__foldl(check_goal_non_term_calls(Module, PPId, VarTypes), Goals,
+ !Errors).
+check_goal_expr_non_term_calls(Module, PPId, VarTypes,
+ call(CallPredId, CallProcId, Args, _, _, _), GoalInfo,
+ !Errors) :-
+ CallPPId = proc(CallPredId, CallProcId),
+ module_info_pred_proc_info(Module, CallPPId, _, ProcInfo),
+ proc_info_get_maybe_termination_info(ProcInfo, TerminationInfo),
+ goal_info_get_context(GoalInfo, Context),
+ (
+ TerminationInfo = yes(can_loop(_))
+ ->
+ TermError = Context - can_loop_proc_called(PPId, CallPPId),
+ !:Errors = [ TermError | !.Errors ]
+ ;
+ true
+ ),
+ (
+ horder_vars(Args, VarTypes)
+ ->
+ HigherOrderError = Context - horder_args(PPId, CallPPId),
+ !:Errors = [ HigherOrderError | !.Errors ]
+ ;
+ true
+ ).
+check_goal_expr_non_term_calls(_, _, _, generic_call(_,_,_,_), GoalInfo,
+ !Errors) :-
+ goal_info_get_context(GoalInfo, Context),
+ !:Errors = [ Context - horder_call | !.Errors ].
+check_goal_expr_non_term_calls(Module, PPId, VarTypes, switch(_, _, Cases), _,
+ !Errors) :-
+ list__foldl(check_cases_non_term_calls(Module, PPId, VarTypes), Cases,
+ !Errors).
+check_goal_expr_non_term_calls(_, _, _, unify(_,_,_,_,_), _, !Errors).
+check_goal_expr_non_term_calls(Module, PPId, VarTypes, disj(Goals), _,
+ !Errors) :-
+ list__foldl(check_goal_non_term_calls(Module, PPId, VarTypes), Goals,
+ !Errors).
+check_goal_expr_non_term_calls(Module, PPId, VarTypes, not(Goal), _, !Errors) :-
+ check_goal_non_term_calls(Module, PPId, VarTypes, Goal, !Errors).
+check_goal_expr_non_term_calls(Module, PPId, VarTypes, some(_, _, Goal), _,
+ !Errors) :-
+ check_goal_non_term_calls(Module, PPId, VarTypes, Goal, !Errors).
+check_goal_expr_non_term_calls(Module, PPId, VarTypes,
+ if_then_else(_, Cond, Then, Else), _, !Errors) :-
+ list__foldl(check_goal_non_term_calls(Module, PPId, VarTypes),
+ [Cond, Then, Else], !Errors).
+check_goal_expr_non_term_calls(_, _, _, foreign_proc(_, _, _, _, _, _, _),
+ _, !Errors).
+check_goal_expr_non_term_calls(Module, PPId, VarTypes, par_conj(Goals), _,
+ !Errors) :-
+ list__foldl(check_goal_non_term_calls(Module, PPId, VarTypes), Goals,
+ !Errors).
+check_goal_expr_non_term_calls(_, _, _, shorthand(_), _, _, _) :-
+ unexpected(this_file,
+ "shorthand goal encountered during termination analysis.").
+
+:- pred check_cases_non_term_calls(module_info::in, pred_proc_id::in,
+ vartypes::in, case::in,
+ list(term_errors__error)::in, list(term_errors__error)::out) is det.
+
+check_cases_non_term_calls(Module, PPId, VarTypes, case(_, Goal), !Errors) :-
+ check_goal_non_term_calls(Module, PPId, VarTypes, Goal, !Errors).
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
% Solve the list of constraints
@@ -375,4 +483,12 @@
map__det_insert(PPVars0, PPId, Var, PPVars)
).
+%-----------------------------------------------------------------------------%
+
+:- func this_file = string.
+
+this_file = "term_pass1.m".
+
+%-----------------------------------------------------------------------------%
+:- end_module term_pass1.
%-----------------------------------------------------------------------------%
Index: compiler/term_pass2.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_pass2.m,v
retrieving revision 1.13
diff -u -r1.13 term_pass2.m
--- compiler/term_pass2.m 5 Nov 2003 03:17:44 -0000 1.13
+++ compiler/term_pass2.m 15 Dec 2003 03:19:34 -0000
@@ -65,6 +65,9 @@
%-----------------------------------------------------------------------------
+ % NOTE: This code assumes that the SCC does not call any
+ % nonterminating procedures. If it does then that fact
+ % should have been detected during pass 1.
prove_termination_in_scc(SCC, Module, PassInfo, SingleArgs, Termination) :-
init_rec_input_suppliers(SCC, Module, InitRecSuppliers),
prove_termination_in_scc_trial(SCC, InitRecSuppliers, down,
Index: compiler/term_traversal.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_traversal.m,v
retrieving revision 1.25
diff -u -r1.25 term_traversal.m
--- compiler/term_traversal.m 8 Dec 2003 03:37:44 -0000 1.25
+++ compiler/term_traversal.m 12 Dec 2003 06:46:59 -0000
@@ -515,8 +515,7 @@
termination_error::in, traversal_info::in, traversal_info::out) is det.
error_if_intersect(_, _, _, error(Errors, CanLoop), error(Errors, CanLoop)).
-error_if_intersect(OutVars, Context, ErrorMsg, ok(Paths, CanLoop), Info)
- :-
+error_if_intersect(OutVars, Context, ErrorMsg, ok(Paths, CanLoop), Info) :-
(
set__to_sorted_list(Paths, PathList),
some_active_vars_in_bag(PathList, OutVars)
Index: tests/term/Mercury.options
===================================================================
RCS file: /home/mercury1/repository/tests/term/Mercury.options,v
retrieving revision 1.3
diff -u -r1.3 Mercury.options
--- tests/term/Mercury.options 8 Dec 2003 03:37:45 -0000 1.3
+++ tests/term/Mercury.options 13 Dec 2003 13:33:43 -0000
@@ -12,6 +12,7 @@
MCFLAGS-existential_error2=--term-norm=num-data-elems
MCFLAGS-existential_error3=--term-norm=num-data-elems
MCFLAGS-fold=--term-norm=simple
+MCFLAGS-inf_const_bug=--term-norm=total
MCFLAGS-my_list=--term-norm=simple
MCFLAGS-lte=--term-norm=simple
MCFLAGS-my_map=--term-norm=simple
Index: tests/term/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/term/Mmakefile,v
retrieving revision 1.22
diff -u -r1.22 Mmakefile
--- tests/term/Mmakefile 8 Dec 2003 03:37:45 -0000 1.22
+++ tests/term/Mmakefile 13 Dec 2003 13:33:15 -0000
@@ -23,6 +23,7 @@
existential_error2 \
existential_error3 \
fold \
+ inf_const_bug \
my_list \
lte \
my_map \
Index: tests/term/inf_const_bug.m
===================================================================
RCS file: tests/term/inf_const_bug.m
diff -N tests/term/inf_const_bug.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/term/inf_const_bug.m 15 Dec 2003 03:22:11 -0000
@@ -0,0 +1,53 @@
+% Regression test - rotd 2003-12-14 and before caused a software error
+% in term_pass2.m.
+%
+% Symptom:
+% Uncaught Mercury exception:
+% Software Error: can_loop detected in pass2 but not pass1
+
+:- module inf_const_bug.
+
+:- interface.
+
+:- type list(T) ---> [] ; [T | list(T)].
+
+:- type pair(T1, T2) ---> (T1 - T2).
+
+:- type a == pair(b, nat).
+
+:- type nat ---> zero ; s(nat).
+
+:- type b ---> b(list(a)).
+
+:- func foo(a) = a.
+
+:- implementation.
+
+foo(B - N) = bar(B) - square(N).
+
+ % We need to ensure that pass 1 also considers this function
+ % otherwise we will miss the fact that the SCC is nonterminating.
+:- func bar(b) = b.
+
+bar(b(As)) = b(map(foo, As)).
+
+:- func square(nat) = nat.
+
+square(A) = multiply(A, A).
+
+:- func multiply(nat, nat) = nat.
+
+multiply(zero, _) = zero.
+multiply(s(X), Y) = add(multiply(X, Y), Y).
+
+:- func add(nat, nat) = nat.
+
+add(zero, Y) = Y.
+add(s(X), Y) = s(add(X, Y)).
+
+:- func map(func(X) = Y, list(X)) = list(Y).
+
+map(_, []) = [].
+map(P, [X | Xs]) = [ P(X) | map(P, Xs) ].
+
+:- end_module inf_const_bug.
Index: tests/term/inf_const_bug.trans_opt_exp
===================================================================
RCS file: tests/term/inf_const_bug.trans_opt_exp
diff -N tests/term/inf_const_bug.trans_opt_exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/term/inf_const_bug.trans_opt_exp 13 Dec 2003 13:32:57 -0000
@@ -0,0 +1,6 @@
+:- module inf_const_bug.
+:- pragma termination_info(inf_const_bug.foo((builtin.in)) = (builtin.out), infinite, can_loop).
+:- pragma termination_info(inf_const_bug.bar((builtin.in)) = (builtin.out), infinite, can_loop).
+:- pragma termination_info(inf_const_bug.square((builtin.in)) = (builtin.out), infinite, cannot_loop).
+:- pragma termination_info(inf_const_bug.multiply((builtin.in), (builtin.in)) = (builtin.out), infinite, cannot_loop).
+:- pragma termination_info(inf_const_bug.map((builtin.in), (builtin.in)) = (builtin.out), infinite, can_loop).
--------------------------------------------------------------------------
mercury-reviews mailing list
post: mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the reviews
mailing list