Should run-time variables that a sophisticated compiler can prove must be equal to a compile-time known value, be treated as a compile-time known value?

[jafingerhut]

During the 2024-Jul-01 language design work group meeting, Jonathan DiLorenzo was asking some questions that I believe might be effectively the same as those described below (@jonathan-dilorenzo feel free to reply if I have misrepresented your questions).

There are P4 programs where it is possible to prove that at a particular point in the execution flow, the value of a run-time variable must be equal to a particular compile-time known value. For example:

control c1 ( /* parameters omitted */ ) {
    bit<8> i;
    bit<8> n;
    apply {
        i = 0;
        // at this point during the execution, the value of i must be 0, a compile-time known value.
        // Thus we could imagine that a sufficiently sophisticated P4 compiler could allow the following assignment,
        // which is _not_ defined by the current language spec:
        n[i:i] = 1;
        i = i + 1;
        // this is another point that we can prove that i must be equal to a compile-time known value, 1
        n[i:i] = 0;    // not supported by current spec, but we are imagining in this example that it is supported
        i = hdr.ethernet.srcAddr[47:40];
        // In this example, we are supposing that hdr.ethernet.srcAddr[47:40] is a field value from a packet
        // being processed, and thus there is no way that even an arbitrarily advanced compiler could know the value
        // of i here, and thus i cannot be treated as a compile-time known value at this point in the execution.
        if (hdr.ethernet.dstAddr == 0) {
            i = 17;
            // an advanced compiler could prove that i must equal 17 here, a compile-time known value
        } else {
            i = 18;
            // an advanced compiler could prove that i must equal 18 here, a compile-time known value
        }
        // Assuming hdr.ethernet.dstAddr is from the packet being processed, no compiler can possibly
        // prove that i is a single compile-time known value here.  It could prove that it must be 17 or 18, but
        // not a single compile-time known value, thus the following line should give a compile-time error,
        // assuming that bit slice indexes must be compile-time known values:
        n[i:i] = 1;
    }
}

I am not attempting here to enumerate all of the conditions for a run-time variable to be provably equal to a single compile-time known value at an arbitrary execution point within a P4 program, only to give some simple examples where it looks easy to do so, and some where it seems impossible to do so.

The discussion during the 2024-Jul-01 LDWG meeting seemed to be related to the questions raised in this issue. Even though it was during a discussion on loops in P4, I believe the discussion was mostly around what a sufficiently advanced compiler might be able to infer about the P4 program after loops had been unrolled.

[jnfoster]

I think compile-time-known-value-ness should be a property of P4's type system. Although it's true that we could, in principle, determine the value of many expressions at compile time, using various complex static analyses, it would be unusual to see this done in a language design. So I fear it would be confusing for programmers to go down this route.

In particular, if compile-time-known-value-ness is computed from type information alone, then it will be robust to various type-preserving refactorings the programmer might perform on their code. For example, in this program,

bit<8> i = 0;
i = i + 1;

the value of i is not compile-time known because local variables are not considered compile-time known.

However, the same might not be true under proposals hinted at here, using complex static analyses. For example, using a static analysis we can certainly determine the value of i at the end of the code block.

But now suppose we add a statement between the declaration of i and the increment:

bit<8> i = 0;
i = i | hdrs.ethernet.srcMac[0:7];
i = i + 1;

Now the value certainly cannot be determined at compile-time, as it depends on packet data. Or, as another example, suppose we invoke an extern with an out or inout parameter, so that it overwrites the value of i.

bit<8> i = 0;
some_hash(i, ...);
i = i + 1;

Even if the backend understood the semantics of the extern, the front-end would not. So again the value of i could not be determined at compile time, which is what we need to do to type check the program.

The distinction between a static analysis and a type system might be subtle. In general, type systems are compositional whereas a static analysis need not be. In this case, the only reasonable static analyses would need to be non-compositional to determine the values of expressions at compile time. This illustrates another argument for not going down this path is that the static analysis itself would take time to implement and -- assuming it were not perfectly precise -- would be confusing for programmers to understand and reason about.

To put it another way: compile-time known value != value determined at compile-time.

[vlstill]

I think compile-time-known-value-ness should be a property of P4's type system. Although it's true that we could, in principle, determine the value of many expressions at compile time, using various complex static analyses, it would be unusual to see this done in a language design. So I fear it would be confusing for programmers to go down this route.

I agree. Also, with sufficiently advanced static analysis it would quickly become quite hard to define in the specification where it should be able to derive that something is compile-time known. Especially since any such static analysis would almost surely have to be heuristic, just imagine a program like this:

bit<1> i = (bit<1>)((hdr.x.a || !hdr.x.b || hdr.x.c) && (hdr.y.a || !hdr.x.a || ...) ...)
x = hdr.v.v1[i:i];

Here, i is compile time know if and only if the expression that defines it is a tautology (i = 1) or is not satisfiable (i = 0), otherwise it depends on the packet. Sure, a sufficiently complex static analysis (capable of sat-solving) would be able to detect that, but one would not want to implement and to wait for SAT solver when compiling :-).

[ChrisDodd]

Perhaps it would be good to include a statement along the lines of

Expressions that are not compile-time-known values that are determined to be constant after some optimization passes may be accepted as compile-time-known values without a diagnostic or error.

[jafingerhut]

@ChrisDodd Interesting perspective. I did not realize this when I created this issue, but I believe that due to the pass LocalCopyPropagation, at least in some kinds of programs, an assignment to a variable with a constant value like x = 7; will cause later occurrences of x to be replaced with 7, and later passes will have no knowledge that 7 was originally a variable, and is thus treated like a compile-time known value.

