mirror of
https://github.com/Mercury-Language/mercury.git
synced 2026-04-15 01:13:30 +00:00
b560f66ab9
After this, I think all modules in the check_hlds package belong there.
compiler/inst_match.m:
compiler/mode_test.m:
Move these modules from the check_hlds package to the hlds package
because most of their uses are outside the semantic analysis passes
that the check_hlds package is intended to contain.
compiler/inst_merge.m:
Move this module from the check_hlds package to the hlds package
because it is imported by only two modules, instmap.m and inst_match.m,
and after this diff, both are in the hlds package.
compiler/implementation_defined_literals.m:
Move this module from the check_hlds package to the hlds package
because it does a straightforward program transformation that
does not have anything to do with semantic analysis (though its
invocation does happen between semantic analysis passes).
compiler/notes/compiler_design.html:
Update the documentation of the goal_path.m module. (I checked the
documentation of the moved modules, which did not need updates,
and found the need for this instead.)
compiler/*.m:
Conform to the changes above. (For many modules, this deletes
their import of the check_hlds package itself.)
634 lines
26 KiB
Mathematica
634 lines
26 KiB
Mathematica
%-----------------------------------------------------------------------------%
|
|
% vim: ft=mercury ts=4 sw=4 et
|
|
%-----------------------------------------------------------------------------%
|
|
% Copyright (C) 1997-1998, 2003-2008, 2010-2012 The University of Melbourne.
|
|
% Copyright (C) 2014-2018, 2022, 2025-2026 The Mercury team.
|
|
% This file may only be copied under the terms of the GNU General
|
|
% Public License - see the file COPYING in the Mercury distribution.
|
|
%-----------------------------------------------------------------------------%
|
|
%
|
|
% File: 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 transform_hlds.term_pass2.
|
|
:- interface.
|
|
|
|
:- import_module hlds.
|
|
:- import_module hlds.hlds_module.
|
|
:- import_module hlds.hlds_pred.
|
|
:- import_module transform_hlds.term_util.
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
% NOTE: This code assumes that the SCC does not call any nonterminating
|
|
% procedures. If it does then, that fact should have been detected
|
|
% during pass 1.
|
|
%
|
|
:- pred prove_termination_in_scc(module_info::in, pass_info::in,
|
|
scc::in, int::in, termination_info::out) is det.
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
:- implementation.
|
|
|
|
:- import_module hlds.goal_transform.
|
|
:- import_module hlds.mode_test.
|
|
:- import_module parse_tree.
|
|
:- import_module parse_tree.prog_data.
|
|
:- import_module parse_tree.prog_data_pragma.
|
|
:- import_module transform_hlds.term_errors.
|
|
:- import_module transform_hlds.term_traversal.
|
|
|
|
:- import_module assoc_list.
|
|
:- import_module bag.
|
|
:- import_module bool.
|
|
:- import_module int.
|
|
:- import_module list.
|
|
:- import_module map.
|
|
:- import_module maybe.
|
|
:- import_module pair.
|
|
:- import_module require.
|
|
:- import_module set.
|
|
:- import_module term.
|
|
:- import_module unit.
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
:- type term_pass2_result
|
|
---> term_pass2_ok(
|
|
call_weight_info,
|
|
used_args
|
|
)
|
|
; term_pass2_error(
|
|
list(term_error)
|
|
).
|
|
|
|
:- type call_weight_info
|
|
---> call_weight_info(list(term_error), call_weight_graph).
|
|
|
|
:- type call_weight_graph == map(pred_proc_id, call_weight_dst_map).
|
|
:- type call_weight_dst_map == map(pred_proc_id, call_weight_edge).
|
|
|
|
% The maximum non-infinite weight from proc to proc,
|
|
% and what context it occurs at.
|
|
%
|
|
:- type call_weight_edge
|
|
---> call_weight_edge(int, prog_context).
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
prove_termination_in_scc(ModuleInfo, PassInfo, SCC, SingleArgs, Termination) :-
|
|
set.to_sorted_list(SCC, SCCProcs),
|
|
init_rec_input_suppliers(SCCProcs, ModuleInfo, InitRecSuppliers),
|
|
prove_termination_in_scc_trial(ModuleInfo, PassInfo, down, SCCProcs,
|
|
InitRecSuppliers, Termination0),
|
|
(
|
|
Termination0 = can_loop(Errors),
|
|
( if
|
|
% 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(SCCProcs, ProcCount),
|
|
ProcCount =< SingleArgs,
|
|
|
|
% Don't try single arg analysis if it cannot cure the reason for
|
|
% the failure of the main analysis.
|
|
not (
|
|
list.member(Error, Errors),
|
|
Error = term_error(_, imported_pred)
|
|
)
|
|
then
|
|
prove_termination_in_scc_single_arg(ModuleInfo, SCCProcs, PassInfo,
|
|
SingleArgTerminates),
|
|
(
|
|
SingleArgTerminates = yes,
|
|
Termination = cannot_loop(unit)
|
|
;
|
|
SingleArgTerminates = no,
|
|
Termination = Termination0
|
|
)
|
|
else
|
|
Termination = Termination0
|
|
)
|
|
;
|
|
Termination0 = cannot_loop(unit),
|
|
Termination = Termination0
|
|
).
|
|
|
|
% 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], ModuleInfo, RecSupplierMap) :-
|
|
init_rec_input_suppliers(PPIds, ModuleInfo, RecSupplierMap0),
|
|
module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
|
|
proc_info_get_headvars(ProcInfo, HeadVars),
|
|
proc_info_get_argmodes(ProcInfo, ArgModes),
|
|
partition_call_args(ModuleInfo, ArgModes, HeadVars, InArgs, _OutVars),
|
|
MapIsInput =
|
|
( pred(HeadVar::in, Bool::out) is det :-
|
|
( if bag.contains(InArgs, HeadVar) then
|
|
Bool = yes
|
|
else
|
|
Bool = no
|
|
)
|
|
),
|
|
list.map(MapIsInput, HeadVars, BoolList),
|
|
map.det_insert(PPId, BoolList, RecSupplierMap0, 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(module_info::in,
|
|
list(pred_proc_id)::in, pass_info::in, bool::out) is det.
|
|
|
|
prove_termination_in_scc_single_arg(ModuleInfo, SCC, PassInfo, Terminates) :-
|
|
(
|
|
SCC = [FirstPPId | LaterPPIds],
|
|
FirstArity = lookup_proc_arity(ModuleInfo, FirstPPId),
|
|
find_min_arity_proc(ModuleInfo, LaterPPIds, FirstPPId, FirstArity,
|
|
TrialPPId, RestSCC),
|
|
prove_termination_in_scc_single_arg_2(ModuleInfo, PassInfo,
|
|
TrialPPId, RestSCC, 1, Terminates)
|
|
;
|
|
SCC = [],
|
|
unexpected($pred, "empty SCC")
|
|
).
|
|
|
|
% Find a procedure of minimum arity among the given list and the tentative
|
|
% guess.
|
|
%
|
|
:- pred find_min_arity_proc(module_info::in, list(pred_proc_id)::in,
|
|
pred_proc_id::in, arity::in, pred_proc_id::out,
|
|
list(pred_proc_id)::out) is det.
|
|
|
|
find_min_arity_proc(_, [], BestSofarPPId, _, BestSofarPPId, []).
|
|
find_min_arity_proc(ModuleInfo, [PPId | PPIds], BestSofarPPId, BestSofarArity,
|
|
BestPPId, RestSCC) :-
|
|
Arity = lookup_proc_arity(ModuleInfo, PPId),
|
|
( if Arity < BestSofarArity then
|
|
find_min_arity_proc(ModuleInfo, PPIds, PPId, Arity, BestPPId,
|
|
RestSCC0),
|
|
RestSCC = [BestSofarPPId | RestSCC0]
|
|
else
|
|
find_min_arity_proc(ModuleInfo, PPIds, BestSofarPPId, BestSofarArity,
|
|
BestPPId, RestSCC0),
|
|
RestSCC = [PPId | RestSCC0]
|
|
).
|
|
|
|
% Perform single arg analysis on the SCC.
|
|
%
|
|
:- pred prove_termination_in_scc_single_arg_2(module_info::in, pass_info::in,
|
|
pred_proc_id::in, list(pred_proc_id)::in, int::in, bool::out) is det.
|
|
|
|
prove_termination_in_scc_single_arg_2(ModuleInfo, PassInfo,
|
|
TrialPPId, RestSCC, ArgNum0, Terminates) :-
|
|
( if
|
|
init_rec_input_suppliers_single_arg(ModuleInfo, TrialPPId, RestSCC,
|
|
ArgNum0, InitRecSuppliers)
|
|
then
|
|
prove_termination_in_scc_trial(ModuleInfo, PassInfo, up,
|
|
[TrialPPId | RestSCC], InitRecSuppliers, Termination),
|
|
(
|
|
Termination = cannot_loop(unit),
|
|
Terminates = yes
|
|
;
|
|
Termination = can_loop(_),
|
|
prove_termination_in_scc_single_arg_2(ModuleInfo, PassInfo,
|
|
TrialPPId, RestSCC, ArgNum0 + 1, Terminates)
|
|
)
|
|
else
|
|
Terminates = no
|
|
).
|
|
|
|
:- pred init_rec_input_suppliers_single_arg(module_info::in, pred_proc_id::in,
|
|
list(pred_proc_id)::in, int::in, used_args::out) is semidet.
|
|
|
|
init_rec_input_suppliers_single_arg(ModuleInfo, TrialPPId, RestSCC, ArgNum,
|
|
RecSupplierMap) :-
|
|
module_info_pred_proc_info(ModuleInfo, TrialPPId, _, ProcInfo),
|
|
proc_info_get_argmodes(ProcInfo, ArgModes),
|
|
init_rec_input_suppliers_add_single_arg(ModuleInfo, ArgModes, ArgNum,
|
|
TrialPPIdRecSuppliers),
|
|
RecSupplierMap0 = map.singleton(TrialPPId, TrialPPIdRecSuppliers),
|
|
init_rec_input_suppliers_single_arg_others(ModuleInfo, RestSCC,
|
|
RecSupplierMap0, RecSupplierMap).
|
|
|
|
:- pred init_rec_input_suppliers_add_single_arg(module_info::in,
|
|
list(mer_mode)::in, int::in, list(bool)::out) is semidet.
|
|
|
|
init_rec_input_suppliers_add_single_arg(ModuleInfo, [Mode | Modes], ArgNum,
|
|
BoolList) :-
|
|
( if
|
|
mode_is_input(ModuleInfo, Mode),
|
|
ArgNum = 1
|
|
then
|
|
list.map(map_to_no, Modes, BoolListTail),
|
|
BoolList = [yes | BoolListTail]
|
|
else if
|
|
( if
|
|
mode_is_output(ModuleInfo, Mode)
|
|
then
|
|
NextArgNum = ArgNum
|
|
else if
|
|
mode_is_input(ModuleInfo, Mode),
|
|
ArgNum > 1
|
|
then
|
|
NextArgNum = ArgNum - 1
|
|
else
|
|
fail
|
|
)
|
|
then
|
|
init_rec_input_suppliers_add_single_arg(ModuleInfo, Modes, NextArgNum,
|
|
BoolListTail),
|
|
BoolList = [no | BoolListTail]
|
|
else
|
|
fail
|
|
).
|
|
|
|
:- pred init_rec_input_suppliers_single_arg_others(module_info::in,
|
|
list(pred_proc_id)::in, used_args::in, used_args::out) is det.
|
|
|
|
init_rec_input_suppliers_single_arg_others(_, [], !RecSupplierMap).
|
|
init_rec_input_suppliers_single_arg_others(ModuleInfo, [PPId | PPIds],
|
|
!RecSupplierMap) :-
|
|
module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
|
|
proc_info_get_headvars(ProcInfo, HeadVars),
|
|
list.map(map_to_no, HeadVars, BoolList),
|
|
map.det_insert(PPId, BoolList, !RecSupplierMap),
|
|
init_rec_input_suppliers_single_arg_others(ModuleInfo, PPIds,
|
|
!RecSupplierMap).
|
|
|
|
:- func lookup_proc_arity(module_info, pred_proc_id) = arity.
|
|
|
|
lookup_proc_arity(ModuleInfo, PPId) = Arity :-
|
|
module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
|
|
proc_info_get_headvars(ProcInfo, HeadVars),
|
|
list.length(HeadVars, Arity).
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
:- type fixpoint_dir
|
|
---> up
|
|
; down.
|
|
|
|
:- pred prove_termination_in_scc_trial(module_info::in, pass_info::in,
|
|
fixpoint_dir::in, list(pred_proc_id)::in, used_args::in,
|
|
termination_info::out) is det.
|
|
|
|
prove_termination_in_scc_trial(ModuleInfo, PassInfo, FixDir,
|
|
SCC, InitRecSuppliers, Termination) :-
|
|
prove_termination_in_scc_fixpoint(ModuleInfo, PassInfo, FixDir,
|
|
SCC, InitRecSuppliers, Result),
|
|
(
|
|
Result = term_pass2_ok(CallInfo, _),
|
|
CallInfo = call_weight_info(InfCalls, CallWeights),
|
|
(
|
|
InfCalls = [_ | _],
|
|
PassInfo = pass_info(_, MaxErrors, _),
|
|
list.take_upto(MaxErrors, InfCalls, ReportedInfCalls),
|
|
Termination = can_loop(ReportedInfCalls)
|
|
;
|
|
InfCalls = [],
|
|
zero_or_positive_weight_cycles(ModuleInfo, CallWeights, Cycles),
|
|
(
|
|
Cycles = [],
|
|
Termination = cannot_loop(unit)
|
|
;
|
|
Cycles = [_ | _],
|
|
PassInfo = pass_info(_, MaxErrors, _),
|
|
list.take_upto(MaxErrors, Cycles, ReportedCycles),
|
|
Termination = can_loop(ReportedCycles)
|
|
)
|
|
)
|
|
;
|
|
Result = term_pass2_error(Errors),
|
|
Termination = can_loop(Errors)
|
|
).
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
:- pred prove_termination_in_scc_fixpoint(module_info::in,
|
|
pass_info::in, fixpoint_dir::in, list(pred_proc_id)::in, used_args::in,
|
|
term_pass2_result::out) is det.
|
|
|
|
prove_termination_in_scc_fixpoint(ModuleInfo, PassInfo, FixDir,
|
|
SCC, RecSupplierMap0, Result) :-
|
|
map.init(NewRecSupplierMap0),
|
|
map.init(CallWeightGraph0),
|
|
CallInfo0 = call_weight_info([], CallWeightGraph0),
|
|
prove_termination_in_scc_pass(ModuleInfo, PassInfo, FixDir,
|
|
SCC, RecSupplierMap0, NewRecSupplierMap0, CallInfo0, Result1),
|
|
(
|
|
Result1 = term_pass2_ok(_, RecSupplierMap1),
|
|
( if RecSupplierMap1 = RecSupplierMap0 then
|
|
% We are at a fixed point, so further analysis
|
|
% will not get any better results.
|
|
Result = Result1
|
|
else
|
|
prove_termination_in_scc_fixpoint(ModuleInfo, PassInfo, FixDir,
|
|
SCC, RecSupplierMap1, Result)
|
|
)
|
|
;
|
|
Result1 = term_pass2_error(_),
|
|
Result = Result1
|
|
).
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
% Process a whole SCC, to determine the termination property of each
|
|
% procedure in that SCC.
|
|
%
|
|
:- pred prove_termination_in_scc_pass(module_info::in, pass_info::in,
|
|
fixpoint_dir::in, list(pred_proc_id)::in, used_args::in, used_args::in,
|
|
call_weight_info::in, term_pass2_result::out) is det.
|
|
|
|
prove_termination_in_scc_pass(_, _, _, [], _, NewRecSupplierMap, CallInfo,
|
|
term_pass2_ok(CallInfo, NewRecSupplierMap)).
|
|
prove_termination_in_scc_pass(ModuleInfo, PassInfo, FixDir, [PPId | PPIds],
|
|
RecSupplierMap, NewRecSupplierMap0, CallInfo0, Result) :-
|
|
module_info_pred_proc_info(ModuleInfo, PPId, PredInfo, ProcInfo),
|
|
pred_info_get_context(PredInfo, Context),
|
|
proc_info_get_goal(ProcInfo, Goal0),
|
|
% The pretest code we add for compiler-generated unification and comparison
|
|
% predicates uses type casts. It uses them in a way that is guaranteed
|
|
% to terminate, but our analysis is not (yet) able to find this out for
|
|
% itself. We therefore analyse only the non-pretest parts of such goals.
|
|
Goal = maybe_strip_equality_pretest(Goal0),
|
|
proc_info_get_var_table(ProcInfo, VarTable),
|
|
map.init(EmptyMap),
|
|
PassInfo = pass_info(FunctorInfo, MaxErrors, MaxPaths),
|
|
init_term_traversal_params(FunctorInfo, PPId, Context, VarTable,
|
|
EmptyMap, RecSupplierMap, MaxErrors, MaxPaths, Params),
|
|
set.init(PathSet0),
|
|
Info0 = term_traversal_ok(PathSet0, []),
|
|
term_traverse_goal(ModuleInfo, Params, Goal, Info0, Info),
|
|
(
|
|
Info = term_traversal_ok(Paths, CanLoop),
|
|
expect(unify(CanLoop, []), $pred,
|
|
"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_get_headvars(ProcInfo, Args),
|
|
bag.init(EmptyBag),
|
|
update_rec_input_suppliers(Args, ActiveVars, FixDir,
|
|
RecSuppliers0, RecSuppliers, EmptyBag, RecSuppliers0Bag),
|
|
map.det_insert(PPId, RecSuppliers,
|
|
NewRecSupplierMap0, NewRecSupplierMap1),
|
|
add_call_arcs(PathList, RecSuppliers0Bag, CallInfo0, CallInfo1),
|
|
prove_termination_in_scc_pass(ModuleInfo, PassInfo, FixDir,
|
|
PPIds, RecSupplierMap, NewRecSupplierMap1, CallInfo1, Result)
|
|
;
|
|
Info = term_traversal_error(Errors, CanLoop),
|
|
expect(unify(CanLoop, []), $pred,
|
|
"can_loop detected in pass2 but not pass1"),
|
|
Result = term_pass2_error(Errors)
|
|
).
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
:- pred update_rec_input_suppliers(list(prog_var)::in, bag(prog_var)::in,
|
|
fixpoint_dir::in, list(bool)::in, list(bool)::out,
|
|
bag(prog_var)::in, bag(prog_var)::out) is det.
|
|
|
|
update_rec_input_suppliers([], _, _, [], [], !RecBag).
|
|
update_rec_input_suppliers([_ | _], _, _, [], [], _, _) :-
|
|
unexpected($pred, "unmatched variables").
|
|
update_rec_input_suppliers([], _, _, [_ | _], [], _, _) :-
|
|
unexpected($pred, "unmatched variables").
|
|
update_rec_input_suppliers([Arg | Args], ActiveVars, FixDir,
|
|
[RecInputSupplier0 | RecInputSuppliers0],
|
|
[RecInputSupplier | RecInputSuppliers], !RecBag) :-
|
|
(
|
|
RecInputSupplier0 = yes,
|
|
bag.insert(Arg, !RecBag)
|
|
;
|
|
RecInputSupplier0 = no
|
|
),
|
|
(
|
|
FixDir = down,
|
|
% This guarantees that the set of rec input suppliers
|
|
% can only decrease.
|
|
( if bag.contains(ActiveVars, Arg) then
|
|
RecInputSupplier = RecInputSupplier0
|
|
else
|
|
RecInputSupplier = no
|
|
)
|
|
;
|
|
FixDir = up,
|
|
% This guarantees that the set of rec input suppliers
|
|
% can only increase.
|
|
( if bag.contains(ActiveVars, Arg) then
|
|
RecInputSupplier = yes
|
|
else
|
|
RecInputSupplier = RecInputSupplier0
|
|
)
|
|
),
|
|
update_rec_input_suppliers(Args, ActiveVars, FixDir,
|
|
RecInputSuppliers0, RecInputSuppliers, !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(term_path_info)::in, bag(prog_var)::in,
|
|
call_weight_info::in, call_weight_info::out) is det.
|
|
|
|
add_call_arcs([], _RecInputSuppliers, !CallInfo).
|
|
add_call_arcs([Path | Paths], RecInputSuppliers, !CallInfo) :-
|
|
Path = term_path_info(PPId, CallSite, GammaConst, GammaVars, ActiveVars),
|
|
(
|
|
CallSite = yes(CallPPIdPrime - ContextPrime),
|
|
CallPPId = CallPPIdPrime,
|
|
Context = ContextPrime
|
|
;
|
|
CallSite = no,
|
|
unexpected($pred, "no call site in path in stage 2")
|
|
),
|
|
(
|
|
GammaVars = []
|
|
;
|
|
GammaVars = [_ | _],
|
|
unexpected($pred, "gamma variables in path in stage 2")
|
|
),
|
|
!.CallInfo = call_weight_info(InfCalls0, CallWeights0),
|
|
( if bag.is_subbag(ActiveVars, RecInputSuppliers) then
|
|
( if map.search(CallWeights0, PPId, NeighbourMap0) then
|
|
( if map.search(NeighbourMap0, CallPPId, OldEdgeInfo) then
|
|
OldEdgeInfo = call_weight_edge(OldWeight, _OldContext),
|
|
( if OldWeight >= GammaConst then
|
|
EdgeInfo = OldEdgeInfo
|
|
else
|
|
EdgeInfo = call_weight_edge(GammaConst, Context)
|
|
),
|
|
map.det_update(CallPPId, EdgeInfo, NeighbourMap0, NeighbourMap)
|
|
else
|
|
EdgeInfo = call_weight_edge(GammaConst, Context),
|
|
map.det_insert(CallPPId, EdgeInfo, NeighbourMap0, NeighbourMap)
|
|
),
|
|
map.det_update(PPId, NeighbourMap, CallWeights0, CallWeights1)
|
|
else
|
|
EdgeInfo = call_weight_edge(GammaConst, Context),
|
|
NeighbourMap = map.singleton(CallPPId, EdgeInfo),
|
|
map.det_insert(PPId, NeighbourMap, CallWeights0, CallWeights1)
|
|
),
|
|
!:CallInfo = call_weight_info(InfCalls0, CallWeights1)
|
|
else
|
|
InfCall = term_error(Context, inf_call(PPId, CallPPId)),
|
|
InfCalls1 = [InfCall | InfCalls0],
|
|
!:CallInfo = call_weight_info(InfCalls1, CallWeights0)
|
|
),
|
|
add_call_arcs(Paths, RecInputSuppliers, !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 nevertheless 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(module_info::in, call_weight_graph::in,
|
|
list(term_error)::out) is det.
|
|
|
|
zero_or_positive_weight_cycles(ModuleInfo, CallWeights, Cycles) :-
|
|
map.to_assoc_list(CallWeights, PPIdsNeighboursMaps),
|
|
zero_or_positive_weight_cycles_from_ppids(ModuleInfo, CallWeights,
|
|
PPIdsNeighboursMaps, Cycles).
|
|
|
|
:- pred zero_or_positive_weight_cycles_from_ppids(module_info::in,
|
|
call_weight_graph::in, assoc_list(pred_proc_id, call_weight_dst_map)::in,
|
|
list(term_error)::out) is det.
|
|
|
|
zero_or_positive_weight_cycles_from_ppids(_, _, [], []).
|
|
zero_or_positive_weight_cycles_from_ppids(ModuleInfo, CallWeights,
|
|
[PPIdNeighboursMap | PPIdsNeighboursMaps], Cycles) :-
|
|
zero_or_positive_weight_cycles_from_ppid(ModuleInfo, CallWeights,
|
|
PPIdNeighboursMap, CyclesHead),
|
|
zero_or_positive_weight_cycles_from_ppids(ModuleInfo, CallWeights,
|
|
PPIdsNeighboursMaps, CyclesTail),
|
|
Cycles = CyclesHead ++ CyclesTail.
|
|
|
|
:- pred zero_or_positive_weight_cycles_from_ppid(module_info::in,
|
|
call_weight_graph::in, pair(pred_proc_id, call_weight_dst_map)::in,
|
|
list(term_error)::out) is det.
|
|
|
|
zero_or_positive_weight_cycles_from_ppid(ModuleInfo, CallWeights,
|
|
PPId - NeighboursMap, Cycles) :-
|
|
map.to_assoc_list(NeighboursMap, NeighboursList),
|
|
PPId = proc(PredId, _ProcId),
|
|
module_info_pred_info(ModuleInfo, PredId, PredInfo),
|
|
pred_info_get_context(PredInfo, Context),
|
|
zero_or_positive_weight_cycles_from_neighbours(CallWeights, PPId,
|
|
Context, 0, NeighboursList, [], Cycles).
|
|
|
|
:- pred zero_or_positive_weight_cycles_from_neighbours(call_weight_graph::in,
|
|
pred_proc_id::in, prog_context::in, int::in,
|
|
assoc_list(pred_proc_id, call_weight_edge)::in,
|
|
assoc_list(pred_proc_id, prog_context)::in, list(term_error)::out) is det.
|
|
|
|
zero_or_positive_weight_cycles_from_neighbours(_, _, _, _, [], _, []).
|
|
zero_or_positive_weight_cycles_from_neighbours(CallWeights,
|
|
LookforPPId, Context, WeightSoFar,
|
|
[Neighbour | Neighbours], RevVisitedCalls, Cycles) :-
|
|
zero_or_positive_weight_cycles_from_neighbour(CallWeights, LookforPPId,
|
|
Context, WeightSoFar, Neighbour, RevVisitedCalls, CyclesHead),
|
|
zero_or_positive_weight_cycles_from_neighbours(CallWeights, LookforPPId,
|
|
Context, WeightSoFar, Neighbours, RevVisitedCalls, CyclesTail),
|
|
Cycles = CyclesHead ++ CyclesTail.
|
|
|
|
:- pred zero_or_positive_weight_cycles_from_neighbour(call_weight_graph::in,
|
|
pred_proc_id::in, prog_context::in, int::in,
|
|
pair(pred_proc_id, call_weight_edge)::in,
|
|
assoc_list(pred_proc_id, prog_context)::in, list(term_error)::out) is det.
|
|
|
|
zero_or_positive_weight_cycles_from_neighbour(CallWeights,
|
|
LookforPPId, ProcContext, WeightSoFar0,
|
|
CurPPId - call_weight_edge(EdgeWeight, Context),
|
|
RevVisitedCalls0, Cycles) :-
|
|
WeightSoFar1 = WeightSoFar0 + EdgeWeight,
|
|
( if CurPPId = LookforPPId then
|
|
% We have a cycle on the looked for ppid.
|
|
( if WeightSoFar1 >= 0 then
|
|
RevVisitedCalls = [CurPPId - Context | RevVisitedCalls0],
|
|
list.reverse(RevVisitedCalls, VisitedCalls),
|
|
CycleError = cycle(LookforPPId, VisitedCalls),
|
|
CycleErrorContext = term_error(ProcContext, CycleError),
|
|
Cycles = [CycleErrorContext]
|
|
else
|
|
Cycles = []
|
|
)
|
|
else if assoc_list.search(RevVisitedCalls0, CurPPId, _) then
|
|
% We have a cycle, but not on the looked-for pred_proc_id. We ignore
|
|
% it here; it will be picked up when we process that pred_proc_id.
|
|
Cycles = []
|
|
else
|
|
% No cycle; try all possible edges from this node.
|
|
RevVisitedCalls1 = [CurPPId - Context | RevVisitedCalls0],
|
|
( if map.search(CallWeights, CurPPId, NeighboursMap) then
|
|
map.to_assoc_list(NeighboursMap, NeighboursList),
|
|
zero_or_positive_weight_cycles_from_neighbours(CallWeights,
|
|
LookforPPId, ProcContext, WeightSoFar1,
|
|
NeighboursList, RevVisitedCalls1, Cycles)
|
|
else
|
|
% In some cases, it is possible for a pred_proc_id to have no
|
|
% entry in CallWeights. This happens e.g. in pretty_printer.m.
|
|
% The array_to_doc_loop function is in an SCC together with
|
|
% the function created from the lambda expression in the
|
|
% argument of format_susp. The lambda function calls
|
|
% array_to_doc_loop, but, while array_to_doc_loop *refers*
|
|
% to the lambda function (which is why they are in the same SCC),
|
|
% it does not *call* the lambda function. And since it cannot call
|
|
% any other procedure in the SCC (there being no others),
|
|
% it will not have an entry in CallWeights.
|
|
Cycles = []
|
|
)
|
|
).
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
:- pred map_to_no(T::in, bool::out) is det.
|
|
|
|
map_to_no(_, no).
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
:- end_module transform_hlds.term_pass2.
|
|
%-----------------------------------------------------------------------------%
|