From f06649bb633d21229a8fd687023a93b7701ef487 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 7 Jul 2017 11:27:19 +0100 Subject: [PATCH 1/6] Adding axioms for arrays of characters in the form of an if expression --- .../refinement/string_constraint_generator.h | 3 ++ .../string_constraint_generator_main.cpp | 31 +++++++++++++++++++ 2 files changed, 34 insertions(+) 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..60bdc637b42 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -272,6 +272,37 @@ 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)); + string_constraintt a1(qvar, max_length, 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)); + string_constraintt a2(qvar2, max_length, 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 From 30306f1fed9a466f20f9a8285add7f7bb4d623bd Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Sun, 9 Jul 2017 10:51:43 +0100 Subject: [PATCH 2/6] Handling of if_exprt in char array assignment We handle that by calling constraint generation for "if" expressions. --- src/solvers/refinement/string_refinement.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index b8605ac3fb7..09d88f7817f 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -218,12 +218,17 @@ 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 2e6d2ce68fd820ed851244affdd463c3c76dab3a Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Sun, 9 Jul 2017 09:41:33 +0100 Subject: [PATCH 3/6] Using warning() for warning messages in string solver --- src/solvers/refinement/string_refinement.cpp | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 09d88f7817f..048ad34e41d 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -231,8 +231,7 @@ bool string_refinementt::add_axioms_for_string_assigns( } 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; } } @@ -375,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; @@ -397,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; } @@ -409,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 From b84d9d59bb9e110a3821ab106dfd69e2751e1c47 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Sun, 9 Jul 2017 10:50:52 +0100 Subject: [PATCH 4/6] Handling of if_exprt in checking universal axioms of string solver --- src/solvers/refinement/string_refinement.cpp | 24 +++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 048ad34e41d..bdc33e7fe6d 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -859,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 @@ -892,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()); From cc201f7a7fdcfa15e66dfbd8dd4e301f211790e1 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Sun, 9 Jul 2017 10:43:03 +0100 Subject: [PATCH 5/6] Test for char array expressions containing if_expr in VCC The added test are failing with versions of the string solver that would not take into account if expressions. --- .../strings-smoke-tests/java_if/test.class | Bin 0 -> 914 bytes .../strings-smoke-tests/java_if/test.desc | 9 +++++++++ .../strings-smoke-tests/java_if/test.java | 16 ++++++++++++++++ 3 files changed, 25 insertions(+) create mode 100644 regression/strings-smoke-tests/java_if/test.class create mode 100644 regression/strings-smoke-tests/java_if/test.desc create mode 100644 regression/strings-smoke-tests/java_if/test.java 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 0000000000000000000000000000000000000000..11958bd6ce9137566602a6e24fad7ad1628c9971 GIT binary patch literal 914 zcmZuvZEw<06n-u(v~*=K#s;Y9m{SY5p>w{)#ptHSMAQ!$&8A-py;(ZD7Tcn~W&8pC z=t}~Li*H~3Pa4mqY|Lqz+4xp{N8Ozk_n!zbC3Z~PWyl$o#g$c?J64$?Kh8zv z*1EQ1ai1Xfx#M_qg5$zp91%{(MJ(%>LRQBm6d3df9}(+h>}7_+nEm#?Lw9}OBYIhM zso;u^tGGrMK0hQp>XL-d7>E9j><~UC%ua{9X(B>3^dcJK;IF!-6C5cr zDqW%3rN_;$J2YU1S&Ij@&#eP3G?%bT37YOE%JfoV^rTp(AZ(#X0trKo))_jLXlJy? zs{^nP0*F~!6T_c0Hsn#DSU}&=RY7H{Ul4mxm9kQE5AsGfK0u;Tm6m@%*~MgyqVG`p zP@jE7vWI-F4=p>|H#CnSZ~sLH-r!4yYKza=aw I4bvz80D92A*8l(j literal 0 HcmV?d00001 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(); + } +} From 05ffc71c54da2f0e59a9b6054dc71390ad65b7e1 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 12 Jul 2017 11:22:59 +0100 Subject: [PATCH 6/6] Setting bound in if_exprt for constant arrays Characters arrays used for strings are either infinite length or constant array with fixed length (ID_array). In this latter case we need to set up the bound of axioms accordingly. --- .../refinement/string_constraint_generator_main.cpp | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 60bdc637b42..00b494eccaf 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -294,12 +294,21 @@ void string_constraint_generatort::add_axioms_for_if_array( // 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)); - string_constraintt a1(qvar, max_length, expr.cond(), qequal); + + // 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)); - string_constraintt a2(qvar2, max_length, not_exprt(expr.cond()), qequal2); + // 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); }