Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
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
Next Next commit
Map don't work without concrete
Fixes:
* aliasing between nested arrays of UtHashMap and its fields
* unsat for get operation from Map
  • Loading branch information
CaelmBleidd committed Oct 25, 2022
commit 3a6f06f55e8bf68ef7b0508967bbff944446706e
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ import org.junit.jupiter.api.Test
import org.utbot.testcheckers.eq
import org.utbot.testcheckers.ge
import org.utbot.testcheckers.withPushingStateFromPathSelectorForConcrete
import org.utbot.testcheckers.withoutConcrete
import org.utbot.testcheckers.withoutMinimization
import org.utbot.tests.infrastructure.CodeGeneration

Expand Down Expand Up @@ -84,6 +85,45 @@ internal class MapsPart1Test : UtValueTestCaseChecker(
)
}

@Test
fun testMapPutAndGet() {
withoutConcrete {
check(
Maps::mapPutAndGet,
eq(1),
{ r -> r == 3 }
)
}
}

@Test
fun testPutInMapFromParameters() {
withoutConcrete {
check(
Maps::putInMapFromParameters,
ignoreExecutionsNumber,
{ values, _ -> values == null },
{ values, r -> 1 in values.keys && r == 3 },
{ values, r -> 1 !in values.keys && r == 3 },
)
}
}

// This test doesn't check anything specific, but the code from MUT
// caused errors with NPE as results while debugging `testPutInMapFromParameters`.
@Test
fun testContainsKeyAndPuts() {
withoutConcrete {
check(
Maps::containsKeyAndPuts,
eq(2),
{ values, _ -> values == null },
{ values, r -> 1 !in values.keys && r == 3 },
coverage = DoNotCalculate
)
}
}

