manticore符号执行某函数，符号化bytes参数后执行卡住，如何解决

Question

我现在在使用manticore动态符号执行，按顺序符号执行合约中的两个函数revoke和kill：

  function revoke(bytes32 _operation) external {
    uint ownerIndex = m_ownerIndex[uint(msg.sender)];
    // make sure they're an owner
    if (ownerIndex == 0) return;
    uint ownerIndexBit = 2**ownerIndex;
    var pending = m_pending[_operation];
    if (pending.ownersDone & ownerIndexBit > 0) {
      pending.yetNeeded++;
      pending.ownersDone -= ownerIndexBit;
      Revoke(msg.sender, _operation);
    }
  }

  function kill(address _to) onlymanyowners(sha3(msg.data)) external {
    suicide(_to);
  }

但是出现了问题，在动态符号执行时

call_fun = 'revoke'
call_fun2 = 'kill'
arg_type = arg_type_by_name[call_fun]
arg_type2 = arg_type_by_name[call_fun2]
args = m.make_symbolic_arguments(arg_type)
args2 = m.make_symbolic_arguments(arg_type2)
print("arg_data  = ",args)
tx_data = ABI.function_call(str(sig_by_name[call_fun]), *args)
tx_data2 = ABI.function_call(str(sig_by_name[call_fun2]), *args2)
symbolic_data = m.make_symbolic_buffer(320)
symbolic_value = m.make_symbolic_value()
m.transaction(caller=user_account, address=contract_account, value=symbolic_value, data=tx_data)
m.transaction(caller=user_account, address=contract_account, value=symbolic_value, data=tx_data2)

执行到该处

m.transaction(caller=user_account, address=contract_account, value=symbolic_value, data=tx_data)

就出现卡顿，我尝试使用shell输出一下args的值：

arg_data  =  ([<BitVecVariable(SVALUE) at 7f4a2217bb00>, <BitVecVariable(SVALUE_1) at 7f4a2217bac0>, <BitVecVariable(SVALUE_2) at 7f4a2217bb80>, <BitVecVariable(SVALUE_3) at 7f4a2217bc00>, <BitVecVariable(SVALUE_4) at 7f4a2217bc80>, <BitVecVariable(SVALUE_5) at 7f4a2217bd40>, <BitVecVariable(SVALUE_6) at 7f4a2217bdc0>, <BitVecVariable(SVALUE_7) at 7f4a2217be40>, <BitVecVariable(SVALUE_8) at 7f4a2217bec0>, <BitVecVariable(SVALUE_9) at 7f4a2217bd00>, <BitVecVariable(SVALUE_10) at 7f4a2217bf80>, <BitVecVariable(SVALUE_11) at 7f4a22230980>, <BitVecVariable(SVALUE_12) at 7f4a22236d80>, <BitVecVariable(SVALUE_13) at 7f4a23c3d2c0>, <BitVecVariable(SVALUE_14) at 7f4a23c2a540>, <BitVecVariable(SVALUE_15) at 7f4a20730bc0>, <BitVecVariable(SVALUE_16) at 7f4a22239240>, <BitVecVariable(SVALUE_17) at 7f4a23cc4dc0>, <BitVecVariable(SVALUE_18) at 7f4a22170e40>, <BitVecVariable(SVALUE_19) at 7f4a2218c640>, <BitVecVariable(SVALUE_20) at 7f4a2218c740>, <BitVecVariable(SVALUE_21) at 7f4a2218c980>, <BitVecVariable(SVALUE_22) at 7f4a2218cb40>, <BitVecVariable(SVALUE_23) at 7f4a2218ca80>, <BitVecVariable(SVALUE_24) at 7f4a2218ca00>, <BitVecVariable(SVALUE_25) at 7f4a2218c8c0>, <BitVecVariable(SVALUE_26) at 7f4a2218cc40>, <BitVecVariable(SVALUE_27) at 7f4a2218ca40>, <BitVecVariable(SVALUE_28) at 7f4a2218cf00>, <BitVecVariable(SVALUE_29) at 7f4a2218ce80>, <BitVecVariable(SVALUE_30) at 7f4a2218c0c0>, <BitVecVariable(SVALUE_31) at 7f4a2218c340>], <BitVecVariable(SVALUE_32) at 7f4a2357f080>)

是因为什么导致符号执行执行到该处一直进行不下去（如数组类型的参数偶尔也会卡住）？如何解决这种卡住的问题？

Answer 1

该回答引用自GPT-3.5,由博主GISer Liu编写：

首先，根据你提供的信息，卡住的原因可能是由于符号执行过程中的某些数据或者程序状态造成了死锁或者无限循环，导致无法继续执行。在你的代码中，我没有看到明显的错误，但是可能存在一些潜在的问题需要进一步排查。

解决这种问题的一般思路是：

1. 排查代码逻辑问题：仔细检查你的合约函数逻辑，确保没有可能导致死锁或者无限循环的地方。特别注意循环结构、条件分支、递归调用等。

2. 检查符号执行工具的设置：确认你使用的符号执行工具（例如Manticore）的配置是否正确，包括符号化参数的范围、符号化变量的约束条件等。可能需要调整这些设置以解决问题。

3. 增加日志输出：在关键的执行步骤前后增加日志输出，记录程序执行的状态，以便定位问题所在。

4. 简化测试用例：如果可能的话，尝试简化你的测试用例，减少符号执行的复杂度，从而更容易定位问题。

5. 查阅文档和社区：查阅Manticore的文档和相关社区，寻求类似问题的解决方案或者其他开发者的帮助。

6. 调试工具：如果符号执行工具提供了调试功能，可以尝试使用调试工具来单步执行程序，观察执行过程中的状态变化，从而更好地理解问题所在。

针对你提到的问题，你可以尝试通过以上方法逐步排查，定位并解决符号执行卡顿的问题。如果需要进一步帮助，欢迎提供更多信息或者具体的代码片段，我将尽力协助解决。

如果该回答解决了您的问题，请采纳！如果没有，请参考以下方案进行修订