Add bounded for statements

[shyukahn]

This PR adds a new subsection 12.8.1. Bounded for statement under 12.8. For statement.

Bounded for statements form a subset of general for statements, and are ensured to be bounded statically by adding the following syntactic constraints:

• Only one variable is mentioned in the initialization statement, condition expression, and the update statement. We call this variable the "loop variable".
• There is only one init statement, which declares and initializes the loop variable.
• The condition expression must be a binary expression i < n where i is the loop variable and n is a local compile time known value.
• There is only one update statement, which must be an assignment statement i += 1 where i is the loop variable.
• The loop variable is a read-only variable within the loop body and the condition expression. It can only be overwritten by the update statement.

For example, this is a bounded for statement, which is a common use of for statements:

bit<8> result = 0;
for (bit<8> i = 0; i < 8; i += 1) {
    result = result + i;
}

On the other hand, these for statements are not considered as bounded for statements, though they may be actually bounded:

bit<8> result = 0;
bit<8> j;
// The init statement must declare and initialize the loop variable
for (j = 0; j < 8; j += 1) {
    result = result + j;
}
// The condition expression must be in the form i < c
for (bit<8> i = 0; i != 8; i += 1) {
    result = result + i;
}
// The update statement must increment i by 1
for (bit<8> i = 0; i < 8; i = i << 1) {
    result = result + i;
}
// i is not modifiable within the loop
for (bit<8> i = 0; i < 8; i += 1) {
    result = result + i;
    i = i + 1;
}

For now, this version states a very simple subset of bounded for statements. This PR is meant to be a starting point of the discussion on adding bounded for statements to the specification.

Additionally, one restriction is added, which also corresponds to general for statements:

• Instantiations are not allowed within for statements.

[jonathan-dilorenzo]

I'd suggest also immediately adding the other two, easily boundable (as far as I can tell) types of for loops to the (Obviously) Bounded subset:

| optAnnotations FOR "(" typeRef name IN forCollectionExpr ")" statement
| optAnnotations FOR "(" annotations typeRef name IN forCollectionExpr ")" 

where you would probably want to restrict the forCollectionExpr to be a local compile time known value. Though I suppose that could be another PR as well.

[shyukahn]

Those 2 for loops have been added to the bounded subset. This is the full syntax for bounded for statements:

forStatement
    : optAnnotations FOR "(" boundedForInitStatement ";" boundedForCondExpr ";"
      boundedForUpdateStatement ")" statement
    | optAnnotations FOR "(" typeRef name IN forCollectionExpr ")" statement
    | optAnnotations FOR "(" annotations typeRef name IN forCollectionExpr ")" statement
    ;

boundedForInitStatement
    : typeRef name "=" initializer
    ;

boundedForCondExpr
    : name '<' expression
    ;

boundedForUpdateStatement
    : name "+=" INTEGER
    ;

Regarding the restriction of forCollectionExpr to local compile time known values, I believe it’s safe to follow the general for statement semantics. Even if the collection size isn't known at compile time, the number of iterations remains fixed and bounded upon entering the loop.

[jafingerhut]

I'd suggest also immediately adding the other two, easily boundable (as far as I can tell) types of for loops to the (Obviously) Bounded subset:

| optAnnotations FOR "(" typeRef name IN forCollectionExpr ")" statement
| optAnnotations FOR "(" annotations typeRef name IN forCollectionExpr ")" 

where you would probably want to restrict the forCollectionExpr to be a local compile time known value. Though I suppose that could be another PR as well.

Currently, forCollectionExpr can only represent a list with a fixed number of elements to iterate over, where that number of elements is compile-time known, even if the values of the elements are not compile-time known.

For example, both of these possible expansions of forCollectionExpr are easily compile-time known by the compiler to have exactly 5 elements, but in the second the values of those elements are not compile-time known, and thus I suspect that the entire list is also not compile-time known, but I think it would be perfectly reasonable to consider both of these bounded loops:

// compile-time known value for `forCollectionExpr`:
for (bit<8> j in {2, 3, 5, 7, 11}) {
    // loop body here
}

// not a compile-time known value for `forCollectionExpr`, but still bounded because the number of elements is known to be 5 at compile time
for (bit<8> j in {hdr.ipv4.tos, 3, variable1, variable2+variable3, 19}) {
    // loop body here
}

[shyukahn]

I added some changes to this PR.

• A disclaimer is added to the beginning of the subsection.

  This is intended to be a minimal subset of bounded for statements. A P4 implementation that supports bounded for statements may choose to implement a larger subset; furthermore, it may reject a for statement if its bound is too large, even if it is statically bounded.

• The loop variable may be incremented by any positive integer, not only 1.

  • There is only one update statement, which must be an assignment statement i += c where i is the loop variable and c is a positive local compile-time known value.
  • Referring to n and c above, the sum n + c should not overflow with respect to the type of the loop variable.

@jafingerhut and @ChrisDodd, could you please review the changes?

[ChrisDodd]

I'm not sure if this is necessary, or is opening another can of worms -- generally, instantiations happen at compile time/config time, so are not allowed in constructs that run at runtime (apply blocks, actions, or functions). But loops are (currently) only allowed in those places (so run at runtime). We don't have a good description of this elsewhere, however.

[jaehyun1ee]

Yes, it indeed opens another can of worms. It is generally true that loops are allowed in apply blocks, actions, or functions that are (conceptually) irrelevant to instantiation.

The tricky case is directApplication within statement:

statement
    : assignmentOrMethodCallStatement
    | directApplication (* this! *)
    | conditionalStatement
    | emptyStatement
    | blockStatement
    | returnStatement
    | exitStatement
    | switchStatement
    ;

Direct application is a syntactic sugar for instantiation + apply invocation. And if we have such within a loop (which is syntactically allowed as per the grammar):

for (bit<8> i = 0; i < 8; i ++) {
   subcontrol.apply();
}

There is no way to statically give unique control-plane names to each of the instances made within the loop.

But also seems like a more general discussion should be made on a separate issue, regarding directApplication, since they may also be nested within conditionalStatements.

if (... some non-trivial condition ...) subcontrol.apply();
else subcontrol.apply();

[jafingerhut]

LGTM. Thanks for generalizing the original proposal to allow more general update statements!