Skip to content

Commit 41f0565

Browse files
committed
[TS] Extend the concrete interpreter: functions, HOFs, Map/Set, ptr_call
Driven by an Unsupported-reason histogram over the open-source corpus: - first-class functions (VFunction): arrow-function locals resolved via their FunctionType signature and file-initializer aliases; ptr_call dispatches through the dynamic function value (recursion of `const f = (...) => ...` now works) - higher-order array intrinsics with real callback invocation: map, filter, forEach, reduce, some, every, find, findIndex, sort - JS Map/Set (VMap/VSet) with SameValueZero keys: get/set/has/delete/ clear/keys/values/forEach, size - `new Array/Map/Set` constructors; Array(n) sizing - extended Math (log/log2/log10/exp/sign/trig/hypot/atan2/...), Number.parseInt/isSafeInteger, Object.keys/values
1 parent e19de97 commit 41f0565

7 files changed

Lines changed: 461 additions & 26 deletions

File tree

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/TypeProfiler.kt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ class TypeProfiler : ExecutionListener {
4545
VNull -> TsHintType.NULL
4646
VUndefined -> TsHintType.UNDEFINED
4747
is VArray -> TsHintType.ARRAY
48-
is VObject, is VNamespace -> TsHintType.OBJECT
48+
else -> TsHintType.OBJECT // objects, namespaces, functions, maps, sets
4949
}
5050
}
5151
}

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

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,15 @@
11
package org.usvm.ts.pbt.interpreter
22

3+
import org.jacodb.ets.model.EtsAssignStmt
34
import org.jacodb.ets.model.EtsClass
45
import org.jacodb.ets.model.EtsClassSignature
6+
import org.jacodb.ets.model.EtsFunctionType
7+
import org.jacodb.ets.model.EtsLocal
58
import org.jacodb.ets.model.EtsMethod
69
import org.jacodb.ets.model.EtsMethodSignature
710
import org.jacodb.ets.model.EtsScene
811
import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME
12+
import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME
913

1014
/**
1115
* Concrete callee resolution over an [EtsScene].
@@ -58,4 +62,57 @@ internal class CallResolver(private val scene: EtsScene) {
5862
.filter { it.name == callee.name && it.cfg.stmts.isNotEmpty() }
5963
return global.singleOrNull()
6064
}
65+
66+
/**
67+
* Variable-name -> method aliases for function values.
68+
*
69+
* Front ends lower `const f = (...) => ...` into an anonymous method
70+
* (`%AM0$...`) plus an assignment `f := %AM0$...` (a local of a
71+
* [EtsFunctionType] whose signature points to the actual method) inside the
72+
* file-initializer (`%dflt::%dflt`). A later `ptr_call f(...)` carries only
73+
* the *variable* name in its callee signature; this map recovers the target.
74+
*/
75+
private val functionAliases: Map<String, EtsMethod> by lazy {
76+
val aliases = mutableMapOf<String, EtsMethod>()
77+
for (cls in scene.projectClasses) {
78+
if (cls.name != DEFAULT_ARK_CLASS_NAME) continue
79+
val fileInit = cls.methods.firstOrNull { it.name == DEFAULT_ARK_METHOD_NAME } ?: continue
80+
for (stmt in fileInit.cfg.stmts) {
81+
if (stmt !is EtsAssignStmt) continue
82+
val lhv = stmt.lhv as? EtsLocal ?: continue
83+
val rhv = stmt.rhv as? EtsLocal ?: continue
84+
val fnType = rhv.type as? EtsFunctionType ?: continue
85+
val target = cls.methods.firstOrNull { it.name == fnType.signature.name }
86+
?: classByName(fnType.signature.enclosingClass.name)
87+
?.methods?.firstOrNull { it.name == fnType.signature.name }
88+
if (target != null && target.cfg.stmts.isNotEmpty()) {
89+
aliases.putIfAbsent(lhv.name, target)
90+
}
91+
}
92+
}
93+
aliases
94+
}
95+
96+
/** Resolve a `ptr_call` target: by function-value alias, then by literal name. */
97+
fun resolveFunctionPointer(callee: EtsMethodSignature): EtsMethod? =
98+
functionAliases[callee.name] ?: resolveStaticMethod(callee)
99+
100+
/** The method behind a file-level `const f = (...) => ...` binding, if any. */
101+
fun functionAliasFor(name: String): EtsMethod? = functionAliases[name]
102+
103+
/**
104+
* Resolve the method behind a [EtsFunctionType]-typed value (a function literal:
105+
* the type signature carries the anonymous method name and its declaring class).
106+
*/
107+
fun methodByFunctionType(type: EtsFunctionType): EtsMethod? {
108+
val sig = type.signature
109+
if (sig.name.isBlank()) return null
110+
val declared = classBySignature(sig.enclosingClass)
111+
?.methods?.firstOrNull { it.name == sig.name && it.cfg.stmts.isNotEmpty() }
112+
if (declared != null) return declared
113+
return scene.projectClasses
114+
.flatMap { it.methods }
115+
.filter { it.name == sig.name && it.cfg.stmts.isNotEmpty() }
116+
.singleOrNull()
117+
}
61118
}

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

