[m-rev.] for review: analysis of generic calls for old termination analyser
Julien Fischer
juliensf at cs.mu.OZ.AU
Mon Jul 4 18:40:29 AEST 2005
For review by anyone.
Estimated hours taken: 5
Branches: main
Add the capability for the old termination analyser to make use of the
results of closure analysis when analysing generic calls. This is part
of a larger set of changes to add support for analysing higher-order
constructs to both termination analysers and the exception analysis.
XXX This change is not particularly useful at the moment because the
procedure dependency graphs we construct do not record information
about higher-order calls. I'll add some test cases for termination
analysis of generic calls when this is fixed.
compiler/term_traversal.m:
When processing generic_calls optionally use information derived
from closure analysis.
compiler/mercury_compile.m:
Optionally run closure analysis when building the .trans_opt files.
Don't look up the value of the analyse_closures option twice.
compiler/term_errors.m:
Distinguish between the different types of generic_call that can be
made. Specialise the warnings produced by the termination analyser
for each type.
TODO: improve warning message where the values of higher-order
variables are known.
compiler/term_util.m:
Add a utility predicate that checks whether the termination_info
for a given procedure has been set to cannot_loop(_).
Julien.
Workspace:/home/earth/juliensf/ws-closure-analysis2
Index: compiler/mercury_compile.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_compile.m,v
retrieving revision 1.334
diff -u -r1.334 mercury_compile.m
--- compiler/mercury_compile.m 17 Jun 2005 10:13:52 -0000 1.334
+++ compiler/mercury_compile.m 29 Jun 2005 05:14:57 -0000
@@ -2065,8 +2065,6 @@
globals__lookup_bool_option(Globals, termination2, Termination2),
globals__lookup_bool_option(Globals, analyse_exceptions,
ExceptionAnalysis),
- globals__lookup_bool_option(Globals, analyse_closures,
- ClosureAnalysis),
(
MakeOptInt = yes,
intermod__write_optfile(!HLDS, !IO),
@@ -2085,12 +2083,8 @@
mercury_compile__frontend_pass_by_phases(!HLDS, FoundModeError,
!IO),
( FoundModeError = no ->
- ( ClosureAnalysis = yes ->
- mercury_compile.maybe_closure_analysis(
- Verbose, Stats, !HLDS, !IO)
- ;
- true
- ),
+ mercury_compile.maybe_closure_analysis(Verbose, Stats,
+ !HLDS, !IO),
(
ExceptionAnalysis = yes,
mercury_compile__maybe_exception_analysis(Verbose, Stats,
@@ -2159,17 +2153,18 @@
:- pred mercury_compile__output_trans_opt_file(module_info::in, io::di,
io::uo) is det.
-mercury_compile__output_trans_opt_file(HLDS0, !IO) :-
+mercury_compile__output_trans_opt_file(!.HLDS, !IO) :-
globals__io_lookup_bool_option(verbose, Verbose, !IO),
globals__io_lookup_bool_option(statistics, Stats, !IO),
- mercury_compile__maybe_exception_analysis(Verbose, Stats, HLDS0, HLDS1,
- !IO),
- mercury_compile__maybe_dump_hlds(HLDS1, 118, "exception_analysis", !IO),
- mercury_compile__maybe_termination(Verbose, Stats, HLDS1, HLDS2, !IO),
- mercury_compile__maybe_dump_hlds(HLDS2, 120, "termination", !IO),
- mercury_compile__maybe_termination2(Verbose, Stats, HLDS2, HLDS, !IO),
- mercury_compile__maybe_dump_hlds(HLDS, 121, "termination_2", !IO),
- trans_opt__write_optfile(HLDS, !IO).
+ mercury_compile__maybe_closure_analysis(Verbose, Stats, !HLDS, !IO),
+ mercury_compile__maybe_dump_hlds(!.HLDS, 117, "closure_analysis", !IO),
+ mercury_compile__maybe_exception_analysis(Verbose, Stats, !HLDS, !IO),
+ mercury_compile__maybe_dump_hlds(!.HLDS, 118, "exception_analysis", !IO),
+ mercury_compile__maybe_termination(Verbose, Stats, !HLDS, !IO),
+ mercury_compile__maybe_dump_hlds(!.HLDS, 120, "termination", !IO),
+ mercury_compile__maybe_termination2(Verbose, Stats, !HLDS, !IO),
+ mercury_compile__maybe_dump_hlds(!.HLDS, 121, "termination_2", !IO),
+ trans_opt__write_optfile(!.HLDS, !IO).
:- pred mercury_compile__frontend_pass_by_phases(module_info::in,
module_info::out, bool::out, io::di, io::uo) is det.
Index: compiler/term_errors.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_errors.m,v
retrieving revision 1.29
diff -u -r1.29 term_errors.m
--- compiler/term_errors.m 24 Mar 2005 02:00:31 -0000 1.29
+++ compiler/term_errors.m 29 Jun 2005 03:53:24 -0000
@@ -58,16 +58,30 @@
; horder_call
% horder_call
% There is a higher order call at the associated
- % context.
- % Valid in both passes.
+ % context. Valid in both passes.
+ ;
+ method_call
+ % method_call
+ % There is a call to a typeclass method at the associated
+ % context. Valid in both passes.
+ ;
+ aditi_call
+ % There is a call to an Aditi builtin at the associated
+ % context. Valid in both passes.
; inf_termination_const(pred_proc_id, pred_proc_id)
- % inf_termination_const(Caller, Callee, Context)
+ % inf_termination_const(Caller, Callee)
% The call from Caller to Callee at the associated
% context is to a procedure (Callee) whose arg size
% info is set to infinite.
% Valid in both passes.
+ ; ho_inf_termination_const(pred_proc_id, list(pred_proc_id))
+ % ho_inf_termination_const(Caller, Callees).
+ % Caller makes a call to either call/N or apply/N
+ % at the associated context. 'Callees' gives the
+ % possible values of the higher-order argument.
+
; not_subset(pred_proc_id, bag(prog_var), bag(prog_var))
% not_subset(Proc, SupplierVariables, InHeadVariables)
% This error occurs when the bag of active variables
@@ -161,6 +175,8 @@
:- import_module varset.
indirect_error(horder_call).
+indirect_error(method_call).
+indirect_error(aditi_call).
indirect_error(pragma_foreign_code).
indirect_error(imported_pred).
indirect_error(can_loop_proc_called(_, _)).
@@ -288,6 +304,12 @@
term_errors__description(horder_call, _, _, Pieces, no) :-
Pieces = [words("It contains a higher order call.")].
+term_errors__description(method_call, _, _, Pieces, no) :-
+ Pieces = [words("It contains a typeclass method call.")].
+
+term_errors__description(aditi_call, _, _, Pieces, no) :-
+ Pieces = [words("It contains an Aditi builtin call.")].
+
term_errors__description(pragma_foreign_code, _, _, Pieces, no) :-
Pieces = [words("It depends on the properties of"),
words("foreign language code included via a"),
@@ -369,6 +391,22 @@
CalleePPId),
Piece3 = words("which has a termination constant of infinity."),
Pieces = Pieces1 ++ [Piece2] ++ CalleePieces ++ [Piece3].
+
+term_errors__description(ho_inf_termination_const(CallerPPId, _ClosurePPIds),
+ Single, Module, Pieces, no) :-
+ (
+ Single = yes(PPId),
+ require(unify(PPId, CallerPPId), "caller outside this SCC"),
+ Pieces1 = [words("It")]
+ ;
+ Single = no,
+ Pieces1 = describe_one_proc_name(Module, should_module_qualify,
+ CallerPPId)
+ ),
+ Piece2 = words("makes one or more higher-order calls."),
+ Piece3 = words("Each of these higher-order calls has a"),
+ Piece4 = words("termination constant of infinity."),
+ Pieces = Pieces1 ++ [Piece2, Piece3, Piece4].
term_errors__description(not_subset(ProcPPId, OutputSuppliers, HeadVars),
Single, Module, Pieces, no) :-
Index: compiler/term_traversal.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_traversal.m,v
retrieving revision 1.34
diff -u -r1.34 term_traversal.m
--- compiler/term_traversal.m 24 Mar 2005 05:34:16 -0000 1.34
+++ compiler/term_traversal.m 30 Jun 2005 07:48:14 -0000
@@ -226,26 +226,66 @@
Params, !Info)
)
).
-
-traverse_goal_2(generic_call(_, _, _, _), GoalInfo, Params, !Info) :-
- %
- % For class method calls, we could probably analyse further
- % than this, since we know that the method being called must come
- % from one of the instance declarations, and we could potentially
- % (globally) analyse these.
- %
- % Aditi builtins are not guaranteed to terminate
- % - all of them cause the transaction to abort if an error occurs
- % (e.g. if the database server dies).
- % - all except `aditi_insert' execute a user-specified goal
- % which could possibly loop. Analysis of the termination of
- % goals executed bottom-up is not yet implemented.
- %
- % The error message for `generic_call's other than higher-order calls
- % could be better.
- %
+
+traverse_goal_2(generic_call(Details, Args, ArgModes, _), GoalInfo, Params, !Info) :-
goal_info_get_context(GoalInfo, Context),
- add_error(Context, horder_call, Params, !Info).
+ (
+ Details = higher_order(Var, _, _, _),
+ ClosureValueMap = goal_info_get_ho_values(GoalInfo),
+ %
+ % If closure analysis has identified a set of values
+ % this higher-order variable can take, then we can check
+ % if they terminate. We cannot anything about the
+ % size of the arguments of the higher-order call, so
+ % we assume that they are unbounded.
+ %
+ params_get_module_info(Params, Module),
+ ( ClosureValues0 = ClosureValueMap ^ elem(Var) ->
+ ClosureValues = set.to_sorted_list(ClosureValues0),
+ list.filter(terminates(Module), ClosureValues,
+ Terminating, NonTerminating),
+ (
+ NonTerminating = [],
+ partition_call_args(Module, ArgModes, Args,
+ _InVars, OutVars),
+ params_get_ppid(Params, PPId),
+ Error = ho_inf_termination_const(PPId,
+ Terminating),
+ error_if_intersect(OutVars, Context, Error,
+ !Info)
+ ;
+ NonTerminating = [_|_],
+ % XXX We should tell the user what the
+ % non-terminating closures are.
+ add_error(Context, horder_call, Params, !Info)
+ )
+ ;
+ add_error(Context, horder_call, Params, !Info)
+ )
+ ;
+ Details = class_method(_, _, _, _),
+ %
+ % For class method calls, we could probably analyse
+ % further than this, since we know that the method being
+ % called must come from one of the instance
+ % declarations, and we could potentially (globally)
+ % analyse these.
+ %
+ add_error(Context, method_call, Params, !Info)
+ ;
+ Details = unsafe_cast
+ ;
+ Details = aditi_builtin(_, _),
+ %
+ % Aditi builtins are not guaranteed to terminate
+ % - all of them cause the transaction to abort if an error occurs
+ % (e.g. if the database server dies).
+ % - all except `aditi_insert' execute a user-specified goal
+ % which could possibly loop. Analysis of the termination of
+ % goals executed bottom-up is not yet implemented.
+ %
+ add_error(Context, aditi_call, Params, !Info)
+ ).
traverse_goal_2(call(CallPredId, CallProcId, Args, _, _, _),
GoalInfo, Params, !Info) :-
Index: compiler/term_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_util.m,v
retrieving revision 1.41
diff -u -r1.41 term_util.m
--- compiler/term_util.m 7 Apr 2005 06:32:16 -0000 1.41
+++ compiler/term_util.m 29 Jun 2005 03:25:48 -0000
@@ -135,6 +135,12 @@
:- pred attributes_imply_termination(pragma_foreign_proc_attributes::in)
is semidet.
+ % terminates(Module, PPId).
+ % Succeeds iff the procedure given by 'PPId' has been
+ % proven to terminate.
+ %
+:- pred terminates(module_info::in, pred_proc_id::in) is semidet.
+
%-----------------------------------------------------------------------------%
% Convert a prog_data__pragma_termination_info into a
@@ -368,6 +374,13 @@
terminates(Attributes) = depends_on_mercury_calls,
may_call_mercury(Attributes) = will_not_call_mercury
).
+
+%-----------------------------------------------------------------------------%
+
+terminates(Module, PPId) :-
+ module_info_pred_proc_info(Module, PPId, _, ProcInfo),
+ proc_info_get_maybe_termination_info(ProcInfo, TerminationInfo),
+ TerminationInfo = yes(cannot_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