From 28a2ada787930a37cf84b9979f24e59fd0a69101 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 13 Dec 2017 15:45:50 +0000 Subject: [PATCH 1/4] Access in empty array should be unconstrained We make the result non-deterministic by introducing a new symbol --- src/solvers/refinement/string_refinement.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 8ff90e94676..7e63e911c1f 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1076,6 +1076,8 @@ exprt fill_in_array_expr(const array_exprt &expr, std::size_t string_max_length) /// 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` +/// * for an access in an empty array `{ }[x]` returns a fresh symbol, this +/// corresponds to a non-deterministic result /// \param expr: an expression containing array accesses /// \return an expression containing no array access static void substitute_array_access(exprt &expr) @@ -1124,13 +1126,17 @@ static void substitute_array_access(exprt &expr) "above")); array_exprt &array_expr=to_array_expr(index_expr.array()); - // Empty arrays do not need to be substituted. + const typet &char_type = index_expr.array().type().subtype(); + + // Access to an empty array is undefined (non deterministic result) if(array_expr.operands().empty()) + { + expr = symbol_exprt("out_of_bound_access", char_type); return; + } size_t last_index=array_expr.operands().size()-1; - const typet &char_type=index_expr.array().type().subtype(); exprt ite=array_expr.operands().back(); if(ite.type()!=char_type) From 682cd1a08dde5e7de89c36c3f895c4599b234999 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 14 Dec 2017 06:39:02 +0000 Subject: [PATCH 2/4] Use a symbol generator to avoid name clashes In substitute_array_access, we generate an unbound symbol for each access in an empty array. --- src/solvers/refinement/string_refinement.cpp | 26 ++++++++++++++------ 1 file changed, 19 insertions(+), 7 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 7e63e911c1f..fec692c9bf9 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1079,11 +1079,16 @@ exprt fill_in_array_expr(const array_exprt &expr, std::size_t string_max_length) /// * for an access in an empty array `{ }[x]` returns a fresh symbol, this /// corresponds to a non-deterministic result /// \param expr: an expression containing array accesses +/// \param symbol_generator: function which given a prefix and a type generates +/// a fresh symbol of the given type /// \return an expression containing no array access -static void substitute_array_access(exprt &expr) +static void substitute_array_access( + exprt &expr, + const std::function + &symbol_generator) { for(auto &op : expr.operands()) - substitute_array_access(op); + substitute_array_access(op, symbol_generator); if(expr.id()==ID_index) { @@ -1112,9 +1117,9 @@ static void substitute_array_access(exprt &expr) // 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); + substitute_array_access(true_case, symbol_generator); exprt false_case=index_exprt(if_expr.false_case(), index_expr.index()); - substitute_array_access(false_case); + substitute_array_access(false_case, symbol_generator); expr=if_exprt(if_expr.cond(), true_case, false_case); return; } @@ -1131,7 +1136,7 @@ static void substitute_array_access(exprt &expr) // Access to an empty array is undefined (non deterministic result) if(array_expr.operands().empty()) { - expr = symbol_exprt("out_of_bound_access", char_type); + expr = symbol_generator("out_of_bound_access", char_type); return; } @@ -1348,6 +1353,12 @@ static std::pair> check_axioms( const auto eom=messaget::eom; static const std::string indent = " "; static const std::string indent2 = " "; + // clang-format off + const auto gen_symbol = [&](const irep_idt &id, const typet &type) + { + return generator.fresh_symbol(id, type); + }; + // clang-format on stream << "string_refinementt::check_axioms:" << eom; @@ -1389,7 +1400,8 @@ static std::pair> check_axioms( negaxiom = simplify_expr(negaxiom, ns); exprt with_concretized_arrays = concretize_arrays_in_expression(negaxiom, max_string_length, ns); - substitute_array_access(with_concretized_arrays); + + substitute_array_access(with_concretized_arrays, gen_symbol); stream << indent << i << ".\n"; debug_check_axioms_step( @@ -1445,7 +1457,7 @@ static std::pair> check_axioms( exprt with_concrete_arrays = concretize_arrays_in_expression(negaxiom, max_string_length, ns); - substitute_array_access(with_concrete_arrays); + substitute_array_access(with_concrete_arrays, gen_symbol); stream << indent << i << ".\n"; debug_check_axioms_step( From 9a7fa2d9000a40524f111bd07354b31bfff47815 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 14 Dec 2017 06:57:38 +0000 Subject: [PATCH 3/4] Correct lower bound in String indexOf --- .../refinement/string_constraint_generator_indexof.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index 27f7e96bfb7..295c18df903 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -59,15 +59,19 @@ exprt string_constraint_generatort::add_axioms_for_index_of( equal_exprt(str[index], c))); axioms.push_back(a3); + const auto zero = from_integer(0, index_type); + const if_exprt lower_bound( + binary_relation_exprt(from_index, ID_le, zero), zero, from_index); + symbol_exprt n=fresh_univ_index("QA_index_of", index_type); string_constraintt a4( - n, from_index, index, contains, not_exprt(equal_exprt(str[n], c))); + n, lower_bound, index, contains, not_exprt(equal_exprt(str[n], c))); axioms.push_back(a4); symbol_exprt m=fresh_univ_index("QA_index_of", index_type); string_constraintt a5( m, - from_index, + lower_bound, str.length(), not_exprt(contains), not_exprt(equal_exprt(str[m], c))); From f3b4c9b7e268a5bce672f715e22e258279b1e32c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 13 Dec 2017 15:02:48 +0000 Subject: [PATCH 4/4] Test for verification of the indexOf method One of these is exhaustive and too slow to run so it is marked as THOROUGH and should be run every time axioms for the indexOf methods are touched. --- .../jbmc-strings/StringIndexOf/Test.class | Bin 0 -> 1179 bytes .../jbmc-strings/StringIndexOf/Test.java | 46 ++++++++++++++++++ .../jbmc-strings/StringIndexOf/test.desc | 7 +++ .../jbmc-strings/StringIndexOf/test2.desc | 14 ++++++ .../StringIndexOf/test_thorough.desc | 7 +++ 5 files changed, 74 insertions(+) create mode 100644 regression/jbmc-strings/StringIndexOf/Test.class create mode 100644 regression/jbmc-strings/StringIndexOf/Test.java create mode 100644 regression/jbmc-strings/StringIndexOf/test.desc create mode 100644 regression/jbmc-strings/StringIndexOf/test2.desc create mode 100644 regression/jbmc-strings/StringIndexOf/test_thorough.desc diff --git a/regression/jbmc-strings/StringIndexOf/Test.class b/regression/jbmc-strings/StringIndexOf/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..736603942034bf2239b6a3d3fb85377f4ae2bceb GIT binary patch literal 1179 zcmah|OHUI~6#ni!JMC0TVQ8@}F9BPM5D6hh2}-IaO;8pP4K9pBJJNyL>U3&|Yq#!| zn22ne7#BX0LNL+2zrpxJOrxGVg|?UwXK^3rJLk;#zH{#P--llT%wpP)0M7amLtKM~ z1V0U^81zGKnumNCRx#qoIgF|pW9S(*D;3Le?Q*Gd-L9DHMJvz1?lCCycFA@Z7{p}i z4ug~_=Pib=CA(zZu0C3~oK^13Am<8JZi^w3T-r3Bn$tzIv@yNnI(BK}N+z44Ou-e` z%x&E=A0I_1Uc`)-nPA_1u6Xn-|4O;)FlRF)(uTBQxQ;1$lVxq|5|Qm~ZFrZS{WJ8h;&vNH7Lt%~hf`BrhHgj=m(n3@xy zj7z+2>!>|`-qz$DGHNM-9d#c@AMiGUUBBdK@M3s5fnUGqv&G#6P9?RJ-7@TOj&G89w4O2tJ|#>T(d1WS=3f zSIO%x?GK216}@NyQy51 zloKfCFzgGJiGVQgu?fZ04kCmVIx*oSW~m)<|6(EE>EO0_I#%dzL|bTA>{VM43UpzvvJ2`$rH&C^lN-VqaNJ<7nHK!rT_o{ literal 0 HcmV?d00001 diff --git a/regression/jbmc-strings/StringIndexOf/Test.java b/regression/jbmc-strings/StringIndexOf/Test.java new file mode 100644 index 00000000000..6732eba723a --- /dev/null +++ b/regression/jbmc-strings/StringIndexOf/Test.java @@ -0,0 +1,46 @@ +public class Test { + + public boolean check(String input_String, char input_char, int input_int) { + // Verify indexOf is conform to its specification + int i = input_String.indexOf(input_char, input_int); + + assert i < input_String.length(); + + int lower_bound; + if (input_int < 0) + lower_bound = 0; + else + lower_bound = input_int; + + if (i == -1) { + for (int j = lower_bound; j < input_String.length(); j++) + assert input_String.charAt(j) != input_char; + } else { + assert i >= lower_bound; + assert input_String.charAt(i) == input_char; + + for (int j = lower_bound; j < i; j++) + assert input_String.charAt(j) != input_char; + } + return true; + } + + public boolean check2() { + // Verification should fail, this is to check the solver does + // not get a contradiction + int i = "hello".indexOf('o', 1); + assert i == 4; + i = "hello".indexOf('h', 1); + assert i == -1; + i = "hello".indexOf('e', 4); + assert i == -1; + i = "hello".indexOf('e', 8); + assert i == -1; + i = "hello".indexOf('x', 0); + assert i == -1; + i = "hello".indexOf('h', -1000); + assert i == 0; + assert false; + return true; + } +} diff --git a/regression/jbmc-strings/StringIndexOf/test.desc b/regression/jbmc-strings/StringIndexOf/test.desc new file mode 100644 index 00000000000..9c17878eb94 --- /dev/null +++ b/regression/jbmc-strings/StringIndexOf/test.desc @@ -0,0 +1,7 @@ +CORE +Test.class +--refine-strings --function Test.check --unwind 4 --string-max-length 3 --java-assume-inputs-non-null +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/jbmc-strings/StringIndexOf/test2.desc b/regression/jbmc-strings/StringIndexOf/test2.desc new file mode 100644 index 00000000000..6fdbcd101f0 --- /dev/null +++ b/regression/jbmc-strings/StringIndexOf/test2.desc @@ -0,0 +1,14 @@ +CORE +Test.class +--refine-strings --function Test.check2 --unwind 10 --string-max-length 10 --java-assume-inputs-non-null +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 32 .* SUCCESS +assertion at file Test.java line 34 .* SUCCESS +assertion at file Test.java line 36 .* SUCCESS +assertion at file Test.java line 38 .* SUCCESS +assertion at file Test.java line 40 .* SUCCESS +assertion at file Test.java line 42 .* SUCCESS +assertion at file Test.java line 43 .* FAILURE +^VERIFICATION FAILED$ +-- diff --git a/regression/jbmc-strings/StringIndexOf/test_thorough.desc b/regression/jbmc-strings/StringIndexOf/test_thorough.desc new file mode 100644 index 00000000000..8e05fa5bfa7 --- /dev/null +++ b/regression/jbmc-strings/StringIndexOf/test_thorough.desc @@ -0,0 +1,7 @@ +THOROUGH +Test.class +--refine-strings --function Test.check --unwind 10 --string-max-length 10 --java-assume-inputs-non-null +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +--