[m-rev.] for review: add termination foreign proc attributes
Julien Fischer
juliensf at students.cs.mu.OZ.AU
Wed Oct 8 16:27:08 AEST 2003
For review by Zoltan.
(This is a revised version of the diff I posted earlier this year).
Estimated hours taken: 14
Branches: main
Accept `terminates' and `does_not_terminate' as foreign proc attributes.
Alter the termination analyser to handle these new attributes.
Change the how the termination analyser treats foreign procs in the
absence of any user-supplied information. The old behaviour was to
treat all foreign procs as terminating; we now consider only those that
do not make any calls back to Mercury as terminating. Foreign procs
that do make calls back to Mercury now considered to be non-terminating.
compiler/hlds_pred.m:
compiler/prog_data.m:
compiler/prog_io_pragma.m:
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 foreign proc attributes do not conflict with termination
pragmas.
Modify assumptions about termination of foreign procs.
Use state variables instead of numbered sequences of variables in
a few places.
compiler/term_util.m:
Move some utility predicates here.
doc/reference_manual.texi:
Document new foreign proc attributes and the new behaviour
of the termination analysis with respect to foreign procs.
tests/term/Mmakefile:
tests/term/foreign_valid.m:
tests/term/foreign_valid.trans_opt_exp:
tests/warnings/Mercury.options:
tests/warnings/Mmakefile:
tests/warnings/foreign_term_invalid.exp:
tests/warnings/foreign_term_invalid.m:
Test cases for the above.
Index: compiler/hlds_pred.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_pred.m,v
retrieving revision 1.129
diff -u -r1.129 hlds_pred.m
--- compiler/hlds_pred.m 19 Sep 2003 11:10:02 -0000 1.129
+++ compiler/hlds_pred.m 22 Sep 2003 02:25:02 -0000
@@ -843,6 +843,9 @@
:- pred purity_to_markers(purity, pred_markers).
:- mode purity_to_markers(in, out) is det.
+:- pred terminates_to_markers(terminates, pred_markers).
+:- mode terminates_to_markers(in, out) is det.
+
:- pred pred_info_get_markers(pred_info, pred_markers).
:- mode pred_info_get_markers(in, out) is det.
@@ -1369,6 +1372,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.97
diff -u -r1.97 prog_data.m
--- compiler/prog_data.m 19 Sep 2003 11:10:04 -0000 1.97
+++ compiler/prog_data.m 3 Oct 2003 04:21:23 -0000
@@ -731,6 +731,9 @@
:- pred purity(pragma_foreign_proc_attributes, purity).
:- mode purity(in, out) is det.
+:- pred terminates(pragma_foreign_proc_attributes, terminates).
+:- mode terminates(in, out) is det.
+
:- pred legacy_purity_behaviour(pragma_foreign_proc_attributes, bool).
:- mode legacy_purity_behaviour(in, out) is det.
@@ -756,6 +759,10 @@
pragma_foreign_proc_attributes).
:- mode set_purity(in, in, out) is det.
+:- pred set_terminates(pragma_foreign_proc_attributes, terminates,
+ pragma_foreign_proc_attributes).
+:- mode set_terminates(in, in, out) is det.
+
:- pred set_legacy_purity_behaviour(pragma_foreign_proc_attributes, bool,
pragma_foreign_proc_attributes).
:- mode set_legacy_purity_behaviour(in, in, out) is det.
@@ -789,6 +796,11 @@
; tabled_for_io_unitize
; tabled_for_descendant_io.
+:- type terminates
+ ---> terminates
+ ; does_not_terminate
+ ; depends_on_mercury_calls.
+
:- type pragma_var
---> pragma_var(prog_var, string, mode).
% variable, name, mode
@@ -1236,6 +1248,7 @@
thread_safe :: thread_safe,
tabled_for_io :: tabled_for_io,
purity :: purity,
+ terminates :: terminates,
% there is some special case behaviour for
% pragma c_code and pragma import purity
% if legacy_purity_behaviour is `yes'
@@ -1247,7 +1260,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, [])).
may_call_mercury(Attrs, Attrs ^ may_call_mercury).
@@ -1259,6 +1272,8 @@
purity(Attrs, Attrs ^ purity).
+terminates(Attrs, Attrs ^ terminates).
+
legacy_purity_behaviour(Attrs, Attrs ^ legacy_purity_behaviour).
set_may_call_mercury(Attrs0, MayCallMercury, Attrs) :-
@@ -1276,6 +1291,9 @@
set_purity(Attrs0, Purity, Attrs) :-
Attrs = Attrs0 ^ purity := Purity.
+set_terminates(Attrs0, Terminates, Attrs) :-
+ Attrs = Attrs0 ^ terminates := Terminates.
+
set_legacy_purity_behaviour(Attrs0, Legacy, Attrs) :-
Attrs = Attrs0 ^ legacy_purity_behaviour := Legacy.
@@ -1284,7 +1302,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"
@@ -1322,8 +1340,18 @@
Purity = (impure),
PurityStrList = []
),
- StringList = [MayCallMercuryStr, ThreadSafeStr, TabledForIOStr |
- PurityStrList] ++
+ (
+ Terminates = terminates,
+ TerminatesStrList = ["terminates"]
+ ;
+ Terminates = does_not_terminate,
+ TerminatesStrList = ["does_not_terminate"]
+ ;
+ Terminates = depends_on_mercury_calls,
+ TerminatesStrList = []
+ ),
+ StringList = [MayCallMercuryStr, ThreadSafeStr, TabledForIOStr] ++
+ TerminatesStrList ++ PurityStrList ++
list__map(extra_attribute_to_string, ExtraAttributes).
add_extra_attribute(Attributes0, NewAttribute,
Index: compiler/prog_io_pragma.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_pragma.m,v
retrieving revision 1.59
diff -u -r1.59 prog_io_pragma.m
--- compiler/prog_io_pragma.m 26 May 2003 09:00:06 -0000 1.59
+++ compiler/prog_io_pragma.m 17 Jun 2003 05:41:08 -0000
@@ -1206,7 +1206,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)).
@@ -1240,7 +1241,10 @@
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)
@@ -1279,6 +1283,8 @@
set_tabled_for_io(Attrs0, TabledForIO, Attrs).
process_attribute(purity(Pure), Attrs0, Attrs) :-
set_purity(Attrs0, Pure, Attrs).
+process_attribute(terminates(Terminates), Attrs0, Attrs) :-
+ set_terminates(Attrs0, Terminates, Attrs).
process_attribute(max_stack_size(Size), Attrs0, Attrs) :-
add_extra_attribute(Attrs0, max_stack_size(Size), Attrs).
@@ -1345,6 +1351,8 @@
Flag = max_stack_size(Size)
; parse_purity_promise(Term, Purity) ->
Flag = purity(Purity)
+ ; parse_terminates(Term, Terminates) ->
+ Flag = terminates(Terminates)
;
fail
).
@@ -1410,6 +1418,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.20
diff -u -r1.20 term_errors.m
--- compiler/term_errors.m 25 Jun 2003 06:57:34 -0000 1.20
+++ compiler/term_errors.m 15 Jul 2003 06:11:13 -0000
@@ -112,9 +112,14 @@
; 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
+ % call Mercury. By default this is assumed to be
+ % non-terminating.
:- type term_errors__error == pair(prog_context, termination_error).
@@ -446,6 +451,14 @@
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."),
+ Piece3 = words("If you *know* that this is actually terminating"),
+ Piece4 = words("then use the `terminates' foreign code attribute"),
+ Piece5 = words("to supress this error."),
+ Pieces = [Piece1, Piece2, Piece3, Piece4, Piece5].
+
%----------------------------------------------------------------------------%
:- pred term_errors_var_bag_description(bag(prog_var)::in, prog_varset::in,
Index: compiler/term_traversal.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_traversal.m,v
retrieving revision 1.23
diff -u -r1.23 term_traversal.m
--- compiler/term_traversal.m 26 May 2003 09:00:10 -0000 1.23
+++ compiler/term_traversal.m 15 Jul 2003 06:09:17 -0000
@@ -103,6 +103,7 @@
:- import_module check_hlds__type_util.
:- import_module hlds__hlds_data.
+:- import_module hlds__error_util.
:- import_module bool, int, require.
@@ -190,15 +191,27 @@
traverse_goal(Else, Params, Info0, Info2),
combine_paths(Info1, Info2, Params, Info).
-traverse_goal_2(foreign_proc(_, CallPredId, CallProcId, Args, _,_,_),
- GoalInfo, Params, Info0, Info) :-
+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, _,
CallProcInfo),
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, Info0, 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, Info0, Info) :-
%
Index: compiler/term_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_util.m,v
retrieving revision 1.28
diff -u -r1.28 term_util.m
--- compiler/term_util.m 8 Oct 2003 05:12:39 -0000 1.28
+++ compiler/term_util.m 8 Oct 2003 05:14:34 -0000
@@ -189,6 +189,19 @@
:- pred get_context_from_scc(list(pred_proc_id)::in, module_info::in,
prog_context::out) is det.
+
+ % Succeeds iff the termination status of a procedure is known.
+:- pred is_termination_known(module_info, pred_proc_id).
+:- mode is_termination_known(in, in) is semidet.
+
+ % Succeeds iff the foreign proc attributes imply that a procedure
+ % terminates.
+:- pred attributes_imply_termination(pragma_foreign_proc_attributes).
+:- mode attributes_imply_termination(in) is semidet.
+
+ % Succeeds iff the given predicate is builtin or compiler generated.
+:- pred is_builtin_or_comp_gen(pred_info).
+:- mode is_builtin_or_comp_gen(in) is semidet.
%-----------------------------------------------------------------------------%
@@ -632,5 +645,22 @@
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).
+attributes_imply_termination(Attributes) :-
+ 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).
+is_builtin_or_comp_gen(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.30
diff -u -r1.30 termination.m
--- compiler/termination.m 26 Sep 2003 05:14:22 -0000 1.30
+++ compiler/termination.m 8 Oct 2003 05:30:08 -0000
@@ -114,35 +114,38 @@
%----------------------------------------------------------------------------%
-termination__pass(Module0, Module) -->
+termination__pass(!Module) -->
% Find out what norm we should use, and set up for using it
globals__io_get_termination_norm(TermNorm),
- { set_functor_info(TermNorm, Module0, FunctorInfo) },
+ { set_functor_info(TermNorm, !.Module, FunctorInfo) },
globals__io_lookup_int_option(termination_error_limit, MaxErrors),
globals__io_lookup_int_option(termination_path_limit, MaxPaths),
{ PassInfo = pass_info(FunctorInfo, MaxErrors, MaxPaths) },
% Process builtin and compiler-generated predicates,
% and user-supplied pragmas.
- { module_info_predids(Module0, PredIds) },
- check_preds(PredIds, Module0, Module1),
+ { module_info_predids(!.Module, PredIds) },
+ check_preds(PredIds, !Module),
% Process all the SCCs of the call graph in a bottom up order.
- { module_info_ensure_dependency_info(Module1, Module2) },
- { module_info_dependency_info(Module2, DepInfo) },
+ { module_info_ensure_dependency_info(!Module) },
+ { module_info_dependency_info(!.Module, DepInfo) },
{ hlds_dependency_info_get_dependency_ordering(DepInfo, SCCs) },
-
- % Ensure that termination pragmas for a proc. do conflict
- % with termination pragmas for other procs. in the same SCC.
- check_pragmas_are_consistent(SCCs, Module2, Module3),
+
+ % Set the termination status of foreign_procs.
+ check_foreign_code_attributes(SCCs, !Module),
+ % Ensure that the termination status for a proc. does not
+ % conflict with the termination status of other procs. in
+ % the same SCC.
+ check_pragmas_are_consistent(SCCs, !Module),
- termination__process_all_sccs(SCCs, Module3, PassInfo, Module),
+ termination__process_all_sccs(SCCs, !.Module, PassInfo, !:Module),
globals__io_lookup_bool_option(make_optimization_interface,
MakeOptInt),
( { MakeOptInt = yes } ->
- termination__make_opt_int(PredIds, Module)
+ termination__make_opt_int(PredIds, !.Module)
;
[]
).
@@ -163,6 +166,106 @@
find_weights(Module, WeightMap).
%----------------------------------------------------------------------------%
+
+% Set the termination status for any procedures implemented using the
+% foreign language interface. If the terminates/does_not_terminate attribute
+% has been set the we set the termination 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
+% terminates/does_not_terminate pragmas.
+
+:- pred check_foreign_code_attributes(list(list(pred_proc_id)), module_info,
+ module_info, io__state, io__state).
+:- mode check_foreign_code_attributes(in, in, out, di, 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), module_info,
+ module_info, io__state, io__state).
+:- mode check_foreign_code_attributes_2(in, in, out, di, uo) is det.
+
+check_foreign_code_attributes_2([], !Module, !IO).
+check_foreign_code_attributes_2([PPId | PPIds], !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(ProcInfo0,
+ yes(cannot_loop), ProcInfo)
+ ;
+ TermErr = Context - does_not_term_foreign(PPId),
+ proc_info_set_maybe_termination_info(ProcInfo0,
+ yes(can_loop([TermErr])), ProcInfo)
+ )
+ ;
+ % If there was a `pragma terminates'
+ % declaration for this predicate
+ % 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(ProcInfo0,
+ yes(can_loop([TermErr])), 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 attributes do not
+ % contradict this.
+ MaybeTermination = yes(can_loop(TermErrs0)),
+ ( terminates(Attributes, terminates) ->
+ TermErr = Context - inconsistent_annotations,
+ TermErrs = [TermErr | TermErrs0],
+ proc_info_set_maybe_termination_info(ProcInfo0,
+ yes(can_loop(TermErrs)), 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(!.Module, PPId, PredInfo,
+ ProcInfo, !:Module)
+ ;
+ true
+ ),
+ check_foreign_code_attributes_2(PPIds, !Module, !IO).
+
+%----------------------------------------------------------------------------%
% Check that any user-supplied termination information (from pragma
% terminates/does_not_terminate) is consistent for each SCC in the program.
%
@@ -267,14 +370,6 @@
PPIdStatus = can_loop(_)
),
check_procs_known_term(Status, PPIds, ModuleInfo).
-
- % Succeeds iff the termination status of a procedure is known.
-:- pred is_termination_known(module_info, pred_proc_id).
-:- mode is_termination_known(in, 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.279
diff -u -r1.279 reference_manual.texi
--- doc/reference_manual.texi 21 Aug 2003 07:01:16 -0000 1.279
+++ doc/reference_manual.texi 8 Sep 2003 04:17:54 -0000
@@ -5542,6 +5542,13 @@
@table @asis
+ at item @samp{terminates}/@samp{does_not_terminate}
+This attribute promises that the given predicate or function definition
+terminates or does not terminate. It is equivalent to the corresponding
+ at samp{pragma terminates} or @samp{pragma does_not_terminate} declaration.
+If omitted, the termination 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
@@ -8294,7 +8301,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
@@ -8313,14 +8320,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 does not terminate.
+
+The foreign code attributes @samp{terminate}/@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 the 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}).
@@ -8339,10 +8351,12 @@
@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.
+does not necessarily terminate. This declaration affects not only the
+predicate specified but also any other predicates that are mutually
+recursive with it.
+
+The following declaration can be used to force the compiler to prove
+the termination of a given predicate or function.
@example
:- pragma check_termination(@var{Name}/@var{Arity}).
Index: tests/term/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/term/Mmakefile,v
retrieving revision 1.21
diff -u -r1.21 Mmakefile
--- tests/term/Mmakefile 8 Oct 2003 05:12:40 -0000 1.21
+++ tests/term/Mmakefile 8 Oct 2003 05:14:42 -0000
@@ -22,6 +22,7 @@
existential_error1 \
existential_error2 \
fold \
+ foreign_valid \
my_list \
lte \
my_map \
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 8 Oct 2003 05:27:07 -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 Jul 2003 06:49:14 -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.8
diff -u -r1.8 Mercury.options
--- tests/warnings/Mercury.options 24 Jul 2003 07:59:46 -0000 1.8
+++ tests/warnings/Mercury.options 8 Oct 2003 05:57:52 -0000
@@ -34,9 +34,10 @@
MCFLAGS-infinite_recursion = --excess-assign --common-struct
MCFLAGS-warn_stubs = --allow-stubs --warn-unused-args
-
- # Conflicting termination pragmas won't show up unless we
- # perform termination analysis.
+
+ # Warnings about the various termination declarations will
+ # not show up unless we perform termination analysis.
MCFLAGS-pragma_term_conflict = --enable-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.32
diff -u -r1.32 Mmakefile
--- tests/warnings/Mmakefile 23 Jul 2003 03:38:17 -0000 1.32
+++ tests/warnings/Mmakefile 8 Oct 2003 05:20:18 -0000
@@ -6,6 +6,7 @@
COMPILE_PROGS= \
arg_order_rearrangment \
+ foreign_term_invalid \
pragma_term_conflict \
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 Jul 2003 06:57:12 -0000
@@ -0,0 +1,10 @@
+foreign_term_invalid.m:011: Warning:
+foreign_term_invalid.m:011: predicate `foreign_term_invalid.test1/1' mode 0
+foreign_term_invalid.m:011: has a pragma does_not_terminate declaration but
+foreign_term_invalid.m:011: also has the `terminates' foreign code attribute
+foreign_term_invalid.m:011: set.
+foreign_term_invalid.m:014: Warning:
+foreign_term_invalid.m:014: predicate `foreign_term_invalid.test2/1' mode 0
+foreign_term_invalid.m:014: has a pragma terminates declaration but also has
+foreign_term_invalid.m:014: the `does_not_terminate' foreign code attribute
+foreign_term_invalid.m:014: 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 15 Jul 2003 05:32:40 -0000
@@ -0,0 +1,25 @@
+
+ % 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;
+").
--------------------------------------------------------------------------
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