Change a hard limit for arrays size

build.gradle.kts

@@ -67,6 +67,7 @@ allprojects {
                 "--add-opens", "java.base/java.util.concurrent=ALL-UNNAMED",
                 "--add-opens", "java.base/java.util.concurrent.locks=ALL-UNNAMED",
                 "--add-opens", "java.base/java.text=ALL-UNNAMED",
+                "--add-opens", "java.base/java.io=ALL-UNNAMED",
                 "--add-opens", "java.base/sun.security.util=ALL-UNNAMED",
                 "--add-opens", "java.base/sun.reflect.generics.repository=ALL-UNNAMED",
                 "--add-opens", "java.base/java.security=ALL-UNNAMED",

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

@@ -512,6 +512,17 @@ object UtSettings : AbstractSettings(logger, defaultKeyForSettingsPath, defaultS
      * it is more important not to fall at all rather than work precisely.
      */
     var treatAbsentMethodsAsUnboundedValue by getBooleanProperty(false)
+
+    // region preferred size options
+    // Changes in this region might severe influence on the performance of symbolic execution.
+
+    /**
+     * A maximum size for any array in the program. Note that input arrays might be less than this value
+     * due to the symbolic engine limitation, see `org.utbot.engine.Traverser.softMaxArraySize`.
+     */
+    var maxArraySize by getIntProperty(1024)
+
+    // endregion
 }
 
 /**

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

@@ -15,6 +15,7 @@ object OpenModulesContainer {
             openPackage("java.base", "java.lang.invoke")
             openPackage("java.base", "jdk.internal.misc")
             openPackage("java.base", "sun.reflect.generics.repository")
+            openPackage("java.base", "java.io")
             openPackage("java.base", "java.lang")
             openPackage("java.base", "java.security")
             openPackage("java.base", "java.util")

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

@@ -0,0 +1,42 @@
+package org.utbot.examples.stdlib
+
+import org.junit.jupiter.api.Test
+import org.utbot.framework.plugin.api.CodegenLanguage
+import org.utbot.framework.plugin.api.UtCompositeModel
+import org.utbot.framework.plugin.api.UtNewInstanceInstrumentation
+import org.utbot.framework.plugin.api.UtPrimitiveModel
+import org.utbot.framework.plugin.api.util.id
+import org.utbot.testcheckers.eq
+import org.utbot.testing.CodeGeneration
+import org.utbot.testing.DoNotCalculate
+import org.utbot.testing.UtValueTestCaseChecker
+
+internal class JavaIOFileInputStreamCheckTest : UtValueTestCaseChecker(
+    testClass = JavaIOFileInputStreamCheck::class,
+    testCodeGeneration = true,
+    pipelines = listOf(
+        TestLastStage(CodegenLanguage.JAVA),
+        TestLastStage(CodegenLanguage.KOTLIN, CodeGeneration) // because of mocks
+    )) {
+    @Test
+    fun testRead() {
+            checkMocksAndInstrumentation(
+                JavaIOFileInputStreamCheck::read,
+                eq(1),
+                { _, _, instrumentation, r ->
+                    val constructorMock = instrumentation.single() as UtNewInstanceInstrumentation
+
+                    val classIdEquality = constructorMock.classId == java.io.FileInputStream::class.id
+                    val callSiteIdEquality = constructorMock.callSites.single() == JavaIOFileInputStreamCheck::class.id
+                    val instance = constructorMock.instances.single() as UtCompositeModel
+                    val methodMock = instance.mocks.entries.single()
+                    val methodNameEquality = methodMock.key.name == "read"
+                    val mockValueResult = r == (methodMock.value.single() as UtPrimitiveModel).value as Int
+
+                    classIdEquality && callSiteIdEquality && instance.isMock && methodNameEquality && mockValueResult
+                },
+                additionalMockAlwaysClasses = setOf(java.io.FileInputStream::class.id),
+                coverage = DoNotCalculate // there is a problem with coverage calculation of mocked values
+            )
+    }
+}

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

@@ -1,6 +1,7 @@
 package org.utbot.engine.overrides.stream;
 
 import org.jetbrains.annotations.NotNull;
+import org.utbot.engine.ResolverKt;
 import org.utbot.engine.overrides.collections.RangeModifiableUnlimitedArray;
 import org.utbot.engine.overrides.collections.UtGenericStorage;
 import org.utbot.framework.plugin.api.visible.UtStreamConsumingException;
@@ -27,7 +28,6 @@
 
 import static org.utbot.api.mock.UtMock.assume;
 import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
-import static org.utbot.engine.ResolverKt.HARD_MAX_ARRAY_SIZE;
 import static org.utbot.engine.overrides.UtOverrideMock.alreadyVisited;
 import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
 import static org.utbot.engine.overrides.UtOverrideMock.parameter;
@@ -70,7 +70,7 @@ public UtDoubleStream(Double[] data, int startInclusive, int endExclusive) {
      * if it was passed as parameter to method under test.
      * <p>
      * Preconditions that are must be satisfied:
-     * <li> elementData.size in 0..HARD_MAX_ARRAY_SIZE. </li>
+     * <li> elementData.size in 0..MAX_STREAM_SIZE. </li>
      * <li> elementData is marked as parameter </li>
      * <li> elementData.storage and it's elements are marked as parameters </li>
      */
@@ -91,7 +91,7 @@ void preconditionCheck() {
 
         assume(elementData.end >= 0);
         // we can create a stream for an array using Stream.of
-        assumeOrExecuteConcretely(elementData.end <= HARD_MAX_ARRAY_SIZE);
+        assumeOrExecuteConcretely(elementData.end <= ResolverKt.MAX_STREAM_SIZE);
 
         // As real primitive streams contain primitives, we cannot accept nulls.
         for (int i = 0; i < elementData.end; i++) {

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

@@ -1,6 +1,7 @@
 package org.utbot.engine.overrides.stream;
 
 import org.jetbrains.annotations.NotNull;
+import org.utbot.engine.ResolverKt;
 import org.utbot.engine.overrides.collections.RangeModifiableUnlimitedArray;
 import org.utbot.engine.overrides.collections.UtGenericStorage;
 import org.utbot.framework.plugin.api.visible.UtStreamConsumingException;
@@ -28,7 +29,6 @@
 
 import static org.utbot.api.mock.UtMock.assume;
 import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
-import static org.utbot.engine.ResolverKt.HARD_MAX_ARRAY_SIZE;
 import static org.utbot.engine.overrides.UtOverrideMock.alreadyVisited;
 import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
 import static org.utbot.engine.overrides.UtOverrideMock.parameter;
@@ -92,7 +92,7 @@ void preconditionCheck() {
 
         assume(elementData.end >= 0);
         // we can create a stream for an array using Stream.of
-        assumeOrExecuteConcretely(elementData.end <= HARD_MAX_ARRAY_SIZE);
+        assumeOrExecuteConcretely(elementData.end <= ResolverKt.MAX_STREAM_SIZE);
 
         // As real primitive streams contain primitives, we cannot accept nulls.
         for (int i = 0; i < elementData.end; i++) {

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

@@ -1,6 +1,7 @@
 package org.utbot.engine.overrides.stream;
 
 import org.jetbrains.annotations.NotNull;
+import org.utbot.engine.ResolverKt;
 import org.utbot.engine.overrides.collections.RangeModifiableUnlimitedArray;
 import org.utbot.engine.overrides.collections.UtGenericStorage;
 import org.utbot.framework.plugin.api.visible.UtStreamConsumingException;
@@ -28,7 +29,6 @@
 
 import static org.utbot.api.mock.UtMock.assume;
 import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
-import static org.utbot.engine.ResolverKt.HARD_MAX_ARRAY_SIZE;
 import static org.utbot.engine.overrides.UtOverrideMock.alreadyVisited;
 import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
 import static org.utbot.engine.overrides.UtOverrideMock.parameter;
@@ -92,7 +92,7 @@ void preconditionCheck() {
 
         assume(elementData.end >= 0);
         // we can create a stream for an array using Stream.of
-        assumeOrExecuteConcretely(elementData.end <= HARD_MAX_ARRAY_SIZE);
+        assumeOrExecuteConcretely(elementData.end <= ResolverKt.MAX_STREAM_SIZE);
 
         // As real primitive streams contain primitives, we cannot accept nulls.
         for (int i = 0; i < elementData.end; i++) {

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

@@ -1,6 +1,7 @@
 package org.utbot.engine.overrides.stream;
 
 import org.jetbrains.annotations.NotNull;
+import org.utbot.engine.ResolverKt;
 import org.utbot.engine.overrides.UtArrayMock;
 import org.utbot.engine.overrides.collections.RangeModifiableUnlimitedArray;
 import org.utbot.engine.overrides.collections.UtGenericStorage;
@@ -31,7 +32,6 @@
 
 import static org.utbot.api.mock.UtMock.assume;
 import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
-import static org.utbot.engine.ResolverKt.HARD_MAX_ARRAY_SIZE;
 import static org.utbot.engine.overrides.UtOverrideMock.alreadyVisited;
 import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
 import static org.utbot.engine.overrides.UtOverrideMock.parameter;
@@ -95,7 +95,7 @@ void preconditionCheck() {
 
         assume(elementData.end >= 0);
         // we can create a stream for an array using Stream.of
-        assume(elementData.end <= HARD_MAX_ARRAY_SIZE);
+        assume(elementData.end <= ResolverKt.MAX_STREAM_SIZE);
 
         visit(this);
     }

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

@@ -100,16 +100,20 @@ import org.utbot.engine.types.OBJECT_TYPE
 import org.utbot.engine.types.STRING_TYPE
 import org.utbot.engine.types.TypeRegistry
 import org.utbot.engine.types.TypeResolver
+import org.utbot.framework.UtSettings
 import org.utbot.framework.plugin.api.visible.UtStreamConsumingException
 import org.utbot.framework.plugin.api.UtStreamConsumingFailure
 import org.utbot.framework.plugin.api.util.constructor.ValueConstructor
 import org.utbot.framework.plugin.api.util.isStatic
 
 // hack
+// IMPORTANT, if these values are used in code for analysis (e.g., in the wrappers),
+// they must be a compilation time constant to avoid extra analysis.
 const val MAX_LIST_SIZE = 10
 const val MAX_RESOLVE_LIST_SIZE = 256
 const val MAX_STRING_SIZE = 40
-internal const val HARD_MAX_ARRAY_SIZE = 256
+internal const val MAX_STREAM_SIZE = 256
+internal val hardMaxArraySize = UtSettings.maxArraySize
 
 internal const val PREFERRED_ARRAY_SIZE = 2
 internal const val MIN_PREFERRED_INTEGER = -256
@@ -1303,7 +1307,7 @@ private fun Traverser.arrayToMethodResult(
     elementType: Type,
     takeElement: (Int) -> UtExpression
 ): MethodResult {
-    val updatedSize = min(size, HARD_MAX_ARRAY_SIZE)
+    val updatedSize = min(size, hardMaxArraySize)
     val newAddr = findNewAddr()
     val length = memory.findArrayLength(newAddr)
 

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

@@ -132,7 +132,6 @@ import org.utbot.framework.plugin.api.util.findFieldByIdOrNull
 import org.utbot.framework.plugin.api.util.jField
 import org.utbot.framework.plugin.api.util.jClass
 import org.utbot.framework.plugin.api.util.id
-import org.utbot.framework.plugin.api.util.isAbstract
 import org.utbot.framework.plugin.api.util.isConstructor
 import org.utbot.framework.plugin.api.util.utContext
 import org.utbot.framework.util.executableId
@@ -2014,7 +2013,19 @@ class Traverser(
         queuedSymbolicStateUpdates += Ge(length, 0).asHardConstraint()
         workaround(HACK) {
             if (size.expr is UtBvLiteral) {
-                softMaxArraySize = min(HARD_MAX_ARRAY_SIZE, max(size.expr.value.toInt(), softMaxArraySize))
+                val sizeValue = size.expr.value.toInt()
+                softMaxArraySize = min(hardMaxArraySize, max(sizeValue, softMaxArraySize))
+
+                if (sizeValue > hardMaxArraySize) {
+                    logger.warn(
+                        "The engine encountered an array initialization with $sizeValue size." +
+                                " It leads to elimination of paths containing current instruction."
+                    )
+                    logger.warn("Current instruction: ${environment.state.stmt}")
+                    logger.warn("Please, consider increasing `UtSettings.maxArraySize` value, " +
+                            "currently it is ${UtSettings.maxArraySize}."
+                    )
+                }
             }
         }
         queuedSymbolicStateUpdates += Le(length, softMaxArraySize).asHardConstraint() // TODO: fix big array length

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

@@ -0,0 +1,12 @@
+package org.utbot.examples.stdlib;
+
+import java.io.FileInputStream;
+import java.io.IOException;
+
+public class JavaIOFileInputStreamCheck {
+    public int read(String s) throws IOException {
+        java.io.FileInputStream fis = new java.io.FileInputStream(s);
+        byte[] b = new byte[1000];
+        return fis.read(b);
+    }
+}

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

@@ -49,15 +49,20 @@ open class SummaryTestCaseGeneratorTest(
         summaryKeys: List<String>,
         methodNames: List<String> = listOf(),
         displayNames: List<String> = listOf(),
-        clusterInfo: List<Pair<UtClusterInfo, Int>> = listOf()
+        clusterInfo: List<Pair<UtClusterInfo, Int>> = listOf(),
+        additionalMockAlwaysClasses: Set<ClassId> = emptySet()
     ) {
         workaround(WorkaroundReason.HACK) {
             // @todo change to the constructor parameter
             checkSolverTimeoutMillis = 0
             checkNpeInNestedMethods = true
             checkNpeInNestedNotPrivateMethods = true
         }
-        val testSet = executionsModel(method.executableId, mockStrategy)
+        val testSet = executionsModel(
+            method.executableId,
+            mockStrategy,
+            additionalMockAlwaysClasses = additionalMockAlwaysClasses
+        )
         val testSetWithSummarization = listOf(testSet).summarizeAll(searchDirectory, sourceFile = null).single()
 
         testSetWithSummarization.executions.checkMatchersWithTextSummary(summaryKeys)

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

@@ -9,6 +9,7 @@ import org.utbot.engine.UtBotSymbolicEngine
 import org.utbot.engine.util.mockListeners.ForceMockListener
 import org.utbot.engine.util.mockListeners.ForceStaticMockListener
 import org.utbot.framework.UtSettings
+import org.utbot.framework.plugin.api.ClassId
 import org.utbot.framework.plugin.api.ExecutableId
 import org.utbot.framework.plugin.api.MockStrategyApi
 import org.utbot.framework.plugin.api.TestCaseGenerator
@@ -44,7 +45,11 @@ class TestSpecificTestCaseGenerator(
 
     private val logger = KotlinLogging.logger {}
 
-    fun generate(method: ExecutableId, mockStrategy: MockStrategyApi): UtMethodTestSet {
+    fun generate(
+        method: ExecutableId,
+        mockStrategy: MockStrategyApi,
+        additionalMockAlwaysClasses: Set<ClassId> = emptySet()
+    ): UtMethodTestSet {
         if (isCanceled()) {
             return UtMethodTestSet(method)
         }
@@ -54,7 +59,7 @@ class TestSpecificTestCaseGenerator(
         val executions = mutableListOf<UtExecution>()
         val errors = mutableMapOf<String, Int>()
 
-        val mockAlwaysDefaults = Mocker.javaDefaultClasses.mapTo(mutableSetOf()) { it.id }
+        val mockAlwaysDefaults = Mocker.javaDefaultClasses.mapTo(mutableSetOf()) { it.id } + additionalMockAlwaysClasses
         val defaultTimeEstimator = ExecutionTimeEstimator(UtSettings.utBotGenerationTimeoutInMillis, 1)
 
         val forceMockListener = ForceMockListener.create(this, conflictTriggers)