@@ -45,13 +45,6 @@ import org.usvm.model.UModelBase
45
45
46
46
private val logger = KotlinLogging .logger {}
47
47
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
-
55
48
/* *
56
49
* A class, responsible for resolving a single [JcExecution] for a specific method from a symbolic state.
57
50
*
@@ -62,8 +55,6 @@ class JcTestExecutor(
62
55
val classpath : JcClasspath ,
63
56
private val runner : UTestConcreteExecutor
64
57
) {
65
-
66
-
67
58
/* *
68
59
* Resolves a [JcTest] from a [method] from a [state].
69
60
*/
@@ -74,9 +65,16 @@ class JcTestExecutor(
74
65
classConstants : Map <JcType , UConcreteHeapRef >,
75
66
allowSymbolicResult : Boolean
76
67
): 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)
78
77
79
- val uTest = createUTest(memoryScopeDescriptor)
80
78
val concreteResult = runCatching {
81
79
runBlocking {
82
80
UTestConcreteExecutionResult (runner.executeAsync(uTest))
@@ -87,13 +85,20 @@ class JcTestExecutor(
87
85
}
88
86
.getOrNull()
89
87
90
-
91
88
val symbolicResult by lazy {
92
89
if (allowSymbolicResult) {
93
90
when (val methodResult = state.methodResult) {
94
91
is JcMethodResult .JcException -> UTestSymbolicExceptionResult (methodResult.type)
95
92
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
+ )
97
102
val resultExpr = resultScope.resolveExpr(methodResult.value, method.returnType)
98
103
val resultInitializer = resultScope.decoderApi.initializerInstructions()
99
104
UTestSymbolicSuccessResult (resultInitializer, resultExpr)
@@ -134,16 +139,16 @@ class JcTestExecutor(
134
139
)
135
140
}
136
141
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
145
150
146
- val mocker = descriptor. state.memory.mocker as JcMocker
151
+ val mocker = state.memory.mocker as JcMocker
147
152
// val staticMethodMocks = mocker.statics TODO global mocks?????????????????????????
148
153
val methodMocks = mocker.symbols
149
154
@@ -152,17 +157,10 @@ class JcTestExecutor(
152
157
.groupBy({ model.eval(it.key) }, { it.value })
153
158
.mapValues { it.value.flatten() }
154
159
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)
165
161
162
+ return memoryScope.createUTest()
163
+ }
166
164
167
165
@Suppress(" UNUSED_PARAMETER" )
168
166
private fun resolveCoverage (method : JcTypedMethod , state : JcState ): JcCoverage {
0 commit comments