Mercury Bugs - mercury
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000414mercuryBugpublic2016-07-25 16:532016-07-29 03:42
Reporterpbone 
Assigned Tozs 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
Platformx86_64OSLinux MintOS Version18
Product Version 
Target VersionFixed in Version 
Summary0000414: The switch detection fails to detect this switch
DescriptionThe switch detection code fails to detect the larger switch, and instead detects a can_fail switch within a disjunction.

    Replay = Loader ^ loader_replay_options,
    (
        ( Replay = replay_none
        ; Replay = replay_save(_)
        ),
        Prefix = Loader ^ loader_prefix
    ;
        Replay = replay_load(_),
        Prefix = Loader ^ loader_replay_prefix
    ).

When I deconstruct Loader outside of the switch and assignment unifications within the switch things work correctly.
Steps To Reproduce$ mmc --allow-stubs --grade asm_fast.gc --compile-to-c testb.m -Dall -dall
testb.m:011: Error: invalid determinism for `prefix_locator'(in) = out:
testb.m:011: the primary mode of a function cannot be `nondet'.
testb.m:011: In `prefix_locator'(in) = out:
testb.m:011: error: implicit determinism declaration not satisfied.
testb.m:011: Declared `det', inferred `nondet'.
testb.m:034: The switch on Replay does not cover
testb.m:034: `replay_load'/1.
testb.m:037: Disjunction has multiple clauses with solutions.
testb.m:038: Unification of `Replay' and `testb.replay_load(V_7)' can fail.
For more information, recompile with `-E'.
Additional InformationMercury ROTD 2016-07-18
GCC 5.4.0 20160609
TagsNo tags attached.
Relationships
Attached Files? testb.m (888) 2016-07-25 16:53
https://bugs.mercurylang.org/file_download.php?file_id=261&type=bug

Notes
(0000899)
zs   
2016-07-25 19:33   
The reason why this happens is that this code exhibits a rare
combination of properties. (a) Both disjuncts of the outer disjunction
contain deconstruction unifications with both Loader and Prefix.
(b) Since Loader's first occurrence in the clause comes *before*
Prefix's first occurrence, it gets the lower variable number,
so switch detection tests whether the disjunction is a switch on
Loader first. (c) Because of point a, it finds that the answer is yes,
with no disjuncts left over. It therefore commits to convertion the
disjunction into a switch on Loader, not even looking to see whether
the disjunction is a switch on any other variable.

Switch detection is inherently incomplete: there will always be switches
that it cannot find, for the same kinds of reasons why determinism
analysis (say of a Turing machine simulator) cannot ever prove that
all det predicates are actually det. Therefore stopping the search
after we find an apparently-satisfactory switch configuration (such as
the switch on Loader appears to be in this case) is justifiable, and
it definitely was the right thing to do in in the 1990s, when this code
was written. Now that we have computer power to burn, we can choose
to keep looking. I will look into that.
(0000900)
pbone   
2016-07-25 21:31   
That's an interesting combination of properties, more complex than I expected, but I did wonder if it had something to do with Loader, and that due to the field access code it is deconstructed in 3 places.

Anyway, it's pretty rare and also easy enough to work around so there's no hurry at all.

Cheers.
(0000901)
zs   
2016-07-29 03:42   
Fix committed 2016 july 27.

Issue History
Date ModifiedUsernameFieldChange
2016-07-25 16:53pboneNew Issue
2016-07-25 16:53pboneFile Added: testb.m
2016-07-25 19:33zsNote Added: 0000899
2016-07-25 19:34zsAssigned To => zs
2016-07-25 19:34zsStatusnew => assigned
2016-07-25 21:31pboneNote Added: 0000900
2016-07-29 03:42zsNote Added: 0000901
2016-07-29 03:42zsStatusassigned => resolved
2016-07-29 03:42zsResolutionopen => fixed