for review: rewrite of termination analysis (part 1)
Zoltan Somogyi
zs at cs.mu.oz.au
Mon Dec 22 14:46:31 AEDT 1997
This part has the new and substandtially rewritten files.
Fergus, please review this. (I have already taken your very partial review
into consideration, except for one point. There is no need at least at the
moment to try to print the names of compiler generated predicates specially,
since no error messages from termination analysis will complain about to them.)
Zoltan.
%-----------------------------------------------------------------------------%
% 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.
%-----------------------------------------------------------------------------%
%
% error_util.m
% Main author: zs.
%
% This module contains code that can be helpful in the formatting of
% error messages.
%
%-----------------------------------------------------------------------------%
:- module error_util.
:- interface.
:- import_module io, list, term, string, int.
% Given a context, a starting indentation level and a list of words,
% print an error message that looks like this:
%
% module.m:10: first line of error message blah blah blah
% module.m:10: second line of error message blah blah blah
% module.m:10: third line of error message blah blah blah
%
% The words will be packed into lines as tightly as possible,
% with spaces between each pair of words, subject to the constraints
% that every line starts with a context, followed by Indent+1 spaces
% on the first line and Indent+3 spaces on later lines, and that every
% line contains at most 79 characters (unless a long single word
% forces the line over this limit).
:- pred write_error_pieces(term__context::in, int::in, list(string)::in,
io__state::di, io__state::uo) is det.
:- implementation.
:- import_module prog_out.
write_error_pieces(Context, Indent, Words) -->
{
% The fixed characters at the start of the line are:
% filename
% :
% line number (min 3 chars)
% :
% space
% indent
Context = term__context(FileName, LineNumber),
string__length(FileName, FileNameLength),
string__int_to_string(LineNumber, LineNumberStr),
string__length(LineNumberStr, LineNumberStrLength0),
( LineNumberStrLength0 < 3 ->
LineNumberStrLength = 3
;
LineNumberStrLength = LineNumberStrLength0
),
Remain is 79 - (FileNameLength + 1 +
LineNumberStrLength + 2 + Indent),
group_words(Words, Remain, Lines)
},
write_lines(Lines, Context, Indent).
:- pred write_lines(list(list(string))::in, term__context::in, int::in,
io__state::di, io__state::uo) is det.
write_lines([], _, _) --> [].
write_lines([Line | Lines], Context, Indent) -->
prog_out__write_context(Context),
{ string__pad_left("", ' ', Indent, IndentStr) },
io__write_string(IndentStr),
write_line(Line),
{ Indent2 is Indent + 2 },
write_nonfirst_lines(Lines, Context, Indent2).
:- pred write_nonfirst_lines(list(list(string))::in, term__context::in, int::in,
io__state::di, io__state::uo) is det.
write_nonfirst_lines([], _, _) --> [].
write_nonfirst_lines([Line | Lines], Context, Indent) -->
prog_out__write_context(Context),
{ string__pad_left("", ' ', Indent, IndentStr) },
io__write_string(IndentStr),
write_line(Line),
write_nonfirst_lines(Lines, Context, Indent).
:- pred write_line(list(string)::in, io__state::di, io__state::uo) is det.
write_line([]) --> [].
write_line([Word | Words]) -->
io__write_string(Word),
write_line_rest(Words),
io__write_char('\n').
:- pred write_line_rest(list(string)::in, io__state::di, io__state::uo) is det.
write_line_rest([]) --> [].
write_line_rest([Word | Words]) -->
io__write_char(' '),
io__write_string(Word),
write_line_rest(Words).
%----------------------------------------------------------------------------%
% Groups the given words into lines. The first line can have up to Max
% characters on it; the later lines (if any) up to Max-2 characters.
% The given list of words must be nonempty, since we always return
% at least one line.
:- pred group_words(list(string)::in, int::in, list(list(string))::out) is det.
group_words(Words, Max, Lines) :-
(
Words = [],
Lines = []
;
Words = [FirstWord | LaterWords],
get_line_of_words(FirstWord, LaterWords, Max, Line, RestWords),
Max2 is Max - 2,
group_nonfirst_line_words(RestWords, Max2, RestLines),
Lines = [Line | RestLines]
).
:- pred group_nonfirst_line_words(list(string)::in, int::in,
list(list(string))::out) is det.
group_nonfirst_line_words(Words, Max, Lines) :-
(
Words = [],
Lines = []
;
Words = [FirstWord | LaterWords],
get_line_of_words(FirstWord, LaterWords, Max, Line, RestWords),
group_nonfirst_line_words(RestWords, Max, RestLines),
Lines = [Line | RestLines]
).
:- pred get_line_of_words(string::in, list(string)::in, int::in,
list(string)::out, list(string)::out) is det.
get_line_of_words(FirstWord, LaterWords, MaxLen, Line, RestWords) :-
string__length(FirstWord, FirstWordLen),
get_later_words(LaterWords, FirstWordLen, MaxLen, [FirstWord],
Line, RestWords).
:- pred get_later_words(list(string)::in, int::in, int::in,
list(string)::in, list(string)::out, list(string)::out) is det.
get_later_words([], _, _, Line, Line, []).
get_later_words([Word | Words], OldLen, MaxLen, Line0, Line, RestWords) :-
string__length(Word, WordLen),
NewLen is OldLen + 1 + WordLen,
( NewLen =< MaxLen ->
append(Line0, [Word], Line1),
get_later_words(Words, NewLen, MaxLen,
Line1, Line, RestWords)
;
Line = Line0,
RestWords = [Word | Words]
).
%-----------------------------------------------------------------------------%
% 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
% the various modules of termination analysis.
%
%-----------------------------------------------------------------------------%
:- module term_errors.
:- interface.
:- import_module hlds_module.
:- import_module io, bag, std_util, list, assoc_list, term.
:- type termination_error
---> pragma_c_code
% The analysis result depends on the change constant
% of a piece of pragma C code, (which cannot be
% obtained without analyzing the C code, which is
% something we cannot do).
% Valid in both passes.
; imported_pred
% The SCC contains some imported procedures,
% whose code is not accessible.
; can_loop_proc_called(pred_proc_id, pred_proc_id)
% can_loop_proc_called(Caller, Callee, Context)
% The call from Caller to Callee at the associated
% context is to a procedure (Callee) whose termination
% info is set to can_loop.
% Although this error does not prevent us from
% producing argument size information, it would
% prevent us from proving termination.
% We look for this error in pass 1; if we find it,
% we do not perform pass 2.
; horder_args(pred_proc_id, pred_proc_id)
% horder_args(Caller, Callee, Context)
% The call from Caller to Callee at the associated
% context has some arguments of a higher order type.
% Valid in both passes.
; horder_call
% horder_call
% There is a higher order call at the associated
% context.
% Valid in both passes.
; inf_termination_const(pred_proc_id, pred_proc_id)
% inf_termination_const(Caller, Callee, Context)
% The call from Caller to Callee at the associated
% context is to a procedure (Callee) whose arg size
% info is set to infinite.
% Valid in both passes.
; not_subset(pred_proc_id, bag(var), bag(var))
% not_subset(Proc, SupplierVariables, InHeadVariables)
% This error occurs when the bag of active variables
% is not a subset of the input head variables.
% Valid error only in pass 1.
; inf_call(pred_proc_id, pred_proc_id)
% inf_call(Caller, Callee)
% The call from Caller to Callee at the associated
% context has infinite weight.
% Valid error only in pass 2.
; cycle(pred_proc_id, assoc_list(pred_proc_id, term__context))
% cycle(StartPPId, CallSites)
% In the cycle of calls starting at StartPPId and
% going through the named call sites may be an
% infinite loop.
; no_eqns
; too_many_paths
% There were too many distinct paths to be analyzed.
% Valid in both passes (which analyze different sets
% of paths).
; solver_failed
% The solver could not find finite termination
% constants for the procedures in the SCC.
% Valid only in pass 1.
; is_builtin(pred_id)
% The termination constant of the given builtin is
% set to infinity; this happens when the type of at
% least one output argument permits a norm greater
% than zero.
; does_not_term_pragma(pred_id).
% The given procedure has a does_not_terminate pragma.
:- type term_errors__error == pair(term__context, termination_error).
:- pred term_errors__report_term_errors(list(pred_proc_id)::in,
list(term_errors__error)::in, module_info::in,
io__state::di, io__state::uo) is det.
% An error is considered an indirect error if it is due either to a
% language feature we cannot analyze or due to an error in another part
% of the code. By default, we do not issue warnings about indirect errors,
% since in the first case, the programmer cannot do anything about it,
% and in the second case, the piece of code that the programmer *can* do
% something about is not this piece.
:- pred indirect_error(term_errors__termination_error).
:- mode indirect_error(in) is semidet.
:- implementation.
:- import_module hlds_out, prog_out, hlds_pred, passes_aux, error_util.
:- import_module mercury_to_mercury, term_util, options, globals.
:- import_module bool, int, string, map, bag, require, varset.
indirect_error(horder_call).
indirect_error(pragma_c_code).
indirect_error(imported_pred).
indirect_error(can_loop_proc_called(_, _)).
indirect_error(horder_args(_, _)).
indirect_error(does_not_term_pragma(_)).
term_errors__report_term_errors(SCC, Errors, Module) -->
{ get_context_from_scc(SCC, Module, Context) },
( { SCC = [PPId] } ->
{ Pieces0 = ["Termination", "of"] },
{ term_errors__describe_one_proc_name(PPId, Module, PredName) },
{ list__append(Pieces0, [PredName], Pieces1) },
{ Single = yes(PPId) }
;
{ Pieces0 = ["Termination", "of", "the",
"mutually", "recursive", "procedures"] },
{ term_errors__describe_several_proc_names(SCC, Module, Context,
PredNames) },
{ list__append(Pieces0, PredNames, Pieces1) },
{ Single = no }
),
(
{ Errors = [] },
{ error("empty list of errors") }
;
{ Errors = [Error] },
{ Pieces2 = ["not", "proven", "for", "the",
"following", "reason:"] },
{ list__append(Pieces1, Pieces2, Pieces) },
write_error_pieces(Context, 0, Pieces),
term_errors__output_error(Error, Single, no, 0, Module)
;
{ Errors = [_, _ | _] },
{ Pieces2 = ["not", "proven", "for", "the",
"following", "reasons:"] },
{ list__append(Pieces1, Pieces2, Pieces) },
write_error_pieces(Context, 0, Pieces),
term_errors__output_errors(Errors, Single, 1, 0, Module)
).
:- pred term_errors__report_arg_size_errors(list(pred_proc_id)::in,
list(term_errors__error)::in, module_info::in,
io__state::di, io__state::uo) is det.
term_errors__report_arg_size_errors(SCC, Errors, Module) -->
{ get_context_from_scc(SCC, Module, Context) },
( { SCC = [PPId] } ->
{ Pieces0 = ["Termination", "constant", "of"] },
{ term_errors__describe_one_proc_name(PPId, Module, PredName) },
{ list__append(Pieces0, [PredName], Pieces1) },
{ Single = yes(PPId) }
;
{ Pieces0 = ["Termination", "constants", "of", "the",
"mutually", "recursive", "procedures"] },
{ term_errors__describe_several_proc_names(SCC, Module, Context,
PredNames) },
{ list__append(Pieces0, PredNames, Pieces1) },
{ Single = no }
),
(
{ Errors = [] },
{ error("empty list of errors") }
;
{ Errors = [Error] },
{ Pieces2 = ["set", "to", "infinity", "for", "the",
"following", "reason:"] },
{ list__append(Pieces1, Pieces2, Pieces) },
write_error_pieces(Context, 0, Pieces),
term_errors__output_error(Error, Single, no, 0, Module)
;
{ Errors = [_, _ | _] },
{ Pieces2 = ["set", "to", "infinity", "for", "the",
"following", "reasons:"] },
{ list__append(Pieces1, Pieces2, Pieces) },
write_error_pieces(Context, 0, Pieces),
term_errors__output_errors(Errors, Single, 1, 0, Module)
).
:- pred term_errors__output_errors(list(term_errors__error)::in,
maybe(pred_proc_id)::in, int::in, int::in, module_info::in,
io__state::di, io__state::uo) is det.
term_errors__output_errors([], _, _, _, _) --> [].
term_errors__output_errors([Error | Errors], Single, ErrNum0, Indent, Module)
-->
term_errors__output_error(Error, Single, yes(ErrNum0), Indent, Module),
{ ErrNum1 is ErrNum0 + 1 },
term_errors__output_errors(Errors, Single, ErrNum1, Indent, Module).
:- pred term_errors__output_error(term_errors__error::in,
maybe(pred_proc_id)::in, maybe(int)::in, int::in, module_info::in,
io__state::di, io__state::uo) is det.
term_errors__output_error(Context - Error, Single, ErrorNum, Indent, Module) -->
{ term_errors__description(Error, Single, Module, Pieces0, Reason) },
{ ErrorNum = yes(N) ->
string__int_to_string(N, Nstr),
string__append_list(["Reason ", Nstr, ":"], Preamble),
Pieces = [Preamble | Pieces0]
;
Pieces = Pieces0
},
write_error_pieces(Context, Indent, Pieces),
( { Reason = yes(InfArgSizePPId) } ->
{ lookup_proc_arg_size_info(Module, InfArgSizePPId, ArgSize) },
( { ArgSize = yes(infinite(ArgSizeErrors)) } ->
% XXX the next line is cheating
{ ArgSizePPIdSCC = [InfArgSizePPId] },
term_errors__report_arg_size_errors(ArgSizePPIdSCC,
ArgSizeErrors, Module)
;
{ error("inf arg size procedure does not have inf arg size") }
)
;
[]
).
:- pred term_errors__description(termination_error::in,
maybe(pred_proc_id)::in, module_info::in, list(string)::out,
maybe(pred_proc_id)::out) is det.
term_errors__description(horder_call, _, _, Pieces, no) :-
Pieces = ["It", "contains", "a", "higher", "order", "call."].
term_errors__description(pragma_c_code, _, _, Pieces, no) :-
Pieces = ["It", "depends", "on", "the", "properties", "of",
"foreign", "language", "code", "included", "via", "a",
"`pragma c_code'", "declaration."].
term_errors__description(inf_call(CallerPPId, CalleePPId),
Single, Module, Pieces, no) :-
(
Single = yes(PPId),
require(unify(PPId, CallerPPId), "caller outside this SCC"),
Piece1 = "It"
;
Single = no,
term_errors__describe_one_proc_name(CallerPPId, Module, Piece1)
),
Piece2 = "calls",
term_errors__describe_one_proc_name(CalleePPId, Module, CalleePiece),
Pieces3 = ["with", "an", "unbounded", "increase", "in", "the",
"size", "of", "the", "input", "arguments."],
Pieces = [Piece1, Piece2, CalleePiece | Pieces3].
term_errors__description(can_loop_proc_called(CallerPPId, CalleePPId),
Single, Module, Pieces, no) :-
(
Single = yes(PPId),
require(unify(PPId, CallerPPId), "caller outside this SCC"),
Piece1 = "It"
;
Single = no,
term_errors__describe_one_proc_name(CallerPPId, Module, Piece1)
),
Piece2 = "calls",
term_errors__describe_one_proc_name(CalleePPId, Module, CalleePiece),
Pieces3 = ["which", "could", "not", "be", "proven", "to", "terminate."],
Pieces = [Piece1, Piece2, CalleePiece | Pieces3].
term_errors__description(imported_pred, _, _, Pieces, no) :-
Pieces = ["It", "contains", "one", "or", "more",
"predicates", "and/or", "functions",
"imported", "from", "another", "module."].
term_errors__description(horder_args(CallerPPId, CalleePPId), Single, Module,
Pieces, no) :-
(
Single = yes(PPId),
require(unify(PPId, CallerPPId), "caller outside this SCC"),
Piece1 = "It"
;
Single = no,
term_errors__describe_one_proc_name(CallerPPId, Module, Piece1)
),
Piece2 = "calls",
term_errors__describe_one_proc_name(CalleePPId, Module, CalleePiece),
Pieces3 = ["with", "one", "or", "more",
"higher", "order", "arguments."],
Pieces = [Piece1, Piece2, CalleePiece | Pieces3].
term_errors__description(inf_termination_const(CallerPPId, CalleePPId),
Single, Module, Pieces, yes(CalleePPId)) :-
(
Single = yes(PPId),
require(unify(PPId, CallerPPId), "caller outside this SCC"),
Piece1 = "It"
;
Single = no,
term_errors__describe_one_proc_name(CallerPPId, Module, Piece1)
),
Piece2 = "calls",
term_errors__describe_one_proc_name(CalleePPId, Module, CalleePiece),
Pieces3 = ["which", "has", "a", "termination", "constant", "of",
"infinity."],
Pieces = [Piece1, Piece2, CalleePiece | Pieces3].
term_errors__description(not_subset(ProcPPId, OutputSuppliers, HeadVars),
Single, Module, Pieces, no) :-
(
Single = yes(PPId),
require(unify(PPId, ProcPPId), "not_subset outside this SCC"),
Pieces1 = ["The", "set", "of", "its", "output", "supplier",
"variables"]
;
Single = no,
term_errors__describe_one_proc_name(ProcPPId, Module,
PPIdPiece),
Pieces1 = ["The", "set", "of", "output", "supplier",
"variables", "of", PPIdPiece]
),
ProcPPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
proc_info_varset(ProcInfo, Varset),
term_errors_var_bag_description(OutputSuppliers, Varset,
OutputSuppliersPieces),
Pieces3 = ["was", "not", "a", "subset", "of", "the", "head",
"variables"],
term_errors_var_bag_description(HeadVars, Varset, HeadVarsPieces),
list__condense([Pieces1, OutputSuppliersPieces, Pieces3,
HeadVarsPieces], Pieces).
term_errors__description(cycle(_StartPPId, CallSites), _, Module, Pieces, no) :-
( CallSites = [DirectCall] ->
term_errors__describe_one_call_site(DirectCall, Module, Site),
Pieces = ["At", "the", "recursive", "call", "at", Site,
"the", "arguments", "are", "not", "guaranteed",
"to", "decrease", "in", "size."]
;
Pieces1 = ["in", "the", "recursive", "cycle",
"through", "the", "calls", "at"],
term_errors__describe_several_call_sites(CallSites, Module,
Sites),
Pieces2 = ["the", "arguments", "are", "not", "guaranteed",
"to", "decrease", "in", "size."],
list__condense([Pieces1, Sites, Pieces2], Pieces)
).
% Pieces = ["there", "was", "a", "cycle", "in", "the", "call", "graph",
% "of", "this", "SCC", "where", "the", "variables", "did", "not",
% "decrease", "in", "size."].
% term_errors__description(positive_value(CallerPPId, CalleePPId),
% Single, Module, Pieces, no) :-
% (
% Single = yes(PPId),
% PPId = CallerPPId,
% Piece1 = "it"
% ;
% Single = no,
% term_errors__describe_one_proc_name(CallerPPId, Module, Piece1)
% ),
% ( CallerPPId = CalleePPId ->
% Pieces2 = ["contains", "a", "directly", "recursive", "call"]
% ;
% term_errors__describe_one_proc_name(CalleePPId, Module,
% CalleePiece),
% Pieces2 = ["recursive", "call", "to", CalleePiece]
% ),
% Pieces3 = ["with", "the", "size", "of", "the", "inputs", "increased."],
% list__append([Piece1 | Pieces2], Pieces3, Pieces).
term_errors__description(too_many_paths, _, _, Pieces, no) :-
Pieces = ["There", "were", "too", "many", "execution", "paths",
"for", "the", "analysis", "to", "process."].
term_errors__description(no_eqns, _, _, Pieces, no) :-
Pieces = ["The", "analysis", "was", "unable", "to", "form", "any",
"constraints", "between", "the", "arguments", "of", "this",
"group", "of", "procedures."].
term_errors__description(solver_failed, _, _, Pieces, no) :-
Pieces = ["The", "solver", "found", "the", "constraints", "produced",
"by", "the", "analysis", "to", "be", "infeasible."].
term_errors__description(is_builtin(_PredId), _Single, _, Pieces, no) :-
% XXX require(unify(Single, yes(_)), "builtin not alone in SCC"),
Pieces = ["It", "is", "a", "builtin", "predicate."].
term_errors__description(does_not_term_pragma(PredId), Single, Module,
Pieces, no) :-
Pieces1 = ["There", "was", "a", "`does_not_terminate'", "pragma",
"defined", "on"],
(
Single = yes(PPId),
PPId = proc(SCCPredId, _),
require(unify(PredId, SCCPredId), "does not terminate pragma outside this SCC"),
Piece2 = "it."
;
Single = no,
term_errors__describe_one_pred_name(PredId, Module,
Piece2Nodot),
string__append(Piece2Nodot, ".", Piece2)
),
list__append(Pieces1, [Piece2], Pieces).
%----------------------------------------------------------------------------%
:- pred term_errors_var_bag_description(bag(var)::in, varset::in,
list(string)::out) is det.
term_errors_var_bag_description(HeadVars, Varset, Pieces) :-
bag__to_assoc_list(HeadVars, HeadVarCountList),
term_errors_var_bag_description_2(HeadVarCountList, Varset, yes,
Pieces).
:- pred term_errors_var_bag_description_2(assoc_list(var, int)::in, varset::in,
bool::in, list(string)::out) is det.
term_errors_var_bag_description_2([], _, _, ["{}"]).
term_errors_var_bag_description_2([Var - Count | VarCounts], Varset, First,
[Piece | Pieces]) :-
varset__lookup_name(Varset, Var, VarName),
( Count > 1 ->
string__append(VarName, "*", VarCountPiece0),
string__int_to_string(Count, CountStr),
string__append(VarCountPiece0, CountStr, VarCountPiece)
;
VarCountPiece = VarName
),
( First = yes ->
string__append("{", VarCountPiece, Piece0)
;
Piece0 = VarCountPiece
),
( VarCounts = [] ->
string__append(Piece0, "}.", Piece),
Pieces = []
;
Piece = Piece0,
term_errors_var_bag_description_2(VarCounts, Varset, First,
Pieces)
).
%----------------------------------------------------------------------------%
:- pred term_errors__describe_one_pred_name(pred_id::in, module_info::in,
string::out) is det.
term_errors__describe_one_pred_name(PredId, Module, Piece) :-
module_info_pred_info(Module, PredId, PredInfo),
pred_info_module(PredInfo, ModuleName),
pred_info_name(PredInfo, PredName),
pred_info_arity(PredInfo, Arity),
pred_info_get_is_pred_or_func(PredInfo, PredOrFunc),
(
PredOrFunc = predicate,
PredOrFuncPart = "predicate ",
OrigArity = Arity
;
PredOrFunc = function,
PredOrFuncPart = "function ",
OrigArity is Arity - 1
),
string__int_to_string(OrigArity, ArityPart),
string__append_list([
PredOrFuncPart,
ModuleName,
":",
PredName,
"/",
ArityPart
], Piece).
:- pred term_errors__describe_one_proc_name(pred_proc_id::in, module_info::in,
string::out) is det.
term_errors__describe_one_proc_name(proc(PredId, ProcId), Module, Piece) :-
term_errors__describe_one_pred_name(PredId, Module, PredPiece),
proc_id_to_int(ProcId, ProcIdInt),
string__int_to_string(ProcIdInt, ProcIdPart),
string__append_list([
PredPiece,
" mode ",
ProcIdPart
], Piece).
:- pred term_errors__describe_several_proc_names(list(pred_proc_id)::in,
module_info::in, term__context::in, list(string)::out) is det.
term_errors__describe_several_proc_names([], _, _, []).
term_errors__describe_several_proc_names([PPId | PPIds], Module,
Context, Pieces) :-
term_errors__describe_one_proc_name(PPId, Module, Piece0),
( PPIds = [] ->
Pieces = [Piece0]
; PPIds = [LastPPId] ->
term_errors__describe_one_proc_name(LastPPId, Module,
LastPiece),
Pieces = [Piece0, "and", LastPiece]
;
string__append(Piece0, ",", Piece),
term_errors__describe_several_proc_names(PPIds, Module,
Context, Pieces1),
Pieces = [Piece | Pieces1]
).
:- pred term_errors__describe_one_call_site(pair(pred_proc_id,
term__context)::in, module_info::in, string::out) is det.
term_errors__describe_one_call_site(PPId - Context, Module, Piece) :-
term_errors__describe_one_proc_name(PPId, Module, ProcName),
Context = term__context(FileName, LineNumber),
string__int_to_string(LineNumber, LineNumberPart),
string__append_list([
ProcName,
" at ",
FileName,
":",
LineNumberPart
], Piece).
:- pred term_errors__describe_several_call_sites(assoc_list(pred_proc_id,
term__context)::in, module_info::in, list(string)::out) is det.
term_errors__describe_several_call_sites([], _, []).
term_errors__describe_several_call_sites([Site | Sites], Module, Pieces) :-
term_errors__describe_one_call_site(Site, Module, Piece0),
( Sites = [] ->
Pieces = [Piece0]
; Sites = [LastSite] ->
term_errors__describe_one_call_site(LastSite, Module,
LastPiece),
Pieces = [Piece0, "and", LastPiece]
;
string__append(Piece0, ",", Piece),
term_errors__describe_several_call_sites(Sites, Module,
Pieces1),
Pieces = [Piece | Pieces1]
).
%----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
% 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.
% Significant parts rewritten by zs.
%
% This file contains the first pass of the termination analysis,
% whose job is to discover an upper bound on the difference between
% the sizes of the output arguments of a procedure on the one hand and
% the sizes of a selected set of input arguments of the procedure
% on the other hand. We refer to this selected set of input arguments
% as the "output suppliers".
%
% For details, please refer to the papers mentioned in termination.m.
%
%-----------------------------------------------------------------------------%
:- module term_pass1.
:- interface.
:- import_module hlds_module, term_util, term_errors.
:- import_module io.
:- type arg_size_result
---> ok(
list(pair(pred_proc_id, int)),
% Gives the gamma of each procedure
% in the SCC.
used_args
% Gives the output suppliers of
% each procedure in the SCC.
)
; error(
list(term_errors__error)
).
:- pred find_arg_sizes_in_scc(list(pred_proc_id)::in, module_info::in,
pass_info::in, arg_size_result::out, list(term_errors__error)::out,
io__state::di, io__state::uo) is det.
%-----------------------------------------------------------------------------%
:- implementation.
:- import_module term_traversal, hlds_pred, hlds_goal, hlds_data.
:- import_module term_errors, mode_util, type_util, lp.
:- import_module int, float, char, string, bool, std_util, list, set, bag, map.
:- import_module term, varset, require.
%-----------------------------------------------------------------------------%
:- type pass1_result
---> ok(
list(path_info),
% One entry for each path through the
% code.
used_args,
% The next output_supplier map.
list(term_errors__error)
% There is any entry in this list for
% each procedure in the SCC in which
% the sey of active vars were not
% a subset of the input arguments.
)
; error(
list(term_errors__error)
).
find_arg_sizes_in_scc(SCC, Module, PassInfo, ArgSize, TermErrors, S0, S) :-
init_output_suppliers(SCC, Module, InitOutputSupplierMap),
find_arg_sizes_in_scc_fixpoint(SCC, Module, PassInfo,
InitOutputSupplierMap, Result, TermErrors),
(
Result = ok(Paths, OutputSupplierMap, SubsetErrors),
( SubsetErrors = [_ | _] ->
ArgSize = error(SubsetErrors),
S = S0
; Paths = [] ->
get_context_from_scc(SCC, Module, Context),
ArgSize = error([Context - no_eqns]),
S = S0
;
solve_equations(Paths, SCC, MaybeSolution, S0, S),
(
MaybeSolution = yes(Solution),
ArgSize = ok(Solution, OutputSupplierMap)
;
MaybeSolution = no,
get_context_from_scc(SCC, Module, Context),
ArgSize = error([Context - solver_failed])
)
)
;
Result = error(Errors),
ArgSize = error(Errors),
S = S0
).
%-----------------------------------------------------------------------------%
% Initialise the output suppliers map.
% Initially, we consider that no input arguments contribute their size
% to the output arguments.
:- pred init_output_suppliers(list(pred_proc_id)::in, module_info::in,
used_args::out) is det.
init_output_suppliers([], _Module, InitMap) :-
map__init(InitMap).
init_output_suppliers([PPId | PPIds], Module, OutputSupplierMap) :-
init_output_suppliers(PPIds, Module, OutputSupplierMap0),
PPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
proc_info_headvars(ProcInfo, HeadVars),
MapToNo = lambda([_HeadVar::in, Bool::out] is det, (Bool = no)),
list__map(MapToNo, HeadVars, BoolList),
map__det_insert(OutputSupplierMap0, PPId, BoolList, OutputSupplierMap).
%-----------------------------------------------------------------------------%
:- pred find_arg_sizes_in_scc_fixpoint(list(pred_proc_id)::in,
module_info::in, pass_info::in, used_args::in, pass1_result::out,
list(term_errors__error)::out) is det.
find_arg_sizes_in_scc_fixpoint(SCC, Module, PassInfo, OutputSupplierMap0,
Result, TermErrors) :-
% unsafe_perform_io(io__write_string("find_arg_sizes_in_scc_pass\n")),
% unsafe_perform_io(io__write(OutputSupplierMap0)),
% unsafe_perform_io(io__write_string("\n")),
find_arg_sizes_in_scc_pass(SCC, Module, PassInfo,
OutputSupplierMap0, [], [], Result1, [], TermErrors1),
(
Result1 = error(_),
Result = Result1,
TermErrors = TermErrors1
;
Result1 = ok(_, OutputSupplierMap1, _),
( OutputSupplierMap1 = OutputSupplierMap0 ->
Result = Result1,
TermErrors = TermErrors1
;
find_arg_sizes_in_scc_fixpoint(SCC, Module,
PassInfo, OutputSupplierMap1,
Result, TermErrors)
)
).
:- pred find_arg_sizes_in_scc_pass(list(pred_proc_id)::in,
module_info::in, pass_info::in, used_args::in,
list(path_info)::in, list(term_errors__error)::in, pass1_result::out,
list(term_errors__error)::in, list(term_errors__error)::out) is det.
find_arg_sizes_in_scc_pass([], _, _, OutputSupplierMap, Paths, SubsetErrors,
Result, TermErrors, TermErrors) :-
Result = ok(Paths, OutputSupplierMap, SubsetErrors).
find_arg_sizes_in_scc_pass([PPId | PPIds], Module, PassInfo,
OutputSupplierMap0, Paths0, SubsetErrors0, Result,
TermErrors0, TermErrors) :-
find_arg_sizes_pred(PPId, Module, PassInfo, OutputSupplierMap0,
Result1, TermErrors1),
list__append(TermErrors0, TermErrors1, TermErrors2),
PassInfo = pass_info(_, MaxErrors, _),
list__take_upto(MaxErrors, TermErrors2, TermErrors3),
(
Result1 = error(_),
Result = Result1,
TermErrors = TermErrors3
;
Result1 = ok(Paths1, OutputSupplierMap1, SubsetErrors1),
list__append(Paths0, Paths1, Paths),
list__append(SubsetErrors0, SubsetErrors1, SubsetErrors),
find_arg_sizes_in_scc_pass(PPIds, Module, PassInfo,
OutputSupplierMap1, Paths, SubsetErrors, Result,
TermErrors3, TermErrors)
).
%-----------------------------------------------------------------------------%
:- pred find_arg_sizes_pred(pred_proc_id::in, module_info::in,
pass_info::in, used_args::in, pass1_result::out,
list(term_errors__error)::out) is det.
find_arg_sizes_pred(PPId, Module, PassInfo, OutputSupplierMap0, Result,
TermErrors) :-
PPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, PredInfo, ProcInfo),
pred_info_context(PredInfo, Context),
proc_info_headvars(ProcInfo, Args),
proc_info_argmodes(ProcInfo, ArgModes),
proc_info_vartypes(ProcInfo, VarTypes),
proc_info_goal(ProcInfo, Goal),
map__init(EmptyMap),
PassInfo = pass_info(FunctorInfo, MaxErrors, MaxPaths),
init_traversal_params(Module, FunctorInfo, PPId, Context, VarTypes,
OutputSupplierMap0, EmptyMap, MaxErrors, MaxPaths, Params),
partition_call_args(Module, ArgModes, Args, InVars, OutVars),
Path0 = path_info(PPId, no, 0, [], OutVars),
set__singleton_set(PathSet0, Path0),
Info0 = ok(PathSet0, []),
traverse_goal(Goal, Params, Info0, Info),
(
Info = ok(Paths, TermErrors),
set__to_sorted_list(Paths, PathList),
upper_bound_active_vars(PathList, AllActiveVars),
map__lookup(OutputSupplierMap0, PPId,
OutputSuppliers0),
update_output_suppliers(Args, AllActiveVars,
OutputSuppliers0, OutputSuppliers),
map__det_update(OutputSupplierMap0, PPId,
OutputSuppliers, OutputSupplierMap),
( bag__is_subbag(AllActiveVars, InVars) ->
SubsetErrors = []
;
SubsetErrors = [Context -
not_subset(PPId, AllActiveVars, InVars)]
),
Result = ok(PathList, OutputSupplierMap, SubsetErrors)
;
Info = error(Errors, TermErrors),
Result = error(Errors)
).
:- pred update_output_suppliers(list(var)::in, bag(var)::in,
list(bool)::in, list(bool)::out) is det.
update_output_suppliers([], _ActiveVars, [], []).
update_output_suppliers([_ | _], _ActiveVars, [], []) :-
error("update_output_suppliers: Unmatched variables").
update_output_suppliers([], _ActiveVars, [_ | _], []) :-
error("update_output_suppliers: Unmatched variables").
update_output_suppliers([Arg | Args], ActiveVars,
[OutputSupplier0 | OutputSuppliers0],
[OutputSupplier | OutputSuppliers]) :-
( bag__contains(ActiveVars, Arg) ->
OutputSupplier = yes
;
% This guarantees that the set of output suppliers can only
% increase, which in turn guarantees that our fixpoint
% computation is monotonic and therefore terminates.
OutputSupplier = OutputSupplier0
),
update_output_suppliers(Args, ActiveVars,
OutputSuppliers0, OutputSuppliers).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
% 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(list(path_info)::in, list(pred_proc_id)::in,
maybe(list(pair(pred_proc_id, int)))::out,
io__state::di, io__state::uo) is det.
solve_equations(Paths, PPIds, Result, S0, S) :-
(
convert_equations(Paths, Varset, Equations,
Objective, PPVars)
->
map__values(PPVars, AllVars0),
list__sort_and_remove_dups(AllVars0, AllVars),
% unsafe_perform_io(io__write_string("before\n")),
% unsafe_perform_io(io__write(Equations)),
% unsafe_perform_io(io__write_string("\n")),
% unsafe_perform_io(io__write(Objective)),
% unsafe_perform_io(io__write_string("\n")),
% unsafe_perform_io(io__write(AllVars)),
% unsafe_perform_io(io__write_string("\n")),
lp_solve(Equations, min, Objective, Varset, AllVars, Soln,
S0, S),
% unsafe_perform_io(io__write_string("after\n")),
(
Soln = unsatisfiable,
Result = no
;
Soln = satisfiable(_ObjVal, SolnVal),
list__map(lookup_coeff(PPVars, SolnVal), PPIds,
SolutionList),
Result = yes(SolutionList)
)
;
Result = no,
S = S0
).
:- pred convert_equations(list(path_info)::in, varset::out, lp__equations::out,
objective::out, map(pred_proc_id, var)::out) is semidet.
convert_equations(Paths, Varset, Equations, Objective, PPVars) :-
varset__init(Varset0),
map__init(PredProcVars0),
set__init(EqnSet0),
convert_equations_2(Paths, PredProcVars0, PPVars, Varset0, Varset,
EqnSet0, EqnSet),
set__to_sorted_list(EqnSet, Equations),
map__values(PPVars, Vars),
Convert = lambda([Var::in, Coeff::out] is det,
(
Coeff = Var - 1.0
)),
list__map(Convert, Vars, Objective).
:- pred convert_equations_2(list(path_info)::in,
map(pred_proc_id, var)::in, map(pred_proc_id, var)::out,
varset::in, varset::out,
set(lp__equation)::in, set(lp__equation)::out) is semidet.
convert_equations_2([], PPVars, PPVars, Varset, Varset, Eqns, Eqns).
convert_equations_2([Path | Paths], PPVars0, PPVars, Varset0, Varset,
Eqns0, Eqns) :-
Path = path_info(ThisPPId, _, IntGamma, PPIds, _),
int__to_float(IntGamma, FloatGamma),
Eqn = eqn(Coeffs, (>=), FloatGamma),
pred_proc_var(ThisPPId, ThisVar, Varset0, Varset2, PPVars0, PPVars1),
Coeffs = [ThisVar - 1.0 | RestCoeffs],
Convert = lambda([PPId::in, Coeff::out, Pair0::in, Pair::out] is det,
(
Pair0 = VS0 - PPV0,
pred_proc_var(PPId, Var, VS0, VS, PPV0, PPV),
Coeff = Var - (-1.0),
Pair = VS - PPV
)),
list__map_foldl(Convert, PPIds, RestCoeffs, Varset2 - PPVars1,
Varset3 - PPVars2),
set__insert(Eqns0, Eqn, Eqns1),
convert_equations_2(Paths, PPVars2, PPVars, Varset3, Varset,
Eqns1, Eqns).
:- pred lookup_coeff(map(pred_proc_id, var)::in, map(var, float)::in,
pred_proc_id::in, pair(pred_proc_id, int)::out) is det.
lookup_coeff(PPIds, Soln, PPId, PPId - ICoeff) :-
map__lookup(PPIds, PPId, Var),
map__lookup(Soln, Var, Coeff),
float__ceiling_to_int(Coeff, ICoeff).
:- pred pred_proc_var(pred_proc_id::in, var::out, varset::in, varset::out,
map(pred_proc_id, var)::in, map(pred_proc_id, var)::out) is det.
pred_proc_var(PPId, Var, Varset0, Varset, PPVars0, PPVars) :-
( map__search(PPVars0, PPId, Var0) ->
Var = Var0,
Varset = Varset0,
PPVars = PPVars0
;
varset__new_var(Varset0, Var, Varset),
map__det_insert(PPVars0, PPId, Var, PPVars)
).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------
% 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 of original version: crs.
% Main author of this version: zs.
%
% This file contains the code that tries to prove that procedures terminate.
%
% For details, please refer to the papers mentioned in termination.m.
%-----------------------------------------------------------------------------
:- module term_pass2.
:- interface.
:- import_module hlds_module, term_util.
:- pred prove_termination_in_scc(list(pred_proc_id)::in, module_info::in,
pass_info::in, int::in, termination_info::out) is det.
:- implementation.
:- import_module term_traversal, term_util, term_errors.
:- import_module hlds_pred, hlds_goal, prog_data, type_util, mode_util.
:- import_module std_util, bool, int, list, assoc_list.
:- import_module set, bag, map, term, require.
:- type fixpoint_dir
---> up
; down.
:- type call_weight_info
== pair(list(term_errors__error), call_weight_graph).
:- type call_weight_graph
== map(pred_proc_id, % The max noninfinite weight
% call from this proc
map(pred_proc_id, % to this proc
pair(term__context, int))).
% is at this context and with
% this weight.
:- type pass2_result
---> ok(
call_weight_info,
used_args
)
; error(
list(term_errors__error)
).
%-----------------------------------------------------------------------------
prove_termination_in_scc(SCC, Module, PassInfo, SingleArgs, Termination) :-
init_rec_input_suppliers(SCC, Module, InitRecSuppliers),
prove_termination_in_scc_trial(SCC, InitRecSuppliers, down,
Module, PassInfo, Termination1),
(
Termination1 = can_loop(Errors),
(
% On large SCCs, single arg analysis can require
% many iterations, so we allow the user to limit
% the size of the SCCs we will try it on.
list__length(SCC, ProcCount),
ProcCount =< SingleArgs,
% Don't try single arg analysis if it cannot cure
% the reason for the failure of the main analysis.
\+ (
member(Error, Errors),
Error = _ - imported_pred
),
prove_termination_in_scc_single_arg(SCC,
Module, PassInfo)
->
Termination = cannot_loop
;
Termination = Termination1
)
;
Termination1 = cannot_loop,
Termination = Termination1
).
% Initialise the set of recursive input suppliers to be the set
% of all input variables in all procedures of the SCC.
:- pred init_rec_input_suppliers(list(pred_proc_id)::in, module_info::in,
used_args::out) is det.
init_rec_input_suppliers([], _, InitMap) :-
map__init(InitMap).
init_rec_input_suppliers([PPId | PPIds], Module, RecSupplierMap) :-
init_rec_input_suppliers(PPIds, Module, RecSupplierMap0),
PPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
proc_info_headvars(ProcInfo, HeadVars),
proc_info_argmodes(ProcInfo, ArgModes),
partition_call_args(Module, ArgModes, HeadVars, InArgs, _OutVars),
MapIsInput = lambda([HeadVar::in, Bool::out] is det,
(
( bag__contains(InArgs, HeadVar) ->
Bool = yes
;
Bool = no
)
)),
list__map(MapIsInput, HeadVars, BoolList),
map__det_insert(RecSupplierMap0, PPId, BoolList, RecSupplierMap).
%-----------------------------------------------------------------------------
% Perform single arg analysis on the SCC.
%
% We pick one procedure in the SCC (one of those with minimal arity).
% We set the recursive input suppliers of this procedure to contain
% only the first input argument, and the recursive input suppliers
% of the other procedures to the empty set, and try a fixpoint
% iteration. If it works, great, if not, try again with the next
% input arg of the selected procedure, until we run out of input
% arguments of that procedure.
%
% While the fixpoint iteration in the main algorithm looks for the
% greatest fixpoint, in which the recursive input supplier sets
% cannot increase, in single arg analysis we are looking for a
% smallest fixpoint starting from a given location, so we must
% make sure that the recursive input supplier sets cannot decrease.
:- pred prove_termination_in_scc_single_arg(list(pred_proc_id)::in,
module_info::in, pass_info::in) is semidet.
prove_termination_in_scc_single_arg(SCC, Module, PassInfo) :-
( SCC = [FirstPPId | LaterPPIds] ->
lookup_proc_arity(FirstPPId, Module, FirstArity),
find_min_arity_proc(LaterPPIds, FirstPPId, FirstArity, Module,
TrialPPId, RestSCC),
prove_termination_in_scc_single_arg_2(TrialPPId, RestSCC, 1,
Module, PassInfo)
;
error("empty SCC in prove_termination_in_scc_single_arg")
).
% Find a procedure of minimum arity among the given list and the
% tentative guess.
:- pred find_min_arity_proc(list(pred_proc_id)::in, pred_proc_id::in, int::in,
module_info::in, pred_proc_id::out, list(pred_proc_id)::out) is det.
find_min_arity_proc([], BestSofarPPId, _, _, BestSofarPPId, []).
find_min_arity_proc([PPId | PPIds], BestSofarPPId, BestSofarArity, Module,
BestPPId, RestSCC) :-
lookup_proc_arity(PPId, Module, Arity),
( Arity < BestSofarArity ->
find_min_arity_proc(PPIds, PPId, Arity,
Module, BestPPId, RestSCC0),
RestSCC = [BestSofarPPId | RestSCC0]
;
find_min_arity_proc(PPIds, BestSofarPPId, BestSofarArity,
Module, BestPPId, RestSCC0),
RestSCC = [PPId | RestSCC0]
).
% Perform single arg analysis on the SCC.
:- pred prove_termination_in_scc_single_arg_2(pred_proc_id::in,
list(pred_proc_id)::in, int::in, module_info::in, pass_info::in)
is semidet.
prove_termination_in_scc_single_arg_2(TrialPPId, RestSCC, ArgNum0,
Module, PassInfo) :-
init_rec_input_suppliers_single_arg(TrialPPId, RestSCC,
ArgNum0, Module, InitRecSuppliers),
prove_termination_in_scc_trial([TrialPPId | RestSCC], InitRecSuppliers,
up, Module, PassInfo, Termination),
( Termination = cannot_loop ->
true
;
ArgNum1 is ArgNum0 + 1,
prove_termination_in_scc_single_arg_2(TrialPPId, RestSCC,
ArgNum1, Module, PassInfo)
).
:- pred init_rec_input_suppliers_single_arg(pred_proc_id::in,
list(pred_proc_id)::in, int::in, module_info::in, used_args::out)
is semidet.
init_rec_input_suppliers_single_arg(TrialPPId, RestSCC, ArgNum, Module,
RecSupplierMap) :-
TrialPPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
proc_info_argmodes(ProcInfo, ArgModes),
init_rec_input_suppliers_add_single_arg(ArgModes, ArgNum,
Module, TrialPPIdRecSuppliers),
map__init(RecSupplierMap0),
map__det_insert(RecSupplierMap0, TrialPPId, TrialPPIdRecSuppliers,
RecSupplierMap1),
init_rec_input_suppliers_single_arg_others(RestSCC, Module,
RecSupplierMap1, RecSupplierMap).
:- pred init_rec_input_suppliers_add_single_arg(list(mode)::in, int::in,
module_info::in, list(bool)::out) is semidet.
init_rec_input_suppliers_add_single_arg([Mode | Modes], ArgNum, Module,
BoolList) :-
(
mode_is_input(Module, Mode),
ArgNum = 1
->
MapToNo = lambda([_Mode::in, Bool::out] is det,
(
Bool = no
)),
list__map(MapToNo, Modes, BoolList1),
BoolList = [yes | BoolList1]
;
(
mode_is_output(Module, Mode)
->
NextArgNum = ArgNum
;
mode_is_input(Module, Mode),
ArgNum > 1
->
NextArgNum is ArgNum - 1
;
fail
)
->
init_rec_input_suppliers_add_single_arg(Modes, NextArgNum,
Module, BoolList1),
BoolList = [no | BoolList1]
;
fail
).
:- pred init_rec_input_suppliers_single_arg_others(list(pred_proc_id)::in,
module_info::in, used_args::in, used_args::out) is det.
init_rec_input_suppliers_single_arg_others([], _,
RecSupplierMap, RecSupplierMap).
init_rec_input_suppliers_single_arg_others([PPId | PPIds], Module,
RecSupplierMap0, RecSupplierMap) :-
PPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
proc_info_headvars(ProcInfo, HeadVars),
MapToNo = lambda([_HeadVar::in, Bool::out] is det,
(
Bool = no
)),
list__map(MapToNo, HeadVars, BoolList),
map__det_insert(RecSupplierMap0, PPId, BoolList, RecSupplierMap1),
init_rec_input_suppliers_single_arg_others(PPIds, Module,
RecSupplierMap1, RecSupplierMap).
:- pred lookup_proc_arity(pred_proc_id::in, module_info::in, int::out) is det.
lookup_proc_arity(PPId, Module, Arity) :-
PPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
proc_info_headvars(ProcInfo, HeadVars),
list__length(HeadVars, Arity).
%-----------------------------------------------------------------------------
:- pred prove_termination_in_scc_trial(list(pred_proc_id)::in, used_args::in,
fixpoint_dir::in, module_info::in, pass_info::in,
termination_info::out) is det.
prove_termination_in_scc_trial(SCC, InitRecSuppliers, FixDir, Module,
PassInfo, Termination) :-
prove_termination_in_scc_fixpoint(SCC, FixDir, Module, PassInfo,
InitRecSuppliers, Result),
(
Result = ok(CallInfo, _),
CallInfo = InfCalls - CallWeights,
(
InfCalls \= []
->
PassInfo = pass_info(_, MaxErrors, _),
list__take_upto(MaxErrors, InfCalls, ReportedInfCalls),
Termination = can_loop(ReportedInfCalls)
;
zero_or_positive_weight_cycles(CallWeights, Module,
Cycles),
Cycles \= []
->
PassInfo = pass_info(_, MaxErrors, _),
list__take_upto(MaxErrors, Cycles, ReportedCycles),
Termination = can_loop(ReportedCycles)
;
Termination = cannot_loop
)
;
Result = error(Errors),
Termination = can_loop(Errors)
).
%-----------------------------------------------------------------------------
:- pred prove_termination_in_scc_fixpoint(list(pred_proc_id)::in,
fixpoint_dir::in, module_info::in, pass_info::in, used_args::in,
pass2_result::out) is det.
prove_termination_in_scc_fixpoint(SCC, FixDir, Module, PassInfo,
RecSupplierMap0, Result) :-
% unsafe_perform_io(io__write_string("prove_termination_in_scc\n")),
% unsafe_perform_io(io__write(RecSupplierMap0)),
% unsafe_perform_io(io__write_string("\n")),
map__init(NewRecSupplierMap0),
map__init(CallWeightGraph0),
CallInfo0 = [] - CallWeightGraph0,
prove_termination_in_scc_pass(SCC, FixDir, Module, PassInfo,
RecSupplierMap0, NewRecSupplierMap0, CallInfo0, Result1),
(
Result1 = ok(_, RecSupplierMap1),
( RecSupplierMap1 = RecSupplierMap0 ->
% We are at a fixed point, so further analysis
% will not get any better results.
Result = Result1
;
prove_termination_in_scc_fixpoint(SCC, FixDir,
Module, PassInfo, RecSupplierMap1, Result)
)
;
Result1 = error(_),
Result = Result1
).
%-----------------------------------------------------------------------------
% Process a whole SCC, to determine the termination property of each
% procedure in that SCC.
:- pred prove_termination_in_scc_pass(list(pred_proc_id)::in, fixpoint_dir::in,
module_info::in, pass_info::in, used_args::in, used_args::in,
call_weight_info::in, pass2_result::out) is det.
prove_termination_in_scc_pass([], _, _, _, _, NewRecSupplierMap, CallInfo,
ok(CallInfo, NewRecSupplierMap)).
prove_termination_in_scc_pass([PPId | PPIds], FixDir, Module, PassInfo,
RecSupplierMap, NewRecSupplierMap0, CallInfo0, Result) :-
% Get the goal info.
PPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, PredInfo, ProcInfo),
pred_info_context(PredInfo, Context),
proc_info_goal(ProcInfo, Goal),
proc_info_vartypes(ProcInfo, VarTypes),
map__init(EmptyMap),
PassInfo = pass_info(FunctorInfo, MaxErrors, MaxPaths),
init_traversal_params(Module, FunctorInfo, PPId, Context, VarTypes,
EmptyMap, RecSupplierMap, MaxErrors, MaxPaths, Params),
set__init(PathSet0),
Info0 = ok(PathSet0, []),
traverse_goal(Goal, Params, Info0, Info),
(
Info = ok(Paths, CanLoop),
require(unify(CanLoop, []),
"can_loop detected in pass2 but not pass1"),
set__to_sorted_list(Paths, PathList),
upper_bound_active_vars(PathList, ActiveVars),
map__lookup(RecSupplierMap, PPId, RecSuppliers0),
proc_info_headvars(ProcInfo, Args),
bag__init(EmptyBag),
update_rec_input_suppliers(Args, ActiveVars, FixDir,
RecSuppliers0, RecSuppliers,
EmptyBag, RecSuppliers0Bag),
map__det_insert(NewRecSupplierMap0, PPId, RecSuppliers,
NewRecSupplierMap1),
add_call_arcs(PathList, RecSuppliers0Bag,
CallInfo0, CallInfo1),
prove_termination_in_scc_pass(PPIds, FixDir, Module,
PassInfo, RecSupplierMap,
NewRecSupplierMap1, CallInfo1, Result)
;
Info = error(Errors, CanLoop),
require(unify(CanLoop, []),
"can_loop detected in pass2 but not pass1"),
Result = error(Errors)
).
%-----------------------------------------------------------------------------
:- pred update_rec_input_suppliers(list(var)::in, bag(var)::in,
fixpoint_dir::in, list(bool)::in, list(bool)::out,
bag(var)::in, bag(var)::out) is det.
update_rec_input_suppliers([], _, _, [], [], RecBag, RecBag).
update_rec_input_suppliers([_ | _], _, _, [], [], _, _) :-
error("update_rec_input_suppliers: Unmatched variables").
update_rec_input_suppliers([], _, _, [_ | _], [], _, _) :-
error("update_rec_input_suppliers: Unmatched variables").
update_rec_input_suppliers([Arg | Args], ActiveVars, FixDir,
[RecInputSupplier0 | RecInputSuppliers0],
[RecInputSupplier | RecInputSuppliers],
RecBag0, RecBag) :-
(
RecInputSupplier0 = yes,
bag__insert(RecBag0, Arg, RecBag1)
;
RecInputSupplier0 = no,
RecBag1 = RecBag0
),
(
FixDir = down,
% This guarantees that the set of rec input suppliers
% can only decrease.
( bag__contains(ActiveVars, Arg) ->
RecInputSupplier = RecInputSupplier0
;
RecInputSupplier = no
)
;
FixDir = up,
% This guarantees that the set of rec input suppliers
% can only increase.
( bag__contains(ActiveVars, Arg) ->
RecInputSupplier = yes
;
RecInputSupplier = RecInputSupplier0
)
),
update_rec_input_suppliers(Args, ActiveVars, FixDir,
RecInputSuppliers0, RecInputSuppliers, RecBag1, RecBag).
%-----------------------------------------------------------------------------
% This adds the information from a stage 2 traversal to the graph.
% The graph's nodes are the procedures in the current SCC.
% The graph's edges represent calls from one procedure in the SCC to another.
% The number attached to the edge from p to q shows the upper bound
% on the difference between the size of the recursive input supplier arguments
% in the call to q and the size of the recursive input supplier arguments
% in the head of p. If there is no finite upper bound, then we insert the
% details of the call into the list of "infinite" calls.
:- pred add_call_arcs(list(path_info)::in,
bag(var)::in, call_weight_info::in, call_weight_info::out) is det.
add_call_arcs([], _RecInputSuppliers, CallInfo, CallInfo).
add_call_arcs([Path | Paths], RecInputSuppliers, CallInfo0, CallInfo) :-
Path = path_info(PPId, CallSite, GammaConst, GammaVars, ActiveVars),
( CallSite = yes(CallPPIdPrime - ContextPrime) ->
CallPPId = CallPPIdPrime,
Context = ContextPrime
;
error("no call site in path in stage 2")
),
( GammaVars = [] ->
true
;
error("gamma variables in path in stage 2")
),
CallInfo0 = InfCalls0 - CallWeights0,
( bag__is_subbag(ActiveVars, RecInputSuppliers) ->
( map__search(CallWeights0, PPId, NeighbourMap0) ->
( map__search(NeighbourMap0, CallPPId, OldEdgeInfo) ->
OldEdgeInfo = _OldContext - OldWeight,
( OldWeight >= GammaConst ->
EdgeInfo = OldEdgeInfo
;
EdgeInfo = Context - GammaConst
),
map__det_update(NeighbourMap0, CallPPId,
EdgeInfo, NeighbourMap)
;
map__det_insert(NeighbourMap0, CallPPId,
Context - GammaConst, NeighbourMap)
),
map__det_update(CallWeights0, PPId, NeighbourMap,
CallWeights1)
;
map__init(NeighbourMap0),
map__det_insert(NeighbourMap0, CallPPId,
Context - GammaConst, NeighbourMap),
map__det_insert(CallWeights0, PPId, NeighbourMap,
CallWeights1)
),
CallInfo1 = InfCalls0 - CallWeights1
;
InfCalls1 = [Context - inf_call(PPId, CallPPId) | InfCalls0],
CallInfo1 = InfCalls1 - CallWeights0
),
add_call_arcs(Paths, RecInputSuppliers, CallInfo1, CallInfo).
%-----------------------------------------------------------------------------
% We use a simple depth first search to find and return the list
% of all cycles in the call graph of the SCC where the change in
% the size of the recursive input supplier arguments of the procedure
% that serves as the start and end point of the circularity are
% not guaranteed to decrease.
%
% Finding one such cycle is enough for us to conclude that we
% cannot prove termination of the procedures in the SCC; we collect
% all cycles because it may be useful to print them out (if not
% all, then maybe a limited set).
:- pred zero_or_positive_weight_cycles(call_weight_graph::in,
module_info::in, list(term_errors__error)::out) is det.
zero_or_positive_weight_cycles(CallWeights, Module, Cycles) :-
map__keys(CallWeights, PPIds),
zero_or_positive_weight_cycles_2(PPIds, CallWeights, Module, Cycles).
:- pred zero_or_positive_weight_cycles_2(list(pred_proc_id)::in,
call_weight_graph::in, module_info::in,
list(term_errors__error)::out) is det.
zero_or_positive_weight_cycles_2([], _, _, []).
zero_or_positive_weight_cycles_2([PPId | PPIds], CallWeights, Module, Cycles) :-
zero_or_positive_weight_cycles_from(PPId, CallWeights, Module, Cycles1),
zero_or_positive_weight_cycles_2(PPIds, CallWeights, Module, Cycles2),
list__append(Cycles1, Cycles2, Cycles).
:- pred zero_or_positive_weight_cycles_from(pred_proc_id::in,
call_weight_graph::in, module_info::in,
list(term_errors__error)::out) is det.
zero_or_positive_weight_cycles_from(PPId, CallWeights, Module, Cycles) :-
map__lookup(CallWeights, PPId, NeighboursMap),
map__to_assoc_list(NeighboursMap, NeighboursList),
PPId = proc(PredId, _ProcId),
module_info_pred_info(Module, PredId, PredInfo),
pred_info_context(PredInfo, Context),
zero_or_positive_weight_cycles_from_neighbours(NeighboursList,
PPId, Context, 0, [], CallWeights, Cycles).
:- pred zero_or_positive_weight_cycles_from_neighbours(assoc_list(pred_proc_id,
pair(term__context, int))::in, pred_proc_id::in, term__context::in,
int::in, assoc_list(pred_proc_id, term__context)::in,
call_weight_graph::in, list(term_errors__error)::out) is det.
zero_or_positive_weight_cycles_from_neighbours([], _, _, _, _, _, []).
zero_or_positive_weight_cycles_from_neighbours([Neighbour | Neighbours],
LookforPPId, Context, WeightSoFar, VisitedCalls, CallWeights,
Cycles) :-
zero_or_positive_weight_cycles_from_neighbour(Neighbour, LookforPPId,
Context, WeightSoFar, VisitedCalls, CallWeights, Cycles1),
zero_or_positive_weight_cycles_from_neighbours(Neighbours, LookforPPId,
Context, WeightSoFar, VisitedCalls, CallWeights, Cycles2),
list__append(Cycles1, Cycles2, Cycles).
:- pred zero_or_positive_weight_cycles_from_neighbour(pair(pred_proc_id,
pair(term__context, int))::in, pred_proc_id::in, term__context::in,
int::in, assoc_list(pred_proc_id, term__context)::in,
call_weight_graph::in, list(term_errors__error)::out) is det.
zero_or_positive_weight_cycles_from_neighbour(CurPPId - (Context - EdgeWeight),
LookforPPId, ProcContext, WeightSoFar0, VisitedCalls,
CallWeights, Cycles) :-
WeightSoFar1 is WeightSoFar0 + EdgeWeight,
(
CurPPId = LookforPPId
->
% We have a cycle on the looked for ppid.
( WeightSoFar1 >= 0 ->
FinalVisitedCalls = [CurPPId - Context | VisitedCalls],
list__reverse(FinalVisitedCalls, RevFinalVisitedCalls),
Cycles = [ProcContext -
cycle(LookforPPId, RevFinalVisitedCalls)]
;
Cycles = []
)
;
assoc_list__keys(VisitedCalls, VisitedPPIds),
list__member(CurPPId, VisitedPPIds)
->
% We have a cycle, but not on the looked for ppid.
% We ignore it here; it will be picked up when we process
% that ppid.
Cycles = []
;
% No cycle; try all possible edges from this node.
NewVisitedCalls = [CurPPId - Context | VisitedCalls],
map__lookup(CallWeights, CurPPId, NeighboursMap),
map__to_assoc_list(NeighboursMap, NeighboursList),
zero_or_positive_weight_cycles_from_neighbours(NeighboursList,
LookforPPId, ProcContext, WeightSoFar1,
NewVisitedCalls, CallWeights, Cycles)
).
%-----------------------------------------------------------------------------
%-----------------------------------------------------------------------------%
% 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_traversal.m
%
% Main author: crs.
% Significant rewrite by zs.
%
% This module contains the code used to traverse procedure bodies
% for both passes of termination analysis.
%
% For details, please refer to the papers mentioned in termination.m.
%
%-----------------------------------------------------------------------------%
:- module term_traversal.
:- interface.
:- import_module term_util, term_errors.
:- import_module hlds_module, hlds_pred, hlds_goal, prog_data.
:- import_module list, bag, map, std_util, term.
:- type traversal_info
---> ok(
set(path_info),
% Information about the paths we have
% followed. With a conjunction of
% length N, each of whose elements is
% a branched control structure, the
% number of paths through the
% conjunction is 2^N. The reason why
% we use a set of path_infos instead
% of a list is that this can postpone
% the representation getting too big
% if (as is at least moderately likely)
% many of the paths have identical
% properties.
list(term_errors__error)
% Have we processed a call to a
% procedure whose maybe termination
% info was yes(can_loop(_))?
% If yes, record the error here.
% (This is not an error in pass 1,
% but we want to find this out in
% pass 1 so we can avoid doing pass 2.)
)
; error(
list(term_errors__error),
% Errors which are fatal in both
% passes.
list(term_errors__error)
% Have we processed a call to a
% procedure whose maybe termination
% info was yes(can_loop(_))?
% If yes, record the error here.
% (This is not an error in pass 1,
% but we want to find this out in
% pass 1 so we can avoid doing pass 2.)
).
:- type path_info
---> path_info(
pred_proc_id, % The identify of the procedure
% that this path is within.
maybe(pair(pred_proc_id, term__context)),
% If no, path was started at the end
% of the procedure given by field 1.
% If yes, the arg names the procedure
% at the call to which the path started
% and the context of the call.
% In pass 1, all starts should be no.
% In pass 2, all starts should be yes.
int,
list(pred_proc_id),
bag(var)
% These three fields describe the
% right hand side of the inequation
% we are propagating.
).
:- type traversal_params.
:- pred init_traversal_params(module_info::in, functor_info::in,
pred_proc_id::in, term__context::in, map(var, type)::in,
used_args::in, used_args::in, int::in, int::in,
traversal_params::out) is det.
:- pred traverse_goal(hlds_goal::in, traversal_params::in,
traversal_info::in, traversal_info::out) is det.
:- pred upper_bound_active_vars(list(path_info)::in, bag(var)::out) is det.
:- implementation.
:- import_module hlds_data, type_util.
:- import_module bool, int, set, require.
traverse_goal(Goal, Params, Info0, Info) :-
Goal = GoalExpr - GoalInfo,
(
goal_info_get_determinism(GoalInfo, Detism),
determinism_components(Detism, _, at_most_zero)
->
cannot_succeed(Info0, Info1)
;
Info1 = Info0
),
traverse_goal_2(GoalExpr, GoalInfo, Params, Info1, Info).
:- pred traverse_goal_2(hlds_goal_expr::in, hlds_goal_info::in,
traversal_params::in, traversal_info::in, traversal_info::out) is det.
traverse_goal_2(unify(_Var, _RHS, _UniMode, Unification, _Context),
_GoalInfo, Params, Info0, Info) :-
(
Unification = construct(OutVar, ConsId, Args, Modes),
(
unify_change(OutVar, ConsId, Args, Modes, Params,
Gamma, InVars, OutVars0)
->
bag__insert(OutVars0, OutVar, OutVars),
record_change(InVars, OutVars, Gamma, [], Info0, Info)
;
% length(Args) is not necessarily equal to length(Modes)
% for higher order constructions.
Info = Info0
)
;
Unification = deconstruct(InVar, ConsId, Args, Modes, _),
(
unify_change(InVar, ConsId, Args, Modes, Params,
Gamma0, InVars0, OutVars)
->
bag__insert(InVars0, InVar, InVars),
Gamma is 0 - Gamma0,
record_change(InVars, OutVars, Gamma, [], Info0, Info)
;
error("higher order deconstruction")
)
;
Unification = assign(OutVar, InVar),
bag__init(Empty),
bag__insert(Empty, InVar, InVars),
bag__insert(Empty, OutVar, OutVars),
record_change(InVars, OutVars, 0, [], Info0, Info)
;
Unification = simple_test(_InVar1, _InVar2),
Info = Info0
;
Unification = complicated_unify(_, _),
error("Unexpected complicated_unify in termination analysis")
).
traverse_goal_2(conj(Goals), _, Params, Info0, Info) :-
list__reverse(Goals, RevGoals),
traverse_conj(RevGoals, Params, Info0, Info).
traverse_goal_2(switch(_, _, Cases, _), _, Params, Info0, Info) :-
traverse_switch(Cases, Params, Info0, Info).
traverse_goal_2(disj(Goals, _StoreMap), _, Params, Info0, Info) :-
traverse_disj(Goals, Params, Info0, Info).
traverse_goal_2(not(Goal), _, Params, Info0, Info) :-
% Since goal cannot bind any active variables,
% we don't need to traverse Goal for pass1,
% but it shouldn't hurt either.
traverse_goal(Goal, Params, Info0, Info).
traverse_goal_2(some(_Vars, Goal), _GoalInfo, Params, Info0, Info) :-
traverse_goal(Goal, Params, Info0, Info).
traverse_goal_2(if_then_else(_, Cond, Then, Else, _), _, Params, Info0, Info) :-
traverse_conj([Then, Cond], Params, Info0, Info1),
traverse_goal(Else, Params, Info0, Info2),
combine_paths(Info1, Info2, Params, Info).
traverse_goal_2(pragma_c_code(_, _, CallPredId, CallProcId, Args, _, _, _),
GoalInfo, Params, Info0, Info) :-
params_get_module_info(Params, Module),
module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
CallProcInfo),
proc_info_argmodes(CallProcInfo, CallArgModes),
partition_call_args(Module, CallArgModes, Args, _InVars, OutVars),
goal_info_get_context(GoalInfo, Context),
error_if_intersect(OutVars, Context, pragma_c_code, Info0, Info).
traverse_goal_2(higher_order_call(_, _, _, _, _, _),
GoalInfo, Params, Info0, Info) :-
goal_info_get_context(GoalInfo, Context),
add_error(Context, horder_call, Params, Info0, Info).
% For now, we'll pretend that the class method call is a higher order
% call. In reality, we could probably analyse further than this, since
% we know that the method being called must come from one of the
% instance declarations, and we could potentially (globally) analyse
% these.
traverse_goal_2(class_method_call(_, _, _, _, _, _),
GoalInfo, Params, Info0, Info) :-
goal_info_get_context(GoalInfo, Context),
add_error(Context, horder_call, Params, Info0, Info).
traverse_goal_2(call(CallPredId, CallProcId, Args, _, _, _),
GoalInfo, Params, Info0, Info) :-
goal_info_get_context(GoalInfo, Context),
params_get_module_info(Params, Module),
params_get_ppid(Params, PPId),
CallPPId = proc(CallPredId, CallProcId),
module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
CallProcInfo),
proc_info_argmodes(CallProcInfo, CallArgModes),
proc_info_get_maybe_arg_size_info(CallProcInfo, CallArgSizeInfo),
proc_info_get_maybe_termination_info(CallProcInfo, CallTerminationInfo),
partition_call_args(Module, CallArgModes, Args, InVars, OutVars),
% Handle existing paths
(
CallArgSizeInfo = yes(finite(CallGamma, OutputSuppliers)),
remove_unused_args(InVars, Args, OutputSuppliers, UsedInVars),
record_change(UsedInVars, OutVars, CallGamma, [], Info0, Info1)
;
CallArgSizeInfo = yes(infinite(_)),
error_if_intersect(OutVars, Context,
inf_termination_const(PPId, CallPPId), Info0, Info1)
;
CallArgSizeInfo = no,
% We should get to this point only in pass 1.
% In pass 2, OutputSuppliersMap will be empty,
% which will lead to a runtime abort in map__lookup.
params_get_output_suppliers(Params, OutputSuppliersMap),
map__lookup(OutputSuppliersMap, CallPPId, OutputSuppliers),
remove_unused_args(InVars, Args, OutputSuppliers, UsedInVars),
record_change(UsedInVars, OutVars, 0, [CallPPId], Info0, Info1)
),
% Did we call a non-terminating procedure?
(
CallTerminationInfo = yes(can_loop(_))
->
called_can_loop(Context, can_loop_proc_called(PPId, CallPPId),
Params, Info1, Info2)
;
Info2 = Info1
),
% Did we call a procedure with some procedure-valued arguments?
(
% This is an overapproximation, since it includes
% higher order outputs. XXX
params_get_var_types(Params, VarTypes),
horder_vars(Args, VarTypes)
->
add_error(Context, horder_args(PPId, CallPPId), Params,
Info2, Info3)
;
Info3 = Info2
),
% Do we start another path?
(
params_get_rec_input_suppliers(Params, RecInputSuppliersMap),
map__search(RecInputSuppliersMap, CallPPId, RecInputSuppliers)
->
% We should get to this point only in pass 2, and then
% only if this call is to a procedure in the current SCC.
% In pass 1, RecInputSuppliersMap will be empty.
compute_rec_start_vars(Args, RecInputSuppliers, Bag),
PathStart = yes(CallPPId - Context),
NewPath = path_info(PPId, PathStart, 0, [], Bag),
add_path(NewPath, Info3, Info)
;
Info = Info3
).
%-----------------------------------------------------------------------------%
% Traverse_conj should be invoked with a reversed list of goals.
% This is to keep stack consumption down.
:- pred traverse_conj(list(hlds_goal)::in, traversal_params::in,
traversal_info::in, traversal_info::out) is det.
traverse_conj([], _, Info, Info).
traverse_conj([Goal | Goals], Params, Info0, Info) :-
traverse_goal(Goal, Params, Info0, Info1),
traverse_conj(Goals, Params, Info1, Info).
:- pred traverse_disj(list(hlds_goal)::in, traversal_params::in,
traversal_info::in, traversal_info::out) is det.
traverse_disj([], _, _, ok(Empty, [])) :-
set__init(Empty).
traverse_disj([Goal | Goals], Params, Info0, Info) :-
traverse_goal(Goal, Params, Info0, Info1),
traverse_disj(Goals, Params, Info0, Info2),
combine_paths(Info1, Info2, Params, Info).
:- pred traverse_switch(list(case)::in, traversal_params::in,
traversal_info::in, traversal_info::out) is det.
traverse_switch([], _, _, ok(Empty, [])) :-
set__init(Empty).
traverse_switch([case(_, Goal) | Cases], Params, Info0, Info) :-
traverse_goal(Goal, Params, Info0, Info1),
traverse_switch(Cases, Params, Info0, Info2),
combine_paths(Info1, Info2, Params, Info).
%-----------------------------------------------------------------------------%
:- pred cannot_succeed(traversal_info::in, traversal_info::out) is det.
cannot_succeed(error(Errors, CanLoop), error(Errors, CanLoop)).
cannot_succeed(ok(_, CanLoop), ok(Empty, CanLoop)) :-
set__init(Empty).
:- pred add_path(path_info::in, traversal_info::in, traversal_info::out) is det.
add_path(_, error(Errors, CanLoop), error(Errors, CanLoop)).
add_path(Path, ok(Paths0, CanLoop), ok(Paths, CanLoop)) :-
set__insert(Paths0, Path, Paths).
:- pred add_error(term__context::in, termination_error::in,
traversal_params::in, traversal_info::in, traversal_info::out) is det.
add_error(Context, Error, Params, error(Errors0, CanLoop),
error(Errors, CanLoop)) :-
Errors1 = [Context - Error | Errors0],
params_get_max_errors(Params, MaxErrors),
list__take_upto(MaxErrors, Errors1, Errors).
add_error(Context, Error, _, ok(_, CanLoop),
error([Context - Error], CanLoop)).
:- pred called_can_loop(term__context::in, termination_error::in,
traversal_params::in, traversal_info::in, traversal_info::out) is det.
called_can_loop(Context, Error, Params, error(Errors, CanLoop0),
error(Errors, CanLoop)) :-
CanLoop1 = [Context - Error | CanLoop0],
params_get_max_errors(Params, MaxErrors),
list__take_upto(MaxErrors, CanLoop1, CanLoop).
called_can_loop(Context, Error, Params, ok(Paths, CanLoop0),
ok(Paths, CanLoop)) :-
CanLoop1 = [Context - Error | CanLoop0],
params_get_max_errors(Params, MaxErrors),
list__take_upto(MaxErrors, CanLoop1, CanLoop).
:- pred combine_paths(traversal_info::in, traversal_info::in,
traversal_params::in, traversal_info::out) is det.
combine_paths(error(Errors1, CanLoop1), error(Errors2, CanLoop2), Params,
error(Errors, CanLoop)) :-
params_get_max_errors(Params, MaxErrors),
list__append(Errors1, Errors2, Errors3),
list__take_upto(MaxErrors, Errors3, Errors),
list__append(CanLoop1, CanLoop2, CanLoop3),
list__take_upto(MaxErrors, CanLoop3, CanLoop).
combine_paths(error(Errors1, CanLoop1), ok(_, CanLoop2), Params,
error(Errors1, CanLoop)) :-
params_get_max_errors(Params, MaxErrors),
list__append(CanLoop1, CanLoop2, CanLoop3),
list__take_upto(MaxErrors, CanLoop3, CanLoop).
combine_paths(ok(_, CanLoop1), error(Errors2, CanLoop2), Params,
error(Errors2, CanLoop)) :-
params_get_max_errors(Params, MaxErrors),
list__append(CanLoop1, CanLoop2, CanLoop3),
list__take_upto(MaxErrors, CanLoop3, CanLoop).
combine_paths(ok(Paths1, CanLoop1), ok(Paths2, CanLoop2), Params,
Info) :-
params_get_max_errors(Params, MaxErrors),
list__append(CanLoop1, CanLoop2, CanLoop3),
list__take_upto(MaxErrors, CanLoop3, CanLoop),
set__union(Paths2, Paths1, Paths),
params_get_max_paths(Params, MaxPaths),
(
% Don't try to track the state of too many paths;
% doing so can require too much memory.
set__count(Paths, Count),
Count =< MaxPaths
->
Info = ok(Paths, CanLoop)
;
params_get_context(Params, Context),
Info = error([Context - too_many_paths], CanLoop)
).
%-----------------------------------------------------------------------------%
:- pred compute_rec_start_vars(list(var)::in, list(bool)::in,
bag(var)::out) is det.
compute_rec_start_vars([], [], Out) :-
bag__init(Out).
compute_rec_start_vars([_|_], [], _Out) :-
error("Unmatched vars in compute_rec_start_vars\n").
compute_rec_start_vars([], [_|_], _Out) :-
error("Unmatched vars in compute_rec_start_vars\n").
compute_rec_start_vars([Var | Vars], [RecInputSupplier | RecInputSuppliers],
Out) :-
compute_rec_start_vars(Vars, RecInputSuppliers, Out1),
( RecInputSupplier = yes ->
bag__insert(Out1, Var, Out)
;
Out = Out1
).
%-----------------------------------------------------------------------------%
% unify_change is invoked for unifications of the form X = f(Yi),
% with the first argument giving the identity of X, the second the
% identity of f, the third and fourth the identity and modes of the Yi.
% unify_change returns the norm of f and the bags of input and output
% variables among the Yi. It is up to the caller to look after the
% sign of the norm of f and after the membership of X in either the
% input or output bags. The predicate fails if invoked on a higher
% order unification.
:- pred unify_change(var::in, cons_id::in, list(var)::in, list(uni_mode)::in,
traversal_params::in, int::out, bag(var)::out, bag(var)::out)
is semidet.
unify_change(OutVar, ConsId, Args0, Modes0, Params, Gamma, InVars, OutVars) :-
params_get_functor_info(Params, FunctorInfo),
params_get_var_types(Params, VarTypes),
map__lookup(VarTypes, OutVar, Type),
\+ type_is_higher_order(Type, _, _),
( type_to_type_id(Type, TypeId, _) ->
params_get_module_info(Params, Module),
functor_norm(FunctorInfo, TypeId, ConsId, Module,
Gamma, Args0, Args, Modes0, Modes),
split_unification_vars(Args, Modes, Module, InVars, OutVars)
;
error("variable type in traverse_goal_2")
).
%-----------------------------------------------------------------------------%
:- pred record_change(bag(var)::in, bag(var)::in, int::in,
list(pred_proc_id)::in, traversal_info::in, traversal_info::out) is det.
record_change(_, _, _, _, error(Errors, CanLoop), error(Errors, CanLoop)).
record_change(InVars, OutVars, Gamma, CalledPPIds, ok(Paths0, CanLoop),
ok(NewPaths, CanLoop)) :-
set__to_sorted_list(Paths0, PathsList0),
set__init(NewPaths0),
record_change_2(PathsList0, InVars, OutVars, Gamma, CalledPPIds,
NewPaths0, NewPaths).
:- pred record_change_2(list(path_info)::in, bag(var)::in, bag(var)::in,
int::in, list(pred_proc_id)::in,
set(path_info)::in, set(path_info)::out) is det.
record_change_2([], _, _, _, _, PathSet, PathSet).
record_change_2([Path0 | Paths0], InVars, OutVars, CallGamma, CallPPIds,
PathSet0, PathSet) :-
Path0 = path_info(ProcData, Start, Gamma0, PPIds0, Vars0),
( bag__intersect(OutVars, Vars0) ->
% The change produces some active variables.
Gamma is CallGamma + Gamma0,
list__append(CallPPIds, PPIds0, PPIds),
bag__subtract(Vars0, OutVars, Vars1),
bag__union(InVars, Vars1, Vars),
Path = path_info(ProcData, Start, Gamma, PPIds, Vars)
;
% The change produces no active variables.
Path = Path0
),
set__insert(PathSet0, Path, PathSet1),
record_change_2(Paths0, InVars, OutVars, CallGamma, CallPPIds,
PathSet1, PathSet).
%-----------------------------------------------------------------------------%
:- pred error_if_intersect(bag(var)::in, term__context::in,
termination_error::in, traversal_info::in, traversal_info::out) is det.
error_if_intersect(_, _, _, error(Errors, CanLoop), error(Errors, CanLoop)).
error_if_intersect(OutVars, Context, ErrorMsg, ok(Paths, CanLoop), Info)
:-
(
set__to_sorted_list(Paths, PathList),
some_active_vars_in_bag(PathList, OutVars)
->
Info = error([Context - ErrorMsg], CanLoop)
;
Info = ok(Paths, CanLoop)
).
:- pred some_active_vars_in_bag(list(path_info)::in, bag(var)::in) is semidet.
some_active_vars_in_bag([Path | Paths], OutVars) :-
(
Path = path_info(_, _, _, _, Vars),
bag__intersect(Vars, OutVars)
;
some_active_vars_in_bag(Paths, OutVars)
).
%-----------------------------------------------------------------------------%
upper_bound_active_vars([], ActiveVars) :-
bag__init(ActiveVars).
upper_bound_active_vars([Path | Paths], ActiveVars) :-
upper_bound_active_vars(Paths, ActiveVars1),
Path = path_info(_, _, _, _, ActiveVars2),
bag__least_upper_bound(ActiveVars1, ActiveVars2, ActiveVars).
%-----------------------------------------------------------------------------%
:- type traversal_params
---> traversal_params(
module_info,
functor_info,
pred_proc_id, % The procedure we are tracing through.
term__context, % The context of the procedure.
map(var, type),
map(pred_proc_id, list(bool)),
% Output suppliers of each procedure.
% Empty during pass 2.
map(pred_proc_id, list(bool)),
% Rec input suppliers of each procedure.
% Empty during pass 1.
int, % Max number of errors to gather.
int % Max number of paths to analyze.
).
init_traversal_params(ModuleInfo, FunctorInfo, PredProcId, Context, VarTypes,
OutputSuppliers, RecInputSuppliers, MaxErrors, MaxPaths,
Params) :-
Params = traversal_params(ModuleInfo, FunctorInfo, PredProcId, Context,
VarTypes, OutputSuppliers, RecInputSuppliers,
MaxErrors, MaxPaths).
:- pred params_get_module_info(traversal_params::in, module_info::out)
is det.
:- pred params_get_functor_info(traversal_params::in, functor_info::out)
is det.
:- pred params_get_ppid(traversal_params::in, pred_proc_id::out)
is det.
:- pred params_get_context(traversal_params::in, term__context::out)
is det.
:- pred params_get_var_types(traversal_params::in, map(var, type)::out)
is det.
:- pred params_get_output_suppliers(traversal_params::in,
map(pred_proc_id, list(bool))::out) is det.
:- pred params_get_rec_input_suppliers(traversal_params::in,
map(pred_proc_id, list(bool))::out) is det.
:- pred params_get_max_errors(traversal_params::in, int::out) is det.
:- pred params_get_max_paths(traversal_params::in, int::out) is det.
params_get_module_info(Params, A) :-
Params = traversal_params(A, _, _, _, _, _, _, _, _).
params_get_functor_info(Params, B) :-
Params = traversal_params(_, B, _, _, _, _, _, _, _).
params_get_ppid(Params, C) :-
Params = traversal_params(_, _, C, _, _, _, _, _, _).
params_get_context(Params, D) :-
Params = traversal_params(_, _, _, D, _, _, _, _, _).
params_get_var_types(Params, E) :-
Params = traversal_params(_, _, _, _, E, _, _, _, _).
params_get_output_suppliers(Params, F) :-
Params = traversal_params(_, _, _, _, _, F, _, _, _).
params_get_rec_input_suppliers(Params, G) :-
Params = traversal_params(_, _, _, _, _, _, G, _, _).
params_get_max_errors(Params, H) :-
Params = traversal_params(_, _, _, _, _, _, _, H, _).
params_get_max_paths(Params, I) :-
Params = traversal_params(_, _, _, _, _, _, _, _, I).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
% 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 module:
%
% - defines the types used by termination analysis
% - defines predicates for computing functor norms
% - defines some utility predicates
%
%-----------------------------------------------------------------------------%
:- module term_util.
:- interface.
:- import_module term_errors, prog_data.
:- import_module hlds_module, hlds_pred, hlds_data, hlds_goal.
:- import_module bool, int, list, map, bag, term.
%-----------------------------------------------------------------------------%
% The arg size info defines an upper bound on the difference
% between the sizes of the output arguments of a procedure and the sizes
% of the input arguments:
%
% | input arguments | + constant >= | output arguments |
%
% where | | represents a semilinear norm.
:- type arg_size_info
---> finite(int, list(bool))
% The termination constant is a finite integer.
% The list of bool has a 1:1 correspondence
% with the input arguments of the procedure.
% It stores whether the argument contributes
% to the size of the output arguments.
; infinite(list(term_errors__error)).
% There is no finite integer for which the
% above equation is true. The argument says
% why the analysis failed to find a finite
% constant.
:- type termination_info
---> cannot_loop % This procedure terminates for all
% possible inputs.
; can_loop(list(term_errors__error)).
% The analysis could not prove that the
% procedure terminates.
:- type used_args == map(pred_proc_id, list(bool)).
%-----------------------------------------------------------------------------%
% We use semilinear norms (denoted by ||) to compute the sizes of terms.
% These have the form
%
% | f(t1, ... tn) | = weight(f) + sum of | ti |
% where i is an element of a set I, and I is a subset of {1, ... n}
%
% We currently support four kinds of semilinear norms.
:- type functor_info
---> simple % All non-constant functors have weight 1,
% while constants have weight 0.
% Use the size of all subterms (I = {1, ..., n}.
; total % All functors have weight = arity of the functor.
% Use the size of all subterms (I = {1, ..., n}.
; use_map(weight_table)
% The weight of each functor is given by the table.
% Use the size of all subterms (I = {1, ..., n}.
; use_map_and_args(weight_table).
% The weight of each functor is given by the table,
% and so is the set of arguments of the functor whose
% size should be counted (I is given by the table
% entry of the functor).
:- type unify_info == pair(map(var, type), functor_info).
:- type weight_info ---> weight(int, list(bool)).
:- type weight_table == map(pair(type_id, cons_id), weight_info).
:- pred find_weights(module_info::in, weight_table::out) is det.
% This predicate is computes the weight of a functor and the set of arguments
% of that functor whose sizes should be counted towards the size of the whole
% term.
:- pred functor_norm(functor_info::in, type_id::in, cons_id::in,
module_info::in, int::out, list(var)::in, list(var)::out,
list(uni_mode)::in, list(uni_mode)::out) is det.
:- type pass_info
---> pass_info(
functor_info,
int, % Max number of errors to gather.
int % Max number of paths to analyze.
).
%-----------------------------------------------------------------------------%
% 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::in, list(mode)::in, list(var)::in,
bag(var)::out, bag(var)::out) is det.
% 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)::in, list(uni_mode)::in,
module_info::in, bag(var)::out, bag(var)::out) 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)::in, list(bool)::in,
list(bool)::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.
% This predicate sets the argument size info of a given a list of procedures.
:- pred set_pred_proc_ids_arg_size_info(list(pred_proc_id)::in,
arg_size_info::in, module_info::in, module_info::out) is det.
% This predicate sets the termination info of a given a list of procedures.
:- pred set_pred_proc_ids_termination_info(list(pred_proc_id)::in,
termination_info::in, module_info::in, module_info::out) is det.
:- pred lookup_proc_termination_info(module_info::in, pred_proc_id::in,
maybe(termination_info)::out) is det.
:- pred lookup_proc_arg_size_info(module_info::in, pred_proc_id::in,
maybe(arg_size_info)::out) is det.
% Succeeds if one or more variables in the list are higher order.
:- pred horder_vars(list(var), map(var, type)).
:- mode horder_vars(in, in) is semidet.
% Succeeds if all values of the given type are zero size (for all norms).
:- pred zero_size_type(type, module_info).
:- mode zero_size_type(in, in) is semidet.
:- pred get_context_from_scc(list(pred_proc_id)::in, module_info::in,
term__context::out) is det.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- implementation.
:- import_module inst_match, prog_out, mode_util, type_util.
:- import_module globals, options.
:- import_module io, std_util, assoc_list, require.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
% Calculate the weight to be assigned to each function symbol for the
% use_map and use_map_and_args semilinear norms.
%
% Given a type definition such as
%
% :- type t(Tk) ---> f1(a11, ... a1n1) where n1 is the arity of f1
% ; ...
% ; fm(am1, ... amnm) where nm is the arity of fm
%
% we check, for each aij, whether its type is recursive (i.e. it is t with
% type variable arguments that are a permutation of Tk). The weight info
% we compute for each functor will have a boolean list that has a `yes'
% for each recursive argument and a `no' for each nonrecursive argument.
% The weight to be assigned to the functor is the number of nonrecursive
% arguments, except that we assign a weight of at least 1 to all functors
% which are not constants.
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).
%-----------------------------------------------------------------------------%
% 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(WeightMap), TypeId, ConsId, _Module, Int,
Args, Args, Modes, Modes) :-
( map__search(WeightMap, TypeId - ConsId, WeightInfo) ->
WeightInfo = weight(Int, _)
;
Int = 0
).
functor_norm(use_map_and_args(WeightMap), TypeId, ConsId, _Module, Int,
Args0, Args, Modes0, Modes) :-
( map__search(WeightMap, TypeId - ConsId, WeightInfo) ->
WeightInfo = weight(Int, UseArgList),
(
functor_norm_filter_args(UseArgList, Args0, Args1,
Modes0, Modes1)
->
Modes = Modes1,
Args = Args1
;
error("Unmatched lists in functor_norm_filter_args.")
)
;
Int = 0,
Modes = Modes0,
Args = Args0
).
% This predicate will fail if the length of the input lists are not matched.
:- pred functor_norm_filter_args(list(bool), list(var), list(var),
list(uni_mode), list(uni_mode)).
:- mode functor_norm_filter_args(in, in, out, in, out) is semidet.
functor_norm_filter_args([], [], [], [], []).
functor_norm_filter_args([yes | Bools], [Arg0 | Args0], [Arg0 | Args],
[Mode0 | Modes0], [Mode0 | Modes]) :-
functor_norm_filter_args(Bools, Args0, Args, Modes0, Modes).
functor_norm_filter_args([no | Bools], [_Arg0 | Args0], Args,
[_Mode0 | Modes0], Modes) :-
functor_norm_filter_args(Bools, Args0, Args, Modes0, Modes).
%-----------------------------------------------------------------------------%
partition_call_args(Module, ArgModes, Args, InVarsBag, OutVarsBag) :-
partition_call_args_2(Module, ArgModes, Args, InVars, OutVars),
bag__from_list(InVars, InVarsBag),
bag__from_list(OutVars, OutVarsBag).
:- pred partition_call_args_2(module_info::in, list(mode)::in, list(var)::in,
list(var)::out, list(var)::out) is det.
partition_call_args_2(_, [], [], [], []).
partition_call_args_2(_, [], [_ | _], _, _) :-
error("Unmatched variables in term_util:partition_call_args").
partition_call_args_2(_, [_ | _], [], _, _) :-
error("Unmatched variables in term_util__partition_call_args").
partition_call_args_2(ModuleInfo, [ArgMode | ArgModes], [Arg | Args],
InputArgs, OutputArgs) :-
partition_call_args_2(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
).
% 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")
).
%-----------------------------------------------------------------------------%
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).
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)
).
%-----------------------------------------------------------------------------%
set_pred_proc_ids_arg_size_info([], _ArgSize, Module, Module).
set_pred_proc_ids_arg_size_info([PPId | PPIds], ArgSize, 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_set_maybe_arg_size_info(ProcInfo0, yes(ArgSize), 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_arg_size_info(PPIds, ArgSize, Module1, Module).
set_pred_proc_ids_termination_info([], _Termination, Module, Module).
set_pred_proc_ids_termination_info([PPId | PPIds], Termination,
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_set_maybe_termination_info(ProcInfo0, yes(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_termination_info(PPIds, Termination,
Module1, Module).
lookup_proc_termination_info(Module, PredProcId, MaybeTermination) :-
PredProcId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
proc_info_get_maybe_termination_info(ProcInfo, MaybeTermination).
lookup_proc_arg_size_info(Module, PredProcId, MaybeArgSize) :-
PredProcId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
proc_info_get_maybe_arg_size_info(ProcInfo, MaybeArgSize).
horder_vars([Arg | Args], VarType) :-
(
map__lookup(VarType, Arg, Type),
type_is_higher_order(Type, _, _)
;
horder_vars(Args, VarType)
).
zero_size_type(Type, Module) :-
classify_type(Type, Module, TypeCategory),
zero_size_type_category(TypeCategory, Type, Module, yes).
% 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.
:- pred zero_size_type_category(builtin_type, type, module_info, bool).
:- mode zero_size_type_category(in, in, in, out) is det.
zero_size_type_category(int_type, _, _, yes).
zero_size_type_category(char_type, _, _, yes).
zero_size_type_category(str_type, _, _, yes).
zero_size_type_category(float_type, _, _, yes).
zero_size_type_category(pred_type, _, _, no).
zero_size_type_category(enum_type, _, _, yes).
zero_size_type_category(polymorphic_type, _, _, no).
zero_size_type_category(user_type, _, _, no).
%-----------------------------------------------------------------------------%
get_context_from_scc(SCC, Module, Context) :-
( SCC = [proc(PredId, _) | _] ->
module_info_pred_info(Module, PredId, PredInfo),
pred_info_context(PredInfo, Context)
;
error("Empty SCC in pass 2 of termination analysis")
).
%-----------------------------------------------------------------------------%
More information about the developers
mailing list