Ведение подсчета ссылок в Z3

Question

По каким-то причинам я должен использовать API C++ и API API Z3 вместе. В C++ API подсчет ссылок объектов Z3 хорошо поддерживается, и мне не нужно беспокоиться о том, чтобы делать ошибки. Однако я должен вручную поддерживать подсчет ссылок для объектов Z3, когда я использую C API, потому что 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)； 
} 

Хотя я не увеличивал количество ссылок на AST ссылается res, программа работает хорошо. Если определено значение FAULT_CLAUSE, программа все еще работает, но будет выводиться (= z u) вместо (= x y). Как это объяснить?

Спасибо!

Answer 1

Мое золотое правило для подсчета ссылок: всякий раз, когда моя программа получает указатель на объект Z3, я сразу увеличиваю счетчик ссылок и сохраняю объект где-то в безопасности (т. Е. Теперь я владею 1 ссылкой на этот объект). Только когда я абсолютно уверен, что мне больше не понадобится объект, я назову Z3_dec_ref; с этого момента любой доступ к этому объекту вызовет неопределенное поведение (не обязательно segfault), потому что я больше не владею ссылками - Z3 владеет всеми репертуарами, и он может делать все, что захочет сделать с ними.

Объекты Z3 всегда освобождаются, когда счетчик ссылок обращается в нуль; он находится в вызове dec_ref(), который происходит при освобождении. Если Z3_dec_ref() никогда не вызывается (как в приведенном примере), то объект может оставаться в памяти, поэтому доступ к этой части памяти может, возможно, по-прежнему давать результаты «ok look», но эта часть памяти также может быть перезаписана другими процедурами, чтобы они содержали мусор.

В примере программы данного, мы должны были бы добавить вкл/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++ есть и гораздо более удобным способом: аст/выражение/и т.д. объекты содержат конструктор, который принимает объекты 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 входить вне возможности.