Skip to content

Commit 13d07aa

Browse files
dtimdtim
authored
Check for ArrayStoreException on array update (#971)
1 parent dc0985d commit 13d07aa

File tree

6 files changed

+445
-5
lines changed

6 files changed

+445
-5
lines changed

‎utbot-framework-test/src/test/kotlin/org/utbot/examples/arrays/ArrayStoreExceptionExamplesTest.kt

Lines changed: 214 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,214 @@
1+
package org.utbot.examples.arrays
2+
3+
import org.junit.jupiter.api.Disabled
4+
import org.junit.jupiter.api.Test
5+
import org.utbot.framework.plugin.api.CodegenLanguage
6+
import org.utbot.testcheckers.eq
7+
import org.utbot.tests.infrastructure.AtLeast
8+
import org.utbot.tests.infrastructure.CodeGeneration
9+
import org.utbot.tests.infrastructure.UtValueTestCaseChecker
10+
import org.utbot.tests.infrastructure.isException
11+
12+
class ArrayStoreExceptionExamplesTest : UtValueTestCaseChecker(
13+
testClass = ArrayStoreExceptionExamples::class,
14+
languagePipelines = listOf(
15+
CodeGenerationLanguageLastStage(CodegenLanguage.JAVA),
16+
// Type inference errors in generated Kotlin code
17+
CodeGenerationLanguageLastStage(CodegenLanguage.KOTLIN, CodeGeneration)
18+
)
19+
) {
20+
@Test
21+
fun testCorrectAssignmentSamePrimitiveType() {
22+
checkWithException(
23+
ArrayStoreExceptionExamples::correctAssignmentSamePrimitiveType,
24+
eq(3),
25+
{ data, result -> result.isSuccess && result.getOrNull() == data?.isNotEmpty() }
26+
)
27+
}
28+
29+
@Test
30+
fun testCorrectAssignmentIntToIntegerArray() {
31+
checkWithException(
32+
ArrayStoreExceptionExamples::correctAssignmentIntToIntegerArray,
33+
eq(3),
34+
{ data, result -> result.isSuccess && result.getOrNull() == data?.isNotEmpty() }
35+
)
36+
}
37+
38+
@Test
39+
fun testCorrectAssignmentSubtype() {
40+
checkWithException(
41+
ArrayStoreExceptionExamples::correctAssignmentSubtype,
42+
eq(3),
43+
{ data, result -> result.isSuccess && result.getOrNull() == data?.isNotEmpty() }
44+
)
45+
}
46+
47+
@Test
48+
fun testCorrectAssignmentToObjectArray() {
49+
checkWithException(
50+
ArrayStoreExceptionExamples::correctAssignmentToObjectArray,
51+
eq(3),
52+
{ data, result -> result.isSuccess && result.getOrNull() == data?.isNotEmpty() }
53+
)
54+
}
55+
56+
@Test
57+
fun testWrongAssignmentUnrelatedType() {
58+
checkWithException(
59+
ArrayStoreExceptionExamples::wrongAssignmentUnrelatedType,
60+
eq(3),
61+
{ data, result -> data == null && result.isSuccess },
62+
{ data, result -> data.isEmpty() && result.isSuccess },
63+
{ data, result -> data.isNotEmpty() && result.isException<ArrayStoreException>() },
64+
coverage = AtLeast(91) // TODO: investigate
65+
)
66+
}
67+
68+
@Test
69+
fun testCheckGenericAssignmentWithCorrectCast() {
70+
checkWithException(
71+
ArrayStoreExceptionExamples::checkGenericAssignmentWithCorrectCast,
72+
eq(1),
73+
{ result -> result.isSuccess }
74+
)
75+
}
76+
77+
@Test
78+
fun testCheckGenericAssignmentWithWrongCast() {
79+
checkWithException(
80+
ArrayStoreExceptionExamples::checkGenericAssignmentWithWrongCast,
81+
eq(1),
82+
{ result -> result.isException<ArrayStoreException>() },
83+
coverage = AtLeast(87) // TODO: investigate
84+
)
85+
}
86+
87+
@Test
88+
fun testCheckGenericAssignmentWithExtendsSubtype() {
89+
checkWithException(
90+
ArrayStoreExceptionExamples::checkGenericAssignmentWithExtendsSubtype,
91+
eq(1),
92+
{ result -> result.isSuccess }
93+
)
94+
}
95+
96+
@Test
97+
fun testCheckGenericAssignmentWithExtendsUnrelated() {
98+
checkWithException(
99+
ArrayStoreExceptionExamples::checkGenericAssignmentWithExtendsUnrelated,
100+
eq(1),
101+
{ result -> result.isException<ArrayStoreException>() },
102+
coverage = AtLeast(87) // TODO: investigate
103+
)
104+
}
105+
106+
@Test
107+
fun testCheckObjectAssignment() {
108+
checkWithException(
109+
ArrayStoreExceptionExamples::checkObjectAssignment,
110+
eq(1),
111+
{ result -> result.isSuccess }
112+
)
113+
}
114+
115+
// Should this be allowed at all?
116+
@Test
117+
fun testCheckWrongAssignmentOfItself() {
118+
checkWithException(
119+
ArrayStoreExceptionExamples::checkWrongAssignmentOfItself,
120+
eq(1),
121+
{ result -> result.isException<ArrayStoreException>() },
122+
coverage = AtLeast(87)
123+
)
124+
}
125+
126+
@Test
127+
fun testCheckGoodAssignmentOfItself() {
128+
checkWithException(
129+
ArrayStoreExceptionExamples::checkGoodAssignmentOfItself,
130+
eq(1),
131+
{ result -> result.isSuccess }
132+
)
133+
}
134+
135+
@Test
136+
fun testCheckAssignmentToObjectArray() {
137+
checkWithException(
138+
ArrayStoreExceptionExamples::checkAssignmentToObjectArray,
139+
eq(1),
140+
{ result -> result.isSuccess }
141+
)
142+
}
143+
144+
@Test
145+
fun testArrayCopyForIncompatiblePrimitiveTypes() {
146+
checkWithException(
147+
ArrayStoreExceptionExamples::arrayCopyForIncompatiblePrimitiveTypes,
148+
eq(3),
149+
{ data, result -> data == null && result.isSuccess && result.getOrNull() == null },
150+
{ data, result -> data != null && data.isEmpty() && result.isSuccess && result.getOrNull()?.size == 0 },
151+
{ data, result -> data != null && data.isNotEmpty() && result.isException<ArrayStoreException>() }
152+
)
153+
}
154+
155+
@Test
156+
fun testFill2DPrimitiveArray() {
157+
checkWithException(
158+
ArrayStoreExceptionExamples::fill2DPrimitiveArray,
159+
eq(1),
160+
{ result -> result.isSuccess }
161+
)
162+
}
163+
164+
@Test
165+
fun testFillObjectArrayWithList() {
166+
check(
167+
ArrayStoreExceptionExamples::fillObjectArrayWithList,
168+
eq(2),
169+
{ list, result -> list != null && result != null && result[0] != null },
170+
{ list, result -> list == null && result == null }
171+
)
172+
}
173+
174+
@Test
175+
fun testFillWithTreeSet() {
176+
check(
177+
ArrayStoreExceptionExamples::fillWithTreeSet,
178+
eq(2),
179+
{ treeSet, result -> treeSet != null && result != null && result[0] != null },
180+
{ treeSet, result -> treeSet == null && result == null }
181+
)
182+
}
183+
184+
@Test
185+
fun testFillSomeInterfaceArrayWithSomeInterface() {
186+
check(
187+
ArrayStoreExceptionExamples::fillSomeInterfaceArrayWithSomeInterface,
188+
eq(2),
189+
{ impl, result -> impl == null && result == null },
190+
{ impl, result -> impl != null && result != null && result[0] != null }
191+
)
192+
}
193+
194+
@Test
195+
@Disabled("TODO: Not null path is not found, need to investigate")
196+
fun testFillObjectArrayWithSomeInterface() {
197+
check(
198+
ArrayStoreExceptionExamples::fillObjectArrayWithSomeInterface,
199+
eq(2),
200+
{ impl, result -> impl == null && result == null },
201+
{ impl, result -> impl != null && result != null && result[0] != null }
202+
)
203+
}
204+
205+
@Test
206+
fun testFillWithSomeImplementation() {
207+
check(
208+
ArrayStoreExceptionExamples::fillWithSomeImplementation,
209+
eq(2),
210+
{ impl, result -> impl == null && result == null },
211+
{ impl, result -> impl != null && result != null && result[0] != null }
212+
)
213+
}
214+
}

‎utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
package org.utbot.engine
22

3+
import org.utbot.common.WorkaroundReason
4+
import org.utbot.common.workaround
35
import org.utbot.engine.TypeRegistry.Companion.objectTypeStorage
46
import org.utbot.engine.pc.UtAddrExpression
57
import org.utbot.engine.pc.UtBoolExpression
@@ -11,6 +13,7 @@ import org.utbot.engine.pc.mkOr
1113
import org.utbot.engine.symbolic.*
1214
import org.utbot.framework.plugin.api.FieldId
1315
import org.utbot.framework.plugin.api.UtInstrumentation
16+
import soot.RefType
1417
import java.util.Objects
1518
import soot.Scene
1619
import soot.SootMethod

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

Lines changed: 52 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -65,9 +65,6 @@ import org.utbot.engine.pc.mkNot
6565
import org.utbot.engine.pc.mkOr
6666
import org.utbot.engine.pc.select
6767
import org.utbot.engine.pc.store
68-
import org.utbot.engine.symbolic.HardConstraint
69-
import org.utbot.engine.symbolic.SoftConstraint
70-
import org.utbot.engine.symbolic.Assumption
7168
import org.utbot.engine.symbolic.emptyAssumption
7269
import org.utbot.engine.symbolic.emptyHardConstraint
7370
import org.utbot.engine.symbolic.emptySoftConstraint
@@ -767,6 +764,57 @@ class Traverser(
767764
}
768765
}
769766

