mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 07:27:57 +00:00
Code Activity

Add parameter validation for selected API functions

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-07-27 13:37:19 -07:00
parent e3139d4e03
commit 07613942da
3 changed files with 14 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/api_ast.cpp
View file

@ -225,13 +225,15 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_fresh_func_decl(c, prefix, domain_size, domain, range); LOG_Z3_mk_fresh_func_decl(c, prefix, domain_size, domain, range);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_IS_SORT(range, nullptr);
CHECK_SORTS(domain_size, domain, nullptr);
if (prefix == nullptr) { if (prefix == nullptr) {
prefix = ""; prefix = "";
} }
func_decl* d = mk_c(c)->m().mk_fresh_func_decl(prefix, func_decl* d = mk_c(c)->m().mk_fresh_func_decl(prefix,
domain_size, domain_size,
reinterpret_cast<sort*const*>(domain), to_sorts(domain),
to_sort(range), false); to_sort(range), false);
mk_c(c)->save_ast_trail(d); mk_c(c)->save_ast_trail(d);
@ -243,9 +245,11 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_fresh_const(c, prefix, ty); LOG_Z3_mk_fresh_const(c, prefix, ty);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_IS_SORT(ty, nullptr);
if (prefix == nullptr) { if (prefix == nullptr) {
prefix = ""; prefix = "";
} }
app* a = mk_c(c)->m().mk_fresh_const(prefix, to_sort(ty), false); app* a = mk_c(c)->m().mk_fresh_const(prefix, to_sort(ty), false);
mk_c(c)->save_ast_trail(a); mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a)); RETURN_Z3(of_ast(a));
@ -654,6 +658,7 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_get_sort_name(c, t); LOG_Z3_get_sort_name(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_IS_SORT(t, of_symbol(symbol::null));
CHECK_VALID_AST(t, of_symbol(symbol::null)); CHECK_VALID_AST(t, of_symbol(symbol::null));
return of_symbol(to_sort(t)->get_name()); return of_symbol(to_sort(t)->get_name());
Z3_CATCH_RETURN(of_symbol(symbol::null)); Z3_CATCH_RETURN(of_symbol(symbol::null));

11
src/api/api_context.h
View file

@ -286,10 +286,13 @@ namespace api {
inline api::context * mk_c(Z3_context c) { return reinterpret_cast<api::context*>(c); } inline api::context * mk_c(Z3_context c) { return reinterpret_cast<api::context*>(c); }
#define RESET_ERROR_CODE() { mk_c(c)->reset_error_code(); } #define RESET_ERROR_CODE() { mk_c(c)->reset_error_code(); }
#define SET_ERROR_CODE(ERR, MSG) { mk_c(c)->set_error_code(ERR, MSG); } #define SET_ERROR_CODE(ERR, MSG) { mk_c(c)->set_error_code(ERR, MSG); }
#define CHECK_NON_NULL(_p_,_ret_) { if (_p_ == 0) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is null"); return _ret_; } } #define CHECK_NON_NULL(_p_,_ret_) { if (_p_ == nullptr) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is null"); return _ret_; } }
#define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "not a valid ast"); return _ret_; } } #define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == nullptr || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "not a valid ast"); return _ret_; } }
inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); } inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); }
#define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == 0 || !is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not an expression"); return _ret_; } } #define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == nullptr || !is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not an expression"); return _ret_; } }
#define CHECK_IS_SORT(_p_, _ret_) { if (_p_ == nullptr || !is_sort(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not a sort"); return _ret_; } }
#define CHECK_SORTS(_n_, _ps_, _ret_) { for (unsigned i = 0; i < _n_; ++i) if (!is_sort(_ps_[i])) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not a sort"); return _ret_; } }
inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); } inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); }
#define CHECK_FORMULA(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return _ret_; } } #define CHECK_FORMULA(_a_, _ret_) { if (_a_ == nullptr || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return _ret_; } }
inline void check_sorts(Z3_context c, ast * n) { mk_c(c)->check_sorts(n); } inline void check_sorts(Z3_context c, ast * n) { mk_c(c)->check_sorts(n); }

1
src/api/api_util.h
View file

@ -67,6 +67,7 @@ inline ast * const * to_asts(Z3_ast const* a) { return reinterpret_cast<ast* con
inline sort * to_sort(Z3_sort a) { return reinterpret_cast<sort*>(a); } inline sort * to_sort(Z3_sort a) { return reinterpret_cast<sort*>(a); }
inline Z3_sort of_sort(sort* s) { return reinterpret_cast<Z3_sort>(s); } inline Z3_sort of_sort(sort* s) { return reinterpret_cast<Z3_sort>(s); }
inline bool is_sort(Z3_sort a) { return is_sort(to_sort(a)); }
inline sort * const * to_sorts(Z3_sort const* a) { return reinterpret_cast<sort* const*>(a); } inline sort * const * to_sorts(Z3_sort const* a) { return reinterpret_cast<sort* const*>(a); }
inline Z3_sort const * of_sorts(sort* const* s) { return reinterpret_cast<Z3_sort const*>(s); } inline Z3_sort const * of_sorts(sort* const* s) { return reinterpret_cast<Z3_sort const*>(s); }