@@ -45,13 +45,6 @@ import org.usvm.model.UModelBase
4545
4646private 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-
5548/* *
5649 * A class, responsible for resolving a single [JcExecution] for a specific method from a symbolic state.
5750 *
@@ -62,8 +55,6 @@ class JcTestExecutor(
6255 val classpath : JcClasspath ,
6356 private val runner : UTestConcreteExecutor
6457) {
65-
66-
6758 /* *
6859 * Resolves a [JcTest] from a [method] from a [state].
6960 */
@@ -74,9 +65,16 @@ class JcTestExecutor(
7465 classConstants : Map <JcType , UConcreteHeapRef >,
7566 allowSymbolicResult : Boolean
7667 ): JcExecution ? {
77- val memoryScopeDescriptor = MemoryScopeDescriptor (method, state, stringConstants, classConstants)
68+ val model = state.models.first()
69+ val mocker = state.memory.mocker as JcMocker
70+
71+ val resolvedMethodMocks = mocker.symbols
72+ .entries
73+ .groupBy({ model.eval(it.key) }, { it.value })
74+ .mapValues { it.value.flatten() }
75+
76+ val uTest = createUTest(method, state, stringConstants, classConstants)
7877
79- val uTest = createUTest(memoryScopeDescriptor)
8078 val concreteResult = runCatching {
8179 runBlocking {
8280 UTestConcreteExecutionResult (runner.executeAsync(uTest))
@@ -87,13 +85,20 @@ class JcTestExecutor(
8785 }
8886 .getOrNull()
8987
90-
9188 val symbolicResult by lazy {
9289 if (allowSymbolicResult) {
9390 when (val methodResult = state.methodResult) {
9491 is JcMethodResult .JcException -> UTestSymbolicExceptionResult (methodResult.type)
9592 is JcMethodResult .Success -> {
96- val resultScope = createMemoryScope(memoryScopeDescriptor)
93+ val resultScope = MemoryScope (
94+ state.ctx,
95+ model,
96+ state.memory,
97+ stringConstants,
98+ classConstants,
99+ resolvedMethodMocks,
100+ method
101+ )
97102 val resultExpr = resultScope.resolveExpr(methodResult.value, method.returnType)
98103 val resultInitializer = resultScope.decoderApi.initializerInstructions()
99104 UTestSymbolicSuccessResult (resultInitializer, resultExpr)
@@ -134,16 +139,16 @@ class JcTestExecutor(
134139 )
135140 }
136141
137- fun createUTest (memoryScopeDescriptor : MemoryScopeDescriptor ): UTest {
138- val memoryScope = createMemoryScope(memoryScopeDescriptor)
139- return memoryScope.createUTest()
140- }
141-
142- private fun createMemoryScope ( descriptor : MemoryScopeDescriptor ): MemoryScope {
143- val model = descriptor. state.models.first()
144- val ctx = descriptor. state.ctx
142+ fun createUTest (
143+ method : JcTypedMethod ,
144+ state : JcState ,
145+ stringConstants : Map < String , UConcreteHeapRef >,
146+ classConstants : Map < JcType , UConcreteHeapRef >,
147+ ): UTest {
148+ val model = state.models.first()
149+ val ctx = state.ctx
145150
146- val mocker = descriptor. state.memory.mocker as JcMocker
151+ val mocker = state.memory.mocker as JcMocker
147152 // val staticMethodMocks = mocker.statics TODO global mocks?????????????????????????
148153 val methodMocks = mocker.symbols
149154
@@ -152,17 +157,10 @@ class JcTestExecutor(
152157 .groupBy({ model.eval(it.key) }, { it.value })
153158 .mapValues { it.value.flatten() }
154159
155- return MemoryScope (
156- ctx,
157- model,
158- model,
159- descriptor.stringConstants,
160- descriptor.classConstants,
161- resolvedMethodMocks,
162- descriptor.method,
163- )
164- }
160+ val memoryScope = MemoryScope (ctx, model, model, stringConstants, classConstants, resolvedMethodMocks, method)
165161
162+ return memoryScope.createUTest()
163+ }
166164
167165 @Suppress(" UNUSED_PARAMETER" )
168166 private fun resolveCoverage (method : JcTypedMethod , state : JcState ): JcCoverage {
0 commit comments