Verify mock correctness and selection a little more careful #2074 (#2153)

Co-authored-by: Alexey Menshutin <alex.menshutin99@gmail.com>

Author: EgorkaKulikov

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

@@ -28,6 +28,7 @@ import org.utbot.framework.plugin.api.UtModel
 import org.utbot.framework.plugin.api.UtNullModel
 import org.utbot.framework.plugin.api.UtPrimitiveModel
 import org.utbot.framework.plugin.api.getIdOrThrow
+import org.utbot.framework.plugin.api.id
 import org.utbot.framework.plugin.api.util.fieldId
 import org.utbot.framework.plugin.api.util.id
 import org.utbot.framework.plugin.api.util.objectArrayClassId
@@ -208,7 +209,10 @@ class RangeModifiableUnlimitedArrayWrapper : WrapperInterface {
                 ?: OBJECT_TYPE
 
             val resultObject = if (valueType is RefType) {
-                createObject(addr, valueType, useConcreteType = false)
+                val mockInfoGenerator = UtMockInfoGenerator { mockAddr ->
+                    UtObjectMockInfo(valueType.id, mockAddr)
+                }
+                createObject(addr, valueType, useConcreteType = false, mockInfoGenerator)
             } else {
                 require(valueType is ArrayType) {
                     "Unexpected Primitive Type $valueType in generic parameter for RangeModifiableUnlimitedArray $wrapper"
@@ -431,7 +435,9 @@ class AssociativeArrayWrapper : WrapperInterface {
         with(traverser) {
             val value = getStorageArrayExpression(wrapper).select(parameters[0].addr)
             val addr = UtAddrExpression(value)
-            val resultObject = createObject(addr, OBJECT_TYPE, useConcreteType = false)
+            // TODO it is probably a bug, what mock generator should we provide here?
+            //      Seems like we don't know anything about its type here
+            val resultObject = createObject(addr, OBJECT_TYPE, useConcreteType = false, mockInfoGenerator = null)
 
             val typeIndex = wrapper.asWrapperOrNull?.selectOperationTypeIndex
                 ?: error("Wrapper was expected, got $wrapper")

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

@@ -381,7 +381,12 @@ data class ThrowableWrapper(val throwable: Throwable) : WrapperInterface {
         workaround(MAKE_SYMBOLIC) {
             listOf(
                 MethodResult(
-                    createConst(method.returnType, typeRegistry.findNewSymbolicReturnValueName())
+                    createConst(
+                        method.returnType,
+                        typeRegistry.findNewSymbolicReturnValueName(),
+                        // we don't want to mock anything returned from a throwable instance's methods
+                        mockInfoGenerator = null
+                    )
                 )
             )
         }

utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt

@@ -292,8 +292,11 @@ class Resolver(
         // Associates mock infos by concrete addresses
         // Sometimes we might have two mocks with the same concrete address, and here we group their mockInfos
         // Then we should merge executables for mocks with the same concrete addresses with respect to the calls order
-        val mocks = memory
-            .mocks()
+        val memoryMocks = memory.mocks()
+            // TODO add a comment about why is it impossible to have nulls here
+            .filter { holder.concreteAddr(it.mockInfo.addr) != SYMBOLIC_NULL_ADDR }
+
+        val mocks = memoryMocks
             .groupBy { enriched -> holder.concreteAddr(enriched.mockInfo.addr) }
             .map { (address, mockInfos) -> address to mockInfos.mergeExecutables() }
 
@@ -303,7 +306,7 @@ class Resolver(
         val staticMethodMocks = mutableMapOf<MethodId, List<UtModel>>()
 
         // Enriches mock info with information from callsToMocks
-        memory.mocks().forEach { (mockInfo, executables) ->
+        memoryMocks.forEach { (mockInfo, executables) ->
             when (mockInfo) {
                 // Collects static field mocks differently
                 is UtFieldMockInfo -> if (mockInfo.ownerAddr == null) {
@@ -319,7 +322,7 @@ class Resolver(
         }
 
         // Collects instrumentation
-        val newInstancesInstrumentation = memory.mocks()
+        val newInstancesInstrumentation = memoryMocks
             .map { it.mockInfo }
             .filterIsInstance<UtNewInstanceMockInfo>()
             .groupBy { it.classId }
@@ -1219,7 +1222,8 @@ fun Traverser.toMethodResult(value: Any?, sootType: Type): MethodResult {
     return when (value) {
         null -> asMethodResult {
             if (sootType is RefType) {
-                createObject(nullObjectAddr, sootType, useConcreteType = true)
+                // We don't want to mock values we took from a concrete environment
+                createObject(nullObjectAddr, sootType, useConcreteType = true, mockInfoGenerator = null)
             } else {
                 createArray(nullObjectAddr, sootType as ArrayType, useConcreteType = true)
             }
@@ -1262,7 +1266,8 @@ fun Traverser.toMethodResult(value: Any?, sootType: Type): MethodResult {
                             ?.let { type -> type to true }
                             ?: (elementType to false)
 
-                    createObject(addr, type, useConcreteType)
+                    // We don't want to mock values we took from a concrete environment
+                    createObject(addr, type, useConcreteType, mockInfoGenerator = null)
                 } else {
                     require(elementType is ArrayType)
                     // We cannot use concrete types since we do not receive
@@ -1296,7 +1301,8 @@ fun Traverser.toMethodResult(value: Any?, sootType: Type): MethodResult {
                         ?.let { type -> type to true }
                         ?: (sootType as RefType to false)
 
-                    createObject(addr, type, useConcreteType)
+                    // We don't want to mock values we took from a concrete environment
+                    createObject(addr, type, useConcreteType, mockInfoGenerator = null)
                 }
             }
         }

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

@@ -776,8 +776,16 @@ class Traverser(
 
     private fun TraversalContext.skipVerticesForThrowableCreation(current: JAssignStmt) {
         val rightType = current.rightOp.type as RefType
-        val exceptionType = Scene.v().getSootClass(rightType.className).type
-        val createdException = createObject(findNewAddr(), exceptionType, true)
+        val exceptionType = Scene.v().getRefType(rightType.className)
+        val mockInfoGenerator = UtMockInfoGenerator { mockAddr ->
+            UtNewInstanceMockInfo(exceptionType.id, mockAddr, environment.method.declaringClass.id)
+        }
+        val createdException = createObject(
+            findNewAddr(),
+            exceptionType,
+            useConcreteType = true,
+            mockInfoGenerator = mockInfoGenerator
+        )
         val currentExceptionJimpleLocal = current.leftOp as JimpleLocal
 
         queuedSymbolicStateUpdates += localMemoryUpdate(currentExceptionJimpleLocal.variable to createdException)
@@ -1017,10 +1025,8 @@ class Traverser(
         }
         is StaticFieldRef -> {
             val declaringClassType = fieldRef.field.declaringClass.type
-            val fieldTypeId = fieldRef.field.type.classId
             val generator = UtMockInfoGenerator { mockAddr ->
-                val fieldId = FieldId(declaringClassType.id, fieldRef.field.name)
-                UtFieldMockInfo(fieldTypeId, mockAddr, fieldId, ownerAddr = null)
+                UtStaticObjectMockInfo(declaringClassType.id, mockAddr)
             }
             findOrCreateStaticObject(declaringClassType, generator)
         }
@@ -1375,7 +1381,7 @@ class Traverser(
         addr: UtAddrExpression,
         type: RefType,
         useConcreteType: Boolean,
-        mockInfoGenerator: UtMockInfoGenerator? = null
+        mockInfoGenerator: UtMockInfoGenerator?
     ): ObjectValue {
         touchAddress(addr)
         val nullEqualityConstraint = mkEq(addr, nullObjectAddr)
@@ -1422,10 +1428,10 @@ class Traverser(
 
                 // add typeConstraint for mocked object. It's a declared type of the object.
                 val typeConstraint = typeRegistry.typeConstraint(addr, mockedObject.typeStorage).all()
-                val isMockConstraint = mkEq(typeRegistry.isMock(mockedObject.addr), UtTrue)
+                val isMockConstraint = typeRegistry.isMockConstraint(mockedObject.addr)
 
                 queuedSymbolicStateUpdates += typeConstraint.asHardConstraint()
-                queuedSymbolicStateUpdates += mkOr(isMockConstraint, nullEqualityConstraint).asHardConstraint()
+                queuedSymbolicStateUpdates += isMockConstraint.asHardConstraint()
 
                 return mockedObject
             }
@@ -1505,7 +1511,7 @@ class Traverser(
         }
 
         val concreteImplementation: Concrete? = when (applicationContext.typeReplacementMode) {
-            AnyImplementor -> findConcreteImplementation(addr, type, typeHardConstraint, nullEqualityConstraint)
+            AnyImplementor -> findConcreteImplementation(addr, type, typeHardConstraint)
 
             // If our type is not abstract, both in `KnownImplementors` and `NoImplementors` mode,
             // we should just still use concrete implementation that represents itself
@@ -1521,7 +1527,7 @@ class Traverser(
             KnownImplementor,
             NoImplementors -> {
                 if (!type.isAbstractType) {
-                    findConcreteImplementation(addr, type, typeHardConstraint, nullEqualityConstraint)
+                    findConcreteImplementation(addr, type, typeHardConstraint)
                 } else {
                     mockInfoGenerator?.let {
                         return createMockedObject(addr, type, it, nullEqualityConstraint)
@@ -1540,12 +1546,11 @@ class Traverser(
         addr: UtAddrExpression,
         type: RefType,
         typeHardConstraint: HardConstraint,
-        nullEqualityConstraint: UtBoolExpression,
     ): Concrete? {
         val isMockConstraint = mkEq(typeRegistry.isMock(addr), UtFalse)
 
         queuedSymbolicStateUpdates += typeHardConstraint
-        queuedSymbolicStateUpdates += mkOr(isMockConstraint, nullEqualityConstraint).asHardConstraint()
+        queuedSymbolicStateUpdates += isMockConstraint.asHardConstraint()
 
         // If we have this$0 with UtArrayList type, we have to create such instance.
         // We should create an object with typeStorage of all possible real types and concrete implementation
@@ -1583,10 +1588,10 @@ class Traverser(
 
         // add typeConstraint for mocked object. It's a declared type of the object.
         val typeConstraint = typeRegistry.typeConstraint(addr, mockedObject.typeStorage).all()
-        val isMockConstraint = mkEq(typeRegistry.isMock(mockedObject.addr), UtTrue)
+        val isMockConstraint = typeRegistry.isMockConstraint(mockedObject.addr)
 
         queuedSymbolicStateUpdates += typeConstraint.asHardConstraint()
-        queuedSymbolicStateUpdates += mkOr(isMockConstraint, nullEqualityConstraint).asHardConstraint()
+        queuedSymbolicStateUpdates += isMockConstraint.asHardConstraint()
 
         return mockedObject
     }
@@ -1606,7 +1611,8 @@ class Traverser(
                     // instead of it we create an unbounded symbolic variable
                     workaround(HACK) {
                         offerState(environment.state.withLabel(StateLabel.CONCRETE))
-                        createObject(addr, refType, useConcreteType = true)
+                        // We don't need to mock a string constant creation
+                        createObject(addr, refType, useConcreteType = true, mockInfoGenerator = null)
                     }
                 } else {
                     val typeStorage = TypeStorage.constructTypeStorageWithSingleType(refType)
@@ -2254,7 +2260,7 @@ class Traverser(
         addr: UtAddrExpression,
         fieldType: Type,
         chunkId: ChunkId,
-        mockInfoGenerator: UtMockInfoGenerator? = null
+        mockInfoGenerator: UtMockInfoGenerator?
     ): SymbolicValue {
         val descriptor = MemoryChunkDescriptor(chunkId, objectType, fieldType)
         val array = memory.findArray(descriptor)
@@ -2395,10 +2401,10 @@ class Traverser(
      * Since createConst called only for objects from outside at the beginning of the analysis,
      * we can set Le(addr, NULL_ADDR) for all RefValue objects.
      */
-    private fun Value.createConst(pName: String, mockInfoGenerator: UtMockInfoGenerator? = null): SymbolicValue =
+    private fun Value.createConst(pName: String, mockInfoGenerator: UtMockInfoGenerator?): SymbolicValue =
         createConst(type, pName, mockInfoGenerator)
 
-    fun createConst(type: Type, pName: String, mockInfoGenerator: UtMockInfoGenerator? = null): SymbolicValue =
+    fun createConst(type: Type, pName: String, mockInfoGenerator: UtMockInfoGenerator?): SymbolicValue =
         when (type) {
             is ByteType -> mkBVConst(pName, UtByteSort).toByteValue()
             is ShortType -> mkBVConst(pName, UtShortSort).toShortValue()
@@ -3460,9 +3466,9 @@ class Traverser(
 
     private fun unboundedVariable(name: String, method: SootMethod): MethodResult {
         val value = when (val returnType = method.returnType) {
-            is RefType -> createObject(findNewAddr(), returnType, useConcreteType = true)
+            is RefType -> createObject(findNewAddr(), returnType, useConcreteType = true, mockInfoGenerator = null)
             is ArrayType -> createArray(findNewAddr(), returnType, useConcreteType = true)
-            else -> createConst(returnType, "$name${unboundedConstCounter++}")
+            else -> createConst(returnType, "$name${unboundedConstCounter++}", mockInfoGenerator = null)
         }
 
         return MethodResult(value)

utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeRegistry.kt

@@ -199,6 +199,20 @@ class TypeRegistry {
      */
     fun isMock(addr: UtAddrExpression) = isMockArray.select(addr)
 
+    private fun mockCorrectnessConstraint(addr: UtAddrExpression) =
+        mkOr(
+            mkEq(isMock(addr), UtFalse),
+            mkNot(mkEq(addr, nullObjectAddr))
+        )
+
+    fun isMockConstraint(addr: UtAddrExpression) = mkAnd(
+        mkOr(
+            mkEq(isMock(addr), UtTrue),
+            mkEq(addr, nullObjectAddr)
+        ),
+        mockCorrectnessConstraint(addr)
+    )
+
     /**
      * Makes the numbers of dimensions for every object in the program equal to zero by default
      */