[m-rev.] for review: change termination analysis for foreign_procs

Julien Fischer juliensf at students.cs.mu.OZ.AU
Mon Feb 9 15:49:29 AEDT 2004


Estimated hours taken: 19
Branches: main

Change how the termination analysis deals with foreign_procs.
Add `terminates' and `does_not_terminate' as foreign proc attributes.

Currently the termination analysis assumes that all procedures implemented
via the foreign language interface will terminate.  For foreign code
that does not make calls back to Mercury this is generally the behaviour
we want but for foreign code that does make calls back to Mercury we should
not assume termination because we do not know what Mercury procedures may be
called.

This change alters the termination analysis so that in the absence of
of any user supplied information foreign_procs that do not call Mercury
are considered terminating and those that do make calls back to Mercury
are non-terminating.  This new behaviour is safer than the old behaviour.
For example some of the compiler's optimization passes may rely on
information from the termination analysis about whether or not a predicate
will terminate.

The second part of this diff adds `terminates' and `does_not_terminate'
as foreign_proc attributes.  This is a cleaner way of specifying termination
properties than pragma terminates/does_not_terminate and it is also
more flexible than the pragmas.  For example, in cases where procedures have
both foreign and Mercury clauses, pragma terminates/does_not_terminate
declarations will apply to both.  Foreign code attributes allows us to
specify the termination properties of the foreign clauses and leave the
termination analysis to work out the termination properties of the
Mercury clauses.

compiler/hlds_pred.m:
compiler/prog_data.m:
compiler/prog_io_pragma:
	Handle terminates/does_not_terminate as foreign proc attributes.

compiler/term_errors.m:
compiler/term_traversal.m:
compiler/termination.m:
	Handle terminates/does_not_terminate as foreign proc attributes.
	Check that the foreign proc attributes do not conflict with any
	termination pragmas that the user has supplied.
	Modify assumptions about the termination of foreign procs.
compiler/term_util.m:
	Move some utility predicates to this module.

doc/reference_manual.texi:
	Document new foreign proc attributes and the new behaviour
	of the termination analysis for foreign_procs.
	Fix a typo.

tests/term/Mmakefile:
tests/term/foreign_valid.m:
tests/term/foreign_valid.trans_opt_exp:
tests/warnings/Mmakefile:
tests/warnings/foreign_term_invalid.m:
tests/warnings/foreign_term_invalid.exp:
	Test cases for the above.

Julien.


Index: compiler/hlds_pred.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_pred.m,v
retrieving revision 1.138
diff -u -r1.138 hlds_pred.m
--- compiler/hlds_pred.m	21 Dec 2003 05:04:34 -0000	1.138
+++ compiler/hlds_pred.m	3 Feb 2004 06:54:35 -0000
@@ -779,6 +779,8 @@

 :- pred purity_to_markers(purity::in, pred_markers::out) is det.

+:- pred terminates_to_markers(terminates::in, pred_markers::out) is det.
+
 :- pred pred_info_get_markers(pred_info::in, pred_markers::out) is det.

 :- pred pred_info_set_markers(pred_markers::in, pred_info::in, pred_info::out)
@@ -1289,6 +1291,10 @@
 purity_to_markers(pure, []).
 purity_to_markers(semipure, [semipure]).
 purity_to_markers(impure, [impure]).
+
+terminates_to_markers(terminates, [terminates]).
+terminates_to_markers(does_not_terminate, [does_not_terminate]).
+terminates_to_markers(depends_on_mercury_calls, []).

 pred_info_get_markers(PredInfo, PredInfo ^ markers).

Index: compiler/prog_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_data.m,v
retrieving revision 1.103
diff -u -r1.103 prog_data.m
--- compiler/prog_data.m	23 Dec 2003 03:10:39 -0000	1.103
+++ compiler/prog_data.m	4 Feb 2004 05:48:45 -0000
@@ -821,6 +821,7 @@
 :- func may_call_mercury(pragma_foreign_proc_attributes) = may_call_mercury.
 :- func thread_safe(pragma_foreign_proc_attributes) = thread_safe.
 :- func purity(pragma_foreign_proc_attributes) = purity.
