Skip to content

Commit 84ca477

Browse files
dtimdtim
committed
Check for ArrayStoreException on array update
TODO: check primitive types
1 parent b98f12e commit 84ca477

File tree

3 files changed

+307
-5
lines changed

3 files changed

+307
-5
lines changed

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

Lines changed: 162 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,162 @@
1+
package org.utbot.examples.arrays
2+
3+
import org.junit.jupiter.api.Test
4+
import org.utbot.framework.plugin.api.CodegenLanguage
5+
import org.utbot.testcheckers.eq
6+
import org.utbot.tests.infrastructure.AtLeast
7+
import org.utbot.tests.infrastructure.CodeGeneration
8+
import org.utbot.tests.infrastructure.UtValueTestCaseChecker
9+
import org.utbot.tests.infrastructure.isException
10+
11+
class ArrayStoreExceptionExamplesTest : UtValueTestCaseChecker(
12+
testClass = ArrayStoreExceptionExamples::class,
13+
languagePipelines = listOf(
14+
CodeGenerationLanguageLastStage(CodegenLanguage.JAVA),
15+
// Type inference errors in generated Kotlin code (Number)
16+
CodeGenerationLanguageLastStage(CodegenLanguage.KOTLIN, CodeGeneration)
17+
)
18+
) {
19+
@Test
20+
fun testCorrectAssignmentSamePrimitiveType() {
21+
checkWithException(
22+
ArrayStoreExceptionExamples::correctAssignmentSamePrimitiveType,
23+
eq(3),
24+
{ data, result -> result.isSuccess && result.getOrNull() == data?.isNotEmpty() }
25+
)
26+
}
27+
28+
@Test
29+
fun testCorrectAssignmentIntToIntegerArray() {
30+
checkWithException(
31+
ArrayStoreExceptionExamples::correctAssignmentIntToIntegerArray,
32+
eq(3),
33+
{ data, result -> result.isSuccess && result.getOrNull() == data?.isNotEmpty() }
34+
)
35+
}
36+
37+
@Test
38+
fun testCorrectAssignmentSubtype() {
39+
checkWithException(
40+
ArrayStoreExceptionExamples::correctAssignmentSubtype,
41+
eq(3),
42+
{ data, result -> result.isSuccess && result.getOrNull() == data?.isNotEmpty() }
43+
)
44+
}
45+
46+
@Test
47+
fun testCorrectAssignmentToObjectArray() {
48+
checkWithException(
49+
ArrayStoreExceptionExamples::correctAssignmentToObjectArray,
50+
eq(3),
51+
{ data, result -> result.isSuccess && result.getOrNull() == data?.isNotEmpty() }
52+
)
53+
}
54+
55+
@Test
56+
fun testWrongAssignmentUnrelatedType() {
57+
checkWithException(
58+
ArrayStoreExceptionExamples::wrongAssignmentUnrelatedType,
59+
eq(3),
60+
{ data, result -> data == null && result.isSuccess },
61+
{ data, result -> data.isEmpty() && result.isSuccess },
62+
{ data, result -> data.isNotEmpty() && result.isException<ArrayStoreException>() },
63+
coverage = AtLeast(91) // TODO: investigate
64+
)
65+
}
66+
67+
@Test
68+
fun testCheckGenericAssignmentWithCorrectCast() {
69+
checkWithException(
70+
ArrayStoreExceptionExamples::checkGenericAssignmentWithCorrectCast,
71+
eq(1),
72+
{ result -> result.isSuccess }
73+
)
74+
}
75+
76+
@Test
77+
fun testCheckGenericAssignmentWithWrongCast() {
78+
checkWithException(
79+
ArrayStoreExceptionExamples::checkGenericAssignmentWithWrongCast,
80+
eq(1),
81+
{ result -> result.isException<ArrayStoreException>() },
82+
coverage = AtLeast(87) // TODO: investigate
83+
)
84+
}
85+
86+
@Test
87+
fun testCheckGenericAssignmentWithExtendsSubtype() {
88+
checkWithException(
89+
ArrayStoreExceptionExamples::checkGenericAssignmentWithExtendsSubtype,
90+
eq(1),
91+
{ result -> result.isSuccess }
92+
)
93+
}
94+
95+
@Test
96+
fun testCheckGenericAssignmentWithExtendsUnrelated() {
97+
checkWithException(
98+
ArrayStoreExceptionExamples::checkGenericAssignmentWithExtendsUnrelated,
99+
eq(1),
100+
{ result -> result.isException<ArrayStoreException>() },
101+
coverage = AtLeast(87) // TODO: investigate
102+
)
103+
}
104+
105+
@Test
106+
fun testCheckObjectAssignment() {
107+
checkWithException(
108+
ArrayStoreExceptionExamples::checkObjectAssignment,
109+
eq(1),
110+
{ result -> result.isSuccess }
111+
)
112+
}
113+
114+
// Should this be allowed at all?
115+
@Test
116+
fun testCheckWrongAssignmentOfItself() {
117+
checkWithException(
118+
ArrayStoreExceptionExamples::checkWrongAssignmentOfItself,
119+
eq(1),
120+
{ result -> result.isException<ArrayStoreException>() },
121+
coverage = AtLeast(87)
122+
)
123+
}
124+
125+
@Test
126+
fun testCheckGoodAssignmentOfItself() {
127+
checkWithException(
128+
ArrayStoreExceptionExamples::checkGoodAssignmentOfItself,
129+
eq(1),
130+
{ result -> result.isSuccess }
131+
)
132+
}
133+
134+
@Test
135+
fun testCheckAssignmentToObjectArray() {
136+
checkWithException(
137+
ArrayStoreExceptionExamples::checkAssignmentToObjectArray,
138+
eq(1),
139+
{ result -> result.isSuccess }
140+
)
141+
}
142+
143+
@Test
144+
fun testArrayCopyForIncompatiblePrimitiveTypes() {
145+
checkWithException(
146+
ArrayStoreExceptionExamples::arrayCopyForIncompatiblePrimitiveTypes,
147+
eq(3),
148+
{ data, result -> data == null && result.isSuccess && result.getOrNull() == null },
149+
{ data, result -> data != null && data.isEmpty() && result.isSuccess && result.getOrNull()?.size == 0 },
150+
{ data, result -> data != null && data.isNotEmpty() && result.isException<ArrayStoreException>() }
151+
)
152+
}
153+
154+
@Test
155+
fun testFill2DPrimitiveArray() {
156+
checkWithException(
157+
ArrayStoreExceptionExamples::fill2DPrimitiveArray,
158+
eq(1),
159+
{ result -> result.isSuccess }
160+
)
161+
}
162+
}

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

