mirror of
https://github.com/Z3Prover/z3
synced 2026-07-23 23:42:33 +00:00
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
This commit is contained in:
1sgtpepper
GitHub
parent
0105b220fd
commit
479ff3476e
2 changed files with 107 additions and 8 deletions
|
|
@ -190,16 +190,40 @@ extern "C" {
|
|||
func_decl* _d = reinterpret_cast<func_decl*>(d);
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
if (_d->is_polymorphic()) {
|
||||
polymorphism::util u(m);
|
||||
polymorphism::substitution sub(m);
|
||||
ptr_buffer<sort> 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);
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue