Actions in P4light appear dynamically scoped

[hackedy]

I think the P4light semantics isn't implementing lexical scoping for actions and it's breaking type safety. For instance, in stf-test/custom-stf-tests/dynamic.p4 this code actually assigns the boolean x to the header field hdr.h.x. That field is supposed to be a bit<8> and later operations involving it fall apart because they get a ValBaseBool instead.

control IngressI(inout H hdr, inout M meta, inout std_meta_t std_meta) {
  bit<8> x = hdr.h.x;
  action nop() { hdr.h.x = x; }
  bool x;
  apply {
    nop();
    std_meta.egress_spec = 9;
  }
}

The error message I get for the corresponding STF test:

[failure] bool list of irregular length 1 passed to bits_to_string
          Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
          Called from Petr4__Stf.run_test in file "lib/stf.ml", line 39, characters 22-70
          Called from Petr4test__Test.stf_alco_test.run_stf_alcotest in file "stf-test/test.ml", line 109, characters 30-64
          Called from Alcotest_engine__Core.Make.protect_test.(fun) in file "src/alcotest-engine/core.ml", line 180, characters 17-23
          Called from Alcotest_engine__Monad.Identity.catch in file "src/alcotest-engine/monad.ml", line 24, characters 31-35

[QinshiWang]

bit<8> x;
bool x;

looks invalid to me.

[jnfoster]

@QinshiWang the spec does not say that duplicate declarations are illegal, although `p4c enforces that condition.

@hackedy does the dynamic scoping still occur if you do it like this?

header h_t {
  bit<8> f;
}

control C(inout h_t h) {
  bit<8> x = 0xFF;
  action nop() { h.f = x; }
  apply {
    nop();
  }   
}

control D() {
  h_t h;
  bool x = true;
  C() c;
  apply {
    c.apply(h);
  }
}

This program passes p4test.

[QinshiWang]

I think it's reasonable to restrict no duplicated names in the same scope except overloading.

I believe the example above is handled correctly.

[hackedy]

Yeah I think that's handled correctly because the different x variables will come with different locators due to being defined in different scopes. I'll add it to the repo as an STF test though to make sure.

[hackedy]

If we want to reject duplicate names in the same scope then this is a typechecker bug and we should fix the typechecker to throw an error for duplicate names.

[jnfoster]

My reading of the spec is that it does not mandate an error on duplicate names. So I would prefer us not to add the check in Petr4.

[hackedy]

Relevant issues: p4lang/p4-spec#974, p4lang/p4c#1932.

[hackedy]

This works in P4light too.

control C(inout h_t h, in bool x) {
  bit<8> x = 0xFF;
  action nop() { h.f = x; }
  apply {
    nop();
  }   
}

control MyIngress(inout hdr_t hdr,
                  inout metadata meta,
                  inout standard_metadata_t standard_metadata) {
  C() c;
  apply {
    c.apply(hdr.h, false);
  }
}

[jnfoster]

@hackedy works == lexical scope?

[QinshiWang]

Yeah I think that's handled correctly because the different x variables will come with different locators due to being defined in different scopes. I'll add it to the repo as an STF test though to make sure.

Your understanding is not correct. Indeed, my first version of locator assigned different locators in this case. But the current version assigns x for both of them. They are distinguished because they are in different control blocks and calling a control block starts a new stack frame.

[QinshiWang]

https://github.com/verified-network-toolchain/petr4/issues/393#issuecomment-1430451715 I guess this works just because you're lucky. This won't work:

control C(inout h_t h, in bool x) {
  action nop() { h.f = x ? 0 : 1; }
  bit<8> x = 0xFF;  
  apply {
    nop();
  }   
}

control MyIngress(inout hdr_t hdr,
                  inout metadata meta,
                  inout standard_metadata_t standard_metadata) {
  C() c;
  apply {
    c.apply(hdr.h, false);
  }
}

[QinshiWang]

If we want to allow duplicated and shadowing names in the same scope, we can do that in locator generation, although I think it's a very bad language design.

[jnfoster]

FWIW, OCaml has this, and it's a much-loved feature. So I disagree with the sweeping statement.

[QinshiWang]

Yes. In OCaml, this is well-accepted, for two reasons: (1) one cannot reassign a variable in OCaml; (2) it is a common practice of functional programming. But IMO, P4 is more like C/Java. It's what I expect for P4 users.

[hackedy]

Rust supports shadowing within one scope, so it's not unheard of for an imperative language. I was curious so I looked at a couple textbook treatments of imperative programs with block structure. In Mitchell's Foundations of Programming Languages block structure is desugared into a lambda calculus with refs. So it handles shadowing smoothly but involves what appears to be a heap, which has to have locations allocated and deallocated on block boundaries. In Harper's PFPL treatment of "Idealized Algol" everything within a given scope must have distinct names, but the text suggests first renaming to avoid clashes. In Reynolds' "Essence of Algol," which is what both of these are based on, I think variables can be repeated, but it's a little hard for me to tell.

[QinshiWang]

How about control plan names? For example,

control C(inout h_t h, in bool x) {
  ...
}

control MyIngress(inout hdr_t hdr,
                  inout metadata meta,
                  inout standard_metadata_t standard_metadata) {
  C() c;
  C() c;
  apply {
    c.apply(hdr.h, false);
  }
}

[jnfoster]

If this is allowed, I think the second c should be the one named ... .c ... in the control-plane API. If access to the first c is needed, then a @name(...) annotation would be needed.

[QinshiWang]

I think the manual says, if both two cs has controllable entities, which are

value sets tables keys actions extern instances

then this program is not allowed without a @name clause. If at most one of them has controllable entities, then it's fine.