diff --git a/gradlew b/gradlew old mode 100644 new mode 100755 diff --git a/utbot-cli/src/main/kotlin/org/utbot/cli/GenerateTestsAbstractCommand.kt b/utbot-cli/src/main/kotlin/org/utbot/cli/GenerateTestsAbstractCommand.kt index 83aa105b0f..d8fb42ba6e 100644 --- a/utbot-cli/src/main/kotlin/org/utbot/cli/GenerateTestsAbstractCommand.kt +++ b/utbot-cli/src/main/kotlin/org/utbot/cli/GenerateTestsAbstractCommand.kt @@ -143,8 +143,10 @@ abstract class GenerateTestsAbstractCommand(name: String, help: String) : protected fun getWorkingDirectory(classFqn: String): Path? { val classRelativePath = classFqnToPath(classFqn) + ".class" val classAbsoluteURL = classLoader.getResource(classRelativePath) ?: return null - val classAbsolutePath = replaceSeparator(classAbsoluteURL.toPath().toString()) + val classAbsolutePath = replaceSeparator(classAbsoluteURL.file.removePrefix("file:")) .removeSuffix(classRelativePath) + .removeSuffix("/") + .removeSuffix("!") return Paths.get(classAbsolutePath) } @@ -222,7 +224,9 @@ abstract class GenerateTestsAbstractCommand(name: String, help: String) : protected fun saveToFile(snippet: String, outputPath: String?) = outputPath?.let { - Files.write(it.toPath(), listOf(snippet)) + val path = it.toPath() + path.toFile().parentFile?.mkdirs() + Files.write(path, listOf(snippet)) } protected fun now(): LocalDateTime = LocalDateTime.now() diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt index 43fd1c1856..aa9366296b 100644 --- a/utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt +++ b/utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt @@ -380,6 +380,28 @@ object UtSettings : AbstractSettings( */ var ignoreStaticsFromTrustedLibraries by getBooleanProperty(true) + /** + * Flag for enabling model synthesis + */ + var enableSynthesis by getBooleanProperty(false) + + /** + * Flag for enabling model synthesis + */ + var enableSynthesisCache by getBooleanProperty(true) + + /** + * Timeout model synthesis + * + */ + var synthesisTimeoutInMillis by getLongProperty(60000L) + + /** + * Max depth for synthesis search + * + */ + var synthesisMaxDepth by getIntProperty(10) + /** * Use the sandbox in the concrete executor. * @@ -439,7 +461,12 @@ enum class PathSelectorType { /** * [RandomPathSelector] */ - RANDOM_PATH_SELECTOR + RANDOM_PATH_SELECTOR, + + /** + * [ScoringPathSelector] + */ + SCORING_PATH_SELECTOR } enum class TestSelectionStrategyType { 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 index ad2239497c..0897f3ff1d 100644 --- 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 @@ -136,7 +136,8 @@ class UtSymbolicExecution( coverage: Coverage? = null, summary: List? = null, testMethodName: String? = null, - displayName: String? = null + displayName: String? = null, + val constrainedExecution: ConstrainedExecution? = null ) : UtExecution(stateBefore, stateAfter, result, coverage, summary, testMethodName, displayName) { /** * By design the 'before' and 'after' states contain info about the same fields. @@ -169,7 +170,12 @@ class UtSymbolicExecution( append(")") } - fun copy(stateAfter: EnvironmentModels, result: UtExecutionResult, coverage: Coverage): UtResult { + fun copy( + stateBefore: EnvironmentModels, + stateAfter: EnvironmentModels, + result: UtExecutionResult, + coverage: Coverage?, + ): UtExecution { return UtSymbolicExecution( stateBefore, stateAfter, @@ -180,7 +186,8 @@ class UtSymbolicExecution( coverage, summary, testMethodName, - displayName + displayName, + constrainedExecution ) } } @@ -468,6 +475,80 @@ data class UtArrayModel( } } +/** + * Models for values with constraints + */ +sealed class UtConstraintModel( + open val variable: UtConstraintVariable +) : UtModel(variable.classId) { + abstract val utConstraints: Set +} + +data class UtPrimitiveConstraintModel( + override val variable: UtConstraintVariable, + override val utConstraints: Set, + val concrete: Any? = null +) : UtConstraintModel(variable) { +} + +data class UtReferenceConstraintModel( + override val variable: UtConstraintVariable, + override val utConstraints: Set, +) : UtConstraintModel(variable) { + fun isNull() = utConstraints.any { + it is UtRefEqConstraint && it.lhv == variable && it.rhv is UtConstraintNull + } +} + +data class UtReferenceToConstraintModel( + override val variable: UtConstraintVariable, + val reference: UtModel, + override val utConstraints: Set = emptySet() +) : UtConstraintModel(variable) + +sealed class UtElementContainerConstraintModel( + override val variable: UtConstraintVariable, + open val length: UtModel, + open val elements: Map, + open val baseConstraints: Set = emptySet() +) : UtConstraintModel(variable) { + final override val utConstraints: Set get() = + baseConstraints + elements.toList().fold((length as UtConstraintModel).utConstraints) { acc, pair -> + acc + + ((pair.first as? UtConstraintModel)?.utConstraints ?: emptySet()) + + ((pair.second as? UtConstraintModel)?.utConstraints ?: emptySet()) + } +} + +data class UtArrayConstraintModel( + override val variable: UtConstraintVariable, + override val length: UtModel, + override val elements: Map, + override val baseConstraints: Set = emptySet() +) : UtElementContainerConstraintModel(variable, length, elements) + +data class UtListConstraintModel( + override val variable: UtConstraintVariable, + override val length: UtModel, + override val elements: Map, + override val baseConstraints: Set = emptySet() +) : UtElementContainerConstraintModel(variable, length, elements) + +data class UtSetConstraintModel( + override val variable: UtConstraintVariable, + override val length: UtModel, + override val elements: Map, + override val baseConstraints: Set = emptySet() +) : UtElementContainerConstraintModel(variable, length, elements) + +data class UtMapConstraintModel( + override val variable: UtConstraintVariable, + override val length: UtModel, + override val elements: Map, + override val baseConstraints: Set = emptySet() +) : UtElementContainerConstraintModel(variable, length, elements) + + /** * Model for complex objects with assemble instructions. * 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 new file mode 100644 index 0000000000..6bb11ceb67 --- /dev/null +++ b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/UtConstraintVisitor.kt @@ -0,0 +1,51 @@ +package org.utbot.framework.plugin.api + +interface UtConstraintVariableVisitor { + fun visitUtConstraintParameter(expr: UtConstraintParameter): T + fun visitUtConstraintNull(expr: UtConstraintNull): T + fun visitUtConstraintFieldAccess(expr: UtConstraintFieldAccess): T + fun visitUtConstraintArrayAccess(expr: UtConstraintArrayAccess): T + fun visitUtConstraintArrayLengthAccess(expr: UtConstraintArrayLength): T + fun visitUtConstraintBoolConstant(expr: UtConstraintBoolConstant): T + fun visitUtConstraintCharConstant(expr: UtConstraintCharConstant): T + fun visitUtConstraintNumericConstant(expr: UtConstraintNumericConstant): T + fun visitUtConstraintAdd(expr: UtConstraintAdd): T + fun visitUtConstraintAnd(expr: UtConstraintAnd): T + fun visitUtConstraintCmp(expr: UtConstraintCmp): T + fun visitUtConstraintCmpg(expr: UtConstraintCmpg): T + fun visitUtConstraintCmpl(expr: UtConstraintCmpl): T + fun visitUtConstraintDiv(expr: UtConstraintDiv): T + fun visitUtConstraintMul(expr: UtConstraintMul): T + fun visitUtConstraintOr(expr: UtConstraintOr): T + fun visitUtConstraintRem(expr: UtConstraintRem): T + fun visitUtConstraintShl(expr: UtConstraintShl): T + fun visitUtConstraintShr(expr: UtConstraintShr): T + fun visitUtConstraintSub(expr: UtConstraintSub): 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 { + fun visitUtNegatedConstraint(expr: UtNegatedConstraint): T + + fun visitUtRefEqConstraint(expr: UtRefEqConstraint): T + + fun visitUtRefGenericEqConstraint(expr: UtRefGenericEqConstraint): T + + fun visitUtRefTypeConstraint(expr: UtRefTypeConstraint): T + fun visitUtRefGenericTypeConstraint(expr: UtRefGenericTypeConstraint): T + + fun visitUtBoolConstraint(expr: UtBoolConstraint): T + fun visitUtEqConstraint(expr: UtEqConstraint): T + fun visitUtLtConstraint(expr: UtLtConstraint): T + fun visitUtGtConstraint(expr: UtGtConstraint): T + fun visitUtLeConstraint(expr: UtLeConstraint): T + fun visitUtGeConstraint(expr: UtGeConstraint): T + fun visitUtAndConstraint(expr: UtAndConstraint): T + fun visitUtOrConstraint(expr: UtOrConstraint): T +} diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/constraint/ConstraintApi.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/constraint/ConstraintApi.kt new file mode 100644 index 0000000000..7c6d98a416 --- /dev/null +++ b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/constraint/ConstraintApi.kt @@ -0,0 +1,503 @@ +package org.utbot.framework.plugin.api + +import org.utbot.framework.plugin.api.constraint.UtConstraintVariableCollector +import org.utbot.framework.plugin.api.util.* + +sealed class UtConstraintVariable { + abstract val classId: ClassId + val isPrimitive get() = classId.isPrimitive + val isArray get() = classId.isArray + + abstract fun accept(visitor: UtConstraintVariableVisitor): T +} + +data class UtConstraintNull(override val classId: ClassId) : UtConstraintVariable() { + override fun toString(): String = "null" + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintNull(this) + } +} + +data class UtConstraintParameter( + val name: String, + override val classId: ClassId +) : UtConstraintVariable() { + override fun toString(): String = name + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintParameter(this) + } +} + +data class UtConstraintFieldAccess( + val instance: UtConstraintVariable, + val fieldId: FieldId, +) : UtConstraintVariable() { + override val classId: ClassId + get() = fieldId.type + + override fun toString(): String = "$instance.${fieldId.name}" + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintFieldAccess(this) + } +} + +data class UtConstraintArrayAccess( + val instance: UtConstraintVariable, + val index: UtConstraintVariable, + override val classId: ClassId +) : UtConstraintVariable() { + override fun toString(): String = "$instance[$index]" + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintArrayAccess(this) + } +} + +data class UtConstraintArrayLength( + val instance: UtConstraintVariable, +) : UtConstraintVariable() { + override val classId: ClassId = Integer.TYPE.id + override fun toString(): String = "$instance.length" + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintArrayLengthAccess(this) + } +} + +data class UtConstraintBoolConstant( + val value: Boolean +) : UtConstraintVariable() { + override val classId: ClassId = primitiveModelValueToClassId(value) + + override fun toString(): String = "$value" + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintBoolConstant(this) + } +} + +data class UtConstraintCharConstant( + val value: Char, +) : UtConstraintVariable() { + override val classId: ClassId = primitiveModelValueToClassId(value) + + override fun toString(): String = "$value" + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintCharConstant(this) + } +} + +data class UtConstraintNumericConstant( + val value: Number, +) : UtConstraintVariable() { + override val classId: ClassId = primitiveModelValueToClassId(value) + + override fun toString(): String = "$value" + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintNumericConstant(this) + } +} + +sealed class UtConstraintExpr : UtConstraintVariable() + +sealed class UtConstraintBinExpr( + open val lhv: UtConstraintVariable, + open val rhv: UtConstraintVariable +) : UtConstraintExpr() + +data class UtConstraintAdd( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = lhv.classId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintAdd(this) + } +} + +data class UtConstraintAnd( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = lhv.classId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintAnd(this) + } +} + +data class UtConstraintCmp( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = intClassId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintCmp(this) + } +} + +data class UtConstraintCmpg( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = intClassId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintCmpg(this) + } +} + +data class UtConstraintCmpl( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = intClassId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintCmpl(this) + } +} + +data class UtConstraintDiv( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = lhv.classId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintDiv(this) + } +} + +data class UtConstraintMul( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = lhv.classId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintMul(this) + } +} + +data class UtConstraintOr( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = lhv.classId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintOr(this) + } +} + +data class UtConstraintRem( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = lhv.classId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintRem(this) + } +} + +data class UtConstraintShl( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = lhv.classId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintShl(this) + } +} + +data class UtConstraintShr( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = lhv.classId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintShr(this) + } +} + +data class UtConstraintSub( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = lhv.classId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintSub(this) + } +} + +data class UtConstraintUshr( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = lhv.classId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintUshr(this) + } +} + +data class UtConstraintXor( + override val lhv: UtConstraintVariable, + override val rhv: UtConstraintVariable +) : UtConstraintBinExpr(lhv, rhv) { + override val classId: ClassId + get() = lhv.classId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintXor(this) + } +} + +data class UtConstraintNot( + val operand: UtConstraintVariable +) : UtConstraintExpr() { + override val classId: ClassId + get() = operand.classId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintNot(this) + } +} + +data class UtConstraintNeg( + val operand: UtConstraintVariable +) : UtConstraintExpr() { + override val classId: ClassId + get() = operand.classId + + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintNeg(this) + } +} + +data class UtConstraintCast( + val operand: UtConstraintVariable, + override val classId: ClassId +) : UtConstraintExpr() { + override fun accept(visitor: UtConstraintVariableVisitor): T { + return visitor.visitUtConstraintCast(this) + } +} + +sealed class UtConstraint { + abstract fun negated(): UtConstraint + abstract fun accept(visitor: UtConstraintVisitor): T +} + +data class UtNegatedConstraint(val constraint: UtConstraint) : UtConstraint() { + override fun negated(): UtConstraint = constraint + override fun accept(visitor: UtConstraintVisitor): T { + return visitor.visitUtNegatedConstraint(this) + } + + override fun toString(): String = "!($constraint)" +} + +sealed class UtReferenceConstraint : UtConstraint() + +data class UtRefEqConstraint(val lhv: UtConstraintVariable, val rhv: UtConstraintVariable) : UtReferenceConstraint() { + override fun negated(): UtConstraint = UtNegatedConstraint(this) + + override fun toString(): String = "$lhv == $rhv" + + override fun accept(visitor: UtConstraintVisitor): T { + return visitor.visitUtRefEqConstraint(this) + } +} + +data class UtRefGenericEqConstraint( + val lhv: UtConstraintVariable, + val rhv: UtConstraintVariable, + val mapping: Map +) : UtReferenceConstraint() { + override fun negated(): UtConstraint = UtNegatedConstraint(this) + + override fun toString(): String = "$lhv == $rhv <$mapping>" + + override fun accept(visitor: UtConstraintVisitor): T { + return visitor.visitUtRefGenericEqConstraint(this) + } +} + +data class UtRefTypeConstraint(val operand: UtConstraintVariable, val type: ClassId) : UtReferenceConstraint() { + override fun negated(): UtConstraint = UtNegatedConstraint(this) + + override fun toString(): String = "$operand is $type" + + override fun accept(visitor: UtConstraintVisitor): T { + return visitor.visitUtRefTypeConstraint(this) + } +} + +data class UtRefGenericTypeConstraint( + val operand: UtConstraintVariable, + val base: UtConstraintVariable, + val parameterIndex: Int +) : UtReferenceConstraint() { + override fun negated(): UtConstraint = UtNegatedConstraint(this) + + override fun toString(): String = "$operand is $base<$parameterIndex>" + + override fun accept(visitor: UtConstraintVisitor): T { + return visitor.visitUtRefGenericTypeConstraint(this) + } +} + + +sealed class UtPrimitiveConstraint : UtConstraint() + +data class UtBoolConstraint(val operand: UtConstraintVariable) : UtPrimitiveConstraint() { + override fun negated(): UtConstraint = UtBoolConstraint(UtConstraintNot(operand)) + + override fun accept(visitor: UtConstraintVisitor): T { + return visitor.visitUtBoolConstraint(this) + } +} + +data class UtEqConstraint(val lhv: UtConstraintVariable, val rhv: UtConstraintVariable) : UtPrimitiveConstraint() { + override fun negated(): UtConstraint = UtNegatedConstraint(this) + + override fun toString(): String = "$lhv == $rhv" + + override fun accept(visitor: UtConstraintVisitor): T { + return visitor.visitUtEqConstraint(this) + } +} + +data class UtLtConstraint(val lhv: UtConstraintVariable, val rhv: UtConstraintVariable) : UtPrimitiveConstraint() { + override fun negated(): UtConstraint = UtGeConstraint(lhv, rhv) + + override fun toString(): String = "$lhv < $rhv" + + override fun accept(visitor: UtConstraintVisitor): T { + return visitor.visitUtLtConstraint(this) + } +} + +data class UtGtConstraint(val lhv: UtConstraintVariable, val rhv: UtConstraintVariable) : UtPrimitiveConstraint() { + override fun negated(): UtConstraint = UtLeConstraint(lhv, rhv) + + override fun toString(): String = "$lhv > $rhv" + + override fun accept(visitor: UtConstraintVisitor): T { + return visitor.visitUtGtConstraint(this) + } +} + +data class UtLeConstraint(val lhv: UtConstraintVariable, val rhv: UtConstraintVariable) : UtPrimitiveConstraint() { + override fun negated(): UtConstraint = UtGtConstraint(lhv, rhv) + + override fun toString(): String = "$lhv <= $rhv" + + override fun accept(visitor: UtConstraintVisitor): T { + return visitor.visitUtLeConstraint(this) + } +} + +data class UtGeConstraint(val lhv: UtConstraintVariable, val rhv: UtConstraintVariable) : UtPrimitiveConstraint() { + override fun negated(): UtConstraint = UtLtConstraint(lhv, rhv) + + override fun toString(): String = "$lhv >= $rhv" + + override fun accept(visitor: UtConstraintVisitor): T { + return visitor.visitUtGeConstraint(this) + } +} + +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)" + + override fun accept(visitor: UtConstraintVisitor): T { + return visitor.visitUtAndConstraint(this) + } +} + +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)" + + override fun accept(visitor: UtConstraintVisitor): T { + return visitor.visitUtOrConstraint(this) + } +} + + +fun UtConstraint.flatMap() = flatMap { true } +fun UtConstraint.flatMap(predicate: (UtConstraintVariable) -> Boolean) = + this.accept(UtConstraintVariableCollector(predicate)) + +operator fun UtConstraint.contains(variable: UtConstraintVariable) = this.accept(UtConstraintVariableCollector { + it == variable +}).isNotEmpty() + +operator fun UtConstraint.contains(variables: Set) = + this.accept(UtConstraintVariableCollector { + it in variables + }).isNotEmpty() + +data class ConstrainedExecution( + val modelsBefore: List, + val modelsAfter: List +) + + +val ClassId.defaultVariable: UtConstraintVariable + get() = when (this) { + voidClassId -> error("Unexpected") + booleanClassId -> UtConstraintBoolConstant(false) + charClassId -> UtConstraintCharConstant(0.toChar()) + byteClassId -> UtConstraintNumericConstant(0.toByte()) + shortClassId -> UtConstraintNumericConstant(0.toShort()) + intClassId -> UtConstraintNumericConstant(0) + longClassId -> UtConstraintNumericConstant(0.toLong()) + floatClassId -> UtConstraintNumericConstant(0.toFloat()) + doubleClassId -> UtConstraintNumericConstant(0.toDouble()) + else -> UtConstraintNull(this) + } + +val ClassId.defaultValue: Any + get() = when (this) { + voidClassId -> Unit + booleanClassId -> false + charClassId -> 0.toChar() + byteClassId -> 0.toByte() + shortClassId -> 0.toShort() + intClassId -> 0 + longClassId -> 0.toLong() + floatClassId -> 0.toFloat() + doubleClassId -> 0.toDouble() + else -> UtNullModel(this) + } \ No newline at end of file diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/constraint/UtConstraintTransformer.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/constraint/UtConstraintTransformer.kt new file mode 100644 index 0000000000..5080eb2f59 --- /dev/null +++ b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/constraint/UtConstraintTransformer.kt @@ -0,0 +1,253 @@ +package org.utbot.framework.plugin.api.constraint + +import org.utbot.framework.plugin.api.* + +class UtConstraintTransformer( + val mapping: Map +) : UtConstraintVisitor, UtConstraintVariableVisitor { + + private inline fun replace( + expr: T, + body: T.() -> UtConstraintVariable + ): UtConstraintVariable = mapping.getOrElse(expr) { expr.body() } + + override fun visitUtConstraintParameter(expr: UtConstraintParameter) = replace(expr) { expr } + + override fun visitUtConstraintNull(expr: UtConstraintNull) = replace(expr) { expr } + + override fun visitUtConstraintFieldAccess(expr: UtConstraintFieldAccess) = replace(expr) { + UtConstraintFieldAccess( + instance.accept(this@UtConstraintTransformer), + fieldId + ) + } + + override fun visitUtConstraintArrayAccess(expr: UtConstraintArrayAccess) = replace(expr) { + UtConstraintArrayAccess( + instance.accept(this@UtConstraintTransformer), + index.accept(this@UtConstraintTransformer), + classId + ) + } + + override fun visitUtConstraintArrayLengthAccess(expr: UtConstraintArrayLength) = replace(expr) { + UtConstraintArrayLength( + instance.accept(this@UtConstraintTransformer), + ) + } + + override fun visitUtConstraintBoolConstant(expr: UtConstraintBoolConstant) = replace(expr) { expr } + + override fun visitUtConstraintCharConstant(expr: UtConstraintCharConstant) = replace(expr) { expr } + + override fun visitUtConstraintNumericConstant(expr: UtConstraintNumericConstant) = replace(expr) { expr } + + override fun visitUtConstraintAdd(expr: UtConstraintAdd) = replace(expr) { + UtConstraintAdd( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintAnd(expr: UtConstraintAnd) = replace(expr) { + UtConstraintAnd( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintCmp(expr: UtConstraintCmp) = replace(expr) { + UtConstraintCmp( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintCmpg(expr: UtConstraintCmpg) = replace(expr) { + UtConstraintCmpg( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintCmpl(expr: UtConstraintCmpl) = replace(expr) { + UtConstraintCmpl( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintDiv(expr: UtConstraintDiv) = replace(expr) { + UtConstraintDiv( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintMul(expr: UtConstraintMul) = replace(expr) { + UtConstraintMul( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintOr(expr: UtConstraintOr) = replace(expr) { + UtConstraintOr( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintRem(expr: UtConstraintRem) = replace(expr) { + UtConstraintRem( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintShl(expr: UtConstraintShl) = replace(expr) { + UtConstraintShl( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintShr(expr: UtConstraintShr) = replace(expr) { + UtConstraintShr( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintSub(expr: UtConstraintSub) = replace(expr) { + UtConstraintSub( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintUshr(expr: UtConstraintUshr) = replace(expr) { + UtConstraintUshr( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintXor(expr: UtConstraintXor) = replace(expr) { + UtConstraintXor( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtConstraintNot(expr: UtConstraintNot) = replace(expr) { + UtConstraintNot( + operand.accept(this@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 visitUtNegatedConstraint(expr: UtNegatedConstraint): UtConstraint = with(expr) { + UtNegatedConstraint( + expr.constraint.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtRefEqConstraint(expr: UtRefEqConstraint) = with(expr) { + UtRefEqConstraint( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtRefGenericEqConstraint(expr: UtRefGenericEqConstraint): UtConstraint = with(expr) { + UtRefGenericEqConstraint( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer), + mapping + ) + } + + override fun visitUtRefTypeConstraint(expr: UtRefTypeConstraint) = with(expr) { + UtRefTypeConstraint( + operand.accept(this@UtConstraintTransformer), + type + ) + } + + override fun visitUtRefGenericTypeConstraint(expr: UtRefGenericTypeConstraint): UtConstraint = with(expr) { + UtRefGenericTypeConstraint( + operand.accept(this@UtConstraintTransformer), + base.accept(this@UtConstraintTransformer), + parameterIndex + ) + } + + + override fun visitUtBoolConstraint(expr: UtBoolConstraint) = with(expr) { + UtBoolConstraint( + operand.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtEqConstraint(expr: UtEqConstraint) = with(expr) { + UtEqConstraint( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtLtConstraint(expr: UtLtConstraint) = with(expr) { + UtLtConstraint( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtGtConstraint(expr: UtGtConstraint) = with(expr) { + UtGtConstraint( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtLeConstraint(expr: UtLeConstraint) = with(expr) { + UtLeConstraint( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtGeConstraint(expr: UtGeConstraint) = with(expr) { + UtGeConstraint( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtAndConstraint(expr: UtAndConstraint) = with(expr) { + UtAndConstraint( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } + + override fun visitUtOrConstraint(expr: UtOrConstraint) = with(expr) { + UtOrConstraint( + lhv.accept(this@UtConstraintTransformer), + rhv.accept(this@UtConstraintTransformer) + ) + } +} \ No newline at end of file diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/constraint/UtConstraintVariableCollector.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/constraint/UtConstraintVariableCollector.kt new file mode 100644 index 0000000000..dbfbfda328 --- /dev/null +++ b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/constraint/UtConstraintVariableCollector.kt @@ -0,0 +1,187 @@ +package org.utbot.framework.plugin.api.constraint + +import org.utbot.framework.plugin.api.* + +class UtConstraintVariableCollector( + val predicate: (UtConstraintVariable) -> Boolean +) : UtConstraintVisitor>, UtConstraintVariableVisitor { + private val result = mutableSetOf() + + private inline fun visitVar(expr: UtConstraintVariable, body: () -> Unit) { + if (predicate(expr)) result += expr + body() + } + + private inline fun visitConstraint(expr: UtConstraint, body: () -> Unit): Set { + body() + return result + } + + + override fun visitUtConstraintParameter(expr: UtConstraintParameter) = visitVar(expr) {} + + override fun visitUtConstraintNull(expr: UtConstraintNull) = visitVar(expr) {} + + override fun visitUtConstraintFieldAccess(expr: UtConstraintFieldAccess) = visitVar(expr) { + expr.instance.accept(this) + } + + override fun visitUtConstraintArrayAccess(expr: UtConstraintArrayAccess) = visitVar(expr) { + expr.instance.accept(this) + expr.index.accept(this) + } + + override fun visitUtConstraintArrayLengthAccess(expr: UtConstraintArrayLength) = visitVar(expr) { + expr.instance.accept(this) + } + + override fun visitUtConstraintBoolConstant(expr: UtConstraintBoolConstant) = visitVar(expr) {} + + override fun visitUtConstraintCharConstant(expr: UtConstraintCharConstant) = visitVar(expr) {} + + override fun visitUtConstraintNumericConstant(expr: UtConstraintNumericConstant) = visitVar(expr) {} + + override fun visitUtConstraintAdd(expr: UtConstraintAdd) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintAnd(expr: UtConstraintAnd) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintCmp(expr: UtConstraintCmp) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintCmpg(expr: UtConstraintCmpg) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintCmpl(expr: UtConstraintCmpl) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintDiv(expr: UtConstraintDiv) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintMul(expr: UtConstraintMul) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintOr(expr: UtConstraintOr) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintRem(expr: UtConstraintRem) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintShl(expr: UtConstraintShl) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintShr(expr: UtConstraintShr) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintSub(expr: UtConstraintSub) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintUshr(expr: UtConstraintUshr) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintXor(expr: UtConstraintXor) = visitVar(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtConstraintNot(expr: UtConstraintNot) = visitVar(expr) { + 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 visitUtNegatedConstraint(expr: UtNegatedConstraint) = visitConstraint(expr) { + expr.constraint.accept(this) + } + + override fun visitUtRefEqConstraint(expr: UtRefEqConstraint) = visitConstraint(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtRefGenericEqConstraint(expr: UtRefGenericEqConstraint) = visitConstraint(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtRefTypeConstraint(expr: UtRefTypeConstraint) = visitConstraint(expr) { + expr.operand.accept(this) + } + + override fun visitUtRefGenericTypeConstraint(expr: UtRefGenericTypeConstraint) = visitConstraint(expr) { + expr.operand.accept(this) + expr.base.accept(this) + } + + override fun visitUtBoolConstraint(expr: UtBoolConstraint) = visitConstraint(expr) { + expr.operand.accept(this) + } + + override fun visitUtEqConstraint(expr: UtEqConstraint) = visitConstraint(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtLtConstraint(expr: UtLtConstraint) = visitConstraint(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtGtConstraint(expr: UtGtConstraint) = visitConstraint(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtLeConstraint(expr: UtLeConstraint) = visitConstraint(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtGeConstraint(expr: UtGeConstraint) = visitConstraint(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtAndConstraint(expr: UtAndConstraint) = visitConstraint(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtOrConstraint(expr: UtOrConstraint) = visitConstraint(expr) { + expr.lhv.accept(this) + expr.rhv.accept(this) + } +} \ No newline at end of file diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/util/IdUtil.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/util/IdUtil.kt index 4addbd3f0d..cbc7d51381 100644 --- a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/util/IdUtil.kt +++ b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/util/IdUtil.kt @@ -267,6 +267,7 @@ val atomicIntegerGetAndIncrement = MethodId(atomicIntegerClassId, "getAndIncreme val iterableClassId = java.lang.Iterable::class.id val mapClassId = java.util.Map::class.id +val setClassId = java.util.Set::class.id val dateClassId = java.util.Date::class.id @@ -357,6 +358,9 @@ val ClassId.isIterable: Boolean val ClassId.isMap: Boolean get() = isSubtypeOf(mapClassId) +val ClassId.isSet: Boolean + get() = isSubtypeOf(setClassId) + val ClassId.isIterableOrMap: Boolean get() = isIterable || isMap diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/util/UtContext.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/util/UtContext.kt index 9152d986c3..7555ff9e42 100644 --- a/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/util/UtContext.kt +++ b/utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/util/UtContext.kt @@ -51,7 +51,7 @@ class UtContext(val classLoader: ClassLoader) : ThreadContextElement fun currentContext(): UtContext? = threadLocalContextHolder.get() fun setUtContext(context: UtContext): AutoCloseable = Cookie(context) - private fun restore(contextToRestore : UtContext?) { + private fun restore(contextToRestore: UtContext?) { if (contextToRestore != null) { threadLocalContextHolder.set(contextToRestore) } else { diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/examples/synthesis/SynthesisExamplesTest.kt b/utbot-framework-test/src/test/kotlin/org/utbot/examples/synthesis/SynthesisExamplesTest.kt new file mode 100644 index 0000000000..6e41de7f50 --- /dev/null +++ b/utbot-framework-test/src/test/kotlin/org/utbot/examples/synthesis/SynthesisExamplesTest.kt @@ -0,0 +1,265 @@ +package org.utbot.examples.synthesis + +import org.junit.jupiter.api.AfterAll +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.BeforeEach +import org.utbot.framework.UtSettings +import org.utbot.framework.plugin.api.CodegenLanguage +import org.utbot.framework.synthesis.Synthesizer +import org.utbot.tests.infrastructure.DoNotCalculate +import org.utbot.tests.infrastructure.UtValueTestCaseChecker +import org.utbot.tests.infrastructure.ignoreExecutionsNumber +import org.utbot.tests.infrastructure.isException + +class SynthesisExamplesTest : UtValueTestCaseChecker( + testClass = SynthesisExamples::class, + testCodeGeneration = true, + languagePipelines = listOf( + CodeGenerationLanguageLastStage(CodegenLanguage.JAVA), + // kotlin is turned off, because UtBot Kotlin code generation + // currently does not support collections + // CodeGenerationLanguageLastStage(CodegenLanguage.KOTLIN) + ) +) { + private val initialEnableSynthesizer = UtSettings.enableSynthesis + private val initialEnableSynthesisCache = UtSettings.enableSynthesisCache + private val initialTimeoutInMillis = UtSettings.synthesisTimeoutInMillis + private val initialMaxDepth = UtSettings.synthesisMaxDepth + + companion object { + private const val EPS = 1e5 + } + + @BeforeAll + fun enableSynthesizer() { + UtSettings.enableSynthesis = true + UtSettings.enableSynthesisCache = true + UtSettings.synthesisTimeoutInMillis = 60_000 + UtSettings.synthesisMaxDepth = 10 + } + + @AfterAll + fun disableSynthesizer() { + UtSettings.enableSynthesis = initialEnableSynthesizer + UtSettings.enableSynthesisCache = initialEnableSynthesisCache + UtSettings.synthesisTimeoutInMillis = initialTimeoutInMillis + UtSettings.synthesisMaxDepth = initialMaxDepth + } + + @BeforeEach + fun cleanupSynthesizer() { + Synthesizer.cleanStats() + } + + @Test + fun testSynthesizePoint() { + checkWithException( + SynthesisExamples::synthesizePoint, + ignoreExecutionsNumber, + { _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertEquals(1.0, Synthesizer.successRate, EPS) + } + + @Test + fun testSynthesizeInterface() { + checkWithException( + SynthesisExamples::synthesizeInterface, + ignoreExecutionsNumber, + { _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertEquals(1.0, Synthesizer.successRate, EPS) + } + + @Test + fun testSynthesizeList() { + checkWithException( + SynthesisExamples::synthesizeList, + ignoreExecutionsNumber, + { _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertTrue(Synthesizer.successRate > 0.85) + } + + @Test + fun testSynthesizeSet() { + checkWithException( + SynthesisExamples::synthesizeSet, + ignoreExecutionsNumber, + { _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertTrue(Synthesizer.successRate > 0.5) + } + + @Test + fun testSynthesizeList2() { + checkWithException( + SynthesisExamples::synthesizeList2, + ignoreExecutionsNumber, + { _, _, _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertEquals(1.0, Synthesizer.successRate, EPS) + } + + @Test + fun testSynthesizeObject() { + checkWithException( + SynthesisExamples::synthesizeObject, + ignoreExecutionsNumber, + { _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertEquals(1.0, Synthesizer.successRate, EPS) + } + + @Test + fun testSynthesizeDeepComplexObject() { + checkWithException( + SynthesisExamples::synthesizeDeepComplexObject, + ignoreExecutionsNumber, + { _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertEquals(1.0, Synthesizer.successRate, EPS) + } + + @Test + fun testSynthesizeComplexCounter() { + checkWithException( + SynthesisExamples::synthesizeComplexCounter, + ignoreExecutionsNumber, + { _, _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertEquals(1.0, Synthesizer.successRate, EPS) + } + + @Test + fun testSynthesizeComplexObject() { + checkWithException( + SynthesisExamples::synthesizeComplexObject, + ignoreExecutionsNumber, + { _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertEquals(1.0, Synthesizer.successRate, EPS) + } + + @Test + fun testSynthesizeComplexCounter2() { + checkWithException( + SynthesisExamples::synthesizeComplexCounter2, + ignoreExecutionsNumber, + { _, _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertEquals(1.0, Synthesizer.successRate, EPS) + } + + @Test + fun testSynthesizeComplexCounter3() { + checkWithException( + SynthesisExamples::synthesizeComplexCounter3, + ignoreExecutionsNumber, + { _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertTrue(Synthesizer.successRate > 0.8) + } + + @Test + fun testSynthesizeComplexObject2() { + checkWithException( + SynthesisExamples::synthesizeComplexObject2, + ignoreExecutionsNumber, + { _, _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertEquals(1.0, Synthesizer.successRate, EPS) + } + + @Test + fun testSynthesizeInt() { + checkWithException( + SynthesisExamples::synthesizeInt, + ignoreExecutionsNumber, + { _, _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertEquals(1.0, Synthesizer.successRate, EPS) + } + + @Test + fun testSynthesizeSimpleList() { + checkWithException( + SynthesisExamples::synthesizeSimpleList, + ignoreExecutionsNumber, + { _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertTrue(Synthesizer.successRate > 0.8) + } + + @Test + fun testSynthesizeIntArray() { + checkWithException( + SynthesisExamples::synthesizeIntArray, + ignoreExecutionsNumber, + { _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertTrue(Synthesizer.successRate > 0.8) + } + + @Test + fun testSynthesizePointArray() { + checkWithException( + SynthesisExamples::synthesizePointArray, + ignoreExecutionsNumber, + { _, _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertTrue(Synthesizer.successRate > 0.8) + } + + @Test + fun testSynthesizePointArray2() { + checkWithException( + SynthesisExamples::synthesizePointArray2, + ignoreExecutionsNumber, + { _, _, _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertTrue(Synthesizer.successRate > 0.8) + } + + @Test + fun testSynthesizeDoublePointArray() { + checkWithException( + SynthesisExamples::synthesizeDoublePointArray, + ignoreExecutionsNumber, + { _, _, _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertTrue(Synthesizer.successRate > 0.8) + } + + @Test + fun testSynthesizeInterfaceArray() { + checkWithException( + SynthesisExamples::synthesizeInterfaceArray, + ignoreExecutionsNumber, + { _, _, r -> r.isException() }, + coverage = DoNotCalculate + ) + assertTrue(Synthesizer.successRate > 0.9) + } +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt index 1de5fa185a..8627e56256 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt @@ -300,7 +300,6 @@ val UtSort.defaultValue: UtExpression // empty string because we want to have a default value of the same sort as the items stored in the strings array UtSeqSort -> mkString("") is UtArraySort -> if (itemSort is UtArraySort) nullObjectAddr else mkArrayWithConst(this, itemSort.defaultValue) - else -> nullObjectAddr } /** diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/JimpleCreation.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/JimpleCreation.kt index 4c7887eab9..0607261e66 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/JimpleCreation.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/JimpleCreation.kt @@ -1,28 +1,47 @@ package org.utbot.engine +import soot.Local +import soot.Modifier +import soot.RefType import soot.SootClass import soot.SootMethod import soot.Type import soot.Unit import soot.Value import soot.jimple.AddExpr +import soot.jimple.ArrayRef import soot.jimple.AssignStmt +import soot.jimple.DynamicInvokeExpr import soot.jimple.GeExpr import soot.jimple.GotoStmt import soot.jimple.IdentityStmt import soot.jimple.IfStmt import soot.jimple.IntConstant +import soot.jimple.InterfaceInvokeExpr import soot.jimple.InvokeExpr import soot.jimple.InvokeStmt import soot.jimple.Jimple import soot.jimple.JimpleBody import soot.jimple.NewArrayExpr +import soot.jimple.NewExpr import soot.jimple.ParameterRef import soot.jimple.ReturnStmt import soot.jimple.ReturnVoidStmt +import soot.jimple.SpecialInvokeExpr import soot.jimple.StaticInvokeExpr +import soot.jimple.VirtualInvokeExpr -fun SootMethod.toStaticInvokeExpr(): StaticInvokeExpr = Jimple.v().newStaticInvokeExpr(this.makeRef()) +fun SootMethod.toStaticInvokeExpr(parameters: List = emptyList()): StaticInvokeExpr = + Jimple.v().newStaticInvokeExpr(this.makeRef(), parameters) + +fun SootMethod.toSpecialInvoke(base: Local, parameters: List = emptyList()): SpecialInvokeExpr = + Jimple.v().newSpecialInvokeExpr(base, this.makeRef(), parameters) + +fun SootMethod.toVirtualInvoke(base: Local, parameters: List = emptyList()): VirtualInvokeExpr = + Jimple.v().newVirtualInvokeExpr(base, this.makeRef(), parameters) + +fun SootMethod.toInterfaceInvoke(base: Local, parameters: List = emptyList()): InterfaceInvokeExpr = + Jimple.v().newInterfaceInvokeExpr(base, this.makeRef(), parameters) fun InvokeExpr.toInvokeStmt(): InvokeStmt = Jimple.v().newInvokeStmt(this) @@ -36,6 +55,10 @@ fun identityStmt(local: Value, identityRef: Value): IdentityStmt = Jimple.v().ne fun newArrayExpr(type: Type, size: Value): NewArrayExpr = Jimple.v().newNewArrayExpr(type, size) +fun newArrayRef(base: Value, index: Value): ArrayRef = Jimple.v().newArrayRef(base, index) + +fun newExpr(type: RefType): NewExpr = Jimple.v().newNewExpr(type) + fun assignStmt(variable: Value, rValue: Value): AssignStmt = Jimple.v().newAssignStmt(variable, rValue) fun intConstant(value: Int): IntConstant = IntConstant.v(value) @@ -60,10 +83,14 @@ fun createSootMethod( argsTypes: List, returnType: Type, declaringClass: SootClass, - graphBody: JimpleBody -) = SootMethod(name, argsTypes, returnType) + graphBody: JimpleBody, + isStatic: Boolean = false +) = SootMethod(name, argsTypes, returnType, Modifier.STATIC.takeIf { isStatic } ?: 0) .also { it.declaringClass = declaringClass + if (declaringClass.declaresMethod(it.subSignature)) { + declaringClass.removeMethod(declaringClass.getMethod(it.subSignature)) + } declaringClass.addMethod(it) graphBody.method = it it.activeBody = graphBody diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt index f42f50d63f..395634d24a 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt @@ -79,6 +79,7 @@ import soot.Scene import soot.ShortType import soot.SootClass import soot.SootField +import soot.SootMethod import soot.Type import soot.VoidType import java.awt.color.ICC_ProfileRGB @@ -118,7 +119,7 @@ class Resolver( val typeRegistry: TypeRegistry, private val typeResolver: TypeResolver, val holder: UtSolverStatusSAT, - methodUnderTest: ExecutableId, + packageName: String, private val softMaxArraySize: Int ) { @@ -133,7 +134,7 @@ class Resolver( private val instrumentation = mutableListOf() private val requiredInstanceFields = mutableMapOf>() - private val assembleModelGenerator = AssembleModelGenerator(methodUnderTest.classId.packageName) + private val assembleModelGenerator = AssembleModelGenerator(packageName) /** * Contains FieldId of the static field which is construction at the moment and null of there is no such field. @@ -1238,4 +1239,4 @@ private fun List.mergeExecutables(): MockInfoEnriched { return mockInfoEnriched.copy(executables = methodToExecutables) } -data class ResolvedModels(val parameters: List, val statics: Map) \ No newline at end of file +data class ResolvedModels(val parameters: List, val statics: Map) diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt index d5139836bd..6cbfb404d7 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt @@ -99,6 +99,8 @@ import org.utbot.framework.plugin.api.util.jClass import org.utbot.framework.plugin.api.util.id import org.utbot.framework.plugin.api.util.isConstructor import org.utbot.framework.plugin.api.util.utContext +import org.utbot.framework.synthesis.postcondition.constructors.EmptyPostCondition +import org.utbot.framework.synthesis.postcondition.constructors.PostConditionConstructor import org.utbot.framework.util.executableId import org.utbot.framework.util.graph import org.utbot.framework.util.isInaccessibleViaReflection @@ -202,13 +204,14 @@ import kotlin.reflect.jvm.javaType private val CAUGHT_EXCEPTION = LocalVariable("@caughtexception") class Traverser( - private val methodUnderTest: ExecutableId, + private val methodUnderTest: SymbolicEngineTarget, internal val typeRegistry: TypeRegistry, internal val hierarchy: Hierarchy, // TODO HACK violation of encapsulation internal val typeResolver: TypeResolver, private val globalGraph: InterProceduralUnitGraph, private val mocker: Mocker, + private val postConditionConstructor: PostConditionConstructor = EmptyPostCondition, ) : UtContextInitializer() { private val visitedStmts: MutableSet = mutableSetOf() @@ -218,6 +221,9 @@ class Traverser( // TODO: move this and other mutable fields to [TraversalContext] lateinit var environment: Environment + + val isInitialized get() = this::environment.isInitialized + private val solver: UtSolver get() = environment.state.solver @@ -238,7 +244,7 @@ class Traverser( private val preferredCexInstanceCache = mutableMapOf>() - private var queuedSymbolicStateUpdates = SymbolicStateUpdate() + internal var queuedSymbolicStateUpdates = SymbolicStateUpdate() private val objectCounter = AtomicInteger(TypeRegistry.objectCounterInitialValue) private fun findNewAddr(insideStaticInitializer: Boolean): UtAddrExpression { @@ -959,12 +965,16 @@ class Traverser( * Stores information about the generic types used in the parameters of the method under test. */ private fun updateGenericTypeInfo(identityRef: IdentityRef, value: ReferenceValue) { - val callable = methodUnderTest.executable + val executableId = when (methodUnderTest) { + is ExecutableIdTarget -> methodUnderTest.executableId + else -> return + } + val callable = executableId.executable val kCallable = ::updateGenericTypeInfo val test = kCallable.instanceParameter?.type?.javaType val type = if (identityRef is ThisRef) { // TODO: for ThisRef both methods don't return parameterized type - if (methodUnderTest.isConstructor) { + if (executableId.isConstructor) { callable.annotatedReturnType?.type } else { callable.declaringClass // same as it was, but it isn't parametrized type @@ -2050,12 +2060,12 @@ class Traverser( else -> error("Can't create const from ${type::class}") } - private fun createEnum(type: RefType, addr: UtAddrExpression): ObjectValue { + internal fun createEnum(type: RefType, addr: UtAddrExpression, concreteOrdinal: Int? = null): ObjectValue { val typeStorage = typeResolver.constructTypeStorage(type, useConcreteType = true) queuedSymbolicStateUpdates += typeRegistry.typeConstraint(addr, typeStorage).all().asHardConstraint() - val ordinal = findEnumOrdinal(type, addr) + val ordinal = concreteOrdinal?.let { it.primitiveToSymbolic() } ?: findEnumOrdinal(type, addr) val enumSize = classLoader.loadClass(type.sootClass.name).enumConstants.size queuedSymbolicStateUpdates += mkOr(Ge(ordinal, 0), addrEq(addr, nullObjectAddr)).asHardConstraint() @@ -2067,6 +2077,16 @@ class Traverser( return ObjectValue(typeStorage, addr) } + internal fun createClassRef(sootType: Type): SymbolicValue { + val result = if (sootType is RefLikeType) { + typeRegistry.createClassRef(sootType.baseType, sootType.numDimensions) + } else { + error("Can't get class constant for $sootType") + } + queuedSymbolicStateUpdates += result.symbolicStateUpdate + return (result.symbolicResult as SymbolicSuccess).value + } + private fun arrayUpdate(array: ArrayValue, index: PrimitiveValue, value: UtExpression): MemoryUpdate { val type = array.type val chunkId = typeRegistry.arrayChunkId(type) @@ -2112,7 +2132,7 @@ class Traverser( return memory.findArray(descriptor).select(addr) } - private fun touchMemoryChunk(chunkDescriptor: MemoryChunkDescriptor) { + internal fun touchMemoryChunk(chunkDescriptor: MemoryChunkDescriptor) { queuedSymbolicStateUpdates += MemoryUpdate(touchedChunkDescriptors = persistentSetOf(chunkDescriptor)) } @@ -2129,7 +2149,7 @@ class Traverser( * * If the field belongs to a substitute object, record the read access for the real type instead. */ - private fun recordInstanceFieldRead(addr: UtAddrExpression, field: SootField) { + internal fun recordInstanceFieldRead(addr: UtAddrExpression, field: SootField) { val realType = typeRegistry.findRealType(field.declaringClass.type) if (realType is RefType) { val readOperation = InstanceFieldReadOperation(addr, FieldId(realType.id, field.name)) @@ -3418,6 +3438,14 @@ class Traverser( queuedSymbolicStateUpdates += mkNot(mkEq(symbolicResult.value.addr, nullObjectAddr)).asHardConstraint() } + if (!environment.state.isInNestedMethod()) { + val postConditionUpdates = postConditionConstructor.constructPostCondition( + this@Traverser, + symbolicResult + ) + queuedSymbolicStateUpdates += postConditionUpdates + } + val symbolicState = environment.state.symbolicState + queuedSymbolicStateUpdates val memory = symbolicState.memory val solver = symbolicState.solver @@ -3484,4 +3512,4 @@ class Traverser( queuedSymbolicStateUpdates = prevSymbolicStateUpdate } } -} \ No newline at end of file +} diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt index 0a154100f8..a831719775 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt @@ -7,6 +7,7 @@ import org.utbot.analytics.Predictors import org.utbot.common.bracket import org.utbot.common.debug import org.utbot.engine.MockStrategy.NO_MOCKS +import org.utbot.engine.constraints.ConstraintResolver import org.utbot.engine.pc.UtArraySelectExpression import org.utbot.engine.pc.UtBoolExpression import org.utbot.engine.pc.UtContextInitializer @@ -15,19 +16,9 @@ import org.utbot.engine.pc.UtSolverStatusSAT import org.utbot.engine.pc.findTheMostNestedAddr import org.utbot.engine.pc.mkEq import org.utbot.engine.pc.mkInt -import org.utbot.engine.selectors.PathSelector -import org.utbot.engine.selectors.StrategyOption -import org.utbot.engine.selectors.coveredNewSelector -import org.utbot.engine.selectors.cpInstSelector -import org.utbot.engine.selectors.forkDepthSelector -import org.utbot.engine.selectors.inheritorsSelector -import org.utbot.engine.selectors.mlSelector +import org.utbot.engine.selectors.* import org.utbot.engine.selectors.nurs.NonUniformRandomSearch -import org.utbot.engine.selectors.pollUntilFastSAT -import org.utbot.engine.selectors.randomPathSelector -import org.utbot.engine.selectors.randomSelector import org.utbot.engine.selectors.strategies.GraphViz -import org.utbot.engine.selectors.subpathGuidedSelector import org.utbot.engine.symbolic.SymbolicState import org.utbot.engine.symbolic.asHardConstraint import org.utbot.engine.util.mockListeners.MockListener @@ -36,28 +27,13 @@ import org.utbot.framework.PathSelectorType import org.utbot.framework.UtSettings import org.utbot.framework.UtSettings.checkSolverTimeoutMillis import org.utbot.framework.UtSettings.enableFeatureProcess +import org.utbot.framework.UtSettings.enableSynthesis import org.utbot.framework.UtSettings.pathSelectorStepsLimit -import org.utbot.framework.UtSettings.pathSelectorType import org.utbot.framework.UtSettings.processUnknownStatesDuringConcreteExecution import org.utbot.framework.UtSettings.useDebugVisualization import org.utbot.framework.concrete.UtConcreteExecutionData import org.utbot.framework.concrete.UtConcreteExecutionResult import org.utbot.framework.concrete.UtExecutionInstrumentation -import org.utbot.framework.plugin.api.ClassId -import org.utbot.framework.plugin.api.ConcreteExecutionFailureException -import org.utbot.framework.plugin.api.EnvironmentModels -import org.utbot.framework.plugin.api.ExecutableId -import org.utbot.framework.plugin.api.Instruction -import org.utbot.framework.plugin.api.Step -import org.utbot.framework.plugin.api.UtAssembleModel -import org.utbot.framework.plugin.api.UtConcreteExecutionFailure -import org.utbot.framework.plugin.api.UtError -import org.utbot.framework.plugin.api.UtFailedExecution -import org.utbot.framework.plugin.api.UtInstrumentation -import org.utbot.framework.plugin.api.UtNullModel -import org.utbot.framework.plugin.api.UtOverflowFailure -import org.utbot.framework.plugin.api.UtResult -import org.utbot.framework.plugin.api.UtSymbolicExecution import org.utbot.framework.util.graph import org.utbot.framework.plugin.api.util.isStatic import org.utbot.framework.plugin.api.util.description @@ -66,7 +42,8 @@ import org.utbot.framework.plugin.api.util.isConstructor import org.utbot.framework.plugin.api.util.isEnum import org.utbot.framework.plugin.api.util.utContext import org.utbot.framework.plugin.api.util.voidClassId -import org.utbot.framework.util.sootMethod +import org.utbot.framework.synthesis.postcondition.constructors.EmptyPostCondition +import org.utbot.framework.synthesis.postcondition.constructors.PostConditionConstructor import org.utbot.fuzzer.FallbackModelProvider import org.utbot.fuzzer.FuzzedMethodDescription import org.utbot.fuzzer.FuzzedValue @@ -83,8 +60,11 @@ import org.utbot.fuzzer.fuzz import org.utbot.fuzzer.providers.ObjectModelProvider import org.utbot.fuzzer.withMutations import org.utbot.instrumentation.ConcreteExecutor +import org.utbot.summary.jimpleBody +import soot.SootMethod import soot.jimple.Stmt import soot.tagkit.ParamNamesTag +import soot.toolkits.graph.ExceptionalUnitGraph import java.lang.reflect.Method import kotlin.random.Random import kotlin.system.measureTimeMillis @@ -101,6 +81,9 @@ import kotlinx.coroutines.flow.onStart import kotlinx.coroutines.isActive import kotlinx.coroutines.job import kotlinx.coroutines.yield +import org.utbot.framework.plugin.api.* +import org.utbot.framework.plugin.api.Step +import org.utbot.framework.util.sootMethod val logger = KotlinLogging.logger {} val pathLogger = KotlinLogging.logger(logger.name + ".path") @@ -116,56 +99,103 @@ class EngineController { //for debugging purpose only private var stateSelectedCount = 0 -private val defaultIdGenerator = ReferencePreservingIntIdGenerator() +internal val defaultIdGenerator = ReferencePreservingIntIdGenerator() -private fun pathSelector(graph: InterProceduralUnitGraph, typeRegistry: TypeRegistry) = - when (pathSelectorType) { - PathSelectorType.COVERED_NEW_SELECTOR -> coveredNewSelector(graph) { - withStepsLimit(pathSelectorStepsLimit) - } - PathSelectorType.INHERITORS_SELECTOR -> inheritorsSelector(graph, typeRegistry) { - withStepsLimit(pathSelectorStepsLimit) - } - PathSelectorType.SUBPATH_GUIDED_SELECTOR -> subpathGuidedSelector(graph, StrategyOption.DISTANCE) { - withStepsLimit(pathSelectorStepsLimit) - } - PathSelectorType.CPI_SELECTOR -> cpInstSelector(graph, StrategyOption.DISTANCE) { - withStepsLimit(pathSelectorStepsLimit) - } - PathSelectorType.FORK_DEPTH_SELECTOR -> forkDepthSelector(graph, StrategyOption.DISTANCE) { - withStepsLimit(pathSelectorStepsLimit) - } - PathSelectorType.ML_SELECTOR -> mlSelector(graph, StrategyOption.DISTANCE) { - withStepsLimit(pathSelectorStepsLimit) - } - PathSelectorType.TORCH_SELECTOR -> mlSelector(graph, StrategyOption.DISTANCE) { - withStepsLimit(pathSelectorStepsLimit) - } - PathSelectorType.RANDOM_SELECTOR -> randomSelector(graph, StrategyOption.DISTANCE) { - withStepsLimit(pathSelectorStepsLimit) - } - PathSelectorType.RANDOM_PATH_SELECTOR -> randomPathSelector(graph, StrategyOption.DISTANCE) { - withStepsLimit(pathSelectorStepsLimit) - } +private fun pathSelector( + graph: InterProceduralUnitGraph, + traverser: Traverser, + pathSelectorType: PathSelectorType, + postConditionConstructor: PostConditionConstructor +) = when (pathSelectorType) { + PathSelectorType.COVERED_NEW_SELECTOR -> coveredNewSelector(graph) { + withStepsLimit(pathSelectorStepsLimit) + } + + PathSelectorType.INHERITORS_SELECTOR -> inheritorsSelector(graph, traverser.typeRegistry) { + withStepsLimit(pathSelectorStepsLimit) + } + + PathSelectorType.SUBPATH_GUIDED_SELECTOR -> subpathGuidedSelector(graph, StrategyOption.DISTANCE) { + withStepsLimit(pathSelectorStepsLimit) + } + + PathSelectorType.CPI_SELECTOR -> cpInstSelector(graph, StrategyOption.DISTANCE) { + withStepsLimit(pathSelectorStepsLimit) + } + + PathSelectorType.FORK_DEPTH_SELECTOR -> forkDepthSelector(graph, StrategyOption.DISTANCE) { + withStepsLimit(pathSelectorStepsLimit) + } + + PathSelectorType.ML_SELECTOR -> mlSelector(graph, StrategyOption.DISTANCE) { + withStepsLimit(pathSelectorStepsLimit) + } + + PathSelectorType.TORCH_SELECTOR -> mlSelector(graph, StrategyOption.DISTANCE) { + withStepsLimit(pathSelectorStepsLimit) + } + + PathSelectorType.RANDOM_SELECTOR -> randomSelector(graph, StrategyOption.DISTANCE) { + withStepsLimit(pathSelectorStepsLimit) + } + + PathSelectorType.RANDOM_PATH_SELECTOR -> randomPathSelector(graph, StrategyOption.DISTANCE) { + withStepsLimit(pathSelectorStepsLimit) + } + + PathSelectorType.SCORING_PATH_SELECTOR -> scoringPathSelector( + graph, + postConditionConstructor.scoringBuilder().build(graph, traverser) + ) { + withStepsLimit(pathSelectorStepsLimit) + } +} + +sealed class SymbolicEngineTarget { + abstract val graph: ExceptionalUnitGraph + abstract val classId: ClassId + abstract val sootMethod: SootMethod + + val packageName: String get() = sootMethod.declaringClass.packageName + + companion object { + fun from(utMethod: ExecutableId) = ExecutableIdTarget(utMethod) + fun from(sootMethod: SootMethod) = SootMethodTarget(sootMethod) } +} + +data class ExecutableIdTarget( + val executableId: ExecutableId +) : SymbolicEngineTarget() { + override val graph: ExceptionalUnitGraph = executableId.sootMethod.jimpleBody().graph() + override val classId: ClassId = executableId.classId + override val sootMethod: SootMethod = graph.body.method +} + +data class SootMethodTarget( + override val sootMethod: SootMethod +) : SymbolicEngineTarget() { + override val graph: ExceptionalUnitGraph = sootMethod.jimpleBody().graph() + override val classId: ClassId = sootMethod.declaringClass.id +} class UtBotSymbolicEngine( private val controller: EngineController, - private val methodUnderTest: ExecutableId, + private val methodUnderTest: SymbolicEngineTarget, classpath: String, dependencyPaths: String, mockStrategy: MockStrategy = NO_MOCKS, chosenClassesToMockAlways: Set, - private val solverTimeoutInMillis: Int = checkSolverTimeoutMillis + private val solverTimeoutInMillis: Int = checkSolverTimeoutMillis, + private val useSynthesis: Boolean = enableSynthesis, + private val postConditionConstructor: PostConditionConstructor = EmptyPostCondition, + private val pathSelectorType: PathSelectorType = UtSettings.pathSelectorType ) : UtContextInitializer() { - private val graph = methodUnderTest.sootMethod.jimpleBody().apply { - logger.trace { "JIMPLE for $methodUnderTest:\n$this" } - }.graph() + private val graph get() = methodUnderTest.graph private val methodUnderAnalysisStmts: Set = graph.stmts.toSet() private val globalGraph = InterProceduralUnitGraph(graph) private val typeRegistry: TypeRegistry = TypeRegistry() - private val pathSelector: PathSelector = pathSelector(globalGraph, typeRegistry) internal val hierarchy: Hierarchy = Hierarchy(typeRegistry) @@ -195,17 +225,24 @@ class UtBotSymbolicEngine( typeResolver, globalGraph, mocker, + postConditionConstructor + ) + + private val pathSelector: PathSelector = pathSelector( + globalGraph, + traverser, + pathSelectorType, + postConditionConstructor ) //HACK (long strings) internal var softMaxArraySize = 40 - private val concreteExecutor = - ConcreteExecutor( - UtExecutionInstrumentation, - classpath, - dependencyPaths - ).apply { this.classLoader = utContext.classLoader } + private val concreteExecutor = ConcreteExecutor( + UtExecutionInstrumentation, + classpath, + dependencyPaths + ).apply { this.classLoader = utContext.classLoader } private val featureProcessor: FeatureProcessor? = if (enableFeatureProcess) EngineAnalyticsContext.featureProcessorFactory(globalGraph) else null @@ -245,7 +282,7 @@ class UtBotSymbolicEngine( val initState = ExecutionState( initStmt, SymbolicState(UtSolver(typeRegistry, trackableResources, solverTimeoutInMillis)), - executionStack = persistentListOf(ExecutionStackElement(null, method = graph.body.method)) + executionStack = persistentListOf(ExecutionStackElement(null, method = methodUnderTest.sootMethod)) ) pathSelector.offer(initState) @@ -289,36 +326,40 @@ class UtBotSymbolicEngine( typeRegistry, typeResolver, state.solver.lastStatus as UtSolverStatusSAT, - methodUnderTest, + methodUnderTest.packageName, softMaxArraySize ) val resolvedParameters = state.methodUnderTestParameters val (modelsBefore, _, instrumentation) = resolver.resolveModels(resolvedParameters) - val stateBefore = modelsBefore.constructStateForMethod(methodUnderTest) - - try { - val concreteExecutionResult = - concreteExecutor.executeConcretely(methodUnderTest, stateBefore, instrumentation) - - val concreteUtExecution = UtSymbolicExecution( - stateBefore, - concreteExecutionResult.stateAfter, - concreteExecutionResult.result, - instrumentation, - mutableListOf(), - listOf(), - concreteExecutionResult.coverage - ) - emit(concreteUtExecution) - - logger.debug { "concolicStrategy<${methodUnderTest}>: returned $concreteUtExecution" } - } catch (e: CancellationException) { - logger.debug(e) { "Cancellation happened" } - } catch (e: ConcreteExecutionFailureException) { - emitFailedConcreteExecutionResult(stateBefore, e) - } catch (e: Throwable) { - emit(UtError("Concrete execution failed", e)) + + if (methodUnderTest is ExecutableIdTarget) { + val executableId = methodUnderTest.executableId + val stateBefore = modelsBefore.constructStateForMethod(executableId) + + try { + val concreteExecutionResult = + concreteExecutor.executeConcretely(executableId, stateBefore, instrumentation) + + val concreteUtExecution = UtSymbolicExecution( + stateBefore, + concreteExecutionResult.stateAfter, + concreteExecutionResult.result, + instrumentation, + mutableListOf(), + listOf(), + concreteExecutionResult.coverage + ) + emit(concreteUtExecution) + + logger.debug { "concolicStrategy<${methodUnderTest}>: returned $concreteUtExecution" } + } catch (e: CancellationException) { + logger.debug(e) { "Cancellation happened" } + } catch (e: ConcreteExecutionFailureException) { + emitFailedConcreteExecutionResult(stateBefore, e) + } catch (e: Throwable) { + emit(UtError("Concrete execution failed", e)) + } } } @@ -379,9 +420,13 @@ class UtBotSymbolicEngine( * @param modelProvider provides model values for a method */ fun fuzzing(until: Long = Long.MAX_VALUE, modelProvider: (ModelProvider) -> ModelProvider = { it }) = flow { - val isFuzzable = methodUnderTest.parameters.all { classId -> + val executableId = when (methodUnderTest) { + is ExecutableIdTarget -> methodUnderTest.executableId + else -> return@flow + } + val isFuzzable = executableId.parameters.all { classId -> classId != Method::class.java.id && // causes the child process crash at invocation - classId != Class::class.java.id // causes java.lang.IllegalAccessException: java.lang.Class at sun.misc.Unsafe.allocateInstance(Native Method) + classId != Class::class.java.id // causes java.lang.IllegalAccessException: java.lang.Class at sun.misc.Unsafe.allocateInstance(Native Method) } if (!isFuzzable) { return@flow @@ -398,8 +443,8 @@ class UtBotSymbolicEngine( val random = Random(0) val thisInstance = when { - methodUnderTest.isStatic -> null - methodUnderTest.isConstructor -> if ( + executableId.isStatic -> null + executableId.isConstructor -> if ( classUnderTest.isAbstract || // can't instantiate abstract class classUnderTest.isEnum // can't reflectively create enum objects ) { @@ -407,6 +452,7 @@ class UtBotSymbolicEngine( } else { null } + else -> { ObjectModelProvider(defaultIdGenerator).withFallback(fallbackModelProvider).generate( syntheticMethodForFuzzingThisInstanceDescription @@ -418,8 +464,8 @@ class UtBotSymbolicEngine( } } - val methodUnderTestDescription = FuzzedMethodDescription(methodUnderTest, collectConstantsForFuzzer(graph)).apply { - compilableName = if (!methodUnderTest.isConstructor) methodUnderTest.name else null + val methodUnderTestDescription = FuzzedMethodDescription(executableId, collectConstantsForFuzzer(graph)).apply { + compilableName = if (!executableId.isConstructor) executableId.name else null className = classUnderTest.simpleName packageName = classUnderTest.packageName val names = graph.body.method.tags.filterIsInstance().firstOrNull()?.names @@ -429,7 +475,7 @@ class UtBotSymbolicEngine( val coveredInstructionValues = linkedMapOf, List>() var attempts = 0 val attemptsLimit = UtSettings.fuzzingMaxAttempts - val hasMethodUnderTestParametersToFuzz = methodUnderTest.parameters.isNotEmpty() + val hasMethodUnderTestParametersToFuzz = executableId.parameters.isNotEmpty() val fuzzedValues = if (hasMethodUnderTestParametersToFuzz) { fuzz(methodUnderTestDescription, modelProvider(defaultModelProviders(defaultIdGenerator))) } else { @@ -438,7 +484,9 @@ class UtBotSymbolicEngine( totalLimit = 500 }) }.withMutations( - TrieBasedFuzzerStatistics(coveredInstructionValues), methodUnderTestDescription, *defaultModelMutators().toTypedArray() + TrieBasedFuzzerStatistics(coveredInstructionValues), + methodUnderTestDescription, + *defaultModelMutators().toTypedArray() ) fuzzedValues.forEach { values -> if (controller.job?.isActive == false || System.currentTimeMillis() >= until) { @@ -454,7 +502,7 @@ class UtBotSymbolicEngine( } val concreteExecutionResult: UtConcreteExecutionResult? = try { - concreteExecutor.executeConcretely(methodUnderTest, initialEnvironmentModels, listOf()) + concreteExecutor.executeConcretely(executableId, initialEnvironmentModels, listOf()) } catch (e: CancellationException) { logger.debug { "Cancelled by timeout" }; null } catch (e: ConcreteExecutionFailureException) { @@ -527,24 +575,42 @@ class UtBotSymbolicEngine( Predictors.testName.provide(state.path, predictedTestName, "") // resolving - val resolver = - Resolver(hierarchy, memory, typeRegistry, typeResolver, holder, methodUnderTest, softMaxArraySize) + val resolver = Resolver( + hierarchy, + memory, + typeRegistry, + typeResolver, + holder, + methodUnderTest.packageName, + softMaxArraySize + ) val (modelsBefore, modelsAfter, instrumentation) = resolver.resolveModels(parameters) val symbolicExecutionResult = resolver.resolveResult(symbolicResult) - val stateBefore = modelsBefore.constructStateForMethod(methodUnderTest) - val stateAfter = modelsAfter.constructStateForMethod(methodUnderTest) + val stateBefore = modelsBefore.constructStateForMethod(methodUnderTest.sootMethod) + val stateAfter = modelsAfter.constructStateForMethod(methodUnderTest.sootMethod) require(stateBefore.parameters.size == stateAfter.parameters.size) + val resolvedConstraints = if (useSynthesis) { + ConstraintResolver( + memory, + holder, + solver.query, + typeRegistry, + typeResolver + ).run { resolveModels(parameters) } + } else null + val symbolicUtExecution = UtSymbolicExecution( stateBefore = stateBefore, stateAfter = stateAfter, result = symbolicExecutionResult, instrumentation = instrumentation, path = entryMethodPath(state), - fullPath = state.fullPath() + fullPath = state.fullPath(), + constrainedExecution = resolvedConstraints ) globalGraph.traversed(state) @@ -564,27 +630,41 @@ class UtBotSymbolicEngine( //It's possible that symbolic and concrete stateAfter/results are diverged. //So we trust concrete results more. - try { - logger.debug().bracket("processResult<$methodUnderTest>: concrete execution") { - - //this can throw CancellationException - val concreteExecutionResult = concreteExecutor.executeConcretely( - methodUnderTest, - stateBefore, - instrumentation - ) + when (methodUnderTest) { + is ExecutableIdTarget -> { + try { + logger.debug().bracket("processResult<$methodUnderTest>: concrete execution") { + + //this can throw CancellationException + val concreteExecutionResult = concreteExecutor.executeConcretely( + methodUnderTest.executableId, + stateBefore, + instrumentation + ) - val concolicUtExecution = symbolicUtExecution.copy( - stateAfter = concreteExecutionResult.stateAfter, - result = concreteExecutionResult.result, - coverage = concreteExecutionResult.coverage - ) + val concolicUtExecution = symbolicUtExecution.copy( + stateBefore = symbolicUtExecution.stateBefore, + stateAfter = concreteExecutionResult.stateAfter, + result = concreteExecutionResult.result, + coverage = concreteExecutionResult.coverage + ) - emit(concolicUtExecution) - logger.debug { "processResult<${methodUnderTest}>: returned $concolicUtExecution" } + emit(concolicUtExecution) + logger.debug { "processResult<${methodUnderTest}>: returned $concolicUtExecution" } + } + } catch (e: ConcreteExecutionFailureException) { + emitFailedConcreteExecutionResult(stateBefore, e) + } + } + + is SootMethodTarget -> { + logger.debug { + "processResult<${methodUnderTest}>: no concrete execution allowed, " + + "emit purely symbolic result $symbolicUtExecution" + } + emit(symbolicUtExecution) + return } - } catch (e: ConcreteExecutionFailureException) { - emitFailedConcreteExecutionResult(stateBefore, e) } } @@ -614,7 +694,16 @@ private fun ResolvedModels.constructStateForMethod(methodUnderTest: ExecutableId return EnvironmentModels(thisInstanceBefore, paramsBefore, statics) } -private suspend fun ConcreteExecutor.executeConcretely( +private fun ResolvedModels.constructStateForMethod(method: SootMethod): EnvironmentModels { + val (thisInstanceBefore, paramsBefore) = when { + method.isStatic -> null to parameters + method.isConstructor -> null to parameters.drop(1) + else -> parameters.first() to parameters.drop(1) + } + return EnvironmentModels(thisInstanceBefore, paramsBefore, statics) +} + +internal suspend fun ConcreteExecutor.executeConcretely( methodUnderTest: ExecutableId, stateBefore: EnvironmentModels, instrumentation: List diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ValueConstructor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ValueConstructor.kt index bcef64e327..dbad2748f6 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/ValueConstructor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/ValueConstructor.kt @@ -195,6 +195,7 @@ class ValueConstructor { is UtAssembleModel -> UtConcreteValue(constructFromAssembleModel(model)) is UtLambdaModel -> UtConcreteValue(constructFromLambdaModel(model)) is UtVoidModel -> UtConcreteValue(Unit) + else -> error("Unexpected ut model: $model") } } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/constraints/ConstraintResolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/constraints/ConstraintResolver.kt new file mode 100644 index 0000000000..f5f38baeec --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/constraints/ConstraintResolver.kt @@ -0,0 +1,453 @@ +package org.utbot.engine.constraints + +import org.utbot.engine.* +import org.utbot.engine.pc.* +import org.utbot.engine.pc.constraint.UtVarContext +import org.utbot.framework.plugin.api.* +import org.utbot.framework.plugin.api.constraint.UtConstraintTransformer +import org.utbot.framework.plugin.api.constraint.UtConstraintVariableCollector +import org.utbot.framework.plugin.api.util.intClassId +import org.utbot.framework.plugin.api.util.isPrimitive +import org.utbot.framework.plugin.api.util.objectClassId + +/** + * Constructs path conditions using calculated model. Can construct them for initial and current memory states that reflect + * initial parameters or current values for concrete call. + */ +class ConstraintResolver( + private val memory: Memory, + private val holder: UtSolverStatusSAT, + private val query: BaseQuery, + typeRegistry: TypeRegistry, + typeResolver: TypeResolver, + private val useSoftConstraints: Boolean = false +) { + companion object { + private const val MAX_ARRAY_LENGTH = 10 + } + + lateinit var state: MemoryState + private val variableContext: UtVarContext = UtVarContext(holder, typeRegistry, typeResolver) + private val resolvedConstraints = mutableMapOf() + + /** + * Contains FieldId of the static field which is construction at the moment and null of there is no such field. + * It is used to find initial state for the fieldId in the [Memory.findArray] method. + */ + private var staticFieldUnderResolving: FieldId? = null + + private fun clearState() { + resolvedConstraints.clear() + resolvedConstraints.clear() + } + + private inline fun withMemoryState(state: MemoryState, block: () -> T): T { + try { + this.state = state + clearState() + return block() + } finally { + clearState() + } + } + + private inline fun withStaticMemoryState(staticFieldUnderResolving: FieldId, block: () -> T): T { + return if (state == MemoryState.INITIAL) { + try { + this.staticFieldUnderResolving = staticFieldUnderResolving + this.state = MemoryState.STATIC_INITIAL + block() + } finally { + this.staticFieldUnderResolving = null + this.state = MemoryState.INITIAL + } + } else { + block() + } + } + + private inline fun traverseQuery(action: (UtExpression) -> Unit) { + query.hard.forEach(action) + if (useSoftConstraints) { + query.soft.forEach(action) + } + } + + + internal fun resolveModels(parameters: List): ConstrainedExecution { + val allAddresses = UtExprCollector { it is UtAddrExpression }.let { + traverseQuery { constraint -> + constraint.accept(it) + } + it.results + }.groupBy { holder.concreteAddr(it as UtAddrExpression) }.mapValues { it.value.toSet() } + val staticsBefore = memory.staticFields().map { (fieldId, states) -> fieldId to states.stateBefore } + val staticsAfter = memory.staticFields().map { (fieldId, states) -> fieldId to states.stateAfter } + + val modelsBefore = withMemoryState(MemoryState.INITIAL) { + internalResolveModel(parameters, staticsBefore, allAddresses) + } + + val modelsAfter = withMemoryState(MemoryState.CURRENT) { + val resolvedModels = internalResolveModel(parameters, staticsAfter, allAddresses) + resolvedModels + } + + return ConstrainedExecution(modelsBefore.parameters, modelsAfter.parameters) + } + + private fun internalResolveModel( + parameters: List, + statics: List>, + addrs: Map> + ): ResolvedModels { + val parameterModels = parameters.map { resolveModel(it, addrs) } + + val staticModels = statics.map { (fieldId, value) -> + withStaticMemoryState(fieldId) { + resolveModel(value, addrs) + } + } + + val allStatics = staticModels.mapIndexed { i, model -> statics[i].first to model }.toMap() + return ResolvedModels(parameterModels, allStatics) + } + + private fun resolveModel( + value: SymbolicValue, + addrs: Map> + ): UtModel = when (value) { + is PrimitiveValue -> buildModel( + value.expr.variable, + collectAtoms(value, addrs), + emptySet(), + null + ) + + is ReferenceValue -> buildModel( + value.addr.variable, + collectAtoms(value, addrs), + addrs[value.addr.variable.addr]!!.map { it.variable }.toSet(), + value.concrete + ) + } + + private fun collectConstraintAtoms(predicate: (UtExpression) -> Boolean): Set = + UtAtomCollector(predicate).run { + traverseQuery { constraint -> + constraint.accept(this) + } + result + }.mapNotNull { + it.accept(UtConstraintBuilder(variableContext)) + }.toSet() + + private fun collectAtoms(value: SymbolicValue, addrs: Map>): Set = + when (value) { + is PrimitiveValue -> collectConstraintAtoms { it == value.expr } + is ReferenceValue -> { + val valueExprs = addrs[holder.concreteAddr(value.addr)]!! + collectConstraintAtoms { it in valueExprs } + } + } + + private fun buildModel( + variable: UtConstraintVariable, + atoms: Set, + aliases: Set, + concrete: Concrete? = null + ): UtModel = when { + variable.isPrimitive -> buildPrimitiveModel(variable, atoms, aliases) + variable.addr == SYMBOLIC_NULL_ADDR -> UtNullModel(variable.classId) + variable.addr in resolvedConstraints -> UtReferenceToConstraintModel( + variable, + resolvedConstraints.getValue(variable.addr) + ) + + variable.isArray -> buildArrayModel(variable, atoms, aliases).also { + resolvedConstraints[variable.addr] = it + } + + else -> when (concrete) { + null -> buildObjectModel(variable, atoms, aliases).also { + resolvedConstraints[variable.addr] = it + } + + else -> buildConcreteModel(concrete, variable, atoms, aliases) + } + } + + private fun buildPrimitiveModel( + variable: UtConstraintVariable, + atoms: Set, + aliases: Set + ): UtModel { + assert(variable.isPrimitive) + + val allAliases = aliases + variable + val primitiveConstraints = atoms.filter { constraint -> + allAliases.any { it in constraint } + }.map { it.accept(UtConstraintTransformer(aliases.associateWith { variable })) }.toSet() + + return UtPrimitiveConstraintModel( + variable, primitiveConstraints, concrete = variableContext.evalOrNull(variable) + ) + } + + private fun buildObjectModel( + variable: UtConstraintVariable, + atoms: Set, + aliases: Set + ): UtModel { + assert(!variable.isPrimitive && !variable.isArray) + assert(aliases.all { !it.isPrimitive && !it.isArray }) + + val allAliases = aliases + variable + val refConstraints = atoms.filter { constraint -> + allAliases.any { it in constraint } + }.toSet() + + return UtReferenceConstraintModel( + variable, refConstraints + ) + } + + private fun buildArrayModel( + variable: UtConstraintVariable, + atoms: Set, + aliases: Set + ): UtModel { + assert(variable.isArray) + assert(aliases.all { it.isArray }) + val elementClassId = variable.classId.elementClassId!! + + val allAliases = aliases + variable + val lengths = atoms.flatMap { it.flatMap() }.filter { + it is UtConstraintArrayLength && it.instance in allAliases + }.toSet() + val lengthVariable = UtConstraintArrayLength(variable) + val lengthModel = buildModel(lengthVariable, atoms, lengths, null) + val concreteLength = lengths.firstOrNull()?.let { variableContext.evalOrNull(it) as Int } ?: MAX_ARRAY_LENGTH + + val indexMap = atoms + .flatten { index -> + index is UtConstraintArrayAccess && index.instance in allAliases + } + .map { (it as UtConstraintArrayAccess).index } + .filter { (variableContext.evalOrNull(it) as Int) < concreteLength } + .groupBy { variableContext.evalOrNull(it) } + .mapValues { it.value.toSet() } + + var indexCount = 0 + val elements = indexMap.map { (key, indices) -> + + // create new variable that represents current index + val indexVariable = UtConstraintParameter( + "${variable}_index${indexCount++}", intClassId + ) + val indexModel = UtPrimitiveConstraintModel( + indexVariable, + indices.map { UtEqConstraint(indexVariable, it) }.toSet(), + concrete = key + ) + + // bind newly created variable with actual indices information + val indexWithExpr = allAliases + .flatMap { base -> + indices.map { UtConstraintArrayAccess(base, it, elementClassId) } + }.first { variableContext.hasExpr(it) } + val elementType = when { + elementClassId.isPrimitive -> elementClassId + else -> variableContext.evalTypeOrNull(indexWithExpr)?.classId ?: elementClassId + } + val arrayAccess = UtConstraintArrayAccess(variable, indexVariable, elementType) + variableContext.bind(arrayAccess, indexWithExpr) + + // compute aliases and build the actual model + val indexAliases = indices.flatMap { idx -> + allAliases.map { UtConstraintArrayAccess(it, idx, elementClassId) } + }.toSet() + val res = buildModel(arrayAccess, atoms, indexAliases).withConstraints( + indices.map { UtEqConstraint(it, indexVariable) }.toSet() + setOf( + UtGeConstraint(indexVariable, UtConstraintNumericConstant(0)), + UtLtConstraint(indexVariable, lengthVariable) + ) + ) + (indexModel as UtModel) to res + }.toMap() + + return UtArrayConstraintModel( + variable, + lengthModel, + elements, + setOf() + ) + } + + private fun buildConcreteModel( + concrete: Concrete, + variable: UtConstraintVariable, + atoms: Set, + aliases: Set + ): UtModel = when (concrete.value) { + is ListWrapper -> buildListModel(concrete.value, variable, atoms, aliases) + is SetWrapper -> buildSetModel(concrete.value, variable, atoms, aliases) + is MapWrapper -> buildMapModel(concrete.value, variable, atoms, aliases) + else -> buildObjectModel(variable, atoms, aliases) + } + + private fun buildListModel( + concrete: ListWrapper, + variable: UtConstraintVariable, + atoms: Set, + aliases: Set + ): UtModel { + val allAliases = aliases + variable + val refConstraints = atoms.filter { constraint -> + allAliases.any { it in constraint } + }.toSet() + + val default = { buildObjectModel(variable, atoms, aliases) } + val elementData = atoms + .flatten { it is UtConstraintFieldAccess && it.instance == variable && it.fieldId.name == "elementData" } + .firstOrNull() as? UtConstraintFieldAccess ?: return default() + val storageArray = atoms + .flatten { it is UtConstraintFieldAccess && it.instance == elementData && it.fieldId.name == "storage" } + .firstOrNull() as? UtConstraintFieldAccess ?: return default() + val aliasArrays = aliases.map { + UtConstraintFieldAccess(UtConstraintFieldAccess(it, elementData.fieldId), storageArray.fieldId) + }.toSet() + val array = buildArrayModel(storageArray, atoms, aliasArrays) as UtArrayConstraintModel + val concreteLength = (array.length as UtPrimitiveConstraintModel).concrete as Int + val concreteIndices = array.elements.toList().associate { (index, value) -> + (index as UtPrimitiveConstraintModel).concrete as Int to ((index as UtModel) to value) + } + val completedElements = (0 until concreteLength).associate { + if (it in concreteIndices) concreteIndices[it]!! + else { + UtPrimitiveConstraintModel( + UtConstraintNumericConstant(it), + emptySet(), + it + ) to UtNullModel(objectClassId) + } + } + return UtListConstraintModel( + variable, + array.length, + completedElements, + array.utConstraints + refConstraints + ) + } + + private fun buildSetModel( + concrete: SetWrapper, + variable: UtConstraintVariable, + atoms: Set, + aliases: Set + ): UtModel { + val allAliases = aliases + variable + val refConstraints = atoms.filter { constraint -> + allAliases.any { it in constraint } + }.toSet() + + val default = { buildObjectModel(variable, atoms, aliases) } + val elementData = atoms + .flatten { it is UtConstraintFieldAccess && it.instance == variable && it.fieldId.name == "elementData" } + .firstOrNull() as? UtConstraintFieldAccess ?: return default() + val storageArray = atoms + .flatten { it is UtConstraintFieldAccess && it.instance == elementData && it.fieldId.name == "storage" } + .firstOrNull() as? UtConstraintFieldAccess ?: return default() + val aliasArrays = aliases.map { + UtConstraintFieldAccess(UtConstraintFieldAccess(it, elementData.fieldId), storageArray.fieldId) + }.toSet() + val array = buildArrayModel(storageArray, atoms, aliasArrays) as UtArrayConstraintModel + return UtSetConstraintModel( + variable, + array.length, + array.elements, + array.utConstraints + refConstraints + ) + } + + private fun buildMapModel( + concrete: MapWrapper, + variable: UtConstraintVariable, + atoms: Set, + aliases: Set + ): UtModel { + val allAliases = aliases + variable + val refConstraints = atoms.filter { constraint -> + allAliases.any { it in constraint } + }.toSet() + + val default = { buildObjectModel(variable, atoms, aliases) } + val keysField = atoms + .flatten { it is UtConstraintFieldAccess && it.instance == variable && it.fieldId.name == "keys" } + .firstOrNull() as? UtConstraintFieldAccess ?: return default() + val keysStorageArray = atoms + .flatten { it is UtConstraintFieldAccess && it.instance == keysField && it.fieldId.name == "storage" } + .firstOrNull() as? UtConstraintFieldAccess ?: return default() + val keysAliasArrays = aliases.map { + UtConstraintFieldAccess(UtConstraintFieldAccess(it, keysField.fieldId), keysStorageArray.fieldId) + }.toSet() + val keys = buildArrayModel(keysStorageArray, atoms, keysAliasArrays) as UtArrayConstraintModel + val concreteKeys = keys.elements.toList().associate { (index, value) -> + (index as UtPrimitiveConstraintModel).concrete as Int to ((index as UtModel) to value) + } + + val valuesField = + atoms.flatten { it is UtConstraintFieldAccess && it.instance == variable && it.fieldId.name == "values" } + .firstOrNull() as? UtConstraintFieldAccess ?: return default() + val valuesStorageArray = atoms + .flatten { it is UtConstraintFieldAccess && it.instance == valuesField && it.fieldId.name == "storage" } + .firstOrNull() as? UtConstraintFieldAccess ?: return default() + val valuesAliasArrays = aliases.map { + UtConstraintFieldAccess(UtConstraintFieldAccess(it, valuesField.fieldId), valuesStorageArray.fieldId) + }.toSet() + val values = buildArrayModel(valuesStorageArray, atoms, valuesAliasArrays) as UtArrayConstraintModel + val concreteValues = values.elements.toList().associate { (index, value) -> + (index as UtPrimitiveConstraintModel).concrete as Int to ((index as UtModel) to value) + } + + val mapElements = concreteKeys.mapValues { (key, values) -> + values.second to concreteValues.getOrDefault( + key, + UtNullModel(objectClassId) to UtNullModel(objectClassId) + ).second + }.values.toMap() + + return UtMapConstraintModel( + variable, + keys.length, + mapElements, + refConstraints + ) + } + + private val UtExpression.variable get() = accept(variableContext) + private val UtConstraintVariable.expr get() = variableContext[this] + + private val UtConstraintVariable.exprUnsafe + get() = when { + variableContext.hasExpr(this) -> variableContext[this] + else -> null + } + private val UtConstraintVariable.addr get() = holder.concreteAddr(expr as UtAddrExpression) + + private fun UtModel.withConstraints(constraints: Set) = when (this) { + is UtPrimitiveConstraintModel -> copy(utConstraints = utConstraints + constraints) + is UtReferenceConstraintModel -> copy(utConstraints = utConstraints + constraints) + is UtReferenceToConstraintModel -> copy(utConstraints = utConstraints + constraints) + is UtArrayConstraintModel -> copy(baseConstraints = baseConstraints + constraints) + is UtListConstraintModel -> copy(baseConstraints = baseConstraints + constraints) + is UtSetConstraintModel -> copy(baseConstraints = baseConstraints + constraints) + is UtMapConstraintModel -> copy(baseConstraints = baseConstraints + constraints) + else -> this + } + + private fun Set.flatten(predicate: (UtConstraintVariable) -> Boolean): Set = + this.flatMap { + it.accept(UtConstraintVariableCollector(predicate)) + }.toSet() +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtAtomCollector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtAtomCollector.kt new file mode 100644 index 0000000000..d92e71541a --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtAtomCollector.kt @@ -0,0 +1,242 @@ +package org.utbot.engine.pc + +class UtAtomCollector(val predicate: (UtExpression) -> Boolean) : UtExpressionVisitor> { + val result = mutableSetOf() + private var currentParent: UtExpression? = null + + private inline fun visitBooleanExpr(expr: T, visitor: (T) -> Unit): Set { + val oldParent = currentParent + if (expr.sort is UtBoolSort) { + currentParent = expr + } + if (predicate(expr)) { + result += currentParent!! + } else { + visitor(expr) + } + currentParent = oldParent + return result + } + + override fun visit(expr: UtArraySelectExpression): Set = visitBooleanExpr(expr) { + it.arrayExpression.accept(this) + it.index.accept(this) + } + + override fun visit(expr: UtConstArrayExpression): Set = visitBooleanExpr(expr) { + it.constValue.accept(this) + } + + override fun visit(expr: UtMkArrayExpression): Set = visitBooleanExpr(expr) {} + + override fun visit(expr: UtArrayMultiStoreExpression): Set = visitBooleanExpr(expr) { + it.initial.accept(this) + it.stores.forEach { store -> + store.index.accept(this) + store.value.accept(this) + } + } + + override fun visit(expr: UtBvLiteral): Set = visitBooleanExpr(expr) {} + + override fun visit(expr: UtBvConst): Set = visitBooleanExpr(expr) {} + + override fun visit(expr: UtAddrExpression): Set = visitBooleanExpr(expr) { + it.internal.accept(this) + } + + override fun visit(expr: UtFpLiteral): Set = visitBooleanExpr(expr) {} + + override fun visit(expr: UtFpConst): Set = visitBooleanExpr(expr) {} + + override fun visit(expr: UtOpExpression): Set = visitBooleanExpr(expr) { + it.left.expr.accept(this) + it.right.expr.accept(this) + } + + override fun visit(expr: UtTrue): Set = visitBooleanExpr(expr) {} + + override fun visit(expr: UtFalse): Set = visitBooleanExpr(expr) {} + + override fun visit(expr: UtEqExpression): Set = visitBooleanExpr(expr) { + it.left.accept(this) + it.right.accept(this) + } + + override fun visit(expr: UtBoolConst): Set = visitBooleanExpr(expr) {} + + override fun visit(expr: NotBoolExpression): Set = visitBooleanExpr(expr) { + it.expr.accept(this) + } + + override fun visit(expr: UtOrBoolExpression): Set = visitBooleanExpr(expr) { + it.exprs.forEach { operand -> operand.accept(this) } + } + + override fun visit(expr: UtAndBoolExpression): Set = visitBooleanExpr(expr) { + it.exprs.forEach { operand -> operand.accept(this) } + } + + override fun visit(expr: UtNegExpression): Set = visitBooleanExpr(expr) { + it.variable.expr.accept(this) + } + + override fun visit(expr: UtCastExpression): Set = visitBooleanExpr(expr) { + it.variable.expr.accept(this) + } + + override fun visit(expr: UtBoolOpExpression): Set = visitBooleanExpr(expr) { + it.left.expr.accept(this) + it.right.expr.accept(this) + } + + override fun visit(expr: UtIsExpression): Set = visitBooleanExpr(expr) { + it.addr.accept(this) + } + + override fun visit(expr: UtGenericExpression): Set = visitBooleanExpr(expr) { + it.addr.accept(this) + } + + override fun visit(expr: UtIsGenericTypeExpression): Set = visitBooleanExpr(expr) { + it.addr.accept(this) + } + + override fun visit(expr: UtEqGenericTypeParametersExpression): Set = visitBooleanExpr(expr) { + it.firstAddr.accept(this) + it.secondAddr.accept(this) + } + + override fun visit(expr: UtInstanceOfExpression): Set = visitBooleanExpr(expr) { + it.constraint.accept(this) + } + + override fun visit(expr: UtIteExpression): Set = visitBooleanExpr(expr) { + it.condition.accept(this) + it.thenExpr.accept(this) + it.elseExpr.accept(this) + } + + override fun visit(expr: UtMkTermArrayExpression): Set = visitBooleanExpr(expr) { + it.array.accept(this) + it.defaultValue?.accept(this) + } + + override fun visit(expr: UtStringConst): Set = visitBooleanExpr(expr) {} + + override fun visit(expr: UtConcatExpression): Set = visitBooleanExpr(expr) { + it.parts.forEach { part -> part.accept(this) } + } + + override fun visit(expr: UtConvertToString): Set = visitBooleanExpr(expr) { + expr.expression.accept(this) + } + + override fun visit(expr: UtStringToInt): Set = visitBooleanExpr(expr) { + expr.expression.accept(this) + } + + override fun visit(expr: UtStringLength): Set = visitBooleanExpr(expr) { + expr.string.accept(this) + } + + override fun visit(expr: UtStringPositiveLength): Set = visitBooleanExpr(expr) { + expr.string.accept(this) + } + + override fun visit(expr: UtStringCharAt): Set = visitBooleanExpr(expr) { + expr.string.accept(this) + expr.index.accept(this) + } + + override fun visit(expr: UtStringEq): Set = visitBooleanExpr(expr) { + expr.left.accept(this) + expr.right.accept(this) + } + + override fun visit(expr: UtSubstringExpression): Set = visitBooleanExpr(expr) { + expr.string.accept(this) + expr.beginIndex.accept(this) + expr.length.accept(this) + } + + override fun visit(expr: UtReplaceExpression): Set = visitBooleanExpr(expr) { + expr.string.accept(this) + expr.regex.accept(this) + expr.replacement.accept(this) + } + + override fun visit(expr: UtStartsWithExpression): Set = visitBooleanExpr(expr) { + expr.string.accept(this) + expr.prefix.accept(this) + } + + override fun visit(expr: UtEndsWithExpression): Set = visitBooleanExpr(expr) { + expr.string.accept(this) + expr.suffix.accept(this) + } + + override fun visit(expr: UtIndexOfExpression): Set = visitBooleanExpr(expr) { + expr.string.accept(this) + expr.substring.accept(this) + } + + override fun visit(expr: UtContainsExpression): Set = visitBooleanExpr(expr) { + expr.string.accept(this) + expr.substring.accept(this) + } + + override fun visit(expr: UtToStringExpression): Set = visitBooleanExpr(expr) { + expr.notNullExpr.accept(this) + expr.isNull.accept(this) + } + + override fun visit(expr: UtSeqLiteral): Set = visitBooleanExpr(expr) {} + + override fun visit(expr: UtArrayToString): Set = visitBooleanExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArrayInsert): Set = visitBooleanExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArrayInsertRange): Set = visitBooleanExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArrayRemove): Set = visitBooleanExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArrayRemoveRange): Set = visitBooleanExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArraySetRange): Set = visitBooleanExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArrayShiftIndexes): Set = visitBooleanExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArrayApplyForAll): Set = visitBooleanExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtStringToArray): Set = visitBooleanExpr(expr) { + expr.stringExpression.accept(this) + expr.offset.expr.accept(this) + } + + override fun visit(expr: UtAddNoOverflowExpression): Set = visitBooleanExpr(expr) { + expr.left.accept(this) + expr.right.accept(this) + } + + override fun visit(expr: UtSubNoOverflowExpression): Set = visitBooleanExpr(expr) { + expr.left.accept(this) + expr.right.accept(this) + } +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExprCollector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExprCollector.kt new file mode 100644 index 0000000000..97df004cbf --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExprCollector.kt @@ -0,0 +1,236 @@ +package org.utbot.engine.pc + +class UtExprCollector(val predicate: (UtExpression) -> Boolean) : UtExpressionVisitor> { + val results = mutableSetOf() + + private inline fun visitExpr(expr: T, body: (T) -> Unit): Set { + if (predicate(expr)) { + results += expr + } + body(expr) + return results + } + + override fun visit(expr: UtArraySelectExpression): Set = visitExpr(expr) { + it.arrayExpression.accept(this) + it.index.accept(this) + } + + override fun visit(expr: UtConstArrayExpression): Set = visitExpr(expr) { + it.constValue.accept(this) + } + + override fun visit(expr: UtMkArrayExpression): Set = visitExpr(expr) {} + + override fun visit(expr: UtArrayMultiStoreExpression): Set = visitExpr(expr) { + it.initial.accept(this) + it.stores.forEach { store -> + store.index.accept(this) + store.value.accept(this) + } + } + + override fun visit(expr: UtBvLiteral): Set = visitExpr(expr) {} + + override fun visit(expr: UtBvConst): Set = visitExpr(expr) {} + + override fun visit(expr: UtAddrExpression): Set = visitExpr(expr) { + it.internal.accept(this) + } + + override fun visit(expr: UtFpLiteral): Set = visitExpr(expr) {} + + override fun visit(expr: UtFpConst): Set = visitExpr(expr) {} + + override fun visit(expr: UtOpExpression): Set = visitExpr(expr) { + it.left.expr.accept(this) + it.right.expr.accept(this) + } + + override fun visit(expr: UtTrue): Set = visitExpr(expr) {} + + override fun visit(expr: UtFalse): Set = visitExpr(expr) {} + + override fun visit(expr: UtEqExpression): Set = visitExpr(expr) { + it.left.accept(this) + it.right.accept(this) + } + + override fun visit(expr: UtBoolConst): Set = visitExpr(expr) {} + + override fun visit(expr: NotBoolExpression): Set = visitExpr(expr) { + it.expr.accept(this) + } + + override fun visit(expr: UtOrBoolExpression): Set = visitExpr(expr) { + it.exprs.forEach { operand -> operand.accept(this) } + } + + override fun visit(expr: UtAndBoolExpression): Set = visitExpr(expr) { + it.exprs.forEach { operand -> operand.accept(this) } + } + + override fun visit(expr: UtNegExpression): Set = visitExpr(expr) { + it.variable.expr.accept(this) + } + + override fun visit(expr: UtCastExpression): Set = visitExpr(expr) { + it.variable.expr.accept(this) + } + + override fun visit(expr: UtBoolOpExpression): Set = visitExpr(expr) { + it.left.expr.accept(this) + it.right.expr.accept(this) + } + + override fun visit(expr: UtIsExpression): Set = visitExpr(expr) { + it.addr.accept(this) + } + + override fun visit(expr: UtGenericExpression): Set = visitExpr(expr) { + it.addr.accept(this) + } + + override fun visit(expr: UtIsGenericTypeExpression): Set = visitExpr(expr) { + it.addr.accept(this) + } + + override fun visit(expr: UtEqGenericTypeParametersExpression): Set = visitExpr(expr) { + it.firstAddr.accept(this) + it.secondAddr.accept(this) + } + + override fun visit(expr: UtInstanceOfExpression): Set = visitExpr(expr) { + it.constraint.accept(this) + } + + override fun visit(expr: UtIteExpression): Set = visitExpr(expr) { + it.condition.accept(this) + it.thenExpr.accept(this) + it.elseExpr.accept(this) + } + + override fun visit(expr: UtMkTermArrayExpression): Set = visitExpr(expr) { + it.array.accept(this) + it.defaultValue?.accept(this) + } + + override fun visit(expr: UtStringConst): Set = visitExpr(expr) {} + + override fun visit(expr: UtConcatExpression): Set = visitExpr(expr) { + it.parts.forEach { part -> part.accept(this) } + } + + override fun visit(expr: UtConvertToString): Set = visitExpr(expr) { + expr.expression.accept(this) + } + + override fun visit(expr: UtStringToInt): Set = visitExpr(expr) { + expr.expression.accept(this) + } + + override fun visit(expr: UtStringLength): Set = visitExpr(expr) { + expr.string.accept(this) + } + + override fun visit(expr: UtStringPositiveLength): Set = visitExpr(expr) { + expr.string.accept(this) + } + + override fun visit(expr: UtStringCharAt): Set = visitExpr(expr) { + expr.string.accept(this) + expr.index.accept(this) + } + + override fun visit(expr: UtStringEq): Set = visitExpr(expr) { + expr.left.accept(this) + expr.right.accept(this) + } + + override fun visit(expr: UtSubstringExpression): Set = visitExpr(expr) { + expr.string.accept(this) + expr.beginIndex.accept(this) + expr.length.accept(this) + } + + override fun visit(expr: UtReplaceExpression): Set = visitExpr(expr) { + expr.string.accept(this) + expr.regex.accept(this) + expr.replacement.accept(this) + } + + override fun visit(expr: UtStartsWithExpression): Set = visitExpr(expr) { + expr.string.accept(this) + expr.prefix.accept(this) + } + + override fun visit(expr: UtEndsWithExpression): Set = visitExpr(expr) { + expr.string.accept(this) + expr.suffix.accept(this) + } + + override fun visit(expr: UtIndexOfExpression): Set = visitExpr(expr) { + expr.string.accept(this) + expr.substring.accept(this) + } + + override fun visit(expr: UtContainsExpression): Set = visitExpr(expr) { + expr.string.accept(this) + expr.substring.accept(this) + } + + override fun visit(expr: UtToStringExpression): Set = visitExpr(expr) { + expr.notNullExpr.accept(this) + expr.isNull.accept(this) + } + + override fun visit(expr: UtSeqLiteral): Set = visitExpr(expr) {} + + override fun visit(expr: UtArrayToString): Set = visitExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArrayInsert): Set = visitExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArrayInsertRange): Set = visitExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArrayRemove): Set = visitExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArrayRemoveRange): Set = visitExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArraySetRange): Set = visitExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArrayShiftIndexes): Set = visitExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtArrayApplyForAll): Set = visitExpr(expr) { + expr.arrayExpression.accept(this) + } + + override fun visit(expr: UtStringToArray): Set = visitExpr(expr) { + expr.stringExpression.accept(this) + expr.offset.expr.accept(this) + } + + override fun visit(expr: UtAddNoOverflowExpression): Set = visitExpr(expr) { + expr.left.accept(this) + expr.right.accept(this) + } + + override fun visit(expr: UtSubNoOverflowExpression): Set = visitExpr(expr) { + expr.left.accept(this) + expr.right.accept(this) + } + +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt index 57184aed87..5b51213a46 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt @@ -8,6 +8,8 @@ import org.utbot.common.md5 import org.utbot.common.trace import org.utbot.engine.Eq import org.utbot.engine.PrimitiveValue +import org.utbot.engine.ReferenceValue +import org.utbot.engine.SymbolicValue import org.utbot.engine.TypeRegistry import org.utbot.engine.pc.UtSolverStatusKind.SAT import org.utbot.engine.pc.UtSolverStatusKind.UNKNOWN @@ -78,6 +80,13 @@ private fun reduceAnd(exprs: List) = } fun mkEq(left: PrimitiveValue, right: PrimitiveValue): UtBoolExpression = Eq(left, right) +fun mkEq(left: ReferenceValue, right: ReferenceValue): UtBoolExpression = mkEq(left.addr, right.addr) + +fun mkEq(left: SymbolicValue, right: SymbolicValue): UtBoolExpression = when (left) { + is PrimitiveValue -> mkEq(left, right as? PrimitiveValue ?: error("Can't cast to PrimitiveValue")) + is ReferenceValue -> mkEq(left, right as? ReferenceValue ?: error("Can't cast to ReferenceValue")) +} + fun mkTrue(): UtBoolLiteral = UtTrue fun mkFalse(): UtBoolLiteral = UtFalse fun mkBool(boolean: Boolean): UtBoolLiteral = if (boolean) UtTrue else UtFalse @@ -157,6 +166,12 @@ data class UtSolver constructor( val rewriter: RewritingVisitor get() = constraints.let { if (it is Query) it.rewriter else RewritingVisitor() } + + /** + * Returns the current constraints. + */ + val query get() = constraints + /** * Returns the current status of the constraints. * Get is mandatory here to avoid situations when we invoked `check` and asked the solver diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt index 0df5e2b37c..33966c6111 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt @@ -13,6 +13,10 @@ import com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CONST_ARRAY import com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_STORE import com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UNINTERPRETED import com.microsoft.z3.eval +import kotlinx.collections.immutable.PersistentMap +import kotlinx.collections.immutable.PersistentSet +import kotlinx.collections.immutable.persistentHashMapOf +import kotlinx.collections.immutable.persistentSetOf /** * Represents current Status of UTSolver. diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt index 4f0d7516d4..6a61161da4 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt @@ -335,7 +335,7 @@ open class Z3TranslatorVisitor( private fun Context.mkBV2Int(expr: UtExpression): IntExpr = if (expr is UtBvLiteral) { - mkInt(expr.value as Long) + mkInt(expr.value.toLong()) } else { mkBV2Int(translate(expr) as BitVecExpr, true) } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/constraint/UtConstraintBuilder.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/constraint/UtConstraintBuilder.kt new file mode 100644 index 0000000000..2bef68512e --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/constraint/UtConstraintBuilder.kt @@ -0,0 +1,180 @@ +package org.utbot.engine.pc + +import org.utbot.engine.* +import org.utbot.engine.Eq +import org.utbot.engine.Ge +import org.utbot.engine.Le +import org.utbot.engine.Lt +import org.utbot.engine.Ne +import org.utbot.engine.pc.constraint.UtDefaultExpressionVisitor +import org.utbot.engine.pc.constraint.UtVarContext +import org.utbot.engine.z3.boolValue +import org.utbot.engine.z3.value +import org.utbot.framework.plugin.api.* +import org.utbot.framework.plugin.api.util.objectClassId + +class NotSupportedByConstraintResolverException : Exception() + +class UtConstraintBuilder( + val variableContext: UtVarContext +) : UtDefaultExpressionVisitor({ + throw NotSupportedByConstraintResolverException() +}) { + val holder get() = variableContext.holder + + private fun shouldSkip(expr: UtExpression): Boolean { + if ("addrToType" in expr.toString()) return true + if ("addrToNumDimensions" in expr.toString()) return true + if ("isMock" in expr.toString()) return true + if ("arraySetRange" in expr.toString()) return true + return false + } + + private fun applyConstraint(expr: UtExpression, constraint: () -> UtConstraint?): UtConstraint? = + when (holder.eval(expr).value()) { + true -> constraint() + false -> constraint()?.negated() + else -> error("Not boolean expr") + } + + override fun visit(expr: UtArraySelectExpression): UtConstraint? = applyConstraint(expr) { + if (shouldSkip(expr)) return@applyConstraint null + if (expr.sort !is UtBoolSort) throw NotSupportedByConstraintResolverException() + UtBoolConstraint(expr.accept(variableContext)) + } + + override fun visit(expr: UtTrue): UtConstraint { + return UtBoolConstraint(UtConstraintBoolConstant(true)) + } + + override fun visit(expr: UtFalse): UtConstraint { + return UtBoolConstraint(UtConstraintBoolConstant(false)) + } + + override fun visit(expr: UtEqExpression): UtConstraint? = applyConstraint(expr) { + if (shouldSkip(expr)) return@applyConstraint null + + val lhv = expr.left.accept(variableContext) + val rhv = expr.right.accept(variableContext) + when { + lhv.isPrimitive && rhv.isPrimitive -> UtEqConstraint(lhv, rhv) + else -> UtRefEqConstraint(lhv, rhv) + } + } + + override fun visit(expr: UtBoolConst): UtConstraint = applyConstraint(expr) { + UtBoolConstraint(expr.accept(variableContext)) + }!! + + override fun visit(expr: NotBoolExpression): UtConstraint? = applyConstraint(expr) { + expr.expr.accept(this)?.let { + UtNegatedConstraint(it) + } + } + + override fun visit(expr: UtOrBoolExpression): UtConstraint? = applyConstraint(expr) { + val vars = expr.exprs.mapNotNull { it.accept(this) } + when { + vars.isEmpty() -> null + vars.size == 1 -> vars.first() + else -> vars.reduce { acc, variable -> UtOrConstraint(acc, variable) } + } + } + + override fun visit(expr: UtAndBoolExpression): UtConstraint? = applyConstraint(expr) { + val vars = expr.exprs.mapNotNull { it.accept(this) } + when { + vars.isEmpty() -> null + vars.size == 1 -> vars.first() + else -> vars.reduce { acc, variable -> UtAndConstraint(acc, variable) } + } + } + + override fun visit(expr: UtBoolOpExpression): UtConstraint? = applyConstraint(expr) { + if (shouldSkip(expr)) return@applyConstraint null + val lhv = expr.left.expr.accept(variableContext) + val rhv = expr.right.expr.accept(variableContext) + when (expr.operator) { + Le -> { + if (!lhv.isPrimitive || !rhv.isPrimitive) return@applyConstraint null + UtLeConstraint(lhv, rhv) + } + + Lt -> { + if (!lhv.isPrimitive || !rhv.isPrimitive) return@applyConstraint null + UtLtConstraint(lhv, rhv) + } + + Ge -> { + if (!lhv.isPrimitive || !rhv.isPrimitive) return@applyConstraint null + UtGeConstraint(lhv, rhv) + } + + Gt -> { + if (!lhv.isPrimitive || !rhv.isPrimitive) return@applyConstraint null + UtGtConstraint(lhv, rhv) + } + + Eq -> when (lhv.isPrimitive && rhv.isPrimitive) { + true -> UtEqConstraint(lhv, rhv) + false -> UtRefEqConstraint(lhv, rhv.wrapToRef()) + } + + Ne -> when (lhv.isPrimitive && rhv.isPrimitive) { + true -> UtEqConstraint(lhv, rhv).negated() + false -> UtEqConstraint(lhv, rhv.wrapToRef()).negated() + } + } + } + + fun UtConstraintVariable.wrapToRef(): UtConstraintVariable = when (this) { + is UtConstraintNumericConstant -> when (this.value) { + 0 -> UtConstraintNull(objectClassId) + else -> error("Unexpected") + } + else -> this + } + + override fun visit(expr: UtIsExpression): UtConstraint? { + if (shouldSkip(expr)) return null + val operand = expr.addr.accept(variableContext) + return UtRefTypeConstraint(operand, expr.type.classId) + } + + override fun visit(expr: UtGenericExpression): UtConstraint? { + return null + } + + override fun visit(expr: UtIsGenericTypeExpression): UtConstraint? = applyConstraint(expr) { + if (shouldSkip(expr)) return@applyConstraint null + UtRefGenericTypeConstraint( + expr.addr.accept(variableContext), + expr.baseAddr.accept(variableContext), + expr.parameterTypeIndex + ) + } + + override fun visit(expr: UtEqGenericTypeParametersExpression): UtConstraint? = applyConstraint(expr) { + if (shouldSkip(expr)) return@applyConstraint null + + val lhv = expr.firstAddr.accept(variableContext) + val rhv = expr.secondAddr.accept(variableContext) + UtRefGenericEqConstraint(lhv, rhv, expr.indexMapping) + } + + override fun visit(expr: UtInstanceOfExpression): UtConstraint? = applyConstraint(expr) { + expr.constraint.accept(this) + } + + override fun visit(expr: UtIteExpression): UtConstraint? = applyConstraint(expr) { + val condValue = holder.eval(expr.condition).boolValue() + assert(expr.thenExpr.sort is UtBoolSort) + assert(expr.elseExpr.sort is UtBoolSort) + when { + condValue -> expr.thenExpr.accept(this) + else -> expr.elseExpr.accept(this) + } + } + + override fun visit(expr: UtMkTermArrayExpression): UtConstraint? = null +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/constraint/UtDefaultExpressionVisitor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/constraint/UtDefaultExpressionVisitor.kt new file mode 100644 index 0000000000..761325bafc --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/constraint/UtDefaultExpressionVisitor.kt @@ -0,0 +1,68 @@ +package org.utbot.engine.pc.constraint + +import org.utbot.engine.pc.* + +open class UtDefaultExpressionVisitor( + val default: () -> TResult +) : UtExpressionVisitor { + override fun visit(expr: UtArraySelectExpression): TResult = default() + override fun visit(expr: UtConstArrayExpression): TResult = default() + override fun visit(expr: UtMkArrayExpression): TResult = default() + override fun visit(expr: UtArrayMultiStoreExpression): TResult = default() + override fun visit(expr: UtBvLiteral): TResult = default() + override fun visit(expr: UtBvConst): TResult = default() + override fun visit(expr: UtAddrExpression): TResult = default() + override fun visit(expr: UtFpLiteral): TResult = default() + override fun visit(expr: UtFpConst): TResult = default() + override fun visit(expr: UtOpExpression): TResult = default() + override fun visit(expr: UtTrue): TResult = default() + override fun visit(expr: UtFalse): TResult = default() + override fun visit(expr: UtEqExpression): TResult = default() + override fun visit(expr: UtBoolConst): TResult = default() + override fun visit(expr: NotBoolExpression): TResult = default() + override fun visit(expr: UtOrBoolExpression): TResult = default() + override fun visit(expr: UtAndBoolExpression): TResult = default() + override fun visit(expr: UtNegExpression): TResult = default() + override fun visit(expr: UtCastExpression): TResult = default() + override fun visit(expr: UtBoolOpExpression): TResult = default() + override fun visit(expr: UtIsExpression): TResult = default() + override fun visit(expr: UtGenericExpression): TResult = default() + override fun visit(expr: UtIsGenericTypeExpression): TResult = default() + override fun visit(expr: UtEqGenericTypeParametersExpression): TResult = default() + override fun visit(expr: UtInstanceOfExpression): TResult = default() + override fun visit(expr: UtIteExpression): TResult = default() + override fun visit(expr: UtMkTermArrayExpression): TResult = default() + + // UtString expressions + override fun visit(expr: UtStringConst): TResult = default() + override fun visit(expr: UtConcatExpression): TResult = default() + override fun visit(expr: UtConvertToString): TResult = default() + override fun visit(expr: UtStringToInt): TResult = default() + override fun visit(expr: UtStringLength): TResult = default() + override fun visit(expr: UtStringPositiveLength): TResult = default() + override fun visit(expr: UtStringCharAt): TResult = default() + override fun visit(expr: UtStringEq): TResult = default() + override fun visit(expr: UtSubstringExpression): TResult = default() + override fun visit(expr: UtReplaceExpression): TResult = default() + override fun visit(expr: UtStartsWithExpression): TResult = default() + override fun visit(expr: UtEndsWithExpression): TResult = default() + override fun visit(expr: UtIndexOfExpression): TResult = default() + override fun visit(expr: UtContainsExpression): TResult = default() + override fun visit(expr: UtToStringExpression): TResult = default() + override fun visit(expr: UtSeqLiteral): TResult = default() + override fun visit(expr: UtArrayToString): TResult = default() + + // UtArray expressions from extended array theory + override fun visit(expr: UtArrayInsert): TResult = default() + override fun visit(expr: UtArrayInsertRange): TResult = default() + override fun visit(expr: UtArrayRemove): TResult = default() + override fun visit(expr: UtArrayRemoveRange): TResult = default() + override fun visit(expr: UtArraySetRange): TResult = default() + override fun visit(expr: UtArrayShiftIndexes): TResult = default() + override fun visit(expr: UtArrayApplyForAll): TResult = default() + override fun visit(expr: UtStringToArray): TResult = default() + + // Add and Sub with overflow detection + override fun visit(expr: UtAddNoOverflowExpression): TResult = default() + override fun visit(expr: UtSubNoOverflowExpression): TResult = default() +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/constraint/UtVarContext.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/constraint/UtVarContext.kt new file mode 100644 index 0000000000..636827f27a --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/constraint/UtVarContext.kt @@ -0,0 +1,382 @@ +package org.utbot.engine.pc.constraint + +import org.utbot.engine.* +import org.utbot.engine.pc.* +import org.utbot.engine.z3.boolValue +import org.utbot.engine.z3.intValue +import org.utbot.engine.z3.value +import org.utbot.framework.plugin.api.* +import org.utbot.framework.plugin.api.UtConstraintParameter +import org.utbot.framework.plugin.api.util.* +import soot.ArrayType +import soot.PrimType +import soot.RefType +import soot.Type + + +class UtVarContext( + val holder: UtSolverStatusSAT, + val typeRegistry: TypeRegistry, + val typeResolver: TypeResolver, +) : UtDefaultExpressionVisitor({ + throw NotSupportedByConstraintResolverException() +}) { + private val internalAddrs = mutableMapOf() + private val var2Expression = mutableMapOf() + + fun evalOrNull(variable: UtConstraintVariable) = when { + hasExpr(variable) -> holder.eval(var2Expression[variable]!!).value() + else -> null + } + + operator fun get(variable: UtConstraintVariable) = var2Expression[variable] + ?: throw IllegalArgumentException() + + fun hasExpr(variable: UtConstraintVariable) = variable in var2Expression + + fun bind(base: UtConstraintVariable, binder: UtConstraintVariable) { + if (!hasExpr(binder)) + throw IllegalArgumentException() + var2Expression[base] = var2Expression[binder]!! + } + + fun evalTypeOrNull(variable: UtConstraintVariable): Type? { + val addr = var2Expression[variable] as? UtAddrExpression ?: return null + return holder.findTypeOrNull(addr) + } + + + override fun visit(expr: UtArraySelectExpression): UtConstraintVariable { + val res = when (val base = expr.arrayExpression.accept(this)) { + is UtConstraintParameter -> when (base.name) { + "arraysLength" -> { + val instance = expr.index.accept(this) + UtConstraintArrayLength(instance) + } + + "RefValues_Arrays" -> expr.index.accept(this) + "Multi_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("_", limit = 2) + val fieldId = FieldId(ClassId(type), field) + fieldId.type + UtConstraintFieldAccess(instance, fieldId) + } catch (e: Throwable) { + arrayAccess(base, instance) + } + } + } + + is UtConstraintFieldAccess -> arrayAccess(base, expr.index.accept(this)) + is UtConstraintNumericConstant -> expr.index.accept(this) + is UtConstraintNull -> UtConstraintArrayAccess(base, expr.index.accept(this), objectClassId) + is UtConstraintArrayAccess -> arrayAccess(base, expr.index.accept(this)) + else -> error("Unexpected: $base") + } + if (res.isPrimitive) { + var2Expression[res] = expr + } + return res + } + + private fun arrayAccess(base: UtConstraintVariable, index: UtConstraintVariable) = when { + base.classId.isArray && index.classId.isPrimitive -> { + UtConstraintArrayAccess(base, index, base.classId.elementClassId!!) + } + + base.classId.isMap -> { + UtConstraintArrayAccess(base, index, objectClassId) + } + + base.classId.isSet -> { + UtConstraintArrayAccess(base, index, objectClassId) + } + + else -> index + } + + override fun visit(expr: UtMkArrayExpression): UtConstraintVariable { + return UtConstraintParameter(expr.name, objectClassId).also { + var2Expression[it] = expr + } + } + + override fun visit(expr: UtArrayMultiStoreExpression): UtConstraintVariable { + if (expr.initial !is UtConstArrayExpression) { + return expr.initial.accept(this) + } + + val stores = expr.stores.map { it.index.accept(this) } + return stores.first() + } + + override fun visit(expr: UtBvLiteral): UtConstraintVariable { + return UtConstraintNumericConstant(expr.value).also { + var2Expression[it] = expr + } + } + + override fun visit(expr: UtBvConst): UtConstraintVariable { + return UtConstraintParameter( + expr.name, + when (expr.size) { + 8 -> primitiveModelValueToClassId(0.toByte()) + 16 -> primitiveModelValueToClassId(0.toShort()) + 32 -> primitiveModelValueToClassId(0) + 64 -> primitiveModelValueToClassId(0L) + else -> error("Unexpected") + } + ).also { + var2Expression[it] = expr + } + } + + override fun visit(expr: UtAddrExpression): UtConstraintVariable { + return when (val internal = expr.internal) { + is UtBvConst -> UtConstraintParameter( + (expr.internal as UtBvConst).name, + holder.findTypeOrNull(expr)?.classId ?: objectClassId + ) + + is UtBvLiteral -> when (internal.value) { + 0 -> UtConstraintNull(objectClassId) + else -> internalAddrs.getOrPut(internal.value.toInt()) { + UtConstraintParameter( + "object${internal.value}", + holder.findTypeOrNull(expr)?.classId ?: objectClassId + ) + } + } + + else -> expr.internal.accept(this) + }.also { + var2Expression[it] = expr + } + } + + override fun visit(expr: UtFpLiteral): UtConstraintVariable = UtConstraintNumericConstant(expr.value).also { + var2Expression[it] = expr + } + + override fun visit(expr: UtFpConst): UtConstraintVariable = + UtConstraintParameter( + expr.name, when (expr.sort) { + UtFp32Sort -> floatClassId + UtFp64Sort -> doubleClassId + else -> error("Unexpected") + } + ).also { + var2Expression[it] = expr + } + + override fun visit(expr: UtOpExpression): UtConstraintVariable { + val lhv = expr.left.expr.accept(this) + val rhv = expr.right.expr.accept(this) + return when (expr.operator) { + Add -> UtConstraintAdd(lhv, rhv) + And -> UtConstraintAnd(lhv, rhv) + Cmp -> UtConstraintCmp(lhv, rhv) + Cmpg -> UtConstraintCmpg(lhv, rhv) + Cmpl -> UtConstraintCmpl(lhv, rhv) + Div -> UtConstraintDiv(lhv, rhv) + Mul -> UtConstraintMul(lhv, rhv) + Or -> UtConstraintOr(lhv, rhv) + Rem -> UtConstraintRem(lhv, rhv) + Shl -> UtConstraintShl(lhv, rhv) + Shr -> UtConstraintShr(lhv, rhv) + Sub -> UtConstraintSub(lhv, rhv) + Ushr -> UtConstraintUshr(lhv, rhv) + Xor -> UtConstraintXor(lhv, rhv) + }.also { + var2Expression[it] = expr + } + } + + override fun visit(expr: UtTrue): UtConstraintVariable { + return UtConstraintBoolConstant(true).also { + var2Expression[it] = expr + } + } + + override fun visit(expr: UtFalse): UtConstraintVariable { + return UtConstraintBoolConstant(true).also { + var2Expression[it] = expr + } + } + + override fun visit(expr: UtBoolConst): UtConstraintVariable { + return UtConstraintParameter(expr.name, booleanClassId).also { + var2Expression[it] = expr + } + } + + override fun visit(expr: NotBoolExpression): UtConstraintVariable { + return UtConstraintNot(expr.expr.accept(this)).also { + var2Expression[it] = expr + } + } + + override fun visit(expr: UtNegExpression): UtConstraintVariable { + return UtConstraintNeg( + expr.variable.expr.accept(this) + ).also { + var2Expression[it] = expr.variable.expr + } + } + + override fun visit(expr: UtCastExpression): UtConstraintVariable { + return UtConstraintCast( + expr.variable.expr.accept(this), + expr.type.classId + ).also { + var2Expression[it] = expr.variable.expr + } + } + + override fun visit(expr: UtIteExpression): UtConstraintVariable { + val condValue = holder.eval(expr.condition).boolValue() + return when { + condValue -> expr.thenExpr.accept(this) + else -> expr.elseExpr.accept(this) + } + } + + /** + * Returns evaluated type by object's [addr] or null if there is no information about evaluated typeId. + */ + private fun UtSolverStatusSAT.findTypeOrNull(addr: UtAddrExpression): Type? { + val base = findBaseTypeOrNull(addr) + val dimensions = findNumDimensionsOrNull(addr) + return base?.let { b -> + dimensions?.let { d -> + if (d == 0) b + else b.makeArrayType(d) + } + } + } + + /** + * Returns evaluated type by object's [addr] or null if there is no information about evaluated typeId. + */ + private fun UtSolverStatusSAT.findBaseTypeOrNull(addr: UtAddrExpression): Type? { + val typeId = eval(typeRegistry.symTypeId(addr)).intValue() + return typeRegistry.typeByIdOrNull(typeId) + } + + /** + * We have a constraint stated that every number of dimensions is in [0..MAX_NUM_DIMENSIONS], so if we have a value + * from outside of the range, it means that we have never touched the number of dimensions for the given addr. + */ + private fun UtSolverStatusSAT.findNumDimensionsOrNull(addr: UtAddrExpression): Int? { + val numDimensions = eval(typeRegistry.symNumDimensions(addr)).intValue() + return if (numDimensions in 0..MAX_NUM_DIMENSIONS) numDimensions else null + } + + private fun UtSolverStatusSAT.constructTypeOrNull(addr: UtAddrExpression, defaultType: Type): Type? { + val evaluatedType = findBaseTypeOrNull(addr) ?: return defaultType + val numDimensions = findNumDimensionsOrNull(addr) ?: defaultType.numDimensions + + // If we have numDimensions greater than zero, we have to check if the object is a java.lang.Object + // that is actually an instance of some array (e.g., Object -> Int[]) + if (defaultType.isJavaLangObject() && numDimensions > 0) { + return evaluatedType.makeArrayType(numDimensions) + } + + // If it does not, the numDimension must be exactly the same as in the defaultType; otherwise, it means that we + // have never `touched` the element during the analysis. Note that `isTouched` does not point on it, + // because there might be an aliasing between this addr and an addr of some other object, that we really + // touched, e.g., the addr of `this` object. In such case we can remove null to construct UtNullModel later. + if (numDimensions != defaultType.numDimensions) { + return null + } + + require(numDimensions == defaultType.numDimensions) + + // if we have a RefType, but not an instance of java.lang.Object, or an java.lang.Object with zero dimension + if (defaultType is RefType) { + val inheritors = typeResolver.findOrConstructInheritorsIncludingTypes(defaultType) + return evaluatedType.takeIf { evaluatedType in inheritors } + ?: fallbackToDefaultTypeIfPossible(evaluatedType, defaultType) + } + + defaultType as ArrayType + + return constructArrayTypeOrNull(evaluatedType, defaultType, numDimensions) + ?: fallbackToDefaultTypeIfPossible(evaluatedType, defaultType) + } + + private fun constructArrayTypeOrNull(evaluatedType: Type, defaultType: ArrayType, numDimensions: Int): ArrayType? { + if (numDimensions <= 0) return null + + val actualType = evaluatedType.makeArrayType(numDimensions) + val actualBaseType = actualType.baseType + val defaultBaseType = defaultType.baseType + val defaultNumDimensions = defaultType.numDimensions + + if (actualType == defaultType) return actualType + + // i.e., if defaultType is Object[][], the actualType must be at least primType[][][] + if (actualBaseType is PrimType && defaultBaseType.isJavaLangObject() && numDimensions > defaultNumDimensions) { + return actualType + } + + // i.e., if defaultType is Object[][], the actualType must be at least RefType[][] + if (actualBaseType is RefType && defaultBaseType.isJavaLangObject() && numDimensions >= defaultNumDimensions) { + return actualType + } + + if (actualBaseType is RefType && defaultBaseType is RefType) { + val inheritors = typeResolver.findOrConstructInheritorsIncludingTypes(defaultBaseType) + // if actualBaseType in inheritors, actualType and defaultType must have the same numDimensions + if (actualBaseType in inheritors && numDimensions == defaultNumDimensions) return actualType + } + + return null + } + + /** + * Tries to determine whether it is possible to use [defaultType] instead of [actualType] or not. + */ + private fun fallbackToDefaultTypeIfPossible(actualType: Type, defaultType: Type): Type? { + val defaultBaseType = defaultType.baseType + + // It might be confusing we do we return null instead of default type here for the touched element. + // The answer is because sometimes we may have a real object with different type as an element here. + // I.e. we have int[][]. In the z3 memory it is an infinite array represented by const model and stores. + // Let's assume we know that the array has only one element. It means that solver can do whatever it wants + // with every other element but the first one. In such cases sometimes it sets as const model (or even store + // outside the array's length) existing objects (that has been touched during the execution) with a wrong + // (for the array) type. Because of such cases we have to return null as a sign that construction failed. + // If we return defaultType, it will mean that it might try to put model with an inappropriate type + // as const or store model. + if (defaultBaseType is PrimType) return null + + val actualBaseType = actualType.baseType + + require(actualBaseType is RefType) { "Expected RefType, but $actualBaseType found" } + require(defaultBaseType is RefType) { "Expected RefType, but $defaultBaseType found" } + + val ancestors = typeResolver.findOrConstructAncestorsIncludingTypes(defaultBaseType) + + // This is intended to fix a specific problem. We have code: + // ColoredPoint foo(Point[] array) { + // array[0].x = 5; + // return (ColoredPoint[]) array; + // } + // Since we don't have a way to connect types of the array and the elements within it, there might be situation + // when the array is ColoredPoint[], but the first element of it got type Point from the solver. + // In such case here we'll have ColoredPoint as defaultType and Point as actualType. It is obvious from the example + // that we can construct ColoredPoint instance instead of it with randomly filled colored-specific fields. + return defaultType.takeIf { actualBaseType in ancestors && actualType.numDimensions == defaultType.numDimensions } + } +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BasePathSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BasePathSelector.kt index 0e400f527a..07dddcfcc7 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BasePathSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BasePathSelector.kt @@ -60,14 +60,14 @@ abstract class BasePathSelector( /** * @return true if [utSolver] constraints are satisfiable */ - private fun checkUnsat(utSolver: UtSolver): Boolean = - utSolver.assertions.isNotEmpty() && utSolver.check(respectSoft = false).statusKind != SAT + protected fun checkUnsat(state: ExecutionState): Boolean = + state.solver.assertions.isNotEmpty() && state.solver.check(respectSoft = false).statusKind != SAT /** * check fast unsat on forks */ private fun checkUnsatIfFork(state: ExecutionState) = - state.path.isNotEmpty() && choosingStrategy.graph.isFork(state.path.last()) && checkUnsat(state.solver) + state.path.isNotEmpty() && choosingStrategy.graph.isFork(state.path.last()) && checkUnsat(state) override fun poll(): ExecutionState? { if (stoppingStrategy.shouldStop()) { diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathSelectorBuilder.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathSelectorBuilder.kt index b529e6d456..d8cc5af0d3 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathSelectorBuilder.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathSelectorBuilder.kt @@ -17,14 +17,7 @@ import org.utbot.engine.selectors.nurs.NeuroSatSelector import org.utbot.engine.selectors.nurs.RPSelector import org.utbot.engine.selectors.nurs.SubpathGuidedSelector import org.utbot.engine.selectors.nurs.VisitCountingSelector -import org.utbot.engine.selectors.strategies.ChoosingStrategy -import org.utbot.engine.selectors.strategies.DistanceStatistics -import org.utbot.engine.selectors.strategies.EdgeVisitCountingStatistics -import org.utbot.engine.selectors.strategies.GeneratedTestCountingStatistics -import org.utbot.engine.selectors.strategies.StatementsStatistics -import org.utbot.engine.selectors.strategies.StepsLimitStoppingStrategy -import org.utbot.engine.selectors.strategies.StoppingStrategy -import org.utbot.engine.selectors.strategies.SubpathStatistics +import org.utbot.engine.selectors.strategies.* import org.utbot.framework.UtSettings.seedInPathSelector /** @@ -145,6 +138,15 @@ fun randomSelector( builder: RandomSelectorBuilder.() -> Unit ) = RandomSelectorBuilder(graph, strategy).apply(builder).build() +/** + * build [scoringPathSelector] using [ScoringPathSelectorBuilder] + */ +fun scoringPathSelector( + graph: InterProceduralUnitGraph, + scoringStrategy: ScoringStrategy, + builder: ScoringPathSelectorBuilder.() -> (Unit) +) = ScoringPathSelectorBuilder(graph, scoringStrategy).apply(builder).build() + /** * build [RPSelector] using [RPSelectorBuilder] */ @@ -405,6 +407,24 @@ class RandomSelectorBuilder internal constructor( ) } +/** + * Builder for [ScoringSelector]. Used in [scoringSelector] + * + * @param strategy [ScoringStrategy] for choosingStrategy for this PathSelector + */ +class ScoringPathSelectorBuilder internal constructor( + graph: InterProceduralUnitGraph, + val scoringStrategy: ScoringStrategy, + context: PathSelectorContext = PathSelectorContext(graph) +) : PathSelectorBuilder(graph, context) { + var seed: Int = 42 + override fun build() = ScoringPathSelector( + scoringStrategy, + requireNotNull(context.stoppingStrategy) { "StoppingStrategy isn't specified" }, + seed + ) +} + /** * Builder for [RPSelector]. Used in [rpSelector] * diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/ScoringPathSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/ScoringPathSelector.kt new file mode 100644 index 0000000000..aa7aa0ff1d --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/ScoringPathSelector.kt @@ -0,0 +1,22 @@ +package org.utbot.engine.selectors + +import org.utbot.engine.* +import org.utbot.engine.selectors.nurs.NonUniformRandomSearch +import org.utbot.engine.selectors.strategies.ScoringStrategy +import org.utbot.engine.selectors.strategies.StoppingStrategy + +class ScoringPathSelector( + override val choosingStrategy: ScoringStrategy, + stoppingStrategy: StoppingStrategy, + seed: Int? = 42 +) : NonUniformRandomSearch(choosingStrategy, stoppingStrategy, seed) { + + init { + choosingStrategy.subscribe(this) + } + + override val ExecutionState.cost: Double + get() = choosingStrategy[this] + + override val name = "ScoringPathSelector" +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/ConstraintScoringStrategy.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/ConstraintScoringStrategy.kt new file mode 100644 index 0000000000..48b6ccca0b --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/ConstraintScoringStrategy.kt @@ -0,0 +1,397 @@ +package org.utbot.engine.selectors.strategies + +import com.microsoft.z3.Expr +import kotlinx.collections.immutable.PersistentList +import mu.KotlinLogging +import org.utbot.engine.* +import org.utbot.engine.pc.UtAddrExpression +import org.utbot.engine.pc.UtSolverStatus +import org.utbot.engine.pc.UtSolverStatusSAT +import org.utbot.engine.symbolic.Assumption +import org.utbot.engine.util.abs +import org.utbot.engine.util.compareTo +import org.utbot.engine.util.minus +import org.utbot.engine.z3.boolValue +import org.utbot.engine.z3.intValue +import org.utbot.engine.z3.value +import org.utbot.framework.plugin.api.* +import org.utbot.framework.plugin.api.util.isSubtypeOf +import org.utbot.framework.synthesis.SynthesisMethodContext +import org.utbot.framework.synthesis.SynthesisUnitContext +import org.utbot.framework.synthesis.postcondition.constructors.ConstraintBasedPostConditionConstructor +import org.utbot.framework.synthesis.postcondition.constructors.UtConstraint2ExpressionConverter +import soot.ArrayType +import soot.PrimType +import soot.RefType +import soot.Type +import soot.jimple.Stmt +import java.lang.Double.min + +private typealias StmtPath = PersistentList + +class ConstraintScoringStrategyBuilder( + private val models: List, + private val unitContext: SynthesisUnitContext, + private val methodContext: SynthesisMethodContext, + private val postCondition: ConstraintBasedPostConditionConstructor +) : ScoringStrategyBuilder { + override fun build(graph: InterProceduralUnitGraph, traverser: Traverser): ScoringStrategy = + ConstraintScoringStrategy(graph, models, unitContext, methodContext, traverser, postCondition) +} + +class ConstraintScoringStrategy( + graph: InterProceduralUnitGraph, + private val models: List, + private val unitContext: SynthesisUnitContext, + private val methodContext: SynthesisMethodContext, + private val traverser: Traverser, + private val postCondition: ConstraintBasedPostConditionConstructor +) : ScoringStrategy(graph) { + private val logger = KotlinLogging.logger("ModelSynthesisScoringStrategy") + private val stateModels = hashMapOf() + private val pathScores = hashMapOf() + + private val distanceStatistics = DistanceStatistics(graph) + private val typeRegistry = traverser.typeRegistry + private val hierarchy = Hierarchy(typeRegistry) + private val typeResolver: TypeResolver = TypeResolver(typeRegistry, hierarchy) + + companion object { + private const val DEPTH_CHECK = 10 + private const val PATH_SCORE_COEFFICIENT = 1.0 + private const val MODEL_SCORE_COEFFICIENT = 100.0 + + internal const val INF_SCORE = Double.MAX_VALUE + internal const val MAX_SCORE = 1.0 + internal const val MIN_SCORE = 0.0 + } + + private fun shouldDropBasedOnScores(state: ExecutionState): Boolean { + val previous = run { + var current = state.path + val res = mutableListOf() + repeat(DEPTH_CHECK) { + if (current.isEmpty()) return@repeat + res += current + current = current.removeAt(current.lastIndex) + } + res.reversed() + } + val scores = previous.map { pathScores.getOrDefault(it, INF_SCORE) } + return scores.size >= DEPTH_CHECK && (0 until scores.lastIndex).all { scores[it] <= scores[it + 1] } + } + + override fun shouldDrop(state: ExecutionState): Boolean { + return shouldDropBasedOnScores(state) || distanceStatistics.shouldDrop(state) + } + + override fun score(executionState: ExecutionState): Double = pathScores.getOrPut(executionState.path) { + computePathScore(executionState) * PATH_SCORE_COEFFICIENT + + computeModelScore(executionState) * MODEL_SCORE_COEFFICIENT + } + + private fun computePathScore(executionState: ExecutionState): Double = + executionState.path.groupBy { it }.mapValues { it.value.size - 1 }.values.sum().toDouble() + + + private fun computeModelScore(executionState: ExecutionState): Double { + if (!traverser.isInitialized) return MIN_SCORE + val solver = executionState.solver + val postCondition = postCondition.constructSoftPostCondition(traverser) + val newSolver = solver.add( + postCondition.hardConstraints, + postCondition.softConstraints, + Assumption() + ) + val holder = stateModels.getOrPut(executionState) { + newSolver.check(respectSoft = true) + } as? UtSolverStatusSAT ?: return INF_SCORE + + val memory = executionState.executionStack.first().localVariableMemory + return computeScore(holder, memory) + } + + private fun computeScore( + holder: UtSolverStatusSAT, + memory: LocalVariableMemory + ): Double { + var currentScore = 0.0 + for (model in models) { + currentScore += computeModelScore(holder, memory, model) + } + return currentScore + } + + private fun computeModelScore( + holder: UtSolverStatusSAT, + memory: LocalVariableMemory, + model: UtModel + ): Double = when (model) { + is UtNullModel -> { + val modelUnit = unitContext[model] + val local = methodContext.unitToLocal[modelUnit] ?: error("null model should be defined as local variable") + val symbolic = memory.local(LocalVariable(local.name)) + when (symbolic?.let { holder.concreteAddr(it.addr) }) { + SYMBOLIC_NULL_ADDR -> MIN_SCORE + else -> MAX_SCORE + } + } + + is UtConstraintModel -> { + val scorer = UtConstraintScorer( + holder, + UtConstraint2ExpressionConverter(traverser), + typeRegistry, + typeResolver + ) + model.utConstraints.sumOf { it.accept(scorer) } + } + + else -> error("Not supported") + } +} + +class UtConstraintScorer( + private val holder: UtSolverStatusSAT, + private val varBuilder: UtConstraint2ExpressionConverter, + private val typeRegistry: TypeRegistry, + private val typeResolver: TypeResolver, +) : UtConstraintVisitor { + companion object { + private const val MAX_SCORE = ConstraintScoringStrategy.MAX_SCORE + private const val MIN_SCORE = ConstraintScoringStrategy.MIN_SCORE + private const val EPS = 0.01 + } + + + override fun visitUtNegatedConstraint(expr: UtNegatedConstraint): Double { + val cmp = expr.constraint.accept(this) + return MAX_SCORE - cmp + } + + override fun visitUtRefEqConstraint(expr: UtRefEqConstraint): Double { + val lhv = expr.lhv.accept(varBuilder) + val rhv = expr.rhv.accept(varBuilder) + + val lhvValue = holder.eval(lhv.addr).value() + val rhvValue = holder.eval(rhv.addr).value() + return when (lhvValue) { + rhvValue -> MIN_SCORE + else -> MAX_SCORE + } + } + + override fun visitUtRefGenericEqConstraint(expr: UtRefGenericEqConstraint): Double { + return MIN_SCORE // not considered in the scoring + } + + override fun visitUtRefTypeConstraint(expr: UtRefTypeConstraint): Double { + val operand = expr.operand.accept(varBuilder) + val classId = holder.findTypeOrNull(operand.addr)?.classId + return when { + classId == null -> MAX_SCORE + classId == expr.type -> MIN_SCORE + classId.isSubtypeOf(expr.type) -> MIN_SCORE + else -> MAX_SCORE + } + } + + override fun visitUtRefGenericTypeConstraint(expr: UtRefGenericTypeConstraint): Double { + return MIN_SCORE // not considered in the scoring + } + + override fun visitUtBoolConstraint(expr: UtBoolConstraint): Double { + val operand = expr.operand.accept(varBuilder) as PrimitiveValue + return when (holder.eval(operand.expr).boolValue()) { + true -> MIN_SCORE + else -> MAX_SCORE + } + } + + override fun visitUtEqConstraint(expr: UtEqConstraint): Double { + val lhv = expr.lhv.accept(varBuilder) as PrimitiveValue + val rhv = expr.rhv.accept(varBuilder) as PrimitiveValue + + val lhvValue = holder.eval(lhv.expr).numberValue() + val rhvValue = holder.eval(rhv.expr).numberValue() + + return when (lhvValue) { + rhvValue -> MIN_SCORE + else -> MAX_SCORE + } + } + + private fun scoreNumericComparison( + lhvVar: UtConstraintVariable, + rhvVar: UtConstraintVariable, + satisfied: (Number, Number) -> Boolean + ): Double { + val lhv = lhvVar.accept(varBuilder) as PrimitiveValue + val rhv = rhvVar.accept(varBuilder) as PrimitiveValue + + val lhvValue = holder.eval(lhv.expr).numberValue() + val rhvValue = holder.eval(rhv.expr).numberValue() + + return when { + satisfied(lhvValue, rhvValue) -> MIN_SCORE + else -> MAX_SCORE - MAX_SCORE / (MAX_SCORE + (lhvValue - rhvValue).abs().toDouble() + EPS) + } + } + + override fun visitUtLtConstraint(expr: UtLtConstraint): Double = + scoreNumericComparison(expr.lhv, expr.rhv) { a, b -> a < b } + + override fun visitUtGtConstraint(expr: UtGtConstraint): Double = + scoreNumericComparison(expr.lhv, expr.rhv) { a, b -> a > b } + + override fun visitUtLeConstraint(expr: UtLeConstraint): Double = + scoreNumericComparison(expr.lhv, expr.rhv) { a, b -> a <= b } + + override fun visitUtGeConstraint(expr: UtGeConstraint): Double = + scoreNumericComparison(expr.lhv, expr.rhv) { a, b -> a >= b } + + override fun visitUtAndConstraint(expr: UtAndConstraint): Double { + return expr.lhv.accept(this) + expr.rhv.accept(this) + } + + override fun visitUtOrConstraint(expr: UtOrConstraint): Double { + return min(expr.lhv.accept(this), expr.rhv.accept(this)) + } + + private fun Expr.numberValue() = this.value().asNumber() + + private fun Any.asNumber(): Number = when (this) { + is Number -> this + is Char -> this.code + else -> error("should be a number") + } + + /** + * Returns evaluated type by object's [addr] or null if there is no information about evaluated typeId. + */ + private fun UtSolverStatusSAT.findTypeOrNull(addr: UtAddrExpression): Type? { + val base = findBaseTypeOrNull(addr) + val dimensions = findNumDimensionsOrNull(addr) + return base?.let { b -> + dimensions?.let { d -> + if (d == 0) b + else b.makeArrayType(d) + } + } + } + + /** + * Returns evaluated type by object's [addr] or null if there is no information about evaluated typeId. + */ + private fun UtSolverStatusSAT.findBaseTypeOrNull(addr: UtAddrExpression): Type? { + val typeId = eval(typeRegistry.symTypeId(addr)).intValue() + return typeRegistry.typeByIdOrNull(typeId) + } + + /** + * We have a constraint stated that every number of dimensions is in [0..MAX_NUM_DIMENSIONS], so if we have a value + * from outside of the range, it means that we have never touched the number of dimensions for the given addr. + */ + private fun UtSolverStatusSAT.findNumDimensionsOrNull(addr: UtAddrExpression): Int? { + val numDimensions = eval(typeRegistry.symNumDimensions(addr)).intValue() + return if (numDimensions in 0..MAX_NUM_DIMENSIONS) numDimensions else null + } + + private fun UtSolverStatusSAT.constructTypeOrNull(addr: UtAddrExpression, defaultType: Type): Type? { + val evaluatedType = findBaseTypeOrNull(addr) ?: return defaultType + val numDimensions = findNumDimensionsOrNull(addr) ?: defaultType.numDimensions + + // If we have numDimensions greater than zero, we have to check if the object is a java.lang.Object + // that is actually an instance of some array (e.g., Object -> Int[]) + if (defaultType.isJavaLangObject() && numDimensions > 0) { + return evaluatedType.makeArrayType(numDimensions) + } + + // If it does not, the numDimension must be exactly the same as in the defaultType; otherwise, it means that we + // have never `touched` the element during the analysis. Note that `isTouched` does not point on it, + // because there might be an aliasing between this addr and an addr of some other object, that we really + // touched, e.g., the addr of `this` object. In such case we can remove null to construct UtNullModel later. + if (numDimensions != defaultType.numDimensions) { + return null + } + + require(numDimensions == defaultType.numDimensions) + + // if we have a RefType, but not an instance of java.lang.Object, or an java.lang.Object with zero dimension + if (defaultType is RefType) { + val inheritors = typeResolver.findOrConstructInheritorsIncludingTypes(defaultType) + return evaluatedType.takeIf { evaluatedType in inheritors } + ?: fallbackToDefaultTypeIfPossible(evaluatedType, defaultType) + } + + defaultType as ArrayType + + return constructArrayTypeOrNull(evaluatedType, defaultType, numDimensions) + ?: fallbackToDefaultTypeIfPossible(evaluatedType, defaultType) + } + + private fun constructArrayTypeOrNull(evaluatedType: Type, defaultType: ArrayType, numDimensions: Int): ArrayType? { + if (numDimensions <= 0) return null + + val actualType = evaluatedType.makeArrayType(numDimensions) + val actualBaseType = actualType.baseType + val defaultBaseType = defaultType.baseType + val defaultNumDimensions = defaultType.numDimensions + + if (actualType == defaultType) return actualType + + // i.e., if defaultType is Object[][], the actualType must be at least primType[][][] + if (actualBaseType is PrimType && defaultBaseType.isJavaLangObject() && numDimensions > defaultNumDimensions) { + return actualType + } + + // i.e., if defaultType is Object[][], the actualType must be at least RefType[][] + if (actualBaseType is RefType && defaultBaseType.isJavaLangObject() && numDimensions >= defaultNumDimensions) { + return actualType + } + + if (actualBaseType is RefType && defaultBaseType is RefType) { + val inheritors = typeResolver.findOrConstructInheritorsIncludingTypes(defaultBaseType) + // if actualBaseType in inheritors, actualType and defaultType must have the same numDimensions + if (actualBaseType in inheritors && numDimensions == defaultNumDimensions) return actualType + } + + return null + } + + /** + * Tries to determine whether it is possible to use [defaultType] instead of [actualType] or not. + */ + private fun fallbackToDefaultTypeIfPossible(actualType: Type, defaultType: Type): Type? { + val defaultBaseType = defaultType.baseType + + // It might be confusing we do we return null instead of default type here for the touched element. + // The answer is because sometimes we may have a real object with different type as an element here. + // I.e. we have int[][]. In the z3 memory it is an infinite array represented by const model and stores. + // Let's assume we know that the array has only one element. It means that solver can do whatever it wants + // with every other element but the first one. In such cases sometimes it sets as const model (or even store + // outside the array's length) existing objects (that has been touched during the execution) with a wrong + // (for the array) type. Because of such cases we have to return null as a sign that construction failed. + // If we return defaultType, it will mean that it might try to put model with an inappropriate type + // as const or store model. + if (defaultBaseType is PrimType) return null + + val actualBaseType = actualType.baseType + + require(actualBaseType is RefType) { "Expected RefType, but $actualBaseType found" } + require(defaultBaseType is RefType) { "Expected RefType, but $defaultBaseType found" } + + val ancestors = typeResolver.findOrConstructAncestorsIncludingTypes(defaultBaseType) + + // This is intended to fix a specific problem. We have code: + // ColoredPoint foo(Point[] array) { + // array[0].x = 5; + // return (ColoredPoint[]) array; + // } + // Since we don't have a way to connect types of the array and the elements within it, there might be situation + // when the array is ColoredPoint[], but the first element of it got type Point from the solver. + // In such case here we'll have ColoredPoint as defaultType and Point as actualType. It is obvious from the example + // that we can construct ColoredPoint instance instead of it with randomly filled colored-specific fields. + return defaultType.takeIf { actualBaseType in ancestors && actualType.numDimensions == defaultType.numDimensions } + } +} diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/ScoringStrategy.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/ScoringStrategy.kt new file mode 100644 index 0000000000..e457a1f550 --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/ScoringStrategy.kt @@ -0,0 +1,213 @@ +package org.utbot.engine.selectors.strategies + +import kotlinx.collections.immutable.PersistentList +import mu.KotlinLogging +import org.utbot.engine.* +import org.utbot.engine.pc.UtSolverStatus +import org.utbot.engine.pc.UtSolverStatusSAT +import org.utbot.framework.plugin.api.* +import org.utbot.framework.plugin.api.util.objectClassId +import soot.jimple.Stmt +import soot.toolkits.graph.ExceptionalUnitGraph +import kotlin.math.abs + +abstract class ScoringStrategy(graph: InterProceduralUnitGraph) : TraverseGraphStatistics(graph), ChoosingStrategy { + abstract fun score(executionState: ExecutionState): Double + + operator fun get(state: ExecutionState): Double = score(state) +} + +interface ScoringStrategyBuilder { + + fun build(graph: InterProceduralUnitGraph, traverser: Traverser): ScoringStrategy +} + +class ModelScoringStrategyBuilder( + private val targets: Map +) : ScoringStrategyBuilder { + override fun build(graph: InterProceduralUnitGraph, traverser: Traverser): ScoringStrategy = + ModelSynthesisScoringStrategy(graph, targets, traverser.typeRegistry) +} + +val defaultScoringStrategy get() = ModelScoringStrategyBuilder(emptyMap()) + + +private typealias Path = PersistentList + +class ModelSynthesisScoringStrategy( + graph: InterProceduralUnitGraph, + private val targets: Map, + private val typeRegistry: TypeRegistry +) : ScoringStrategy(graph) { + private val logger = KotlinLogging.logger("ModelSynthesisScoringStrategy") + private val distanceStatistics = DistanceStatistics(graph) + + companion object { + private const val SOFT_MAX_ARRAY_SIZE = 40 + private const val DEPTH_CHECK = 10 + + private const val PATH_SCORE_COEFFICIENT = 1.0 + private const val MODEL_SCORE_COEFFICIENT = 100.0 + + private const val INF_SCORE = Double.MAX_VALUE + private const val MAX_SCORE = 1.0 + private const val EPS = 0.01 + } + + // needed for resolver + private val hierarchy = Hierarchy(typeRegistry) + private val typeResolver: TypeResolver = TypeResolver(typeRegistry, hierarchy) + + private val stateModels = hashMapOf() + private val pathScores = hashMapOf() + + private fun buildResolver(memory: Memory, holder: UtSolverStatusSAT) = + Resolver(hierarchy, memory, typeRegistry, typeResolver, holder, "", SOFT_MAX_ARRAY_SIZE) + + override fun onTraversed(executionState: ExecutionState) { + distanceStatistics.onTraversed(executionState) + } + + override fun onVisit(edge: Edge) { + distanceStatistics.onVisit(edge) + } + + override fun onVisit(executionState: ExecutionState) { + distanceStatistics.onVisit(executionState) + } + + override fun onJoin(stmt: Stmt, graph: ExceptionalUnitGraph, shouldRegister: Boolean) { + distanceStatistics.onJoin(stmt, graph, shouldRegister) + } + + private fun shouldDropBasedOnScores(state: ExecutionState): Boolean { + val previous = run { + var current = state.path + val res = mutableListOf() + repeat(DEPTH_CHECK) { + if (current.isEmpty()) return@repeat + res += current + current = current.removeAt(current.lastIndex) + } + res.reversed() + } + val scores = previous.map { pathScores.getOrDefault(it, INF_SCORE) } + return scores.size >= DEPTH_CHECK && (0 until scores.lastIndex).all { scores[it] <= scores[it + 1] } + } + + override fun shouldDrop(state: ExecutionState): Boolean { + return shouldDropBasedOnScores(state) || distanceStatistics.shouldDrop(state) + } + + override fun score(executionState: ExecutionState): Double = pathScores.getOrPut(executionState.path) { + computePathScore(executionState) * PATH_SCORE_COEFFICIENT + + computeModelScore(executionState) * MODEL_SCORE_COEFFICIENT + } + + private fun computePathScore(executionState: ExecutionState): Double = + executionState.path.groupBy { it }.mapValues { it.value.size - 1 }.values.sum().toDouble() + + private fun computeModelScore(executionState: ExecutionState): Double { + val status = stateModels.getOrPut(executionState) { + executionState.solver.check(respectSoft = true) + } as? UtSolverStatusSAT ?: return INF_SCORE + val resolver = buildResolver(executionState.memory, status) + val entryStack = executionState.executionStack.first().localVariableMemory + val parameters = targets.keys.mapNotNull { entryStack.local(it) } + if (parameters.size != targets.keys.size) return INF_SCORE + + val afterParameters = resolver.resolveModels(parameters).modelsAfter.parameters + val models = targets.keys + .zip(afterParameters) + .toMap() + .mapValues { (_, model) -> + when (model) { + is UtAssembleModel -> model.origin!! + else -> model + } + } + + return computeScore(targets, models) + } + + private fun computeScore( + target: Map, + current: Map + ): Double { + var currentScore = 0.0 + for ((variable, model) in target) { + val comparison = when (val computedModel = current[variable]) { + null -> model.maxScore + else -> model.score(computedModel) + } + currentScore += comparison + } + return currentScore + } + + private val UtModel.maxScore: Double + get() = when (this) { + is UtPrimitiveModel -> MAX_SCORE + is UtAssembleModel -> this.origin?.maxScore ?: MAX_SCORE + is UtCompositeModel -> { + var res = 0.0 + for ((_, fieldModel) in this.fields) { + res += fieldModel.maxScore + } + res + } + + else -> INF_SCORE + } + + private fun UtModel.score(other: UtModel): Double = when { + this.javaClass != other.javaClass -> maxScore + this is UtPrimitiveModel -> { + other as UtPrimitiveModel + maxScore - maxScore / (maxScore + (this - other).abs().toDouble() + EPS) + } + + this is UtCompositeModel -> { + other as UtCompositeModel + var score = 0.0 + for ((field, fieldModel) in this.fields) { + val otherField = other.fields[field] + score += when (otherField) { + null -> fieldModel.maxScore + else -> fieldModel.score(otherField) + } + } + score + } + + else -> MAX_SCORE.also { + logger.error { "Unknown ut model" } + } + } + + private infix operator fun UtPrimitiveModel.minus(other: UtPrimitiveModel): Number = when (val value = this.value) { + is Byte -> value - (other.value as Byte) + is Short -> value - (other.value as Short) + is Char -> value - (other.value as Char) + is Int -> value - (other.value as Int) + is Long -> value - (other.value as Long) + is Float -> value - (other.value as Float) + is Double -> value - (other.value as Double) + is Boolean -> if (value) 1 else 0 - if (other.value as Boolean) 1 else 0 + else -> MAX_SCORE.also { + logger.error { "Unknown primitive model" } + } + } + + private fun Number.abs(): Number = when (this) { + is Byte -> abs(this.toInt()).toByte() + is Short -> abs(this.toInt()).toShort() + is Int -> abs(this) + is Long -> abs(this) + is Float -> abs(this) + is Double -> abs(this) + else -> 0.also { + logger.error { "Unknown number" } + } + } +} diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/util/numbers.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/util/numbers.kt new file mode 100644 index 0000000000..aec3da86c2 --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/util/numbers.kt @@ -0,0 +1,160 @@ +package org.utbot.engine.util + +import kotlin.reflect.KClass + + +fun Boolean.toInt(): Int = if (this) 1 else 0 +fun Int.toBoolean(): Boolean = this > 0 +fun Number.toBoolean(): Boolean = toInt().toBoolean() + +fun Number.recast(type: KClass<*>): Any = when (type) { + Byte::class -> toByte() + Short::class -> toShort() + Int::class -> toInt() + Long::class -> toLong() + Float::class -> toFloat() + Double::class -> toDouble() + else -> throw IllegalStateException("Unsupported number type") +} + +inline fun Number.recast() = recast(T::class) as T + +operator fun Number.plus(other: Number): Number = when (this) { + is Long -> this.toLong() + other.toLong() + is Int -> this.toInt() + other.toInt() + is Short -> this.toShort() + other.toShort() + is Byte -> this.toByte() + other.toByte() + is Double -> this.toDouble() + other.toDouble() + is Float -> this.toFloat() + other.toFloat() + else -> error("Unknown numeric type") +} + +operator fun Number.minus(other: Number): Number = when (this) { + is Long -> this.toLong() - other.toLong() + is Int -> this.toInt() - other.toInt() + is Short -> this.toShort() - other.toShort() + is Byte -> this.toByte() - other.toByte() + is Double -> this.toDouble() - other.toDouble() + is Float -> this.toFloat() - other.toFloat() + else -> error("Unknown numeric type") +} + +operator fun Number.times(other: Number): Number = when (this) { + is Long -> this.toLong() * other.toLong() + is Int -> this.toInt() * other.toInt() + is Short -> this.toShort() * other.toShort() + is Byte -> this.toByte() * other.toByte() + is Double -> this.toDouble() * other.toDouble() + is Float -> this.toFloat() * other.toFloat() + else -> error("Unknown numeric type") +} + +operator fun Number.div(other: Number): Number = when (this) { + is Long -> this.toLong() / other.toLong() + is Int -> this.toInt() / other.toInt() + is Short -> this.toShort() / other.toShort() + is Byte -> this.toByte() / other.toByte() + is Double -> this.toDouble() / other.toDouble() + is Float -> this.toFloat() / other.toFloat() + else -> error("Unknown numeric type") +} + +operator fun Number.rem(other: Number): Number = when (this) { + is Long -> this.toLong() % other.toLong() + is Int -> this.toInt() % other.toInt() + is Short -> this.toShort() % other.toShort() + is Byte -> this.toByte() % other.toByte() + is Double -> this.toDouble() % other.toDouble() + is Float -> this.toFloat() % other.toFloat() + else -> error("Unknown numeric type") +} + +operator fun Number.unaryMinus(): Number = when (this) { + is Long -> this.toLong().unaryMinus() + is Int -> this.toInt().unaryMinus() + is Short -> this.toShort().unaryMinus() + is Byte -> this.toByte().unaryMinus() + is Double -> this.toDouble().unaryMinus() + is Float -> this.toFloat().unaryMinus() + else -> error("Unknown numeric type") +} + +operator fun Number.compareTo(other: Number): Int = when (this) { + is Long -> this.toLong().compareTo(other.toLong()) + is Int -> this.toInt().compareTo(other.toInt()) + is Short -> this.toShort().compareTo(other.toShort()) + is Byte -> this.toByte().compareTo(other.toByte()) + is Double -> this.toDouble().compareTo(other.toDouble()) + is Float -> this.toFloat().compareTo(other.toFloat()) + else -> error("Unknown numeric type") +} + +fun Number.shl(bits: Int): Number = when (this) { + is Long -> this.toLong().shl(bits) + is Int -> this.toInt().shl(bits) + is Short -> this.toShort().shl(bits) + is Byte -> this.toByte().shl(bits) + is Double -> this.toDouble().shl(bits) + is Float -> this.toFloat().shl(bits) + else -> error("Unknown numeric type") +} + +fun Number.shr(bits: Int): Number = when (this) { + is Long -> this.toLong().shr(bits) + is Int -> this.toInt().shr(bits) + is Short -> this.toShort().shr(bits) + is Byte -> this.toByte().shr(bits) + is Double -> this.toDouble().shr(bits) + is Float -> this.toFloat().shr(bits) + else -> error("Unknown numeric type") +} + +fun Number.ushr(bits: Int): Number = when (this) { + is Long -> this.toLong().ushr(bits) + is Int -> this.toInt().ushr(bits) + is Short -> this.toShort().ushr(bits) + is Byte -> this.toByte().ushr(bits) + is Double -> this.toDouble().ushr(bits) + is Float -> this.toFloat().ushr(bits) + else -> error("Unknown numeric type") +} + +infix fun Number.and(other: Number): Number = when (this) { + is Long -> this.toLong() and other.toLong() + is Int -> this.toInt() and other.toInt() + is Short -> this.toShort() and other.toShort() + is Byte -> this.toByte() and other.toByte() + is Double -> this.toDouble() and other.toDouble() + is Float -> this.toFloat() and other.toFloat() + else -> error("Unknown numeric type") +} + +infix fun Number.or(other: Number): Number = when (this) { + is Long -> this.toLong() or other.toLong() + is Int -> this.toInt() or other.toInt() + is Short -> this.toShort() or other.toShort() + is Byte -> this.toByte() or other.toByte() + is Double -> this.toDouble() or other.toDouble() + is Float -> this.toFloat() or other.toFloat() + else -> error("Unknown numeric type") +} + +infix fun Number.xor(other: Number): Number = when (this) { + is Long -> this.toLong() xor other.toLong() + is Int -> this.toInt() xor other.toInt() + is Short -> this.toShort() xor other.toShort() + is Byte -> this.toByte() xor other.toByte() + is Double -> this.toDouble() xor other.toDouble() + is Float -> this.toFloat() xor other.toFloat() + else -> error("Unknown numeric type") +} + +fun Number.abs(): Number = when (this) { + is Long -> kotlin.math.abs(this) + is Int -> kotlin.math.abs(this) + is Short -> kotlin.math.abs(this.toInt()).toShort() + is Byte -> kotlin.math.abs(this.toInt()).toByte() + is Double -> kotlin.math.abs(this) + is Float -> kotlin.math.abs(this) + else -> error("Unknown numeric type") +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Extensions.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Extensions.kt index 7fc3dc0904..f996b7b572 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Extensions.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Extensions.kt @@ -41,6 +41,7 @@ fun Expr.value(unsigned: Boolean = false): Any = when (this) { } internal fun Expr.intValue() = this.value() as Int +internal fun Expr.boolValue() = this.value() as Boolean /** * Converts a variable to given type. diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Z3initializer.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Z3initializer.kt index 97677c78cd..134a4f2e81 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Z3initializer.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Z3initializer.kt @@ -4,7 +4,6 @@ import com.microsoft.z3.Context import com.microsoft.z3.Global import org.utbot.common.FileUtil import java.io.File -import java.nio.file.Files.createTempDirectory abstract class Z3Initializer : AutoCloseable { protected val context: Context by lazy { diff --git a/utbot-framework/src/main/kotlin/org/utbot/external/api/UtModelFactory.kt b/utbot-framework/src/main/kotlin/org/utbot/external/api/UtModelFactory.kt index ec12b3319c..03c5f49dde 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/external/api/UtModelFactory.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/external/api/UtModelFactory.kt @@ -83,4 +83,4 @@ fun fieldIdForJavaField(field: Field): FieldId { */ fun classIdForType(clazz: Class<*>): ClassId { return clazz.id -} \ No newline at end of file +} diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/assemble/AssembleModelGenerator.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/assemble/AssembleModelGenerator.kt index 3ea84673ec..e1740a71ec 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/framework/assemble/AssembleModelGenerator.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/assemble/AssembleModelGenerator.kt @@ -11,30 +11,7 @@ import org.utbot.framework.modifications.AnalysisMode.SettersAndDirectAccessors import org.utbot.framework.modifications.ConstructorAnalyzer import org.utbot.framework.modifications.ConstructorAssembleInfo import org.utbot.framework.modifications.UtBotFieldsModificatorsSearcher -import org.utbot.framework.plugin.api.ClassId -import org.utbot.framework.plugin.api.ConstructorId -import org.utbot.framework.plugin.api.DirectFieldAccessId -import org.utbot.framework.plugin.api.ExecutableId -import org.utbot.framework.plugin.api.FieldId -import org.utbot.framework.plugin.api.StatementId -import org.utbot.framework.plugin.api.UtArrayModel -import org.utbot.framework.plugin.api.UtAssembleModel -import org.utbot.framework.plugin.api.UtClassRefModel -import org.utbot.framework.plugin.api.UtCompositeModel -import org.utbot.framework.plugin.api.UtDirectSetFieldModel -import org.utbot.framework.plugin.api.UtEnumConstantModel -import org.utbot.framework.plugin.api.UtExecutableCallModel -import org.utbot.framework.plugin.api.UtLambdaModel -import org.utbot.framework.plugin.api.UtModel -import org.utbot.framework.plugin.api.UtNewInstanceInstrumentation -import org.utbot.framework.plugin.api.UtNullModel -import org.utbot.framework.plugin.api.UtPrimitiveModel -import org.utbot.framework.plugin.api.UtReferenceModel -import org.utbot.framework.plugin.api.UtStatementModel -import org.utbot.framework.plugin.api.UtStaticMethodInstrumentation -import org.utbot.framework.plugin.api.UtVoidModel -import org.utbot.framework.plugin.api.hasDefaultValue -import org.utbot.framework.plugin.api.isMockModel +import org.utbot.framework.plugin.api.* import org.utbot.framework.plugin.api.util.defaultValueModel import org.utbot.framework.plugin.api.util.executableId import org.utbot.framework.plugin.api.util.jClass @@ -185,6 +162,7 @@ class AssembleModelGenerator(private val methodPackageName: String) { is UtClassRefModel, is UtVoidModel, is UtEnumConstantModel, + is UtConstraintModel, is UtLambdaModel -> utModel is UtArrayModel -> assembleArrayModel(utModel) is UtCompositeModel -> assembleCompositeModel(utModel) diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/codegen/model/constructor/tree/CgMethodConstructor.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/codegen/model/constructor/tree/CgMethodConstructor.kt index 3be50621e5..0f39fa8927 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/framework/codegen/model/constructor/tree/CgMethodConstructor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/codegen/model/constructor/tree/CgMethodConstructor.kt @@ -76,43 +76,7 @@ import org.utbot.framework.codegen.model.util.nullLiteral import org.utbot.framework.codegen.model.util.resolve import org.utbot.framework.fields.ExecutionStateAnalyzer import org.utbot.framework.fields.FieldPath -import org.utbot.framework.plugin.api.BuiltinClassId -import org.utbot.framework.plugin.api.BuiltinMethodId -import org.utbot.framework.plugin.api.ClassId -import org.utbot.framework.plugin.api.CodegenLanguage -import org.utbot.framework.plugin.api.ConcreteExecutionFailureException -import org.utbot.framework.plugin.api.ConstructorId -import org.utbot.framework.plugin.api.ExecutableId -import org.utbot.framework.plugin.api.FieldId -import org.utbot.framework.plugin.api.MethodId -import org.utbot.framework.plugin.api.TimeoutException -import org.utbot.framework.plugin.api.TypeParameters -import org.utbot.framework.plugin.api.UtArrayModel -import org.utbot.framework.plugin.api.UtAssembleModel -import org.utbot.framework.plugin.api.UtClassRefModel -import org.utbot.framework.plugin.api.UtCompositeModel -import org.utbot.framework.plugin.api.UtConcreteExecutionFailure -import org.utbot.framework.plugin.api.UtDirectSetFieldModel -import org.utbot.framework.plugin.api.UtEnumConstantModel -import org.utbot.framework.plugin.api.UtExecution -import org.utbot.framework.plugin.api.UtExecutionFailure -import org.utbot.framework.plugin.api.UtExecutionSuccess -import org.utbot.framework.plugin.api.UtExplicitlyThrownException -import org.utbot.framework.plugin.api.UtLambdaModel -import org.utbot.framework.plugin.api.UtModel -import org.utbot.framework.plugin.api.UtNewInstanceInstrumentation -import org.utbot.framework.plugin.api.UtNullModel -import org.utbot.framework.plugin.api.UtPrimitiveModel -import org.utbot.framework.plugin.api.UtReferenceModel -import org.utbot.framework.plugin.api.UtSandboxFailure -import org.utbot.framework.plugin.api.UtStaticMethodInstrumentation -import org.utbot.framework.plugin.api.UtSymbolicExecution -import org.utbot.framework.plugin.api.UtTimeoutException -import org.utbot.framework.plugin.api.UtVoidModel -import org.utbot.framework.plugin.api.isNotNull -import org.utbot.framework.plugin.api.isNull -import org.utbot.framework.plugin.api.onFailure -import org.utbot.framework.plugin.api.onSuccess +import org.utbot.framework.plugin.api.* import org.utbot.framework.plugin.api.util.doubleArrayClassId import org.utbot.framework.plugin.api.util.doubleClassId import org.utbot.framework.plugin.api.util.doubleWrapperClassId @@ -187,7 +151,12 @@ internal class CgMethodConstructor(val context: CgContext) : CgContextOwner by c instrumentation .filterIsInstance() .groupBy { it.methodId.classId } - .forEach { (classId, methodMocks) -> mockFrameworkManager.mockStaticMethodsOfClass(classId, methodMocks) } + .forEach { (classId, methodMocks) -> + mockFrameworkManager.mockStaticMethodsOfClass( + classId, + methodMocks + ) + } if (generateWarningsForStaticMocking && forceStaticMocking == ForceStaticMocking.FORCE) { // warn user about forced using static mocks @@ -403,7 +372,7 @@ internal class CgMethodConstructor(val context: CgContext) : CgContextOwner by c +CgMultilineComment(warningLine + neededStackTraceLines.reversed()) } - private fun String.escapeControlChars() : String { + private fun String.escapeControlChars(): String { return this.replace("\b", "\\b").replace("\n", "\\n").replace("\t", "\\t").replace("\r", "\\r") } @@ -700,6 +669,10 @@ internal class CgMethodConstructor(val context: CgContext) : CgContextOwner by c // Unit result is considered in generateResultAssertions method error("Unexpected UtVoidModel in deep equals") } + + else -> { + error("Unexpected ${expectedModel::class.java} in deep equals") + } } } } @@ -967,6 +940,7 @@ internal class CgMethodConstructor(val context: CgContext) : CgContextOwner by c is UtArrayModel, is UtClassRefModel, is UtEnumConstantModel, + is UtConstraintModel, is UtVoidModel -> { // only [UtCompositeModel] and [UtAssembleModel] have fields to traverse } @@ -1008,6 +982,7 @@ internal class CgMethodConstructor(val context: CgContext) : CgContextOwner by c is UtArrayModel, is UtClassRefModel, is UtEnumConstantModel, + is UtConstraintModel, is UtVoidModel -> { // only [UtCompositeModel] and [UtAssembleModel] have fields to traverse } @@ -1819,4 +1794,4 @@ internal class CgMethodConstructor(val context: CgContext) : CgContextOwner by c +this } } -} \ No newline at end of file +} diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/codegen/model/constructor/tree/CgVariableConstructor.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/codegen/model/constructor/tree/CgVariableConstructor.kt index 85d7c9893b..8cdeef2851 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/framework/codegen/model/constructor/tree/CgVariableConstructor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/codegen/model/constructor/tree/CgVariableConstructor.kt @@ -31,35 +31,8 @@ import org.utbot.framework.codegen.model.util.isAccessibleFrom import org.utbot.framework.codegen.model.util.lessThan import org.utbot.framework.codegen.model.util.nullLiteral import org.utbot.framework.codegen.model.util.resolve -import org.utbot.framework.plugin.api.BuiltinClassId -import org.utbot.framework.plugin.api.ClassId -import org.utbot.framework.plugin.api.ConstructorId -import org.utbot.framework.plugin.api.MethodId -import org.utbot.framework.plugin.api.UtArrayModel -import org.utbot.framework.plugin.api.UtAssembleModel -import org.utbot.framework.plugin.api.UtClassRefModel -import org.utbot.framework.plugin.api.UtCompositeModel -import org.utbot.framework.plugin.api.UtDirectSetFieldModel -import org.utbot.framework.plugin.api.UtEnumConstantModel -import org.utbot.framework.plugin.api.UtExecutableCallModel -import org.utbot.framework.plugin.api.UtLambdaModel -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.UtReferenceModel -import org.utbot.framework.plugin.api.UtVoidModel -import org.utbot.framework.plugin.api.util.classClassId -import org.utbot.framework.plugin.api.util.defaultValueModel -import org.utbot.framework.plugin.api.util.jField -import org.utbot.framework.plugin.api.util.findFieldByIdOrNull -import org.utbot.framework.plugin.api.util.id -import org.utbot.framework.plugin.api.util.intClassId -import org.utbot.framework.plugin.api.util.isArray -import org.utbot.framework.plugin.api.util.isPrimitiveWrapperOrString -import org.utbot.framework.plugin.api.util.isStatic -import org.utbot.framework.plugin.api.util.stringClassId -import org.utbot.framework.plugin.api.util.supertypeOfAnonymousClass -import org.utbot.framework.plugin.api.util.wrapperByPrimitive +import org.utbot.framework.plugin.api.* +import org.utbot.framework.plugin.api.util.* /** * Constructs CgValue or CgVariable given a UtModel @@ -114,6 +87,7 @@ internal class CgVariableConstructor(val context: CgContext) : is UtPrimitiveModel -> CgLiteral(model.classId, model.value) is UtReferenceModel -> error("Unexpected UtReferenceModel: ${model::class}") is UtVoidModel -> error("Unexpected UtVoidModel: ${model::class}") + is UtConstraintModel -> error("Unexpected ut model: ${model::class}") } } } @@ -478,4 +452,4 @@ internal class CgVariableConstructor(val context: CgContext) : private fun String.toVarName(): String = nameGenerator.variableName(this) -} \ No newline at end of file +} diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/concrete/MockValueConstructor.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/concrete/MockValueConstructor.kt index 4768cbf68b..cbabd300c3 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/framework/concrete/MockValueConstructor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/concrete/MockValueConstructor.kt @@ -133,6 +133,7 @@ class MockValueConstructor( is UtAssembleModel -> UtConcreteValue(constructFromAssembleModel(model), model.classId.jClass) is UtLambdaModel -> UtConcreteValue(constructFromLambdaModel(model)) is UtVoidModel -> UtConcreteValue(Unit) + else -> error("Unexpected model ${model::class}") } } diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/fields/ExecutionStateAnalyzer.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/fields/ExecutionStateAnalyzer.kt index 196ee58532..723abc6fee 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/framework/fields/ExecutionStateAnalyzer.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/fields/ExecutionStateAnalyzer.kt @@ -266,5 +266,6 @@ fun UtModel.accept(visitor: UtModelVisitor, data: D) = visitor.run { is UtPrimitiveModel -> visit(element, data) is UtReferenceModel -> visit(element, data) is UtVoidModel -> visit(element, data) + else -> error("Unexpected ${this::class.java} model it accept") } } diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/minimization/Minimization.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/minimization/Minimization.kt index c6b336098a..b33f4b07a9 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/framework/minimization/Minimization.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/minimization/Minimization.kt @@ -1,24 +1,7 @@ package org.utbot.framework.minimization import org.utbot.framework.UtSettings -import org.utbot.framework.plugin.api.EnvironmentModels -import org.utbot.framework.plugin.api.UtArrayModel -import org.utbot.framework.plugin.api.UtAssembleModel -import org.utbot.framework.plugin.api.UtClassRefModel -import org.utbot.framework.plugin.api.UtCompositeModel -import org.utbot.framework.plugin.api.UtConcreteExecutionFailure -import org.utbot.framework.plugin.api.UtDirectSetFieldModel -import org.utbot.framework.plugin.api.UtEnumConstantModel -import org.utbot.framework.plugin.api.UtExecutableCallModel -import org.utbot.framework.plugin.api.UtExecution -import org.utbot.framework.plugin.api.UtExecutionFailure -import org.utbot.framework.plugin.api.UtExecutionResult -import org.utbot.framework.plugin.api.UtLambdaModel -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.UtStatementModel -import org.utbot.framework.plugin.api.UtVoidModel +import org.utbot.framework.plugin.api.* /** @@ -221,7 +204,7 @@ private fun UtModel.calculateSize(used: MutableSet = mutableSetOf()): I return when (this) { is UtNullModel, is UtPrimitiveModel, UtVoidModel -> 0 - is UtClassRefModel, is UtEnumConstantModel, is UtArrayModel -> 1 + is UtClassRefModel, is UtEnumConstantModel, is UtArrayModel, is UtConstraintModel -> 1 is UtAssembleModel -> 1 + allStatementsChain.sumOf { it.calculateSize(used) } is UtCompositeModel -> 1 + fields.values.sumOf { it.calculateSize(used) } is UtLambdaModel -> 1 + capturedValues.sumOf { it.calculateSize(used) } @@ -260,4 +243,4 @@ private fun addExtraIfLastInstructionIsException( * Takes an exception name, a class name, a method signature and a line number from exception. */ private fun Throwable.exceptionToInfo(): String = - this::class.java.name + (this.stackTrace.firstOrNull()?.run { className + methodName + lineNumber } ?: "null") \ No newline at end of file + this::class.java.name + (this.stackTrace.firstOrNull()?.run { className + methodName + lineNumber } ?: "null") diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/plugin/api/TestCaseGenerator.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/plugin/api/TestCaseGenerator.kt index 8c8a35f602..d7b5bd93eb 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/framework/plugin/api/TestCaseGenerator.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/plugin/api/TestCaseGenerator.kt @@ -15,13 +15,13 @@ import org.utbot.common.bracket import org.utbot.common.runBlockingWithCancellationPredicate import org.utbot.common.runIgnoringCancellationException import org.utbot.common.trace -import org.utbot.engine.EngineController -import org.utbot.engine.Mocker -import org.utbot.engine.UtBotSymbolicEngine +import org.utbot.engine.* +import org.utbot.engine.executeConcretely import org.utbot.framework.TestSelectionStrategyType import org.utbot.framework.UtSettings import org.utbot.framework.UtSettings.checkSolverTimeoutMillis import org.utbot.framework.UtSettings.disableCoroutinesDebug +import org.utbot.framework.UtSettings.enableSynthesis import org.utbot.framework.UtSettings.utBotGenerationTimeoutInMillis import org.utbot.framework.UtSettings.warmupConcreteExecution import org.utbot.framework.codegen.model.util.checkFrameworkDependencies @@ -35,12 +35,17 @@ import org.utbot.framework.plugin.api.util.intArrayClassId import org.utbot.framework.plugin.api.util.utContext import org.utbot.framework.plugin.api.util.withUtContext import org.utbot.framework.plugin.services.JdkInfo +import org.utbot.framework.synthesis.Synthesizer +import org.utbot.framework.synthesis.postcondition.constructors.EmptyPostCondition +import org.utbot.framework.synthesis.postcondition.constructors.PostConditionConstructor import org.utbot.framework.util.SootUtils +import org.utbot.framework.util.executableId import org.utbot.framework.util.jimpleBody import org.utbot.framework.util.toModel import org.utbot.instrumentation.ConcreteExecutor import org.utbot.instrumentation.warmup import org.utbot.instrumentation.warmup.Warmup +import soot.SootMethod import java.io.File import java.nio.file.Path import java.util.* @@ -119,12 +124,22 @@ open class TestCaseGenerator( @Throws(CancellationException::class) fun generateAsync( controller: EngineController, - method: ExecutableId, + method: SymbolicEngineTarget, mockStrategy: MockStrategyApi, chosenClassesToMockAlways: Set = Mocker.javaDefaultClasses.mapTo(mutableSetOf()) { it.id }, - executionTimeEstimator: ExecutionTimeEstimator = ExecutionTimeEstimator(utBotGenerationTimeoutInMillis, 1) + executionTimeEstimator: ExecutionTimeEstimator = ExecutionTimeEstimator(utBotGenerationTimeoutInMillis, 1), + useSynthesis: Boolean = enableSynthesis, + postConditionConstructor: PostConditionConstructor = EmptyPostCondition, ): Flow { - val engine = createSymbolicEngine(controller, method, mockStrategy, chosenClassesToMockAlways, executionTimeEstimator) + val engine = createSymbolicEngine( + controller, + method, + mockStrategy, + chosenClassesToMockAlways, + executionTimeEstimator, + useSynthesis, + postConditionConstructor, + ) engineActions.map { engine.apply(it) } engineActions.clear() return defaultTestFlow(engine, executionTimeEstimator.userTimeout) @@ -159,10 +174,12 @@ open class TestCaseGenerator( val engine: UtBotSymbolicEngine = createSymbolicEngine( controller, - method, + SymbolicEngineTarget.from(method), mockStrategy, chosenClassesToMockAlways, - executionTimeEstimator + executionTimeEstimator, + enableSynthesis, + EmptyPostCondition ) engineActions.map { engine.apply(it) } @@ -218,7 +235,7 @@ open class TestCaseGenerator( return methods.map { method -> UtMethodTestSet( method, - minimizeExecutions(method2executions.getValue(method)), + minimizeExecutions(method2executions.getValue(method).toAssemble(method)), jimpleBody(method), method2errors.getValue(method) ) @@ -254,10 +271,12 @@ open class TestCaseGenerator( private fun createSymbolicEngine( controller: EngineController, - method: ExecutableId, + method: SymbolicEngineTarget, mockStrategyApi: MockStrategyApi, chosenClassesToMockAlways: Set, - executionTimeEstimator: ExecutionTimeEstimator + executionTimeEstimator: ExecutionTimeEstimator, + useSynthesis: Boolean, + postConditionConstructor: PostConditionConstructor = EmptyPostCondition, ): UtBotSymbolicEngine { logger.debug("Starting symbolic execution for $method --$mockStrategyApi--") return UtBotSymbolicEngine( @@ -267,7 +286,9 @@ open class TestCaseGenerator( dependencyPaths = dependencyPaths, mockStrategy = mockStrategyApi.toModel(), chosenClassesToMockAlways = chosenClassesToMockAlways, - solverTimeoutInMillis = executionTimeEstimator.updatedSolverCheckTimeoutMillis + solverTimeoutInMillis = executionTimeEstimator.updatedSolverCheckTimeoutMillis, + useSynthesis = useSynthesis, + postConditionConstructor = postConditionConstructor ) } @@ -332,6 +353,95 @@ open class TestCaseGenerator( } } + internal fun generateWithPostCondition( + method: SootMethod, + mockStrategy: MockStrategyApi, + postConditionConstructor: PostConditionConstructor, + ): List { + if (isCanceled()) return emptyList() + + val executions = mutableListOf() + val errors = mutableMapOf() + + + runIgnoringCancellationException { + runBlockingWithCancellationPredicate(isCanceled) { + generateAsync( + EngineController(), + SymbolicEngineTarget.from(method), + mockStrategy, + useSynthesis = false, + postConditionConstructor = postConditionConstructor, + ).collect { + when (it) { + is UtExecution -> executions += it + is UtError -> errors.merge(it.description, 1, Int::plus) + } + } + } + } + + val minimizedExecutions = minimizeExecutions(executions) + return minimizedExecutions + } + + protected fun List.toAssemble(method: ExecutableId): List = + map { execution -> + val symbolicExecution = (execution as? UtSymbolicExecution) + ?: return@map execution + + val newBeforeState = mapEnvironmentModels(method, symbolicExecution, symbolicExecution.stateBefore) { + it.modelsBefore + } ?: return@map execution + val newAfterState = getConcreteAfterState(method, newBeforeState) ?: return@map execution + + symbolicExecution.copy( + newBeforeState, + newAfterState, + symbolicExecution.result, + symbolicExecution.coverage + ) + } + + private fun mapEnvironmentModels( + method: ExecutableId, + symbolicExecution: UtSymbolicExecution, + models: EnvironmentModels, + selector: (ConstrainedExecution) -> List + ): EnvironmentModels? { + val constrainedExecution = symbolicExecution.constrainedExecution ?: return null + val aa = Synthesizer(this@TestCaseGenerator, method, selector(constrainedExecution)) + val synthesizedModels = aa.synthesize() + + val (synthesizedThis, synthesizedParameters) = models.thisInstance?.let { + synthesizedModels.first() to synthesizedModels.drop(1) + } ?: (null to synthesizedModels) + val newThisModel = models.thisInstance?.let { synthesizedThis ?: it } + val newParameters = models.parameters.zip(synthesizedParameters).map { it.second ?: it.first } + return EnvironmentModels( + newThisModel, + newParameters, + models.statics + ) + } + + private fun getConcreteAfterState(method: ExecutableId, stateBefore: EnvironmentModels): EnvironmentModels? = try { + val concreteExecutor = ConcreteExecutor( + UtExecutionInstrumentation, + this.classpath ?: "", + dependencyPaths + ).apply { this.classLoader = utContext.classLoader } + val concreteExecutionResult = runBlocking { + concreteExecutor.executeConcretely( + method, + stateBefore, + emptyList() + ) + } + concreteExecutionResult.stateAfter + } catch (e: Throwable) { + null + } } diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/CompositeUnitExpander.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/CompositeUnitExpander.kt new file mode 100644 index 0000000000..6bb609fb4a --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/CompositeUnitExpander.kt @@ -0,0 +1,61 @@ +package org.utbot.framework.synthesis + +import org.utbot.framework.modifications.StatementsStorage +import org.utbot.framework.plugin.api.ClassId +import org.utbot.framework.plugin.api.ConstructorId +import org.utbot.framework.plugin.api.ExecutableId +import org.utbot.framework.plugin.api.MethodId +import org.utbot.framework.plugin.api.util.isStatic + +class CompositeUnitExpander( + private val statementsStorage: StatementsStorage +) { + private fun ExecutableId.thisParamOrEmptyList() = + if (this is MethodId && !this.isStatic) { + listOf(this.classId) + } else { + emptyList() + } + + private val StatementsStorage.definedClasses get() = items.keys.map { it.classId }.toSet() + + fun expand(objectUnit: ObjectUnit): List { + if (objectUnit.isPrimitive()) { + return emptyList() + } + if (objectUnit.classId !in statementsStorage.definedClasses) { + statementsStorage.update(setOf(objectUnit.classId).expandable()) + } + val mutators = findAllMutators(objectUnit.classId) + + val expanded = mutators.map { method -> + MethodUnit( + objectUnit.classId, + method, + (method.thisParamOrEmptyList() + method.parameters).map { ObjectUnit(it) } + ) + } + return expanded + } + + private fun findAllMutators(classId: ClassId) = findConstructors(classId) + findMutators(classId) + + private fun findConstructors(classId: ClassId): List = + statementsStorage.items + .filterKeys { method -> method.classId == classId } + .keys + .filterIsInstance() + .toList() + + private fun findMutators(classId: ClassId): List = + statementsStorage.items + .filter { (method, info) -> + val sameClass = method.classId == classId + val modifiesSomething = info.modifiedFields.any { it.declaringClass == classId } + val isStaticInit = method.name == "" + sameClass && modifiesSomething && !isStaticInit + } + .keys + .filterIsInstance() + .toList() +} diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/Resolver.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/Resolver.kt new file mode 100644 index 0000000000..70958246d6 --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/Resolver.kt @@ -0,0 +1,160 @@ +package org.utbot.framework.synthesis + +import org.utbot.engine.defaultIdGenerator +import org.utbot.framework.plugin.api.* +import org.utbot.framework.plugin.api.util.defaultValueModel +import org.utbot.framework.util.nextModelName +import java.util.IdentityHashMap + +class Resolver( + parameterModels: List, + val synthesisUnitContext: SynthesisUnitContext, + unitToParameter: IdentityHashMap, +) { + private val unitToModel = IdentityHashMap().apply { + unitToParameter.toList().forEach { (it, parameter) -> this[it] = parameterModels[parameter.number] } + } + + fun resolve(unit: SynthesisUnit): UtModel = + when (unit) { + is MethodUnit -> unitToModel.getOrPut(unit) { resolveMethodUnit(unit) } + is ObjectUnit -> unitToModel[unit] ?: error("Can't map $unit") + is NullUnit -> UtNullModel(unit.classId) + is ReferenceToUnit -> resolve(synthesisUnitContext[unit.reference]) + is ArrayUnit -> unitToModel.getOrPut(unit) { resolveArray(unit) } + is ListUnit -> unitToModel.getOrPut(unit) { resolveList(unit) } + is SetUnit -> unitToModel.getOrPut(unit) { resolveSet(unit) } + is MapUnit -> unitToModel.getOrPut(unit) { resolveMap(unit) } + } + + private fun resolveMethodUnit(unit: MethodUnit): UtModel = + when (val method = unit.method) { + is ConstructorId -> resolveConstructorInvoke(unit, method) + is MethodId -> resolveVirtualInvoke(unit, method) + else -> error("Unexpected method unit in resolver: $unit") + } + + private fun resolveVirtualInvoke(unit: MethodUnit, method: MethodId): UtModel { + val resolvedModels = unit.params.map { resolve(it) } + + val thisModel = resolvedModels.firstOrNull() ?: error("No `this` parameter found for $method") + val modelsWithoutThis = resolvedModels.drop(1) + + if (thisModel !is UtAssembleModel) { + error("$thisModel is not assemble") + } + + val modificationChain = (thisModel.modificationsChain as? MutableList) + ?: error("Can't cast to mutable") + + modificationChain.add( + UtExecutableCallModel(thisModel, unit.method, modelsWithoutThis) + ) + + return thisModel + } + + private fun resolveConstructorInvoke(unit: MethodUnit, method: ConstructorId): UtModel { + val resolvedModels = unit.params.map { resolve(it) } + + val instantiationChain = mutableListOf() + val modificationChain = mutableListOf() + + val model = UtAssembleModel( + defaultIdGenerator.createId(), + unit.classId, + nextModelName("refModel_${unit.classId.simpleName}"), + instantiationChain, + modificationChain + ) + + instantiationChain.add( + UtExecutableCallModel(model, unit.method, resolvedModels, model) + ) + + return model + } + + private fun resolveCollection( + unit: ElementContainingUnit, + constructorId: ConstructorId, + modificationId: MethodId + ): UtModel { + val elements = unit.elements.map { resolve(synthesisUnitContext[it.second]) } + + val instantiationChain = mutableListOf() + val modificationChain = mutableListOf() + + val model = UtAssembleModel( + defaultIdGenerator.createId(), + unit.classId, + nextModelName("refModel_${unit.classId.simpleName}"), + instantiationChain, + modificationChain + ) + + instantiationChain.add( + UtExecutableCallModel(model, constructorId, listOf(), model) + ) + + for (value in elements) { + modificationChain.add( + UtExecutableCallModel( + model, modificationId, listOf(value), + ) + ) + } + + return model + } + + private fun resolveList(unit: ListUnit): UtModel = resolveCollection(unit, unit.constructorId, unit.addId) + + private fun resolveSet(unit: SetUnit): UtModel = resolveCollection(unit, unit.constructorId, unit.addId) + + private fun resolveMap(unit: MapUnit): UtModel { + val elements = unit.elements.map { + resolve(synthesisUnitContext[it.first]) to resolve(synthesisUnitContext[it.second]) + } + + val instantiationChain = mutableListOf() + val modificationChain = mutableListOf() + + val model = UtAssembleModel( + defaultIdGenerator.createId(), + unit.classId, + nextModelName("refModel_${unit.classId.simpleName}"), + instantiationChain, + modificationChain + ) + + instantiationChain.add( + UtExecutableCallModel(model, unit.constructorId, listOf(), model) + ) + + for ((key, value) in elements) { + modificationChain.add( + UtExecutableCallModel( + model, unit.putId, listOf(key, value), + ) + ) + } + + return model + } + + private fun resolveArray(unit: ArrayUnit): UtModel { + val lengthModel = resolve(synthesisUnitContext[unit.length]) as UtPrimitiveModel + val elements = unit.elements.associate { + ((resolve(synthesisUnitContext[it.first]) as UtPrimitiveModel).value as Int) to resolve(synthesisUnitContext[it.second]) + } + + return UtArrayModel( + defaultIdGenerator.createId(), + unit.classId, + lengthModel.value as Int, + unit.classId.elementClassId!!.defaultValueModel(), + elements.toMutableMap() + ) + } +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/SynthesisMethodContext.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/SynthesisMethodContext.kt new file mode 100644 index 0000000000..deec7c13a7 --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/SynthesisMethodContext.kt @@ -0,0 +1,236 @@ +package org.utbot.framework.synthesis + +import org.utbot.engine.* +import org.utbot.framework.plugin.api.* +import org.utbot.framework.plugin.api.util.* +import soot.ArrayType +import soot.RefType +import soot.SootClass +import soot.SootMethod +import soot.Type +import soot.VoidType +import soot.jimple.IdentityStmt +import soot.jimple.JimpleBody +import soot.jimple.NullConstant +import soot.jimple.Stmt +import soot.jimple.internal.JimpleLocal +import soot.BooleanType +import soot.ByteType +import soot.CharType +import soot.DoubleType +import soot.FloatType +import soot.IntType +import soot.LongType +import soot.RefLikeType +import soot.Scene +import soot.ShortType +import java.util.* + +internal fun ClassId.toSoot(): SootClass = Scene.v().getSootClass(this.name) + +internal fun ClassId.toSootType(): Type = when { + this.isPrimitive -> when (this) { + booleanClassId -> BooleanType.v() + byteClassId -> ByteType.v() + shortClassId -> ShortType.v() + charClassId -> CharType.v() + intClassId -> IntType.v() + longClassId -> LongType.v() + floatClassId -> FloatType.v() + doubleClassId -> DoubleType.v() + else -> error("Unexpected primitive type: $this") + } + this.isArray -> elementClassId!!.toSootType().makeArrayType() + else -> toSoot().type +} + +data class SynthesisParameter( + val type: Type, + val number: Int +) + + +class SynthesisMethodContext( + private val context: SynthesisUnitContext +) { + private var localCounter = 0 + private fun nextName() = "\$r${localCounter++}" + + private var parameterCount = 0 + private fun nextParameterCount() = parameterCount++ + + private val identities = mutableListOf() + private val parameters_ = mutableListOf() + private val stmts = mutableListOf() + private val unitToLocal_ = IdentityHashMap() + + val parameters: List by ::parameters_ + val returnType: Type = VoidType.v() + val body: JimpleBody + val unitToLocal: Map get() = unitToLocal_ + + val unitToParameter = IdentityHashMap() + + init { + for (model in context.models) { + val unit = context[model] + val local = synthesizeUnit(unit) + unitToLocal_[unit] = local + } + val returnStmt = returnVoidStatement() + + body = (identities + stmts + returnStmt).toGraphBody() + } + + fun method(name: String, declaringClass: SootClass): SootMethod { + val parameterTypes = parameters.map { it.type } + + return createSootMethod(name, parameterTypes, returnType, declaringClass, body, isStatic = true) + } + + fun resolve(parameterModels: List): List { + val resolver = Resolver(parameterModels, context, unitToParameter) + return context.models.map { resolver.resolve(context[it]) } + } + + private fun synthesizeUnit(unit: SynthesisUnit): JimpleLocal = when (unit) { + is ObjectUnit -> synthesizeCompositeUnit(unit) + is MethodUnit -> synthesizeMethodUnit(unit) + is NullUnit -> synthesizeNullUnit(unit) + is ElementContainingUnit -> synthesizeElementContainingUnit(unit) + is ReferenceToUnit -> synthesizeRefUnit(unit) + }.also { + unitToLocal_[unit] = it + } + + private fun synthesizeCompositeUnit(unit: SynthesisUnit): JimpleLocal { + val sootType = unit.classId.toSootType() + val parameterNumber = nextParameterCount() + val parameterRef = parameterRef(sootType, parameterNumber) + val local = JimpleLocal(nextName(), sootType) + val identity = identityStmt(local, parameterRef) + + identities += identity + val parameter = SynthesisParameter(sootType, parameterNumber) + parameters_ += parameter + unitToParameter[unit] = parameter + + return local + } + + private fun synthesizeMethodUnit(unit: MethodUnit): JimpleLocal { + val parameterLocals = unit.params.map { synthesizeUnit(it) } + val result = with(unit.method) { + when { + this is ConstructorId -> synthesizeConstructorInvoke(this, parameterLocals) + this is MethodId && isStatic -> synthesizeStaticInvoke(this, parameterLocals) + this is MethodId -> synthesizeVirtualInvoke(this, parameterLocals) + else -> error("Unexpected method unit in synthesizer: $unit") + } + } + return result + } + + private fun synthesizeNullUnit(unit: NullUnit): JimpleLocal { + val sootType = unit.classId.toSootType() + val local = JimpleLocal(nextName(), sootType) + stmts += assignStmt(local, NullConstant.v()) + return local + } + + private fun synthesizeRefUnit(unit: ReferenceToUnit): JimpleLocal { + val sootType = unit.classId.toSootType() + val ref = unitToLocal[context[unit.reference]]!! + val local = JimpleLocal(nextName(), sootType) + stmts += assignStmt(local, ref) + return local + } + + private fun synthesizeElementContainingUnit(unit: ElementContainingUnit): JimpleLocal { + val lengthLocal = synthesizeUnit(context[unit.length]) + val unitLocal = synthesizeCreateExpr(unit, lengthLocal) + for ((key, value) in unit.elements) { + val indexLocal = synthesizeUnit(context[key]) + val valueLocal = synthesizeUnit(context[value]) + + synthesizeSetExpr(unit, unitLocal, indexLocal, valueLocal) + } + return unitLocal + } + + private fun synthesizeCreateExpr(unit: ElementContainingUnit, lengthLocal: JimpleLocal): JimpleLocal = when (unit) { + is ArrayUnit -> { + val arrayType = unit.classId.toSootType() as ArrayType + val arrayLocal = JimpleLocal(nextName(), arrayType) + val arrayExpr = newArrayExpr(arrayType.elementType, lengthLocal) + stmts += assignStmt(arrayLocal, arrayExpr) + arrayLocal + } + + is ListUnit -> synthesizeConstructorInvoke(unit.constructorId, listOf()) + is SetUnit -> synthesizeConstructorInvoke(unit.constructorId, listOf()) + is MapUnit -> synthesizeConstructorInvoke(unit.constructorId, listOf()) + } + + private fun synthesizeSetExpr( + unit: ElementContainingUnit, + unitLocal: JimpleLocal, + key: JimpleLocal, + value: JimpleLocal + ): Any = when (unit) { + is ArrayUnit -> { + val arrayRef = newArrayRef(unitLocal, key) + stmts += assignStmt(arrayRef, value) + } + + is ListUnit -> synthesizeVirtualInvoke(unit.addId, listOf(unitLocal, value)) + + is SetUnit -> synthesizeVirtualInvoke(unit.addId, listOf(unitLocal, value)) + + is MapUnit -> synthesizeVirtualInvoke(unit.putId, listOf(unitLocal, key, value)) + } + + private fun synthesizeVirtualInvoke(method: MethodId, parameterLocals: List): JimpleLocal { + val local = parameterLocals.firstOrNull() ?: error("No this parameter found for $method") + val parametersWithoutThis = parameterLocals.drop(1) + + val sootMethod = method.classId.toSoot().methods.first { it.pureJavaSignature == method.signature } + val invokeStmt = when { + sootMethod.declaringClass.isInterface -> sootMethod.toInterfaceInvoke(local, parametersWithoutThis) + else -> sootMethod.toVirtualInvoke(local, parametersWithoutThis) + }.toInvokeStmt() + + stmts += invokeStmt + + return local + } + private fun synthesizeStaticInvoke(method: MethodId, parameterLocals: List): JimpleLocal { + val sootMethod = method.classId.toSoot().methods.first { it.pureJavaSignature == method.signature } + val invokeExpr = sootMethod.toStaticInvokeExpr(parameterLocals) + val invokeResult = JimpleLocal(nextName(), sootMethod.returnType) + + + stmts += assignStmt(invokeResult, invokeExpr) + + return invokeResult + } + + private fun synthesizeConstructorInvoke( + method: ConstructorId, + parameterLocals: List + ): JimpleLocal { + val sootType = method.classId.toSootType() as RefType + val local = JimpleLocal(nextName(), sootType) + val new = newExpr(sootType) + val assignStmt = assignStmt(local, new) + + stmts += assignStmt + + val sootMethod = method.classId.toSoot().methods.first { it.pureJavaSignature == method.signature } + val invokeStmt = sootMethod.toSpecialInvoke(local, parameterLocals).toInvokeStmt() + + stmts += invokeStmt + + return local + } +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/SynthesisUnit.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/SynthesisUnit.kt new file mode 100644 index 0000000000..203a2dc8cb --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/SynthesisUnit.kt @@ -0,0 +1,87 @@ +package org.utbot.framework.synthesis + +import org.utbot.framework.plugin.api.ClassId +import org.utbot.framework.plugin.api.ExecutableId +import org.utbot.framework.plugin.api.UtModel +import org.utbot.framework.plugin.api.util.objectClassId +import org.utbot.framework.plugin.api.util.primitives + +sealed class SynthesisUnit { + abstract val classId: ClassId +} + +data class ObjectUnit( + override val classId: ClassId +) : SynthesisUnit() { + fun isPrimitive() = classId in primitives +} + +sealed class ElementContainingUnit( + override val classId: ClassId, + open val elements: List>, + open val length: UtModel +) : SynthesisUnit() { + fun isPrimitive() = classId.elementClassId in primitives +} + +data class ArrayUnit( + override val classId: ClassId, + override val elements: List>, + override val length: UtModel +) : ElementContainingUnit(classId, elements, length) + +data class ListUnit( + override val classId: ClassId, + override val elements: List>, + override val length: UtModel +) : ElementContainingUnit(classId, elements, length) { + val constructorId get() = classId.allConstructors.first { it.parameters.isEmpty() } + val addId get() = classId.allMethods.first { + it.name == "add" && it.parameters == listOf(objectClassId) + } +} + +data class SetUnit( + override val classId: ClassId, + override val elements: List>, + override val length: UtModel +) : ElementContainingUnit(classId, elements, length) { + val constructorId get() = classId.allConstructors.first { it.parameters.isEmpty() } + val addId get() = classId.allMethods.first { + it.name == "add" && it.parameters == listOf(objectClassId) + } +} + +data class MapUnit( + override val classId: ClassId, + override val elements: List>, + override val length: UtModel +) : ElementContainingUnit(classId, elements, length) { + val constructorId get() = classId.allConstructors.first { it.parameters.isEmpty() } + val putId get() = classId.allMethods.first { + it.name == "put" && it.parameters == listOf(objectClassId, objectClassId) + } +} + +data class NullUnit( + override val classId: ClassId +) : SynthesisUnit() + +data class ReferenceToUnit( + override val classId: ClassId, + val reference: UtModel +) : SynthesisUnit() + +data class MethodUnit( + override val classId: ClassId, + val method: ExecutableId, + val params: List +) : SynthesisUnit() + +fun SynthesisUnit.isFullyDefined(): Boolean = when (this) { + is NullUnit -> true + is ReferenceToUnit -> true + is ObjectUnit -> isPrimitive() + is ElementContainingUnit -> true + is MethodUnit -> params.all { it.isFullyDefined() } +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/SynthesisUnitChecker.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/SynthesisUnitChecker.kt new file mode 100644 index 0000000000..99af7c18d4 --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/SynthesisUnitChecker.kt @@ -0,0 +1,48 @@ +package org.utbot.framework.synthesis + +import com.jetbrains.rd.util.AtomicInteger +import mu.KotlinLogging +import org.utbot.framework.PathSelectorType +import org.utbot.framework.UtSettings +import org.utbot.framework.plugin.api.MockStrategyApi +import org.utbot.framework.plugin.api.TestCaseGenerator +import org.utbot.framework.plugin.api.UtExecutionSuccess +import org.utbot.framework.plugin.api.UtModel +import org.utbot.framework.synthesis.postcondition.constructors.ConstraintBasedPostConditionConstructor +import soot.SootClass + +class SynthesisUnitChecker( + val testCaseGenerator: TestCaseGenerator, + val declaringClass: SootClass, +) { + companion object { + private val initializerMethodId = AtomicInteger() + } + + private val logger = KotlinLogging.logger("ConstrainedSynthesisUnitChecker") + + fun tryGenerate(synthesisUnitContext: SynthesisUnitContext, parameters: List): List? { + if (!synthesisUnitContext.isFullyDefined) return null + + val synthesisMethodContext = SynthesisMethodContext(synthesisUnitContext) + val method = synthesisMethodContext.method("\$initializer_${initializerMethodId.getAndIncrement()}", declaringClass) + + val execution = run { + val executions = testCaseGenerator.generateWithPostCondition( + method, + MockStrategyApi.NO_MOCKS, + ConstraintBasedPostConditionConstructor( + parameters, + synthesisUnitContext, + synthesisMethodContext + ) + ) + executions.firstOrNull { it.result is UtExecutionSuccess } + } ?: return null + + logger.debug { "Constructed method" } + logger.debug { method.activeBody } + + return synthesisMethodContext.resolve(listOfNotNull(execution.stateBefore.thisInstance) + execution.stateBefore.parameters) + } +} 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 new file mode 100644 index 0000000000..0d0332edf9 --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/Synthesizer.kt @@ -0,0 +1,379 @@ +package org.utbot.framework.synthesis + +import mu.KotlinLogging +import org.utbot.framework.UtSettings.enableSynthesisCache +import org.utbot.framework.UtSettings.synthesisMaxDepth +import org.utbot.framework.UtSettings.synthesisTimeoutInMillis +import org.utbot.framework.modifications.StatementsStorage +import org.utbot.framework.plugin.api.* +import org.utbot.framework.plugin.api.util.isArray +import org.utbot.framework.plugin.api.util.isPrimitive +import org.utbot.framework.plugin.api.util.objectClassId +import org.utbot.framework.synthesis.postcondition.constructors.ConstraintBasedPostConditionException + +internal fun Collection.expandable() = filter { !it.isArray && !it.isPrimitive }.toSet() + +private object SynthesisCache { + private val successfulInitializers = + mutableMapOf, MutableList>>() + + operator fun get(utMethod: ExecutableId, parameters: List): List = + successfulInitializers.getOrPut(utMethod, ::mutableMapOf).getOrPut(parameters, ::mutableListOf) + + operator fun set(utMethod: ExecutableId, parameters: List, synthesisUnitContext: SynthesisUnitContext) = + successfulInitializers.getOrPut(utMethod, ::mutableMapOf).getOrPut(parameters, ::mutableListOf) + .add(synthesisUnitContext) +} + +class Synthesizer( + val testCaseGenerator: TestCaseGenerator, + val method: ExecutableId, + val parameters: List, + val depth: Int = synthesisMaxDepth +) { + companion object { + private val logger = KotlinLogging.logger("ConstrainedSynthesizer") + private var attempts = 0 + private var successes = 0 + private var cacheHits = 0 + + val successRate: Double + get() = when (attempts) { + 0 -> 0.0 + else -> successes.toDouble() / attempts + } + + fun cleanStats() { + attempts = 0 + successes = 0 + cacheHits = 0 + } + + + private fun stats(): String = buildString { + appendLine("Synthesizer stats:") + appendLine("Total attempts - $attempts") + appendLine("Successful attempts - $successes") + appendLine("Cache hits - $cacheHits") + appendLine("Success rate - ${String.format("%.2f", 100.0 * successRate)}") + } + + private fun success() { + ++attempts + ++successes + logger.debug { stats() } + } + + private fun failure() { + ++attempts + logger.debug { stats() } + } + } + + private val parametersMap = parameters.withIndex().associate { it.value to it.index } + private val logger = KotlinLogging.logger("ConstrainedSynthesizer") + private val statementStorage = StatementsStorage().also { storage -> + storage.update(parameters.map { it.classId }.expandable()) + } + + private val unitChecker = SynthesisUnitChecker(testCaseGenerator, objectClassId.toSoot()) + + private fun splitModels(): Set> { + val result = parameters.map { mutableSetOf(it) }.toMutableSet() + while (true) { + var changed = false + loopExit@ for (current in result) { + for (next in result) { + if (current == next) continue + + for (currentModel in current.filterIsInstance()) { + for (nextModel in next.filterIsInstance()) { + if (nextModel.utConstraints.any { currentModel.variable in it }) { + result.remove(next) + current.addAll(next) + changed = true + break@loopExit + } + } + } + } + } + if (!changed) break + } + return result.map { models -> models.sortedBy { parametersMap[it] } }.toSet() + } + + fun synthesize( + timeLimit: Long = synthesisTimeoutInMillis, + enableCache: Boolean = enableSynthesisCache + ): List { + val modelSubsets = splitModels() + val startTime = System.currentTimeMillis() + val timeLimitExceeded = { System.currentTimeMillis() - startTime > timeLimit } + + val result = MutableList(parameters.size) { null } + for (models in modelSubsets) { + val modelIndices = models.map { parametersMap[it]!! } + var found = false + + if (enableCache) { + for (cachedUnitContext in SynthesisCache[method, modelIndices]) { + if (timeLimitExceeded()) break + + val assembleModel = try { + val mappedUnitContext = cachedUnitContext.copyWithNewModelsOrNull(models) ?: continue + unitChecker.tryGenerate(mappedUnitContext, models) + } catch (e: ConstraintBasedPostConditionException) { + logger.warn { "Error during assemble model generation from cached unit context" } + null + } + if (assembleModel != null) { + logger.debug { "Found $assembleModel" } + cacheHits++ + found = true + break + } + } + } + + val queueIterator = SynthesisUnitContextQueue(models, statementStorage, depth) + while ( + queueIterator.hasNext() && + !timeLimitExceeded() && + !found + ) { + val unitContext = queueIterator.next() + if (!unitContext.isFullyDefined) continue + + val assembleModel = try { + unitChecker.tryGenerate(unitContext, models) + } catch (e: Throwable) { + logger.error { "Error during assemble model generation" } + logger.error(e.message) + logger.error(e.stackTraceToString()) + null + } + + if (assembleModel != null) { + logger.debug { "Found $assembleModel" } + for ((index, assemble) in modelIndices.zip(assembleModel)) { + result[index] = assemble + } + SynthesisCache[method, modelIndices] = unitContext + found = true + } + } + + when { + found -> success() + else -> failure() + } + } + return result + } +} + +class SynthesisUnitContext( + val models: List, + initialMap: Map = emptyMap() +) { + private val mapping = initialMap.toMutableMap() + + val isFullyDefined get() = models.all { it.synthesisUnit.isFullyDefined() } + + init { + models.forEach { it.synthesisUnit } + } + + val UtModel.synthesisUnit: SynthesisUnit + get() = mapping.getOrPut(this) { + when (this) { + is UtNullModel -> NullUnit(this.classId) + is UtPrimitiveConstraintModel -> ObjectUnit(this.classId) + is UtReferenceConstraintModel -> ObjectUnit(this.classId) + is UtArrayConstraintModel -> ArrayUnit( + this.classId, + this.elements.toList(), + this.length + ) + + is UtListConstraintModel -> ListUnit( + this.classId, + this.elements.toList(), + this.length + ) + + is UtSetConstraintModel -> SetUnit( + this.classId, + this.elements.toList(), + this.length + ) + + is UtMapConstraintModel -> MapUnit( + this.classId, + this.elements.toList(), + this.length + ) + + is UtReferenceToConstraintModel -> ReferenceToUnit(this.classId, this.reference) + else -> error("Only UtSynthesisModel supported") + } + } + + operator fun get(utModel: UtModel): SynthesisUnit = mapping[utModel] + ?: utModel.synthesisUnit + + fun set(model: UtModel, newUnit: SynthesisUnit): SynthesisUnitContext { + val newMapping = mapping.toMutableMap() + newMapping[model] = newUnit + return SynthesisUnitContext(models, newMapping) + } + + private fun SynthesisUnit.isFullyDefined(): Boolean = when (this) { + is NullUnit -> true + is ReferenceToUnit -> true + is ObjectUnit -> isPrimitive() + is ElementContainingUnit -> elements.all { + this@SynthesisUnitContext[it.first].isFullyDefined() && this@SynthesisUnitContext[it.second].isFullyDefined() + } + + is MethodUnit -> params.all { it.isFullyDefined() } + } + + fun copyWithNewModelsOrNull(newModels: List): SynthesisUnitContext? { + // if current context contains some internal models -- we cannot copy it + if (mapping.size != models.size) return null + + val modelMapping = models.zip(newModels).toMap() + + // if we have non-null model matched to a null unit (or vice-versa) -- we don't need to create a copy + if (modelMapping.any { + (it.value is UtNullModel && mapping[it.key] !is NullUnit) + || (it.key is UtNullModel && mapping[it.value] !is NullUnit) + }) return null + + return SynthesisUnitContext(newModels, mapping.mapKeys { + modelMapping[it.key] ?: return null + }) + } +} + +class SynthesisUnitContextQueue( + val models: List, + statementsStorage: StatementsStorage, + val depth: Int +) : Iterator { + private val leafExpander = CompositeUnitExpander(statementsStorage) + val queue = ArrayDeque().also { + it.addLast(SynthesisUnitContext(models)) + } + + override fun hasNext(): Boolean { + return queue.isNotEmpty() + } + + override fun next(): SynthesisUnitContext { + val result = queue.removeFirst() + queue.addAll(produceNext(result)) + return result + } + + private fun produceNext(context: SynthesisUnitContext): List { + var index = 0 + var currentContext = context + while (true) { + with(currentContext) { + if (index >= models.size) { + return emptyList() + } + + val currentModel = models[index] + val newContexts = produce(currentContext, currentModel) + if (newContexts.isEmpty()) { + currentContext = currentContext.set(currentModel, currentModel.synthesisUnit) + index++ + } else { + return newContexts + } + } + } + } + + private fun produce( + context: SynthesisUnitContext, + model: UtModel + ): List = when (val unit = context[model]) { + is NullUnit -> emptyList() + is ReferenceToUnit -> emptyList() + is MethodUnit -> produce(unit).map { + context.set(model, it) + } + + is ObjectUnit -> produce(unit).map { + context.set(model, it) + } + + is ElementContainingUnit -> when { + unit.isPrimitive() -> emptyList() + else -> { + var currentContext = context + var result = emptyList() + var index = 0 + + while (true) { + model as UtElementContainerConstraintModel + if (index >= unit.elements.size) break + + val currentKeyModel = unit.elements[index].first + val currentValueModel = unit.elements[index].second + + val newKeyLeafs = produce(context, currentKeyModel) + if (newKeyLeafs.isEmpty()) { + val newValueLeafs = produce(context, currentValueModel) + if (newValueLeafs.isEmpty()) { + for (i in 0..index) { + currentContext = currentContext.set(currentKeyModel, currentContext[currentValueModel]) + currentContext = + currentContext.set(currentValueModel, currentContext[currentValueModel]) + } + index++ + } else { + result = newValueLeafs + break + } + } else { + result = newKeyLeafs + break + } + } + result + } + } + } + + private fun produce(state: SynthesisUnit): List = + when (state) { + is MethodUnit -> state.params.run { + flatMapIndexed { idx, leaf -> + val newLeafs = produce(leaf) + newLeafs.map { newLeaf -> + val newParams = toMutableList() + newParams[idx] = newLeaf + state.copy(params = newParams) + } + } + } + + is ObjectUnit -> { + val leafs = leafExpander.expand(state) + when { + state.isPrimitive() -> leafs + else -> listOf(NullUnit(state.classId)) + leafs + } + } + + is NullUnit -> emptyList() + is ReferenceToUnit -> emptyList() + is ElementContainingUnit -> emptyList() + } +} diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/postcondition/constructors/ConstraintBasedPostConditionConstructor.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/postcondition/constructors/ConstraintBasedPostConditionConstructor.kt new file mode 100644 index 0000000000..2568add4b8 --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/postcondition/constructors/ConstraintBasedPostConditionConstructor.kt @@ -0,0 +1,461 @@ +package org.utbot.framework.synthesis.postcondition.constructors + +import org.utbot.engine.* +import org.utbot.engine.pc.* +import org.utbot.engine.selectors.strategies.ConstraintScoringStrategyBuilder +import org.utbot.engine.selectors.strategies.ScoringStrategyBuilder +import org.utbot.engine.symbolic.SymbolicStateUpdate +import org.utbot.engine.symbolic.asHardConstraint +import org.utbot.engine.symbolic.asSoftConstraint +import org.utbot.framework.plugin.api.* +import org.utbot.framework.plugin.api.UtConstraintParameter +import org.utbot.framework.plugin.api.util.* +import org.utbot.framework.synthesis.SynthesisMethodContext +import org.utbot.framework.synthesis.SynthesisUnitContext +import org.utbot.framework.synthesis.toSoot +import org.utbot.framework.synthesis.toSootType +import soot.ArrayType +import soot.RefType + + +class ConstraintBasedPostConditionException(msg: String) : Exception(msg) + +class ConstraintBasedPostConditionConstructor( + private val models: List, + private val unitContext: SynthesisUnitContext, + private val methodContext: SynthesisMethodContext +) : PostConditionConstructor { + + override fun constructPostCondition( + traverser: Traverser, + symbolicResult: SymbolicResult? + ): SymbolicStateUpdate = UtConstraint2ExpressionConverter(traverser).run { + var constraints = SymbolicStateUpdate() + val entryFrame = traverser.environment.state.executionStack.first() + val frameParameters = entryFrame.parameters.map { it.value } + for (model in models) { + constraints += buildPostCondition( + model, + this, + frameParameters, + traverser.environment.state.localVariableMemory + ).asHardConstraint() + } + constraints + } + + override fun constructSoftPostCondition( + traverser: Traverser, + ): SymbolicStateUpdate = UtConstraint2ExpressionConverter( + traverser + ).run { + var constraints = SymbolicStateUpdate() + if (traverser.isInitialized) { + val entryFrame = traverser.environment.state.executionStack.first() + val frameParameters = entryFrame.parameters.map { it.value } + for (model in models) { + constraints += buildPostCondition( + model, + this, + frameParameters, + traverser.environment.state.localVariableMemory + ).asSoftConstraint() + } + } + constraints + } + + override fun scoringBuilder(): ScoringStrategyBuilder { + return ConstraintScoringStrategyBuilder( + models, + unitContext, + methodContext, + this + ) + } + + private fun buildPostCondition( + model: UtModel, + builder: UtConstraint2ExpressionConverter, + parameters: List, + localVariableMemory: LocalVariableMemory, + ): Set = buildSet { + val modelUnit = unitContext[model] + val symbolicValue = when { + model.classId.isPrimitive -> methodContext.unitToParameter[modelUnit]?.let { parameters[it.number] } + ?: throw ConstraintBasedPostConditionException("$modelUnit does not map to any parameter") + else -> localVariableMemory.local(methodContext.unitToLocal[modelUnit]!!.variable) + ?: return@buildSet + } + when (model) { + is UtNullModel -> { + add(mkEq(symbolicValue.addr, nullObjectAddr)) + } + + is UtConstraintModel -> { + if (model is UtElementContainerConstraintModel) { + addAll(buildPostCondition(model.length, builder, parameters, localVariableMemory)) + for ((index, element) in model.elements) { + addAll(buildPostCondition(index, builder, parameters, localVariableMemory)) + addAll(buildPostCondition(element, builder, parameters, localVariableMemory)) + } + } + for (constraint in model.utConstraints) { + add(constraint.accept(builder)) + } + add(mkEq(symbolicValue, model.variable.accept(builder))) + } + + else -> error("Unknown model: ${model::class}") + } + } +} + +class UtConstraint2ExpressionConverter( + private val traverser: Traverser +) : UtConstraintVisitor, UtConstraintVariableVisitor { + override fun visitUtConstraintParameter(expr: UtConstraintParameter): SymbolicValue = with(expr) { + when { + isPrimitive -> { + val newName = "post_condition_$name" + when (classId) { + voidClassId -> voidValue + booleanClassId -> mkBoolConst(newName).toBoolValue() + byteClassId -> mkBVConst(newName, UtByteSort).toByteValue() + shortClassId -> mkBVConst(newName, UtShortSort).toShortValue() + charClassId -> mkBVConst(newName, UtCharSort).toCharValue() + intClassId -> mkBVConst(newName, UtIntSort).toIntValue() + longClassId -> mkBVConst(newName, UtLongSort).toLongValue() + floatClassId -> mkFpConst(newName, Float.SIZE_BITS).toFloatValue() + doubleClassId -> mkFpConst(newName, Double.SIZE_BITS).toDoubleValue() + else -> error("Unknown primitive parameter: $this") + } + } + + isArray -> { + val sootType = classId.toSootType() as ArrayType + val addr = UtAddrExpression(mkBVConst("post_condition_${name}", UtIntSort)) + traverser.createArray(addr, sootType, useConcreteType = addr.isThisAddr) + } + + else -> { + val sootType = classId.toSoot().type + val addr = UtAddrExpression(mkBVConst("post_condition_${name}", UtIntSort)) + traverser.createObject(addr, sootType, useConcreteType = addr.isThisAddr) + } + } + } + + override fun visitUtConstraintNull(expr: UtConstraintNull): SymbolicValue = with(expr) { + when { + classId.isArray -> traverser.createArray(nullObjectAddr, classId.toSootType() as ArrayType) + else -> traverser.createObject( + nullObjectAddr, + classId.toSoot().type, + mockInfoGenerator = null, + useConcreteType = false + ) + } + } + + override fun visitUtConstraintFieldAccess(expr: UtConstraintFieldAccess): SymbolicValue = with(expr) { + val sootField = fieldId.declaringClass.toSoot().getFieldByName(fieldId.name) + val type = sootField.declaringClass.type + val instanceVal = instance.accept(this@UtConstraint2ExpressionConverter) + try { + traverser.createFieldOrMock( + type, + instanceVal.addr, + sootField, + mockInfoGenerator = null + ) + } catch (e: Throwable) { + throw e + } + } + + override fun visitUtConstraintArrayAccess(expr: UtConstraintArrayAccess): SymbolicValue = with(expr) { + val arrayInstance = instance.accept(this@UtConstraint2ExpressionConverter) + val index = index.accept(this@UtConstraint2ExpressionConverter) + val type = instance.classId.toSootType() as? ArrayType ?: ArrayType.v(OBJECT_TYPE.sootClass.type, 1) + val elementType = type.elementType + val chunkId = traverser.typeRegistry.arrayChunkId(type) + val descriptor = MemoryChunkDescriptor(chunkId, type, elementType).also { traverser.touchMemoryChunk(it) } + val array = traverser.memory.findArray(descriptor) + + when (elementType) { + is RefType -> { + val generator = UtMockInfoGenerator { mockAddr -> UtObjectMockInfo(elementType.id, mockAddr) } + + val objectValue = traverser.createObject( + UtAddrExpression(array.select(arrayInstance.addr, index.exprValue)), + elementType, + useConcreteType = false, + generator + ) + + if (objectValue.type.isJavaLangObject()) { + traverser.queuedSymbolicStateUpdates += traverser.typeRegistry.zeroDimensionConstraint(objectValue.addr) + .asSoftConstraint() + } + + objectValue + } + + is ArrayType -> traverser.createArray( + UtAddrExpression(array.select(arrayInstance.addr, index.exprValue)), + elementType, + useConcreteType = false + ) + + else -> PrimitiveValue(elementType, array.select(arrayInstance.addr, index.exprValue)) + } + } + + override fun visitUtConstraintArrayLengthAccess(expr: UtConstraintArrayLength): SymbolicValue = with(expr) { + val array = instance.accept(this@UtConstraint2ExpressionConverter) + traverser.memory.findArrayLength(array.addr) + } + + override fun visitUtConstraintBoolConstant(expr: UtConstraintBoolConstant): SymbolicValue = + expr.value.toPrimitiveValue() + + override fun visitUtConstraintCharConstant(expr: UtConstraintCharConstant): SymbolicValue = + expr.value.toPrimitiveValue() + + override fun visitUtConstraintNumericConstant(expr: UtConstraintNumericConstant): SymbolicValue = + expr.value.primitiveToSymbolic() + + override fun visitUtConstraintAdd(expr: UtConstraintAdd): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + Add(elhv, erhv) + ) + } + + override fun visitUtConstraintAnd(expr: UtConstraintAnd): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + And(elhv, erhv) + ) + } + + override fun visitUtConstraintCmp(expr: UtConstraintCmp): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + Cmp(elhv, erhv) + ) + } + + override fun visitUtConstraintCmpg(expr: UtConstraintCmpg): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + Cmpg(elhv, erhv) + ) + } + + override fun visitUtConstraintCmpl(expr: UtConstraintCmpl): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + Cmpl(elhv, erhv) + ) + } + + override fun visitUtConstraintDiv(expr: UtConstraintDiv): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + Div(elhv, erhv) + ) + } + + override fun visitUtConstraintMul(expr: UtConstraintMul): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + Mul(elhv, erhv) + ) + } + + override fun visitUtConstraintOr(expr: UtConstraintOr): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + Or(elhv, erhv) + ) + } + + override fun visitUtConstraintRem(expr: UtConstraintRem): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + Rem(elhv, erhv) + ) + } + + override fun visitUtConstraintShl(expr: UtConstraintShl): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + Shl(elhv, erhv) + ) + } + + override fun visitUtConstraintShr(expr: UtConstraintShr): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + Shr(elhv, erhv) + ) + } + + override fun visitUtConstraintSub(expr: UtConstraintSub): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + Sub(elhv, erhv) + ) + } + + override fun visitUtConstraintUshr(expr: UtConstraintUshr): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + Ushr(elhv, erhv) + ) + } + + override fun visitUtConstraintXor(expr: UtConstraintXor): SymbolicValue = with(expr) { + val elhv = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val erhv = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + classId.toSootType(), + Xor(elhv, erhv) + ) + } + + override fun visitUtConstraintNot(expr: UtConstraintNot): SymbolicValue = with(expr) { + val oper = operand.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue(oper.type, mkNot(oper.expr as UtBoolExpression)) + } + + override fun visitUtConstraintNeg(expr: UtConstraintNeg): SymbolicValue = with(expr) { + val oper = operand.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + PrimitiveValue( + oper.type, UtNegExpression(oper) + ) + } + + override fun visitUtConstraintCast(expr: UtConstraintCast): SymbolicValue = with(expr) { + val oper = operand.accept(this@UtConstraint2ExpressionConverter) as? PrimitiveValue + ?: error("a") + PrimitiveValue( + oper.type, UtCastExpression(oper, classId.toSootType()) + ) + } + + override fun visitUtNegatedConstraint(expr: UtNegatedConstraint): UtBoolExpression = with(expr) { + mkNot(constraint.accept(this@UtConstraint2ExpressionConverter)) + } + + override fun visitUtRefEqConstraint(expr: UtRefEqConstraint): UtBoolExpression = with(expr) { + val lhvVal = lhv.accept(this@UtConstraint2ExpressionConverter) + val rhvVal = rhv.accept(this@UtConstraint2ExpressionConverter) + mkEq(lhvVal, rhvVal) + } + + override fun visitUtRefGenericEqConstraint(expr: UtRefGenericEqConstraint) = with(expr) { + val lhvVal = lhv.accept(this@UtConstraint2ExpressionConverter) + val rhvVal = rhv.accept(this@UtConstraint2ExpressionConverter) + UtEqGenericTypeParametersExpression(lhvVal.addr, rhvVal.addr, mapping) + } + + override fun visitUtRefTypeConstraint(expr: UtRefTypeConstraint): UtBoolExpression = with(expr) { + val lhvVal = operand.accept(this@UtConstraint2ExpressionConverter) + val type = type.toSootType() + traverser.typeRegistry + .typeConstraint( + lhvVal.addr, + traverser.typeResolver.constructTypeStorage(type, false) + ) + .isConstraint() + } + + override fun visitUtRefGenericTypeConstraint(expr: UtRefGenericTypeConstraint): UtBoolExpression = with(expr) { + val operandVal = operand.accept(this@UtConstraint2ExpressionConverter) + val baseVal = base.accept(this@UtConstraint2ExpressionConverter) + UtIsGenericTypeExpression(operandVal.addr, baseVal.addr, parameterIndex) + } + + override fun visitUtBoolConstraint(expr: UtBoolConstraint): UtBoolExpression = + when (val bool = expr.operand.accept(this@UtConstraint2ExpressionConverter).exprValue) { + is UtBoolExpression -> bool + is UtArraySelectExpression -> UtEqExpression(bool, UtTrue) + else -> throw NotSupportedByConstraintResolverException() + } + + override fun visitUtEqConstraint(expr: UtEqConstraint): UtBoolExpression = with(expr) { + val lhvVal = lhv.accept(this@UtConstraint2ExpressionConverter) + val rhvVal = rhv.accept(this@UtConstraint2ExpressionConverter) + mkEq(lhvVal, rhvVal) + } + + override fun visitUtLtConstraint(expr: UtLtConstraint): UtBoolExpression = with(expr) { + val lhvVal = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val rhvVal = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + Lt(lhvVal, rhvVal) + } + + override fun visitUtGtConstraint(expr: UtGtConstraint): UtBoolExpression = with(expr) { + val lhvVal = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val rhvVal = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + Gt(lhvVal, rhvVal) + } + + override fun visitUtLeConstraint(expr: UtLeConstraint): UtBoolExpression = with(expr) { + val lhvVal = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val rhvVal = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + Le(lhvVal, rhvVal) + } + + override fun visitUtGeConstraint(expr: UtGeConstraint): UtBoolExpression = with(expr) { + val lhvVal = lhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + val rhvVal = rhv.accept(this@UtConstraint2ExpressionConverter) as PrimitiveValue + Ge(lhvVal, rhvVal) + } + + override fun visitUtAndConstraint(expr: UtAndConstraint): UtBoolExpression = mkAnd( + expr.lhv.accept(this), + expr.rhv.accept(this) + ) + + override fun visitUtOrConstraint(expr: UtOrConstraint): UtBoolExpression = mkOr( + expr.lhv.accept(this), + expr.rhv.accept(this) + ) + + private val SymbolicValue.exprValue + get() = when (this) { + is ReferenceValue -> addr + is PrimitiveValue -> expr + } +} + diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/postcondition/constructors/PostConditionConstructor.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/postcondition/constructors/PostConditionConstructor.kt new file mode 100644 index 0000000000..0fc6dcd83f --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/synthesis/postcondition/constructors/PostConditionConstructor.kt @@ -0,0 +1,34 @@ +package org.utbot.framework.synthesis.postcondition.constructors + +import org.utbot.engine.* +import org.utbot.engine.selectors.strategies.ScoringStrategyBuilder +import org.utbot.engine.selectors.strategies.defaultScoringStrategy +import org.utbot.engine.symbolic.SymbolicState +import org.utbot.engine.symbolic.SymbolicStateUpdate + +interface PostConditionConstructor { + fun constructPostCondition( + traverser: Traverser, + symbolicResult: SymbolicResult? + ): SymbolicStateUpdate + + fun constructSoftPostCondition( + traverser: Traverser, + ): SymbolicStateUpdate + + fun scoringBuilder(): ScoringStrategyBuilder +} + +internal object EmptyPostCondition : PostConditionConstructor { + override fun constructPostCondition( + traverser: Traverser, + symbolicResult: SymbolicResult? + ): SymbolicStateUpdate = SymbolicStateUpdate() + + override fun constructSoftPostCondition( + traverser: Traverser, + ): SymbolicStateUpdate = SymbolicStateUpdate() + + override fun scoringBuilder(): ScoringStrategyBuilder = defaultScoringStrategy +} + diff --git a/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/TestSpecificTestCaseGenerator.kt b/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/TestSpecificTestCaseGenerator.kt index 0b2c9d87dd..0c77b6c7b7 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/TestSpecificTestCaseGenerator.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/TestSpecificTestCaseGenerator.kt @@ -6,6 +6,7 @@ import org.utbot.common.runBlockingWithCancellationPredicate import org.utbot.common.runIgnoringCancellationException import org.utbot.engine.EngineController import org.utbot.engine.Mocker +import org.utbot.engine.SymbolicEngineTarget import org.utbot.engine.UtBotSymbolicEngine import org.utbot.engine.util.mockListeners.ForceMockListener import org.utbot.engine.util.mockListeners.ForceStaticMockListener @@ -19,6 +20,7 @@ import org.utbot.framework.plugin.api.UtExecution import org.utbot.framework.plugin.api.UtMethodTestSet import org.utbot.framework.plugin.api.util.id import org.utbot.framework.plugin.services.JdkInfoDefaultProvider +import org.utbot.framework.synthesis.postcondition.constructors.EmptyPostCondition import org.utbot.framework.util.jimpleBody import java.nio.file.Path @@ -70,14 +72,20 @@ class TestSpecificTestCaseGenerator( runBlockingWithCancellationPredicate(isCanceled) { val controller = EngineController() controller.job = launch { - super - .generateAsync(controller, method, mockStrategy, mockAlwaysDefaults, defaultTimeEstimator) - .collect { - when (it) { - is UtExecution -> executions += it - is UtError -> errors.merge(it.description, 1, Int::plus) - } + super.generateAsync( + controller, + SymbolicEngineTarget.from(method), + mockStrategy, + mockAlwaysDefaults, + defaultTimeEstimator, + UtSettings.enableSynthesis, + EmptyPostCondition + ).collect { + when (it) { + is UtExecution -> executions += it + is UtError -> errors.merge(it.description, 1, Int::plus) } + } } } } @@ -85,7 +93,7 @@ class TestSpecificTestCaseGenerator( forceMockListener?.detach(this, forceMockListener) forceStaticMockListener?.detach(this, forceStaticMockListener) - val minimizedExecutions = super.minimizeExecutions(executions) + val minimizedExecutions = super.minimizeExecutions(executions.toAssemble(method)) return UtMethodTestSet(method, minimizedExecutions, jimpleBody(method), errors) } -} \ No newline at end of file +} diff --git a/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/UtModelTestCaseChecker.kt b/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/UtModelTestCaseChecker.kt index a33b5b980b..7286a3c59c 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/UtModelTestCaseChecker.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/UtModelTestCaseChecker.kt @@ -37,6 +37,7 @@ import org.utbot.testcheckers.ExecutionsNumberMatcher import java.nio.file.Path import kotlin.reflect.KClass import kotlin.reflect.KFunction +import kotlin.reflect.KFunction0 import kotlin.reflect.KFunction1 import kotlin.reflect.KFunction2 import kotlin.reflect.KFunction3 @@ -80,6 +81,16 @@ abstract class UtModelTestCaseChecker( arguments = ::withStaticsAfter ) + protected fun checkThis( + method: KFunction1<*, *>, + branches: ExecutionsNumberMatcher, + vararg matchers: (UtModel, UtExecutionResult) -> Boolean, + mockStrategy: MockStrategyApi = NO_MOCKS + ) = internalCheck( + method, mockStrategy, branches, matchers, + arguments = ::withThisAndResult + ) + private fun internalCheck( method: KFunction<*>, mockStrategy: MockStrategyApi, @@ -200,6 +211,7 @@ abstract class UtModelTestCaseChecker( } } +private fun withThisAndResult(ex: UtExecution) = listOf(ex.stateBefore.thisInstance) + ex.stateBefore.parameters + ex.result private fun withResult(ex: UtExecution) = ex.stateBefore.parameters + ex.result private fun withStaticsAfter(ex: UtExecution) = ex.stateBefore.parameters + ex.stateAfter.statics + ex.result diff --git a/utbot-junit-contest/src/main/kotlin/org/utbot/contest/Contest.kt b/utbot-junit-contest/src/main/kotlin/org/utbot/contest/Contest.kt index 2f5a27cfd2..d1e8e27274 100644 --- a/utbot-junit-contest/src/main/kotlin/org/utbot/contest/Contest.kt +++ b/utbot-junit-contest/src/main/kotlin/org/utbot/contest/Contest.kt @@ -60,6 +60,7 @@ import kotlinx.coroutines.newSingleThreadContext import kotlinx.coroutines.runBlocking import kotlinx.coroutines.withTimeoutOrNull import kotlinx.coroutines.yield +import org.utbot.engine.SymbolicEngineTarget internal const val junitVersion = 4 private val logger = KotlinLogging.logger {} @@ -306,7 +307,7 @@ fun runGeneration( } - testCaseGenerator.generateAsync(controller, method, mockStrategyApi) + testCaseGenerator.generateAsync(controller, SymbolicEngineTarget.Companion.from(method), mockStrategyApi) .collect { result -> when (result) { is UtExecution -> { diff --git a/utbot-sample/src/main/java/org/utbot/examples/synthesis/ComplexCounter.java b/utbot-sample/src/main/java/org/utbot/examples/synthesis/ComplexCounter.java new file mode 100644 index 0000000000..90f9bfe871 --- /dev/null +++ b/utbot-sample/src/main/java/org/utbot/examples/synthesis/ComplexCounter.java @@ -0,0 +1,37 @@ +package org.utbot.examples.synthesis; + +public class ComplexCounter { + private int a; + private int b; + + public ComplexCounter() { + this.a = 0; + this.b = 0; + } + + public int getA() { + return a; + } + + public int getB() { + return b; + } + + public void incrementA(int value) { + if (value < 0) return; + for (int i = 0; i < value; ++i) { + this.a++; + } + } + + public void incrementB(int value) { + if (value > 0) { + this.b += value; + } + } + + @Override + public String toString() { + return "C"; + } +} diff --git a/utbot-sample/src/main/java/org/utbot/examples/synthesis/ComplexObject.java b/utbot-sample/src/main/java/org/utbot/examples/synthesis/ComplexObject.java new file mode 100644 index 0000000000..9789fe0561 --- /dev/null +++ b/utbot-sample/src/main/java/org/utbot/examples/synthesis/ComplexObject.java @@ -0,0 +1,13 @@ +package org.utbot.examples.synthesis; + +public class ComplexObject { + public ComplexObject(Point a) { + this.a = a; + } + + public Point getA() { + return a; + } + + private Point a; +} diff --git a/utbot-sample/src/main/java/org/utbot/examples/synthesis/DeepComplexObject.java b/utbot-sample/src/main/java/org/utbot/examples/synthesis/DeepComplexObject.java new file mode 100644 index 0000000000..0498df8acc --- /dev/null +++ b/utbot-sample/src/main/java/org/utbot/examples/synthesis/DeepComplexObject.java @@ -0,0 +1,17 @@ +package org.utbot.examples.synthesis; + +public class DeepComplexObject { + public DeepComplexObject(ComplexObject o) { + this.o = o; + } + + private ComplexObject o; + + public ComplexObject getO() { + return o; + } + + public void setO() { + o = null; + } +} \ No newline at end of file diff --git a/utbot-sample/src/main/java/org/utbot/examples/synthesis/Point.java b/utbot-sample/src/main/java/org/utbot/examples/synthesis/Point.java new file mode 100644 index 0000000000..472575e278 --- /dev/null +++ b/utbot-sample/src/main/java/org/utbot/examples/synthesis/Point.java @@ -0,0 +1,36 @@ +package org.utbot.examples.synthesis; + +import java.util.Objects; + +public class Point implements SynthesisInterface { + + private int x; + private int y; + + public Point(int area) { + this.x = area / 10; + this.y = area - 10; + } + + @Override + public int getX() { + return x; + } + + public int getY() { + return y; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (!(o instanceof Point)) return false; + Point point = (Point) o; + return x == point.x && y == point.y; + } + + @Override + public int hashCode() { + return Objects.hash(x, y); + } +} \ No newline at end of file diff --git a/utbot-sample/src/main/java/org/utbot/examples/synthesis/SimpleList.java b/utbot-sample/src/main/java/org/utbot/examples/synthesis/SimpleList.java new file mode 100644 index 0000000000..f459578dff --- /dev/null +++ b/utbot-sample/src/main/java/org/utbot/examples/synthesis/SimpleList.java @@ -0,0 +1,24 @@ +package org.utbot.examples.synthesis; + +public class SimpleList { + private Point[] points = new Point[10]; + private int size = 0; + + public Point get(int index) { + if (index >= size) throw new IndexOutOfBoundsException(); + return points[index]; + } + + public void add(Point p) { + if (points.length <= size) { + Point[] newArr = new Point[points.length * 2]; + System.arraycopy(newArr, 0, points, 0, points.length); + points = newArr; + } + points[size++] = p; + } + + public int size() { + return size; + } +} diff --git a/utbot-sample/src/main/java/org/utbot/examples/synthesis/SynthesisExamples.java b/utbot-sample/src/main/java/org/utbot/examples/synthesis/SynthesisExamples.java new file mode 100644 index 0000000000..1ce9528478 --- /dev/null +++ b/utbot-sample/src/main/java/org/utbot/examples/synthesis/SynthesisExamples.java @@ -0,0 +1,139 @@ +package org.utbot.examples.synthesis; + +import java.util.*; + +public class SynthesisExamples { + public void synthesizePoint(Point p) { + if (p.getX() > 125) { + if (p.getY() < 100000) { + throw new IllegalArgumentException(); + } + } + } + + public void synthesizeInterface(SynthesisInterface i) { + if (i.getX() == 10) { + throw new IllegalArgumentException(); + } + } + + public void synthesizeList(List points) { + if (points.get(0).getX() >= 14) { + throw new IllegalArgumentException(); + } + } + + public void synthesizeSet(Set points) { + for (Point p : points) { + if (p.getX() >= 14) { + throw new IllegalArgumentException(); + } + } + } + + public void synthesizeList2(int length, int index, int value) { + ArrayList p = new ArrayList<>(Arrays.asList(new Point[length])); + p.set(index, new Point(value)); + synthesizeList(p); + } + + public void synthesizeObject(Object o) { + if (o instanceof Point) { + throw new IllegalArgumentException(); + } else { + throw new IllegalArgumentException(); + } + } + + public void synthesizeDeepComplexObject(DeepComplexObject c) { + if (c.getO().getA().getY() == 1) { + throw new IllegalArgumentException(); + } + } + + public void synthesizeComplexCounter(ComplexCounter c, ComplexObject b) { + if (c.getA() == 5 && b.getA().getX() == 1000) { + throw new IllegalArgumentException(); + } + } + + public void synthesizeComplexObject(ComplexObject b) { + if (b.getA().getX() == 1000) { + throw new IllegalArgumentException(); + } + } + + public void synthesizeComplexCounter2(ComplexCounter c, ComplexCounter d) { + ComplexCounter f = new ComplexCounter(); + f.incrementA(5); + int a = c.getA(); + int b = f.getB(); + if (c != d) { + if (a == b) { + throw new IllegalArgumentException(); + } + } + } + + public void synthesizeComplexCounter3(ComplexCounter c) { + ComplexCounter f = new ComplexCounter(); + f.incrementA(4); + if (c != f) { + throw new IllegalArgumentException(); + } + } + + public void synthesizeComplexObject2(ComplexObject a, ComplexObject b) { + if (a.getA() == b.getA()) { + throw new IllegalArgumentException(); + } + } + + public void synthesizeInt(int a, int b) { + if (a >= 2) { + if (b <= 11) { + throw new IllegalArgumentException(); + } + } + } + + public void synthesizeSimpleList(SimpleList a) { + if (a.size() == 2) { + if (a.get(0).getX() == 2) { + if (a.get(1).getY() == 11) { + throw new IllegalArgumentException(); + } + } + } + } + + public void synthesizeIntArray(int[] a) { + if (a.length > 10) { + throw new IllegalArgumentException(); + } + } + + public void synthesizePointArray(Point[] a, int i) { + if (a[i].getX() > 14) { + throw new IllegalArgumentException(); + } + } + + public void synthesizePointArray2(Point[] array, int x, int y) { + if (array[x].getX() == y) { + throw new IllegalArgumentException(); + } + } + + public void synthesizeDoublePointArray(Point[][] a, int i, int j) { + if (a[i][j].getX() > 14) { + throw new IllegalArgumentException(); + } + } + + public void synthesizeInterfaceArray(SynthesisInterface[] a, int i) { + if (a[i].getX() == 10) { + throw new IllegalArgumentException(); + } + } +} diff --git a/utbot-sample/src/main/java/org/utbot/examples/synthesis/SynthesisInterface.java b/utbot-sample/src/main/java/org/utbot/examples/synthesis/SynthesisInterface.java new file mode 100644 index 0000000000..7333f3f68f --- /dev/null +++ b/utbot-sample/src/main/java/org/utbot/examples/synthesis/SynthesisInterface.java @@ -0,0 +1,5 @@ +package org.utbot.examples.synthesis; + +public interface SynthesisInterface { + int getX(); +} diff --git a/utbot-sample/src/main/java/org/utbot/examples/synthesis/SynthesisInterfaceImpl.java b/utbot-sample/src/main/java/org/utbot/examples/synthesis/SynthesisInterfaceImpl.java new file mode 100644 index 0000000000..b7866e425d --- /dev/null +++ b/utbot-sample/src/main/java/org/utbot/examples/synthesis/SynthesisInterfaceImpl.java @@ -0,0 +1,8 @@ +package org.utbot.examples.synthesis; + +public class SynthesisInterfaceImpl implements SynthesisInterface { + @Override + public int getX() { + return 'A'; + } +}