+:- func terminates(pragma_foreign_proc_attributes) = terminates.
 :- func legacy_purity_behaviour(pragma_foreign_proc_attributes) = bool.
 :- func foreign_language(pragma_foreign_proc_attributes) = foreign_language.
 :- func tabled_for_io(pragma_foreign_proc_attributes) = tabled_for_io.
@@ -847,6 +848,10 @@
 	pragma_foreign_proc_attributes::in,
 	pragma_foreign_proc_attributes::out) is det.

+:- pred set_terminates(terminates::in,
+	pragma_foreign_proc_attributes::in,
+	pragma_foreign_proc_attributes::out) is det.
+
 :- pred set_legacy_purity_behaviour(bool::in,
 	pragma_foreign_proc_attributes::in,
 	pragma_foreign_proc_attributes::out) is det.
@@ -882,6 +887,11 @@
 		% we explicitly store the name because we need the real
 		% name in code_gen

+:- type terminates
+	--->	terminates
+	;	does_not_terminate
+	;	depends_on_mercury_calls.
+
 :- type pragma_foreign_proc_extra_attribute
 	--->	max_stack_size(int).

@@ -1345,6 +1355,7 @@
 				% there is some special case behaviour for
 				% pragma c_code and pragma import purity
 				% if legacy_purity_behaviour is `yes'
+			terminates		:: terminates,
 			legacy_purity_behaviour	:: bool,
 			extra_attributes	::
 				list(pragma_foreign_proc_extra_attribute)
@@ -1352,7 +1363,7 @@

 default_attributes(Language) =
 	attributes(Language, may_call_mercury, not_thread_safe,
-		not_tabled_for_io, impure, no, []).
+		not_tabled_for_io, impure, depends_on_mercury_calls, no, []).

 set_may_call_mercury(MayCallMercury, Attrs0, Attrs) :-
 	Attrs = Attrs0 ^ may_call_mercury := MayCallMercury.
@@ -1364,6 +1375,8 @@
 	Attrs = Attrs0 ^ tabled_for_io := TabledForIo.
 set_purity(Purity, Attrs0, Attrs) :-
 	Attrs = Attrs0 ^ purity := Purity.
+set_terminates(Terminates, Attrs0, Attrs) :-
+	Attrs = Attrs0 ^ terminates := Terminates.
 set_legacy_purity_behaviour(Legacy, Attrs0, Attrs) :-
 	Attrs = Attrs0 ^ legacy_purity_behaviour := Legacy.

@@ -1372,7 +1385,7 @@
 	% in the attribute list -- the foreign language specifier string
 	% is at the start of the pragma.
 	Attrs = attributes(_Lang, MayCallMercury, ThreadSafe, TabledForIO,
-			Purity,	_LegacyBehaviour, ExtraAttributes),
+			Purity,	Terminates, _LegacyBehaviour, ExtraAttributes),
 	(
 		MayCallMercury = may_call_mercury,
 		MayCallMercuryStr = "may_call_mercury"
@@ -1410,8 +1423,18 @@
 		Purity = (impure),
 		PurityStrList = []
 	),
+	(
+		Terminates = terminates,
+		TerminatesStrList = ["terminates"]
+	;
+		Terminates = does_not_terminate,
+		TerminatesStrList = ["does_not_terminate"]
+	;
+		Terminates = depends_on_mercury_calls,
+		TerminatesStrList = []
+	),
 	StringList = [MayCallMercuryStr, ThreadSafeStr, TabledForIOStr |
-			PurityStrList] ++
+			PurityStrList] ++ TerminatesStrList ++
 		list__map(extra_attribute_to_string, ExtraAttributes).

 add_extra_attribute(NewAttribute, Attributes0,
Index: compiler/prog_io_pragma.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_pragma.m,v
retrieving revision 1.63
diff -u -r1.63 prog_io_pragma.m
--- compiler/prog_io_pragma.m	21 Dec 2003 05:04:37 -0000	1.63
+++ compiler/prog_io_pragma.m	4 Feb 2004 06:02:00 -0000
@@ -1213,7 +1213,8 @@
 	;	tabled_for_io(tabled_for_io)
 	;	purity(purity)
 	;	aliasing
-	;	max_stack_size(int).
+	;	max_stack_size(int)
+	;	terminates(terminates).

 :- pred parse_pragma_foreign_proc_attributes_term(foreign_language, string,
 		term, maybe1(pragma_foreign_proc_attributes)).
@@ -1247,7 +1248,12 @@
 			tabled_for_io(not_tabled_for_io),
 		purity(pure) - purity(impure),
 		purity(pure) - purity(semipure),
-		purity(semipure) - purity(impure)
+		purity(semipure) - purity(impure),
+		terminates(terminates) - terminates(does_not_terminate),
+		terminates(depends_on_mercury_calls) -
+			terminates(terminates),
+		terminates(depends_on_mercury_calls) -
+			terminates(does_not_terminate)
 	],
 	(
 		parse_pragma_foreign_proc_attributes_term0(Term, AttrList)
@@ -1285,6 +1291,8 @@
 	set_tabled_for_io(TabledForIO, !Attrs).
 process_attribute(purity(Pure), !Attrs) :-
 	set_purity(Pure, !Attrs).
+process_attribute(terminates(Terminates), !Attrs) :-
+	set_terminates(Terminates, !Attrs).
 process_attribute(max_stack_size(Size), !Attrs) :-
 	add_extra_attribute(max_stack_size(Size), !Attrs).

@@ -1350,6 +1358,8 @@
 		Flag = max_stack_size(Size)
 	; parse_purity_promise(Term, Purity) ->
 		Flag = purity(Purity)
+	; parse_terminates(Term, Terminates) ->
+		Flag = terminates(Terminates)
 	;
 		fail
 	).
@@ -1415,6 +1425,13 @@
 		(pure)).
 parse_purity_promise(term__functor(term__atom("promise_semipure"), [], _),
 		(semipure)).
+
+:- pred parse_terminates(term::in, terminates::out) is semidet.
+
+parse_terminates(term__functor(term__atom("terminates"), [], _),
+		terminates).
+parse_terminates(term__functor(term__atom("does_not_terminate"), [], _),
+		does_not_terminate).

 % parse a pragma foreign_code declaration

Index: compiler/term_errors.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_errors.m,v
retrieving revision 1.21
diff -u -r1.21 term_errors.m
--- compiler/term_errors.m	5 Nov 2003 03:17:44 -0000	1.21
+++ compiler/term_errors.m	6 Feb 2004 07:42:00 -0000
@@ -112,10 +112,15 @@
 	;	does_not_term_pragma(pred_id)
 			% The given procedure has a does_not_terminate pragma.

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

+	;	does_not_term_foreign(pred_proc_id).
+			% The procedure contains foreign code that may
+			% make calls back to Mercury.  By default such
+			% code is assumed to be non-terminating.
+
 :- type term_errors__error == pair(prog_context, termination_error).

 :- pred term_errors__report_term_errors(list(pred_proc_id)::in,
@@ -445,6 +450,11 @@

 term_errors__description(inconsistent_annotations, _, _, Pieces, no) :-
 	Pieces = [words("The termination pragmas are inconsistent.")].
+
+term_errors__description(does_not_term_foreign(_), _, _, Pieces, no) :-
+	Piece1 = words("It contains foreign code that"),
+	Piece2 = words("makes one or more calls back to Mercury."),
+	Pieces = [Piece1, Piece2].

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

Index: compiler/term_traversal.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_traversal.m,v
retrieving revision 1.27
diff -u -r1.27 term_traversal.m
--- compiler/term_traversal.m	3 Feb 2004 04:07:52 -0000	1.27
+++ compiler/term_traversal.m	9 Feb 2004 03:57:18 -0000
@@ -195,7 +195,7 @@
 	traverse_goal(Else, Params, !.Info, ElseInfo),
 	combine_paths(CondThenInfo, ElseInfo, Params, !:Info).

-traverse_goal_2(foreign_proc(_, CallPredId, CallProcId, Args, _,_,_),
+traverse_goal_2(foreign_proc(Attributes, CallPredId, CallProcId, Args, _,_,_),
 		GoalInfo, Params, !Info) :-
 	params_get_module_info(Params, Module),
 	module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
@@ -203,7 +203,19 @@
 	proc_info_argmodes(CallProcInfo, CallArgModes),
 	partition_call_args(Module, CallArgModes, Args, _InVars, OutVars),
 	goal_info_get_context(GoalInfo, Context),
-	error_if_intersect(OutVars, Context, pragma_foreign_code, !Info).
+
+	( is_termination_known(Module, proc(CallPredId, CallProcId)) ->
+		error_if_intersect(OutVars, Context, pragma_foreign_code,
+			!Info)
+	;
+		( attributes_imply_termination(Attributes) ->
+			error_if_intersect(OutVars, Context,
+				pragma_foreign_code, !Info)
+		;
+			add_error(Context, does_not_term_pragma(CallPredId),
+				Params, !Info)
+		)
+	).

 traverse_goal_2(generic_call(_, _, _, _), GoalInfo, Params, !Info) :-
 	%
Index: compiler/term_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_util.m,v
retrieving revision 1.33
diff -u -r1.33 term_util.m
--- compiler/term_util.m	3 Feb 2004 04:07:53 -0000	1.33
+++ compiler/term_util.m	4 Feb 2004 06:06:33 -0000
@@ -132,13 +132,23 @@
 :- pred lookup_proc_arg_size_info(module_info::in, pred_proc_id::in,
 	maybe(arg_size_info)::out) is det.

-% Succeeds if one or more variables in the list are higher order.
-
+	% Succeeds if one or more variables in the list are higher order.
 :- pred horder_vars(list(prog_var)::in , map(prog_var, type)::in) is semidet.

 :- pred get_context_from_scc(list(pred_proc_id)::in, module_info::in,
 	prog_context::out) is det.

+	% Succeeds if the termination status of a procedure is known.
+:- pred is_termination_known(module_info::in, pred_proc_id::in) is semidet.
+
+	% Succeeds if the foreign proc attributes imply that a procedure
+	% is terminating.
+:- pred attributes_imply_termination(pragma_foreign_proc_attributes::in)
+	is semidet.
+
+	% Succeeds if the given predicate is builtin or compiler generated.
+:- pred is_builtin_or_comp_gen(pred_info::in) is semidet.
+
 %-----------------------------------------------------------------------------%

 % Convert a prog_data__pragma_termination_info into a
@@ -354,6 +364,27 @@
 add_context_to_arg_size_info(yes(finite(A, B)), _, yes(finite(A, B))).
 add_context_to_arg_size_info(yes(infinite), Context,
 		yes(infinite([Context - imported_pred]))).
+
+%-----------------------------------------------------------------------------%
+
+is_termination_known(Module, PPId) :-
+	module_info_pred_proc_info(Module, PPId, _, ProcInfo),
+	proc_info_get_maybe_termination_info(ProcInfo, yes(_)).
+
+attributes_imply_termination(Attributes) :-
+	(
+		terminates(Attributes) = terminates
+	;
+		terminates(Attributes) = depends_on_mercury_calls,
+		may_call_mercury(Attributes) = will_not_call_mercury
+	).
+
+is_builtin_or_comp_gen(PredInfo) :-
+	(
+		pred_info_is_builtin(PredInfo)
+	;
+		pred_info_get_maybe_special_pred(PredInfo, yes(_))
+	).

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

Index: compiler/termination.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/termination.m,v
retrieving revision 1.37
diff -u -r1.37 termination.m
--- compiler/termination.m	16 Jan 2004 05:32:13 -0000	1.37
+++ compiler/termination.m	4 Feb 2004 06:52:15 -0000
@@ -133,7 +133,10 @@
 	module_info_ensure_dependency_info(!Module),
 	module_info_dependency_info(!.Module, DepInfo),
 	hlds_dependency_info_get_dependency_ordering(DepInfo, SCCs),
-
+
+		% Set the termination status of foreign_procs.
+	check_foreign_code_attributes(SCCs, !Module, !IO),
+
 		% Ensure that termination pragmas for a proc. do conflict
 		% with termination pragmas for other procs. in the same SCC.
 	check_pragmas_are_consistent(SCCs, !Module, !IO),
@@ -149,6 +152,109 @@
 	).

 %----------------------------------------------------------------------------%
+%
+% Handle foreign code attributes.
+%
+
+% Set the termination status for any procedures implemented using the
+% foreign language interface.  If the terminates/does_not_terminate
+% attribute has been set then we set the termination status of the procedure
+% accordingly.  Otherwise the procedure is considered to be terminating
+% if it does not call Mercury and non-terminating if it does.
+%
+% We also check that the foreign code attributes do not conflict with any
+% termination pragmas that have been supplied for the procedure.
+
+:- pred check_foreign_code_attributes(list(list(pred_proc_id))::in,
+	module_info::in, module_info::out, io::di, io::uo) is det.
+
+check_foreign_code_attributes(SCCs, !Module, !IO) :-
+	list__foldl2(check_foreign_code_attributes_2, SCCs, !Module, !IO).
+
+:- pred check_foreign_code_attributes_2(list(pred_proc_id)::in, module_info::in,
+	module_info::out, io::di, io::uo) is det.
+
+	% This case shouldn't happen.
+check_foreign_code_attributes_2([], _, _, _, _) :-
+	unexpected(this_file, "check_foreign_code_attributes_2/5: empty SCC.").
+check_foreign_code_attributes_2([PPId], !Module, !IO) :-
+	module_info_pred_proc_info(!.Module, PPId, PredInfo, ProcInfo0),
+	(
+		not is_builtin_or_comp_gen(PredInfo),
+		proc_info_goal(ProcInfo0, Goal),
+		fst(Goal) = foreign_proc(Attributes, _, _, _, _, _, _)
+	->
+		proc_info_get_maybe_termination_info(ProcInfo0,
+			MaybeTermination),
+		proc_info_context(ProcInfo0, Context),
+		(
+			MaybeTermination = no,
+			( attributes_imply_termination(Attributes) ->
+				proc_info_set_maybe_termination_info(
+					yes(cannot_loop), ProcInfo0, ProcInfo)
+			;
+				TermErr = Context - does_not_term_foreign(PPId),
+				proc_info_set_maybe_termination_info(
+					yes(can_loop([TermErr])), ProcInfo0,
+					ProcInfo)
+			)
+		;
+			% 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),
+			( terminates(Attributes) = does_not_terminate ->
+				TermErr = Context - inconsistent_annotations,
+				proc_info_set_maybe_termination_info(
+					yes(can_loop([TermErr])), ProcInfo0,
+					ProcInfo),
+				error_util__describe_one_proc_name(!.Module,
+					PPId, ProcName),
+				Piece1 = words("has a pragma terminates"),
+				Piece2 = words("declaration but also has the"),
+				Piece3 = words("`does_not_terminate' foreign"),
+				Piece4 = words("code attribute set."),
+				Components = [words("Warning:"),
+					fixed(ProcName), Piece1, Piece2,
+					Piece3, Piece4],
+				error_util__report_warning(Context, 0,
+					Components, !IO)
+			;
+				ProcInfo = ProcInfo0
+			)
+		;
+			% In this case there was a `pragma does_not_terminate'
+			% declaration - check that the foreign code attribute
+			% does not contradict this.
+			MaybeTermination = yes(can_loop(TermErrs0)),
+			( terminates(Attributes) = terminates ->
+			    TermErr = Context - inconsistent_annotations,
+			    TermErrs = [TermErr | TermErrs0 ],
+			    proc_info_set_maybe_termination_info(
+			        yes(can_loop(TermErrs)),
+			        ProcInfo0, ProcInfo),
+			    error_util__describe_one_proc_name(!.Module,
+			        PPId, ProcName),
+			    Piece1 = words("has a pragma does_not_terminate"),
+			    Piece2 = words("declaration but also has the"),
+			    Piece3 = words("`terminates' foreign code"),
+			    Piece4 = words("attribute set."),
+			    Components = [words("Warning:"), fixed(ProcName),
+				Piece1, Piece2, Piece3, Piece4],
+			    error_util__report_warning(Context, 0, Components,
+			        !IO)
+			;
+			    ProcInfo = ProcInfo0
+			)
+		),
+		module_info_set_pred_proc_info(PPId, PredInfo, ProcInfo,
+			!Module)
+	;
+		true
+	).
+check_foreign_code_attributes_2([_, _ | _], !Module, !IO).
+
+%----------------------------------------------------------------------------%
 % Check that any user-supplied termination information (from pragma
 % terminates/does_not_terminate) is consistent for each SCC in the program.
 %
