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

[Julien Fischer]

On Mon, 9 Feb 2004, Fergus Henderson wrote:

> On 09-Feb-2004, Julien Fischer <juliensf at students.cs.mu.OZ.AU> wrote:
> >
> > Index: compiler/prog_data.m
> ...
> > @@ -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.
>
> Please add some comments here explaining the purpose of this type.
>
Done. (see relative diff below).

> Also, please add some comments explaining the exact meaning of the
> different alternatives.  In particular, does "does_not_terminate" mean
> that *every* call to the procedure will not terminate, or just that
> *some* calls (with particular arguments) will not terminate?
>
Either one depending on the procedure.  The point is that
it does not terminate for all input.  Whether or not it terminates
for some input and not for other input or it does not terminate for
any input is not relevant here.
I've added the comments to the type clarifying all this.

...
> If the latter, then wouldn't it be better to spell it
> "may_not_terminate" rather than "does_not_terminate"?
>

I called it that because the corresponding pragma is `does_not_terminate'.
I don't think it would be a good idea to have different names
for the two things.

> > Index: compiler/term_errors.m
> ...
> > +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].
>
> s/makes/may make/
>
Done.

> > Index: compiler/term_util.m
> ...
> > +	% Succeeds if the given predicate is builtin or compiler generated.
> > +:- pred is_builtin_or_comp_gen(pred_info::in) is semidet.
>
> The term "builtin" is not well-defined.
> Please explain exactly what is meant here.
>
This predicate is unnecessary (see below). I've deleted it.
(In this context builtin refers to things that the termination analyser
assumes terminate).

> > Index: compiler/termination.m
> ...
> > +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, _, _, _, _, _, _)
>
> Why do you need to call "not is_builtin_or_comp_gen" here?
> (Please add a comment explaining that.)
>
We don't need it.  It was something that I thought was necessary at
one point and then forgot to delete.  It's gone.

> > +	->
> > +		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
> > +			)
>
> Should that be an error, rather than just a warning?
>

"Errors" similar to this, e.g. inconsistent pragmas for mutually recursive
procedures, are currently all warnings.

If this is to made an error then there are a number of other things
that ought to be errors as well.  Unless anyone feels strongly
about the matter, I'll leave it as is.

> > 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.
>
> I suggest s/pragma does_not_terminate/`pragma does_not_terminate'/.
>
Done.


Relative diff follows:

diff -u compiler/prog_data.m compiler/prog_data.m
--- compiler/prog_data.m	4 Feb 2004 05:48:45 -0000
+++ compiler/prog_data.m	10 Feb 2004 04:24:59 -0000
@@ -887,11 +887,22 @@
 		% we explicitly store the name because we need the real
 		% name in code_gen

+	% This type specifies the termination property of a procedure
+	% defined using pragma c_code or pragma foreign_proc.
 :- type terminates
 	--->	terminates
+			% The foreign code will terminate for all input.
+			% (assuming any input streams are finite).
+
 	;	does_not_terminate
+			% The foreign code will not necessarily terminate for
+			% some (possibly all) input.
+
 	;	depends_on_mercury_calls.
-
+			% The termination of the foreign code depends
+			% on whether the code makes calls back to Mercury
+			% (See termination.m for details).
+
 :- type pragma_foreign_proc_extra_attribute
 	--->	max_stack_size(int).

diff -u compiler/term_errors.m compiler/term_errors.m
--- compiler/term_errors.m	6 Feb 2004 07:42:00 -0000
+++ compiler/term_errors.m	9 Feb 2004 07:49:29 -0000
@@ -453,7 +453,7 @@

 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."),
+	Piece2 = words("may make one or more calls back to Mercury."),
 	Pieces = [Piece1, Piece2].

 %----------------------------------------------------------------------------%
diff -u compiler/term_util.m compiler/term_util.m
--- compiler/term_util.m	4 Feb 2004 06:06:33 -0000
+++ compiler/term_util.m	9 Feb 2004 08:08:57 -0000
@@ -146,9 +146,6 @@
 :- 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
@@ -380,11 +377,4 @@
 	).

-is_builtin_or_comp_gen(PredInfo) :-
-	(
-		pred_info_is_builtin(PredInfo)
-	;
-		pred_info_get_maybe_special_pred(PredInfo, yes(_))
-	).
-
 %-----------------------------------------------------------------------------%

diff -u compiler/termination.m compiler/termination.m
--- compiler/termination.m	4 Feb 2004 06:52:15 -0000
+++ compiler/termination.m	9 Feb 2004 08:08:32 -0000
@@ -180,7 +180,6 @@
 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, _, _, _, _, _, _)
 	->
@@ -210,7 +209,7 @@
 					ProcInfo),
 				error_util__describe_one_proc_name(!.Module,
 					PPId, ProcName),
-				Piece1 = words("has a pragma terminates"),
+				Piece1 = words("has a `pragma terminates'"),
 				Piece2 = words("declaration but also has the"),
 				Piece3 = words("`does_not_terminate' foreign"),
 				Piece4 = words("code attribute set."),
@@ -235,7 +234,7 @@
 			        ProcInfo0, ProcInfo),
 			    error_util__describe_one_proc_name(!.Module,
 			        PPId, ProcName),
-			    Piece1 = words("has a pragma does_not_terminate"),
+			    Piece1 = words("has a `pragma does_not_terminate'"),
 			    Piece2 = words("declaration but also has the"),
 			    Piece3 = words("`terminates' foreign code"),
 			    Piece4 = words("attribute set."),
diff -u tests/warnings/foreign_term_invalid.exp tests/warnings/foreign_term_invalid.exp
--- tests/warnings/foreign_term_invalid.exp	4 Feb 2004 06:52:52 -0000
+++ tests/warnings/foreign_term_invalid.exp	9 Feb 2004 08:17:23 -0000
@@ -3,8 +3,8 @@
-foreign_term_invalid.m:009:   has a pragma does_not_terminate declaration but
+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.
+foreign_term_invalid.m:010:   has a `pragma terminates' declaration but also
+foreign_term_invalid.m:010:   has the `does_not_terminate' foreign code
+foreign_term_invalid.m:010:   attribute set.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------