Maintaining reference counting in Z3
For some reason I have to use the C ++ API and API Z3 API together. In the C ++ API, Z3 object reference counting is well supported and I don't have to worry about making mistakes. However, I have to manually maintain reference counting for Z3 objects when I use the C API because the C ++ API is used Z3_mk_context_rc
to create context. I have a couple of problems with the reference counting service in Z3.
(1) If the reference count of a Z3_ast
is reduced to 0, what should free the memory of that Z3_ast
? And when?
(2) 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)οΌ
}
While I have not incremented the reference count for the AST that is being referenced res
, the program works well. If FAULT_CLAUSE
defined, the program is still running, but it will output (= z u)
instead (= x y)
. How can this be explained?
Thank!
source to share
My golden rule for reference counting is, whenever my program gets a pointer to a Z3 object, I immediately increment the reference count and keep the object somewhere safe (i.e. I now own 1 reference to that object). Only when I am absolutely certain that I will no longer need the object, will I call Z3_dec_ref; from now on, any access to this object will cause undefined behavior (not necessarily segfault), because I no longer own the links - Z3 owns all the remarkets and can do whatever it wants to do with them.
Z3 objects are always deallocated when the reference count goes to zero; it's in the call to dec_ref () that the deal is freed. If Z3_dec_ref () is never called (as in the example above), then the object may remain in memory, so accessing that portion of memory might still give "ok look" results, but that portion of memory might also be overwritten by others procedures to contain garbage.
In the above example program, we will 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 is Z3_mk_eq
reusing the chunk of memory that was previously held res
because apparently only the library itself had a reference to it, so it is free to choose what to do with the memory. The consequence is that the call Z3_ast_to_string
reads from the right side of memory (which contained res
), but the contents of that side of memory changed at the same time.
This was a long explanation for anyone who needs to manage ref counts in C. In the case of C ++ there is also a much more convenient way: ast / expr / etc objects contain a constructor that accepts C objects, so we can build managed objects. just by wrapping them in constructor calls; in this specific example, which can be done like this:
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;
}
There expr
is a call inside the destructor Z3_dec_ref
, so it will be called automatically at the end of the function when res
and fe
go is out of scope.
source to share