3 Commits

Author	SHA1	Message	Date
Zoltan Somogyi	b4813457c9	A rewrite of termination analysis to make it significantly easier to modify, ... 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.	1997-12-22 10:01:33 +00:00
Thomas Conway	3c3e5fbda2	Modify termination analysis to use a linear inequation solver ... Estimated hours taken: 35 Modify termination analysis to use a linear inequation solver written in Mercury rather than invoking an external 3rd party one. compiler/term_pass1.m: Remove all the code for writing out the system of equations, invoking the solver and parsing the output. Add code to convert the system of equations into the format expected by the solver, and call the solver. compiler/term_errors.m: the 'lpsolve_failed' constructor goes from arity 1 to arity 0. modify the output of error messages accordingly. compiler/lp.m: NEW file. Contains the linear inequation solver based on the standard simplex method.	1997-10-20 04:12:41 +00:00
Christopher Rodd Speirs	f9ad85698a	Add termination analysis to the compiler. The termination analysis ... Estimated hours taken: 500 Add termination analysis to the compiler. The termination analysis annotates each procinfo structure with termination information stating whether each procedure is guaranteed to terminate. Add transitive intermodule optimization to the compiler. Transitive intermodule optimization uses .trans_opt files to store optimization information. The difference between .trans_opt files and .opt files is that .trans_opt files may depend on other .trans_opt files, whereas .opt files may only depend on a .m file. compiler/termination.m: New file. The main module which controls the termination analysis. compiler/term_pass1.m: New file. This file implements the first pass of the termination analysis which attempts to derive relationships between the relative sizes of variables. This information is used by term_pass2.m compiler/term_pass2.m: New file. The second pass of the termination analysis attempts to prove that each predicate or function in the program is guaranteed to terminate. compiler/term_util.m: New file. Contains utilities which are used in various stages of the termination analysis. compiler/term_errors.m: New file. Contains predicates for printing out error messages produced by termination analysis. compiler/trans_opt.m: New file. This module contains predicates for both reading in and writing .trans_opt files. compiler/globals.m: compiler/handle_options.m: compiler/options.m: Various modifications to handle the new options. Some of the new options imply other options, and the `--termination-norm' option is a string option which needs processing. compiler/hlds_goal.m: Added a comment that the list(uni_mode) subfield of construct, and the unify_mode subfield of unify are not necessarily valid when the unification applies to higher order terms. compiler/hlds_out.m: Added code to output termination information, as well as code to print out the new markers. compiler/hlds_pred.m: Added the termination subfield to the proc_info structure and added code to support it. Also added support for the new markers. compiler/make_hlds.m: compiler/mercury_to_mercury.m: compiler/module_qual.m: compiler/modules.m: compiler/prog_io_pragma.m: Added support for the new pragmas, `termination_info', `teminates', `check_termination' and `does_not_terminate'. compiler/prog_data.m: Added the new pragmas to the pragma_type. Also reformatted the type declarations to conform with the coding specifications. compiler/prog_io.m: Reformatted some code and comments. compiler/mercury_compiler.m: Added code to call the termination analyser and to call the predicate which creates .trans_opt files. doc/reference_manual.texi: Documented the termination analysis and the new pragmas. doc/user_guide.texi: Documented the new options.	1997-10-09 09:39:41 +00:00