[m-rev.] diff: fix termination pragmas
Julien Fischer
juliensf at students.cs.mu.OZ.AU
Tue Jun 24 14:16:11 AEST 2003
Estimated hours take: 5.5
Branches: main
Fix a bug in the termination analyser that caused it to ignore
pragma terminates/does_not_terminate declarations.
compiler/error_util:
Add a predicate describe_several_pred_names/3.
compiler/term_errors:
Add an error type indicating that the cause of non-termination was
inconsistent termination pragmas.
compiler/termination:
Fix a bug that caused pragma terminates and pragma does_not_terminate
declarations to be ignored.
Check that SCCs in the call-graph have not been annotated with
termination pragmas that are inconsistent.
Remove some old style lambda expressions.
doc/reference_manual.texi:
Describe how pramga terminates/does_not_terminate interact with
mutually recursive procedures.
tests/term/Mmakefile:
tests/term/pragma_non_term.m:
tests/term/pragma_non_term.trans_opt_exp:
tests/term/pragma_term.m:
tests/term/pragam_term.trans_opt_exp:
tests/warnings/Mercury.options:
tests/warnings/Mmakefile:
tests/warnings/pragma_term_conflict.m:
tests/warnings/pragma_term_conflict.exp:
Add some test cases for the termination pragmas.
Index: compiler/error_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/error_util.m,v
retrieving revision 1.22
diff -u -r1.22 error_util.m
--- compiler/error_util.m 26 May 2003 08:59:53 -0000 1.22
+++ compiler/error_util.m 20 Jun 2003 03:24:32 -0000
@@ -91,6 +91,9 @@
:- pred error_util__describe_one_pred_name(module_info::in, pred_id::in,
string::out) is det.
+:- pred error_util__describe_several_pred_names(module_info::in,
+ list(pred_id)::in, list(format_component)::out) is det.
+
:- pred error_util__describe_one_proc_name(module_info::in, pred_proc_id::in,
string::out) is det.
@@ -458,6 +461,10 @@
"'"], Piece)
).
+error_util__describe_several_pred_names(Module, PredId, Pieces) :-
+ list__map(error_util__describe_one_pred_name(Module), PredId, Pieces0),
+ error_util__list_to_pieces(Pieces0, Pieces).
+
error_util__describe_one_proc_name(Module, proc(PredId, ProcId), Piece) :-
error_util__describe_one_pred_name(Module, PredId, PredPiece),
proc_id_to_int(ProcId, ProcIdInt),
@@ -471,6 +478,8 @@
error_util__describe_several_proc_names(Module, PPIds, Pieces) :-
list__map(error_util__describe_one_proc_name(Module), PPIds, Pieces0),
error_util__list_to_pieces(Pieces0, Pieces).
+
+
error_util__describe_one_call_site(Module, PPId - Context, Piece) :-
error_util__describe_one_proc_name(Module, PPId, ProcName),
Index: compiler/term_errors.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_errors.m,v
retrieving revision 1.19
diff -u -r1.19 term_errors.m
--- compiler/term_errors.m 26 May 2003 09:00:10 -0000 1.19
+++ compiler/term_errors.m 24 Jun 2003 04:06:49 -0000
@@ -109,8 +109,12 @@
% least one output argument permits a norm greater
% than zero.
- ; does_not_term_pragma(pred_id).
+ ; does_not_term_pragma(pred_id)
% The given procedure has a does_not_terminate pragma.
+
+ ; inconsistent_annotations.
+ % The pragma terminates/does_not_terminate declarations
+ % for the procedures in this SCC are inconsistent.
:- type term_errors__error == pair(prog_context, termination_error).
@@ -438,6 +442,9 @@
Piece2 = fixed(Piece2Str)
),
list__append(Pieces1, [Piece2], Pieces).
+
+term_errors__description(inconsistent_annotations, _, _, Pieces, no) :-
+ Pieces = [words("The termination pragmas are inconsistent.")].
%----------------------------------------------------------------------------%
Index: compiler/termination.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/termination.m,v
retrieving revision 1.28
diff -u -r1.28 termination.m
--- compiler/termination.m 27 May 2003 05:57:21 -0000 1.28
+++ compiler/termination.m 24 Jun 2003 03:57:52 -0000
@@ -91,6 +91,7 @@
:- import_module check_hlds__inst_match.
:- import_module check_hlds__mode_util.
:- import_module check_hlds__type_util.
+:- import_module hlds__error_util.
:- import_module hlds__hlds_data.
:- import_module hlds__hlds_goal.
:- import_module hlds__hlds_out.
@@ -131,7 +132,12 @@
{ module_info_ensure_dependency_info(Module1, Module2) },
{ module_info_dependency_info(Module2, DepInfo) },
{ hlds_dependency_info_get_dependency_ordering(DepInfo, SCCs) },
- termination__process_all_sccs(SCCs, Module2, PassInfo, Module),
+
+ % Ensure that termination pragmas for a proc. do conflict
+ % with termination pragmas for other procs. in the same SCC.
+ check_pragmas_are_consistent(SCCs, Module2, Module3),
+
+ termination__process_all_sccs(SCCs, Module3, PassInfo, Module),
globals__io_lookup_bool_option(make_optimization_interface,
MakeOptInt),
@@ -157,6 +163,111 @@
find_weights(Module, WeightMap).
%----------------------------------------------------------------------------%
+% Check that any user-supplied termination information (from pragma
+% terminates/does_not_terminate) is consistent for each SCC in the program.
+%
+% The information will not be consistent if:
+% (1) One or more procs. in the SCC has a terminates pragma *and* one or more
+% procs. in the SCC has a does_not_terminate pragma.
+% (2) One or more procs. in the SCC has a termination pragma (of either sort),
+% *and* the termination status of one or more procs. in the SCC is
+% unknown. (We check this after checking for the first case, so the
+% termination info. for the known procs. will be consistent.)
+%
+% In the first case set the termination for all procs. in the SCC to
+% can_loop and emit a warning. In the second, set the termination of any
+% procs. whose termination status is unknown to be the same as those whose
+% termination status is known.
+
+:- pred check_pragmas_are_consistent(list(list(pred_proc_id)), module_info,
+ module_info, io__state, io__state).
+:- mode check_pragmas_are_consistent(in, in, out, di, uo) is det.
+
+check_pragmas_are_consistent(SCCs, Module0, Module) -->
+ list__foldl2(check_scc_pragmas_are_consistent, SCCs, Module0, Module).
+
+:- pred check_scc_pragmas_are_consistent(list(pred_proc_id), module_info,
+ module_info, io__state, io__state).
+:- mode check_scc_pragmas_are_consistent(in, in, out, di, uo) is det.
+
+check_scc_pragmas_are_consistent(SCC, Module0, Module, !IO) :-
+ list__filter(is_termination_known(Module0), SCC, SCCTerminationKnown,
+ SCCTerminationUnknown),
+ (
+ SCCTerminationKnown = [],
+ Module = Module0
+ ;
+ SCCTerminationKnown = [KnownPPId | _],
+ module_info_pred_proc_info(Module0, KnownPPId, _, KnownProcInfo),
+ proc_info_get_maybe_termination_info(KnownProcInfo, MaybeKnownTerm),
+ (
+ MaybeKnownTerm = no,
+ unexpected(this_file, "No termination info. found.")
+ ;
+ MaybeKnownTerm = yes(KnownTermStatus)
+ ),
+ (
+ check_procs_known_term(KnownTermStatus, SCCTerminationKnown,
+ Module0)
+ ->
+ % Force any procs. in the SCC whose termination status is
+ % unknown to have the same termination status as those that
+ % are known.
+ set_termination_infos(SCCTerminationUnknown, KnownTermStatus,
+ Module0, Module)
+ ;
+ % There is a conflict between the user-supplied termination
+ % information for two or more procs. in this SCC. Emit
+ % a warning and then assume that they all loop.
+ get_context_from_scc(SCCTerminationKnown, Module0, Context),
+ NewTermStatus = can_loop([Context - inconsistent_annotations]),
+ set_termination_infos(SCC, NewTermStatus, Module0, Module),
+
+ PredIds = list__map((func(proc(PredId, _)) = PredId),
+ SCCTerminationKnown),
+ error_util__describe_several_pred_names(Module, PredIds,
+ PredNames),
+ Piece1 = words("are mutually recursive but some of their"),
+ Piece2 = words("termination pragmas are inconsistent."),
+ Components = [words("Warning:")] ++ PredNames ++ [Piece1, Piece2],
+ error_util__report_warning(Context, 0, Components, !IO)
+ )
+ ).
+
+ % Check that all procedures in an SCC whose termination status is known
+ % have the same termination status.
+:- pred check_procs_known_term(termination_info, list(pred_proc_id),
+ module_info).
+:- mode check_procs_known_term(in, in, in) is semidet.
+
+check_procs_known_term(_, [], _).
+check_procs_known_term(Status, [PPId | PPIds], ModuleInfo) :-
+ module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
+ proc_info_get_maybe_termination_info(ProcInfo, MaybeTerm),
+ (
+ MaybeTerm = no,
+ unexpected(this_file, "No termination info for procedure.")
+ ;
+ MaybeTerm = yes(PPIdStatus)
+ ),
+ (
+ Status = cannot_loop,
+ PPIdStatus = cannot_loop
+ ;
+ Status = can_loop(_),
+ PPIdStatus = can_loop(_)
+ ),
+ check_procs_known_term(Status, PPIds, ModuleInfo).
+
+ % Succeeds iff the termination status of a procedure is known.
+:- pred is_termination_known(module_info, pred_proc_id).
+:- mode is_termination_known(in, in) is semidet.
+
+is_termination_known(Module, PPId) :-
+ module_info_pred_proc_info(Module, PPId, _, ProcInfo),
+ proc_info_get_maybe_termination_info(ProcInfo, yes(_)).
+
+%----------------------------------------------------------------------------%
:- pred termination__process_all_sccs(list(list(pred_proc_id)), module_info,
pass_info, module_info, io__state, io__state).
@@ -176,12 +287,12 @@
:- mode termination__process_scc(in, in, in, out, di, uo) is det.
termination__process_scc(SCC, Module0, PassInfo, Module) -->
- { IsArgSizeKnown = lambda([PPId::in] is semidet, (
+ { IsArgSizeKnown = (pred(PPId::in) is semidet :-
PPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module0, PredId, ProcId,
_, ProcInfo),
proc_info_get_maybe_arg_size_info(ProcInfo, yes(_))
- )) },
+ ) },
{ list__filter(IsArgSizeKnown, SCC,
_SCCArgSizeKnown, SCCArgSizeUnknown) },
( { SCCArgSizeUnknown = [] } ->
@@ -203,24 +314,22 @@
ArgSizeErrors = Errors
}
),
- { IsTerminationKnown = lambda([PPId::in] is semidet, (
- PPId = proc(PredId, ProcId),
- module_info_pred_proc_info(Module0, PredId, ProcId,
- _, ProcInfo),
- proc_info_get_maybe_arg_size_info(ProcInfo, yes(_))
- )) },
- { list__filter(IsTerminationKnown, SCC,
+ { list__filter(is_termination_known(Module1), SCC,
_SCCTerminationKnown, SCCTerminationUnknown) },
( { SCCTerminationUnknown = [] } ->
+ %
+ % We may possibly have encountered inconsistent
+ % terminates/does_not_terminate pragmas for this SCC,
+ % so we need to report errors here as well.
{ Module = Module1 }
;
- { IsFatal = lambda([ContextError::in] is semidet, (
+ { IsFatal = (pred(ContextError::in) is semidet :-
ContextError = _Context - Error,
( Error = horder_call
; Error = horder_args(_, _)
; Error = imported_pred
)
- )) },
+ ) },
{ list__filter(IsFatal, ArgSizeErrors, FatalErrors) },
{ list__append(TermErrors, FatalErrors, BothErrors) },
( { BothErrors = [_ | _] } ->
@@ -239,9 +348,9 @@
),
{ set_termination_infos(SCCTerminationUnknown,
TerminationResult, Module1, Module2) },
- ( { TerminationResult = can_loop(TerminationErrors) } ->
- report_termination_errors(SCC, TerminationErrors,
- Module2, Module)
+ ( { TerminationResult = can_loop(TerminationErrors) } ->
+ report_termination_errors(SCC, TerminationErrors, Module2,
+ Module)
;
{ Module = Module2 }
)
@@ -846,3 +955,9 @@
[]
)
).
+
+%----------------------------------------------------------------------------%
+
+:- func this_file = string.
+
+this_file = "termination.m".
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.275
diff -u -r1.275 reference_manual.texi
--- doc/reference_manual.texi 19 May 2003 14:24:31 -0000 1.275
+++ doc/reference_manual.texi 19 Jun 2003 07:23:22 -0000
@@ -8331,7 +8331,9 @@
or function is guaranteed to terminate for any input. This is useful
when the compiler cannot prove termination of some predicates or
functions which are in turn preventing the compiler from proving
-termination of other predicates or functions.
+termination of other predicates or functions. This declaration
+effects not only the predicate specified but also
+any other predicates that are mutually recursive with it.
@example
:- pragma does_not_terminate(@var{Name}/@var{Arity}).
@@ -8340,7 +8342,8 @@
This declaration may be used to inform the compiler that this predicate
does not necessarily terminate. This is useful for procedures defined
using the C interface, which the compiler assumes to terminate by
-default.
+default. This declaration effects not only the predicate specified
+but also any other predicates that are mutually recursive with it.
@example
:- pragma check_termination(@var{Name}/@var{Arity}).
Index: tests/term/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/term/Mmakefile,v
retrieving revision 1.19
diff -u -r1.19 Mmakefile
--- tests/term/Mmakefile 12 Jan 2003 22:33:31 -0000 1.19
+++ tests/term/Mmakefile 18 Jun 2003 09:11:11 -0000
@@ -57,6 +57,8 @@
pl8_3_1a \
pl8_4_1 \
pl8_4_2 \
+ pragma_non_term \
+ pragma_term \
queens \
quicksort \
select \
Index: tests/term/pragma_non_term.m
===================================================================
RCS file: tests/term/pragma_non_term.m
diff -N tests/term/pragma_non_term.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/term/pragma_non_term.m 18 Jun 2003 09:07:19 -0000
@@ -0,0 +1,12 @@
+:- module pragma_non_term.
+
+:- interface.
+
+:- pred a is det.
+
+:- implementation.
+
+:- pragma does_not_terminate(a/0).
+
+a :- true.
+
Index: tests/term/pragma_non_term.trans_opt_exp
===================================================================
RCS file: tests/term/pragma_non_term.trans_opt_exp
diff -N tests/term/pragma_non_term.trans_opt_exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/term/pragma_non_term.trans_opt_exp 18 Jun 2003 09:08:15 -0000
@@ -0,0 +1,2 @@
+:- module pragma_non_term.
+:- pragma termination_info((pragma_non_term.a), finite(0, []), can_loop).
Index: tests/term/pragma_term.m
===================================================================
RCS file: tests/term/pragma_term.m
diff -N tests/term/pragma_term.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/term/pragma_term.m 19 Jun 2003 04:49:37 -0000
@@ -0,0 +1,11 @@
+:- module pragma_term.
+
+:- interface.
+
+:- pred a is det.
+
+:- implementation.
+
+:- pragma terminates(a/0).
+
+a :- a.
Index: tests/term/pragma_term.trans_opt_exp
===================================================================
RCS file: tests/term/pragma_term.trans_opt_exp
diff -N tests/term/pragma_term.trans_opt_exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/term/pragma_term.trans_opt_exp 18 Jun 2003 09:10:28 -0000
@@ -0,0 +1,2 @@
+:- module pragma_term.
+:- pragma termination_info((pragma_term.a), finite(0, []), cannot_loop).
Index: tests/warnings/Mercury.options
===================================================================
RCS file: /home/mercury1/repository/tests/warnings/Mercury.options,v
retrieving revision 1.6
diff -u -r1.6 Mercury.options
--- tests/warnings/Mercury.options 20 May 2003 08:45:19 -0000 1.6
+++ tests/warnings/Mercury.options 24 Jun 2003 03:46:51 -0000
@@ -34,3 +34,7 @@
MCFLAGS-infinite_recursion = --excess-assign --common-struct
MCFLAGS-warn_stubs = --allow-stubs --warn-unused-args
+
+ # Conflicting termination pragmas won't show up unless we
+ # perform termination analysis.
+MCFLAGS-pragma_term_conflict = --enable-termination
Index: tests/warnings/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/warnings/Mmakefile,v
retrieving revision 1.30
diff -u -r1.30 Mmakefile
--- tests/warnings/Mmakefile 21 Feb 2003 01:57:38 -0000 1.30
+++ tests/warnings/Mmakefile 20 Jun 2003 06:48:53 -0000
@@ -5,7 +5,8 @@
#-----------------------------------------------------------------------------#
COMPILE_PROGS= \
- arg_order_rearrangment
+ arg_order_rearrangment \
+ pragma_term_conflict
ERRORCHECK_PROGS= \
ambiguous_overloading \
Index: tests/warnings/pragma_term_conflict.exp
===================================================================
RCS file: tests/warnings/pragma_term_conflict.exp
diff -N tests/warnings/pragma_term_conflict.exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/warnings/pragma_term_conflict.exp 24 Jun 2003 03:48:53 -0000
@@ -0,0 +1,4 @@
+pragma_term_conflict.m:008: Warning: predicate `pragma_term_conflict.a/0' and
+pragma_term_conflict.m:008: predicate `pragma_term_conflict.b/0' are mutually
+pragma_term_conflict.m:008: recursive but some of their termination pragmas
+pragma_term_conflict.m:008: are inconsistent.
Index: tests/warnings/pragma_term_conflict.m
===================================================================
RCS file: tests/warnings/pragma_term_conflict.m
diff -N tests/warnings/pragma_term_conflict.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/warnings/pragma_term_conflict.m 20 Jun 2003 06:29:19 -0000
@@ -0,0 +1,21 @@
+
+ % Check termination pragmas do not conflict with each other when
+ % analysing mutually recursive predicates.
+:- module pragma_term_conflict.
+
+:- interface.
+
+:- pred a is det.
+
+:- implementation.
+
+:- pred b is det.
+
+:- pred c is det.
+
+:- pragma terminates(a/0).
+:- pragma does_not_terminate(b/0).
+
+a :- b.
+b :- c.
+c :- a.
--------------------------------------------------------------------------
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