Type unification fails with untyped integers.

[ChrisDodd]

When trying to infer types to a type-abstract extern function, unification fails if the extern is called with an untyped integer:

extern void func<T>(in T x);

control proto();
package top(proto _p);

control c() {
    apply {
        func(5);
    }
}

top(c()) main;

gives an error

t.p4(9): error: func: cannot infer type for type parameter T
        func(5);
        ^^^^^^^
t.p4(2)
extern void func<T>(in T x);
                 ^

(using a typed integer, eg 8w5 works fine).

This is an area that the spec doesn't really talk about, as we've deliberately tried to avoid getting into complex type inferencing issues. It kind-of makes sense to have untyped integers not infer a type for their argument, but it makes it inconvenient to have type-"friendly" methods in an architecture (extern functions that can take any type of argument without requiring an explicit cast), which can't then work with untyped integer constants.

[mihaibudiu]

I think that this is the correct behavior. Since this invocation is executed at runtime, the type of the argument must be specified. Note that we should allow int values for constructors.

[jafingerhut]

I don't know the type-checking intricacies in today's compiler, or whether there are more fundamental issues involved here, but the compiler does allow assignments to an lvalue of type bit or int, with a right-hand side that is an expression of type int (unlimited precision).

Is there a reason that such 'auto-conversion from int to bit or int' is more difficult when the int is a parameter to an extern?

[mihaibudiu]

The parameter in question has a type given by a type variable. The assignment is used to guess the value of the type variable. For some type variables we cannot allow the type to be int.

[jafingerhut]

Got it. Thanks for the explanation.

[jnfoster]

Sorry, now I'm getting confused. Are we saying that a polymorphic function like f is not actually polymorphic?

I like to think of int as the union of bit<k> for all k (or perhaps, up to the maximum width values supported on the target). So if f doesn't work for int, it follows that there must exist a k such that it does not work for bit<k> either. (Suppose not, then f works for all bit<k> and therefore also for int). How would the type inference algorithm know that it should produce a failure for bit<k> x = n; f(x); or equivalently for f(kwn) too?

[jnfoster]

I realize that some externs assume their (generic) arguments are struct-like types, etc. -- e.g., consider packet_in. Yet because our type system lacks constraints on type variables, we cannot express those conditions directly in the language. Hence, we have to use run-time checks in the extern itself. (We can and have added more precise typing rules for built-in externs like packet_in as special cases in the compiler, but the front-end won't know about third-party architectures. So I think a run-time check is the only option in general).

But that's not the issue here -- we're just talking about being polymorphic over numeric base types.

[mihaibudiu]

Int is not the union of Bit types, it is a separate type with similar operations syntactically, but whose semantics are actually different. It is reserved for values that are computed at compile-time. Any value that exists at runtime must have a type which is not int.

[jnfoster]

What goes wrong if we added the constraint T=min_width(e) for an expression e of type int during unification? That would be enough to represent the value and communicate it to the extern.

[ChrisDodd]

The motivation for this question is dealing with things like counter/meter indexes. In p4_14, it was pretty easy -- you just declare the size of the counter/meter and the compiler figures out the bit sizes of things from there: (eliding some stuff relating to counter type)

counter ctr {  size: 8192 }
action bump(idx) { ctr.count(idx); }

In p4_16/v1model (currently) you need explicit types and casts:

counter(8192) ctr;
action bump(bit<13> idx) { ctr.count((bit<32>)idx); }

We could get rid of the need for the explicit bit<32> cast by making it a type parameter on the count method (eg, in v1model it becomes void count<I>(int I index);), but then calling with an integer constant fails with a very confusing error message:

action bump0() { ctr.count(0); }   -- error "cannot infer type for type parameter I"

Arguably we should use a type parameter on the extern, but then the user has to write:

counter<bit<13>> ctr(8192);

This at least puts the related numbers right next to each other, and forces the user to having matching types on the action parameter.

[tomrodeheffer]

From Chris's code snippet A:

extern void func<T>(in T x);
...
        func(5);

I would say that TypeInference ought to infer that T is int and then there should be a subsequent error "infinite-width type int cannot be used as a run-time type". But I see that what actually happens in the compiler is that TypeInference complains that it can't infer T.

This relates to the discussion in p4-spec issue #331 about what int really means. I would champion the approach that int ought to be an acceptable type in the grammar but semantically restricted from appearing in any position that involves a run-time value. This approach would systematize the handling of int. As we see from snippet A, a compiler code-transformation can produce a declaration of int even though the input grammar prohibits it.

There are trickier cases than snippet A. For example, snippet B from tuintt.p4.txt:

extern void func<T>(in T x);
...
        func({5});

I would say that TypeInference ought to infer that T is tuple<int> and then subsequently there should be an error "infinite-width type tuple<int> cannot be used as a run-time type". But what does the current compiler do? Well, it depends. Just running p4test you get:

p4test -v tuintt.p4
...
MidEnd_21_StrengthReduction
In file: /home/tom/p4lang/p4c/build/ir/ir-generated.cpp:1175
Compiler Bug: /home/tom/p4lang/p4c/build/ir/ir-generated.cpp:1175: Null type

But if you ask p4test to dump p4 code after every pass, you get:

p4test -v --top4 "" tuintt.p4
...
FrontEnd_8_BindTypeVariables
Writing program to ./tuintt-FrontEnd_8_BindTypeVariables.p4
In file: ../frontends/p4/toP4/toP4.cpp:258
Compiler Bug: ../frontends/p4/toP4/toP4.cpp:258: Null p4type

Either way it's a compiler bug. We see that a violation has been introduced at or before pass BindTypeVariables but this violation is normally not tripped over until pass StrengthReduction. Interestingly, BindTypeVariables immediately follows TypeInference. I suspect that TypeInference is actually the pass that introduces the violation but in a form not detected by the dumping of p4 code.

Or, to put my surmise in terms of how the current compiler thinks, in snippet B it seems that TypeInference failed to realize that it could not infer the type of T and it left a bomb behind instead.

[jnfoster]

To me, this is the right way to think about the problem, and the right way to organize the compiler:

• Type inference is totally vanilla, and does nothing special with int (so T can be assigned type int).
• Somewhere later in the type checker / compiler front-end, we enforce the condition that no run-time values have type int and signal an error if appropriate.
  This will make it clear what's going on, and simplify the passes if each one does a smaller number of things.

[mihaibudiu]

I have tagged this as enhancement, because I think that the fix is to just give a better error message.
There may be a few more issues to file based on @tomrodeheffer's comment, we'll have to analyze these one by one.

[mihaibudiu]

I hope we can close this issue. The issue about allowing 'int' as a type should be a spec issue.

[ChrisDodd]

Yes, I think the revised error message (can't infer bit width for type parameter) is much clearer and tells the user what to do (use a constant with an explicit size).