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

[Fergus Henderson]

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.

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?

If the former, then what is the user supposed to do for procedures
that terminate for some arguments but not for others?

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

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

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

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

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

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

Likewise here?

> 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'/.

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

Likewise.


Otherwise that change looks fine.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------