在Z3中模擬x86操作碼'bsf'的語義

Question

我正在使用Z3來處理一些彙編程序分析任務。我被困在模擬x86操作碼bsf的語義。

bsf operand1 operand2的語義定義爲在源操作數（操作數1）中搜索最低有效集位（1位）。

其語義可以C模擬爲：

if(operand1 == 0) { 
    ZF = 0; 
    operand2 = Undefined; 
} 
else { 
    ZF = 0; 
    Temporary = 0; 
    while(Bit(operand1, Temporary) == 0) { 
    Temporary = Temporary + 1; 
    operand2 = Temporary; 
    } 
} 

現在，假設每個操作數（例如，註冊）保持symbolic expression，我試圖模擬上述語義Z3Py。我寫的代碼是這樣的（簡化）：

def aux_bsf(x):  # x is operand1 
    if simplify(x == 0): 
     raise Exception("undefined in aux_bsf") 
    else: 
     n = x.size() 
     for i in range(n): 
      b = Extract(i, i, x) 
      if simplify(b == 1): 
      return BitVecVal(i, 32) 

    raise Exception("undefined in bsf") 

不過，我發現的simplify(x==0)評價（例如，x等於BitVecVal(13, 32) + BitVec("symbol1", 32)）總是等於True。換句話說，我總是被困在第一個例外！

我在這裏做錯了什麼..？

============================================== ====== OK，所以我想我需要的是這樣的：

def aux_bsf(x): 
    def aux(x, i): 
     if i == 31: 
      return 31 
     else: 
      return If(Extract(i, i, x) == 1, i, aux(x, i+1)) 
    return aux(x, 0) 

Answer 1

簡化（x == 0）返回表達，它不會返回真/假，其中假= 0. Python會將表達式引用視爲非零值，因此需要第一個分支。除非'x'是位向量常量，否則簡化不會返回一個確定的值。同樣的問題是簡化（b == 1）。

您可以編碼等功能操作數1和操作數2，例如，東西之間的關係沿着線：

def aux_bsf(s, x, y): 
    for k in range(x.size()): 
     s.Add(Implies(lsb(k, x), y == k) 

def lsb(k, x): 
    first0 = True 
    if k > 0: 
     first0 = Extract(x, k-1,0) == 0 
    return And(Extract(x,k,k) == 1, first0) 

也可以使用未解釋的功能，其中aux_bsf是不足規定的情形。

例如：

def aux_bsf(x): 
    bv = x.sort() 
    bsf_undef = Function('bsf-undef', bv, bv) 
    result = bsf_undef(x) 
    for k in reverse(range(bv.size())) 
     result = If(Extract(x, k, k) == 1), BitVecVal(k, bv), result) 
    return result 

def reverse(xs): 
    ....