767+
/**
768+
* Check for [ArrayStoreException] when an array element is assigned
769+
*
770+
* @param arrayInstance Symbolic value corresponding to the array being updated
771+
* @param value Symbolic value corresponding to the right side of the assignment
772+
*/
773+
private fun TraversalContext.arrayStoreExceptionCheck(arrayInstance: SymbolicValue, value: SymbolicValue) {
774+
require(arrayInstance is ArrayValue)
775+
val valueType = value.type
776+
val valueBaseType = valueType.baseType
777+
val arrayElementType = arrayInstance.type.elementType
778+
779+
// We should check for [ArrayStoreException] only for reference types.
780+
// * For arrays of primitive types, incorrect assignment is prevented as compile time.
781+
// * When assigning primitive literals (e.g., `1`) to arrays of corresponding boxed classes (`Integer`),
782+
// the conversion to the reference type is automatic.
783+
// * [System.arraycopy] and similar functions that can throw [ArrayStoreException] accept [Object] arrays
784+
// as arguments, so array elements are references.
785+
786+
if (valueBaseType is RefType) {
787+
val arrayElementTypeStorage = typeResolver.constructTypeStorage(arrayElementType, useConcreteType = false)
788+
789+
// Generate ASE only if [value] is not a subtype of the type of array elements
790+
val isExpression = typeRegistry.typeConstraint(value.addr, arrayElementTypeStorage).isConstraint()
791+
val notIsExpression = mkNot(isExpression)
792+
793+
// `null` is compatible with any reference type, so we should not throw ASE when `null` is assigned
794+
val nullEqualityConstraint = addrEq(value.addr, nullObjectAddr)
795+
val notNull = mkNot(nullEqualityConstraint)
796+
797+
// Currently the negation of [UtIsExpression] seems to work incorrectly for [java.lang.Object]:
798+
// https://github.com/UnitTestBot/UTBotJava/issues/1007
799+
800+
// It is related to [org.utbot.engine.pc.Z3TranslatorVisitor.filterInappropriateTypes] that removes
801+
// internal engine classes for [java.lang.Object] type storage, and this logic is not fully
802+
// consistent with the negation.
803+
804+
// Here we have a specific test for [java.lang.Object] as the type of array elements:
805+
// any reference type may be assigned to elements of an Object array, so we should not generate
806+
// [ArrayStoreException] in these cases.
807+
808+
// TODO: remove enclosing `if` when [UtIfExpression] negation is fixed
809+
if (!arrayElementType.isJavaLangObject()) {
810+
implicitlyThrowException(ArrayStoreException(), setOf(notIsExpression, notNull))
811+
}
812+
813+
// If ASE is not thrown, we know that either the value is null, or it has a compatible type
814+
queuedSymbolicStateUpdates += mkOr(isExpression, nullEqualityConstraint).asHardConstraint()
815+
}
816+
}
817+
770818
/**
771819
* Traverses left part of assignment i.e. where to store resolved value.
772820
*/
@@ -782,12 +830,11 @@ class Traverser(
782830

783831
queuedSymbolicStateUpdates += Le(length, softMaxArraySize).asHardConstraint() // TODO: fix big array length
784832

785-
// TODO array store exception
833+
arrayStoreExceptionCheck(arrayInstance, value)
786834

787835
// add constraint for possible array type
788836
val valueType = value.type
789837
val valueBaseType = valueType.baseType
790-
791838
if (valueBaseType is RefType) {
792839
val valueTypeAncestors = typeResolver.findOrConstructAncestorsIncludingTypes(valueBaseType)
793840
val valuePossibleBaseTypes = value.typeStorage.possibleConcreteTypes.map { it.baseType }

0 commit comments

Comments
 (0)