diff --git a/utbot-analytics/src/main/kotlin/org/utbot/features/UtExpressionStructureCounter.kt b/utbot-analytics/src/main/kotlin/org/utbot/features/UtExpressionStructureCounter.kt index f6f209875c..202be80baf 100644 --- a/utbot-analytics/src/main/kotlin/org/utbot/features/UtExpressionStructureCounter.kt +++ b/utbot-analytics/src/main/kotlin/org/utbot/features/UtExpressionStructureCounter.kt @@ -34,21 +34,6 @@ val featureIndex = listOf( UtBoolOpExpression::class.simpleName, UtIsExpression::class.simpleName, UtIteExpression::class.simpleName, - UtStringConst::class.simpleName, - UtConcatExpression::class.simpleName, - UtConvertToString::class.simpleName, - UtStringLength::class.simpleName, - UtStringPositiveLength::class.simpleName, - UtStringCharAt::class.simpleName, - UtStringEq::class.simpleName, - UtSubstringExpression::class.simpleName, - UtReplaceExpression::class.simpleName, - UtStartsWithExpression::class.simpleName, - UtEndsWithExpression::class.simpleName, - UtIndexOfExpression::class.simpleName, - UtContainsExpression::class.simpleName, - UtToStringExpression::class.simpleName, - UtSeqLiteral::class.simpleName, TREES, MAX_NODES, MIN_NODES, @@ -216,59 +201,6 @@ class UtExpressionStructureCounter(private val input: Iterable) : ) } - //const string value - override fun visit(expr: UtStringConst) = NestStat() - - override fun visit(expr: UtConcatExpression) = multipleExpression(expr.parts) - - override fun visit(expr: UtConvertToString): NestStat { - val stat = buildState(expr.expression) - stat.level++ - stat.nodes++ - return stat - } - - override fun visit(expr: UtStringToInt): NestStat { - val stat = buildState(expr.expression) - stat.level++ - stat.nodes++ - return stat - } - - override fun visit(expr: UtStringLength): NestStat { - val stat = buildState(expr.string) - stat.level++ - stat.nodes++ - return stat - } - - override fun visit(expr: UtStringPositiveLength): NestStat { - val stat = buildState(expr.string) - stat.level++ - stat.nodes++ - return stat - } - - override fun visit(expr: UtStringCharAt) = multipleExpressions(expr.string, expr.index) - - override fun visit(expr: UtStringEq) = multipleExpressions(expr.left, expr.right) - - override fun visit(expr: UtSubstringExpression) = multipleExpressions(expr.string, expr.beginIndex, expr.length) - - override fun visit(expr: UtReplaceExpression) = multipleExpressions(expr.string, expr.regex, expr.replacement) - - override fun visit(expr: UtStartsWithExpression) = multipleExpressions(expr.string, expr.prefix) - - override fun visit(expr: UtEndsWithExpression) = multipleExpressions(expr.string, expr.suffix) - - override fun visit(expr: UtIndexOfExpression) = multipleExpressions(expr.string, expr.substring) - - override fun visit(expr: UtContainsExpression) = multipleExpressions(expr.string, expr.substring) - - override fun visit(expr: UtToStringExpression) = multipleExpressions(expr.notNullExpr, expr.isNull) - - override fun visit(expr: UtSeqLiteral) = NestStat() - private fun multipleExpressions(vararg expressions: UtExpression) = multipleExpression(expressions.toList()) private fun multipleExpression(expressions: List): NestStat { @@ -311,14 +243,6 @@ class UtExpressionStructureCounter(private val input: Iterable) : override fun visit(expr: UtArrayApplyForAll): NestStat { return NestStat() } - - override fun visit(expr: UtStringToArray): NestStat { - return NestStat() - } - - override fun visit(expr: UtArrayToString): NestStat { - return NestStat() - } } data class NestStat(var nodes: Int = 1, var level: Int = 1) diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/examples/strings/GenericExamplesTest.kt b/utbot-framework-test/src/test/kotlin/org/utbot/examples/strings/GenericExamplesTest.kt new file mode 100644 index 0000000000..75261198a4 --- /dev/null +++ b/utbot-framework-test/src/test/kotlin/org/utbot/examples/strings/GenericExamplesTest.kt @@ -0,0 +1,38 @@ +package org.utbot.examples.strings + +import org.utbot.tests.infrastructure.UtValueTestCaseChecker +import org.utbot.tests.infrastructure.isException +import org.utbot.tests.infrastructure.CodeGeneration +import org.utbot.framework.plugin.api.CodegenLanguage +import org.junit.jupiter.api.Disabled +import org.junit.jupiter.api.Test +import org.utbot.testcheckers.eq + +@Disabled("TODO: Fails and takes too long") +internal class GenericExamplesTest : UtValueTestCaseChecker( + testClass = GenericExamples::class, + testCodeGeneration = true, + languagePipelines = listOf( + CodeGenerationLanguageLastStage(CodegenLanguage.JAVA), + CodeGenerationLanguageLastStage(CodegenLanguage.KOTLIN, CodeGeneration) + ) +) { + @Test + fun testContainsOkWithIntegerType() { + checkWithException( + GenericExamples::containsOk, + eq(2), + { obj, result -> obj == null && result.isException() }, + { obj, result -> obj != null && result.isSuccess && result.getOrNull() == false } + ) + } + + @Test + fun testContainsOkExampleTest() { + check( + GenericExamples::containsOkExample, + eq(1), + { result -> result == true } + ) + } +} diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/examples/strings/StringExamplesTest.kt b/utbot-framework-test/src/test/kotlin/org/utbot/examples/strings/StringExamplesTest.kt index 6275940f52..f2c879cd84 100644 --- a/utbot-framework-test/src/test/kotlin/org/utbot/examples/strings/StringExamplesTest.kt +++ b/utbot-framework-test/src/test/kotlin/org/utbot/examples/strings/StringExamplesTest.kt @@ -26,17 +26,13 @@ internal class StringExamplesTest : UtValueTestCaseChecker( ) ) { @Test - @Disabled("Flaky test: https://github.com/UnitTestBot/UTBotJava/issues/131 (will be enabled in new strings PR)") fun testByteToString() { - // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131 - withSolverTimeoutInMillis(5000) { - check( - StringExamples::byteToString, - eq(2), - { a, b, r -> a > b && r == a.toString() }, - { a, b, r -> a <= b && r == b.toString() }, - ) - } + check( + StringExamples::byteToString, + eq(2), + { a, b, r -> a > b && r == a.toString() }, + { a, b, r -> a <= b && r == b.toString() }, + ) } @Test @@ -53,43 +49,34 @@ internal class StringExamplesTest : UtValueTestCaseChecker( @Test fun testShortToString() { - // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131 - withSolverTimeoutInMillis(5000) { - check( - StringExamples::shortToString, - eq(2), - { a, b, r -> a > b && r == a.toString() }, - { a, b, r -> a <= b && r == b.toString() }, - ) - } + check( + StringExamples::shortToString, + ignoreExecutionsNumber, + { a, b, r -> a > b && r == a.toString() }, + { a, b, r -> a <= b && r == b.toString() }, + ) } @Test fun testIntToString() { - // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131 - withSolverTimeoutInMillis(5000) { - check( - StringExamples::intToString, - ignoreExecutionsNumber, - { a, b, r -> a > b && r == a.toString() }, - { a, b, r -> a <= b && r == b.toString() }, - ) - } + check( + StringExamples::intToString, + ignoreExecutionsNumber, + { a, b, r -> a > b && r == a.toString() }, + { a, b, r -> a <= b && r == b.toString() }, + ) } @Test fun testLongToString() { - // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131 - withSolverTimeoutInMillis(5000) { - check( - StringExamples::longToString, - ignoreExecutionsNumber, - { a, b, r -> a > b && r == a.toString() }, - { a, b, r -> a <= b && r == b.toString() }, - ) - } + check( + StringExamples::longToString, + ignoreExecutionsNumber, + { a, b, r -> a > b && r == a.toString() }, + { a, b, r -> a <= b && r == b.toString() }, + ) } @Test @@ -250,6 +237,15 @@ internal class StringExamplesTest : UtValueTestCaseChecker( ) } + @Test + fun testIsStringBuilderEmpty() { + check( + StringExamples::isStringBuilderEmpty, + eq(2), + { stringBuilder, result -> result == stringBuilder.isEmpty() } + ) + } + @Test @Disabled("Flaky on GitHub: https://github.com/UnitTestBot/UTBotJava/issues/1004") fun testIsValidUuid() { @@ -585,7 +581,7 @@ internal class StringExamplesTest : UtValueTestCaseChecker( withPushingStateFromPathSelectorForConcrete { check( StringExamples::equalsIgnoreCase, - eq(2), + ignoreExecutionsNumber, { s, r -> "SUCCESS".equals(s, ignoreCase = true) && r == "success" }, { s, r -> !"SUCCESS".equals(s, ignoreCase = true) && r == "failure" }, ) diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/Byte.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/Byte.java index 1189d16e6f..46f7cab42f 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/Byte.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/Byte.java @@ -1,10 +1,10 @@ package org.utbot.engine.overrides; import org.utbot.api.annotation.UtClassMock; -import org.utbot.engine.overrides.strings.UtNativeString; -import org.utbot.engine.overrides.strings.UtString; import org.utbot.engine.overrides.strings.UtStringBuilder; +import java.util.Arrays; + import static org.utbot.api.mock.UtMock.assume; import static org.utbot.engine.overrides.UtLogicMock.ite; import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely; @@ -54,11 +54,31 @@ public static String toString(byte b) { // and reduce time of solving queries with bv2int expressions assume(b < 128); assume(b >= -128); - // prefix = condition ? "-" : "" - String prefix = ite(condition, "-", ""); - UtStringBuilder sb = new UtStringBuilder(prefix); - // value = condition ? -i : i - int value = ite(condition, (byte) -b, b); - return sb.append(new UtString(new UtNativeString(value)).toStringImpl()).toString(); + + if (b == -128) { + return "-128"; + } else { + String prefix = ite(condition, "-", ""); + int value = ite(condition, (byte) -b, b); + char[] reversed = new char[3]; + int offset = 0; + while (value > 0) { + reversed[offset] = (char) ('0' + value % 10); + value = value / 10; + offset++; + } + + if (offset > 0) { + char[] buffer = new char[offset]; + int counter = 0; + while (offset > 0) { + offset--; + buffer[counter++] = reversed[offset]; + } + return prefix + new String(buffer); + } else { + return "0"; + } + } } } diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/Integer.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/Integer.java index 32e2e48e28..1517e60045 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/Integer.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/Integer.java @@ -1,8 +1,6 @@ package org.utbot.engine.overrides; import org.utbot.api.annotation.UtClassMock; -import org.utbot.engine.overrides.strings.UtNativeString; -import org.utbot.engine.overrides.strings.UtString; import org.utbot.engine.overrides.strings.UtStringBuilder; import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely; @@ -75,17 +73,30 @@ public static String toString(int i) { if (i == 0x80000000) { // java.lang.MIN_VALUE return "-2147483648"; } - // assumes are placed here to limit search space of solver - // and reduce time of solving queries with bv2int expressions - assumeOrExecuteConcretely(i <= 0x8000); - assumeOrExecuteConcretely(i >= -0x8000); + // condition = i < 0 boolean condition = less(i, 0); // prefix = condition ? "-" : "" String prefix = ite(condition, "-", ""); - UtStringBuilder sb = new UtStringBuilder(prefix); - // value = condition ? -i : i int value = ite(condition, -i, i); - return sb.append(new UtString(new UtNativeString(value)).toStringImpl()).toString(); + char[] reversed = new char[10]; + int offset = 0; + while (value > 0) { + reversed[offset] = (char) ('0' + value % 10); + value = value / 10; + offset++; + } + + if (offset > 0) { + char[] buffer = new char[offset]; + int counter = 0; + while (offset > 0) { + offset--; + buffer[counter++] = reversed[offset]; + } + return prefix + new String(buffer); + } else { + return "0"; + } } } diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/Long.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/Long.java index 22584bede5..b9cf5afa93 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/Long.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/Long.java @@ -1,8 +1,6 @@ package org.utbot.engine.overrides; import org.utbot.api.annotation.UtClassMock; -import org.utbot.engine.overrides.strings.UtNativeString; -import org.utbot.engine.overrides.strings.UtString; import org.utbot.engine.overrides.strings.UtStringBuilder; import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely; @@ -75,17 +73,30 @@ public static String toString(long l) { if (l == 0x8000000000000000L) { // java.lang.Long.MIN_VALUE return "-9223372036854775808"; } - // assumes are placed here to limit search space of solver - // and reduce time of solving queries with bv2int expressions - assumeOrExecuteConcretely(l <= 10000); - assumeOrExecuteConcretely(l >= -10000); // condition = l < 0 boolean condition = less(l, 0); // prefix = condition ? "-" : "" String prefix = ite(condition, "-", ""); - UtStringBuilder sb = new UtStringBuilder(prefix); // value = condition ? -l : l long value = ite(condition, -l, l); - return sb.append(new UtString(new UtNativeString(value)).toStringImpl()).toString(); + char[] reversed = new char[19]; + int offset = 0; + while (value > 0) { + reversed[offset] = (char) ('0' + value % 10); + value = value / 10; + offset++; + } + + if (offset > 0) { + char[] buffer = new char[offset]; + int i = 0; + while (offset > 0) { + offset--; + buffer[i++] = reversed[offset]; + } + return prefix + new String(buffer); + } else { + return "0"; + } } } diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/Short.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/Short.java index 529b4a3829..57943976e6 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/Short.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/Short.java @@ -1,8 +1,6 @@ package org.utbot.engine.overrides; import org.utbot.api.annotation.UtClassMock; -import org.utbot.engine.overrides.strings.UtNativeString; -import org.utbot.engine.overrides.strings.UtString; import org.utbot.engine.overrides.strings.UtStringBuilder; import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely; @@ -52,11 +50,32 @@ public static String toString(short s) { // and reduce time of solving queries with bv2int expressions assumeOrExecuteConcretely(s <= 10000); assumeOrExecuteConcretely(s >= -10000); - // prefix = condition ? "-" : "" - String prefix = ite(condition, "-", ""); - UtStringBuilder sb = new UtStringBuilder(prefix); - // value = condition ? -i : i - int value = ite(condition, (short)-s, s); - return sb.append(new UtString(new UtNativeString(value)).toStringImpl()).toString(); + + if (s == -32768) { + return "-32768"; + } else { + // prefix = condition ? "-" : "" + String prefix = ite(condition, "-", ""); + int value = ite(condition, (short) -s, s); + char[] reversed = new char[5]; + int offset = 0; + while (value > 0) { + reversed[offset] = (char) ('0' + value % 10); + value = value / 10; + offset++; + } + + if (offset > 0) { + char[] repr = new char[offset]; + int i = 0; + while (offset > 0) { + offset--; + repr[i++] = reversed[offset]; + } + return prefix + new String(repr); + } else { + return "0"; + } + } } } diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtArrayList.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtArrayList.java index e7990f1d6a..15914e2da1 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtArrayList.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtArrayList.java @@ -167,6 +167,25 @@ public T[] toArray(@NotNull T[] a) { return a; } + @Override + public String toString() { + StringBuilder builder = new StringBuilder(); + builder.append("["); + int size = size(); + if (size > 0) { + builder.append(get(0)); + } + + if (size > 1) { + for (int i = 1; i < size; i++) { + builder.append(", "); + builder.append(get(i)); + } + } + builder.append("]"); + return builder.toString(); + } + @Override public boolean add(E e) { preconditionCheck(); diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/strings/UtNativeString.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/strings/UtNativeString.java deleted file mode 100644 index 5d75c6dd05..0000000000 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/strings/UtNativeString.java +++ /dev/null @@ -1,102 +0,0 @@ -package org.utbot.engine.overrides.strings; - -/** - * An auxiliary class without implementation, - * that specifies interface of interaction with - * smt string objects. - * @see org.utbot.engine.UtNativeStringWrapper - */ -@SuppressWarnings("unused") -public class UtNativeString { - /** - * Constructor, that creates a new symbolic string. - * Length and content can be arbitrary and is set - * via path constraints. - */ - public UtNativeString() {} - - /** - * Constructor, that creates a new string - * that is equal smt expression: int2string(i)> - * - * if i is greater or equal to 0, than - * constructed string will be equal to - * i.toString()>, otherwise, it is undefined - * @param i number, that needs to be converted to string - */ - public UtNativeString(int i) { } - - /** - * Constructor, that creates a new string - * that is equal smt expression: int2string(l) - *

