diff --git a/compiler/notes/compiler_design.html b/compiler/notes/compiler_design.html index 46617ca15..40fe7059a 100644 --- a/compiler/notes/compiler_design.html +++ b/compiler/notes/compiler_design.html @@ -1792,11 +1792,19 @@ which are in the termination.term_constr package, are term_constr_errors.m generates error messages for termination problems.

-The termination package also contains two other modules: -term_norm.m, which defines the metrics we can use -to measure the sizes of terms (inputs and outputs), and -term_post_analysis.m, which contains error checking routines and optimizations -that depend upon the information obtained by termination analysis. +The termination package also contains three other modules: +

  • Trailing analysis (trailing_analysis.mi) annotates each module with information about whether the procedures in the module modify the trail or not. diff --git a/compiler/term_constr_errors.m b/compiler/term_constr_errors.m index 20fb9f316..b2bc878a3 100644 --- a/compiler/term_constr_errors.m +++ b/compiler/term_constr_errors.m @@ -80,8 +80,7 @@ :- import_module libs. :- import_module libs.globals. :- import_module libs.options. -:- import_module termination.term_osi. % ZZZ -:- import_module termination.term_osi.term_osi_util. +:- import_module termination.term_util. :- import_module bool. :- import_module cord. diff --git a/compiler/term_constr_initial.m b/compiler/term_constr_initial.m index ceb656b68..81bb0df24 100644 --- a/compiler/term_constr_initial.m +++ b/compiler/term_constr_initial.m @@ -77,8 +77,7 @@ :- import_module termination.term_constr.term_constr_errors. :- import_module termination.term_constr.term_constr_main_types. :- import_module termination.term_constr.term_constr_util. -:- import_module termination.term_osi. % ZZZ -:- import_module termination.term_osi.term_osi_util. +:- import_module termination.term_util. :- import_module bool. :- import_module int. diff --git a/compiler/term_osi_errors.m b/compiler/term_osi_errors.m index b7a2b4140..9b9755870 100644 --- a/compiler/term_osi_errors.m +++ b/compiler/term_osi_errors.m @@ -174,6 +174,7 @@ :- import_module parse_tree.prog_data_pragma. :- import_module parse_tree.var_table. :- import_module termination.term_osi.term_osi_util. +:- import_module termination.term_util. :- import_module cord. :- import_module int. diff --git a/compiler/term_osi_main.m b/compiler/term_osi_main.m index 7ed7b257d..b62cd7467 100644 --- a/compiler/term_osi_main.m +++ b/compiler/term_osi_main.m @@ -61,6 +61,7 @@ :- import_module termination.term_osi.term_osi_pass2. :- import_module termination.term_osi.term_osi_util. :- import_module termination.term_post_analysis. +:- import_module termination.term_util. :- import_module bool. :- import_module map. diff --git a/compiler/term_osi_pass1.m b/compiler/term_osi_pass1.m index 673ac7d15..5a627f237 100644 --- a/compiler/term_osi_pass1.m +++ b/compiler/term_osi_pass1.m @@ -66,6 +66,7 @@ :- import_module parse_tree.prog_data_pragma. :- import_module parse_tree.var_table. :- import_module termination.term_osi.term_osi_traversal. +:- import_module termination.term_util. :- import_module bag. :- import_module bool. diff --git a/compiler/term_osi_traversal.m b/compiler/term_osi_traversal.m index b8c84feee..77629c5d7 100644 --- a/compiler/term_osi_traversal.m +++ b/compiler/term_osi_traversal.m @@ -119,6 +119,7 @@ :- import_module parse_tree.prog_data_pragma. :- import_module parse_tree.prog_type. :- import_module parse_tree.prog_type_test. +:- import_module termination.term_util. :- import_module bool. :- import_module int. diff --git a/compiler/term_osi_util.m b/compiler/term_osi_util.m index 254dbf31f..698b87ec8 100644 --- a/compiler/term_osi_util.m +++ b/compiler/term_osi_util.m @@ -7,7 +7,7 @@ % Public License - see the file COPYING in the Mercury distribution. %---------------------------------------------------------------------------% % -% File: term_util.m. +% File: term_osi_util.m. % Main author: crs. % % This module: @@ -23,12 +23,9 @@ :- import_module hlds. :- import_module hlds.hlds_goal. :- import_module hlds.hlds_module. -:- import_module hlds.hlds_pred. -:- import_module hlds.hlds_proc. :- import_module hlds.pred_proc_id. :- import_module parse_tree. :- import_module parse_tree.prog_data. -:- import_module parse_tree.prog_data_foreign. :- import_module parse_tree.prog_data_pragma. :- import_module parse_tree.var_table. :- import_module termination.term_norm. @@ -135,14 +132,6 @@ % :- pred pred_proc_id_terminates(module_info::in, pred_proc_id::in) is semidet. -%---------------------% - - % Succeed if all arguments of the given procedure of the given predicate - % are either input or zero size. - % -:- pred all_args_input_or_zero_size(module_info::in, pred_info::in, - proc_info::in) is semidet. - %---------------------% % This predicate sets the argument size info of a given a list of @@ -171,54 +160,18 @@ :- pred add_context_to_arg_size_info(maybe(pragma_arg_size_info)::in, prog_context::in, maybe(arg_size_info)::out) is det. -%---------------------------------------------------------------------------% - -:- pred get_context_from_scc(module_info::in, scc::in, prog_context::out) - is det. - -%---------------------------------------------------------------------------% - - % Succeeds if the foreign proc attributes imply that a procedure is - % terminating. - % -:- pred attributes_imply_termination(foreign_proc_attributes::in) - is semidet. - -%---------------------------------------------------------------------------% - -:- type maybe_believe_check_termination - ---> do_not_believe_check_termination - ; do_believe_check_termination. - - % When we process imported predicates, should we believe that - % the presence of a 'check_termination' pragma, or rather the pred marker - % indicating the presence of such a pragma, guarantees that (in the absence - % of an error from that pragma) the predicate will actually terminate? - % - % The check_termination pragma will be checked by the compiler - % when it compiles the source file that the predicate was imported from. - % However, when we make .opt files, we do not check whether predicates - % with check_termination pragmas actually terminate, so we cannot assume - % that they do, since any violations of that assumption will *not* be - % reported. - % -:- pred should_we_believe_check_termination_markers(module_info::in, - maybe_believe_check_termination::out) is det. - %---------------------------------------------------------------------------% %---------------------------------------------------------------------------% :- implementation. +:- import_module hlds.hlds_pred. +:- import_module hlds.hlds_proc. :- import_module hlds.inst_test. :- import_module hlds.mode_test. -:- import_module libs. -:- import_module libs.globals. -:- import_module libs.op_mode. :- import_module parse_tree.prog_type_test. :- import_module require. -:- import_module set. %---------------------------------------------------------------------------% %---------------------------------------------------------------------------% @@ -343,30 +296,6 @@ pred_proc_id_terminates(ModuleInfo, PPId) :- %---------------------------------------------------------------------------% -all_args_input_or_zero_size(ModuleInfo, PredInfo, ProcInfo) :- - pred_info_get_arg_types(PredInfo, TypeList), - proc_info_get_argmodes(ProcInfo, ModeList), - all_args_input_or_zero_size_2(TypeList, ModeList, ModuleInfo). - -:- pred all_args_input_or_zero_size_2(list(mer_type)::in, list(mer_mode)::in, - module_info::in) is semidet. - -all_args_input_or_zero_size_2([], [], _). -all_args_input_or_zero_size_2([], [_|_], _) :- - unexpected($pred, "unmatched lists"). -all_args_input_or_zero_size_2([_|_], [], _) :- - unexpected($pred, "unmatched lists"). -all_args_input_or_zero_size_2([Type | Types], [Mode | Modes], ModuleInfo) :- - ( if mode_is_input(ModuleInfo, Mode) then - % The variable is an input variables, so its size is irrelevant. - all_args_input_or_zero_size_2(Types, Modes, ModuleInfo) - else - term_norm.zero_size_type(ModuleInfo, Type), - all_args_input_or_zero_size_2(Types, Modes, ModuleInfo) - ). - -%---------------------------------------------------------------------------% - set_pred_proc_ids_arg_size_info([], _ArgSize, !ModuleInfo). set_pred_proc_ids_arg_size_info([PPId | PPIds], ArgSize, !ModuleInfo) :- PPId = proc(PredId, ProcId), @@ -401,40 +330,6 @@ add_context_to_arg_size_info(yes(finite(A, B)), _, yes(finite(A, B))). add_context_to_arg_size_info(yes(infinite(_)), Context, yes(infinite([term_error(Context, imported_pred)]))). -%---------------------------------------------------------------------------% - -get_context_from_scc(ModuleInfo, SCC, Context) :- - set.to_sorted_list(SCC, SCCProcs), - ( - SCCProcs = [proc(PredId, _) | _], - module_info_pred_info(ModuleInfo, PredId, PredInfo), - pred_info_get_context(PredInfo, Context) - ; - SCCProcs = [], - unexpected($pred, "empty SCC") - ). - -%---------------------------------------------------------------------------% - -attributes_imply_termination(Attributes) :- - ( - get_terminates(Attributes) = proc_terminates - ; - get_terminates(Attributes) = depends_on_mercury_calls, - get_may_call_mercury(Attributes) = proc_will_not_call_mercury - ). - -%---------------------------------------------------------------------------% - -should_we_believe_check_termination_markers(ModuleInfo, Believe) :- - module_info_get_globals(ModuleInfo, Globals), - globals.get_op_mode(Globals, OpMode), - ( if OpMode = opm_top_args(opma_augment(opmau_make_plain_opt), _) then - Believe = do_not_believe_check_termination - else - Believe = do_believe_check_termination - ). - %---------------------------------------------------------------------------% :- end_module termination.term_osi.term_osi_util. %---------------------------------------------------------------------------% diff --git a/compiler/term_util.m b/compiler/term_util.m new file mode 100644 index 000000000..ae9bacdc8 --- /dev/null +++ b/compiler/term_util.m @@ -0,0 +1,149 @@ +%---------------------------------------------------------------------------% +% vim: ft=mercury ts=4 sw=4 et +%---------------------------------------------------------------------------% +% Copyright (C) 1997-2007, 2010-2012 The University of Melbourne. +% Copyright (C) 2014-2019, 2021-2023, 2025-2026 The Mercury team. +% This file may only be copied under the terms of the GNU General +% Public License - see the file COPYING in the Mercury distribution. +%---------------------------------------------------------------------------% +% +% File: term_util.m. +% Main author: crs. +% +% This module defines some types and utility predicates that are either +% - actually used by both our termination analysers, or +% - could potentially be used by both our termination analysers. +% +%---------------------------------------------------------------------------% + +:- module termination.term_util. +:- interface. + +:- import_module hlds. +:- import_module hlds.hlds_module. +:- import_module hlds.hlds_pred. +:- import_module hlds.hlds_proc. +:- import_module hlds.pred_proc_id. +:- import_module parse_tree. +:- import_module parse_tree.prog_data. +:- import_module parse_tree.prog_data_foreign. + +%---------------------------------------------------------------------------% + +:- pred get_context_from_scc(module_info::in, scc::in, prog_context::out) + is det. + +%---------------------------------------------------------------------------% + + % Succeeds if the foreign proc attributes imply that a procedure is + % terminating. + % +:- pred attributes_imply_termination(foreign_proc_attributes::in) + is semidet. + +%---------------------------------------------------------------------------% + +:- type maybe_believe_check_termination + ---> do_not_believe_check_termination + ; do_believe_check_termination. + + % When we process imported predicates, should we believe that + % the presence of a 'check_termination' pragma, or rather the pred marker + % indicating the presence of such a pragma, guarantees that (in the absence + % of an error from that pragma) the predicate will actually terminate? + % + % The check_termination pragma will be checked by the compiler + % when it compiles the source file that the predicate was imported from. + % However, when we make .opt files, we do not check whether predicates + % with check_termination pragmas actually terminate, so we cannot assume + % that they do, since any violations of that assumption will *not* be + % reported. + % +:- pred should_we_believe_check_termination_markers(module_info::in, + maybe_believe_check_termination::out) is det. + +%---------------------------------------------------------------------------% + + % Succeed if all arguments of the given procedure of the given predicate + % are either input or zero size. + % +:- pred all_args_input_or_zero_size(module_info::in, pred_info::in, + proc_info::in) is semidet. + +%---------------------------------------------------------------------------% +%---------------------------------------------------------------------------% + +:- implementation. + +:- import_module hlds.mode_test. +:- import_module libs. +:- import_module libs.globals. +:- import_module libs.op_mode. +:- import_module termination.term_norm. + +:- import_module list. +:- import_module require. +:- import_module set. + +%---------------------------------------------------------------------------% +%---------------------------------------------------------------------------% + +get_context_from_scc(ModuleInfo, SCC, Context) :- + set.to_sorted_list(SCC, SCCProcs), + ( + SCCProcs = [proc(PredId, _) | _], + module_info_pred_info(ModuleInfo, PredId, PredInfo), + pred_info_get_context(PredInfo, Context) + ; + SCCProcs = [], + unexpected($pred, "empty SCC") + ). + +%---------------------------------------------------------------------------% + +attributes_imply_termination(Attributes) :- + ( + get_terminates(Attributes) = proc_terminates + ; + get_terminates(Attributes) = depends_on_mercury_calls, + get_may_call_mercury(Attributes) = proc_will_not_call_mercury + ). + +%---------------------------------------------------------------------------% + +should_we_believe_check_termination_markers(ModuleInfo, Believe) :- + module_info_get_globals(ModuleInfo, Globals), + globals.get_op_mode(Globals, OpMode), + ( if OpMode = opm_top_args(opma_augment(opmau_make_plain_opt), _) then + Believe = do_not_believe_check_termination + else + Believe = do_believe_check_termination + ). + +%---------------------------------------------------------------------------% + +all_args_input_or_zero_size(ModuleInfo, PredInfo, ProcInfo) :- + pred_info_get_arg_types(PredInfo, TypeList), + proc_info_get_argmodes(ProcInfo, ModeList), + all_args_input_or_zero_size_2(TypeList, ModeList, ModuleInfo). + +:- pred all_args_input_or_zero_size_2(list(mer_type)::in, list(mer_mode)::in, + module_info::in) is semidet. + +all_args_input_or_zero_size_2([], [], _). +all_args_input_or_zero_size_2([], [_|_], _) :- + unexpected($pred, "unmatched lists"). +all_args_input_or_zero_size_2([_|_], [], _) :- + unexpected($pred, "unmatched lists"). +all_args_input_or_zero_size_2([Type | Types], [Mode | Modes], ModuleInfo) :- + ( if mode_is_input(ModuleInfo, Mode) then + % The variable is an input variables, so its size is irrelevant. + all_args_input_or_zero_size_2(Types, Modes, ModuleInfo) + else + term_norm.zero_size_type(ModuleInfo, Type), + all_args_input_or_zero_size_2(Types, Modes, ModuleInfo) + ). + +%---------------------------------------------------------------------------% +:- end_module termination.term_util. +%---------------------------------------------------------------------------% diff --git a/compiler/termination.m b/compiler/termination.m index 3555cf623..503d7b848 100644 --- a/compiler/termination.m +++ b/compiler/termination.m @@ -8,9 +8,9 @@ % % This package contains our two termination analysis systems. % -% At the moment, they are wholly separate, but they do contain -% some very similar code. If these are ever factored out, this package -% is the natural home of the results. +% The two systems' code bases are *almost* wholly separate, but +% they do contain some shared code. This package is the natural home +% for that shared code. % %-----------------------------------------------------------------------------% @@ -25,6 +25,7 @@ :- implementation. :- include_module term_post_analysis. +:- include_module term_util. %-----------------------------------------------------------------------------% :- end_module termination.