我正在從事一個逆向工程專案，要求我對匯編代碼執行反向切片。對于給定匯編代碼函式中的給定匯編代碼暫存器，我想檢測匯編函式中執行更新該暫存器的操作的所有指令。長話短說，我將這些指令的操作表示為 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 運算式，(z3_ctx.select(mem, i))只是現在我想要一個映射而不是 z3 中的陣列
所以我的問題是如何在 z3 中構造一個映射，其鍵和值是 z3 運算式，因為我想將此映射中的加載操作表示為 z3 運算式，類似于 (z3_ctx.select(mem, i))z3 陣列的情況，只是現在 i 本身是 z3 運算式(bvadd #x0000000d r2)
uj5u.com熱心網友回復：
從位向量到位向量的 SMTLib 陣列可以很好地解決這個問題。從 API 的角度來看，在 SMT 解決方案中amap和 an之間沒有區別array：您可以使用位向量來解決它，就像您想要做的那樣。
您的訊息表明您擔心無法使用 z3 運算式“尋址”陣列？這不是真的。可以使用正確位向量型別的任意 z3 運算式尋址從位向量到位向量的陣列。
如果您嘗試了上述操作并遇到問題，請發布出現錯誤的代碼。否則，它應該可以正常作業。（話雖如此，這并不意味著它會是“高性能的”。從性能的角度來看，記憶體通常是求解器的軟肋；但那完全是另一個話題。）
轉載請註明出處，本文鏈接：https://www.uj5u.com/qianduan/313729.html
上一篇：使用x86程式集初始化串口
下一篇：從匯編代碼和骨架C派生陣列的大小