Skip to content

Commit 26b2507

Browse files
committed
[TS] Prefer class definitions over phantom import declarations; richer diagnostics
Path-alias imports (`@/comparator`) produce phantom classes — a signature with no method bodies — that shadowed the real same-named class in method resolution and in input generation. The resolver now ranks same-named classes by substance (method bodies + fields), falls back from a phantom exact signature match to a substantial twin, and resolveInstanceMethod tries substantial twins when the receiver's own chain has no body for the method; the generator instantiates the most substantial class of a name. Unsupported diagnostics now print the receiver class signature (for objects) and the target method signature (for function values), which localized the next frontier precisely: several corpus files declare comparator fields with a function type in the IR while the code calls Comparator *methods* on them (`this.#compareFn.lessThan(a, b)`) — a ts-frontend field-typing mismatch, recorded as jacodb#361 feedback rather than papered over by generator heuristics.
1 parent 42cfeb5 commit 26b2507

3 files changed

Lines changed: 36 additions & 11 deletions

File tree

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/gen/Generators.kt

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -73,15 +73,11 @@ class InputGenerator(
7373
is EtsArrayType -> genArray(type.elementType, depth)
7474

7575
is EtsClassType -> genRefByName(type.signature.name, depth)
76-
?: run {
77-
val cls = scene.projectAndSdkClasses.firstOrNull { it.signature == type.signature }
78-
?: scene.projectAndSdkClasses.firstOrNull { it.name == type.signature.name }
79-
if (cls != null) instantiate(cls, depth) else VObject(null)
80-
}
76+
?: substantialClassByName(type.signature.name)?.let { instantiate(it, depth) }
77+
?: VObject(null)
8178

8279
is EtsUnclearRefType -> genRefByName(type.name, depth)
83-
?: scene.projectAndSdkClasses.firstOrNull { it.name == type.name }
84-
?.let { instantiate(it, depth) }
80+
?: substantialClassByName(type.name)?.let { instantiate(it, depth) }
8581
?: VObject(null)
8682

8783
is EtsFunctionType -> genFunction(type)
@@ -183,6 +179,12 @@ class InputGenerator(
183179
return VArray(MutableList(size) { generate(elementType, depth + 1) })
184180
}
185181

182+
/** Prefer definitions over phantom declarations produced by path-alias imports. */
183+
private fun substantialClassByName(name: String): EtsClass? =
184+
scene.projectAndSdkClasses
185+
.filter { it.name == name }
186+
.maxByOrNull { c -> c.methods.count { it.cfg.stmts.isNotEmpty() } * 2 + c.fields.size }
187+
186188
private fun instantiate(cls: EtsClass, depth: Int): VObject {
187189
val fields = mutableMapOf<String, VValue>()
188190
if (depth < 3) {

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/CallResolver.kt

Lines changed: 22 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,14 +21,27 @@ import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME
2121
internal class CallResolver(private val scene: EtsScene) {
2222

2323
private val classesByName: Map<String, List<EtsClass>> by lazy {
24-
(scene.projectClasses + scene.sdkClasses).groupBy { it.name }
24+
(scene.projectClasses + scene.sdkClasses)
25+
.groupBy { it.name }
26+
// Prefer definitions over declarations: path-alias imports produce
27+
// phantom classes (a signature with no method bodies) that would
28+
// otherwise shadow the real class of the same name.
29+
.mapValues { (_, classes) -> classes.sortedByDescending { it.substance() } }
2530
}
2631

32+
private fun EtsClass.substance(): Int =
33+
methods.count { it.cfg.stmts.isNotEmpty() } * 2 + fields.size
34+
2735
fun classByName(name: String): EtsClass? = classesByName[name]?.firstOrNull()
2836

2937
fun classBySignature(signature: EtsClassSignature): EtsClass? {
3038
val candidates = classesByName[signature.name] ?: return null
31-
return candidates.firstOrNull { it.signature == signature } ?: candidates.firstOrNull()
39+
val exact = candidates.firstOrNull { it.signature == signature }
40+
// A phantom exact match loses to a substantial same-named class.
41+
if (exact != null && exact.substance() == 0) {
42+
candidates.firstOrNull { it.substance() > 0 }?.let { return it }
43+
}
44+
return exact ?: candidates.firstOrNull()
3245
}
3346

3447
/** Resolve an instance method by name on [cls], walking the superclass chain. */
@@ -40,7 +53,13 @@ internal class CallResolver(private val scene: EtsScene) {
4053
?.let { return it }
4154
current = current.superClass?.let { classBySignature(it) }
4255
}
43-
return null
56+
// The receiver's class may be a phantom produced by a path-alias import:
57+
// fall back to a substantial same-named class that declares the method.
58+
return classesByName[cls.name].orEmpty()
59+
.asSequence()
60+
.filter { it !== cls }
61+
.mapNotNull { twin -> twin.methods.firstOrNull { it.name == name && it.cfg.stmts.isNotEmpty() } }
62+
.firstOrNull()
4463
}
4564

4665
/** Resolve a static call target (including free functions in the default class). */

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/EtsConcreteInterpreter.kt

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -584,7 +584,11 @@ class EtsConcreteInterpreter(
584584

585585
Intrinsics.callInstance(receiver, name, args, ::invokeFunction)
586586
?: throw UnsupportedFeatureSignal(
587-
"instance method: $name on ${receiver::class.simpleName}"
587+
"instance method: $name on " + when (receiver) {
588+
is VObject -> "VObject(${receiver.cls?.signature ?: "<record>"})"
589+
is VFunction -> "VFunction(${receiver.method.signature})"
590+
else -> receiver::class.simpleName
591+
}
588592
)
589593
}
590594

0 commit comments

Comments
 (0)