由于某些原因,我必须同时使用 Z3 的 C++ API 和 C API。在 C++ API 中,Z3 对象的引用计数得到了很好的维护,我不必担心出错。但是,当我使用 C API 时,我必须手动维护 Z3 对象的引用计数,因为 C++ API 使用 Z3_mk_context_rc
来创建上下文。我在 Z3 中有几个关于引用计数维护的问题。
(1) 如果一个Z3_ast
的引用计数减为0,什么负责释放这个Z3_ast
的内存?什么时候?
(2) 下面的代码
void rctry(context & c)
{
expr x = c.int_const("x");
expr y = c.int_const("y");
Z3_ast res = Z3_mk_eq(c,x,y);
#ifdef FAULT_CLAUSE
expr z = c.int_const("z");
expr u = c.int_const("u");
Z3_ast fe = Z3_mk_eq(c,z,u);
#endif
std::cout << Z3_ast_to_string(c,res) << std::endl;
}
void main()
{
config cfg;
cfg.set("MODEL", true);
cfg.set("PROOF", true);
context c(cfg);
rctry(c);
}
虽然我没有为 res
引用的 AST 增加引用计数,但程序运行良好。如果定义了 FAULT_CLAUSE
,程序仍然可以运行,但它会输出 (= z u)
而不是 (= xy)
。怎么解释呢?
谢谢!
最佳答案
我引用计数的黄金法则是:每当我的程序接收到指向 Z3 对象的指针时,我立即增加引用计数并将对象保存在安全的地方(即,我现在拥有对该对象的 1 个引用)。只有当我绝对确定不再需要该对象时,我才会调用 Z3_dec_ref;从那时起,对该对象的任何访问都将触发未定义的行为(不一定是段错误),因为我不再拥有任何引用 - Z3 拥有所有引用并且它可以对它们做任何它想做的事情。
当引用计数变为零时,Z3 对象总是被释放;释放发生在对 dec_ref() 的调用中。如果 Z3_dec_ref() 从未被调用(就像在给定的示例中),那么对象可能保留在内存中,因此访问内存的特定部分可能仍然会给出“看起来不错”的结果,但内存的那部分也可能被覆盖通过其他程序使它们包含垃圾。
在给出的示例程序中,我们需要按如下方式添加 inc/dec_ref 调用:
void rctry(context & c)
{
expr x = c.int_const("x");
expr y = c.int_const("y");
Z3_ast res = Z3_mk_eq(c,x,y);
Z3_inc_ref(c, res); // I own 1 ref to res!
#ifdef FAULT_CLAUSE
expr z = c.int_const("z");
expr u = c.int_const("u");
Z3_ast fe = Z3_mk_eq(c,z,u);
Z3_inc_ref(c, fe); I own 1 ref to fe!
#endif
std::cout << Z3_ast_to_string(c, res) << std::endl;
#ifdef FAULT_CLAUSE
Z3_dec_ref(c, fe); // I give up my ref to fe.
#endif
Z3_dec_ref(c, res); // I give up my ref to res.
}
输出(= z u)
的解释是第二次调用Z3_mk_eq
重新使用以前保存 res
的内存块,因为显然
只有库本身有对它的引用,所以可以自由选择要引用的内容
做内存。结果是调用 Z3_ast_to_string
从内存的右侧部分(用于包含 res
)读取,但是
同时,那部分内存的内容发生了变化。
对于任何需要在 C 中管理引用计数的人来说,这是一个很长的解释。在 对于 C++,还有一种更方便的方法:ast/expr/etc 对象包含一个接受 C 对象的构造函数。因此,我们可以构建 通过简单地将它们包装在构造函数调用中来管理对象;在这个 可以按如下方式完成的特定示例:
void rctry(context & c)
{
expr x = c.int_const("x");
expr y = c.int_const("y");
expr res = expr(c, Z3_mk_eq(c, x, y)); // res is now a managed expr
#ifdef FAULT_CLAUSE
expr z = c.int_const("z");
expr u = c.int_const("u");
expr fe = expr(c, Z3_mk_eq(c,z,u)); // fe is now a managed expr
#endif
std::cout << Z3_ast_to_string(c, res) << std::endl;
}
在 expr
的析构函数中有一个对 Z3_dec_ref
的调用,所以它
将在函数结束时自动调用,当 res
和 fe
去
超出范围。
关于z3 - Z3中引用计数的维护,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/27200320/