Skip to content

Commit 42cfeb5

Browse files
CaelmBleiddCaelmBleidd
committed
[TS] Generators produce real functions and containers; new intrinsics; whitelist NaN-idiom family vs the pinned engine
Driven by the new per-reason Unsupported histogram (now a report feature): - function-typed inputs (callbacks, comparator fields — 2318 hits) generate a VFunction over a scene method of matching arity instead of junk - Map/Set/Array-typed fields and parameters generate real containers - intrinsics: global isFinite (372), JSON.stringify (748) with ES semantics (undefined/function omitted in objects, null in arrays, circular structures throw), string split/localeCompare/startsWith/ endsWith/charCodeAt/repeat - unsupported-reason histogram is collected by PbtPhase, serialized in reports and printed by the CLI summary Effect on the datastructures corpus (PBT_ONLY): covered branches 434 -> 451, unsupported executions 6718 -> 4216. Three more And methods join the whitelist: the interpreter-side idiom alignment is JS-correct on `if (NaN)` while the pinned engine still reads it as NaN != 0 = true; the family is fixed by the truthiness-idiom commits in ts-interpreter-fixes and will be unwhitelisted after the merge.
1 parent dc95536 commit 42cfeb5

7 files changed

Lines changed: 175 additions & 5 deletions

File tree

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

Lines changed: 68 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,20 +5,25 @@ import org.jacodb.ets.model.EtsArrayType
55
import org.jacodb.ets.model.EtsBooleanType
66
import org.jacodb.ets.model.EtsClass
77
import org.jacodb.ets.model.EtsClassType
8+
import org.jacodb.ets.model.EtsFunctionType
89
import org.jacodb.ets.model.EtsMethod
910
import org.jacodb.ets.model.EtsNullType
1011
import org.jacodb.ets.model.EtsNumberType
1112
import org.jacodb.ets.model.EtsScene
1213
import org.jacodb.ets.model.EtsStringType
1314
import org.jacodb.ets.model.EtsType
15+
import org.jacodb.ets.model.EtsUnclearRefType
1416
import org.jacodb.ets.model.EtsUndefinedType
1517
import org.jacodb.ets.model.EtsUnionType
1618
import org.jacodb.ets.model.EtsUnknownType
1719
import org.usvm.ts.pbt.interpreter.VArray
1820
import org.usvm.ts.pbt.interpreter.VBool
21+
import org.usvm.ts.pbt.interpreter.VFunction
22+
import org.usvm.ts.pbt.interpreter.VMap
1923
import org.usvm.ts.pbt.interpreter.VNull
2024
import org.usvm.ts.pbt.interpreter.VNumber
2125
import org.usvm.ts.pbt.interpreter.VObject
26+
import org.usvm.ts.pbt.interpreter.VSet
2227
import org.usvm.ts.pbt.interpreter.VString
2328
import org.usvm.ts.pbt.interpreter.VUndefined
2429
import org.usvm.ts.pbt.interpreter.VValue
@@ -67,11 +72,19 @@ class InputGenerator(
6772

6873
is EtsArrayType -> genArray(type.elementType, depth)
6974

70-
is EtsClassType -> {
71-
val cls = scene.projectAndSdkClasses.firstOrNull { it.signature == type.signature }
72-
?: scene.projectAndSdkClasses.firstOrNull { it.name == type.signature.name }
73-
if (cls != null) instantiate(cls, depth) else VObject(null)
74-
}
75+
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+
}
81+
82+
is EtsUnclearRefType -> genRefByName(type.name, depth)
83+
?: scene.projectAndSdkClasses.firstOrNull { it.name == type.name }
84+
?.let { instantiate(it, depth) }
85+
?: VObject(null)
86+
87+
is EtsFunctionType -> genFunction(type)
7588

7689
is EtsUnionType ->
7790
if (type.types.isEmpty()) genAny(depth)
@@ -114,6 +127,56 @@ class InputGenerator(
114127
)
115128
}
116129

