Skip to content

Commit 24d1003

Browse files
committed
Initial implementation of usvm tests generation in UtBot flow
1 parent 5d68839 commit 24d1003

File tree

12 files changed

+390
-111
lines changed

12 files changed

+390
-111
lines changed

utbot-framework/build.gradle

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@ dependencies {
1515
api project(':utbot-rd')
1616
api project(':utbot-modificators-analyzer')
1717

18+
api project(':utbot-usvm')
19+
1820
implementation group: 'com.jetbrains.rd', name: 'rd-framework', version: rdVersion
1921
implementation group: 'com.jetbrains.rd', name: 'rd-core', version: rdVersion
2022

Lines changed: 207 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,219 @@
11
package org.utbot.engine
22

33
import kotlinx.coroutines.flow.Flow
4-
import kotlinx.coroutines.flow.emptyFlow
4+
import kotlinx.coroutines.flow.flow
5+
import kotlinx.coroutines.runBlocking
6+
import mu.KotlinLogging
7+
import org.jacodb.approximation.Approximations
8+
import org.jacodb.impl.features.InMemoryHierarchy
9+
import org.usvm.PathSelectionStrategy
10+
import org.usvm.PathSelectorFairnessStrategy
11+
import org.usvm.SolverType
12+
import org.usvm.UMachineOptions
13+
import org.usvm.api.JcCoverage
14+
import org.usvm.machine.JcMachine
15+
import org.usvm.machine.state.JcState
16+
import org.usvm.types.ClassScorer
17+
import org.usvm.types.TypeScorer
18+
import org.usvm.types.scoreClassNode
19+
import org.utbot.common.utBotTempDirectory
20+
import org.utbot.framework.UtSettings
21+
import org.utbot.framework.codegen.domain.builtin.UtilMethodProviderPlaceholder
22+
import org.utbot.framework.context.ConcreteExecutionContext
23+
import org.utbot.framework.fuzzer.ReferencePreservingIntIdGenerator
524
import org.utbot.framework.plugin.api.ExecutableId
25+
import org.utbot.framework.plugin.api.InstrumentedProcessDeathException
26+
import org.utbot.framework.plugin.api.UtConcreteExecutionFailure
27+
import org.utbot.framework.plugin.api.UtError
28+
import org.utbot.framework.plugin.api.UtFailedExecution
629
import org.utbot.framework.plugin.api.UtResult
30+
import org.utbot.framework.plugin.api.UtSymbolicExecution
31+
import org.utbot.framework.plugin.api.util.utContext
32+
import org.utbot.framework.plugin.services.JdkInfoService
33+
import org.utbot.instrumentation.ConcreteExecutor
34+
import org.utbot.instrumentation.instrumentation.execution.UtConcreteExecutionResult
35+
import org.utbot.instrumentation.instrumentation.execution.UtExecutionInstrumentation
36+
import org.utbot.usvm.converter.JcToUtExecutionConverter
37+
import org.utbot.usvm.converter.SimpleInstructionIdProvider
38+
import org.utbot.usvm.converter.UtExecutionInitialState
39+
import org.utbot.usvm.converter.toExecutableId
40+
import org.utbot.usvm.jc.JcContainer
41+
import org.utbot.usvm.jc.JcExecution
42+
import org.utbot.usvm.jc.JcTestExecutor
43+
import org.utbot.usvm.jc.findMethodOrNull
44+
import org.utbot.usvm.jc.typedMethod
45+
import org.utbot.usvm.machine.analyzeAsync
46+
import java.io.File
47+
import java.util.concurrent.CancellationException
48+
import kotlin.time.Duration.Companion.milliseconds
749

850
object UsvmSymbolicEngine {
9-
// TODO implement
51+
52+
private val logger = KotlinLogging.logger {}
53+
1054
fun runUsvmGeneration(
1155
methods: List<ExecutableId>,
1256
classpath: String,
57+
concreteExecutionContext: ConcreteExecutionContext,
1358
timeoutMillis: Long
14-
): Flow<Pair<ExecutableId, UtResult>> =
15-
emptyFlow()
59+
): Flow<Pair<ExecutableId, UtResult>> = flow {
60+
var analysisResult: AnalysisResult? = null
61+
62+
val classpathFiles = classpath.split(File.pathSeparator).map { File(it) }
63+
val jcContainer = createJcContainer(classpathFiles)
64+
65+
val jcMethods = methods
66+
.mapNotNull { methodId -> jcContainer.cp.findMethodOrNull(methodId).also {
67+
if (it == null) {
68+
logger.error { "Method [$methodId] not found in jcClasspath [${jcContainer.cp}]" }
69+
}
70+
}
71+
}
72+
73+
JcMachine(
74+
cp = jcContainer.cp,
75+
options = UMachineOptions(
76+
timeout = timeoutMillis.milliseconds,
77+
pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
78+
pathSelectorFairnessStrategy = PathSelectorFairnessStrategy.COMPLETELY_FAIR,
79+
solverType = SolverType.Z3,
80+
)
81+
).use { jcMachine ->
82+
jcMachine.analyzeAsync(
83+
forceTerminationTimeout = (timeoutMillis * 1.1 + 2000).toLong(),
84+
methods = jcMethods,
85+
targets = emptyList()
86+
) { state ->
87+
val jcExecutionConstruction = constructJcExecution(jcMachine, state, jcContainer)
88+
89+
val jcExecution = jcExecutionConstruction.jcExecution
90+
val executableId = jcExecution.method.method.toExecutableId(jcContainer.cp)
91+
92+
val executionConverter = JcToUtExecutionConverter(
93+
jcExecution = jcExecution,
94+
jcClasspath = jcContainer.cp,
95+
idGenerator = ReferencePreservingIntIdGenerator(),
96+
instructionIdProvider = SimpleInstructionIdProvider(),
97+
utilMethodProvider = UtilMethodProviderPlaceholder,
98+
)
99+
100+
val utResult = if (jcExecutionConstruction.useUsvmExecutor) {
101+
executionConverter.convert()
102+
} else {
103+
val initialState = executionConverter.convertInitialStateOnly()
104+
val concreteExecutor = ConcreteExecutor(concreteExecutionContext.instrumentationFactory, classpath)
105+
.apply { this.classLoader = utContext.classLoader }
106+
107+
runStandardConcreteExecution(concreteExecutor, executableId, initialState)
108+
}
109+
110+
utResult?.let {
111+
analysisResult = AnalysisResult(executableId, it)
112+
}
113+
}
114+
}
115+
116+
analysisResult?.let {
117+
emit(it.executableId to it.utResult)
118+
}
119+
}
120+
121+
private fun constructJcExecution(
122+
jcMachine: JcMachine,
123+
state: JcState,
124+
jcContainer: JcContainer,
125+
): JcExecutionConstruction {
126+
val executor = JcTestExecutor(jcContainer.cp, jcContainer.runner)
127+
128+
val realJcExecution = runCatching {
129+
executor.execute(
130+
method = state.entrypoint.typedMethod,
131+
state = state,
132+
stringConstants = jcMachine.stringConstants,
133+
classConstants = jcMachine.classConstants,
134+
allowSymbolicResult = false
135+
)
136+
}.getOrElse { null }
137+
138+
realJcExecution?.let {
139+
return JcExecutionConstruction(
140+
jcExecution = it,
141+
useUsvmExecutor = true,
142+
)
143+
}
144+
145+
val jcExecutionWithUTest = JcExecution(
146+
method = state.entrypoint.typedMethod,
147+
uTest = executor.createUTest(
148+
method = state.entrypoint.typedMethod,
149+
state = state,
150+
stringConstants = jcMachine.stringConstants,
151+
classConstants = jcMachine.classConstants,
152+
),
153+
uTestExecutionResultWrappers = emptySequence(),
154+
coverage = JcCoverage(emptyMap()),
155+
)
156+
157+
return JcExecutionConstruction(
158+
jcExecution = jcExecutionWithUTest,
159+
useUsvmExecutor = false,
160+
)
161+
}
162+
163+
private fun runStandardConcreteExecution(
164+
concreteExecutor: ConcreteExecutor<UtConcreteExecutionResult, UtExecutionInstrumentation>,
165+
executableId: ExecutableId,
166+
initialState: UtExecutionInitialState,
167+
): UtResult? {
168+
return try {
169+
val concreteExecutionResult = runBlocking {
170+
concreteExecutor.executeConcretely(
171+
executableId,
172+
initialState.stateBefore,
173+
initialState.instrumentations,
174+
UtSettings.concreteExecutionDefaultTimeoutInInstrumentedProcessMillis,
175+
)
176+
}
177+
178+
UtSymbolicExecution(
179+
initialState.stateBefore,
180+
concreteExecutionResult.stateAfter,
181+
concreteExecutionResult.result,
182+
concreteExecutionResult.newInstrumentation ?: initialState.instrumentations,
183+
mutableListOf(),
184+
listOf(),
185+
concreteExecutionResult.coverage
186+
)
187+
} catch (e: CancellationException) {
188+
logger.debug(e) { "Cancellation happened" }
189+
null
190+
} catch (e: InstrumentedProcessDeathException) {
191+
UtFailedExecution(
192+
stateBefore = initialState.stateBefore,
193+
result = UtConcreteExecutionFailure(e)
194+
)
195+
} catch (e: Throwable) {
196+
UtError("Concrete execution failed", e)
197+
}
198+
}
199+
200+
private fun createJcContainer(classpathFiles: List<File>) = JcContainer(
201+
usePersistence = false,
202+
persistenceDir = utBotTempDirectory.toFile().resolve("jacoDbPersisitenceDirectory"),
203+
classpath = classpathFiles,
204+
javaHome = JdkInfoService.provide().path.toFile(),
205+
) {
206+
installFeatures(InMemoryHierarchy, Approximations, ClassScorer(TypeScorer, ::scoreClassNode))
207+
loadByteCode(classpathFiles)
208+
}
209+
210+
data class JcExecutionConstruction(
211+
val jcExecution: JcExecution,
212+
val useUsvmExecutor: Boolean,
213+
)
214+
215+
data class AnalysisResult(
216+
val executableId: ExecutableId,
217+
val utResult: UtResult,
218+
)
16219
}

