more expressions supported

UnitTestBot · AbdullinAM · Jun 20, 2022 · Jun 20, 2022 · Jun 22, 2022 · Jun 28, 2022
commit 4a14606d099cf5c918aef66522a5dc9f2cb244df
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
@@ -4,7 +4,11 @@ import org.utbot.framework.plugin.api.util.*
 
 sealed class UtConstraintVariable {
     abstract val classId: ClassId
-    val isPrimitive get() = classId.isPrimitive
+    val isPrimitive get() = try {
+        classId.isPrimitive
+    } catch (e: Throwable) {
+        throw e
+    }
     val isArray get() = classId.isArray
 
     abstract fun <T> accept(visitor: UtConstraintVariableVisitor<T>): T
@@ -288,6 +292,26 @@ data class UtConstraintNot(
     }
 }
 
+data class UtConstraintNeg(
+    val operand: UtConstraintVariable
+) : UtConstraintExpr() {
+    override val classId: ClassId
+        get() = operand.classId
+
+    override fun <T> accept(visitor: UtConstraintVariableVisitor<T>): T {
+        return visitor.visitUtConstraintNeg(this)
+    }
+}
+
+data class UtConstraintCast(
+    val operand: UtConstraintVariable,
+    override val classId: ClassId
+) : UtConstraintExpr() {
+    override fun <T> accept(visitor: UtConstraintVariableVisitor<T>): T {
+        return visitor.visitUtConstraintCast(this)
+    }
+}
+
 sealed class UtConstraint {
     abstract fun negated(): UtConstraint
     abstract fun <T> accept(visitor: UtConstraintVisitor<T>): T

diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/UtConstraintVisitor.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/UtConstraintVisitor.kt
@@ -24,6 +24,10 @@ interface UtConstraintVariableVisitor<T> {
     fun visitUtConstraintUshr(expr: UtConstraintUshr): T
     fun visitUtConstraintXor(expr: UtConstraintXor): T
     fun visitUtConstraintNot(expr: UtConstraintNot): T
+
+    fun visitUtConstraintNeg(expr: UtConstraintNeg): T
+
+    fun visitUtConstraintCast(expr: UtConstraintCast): T
 }
 
 interface UtConstraintVisitor<T> {

diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ConstraintResolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ConstraintResolver.kt
@@ -205,7 +205,7 @@ class ConstraintResolver(
         }.toSet()
         val lengthVariable = UtConstraintArrayLength(variable)
         val lengthModel = buildModel(atoms, lengthVariable, lengths)
-        val concreteLength = holder.eval(lengths.first().expr).value() as Int
+        val concreteLength = lengths.firstOrNull()?.let { holder.eval(it.expr).value() as Int } ?: 100
 
         val indexMap = atoms
             .flatMap {

diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/UtConstraintTransformer.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/UtConstraintTransformer.kt
@@ -146,6 +146,19 @@ class UtConstraintTransformer(
         )
     }
 
+    override fun visitUtConstraintNeg(expr: UtConstraintNeg) = replace(expr) {
+        UtConstraintNeg(
+            operand.accept(this@UtConstraintTransformer)
+        )
+    }
+
+    override fun visitUtConstraintCast(expr: UtConstraintCast) = replace(expr) {
+        UtConstraintCast(
+            operand.accept(this@UtConstraintTransformer),
+            classId
+        )
+    }
+
     override fun visitUtRefEqConstraint(expr: UtRefEqConstraint) = with(expr) {
         UtRefEqConstraint(
             lhv.accept(this@UtConstraintTransformer),

diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/UtConstraintVariableCollector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/UtConstraintVariableCollector.kt
@@ -115,6 +115,14 @@ class UtConstraintVariableCollector(
         expr.operand.accept(this)
     }
 
+    override fun visitUtConstraintNeg(expr: UtConstraintNeg) = visitVar(expr) {
+        expr.operand.accept(this)
+    }
+
+    override fun visitUtConstraintCast(expr: UtConstraintCast) = visitVar(expr) {
+        expr.operand.accept(this)
+    }
+
     override fun visitUtRefEqConstraint(expr: UtRefEqConstraint) = visitConstraint(expr) {
         expr.lhv.accept(this)
         expr.rhv.accept(this)

diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtVarBuilder.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtVarBuilder.kt
@@ -29,22 +29,19 @@ class UtVarBuilder(
                     val instance = expr.index.accept(this)
                     UtConstraintArrayLength(instance)
                 }
-                "RefValues_Arrays" -> {
-                    val instance = expr.index.accept(this)
-                    instance
-                }
-                "char_Arrays" -> {
-                    val instance = expr.index.accept(this)
-                    instance
-                }
-                "int_Arrays" -> {
-                    val instance = expr.index.accept(this)
-                    instance
-                }
+                "RefValues_Arrays" -> expr.index.accept(this)
+                "boolean_Arrays" -> expr.index.accept(this)
+                "char_Arrays" -> expr.index.accept(this)
+                "int_Arrays" -> expr.index.accept(this)
+                "long_Arrays" -> expr.index.accept(this)
+                "byte_Arrays" -> expr.index.accept(this)
+                "short_Arrays" -> expr.index.accept(this)
+                "float_Arrays" -> expr.index.accept(this)
+                "double_Arrays" -> expr.index.accept(this)
                 else -> {
                     val instance = expr.index.accept(this)
                     try {
-                        val (type, field) = base.name.split("_")
+                        val (type, field) = base.name.split("_", limit = 2)
                         UtConstraintFieldAccess(instance, FieldId(ClassId(type), field))
                     } catch (e: Throwable) {
                         arrayAccess(base, instance)
@@ -55,6 +52,7 @@ class UtVarBuilder(
                 val index = expr.index.accept(this)
                 arrayAccess(base, index)
             }
+            is UtConstraintNumericConstant -> expr.index.accept(this)
             is UtConstraintNull -> UtConstraintArrayAccess(base, expr.index.accept(this), objectClassId)
             else -> error("Unexpected: $base")
         }
@@ -77,7 +75,7 @@ class UtVarBuilder(
             System.err.println(base.classId)
             System.err.println(index)
             System.err.println(index.classId)
-            TODO()
+            index
         }
     }
 
@@ -217,11 +215,20 @@ class UtVarBuilder(
     }
 
     override fun visit(expr: UtNegExpression): UtConstraintVariable {
-        TODO("Not yet implemented")
+        return UtConstraintNeg(
+            expr.variable.expr.accept(this)
+        ).also {
+            backMapping[it] = expr.variable.expr
+        }
     }
 
     override fun visit(expr: UtCastExpression): UtConstraintVariable {
-        TODO("Not yet implemented")
+        return UtConstraintCast(
+            expr.variable.expr.accept(this),
+            expr.type.classId
+        ).also {
+            backMapping[it] = expr.variable.expr
+        }
     }
 
     override fun visit(expr: UtBoolOpExpression): UtConstraintVariable {

diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/Synthesizer.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/Synthesizer.kt
@@ -46,7 +46,7 @@ class Synthesizer(
     private val queueIterator = SynthesisUnitContextQueue(parameters, statementStorage, depth)
     private val unitChecker = SynthesisUnitChecker(objectClassId.toSoot())
 
-    fun synthesize(timeLimit: Long = 10000L): List<UtModel>? {
+    fun synthesize(timeLimit: Long = 100000L): List<UtModel>? {
         val currentTime = { System.currentTimeMillis() }
         val startTime = currentTime()
         while (queueIterator.hasNext() && ((currentTime() - startTime) < timeLimit)) {

diff --git a/...framework/synthesis/postcondition/constructors/ConstraintBasedPostConditionConstructor.kt b/...framework/synthesis/postcondition/constructors/ConstraintBasedPostConditionConstructor.kt
@@ -120,7 +120,7 @@ private class UtConstraintBuilder(
                 }
             }
             isArray -> {
-                val sootType = classId.toSootType().arrayType
+                val sootType = classId.toSootType() as ArrayType
                 val addr = UtAddrExpression(mkBVConst("post_condition_${name}", UtIntSort))
                 engine.createArray(addr, sootType, useConcreteType = addr.isThisAddr)
             }
@@ -341,6 +341,20 @@ private class UtConstraintBuilder(
         PrimitiveValue(oper.type, mkNot(oper.expr as UtBoolExpression))
     }
 
+    override fun visitUtConstraintNeg(expr: UtConstraintNeg): SymbolicValue = with(expr) {
+        val oper = operand.accept(this@UtConstraintBuilder) as PrimitiveValue
+        PrimitiveValue(
+            oper.type, UtNegExpression(oper)
+        )
+    }
+
+    override fun visitUtConstraintCast(expr: UtConstraintCast): SymbolicValue = with(expr) {
+        val oper = operand.accept(this@UtConstraintBuilder) as PrimitiveValue
+        PrimitiveValue(
+            oper.type, UtCastExpression(oper, classId.toSootType())
+        )
+    }
+
     override fun visitUtRefEqConstraint(expr: UtRefEqConstraint): UtBoolExpression = with(expr) {
         val lhvVal = lhv.accept(this@UtConstraintBuilder)
         val rhvVal = rhv.accept(this@UtConstraintBuilder)