Skip to content

Commit 268b0c3

Browse files
CaelmBleiddCaelmBleidd
committed
Map don't work without concrete
Fixes: * aliasing between nested arrays of UtHashMap and its fields * unsat for get operation from Map
1 parent 6ce8761 commit 268b0c3

File tree

6 files changed

+202
-40
lines changed

6 files changed

+202
-40
lines changed

‎utbot-framework-test/src/test/kotlin/org/utbot/examples/collections/MapsPart1Test.kt

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ import org.junit.jupiter.api.Test
1212
import org.utbot.testcheckers.eq
1313
import org.utbot.testcheckers.ge
1414
import org.utbot.testcheckers.withPushingStateFromPathSelectorForConcrete
15+
import org.utbot.testcheckers.withoutConcrete
1516
import org.utbot.testcheckers.withoutMinimization
1617
import org.utbot.tests.infrastructure.CodeGeneration
1718

@@ -84,6 +85,44 @@ internal class MapsPart1Test : UtValueTestCaseChecker(
8485
)
8586
}
8687

88+
@Test
89+
fun testMapPutAndGet() {
90+
withoutConcrete {
91+
check(
92+
Maps::mapPutAndGet,
93+
eq(1),
94+
{ r -> r == 3 }
95+
)
96+
}
97+
}
98+
99+
@Test
100+
fun testPutInMapFromParameters() {
101+
withoutConcrete {
102+
check(
103+
Maps::putInMapFromParameters,
104+
ignoreExecutionsNumber,
105+
{ values, _ -> values == null },
106+
{ values, r -> 1 in values.keys && r == 3 },
107+
{ values, r -> 1 !in values.keys && r == 3 },
108+
)
109+
}
110+
}
111+
112+
// This test doesn't check anything specific, but the code from MUT
113+
// caused errors with NPE as results while debugging `testPutInMapFromParameters`.
114+
@Test
115+
fun testContainsKeyAndPuts() {
116+
withoutConcrete {
117+
check(
118+
Maps::containsKeyAndPuts,
119+
ignoreExecutionsNumber,
120+
{ values, _ -> values == null },
121+
{ values, r -> 1 !in values.keys && r == 3 },
122+
)
123+
}
124+
}
125+
87126
@Test
88127
fun testFindAllChars() {
89128
check(
@@ -324,4 +363,25 @@ internal class MapsPart1Test : UtValueTestCaseChecker(
324363
coverage = DoNotCalculate
325364
)
326365
}
366+
367+
@Test
368+
fun testCreateMapWithString() {
369+
withoutConcrete {
370+
check(
371+
Maps::createMapWithString,
372+
eq(1),
373+
{ r -> r!!.isEmpty() }
374+
)
375+
}
376+
}
377+
@Test
378+
fun testCreateMapWithEnum() {
379+
withoutConcrete {
380+
check(
381+
Maps::createMapWithEnum,
382+
eq(1),
383+
{ r -> r != null && r.size == 2 && r[Maps.WorkDays.Monday] == 112 && r[Maps.WorkDays.Friday] == 567 }
384+
)
385+
}
386+
}
327387
}

‎utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtHashMap.java

Lines changed: 16 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,12 @@ void preconditionCheck() {
102102
parameter(keys);
103103
parameter(keys.storage);
104104

105+
// Following three instructions are required to avoid possible aliasing
106+
// between nested arrays
107+
assume(keys.storage != values.storage);
108+
assume(keys.storage != values.touched);
109+
assume(values.storage != values.touched);
110+
105111
assume(values.size == keys.end);
106112
assume(values.touched.length == keys.end);
107113
doesntThrow();
@@ -205,11 +211,18 @@ public V put(K key, V value) {
205211
if (index == -1) {
206212
oldValue = null;
207213
keys.set(keys.end++, key);
214+
values.store(key, value);
208215
} else {
209-
// newKey equals to oldKey so we can use it instead
210-
oldValue = values.select(key);
216+
K oldKey = keys.get(index);
217+
oldValue = values.select(oldKey);
218+
values.store(oldKey, value);
211219
}
212-
values.store(key, value);
220+
221+
// Avoid optimization here. Despite the fact that old key is equal
222+
// to a new one in case of `index != -1`, it is important to have
223+
// this connection between `index`, `key`, `oldKey` and `value`.
224+
// So, do not rewrite it with `values.store(key, value)` extracted from the if instruction
225+
213226
return oldValue;
214227
}
215228

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

Lines changed: 53 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -215,13 +215,17 @@ class RangeModifiableUnlimitedArrayWrapper : WrapperInterface {
215215
createArray(addr, valueType, useConcreteType = false)
216216
}
217217

218-
listOf(
219-
MethodResult(
220-
SymbolicSuccess(resultObject),
221-
typeRegistry.typeConstraintToGenericTypeParameter(addr, wrapper.addr, i = TYPE_PARAMETER_INDEX)
222-
.asHardConstraint()
223-
)
224-
)
218+
val typeIndex = wrapper.asWrapperOrNull?.getOperationTypeIndex
219+
?: error("Wrapper was expected, got $wrapper")
220+
val typeConstraint = typeRegistry.typeConstraintToGenericTypeParameter(
221+
addr,
222+
wrapper.addr,
223+
i = typeIndex
224+
).asHardConstraint()
225+
226+
val methodResult = MethodResult(SymbolicSuccess(resultObject), typeConstraint)
227+
228+
listOf(methodResult)
225229
}
226230

