在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): 
    ....