@@ -248,13 +354,6 @@
 		PPIdStatus = can_loop(_)
 	),
 	check_procs_known_term(Status, PPIds, Module).
-
-	% Succeeds iff the termination status of a procedure is known.
-:- pred is_termination_known(module_info::in, pred_proc_id::in) is semidet.
-
-is_termination_known(Module, PPId) :-
-	module_info_pred_proc_info(Module, PPId, _, ProcInfo),
-	proc_info_get_maybe_termination_info(ProcInfo, yes(_)).

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

Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.289
diff -u -r1.289 reference_manual.texi
--- doc/reference_manual.texi	5 Feb 2004 08:58:16 -0000	1.289
+++ doc/reference_manual.texi	5 Feb 2004 11:33:04 -0000
@@ -5549,6 +5549,13 @@

 @table @asis

+ at item @samp{terminates}/@samp{does_not_terminate}
+This attribute specifies the termination properties of the given predicate
+or function definition.  It is equivalent to the corresponding
+ at samp{pragma terminates} or @samp{pragma does_not_terminate} declaration.
+If omitted, the termination property of the procedure is determined by the
+value of the @samp{may_call_mercury}/@samp{will_not_call_mercury} attribute.
+See @ref{Termination analysis} for more details.
 @item @samp{max_stack_size(Size)}
 This attribute declares the maximum stack usage of a particular piece of
 code.  The unit that @samp{Size} is measured in depends upon foreign language
