|View Issue Details [ Jump to Notes ]||[ Issue History ] [ Print ]|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0000414||mercury||Bug||public||2016-07-25 16:53||2016-07-29 03:42|
|Platform||x86_64||OS||Linux Mint||OS Version||18|
|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: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.|
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.
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.
|Fix committed 2016 july 27.|
|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|