Fails to reject duplicate switch labels

[KunJeong]

According to 12.7.3. of the spec, duplicate switch labels are not allowed:

12.7.3. Notes common to all switch statements
It is a compile-time error if two labels of a switch statement equal each other.

However, p4test does not print any errors for the following program:

extern bit<8> baz();
control c()() {
  apply {
    switch (baz()) {
      1: {}
      1: {}
    }
  }
}

[KunJeong]

I've modified this into a minimal reproducible example in which the control does not get removed. The I followed the transformations done by the compiler to isolate the root cause.

Step 1: Initial program

#include <core.p4>

control C();
package Pkg(C c);
extern bit<8> baz();
control c() {
  apply {
    switch (baz()) {
      1: {}
      1: {}
    }
  }
}
Pkg(c()) main;

Step 2: "0131-SideEffectOrdering_1_DoSimplifyExpressions"

This pass inserts temporary variables for the switch key.

#include <core.p4>

control C();
package Pkg(C c);
extern bit<8> baz();
control c() {
  bit<8> tmp;
  apply {
    tmp = baz();
    switch (tmp) {
      1: {}
      1: {}
    }
  }
}
Pkg(c()) main;

Step 3: "0507-EliminateSwitch_1_DoEliminateSwitch"

The duplicate switch label is transformed into duplicate keys for entries, and this is left untouched until the last pass.

#include <core.p4>

extern bit<8> baz();
control C();
package Pkg(C c);
control c() {
    @name("c.tmp") bit<8> tmp;
    bit<8> switch_0_key;
    @hidden action switch_0_case() {
    }                                                                                        
    @hidden action switch_0_case_0() {
    }
    @hidden action switch_0_case_1() {
    }
    @hidden table switch_0_table {
        key = {
            switch_0_key: exact;
        }
        actions = {
            switch_0_case();
            switch_0_case_0();
            switch_0_case_1();
        }
        const default_action = switch_0_case_1();
        const entries = {
                        const 8w1 : switch_0_case();
                        const 8w1 : switch_0_case_0();
        }
    }
    apply {
        tmp = baz();
        {
            switch_0_key = tmp;
            switch (switch_0_table.apply().action_run) {
                switch_0_case: {
                }
                switch_0_case_0: {
                }
                switch_0_case_1: {
                }
            }
        }
    }
}

Pkg(c()) main;

Note that with testdata/p4_16_errors/duplicate_label.p4, the duplicate label is caught in pass "0018-FrontEnd_13_(anonymous namespace)::SetStrictStruct". The only difference is that duplicate_label.p4 uses table apply action_run as the switch key.

// duplicate_label.p4

control c(out bit arun) {
    action a() {}
    table t {
        actions = { a; }
        default_action = a;
    }
    apply {
        switch (t.apply().action_run) {
            a: { arun = 1; }
            a: { arun = 1; }  // duplicate label
        }
    }
}

I hope this helps in isolating the root cause.