@@ -8488,7 +8495,7 @@
 termination cannot be proved, the compiler will emit an error message
 detailing the reason that termination could not be proved.

-The option @samp{--check-termination} option, which may be abbreviated
+The option @samp{--check-termination}, which may be abbreviated
 to @samp{--check-term} or @samp{--chk-term}, forces the compiler to
 check the termination of all predicates in the module.
 It is common for the compiler to be unable to prove termination of some
@@ -8507,14 +8514,19 @@
 optimization is enabled, the compiler must assume that any imported
 predicate may not terminate.

-Currently the compiler assumes that all procedures defined using the C
-interface (@samp{pragma c_code}) terminate for all input.
-If this is not the case, a @samp{pragma does_not_terminate} declaration
-should be used to inform the compiler that this C code may not terminate.
+By default, the compiler assumes that a procedure defined
+using the foreign language interface will terminate for all input
+if it does not call Mercury.  If it does call Mercury then by default
+the compiler will assume that it may not terminate.
+
+The foreign code attributes @samp{terminates}/@samp{does_not_terminate}
+may be used to force the compiler to treat a foreign_proc as
+terminating/non-terminating irrespective of whether it calls Mercury.
+As a matter of style, it is preferable to use foreign code attributes
+for foreign_procs rather than the termination pragmas described below.

 The following declarations can be used to inform the compiler of the
