CODEWITHSUNDEEP
z3
cxcfan
cxcfan

Reputation: 185

Maintenance of reference counting in Z3

By some reasons I have to use C++ API and C API of Z3 together. In C++ API, reference counting of Z3 objects are well maintained and I needn't to worry about making mistakes. However I have to manually maintain reference counting for Z3 objects when I use C API because C++ API uses Z3_mk_context_rc to create the context. I have several problems on reference counting maintenance in Z3.

(1) If the reference counting of a Z3_ast is reduced to 0, what is responsible to release the memory of this Z3_ast? And when?

(2) The code below

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)；
}

Although I didn't increase reference count for AST referenced by res, the program works well. If FAULT_CLAUSE is defined, program still works, but it will output (= z u) instead of (= x y). How to explain this?

Thank you!

Upvotes: 3

Views: 425

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8392

My golden rule for reference counting is: Whenever my program receives a pointer to a Z3 object, I immediately increment the ref count and I save the object somewhere safe (i.e., I now own 1 reference to that object). Only when I'm absolutely sure that I will not need the object any longer, then I will call Z3_dec_ref; from that point on, any access to that object will trigger undefined behavior (not necessarily a segfault), because I don't own any references anymore - Z3 owns all the rerferences and it can do whatever it wants to do with them.

Z3 objects are always deallocated when the ref count goes to zero; it's within the call to dec_ref() that the deallocation happens. If Z3_dec_ref() is never called (like in the example given), then the object may remain in memory so accessing that particular part of the memory might perhaps still give "ok looking" results, but that part of the memory may also be overwritten by other procedures so that they contain garbage.

In the example program given, we would need to add inc/dec_ref calls as follows:

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.
}

The explanation for the output (= z u) is that the second call to Z3_mk_eq re-uses the chunk of memory that previously held res, because apparently only the library itself had a reference to it, so it is free to chose what to do with the memory. The consequence is that the call to Z3_ast_to_string reads from the right part of the memory (that used to contain res), but the contents of that part of the memory have changed in the meanwhile.

That was the long explanation for anybody who needs to manage ref counts in C. In the case of C++ there is also a much more convenient way: the ast/expr/etc objects contain a constructor that takes C objects. Therefore, we can construct managed objects by simply wrapping them in constructor calls; in this particular example that could be done as follows:

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;        
}

Within the destructor of expr there is a call to Z3_dec_ref, so that it will be called automatically at the end of the function, when res and fe go out of scope.

Upvotes: 3

Related Questions