Skip to content

Commit 607d5d7

Browse files
tepa46tepa46
committed
Refactoring
1 parent f4e1410 commit 607d5d7

File tree

4 files changed

+52
-60
lines changed

4 files changed

+52
-60
lines changed

‎utbot-framework/src/main/kotlin/org/utbot/engine/UsvmSymbolicEngine.kt

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@ import org.utbot.usvm.jc.JcTestExecutor
4444
import org.utbot.usvm.jc.UTestConcreteExecutionResult
4545
import org.utbot.usvm.jc.findMethodOrNull
4646
import org.utbot.usvm.jc.typedMethod
47+
import org.utbot.usvm.jc.MemoryScopeDescriptor
4748
import org.utbot.usvm.machine.analyzeAsync
4849
import java.io.File
4950
import java.util.concurrent.CancellationException
@@ -60,8 +61,6 @@ object UsvmSymbolicEngine {
6061
timeoutMillis: Long
6162
): List<Pair<ExecutableId, UtResult>> {
6263

63-
JcContainer.specifyContainerTimeout(UtSettings.concreteExecutionDefaultTimeoutInInstrumentedProcessMillis)
64-
6564
val collectedExecutions = mutableListOf<Pair<ExecutableId, UtResult>>()
6665
val classpathFiles = classpath.split(File.pathSeparator).map { File(it) }
6766

@@ -154,14 +153,16 @@ object UsvmSymbolicEngine {
154153
return realJcExecution
155154
}
156155

156+
val memoryScopeDescriptor = MemoryScopeDescriptor(
157+
state.entrypoint.typedMethod,
158+
state,
159+
jcMachine.stringConstants,
160+
jcMachine.classConstants,
161+
)
162+
157163
return JcExecution(
158164
method = state.entrypoint.typedMethod,
159-
uTest = executor.createUTest(
160-
method = state.entrypoint.typedMethod,
161-
state = state,
162-
stringConstants = jcMachine.stringConstants,
163-
classConstants = jcMachine.classConstants,
164-
),
165+
uTest = executor.createUTest(memoryScopeDescriptor),
165166
uTestExecutionResultWrappers = emptySequence(),
166167
coverage = JcCoverage(emptyMap()),
167168
)

‎utbot-junit-contest/src/main/kotlin/org/utbot/contest/usvm/ContestUsvm.kt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ import org.utbot.usvm.converter.JcToUtExecutionConverter
5050
import org.utbot.usvm.converter.SimpleInstructionIdProvider
5151
import org.utbot.usvm.converter.toExecutableId
5252
import org.utbot.usvm.jc.JcContainer
53-
import org.utbot.usvm.jc.JcContainer.Companion.TEST_EXECUTION_TIMEOUT
53+
import org.utbot.usvm.jc.JcContainer.Companion.testExecutionTimeout
5454
import org.utbot.usvm.jc.JcJars
5555
import org.utbot.usvm.jc.JcTestExecutor
5656
import org.utbot.usvm.jc.findMethodOrNull
@@ -168,7 +168,7 @@ fun runUsvmGeneration(
168168
options = UMachineOptions(
169169
// TODO usvm-sbft: if we have less than CONTEST_TEST_EXECUTION_TIMEOUT time left, we should try execute
170170
// with smaller timeout, but instrumentation currently doesn't allow to change timeout for individual runs
171-
timeout = generationTimeoutMillisWithoutCodegen.milliseconds - alreadySpentBudgetMillis.milliseconds - TEST_EXECUTION_TIMEOUT,
171+
timeout = generationTimeoutMillisWithoutCodegen.milliseconds - alreadySpentBudgetMillis.milliseconds - testExecutionTimeout,
172172
pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
173173
pathSelectorFairnessStrategy = PathSelectorFairnessStrategy.COMPLETELY_FAIR,
174174
solverType = SolverType.Z3, // TODO: usvm-ksmt: Yices doesn't work on old linux

‎utbot-usvm/src/main/kotlin/org/utbot/usvm/jc/JcContainer.kt

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,9 @@ import org.usvm.instrumentation.executor.UTestConcreteExecutor
1212
import org.usvm.instrumentation.instrumentation.JcRuntimeTraceInstrumenterFactory
1313
import org.usvm.util.ApproximationPaths
1414
import org.usvm.util.classpathWithApproximations
15+
import org.utbot.framework.UtSettings
1516
import java.io.File
16-
import kotlin.time.Duration.Companion.seconds
17+
import kotlin.time.Duration.Companion.milliseconds
1718

1819
private val logger = KotlinLogging.logger {}
1920

@@ -79,7 +80,7 @@ class JcContainer(
7980
pathToJava = javaHome.absolutePath,
8081
),
8182
persistenceLocation,
82-
TEST_EXECUTION_TIMEOUT
83+
testExecutionTimeout
8384
)
8485
runBlocking {
8586
db.awaitBackgroundJobs()
@@ -93,13 +94,8 @@ class JcContainer(
9394
}
9495

9596
companion object : AutoCloseable {
96-
fun specifyContainerTimeout(timeout: Long) {
97-
testExecutionTimeout = timeout.seconds
98-
}
99-
100-
private var testExecutionTimeout = 1.seconds
101-
102-
val TEST_EXECUTION_TIMEOUT = testExecutionTimeout
97+
val testExecutionTimeout
98+
get() = UtSettings.concreteExecutionDefaultTimeoutInInstrumentedProcessMillis.milliseconds
10399

104100
private val cache = HashMap<List<File>, JcContainer>()
105101

‎utbot-usvm/src/main/kotlin/org/utbot/usvm/jc/JcTestExecutor.kt

Lines changed: 36 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,13 @@ import org.usvm.model.UModelBase
4545

4646
private val logger = KotlinLogging.logger {}
4747

48+
data class MemoryScopeDescriptor(
49+
val method: JcTypedMethod,
50+
val state: JcState,
51+
val stringConstants: Map<String, UConcreteHeapRef>,
52+
val classConstants: Map<JcType, UConcreteHeapRef>,
53+
)
54+
4855
/**
4956
* A class, responsible for resolving a single [JcExecution] for a specific method from a symbolic state.
5057
*
@@ -55,13 +62,8 @@ class JcTestExecutor(
5562
val classpath: JcClasspath,
5663
private val runner: UTestConcreteExecutor
5764
) {
58-
private val memoryScopeCache = mutableMapOf<MemoryScopeDescriptor, MemoryScope>()
59-
data class MemoryScopeDescriptor(
60-
val method: JcTypedMethod,
61-
val state: JcState,
62-
val stringConstants: Map<String, UConcreteHeapRef>,
63-
val classConstants: Map<JcType, UConcreteHeapRef>,
64-
)
65+
66+
6567
/**
6668
* Resolves a [JcTest] from a [method] from a [state].
6769
*/
@@ -72,8 +74,9 @@ class JcTestExecutor(
7274
classConstants: Map<JcType, UConcreteHeapRef>,
7375
allowSymbolicResult: Boolean
7476
): JcExecution? {
75-
val uTest = createUTest(method, state, stringConstants, classConstants)
77+
val memoryScopeDescriptor = MemoryScopeDescriptor(method, state, stringConstants, classConstants)
7678

79+
val uTest = createUTest(memoryScopeDescriptor)
7780
val concreteResult = runCatching {
7881
runBlocking {
7982
UTestConcreteExecutionResult(runner.executeAsync(uTest))
@@ -84,7 +87,6 @@ class JcTestExecutor(
8487
}
8588
.getOrNull()
8689

87-
val memoryScopeDescriptor = MemoryScopeDescriptor(method, state, stringConstants, classConstants)
8890

8991
val symbolicResult by lazy {
9092
if (allowSymbolicResult) {
@@ -132,42 +134,35 @@ class JcTestExecutor(
132134
)
133135
}
134136

135-
fun createUTest(
136-
method: JcTypedMethod,
137-
state: JcState,
138-
stringConstants: Map<String, UConcreteHeapRef>,
139-
classConstants: Map<JcType, UConcreteHeapRef>,
140-
): UTest {
141-
val memoryScopeDescriptor = MemoryScopeDescriptor(method, state, stringConstants, classConstants)
137+
fun createUTest(memoryScopeDescriptor: MemoryScopeDescriptor): UTest {
142138
val memoryScope = createMemoryScope(memoryScopeDescriptor)
143-
144139
return memoryScope.createUTest()
145140
}
146141

147-
private fun createMemoryScope(descriptor: MemoryScopeDescriptor): MemoryScope =
148-
memoryScopeCache.getOrPut(descriptor) {
149-
val model = descriptor.state.models.first()
150-
val ctx = descriptor.state.ctx
151-
152-
val mocker = descriptor.state.memory.mocker as JcMocker
153-
// val staticMethodMocks = mocker.statics TODO global mocks?????????????????????????
154-
val methodMocks = mocker.symbols
155-
156-
val resolvedMethodMocks = methodMocks
157-
.entries
158-
.groupBy({ model.eval(it.key) }, { it.value })
159-
.mapValues { it.value.flatten() }
160-
161-
MemoryScope(
162-
ctx,
163-
model,
164-
model,
165-
descriptor.stringConstants,
166-
descriptor.classConstants,
167-
resolvedMethodMocks,
168-
descriptor.method,
169-
)
170-
}
142+
private fun createMemoryScope(descriptor: MemoryScopeDescriptor): MemoryScope {
143+
val model = descriptor.state.models.first()
144+
val ctx = descriptor.state.ctx
145+
146+
val mocker = descriptor.state.memory.mocker as JcMocker
147+
// val staticMethodMocks = mocker.statics TODO global mocks?????????????????????????
148+
val methodMocks = mocker.symbols
149+
150+
val resolvedMethodMocks = methodMocks
151+
.entries
152+
.groupBy({ model.eval(it.key) }, { it.value })
153+
.mapValues { it.value.flatten() }
154+
155+
return MemoryScope(
156+
ctx,
157+
model,
158+
model,
159+
descriptor.stringConstants,
160+
descriptor.classConstants,
161+
resolvedMethodMocks,
162+
descriptor.method,
163+
)
164+
}
165+
171166

172167
@Suppress("UNUSED_PARAMETER")
173168
private fun resolveCoverage(method: JcTypedMethod, state: JcState): JcCoverage {

0 commit comments

Comments
 (0)