Memory array mode makes Triton no longer able to keep track of symbolic variables stored in memory

[zwyz]

I'm executing some code inside Triton. The initial state is:

ctx.setConcreteRegisterValue(ctx.registers.rbp, 0x9ffffff0)
ctx.setConcreteRegisterValue(ctx.registers.rsp, 0x9ffffff0)
ctx.setConcreteRegisterValue(ctx.registers.rip, 0x1400C16E0)
ctx.symbolizeRegister(ctx.registers.rcx, 'client')
ctx.symbolizeRegister(ctx.registers.rdx, 'packet')

The code I'm executing is:

0x1400c16e0: mov qword ptr [rsp + 0x20], r9
0x1400c16e5: mov dword ptr [rsp + 0x18], r8d
0x1400c16ea: push rbp
0x1400c16eb: push rbx
0x1400c16ec: push rsi
0x1400c16ed: push rdi
0x1400c16ee: push r12
0x1400c16f0: push r14
0x1400c16f2: push r15
0x1400c16f4: lea rbp, [rsp - 0x27]
0x1400c16f9: sub rsp, 0xe0
0x1400c1700: mov r15, rcx
0x1400c1703: mov r14, rdx
0x1400c1706: lea rcx, [rbp + 7]
0x1400c170a: call 0x14002b380
0x14002b380: mov qword ptr [rsp + 0x10], rdx
0x14002b385: mov qword ptr [rsp + 8], rcx
0x14002b38a: mov rax, qword ptr [rsp + 8]
0x14002b38f: mov rcx, qword ptr [rsp + 0x10]
0x14002b394: mov qword ptr [rax], rcx
0x14002b397: mov rax, qword ptr [rsp + 8]
0x14002b39c: mov qword ptr [rax + 8], 0
0x14002b3a4: mov rax, qword ptr [rsp + 8]
0x14002b3a9: ret
0x1400c170f: lea rcx, [rbp + 7]
0x1400c1713: call 0x14002b3c0
0x14002b3c0: mov qword ptr [rsp + 8], rcx
0x14002b3c5: sub rsp, 0x18
0x14002b3c9: mov rax, qword ptr [rsp + 0x20]
0x14002b3ce: mov rax, qword ptr [rax]
0x14002b3d1: mov qword ptr [rsp], rax
0x14002b3d5: mov rax, qword ptr [rsp]
0x14002b3d9: add rsp, 0x18
0x14002b3dd: ret
0x1400c1718: xor ebx, ebx
0x1400c171a: mov edi, 0xffffffff
0x1400c171f: mov dword ptr [rbp - 0x75], ebx
0x1400c1722: add qword ptr [rax + 0x18], 4
0x1400c1727: mov r9, qword ptr [rax + 0x18]

With MEMORY_ARRAY mode off, everything works fine until the second to last line, the output of ctx.liftToPython(ctx.getSymbolicRegister(ctx.registers.rax)) is just:

packet = int(input())
ref_1 = packet
ref_156 = ref_1 # MOV operation
ref_221 = ref_156 # MOV operation
ref_234 = ref_221 # MOV operation

But because MEMORY_ARRAY is off, r9 is no longer a symbolic value, the output of ctx.liftToPython(ctx.getSymbolicRegister(ctx.registers.rax)) is

ref_279 = 0x4 # MOV operation

But the problem is, if I turn on MEMORY_ARRAY mode on, the output of ctx.liftToPython(ctx.getSymbolicRegister(ctx.registers.r9)) is this very complicated expression. Triton no longer knows that rax is just packet and instead the expression involves storing the bytes of packet and loading them back later on into rax.

Is it somehow possible to have rax just be packet, and r9 be select(..., packet + 0x18)? With memory array mode off, Triton was able to keep track that rax was packet, so I'd expect that it should be able to do that with memory array mode on too, and only r9 becomes a select expression?