Lines changed: 91 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ import org.jacodb.ets.model.EtsDivExpr
1717
import org.jacodb.ets.model.EtsEntity
1818
import org.jacodb.ets.model.EtsEqExpr
1919
import org.jacodb.ets.model.EtsExpExpr
20+
import org.jacodb.ets.model.EtsFunctionType
2021
import org.jacodb.ets.model.EtsGlobalRef
2122
import org.jacodb.ets.model.EtsGtEqExpr
2223
import org.jacodb.ets.model.EtsGtExpr
@@ -198,6 +199,7 @@ class EtsConcreteInterpreter(
198199
// Immediates
199200
is EtsLocal -> frame.locals[e.name]
200201
?: frame.args.getOrNull(parameterIndexOfLocal(frame, e.name) ?: -1)
202+
?: functionValueOf(e)
201203
?: VUndefined
202204

203205
is EtsNumberConstant -> VNumber(e.value)
@@ -325,6 +327,20 @@ class EtsConcreteInterpreter(
325327
private fun isZeroConstant(e: EtsEntity): Boolean =
326328
e is EtsNumberConstant && e.value == 0.0
327329

330+
/**
331+
* A local of a function type that was never assigned is a function
332+
* *literal reference*: its type signature names the lowered method
333+
* (e.g. `factorial := %AM0$%dflt` in the file initializer).
334+
*/
335+
private fun functionValueOf(e: EtsLocal): VValue? {
336+
val fnType = e.type as? EtsFunctionType ?: return null
337+
val method = resolver.methodByFunctionType(fnType)
338+
?: resolver.resolveFunctionPointer(fnType.signature)
339+
?: resolver.functionAliasFor(e.name)
340+
?: return null
341+
return VFunction(method)
342+
}
343+
328344
private inline fun numeric(
329345
left: EtsEntity,
330346
right: EtsEntity,
@@ -357,6 +373,9 @@ class EtsConcreteInterpreter(
357373
}
358374
return when (v) {
359375
is VArray -> typeName == "Array"
376+
is VMap -> typeName == "Map"
377+
is VSet -> typeName == "Set"
378+
is VFunction -> typeName == "Function"
360379
is VObject -> {
361380
var cls = v.cls
362381
val visited = mutableSetOf<String>()
@@ -398,6 +417,8 @@ class EtsConcreteInterpreter(
398417
is VObject -> instance.fields[name] ?: VUndefined
399418
is VArray -> if (name == "length") VNumber(instance.elements.size.toDouble()) else VUndefined
400419
is VString -> if (name == "length") VNumber(instance.value.length.toDouble()) else VUndefined
420+
is VMap -> if (name == "size") VNumber(instance.entries.size.toDouble()) else VUndefined
421+
is VSet -> if (name == "size") VNumber(instance.elements.size.toDouble()) else VUndefined
401422
is VNamespace -> Intrinsics.namespaceField(instance.name, name)
402423
?: throw UnsupportedFeatureSignal("namespace field: ${instance.name}.$name")
403424

@@ -414,11 +435,24 @@ class EtsConcreteInterpreter(
414435
}
415436

416437
private fun newObject(e: EtsNewExpr): VValue {
438+
val typeName = when (val t = e.type) {
439+
is EtsClassType -> t.signature.name
440+
is EtsUnclearRefType -> t.name
441+
else -> null
442+
}
417443
val cls = when (val t = e.type) {
418444
is EtsClassType -> resolver.classBySignature(t.signature)
419445
is EtsUnclearRefType -> resolver.classByName(t.name)
420446
else -> null
421447
}
448+
if (cls == null) {
449+
// Built-in containers are not scene classes
450+
when (typeName) {
451+
"Array" -> return VArray()
452+
"Map" -> return VMap()
453+
"Set" -> return VSet()
454+
}
455+
}
422456
return VObject(cls)
423457
}
424458

@@ -504,14 +538,46 @@ class EtsConcreteInterpreter(
504538
}
505539
}
506540

507-
// Constructor of a class outside the scene (e.g. `new Error(msg)`):
508-
// model as a record initialization.
509-
if (name == CONSTRUCTOR_NAME && receiver is VObject) {
510-
args.firstOrNull()?.let { receiver.fields["message"] = it }
511-
return receiver
541+
// Constructors of classes outside the scene.
542+
if (name == CONSTRUCTOR_NAME) {
543+
when (receiver) {
544+
is VObject -> {
545+
// e.g. `new Error(msg)`: model as record initialization
546+
args.firstOrNull()?.let { receiver.fields["message"] = it }
547+
return receiver
548+
}
549+
550+
is VArray -> {
551+
// `new Array(n)` / `new Array(a, b, ...)`
552+
if (args.size == 1 && args[0] is VNumber) {
553+
val n = (args[0] as VNumber).value
554+
if (n == floor(n) && n >= 0) {
555+
receiver.elements.clear()
556+
repeat(n.toInt()) { receiver.elements.add(VUndefined) }
557+
} else {
558+
throw JsThrowSignal(VString("RangeError: Invalid array length"))
559+
}
560+
} else {
561+
receiver.elements.clear()
562+
receiver.elements.addAll(args)
563+
}
564+
return receiver
565+
}
566+
567+
is VMap, is VSet -> {
568+
if (args.isEmpty() || args[0] == VUndefined || args[0] == VNull) return receiver
569+
if (receiver is VSet && args[0] is VArray) {
570+
(args[0] as VArray).elements.forEach { receiver.elements.add(it) }
571+
return receiver
572+
}
573+
throw UnsupportedFeatureSignal("iterable constructor argument for Map/Set")
574+
}
575+
576+
else -> Unit
577+
}
512578
}
513579

514-
Intrinsics.callInstance(receiver, name, args)
580+
Intrinsics.callInstance(receiver, name, args, ::invokeFunction)
515581
?: throw UnsupportedFeatureSignal(
516582
"instance method: $name on ${receiver::class.simpleName}"
517583
)
@@ -528,7 +594,21 @@ class EtsConcreteInterpreter(
528594
runMethod(callee, VUndefined, padArgs(callee, args))
529595
}
530596

531-
is EtsPtrCallExpr -> throw UnsupportedFeatureSignal("ptr call: $expr")
597+
is EtsPtrCallExpr -> {
598+
// Prefer the dynamic function value held by the pointer local
599+
val ptrValue = eval(expr.ptr, frame)
600+
if (ptrValue is VFunction) {
601+
runMethod(ptrValue.method, ptrValue.thisValue, padArgs(ptrValue.method, args))
602+
} else {
603+
val callee = resolver.resolveFunctionPointer(expr.callee)
604+
if (callee != null) {
605+
runMethod(callee, frame.thisValue, padArgs(callee, args))
606+
} else {
607+
Intrinsics.callConversion(expr.callee.name, args)
608+
?: throw UnsupportedFeatureSignal("ptr call: ${expr.callee.name}")
609+
}
610+
}
611+
}
532612

533613
else -> throw UnsupportedFeatureSignal("call kind: ${expr::class.simpleName}")
534614
}
@@ -538,5 +618,9 @@ class EtsConcreteInterpreter(
538618
if (args.size >= callee.parameters.size) return args
539619
return args + List(callee.parameters.size - args.size) { VUndefined }
540620
}
621+
622+
/** Host callback for higher-order intrinsics (`arr.map(f)`, `map.forEach(f)`, ...). */
623+
private fun invokeFunction(fn: VFunction, args: List<VValue>): VValue =
624+
runMethod(fn.method, fn.thisValue, padArgs(fn.method, args))
541625
}
542626
}

0 commit comments

Comments
 (0)