[m-rev.] diff: use intermodule analysis for termination analysis (stage 1)
Julien Fischer
juliensf at cs.mu.OZ.AU
Wed Feb 1 15:16:39 AEDT 2006
Estimated hours taken: 4
Branches: main
Preliminary working on converting the termination analyser to use the
intermodule analysis framework. This mainly involves threading the
module_info and io.state through more of the code and changing some code that
was semidet to det returning a boolean (because it now takes the
io.state). I've put placeholders , XXX intermod, in the spots that need to be
further modified.
compiler/term_errors.m:
compiler/term_pass1.m:
compiler/term_pass2.m:
compiler/term_util.m:
compiler/term_traversal.m:
compiler/termination.m:
Prepare to convert termination analysis to use the intermodule
analysis framework.
Fix some layout problems.
Julien.
Index: compiler/term_errors.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_errors.m,v
retrieving revision 1.34
diff -u -r1.34 term_errors.m
--- compiler/term_errors.m 28 Nov 2005 04:11:56 -0000 1.34
+++ compiler/term_errors.m 31 Jan 2006 06:27:05 -0000
@@ -142,6 +142,7 @@
% make calls back to Mercury. By default such
% code is assumed to be non-terminating.
+:- type termination_error_contexts == list(termination_error_context).
:- type termination_error_context == pair(prog_context, termination_error).
:- pred report_term_errors(list(pred_proc_id)::in,
Index: compiler/term_pass1.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_pass1.m,v
retrieving revision 1.25
diff -u -r1.25 term_pass1.m
--- compiler/term_pass1.m 28 Nov 2005 04:11:56 -0000 1.25
+++ compiler/term_pass1.m 1 Feb 2006 03:12:39 -0000
@@ -36,20 +36,19 @@
:- 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(termination_error_context)
- ).
+ 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(termination_error_context)
+ ).
-:- pred find_arg_sizes_in_scc(list(pred_proc_id)::in, module_info::in,
+:- pred find_arg_sizes_in_scc(list(pred_proc_id)::in,
pass_info::in, arg_size_result::out, list(termination_error_context)::out,
- io::di, io::uo) is det.
+ module_info::in, module_info::out, io::di, io::uo) is det.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
@@ -97,10 +96,10 @@
list(termination_error_context)
).
-find_arg_sizes_in_scc(SCC, ModuleInfo, PassInfo, ArgSize, TermErrors, !IO) :-
- init_output_suppliers(SCC, ModuleInfo, InitOutputSupplierMap),
- find_arg_sizes_in_scc_fixpoint(SCC, ModuleInfo, PassInfo,
- InitOutputSupplierMap, Result, TermErrors),
+find_arg_sizes_in_scc(SCC, PassInfo, ArgSize, TermErrors, !ModuleInfo, !IO) :-
+ init_output_suppliers(SCC, !.ModuleInfo, InitOutputSupplierMap),
+ find_arg_sizes_in_scc_fixpoint(SCC, PassInfo,
+ InitOutputSupplierMap, Result, TermErrors, !ModuleInfo, !IO),
(
Result = ok(Paths, OutputSupplierMap, SubsetErrors),
(
@@ -110,7 +109,7 @@
SubsetErrors = [],
(
Paths = [],
- get_context_from_scc(SCC, ModuleInfo, Context),
+ get_context_from_scc(SCC, !.ModuleInfo, Context),
ArgSize = error([Context - no_eqns])
;
Paths = [_|_],
@@ -120,7 +119,7 @@
ArgSize = ok(Solution, OutputSupplierMap)
;
MaybeSolution = no,
- get_context_from_scc(SCC, ModuleInfo, Context),
+ get_context_from_scc(SCC, !.ModuleInfo, Context),
ArgSize = error([Context - solver_failed])
)
)
@@ -152,74 +151,77 @@
%-----------------------------------------------------------------------------%
:- 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(termination_error_context)::out) is det.
+ pass_info::in, used_args::in, pass1_result::out,
+ list(termination_error_context)::out, module_info::in, module_info::out,
+ io::di, io::uo) is det.
-find_arg_sizes_in_scc_fixpoint(SCC, ModuleInfo, PassInfo, OutputSupplierMap0,
- Result, TermErrors) :-
- find_arg_sizes_in_scc_pass(SCC, ModuleInfo, PassInfo,
- OutputSupplierMap0, [], [], Result1, [], TermErrors1),
+find_arg_sizes_in_scc_fixpoint(SCC, PassInfo, OutputSupplierMap0,
+ Result, TermErrors, !ModuleInfo, !IO) :-
+ find_arg_sizes_in_scc_pass(SCC, PassInfo, OutputSupplierMap0, [], [],
+ Result0, [], TermErrors0, !ModuleInfo, !IO),
(
- Result1 = error(_),
- Result = Result1,
- TermErrors = TermErrors1
+ Result0 = error(_),
+ Result = Result0,
+ TermErrors = TermErrors0
;
- Result1 = ok(_, OutputSupplierMap1, _),
+ Result0 = ok(_, OutputSupplierMap1, _),
( OutputSupplierMap1 = OutputSupplierMap0 ->
- Result = Result1,
- TermErrors = TermErrors1
+ Result = Result0,
+ TermErrors = TermErrors0
;
- find_arg_sizes_in_scc_fixpoint(SCC, ModuleInfo, PassInfo,
- OutputSupplierMap1, Result, TermErrors)
+ find_arg_sizes_in_scc_fixpoint(SCC, PassInfo,
+ OutputSupplierMap1, Result, TermErrors, !ModuleInfo, !IO)
)
).
:- 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(termination_error_context)::in, pass1_result::out,
- list(termination_error_context)::in,
- list(termination_error_context)::out) is det.
+ pass_info::in, used_args::in, list(path_info)::in,
+ termination_error_contexts::in, pass1_result::out,
+ termination_error_contexts::in, termination_error_contexts::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
-find_arg_sizes_in_scc_pass([], _, _, OutputSupplierMap, Paths, SubsetErrors,
- Result, !TermErrors) :-
+find_arg_sizes_in_scc_pass([], _, OutputSupplierMap, Paths, SubsetErrors,
+ Result, !TermErrors, !ModuleInfo, !IO) :-
Result = ok(Paths, OutputSupplierMap, SubsetErrors).
-find_arg_sizes_in_scc_pass([PPId | PPIds], ModuleInfo, PassInfo,
+find_arg_sizes_in_scc_pass([PPId | PPIds], PassInfo,
OutputSupplierMap0, Paths0, SubsetErrors0, Result,
- !TermErrors) :-
- find_arg_sizes_pred(PPId, ModuleInfo, PassInfo, OutputSupplierMap0,
- Result1, ProcTermErrors),
+ !TermErrors, !ModuleInfo, !IO) :-
+ find_arg_sizes_pred(PPId, PassInfo, OutputSupplierMap0,
+ Result1, ProcTermErrors, !ModuleInfo, !IO),
!:TermErrors = !.TermErrors ++ ProcTermErrors,
PassInfo = pass_info(_, MaxErrors, _),
list.take_upto(MaxErrors, !TermErrors),
(
Result1 = error(_),
Result = Result1,
+ %
% The error does not necessarily mean that this SCC is nonterminating.
% We need to check that the remainder of this SCC does not make any
% nonterminating calls otherwise we might get a software error during
% pass 2.
% (See below for details).
- list.foldl(check_proc_non_term_calls(ModuleInfo), PPIds, [],
- OtherTermErrors),
+ %
+ list.foldl3(check_proc_non_term_calls, PPIds, [],
+ OtherTermErrors, !ModuleInfo, !IO),
list.append(OtherTermErrors, !TermErrors)
;
Result1 = ok(Paths1, OutputSupplierMap1, SubsetErrors1),
Paths = Paths0 ++ Paths1,
SubsetErrors = SubsetErrors0 ++ SubsetErrors1,
- find_arg_sizes_in_scc_pass(PPIds, ModuleInfo, PassInfo,
+ find_arg_sizes_in_scc_pass(PPIds, PassInfo,
OutputSupplierMap1, Paths, SubsetErrors, Result,
- !TermErrors)
+ !TermErrors, !ModuleInfo, !IO)
).
%-----------------------------------------------------------------------------%
-:- pred find_arg_sizes_pred(pred_proc_id::in, module_info::in,
- pass_info::in, used_args::in, pass1_result::out,
- list(termination_error_context)::out) is det.
-
-find_arg_sizes_pred(PPId, ModuleInfo, PassInfo, OutputSupplierMap0, Result,
- TermErrors) :-
- module_info_pred_proc_info(ModuleInfo, PPId, PredInfo, ProcInfo),
+:- pred find_arg_sizes_pred(pred_proc_id::in, pass_info::in, used_args::in,
+ pass1_result::out, termination_error_contexts::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
+
+find_arg_sizes_pred(PPId, PassInfo, OutputSupplierMap0, Result,
+ TermErrors, !ModuleInfo, !IO) :-
+ module_info_pred_proc_info(!.ModuleInfo, PPId, PredInfo, ProcInfo),
pred_info_context(PredInfo, Context),
proc_info_headvars(ProcInfo, Args),
proc_info_argmodes(ProcInfo, ArgModes),
@@ -227,14 +229,14 @@
proc_info_goal(ProcInfo, Goal),
map.init(EmptyMap),
PassInfo = pass_info(FunctorInfo, MaxErrors, MaxPaths),
- init_traversal_params(ModuleInfo, FunctorInfo, PPId, Context, VarTypes,
+ init_traversal_params(FunctorInfo, PPId, Context, VarTypes,
OutputSupplierMap0, EmptyMap, MaxErrors, MaxPaths, Params),
- partition_call_args(ModuleInfo, ArgModes, Args, InVars, OutVars),
+ partition_call_args(!.ModuleInfo, 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),
+ traverse_goal(Goal, Params, Info0, Info, !ModuleInfo, !IO),
(
Info = ok(Paths, TermErrors),
@@ -249,8 +251,7 @@
( bag.is_subbag(AllActiveVars, InVars) ->
SubsetErrors = []
;
- SubsetErrors = [Context -
- not_subset(PPId, AllActiveVars, InVars)]
+ SubsetErrors = [Context - not_subset(PPId, AllActiveVars, InVars)]
),
Result = ok(PathList, OutputSupplierMap, SubsetErrors)
;
@@ -293,46 +294,45 @@
% run pass 2 if the procedure contains any calls to nonterminating procedures
% lower down the call-graph (see term_pass2.m for details).
-:- pred check_proc_non_term_calls(module_info::in, pred_proc_id::in,
- list(termination_error_context)::in,
- list(termination_error_context)::out) is det.
+:- pred check_proc_non_term_calls(pred_proc_id::in,
+ termination_error_contexts::in, termination_error_contexts::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
-check_proc_non_term_calls(ModuleInfo, PPId, !Errors) :-
- module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
+check_proc_non_term_calls(PPId, !Errors, !ModuleInfo, !IO) :-
+ module_info_pred_proc_info(!.ModuleInfo, PPId, _, ProcInfo),
proc_info_goal(ProcInfo, Goal),
proc_info_vartypes(ProcInfo, VarTypes),
- check_goal_non_term_calls(ModuleInfo, PPId, VarTypes, Goal, !Errors).
+ check_goal_non_term_calls(PPId, VarTypes, Goal, !Errors, !ModuleInfo,
+ !IO).
-:- pred check_goal_non_term_calls(module_info::in, pred_proc_id::in,
- vartypes::in, hlds_goal::in,
- list(termination_error_context)::in, list(termination_error_context)::out)
- is det.
+:- pred check_goal_non_term_calls(
+ pred_proc_id::in, vartypes::in, hlds_goal::in,
+ termination_error_contexts::in, termination_error_contexts::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
-check_goal_non_term_calls(ModuleInfo, PPId, VarTypes, Goal, !Errors) :-
+check_goal_non_term_calls(PPId, VarTypes, Goal, !Errors, !ModuleInfo, !IO) :-
Goal = GoalExpr - GoalInfo,
- check_goal_expr_non_term_calls(ModuleInfo, PPId, VarTypes, GoalExpr, GoalInfo,
- !Errors).
+ check_goal_expr_non_term_calls(PPId, VarTypes, GoalExpr, GoalInfo,
+ !Errors, !ModuleInfo, !IO).
-:- pred check_goal_expr_non_term_calls(module_info::in, pred_proc_id::in,
+:- pred check_goal_expr_non_term_calls(pred_proc_id::in,
vartypes::in, hlds_goal_expr::in, hlds_goal_info::in,
- list(termination_error_context)::in, list(termination_error_context)::out)
- is det.
+ termination_error_contexts::in, termination_error_contexts::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
-check_goal_expr_non_term_calls(ModuleInfo, PPId, VarTypes, Goal, _, !Errors):-
- (
- Goal = conj(Goals)
- ;
- Goal = par_conj(Goals)
- ;
- Goal = disj(Goals)
+check_goal_expr_non_term_calls(PPId, VarTypes, Goal, _, !Errors,
+ !ModuleInfo, !IO):-
+ ( Goal = conj(Goals)
+ ; Goal = par_conj(Goals)
+ ; Goal = disj(Goals)
),
- list.foldl(check_goal_non_term_calls(ModuleInfo, PPId, VarTypes), Goals,
- !Errors).
-check_goal_expr_non_term_calls(ModuleInfo, PPId, VarTypes, Goal, GoalInfo,
- !Errors) :-
+ list.foldl3(check_goal_non_term_calls(PPId, VarTypes), Goals,
+ !Errors, !ModuleInfo, !IO).
+check_goal_expr_non_term_calls(PPId, VarTypes, Goal, GoalInfo,
+ !Errors, !ModuleInfo, !IO) :-
Goal = call(CallPredId, CallProcId, Args, _, _, _),
CallPPId = proc(CallPredId, CallProcId),
- module_info_pred_proc_info(ModuleInfo, CallPPId, _, ProcInfo),
+ module_info_pred_proc_info(!.ModuleInfo, CallPPId, _, ProcInfo),
proc_info_get_maybe_termination_info(ProcInfo, TerminationInfo),
goal_info_get_context(GoalInfo, Context),
(
@@ -351,39 +351,50 @@
;
true
).
-check_goal_expr_non_term_calls(_, _, _, Goal, GoalInfo, !Errors) :-
+check_goal_expr_non_term_calls(_, _, Goal, GoalInfo, !Errors, !ModuleInfo,
+ !IO) :-
+ % XXX Use closure analysis results here.
Goal = generic_call(_, _, _, _),
goal_info_get_context(GoalInfo, Context),
list.cons(Context - horder_call, !Errors).
-check_goal_expr_non_term_calls(ModuleInfo, PPId, VarTypes, Goal, _, !Errors) :-
+check_goal_expr_non_term_calls(PPId, VarTypes, Goal, _, !Errors, !ModuleInfo,
+ !IO) :-
Goal = switch(_, _, Cases),
- list.foldl(check_cases_non_term_calls(ModuleInfo, PPId, VarTypes), Cases,
- !Errors).
-check_goal_expr_non_term_calls(_, _, _, unify(_, _, _, _, _), _, !Errors).
-check_goal_expr_non_term_calls(ModuleInfo, PPId, VarTypes, not(Goal), _,
- !Errors) :-
- check_goal_non_term_calls(ModuleInfo, PPId, VarTypes, Goal, !Errors).
-check_goal_expr_non_term_calls(ModuleInfo, PPId, VarTypes, Goal, _, !Errors) :-
+ list.foldl3(check_cases_non_term_calls(PPId, VarTypes), Cases,
+ !Errors, !ModuleInfo, !IO).
+check_goal_expr_non_term_calls(_, _, unify(_, _, _, _, _), _, !Errors,
+ !ModuleInfo, !IO).
+check_goal_expr_non_term_calls(PPId, VarTypes, not(Goal), _,
+ !Errors, !ModuleInfo, !IO) :-
+ check_goal_non_term_calls(PPId, VarTypes, Goal, !Errors, !ModuleInfo,
+ !IO).
+check_goal_expr_non_term_calls(PPId, VarTypes, Goal, _, !Errors, !ModuleInfo,
+ !IO) :-
Goal = scope(_, ScopeGoal),
- check_goal_non_term_calls(ModuleInfo, PPId, VarTypes, ScopeGoal, !Errors).
-check_goal_expr_non_term_calls(ModuleInfo, PPId, VarTypes, Goal, _, !Errors) :-
+ check_goal_non_term_calls(PPId, VarTypes, ScopeGoal, !Errors, !ModuleInfo,
+ !IO).
+check_goal_expr_non_term_calls(PPId, VarTypes, Goal, _, !Errors, !ModuleInfo,
+ !IO) :-
Goal = if_then_else(_, Cond, Then, Else),
- Goals = [ Cond, Then, Else ],
- list.foldl(check_goal_non_term_calls(ModuleInfo, PPId, VarTypes), Goals,
- !Errors).
-check_goal_expr_non_term_calls(_, _, _, Goal, _, !Errors) :-
- Goal = foreign_proc(_, _, _, _, _, _).
-check_goal_expr_non_term_calls(_, _, _, shorthand(_), _, _, _) :-
+ Goals = [Cond, Then, Else],
+ list.foldl3(check_goal_non_term_calls(PPId, VarTypes), Goals,
+ !Errors, !ModuleInfo, !IO).
+check_goal_expr_non_term_calls(_, _, Goal, _, !Errors, !ModuleInfo, !IO) :-
+ % XXX This looks incomplete - juliensf.
+ Goal = foreign_proc(_, _, _, _, _, _).
+check_goal_expr_non_term_calls(_, _, shorthand(_), _, _, _, _, _, _, _) :-
unexpected(this_file,
"shorthand goal encountered during termination analysis.").
-:- pred check_cases_non_term_calls(module_info::in, pred_proc_id::in,
- vartypes::in, case::in,
- list(termination_error_context)::in,
- list(termination_error_context)::out) is det.
-
-check_cases_non_term_calls(ModuleInfo, PPId, VarTypes, case(_, Goal), !Errors) :-
- check_goal_non_term_calls(ModuleInfo, PPId, VarTypes, Goal, !Errors).
+:- pred check_cases_non_term_calls(
+ pred_proc_id::in, vartypes::in, case::in,
+ termination_error_contexts::in, termination_error_contexts::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
+
+check_cases_non_term_calls(PPId, VarTypes, case(_, Goal), !Errors,
+ !ModuleInfo, !IO) :-
+ check_goal_non_term_calls(PPId, VarTypes, Goal, !Errors,
+ !ModuleInfo, !IO).
%-----------------------------------------------------------------------------%
%
Index: compiler/term_pass2.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_pass2.m,v
retrieving revision 1.23
diff -u -r1.23 term_pass2.m
--- compiler/term_pass2.m 28 Nov 2005 04:11:56 -0000 1.23
+++ compiler/term_pass2.m 1 Feb 2006 03:27:40 -0000
@@ -22,14 +22,18 @@
:- import_module hlds.hlds_pred.
:- import_module transform_hlds.term_util.
+:- import_module io.
:- import_module list.
+%-----------------------------------------------------------------------------%
+
% 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(list(pred_proc_id)::in, module_info::in,
- pass_info::in, int::in, termination_info::out) is det.
+:- pred prove_termination_in_scc(list(pred_proc_id)::in,
+ pass_info::in, int::in, termination_info::out, module_info::in,
+ module_info::out, io::di, io::uo) is det.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
@@ -61,34 +65,32 @@
; down.
:- type call_weight_info
- == pair(list(termination_error_context), call_weight_graph).
+ == pair(termination_error_contexts, 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(prog_context, int))).
- % is at this context and with
- % this weight.
+ % The maximum non-infinite weight from proc to proc and which context
+ % it occurs at.
+ %
+:- type call_weight_graph == map(pred_proc_id, call_weight_dst_map).
+:- type call_weight_dst_map == map(pred_proc_id, pair(prog_context, int)).
:- type pass2_result
- ---> ok(
- call_weight_info,
- used_args
- )
-
- ; error(
- list(termination_error_context)
- ).
+ ---> ok(
+ call_weight_info,
+ used_args
+ )
+ ; error(
+ termination_error_contexts
+ ).
%------------------------------------------------------------------------------%
-prove_termination_in_scc(SCC, ModuleInfo, PassInfo, SingleArgs, Termination) :-
- init_rec_input_suppliers(SCC, ModuleInfo, InitRecSuppliers),
- prove_termination_in_scc_trial(SCC, InitRecSuppliers, down, ModuleInfo,
- PassInfo, Termination1),
+prove_termination_in_scc(SCC, PassInfo, SingleArgs, Termination,
+ !ModuleInfo, !IO) :-
+ init_rec_input_suppliers(SCC, !.ModuleInfo, InitRecSuppliers),
+ prove_termination_in_scc_trial(SCC, InitRecSuppliers, down, PassInfo,
+ Termination0, !ModuleInfo, !IO),
(
- Termination1 = can_loop(Errors),
+ Termination0 = 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
@@ -101,16 +103,23 @@
\+ (
list.member(Error, Errors),
Error = _ - imported_pred
- ),
- prove_termination_in_scc_single_arg(SCC, ModuleInfo, PassInfo)
+ )
->
- Termination = cannot_loop(unit)
+ prove_termination_in_scc_single_arg(SCC, PassInfo,
+ SingleArgTerminates, !ModuleInfo, !IO),
+ (
+ SingleArgTerminates = yes,
+ Termination = cannot_loop(unit)
+ ;
+ SingleArgTerminates = no,
+ Termination = Termination0
+ )
;
- Termination = Termination1
+ Termination = Termination0
)
;
- Termination1 = cannot_loop(unit),
- Termination = Termination1
+ Termination0 = cannot_loop(unit),
+ Termination = Termination0
).
% Initialise the set of recursive input suppliers to be the set of all
@@ -155,16 +164,18 @@
% sets cannot decrease.
%
:- pred prove_termination_in_scc_single_arg(list(pred_proc_id)::in,
- module_info::in, pass_info::in) is semidet.
+ pass_info::in, bool::out, module_info::in, module_info::out,
+ io::di, io::uo) is det.
-prove_termination_in_scc_single_arg(SCC, ModuleInfo, PassInfo) :-
+prove_termination_in_scc_single_arg(SCC, PassInfo, Terminates, !ModuleInfo,
+ !IO) :-
(
SCC = [FirstPPId | LaterPPIds],
- lookup_proc_arity(FirstPPId, ModuleInfo, FirstArity),
- find_min_arity_proc(LaterPPIds, FirstPPId, FirstArity, ModuleInfo,
+ FirstArity = lookup_proc_arity(FirstPPId, !.ModuleInfo),
+ find_min_arity_proc(LaterPPIds, FirstPPId, FirstArity, !.ModuleInfo,
TrialPPId, RestSCC),
prove_termination_in_scc_single_arg_2(TrialPPId, RestSCC, 1,
- ModuleInfo, PassInfo)
+ PassInfo, Terminates, !ModuleInfo, !IO)
;
SCC = [],
unexpected(this_file,
@@ -174,13 +185,14 @@
% 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.
+:- pred find_min_arity_proc(list(pred_proc_id)::in, pred_proc_id::in,
+ arity::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, ModuleInfo,
BestPPId, RestSCC) :-
- lookup_proc_arity(PPId, ModuleInfo, Arity),
+ Arity = lookup_proc_arity(PPId, ModuleInfo),
( Arity < BestSofarArity ->
find_min_arity_proc(PPIds, PPId, Arity, ModuleInfo, BestPPId,
RestSCC0),
@@ -194,22 +206,28 @@
% 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.
+ list(pred_proc_id)::in, int::in, pass_info::in, bool::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
prove_termination_in_scc_single_arg_2(TrialPPId, RestSCC, ArgNum0,
- ModuleInfo, PassInfo) :-
- init_rec_input_suppliers_single_arg(TrialPPId, RestSCC,
- ArgNum0, ModuleInfo, InitRecSuppliers),
- prove_termination_in_scc_trial([TrialPPId | RestSCC], InitRecSuppliers,
- up, ModuleInfo, PassInfo, Termination),
- (
- Termination = cannot_loop(unit)
+ PassInfo, Terminates, !ModuleInfo, !IO) :-
+ (
+ init_rec_input_suppliers_single_arg(TrialPPId, RestSCC,
+ ArgNum0, !.ModuleInfo, InitRecSuppliers)
+ ->
+ prove_termination_in_scc_trial([TrialPPId | RestSCC], InitRecSuppliers,
+ up, PassInfo, Termination, !ModuleInfo, !IO),
+ (
+ Termination = cannot_loop(unit),
+ Terminates = yes
+ ;
+ Termination = can_loop(_),
+ ArgNum1 = ArgNum0 + 1,
+ prove_termination_in_scc_single_arg_2(TrialPPId, RestSCC,
+ ArgNum1, PassInfo, Terminates, !ModuleInfo, !IO)
+ )
;
- Termination = can_loop(_),
- ArgNum1 = ArgNum0 + 1,
- prove_termination_in_scc_single_arg_2(TrialPPId, RestSCC,
- ArgNum1, ModuleInfo, PassInfo)
+ Terminates = no
).
:- pred init_rec_input_suppliers_single_arg(pred_proc_id::in,
@@ -231,21 +249,21 @@
:- pred init_rec_input_suppliers_add_single_arg(list(mer_mode)::in, int::in,
module_info::in, list(bool)::out) is semidet.
-init_rec_input_suppliers_add_single_arg([Mode | Modes], ArgNum, Module,
+init_rec_input_suppliers_add_single_arg([Mode | Modes], ArgNum, ModuleInfo,
BoolList) :-
(
- mode_is_input(Module, Mode),
+ mode_is_input(ModuleInfo, Mode),
ArgNum = 1
->
list.map(map_to_no, Modes, BoolList1),
BoolList = [yes | BoolList1]
;
(
- mode_is_output(Module, Mode)
+ mode_is_output(ModuleInfo, Mode)
->
NextArgNum = ArgNum
;
- mode_is_input(Module, Mode),
+ mode_is_input(ModuleInfo, Mode),
ArgNum > 1
->
NextArgNum = ArgNum - 1
@@ -254,7 +272,7 @@
)
->
init_rec_input_suppliers_add_single_arg(Modes, NextArgNum,
- Module, BoolList1),
+ ModuleInfo, BoolList1),
BoolList = [no | BoolList1]
;
fail
@@ -273,23 +291,23 @@
init_rec_input_suppliers_single_arg_others(PPIds, Module,
!RecSupplierMap).
-:- pred lookup_proc_arity(pred_proc_id::in, module_info::in, int::out) is det.
+:- func lookup_proc_arity(pred_proc_id, module_info) = arity.
-lookup_proc_arity(PPId, Module, Arity) :-
- module_info_pred_proc_info(Module, PPId, _, ProcInfo),
+lookup_proc_arity(PPId, ModuleInfo) = Arity :-
+ module_info_pred_proc_info(ModuleInfo, PPId, _, 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.
+ fixpoint_dir::in, pass_info::in, termination_info::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
-prove_termination_in_scc_trial(SCC, InitRecSuppliers, FixDir, ModuleInfo,
- PassInfo, Termination) :-
- prove_termination_in_scc_fixpoint(SCC, FixDir, ModuleInfo, PassInfo,
- InitRecSuppliers, Result),
+prove_termination_in_scc_trial(SCC, InitRecSuppliers, FixDir,
+ PassInfo, Termination, !ModuleInfo, !IO) :-
+ prove_termination_in_scc_fixpoint(SCC, FixDir, PassInfo,
+ InitRecSuppliers, Result, !ModuleInfo, !IO),
(
Result = ok(CallInfo, _),
CallInfo = InfCalls - CallWeights,
@@ -300,7 +318,7 @@
list.take_upto(MaxErrors, InfCalls, ReportedInfCalls),
Termination = can_loop(ReportedInfCalls)
;
- zero_or_positive_weight_cycles(CallWeights, ModuleInfo, Cycles),
+ zero_or_positive_weight_cycles(CallWeights, !.ModuleInfo, Cycles),
Cycles \= []
->
PassInfo = pass_info(_, MaxErrors, _),
@@ -317,16 +335,17 @@
%-----------------------------------------------------------------------------%
:- 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.
+ fixpoint_dir::in, pass_info::in, used_args::in, pass2_result::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
-prove_termination_in_scc_fixpoint(SCC, FixDir, ModuleInfo, PassInfo,
- RecSupplierMap0, Result) :-
+prove_termination_in_scc_fixpoint(SCC, FixDir, PassInfo,
+ RecSupplierMap0, Result, !ModuleInfo, !IO) :-
map.init(NewRecSupplierMap0),
map.init(CallWeightGraph0),
CallInfo0 = [] - CallWeightGraph0,
- prove_termination_in_scc_pass(SCC, FixDir, ModuleInfo, PassInfo,
- RecSupplierMap0, NewRecSupplierMap0, CallInfo0, Result1),
+ prove_termination_in_scc_pass(SCC, FixDir, PassInfo,
+ RecSupplierMap0, NewRecSupplierMap0, CallInfo0, Result1, !ModuleInfo,
+ !IO),
(
Result1 = ok(_, RecSupplierMap1),
( RecSupplierMap1 = RecSupplierMap0 ->
@@ -335,7 +354,7 @@
Result = Result1
;
prove_termination_in_scc_fixpoint(SCC, FixDir,
- ModuleInfo, PassInfo, RecSupplierMap1, Result)
+ PassInfo, RecSupplierMap1, Result, !ModuleInfo, !IO)
)
;
Result1 = error(_),
@@ -348,24 +367,26 @@
% 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, ModuleInfo, PassInfo,
- RecSupplierMap, NewRecSupplierMap0, CallInfo0, Result) :-
- module_info_pred_proc_info(ModuleInfo, PPId, PredInfo, ProcInfo),
+ pass_info::in, used_args::in, used_args::in,
+ call_weight_info::in, pass2_result::out, module_info::in, module_info::out,
+ io::di, io::uo) is det.
+
+prove_termination_in_scc_pass([], _, _, _, NewRecSupplierMap, CallInfo,
+ ok(CallInfo, NewRecSupplierMap), !ModuleInfo, !IO).
+prove_termination_in_scc_pass([PPId | PPIds], FixDir, PassInfo,
+ RecSupplierMap, NewRecSupplierMap0, CallInfo0, Result,
+ !ModuleInfo, !IO) :-
+ module_info_pred_proc_info(!.ModuleInfo, PPId, 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(ModuleInfo, FunctorInfo, PPId, Context, VarTypes,
+ init_traversal_params(FunctorInfo, PPId, Context, VarTypes,
EmptyMap, RecSupplierMap, MaxErrors, MaxPaths, Params),
set.init(PathSet0),
Info0 = ok(PathSet0, []),
- traverse_goal(Goal, Params, Info0, Info),
+ traverse_goal(Goal, Params, Info0, Info, !ModuleInfo, !IO),
(
Info = ok(Paths, CanLoop),
expect(unify(CanLoop, []), this_file,
@@ -381,8 +402,9 @@
map.det_insert(NewRecSupplierMap0, PPId, RecSuppliers,
NewRecSupplierMap1),
add_call_arcs(PathList, RecSuppliers0Bag, CallInfo0, CallInfo1),
- prove_termination_in_scc_pass(PPIds, FixDir, ModuleInfo,
- PassInfo, RecSupplierMap, NewRecSupplierMap1, CallInfo1, Result)
+ prove_termination_in_scc_pass(PPIds, FixDir,
+ PassInfo, RecSupplierMap, NewRecSupplierMap1, CallInfo1, Result,
+ !ModuleInfo, !IO)
;
Info = error(Errors, CanLoop),
expect(unify(CanLoop, []), this_file,
@@ -458,9 +480,10 @@
unexpected(this_file,
"add_call_arcs/4: no call site in path in stage 2.")
),
- ( GammaVars = [] ->
- true
+ (
+ GammaVars = []
;
+ GammaVars = [_|_],
unexpected(this_file,
"add_call_arc/4: gamma variables in path in stage 2.")
),
@@ -527,13 +550,13 @@
:- pred zero_or_positive_weight_cycles_from(pred_proc_id::in,
call_weight_graph::in, module_info::in,
- list(termination_error_context)::out) is det.
+ termination_error_contexts::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),
+ 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).
Index: compiler/term_traversal.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_traversal.m,v
retrieving revision 1.42
diff -u -r1.42 term_traversal.m
--- compiler/term_traversal.m 28 Nov 2005 04:11:57 -0000 1.42
+++ compiler/term_traversal.m 1 Feb 2006 03:00:58 -0000
@@ -29,6 +29,7 @@
:- import_module transform_hlds.term_util.
:- import_module bag.
+:- import_module io.
:- import_module list.
:- import_module set.
:- import_module std_util.
@@ -93,13 +94,15 @@
:- type traversal_params.
-:- pred init_traversal_params(module_info::in, functor_info::in,
+:- pred init_traversal_params(functor_info::in,
pred_proc_id::in, prog_context::in, vartypes::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 traverse_goal(
+ hlds_goal::in, traversal_params::in,
+ traversal_info::in, traversal_info::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
:- pred upper_bound_active_vars(list(path_info)::in, bag(prog_var)::out) is det.
@@ -122,7 +125,7 @@
%-----------------------------------------------------------------------------%
-traverse_goal(Goal, Params, !Info) :-
+traverse_goal(Goal, Params, !Info, !ModuleInfo, !IO) :-
Goal = GoalExpr - GoalInfo,
(
goal_info_get_determinism(GoalInfo, Detism),
@@ -132,17 +135,18 @@
;
true
),
- traverse_goal_2(GoalExpr, GoalInfo, Params, !Info).
+ traverse_goal_2(GoalExpr, GoalInfo, Params, !Info, !ModuleInfo, !IO).
:- pred traverse_goal_2(hlds_goal_expr::in, hlds_goal_info::in,
- traversal_params::in, traversal_info::in, traversal_info::out) is det.
+ traversal_params::in, traversal_info::in, traversal_info::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
-traverse_goal_2(unify(_Var, _RHS, _UniMode, Unification, _Context),
- _GoalInfo, Params, !Info) :-
+traverse_goal_2(Goal, _GoalInfo, Params, !Info, !ModuleInfo, !IO) :-
+ Goal = unify(_Var, _RHS, _UniMode, Unification, _Context),
(
Unification = construct(OutVar, ConsId, Args, Modes, _, _, _),
(
- unify_change(OutVar, ConsId, Args, Modes, Params,
+ unify_change(!.ModuleInfo, OutVar, ConsId, Args, Modes, Params,
Gamma, InVars, OutVars0)
->
bag.insert(OutVars0, OutVar, OutVars),
@@ -155,7 +159,7 @@
;
Unification = deconstruct(InVar, ConsId, Args, Modes, _, _),
(
- unify_change(InVar, ConsId, Args, Modes, Params,
+ unify_change(!.ModuleInfo, InVar, ConsId, Args, Modes, Params,
Gamma0, InVars0, OutVars)
->
bag.insert(InVars0, InVar, InVars),
@@ -163,7 +167,7 @@
record_change(InVars, OutVars, Gamma, [], !Info)
;
unexpected(this_file,
- "traverse_goal_2/5: higher order deconstruction.")
+ "traverse_goal_2/5: higher order deconstruction.")
)
;
Unification = assign(OutVar, InVar),
@@ -178,47 +182,47 @@
unexpected(this_file, "traverse_goal_2/5: complicated unify.")
).
-traverse_goal_2(conj(Goals), _, Params, !Info) :-
+traverse_goal_2(conj(Goals), _, Params, !Info, !ModuleInfo, !IO) :-
list.reverse(Goals, RevGoals),
- traverse_conj(RevGoals, Params, !Info).
+ traverse_conj(RevGoals, Params, !Info, !ModuleInfo, !IO).
-traverse_goal_2(par_conj(Goals), _, Params, !Info) :-
+traverse_goal_2(par_conj(Goals), _, Params, !Info, !ModuleInfo, !IO) :-
list.reverse(Goals, RevGoals),
- traverse_conj(RevGoals, Params, !Info).
+ traverse_conj(RevGoals, Params, !Info, !ModuleInfo, !IO).
-traverse_goal_2(switch(_, _, Cases), _, Params, !Info) :-
- traverse_switch(Cases, Params, !Info).
+traverse_goal_2(switch(_, _, Cases), _, Params, !Info, !ModuleInfo, !IO) :-
+ traverse_switch(Cases, Params, !Info, !ModuleInfo, !IO).
-traverse_goal_2(disj(Goals), _, Params, !Info) :-
- traverse_disj(Goals, Params, !Info).
+traverse_goal_2(disj(Goals), _, Params, !Info, !ModuleInfo, !IO) :-
+ traverse_disj(Goals, Params, !Info, !ModuleInfo, !IO).
-traverse_goal_2(not(Goal), _, Params, !Info) :-
- % The negated goal will not affect the argument sizes since it
- % cannot bind any active variables. However, we must traverse
- % it anyway during pass 1 to ensure that it does not call any
- % non-terminating procedures. Pass 2 relies on pass 1 having
- % done this.
- traverse_goal(Goal, Params, !Info).
-
-traverse_goal_2(scope(_, Goal), _GoalInfo, Params, !Info) :-
- traverse_goal(Goal, Params, !Info).
-
-traverse_goal_2(if_then_else(_, Cond, Then, Else), _, Params, !Info) :-
- traverse_conj([Then, Cond], Params, !.Info, CondThenInfo),
- traverse_goal(Else, Params, !.Info, ElseInfo),
+traverse_goal_2(not(Goal), _, Params, !Info, !ModuleInfo, !IO) :-
+ % The negated goal will not affect the argument sizes since it cannot bind
+ % any active variables. However, we must traverse it during pass 1 to
+ % ensure that it does not call any non-terminating procedures. Pass 2
+ % relies on pass 1 having done this.
+ traverse_goal(Goal, Params, !Info, !ModuleInfo, !IO).
+
+traverse_goal_2(scope(_, Goal), _GoalInfo, Params, !Info, !ModuleInfo, !IO) :-
+ traverse_goal(Goal, Params, !Info, !ModuleInfo, !IO).
+
+traverse_goal_2(Goal, _, Params, !Info, !ModuleInfo, !IO) :-
+ Goal = if_then_else(_, Cond, Then, Else),
+ traverse_conj([Then, Cond], Params, !.Info, CondThenInfo, !ModuleInfo,
+ !IO),
+ traverse_goal(Else, Params, !.Info, ElseInfo, !ModuleInfo, !IO),
combine_paths(CondThenInfo, ElseInfo, Params, !:Info).
-traverse_goal_2(Goal, GoalInfo, Params, !Info) :-
+traverse_goal_2(Goal, GoalInfo, Params, !Info, !ModuleInfo, !IO) :-
Goal = foreign_proc(Attributes, CallPredId, CallProcId, Args, _, _),
- params_get_module_info(Params, ModuleInfo),
- module_info_pred_proc_info(ModuleInfo, CallPredId, CallProcId, _,
+ module_info_pred_proc_info(!.ModuleInfo, CallPredId, CallProcId, _,
CallProcInfo),
proc_info_argmodes(CallProcInfo, CallArgModes),
ArgVars = list.map(foreign_arg_var, Args),
- partition_call_args(ModuleInfo, CallArgModes, ArgVars, _InVars, OutVars),
+ partition_call_args(!.ModuleInfo, CallArgModes, ArgVars, _InVars, OutVars),
goal_info_get_context(GoalInfo, Context),
- ( is_termination_known(ModuleInfo, proc(CallPredId, CallProcId)) ->
+ ( is_termination_known(!.ModuleInfo, proc(CallPredId, CallProcId)) ->
error_if_intersect(OutVars, Context, pragma_foreign_code, !Info)
;
( attributes_imply_termination(Attributes) ->
@@ -228,7 +232,7 @@
)
).
-traverse_goal_2(Goal, GoalInfo, Params, !Info) :-
+traverse_goal_2(Goal, GoalInfo, Params, !Info, !ModuleInfo, !IO) :-
Goal = generic_call(Details, Args, ArgModes, _),
goal_info_get_context(GoalInfo, Context),
(
@@ -240,14 +244,14 @@
% anything about the size of the arguments of the higher-order call,
% so we assume that they are unbounded.
%
- params_get_module_info(Params, ModuleInfo),
( ClosureValues0 = ClosureValueMap ^ elem(Var) ->
ClosureValues = set.to_sorted_list(ClosureValues0),
- list.filter(terminates(ModuleInfo), ClosureValues,
+ % XXX intermod
+ list.filter(terminates(!.ModuleInfo), ClosureValues,
Terminating, NonTerminating),
(
NonTerminating = [],
- partition_call_args(ModuleInfo, ArgModes, Args,
+ partition_call_args(!.ModuleInfo, ArgModes, Args,
_InVars, OutVars),
params_get_ppid(Params, PPId),
Error = ho_inf_termination_const(PPId, Terminating),
@@ -285,20 +289,20 @@
add_error(Context, aditi_call, Params, !Info)
).
-traverse_goal_2(Goal, GoalInfo, Params, !Info) :-
+traverse_goal_2(Goal, GoalInfo, Params, !Info, !ModuleInfo, !IO) :-
Goal = call(CallPredId, CallProcId, Args, _, _, _),
goal_info_get_context(GoalInfo, Context),
- params_get_module_info(Params, ModuleInfo),
params_get_ppid(Params, PPId),
CallPPId = proc(CallPredId, CallProcId),
- module_info_pred_proc_info(ModuleInfo, CallPredId, CallProcId, _,
+ module_info_pred_proc_info(!.ModuleInfo, CallPredId, CallProcId, _,
CallProcInfo),
proc_info_argmodes(CallProcInfo, CallArgModes),
+ % XXX intermod
proc_info_get_maybe_arg_size_info(CallProcInfo, CallArgSizeInfo),
proc_info_get_maybe_termination_info(CallProcInfo, CallTerminationInfo),
- partition_call_args(ModuleInfo, CallArgModes, Args, InVars, OutVars),
+ partition_call_args(!.ModuleInfo, CallArgModes, Args, InVars, OutVars),
% Handle existing paths
(
@@ -311,9 +315,9 @@
inf_termination_const(PPId, CallPPId), !Info)
;
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.
+ % 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),
@@ -359,7 +363,7 @@
true
).
-traverse_goal_2(shorthand(_), _, _, _, _) :-
+traverse_goal_2(shorthand(_), _, _, _, _, _, _, _, _) :-
% These should have been expanded out by now.
unexpected(this_file, "traverse_goal_2/5: shorthand goal.").
@@ -368,32 +372,35 @@
% 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).
-traverse_conj([Goal | Goals], Params, !Info) :-
- traverse_goal(Goal, Params, !Info),
- traverse_conj(Goals, Params, !Info).
+:- pred traverse_conj(hlds_goals::in, traversal_params::in,
+ traversal_info::in, traversal_info::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
+
+traverse_conj([], _, !Info, !ModuleInfo, !IO).
+traverse_conj([Goal | Goals], Params, !Info, !ModuleInfo, !IO) :-
+ traverse_goal(Goal, Params, !Info, !ModuleInfo, !IO),
+ traverse_conj(Goals, Params, !Info, !ModuleInfo, !IO).
+
+:- pred traverse_disj(hlds_goals::in, traversal_params::in,
+ traversal_info::in, traversal_info::out, module_info::in,
+ module_info::out, io::di, io::uo) is det.
-:- pred traverse_disj(list(hlds_goal)::in, traversal_params::in,
- traversal_info::in, traversal_info::out) is det.
-
-traverse_disj([], _, _, ok(Empty, [])) :-
+traverse_disj([], _, _, ok(Empty, []), !ModuleInfo, !IO) :-
set.init(Empty).
-traverse_disj([Goal | Goals], Params, !Info) :-
- traverse_goal(Goal, Params, !.Info, GoalInfo),
- traverse_disj(Goals, Params, !.Info, GoalsInfo),
+traverse_disj([Goal | Goals], Params, !Info, !ModuleInfo, !IO) :-
+ traverse_goal(Goal, Params, !.Info, GoalInfo, !ModuleInfo, !IO),
+ traverse_disj(Goals, Params, !.Info, GoalsInfo, !ModuleInfo, !IO),
combine_paths(GoalInfo, GoalsInfo, Params, !:Info).
:- pred traverse_switch(list(case)::in, traversal_params::in,
- traversal_info::in, traversal_info::out) is det.
+ traversal_info::in, traversal_info::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
-traverse_switch([], _, _, ok(Empty, [])) :-
+traverse_switch([], _, _, ok(Empty, []), !ModuleInfo, !IO) :-
set.init(Empty).
-traverse_switch([case(_, Goal) | Cases], Params, !Info) :-
- traverse_goal(Goal, Params, !.Info, GoalInfo),
- traverse_switch(Cases, Params, !.Info, CasesInfo),
+traverse_switch([case(_, Goal) | Cases], Params, !Info, !ModuleInfo, !IO) :-
+ traverse_goal(Goal, Params, !.Info, GoalInfo, !ModuleInfo, !IO),
+ traverse_switch(Cases, Params, !.Info, CasesInfo, !ModuleInfo, !IO),
combine_paths(GoalInfo, CasesInfo, Params, !:Info).
%-----------------------------------------------------------------------------%
@@ -507,17 +514,17 @@
% input or output bags. The predicate fails if invoked on a higher
% order unification.
%
-:- pred unify_change(prog_var::in, cons_id::in, list(prog_var)::in,
- list(uni_mode)::in, traversal_params::in, int::out, bag(prog_var)::out,
- bag(prog_var)::out) is semidet.
+:- pred unify_change(module_info::in, prog_var::in, cons_id::in,
+ list(prog_var)::in, list(uni_mode)::in, traversal_params::in, int::out,
+ bag(prog_var)::out, bag(prog_var)::out) is semidet.
-unify_change(OutVar, ConsId, Args0, Modes0, Params, Gamma, InVars, OutVars) :-
+unify_change(ModuleInfo, 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_ctor_and_args(Type, TypeCtor, _) ->
- params_get_module_info(Params, ModuleInfo),
filter_args_and_modes(VarTypes, Args0, Args1, Modes0, Modes1),
functor_norm(FunctorInfo, TypeCtor, ConsId, ModuleInfo,
Gamma, Args1, Args, Modes1, Modes),
@@ -613,42 +620,38 @@
:- type traversal_params
---> traversal_params(
- module_info :: module_info,
-
- functor_info :: functor_info,
+ functor_info :: functor_info,
- ppid :: pred_proc_id,
- % The procedure we are tracing through.
+ ppid :: pred_proc_id,
+ % The procedure we are tracing through.
- context :: prog_context,
- % The context of the procedure.
+ context :: prog_context,
+ % The context of the procedure.
- vartypes :: vartypes,
+ vartypes :: vartypes,
- output_suppliers :: map(pred_proc_id, list(bool)),
- % Output suppliers of each procedure.
- % Empty during pass 2.
+ output_suppliers :: map(pred_proc_id, list(bool)),
+ % Output suppliers of each procedure.
+ % Empty during pass 2.
rec_input_supplier :: map(pred_proc_id, list(bool)),
- % Rec input suppliers of each procedure.
- % Empty during pass 1.
+ % Recursive input suppliers of each procedure.
+ % Empty during pass 1.
- max_errors :: int,
- % Max number of errors to gather.
+ max_errors :: int,
+ % Maximum number of errors to gather.
- max_paths :: int
- % Max number of paths to analyze.
- ).
+ max_paths :: int
+ % Maximum number of paths to analyze.
+ ).
-init_traversal_params(ModuleInfo, FunctorInfo, PredProcId, Context, VarTypes,
+init_traversal_params(FunctorInfo, PredProcId, Context, VarTypes,
OutputSuppliers, RecInputSuppliers, MaxErrors, MaxPaths,
Params) :-
- Params = traversal_params(ModuleInfo, FunctorInfo, PredProcId, Context,
+ Params = traversal_params(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)
@@ -664,7 +667,6 @@
:- 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, Params ^ module_info).
params_get_functor_info(Params, Params ^ functor_info).
params_get_ppid(Params, Params ^ ppid).
params_get_context(Params, Params ^ context).
Index: compiler/term_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_util.m,v
retrieving revision 1.46
diff -u -r1.46 term_util.m
--- compiler/term_util.m 28 Nov 2005 04:11:57 -0000 1.46
+++ compiler/term_util.m 31 Jan 2006 07:18:29 -0000
@@ -54,23 +54,22 @@
%
% where | | represents a semilinear norm.
%
-:- type arg_size_info ==
- generic_arg_size_info(list(termination_error_context)).
+:- type arg_size_info == generic_arg_size_info(termination_error_contexts).
:- type termination_info ==
- generic_termination_info(unit, list(termination_error_context)).
+ generic_termination_info(unit, termination_error_contexts).
% The type `used_args' holds a mapping which specifies for each procedure
% which of its arguments are used.
%
-:- type used_args == map(pred_proc_id, list(bool)).
+:- type used_args == map(pred_proc_id, list(bool)).
:- type pass_info
- ---> pass_info(
- functor_info,
- int, % Max number of errors to gather.
- int % Max number of paths to analyze.
- ).
+ ---> pass_info(
+ functor_info,
+ int, % Max number of errors to gather.
+ int % Max number of paths to analyze.
+ ).
%-----------------------------------------------------------------------------%
Index: compiler/termination.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/termination.m,v
retrieving revision 1.58
diff -u -r1.58 termination.m
--- compiler/termination.m 28 Nov 2005 04:11:57 -0000 1.58
+++ compiler/termination.m 1 Feb 2006 03:09:42 -0000
@@ -192,8 +192,8 @@
( terminates(Attributes) = does_not_terminate ->
TermErr = Context - inconsistent_annotations,
TermStatus = yes(can_loop([TermErr])),
- proc_info_set_maybe_termination_info(TermStatus,
- !ProcInfo),
+ % XXX intermod
+ proc_info_set_maybe_termination_info(TermStatus, !ProcInfo),
ProcNamePieces = describe_one_proc_name(!.ModuleInfo,
should_module_qualify, PPId),
Components =
@@ -217,6 +217,7 @@
TermErr = Context - inconsistent_annotations,
TermErrs = [TermErr | TermErrs0 ],
TermStatus = yes(can_loop(TermErrs)),
+ % XXX intermod
proc_info_set_maybe_termination_info(TermStatus,
!ProcInfo),
ProcNamePieces = describe_one_proc_name(!.ModuleInfo,
@@ -279,10 +280,8 @@
SCCTerminationKnown = []
;
SCCTerminationKnown = [KnownPPId | _],
- module_info_pred_proc_info(!.ModuleInfo, KnownPPId, _,
- KnownProcInfo),
- proc_info_get_maybe_termination_info(KnownProcInfo,
- MaybeKnownTerm),
+ module_info_pred_proc_info(!.ModuleInfo, KnownPPId, _, KnownProcInfo),
+ proc_info_get_maybe_termination_info(KnownProcInfo, MaybeKnownTerm),
(
MaybeKnownTerm = no,
unexpected(this_file, "No termination info. found.")
@@ -371,12 +370,12 @@
TermErrors = []
;
SCCArgSizeUnknown = [_|_],
- find_arg_sizes_in_scc(SCCArgSizeUnknown, !.ModuleInfo, PassInfo,
- ArgSizeResult, TermErrors, !IO),
+ find_arg_sizes_in_scc(SCCArgSizeUnknown, PassInfo, ArgSizeResult,
+ TermErrors, !ModuleInfo, !IO),
(
ArgSizeResult = ok(Solutions, OutputSupplierMap),
- set_finite_arg_size_infos(Solutions,
- OutputSupplierMap, !ModuleInfo),
+ set_finite_arg_size_infos(Solutions, OutputSupplierMap,
+ !ModuleInfo),
ArgSizeErrors = []
;
ArgSizeResult = error(Errors),
@@ -408,16 +407,14 @@
% These errors prevent pass 2 from proving termination
% in any case, so we may as well not prove it quickly.
PassInfo = pass_info(_, MaxErrors, _),
- list.take_upto(MaxErrors, BothErrors,
- ReportedErrors),
+ list.take_upto(MaxErrors, BothErrors, ReportedErrors),
TerminationResult = can_loop(ReportedErrors)
;
BothErrors = [],
globals.io_lookup_int_option(termination_single_args,
SingleArgs, !IO),
prove_termination_in_scc(SCCTerminationUnknown,
- !.ModuleInfo, PassInfo, SingleArgs,
- TerminationResult)
+ PassInfo, SingleArgs, TerminationResult, !ModuleInfo, !IO)
),
set_termination_infos(SCCTerminationUnknown, TerminationResult,
!ModuleInfo),
@@ -448,8 +445,8 @@
map__lookup(ProcTable, ProcId, ProcInfo),
map__lookup(OutputSupplierMap, PPId, OutputSuppliers),
ArgSizeInfo = finite(Gamma, OutputSuppliers),
- proc_info_set_maybe_arg_size_info(yes(ArgSizeInfo),
- ProcInfo, ProcInfo1),
+ % XXX intermod
+ proc_info_set_maybe_arg_size_info(yes(ArgSizeInfo), ProcInfo, ProcInfo1),
map__set(ProcTable, ProcId, ProcInfo1, ProcTable1),
pred_info_set_procedures(ProcTable1, PredInfo, PredInfo1),
map__set(PredTable0, PredId, PredInfo1, PredTable),
@@ -466,8 +463,8 @@
map.lookup(PredTable0, PredId, PredInfo),
pred_info_procedures(PredInfo, ProcTable),
map.lookup(ProcTable, ProcId, ProcInfo),
- proc_info_set_maybe_arg_size_info(yes(ArgSizeInfo),
- ProcInfo, ProcInfo1),
+ % XXX intermod
+ proc_info_set_maybe_arg_size_info(yes(ArgSizeInfo), ProcInfo, ProcInfo1),
map.set(ProcTable, ProcId, ProcInfo1, ProcTable1),
pred_info_set_procedures(ProcTable1, PredInfo, PredInfo1),
map.set(PredTable0, PredId, PredInfo1, PredTable),
@@ -486,6 +483,7 @@
map.lookup(PredTable0, PredId, PredInfo0),
pred_info_procedures(PredInfo0, ProcTable0),
map.lookup(ProcTable0, ProcId, ProcInfo0),
+ % XXX intermod
proc_info_set_maybe_termination_info(yes(TerminationInfo),
ProcInfo0, ProcInfo),
map.det_update(ProcTable0, ProcId, ProcInfo, ProcTable),
@@ -495,12 +493,11 @@
set_termination_infos(PPIds, TerminationInfo, !ModuleInfo).
:- pred report_termination_errors(list(pred_proc_id)::in,
- list(termination_error_context)::in,
+ termination_error_contexts::in,
module_info::in, module_info::out, io::di, io::uo) is det.
report_termination_errors(SCC, Errors, !ModuleInfo, !IO) :-
- globals.io_lookup_bool_option(check_termination,
- NormalErrors, !IO),
+ globals.io_lookup_bool_option(check_termination, NormalErrors, !IO),
globals.io_lookup_bool_option(verbose_check_termination,
VerboseErrors, !IO),
(
@@ -525,7 +522,7 @@
\+ pred_info_is_imported(PredInfo)
),
list.filter(IsNonImported, SCC, NonImportedPPIds),
- NonImportedPPIds = [_ | _],
+ NonImportedPPIds = [_|_],
% Don't emit non-termination warnings for the compiler
% generated wrapper predicates for solver type initialisation
@@ -535,13 +532,11 @@
% wrapper.
list.all_false(is_solver_init_wrapper_pred(!.ModuleInfo), SCC),
- % Only output warnings of non-termination for direct
- % errors. If there are no direct errors then output
- % the indirect errors - this is better than giving
- % no reason at all. If verbose errors is enabled then
- % output both sorts of error.
- % (See term_errors.m for details of direct and indirect
- % errors).
+ % Only output warnings of non-termination for direct errors. If there
+ % are no direct errors then output the indirect errors - this is
+ % better than giving no reason at all. If verbose errors is enabled
+ % then output both sorts of error.
+ % (See term_errors.m for details of direct and indirect errors.)
( VerboseErrors = yes ->
PrintErrors = Errors
@@ -600,8 +595,7 @@
check_preds([], !ModuleInfo, !IO).
check_preds([PredId | PredIds], !ModuleInfo, !IO) :-
write_pred_progress_message("% Checking ", PredId, !.ModuleInfo, !IO),
- globals.io_lookup_bool_option(make_optimization_interface,
- MakeOptInt, !IO),
+ globals.io_lookup_bool_option(make_optimization_interface, MakeOptInt, !IO),
module_info_preds(!.ModuleInfo, PredTable0),
map.lookup(PredTable0, PredId, PredInfo0),
pred_info_import_status(PredInfo0, ImportStatus),
@@ -740,7 +734,7 @@
% in the case where the type has user-defined equality.
%
:- pred special_pred_id_to_termination(special_pred_id::in,
- list(prog_var)::in, arg_size_info::out, termination_info::out) is det.
+ prog_vars::in, arg_size_info::out, termination_info::out) is det.
special_pred_id_to_termination(spec_pred_compare, HeadVars, ArgSize,
Termination) :-
@@ -783,6 +777,7 @@
Error = is_builtin(PredId),
ArgSizeInfo = yes(infinite([Context - Error]))
),
+ % XXX intermod
proc_info_set_maybe_arg_size_info(ArgSizeInfo, ProcInfo0, ProcInfo1),
proc_info_set_maybe_termination_info(yes(cannot_loop(unit)),
ProcInfo1, ProcInfo),
@@ -872,6 +867,7 @@
proc_info_get_maybe_termination_info(ProcInfo0, no)
)
->
+ % XXX intermod
proc_info_set_maybe_termination_info(yes(Termination),
ProcInfo0, ProcInfo),
svmap.det_update(ProcId, ProcInfo, !ProcTable)
--------------------------------------------------------------------------
mercury-reviews mailing list
post: mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the reviews
mailing list