mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-15 17:49:59 +00:00
Code Activity

Merge pull request #8972 from Z3Prover/copilot/fix-deep-api-bugs

Browse source 
Fix input validation and null-safety bugs in Z3 C API
This commit is contained in:
Nikolaj Bjorner 2026-03-12 17:03:55 -07:00 • committed by GitHub
commit 225b3c1f30
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
8 changed files with 49 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_array.cpp
View file

@ -38,6 +38,10 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_array_sort_n(c, n, domain, range);
RESET_ERROR_CODE();
if (n == 0) {
SET_ERROR_CODE(Z3_INVALID_ARG, "array sort requires at least one domain sort");
RETURN_Z3(nullptr);
}
vector<parameter> params;
for (unsigned i = 0; i < n; ++i) params.push_back(parameter(to_sort(domain[i])));
params.push_back(parameter(to_sort(range)));

8
src/api/api_ast.cpp
View file

@ -898,6 +898,10 @@ extern "C" {
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
expr * a = to_expr(_a);
if (num_exprs > 0 && (!_from || !_to)) {
SET_ERROR_CODE(Z3_INVALID_ARG, "null from/to arrays with non-zero num_exprs");
RETURN_Z3(of_expr(nullptr));
}
expr * const * from = to_exprs(num_exprs, _from);
expr * const * to = to_exprs(num_exprs, _to);
expr * r = nullptr;
@ -1514,6 +1518,10 @@ extern "C" {
LOG_Z3_translate(c, a, target);
RESET_ERROR_CODE();
CHECK_VALID_AST(a, nullptr);
if (!target) {
SET_ERROR_CODE(Z3_INVALID_ARG, "null target context");
RETURN_Z3(nullptr);
}
if (c == target) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
RETURN_Z3(nullptr);

1
src/api/api_fpa.cpp
View file

@ -167,6 +167,7 @@ extern "C" {
RESET_ERROR_CODE();
if (ebits < 2 || sbits < 3) {
SET_ERROR_CODE(Z3_INVALID_ARG, "ebits should be at least 2, sbits at least 3");
RETURN_Z3(nullptr);
}
api::context * ctx = mk_c(c);
sort * s = ctx->fpautil().mk_float_sort(ebits, sbits);

8
src/api/api_model.cpp
View file

@ -64,6 +64,7 @@ extern "C" {
LOG_Z3_model_get_const_interp(c, m, a);
RESET_ERROR_CODE();
CHECK_NON_NULL(m, nullptr);
CHECK_NON_NULL(a, nullptr);
expr * r = to_model_ref(m)->get_const_interp(to_func_decl(a));
if (!r) {
RETURN_Z3(nullptr);
@ -212,6 +213,10 @@ extern "C" {
Z3_TRY;
LOG_Z3_model_translate(c, m, target);
RESET_ERROR_CODE();
if (!target) {
SET_ERROR_CODE(Z3_INVALID_ARG, "null target context");
RETURN_Z3(nullptr);
}
Z3_model_ref* dst = alloc(Z3_model_ref, *mk_c(target));
ast_translation tr(mk_c(c)->m(), mk_c(target)->m());
dst->m_model = to_model_ref(m)->translate(tr);
@ -246,7 +251,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_add_func_interp(c, m, f, else_val);
RESET_ERROR_CODE();
CHECK_NON_NULL(f, nullptr);
CHECK_NON_NULL(m, nullptr);
CHECK_NON_NULL(f, nullptr);
func_decl* d = to_func_decl(f);
model* mdl = to_model_ref(m);
Z3_func_interp_ref * f_ref = alloc(Z3_func_interp_ref, *mk_c(c), mdl);

6
src/api/api_opt.cpp
View file

@ -94,7 +94,11 @@ extern "C" {
Z3_TRY;
LOG_Z3_optimize_assert_soft(c, o, a, weight, id);
RESET_ERROR_CODE();
CHECK_FORMULA(a,0);
CHECK_FORMULA(a,0);
if (!weight) {
SET_ERROR_CODE(Z3_INVALID_ARG, "null weight string");
return 0;
}
rational w(weight);
return to_optimize_ptr(o)->add_soft_constraint(to_expr(a), w, to_symbol(id));
Z3_CATCH_RETURN(0);

4
src/api/api_quant.cpp
View file

@ -321,6 +321,10 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_pattern(c, num_patterns, terms);
RESET_ERROR_CODE();
if (num_patterns == 0) {
SET_ERROR_CODE(Z3_INVALID_ARG, "pattern requires at least one term");
RETURN_Z3(nullptr);
}
for (unsigned i = 0; i < num_patterns; ++i) {
if (!is_app(to_expr(terms[i]))) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);

12
src/api/api_seq.cpp
View file

@ -48,6 +48,10 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_string(c, str);
RESET_ERROR_CODE();
if (!str) {
SET_ERROR_CODE(Z3_INVALID_ARG, "null string");
RETURN_Z3(nullptr);
}
zstring s(str);
app* a = mk_c(c)->sutil().str.mk_string(s);
mk_c(c)->save_ast_trail(a);
@ -59,6 +63,10 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_lstring(c, sz, str);
RESET_ERROR_CODE();
if (sz > 0 && !str) {
SET_ERROR_CODE(Z3_INVALID_ARG, "null string buffer");
RETURN_Z3(nullptr);
}
unsigned_vector chs;
for (unsigned i = 0; i < sz; ++i) chs.push_back((unsigned char)str[i]);
zstring s(sz, chs.data());
@ -314,6 +322,10 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_re_loop(c, r, lo, hi);
RESET_ERROR_CODE();
if (hi != 0 && lo > hi) {
SET_ERROR_CODE(Z3_INVALID_ARG, "loop lower bound must not exceed upper bound");
RETURN_Z3(nullptr);
}
app* a = hi == 0 ? mk_c(c)->sutil().re.mk_loop(to_expr(r), lo) : mk_c(c)->sutil().re.mk_loop(to_expr(r), lo, hi);
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));

15
src/api/api_solver.cpp
View file

@ -379,14 +379,15 @@ extern "C" {
LOG_Z3_solver_from_file(c, s, file_name);
char const* ext = get_extension(file_name);
std::ifstream is(file_name);
init_solver(c, s);
if (!is) {
SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr);
}
else if (ext && (std::string("dimacs") == ext || std::string("cnf") == ext)) {
init_solver(c, s);
solver_from_dimacs_stream(c, s, is);
}
else {
init_solver(c, s);
solver_from_stream(c, s, is);
}
Z3_CATCH;
@ -1153,24 +1154,24 @@ extern "C" {
void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh) {
Z3_TRY;
RESET_ERROR_CODE();
user_propagator::created_eh_t c = (void(*)(void*, user_propagator::callback*, expr*))created_eh;
to_solver_ref(s)->user_propagate_register_created(c);
user_propagator::created_eh_t created_fn = (void(*)(void*, user_propagator::callback*, expr*))created_eh;
to_solver_ref(s)->user_propagate_register_created(created_fn);
Z3_CATCH;
}
void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh) {
Z3_TRY;
RESET_ERROR_CODE();
user_propagator::decide_eh_t c = (void(*)(void*, user_propagator::callback*, expr*, unsigned, bool))decide_eh;
to_solver_ref(s)->user_propagate_register_decide(c);
user_propagator::decide_eh_t decide_fn = (void(*)(void*, user_propagator::callback*, expr*, unsigned, bool))decide_eh;
to_solver_ref(s)->user_propagate_register_decide(decide_fn);
Z3_CATCH;
}
void Z3_API Z3_solver_propagate_on_binding(Z3_context c, Z3_solver s, Z3_on_binding_eh binding_eh) {
Z3_TRY;
RESET_ERROR_CODE();
user_propagator::binding_eh_t c = (bool(*)(void*, user_propagator::callback*, expr*, expr*))binding_eh;
to_solver_ref(s)->user_propagate_register_on_binding(c);
user_propagator::binding_eh_t binding_fn = (bool(*)(void*, user_propagator::callback*, expr*, expr*))binding_eh;
to_solver_ref(s)->user_propagate_register_on_binding(binding_fn);
Z3_CATCH;
}