MEMORY_ARRAY and sub-word symbolic reasoning

[0x9047]

def test_symbolic_rw_in_array_mode():
    code = {
        0x1000: bytes.fromhex("FD030091"),  # mov x29, sp
        0x1004: bytes.fromhex("FF4300D1"),  # sub sp, sp, #16
        0x1008: bytes.fromhex("400580D2"),  # mov x0, #42
        0x100C: bytes.fromhex("E00300B9"),  # str w0, [sp, #0]
        0x1010: bytes.fromhex("E10340F9"),  # ldr x1, [sp, #0]
        0x1014: bytes.fromhex("E20380B9"),  # ldrsw x2, [sp, #0]
        0x1018: bytes.fromhex("E30780B9"),  # ldrsw x3, [sp, #4]
        0x101C: bytes.fromhex("BF030091"),  # mov sp, x29
    }

    ctx = triton.TritonContext(triton.ARCH.AARCH64)
    ctx.setMode(triton.MODE.MEMORY_ARRAY, True)
    ctx.symbolizeRegister(ctx.registers.sp)
    ctx.setMode(triton.MODE.SYMBOLIZE_LOAD, True)
    ctx.setMode(triton.MODE.SYMBOLIZE_STORE, True)

    for addr, opcode in code.items():
        inst = triton.Instruction()
        inst.setAddress(addr)
        inst.setOpcode(opcode)
        ctx.processing(inst)

    x1 = ctx.getSymbolicRegister(ctx.registers.x1)

    # x1 should have multiple possible values, since only half of its bytes are fixed... right?
    assert len(ctx.getModel(x1.getAst() != x1.getAst().evaluate())) > 0

[0x9047]

Sorry... Unintentionally closed it. Re-opening it now.