From 479ff3476e6cb28a157d9a92faf68e69f8ea224a Mon Sep 17 00:00:00 2001 From: 1sgtpepper Date: Wed, 22 Jul 2026 10:11:38 +0800 Subject: [PATCH] Fix polymorphic application arity validation (#10179) ## Summary Validate a polymorphic declaration's arity before matching argument sorts. This prevents `Z3_mk_app` from reading past the declaration domain and makes both too-few and too-many arguments return `Z3_INVALID_ARG`. Adds C API regression coverage for valid, too-few, and too-many applications. Fixes #10177. ## Testing - `./build-release/test-z3 api` - `./build-release/test-z3 /a` (92 passed) - Standalone #10177 reproducer against the patched shared library --- src/api/api_ast.cpp | 40 +++++++++++++++++++----- src/test/api.cpp | 75 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 107 insertions(+), 8 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index f33f93e29f..e98104e1b4 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -190,16 +190,40 @@ extern "C" { func_decl* _d = reinterpret_cast(d); ast_manager& m = mk_c(c)->m(); if (_d->is_polymorphic()) { - polymorphism::util u(m); - polymorphism::substitution sub(m); - ptr_buffer domain; - for (unsigned i = 0; i < num_args; ++i) { - if (!sub.match(_d->get_domain(i), arg_list[i]->get_sort())) - SET_ERROR_CODE(Z3_INVALID_ARG, "failed to match argument of polymorphic function"); - domain.push_back(arg_list[i]->get_sort()); + if (_d->get_arity() != num_args && + !_d->is_left_associative() && !_d->is_right_associative() && !_d->is_chainable()) { + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid function application, wrong number of arguments"); + return nullptr; } + polymorphism::substitution sub(m); + auto match = [&](unsigned domain_idx, unsigned arg_idx) { + if (!sub.match(_d->get_domain(domain_idx), arg_list[arg_idx]->get_sort())) { + SET_ERROR_CODE(Z3_INVALID_ARG, "failed to match argument of polymorphic function"); + return false; + } + return true; + }; + for (unsigned i = 0; i < num_args; ++i) { + unsigned domain_idx = i; + if (_d->is_associative()) + domain_idx = 0; + else if (_d->is_right_associative()) + domain_idx = i + 1 == num_args && num_args > 1 ? 1 : 0; + else if (_d->is_left_associative()) + domain_idx = i == 0 ? 0 : 1; + else if (_d->is_chainable()) { + if ((i > 0 && !match(1, i)) || (i + 1 < num_args && !match(0, i))) + return nullptr; + continue; + } + if (!match(domain_idx, i)) + return nullptr; + } + sort_ref_buffer domain(m); + for (unsigned i = 0; i < _d->get_arity(); ++i) + domain.push_back(sub(_d->get_domain(i))); sort_ref range = sub(_d->get_range()); - _d = m.instantiate_polymorphic(_d, num_args, domain.data(), range); + _d = m.instantiate_polymorphic(_d, _d->get_arity(), domain.data(), range); } app* a = m.mk_app(_d, num_args, arg_list.data()); mk_c(c)->save_ast_trail(a); diff --git a/src/test/api.cpp b/src/test/api.cpp index b1765fdd4a..33dac3af0c 100644 --- a/src/test/api.cpp +++ b/src/test/api.cpp @@ -40,6 +40,80 @@ void test_apps() { Z3_del_context(ctx); } +static void test_mk_app_polymorphic_arity() { + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code) {}); + + Z3_sort type_var = Z3_mk_type_variable(ctx, Z3_mk_string_symbol(ctx, "A")); + Z3_func_decl f = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx, "f"), 1, &type_var, type_var); + Z3_sort int_sort = Z3_mk_int_sort(ctx); + Z3_ast args[] = { + Z3_mk_int(ctx, 1, int_sort), Z3_mk_int(ctx, 2, int_sort), Z3_mk_int(ctx, 3, int_sort) + }; + + ENSURE(Z3_mk_app(ctx, f, 1, args)); + ENSURE(Z3_get_error_code(ctx) == Z3_OK); + ENSURE(!Z3_mk_app(ctx, f, 0, nullptr)); + ENSURE(Z3_get_error_code(ctx) == Z3_INVALID_ARG); + ENSURE(!Z3_mk_app(ctx, f, 2, args)); + ENSURE(Z3_get_error_code(ctx) == Z3_INVALID_ARG); + + Z3_sort set_type_var = Z3_mk_set_sort(ctx, type_var); + Z3_ast poly_set = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "poly_set"), set_type_var); + Z3_ast poly_sets[] = { poly_set, poly_set }; + Z3_ast set_union = Z3_mk_set_union(ctx, 2, poly_sets); + Z3_func_decl set_union_decl = Z3_get_app_decl(ctx, Z3_to_app(ctx, set_union)); + ENSURE(Z3_get_arity(ctx, set_union_decl) == 2); + + Z3_sort int_set_sort = Z3_mk_set_sort(ctx, int_sort); + Z3_ast int_sets[] = { + Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "int_set1"), int_set_sort), + Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "int_set2"), int_set_sort), + Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "int_set3"), int_set_sort) + }; + ENSURE(Z3_mk_app(ctx, set_union_decl, 1, int_sets)); + ENSURE(Z3_get_error_code(ctx) == Z3_OK); + Z3_ast set_union3 = Z3_mk_app(ctx, set_union_decl, 3, int_sets); + ENSURE(set_union3); + ENSURE(Z3_get_error_code(ctx) == Z3_OK); + Z3_app set_union3_app = Z3_to_app(ctx, set_union3); + Z3_func_decl set_union3_decl = Z3_get_app_decl(ctx, set_union3_app); + ENSURE(Z3_get_arity(ctx, set_union3_decl) == 2); + ENSURE(Z3_get_app_num_args(ctx, set_union3_app) == 2); + ENSURE(Z3_get_app_arg(ctx, set_union3_app, 0) == int_sets[0]); + Z3_app set_union3_tail = Z3_to_app(ctx, Z3_get_app_arg(ctx, set_union3_app, 1)); + ENSURE(Z3_get_app_num_args(ctx, set_union3_tail) == 2); + ENSURE(Z3_get_app_arg(ctx, set_union3_tail, 0) == int_sets[1]); + ENSURE(Z3_get_app_arg(ctx, set_union3_tail, 1) == int_sets[2]); + + Z3_sort bool_set_sort = Z3_mk_set_sort(ctx, Z3_mk_bool_sort(ctx)); + Z3_ast bool_set = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "bool_set"), bool_set_sort); + Z3_ast incompatible_sets[] = { int_sets[0], int_sets[1], bool_set }; + ENSURE(!Z3_mk_app(ctx, set_union_decl, 3, incompatible_sets)); + ENSURE(Z3_get_error_code(ctx) == Z3_INVALID_ARG); + + Z3_ast poly_value = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "poly_value"), type_var); + Z3_ast poly_eq = Z3_mk_eq(ctx, poly_value, poly_value); + Z3_func_decl eq_decl = Z3_get_app_decl(ctx, Z3_to_app(ctx, poly_eq)); + ENSURE(Z3_mk_app(ctx, eq_decl, 3, args)); + ENSURE(Z3_get_error_code(ctx) == Z3_OK); + + Z3_sort re_type_var = Z3_mk_re_sort(ctx, Z3_mk_seq_sort(ctx, type_var)); + Z3_ast empty_re_type_var = Z3_mk_re_empty(ctx, re_type_var); + Z3_ast poly_res[] = { empty_re_type_var, empty_re_type_var }; + Z3_ast re_union = Z3_mk_re_union(ctx, 2, poly_res); + Z3_func_decl re_union_decl = Z3_get_app_decl(ctx, Z3_to_app(ctx, re_union)); + Z3_sort re_int = Z3_mk_re_sort(ctx, Z3_mk_seq_sort(ctx, int_sort)); + Z3_ast empty_re_int = Z3_mk_re_empty(ctx, re_int); + Z3_ast int_res[] = { empty_re_int, empty_re_int, empty_re_int }; + ENSURE(Z3_mk_app(ctx, re_union_decl, 3, int_res)); + ENSURE(Z3_get_error_code(ctx) == Z3_OK); + + Z3_del_context(ctx); +} + void test_bvneg() { Z3_config cfg = Z3_mk_config(); Z3_set_param_value(cfg,"MODEL","true"); @@ -305,6 +379,7 @@ void test_max_reg() { void tst_api() { test_apps(); + test_mk_app_polymorphic_arity(); test_bvneg(); test_mk_distinct(); test_optimize_translate();