p4lang / p4-spec

Apache License 2.0
177 stars 80 forks source link

Should it be legal to have a reference of an extern type name within the definition of that extern? #1262

Open jafingerhut opened 1 year ago

jafingerhut commented 1 year ago

The latest open source p4test as of 2023-Jul-21 source p4lang/p4c source code allows this definition of an extern without any errors or warnings, as I would expect:

extern Foo {
    Foo();
}

extern Bar {
    Bar();

    // Legal according to p4test and P4_16 language spec:
    void m1(Foo x);
}

but this one causes an error:

extern Bar {
    Bar();

    // Language spec doesn't explicitly say whether the following is
    // legal, but as of 2023-Jul-24, p4test gives error
    // "Self-referencing types not supported: 'Bar' within
    // 'Bar':
    void m2(Bar x);
}

Full example v1model program is attached to this issue.

Is there some subtlety in formally defining a type system for P4 that anyone is aware of, and/or a difficulty in implementing type checking in open source p4c, by allowing such self-referencing extern types? [Uploading test-extern-as-parameter-to-extern-method-call.p4.txt…]()

apinski-cavium commented 1 year ago

I asked if the first example should really be valid before https://github.com/p4lang/p4-spec/issues/1087

There is another place which talks about when names are defined I thought.

jafingerhut commented 1 year ago

@mihaibudiu Do you have any knowledge of whether this p4c limitation is a minor or fundamental issue in p4c?

mihaibudiu commented 1 year ago

In general we want to avoid defining recursive types, so that's a good reason prohibiting references to a type which within the definition of itself. But this construct is not leading to a recursive type, and it is possible it could be accepted. Perhaps a Petra model would be a better answer.

jnfoster commented 1 year ago

Petr4 accepts this program.

I haven't done a formal proof, but I don't believe allowing an extern to take an arguments of its own type is dangerous from a non-termination perspective. Once the computation is off in extern land, we already make no claims about semantic restrictions.

jnfoster commented 1 year ago

In fact, p4test accepts this variant...

extern Bar {
  Bar();
  void m2<T>(T x);
}

control C() {
  Bar() b;
  apply {
    b.m2<Bar>(b);
  }
}

H/T @rcgoodfellow for coming up with it.

jafingerhut commented 1 year ago

For reference, attached is a complete v1model architecture program that gives no error when you run p4test on it, based upon Nate's example in the previous comment (I only changed the name of the method from m2 to add_dependency).

test-extern-as-parameter-to-extern-method-call-v2.p4.txt

jnfoster commented 11 months ago

Changes needed to close this issue.