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..f08a69c94a --- /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, + pipelines = listOf( + TestLastStage(CodegenLanguage.JAVA), + TestLastStage(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 7ff61edaad..0b9e8500f2 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,32 @@ 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 + fun testByteToStringWithConstants() { + val values: Array = arrayOf( + Byte.MIN_VALUE, + (Byte.MIN_VALUE + 100).toByte(), + 0.toByte(), + (Byte.MAX_VALUE - 100).toByte(), + Byte.MAX_VALUE + ) + + val expected = values.map { it.toString() } + + check( + StringExamples::byteToStringWithConstants, + eq(1), + { r -> r != null && r.indices.all { r[it] == expected[it] } } + ) } @Test @@ -53,45 +68,91 @@ 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 testShortToStringWithConstants() { + val values: Array = arrayOf( + Short.MIN_VALUE, + (Short.MIN_VALUE + 100).toShort(), + 0.toShort(), + (Short.MAX_VALUE - 100).toShort(), + Short.MAX_VALUE + ) + + val expected = values.map { it.toString() } + + check( + StringExamples::shortToStringWithConstants, + eq(1), + { r -> r != null && r.indices.all { r[it] == expected[it] } } + ) + } @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 testIntToStringWithConstants() { + val values: Array = arrayOf( + Integer.MIN_VALUE, + Integer.MIN_VALUE + 100, + 0, + Integer.MAX_VALUE - 100, + Integer.MAX_VALUE + ) + + val expected = values.map { it.toString() } + + check( + StringExamples::intToStringWithConstants, + eq(1), + { r -> r != null && r.indices.all { r[it] == expected[it] } } + ) + } @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 + fun testLongToStringWithConstants() { + val values: Array = arrayOf( + Long.MIN_VALUE, + Long.MIN_VALUE + 100L, + 0L, + Long.MAX_VALUE - 100L, + Long.MAX_VALUE + ) + + val expected = values.map { it.toString() } + + check( + StringExamples::longToStringWithConstants, + eq(1), + { r -> r != null && r.indices.all { r[it] == expected[it] } } + ) + } + @Test fun testStartsWithLiteral() { check( @@ -250,6 +311,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() { @@ -332,7 +402,7 @@ internal class StringExamplesTest : UtValueTestCaseChecker( fun testSubstring() { checkWithException( StringExamples::substring, - between(5..7), + between(5..8), { s, _, r -> s == null && r.isException() }, { s, i, r -> s != null && i < 0 || i > s.length && r.isException() }, { s, i, r -> s != null && i in 0..s.length && r.getOrThrow() == s.substring(i) && s.substring(i) != "password" }, @@ -585,13 +655,14 @@ 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" }, ) } } + // TODO: This test fails without concrete execution as it uses a symbolic variable @Test fun testListToString() { check( 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..717e2c4f2b 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; @@ -48,17 +48,39 @@ public static byte parseByte(String s, int radix) { @SuppressWarnings("ConstantConditions") public static String toString(byte b) { - // condition = b < 0 - boolean condition = less(b, (byte) 0); + if (b == -128) { + return "-128"; + } + + if (b == 0) { + return "0"; + } + // assumes are placed here to limit search space of solver // 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(); + assume(b <= 127); + assume(b > -128); + assume(b != 0); + + // isNegative = b < 0 + boolean isNegative = less(b, (byte) 0); + String prefix = ite(isNegative, "-", ""); + + int value = ite(isNegative, (byte) -b, b); + char[] reversed = new char[3]; + int offset = 0; + while (value > 0) { + reversed[offset] = (char) ('0' + (value % 10)); + value /= 10; + offset++; + } + + char[] buffer = new char[offset]; + int counter = 0; + while (offset > 0) { + offset--; + buffer[counter++] = reversed[offset]; + } + return prefix + new String(buffer); } } 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..34d936364c 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,10 +1,9 @@ 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.assume; import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely; import static org.utbot.engine.overrides.UtLogicMock.ite; import static org.utbot.engine.overrides.UtLogicMock.less; @@ -71,21 +70,35 @@ public static int parseUnsignedInt(String s, int radix) { } } + @SuppressWarnings("ConstantConditions") public static String toString(int i) { - if (i == 0x80000000) { // java.lang.MIN_VALUE + if (i == 0x80000000) { // java.lang.Integer.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(); + + if (i == 0) { + return "0"; + } + + // isNegative = i < 0 + boolean isNegative = less(i, 0); + String prefix = ite(isNegative, "-", ""); + + int value = ite(isNegative, -i, i); + char[] reversed = new char[10]; + int offset = 0; + while (value > 0) { + reversed[offset] = (char) ('0' + (value % 10)); + value /= 10; + offset++; + } + + char[] buffer = new char[offset]; + int counter = 0; + while (offset > 0) { + offset--; + buffer[counter++] = reversed[offset]; + } + return prefix + new String(buffer); } } 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..2128115279 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,10 +1,9 @@ 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.assume; import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely; import static org.utbot.engine.overrides.UtLogicMock.ite; import static org.utbot.engine.overrides.UtLogicMock.less; @@ -71,21 +70,35 @@ public static long parseUnsignedLong(String s, int radix) { } } + @SuppressWarnings("ConstantConditions") 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(); + + if (l == 0) { + return "0"; + } + + // isNegative = i < 0 + boolean isNegative = less(l, 0); + String prefix = ite(isNegative, "-", ""); + + long value = ite(isNegative, -l, l); + char[] reversed = new char[19]; + int offset = 0; + while (value > 0) { + reversed[offset] = (char) ('0' + (value % 10)); + value /= 10; + offset++; + } + + char[] buffer = new char[offset]; + int counter = 0; + while (offset > 0) { + offset--; + buffer[counter++] = reversed[offset]; + } + return prefix + new String(buffer); } } 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..d64533bb78 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,10 +1,9 @@ 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.assume; import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely; import static org.utbot.engine.overrides.UtLogicMock.ite; import static org.utbot.engine.overrides.UtLogicMock.less; @@ -45,18 +44,41 @@ public static java.lang.Short parseShort(String s, int radix) { } } + @SuppressWarnings("ConstantConditions") public static String toString(short s) { - // condition = s < 0 - boolean condition = less(s, (short) 0); + if (s == -32768) { + return "-32768"; + } + + if (s == 0) { + return "0"; + } + // assumes are placed here to limit search space of solver // 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(); + assume(s <= 32767); + assume(s > -32768); + assume(s != 0); + + // isNegative = s < 0 + boolean isNegative = less(s, (short) 0); + String prefix = ite(isNegative, "-", ""); + + int value = ite(isNegative, (short) -s, s); + char[] reversed = new char[5]; + int offset = 0; + while (value > 0) { + reversed[offset] = (char) ('0' + (value % 10)); + value /= 10; + offset++; + } + + char[] buffer = new char[offset]; + int counter = 0; + while (offset > 0) { + offset--; + buffer[counter++] = reversed[offset]; + } + return prefix + new String(buffer); } } 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..1cd5024061 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]; @@ -774,7 +756,7 @@ public String concat(String str) { } char[] newValue = new char[length + str.length()]; UtArrayMock.arraycopy(value, 0, newValue, 0, length); - UtArrayMock.arraycopy(otherVal, 0, newValue, length + 1, str.length()); + UtArrayMock.arraycopy(otherVal, 0, newValue, length, str.length()); return new String(newValue); } @@ -866,47 +848,20 @@ public String replace(CharSequence target, CharSequence replacement) { return toString().replace(target, replacement); } + private String[] splitWithLimitImpl(String regex, int limit) { + return toString().split(regex, limit); + } + public String[] split(String regex, int limit) { - preconditionCheck(); - if (regex == null) { - throw new NullPointerException(); - } - if (limit < 0) { - throw new IllegalArgumentException(); - } - if (regex.length() == 0) { - 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); + return splitWithLimitImpl(regex, limit); + } + + private String[] splitImpl(String regex) { + return toString().split(regex); } public String[] split(String regex) { - preconditionCheck(); - if (regex == null) { - throw new NullPointerException(); - } - 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]); - } - return strings; - } - executeConcretely(); - return toStringImpl().split(regex); + return splitImpl(regex); } public String toLowerCase(Locale locale) { 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 3e29087cf6..1ae6418cec 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 @@ -297,8 +296,6 @@ val UtSort.defaultValue: UtExpression UtFp32Sort -> mkFloat(0f) 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 8edee10242..f17121f62e 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 936ca1a137..6bcc8a24ae 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/ObjectWrappers.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/ObjectWrappers.kt @@ -18,7 +18,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 @@ -58,7 +57,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) @@ -140,7 +138,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/Strings.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt index 0af61b14f8..ee7e10e1ef 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt @@ -1,30 +1,20 @@ package org.utbot.engine import com.github.curiousoddman.rgxgen.RgxGen -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 @@ -32,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 @@ -43,15 +32,12 @@ 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 import soot.SootClass import soot.SootField import soot.SootMethod -import kotlin.reflect.KFunction4 val utStringClass: SootClass get() = Scene.v().getSootClass(UtString::class.qualifiedName) @@ -77,71 +63,14 @@ 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) + } + else -> { + null } - else -> return null } } @@ -186,200 +115,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 { - override fun isWrappedMethod(method: SootMethod): Boolean = method.subSignature in wrappedMethods - - override operator fun Traverser.invoke( + private fun Traverser.symbolicMatchesMethodImpl( wrapper: ObjectValue, - method: SootMethod, parameters: List - ): List { - val wrappedMethodResult = wrappedMethods[method.subSignature] - ?: error("unknown wrapped method ${method.subSignature} for ${this::class}") - - return wrappedMethodResult(this, wrapper, method, parameters) - } + ): List? { + val arg = parameters[0] as ObjectValue + val matchingLengthExpr = getIntFieldValue(arg, STRING_LENGTH).accept(RewritingVisitor()) - @Suppress("UNUSED_PARAMETER") - private fun defaultInitMethodWrapper( - traverser: Traverser, - wrapper: ObjectValue, - method: SootMethod, - parameters: List - ): List = - with(traverser) { - val newString = mkString(nextStringName()) + if (!matchingLengthExpr.isConcrete) return null - val memoryUpdate = MemoryUpdate( - stores = persistentListOf(simplifiedNamedStore(valueDescriptor, wrapper.addr, newString)), - touchedChunkDescriptors = persistentSetOf(valueDescriptor) - ) + val matchingValueExpr = + selectArrayExpressionFromMemory(getValueArray(arg.addr)).accept(RewritingVisitor()) + val matchingLength = matchingLengthExpr.toConcrete() as Int + val matchingValue = CharArray(matchingLength) - listOf( - MethodResult( - SymbolicSuccess(voidValue), - memoryUpdates = memoryUpdate - ) - ) - } + for (i in 0 until matchingLength) { + val charExpr = matchingValueExpr.select(mkInt(i)).accept(RewritingVisitor()) - @Suppress("UNUSED_PARAMETER") - private fun initFromIntMethodWrapper( - traverser: Traverser, - wrapper: ObjectValue, - method: SootMethod, - parameters: List - ): List = - with(traverser) { - val newString = UtConvertToString((parameters[0] as PrimitiveValue).expr) - val memoryUpdate = MemoryUpdate( - stores = persistentListOf(simplifiedNamedStore(valueDescriptor, wrapper.addr, newString)), - touchedChunkDescriptors = persistentSetOf(valueDescriptor) - ) + if (!charExpr.isConcrete) return null - listOf( - MethodResult( - SymbolicSuccess(voidValue), - memoryUpdates = memoryUpdate - ) - ) + matchingValue[i] = (charExpr.toConcrete() as Number).toChar() } - @Suppress("UNUSED_PARAMETER") - private fun initFromLongMethodWrapper( - traverser: Traverser, - wrapper: ObjectValue, - method: SootMethod, - parameters: List - ): List = - with(traverser) { - val newString = UtConvertToString((parameters[0] as PrimitiveValue).expr) - val memoryUpdate = MemoryUpdate( - stores = persistentListOf(simplifiedNamedStore(valueDescriptor, wrapper.addr, newString)), - touchedChunkDescriptors = persistentSetOf(valueDescriptor) - ) + val rgxGen = RgxGen(String(matchingValue)) + val matching = rgxGen.generate() + val notMatching = rgxGen.generateNotMatching() - listOf( - MethodResult( - SymbolicSuccess(voidValue), - memoryUpdates = memoryUpdate - ) - ) - } - - @Suppress("UNUSED_PARAMETER") - private fun lengthMethodWrapper( - traverser: Traverser, - wrapper: ObjectValue, - method: SootMethod, - parameters: List - ): List = - with(traverser) { - val result = UtStringLength(memory.nativeStringValue(wrapper.addr)) - - listOf(MethodResult(SymbolicSuccess(result.toByteValue().cast(IntType.v())))) - } - - @Suppress("UNUSED_PARAMETER") - private fun charAtMethodWrapper( - traverser: Traverser, - wrapper: ObjectValue, - method: SootMethod, - parameters: List - ): List = - with(traverser) { - val index = (parameters[0] as PrimitiveValue).expr - val result = UtStringCharAt(memory.nativeStringValue(wrapper.addr), index) - - listOf(MethodResult(SymbolicSuccess(result.toCharValue()))) - } - - @Suppress("UNUSED_PARAMETER") - private fun codePointAtMethodWrapper( - traverser: Traverser, - wrapper: ObjectValue, - method: SootMethod, - parameters: List - ): List = - with(traverser) { - val index = (parameters[0] as PrimitiveValue).expr - val result = UtStringCharAt(memory.nativeStringValue(wrapper.addr), index) + val thisLength = getIntFieldValue(wrapper, STRING_LENGTH) + val thisValue = selectArrayExpressionFromMemory(getValueArray(wrapper.addr)) - listOf(MethodResult(SymbolicSuccess(result.toCharValue().cast(IntType.v())))) + val matchingConstraints = mutableSetOf() + matchingConstraints += mkEq(thisLength, mkInt(matching.length)) + for (i in matching.indices) { + matchingConstraints += mkEq(thisValue.select(mkInt(i)), mkChar(matching[i])) } - @Suppress("UNUSED_PARAMETER") - private fun toIntegerMethodWrapper( - traverser: Traverser, - wrapper: ObjectValue, - method: SootMethod, - parameters: List - ): List = - with(traverser) { - val result = UtStringToInt(memory.nativeStringValue(wrapper.addr), UtIntSort) - - listOf(MethodResult(SymbolicSuccess(result.toIntValue()))) + val notMatchingConstraints = mutableSetOf() + notMatchingConstraints += mkEq(thisLength, mkInt(notMatching.length)) + for (i in notMatching.indices) { + notMatchingConstraints += mkEq(thisValue.select(mkInt(i)), mkChar(notMatching[i])) } - @Suppress("UNUSED_PARAMETER") - private fun toLongMethodWrapper( - traverser: Traverser, - wrapper: ObjectValue, - method: SootMethod, - parameters: List - ): List = - with(traverser) { - val result = UtStringToInt(memory.nativeStringValue(wrapper.addr), UtLongSort) - - listOf(MethodResult(SymbolicSuccess(result.toLongValue()))) - } + return listOf( + MethodResult(UtTrue.toBoolValue(), matchingConstraints.asHardConstraint()), + MethodResult(UtFalse.toBoolValue(), notMatchingConstraints.asHardConstraint()) + ) + } - @Suppress("UNUSED_PARAMETER") - private fun toCharArrayMethodWrapper( - traverser: Traverser, + private fun Traverser.symbolicCharAtMethodImpl( wrapper: ObjectValue, - method: SootMethod, parameters: List - ): List = - with(traverser) { - 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) - ) + ): 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() ) - } - override val wrappedMethods: Map = - mapOf( - "void ()" to ::defaultInitMethodWrapper, - "void (int)" to ::initFromIntMethodWrapper, - "void (long)" to ::initFromLongMethodWrapper, - "int length()" to ::lengthMethodWrapper, - "char charAt(int)" to ::charAtMethodWrapper, - "int codePointAt(int)" to ::codePointAtMethodWrapper, - "int toInteger()" to ::toIntegerMethodWrapper, - "long toLong()" to ::toLongMethodWrapper, - "char[] toCharArray(int)" to ::toCharArrayMethodWrapper, - ) - - private val valueDescriptor = NATIVE_STRING_VALUE_DESCRIPTOR + val valueExpr = selectArrayExpressionFromMemory(getValueArray(wrapper.addr)) - override fun value(resolver: Resolver, wrapper: ObjectValue): UtModel = UtNullModel(STRING_TYPE.classId) + 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 5f226f8524..e573ada66b 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 @@ -96,8 +96,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 e92dadf74f..3460aae522 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 @@ -153,7 +153,6 @@ private val classesToLoad = arrayOf( org.utbot.engine.overrides.collections.UtGenericStorage::class, org.utbot.engine.overrides.collections.UtGenericAssociative::class, org.utbot.engine.overrides.PrintStream::class, - org.utbot.engine.UtNativeStringWrapper::class, org.utbot.engine.overrides.strings.UtString::class, org.utbot.engine.overrides.strings.UtStringBuilder::class, org.utbot.engine.overrides.strings.UtStringBuffer::class, diff --git a/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/UtValueTestCaseChecker.kt b/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/UtValueTestCaseChecker.kt index 8cdf559742..11c426c1ce 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/UtValueTestCaseChecker.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/UtValueTestCaseChecker.kt @@ -2364,11 +2364,10 @@ abstract class UtValueTestCaseChecker( // TODO check that all generated classes have different content JIRA:1415 logger.info { "Total configurations: ${succeeded.size + failed.size}. Failed: ${failed.size}." } - require(failed.isEmpty()) { val separator = System.lineSeparator() val failedConfigurations = failed.joinToString(prefix = separator, separator = separator) - + logger.error { "Failed configurations: $failedConfigurations" } "Failed configurations: $failedConfigurations" } } 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..2c5774600f 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; @@ -44,6 +46,16 @@ public String intToString(int a, int b) { } } + public String[] intToStringWithConstants() { + return new String[]{ + Integer.toString(Integer.MIN_VALUE), + Integer.toString(Integer.MIN_VALUE + 100), + Integer.toString(0), + Integer.toString(Integer.MAX_VALUE - 100), + Integer.toString(Integer.MAX_VALUE) + }; + } + public String longToString(long a, long b) { if (a > b) { return Long.toString(a); @@ -52,6 +64,16 @@ public String longToString(long a, long b) { } } + public String[] longToStringWithConstants() { + return new String[]{ + Long.toString(Long.MIN_VALUE), + Long.toString(Long.MIN_VALUE + 100L), + Long.toString(0), + Long.toString(Long.MAX_VALUE - 100L), + Long.toString(Long.MAX_VALUE) + }; + } + public String startsWithLiteral(String str) { if (str.startsWith("1234567890")) { str = str.replace("3", "A"); @@ -74,6 +96,16 @@ public String byteToString(byte a, byte b) { } } + public String[] byteToStringWithConstants() { + return new String[]{ + Byte.toString(Byte.MIN_VALUE), + Byte.toString((byte) (Byte.MIN_VALUE + 100)), + Byte.toString((byte) 0), + Byte.toString((byte) (Byte.MAX_VALUE - 100)), + Byte.toString(Byte.MAX_VALUE) + }; + } + public String replace(String a, String b) { return a.replace("abc", b); } @@ -94,6 +126,16 @@ public String shortToString(short a, short b) { } } + public String[] shortToStringWithConstants() { + return new String[]{ + Short.toString(Short.MIN_VALUE), + Short.toString((short) (Short.MIN_VALUE + 100)), + Short.toString((short) 0), + Short.toString((short) (Short.MAX_VALUE - 100)), + Short.toString(Short.MAX_VALUE) + }; + } + public String booleanToString(boolean a, boolean b) { if (a ^ b) { return Boolean.toString(a ^ b); @@ -175,6 +217,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}");