From 8fda4f904dd45a4fd0a2e784b6f1ee0e6514f246 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 30 Jun 2020 15:04:40 +0100 Subject: [PATCH] API: dont deref already free'd memory on error --- src/api/api_context.cpp | 11 ++++++++++- src/api/api_context.h | 1 + src/api/api_opt.cpp | 4 ++-- src/api/api_parsers.cpp | 8 ++++---- src/api/api_solver.cpp | 10 +++++----- src/api/api_solver.h | 2 +- src/api/api_tactic.cpp | 2 +- 7 files changed, 24 insertions(+), 14 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index e7d9b4ec2..91cfa3ab8 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -147,6 +147,14 @@ namespace api { } } + void context::set_error_code(Z3_error_code err, std::string &&opt_msg) { + m_error_code = err; + if (err != Z3_OK) { + m_exception_msg = std::move(opt_msg); + invoke_error_handler(err); + } + } + void context::check_searching() { if (m_searching) { set_error_code(Z3_INVALID_USAGE, "cannot use function while searching"); // TBD: error code could be fixed. @@ -287,7 +295,8 @@ namespace api { buffer << mk_bounded_pp(a->get_arg(i), m(), 3) << " of sort "; buffer << mk_pp(m().get_sort(a->get_arg(i)), m()) << "\n"; } - warning_msg("%s",buffer.str().c_str()); + auto str = buffer.str(); + warning_msg("%s", str.c_str()); break; } case AST_VAR: diff --git a/src/api/api_context.h b/src/api/api_context.h index da444165f..c83471594 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -170,6 +170,7 @@ namespace api { Z3_error_code get_error_code() const { return m_error_code; } void reset_error_code() { m_error_code = Z3_OK; } void set_error_code(Z3_error_code err, char const* opt_msg); + void set_error_code(Z3_error_code err, std::string &&opt_msg); void set_error_handler(Z3_error_handler h) { m_error_handler = h; } // Sign an error if solver is searching void check_searching(); diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index e509bc528..2076ee5f6 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -358,14 +358,14 @@ extern "C" { try { if (!parse_smt2_commands(*ctx.get(), s)) { ctx = nullptr; - SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str()); + SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); return; } } catch (z3_exception& e) { errstrm << e.msg(); ctx = nullptr; - SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str()); + SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); return; } diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index c0da66164..b49d6b99c 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -90,14 +90,14 @@ extern "C" { try { if (!parse_smt2_commands(*ctx.get(), is)) { ctx = nullptr; - SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str()); + SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); return of_ast_vector(v); } } catch (z3_exception& e) { errstrm << e.msg(); ctx = nullptr; - SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str()); + SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); return of_ast_vector(v); } for (expr* e : ctx->tracked_assertions()) { @@ -157,13 +157,13 @@ extern "C" { ctx->set_diagnostic_stream(ous); try { if (!parse_smt2_commands(*ctx.get(), is)) { - SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str().c_str()); + SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str()); RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); } } catch (z3_exception& e) { if (ous.str().empty()) ous << e.msg(); - SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str().c_str()); + SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str()); RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); } RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 596ba011d..f4fc71843 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -105,10 +105,10 @@ extern "C" { m_out.flush(); } - solver2smt2_pp::solver2smt2_pp(ast_manager& m, char const* file): + solver2smt2_pp::solver2smt2_pp(ast_manager& m, const std::string& file): m_pp_util(m), m_out(file), m_tracked(m) { if (!m_out) { - throw default_exception("could not open " + std::string(file) + " for output"); + throw default_exception("could not open " + file + " for output"); } } @@ -155,7 +155,7 @@ extern "C" { solver_params sp(to_solver(s)->m_params); symbol smt2log = sp.smtlib2_log(); if (smt2log.is_non_empty_string() && !to_solver(s)->m_pp) { - to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str().c_str()); + to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str()); } } @@ -247,7 +247,7 @@ extern "C" { if (!parse_smt2_commands(*ctx.get(), is)) { ctx = nullptr; - SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str()); + SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); return; } @@ -266,7 +266,7 @@ extern "C" { std::stringstream err; sat::solver solver(to_solver_ref(s)->get_params(), m.limit()); if (!parse_dimacs(is, err, solver)) { - SET_ERROR_CODE(Z3_PARSER_ERROR, err.str().c_str()); + SET_ERROR_CODE(Z3_PARSER_ERROR, err.str()); return; } sat2goal s2g; diff --git a/src/api/api_solver.h b/src/api/api_solver.h index c22189857..25b9c67d7 100644 --- a/src/api/api_solver.h +++ b/src/api/api_solver.h @@ -28,7 +28,7 @@ struct solver2smt2_pp { expr_ref_vector m_tracked; unsigned_vector m_tracked_lim; - solver2smt2_pp(ast_manager& m, char const* file); + solver2smt2_pp(ast_manager& m, const std::string& file); void assert_expr(expr* e); void assert_expr(expr* e, expr* t); void push(); diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 491fb8354..865fbf6d4 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -54,7 +54,7 @@ extern "C" { if (t == nullptr) { std::stringstream err; err << "unknown tactic " << name; - SET_ERROR_CODE(Z3_INVALID_ARG, err.str().c_str()); + SET_ERROR_CODE(Z3_INVALID_ARG, err.str()); RETURN_Z3(nullptr); } tactic * new_t = t->mk(mk_c(c)->m());