mercury/compiler/term_errors.m

%-----------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%-----------------------------------------------------------------------------%
% Copyright (C) 1997-2000, 2003-2006, 2010-2011 The University of Melbourne.
% Copyright (C) 2014-2022, 2024-2025 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_errors.m.
% Main author: crs.
%
% This module prints out the various error messages that are produced by the
% various modules of termination analysis.
%
%-----------------------------------------------------------------------------%

:- module transform_hlds.term_errors.
:- interface.

:- import_module hlds.
:- import_module hlds.hlds_module.
:- import_module hlds.hlds_pred.
:- import_module parse_tree.
:- import_module parse_tree.error_spec.
:- import_module parse_tree.prog_data.

:- import_module assoc_list.
:- import_module bag.
:- import_module bool.
:- import_module list.

%-----------------------------------------------------------------------------%

:- type term_error_kind
    --->    pragma_foreign_code
            % The analysis result depends on the change constant of a piece
            % of pragma foreign code, (which cannot be obtained without
            % analyzing the foreign code, which is something we cannot do).
            % Valid in both passes.

    ;       imported_pred
            % The SCC contains some imported procedures,
            % whose code is not accessible.

    ;       can_loop_proc_called(pred_proc_id, pred_proc_id)
            % can_loop_proc_called(Caller, Callee)
            % The call from Caller to Callee at the associated context
            % is to a procedure (Callee) whose termination info is
            % set to can_loop.
            % Although this error does not prevent us from producing
            % argument size information, it would prevent us from proving
            % termination.
            % We look for this error in pass 1; if we find it,
            % we do not perform pass 2.

    ;       horder_args(pred_proc_id, pred_proc_id)
            % horder_args(Caller, Callee, Context)
            % The call from Caller to Callee at the associated context
            % has some arguments of a higher order type.
            % Valid in both passes.

    ;       horder_call
            % horder_call
            % There is a higher order call at the associated context.
            % Valid in both passes.

    ;       method_call
            % method_call
            % There is a call to a typeclass method at the associated context.
            % Valid in both passes.

    ;       inf_termination_const(pred_proc_id, pred_proc_id)
            % inf_termination_const(Caller, Callee)
            % The call from Caller to Callee at the associated context is
            % to a procedure (Callee) whose arg size info is set to infinite.
            % Valid in both passes.

    ;       ho_inf_termination_const(pred_proc_id, list(pred_proc_id))
            % ho_inf_termination_const(Caller, Callees).
            % Caller makes a call to either call/N or apply/N at the
            % associated context. 'Callees' gives the possible values
            % of the higher-order argument.

    ;       not_subset(pred_proc_id, bag(prog_var), bag(prog_var))
            % not_subset(Proc, SupplierVariables, InHeadVariables)
            % This error occurs when the bag of active variables
            % is not a subset of the input head variables.
            % Valid error only in pass 1.

    ;       inf_call(pred_proc_id, pred_proc_id)
            % inf_call(Caller, Callee)
            % The call from Caller to Callee at the associated context
            % has infinite weight.
            % Valid error only in pass 2.

    ;       cycle(pred_proc_id, assoc_list(pred_proc_id, prog_context))
            % cycle(StartPPId, CallSites)
            % In the cycle of calls starting at StartPPId and going through
            % the named call sites may be an infinite loop.
            % Valid error only in pass 2.

    ;       no_eqns
            % There are no equations in this SCC.
            % This has 2 possible causes. (1) If the predicate has
            % no output arguments, no equations will be created
            % for them. The change constant of the predicate is
            % undefined, but it will also never be used.
            % (2) If the procedure is a builtin predicate, with
            % an empty body, traversal cannot create any equations.
            % Valid error only in pass 1.

    ;       too_many_paths
            % There are too many distinct paths to be analyzed.
            % Valid in both passes (which analyze different sets of paths).

    ;       solver_failed
            % The solver could not find finite termination constants
            % for the procedures in the SCC.
            % Valid only in pass 1.

    ;       is_builtin(pred_id)
            % The termination constant of the given builtin is set to
            % infinity; this happens when the type of at least one
            % output argument permits a norm greater than zero.

    ;       does_not_term_pragma(pred_id)
            % The given procedure has a does_not_terminate pragma.

    ;       inconsistent_annotations
            % The pragma terminates/does_not_terminate declarations
            % for the procedures in this SCC are inconsistent.

    ;       does_not_term_foreign(pred_proc_id).
            % The procedure contains foreign code that may make calls
            % back to Mercury. By default, we assume such code to be
            % non-terminating.

