Сoncrete values for enums (#19)

Author: Damtev

utbot-core/src/main/kotlin/org/utbot/common/KClassUtil.kt

@@ -28,4 +28,4 @@ fun Method.invokeCatching(obj: Any?, args: List<Any?>) = try {
     Result.success(invoke(obj, *args.toTypedArray()))
 } catch (e: InvocationTargetException) {
     Result.failure<Nothing>(e.targetException)
-}
+}

utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt

@@ -31,7 +31,7 @@ internal class SettingDelegate<T>(val initializer: () -> T) {
 /**
  * Default concrete execution timeout (in milliseconds).
  */
-const val DEFAULT_CONCRETE_EXECUTION_TIMEOUT_IN_CHILD_PROCESS_MS = 100L
+const val DEFAULT_CONCRETE_EXECUTION_TIMEOUT_IN_CHILD_PROCESS_MS = 1000L
 
 object UtSettings {
     private val properties = Properties().also { props ->

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

@@ -25,6 +25,7 @@ import org.utbot.engine.pc.mkLong
 import org.utbot.engine.pc.mkShort
 import org.utbot.engine.pc.select
 import org.utbot.engine.pc.store
+import org.utbot.engine.util.statics.concrete.isEnumValuesFieldName
 import org.utbot.engine.symbolic.asHardConstraint
 import org.utbot.engine.z3.intValue
 import org.utbot.engine.z3.value
@@ -82,6 +83,7 @@ import soot.PrimType
 import soot.RefType
 import soot.Scene
 import soot.ShortType
+import soot.SootClass
 import soot.SootField
 import soot.Type
 import soot.VoidType
@@ -1068,7 +1070,7 @@ fun UtBotSymbolicEngine.toMethodResult(value: Any?, sootType: Type): MethodResul
             arrayToMethodResult(value.size, elementType) {
                 if (value[it] == null) return@arrayToMethodResult nullObjectAddr
 
-                val addr = UtAddrExpression(mkBVConst("staticVariable${value.hashCode()}", UtInt32Sort))
+                val addr = UtAddrExpression(mkBVConst("staticVariable${value.hashCode()}_$it", UtInt32Sort))
 
                 val createdElement = if (elementType is RefType) {
                     val className = value[it]!!.javaClass.id.name
@@ -1141,6 +1143,30 @@ private fun UtBotSymbolicEngine.arrayToMethodResult(
     )
 }
 
+fun UtBotSymbolicEngine.constructEnumStaticFieldResult(
+    fieldName: String,
+    fieldType: Type,
+    declaringClass: SootClass,
+    enumConstantSymbolicResultsByName: Map<String, MethodResult>,
+    staticFieldConcreteValue: Any?,
+    enumConstantSymbolicValues: List<ObjectValue>
+): MethodResult =
+    if (isEnumValuesFieldName(fieldName)) {
+        // special case to fill $VALUES array with already created symbolic values for enum constants runtime values
+        arrayToMethodResult(enumConstantSymbolicValues.size, declaringClass.type) { i ->
+            enumConstantSymbolicValues[i].addr
+        }
+    } else {
+        if (fieldName in enumConstantSymbolicResultsByName) {
+            // it is field to store enum constant so we use already created symbolic value from runtime enum constant
+            enumConstantSymbolicResultsByName.getValue(fieldName)
+        } else {
+            // otherwise, it is a common static field,
+            // and we have to create new symbolic value for it using its concrete value
+            toMethodResult(staticFieldConcreteValue, fieldType)
+        }
+    }
+
 private val Type.unsigned: Boolean
     get() = this is CharType
 

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

@@ -18,7 +18,6 @@ import soot.Scene
 import soot.SootField
 import soot.Type
 import soot.VoidType
-import sun.reflect.Reflection
 
 class TypeResolver(private val typeRegistry: TypeRegistry, private val hierarchy: Hierarchy) {
 

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

@@ -75,6 +75,12 @@ import org.utbot.engine.symbolic.SymbolicStateUpdate
 import org.utbot.engine.symbolic.asHardConstraint
 import org.utbot.engine.symbolic.asSoftConstraint
 import org.utbot.engine.symbolic.asUpdate
+import org.utbot.engine.util.statics.concrete.associateEnumSootFieldsWithConcreteValues
+import org.utbot.engine.util.statics.concrete.isEnumAffectingExternalStatics
+import org.utbot.engine.util.statics.concrete.isEnumValuesFieldName
+import org.utbot.engine.util.statics.concrete.makeEnumNonStaticFieldsUpdates
+import org.utbot.engine.util.statics.concrete.makeEnumStaticFieldsUpdates
+import org.utbot.engine.util.statics.concrete.makeSymbolicValuesFromEnumConcreteValues
 import org.utbot.framework.PathSelectorType
 import org.utbot.framework.UtSettings
 import org.utbot.framework.UtSettings.checkSolverTimeoutMillis
@@ -152,6 +158,7 @@ import kotlinx.collections.immutable.persistentHashMapOf
 import kotlinx.collections.immutable.persistentListOf
 import kotlinx.collections.immutable.persistentSetOf
 import kotlinx.collections.immutable.toPersistentList
+import kotlinx.collections.immutable.toPersistentMap
 import kotlinx.collections.immutable.toPersistentSet
 import kotlinx.coroutines.CancellationException
 import kotlinx.coroutines.Job
@@ -196,7 +203,6 @@ import soot.jimple.Expr
 import soot.jimple.FieldRef
 import soot.jimple.FloatConstant
 import soot.jimple.IdentityRef
-import soot.jimple.InstanceFieldRef
 import soot.jimple.IntConstant
 import soot.jimple.InvokeExpr
 import soot.jimple.LongConstant
@@ -876,7 +882,7 @@ class UtBotSymbolicEngine(
         stmt: Stmt
     ): Boolean {
         if (shouldProcessStaticFieldConcretely(fieldRef)) {
-            return processStaticFieldConcretely(fieldRef)
+            return processStaticFieldConcretely(fieldRef, stmt)
         }
 
         val field = fieldRef.field
@@ -922,7 +928,9 @@ class UtBotSymbolicEngine(
             // Note that this list is not exhaustive, so it may be supplemented in the future.
             val packagesToProcessConcretely = javaPackagesToProcessConcretely + sunPackagesToProcessConcretely
 
-            return packagesToProcessConcretely.any { className.startsWith(it) }
+            val declaringClass = fieldRef.field.declaringClass
+
+            val isFromPackageToProcessConcretely = packagesToProcessConcretely.any { className.startsWith(it) }
                     // it is required to remove classes we override, since
                     // we could accidentally initialize their final fields
                     // with values that will later affect our overridden classes
@@ -933,6 +941,13 @@ class UtBotSymbolicEngine(
                     //hardcoded string for class name is used cause class is not public
                     //this is a hack to avoid crashing on code with Math.random()
                     && !className.endsWith("RandomNumberGeneratorHolder")
+
+            // we can process concretely only enums that does not affect the external system
+            val isEnumNotAffectingExternalStatics = declaringClass.let {
+                it.isEnum && !it.isEnumAffectingExternalStatics(typeResolver)
+            }
+
+            return isEnumNotAffectingExternalStatics || isFromPackageToProcessConcretely
         }
     }
 
@@ -954,7 +969,7 @@ class UtBotSymbolicEngine(
      *
      * Returns true if processing takes place and Engine should end traversal of current statement.
      */
-    private fun processStaticFieldConcretely(fieldRef: StaticFieldRef): Boolean {
+    private fun processStaticFieldConcretely(fieldRef: StaticFieldRef, stmt: Stmt): Boolean {
         val field = fieldRef.field
         val fieldId = field.fieldId
         if (memory.isInitialized(fieldId)) {
@@ -963,26 +978,123 @@ class UtBotSymbolicEngine(
 
         // Gets concrete value, converts to symbolic value
         val declaringClass = field.declaringClass
+
+        val (edge, updates) = if (declaringClass.isEnum) {
+            makeConcreteUpdatesForEnums(fieldId, declaringClass, stmt)
+        } else {
+            makeConcreteUpdatesForNonEnumStaticField(field, fieldId, declaringClass)
+        }
+
+        val newState = environment.state.updateQueued(edge, updates)
+        pathSelector.offer(newState)
+
+        return true
+    }
+
+    private fun makeConcreteUpdatesForEnums(
+        fieldId: FieldId,
+        declaringClass: SootClass,
+        stmt: Stmt
+    ): Pair<Edge, SymbolicStateUpdate> {
+        val type = declaringClass.type
+        val jClass = type.id.jClass
+
+        // symbolic value for enum class itself
+        val enumClassValue = findOrCreateStaticObject(type)
+
+        // values for enum constants
+        val enumConstantConcreteValues = jClass.enumConstants.filterIsInstance<Enum<*>>()
+
+        val (enumConstantSymbolicValues, enumConstantSymbolicResultsByName) =
+            makeSymbolicValuesFromEnumConcreteValues(type, enumConstantConcreteValues)
+
+        val enumFields = typeResolver.findFields(type)
+
+        val sootFieldsWithRuntimeValues =
+            associateEnumSootFieldsWithConcreteValues(enumFields, enumConstantConcreteValues)
+
+        val (staticFields, nonStaticFields) = sootFieldsWithRuntimeValues.partition { it.first.isStatic }
+
+        val (staticFieldUpdates, curFieldSymbolicValueForLocalVariable) = makeEnumStaticFieldsUpdates(
+            staticFields,
+            declaringClass,
+            enumConstantSymbolicResultsByName,
+            enumConstantSymbolicValues,
+            enumClassValue,
+            fieldId
+        )
+
+        val nonStaticFieldsUpdates = makeEnumNonStaticFieldsUpdates(enumConstantSymbolicValues, nonStaticFields)
+
+        // we do not mark static fields for enum constants and $VALUES as meaningful
+        // because we should not set them in generated code
+        val meaningfulStaticFields = staticFields.filterNot {
+            val name = it.first.name
+
+            name in enumConstantSymbolicResultsByName.keys || isEnumValuesFieldName(name)
+        }
+
+        val initializedStaticFieldsMemoryUpdate = MemoryUpdate(
+            initializedStaticFields = staticFields.associate { it.first.fieldId to it.second.single() }.toPersistentMap(),
+            meaningfulStaticFields = meaningfulStaticFields.map { it.first.fieldId }.toPersistentSet()
+        )
+
+        var allUpdates = staticFieldUpdates + nonStaticFieldsUpdates + initializedStaticFieldsMemoryUpdate
+
+        // we need to make locals update if it is an assignment statement
+        // for enums we have only two types for assignment with enums — enum constant or $VALUES field
+        // for example, a jimple body for Enum::values method starts with the following lines:
+        //  public static ClassWithEnum$StatusEnum[] values()
+        //  {
+        //      ClassWithEnum$StatusEnum[] $r0, $r2;
+        //      java.lang.Object $r1;
+        //      $r0 = <ClassWithEnum$StatusEnum: ClassWithEnum$StatusEnum[] $VALUES>;
+        //      $r1 = virtualinvoke $r0.<java.lang.Object: java.lang.Object clone()>();
+
+        // so, we have to make an update for the local $r0
+        if (stmt is JAssignStmt) {
+            val local = stmt.leftOp as JimpleLocal
+            val localUpdate = localMemoryUpdate(
+                local.variable to curFieldSymbolicValueForLocalVariable
+            )
+
+            allUpdates += localUpdate
+        }
+
+        // enum static initializer can be the first statement in method so there will be no last edge
+        // for example, as it is during Enum::values method analysis:
+        // public static ClassWithEnum$StatusEnum[] values()
+        // {
+        //      ClassWithEnum$StatusEnum[] $r0, $r2;
+        //      java.lang.Object $r1;
+
+        //      $r0 = <ClassWithEnum$StatusEnum: ClassWithEnum$StatusEnum[] $VALUES>;
+        val edge = environment.state.lastEdge ?: globalGraph.succ(stmt)
+
+        return edge to allUpdates
+    }
+
+    private fun makeConcreteUpdatesForNonEnumStaticField(
+        field: SootField,
+        fieldId: FieldId,
+        declaringClass: SootClass
+    ): Pair<Edge, SymbolicStateUpdate> {
         val concreteValue = extractConcreteValue(field, declaringClass)
         val (symbolicResult, symbolicStateUpdate) = toMethodResult(concreteValue, field.type)
         val symbolicValue = (symbolicResult as SymbolicSuccess).value
 
         // Collects memory updates
         val initializedFieldUpdate =
             MemoryUpdate(initializedStaticFields = persistentHashMapOf(fieldId to concreteValue))
+
         val objectUpdate = objectUpdate(
             instance = findOrCreateStaticObject(declaringClass.type),
             field = field,
             value = valueToExpression(symbolicValue, field.type)
         )
         val allUpdates = symbolicStateUpdate + initializedFieldUpdate + objectUpdate
-        pathSelector.offer(
-            environment.state.updateQueued(
-                edge = environment.state.lastEdge!!,
-                allUpdates
-            )
-        )
-        return true
+
+        return environment.state.lastEdge!! to allUpdates
     }
 
     // Some fields are inaccessible with reflection, so we have to instantiate it by ourselves.
@@ -1200,7 +1312,7 @@ class UtBotSymbolicEngine(
     /**
      * Converts value to expression with cast to target type for primitives.
      */
-    private fun valueToExpression(value: SymbolicValue, type: Type): UtExpression = when (value) {
+    fun valueToExpression(value: SymbolicValue, type: Type): UtExpression = when (value) {
         is ReferenceValue -> value.addr
         // TODO: shall we add additional constraint that aligned expression still equals original?
         // BitVector can lose valuable bites during extraction
@@ -2028,6 +2140,7 @@ class UtBotSymbolicEngine(
         val touchedStaticFields = persistentListOf(staticFieldMemoryUpdate)
         queuedSymbolicStateUpdates += MemoryUpdate(staticFieldsUpdates = touchedStaticFields)
 
+        // TODO filter enum constant static fields JIRA:1681
         if (!environment.method.isStaticInitializer && !fieldId.isSynthetic) {
             queuedSymbolicStateUpdates += MemoryUpdate(meaningfulStaticFields = persistentSetOf(fieldId))
         }