[m-rev.] for review: new termination analyser (part 6 of 6)
Julien Fischer
juliensf at cs.mu.OZ.AU
Thu Mar 24 15:47:26 AEDT 2005
+%----------------------------------------------------------------------------%
Index: compiler/term_constr_pass2.m
===================================================================
RCS file: compiler/term_constr_pass2.m
diff -N compiler/term_constr_pass2.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/term_constr_pass2.m 23 Mar 2005 23:35:19 -0000
@@ -0,0 +1,706 @@
+%-----------------------------------------------------------------------------%
+% 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_pass2.m
+% main author: juliensf
+%
+% This module analyses a SCC of the call-graph and tries to prove that
+% it terminates.
+%
+% XXX This version is just a place-holder. It attempts a very simple
+% proof method which is essentially what the existing termination analyser
+% does.
+%
+%-----------------------------------------------------------------------------%
+
+:- module transform_hlds.term_constr_pass2.
+
+:- interface.
+
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_pred.
+
+:- import_module transform_hlds.termination2.
+
+:- import_module io.
+:- import_module list.
+
+%-----------------------------------------------------------------------------%
+
+:- type pass2_options.
+
+:- func pass2_options_init(int) = pass2_options.
+
+:- pred prove_termination_in_scc(pass2_options::in, list(pred_proc_id)::in,
+ module_info::in, constr_termination_info::out, io::di, io::uo) is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module check_hlds.mode_util.
+
+:- import_module hlds.hlds_pred.
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_out.
+
+:- import_module libs.globals.
+:- import_module libs.lp_rational.
+:- import_module libs.options.
+:- import_module libs.polyhedron.
+:- import_module libs.rat.
+
+:- import_module parse_tree.error_util.
+:- import_module parse_tree.prog_data.
+:- import_module parse_tree.mercury_to_mercury.
+
+:- import_module transform_hlds.term_constr_util.
+:- import_module transform_hlds.term_constr_errors.
+:- import_module transform_hlds.term_constr_data.
+
+:- import_module assoc_list.
+:- import_module bimap.
+:- import_module bool.
+:- import_module int.
+:- import_module map.
+:- import_module require.
+:- import_module set.
+:- import_module std_util.
+:- import_module string.
+:- import_module term.
+:- import_module varset.
+
+%-----------------------------------------------------------------------------%
+%
+% Handle pass 2 options.
+%
+
+:- type pass2_options
+ ---> pass2_options(
+ max_matrix_size :: int
+ ).
+
+pass2_options_init(MaxSize) = pass2_options(MaxSize).
+
+%-----------------------------------------------------------------------------%
+
+:- type scc == list(abstract_ppid).
+
+ % Each edge in the call-graph represents a single call site.
+ %
+:- type edge
+ ---> edge(
+ head :: abstract_ppid,
+ % The procedure that is making the call.
+
+ zeros :: set(size_var),
+ % Variables in the procedure known to have
+ % zero-size.
+
+ head_args :: size_vars,
+ % The size_vars that correspond to the
+ % variables in the head of the procedure.
+
+ label :: polyhedron,
+ % The constraints that occur between the
+ % head of the procedure and the call.
+
+ call :: abstract_ppid,
+ % The callee procedure.
+
+ call_args :: size_vars
+ % The size_vars that correspond to the
+ % variables in the procedure call.
+ ).
+
+:- type edges == list(edge).
+
+:- type cycle
+ ---> cycle(
+ nodes :: list(abstract_ppid),
+ % A list of every procedure involved in
+ % this cycle.
+
+ edges :: list(edge)
+ % A list of edges involved in this cycle.
+ % Note: It is not ordered. This allows
+ % us to decide (later) on where we want
+ % the cycle to start.
+ ).
+
+:- type cycles == list(cycle).
+
+ % A c_cycle is a collapsed cycle; where equalities have replaced
+ % calls between corresponding edges.
+
+%
+% A little clarification on this: Each `c_cycles' field is list of
+% elementary cycles that start and end at `start'.
+%
+
+:- type cycle_set
+ ---> c_set(
+ start :: abstract_ppid,
+ c_cycles :: list(edge)
+ ).
+
+%-----------------------------------------------------------------------------%
+
+prove_termination_in_scc(_, [], _, cannot_loop(analysis), !IO).
+prove_termination_in_scc(Options, SCC0 @ [_|_], ModuleInfo, Result, !IO) :-
+ AbstractSCC = get_abstract_scc(ModuleInfo, SCC0),
+ % XXX Pass 1 should really set this up.
+ SCC = list.map((func(A) = real(A)), SCC0),
+ ( scc_contains_recursion(AbstractSCC) ->
+ Varset = varset_from_abstract_scc(AbstractSCC),
+ Edges = label_edges_in_scc(AbstractSCC, ModuleInfo,
+ Options ^ max_matrix_size),
+ Cycles = find_elementary_cycles_in_scc(SCC, Edges),
+ CycleSets = partition_cycles(SCC, Cycles),
+ prove_termination(CycleSets, AbstractSCC, Varset, Result)
+ ;
+ Result = cannot_loop(analysis)
+ ).
+
+%-----------------------------------------------------------------------------%
+%
+% Predicates for labelling edges.
+%
+
+% Work out what the constraints are between each procedure head and each
+% call for every call in the SCC. This information is implicit in the
+% AR, so we traverse the AR building up a list of labelled edges as
+% we go - this is similar to the fixpoint calculation we performed in pass 1
+% except that we can stop after we have examined the last call. This often
+% means that we can avoid performing unnecessary convex hull operations.
+
+:- func label_edges_in_scc(abstract_scc, module_info, int) = edges.
+
+label_edges_in_scc(Procs, ModuleInfo, MaxMatrixSize) = Edges :-
+ FindEdges = (pred(Proc::in, !.Edges::in, !:Edges::out) is det :-
+ find_edges_in_goal(Proc, Procs, ModuleInfo, MaxMatrixSize,
+ Proc ^ body, 1, _, polyhedron.identity, _, [],
+ ProcEdges, yes, _),
+ list.append(ProcEdges, !Edges)
+ ),
+ list.foldl(FindEdges, Procs, [], Edges).
+
+ % The four accumulators here are for:
+ % (1) the number of calls seen so far
+ % (2) the constraints so far
+ % (3) the edges found
+ % (4) whether to abort or continue looking
+ %
+:- pred find_edges_in_goal(abstract_proc::in, abstract_scc::in,
+ module_info::in, int::in, abstract_goal::in, int::in, int::out,
+ polyhedron::in, polyhedron::out, edges::in, edges::out, bool::in,
+ bool::out) is det.
+
+find_edges_in_goal(Proc, AbstractSCC, ModuleInfo, MaxMatrixSize,
+ AbstractGoal, !Calls, !Polyhedron, !Edges, !Continue) :-
+ AbstractGoal = disj(Goals, _, Locals, _),
+ (
+ !.Continue = yes,
+ %
+ % XXX We may be able to prove termination in more cases
+ % if we pass in !.Polyhedron instead of
+ % of polyhedron.identity ... although I don't think
+ % it is a major concern at the moment.
+ %
+ find_edges_in_disj(Proc, AbstractSCC, ModuleInfo,
+ MaxMatrixSize, polyhedron.identity, Goals, !Calls,
+ [], DisjConstrs0, [], Edges1, !Continue),
+ Edges2 = list.map(fix_edges(!.Polyhedron), Edges1),
+ list.append(Edges2, !Edges),
+ (
+ !.Continue = yes,
+ Varset = Proc ^ varset,
+ DisjConstrs = polyhedron.project_all(Varset, Locals,
+ DisjConstrs0),
+ Constrs2 = list.foldl(
+ polyhedron.convex_union(Varset,
+ yes(MaxMatrixSize)), DisjConstrs,
+ polyhedron.empty),
+ polyhedron.intersection(Constrs2, !Polyhedron)
+ ;
+ !.Continue = no
+ )
+ ;
+ !.Continue = no
+ ).
+
+find_edges_in_goal(Proc, AbstractSCC, ModuleInfo, MaxMatrixSize,
+ AbstractGoal, !Calls, !Polyhedron, !Edges, !Continue) :-
+ AbstractGoal = conj(Goals, Locals, _),
+ (
+ !.Continue = yes,
+ list.foldl4(find_edges_in_goal(Proc, AbstractSCC, ModuleInfo,
+ MaxMatrixSize),
+ Goals, !Calls, !Polyhedron, !Edges, !Continue),
+ (
+ !.Continue = yes,
+ polyhedron.project(Locals, Proc ^ varset, !Polyhedron)
+ ;
+ !.Continue = no
+ )
+ ;
+ !.Continue = no
+ ).
+
+find_edges_in_goal(Proc, _AbstractSCC, ModuleInfo, _,
+ call(CallPPId0, _, CallVars, ZeroVars, _, _, _),
+ !Calls, !Polyhedron, !Edges, !Continue) :-
+ %
+ % Having found a call we now need to construct a label for that
+ % edge and then continue looking for more edges.
+ %
+ Edge = edge(Proc ^ ppid, Proc ^ zeros, Proc ^ head_vars, !.Polyhedron,
+ CallPPId0, CallVars),
+ list.cons(Edge, !Edges),
+ %
+ % Update the call count and maybe stop processing if that was
+ % the last call.
+ %
+ !:Calls = !.Calls + 1,
+ ( if !.Calls > Proc ^ calls
+ then !:Continue = no
+ else true
+ ),
+
+ (
+ !.Continue = no
+ ;
+ !.Continue = yes,
+ CallPPId0 = real(CallPPId),
+ module_info_pred_proc_info(ModuleInfo, CallPPId, _,
+ CallProcInfo),
+ proc_info_get_termination2_info(CallProcInfo, CallTermInfo),
+ MaybeArgSizeInfo = CallTermInfo ^ success_constrs,
+ (
+ MaybeArgSizeInfo = no,
+ unexpected(this_file,
+ "Proc with no arg size info in pass 2.")
+ ;
+ MaybeArgSizeInfo = yes(ArgSizePolyhedron0),
+ %
+ % If the polyhedron is universe then
+ % there's no point running the substitution.
+ %
+ ( polyhedron.is_universe(ArgSizePolyhedron0) ->
+ true
+ ;
+ MaybeCallProc = CallTermInfo ^ abstract_rep,
+ ( if MaybeCallProc = yes(CallProc0)
+ then CallProc = CallProc0
+ else unexpected(this_file,
+ "No abstract representation for proc.")
+ ),
+ HeadVars = CallProc ^ head_vars,
+ Subst = map.from_corresponding_lists(HeadVars,
+ CallVars),
+ Eqns0 = non_false_constraints(
+ ArgSizePolyhedron0),
+ Eqns1 = substitute_size_vars(Eqns0, Subst),
+ Eqns = lp_rational.set_vars_to_zero(ZeroVars, Eqns1),
+ ArgSizePolyhedron = from_constraints(Eqns),
+ polyhedron.intersection(ArgSizePolyhedron,
+ !Polyhedron)
+ )
+ )
+ ).
+
+find_edges_in_goal(_, _, _, _, AbstractGoal, !Calls, !Polyhedron, !Edges,
+ !Continue) :-
+ AbstractGoal = primitive(Primitive, _, _),
+ (
+ !.Continue = yes,
+ polyhedron.intersection(Primitive, !Polyhedron)
+ ;
+ !.Continue = no
+ ).
+
+:- pred find_edges_in_disj(abstract_proc::in, abstract_scc::in, module_info::in,
+ int::in, polyhedron::in, abstract_goals::in, int::in, int::out,
+ polyhedra::in, polyhedra::out, edges::in, edges::out, bool::in,
+ bool::out) is det.
+
+find_edges_in_disj(_, _, _, _, _, [], !Calls, !DisjConstrs, !Edges, !Continue).
+find_edges_in_disj(Proc, AbstractSCC, ModuleInfo, MaxMatrixSize, TopPoly,
+ [Disj | Disjs], !Calls, !DisjConstrs, !Edges, !Continue) :-
+ find_edges_in_goal(Proc, AbstractSCC, ModuleInfo, MaxMatrixSize, Disj,
+ !Calls, TopPoly, Constrs, !Edges, !Continue),
+ list.cons(Constrs, !DisjConstrs),
+ %
+ % This is why it is important that after numbering the
+ % calls in the AR we don't change anything around; otherwise
+ % this short-circuiting will not work correctly.
+ %
+ (
+ !.Continue = yes,
+ find_edges_in_disj(Proc, AbstractSCC, ModuleInfo,
+ MaxMatrixSize, TopPoly, Disjs, !Calls, !DisjConstrs,
+ !Edges, !Continue)
+ ;
+ !.Continue = no
+ ).
+
+:- func fix_edges(polyhedron, edge) = edge.
+
+fix_edges(Poly, Edge0) = Edge :-
+ Edge = Edge0 ^ label := polyhedron.intersection(Poly, Edge0 ^ label).
+
+%-----------------------------------------------------------------------------%
+%
+% Cycle detection.
+%
+
+% To find the elementary cycles of this SCC we perform a DFS of the call-graph.
+% Since the call-graph is technically a psuedograph (ie. it admits parallel
+% edges and self-loops), we first of all strip out any self-loops to make
+% things easier.
+
+:- func find_elementary_cycles_in_scc(list(abstract_ppid), edges) = cycles.
+
+find_elementary_cycles_in_scc(SCC, Edges0) = Cycles :-
+ %
+ % Get any self-loops for each procedure.
+ %
+ list.filter_map(direct_call, Edges0, Cycles0, Edges),
+ %
+ % Find larger elementary cycles in what is left.
+ %
+ Cycles1 = find_cycles(SCC, Edges),
+ Cycles = Cycles0 ++ Cycles1.
+
+ % Succeeds iff Edge is an edge that represents
+ % a directly recursive call (a self-loop in
+ % the psuedograph)
+ %
+:- pred direct_call(edge::in, cycle::out) is semidet.
+
+direct_call(Edge, Cycle) :-
+ Edge ^ head = Edge ^ call,
+ Cycle = cycle([Edge ^ head], [Edge]).
+
+:- func find_cycles(list(abstract_ppid), edges) = cycles.
+
+find_cycles(SCC, Edges) = Cycles :-
+ EdgeMap = partition_edges(SCC, Edges),
+ Cycles = search_for_cycles(SCC, EdgeMap).
+
+ % Builds a map from `pred_proc_id' to a list of the edges that begin
+ % with the `pred_proc_id.
+ %
+:- func partition_edges(list(abstract_ppid), edges) = map(abstract_ppid, edges).
+
+partition_edges([], _) = map.init.
+partition_edges([ProcId | SCC], Edges0) = Map :-
+ Map0 = partition_edges(SCC, Edges0),
+ Edges = list.filter((pred(Edge::in) is semidet :- ProcId = Edge ^ head), Edges0),
+ Map = map.det_insert(Map0, ProcId, Edges).
+
+:- func search_for_cycles(list(abstract_ppid), map(abstract_ppid, edges))
+ = cycles.
+
+search_for_cycles([], _) = [].
+search_for_cycles([Start | Rest], Map0) = Cycles :-
+ Cycles0 = search_for_cycles_2(Start, Map0),
+ Map = map.delete(Map0, Start),
+ Cycles1 = search_for_cycles(Rest, Map),
+ Cycles = Cycles0 ++ Cycles1.
+
+:- func search_for_cycles_2(abstract_ppid, map(abstract_ppid, edges)) = cycles.
+
+search_for_cycles_2(StartPPId, Map) = Cycles :-
+ InitialEdges = Map ^ det_elem(StartPPId),
+ list.foldl(search_for_cycles_3(StartPPId, [], Map, []), InitialEdges,
+ [], Cycles).
+
+:- pred search_for_cycles_3(abstract_ppid::in, edges::in,
+ map(abstract_ppid, edges)::in, list(abstract_ppid)::in, edge::in,
+ cycles::in, cycles::out) is det.
+
+search_for_cycles_3(Start, SoFar, Map, Visited, Edge, !Cycles) :-
+ ( Start = Edge ^ call ->
+ Cycle = cycle([Edge ^ head | Visited], [Edge | SoFar]),
+ list.cons(Cycle, !Cycles)
+ ;
+ ( MoreEdges0 = Map ^ elem(Edge ^ call) ->
+ NotVisited = (pred(E::in) is semidet :-
+ not list.member(E ^ head, Visited)
+ ),
+ MoreEdges = list.filter(NotVisited, MoreEdges0),
+ list.foldl(search_for_cycles_3(Start, [Edge | SoFar],
+ Map, [Edge ^ head | Visited]), MoreEdges,
+ !Cycles)
+ ;
+ true
+ )
+ ).
+
+%-----------------------------------------------------------------------------%
+%
+% Partitioning sets of cycles.
+%
+
+:- func partition_cycles(scc, cycles) = list(cycle_set).
+
+partition_cycles([], _) = [].
+partition_cycles([Proc | Procs], Cycles0) = CycleSets :-
+ list.filter(cycle_contains_proc(Proc), Cycles0, PCycles, Cycles1),
+ CycleSets0 = partition_cycles(Procs, Cycles1),
+ PEdges = list.map(collapse_cycle(Proc), PCycles),
+ ( if PEdges = []
+ then CycleSets = CycleSets0
+ else CycleSets = [c_set(Proc, PEdges) | CycleSets0]
+ ).
+
+:- func get_proc_from_abstract_scc(list(abstract_proc), abstract_ppid)
+ = abstract_proc.
+
+get_proc_from_abstract_scc([], _) = _ :-
+ unexpected(this_file, "Cannot find proc.").
+get_proc_from_abstract_scc([ Proc | Procs ], PPId) =
+ ( Proc ^ ppid = PPId ->
+ Proc
+ ;
+ get_proc_from_abstract_scc(Procs, PPId)
+ ).
+
+%-----------------------------------------------------------------------------%
+%
+% Termination checking.
+%
+
+% This approach is very crude. It just checks that the sum of all
+% the non-zero arguments is decreasing around all the elementary cycles.
+
+:- pred prove_termination(list(cycle_set)::in, abstract_scc::in, size_varset::in,
+ constr_termination_info::out) is det.
+
+prove_termination(Cycles, AbstractSCC, Varset, Result) :-
+ ( total_sum_decrease(AbstractSCC, Varset, Cycles) ->
+ Result = cannot_loop(analysis)
+ ;
+ % NOTE: the context here will never be used, in any
+ % case it's not clear what it should be.
+ Error = term.context_init - cond_not_satisfied,
+ Result = can_loop([Error])
+ ).
+
+:- pred total_sum_decrease(abstract_scc::in, size_varset::in,
+ list(cycle_set)::in) is semidet.
+
+total_sum_decrease(_, _, []).
+total_sum_decrease(AbstractSCC, Varset, [c_set(Start, Loops) | Cycles]):-
+ total_sum_decrease_2(AbstractSCC, Varset, Start, Loops),
+ total_sum_decrease(AbstractSCC, Varset, Cycles).
+
+:- pred total_sum_decrease_2(abstract_scc::in, size_varset::in,
+ abstract_ppid::in, list(edge)::in) is semidet.
+
+total_sum_decrease_2(_, _, _, []).
+total_sum_decrease_2(AbstractSCC, Varset, PPId, Loops @ [_|_]) :-
+ all [Loop] list.member(Loop, Loops) =>
+ strict_decrease_around_loop(AbstractSCC, Varset, PPId, Loop).
+
+ % Succeeds iff there is strict decrease in the sum of *all*
+ % the arguments around the given loop.
+ %
+:- pred strict_decrease_around_loop(abstract_scc::in, size_varset::in,
+ abstract_ppid::in, edge::in) is semidet.
+
+strict_decrease_around_loop(AbstractSCC, Varset, PPId, Loop) :-
+ ( if (PPId \= Loop ^ head ; PPId \= Loop ^ call)
+ then unexpected(this_file, "Badly formed loop.")
+ else true
+ ),
+ IsActive = (func(Var::in, Input::in) = (Var::out) is semidet :-
+ Input = yes
+ ),
+ Proc = get_proc_from_abstract_scc(AbstractSCC, PPId),
+ Inputs = Proc ^ inputs,
+ HeadArgs = list.filter_map_corresponding(IsActive, Loop ^ head_args,
+ Inputs),
+ CallArgs = list.filter_map_corresponding(IsActive, Loop ^ call_args,
+ Inputs),
+ Terms = make_coeffs(HeadArgs, -one) ++ make_coeffs(CallArgs, one),
+ %
+ % NOTE: if you examine the condition it may contain less
+ % variables than you expect. This is because if the same
+ % argument occurs in the head and the call they will cancel
+ % each other out.
+ %
+ Condition = constraint(Terms, (=<), -one),
+ Label = polyhedron.non_false_constraints(Loop ^ label),
+ entailed(Varset, Label, Condition).
+
+:- pred cycle_contains_proc(abstract_ppid::in, cycle::in) is semidet.
+
+cycle_contains_proc(PPId, cycle(Nodes, _)) :- list.member(PPId, Nodes).
+
+ % XXX Fix this name.
+:- func make_coeffs(size_vars, rat) = lp_terms.
+
+make_coeffs(Vars, Coeff) = list.map((func(Var) = Var - Coeff), Vars).
+
+%-----------------------------------------------------------------------------%
+
+ % Collapse all the cycles so that they all start with the given
+ % procedure and all the edge labels between are conjoined.
+ %
+:- func collapse_cycles(abstract_ppid, cycles) = edges.
+
+collapse_cycles(Start, Cycles) = list.map(collapse_cycle(Start), Cycles).
+
+:- func collapse_cycle(abstract_ppid, cycle) = edge.
+
+collapse_cycle(_, cycle(_, [])) = _ :-
+ unexpected(this_file, "Trying to collapse a cycle with no edges.").
+collapse_cycle(_, cycle(_, [Edge])) = Edge.
+collapse_cycle(StartPPId, cycle(_, Edges0 @ [_,_|_])) = CollapsedCycle :-
+ order_nodes(StartPPId, Edges0, Edges),
+ ( if Edges = [StartEdge0 | Rest0]
+ then StartEdge = StartEdge0, Rest = Rest0
+ else unexpected(this_file, "Error while collapsing cycles.")
+ ),
+ StartEdge = edge(_, Zeros0, HeadVars, Polyhedron0, _, CallVars0),
+ collapse_cycle_2(Rest, Zeros0, Zeros, CallVars0, CallVars, Polyhedron0,
+ Polyhedron),
+ CollapsedCycle = edge(StartPPId, Zeros, HeadVars, Polyhedron,
+ StartPPId, CallVars).
+
+:- pred collapse_cycle_2(edges::in, zero_vars::in, zero_vars::out,
+ size_vars::in, size_vars::out, polyhedron::in, polyhedron::out) is det.
+
+collapse_cycle_2([], !Zeros, !CallVars, !Polyhedron).
+collapse_cycle_2([Edge | Edges], !Zeros, !CallVars, !Polyhedron) :-
+ set.union(Edge ^ zeros, !Zeros),
+ HeadVars = Edge ^ head_args,
+ Subst0 = assoc_list.from_corresponding_lists(HeadVars, !.CallVars),
+ bimap.set_from_assoc_list(Subst0, bimap.init, Subst),
+ %
+ % We now need to substitute variables from the call to *this*
+ % predicate for head variables in both the constraints from the
+ % body of the predicate and also into the variables in the
+ % calls to the next predicate.
+ %
+ % While it might be easier to put equality constraints
+ % between the caller's arguments and the callee's head
+ % arguments the substitution is in some ways more desirable
+ % as we can detect some neutral arguments more directly.
+ %
+ !:CallVars = list.map(subst_size_var(Subst), Edge ^ call_args),
+ %
+ % These should be non-false, so throw an exception if they
+ % are not.
+ %
+ Constraints0 = polyhedron.non_false_constraints(!.Polyhedron),
+ Constraints1 = polyhedron.non_false_constraints(Edge ^ label),
+ Constraints2 = list.map(subst_size_var_eqn(Subst), Constraints1),
+ Constraints3 = Constraints0 ++ Constraints2,
+ !:Polyhedron = polyhedron.from_constraints(Constraints3),
+ collapse_cycle_2(Edges, !Zeros, !CallVars, !Polyhedron).
+
+:- pred order_nodes(abstract_ppid::in, edges::in, edges::out) is det.
+
+order_nodes(StartPPId, Edges0, [Edge | Edges]) :-
+ EdgeMap = build_edge_map(Edges0),
+ Edge = EdgeMap ^ det_elem(StartPPId),
+ order_nodes_2(StartPPId, Edge ^ call, EdgeMap, Edges).
+
+:- pred order_nodes_2(abstract_ppid::in, abstract_ppid::in,
+ map(abstract_ppid, edge)::in, edges::out) is det.
+
+order_nodes_2(StartPPId, CurrPPId, Map, Edges) :-
+ ( if StartPPId = CurrPPId
+ then Edges = []
+ else
+ Edge = Map ^ det_elem(CurrPPId),
+ order_nodes_2(StartPPId, Edge ^ call, Map, Edges0),
+ Edges = [Edge | Edges0]
+ ).
+
+:- func build_edge_map(edges) = map(abstract_ppid, edge).
+
+build_edge_map([]) = map.init.
+build_edge_map([Edge | Edges]) =
+ map.det_insert(build_edge_map(Edges), Edge ^ head, Edge).
+
+:- func subst_size_var_eqn(bimap(size_var, size_var), constraint) = constraint.
+
+subst_size_var_eqn(Map, Eqn0) = Eqn :-
+ constraint(Eqn0, Coeffs0, Operator, Constant),
+ Coeffs = list.map(subst_size_var_coeff(Map), Coeffs0),
+ Eqn = constraint(Coeffs, Operator, Constant).
+
+:- func subst_size_var_coeff(bimap(size_var, size_var), lp_term) = lp_term.
+
+subst_size_var_coeff(Map, Var0 - Coeff) = Var - Coeff :-
+ Var = subst_size_var(Map, Var0).
+
+:- func subst_size_var(bimap(size_var, size_var), size_var) = size_var.
+
+subst_size_var(Map, Old) = (if bimap.search(Map, Old, New) then New else Old).
+
+%-----------------------------------------------------------------------------%
+%
+% Predicates for printing out debugging traces.
+%
+
+:- pred write_cycles(cycles::in, module_info::in, size_varset::in,
+ io::di, io::uo) is det.
+
+write_cycles([], _, _, !IO).
+write_cycles([Cycle | Cycles], ModuleInfo, Varset, !IO) :-
+ io.write_string("Cycle in SCC:\n", !IO),
+ write_cycle(Cycle ^ nodes, ModuleInfo, !IO),
+ io.write_list(Cycle ^ edges, "\n", write_edge(ModuleInfo, Varset), !IO),
+ io.nl(!IO),
+ write_cycles(Cycles, ModuleInfo, Varset, !IO).
+
+:- pred write_cycle(list(abstract_ppid)::in, module_info::in, io::di, io::uo)
+ is det.
+
+write_cycle([], _, !IO).
+write_cycle([ Proc | Procs ], ModuleInfo, !IO) :-
+ io.write_string("\t- ", !IO),
+ Proc = real(proc(PredId, ProcId)),
+ hlds_out.write_pred_proc_id(ModuleInfo, PredId, ProcId, !IO),
+ io.nl(!IO),
+ write_cycle(Procs, ModuleInfo, !IO).
+
+:- pred write_edge(module_info::in, size_varset::in, edge::in,
+ io::di, io::uo) is det.
+
+write_edge(ModuleInfo, Varset, Edge, !IO) :-
+ io.write_string("Edge is:\n\tHead: ", !IO),
+ Edge ^ head = real(proc(PredId, ProcId)),
+ hlds_out.write_pred_proc_id(ModuleInfo, PredId, ProcId, !IO),
+ io.write_string(" : ", !IO),
+ write_size_vars(Varset, Edge ^ head_args, !IO),
+ io.write_string(" :- \n", !IO),
+ io.write_string("\tConstraints are: \n", !IO),
+ write_polyhedron(Edge ^ label, Varset, !IO),
+ io.write_string("\n\tCall is: ", !IO),
+ Edge ^ call = real(proc(CallPredId, CallProcId)),
+ hlds_out.write_pred_proc_id(ModuleInfo, CallPredId, CallProcId, !IO),
+ io.write_string(" : ", !IO),
+ write_size_vars(Varset, Edge ^ call_args, !IO),
+ io.write_string(" :- \n", !IO),
+ io.nl(!IO).
+
+%-----------------------------------------------------------------------------%
+
+:- func this_file = string.
+this_file = "term_constr_pass2.m".
+
+%-----------------------------------------------------------------------------%
+:- end_module transform_hlds.term_constr_pass2.
+%-----------------------------------------------------------------------------%
Index: compiler/term_constr_util.m
===================================================================
RCS file: compiler/term_constr_util.m
diff -N compiler/term_constr_util.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/term_constr_util.m 23 Mar 2005 23:37:14 -0000
@@ -0,0 +1,532 @@
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%------------------------------------------------------------------------------%
+% Copyright (C) 1997-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_util.m
+% Main author: juliensf
+%
+% This module defines some utility predicates used by the termination analyser.
+%
+%------------------------------------------------------------------------------%
+
+:- module transform_hlds.term_constr_util.
+
+:- interface.
+
+:- import_module hlds.hlds_pred.
+:- import_module hlds.hlds_module.
+
+:- import_module libs.lp_rational.
+:- import_module libs.polyhedron.
+
+:- import_module parse_tree.prog_data.
+
+:- import_module transform_hlds.termination2.
+:- import_module transform_hlds.term_constr_data.
+
+:- import_module bool.
+:- import_module io.
+:- import_module list.
+:- import_module map.
+:- import_module std_util.
+
+%------------------------------------------------------------------------------%
+%
+% Predicates for storing things in the HLDS.
+%
+
+ % This predicate sets the argument size info (in terms of constraints
+ % on inter-argument size relationships) of a given list of procedures.
+ %
+:- pred set_pred_proc_ids_constr_arg_size_info(list(pred_proc_id)::in,
+ constr_arg_size_info::in, module_info::in, module_info::out) is det.
+
+:- func lookup_proc_constr_arg_size_info(module_info, pred_proc_id) =
+ maybe(constr_arg_size_info).
+
+ % Retrieve the abstraction representation from the module_info.
+ %
+:- func get_abstract_scc(module_info, list(pred_proc_id)) = abstract_scc.
+
+:- func get_abstract_proc(module_info, pred_proc_id) = abstract_proc.
+
+%------------------------------------------------------------------------------%
+%
+% Predicates for size_vars.
+%
+
+ % Given a list of prog_vars, allocate one size_var per prog_var.
+ % Return the varset from which the size_vars were allocated and
+ % a map between prog_vars and size_vars.
+ %
+:- pred make_size_var_map(list(prog_var)::in, size_varset::out,
+ size_var_map::out) is det.
+
+ % Give a list of prog_vars, allocate one size_var per prog_var.
+ % Allocate the size_vars from the provided size_varset. Return
+ % a map between prog_vars and size_vars.
+ %
+:- pred make_size_var_map(list(prog_var)::in,
+ size_varset::in, size_varset::out, size_var_map::out) is det.
+
+ % Takes a list of prog_vars and outputs the corresponding
+ % list of size_vars, based on the given map.
+ %
+:- func prog_vars_to_size_vars(size_var_map, prog_vars) = size_vars.
+:- func prog_var_to_size_var(size_var_map, prog_var) = size_var.
+
+ % Returns a set containing all the size_vars corresponding to prog_vars
+ % that have a type that is always of zero size. i.e. all those for which
+ % the functor norm returns zero for all values of the type.
+ %
+:- func find_zero_size_vars(module_info, size_var_map, vartypes) = zero_vars.
+
+:- func derive_nonneg_eqns(size_var_map, zero_vars) = constraints.
+
+:- type var_substitution == map(size_var, size_var).
+
+ % compose_bijections:
+ % Takes two lists of vars of equal length, each list
+ % with a corresponding map from the vars in the list to size_vars.
+ % There is an implicit bijection between the two lists
+ % (based on the order of the lists).
+ % This predicate composes all three maps to produce a map
+ % from sizevar to sizevar (keys are the elements of the first list,
+ % values the values in the first map).
+ %
+:- func compose_bijections(size_vars, size_vars) = var_substitution.
+
+ % Create a non-negativity constraint for each size_var in the list,
+ % *except* if it has zero-size type.
+ %
+:- func make_arg_constraints(size_vars, zero_vars) = constraints.
+
+ % Check that a size_var is a member of the set of zero size_vars.
+ % XXX Ideally we would just use set.member directly but the arguments
+ % of that procedure are around the wrong way for use in most higher
+ % order procedures.
+ %
+:- pred is_zero_size_var(zero_vars::in, size_var::in) is semidet.
+
+%-----------------------------------------------------------------------------%
+
+:- pred add_context_to_constr_termination_info(
+ maybe(pragma_termination_info)::in, prog_context::in,
+ maybe(constr_termination_info)::out) is det.
+
+%------------------------------------------------------------------------------%
+
+ % substitute_size_vars: Takes a list of constraints and a
+ % var_substitution. Returns the constraints with the specified
+ % substitutions made.
+ %
+:- func substitute_size_vars(constraints, map(size_var, size_var))
+ = constraints.
+
+%------------------------------------------------------------------------------%
+%
+% Predicates for printing out debugging traces.
+%
+% In order to use these the option `--debug-term' must be set.
+
+ % Call the specified predicate.
+ %
+:- pred maybe_write_trace(pred(io, io), io, io).
+:- mode maybe_write_trace(pred(di, uo) is det, di, uo) is det.
+
+ % As above but if the boolean argument is `yes', print a newline
+ % to stdout before flushing the output.
+ %
+:- pred maybe_write_trace(pred(io, io), bool, io, io).
+:- mode maybe_write_trace(pred(di, uo) is det, in, di, uo) is det.
+
+ % Write the given string to stdout.
+ %
+:- pred maybe_write_string(string::in, io::di, io::uo) is det.
+
+ % Write a newline to stdout.
+ %
+:- pred maybe_write_nl(io::di, io::uo) is det.
+
+:- pred maybe_write_scc_procs(list(pred_proc_id)::in, module_info::in,
+ int::in, io::di, io::uo) is det.
+
+:- pred maybe_write_proc_name(pred_proc_id::in, string::in, module_info::in,
+ int::in, io::di, io::uo) is det.
+
+:- pred write_size_vars(size_varset::in, size_vars::in, io::di, io::uo) is det.
+
+:- pred dump_size_varset(size_varset::in, io::di, io::uo) is det.
+
+:- pred dump_size_vars(size_vars::in, size_varset::in, io::di, io::uo) is det.
+
+%------------------------------------------------------------------------------%
+
+:- pred update_arg_size_info(pred_proc_id::in, polyhedron::in, module_info::in,
+ module_info::out) is det.
+
+ % If Override is yes, then this predicate overrides any existing
+ % termination information. If Override is no, then it leaves the
+ % proc_info of a procedure unchanged unless the proc_info had no
+ % termination information (i.e. the maybe(termination_info)
+ % field was set to "no").
+ %
+:- pred change_procs_constr_termination_info(list(proc_id)::in, bool::in,
+ constr_termination_info::in, proc_table::in, proc_table::out) is det.
+
+ % This predicate sets the arg_size_info property of the given
+ % list of procedures. If Override is yes, then this predicate
+ % overrides any existing arg_size information. If Override is
+ % no, then it leaves the proc_info of a procedure unchanged
+ % unless the proc_info had no arg_size information (i.e. the
+ % maybe(arg_size_info) field was set to "no").
+ %
+:- pred change_procs_constr_arg_size_info(list(proc_id)::in, bool::in,
+ constr_arg_size_info::in, proc_table::in, proc_table::out) is det.
+
+:- pred all_args_input_or_zero_size(module_info::in, pred_info::in,
+ proc_info::in) is semidet.
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module check_hlds.type_util.
+:- import_module check_hlds.mode_util.
+
+:- import_module libs.options.
+:- import_module libs.globals.
+:- import_module libs.rat.
+
+:- import_module hlds.hlds_goal.
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_out.
+:- import_module hlds.hlds_pred.
+:- import_module hlds.quantification.
+
+:- import_module parse_tree.error_util.
+:- import_module parse_tree.mercury_to_mercury.
+:- import_module parse_tree.prog_type.
+
+:- import_module transform_hlds.termination2.
+:- import_module transform_hlds.term_constr_errors.
+:- import_module transform_hlds.term_norm.
+
+:- import_module int.
+:- import_module set.
+:- import_module string.
+:- import_module svmap.
+:- import_module svvarset.
+:- import_module term.
+:- import_module varset.
+
+%------------------------------------------------------------------------------%
+
+set_pred_proc_ids_constr_arg_size_info([], _ArgSize, !ModuleInfo).
+set_pred_proc_ids_constr_arg_size_info([PPId | PPIds], ArgSize, !ModuleInfo) :-
+ PPId = proc(PredId, ProcId),
+ module_info_preds(!.ModuleInfo, PredTable0),
+ PredInfo0 = PredTable0 ^ det_elem(PredId),
+ pred_info_procedures(PredInfo0, ProcTable0),
+ ProcInfo0 = ProcTable0 ^ det_elem(ProcId),
+ proc_info_get_termination2_info(ProcInfo0, TermInfo0),
+ TermInfo = TermInfo0 ^ success_constrs := yes(ArgSize),
+ proc_info_set_termination2_info(TermInfo, ProcInfo0, ProcInfo),
+ ProcTable = ProcTable0 ^ det_elem(ProcId) := ProcInfo,
+ pred_info_set_procedures(ProcTable, PredInfo0, PredInfo),
+ PredTable = PredTable0 ^ det_elem(PredId) := PredInfo,
+ module_info_set_preds(PredTable, !ModuleInfo),
+ set_pred_proc_ids_constr_arg_size_info(PPIds, ArgSize, !ModuleInfo).
+
+lookup_proc_constr_arg_size_info(ModuleInfo, PredProcId) = MaybeArgSizeInfo :-
+ PredProcId = proc(PredId, ProcId),
+ module_info_pred_proc_info(ModuleInfo, PredId, ProcId, _, ProcInfo),
+ proc_info_get_termination2_info(ProcInfo, TermInfo),
+ MaybeArgSizeInfo = TermInfo ^ success_constrs.
+
+%------------------------------------------------------------------------------%
+
+make_size_var_map(ProgVars, SizeVarset, SizeVarMap) :-
+ make_size_var_map(ProgVars, varset.init, SizeVarset, SizeVarMap).
+
+make_size_var_map(ProgVars, !SizeVarset, SizeVarMap) :-
+ list.foldl2(make_size_var_map_2, ProgVars,
+ map.init, SizeVarMap, !SizeVarset).
+
+:- pred make_size_var_map_2(prog_var::in, size_var_map::in, size_var_map::out,
+ size_varset::in, size_varset::out) is det.
+
+make_size_var_map_2(ProgVar, !SizeVarMap, !SizeVarset) :-
+ svvarset.new_var(SizeVar, !SizeVarset),
+ svmap.set(ProgVar, SizeVar, !SizeVarMap).
+
+prog_vars_to_size_vars(SizeVarMap, Vars)
+ = list.map(prog_var_to_size_var(SizeVarMap), Vars).
+
+prog_var_to_size_var(SizeVarMap, Var) = SizeVar :-
+ ( if map.search(SizeVarMap, Var, SizeVar0)
+ then SizeVar = SizeVar0
+ else unexpected(this_file,
+ "prog_var_to_size_var/2: prog_var not in size_var_map.")
+ ).
+
+find_zero_size_vars(ModuleInfo, SizeVarMap, VarTypes) = Zeros :-
+ ProgVars = map.keys(SizeVarMap),
+ ZeroProgVars = list.filter(is_zero_size_prog_var(ModuleInfo, VarTypes),
+ ProgVars),
+ %
+ % Build zeros from corresponding size_vars.
+ %
+ ZerosList = prog_vars_to_size_vars(SizeVarMap, ZeroProgVars),
+ Zeros = set.from_list(ZerosList).
+
+:- pred is_zero_size_prog_var(module_info::in, vartypes::in,
+ prog_var::in) is semidet.
+
+is_zero_size_prog_var(ModuleInfo, VarTypes, Var) :-
+ Type = VarTypes ^ det_elem(Var),
+ (
+ term_norm.zero_size_type(Type, ModuleInfo)
+ ;
+ % We don't include the io.state and store.store
+ % in the constraints - they won't tell us anything
+ % useful.
+ type_util.is_dummy_argument_type(Type)
+ ;
+ prog_type.type_is_higher_order(Type, _, _, _, _)
+ ).
+
+add_context_to_constr_termination_info(no, _, no).
+add_context_to_constr_termination_info(yes(cannot_loop(_)), _,
+ yes(cannot_loop(import_supplied))).
+add_context_to_constr_termination_info(yes(can_loop(_)), Context,
+ yes(can_loop([Context - imported_pred]))).
+
+%------------------------------------------------------------------------------%
+
+substitute_size_vars(Constraints0, SubstMap) = Constraints :-
+ SubVarInCoeff = (func(OldVar - Rat) = NewVar - Rat :-
+ NewVar = SubstMap ^ det_elem(OldVar)
+ ),
+ SubVarInEqn = (func(Constr) = constraint(Coeffs, Op, Rat) :-
+ constraint(Constr, Coeffs0, Op, Rat),
+ Coeffs = list.map(SubVarInCoeff, Coeffs0)
+ ),
+ Constraints = list.map(SubVarInEqn, Constraints0).
+
+%------------------------------------------------------------------------------%
+%
+% Utility procedures used by various parts of the IR analysis.
+%
+
+ % derive_nonneg_eqns(SizeVarMap, Zeros).
+ % Returns a list of constraints of the form "x >= 0" for every size_var
+ % x that is is in `SizeVarMap' and is not in the set `Zeros'.
+ %
+derive_nonneg_eqns(SizeVarMap, Zeros) = Eqns :-
+ derive_nonneg_eqns(SizeVarMap, Zeros, Eqns).
+
+:- pred derive_nonneg_eqns(size_var_map::in, zero_vars::in,
+ constraints::out) is det.
+
+derive_nonneg_eqns(SizeVarMap, Zeros, NonNegs) :-
+ SizeVars = map.values(SizeVarMap),
+ list.filter(isnt(is_zero_size_var(Zeros)), SizeVars, NonZeroSizeVars),
+ NonNegs = list.map(make_nonneg_constr, NonZeroSizeVars).
+
+compose_bijections(Args, HeadVars) = SubstMap :-
+ compose_bijections(Args, HeadVars, map.init, SubstMap).
+
+:- pred compose_bijections(size_vars::in, size_vars::in,
+ var_substitution::in, var_substitution::out) is det.
+
+compose_bijections([], [], !Subst).
+compose_bijections([_|_], [], _, _) :-
+ unexpected(this_file, "compose_bijections/5: unmatched lists.").
+compose_bijections([], [_|_], _, _) :-
+ unexpected(this_file, "compose_bijections/5: unmatched lists.").
+compose_bijections([Arg | Args], [HeadVar | HeadVars], !Subst) :-
+ svmap.det_insert(HeadVar, Arg, !Subst),
+ compose_bijections(Args, HeadVars, !Subst).
+
+make_arg_constraints([], _) = [].
+make_arg_constraints([Var | Vars], Zeros) = Constraints :-
+ Constraints0 = make_arg_constraints(Vars, Zeros),
+ ( if set.member(Var, Zeros)
+ then Constraints = Constraints0
+ else Constraints =
+ [ constraint([Var - one], (>=), zero) | Constraints0 ]
+ ).
+
+is_zero_size_var(Zeros, SizeVar) :- set.member(SizeVar, Zeros).
+
+%------------------------------------------------------------------------------%
+%
+% Predicates for printing out debugging traces ...
+%
+
+maybe_write_trace(TracePred, !IO) :-
+ maybe_write_trace(TracePred, no, !IO).
+
+maybe_write_trace(TracePred, NewLine, !IO) :-
+ globals.io_lookup_bool_option(debug_term, Trace, !IO),
+ (
+ Trace = yes,
+ TracePred(!IO),
+ ( if NewLine = yes then io.nl(!IO) else true ),
+ io.flush_output(!IO)
+ ;
+ Trace = no
+ ).
+
+maybe_write_nl(!IO) :- maybe_write_string("\n", !IO).
+
+maybe_write_string(String, !IO) :-
+ globals.io_lookup_bool_option(debug_term, Debug, !IO),
+ (
+ Debug = yes,
+ io.write_string(String, !IO),
+ io.flush_output(!IO)
+ ;
+ Debug = no
+ ).
+
+maybe_write_scc_procs(SCC, ModuleInfo, _, !IO) :-
+ write_scc_procs_2(SCC, ModuleInfo, !IO),
+ io.nl(!IO).
+
+:- pred write_scc_procs_2(list(pred_proc_id)::in, module_info::in,
+ io::di, io::uo) is det.
+
+write_scc_procs_2([], _, !IO).
+write_scc_procs_2([PPId | PPIds], ModuleInfo, !IO) :-
+ io.write_char('\t', !IO),
+ hlds_out.write_pred_proc_id(ModuleInfo, PPId, !IO),
+ io.nl(!IO),
+ write_scc_procs_2(PPIds, ModuleInfo, !IO).
+
+maybe_write_proc_name(PPId, String, ModuleInfo, _, !IO) :-
+ io.write_string(String, !IO),
+ hlds_out.write_pred_proc_id(ModuleInfo, PPId, !IO),
+ io.nl(!IO).
+
+write_size_vars(Varset, Vars, !IO) :-
+ WriteSizeVar = (pred(Var::in, !.IO::di, !:IO::uo) is det :-
+ varset.lookup_name(Varset, Var, Name),
+ io.write_string(Name, !IO)
+ ),
+ io.write_char('[', !IO),
+ io.write_list(Vars, ", ", WriteSizeVar, !IO),
+ io.write_char(']', !IO).
+
+%------------------------------------------------------------------------------%
+
+dump_size_vars(Vars, Varset, !IO) :-
+ dump_size_varset_2(Vars, Varset, !IO).
+
+dump_size_varset(Varset, !IO) :-
+ Vars = varset.vars(Varset),
+ dump_size_varset_2(Vars, Varset, !IO).
+
+:- pred dump_size_varset_2(size_vars::in, size_varset::in, io::di, io::uo)
+ is det.
+
+dump_size_varset_2([], _, !IO).
+dump_size_varset_2([Var | Vars], Varset, !IO) :-
+ Name = varset.lookup_name(Varset, Var),
+ io.write(Var, !IO),
+ io.format(" = %s\n", [s(Name)], !IO),
+ dump_size_varset_2(Vars, Varset, !IO).
+
+%------------------------------------------------------------------------------%
+
+update_arg_size_info(PPID, Polyhedron, !ModuleInfo) :-
+ set_pred_proc_ids_constr_arg_size_info([PPID], Polyhedron,
+ !ModuleInfo).
+
+%------------------------------------------------------------------------------%
+
+change_procs_constr_termination_info([], _, _, !ProcTable).
+change_procs_constr_termination_info([ProcId | ProcIds], Override, Termination,
+ !ProcTable) :-
+ ProcInfo0 = !.ProcTable ^ det_elem(ProcId),
+ proc_info_get_termination2_info(ProcInfo0, TermInfo0),
+ ( (Override = yes ; TermInfo0 ^ term_status = no) ->
+ TermInfo = TermInfo0 ^ term_status := yes(Termination),
+ proc_info_set_termination2_info(TermInfo, ProcInfo0, ProcInfo),
+ svmap.det_update(ProcId, ProcInfo, !ProcTable)
+ ;
+ true
+ ),
+ change_procs_constr_termination_info(ProcIds, Override, Termination,
+ !ProcTable).
+
+change_procs_constr_arg_size_info([], _, _, !ProcTable).
+change_procs_constr_arg_size_info([ProcId | ProcIds], Override, ArgSize,
+ !ProcTable) :-
+ ProcInfo0 = !.ProcTable ^ det_elem(ProcId),
+ proc_info_get_termination2_info(ProcInfo0, TermInfo0),
+ ( (Override = yes ; TermInfo0 ^ success_constrs = no) ->
+ TermInfo = TermInfo0 ^ success_constrs := yes(ArgSize),
+ proc_info_set_termination2_info(TermInfo, ProcInfo0, ProcInfo),
+ svmap.det_update(ProcId, ProcInfo, !ProcTable)
+ ;
+ true
+ ),
+ change_procs_constr_arg_size_info(ProcIds, Override, ArgSize,
+ !ProcTable).
+
+all_args_input_or_zero_size(ModuleInfo, PredInfo, ProcInfo) :-
+ pred_info_arg_types(PredInfo, TypeList),
+ proc_info_argmodes(ProcInfo, ModeList),
+ all_args_input_or_zero_size_2(TypeList, ModeList, ModuleInfo).
+
+:- pred all_args_input_or_zero_size_2(list(type)::in, list(mode)::in,
+ module_info::in) is semidet.
+
+all_args_input_or_zero_size_2([], [], _).
+all_args_input_or_zero_size_2([], [_|_], _) :-
+ unexpected(this_file,
+ "all_args_input_or_zero_size_2/3: unmatched lists.").
+all_args_input_or_zero_size_2([_|_], [], _) :-
+ unexpected(this_file,
+ "all_args_input_or_zero_size_2/3: unmatched lists.").
+all_args_input_or_zero_size_2([Type | Types], [Mode | Modes], ModuleInfo) :-
+ ( mode_util.mode_is_input(ModuleInfo, Mode) ->
+ all_args_input_or_zero_size_2(Types, Modes, ModuleInfo)
+ ;
+ term_norm.zero_size_type(Type, ModuleInfo),
+ all_args_input_or_zero_size_2(Types, Modes, ModuleInfo)
+ ).
+
+%----------------------------------------------------------------------------%
+
+get_abstract_scc(ModuleInfo, SCC) =
+ list.map(get_abstract_proc(ModuleInfo), SCC).
+
+get_abstract_proc(ModuleInfo, PPId) = AbstractProc :-
+ module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
+ proc_info_get_termination2_info(ProcInfo, TermInfo),
+ MaybeAbstractProc = TermInfo ^ abstract_rep,
+ (
+ MaybeAbstractProc = yes(AbstractProc)
+ ;
+ MaybeAbstractProc = no,
+ unexpected(this_file,
+ "get_abstract_proc/2: no abstract rep. for proc.")
+ ).
+
+%------------------------------------------------------------------------------%
+
+:- func this_file = string.
+
+this_file = "term_constr_util.m".
+
+%------------------------------------------------------------------------------%
+:- end_module term_constr_util.
+%------------------------------------------------------------------------------%
Index: compiler/term_norm.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_norm.m,v
retrieving revision 1.7
diff -u -r1.7 term_norm.m
--- compiler/term_norm.m 22 Mar 2005 06:40:28 -0000 1.7
+++ compiler/term_norm.m 22 Mar 2005 22:04:36 -0000
@@ -25,27 +25,45 @@
%-----------------------------------------------------------------------------%
-% The functor_info type contains information about how the weight of a term
-% is calculated.
-
+ % The functor_info type contains information about how the weight
+ % of a term is calculated.
+ %
:- type functor_info.
-% This predicate sets the functor_info depending on the value of the
-% termination_norm option.
-
-:- pred set_functor_info(globals__termination_norm::in, module_info::in,
- functor_info::out) is det.
-
-% This predicate computes the weight of a functor and the set of arguments
-% of that functor whose sizes should be counted towards the size of the whole
-% term.
-
+ % This predicate sets the functor_info depending on the value of the
+ % termination_norm or termination2_norm option.
+ %
+:- func set_functor_info(globals.termination_norm, module_info) = functor_info.
+
+ % This predicate computes the weight of a functor and the set of
+ % arguments of that functor whose sizes should be counted towards the
+ % size of the whole term.
+ %
+ % NOTE: the list of arguments and the list of modes must be the
+ % same length. They must also *not* contain any type-info
+ % related arguments as this may cause an exception to be thrown
+ % when using the `--num-data-elems' norm. (This is because the
+ % weight table doesn't keep track of type-info related variables
+ % - it used to but intervening compiler passes tend to do things
+ % to the code in the mean time so the whole lot becomes
+ % inconsistent - in the end it's just easier to ignore them).
+ %
:- pred functor_norm(functor_info::in, type_ctor::in, cons_id::in,
module_info::in, int::out, list(prog_var)::in, list(prog_var)::out,
list(uni_mode)::in, list(uni_mode)::out) is det.
-% Succeeds if all values of the given type are zero size (for all norms).
-
+ % This function computes a lower bound on the weight of a fuctor.
+ % If the lower bound is zero then the weight of that functor is
+ % also zero. If the lower bound is non-zero then there may be
+ % no upper bound on the size of the functor. (And if there was
+ % this function wouldn't tell you about it anyhow).
+ %
+:- func functor_lower_bound(functor_info, type_ctor, cons_id, module_info)
+ = int.
+
+ % Succeeds if all values of the given type are zero size
+ % (for all norms).
+ %
:- pred zero_size_type((type)::in, module_info::in) is semidet.
%-----------------------------------------------------------------------------%
@@ -58,6 +76,7 @@
:- import_module check_hlds__type_util.
:- import_module hlds__hlds_data.
:- import_module libs__options.
+:- import_module parse_tree__error_util.
:- import_module parse_tree__prog_out.
:- import_module parse_tree__prog_type.
@@ -66,6 +85,7 @@
:- import_module map.
:- import_module require.
:- import_module std_util.
+:- import_module string.
%-----------------------------------------------------------------------------%
@@ -226,11 +246,11 @@
%-----------------------------------------------------------------------------%
-set_functor_info(total, _Module, total).
-set_functor_info(simple, _Module, simple).
-set_functor_info(num_data_elems, Module, use_map_and_args(WeightMap)) :-
+set_functor_info(total, _Module) = total.
+set_functor_info(simple, _Module) = simple.
+set_functor_info(num_data_elems, Module) = use_map_and_args(WeightMap) :-
find_weights(Module, WeightMap).
-set_functor_info(size_data_elems, Module, use_map(WeightMap)) :-
+set_functor_info(size_data_elems, Module) = use_map(WeightMap) :-
find_weights(Module, WeightMap).
%-----------------------------------------------------------------------------%
@@ -268,14 +288,14 @@
->
true
;
- error("Unmatched lists in functor_norm_filter_args.")
+ unexpected(this_file, "Unmatched lists in " ++
+ "functor_norm_filter_args.")
)
;
Int = 0
).
% This predicate will fail if the length of the input lists are not matched.
-
:- pred functor_norm_filter_args(list(bool)::in, list(prog_var)::in,
list(prog_var)::out, list(uni_mode)::in, list(uni_mode)::out)
is semidet.
@@ -290,8 +310,26 @@
%-----------------------------------------------------------------------------%
+functor_lower_bound(simple, _, ConsId, _) =
+ ( if ConsId = cons(_, Arity), Arity \= 0 then 1 else 0).
+functor_lower_bound(total, _, ConsId, _) =
+ ( if ConsId = cons(_, Arity) then Arity else 0 ).
+functor_lower_bound(use_map(WeightMap), TypeCtor, ConsId, _) = Weight :-
+ ( if search_weight_table(WeightMap, TypeCtor, ConsId, WeightInfo)
+ then WeightInfo = weight(Weight, _)
+ else Weight = 0
+ ).
+functor_lower_bound(use_map_and_args(WeightMap), TypeCtor, ConsId, _)
+ = Weight :-
+ ( if search_weight_table(WeightMap, TypeCtor, ConsId, WeightInfo)
+ then WeightInfo = weight(Weight, _)
+ else Weight = 0
+ ).
+
+%-----------------------------------------------------------------------------%
+
zero_size_type(Type, Module) :-
- classify_type(Module, Type) = TypeCategory,
+ type_util.classify_type(Module, Type) = TypeCategory,
zero_size_type_category(TypeCategory, yes).
:- pred zero_size_type_category(type_category::in, bool::out) is det.
@@ -312,5 +350,11 @@
zero_size_type_category(user_ctor_type, no).
%-----------------------------------------------------------------------------%
-:- end_module transform_hlds__term_norm.
+
+:- func this_file = string.
+
+this_file = "term_norm.m".
+
+%-----------------------------------------------------------------------------%
+:- end_module term_norm.
%-----------------------------------------------------------------------------%
Index: compiler/term_pass2.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_pass2.m,v
retrieving revision 1.18
diff -u -r1.18 term_pass2.m
--- compiler/term_pass2.m 22 Mar 2005 06:40:28 -0000 1.18
+++ compiler/term_pass2.m 22 Mar 2005 06:49:36 -0000
@@ -103,12 +103,12 @@
prove_termination_in_scc_single_arg(SCC,
Module, PassInfo)
->
- Termination = cannot_loop
+ Termination = cannot_loop(unit)
;
Termination = Termination1
)
;
- Termination1 = cannot_loop,
+ Termination1 = cannot_loop(unit),
Termination = Termination1
).
@@ -202,7 +202,7 @@
ArgNum0, Module, InitRecSuppliers),
prove_termination_in_scc_trial([TrialPPId | RestSCC], InitRecSuppliers,
up, Module, PassInfo, Termination),
- ( Termination = cannot_loop ->
+ ( Termination = cannot_loop(unit) ->
true
;
ArgNum1 = ArgNum0 + 1,
@@ -306,7 +306,7 @@
list__take_upto(MaxErrors, Cycles, ReportedCycles),
Termination = can_loop(ReportedCycles)
;
- Termination = cannot_loop
+ Termination = cannot_loop(unit)
)
;
Result = error(Errors),
Index: compiler/term_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_util.m,v
retrieving revision 1.40
diff -u -r1.40 term_util.m
--- compiler/term_util.m 24 Mar 2005 02:00:31 -0000 1.40
+++ compiler/term_util.m 24 Mar 2005 02:26:59 -0000
@@ -56,7 +56,7 @@
generic_arg_size_info(list(term_errors__error)).
:- type termination_info ==
- generic_termination_info(list(term_errors__error)).
+ generic_termination_info(unit, list(term_errors__error)).
% The type `used_args' holds a mapping which specifies for each procedure
% which of its arguments are used.
@@ -345,9 +345,10 @@
%-----------------------------------------------------------------------------%
add_context_to_termination_info(no, _, no).
-add_context_to_termination_info(yes(cannot_loop), _, yes(cannot_loop)).
+add_context_to_termination_info(yes(cannot_loop(_)), _,
+ yes(cannot_loop(unit))).
add_context_to_termination_info(yes(can_loop(_)), Context,
- yes(can_loop([Context - imported_pred]))).
+ yes(can_loop([Context - imported_pred]))).
add_context_to_arg_size_info(no, _, no).
add_context_to_arg_size_info(yes(finite(A, B)), _, yes(finite(A, B))).
Index: compiler/termination.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/termination.m,v
retrieving revision 1.50
diff -u -r1.50 termination.m
--- compiler/termination.m 22 Mar 2005 06:40:28 -0000 1.50
+++ compiler/termination.m 22 Mar 2005 06:49:36 -0000
@@ -114,7 +114,7 @@
% Find out what norm we should use, and set up for using it
globals__io_get_termination_norm(TermNorm, !IO),
- set_functor_info(TermNorm, !.Module, FunctorInfo),
+ FunctorInfo = set_functor_info(TermNorm, !.Module),
globals__io_lookup_int_option(termination_error_limit, MaxErrors, !IO),
globals__io_lookup_int_option(termination_path_limit, MaxPaths, !IO),
PassInfo = pass_info(FunctorInfo, MaxErrors, MaxPaths),
@@ -186,7 +186,8 @@
MaybeTermination = no,
( attributes_imply_termination(Attributes) ->
proc_info_set_maybe_termination_info(
- yes(cannot_loop), ProcInfo0, ProcInfo)
+ yes(cannot_loop(unit)),
+ ProcInfo0, ProcInfo)
;
TermErr = Context - does_not_term_foreign(PPId),
proc_info_set_maybe_termination_info(
@@ -197,7 +198,7 @@
% If there was a `pragma terminates' declaration
% for this procedure then check that the foreign
% code attributes do not contradict this.
- MaybeTermination = yes(cannot_loop),
+ MaybeTermination = yes(cannot_loop(_)),
( terminates(Attributes) = does_not_terminate ->
TermErr = Context - inconsistent_annotations,
proc_info_set_maybe_termination_info(
@@ -344,8 +345,8 @@
MaybeTerm = yes(PPIdStatus)
),
(
- Status = cannot_loop,
- PPIdStatus = cannot_loop
+ Status = cannot_loop(_),
+ PPIdStatus = cannot_loop(_)
;
Status = can_loop(_),
PPIdStatus = can_loop(_)
@@ -620,7 +621,7 @@
->
( check_marker(Markers, terminates) ->
change_procs_termination_info(ProcIds, yes,
- cannot_loop, ProcTable0, ProcTable2)
+ cannot_loop(unit), ProcTable0, ProcTable2)
;
ProcTable2 = ProcTable0
)
@@ -644,7 +645,7 @@
)
->
change_procs_termination_info(ProcIds, yes,
- cannot_loop, ProcTable0, ProcTable1)
+ cannot_loop(unit), ProcTable0, ProcTable1)
;
TerminationError = Context - imported_pred,
TerminationInfo = can_loop([TerminationError]),
@@ -742,15 +743,15 @@
special_pred_id_to_termination(compare, HeadVars, ArgSize, Termination) :-
term_util__make_bool_list(HeadVars, [no, no, no], OutList),
ArgSize = finite(0, OutList),
- Termination = cannot_loop.
+ Termination = cannot_loop(unit).
special_pred_id_to_termination(unify, HeadVars, ArgSize, Termination) :-
term_util__make_bool_list(HeadVars, [yes, yes], OutList),
ArgSize = finite(0, OutList),
- Termination = cannot_loop.
+ Termination = cannot_loop(unit).
special_pred_id_to_termination(index, HeadVars, ArgSize, Termination) :-
term_util__make_bool_list(HeadVars, [no, no], OutList),
ArgSize = finite(0, OutList),
- Termination = cannot_loop.
+ Termination = cannot_loop(unit).
special_pred_id_to_termination(initialise, _, _, _) :-
unexpected(this_file, "special_pred_id_to_termination/4 " ++
"initialise predicate").
@@ -778,8 +779,8 @@
ArgSizeInfo = yes(infinite([Context - Error]))
),
proc_info_set_maybe_arg_size_info(ArgSizeInfo, ProcInfo0, ProcInfo1),
- proc_info_set_maybe_termination_info(yes(cannot_loop), ProcInfo1,
- ProcInfo),
+ proc_info_set_maybe_termination_info(yes(cannot_loop(unit)),
+ ProcInfo1, ProcInfo),
map__det_update(!.ProcTable, ProcId, ProcInfo, !:ProcTable),
set_builtin_terminates(ProcIds, PredId, PredInfo, Module, !ProcTable).
Index: compiler/termination2.m
===================================================================
RCS file: compiler/termination2.m
diff -N compiler/termination2.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/termination2.m 24 Mar 2005 04:17:13 -0000
@@ -0,0 +1,736 @@
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%-----------------------------------------------------------------------------%
+% Copyright (C) 1997,2002-2005 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: termination2.m
+% main author: juliensf
+%
+% This module contains the top level of a termination analyser for Mercury.
+% It is responsible for setting up the relevant data structures and invoking
+% all the other passes.
+%
+% --------
+% Overview
+% --------
+%
+% The main data structures used by this analysis are defined in
+% term_constr_data.m.
+%
+% The analysis is carried out in three passes:
+%
+% * Pass 0 - Setup information for builtin predicates and process any
+% information from user annotations like termination pragmas and
+% foreign proc. attributes. Also, set up information imported from
+% `.opt' and `.trans_opt' files. (See term_constr_initial.m.)
+%
+% Each of passes 1 and 2 are run consecutively on each SCC of the
+% program call-graph. This is done in bottom-up order.
+%
+% * Pass 1 - Interargument size relationship (IR) analysis.
+%
+% (a) Convert HLDS to the abstract representation (AR) defined
+% in term_constr_data.m. (See term_constr_build.m.)
+%
+% (b) Perform fixpoint calculation to derive IR information.
+% ( See term_constr_fixpoint.m.)
+%
+% * Pass 2 - Termination.
+% Use the information from pass 1 to attempt to find a proof that the
+% procedures in a SCC terminate.
+% There is an example of such a proof finder in term_constr_pass2.m,
+% although we will probably end up with several such modules, each
+% of which tries a different approach.
+%
+% In addition there are some utility procedures in term_constr_util.m
+% and some predicates for handling error messages in term_constr_error.m.
+%
+% The machinery for handling convex constraints (polyhedra) is in:
+%
+% * polyhedron.m
+% * lp_rational.m
+% * rat.m
+%
+% TODO:
+% * add support for higher-order code and intermodule
+% mutual recursion.
+%
+% * add support for user-defined IR constraints for foreign
+% code, :- pragma arg_size_relation(...) or something.
+%
+% * experiment with different types of widening.
+%
+% * experiment with different representation for the polyhedra.
+%
+%----------------------------------------------------------------------------%
+
+:- module transform_hlds.termination2.
+
+:- interface.
+
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_pred.
+
+:- import_module parse_tree.prog_data.
+
+:- import_module libs.polyhedron.
+
+:- import_module mdbcomp.prim_data.
+
+:- import_module transform_hlds.term_constr_data.
+:- import_module transform_hlds.term_constr_errors.
+
+:- import_module io.
+:- import_module list.
+:- import_module std_util.
+
+%----------------------------------------------------------------------------%
+%
+% Types that define termination information about procedures.
+%
+
+ % This type is the interargument size relationships between
+ % the arguments of a predicate.
+ %
+:- type constr_arg_size_info == polyhedron.
+
+ % Whether or not a procedure is terminating and some idea of why
+ % this is or is not the case.
+ %
+:- type constr_termination_info ==
+ generic_termination_info(term_reason, term2_errors).
+
+ % Why does the termination analyser think that a procedure is
+ % terminating? This is useful for debugging purposes.
+ %
+:- type term_reason
+ ---> builtin % procedure was a builtin.
+
+ ; pragma_supplied % procedure has pramga terminates decl.
+
+ ; foreign_supplied % procedure has foreign code attribute.
+
+ ; import_supplied % This procedure was imported and it's
+ % termination info. was read in from a .opt
+ % or .trans_opt file.
+
+ ; analysis. % Termination info. was derived via analysis.
+
+ % Whether a procedure may be involved in mutual recursion
+ % across module boundaries.
+ %
+ % XXX Termination analysis of mutual recursion across module boundaries
+ % NYI.
+ %
+:- type intermod_status
+ ---> not_mutually_recursive
+ ; may_be_mutually_recursive.
+
+%----------------------------------------------------------------------------%
+%
+% The `termination2_info' structure.
+%
+
+% All the information needed by the termination analysis is stored in
+% this structure. There is one such structure attached to every
+% procedure in the module.
+
+:- type termination2_info.
+
+:- func term2_info_init = termination2_info.
+
+:- func termination2_info ^ size_var_map = size_var_map.
+:- func termination2_info ^ import_headvarids = maybe(list(int)).
+:- func termination2_info ^ import_success =
+ maybe(pragma_constr_arg_size_info).
+:- func termination2_info ^ import_failure =
+ maybe(pragma_constr_arg_size_info).
+:- func termination2_info ^ success_constrs = maybe(constr_arg_size_info).
+:- func termination2_info ^ failure_constrs = maybe(constr_arg_size_info).
+:- func termination2_info ^ term_status = maybe(constr_termination_info).
+:- func termination2_info ^ abstract_rep = maybe(abstract_proc).
+:- func termination2_info ^ intermod_status = maybe(intermod_status).
+:- func termination2_info ^ head_vars = list(size_var).
+
+:- func termination2_info ^ size_var_map := size_var_map = termination2_info.
+:- func termination2_info ^ import_headvarids := maybe(list(int)) =
+ termination2_info.
+:- func termination2_info ^ import_success :=
+ maybe(pragma_constr_arg_size_info) = termination2_info.
+:- func termination2_info ^ import_failure :=
+ maybe(pragma_constr_arg_size_info) = termination2_info.
+:- func termination2_info ^ success_constrs := maybe(constr_arg_size_info)
+ = termination2_info.
+:- func termination2_info ^ failure_constrs := maybe(constr_arg_size_info)
+ = termination2_info.
+:- func termination2_info ^ term_status := maybe(constr_termination_info)
+ = termination2_info.
+:- func termination2_info ^ intermod_status := maybe(intermod_status)
+ = termination2_info.
+:- func termination2_info ^ abstract_rep := maybe(abstract_proc)
+ = termination2_info.
+:- func termination2_info ^ head_vars := list(size_var)
+ = termination2_info.
+
+%----------------------------------------------------------------------------%
+%
+% Termination analysis.
+%
+
+ % Perform termination analysis on a module.
+ %
+:- pred termination2.pass(module_info::in, module_info::out, io::di, io::uo)
+ is det.
+
+:- pred termination2.output_maybe_constr_arg_size_info(
+ maybe(constr_arg_size_info)::in, io::di, io::uo) is det.
+
+:- pred termination2.output_maybe_termination2_info(
+ maybe(constr_termination_info)::in, io::di, io::uo) is det.
+
+ % Write out a termination2_info pragma for the predicate if:
+ % - it is exported.
+ % - it is not compiler generated.
+ %
+:- pred termination2.output_pred_termination2_info(module_info::in,
+ pred_id::in, io::di, io::uo) is det.
+
+ % This predicate outputs termination_info pragmas;
+ % such annotations can be part of .opt and .trans_opt files.
+ %
+:- pred termination2.output_pragma_termination2_info(pred_or_func::in,
+ sym_name::in, list(mode)::in, prog_context::in,
+ maybe(constr_arg_size_info)::in, maybe(constr_arg_size_info)::in,
+ maybe(constr_termination_info)::in, size_vars::in, 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.rat.
+
+:- 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.dependency_graph.
+:- import_module transform_hlds.term_constr_build.
+:- import_module transform_hlds.term_constr_data.
+:- import_module transform_hlds.term_constr_errors.
+:- import_module transform_hlds.term_constr_fixpoint.
+:- import_module transform_hlds.term_constr_initial.
+:- import_module transform_hlds.term_constr_pass2.
+:- import_module transform_hlds.term_constr_util.
+:- import_module transform_hlds.term_norm.
+
+:- import_module bool.
+:- import_module char.
+:- import_module int.
+:- import_module map.
+:- import_module set.
+:- import_module string.
+:- import_module term.
+:- import_module varset.
+
+%------------------------------------------------------------------------------%
+%
+% The termination2_info structure.
+%
+
+:- type termination2_info
+ ---> term2_info(
+ size_var_map :: size_var_map,
+ % Map between prog_vars and size_vars.
+ % Each procedure should have one of these.
+
+ head_vars :: list(size_var),
+ % These are the size variables that occur in argument
+ % size constraints. For procedures that are imported
+ % via a `.opt' or `.trans_opt' file we set these during
+ % the initial pass, for procedures in the module we are
+ % analysing, pass 1 sets it.
+
+ import_headvarids :: maybe(list(int)),
+ import_success :: maybe(pragma_constr_arg_size_info),
+ import_failure :: maybe(pragma_constr_arg_size_info),
+ % Arg size info. imported from another module via a
+ % `.opt' or `.trans_opt' file. The preprocessing pass
+ % needs to convert these to the proper form. These
+ % particular fields are of no use after that.
+
+ success_constrs :: maybe(constr_arg_size_info),
+ % The interargument size relationships
+ % (expressed as convex constraints)
+ % obtained during pass 1.
+
+ failure_constrs :: maybe(constr_arg_size_info),
+ % Failure constraints for predicates that
+ % can fail (set by pass 1).
+
+ term_status :: maybe(constr_termination_info),
+ % The termination status of the procedure as determined
+ % by pass 2.
+
+ intermod_status :: maybe(intermod_status),
+ % Is this procedure (possibly) involved in mutual
+ % recursion across module boundaries. Set by pass 1.
+
+ abstract_rep :: maybe(abstract_proc)
+ % The abstract representation of this
+ % proc. Set by term_constr_build.m.
+ ).
+
+term2_info_init = term2_info(map.init, [], no, no, no, no, no, no, no, no).
+
+%----------------------------------------------------------------------------%
+%
+% Main pass.
+%
+
+% The analysis proceeds as follows:
+%
+% * Preprocess the module:
+% - setup information from termination pragmas
+% - setup information from foreign proc attributes
+% - setup information about imported procedures
+% - setup termination information for builtin predicates
+%
+% * Analyse the module - process SCCs bottom-up.
+%
+% * Optionally write out termination information to the `.opt' and
+% `.trans_opt' files.
+%
+
+termination2.pass(!ModuleInfo, !IO) :-
+ %
+ % Get options required by the build pass.
+ % These are:
+ % - which norm we are using.
+ % - whether we are propagating failure constraints.
+ %
+ globals.io_get_termination2_norm(Norm, !IO),
+ FunctorInfo = term_norm.set_functor_info(Norm, !.ModuleInfo),
+ globals.io_lookup_bool_option(propagate_failure_constrs, Fail, !IO),
+ globals.io_lookup_bool_option(arg_size_analysis_only, ArgSizeOnly,
+ !IO),
+ BuildOptions = build_options_init(FunctorInfo, Fail, ArgSizeOnly),
+ %
+ % Get options required by the fixpoint pass.
+ % These are:
+ % - what cutoff value we are using
+ % - the maximum allowable matrix size
+ % (this is also used in pass 2).
+ %
+ globals.io_lookup_int_option(term2_maximum_matrix_size, MaxSize, !IO),
+ globals.io_lookup_int_option(widening_limit, CutOff, !IO),
+ %
+ % NOTE: we may eventually allow other types of widening.
+ %
+ Widening = after_fixed_cutoff(CutOff),
+ FixpointOptions = fixpoint_options_init(Widening, MaxSize),
+ %
+ % Get options required by pass 2.
+ % Currently this is just the maximum matrix size.
+ %
+ Pass2Options = pass2_options_init(MaxSize),
+ %
+ % Setup termination information for builtins and compiler generated
+ % predicates. Setup information from termination pragmas and
+ % foreign proc attributes.
+ %
+ term_constr_initial.preprocess_module(!ModuleInfo, !IO),
+ %
+ % Analyse the module per SCC in bottom-up fashion.
+ %
+ module_info_ensure_dependency_info(!ModuleInfo),
+ module_info_dependency_info(!.ModuleInfo, DepInfo),
+ hlds_dependency_info_get_dependency_ordering(DepInfo, SCCs),
+ list.foldl2(
+ analyse_scc(SCCs, BuildOptions, FixpointOptions, Pass2Options),
+ SCCs, !ModuleInfo, !IO),
+ %
+ % Write `.opt' and `.trans_opt' files.
+ %
+ maybe_make_optimization_interface(!.ModuleInfo, !IO).
+
+%----------------------------------------------------------------------------%
+%
+% Analyse a single SCC.
+%
+
+ % Analyse a single SCC of the call graph. This will require results
+ % concerning SCCs lower down the call graph.
+ %
+ % The normal procedure for analysing a SCC is:
+ %
+ % (1) Build the abstract representation (AR) of the procedures in
+ % the SCC. (term_constr_build.m).
+ %
+ % (2) Use a fixpoint iteration to derive interargument size
+ % relationships for the procedures in the SCC.
+ % (term_constr_fixpoint.m).
+ %
+ % (3) Use this information to try and find a proof that the procedures
+ % in the SCC terminate. (term_constr_pass2.m).
+ %
+ % Exactly which of the above steps gets carried out depends upon
+ % what (if any) additional information the user has supplied.
+ %
+ % For Mercury procedures:
+ % If the procedure is marked as terminating/non-terminating, we
+ % still carry out steps (1) and (2). If a procedure has been
+ % supplied with an argument size constraint we carry out steps (1)
+ % and (3). If both have been supplied we do not carry out any
+ % steps.
+ %
+ % The usual caveats regarding the termination pragmas and mutual
+ % recursion apply (see the reference manual).
+ %
+ % XXX What do we do about pragma arg_size_info and mutual recursion?
+ % (Nothing yet, because it isn't implemented :-( )
+ %
+ % For procedures implemented as foreign code:
+ % The usual defaults (see reference manual) apply.
+ % If no argument size constraint is supplied then non-zero arguments
+ % are assumed to have unbounded size.
+ %
+:- pred analyse_scc(dependency_ordering::in, build_options::in,
+ fixpoint_options::in, pass2_options::in,
+ list(pred_proc_id)::in, module_info::in, module_info::out, io::di,
+ io::uo) is det.
+
+analyse_scc(DepOrder, BuildOpts, FixpointOpts, Pass2Opts, SCC, !ModuleInfo,
+ !IO) :-
+ %
+ % Since all of the passes are potentially optional we need to
+ % initialise the size_var_maps separately. If they are left
+ % uninitialised intermodule optimization will not work.
+ %
+ NeedsAR = list.filter(proc_needs_ar_built(!.ModuleInfo), SCC),
+ %
+ % Build the abstract representation for those procedures that
+ % require it. (those that do not already have both arg_size_info and
+ % termination info).
+ %
+ term_constr_build.build_abstract_scc(DepOrder, NeedsAR, BuildOpts,
+ BuildErrors, !ModuleInfo, !IO),
+ %
+ % We only perform the fixpoint computation for those procedures
+ % where we can gain meaningful information from it. We do not
+ % do it when:
+ % - the information is already known.
+ % - the argument size relationships depend upon higher-order calls.
+ %
+ NeedsArgSize = list.filter(isnt(has_arg_size_info(!.ModuleInfo)),
+ NeedsAR),
+ term_constr_fixpoint.do_fixpoint_calculation(FixpointOpts,
+ NeedsArgSize, 1, FixpointErrors, !ModuleInfo, !IO),
+ %
+ % Errors detected during pass 1 always result in the rest of the
+ % analysis being aborted for the SCC under consideration.
+ %
+ Pass1Errors = BuildErrors ++ FixpointErrors,
+ Pass1Result = ( if Pass1Errors = [] then ok else error(Pass1Errors) ),
+ globals.io_lookup_bool_option(arg_size_analysis_only, ArgSizeOnly,
+ !IO),
+ (
+ ArgSizeOnly = no
+ ->
+ NeedsTerm = list.filter(isnt(has_term_info(!.ModuleInfo)),
+ NeedsAR),
+ %
+ % Some procedures may not have arg_size_info, but
+ % may have termination info, i.e. those that have
+ % a pragma terminates or does_not_terminate declaration.
+ %
+ ( Pass1Result = error(Pass1Errors) ->
+ Pass2Result = can_loop(Pass1Errors)
+ ;
+ term_constr_pass2.prove_termination_in_scc(Pass2Opts,
+ NeedsTerm, !.ModuleInfo, Pass2Result, !IO)
+ ),
+ %
+ % Set the termination property for this procedure and
+ % report any errors that we found during pass 2.
+ %
+ set_termination_info_for_procs(NeedsTerm, Pass2Result,
+ !ModuleInfo),
+ ( Pass2Result = can_loop(Errors) ->
+ report_termination2_errors(NeedsTerm, Errors,
+ !ModuleInfo, !IO)
+ ;
+ true
+ )
+ ;
+ true
+ ).
+
+%------------------------------------------------------------------------------%
+%
+% Procedures for storing termination2_info in the HLDS.
+%
+
+:- pred set_termination_info_for_procs(list(pred_proc_id)::in,
+ constr_termination_info::in, module_info::in, module_info::out) is det.
+
+set_termination_info_for_procs(PPIds, TerminationInfo, !ModuleInfo) :-
+ list.foldl(set_termination_info_for_proc(TerminationInfo), PPIds,
+ !ModuleInfo).
+
+:- pred set_termination_info_for_proc(constr_termination_info::in,
+ pred_proc_id::in, module_info::in, module_info::out) is det.
+
+set_termination_info_for_proc(TerminationInfo, PPId, !ModuleInfo) :-
+ module_info_pred_proc_info(!.ModuleInfo, PPId, PredInfo, ProcInfo0),
+ proc_info_get_termination2_info(ProcInfo0, TermInfo0),
+ TermInfo = TermInfo0 ^ term_status := yes(TerminationInfo),
+ proc_info_set_termination2_info(TermInfo, ProcInfo0, ProcInfo),
+ module_info_set_pred_proc_info(PPId, PredInfo, ProcInfo, !ModuleInfo).
+
+%-----------------------------------------------------------------------------%
+%
+% Predicates for writing optimization interfaces.
+%
+
+:- pred maybe_make_optimization_interface(module_info::in, io::di, io::uo)
+ is det.
+
+maybe_make_optimization_interface(ModuleInfo, !IO) :-
+ globals.io_lookup_bool_option(make_optimization_interface, MakeOptInt,
+ !IO),
+ module_info_predids(ModuleInfo, PredIds),
+ ( if MakeOptInt = yes
+ then make_opt_int(PredIds, ModuleInfo, !IO)
+ else true
+ ).
+
+:- pred make_opt_int(list(pred_id)::in, module_info::in, io::di, io::uo) is det.
+
+make_opt_int(_PredIds, _ModuleInfo, !IO).
+
+% XXX The code for writing .opt files is currently disabled.
+
+% module_info_name(ModuleInfo, ModuleName),
+% module_name_to_file_name(ModuleName, ".opt.tmp", no, OptFileName, !IO),
+% globals.io_lookup_bool_option(verbose, Verbose, !IO),
+% maybe_write_string(Verbose,
+% "% Appending termination2_info pragmas to `", !IO),
+% maybe_write_string(Verbose, OptFileName, !IO),
+% maybe_write_string(Verbose, "'...", !IO),
+% maybe_flush_output(Verbose, !IO),
+% io.open_append(OptFileName, OptFileRes, !IO),
+% (
+% OptFileRes = ok(OptFile),
+% io.set_output_stream(OptFile, OldStream, !IO),
+% list.foldl(output_pred_termination2_info(ModuleInfo), PredIds,
+% !IO),
+% io.set_output_stream(OldStream, _, !IO),
+% io.close_output(OptFile, !IO),
+% maybe_write_string(Verbose, " done.\n", !IO)
+% ;
+% OptFileRes = error(IOError),
+% % failed to open the .opt file for processing
+% maybe_write_string(Verbose, " failed!\n", !IO),
+% io.error_message(IOError, IOErrorMessage),
+% io.write_strings(["Error opening file `",
+% OptFileName, "' for output: ", IOErrorMessage], !IO),
+% io.set_exit_status(1, !IO)
+% ).
+
+output_pred_termination2_info(ModuleInfo, PredId, !IO) :-
+ %
+ % Don't try to output termination2_info pragmas unless
+ % the analysis was actually run. Doing otherwise won't
+ % work because the necessary information will not have been set
+ % up.
+ %
+ globals.io_lookup_bool_option(termination2, RunningTerm2, !IO),
+ ( RunningTerm2 = yes ->
+ module_info_pred_info(ModuleInfo, PredId, PredInfo),
+ pred_info_import_status(PredInfo, ImportStatus),
+ module_info_type_spec_info(ModuleInfo, TypeSpecInfo),
+ TypeSpecInfo = type_spec_info(_, TypeSpecForcePreds, _, _),
+ (
+ (ImportStatus = exported
+ ;ImportStatus = opt_exported),
+ not hlds_pred.is_unify_or_compare_pred(PredInfo),
+ not set.member(PredId, TypeSpecForcePreds)
+ ->
+ PredName = pred_info_name(PredInfo),
+ pred_info_procedures(PredInfo, ProcTable),
+ pred_info_context(PredInfo, Context),
+ PredOrFunc = pred_info_is_pred_or_func(PredInfo),
+ ModuleName = pred_info_module(PredInfo),
+ ProcIds = pred_info_procids(PredInfo),
+ SymName = qualified(ModuleName, PredName),
+ make_opt_int_procs(PredId, ProcIds, ProcTable, PredOrFunc,
+ SymName, Context, !IO)
+ ;
+ true
+ )
+ ;
+ true
+ ).
+
+:- pred make_opt_int_procs(pred_id::in, list(proc_id)::in,
+ proc_table::in, pred_or_func::in, sym_name::in, prog_context::in,
+ io::di, io::uo) is det.
+
+make_opt_int_procs(_PredId, [], _, _, _, _, !IO).
+make_opt_int_procs(PredId, [ ProcId | ProcIds ], ProcTable,
+ PredOrFunc, SymName, Context, !IO) :-
+ ProcInfo = ProcTable ^ det_elem(ProcId),
+ proc_info_get_termination2_info(ProcInfo, TermInfo),
+ proc_info_declared_argmodes(ProcInfo, ModeList),
+ proc_info_headvars(ProcInfo, HeadVars),
+ SizeVarMap = TermInfo ^ size_var_map,
+ HeadSizeVars = prog_vars_to_size_vars(SizeVarMap, HeadVars),
+ output_pragma_termination2_info(PredOrFunc, SymName,
+ ModeList, Context, TermInfo ^ success_constrs,
+ TermInfo ^ failure_constrs, TermInfo ^ term_status,
+ HeadSizeVars, !IO),
+ make_opt_int_procs(PredId, ProcIds, ProcTable,
+ PredOrFunc, SymName, Context, !IO).
+
+%----------------------------------------------------------------------------%
+%
+% Predicates for writing termination2_info pragmas.
+%
+
+% NOTE: if these predicates are changed then prog_io_pragma.m must
+% also be changed so that it can parse the resulting pragma
+% termination2_info declarations.
+
+output_pragma_termination2_info(PredOrFunc, SymName, ModeList,
+ Context, MaybeSuccess, MaybeFailure, MaybeTermination,
+ HeadVars, !IO) :-
+ io.write_string(":- pragma termination2_info(", !IO),
+ (
+ PredOrFunc = predicate,
+ mercury_output_pred_mode_subdecl(varset.init, SymName,
+ ModeList, no, Context, !IO)
+ ;
+ PredOrFunc = function,
+ pred_args_to_func_args(ModeList, FuncModeList, RetMode),
+ mercury_output_func_mode_subdecl(varset.init, SymName,
+ FuncModeList, RetMode, no, Context, !IO)
+ ),
+ io.write_string(", ", !IO),
+ output_headvars(HeadVars, !IO),
+ io.write_string(", ", !IO),
+ output_maybe_constr_arg_size_info(MaybeSuccess, !IO),
+ io.write_string(", ", !IO),
+ output_maybe_constr_arg_size_info(MaybeFailure, !IO),
+ io.write_string(", ", !IO),
+ output_maybe_termination2_info(MaybeTermination, !IO),
+ io.write_string(").\n", !IO).
+
+:- pred output_headvars(size_vars::in, io::di, io::uo) is det.
+
+output_headvars(Vars, !IO) :-
+ io.write_char('[', !IO),
+ io.write_list(Vars, ", ", output_headvar, !IO),
+ io.write_char(']', !IO).
+
+:- pred output_headvar(size_var::in, io::di, io::uo) is det.
+
+output_headvar(Var, !IO) :-
+ io.write_int(term.var_to_int(Var), !IO).
+
+output_maybe_constr_arg_size_info(MaybeArgSizeConstrs, !IO) :-
+ (
+ MaybeArgSizeConstrs = no,
+ io.write_string("not_set", !IO)
+ ;
+ MaybeArgSizeConstrs = yes(Polyhedron),
+ io.write_string("constraints(", !IO),
+ Constraints = polyhedron.non_false_constraints(Polyhedron),
+ OutputVar = (func(Var) =
+ int_to_string(term.var_to_int(Var))
+ ),
+ lp_rational.output_constraints(OutputVar, Constraints, !IO),
+ io.write_char(')', !IO)
+ ).
+
+output_maybe_termination2_info(MaybeConstrTermInfo, !IO) :-
+ (
+ MaybeConstrTermInfo = no,
+ io.write_string("not_set", !IO)
+ ;
+ MaybeConstrTermInfo = yes(cannot_loop(_)),
+ io.write_string("cannot_loop", !IO)
+ ;
+ MaybeConstrTermInfo = yes(can_loop(_)),
+ io.write_string("can_loop", !IO)
+ ).
+
+%----------------------------------------------------------------------------%
+%
+% Utility predicates.
+%
+
+% These test whether various fields in the termination2_info struct have
+% been set.
+
+ % Succeeds iff the given procedure has argument size constraints
+ % associated with it.
+ %
+:- pred has_arg_size_info(module_info::in, pred_proc_id::in) is semidet.
+
+has_arg_size_info(ModuleInfo, PPId) :-
+ module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
+ proc_info_get_termination2_info(ProcInfo, TermInfo),
+ TermInfo ^ success_constrs = yes(_).
+
+ % Succeeds iff the termination status of a the given
+ % procedure has been set.
+ %
+:- pred has_term_info(module_info::in, pred_proc_id::in) is semidet.
+
+has_term_info(ModuleInfo, PPId) :-
+ module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
+ proc_info_get_termination2_info(ProcInfo, TermInfo),
+ TermInfo ^ term_status = yes(_).
+
+:- pred proc_needs_ar_built(module_info::in, pred_proc_id::in) is semidet.
+
+proc_needs_ar_built(ModuleInfo, PPId) :-
+ module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
+ proc_info_get_termination2_info(ProcInfo, TermInfo),
+ (
+ TermInfo ^ success_constrs = no
+ ;
+ TermInfo ^ term_status = no
+ ).
+
+%------------------------------------------------------------------------------%
+
+:- func this_file = string.
+
+this_file = "termination2.m".
+
+%------------------------------------------------------------------------------%
+:- end_module termination2.
+%------------------------------------------------------------------------------%
Index: compiler/trans_opt.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/trans_opt.m,v
retrieving revision 1.27
diff -u -r1.27 trans_opt.m
--- compiler/trans_opt.m 22 Mar 2005 06:40:29 -0000 1.27
+++ compiler/trans_opt.m 22 Mar 2005 06:49:36 -0000
@@ -84,6 +84,7 @@
:- import_module parse_tree__prog_out.
:- import_module transform_hlds__intermod.
:- import_module transform_hlds__termination.
+:- import_module transform_hlds__termination2.
:- import_module transform_hlds__exception_analysis.
:- import_module list.
@@ -132,13 +133,17 @@
module_info_predids(Module, PredIds),
list__foldl(termination__write_pred_termination_info(Module),
PredIds, !IO),
+% XXX Writing termination2_info pragma to .trans_opt files is currently
+% disabled.
+% list__foldl(termination2__output_pred_termination2_info(Module),
+% PredIds, !IO),
module_info_exception_info(Module, ExceptionInfo),
list__foldl(
exception_analysis__write_pragma_exceptions(Module,
ExceptionInfo),
PredIds, !IO),
-
+
io__set_output_stream(OldStream, _, !IO),
io__close_output(Stream, !IO),
Index: compiler/transform_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/transform_hlds.m,v
retrieving revision 1.16
diff -u -r1.16 transform_hlds.m
--- compiler/transform_hlds.m 6 Mar 2005 05:17:30 -0000 1.16
+++ compiler/transform_hlds.m 22 Mar 2005 06:44:45 -0000
@@ -40,8 +40,22 @@
:- include_module term_util.
:- include_module lp. % this could alternatively go in the `libs' module
-:- include_module post_term_analysis.
+:- include_module termination2.
+ %
+ % The termination analyser.
+ %
+ :- include_module term_constr_initial.
+ % Pass 1.
+ :- include_module term_constr_build.
+ :- include_module term_constr_fixpoint.
+ % Pass 2.
+ :- include_module term_constr_pass2.
+ % Other bits.
+ :- include_module term_constr_util.
+ :- include_module term_constr_data.
+ :- include_module term_constr_errors.
+:- include_module post_term_analysis.
:- include_module exception_analysis.
% Optimizations (HLDS -> HLDS)
--------------------------------------------------------------------------
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