[m-rev.] for review: termination analysis of initialisation predicates

[Julien Fischer]

On Thu, 24 Feb 2005, Julien Fischer wrote:

> (This is currently bootchecking).
>
> For review by Ralph.
>
> Estimated hours taken: 1
> Branches: main, release
>
> Improve the termination analysis of solver type initialisation
> predicates by running the main analysis on them rather than setting
> argument size information and termination status beforehand.
>
> compiler/termination.m:
> 	Ran the main analysis on solver type intialisation predicates.
>
> 	Update an XXX comment about user-defined equality, comparison
> 	and initialisation predicates.  It no longer applies to
> 	initialisation predicates and never applied to comparison predicates
> 	anyway.
>

One thing I forgot to do was disable warnings for compiler generated
wrapper predicates for solver type initialisers.  The modified diff
below fixes that (and also fixes a mispelling of the word initialisation).

Index: termination.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/termination.m,v
retrieving revision 1.48
diff -u -r1.48 termination.m
--- termination.m	22 Jan 2005 06:10:53 -0000	1.48
+++ termination.m	24 Feb 2005 05:58:29 -0000
@@ -96,7 +96,7 @@
 :- import_module bool, std_util, list.
 :- import_module map, int, char, string, relation.
 :- import_module require, bag, set, term.
-:- import_module varset.
+:- import_module varset, svmap.

 %----------------------------------------------------------------------------%

@@ -514,6 +514,14 @@
 		list__filter(IsNonImported, SCC, NonImportedPPIds),
 		NonImportedPPIds = [_ | _],

+		% Don't emit non-termination warnings for the compiler
+		% generated wrapper predicates for solver type initialisation
+		% predicates.  If they don't terminate there's nothing the user
+		% can do about it anyway - the problem is with the
+		% initialisation predicate specified by the user, not the
+		% wrapper.
+		list__all_false(is_solver_init_wrapper_pred(!.Module), 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
@@ -545,6 +553,18 @@
 		true
 	).

+	% Succeeds iff the given PPId is a compiler generated wrapper
+	% predicate for a solver type initialisation predicate.
+	%
+:- pred is_solver_init_wrapper_pred(module_info::in, pred_proc_id::in)
+	is semidet.
+
+is_solver_init_wrapper_pred(ModuleInfo, proc(PredId, _)) :-
+	module_info_pred_info(ModuleInfo, PredId, PredInfo),
+	pred_info_get_origin(PredInfo, PredOrigin),
+	PredOrigin = special_pred(SpecialPredId - _),
+	SpecialPredId = initialise.
+
 %----------------------------------------------------------------------------%

 :- pred check_preds(list(pred_id)::in, module_info::in, module_info::out,
@@ -683,18 +703,28 @@

 set_generated_terminates([], _, !ProcTable).
 set_generated_terminates([ProcId | ProcIds], SpecialPredId, !ProcTable) :-
-	map__lookup(!.ProcTable, ProcId, ProcInfo0),
-	proc_info_headvars(ProcInfo0, HeadVars),
-	special_pred_id_to_termination(SpecialPredId, HeadVars,
-		ArgSize, Termination),
-	proc_info_set_maybe_arg_size_info(yes(ArgSize), ProcInfo0, ProcInfo1),
-	proc_info_set_maybe_termination_info(yes(Termination),
-		ProcInfo1, ProcInfo),
-	map__det_update(!.ProcTable, ProcId, ProcInfo, !:ProcTable),
+	%
+	% We don't need to do anything special for solver type initialisation
+	% predicates.  Leaving it up to the analyser may result in better
+	% argument size information anyway.
+	%
+	( SpecialPredId \= initialise ->
+		map__lookup(!.ProcTable, ProcId, ProcInfo0),
+		proc_info_headvars(ProcInfo0, HeadVars),
+		special_pred_id_to_termination(SpecialPredId, HeadVars,
+			ArgSize, Termination),
+		proc_info_set_maybe_arg_size_info(yes(ArgSize), ProcInfo0,
+			ProcInfo1),
+		proc_info_set_maybe_termination_info(yes(Termination),
+			ProcInfo1, ProcInfo),
+		svmap__det_update(ProcId, ProcInfo, !ProcTable)
+	;
+		true
+	),
 	set_generated_terminates(ProcIds, SpecialPredId, !ProcTable).

-	% XXX The ArgSize arguments for unify, compare and initialise
-	% are not necessarily correct since these may be user-defined.
+	% XXX The ArgSize argument for unify predicates may not be correct
+	% 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.
@@ -711,10 +741,9 @@
 	term_util__make_bool_list(HeadVars, [no, no], OutList),
 	ArgSize = finite(0, OutList),
 	Termination = cannot_loop.
-special_pred_id_to_termination(initialise, HeadVars, ArgSize, Termination) :-
-	term_util__make_bool_list(HeadVars, [yes], OutList),
-	ArgSize = finite(0, OutList),
-	Termination = cannot_loop.
+special_pred_id_to_termination(initialise, _, _, _) :-
+	unexpected(this_file, "special_pred_id_to_termination/4 " ++
+		"initialise predicate").

 % The list of proc_ids must refer to builtin predicates.  This predicate
 % sets the termination information of builtin predicates.

Julien.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------