Skip to content

Commit 97ae9c5

Browse files
committed
[TS] Resolver: guard cyclic object graphs; look fake objects up by both key forms
- resolveTsClass now cuts cycles in object graphs (linked nodes made the recursive field resolution overflow the stack: the last 2 of 68 input-resolution failures on the datastructures corpus, now 0) - the fake-object bookkeeping in prepareForResolve stores lvalues with model-evaluated refs, while the lookup queried with the raw symbolic ref only; query by both key forms Diagnosis note: the residual replay divergence on the datastructures corpus is dominated by paths that go through engine-mocked calls (e.g. Object.prototype.hasOwnProperty.call), where the model legitimately leaves the object fields unconstrained — the replay correctly refuses to credit such branches; the number is the measured price of the remaining mocks.
1 parent 668cfaf commit 97ae9c5

1 file changed

Lines changed: 18 additions & 2 deletions

File tree

usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -478,6 +478,9 @@ open class TsTestStateResolver(
478478
return classes.first()
479479
}
480480

481+
/** Object references currently being resolved: guards against cyclic object graphs. */
482+
private val classResolutionInProgress = mutableSetOf<UConcreteHeapRef>()
483+
481484
private fun resolveTsClass(
482485
concreteRef: UConcreteHeapRef,
483486
heapRef: UHeapRef,
@@ -489,6 +492,12 @@ open class TsTestStateResolver(
489492
}
490493
check(type is EtsRefType) { "Expected EtsRefType, but got $type" }
491494
val clazz = resolveClass(type)
495+
if (!classResolutionInProgress.add(concreteRef)) {
496+
// A cyclic object graph (e.g. linked nodes): cut the cycle instead of
497+
// overflowing the stack; the replay validates the resulting input.
498+
return TsTestValue.TsClass(clazz.name, emptyMap())
499+
}
500+
try {
492501
val properties = clazz.fields
493502
.filterNot { field ->
494503
field as EtsFieldImpl
@@ -498,11 +507,15 @@ open class TsTestStateResolver(
498507
val sort = typeToSort(field.type)
499508
if (sort == unresolvedSort) {
500509
val lValue = mkFieldLValue(addressSort, heapRef, field.signature)
510+
// The bookkeeping in prepareForResolve stores lvalues with
511+
// model-EVALUATED refs, while `heapRef` here may be the raw
512+
// symbolic input ref: look the fake object up by both keys.
513+
val lValueInModel = mkFieldLValue(addressSort, evaluateInModel(heapRef), field.signature)
501514

502515
val fakeObject = if (memory is UModel) {
503-
resolvedLValuesToFakeObjects.firstOrNull { it.first == lValue }?.second
516+
resolvedLValuesToFakeObjects.firstOrNull { it.first == lValue || it.first == lValueInModel }?.second
504517
} else {
505-
resolvedLValuesToFakeObjects.lastOrNull { it.first == lValue }?.second
518+
resolvedLValuesToFakeObjects.lastOrNull { it.first == lValue || it.first == lValueInModel }?.second
506519
}
507520

508521
if (fakeObject != null) {
@@ -529,6 +542,9 @@ open class TsTestStateResolver(
529542
}
530543
}
531544
TsTestValue.TsClass(clazz.name, properties)
545+
} finally {
546+
classResolutionInProgress.remove(concreteRef)
547+
}
532548
}
533549

534550
internal var resolveMode: ResolveMode = ResolveMode.ERROR

0 commit comments

Comments
 (0)