Map don't work without concrete

CaelmBleidd · CaelmBleidd · commit a1e577e4cadf · 2022-10-25T16:55:03.000+08:00
Fixes:
* aliasing between nested arrays of UtHashMap and its fields
* unsat for get operation from Map
diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/examples/collections/MapsPart1Test.kt b/utbot-framework-test/src/test/kotlin/org/utbot/examples/collections/MapsPart1Test.kt
@@ -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
 
@@ -84,6 +85,44 @@ 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,
+                ignoreExecutionsNumber,
+                { values, _ -> values == null },
+                { values, r -> 1 !in values.keys && r == 3 },
+            )
+        }
+    }
+
     @Test
     fun testFindAllChars() {
         check(
@@ -324,4 +363,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 }
+            )
+        }
+    }
 }
diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtHashMap.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtHashMap.java
@@ -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();
@@ -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;
     }
 
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ArrayObjectWrappers.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ArrayObjectWrappers.kt
@@ -215,13 +215,16 @@ 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("Unexpected wrapper $wrapper")
+            val typeConstraint = typeRegistry.typeConstraintToGenericTypeParameter(
+                addr,
+                wrapper.addr,
+                i = typeIndex
+            ).asHardConstraint()
+
+            val methodResult = MethodResult(SymbolicSuccess(resultObject), typeConstraint)
+
+            listOf(methodResult)
         }
 
     @Suppress("UNUSED_PARAMETER")
@@ -418,16 +421,16 @@ 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("Unexpected wrapper $wrapper")
+            val hardConstraints = typeRegistry.typeConstraintToGenericTypeParameter(
+                addr,
+                wrapper.addr,
+                typeIndex
+            ).asHardConstraint()
+
+            val methodResult = MethodResult(SymbolicSuccess(resultObject), hardConstraints)
+
+            listOf(methodResult)
         }
 
     @Suppress("UNUSED_PARAMETER")
@@ -440,21 +443,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(
@@ -480,7 +493,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 ->
@@ -504,7 +517,7 @@ class AssociativeArrayWrapper : WrapperInterface {
 
         val storageValues = UtArrayModel(
             resolver.holder.concreteAddr(UtAddrExpression(storageArrayAddr)),
-            objectClassId,
+            objectArrayClassId,
             sizeValue,
             UtNullModel(objectClassId),
             stores = (0 until sizeValue).associateTo(mutableMapOf()) { i ->
@@ -518,10 +531,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
     }
 
@@ -537,7 +552,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
+}
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ObjectWrappers.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ObjectWrappers.kt
@@ -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
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt
@@ -3534,7 +3534,7 @@ class Traverser(
 
         // toplevel method
         // TODO: investigate very strange behavior when some constraints are not added leading to failing CodegenExampleTest::firstExampleTest fails
-        val terminalExecutionState = environment.state.copy(
+         val terminalExecutionState = environment.state.copy(
             symbolicState = symbolicState,
             methodResult = methodResult, // the way to put SymbolicResult into terminal state
             label = StateLabel.TERMINAL
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpression.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpression.kt
@@ -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 {
diff --git a/utbot-sample/src/main/java/org/utbot/examples/collections/Maps.java b/utbot-sample/src/main/java/org/utbot/examples/collections/Maps.java
@@ -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;
@@ -25,6 +27,35 @@ String mapToString(long startTime, int pageSize, int pageNum) {
         return params.toString();
     }
 
+    Integer mapPutAndGet() {
+        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++) {
@@ -261,4 +292,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
+    }
 }

Original file line number	Diff line number	Diff line change
`@@ -455,7 +455,7 @@ class UtIsGenericTypeExpression(`
`455`	`455`	`override fun <TResult> accept(visitor: UtExpressionVisitor<TResult>): TResult = visitor.visit(this)`
`456`	`456`
`457`	`457`	`override fun toString(): String {`
`458`		`- return "(generic-is $addr $baseAddr<\$$parameterTypeIndex>)"`
	`458`	`+ return "(generic-is $addr baseAddr<ParamTypeIndex>: $baseAddr<\$$parameterTypeIndex>)"`
`459`	`459`	`}`
`460`	`460`
`461`	`461`	`override fun equals(other: Any?): Boolean {`