From 363b69f58856b95814f45065eee82f2e27e120e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 May 2022 16:44:13 -0700 Subject: [PATCH] fix #6034 --- scripts/update_api.py | 17 ++++++++++++----- src/api/api_ast_map.cpp | 1 - src/api/api_ast_vector.cpp | 1 - src/api/api_context.cpp | 3 ++- src/api/api_goal.cpp | 1 - src/api/api_model.cpp | 1 - src/api/api_opt.cpp | 1 - src/api/api_params.cpp | 5 ++--- src/api/api_solver.cpp | 7 +++---- src/api/api_tactic.cpp | 3 --- 10 files changed, 19 insertions(+), 21 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 6fb4fee53..24cf3745b 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -308,6 +308,13 @@ def display_args_to_z3(params): NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ] Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ] +Unchecked = frozenset([ 'Z3_dec_ref', 'Z3_params_dec_ref', 'Z3_model_dec_ref', + 'Z3_func_interp_dec_ref', 'Z3_func_entry_dec_ref', + 'Z3_goal_dec_ref', 'Z3_tactic_dec_ref', 'Z3_probe_dec_ref', + 'Z3_fixedpoint_dec_ref', 'Z3_param_descrs_dec_ref', + 'Z3_ast_vector_dec_ref', 'Z3_ast_map_dec_ref', + 'Z3_apply_result_dec_ref', 'Z3_solver_dec_ref', + 'Z3_stats_dec_ref', 'Z3_optimize_dec_ref']) def mk_py_wrappers(): core_py.write(""" @@ -377,7 +384,7 @@ def mk_py_wrapper_single(sig, decode_string=True): core_py.write(" %s_elems.f(" % lval) display_args_to_z3(params) core_py.write(")\n") - if len(params) > 0 and param_type(params[0]) == CONTEXT and not name in Unwrapped: + if len(params) > 0 and param_type(params[0]) == CONTEXT and not name in Unwrapped and not name in Unchecked: core_py.write(" _elems.Check(a0)\n") if result == STRING and decode_string: core_py.write(" return _to_pystr(r)\n") @@ -498,7 +505,7 @@ def mk_dotnet_wrappers(dotnet): dotnet.write(" if (r == IntPtr.Zero)\n") dotnet.write(" throw new Z3Exception(\"Object allocation failed.\");\n") else: - if len(params) > 0 and param_type(params[0]) == CONTEXT: + if len(params) > 0 and param_type(params[0]) == CONTEXT and name not in Unchecked: dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n") dotnet.write(" if (err != Z3_error_code.Z3_OK)\n") dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg(a0, (uint)err)));\n") @@ -671,7 +678,7 @@ def mk_java(java_dir, package_name): java_native.write(" if (res == 0)\n") java_native.write(" throw new Z3Exception(\"Object allocation failed.\");\n") else: - if len(params) > 0 and param_type(params[0]) == CONTEXT: + if len(params) > 0 and param_type(params[0]) == CONTEXT and name not in Unchecked: java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n') java_native.write(' if (err != Z3_error_code.Z3_OK)\n') java_native.write(' throw new Z3Exception(INTERNALgetErrorMsg(a0, err.toInt()));\n') @@ -1494,7 +1501,7 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface # determine if the function has a context as parameter. have_context = (len(params) > 0) and (param_type(params[0]) == CONTEXT) - if have_context and name not in Unwrapped: + if have_context and name not in Unwrapped and name not in Unchecked: ml_wrapper.write(' Z3_error_code ec;\n') if result != VOID: @@ -1620,7 +1627,7 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface if release_caml_gc: ml_wrapper.write('\n caml_acquire_runtime_system();\n') - if have_context and name not in Unwrapped: + if have_context and name not in Unwrapped and name not in Unchecked: ml_wrapper.write(' ec = Z3_get_error_code(ctx_p->ctx);\n') ml_wrapper.write(' if (ec != Z3_OK) {\n') ml_wrapper.write(' const char * msg = Z3_get_error_msg(ctx_p->ctx, ec);\n') diff --git a/src/api/api_ast_map.cpp b/src/api/api_ast_map.cpp index 714712faf..e252b9aca 100644 --- a/src/api/api_ast_map.cpp +++ b/src/api/api_ast_map.cpp @@ -52,7 +52,6 @@ extern "C" { void Z3_API Z3_ast_map_dec_ref(Z3_context c, Z3_ast_map m) { Z3_TRY; LOG_Z3_ast_map_dec_ref(c, m); - RESET_ERROR_CODE(); if (m) to_ast_map(m)->dec_ref(); Z3_CATCH; diff --git a/src/api/api_ast_vector.cpp b/src/api/api_ast_vector.cpp index 335fb6170..a8a64ce2c 100644 --- a/src/api/api_ast_vector.cpp +++ b/src/api/api_ast_vector.cpp @@ -47,7 +47,6 @@ extern "C" { void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v) { Z3_TRY; LOG_Z3_ast_vector_dec_ref(c, v); - RESET_ERROR_CODE(); if (v) to_ast_vector(v)->dec_ref(); Z3_CATCH; diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 3eb375f12..9f7376c68 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -374,8 +374,9 @@ extern "C" { void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a) { Z3_TRY; LOG_Z3_dec_ref(c, a); - RESET_ERROR_CODE(); if (a && to_ast(a)->get_ref_count() == 0) { + // the error is unchecked (but should not happen) in GC'ed wrappers + RESET_ERROR_CODE(); SET_ERROR_CODE(Z3_DEC_REF_ERROR, nullptr); return; } diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp index 7e2b5cd55..dd9f8959f 100644 --- a/src/api/api_goal.cpp +++ b/src/api/api_goal.cpp @@ -52,7 +52,6 @@ extern "C" { void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g) { Z3_TRY; LOG_Z3_goal_dec_ref(c, g); - RESET_ERROR_CODE(); if (g) to_goal(g)->dec_ref(); Z3_CATCH; diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index f22873f7b..3512b4b05 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -53,7 +53,6 @@ extern "C" { void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m) { Z3_TRY; LOG_Z3_model_dec_ref(c, m); - RESET_ERROR_CODE(); if (m) { to_model(m)->dec_ref(); } diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index a682a83da..140c655cd 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -67,7 +67,6 @@ extern "C" { void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize o) { Z3_TRY; LOG_Z3_optimize_dec_ref(c, o); - RESET_ERROR_CODE(); if (o) to_optimize(o)->dec_ref(); Z3_CATCH; diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp index d17018638..6e06fbf78 100644 --- a/src/api/api_params.cpp +++ b/src/api/api_params.cpp @@ -54,7 +54,6 @@ extern "C" { void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p) { Z3_TRY; LOG_Z3_params_dec_ref(c, p); - RESET_ERROR_CODE(); if (p) to_params(p)->dec_ref(); Z3_CATCH; @@ -141,8 +140,8 @@ extern "C" { void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p) { Z3_TRY; LOG_Z3_param_descrs_dec_ref(c, p); - RESET_ERROR_CODE(); - to_param_descrs(p)->dec_ref(); + if (p) + to_param_descrs(p)->dec_ref(); Z3_CATCH; } diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 05b125546..b8765a69b 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -207,7 +207,7 @@ extern "C" { if (!smt_logics::supported_logic(to_symbol(logic))) { std::ostringstream strm; strm << "logic '" << to_symbol(logic) << "' is not recognized"; - throw default_exception(strm.str()); + SET_ERROR_CODE(Z3_INVALID_ARG, strm.str()); RETURN_Z3(nullptr); } else { @@ -412,9 +412,8 @@ extern "C" { void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s) { Z3_TRY; LOG_Z3_solver_dec_ref(c, s); - RESET_ERROR_CODE(); - if (s) - to_solver(s)->dec_ref(); + if (s) + to_solver(s)->dec_ref(); Z3_CATCH; } diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index f67a373dd..edf9ab262 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -73,7 +73,6 @@ extern "C" { void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic t) { Z3_TRY; LOG_Z3_tactic_dec_ref(c, t); - RESET_ERROR_CODE(); if (t) to_tactic(t)->dec_ref(); Z3_CATCH; @@ -104,7 +103,6 @@ extern "C" { void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p) { Z3_TRY; LOG_Z3_probe_dec_ref(c, p); - RESET_ERROR_CODE(); if (p) to_probe(p)->dec_ref(); Z3_CATCH; @@ -477,7 +475,6 @@ extern "C" { void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r) { Z3_TRY; LOG_Z3_apply_result_dec_ref(c, r); - RESET_ERROR_CODE(); if (r) to_apply_result(r)->dec_ref(); Z3_CATCH;