Add parameter validation for selected API functions

Author: NikolajBjorner

src/api/api_ast.cpp

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

src/api/api_context.h

@@ -286,10 +286,13 @@ namespace api {
 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 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_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_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_ == 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)); }
-#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)); }
-#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); }

src/api/api_util.h

@@ -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 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 Z3_sort const * of_sorts(sort* const* s) { return reinterpret_cast<Z3_sort const*>(s); }