From 87ff9de3484f7158ec02a1de1837eb444b8cbeaf Mon Sep 17 00:00:00 2001 From: Jesse Sigal Date: Wed, 28 Jun 2017 13:45:29 +0100 Subject: [PATCH 1/3] Fixed function inversion. Now takes into account the multi-arity of plus (was previously assumed to be binary). --- src/solvers/refinement/string_refinement.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 86b36a94790..09caf6ab121 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1076,8 +1076,10 @@ std::map string_refinementt::map_representation_of_sum( to_process.pop_back(); if(cur.id()==ID_plus) { - to_process.push_back(std::make_pair(cur.op1(), positive)); - to_process.push_back(std::make_pair(cur.op0(), positive)); + for(const exprt &op : cur.operands()) + { + to_process.push_back(std::make_pair(op, positive)); + } } else if(cur.id()==ID_minus) { From cd29f689d331f5e32bfdc810eb65972376f62780 Mon Sep 17 00:00:00 2001 From: Jesse Sigal Date: Wed, 28 Jun 2017 15:54:12 +0100 Subject: [PATCH 2/3] Extended check_axioms for not_contains and refactored Previously when checking if axioms were satisfied by the model returned after SAT, the check_axioms function would assume all not_contains axioms were violated. They are now actually checked. Factored out the solver creation and usage into `string_refinementt::is_axiom_sat`. It now sets the valuation of a chosen var to a witness for use outside of the function. Additionally, the orignal functions for adding negations to the solver now return expressions. --- src/solvers/refinement/string_refinement.cpp | 217 ++++++++++++++----- src/solvers/refinement/string_refinement.h | 9 +- 2 files changed, 172 insertions(+), 54 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 09caf6ab121..b8605ac3fb7 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -923,13 +923,73 @@ void string_refinementt::substitute_array_access(exprt &expr) const } } -/// negates the constraint and add it to the solver. the intended usage is to -/// find an assignement of the universal variable that would violate the axiom, -/// to avoid false positives the symbols other than the universal variable -/// should have been replaced by there valuation in the current model -/// \par parameters: a string constraint and a solver for non string expressions -void string_refinementt::add_negation_of_constraint_to_solver( - const string_constraintt &axiom, supert &solver) +/// Negates the constraint to be fed to a solver. The intended usage is to find +/// an assignement of the universal variable that would violate the axiom. To +/// avoid false positives, the symbols other than the universal variable should +/// have been replaced by their valuation in the current model. +/// \pre Symbols other than the universal variable should have been replaced by +/// their valuation in the current model. +/// \param axiom: the not_contains constraint to add the negation of +/// \param val: the existential witness for the axiom +/// \param univ_var: the universal variable for the negation of the axiom +/// \return: the negation of the axiom under the current evaluation +exprt string_refinementt::negation_of_not_contains_constraint( + const string_not_contains_constraintt &axiom, + const exprt &val, + const symbol_exprt &univ_var) +{ + exprt lbu=axiom.univ_lower_bound(); + exprt ubu=axiom.univ_upper_bound(); + if(lbu.id()==ID_constant && ubu.id()==ID_constant) + { + mp_integer lb_int, ub_int; + to_integer(to_constant_expr(lbu), lb_int); + to_integer(to_constant_expr(ubu), ub_int); + if(ub_int<=lb_int) + { + debug() << "empty constraint with current model" << eom; + return false_exprt(); + } + } + + exprt lbe=axiom.exists_lower_bound(); + exprt ube=axiom.exists_upper_bound(); + + if(axiom.premise()==false_exprt()) + { + debug() << "(string_refinement::check_axioms) adding false" << eom; + return false_exprt(); + } + + // Witness is the Skolem function for the existential, which we evaluate at + // univ_var. + and_exprt univ_bounds( + binary_relation_exprt(lbu, ID_le, univ_var), + binary_relation_exprt(ubu, ID_gt, univ_var)); + and_exprt exists_bounds( + binary_relation_exprt(lbe, ID_le, val), + binary_relation_exprt(ube, ID_gt, val)); + equal_exprt equal_chars( + axiom.s0()[plus_exprt(univ_var, val)], + axiom.s1()[val]); + and_exprt negaxiom(univ_bounds, axiom.premise(), exists_bounds, equal_chars); + + debug() << "(sr::check_axioms) negated not_contains axiom: " + << from_expr(ns, "", negaxiom) << eom; + substitute_array_access(negaxiom); + return negaxiom; +} + +/// Negates the constraint to be fed to a solver. The intended usage is to find +/// an assignement of the universal variable that would violate the axiom. To +/// avoid false positives, the symbols other than the universal variable should +/// have been replaced by their valuation in the current model. +/// \pre Symbols other than the universal variable should have been replaced by +/// their valuation in the current model. +/// \param axiom: the not_contains constraint to add the negation of +/// \return: the negation of the axiom under the current evaluation +exprt string_refinementt::negation_of_constraint( + const string_constraintt &axiom) { exprt lb=axiom.lower_bound(); exprt ub=axiom.upper_bound(); @@ -941,24 +1001,23 @@ void string_refinementt::add_negation_of_constraint_to_solver( if(ub_int<=lb_int) { debug() << "empty constraint with current model" << eom; - solver << false_exprt(); - return; + return false_exprt(); } } if(axiom.premise()==false_exprt()) { - debug() << "(string_refinement::check_axioms) adding false" << eom; - solver << false_exprt(); - return; + debug() << "(string_refinement::check_axioms) adding false" << eom; + return false_exprt(); } and_exprt premise(axiom.premise(), axiom.univ_within_bounds()); and_exprt negaxiom(premise, not_exprt(axiom.body())); - debug() << "(sr::check_axioms) negated axiom: " << from_expr(ns, "", negaxiom) << eom; + debug() << "(sr::check_axioms) negated axiom: " + << from_expr(ns, "", negaxiom) << eom; substitute_array_access(negaxiom); - solver << negaxiom; + return negaxiom; } /// return true if the current model satisfies all the axioms @@ -979,63 +1038,89 @@ bool string_refinementt::check_axioms() for(size_t i=0; i violated_not_contains; + debug() << "there are " << not_contains_axioms.size() << " not_contains axioms" << eom; - - for(auto nc_axiom : not_contains_axioms) + for(size_t i=0; i string_refinementt::map_representation_of_sum( to_process.pop_back(); if(cur.id()==ID_plus) { - for(const exprt &op : cur.operands()) - { + for(const auto &op : cur.operands()) to_process.push_back(std::make_pair(op, positive)); - } } else if(cur.id()==ID_minus) { @@ -1535,3 +1618,33 @@ exprt string_refinementt::get(const exprt &expr) const return substitute_array_lists(ecopy); } + +/// Creates a solver with `axiom` as the only formula added and runs it. If it +/// is SAT, then true is returned and the given evalutation of `var` is stored +/// in `witness`. If UNSAT, then what witness is is undefined. +/// \param [in] axiom: the axiom to be checked +/// \param [in] var: the variable whose evaluation will be stored in witness +/// \param [out] witness: the witness of the satisfying assignment if one +/// exists. If UNSAT, then behaviour is undefined. +/// \return: true if axiom is SAT, false if UNSAT +bool string_refinementt::is_axiom_sat( + const exprt &axiom, const symbol_exprt& var, exprt &witness) +{ + satcheck_no_simplifiert sat_check; + supert solver(ns, sat_check); + solver.set_ui(ui); + solver << axiom; + + switch(solver()) + { + case decision_proceduret::resultt::D_SATISFIABLE: + { + witness=solver.get(var); + return true; + } + case decision_proceduret::resultt::D_UNSATISFIABLE: + return false; + default: + throw "failure in checking axiom"; + } +} diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index ba189c247b7..419ad086f84 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -121,10 +121,15 @@ class string_refinementt: public bv_refinementt void set_to(const exprt &expr, bool value) override; void add_instantiations(); - void add_negation_of_constraint_to_solver( - const string_constraintt &axiom, supert &solver); + exprt negation_of_not_contains_constraint( + const string_not_contains_constraintt &axiom, + const exprt &val, + const symbol_exprt &univ_var); + exprt negation_of_constraint(const string_constraintt &axiom); void fill_model(); bool check_axioms(); + bool is_axiom_sat( + const exprt &axiom, const symbol_exprt& var, exprt &witness); void set_char_array_equality(const exprt &lhs, const exprt &rhs); void update_index_set(const exprt &formula); From 05516bbf5dfa239c06c1291f1d7c3f45585fb952 Mon Sep 17 00:00:00 2001 From: Jesse Sigal Date: Thu, 29 Jun 2017 11:22:00 +0100 Subject: [PATCH 3/3] Added regresion test for indexOf Added the originating test for the bug to smoke tests. --- .../strings-smoke-tests/java_index_of2/test.desc | 7 +++++++ .../java_index_of2/test_index_of2.class | Bin 0 -> 640 bytes .../java_index_of2/test_index_of2.java | 9 +++++++++ 3 files changed, 16 insertions(+) create mode 100644 regression/strings-smoke-tests/java_index_of2/test.desc create mode 100644 regression/strings-smoke-tests/java_index_of2/test_index_of2.class create mode 100644 regression/strings-smoke-tests/java_index_of2/test_index_of2.java diff --git a/regression/strings-smoke-tests/java_index_of2/test.desc b/regression/strings-smoke-tests/java_index_of2/test.desc new file mode 100644 index 00000000000..09a7398d4b7 --- /dev/null +++ b/regression/strings-smoke-tests/java_index_of2/test.desc @@ -0,0 +1,7 @@ +CORE +test_index_of2.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- diff --git a/regression/strings-smoke-tests/java_index_of2/test_index_of2.class b/regression/strings-smoke-tests/java_index_of2/test_index_of2.class new file mode 100644 index 0000000000000000000000000000000000000000..cb7aacc4a7a627dd3b9c169e3a2ae1e077c418a6 GIT binary patch literal 640 zcmZ`$T}vBL5IvLZ<|gZ^G4Ug9qgI<1t589F)0P%(L5Lp^5$cQF?B0Z%#@({JDgG9p zeDhfa1%>+Ve`@L6tr~prWoGW&IcLty-2J`&4PY7X9278-N5w%IFA5NNDe%gHjR}FO zgGo#YOcTmA8OJJ0bQr|zI+o3@@(Hw0$gS!?C!Yw}x%YbnYc2E@VYsdXwbeUps%X~~ z^T(mo0by*e-jToLVpj(3#YPh8puJ*ngN;ObKQ`shv|QjdA;0Q%@41~u*o!>%O&g|i zqT=L02fjKw2wO`Z44(@Zg9IU)p08SM7c-c3;b4GJ>G%8cFvHg<3M0bMQzn5oE^2s7 zDE2Yi&5rVtC#nCkxm&7XyY&5#_^@a>UDi8BSzA5;a(d=HF13RzA&0wX1HiTp8ybqXtc V0jtmWAj+`V$he=4^s%(z_&