130+
/** Built-in container types are not scene classes. */
131+
private fun genRefByName(name: String, depth: Int): VValue? = when (name) {
132+
"Array" -> genArray(EtsUnknownType, depth)
133+
"Map" -> {
134+
val map = VMap()
135+
repeat(random.nextInt(0, 4)) {
136+
map.entries[genPrimitiveKey()] = generate(EtsUnknownType, depth + 1)
137+
}
138+
map
139+
}
140+
141+
"Set" -> {
142+
val set = VSet()
143+
repeat(random.nextInt(0, 4)) { set.elements.add(genPrimitiveKey()) }
144+
set
145+
}
146+
147+
else -> null
148+
}
149+
150+
private fun genPrimitiveKey(): VValue = when (random.nextInt(3)) {
151+
0 -> genNumber()
152+
1 -> genString()
153+
else -> VBool(random.nextBoolean())
154+
}
155+
156+
/**
157+
* A function-typed input (a callback, a comparator field): pick a scene
158+
* method with a matching arity — real projects usually have a suitable one
159+
* (e.g. `defaultCompare`) — falling back to any method of that arity.
160+
*/
161+
private fun genFunction(type: EtsFunctionType): VValue {
162+
val sig = type.signature
163+
val declared = scene.projectAndSdkClasses.asSequence()
164+
.flatMap { it.methods }
165+
.filter { it.cfg.stmts.isNotEmpty() }
166+
.firstOrNull { it.name == sig.name && sig.name.isNotBlank() }
167+
if (declared != null) return VFunction(declared)
168+
169+
val arity = sig.parameters.size
170+
val candidates = scene.projectClasses
171+
.flatMap { it.methods }
172+
.filter {
173+
it.cfg.stmts.isNotEmpty() && it.parameters.size == arity &&
174+
!it.name.startsWith("%") && it.name != "constructor"
175+
}
176+
if (candidates.isEmpty()) return VUndefined
177+
return VFunction(candidates[random.nextInt(candidates.size)])
178+
}
179+
117180
private fun genArray(elementType: EtsType, depth: Int): VArray {
118181
var size = 0
119182
while (size < 8 && random.nextDouble() < 0.6) size++ // geometric

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,7 @@ class HybridAnalyzer(
9393
diverged = pbt.stats.diverged,
9494
unsupported = pbt.stats.unsupported,
9595
wallMs = (System.nanoTime() - pbtStart) / 1_000_000,
96+
unsupportedReasons = pbt.stats.unsupportedReasons,
9697
failures = pbt.failures.map { failure ->
9798
FailureReport(
9899
description = failure.description,

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,8 @@ data class PbtStats(
4747
val diverged: Int,
4848
val unsupported: Int,
4949
val elapsedMs: Long,
50+
/** Truncated reason -> count, for prioritizing interpreter/engine gaps. */
51+
val unsupportedReasons: Map<String, Int> = emptyMap(),
5052
)
5153

5254
class PbtResult(
@@ -84,6 +86,7 @@ class PbtPhase(
8486
var diverged = 0
8587
var unsupported = 0
8688
var executions = 0
89+
val unsupportedReasons = mutableMapOf<String, Int>()
8790

8891
val start = TimeSource.Monotonic.markNow()
8992
coverage.phase = "pbt"
@@ -107,6 +110,8 @@ class PbtPhase(
107110
is ExecutionResult.Diverged -> diverged++
108111
is ExecutionResult.Unsupported -> {
109112
unsupported++
113+
val key = result.reason.take(60)
114+
unsupportedReasons[key] = (unsupportedReasons[key] ?: 0) + 1
110115
logger.debug { "unsupported: ${result.reason}" }
111116
}
112117
}
@@ -136,6 +141,7 @@ class PbtPhase(
136141
diverged = diverged,
137142
unsupported = unsupported,
138143
elapsedMs = start.elapsedNow().inWholeMilliseconds,
144+
unsupportedReasons = unsupportedReasons,
139145
)
140146
logger.info {
141147
"PBT phase for ${method.name}: $stats, " +

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

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,11 @@ internal object Intrinsics {
2727
fun callNamespace(namespace: String, method: String, args: List<VValue>): VValue? = when (namespace) {
2828
"console", "Logger" -> VUndefined // logging is a no-op
2929

30+
"JSON" -> when (method) {
31+
"stringify" -> VString(jsonStringify(args.getOrElse(0) { VUndefined }, mutableSetOf()) ?: "undefined")
32+
else -> null
33+
}
34+
3035
"Math" -> {
3136
val x = args.getOrElse(0) { VUndefined }
3237
val n = JsSemantics.toNumber(x)
@@ -105,6 +110,51 @@ internal object Intrinsics {
105110
else -> null
106111
}
107112

113+
/**
114+
* `JSON.stringify` per ES semantics for the modeled value universe:
115+
* undefined/functions are omitted in objects and become null in arrays;
116+
* Map/Set serialize as plain empty objects; circular structures throw.
117+
* @return null when the top-level value is not serializable (undefined/function).
118+
*/
119+
private fun jsonStringify(v: VValue, visited: MutableSet<VValue>): String? = when (v) {
120+
VUndefined, is VFunction, is VNamespace -> null
121+
VNull -> "null"
122+
is VBool -> v.value.toString()
123+
is VNumber -> if (v.value.isFinite()) JsSemantics.numberToString(v.value) else "null"
124+
is VString -> jsonQuote(v.value)
125+
is VMap, is VSet -> "{}"
126+
is VArray -> {
127+
if (!visited.add(v)) throw JsThrowSignal(VString("TypeError: Converting circular structure to JSON"))
128+
val body = v.elements.joinToString(",") { jsonStringify(it, visited) ?: "null" }
129+
visited.remove(v)
130+
"[$body]"
131+
}
132+
133+
is VObject -> {
134+
if (!visited.add(v)) throw JsThrowSignal(VString("TypeError: Converting circular structure to JSON"))
135+
val body = v.fields.entries.mapNotNull { (k, value) ->
136+
jsonStringify(value, visited)?.let { "${jsonQuote(k)}:$it" }
137+
}.joinToString(",")
138+
visited.remove(v)
139+
"{$body}"
140+
}
141+
}
142+
143+
private fun jsonQuote(s: String): String = buildString {
144+
append('"')
145+
for (c in s) {
146+
when (c) {
147+
'"' -> append("\\\"")
148+
'\\' -> append("\\\\")
149+
'\n' -> append("\\n")
150+
'\r' -> append("\\r")
151+
'\t' -> append("\\t")
152+
else -> if (c < ' ') append("\\u%04x".format(c.code)) else append(c)
153+
}
154+
}
155+
append('"')
156+
}
157+
108158
private fun parseIntJs(args: List<VValue>): VNumber {
109159
val s = JsSemantics.toStringJs(args.getOrElse(0) { VUndefined }).trim()
110160
val radix = args.getOrNull(1)?.let { JsSemantics.toInt32(it) }?.takeIf { it != 0 } ?: 10
@@ -158,6 +208,8 @@ internal object Intrinsics {
158208
"Boolean" -> VBool(args.isNotEmpty() && JsSemantics.truthy(x))
159209
"String" -> VString(if (args.isEmpty()) "" else JsSemantics.toStringJs(x))
160210
"isNaN" -> VBool(JsSemantics.toNumber(x).isNaN())
211+
"isFinite" -> VBool(JsSemantics.toNumber(x).isFinite())
212+
"parseInt" -> parseIntJs(args)
161213
"parseFloat" -> VNumber(JsSemantics.stringToNumber(JsSemantics.toStringJs(x)))
162214
else -> null
163215
}
@@ -437,6 +489,38 @@ internal object Intrinsics {
437489

438490
"includes" -> VBool(s.value.contains(JsSemantics.toStringJs(args.getOrElse(0) { VUndefined })))
439491

492+
"split" -> {
493+
val sep = args.getOrNull(0)
494+
when {
495+
sep == null || sep == VUndefined -> VArray(mutableListOf(s))
496+
else -> {
497+
val sepStr = JsSemantics.toStringJs(sep)
498+
val parts = if (sepStr.isEmpty()) s.value.map { it.toString() }
499+
else s.value.split(sepStr)
500+
VArray(parts.map { VString(it) as VValue }.toMutableList())
501+
}
502+
}
503+
}
504+
505+
"localeCompare" -> VNumber(
506+
s.value.compareTo(JsSemantics.toStringJs(args.getOrElse(0) { VUndefined }))
507+
.coerceIn(-1, 1).toDouble()
508+
)
509+
510+
"startsWith" -> VBool(s.value.startsWith(JsSemantics.toStringJs(args.getOrElse(0) { VUndefined })))
511+
"endsWith" -> VBool(s.value.endsWith(JsSemantics.toStringJs(args.getOrElse(0) { VUndefined })))
512+
513+
"charCodeAt" -> {
514+
val i = JsSemantics.toNumber(args.getOrElse(0) { VNumber(0.0) }).toInt()
515+
if (i in s.value.indices) VNumber(s.value[i].code.toDouble()) else VNumber(Double.NaN)
516+
}
517+
518+
"repeat" -> {
519+
val n = JsSemantics.toNumber(args.getOrElse(0) { VUndefined })
520+
if (n.isNaN() || n < 0) throw JsThrowSignal(VString("RangeError: Invalid count value"))
521+
VString(s.value.repeat(n.toInt()))
522+
}
523+
440524
"toUpperCase" -> VString(s.value.uppercase())
441525
"toLowerCase" -> VString(s.value.lowercase())
442526
"trim" -> VString(s.value.trim())

‎usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/HybridReport.kt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,7 @@ data class PbtReport(
6464
val unsupported: Int,
6565
val wallMs: Long,
6666
val failures: List<FailureReport>,
67+
val unsupportedReasons: Map<String, Int> = emptyMap(),
6768
)
6869

6970
@Serializable

‎usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/Main.kt‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -226,6 +226,18 @@ private fun printSummary(mode: String, report: HybridReport, analysisFailures: I
226226
if (totalStmts > 0) 100.0 * coveredStmts / totalStmts else 100.0,
227227
)
228228
)
229+
val reasonTotals = mutableMapOf<String, Int>()
230+
for (m in ms) {
231+
for ((k, v) in m.pbt?.unsupportedReasons.orEmpty()) {
232+
reasonTotals[k] = (reasonTotals[k] ?: 0) + v
233+
}
234+
}
235+
if (reasonTotals.isNotEmpty()) {
236+
println(" top unsupported reasons:")
237+
reasonTotals.entries.sortedByDescending { it.value }.take(10).forEach { (k, v) ->
238+
println(" %6d %s".format(v, k))
239+
}
240+
}
229241
println(
230242
" pbt failures: $failures, unsupported executions: $unsupported; " +
231243
"symbolic targets: ${targets.size}, reached: ${targets.count { it.reached }}, " +

‎usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/ConcreteVsSymbolicDifferentialTest.kt‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,9 @@ class ConcreteVsSymbolicDifferentialTest {
8585
"Add.addUnknownValues",
8686
"Less.lessUnknown",
8787
"And.andOfUnknown", // FIXED in caelmbleidd/ts-interpreter-fixes (truthiness idiom
88+
"And.andOfNumberAndNumber", // same family: pinned engine reads `if (NaN)` as
89+
"And.andOfBooleanAndNumber", // NaN != 0 = true; fixed by the same idiom commit
90+
"And.andOfNumberAndBoolean", // in the engine branch
8891
// resolved via mkTruthyExpr for all operand kinds); unwhitelist after the
8992
// engine branch is merged and the dependency is picked up.
9093
"TypeCoercion.transitiveCoercionNoTypes",

0 commit comments

Comments
 (0)