On Wed, 2025-02-19 at 13:56 +0100, Kumar Kartikeya Dwivedi wrote: [...] > It also leads to veristat regression (+80-100% in states) in two selftests. > > We probably want to avoid doing push_stack due to the states increase, > and instead mark the stack slot instead whenever the returned > PTR_TO_MEM is used for writing, but we'll have to keep remarking > whenever writes happen, so it requires stashing some stack slot state > in the register. > The other option is invalidating the returned PTR_TO_MEM when the > buffer on the stack is written to (i.e. the stack location gets > reused). Would it be wrong, to always consider r0 to be a pointer to stack if buffer is provided? It's like modelling the PTR_TO_MEM with some additional precision. Otherwise, I think push_stack() is fine, as it keeps implementation simple.
