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..2e6fdc5b49 --- /dev/null +++ b/utbot-framework-test/src/test/kotlin/org/utbot/examples/arrays/ArrayStoreExceptionExamplesTest.kt @@ -0,0 +1,214 @@ +package org.utbot.examples.arrays + +import org.junit.jupiter.api.Disabled +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 + 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 } + ) + } + + @Test + fun testFillObjectArrayWithList() { + check( + ArrayStoreExceptionExamples::fillObjectArrayWithList, + eq(2), + { list, result -> list != null && result != null && result[0] != null }, + { list, result -> list == null && result == null } + ) + } + + @Test + fun testFillWithTreeSet() { + check( + ArrayStoreExceptionExamples::fillWithTreeSet, + eq(2), + { treeSet, result -> treeSet != null && result != null && result[0] != null }, + { treeSet, result -> treeSet == null && result == null } + ) + } + + @Test + fun testFillSomeInterfaceArrayWithSomeInterface() { + check( + ArrayStoreExceptionExamples::fillSomeInterfaceArrayWithSomeInterface, + eq(2), + { impl, result -> impl == null && result == null }, + { impl, result -> impl != null && result != null && result[0] != null } + ) + } + + @Test + @Disabled("TODO: Not null path is not found, need to investigate") + fun testFillObjectArrayWithSomeInterface() { + check( + ArrayStoreExceptionExamples::fillObjectArrayWithSomeInterface, + eq(2), + { impl, result -> impl == null && result == null }, + { impl, result -> impl != null && result != null && result[0] != null } + ) + } + + @Test + fun testFillWithSomeImplementation() { + check( + ArrayStoreExceptionExamples::fillWithSomeImplementation, + eq(2), + { impl, result -> impl == null && result == null }, + { impl, result -> impl != null && result != null && result[0] != null } + ) + } +} diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt index 1b11f25c07..b4e09996af 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt @@ -1,5 +1,7 @@ package org.utbot.engine +import org.utbot.common.WorkaroundReason +import org.utbot.common.workaround import org.utbot.engine.TypeRegistry.Companion.objectTypeStorage import org.utbot.engine.pc.UtAddrExpression import org.utbot.engine.pc.UtBoolExpression @@ -11,6 +13,7 @@ import org.utbot.engine.pc.mkOr import org.utbot.engine.symbolic.* import org.utbot.framework.plugin.api.FieldId import org.utbot.framework.plugin.api.UtInstrumentation +import soot.RefType import java.util.Objects import soot.Scene import soot.SootMethod 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 bb8fe91e87..fe6310a94e 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,57 @@ 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 valueType = value.type + val valueBaseType = valueType.baseType + val arrayElementType = arrayInstance.type.elementType + + // We should check for [ArrayStoreException] only for reference types. + // * For arrays of primitive types, incorrect assignment is prevented as compile time. + // * When assigning primitive literals (e.g., `1`) to arrays of corresponding boxed classes (`Integer`), + // the conversion to the reference type is automatic. + // * [System.arraycopy] and similar functions that can throw [ArrayStoreException] accept [Object] arrays + // as arguments, so array elements are references. + + if (valueBaseType is RefType) { + val arrayElementTypeStorage = typeResolver.constructTypeStorage(arrayElementType, useConcreteType = false) + + // Generate ASE only if [value] is not a subtype of the type of array elements + val isExpression = typeRegistry.typeConstraint(value.addr, arrayElementTypeStorage).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) + + // Currently the negation of [UtIsExpression] seems to work incorrectly for [java.lang.Object]: + // https://github.com/UnitTestBot/UTBotJava/issues/1007 + + // It is related to [org.utbot.engine.pc.Z3TranslatorVisitor.filterInappropriateTypes] that removes + // internal engine classes for [java.lang.Object] type storage, and this logic is not fully + // consistent with the negation. + + // Here we have a specific test for [java.lang.Object] as the type of array elements: + // any reference type may be assigned to elements of an Object array, so we should not generate + // [ArrayStoreException] in these cases. + + // TODO: remove enclosing `if` when [UtIfExpression] negation is fixed + if (!arrayElementType.isJavaLangObject()) { + 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 +830,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..fe201e0cbb --- /dev/null +++ b/utbot-sample/src/main/java/org/utbot/examples/arrays/ArrayStoreExceptionExamples.java @@ -0,0 +1,163 @@ +package org.utbot.examples.arrays; + +import java.util.ArrayList; +import java.util.List; +import java.util.TreeSet; + +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; + } + + public Object[] fillObjectArrayWithList(List list) { + if (list == null) + return null; + + Object[] result = new Object[1]; + result[0] = list; + return result; + } + + public Object[] fillWithTreeSet(TreeSet treeSet) { + if (treeSet == null) + return null; + + Object[] result = new Object[1]; + result[0] = treeSet; + return result; + } + + public SomeInterface[] fillSomeInterfaceArrayWithSomeInterface(SomeInterface impl) { + if (impl == null) + return null; + + SomeInterface[] result = new SomeInterface[1]; + result[0] = impl; + return result; + } + + public Object[] fillObjectArrayWithSomeInterface(SomeInterface impl) { + if (impl == null) + return null; + + Object[] result = new Object[1]; + result[0] = impl; + return result; + } + + public Object[] fillWithSomeImplementation(SomeImplementation impl) { + if (impl == null) + return null; + + Object[] result = new Object[1]; + result[0] = impl; + return result; + } + + 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; + } +} diff --git a/utbot-sample/src/main/java/org/utbot/examples/arrays/SomeImplementation.java b/utbot-sample/src/main/java/org/utbot/examples/arrays/SomeImplementation.java new file mode 100644 index 0000000000..d67592ff91 --- /dev/null +++ b/utbot-sample/src/main/java/org/utbot/examples/arrays/SomeImplementation.java @@ -0,0 +1,8 @@ +package org.utbot.examples.arrays; + +public class SomeImplementation implements SomeInterface { + @Override + public int foo() { + return 0; + } +} diff --git a/utbot-sample/src/main/java/org/utbot/examples/arrays/SomeInterface.java b/utbot-sample/src/main/java/org/utbot/examples/arrays/SomeInterface.java new file mode 100644 index 0000000000..35b7c5a38a --- /dev/null +++ b/utbot-sample/src/main/java/org/utbot/examples/arrays/SomeInterface.java @@ -0,0 +1,5 @@ +package org.utbot.examples.arrays; + +public interface SomeInterface { + int foo(); +}