Skip to content

Commit d747447

Browse files
committed
Extract mock method
1 parent 6e4414a commit d747447

File tree

1 file changed

+25
-38
lines changed

1 file changed

+25
-38
lines changed

usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt

Lines changed: 25 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ import org.jacodb.ets.base.EtsThrowStmt
2121
import org.jacodb.ets.base.EtsType
2222
import org.jacodb.ets.base.EtsValue
2323
import org.jacodb.ets.model.EtsMethod
24+
import org.jacodb.ets.model.EtsMethodSignature
2425
import org.jacodb.ets.utils.callExpr
2526
import org.jacodb.ets.utils.getDeclaredLocals
2627
import org.usvm.StepResult
@@ -164,25 +165,7 @@ class TsInterpreter(
164165
}
165166

166167
if (!tsOptions.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) {
167-
scope.doWithState {
168-
with(ctx) {
169-
val resultSort = typeToSort(it.method.returnType)
170-
val resultValue = when (resultSort) {
171-
is UAddressSort -> makeSymbolicRefUntyped()
172-
is TsUnresolvedSort -> {
173-
mkFakeValue(
174-
scope,
175-
makeSymbolicPrimitive(ctx.boolSort),
176-
makeSymbolicPrimitive(ctx.fp64Sort),
177-
makeSymbolicRefUntyped()
178-
)
179-
}
180-
181-
else -> makeSymbolicPrimitive(resultSort)
182-
}
183-
this@doWithState.methodResult = TsMethodResult.Success.MockedCall(it.method, resultValue)
184-
}
185-
}
168+
mockMethodCall(scope, it.method)
186169
return
187170
}
188171

@@ -305,25 +288,7 @@ class TsInterpreter(
305288
}
306289

307290
// intraprocedural analysis
308-
scope.doWithState {
309-
with(ctx) {
310-
val resultSort = typeToSort(stmt.expr.method.returnType)
311-
val resultValue = when (resultSort) {
312-
is UAddressSort -> makeSymbolicRefUntyped()
313-
is TsUnresolvedSort -> {
314-
mkFakeValue(
315-
scope,
316-
makeSymbolicPrimitive(ctx.boolSort),
317-
makeSymbolicPrimitive(ctx.fp64Sort),
318-
makeSymbolicRefUntyped()
319-
)
320-
}
321-
322-
else -> makeSymbolicPrimitive(resultSort)
323-
}
324-
methodResult = TsMethodResult.Success.MockedCall(stmt.expr.method, resultValue)
325-
}
326-
}
291+
mockMethodCall(scope, stmt.method.signature)
327292
}
328293

329294
private fun visitThrowStmt(scope: TsStepScope, stmt: EtsThrowStmt) {
@@ -417,6 +382,28 @@ class TsInterpreter(
417382
return state
418383
}
419384

385+
private fun mockMethodCall(scope: TsStepScope, method: EtsMethodSignature) {
386+
scope.doWithState {
387+
with(ctx) {
388+
val resultSort = typeToSort(method.returnType)
389+
val resultValue = when (resultSort) {
390+
is UAddressSort -> makeSymbolicRefUntyped()
391+
is TsUnresolvedSort -> {
392+
mkFakeValue(
393+
scope,
394+
makeSymbolicPrimitive(ctx.boolSort),
395+
makeSymbolicPrimitive(ctx.fp64Sort),
396+
makeSymbolicRefUntyped()
397+
)
398+
}
399+
400+
else -> makeSymbolicPrimitive(resultSort)
401+
}
402+
methodResult = TsMethodResult.Success.MockedCall(method, resultValue)
403+
}
404+
}
405+
}
406+
420407
// TODO: expand with interpreter implementation
421408
private val EtsStmt.nextStmt: EtsStmt?
422409
get() = applicationGraph.successors(this).firstOrNull()

0 commit comments

Comments
 (0)