[m-rev.] for review: add terminates/does_not_terminate foreign proc attributes
Julien Fischer
juliensf at students.cs.mu.OZ.AU
Tue Jul 15 16:20:17 AEST 2003
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 and
and also make the termination analyser assume (in the absence of
either termination pragmas or foreign proc attributes) that foreign
procs that do not call Mercury are terminating and those that are declared
to call Mercury are non-terminating.
Note: Several modules in the standard library may require modification
after this change because the default termination status of those
foreign procs. that may call Mercury will change.
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.
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.
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 new behaviour of the termination analysis.
Index: compiler/hlds_pred.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_pred.m,v
retrieving revision 1.128
diff -u -r1.128 hlds_pred.m
--- compiler/hlds_pred.m 23 Jun 2003 17:02:54 -0000 1.128
+++ compiler/hlds_pred.m 14 Jul 2003 05:29:17 -0000
@@ -858,6 +858,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.
@@ -1384,6 +1387,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.94
diff -u -r1.94 prog_data.m
--- compiler/prog_data.m 17 Jun 2003 07:53:28 -0000 1.94
+++ compiler/prog_data.m 18 Jun 2003 04:07:46 -0000
@@ -721,6 +721,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.
@@ -746,6 +749,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.
@@ -779,6 +786,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
@@ -1219,9 +1231,10 @@
---> attributes(
foreign_language :: foreign_language,
may_call_mercury :: may_call_mercury,
- thread_safe :: thread_safe,
+ thread_safe :: thread_safe,
tabled_for_io :: tabled_for_io,
- purity :: purity,
+ purity :: purity,
+ terminates :: terminates,
% there is some special case behaviour for
% pragma c_code and pragma import purity
% if legacy_purity_behaviour is `yes'
@@ -1233,7 +1246,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).
@@ -1245,6 +1258,8 @@
purity(Attrs, Attrs ^ purity).
+terminates(Attrs, Attrs ^ terminates).
+
legacy_purity_behaviour(Attrs, Attrs ^ legacy_purity_behaviour).
set_may_call_mercury(Attrs0, MayCallMercury, Attrs) :-
@@ -1262,6 +1277,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.
@@ -1270,7 +1288,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"
@@ -1308,8 +1326,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.25
diff -u -r1.25 term_util.m
--- compiler/term_util.m 26 May 2003 09:00:10 -0000 1.25
+++ compiler/term_util.m 15 Jul 2003 05:40:51 -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.
%-----------------------------------------------------------------------------%
@@ -626,5 +639,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.29
diff -u -r1.29 termination.m
--- compiler/termination.m 25 Jun 2003 06:57:34 -0000 1.29
+++ compiler/termination.m 15 Jul 2003 06:12:09 -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,104 @@
find_weights(Module, WeightMap).
%----------------------------------------------------------------------------%
+% Set the termination status for any procedures defined in foriegn languages.
+% If the terminates/does_not_terminate attribute has been set the we
+% set the termination accordingly, otherwise as 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)
+ )
+ ;
+ % In this case there was a `pragma terminates'
+ % declaration. 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.
%
@@ -258,14 +359,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.276
diff -u -r1.276 reference_manual.texi
--- doc/reference_manual.texi 25 Jun 2003 06:57:34 -0000 1.276
+++ doc/reference_manual.texi 14 Jul 2003 06:01:24 -0000
@@ -5543,6 +5543,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
@@ -8295,7 +8302,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
@@ -8314,14 +8321,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}).
@@ -8340,10 +8352,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.20
diff -u -r1.20 Mmakefile
--- tests/term/Mmakefile 25 Jun 2003 06:57:34 -0000 1.20
+++ tests/term/Mmakefile 4 Jul 2003 06:52:48 -0000
@@ -20,6 +20,7 @@
dds3_17 \
dds3_8 \
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 15 Jul 2003 05:31:48 -0000
@@ -0,0 +1,74 @@
+:- 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;
+").
+
+
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.7
diff -u -r1.7 Mercury.options
--- tests/warnings/Mercury.options 25 Jun 2003 06:57:35 -0000 1.7
+++ tests/warnings/Mercury.options 4 Jul 2003 06:55:35 -0000
@@ -34,7 +34,8 @@
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
Index: tests/warnings/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/warnings/Mmakefile,v
retrieving revision 1.31
diff -u -r1.31 Mmakefile
--- tests/warnings/Mmakefile 25 Jun 2003 06:57:34 -0000 1.31
+++ tests/warnings/Mmakefile 4 Jul 2003 06:57:39 -0000
@@ -6,6 +6,7 @@
COMPILE_PROGS= \
arg_order_rearrangment \
+ foreign_term_invalid \
pragma_term_conflict
ERRORCHECK_PROGS= \
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