Triton项目中AArch64架构LDRSW指令的符号执行问题探讨

在符号执行引擎Triton的AArch64架构实现中，发现了一个关于LDRSW（Load Register Signed Word）指令语义处理的潜在情况。这个问题会导致生成的符号表达式出现异常，进而影响后续的符号执行和约束求解过程。

问题现象

当使用Triton处理AArch64架构的LDRSW指令时，生成的符号表达式包含了一个不正常的zero_extend操作。具体表现为：

1. 执行LDRSW指令后，寄存器值的符号表达式包含了一个操作数为4294967264（即0xFFFFFFE0）的zero_extend操作
2. 当尝试简化这个表达式时，Z3求解器会抛出"invalid zero_extend application"异常

技术背景

LDRSW是AArch64架构中的一条加载指令，它将内存中的一个32位有符号整数加载到64位寄存器中，并进行符号扩展。正确的语义应该是：

1. 从内存加载32位值
2. 进行符号扩展至64位
3. 存储到目标寄存器

问题根源

通过探讨Triton源码，发现情况出在aarch64Semantics.cpp文件中LDRSW指令的语义实现部分。当前的实现错误地使用了zero_extend操作，而实际上应该使用sign_extend操作。

具体来说，代码中应该使用符号扩展（sx）将32位值扩展到64位，而不是使用零扩展（zx）。错误的实现导致了表达式生成异常，进而影响了后续的符号执行过程。

解决方案

正确的实现应该修改为使用符号扩展操作：

auto node1 = this->astCtxt->sx(dst.getBitSize() - 32, this->astCtxt->extract(31, 0, op));

这个修改确保了：

1. 从内存值中提取32位数据
2. 正确地进行符号扩展至目标寄存器大小
3. 生成符合指令语义的符号表达式

影响范围

这个问题主要影响：

1. 使用Triton进行AArch64架构符号执行的场景
2. 特别是涉及LDRSW指令的探讨
3. 后续依赖这些符号表达式的约束求解过程

总结

符号执行引擎的准确性依赖于对指令语义的精确建模。这个案例展示了即使是单个指令的语义实现错误，也可能导致整个分析流程出现问题。通过对这类情况的修复，可以提高符号执行引擎的可靠性和准确性，为二进制探讨和问题发现提供更坚实的基础。

对于使用Triton的研究人员和开发者来说，理解这类底层语义实现细节有助于更好地利用工具，并在遇到类似情况时能够快速定位和解决。