On Wed, Feb 19, 2025 at 1:20 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > 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. Discussed plenty of options offline with Kumar. The next step is to experiment returning PTR_TO_STACK with mem_size.