utbot-framework/src/main/kotlin/org/utbot/framework/codegen/domain/builtin/UtilMethodProviderPlaceholder.kt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import org.utbot.framework.plugin.api.UtExecutableCallModel
77
import org.utbot.framework.plugin.api.UtModel
88
import org.utbot.framework.plugin.api.UtStatementCallModel
99
import org.utbot.framework.plugin.api.UtStatementModel
10+
import org.utbot.framework.utils.UtilMethodProvider
1011

1112
/**
1213
* Can be used in `UtModel`s to denote class containing util methods,

utbot-framework/src/main/kotlin/org/utbot/framework/plugin/api/TestCaseGenerator.kt

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -291,7 +291,15 @@ open class TestCaseGenerator(
291291
logger.debug("test generator global scope lifecycle check ended")
292292
}
293293

294-
consumeUtResultFlow(UsvmSymbolicEngine.runUsvmGeneration(methods, classpathForEngine, usvmTimeoutMillis))
294+
// retrieves from cache ConcreteExecutor(concreteExecutionContext.instrumentationFactory, classpathForEngine)
295+
consumeUtResultFlow(
296+
UsvmSymbolicEngine.runUsvmGeneration(
297+
methods = methods,
298+
classpath = classpathForEngine,
299+
concreteExecutionContext = concreteExecutionContext,
300+
timeoutMillis = usvmTimeoutMillis,
301+
)
302+
)
295303
}
296304
}
297305

utbot-junit-contest/build.gradle

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -172,16 +172,6 @@ dependencies {
172172

173173
implementation "org.burningwave:core:12.62.7"
174174

175-
implementation "$usvmRepo:usvm-core:$usvmVersion"
176-
implementation "$usvmRepo:usvm-jvm:$usvmVersion"
177-
implementation "$usvmRepo:usvm-jvm-api:$usvmVersion"
178-
implementation "$usvmRepo:usvm-jvm-instrumentation:$usvmVersion"
179-
implementation "$usvmRepo:usvm-jvm-instrumentation-collectors:$usvmVersion"
180-
181-
implementation group: "org.jacodb", name: "jacodb-core", version: jacoDbVersion
182-
implementation group: "org.jacodb", name: "jacodb-analysis", version: jacoDbVersion
183-
implementation group: "org.jacodb", name: "jacodb-approximations", version: jacoDbVersion
184-
185175
// TODO uvms-sbft-hack: UtBot has `fastutil:8.3.0` on the classpath that overrides classes from
186176
// `fastutil-core:8.5.11` that USVM adds. Solution: bump `fastutil` version to `8.5.11`
187177
runtimeOnly("it.unimi.dsi:fastutil:8.5.11")

0 commit comments

Comments
 (0)