Skip to content

Check for ArrayStoreException on array update #971

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Sep 25, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -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<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 }
)
}

@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 }
)
}
}
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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
Expand Down
57 changes: 52 additions & 5 deletions utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we have an issue with it?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I created the issue: #1007.

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.
*/
Expand All @@ -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 }
Expand Down
Loading