From b24ee6351e2314b09300327e6af7fac02cfbc110 Mon Sep 17 00:00:00 2001 From: Sehyuk Ahn Date: Mon, 19 Jan 2026 16:15:59 +0900 Subject: [PATCH 1/6] Add bounded for statements Signed-off-by: Sehyuk Ahn --- p4-16/spec/P4-16-spec.adoc | 23 +++++++++++++++++++++++ p4-16/spec/grammar.adoc | 14 ++++++++++++++ 2 files changed, 37 insertions(+) diff --git a/p4-16/spec/P4-16-spec.adoc b/p4-16/spec/P4-16-spec.adoc index a0088aef3f..f7a6aec895 100644 --- a/p4-16/spec/P4-16-spec.adoc +++ b/p4-16/spec/P4-16-spec.adoc @@ -5881,6 +5881,29 @@ 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 bounded `for` statement is a `for` statement with stronger syntactic constraints to ensure its boundedness statically. + +[source,bison] +---- +include::grammar.adoc[tag=boundedForStatement] + +include::grammar.adoc[tag=assignmentStatementWithoutSemicolon] +---- + +`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". +- 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. +- There is only one update statement, which must be an assignment statement `i = i + c`. `i` is the loop variable and `c` must be a positive local compile-time known value. +- 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 semantics of bounded `for` statements are the same as general `for` statements. + [#sec-packet-parsing] == Packet parsing diff --git a/p4-16/spec/grammar.adoc b/p4-16/spec/grammar.adoc index 26b0ec5180..8d98b85572 100644 --- a/p4-16/spec/grammar.adoc +++ b/p4-16/spec/grammar.adoc @@ -926,6 +926,20 @@ forCollectionExpr ; // end::forCollectionExpr[] +// tag::boundedForStatement[] +boundedForStatement + : optAnnotations FOR "(" variableDeclarationWithoutSemicolon ";" + expression ";" assignmentStatementWithoutSemicolon ")" statement + | optAnnotations FOR "(" typeRef name IN forCollectionExpr ")" statement + | optAnnotations FOR "(" annotations typeRef name IN forCollectionExpr ")" statement + ; +// end::boundedForStatement[] + +// tag::assignmentStatementWithoutSemicolon[] +assignmentStatementWithoutSemicolon + : lvalue "=" expression +// end::assignmentStatementWithoutSemicolon[] + /************************* TABLE *********************************/ // tag::tableDeclaration[] From b79fa559b8a2786e30c866ab152998cf736ee023 Mon Sep 17 00:00:00 2001 From: Sehyuk Ahn Date: Mon, 19 Jan 2026 17:24:59 +0900 Subject: [PATCH 2/6] Specify bounded for statements as another version of for statements Signed-off-by: Sehyuk Ahn --- p4-16/spec/P4-16-spec.adoc | 10 +++++++--- p4-16/spec/grammar.adoc | 24 +++++++++++++++++++++--- 2 files changed, 28 insertions(+), 6 deletions(-) diff --git a/p4-16/spec/P4-16-spec.adoc b/p4-16/spec/P4-16-spec.adoc index f7a6aec895..8b3429b9fe 100644 --- a/p4-16/spec/P4-16-spec.adoc +++ b/p4-16/spec/P4-16-spec.adoc @@ -5883,13 +5883,17 @@ The scope of any declaration in a `for` statement is limited to the `for` statem ==== Bounded for statement -A bounded `for` statement is a `for` statement with stronger syntactic constraints to ensure its boundedness statically. +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. [source,bison] ---- include::grammar.adoc[tag=boundedForStatement] -include::grammar.adoc[tag=assignmentStatementWithoutSemicolon] +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: @@ -5897,7 +5901,7 @@ include::grammar.adoc[tag=assignmentStatementWithoutSemicolon] - 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. -- There is only one update statement, which must be an assignment statement `i = i + c`. `i` is the loop variable and `c` must be a positive 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. The above constraints guarantee boundedness since the loop variable monotonically increases and has an upper bound. diff --git a/p4-16/spec/grammar.adoc b/p4-16/spec/grammar.adoc index 8d98b85572..423a56fe9c 100644 --- a/p4-16/spec/grammar.adoc +++ b/p4-16/spec/grammar.adoc @@ -927,14 +927,32 @@ forCollectionExpr // end::forCollectionExpr[] // tag::boundedForStatement[] -boundedForStatement - : optAnnotations FOR "(" variableDeclarationWithoutSemicolon ";" - expression ";" assignmentStatementWithoutSemicolon ")" statement +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[] + // tag::assignmentStatementWithoutSemicolon[] assignmentStatementWithoutSemicolon : lvalue "=" expression From 771578abe72991596c72c8d4fc1fc047a83cbcfa Mon Sep 17 00:00:00 2001 From: Sehyuk Ahn Date: Mon, 19 Jan 2026 17:25:52 +0900 Subject: [PATCH 3/6] Forbid instantiations within a for statement Signed-off-by: Sehyuk Ahn --- p4-16/spec/P4-16-spec.adoc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/p4-16/spec/P4-16-spec.adoc b/p4-16/spec/P4-16-spec.adoc index 8b3429b9fe..cd278d9515 100644 --- a/p4-16/spec/P4-16-spec.adoc +++ b/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. From a7b002996bfd4a949a6cc3e86e8a8273928bd4b4 Mon Sep 17 00:00:00 2001 From: Sehyuk Ahn Date: Wed, 21 Jan 2026 11:58:04 +0900 Subject: [PATCH 4/6] Require the upper bounds of 3-clause for loops to be a local compile time known value Signed-off-by: Sehyuk Ahn --- p4-16/spec/P4-16-spec.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/p4-16/spec/P4-16-spec.adoc b/p4-16/spec/P4-16-spec.adoc index cd278d9515..22aa85bfd0 100644 --- a/p4-16/spec/P4-16-spec.adoc +++ b/p4-16/spec/P4-16-spec.adoc @@ -5902,7 +5902,7 @@ include::grammar.adoc[tag=boundedForUpdateStatement] - 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. +- 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. From 1d2ee63fee41469bdca7d8bf40bf041ad2463920 Mon Sep 17 00:00:00 2001 From: Sehyuk Ahn Date: Tue, 10 Feb 2026 13:57:12 +0900 Subject: [PATCH 5/6] Remove unused assignmentStatementWithoutSemicolon Signed-off-by: Sehyuk Ahn --- p4-16/spec/grammar.adoc | 5 ----- 1 file changed, 5 deletions(-) diff --git a/p4-16/spec/grammar.adoc b/p4-16/spec/grammar.adoc index 423a56fe9c..c356a2594d 100644 --- a/p4-16/spec/grammar.adoc +++ b/p4-16/spec/grammar.adoc @@ -953,11 +953,6 @@ boundedForUpdateStatement ; // end::boundedForUpdateStatement[] -// tag::assignmentStatementWithoutSemicolon[] -assignmentStatementWithoutSemicolon - : lvalue "=" expression -// end::assignmentStatementWithoutSemicolon[] - /************************* TABLE *********************************/ // tag::tableDeclaration[] From 2d5a10454890b735e085b21939c2bfdb3ca9e7a5 Mon Sep 17 00:00:00 2001 From: Sehyuk Ahn Date: Mon, 23 Feb 2026 13:05:09 +0900 Subject: [PATCH 6/6] Allow incrementing more than 1 and add disclaimer Signed-off-by: Sehyuk Ahn --- p4-16/spec/P4-16-spec.adoc | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/p4-16/spec/P4-16-spec.adoc b/p4-16/spec/P4-16-spec.adoc index 22aa85bfd0..727c385037 100644 --- a/p4-16/spec/P4-16-spec.adoc +++ b/p4-16/spec/P4-16-spec.adoc @@ -5887,6 +5887,8 @@ The scope of any declaration in a `for` statement is limited to the `for` statem 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] @@ -5900,15 +5902,15 @@ 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". -- 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. +- 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` or `int`. +- 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 semantics of bounded `for` statements are the same as general `for` statements. +The runtime semantics of bounded `for` statements are the same as general `for` statements. [#sec-packet-parsing] == Packet parsing