Lines changed: 29 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,34 @@ 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 valueBaseType = value.type.baseType
776+
val arrayElementType = arrayInstance.type.elementType
777+
val arrayTypeStorage = typeResolver.constructTypeStorage(arrayElementType, useConcreteType = false)
778+
779+
if (valueBaseType is RefType) {
780+
// Generate ASE only if [value] is not a subtype of the type of array elements
781+
val isExpression = typeRegistry.typeConstraint(value.addr, arrayTypeStorage).isConstraint()
782+
val notIsExpression = mkNot(isExpression)
783+
784+
// `null` is compatible with any reference type, so we should not throw ASE when `null` is assigned
785+
val nullEqualityConstraint = addrEq(value.addr, nullObjectAddr)
786+
val notNull = mkNot(nullEqualityConstraint)
787+
788+
implicitlyThrowException(ArrayStoreException(), setOf(notIsExpression, notNull))
789+
790+
// If ASE is not thrown, we know that either the value is null, or it has a compatible type
791+
queuedSymbolicStateUpdates += mkOr(isExpression, nullEqualityConstraint).asHardConstraint()
792+
}
793+
}
794+
770795
/**
771796
* Traverses left part of assignment i.e. where to store resolved value.
772797
*/
@@ -782,12 +807,11 @@ class Traverser(
782807

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

785-
// TODO array store exception
810+
arrayStoreExceptionCheck(arrayInstance, value)
786811

787812
// add constraint for possible array type
788813
val valueType = value.type
789814
val valueBaseType = valueType.baseType
790-
791815
if (valueBaseType is RefType) {
792816
val valueTypeAncestors = typeResolver.findOrConstructAncestorsIncludingTypes(valueBaseType)
793817
val valuePossibleBaseTypes = value.typeStorage.possibleConcreteTypes.map { it.baseType }

‎utbot-sample/src/main/java/org/utbot/examples/arrays/ArrayStoreExceptionExamples.java

Lines changed: 116 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
package org.utbot.examples.arrays;
2+
3+
import java.util.ArrayList;
4+
5+
public class ArrayStoreExceptionExamples {
6+
7+
public boolean correctAssignmentSamePrimitiveType(int[] data) {
8+
if (data == null || data.length == 0) return false;
9+
data[0] = 1;
10+
return true;
11+
}
12+
13+
public boolean correctAssignmentIntToIntegerArray(Integer[] data) {
14+
if (data == null || data.length == 0) return false;
15+
data[0] = 1;
16+
return true;
17+
}
18+
19+
public boolean correctAssignmentSubtype(Number[] data) {
20+
if (data == null || data.length == 0) return false;
21+
data[0] = 15;
22+
return true;
23+
}
24+
25+
public boolean correctAssignmentToObjectArray(Object[] data) {
26+
if (data == null || data.length < 2) return false;
27+
data[0] = 1;
28+
data[1] = new ArrayList<Integer>();
29+
return true;
30+
}
31+
32+
public void wrongAssignmentUnrelatedType(Integer[] data) {
33+
if (data == null || data.length == 0) return;
34+
((Object[]) data)[0] = "x";
35+
}
36+
37+
public void wrongAssignmentSupertype(Integer[] data) {
38+
if (data == null || data.length == 0) return;
39+
Number x = 1.2;
40+
((Number[]) data)[0] = x;
41+
}
42+
43+
public void checkGenericAssignmentWithCorrectCast() {
44+
Number[] data = new Number[3];
45+
genericAssignmentWithCast(data, 5);
46+
}
47+
48+
public void checkGenericAssignmentWithWrongCast() {
49+
Number[] data = new Number[3];
50+
genericAssignmentWithCast(data, "x");
51+
}
52+
53+
public void checkGenericAssignmentWithExtendsSubtype() {
54+
Number[] data = new Number[3];
55+
genericAssignmentWithExtends(data, 7);
56+
}
57+
58+
public void checkGenericAssignmentWithExtendsUnrelated() {
59+
Number[] data = new Number[3];
60+
genericAssignmentWithExtends(data, "x");
61+
}
62+
63+
public void checkObjectAssignment() {
64+
Object[] data = new Object[3];
65+
data[0] = "x";
66+
}
67+
68+
public void checkAssignmentToObjectArray() {
69+
Object[] data = new Object[3];
70+
data[0] = 1;
71+
data[1] = "a";
72+
data[2] = data;
73+
}
74+
75+
public void checkWrongAssignmentOfItself() {
76+
Number[] data = new Number[2];
77+
genericAssignmentWithCast(data, data);
78+
}
79+
80+
public void checkGoodAssignmentOfItself() {
81+
Object[] data = new Object[2];
82+
genericAssignmentWithCast(data, data);
83+
}
84+
85+
public int[] arrayCopyForIncompatiblePrimitiveTypes(long[] data) {
86+
if (data == null)
87+
return null;
88+
89+
int[] result = new int[data.length];
90+
if (data.length != 0) {
91+
System.arraycopy(data, 0, result, 0, data.length);
92+
}
93+
94+
return result;
95+
}
96+
97+
public int[][] fill2DPrimitiveArray() {
98+
int[][] data = new int[2][3];
99+
for (int i = 0; i < 2; i++) {
100+
for (int j = 0; j < 3; j++) {
101+
data[i][j] = i * 3 + j;
102+
}
103+
}
104+
return data;
105+
}
106+
107+
private <T, E> void genericAssignmentWithCast(T[] data, E element) {
108+
if (data == null || data.length == 0) return;
109+
data[0] = (T) element;
110+
}
111+
112+
private <T, E extends T> void genericAssignmentWithExtends(T[] data, E element) {
113+
if (data == null || data.length == 0) return;
114+
data[0] = element;
115+
}
116+
}

0 commit comments

Comments
 (0)