- * if i is greater or equal to 0, than - * constructed string will be equal to - * l.toString(), otherwise, it is undefined - * @param l number, that needs to be converted to string - */ - public UtNativeString(long l) {} - - /** - * Returned variable's expression is equal to - * mkInt2BV(str.length(this), Long.SIZE_BITS) - * @return the length of this string - */ - public int length() { - return 0; - } - - /** - * If string represent a decimal positive number, - * then returned value is equal to Integer.valueOf(this)> - * Otherwise, the result is equal to -1 - *

- * Returned variable's expression is equal to - * mkInt2BV(string2int(this), Long.SIZE_BITS) - */ - public int toInteger() { return 0; } - - /** - * If string represent a decimal positive number, - * then returned value is equal to Long.valueOf(this)> - * Otherwise, the result is equal to -1L - *

- * Returned variable's expression is equal to - * mkInt2BV(string2int(this), Long.SIZE_BITS)> - */ - public long toLong() { return 0; } - - /** - * If i in valid index range of string, then - * a returned value's expression is equal to - * mkSeqNth(this, i).cast(char) - * @param i the index of char value to be returned - * @return the specified char value - */ - public char charAt(int i) { - return '\0'; - } - - /** - * Returns a char array with the same content as this string, - * shifted by offset indexes to the left. - *

- * The returned value's UtExpression is equal to - * UtStringToArray(this, offset). - * @param offset - the number of indexes to be shifted to the left - * @return array of the string chars with shifted indexes by specified offset. - * @see org.utbot.engine.pc.UtArrayToString - */ - public char[] toCharArray(int offset) { return null; } - - /** - * If i in valid index range of string, then - * a returned value's expression is equal to - * mkSeqNth(this, i).cast(int) - * @param i the index of codePoint value to be returned - * @return the specified codePoint value - */ - public int codePointAt(int i) { - return 0; - } -} diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/strings/UtString.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/strings/UtString.java index 9db996fb52..627cea0d8a 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/strings/UtString.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/strings/UtString.java @@ -20,24 +20,6 @@ public class UtString implements java.io.Serializable, Comparable, CharS private static final long serialVersionUID = -6849794470754667710L; - public UtString(UtNativeString str) { - visit(this); - length = str.length(); - value = str.toCharArray(0); - } - - public static UtNativeString toUtNativeString(String s, int offset) { - char[] value = s.toCharArray(); - int length = value.length; - UtNativeString nativeString = new UtNativeString(); - assume(nativeString.length() == length - offset); - assume(nativeString.length() <= 2); - for (int i = offset; i < length; i++) { - assume(nativeString.charAt(i - offset) == value[i]); - } - return nativeString; - } - public UtString() { visit(this); value = new char[0]; @@ -344,8 +326,6 @@ public byte[] getBytes() { } private boolean contentEquals(char[] otherValue, int toffset, int ooffset, int n) { - //TODO: remove assume - assume(n <= 25); for (int j = 0; j < n; j++) { int i1 = toffset + j; int i2 = ooffset + j; @@ -358,8 +338,6 @@ private boolean contentEquals(char[] otherValue, int toffset, int ooffset, int n // for simpler analysis instead of contentEquals(otherValue, 0, 0, int n) private boolean contentEqualsZeroOffset(char[] otherValue, int n) { - //TODO: remove assume - assume(n <= 25); for (int i = 0; i < n; i++) { if (value[i] != otherValue[i]) { return false; @@ -433,8 +411,6 @@ public boolean contentEquals(CharSequence cs) { if (n != cs.length()) { return false; } - // TODO: remove assume - assume(n <= 25); for (int i = 0; i < n; i++) { if (v1[i] != cs.charAt(i)) { return false; @@ -455,8 +431,6 @@ public boolean equalsIgnoreCase(String anotherString) { return false; } char[] otherValue = anotherString.toCharArray(); - // TODO remove assume - assume(n <= 25); for (int j = 0; j < n; j++) { if (java.lang.Character.toLowerCase(value[j]) != java.lang.Character.toLowerCase(otherValue[j])) { return false; @@ -553,8 +527,6 @@ public boolean regionMatches(boolean ignoreCase, int toffset, char[] pa = other.toCharArray(); if (ignoreCase) { - // TODO remove assume - assume(len <= 25); for (int j = 0; j < len; j++) { if (java.lang.Character.toLowerCase(value[j + toffset]) != java.lang.Character.toLowerCase(pa[j + ooffset])) { return false; @@ -613,8 +585,6 @@ public int indexOf(int ch, int fromIndex) { if (ch < java.lang.Character.MIN_SUPPLEMENTARY_CODE_POINT) { // handle most cases here (ch is a BMP code point or a // negative value (invalid code point)) - // TODO remove assume - assume(max - fromIndex <= 10); for (int i = fromIndex; i < max; i++) { if (value[i] == ch) { return i; @@ -631,8 +601,6 @@ private int indexOfSupplementary(int ch, int fromIndex) { final char hi = java.lang.Character.highSurrogate(ch); final char lo = java.lang.Character.lowSurrogate(ch); final int max = length - 1; - // TODO remove assume - assume(max - fromIndex <= 10); for (int i = fromIndex; i < max; i++) { if (value[i] == hi && value[i + 1] == lo) { return i; @@ -692,8 +660,6 @@ public int indexOf(String str, int fromIndex) { } char[] v2 = str.toCharArray(); char ch = v2[0]; - // TODO remove assume - assume(max - fromIndex <= 10); for (int i = fromIndex; i < max; i++) { if (value[i] == ch && contentEquals(v2, i + 1, 1, strLength - 1)) { return i; @@ -721,8 +687,6 @@ public int lastIndexOf(String str, int fromIndex) { } char[] v2 = str.toCharArray(); char ch = v2[0]; - // TODO remove assume - assume(fromIndex <= 10); for (int i = fromIndex; i >= 0; i--) { if (value[i] == ch && contentEquals(v2, i + 1, 1, strLength - 1)) { return i; @@ -830,8 +794,6 @@ public String replaceFirst(String regex, String replacement) { if (replacement == null) { throw new NullPointerException(); } - assume(regex.length() < 10); - assume(replacement.length() < 10); executeConcretely(); return toString().replaceFirst(regex, replacement); } @@ -845,8 +807,6 @@ public String replaceAll(String regex, String replacement) { if (replacement == null) { throw new NullPointerException(); } - assume(regex.length() < 10); - assume(replacement.length() < 10); executeConcretely(); return toString().replaceAll(regex, replacement); } @@ -860,12 +820,20 @@ public String replace(CharSequence target, CharSequence replacement) { if (replacement == null) { throw new NullPointerException(); } - assume(target.length() < 10); - assume(replacement.length() < 10); executeConcretely(); return toString().replace(target, replacement); } + public String[] splitWithLimitImpl(String regex, int limit) { + return toString().split(regex, limit); + } + + public String[] split(String regex, int limit) { + preconditionCheck(); + return splitWithLimitImpl(regex, limit); + } + + /* public String[] split(String regex, int limit) { preconditionCheck(); if (regex == null) { @@ -878,18 +846,26 @@ public String[] split(String regex, int limit) { int size = limit == 0 ? length + 1 : min(limit, length + 1); String[] strings = new String[size]; strings[size] = substring(size - 1); - // TODO remove assume - assume(size < 10); for (int i = 0; i < size - 1; i++) { strings[i] = Character.toString(value[i]); } return strings; } - assume(regex.length() < 10); executeConcretely(); return toStringImpl().split(regex, limit); } + */ + + public String[] splitImpl(String regex) { + return toString().split(regex); + } + public String[] split(String regex) { + preconditionCheck(); + return splitImpl(regex); + } + + /* public String[] split(String regex) { preconditionCheck(); if (regex == null) { @@ -898,8 +874,6 @@ public String[] split(String regex) { if (regex.length() == 0) { String[] strings = new String[length + 1]; strings[length] = ""; - // TODO remove assume - assume(length <= 25); for (int i = 0; i < length; i++) { strings[i] = Character.toString(value[i]); } @@ -908,6 +882,7 @@ public String[] split(String regex) { executeConcretely(); return toStringImpl().split(regex); } + */ public String toLowerCase(Locale locale) { preconditionCheck(); diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt index 1de5fa185a..0e1f9c357e 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt @@ -29,7 +29,6 @@ import org.utbot.engine.pc.mkFloat import org.utbot.engine.pc.mkInt import org.utbot.engine.pc.mkLong import org.utbot.engine.pc.mkShort -import org.utbot.engine.pc.mkString import org.utbot.engine.pc.toSort import org.utbot.framework.UtSettings.checkNpeInNestedMethods import org.utbot.framework.UtSettings.checkNpeInNestedNotPrivateMethods @@ -298,7 +297,6 @@ val UtSort.defaultValue: UtExpression UtFp64Sort -> mkDouble(0.0) UtBoolSort -> mkBool(false) // empty string because we want to have a default value of the same sort as the items stored in the strings array - UtSeqSort -> mkString("") is UtArraySort -> if (itemSort is UtArraySort) nullObjectAddr else mkArrayWithConst(this, itemSort.defaultValue) else -> nullObjectAddr } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt index b398b18b24..b9c5a4dba0 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt @@ -6,7 +6,6 @@ import org.utbot.common.workaround import org.utbot.engine.MemoryState.CURRENT import org.utbot.engine.MemoryState.INITIAL import org.utbot.engine.MemoryState.STATIC_INITIAL -import org.utbot.engine.overrides.strings.UtNativeString import org.utbot.engine.pc.RewritingVisitor import org.utbot.engine.pc.UtAddrExpression import org.utbot.engine.pc.UtAddrSort @@ -1077,8 +1076,6 @@ fun localMemoryUpdate(vararg updates: Pair) = private val STRING_INTERNAL = ChunkId(java.lang.String::class.qualifiedName!!, "internal") -private val NATIVE_STRING_VALUE = ChunkId(UtNativeString::class.qualifiedName!!, "value") - internal val STRING_LENGTH get() = utStringClass.getField("length", IntType.v()) internal val STRING_VALUE @@ -1091,15 +1088,6 @@ internal val STRING_INTERNAL_DESCRIPTOR: MemoryChunkDescriptor get() = MemoryChunkDescriptor(STRING_INTERNAL, STRING_TYPE, SeqType) -internal val NATIVE_STRING_VALUE_DESCRIPTOR: MemoryChunkDescriptor - get() = MemoryChunkDescriptor(NATIVE_STRING_VALUE, utNativeStringClass.type, SeqType) - -/** - * Returns internal string representation by String object address, addr -> String - */ -fun Memory.nativeStringValue(addr: UtAddrExpression) = - PrimitiveValue(SeqType, findArray(NATIVE_STRING_VALUE_DESCRIPTOR).select(addr)).expr - private const val STRING_INTERN_MAP_LABEL = "java.lang.String_intern_map" /** diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ObjectWrappers.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ObjectWrappers.kt index 87e7470496..ee7af69f9f 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/ObjectWrappers.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/ObjectWrappers.kt @@ -15,7 +15,6 @@ import org.utbot.engine.overrides.collections.RangeModifiableUnlimitedArray import org.utbot.engine.overrides.collections.UtHashMap import org.utbot.engine.overrides.collections.UtHashSet import org.utbot.engine.overrides.security.UtSecurityManager -import org.utbot.engine.overrides.strings.UtNativeString import org.utbot.engine.overrides.strings.UtString import org.utbot.engine.overrides.strings.UtStringBuffer import org.utbot.engine.overrides.strings.UtStringBuilder @@ -54,7 +53,6 @@ val classToWrapper: MutableMap = putSootClass(UtStringBuilder::class, utStringBuilderClass) putSootClass(java.lang.StringBuffer::class, utStringBufferClass) putSootClass(UtStringBuffer::class, utStringBufferClass) - putSootClass(UtNativeString::class, utNativeStringClass) putSootClass(java.lang.CharSequence::class, utStringClass) putSootClass(java.lang.String::class, utStringClass) putSootClass(UtString::class, utStringClass) @@ -134,7 +132,6 @@ private val wrappers = mapOf( wrap(UtStringBuilder::class) { type, addr -> objectValue(type, addr, UtStringBuilderWrapper()) }, wrap(java.lang.StringBuffer::class) { type, addr -> objectValue(type, addr, UtStringBufferWrapper()) }, wrap(UtStringBuffer::class) { type, addr -> objectValue(type, addr, UtStringBufferWrapper()) }, - wrap(UtNativeString::class) { type, addr -> objectValue(type, addr, UtNativeStringWrapper()) }, wrap(java.lang.CharSequence::class) { type, addr -> objectValue(type, addr, StringWrapper()) }, wrap(java.lang.String::class) { type, addr -> objectValue(type, addr, StringWrapper()) }, wrap(UtString::class) { type, addr -> objectValue(type, addr, StringWrapper()) }, diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt index ec4dcd7a9b..a049d25800 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt @@ -94,7 +94,7 @@ import kotlinx.collections.immutable.persistentSetOf // hack const val MAX_LIST_SIZE = 10 const val MAX_RESOLVE_LIST_SIZE = 256 -const val MAX_STRING_SIZE = 40 +const val MAX_STRING_SIZE = 256 internal const val HARD_MAX_ARRAY_SIZE = 256 internal const val PREFERRED_ARRAY_SIZE = 2 diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt index 08a6083c36..ad68dd14fc 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt @@ -1,31 +1,20 @@ package org.utbot.engine import com.github.curiousoddman.rgxgen.RgxGen -import org.utbot.common.unreachableBranch -import org.utbot.engine.overrides.strings.UtNativeString import org.utbot.engine.overrides.strings.UtString import org.utbot.engine.overrides.strings.UtStringBuffer import org.utbot.engine.overrides.strings.UtStringBuilder import org.utbot.engine.pc.RewritingVisitor import org.utbot.engine.pc.UtAddrExpression import org.utbot.engine.pc.UtBoolExpression -import org.utbot.engine.pc.UtConvertToString import org.utbot.engine.pc.UtFalse -import org.utbot.engine.pc.UtIntSort -import org.utbot.engine.pc.UtLongSort -import org.utbot.engine.pc.UtStringCharAt -import org.utbot.engine.pc.UtStringLength -import org.utbot.engine.pc.UtStringToArray -import org.utbot.engine.pc.UtStringToInt import org.utbot.engine.pc.UtTrue -import org.utbot.engine.pc.cast import org.utbot.engine.pc.isConcrete import org.utbot.engine.pc.mkAnd import org.utbot.engine.pc.mkChar import org.utbot.engine.pc.mkEq import org.utbot.engine.pc.mkInt import org.utbot.engine.pc.mkNot -import org.utbot.engine.pc.mkString import org.utbot.engine.pc.select import org.utbot.engine.pc.toConcrete import org.utbot.engine.symbolic.asHardConstraint @@ -33,7 +22,6 @@ import org.utbot.framework.plugin.api.UtArrayModel import org.utbot.framework.plugin.api.UtAssembleModel import org.utbot.framework.plugin.api.UtExecutableCallModel import org.utbot.framework.plugin.api.UtModel -import org.utbot.framework.plugin.api.UtNullModel import org.utbot.framework.plugin.api.UtPrimitiveModel import org.utbot.framework.plugin.api.UtStatementModel import org.utbot.framework.plugin.api.classId @@ -44,8 +32,6 @@ import org.utbot.framework.plugin.api.util.constructorId import org.utbot.framework.plugin.api.util.defaultValueModel import org.utbot.framework.util.nextModelName import kotlin.math.max -import kotlinx.collections.immutable.persistentListOf -import kotlinx.collections.immutable.persistentSetOf import soot.CharType import soot.IntType import soot.Scene @@ -63,6 +49,10 @@ class StringWrapper : BaseOverriddenWrapper(utStringClass.name) { overriddenClass.getMethodByName(UtString::matchesImpl.name).subSignature private val charAtMethodSignature = overriddenClass.getMethodByName(UtString::charAtImpl.name).subSignature + private val splitWithLimitMethodSignature = + overriddenClass.getMethodByName(UtString::splitWithLimitImpl.name).subSignature + private val splitMethodSignature = + overriddenClass.getMethodByName(UtString::splitImpl.name).subSignature private fun Traverser.getValueArray(addr: UtAddrExpression) = getArrayField(addr, overriddenClass, STRING_VALUE) @@ -77,71 +67,20 @@ class StringWrapper : BaseOverriddenWrapper(utStringClass.name) { listOf(MethodResult(wrapper.copy(typeStorage = TypeStorage(method.returnType)))) } matchesMethodSignature -> { - val arg = parameters[0] as ObjectValue - val matchingLengthExpr = getIntFieldValue(arg, STRING_LENGTH).accept(RewritingVisitor()) - - if (!matchingLengthExpr.isConcrete) return null - - val matchingValueExpr = - selectArrayExpressionFromMemory(getValueArray(arg.addr)).accept(RewritingVisitor()) - val matchingLength = matchingLengthExpr.toConcrete() as Int - val matchingValue = CharArray(matchingLength) - - for (i in 0 until matchingLength) { - val charExpr = matchingValueExpr.select(mkInt(i)).accept(RewritingVisitor()) - - if (!charExpr.isConcrete) return null - - matchingValue[i] = (charExpr.toConcrete() as Number).toChar() - } - - val rgxGen = RgxGen(String(matchingValue)) - val matching = (rgxGen.generate()) - val notMatching = rgxGen.generateNotMatching() - - val thisLength = getIntFieldValue(wrapper, STRING_LENGTH) - val thisValue = selectArrayExpressionFromMemory(getValueArray(wrapper.addr)) - - val matchingConstraints = mutableSetOf() - matchingConstraints += mkEq(thisLength, mkInt(matching.length)) - for (i in matching.indices) { - matchingConstraints += mkEq(thisValue.select(mkInt(i)), mkChar(matching[i])) - } - - val notMatchingConstraints = mutableSetOf() - notMatchingConstraints += mkEq(thisLength, mkInt(notMatching.length)) - for (i in notMatching.indices) { - notMatchingConstraints += mkEq(thisValue.select(mkInt(i)), mkChar(notMatching[i])) - } - - return listOf( - MethodResult(UtTrue.toBoolValue(), matchingConstraints.asHardConstraint()), - MethodResult(UtFalse.toBoolValue(), notMatchingConstraints.asHardConstraint()) - ) + symbolicMatchesMethodImpl(wrapper, parameters) } charAtMethodSignature -> { - val index = parameters[0] as PrimitiveValue - val lengthExpr = getIntFieldValue(wrapper, STRING_LENGTH) - val inBoundsCondition = mkAnd(Le(0.toPrimitiveValue(), index), Lt(index, lengthExpr.toIntValue())) - val failMethodResult = - MethodResult( - explicitThrown( - StringIndexOutOfBoundsException(), - findNewAddr(), - environment.state.isInNestedMethod() - ), - hardConstraints = mkNot(inBoundsCondition).asHardConstraint() - ) - - val valueExpr = selectArrayExpressionFromMemory(getValueArray(wrapper.addr)) - - val returnResult = MethodResult( - valueExpr.select(index.expr).toCharValue(), - hardConstraints = inBoundsCondition.asHardConstraint() - ) - return listOf(returnResult, failMethodResult) + symbolicCharAtMethodImpl(wrapper, parameters) + } + splitWithLimitMethodSignature -> { + null + } + splitMethodSignature -> { + null + } + else -> { + null } - else -> return null } } @@ -186,101 +125,79 @@ class StringWrapper : BaseOverriddenWrapper(utStringClass.name) { ) return UtAssembleModel(addr, classId, modelName, instantiationCall) } -} - -internal val utNativeStringClass = Scene.v().getSootClass(UtNativeString::class.qualifiedName) - -private var stringNameIndex = 0 -private fun nextStringName() = "\$string${stringNameIndex++}" -class UtNativeStringWrapper : WrapperInterface { - private val valueDescriptor = NATIVE_STRING_VALUE_DESCRIPTOR - override fun Traverser.invoke( + private fun Traverser.symbolicMatchesMethodImpl( wrapper: ObjectValue, - method: SootMethod, parameters: List - ): List = - when (method.subSignature) { - "void ()" -> { - val newString = mkString(nextStringName()) - - val memoryUpdate = MemoryUpdate( - stores = persistentListOf(simplifiedNamedStore(valueDescriptor, wrapper.addr, newString)), - touchedChunkDescriptors = persistentSetOf(valueDescriptor) - ) - listOf( - MethodResult( - SymbolicSuccess(voidValue), - memoryUpdates = memoryUpdate - ) - ) - } - "void (int)" -> { - val newString = UtConvertToString((parameters[0] as PrimitiveValue).expr) - val memoryUpdate = MemoryUpdate( - stores = persistentListOf(simplifiedNamedStore(valueDescriptor, wrapper.addr, newString)), - touchedChunkDescriptors = persistentSetOf(valueDescriptor) - ) - listOf( - MethodResult( - SymbolicSuccess(voidValue), - memoryUpdates = memoryUpdate - ) - ) - } - "void (long)" -> { - val newString = UtConvertToString((parameters[0] as PrimitiveValue).expr) - val memoryUpdate = MemoryUpdate( - stores = persistentListOf(simplifiedNamedStore(valueDescriptor, wrapper.addr, newString)), - touchedChunkDescriptors = persistentSetOf(valueDescriptor) - ) - listOf( - MethodResult( - SymbolicSuccess(voidValue), - memoryUpdates = memoryUpdate - ) - ) - } - "int length()" -> { - val result = UtStringLength(memory.nativeStringValue(wrapper.addr)) - listOf(MethodResult(SymbolicSuccess(result.toByteValue().cast(IntType.v())))) - } - "char charAt(int)" -> { - val index = (parameters[0] as PrimitiveValue).expr - val result = UtStringCharAt(memory.nativeStringValue(wrapper.addr), index) - listOf(MethodResult(SymbolicSuccess(result.toCharValue()))) - } - "int codePointAt(int)" -> { - val index = (parameters[0] as PrimitiveValue).expr - val result = UtStringCharAt(memory.nativeStringValue(wrapper.addr), index) - listOf(MethodResult(SymbolicSuccess(result.toCharValue().cast(IntType.v())))) - } - "int toInteger()" -> { - val result = UtStringToInt(memory.nativeStringValue(wrapper.addr), UtIntSort) - listOf(MethodResult(SymbolicSuccess(result.toIntValue()))) - } - "long toLong()" -> { - val result = UtStringToInt(memory.nativeStringValue(wrapper.addr), UtLongSort) - listOf(MethodResult(SymbolicSuccess(result.toLongValue()))) - } - "char[] toCharArray(int)" -> { - val stringExpression = memory.nativeStringValue(wrapper.addr) - val result = UtStringToArray(stringExpression, parameters[0] as PrimitiveValue) - val length = UtStringLength(stringExpression) - val type = CharType.v() - val arrayType = type.arrayType - val arrayValue = createNewArray(length.toIntValue(), arrayType, type) - listOf( - MethodResult( - SymbolicSuccess(arrayValue), - memoryUpdates = arrayUpdateWithValue(arrayValue.addr, arrayType, result) - ) - ) - } - else -> unreachableBranch("Unknown signature at the NativeStringWrapper.invoke: ${method.signature}") + ): List? { + val arg = parameters[0] as ObjectValue + val matchingLengthExpr = getIntFieldValue(arg, STRING_LENGTH).accept(RewritingVisitor()) + + if (!matchingLengthExpr.isConcrete) return null + + val matchingValueExpr = + selectArrayExpressionFromMemory(getValueArray(arg.addr)).accept(RewritingVisitor()) + val matchingLength = matchingLengthExpr.toConcrete() as Int + val matchingValue = CharArray(matchingLength) + + for (i in 0 until matchingLength) { + val charExpr = matchingValueExpr.select(mkInt(i)).accept(RewritingVisitor()) + + if (!charExpr.isConcrete) return null + + matchingValue[i] = (charExpr.toConcrete() as Number).toChar() } - override fun value(resolver: Resolver, wrapper: ObjectValue): UtModel = UtNullModel(STRING_TYPE.classId) + val rgxGen = RgxGen(String(matchingValue)) + val matching = (rgxGen.generate()) + val notMatching = rgxGen.generateNotMatching() + + val thisLength = getIntFieldValue(wrapper, STRING_LENGTH) + val thisValue = selectArrayExpressionFromMemory(getValueArray(wrapper.addr)) + + val matchingConstraints = mutableSetOf() + matchingConstraints += mkEq(thisLength, mkInt(matching.length)) + for (i in matching.indices) { + matchingConstraints += mkEq(thisValue.select(mkInt(i)), mkChar(matching[i])) + } + + val notMatchingConstraints = mutableSetOf() + notMatchingConstraints += mkEq(thisLength, mkInt(notMatching.length)) + for (i in notMatching.indices) { + notMatchingConstraints += mkEq(thisValue.select(mkInt(i)), mkChar(notMatching[i])) + } + + return listOf( + MethodResult(UtTrue.toBoolValue(), matchingConstraints.asHardConstraint()), + MethodResult(UtFalse.toBoolValue(), notMatchingConstraints.asHardConstraint()) + ) + } + + private fun Traverser.symbolicCharAtMethodImpl( + wrapper: ObjectValue, + parameters: List + ): List { + val index = parameters[0] as PrimitiveValue + val lengthExpr = getIntFieldValue(wrapper, STRING_LENGTH) + val inBoundsCondition = mkAnd(Le(0.toPrimitiveValue(), index), Lt(index, lengthExpr.toIntValue())) + val failMethodResult = + MethodResult( + explicitThrown( + StringIndexOutOfBoundsException(), + findNewAddr(), + environment.state.isInNestedMethod() + ), + hardConstraints = mkNot(inBoundsCondition).asHardConstraint() + ) + + val valueExpr = selectArrayExpressionFromMemory(getValueArray(wrapper.addr)) + + val returnResult = MethodResult( + valueExpr.select(index.expr).toCharValue(), + hardConstraints = inBoundsCondition.asHardConstraint() + ) + return listOf(returnResult, failMethodResult) + } } sealed class UtAbstractStringBuilderWrapper(className: String) : BaseOverriddenWrapper(className) { diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/ExtendedArrayExpressions.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/ExtendedArrayExpressions.kt index e905322647..637dc6fccd 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/ExtendedArrayExpressions.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/ExtendedArrayExpressions.kt @@ -12,7 +12,6 @@ data class UtArrayInsert( ) : UtExtendedArrayExpression(arrayExpression.sort as UtArraySort) { override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - override val hashCode = Objects.hash(arrayExpression, index, element) override fun hashCode(): Int = hashCode @@ -162,29 +161,6 @@ data class UtArrayRemoveRange( } } -data class UtStringToArray( - val stringExpression: UtExpression, - val offset: PrimitiveValue -) : UtExtendedArrayExpression(UtArraySort(UtIntSort, UtCharSort)) { - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override val hashCode = Objects.hash(stringExpression, offset) - - override fun hashCode(): Int = hashCode - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtStringToArray - - if (stringExpression != other.stringExpression) return false - if (offset != other.offset) return false - - return true - } -} - data class UtArrayApplyForAll( val arrayExpression: UtExpression, val constraint: (UtExpression, PrimitiveValue) -> UtBoolExpression diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt index 6911237cea..50f529876a 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt @@ -165,19 +165,6 @@ data class Query( } } - /** - * Mark that part of UtStringEq is equal to concrete part to substitute it in constraints added later. - * - * Eq expressions with both concrete parts are simplified in RewritingVisitor.visit(UtStringEq) - */ - private fun MutableMap.putEq(eqExpr: UtStringEq) { - when { - eqExpr.left.isConcrete -> this[eqExpr.right] = eqExpr.left - eqExpr.right.isConcrete -> this[eqExpr.left] = eqExpr.right - else -> this[eqExpr] = UtTrue - } - } - /** * @return * [this] if constraints are satisfied under this model. @@ -208,7 +195,6 @@ data class Query( for (expr in addedHard) { when (expr) { is UtEqExpression -> addedEqs.putEq(expr) - is UtStringEq -> addedEqs.putEq(expr) is UtBoolOpExpression -> when (expr.operator) { Eq -> addedEqs.putEq(expr) Lt -> if (expr.right.expr.isConcrete && expr.right.expr.isInteger()) { diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/RewritingVisitor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/RewritingVisitor.kt index 9453aa393e..a94f15e6fd 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/RewritingVisitor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/RewritingVisitor.kt @@ -953,167 +953,6 @@ open class RewritingVisitor( override fun visit(expr: UtMkTermArrayExpression): UtExpression = applySimplification(expr, false) - override fun visit(expr: UtStringConst): UtExpression = expr - - // CONFLUENCE:UtBot+Expression+Optimizations#UtBotExpressionOptimizations-sConcat - // UtConcat("A_1", "A_2", ..., "A_n") ---> "A_1A_2...A_n" - override fun visit(expr: UtConcatExpression): UtExpression = - applySimplification(expr) { - val parts = expr.parts.map { it.accept(this) as UtStringExpression } - if (parts.all { it.isConcrete }) { - UtSeqLiteral(parts.joinToString { it.toConcrete() as String }) - } else { - UtConcatExpression(parts) - } - } - - override fun visit(expr: UtConvertToString): UtExpression = - applySimplification(expr) { UtConvertToString(expr.expression.accept(this)) } - - override fun visit(expr: UtStringToInt): UtExpression = - applySimplification(expr) { UtStringToInt(expr.expression.accept(this), expr.sort) } - - // CONFLUENCE:UtBot+Expression+Optimizations#UtBotExpressionOptimizations-sLength - // UtLength "A" ---> "A".length - override fun visit(expr: UtStringLength): UtExpression = - applySimplification(expr) { - val string = expr.string.accept(this) - when { - string is UtArrayToString -> string.length.expr - string.isConcrete -> mkInt((string.toConcrete() as String).length) - else -> UtStringLength(string) - } - } - - // CONFLUENCE:UtBot+Expression+Optimizations#UtBotExpressionOptimizations-sPositiveLength - // UtPositiveLength "A" ---> UtTrue - override fun visit(expr: UtStringPositiveLength): UtExpression = - applySimplification(expr) { - val string = expr.string.accept(this) - if (string.isConcrete) UtTrue else UtStringPositiveLength(string) - } - - // CONFLUENCE:UtBot+Expression+Optimizations#UtBotExpressionOptimizations-sCharAt - // UtCharAt "A" (Integral i) ---> "A".charAt(i) - override fun visit(expr: UtStringCharAt): UtExpression = - applySimplification(expr) { - val index = expr.index.accept(this) - val string = withNewSelect(index) { expr.string.accept(this) } - if (allConcrete(string, index)) { - (string.toConcrete() as String)[index.toConcrete() as Int].primitiveToSymbolic().expr - } else { - UtStringCharAt(string, index) - } - } - - override fun visit(expr: UtStringEq): UtExpression = - applySimplification(expr) { - val left = expr.left.accept(this) - val right = expr.right.accept(this) - when { - // CONFLUENCE:UtBot+Expression+Optimizations#UtBotExpressionOptimizations-eqConcrete - // Eq("A", "B") ---> "A" == "B" - allConcrete(left, right) -> mkBool(left.toConcrete() == right.toConcrete()) - // CONFLUENCE:UtBot+Expression+Optimizations#UtBotExpressionOptimizations-eqEqual - // Eq(a, a) ---> true - left == right -> UtTrue - else -> UtStringEq(left, right) - } - } - - // CONFLUENCE:UtBot+Expression+Optimizations#UtBotExpressionOptimizations-sSubstring - // UtSubstring "A" (Integral begin) (Integral end) ---> "A".substring(begin, end) - override fun visit(expr: UtSubstringExpression): UtExpression = - applySimplification(expr) { - val string = expr.string.accept(this) - val beginIndex = expr.beginIndex.accept(this) - val length = expr.length.accept(this) - if (allConcrete(string, beginIndex, length)) { - val begin = beginIndex.toConcrete() as Int - val end = begin + length.toConcrete() as Int - UtSeqLiteral((string.toConcrete() as String).substring(begin, end)) - } else { - UtSubstringExpression(string, beginIndex, length) - } - } - - override fun visit(expr: UtReplaceExpression): UtExpression = applySimplification(expr, false) - - // CONFLUENCE:UtBot+Expression+Optimizations#UtBotExpressionOptimizations-sStartsWith - // UtStartsWith "A" "P" ---> "A".startsWith("P") - override fun visit(expr: UtStartsWithExpression): UtExpression = - applySimplification(expr) { - val string = expr.string.accept(this) - val prefix = expr.prefix.accept(this) - if (allConcrete(string, prefix)) { - val concreteString = string.toConcrete() as String - val concretePrefix = prefix.toConcrete() as String - mkBool(concreteString.startsWith(concretePrefix)) - } else { - UtStartsWithExpression(string, prefix) - } - } - - // CONFLUENCE:UtBot+Expression+Optimizations#UtBotExpressionOptimizations-sEndsWith - // UtEndsWith "A" "S" ---> "A".endsWith("S") - override fun visit(expr: UtEndsWithExpression): UtExpression = - applySimplification(expr) { - val string = expr.string.accept(this) - val suffix = expr.suffix.accept(this) - if (allConcrete(string, suffix)) { - val concreteString = string.toConcrete() as String - val concreteSuffix = suffix.toConcrete() as String - mkBool(concreteString.endsWith(concreteSuffix)) - } else { - UtEndsWithExpression(string, suffix) - } - } - - // CONFLUENCE:UtBot+Expression+Optimizations#UtBotExpressionOptimizations-sIndexOf - // UtIndexOf "A" "S" ---> "A".indexOf("S") - override fun visit(expr: UtIndexOfExpression): UtExpression = applySimplification(expr) { - val string = expr.string.accept(this) - val substring = expr.substring.accept(this) - if (allConcrete(string, substring)) { - val concreteString = string.toConcrete() as String - val concreteSubstring = substring.toConcrete() as String - mkInt(concreteString.indexOf(concreteSubstring)) - } else { - UtIndexOfExpression(string, substring) - } - } - - // CONFLUENCE:UtBot+Expression+Optimizations#UtBotExpressionOptimizations-sContains - // UtContains "A" "S" ---> "A".contains("S") - override fun visit(expr: UtContainsExpression): UtExpression = - applySimplification(expr) { - val string = expr.string.accept(this) - val substring = expr.substring.accept(this) - if (allConcrete(string, substring)) { - val concreteString = string.toConcrete() as String - val concreteSubstring = substring.toConcrete() as String - mkBool(concreteString.contains(concreteSubstring)) - } else { - UtContainsExpression(string, substring) - } - } - - override fun visit(expr: UtToStringExpression): UtExpression = - applySimplification(expr) { - UtToStringExpression(expr.isNull.accept(this) as UtBoolExpression, expr.notNullExpr.accept(this)) - } - - override fun visit(expr: UtArrayToString): UtExpression = - applySimplification(expr) { - UtArrayToString( - expr.arrayExpression.accept(this), - expr.offset.expr.accept(this).toIntValue(), - expr.length.expr.accept(this).toIntValue() - ) - } - - override fun visit(expr: UtSeqLiteral): UtExpression = expr - override fun visit(expr: UtConstArrayExpression): UtExpression = applySimplification(expr) { UtConstArrayExpression(expr.constValue.accept(this), expr.sort) @@ -1177,22 +1016,11 @@ open class RewritingVisitor( expr.constraint ) } - - override fun visit(expr: UtStringToArray): UtExpression = applySimplification(expr, false) { - UtStringToArray( - expr.stringExpression.accept(this), - expr.offset.expr.accept(this).toIntValue() - ) - } } - private val arrayExpressionAxiomInstantiationCache = IdentityHashMap() -private val stringExpressionAxiomInstantiationCache = - IdentityHashMap() - private val arrayExpressionAxiomIndex = AtomicInteger(0) private fun instantiateArrayAsNewConst(arrayExpression: UtExtendedArrayExpression) = @@ -1204,7 +1032,6 @@ private fun instantiateArrayAsNewConst(arrayExpression: UtExtendedArrayExpressio is UtArrayRemoveRange -> "RemoveRange" is UtArraySetRange -> "SetRange" is UtArrayShiftIndexes -> "ShiftIndexes" - is UtStringToArray -> "StringToArray" is UtArrayApplyForAll -> error("UtArrayApplyForAll cannot be instantiated as new const array") } UtMkArrayExpression( @@ -1213,15 +1040,6 @@ private fun instantiateArrayAsNewConst(arrayExpression: UtExtendedArrayExpressio ) } -private fun instantiateStringAsNewConst(stringExpression: UtStringExpression) = - stringExpressionAxiomInstantiationCache.getOrPut(stringExpression) { - val suffix = when (stringExpression) { - is UtArrayToString -> "ArrayToString" - else -> unreachableBranch("Cannot instantiate new string const for $stringExpression") - } - UtStringConst("_str$suffix${arrayExpressionAxiomIndex.getAndIncrement()}") - } - /** * Visitor that applies the same simplifications as [RewritingVisitor] and instantiate axioms for extended array theory. * @@ -1378,34 +1196,6 @@ class AxiomInstantiationRewritingVisitor( return arrayExpression } - override fun visit(expr: UtStringToArray): UtExpression { - val arrayInstance = instantiateArrayAsNewConst(expr) - val offset = expr.offset.expr.accept(this).toIntValue() - val selectedIndex = selectIndexStack.last() - val pushedIndex = Add(selectedIndex, offset) - val stringExpression = withNewSelect(pushedIndex) { expr.stringExpression.accept(this) } - - instantiatedAxiomExpressions += UtEqExpression( - UtStringCharAt(stringExpression, pushedIndex), - arrayInstance.select(selectedIndex.expr) - ) - return arrayInstance - } - - override fun visit(expr: UtArrayToString): UtExpression { - val stringInstance = instantiateStringAsNewConst(expr) - val offset = expr.offset.expr.accept(this).toIntValue() - val selectedIndex = selectIndexStack.last() - val pushedIndex = Add(selectedIndex, offset) - val arrayExpression = withNewSelect(pushedIndex) { expr.arrayExpression.accept(this) } - - instantiatedAxiomExpressions += UtEqExpression( - arrayExpression.select(pushedIndex), - UtStringCharAt(stringInstance, selectedIndex.expr) - ) - return stringInstance - } - val instantiatedArrayAxioms: List get() = instantiatedAxiomExpressions } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/StringExpressions.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/StringExpressions.kt deleted file mode 100644 index a06de568a3..0000000000 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/StringExpressions.kt +++ /dev/null @@ -1,422 +0,0 @@ -package org.utbot.engine.pc - -import org.utbot.common.WorkaroundReason.HACK -import org.utbot.common.workaround -import org.utbot.engine.PrimitiveValue -import java.util.Objects - -sealed class UtStringExpression : UtExpression(UtSeqSort) - -data class UtStringConst(val name: String) : UtStringExpression() { - - override val hashCode = Objects.hash(name) - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(String$sort $name)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtStringConst - - if (name != other.name) return false - - return true - } - - override fun hashCode() = hashCode -} - -data class UtConcatExpression(val parts: List) : UtStringExpression() { - override val hashCode = parts.hashCode() - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(str.concat ${parts.joinToString()})" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtConcatExpression - - if (parts != other.parts) return false - - return true - } - - override fun hashCode() = hashCode -} - -data class UtConvertToString(val expression: UtExpression) : UtStringExpression() { - init { - require(expression.sort is UtBvSort) - } - - override val hashCode = expression.hashCode() - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(str.tostr $expression)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtConvertToString - - if (expression != other.expression) return false - - return true - } - - override fun hashCode() = hashCode -} - -data class UtStringToInt(val expression: UtExpression, override val sort: UtBvSort) : UtBvExpression(sort) { - init { - require(expression.sort is UtSeqSort) - } - - override val hashCode = Objects.hash(expression, sort) - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(str.toint $expression)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtStringToInt - - if (expression != other.expression) return false - if (sort != other.sort) return false - - return true - } - - override fun hashCode() = hashCode -} - -data class UtStringLength(val string: UtExpression) : UtBvExpression(UtIntSort) { - override val hashCode = string.hashCode() - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(str.len $string)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtStringLength - - if (string != other.string) return false - - return true - } - - override fun hashCode() = hashCode -} - -/** - * Creates constraint to get rid of negative string length (z3 bug?) - */ -data class UtStringPositiveLength(val string: UtExpression) : UtBoolExpression() { - override val hashCode = string.hashCode() - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(positive.str.len $string)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtStringPositiveLength - - if (string != other.string) return false - - return true - } - - override fun hashCode() = hashCode -} - -data class UtStringCharAt( - val string: UtExpression, - val index: UtExpression -) : UtExpression(UtCharSort) { - override val hashCode = Objects.hash(string, index) - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(str.at $string $index)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtStringCharAt - - if (string != other.string) return false - if (index != other.index) return false - - return true - } - - override fun hashCode() = hashCode -} - -data class UtStringEq(val left: UtExpression, val right: UtExpression) : UtBoolExpression() { - override val hashCode = Objects.hash(left, right) - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(str.eq $left $right)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtStringEq - - if (left != other.left) return false - if (right != other.right) return false - - return true - } - - override fun hashCode() = hashCode -} - -data class UtSubstringExpression( - val string: UtExpression, - val beginIndex: UtExpression, - val length: UtExpression -) : UtStringExpression() { - override val hashCode = Objects.hash(string, beginIndex, length) - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(str.substr $string $beginIndex $length)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtSubstringExpression - - if (string != other.string) return false - if (beginIndex != other.beginIndex) return false - if (length != other.length) return false - - return true - } - - override fun hashCode() = hashCode -} - -data class UtReplaceExpression( - val string: UtExpression, - val regex: UtExpression, - val replacement: UtExpression -) : UtStringExpression() { - override val hashCode = Objects.hash(string, regex, replacement) - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(str.replace $string $regex $replacement)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtReplaceExpression - - if (string != other.string) return false - if (regex != other.regex) return false - if (replacement != other.replacement) return false - - return true - } - - override fun hashCode() = hashCode -} - -data class UtStartsWithExpression( - val string: UtExpression, - val prefix: UtExpression -) : UtBoolExpression() { - override val hashCode = Objects.hash(string, prefix) - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(str.prefixof $string $prefix)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtStartsWithExpression - - if (string != other.string) return false - if (prefix != other.prefix) return false - - return true - } - - override fun hashCode() = hashCode -} - -data class UtEndsWithExpression( - val string: UtExpression, - val suffix: UtExpression -) : UtBoolExpression() { - override val hashCode = Objects.hash(string, suffix) - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(str.suffixof $string $suffix)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtEndsWithExpression - - if (string != other.string) return false - if (suffix != other.suffix) return false - - return true - } - - override fun hashCode() = hashCode -} - -data class UtIndexOfExpression( - val string: UtExpression, - val substring: UtExpression -) : UtBoolExpression() { - override val hashCode = Objects.hash(string, substring) - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(str.indexof $string $substring)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtIndexOfExpression - - if (string != other.string) return false - if (substring != other.substring) return false - - return true - } - - override fun hashCode() = hashCode - -} - -data class UtContainsExpression( - val string: UtExpression, - val substring: UtExpression -) : UtBoolExpression() { - override val hashCode = Objects.hash(string, substring) - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(str.contains $string $substring)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtContainsExpression - - if (string != other.string) return false - if (substring != other.substring) return false - - return true - } - - override fun hashCode() = hashCode -} - -data class UtToStringExpression( - val isNull: UtBoolExpression, - val notNullExpr: UtExpression -) : UtStringExpression() { - override val hashCode = Objects.hash(isNull, notNullExpr) - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(ite $isNull 'null' $notNullExpr)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtToStringExpression - - if (isNull != other.isNull) return false - if (notNullExpr != other.notNullExpr) return false - - return true - } - - override fun hashCode() = hashCode -} - -data class UtArrayToString( - val arrayExpression: UtExpression, - val offset: PrimitiveValue, - val length: PrimitiveValue -) : UtStringExpression() { - override val hashCode = Objects.hash(arrayExpression, offset) - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = "(str.array_to_str $arrayExpression, offset = $offset)" - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtArrayToString - - if (arrayExpression == other.arrayExpression) return false - if (offset == other.offset) return false - - return true - } - - override fun hashCode() = hashCode -} - -// String literal (not a String Java object!) -data class UtSeqLiteral(val value: String) : UtExpression(UtSeqSort) { - override val hashCode = value.hashCode() - - override fun accept(visitor: UtExpressionVisitor): TResult = visitor.visit(this) - - override fun toString() = value - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UtSeqLiteral - - if (value != other.value) return false - - return true - } - - override fun hashCode() = hashCode -} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpression.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpression.kt index 94e3944172..8a1da26d78 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpression.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpression.kt @@ -27,7 +27,6 @@ val UtExpression.isConcrete: Boolean get() = when (this) { is UtBvLiteral -> true is UtFpLiteral -> true - is UtSeqLiteral -> true is UtBoolLiteral -> true is UtAddrExpression -> internal.isConcrete else -> false @@ -36,7 +35,6 @@ val UtExpression.isConcrete: Boolean fun UtExpression.toConcrete(): Any = when (this) { is UtBvLiteral -> this.value is UtFpLiteral -> this.value - is UtSeqLiteral -> this.value UtTrue -> true UtFalse -> false is UtAddrExpression -> internal.toConcrete() diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpressionVisitor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpressionVisitor.kt index 760633ff37..a5465a0c5f 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpressionVisitor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpressionVisitor.kt @@ -29,25 +29,6 @@ interface UtExpressionVisitor { fun visit(expr: UtIteExpression): TResult fun visit(expr: UtMkTermArrayExpression): TResult - // UtString expressions - fun visit(expr: UtStringConst): TResult - fun visit(expr: UtConcatExpression): TResult - fun visit(expr: UtConvertToString): TResult - fun visit(expr: UtStringToInt): TResult - fun visit(expr: UtStringLength): TResult - fun visit(expr: UtStringPositiveLength): TResult - fun visit(expr: UtStringCharAt): TResult - fun visit(expr: UtStringEq): TResult - fun visit(expr: UtSubstringExpression): TResult - fun visit(expr: UtReplaceExpression): TResult - fun visit(expr: UtStartsWithExpression): TResult - fun visit(expr: UtEndsWithExpression): TResult - fun visit(expr: UtIndexOfExpression): TResult - fun visit(expr: UtContainsExpression): TResult - fun visit(expr: UtToStringExpression): TResult - fun visit(expr: UtSeqLiteral): TResult - fun visit(expr: UtArrayToString): TResult - // UtArray expressions from extended array theory fun visit(expr: UtArrayInsert): TResult fun visit(expr: UtArrayInsertRange): TResult @@ -56,7 +37,6 @@ interface UtExpressionVisitor { fun visit(expr: UtArraySetRange): TResult fun visit(expr: UtArrayShiftIndexes): TResult fun visit(expr: UtArrayApplyForAll): TResult - fun visit(expr: UtStringToArray): TResult // Add and Sub with overflow detection fun visit(expr: UtAddNoOverflowExpression): TResult diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt index 57184aed87..8721b5eb18 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt @@ -97,8 +97,6 @@ fun UtExpression.select(outerIndex: UtExpression, nestedIndex: UtExpression) = fun UtExpression.store(index: UtExpression, elem: UtExpression) = UtArrayMultiStoreExpression(this, index, elem) -fun mkString(value: String): UtStringConst = UtStringConst(value) - fun PrimitiveValue.align(): PrimitiveValue = when (type) { is ByteType, is ShortType, is CharType -> UtCastExpression(this, IntType.v()).toIntValue() else -> this diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3EvaluatorVisitor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3EvaluatorVisitor.kt index 1f0e886fd8..ec09cde2cd 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3EvaluatorVisitor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3EvaluatorVisitor.kt @@ -168,12 +168,6 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra eval(arrayExpression.select(mkInt(lastIndex - offset))) } - override fun visit(expr: UtStringToArray): Expr = expr.run { - val lastIndex = selectIndexStack.last().intValue() - val offset = eval(offset.expr).intValue() - eval(UtStringCharAt(stringExpression, mkInt(lastIndex + offset))) - } - override fun visit(expr: UtAddrExpression): Expr = eval(expr.internal) override fun visit(expr: UtOpExpression): Expr = expr.run { @@ -244,99 +238,6 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra if (eval(condition).value() as Boolean) eval(thenExpr) else eval(elseExpr) } - override fun visit(expr: UtConcatExpression): Expr = expr.run { - translator.withContext { mkConcat(*parts.map { eval(it) as SeqExpr }.toTypedArray()) } - } - - override fun visit(expr: UtStringLength): Expr = expr.run { - translator.withContext { - if (string is UtArrayToString) { - eval(string.length.expr) - } else { - mkInt2BV(MAX_STRING_LENGTH_SIZE_BITS, mkLength(eval(string) as SeqExpr)) - } - } - } - - override fun visit(expr: UtStringPositiveLength): Expr = expr.run { - translator.withContext { - mkGe(mkLength(eval(string) as SeqExpr), mkInt(0)) - } - } - - override fun visit(expr: UtStringCharAt): Expr = expr.run { - translator.withContext { - val charAtExpr = mkSeqNth(eval(string) as SeqExpr, mkBV2Int(eval(index) as BitVecExpr, true)) - val z3var = charAtExpr.z3Variable(ByteType.v()) - convertVar(z3var, CharType.v()).expr - } - } - - override fun visit(expr: UtStringEq): Expr = expr.run { - translator.withContext { - mkEq(eval(left), eval(right)) - } - } - - override fun visit(expr: UtSubstringExpression): Expr = expr.run { - translator.withContext { - mkExtract( - eval(string) as SeqExpr, - mkBV2Int(eval(beginIndex) as BitVecExpr, true), - mkBV2Int(eval(length) as BitVecExpr, true) - ) - } - } - - override fun visit(expr: UtReplaceExpression): Expr = expr.run { - workaround(WorkaroundReason.HACK) { // mkReplace replaces first occasion only - translator.withContext { - mkReplace( - eval(string) as SeqExpr, - eval(regex) as SeqExpr, - eval(replacement) as SeqExpr - ) - } - } - } - - // Attention, prefix is a first argument! - override fun visit(expr: UtStartsWithExpression): Expr = expr.run { - translator.withContext { - mkPrefixOf(eval(prefix) as SeqExpr, eval(string) as SeqExpr) - } - } - - // Attention, suffix is a first argument! - override fun visit(expr: UtEndsWithExpression): Expr = expr.run { - translator.withContext { - mkSuffixOf(eval(suffix) as SeqExpr, eval(string) as SeqExpr) - } - } - - override fun visit(expr: UtIndexOfExpression): Expr = expr.run { - val string = eval(string) as SeqExpr - val substring = eval(substring) as SeqExpr - translator.withContext { - mkInt2BV( - MAX_STRING_LENGTH_SIZE_BITS, - mkIndexOf(string, substring, mkInt(0)) - ) - } - } - - override fun visit(expr: UtContainsExpression): Expr = expr.run { - val substring = eval(substring) as SeqExpr - val string = eval(string) as SeqExpr - translator.withContext { - mkGe(mkIndexOf(string, substring, mkInt(0)), mkInt(0)) - } - } - - override fun visit(expr: UtToStringExpression): Expr = expr.run { - if (eval(isNull).value() as Boolean) translator.withContext { mkString("null") } else eval(notNullExpr) - } - override fun visit(expr: UtArrayApplyForAll): Expr = expr.run { eval(expr.arrayExpression.select(mkInt(selectIndexStack.last().intValue()))) } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt index 4f0d7516d4..68a3be82fc 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt @@ -305,34 +305,6 @@ open class Z3TranslatorVisitor( } } - override fun visit(expr: UtStringConst): Expr = expr.run { z3Context.mkConst(name, sort.toZ3Sort(z3Context)) } - - override fun visit(expr: UtConcatExpression): Expr = - expr.run { z3Context.mkConcat(*parts.map { translate(it) as SeqExpr }.toTypedArray()) } - - override fun visit(expr: UtConvertToString): Expr = expr.run { - when (expression) { - is UtBvLiteral -> z3Context.mkString(expression.value.toString()) - else -> { - val intValue = z3Context.mkBV2Int(translate(expression) as BitVecExpr, true) - z3Context.intToString(intValue) - } - } - } - - override fun visit(expr: UtStringToInt): Expr = expr.run { - val intValue = z3Context.stringToInt(translate(expression)) - z3Context.mkInt2BV(size, intValue) - } - - override fun visit(expr: UtStringLength): Expr = expr.run { - z3Context.mkInt2BV(MAX_STRING_LENGTH_SIZE_BITS, z3Context.mkLength(translate(string) as SeqExpr)) - } - - override fun visit(expr: UtStringPositiveLength): Expr = expr.run { - z3Context.mkGe(z3Context.mkLength(translate(string) as SeqExpr), z3Context.mkInt(0)) - } - private fun Context.mkBV2Int(expr: UtExpression): IntExpr = if (expr is UtBvLiteral) { mkInt(expr.value as Long) @@ -340,64 +312,6 @@ open class Z3TranslatorVisitor( mkBV2Int(translate(expr) as BitVecExpr, true) } - - override fun visit(expr: UtStringCharAt): Expr = expr.run { - val charAtExpr = z3Context.mkSeqNth(translate(string) as SeqExpr, z3Context.mkBV2Int(index)) - val z3var = charAtExpr.z3Variable(ByteType.v()) - z3Context.convertVar(z3var, CharType.v()).expr - } - - override fun visit(expr: UtStringEq): Expr = expr.run { z3Context.mkEq(translate(left), translate(right)) } - - override fun visit(expr: UtSubstringExpression): Expr = expr.run { - z3Context.mkExtract( - translate(string) as SeqExpr, - z3Context.mkBV2Int(beginIndex), - z3Context.mkBV2Int(length) - ) - } - - override fun visit(expr: UtReplaceExpression): Expr = expr.run { - workaround(WorkaroundReason.HACK) { // mkReplace replaces first occasion only - z3Context.mkReplace( - translate(string) as SeqExpr, - translate(regex) as SeqExpr, - translate(replacement) as SeqExpr - ) - } - } - - // Attention, prefix is a first argument! - override fun visit(expr: UtStartsWithExpression): Expr = expr.run { - z3Context.mkPrefixOf(translate(prefix) as SeqExpr, translate(string) as SeqExpr) - } - - // Attention, suffix is a first argument! - override fun visit(expr: UtEndsWithExpression): Expr = expr.run { - z3Context.mkSuffixOf(translate(suffix) as SeqExpr, translate(string) as SeqExpr) - } - - override fun visit(expr: UtIndexOfExpression): Expr = expr.run { - z3Context.mkInt2BV( - MAX_STRING_LENGTH_SIZE_BITS, - z3Context.mkIndexOf(translate(string) as SeqExpr, translate(substring) as SeqExpr, z3Context.mkInt(0)) - ) - } - - override fun visit(expr: UtContainsExpression): Expr = expr.run { - z3Context.mkGe( - z3Context.mkIndexOf(translate(string) as SeqExpr, translate(substring) as SeqExpr, z3Context.mkInt(0)), - z3Context.mkInt(0) - ) - } - - override fun visit(expr: UtToStringExpression): Expr = expr.run { - z3Context.mkITE(translate(isNull) as BoolExpr, z3Context.mkString("null"), translate(notNullExpr)) - - } - - override fun visit(expr: UtSeqLiteral): Expr = expr.run { z3Context.mkString(value) } - companion object { const val MAX_TYPE_NUMBER_FOR_ENUMERATION = 64 } @@ -416,7 +330,5 @@ open class Z3TranslatorVisitor( override fun visit(expr: UtArrayApplyForAll): Expr = error("translate of UtArrayApplyForAll expression") - override fun visit(expr: UtStringToArray): Expr = error("translate of UtStringToArray expression") - override fun visit(expr: UtArrayToString): Expr = error("translate of UtArrayToString expression") } \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/util/SootUtils.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/util/SootUtils.kt index db738b1b7c..214400aa19 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/framework/util/SootUtils.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/util/SootUtils.kt @@ -2,7 +2,6 @@ package org.utbot.framework.util import org.utbot.api.mock.UtMock import org.utbot.common.FileUtil -import org.utbot.engine.UtNativeStringWrapper import org.utbot.engine.jimpleBody import org.utbot.engine.overrides.Boolean import org.utbot.engine.overrides.Byte @@ -189,7 +188,6 @@ private val classesToLoad = arrayOf( UtGenericStorage::class, UtGenericAssociative::class, PrintStream::class, - UtNativeStringWrapper::class, UtString::class, UtStringBuilder::class, UtStringBuffer::class, diff --git a/utbot-sample/src/main/java/org/utbot/examples/strings/GenericExamples.java b/utbot-sample/src/main/java/org/utbot/examples/strings/GenericExamples.java new file mode 100644 index 0000000000..55f0be4196 --- /dev/null +++ b/utbot-sample/src/main/java/org/utbot/examples/strings/GenericExamples.java @@ -0,0 +1,11 @@ +package org.utbot.examples.strings; + +public class GenericExamples { + public boolean containsOk(T obj) { + return obj.toString().contains("ok"); + } + + public boolean containsOkExample() { + return new GenericExamples().containsOk("Elders have spoken"); + } +} diff --git a/utbot-sample/src/main/java/org/utbot/examples/strings/StringExamples.java b/utbot-sample/src/main/java/org/utbot/examples/strings/StringExamples.java index 73c624ae92..18528e5d98 100644 --- a/utbot-sample/src/main/java/org/utbot/examples/strings/StringExamples.java +++ b/utbot-sample/src/main/java/org/utbot/examples/strings/StringExamples.java @@ -1,5 +1,7 @@ package org.utbot.examples.strings; +import org.jetbrains.annotations.NotNull; + import java.util.Arrays; import static java.lang.Boolean.valueOf; @@ -175,6 +177,16 @@ public String nullableStringBuffer(StringBuffer buffer, int i) { return buffer.toString(); } + @SuppressWarnings("RedundantIfStatement") + public boolean isStringBuilderEmpty(@NotNull StringBuilder stringBuilder) { + String content = stringBuilder.toString(); + if (content.length() == 0) { + return true; + } + + return false; + } + public boolean isValidUuid(String uuid) { return isNotBlank(uuid) && uuid .matches("[0-9a-f]{8}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{12}");