From 9a8c063036dfd4c1f7a6c3d6d566df704108eb4c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 16 Aug 2017 07:02:22 +0100 Subject: [PATCH 01/12] Setting string-max-length for several tests Cbmc can potentialy run out of memory if no maximum string length is set. This happens more often with the new version of check axioms because a concretization step is made to be more precise in the check. --- regression/strings-smoke-tests/java_append_char/test.desc | 2 +- regression/strings-smoke-tests/java_case/test.desc | 2 +- regression/strings-smoke-tests/java_insert_char/test.desc | 2 +- regression/strings-smoke-tests/java_insert_char_array/test.desc | 2 +- regression/strings-smoke-tests/java_insert_int/test.desc | 2 +- regression/strings-smoke-tests/java_insert_multiple/test.desc | 2 +- regression/strings-smoke-tests/java_insert_string/test.desc | 2 +- regression/strings-smoke-tests/java_int_to_string/test3.desc | 2 +- regression/strings-smoke-tests/java_int_to_string/test5.desc | 2 +- .../java_int_to_string_with_radix/test_binary1.desc | 2 +- .../java_int_to_string_with_radix/test_binary2.desc | 2 +- .../java_int_to_string_with_radix/test_hex1.desc | 2 +- .../java_int_to_string_with_radix/test_hex2.desc | 2 +- .../java_int_to_string_with_radix/test_hex3.desc | 2 +- .../java_int_to_string_with_radix/test_octal2.desc | 2 +- .../java_int_to_string_with_radix/test_octal3.desc | 2 +- .../java_long_to_string_with_radix/test_hex1.desc | 2 +- .../java_long_to_string_with_radix/test_hex3.desc | 2 +- .../java_long_to_string_with_radix/test_octal1.desc | 2 +- .../java_long_to_string_with_radix/test_octal2.desc | 2 +- .../java_long_to_string_with_radix/test_octal3.desc | 2 +- regression/strings-smoke-tests/java_value_of_float/test.desc | 2 +- regression/strings-smoke-tests/java_value_of_float_2/test.desc | 2 +- regression/strings-smoke-tests/java_value_of_long/test.desc | 2 +- regression/strings/StringStartEnd02/test.desc | 2 +- regression/strings/java_append_char/test.desc | 2 +- regression/strings/java_case/test.desc | 2 +- regression/strings/java_char_array_init/test.desc | 2 +- regression/strings/java_insert_char/test.desc | 2 +- regression/strings/java_insert_char_array/test.desc | 2 +- regression/strings/java_insert_int/test.desc | 2 +- regression/strings/java_insert_string/test.desc | 2 +- 32 files changed, 32 insertions(+), 32 deletions(-) diff --git a/regression/strings-smoke-tests/java_append_char/test.desc b/regression/strings-smoke-tests/java_append_char/test.desc index 88d1cbf2114..7fdd9f47961 100644 --- a/regression/strings-smoke-tests/java_append_char/test.desc +++ b/regression/strings-smoke-tests/java_append_char/test.desc @@ -1,6 +1,6 @@ CORE test_append_char.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_case/test.desc b/regression/strings-smoke-tests/java_case/test.desc index d2508fa3489..2889787e47a 100644 --- a/regression/strings-smoke-tests/java_case/test.desc +++ b/regression/strings-smoke-tests/java_case/test.desc @@ -1,6 +1,6 @@ CORE test_case.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* file test_case.java line 10 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_insert_char/test.desc b/regression/strings-smoke-tests/java_insert_char/test.desc index 0e9a06d5afb..88200524d70 100644 --- a/regression/strings-smoke-tests/java_insert_char/test.desc +++ b/regression/strings-smoke-tests/java_insert_char/test.desc @@ -1,6 +1,6 @@ CORE test_insert_char.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_insert_char_array/test.desc b/regression/strings-smoke-tests/java_insert_char_array/test.desc index 082771dd2db..6fc7a12f439 100644 --- a/regression/strings-smoke-tests/java_insert_char_array/test.desc +++ b/regression/strings-smoke-tests/java_insert_char_array/test.desc @@ -1,6 +1,6 @@ CORE test_insert_char_array.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_insert_int/test.desc b/regression/strings-smoke-tests/java_insert_int/test.desc index dc039fedbea..488e2bc8766 100644 --- a/regression/strings-smoke-tests/java_insert_int/test.desc +++ b/regression/strings-smoke-tests/java_insert_int/test.desc @@ -1,6 +1,6 @@ FUTURE test_insert_int.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_insert_multiple/test.desc b/regression/strings-smoke-tests/java_insert_multiple/test.desc index bb9a23f1b5c..d3236ab78ee 100644 --- a/regression/strings-smoke-tests/java_insert_multiple/test.desc +++ b/regression/strings-smoke-tests/java_insert_multiple/test.desc @@ -1,6 +1,6 @@ CORE test_insert_multiple.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_insert_string/test.desc b/regression/strings-smoke-tests/java_insert_string/test.desc index 44bf9f268d9..2b91905e17e 100644 --- a/regression/strings-smoke-tests/java_insert_string/test.desc +++ b/regression/strings-smoke-tests/java_insert_string/test.desc @@ -1,6 +1,6 @@ CORE test_insert_string.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_int_to_string/test3.desc b/regression/strings-smoke-tests/java_int_to_string/test3.desc index 5b48152f26e..97565815465 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test3.desc +++ b/regression/strings-smoke-tests/java_int_to_string/test3.desc @@ -1,6 +1,6 @@ CORE Test3.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string/test5.desc b/regression/strings-smoke-tests/java_int_to_string/test5.desc index 08531bc36e0..524a176db3f 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test5.desc +++ b/regression/strings-smoke-tests/java_int_to_string/test5.desc @@ -1,6 +1,6 @@ CORE Test5.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc index 1f7de38eee8..20bd5377109 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc @@ -1,6 +1,6 @@ CORE Test_binary1.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc index cb1dd600e34..370139d2c42 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc @@ -1,6 +1,6 @@ CORE Test_binary2.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc index 4b691b9c528..48d705734ac 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc @@ -1,6 +1,6 @@ CORE Test_hex1.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc index d21d067e620..89c4928e147 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc @@ -1,6 +1,6 @@ CORE Test_hex2.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc index c9fbfae377e..0c5ff51b802 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc @@ -1,6 +1,6 @@ CORE Test_hex3.class ---refine-strings +--refine-strings --string-max-length 100 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc index 06520bcde35..aee4977a75f 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc @@ -1,6 +1,6 @@ CORE Test_octal2.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc index 32f319a9876..b7a5ceb3ce1 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc @@ -1,6 +1,6 @@ CORE Test_octal3.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc index 4b691b9c528..48d705734ac 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc @@ -1,6 +1,6 @@ CORE Test_hex1.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc index c9fbfae377e..0c5ff51b802 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc @@ -1,6 +1,6 @@ CORE Test_hex3.class ---refine-strings +--refine-strings --string-max-length 100 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc index 9afe7b06279..8188ebc0ee9 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc @@ -1,6 +1,6 @@ CORE Test_octal1.class ---refine-strings +--refine-strings --string-max-length 100 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc index 06520bcde35..3884ae1fa9f 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc @@ -1,6 +1,6 @@ CORE Test_octal2.class ---refine-strings +--refine-strings --string-max-length 100 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc index 32f319a9876..527357b801e 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc @@ -1,6 +1,6 @@ CORE Test_octal3.class ---refine-strings +--refine-strings --string-max-length 100 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_value_of_float/test.desc b/regression/strings-smoke-tests/java_value_of_float/test.desc index d1cc84bd13a..4e3e8769be6 100644 --- a/regression/strings-smoke-tests/java_value_of_float/test.desc +++ b/regression/strings-smoke-tests/java_value_of_float/test.desc @@ -1,6 +1,6 @@ CORE test.class ---refine-strings --function test.check +--refine-strings --function test.check --string-max-length 100 ^EXIT=10$ ^SIGNAL=0$ assertion.* file test.java line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_value_of_float_2/test.desc b/regression/strings-smoke-tests/java_value_of_float_2/test.desc index 8a2a2bc6207..370b9327f58 100644 --- a/regression/strings-smoke-tests/java_value_of_float_2/test.desc +++ b/regression/strings-smoke-tests/java_value_of_float_2/test.desc @@ -1,6 +1,6 @@ KNOWNBUG test.class ---refine-strings --function test.check +--refine-strings --function test.check --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* file test.java line 6 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_value_of_long/test.desc b/regression/strings-smoke-tests/java_value_of_long/test.desc index f96a114f708..c7ea25ab2f8 100644 --- a/regression/strings-smoke-tests/java_value_of_long/test.desc +++ b/regression/strings-smoke-tests/java_value_of_long/test.desc @@ -1,6 +1,6 @@ CORE test.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* file test.java line 9 .* SUCCESS$ diff --git a/regression/strings/StringStartEnd02/test.desc b/regression/strings/StringStartEnd02/test.desc index a650aa0ebe9..deddbb5b902 100644 --- a/regression/strings/StringStartEnd02/test.desc +++ b/regression/strings/StringStartEnd02/test.desc @@ -1,6 +1,6 @@ CORE StringStartEnd02.class ---refine-strings --unwind 30 +--refine-strings --unwind 30 --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 13 .* FAILURE$ diff --git a/regression/strings/java_append_char/test.desc b/regression/strings/java_append_char/test.desc index e39f1d5ebe8..1c583f7be2d 100644 --- a/regression/strings/java_append_char/test.desc +++ b/regression/strings/java_append_char/test.desc @@ -1,6 +1,6 @@ CORE test_append_char.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/java_case/test.desc b/regression/strings/java_case/test.desc index 1dee2b7dd3e..22d58ddb3ac 100644 --- a/regression/strings/java_case/test.desc +++ b/regression/strings/java_case/test.desc @@ -1,6 +1,6 @@ CORE test_case.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ diff --git a/regression/strings/java_char_array_init/test.desc b/regression/strings/java_char_array_init/test.desc index 3efff6619b7..61a71f5034f 100644 --- a/regression/strings/java_char_array_init/test.desc +++ b/regression/strings/java_char_array_init/test.desc @@ -1,6 +1,6 @@ CORE test_init.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 14.* FAILURE$ diff --git a/regression/strings/java_insert_char/test.desc b/regression/strings/java_insert_char/test.desc index 406a20e9c52..cdda3eeae95 100644 --- a/regression/strings/java_insert_char/test.desc +++ b/regression/strings/java_insert_char/test.desc @@ -1,6 +1,6 @@ CORE test_insert_char.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ diff --git a/regression/strings/java_insert_char_array/test.desc b/regression/strings/java_insert_char_array/test.desc index 49a3afbffce..648fec2fa7d 100644 --- a/regression/strings/java_insert_char_array/test.desc +++ b/regression/strings/java_insert_char_array/test.desc @@ -1,6 +1,6 @@ CORE test_insert_char_array.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 12.* FAILURE$ diff --git a/regression/strings/java_insert_int/test.desc b/regression/strings/java_insert_int/test.desc index aa1f5cacab2..bc25e9abf3c 100644 --- a/regression/strings/java_insert_int/test.desc +++ b/regression/strings/java_insert_int/test.desc @@ -1,6 +1,6 @@ CORE test_insert_int.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ diff --git a/regression/strings/java_insert_string/test.desc b/regression/strings/java_insert_string/test.desc index 7ed578bfca5..79fa2931c93 100644 --- a/regression/strings/java_insert_string/test.desc +++ b/regression/strings/java_insert_string/test.desc @@ -1,6 +1,6 @@ CORE test_insert_string.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ From f255abb988de26f36e3f23616ddf1407ffac46c6 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 18 Aug 2017 11:47:59 +0100 Subject: [PATCH 02/12] Adding a next_sibling_or_parent iterator This allows to skip childrens of a node in iteration. Useful when substituting an expression with another on which we do not want to iterate. --- src/util/expr_iterator.h | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/util/expr_iterator.h b/src/util/expr_iterator.h index 7f6b83440f0..be228bcfba4 100644 --- a/src/util/expr_iterator.h +++ b/src/util/expr_iterator.h @@ -55,7 +55,6 @@ inline bool operator==( const depth_iterator_expr_statet &right) { return left.it==right.it && left.expr.get()==right.expr.get(); } - /// Depth first search iterator base - iterates over supplied expression /// and all its operands recursively. /// Base class using CRTP @@ -97,11 +96,19 @@ class depth_iterator_baset return this->downcast(); } + depth_iterator_t &next_sibling_or_parent() + { + PRECONDITION(!m_stack.empty()); + m_stack.back().it=m_stack.back().end; + ++(*this); + return this->downcast(); + } + /// Post-increment operator /// Expensive copy. Avoid if possible depth_iterator_t operator++(int) { - depth_iterator_t tmp(*this); + depth_iterator_t tmp(this->downcast()); this->operator++(); return tmp; } From 5d3771a7ed2efa4db34c1622dd707a0207ce710b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 18 Aug 2017 11:51:42 +0100 Subject: [PATCH 03/12] Adding unit tests for next_sibling_or_parent of an iterator --- unit/util/expr_iterator.cpp | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/unit/util/expr_iterator.cpp b/unit/util/expr_iterator.cpp index 4b914b01551..b806448b5c9 100644 --- a/unit/util/expr_iterator.cpp +++ b/unit/util/expr_iterator.cpp @@ -133,3 +133,26 @@ TEST_CASE("Iterate over a 3-level tree, mutate - set all types to ID_symbol") REQUIRE(expr.get().id()==ID_symbol); } } + +TEST_CASE("next_sibling_or_parent, next sibling") +{ + std::vector input(4); + input[1].operands()={ input[3] }; + input[2].id(ID_int); + input[0].operands()={ input[1], input[2] }; + auto it=input[0].depth_begin(); + it++; + it.next_sibling_or_parent(); + REQUIRE(*it==input[2]); +} + +TEST_CASE("next_sibling_or_parent, next parent ") +{ + std::vector input(3); + input[1].operands()={ input[2] }; + input[0].operands()={ input[1] }; + auto it=input[0].depth_begin(); + it++; + it.next_sibling_or_parent(); + REQUIRE(it==input[0].depth_end()); +} From df61cebbfac2d898e4677e0a51bdc96d43aa1c79 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 15 Aug 2017 14:01:48 +0100 Subject: [PATCH 04/12] Better debug info --- src/solvers/refinement/string_refinement.cpp | 29 +++++++++++++------- 1 file changed, 19 insertions(+), 10 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 6b8966c7d6f..e3f7886bb80 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1088,17 +1088,14 @@ static exprt negation_of_constraint(const string_constraintt &axiom) /// \return a Boolean bool string_refinementt::check_axioms() { - debug() << "string_refinementt::check_axioms: ===============" - << "===========================================" << eom; - debug() << "string_refinementt::check_axioms: build the" - << " interpretation from the model of the prop_solver" << eom; + debug() << "string_refinementt::check_axioms:" << eom; debug_model(); // Maps from indexes of violated universal axiom to a witness of violation std::map violated; - debug() << "there are " << universal_axioms.size() - << " universal axioms" << eom; + debug() << "string_refinement::check_axioms: " << universal_axioms.size() + << " universal axioms:" << eom; for(size_t i=0; i Date: Tue, 29 Aug 2017 10:34:27 +0100 Subject: [PATCH 05/12] Function for conversion from expression to size_t --- src/solvers/refinement/string_refinement.cpp | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index e3f7886bb80..aa1b7b04c92 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -289,6 +289,26 @@ bool string_refinementt::add_axioms_for_string_assigns( return true; } +/// Convert exprt to a specific type. Throw bad_cast if conversion +/// cannot be performed +/// Generic case doesn't exist, specialize for different types accordingly +/// TODO: this should go to util +template +T expr_cast(const exprt&); + +template<> +std::size_t expr_cast(const exprt& val_expr) +{ + mp_integer val_mb; + if(to_integer(val_expr, val_mb)) + throw std::bad_cast(); + if(!val_mb.is_long()) + throw std::bad_cast(); + if(val_mb<0) + throw std::bad_cast(); + return val_mb.to_long(); +} + /// If the expression is of type string, then adds constants to the index set to /// force the solver to pick concrete values for each character, and fill the /// maps `found_length` and `found_content`. From f042ff7574cdbffbf865ca77e338698c9d15d92c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 29 Aug 2017 10:57:23 +0100 Subject: [PATCH 06/12] Replace pad_vector by fill_in_map_as_vector This function takes a map as argument which is more appropriate for the operation to perform. This also refactors `concretize_string` and `get_array` to use fill_in_map_as_vector --- src/solvers/refinement/string_refinement.cpp | 157 ++++++------------- src/solvers/refinement/string_refinement.h | 64 ++++---- 2 files changed, 80 insertions(+), 141 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index aa1b7b04c92..b2a3ad487bd 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -313,84 +313,55 @@ std::size_t expr_cast(const exprt& val_expr) /// force the solver to pick concrete values for each character, and fill the /// maps `found_length` and `found_content`. /// -/// The way this is done is by looking for the length of the string, -/// then for each `i` in the index set, look at the value found by -/// the solver and put it in the `result` table. -/// For indexes that are not present in the index set, we put the -/// same value as the next index that is present in the index set. -/// We do so by traversing the array backward, remembering the -/// last value that has been initialized. +/// The way this is done is by looking for the length of the string, +/// then for each `i` in the index set, look at the value found by +/// the solver and put it in the `result` table. +/// For indexes that are not present in the index set, we put the +/// same value as the next index that is present in the index set. +/// We do so by traversing the array backward, remembering the +/// last value that has been initialized. void string_refinementt::concretize_string(const exprt &expr) { if(is_refined_string_type(expr.type())) { - string_exprt str=to_string_expr(expr); - exprt length=get(str.length()); + const string_exprt str=to_string_expr(expr); + const exprt length=get(str.length()); exprt content=str.content(); replace_expr(symbol_resolve, content); found_length[content]=length; - mp_integer found_length; - if(!to_integer(length, found_length)) - { - INVARIANT( - found_length.is_long(), - string_refinement_invariantt("the length of a string should be a " - "long")); - INVARIANT( - found_length>=0, - string_refinement_invariantt("the length of a string should be >= 0")); - size_t concretize_limit=found_length.to_long(); - INVARIANT( - concretize_limit<=generator.max_string_length, - string_refinement_invariantt("string length must be less than the max " - "length")); - exprt content_expr=str.content(); - std::vector result; - - if(index_set[str.content()].empty()) - return; - - // Use the last index as the default character value - exprt last_concretized=simplify_expr( - get(str[minus_exprt(length, from_integer(1, length.type()))]), ns); - result.resize(concretize_limit, last_concretized); + const auto string_length=expr_cast(length); + INVARIANT( + string_length<=generator.max_string_length, + string_refinement_invariantt("string length must be less than the max " + "length")); + if(index_set[str.content()].empty()) + return; - // Keep track of the indexes for which we have actual values - std::set initialized; + std::map map; - for(const auto &i : index_set[str.content()]) + for(const auto &i : index_set[str.content()]) + { + const exprt simple_i=simplify_expr(get(i), ns); + mp_integer mpi_index; + bool conversion_failure=to_integer(simple_i, mpi_index); + if(!conversion_failure && mpi_index>=0 && mpi_index=concretize_limit) - { - debug() << "concretize_string: ignoring out of bound index: " - << from_expr(ns, "", simple_i) << eom; - } - else - { - // Add an entry in the result vector - size_t index=mp_index.to_long(); - exprt str_i=simplify_expr(str[simple_i], ns); - exprt value=simplify_expr(get(str_i), ns); - result[index]=value; - initialized.insert(index); - } + const exprt str_i=simplify_expr(str[simple_i], ns); + const exprt value=simplify_expr(get(str_i), ns); + std::size_t index=mpi_index.to_long(); + map.emplace(index, value); + } + else + { + debug() << "concretize_string: ignoring out of bound index: " + << from_expr(ns, "", simple_i) << eom; } - - // Pad the concretized values to the left to assign the uninitialized - // values of result. The indices greater than concretize_limit are - // already assigned to last_concretized. - pad_vector(result, initialized, last_concretized); - - array_exprt arr(to_array_type(content.type())); - arr.operands()=result; - debug() << "Concretized " << from_expr(ns, "", content_expr) - << " = " << from_expr(ns, "", arr) << eom; - found_content[content]=arr; } + array_exprt arr(to_array_type(content.type())); + arr.operands()=fill_in_map_as_vector(map); + debug() << "Concretized " << from_expr(ns, "", str.content()) + << " = " << from_expr(ns, "", arr) << eom; + found_content[content]=arr; } } @@ -735,62 +706,38 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const return empty_ret; } - std::vector concrete_array(n); - if(arr_val.id()=="array-list") { - std::set initialized; + DATA_INVARIANT( + arr_val.operands().size()%2==0, + string_refinement_invariantt("and index expression must be on a symbol, " + "with, array_of, if, or array, and all " + "cases besides array are handled above")); + std::map initial_map; for(size_t i=0; i - void pad_vector( - std::vector &result, - std::set &initialized, - T1 last_concretized) const; void concretize_string(const exprt &expr); void concretize_results(); @@ -164,39 +159,36 @@ class string_refinementt: public bv_refinementt exprt substitute_array_lists(exprt expr, size_t string_max_length); -/// Utility function for concretization of strings. Copies concretized values to -/// the left to initialize the unconcretized indices of concrete_array. -/// \param concrete_array: the vector to populate -/// \param initialized: the vector containing the indices of the concretized -/// values -/// \param last_concretized: initial value of the last concretized index -template -void string_refinementt::pad_vector( - std::vector &concrete_array, - std::set &initialized, - T1 last_concretized) const +exprt concretize_arrays_in_expression( + exprt expr, std::size_t string_max_length); + +/// Convert index-value map to a vector of values. If a value for an +/// index is not defined, set it to the value referenced by the next higher +/// index. The length of the resulting vector is the key of the map's +/// last element + 1 +/// \param index_value: map containing values of specific vector cells +/// \return Vector containing values as described in the map +template +std::vector fill_in_map_as_vector( + const std::map &index_value) { - // Pad the concretized values to the left to assign the uninitialized - // values of result. The indices greater than concretize_limit are - // already assigned to last_concretized. - for(auto j=initialized.rbegin(); j!=initialized.rend();) + std::vector result; + if(!index_value.empty()) { - size_t i=*j; - // The leftmost index to pad is the value + 1 of the next element in - // 'initialized'. Since we cannot use the binary '+' operator on set - // iterators, we must increment the iterator here instead of in the - // for loop. - j++; - size_t leftmost_index_to_pad=(j!=initialized.rend()?*(j)+1:0); - // pad until we reach the next initialized index (right to left) - while(i>leftmost_index_to_pad) - concrete_array[(i--)-1]=last_concretized; - INVARIANT( - i==leftmost_index_to_pad, - string_refinement_invariantt("Loop decrements i until it is not greater " - " than leftmost_index_to_pad")); - if(i>0) - last_concretized=concrete_array[i-1]; + result.resize(index_value.rbegin()->first+1); + for(auto it=index_value.rbegin(); it!=index_value.rend(); ++it) + { + const std::size_t index=it->first; + const T value=it->second; + const auto next=std::next(it); + const std::size_t leftmost_index_to_pad= + next!=index_value.rend() + ? next->first+1 + : 0; + for(std::size_t j=leftmost_index_to_pad; j<=index; j++) + result[j]=value; + } } + return result; } #endif From 1fd5bb2c1e6c7c090d015bd97b691a2c281afeeb Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 29 Aug 2017 11:02:32 +0100 Subject: [PATCH 07/12] Adding return check in substitute_array_with_expr --- src/solvers/refinement/string_refinement.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index b2a3ad487bd..01d3af1567c 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -848,6 +848,7 @@ exprt string_refinementt::substitute_array_with_expr( exprt else_expr=substitute_array_with_expr(with_expr.old(), index); const typet &type=then_expr.type(); CHECK_RETURN(else_expr.type()==type); + CHECK_RETURN(index.type()==with_expr.where().type()); return if_exprt( equal_exprt(index, with_expr.where()), then_expr, else_expr, type); } From 88c664c49979096bb73f952692a8479be88b3db9 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 29 Aug 2017 11:03:39 +0100 Subject: [PATCH 08/12] Add a function that fill an array represented by a with expression This interpret the result by propagating values that are set, to the left. --- src/solvers/refinement/string_refinement.cpp | 36 ++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 01d3af1567c..988ba93322f 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -863,6 +863,42 @@ exprt string_refinementt::substitute_array_with_expr( } } +/// Fill an array represented by a list of with_expr by propagating values to +/// the left. For instance `ARRAY_OF(12) WITH[2:=24] WITH[4:=42]` will give +/// `{ 24, 24, 24, 42, 42 }` +/// \param expr: an array expression in the form +/// `ARRAY_OF(x) WITH [i0:=v0] ... WITH [iN:=vN]` +/// \param string_max_length: bound on the length of strings +/// \return an array expression with filled in values, or expr if it is simply +/// an `ARRAY_OF(x)` expression +exprt fill_in_array_with_expr(const exprt &expr, std::size_t string_max_length) +{ + PRECONDITION(expr.type().id()==ID_array); + PRECONDITION(expr.id()==ID_with || expr.id()==ID_array_of); + + // Nothing to do for empty array + if(expr.id()==ID_array_of) + return expr; + + // Map of the parts of the array that are initialized + std::map initial_map; + + for(exprt it=expr; it.id()==ID_with; it=to_with_expr(it).old()) + { + // Add to `initial_map` all the pairs (index,value) contained in `WITH` + // statements + const with_exprt with_expr=to_with_expr(it); + const exprt &then_expr=with_expr.new_value(); + const auto index=expr_cast(with_expr.where()); + if(index Date: Tue, 29 Aug 2017 11:05:15 +0100 Subject: [PATCH 09/12] Remove useless line break --- src/solvers/refinement/string_refinement.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 988ba93322f..bd89531e19d 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -928,8 +928,7 @@ void string_refinementt::substitute_array_access(exprt &expr) const if(index_expr.array().id()==ID_with) { - expr=substitute_array_with_expr( - index_expr.array(), index_expr.index()); + expr=substitute_array_with_expr(index_expr.array(), index_expr.index()); return; } From e18a6bd8068312897094d47c63ccf8574413de02 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 29 Aug 2017 11:06:08 +0100 Subject: [PATCH 10/12] Add a function interpreting arrays inside an expression This interpret them in a way that makes sense to the string solver, by propagating values to the left. --- src/solvers/refinement/string_refinement.cpp | 27 ++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index bd89531e19d..6422a71c1ad 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -24,6 +24,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #include #include +#include #include #include #include @@ -1087,6 +1088,32 @@ static exprt negation_of_constraint(const string_constraintt &axiom) return negaxiom; } +/// Result of the solver `supert` should not be interpreted literally for char +/// arrays as not all indices are present in the index set. +/// In the given expression, we populate arrays at the indices for which the +/// solver has no constraint by copying values to the left. +/// For example an expression `ARRAY_OF(0) WITH [1:=2] WITH [4:=3]` would +/// be interpreted as `{ 2, 2, 3, 3, 3}`. +/// \param expr: expression to interpret +/// \param string_max_length: maximum size of arrays to consider +/// \return the interpreted expression +exprt concretize_arrays_in_expression(exprt expr, std::size_t string_max_length) +{ + auto it=expr.depth_begin(); + const auto end=expr.depth_end(); + while(it!=end) + { + if(it->id()==ID_with && it->type().id()==ID_array) + { + it.mutate()=fill_in_array_with_expr(*it, string_max_length); + it.next_sibling_or_parent(); + } + else + ++it; + } + return expr; +} + /// return true if the current model satisfies all the axioms /// \return a Boolean bool string_refinementt::check_axioms() From 2c7f23c409e6d5ecb592160857cf84cd1c6de443 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 29 Aug 2017 11:07:29 +0100 Subject: [PATCH 11/12] Concretize arrays in axioms when string solver checks axioms This makes the string solver more likely to come up with a solution to the formulas that are passed to it. --- src/solvers/refinement/string_refinement.cpp | 30 +++++++++++--------- 1 file changed, 17 insertions(+), 13 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 6422a71c1ad..04fb0fbdc3f 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1140,21 +1140,25 @@ bool string_refinementt::check_axioms() exprt negaxiom=negation_of_constraint(axiom_in_model); - debug() << " - axiom:\n" - << " " << from_expr(ns, "", axiom) << eom; - debug() << " - axiom_in_model:\n" - << " " << from_expr(ns, "", axiom_in_model) << eom; - debug() << " - negated_axiom:\n" - << " " << from_expr(ns, "", negaxiom) << eom; - - substitute_array_access(negaxiom, true); - - debug() << " - negated_axiom_without_array_access:\n" - << " " << from_expr(ns, "", negaxiom) << eom; - + debug() << " "<< i << ".\n" + << " - axiom:\n" + << " " << from_expr(ns, "", axiom) << eom; + debug() << " - axiom_in_model:\n" + << " " << from_expr(ns, "", axiom_in_model) << eom; + debug() << " - negated_axiom:\n" + << " " << from_expr(ns, "", negaxiom) << eom; + + exprt with_concretized_arrays=concretize_arrays_in_expression( + negaxiom, generator.max_string_length); + debug() << " - negated_axiom_with_concretized_array_access:\n" + << " " << from_expr(ns, "", with_concretized_arrays) << eom; + + substitute_array_access(with_concretized_arrays); + debug() << " - negated_axiom_without_array_access:\n" + << " " << from_expr(ns, "", with_concretized_arrays) << eom; exprt witness; - bool is_sat=is_axiom_sat(negaxiom, univ_var, witness); + bool is_sat=is_axiom_sat(with_concretized_arrays, univ_var, witness); if(is_sat) { From 8f51b01dba586215d98074ce5b7144650f14af39 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 17 Aug 2017 21:54:33 +0100 Subject: [PATCH 12/12] Adding unit test for concretize_arrays_in_expression --- unit/Makefile | 1 + .../string_refinement/concretize_array.cpp | 56 +++++++++++++++++++ 2 files changed, 57 insertions(+) create mode 100644 unit/solvers/refinement/string_refinement/concretize_array.cpp diff --git a/unit/Makefile b/unit/Makefile index 8fae7e49ca1..b24eeeab1ad 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -24,6 +24,7 @@ SRC += unit_tests.cpp \ solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \ solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \ solvers/refinement/string_refinement/substitute_array_list.cpp \ + solvers/refinement/string_refinement/concretize_array.cpp \ catch_example.cpp \ # Empty last line diff --git a/unit/solvers/refinement/string_refinement/concretize_array.cpp b/unit/solvers/refinement/string_refinement/concretize_array.cpp new file mode 100644 index 00000000000..ab4dc31ae5f --- /dev/null +++ b/unit/solvers/refinement/string_refinement/concretize_array.cpp @@ -0,0 +1,56 @@ +/*******************************************************************\ + + Module: Unit tests for concretize_array_expression in + solvers/refinement/string_refinement.cpp + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include +#include +#include +#include + +SCENARIO("concretize_array_expression", + "[core][solvers][refinement][string_refinement]") +{ + const typet char_type=unsignedbv_typet(16); + const typet int_type=signedbv_typet(32); + const exprt index1=from_integer(1, int_type); + const exprt charx=from_integer('x', char_type); + const exprt index4=from_integer(4, int_type); + const exprt chary=from_integer('y', char_type); + const exprt index100=from_integer(100, int_type); + const exprt char0=from_integer('0', char_type); + const exprt index2=from_integer(2, int_type); + array_typet array_type(char_type, infinity_exprt(int_type)); + + // input_expr is + // `'0' + (ARRAY_OF(0) WITH [1:=x] WITH [4:=y] WITH [100:=z])[2]` + const plus_exprt input_expr( + from_integer('0', char_type), + index_exprt( + with_exprt( + with_exprt( + with_exprt( + array_of_exprt(from_integer(0, char_type), array_type), + index1, + charx), + index4, + chary), + index100, + from_integer('z', char_type)), + index2)); + + // String max length is 50, so index 100 should get ignored. + const exprt concrete=concretize_arrays_in_expression(input_expr, 50); + + // The expected result is `'0' + { 'x', 'x', 'y', 'y', 'y' }` + array_exprt array(array_type); + array.operands()={charx, charx, chary, chary, chary}; + const plus_exprt expected(char0, index_exprt(array, index2)); + REQUIRE(concrete==expected); +}