for review: rewrite of termination analysis

Zoltan Somogyi zs at cs.mu.oz.au
Mon Dec 22 14:40:43 AEDT 1997


The diff will follow this message in three parts.

Estimated hours taken: 60

A rewrite of termination analysis to make it significantly easier to modify,
and to extend its capabilities.

compiler/error_util.m:
	A new file containing code that makes it easier to generate
	nicely formatted error messages.

compiler/termination.m:
	Updates to reflect the changes to the representation of termination
	information.

	Instead of doing pass 1 on all SCCs and then pass 2 on all SCCs,
	we now do both pass 1 and 2 on an SCC before moving on to the next.

	Do not insist that either all procedures in an SCC are
	compiler-generated or all are user-written, since this need not be
	true in the presence of user-defined equality predicates.

	Clarify the structure of the code that handles builtins and compiler
	generated predicates.

	Concentrate all the code for updating module_infos in this module.
	Previously it was scattered in several places in several files.

	Put all the code for writing out termination information at the
	end of the module in a logical order.

compiler/term_traversal.m:
	A new file containing code used by both pass 1 and pass 2 to
	traverse procedure bodies.

compiler/term_pass1.m:
	Use the new traversal module.

	Clarify the fixpoint computation on the set of output supplier
	arguments.

	Remove duplicates from the list of equations given to the solver.
	This avoids a det stack overflow in lp.m when doing termination
	analysis on options.m.

	If an output argument of a predicate makes sense only in the absence
	of errors, then return it only in the absence of errors.

compiler/term_pass2.m:
	Use the new traversal module. Unlike the previous code, this allows us
	to ignore recursive calls with input arguments bigger than the head
	if those calls occur after goals that cannot succeed (since those
	calls will never be reached).

	Implement a better way of doing single argument analysis, which
	(unlike the previous version) works in the presence of mutual recursion
	and other calls between the recursive call and the start of the clause.

	Implement a more precise way of checking for recursions that don't
	cause termination problems. We now allow calls from p to q in which
	the recursive input supplier arguments can grow, provided that on
	any path on which q can call p, directly or indirectly, the recursive
	input supplier arguments shrink by a greater amount.

	If an output argument of a predicate makes sense only in the absence
	of errors, then return it only in the absence of errors.

compiler/term_util.m:
	Updates to reflect the changes to the representation of termination
	information.

	Reorder to put related code together.

	Change the interface of several predicates to better reflect the
	way they are used.

	Add some more utility predicates.

compiler/term_errors.m:
	Small changes to the set of possible errors, and major changes in
	the way the messages are printed out (we now use error_util).

compiler/options.m:
	Change --term-single-arg from being a bool to an int option,
	whose value indicates the maximum size of an SCC in which we try
	single argument analysis. (Large SCCs can cause single-arg analysis
	to require a lot of iterations.)

	Add an (int) option that controls the max number of paths
	that we are willing to analyze (analyzing too many paths can cause
	det stack overflow).

	Add an (int) option that controls the max number of causes of
	nontermination that we print out.

compiler/hlds_pred.m:
	Use two separate slots in the proc_info to hold argument size data
	and termination info, instead of the single slot used until now.
	The two kinds of information are produced and used separately.

	Make the layout of the get and set procedures for proc_infos more
	regular, to facilitate later updates.

	The procedures proc_info_{,set_}variables did the same work as
	proc_info_{,set_}varset. To eliminate potential confusion, I
	removed the first set.

compiler/*.m:
	Change proc_info_{,set_}variables to proc_info_{,set_}varset.

compiler/hlds_out.m:
compiler/make_hlds.m:
compiler/mercury_to_mercury.m:
	Change the code to handle the arg size data and the termination
	info separately.

compiler/prog_data.m:
	Change the internal representation of termination_info pragmas to
	hold the arg size data and the termination info separately.

compiler/prog_io_pragma.m:
	Change the external representation of termination_info pragmas to
	group the arg size data together with the output supplier data,
	to which it is logically connected.

compiler/module_qual.m:
compiler/modules.m:
	Change the code to accommodate the change to the internal
	representation of termination_info pragmas.

compiler/notes/compiler_design.html:
	Fix some documentation rot, and clarify some points.

	Document termination analysis.

doc/user_guide.texi:
	Document --term-single-arg and the new options.

	Remove spaces from the ends of lines.

library/bag.m:
	Add a new predicate, bag__least_upper_bound.

	Fix code that would do the wrong thing if executed by Prolog.

	Remove spaces from the ends of lines.

library/list.m:
	Add a new predicate, list__take_upto.

library/set{,_ordlist}.m:
	Add a new predicate, set{,_ordlist}__count.

tests/term/*:
	A bunch of new test cases to test the behaviour of termination
	analysis. They are the small benchmark suite from our paper.

tests/Mmakefile:
	Enable the new test case directory.

Zoltan.



More information about the developers mailing list