227231
@Suppress("UNUSED_PARAMETER")
@@ -418,16 +422,17 @@ class AssociativeArrayWrapper : WrapperInterface {
418422
val addr = UtAddrExpression(value)
419423
val resultObject = createObject(addr, OBJECT_TYPE, useConcreteType = false)
420424

421-
listOf(
422-
MethodResult(
423-
SymbolicSuccess(resultObject),
424-
typeRegistry.typeConstraintToGenericTypeParameter(
425-
addr,
426-
wrapper.addr,
427-
TYPE_PARAMETER_INDEX
428-
).asHardConstraint()
429-
)
430-
)
425+
val typeIndex = wrapper.asWrapperOrNull?.selectOperationTypeIndex
426+
?: error("Wrapper was expected, got $wrapper")
427+
val hardConstraints = typeRegistry.typeConstraintToGenericTypeParameter(
428+
addr,
429+
wrapper.addr,
430+
typeIndex
431+
).asHardConstraint()
432+
433+
val methodResult = MethodResult(SymbolicSuccess(resultObject), hardConstraints)
434+
435+
listOf(methodResult)
431436
}
432437

433438
@Suppress("UNUSED_PARAMETER")
@@ -440,21 +445,31 @@ class AssociativeArrayWrapper : WrapperInterface {
440445
with(traverser) {
441446
val storageValue = getStorageArrayExpression(wrapper).store(parameters[0].addr, parameters[1].addr)
442447
val sizeValue = getIntFieldValue(wrapper, sizeField)
448+
449+
// it is the reason why it's important to use an `oldKey` in `UtHashMap.put` method.
450+
// We navigate in the associative array using only this old address, not a new one.
443451
val touchedValue = getTouchedArrayExpression(wrapper).store(sizeValue, parameters[0].addr)
444-
listOf(
445-
MethodResult(
446-
SymbolicSuccess(voidValue),
447-
memoryUpdates = arrayUpdateWithValue(
448-
getStorageArrayField(wrapper.addr).addr,
449-
OBJECT_TYPE.arrayType,
450-
storageValue
451-
) + arrayUpdateWithValue(
452-
getTouchedArrayField(wrapper.addr).addr,
453-
OBJECT_TYPE.arrayType,
454-
touchedValue,
455-
) + objectUpdate(wrapper, sizeField, Add(sizeValue.toIntValue(), 1.toPrimitiveValue()))
456-
)
452+
val storageArrayAddr = getStorageArrayField(wrapper.addr).addr
453+
val touchedArrayFieldAddr = getTouchedArrayField(wrapper.addr).addr
454+
455+
val storageArrayUpdate = arrayUpdateWithValue(
456+
storageArrayAddr,
457+
OBJECT_TYPE.arrayType,
458+
storageValue
459+
)
460+
461+
val touchedArrayUpdate = arrayUpdateWithValue(
462+
touchedArrayFieldAddr,
463+
OBJECT_TYPE.arrayType,
464+
touchedValue,
457465
)
466+
467+
val sizeUpdate = objectUpdate(wrapper, sizeField, Add(sizeValue.toIntValue(), 1.toPrimitiveValue()))
468+
469+
val memoryUpdates = storageArrayUpdate + touchedArrayUpdate + sizeUpdate
470+
val methodResult = MethodResult(SymbolicSuccess(voidValue), memoryUpdates = memoryUpdates)
471+
472+
listOf(methodResult)
458473
}
459474

460475
override val wrappedMethods: Map<String, MethodSymbolicImplementation> = mapOf(
@@ -480,7 +495,7 @@ class AssociativeArrayWrapper : WrapperInterface {
480495
// construct model values of an array
481496
val touchedValues = UtArrayModel(
482497
resolver.holder.concreteAddr(UtAddrExpression(touchedArrayAddr)),
483-
objectClassId,
498+
objectArrayClassId,
484499
sizeValue,
485500
UtNullModel(objectClassId),
486501
stores = (0 until sizeValue).associateWithTo(mutableMapOf()) { i ->
@@ -504,7 +519,7 @@ class AssociativeArrayWrapper : WrapperInterface {
504519

505520
val storageValues = UtArrayModel(
506521
resolver.holder.concreteAddr(UtAddrExpression(storageArrayAddr)),
507-
objectClassId,
522+
objectArrayClassId,
508523
sizeValue,
509524
UtNullModel(objectClassId),
510525
stores = (0 until sizeValue).associateTo(mutableMapOf()) { i ->
@@ -518,10 +533,12 @@ class AssociativeArrayWrapper : WrapperInterface {
518533
)
519534
})
520535

521-
val model = UtCompositeModel(resolver.holder.concreteAddr(wrapper.addr), associativeArrayId, false)
536+
val model = UtCompositeModel(resolver.holder.concreteAddr(wrapper.addr), associativeArrayId, isMock = false)
537+
522538
model.fields[sizeField.fieldId] = UtPrimitiveModel(sizeValue)
523539
model.fields[touchedField.fieldId] = touchedValues
524540
model.fields[storageField.fieldId] = storageValues
541+
525542
return model
526543
}
527544

@@ -537,7 +554,7 @@ class AssociativeArrayWrapper : WrapperInterface {
537554
private fun Traverser.getStorageArrayExpression(
538555
wrapper: ObjectValue
539556
): UtExpression = selectArrayExpressionFromMemory(getStorageArrayField(wrapper.addr))
540-
}
541557

542-
// Arrays and lists have the only type parameter with index zero
543-
private const val TYPE_PARAMETER_INDEX = 0
558+
override val selectOperationTypeIndex: Int
559+
get() = 1
560+
}

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -244,6 +244,21 @@ interface WrapperInterface {
244244
}
245245

246246
fun value(resolver: Resolver, wrapper: ObjectValue): UtModel
247+
248+
/**
249+
* It is an index for type parameter corresponding to the result
250+
* value of `select` operation. For example, for arrays and lists it's zero,
251+
* for associative array it's one.
252+
*/
253+
open val selectOperationTypeIndex: Int
254+
get() = 0
255+
256+
/**
257+
* Similar to [selectOperationTypeIndex], it is responsible for type index
258+
* of the returning value from `get` operation
259+
*/
260+
open val getOperationTypeIndex: Int
261+
get() = 0
247262
}
248263

249264
// TODO: perhaps we have to have wrapper around concrete value here

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -455,7 +455,7 @@ class UtIsGenericTypeExpression(
455455
override fun <TResult> accept(visitor: UtExpressionVisitor<TResult>): TResult = visitor.visit(this)
456456

457457
override fun toString(): String {
458-
return "(generic-is $addr $baseAddr<\$$parameterTypeIndex>)"
458+
return "(generic-is $addr baseAddr<ParamTypeIndex>: $baseAddr<\$$parameterTypeIndex>)"
459459
}
460460

461461
override fun equals(other: Any?): Boolean {

‎utbot-sample/src/main/java/org/utbot/examples/collections/Maps.java

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

3+
import org.utbot.api.mock.UtMock;
4+
35
import java.util.ArrayList;
46
import java.util.HashMap;
57
import java.util.LinkedHashMap;
@@ -25,6 +27,36 @@ String mapToString(long startTime, int pageSize, int pageNum) {
2527
return params.toString();
2628
}
2729

30+
@SuppressWarnings("OverwrittenKey")
31+
Integer mapPutAndGet() {
32+
Map<Long, Integer> values = new HashMap<>();
33+
34+
values.put(1L, 2);
35+
values.put(1L, 3);
36+
37+
return values.get(1L);
38+
}
39+
40+
@SuppressWarnings("OverwrittenKey")
41+
Integer putInMapFromParameters(Map<Long, Integer> values) {
42+
values.put(1L, 2);
43+
values.put(1L, 3);
44+
45+
return values.get(1L);
46+
}
47+
48+
@SuppressWarnings("OverwrittenKey")
49+
Integer containsKeyAndPuts(Map<Long, Integer> values) {
50+
UtMock.assume(!values.containsKey(1L));
51+
52+
values.put(1L, 2);
53+
values.put(1L, 3);
54+
55+
UtMock.assume(values.get(1L).equals(3));
56+
57+
return values.get(1L);
58+
}
59+
2860
Map<Character, Integer> countChars(String s) {
2961
Map<Character, Integer> map = new LinkedHashMap<>();
3062
for (int i = 0; i < s.length(); i++) {
@@ -261,4 +293,29 @@ public List<String> mapOperator(Map<String, String> map) {
261293
return new ArrayList<>(map.values());
262294
}
263295
}
296+
297+
public Map<String, Integer> createMapWithString() {
298+
Map<String, Integer> map = new HashMap<>();
299+
map.put("tuesday", 354);
300+
map.remove("tuesday");
301+
302+
return map;
303+
}
304+
public Map<WorkDays, Integer> createMapWithEnum() {
305+
Map<WorkDays, Integer> map = new HashMap<>();
306+
map.put(WorkDays.Monday, 112);
307+
map.put(WorkDays.Tuesday, 354);
308+
map.put(WorkDays.Friday, 567);
309+
map.remove(WorkDays.Tuesday);
310+
311+
return map;
312+
}
313+
314+
public enum WorkDays {
315+
Monday,
316+
Tuesday,
317+
Wednesday,
318+
Thursday,
319+
Friday
320+
}
264321
}

0 commit comments

Comments
 (0)