mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

harden a few API methods against longjumps in set_error. Memory leak exposed in #1297

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-11 09:53:02 -07:00
parent 09ea370ea3
commit c093e6d4b9
4 changed files with 26 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/api/api_opt.cpp
View file

@ -283,15 +283,16 @@ extern "C" {
Z3_optimize opt, Z3_optimize opt,
std::istream& s) { std::istream& s) {
ast_manager& m = mk_c(c)->m(); ast_manager& m = mk_c(c)->m();
cmd_context ctx(false, &m); scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &m);
install_opt_cmds(ctx, to_optimize_ptr(opt)); install_opt_cmds(*ctx.get(), to_optimize_ptr(opt));
ctx.set_ignore_check(true); ctx->set_ignore_check(true);
if (!parse_smt2_commands(ctx, s)) { if (!parse_smt2_commands(*ctx.get(), s)) {
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR); SET_ERROR_CODE(Z3_PARSER_ERROR);
return; return;
} }
ptr_vector<expr>::const_iterator it = ctx.begin_assertions(); ptr_vector<expr>::const_iterator it = ctx->begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions(); ptr_vector<expr>::const_iterator end = ctx->end_assertions();
for (; it != end; ++it) { for (; it != end; ++it) {
to_optimize_ptr(opt)->add_hard_constraint(*it); to_optimize_ptr(opt)->add_hard_constraint(*it);
} }
@ -320,9 +321,6 @@ extern "C" {
std::ostringstream strm; std::ostringstream strm;
strm << "Could not open file " << s; strm << "Could not open file " << s;
throw default_exception(strm.str()); throw default_exception(strm.str());
SET_ERROR_CODE(Z3_PARSER_ERROR);
return;
} }
Z3_optimize_from_stream(c, d, is); Z3_optimize_from_stream(c, d, is);
Z3_CATCH; Z3_CATCH;

25
src/api/api_parsers.cpp
View file

