Z3 API : 고정 소수점 SMTLib 문자열을 파싱 할 때 충돌이 발생합니다.

Question

Z3의 C/C++ API를 사용하여 SMTLib2 형식의 고정 소수점 제약 조건 (특히 SeaHorn에서 생성 된 파일)을 구문 분석하려고합니다. 그러나 문자열을 구문 분석 할 때 응용 프로그램이 중단됩니다 (Z3_fixedpoint_from_string 메서드 사용). 함께 작업하는 Z3 버전은 4.5.1 64 비트 버전입니다.

소스에서 컴파일 한 Z3 바이너리로 작품을 구문 분석하려고하는 SMTLib 파일은 Z3_fixedpoint_from_string을 호출 할 때 세그먼트 화 오류로 실행됩니다. 문제가 고정 소수점 컨텍스트에 관계를 추가하는 것과 관련되어 있다고 생각하는 시점까지 문제를 좁혔습니다. 내 컴퓨터에 독방 감금 오류를 생성하는 간단한 예는 다음과 같다 : 유효하지 않은 읽기 및 쓰기의

#include "z3.h" 

int main() 
{ 
    Z3_context c = Z3_mk_context(Z3_mk_config()); 
    Z3_fixedpoint f = Z3_mk_fixedpoint(c); 

    Z3_fixedpoint_from_string (c, f, "(declare-rel R())"); 

    Z3_del_context(c); 
} 

Valgrind의이 코드를 실행 많이보고합니다. 그래서, 이것은 API가 사용되는 방식이 아니거나 어딘가에 문제가있는 것입니다. 불행히도 고정 소수점 엔진을 프로그래밍 방식으로 사용하는 방법에 대한 예제를 찾을 수 없었습니다. 그러나 예를 들어 Z3_fixedpoint_from_string (c, f, "(declare-var x Int)");을 호출하면 정상적으로 작동합니다.

BTW, 여기는 Z3_del_fixedpoint()입니까?

Answer 1

고정 소수점 개체 "f"는 참조 횟수입니다. 호출자는 참조 카운트가 작성된 직후에이를 취해야합니다. 이것을 제어하기 위해 C++ 스마트 포인터를 사용하는 것이 더 쉽습니다. 다른 개체를 제어하는 ​​것과 유사합니다. C++ API는 고정 소수점 개체에 대한 래퍼를 가지지 않으므로 다른 래퍼 스타일로 자신을 직접 만들어야합니다.

대신 del_fixedpoint는 참조 카운터를 사용합니다.

class fixedpoint : public object { 
    Z3_fixedpoint m_fp; 
public: 
    fixedpoint(context& c):object(c) { mfp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); } 
    ~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); } 
    operator Z3_fixedpoint() const { return m_fp; } 

    void from_string(char const* s) { 
     Z3_fixedpoint_from_string (ctx(), m_fp, s); 
    } 

}; 

int main() 
{ 
    context c; 
    fixedpoint f(c); 
    f.from_string("....");  
}