Mercury Bugs - mercury
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000220mercuryBugpublic2011-10-05 14:582011-10-05 15:39
Reportercolanderman 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusnewResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0000220: Termination analysis produces spurious "termination constant of infinity" errors
DescriptionFor certain (not all) functions and/or predicates XXX and YYY, where YYY has :- pragma terminates set, termination analysis will report that:

"Termination of predicate XXX not proven for the following reason:
 It calls predicate YYY which has a termination constant of infinity."

and that:

"Termination constant of function YYY set to infinity for the following reason:
 It contains one or more predicates and/or functions imported from another module."

Expected behavior is that :- pragma terminates(YYY) causes the compiler to assume YYY terminates, regardless of its body.

This bug is not exhibited by all such predicates or functions; see attached test case.
Additional Information11.07-beta-2011-09-30
TagsNo tags attached.
Relationships
Attached Files? termination.m (885) 2011-10-05 14:58
https://bugs.mercurylang.org/file_download.php?file_id=130&type=bug
? termination.err (3,389) 2011-10-05 14:59
https://bugs.mercurylang.org/file_download.php?file_id=131&type=bug

Notes
(0000364)
colanderman   
2011-10-05 15:17   
Looking through the compiler source I think I understand why: because the output arguments of a function/predicate are considered as a whole. In the attached example, one output argument (which does decrease) is used, but the other (which is not known to decrease) is not. The compiler does not maintain enough info to distinguish the two, so it necessarily infers the worst case (infinite termination constant).

Perhaps :- pragma terminates() should allow optional setting of the termination constant for a given mode? Or should set it to 0?

Either way this is probably a wishlist item and not a bug per se.
(0000365)
colanderman   
2011-10-05 15:39   
Nevermind. I just found :- pragma termination_info, and --check-term2, which seems to obviate this need entirely. You guys are good at keeping secrets ;)

Issue History
Date ModifiedUsernameFieldChange
2011-10-05 14:58colandermanNew Issue
2011-10-05 14:58colandermanFile Added: termination.m
2011-10-05 14:59colandermanFile Added: termination.err
2011-10-05 15:17colandermanNote Added: 0000364
2011-10-05 15:39colandermanNote Added: 0000365