Add bounded for statements

p4-16/spec/P4-16-spec.adoc

@@ -5872,6 +5872,8 @@ element in a list expression, array or header stack.  The list or range expressi
 will only be evaluated once, before the first iteration of the loop.  All side effects
 in the list or range expression will occur before the first iteration of the loop body.
 
+Instantiations are not allowed within `for` statements.
+
 A `break;` statement may be executed in a loop body to immediately exit the loop,
 without executing the rest of the body or the update statements.
 
@@ -5881,6 +5883,35 @@ either execute the loop body again, or terminate the loop.
 
 The scope of any declaration in a `for` statement is limited to the `for` statement and its body.
 
+==== Bounded for statement
+
+A P4 implementation may support a bounded version of `for` statements with stronger syntactic constraints instead of general `for` statements to ensure its boundedness statically.
+
+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.
+
+[source,bison]
+----
+include::grammar.adoc[tag=boundedForStatement]
+
+include::grammar.adoc[tag=boundedForInitStatement]
+
+include::grammar.adoc[tag=boundedForCondExpr]
+
+include::grammar.adoc[tag=boundedForUpdateStatement]
+----
+
+`for`-`in` statements remain the same as general `for`-`in` statements as a `forCollectionExpr` always contains finitely many values. However, 3-clause `for` statements are not guaranteed to be bounded in general. The following constraints are added to bounded 3-clause `for` statements:
+
+- Only one variable is mentioned in the initialization statement, condition expression, and the update statement. We call this variable the "loop variable". The type of the loop variable must be `bit<W>` or `int<W>`.
+- 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 += 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.
+- 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.
+
+The above constraints guarantee boundedness since the loop variable monotonically increases and has an upper bound.
+
+The runtime semantics of bounded `for` statements are the same as general `for` statements.
+
 [#sec-packet-parsing]
 == Packet parsing
 

p4-16/spec/grammar.adoc

@@ -926,6 +926,33 @@ forCollectionExpr
     ;
 // end::forCollectionExpr[]
 
+// tag::boundedForStatement[]
+forStatement
+    : optAnnotations FOR "(" boundedForInitStatement ";" boundedForCondExpr ";"
+      boundedForUpdateStatement ")" statement
+    | optAnnotations FOR "(" typeRef name IN forCollectionExpr ")" statement
+    | optAnnotations FOR "(" annotations typeRef name IN forCollectionExpr ")" statement
+    ;
+// end::boundedForStatement[]
+
+// tag::boundedForInitStatement[]
+boundedForInitStatement
+    : typeRef name "=" initializer
+    ;
+// end::boundedForInitStatement[]
+
+// tag::boundedForCondExpr[]
+boundedForCondExpr
+    : name '<' expression
+    ;
+// end::boundedForCondExpr[]
+
+// tag::boundedForUpdateStatement[]
+boundedForUpdateStatement
+    : name "+=" INTEGER
+    ;
+// end::boundedForUpdateStatement[]
+
 /************************* TABLE *********************************/
 
 // tag::tableDeclaration[]