[m-rev.] for review: new termination analyser (part 5 of 6)
Julien Fischer
juliensf at cs.mu.OZ.AU
Thu Mar 24 15:46:45 AEDT 2005
+%-----------------------------------------------------------------------------%
Index: compiler/term_constr_errors.m
===================================================================
RCS file: compiler/term_constr_errors.m
diff -N compiler/term_constr_errors.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/term_constr_errors.m 9 Mar 2005 03:43:17 -0000
@@ -0,0 +1,282 @@
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%-----------------------------------------------------------------------------%
+% Copyright (C) 2002 The University of Melbourne.
+% This file may only be copied under the terms of the GNU General
+% Public License - see the file COPYING in the Mercury distribution.
+%-----------------------------------------------------------------------------%
+%
+% term_constr_errors.m
+% main author: juliensf.
+%
+%-----------------------------------------------------------------------------%
+
+:- module transform_hlds.term_constr_errors.
+
+:- interface.
+
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_pred.
+
+:- import_module parse_tree.prog_data.
+
+:- import_module io.
+:- import_module list.
+:- import_module std_util.
+
+%-----------------------------------------------------------------------------%
+%
+% Termination 2 Errors
+%
+
+% The termination errors are all in reference to possible non-termination.
+% While it is possible for pass 1 to go amiss the worst that will happen
+% (barring an abnormal abort) is that the size of the arguments will be
+% unconstrained.
+
+:- type termination2_error
+ ---> imported_pred
+ % Termination could not be proved because
+ % it depends upon information from another
+ % module and that information is not
+ % available.
+
+ ; can_loop_proc_called(pred_proc_id, pred_proc_id)
+ % Termination could not be proved because
+ % the procedure called another procedure
+ % that may not terminate.
+
+ ; cond_not_satisfied
+ % Termination could not be proved because
+ % no set of decreasing argument could e found.
+
+ ; horder_call
+ % Termination could not be proved because
+ % the procedure makes higher-order calls.
+
+ ; does_not_term_pragma(pred_id)
+ % Termination could not be proved because
+ % the procedure was marked with a
+ % `does_not_terminate' pragma.
+
+ ; foreign_proc_called(pred_proc_id).
+ % Termination depends upon the properties
+ % of a piece of foreign code that cannot
+ % be established as terminating.
+
+:- type term_constr_errors.error == pair(prog_context, termination2_error).
+
+:- type term2_errors == list(term_constr_errors.error).
+
+%-----------------------------------------------------------------------------%
+
+:- pred report_termination2_errors(list(pred_proc_id)::in, term2_errors::in,
+ module_info::in, module_info::out, io::di, io::uo) is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module libs.globals.
+:- import_module libs.options.
+
+:- import_module parse_tree.error_util.
+:- import_module hlds.hlds_error_util.
+
+:- import_module transform_hlds.term_util.
+
+:- import_module bool.
+:- import_module int.
+:- import_module require.
+:- import_module string.
+
+%-----------------------------------------------------------------------------%
+
+report_termination2_errors(SCC, Errors, !Module, !IO) :-
+ globals.io_lookup_bool_option(check_termination2, NormalErrors, !IO),
+ globals.io_lookup_bool_option(verbose_check_termination2,
+ VerboseErrors, !IO),
+ (
+ IsCheckTerm = (pred(PPId::in) is semidet :-
+ module_info_pred_proc_info(!.Module, PPId, PredInfo, _),
+ not pred_info_is_imported(PredInfo),
+ pred_info_get_markers(PredInfo, Markers),
+ check_marker(Markers, check_termination)
+ ),
+ CheckTermPPIds = list.filter(IsCheckTerm, SCC),
+ list.is_not_empty(CheckTermPPIds)
+ ->
+ report_term_errors(SCC, Errors, !.Module, !IO),
+ io.set_exit_status(1, !IO),
+ module_info_incr_errors(!Module)
+ ;
+ IsNonImported = (pred(PPId::in) is semidet :-
+ module_info_pred_proc_info(!.Module, PPId, PredInfo, _),
+ not pred_info_is_imported(PredInfo)
+ ),
+ NonImportedPPIds = list.filter(IsNonImported, SCC),
+ list.is_not_empty(NonImportedPPIds),
+ ( VerboseErrors = yes ->
+ PrintErrors = Errors
+ ; NormalErrors = yes ->
+ IsNonSimple = (pred(ContextError::in) is semidet :-
+ ContextError = _ - Error,
+ not indirect_error(Error)
+ ),
+ PrintErrors0 = list.filter(IsNonSimple, Errors),
+ %
+ % If there are no direct errors report
+ % the indirect ones instead.
+ %
+ ( if PrintErrors0 = []
+ then PrintErrors = Errors
+ else PrintErrors = PrintErrors0
+ )
+ ;
+ fail
+ )
+ ->
+ term_constr_errors.report_term_errors(SCC, PrintErrors,
+ !.Module, !IO)
+ ;
+ true
+ ).
+
+%-----------------------------------------------------------------------------%
+
+:- pred report_term_errors(list(pred_proc_id)::in, term2_errors::in,
+ module_info::in, io::di, io::uo) is det.
+
+report_term_errors(SCC, Errors, Module, !IO) :-
+ get_context_from_scc(SCC, Module, Context),
+ ( SCC = [PPId] ->
+ Pieces0 = [words("Termination of")],
+ ProcName = describe_one_proc_name(Module, should_module_qualify,
+ PPId),
+ Pieces1 = Pieces0 ++ ProcName,
+ Single = yes(PPId)
+ ;
+ Pieces0 = [
+ words("Termination of the mutually"),
+ words("recursive procedures")
+ ],
+ ProcNames = describe_several_proc_names(Module,
+ should_module_qualify, SCC),
+ Pieces1 = Pieces0 ++ ProcNames,
+ Single = no
+ ),
+ (
+ Errors = [],
+ Pieces2 = [words("not proven, for unknown reason(s).")],
+ write_error_pieces(Context, 0, Pieces1 ++ Pieces2, !IO)
+ ;
+ Errors = [Error],
+ Pieces2 = [words("not proven for the following reason:")],
+ write_error_pieces(Context, 0, Pieces1 ++ Pieces2, !IO),
+ output_error(Error, Single, no, 0, Module, !IO)
+ ;
+ Errors = [_, _ | _],
+ Pieces2 = [words("not proven for the following reasons:")],
+ write_error_pieces(Context, 0, Pieces1 ++ Pieces2, !IO),
+ output_errors(Errors, Single, 1, 0, Module, !IO)
+ ).
+
+:- pred output_errors(term2_errors::in,
+ maybe(pred_proc_id)::in, int::in, int::in, module_info::in,
+ io::di, io::uo) is det.
+
+output_errors([], _, _, _, _, !IO).
+output_errors([Error | Errors], Single, ErrNum0, Indent, Module, !IO) :-
+ output_error(Error, Single, yes(ErrNum0), Indent, Module, !IO),
+ output_errors(Errors, Single, ErrNum0 + 1, Indent, Module, !IO).
+
+:- pred output_error(term_constr_errors.error::in, maybe(pred_proc_id)::in,
+ maybe(int)::in, int::in, module_info::in, io::di, io::uo) is det.
+
+output_error(Context - Error, Single, ErrorNum, Indent, Module, !IO) :-
+ description(Error, Single, Module, Pieces0, _),
+ ( ErrorNum = yes(N) ->
+ string.int_to_string(N, Nstr),
+ string.append_list(["Reason ", Nstr, ":"], Preamble),
+ Pieces = [fixed(Preamble) | Pieces0]
+ ;
+ Pieces = Pieces0
+ ),
+ write_error_pieces(Context, Indent, Pieces, !IO).
+
+:- pred description(termination2_error::in,
+ maybe(pred_proc_id)::in, module_info::in, list(format_component)::out,
+ maybe(pred_proc_id)::out) is det.
+
+description(cond_not_satisfied, _, _, Pieces, no) :-
+ Pieces = [
+ words("The termination condition"),
+ words("is not satisfiable.")
+ ].
+
+description(imported_pred, _, _, Pieces, no) :-
+ Pieces = [
+ words("It contains one or more"),
+ words("predicates and/or functions"),
+ words("imported from another module.")
+ ].
+
+description(can_loop_proc_called(CallerPPId, CalleePPId),
+ Single, Module, Pieces, no) :-
+ (
+ Single = yes(PPId),
+ require(unify(PPId, CallerPPId), "caller outside this SCC"),
+ Piece1 = [words("It")]
+ ;
+ Single = no,
+ ProcName = describe_one_proc_name(Module, should_module_qualify,
+ CallerPPId),
+ Piece1 = ProcName
+ ),
+ Piece2 = words("calls"),
+ CalleePiece = describe_one_proc_name(Module, should_module_qualify,
+ CalleePPId),
+ Pieces3 = [words("which could not be proven to terminate.")],
+ Pieces = Piece1 ++ [Piece2] ++ CalleePiece ++ Pieces3.
+
+description(horder_call, _, _, Pieces, no) :-
+ Pieces = [words("It contains a higher-order call.")].
+
+description(does_not_term_pragma(PredId), Single, Module, Pieces, no) :-
+ Pieces1 = [
+ words("There is a"),
+ fixed("`:- pragma does_not_terminate'"),
+ words("declaration for")
+ ],
+ (
+ Single = yes(PPId),
+ PPId = proc(SCCPredId, _),
+ require(unify(PredId, SCCPredId),
+ "does not terminate pragma outside this SCC"),
+ Piece2 = [words("it.")]
+ ;
+ Single = no,
+ Piece2Nodot = describe_one_pred_name(Module,
+ should_module_qualify, PredId),
+ Piece2 = Piece2Nodot ++ [words(".")]
+ ),
+ Pieces = Pieces1 ++ Piece2.
+
+description(foreign_proc_called(PPId), _Single, Module, Pieces, no) :-
+ Name = describe_one_proc_name(Module, should_module_qualify, PPId),
+ Pieces = [words("There is a call the foreign procedure")] ++
+ Name ++ [words("which is not known to terminate.")].
+
+%-----------------------------------------------------------------------------%
+
+:- pred indirect_error(termination2_error::in) is semidet.
+
+indirect_error(imported_pred).
+indirect_error(horder_call).
+indirect_error(does_not_term_pragma(_)).
+indirect_error(can_loop_proc_called(_, _)).
+
+%-----------------------------------------------------------------------------%
+:- end_module term_constr_errors.
+%-----------------------------------------------------------------------------%
Index: compiler/term_constr_fixpoint.m
===================================================================
RCS file: compiler/term_constr_fixpoint.m
diff -N compiler/term_constr_fixpoint.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/term_constr_fixpoint.m 24 Mar 2005 04:20:56 -0000
@@ -0,0 +1,484 @@
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%-----------------------------------------------------------------------------%
+% Copyright (C) 2002 The University of Melbourne.
+% 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_constr_fixpoint.m
+% main author: juliensf
+%
+% TODO:
+% * code for handling calls could do with a cleanup.
+%
+% NOTE: the code in this module should not refer to things in the HLDS
+% (with the exception of the termination2_info slots in the
+% proc_sub_info structure)
+%
+%-----------------------------------------------------------------------------%
+
+:- module transform_hlds.term_constr_fixpoint.
+
+:- interface.
+
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_pred.
+
+:- import_module transform_hlds.term_constr_data.
+:- import_module transform_hlds.term_constr_errors.
+
+:- import_module io.
+:- import_module list.
+
+%-----------------------------------------------------------------------------%
+
+ % Calculate the next approximation to the argument size constraints.
+ %
+ % ChangeFlag is `yes' if the constraints for any procedure in the SCC
+ % have changed since the previous iteration.
+ %
+:- pred do_fixpoint_calculation(fixpoint_options::in, list(pred_proc_id)::in,
+ int::in, term2_errors::out, module_info::in, module_info::out,
+ io::di, io::uo) is det.
+
+:- type fixpoint_options.
+
+:- func fixpoint_options_init(widening, int) = fixpoint_options.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module check_hlds.type_util.
+
+:- import_module libs.globals.
+:- import_module libs.lp_rational.
+:- import_module libs.options.
+:- import_module libs.polyhedron.
+
+:- import_module transform_hlds.term_constr_data.
+:- import_module transform_hlds.term_constr_util.
+:- import_module transform_hlds.termination2.
+
+:- import_module hlds.hlds_data.
+:- import_module hlds.hlds_goal.
+:- import_module hlds.hlds_out.
+
+:- import_module parse_tree.error_util.
+:- import_module parse_tree.prog_data.
+
+:- import_module assoc_list.
+:- import_module bool.
+:- import_module int.
+:- import_module map.
+:- import_module set.
+:- import_module std_util.
+:- import_module string.
+:- import_module term.
+:- import_module varset.
+
+%------------------------------------------------------------------------------%
+
+:- type fixpoint_options
+ ---> fixpoint_options(
+ widening :: widening,
+ max_size :: int
+ ).
+
+fixpoint_options_init(Widening, MaxMatrixSize) =
+ fixpoint_options(Widening, MaxMatrixSize).
+
+%------------------------------------------------------------------------------%
+%
+% Perform a fixpoint iteration on the AR.
+%
+
+ % The information for each procedure in the SCC returned by a single
+ % iteration of the fixpoint calculation.
+ %
+:- type iteration_info
+ ---> iteration_info(
+ pred_proc_id,
+ arg_size_poly :: polyhedron,
+ change_flag :: bool
+ ).
+
+:- type iteration_infos == list(iteration_info).
+
+do_fixpoint_calculation(Options, SCC, Iteration, [], !ModuleInfo, !IO) :-
+ AbstractSCC = get_abstract_scc(!.ModuleInfo, SCC),
+ %
+ % Carry out one iteration of fixpoint computation. We need to
+ % do this for all SCCs at least once in order to obtain the argument
+ % size constraints for non-recursive procedures. We could do that
+ % during the build phase for non-recursive procedures (and in fact used
+ % to) but the code ends up being a horrible mess.
+ %
+ list.foldl2(traverse_abstract_proc(Iteration, Options, !.ModuleInfo),
+ AbstractSCC, [], IterationInfos, !IO),
+ ChangeFlag = or_flags(IterationInfos),
+ (
+ ChangeFlag = yes
+ ->
+ list.foldl(update_size_info, IterationInfos, !ModuleInfo),
+ do_fixpoint_calculation(Options, SCC, Iteration + 1,
+ _, !ModuleInfo, !IO)
+ ;
+ % If one of the polyhedra in the SCC has `false' as its
+ % argument size constraint then the analysis failed. In that
+ % case set the argument size constraints for every procedure
+ % in the SCC to `true'.
+ % XXX Should this be happening?
+ %
+ (
+ list.member(OneInfo, IterationInfos),
+ polyhedron.is_empty(OneInfo ^ arg_size_poly)
+ ->
+ ChangePoly = (func(Info0) = Info :-
+ Identity = polyhedron.identity,
+ Info = Info0 ^ arg_size_poly := Identity
+ ),
+ list.foldl(update_size_info, list.map(ChangePoly, IterationInfos),
+ !ModuleInfo)
+ ;
+ list.foldl(update_size_info, IterationInfos, !ModuleInfo)
+ )
+ ).
+
+:- func or_flags(iteration_infos) = bool.
+
+or_flags([]) = no.
+or_flags([Info | Infos]) = bool.or(Info ^ change_flag, or_flags(Infos)).
+
+:- pred update_size_info(iteration_info::in, module_info::in, module_info::out)
+ is det.
+
+update_size_info(Info, !ModuleInfo) :-
+ Info = iteration_info(PPId, Poly, _),
+ update_arg_size_info(PPId, Poly, !ModuleInfo).
+
+%------------------------------------------------------------------------------%
+
+:- pred traverse_abstract_proc(int::in, fixpoint_options::in,
+ module_info::in, abstract_proc::in, iteration_infos::in,
+ iteration_infos::out, io::di, io::uo) is det.
+
+traverse_abstract_proc(Iteration, Options, ModuleInfo, Proc, !IterationInfo,
+ !IO) :-
+ WideningInfo = Options ^ widening,
+ MaxMatrixSize = Options ^ max_size,
+ AbstractPPId = Proc ^ ppid,
+ AbstractPPId = real(PPId),
+ Varset = Proc ^ varset,
+ Zeros = Proc ^ zeros,
+ HeadVars = Proc ^ head_vars,
+ %
+ % Print out the debugging traces.
+ %
+ maybe_write_trace(io.write(PPId), !IO),
+ maybe_write_trace(io.write_string(": "), !IO),
+ maybe_write_trace(hlds_out.write_pred_proc_id(ModuleInfo, PPId), !IO),
+ maybe_write_trace(io.write_string(" "), !IO),
+ maybe_write_trace(write_size_vars(Varset, HeadVars), !IO),
+ maybe_write_trace(io.format("\nIteration %d:\n", [i(Iteration)]), !IO),
+ %
+ % Begin by traversing the procedure and calculating the
+ % IR approximation for this iteration.
+ %
+ Info = init_fixpoint_info(ModuleInfo, Varset, PPId, MaxMatrixSize,
+ HeadVars, Zeros),
+
+ some [!Polyhedron] (
+ traverse_abstract_goal(Info, Proc ^ body, polyhedron.identity,
+ !:Polyhedron),
+ polyhedron.optimize(Varset, !Polyhedron),
+ %
+ % XXX Bug workaround - the build pass sometimes stuffs up
+ % the local variable set for if-then-elses.
+ % (See comments in term_constr_build.m).
+ %
+ BugConstrs0 = polyhedron.constraints(!.Polyhedron),
+ ConstrVarsSet = get_vars_from_constraints(BugConstrs0),
+ HeadVarSet = set.from_list(HeadVars),
+ BadVarsSet = set.difference(ConstrVarsSet, HeadVarSet),
+ BadVars = set.to_sorted_list(BadVarsSet),
+ !:Polyhedron = polyhedron.project(BadVars, Varset, !.Polyhedron),
+ polyhedron.optimize(Varset, !Polyhedron),
+ %
+ % XXX End of bug workaround.
+ % Print out the polyhedron obtained during this iteration.
+ %
+ maybe_write_trace(polyhedron.write_polyhedron(!.Polyhedron, Varset),
+ !IO),
+ maybe_write_trace(io.nl, !IO),
+ %
+ % Look up the constraints obtained during the previous
+ % iteration.
+ %
+ ArgSizeInfo = lookup_proc_constr_arg_size_info(ModuleInfo, PPId),
+ %
+ % NOTE: `!.Polyhedron' is the set of constraints obtained by
+ % *this* iteration. `OldPolyhedron' is the set of constraints
+ % obtained by the *previous* iteration -- which may in fact
+ % be `empty' (false).
+ %
+ (
+ % If there were no constraints for the procedure then
+ % we are at the beginning of the analysis.
+ %
+ ArgSizeInfo = no,
+ OldPolyhedron = polyhedron.empty
+ ;
+ ArgSizeInfo = yes(SizeInfo),
+ SizeInfo = OldPolyhedron
+ ),
+ ( polyhedron.is_empty(!.Polyhedron) ->
+ ( if polyhedron.is_empty(OldPolyhedron)
+ then ChangeFlag = no
+ else unexpected(this_file, "old polyhedron is empty.")
+ )
+ ;
+ % If the procedure is not recursive then we need only perform one
+ % pass over the AR - subsequent iterations will yield the same result.
+ %
+ ( if Proc ^ recursion = none then ChangeFlag = no
+ else if polyhedron.is_empty(OldPolyhedron) then ChangeFlag = yes
+ else test_fixpoint_and_perhaps_widen(WideningInfo, Varset,
+ Iteration, OldPolyhedron, !Polyhedron, ChangeFlag)
+ )
+ ),
+ ThisIterationInfo = iteration_info(PPId, !.Polyhedron, ChangeFlag)
+ ),
+ list.cons(ThisIterationInfo, !IterationInfo).
+
+%------------------------------------------------------------------------------%
+
+:- type fixpoint_info
+ ---> fixpoint_info(
+ module_info :: module_info,
+ varset :: size_varset,
+ ppid :: pred_proc_id,
+ max_matrix_size :: int,
+ curr_head_vars :: head_vars,
+ zeros :: zero_vars
+ ).
+
+:- func init_fixpoint_info(module_info, size_varset, pred_proc_id, int,
+ head_vars, zero_vars) = fixpoint_info.
+
+init_fixpoint_info(ModuleInfo, Varset, PPId, MaxMatrixSize, HeadVars, Zeros) =
+ fixpoint_info(ModuleInfo, Varset, PPId, MaxMatrixSize, HeadVars, Zeros).
+
+%------------------------------------------------------------------------------%
+
+:- pred traverse_abstract_goal(fixpoint_info::in, abstract_goal::in,
+ polyhedron::in, polyhedron::out) is det.
+
+traverse_abstract_goal(Info, disj(Goals, _Size, Locals, _), !Polyhedron) :-
+ %
+ % There are number of possible improvements that should be made here:
+ %
+ % - Take the intersection each disjunct with the constraints
+ % before the disjunction and compute the convex hull of that.
+ % This is more accurate but slower. (XXX There is some code for this
+ % in term_constr_data.m but it needs to be moved here). To do
+ % this you need to add the constraints that occur to
+ % left of the disjunctions to `PriorConstraints'.
+ %
+ % - Try computing the convex hull of large disjunctions
+ % pairwise rather than linearly. There is code to do this
+ % below but we currently don't use it.
+ %
+ PriorConstraints = polyhedron.identity,
+ traverse_abstract_disj_linearly(Goals, Locals, Info, PriorConstraints,
+ Polyhedron0),
+ post_process_abstract_goal(Locals, Info, Polyhedron0, !Polyhedron).
+
+traverse_abstract_goal(Info, conj(Goals, Locals, _), !Polyhedron) :-
+ list.foldl(traverse_abstract_goal(Info), Goals, polyhedron.identity,
+ Polyhedron0),
+ post_process_abstract_goal(Locals, Info, Polyhedron0, !Polyhedron).
+
+traverse_abstract_goal(Info, AbstractGoal, !Polyhedron) :-
+ AbstractGoal = call(CallPPId0, _, CallVars, CallZeros, Locals, _,
+ CallArgsPoly),
+ CallPPId0 = real(CallPPId),
+ module_info_pred_proc_info(Info ^ module_info, CallPPId, _,
+ CallProcInfo),
+ proc_info_get_termination2_info(CallProcInfo, CallTerm2Info),
+ CallArgSizeInfo = CallTerm2Info ^ success_constrs,
+ (
+ CallArgSizeInfo = no,
+ !:Polyhedron = polyhedron.empty
+ ;
+ CallArgSizeInfo = yes(SizeInfo),
+ ( polyhedron.is_empty(SizeInfo) ->
+ !:Polyhedron = polyhedron.empty
+ ;
+ ( not polyhedron.is_universe(SizeInfo) ->
+ HeadVars = CallTerm2Info ^ head_vars,
+ SubstMap = compose_bijections(CallVars,
+ HeadVars),
+ Polyhedron0 = polyhedron.substitute_vars(
+ SubstMap, SizeInfo),
+ Polyhedron1 = intersection(Polyhedron0,
+ CallArgsPoly),
+ %
+ % Set any zero_vars in the constraints
+ % to zero (ie. delete the terms). We need
+ % to do this when a polymorphic arguments
+ % are zero sized.
+ %
+ Polyhedron2 = polyhedron.zero_vars(CallZeros,
+ Polyhedron1),
+ post_process_abstract_goal(Locals, Info,
+ Polyhedron2, !Polyhedron)
+ ;
+ true % Constraint store += true
+ )
+ )
+ ).
+
+traverse_abstract_goal(Info, primitive(Poly, Locals, _), !Polyhedron) :-
+ post_process_abstract_goal(Locals, Info, Poly, !Polyhedron).
+
+%------------------------------------------------------------------------------%
+
+:- pred post_process_abstract_goal(size_vars::in, fixpoint_info::in,
+ polyhedron::in, polyhedron::in, polyhedron::out) is det.
+
+post_process_abstract_goal(Locals, Info, GoalPolyhedron0, !Polyhedron) :-
+ ( if polyhedron.is_empty(GoalPolyhedron0)
+ then GoalPolyhedron = polyhedron.empty
+ else GoalPolyhedron = polyhedron.project(Locals, Info ^ varset,
+ GoalPolyhedron0)
+ ),
+ polyhedron.intersection(GoalPolyhedron, !Polyhedron).
+
+%------------------------------------------------------------------------------%
+%
+% Predicates for handling disjunctions.
+%
+
+ % This version computes the convex hull linearly.
+ % That is, ( A ; B ; C ; D) is processed as:
+ %
+ % ((((identity \/ A ) \/ B ) \/ C ) \/ D)
+ %
+:- pred traverse_abstract_disj_linearly(abstract_goals::in,
+ size_vars::in, fixpoint_info::in, polyhedron::in, polyhedron::out)
+ is det.
+
+traverse_abstract_disj_linearly(Goals, Locals, Info, !Polyhedron) :-
+ list.foldl(traverse_abstract_disjunct_linearly(Info, Locals),
+ Goals, polyhedron.empty, ConvexUnion),
+ polyhedron.intersection(ConvexUnion, !Polyhedron).
+
+:- pred traverse_abstract_disjunct_linearly(fixpoint_info::in,
+ size_vars::in, abstract_goal::in, polyhedron::in, polyhedron::out)
+ is det.
+
+traverse_abstract_disjunct_linearly(Info, Locals, Goal, !Polyhedron) :-
+ Varset = Info ^ varset,
+ traverse_abstract_goal(Info, Goal, polyhedron.identity, Polyhedron0),
+ Polyhedron1 = polyhedron.project(Locals, Varset, Polyhedron0),
+ polyhedron.convex_union(Varset, yes(Info ^ max_matrix_size),
+ Polyhedron1, !Polyhedron).
+
+ % This version computes the convex hull pairwise. That is
+ % ( A ; B ; C ; D) is processed as: (( A \/ B ) \/ ( C \/ D)).
+ %
+ % XXX This code is currently unused.
+ %
+:- pred traverse_abstract_disj_pairwise(abstract_goals::in, size_vars::in,
+ fixpoint_info::in, polyhedron::in, polyhedron::out) is det.
+
+traverse_abstract_disj_pairwise(Goals, Locals, Info, !Polyhedron) :-
+ Varset = Info ^ varset,
+ % XXX at the moment, could be !.Poly...
+ PolyToLeft = polyhedron.identity,
+ %
+ % First convert the list of goals into their corresponding
+ % polyhedra
+ %
+ ToPoly = (func(Goal) = Poly :-
+ traverse_abstract_goal(Info, Goal, PolyToLeft, Poly0),
+ Poly = polyhedron.project(Locals, Varset, Poly0)
+ ),
+ Polyhedra0 = list.map(ToPoly, Goals),
+ %
+ % Now pairwise convex hull them.
+ %
+ HullOp = (func(A, B) = C :-
+ polyhedron.convex_union(Varset, yes(Info ^ max_matrix_size),
+ A, B, C)
+ ),
+ ConvexUnion = pairwise_map(HullOp, [ polyhedron.empty | Polyhedra0]),
+ polyhedron.intersection(ConvexUnion, !Polyhedron).
+
+ % This assumes that the operation in question is associative and
+ % commutative.
+ %
+ :- func pairwise_map(func(T, T) = T, list(T)) = T.
+
+pairwise_map(_, []) = _ :- unexpected(this_file, "pairwise_map: empty list").
+pairwise_map(_, [X]) = X.
+pairwise_map(Op, List @ [_, _ | _]) = X :-
+ pairwise_map_2(Op, List, [], X0),
+ X = pairwise_map(Op, X0).
+
+:- pred pairwise_map_2(func(T, T) = T, list(T), list(T), list(T)).
+:- mode pairwise_map_2(func(in, in) = out is det, in, in, out) is det.
+
+pairwise_map_2(_, [], !Acc).
+pairwise_map_2(_, [X], Acc, [X | Acc]).
+pairwise_map_2(Op, [X, Y | Rest], !Acc) :-
+ list.cons(Op(X, Y), !Acc),
+ pairwise_map_2(Op, Rest, !Acc).
+
+%------------------------------------------------------------------------------%
+%
+% Fixpoint test.
+%
+
+:- pred test_fixpoint_and_perhaps_widen(widening::in, size_varset::in, int::in,
+ polyhedron::in, polyhedron::in, polyhedron::out, bool::out) is det.
+
+test_fixpoint_and_perhaps_widen(after_fixed_cutoff(Threshold), Varset,
+ Iteration, OldPoly, NewPoly, ResultPoly, ChangeFlag) :-
+ ( Iteration > Threshold ->
+ ResultPoly = widen(OldPoly, NewPoly, Varset)
+ ;
+ ResultPoly = NewPoly
+ ),
+ ChangeFlag = test_fixpoint(NewPoly, OldPoly, Varset).
+
+:- func test_fixpoint(polyhedron, polyhedron, size_varset) = bool.
+
+test_fixpoint(NewPoly, OldPoly, Varset) = ChangeFlag :-
+ %
+ % Constraints from this iteration.
+ %
+ NewConstraints = polyhedron.non_false_constraints(NewPoly),
+ %
+ % Constraints from previous iteration.
+ %
+ OldConstraints = polyhedron.non_false_constraints(OldPoly),
+ UnchangedConstraints = list.filter(entailed(Varset, NewConstraints),
+ OldConstraints),
+ ( if list.same_length(OldConstraints, UnchangedConstraints)
+ then ChangeFlag = no
+ else ChangeFlag = yes
+ ).
+
+%-----------------------------------------------------------------------------
+
+:- func this_file = string.
+
+this_file = "term_constr_fixpoint.m".
+
+%-----------------------------------------------------------------------------%
+:- end_module transform_hlds.term_constr_fixpoint.
+%-----------------------------------------------------------------------------%
Index: compiler/term_constr_initial.m
===================================================================
RCS file: compiler/term_constr_initial.m
diff -N compiler/term_constr_initial.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/term_constr_initial.m 24 Mar 2005 04:19:36 -0000
@@ -0,0 +1,586 @@
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%----------------------------------------------------------------------------%
+% Copyright (C) 2003 The University of Melbourne.
+% 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_constr_initial.m
+% main author: juliensf
+%
+% This module fills in the appropriate argument size information and
+% termination property for builtin and compiler generated predicates.
+% It also handles the processing of termination pragmas and sets
+% the termination properties for foreign procedures.
+
+% Handling of pragma terminates/does_not_terminate
+%
+% At the moment we set the termination status as appropriate, set the arg
+% size information to true and fill in the size_var_map with dummy values
+% (because intermodule optimization requires these values to be in place).
+% If we ever support user specified arg size constraints this scheme
+% will need modifying - in particular we will need to make sure that
+% the identity of the variables in the size_var_map matches those
+% in the constraints.
+
+% A lot of this code is based on that in termination.m that does the
+% equivalent jobs for the old termination analyser.
+
+%----------------------------------------------------------------------------%
+
+:- module transform_hlds.term_constr_initial.
+
+:- interface.
+
+:- import_module hlds.hlds_module.
+
+:- import_module io.
+
+ % Prepare a module for running the main termination pass.
+ % This involves setting up argument size and termination information
+ % for builtin and compiler-generated predicates and also setting
+ % the termination status of those predicates that have termination
+ % pragmas attached to them.
+ %
+ % XXX Fix handling of terminates/does_not_terminate foreign proc.
+ % attributes.
+ %
+:- pred term_constr_initial.preprocess_module(module_info::in,
+ module_info::out, io::di, io::uo) is det.
+
+%----------------------------------------------------------------------------%
+%----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module check_hlds.inst_match.
+:- import_module check_hlds.mode_util.
+:- import_module check_hlds.type_util.
+
+:- import_module hlds.hlds_data.
+:- import_module hlds.hlds_goal.
+:- import_module hlds.hlds_pred.
+:- import_module hlds.hlds_out.
+:- import_module hlds.passes_aux.
+:- import_module hlds.special_pred.
+
+:- import_module libs.globals.
+:- import_module libs.lp_rational.
+:- import_module libs.options.
+:- import_module libs.polyhedron.
+:- import_module libs.rat.
+
+:- import_module mdbcomp.prim_data.
+
+:- import_module parse_tree.error_util.
+:- import_module parse_tree.mercury_to_mercury.
+:- import_module parse_tree.modules.
+:- import_module parse_tree.prog_data.
+:- import_module parse_tree.prog_out.
+:- import_module parse_tree.prog_util.
+
+:- import_module transform_hlds.termination2.
+:- import_module transform_hlds.dependency_graph.
+:- import_module transform_hlds.term_constr_util.
+:- import_module transform_hlds.term_constr_errors.
+:- import_module transform_hlds.term_constr_data.
+:- import_module transform_hlds.term_norm.
+
+:- import_module bool.
+:- import_module bag.
+:- import_module char.
+:- import_module int.
+:- import_module list.
+:- import_module map.
+:- import_module relation.
+:- import_module require.
+:- import_module set.
+:- import_module std_util.
+:- import_module string.
+:- import_module svmap.
+:- import_module svvarset.
+:- import_module term.
+:- import_module varset.
+
+%----------------------------------------------------------------------------%
+%
+% Process each predicate and set the termination property
+%
+
+% Sets termination to `cannot_loop' if:
+% - there is a `terminates' pragma defined for the predicate.
+% - there is a `check_termination' pragma defined for the predicate
+% *and* the compiler is not currently generating the intermodule
+% optimization file.
+% - the predicate is builtin or compiler generated. (These are assumed
+% to terminate.
+%
+% Set the termination to `can_loop' if:
+% - there is a `does_not_terminate' pragma defined for this predicate.
+% - the predicate is imported and there is no other source of information
+% - about it (termination_info pragmas, terminates pragmas, builtin).
+%
+% XXX This does the wrong thing for copy/2 & typed_unify/2. In both
+% cases the constraints should that |HeadVar__1| = |HeadVar__2|.
+
+preprocess_module(!ModuleInfo, !IO) :-
+ module_info_predids(!.ModuleInfo, PredIds),
+ process_builtin_preds(PredIds, !ModuleInfo, !IO),
+ process_imported_preds(PredIds, !ModuleInfo).
+
+%----------------------------------------------------------------------------%
+%
+% Set the argument size constraints for imported procedures.
+%
+
+% When interargument size constraints are imported from other modules there
+% are two parts. The first of the these is a list of ints. Each int
+% represents one of a procedures arguments (including typeinfo related ones).
+%
+% XXX Since typeinfos all became zero-sized we don't actually need this list.
+% (I forget the reason we did need it, I think it was something to do with
+% the fact that the compiler cannot (presently) distinguish between typeinfos
+% it has introduced and ones that were there anyway - in some of the library
+% modules).
+%
+% The second piece of information here is the constraints themselves which
+% have been using the integer variable ids to represent actual variables.
+%
+% We now know the actual head_vars so we create size_vars and substitute
+% these into the actual constraints.
+%
+
+:- pred process_imported_preds(list(pred_id)::in,
+ module_info::in, module_info::out) is det.
+
+process_imported_preds(PredIds, !ModuleInfo) :-
+ list.foldl(process_imported_pred, PredIds, !ModuleInfo).
+
+:- pred process_imported_pred(pred_id::in, module_info::in, module_info::out)
+ is det.
+
+process_imported_pred(PredId, !ModuleInfo) :-
+ some [!PredTable] (
+ module_info_preds(!.ModuleInfo, !:PredTable),
+ module_info_type_spec_info(!.ModuleInfo, TypeSpecInfo),
+ TypeSpecInfo = type_spec_info(_, TypeSpecPredIds, _, _),
+ ( not set.member(PredId, TypeSpecPredIds) ->
+ PredInfo0 = !.PredTable ^ det_elem(PredId),
+ process_imported_procs(PredInfo0, PredInfo),
+ svmap.det_update(PredId, PredInfo, !PredTable),
+ module_info_set_preds(!.PredTable, !ModuleInfo)
+ ;
+ true
+ )
+ ).
+
+:- pred process_imported_procs(pred_info::in, pred_info::out) is det.
+
+process_imported_procs(!PredInfo) :-
+ some [!ProcTable] (
+ pred_info_procedures(!.PredInfo, !:ProcTable),
+ ProcIds = pred_info_procids(!.PredInfo),
+ list.foldl(process_imported_proc, ProcIds, !ProcTable),
+ pred_info_set_procedures(!.ProcTable, !PredInfo)
+ ).
+
+:- pred process_imported_proc(proc_id::in, proc_table::in, proc_table::out)
+ is det.
+
+process_imported_proc(ProcId, !ProcTable) :-
+ some [!ProcInfo] (
+ !:ProcInfo = !.ProcTable ^ det_elem(ProcId),
+ proc_info_get_termination2_info(!.ProcInfo, TermInfo0),
+ process_imported_term_info(!.ProcInfo, TermInfo0, TermInfo),
+ proc_info_set_termination2_info(TermInfo, !ProcInfo),
+ svmap.det_update(ProcId, !.ProcInfo, !ProcTable)
+ ).
+
+:- pred process_imported_term_info(proc_info::in,
+ termination2_info::in, termination2_info::out) is det.
+
+process_imported_term_info(ProcInfo, !TermInfo) :-
+ ( !.TermInfo ^ import_headvarids = yes(HeadVarIds) ->
+ proc_info_headvars(ProcInfo, HeadVars),
+ make_size_var_map(HeadVars, _SizeVarset, SizeVarMap),
+ map.from_corresponding_lists(HeadVarIds, HeadVars, IdsToProgVars),
+ create_substitution_map(HeadVarIds, IdsToProgVars, SizeVarMap,
+ SubstMap),
+ create_arg_size_polyhedron(SubstMap, !.TermInfo ^ import_success,
+ MaybeSuccessPoly),
+ create_arg_size_polyhedron(SubstMap, !.TermInfo ^ import_failure,
+ MaybeFailurePoly),
+ SizeVars = prog_vars_to_size_vars(SizeVarMap, HeadVars),
+ !:TermInfo = !.TermInfo ^ size_var_map := SizeVarMap,
+ !:TermInfo = !.TermInfo ^ head_vars := SizeVars,
+ !:TermInfo = !.TermInfo ^ success_constrs := MaybeSuccessPoly,
+ !:TermInfo = !.TermInfo ^ failure_constrs := MaybeFailurePoly,
+ !:TermInfo = !.TermInfo ^ import_headvarids := no,
+ !:TermInfo = !.TermInfo ^ import_success := no,
+ !:TermInfo = !.TermInfo ^ import_failure := no
+ ;
+ true
+ ).
+
+:- pred create_substitution_map(list(int)::in, map(int, prog_var)::in,
+ size_var_map::in, map(int, size_var)::out) is det.
+
+create_substitution_map(Ids, IdToProgVar, SizeVarMap, IdToSizeVar) :-
+ list.foldl((pred(Id::in, !.Map::in, !:Map::out) is det :-
+ ProgVar = IdToProgVar ^ det_elem(Id),
+ SizeVar = map.lookup(SizeVarMap, ProgVar),
+ svmap.set(Id, SizeVar, !Map)
+ ), Ids, map.init, IdToSizeVar).
+
+:- pred create_arg_size_polyhedron(map(int, var)::in,
+ maybe(pragma_constr_arg_size_info)::in, maybe(polyhedron)::out) is det.
+
+create_arg_size_polyhedron(_, no, no).
+create_arg_size_polyhedron(SubstMap, yes(PragmaArgSizeInfo),
+ yes(Polyhedron)) :-
+ list.map(create_arg_size_constraint(SubstMap), PragmaArgSizeInfo,
+ Constraints),
+ Polyhedron = polyhedron.from_constraints(Constraints).
+
+:- pred create_arg_size_constraint(map(int, var)::in, arg_size_constr::in,
+ constraint::out) is det.
+
+create_arg_size_constraint(SubstMap, le(Terms0, Constant), Constraint) :-
+ list.map(create_lp_term(SubstMap), Terms0, Terms),
+ Constraint = constraint(Terms, (=<), Constant).
+create_arg_size_constraint(SubstMap, eq(Terms0, Constant), Constraint) :-
+ list.map(create_lp_term(SubstMap), Terms0, Terms),
+ Constraint = constraint(Terms, (=), Constant).
+
+:- pred create_lp_term(map(int, var)::in, pair(int, rat)::in, lp_term::out)
+ is det.
+
+create_lp_term(SubstMap, VarId - Coefficient, Var - Coefficient) :-
+ Var = SubstMap ^ det_elem(VarId).
+
+%----------------------------------------------------------------------------%
+%
+% Set up information for builtins.
+%
+
+:- pred process_builtin_preds(list(pred_id)::in,
+ module_info::in, module_info::out, io::di, io::uo) is det.
+
+process_builtin_preds([], !ModuleInfo, !IO).
+process_builtin_preds([PredId | PredIds], !ModuleInfo, !IO) :-
+ write_pred_progress_message("% Termination checking ", PredId,
+ !.ModuleInfo, !IO),
+ globals.io_lookup_bool_option(make_optimization_interface, MakeOptInt,
+ !IO),
+ some [!PredTable] (
+ module_info_preds(!.ModuleInfo, !:PredTable),
+ PredInfo0 = !.PredTable ^ det_elem(PredId),
+ process_builtin_procs(MakeOptInt, PredId, !.ModuleInfo,
+ PredInfo0, PredInfo),
+ svmap.det_update(PredId, PredInfo, !PredTable),
+ module_info_set_preds(!.PredTable, !ModuleInfo)
+ ),
+ process_builtin_preds(PredIds, !ModuleInfo, !IO).
+
+ % It is possible for compiler generated/mercury builtin
+ % predicates to be imported or locally defined, so they
+ % must be covered here separately.
+ %
+:- pred process_builtin_procs(bool::in, pred_id::in, module_info::in,
+ pred_info::in, pred_info::out) is det.
+
+process_builtin_procs(MakeOptInt, PredId, ModuleInfo, !PredInfo) :-
+ pred_info_import_status(!.PredInfo, ImportStatus),
+ pred_info_get_markers(!.PredInfo, Markers),
+ pred_info_context(!.PredInfo, Context),
+ some [!ProcTable] (
+ pred_info_procedures(!.PredInfo, !:ProcTable),
+ ProcIds = pred_info_procids(!.PredInfo),
+ (
+ set_compiler_gen_terminates(!.PredInfo, ProcIds, PredId,
+ ModuleInfo, !ProcTable)
+ ->
+ true
+ ;
+ status_defined_in_this_module(ImportStatus, yes)
+ ->
+ % XXX At the moment if a procedure has a pragma terminates
+ % declaration its argument size information is set to true.
+ % If we allow the user to specify the arg size info this
+ % will need to change. This also means that the
+ % size_var_map for the procedure is never created. This
+ % causes problems with intermodule optimization. The
+ % current workaround is to set up a dummy size_var_map for
+ % each procedure.
+ %
+ ( check_marker(Markers, terminates) ->
+ TermStatus = cannot_loop(pragma_supplied),
+ change_procs_constr_termination_info(ProcIds,
+ yes, TermStatus, !ProcTable),
+ ArgSizeInfo = polyhedron.identity,
+ change_procs_constr_arg_size_info(ProcIds, yes,
+ ArgSizeInfo, !ProcTable),
+ initialise_size_var_maps(ProcIds, !ProcTable)
+ ;
+ true
+ )
+ ;
+ % Not defined in this module.
+
+ % All of the predicates that are processed in this section
+ % are imported in some way. With imported predicates, any
+ % 'check_termination' pragmas will be checked by the
+ % compiler when it compiles the relevant source file (that
+ % the predicate was imported from). When making the
+ % intermodule optimization interfaces, the check_termination
+ % will not be checked when the relevant source file is compiled,
+ % so it cannot be depended upon.
+ (
+ (
+ check_marker(Markers, terminates)
+ ;
+ MakeOptInt = no,
+ check_marker(Markers, check_termination)
+ )
+ ->
+ change_procs_constr_termination_info(ProcIds, yes,
+ cannot_loop(pragma_supplied), !ProcTable)
+ ;
+ change_procs_constr_termination_info(ProcIds, no,
+ can_loop([]), !ProcTable)
+ ),
+ ArgSizeInfo = polyhedron.identity,
+ change_procs_constr_arg_size_info(ProcIds, yes, ArgSizeInfo,
+ !ProcTable)
+ ),
+ ( check_marker(Markers, does_not_terminate) ->
+ TerminationInfo =
+ can_loop([Context - does_not_term_pragma(PredId)]),
+ NonTermArgSizeInfo = polyhedron.identity,
+ change_procs_constr_termination_info(ProcIds, yes,
+ TerminationInfo, !ProcTable),
+ change_procs_constr_arg_size_info(ProcIds, yes,
+ NonTermArgSizeInfo, !ProcTable),
+ initialise_size_var_maps(ProcIds, !ProcTable)
+ ;
+ true
+ ),
+ pred_info_set_procedures(!.ProcTable, !PredInfo)
+ ).
+:- pred set_compiler_gen_terminates(pred_info::in, list(proc_id)::in,
+ pred_id::in, module_info::in, proc_table::in, proc_table::out)
+ is semidet.
+
+set_compiler_gen_terminates(PredInfo, ProcIds, PredId, ModuleInfo,
+ !ProcTable) :-
+ ( hlds_pred.pred_info_is_builtin(PredInfo) ->
+ set_builtin_terminates(ProcIds, PredId, PredInfo, ModuleInfo,
+ !ProcTable)
+ ;
+ (
+ Name = pred_info_name(PredInfo),
+ Arity = pred_info_orig_arity(PredInfo),
+ special_pred_name_arity(SpecPredId0, Name, Arity),
+ ModuleName = pred_info_module(PredInfo),
+ any_mercury_builtin_module(ModuleName)
+ ->
+ SpecialPredId = SpecPredId0
+ ;
+ pred_info_get_origin(PredInfo, PredOrigin),
+ PredOrigin = special_pred(SpecialPredId - _)
+ )
+ ->
+ set_generated_terminates(ProcIds, SpecialPredId, ModuleInfo,
+ !ProcTable)
+ ;
+ fail
+ ).
+
+:- pred set_generated_terminates(list(proc_id)::in, special_pred_id::in,
+ module_info::in, proc_table::in, proc_table::out) is det.
+
+set_generated_terminates([], _, _, !ProcTable).
+set_generated_terminates([ProcId | ProcIds], SpecialPredId, ModuleInfo,
+ !ProcTable) :-
+ %
+ % We don't need to do anything special for solver type initialisation
+ % predicates. Leaving it up to the analyser may result in better
+ % argument size information anyway.
+ %
+ ( SpecialPredId \= initialise ->
+ ProcInfo0 = !.ProcTable ^ det_elem(ProcId),
+ proc_info_headvars(ProcInfo0, HeadVars),
+ proc_info_vartypes(ProcInfo0, VarTypes),
+ special_pred_id_to_termination(SpecialPredId, HeadVars, ModuleInfo,
+ VarTypes, ArgSize, Termination, VarMap, HeadSizeVars),
+ some [!TermInfo] (
+ proc_info_get_termination2_info(ProcInfo0, !:TermInfo),
+ !:TermInfo = !.TermInfo ^ success_constrs := yes(ArgSize),
+ !:TermInfo = !.TermInfo ^ term_status := yes(Termination),
+ IntermodStatus = yes(not_mutually_recursive),
+ !:TermInfo = !.TermInfo ^ intermod_status := IntermodStatus,
+ !:TermInfo = !.TermInfo ^ size_var_map := VarMap,
+ !:TermInfo = !.TermInfo ^ head_vars := HeadSizeVars,
+ proc_info_set_termination2_info(!.TermInfo, ProcInfo0,
+ ProcInfo)
+ ),
+ svmap.det_update(ProcId, ProcInfo, !ProcTable)
+ ;
+ true
+ ),
+ set_generated_terminates(ProcIds, SpecialPredId, ModuleInfo,
+ !ProcTable).
+
+ % Handle the generation of constraints for special predicates.
+ % XXX argument size constraints for unify predicates for types
+ % with user-defined equality may not be correct.
+ %
+:- pred special_pred_id_to_termination(special_pred_id::in, prog_vars::in,
+ module_info::in, vartypes::in, constr_arg_size_info::out,
+ constr_termination_info::out, size_var_map::out, size_vars::out) is det.
+
+special_pred_id_to_termination(compare, HeadProgVars, ModuleInfo, VarTypes,
+ ArgSizeInfo, Termination, SizeVarMap, HeadSizeVars) :-
+ make_info(HeadProgVars, ModuleInfo, VarTypes, ArgSizeInfo, Termination,
+ SizeVarMap, HeadSizeVars).
+special_pred_id_to_termination(unify, HeadProgVars, ModuleInfo, VarTypes,
+ ArgSizeInfo, Termination, SizeVarMap, HeadSizeVars) :-
+ make_size_var_map(HeadProgVars, _SizeVarset, SizeVarMap),
+ HeadSizeVars = prog_vars_to_size_vars(SizeVarMap, HeadProgVars),
+ Zeros = find_zero_size_vars(ModuleInfo, SizeVarMap, VarTypes),
+ NonZeroHeadSizeVars = list.filter(isnt(is_zero_size_var(Zeros)),
+ HeadSizeVars),
+ %
+ % unify may have more than two input arguments if one of them is a
+ % type-info related arg, or some such thing. Since all these have
+ % zero-size type, after removing them there are two possibilities.
+ % The list of non-zero size type head_vars is empty (if the
+ % arguments are zero-sized) or it contains two elements.
+ %
+ ( NonZeroHeadSizeVars = [] ->
+ Constrs = []
+ ; NonZeroHeadSizeVars = [VarA, VarB] ->
+ Constrs = [make_vars_eq_constraint(VarA, VarB)]
+ ;
+ unexpected(this_file, "special_pred_id_to_termination/7: " ++
+ "wrong number of args for unify.")
+ ),
+ Polyhedron = polyhedron.from_constraints(Constrs),
+ ArgSizeInfo = Polyhedron,
+ Termination = cannot_loop(builtin).
+special_pred_id_to_termination(index, HeadProgVars, ModuleInfo, VarTypes,
+ ArgSize, Termination, SizeVarMap, HeadSizeVars) :-
+ NumToDrop = list.length(HeadProgVars) - 2,
+ ( list.drop(NumToDrop, HeadProgVars, _ZeroSizeHeadVars) ->
+ make_info(HeadProgVars, ModuleInfo, VarTypes, ArgSize,
+ Termination, SizeVarMap, HeadSizeVars)
+ ;
+ unexpected(this_file,
+ "Less than two arguments to builtin index.")
+ ).
+special_pred_id_to_termination(initialise, _, _, _, _, _, _, _) :-
+ unexpected(this_file, "special_pred_id_to_termination/8 " ++
+ "initialise predicate").
+
+ % Sets up the arg_size an termination info for those special preds
+ % (compare and index) where we don't know any arg-size constraints.
+ %
+:- pred make_info(list(prog_var)::in, module_info::in, vartypes::in,
+ constr_arg_size_info::out, constr_termination_info::out,
+ size_var_map::out, size_vars::out) is det.
+
+make_info(HeadProgVars, ModuleInfo, VarTypes, ArgSize, Termination, SizeVarMap,
+ HeadSizeVars) :-
+ make_size_var_map(HeadProgVars, _SizeVarset, SizeVarMap),
+ Zeros = find_zero_size_vars(ModuleInfo, SizeVarMap, VarTypes),
+ Constraints = derive_nonneg_eqns(SizeVarMap, Zeros),
+ Polyhedron = polyhedron.from_constraints(Constraints),
+ ArgSize = Polyhedron,
+ Termination = cannot_loop(builtin),
+ HeadSizeVars = prog_vars_to_size_vars(SizeVarMap, HeadProgVars).
+
+ % Set the termination information for builtin
+ % predicates. The list of proc_ids must refer to builtin predicates.
+ %
+:- pred set_builtin_terminates(list(proc_id)::in, pred_id::in, pred_info::in,
+ module_info::in, proc_table::in, proc_table::out) is det.
+
+set_builtin_terminates([], _, _, _, !ProcTable).
+set_builtin_terminates([ProcId | ProcIds], PredId, PredInfo, ModuleInfo,
+ !ProcTable) :-
+ ProcInfo0 = !.ProcTable ^ det_elem(ProcId),
+ proc_info_headvars(ProcInfo0, HeadVars),
+ PredModule = pred_info_module(PredInfo),
+ PredName = pred_info_name(PredInfo),
+ PredArity = pred_info_orig_arity(PredInfo),
+ make_size_var_map(HeadVars, _SizeVarset, SizeVarMap),
+ (
+ hlds_pred.no_type_info_builtin(PredModule, PredName, PredArity)
+ ->
+ Constrs = process_no_type_info_builtin(PredName, HeadVars,
+ SizeVarMap)
+ ;
+ all_args_input_or_zero_size(ModuleInfo, PredInfo, ProcInfo0)
+ ->
+ Constrs = []
+ ;
+ unexpected(this_file, "builtin with non-zero-size args.")
+ ),
+ Polyhedron = polyhedron.from_constraints(Constrs),
+ ArgSizeInfo = yes(Polyhedron),
+ HeadSizeVars = prog_vars_to_size_vars(SizeVarMap, HeadVars),
+ some [!TermInfo] (
+ proc_info_get_termination2_info(ProcInfo0, !:TermInfo),
+ !:TermInfo = !.TermInfo ^ success_constrs := ArgSizeInfo,
+ !:TermInfo = !.TermInfo ^ term_status := yes(cannot_loop(builtin)),
+ !:TermInfo = !.TermInfo ^ intermod_status := yes(not_mutually_recursive),
+ !:TermInfo = !.TermInfo ^ size_var_map := SizeVarMap,
+ !:TermInfo = !.TermInfo ^ head_vars := HeadSizeVars,
+ proc_info_set_termination2_info(!.TermInfo, ProcInfo0, ProcInfo)
+ ),
+ svmap.det_update(ProcId, ProcInfo, !ProcTable),
+ set_builtin_terminates(ProcIds, PredId, PredInfo, ModuleInfo,
+ !ProcTable).
+
+:- func process_no_type_info_builtin(string, prog_vars, size_var_map)
+ = constraints.
+
+process_no_type_info_builtin(PredName, HeadVars, SizeVarMap) = Constraints :-
+ (
+ HeadVars = [HVar1, HVar2],
+ (PredName = "unsafe_type_cast" ; PredName = "unsafe_promise_unique")
+ ->
+ SizeVar1 = prog_var_to_size_var(SizeVarMap, HVar1),
+ SizeVar2 = prog_var_to_size_var(SizeVarMap, HVar2),
+ Constraints = [make_vars_eq_constraint(SizeVar1, SizeVar2)]
+ ;
+ unexpected(this_file,
+ "Unrecognised predicate passed to process_special_builtin.")
+ ).
+
+%----------------------------------------------------------------------------%
+
+:- pred initialise_size_var_maps(list(proc_id)::in,
+ proc_table::in, proc_table::out) is det.
+
+initialise_size_var_maps([], !ProcTable).
+initialise_size_var_maps([ProcId | ProcIds], !ProcTable) :-
+ ProcInfo0 = !.ProcTable ^ det_elem(ProcId),
+ proc_info_get_termination2_info(ProcInfo0, TermInfo0),
+ proc_info_headvars(ProcInfo0, HeadVars),
+ make_size_var_map(HeadVars, _SizeVarset, SizeVarMap),
+ TermInfo = TermInfo0 ^ size_var_map := SizeVarMap,
+ proc_info_set_termination2_info(TermInfo, ProcInfo0, ProcInfo),
+ svmap.det_update(ProcId, ProcInfo, !ProcTable),
+ initialise_size_var_maps(ProcIds, !ProcTable).
+
+%----------------------------------------------------------------------------%
+
+:- func this_file = string.
+
+this_file = "term_constr_initial.m".
+
+%----------------------------------------------------------------------------%
+:- end_module term_constr_initial.
+%----------------------------------------------------------------------------%
--------------------------------------------------------------------------
mercury-reviews mailing list
post: mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the reviews
mailing list