Skip to content

Commit a15dc8f

Browse files
committed
[TS] Mock unresolved virtual calls instead of killing the state
Coverage investigation on an open-source corpus showed that 155 of 172 unreached symbolic targets died in under 100ms: TsInterpreter killed the state (assert(false)) on ANY unresolved callee (e.g. Number.isInteger), making everything after such a call unreachable. All three unresolved-call sites in visitVirtualMethodCall now fall back to mockMethodCall + returnSite, mirroring the pre-existing unresolved-constructor approximation. Full usvm-ts suite stays green (422 tests). NOTE: an engine fix, staged to be extracted into a separate PR.
1 parent dab6d43 commit a15dc8f

1 file changed

Lines changed: 11 additions & 3 deletions

File tree

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

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,11 @@ class TsInterpreter(
183183
}
184184
return
185185
}
186-
scope.assert(falseExpr)
186+
// Approximate a call on an unresolved class with a mock instead of
187+
// killing the state: otherwise a single unmodeled call (e.g. an SDK
188+
// function) makes everything after it unreachable.
189+
mockMethodCall(scope, stmt.callee)
190+
scope.doWithState { newStmt(stmt.returnSite) }
187191
return
188192
}
189193
if (classes.size > 1) {
@@ -203,7 +207,9 @@ class TsInterpreter(
203207
logger.warn {
204208
"Could not resolve method: ${stmt.callee} on type: $type"
205209
}
206-
scope.assert(falseExpr)
210+
// Mock instead of killing the state (see the comment above).
211+
mockMethodCall(scope, stmt.callee)
212+
scope.doWithState { newStmt(stmt.returnSite) }
207213
return
208214
}
209215
} else {
@@ -212,7 +218,9 @@ class TsInterpreter(
212218
if (stmt.callee.name !in listOf("then")) {
213219
logger.warn { "Could not resolve method: ${stmt.callee}" }
214220
}
215-
scope.assert(falseExpr)
221+
// Mock instead of killing the state (see the comment above).
222+
mockMethodCall(scope, stmt.callee)
223+
scope.doWithState { newStmt(stmt.returnSite) }
216224
return
217225
}
218226
concreteMethods += methods

0 commit comments

Comments
 (0)