[m-rev.] for review: Fix for semidet in det context abort (Mantis bug #586).

[Peter Wang]

There was a rare interaction between the saved vars const, follow code,
and simplification passes that led to a "semidet model in det context"
abort in the low-level code generator. I could only reproduce the
problem in deep profiling grades with the split-switch-arms pass enabled.

compiler/saved_vars.m:
    Do not duplicate a goal to construct a Var (where it is assigned a
    constant value) after a switch on the same Var.

tests/valid/Mercury.options:
tests/valid/Mmakefile:
tests/valid/bug586.m:
    Add test case.

diff --git a/compiler/saved_vars.m b/compiler/saved_vars.m
index 063bfac995..4f1e0b5e5d 100644
--- a/compiler/saved_vars.m
+++ b/compiler/saved_vars.m
@@ -489,15 +489,36 @@ saved_vars_delay_goal([Goal0 | Goals0], Goals, Construct, Var, IsNonLocal,
                 IsNonLocal, !SlotInfo),
             Goals = [Goal1 | Goals1]
         ;
-            Goal0Expr = switch(SwitchVar, CF, Cases0),
+            Goal0Expr = switch(SwitchVar, CanFail, Cases0),
             ( if SwitchVar = Var then
-                saved_vars_delay_goal(Goals0, Goals1, Construct, Var,
-                    IsNonLocal, !SlotInfo),
+                (
+                    IsNonLocal = yes,
+                    % If this is a switch on Var, and Var is a non-local
+                    % variable, then insert the goal that constructs Var here,
+                    % and do not duplicate the construction at the end of the
+                    % conjunction.
+                    %
+                    % Otherwise, the following sequence of events could occur:
+                    % 1. The Construct goal is duplicated after the switch.
+                    % 2. The follow_code pass duplicates the Construct goal
+                    % into each of the switch arms.
+                    % 3. In one or more switch arms, the duplicated goal is
+                    % simplified to a fail goal, as it unifies Var with a
+                    % functor that cannot occur in that switch arm.
+                    % 4. The switch becomes semidet, which leads to an abort in
+                    % the code generator if the switch occurs in a det context.
+                    Goals1 = Goals0
+                ;
+                    IsNonLocal = no,
+                    saved_vars_delay_goal(Goals0, Goals1, Construct, Var,
+                        IsNonLocal, !SlotInfo)
+                ),
                 Goals = [Construct, Goal0 | Goals1]
             else
                 push_into_cases_rename(Cases0, Cases, Construct, Var,
                     !SlotInfo),
-                Goal1 = hlds_goal(switch(SwitchVar, CF, Cases), Goal0Info),
+                Goal1 = hlds_goal(switch(SwitchVar, CanFail, Cases),
+                    Goal0Info),
                 saved_vars_delay_goal(Goals0, Goals1, Construct, Var,
                     IsNonLocal, !SlotInfo),
                 Goals = [Goal1 | Goals1]
diff --git a/tests/valid/Mercury.options b/tests/valid/Mercury.options
index 146d81b9dd..871778e112 100644
--- a/tests/valid/Mercury.options
+++ b/tests/valid/Mercury.options
@@ -56,6 +56,7 @@ MCFLAGS-bug493                      += --loop-invariants
 MCFLAGS-bug512                      += -O5 --intermodule-optimization
 MCFLAGS-bug539                      += --optimize-constructor-last-call
 MCFLAGS-bug544                      += -O5
+MCFLAGS-bug586                      += --optimize-saved-vars-const --follow-code
 MCFLAGS-compl_unify_bug             += -O3
 MCFLAGS-constraint_prop_bug         += -O0 --common-struct
 MCFLAGS-constraint_prop_bug         += --local-constraint-propagation
diff --git a/tests/valid/Mmakefile b/tests/valid/Mmakefile
index 00347e9a2e..9783276b28 100644
--- a/tests/valid/Mmakefile
+++ b/tests/valid/Mmakefile
@@ -140,6 +140,7 @@ OTHER_PROGS = \
 	bug539 \
 	bug544 \
 	bug572 \
+	bug586 \
 	bug85 \
 	builtin_false \
 	call_failure \
diff --git a/tests/valid/bug586.m b/tests/valid/bug586.m
new file mode 100644
index 0000000000..97a1216274
--- /dev/null
+++ b/tests/valid/bug586.m
@@ -0,0 +1,83 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+%
+% This is a regression test for Mantis bug #586. A rare interaction between
+% the saved vars const, follow code and simplification passes led to an abort
+% in the code generator. The problem has only been observed in deep profiling
+% grades with the split switch arms pass enabled, but otherwise is not
+% related.
+%
+%   Uncaught Mercury exception:
+%   Software Error: predicate `ll_backend.code_gen.generate_goal'/7:
+%   Unexpected: semidet model in det context
+%
+% The problem is this. After the deep profiling transformation,
+% the saved_vars_const pass runs and tries to delay the construction of Val0.
+% When it gets to the switch, Val0 is required, so it is constructed,
+% but because Val0 is a non-local variable, it also duplicated the
+% construction goal at the end of the conjunction.
+%
+%   Val0 = auto,    % construction goal
+%   ( % cannot_fail switch on Val0
+%       Val0 = auto,
+%       ...
+%   ;
+%       Val0 = computed(Val)
+%   ),
+%   ... ,
+%   Val0 = auto     % duplicated construction goal
+%
+% After the followcode pass moves the unification into the switch arms,
+% simplification determines that the unification "Val0 = auto" cannot succeed
+% in the computed/1 arm, and replaces it with failure, making the entire
+% switch semidet. This leads to the "semidet model in a det context" abort.
+
+:- module bug586.
+:- interface.
+
+:- type parent
+    --->    parent(
+                align :: align
+            ).
+
+:- type unresolved_spec
+    --->    initial
+    ;       inherit
+    ;       value(spec_align).
+
+:- type spec_align
+    --->    computed(align)
+    ;       auto.
+
+:- type align
+    --->    start
+    ;       end.
+
+:- func get_computed_align(unresolved_spec, parent) = align.
+
+%--------------------------------------------------------------------%
+
+:- implementation.
+
+get_computed_align(Spec, Parent) = Val :-
+    (
+        Spec = inherit,
+        Val = start
+    ;
+        (
+            Spec = initial,
+            Val0 = auto
+        ;
+            Spec = value(Val0)
+        ),
+        ParentVal = Parent ^ align,
+        (
+            Val0 = auto,
+            Val = ParentVal
+        ;
+            Val0 = computed(Val)
+        )
+    ).
+
+%--------------------------------------------------------------------%
-- 
2.54.0