@Test
fun testFindAllChars() {
check(
Expand Down Expand Up @@ -324,4 +364,25 @@ internal class MapsPart1Test : UtValueTestCaseChecker(
coverage = DoNotCalculate
)
}

@Test
fun testCreateMapWithString() {
withoutConcrete {
check(
Maps::createMapWithString,
eq(1),
{ r -> r!!.isEmpty() }
)
}
}
@Test
fun testCreateMapWithEnum() {
withoutConcrete {
check(
Maps::createMapWithEnum,
eq(1),
{ r -> r != null && r.size == 2 && r[Maps.WorkDays.Monday] == 112 && r[Maps.WorkDays.Friday] == 567 }
)
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -102,6 +102,12 @@ void preconditionCheck() {
parameter(keys);
parameter(keys.storage);

// Following three instructions are required to avoid possible aliasing
// between nested arrays
assume(keys.storage != values.storage);
assume(keys.storage != values.touched);
assume(values.storage != values.touched);

assume(values.size == keys.end);
assume(values.touched.length == keys.end);
doesntThrow();
Expand Down Expand Up @@ -205,11 +211,18 @@ public V put(K key, V value) {
if (index == -1) {
oldValue = null;
keys.set(keys.end++, key);
values.store(key, value);
} else {
// newKey equals to oldKey so we can use it instead
oldValue = values.select(key);
K oldKey = keys.get(index);
oldValue = values.select(oldKey);
values.store(oldKey, value);
}
values.store(key, value);

// Avoid optimization here. Despite the fact that old key is equal
// to a new one in case of `index != -1`, it is important to have
// this connection between `index`, `key`, `oldKey` and `value`.
// So, do not rewrite it with `values.store(key, value)` extracted from the if instruction

return oldValue;
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -215,13 +215,17 @@ class RangeModifiableUnlimitedArrayWrapper : WrapperInterface {
createArray(addr, valueType, useConcreteType = false)
}

listOf(
MethodResult(
SymbolicSuccess(resultObject),
typeRegistry.typeConstraintToGenericTypeParameter(addr, wrapper.addr, i = TYPE_PARAMETER_INDEX)
.asHardConstraint()
)
)
val typeIndex = wrapper.asWrapperOrNull?.getOperationTypeIndex
?: error("Wrapper was expected, got $wrapper")
val typeConstraint = typeRegistry.typeConstraintToGenericTypeParameter(
addr,
wrapper.addr,
i = typeIndex
).asHardConstraint()

val methodResult = MethodResult(SymbolicSuccess(resultObject), typeConstraint)

listOf(methodResult)
}

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

listOf(
MethodResult(
SymbolicSuccess(resultObject),
typeRegistry.typeConstraintToGenericTypeParameter(
addr,
wrapper.addr,
TYPE_PARAMETER_INDEX
).asHardConstraint()
)
)
val typeIndex = wrapper.asWrapperOrNull?.selectOperationTypeIndex
?: error("Wrapper was expected, got $wrapper")
val hardConstraints = typeRegistry.typeConstraintToGenericTypeParameter(
addr,
wrapper.addr,
typeIndex
).asHardConstraint()

val methodResult = MethodResult(SymbolicSuccess(resultObject), hardConstraints)

listOf(methodResult)
}

@Suppress("UNUSED_PARAMETER")
Expand All @@ -440,21 +445,31 @@ class AssociativeArrayWrapper : WrapperInterface {
with(traverser) {
val storageValue = getStorageArrayExpression(wrapper).store(parameters[0].addr, parameters[1].addr)
val sizeValue = getIntFieldValue(wrapper, sizeField)

// it is the reason why it's important to use an `oldKey` in `UtHashMap.put` method.
// We navigate in the associative array using only this old address, not a new one.
val touchedValue = getTouchedArrayExpression(wrapper).store(sizeValue, parameters[0].addr)
listOf(
MethodResult(
SymbolicSuccess(voidValue),
memoryUpdates = arrayUpdateWithValue(
getStorageArrayField(wrapper.addr).addr,
OBJECT_TYPE.arrayType,
storageValue
) + arrayUpdateWithValue(
getTouchedArrayField(wrapper.addr).addr,
OBJECT_TYPE.arrayType,
touchedValue,
) + objectUpdate(wrapper, sizeField, Add(sizeValue.toIntValue(), 1.toPrimitiveValue()))
)
val storageArrayAddr = getStorageArrayField(wrapper.addr).addr
val touchedArrayFieldAddr = getTouchedArrayField(wrapper.addr).addr

val storageArrayUpdate = arrayUpdateWithValue(
storageArrayAddr,
OBJECT_TYPE.arrayType,
storageValue
)

val touchedArrayUpdate = arrayUpdateWithValue(
touchedArrayFieldAddr,
OBJECT_TYPE.arrayType,
touchedValue,
)

val sizeUpdate = objectUpdate(wrapper, sizeField, Add(sizeValue.toIntValue(), 1.toPrimitiveValue()))

val memoryUpdates = storageArrayUpdate + touchedArrayUpdate + sizeUpdate
val methodResult = MethodResult(SymbolicSuccess(voidValue), memoryUpdates = memoryUpdates)

listOf(methodResult)
}

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

val storageValues = UtArrayModel(
resolver.holder.concreteAddr(UtAddrExpression(storageArrayAddr)),
objectClassId,
objectArrayClassId,
sizeValue,
UtNullModel(objectClassId),
stores = (0 until sizeValue).associateTo(mutableMapOf()) { i ->
Expand All @@ -518,10 +533,12 @@ class AssociativeArrayWrapper : WrapperInterface {
)
})

val model = UtCompositeModel(resolver.holder.concreteAddr(wrapper.addr), associativeArrayId, false)
val model = UtCompositeModel(resolver.holder.concreteAddr(wrapper.addr), associativeArrayId, isMock = false)

model.fields[sizeField.fieldId] = UtPrimitiveModel(sizeValue)
model.fields[touchedField.fieldId] = touchedValues
model.fields[storageField.fieldId] = storageValues

return model
}

Expand All @@ -537,7 +554,7 @@ class AssociativeArrayWrapper : WrapperInterface {
private fun Traverser.getStorageArrayExpression(
wrapper: ObjectValue
): UtExpression = selectArrayExpressionFromMemory(getStorageArrayField(wrapper.addr))
}

// Arrays and lists have the only type parameter with index zero
private const val TYPE_PARAMETER_INDEX = 0
override val selectOperationTypeIndex: Int
get() = 1
}
15 changes: 15 additions & 0 deletions utbot-framework/src/main/kotlin/org/utbot/engine/ObjectWrappers.kt
Original file line number Diff line number Diff line change
Expand Up @@ -244,6 +244,21 @@ interface WrapperInterface {
}

fun value(resolver: Resolver, wrapper: ObjectValue): UtModel

/**
* It is an index for type parameter corresponding to the result
* value of `select` operation. For example, for arrays and lists it's zero,
* for associative array it's one.
*/
open val selectOperationTypeIndex: Int
get() = 0

/**
* Similar to [selectOperationTypeIndex], it is responsible for type index
* of the returning value from `get` operation
*/
open val getOperationTypeIndex: Int
get() = 0
}

// TODO: perhaps we have to have wrapper around concrete value here
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -455,7 +455,7 @@ class UtIsGenericTypeExpression(
override fun <TResult> accept(visitor: UtExpressionVisitor<TResult>): TResult = visitor.visit(this)

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

override fun equals(other: Any?): Boolean {
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
package org.utbot.examples.collections;

import org.utbot.api.mock.UtMock;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.LinkedHashMap;
Expand All @@ -25,6 +27,36 @@ String mapToString(long startTime, int pageSize, int pageNum) {
return params.toString();
}

@SuppressWarnings("OverwrittenKey")
Integer mapPutAndGet() {
Comment thread
CaelmBleidd marked this conversation as resolved.
Map<Long, Integer> values = new HashMap<>();

values.put(1L, 2);
values.put(1L, 3);

return values.get(1L);
}

@SuppressWarnings("OverwrittenKey")
Integer putInMapFromParameters(Map<Long, Integer> values) {
values.put(1L, 2);
values.put(1L, 3);

return values.get(1L);
}

@SuppressWarnings("OverwrittenKey")
Integer containsKeyAndPuts(Map<Long, Integer> values) {
UtMock.assume(!values.containsKey(1L));

values.put(1L, 2);
values.put(1L, 3);

UtMock.assume(values.get(1L).equals(3));

return values.get(1L);
}

Map<Character, Integer> countChars(String s) {
Map<Character, Integer> map = new LinkedHashMap<>();
for (int i = 0; i < s.length(); i++) {
Expand Down Expand Up @@ -261,4 +293,29 @@ public List<String> mapOperator(Map<String, String> map) {
return new ArrayList<>(map.values());
}
}

public Map<String, Integer> createMapWithString() {
Map<String, Integer> map = new HashMap<>();
map.put("tuesday", 354);
map.remove("tuesday");

return map;
}
public Map<WorkDays, Integer> createMapWithEnum() {
Map<WorkDays, Integer> map = new HashMap<>();
map.put(WorkDays.Monday, 112);
map.put(WorkDays.Tuesday, 354);
map.put(WorkDays.Friday, 567);
map.remove(WorkDays.Tuesday);

return map;
}

public enum WorkDays {
Monday,
Tuesday,
Wednesday,
Thursday,
Friday
}
}