So p4c today appears to already implement some situations where it can treat a run-time variable expression as a compile-time known value, when LocalCopyPropagation makes such a substitution.

[vlstill]

@ChrisDodd Interesting perspective. I did not realize this when I created this issue, but I believe that due to the pass LocalCopyPropagation, at least in some kinds of programs, an assignment to a variable with a constant value like x = 7; will cause later occurrences of x to be replaced with 7, and later passes will have no knowledge that 7 was originally a variable, and is thus treated like a compile-time known value.

So p4c today appears to already implement some situations where it can treat a run-time variable expression as a compile-time known value, when LocalCopyPropagation makes such a substitution.

Yes, another case where the compiler accepts code that is not permitted by the spec is the current behavior of modulo and division in the compiler. If you write e.g. hdr.foo.x / 2, the code compiles, because strength reduction converts it to shift. For hdr.foo.x / 3 it does not compile currently, and complains that / only works for constants, or something like that (which is why I raised #1327).

In general, I think it is a poor practice to let compiler heuristics define what code should be accepted and what not. In P4, we need to have some cases when that happens -- because of limitations of certain backends -- but I don't think we should introduce such cases into the common core of P4. Once a language depends on compiler heuristics, it is for example very hard to implement another independent compiler for the language.

[jafingerhut]

@ChrisDodd Interesting perspective. I did not realize this when I created this issue, but I believe that due to the pass LocalCopyPropagation, at least in some kinds of programs, an assignment to a variable with a constant value like x = 7; will cause later occurrences of x to be replaced with 7, and later passes will have no knowledge that 7 was originally a variable, and is thus treated like a compile-time known value.
So p4c today appears to already implement some situations where it can treat a run-time variable expression as a compile-time known value, when LocalCopyPropagation makes such a substitution.

Yes, another case where the compiler accepts code that is not permitted by the spec is the current behavior of modulo and division in the compiler. If you write e.g. hdr.foo.x / 2, the code compiles, because strength reduction converts it to shift. For hdr.foo.x / 3 it does not compile currently, and complains that / only works for constants, or something like that (which is why I raised #1327).

In general, I think it is a poor practice to let compiler heuristics define what code should be accepted and what not. In P4, we need to have some cases when that happens -- because of limitations of certain backends -- but I don't think we should introduce such cases into the common core of P4. Once a language depends on compiler heuristics, it is for example very hard to implement another independent compiler for the language.

Note: I made my observation not because I hope to codify in the spec the compiler's behavior. I don't think that is a good idea.

The reason for my observation is that if we wanted the spec to say "variables must never be treated as compile-time known values", and we wanted to be strict in p4c about this, then it appears we would need to make those checks before the LocalCopyPropagation pass, and perhaps before other passes that have a similar effect of changing variables to constants in the IR. I am not advocating this approach, either.

In short, I think Chris's suggested statement is a good one, as it reflects current practice in p4c.

[asl]

Yes, another case where the compiler accepts code that is not permitted by the spec is the current behavior of modulo and division in the compiler.

One of the reasons for this is that frontend does transformations that it should not (e.g. strength reduction and many others). And midend and other places might produce important diagnostics.

It might be profitable to learn from e.g. constexpr / consteval definitions to see how certain compile-time guarantees could be added to the language itself.

[asl]

@jafingerhut LocalCopyPropagation is a part of midend. So, it might not be run at all. I think all the spec-imposed language semantics should be enforced in frontend only. Everything else is target-specific IR transformations that might yield some target-specific language extensions.

[jafingerhut]

So the original intent of this issue was as stated in its title, because during discussions of whether loop variables should be allowed in places where compile-time known values are required (e.g. in [hi:lo] expressions of a bit slice), some people were asking: why not let some occurrences of variables be considered compile-time known?

So there are several approaches we can take to that question:

(a) Add text to the language spec requiring that implementations treat run-time variable values as compile-time known values, and perhaps even list some examples where they must be treated so, and others where they must not, and leave other cases up to the implementation.

(b) Add text to the language spec requiring that implementations ALWAYS treat run-time variables as NOT a compile-time known value, and they MUST give an error at compile time if you attempt to use a variable in a place where a compile-time known value is required.

(c) Add a statement to the spec as Chris Dodd suggested: "Expressions that are not compile-time-known values that are determined to be constant after some optimization passes may be accepted as compile-time-known values without a diagnostic or error."

(d) Change nothing in the spec, leaving this topic unmentioned.

(e) something else I have not thought of.

I do not have a sample P4 program at the moment to prove that the current version of p4c violates (b), but I believe they can be constructed.

[vlstill]

Yes, another case where the compiler accepts code that is not permitted by the spec is the current behavior of modulo and division in the compiler.

One of the reasons for this is that frontend does transformations that it should not (e.g. strength reduction and many others). And midend and other places might produce important diagnostics.

Yes, the biggest problem is probably disentangling typechecking from the premature optimizations in frontend.

It might be profitable to learn from e.g. constexpr / consteval definitions to see how certain compile-time guarantees could be added to the language itself.

I agree, although it seems to me C++ is approaching a point where all functions (except those containing IO?) can be constexpr. I can imagine that constant-evaluation of functions can be available for all functions, with a specified constructs leading to compilation error (i.e. invoking an extern that is not @pure).

[asl]

(e) something else I have not thought of.

I guess the thing is: if something is required to be a compile-time known constant, then it should be diagnosed so (long before passes like LocalConstantPropagation). If some optimizations are required for compile-time known semantics, then they should be run before the corresponding checks to be done and spec should be aligned with the implementation.