Termination Analysis part 1
Christopher Rodd SPEIRS
crs at students.cs.mu.oz.au
Sat Oct 4 13:19:52 AEST 1997
I sent this last night, but it doesnt seem to have appeared anywhere,
so ill try sending it again. Sorry if anyone receives two copies.
Here is the first installment of the termination analysis, all ready for
Fergus to review.
This is a copy of the 5 files that termination analysis adds to the
compiler, termination.m, term_pass1.m, term_pass2.m, term_util.m and
term_errors.m The second (and last installment) will contain the changes
that have been made to existing code, the log message as well as a new
file, trans_opt.m. A full description of what that file handles will be
given when I post it. You can expect the second installment to come
sometime during the weekend. This version of the compiler is installed
at /home/mercury1/crs/term/mercury
Before I add the files, there is a decision that needs to be made about
the options which control the termination analysis. Currently there are
two options to control termination analysis:
--enable-termination
This option enables the analyser. This means that the compiler
will emit warnings for any predicate which cannot be proved to
terminate and has a check_termination pragma defined on it.
--check-termination
This option implies the --enable-termination option. When this
option is enabled, warnings are emitted for every predicate
which the compiler could not prove to terminate, unless the
proof failed because the analysis is not powerful enough. For
example, warnings are not emitted if termination could not be
proved just because a higher order call was made.
If verbose errors are enabled (-E), then warnings are emitted
for every predicate which could not be proved to terminate.
Unfortunatly, this is often a huge list of errors which are not
very useful, but sometimes it is required.
Now, the questions - Firstly, should we add a
--verbose-termination-errors option? If we do, then should this option
imply the --check-termination option? Also, do we want a shorter form of
--verbose-termination-errors? If so, what? We do currently have short
forms of --check-termination (--chk-term) and --enable-termination
(--enable-term).
Oh well, enough of that, here are the files...
Chris
%-----------------------------------------------------------------------------
%
% Copyright (C) 1997 The University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------
%
% termination.m
% Main author: crs.
%
% This termination analysis is based on the algorithm given by Gerhard Groeger
% and Lutz Plumer in their paper "Handling of Mutual Recursion in Automatic
% Termination Proofs for Logic Programs" which was printed in JICSLP '92
% (the proceedings of the Joint International Conference and Symposium on
% Logic Programming 1992) pages 336 - 350.
%
% Details about this implementation are covered in:
% Chris Speirs, Zoltan Somogyi, and Harald Sondergaard. Termination
% analysis for Mercury. In P. Van Hentenryck, editor, Static Analysis:
% Proceedings of the 4th International Symposium, Lecture Notes in Computer
% Science. Springer, 1997. A more detailed version is available for
% download from http://www.cs.mu.oz.au/publications/tr_db/mu_97_09.ps.gz
%
% Currently, this implementation assumes that all c_code terminates.
% It also fails to prove termination for any predicate that involves higher
% order calls.
%
% The termination analysis may use a number of different norms to calculate
% the size of a term. These are set by using the --termination-norm string
% option. To add a new norm, the following files must be modified:
% globals.m To change the termination_norm type and
% convert_termination_norm predicate.
% handle_options.m To change the error message that is produced when
% an incorrect argument is given to
% --termination-norm.
% term_util.m To change the functor_norm predicate and change the
% functor_alg type.
% termination.m To change the set_functor_info predicate.
%
%-----------------------------------------------------------------------------
:- module termination.
:- interface.
:- import_module io.
:- import_module hlds_module, term_util.
% The top level predicate. This controls all of the termination analysis
:- pred termination__pass(module_info, module_info, io__state, io__state).
:- mode termination__pass(in, out, di, uo) is det.
% This predicate prints out a termination structure.
:- pred termination__out(termination, io__state, io__state).
:- mode termination__out(in, di, uo) is det.
% This predicate prints out the used_args structure
:- pred termination__out_used_args(termination, io__state, io__state).
:- mode termination__out_used_args(in, di, uo) is det.
% This predicate prints out the termination constant
:- pred termination__out_const(termination, io__state, io__state).
:- mode termination__out_const(in, di, uo) is det.
% This predicate prints out whether or not a predicate terminates
% The possible values are: (yes/dont_know/not_set).
:- pred termination__out_terminates(termination, io__state, io__state).
:- mode termination__out_terminates(in, di, uo) is det.
% This predicate outputs termination_info pragmas which are used in .trans_opt
% and .opt files.
:- pred termination__output_pragma_termination_info(pred_or_func, sym_name,
list(mode), termination, term__context, io__state, io__state).
:- mode termination__output_pragma_termination_info(in, in, in, in, in,
di, uo) is det.
%----------------------------------------------------------------------------%
:- implementation.
:- import_module map, std_util, bool, int, char, string, relation.
:- import_module list, require, bag, set, term.
:- import_module inst_match, passes_aux, options, globals, prog_data.
:- import_module hlds_data, hlds_pred, hlds_goal, dependency_graph.
:- import_module mode_util, hlds_out, code_util, prog_out.
:- import_module mercury_to_mercury, varset, type_util, special_pred.
:- import_module term_pass1, term_pass2, term_errors.
%-----------------------------------------------------------------------------%
termination__pass(Module0, Module) -->
globals__io_lookup_bool_option(verbose, Verbose),
globals__io_get_termination_norm(TermNorm),
maybe_write_string(Verbose, "% Checking termination...\n"),
{ module_info_ensure_dependency_info(Module0, Module1) },
{ module_info_predids(Module1, PredIds) },
% Process builtin predicates.
check_preds(PredIds, Module1, Module2),
% Find the functor_info.
{ set_functor_info(TermNorm, Module2, FunctorInfo) },
proc_inequalities(Module2, FunctorInfo, Module3),
termination(Module3, FunctorInfo, Module),
globals__io_lookup_bool_option(make_optimization_interface,
MakeOptInt),
( { MakeOptInt = yes } ->
termination__make_opt_int(PredIds, Module)
;
[]
),
maybe_write_string(Verbose, "% Termination checking done.\n").
% This predicate sets the functor info depending on the value of the
% termination_norm option. The functor info field stores the weight which
% is associated with each functor, and may contain information about which
% subterms contribute to the size of that functor.
:- pred set_functor_info(globals__termination_norm, module_info, functor_info).
:- mode set_functor_info(in, in, out) is det.
set_functor_info(total, _Module, total).
set_functor_info(simple, _Module, simple).
set_functor_info(num_data_elems, Module, use_map_and_args(WeightMap)) :-
find_weights(Module, WeightMap).
set_functor_info(size_data_elems, Module, use_map(WeightMap)) :-
find_weights(Module, WeightMap).
%-----------------------------------------------------------------------------%
% These termination__out* predicates are used to print out the
% termination_info pragmas. If they are changed, then prog_io_pragma.m
% must also be changed so that it can parse the resulting pragma
% termination_info declarations.
% XXX could these predicates be replaced by calls to io__write?
termination__out(Termination) -->
termination__out_terminates(Termination),
io__write_string("("),
termination__out_const(Termination),
io__write_string(")").
termination__out_used_args(term(_Const, _Term, MaybeUsedArgs, _)) -->
(
{ MaybeUsedArgs = yes([]) },
io__write_string("yes([])")
;
{ MaybeUsedArgs = yes([UsedArg | UsedArgs]) },
io__write_string("yes([ "),
io__write(UsedArg),
termination__out_used_args_2(UsedArgs),
io__write_string(" ])")
;
{ MaybeUsedArgs = no },
io__write_string("no")
).
:- pred termination__out_used_args_2(list(bool), io__state, io__state).
:- mode termination__out_used_args_2(in, di, uo) is det.
termination__out_used_args_2([]) --> [].
termination__out_used_args_2([ UsedArg | UsedArgs ]) -->
io__write_string(", "),
io__write(UsedArg),
termination__out_used_args_2(UsedArgs).
termination__out_terminates(term(_, Term, _, _)) -->
termination__out_terminates_2(Term).
:- pred termination__out_terminates_2(terminates, io__state, io__state).
:- mode termination__out_terminates_2(in, di, uo) is det.
termination__out_terminates_2(not_set) -->
io__write_string("not_set").
termination__out_terminates_2(dont_know) -->
io__write_string("dont_know").
termination__out_terminates_2(yes) -->
io__write_string("yes").
termination__out_const(term(Const, _, _, _)) -->
termination__out_const_2(Const).
:- pred termination__out_const_2(term_util__constant, io__state, io__state).
:- mode termination__out_const_2(in, di, uo) is det.
termination__out_const_2(inf(_)) -->
io__write_string("infinite").
termination__out_const_2(not_set) -->
io__write_string("not_set").
termination__out_const_2(set(Int)) -->
io__write_string("set("),
io__write_int(Int),
io__write_string(")").
termination__output_pragma_termination_info(PredOrFunc, SymName,
ModeList, Termination, Context) -->
io__write_string(":- pragma termination_info("),
{ varset__init(InitVarSet) },
(
{ PredOrFunc = predicate },
mercury_output_pred_mode_subdecl(InitVarSet, SymName,
ModeList, no, Context)
;
{ PredOrFunc = function },
{ pred_args_to_func_args(ModeList, FuncModeList, RetMode) },
mercury_output_func_mode_subdecl(InitVarSet, SymName,
FuncModeList, RetMode, no, Context)
),
io__write_string(", "),
termination__out_const(Termination),
io__write_string(", "),
termination__out_terminates(Termination),
io__write_string(", "),
termination__out_used_args(Termination),
io__write_string(").\n").
%-----------------------------------------------------------------------------%
:- pred check_preds(list(pred_id), module_info, module_info,
io__state, io__state).
:- mode check_preds(in, in, out, di, uo) is det.
% This predicate processes each predicate and sets the termination property
% if possible. This is done as follows: Set the termination to yes if:
% - there is a terminates pragma defined for the predicate
% - there is a `check_termination' pragma defined for the predicate, and it
% is imported, and the compiler is not currently generating the
% intermodule optimization file.
% - the predicate is a builtin predicate or is compiler generated (This
% also sets the termination constant and UsedArgs).
%
% Set the termination to dont_know if:
% - there is a `does_not_terminate' pragma defined for this predicate.
% - the predicate is imported and there is no other source of information
% about it (termination_info pragmas, terminates pragmas,
% check_termination pragmas, builtin/compiler generated).
check_preds([], Module, Module, State, State).
check_preds([PredId | PredIds] , Module0, Module, State0, State) :-
globals__io_lookup_bool_option(make_optimization_interface,
MakeOptInt, State0, State1),
module_info_preds(Module0, PredTable0),
map__lookup(PredTable0, PredId, PredInfo0),
pred_info_import_status(PredInfo0, ImportStatus),
pred_info_context(PredInfo0, Context),
pred_info_procedures(PredInfo0, ProcTable0),
pred_info_get_marker_list(PredInfo0, Markers),
map__keys(ProcTable0, ProcIds),
(
% It is possible for compiler generated/mercury builtin
% predicates to be imported or locally defined, so they
% must be covered here, seperatly.
set_compiler_gen_terminates(ProcIds, PredInfo0,
Module0, ProcTable0, ProcTable1)
->
ProcTable2 = ProcTable1
; % else if
( ImportStatus = exported
; ImportStatus = local
; ImportStatus = pseudo_exported
)
->
( list__member(request(terminates), Markers) ->
MaybeFind = no,
ReplaceTerminate = yes,
MaybeError = no,
change_procs_terminate(ProcIds, MaybeFind,
ReplaceTerminate, MaybeError,
ProcTable0, ProcTable2)
;
ProcTable2 = ProcTable0
)
; %else if
( ImportStatus = imported
; ImportStatus = opt_imported
; ImportStatus = pseudo_imported % should this be here?
)
->
% All of the predicates that are processed in this section
% are imported in some way.
% With imported predicates, any 'check_termination'
% pragmas will be checked by the compiler when it compiles
% the relevant source file (that the predicate was imported
% from). When making the intermodule optimizations, the
% check_termination will not be checked when the relevant
% source file is compiled, so it cannot be depended upon.
(
(
list__member(request(terminates), Markers)
;
MakeOptInt = no,
list__member(request(check_termination), Markers)
)
->
change_procs_terminate(ProcIds, no, yes, no,
ProcTable0, ProcTable1)
;
% go through, changing each 'not_set' to 'dont_know'
MaybeFind = yes(not_set),
ReplaceTerminate = dont_know,
MaybeError = yes(Context - imported_pred),
change_procs_terminate(ProcIds, MaybeFind,
ReplaceTerminate, MaybeError, ProcTable0,
ProcTable1)
),
MaybeFindConst = yes(not_set),
ConstError = imported_pred,
ReplaceConst = inf(Context - ConstError),
change_procs_const(ProcIds, MaybeFindConst, ReplaceConst,
ProcTable1, ProcTable2)
;
% ( ImportStatus = abstract_imported
% ; ImportStatus = abstract_exported
% ),
% This should not happen, as procedures are being processed
% here, and these import_status' refer to abstract types.
error("termination__check_preds: Unexpected import status of a predicate")
),
( list__member(request(does_not_terminate), Markers) ->
MaybeFind1 = no,
ReplaceTerminate1 = dont_know,
MaybeError1 = yes(Context - does_not_term_pragma(PredId)),
change_procs_terminate(ProcIds, MaybeFind1,
ReplaceTerminate1, MaybeError1, ProcTable2, ProcTable)
;
ProcTable = ProcTable2
),
pred_info_set_procedures(PredInfo0, ProcTable, PredInfo),
map__set(PredTable0, PredId, PredInfo, PredTable),
module_info_set_preds(Module0, PredTable, Module1),
check_preds(PredIds, Module1, Module, State1, State).
% This predicate checks each ProcId in the list to see if it is a compiler
% generated predicate, or a mercury_builtin predicate. If it is, then the
% compiler sets the termination property of the ProcIds accordingly.
:- pred set_compiler_gen_terminates(list(proc_id), pred_info, module_info,
proc_table, proc_table).
:- mode set_compiler_gen_terminates(in, in, in, in, out) is semidet.
set_compiler_gen_terminates([], _PredInfo, _Module, ProcTable, ProcTable).
set_compiler_gen_terminates([ ProcId | ProcIds ], PredInfo, Module,
ProcTable0, ProcTable) :-
( code_util__predinfo_is_builtin(PredInfo) ->
set_builtin_terminates([ ProcId | ProcIds ], PredInfo,
Module, ProcTable0, ProcTable)
;
pred_info_name(PredInfo, Name),
pred_info_arity(PredInfo, Arity),
(
special_pred_name_arity(SpecPredId0, Name, _, Arity),
pred_info_module(PredInfo, ModuleName),
ModuleName = "mercury_builtin"
->
SpecialPredId = SpecPredId0
;
special_pred_name_arity(SpecialPredId, _, Name, Arity)
),
map__lookup(ProcTable0, ProcId, ProcInfo0),
proc_info_headvars(ProcInfo0, HeadVars),
termination__special_pred_id_to_termination(SpecialPredId,
HeadVars, Termination),
% The procedure is a compiler generated procedure, so enter the
% data in the proc_info.
proc_info_set_termination(ProcInfo0, Termination, ProcInfo),
map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable1),
set_compiler_gen_terminates(ProcIds, PredInfo, Module,
ProcTable1, ProcTable)
).
:- pred termination__special_pred_id_to_termination(special_pred_id,
list(var), termination).
:- mode termination__special_pred_id_to_termination(in, in, out) is det.
termination__special_pred_id_to_termination(compare, HeadVars, Termination) :-
term_util__make_bool_list(HeadVars, [no, no, no], OutList),
Termination = term(set(0), yes, yes(OutList), no).
termination__special_pred_id_to_termination(unify, HeadVars, Termination) :-
term_util__make_bool_list(HeadVars, [yes, yes], OutList),
Termination = term(set(0), yes, yes(OutList), no).
termination__special_pred_id_to_termination(index, HeadVars, Termination) :-
term_util__make_bool_list(HeadVars, [no, no], OutList),
Termination = term(set(0), yes, yes(OutList), no).
% The list of proc_ids must refer to builtin predicates. This predicate
% sets the termination information of builtin predicates.
:- pred set_builtin_terminates(list(proc_id), pred_info, module_info,
proc_table, proc_table).
:- mode set_builtin_terminates(in, in, in, in, out) is det.
set_builtin_terminates([], _, _, ProcTable, ProcTable).
set_builtin_terminates([ProcId | ProcIds], PredInfo, Module, ProcTable0,
ProcTable) :-
map__lookup(ProcTable0, ProcId, ProcInfo0),
( attempt_set_proc_const(Module, PredInfo, ProcInfo0) ->
% For attempt_set_proc_const to succeed on a procedure, the
% output variables of that procedure must all be of a type
% whose norm will be zero. Hence the size of the output
% variables will all be 0, independent of the size of the
% input variables. Therefore, as the size of the output
% variables do not depend on the size of the input
% variables, UsedArgs should be set to yes([no, no, ...]).
Const = set(0),
proc_info_headvars(ProcInfo0, HeadVars),
term_util__make_bool_list(HeadVars, [], Bools),
UsedArgs = yes(Bools)
;
pred_info_context(PredInfo, Context),
Const = inf(Context - is_builtin),
UsedArgs = no
),
Term = term(Const, yes, UsedArgs, no),
proc_info_set_termination(ProcInfo0, Term, ProcInfo),
map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable1),
set_builtin_terminates(ProcIds, PredInfo, Module, ProcTable1,
ProcTable).
% For attempt_set_proc_const to succeed, the output variables of
% that procedure must all be of a type that will always have a norm of 0.
% Hence the size of the output vars will always be 0, independent of the
% size of the input variables. Therefore, if attempt_set_proc_const
% succeeds on a predicate, then the termination constant of that predicate
% can be set to 0, independantly of what the predicate does.
:- pred attempt_set_proc_const(module_info, pred_info, proc_info).
:- mode attempt_set_proc_const(in, in, in) is semidet.
attempt_set_proc_const(Module, PredInfo, ProcInfo) :-
pred_info_arg_types(PredInfo, _, TypeList),
proc_info_argmodes(ProcInfo, ModeList),
attempt_set_proc_const_2(TypeList, ModeList, Module).
:- pred attempt_set_proc_const_2(list(type), list(mode), module_info).
:- mode attempt_set_proc_const_2(in, in, in) is semidet.
attempt_set_proc_const_2([], [], _).
attempt_set_proc_const_2([], [_|_], _) :-
error("termination__attempt_set_proc_const_2: Unmatched variables.").
attempt_set_proc_const_2([_|_], [], _) :-
error("termination:attempt_set_proc_const_2: Unmatched variables").
attempt_set_proc_const_2([Type | Types], [Mode | Modes], Module) :-
( mode_is_input(Module, Mode) ->
% The variable is an input variables, so its size is
% irrelevant.
attempt_set_proc_const_2(Types, Modes, Module)
;
classify_type(Type, Module, TypeCategory),
% User_type could be a type_info, which should be called
% size 0. This is not a big problem, as most type_infos
% are input.
TypeCategory \= user_type(_),
% This could be changed, by looking up the polymorphic type,
% and seeing if it is recursive, or could it?
TypeCategory \= polymorphic_type,
TypeCategory \= pred_type,
attempt_set_proc_const_2(Types, Modes, Module)
).
% This predicate changes the terminate property of a list of procedures.
% change_procs_terminate(ProcList,MaybeFind, Replace, MaybeError,
% ProcTable, ProcTable).
% If MaybeFind is no, then this predicate changes the terminates and
% MaybeError field of all the procedures passed to it. If MaybeFind is set
% to yes(OldTerminates) then the terminates and MaybeError field of a
% procedure is only changed if the Terminates field was OldTerminates.
:- pred change_procs_terminate(list(proc_id), maybe(terminates), terminates,
maybe(term_errors__error), proc_table, proc_table).
:- mode change_procs_terminate(in, in, in, in, in, out) is det.
change_procs_terminate([], _Find, _Replace, _, ProcTable, ProcTable).
change_procs_terminate([ProcId | ProcIds], MaybeFind, Replace, MaybeError,
ProcTable0, ProcTable) :-
map__lookup(ProcTable0, ProcId, ProcInfo0),
proc_info_termination(ProcInfo0, Termination),
(
Termination = term(Const, Terminates, UsedArgs, _Error),
(
MaybeFind = yes(Terminates)
;
MaybeFind = no
)
->
Termination1 = term(Const, Replace, UsedArgs, MaybeError),
proc_info_set_termination(ProcInfo0, Termination1, ProcInfo),
map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable1)
;
ProcTable1 = ProcTable0
),
change_procs_terminate(ProcIds, MaybeFind, Replace, MaybeError,
ProcTable1, ProcTable).
% This predicate changes the termination constant of a list of procedures.
% change_procs_const(ProcList,MaybeFind, Replace, ProcTable, ProcTable).
% If MaybeFind is no, then this predicate changes the constant
% field of all the procedures passed to it. If MaybeFind is set
% to yes(OldConst) then the termination constant of a procedure is
% only changed if the Constant field was OldConst.
:- pred change_procs_const(list(proc_id), maybe(term_util__constant),
term_util__constant, proc_table, proc_table).
:- mode change_procs_const(in, in, in, in, out) is det.
change_procs_const([], _Find, _Replace, ProcTable, ProcTable).
change_procs_const([ProcId | ProcIds], MaybeFind, Replace, ProcTable0,
ProcTable) :-
map__lookup(ProcTable0, ProcId, ProcInfo0),
proc_info_termination(ProcInfo0, Termination),
(
Termination = term(Const, Term, UsedArgs, MaybeError),
(
MaybeFind = yes(Const)
;
MaybeFind = no
)
->
Termination1 = term(Replace, Term, UsedArgs, MaybeError),
proc_info_set_termination(ProcInfo0, Termination1, ProcInfo),
map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable1)
;
ProcTable1 = ProcTable0
),
change_procs_const(ProcIds, MaybeFind, Replace, ProcTable1, ProcTable).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
% These predicates are used to add the termination_info pragmas to the .opt
% file. It is oftern better to use the .trans_opt file, as it gives
% much better accuracy. The two files are not mutually exclusive, and
% termination information may be stored in both.
:- pred termination__make_opt_int(list(pred_id), module_info, io__state,
io__state).
:- mode termination__make_opt_int(in, in, di, uo) is det.
termination__make_opt_int(PredIds, Module) -->
{ module_info_name(Module, ModuleName) },
{ string__append(ModuleName, ".opt", OptFileName) },
io__open_append(OptFileName, OptFileRes),
( { OptFileRes = ok(OptFile) } ->
io__set_output_stream(OptFile, OldStream),
termination__make_opt_int_preds(PredIds, Module),
io__set_output_stream(OldStream, _),
io__close_output(OptFile)
;
% failed to open the .opt file for processing
io__write_strings(["Cannot open `",
OptFileName, "' for output\n"]),
io__set_exit_status(1)
).
:- pred termination__make_opt_int_preds(list(pred_id), module_info,
io__state, io__state).
:- mode termination__make_opt_int_preds(in, in, di, uo) is det.
termination__make_opt_int_preds([], _Module) --> [].
termination__make_opt_int_preds([ PredId | PredIds ], Module) -->
{ module_info_preds(Module, PredTable) },
{ map__lookup(PredTable, PredId, PredInfo) },
{ pred_info_import_status(PredInfo, ImportStatus) },
(
{ ImportStatus = exported },
{ \+ code_util__compiler_generated(PredInfo) }
->
{ pred_info_name(PredInfo, PredName) },
{ pred_info_procedures(PredInfo, ProcTable) },
{ pred_info_procids(PredInfo, ProcIds) },
{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
{ pred_info_module(PredInfo, ModuleName) },
{ pred_info_context(PredInfo, Context) },
{ SymName = qualified(ModuleName, PredName) },
termination__make_opt_int_procs(PredId, ProcIds, ProcTable,
PredOrFunc, SymName, Context)
;
[]
),
termination__make_opt_int_preds(PredIds, Module).
:- pred termination__make_opt_int_procs(pred_id, list(proc_id), proc_table,
pred_or_func, sym_name, term__context, io__state, io__state).
:- mode termination__make_opt_int_procs(in, in, in, in, in, in, di, uo) is det.
termination__make_opt_int_procs(_PredId, [], _, _, _, _) --> [].
termination__make_opt_int_procs(PredId, [ ProcId | ProcIds ], ProcTable,
PredOrFunc, SymName, Context) -->
{ map__lookup(ProcTable, ProcId, ProcInfo) },
{ proc_info_termination(ProcInfo, Termination) },
{ proc_info_declared_argmodes(ProcInfo, ModeList) },
termination__output_pragma_termination_info(PredOrFunc, SymName,
ModeList, Termination, Context),
termination__make_opt_int_procs(PredId, ProcIds, ProcTable,
PredOrFunc, SymName, Context).
%-----------------------------------------------------------------------------
%
% Copyright (C) 1997 The University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------
%
% term_pass1.m
% Main author: crs.
%
% This file contains the first pass of the termination analysis.
% It sets the termination constant for all procedures, and also sets the
% terminates value for some procedures. (eg if the predicate contains higher
% order arguments or calls.)
%
% The first pass processes each SCC in turn, following the dependency
% ordering given by hlds_dependency_info_get_dependency_ordering/2.
% The termination constant is set by first generating a list of
% constraints. This list of constraints will contain one variable for each
% procedure in the SCC that is currently being processed. After the
% complete set of constraints have been created, they are then solved using
% lp_solve. As there is a single variable associated with each procedure,
% each variable is named using the pred_proc_id of the relevant procedure.
% Therefore, in some places in the program (eg term_pass1__equation), the
% pred_proc_id is actually referring to the variable associated with that
% procedure which still needs to be solved.
%
%-----------------------------------------------------------------------------
%
:- module term_pass1.
:- interface.
:- import_module io, hlds_module, term_util.
% This is the top level predicate of term_pass1. It processes all of the
% procedures in the module, and sets the termination constant of each of
% them. The procedures are processed in the order given by
% hlds_dependency_info_get_dependency_ordering. The results of the
% analysis are stored in the termination subterm of the proc_info
% structure.
:- pred proc_inequalities(module_info, functor_info, module_info,
io__state, io__state).
:- mode proc_inequalities(in, in, out, di, uo) is det.
%------------------------------------------------------------------------------
:- implementation.
:- import_module int, list, bag, require, bool, std_util, char, map, string.
:- import_module hlds_pred, hlds_goal, hlds_data.
:- import_module term_errors, mode_util, type_util, term.
%------------------------------------------------------------------------------
% This section contains proc_inequalities and its supporting functions.
% proc_inequalities goes through the dependency ordering, applying
% proc_inequalities to each SCC in turn. proc_inequalities returns a set of
% constraints which are then solved using lp_solve.
% term_pass1__equation stores a single constraint.
% The constraint is of the form:
% pred_proc_id - list(pred_proc_id) >= term_util__constant
% Where pred_proc_id represents a variable which relates the total size of
% the input variables to the total size of the output variables. For
% details of what these constraints mean, please refer to one of the papers
% listed at the start of termination.m.
:- type term_pass1__equation
---> eqn(term_util__constant, pred_proc_id, list(pred_proc_id)).
:- type used_args == map(pred_proc_id, list(bool)).
proc_inequalities(Module0, FunctorInfo, Module) -->
{ module_info_dependency_info(Module0, DependencyInfo) },
{ hlds_dependency_info_get_dependency_ordering(DependencyInfo,
DependOrdering) },
proc_inequalities_module(Module0, DependOrdering, FunctorInfo, Module).
:- pred proc_inequalities_module(module_info, dependency_ordering, functor_info,
module_info, io__state, io__state).
:- mode proc_inequalities_module(in, in, in, out, di, uo) is det.
proc_inequalities_module(Module, [], _FunctorInfo, Module) --> [].
proc_inequalities_module(Module0, [ SCC | SCCs ], FunctorInfo, Module) -->
{ init_used_args(Module0, SCC, InitUsedArgs) },
proc_inequalities_scc(Module0, SCC, FunctorInfo, SCC - InitUsedArgs,
InitUsedArgs, [], Module2),
proc_inequalities_module(Module2, SCCs, FunctorInfo, Module).
:- pred proc_inequalities_scc(module_info, list(pred_proc_id), functor_info,
pair(list(pred_proc_id), used_args), used_args,
list(term_pass1__equation), module_info, io__state, io__state).
:- mode proc_inequalities_scc(in, in, in, in, in, in, out, di, uo) is det.
proc_inequalities_scc(Module0, [], FunctorInfo, SCC - OldUsedArgs,
NewUsedArgs, Offs0, Module) -->
% First check used_args. If a fixed point has been reached, then
% continue with the analysis and solve the resulting constraints.
% If a fixed point has not been reached, then recurse on the new
% used args.
% XXX is it valid to compare maps using equality?
( { OldUsedArgs = NewUsedArgs } ->
% A fixed point has been reached. So process the
% constraints that have been created.
% Solve the equations that have been created.
{ proc_inequalities_scc_remove_useless_offsets(Offs0, Module0,
Offs, Res) },
% XXX what is the correct context to use when referring to
% a whole SCC?
( { SCC = [proc(PredId, _)] } ->
{ module_info_pred_info(Module0, PredId, PredInfo) },
{ pred_info_context(PredInfo, Context) }
;
{ term__context_init(Context) }
),
( { Res = error(Error) } ->
% There is a directly recursive call where the
% variables grow between the head and recursive
% call. Therefore the output is infinitly larger
% than the input.
% e.g. foo(A) :- foo([1|A]).
{ set_pred_proc_ids_const(SCC, inf(Error), Module0,
Module) }
; { Offs = [] } ->
% There are no equations in this SCC
% This has 2 possible causes. If the predicate has
% no output arguments, then the relative size of
% input and output arguments is undefined. If
% there are no output arguments, then there will be
% no equations created. The other possibility is
% that the procedure is a builtin predicate, which
% has an empty body.
{ NewConst = inf(Context - no_eqns) },
{ set_pred_proc_ids_const(SCC, NewConst,
Module0, Module) }
;
solve_equations(Module0, Offs, SCC, NewUsedArgs,
Context, Module)
)
;
% The analysis has not reached a fixed point, so recurse.
proc_inequalities_scc(Module0, SCC, FunctorInfo,
SCC - NewUsedArgs, NewUsedArgs, [], Module)
).
proc_inequalities_scc(Module0, [PPId | PPIds], FunctorInfo,
SCC - OldUsedArgsMap, UsedArgsMap0, Offs0, Module) -->
{ PPId = proc(PredId, ProcId) },
{ module_info_pred_proc_info(Module0, PredId, ProcId, _PredInfo,
ProcInfo) },
{ proc_info_termination(ProcInfo, Termination) },
( { Termination = term(not_set, _, _, _) } ->
{ proc_inequalities_pred(Module0, PredId, ProcId, FunctorInfo,
Offs1, Res, OldUsedArgsMap, NewUsedArgs) },
(
{ Res = error(Error) },
% proc_inequalities failed, so set all the
% termination constants to infinity.
{ set_pred_proc_ids_const(SCC, inf(Error),
Module0, Module2) },
% If the error detected guarantees that the
% analysis will not be able to prove termination,
% then we may as well set the termination property
% to dont_know, and save time in the second stage.
(
{ ( Error = _Context - horder_call
; Error = _Context - horder_args(_, _)
; Error = _ - dont_know_proc_called(_, _)
) }
->
do_ppid_check_terminates(SCC, Error,
Module2, Module)
;
{ Module = Module2 }
)
;
{ Res = ok },
{ list__append(Offs0, Offs1, Offs) },
{ map__det_update(UsedArgsMap0, PPId, NewUsedArgs,
UsedArgsMap) },
proc_inequalities_scc(Module0, PPIds, FunctorInfo,
SCC - OldUsedArgsMap,
UsedArgsMap, Offs, Module)
)
;
% The termination constant has already been set - hopefully
% this is true of all the procedures in this SCC. Perhaps
% it would be wise to add a check that this is the case.
{ Module = Module0 }
).
% This procedure removes offsets where there are no variables in the offset.
% It would be nice if lp_solve would accept constraints of the form
% (0 >= -1), but it doesnt so they need to be removed manually, which is
% what this procedure does. If this procedure returns an error then the
% constraints are unsatisfiable (0 >= 1). If the return value is `ok' the
% the constraints that were removed were all satisfiable.
:- pred proc_inequalities_scc_remove_useless_offsets(
list(term_pass1__equation), module_info, list(term_pass1__equation),
term_util__result(term_errors__error)).
:- mode proc_inequalities_scc_remove_useless_offsets(in, in, out, out) is det.
proc_inequalities_scc_remove_useless_offsets([], _Module, [], ok).
proc_inequalities_scc_remove_useless_offsets([ Off0 | Offs0 ], Module,
Offs, Res) :-
( Off0 = eqn(Const, PPId, [ PPId ]) ->
% in this case there is direct recursion
(
(
Const = set(Int),
Int > 0
;
Const = inf(_)
)
->
% In this case the recursive call is with larger
% variables. Hence the output could be unbounded
PPId = proc(PredId, _ProcId),
module_info_pred_info(Module, PredId, PredInfo),
pred_info_context(PredInfo, Context),
Res = error(Context - positive_value(PPId, PPId)),
Offs = Offs0
;
proc_inequalities_scc_remove_useless_offsets(Offs0,
Module, Offs, Res)
)
;
proc_inequalities_scc_remove_useless_offsets(Offs0, Module,
Offs1, Res),
Offs = [ Off0 | Offs1]
).
% This predicate takes the results from solve_equations (if it successfully
% solved the constraints), and inserts these results into the
% predicate_table.
:- pred proc_inequalities_set_module(list(pair(pred_proc_id, int)),
used_args, pred_table, pred_table).
:- mode proc_inequalities_set_module(in, in, in, out) is det.
proc_inequalities_set_module([], _, PredTable, PredTable).
proc_inequalities_set_module([ Soln | Solns ], UsedArgsMap,
PredTable0, PredTable) :-
Soln = PPId - Int,
Const = set(Int),
PPId = proc(PredId, ProcId),
map__lookup(PredTable0, PredId, PredInfo),
pred_info_procedures(PredInfo, ProcTable),
map__lookup(ProcTable, ProcId, ProcInfo),
map__lookup(UsedArgsMap, PPId, UsedArgs),
proc_info_termination(ProcInfo, term(Const0, B, _, D)),
( Const0 = not_set ->
proc_info_set_termination(ProcInfo,
term(Const, B, yes(UsedArgs), D), ProcInfo1)
;
% This can only happen if an imported pred was in the same
% SCC as some local preds, or if somehow some equations
% were made for an imported pred. Both of these occurances
% represent an error in the code.
error("term_pass1__proc_inequalities_set_module: Error"),
ProcInfo1 = ProcInfo
),
map__set(ProcTable, ProcId, ProcInfo1, ProcTable1),
pred_info_set_procedures(PredInfo, ProcTable1, PredInfo1),
map__set(PredTable0, PredId, PredInfo1, PredTable1),
proc_inequalities_set_module(Solns, UsedArgsMap,PredTable1, PredTable).
% Used to initialise the used_args map. Initially, all arguments are
% considered to be unused.
:- pred init_used_args(module_info, list(pred_proc_id), used_args).
:- mode init_used_args(in, in, out) is det.
init_used_args(_Module, [], InitMap) :-
map__init(InitMap).
init_used_args(Module, [PPId | PPIds], Out) :-
init_used_args(Module, PPIds, Out0),
PPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
proc_info_headvars(ProcInfo, HeadVars),
term_util__make_bool_list(HeadVars, [], BoolList),
map__det_insert(Out0, PPId, BoolList, Out).
% Used to insert the information in the used_args map into the pred_table.
:- pred set_used_args(pred_table, list(pred_proc_id), used_args, pred_table).
:- mode set_used_args(in, in, in, out) is det.
set_used_args(PredTable, [], _, PredTable).
set_used_args(PredTable0, [PPId | PPIds], UsedArgsMap, PredTable) :-
PPId = proc(PredId, ProcId),
map__lookup(PredTable0, PredId, PredInfo0),
pred_info_procedures(PredInfo0, ProcTable0),
map__lookup(ProcTable0, ProcId, ProcInfo0),
proc_info_termination(ProcInfo0, Term0),
map__lookup(UsedArgsMap, PPId, UsedArgs),
Term0 = term(Const, Terminates, _UsedArgs, MaybeError),
Term = term(Const, Terminates, yes(UsedArgs), MaybeError),
proc_info_set_termination(ProcInfo0, Term, ProcInfo),
map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable),
pred_info_set_procedures(PredInfo0, ProcTable, PredInfo),
map__det_update(PredTable0, PredId, PredInfo, PredTable1),
set_used_args(PredTable1, PPIds, UsedArgsMap, PredTable).
%-----------------------------------------------------------------------------%
% This section contains proc_inequalities_pred and its supporting functions.
% proc_inequalities_pred processes a predicate, and forms a set of
% inequalities relating the size of that predicates inputs to the size of
% the outputs. proc_inequalities_goal processes a goal, and finds an
% inequality relating the sizeof(input arguments) to the sizeof(output
% arguments). If it finds a valid inequality, then it returns the offset
% of the inequality (with Res set to ok). If no inequality can be found,
% then proc_inequalities_pred returns Res = error().
:- type proc_inequalities_equ == list(pair(term_pass1__equation, bag(var))).
:- type proc_inequalities_info == pair(unify_info, used_args).
% proc_inequalities_info == UnifyInfo - CallInfo
:- pred proc_inequalities_pred(module_info, pred_id, proc_id, functor_info,
list(term_pass1__equation), term_util__result(term_errors__error),
used_args, list(bool)).
:- mode proc_inequalities_pred(in, in, in, in, out, out, in, out) is det.
proc_inequalities_pred(Module, PredId, ProcId, FunctorInfo, Offs, Res,
OldUsedArgsMap, NewUsedArgs):-
module_info_pred_proc_info(Module, PredId, ProcId, PredInfo, ProcInfo),
proc_info_headvars(ProcInfo, Args),
proc_info_argmodes(ProcInfo, ArgModes),
proc_info_vartypes(ProcInfo, VarTypes),
proc_info_goal(ProcInfo, GoalExpr - GoalInfo),
partition_call_args(Module, ArgModes, Args, InVars, OutVars),
bag__from_list(InVars, InVarsBag),
bag__from_list(OutVars, OutVarsBag),
PPId = proc(PredId, ProcId),
InitEqn = eqn(set(0), PPId, []),
UnifyInfo = VarTypes - FunctorInfo,
CallInfo = OldUsedArgsMap,
Info = UnifyInfo - CallInfo,
proc_inequalities_goal(GoalExpr, GoalInfo, Module, Info, PPId,
Res1, [ InitEqn - OutVarsBag ], OffsVars),
split_offs_vars(OffsVars, Offs, InVars2Bag),
( Res1 = ok ->
( bag__is_subbag(InVars2Bag, InVarsBag) ->
map__lookup(OldUsedArgsMap, PPId, OldUsedArgs),
proc_inequalities_used_args(Args, InVars2Bag,
OldUsedArgs, NewUsedArgs),
Res = ok
;
pred_info_context(PredInfo, Context),
% If Res is error(), then The Used Args should not
% matter
NewUsedArgs = [],
Res = error(Context -
not_subset(PPId, InVars2Bag, InVarsBag))
)
;
NewUsedArgs = [],
Res = Res1
).
:- pred proc_inequalities_used_args(list(var), bag(var), list(bool), list(bool)).
:- mode proc_inequalities_used_args(in, in, in, out) is det.
proc_inequalities_used_args([], _InVarsBag, [], []).
proc_inequalities_used_args([_ | _], _InVarsBag, [], []) :-
error("term_pass1__proc_inequalities_used_args: Unmatched variables").
proc_inequalities_used_args([], _InVarsBag, [_ | _], []) :-
error("term_pass1:proc_inequalities_used_args: Unmatched variables").
proc_inequalities_used_args([ Arg | Args ], InVarsBag,
[ OldUsedArg | OldUsedArgs ], [ UsedArg | UsedArgs ]):-
( bag__contains(InVarsBag, Arg) ->
UsedArg = yes
;
UsedArg = OldUsedArg % This guarantees monotonicity
),
proc_inequalities_used_args(Args, InVarsBag, OldUsedArgs, UsedArgs).
% proc_inequalities_goal fails (returns Result = error()) if it cannot form an
% inequality. i.e. if there are higher order calls, higher order
% arguments, or pragma-c-code with relevent output variables. The reason
% for checking for higher order arguments is that this traps calls to
% solutions, which would not otherwise be checked.
:- pred proc_inequalities_goal(hlds_goal_expr, hlds_goal_info, module_info,
proc_inequalities_info, pred_proc_id,
term_util__result(term_errors__error),
proc_inequalities_equ, proc_inequalities_equ).
:- mode proc_inequalities_goal(in, in, in, in, in, out, in, out) is det.
proc_inequalities_goal(conj([]), _, _Module, _, _PPId, ok, Offs, Offs).
proc_inequalities_goal(conj([ Goal | Goals ]), GoalInfo, Module, Info,
PPId, Res, Offs0, Offs) :-
( goal_will_fail(GoalInfo) ->
Res = ok,
Offs = []
;
proc_inequalities_conj(Goal, Goals, Module, Info, PPId,
Res, Offs0, Offs)
).
% This clause fails (returns Res=error()) if:
% The called predicate contains higher order arguments
% The terminates value of the called predicate is 'dont_know'
% The termination constant of the called predicate is infinite
proc_inequalities_goal(call(CallPredId, CallProcId, Args, _IsBuiltin, _, _SymName),
GoalInfo, Module, Info, PPId, Res, Offs0, Offs) :-
module_info_pred_proc_info(Module, CallPredId,
CallProcId, _CallPredInfo, CallProcInfo),
proc_info_argmodes(CallProcInfo, CallArgModes),
partition_call_args(Module, CallArgModes, Args, InVars, OutVars),
bag__from_list(OutVars, OutVarsBag),
( goal_will_fail(GoalInfo) ->
Res = ok,
Offs = []
; proc_inequalities_check_intersect(Offs0, OutVarsBag) ->
% no intersection.
Offs = Offs0,
Res = ok
;
Info = _UnifyInfo - UsedArgsMap,
CallPPId = proc(CallPredId, CallProcId),
PPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _PredInfo,
ProcInfo),
goal_info_get_context(GoalInfo, Context),
proc_info_vartypes(ProcInfo, VarType),
proc_info_termination(CallProcInfo, CallTermination),
CallTermination = term(CallTermConst, CallTerminates,
CallUsedArgs, _),
( CallTerminates = dont_know ->
Error = dont_know_proc_called(PPId, CallPPId),
Res = error(Context - Error),
Offs = Offs0
; \+ check_horder_args(Args, VarType) ->
Res = error(Context - horder_args(PPId, CallPPId)),
Offs = Offs0
;
bag__from_list(InVars, InVarsBag0),
(
CallUsedArgs = yes(UsedVars)
->
remove_unused_args(InVarsBag0, Args, UsedVars,
InVarsBag1)
; %else if
map__search(UsedArgsMap, CallPPId, UsedVars)
->
% In this case, it must be a mutually
% recursive call. As it is a mutually
% recursive call, the termination constant
% should be not_set.
require(unify(CallTermConst, not_set),
"Unexpected value in term_pass1__\
proc_inequalities(call)"),
remove_unused_args(InVarsBag0, Args,
UsedVars, InVarsBag1)
;
InVarsBag1 = InVarsBag0
),
(
CallTermConst = not_set,
Res = ok,
Eqn = eqn(set(0), PPId, [CallPPId]),
proc_inequalities_modify_offs(InVarsBag1,
OutVarsBag, Eqn, Offs0, Offs)
;
CallTermConst = set(Int),
Res = ok,
Eqn = eqn(set(Int), PPId, []),
proc_inequalities_modify_offs(InVarsBag1,
OutVarsBag, Eqn, Offs0, Offs)
;
CallTermConst = inf(_),
Offs = Offs0,
Res = error(Context -
inf_termination_const(PPId, CallPPId))
)
)
).
proc_inequalities_goal(higher_order_call(_, _, _, _, _, _),
GoalInfo, _Module, _, _PPId, Error, Offs, Offs) :-
goal_info_get_context(GoalInfo, Context),
Error = error(Context - horder_call).
proc_inequalities_goal(switch(_SwitchVar, _CanFail, Cases, _StoreMap), GoalInfo,
Module, Info, PPId, Res, Offs0, Offs) :-
( goal_will_fail(GoalInfo) ->
Res = ok,
Offs = []
;
proc_inequalities_switch(Cases, GoalInfo, Module,
Info, PPId, Res, Offs0, Offs)
).
proc_inequalities_goal(unify(_Var, _RHS, _UnifyMode, Unification, _UnifyContext),
GoalInfo, Module, Info, PPId, ok, Offs0, Offs) :-
Info = UnifyInfo - _CallInfo,
( goal_will_fail(GoalInfo) ->
Offs = []
;
(
Unification = construct(OutVar, ConsId, Args0, Modes0),
UnifyInfo = VarTypes - FunctorInfo,
% Need to check if OutVar is a higher order type.
% If so, return Offs unmodified. XXX i am not sure
% that this is always valid. If the horder type is
% used elsewhere (eg in an argument to a call),
% then it will be picked up there, and will return
% Res = error(horder...). If this check is not made
% then split_unification_vars can quit with an
% error, as length(Args) is not necessarily equal
% to length(Modes) for higher order unifications.
map__lookup(VarTypes, OutVar, Type),
( type_is_higher_order(Type, _, _) ->
Offs = Offs0
;
( type_to_type_id(Type, TypeIdPrime, _) ->
TypeId = TypeIdPrime
;
error("Variable type in termination analysis")
),
functor_norm(FunctorInfo, TypeId, ConsId,
Module, FunctorNorm, Args0, Args,
Modes0, Modes),
split_unification_vars(Args, Modes, Module,
InVarsBag , OutVarsBag0),
bag__insert(OutVarsBag0, OutVar, OutVarsBag),
Eqn = eqn(set(FunctorNorm), PPId, []),
proc_inequalities_modify_offs(InVarsBag,
OutVarsBag, Eqn, Offs0, Offs)
)
;
Unification = deconstruct(InVar, ConsId,
Args0, Modes0, _),
UnifyInfo = VarTypes - FunctorInfo,
map__lookup(VarTypes, InVar, Type),
( type_to_type_id(Type, TypeIdPrime, _) ->
TypeId = TypeIdPrime
;
error("variable type in termination analysis")
),
functor_norm(FunctorInfo, TypeId, ConsId, Module,
FunctorNorm, Args0, Args, Modes0, Modes),
split_unification_vars(Args, Modes, Module,
InVarsBag , OutVarsBag),
bag__insert(InVarsBag, InVar, InVarsBag0),
Eqn = eqn(set(- FunctorNorm), PPId, []),
proc_inequalities_modify_offs(InVarsBag0, OutVarsBag,
Eqn, Offs0, Offs)
;
Unification = assign(OutVar, InVar),
Eqn = eqn(set(0), PPId, []),
bag__init(InitBag),
bag__insert(InitBag, InVar, InVarBag),
bag__insert(InitBag, OutVar, OutVarBag),
proc_inequalities_modify_offs(InVarBag, OutVarBag, Eqn,
Offs0, Offs)
;
Unification = simple_test(_InVar1, _InVar2),
Offs = Offs0
;
Unification = complicated_unify(_, _),
error("Unexpected complicated_unify in termination.m")
)
).
% No variables are bound in an empty disjunction (fail), so it does not
% make sense to define an equation relating input variables to output
% variables.
proc_inequalities_goal(disj([], _), _, _Module, _, _PPId, ok, _Offs, []).
proc_inequalities_goal(disj([ Goal | Goals ], _StoreMap),
GoalInfo, Module, Info, PPId, Res, Offs0, Offs) :-
( goal_will_fail(GoalInfo) ->
Res = ok,
Offs = []
;
proc_inequalities_disj(Goal, Goals, GoalInfo, Module, Info,
PPId, Res, Offs0, Offs)
).
% As we are trying to form a relationship between variables sizes, and no
% variables can be bound in a not, we dont need to evaluate inside the not
proc_inequalities_goal(not(_), GoalInfo, _Module, _, _PPId, ok, Offs0, Offs) :-
( goal_will_fail(GoalInfo) ->
Offs = []
;
Offs = Offs0
).
proc_inequalities_goal(some(_Vars, GoalExpr - GoalInfo), SomeGoalInfo,
Module, Info, PPId, Res, Offs0, Offs) :-
( goal_will_fail(SomeGoalInfo) ->
Res = ok,
Offs = []
;
proc_inequalities_goal(GoalExpr, GoalInfo, Module, Info,
PPId, Res, Offs0, Offs)
).
% an if-then-else is processed as:
% (
% if_goal,
% then_goal
% ;
% % the reason that there is no need for a not(if_goal) here is that
% % no variables are bound in a not. If the if_goal is
% % non-terminating, then this will be discovered in when the if-then
% % goal is processed
% else_goal
% )
proc_inequalities_goal(if_then_else(_Vars, IfGoal, ThenGoal, ElseGoal, _),
GoalInfo, Module, Info, PPId, Res, Offs0, Offs) :-
( goal_will_fail(GoalInfo) ->
Res = ok,
Offs = []
;
NewThenGoal = conj([IfGoal, ThenGoal]) - GoalInfo,
proc_inequalities_disj(NewThenGoal, [ElseGoal], GoalInfo,
Module, Info, PPId, Res, Offs0, Offs)
).
proc_inequalities_goal(
pragma_c_code(_, _, CallPredId, CallProcId, Args, _, _, _),
GoalInfo, Module, _Info, _PPId, Res, Offs0, Offs) :-
(goal_will_fail(GoalInfo) ->
Res = ok,
Offs = []
;
module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
CallProcInfo),
proc_info_argmodes(CallProcInfo, CallArgModes),
partition_call_args(Module, CallArgModes, Args,
_InVars, OutVars),
bag__from_list(OutVars, OutVarBag),
( proc_inequalities_check_intersect(Offs, OutVarBag) ->
% no intersection
% c_code has no important output vars, so we need
% no error
Res = ok
;
goal_info_get_context(GoalInfo, Context),
Res = error(Context - pragma_c_code)
),
Offs = Offs0
).
%-----------------------------------------------------------------------------%
:- pred proc_inequalities_conj(hlds_goal, list(hlds_goal),
module_info, proc_inequalities_info, pred_proc_id,
term_util__result(term_errors__error), proc_inequalities_equ,
proc_inequalities_equ).
:- mode proc_inequalities_conj(in, in, in, in, in, out, in, out) is det.
proc_inequalities_conj(Goal, [], Module, Info, PPId, Res,
Offs0, Offs) :-
Goal = GoalExpr - GoalInfo,
proc_inequalities_goal(GoalExpr, GoalInfo, Module, Info,
PPId, Res, Offs0, Offs).
proc_inequalities_conj(Goal, [ Goal2 | Goals ], Module, Info, PPId,
Res, Offs0, Offs) :-
proc_inequalities_conj(Goal2, Goals, Module, Info,
PPId, Res1, Offs0, Offs1),
( Res1 = ok ->
Goal = GoalExpr - GoalInfo,
proc_inequalities_goal(GoalExpr, GoalInfo, Module, Info,
PPId, Res, Offs1, Offs)
;
Res = Res1,
Offs = Offs1
).
:- pred proc_inequalities_switch(list(case), hlds_goal_info,
module_info, proc_inequalities_info, pred_proc_id,
term_util__result(term_errors__error), proc_inequalities_equ,
proc_inequalities_equ).
:- mode proc_inequalities_switch(in, in, in, in, in, out, in, out) is det.
proc_inequalities_switch([], _, _Module, _, _PPId, ok, Offs, Offs) :-
error("Unexpected empty switch in term_pass1:proc_inequalities_switch").
proc_inequalities_switch([ Case | Cases ], SwitchGoalInfo,
Module, Info, PPId, Res, Offs0, Offs) :-
Case = case(_ConsId, Goal),
Goal = GoalExpr - GoalInfo,
proc_inequalities_goal(GoalExpr, GoalInfo, Module, Info,
PPId, Res1, Offs0, Offs1),
( Res1 = error(_) ->
Res = Res1,
Offs = Offs1
; Cases = [] ->
Res = Res1,
Offs = Offs1
;
proc_inequalities_switch(Cases, SwitchGoalInfo,
Module, Info, PPId, Res2, Offs0, Offs2),
( Res2 = error(_) ->
Res = Res2,
Offs = Offs2
;
list__append(Offs1, Offs2, Offs),
Res = ok
)
).
:- pred proc_inequalities_disj(hlds_goal, list(hlds_goal), hlds_goal_info,
module_info, proc_inequalities_info, pred_proc_id,
term_util__result(term_errors__error), proc_inequalities_equ,
proc_inequalities_equ).
:- mode proc_inequalities_disj(in, in, in, in, in, in, out, in, out) is det.
proc_inequalities_disj(Goal, [], _, Module, Info, PPId,
Res, Offs0, Offs) :-
Goal = GoalExpr - GoalInfo,
proc_inequalities_goal(GoalExpr, GoalInfo, Module, Info,
PPId, Res, Offs0, Offs).
proc_inequalities_disj(Goal, [Goal2 | Goals], DisjGoalInfo, Module,
Info, PPId, Res, Offs0, Offs) :-
proc_inequalities_disj(Goal2, Goals, DisjGoalInfo, Module,
Info, PPId, Res1, Offs0, Offs1),
Goal = GoalExpr - GoalInfo,
proc_inequalities_goal(GoalExpr, GoalInfo, Module, Info,
PPId, Res2, Offs0, Offs2),
( Res1 = error(_) ->
Res = Res1,
Offs = Offs1
; Res2 = error(_) ->
Res = Res2,
Offs = Offs2
;
list__append(Offs1, Offs2, Offs),
Res = ok
).
%-----------------------------------------------------------------------------%
% support functions for proc_inequalities
:- pred proc_inequalities_modify_offs(bag(var), bag(var), term_pass1__equation,
proc_inequalities_equ, proc_inequalities_equ).
:- mode proc_inequalities_modify_offs(in, in, in, in, out) is det.
proc_inequalities_modify_offs(_, _, _, [], []).
proc_inequalities_modify_offs(InVars, OutVars, ModEqn, [Out0 | Out0s],
[Out | Outs ]) :-
Out0 = Equation0 - Vars0,
( bag__intersect(OutVars, Vars0) ->
% There is an intersection
bag__subtract(Vars0, OutVars, Vars1),
bag__union(Vars1, InVars, Vars),
eqn_add(ModEqn, Equation0, Equation),
Out = Equation - Vars
;
Out = Out0
),
proc_inequalities_modify_offs(InVars, OutVars, ModEqn, Out0s, Outs).
% Adds two equations together.
:- pred eqn_add(term_pass1__equation, term_pass1__equation,
term_pass1__equation).
:- mode eqn_add(in, in, out) is det.
eqn_add(eqn(Const1, PPId1, PPList1), eqn(Const2, PPId2, PPList2), Out) :-
( PPId1 = PPId2 ->
( ( Const1 = not_set ; Const2 = not_set ) ->
OutConst = not_set
; ( Const1 = inf(Error) ) ->
OutConst = inf(Error)
; ( Const2 = inf(Error) ) ->
OutConst = inf(Error)
; ( Const1 = set(Num1), Const2 = set(Num2)) ->
OutNum = Num1 + Num2,
OutConst = set(OutNum)
;
% This really cant happen, as Const1 and Const2 can
% only be (not_set ; inf ; set(int))
% as the disjunction is not flattened, mercury cant
% work it out, and would call the pred semidet
error("term_pass1__eqn_add\n")
),
list__append(PPList1, PPList2, OutPPList),
Out = eqn(OutConst, PPId1, OutPPList)
;
% It makes no sense to add equations with different PPId
% values. Its like trying to add apples to oranges.
error("term_pass1:eqn_add was called with illegal arguments\n")
).
:- pred proc_inequalities_check_intersect(proc_inequalities_equ, bag(var)).
:- mode proc_inequalities_check_intersect(in, in) is semidet.
% Succeeds if there is no intersection.
proc_inequalities_check_intersect([], _).
proc_inequalities_check_intersect([ Out | Outs ], OutVarBag) :-
Out = _Equation - OutBag,
\+ bag__intersect(OutBag, OutVarBag),
proc_inequalities_check_intersect(Outs, OutVarBag).
% This predicate takes the list of pair(equation, bag(var)), and splits it
% up into a list(equation) and a bag(var). The output bag(var) is given by
% taking the least-upper-bound of each of the bags in the initial list.
% The least upper bound is the smallest multiset such that each bag in the
% initial list is a subset of the least upper bound.
:- pred split_offs_vars(proc_inequalities_equ, list(term_pass1__equation),
bag(var)).
:- mode split_offs_vars(in, out, out) is det.
split_offs_vars([], [], InitBag) :-
bag__init(InitBag).
split_offs_vars([ X | Xs ], [ Off | Offs ], VarBag) :-
split_offs_vars(Xs, Offs, Bag0),
X = Off - SubBag,
% now need to produce the least upper bound of Bag0 and SubBag
% eg. need least upper bound of {1, 1, 2, 2, 3 }, {1, 1, 2, 3, 3, 3}
% bag__subtract({1, 1, 2, 2, 3 }, {1, 1, 2, 3, 3, 3}, {2}),
% bag__union({1, 1, 2, 3, 3, 3}, {2}, {1, 1, 2, 2, 3, 3, 3}).
% and {1, 1, 2, 2, 3, 3, 3} is the correct least upper bound
bag__subtract(Bag0, SubBag, Bag1),
bag__union(Bag1, SubBag, VarBag).
% This predicate takes a goal_info, and succeeds iff that goal will fail.
:- pred goal_will_fail(hlds_goal_info).
:- mode goal_will_fail(in) is semidet.
goal_will_fail(GoalInfo) :-
goal_info_get_determinism(GoalInfo, Detism),
determinism_components(Detism, _, at_most_zero).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
% Solve the list of constraints
% output is of the form required by lp_solve.
% which is given the input = [eqn(Const, PPid, [PPidList])]
% max: .......
% c1: PPid - (PPidList) > Const;
% c2: PPid - (PPidList) > Const;
% where PPid (proc(PredId, ProcId)) is printed as ' aPredId_ProcId - b '
% The choice of the letter `a' is arbitrary, and is chosen as lp_solve does
% not allow variables to start with digits.
% The variable `b' is used as lp_solve will only solve for positive values
% of variables. replacing each variable occurance with ` a#_# - b ', this
% avoids the problem of only allowing positive variables as a#_# - b can
% be negative even when a#_# and b are both positive.
%
:- pred solve_equations(module_info, list(term_pass1__equation),
list(pred_proc_id), used_args, term__context, module_info,
io__state, io__state).
:- mode solve_equations(in, in, in, in, in, out, di, uo) is det.
solve_equations(Module0, Equations, PPIds, UsedArgs, Context, Module) -->
io__tmpnam(ConstraintFile),
solve_equations_create_constraint_file(Equations, PPIds,
ConstraintFile, ConstraintSucc),
( { ConstraintSucc = yes } ->
solve_equations_solve_constraint_file(ConstraintFile, Soln)
;
% Failed to create the constraint file.
{ Soln = fatal_error }
),
% The equations have been solved, now put the
% results into the module_info.
( { Soln = solved(SolutionList) } ->
% The solver successfully solved the constraints.
{ module_info_preds(Module0, PredTable0) },
{ proc_inequalities_set_module(SolutionList, UsedArgs,
PredTable0, PredTable) },
{ module_info_set_preds(Module0, PredTable,
Module) }
; { Soln = optimal } ->
% All 'optimal' results should have been
% changed into a list of solutions in
% solve_equations.
{ error("term_pass1__solve_equations: Unexpected Value\n")}
;
% The constraint solver failed to solve the
% set of constraints - set the termination
% constant to infinity.
{ Error = Context - lpsolve_failed(Soln) },
{ set_pred_proc_ids_const(PPIds,
inf(Error), Module0, Module) }
).
:- pred solve_equations_solve_constraint_file(string, eqn_soln,
io__state, io__state).
:- mode solve_equations_solve_constraint_file(in, out, di, uo) is det.
solve_equations_solve_constraint_file(ConstraintFile, Soln) -->
io__tmpnam(OutputFile),
% run lp_solve
solve_equations_run_lp_solve(ConstraintFile, OutputFile, MaybeResult),
(
{ MaybeResult = yes(Result) },
( { Result = optimal } ->
solve_equations_process_output_file(OutputFile, Soln0)
;
% lp_solve failed to solve the constraints.
% This could be for a number of reasons,
% and the value of Result will represent
% the reason.
{ Soln0 = Result }
)
;
{ MaybeResult = no },
{ Soln0 = fatal_error }
),
% Remove and close all temporary files.
solve_equations_remove_file(ConstraintFile, Success0),
solve_equations_remove_file(OutputFile, Success1),
{ bool__or(Success0, Success1, Success) },
{ (
Success = yes,
Soln = Soln0
;
Success = no,
Soln = fatal_error
) }.
% This runs lp_solve, and outputs an error message and returns `no'
% if the system call fails. On success, it returns the return value of
% lp_solve after the return value has been changed from an integer into a
% lpsolve_ret_val type.
:- pred solve_equations_run_lp_solve(string, string, maybe(eqn_soln),
io__state, io__state).
:- mode solve_equations_run_lp_solve(in, in, out, di, uo) is det.
solve_equations_run_lp_solve(ConstraintFile, OutputFile, MaybeResult) -->
io__get_environment_var("MERCURY_LPSOLVE", Lpsolve0),
( { Lpsolve0 = yes(Lpsolve1) } ->
{ Lpsolve = Lpsolve1 }
;
{ Lpsolve = "lp_solve" }
),
{ string__append_list([ Lpsolve, " <",
ConstraintFile, " > ",
OutputFile], Command) },
io__call_system(Command, Res0),
% Test the return value
(
{ Res0 = ok(RetVal) },
{ lpsolve_ret_val(RetVal, Result) },
{ MaybeResult = yes(Result) }
;
{ Res0 = error(Error0) },
io__progname_base("term_pass1.m", ProgName),
{ io__error_message(Error0, Msg0) },
io__write_strings([
ProgName,
": Error with system call `",
Command,
"': ",
Msg0,
"\n" ]),
io__set_exit_status(1),
{ MaybeResult = no }
).
:- pred solve_equations_remove_file(string, bool, io__state, io__state).
:- mode solve_equations_remove_file(in, out, di, uo) is det.
solve_equations_remove_file(File, Success) -->
io__remove_file(File, Res1),
( { Res1 = error(Error1) } ->
io__progname_base("term_pass1.m", ProgName),
{ io__error_message(Error1, Msg1) },
io__write_strings([
ProgName,
": Error deleting temporary file `",
File,
"' : ",
Msg1,
"\n" ]),
io__set_exit_status(1),
{ Success = no }
;
{ Success = yes }
).
% This predicate creates the constraint file in a format suitable for
% lp_solve. This really shouldn't be called with Equations=[] as lp_solve
% exits with an error if it is called without any constraints.
:- pred solve_equations_create_constraint_file(list(term_pass1__equation),
list(pred_proc_id), string, bool, io__state, io__state).
:- mode solve_equations_create_constraint_file(in, in, in, out, di, uo) is det.
solve_equations_create_constraint_file(Equations, PPIds,
ConstraintFile, Success) -->
io__open_output(ConstraintFile, Res),
( { Res = error(Error) },
% error message and quit
io__progname_base("termination.m", ProgName),
{ io__error_message(Error, Msg) },
io__write_string(ProgName),
io__write_string(": cannot open temporary file `"),
io__write_string(ConstraintFile),
io__write_string("' for output: "),
io__write_string(Msg),
io__write_string("\n"),
io__set_exit_status(1),
{ Success = no }
;
{ Res = ok(Stream) },
( { Equations = [] } ->
{ Success = no }
;
io__set_output_stream(Stream, OldStream),
% create the constraint file
output_equations(Equations, PPIds, Success),
io__set_output_stream(OldStream, _),
io__close_output(Stream)
)
).
% Prepare to parse the output from lp_solve.
:- pred solve_equations_process_output_file(string, eqn_soln,
io__state, io__state).
:- mode solve_equations_process_output_file(in, out, di, uo) is det.
solve_equations_process_output_file(OutputFile, Soln) -->
io__open_input(OutputFile, OutputRes),
( { OutputRes = error(Error) },
io__progname_base("term_pass1.m", ProgName),
{ io__error_message(Error, Msg) },
io__write_string(ProgName),
io__write_string(": cannot open temporary file `"),
io__write_string(OutputFile),
io__write_string("' for input: "),
io__write_string(Msg),
io__write_string("\n"),
io__set_exit_status(1),
{ Soln = fatal_error }
;
{ OutputRes = ok(Stream) },
io__set_input_stream(Stream, OldStream),
% need to interpret it now
solve_equations_parse_output_file(Soln),
io__set_input_stream(OldStream, _),
io__close_input(Stream)
).
% Parse the output from lp_solve.
:- pred solve_equations_parse_output_file(eqn_soln, io__state, io__state).
:- mode solve_equations_parse_output_file(out, di, uo) is det.
solve_equations_parse_output_file(Soln) -->
io__read_line(Res1),
( { Res1 = ok(_) } ->
solve_equations_parse_output_file_2(Soln0, MaybeBVal),
( { Soln0 = solved(Result0) } ->
( { MaybeBVal = yes(BVal) } ->
{ solve_equations_output_file_2(Result0, BVal,
Result) },
{ Soln = solved(Result) }
;
{ Soln = parse_error }
)
;
io__write_string(
"parse_output_file returned not solved\n"),
{ Soln = parse_error }
)
;
{ Soln = parse_error }
).
:- pred solve_equations_output_file_2(list(pair(pred_proc_id, int)), int,
list(pair(pred_proc_id, int))).
:- mode solve_equations_output_file_2(in, in, out) is det.
solve_equations_output_file_2([], _, []).
solve_equations_output_file_2([X | Xs], BVal, [Y | Ys]) :-
X = PPId - XVal, % pair deconstruction
YVal is XVal - BVal, % subtraction
Y = PPId - YVal, % pair construction
solve_equations_output_file_2(Xs, BVal, Ys).
:- pred solve_equations_parse_output_file_2(eqn_soln, maybe(int), io__state,
io__state).
:- mode solve_equations_parse_output_file_2(out, out, di, uo) is det.
solve_equations_parse_output_file_2(Soln, BVal) -->
io__read_line(Res1),
( { Res1 = ok([ X | Xs ]) } ->
(
{ X = 'a' },
{ char_list_remove_int(Xs, PredInt, Xs1) },
{ Xs1 = [ '_' | Xs2 ] },
{ char_list_remove_int(Xs2, ProcInt, Xs3) },
{ char_list_remove_whitespace(Xs3, Xs4) },
{ char_list_remove_int(Xs4, Value, _Xs5) }
->
% Have found a solution.
{ pred_id_to_int(PredId, PredInt) },
{ proc_id_to_int(ProcId, ProcInt) },
solve_equations_parse_output_file_2(Soln0, BVal),
( { Soln0 = solved(SolnList) } ->
{ NewSoln = proc(PredId, ProcId) - Value },
{ Soln = solved([NewSoln | SolnList ]) }
;
{ Soln = Soln0 }
)
; % else if
{ X = 'b' },
{ char_list_remove_whitespace(Xs, Xs1) },
{ char_list_remove_int(Xs1, Value, _Xs2) }
->
solve_equations_parse_output_file_2(Soln, _Bval),
{ BVal = yes(Value) }
;
{ Soln = parse_error },
{ BVal = no }
)
; { Res1 = eof } ->
{ Soln = solved([]) },
{ BVal = no }
;
{ Soln = parse_error },
{ BVal = no }
).
:- pred char_list_remove_int(list(char), int, list(char)).
:- mode char_list_remove_int(in, out, out) is semidet.
char_list_remove_int([X | Xs], Int, ListOut) :-
char__is_digit(X),
char__to_int(X, Int0),
char__to_int('0', IntValueofZero),
Int1 is Int0 - IntValueofZero,
char_list_remove_int_2(Xs, Int1, Int, ListOut).
:- pred char_list_remove_int_2(list(char), int, int, list(char)).
:- mode char_list_remove_int_2(in, in, out, out) is semidet.
char_list_remove_int_2([], Int, Int, []).
char_list_remove_int_2([X | Xs], Int0, Int, ListOut) :-
( char__is_digit(X) ->
char__to_int('0', IntValueofZero),
char__to_int(X, Int1),
Int2 is Int0 * 10 + Int1 - IntValueofZero,
char_list_remove_int_2(Xs, Int2, Int, ListOut)
;
ListOut = [ X | Xs ],
Int = Int0
).
:- pred char_list_remove_whitespace(list(char), list(char)).
:- mode char_list_remove_whitespace(in, out) is det.
char_list_remove_whitespace([], []).
char_list_remove_whitespace([ X | Xs ], Out) :-
( char__is_whitespace(X) ->
char_list_remove_whitespace(Xs, Out)
;
Out = [ X | Xs ]
).
:- pred lpsolve_ret_val(int, eqn_soln).
:- mode lpsolve_ret_val(in, out) is det.
lpsolve_ret_val(Int, Result) :-
( Int = 0 -> Result = optimal
; Int = 2 -> Result = infeasible
; Int = 3 -> Result = unbounded
; Result = failure
).
%-----------------------------------------------------------------------------%
% These predicates are used to output a list of equations in a form
% suitable for lp_solve.
:- pred output_equations(list(term_pass1__equation), list(pred_proc_id),
bool, io__state , io__state).
:- mode output_equations(in, in, out, di, uo) is det.
output_equations(Xs, PPIds, Success) -->
% output: 'max: # b - PPIds'
io__write_string("max: "),
{ list__length(PPIds, Length) },
io__write_int(Length),
io__write_string(" b "),
output_eqn_2(PPIds),
io__write_string(";\n"),
output_equations_2(Xs, 1, Success).
:- pred output_equations_2(list(term_pass1__equation), int,
bool, io__state , io__state).
:- mode output_equations_2(in, in, out, di, uo) is det.
output_equations_2([], _Count, yes) --> [].
output_equations_2([ X | Xs ], Count, Succ) -->
output_eqn(X, Count, Succ0),
( { Succ0 = yes } ->
{ Count1 is Count + 1 },
output_equations_2(Xs, Count1, Succ)
;
{ Succ = Succ0 }
).
:- pred output_eqn(term_pass1__equation, int, bool, io__state,
io__state).
:- mode output_eqn(in, in, out, di, uo) is det.
% each constraint is of the form:
% c#: # b + PPId - (PPIdList) > Const;
% each PPId is printed as `aPredId_ProcId'
% As each PPId can be negative, and lp_solve allows only positive
% variables, we introduce a dummy variable 'b' such that
% Actual PPId value = returned PPId value - b, where the returned value is
% always non-negative
output_eqn(Eqn, Count, Succ) -->
{ Eqn = eqn(Const, PPId, PPIdList0) },
{ list__length(PPIdList0, Length) },
% As there are `Length' negative PPIds, and 1 positive PPId, and
% each PPId is replaced with `PPId - b', the multiplier of b is
% Length - 1.
{ BMultiplier is Length - 1 },
( { list__delete_first(PPIdList0, PPId, PPIdList1) } ->
{ Deleted = yes },
{ PPIdList = PPIdList1 }
;
{ Deleted = no },
{ PPIdList = PPIdList0 }
),
(
{ Length = 1 },
{ Deleted = yes }
->
% There is nothing on the left hand side of the
% constraint, as there was only one element in the list,
% and it was deleted. Therefore the left hand side of the
% equation is PPId - PPId which lpsolve does not process.
% Constraints of this type should all be removed by
% proc_inequalities_scc_remove_useless_offsets.
{ Succ = no }
;
% output 'c#: '
io__write_char('c'),
io__write_int(Count),
io__write_string(": "),
% maybe output '# b '
( { BMultiplier = 0 } ->
[]
;
io__write_int(BMultiplier),
io__write_string(" b ")
),
% maybe output ' + PPId'
( { Deleted = yes } ->
[]
;
io__write_string(" + a"),
output_eqn_ppid(PPId)
),
% output `PPIdList'
output_eqn_2(PPIdList),
% output ` > Const;'
io__write_string(" > "),
( { Const = set(Int) } ->
io__write_int(Int),
{ Succ = yes }
;
{ Succ = no }
),
io__write_string(";\n")
).
% Outputs each of the pred proc id's in the form: ' - aPredId_ProcId'
:- pred output_eqn_2(list(pred_proc_id), io__state, io__state).
:- mode output_eqn_2(in, di, uo) is det.
output_eqn_2([]) --> [].
output_eqn_2([ X | Xs ]) -->
io__write_string(" - a"),
output_eqn_ppid(X),
output_eqn_2(Xs).
% Outputs a pred proc id in the form "PredId_ProcId"
:- pred output_eqn_ppid(pred_proc_id, io__state, io__state).
:- mode output_eqn_ppid(in, di, uo) is det.
output_eqn_ppid(proc(PredId, ProcId)) -->
{ pred_id_to_int(PredId, PredInt) },
{ proc_id_to_int(ProcId, ProcInt) },
io__write_int(PredInt),
io__write_char('_'),
io__write_int(ProcInt).
%-----------------------------------------------------------------------------
%
% Copyright (C) 1997 The University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------
%
% term_pass2.m
% Main author: crs.
%
% This file contains the actual termination analysis. This file processes
% through each procedure, and sets the terminates property of each one.
%
% Termination analysis:
% This goes through each of the SCC's in turn, analysing them to determine
% which predicates terminate.
%
%-----------------------------------------------------------------------------
:- module term_pass2.
:- interface.
:- import_module io, hlds_module, term_util.
% Analyse each predicate in the order given by
% hlds_dependency_info_get_dependency_ordering to determine whether or not
% it terminates. Put the result of the analysis into the termination
% field of the proc_info structure..
:- pred termination(module_info, functor_info, module_info,
io__state, io__state).
:- mode termination(in, in, out, di, uo) is det.
:- implementation.
:- import_module bag, hlds_pred, std_util, int, list, relation, require.
:- import_module set, hlds_goal, term_util, term_errors, bool.
:- import_module globals, options, map, term, type_util.
% Used in termination_goal to keep track of the relative sizes of variables
% between the head of a predicate and any recursive calls.
:- type termination_call
---> tuple(pred_proc_id, % The called procedure
int, % The relative size of the active
% variables, in comparison with the
% size of the variables in the
% recursive call.
bag(var), % The bag of active variables.
maybe(var), % Only for single argrgument analysis.
% This stores which head variable
% is being traced by this tuple.
term__context). % Where the call occured.
termination(Module0, FunctorInfo, Module) -->
{ module_info_dependency_info(Module0, DependencyInfo) },
{ hlds_dependency_info_get_dependency_ordering(DependencyInfo,
DependencyOrdering) },
termination_module(Module0, DependencyOrdering, FunctorInfo, Module).
:- pred termination_module(module_info, dependency_ordering, functor_info,
module_info, io__state, io__state).
:- mode termination_module(in, in, in, out, di, uo) is det.
termination_module(Module, [], _FunctorInfo, Module) --> [].
termination_module(Module0, [SCC | SCCs], FunctorInfo, Module) -->
termination_module_check_terminates(SCC, SCC, Module0, Module1, Succ),
( { Succ = yes } ->
% Need to run termination checking on this SCC.
% Initialise the relation
{ relation__init(Relation0) },
% Add each procedure to the relation.
{ add_pred_procs_to_relation(SCC, Relation0, Relation1) },
% Analyse the current SCC.
{ init_used_args(SCC, Module1, InitUsedArgs) },
{ call_termination_scc(SCC, FunctorInfo, Module1, Res,
InitUsedArgs, Relation1, Relation2) },
(
{ Res = ok },
% Check that the relation returned is acyclic
% and set the termination property accordingly.
( { relation__tsort(Relation2, _) } ->
% All the procedures in this SCC terminate,
% set all termination properties to yes.
{ set_pred_proc_ids_terminates(SCC,
yes, no, Module1, Module3) }
;
( { SCC = [ proc(PredId, _) | _ ] } ->
{ module_info_pred_info(Module1,
PredId, PredInfo) },
{ pred_info_context(PredInfo,
Context) }
;
{ error("Unexpected empty list in term_pass2__termination_module/6")}
),
% Try doing single argument analysis.
termination_scc_single_args(SCC, FunctorInfo,
Context - not_dag, InitUsedArgs,
Module1, Module3)
)
;
{ Res = error(Error) },
% Normal analysis failed, try doing single argument
% analysis.
termination_scc_single_args(SCC, FunctorInfo,
Error, InitUsedArgs, Module1, Module3)
)
;
% All the termination properties are already set.
{ Module3 = Module1 }
),
termination_module(Module3, SCCs, FunctorInfo, Module).
% If this predicate returns Succ = yes, then termination analysis needs to be
% run on this SCC. If it returns Succ = no, then the termination
% properties of this SCC have already been set.
% XXX this can be improved. If ANY Terminates in the SCC is set to dont_know,
% then the whole SCC can be set to dont_know
:- pred termination_module_check_terminates(list(pred_proc_id),
list(pred_proc_id), module_info, module_info, bool,
io__state, io__state).
:- mode termination_module_check_terminates(in, in, in, out, out,
di, uo) is det.
termination_module_check_terminates([], _SCC, Module, Module, no) --> [].
termination_module_check_terminates([ PPId | PPIds ], SCC, Module0,
Module, Succ) -->
{ PPId = proc(PredId, ProcId) },
{ module_info_pred_proc_info(Module0, PredId, ProcId, _, ProcInfo) },
{ proc_info_termination(ProcInfo, Term) },
{ Term = term(_Const, Terminates, _UsedArgs, MaybeError) },
(
{ Terminates = not_set },
{ Succ = yes },
{ Module = Module0 }
;
{ Terminates = yes },
termination_module_check_terminates(PPIds, SCC, Module0,
Module, Succ)
;
{ Terminates = dont_know},
{ Succ = no },
( { MaybeError = yes(Error) } ->
do_ppid_check_terminates(SCC, Error, Module0, Module)
;
{ error("term_pass2.m: unexpected value in termination_module_check_terminates/6") }
)
).
% This predicate runs termination_scc until a fixed point for UsedArgs
% is reached.
:- pred call_termination_scc(list(pred_proc_id), functor_info, module_info,
term_util__result(term_errors__error), map(pred_proc_id, set(var)),
relation(pred_proc_id), relation(pred_proc_id)).
:- mode call_termination_scc(in, in, in, out, in, in, out) is det.
call_termination_scc(SCC, FunctorInfo, Module, Result, UsedArgs0,
Relation0, Relation) :-
termination_scc(SCC, FunctorInfo, Module, Res1, UsedArgs0, UsedArgs1,
Relation0, Relation1),
(
% If some other error prevented the analysis from proving
% termination, then finding a fixed point will not assist
% in proving termination, so we may as well stop here.
( Res1 = error(_ - not_subset(_, _, _))
; Res1 = error(_ - positive_value(_, _))
),
UsedArgs1 \= UsedArgs0 % If these are equal, then we are at
% a fixed point, so further
% analysis will not get any better
% results.
->
% We can use the new Used Args values, and try again.
call_termination_scc(SCC, FunctorInfo, Module, Result,
UsedArgs1, Relation0, Relation)
;
Relation = Relation1,
Result = Res1
).
% This initialises the used arguments to be the set of input variables.
:- pred init_used_args(list(pred_proc_id), module_info,
map(pred_proc_id, set(var))).
:- mode init_used_args(in, in, out) is det.
init_used_args([], _, InitMap) :-
map__init(InitMap).
init_used_args([PPId | PPIds], Module, UsedArgs) :-
init_used_args(PPIds, Module, UsedArgs0),
PPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
proc_info_headvars(ProcInfo, Args),
proc_info_argmodes(ProcInfo, ArgModes),
partition_call_args(Module, ArgModes, Args, InArgs, _OutVars),
set__list_to_set(InArgs, ArgSet),
map__det_insert(UsedArgs0, PPId, ArgSet, UsedArgs).
% Given a list of all the arguments of a predicate, find out which
% arguments are unused, so that they can be removed from the used arguments
% list for that predicate.
:- pred termination_scc_calc_unused_args(list(var), list(termination_call),
list(var)).
:- mode termination_scc_calc_unused_args(in, in, out) is det.
termination_scc_calc_unused_args(Vars, [], Vars).
termination_scc_calc_unused_args(Vars0, [X | Xs], Vars) :-
X = tuple(_, _, VarBag, _, _),
termination_scc_calc_unused_args_2(Vars0, VarBag, Vars1),
termination_scc_calc_unused_args(Vars1, Xs, Vars).
:- pred termination_scc_calc_unused_args_2(list(var), bag(var), list(var)).
:- mode termination_scc_calc_unused_args_2(in, in, out) is det.
termination_scc_calc_unused_args_2([], _, []).
termination_scc_calc_unused_args_2([ X | Xs ], Vars, Ys) :-
( bag__contains(Vars, X) ->
% If the variable is in the bag, then it is used.
% Therefore, it should not be in the list of unused vars
termination_scc_calc_unused_args_2(Xs, Vars, Ys)
;
termination_scc_calc_unused_args_2(Xs, Vars, Ys0),
Ys = [X | Ys0]
).
% Process a whole SCC, to determine the termination property of each
% procedure in that SCC.
:- pred termination_scc(list(pred_proc_id), functor_info, module_info,
term_util__result(term_errors__error), map(pred_proc_id, set(var)),
map(pred_proc_id, set(var)), relation(pred_proc_id),
relation(pred_proc_id)).
:- mode termination_scc(in, in, in, out, in, out, in, out) is det.
termination_scc([], _, _Module, ok, UsedArgs, UsedArgs, Relation, Relation).
termination_scc([ PPId | PPIds ], FunctorInfo, Module, Result,
UsedArgs0, UsedArgs, Relation0, Relation) :-
% Get the goal info.
PPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _PredInfo, ProcInfo),
proc_info_termination(ProcInfo, Termination),
( Termination = term(_Const, dont_know, _, MaybeError) ->
% If the termination property is set to dont_know then
% MaybeError should contain an error.
( MaybeError = yes(Error) ->
Result = error(Error)
;
error("term_pass2.m: Unexpected value in term_pass2:termination_scc")
),
UsedArgs = UsedArgs0,
Relation = Relation0
;
proc_info_goal(ProcInfo, Goal),
proc_info_vartypes(ProcInfo, VarTypes),
Goal = GoalExpr - GoalInfo,
% Analyse goal info. This returns a list of ppid - size
% pairs.
UnifyInfo = VarTypes - FunctorInfo,
CallInfo = call_info(PPId, UsedArgs0, no),
termination_goal(GoalExpr, GoalInfo, Module, UnifyInfo,
CallInfo, Res0, [], Out),
proc_info_argmodes(ProcInfo, ArgModes),
proc_info_headvars(ProcInfo, Args),
partition_call_args(Module, ArgModes, Args, InVars, _OutVars),
bag__from_list(InVars, InVarsBag),
( Res0 = ok ->
termination_scc_calc_unused_args(Args, Out, UnUsedArgs),
map__lookup(UsedArgs0, PPId, OldUsedArgs),
set__delete_list(OldUsedArgs, UnUsedArgs, NewUsedArgs),
termination_add_arcs_to_relation(PPId, Out,
InVarsBag, Res1, Relation0, Relation1),
( Res1 = ok ->
termination_scc(PPIds, FunctorInfo, Module,
Result, UsedArgs0, UsedArgs1,
Relation1, Relation)
;
% We failed because of positive value, or
% because of not_subset. Keep analysing,
% to discover the used variables, of the other
% procedures.
termination_scc(PPIds, FunctorInfo, Module,
Res2, UsedArgs0, UsedArgs1,
Relation0, _Relation),
Relation = Relation0,
% We know that Res1 is not_subset or
% positive_value. If Res2 is ok, then we
% need to return Res1 (so that the calling
% predicate knows that the analysis
% failed). If Res2 is an error, then it
% needs to be returned. If Res2 is also
% not_subset or positive_value, then fine,
% the analysis will be re-run. If it is
% some other error, then re-running the
% analysis will not gain anything.
( Res2 = ok ->
Result = Res1
;
Result = Res2
)
),
% Add the used vars from the current pass to the
% UsedArgs map.
map__det_update(UsedArgs1, PPId, NewUsedArgs, UsedArgs)
;
UsedArgs = UsedArgs0,
Result = Res0,
Relation = Relation0
)
).
% This runs single argument analysis on the goal. This is only run if
% normal termination analysis failed.
:- pred termination_scc_single_args(list(pred_proc_id), functor_info,
term_errors__error, map(pred_proc_id, set(var)),
module_info, module_info, io__state, io__state).
:- mode termination_scc_single_args(in, in, in, in, in, out, di, uo) is det.
termination_scc_single_args([], _, _, _, Module, Module) -->
{ error("term_pass2__termination_scc_single_args: there should be\nat least 1 predicate in a SCC\n") }.
termination_scc_single_args([PPId | Rest], FunctorInfo, Error, UsedArgs,
Module0, Module) -->
globals__io_lookup_bool_option(termination_single_args, SingleArgs),
{ SCC = [PPId | Rest] },
{ PPId = proc(PredId, ProcId) },
{ set__init(InitSet) },
(
{ SingleArgs = yes },
{ Rest = [] },
{ Error \= _ - imported_pred }
% What other errors would prevent single argument analysis
% from succeeding?
->
% Can do single argument analysis.
{ module_info_pred_proc_info(Module0, PredId, ProcId,
_PredInfo, ProcInfo) },
{ proc_info_goal(ProcInfo, Goal) },
{ proc_info_vartypes(ProcInfo, VarTypes) },
{ Goal = GoalExpr - GoalInfo },
{ UnifyInfo = VarTypes - FunctorInfo },
{ CallInfo = call_info(PPId, UsedArgs, yes) },
{ termination_goal(GoalExpr, GoalInfo, Module0,
UnifyInfo, CallInfo, Res0, [], Out) },
( { Res0 = error(Error2) } ->
% The context of single_arg_failed needs to be the
% same as the context of the Normal analysis error
% message.
{ Error = Context - _ },
{ Error3 = Context - single_arg_failed(Error, Error2) },
do_ppid_check_terminates(SCC, Error3,
Module0, Module)
; { termination_scc_single_2(Out, InitSet, InitSet) } ->
% Single argument analysis succeded.
{ set_pred_proc_ids_terminates(SCC, yes, yes(Error),
Module0, Module) }
;
% Single argument analysis failed to prove
% termination.
{ Error = Context - _ },
{ Error2 = Context - single_arg_failed(Error) },
do_ppid_check_terminates(SCC, Error2,
Module0, Module)
)
;
% Cant do single argument analysis.
do_ppid_check_terminates(SCC, Error,
Module0, Module)
).
:- pred termination_scc_single_2(list(termination_call), set(var), set(var)).
:- mode termination_scc_single_2(in, in, in) is semidet.
termination_scc_single_2([], NegSet, NonNegSet) :-
set__difference(NegSet, NonNegSet, DiffSet),
% Check that there is at least one head variable that is always
% strictly decreasing in size between the head of the procedure and
% the recursive call.
set__remove_least(DiffSet, _, _).
termination_scc_single_2([Off | Offs], NegSet0, NonNegSet0) :-
Off = tuple(_, Int, VarBag0, MaybeVar, _Context),
(
MaybeVar = no,
error("termination.m: Maybevar should be yes in single argument analysis\n")
;
MaybeVar = yes(HeadVar),
(
Int < 0,
% Check that the variable that was recursed on did
% not change positions between the head and
% recursive call. I am not sure if the first call
% to bag__remove is actually required to succeed
bag__remove(VarBag0, HeadVar, VarBag1),
\+ bag__remove_smallest(VarBag1, _, _)
->
set__insert(NegSet0, HeadVar, NegSet),
termination_scc_single_2(Offs, NegSet, NonNegSet0)
;
set__insert(NonNegSet0, HeadVar, NonNegSet),
termination_scc_single_2(Offs, NegSet0, NonNegSet)
)
).
% This adds the information from termination_goal to the relation.
% The relation is between the procedures in the current SCC. An arc
% shows that one procedure calls another with the size of the variables
% unchanged between the head and the (possibly indirect) recursive call.
% Any loops in the relation show possible non-termination. This predicate
% also checks that the calculated input variables are subsets of the actual
% input variables
:- pred termination_add_arcs_to_relation(pred_proc_id, list(termination_call),
bag(var), term_util__result(term_errors__error),
relation(pred_proc_id), relation(pred_proc_id)).
:- mode termination_add_arcs_to_relation(in, in, in, out, in, out) is det.
termination_add_arcs_to_relation(_PPid, [], _Vars, ok, Relation, Relation).
termination_add_arcs_to_relation(PPId, [X | Xs], Vars, Result, Relation0,
Relation) :-
X = tuple(CalledPPId, Value, Bag, _Var, Context),
( bag__is_subbag(Bag, Vars) ->
compare(Res, Value, 0),
(
Res = (>),
Result = error(Context -
positive_value(PPId, CalledPPId)),
Relation = Relation0
;
Res = (=),
% Add the arc to the relation.
relation__lookup_element(Relation0, PPId, Key),
relation__lookup_element(Relation0, CalledPPId,
CalledKey),
relation__add(Relation0, Key, CalledKey, Relation1),
termination_add_arcs_to_relation(PPId, Xs, Vars,
Result, Relation1, Relation)
;
Res = (<),
termination_add_arcs_to_relation(PPId, Xs, Vars,
Result, Relation0, Relation)
)
;
Result = error(Context - not_subset(PPId, Bag, Vars)),
Relation = Relation0
).
:- pred add_pred_procs_to_relation(list(pred_proc_id), relation(pred_proc_id),
relation(pred_proc_id)).
:- mode add_pred_procs_to_relation(in, in, out) is det.
add_pred_procs_to_relation([], Relation, Relation).
add_pred_procs_to_relation([PPId | PPIds], Relation0, Relation) :-
relation__add_element(Relation0, PPId, _, Relation1),
add_pred_procs_to_relation(PPIds, Relation1, Relation).
%-----------------------------------------------------------------------------%
% termination_goal is the main section of the analysis for pass 2. It
% processes the goal of a single procedure, and returns a list of
% termination_call structures. Each termination_call structure represents
% a single (mutually or directly) recursive call, and also tracks the
% relative size of the input variables in the recursive call, in comparison
% to the variables in the head.
:- type call_info --->
call_info(
% The pred_proc_id of the predicate that we are
% currently processing.
pred_proc_id,
% A map from each procedure in the current SCC to
% the used-vars for that procedure. It is used to
% find whether or not a call is mutually recursive,
% and to find the used-variables of the predicate
% that is being called.
map(pred_proc_id, set(var)),
bool % are we doing single argument analysis?
).
:- pred termination_goal(hlds_goal_expr, hlds_goal_info, module_info,
unify_info, call_info, term_util__result(term_errors__error),
list(termination_call), list(termination_call)).
:- mode termination_goal(in, in, in, in, in, out, in, out) is det.
termination_goal(conj(Goals),
_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
termination_conj(Goals, Module, UnifyInfo, CallInfo, Res,
Out0, Out).
% This processes calls when doing normal termination analysis (as opposed
% to single argument analysis).
termination_goal(call(CallPredId, CallProcId, Args, _IsBuiltin, _, _),
GoalInfo, Module, _UnifyInfo, call_info(PPId, UsedArgsMap, no),
Res, Out0, Out) :-
PPId = proc(PredId, ProcId),
CallPPId = proc(CallPredId, CallProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
CallProcInfo),
proc_info_vartypes(ProcInfo, VarType),
proc_info_argmodes(CallProcInfo, CallArgModes),
proc_info_termination(CallProcInfo, CallTermination),
CallTermination = term(CallTermConst, CallTerminates, CallUsedArgs, _),
goal_info_get_context(GoalInfo, Context),
partition_call_args(Module, CallArgModes, Args, InVars, OutVars),
bag__from_list(InVars, InVarBag0),
bag__from_list(OutVars, OutVarBag),
( CallUsedArgs = yes(UsedVars) ->
remove_unused_args(InVarBag0, Args, UsedVars,
InVarBag1)
;
InVarBag1 = InVarBag0
),
% Step 1 - modify Out0
(
CallTermConst = set(Int),
termination_goal_modify_out(InVarBag1, OutVarBag, Int,
Out0, Out1),
Res0 = ok
;
CallTermConst = not_set,
error("Unexpected Termination Constant in termination.m"),
Res0 = ok,
Out1 = Out0
;
CallTermConst = inf(_),
( termination_goal_check_intersect(Out0, OutVarBag) ->
% There is no intersection, so just continue
Res0 = ok
;
Res0 = error(Context -
inf_termination_const(PPId, CallPPId))
),
Out1 = Out0
),
% Step 2 - do we add another arc?
( CallTerminates = dont_know ->
Res = error(Context - dont_know_proc_called(PPId, CallPPId)),
Out = Out0
; \+ check_horder_args(Args, VarType) ->
Res = error(Context - horder_args(PPId, CallPPId)),
Out = Out0
;
( map__search(UsedArgsMap, CallPPId, RecursiveUsedArgs) ->
% The called procedure is in the map, so the call is
% recursive - add it to Out.
proc_info_headvars(CallProcInfo, HeadVars),
termination_call_2(Args, HeadVars,
RecursiveUsedArgs, Bag),
NewOutElem = tuple(CallPPId, 0, Bag, no, Context),
Out = [ NewOutElem | Out1 ]
;
% The call is not recursive
Out = Out1
),
Res = Res0
).
termination_goal(call(CallPredId, CallProcId, Args, _IsBuiltin, _, _),
GoalInfo, Module, _UnifyInfo,
call_info(PPId, _UsedArgsMap, yes), Res, Out0, Out) :-
PPId = proc(PredId, ProcId),
CallPPId = proc(CallPredId, CallProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
CallProcInfo),
proc_info_vartypes(ProcInfo, VarType),
proc_info_argmodes(CallProcInfo, CallArgModes),
proc_info_headvars(CallProcInfo, HeadVars),
proc_info_termination(CallProcInfo, CallTermination),
CallTermination = term(_, CallTerminates, _CallUsedArgs, _),
goal_info_get_context(GoalInfo, Context),
partition_call_args(Module, CallArgModes, Args, InVars, OutVars),
partition_call_args(Module, CallArgModes, HeadVars, InHeadVars, _),
bag__from_list(OutVars, OutVarBag),
% Step 1 - modify Out0
( termination_goal_check_intersect(Out0, OutVarBag) ->
% There is no intersection, so just continue.
Res0 = ok,
Out1 = Out0
;
% This analysis could be much better, but it will do for
% now.
Res0 = error(Context - call_in_single_arg(CallPPId)),
Out1 = Out0
),
% Step 2 - do we add another arc?
( CallTerminates = dont_know ->
Res = error(Context - dont_know_proc_called(PPId, CallPPId)),
Out = Out0
; \+ check_horder_args(Args, VarType) ->
Res = error(Context - horder_args(PPId, CallPPId)),
Out = Out0
;
( CallPPId = PPId ->
% The call is recursive - add it to Out
termination_call(InVars, InHeadVars, PPId,
Context, Out1, Out)
;
% The call is not recursive
Out = Out1
),
Res = Res0
).
termination_goal(higher_order_call(_, _, _, _, _, _),
GoalInfo, _Module, _UnifyInfo, _CallInfo, Res, Out0, Out) :-
goal_info_get_context(GoalInfo, Context),
Res = error(Context - horder_call),
Out = Out0.
termination_goal(switch(_Var, _CanFail, Cases, _StoreMap),
_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
termination_switch(Cases, Module, UnifyInfo, CallInfo,
Res, Out0, Out).
termination_goal(unify(_Var, _RHS, _UniMode, Unification, _Context),
_GInfo, Module, UnifyInfo, _CallInfo, ok, Out0, Out) :-
(
Unification = construct(OutVar, ConsId, Args0, Modes0),
UnifyInfo = VarTypes - FunctorInfo,
map__lookup(VarTypes, OutVar, Type),
% length(Args) is not necessarily equal to length(Modes)
% for higher order constructions.
( type_is_higher_order(Type, _, _) ->
Out = Out0
;
( type_to_type_id(Type, TypeIdPrime, _) ->
TypeId = TypeIdPrime
;
error("variable type in termination_goal")
),
functor_norm(FunctorInfo, TypeId, ConsId, Module,
FunctorNorm, Args0, Args, Modes0, Modes),
split_unification_vars(Args, Modes, Module, InVarBag,
OutVarBag0),
bag__insert(OutVarBag0, OutVar, OutVarBag),
termination_goal_modify_out(InVarBag, OutVarBag,
FunctorNorm, Out0, Out)
)
;
Unification = deconstruct(InVar, ConsId, Args0, Modes0, _),
UnifyInfo = VarTypes - FunctorInfo,
map__lookup(VarTypes, InVar, Type),
( type_to_type_id(Type, TypeIdPrime, _) ->
TypeId = TypeIdPrime
;
error("variable type in termination analysis")
),
functor_norm(FunctorInfo, TypeId, ConsId, Module,
FunctorNorm, Args0, Args, Modes0, Modes),
split_unification_vars(Args, Modes, Module, InVarBag0,
OutVarBag),
bag__insert(InVarBag0, InVar, InVarBag),
termination_goal_modify_out(InVarBag, OutVarBag,
(- FunctorNorm), Out0, Out)
;
Unification = assign(OutVar, InVar),
bag__init(InitBag),
bag__insert(InitBag, InVar, InVarBag),
bag__insert(InitBag, OutVar, OutVarBag),
termination_goal_modify_out(InVarBag, OutVarBag, 0, Out0, Out)
;
Unification = simple_test(_InVar1, _InVar2),
Out = Out0
;
Unification = complicated_unify(_, _),
error("Unexpected complicated_unify in term_pass2.m")
).
termination_goal(disj(Goals, _StoreMap),
_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
termination_disj(Goals, Module, UnifyInfo, CallInfo, Res, Out0, Out).
termination_goal(not(GoalExpr - GoalInfo),
_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
termination_goal(GoalExpr, GoalInfo, Module, UnifyInfo, CallInfo,
Res, Out0, Out).
termination_goal(some(_Vars, GoalExpr - GoalInfo),
_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
termination_goal(GoalExpr, GoalInfo, Module, UnifyInfo, CallInfo,
Res, Out0, Out).
termination_goal(if_then_else(_Vars, CondGoal, ThenGoal, ElseGoal, _),
_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
CondGoal = CondExpr - CondGoalInfo,
ThenGoal = ThenExpr - ThenGoalInfo,
ElseGoal = ElseExpr - ElseGoalInfo,
termination_goal(ThenExpr, ThenGoalInfo, Module, UnifyInfo, CallInfo,
ThenRes, Out0, ThenOut),
termination_goal(ElseExpr, ElseGoalInfo, Module, UnifyInfo, CallInfo,
ElseRes, Out0, ElseOut),
( ThenRes = error(_) ->
Res = ThenRes,
Out = ThenOut
; ElseRes = error(_) ->
Res = ElseRes,
Out = ElseOut
;
% They both succeded - join the outs
list__append(ThenOut, ElseOut, Out1),
termination_goal(CondExpr, CondGoalInfo, Module,
UnifyInfo, CallInfo, Res, Out1, Out)
).
termination_goal(pragma_c_code(_, _, CallPredId, CallProcId, Args, _, _, _),
GoalInfo, Module, _UnifyInfo, _CallInfo, Res, Out, Out) :-
module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
CallProcInfo),
proc_info_argmodes(CallProcInfo, CallArgModes),
partition_call_args(Module, CallArgModes, Args, _InVars, OutVars),
bag__from_list(OutVars, OutVarBag),
( termination_goal_check_intersect(Out, OutVarBag) ->
% c_code has no important output variables, so we
% dont need an error.
Res = ok
;
goal_info_get_context(GoalInfo, Context),
Res = error(Context - pragma_c_code)
).
%-----------------------------------------------------------------------------%
% These following predicates all support termination_goal.
:- pred termination_conj(list(hlds_goal), module_info,
unify_info, call_info, term_util__result(term_errors__error),
list(termination_call), list(termination_call)).
:- mode termination_conj(in, in, in, in, out, in, out) is det.
termination_conj([] , _Module, _UnifyInfo, _CallInfo, ok, Out, Out).
termination_conj([ Goal | Goals ], Module, UnifyInfo, CallInfo,
Res, Out0, Out) :-
Goal = GoalExpr - GoalInfo,
termination_conj(Goals, Module, UnifyInfo, CallInfo,
Res0, Out0, Out1),
( Res0 = ok ->
termination_goal(GoalExpr, GoalInfo, Module,
UnifyInfo, CallInfo, Res, Out1, Out)
;
Res = Res0,
Out = Out1
).
% Used by single argument analysis to make a seperate Out for each input
% variable in a recursive call.
:- pred termination_call(list(var), list(var), pred_proc_id,
term__context, list(termination_call), list(termination_call)).
:- mode termination_call(in, in, in, in, in, out) is det.
termination_call([], [], _, _, Out, Out).
termination_call([_|_], [], _, _, Out, Out) :-
error("term_pass2__termination_call: Unmatched variables\n").
termination_call([], [_|_], _, _, Out, Out) :-
error("term_pass2:termination_call: Unmatched variables\n").
termination_call([ Var | Vars ], [ HeadVar | HeadVars ], PPId,
Context, Outs0, Outs) :-
bag__init(Bag0),
bag__insert(Bag0, Var, Bag),
Out = tuple(PPId, 0, Bag, yes(HeadVar), Context),
termination_call(Vars, HeadVars, PPId, Context,
[Out | Outs0], Outs).
% Used to set the bag of input variables for a recursive call, according to
% the set of used arguments.
:- pred termination_call_2(list(var), list(var), set(var), bag(var)).
:- mode termination_call_2(in, in, in, out) is det.
termination_call_2([], [], _, Out) :-
bag__init(Out).
termination_call_2([_|_], [], _, _Out) :-
error("Unmatched vars in termination_call_2\n").
termination_call_2([], [_|_], _, _Out) :-
error("Unmatched vars in termination_call_2\n").
termination_call_2([Var | Vars], [HeadVar | HeadVars],
UsedSet, OutBag) :-
termination_call_2(Vars, HeadVars, UsedSet, OutBag0),
( set__member(HeadVar, UsedSet) ->
bag__insert(OutBag0, Var, OutBag)
;
OutBag = OutBag0
).
:- pred termination_switch(list(case), module_info,
unify_info, call_info, term_util__result(term_errors__error),
list(termination_call), list(termination_call)).
:- mode termination_switch(in, in, in, in, out, in, out) is det.
termination_switch([] , _Module, _UnifyInfo, _CallInfo, ok, Out, Out) :-
error("term_pass2:termination_switch: unexpected empty switch\n").
termination_switch([ Case | Cases ], Module, UnifyInfo,
CallInfo, Res, Out0, Out):-
Case = case(_, Goal),
Goal = GoalExpr - GoalInfo,
( Cases = [] ->
Res1 = ok,
Out1 = Out0
;
termination_switch(Cases, Module, UnifyInfo, CallInfo,
Res1, Out0, Out1)
),
( Res1 = ok ->
termination_goal(GoalExpr, GoalInfo,
Module, UnifyInfo, CallInfo, Res, Out0, Out2),
list__append(Out1, Out2, Out)
;
Res = Res1,
Out = Out1
).
:- pred termination_disj(list(hlds_goal), module_info,
unify_info, call_info, term_util__result(term_errors__error),
list(termination_call), list(termination_call)).
:- mode termination_disj(in, in, in, in, out, in, out) is det.
termination_disj([] , _Module, _UnifyInfo, _CallInfo, ok, Out, Out):-
( Out = [] ->
true
;
error("term_pass2:termination_disj: Unexpected value after disjunction\n")
).
termination_disj([ Goal | Goals ], Module, UnifyInfo,
CallInfo, Res, Out0, Out) :-
Goal = GoalExpr - GoalInfo,
( Goals = [] ->
Res1 = ok,
Out1 = Out0
;
termination_disj(Goals, Module, UnifyInfo, CallInfo,
Res1, Out0, Out1)
),
( Res1 = ok ->
termination_goal(GoalExpr, GoalInfo, Module,
UnifyInfo, CallInfo, Res, Out0, Out2),
list__append(Out1, Out2, Out)
;
Res = Res1,
Out = Out1
).
:- pred termination_goal_check_intersect(list(termination_call), bag(var)).
:- mode termination_goal_check_intersect(in, in) is semidet.
% termination_goal_check_intersect succeeds if there is no intersection
% between any one of the Outs and the OutVarBag.
termination_goal_check_intersect([], _).
termination_goal_check_intersect([ Out | Outs ], OutVarBag) :-
Out = tuple(_PPId, _Const, OutBag, _Var, _Context),
\+ bag__intersect(OutBag, OutVarBag),
termination_goal_check_intersect(Outs, OutVarBag).
:- pred termination_goal_modify_out(bag(var), bag(var), int,
list(termination_call), list(termination_call)).
:- mode termination_goal_modify_out(in, in, in, in, out) is det.
termination_goal_modify_out(_, _, _, [], []).
termination_goal_modify_out(InVars, OutVars, Off,
[Out0 | Out0s], [Out | Outs]):-
Out0 = tuple(PPId, Int0, Vars0, Var, Context),
( bag__intersect(OutVars, Vars0) ->
% There is an intersection.
bag__subtract(Vars0, OutVars, Vars1),
bag__union(InVars, Vars1, Vars),
Int = Int0 + Off,
Out = tuple(PPId, Int, Vars, Var, Context)
;
% There is not an intersection.
Out = Out0
),
termination_goal_modify_out(InVars, OutVars, Off, Out0s, Outs).
%-----------------------------------------------------------------------------
%
% Copyright (C) 1997 The University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------
%
% term_util.m
% Main author: crs.
%
% This file contains utilities that are used by termination analysis.
%
%-----------------------------------------------------------------------------
:- module term_util.
:- interface.
:- import_module list, bool, bag, int, hlds_module, hlds_pred, hlds_data.
:- import_module term_errors, io, hlds_goal, term, prog_data, map.
% term(TermConstant, Terminates, UsedArgs, MaybeError)
% TermConstant See description below
% Terminates See description below
% UsedArgs This list of bool, when set, has a 1:1
% correspondance with the arguments of the
% procedure. It stores whether the argument
% is used in producing the output
% arguments.
% MaybeError If the analysis fails to prove termination
% of a procedure, then this value indicates
% the reason that the analysis failed.
:- type termination
---> term(term_util__constant, terminates, maybe(list(bool)),
maybe(term_errors__error)).
% term_util__constant defines the level by which a procedures arguments
% grow or shrink. It is used to determine the termination properties of a
% predicate. The termination constant defines the relative sizes of input
% and output arguments in the following equation:
% | input arguments | + constant >= | output arguments |
% where | | represents a semilinear norm.
:- type term_util__constant
---> inf(term_errors__error)
% The smallest constant that the analysis
% could prove was valid is infinity.
% Whenever a constant is set to infinity,
% an error is associated with it which
% states why the analysis failed to find a
% smaller constant.
; not_set % The termination constant has not been
% set yet. After
% term_pass1:proc_inequalities has been
% run, the constant should be set for all
% the procedures in the module. Failure to
% set the constant would indicate a
% programming error.
; set(int). % The termination constant has been
% set to int.
:- type terminates
---> dont_know % The analysis could not prove that the
% procedure terminates.
; not_set % Each procedure has its `terminates' set
% set to not_set initially.
% The termination analysis uses the fact
% that if a procedure is called whose
% terminates is not_set, then the call is
% mutually recursive. (If the call is not
% mutually recursive, then the analysis
% will have already processed the
% procedure, and would have set the
% constant). term_pass2:termination should
% set the terminates value of all
% procedures. Failure to do so indicates a
% software error.
; yes. % This procedure terminates for all
% possible inputs.
% The functor algorithm defines how a weight is assigned to each functor.
:- type functor_algorithm
---> simple % simple assigns all non-constant
% functors a norm of 1.
; total % All functors have a norm = arity of functor
% Use the weight table to find the
% weight of any constructor.
; use_map(weight_table)
% Use the weight table, and use its bool list to
% determine which arguments of any functor are to
% be considered when calculating the norm of a
% functor.
; use_map_and_args(weight_table).
:- type term_util__result(T)
---> ok
; error(T).
:- type unify_info == pair(map(var, type), functor_info).
:- type functor_info == functor_algorithm.
% These types are used to assign functor weights to functor symbols
% The weight_info is assigned to a cons_id. weight(Integer, BoolList) gives
% the weight to assign to this functor symbol, and the BoolList states
% whether or not each argument of this functor should be used to calculate
% the size of the output. That is, the BoolList has a 1:1 mapping with the
% arguments of the functor.
:- type weight_info ---> weight(int, list(bool)).
:- type weight_table == map(pair(type_id, cons_id), weight_info).
% This predicate provides an initialised termination structure.
:- pred term_util__init(termination).
:- mode term_util__init(out) is det.
% This predicate calculates a weight table according to the following
% rules:
% If a type is directly recursive, its weight is given by the number of
% directly recursive arguments of this cons id. For example, a list has
% size 1, a binary tree has size 2. Each element of the bool list is
% assigned yes if the corresponding argument is directly recursive, and no
% otherwise.
% If a type is not directly recursive, then it is assigned a weight of 1,
% and the bool list is set to be all yes.
%
% If the bool list is used (by setting functor_algorithm to
% use_map_and_args), then the effect of this norm is that the size
% of a data structure is given by the number of data elements in the data
% structure. If the bool list is ignored, then the size of all the
% arguments of any functor considered, then the size of a data structure is
% given by the total size of its data elements.
:- pred find_weights(module_info::in, weight_table::out) is det.
% This predicate is used to assign a norm (integer) to a functor, depending
% on its type. Depending on the functor_algorithm, this predicate may also
% modify the list of args and modes.
:- pred functor_norm(functor_info, type_id, cons_id, module_info, int,
list(var), list(var), list(uni_mode), list(uni_mode)).
:- mode functor_norm(in, in, in, in, out, in, out, in, out) is det.
% This predicate should be called whenever a procedure needs its termination
% set to dont_know. This predicate checks to see whether the termination
% is already set to dont_know, and if so it does nothing. If the
% termination is set to yes, or not_set, it changes the termination to
% dont_know, and checks whether a
% check_termination pragma has been defined for this predicate, and if so,
% this outputs a useful error message.
:- pred do_ppid_check_terminates(list(pred_proc_id), term_errors__error,
module_info, module_info, io__state, io__state).
:- mode do_ppid_check_terminates(in, in, in, out, di, uo) is det.
% Used to create lists of boolean values, which are used for used_args.
% make_bool_list(HeadVars, BoolIn, BoolOut) creates a bool list which is
% (length(HeadVars) - length(BoolIn)) `no' followed by BoolIn. This is
% used to set the used args for compiler generated predicates. The no's
% at the start are because the Type infos are not used. length(BoolIn)
% should equal the arity of the predicate, and the difference in length
% between the arity of the procedure and the arity of the predicate is
% the number of type infos.
:- pred term_util__make_bool_list(list(_T), list(bool), list(bool)).
:- mode term_util__make_bool_list(in, in, out) is det.
% This predicate partitions the arguments of a call into a list of input
% variables and a list of output variables,
:- pred partition_call_args(module_info, list(mode), list(var), list(var),
list(var)).
:- mode partition_call_args(in, in, in, out, out) is det.
% Removes variables from the InVarBag that are not used in the call.
% remove_unused_args(InVarBag0, VarList, BoolList, InVarBag)
% VarList and BoolList are corresponding lists. Any variable in VarList
% that has a `no' in the corresponding place in the BoolList is removed
% from InVarBag.
:- pred remove_unused_args(bag(var), list(var), list(bool), bag(var)).
:- mode remove_unused_args(in, in, in, out) is det.
% Given a list of pred_proc_ids, this predicate sets the termination
% constant of them all to the constant that is passed to it.
:- pred set_pred_proc_ids_const(list(pred_proc_id), term_util__constant,
module_info, module_info).
:- mode set_pred_proc_ids_const(in, in, in, out) is det.
% Given a list of pred_proc_ids, this predicate sets the error and
% terminates value of them all to the values that are passed to the
% predicate.
:- pred set_pred_proc_ids_terminates(list(pred_proc_id), terminates,
maybe(term_errors__error), module_info, module_info).
:- mode set_pred_proc_ids_terminates(in, in, in, in, out) is det.
% Fails if one or more variables in the list are higher order
:- pred check_horder_args(list(var), map(var, type)).
:- mode check_horder_args(in, in) is semidet.
% Given a list of variables from a unification, this predicate divides the
% list into a bag of input variables, and a bag of output variables.
:- pred split_unification_vars(list(var), list(uni_mode), module_info,
bag(var), bag(var)).
:- mode split_unification_vars(in, in, in, out, out) is det.
:- implementation.
:- import_module map, std_util, require, mode_util, prog_out, type_util.
:- import_module globals, options, inst_match, assoc_list.
term_util__init(term(not_set, not_set, no, no)).
check_horder_args([], _).
check_horder_args([Arg | Args], VarType) :-
map__lookup(VarType, Arg, Type),
\+ type_is_higher_order(Type, _, _),
check_horder_args(Args, VarType).
set_pred_proc_ids_const([], _Const, Module, Module).
set_pred_proc_ids_const([PPId | PPIds], Const, Module0, Module) :-
PPId = proc(PredId, ProcId),
module_info_preds(Module0, PredTable0),
map__lookup(PredTable0, PredId, PredInfo0),
pred_info_procedures(PredInfo0, ProcTable0),
map__lookup(ProcTable0, ProcId, ProcInfo0),
proc_info_termination(ProcInfo0, Termination0),
Termination0 = term(_Const, Term, UsedArgs, MaybeError),
Termination = term(Const, Term, UsedArgs, MaybeError),
proc_info_set_termination(ProcInfo0, Termination, ProcInfo),
map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable),
pred_info_set_procedures(PredInfo0, ProcTable, PredInfo),
map__det_update(PredTable0, PredId, PredInfo, PredTable),
module_info_set_preds(Module0, PredTable, Module1),
set_pred_proc_ids_const(PPIds, Const, Module1, Module).
set_pred_proc_ids_terminates([], _Terminates, _, Module, Module).
set_pred_proc_ids_terminates([PPId | PPIds], Terminates, MaybeError,
Module0, Module) :-
PPId = proc(PredId, ProcId),
module_info_preds(Module0, PredTable0),
map__lookup(PredTable0, PredId, PredInfo0),
pred_info_procedures(PredInfo0, ProcTable0),
map__lookup(ProcTable0, ProcId, ProcInfo0),
proc_info_termination(ProcInfo0, Termination0),
Termination0 = term(Const, _Terminates, UsedArgs, _),
Termination = term(Const, Terminates, UsedArgs, MaybeError),
proc_info_set_termination(ProcInfo0, Termination, ProcInfo),
map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable),
pred_info_set_procedures(PredInfo0, ProcTable, PredInfo),
map__det_update(PredTable0, PredId, PredInfo, PredTable),
module_info_set_preds(Module0, PredTable, Module1),
set_pred_proc_ids_terminates(PPIds, Terminates, MaybeError,
Module1, Module).
remove_unused_args(Vars, [], [], Vars).
remove_unused_args(Vars, [], [_X | _Xs], Vars) :-
error("Unmatched variables in term_util:remove_unused_args").
remove_unused_args(Vars, [_X | _Xs], [], Vars) :-
error("Unmatched variables in term_util__remove_unused_args").
remove_unused_args(Vars0, [ Arg | Args ], [ UsedVar | UsedVars ], Vars) :-
( UsedVar = yes ->
% The variable is used, so leave it
remove_unused_args(Vars0, Args, UsedVars, Vars)
;
% The variable is not used in producing output vars, so
% dont include it as an input variable.
bag__delete(Vars0, Arg, Vars1),
remove_unused_args(Vars1, Args, UsedVars, Vars)
).
% For these next two predicates (split_unification_vars and
% partition_call_args) there is a problem of what needs to be done for
% partially instantiated data structures. The correct answer is that the
% system shoud use a norm such that the size of the uninstantiated parts of
% a partially instantiated structure have no effect on the size of the data
% structure according to the norm. For example when finding the size of a
% list-skeleton, list-length norm should be used. Therefore, the size of
% any term must be given by
% sizeof(term) = constant + sum of the size of each
% (possibly partly) instantiated subterm.
% It is probably easiest to implement this by modifying term_weights.
% The current implementation does not correctly handle partially
% instantiated data structures.
split_unification_vars([], Modes, _ModuleInfo, Vars, Vars) :-
bag__init(Vars),
( Modes = [] ->
true
;
error("term_util:split_unification_vars: Unmatched Variables")
).
split_unification_vars([Arg | Args], Modes, ModuleInfo,
InVars, OutVars):-
( Modes = [UniMode | UniModes] ->
split_unification_vars(Args, UniModes, ModuleInfo,
InVars0, OutVars0),
UniMode = ((_VarInit - ArgInit) -> (_VarFinal - ArgFinal)),
( % if
inst_is_bound(ModuleInfo, ArgInit)
->
% Variable is an input variable
bag__insert(InVars0, Arg, InVars),
OutVars = OutVars0
; % else if
inst_is_free(ModuleInfo, ArgInit),
inst_is_bound(ModuleInfo, ArgFinal)
->
% Variable is an output variable
InVars = InVars0,
bag__insert(OutVars0, Arg, OutVars)
; % else
InVars = InVars0,
OutVars = OutVars0
)
;
error("term_util__split_unification_vars: Unmatched Variables")
).
partition_call_args(_, [], [_ | _], _, _) :-
error("Unmatched variables in term_util:partition_call_args").
partition_call_args(_, [_ | _], [], _, _) :-
error("Unmatched variables in term_util__partition_call_args").
partition_call_args(_, [], [], [], []).
partition_call_args(ModuleInfo, [ArgMode | ArgModes], [Arg | Args],
InputArgs, OutputArgs) :-
partition_call_args(ModuleInfo, ArgModes, Args,
InputArgs1, OutputArgs1),
( mode_is_input(ModuleInfo, ArgMode) ->
InputArgs = [Arg | InputArgs1],
OutputArgs = OutputArgs1
; mode_is_output(ModuleInfo, ArgMode) ->
InputArgs = InputArgs1,
OutputArgs = [Arg | OutputArgs1]
;
InputArgs = InputArgs1,
OutputArgs = OutputArgs1
).
term_util__make_bool_list(HeadVars0, Bools, Out) :-
list__length(Bools, Arity),
( list__drop(Arity, HeadVars0, HeadVars1) ->
HeadVars = HeadVars1
;
error("Unmatched variables in term_util:make_bool_list")
),
term_util__make_bool_list_2(HeadVars, Bools, Out).
:- pred term_util__make_bool_list_2(list(_T), list(bool), list(bool)).
:- mode term_util__make_bool_list_2(in, in, out) is det.
term_util__make_bool_list_2([], Bools, Bools).
term_util__make_bool_list_2([ _ | Vars ], Bools, [no | Out]) :-
term_util__make_bool_list_2(Vars, Bools, Out).
%----------------------------------------------------------------------------%
% Although the module info is not used in either of these norms, it could
% be needed for other norms, so it should not be removed.
functor_norm(simple, _, ConsId, _, Int, Args, Args, Modes, Modes) :-
(
ConsId = cons(_, Arity),
Arity \= 0
->
Int = 1
;
Int = 0
).
functor_norm(total, _, ConsId, _Module, Int, Args, Args, Modes, Modes) :-
( ConsId = cons(_, Arity) ->
Int = Arity
;
Int = 0
).
functor_norm(use_map(ConsIdMap), TypeId, ConsId, _Module, Int,
Args, Args, Modes, Modes) :-
( map__search(ConsIdMap, TypeId - ConsId, WeightInfo) ->
WeightInfo = weight(Int, _)
;
Int = 0
).
functor_norm(use_map_and_args(ConsIdMap), TypeId, ConsId, _Module, Int,
Args0, Args, Modes0, Modes) :-
( map__search(ConsIdMap, TypeId - ConsId, WeightInfo) ->
WeightInfo = weight(Int, UseArgList),
(
functor_norm_remove_elems(UseArgList, Args0, Args1,
Modes0, Modes1)
->
Modes = Modes1,
Args = Args1
;
error("Unmatched lists in term_util__functor_norm_remove_elems.")
)
;
Int = 0,
Modes = Modes0,
Args = Args0
).
% This predicate will fail if the length of the input lists are not matched.
:- pred functor_norm_remove_elems(list(bool), list(var), list(var),
list(uni_mode), list(uni_mode)).
:- mode functor_norm_remove_elems(in, in, out, in, out) is semidet.
functor_norm_remove_elems([], [], [], [], []).
functor_norm_remove_elems([yes | Bools], [Arg0 | Args0], [Arg0 | Args],
[Mode0 | Modes0], [Mode0 | Modes]) :-
functor_norm_remove_elems(Bools, Args0, Args, Modes0, Modes).
functor_norm_remove_elems([no | Bools], [_Arg0 | Args0], Args,
[_Mode0 | Modes0], Modes) :-
functor_norm_remove_elems(Bools, Args0, Args, Modes0, Modes).
%----------------------------------------------------------------------------%
do_ppid_check_terminates([] , _Error, Module, Module) --> [].
do_ppid_check_terminates([ PPId | PPIds ], Error, Module0, Module) -->
% look up markers
{ PPId = proc(PredId, ProcId) },
{ module_info_preds(Module0, PredTable0) },
{ map__lookup(PredTable0, PredId, PredInfo0) },
{ pred_info_procedures(PredInfo0, ProcTable0) },
{ map__lookup(ProcTable0, ProcId, ProcInfo0) },
{ proc_info_termination(ProcInfo0, Termination0) },
{ Termination0 = term(Const, Terminates, UsedArgs, _) },
( { Terminates = dont_know } ->
{ Module2 = Module0 }
;
{ Termination = term(Const, dont_know, UsedArgs, yes(Error)) },
{ proc_info_set_termination(ProcInfo0, Termination, ProcInfo)},
{ map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable) },
{ pred_info_set_procedures(PredInfo0, ProcTable, PredInfo) },
{ map__det_update(PredTable0, PredId, PredInfo, PredTable) },
{ module_info_set_preds(Module0, PredTable, Module1) },
{ pred_info_get_marker_list(PredInfo, MarkerList) },
globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
% If a check_terminates pragma exists, print out an error
% message.
% Note that this allows the one error to be printed out
% multiple times. This is because one error can cause a
% number of predicates to be non terminating, and if
% check_terminates is defined on all of the predicates,
% then the error is printed out for each of them.
(
{ list__member(request(check_termination), MarkerList) }
->
term_errors__output(PredId, ProcId, Module1,
Success),
% Success is only no if there was no error
% defined for this predicate. As we just set the
% error, term_errors__output should succeed.
{ require(unify(Success, yes), "term_util.m: Unexpected value in do_ppid_check_terminates") },
io__set_exit_status(1),
{ module_info_incr_errors(Module1, Module2) }
; % else if
{ \+ pred_info_is_imported(PredInfo) },
% Only output warnings of non-termination for
% important errors, unless verbose errors are
% enabled. Important errors are errors where the
% compiler analysed the code and was not able to
% prove termination. Unimportant warnings are
% created when code is used/called which the
% compiler was unable to analyse/prove termination
% of.
(
{ VerboseErrors = yes }
;
{ Error = _Context - TermError },
{ \+ simple_error(TermError) }
)
->
term_errors__output(PredId, ProcId, Module1,
Success),
% Success is only no if there was no error
% defined for this predicate. As we just set the
% error, term_errors__output should succeed.
{ require(unify(Success, yes), "term_util.m: Unexpected value in do_ppid_check_terminates") },
{ Module2 = Module1 }
;
% Even though the predicate does not terminate, no
% warning has been requested for it.
{ Module2 = Module1 }
)
),
do_ppid_check_terminates(PPIds, Error, Module2, Module).
%----------------------------------------------------------------------------%
%----------------------------------------------------------------------------%
% This predicate calculates a weight table according to the following
% rules:
% If a type is directly recursive, its weight is given by the number of
% directly recursive arguments of this cons id. For example, a list has
% size 1, a binary tree has size 2. Each element of the bool list is
% assigned yes if the corresponding argument is directly recursive, and no
% otherwise.
% If a type is not directly recursive, then it is assigned a weight of 1,
% and the bool list is set to be all yes.
%
% If the bool list is used, then the effect of this norm is that the size
% of a data structure is given by the number of data elements in the data
% structure. If the bool list is ignored, and the size of all the
% arguments are considered, then the size of a data structure is given by
% the total size of its data elements.
find_weights(ModuleInfo, Weights) :-
module_info_types(ModuleInfo, TypeTable),
map__to_assoc_list(TypeTable, TypeList),
map__init(Weights0),
find_weights_for_type_list(TypeList, Weights0, Weights).
:- pred find_weights_for_type_list(assoc_list(type_id, hlds_type_defn)::in,
weight_table::in, weight_table::out) is det.
find_weights_for_type_list([], Weights, Weights).
find_weights_for_type_list([TypeId - TypeDefn | TypeList], Weights0, Weights) :-
find_weights_for_type(TypeId, TypeDefn, Weights0, Weights1),
find_weights_for_type_list(TypeList, Weights1, Weights).
:- pred find_weights_for_type(type_id::in, hlds_type_defn::in,
weight_table::in, weight_table::out) is det.
find_weights_for_type(TypeId, TypeDefn, Weights0, Weights) :-
hlds_data__get_type_defn_body(TypeDefn, TypeBody),
(
TypeBody = du_type(Constructors, _, _, _),
hlds_data__get_type_defn_tparams(TypeDefn, TypeParams),
find_weights_for_cons_list(Constructors, TypeId, TypeParams,
Weights0, Weights)
;
TypeBody = uu_type(_),
error("undiscriminated union types not yet implemented")
;
% This type does not introduce any functors
TypeBody = eqv_type(_),
Weights = Weights0
;
% This type may introduce some functors,
% but we will never see them in this analysis
TypeBody = abstract_type,
Weights = Weights0
).
:- pred find_weights_for_cons_list(list(constructor)::in,
type_id::in, list(type_param)::in,
weight_table::in, weight_table::out) is det.
find_weights_for_cons_list([], _, _, Weights, Weights).
find_weights_for_cons_list([Constructor | Constructors], TypeId, Params,
Weights0, Weights) :-
find_weights_for_cons(Constructor, TypeId, Params, Weights0, Weights1),
find_weights_for_cons_list(Constructors, TypeId, Params,
Weights1, Weights).
:- pred find_weights_for_cons(constructor::in,
type_id::in, list(type_param)::in,
weight_table::in, weight_table::out) is det.
find_weights_for_cons(SymName - Args, TypeId, Params, Weights0, Weights) :-
list__length(Args, Arity),
( Arity > 0 ->
find_and_count_nonrec_args(Args, TypeId, Params,
NumNonRec, ArgInfos0),
( NumNonRec = 0 ->
Weight = 1,
list__duplicate(Arity, yes, ArgInfos)
;
Weight = NumNonRec,
ArgInfos = ArgInfos0
),
WeightInfo = weight(Weight, ArgInfos)
;
WeightInfo = weight(0, [])
),
ConsId = cons(SymName, Arity),
map__det_insert(Weights0, TypeId - ConsId, WeightInfo, Weights).
:- pred find_and_count_nonrec_args(list(constructor_arg)::in,
type_id::in, list(type_param)::in,
int::out, list(bool)::out) is det.
find_and_count_nonrec_args([], _, _, 0, []).
find_and_count_nonrec_args([Arg | Args], Id, Params, NonRecArgs, ArgInfo) :-
find_and_count_nonrec_args(Args, Id, Params, NonRecArgs0, ArgInfo0),
( is_arg_recursive(Arg, Id, Params) ->
NonRecArgs = NonRecArgs0,
ArgInfo = [yes | ArgInfo0]
;
NonRecArgs is NonRecArgs0 + 1,
ArgInfo = [no | ArgInfo0]
).
:- pred is_arg_recursive(constructor_arg::in,
type_id::in, list(type_param)::in) is semidet.
is_arg_recursive(Arg, Id, Params) :-
Arg = _Name - ArgType,
type_to_type_id(ArgType, ArgTypeId, ArgTypeParams),
Id = ArgTypeId,
list__perm(Params, ArgTypeParams).
%-----------------------------------------------------------------------------%
%
% Copyright (C) 1997 The University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------%
%
% term_errors.m
% Main author: crs.
%
% This module prints out the various error messages that are produced by
% termination.m
%
%-----------------------------------------------------------------------------%
:- module term_errors.
:- interface.
:- import_module io, bag, std_util, term, list, bool.
:- import_module hlds_module.
% term_errors__output(PredId, ProcId, Module, Success, IO0, IO).
% This is used to print out the errors found by termination analysis.
% Success returns yes if an error was successfully printed out.
% Success will be no if there was no termination error for that
% procedure.
:- pred term_errors__output(pred_id, proc_id, module_info, bool,
io__state, io__state).
:- mode term_errors__output(in, in, in, out, di, uo) is det.
% term_errors__output_const_error(PredId, ProcId, Module, Success, IO0, IO).
% This prints out any errors which occured when trying to set the
% termination constant. An error message will only be available if
% the termination constant is set to 'inf'.
% Success returns yes if an error was successfully printed out.
% Success will be no if there was no termination error for that
% procedure.
:- pred term_errors__output_const_error(pred_id, proc_id, module_info, bool,
io__state, io__state).
:- mode term_errors__output_const_error(in, in, in, out, di, uo) is det.
% This is used to print out error messages for the hlds dumps. These are
% much more concise than the normal error messages.
:- pred term_errors__output_hlds(pred_id, proc_id, module_info,
io__state, io__state).
:- mode term_errors__output_hlds(in, in, in, di, uo) is det.
:- type term_errors__error == pair(term__context, termination_error).
% With these error messages, they do not necessarily need to involve the
% procedure that they are assigned to. It is possible that an error
% occured when processing other predicates in the same SCC, and therefore
% the termination (or termination constant) of this predicate was set to
% dont_know (or infinity), even though the error occured in a different
% predicate.
:- type termination_error
% A recursive call is made with variables that are
% strictly larger than in the head. Note that
% the recursive call may be indirect, so this does
% not neccessarily indicate non-termination.
% The first PPId is the calling proc. The second
% PPId is the called procedure.
---> positive_value(pred_proc_id, pred_proc_id)
; horder_call
; pragma_c_code
; imported_pred
% dont_know_proc_called(CallerProc, CalleeProc)
% A call was made from CallerProc to CalleeProc,
% where the termination constant of the CalleeProc
% is set to dont_know.
; dont_know_proc_called(pred_proc_id, pred_proc_id)
% horder_args(CallerProc, CalleeProc)
% This error message indicates that the CallerProc
% called the CalleeProc where some of the arguments
% are of a higher order type.
; horder_args(pred_proc_id, pred_proc_id)
; inf_termination_const(pred_proc_id, pred_proc_id)
% not_subset(Proc, SupplierVariables, InHeadVariables)
% This error occurs when the Supplier variables
% (either Recursive-input suppliers or Output
% suppliers, depending on whether the error was
% associated with a dont_know or with a constant of
% infinity) is not a subset of the input head
% variables.
; not_subset(pred_proc_id, bag(var), bag(var))
; not_dag
; no_eqns
; lpsolve_failed(eqn_soln)
; call_in_single_arg(pred_proc_id)
% single argument analysis did not find a head
% variable that was decreasing in size.
; single_arg_failed(term_errors__error)
% single_arg_failed(ReasonForNormalAnalysisFailing,
% ReasonForSingleArgAnalysisFailing)
; single_arg_failed(term_errors__error, term_errors__error)
% the termination constant of a builtin predicate
% is set to infinity if the types of the builtin
% predicate may have a norm greater than 0.
; is_builtin
; does_not_term_pragma(pred_id).
% eqn_soln are used to report the results from solving the equations
% created in the first pass. The first 4 (optimal - failure) represent
% output states from lp_solve.
:- type eqn_soln
---> optimal
; infeasible
; unbounded
; failure
; fatal_error % unable to open a file, or make a system call
; parse_error % unable to parse the output from lp_solve
; solved(list(pair(pred_proc_id, int))).
% An error is considered a simple error if it is likely that the error is
% caused by the analysis failing, instead of being due to a programming
% error.
:- pred simple_error(term_errors__termination_error).
:- mode simple_error(in) is semidet.
:- implementation.
:- import_module hlds_out, prog_out, hlds_pred, passes_aux, require.
:- import_module mercury_to_mercury, term_util, bag, options, globals.
simple_error(horder_call).
simple_error(pragma_c_code).
simple_error(imported_pred).
simple_error(dont_know_proc_called(_, _)).
simple_error(call_in_single_arg(_)).
simple_error(horder_args(_, _)).
simple_error(single_arg_failed(_Context - Error)) :- simple_error(Error).
simple_error(single_arg_failed(_Con1 - Err1, _Con2 - Err2)) :-
simple_error(Err1), simple_error(Err2).
simple_error(does_not_term_pragma(_)).
term_errors__output(PredId, ProcId, Module, Success) -->
{ module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo) },
{ proc_info_termination(ProcInfo, Termination) },
{ Termination = term(_Const, _Terminates, _UsedArgs, MaybeError) },
( { MaybeError = yes(Context - Error) } ->
prog_out__write_context(Context),
io__write_string("Termination of "),
hlds_out__write_pred_id(Module, PredId),
io__nl,
prog_out__write_context(Context),
io__write_string(" not proved because "),
{ ConstErrorOutput = no },
{ ForHLDSDump = no },
term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput,
ForHLDSDump, Context - Error),
{ Success = yes }
;
{ Success = no }
).
term_errors__output_const_error(PredId, ProcId, Module, Success) -->
{ module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo) },
{ proc_info_termination(ProcInfo, Termination) },
{ Termination = term(Const, _Terminates, _UsedArgs, _MaybeError) },
( { Const = inf(Context - Error) } ->
prog_out__write_context(Context),
io__write_string("Termination constant of "),
hlds_out__write_pred_id(Module, PredId),
io__nl,
prog_out__write_context(Context),
io__write_string(" set to infinity because "),
{ ConstErrorOutput = yes },
{ ForHLDSDump = no },
term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput,
ForHLDSDump, Context - Error),
{ Success = yes }
;
{ Success = no }
).
term_errors__output_hlds(PredId, ProcId, Module) -->
{ module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo) },
{ proc_info_termination(ProcInfo, Termination) },
{ Termination = term(Const, _Terminates, _UsedArgs, MaybeError) },
{ ForHLDSDump = yes },
( { MaybeError = yes(TermContext - TermError) } ->
io__write_string("% "),
prog_out__write_context(TermContext),
io__write_string("Termination not proved because "),
{ ConstErrorOutput0 = no },
term_errors__output_2(PredId,ProcId, Module, ConstErrorOutput0,
ForHLDSDump, TermContext - TermError)
;
[]
),
( { Const = inf(ConstContext - ConstError) } ->
io__write_string("% "),
prog_out__write_context(ConstContext),
io__write_string("Termination const set to inf because "),
{ ConstErrorOutput1 = yes },
term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput1,
ForHLDSDump, ConstContext - ConstError)
;
[]
).
:- pred term_errors__output_same_SCC(pred_id, module_info, term__context,
bool, io__state, io__state).
:- mode term_errors__output_same_SCC(in, in, in, in, di, uo) is det.
term_errors__output_same_SCC(PredId, Module, Context, ForHLDSDump) -->
io__write_string("it is in the same SCC as the\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" "),
hlds_out__write_pred_id(Module, PredId).
% term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput,
% ForHLDSDump, Error, IO0, IO).
% If this predicate is called from term_errors__output_const_error, then
% ConstErrorOutput should be set to `yes' to indicate that the error
% message should describe why the constant was set to infinity.
% If ConstErrorOutput is set to `no' then term_errors__output_2 describes
% why the analysis could not prove termination.
%
% If ForHLDSDump is set to yes, then a % must be placed at the beginning of
% each line, because the output is for the HLDS dump.
%
% This predicate is used by both term_errors__output() and
% term_errors__output_const_error() to print out the reason for the error.
% Before calling output_2, term_errors__output prints out:
% myfile.m:300: Termination of predicate `myfile:yourpredicate/3'
% myfile.m:300: not proved because
%
% and term_errors__output_const_error prints out:
% myfile.m:300: Termination constant of function `myfile:myfunction/6'
% myfile.m:300: set to infinity because
%
:- pred term_errors__output_2(pred_id, proc_id, module_info, bool, bool,
term_errors__error, io__state, io__state).
:- mode term_errors__output_2(in, in, in, in, in, in, di, uo) is det.
term_errors__output_2(PredId, _ProcId, Module, _ConstErrorOutput, ForHLDSDump,
Context - positive_value(CallerPPId, CalledPPId)) -->
{ CalledPPId = proc(CalledPredId, _CalledProcId) },
{ CallerPPId = proc(CallerPredId, _CallerProcId) },
( { PredId = CallerPredId } ->
io__write_string("it contains a ")
;
term_errors__output_same_SCC(PredId, Module, Context,
ForHLDSDump),
io__write_string(" which contains a ")
),
( { PredId = CalledPredId } ->
io__write_string("directly\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" recursive call ")
;
io__write_string("recursive\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string("call to "),
hlds_out__write_pred_id(Module, CalledPredId),
io__nl,
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" ")
),
io__write_string("with the size of the variables increased.\n").
term_errors__output_2(_PredId, _ProcId, _Module, _ConstErrOutput, _ForHLDSDump,
_Context - horder_call) -->
io__write_string("it contains a higher order call\n").
term_errors__output_2(_PredId, _ProcId, _Module, _ConstErrOutput, _ForHLDSDump,
_Context - pragma_c_code) -->
io__write_string("it contains a pragma c_code() declaration\n").
term_errors__output_2(PredId, _ProcId, Module, _ConstErrorOutput, ForHLDSDump,
Context - dont_know_proc_called(CallerPPId, CalleePPId)) -->
{ CallerPPId = proc(CallerPredId, _CallerProcId) },
{ CalleePPId = proc(CalleePredId, _CalleeProcId) },
( { PredId = CallerPredId } ->
io__write_string("it calls the ")
;
term_errors__output_same_SCC(CallerPredId, Module, Context,
ForHLDSDump),
io__write_string("which calls the ")
),
io__nl,
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" "),
hlds_out__write_pred_id(Module, CalleePredId),
io__nl,
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" which could not be proved to terminate\n").
term_errors__output_2(_PredId, _ProcId, _Module, _ConstErrOutput, _ForHLDSDump,
_Context - imported_pred) -->
io__write_string("it was imported.\n").
term_errors__output_2(PredId, _ProcId, Module, _ConstErrorOutput, ForHLDSDump,
Context - horder_args(CallerPPId, CalleePPId)) -->
% OtherPPId may refer to the current Predicate, or it may refer to
% another predicate in the same SCC
{ CallerPPId = proc(CallerPredId, _CallerProcId) },
{ CalleePPId = proc(CalleePredId, _CalleeProcId) },
( { PredId = CallerPredId } ->
io__write_string("it calls the ")
;
term_errors__output_same_SCC(CallerPredId, Module, Context,
ForHLDSDump),
io__write_string("which calls the")
),
io__nl,
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" "),
hlds_out__write_pred_id(Module, CalleePredId),
io__nl,
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(
" where the call contains higher order argument(s)\n").
term_errors__output_2(PredId, _ProcId, Module, ConstErrorOutput, ForHLDSDump,
Context - inf_termination_const(CallerPPId, CalleePPId)) -->
{ CallerPPId = proc(CallerPredId, _CallerProcId) },
{ CalleePPId = proc(CalleePredId, CalleeProcId) },
( { PredId = CallerPredId } ->
io__write_string("it calls the ")
;
term_errors__output_same_SCC(CallerPredId, Module, Context,
ForHLDSDump),
io__write_string("which calls the ")
),
io__nl,
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" "),
hlds_out__write_pred_id(Module, CalleePredId),
io__nl,
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(
" which has a termination constant of infinity\n"),
(
{ ForHLDSDump = no },
{ ConstErrorOutput = no }
->
{ module_info_pred_proc_info(Module, CalleePredId,
CalleeProcId, _, CalleeProcInfo) },
{ proc_info_termination(CalleeProcInfo, CalleeTermination) },
{ CalleeTermination = term(CalleeConst, _, _, _) },
globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
(
{ CalleeConst = inf(CalleeContext - CalleeConstError)},
(
{ \+ simple_error(CalleeConstError) }
;
{ VerboseErrors = yes }
)
->
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(CalleeContext),
io__write_string(" The termination constant of that predicate was set to\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(CalleeContext),
io__write_string(" infinity because "),
{ NewConstErrorOutput = yes },
term_errors__output_2(CalleePredId, CalleeProcId,
Module, NewConstErrorOutput, ForHLDSDump,
CalleeContext - CalleeConstError)
;
[]
)
;
[]
).
% If hlds dump, should print out variables in numerical form
% If verbose errors requested (-E), should list variables
term_errors__output_2(PredId, _ProcId, Module, ConstErrorOutput, ForHLDSDump,
Context - not_subset(OtherPPId,
SupplierVarsBag, HeadVarsBag)) -->
{ OtherPPId = proc(OtherPredId, OtherProcId) },
{ module_info_pred_proc_info(Module, OtherPredId, OtherProcId,
OtherPredInfo, OtherProcInfo) },
{ pred_info_get_is_pred_or_func(OtherPredInfo, OtherPredOrFunc) },
( { OtherPredId = PredId } ->
[]
;
term_errors__output_same_SCC(OtherPredId, Module, Context,
ForHLDSDump),
( { ConstErrorOutput = yes } ->
io__write_string(
". The termination constant of that\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" "),
hlds_out__write_pred_or_func(OtherPredOrFunc),
io__write_string(" was set to infinity because ")
;
io__write_string(". Termination of that\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" "),
hlds_out__write_pred_or_func(OtherPredOrFunc),
io__write_string(" could not be proved because ")
)
),
io__write_string("the analysis\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" found that the set of "),
( { ConstErrorOutput = yes } ->
io__write_string("output ")
;
io__write_string("recursive input ")
),
io__write_string("supplier variables\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" was not a subset of the head variables of the "),
hlds_out__write_pred_or_func(OtherPredOrFunc),
io__write_string(".\n"),
% Print out the variables as calculated.
{ proc_info_variables(OtherProcInfo, VarSet) },
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" The "),
( { ConstErrorOutput = yes } ->
io__write_string("output ")
;
io__write_string("recursive input ")
),
io__write_string("supplier variables are\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" "),
{ bag__to_list(SupplierVarsBag, SupplierVars) },
mercury_output_vars(SupplierVars, VarSet, no),
io__nl,
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" The input head variables are\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" "),
{ bag__to_list(HeadVarsBag, HeadVars) },
mercury_output_vars(HeadVars, VarSet, no),
io__nl.
term_errors__output_2(_PredId, _ProcId, _Module, _ConstErrorOutput, ForHLDSDump,
Context - not_dag) -->
io__write_string("there was a cycle in the call graph of\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(
" this SCC where the variables did not decrease in size\n").
term_errors__output_2(_PredId, _ProcId, _Module, ConstErrorOutput, ForHLDSDump,
Context - no_eqns)-->
{ require(unify(ConstErrorOutput, yes),
"Unexpected value in term_errors__output_2(no_eqns)") },
io__write_string("the analysis was unable to form any\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(
" constraints between the arguments of the predicates\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" and functions in this SCC\n").
term_errors__output_2(_PredId, _ProcId, _Module, _ConstErrorOutput, ForHLDSDump,
Context - lpsolve_failed(Reason)) -->
io__write_string("the constraint solver "),
(
{ Reason = optimal },
{ error("term_errors:output_2 Unexpected return value from lp_solve") }
;
{ Reason = infeasible },
io__write_string("found the\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" constraints that the analysis produced to be infeasible\n")
;
{ Reason = unbounded },
io__write_string("found that the\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(
" constraints were not strong enough to put a\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(
" bound on the value of the change constants\n")
;
{ Reason = failure },
io__write_string("was unable to\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(
" solve the constraints that were produced\n")
;
{ Reason = fatal_error },
io__set_exit_status(1),
io__write_string("was unable to create and/or\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" remove the temporary files it required\n")
;
{ Reason = parse_error },
{ error("term_errors:output_2 Unexpected return value from lp_solve") }
;
{ Reason = solved(_) },
{ error("term_errors:output_2 Unexpected return value from lp_solve") }
).
% call_in_single_arg will only be printed out as the second part of the
% single_arg_failed(NormErr, SingleErr) error. Therefore, the following
% lines have already been printed out:
% Single argument termination analysis failed to
% prove termination because
term_errors__output_2(_PredId, _ProcId, Module, _ConstErrorOutput, ForHLDSDump,
Context - call_in_single_arg(PPId)) -->
{ PPId = proc(CallPredId, _CallProcId) },
io__write_string("it encountered a call to\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" "),
hlds_out__write_pred_id(Module, CallPredId),
io__nl,
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" which could not be processed.\n").
term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput, ForHLDSDump,
Context - single_arg_failed(Error)) -->
term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput,
ForHLDSDump, Error),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(
" Single argument analysis failed to find a head variable\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" that was always decreasing in size.\n").
term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput, ForHLDSDump,
_Context - single_arg_failed(NormErr, SingleArgErr)) -->
{ NormErr = NormalContext - NormalError },
{ SingleArgErr = SingleArgContext - SingleArgError },
% single argument analysis is independent of finding the
% termination constant. The error for a termination
% constant should never be single_arg_failed.
{ require(unify(ConstErrorOutput, no),
"Unexpected value in term_errors__output_2") },
term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput,
ForHLDSDump, NormalContext - NormalError),
globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
(
{ SingleArgError \= NormalError },
{ VerboseErrors = yes }
->
% Only output a single argument error if verbose errors are
% enabled, and it is different from the normal error
% message.
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(SingleArgContext),
io__write_string(
" Single argument termination analysis failed to\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(SingleArgContext),
io__write_string(" prove termination because "),
term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput,
ForHLDSDump, SingleArgContext - SingleArgError)
;
[]
).
term_errors__output_2(_PredId, _ProcId, _Module, ConstErrorOutput, _ForHLDSDump,
_Context - is_builtin) -->
{ require(unify(ConstErrorOutput, yes),
"Unexpected value in term_errors:output_2") },
io__write_string("it is a builtin predicate\n").
term_errors__output_2(PredId, _ProcId, Module, ConstErrorOutput, ForHLDSDump,
Context - does_not_term_pragma(OtherPredId)) -->
{ require(unify(ConstErrorOutput, no),
"Unexpected value in term_errors:output_2") },
io__write_string("there was a `does_not_terminate'\n"),
maybe_write_string(ForHLDSDump, "% "),
prog_out__write_context(Context),
io__write_string(" pragma defined on "),
( { PredId = OtherPredId } ->
{ module_info_pred_info(Module, PredId, PredInfo) },
{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
io__write_string("this "),
hlds_out__write_pred_or_func(PredOrFunc),
io__nl
;
io__write_string("the "),
hlds_out__write_pred_id(Module, OtherPredId),
io__nl
).
More information about the developers
mailing list