@ -56,7 +56,7 @@ extern "C" {
Z3_func_decl const decls[]) { Z3_func_decl const decls[]) {
Z3_TRY; Z3_TRY;
LOG_Z3_parse_smtlib_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls); LOG_Z3_parse_smtlib_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
std::ostringstream* outs = alloc(std::ostringstream); scoped_ptr<std::ostringstream> outs = alloc(std::ostringstream);
bool ok = false; bool ok = false;
RESET_ERROR_CODE(); RESET_ERROR_CODE();
@ -69,7 +69,7 @@ extern "C" {
ok = false; ok = false;
} }
mk_c(c)->m_smtlib_error_buffer = outs->str(); mk_c(c)->m_smtlib_error_buffer = outs->str();
dealloc(outs); outs = nullptr;
if (!ok) { if (!ok) {
mk_c(c)->reset_parser(); mk_c(c)->reset_parser();
SET_ERROR_CODE(Z3_PARSER_ERROR); SET_ERROR_CODE(Z3_PARSER_ERROR);
@ -89,7 +89,7 @@ extern "C" {
LOG_Z3_parse_smtlib_file(c, file_name, num_sorts, sort_names, types, num_decls, decl_names, decls); LOG_Z3_parse_smtlib_file(c, file_name, num_sorts, sort_names, types, num_decls, decl_names, decls);
bool ok = false; bool ok = false;
RESET_ERROR_CODE(); RESET_ERROR_CODE();
std::ostringstream* outs = alloc(std::ostringstream); scoped_ptr<std::ostringstream> outs = alloc(std::ostringstream);
init_smtlib_parser(c, num_sorts, sort_names, types, num_decls, decl_names, decls); init_smtlib_parser(c, num_sorts, sort_names, types, num_decls, decl_names, decls);
mk_c(c)->m_smtlib_parser->set_error_stream(*outs); mk_c(c)->m_smtlib_parser->set_error_stream(*outs);
try { try {
@ -99,7 +99,7 @@ extern "C" {
ok = false; ok = false;
} }
mk_c(c)->m_smtlib_error_buffer = outs->str(); mk_c(c)->m_smtlib_error_buffer = outs->str();
dealloc(outs); outs = nullptr;
if (!ok) { if (!ok) {
mk_c(c)->reset_parser(); mk_c(c)->reset_parser();
SET_ERROR_CODE(Z3_PARSER_ERROR); SET_ERROR_CODE(Z3_PARSER_ERROR);
@ -262,21 +262,22 @@ extern "C" {
Z3_symbol const decl_names[], Z3_symbol const decl_names[],
Z3_func_decl const decls[]) { Z3_func_decl const decls[]) {
Z3_TRY; Z3_TRY;
cmd_context ctx(false, &(mk_c(c)->m())); scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
ctx.set_ignore_check(true); ctx->set_ignore_check(true);
for (unsigned i = 0; i < num_decls; ++i) { for (unsigned i = 0; i < num_decls; ++i) {
ctx.insert(to_symbol(decl_names[i]), to_func_decl(decls[i])); ctx->insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
} }
for (unsigned i = 0; i < num_sorts; ++i) { for (unsigned i = 0; i < num_sorts; ++i) {
psort* ps = ctx.pm().mk_psort_cnst(to_sort(sorts[i])); psort* ps = ctx->pm().mk_psort_cnst(to_sort(sorts[i]));
ctx.insert(ctx.pm().mk_psort_user_decl(0, to_symbol(sort_names[i]), ps)); ctx->insert(ctx->pm().mk_psort_user_decl(0, to_symbol(sort_names[i]), ps));
} }
if (!parse_smt2_commands(ctx, is)) { if (!parse_smt2_commands(*ctx.get(), is)) {
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR); SET_ERROR_CODE(Z3_PARSER_ERROR);
return of_ast(mk_c(c)->m().mk_true()); return of_ast(mk_c(c)->m().mk_true());
} }
ptr_vector<expr>::const_iterator it = ctx.begin_assertions(); ptr_vector<expr>::const_iterator it = ctx->begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions(); ptr_vector<expr>::const_iterator end = ctx->end_assertions();
unsigned size = static_cast<unsigned>(end - it); unsigned size = static_cast<unsigned>(end - it);
return of_ast(mk_c(c)->mk_and(size, it)); return of_ast(mk_c(c)->mk_and(size, it));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);

4
src/api/api_quant.cpp
View file

@ -63,9 +63,11 @@ extern "C" {
RESET_ERROR_CODE(); RESET_ERROR_CODE();
if (!mk_c(c)->m().is_bool(to_expr(body))) { if (!mk_c(c)->m().is_bool(to_expr(body))) {
SET_ERROR_CODE(Z3_SORT_ERROR); SET_ERROR_CODE(Z3_SORT_ERROR);
return nullptr;
} }
if (num_patterns > 0 && num_no_patterns > 0) { if (num_patterns > 0 && num_no_patterns > 0) {
SET_ERROR_CODE(Z3_INVALID_USAGE); SET_ERROR_CODE(Z3_INVALID_USAGE);
return nullptr;
} }
expr * const* ps = reinterpret_cast<expr * const*>(patterns); expr * const* ps = reinterpret_cast<expr * const*>(patterns);
expr * const* no_ps = reinterpret_cast<expr * const*>(no_patterns); expr * const* no_ps = reinterpret_cast<expr * const*>(no_patterns);
@ -76,7 +78,7 @@ extern "C" {
for (unsigned i = 0; i < num_patterns; i++) { for (unsigned i = 0; i < num_patterns; i++) {
if (!v(num_decls, ps[i], 0, 0)) { if (!v(num_decls, ps[i], 0, 0)) {
SET_ERROR_CODE(Z3_INVALID_PATTERN); SET_ERROR_CODE(Z3_INVALID_PATTERN);
return 0; return nullptr;
} }
} }
} }

3
src/api/api_solver.cpp
View file

@ -442,6 +442,7 @@ extern "C" {
unsigned sz = __assumptions.size(); unsigned sz = __assumptions.size();
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
if (!is_expr(__assumptions[i])) { if (!is_expr(__assumptions[i])) {
_assumptions.finalize(); _consequences.finalize(); _variables.finalize();
SET_ERROR_CODE(Z3_INVALID_USAGE); SET_ERROR_CODE(Z3_INVALID_USAGE);
return Z3_L_UNDEF; return Z3_L_UNDEF;
} }
@ -451,6 +452,7 @@ extern "C" {
sz = __variables.size(); sz = __variables.size();
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
if (!is_expr(__variables[i])) { if (!is_expr(__variables[i])) {
_assumptions.finalize(); _consequences.finalize(); _variables.finalize();
SET_ERROR_CODE(Z3_INVALID_USAGE); SET_ERROR_CODE(Z3_INVALID_USAGE);
return Z3_L_UNDEF; return Z3_L_UNDEF;
} }
@ -471,6 +473,7 @@ extern "C" {
} }
catch (z3_exception & ex) { catch (z3_exception & ex) {
to_solver_ref(s)->set_reason_unknown(eh); to_solver_ref(s)->set_reason_unknown(eh);
_assumptions.finalize(); _consequences.finalize(); _variables.finalize();
mk_c(c)->handle_exception(ex); mk_c(c)->handle_exception(ex);
return Z3_L_UNDEF; return Z3_L_UNDEF;
} }