[m-dev.] Tdiff: termination analysis (BIG!)

[Fergus Henderson]

Another installment...

Christopher Rodd SPEIRS, you wrote:
> 
> termination__maybe_output_error(Module, term(Const, _, _, MaybeError)) -->
> 	( { MaybeError = yes(Error) } ->
> 		io__write_string("% unable to determine termination as:"),
> 		term_error__output(no, Module, Error)
> 	;
> 		[]
> 	),
> 	( { Const = inf(yes(ConstError)) } ->
> 		io__write_string("% unable to set const as:"),
> 		term_error__output(no, Module, ConstError)
> 	;
> 		[]
> 	).

Please use "since" or "because" or "due to" rather than "as" here.

> 	(
> 		(
> 		ImportStatus = exported
> 		; ImportStatus = local
> 		; ImportStatus = pseudo_exported
> 		)

Please indent all the unifications equally, i.e.

 		( ImportStatus = exported
 		; ImportStatus = local
 		; ImportStatus = pseudo_exported
 		)

(ditto elsewhere)

> 	->
> 		pred_info_get_marker_list(PredInfo0, Markers),
> 		( list__member(request(terminates), Markers) ->
> 			change_procs_terminate(ProcIds, no, yes,
> 				 no, ProcTable0, ProcTable2)

Please use variable names to explain the meaning of these `no's and `yes's.
i.e.

			Something = no,
			SomethingElse = yes,
			AnotherSomething = no,
 			change_procs_terminate(ProcIds, Something,
				SomethingElse, AnotherSometing,
				ProcTable0, ProcTable2)

(ditto in one or two other places)

> 	; %else if
> 		(
> 		ImportStatus = imported
> 		; ImportStatus = opt_decl  % should this be here?
> 		; ImportStatus = opt_imported
> 		; ImportStatus = pseudo_imported  % should this be here?
> 		)
> 	->
> 		% all of the predicates that are processed here are imported
> 		% in some way
> 		% with imported predicates, any 'request(check_termination)'
> 		% markers will be checked by the compiler when it compiles
> 		% relevant source file (that the pred was imported from)
> 		% When making the intermodule optimizations, the 
> 		% check_termination will not be checked, so it cannot
> 		% be depended upon

Please punctuate your comments.

I don't understand the last sentence.  Please restate it more clearly.

(Why won't the check_termination be checked when making the
intermodule optimizations?)

> %		(
> %		ImportStatus = abstract_imported
> %		; ImportStatus = abstract_exported
> %		),
> 		% this should not happen, as procedures are being processed
> 		% here, and these import_status' refer to abstract types
> 		error("Unexpected Import Status of a predicate"),
> 		ProcTable2 = ProcTable0,
> 		State0 = State1

You can delete those two unifications after the call to error/1, they're
not needed.

> 	),
> 	( 
> 		% dont know if compiler gen/mercury_builtin preds will be 
> 		% imported or not

s/gen/generated/   (I presume I got that expansion right?)

I'm not going to be picky about punctuation, but remember that code
is written once and read many times, so it is worth while getting
the punctuation right.

> % this pred checs to see if the ProcId is a compiler generated pred, or a
> % mercury_builtin pred.  If it is, then it sets the termination property 
> % of the ProcIds accordingly.

Do you mean a pred defined in module `mercury_builtin',
or do you mean a builtin pred, such as `int:<'?
Either way, please make it clear.

> :- pred set_compiler_gen_terminates(list(proc_id), pred_info, module_info,
> 	proc_table, proc_table).
> :- mode set_compiler_gen_terminates(in, in, in, in, out) is semidet.
> set_compiler_gen_terminates([], _PredInfo, _Module, ProcTable, ProcTable).
> set_compiler_gen_terminates([ ProcId | ProcIds ], PredInfo, Module, 
> 		ProcTable0, ProcTable) :-
> 	pred_info_name(PredInfo, PredName),
> 	pred_info_arity(PredInfo, Arity),
> 	pred_info_module(PredInfo, ModuleName),
> 	( Arity = 3 ->
> 		(
> 			PredName = "__Compare__"
> 		;
> 			ModuleName = "mercury_builtin",
> 			PredName = "compare"
> 		),
> 		map__lookup(ProcTable0, ProcId, ProcInfo0),
> 		term_util__make_bool_list(ProcInfo0,
> 			[no, no, no], OutList),
> 		Termination = term(set(0), yes, yes(OutList), no)
> 	; Arity = 2 ->
> 		(
> 			(
> 				PredName = "__Unify__"
> 			;
> 				ModuleName = "mercury_builtin",
> 				PredName = "unify"
> 			)
> 		->
> 			map__lookup(ProcTable0, ProcId, ProcInfo0),
> 			term_util__make_bool_list(ProcInfo0,
> 				[yes, yes], OutList),
> 			Termination = term(set(0), yes,
> 				yes(OutList), no)
> 		; % else if
> 			( 
> 				PredName = "__Index__"
> 			;
> 				ModuleName = "mercury_builtin",
> 				PredName = "index"
> 			)
> 		->
> 			map__lookup(ProcTable0, ProcId, ProcInfo0),
> 			term_util__make_bool_list(ProcInfo0,
> 				[no, no], OutList),
> 			Termination = term(set(0), yes,
> 				yes(OutList), no)
> 		; % else if
> 			% XXX what is the relationship between size of
> 			% input and size of output in Term_To_Type and
> 			% Type_To_Term?  Which arguments are used to make
> 			% the output variables?
> 			PredName = "__Term_To_Type__"
> 		->
> 			map__lookup(ProcTable0, ProcId, ProcInfo0),
> 			Termination = term(inf(no), yes, no, no)
> 		;
> 			PredName = "__Type_To_Term__",
> 			map__lookup(ProcTable0, ProcId, ProcInfo0),
> 			Termination = term(inf(no), yes, no, no)
> 		)

This is not going to be maintainable.  Someone is going to come along
and add a new special pred and they are not going to know that they
need to modify termination analysis.  There is also quite a bit of code
duplication there.

You should use a more table-driven approach. 
Use special_pred_name_arity to convert pred names & arities to a
special_pred_id, and than have a det pred indexed on special_pred_id
that gives whatever information is needed for termination analysis.

> 	;
> 		ModuleName = "mercury_builtin",
> 		map__lookup(ProcTable0, ProcId, ProcInfo0),
> 		( attempt_set_proc_const(Module, PredInfo, ProcInfo0) ->
> 			proc_info_headvars(ProcInfo0, HeadVars),
> 			term_util__make_bool_list_2(HeadVars, [], Bools),
> 			UsedArgs = yes(Bools),
> 			Termination = term(set(0), yes, UsedArgs, no)
> 		;
> 			proc_info_termination(ProcInfo0, OldTerm),
> 			OldTerm = term(OldConst, _, OldUsedArgs, _),
> 			Termination = term(OldConst, yes, OldUsedArgs, no)
> 		)
> 	),

I don't understand what that code does.  Please document it.

> 	% it is a compiler generated procedure, so enter the data in
> 	% the proc_inf

s/proc_inf/proc_info/

> % for attempt_set_proc_const to succeed, the output vars of
> % that proc must all be of a type that cannot be recursive.
> % hence the size of the output vars will all be size 0,
> % independent on the input variables. 

s/on/of/

> attempt_set_proc_const_2([Type | Types], [Mode | Modes], Module) :-
> 	( mode_is_input(Module, Mode) ->
> 		% doesnt matter what type it is
> 		attempt_set_proc_const_2(Types, Modes, Module)

Do you mean `mode_is_fully_input' here?

> 	;
> 		classify_type(Type, Module, TypeOfType),
> 		% 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.
> 		TypeOfType \= user_type(_), 
> 		% this could be changed, by looking up the poly type, 
> 		% and seeing if that is recursive, or could it?
> 		TypeOfType \= polymorphic_type, 
> 		TypeOfType \= pred_type,
> 		attempt_set_proc_const_2(Types, Modes, Module)
> 	).

I think s/TypeOfType/TypeCategory/ would make it clearer.

> :- module term_pass1.
> 
> :- interface.
> 
> :- import_module io, hlds_module.
> 
> % get dependency ordering, and call proc_ineq_2 with them
> :- pred proc_inequalities(module_info, module_info, io__state, 
> 	io__state).
> :- mode proc_inequalities(in, out, di, uo) is det.

That is not good as interface documentation.
The reader should not have to read the entire module to understand
what a procedure does.

Please use something like

	% proc_inequalities computes [whatever it computes] for each procedure
	% and stores the results in the [whatever] field in the proc_info.

> :- implementation.
> 
> :- import_module term_util, hlds_pred, hlds_goal, hlds_data, int, bag.
> :- import_module term_error, list, require, bool, std_util, char, map, string.
> :- import_module mode_util.
> 
> % this section contains proc_inequalities and its supporting functions.
> % proc_inequalities goes through the dependency ordering, applying 
> % goal_inequality to each SCC in turn, and solving the resulting constraints

What does "dependency ordering" mean?  What sort of dependencies?
I think it would be clearer if you said

	traverses the module's call graph bottom-up

instead of

	goes through the dependency ordering

> % Types used only in this section
> %
> % term_pass1__equation stores a single constraint
> % the constraint is of the form:
> % pred_proc_id - list(pred_proc_id) >= term_util__constant
> :- type term_pass1__equation
> 	---> 	eqn(term_util__constant, pred_proc_id, list(pred_proc_id)).

What does the constraint mean?
I don't understand this subtraction operator on pred_proc_ids.

> 		;
> 			% Hmm, this shouldnt happen...
> 			{ Module = Module0 },
> 			{ error("Unexpected setting of termination constant")}

The unification `Module = Module0' is redundant.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.