z3::operator-导致程序终止

Question

这段c++代码使用了z3运算符。

std::vector<z3::expr> bv_vector_immediate = {};
int immediate_int = immediates[0]->get_immediate_value_int();
bv_vector_immediate.push_back(z3_ctx.bv_val(immediate_int, 64));
Z3_LHS = get_register_value(register1).back(); //bv_val(0, 64)
Z3_RHS = bv_vector_immediate.back();  //bv_val(10, 64)  
output =  z3::operator-(Z3_LHS,Z3_RHS);
std::cout << z3_solver.check() << "n";
z3::model m = z3_solver.get_model();
bv_vector_output.push_back(m.eval(output));
std::cout << Z3_LHS << "-" << Z3_RHS << " = " << m.eval(output).get_numeral_int64() << std::endl;

我得到的输出是:

terminate called after throwing an instance of 'z3::exception'
Aborted (core dumped)

但是，当我通过更改这一行将操作符更改为+时，代码正常工作。

output =  z3::operator+(Z3_LHS,Z3_RHS);

我相信由于-操作的结果产生负值，在最后一行std::cout << Z3_LHS << "-" << Z3_RHS << " = " << m.eval(output).get_numeral_int64() << std::endl;抛出一些z3异常。那么，我如何才能解决这个问题，即从一个较大的位向量值减去一个较小的位向量值，得到一个z3表达式的数字整数表示。我只能找到那些z3函数来获得位向量值z3表达式的int表示:get_numeral_int64, get_numeral_uint64, get_numeral_int, get_numeral_uint。

Answer 1

请始终张贴可复制的代码段。只是发布"部分"。你的代码使得其他人很难诊断问题。

话虽如此，您的问题是值0-10不适合作为位向量的int64值。这是一个最小的复制器:

#include <z3++.h>
using namespace z3;
using namespace std;
int main ()
{
context c;
expr lhs    = c.bv_val( 0, 64);
expr rhs    = c.bv_val(10, 64);
expr output = lhs - rhs;
solver s(c);
cout << s.check() << endl;
model m = s.get_model();
cout << m.eval(output).get_numeral_int64() << endl;
return 0;
};

当我运行这个，我得到:

$ g++ -std=c++11 a.cpp -l z3
$ ./a.out
sat
libc++abi: terminating with uncaught exception of type z3::exception

你可能会问为什么会这样?结果，毕竟是0-10，即-10，它可以很好地适应64位向量。但是回想一下，位向量算术没有符号的概念;它是有符号算术的运算。因此，在64位算术中，-10实际上与18446744073709551606是相同的值，这确实不适合int64的范围，其最大值是9223372036854775807。

如何解决这个问题?这取决于你如何处理这些位向量值。我假设你想把这些当作有符号整数值。然后，在上面的复制器中，将最后一行更改为:

cout << (int64_t) m.eval(output).get_numeral_uint64() << endl;

当我像这样运行时，我得到:

sat
-10

这可能是你想要的。

在z3中，位向量值没有与之相关的符号。它们只是一堆比特。但是当您对它们进行操作时，您需要小心选择正确的带符号/无符号操作。(请注意，对于一些操作，如加法/减法，它是相同的操作;但是对于其他的，比如比较和值的提取，你必须特别注意符号。)您可能需要查看http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml，对于哪些操作需要注意符号。经验法则:在模型中提取实际值将始终必须注意签名。

旁注我进一步认为这实际上是z3的c++ API的一个缺点。更高级别的API实际上可以跟踪签名并自动为您使用正确的操作，而最终用户无需跟踪签名。不幸的是，C/c++ API并不是那么高级。但那是另一个话题了。