我正在从事一个逆向工程项目，我被要求对汇编代码执行向后切片。对于给定汇编代码函数中的给定汇编代码寄存器，我想检测汇编函数中执行更新该寄存器的操作的所有指令。长话短说，我将这些指令的操作表示为z3表达式，例如
sub r2 r2 10
add r1 r2 3
寄存器r1表示为(bvadd #x0000000d r2))。但是对于像这样的LDR指令
ldr r2,[r2, #13]
add r1 r2 3
我想把内存表示成一个映射它有z3表达式作为键和值所以ldr指令应该是一个形式为(z3_ctx.select(mem, i))的z3表达式现在我想要一个映射而不是z3中的数组
所以我的问题是我如何在z3中构建一个映射，其键和值是z3表达式，因为我想将这个映射中的加载操作表示为类似于(z3_ctx.select(mem, i))的z3表达式，在z3数组的情况下，现在I本身是z3表达式(bvadd #x0000000d r2)
从位向量到位向量的SMTLib数组可以很好地工作。从API的角度来看，在smt求解中，map和array之间没有区别:您使用位向量对其进行寻址，就像您想要做的那样。
你的信息表明你担心你将无法"地址"。使用z3表达式的数组?这不是真的。一个从位向量到位向量的数组可以用正确的位向量类型的任意z3表达式寻址。
如果您尝试了上面的方法并遇到了问题，请发布导致错误的代码。否则，它应该工作得很好。(话虽如此，这并不意味着它将是"高性能的"。从性能的角度来看，记忆通常是解决者的软肋;但这是另一个话题。)