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

[Fergus Henderson]

The final installment for this round of reviewing...

Christopher Rodd SPEIRS, you wrote:
> 
> %-----------------------------------------------------------------------------%
> % support functions for goal_inequality
> 
> :- pred join_offsets(list(term_pass1__equation), list(term_pass1__equation),
> 	list(term_pass1__equation)).
> :- mode join_offsets(in, in, out) is det.

Please document this predicate.

> join_offsets(In1, In2, Out) :-
> 	( In2 = [] ->
> 		Out = In1
> 	; 	
> 		(	
> 			In1 = [],
> 			Out = In2
> 		;
> 			In1 = [X | Xs],
> 			list__map(eqn_add(X), In2, Out1),
> 			( Xs = [] ->
> 				Out = Out1
> 			;
> 				join_offsets(Xs, In2, Out0),
> 				list__append(Out0, Out1, Out)
> 			)
> 			%list__merge_and_remove_dups(Out0, Out1, Out)

There's no need to special-case Xs = [] here.

> % Solve the list of constraints 
> 
> % output is of the form required by lp_solve (not yet)

I don't understand the "(not yet)" comment.

> 		io__get_environment_var("LPSOLVE", Lpsolve0),

Please prefix all environment variable names with `MERCURY_', to avoid
name clashes.

> 			;
> 				% Damn, it failed, interpret result, 
> 				% and were done

s/it failed,/it failed;/
s/were/we're/

> 		% dont forget to close, and delete files!!
> 		io__remove_file(ConstraintFile, Res1),
> 		( { Res1 = error(Error1) } ->
> 			{ io__error_message(Error1, Msg1) },
> 			io__write_strings([
> 				ProgName,
> 				": Error unlinking temporary file `",

s/unlinking/deleting/
(Ditto elsewhere)

> :- pred solve_eqns_parse_output_file(eqn_soln, io__state, io__state).
> :- mode solve_eqns_parse_output_file(out, di, uo) is det.
> solve_eqns_parse_output_file(Soln) -->
> 	io__read_line(Res1),
> 	( { Res1 = ok(_) } ->
> 		solve_eqns_parse_output_file_2(Soln0, MaybeBVal),
> 		( { Soln0 = solved(Result0) } ->
> 			( { MaybeBVal = yes(BVal) } ->
> 				{ solve_eqns_output_file_2(Result0, BVal,
> 					Result) },
> 				{ Soln = solved(Result) }
> 			;
> 				io__write_string("no bval\n"),
> 				{ Soln = parse_error }
> 			)
> 		;
> 			io__write_string(
> 				"parse_output_file returned not solved\n"),
> 			{ Soln = parse_error }
> 		)
> 	;
> 		{ Soln = parse_error }
> 	).

Should those calls to io__write_string really be there?

> :- pred solve_eqns_output_file_2(list(pair(pred_proc_id, int)), int,
> 	list(pair(pred_proc_id, int))).
> :- mode solve_eqns_output_file_2(in, in, out) is det.
> solve_eqns_output_file_2([], _, []). 
> solve_eqns_output_file_2([X | Xs], BVal, [Y | Ys]) :-
> 	X = PPId - XVal, 	% pair deconstruction
> 	YVal = XVal - BVal,	% subtraction

s/=/is/  (otherwise it won't work with NU-Prolog or SICStus Prolog).

> :- pred solve_eqns_parse_output_file_2(eqn_soln, maybe(int), io__state,
> 	io__state).
> :- mode solve_eqns_parse_output_file_2(out, out, di, uo) is det.
> solve_eqns_parse_output_file_2(Soln, BVal) -->
> 	io__read_line(Res1),
> 	( { Res1 = ok([ X | Xs ]) } ->
> 		( 
> 			{ X = 'a' },

What does the magic character 'a' mean?
Please at least document this better.

> 		; 
> 			{ X = 'b' },

Ditto for 'b'.

> :- pred char_list_remove_int(list(char), int, list(char)).
> :- mode char_list_remove_int(in, out, out) is semidet.
> char_list_remove_int([X | Xs], Int, ListOut) :-
> 	char__is_digit(X),
> 	char__to_int(X, Int0),
> 	Int1 = Int0 - 48,   % char__to_int('0', 48).
> 	char_list_remove_int_2(Xs, Int1, Int, ListOut).

Now where did we put the gun after we shot the last summer student...  ;-)

Magic numbers are evil.  Please avoid them.

> :- pred char_list_remove_int_2(list(char), int, int, list(char)).
> :- mode char_list_remove_int_2(in, in, out, out) is semidet.
> 
> char_list_remove_int_2([], Int, Int, []).
> char_list_remove_int_2([X | Xs], Int0, Int, ListOut) :-
> 	( char__is_digit(X) ->
> 		char__to_int(X, Int1),
> 		Int2 = Int0 * 10 + Int1 - 48,

Ditto.

> :- pred lpsolve_ret_val(int, eqn_soln).
> :- mode lpsolve_ret_val(in, out) is det.
> lpsolve_ret_val(Int, Result) :-
> 	( Int = -1	->	Result = fatal_error
> 	; Int = 0	->	Result = optimal
> 	; Int = 1	->	Result = failure
> 	; Int = 2	->	Result = infeasible
> 	; Int = 3	->	Result = unbounded
> 	; Int = 4	->	Result = failure
> 	; Int = 5	->	Result = failure
> 	; 			Result = failure
> 	).

Why all the different failure cases?  Please document them.

> 		{ Succ = no}	% XXX is this correct, or should we return 
> 				% the fact that we didnt output a constraint
> 				% currently if we dont print out any constraints
> 				% then lp_solve fails.

Please punctuate those sentences.

> % Copyright (C) 1995 University of Melbourne.

Please check the copyright dates on all the files you're adding.

> % used in termination_3_goal to keep track of the relative sizes of variables
> % between the head of a pred and any recursive calls.
> % the last argument is only used when doing single argument analysis.  It
> % stores which headvar was initially placed in this tuple.
> :- type termination_3
> 	--->	tuple(pred_proc_id, 	% The called proc
> 			int, 		% the relative size of the active
> 					% vars, in comparison with the 
> 					% recursive call
> 			bag(var), 	% tha bag of active vars
> 			maybe(var), 	% only for single arg. analysis
> 					% stores which headvar is being
> 					% traced by this tuple
> 			term__context).	% Where the call occured

It would be helpful if you could use better names than `termination_3'
and `tuple'.

> :- pred termination_2(module_info, dependency_ordering, module_info, io__state,
> 	io__state).
> :- mode termination_2(in, in, out, di, uo) is det.
> termination_2(Module, [], Module) --> [].
> termination_2(Module0, [SCC | SCCs], Module) -->
> 			% YYY
> 			%{ c_puts("termination_2") },

You need to fix that % YYY comment.

> :- pred termination_3(list(pred_proc_id), module_info, 
> 	term_util__result(term_error__error), relation(pred_proc_id), 
> 	relation(pred_proc_id)).
> :- mode termination_3(in, in, out, in, out) is det.

Some documentation for this pred would be good idea.
Also more informative names would help.

> 	(
> 		{ SingleArgs = yes },
> 		{ Rest = [] },
> 		{ Error \= _ - dont_know_proc(_) }
> 		% and Error=???

That comment is quite confusing.

> 			% single arg failed - bummer

Please use a term that wouldn't possibly offend anyone, rather than "bummer".
Remember that this code may be read by people from different cultures...

> 			Int < 0,
> 			% check that the var that was recursed on did not 
> 			% changeplace between the head and recursive call.  
> 			% I am not sure if the first call is actually 
> 			% required to succeed

s/changeplace/change place/

> 			bag__remove(VarBag0, HeadVar, VarBag1),
> 			\+ bag__remove_smallest(VarBag1, _, _)

Hmm, wouldn't `\+ bag__is_empty(VarBag1)' be better?

> 	;
> 		CallTermConst = not_set,
> 		error("Unexpected Termination Constant in termination.m"),
> 		Res0 = ok,
> 		Out1 = Out0

Delete the assignments to Res0 and Out1, they're not needed.
A comment here explaining why this condition was impossible
would be helpful.

> 	% step 1 - modify Out0

Could you please expand on that comment a bit?
Modify Out0 in what way?  What is this code trying to achieve?

> termination_3_goal(pragma_c_code(_, _, CallPredId, CallProcId, Args, _, _),
> 	GoalInfo, Module, _UnifyInfo, _CallInfo, Res, Out, Out) :-
> 
> 	module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
> 		CallProcInfo),
> 	proc_info_argmodes(CallProcInfo, CallArgModes),
> 	partition_call_args(Module, CallArgModes, Args, _InVars, OutVars),
> 	bag__from_list(OutVars, OutVarBag),
> 
> 	( termination_3_check_intersect(Out, OutVarBag) ->
> 		% c_code has no important output vars, so we need no error
> 		Res = ok
> 	;
> 		goal_info_get_context(GoalInfo, Context),
> 		Res = error(Context - pragma_c_code)
> 	).

A comment here explaining how you treat pragma c_codes would be helpful.

> %-----------------------------------------------------------------------------%
> % These following predicates all support termination_3_goal. 

s/all support/are all subroutines of/

> :- pred termination_3_modify_out(bag(var), bag(var), int, list(termination_3), 
> 	list(termination_3)).
> :- mode termination_3_modify_out(in, in, in, in, out) is det.
> termination_3_modify_out(_, _, _, [], []).
> termination_3_modify_out(InVars, OutVars, Off, [Out0 | Out0s], [Out | Outs]):-
> 	Out0 = tuple(PPId, Int0, Vars0, Var, Context),
> 	( bag__intersect(OutVars, Vars0) ->
> 		% there is an intersection
> 		bag__subtract(Vars0, OutVars, Vars1),
> 		bag__union(InVars, Vars1, Vars),
> 		Int = Int0 + Off,
> 		Out = tuple(PPId, Int, Vars, Var, Context)
> 	;
> 		% there is not an intersection
> 		Out = Out0
> 	),
> 	termination_3_modify_out(InVars, OutVars, Off, Out0s, Outs).

What is the variable "Off" supposed to represent here?
More meaningful variable names and/or better documentation would help here.

> :- module term_util.
> 
> :- interface.
> 
> :- import_module list, bool, bag, int, hlds_module, hlds_pred, hlds_data.
> :- import_module term_error, io, hlds_goal.
> 
> :- type termination 
> 	--->	 term(term_util__constant, terminates, maybe(list(bool)),
> 		maybe(term_error__error)).
> 	%   the final list has a 1:1 correspondance with the arguments of the
> 	%   proc.  it stores whether the arg is used in producing the 
> 	%   output args.  

What is the type `termination' used for?
Please document that.
Also, what do you mean by the "final" list?

> % 
> :- pred term_util__make_bool_list(proc_info, list(bool), list(bool)).
> :- mode term_util__make_bool_list(in, in, out) is det.
> 
> :- pred term_util__make_bool_list_2(list(var), list(bool), list(bool)).
> :- mode term_util__make_bool_list_2(in, in, out) is det.

Please document these.  Also, if something is exported from a module,
it should have a more meaningful name than `..._2'.

> :- pred partition_call_args(module_info, list(mode),
> 		list(var), list(var), list(var)).
> :- mode partition_call_args(in, in, in, out, out) is det.

Please document this.

> % removes vars from the InVarBag that are not used in the call
> :- pred remove_unused_args(bag(var), list(var), list(bool), bag(var)).
> :- mode remove_unused_args(in, in, in, out) is det.

The documentation here is not clear.  What are the intended
semantics of each argument?

> :- pred set_pred_proc_ids_const(list(pred_proc_id), term_util__constant,
> 	module_info, module_info).
> :- mode set_pred_proc_ids_const(in, in, in, out) is det.
> 
> :- pred set_pred_proc_ids_terminates(list(pred_proc_id), terminates,
> 	maybe(term_error__error), module_info, module_info).
> :- mode set_pred_proc_ids_terminates(in, in, in, in, out) is det.

> :- pred split_unification_vars(list(var), list(uni_mode), module_info,
> 	bag(var), bag(var)).
> :- mode split_unification_vars(in, in, in, out, out) is det.

Please document these.

> split_unification_vars([], Modes, _ModuleInfo, Vars, Vars) :-
> 	bag__init(Vars),
> 	( Modes = [] ->
> 		true
> 	;
> 		error("Error in termination.m")
> 	).

This is in term_util.m, so the error message shouldn't say termination.m.
Please add a comment explaining why this is an error.

> split_unification_vars([Arg | Args], Modes, ModuleInfo,
> 		InVars,OutVars):-

s/,/, /

> 
> 	( Modes = [UniMode | UniModes] ->
> 		split_unification_vars(Args, UniModes, ModuleInfo,
> 			InVars0, OutVars0),
> 		UniMode = ((_VarInit - ArgInit) -> (_VarFinal - ArgFinal)),
> 		( %if
> 			inst_is_bound(ModuleInfo, ArgInit) 
> 		->
> 			(
> 				% is input var
> 				bag__insert(InVars0, Arg, InVars),
> 				OutVars = OutVars0
> 			)
> 		; %elseif
> 			( 
> 				inst_is_free(ModuleInfo, ArgInit),
> 				inst_is_bound(ModuleInfo, ArgFinal) 
> 			) 
> 		->
> 			%is outputvar
> 			InVars = InVars0,
> 			bag__insert(OutVars0, Arg, OutVars)
> 		; %else
> 			InVars = InVars0,
> 			OutVars = OutVars0
> 		)
> 	;
> 		error("Error in termination.m")
> 	).

This is buggy, as we discussed.

> 	proc_info_termination(ProcInfo0, Termination0),
> 	Termination0 = term(_Const, Term, UsedArgs, MaybeError),
> 	Termination = term(Const, Term, UsedArgs, MaybeError),
> 	% YYY
> 	%c_put_term(PPId, Termination),
> 	proc_info_set_termination(ProcInfo0, Termination, ProcInfo),

That % YYY comment needs fixing.

> 	Termination0 = term(Const, _Terminates, UsedArgs, _),
> 	Termination = term(Const, Terminates, UsedArgs, MaybeError),
> 	% YYY
> 	%c_put_term(PPId, Termination),
> 	proc_info_set_termination(ProcInfo0, Termination, ProcInfo),

Ditto.

> 	error("Unmatched Vars in termination.m").

s/Vars/vars/

> partition_call_args(ModuleInfo, [ArgMode | ArgModes], [Arg | Args],
> 		InputArgs, OutputArgs) :-
> 	partition_call_args(ModuleInfo, ArgModes, Args,
> 		InputArgs1, OutputArgs1),
> 	( mode_is_input(ModuleInfo, ArgMode) ->
> 		InputArgs = [Arg | InputArgs1],
> 		OutputArgs = OutputArgs1
> 	; mode_is_output(ModuleInfo, ArgMode) ->
> 		InputArgs = InputArgs1,
> 		OutputArgs = [Arg | OutputArgs1]
> 	;
> 		InputArgs = InputArgs1,
> 		OutputArgs = OutputArgs1
> 	).

Should those be calls to mode_is_fully_input and mode_is_fully_output?

> functor_norm(simple, ConsId, _, Int) :-
> 	( 
> 		ConsId = cons(_, Arity),
> 		Arity \= 0
> 	->
> 		Int = 1
> 	;
> 		Int = 0
> 	).

That doesn't match the documentation, which says "assigns all functors
a norm of 1".  You should change the documentation to say "assigns all
functors a norm of 1 and all constants a norm of zero".

> functor_norm(total, ConsId, _Module, Int) :-
> 	( ConsId = cons(_, Arity) ->
> 		Int = Arity
> 	;
> 		Int = 1
> 	).

What about pred_consts?

> :- type term_error__error == pair(term__context, termination_error).
> :- type termination_error
> 	--->	positive_value(pred_proc_id, pred_proc_id)
> 			% a recursive call is made with variables that are 
> 			% strictly larger than in the head.  note that 
> 			% the recursive call may be indirect, so this does 
> 			% not neccessarily indicate non-termination.
> 			% The first PPId is the calling proc.  The second
> 			% PPId is the called proc, and the context is the
> 			% line where the call occurs.

s/indirect/conditional/ ?

> 	;	not_subset(bag(var), bag(var))
> 	;	horder_call
> 	;	pragma_c_code
> 	;	dont_know_proc(pred_proc_id)
> 	;	dont_know_proc_called(pred_proc_id)
> 	;	horder_args(pred_proc_id)
> 	;	inf_termination_const(pred_proc_id)
> 	;	ite_wrong_vars(bag(var), bag(var))
> 	;       switch_wrong_vars(bag(var), bag(var))
> 	;       disj_wrong_vars(bag(var), bag(var))
> 	;	not_dag
> 	;	no_eqns
> 	;	lpsolve_failed(eqn_soln)
> 	;	call_in_single_arg(pred_proc_id)
> 	;	single_arg_failed(term_error__error)
> 	;	single_arg_failed(term_error__error, term_error__error).

Please document these.  E.g. what does `not_subset' indicate,
and what do the arguments mean (what is the correct argument order?).
What does `dont_know_proc' mean, and when could it occur?
What do `inf', `ite', and `dag' stand for?  What does wrong_vars mean?
etc.

> % eqn_soln are used to report the results from solving the equations
> % created in the first pass.  The first 4 (optimal - failure) represent
> % output states from lp_solve. 
> :- type eqn_soln
> 	---> 	optimal		
> 	;	infeasible
> 	;	unbounded
> 	;	failure
> 	;	fatal_error 	% unable to open a file, or make a system call
> 	;	parse_error	% unable to parse the output from lp_solve
> 	;	solved(list(pair(pred_proc_id, int))).

What's the difference between infeasible, unbounded, and failure?
What's the difference between optimal and solved?

> :- implementation.
> 
> :- import_module hlds_out, prog_out, hlds_pred.
> 
> term_error__output(MaybePredId, Module, 
> 		Context - positive_value(CallerPPId, CalledPPId)) -->	
> 	( { MaybePredId = yes(PredId) } ->
> 		{ CalledPPId = proc(CalledPredId, _CalledProcId) },
> 		{ CallerPPId = proc(CallerPredId, _CallerProcId) },
> 		prog_out__write_context(Context),
> 		io__write_string("Unable to check termination in predicate:\n"),

s/://

> 		prog_out__write_context(Context),
> 		hlds_out__write_pred_id(Module, PredId),

> 		( { PredId = CallerPredId } ->
> 			io__write_string("as it contains a\n")

s/as/ as/

Please add test cases to exercise all these errors and warnings.

> 		;
> 			io__nl,
> 			prog_out__write_context(Context),
> 			io__write_string(
> 				"as it is in the same SCC as the following predicate\n"
> 				),

s/as/  as/

You need to indent the second and subsequent lines of error messages by
two spaces.

> 			prog_out__write_context(Context),
> 			hlds_out__write_pred_id(Module, CallerPredId),

Add
 			io__write_string("  "),

before the call to write_pred_id.

> 		prog_out__write_context(Context),
> 		( { PredId = CalledPredId } ->
> 			io__write_string("directly recursive call")
> 		;
> 			io__write_string("recursive call to"),
> 			hlds_out__write_pred_id(Module, CalledPredId),
> 			io__nl,
> 			prog_out__write_context(Context)
> 		),
> 		io__write_string("with the size of the variables increased.\n")

More buggy formatting.
Please fix it.

> 	;
> 		% only for hlds_dump
> 		{ CalledPPId = proc(CalledPredId, _CalledProcId) },
> 		{ CallerPPId = proc(CallerPredId, _CallerProcId) },
> 		prog_out__write_context(Context),
> 		io__write_string("this SCC contains a recursive call from "),
> 		hlds_out__write_pred_id(Module, CallerPredId),
> 		io__write_string("to "),
> 		hlds_out__write_pred_id(Module, CalledPredId),
> 		io__write_string("with the size of the variables increased.\n")
> 	).
> term_error__output(MaybePredId, Module, Context - horder_call) -->
> 	prog_out__write_context(Context),
> 	( { MaybePredId = yes(PredId) } ->
> 		hlds_out__write_pred_id(Module, PredId)
> 	;
> 		[]
> 	),
> 	io__write_string("horder_call\n").

Does that string ("horder_call") get output in messages that the user will see?
If so, you need to write it in English, not cryptic abbreviations.
Ditto for all the remaining clauses for this predicate.

I would like to see test cases that exercise all these errors and warnings.

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