pop semantics: bottom fields not invalidated about behavioral-model HOT 5 CLOSED

Works with the following parser:

parser start {
  extract(ext[next]);
  extract(ext[next]);
  return ingress;
}

We need to figure out if David's code is valid and should run on bmv2.
Also, what about the following:

parser start {
  extract(ext[1]);
  return ingress;
}

Is it valid or does it contradict the definition of a header stack?

from behavioral-model.

Thanks. With a refined example, I can trigger the behavior a different way: define two header stacks, ext and ext_cpy. Extract to ext. Copy all elements from ext to ext_cpy. Pop from ext_cpy. The bottom-most elements of ext_cpy will not be invalidated, but should, I believe. I've attached revised code, commands, and nano output.
copy_pop_test.txt
commands.txt
nano_out.txt

from behavioral-model.

That is exactly the same thing happening actually. You are copying headers to the stack without allocating space in the stack. If you add a call to push(ext_copy, 2) before the 2 calls to copy_header, you will be fine.
I have been investigating a little and I think that the next iteration of the P4 spec will describe the operational semantics of header stacks much more precisely than the current version. When this is released I will see if I can update bmv2.
In the mean time, I will say that as far as bmv2 is concerned, only the following operations can affect the size of a stack: extract(stack[next]), push(stack, count) and pop(stack, count). Other operations may be used to change header content but cannot be used to affect header validity in the stack. So for example, remove_header(stack[1]) is "undefined behavior" in bmv2 at that point.

from behavioral-model.

OK, makes sense; I hadn't been equating validity/non-validity with allocating space in the stack, because in my mind the space for the stack is allocated when it is declared. And the copy_header semantics per the spec say the mere act of copying one valid header stack element to another makes the destination valid: "If the source header instance was invalid, the destination header instance becomes invalid; otherwise the destination will be valid after the operation."
I will adjust in the meantime.

from behavioral-model.

Strict conformance with the P4_16 spec with regards to stack operational semantics has been enabled by default with release 1.11 (https://github.com/p4lang/behavioral-model/releases/tag/1.11.0). Pop will now shift the entire stack, instead of just the elements of the stack extracted in the parser. It is possible to revert back to the old behavior at compile time with the --disable-WP4-16-stacks configure flag.

from behavioral-model.