:- type term_error
    --->    term_error(prog_context, term_error_kind).

:- pred report_term_errors(module_info::in, scc::in, list(term_error)::in,
    list(error_spec)::in, list(error_spec)::out) is det.

    % An error is considered an indirect error if it is due either to a
    % language feature we cannot analyze or due to an error in another part
    % of the code. By default, we do not issue warnings about indirect errors,
    % since in the first case, the programmer cannot do anything about it,
    % and in the second case, the piece of code that the programmer *can* do
    % something about is not this piece.
    %
:- func term_error_kind_is_direct_error(term_error_kind) = bool.

    % A fatal error is one that prevents pass 2 from proving termination.
    %
:- func term_error_kind_is_fatal_error(term_error_kind) = bool.

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

:- implementation.

:- import_module hlds.hlds_error_util.
:- import_module libs.
:- import_module libs.options.
:- import_module parse_tree.prog_data_pragma.
:- import_module parse_tree.var_table.
:- import_module transform_hlds.term_util.

:- import_module cord.
:- import_module int.
:- import_module maybe.
:- import_module pair.
:- import_module require.
:- import_module set.
:- import_module string.
:- import_module term.

%-----------------------------------------------------------------------------%

report_term_errors(ModuleInfo, SCC, Errors, !Specs) :-
    get_context_from_scc(ModuleInfo, SCC, Context),
    ( if set.is_singleton(SCC, PPId) then
        Pieces1 = [words("Termination of")] ++
            describe_qual_proc_name(ModuleInfo, PPId),
        Single = yes(PPId)
    else
        Pieces1 = [words("Termination of the "),
            words("mutually recursive procedures")] ++
            describe_several_proc_names(ModuleInfo, no,
                should_module_qualify, set.to_sorted_list(SCC)),
        Single = no
    ),
    (
        Errors = [],
        % XXX This should never happen but for some reason, it often does.
        % error("empty list of errors")
        Pieces2 = [words("not proven, for unknown reason(s).")],
        Pieces = Pieces1 ++ Pieces2,
        ReasonMsgsCord = cord.init
    ;
        Errors = [Error],
        Pieces2 = [words("not proven for the following reason:")],
        Pieces = Pieces1 ++ Pieces2,
        describe_term_error(ModuleInfo, Single, Error, no,
            cord.init, ReasonMsgsCord, !Specs)
    ;
        Errors = [_, _ | _],
        Pieces2 = [words("not proven for the following reasons:")],
        Pieces = Pieces1 ++ Pieces2,
        describe_term_errors(ModuleInfo, Single, Errors, 1,
            cord.init, ReasonMsgsCord, !Specs)
    ),
    ReasonMsgs = cord.list(ReasonMsgsCord),
    Msgs = [msg(Context, Pieces) | ReasonMsgs],
    Severity = severity_warning(warn_requested_by_option),
    Spec = error_spec($pred, Severity, phase_termination_analysis, Msgs),
    !:Specs = [Spec | !.Specs].

