z3 - Z3中引用计数的维护

Question

由于某些原因，我必须同时使用 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)。怎么解释呢？

谢谢!

Answer 1

我引用计数的黄金法则是:每当我的程序接收到指向 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 去超出范围。