Value set analysis loses track of stack offset value

[ZetaTwo]

Version and Platform (required):

• Binary Ninja Version: latest dev (will update this with exact number when I get home)
• OS: Linux Ubuntu
• OS Version: 22.04 LTS
• CPU Architecture: x64

Bug Description: I have a snippet of code like this:

0x1446f95f1: mov qword [rsp], rbp
0x1446f95f5: sub rsp, 0x40

When the first instruction is executing, rbp contains a certain offset in the current frame:

(f is the function containing this)
>>> f.get_reg_value_at(0x1446f95f1, 'rbp')
<stack frame offset -0x210> # <- this value is important
>>> f.get_reg_value_at(0x1446f95f1, 'rsp')
<stack frame offset -0x250> # <- current stack offset
>>> f.get_stack_contents_at(0x1446f95f1, -0x250, 8)
<undetermined> # <- makes sense, we haven't assigned the value yet

So far, so good, however immediately after the instruction has executed, Binja does not know what is on top of the stack:

>>> f.get_stack_contents_at(0x1446f95f5, -0x250, 8)
<undetermined> # <- this should be "<stack frame offset -0x210>", not "<undetermined>"

This is an issue because later in the function the code restores the rbp and uses it as a base, something like:

mov rbp, [rsp + xxx] # pointing to the same location as above
mov rax, [rbp + 0x30] # Can not resolve where on the stack this points to
jmp rax # destination of this jump unknown even though it's a constant value in reality

Expected Behavior: I expect the value set analysis to keep track of the register value when pushed on the stack.

[plafosse]

Any chance you can share the binary or what the MLILSSA looks like?

[ZetaTwo]

MLILSSA looks like this:

I can not share the binary publicly but @fuzyll already has it and I can send it to you on Slack as well.

[fuzyll]

Apparently I forgot to put it in this issue, but the magic words for finding the binary are "playful brisk dairy sauna".