:- pred report_arg_size_errors(module_info::in, scc::in, list(term_error)::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_arg_size_errors(ModuleInfo, SCC, Errors, !Specs) :-
    get_context_from_scc(ModuleInfo, SCC, Context),
    ( if set.is_singleton(SCC, PPId) then
        Pieces1 = [words("Termination constant of")] ++
            describe_qual_proc_name(ModuleInfo, PPId),
        Single = yes(PPId)
    else
        Pieces1 = [words("Termination constants"),
            words("of the mutually recursive procedures")] ++
            describe_several_proc_names(ModuleInfo, no,
                should_module_qualify, set.to_sorted_list(SCC)),
        Single = no
    ),
    Piece2 = words("set to infinity for the following"),
    (
        Errors = [],
        unexpected($pred, "empty list of errors")
    ;
        Errors = [Error],
        Piece3 = words("reason:"),
        Pieces = Pieces1 ++ [Piece2, Piece3],
        describe_term_error(ModuleInfo, Single, Error, no,
            cord.init, ReasonMsgsCord, !Specs)
    ;
        Errors = [_, _ | _],
        Piece3 = words("reasons:"),
        Pieces = Pieces1 ++ [Piece2, Piece3],
        describe_term_errors(ModuleInfo, Single, Errors, 1,
            cord.init, ReasonMsgsCord, !Specs)
    ),
    ReasonMsgs = cord.list(ReasonMsgsCord),
    Msgs = [msg(Context, Pieces) | ReasonMsgs],
    Severity = severity_warning(warn_requested_by_option),
    Spec = error_spec($pred, Severity, phase_termination_analysis, Msgs),
    !:Specs = [Spec | !.Specs].

:- pred describe_term_errors(module_info::in, maybe(pred_proc_id)::in,
    list(term_error)::in, int::in, cord(error_msg)::in, cord(error_msg)::out,
    list(error_spec)::in, list(error_spec)::out) is det.

describe_term_errors(_, _, [], _, !Msgs, !Specs).
describe_term_errors(ModuleInfo, Single, [Error | Errors], ErrNum0,
        !Msgs, !Specs) :-
    describe_term_error(ModuleInfo, Single, Error, yes(ErrNum0),
        !Msgs, !Specs),
    describe_term_errors(ModuleInfo, Single, Errors, ErrNum0 + 1,
        !Msgs, !Specs).

:- pred describe_term_error(module_info::in, maybe(pred_proc_id)::in,
    term_error::in, maybe(int)::in, cord(error_msg)::in, cord(error_msg)::out,
    list(error_spec)::in, list(error_spec)::out) is det.

describe_term_error(ModuleInfo, Single, TermErrorContext, ErrorNum,
        !ReasonMsgs, !Specs) :-
    TermErrorContext = term_error(Context, ErrorKind),
    term_error_kind_description(ModuleInfo, Single, ErrorKind, Pieces0,
        Reason),
    (
        ErrorNum = yes(N),
        string.int_to_string(N, Nstr),
        Preamble = "Reason " ++ Nstr ++ ":",
        Pieces = [fixed(Preamble) | Pieces0]
    ;
        ErrorNum = no,
        Pieces = Pieces0
    ),
    ReasonMsg = error_msg(yes(Context), always_treat_as_first, 0u,
        [always(Pieces)]),
    !:ReasonMsgs = cord.snoc(!.ReasonMsgs, ReasonMsg),
    (
        Reason = yes(InfArgSizePPId),
        lookup_proc_arg_size_info(ModuleInfo, InfArgSizePPId, ArgSize),
        ( if ArgSize = yes(infinite(ArgSizeErrors)) then
            % XXX Should we add a Msg about the relevance of the spec
            % added by the folliwng call?
            % XXX the next line is cheating
            ArgSizePPIdSCC = set.make_singleton_set(InfArgSizePPId),
            report_arg_size_errors(ModuleInfo, ArgSizePPIdSCC, ArgSizeErrors,
                !Specs)
        else
            unexpected($pred,
                "inf arg size procedure does not have inf arg size")
        )
    ;
        Reason = no
    ).

:- pred term_error_kind_description(module_info::in, maybe(pred_proc_id)::in,
    term_error_kind::in, list(format_piece)::out,
    maybe(pred_proc_id)::out) is det.

term_error_kind_description(ModuleInfo, Single, ErrorKind, Pieces, Reason) :-
    (
        ErrorKind = horder_call,
        Pieces = [words("It contains a higher order call."), nl],
        Reason = no
    ;
        ErrorKind = method_call,
        Pieces = [words("It contains a typeclass method call."), nl],
        Reason = no
    ;
        ErrorKind = pragma_foreign_code,
        Pieces = [words("It depends on the properties of"),
            words("foreign language code included via a"),
            pragma_decl("foreign_proc"), words("declaration."), nl],
        Reason = no
    ;
        ErrorKind = inf_call(CallerPPId, CalleePPId),
        (
            Single = yes(PPId),
            expect(unify(PPId, CallerPPId), $pred,
                "inf_call: caller outside this SCC"),
            Pieces1 = [words("It")]
        ;
            Single = no,
            Pieces1 = describe_qual_proc_name(ModuleInfo, CallerPPId)
        ),
        Piece2 = words("calls"),
        CalleePieces = describe_qual_proc_name(ModuleInfo, CalleePPId),
        Pieces3 = [words("with an unbounded increase"),
            words("in the size of the input arguments."), nl],
        Pieces = Pieces1 ++ [Piece2] ++ CalleePieces ++ Pieces3,
        Reason = no
    ;
        ErrorKind = can_loop_proc_called(CallerPPId, CalleePPId),
        (
            Single = yes(PPId),
            expect(unify(PPId, CallerPPId), $pred,
                "can_loop_proc_called: caller outside this SCC"),
            Pieces1 = [words("It")]
        ;
            Single = no,
            Pieces1 = describe_qual_proc_name(ModuleInfo, CallerPPId)
        ),
        Piece2 = words("calls"),
        CalleePieces = describe_qual_proc_name(ModuleInfo, CalleePPId),
        Piece3 = words("which could not be proven to terminate."),
        Pieces = Pieces1 ++ [Piece2] ++ CalleePieces ++ [Piece3, nl],
        Reason = no
    ;
        ErrorKind = imported_pred,
        Pieces = [words("It contains one or more"),
            words("predicates and/or functions"),
            words("imported from another module."), nl],
        Reason = no
    ;
        ErrorKind = horder_args(CallerPPId, CalleePPId),
        (
            Single = yes(PPId),
            expect(unify(PPId, CallerPPId), $pred,
                "horder_args: caller outside this SCC"),
            Pieces1 = [words("It")]
        ;
            Single = no,
            Pieces1 = describe_qual_proc_name(ModuleInfo, CallerPPId)
        ),
        Piece2 = words("calls"),
        CalleePieces = describe_qual_proc_name(ModuleInfo, CalleePPId),
        Piece3 = words("with one or more higher order arguments."),
        Pieces = Pieces1 ++ [Piece2] ++ CalleePieces ++ [Piece3, nl],
        Reason = no
    ;
        ErrorKind = inf_termination_const(CallerPPId, CalleePPId),
        (
            Single = yes(PPId),
            expect(unify(PPId, CallerPPId), $pred,
                "inf_termination_const: caller outside this SCC"),
            Pieces1 = [words("It")]
        ;
            Single = no,
            Pieces1 = describe_qual_proc_name(ModuleInfo, CallerPPId)
        ),
        Piece2 = words("calls"),
        CalleePieces = describe_qual_proc_name(ModuleInfo, CalleePPId),
        Piece3 = words("which has a termination constant of infinity."),
        Pieces = Pieces1 ++ [Piece2] ++ CalleePieces ++ [Piece3, nl],
        Reason = yes(CalleePPId)
    ;
        ErrorKind = ho_inf_termination_const(CallerPPId, _ClosurePPIds),
        % XXX We should print out the names of the non-terminating closures.
        (
            Single = yes(PPId),
            expect(unify(PPId, CallerPPId), $pred,
                "ho_info_termination_const: caller outside this SCC"),
            Pieces1 = [words("It")]
        ;
            Single = no,
            Pieces1 = describe_qual_proc_name(ModuleInfo, CallerPPId)
        ),
        Pieces2 = [words("makes one or more higher-order calls."),
            words("Each of these higher-order calls has a"),
            words("termination constant of infinity."), nl],
        Pieces = Pieces1 ++ Pieces2,
        Reason = no
    ;
        ErrorKind = not_subset(ProcPPId, OutputSuppliers, HeadVars),
        (
            Single = yes(PPId),
            ( if PPId = ProcPPId then
                Pieces1 = [words("The set of its output supplier variables")]
            else
                % XXX this should never happen (but it does)
                % error("not_subset outside this SCC"),
                PPIdPieces = describe_qual_proc_name(ModuleInfo, ProcPPId),
                Pieces1 = [words("The set of output supplier variables of")
                    | PPIdPieces]
            )
        ;
            Single = no,
            PPIdPieces = describe_qual_proc_name(ModuleInfo, ProcPPId),
            Pieces1 = [words("The set of output supplier variables of") |
                PPIdPieces]
        ),
        ProcPPId = proc(PredId, ProcId),
        module_info_pred_proc_info(ModuleInfo, PredId, ProcId, _, ProcInfo),
        proc_info_get_var_table(ProcInfo, VarTable),
        term_errors_var_bag_description(VarTable, OutputSuppliers,
            OutputSuppliersNames),
        list.map((pred(OS::in, FOS::out) is det :- FOS = fixed(OS)),
            OutputSuppliersNames, OutputSuppliersPieces),
        Pieces3 = [words("is not a subset of the head variables")],
        term_errors_var_bag_description(VarTable, HeadVars, HeadVarsNames),
        list.map((pred(HV::in, FHV::out) is det :- FHV = fixed(HV)),
            HeadVarsNames, HeadVarsPieces),
        Pieces = Pieces1 ++ OutputSuppliersPieces ++ Pieces3 ++
            HeadVarsPieces ++ [suffix("."), nl],
        Reason = no
    ;
        ErrorKind = cycle(_StartPPId, CallSites),
        ( if CallSites = [DirectCall] then
            SitePieces = describe_one_call_site(ModuleInfo, no,
                should_module_qualify, DirectCall),
            Pieces = [words("At the recursive call to") | SitePieces] ++
                [words("the arguments are not guaranteed"),
                words("to decrease in size."), nl]
        else
            Pieces = [words("In the recursive cycle through the calls to")] ++
                describe_several_call_sites(ModuleInfo, no,
                    should_module_qualify, CallSites) ++
                [words("the arguments are"),
                    words("not guaranteed to decrease in size."), nl]
        ),
        Reason = no
    ;
        ErrorKind = too_many_paths,
        Pieces = [words("There are too many execution paths"),
            words("for the analysis to process."), nl],
        Reason = no
    ;
        ErrorKind = no_eqns,
        Pieces = [words("The analysis was unable to form any constraints"),
            words("between the arguments of this group of procedures."), nl],
        Reason = no
    ;
        ErrorKind = solver_failed,
        Pieces = [words("The solver found the constraints produced"),
            words("by the analysis to be infeasible."), nl],
        Reason = no
    ;
        ErrorKind = is_builtin(_PredId),
        % XXX expect(unify(Single, yes(_)), $pred,
        %       "builtin not alone in SCC"),
        Pieces = [words("It is a builtin predicate."), nl],
        Reason = no
    ;
        ErrorKind = does_not_term_pragma(PredId),
        Pieces1 = [words("There is a"), pragma_decl("does_not_terminate"),
            words("declaration for")],
        (
            Single = yes(PPId),
            PPId = proc(SCCPredId, _),
            expect(unify(PredId, SCCPredId), $pred,
                "does not terminate pragma outside this SCC"),
            Pieces2 = [words("it."), nl]
        ;
            Single = no,
            Pieces2 = describe_qual_pred_name(ModuleInfo, PredId) ++
                [suffix("."), nl]
        ),
        Pieces = Pieces1 ++ Pieces2,
        Reason = no
    ;
        ErrorKind = inconsistent_annotations,
        Pieces = [words("The termination pragmas are inconsistent."), nl],
        Reason = no
    ;
        ErrorKind = does_not_term_foreign(_),
        Pieces = [words("It contains foreign code that"),
            words("may make one or more calls back to Mercury."), nl],
        Reason = no
    ).

%----------------------------------------------------------------------------%

:- pred term_errors_var_bag_description(var_table::in, bag(prog_var)::in,
    list(string)::out) is det.

term_errors_var_bag_description(VarTable, HeadVars, Pieces) :-
    bag.to_assoc_list(HeadVars, HeadVarsCounts),
    (
        HeadVarsCounts = [],
        Pieces = ["{}"]
    ;
        HeadVarsCounts = [FirstVarCount | LaterVarsCounts],
        term_errors_var_bag_desc_loop(VarTable, "{",
            FirstVarCount, LaterVarsCounts, Pieces)
    ).

:- pred term_errors_var_bag_desc_loop(var_table::in, string::in,
    pair(prog_var, int)::in, assoc_list(prog_var, int)::in,
    list(string)::out) is det.

term_errors_var_bag_desc_loop(VarTable, Prefix,
        Var - Count, VarsCounts, [Piece | Pieces]) :-
    VarName = var_table_entry_name(VarTable, Var),
    ( if Count > 1 then
        string.format("%s%s*%d", [s(Prefix), s(VarName), i(Count)], Piece0)
    else
        string.format("%s%s", [s(Prefix), s(VarName)], Piece0)
    ),
    (
        VarsCounts = [],
        Piece = Piece0 ++ "}.",
        Pieces = []
    ;
        VarsCounts = [HeadVarCount | TailVarsCounts],
        Piece = Piece0,
        term_errors_var_bag_desc_loop(VarTable, "",
            HeadVarCount, TailVarsCounts, Pieces)
    ).

%-----------------------------------------------------------------------------%

% XXX Some of the following (and in is_fatal_error/1 as well) look wrong.
% Some of them should probably be calling unexpected/2 - juliensf.

term_error_kind_is_direct_error(ErrorKind) = IsDirect :-
    (
        ( ErrorKind = horder_call
        ; ErrorKind = method_call
        ; ErrorKind = pragma_foreign_code
        ; ErrorKind = imported_pred
        ; ErrorKind = can_loop_proc_called(_, _)
        ; ErrorKind = horder_args(_, _)
        ; ErrorKind = does_not_term_pragma(_)
        ),
        IsDirect = no
    ;
        ( ErrorKind = cycle(_, _)
        ; ErrorKind = does_not_term_foreign(_)
        ; ErrorKind = ho_inf_termination_const(_, _)
        ; ErrorKind = inf_call(_, _)
        ; ErrorKind = inf_termination_const(_, _)
        ; ErrorKind = is_builtin(_)
        ; ErrorKind = no_eqns
        ; ErrorKind = not_subset(_, _, _)
        ; ErrorKind = solver_failed
        ; ErrorKind = too_many_paths
        ; ErrorKind = inconsistent_annotations
        ),
        IsDirect = yes
    ).

term_error_kind_is_fatal_error(ErrorKind) = IsFatal :-
    (
        ( ErrorKind = horder_call
        ; ErrorKind = horder_args(_, _)
        ; ErrorKind = imported_pred
        ; ErrorKind = method_call
        ),
        IsFatal = yes
    ;
        ( ErrorKind = pragma_foreign_code
        ; ErrorKind = can_loop_proc_called(_, _)
        ; ErrorKind = does_not_term_pragma(_)
        ; ErrorKind = cycle(_, _)
        ; ErrorKind = does_not_term_foreign(_)
        ; ErrorKind = ho_inf_termination_const(_, _)
        ; ErrorKind = inf_call(_, _)
        ; ErrorKind = inf_termination_const(_, _)
        ; ErrorKind = is_builtin(_)
        ; ErrorKind = no_eqns
        ; ErrorKind = not_subset(_, _, _)
        ; ErrorKind = solver_failed
        ; ErrorKind = too_many_paths
        ; ErrorKind = inconsistent_annotations
        ),
        IsFatal = no
    ).

%----------------------------------------------------------------------------%
:- end_module transform_hlds.term_errors.
%----------------------------------------------------------------------------%