Skip to content

Commit fde5281

Browse files
CaelmBleiddCaelmBleidd
authored
Change a hard limit for arrays size (#2006)
1 parent a043c33 commit fde5281

File tree

15 files changed

+649
-278
lines changed

15 files changed

+649
-278
lines changed

‎build.gradle.kts

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,7 @@ allprojects {
6767
"--add-opens", "java.base/java.util.concurrent=ALL-UNNAMED",
6868
"--add-opens", "java.base/java.util.concurrent.locks=ALL-UNNAMED",
6969
"--add-opens", "java.base/java.text=ALL-UNNAMED",
70+
"--add-opens", "java.base/java.io=ALL-UNNAMED",
7071
"--add-opens", "java.base/sun.security.util=ALL-UNNAMED",
7172
"--add-opens", "java.base/sun.reflect.generics.repository=ALL-UNNAMED",
7273
"--add-opens", "java.base/java.security=ALL-UNNAMED",

‎utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -512,6 +512,17 @@ object UtSettings : AbstractSettings(logger, defaultKeyForSettingsPath, defaultS
512512
* it is more important not to fall at all rather than work precisely.
513513
*/
514514
var treatAbsentMethodsAsUnboundedValue by getBooleanProperty(false)
515+
516+
// region preferred size options
517+
// Changes in this region might severe influence on the performance of symbolic execution.
518+
519+
/**
520+
* A maximum size for any array in the program. Note that input arrays might be less than this value
521+
* due to the symbolic engine limitation, see `org.utbot.engine.Traverser.softMaxArraySize`.
522+
*/
523+
var maxArraySize by getIntProperty(1024)
524+
525+
// endregion
515526
}
516527

517528
/**

‎utbot-framework-api/src/main/kotlin/org/utbot/framework/process/OpenModulesContainer.kt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ object OpenModulesContainer {
1515
openPackage("java.base", "java.lang.invoke")
1616
openPackage("java.base", "jdk.internal.misc")
1717
openPackage("java.base", "sun.reflect.generics.repository")
18+
openPackage("java.base", "java.io")
1819
openPackage("java.base", "java.lang")
1920
openPackage("java.base", "java.security")
2021
openPackage("java.base", "java.util")

‎utbot-framework-test/src/test/kotlin/org/utbot/examples/stdlib/JavaIOFileInputStreamCheck.kt

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
package org.utbot.examples.stdlib
2+
3+
import org.junit.jupiter.api.Test
4+
import org.utbot.framework.plugin.api.CodegenLanguage
5+
import org.utbot.framework.plugin.api.UtCompositeModel
6+
import org.utbot.framework.plugin.api.UtNewInstanceInstrumentation
7+
import org.utbot.framework.plugin.api.UtPrimitiveModel
8+
import org.utbot.framework.plugin.api.util.id
9+
import org.utbot.testcheckers.eq
10+
import org.utbot.testing.CodeGeneration
11+
import org.utbot.testing.DoNotCalculate
12+
import org.utbot.testing.UtValueTestCaseChecker
13+
14+
internal class JavaIOFileInputStreamCheckTest : UtValueTestCaseChecker(
15+
testClass = JavaIOFileInputStreamCheck::class,
16+
testCodeGeneration = true,
17+
pipelines = listOf(
18+
TestLastStage(CodegenLanguage.JAVA),
19+
TestLastStage(CodegenLanguage.KOTLIN, CodeGeneration) // because of mocks
20+
)) {
21+
@Test
22+
fun testRead() {
23+
checkMocksAndInstrumentation(
24+
JavaIOFileInputStreamCheck::read,
25+
eq(1),
26+
{ _, _, instrumentation, r ->
27+
val constructorMock = instrumentation.single() as UtNewInstanceInstrumentation
28+
29+
val classIdEquality = constructorMock.classId == java.io.FileInputStream::class.id
30+
val callSiteIdEquality = constructorMock.callSites.single() == JavaIOFileInputStreamCheck::class.id
31+
val instance = constructorMock.instances.single() as UtCompositeModel
32+
val methodMock = instance.mocks.entries.single()
33+
val methodNameEquality = methodMock.key.name == "read"
34+
val mockValueResult = r == (methodMock.value.single() as UtPrimitiveModel).value as Int
35+
36+
classIdEquality && callSiteIdEquality && instance.isMock && methodNameEquality && mockValueResult
37+
},
38+
additionalMockAlwaysClasses = setOf(java.io.FileInputStream::class.id),
39+
coverage = DoNotCalculate // there is a problem with coverage calculation of mocked values
40+
)
41+
}
42+
}

‎utbot-framework/src/main/java/org/utbot/engine/overrides/stream/UtDoubleStream.java

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package org.utbot.engine.overrides.stream;
22

33
import org.jetbrains.annotations.NotNull;
4+
import org.utbot.engine.ResolverKt;
45
import org.utbot.engine.overrides.collections.RangeModifiableUnlimitedArray;
56
import org.utbot.engine.overrides.collections.UtGenericStorage;
67
import org.utbot.framework.plugin.api.visible.UtStreamConsumingException;
@@ -27,7 +28,6 @@
2728

2829
import static org.utbot.api.mock.UtMock.assume;
2930
import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
30-
import static org.utbot.engine.ResolverKt.HARD_MAX_ARRAY_SIZE;
3131
import static org.utbot.engine.overrides.UtOverrideMock.alreadyVisited;
3232
import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
3333
import static org.utbot.engine.overrides.UtOverrideMock.parameter;
@@ -70,7 +70,7 @@ public UtDoubleStream(Double[] data, int startInclusive, int endExclusive) {
7070
* if it was passed as parameter to method under test.
7171
* <p>
7272
* Preconditions that are must be satisfied:
73-
* <li> elementData.size in 0..HARD_MAX_ARRAY_SIZE. </li>
73+
* <li> elementData.size in 0..MAX_STREAM_SIZE. </li>
7474
* <li> elementData is marked as parameter </li>
7575
* <li> elementData.storage and it's elements are marked as parameters </li>
7676
*/
@@ -91,7 +91,7 @@ void preconditionCheck() {
9191

9292
assume(elementData.end >= 0);
9393
// we can create a stream for an array using Stream.of
94-
assumeOrExecuteConcretely(elementData.end <= HARD_MAX_ARRAY_SIZE);
94+
assumeOrExecuteConcretely(elementData.end <= ResolverKt.MAX_STREAM_SIZE);
9595

9696
// As real primitive streams contain primitives, we cannot accept nulls.
9797
for (int i = 0; i < elementData.end; i++) {

‎utbot-framework/src/main/java/org/utbot/engine/overrides/stream/UtIntStream.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package org.utbot.engine.overrides.stream;
22

33
import org.jetbrains.annotations.NotNull;
4+
import org.utbot.engine.ResolverKt;
45
import org.utbot.engine.overrides.collections.RangeModifiableUnlimitedArray;
56
import org.utbot.engine.overrides.collections.UtGenericStorage;
67
import org.utbot.framework.plugin.api.visible.UtStreamConsumingException;
@@ -28,7 +29,6 @@
2829

2930
import static org.utbot.api.mock.UtMock.assume;
3031
import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
31-
import static org.utbot.engine.ResolverKt.HARD_MAX_ARRAY_SIZE;
3232
import static org.utbot.engine.overrides.UtOverrideMock.alreadyVisited;
3333
import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
3434
import static org.utbot.engine.overrides.UtOverrideMock.parameter;
@@ -92,7 +92,7 @@ void preconditionCheck() {
9292

9393
assume(elementData.end >= 0);
9494
// we can create a stream for an array using Stream.of
95-
assumeOrExecuteConcretely(elementData.end <= HARD_MAX_ARRAY_SIZE);
95+
assumeOrExecuteConcretely(elementData.end <= ResolverKt.MAX_STREAM_SIZE);
9696

9797
// As real primitive streams contain primitives, we cannot accept nulls.
9898
for (int i = 0; i < elementData.end; i++) {

‎utbot-framework/src/main/java/org/utbot/engine/overrides/stream/UtLongStream.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package org.utbot.engine.overrides.stream;
22

33
import org.jetbrains.annotations.NotNull;
4+
import org.utbot.engine.ResolverKt;
45
import org.utbot.engine.overrides.collections.RangeModifiableUnlimitedArray;
56
import org.utbot.engine.overrides.collections.UtGenericStorage;
67
import org.utbot.framework.plugin.api.visible.UtStreamConsumingException;
@@ -28,7 +29,6 @@
2829

2930
import static org.utbot.api.mock.UtMock.assume;
3031
import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
31-
import static org.utbot.engine.ResolverKt.HARD_MAX_ARRAY_SIZE;
3232
import static org.utbot.engine.overrides.UtOverrideMock.alreadyVisited;
3333
import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
3434
import static org.utbot.engine.overrides.UtOverrideMock.parameter;
@@ -92,7 +92,7 @@ void preconditionCheck() {
9292

9393
assume(elementData.end >= 0);
9494
// we can create a stream for an array using Stream.of
95-
assumeOrExecuteConcretely(elementData.end <= HARD_MAX_ARRAY_SIZE);
95+
assumeOrExecuteConcretely(elementData.end <= ResolverKt.MAX_STREAM_SIZE);
9696

9797
// As real primitive streams contain primitives, we cannot accept nulls.
9898
for (int i = 0; i < elementData.end; i++) {

‎utbot-framework/src/main/java/org/utbot/engine/overrides/stream/UtStream.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package org.utbot.engine.overrides.stream;
22

33
import org.jetbrains.annotations.NotNull;
4+
import org.utbot.engine.ResolverKt;
45
import org.utbot.engine.overrides.UtArrayMock;
56
import org.utbot.engine.overrides.collections.RangeModifiableUnlimitedArray;
67
import org.utbot.engine.overrides.collections.UtGenericStorage;
@@ -31,7 +32,6 @@
3132

3233
import static org.utbot.api.mock.UtMock.assume;
3334
import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
34-
import static org.utbot.engine.ResolverKt.HARD_MAX_ARRAY_SIZE;
3535
import static org.utbot.engine.overrides.UtOverrideMock.alreadyVisited;
3636
import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
3737
import static org.utbot.engine.overrides.UtOverrideMock.parameter;
@@ -95,7 +95,7 @@ void preconditionCheck() {
9595

9696
assume(elementData.end >= 0);
9797
// we can create a stream for an array using Stream.of
98-
assume(elementData.end <= HARD_MAX_ARRAY_SIZE);
98+
assume(elementData.end <= ResolverKt.MAX_STREAM_SIZE);
9999

100100
visit(this);
101101
}

‎utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -100,16 +100,20 @@ import org.utbot.engine.types.OBJECT_TYPE
100100
import org.utbot.engine.types.STRING_TYPE
101101
import org.utbot.engine.types.TypeRegistry
102102
import org.utbot.engine.types.TypeResolver
103+
import org.utbot.framework.UtSettings
103104
import org.utbot.framework.plugin.api.visible.UtStreamConsumingException
104105
import org.utbot.framework.plugin.api.UtStreamConsumingFailure
105106
import org.utbot.framework.plugin.api.util.constructor.ValueConstructor
106107
import org.utbot.framework.plugin.api.util.isStatic
107108

108109
// hack
110+
// IMPORTANT, if these values are used in code for analysis (e.g., in the wrappers),
111+
// they must be a compilation time constant to avoid extra analysis.
109112
const val MAX_LIST_SIZE = 10
110113
const val MAX_RESOLVE_LIST_SIZE = 256
111114
const val MAX_STRING_SIZE = 40
112-
internal const val HARD_MAX_ARRAY_SIZE = 256
115+
internal const val MAX_STREAM_SIZE = 256
116+
internal val hardMaxArraySize = UtSettings.maxArraySize
113117

114118
internal const val PREFERRED_ARRAY_SIZE = 2
115119
internal const val MIN_PREFERRED_INTEGER = -256
@@ -1303,7 +1307,7 @@ private fun Traverser.arrayToMethodResult(
13031307
elementType: Type,
13041308
takeElement: (Int) -> UtExpression
13051309
): MethodResult {
1306-
val updatedSize = min(size, HARD_MAX_ARRAY_SIZE)
1310+
val updatedSize = min(size, hardMaxArraySize)
13071311
val newAddr = findNewAddr()
13081312
val length = memory.findArrayLength(newAddr)
13091313

‎utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,6 @@ import org.utbot.framework.plugin.api.util.findFieldByIdOrNull
132132
import org.utbot.framework.plugin.api.util.jField
133133
import org.utbot.framework.plugin.api.util.jClass
134134
import org.utbot.framework.plugin.api.util.id
135-
import org.utbot.framework.plugin.api.util.isAbstract
136135
import org.utbot.framework.plugin.api.util.isConstructor
137136
import org.utbot.framework.plugin.api.util.utContext
138137
import org.utbot.framework.util.executableId
@@ -2014,7 +2013,19 @@ class Traverser(
20142013
queuedSymbolicStateUpdates += Ge(length, 0).asHardConstraint()
20152014
workaround(HACK) {
20162015
if (size.expr is UtBvLiteral) {
2017-
softMaxArraySize = min(HARD_MAX_ARRAY_SIZE, max(size.expr.value.toInt(), softMaxArraySize))
2016+
val sizeValue = size.expr.value.toInt()
2017+
softMaxArraySize = min(hardMaxArraySize, max(sizeValue, softMaxArraySize))
2018+
2019+
if (sizeValue > hardMaxArraySize) {
2020+
logger.warn(
2021+
"The engine encountered an array initialization with $sizeValue size." +
2022+
" It leads to elimination of paths containing current instruction."
2023+
)
2024+
logger.warn("Current instruction: ${environment.state.stmt}")
2025+
logger.warn("Please, consider increasing `UtSettings.maxArraySize` value, " +
2026+
"currently it is ${UtSettings.maxArraySize}."
2027+
)
2028+
}
20182029
}
20192030
}
20202031
queuedSymbolicStateUpdates += Le(length, softMaxArraySize).asHardConstraint() // TODO: fix big array length

‎utbot-sample/src/main/java/org/utbot/examples/stdlib/JavaIOFileInputStreamCheck.java

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
package org.utbot.examples.stdlib;
2+
3+
import java.io.FileInputStream;
4+
import java.io.IOException;
5+
6+
public class JavaIOFileInputStreamCheck {
7+
public int read(String s) throws IOException {
8+
java.io.FileInputStream fis = new java.io.FileInputStream(s);
9+
byte[] b = new byte[1000];
10+
return fis.read(b);
11+
}
12+
}

‎utbot-summary-tests/src/test/kotlin/examples/SummaryTestCaseGeneratorTest.kt

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,15 +49,20 @@ open class SummaryTestCaseGeneratorTest(
4949
summaryKeys: List<String>,
5050
methodNames: List<String> = listOf(),
5151
displayNames: List<String> = listOf(),
52-
clusterInfo: List<Pair<UtClusterInfo, Int>> = listOf()
52+
clusterInfo: List<Pair<UtClusterInfo, Int>> = listOf(),
53+
additionalMockAlwaysClasses: Set<ClassId> = emptySet()
5354
) {
5455
workaround(WorkaroundReason.HACK) {
5556
// @todo change to the constructor parameter
5657
checkSolverTimeoutMillis = 0
5758
checkNpeInNestedMethods = true
5859
checkNpeInNestedNotPrivateMethods = true
5960
}
60-
val testSet = executionsModel(method.executableId, mockStrategy)
61+
val testSet = executionsModel(
62+
method.executableId,
63+
mockStrategy,
64+
additionalMockAlwaysClasses = additionalMockAlwaysClasses
65+
)
6166
val testSetWithSummarization = listOf(testSet).summarizeAll(searchDirectory, sourceFile = null).single()
6267

6368
testSetWithSummarization.executions.checkMatchersWithTextSummary(summaryKeys)

‎utbot-testing/src/main/kotlin/org/utbot/testing/TestSpecificTestCaseGenerator.kt

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ import org.utbot.engine.UtBotSymbolicEngine
99
import org.utbot.engine.util.mockListeners.ForceMockListener
1010
import org.utbot.engine.util.mockListeners.ForceStaticMockListener
1111
import org.utbot.framework.UtSettings
12+
import org.utbot.framework.plugin.api.ClassId
1213
import org.utbot.framework.plugin.api.ExecutableId
1314
import org.utbot.framework.plugin.api.MockStrategyApi
1415
import org.utbot.framework.plugin.api.TestCaseGenerator
@@ -44,7 +45,11 @@ class TestSpecificTestCaseGenerator(
4445

4546
private val logger = KotlinLogging.logger {}
4647

47-
fun generate(method: ExecutableId, mockStrategy: MockStrategyApi): UtMethodTestSet {
48+
fun generate(
49+
method: ExecutableId,
50+
mockStrategy: MockStrategyApi,
51+
additionalMockAlwaysClasses: Set<ClassId> = emptySet()
52+
): UtMethodTestSet {
4853
if (isCanceled()) {
4954
return UtMethodTestSet(method)
5055
}
@@ -54,7 +59,7 @@ class TestSpecificTestCaseGenerator(
5459
val executions = mutableListOf<UtExecution>()
5560
val errors = mutableMapOf<String, Int>()
5661

57-
val mockAlwaysDefaults = Mocker.javaDefaultClasses.mapTo(mutableSetOf()) { it.id }
62+
val mockAlwaysDefaults = Mocker.javaDefaultClasses.mapTo(mutableSetOf()) { it.id } + additionalMockAlwaysClasses
5863
val defaultTimeEstimator = ExecutionTimeEstimator(UtSettings.utBotGenerationTimeoutInMillis, 1)
5964

6065
val forceMockListener = ForceMockListener.create(this, conflictTriggers)

0 commit comments

Comments
 (0)