mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

theory_str binary search crash avoidance when a negative length is reached

Browse source
This commit is contained in:
Murphy Berzish 2016-12-31 13:28:32 -05:00
parent 0a6c23148f
commit f3e064cb07
1 changed files with 21 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/smt/theory_str.cpp
View file

@ -8426,6 +8426,13 @@ std::string theory_str::gen_val_string(int len, int_vector & encoding) {
bool theory_str::get_next_val_encode(int_vector & base, int_vector & next) { bool theory_str::get_next_val_encode(int_vector & base, int_vector & next) {
SASSERT(charSetSize > 0); SASSERT(charSetSize > 0);
TRACE("t_str_value_test_bug", tout << "base vector: [ ";
for (unsigned i = 0; i < base.size(); ++i) {
tout << base[i] << " ";
}
tout << "]" << std::endl;
);
int s = 0; int s = 0;
int carry = 0; int carry = 0;
next.reset(); next.reset();
@ -9228,6 +9235,7 @@ expr_ref theory_str::binary_search_case_split(expr * freeVar, expr * tester, bin
expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenTester, std::string previousLenTesterValue) { expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenTester, std::string previousLenTesterValue) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
context & ctx = get_context();
if (binary_search_len_tester_stack.contains(freeVar) && !binary_search_len_tester_stack[freeVar].empty()) { if (binary_search_len_tester_stack.contains(freeVar) && !binary_search_len_tester_stack[freeVar].empty()) {
TRACE("t_str_binary_search", tout << "checking existing length testers for " << mk_pp(freeVar, m) << std::endl; TRACE("t_str_binary_search", tout << "checking existing length testers for " << mk_pp(freeVar, m) << std::endl;
@ -9337,6 +9345,19 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT
return next_case_split; return next_case_split;
} else { // lastTesterConstant is a concrete value } else { // lastTesterConstant is a concrete value
TRACE("t_str", tout << "length is fixed; generating models for free var" << std::endl;); TRACE("t_str", tout << "length is fixed; generating models for free var" << std::endl;);
// defensive check that this length did not converge on a negative value.
binary_search_info lastBounds;
if (!binary_search_len_tester_info.find(lastTester, lastBounds)) {
// unexpected
TRACE("t_str_binary_search", tout << "WARNING: no bounds information available for last tester!" << std::endl;);
// TODO resolve this
NOT_IMPLEMENTED_YET();
}
if (lastBounds.midPoint.is_neg()) {
TRACE("t_str_binary_search", tout << "WARNING: length search converged on a negative value. Negating this constraint." << std::endl;);
expr_ref axiom(m.mk_not(ctx.mk_eq_atom(mk_strlen(freeVar), m_autil.mk_numeral(lastBounds.midPoint, true))), m);
return axiom;
}
// length is fixed // length is fixed
expr * valueAssert = gen_free_var_options(freeVar, lastTester, lastTesterConstant, NULL, ""); expr * valueAssert = gen_free_var_options(freeVar, lastTester, lastTesterConstant, NULL, "");
return valueAssert; return valueAssert;