diff --git a/regression/strings-smoke-tests/java_if/test.class b/regression/strings-smoke-tests/java_if/test.class new file mode 100644 index 00000000000..11958bd6ce9 Binary files /dev/null and b/regression/strings-smoke-tests/java_if/test.class differ diff --git a/regression/strings-smoke-tests/java_if/test.desc b/regression/strings-smoke-tests/java_if/test.desc new file mode 100644 index 00000000000..382365ad33b --- /dev/null +++ b/regression/strings-smoke-tests/java_if/test.desc @@ -0,0 +1,9 @@ +CORE +test.class +--refine-strings --string-max-length 100 +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 12.* SUCCESS$ +^\[.*assertion.2\].* line 13.* FAILURE$ +-- +$ignoring\s*char\s*array diff --git a/regression/strings-smoke-tests/java_if/test.java b/regression/strings-smoke-tests/java_if/test.java new file mode 100644 index 00000000000..9760eb7bb2a --- /dev/null +++ b/regression/strings-smoke-tests/java_if/test.java @@ -0,0 +1,16 @@ +public class test +{ + public static String main() + { + Object t[] = new Object[5]; + t[0] = "world!"; + StringBuilder s = new StringBuilder("Hello "); + if(t[0] instanceof String) + { + s.append((String) t[0]); + } + assert(s.toString().equals("Hello world!")); + assert(!s.toString().equals("Hello world!")); + return s.toString(); + } +} diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 55c453d480d..3005a341000 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -94,6 +94,9 @@ class string_constraint_generatort static constant_exprt constant_char(int i, const typet &char_type); + // Used by string refinement + void add_axioms_for_if_array(const exprt &lhs, const if_exprt &expr); + private: // The integer with the longest string is Integer.MIN_VALUE which is -2^31, // that is -2147483648 so takes 11 characters to write. diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 8ac4f30f26c..00b494eccaf 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -272,6 +272,46 @@ string_exprt string_constraint_generatort::add_axioms_for_if( return res; } +/// Add axioms enforcing that the content of the first array is equal to +/// the true case array if the condition is true and +/// the else case array otherwise. +/// \param lhs: an expression +/// \param expr: an if expression of type array +void string_constraint_generatort::add_axioms_for_if_array( + const exprt &lhs, const if_exprt &expr) +{ + PRECONDITION(lhs.type()==expr.type()); + PRECONDITION(expr.type().id()==ID_array); + exprt t=expr.true_case(); + exprt f=expr.false_case(); + INVARIANT(t.type()==f.type(), "branches of if_exprt should have same type"); + const array_typet &type=to_array_type(t.type()); + const typet &index_type=type.size().type(); + const exprt max_length=from_integer(max_string_length, index_type); + + // We add axioms: + // a1 : forall qvar lhs[qvar] = t[qvar] + // a1 : forall qvar2 lhs[qvar] = f[qvar] + symbol_exprt qvar=fresh_univ_index("QA_array_if_true", index_type); + equal_exprt qequal(index_exprt(lhs, qvar), index_exprt(t, qvar)); + + // In case t is a constant array of fixed length is does not make sense + // to talk about indexes exceeding this length + exprt upper_bound_t= + (t.id()==ID_array)?from_integer(t.operands().size(), index_type):max_length; + string_constraintt a1(qvar, upper_bound_t, expr.cond(), qequal); + axioms.push_back(a1); + + symbol_exprt qvar2=fresh_univ_index("QA_array_if_false", index_type); + equal_exprt qequal2(index_exprt(lhs, qvar2), index_exprt(f, qvar2)); + // In case f is a constant array of fixed length is does not make sense + // to talk about indexes exceeding this length + exprt upper_bound_f= + (f.id()==ID_array)?from_integer(f.operands().size(), index_type):max_length; + string_constraintt a2(qvar2, upper_bound_f, not_exprt(expr.cond()), qequal2); + axioms.push_back(a2); +} + /// if a symbol representing a string is present in the symbol_to_string table, /// returns the corresponding string, if the symbol is not yet present, creates /// a new string with the correct type depending on whether the mode is java or diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index b8605ac3fb7..bdc33e7fe6d 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -218,16 +218,20 @@ bool string_refinementt::add_axioms_for_string_assigns( add_symbol_to_symbol_map(lhs, rhs); return false; } - else if(rhs.id() == ID_nondet_symbol) + else if(rhs.id()==ID_nondet_symbol) { add_symbol_to_symbol_map( lhs, generator.fresh_symbol("nondet_array", lhs.type())); return false; } + else if(rhs.id()==ID_if) + { + generator.add_axioms_for_if_array(lhs, to_if_expr(rhs)); + return false; + } else { - debug() << "string_refinement warning: not handling char_array: " - << from_expr(ns, "", rhs) << eom; + warning() << "ignoring char array " << from_expr(ns, "", rhs) << eom; return true; } } @@ -370,8 +374,8 @@ void string_refinementt::set_to(const exprt &expr, bool value) if(eq_expr.lhs().type()!=eq_expr.rhs().type()) { - debug() << "(sr::set_to) WARNING: ignoring " - << from_expr(ns, "", expr) << " [inconsistent types]" << eom; + warning() << "ignoring " << from_expr(ns, "", expr) + << " [inconsistent types]" << eom; debug() << "lhs has type: " << eq_expr.lhs().type().pretty(12) << eom; debug() << "rhs has type: " << eq_expr.rhs().type().pretty(12) << eom; return; @@ -392,8 +396,7 @@ void string_refinementt::set_to(const exprt &expr, bool value) // TODO: See if this happens at all. if(lhs.id()!=ID_symbol) { - debug() << "(sr::set_to) WARNING: ignoring " - << from_expr(ns, "", expr) << eom; + warning() << "ignoring " << from_expr(ns, "", expr) << eom; return; } @@ -404,9 +407,8 @@ void string_refinementt::set_to(const exprt &expr, bool value) subst_rhs.type().id() != ID_array || eq_expr.lhs().type().subtype() != subst_rhs.type().subtype()) { - debug() << "(sr::set_to) WARNING: ignoring " - << from_expr(ns, "", expr) << " [inconsistent types after substitution]" - << eom; + warning() << "ignoring " << from_expr(ns, "", expr) + << " [inconsistent types after substitution]" << eom; return; } else @@ -857,9 +859,15 @@ exprt string_refinementt::substitute_array_with_expr( } /// create an equivalent expression where array accesses and 'with' expressions -/// are replaced by 'if' expressions. e.g. for an array access arr[x], where: -/// `arr := {12, 24, 48}` the constructed expression will be: `index==0 ? 12 : -/// index==1 ? 24 : 48` +/// are replaced by 'if' expressions, in particular: +/// * for an array access `arr[x]`, where: +/// `arr := {12, 24, 48}` the constructed expression will be: +/// `index==0 ? 12 : index==1 ? 24 : 48` +/// * for an array access `arr[x]`, where: +/// `arr := array_of(12) with {0:=24} with {2:=42}` the constructed +/// expression will be: `index==0 ? 24 : index==2 ? 42 : 12` +/// * for an array access `(g1?arr1:arr2)[x]` where `arr1 := {12}` and +/// `arr2 := {34}`, the constructed expression will be: `g1 ? 12 : 34` /// \param expr: an expression containing array accesses /// \return an expression containing no array access void string_refinementt::substitute_array_access(exprt &expr) const @@ -890,6 +898,18 @@ void string_refinementt::substitute_array_access(exprt &expr) const return; } + if(index_expr.array().id()==ID_if) + { + // Substitute recursively in branches of conditional expressions + if_exprt if_expr=to_if_expr(index_expr.array()); + exprt true_case=index_exprt(if_expr.true_case(), index_expr.index()); + substitute_array_access(true_case); + exprt false_case=index_exprt(if_expr.false_case(), index_expr.index()); + substitute_array_access(false_case); + expr=if_exprt(if_expr.cond(), true_case, false_case); + return; + } + assert(index_expr.array().id()==ID_array); array_exprt &array_expr=to_array_expr(index_expr.array());