-termination properties of a predicate or function, or to force the
-compiler to prove termination of a given predicate or function.
+termination properties of a predicate or function.

 @example
 :- pragma terminates(@var{Name}/@var{Arity}).
@@ -8533,10 +8545,9 @@
 @end example

 This declaration may be used to inform the compiler that this predicate
-does not necessarily terminate.  This is useful for procedures defined
-using the C interface, which the compiler assumes to terminate by
-default.  This declaration affects not only the predicate specified
-but also any other predicates that are mutually recursive with it.
+may not terminate.  This declaration affects not only the predicate
+specified but also any other predicates that are mutually recursive
+with it.

 @example
 :- pragma check_termination(@var{Name}/@var{Arity}).
Index: tests/term/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/term/Mmakefile,v
retrieving revision 1.23
diff -u -r1.23 Mmakefile
--- tests/term/Mmakefile	15 Dec 2003 07:11:06 -0000	1.23
+++ tests/term/Mmakefile	4 Feb 2004 05:44:11 -0000
@@ -23,6 +23,7 @@
 	existential_error2 \
 	existential_error3 \
 	fold \
+	foreign_valid \
 	inf_const_bug \
 	my_list \
 	lte \
Index: tests/term/foreign_valid.m
===================================================================
RCS file: tests/term/foreign_valid.m
diff -N tests/term/foreign_valid.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/term/foreign_valid.m	4 Feb 2004 05:43:56 -0000
@@ -0,0 +1,82 @@
+:- module foreign_valid.
+
+:- interface.
+
+:- import_module int.
+
+:- pred test1(int::out) is det.
+:- pred test2(int::out) is det.
+:- pred test3(int::out) is det.
+:- pred test4(int::out) is det.
+:- pred test5(int::out) is det.
+:- pred test6(int::out) is det.
+:- pred test7(int::out) is det.
+:- pred test8(int::out) is det.
+:- pred test9(int::out) is det.
+:- pred test10(int::out) is det.
+
+:- implementation.
+
+:- pragma foreign_proc("C", test1(X::out),
+	[will_not_call_mercury, promise_pure, thread_safe],
+"
+	X = (MR_Integer) 3;
+").
+
+:- pragma foreign_proc("C", test2(X::out),
+	[may_call_mercury, promise_pure, thread_safe],
+"
+	X = (MR_Integer) 3;
+").
+
+:- pragma foreign_proc("C", test3(X::out),
+	[will_not_call_mercury, promise_pure, thread_safe, does_not_terminate], "
+	X = (MR_Integer) 3;
+").
+
+:- pragma foreign_proc("C", test4(X::out),
+	[may_call_mercury, promise_pure, thread_safe, terminates],
+"
+	X = (MR_Integer) 3;
+").
+
+:- pragma foreign_proc("C", test5(X::out),
+	[will_not_call_mercury, promise_pure, thread_safe, terminates],
+"
+	X = (MR_Integer) 3;
+").
+
+:- pragma foreign_proc("C", test6(X::out),
+	[may_call_mercury, promise_pure, thread_safe, does_not_terminate],
+"
+	X = (MR_Integer) 3;
+").
+
+:- pragma terminates(test7/1).
+:- pragma foreign_proc("C", test7(X::out),
+	[may_call_mercury, promise_pure, thread_safe],
+"
+	X = (MR_Integer) 3;
+").
+
+:- pragma does_not_terminate(test8/1).
+:- pragma foreign_proc("C", test8(X::out),
+	[will_not_call_mercury, promise_pure, thread_safe],
+"
+	X = (MR_Integer) 3;
+").
+
+:- pragma terminates(test9/1).
+:- pragma foreign_proc("C", test9(X::out),
+	[may_call_mercury, promise_pure, thread_safe, terminates],
+"
+	X = (MR_Integer) 3;
+").
+
+:- pragma does_not_terminate(test10/1).
+:- pragma foreign_proc("C", test10(X::out),
+	[will_not_call_mercury, promise_pure, thread_safe, does_not_terminate], "
+	X = (MR_Integer) 3;
+").
+
+:- end_module foreign_valid.
Index: tests/term/foreign_valid.trans_opt_exp
===================================================================
RCS file: tests/term/foreign_valid.trans_opt_exp
diff -N tests/term/foreign_valid.trans_opt_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/term/foreign_valid.trans_opt_exp	4 Feb 2004 05:49:40 -0000
@@ -0,0 +1,11 @@
+:- module foreign_valid.
+:- pragma termination_info(foreign_valid.test1((builtin.out)), infinite, cannot_loop).
+:- pragma termination_info(foreign_valid.test2((builtin.out)), infinite, can_loop).
+:- pragma termination_info(foreign_valid.test3((builtin.out)), infinite, can_loop).
+:- pragma termination_info(foreign_valid.test4((builtin.out)), infinite, cannot_loop).
+:- pragma termination_info(foreign_valid.test5((builtin.out)), infinite, cannot_loop).
+:- pragma termination_info(foreign_valid.test6((builtin.out)), infinite, can_loop).
+:- pragma termination_info(foreign_valid.test7((builtin.out)), infinite, cannot_loop).
+:- pragma termination_info(foreign_valid.test8((builtin.out)), infinite, can_loop).
+:- pragma termination_info(foreign_valid.test9((builtin.out)), infinite, cannot_loop).
+:- pragma termination_info(foreign_valid.test10((builtin.out)), infinite, can_loop).
Index: tests/warnings/Mercury.options
===================================================================
RCS file: /home/mercury1/repository/tests/warnings/Mercury.options,v
retrieving revision 1.9
diff -u -r1.9 Mercury.options
--- tests/warnings/Mercury.options	12 Jan 2004 05:24:32 -0000	1.9
+++ tests/warnings/Mercury.options	4 Feb 2004 06:48:48 -0000
@@ -39,5 +39,6 @@
 	# to make sure that it is enabled otherwise the tests will fail.
 MCFLAGS-pragma_term_conflict = --enable-termination
 MCFLAGS-term_indirect_warning = --check-termination
+MCFLAGS-foreign_term_invalid = --enable-termination

 MCFLAGS-warn_dead_procs 	= --warn-dead-procs --infer-all
Index: tests/warnings/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/warnings/Mmakefile,v
retrieving revision 1.33
diff -u -r1.33 Mmakefile
--- tests/warnings/Mmakefile	12 Jan 2004 05:24:32 -0000	1.33
+++ tests/warnings/Mmakefile	4 Feb 2004 06:46:59 -0000
@@ -6,6 +6,7 @@

 COMPILE_PROGS=	\
 	arg_order_rearrangment \
+	foreign_term_invalid \
 	pragma_term_conflict \
 	term_indirect_warning \
 	warn_dead_procs
Index: tests/warnings/foreign_term_invalid.exp
===================================================================
RCS file: tests/warnings/foreign_term_invalid.exp
diff -N tests/warnings/foreign_term_invalid.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/warnings/foreign_term_invalid.exp	4 Feb 2004 06:52:52 -0000
@@ -0,0 +1,10 @@
+foreign_term_invalid.m:009: Warning:
+foreign_term_invalid.m:009:   predicate `foreign_term_invalid.test1/1' mode 0
+foreign_term_invalid.m:009:   has a pragma does_not_terminate declaration but
+foreign_term_invalid.m:009:   also has the `terminates' foreign code attribute
+foreign_term_invalid.m:009:   set.
+foreign_term_invalid.m:010: Warning:
+foreign_term_invalid.m:010:   predicate `foreign_term_invalid.test2/1' mode 0
+foreign_term_invalid.m:010:   has a pragma terminates declaration but also has
+foreign_term_invalid.m:010:   the `does_not_terminate' foreign code attribute
+foreign_term_invalid.m:010:   set.
Index: tests/warnings/foreign_term_invalid.m
===================================================================
RCS file: tests/warnings/foreign_term_invalid.m
diff -N tests/warnings/foreign_term_invalid.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/warnings/foreign_term_invalid.m	4 Feb 2004 06:46:17 -0000
@@ -0,0 +1,26 @@
+	% These should issue warnings about termination pragmas conflicting
+	% with foreign proc attributes.
+:- module foreign_term_invalid.
+
+:- interface.
+
+:- import_module int.
+
+:- pred test1(int::out) is det.
+:- pred test2(int::out) is det.
+
+:- implementation.
+
+:- pragma does_not_terminate(test1/1).
+:- pragma foreign_proc("C", test1(X::out),
+	[will_not_call_mercury, promise_pure, thread_safe, terminates], "
+	X = (MR_Integer) 3;
+").
+
+:- pragma terminates(test2/1).
+:- pragma foreign_proc("C", test2(X::out),
+	[may_call_mercury, promise_pure, thread_safe, does_not_terminate], "
+	X = (MR_Integer) 3;
+").
+
+:- end_module foreign_term_invalid.

--------------------------------------------------------------------------
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