diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/examples/arrays/ArrayStoreExceptionExamplesTest.kt b/utbot-framework-test/src/test/kotlin/org/utbot/examples/arrays/ArrayStoreExceptionExamplesTest.kt new file mode 100644 index 0000000000..9f15fe6366 --- /dev/null +++ b/utbot-framework-test/src/test/kotlin/org/utbot/examples/arrays/ArrayStoreExceptionExamplesTest.kt @@ -0,0 +1,162 @@ +package org.utbot.examples.arrays + +import org.junit.jupiter.api.Test +import org.utbot.framework.plugin.api.CodegenLanguage +import org.utbot.testcheckers.eq +import org.utbot.tests.infrastructure.AtLeast +import org.utbot.tests.infrastructure.CodeGeneration +import org.utbot.tests.infrastructure.UtValueTestCaseChecker +import org.utbot.tests.infrastructure.isException + +class ArrayStoreExceptionExamplesTest : UtValueTestCaseChecker( + testClass = ArrayStoreExceptionExamples::class, + languagePipelines = listOf( + CodeGenerationLanguageLastStage(CodegenLanguage.JAVA), + // Type inference errors in generated Kotlin code (Number) + CodeGenerationLanguageLastStage(CodegenLanguage.KOTLIN, CodeGeneration) + ) +) { + @Test + fun testCorrectAssignmentSamePrimitiveType() { + checkWithException( + ArrayStoreExceptionExamples::correctAssignmentSamePrimitiveType, + eq(3), + { data, result -> result.isSuccess && result.getOrNull() == data?.isNotEmpty() } + ) + } + + @Test + fun testCorrectAssignmentIntToIntegerArray() { + checkWithException( + ArrayStoreExceptionExamples::correctAssignmentIntToIntegerArray, + eq(3), + { data, result -> result.isSuccess && result.getOrNull() == data?.isNotEmpty() } + ) + } + + @Test + fun testCorrectAssignmentSubtype() { + checkWithException( + ArrayStoreExceptionExamples::correctAssignmentSubtype, + eq(3), + { data, result -> result.isSuccess && result.getOrNull() == data?.isNotEmpty() } + ) + } + + @Test + fun testCorrectAssignmentToObjectArray() { + checkWithException( + ArrayStoreExceptionExamples::correctAssignmentToObjectArray, + eq(3), + { data, result -> result.isSuccess && result.getOrNull() == data?.isNotEmpty() } + ) + } + + @Test + fun testWrongAssignmentUnrelatedType() { + checkWithException( + ArrayStoreExceptionExamples::wrongAssignmentUnrelatedType, + eq(3), + { data, result -> data == null && result.isSuccess }, + { data, result -> data.isEmpty() && result.isSuccess }, + { data, result -> data.isNotEmpty() && result.isException() }, + coverage = AtLeast(91) // TODO: investigate + ) + } + + @Test + fun testCheckGenericAssignmentWithCorrectCast() { + checkWithException( + ArrayStoreExceptionExamples::checkGenericAssignmentWithCorrectCast, + eq(1), + { result -> result.isSuccess } + ) + } + + @Test + fun testCheckGenericAssignmentWithWrongCast() { + checkWithException( + ArrayStoreExceptionExamples::checkGenericAssignmentWithWrongCast, + eq(1), + { result -> result.isException() }, + coverage = AtLeast(87) // TODO: investigate + ) + } + + @Test + fun testCheckGenericAssignmentWithExtendsSubtype() { + checkWithException( + ArrayStoreExceptionExamples::checkGenericAssignmentWithExtendsSubtype, + eq(1), + { result -> result.isSuccess } + ) + } + + @Test + fun testCheckGenericAssignmentWithExtendsUnrelated() { + checkWithException( + ArrayStoreExceptionExamples::checkGenericAssignmentWithExtendsUnrelated, + eq(1), + { result -> result.isException() }, + coverage = AtLeast(87) // TODO: investigate + ) + } + + @Test + fun testCheckObjectAssignment() { + checkWithException( + ArrayStoreExceptionExamples::checkObjectAssignment, + eq(1), + { result -> result.isSuccess } + ) + } + + // Should this be allowed at all? + @Test + fun testCheckWrongAssignmentOfItself() { + checkWithException( + ArrayStoreExceptionExamples::checkWrongAssignmentOfItself, + eq(1), + { result -> result.isException() }, + coverage = AtLeast(87) + ) + } + + @Test + fun testCheckGoodAssignmentOfItself() { + checkWithException( + ArrayStoreExceptionExamples::checkGoodAssignmentOfItself, + eq(1), + { result -> result.isSuccess } + ) + } + + @Test + fun testCheckAssignmentToObjectArray() { + checkWithException( + ArrayStoreExceptionExamples::checkAssignmentToObjectArray, + eq(1), + { result -> result.isSuccess } + ) + } + + @Test + fun testArrayCopyForIncompatiblePrimitiveTypes() { + checkWithException( + ArrayStoreExceptionExamples::arrayCopyForIncompatiblePrimitiveTypes, + eq(3), + { data, result -> data == null && result.isSuccess && result.getOrNull() == null }, + { data, result -> data != null && data.isEmpty() && result.isSuccess && result.getOrNull()?.size == 0 }, + { data, result -> data != null && data.isNotEmpty() && result.isException() } + ) + } + + @Test + fun testFill2DPrimitiveArray() { + checkWithException( + ArrayStoreExceptionExamples::fill2DPrimitiveArray, + eq(1), + { result -> result.isSuccess } + ) + } +} diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt index d5139836bd..fbdd4f012b 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt @@ -65,9 +65,6 @@ import org.utbot.engine.pc.mkNot import org.utbot.engine.pc.mkOr import org.utbot.engine.pc.select import org.utbot.engine.pc.store -import org.utbot.engine.symbolic.HardConstraint -import org.utbot.engine.symbolic.SoftConstraint -import org.utbot.engine.symbolic.Assumption import org.utbot.engine.symbolic.emptyAssumption import org.utbot.engine.symbolic.emptyHardConstraint import org.utbot.engine.symbolic.emptySoftConstraint @@ -767,6 +764,34 @@ class Traverser( } } + /** + * Check for [ArrayStoreException] when an array element is assigned + * + * @param arrayInstance Symbolic value corresponding to the array being updated + * @param value Symbolic value corresponding to the right side of the assignment + */ + private fun TraversalContext.arrayStoreExceptionCheck(arrayInstance: SymbolicValue, value: SymbolicValue) { + require(arrayInstance is ArrayValue) + val valueBaseType = value.type.baseType + val arrayElementType = arrayInstance.type.elementType + val arrayTypeStorage = typeResolver.constructTypeStorage(arrayElementType, useConcreteType = false) + + if (valueBaseType is RefType) { + // Generate ASE only if [value] is not a subtype of the type of array elements + val isExpression = typeRegistry.typeConstraint(value.addr, arrayTypeStorage).isConstraint() + val notIsExpression = mkNot(isExpression) + + // `null` is compatible with any reference type, so we should not throw ASE when `null` is assigned + val nullEqualityConstraint = addrEq(value.addr, nullObjectAddr) + val notNull = mkNot(nullEqualityConstraint) + + implicitlyThrowException(ArrayStoreException(), setOf(notIsExpression, notNull)) + + // If ASE is not thrown, we know that either the value is null, or it has a compatible type + queuedSymbolicStateUpdates += mkOr(isExpression, nullEqualityConstraint).asHardConstraint() + } + } + /** * Traverses left part of assignment i.e. where to store resolved value. */ @@ -782,12 +807,11 @@ class Traverser( queuedSymbolicStateUpdates += Le(length, softMaxArraySize).asHardConstraint() // TODO: fix big array length - // TODO array store exception + arrayStoreExceptionCheck(arrayInstance, value) // add constraint for possible array type val valueType = value.type val valueBaseType = valueType.baseType - if (valueBaseType is RefType) { val valueTypeAncestors = typeResolver.findOrConstructAncestorsIncludingTypes(valueBaseType) val valuePossibleBaseTypes = value.typeStorage.possibleConcreteTypes.map { it.baseType } diff --git a/utbot-sample/src/main/java/org/utbot/examples/arrays/ArrayStoreExceptionExamples.java b/utbot-sample/src/main/java/org/utbot/examples/arrays/ArrayStoreExceptionExamples.java new file mode 100644 index 0000000000..a215c24f13 --- /dev/null +++ b/utbot-sample/src/main/java/org/utbot/examples/arrays/ArrayStoreExceptionExamples.java @@ -0,0 +1,116 @@ +package org.utbot.examples.arrays; + +import java.util.ArrayList; + +public class ArrayStoreExceptionExamples { + + public boolean correctAssignmentSamePrimitiveType(int[] data) { + if (data == null || data.length == 0) return false; + data[0] = 1; + return true; + } + + public boolean correctAssignmentIntToIntegerArray(Integer[] data) { + if (data == null || data.length == 0) return false; + data[0] = 1; + return true; + } + + public boolean correctAssignmentSubtype(Number[] data) { + if (data == null || data.length == 0) return false; + data[0] = 15; + return true; + } + + public boolean correctAssignmentToObjectArray(Object[] data) { + if (data == null || data.length < 2) return false; + data[0] = 1; + data[1] = new ArrayList(); + return true; + } + + public void wrongAssignmentUnrelatedType(Integer[] data) { + if (data == null || data.length == 0) return; + ((Object[]) data)[0] = "x"; + } + + public void wrongAssignmentSupertype(Integer[] data) { + if (data == null || data.length == 0) return; + Number x = 1.2; + ((Number[]) data)[0] = x; + } + + public void checkGenericAssignmentWithCorrectCast() { + Number[] data = new Number[3]; + genericAssignmentWithCast(data, 5); + } + + public void checkGenericAssignmentWithWrongCast() { + Number[] data = new Number[3]; + genericAssignmentWithCast(data, "x"); + } + + public void checkGenericAssignmentWithExtendsSubtype() { + Number[] data = new Number[3]; + genericAssignmentWithExtends(data, 7); + } + + public void checkGenericAssignmentWithExtendsUnrelated() { + Number[] data = new Number[3]; + genericAssignmentWithExtends(data, "x"); + } + + public void checkObjectAssignment() { + Object[] data = new Object[3]; + data[0] = "x"; + } + + public void checkAssignmentToObjectArray() { + Object[] data = new Object[3]; + data[0] = 1; + data[1] = "a"; + data[2] = data; + } + + public void checkWrongAssignmentOfItself() { + Number[] data = new Number[2]; + genericAssignmentWithCast(data, data); + } + + public void checkGoodAssignmentOfItself() { + Object[] data = new Object[2]; + genericAssignmentWithCast(data, data); + } + + public int[] arrayCopyForIncompatiblePrimitiveTypes(long[] data) { + if (data == null) + return null; + + int[] result = new int[data.length]; + if (data.length != 0) { + System.arraycopy(data, 0, result, 0, data.length); + } + + return result; + } + + public int[][] fill2DPrimitiveArray() { + int[][] data = new int[2][3]; + for (int i = 0; i < 2; i++) { + for (int j = 0; j < 3; j++) { + data[i][j] = i * 3 + j; + } + } + return data; + } + + private void genericAssignmentWithCast(T[] data, E element) { + if (data == null || data.length == 0) return; + data[0] = (T) element; + } + + private void genericAssignmentWithExtends(T[] data, E element) { + if (data == null || data.length == 0) return; + data[0] = element; + } +}