search

verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
74 stars 20 forks source link

Copy-out on exit signal #321

Open QinshiWang opened 2 years ago

QinshiWang commented 2 years ago

Out parameters are still copied out on exit signal. Is that okay?

QinshiWang commented 2 years ago

I know that when the signal is exit, the stack frame (mem) is irrelevant, but it sounds to be error-prone.

jnfoster commented 2 years ago

Yes, this is the desired behavior. I can dig up the spec issue if you're curious...

QinshiWang commented 2 years ago

Any copy-out behavior due to direction out or inout parameters of the enclosing action or control, and all of its callers, are still performed after the execution of the exit statement. See Section 6.7 for details on copy-out behavior.

So our implementation is not a bug. But I assert that for the behavior of the program, whether to copy out is irrelevant.