Skip to content

Commit

Permalink
Use same memoryScope to resolve uTest and symbolicResult.
Browse files Browse the repository at this point in the history
  • Loading branch information
IlyaMuravjov authored and EgorkaKulikov committed Dec 22, 2023
1 parent c8fc4a5 commit c89b3b2
Showing 1 changed file with 15 additions and 22 deletions.
37 changes: 15 additions & 22 deletions utbot-usvm/src/main/kotlin/org/utbot/usvm/jc/JcTestExecutor.kt
Original file line number Diff line number Diff line change
Expand Up @@ -65,15 +65,8 @@ class JcTestExecutor(
classConstants: Map<JcType, UConcreteHeapRef>,
allowSymbolicResult: Boolean
): JcExecution? {
val model = state.models.first()
val mocker = state.memory.mocker as JcMocker

val resolvedMethodMocks = mocker.symbols
.entries
.groupBy({ model.eval(it.key) }, { it.value })
.mapValues { it.value.flatten() }

val uTest = createUTest(method, state, stringConstants, classConstants)
val memoryScope = createMemoryScope(state, stringConstants, classConstants, method)
val uTest = memoryScope.createUTest()

val concreteResult = runCatching {
runBlocking {
Expand All @@ -90,17 +83,8 @@ class JcTestExecutor(
when (val methodResult = state.methodResult) {
is JcMethodResult.JcException -> UTestSymbolicExceptionResult(methodResult.type)
is JcMethodResult.Success -> {
val resultScope = MemoryScope(
state.ctx,
model,
state.memory,
stringConstants,
classConstants,
resolvedMethodMocks,
method
)
val resultExpr = resultScope.resolveExpr(methodResult.value, method.returnType)
val resultInitializer = resultScope.decoderApi.initializerInstructions()
val resultExpr = memoryScope.resolveExpr(methodResult.value, method.returnType)
val resultInitializer = memoryScope.decoderApi.initializerInstructions()
UTestSymbolicSuccessResult(resultInitializer, resultExpr)
}

Expand Down Expand Up @@ -145,6 +129,16 @@ class JcTestExecutor(
stringConstants: Map<String, UConcreteHeapRef>,
classConstants: Map<JcType, UConcreteHeapRef>,
): UTest {
val memoryScope = createMemoryScope(state, stringConstants, classConstants, method)
return memoryScope.createUTest()
}

private fun createMemoryScope(
state: JcState,
stringConstants: Map<String, UConcreteHeapRef>,
classConstants: Map<JcType, UConcreteHeapRef>,
method: JcTypedMethod
): MemoryScope {
val model = state.models.first()
val ctx = state.ctx

Expand All @@ -158,8 +152,7 @@ class JcTestExecutor(
.mapValues { it.value.flatten() }

val memoryScope = MemoryScope(ctx, model, model, stringConstants, classConstants, resolvedMethodMocks, method)

return memoryScope.createUTest()
return memoryScope
}

@Suppress("UNUSED_PARAMETER")
Expand Down

0 comments on commit c89b3b2

Please sign in to comment.