From 36e579c5b01766f63abc712f30c4999789255b8d Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 5 Apr 2019 13:13:52 +0100 Subject: [PATCH 1/3] Handle nil case in string_refinementt::get If the underlying solver does not know about the existence of an array, it can return nil, which shouldn't be returned inside an index_expression as in particular the type will be broken. --- src/solvers/strings/string_refinement.cpp | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index ac045d66c10..70caadd5625 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -2060,6 +2060,12 @@ exprt string_refinementt::get(const exprt &expr) const } const auto array = supert::get(current.get()); const auto index = get(index_expr->index()); + + // If the underlying solver does not know about the existence of an array, + // it can return nil, which cannot be used in the expression returned here. + if(array.is_nil()) + return index_exprt(current, index); + const exprt unknown = from_integer(CHARACTER_FOR_UNKNOWN, index_expr->type()); if( @@ -2070,12 +2076,9 @@ exprt string_refinementt::get(const exprt &expr) const return sparse_array->to_if_expression(index); } - INVARIANT( - array.is_nil() || array.id() == ID_symbol || - array.id() == ID_nondet_symbol, - std::string("apart from symbols, array valuations can be interpreted as " - "sparse arrays, id: ") + - id2string(array.id())); + INVARIANT(array.id() == ID_symbol || array.id() == ID_nondet_symbol, + "Apart from symbols, array valuations can be interpreted as " + "sparse arrays. Array model : " + array.pretty()); return index_exprt(array, index); } From 9962b7ce85cf7e05ecc148806409205cbf883489 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 5 Apr 2019 13:52:29 +0100 Subject: [PATCH 2/3] Constrain all generated strings to have non-negative length Generated strings should have positive length, not adding these lemmas could potentially lead to overflow errors in check_axioms which means the solver will end with an error because the index set is empty. --- src/solvers/strings/string_refinement.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 70caadd5625..548ebfbeea1 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -790,6 +790,13 @@ decision_proceduret::resultt string_refinementt::dec_solve() for(const auto &instance : initial_instances) add_lemma(instance); + // All generated strings should have non-negative length + for(const auto &string : generator.array_pool.created_strings()) + { + add_lemma(binary_relation_exprt{ + string.length(), ID_ge, from_integer(0, string.length().type())}); + } + while((loop_bound_--) > 0) { dependencies.clean_cache(); From 2c2c5edc49916b86c60b224f11659543388685c0 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 5 Apr 2019 13:03:31 +0100 Subject: [PATCH 3/3] Add a test for the string solver This is an example for which a branch with changes to symex (field-sensitivity) caused failure in the string solver because a nil expression got into the model. --- .../jbmc-strings/StringConcat/Test.class | Bin 5246 -> 5466 bytes .../jbmc-strings/StringConcat/Test.java | 11 +++++++++++ .../test_string_nondet_array.desc | 8 ++++++++ 3 files changed, 19 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/StringConcat/test_string_nondet_array.desc diff --git a/jbmc/regression/jbmc-strings/StringConcat/Test.class b/jbmc/regression/jbmc-strings/StringConcat/Test.class index 7600fbe19d0fec393e7b41d7581e25a5b10474fc..b1d54f1ccb5b39819a42295ffe0335766fb92519 100644 GIT binary patch delta 1030 zcmZXT%TE(g6vn^XX*-u;N?${1M39%*QXYzk3WB`kp#?Z~G_$T0m z5M8h}F(k$`VWCEs7hIT`&5B=m_ez%eMsA&&DL7dZSJ!yF?VqZ}7G#yBojTnnes0N?+2SA!RUO`cp|YIjIsTN1{9Ycj0#ykU?RdE|W z{kx%2s=;BsMrv&fV?jk2iwuwvQgH_n1}PGWsaQf2gK037T|^OMFiwP45;E?pSVmlb zBz^Fh=VH;hV1mIMTD}*ItS}UN{xUNdq2)D6PphO$XSYhj>D7;(bP)3A{U+lMoST4t*v z>;zh~o?aFX3r}e^X%(~&R&GecPPqQwQX`+lsjTKVOOmL~qCmBvG{{<>B2g^`FS85L z(|Ou$eM9sY>r9=XOHp9?hc00$9ANf6I5jG2Lwoj!X`7#lUf8M+iXsc7G_;&+hlPMM zd2H7@HL(O5uDHzC3mhM2O5KXSz*Tw7koI6EAwHpcM RT_%J~FsNOk;d-*^-k&peva|pI delta 839 zcmZXSTTc^F5Xb+g+x8rm?Pc4g5V0sN*A}Uwq6i{V#T%dqS{1OiatVg;fT)Ry@)3+# zdGWzlc{Q8xfQgBTiN+Tne8W%RM}V}AGi~D~?k00~&-~^;Gnv^*lseYGmbO0tIEDos z2Qa8`Mq)^ZhCw!G6^8jtE1Xj}uP~x;LE)mpC56ihR}@AS#uUbD5XDuAYdS0pN=)d8 zutWsc*`(P_Dop9PftwN;9k*~>;?Bz#PsFq>#fX@2#zkJ(KU^)T7~%pVCs6+&_c)hY z&aEt_Cf8P%Ru+dJEiKQ@uNs)aEFpOVchPQlYu(yGG}~FNH#UPTd+!NAV%k6sc>(v- z{KGYg`v&GPZ-3Li*dN_JjZtbC5WxmeFn#$TK&i>L*nUr>u9fb*^hXT6ZD?nY)90~- zXtl?^>G}?GDTsm)5}o8sAX!E>y(S~u@(+Si1?j4&*p~W9L`kjx7QuIkLloX!C0^Aq z@m&9(NZ~N2v8~!SL^!pX7#9+TR}~Q?5wVAG0c|1}BkTxz$~AQvV_efypA%p@iGXqy zVG?c+_*>*r+5pyE^gBc~1~PG`EJ&+Lk*HNbr!ZOcc$MA=yeE1hm`yOyf}<4FZpQa>kPliBR;B6?PvB$~TQFw{`(!4om3WFUDp*|sE-I%? z_u&+aI-$@8x3?Mo>}S<}n5u*Z?(Uh@JliQkyJ*^jrvRNIBT*V#e`V4HbLae+q39Nx fUPHRy!mT+7zoSbR{$2yt_P}Kf@kR`k-KT#69XpA^ diff --git a/jbmc/regression/jbmc-strings/StringConcat/Test.java b/jbmc/regression/jbmc-strings/StringConcat/Test.java index 74f91b81df0..6ea819f3eff 100644 --- a/jbmc/regression/jbmc-strings/StringConcat/Test.java +++ b/jbmc/regression/jbmc-strings/StringConcat/Test.java @@ -312,4 +312,15 @@ public String bufferNonDetLoop5(int cols, int columnWidth, String c, String data assert(false); return sb.toString(); } + + static boolean fromNonDetArray(String[] argv) + { + String s = argv[0]; + String u = s.concat("llo"); + if(u.equals("Hello")) { + return true; + } + return false; + } + } diff --git a/jbmc/regression/jbmc-strings/StringConcat/test_string_nondet_array.desc b/jbmc/regression/jbmc-strings/StringConcat/test_string_nondet_array.desc new file mode 100644 index 00000000000..28307c48203 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcat/test_string_nondet_array.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--function Test.fromNonDetArray --depth 10000 --unwind 5 --throw-runtime-exceptions --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --trace +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED +line 318 no uncaught exception: FAILURE +java.lang.ArrayIndexOutOfBoundsException|java.lang.NullPointerException