From 90e85f44e82d5bc3edab8e8dcdba54805015f24d Mon Sep 17 00:00:00 2001 From: Rustam Sadykov Date: Thu, 21 Jul 2022 11:05:09 +0300 Subject: [PATCH 1/2] Implement state initialization by fuzzing --- .../kotlin/org/utbot/framework/UtSettings.kt | 7 +- .../kotlin/org/utbot/engine/Extensions.kt | 33 ++++ .../main/kotlin/org/utbot/engine/Traverser.kt | 32 ++-- .../org/utbot/engine/UtBotSymbolicEngine.kt | 147 ++++++++++++---- .../mvisitors/ConstraintModelVisitor.kt | 164 ++++++++++++++++++ .../utbot/engine/mvisitors/ModelVisitor.kt | 37 ++++ .../kotlin/org/utbot/engine/pc/UtSolver.kt | 19 +- 7 files changed, 395 insertions(+), 44 deletions(-) create mode 100644 utbot-framework/src/main/kotlin/org/utbot/engine/mvisitors/ConstraintModelVisitor.kt create mode 100644 utbot-framework/src/main/kotlin/org/utbot/engine/mvisitors/ModelVisitor.kt 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 0b428a7065..7d2790cda8 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 @@ -258,7 +258,7 @@ object UtSettings { /** - * Set to true to start fuzzing if symbolic execution haven't return anything + * Set to true to start fuzzing if symbolic execution haven't return anything. */ var useFuzzing: Boolean by getBooleanProperty(true) @@ -272,6 +272,11 @@ object UtSettings { */ var fuzzingTimeoutInMillis: Int by getIntProperty(3_000) + /** + * Set to true to initialize symbolic parameters by values from fuzzing. + */ + var useFuzzingInitialization: Boolean by getBooleanProperty(false) + /** * Generate tests that treat possible overflows in arithmetic operations as errors * that throw Arithmetic Exception. 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 b760070557..dd214b4e99 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt @@ -46,7 +46,11 @@ import kotlin.reflect.jvm.javaMethod import kotlinx.collections.immutable.PersistentMap import kotlinx.collections.immutable.persistentHashMapOf import org.utbot.engine.pc.UtSolverStatusUNDEFINED +import org.utbot.engine.pc.select +import org.utbot.framework.plugin.api.ClassId +import org.utbot.framework.plugin.api.util.isArray import soot.ArrayType +import soot.IntType import soot.PrimType import soot.RefLikeType import soot.RefType @@ -303,6 +307,9 @@ fun classBytecodeSignatureToClassNameOrNull(signature: String?) = ?.replace("$", ".") ?.let { it.substring(1, it.lastIndex) } +val UtMethod.hasThisInParameters: Boolean + get() = !isConstructor && !isStatic + val UtMethod.javaConstructor: Constructor<*>? get() = (callable as? KFunction<*>)?.javaConstructor @@ -484,3 +491,29 @@ val SootMethod.isUtMockAssumeOrExecuteConcretely */ val SootMethod.isPreconditionCheckMethod get() = declaringClass.isOverridden && name == "preconditionCheck" + +/** + * Search symbolic ordinal of enum in memory by address [addr]. + */ +fun Memory.findOrdinal(type: RefType, addr: UtAddrExpression) : PrimitiveValue { + val array = findArray(MemoryChunkDescriptor(ENUM_ORDINAL, type, IntType.v())) + return array.select(addr).toIntValue() +} + +fun ClassId.toSoot(): SootClass = Scene.v().getSootClass(this.name) + +// Our and Soot's representations are not same +fun ClassId.toType(): Type { + var arrayDim = 0 + var result = this + while (result.isArray) { + ++arrayDim + result = result.elementClassId!! + } + val typeResult = Scene.v().getType(result.name) + return if (arrayDim != 0) { + ArrayType.v(typeResult, arrayDim) + } else { + typeResult + } +} 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 4563012cb4..38af9a6c30 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt @@ -255,6 +255,12 @@ class Traverser( // A counter for objects created as native method call result. private var unboundedConstCounter = 0 + fun collectUpdates(): SymbolicStateUpdate { + val updates = queuedSymbolicStateUpdates + queuedSymbolicStateUpdates = SymbolicStateUpdate() + return updates + } + fun traverse(state: ExecutionState): Collection { val context = TraversalContext() @@ -1245,13 +1251,7 @@ class Traverser( } is ClassConstant -> { val sootType = constant.toSootType() - val result = if (sootType is RefLikeType) { - typeRegistry.createClassRef(sootType.baseType, sootType.numDimensions) - } else { - error("Can't get class constant for ${constant.value}") - } - queuedSymbolicStateUpdates += result.symbolicStateUpdate - (result.symbolicResult as SymbolicSuccess).value + createClassRef(sootType) } else -> error("Unsupported type: $constant") } @@ -1990,6 +1990,16 @@ class Traverser( return ObjectValue(typeStorage, addr) } + 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) @@ -2052,7 +2062,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) { + 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)) @@ -2681,10 +2691,8 @@ class Traverser( return when (instance) { is ReferenceValue -> { val type = instance.type - val createClassRef = if (type is RefLikeType) { - typeRegistry.createClassRef(type.baseType, type.numDimensions) - } else { - error("Can't get class name for $type") + val createClassRef = asMethodResult { + createClassRef(type) } OverrideResult(success = true, createClassRef) } 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 9ff7cc09a7..ae1234250c 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt @@ -1,5 +1,8 @@ package org.utbot.engine +import java.lang.reflect.Method +import kotlin.random.Random +import kotlin.system.measureTimeMillis import kotlinx.collections.immutable.persistentListOf import kotlinx.coroutines.CancellationException import kotlinx.coroutines.Job @@ -22,6 +25,8 @@ import org.utbot.common.bracket import org.utbot.common.debug import org.utbot.common.workaround import org.utbot.engine.MockStrategy.NO_MOCKS +import org.utbot.engine.mvisitors.ConstraintModelVisitor +import org.utbot.engine.mvisitors.visit import org.utbot.engine.pc.UtArraySelectExpression import org.utbot.engine.pc.UtBoolExpression import org.utbot.engine.pc.UtContextInitializer @@ -70,17 +75,18 @@ import org.utbot.framework.plugin.api.UtError import org.utbot.framework.plugin.api.UtExecution import org.utbot.framework.plugin.api.UtInstrumentation import org.utbot.framework.plugin.api.UtMethod +import org.utbot.framework.plugin.api.UtModel 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.util.graph import org.utbot.framework.plugin.api.onSuccess +import org.utbot.framework.plugin.api.util.description import org.utbot.framework.plugin.api.util.executableId import org.utbot.framework.plugin.api.util.id import org.utbot.framework.plugin.api.util.utContext -import org.utbot.framework.plugin.api.util.description -import org.utbot.framework.util.jimpleBody import org.utbot.framework.plugin.api.util.voidClassId +import org.utbot.framework.util.graph +import org.utbot.framework.util.jimpleBody import org.utbot.fuzzer.FallbackModelProvider import org.utbot.fuzzer.FuzzedMethodDescription import org.utbot.fuzzer.FuzzedValue @@ -88,16 +94,18 @@ import org.utbot.fuzzer.ModelProvider import org.utbot.fuzzer.Trie import org.utbot.fuzzer.collectConstantsForFuzzer import org.utbot.fuzzer.defaultModelProviders +import org.utbot.fuzzer.exceptIsInstance import org.utbot.fuzzer.fuzz import org.utbot.fuzzer.names.MethodBasedNameSuggester import org.utbot.fuzzer.names.ModelBasedNameSuggester +import org.utbot.fuzzer.providers.CollectionModelProvider +import org.utbot.fuzzer.providers.NullModelProvider import org.utbot.fuzzer.providers.ObjectModelProvider import org.utbot.instrumentation.ConcreteExecutor +import soot.jimple.ParameterRef import soot.jimple.Stmt +import soot.jimple.internal.JIdentityStmt import soot.tagkit.ParamNamesTag -import java.lang.reflect.Method -import kotlin.random.Random -import kotlin.system.measureTimeMillis val logger = KotlinLogging.logger {} val pathLogger = KotlinLogging.logger(logger.name + ".path") @@ -158,6 +166,11 @@ class UtBotSymbolicEngine( logger.trace { "JIMPLE for $methodUnderTest:\n$this" } }.graph() + private val methodUnderTestId = if (methodUnderTest.isConstructor) { + methodUnderTest.javaConstructor!!.executableId + } else { + methodUnderTest.javaMethod!!.executableId + } private val methodUnderAnalysisStmts: Set = graph.stmts.toSet() private val globalGraph = InterProceduralUnitGraph(graph) private val typeRegistry: TypeRegistry = TypeRegistry() @@ -347,7 +360,7 @@ class UtBotSymbolicEngine( } for (newState in newStates) { when (newState.label) { - StateLabel.INTERMEDIATE -> pathSelector.offer(newState) + StateLabel.INTERMEDIATE -> processIntermediateState(newState) StateLabel.CONCRETE -> statesForConcreteExecution.add(newState) StateLabel.TERMINAL -> consumeTerminalState(newState) } @@ -365,28 +378,66 @@ class UtBotSymbolicEngine( } } + private fun getModelProviderToFuzzingInitializing(modelProvider: ModelProvider): ModelProvider = + modelProvider + .with(NullModelProvider) + // these providers use AssembleModel, now impossible to get path conditions from it + .exceptIsInstance() + .exceptIsInstance() /** - * Run fuzzing flow. - * - * @param until is used by fuzzer to cancel all tasks if the current time is over this value - * @param modelProvider provides model values for a method + * Construct sequence of [ExecutionState] that's initialized by fuzzing. */ - fun fuzzing(until: Long = Long.MAX_VALUE, modelProvider: (ModelProvider) -> ModelProvider = { it }) = flow { - val executableId = if (methodUnderTest.isConstructor) { - methodUnderTest.javaConstructor!!.executableId - } else { - methodUnderTest.javaMethod!!.executableId - } + private fun statesInitializedFromFuzzing(state: ExecutionState): Sequence = + fuzzInitialValues(::getModelProviderToFuzzingInitializing) + .map { parameters -> + val stateParametersWithoutThis = if (methodUnderTest.hasThisInParameters) { + state.parameters.drop(1) + } else { + state.parameters + } + val initialConstraints = stateParametersWithoutThis + .zip(parameters) + .flatMap { (parameter, fuzzedValue) -> + buildConstraintsFromModel(parameter.value, fuzzedValue.model) + } + state.update(traverser.collectUpdates()).apply { + solver.checkWithInitialConstraints(initialConstraints) + } + } + + private fun buildConstraintsFromModel(symbolicValue: SymbolicValue, model: UtModel): List { + val modelVisitor = ConstraintModelVisitor(symbolicValue, traverser) + return model.visit(modelVisitor) + } - val isFuzzable = executableId.parameters.all { classId -> + private fun fuzzInitialValues( + modelProvider: (ModelProvider) -> ModelProvider, + methodDescription: FuzzedMethodDescription? = null + ): Sequence> { + val isFuzzable = methodUnderTestId.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 + return emptySequence() } + val methodDescriptionOrDefault = methodDescription ?: + FuzzedMethodDescription(methodUnderTestId, collectConstantsForFuzzer(graph)) + val initializedModelProvider = modelProvider(defaultModelProviders { nextDefaultModelId++ }) + + return fuzz(methodDescriptionOrDefault, initializedModelProvider) + } + + + /** + * Run fuzzing flow. + * + * @param until is used by fuzzer to cancel all tasks if the current time is over this value + * @param modelProvider provides model values for a method + */ + fun fuzzing(until: Long = Long.MAX_VALUE, modelProvider: (ModelProvider) -> ModelProvider = { it }) = flow { val fallbackModelProvider = FallbackModelProvider { nextDefaultModelId++ } val constantValues = collectConstantsForFuzzer(graph) @@ -411,28 +462,28 @@ class UtBotSymbolicEngine( } } - val methodUnderTestDescription = FuzzedMethodDescription(executableId, collectConstantsForFuzzer(graph)).apply { - compilableName = if (methodUnderTest.isMethod) executableId.name else null - className = executableId.classId.simpleName - packageName = executableId.classId.packageName + val methodUnderTestDescription = FuzzedMethodDescription(methodUnderTestId, collectConstantsForFuzzer(graph)).apply { + compilableName = if (methodUnderTest.isMethod) methodUnderTestId.name else null + className = methodUnderTestId.classId.simpleName + packageName = methodUnderTestId.classId.packageName val names = graph.body.method.tags.filterIsInstance().firstOrNull()?.names parameterNameMap = { index -> names?.getOrNull(index) } } val coveredInstructionTracker = Trie(Instruction::id) val coveredInstructionValues = mutableMapOf, List>() var attempts = UtSettings.fuzzingMaxAttempts - val hasMethodUnderTestParametersToFuzz = executableId.parameters.isNotEmpty() + val hasMethodUnderTestParametersToFuzz = methodUnderTestId.parameters.isNotEmpty() val fuzzedValues = if (hasMethodUnderTestParametersToFuzz) { - fuzz(methodUnderTestDescription, modelProvider(defaultModelProviders { nextDefaultModelId++ })) + fuzzInitialValues(modelProvider, methodUnderTestDescription) } else { // in case a method with no parameters is passed fuzzing tries to fuzz this instance with different constructors, setters and field mutators val thisMethodDescription = FuzzedMethodDescription("thisInstance", voidClassId, listOf(methodUnderTest.clazz.id), constantValues).apply { - className = executableId.classId.simpleName - packageName = executableId.classId.packageName + className = methodUnderTestId.classId.simpleName + packageName = methodUnderTestId.classId.packageName } - fuzz(thisMethodDescription, ObjectModelProvider { nextDefaultModelId++ }.apply { + fuzzInitialValues({ ObjectModelProvider { nextDefaultModelId++ }.apply { limitValuesCreatedByFieldAccessors = 500 - }) + } }, thisMethodDescription) } fuzzedValues.forEach { values -> if (System.currentTimeMillis() >= until) { @@ -515,6 +566,42 @@ class UtBotSymbolicEngine( emit(failedConcreteExecution) } + private fun processIntermediateState( + state: ExecutionState + ) { + require(state.label == StateLabel.INTERMEDIATE) + + // create new state initialized by fuzzing if it is the last identity stmt for parameter + val initializedStateByFuzzing = if ( + UtSettings.useFuzzingInitialization && + !state.isInNestedMethod() && + state.stmt is JIdentityStmt && + state.stmt.rightOp is ParameterRef + ) { + var expectedParamsSize = if (methodUnderTest.isConstructor) { + methodUnderTest.javaConstructor!!.parameterCount + } else { + methodUnderTest.javaMethod!!.parameterCount + } + if (methodUnderTest.hasThisInParameters) { + ++expectedParamsSize + } + + // check that is the last parameter identity stmt + if (expectedParamsSize == state.parameters.size) { + statesInitializedFromFuzzing(state).firstOrNull() + } else { + null + } + } else { + null + } + + initializedStateByFuzzing?.let { + pathSelector.offer(it) + } ?: pathSelector.offer(state) + } + private suspend fun FlowCollector.consumeTerminalState( state: ExecutionState, ) { diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/mvisitors/ConstraintModelVisitor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/mvisitors/ConstraintModelVisitor.kt new file mode 100644 index 0000000000..fd51f01faf --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/mvisitors/ConstraintModelVisitor.kt @@ -0,0 +1,164 @@ +package org.utbot.engine.mvisitors + +import org.utbot.engine.ArrayValue +import org.utbot.engine.MemoryChunkDescriptor +import org.utbot.engine.ObjectValue +import org.utbot.engine.PrimitiveValue +import org.utbot.engine.ReferenceValue +import org.utbot.engine.SymbolicValue +import org.utbot.engine.Traverser +import org.utbot.engine.addr +import org.utbot.engine.findOrdinal +import org.utbot.engine.nullObjectAddr +import org.utbot.engine.pc.UtAddrExpression +import org.utbot.engine.pc.UtBoolExpression +import org.utbot.engine.pc.align +import org.utbot.engine.pc.mkEq +import org.utbot.engine.pc.mkNot +import org.utbot.engine.pc.select +import org.utbot.engine.primitiveToLiteral +import org.utbot.engine.primitiveToSymbolic +import org.utbot.engine.toSoot +import org.utbot.engine.toType +import org.utbot.engine.voidValue +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.UtEnumConstantModel +import org.utbot.framework.plugin.api.UtNullModel +import org.utbot.framework.plugin.api.UtPrimitiveModel +import org.utbot.framework.plugin.api.UtVoidModel +import soot.ArrayType +import soot.RefType + +/** + * This class builds type and value constraints for equation [symbolicValue] == specific UtModel. + * + * Note: may create memory updates in [traverser] while visiting. + */ +class ConstraintModelVisitor( + private var symbolicValue: SymbolicValue, + private val traverser: Traverser +) : UtModelVisitor> { + + private inline fun withSymbolicValue( + newSymbolicValue: SymbolicValue, + block: () -> T + ): T { + val old = symbolicValue + return try { + symbolicValue = newSymbolicValue + block() + } finally { + symbolicValue = old + } + } + + private fun mismatchTypes(): List = + emptyList() + + override fun visitArray(model: UtArrayModel): List = + when (val value = symbolicValue) { + is ArrayValue -> { + val constraints = mutableListOf() + constraints += mkNot(mkEq(value.addr, nullObjectAddr)) + val arrayLength = traverser.memory.findArrayLength(value.addr) + constraints += mkEq(arrayLength.align(), model.length.primitiveToSymbolic()) + val type = model.classId.toType() as ArrayType + val elementType = model.classId.elementClassId!!.toType() + val descriptor = MemoryChunkDescriptor(traverser.typeRegistry.arrayChunkId(type), type, elementType) + val array = traverser.memory.findArray(descriptor) + + repeat(model.length) { storeIndex -> + val storeModel = model.stores[storeIndex] ?: model.constModel + val selectedExpr = array.select(value.addr, storeIndex.primitiveToLiteral()) + val storeSymbolicValue = when (elementType) { + is RefType -> traverser.createObject( + UtAddrExpression(selectedExpr), + elementType, + useConcreteType = false, + mockInfoGenerator = null + ) + is ArrayType -> traverser.createArray( + UtAddrExpression(selectedExpr), + elementType, + useConcreteType = false + ) + else -> PrimitiveValue(elementType, selectedExpr) + } + constraints += withSymbolicValue(storeSymbolicValue) { + storeModel.visit(this) + } + } + constraints + } + else -> mismatchTypes() + } + + override fun visitAssemble(model: UtAssembleModel): List { + // TODO: not supported + return mismatchTypes() + } + + override fun visitComposite(model: UtCompositeModel): List = + when (val value = symbolicValue) { + is ObjectValue -> { + val constraints = mutableListOf() + val type = model.classId.toType() as RefType + val typeStorage = traverser.typeResolver.constructTypeStorage(type, useConcreteType = true) + constraints += traverser.typeRegistry.typeConstraint(value.addr, typeStorage).isConstraint() + model.fields.forEach { (field, fieldModel) -> + val sootField = field.declaringClass.toSoot().getFieldByName(field.name) + val fieldSymbolicValue = traverser.createFieldOrMock( + type, + value.addr, + sootField, + mockInfoGenerator = null + ) + traverser.recordInstanceFieldRead(value.addr, sootField) + constraints += withSymbolicValue(fieldSymbolicValue) { + fieldModel.visit(this) + } + } + constraints + } + else -> mismatchTypes() + } + + override fun visitNull(model: UtNullModel): List = + when (val value = symbolicValue) { + is ReferenceValue -> listOf(mkEq(value.addr, nullObjectAddr)) + else -> mismatchTypes() + } + + override fun visitPrimitive(model: UtPrimitiveModel): List = + when(val value = symbolicValue) { + is PrimitiveValue -> listOf(mkEq(value, model.value.primitiveToSymbolic())) + else -> mismatchTypes() + } + + override fun visitVoid(model: UtVoidModel): List = + when (val value = symbolicValue) { + is PrimitiveValue -> listOf(mkEq(voidValue, value)) + else -> mismatchTypes() + } + + override fun visitEnumConstant(model: UtEnumConstantModel): List = + when (val value = symbolicValue) { + is ObjectValue -> { + val ordinal = traverser.memory.findOrdinal(model.classId.toSoot().type, value.addr) + listOf(mkEq(ordinal.expr, model.value.ordinal.primitiveToLiteral())) + } + else -> mismatchTypes() + } + + override fun visitClassRef(model: UtClassRefModel): List = + when (val value = symbolicValue) { + is ObjectValue -> { + val classRef = traverser.createClassRef(model.classId.toSoot().type) + listOf(mkEq(classRef.addr, value.addr)) + } + else -> mismatchTypes() + } +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/mvisitors/ModelVisitor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/mvisitors/ModelVisitor.kt new file mode 100644 index 0000000000..ebcd44c1d1 --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/mvisitors/ModelVisitor.kt @@ -0,0 +1,37 @@ +package org.utbot.engine.mvisitors + +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.UtEnumConstantModel +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.UtVoidModel + +/** + * Class for traversing UtModel. + */ +interface UtModelVisitor { + fun visitArray(model: UtArrayModel): T + fun visitAssemble(model: UtAssembleModel): T + fun visitComposite(model: UtCompositeModel): T + fun visitNull(model: UtNullModel): T + fun visitPrimitive(model: UtPrimitiveModel): T + fun visitVoid(model: UtVoidModel): T + fun visitEnumConstant(model: UtEnumConstantModel): T + fun visitClassRef(model: UtClassRefModel): T +} + +fun UtModel.visit(visitor: UtModelVisitor): T = + when (this) { + is UtClassRefModel -> visitor.visitClassRef(this) + is UtEnumConstantModel -> visitor.visitEnumConstant(this) + is UtNullModel -> visitor.visitNull(this) + is UtPrimitiveModel -> visitor.visitPrimitive(this) + is UtArrayModel -> visitor.visitArray(this) + is UtAssembleModel -> visitor.visitAssemble(this) + is UtCompositeModel -> visitor.visitComposite(this) + UtVoidModel -> visitor.visitVoid(UtVoidModel) + } \ 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 d8dd4d0682..83d4474d71 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 @@ -16,7 +16,6 @@ import org.utbot.engine.prettify import org.utbot.engine.symbolic.Assumption import org.utbot.engine.symbolic.HardConstraint import org.utbot.engine.symbolic.SoftConstraint -import org.utbot.engine.prettify import org.utbot.engine.toIntValue import org.utbot.engine.z3.Z3Initializer import org.utbot.framework.UtSettings @@ -249,6 +248,24 @@ data class UtSolver constructor( z3Solver.reset() } + /** + * Call check of SMT Solver with [initialConstraints]. Used to initialize SMT Solver by fuzzing. + */ + fun checkWithInitialConstraints(initialConstraints: List): UtSolverStatus { + check(respectSoft = false).let { statusHolder -> + if (statusHolder is UtSolverStatusUNSAT) { + return statusHolder + } + } + val translatedConstraints = initialConstraints.translate() + val statusHolder = when (val status = check(translatedConstraints, mutableMapOf())) { + SAT -> UtSolverStatusSAT(translator, z3Solver) + else -> UtSolverStatusUNSAT(status) + } + constraints.withStatus(statusHolder) + return statusHolder + } + private fun check( translatedSoft: MutableMap, translatedAssumptions: MutableMap From a978418ef3a3aa4ba2539a3b95c5e59471bcf097 Mon Sep 17 00:00:00 2001 From: Rustam Sadykov Date: Thu, 21 Jul 2022 11:44:11 +0300 Subject: [PATCH 2/2] turn on fuzzing initialization (for testing) --- .../src/main/kotlin/org/utbot/framework/UtSettings.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 7d2790cda8..6e2d4a99d6 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 @@ -275,7 +275,7 @@ object UtSettings { /** * Set to true to initialize symbolic parameters by values from fuzzing. */ - var useFuzzingInitialization: Boolean by getBooleanProperty(false) + var useFuzzingInitialization: Boolean by getBooleanProperty(true) /** * Generate tests that treat possible overflows in arithmetic operations as errors