[draft] Check for ArrayStoreException on array update

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<ArrayStoreException>() },
+            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<ArrayStoreException>() },
+            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<ArrayStoreException>() },
+            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<ArrayStoreException>() },
+            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<ArrayStoreException>() }
+        )
+    }
+
+    @Test
+    fun testFill2DPrimitiveArray() {
+        checkWithException(
+            ArrayStoreExceptionExamples::fill2DPrimitiveArray,
+            eq(1),
+            { result -> result.isSuccess }
+        )
+    }
+}

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 }

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<Integer>();
+        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 <T, E> void genericAssignmentWithCast(T[] data, E element) {
+        if (data == null || data.length == 0) return;
+        data[0] = (T) element;
+    }
+
+    private <T, E extends T> void genericAssignmentWithExtends(T[] data, E element) {
+        if (data == null || data.length == 0) return;
+        data[0] = element;
+    }
+}