From 308913ebd65c8ceb67dc3822b35154fa9cb00884 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 20 Oct 2026 12:17:04 +0300 Subject: [PATCH 1/3] Propagate failed TypeScript value materialization --- .../org/usvm/ts/calls/CallsCapturedValues.kt | 8 +-- .../usvm/ts/calls/CallsInputMaterializer.kt | 5 +- .../usvm/ts/pbt/usvm/UsvmDomainProjector.kt | 8 ++- .../src/main/kotlin/org/usvm/api/TsMock.kt | 10 ++-- .../main/kotlin/org/usvm/machine/TsContext.kt | 2 +- .../call/TsUnknownCallModelDispatcher.kt | 9 ++-- .../org/usvm/machine/expr/ArrayIterator.kt | 4 +- .../usvm/machine/expr/CallApproximations.kt | 10 ++-- .../usvm/machine/expr/ErrorModelStorage.kt | 4 +- .../kotlin/org/usvm/machine/expr/ReadArray.kt | 10 ++-- .../kotlin/org/usvm/machine/expr/ReadField.kt | 8 +-- .../org/usvm/machine/expr/TsExprResolver.kt | 2 +- .../org/usvm/machine/expr/WriteArray.kt | 4 +- .../org/usvm/machine/expr/WriteField.kt | 14 +++-- .../machine/interpreter/TsInitialState.kt | 5 +- .../usvm/machine/interpreter/TsInterpreter.kt | 13 ++--- .../org/usvm/machine/interpreter/TsPromise.kt | 6 +-- .../org/usvm/machine/types/FakeExprUtil.kt | 51 +++++++++++++------ .../kotlin/org/usvm/util/TypedArrayStorage.kt | 2 +- .../src/main/kotlin/org/usvm/util/Utils.kt | 4 +- .../org/usvm/machine/TsContextFactoryTest.kt | 37 ++++++-------- .../machine/TsMachineFailurePrefixTest.kt | 2 +- .../expr/ExprUtilConditionalValueTest.kt | 35 +++++-------- .../usvm/machine/types/FakeExprUtilTest.kt | 46 +++++++++++------ .../models/UnmodeledGlobalBinding.ts | 4 +- 25 files changed, 166 insertions(+), 137 deletions(-) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCapturedValues.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCapturedValues.kt index ea41a02fee..5484cf610e 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCapturedValues.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCapturedValues.kt @@ -12,7 +12,7 @@ import org.usvm.UHeapRef import org.usvm.api.allocateConcreteRef import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.state.TsState -import org.usvm.machine.types.mkFakeValue +import org.usvm.machine.types.mkInitialFakeValue import org.usvm.ts.pbt.fastcheck.TypeScriptCaptureKind import org.usvm.ts.pbt.fastcheck.TypeScriptSourceCapture import org.usvm.ts.pbt.mapping.EtsLexicalEnvironmentBinding @@ -165,9 +165,9 @@ private fun TsState.captureStorageValue(payload: UExpr<*>, type: EtsType): UExpr if (declaredSort !is TsUnresolvedSort) return payload when (payload.sort) { - boolSort -> mkFakeValue(scope = null, boolValue = payload.asExpr(boolSort)) - fp64Sort -> mkFakeValue(scope = null, fpValue = payload.asExpr(fp64Sort)) - addressSort -> mkFakeValue(scope = null, refValue = payload.asExpr(addressSort)) + boolSort -> mkInitialFakeValue(boolValue = payload.asExpr(boolSort)) + fp64Sort -> mkInitialFakeValue(fpValue = payload.asExpr(fp64Sort)) + addressSort -> mkInitialFakeValue(refValue = payload.asExpr(addressSort)) else -> error("Unsupported captured payload sort: ${payload.sort}") } } diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt index 03d4b20fe8..8f741dd924 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt @@ -14,7 +14,7 @@ import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.state.TsState import org.usvm.machine.types.EtsFakeType import org.usvm.machine.types.extractValue -import org.usvm.machine.types.mkFakeValue +import org.usvm.machine.types.mkInitialFakeValue import org.usvm.sizeSort import org.usvm.ts.pbt.model.ArrayDomain import org.usvm.ts.pbt.model.BooleanDomain @@ -147,8 +147,7 @@ private fun TsState.materializeCallsOptional( fpTypeExpr = numberKind, refTypeExpr = referenceKind, ) - val value = mkFakeValue( - scope = null, + val value = mkInitialFakeValue( boolValue = nestedBool.first ?: falseExpr, fpValue = nestedNumber.first ?: mkFp64(0.0), refValue = reference, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt index 21463bce69..64b2439511 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt @@ -19,7 +19,7 @@ import org.usvm.api.initializeArrayLength import org.usvm.api.makeSymbolicPrimitive import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.state.TsState -import org.usvm.machine.types.mkFakeValue +import org.usvm.machine.types.mkInitialFakeValue import org.usvm.sizeSort import org.usvm.ts.pbt.backend.ProjectionLevel import org.usvm.ts.pbt.mapping.EtsInputBinding @@ -236,8 +236,7 @@ class UsvmDomainProjector( return@with sameSortIte(chooseValue, nestedValue, nilValue) } - val fakeValue = state.mkFakeValue( - scope = null, + val fakeValue = state.mkInitialFakeValue( boolValue = nestedValue.asOptionalBool(), fpValue = nestedValue.asOptionalFp(), refValue = (nestedValue.asOptionalRef() ?: nilValue.asOptionalRef()), @@ -371,8 +370,7 @@ class UsvmDomainProjector( private fun box(value: UExpr): UConcreteHeapRef = with(state.ctx) { if (value is UConcreteHeapRef && value.isFakeObject()) return@with value - state.mkFakeValue( - scope = null, + state.mkInitialFakeValue( boolValue = value.asOptionalBool(), fpValue = value.asOptionalFp(), refValue = value.asOptionalRef(), diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt index 715799695d..84ad71f408 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt @@ -34,7 +34,7 @@ fun mockMethodCall( method: EtsMethodSignature, resultType: EtsType = method.returnType, ) { - val result = makeFreshUnknownCallResult(scope, resultType) + val result = makeFreshUnknownCallResult(scope, resultType) ?: return scope.doWithState { setMockMethodCallResult(method, result) @@ -50,7 +50,7 @@ internal fun TsState.setMockMethodCallResult( } /** Native Date construction retains its allocated identity even when its timestamp is opaque. */ -internal fun makeFreshUnknownCallResult(scope: TsStepScope, call: TsUnknownCall): UExpr<*> { +internal fun makeFreshUnknownCallResult(scope: TsStepScope, call: TsUnknownCall): UExpr<*>? { val date = scope.calcOnState { intrinsicDateConstructorReceiver(call) } if (date == null) return makeFreshUnknownCallResult(scope, call.resultType) @@ -65,7 +65,7 @@ internal fun makeFreshUnknownCallResult(scope: TsStepScope, call: TsUnknownCall) internal fun makeFreshUnknownCallResult( scope: TsStepScope, resultType: EtsType, -): UExpr<*> = scope.calcOnState { +): UExpr<*>? = scope.calcOnState { if (resultType is EtsVoidType) return@calcOnState ctx.mkUndefinedValue() val literal = makeLiteralResult(resultType) if (literal != null) return@calcOnState literal @@ -120,7 +120,7 @@ private fun TsState.makeLiteralResult(type: EtsType): UExpr<*>? = when (type) { else -> null } -private fun TsState.makeFiniteLiteralUnion(scope: TsStepScope, variants: List): UExpr<*> { +private fun TsState.makeFiniteLiteralUnion(scope: TsStepScope, variants: List): UExpr<*>? { var result = requireNotNull(makeLiteralResult(variants.first())) for (variant in variants.drop(1)) { val selected = makeSymbolicPrimitive(ctx.boolSort) @@ -130,7 +130,7 @@ private fun TsState.makeFiniteLiteralUnion(scope: TsStepScope, variants: List false } - fun UExpr<*>.toFakeObject(scope: TsStepScope): UConcreteHeapRef { + fun UExpr<*>.toFakeObject(scope: TsStepScope): UConcreteHeapRef? { if (isFakeObject()) { return this } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt index 3abdbba2f7..5255f494d8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt @@ -74,7 +74,7 @@ class TsModelUnknownCallDispatcher( } TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> { - val result = makeFreshUnknownCallResult(scope, call) + val result = makeFreshUnknownCallResult(scope, call) ?: return TsUnknownCallOutcome.PATH_STOPPED scope.doWithState { setMockMethodCallResult(call.callee, result) newStmt(call.callSite) @@ -98,7 +98,7 @@ class TsModelUnknownCallDispatcher( val freshResidualResult = if ( residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN ) { - makeFreshUnknownCallResult(scope, call) + makeFreshUnknownCallResult(scope, call) ?: return TsUnknownCallOutcome.PATH_STOPPED } else { null } @@ -117,9 +117,10 @@ class TsModelUnknownCallDispatcher( val completion = successor.completion as? TsUnknownCallModelCompletion.Unresolved ?: return@map null - scope.calcOnState { + val result = scope.calcOnState { mkFakeValue(scope = scope, value = completion.value) - } + } ?: return TsUnknownCallOutcome.PATH_STOPPED + result } val guardedStateChanges = application.execution.successors.mapIndexed { index, successor -> successor.guard to modelStateChange( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt index 7eba4f05e6..b66dcd8898 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt @@ -135,13 +135,13 @@ private fun TsExprResolver.advanceArrayIterator( val value = if (done.isTrue) { mkUndefinedValue() } else { - val element = readArrayElement(scope, iterator.array, iterator.index, iterator.arrayType) + val element = readArrayElement(scope, iterator.array, iterator.index, iterator.arrayType) ?: return null iteWriteIntoFakeObject( scope = scope, condition = done, trueBranchValue = mkUndefinedValue(), falseBranchValue = element, - ) + ) ?: return null } scope.calcOnState { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 59788d82b3..160e341659 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -668,7 +668,7 @@ private fun TsExprResolver.removeArrayElement( scope.calcOnState { val newLength = mkBvSubExpr(length, mkBv(1)) val index = if (first) mkBv(0) else newLength - val removed = readArrayElement(scope, array, index, arrayType) + val removed = readArrayElement(scope, array, index, arrayType) ?: return@calcOnState null if (first) { copyArrayElements( @@ -730,10 +730,14 @@ private fun TsExprResolver.handleArrayFill( val containsFakeValue = resolvedValue.sort == addressSort && resolvedValue.asExpr(addressSort).hasFakeValueBranch() val usesBoxedValue = hasResolvedElementSort && (!valueMatchesElementSort || containsFakeValue) - val boxedValue = if (usesBoxedValue) boxArrayValue(scope, resolvedValue) else null + val boxedValue = if (usesBoxedValue) { + boxArrayValue(scope, resolvedValue) ?: return null + } else { + null + } val nativeValue = when { - !hasResolvedElementSort -> resolvedValue.toFakeObject(scope) + !hasResolvedElementSort -> resolvedValue.toFakeObject(scope) ?: return null !usesBoxedValue -> resolvedValue elementSort == boolSort -> falseExpr elementSort == fp64Sort -> mkFp64(0.0) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt index 00b6b981c9..2f74fcbf42 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt @@ -112,9 +112,9 @@ internal fun TsContext.writeModeledErrorField( instance: UHeapRef, field: EtsFieldSignature, value: UExpr<*>, -): Boolean { +): Boolean? { val storageField = resolveErrorStorageField(scope, instance, field) ?: return false - val payload = boxArrayValue(scope, value) + val payload = boxArrayValue(scope, value) ?: return null scope.doWithState { memory.write( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt index b2744e5d02..9d87fc81ae 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt @@ -127,7 +127,7 @@ private fun TsContext.readArrayProperty( return mkUndefinedValue() } - val element = readArrayElement(scope, array, index, arrayType) + val element = readArrayElement(scope, array, index, arrayType) ?: return null if (elementExists.isTrue) { return element } @@ -145,11 +145,11 @@ internal fun TsContext.readArrayElement( array: UHeapRef, index: UExpr, arrayType: EtsArrayType, -): UExpr<*> { +): UExpr<*>? { val present = scope.calcOnState { knownArrayIndexPresence(array, index) } if (present?.isFalse == true) return mkUndefinedValue() - val element = readArrayElementPayload(scope, array, index, arrayType) + val element = readArrayElementPayload(scope, array, index, arrayType) ?: return null if (present == null || present.isTrue) return element return iteWriteIntoFakeObject( @@ -165,7 +165,7 @@ private fun TsContext.readArrayElementPayload( array: UHeapRef, index: UExpr, arrayType: EtsArrayType, -): UExpr<*> { +): UExpr<*>? { // Determine the element sort. val sort = typeToSort(arrayType.componentType) @@ -183,7 +183,7 @@ private fun TsContext.readArrayElementPayload( return scope.calcOnState { val value = readUnresolvedArrayElement(memory, array, index) - val fakeObj = mkFakeValue(scope = scope, value = value) + val fakeObj = mkFakeValue(scope = scope, value = value) ?: return@calcOnState null if (fakeObj != value.refValue) { val refLValue = mkArrayIndexLValue(addressSort, array, index, arrayType) memory.write(refLValue, fakeObj, guard = trueExpr) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index ea355e2842..3f46417f9a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -191,12 +191,12 @@ private fun TsContext.resolveDeclaredField( scope.assert(fieldExists) ?: return null } - val storedValue = readField(scope, instance, field, storageSort) + val storedValue = readField(scope, instance, field, storageSort) ?: return null val value = materializeFieldValue(scope, storedValue, storageSort, declaredType) ?: return null return applyFieldDeletion(scope, deleted, value) } -private fun TsContext.applyFieldDeletion(scope: TsStepScope, deleted: UBoolExpr, value: UExpr<*>): UExpr<*> { +private fun TsContext.applyFieldDeletion(scope: TsStepScope, deleted: UBoolExpr, value: UExpr<*>): UExpr<*>? { if (deleted.isFalse) return value // Conditional deletion yields undefined on the deleted branch, while preserving the stored runtime kind. @@ -349,7 +349,7 @@ private fun TsContext.readField( instance: UHeapRef, field: EtsFieldSignature, sort: USort, -): UExpr<*> { +): UExpr<*>? { if (sort !is TsUnresolvedSort) { val lValue = mkFieldLValue(sort, instance, field.name) return scope.calcOnState { memory.read(lValue) } @@ -370,7 +370,7 @@ private fun TsContext.readField( if (ref.hasFakeValueBranch()) { boxRuntimeValue(scope = scope, value = ref) } else { - val fakeObj = mkFakeValue(scope, bool, fp, ref) + val fakeObj = mkFakeValue(scope, bool, fp, ref) ?: return@calcOnState null lValuesToAllocatedFakeObjects += refLValue to fakeObj memory.write(refLValue, fakeObj, guard = trueExpr) fakeObj diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index daf6d969f6..9da950ce8e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -1376,7 +1376,7 @@ class TsExprResolver( "Promise settlement callback should have exactly one argument, but got ${expr.args.size}" } val value = resolve(expr.args.single()) ?: return null - val fakeValue = value.toFakeObject(scope) + val fakeValue = value.toFakeObject(scope) ?: return null scope.doWithState { if (!isResolved(callback.promise)) { markResolved(callback.promise) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt index 30835f1d42..6a980ad32a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt @@ -196,7 +196,7 @@ fun TsContext.assignToArrayIndex( } } - val fake = boxArrayValue(scope, expr) + val fake = boxArrayValue(scope, expr) ?: return null val kind = fake.getFakeType(scope) val compatibleKind = when (elementSort) { boolSort -> kind.boolTypeExpr @@ -231,7 +231,7 @@ fun TsContext.assignToArrayIndex( index = index.asExpr(sizeSort), type = arrayType, ) - val fakeExpr = boxArrayValue(scope, expr) + val fakeExpr = boxArrayValue(scope, expr) ?: return null return scope.doWithState { memory.write(lValue, fakeExpr, guard = trueExpr) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index 36c411a7ed..947b391258 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt @@ -231,6 +231,7 @@ fun TsContext.assignToInstanceField( field = field, value = expr, ) + if (wroteModeledErrorField == null) return null if (wroteModeledErrorField) return Unit val objectLiteralClass = objectLiteralClass(scope, unwrappedInstance, hierarchy) @@ -273,9 +274,14 @@ fun TsContext.assignToInstanceField( // If the field type is unknown, we create a fake object for the expr and assign it. // Otherwise, assign expr directly. + val fakeObject = if (sort is TsUnresolvedSort) { + boxRuntimeValue(scope = scope, value = expr) ?: return null + } else { + null + } + return scope.doWithState { - if (sort is TsUnresolvedSort) { - val fakeObject = boxRuntimeValue(scope = scope, value = expr) + if (fakeObject != null) { val lValue = mkFieldLValue(addressSort, unwrappedInstance, field) lValuesToAllocatedFakeObjects += lValue to fakeObject memory.write(lValue, fakeObject, guard = trueExpr) @@ -375,7 +381,7 @@ fun TsContext.assignToStaticField( } return if (sort == unresolvedSort) { val lValue = mkFieldLValue(addressSort, instance, field.name) - val fakeObject = expr.toFakeObject(scope) + val fakeObject = expr.toFakeObject(scope) ?: return null scope.doWithState { lValuesToAllocatedFakeObjects += lValue to fakeObject memory.write(lValue, fakeObject, guard = trueExpr) @@ -385,7 +391,7 @@ fun TsContext.assignToStaticField( // A conditional reference can contain a fake value on only one branch. val mayContainFakeValue = expr.sort == addressSort && expr.asExpr(addressSort).hasFakeValueBranch() val value = if (mayContainFakeValue) { - expr.toFakeObject(scope) + expr.toFakeObject(scope) ?: return null } else { expr } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInitialState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInitialState.kt index 617ef1cde0..6c965334e0 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInitialState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInitialState.kt @@ -26,7 +26,7 @@ import org.usvm.machine.state.newStmt import org.usvm.machine.state.parametersWithThisCount import org.usvm.machine.state.symbolicStringBackingConstraint import org.usvm.machine.types.initialInputType -import org.usvm.machine.types.mkFakeValue +import org.usvm.machine.types.mkInitialFakeValue import org.usvm.machine.types.toAuxiliaryType import org.usvm.sizeSort import org.usvm.solver.USatResult @@ -138,8 +138,7 @@ internal fun createInitialStateOrNull( val bool = mkRegisterReading(idx, boolSort) val fp = mkRegisterReading(idx, fp64Sort) val referenceValue = mkRegisterReading(idx, addressSort) - val fakeObject = state.mkFakeValue( - scope = null, + val fakeObject = state.mkInitialFakeValue( boolValue = bool, fpValue = fp, refValue = referenceValue, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 81aa89a000..feed690fa3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -35,6 +35,7 @@ import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME import org.jacodb.ets.utils.callExpr import org.usvm.StepResult import org.usvm.StepScope +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UInterpreter import org.usvm.api.initializeArray @@ -136,7 +137,7 @@ class TsInterpreter( scope = scope, value = result.value, settlement = PromiseState.REJECTED, - ) + ) ?: return scope.stepResult() } else { null } @@ -228,7 +229,6 @@ class TsInterpreter( } private fun visitVirtualMethodCall(scope: TsStepScope, stmt: TsVirtualMethodCallStmt) = with(ctx) { - val instance = stmt.instance val callee = stmt.call.callee @@ -424,7 +424,6 @@ class TsInterpreter( } private fun visitConcreteMethodCall(scope: TsStepScope, stmt: TsConcreteMethodCallStmt) { - // NOTE: USE '.callee' INSTEAD OF '.method' !!! // TODO: observer @@ -491,8 +490,10 @@ class TsInterpreter( } // wrap rest args in array - val content = stmt.args.drop(numNormal).map { - with(ctx) { it.toFakeObject(scope) } + val content = mutableListOf() + for (argument in stmt.args.drop(numNormal)) { + val value = with(ctx) { argument.toFakeObject(scope) } ?: return@doWithState + content += value } val array = scope.calcOnState { // In a common case we cannot determine the type of the array @@ -604,7 +605,7 @@ class TsInterpreter( scope = scope, value = value, settlement = PromiseState.FULFILLED, - ) + ) ?: return } else { value } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsPromise.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsPromise.kt index 2b3e6ae3a3..e38b70d134 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsPromise.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsPromise.kt @@ -26,7 +26,7 @@ import org.usvm.util.mkFieldLValue enum class PromiseState { PENDING, FULFILLED, - REJECTED; + REJECTED, } private val intrinsicPromiseInstanceType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "Promise")) @@ -70,11 +70,11 @@ internal fun TsContext.createSettledPromise( scope: TsStepScope, value: UExpr<*>, settlement: PromiseState, -): UConcreteHeapRef { +): UConcreteHeapRef? { require(settlement != PromiseState.PENDING) val promise = scope.calcOnState { memory.allocConcrete(intrinsicPromiseInstanceType) } - val storedValue = value.toFakeObject(scope) + val storedValue = value.toFakeObject(scope) ?: return null scope.doWithState { markResolved(promise) setPromiseState(promise, settlement) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt index e4cf268059..b8f2ae9e9f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt @@ -33,13 +33,13 @@ import org.usvm.memory.ULValue * execution a live scope is required so that adding the exactly-one constraint also checks satisfiability and updates * the state's models. */ -fun TsState.mkFakeValue( +private fun TsState.createFakeValue( scope: TsStepScope?, // pass `null` only in the initial state, where `scope` is not available! boolValue: UBoolExpr? = null, fpValue: UExpr? = null, refValue: UHeapRef? = null, valueType: EtsFakeType? = null, -): UConcreteHeapRef = with(ctx) { +): UConcreteHeapRef? = with(ctx) { require(boolValue != null || fpValue != null || refValue != null) { "Fake object should contain at least one value" } @@ -64,14 +64,15 @@ fun TsState.mkFakeValue( makeSymbolicPrimitive(boolSort) }, ) - memory.types.allocate(address, type) val constraint = type.mkExactlyOneTypeConstraint(ctx) if (scope != null) { - scope.assert(constraint) + scope.assert(constraint) ?: return@with null } else { pathConstraints += constraint } + memory.types.allocate(address, type) + if (boolValue != null) { val boolLValue = ctx.getIntermediateBoolLValue(address) memory.write(boolLValue, boolValue, guard = ctx.trueExpr) @@ -92,16 +93,35 @@ fun TsState.mkFakeValue( fakeValueRef } +/** Initial construction only adds constraints; no live step scope or solver model exists yet. */ +fun TsState.mkInitialFakeValue( + boolValue: UBoolExpr? = null, + fpValue: UExpr? = null, + refValue: UHeapRef? = null, + valueType: EtsFakeType? = null, +): UConcreteHeapRef = checkNotNull( + createFakeValue(scope = null, boolValue = boolValue, fpValue = fpValue, refValue = refValue, valueType = valueType) +) + +/** A failed live exactly-one assertion stops materialization and must propagate to the interpreter. */ +fun TsState.mkFakeValue( + scope: TsStepScope, + boolValue: UBoolExpr? = null, + fpValue: UExpr? = null, + refValue: UHeapRef? = null, + valueType: EtsFakeType? = null, +): UConcreteHeapRef? = createFakeValue(scope, boolValue, fpValue, refValue, valueType) + fun TsState.mkFakeValue( scope: TsStepScope, value: TsUnresolvedValue, -): UConcreteHeapRef = materializeFakeValue(scope, value, value.refValue) +): UConcreteHeapRef? = materializeFakeValue(scope, value, value.refValue) private fun TsState.materializeFakeValue( scope: TsStepScope, value: TsUnresolvedValue, refValue: UHeapRef, -): UConcreteHeapRef = with(ctx) { +): UConcreteHeapRef? = with(ctx) { when { refValue.isFakeObject() -> refValue @@ -115,7 +135,9 @@ private fun TsState.materializeFakeValue( refValue is UIteExpr<*> -> { val trueValue = materializeFakeValue(scope, value, refValue.trueBranch.asExpr(addressSort)) + ?: return@with null val falseValue = materializeFakeValue(scope, value, refValue.falseBranch.asExpr(addressSort)) + ?: return@with null iteWriteIntoFakeObject( scope = scope, @@ -177,7 +199,7 @@ fun TsContext.iteWriteIntoFakeObject( condition: UBoolExpr, trueBranchValue: UExpr, falseBranchValue: UExpr, -): UConcreteHeapRef = scope.calcOnState { +): UConcreteHeapRef? = scope.calcOnState { val (boolRValueTrueBranch, boolTrueBranchCondition) = extractValue( trueBranchValue, ctx.boolSort, @@ -211,6 +233,13 @@ fun TsContext.iteWriteIntoFakeObject( ::getIntermediateRefLValue ) + val fakeType = EtsFakeType( + boolTypeExpr = mkIte(condition, boolTrueBranchCondition, boolFalseBranchCondition), + fpTypeExpr = mkIte(condition, fpValueTrueBranchCondition, fpValueFalseBranchCondition), + refTypeExpr = mkIte(condition, refValueTrueBranchCondition, refValueFalseBranchCondition) + ) + scope.assert(fakeType.mkExactlyOneTypeConstraint(ctx)) ?: return@calcOnState null + val fakeObject = createFakeObjectRef() val boolLValue = getIntermediateBoolLValue(fakeObject.address) @@ -221,14 +250,6 @@ fun TsContext.iteWriteIntoFakeObject( writeValuesWithGuard(fpRValueTrueBranch, fpRValueFalseBranch, fpLValue, condition) writeValuesWithGuard(refRValueTrueBranch, refRValueFalseBranch, refLValue, condition) - val fakeType = EtsFakeType( - boolTypeExpr = mkIte(condition, boolTrueBranchCondition, boolFalseBranchCondition), - fpTypeExpr = mkIte(condition, fpValueTrueBranchCondition, fpValueFalseBranchCondition), - refTypeExpr = mkIte(condition, refValueTrueBranchCondition, refValueFalseBranchCondition) - ).also { - scope.assert(it.mkExactlyOneTypeConstraint(ctx)) - } - memory.types.allocate(fakeObject.address, fakeType) fakeObject diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/TypedArrayStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/TypedArrayStorage.kt index ba019fb896..b64c5dc461 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/TypedArrayStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/TypedArrayStorage.kt @@ -95,7 +95,7 @@ internal fun TsState.initializeTypedArrayOverrides(array: UHeapRef) = with(ctx) initializedTypedArrayOverrides += array } -internal fun TsContext.boxArrayValue(scope: TsStepScope, value: UExpr<*>): UConcreteHeapRef { +internal fun TsContext.boxArrayValue(scope: TsStepScope, value: UExpr<*>): UConcreteHeapRef? { val containsFakeValue = value.sort == addressSort && value.asExpr(addressSort).hasFakeValueBranch() if (!containsFakeValue) return value.toFakeObject(scope) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt index 51faff657a..9d20d16949 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt @@ -57,7 +57,7 @@ fun EtsType.getClassesForType( fun UHeapRef.createFakeField( scope: TsStepScope, fieldName: String, -): UConcreteHeapRef = with(tctx) { +): UConcreteHeapRef? = with(tctx) { val lValue = mkFieldLValue(addressSort, this@createFakeField, fieldName) val boolLValue = mkFieldLValue(boolSort, this@createFakeField, fieldName) @@ -73,7 +73,7 @@ fun UHeapRef.createFakeField( } scope.calcOnState { - val fakeObject = mkFakeValue(scope, bool, fp, ref) + val fakeObject = mkFakeValue(scope, bool, fp, ref) ?: return@calcOnState null memory.write(lValue, fakeObject.asExpr(ctx.addressSort), guard = ctx.trueExpr) fakeObject } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsContextFactoryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsContextFactoryTest.kt index 975e62fc60..fdaf662217 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsContextFactoryTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsContextFactoryTest.kt @@ -24,7 +24,7 @@ import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsState import org.usvm.machine.types.EtsFakeType import org.usvm.machine.types.TsTypeSystem -import org.usvm.machine.types.mkFakeValue +import org.usvm.machine.types.mkInitialFakeValue import org.usvm.sizeSort import org.usvm.util.EtsHierarchy import org.usvm.util.copyArrayElements @@ -35,6 +35,7 @@ import kotlin.test.assertFailsWith import kotlin.test.assertFalse import kotlin.test.assertIs import kotlin.test.assertNotEquals +import kotlin.test.assertNotNull import kotlin.test.assertSame import kotlin.test.assertTrue import kotlin.time.Duration.Companion.seconds @@ -66,7 +67,7 @@ class TsContextFactoryTest { state.memory.types.allocate(highOrdinaryRef.address, EtsNumberType) val payload = mkFp64(7.0) - val fakeRef = state.mkFakeValue(scope = null, fpValue = payload) + val fakeRef = state.mkInitialFakeValue(fpValue = payload) val nextOrdinaryRef = state.memory.allocConcrete(EtsNumberType) assertFalse(highOrdinaryRef.isFakeObject()) @@ -86,12 +87,12 @@ class TsContextFactoryTest { val selected = mkRegisterReading(idx = 0, sort = boolSort) val trueNumber = mkFp64(7.0) val falseNumber = mkFp64(11.0) - val trueWrapper = state.mkFakeValue(scope = null, fpValue = trueNumber, valueType = EtsFakeType.mkFp(ctx)) - val falseWrapper = state.mkFakeValue(scope = null, fpValue = falseNumber, valueType = EtsFakeType.mkFp(ctx)) + val trueWrapper = state.mkInitialFakeValue(fpValue = trueNumber, valueType = EtsFakeType.mkFp(ctx)) + val falseWrapper = state.mkInitialFakeValue(fpValue = falseNumber, valueType = EtsFakeType.mkFp(ctx)) val conditional = mkIte(selected, trueWrapper, falseWrapper) assertIs>(conditional) - val boxed = conditional.toFakeObject(scope) + val boxed = assertNotNull(conditional.toFakeObject(scope)) val kind = boxed.getFakeType(state.memory) val payload = boxed.extractFp(state.memory) @@ -108,15 +109,13 @@ class TsContextFactoryTest { val zero = mkFp64(0.0) val undefined = mkUndefinedValue() val reference = mkTsNullValue() - val numberWrapper = state.mkFakeValue( - scope = null, + val numberWrapper = state.mkInitialFakeValue( boolValue = falseExpr, fpValue = number, refValue = undefined, valueType = EtsFakeType.mkFp(ctx), ) - val referenceWrapper = state.mkFakeValue( - scope = null, + val referenceWrapper = state.mkInitialFakeValue( boolValue = falseExpr, fpValue = zero, refValue = reference, @@ -125,7 +124,7 @@ class TsContextFactoryTest { val conditional = mkIte(selected, numberWrapper, referenceWrapper) assertIs>(conditional) - val boxed = conditional.toFakeObject(scope) + val boxed = assertNotNull(conditional.toFakeObject(scope)) val kind = boxed.getFakeType(state.memory) val numberPayload = boxed.extractFp(state.memory) val referencePayload = boxed.extractRef(state.memory) @@ -146,15 +145,13 @@ class TsContextFactoryTest { val zero = mkFp64(0.0) val undefined = mkUndefinedValue() val reference = mkTsNullValue() - val numberWrapper = state.mkFakeValue( - scope = null, + val numberWrapper = state.mkInitialFakeValue( boolValue = falseExpr, fpValue = number, refValue = undefined, valueType = EtsFakeType.mkFp(ctx), ) - val boolWrapper = state.mkFakeValue( - scope = null, + val boolWrapper = state.mkInitialFakeValue( boolValue = trueExpr, fpValue = zero, refValue = undefined, @@ -163,7 +160,7 @@ class TsContextFactoryTest { val conditional = mkIte(outer, mkIte(inner, numberWrapper, boolWrapper), reference) assertIs>(conditional) - val boxed = conditional.toFakeObject(scope) + val boxed = assertNotNull(conditional.toFakeObject(scope)) val kind = boxed.getFakeType(state.memory) val numberPayload = boxed.extractFp(state.memory) val referencePayload = boxed.extractRef(state.memory) @@ -178,21 +175,19 @@ class TsContextFactoryTest { @Test fun `boxing a direct wrapper preserves its identity`() = with(ctx) { - val wrapper = state.mkFakeValue( - scope = null, + val wrapper = state.mkInitialFakeValue( fpValue = mkFp64(7.0), valueType = EtsFakeType.mkFp(ctx), ) - val boxed = wrapper.toFakeObject(scope) + val boxed = assertNotNull(wrapper.toFakeObject(scope)) assertSame(wrapper, boxed) } @Test fun `boxing ordinary references ignores wrappers used only in the condition`() = with(ctx) { - val wrapper = state.mkFakeValue( - scope = null, + val wrapper = state.mkInitialFakeValue( fpValue = mkFp64(7.0), valueType = EtsFakeType.mkFp(ctx), ) @@ -202,7 +197,7 @@ class TsContextFactoryTest { val conditional = mkIte(selected, mkTsNullValue(), mkUndefinedValue()) assertIs>(conditional) - val boxed = conditional.toFakeObject(scope) + val boxed = assertNotNull(conditional.toFakeObject(scope)) val kind = boxed.getFakeType(state.memory) val payload = boxed.extractRef(state.memory) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineFailurePrefixTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineFailurePrefixTest.kt index a92c330a3f..f3109422b6 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineFailurePrefixTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineFailurePrefixTest.kt @@ -55,7 +55,7 @@ class TsMachineFailurePrefixTest { assertFalse(result.engineFailed) assertTrue(result.runtimeLimited) assertTrue(result.states.isEmpty()) - assertTrue(result.unsupportedPaths.any { "GLOBAL_BINDING_NOT_MODELED" in it && "Math" in it }) + assertTrue(result.unsupportedPaths.any { "GLOBAL_BINDING_NOT_MODELED" in it && "Reflect" in it }) assertTrue(prefixes.isNotEmpty()) assertTrue(prefixes.all { !it.pathConstraints.isFalse && it.models.isNotEmpty() }) assertTrue(prefixes.all { it.unsupportedReason != null && it.engineFailureReason == null }) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ExprUtilConditionalValueTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ExprUtilConditionalValueTest.kt index b9175b94a7..ffbd7c9d0b 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ExprUtilConditionalValueTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ExprUtilConditionalValueTest.kt @@ -20,7 +20,7 @@ import org.usvm.machine.operator.TsUnaryOperator import org.usvm.machine.state.TsState import org.usvm.machine.types.EtsFakeType import org.usvm.machine.types.TsTypeSystem -import org.usvm.machine.types.mkFakeValue +import org.usvm.machine.types.mkInitialFakeValue import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.URegistersStack import org.usvm.solver.USatResult @@ -95,13 +95,11 @@ class ExprUtilConditionalValueTest { fun `nested wrapper results retain truthiness nullish and numeric selection`() = with(ctx) { val outer = mkRegisterReading(idx = 0, sort = boolSort) val inner = mkRegisterReading(idx = 1, sort = boolSort) - val booleanWrapper = state.mkFakeValue( - scope = null, + val booleanWrapper = state.mkInitialFakeValue( boolValue = trueExpr, valueType = EtsFakeType.mkBool(ctx), ) - val numberWrapper = state.mkFakeValue( - scope = null, + val numberWrapper = state.mkInitialFakeValue( fpValue = mkFp64(0.0), valueType = EtsFakeType.mkFp(ctx), ) @@ -121,8 +119,7 @@ class ExprUtilConditionalValueTest { @Test fun `wrappers used only by a guard are not conditional result wrappers`() = with(ctx) { - val wrapper = state.mkFakeValue( - scope = null, + val wrapper = state.mkInitialFakeValue( fpValue = mkFp64(7.0), valueType = EtsFakeType.mkFp(ctx), ) @@ -171,8 +168,7 @@ class ExprUtilConditionalValueTest { fun `inactive unmodeled reference payload does not reject a numeric wrapper`() = with(ctx) { val number = mkFp64(7.0) val unmodeledObject = state.memory.allocConcrete(EtsAnyType) - val wrapper = state.mkFakeValue( - scope = null, + val wrapper = state.mkInitialFakeValue( fpValue = number, refValue = unmodeledObject, valueType = EtsFakeType.mkFp(ctx), @@ -190,9 +186,8 @@ class ExprUtilConditionalValueTest { val selected = mkRegisterReading(idx = 0, sort = boolSort) val number = mkFp64(7.0) val unmodeledObject = state.memory.allocConcrete(EtsAnyType) - val numberWrapper = state.mkFakeValue(scope = null, fpValue = number, valueType = EtsFakeType.mkFp(ctx)) - val referenceWrapper = state.mkFakeValue( - scope = null, + val numberWrapper = state.mkInitialFakeValue(fpValue = number, valueType = EtsFakeType.mkFp(ctx)) + val referenceWrapper = state.mkInitialFakeValue( refValue = unmodeledObject, valueType = EtsFakeType.mkRef(ctx), ) @@ -215,8 +210,8 @@ class ExprUtilConditionalValueTest { val selected = mkRegisterReading(idx = 0, sort = boolSort) val number = mkFp64(7.0) val string = state.mkInitializedStringConstant(value = "42") - val numberWrapper = state.mkFakeValue(scope = null, fpValue = number, valueType = EtsFakeType.mkFp(ctx)) - val stringWrapper = state.mkFakeValue(scope = null, refValue = string, valueType = EtsFakeType.mkRef(ctx)) + val numberWrapper = state.mkInitialFakeValue(fpValue = number, valueType = EtsFakeType.mkFp(ctx)) + val stringWrapper = state.mkInitialFakeValue(refValue = string, valueType = EtsFakeType.mkRef(ctx)) val conditional = mkIte(selected, numberWrapper, stringWrapper) val numeric = mkNumericExpr(conditional, scope) @@ -275,8 +270,7 @@ class ExprUtilConditionalValueTest { fpTypeExpr = mkNot(selected), refTypeExpr = falseExpr, ) - val wrapper = state.mkFakeValue( - scope = null, + val wrapper = state.mkInitialFakeValue( boolValue = trueExpr, fpValue = mkFp64(7.0), refValue = unmodeledObject, @@ -334,8 +328,7 @@ class ExprUtilConditionalValueTest { fpTypeExpr = selected, refTypeExpr = mkNot(selected), ) - val wrapper = state.mkFakeValue( - scope = null, + val wrapper = state.mkInitialFakeValue( fpValue = mkFp64(7.0), refValue = string, valueType = kinds, @@ -366,14 +359,12 @@ class ExprUtilConditionalValueTest { fpTypeExpr = leftBooleanSelected, refTypeExpr = falseExpr, ) - val left = state.mkFakeValue( - scope = null, + val left = state.mkInitialFakeValue( boolValue = trueExpr, fpValue = mkFp64(2.0), valueType = leftKinds, ) - val right = state.mkFakeValue( - scope = null, + val right = state.mkInitialFakeValue( boolValue = falseExpr, fpValue = mkFp64(1.0), valueType = rightKinds, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/types/FakeExprUtilTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/types/FakeExprUtilTest.kt index 76354377dd..81f0615db3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/types/FakeExprUtilTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/types/FakeExprUtilTest.kt @@ -9,6 +9,7 @@ import org.usvm.UMachineOptions import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.machine.TsComponents import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsState import org.usvm.util.EtsHierarchy import kotlin.test.assertEquals @@ -42,13 +43,11 @@ class FakeExprUtilTest { val selected = mkRegisterReading(idx = 0, sort = boolSort) val trueNumber = mkFp64(7.0) val falseNumber = mkFp64(11.0) - val trueWrapper = state.mkFakeValue( - scope = null, + val trueWrapper = state.mkInitialFakeValue( fpValue = trueNumber, valueType = EtsFakeType.mkFp(ctx), ) - val falseWrapper = state.mkFakeValue( - scope = null, + val falseWrapper = state.mkInitialFakeValue( fpValue = falseNumber, valueType = EtsFakeType.mkFp(ctx), ) @@ -65,14 +64,12 @@ class FakeExprUtilTest { @Test fun `mixed wrappers retain complementary kinds without wrapper reference payloads`() = with(ctx) { val selected = mkRegisterReading(idx = 0, sort = boolSort) - val numberWrapper = state.mkFakeValue( - scope = null, + val numberWrapper = state.mkInitialFakeValue( fpValue = mkFp64(7.0), valueType = EtsFakeType.mkFp(ctx), ) val reference = mkTsNullValue() - val referenceWrapper = state.mkFakeValue( - scope = null, + val referenceWrapper = state.mkInitialFakeValue( refValue = reference, valueType = EtsFakeType.mkRef(ctx), ) @@ -90,8 +87,7 @@ class FakeExprUtilTest { fun `one available payload remains protected by the selected branch guard`() = with(ctx) { val selected = mkRegisterReading(idx = 0, sort = boolSort) val number = mkFp64(7.0) - val wrapper = state.mkFakeValue( - scope = null, + val wrapper = state.mkInitialFakeValue( fpValue = number, valueType = EtsFakeType.mkFp(ctx), ) @@ -115,13 +111,11 @@ class FakeExprUtilTest { val outer = mkRegisterReading(idx = 0, sort = boolSort) val inner = mkRegisterReading(idx = 1, sort = boolSort) val number = mkFp64(7.0) - val numberWrapper = state.mkFakeValue( - scope = null, + val numberWrapper = state.mkInitialFakeValue( fpValue = number, valueType = EtsFakeType.mkFp(ctx), ) - val boolWrapper = state.mkFakeValue( - scope = null, + val boolWrapper = state.mkInitialFakeValue( boolValue = trueExpr, valueType = EtsFakeType.mkBool(ctx), ) @@ -140,8 +134,7 @@ class FakeExprUtilTest { @Test fun `ordinary reference alternatives ignore wrappers used only by the guard`() = with(ctx) { - val wrapper = state.mkFakeValue( - scope = null, + val wrapper = state.mkInitialFakeValue( fpValue = mkFp64(7.0), valueType = EtsFakeType.mkFp(ctx), ) @@ -159,4 +152,25 @@ class FakeExprUtilTest { assertNull(number) assertEquals(falseExpr, numberKind) } + + @Test + fun `live fake construction stops after rejected exactly one constraint`() = with(ctx) { + val scope = TsStepScope(originalState = state, forkBlackList = mockk()) + val invalidType = EtsFakeType(boolTypeExpr = trueExpr, fpTypeExpr = trueExpr, refTypeExpr = falseExpr) + + val value = state.mkFakeValue(scope = scope, boolValue = trueExpr, valueType = invalidType) + + assertNull(value) + assertFalse(scope.stepResult().originalStateAlive) + } + + @Test + fun `live fake construction retains a satisfiable payload`() = with(ctx) { + val scope = TsStepScope(originalState = state, forkBlackList = mockk()) + + val value = state.mkFakeValue(scope = scope, fpValue = mkFp64(17.0), valueType = EtsFakeType.mkFp(ctx)) + + val wrapper = assertNotNull(value) + assertEquals(mkFp64(17.0), state.memory.read(getIntermediateFpLValue(wrapper.address))) + } } diff --git a/usvm-ts/src/test/resources/models/UnmodeledGlobalBinding.ts b/usvm-ts/src/test/resources/models/UnmodeledGlobalBinding.ts index 6dd7305e5d..5dbffc57ba 100644 --- a/usvm-ts/src/test/resources/models/UnmodeledGlobalBinding.ts +++ b/usvm-ts/src/test/resources/models/UnmodeledGlobalBinding.ts @@ -1,7 +1,7 @@ -const nativeMath = Math; +const nativeReflect = Reflect; export class UnmodeledGlobalBinding { read(): any { - return nativeMath; + return nativeReflect; } } From de732a83ae602a772229161d197745c04f905519 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 22:43:41 +0300 Subject: [PATCH 2/3] Test boxed registry identity with explicit branch domains --- .../calls/CallsClassDataRegistryOracleTest.kt | 50 ++++++++++++------- 1 file changed, 32 insertions(+), 18 deletions(-) diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt index f575a1071f..f4b5a58a94 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt @@ -4,6 +4,7 @@ import org.junit.jupiter.api.io.TempDir import org.usvm.SolverType import org.usvm.ts.pbt.model.ArrayDomain import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.ConstantDomain import org.usvm.ts.pbt.model.IntegerDomain import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.NumberDomain @@ -219,28 +220,41 @@ class CallsClassDataRegistryOracleTest { constructorInputs = listOf(PropertyInput(name = "flag", domain = BooleanDomain)), ) - val result = CurrentTsCallsClassCoverageEngine().search( - CallsClassSearchRequest( - harness = harness, - profile = CallsExperimentProfile.EMPTY_STOP, - frozenModelIds = emptySet(), - expectedNativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision, - seed = 1, - budget = 3.seconds, - timeQuantum = 100.milliseconds, - solverQueryLimit = 1.seconds, - solverType = SolverType.YICES, - candidateCap = 20, - requireEntryPointWitness = true, - ), - ) + // Coverage-directed search need not enumerate every input model for each entry point. + val branchInputs = listOf(JsConcreteValue.Boolean(true), JsConcreteValue.Boolean(false)) + val candidates = branchInputs.flatMap { flag -> + val inputs = listOf(PropertyInput(name = "flag", domain = ConstantDomain(flag))) + val branchHarness = harness.copy( + surface = harness.surface.copy(constructorInputs = inputs), + functions = harness.functions.map { it.copy(inputs = inputs) }, + ) + val result = CurrentTsCallsClassCoverageEngine().search( + CallsClassSearchRequest( + harness = branchHarness, + profile = CallsExperimentProfile.EMPTY_STOP, + frozenModelIds = emptySet(), + expectedNativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision, + seed = 1, + budget = 3.seconds, + timeQuantum = 100.milliseconds, + solverQueryLimit = 1.seconds, + solverType = SolverType.YICES, + candidateCap = 20, + requireEntryPointWitness = true, + ), + ) + + val scenarioIds = result.search.candidates.map { it.entryPointId }.toSet() + assertEquals(harness.scenarios.map { it.id }.toSet(), scenarioIds, "flag=$flag") + result.search.candidates.forEach { assertEquals(listOf(flag), it.inputs) } + result.search.candidates + } val constructorScenarioId = harness.scenarios.first().id - val constructorBranches = result.search.candidates.filter { it.entryPointId == constructorScenarioId } + val constructorBranches = candidates.filter { it.entryPointId == constructorScenarioId } .map { it.inputs.single() }.toSet() assertEquals(setOf(JsConcreteValue.Boolean(true), JsConcreteValue.Boolean(false)), constructorBranches) - assertEquals(harness.scenarios.map { it.id }.toSet(), result.search.candidates.map { it.entryPointId }.toSet()) - for (candidate in result.search.candidates) { + for (candidate in candidates) { val index = harness.scenarios.indexOfFirst { it.id == candidate.entryPointId } val original = OriginalTypeScriptClassReplayer( directory, From ce0f38839f20bdc6176155638bef27fce008be0f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 23:37:34 +0300 Subject: [PATCH 3/3] Check untyped coercion through bounded numeric and boolean callers --- .../org/usvm/samples/lang/TypeCoercion.kt | 73 +++++++++++++++++-- .../resources/samples/lang/TypeCoercion.ts | 8 ++ 2 files changed, 76 insertions(+), 5 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/TypeCoercion.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/TypeCoercion.kt index aab7e5c3b6..5733b4e92f 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/TypeCoercion.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/TypeCoercion.kt @@ -3,18 +3,31 @@ package org.usvm.samples.lang import org.jacodb.ets.model.EtsScene import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.StateCollectionStrategy import org.usvm.api.TsTestValue import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath import org.usvm.util.isTruthy +import java.nio.file.Path +import kotlin.io.path.readText private val TsTestValue.TsBoolean.number: Double get() = if (value) 1.0 else 0.0 class TypeCoercion : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + private val tsPath = "/samples/lang/TypeCoercion.ts" override val scene: EtsScene = loadScene(tsPath) + init { + options = options.copy(stopOnCoverage = 0, stateCollectionStrategy = StateCollectionStrategy.ALL) + } + @Test fun `test argWithConst`() { val method = getMethod("argWithConst") @@ -90,12 +103,62 @@ class TypeCoercion : TsMethodTestRunner() { } @Test - fun `test transitiveCoercionNoTypes`() { - val method = getMethod("transitiveCoercionNoTypes") + fun `untyped transitive coercion retains every numeric branch`() { + val method = getMethod("transitiveCoercionNumbers") + + discoverProperties( + method = method, + { _, _, _, result -> result.number == 1.0 }, + { _, _, _, result -> result.number == 2.0 }, + { _, _, _, result -> result.number == 3.0 }, + { _, _, _, result -> result.number == 4.0 }, + invariants = arrayOf({ a, b, c, result -> + result.number == transitiveResult(a.number, b.number, c.number) + }), + ) + } + + @Test + fun `untyped transitive coercion converts boolean inputs to numbers`() { + val method = getMethod("transitiveCoercionBoolean") - discoverProperties( - method, - // Too complicated to write property matchers, examine run log to verify the test. + discoverProperties( + method = method, + { _, _, _, result -> result.number == 2.0 }, + { _, _, _, result -> result.number == 3.0 }, + { _, _, _, result -> result.number == 4.0 }, + invariants = arrayOf({ a, b, c, result -> + result.number == transitiveResult(a.number, b.number, c.number) + }), ) } + + @Test + fun `native coercion agrees with numeric and boolean branch expectations`() { + assertNodeReplay( + source = getResourcePath(tsPath).readText() + "\n" + """ + const subject = new TypeCoercion(); + const numeric = [ + [2, 2, 2, 1], [2, 2, 3, 2], [1, 2, 3, 3], [0, 0, 0, 4], + [NaN, NaN, 2, 3], [Infinity, Infinity, Infinity, 1], [-0, 0, -0, 4], + ]; + for (const [a, b, c, expected] of numeric) { + if (subject.transitiveCoercionNumbers(a, b, c) !== expected) throw Error('numeric coercion'); + } + for (const [a, b, c, expected] of [[0, false, 2, 2], [1, false, 2, 3], [0, false, 0, 4]]) { + if (subject.transitiveCoercionBoolean(a, b, c) !== expected) throw Error('boolean coercion'); + } + """.trimIndent(), + directory = directory, + name = "transitive-coercion", + timeoutMessage = "Native transitive coercion replay timed out", + ) + } + + private fun transitiveResult(a: Double, b: Double, c: Double): Double = when { + a != b -> 3.0 + c == 0.0 || c == 1.0 -> 4.0 + !c.isNaN() && a == c -> 1.0 + else -> 2.0 + } } diff --git a/usvm-ts/src/test/resources/samples/lang/TypeCoercion.ts b/usvm-ts/src/test/resources/samples/lang/TypeCoercion.ts index 79deb9040a..ba01c77b53 100644 --- a/usvm-ts/src/test/resources/samples/lang/TypeCoercion.ts +++ b/usvm-ts/src/test/resources/samples/lang/TypeCoercion.ts @@ -79,6 +79,14 @@ class TypeCoercion { return 3; } + transitiveCoercionNumbers(a: number, b: number, c: number): number { + return this.transitiveCoercionNoTypes(a, b, c); + } + + transitiveCoercionBoolean(a: number, b: boolean, c: number): number { + return this.transitiveCoercionNoTypes(a, b, c); + } + transitiveCoercionNoTypes(a, b, c): number { if (a == b) { if (c != 0 && c != 1) {