0000414: The switch detection fails to detect this switch

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000414

mercury

Bug

public

2016-07-25 16:53

2016-07-29 03:42

Reporter

pbone

Assigned To

Priority

normal

Severity

minor

Reproducibility

always

Status

resolved

Resolution

fixed

Platform

x86_64

Linux Mint

OS Version

Product Version

Target Version

Fixed in Version

Summary

0000414: The switch detection fails to detect this switch

Description

The 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 Information

Mercury ROTD 2016-07-18
GCC 5.4.0 20160609

Tags

No tags attached.

Attached Files

testb.m (888 bytes) 2016-07-25 16:53

Relationships

Relationships

Notes
~0000899 zs (developer) 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 (administrator) 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 (developer) 2016-07-29 03:42	Fix committed 2016 july 27.

Notes

Date Modified	Username	Field	Change
Issue History
2016-07-25 16:53	pbone	New Issue
2016-07-25 16:53	pbone	File Added: testb.m
2016-07-25 19:33	zs	Note Added: 0000899
2016-07-25 19:34	zs	Assigned To	=> zs
2016-07-25 19:34	zs	Status	new => assigned
2016-07-25 21:31	pbone	Note Added: 0000900
2016-07-29 03:42	zs	Note Added: 0000901
2016-07-29 03:42	zs	Status	assigned => resolved
2016-07-29 03:42	zs	Resolution	open => fixed

Issue History