UtConstraintModel implemented

UnitTestBot · AbdullinAM · Jun 20, 2022 · Jun 20, 2022 · Jun 22, 2022 · Jun 28, 2022
commit 4285a5c0c8e49fc747cefa893cbbb046db328ed8
diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/Api.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/Api.kt
@@ -444,6 +444,35 @@ data class UtArrayModel(
     }
 }
 
+/**
+ * Models for values with constraints
+ */
+sealed class UtConstraintModel(
+    open val variable: Var,
+    open val utConstraints: Set<UtConstraint>
+) : UtModel(variable.classId) {
+}
+
+data class UtPrimitiveConstraintModel(
+    override val variable: Var,
+    override val utConstraints: Set<UtConstraint>
+) : UtConstraintModel(variable, utConstraints) {
+}
+
+data class UtReferenceConstraintModel(
+    override val variable: Var,
+    override val utConstraints: Set<UtConstraint>
+) : UtConstraintModel(variable, utConstraints) {
+    fun isNull() = utConstraints.any {
+        it is UtRefEqConstraint && it.lhv == variable && it.rhv is NullVar
+    }
+}
+
+data class UtReferenceToConstraintModel(
+    override val variable: Var,
+    val reference: UtModel
+) : UtConstraintModel(variable, emptySet())
+
 /**
  * Model for complex objects with assemble instructions.
  *

diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/ConstraintApi.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/ConstraintApi.kt
@@ -0,0 +1,150 @@
+package org.utbot.framework.plugin.api
+
+import org.utbot.framework.plugin.api.util.id
+import org.utbot.framework.plugin.api.util.isPrimitive
+
+sealed class Var {
+    abstract val classId: ClassId
+    val isPrimitive get() = classId.isPrimitive
+}
+
+data class NullVar(override val classId: ClassId) : Var() {
+    override fun toString(): String = "null"
+}
+
+data class Parameter(
+    val name: String,
+    override val classId: ClassId
+) : Var() {
+    override fun toString(): String = name
+}
+
+data class FieldAccess(
+    val instance: Var,
+    val fieldId: FieldId,
+) : Var() {
+    override val classId: ClassId
+        get() = fieldId.type
+
+    override fun toString(): String = "$instance.${fieldId.name}"
+}
+
+data class ArrayAccess(
+    val instance: Var,
+    val index: Var,
+    override val classId: ClassId
+) : Var() {
+    override fun toString(): String = "$instance[$index]"
+}
+
+data class ArrayLengthAccess(
+    val instance: Var,
+) : Var() {
+    override val classId: ClassId = Integer.TYPE.id
+    override fun toString(): String = "$instance.length"
+}
+
+data class BoolConstant(
+    val value: Boolean
+) : Var() {
+    override val classId: ClassId = primitiveModelValueToClassId(value)
+
+    override fun toString(): String = "$value"
+}
+
+data class CharConstant(
+    val value: Char,
+) : Var() {
+    override val classId: ClassId = primitiveModelValueToClassId(value)
+
+    override fun toString(): String = "$value"
+}
+
+data class NumericConstant(
+    val value: Number,
+) : Var() {
+    override val classId: ClassId = primitiveModelValueToClassId(value)
+
+    override fun toString(): String = "$value"
+}
+
+
+sealed class UtConstraint {
+    abstract fun negated(): UtConstraint
+}
+
+sealed class UtReferenceConstraint : UtConstraint()
+
+data class UtRefEqConstraint(val lhv: Var, val rhv: Var) : UtReferenceConstraint() {
+    override fun negated(): UtConstraint = UtRefNeqConstraint(lhv, rhv)
+
+    override fun toString(): String = "$lhv == $rhv"
+}
+
+data class UtRefNeqConstraint(val lhv: Var, val rhv: Var) : UtReferenceConstraint() {
+    override fun negated(): UtConstraint = UtRefEqConstraint(lhv, rhv)
+
+    override fun toString(): String = "$lhv != $rhv"
+}
+
+data class UtRefTypeConstraint(val operand: Var, val type: ClassId) : UtReferenceConstraint() {
+    override fun negated(): UtConstraint = UtRefNotTypeConstraint(operand, type)
+
+    override fun toString(): String = "$operand is $type"
+}
+
+data class UtRefNotTypeConstraint(val operand: Var, val type: ClassId) : UtReferenceConstraint() {
+    override fun negated(): UtConstraint = UtRefTypeConstraint(operand, type)
+
+    override fun toString(): String = "$operand !is $type"
+}
+
+sealed class UtPrimitiveConstraint : UtConstraint()
+
+data class UtEqConstraint(val lhv: Var, val rhv: Var) : UtPrimitiveConstraint() {
+    override fun negated(): UtConstraint = UtNeqConstraint(lhv, rhv)
+
+    override fun toString(): String = "$lhv == $rhv"
+}
+
+data class UtNeqConstraint(val lhv: Var, val rhv: Var) : UtPrimitiveConstraint() {
+    override fun negated(): UtConstraint = UtEqConstraint(lhv, rhv)
+
+    override fun toString(): String = "$lhv != $rhv"
+}
+
+data class UtLtConstraint(val lhv: Var, val rhv: Var) : UtPrimitiveConstraint() {
+    override fun negated(): UtConstraint = UtGeConstraint(lhv, rhv)
+
+    override fun toString(): String = "$lhv < $rhv"
+}
+
+data class UtGtConstraint(val lhv: Var, val rhv: Var) : UtPrimitiveConstraint() {
+    override fun negated(): UtConstraint = UtLeConstraint(lhv, rhv)
+
+    override fun toString(): String = "$lhv > $rhv"
+}
+
+data class UtLeConstraint(val lhv: Var, val rhv: Var) : UtPrimitiveConstraint() {
+    override fun negated(): UtConstraint = UtGtConstraint(lhv, rhv)
+
+    override fun toString(): String = "$lhv <= $rhv"
+}
+
+data class UtGeConstraint(val lhv: Var, val rhv: Var) : UtPrimitiveConstraint() {
+    override fun negated(): UtConstraint = UtLtConstraint(lhv, rhv)
+
+    override fun toString(): String = "$lhv >= $rhv"
+}
+
+data class UtAndConstraint(val lhv: UtConstraint, val rhv: UtConstraint) : UtPrimitiveConstraint() {
+    override fun negated(): UtConstraint = UtOrConstraint(lhv.negated(), rhv.negated())
+
+    override fun toString(): String = "($lhv) && ($rhv)"
+}
+
+data class UtOrConstraint(val lhv: UtConstraint, val rhv: UtConstraint) : UtPrimitiveConstraint() {
+    override fun negated(): UtConstraint = UtAndConstraint(lhv.negated(), rhv.negated())
+
+    override fun toString(): String = "($lhv) || ($rhv)"
+}
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ConstraintResolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ConstraintResolver.kt
@@ -4,10 +4,8 @@ import org.utbot.engine.MemoryState.CURRENT
 import org.utbot.engine.MemoryState.INITIAL
 import org.utbot.engine.MemoryState.STATIC_INITIAL
 import org.utbot.engine.z3.value
-import org.utbot.framework.plugin.api.FieldId
 import org.utbot.engine.pc.*
-import org.utbot.framework.plugin.api.ClassId
-import org.utbot.framework.plugin.api.classId
+import org.utbot.framework.plugin.api.*
 import soot.VoidType
 
 data class ResolvedObject(
@@ -31,11 +29,13 @@ data class ResolvedExecutionConstraints(
 class ConstraintResolver(
     private val memory: Memory,
     val holder: UtSolverStatusSAT,
+    val typeRegistry: TypeRegistry,
+    val typeResolver: TypeResolver,
 ) {
 
     lateinit var state: MemoryState
-    private val resolvedConstraints = mutableMapOf<Address, Set<UtBoolExpression>>()
-    private val validSymbols = mutableSetOf<UtExpression>()
+    lateinit var varBuilder: UtVarBuilder
+    private val resolvedConstraints = mutableMapOf<Address, UtModel>()
 
     /**
      * Contains FieldId of the static field which is construction at the moment and null of there is no such field.
@@ -45,7 +45,6 @@ class ConstraintResolver(
 
     private fun clearState() {
         resolvedConstraints.clear()
-        validSymbols.clear()
         resolvedConstraints.clear()
     }
 
@@ -74,8 +73,8 @@ class ConstraintResolver(
         }
     }
 
-    internal fun resolveModels(parameters: List<SymbolicValue>): ResolvedExecutionConstraints {
-        validSymbols.addAll(parameters.map { it.asExpr })
+    internal fun resolveModels(parameters: List<SymbolicValue>): ResolvedExecution {
+        varBuilder = UtVarBuilder(holder, typeRegistry, typeResolver)
         val allAddresses = UtExprCollector { it is UtAddrExpression }.let {
             holder.constraints.hard.forEach { constraint -> constraint.accept(it) }
             holder.constraints.soft.forEach { constraint -> constraint.accept(it) }
@@ -93,14 +92,14 @@ class ConstraintResolver(
             resolvedModels
         }
 
-        return ResolvedExecutionConstraints(modelsBefore, modelsAfter)
+        return ResolvedExecution(modelsBefore, modelsAfter, emptyList())
     }
 
     private fun internalResolveModel(
         parameters: List<SymbolicValue>,
         statics: List<Pair<FieldId, SymbolicValue>>,
         addrs: Map<UtAddrExpression, Address>
-    ): ResolvedConstraints {
+    ): ResolvedModels {
         val parameterModels = parameters.map { resolveModel(it, addrs) }
 
         val staticModels = statics.map { (fieldId, value) ->
@@ -110,61 +109,58 @@ class ConstraintResolver(
         }
 
         val allStatics = staticModels.mapIndexed { i, model -> statics[i].first to model }.toMap()
-        return ResolvedConstraints(parameterModels, allStatics)
+        return ResolvedModels(parameterModels, allStatics)
     }
 
-    fun resolveModel(value: SymbolicValue, addrs: Map<UtAddrExpression, Address>): ResolvedObject = when (value) {
+    fun resolveModel(value: SymbolicValue, addrs: Map<UtAddrExpression, Address>): UtModel = when (value) {
         is PrimitiveValue -> resolvePrimitiveValue(value, addrs)
         is ReferenceValue -> resolveReferenceValue(value, addrs)
     }
 
-    private fun collectConstraintAtoms(predicate: (UtExpression) -> Boolean): Set<UtBoolExpression> = UtAtomCollector(predicate).run {
-        holder.constraints.hard.forEach {
-            it.accept(this)
-        }
-        holder.constraints.soft.forEach {
-            it.accept(this)
-        }
-        result
-    }.map {
-        val rhv = if (holder.eval(it).value() as Boolean) UtTrue else UtFalse
-        UtEqExpression(it, rhv)
-    }.toSet()
+    private fun collectConstraintAtoms(predicate: (UtExpression) -> Boolean): Set<UtConstraint> =
+        UtAtomCollector(predicate).run {
+            holder.constraints.hard.forEach {
+                it.accept(this)
+            }
+            holder.constraints.soft.forEach {
+                it.accept(this)
+            }
+            result
+        }.mapNotNull {
+            it.accept(UtConstraintBuilder(varBuilder))
+        }.toSet()
 
-    private fun collectAtoms(value: SymbolicValue, addrs: Map<UtAddrExpression, Address>): Set<UtBoolExpression> =
+    private fun collectAtoms(value: SymbolicValue, addrs: Map<UtAddrExpression, Address>): Set<UtConstraint> =
         when (value) {
             is PrimitiveValue -> collectConstraintAtoms { it == value.expr }
             is ReferenceValue -> {
                 val concreteAddr = addrs[value.addr]!!
-                if (concreteAddr == NULL_ADDR) {
-                    setOf(
-                        UtEqExpression(UtEqExpression(value.addr, nullObjectAddr), UtTrue)
-                    )
-                } else {
-                    val valueExprs = addrs.filter { it.value == concreteAddr }.keys
-                    validSymbols.addAll(valueExprs)
-                    resolvedConstraints.getOrPut(concreteAddr) {
-                        val set = collectConstraintAtoms { it in valueExprs }.toMutableSet()
-                        set += UtEqExpression(UtEqExpression(value.addr, nullObjectAddr), UtFalse)
-                        set
-                    }
-                }
+                val valueExprs = addrs.filter { it.value == concreteAddr }.keys
+                collectConstraintAtoms { it in valueExprs }
             }
         }
 
-    private fun resolvePrimitiveValue(value: PrimitiveValue, addrs: Map<UtAddrExpression, Address>): ResolvedObject =
+    private fun resolvePrimitiveValue(value: PrimitiveValue, addrs: Map<UtAddrExpression, Address>): UtModel =
         if (value.type == VoidType.v()) {
-            ResolvedObject(value.type.classId, value, Unit, emptySet())
+            UtPrimitiveConstraintModel(Parameter("void", value.type.classId), emptySet())
         } else {
-            ResolvedObject(value.type.classId, value, holder.eval(value.expr), collectAtoms(value, addrs))
+            UtPrimitiveConstraintModel(value.expr.accept(varBuilder), collectAtoms(value, addrs))
         }
 
-    private fun resolveReferenceValue(value: ReferenceValue, addrs: Map<UtAddrExpression, Address>): ResolvedObject =
-        ResolvedObject(value.type.classId, value, holder.concreteAddr(value.addr), collectAtoms(value, addrs))
-
-    private val SymbolicValue.asExpr: UtExpression get() = when (this) {
-        is PrimitiveValue -> expr
-        is ReferenceValue -> addr
+    private fun resolveReferenceValue(value: ReferenceValue, addrs: Map<UtAddrExpression, Address>): UtModel {
+        return when (val address = addrs[value.addr]) {
+            NULL_ADDR -> UtNullModel(value.type.classId)
+            in resolvedConstraints -> UtReferenceToConstraintModel(
+                value.addr.accept(varBuilder),
+                resolvedConstraints[address]!!
+            )
+            else -> UtReferenceConstraintModel(
+                value.addr.accept(varBuilder),
+                collectAtoms(value, addrs)
+            ).also {
+                resolvedConstraints[address!!] = it
+            }
+        }
     }
 }
 
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt
@@ -3684,7 +3684,12 @@ class UtBotSymbolicEngine(
         val stateAfter = modelsAfter.constructStateForMethod(state.executionStack.first().method)
         require(stateBefore.parameters.size == stateAfter.parameters.size)
 
-        val resolvedConstraints = ConstraintResolver(updatedMemory, holder).run { resolveModels(resolvedParameters) }
+        val resolvedConstraints = ConstraintResolver(
+            updatedMemory,
+            holder,
+            typeRegistry,
+            typeResolver
+        ).run { resolveModels(resolvedParameters) }
 
         val symbolicUtExecution = UtExecution(
             stateBefore,

diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ValueConstructor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ValueConstructor.kt
@@ -174,6 +174,7 @@ class ValueConstructor {
             is UtArrayModel -> UtConcreteValue(constructArray(model))
             is UtAssembleModel -> UtConcreteValue(constructFromAssembleModel(model))
             is UtVoidModel -> UtConcreteValue(Unit)
+            else -> error("Unexpected ut model: $model")
         }
     }