0000586: split switch arms issue

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000586

mercury

Bug

public

2026-09-24 17:49

2026-09-30 16:06

Reporter

wangp

Assigned To

wangp

Priority

normal

Severity

minor

Reproducibility

always

Status

resolved

Resolution

fixed

Product Version

Target Version

Fixed in Version

Summary

0000586: split switch arms issue

Description

The compiler aborts on the following test case when targeting a deep profiling grade and --split-switch-arms is enabled (at -O3).

% mmc -s asm_fast.gc.profdeep -O3 -C ssa_cutdown
% Uncaught Mercury exception:
% Software Error: predicate `ll_backend.code_gen.generate_goal'/7: Unexpected: semidet model in det context

Here is the HLDS dump after stage 050-determinism:

    ssa_cutdown.get_computed_align(Spec_4, Parent_5) = Val_6 :-
      % determinism: det
      ( % cannot_fail switch on Spec_4
      % Spec_4 has functor inherit/0
    % determinism: det
    ( % conjunction
      % determinism: det
      Val_6 = ssa_cutdown.start
      % new insts:
      % Val_6 -> unique(ssa_cutdown.start)
    )
    % new insts:
    % Val_6 -> unique(ssa_cutdown.start)
      ;
      % Spec_4 has functor initial/0 or value/1
    % determinism: det
    ( % conjunction
      % determinism: det
      ( % cannot_fail switch on Spec_4
      % Spec_4 has functor initial/0
        % determinism: det
        ( % conjunction
          % determinism: det
          Val0_7 = ssa_cutdown.auto
          % new insts:
          % Val0_7 -> unique(ssa_cutdown.auto)
        )
        % new insts:
        % Val0_7 -> unique(ssa_cutdown.auto)
      ;
      % Spec_4 has functor value/1
        % determinism: det
        Spec_4 = ssa_cutdown.value(Val0_7)
        % new insts:
        % Spec_4 -> bound(ssa_cutdown.value(ground))
        % Val0_7 -> ground
      )
      % new insts:
      % Spec_4 -> bound(ssa_cutdown.initial ; ssa_cutdown.value(ground))
      % Val0_7 -> ground
      ,
      % determinism: det
      Parent_5 = ssa_cutdown.parent(ParentVal_8)
      % new insts:
      % Parent_5 -> bound(ssa_cutdown.parent(ground))
      % ParentVal_8 -> ground
      ,
      % determinism: det
      ( % cannot_fail switch on Val0_7
      % Val0_7 has functor auto/0
        % determinism: det
        ( % conjunction
          % determinism: det
          Val_6 = ParentVal_8
          % new insts:
          % Val_6 -> ground
        )
        % new insts:
        % Val_6 -> ground
      ;
      % Val0_7 has functor computed/1
        % determinism: det
        Val0_7 = ssa_cutdown.computed(Val_6)
        % new insts:
        % Val_6 -> ground
        % Val0_7 -> bound(ssa_cutdown.computed(ground))
      )
      % new insts:
      % Val_6 -> ground
      % Val0_7 -> bound(ssa_cutdown.auto ; ssa_cutdown.computed(ground))
    )
    % new insts:
    % Spec_4 -> bound(ssa_cutdown.initial ; ssa_cutdown.value(ground))
    % Parent_5 -> bound(ssa_cutdown.parent(ground))
    % Val_6 -> ground
      ).
      % new insts:
      % Spec_4 -> bound(ssa_cutdown.inherit ; ssa_cutdown.initial ; ssa_cutdown.value(ground))
      % Val_6 -> ground

After stage 065-frontend_simplify, the "Spec_4 = initial|value" arm
has been split:

    ssa_cutdown.get_computed_align(Spec_4, Parent_5) = Val_6 :-
      % determinism: det
      ( % cannot_fail switch on Spec_4
      % Spec_4 has functor inherit/0
    % determinism: det
    Val_6 = ssa_cutdown.start
    % new insts:
    % Val_6 -> unique(ssa_cutdown.start)
      ;
      % Spec_4 has functor initial/0
    % determinism: det
    ( % conjunction
      % determinism: det
      Val0_7 = ssa_cutdown.auto
      % new insts:
      % Val0_7 -> ground <--- NOTE
      ,
      % determinism: det
      Parent_5 = ssa_cutdown.parent(ParentVal_8)
      % new insts:
      % Parent_5 -> bound(ssa_cutdown.parent(ground))
      % ParentVal_8 -> ground
      ,
      % determinism: det
      ( % cannot_fail switch on Val0_7
      % Val0_7 has functor auto/0
        % determinism: det
        Val_6 = ParentVal_8
        % new insts:
        % Val_6 -> ground
      ;
      % Val0_7 has functor computed/1
        % determinism: det
        Val0_7 = ssa_cutdown.computed(Val_6)
        % new insts:
        % Val_6 -> ground
      )
      % new insts:
      % Val_6 -> ground
      % Val0_7 -> bound(ssa_cutdown.auto ; ssa_cutdown.computed(ground))
    )
    % new insts:
    % Parent_5 -> bound(ssa_cutdown.parent(ground))
    % Val_6 -> ground
      ;
      % Spec_4 has functor value/1
    % determinism: det
    ( % conjunction
      % determinism: det
      Spec_4 = ssa_cutdown.value(Val0_9)
      % new insts:
      % Val0_9 -> ground
      ,
      % determinism: det
      Parent_5 = ssa_cutdown.parent(ParentVal_10)
      % new insts:
      % Parent_5 -> bound(ssa_cutdown.parent(ground))
      % ParentVal_10 -> ground
      ,
      % determinism: det
      ( % cannot_fail switch on Val0_9
      % Val0_9 has functor auto/0
        % determinism: det
        Val_6 = ParentVal_10
        % new insts:
        % Val_6 -> ground
      ;
      % Val0_9 has functor computed/1
        % determinism: det
        Val0_9 = ssa_cutdown.computed(Val_6)
        % new insts:
        % Val_6 -> ground
      )
      % new insts:
      % Val_6 -> ground
      % Val0_9 -> bound(ssa_cutdown.auto ; ssa_cutdown.computed(ground))
    )
    % new insts:
    % Parent_5 -> bound(ssa_cutdown.parent(ground))
    % Val_6 -> ground
      ).
      % new insts:
      % Spec_4 -> bound(ssa_cutdown.inherit ; ssa_cutdown.initial ; ssa_cutdown.value(ground))
      % Parent_5 -> ground
      % Val_6 -> ground

In the Spec_4 = initial case, the unification goal Val0_7 = ssa_cutdown.auto
still has Val0_7 with the inst 'ground' (instead of 'auto').
That leaves the switch on Val0_7 that follows with both cases intact,
even though one of the cases is not possible any more.
I think this is an issue, but not sure if it is *the* issue.

After the deep profiling transformation is applied,
the HLDS dump after stage hlds_dump.325-ll_backend_simplify looks like:

    ssa_cutdown.get_computed_align(Spec_4, Parent_5) = Val_6 :-
      % determinism: semidet
      ( % conjunction
        ...
        ,
        % determinism: semidet
        ( % cannot_fail switch on `Spec_4'
          % Spec_4 has functor inherit/0
          % determinism: det
          ...
        ;
          % Spec_4 has functor initial/0
          % determinism: semidet
          ( % conjunction
            % determinism: det
            CPIndex_18 = 2
            % new insts:
            % CPIndex_18 -> ground
            ,
            % determinism: det
            $pragma_foreign_proc(...)
            ,
            % determinism: det
            Parent_5 = ssa_cutdown.parent(ParentVal_8)
            % new insts:
            % Parent_5 -> bound(ssa_cutdown.parent(ground))
            % ParentVal_8 -> ground
            ,
            % determinism: det
            Val0_7 = ssa_cutdown.auto
            % new insts:
            % Val0_7 -> ground
            ,
            % determinism: semidet
            ( % cannot_fail switch on `Val0_7'
              % Val0_7 has functor auto/0
              % determinism: det
              ( % conjunction
                % determinism: det
                CPIndex_16 = 1
                % new insts:
                % CPIndex_16 -> ground
                ,
                % determinism: det
                $pragma_foreign_proc(...)
                ,
                % determinism: det
                Val_6 = ParentVal_8
                % new insts:
                % Val_6 -> ground
              )
              % new insts:
              % Val_6 -> ground
            ;
              % Val0_7 has functor computed/1
              % determinism: failure
              ( % conjunction
                % determinism: det
                Val0_7 = ssa_cutdown.computed(Val_6)
                % new insts:
                % Val_6 -> ground
                ,
                % determinism: failure <--- NOTE
                fail
                % new insts: unreachable
              )
              % new insts: unreachable
            )
            % new insts:
            % Val_6 -> ground
            % Val0_7 -> bound(ssa_cutdown.auto)
          )
          % new insts:
          % Parent_5 -> bound(ssa_cutdown.parent(ground))
          % Val_6 -> ground
        ;
          ...
        )
        ...
      ).

This time it sees that the switch on Val0_7 cannot match the computed/1
functor, and replaces the tail of the goal with a failure.
The failure propagates up and later leads to the sanity check failure
(semidet model in det context).

Tags

No tags attached.

Attached Files

ssa_cutdown.m (1,176 bytes) 2026-09-24 17:49

Relationships

Relationships

Notes
~0001263 wangp (developer) 2026-09-28 16:11	Actually, a better root cause is this. After the deep profiling transformation, the saved_vars_const pass runs and ends up duplicating the Val0_7 = auto construction unification after the switch on Val0_7. % determinism: det Val0_7 = ssa_cutdown.auto , % determinism: det ( % cannot_fail switch on Val0_7 % Val0_7 has functor auto/0 % determinism: det ( % conjunction % determinism: det CPIndex_16 = 1 , % determinism: det $pragma_foreign_proc ... , % determinism: det Val_6 = ParentVal_8 , % determinism: det ProcLayout_17 = <deep_profiling_proc_layout(pred 0, proc 0)> ) ; % Val0_7 has functor computed/1 % determinism: det Val0_7 = ssa_cutdown.computed(Val_6) ) , % determinism: det ProcLayout_19 = <deep_profiling_proc_layout(pred 0, proc 0)> , % determinism: det Val0_7 = ssa_cutdown.auto % <--- duplicated After the followcode pass moves the unification into the switch arms, simplification determines that the unification with 'auto' cannot succeed in the computed/1 arm, and replaces the goal with failure, making the entire switch semidet. This leads to the semidet model in a det context abort. A fix may be to prevent saved_vars_const from duplicating a goal that constructs Var after a [cannot_fail] switch on on the same Var, e.g. diff --git a/compiler/saved_vars.m b/compiler/saved_vars.m index 063bfac995..c69e873675 100644 --- a/compiler/saved_vars.m +++ b/compiler/saved_vars.m @@ -56,6 +56,7 @@ :- import_module hlds.hlds_pred. :- import_module hlds.hlds_proc_util. :- import_module hlds.hlds_rtti. +:- import_module hlds.make_goal. :- import_module hlds.passes_aux. :- import_module hlds.quantification. :- import_module parse_tree. @@ -491,7 +492,26 @@ saved_vars_delay_goal([Goal0 \| Goals0], Goals, Construct, Var, IsNonLocal, ; Goal0Expr = switch(SwitchVar, CF, Cases0), ( if SwitchVar = Var then - saved_vars_delay_goal(Goals0, Goals1, Construct, Var, + ( + CF = cannot_fail, + % If we duplicate a goal that constructs Var after a + % cannot_fail switch on Var, the goal may be duplicated + % into the switch arms. If simplification determines that + % the unification cannot succeed in one or more of the + % switch arms, it may be replaced with failure, and the + % switch changed from det to semidet. That can lead to + % problems if the switch was in a det context. + % To prevent that sequence of events, we do not duplicate + % a goal that constructs Var after a cannot_fail switch + % on the same Var. + Construct = hlds_goal(_, ConstructGoalInfo), + Context = goal_info_get_context(ConstructGoalInfo), + MaybeConstruct = true_goal(Context) + ; + CF = can_fail, + MaybeConstruct = Construct + ), + saved_vars_delay_goal(Goals0, Goals1, MaybeConstruct, Var, IsNonLocal, !SlotInfo), Goals = [Construct, Goal0 \| Goals1] else

~0001264 wangp (developer) 2026-09-30 16:06	Fixed by commit 5c61949fed

Notes

Date Modified	Username	Field	Change
Issue History
2026-09-24 17:49	wangp	New Issue
2026-09-24 17:49	wangp	File Added: ssa_cutdown.m
2026-09-28 16:11	wangp	Note Added: 0001263
2026-09-30 16:06	wangp	Assigned To	=> wangp
2026-09-30 16:06	wangp	Status	new => resolved
2026-09-30 16:06	wangp	Resolution	open => fixed
2026-09-30 16:06	wangp	Note Added: 0001264

Issue History