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

Reporter

wangp

Assigned To

Priority

normal

Severity

minor

Reproducibility

always

Status

new

Resolution

open

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).

Date Modified	Username	Field
Issue History
2026-09-24 17:49	wangp	New Issue
2026-09-24 17:49	wangp	File Added: ssa_cutdown.m

Relationships

Notes
There are no notes attached to this issue.