-
Notifications
You must be signed in to change notification settings - Fork 444
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Unroll finite loops in the programs with infinite ones #3689
Unroll finite loops in the programs with infinite ones #3689
Conversation
@@ -90,6 +90,7 @@ p4tools_add_xfail_reason( | |||
p4tools_add_xfail_reason( | |||
"testgen-p4c-bmv2" | |||
"differs|Expected ([0-9]+) packets on port ([0-9]+) got ([0-9]+)" | |||
parser-unroll-test9.p4 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This does not look right to me. This indicates that the implementation of unrolling is incorrect?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think that it is a bug of parser unroll. Test was failed with attached STF file.
parser-unroll-test9_8.stf.txt
It contains the stateOutOfBound
:
state stateOutOfBound {
verify(false, error.StackOutOfBounds);
transition reject;
}]
I think that this packed should be dropped, but generated STF doesn't represent that. So, I think that it's a bug of p4tools. @fruffy, What do you think?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
https://github.com/p4lang/behavioral-model/blob/d52ac6257bb3a58606383d03b31ed89671504791/docs/simple_switch.md#restrictions-on-parser-code
In BMv2, packets that enter the reject state are not dropped.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is the packet dropped or is there just a value different?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is the packet dropped or is there just a value different?
In this example, we have some bug in the loop: start
, start_loops
, finite_loop
(when the index is 0), finite_loop1
(when the index is 1), finite_loop2
(when the index is out of bound), stateOutOfBound
. This path and result after the ParserUnroll
are correct.
This problem appears when program has some memory which should be emitted after OutOfBound
.
To demonstrate that I modified parser-unroll-test2 example with one new index
variable which should be emitted. Also I increased the tests numbers to 20 and p4tool
finished with the same problem (Packet 0 on port 0 differs
in case for OutOfBound).
parser-unroll-test2-1.p4.txt
I think that the problem is in generated transition for OutOfBound
state. The state finite_loop2
should have one more assignment before call of the stateOutOfBound. I'll think how to fix it.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So the issue is that an assignment is removed?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
the issue is that an assignment is removed?
Yes, because this assignment happened before OutOfBound.
I no longer can claim to understand the parser unrolling code, so I am leaning heavily on the testing infrastructure. |
I tested these changes with this PR. I have checked manually all changed files to control the result of the ParserUnroll. All results are correct on p4c test bench. There is only one thing which we need keep in mind: infinite loops can't be unrolled by parserUnroll. If you have any suggestion how to do that, please, let me known. |
One way to treat loops that the compiler cannot unroll is to give a warning or an error and leave the parser unchanged. |
It was before this PR. Now, It prints warnings for all infinite loops and leaves them as is, and unrolls all finite loops. |
@mbudiu-vmw, Do we have something that I need to change in this PR? |
No, do you want me to merge it? |
These changes allow to unroll all finite loops in the programs even if it contain infinite once. Be fore these changes it leave a program as is for that cases.