From d51f7a69e18f5be83e8f17dbda88cc50373a1688 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 7 Jul 2025 19:42:38 +0300 Subject: [PATCH 01/21] Begin AwaitExpr support --- buildSrc/src/main/kotlin/Dependencies.kt | 3 +- settings.gradle.kts | 2 +- .../ts/infer/annotation/ExprTypeAnnotator.kt | 12 +-- .../main/kotlin/org/usvm/machine/TsContext.kt | 11 +-- .../org/usvm/machine/expr/TsExprResolver.kt | 86 ++++++++++++++++++- .../usvm/machine/interpreter/TsInterpreter.kt | 61 +++++++------ .../org/usvm/machine/interpreter/TsPromise.kt | 56 ++++++++++++ .../usvm/machine/operator/TsBinaryOperator.kt | 13 ++- .../kotlin/org/usvm/machine/state/TsState.kt | 9 ++ .../kotlin/org/usvm/util/TsStateVisualizer.kt | 8 +- .../kotlin/org/usvm/project/DemoPhotos.kt | 24 ++++-- .../src/test/kotlin/org/usvm/samples/Async.kt | 33 +++++++ .../org/usvm/util/TsMethodTestRunner.kt | 9 +- usvm-ts/src/test/resources/samples/Async.ts | 16 ++++ 14 files changed, 285 insertions(+), 58 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsPromise.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt create mode 100644 usvm-ts/src/test/resources/samples/Async.ts diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 17f3f22abc..277c307ffb 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -116,7 +116,8 @@ object Libs { ) // https://github.com/UnitTestBot/jacodb - private const val jacodbPackage = "com.github.UnitTestBot.jacodb" // use "org.jacodb" with includeBuild + // private const val jacodbPackage = "com.github.UnitTestBot.jacodb" // use "org.jacodb" with includeBuild + private const val jacodbPackage = "org.jacodb" val jacodb_core = dep( group = jacodbPackage, name = "jacodb-core", diff --git a/settings.gradle.kts b/settings.gradle.kts index a0f5b624aa..10f13cd56b 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -28,7 +28,7 @@ findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons" // Actually, `includeBuild("../jacodb")` is enough, but there is a bug in IDEA when path is a symlink. // As a workaround, we convert it to a real absolute path. // See IDEA bug: https://youtrack.jetbrains.com/issue/IDEA-329756 -// includeBuild(file("../jacodb").toPath().toRealPath().toAbsolutePath()) +includeBuild(file("../jacodb").toPath().toRealPath().toAbsolutePath()) pluginManagement { resolutionStrategy { diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ExprTypeAnnotator.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ExprTypeAnnotator.kt index 671630302d..8a2e127de8 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ExprTypeAnnotator.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ExprTypeAnnotator.kt @@ -72,6 +72,8 @@ class ExprTypeAnnotator( private val valueAnnotator: ValueTypeAnnotator, ) : EtsExpr.Visitor { + private fun annotate(local: EtsLocal) = valueAnnotator.visit(local) + private fun annotate(value: EtsValue) = value.accept(valueAnnotator) private fun annotate(expr: EtsExpr) = expr.accept(this) @@ -267,8 +269,8 @@ class ExprTypeAnnotator( ) override fun visit(expr: EtsInstanceCallExpr): EtsExpr { - val baseInferred = annotate(expr.instance) as EtsLocal // safe cast - val argsInferred = expr.args.map { annotate(it) as EtsLocal } // safe cast + val baseInferred = annotate(expr.instance) + val argsInferred = expr.args.map { annotate(it) } val methodInferred = when (val baseType = baseInferred.type) { is EtsClassType -> { val etsClass = scene.projectAndSdkClasses.find { it.signature == baseType.signature } @@ -284,13 +286,13 @@ class ExprTypeAnnotator( } override fun visit(expr: EtsStaticCallExpr): EtsExpr { - val argsInferred = expr.args.map { annotate(it) as EtsLocal } // safe cast + val argsInferred = expr.args.map { annotate(it) } return expr.copy(args = argsInferred) } override fun visit(expr: EtsPtrCallExpr): EtsExpr { - val ptrInferred = annotate(expr.ptr) as EtsLocal // safe cast - val argsInferred = expr.args.map { annotate(it) as EtsLocal } // safe cast + val ptrInferred = annotate(expr.ptr) + val argsInferred = expr.args.map { annotate(it) } return expr.copy(ptr = ptrInferred, args = argsInferred) } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index f5ff13b28f..f2844f33ee 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -36,7 +36,6 @@ import org.usvm.machine.expr.TsUndefinedSort import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.expr.TsVoidSort import org.usvm.machine.expr.TsVoidValue -import org.usvm.machine.expr.tctx import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.EtsFakeType import org.usvm.memory.UReadOnlyMemory @@ -173,13 +172,12 @@ class TsContext( return this } - fun UHeapRef.unwrapRefWithPathConstraint(scope: TsStepScope): UHeapRef = with(tctx) { - if (this@unwrapRefWithPathConstraint.isFakeObject()) { + fun UHeapRef.unwrapRefWithPathConstraint(scope: TsStepScope): UHeapRef { + if (isFakeObject()) { scope.assert(getFakeType(scope).refTypeExpr) - extractRef(scope) - } else { - asExpr(addressSort) + return extractRef(scope) } + return this } fun createFakeObjectRef(): UConcreteHeapRef { @@ -274,7 +272,6 @@ class Constants { } } - enum class IntermediateLValueField { BOOL, FP, REF } 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 c0fa342030..064c493b8f 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 @@ -17,6 +17,7 @@ import org.jacodb.ets.model.EtsBitXorExpr import org.jacodb.ets.model.EtsBooleanConstant import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsCastExpr +import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsConstant import org.jacodb.ets.model.EtsDeleteExpr @@ -77,6 +78,7 @@ import org.jacodb.ets.model.EtsUnsignedRightShiftExpr import org.jacodb.ets.model.EtsValue import org.jacodb.ets.model.EtsVoidExpr import org.jacodb.ets.model.EtsYieldExpr +import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME import org.jacodb.ets.utils.getDeclaredLocals @@ -88,8 +90,8 @@ import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.UIteExpr import org.usvm.USort -import org.usvm.api.initializeArrayLength import org.usvm.api.evalTypeEquals +import org.usvm.api.initializeArrayLength import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type import org.usvm.machine.Constants @@ -98,8 +100,11 @@ import org.usvm.machine.TsContext import org.usvm.machine.TsSizeSort import org.usvm.machine.TsVirtualMethodCallStmt import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.interpreter.getResolvedValue import org.usvm.machine.interpreter.isInitialized +import org.usvm.machine.interpreter.isResolved import org.usvm.machine.interpreter.markInitialized +import org.usvm.machine.interpreter.markResolved import org.usvm.machine.operator.TsBinaryOperator import org.usvm.machine.operator.TsUnaryOperator import org.usvm.machine.state.TsMethodResult @@ -120,6 +125,7 @@ import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.mkRegisterStackLValue import org.usvm.util.resolveEtsField +import org.usvm.util.resolveEtsMethods import org.usvm.util.throwExceptionWithoutStackFrameDrop private val logger = KotlinLogging.logger {} @@ -367,9 +373,51 @@ class TsExprResolver( error("Not supported $expr") } - override fun visit(expr: EtsAwaitExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsAwaitExpr): UExpr? = with(ctx) { + val arg = resolve(expr.arg) ?: return null + + // Awaiting primitives does nothing. + if (arg.sort != addressSort) { + return arg + } + + val promise = arg.asExpr(addressSort) + + val isResolved = scope.calcOnState { isResolved(promise) } + if (!isResolved) { + // If the promise is not resolved yet, we need to call the executor to resolve it. + val executor = scope.calcOnState { + promiseExecutors[expr.arg] + ?: error("Await expression should have a promise executor, but it is not set for ${expr.arg}") + } + check(executor.cfg.stmts.isNotEmpty()) + scope.doWithState { + markResolved(promise) + pushSortsForArguments(instance = null, args = emptyList(), localToIdx) + registerCallee(currentStatement, executor.cfg) + callStack.push(executor, currentStatement) + // TODO: pass meaningful 'instance' for the executor, e.g. some static instance + val instance = mkUndefinedValue() // TODO: 'this' should not be undefined! + memory.stack.push(arrayOf(instance), executor.localsCount) + newStmt(executor.cfg.stmts.first()) + } + null + } else { + // If the promise is already resolved, we can return this value. + // val sort = typeToSort(expr.arg.type) + val sort = typeToSort(EtsUnknownType) + if (sort == unresolvedSort) { + val value = scope.calcOnState { + getResolvedValue(promise, addressSort) + } + check(value.isFakeObject()) + value + } else { + scope.calcOnState { + getResolvedValue(promise, sort) + } + } + } } override fun visit(expr: EtsYieldExpr): UExpr? { @@ -559,6 +607,9 @@ class TsExprResolver( val length = memory.read(lengthLValue) val newLength = mkBvAddExpr(length, 1.toBv()) memory.write(lengthLValue, newLength, guard = ctx.trueExpr) + if (expr.args.size != 1) { + let {} + } val resolvedArg = resolve(expr.args.single()) ?: return@calcOnState null // TODO check sorts compatibility https://github.com/UnitTestBot/usvm/issues/300 @@ -601,6 +652,33 @@ class TsExprResolver( resolved.asExpr(addressSort) } + // Handle Promise constructor + if (expr.callee.enclosingClass.name == "Promise" && expr.callee.name == CONSTRUCTOR_NAME) { + val executorLocal = expr.args.single() + val executors = resolveEtsMethods( + EtsMethodSignature( + enclosingClass = EtsClassSignature.UNKNOWN, + name = executorLocal.name, + parameters = emptyList(), + returnType = EtsUnknownType, + ) + ) + if (executors.isEmpty()) { + logger.error { "Could not resolve executor method: ${executorLocal.name}" } + scope.assert(falseExpr) + return null + } + if (executors.size > 1) { + logger.error { "Ambiguous executor method: ${executorLocal.name}, resolved ${executors.size} times" } + scope.assert(falseExpr) + return null + } + val executor = executors.single() + scope.doWithState { + setPromiseExecutor(expr.instance, executor) + } + } + val resolvedArgs = expr.args.map { resolve(it) ?: return null } val virtualCall = TsVirtualMethodCallStmt( 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 0a61c39664..2e8ee560d4 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 @@ -37,7 +37,6 @@ import org.jacodb.ets.utils.getDeclaredLocals import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UAddressSort -import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UInterpreter import org.usvm.UIteExpr @@ -78,6 +77,7 @@ import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.mkRegisterStackLValue +import org.usvm.util.renderGraph import org.usvm.util.resolveEtsField import org.usvm.util.resolveEtsMethods import org.usvm.util.type @@ -126,6 +126,7 @@ class TsInterpreter( // if no call, visit try { + state.renderGraph(view = false) when (stmt) { is TsVirtualMethodCallStmt -> visitVirtualMethodCall(scope, stmt) is TsConcreteMethodCallStmt -> visitConcreteMethodCall(scope, stmt) @@ -157,27 +158,21 @@ class TsInterpreter( // NOTE: USE '.callee' INSTEAD OF '.method' !!! val instance = requireNotNull(stmt.instance) { "Virtual code invocation with null as an instance" } - val concreteRef = scope.calcOnState { models.first().eval(instance) } - val uncoveredInstance = if (concreteRef.isFakeObject()) { + val unwrappedInstance = if (instance.isFakeObject()) { // TODO support primitives calls // We ignore the possibility of method call on primitives. // Therefore, the fake object should be unwrapped. - scope.assert(concreteRef.getFakeType(scope).refTypeExpr) - concreteRef.extractRef(scope) + scope.assert(instance.getFakeType(scope).refTypeExpr) + instance.extractRef(scope) } else { - concreteRef + instance.asExpr(addressSort) } - // Evaluate uncoveredInstance in a model to avoid too wide type streams later - val resolvedInstance = scope.calcOnState { models.first().eval(uncoveredInstance) } - val concreteMethods: MutableList = mutableListOf() - // TODO: handle 'instance.isFakeObject()' - - if (isAllocatedConcreteHeapRef(resolvedInstance)) { - val type = scope.calcOnState { memory.typeStreamOf(resolvedInstance) }.single() + if (isAllocatedConcreteHeapRef(unwrappedInstance)) { + val type = scope.calcOnState { memory.typeStreamOf(unwrappedInstance) }.single() if (type is EtsClassType) { val classes = graph.hierarchy.classesForType(type) if (classes.isEmpty()) { @@ -186,13 +181,18 @@ class TsInterpreter( return } if (classes.size > 1) { - logger.warn { "Multiple classes with name: ${type.typeName}" } - scope.assert(falseExpr) - return + logger.warn { "Multiple (${classes.size}) classes with name: ${type.typeName}" } + // scope.assert(falseExpr) + // return + for (cls in classes) { + val suitableMethods = cls.methods.filter { it.name == stmt.callee.name } + concreteMethods += suitableMethods + } + } else { + val cls = classes.single() + val suitableMethods = cls.methods.filter { it.name == stmt.callee.name } + concreteMethods += suitableMethods } - val cls = classes.single() - val suitableMethods = cls.methods.filter { it.name == stmt.callee.name } - concreteMethods += suitableMethods } else { logger.warn { "Could not resolve method: ${stmt.callee} on type: $type" @@ -213,11 +213,11 @@ class TsInterpreter( } val possibleTypes = scope.calcOnState { - models.first().typeStreamOf(resolvedInstance as UConcreteHeapRef).take(1000) + memory.typeStreamOf(unwrappedInstance).take(scene.projectAndSdkClasses.size) } if (possibleTypes !is TypesResult.SuccessfulTypesResult) { - error("TODO")// is it right? + error("TODO") // is it right? } val possibleTypesSet = possibleTypes.types.toSet() @@ -264,7 +264,7 @@ class TsInterpreter( val constraint = scope.calcOnState { val ref = stmt.instance.asExpr(addressSort) .takeIf { !it.isFakeObject() } - ?: uncoveredInstance.asExpr(addressSort) + ?: unwrappedInstance.asExpr(addressSort) // TODO: adhoc: "expand" ITE if (ref is UIteExpr<*>) { @@ -299,8 +299,15 @@ class TsInterpreter( // TODO: observer - val entryPoint = graph.entryPoints(stmt.callee).singleOrNull() + if (stmt.callee.signature.enclosingClass.name == "Log") { + mockMethodCall(scope, stmt.callee.signature) + scope.doWithState { + newStmt(stmt.returnSite) + } + return + } + val entryPoint = graph.entryPoints(stmt.callee).singleOrNull() if (entryPoint == null) { // logger.warn { "No entry point for method: ${stmt.callee}, mocking the call" } // If the method doesn't have entry points, @@ -560,13 +567,15 @@ class TsInterpreter( val instance = exprResolver.resolve(lhv.instance)?.asExpr(addressSort) ?: return@doWithState exprResolver.checkUndefinedOrNullPropertyRead(instance) ?: return@doWithState + val instanceRef = instance.unwrapRef(scope) + val etsField = resolveEtsField(lhv.instance, lhv.field, graph.hierarchy) scope.doWithState { // If we access some field, we expect that the object must have this field. // It is not always true for TS, but we decided to process it so. val supertype = EtsAuxiliaryType(properties = setOf(lhv.field.name)) // assert is required to update models - scope.assert(memory.types.evalIsSubtype(instance, supertype)) + scope.assert(memory.types.evalIsSubtype(instanceRef, supertype)) } // If there is no such field, we create a fake field for the expr @@ -578,13 +587,13 @@ class TsInterpreter( if (sort == unresolvedSort) { val fakeObject = expr.toFakeObject(scope) - val lValue = mkFieldLValue(addressSort, instance, lhv.field) + val lValue = mkFieldLValue(addressSort, instanceRef, lhv.field) lValuesToAllocatedFakeObjects += lValue to fakeObject memory.write(lValue, fakeObject, guard = trueExpr) } else { - val lValue = mkFieldLValue(sort, instance, lhv.field) + val lValue = mkFieldLValue(sort, instanceRef, lhv.field) if (lValue.sort != expr.sort) { if (expr.isFakeObject()) { val lhvType = lhv.type 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 new file mode 100644 index 0000000000..a0cc07bea6 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsPromise.kt @@ -0,0 +1,56 @@ +package org.usvm.machine.interpreter + +import org.usvm.UBoolSort +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.USort +import org.usvm.collection.field.UFieldLValue +import org.usvm.isTrue +import org.usvm.machine.TsContext +import org.usvm.machine.state.TsState +import org.usvm.util.mkFieldLValue + +internal const val RESOLVED_FIELD = "__resolved__" + +internal fun TsContext.mkResolvedField(ref: UHeapRef): UFieldLValue { + return mkFieldLValue(boolSort, ref, RESOLVED_FIELD) +} + +// TODO: this should be an extension of UHeapRef or TsContext, not TsState !!! +internal fun TsState.isResolved(promise: UHeapRef): Boolean = with(ctx) { + val resolvedField = mkResolvedField(promise) + return memory.read(resolvedField).isTrue +} + +internal fun TsState.markResolved(promise: UHeapRef) = with(ctx) { + val resolvedField = mkResolvedField(promise) + memory.write(resolvedField, trueExpr, guard = trueExpr) +} + +internal const val RESOLVED_VALUE_FIELD = "__value" + +internal fun TsContext.mkResolvedValueField( + ref: UHeapRef, + sort: Sort, +): UFieldLValue { + return mkFieldLValue(sort, ref, RESOLVED_VALUE_FIELD) +} + +// This should be an extension of TsContext, not TsState !!! +internal fun TsState.getResolvedValue( + promise: UHeapRef, + sort: Sort, +): UExpr = with(ctx) { + check(sort != unresolvedSort) + val resolvedValueField = mkResolvedValueField(promise, sort) + memory.read(resolvedValueField) +} + +internal fun TsState.setResolvedValue( + promise: UHeapRef, + value: UExpr, +) = with(ctx) { + check(value.sort != unresolvedSort) + val resolvedValueField = mkResolvedValueField(promise, value.sort) + memory.write(resolvedValueField, value, guard = trueExpr) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index f5c8be7829..76ecce7aab 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -1133,7 +1133,8 @@ sealed interface TsBinaryOperator { rhs: UHeapRef, scope: TsStepScope, ): UBoolExpr { - TODO("Not yet implemented") + // TODO: LT operator for references is not fully supported + return mkFalse() } override fun TsContext.resolveFakeObject( @@ -1141,7 +1142,8 @@ sealed interface TsBinaryOperator { rhs: UExpr<*>, scope: TsStepScope, ): UBoolExpr { - TODO("Not yet implemented") + // TODO: LT operator for fake objects is not fully supported + return mkFalse() } override fun TsContext.internalResolve( @@ -1149,7 +1151,12 @@ sealed interface TsBinaryOperator { rhs: UExpr<*>, scope: TsStepScope, ): UBoolExpr { - TODO("Not yet implemented") + // TODO: the immediate conversion to numbers is not correct, + // we first need to try to convert arguments to primitive values, + // which might become strings, for which LT has different semantics. + val left = mkNumericExpr(lhs, scope) + val right = mkNumericExpr(rhs, scope) + return mkFpLessExpr(left, right) } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 00556fcf2b..d3340f8845 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -54,6 +54,7 @@ class TsState( val addedArtificialLocals: MutableSet = hashSetOf(), val lValuesToAllocatedFakeObjects: MutableList, UConcreteHeapRef>> = mutableListOf(), var discoveredCallees: UPersistentHashMap, EtsBlockCfg> = persistentHashMapOf(), + var promiseExecutors: UPersistentHashMap = persistentHashMapOf(), ) : UState( ctx = ctx, initOwnership = ownership, @@ -141,6 +142,13 @@ class TsState( return result } + fun setPromiseExecutor( + local: EtsLocal, + method: EtsMethod, + ) { + promiseExecutors = promiseExecutors.put(local, method, ownership) + } + override fun clone(newConstraints: UPathConstraints?): TsState { val newThisOwnership = MutabilityOwnership() val cloneOwnership = MutabilityOwnership() @@ -168,6 +176,7 @@ class TsState( addedArtificialLocals = addedArtificialLocals, lValuesToAllocatedFakeObjects = lValuesToAllocatedFakeObjects.toMutableList(), discoveredCallees = discoveredCallees, + promiseExecutors = promiseExecutors, ) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt b/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt index 4cec881225..c7ed434f95 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt @@ -16,14 +16,18 @@ class TsStateVisualizer : TsInterpreterObserver, UMachineObserver { } } -fun TsState.renderGraph() { +fun TsState.renderGraph(view: Boolean = true) { val graph = InterproceduralCfg(main = entrypoint.cfg, callees = discoveredCallees.toMap()) val dot = graph.toHighlightedDotWithCalls( pathStmts = pathNode.allStatements.toSet(), currentStmt = currentStatement, ) - myRenderDot(dot) + if (view ) { + myRenderDot(dot) + } else { + myRenderDot(dot, viewerCmd = null) + } } @Suppress("DEPRECATION") diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt index bca881d048..a79aa74d99 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt @@ -1,5 +1,6 @@ package org.usvm.project +import mu.KotlinLogging import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.ANONYMOUS_CLASS_PREFIX import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX @@ -14,7 +15,8 @@ import org.usvm.util.TsMethodTestRunner import org.usvm.util.getResourcePath import org.usvm.util.getResourcePathOrNull import kotlin.test.Test -import kotlin.time.Duration.Companion.seconds + +private val logger = KotlinLogging.logger {} @EnabledIf("projectAvailable") class RunOnDemoPhotosProject : TsMethodTestRunner() { @@ -42,14 +44,18 @@ class RunOnDemoPhotosProject : TsMethodTestRunner() { } @Test - fun `test run on each method`() { + fun `test run on each class`() { val exceptions = mutableListOf() val classes = scene.projectClasses .filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) } - println("Total classes: ${classes.size}") + logger.info {"Total classes: ${classes.size}"} + + for (cls in classes) { + logger.info { + "Analyzing class ${cls.name} with ${cls.methods.size} methods" + } - classes.forEach { cls -> val methods = cls.methods .filterNot { it.cfg.stmts.isEmpty() } .filterNot { it.isStatic } @@ -58,12 +64,14 @@ class RunOnDemoPhotosProject : TsMethodTestRunner() { .filterNot { it.name == INSTANCE_INIT_METHOD_NAME } .filterNot { it.name == STATIC_INIT_METHOD_NAME } .filterNot { it.name == CONSTRUCTOR_NAME } + .filterNot { it.name == "loadFileAsset" } + .filterNot { it.name == "onRecover" } - if (methods.isEmpty()) return@forEach + if (methods.isEmpty()) continue runCatching { val tsOptions = TsOptions() - TsMachine(scene, options.copy(timeout = 120.seconds), tsOptions).use { machine -> + TsMachine(scene, options, tsOptions).use { machine -> val states = machine.analyze(methods) states.let {} } @@ -73,9 +81,9 @@ class RunOnDemoPhotosProject : TsMethodTestRunner() { } val exc = exceptions.groupBy { it } - println("Total exceptions: ${exc.size}") + logger.error{"Total exceptions: ${exc.size}"} for (es in exc.values.sortedBy { it.size }.asReversed()) { - println("${es.first()}") + logger.error{"${es.first()}"} } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt new file mode 100644 index 0000000000..c9afeb1a16 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt @@ -0,0 +1,33 @@ +package org.usvm.samples + +import org.jacodb.ets.model.EtsScene +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import kotlin.test.Test + +class Async : TsMethodTestRunner() { + + companion object { + private const val SDK_TYPESCRIPT_PATH = "/sdk/typescript" + private const val SDK_OHOS_PATH = "/sdk/ohos" + } + + private val className = this::class.simpleName!! + + override val scene: EtsScene = loadSampleScene( + className, + sdks = listOf(SDK_TYPESCRIPT_PATH, SDK_OHOS_PATH) + ) + + @Test + fun `create and await promise`() { + val method = getMethod(className, "createAndAwaitPromise") + discoverProperties( + method = method, + { r -> r.number == 1.0 }, + invariants = arrayOf( + { r -> r.number != -1.0 }, + ) + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt index ce5198b8f7..be57b19c81 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt @@ -15,6 +15,7 @@ import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.jacodb.ets.utils.loadEtsProjectAutoConvert import org.junit.jupiter.api.TestInstance import org.junit.jupiter.api.TestInstance.Lifecycle.PER_CLASS import org.usvm.PathSelectionStrategy @@ -44,6 +45,7 @@ abstract class TsMethodTestRunner : TestRunner = emptyList(), // resource paths to SDKs ): EtsScene { val name = "$className.ts" val path = getResourcePath("/samples/$folderPrefix/$name") @@ -51,7 +53,12 @@ abstract class TsMethodTestRunner : TestRunner + val sdkPath = getResourcePath(sdk) + val sdkProject = loadEtsProjectAutoConvert(sdkPath, useArkAnalyzerTypeInference = null) + sdkProject.projectFiles + } + return EtsScene(listOf(file), sdkFiles) } protected fun getMethod(className: String, methodName: String): EtsMethod { diff --git a/usvm-ts/src/test/resources/samples/Async.ts b/usvm-ts/src/test/resources/samples/Async.ts new file mode 100644 index 0000000000..3882c3953d --- /dev/null +++ b/usvm-ts/src/test/resources/samples/Async.ts @@ -0,0 +1,16 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class Async { + createAndAwaitPromise(): number { + const promise = new Promise((resolve) => { + resolve(42); + }); + const resolved = await promise; + if (resolved == 42) { + return 1; + } else { + return -1; // unreachable + } + } +} From b736f181e5ffa10610d597fbc4d1e59aada21264 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 8 Jul 2025 14:46:33 +0300 Subject: [PATCH 02/21] Log the renderer --- .../src/main/kotlin/org/usvm/util/TsStateVisualizer.kt | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt b/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt index c7ed434f95..f80ea4fcba 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt @@ -1,5 +1,6 @@ package org.usvm.util +import mu.KotlinLogging import org.jacodb.ets.utils.InterproceduralCfg import org.jacodb.ets.utils.toHighlightedDotWithCalls import org.usvm.dataflow.ts.util.toMap @@ -10,6 +11,8 @@ import java.nio.file.Path import kotlin.io.path.createTempDirectory import kotlin.io.path.writeText +private val logger = KotlinLogging.logger {} + class TsStateVisualizer : TsInterpreterObserver, UMachineObserver { override fun onStatePeeked(state: TsState) { state.renderGraph() @@ -44,10 +47,11 @@ fun myRenderDot( }, ) { val dotFile = outDir.resolve("$baseName.dot") - val svgFile = outDir.resolveSibling("$baseName.$format") + val outFile = outDir.resolveSibling("$baseName.$format") dotFile.writeText(dot) - Runtime.getRuntime().exec("$dotCmd $dotFile -T$format -o $svgFile").waitFor() + Runtime.getRuntime().exec("$dotCmd $dotFile -T$format -o $outFile").waitFor() + logger.debug { "Rendered DOT to ${format.uppercase()}: $outFile" } if (viewerCmd != null) { - Runtime.getRuntime().exec("$viewerCmd $svgFile").waitFor() + Runtime.getRuntime().exec("$viewerCmd $outFile").waitFor() } } From 0c95e9b945740e2902bb26c0efe38a966f352811 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 8 Jul 2025 14:48:18 +0300 Subject: [PATCH 03/21] Pass the await test --- .../org/usvm/machine/expr/TsExprResolver.kt | 94 ++++++++++++------- .../usvm/machine/interpreter/TsInterpreter.kt | 2 +- .../kotlin/org/usvm/machine/state/TsState.kt | 7 +- 3 files changed, 66 insertions(+), 37 deletions(-) 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 064c493b8f..57d047947a 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 @@ -26,6 +26,7 @@ import org.jacodb.ets.model.EtsEntity import org.jacodb.ets.model.EtsEqExpr import org.jacodb.ets.model.EtsExpExpr import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsGtEqExpr import org.jacodb.ets.model.EtsGtExpr @@ -105,6 +106,7 @@ import org.usvm.machine.interpreter.isInitialized import org.usvm.machine.interpreter.isResolved import org.usvm.machine.interpreter.markInitialized import org.usvm.machine.interpreter.markResolved +import org.usvm.machine.interpreter.setResolvedValue import org.usvm.machine.operator.TsBinaryOperator import org.usvm.machine.operator.TsUnaryOperator import org.usvm.machine.state.TsMethodResult @@ -387,18 +389,22 @@ class TsExprResolver( if (!isResolved) { // If the promise is not resolved yet, we need to call the executor to resolve it. val executor = scope.calcOnState { - promiseExecutors[expr.arg] - ?: error("Await expression should have a promise executor, but it is not set for ${expr.arg}") + promiseExecutors[promise] + ?: error("Await expression should have a promise executor, but it is not set for $promise") } check(executor.cfg.stmts.isNotEmpty()) scope.doWithState { markResolved(promise) - pushSortsForArguments(instance = null, args = emptyList(), localToIdx) + // Note: arguments for 'executor' are: + // - `resolve`, if present in parameters + // - `reject`, if present in parameters + // - `promise` == "this", should be the last + val args = executor.parameters.map{mkUndefinedValue()} + promise + // pushSortsForArguments(instance = null, args = emptyList(), localToIdx) + pushSortsForActualArguments(args) + memory.stack.push(args.toTypedArray(), executor.localsCount) registerCallee(currentStatement, executor.cfg) callStack.push(executor, currentStatement) - // TODO: pass meaningful 'instance' for the executor, e.g. some static instance - val instance = mkUndefinedValue() // TODO: 'this' should not be undefined! - memory.stack.push(arrayOf(instance), executor.localsCount) newStmt(executor.cfg.stmts.first()) } null @@ -625,6 +631,35 @@ class TsExprResolver( } } + // Handle Promise constructor + if (expr.callee.enclosingClass.name == "Promise" && expr.callee.name == CONSTRUCTOR_NAME) { + val promise = resolve(expr.instance)?.asExpr(addressSort) ?: return null + val executorLocal = expr.args.single() + val executors = resolveEtsMethods( + EtsMethodSignature( + enclosingClass = EtsClassSignature.UNKNOWN, + name = executorLocal.name, + parameters = emptyList(), + returnType = EtsUnknownType, + ) + ) + if (executors.isEmpty()) { + logger.error { "Could not resolve executor method: ${executorLocal.name}" } + scope.assert(falseExpr) + return null + } + if (executors.size > 1) { + logger.error { "Ambiguous executor method: ${executorLocal.name}, resolved ${executors.size} times" } + scope.assert(falseExpr) + return null + } + val executor = executors.single() + scope.doWithState { + setPromiseExecutor(promise, executor) + } + return promise + } + return when (val result = scope.calcOnState { methodResult }) { is TsMethodResult.Success -> { scope.doWithState { methodResult = TsMethodResult.NoCall } @@ -652,33 +687,6 @@ class TsExprResolver( resolved.asExpr(addressSort) } - // Handle Promise constructor - if (expr.callee.enclosingClass.name == "Promise" && expr.callee.name == CONSTRUCTOR_NAME) { - val executorLocal = expr.args.single() - val executors = resolveEtsMethods( - EtsMethodSignature( - enclosingClass = EtsClassSignature.UNKNOWN, - name = executorLocal.name, - parameters = emptyList(), - returnType = EtsUnknownType, - ) - ) - if (executors.isEmpty()) { - logger.error { "Could not resolve executor method: ${executorLocal.name}" } - scope.assert(falseExpr) - return null - } - if (executors.size > 1) { - logger.error { "Ambiguous executor method: ${executorLocal.name}, resolved ${executors.size} times" } - scope.assert(falseExpr) - return null - } - val executor = executors.single() - scope.doWithState { - setPromiseExecutor(expr.instance, executor) - } - } - val resolvedArgs = expr.args.map { resolve(it) ?: return null } val virtualCall = TsVirtualMethodCallStmt( @@ -709,6 +717,26 @@ class TsExprResolver( } } + if (expr.callee.name == "resolve") { + val promise = resolve( + EtsThis( + EtsClassType( + EtsClassSignature( + "Promise", + EtsFileSignature("typescript", "lib.es5.d.ts") + ) + ) + ) + ) ?: return null + check(expr.args.size == 1) { "resolve should have exactly one argument" } + val value = resolve(expr.args.single()) ?: return null + val fakeValue = value.toFakeObject(scope) + scope.doWithState { + setResolvedValue(promise.asExpr(addressSort), fakeValue) + } + return mkUndefinedValue() + } + if (expr.callee.name == "\$r") { return scope.calcOnState { val mockSymbol = memory.mocker.createMockSymbol(trackedLiteral = null, addressSort, ownership) 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 2e8ee560d4..61e5cef724 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 @@ -246,7 +246,7 @@ class TsInterpreter( .asSequence() // TODO wrong order, ancestors are unordered .map { graph.hierarchy.getAncestors(it) } - .map { it.first { it.methods.any { it.name == stmt.callee.name } } } + .mapNotNull { it.firstOrNull { it.methods.any { it.name == stmt.callee.name } } } .map { clazz to it.methods.first { it.name == stmt.callee.name } } }.toList().take(10) // TODO check it diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index d3340f8845..f4e5009a62 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -13,6 +13,7 @@ import org.usvm.PathNode import org.usvm.UCallStack import org.usvm.UConcreteHeapRef import org.usvm.UExpr +import org.usvm.UHeapRef import org.usvm.USort import org.usvm.UState import org.usvm.api.targets.TsTarget @@ -54,7 +55,7 @@ class TsState( val addedArtificialLocals: MutableSet = hashSetOf(), val lValuesToAllocatedFakeObjects: MutableList, UConcreteHeapRef>> = mutableListOf(), var discoveredCallees: UPersistentHashMap, EtsBlockCfg> = persistentHashMapOf(), - var promiseExecutors: UPersistentHashMap = persistentHashMapOf(), + var promiseExecutors: UPersistentHashMap = persistentHashMapOf(), ) : UState( ctx = ctx, initOwnership = ownership, @@ -143,10 +144,10 @@ class TsState( } fun setPromiseExecutor( - local: EtsLocal, + promise: UHeapRef, method: EtsMethod, ) { - promiseExecutors = promiseExecutors.put(local, method, ownership) + promiseExecutors = promiseExecutors.put(promise, method, ownership) } override fun clone(newConstraints: UPathConstraints?): TsState { From 1d9f64c8be9298b0c7066fa77b14e0a3f849f070 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 8 Jul 2025 16:12:00 +0300 Subject: [PATCH 04/21] Add PromiseState --- .../org/usvm/machine/expr/TsExprResolver.kt | 63 ++++++++++++++----- .../org/usvm/machine/interpreter/TsPromise.kt | 6 ++ .../kotlin/org/usvm/machine/state/TsState.kt | 15 ++++- 3 files changed, 67 insertions(+), 17 deletions(-) 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 57d047947a..b4e76576c5 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 @@ -95,11 +95,13 @@ import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArrayLength import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type +import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.Constants import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext import org.usvm.machine.TsSizeSort import org.usvm.machine.TsVirtualMethodCallStmt +import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.interpreter.getResolvedValue import org.usvm.machine.interpreter.isInitialized @@ -384,10 +386,20 @@ class TsExprResolver( } val promise = arg.asExpr(addressSort) + check(isAllocatedConcreteHeapRef(promise)) { + "Promise instance should be allocated, but it is not: $promise" + } + + val promiseState = scope.calcOnState { + promiseStates[promise] ?: error("Promise state is not set for $promise") + } val isResolved = scope.calcOnState { isResolved(promise) } - if (!isResolved) { + return if (!isResolved) { // If the promise is not resolved yet, we need to call the executor to resolve it. + check(promiseState == PromiseState.PENDING) { + "Promise state should be PENDING, but it is $promiseState for $promise" + } val executor = scope.calcOnState { promiseExecutors[promise] ?: error("Await expression should have a promise executor, but it is not set for $promise") @@ -399,7 +411,7 @@ class TsExprResolver( // - `resolve`, if present in parameters // - `reject`, if present in parameters // - `promise` == "this", should be the last - val args = executor.parameters.map{mkUndefinedValue()} + promise + val args = executor.parameters.map { mkUndefinedValue() } + promise // pushSortsForArguments(instance = null, args = emptyList(), localToIdx) pushSortsForActualArguments(args) memory.stack.push(args.toTypedArray(), executor.localsCount) @@ -409,18 +421,37 @@ class TsExprResolver( } null } else { - // If the promise is already resolved, we can return this value. - // val sort = typeToSort(expr.arg.type) - val sort = typeToSort(EtsUnknownType) - if (sort == unresolvedSort) { - val value = scope.calcOnState { - getResolvedValue(promise, addressSort) + when (promiseState) { + PromiseState.PENDING -> { + error("Promise state should not be PENDING, but it is for $promise") } - check(value.isFakeObject()) - value - } else { - scope.calcOnState { - getResolvedValue(promise, sort) + + PromiseState.FULFILLED -> { + // If the promise is already resolved, we can return this value. + // val sort = typeToSort(expr.arg.type) + val sort = typeToSort(EtsUnknownType) + if (sort == unresolvedSort) { + val value = scope.calcOnState { + getResolvedValue(promise, addressSort) + } + check(value.isFakeObject()) + value + } else { + scope.calcOnState { + getResolvedValue(promise, sort) + } + } + } + + PromiseState.REJECTED -> { + // If the promise is rejected, we throw an exception. + val reason = scope.calcOnState { + getResolvedValue(promise, addressSort) + } + scope.doWithState { + methodResult = TsMethodResult.TsException(reason, EtsStringType) + } + null } } } @@ -633,7 +664,11 @@ class TsExprResolver( // Handle Promise constructor if (expr.callee.enclosingClass.name == "Promise" && expr.callee.name == CONSTRUCTOR_NAME) { - val promise = resolve(expr.instance)?.asExpr(addressSort) ?: return null + val instance = resolve(expr.instance) ?: return null + val promise = instance.asExpr(addressSort) + check(isAllocatedConcreteHeapRef(promise)) { + "Promise instance should be allocated, but it is not: $promise" + } val executorLocal = expr.args.single() val executors = resolveEtsMethods( EtsMethodSignature( 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 a0cc07bea6..f91f2dcc6b 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 @@ -10,6 +10,12 @@ import org.usvm.machine.TsContext import org.usvm.machine.state.TsState import org.usvm.util.mkFieldLValue +enum class PromiseState { + PENDING, + FULFILLED, + REJECTED; +} + internal const val RESOLVED_FIELD = "__resolved__" internal fun TsContext.mkResolvedField(ref: UHeapRef): UFieldLValue { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index f4e5009a62..87649e8366 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -13,7 +13,6 @@ import org.usvm.PathNode import org.usvm.UCallStack import org.usvm.UConcreteHeapRef import org.usvm.UExpr -import org.usvm.UHeapRef import org.usvm.USort import org.usvm.UState import org.usvm.api.targets.TsTarget @@ -23,6 +22,7 @@ import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.constraints.UPathConstraints import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.PromiseState import org.usvm.memory.ULValue import org.usvm.memory.UMemory import org.usvm.model.UModelBase @@ -55,7 +55,8 @@ class TsState( val addedArtificialLocals: MutableSet = hashSetOf(), val lValuesToAllocatedFakeObjects: MutableList, UConcreteHeapRef>> = mutableListOf(), var discoveredCallees: UPersistentHashMap, EtsBlockCfg> = persistentHashMapOf(), - var promiseExecutors: UPersistentHashMap = persistentHashMapOf(), + var promiseStates: UPersistentHashMap = persistentHashMapOf(), + var promiseExecutors: UPersistentHashMap = persistentHashMapOf(), ) : UState( ctx = ctx, initOwnership = ownership, @@ -143,8 +144,15 @@ class TsState( return result } + fun setPromiseState( + promise: UConcreteHeapRef, + state: PromiseState, + ) { + promiseStates = promiseStates.put(promise, state, ownership) + } + fun setPromiseExecutor( - promise: UHeapRef, + promise: UConcreteHeapRef, method: EtsMethod, ) { promiseExecutors = promiseExecutors.put(promise, method, ownership) @@ -177,6 +185,7 @@ class TsState( addedArtificialLocals = addedArtificialLocals, lValuesToAllocatedFakeObjects = lValuesToAllocatedFakeObjects.toMutableList(), discoveredCallees = discoveredCallees, + promiseStates = promiseStates, promiseExecutors = promiseExecutors, ) } From a63ff8516b62ae34b3ff7660e0a171c388def898 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 8 Jul 2025 16:56:56 +0300 Subject: [PATCH 05/21] Comment about exception --- usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | 1 + 1 file changed, 1 insertion(+) 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 b4e76576c5..e463c87e2f 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 @@ -449,6 +449,7 @@ class TsExprResolver( getResolvedValue(promise, addressSort) } scope.doWithState { + // TODO: create proper exception methodResult = TsMethodResult.TsException(reason, EtsStringType) } null From 46d8d8465532a166262bc7748b3e9e1d071b36c1 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 8 Jul 2025 16:57:06 +0300 Subject: [PATCH 06/21] Refine valueOf handling --- .../main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) 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 e463c87e2f..b510712150 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 @@ -711,8 +711,13 @@ class TsExprResolver( val resolved = resolve(expr.instance) ?: return null if (resolved.sort != addressSort) { - if (expr.callee.name == "valueOf" && expr.args.isEmpty()) { - return resolve(expr.instance) + if (expr.callee.name == "valueOf") { + if (expr.args.isNotEmpty()) { + logger.warn { + "valueOf should have no arguments, but got ${expr.args.size}" + } + } + return resolved } logger.warn { "Calling method on non-ref instance is not yet supported, instruction $expr" } From 5e4c7fb5ffd74df9a76245f28b2b51832e05453c Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 8 Jul 2025 17:28:48 +0300 Subject: [PATCH 07/21] Support rejecting promises --- .../org/usvm/machine/expr/TsExprResolver.kt | 20 +++++++++++++++---- .../usvm/machine/interpreter/TsInterpreter.kt | 14 +++++++++++-- .../src/test/kotlin/org/usvm/samples/Async.kt | 9 +++++++++ usvm-ts/src/test/resources/samples/Async.ts | 7 +++++++ 4 files changed, 44 insertions(+), 6 deletions(-) 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 b510712150..2247b4b4f0 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 @@ -391,7 +391,7 @@ class TsExprResolver( } val promiseState = scope.calcOnState { - promiseStates[promise] ?: error("Promise state is not set for $promise") + promiseStates[promise] ?: PromiseState.PENDING } val isResolved = scope.calcOnState { isResolved(promise) } @@ -406,11 +406,13 @@ class TsExprResolver( } check(executor.cfg.stmts.isNotEmpty()) scope.doWithState { - markResolved(promise) // Note: arguments for 'executor' are: // - `resolve`, if present in parameters // - `reject`, if present in parameters // - `promise` == "this", should be the last + check(executor.parameters.size <= 2) { + "Executor should have at most 2 parameters (resolve and reject), but it has ${executor.parameters.size} for $executor" + } val args = executor.parameters.map { mkUndefinedValue() } + promise // pushSortsForArguments(instance = null, args = emptyList(), localToIdx) pushSortsForActualArguments(args) @@ -758,7 +760,7 @@ class TsExprResolver( } } - if (expr.callee.name == "resolve") { + if (expr.callee.name == "resolve" || expr.callee.name == "reject") { val promise = resolve( EtsThis( EtsClassType( @@ -768,11 +770,21 @@ class TsExprResolver( ) ) ) - ) ?: return null + )?.asExpr(addressSort) ?: return null + check(isAllocatedConcreteHeapRef(promise)) { + "Promise instance should be allocated, but it is not: $promise" + } + val newState = when (expr.callee.name) { + "resolve" -> PromiseState.FULFILLED + "reject" -> PromiseState.REJECTED + else -> error("Unexpected: $expr") + } check(expr.args.size == 1) { "resolve should have exactly one argument" } val value = resolve(expr.args.single()) ?: return null val fakeValue = value.toFakeObject(scope) scope.doWithState { + markResolved(promise.asExpr(addressSort)) + setPromiseState(promise, newState) setResolvedValue(promise.asExpr(addressSort), fakeValue) } return mkUndefinedValue() 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 61e5cef724..fa465f8dab 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 @@ -181,7 +181,7 @@ class TsInterpreter( return } if (classes.size > 1) { - logger.warn { "Multiple (${classes.size}) classes with name: ${type.typeName}" } + logger.warn { "Multiple (${classes.size}) classes with name '${type.typeName}'" } // scope.assert(falseExpr) // return for (cls in classes) { @@ -290,7 +290,17 @@ class TsInterpreter( } constraint to block } - scope.forkMulti(conditionsWithBlocks) + if (conditionsWithBlocks.isEmpty()) { + logger.warn { + "No suitable methods found for call: ${stmt.callee} with instance: $unwrappedInstance" + } + mockMethodCall(scope, stmt.callee) + scope.doWithState { + newStmt(stmt.returnSite) + } + } else { + scope.forkMulti(conditionsWithBlocks) + } } private fun visitConcreteMethodCall(scope: TsStepScope, stmt: TsConcreteMethodCallStmt) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt index c9afeb1a16..0eb426d587 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt @@ -30,4 +30,13 @@ class Async : TsMethodTestRunner() { ) ) } + + @Test + fun `create and await rejecting promise`() { + val method = getMethod(className, "createAndAwaitRejectingPromise") + discoverProperties( + method = method, + { r -> r is TsTestValue.TsException }, + ) + } } diff --git a/usvm-ts/src/test/resources/samples/Async.ts b/usvm-ts/src/test/resources/samples/Async.ts index 3882c3953d..3fa6018a8f 100644 --- a/usvm-ts/src/test/resources/samples/Async.ts +++ b/usvm-ts/src/test/resources/samples/Async.ts @@ -13,4 +13,11 @@ class Async { return -1; // unreachable } } + + createAndAwaitRejectingPromise(): number { + const promise = new Promise((resolve, reject) => { + reject(new Error("An error occurred")); + }); + await promise; + } } From 4903bcb2d5472e59260b14bd35ae888d65a8248b Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 8 Jul 2025 17:54:18 +0300 Subject: [PATCH 08/21] Add tests for `Promise.resolve` and `Promise.reject` Currently fail --- .../src/test/kotlin/org/usvm/samples/Async.kt | 20 +++++++++++++++++++ usvm-ts/src/test/resources/samples/Async.ts | 12 ++++++++++- 2 files changed, 31 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt index 0eb426d587..2f70730d59 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt @@ -39,4 +39,24 @@ class Async : TsMethodTestRunner() { { r -> r is TsTestValue.TsException }, ) } + + @Test + fun `await resolved promise`() { + val method = getMethod(className, "awaitResolvedPromise") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 50.0 }, + ) + ) + } + + @Test + fun `await rejected promise`() { + val method = getMethod(className, "awaitRejectedPromise") + discoverProperties( + method = method, + { r -> r is TsTestValue.TsException }, + ) + } } diff --git a/usvm-ts/src/test/resources/samples/Async.ts b/usvm-ts/src/test/resources/samples/Async.ts index 3fa6018a8f..8f2d67c70c 100644 --- a/usvm-ts/src/test/resources/samples/Async.ts +++ b/usvm-ts/src/test/resources/samples/Async.ts @@ -18,6 +18,16 @@ class Async { const promise = new Promise((resolve, reject) => { reject(new Error("An error occurred")); }); - await promise; + await promise; // exception + } + + awaitResolvedPromise(): number { + const promise = Promise.resolve(50); + return await promise; // 50 + } + + awaitRejectedPromise(): number { + const promise = Promise.reject(new Error("An error occurred")); + await promise; // exception } } From 8cd20f95cdf9f6342d0f4b85814a4e4bae8afea2 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 8 Jul 2025 18:05:35 +0300 Subject: [PATCH 09/21] Support Promise.resolve and Promise.reject --- .../org/usvm/machine/expr/TsExprResolver.kt | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) 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 2247b4b4f0..e21989ae96 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 @@ -91,6 +91,7 @@ import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.UIteExpr import org.usvm.USort +import org.usvm.api.allocateConcreteRef import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArrayLength import org.usvm.dataflow.ts.infer.tryGetKnownType @@ -698,6 +699,25 @@ class TsExprResolver( return promise } + // Handle `Promise.resolve(value)` and `Promise.reject(reason)` calls + if (expr.instance.name == "Promise" && expr.callee.name in listOf("resolve", "reject")) { + val promise = allocateConcreteRef() + val newState = when (expr.callee.name) { + "resolve" -> PromiseState.FULFILLED + "reject" -> PromiseState.REJECTED + else -> error("Unexpected: $expr") + } + check(expr.args.size == 1) { "Promise.${expr.callee.name} should have exactly one argument" } + val value = resolve(expr.args.single()) ?: return null + val fakeValue = value.toFakeObject(scope) + scope.doWithState { + markResolved(promise) + setPromiseState(promise, newState) + setResolvedValue(promise, fakeValue) + } + return promise + } + return when (val result = scope.calcOnState { methodResult }) { is TsMethodResult.Success -> { scope.doWithState { methodResult = TsMethodResult.NoCall } From 8684c318678ee2dd661276bf4b4ebaeb60ba4a82 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 8 Jul 2025 19:16:39 +0300 Subject: [PATCH 10/21] A little bit of vibe coding for new tests --- .../test/kotlin/org/usvm/samples/Async2.kt | 242 ++++++++++++++++++ usvm-ts/src/test/resources/samples/Async2.ts | 201 +++++++++++++++ 2 files changed, 443 insertions(+) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/Async2.kt create mode 100644 usvm-ts/src/test/resources/samples/Async2.ts diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Async2.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Async2.kt new file mode 100644 index 0000000000..8556ed3afd --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Async2.kt @@ -0,0 +1,242 @@ +package org.usvm.samples + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Disabled +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import kotlin.test.Test + +class Async2 : TsMethodTestRunner() { + + companion object { + private const val SDK_TYPESCRIPT_PATH = "/sdk/typescript" + private const val SDK_OHOS_PATH = "/sdk/ohos" + } + + private val className = this::class.simpleName!! + + override val scene: EtsScene = loadSampleScene( + className, + sdks = listOf(SDK_TYPESCRIPT_PATH, SDK_OHOS_PATH) + ) + + @Test + fun `chain promises`() { + val method = getMethod(className, "chainPromises") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 20.0 }, + ) + ) + } + + @Test + fun `chain with rejection`() { + val method = getMethod(className, "chainWithRejection") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 42.0 }, + ) + ) + } + + @Test + fun `await async function`() { + val method = getMethod(className, "awaitAsyncFunction") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 10.0 }, + ) + ) + } + + @Test + fun `multiple awaits`() { + val method = getMethod(className, "multipleAwaits") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 8.0 }, + ) + ) + } + + @Test + fun `promise all`() { + val method = getMethod(className, "promiseAll") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 6.0 }, + ) + ) + } + + @Test + fun `promise race`() { + val method = getMethod(className, "promiseRace") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 42.0 }, + ) + ) + } + + @Disabled("Long running failing test") + @Test + fun `nested async`() { + val method = getMethod(className, "nestedAsync") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 20.0 }, + ) + ) + } + + @Test + fun `conditional await true`() { + val method = getMethod(className, "conditionalAwait") + discoverProperties( + method = method, + { r -> r.number == 100.0 }, + invariants = arrayOf( + { r -> r.number == 100.0 || r.number == 200.0 }, + ) + ) + } + + @Test + fun `async try catch`() { + val method = getMethod(className, "asyncTryCatch") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 50.0 }, + ) + ) + } + + @Test + fun `async finally`() { + val method = getMethod(className, "asyncFinally") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 15.0 }, + ) + ) + } + + @Test + fun `concurrent operations`() { + val method = getMethod(className, "concurrentOperations") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 35.0 }, + ) + ) + } + + @Test + fun `immediate resolve`() { + val method = getMethod(className, "immediateResolve") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 123.0 }, + ) + ) + } + + @Test + fun `immediate reject`() { + val method = getMethod(className, "immediateReject") + discoverProperties( + method = method, + { r -> r is TsTestValue.TsException }, + ) + } + + @Test + fun `conditional promise resolve`() { + val method = getMethod(className, "conditionalPromise") + discoverProperties( + method = method, + { r -> r.number == 777.0 }, + invariants = arrayOf( + { r -> r.number == 777.0 }, + ) + ) + } + + @Test + fun `conditional promise reject`() { + val method = getMethod(className, "conditionalPromise") + discoverProperties( + method = method, + { r -> r is TsTestValue.TsException }, + ) + } + + @Test + fun `await primitives`() { + val method = getMethod(className, "awaitPrimitives") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 42.0 }, + ) + ) + } + + @Test + fun `mixed values`() { + val method = getMethod(className, "mixedValues") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 60.0 }, + ) + ) + } + + @Test + fun `recursive async`() { + val method = getMethod(className, "recursiveAsync") + discoverProperties( + method = method, + { r -> r.number >= 0.0 }, // Sum of 1+2+...+n should be positive + invariants = arrayOf( + { r -> r.number >= 0.0 }, + ) + ) + } + + @Test + fun `nested promise resolution`() { + val method = getMethod(className, "nestedPromiseResolution") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 88.0 }, + ) + ) + } + + @Test + fun `error propagation`() { + val method = getMethod(className, "errorPropagation") + discoverProperties( + method = method, + invariants = arrayOf( + { r -> r.number == 99.0 }, + ) + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/Async2.ts b/usvm-ts/src/test/resources/samples/Async2.ts new file mode 100644 index 0000000000..2c66a64486 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/Async2.ts @@ -0,0 +1,201 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols,ES6RedundantAwait + +class Async2 { + // Test chaining promises + chainPromises(): number { + const promise1 = Promise.resolve(10); + const promise2 = promise1.then((value) => value * 2); + return await promise2; // Should return 20 + } + + // Test promise chaining with rejection + chainWithRejection(): number { + const promise1 = Promise.reject(new Error("First error")); + const promise2 = promise1.catch((error) => 42); + return await promise2; // Should return 42 + } + + // Test async function returning a promise + async asyncFunction(value: number): Promise { + if (value > 0) { + return value * 2; + } else { + throw new Error("Value must be positive"); + } + } + + // Test awaiting an async function + awaitAsyncFunction(): number { + return await this.asyncFunction(5); // Should return 10 + } + + // Test multiple awaits in sequence + multipleAwaits(): number { + const promise1 = Promise.resolve(5); + const promise2 = Promise.resolve(3); + const result1 = await promise1; + const result2 = await promise2; + return result1 + result2; // Should return 8 + } + + // Test Promise.all + promiseAll(): number { + const promises = [ + Promise.resolve(1), + Promise.resolve(2), + Promise.resolve(3), + ]; + const results = await Promise.all(promises); + return results.reduce((sum, val) => sum + val, 0); // Should return 6 + } + + // Test Promise.race + promiseRace(): number { + const promises = [ + Promise.resolve(42), + Promise.resolve(100), + ]; + return await Promise.race(promises); // Should return 42 (first resolved) + } + + // Test nested async/await + nestedAsync(): number { + const inner = async () => { + const value = await Promise.resolve(15); + return value + 5; + }; + return await inner(); // Should return 20 + } + + // Test conditional awaiting + conditionalAwait(usePromise: boolean): number { + if (usePromise) { + return await Promise.resolve(100); + } else { + return 200; + } + } + + // Test exception handling with try/catch + asyncTryCatch(): number { + try { + await Promise.reject(new Error("Test error")); + return -1; // Should not reach this + } catch (error) { + return 50; // Should return this + } + } + + // Test finally block with async + asyncFinally(): number { + let result = 0; + try { + result = await Promise.resolve(10); + } finally { + result += 5; + } + return result; // Should return 15 + } + + // Test setTimeout-like delayed promise + delayedPromise(delay: number, value: number): Promise { + return new Promise((resolve) => { + // Simulate async delay (in real implementation this would use setTimeout) + resolve(value); + }); + } + + // Test concurrent operations + concurrentOperations(): number { + const promise1 = this.delayedPromise(100, 10); + const promise2 = this.delayedPromise(200, 20); + const promise3 = this.delayedPromise(50, 5); + + const results = await Promise.all([promise1, promise2, promise3]); + return results[0] + results[1] + results[2]; // Should return 35 + } + + // Test promise constructor with immediate resolution + immediateResolve(): number { + const promise = new Promise((resolve, reject) => { + const condition = true; + if (condition) { + resolve(123); + } else { + reject(new Error("Should not happen")); + } + }); + return await promise; // Should return 123 + } + + // Test promise constructor with immediate rejection + immediateReject(): number { + const promise = new Promise((resolve, reject) => { + const condition = false; + if (condition) { + resolve(456); + } else { + reject(new Error("Immediate rejection")); + } + }); + return await promise; // Should throw exception + } + + // Test promise with both resolve and reject paths + conditionalPromise(shouldResolve: boolean): number { + const promise = new Promise((resolve, reject) => { + if (shouldResolve) { + resolve(777); + } else { + reject(new Error("Conditional rejection")); + } + }); + return await promise; + } + + // Test awaiting primitive values (should pass through) + awaitPrimitives(): number { + const num = await 42; + const str = await "hello"; + const bool = await true; + return num; // Should return 42 + } + + // Test mixed promise and non-promise values + mixedValues(): number { + const directValue = 10; + const promiseValue = await Promise.resolve(20); + const anotherDirect = 30; + return directValue + promiseValue + anotherDirect; // Should return 60 + } + + // Test recursive async calls + recursiveAsync(count: number): number { + if (count <= 0) { + return 0; + } + const currentValue = await Promise.resolve(count); + const restValue = await this.recursiveAsync(count - 1); + return currentValue + restValue; + } + + // Test promise that resolves to another promise + nestedPromiseResolution(): number { + const innerPromise = Promise.resolve(88); + const outerPromise = Promise.resolve(innerPromise); + return await outerPromise; // Should return 88 + } + + // Test error propagation through promise chain + errorPropagation(): number { + return await Promise.resolve(10) + .then(value => { + if (value > 5) { + throw new Error("Value too large"); + } + return value * 2; + }) + .catch(error => 99); // Should return 99 + } +} From c1724199d13556d880a80af6cf6dcc59f29e57c9 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 9 Jul 2025 17:08:28 +0300 Subject: [PATCH 11/21] Use latest jacodb --- buildSrc/src/main/kotlin/Dependencies.kt | 5 ++--- settings.gradle.kts | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 277c307ffb..ae17da9c71 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "5889d3c784" + const val jacodb = "da338ffc83" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0" @@ -116,8 +116,7 @@ object Libs { ) // https://github.com/UnitTestBot/jacodb - // private const val jacodbPackage = "com.github.UnitTestBot.jacodb" // use "org.jacodb" with includeBuild - private const val jacodbPackage = "org.jacodb" + private const val jacodbPackage = "com.github.UnitTestBot.jacodb" // use "org.jacodb" with includeBuild val jacodb_core = dep( group = jacodbPackage, name = "jacodb-core", diff --git a/settings.gradle.kts b/settings.gradle.kts index 10f13cd56b..a0f5b624aa 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -28,7 +28,7 @@ findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons" // Actually, `includeBuild("../jacodb")` is enough, but there is a bug in IDEA when path is a symlink. // As a workaround, we convert it to a real absolute path. // See IDEA bug: https://youtrack.jetbrains.com/issue/IDEA-329756 -includeBuild(file("../jacodb").toPath().toRealPath().toAbsolutePath()) +// includeBuild(file("../jacodb").toPath().toRealPath().toAbsolutePath()) pluginManagement { resolutionStrategy { From ddb68c4275995bbaab9fdea18f1ff561bd525631 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 9 Jul 2025 17:09:00 +0300 Subject: [PATCH 12/21] Extract handlers for specific calls --- .../org/usvm/machine/expr/TsExprResolver.kt | 229 +++++++++++------- 1 file changed, 140 insertions(+), 89 deletions(-) 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 e21989ae96..b778671c2d 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 @@ -596,7 +596,19 @@ class TsExprResolver( // region CALL - private fun handleNumberIsNaN(arg: UExpr): UBoolExpr? = with(ctx) { + private fun handleValueOf(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + if (expr.args.isNotEmpty()) { + logger.warn { "valueOf() should have no arguments, but got ${expr.args.size}" } + } + + val instance = resolve(expr.instance) ?: return null + instance + } + + private fun handleNumberIsNaN(expr: EtsInstanceCallExpr): UBoolExpr? = with(ctx) { + check(expr.args.size == 1) { "Number.isNaN should have one argument" } + val arg = resolve(expr.args.single()) ?: return null + // 21.1.2.4 Number.isNaN ( number ) // 1. If number is not a Number, return false. // 2. If number is NaN, return true. @@ -619,103 +631,138 @@ class TsExprResolver( } } - override fun visit(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { - if (expr.instance.name == "Number") { - if (expr.callee.name == "isNaN") { - check(expr.args.size == 1) { "Number.isNaN should have one argument" } - return resolveAfterResolved(expr.args.single()) { arg -> - handleNumberIsNaN(arg) - } - } + private fun handleArrayPush(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + val instance = resolve(expr.instance)?.asExpr(addressSort) ?: return null + check(expr.args.size == 1) { + "Array::push() should have exactly one argument, but got ${expr.args.size}" + } + val arg = resolve(expr.args.single()) ?: return null + val arrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + + scope.calcOnState { + // Update the length of the array + val lengthLValue = mkArrayLengthLValue(instance, arrayType) + val length = memory.read(lengthLValue) + val newLength = mkBvAddExpr(length, 1.toBv()) + memory.write(lengthLValue, newLength, guard = trueExpr) + + // Write the new element to the end of the array + // TODO check sorts compatibility https://github.com/UnitTestBot/usvm/issues/300 + val newIndexLValue = mkArrayIndexLValue( + sort = arg.sort, + ref = instance, + index = length, + type = arrayType, + ) + memory.write(newIndexLValue, arg.asExpr(newIndexLValue.sort), guard = ctx.trueExpr) + + // Return the new length of the array (as per ECMAScript spec for Array.push) + newLength + } + } + + private fun handlePromiseConstructor(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + val instance = resolve(expr.instance) ?: return null + val promise = instance.asExpr(addressSort) + check(isAllocatedConcreteHeapRef(promise)) { + "Promise instance should be allocated, but it is not: $promise" } + check(expr.args.size == 1) { + "Promise constructor should have exactly one argument, but got ${expr.args.size}" + } + val executorLocal = expr.args.single() + + // Lookup the executor method + val executors = resolveEtsMethods( + EtsMethodSignature( + enclosingClass = EtsClassSignature.UNKNOWN, + name = executorLocal.name, + parameters = emptyList(), + returnType = EtsUnknownType, + ) + ) + if (executors.isEmpty()) { + logger.error { "Could not resolve executor method: ${executorLocal.name}" } + scope.assert(falseExpr) + return null + } + if (executors.size > 1) { + logger.error { "Ambiguous executor method: ${executorLocal.name}, resolved ${executors.size} times" } + scope.assert(falseExpr) + return null + } + val executor = executors.single() + + // Save the executor for the promise in the state + scope.doWithState { + setPromiseExecutor(promise, executor) + } + + promise + } + + private fun handlePromiseResolveReject(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + val promise = allocateConcreteRef() + val newState = when (expr.callee.name) { + "resolve" -> PromiseState.FULFILLED + "reject" -> PromiseState.REJECTED + else -> error("Unexpected: $expr") + } + check(expr.args.size == 1) { + "Promise.${expr.callee.name}() should have exactly one argument, but got ${expr.args.size}" + } + val value = resolve(expr.args.single()) ?: return null + val fakeValue = value.toFakeObject(scope) + scope.doWithState { + markResolved(promise) + setPromiseState(promise, newState) + setResolvedValue(promise, fakeValue) + } + promise + } + override fun visit(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + // Mock all calls to `Logger` methods if (expr.instance.name == "Logger") { return mkUndefinedValue() } + // Mock `toString()` method calls if (expr.callee.name == "toString") { + if (expr.args.isNotEmpty()) { + logger.warn { "toString() should have no arguments, but got ${expr.args.size}" } + } return mkStringConstant("I am a string", scope) } - // TODO write tests https://github.com/UnitTestBot/usvm/issues/300 - if (expr.callee.name == "push" && expr.instance.type is EtsArrayType) { - return scope.calcOnState { - val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null - val lengthLValue = mkArrayLengthLValue( - resolvedInstance, - EtsArrayType(EtsUnknownType, dimensions = 1) - ) - val length = memory.read(lengthLValue) - val newLength = mkBvAddExpr(length, 1.toBv()) - memory.write(lengthLValue, newLength, guard = ctx.trueExpr) - if (expr.args.size != 1) { - let {} - } - val resolvedArg = resolve(expr.args.single()) ?: return@calcOnState null - - // TODO check sorts compatibility https://github.com/UnitTestBot/usvm/issues/300 - val newIndexLValue = mkArrayIndexLValue( - resolvedArg.sort, - resolvedInstance, - length, - EtsArrayType(EtsUnknownType, dimensions = 1) - ) - memory.write(newIndexLValue, resolvedArg.asExpr(newIndexLValue.sort), guard = ctx.trueExpr) + // Handle `valueOf()` method calls + if (expr.callee.name == "valueOf") { + return handleValueOf(expr) + } - newLength + // Handle `Number.isNaN(...)` calls + if (expr.instance.name == "Number") { + if (expr.callee.name == "isNaN") { + return handleNumberIsNaN(expr) } } - // Handle Promise constructor + // Handle `push` method calls on arrays + // TODO write tests https://github.com/UnitTestBot/usvm/issues/300 + if (expr.callee.name == "push" && expr.instance.type is EtsArrayType) { + return handleArrayPush(expr) + } + + // Handle `Promise` constructor calls if (expr.callee.enclosingClass.name == "Promise" && expr.callee.name == CONSTRUCTOR_NAME) { - val instance = resolve(expr.instance) ?: return null - val promise = instance.asExpr(addressSort) - check(isAllocatedConcreteHeapRef(promise)) { - "Promise instance should be allocated, but it is not: $promise" - } - val executorLocal = expr.args.single() - val executors = resolveEtsMethods( - EtsMethodSignature( - enclosingClass = EtsClassSignature.UNKNOWN, - name = executorLocal.name, - parameters = emptyList(), - returnType = EtsUnknownType, - ) - ) - if (executors.isEmpty()) { - logger.error { "Could not resolve executor method: ${executorLocal.name}" } - scope.assert(falseExpr) - return null - } - if (executors.size > 1) { - logger.error { "Ambiguous executor method: ${executorLocal.name}, resolved ${executors.size} times" } - scope.assert(falseExpr) - return null - } - val executor = executors.single() - scope.doWithState { - setPromiseExecutor(promise, executor) - } - return promise + return handlePromiseConstructor(expr) } // Handle `Promise.resolve(value)` and `Promise.reject(reason)` calls - if (expr.instance.name == "Promise" && expr.callee.name in listOf("resolve", "reject")) { - val promise = allocateConcreteRef() - val newState = when (expr.callee.name) { - "resolve" -> PromiseState.FULFILLED - "reject" -> PromiseState.REJECTED - else -> error("Unexpected: $expr") + if (expr.instance.name == "Promise") { + if (expr.callee.name in listOf("resolve", "reject")) { + return handlePromiseResolveReject(expr) } - check(expr.args.size == 1) { "Promise.${expr.callee.name} should have exactly one argument" } - val value = resolve(expr.args.single()) ?: return null - val fakeValue = value.toFakeObject(scope) - scope.doWithState { - markResolved(promise) - setPromiseState(promise, newState) - setResolvedValue(promise, fakeValue) - } - return promise } return when (val result = scope.calcOnState { methodResult }) { @@ -736,13 +783,13 @@ class TsExprResolver( if (expr.callee.name == "valueOf") { if (expr.args.isNotEmpty()) { logger.warn { - "valueOf should have no arguments, but got ${expr.args.size}" + "valueOf() should have no arguments, but got ${expr.args.size}" } } return resolved } - logger.warn { "Calling method on non-ref instance is not yet supported, instruction $expr" } + logger.warn { "Calling method on non-ref instance is not yet supported: $expr" } scope.assert(falseExpr) return null } @@ -767,20 +814,22 @@ class TsExprResolver( override fun visit(expr: EtsStaticCallExpr): UExpr<*>? = with(ctx) { if (expr.callee.name == "Number") { - check(expr.args.size == 1) { "Number constructor should have exactly one argument" } - return resolveAfterResolved(expr.args.single()) { - mkNumericExpr(it, scope) + check(expr.args.size == 1) { + "Number() should have exactly one argument, but got ${expr.args.size}" } + val arg = resolve(expr.args.single()) ?: return null + return mkNumericExpr(arg, scope) } if (expr.callee.name == "Boolean") { - check(expr.args.size == 1) { "Boolean constructor should have exactly one argument" } - return resolveAfterResolved(expr.args.single()) { - mkTruthyExpr(it, scope) + check(expr.args.size == 1) { + "Boolean() should have exactly one argument, but got ${expr.args.size}" } + val arg = resolve(expr.args.single()) ?: return null + return mkTruthyExpr(arg, scope) } - if (expr.callee.name == "resolve" || expr.callee.name == "reject") { + if (expr.callee.name in listOf("resolve", "reject")) { val promise = resolve( EtsThis( EtsClassType( @@ -799,7 +848,9 @@ class TsExprResolver( "reject" -> PromiseState.REJECTED else -> error("Unexpected: $expr") } - check(expr.args.size == 1) { "resolve should have exactly one argument" } + check(expr.args.size == 1) { + "${expr.callee.name}() should have exactly one argument, but got ${expr.args.size}" + } val value = resolve(expr.args.single()) ?: return null val fakeValue = value.toFakeObject(scope) scope.doWithState { From f3e8b1be639f4b60cc4293c8512ff1be00e35713 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 9 Jul 2025 17:54:59 +0300 Subject: [PATCH 13/21] Do not render graph on every step --- .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 2 -- 1 file changed, 2 deletions(-) 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 fa465f8dab..be8f1e8d63 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 @@ -77,7 +77,6 @@ import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.mkRegisterStackLValue -import org.usvm.util.renderGraph import org.usvm.util.resolveEtsField import org.usvm.util.resolveEtsMethods import org.usvm.util.type @@ -126,7 +125,6 @@ class TsInterpreter( // if no call, visit try { - state.renderGraph(view = false) when (stmt) { is TsVirtualMethodCallStmt -> visitVirtualMethodCall(scope, stmt) is TsConcreteMethodCallStmt -> visitConcreteMethodCall(scope, stmt) From 0080ef84b63070c7da61f72d584b88840da1b6bd Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 9 Jul 2025 17:55:41 +0300 Subject: [PATCH 14/21] Disable generated tests --- usvm-ts/src/test/kotlin/org/usvm/samples/Async2.kt | 1 + 1 file changed, 1 insertion(+) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Async2.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Async2.kt index 8556ed3afd..bd2c80f7a0 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Async2.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Async2.kt @@ -6,6 +6,7 @@ import org.usvm.api.TsTestValue import org.usvm.util.TsMethodTestRunner import kotlin.test.Test +@Disabled("Vibe code") class Async2 : TsMethodTestRunner() { companion object { From 9b35b1bd68c213b88d914fffb92a68a7909d4fa4 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 10 Jul 2025 13:24:36 +0300 Subject: [PATCH 15/21] Format --- usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt | 2 +- usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt b/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt index f80ea4fcba..430b9cdc02 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt @@ -26,7 +26,7 @@ fun TsState.renderGraph(view: Boolean = true) { currentStmt = currentStatement, ) - if (view ) { + if (view) { myRenderDot(dot) } else { myRenderDot(dot, viewerCmd = null) diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt index a79aa74d99..e63fdc0b8a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt @@ -49,7 +49,7 @@ class RunOnDemoPhotosProject : TsMethodTestRunner() { val classes = scene.projectClasses .filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) } - logger.info {"Total classes: ${classes.size}"} + logger.info { "Total classes: ${classes.size}" } for (cls in classes) { logger.info { @@ -81,9 +81,9 @@ class RunOnDemoPhotosProject : TsMethodTestRunner() { } val exc = exceptions.groupBy { it } - logger.error{"Total exceptions: ${exc.size}"} + logger.error { "Total exceptions: ${exc.size}" } for (es in exc.values.sortedBy { it.size }.asReversed()) { - logger.error{"${es.first()}"} + logger.error { "${es.first()}" } } } From 8d94f5921209694d2e2d2ef95ff6c21298b3b27b Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 10 Jul 2025 13:26:38 +0300 Subject: [PATCH 16/21] Remove disabled tests --- .../test/kotlin/org/usvm/samples/Async2.kt | 243 ------------------ usvm-ts/src/test/resources/samples/Async2.ts | 201 --------------- 2 files changed, 444 deletions(-) delete mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/Async2.kt delete mode 100644 usvm-ts/src/test/resources/samples/Async2.ts diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Async2.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Async2.kt deleted file mode 100644 index bd2c80f7a0..0000000000 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Async2.kt +++ /dev/null @@ -1,243 +0,0 @@ -package org.usvm.samples - -import org.jacodb.ets.model.EtsScene -import org.junit.jupiter.api.Disabled -import org.usvm.api.TsTestValue -import org.usvm.util.TsMethodTestRunner -import kotlin.test.Test - -@Disabled("Vibe code") -class Async2 : TsMethodTestRunner() { - - companion object { - private const val SDK_TYPESCRIPT_PATH = "/sdk/typescript" - private const val SDK_OHOS_PATH = "/sdk/ohos" - } - - private val className = this::class.simpleName!! - - override val scene: EtsScene = loadSampleScene( - className, - sdks = listOf(SDK_TYPESCRIPT_PATH, SDK_OHOS_PATH) - ) - - @Test - fun `chain promises`() { - val method = getMethod(className, "chainPromises") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 20.0 }, - ) - ) - } - - @Test - fun `chain with rejection`() { - val method = getMethod(className, "chainWithRejection") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 42.0 }, - ) - ) - } - - @Test - fun `await async function`() { - val method = getMethod(className, "awaitAsyncFunction") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 10.0 }, - ) - ) - } - - @Test - fun `multiple awaits`() { - val method = getMethod(className, "multipleAwaits") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 8.0 }, - ) - ) - } - - @Test - fun `promise all`() { - val method = getMethod(className, "promiseAll") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 6.0 }, - ) - ) - } - - @Test - fun `promise race`() { - val method = getMethod(className, "promiseRace") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 42.0 }, - ) - ) - } - - @Disabled("Long running failing test") - @Test - fun `nested async`() { - val method = getMethod(className, "nestedAsync") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 20.0 }, - ) - ) - } - - @Test - fun `conditional await true`() { - val method = getMethod(className, "conditionalAwait") - discoverProperties( - method = method, - { r -> r.number == 100.0 }, - invariants = arrayOf( - { r -> r.number == 100.0 || r.number == 200.0 }, - ) - ) - } - - @Test - fun `async try catch`() { - val method = getMethod(className, "asyncTryCatch") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 50.0 }, - ) - ) - } - - @Test - fun `async finally`() { - val method = getMethod(className, "asyncFinally") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 15.0 }, - ) - ) - } - - @Test - fun `concurrent operations`() { - val method = getMethod(className, "concurrentOperations") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 35.0 }, - ) - ) - } - - @Test - fun `immediate resolve`() { - val method = getMethod(className, "immediateResolve") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 123.0 }, - ) - ) - } - - @Test - fun `immediate reject`() { - val method = getMethod(className, "immediateReject") - discoverProperties( - method = method, - { r -> r is TsTestValue.TsException }, - ) - } - - @Test - fun `conditional promise resolve`() { - val method = getMethod(className, "conditionalPromise") - discoverProperties( - method = method, - { r -> r.number == 777.0 }, - invariants = arrayOf( - { r -> r.number == 777.0 }, - ) - ) - } - - @Test - fun `conditional promise reject`() { - val method = getMethod(className, "conditionalPromise") - discoverProperties( - method = method, - { r -> r is TsTestValue.TsException }, - ) - } - - @Test - fun `await primitives`() { - val method = getMethod(className, "awaitPrimitives") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 42.0 }, - ) - ) - } - - @Test - fun `mixed values`() { - val method = getMethod(className, "mixedValues") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 60.0 }, - ) - ) - } - - @Test - fun `recursive async`() { - val method = getMethod(className, "recursiveAsync") - discoverProperties( - method = method, - { r -> r.number >= 0.0 }, // Sum of 1+2+...+n should be positive - invariants = arrayOf( - { r -> r.number >= 0.0 }, - ) - ) - } - - @Test - fun `nested promise resolution`() { - val method = getMethod(className, "nestedPromiseResolution") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 88.0 }, - ) - ) - } - - @Test - fun `error propagation`() { - val method = getMethod(className, "errorPropagation") - discoverProperties( - method = method, - invariants = arrayOf( - { r -> r.number == 99.0 }, - ) - ) - } -} diff --git a/usvm-ts/src/test/resources/samples/Async2.ts b/usvm-ts/src/test/resources/samples/Async2.ts deleted file mode 100644 index 2c66a64486..0000000000 --- a/usvm-ts/src/test/resources/samples/Async2.ts +++ /dev/null @@ -1,201 +0,0 @@ -// @ts-nocheck -// noinspection JSUnusedGlobalSymbols,ES6RedundantAwait - -class Async2 { - // Test chaining promises - chainPromises(): number { - const promise1 = Promise.resolve(10); - const promise2 = promise1.then((value) => value * 2); - return await promise2; // Should return 20 - } - - // Test promise chaining with rejection - chainWithRejection(): number { - const promise1 = Promise.reject(new Error("First error")); - const promise2 = promise1.catch((error) => 42); - return await promise2; // Should return 42 - } - - // Test async function returning a promise - async asyncFunction(value: number): Promise { - if (value > 0) { - return value * 2; - } else { - throw new Error("Value must be positive"); - } - } - - // Test awaiting an async function - awaitAsyncFunction(): number { - return await this.asyncFunction(5); // Should return 10 - } - - // Test multiple awaits in sequence - multipleAwaits(): number { - const promise1 = Promise.resolve(5); - const promise2 = Promise.resolve(3); - const result1 = await promise1; - const result2 = await promise2; - return result1 + result2; // Should return 8 - } - - // Test Promise.all - promiseAll(): number { - const promises = [ - Promise.resolve(1), - Promise.resolve(2), - Promise.resolve(3), - ]; - const results = await Promise.all(promises); - return results.reduce((sum, val) => sum + val, 0); // Should return 6 - } - - // Test Promise.race - promiseRace(): number { - const promises = [ - Promise.resolve(42), - Promise.resolve(100), - ]; - return await Promise.race(promises); // Should return 42 (first resolved) - } - - // Test nested async/await - nestedAsync(): number { - const inner = async () => { - const value = await Promise.resolve(15); - return value + 5; - }; - return await inner(); // Should return 20 - } - - // Test conditional awaiting - conditionalAwait(usePromise: boolean): number { - if (usePromise) { - return await Promise.resolve(100); - } else { - return 200; - } - } - - // Test exception handling with try/catch - asyncTryCatch(): number { - try { - await Promise.reject(new Error("Test error")); - return -1; // Should not reach this - } catch (error) { - return 50; // Should return this - } - } - - // Test finally block with async - asyncFinally(): number { - let result = 0; - try { - result = await Promise.resolve(10); - } finally { - result += 5; - } - return result; // Should return 15 - } - - // Test setTimeout-like delayed promise - delayedPromise(delay: number, value: number): Promise { - return new Promise((resolve) => { - // Simulate async delay (in real implementation this would use setTimeout) - resolve(value); - }); - } - - // Test concurrent operations - concurrentOperations(): number { - const promise1 = this.delayedPromise(100, 10); - const promise2 = this.delayedPromise(200, 20); - const promise3 = this.delayedPromise(50, 5); - - const results = await Promise.all([promise1, promise2, promise3]); - return results[0] + results[1] + results[2]; // Should return 35 - } - - // Test promise constructor with immediate resolution - immediateResolve(): number { - const promise = new Promise((resolve, reject) => { - const condition = true; - if (condition) { - resolve(123); - } else { - reject(new Error("Should not happen")); - } - }); - return await promise; // Should return 123 - } - - // Test promise constructor with immediate rejection - immediateReject(): number { - const promise = new Promise((resolve, reject) => { - const condition = false; - if (condition) { - resolve(456); - } else { - reject(new Error("Immediate rejection")); - } - }); - return await promise; // Should throw exception - } - - // Test promise with both resolve and reject paths - conditionalPromise(shouldResolve: boolean): number { - const promise = new Promise((resolve, reject) => { - if (shouldResolve) { - resolve(777); - } else { - reject(new Error("Conditional rejection")); - } - }); - return await promise; - } - - // Test awaiting primitive values (should pass through) - awaitPrimitives(): number { - const num = await 42; - const str = await "hello"; - const bool = await true; - return num; // Should return 42 - } - - // Test mixed promise and non-promise values - mixedValues(): number { - const directValue = 10; - const promiseValue = await Promise.resolve(20); - const anotherDirect = 30; - return directValue + promiseValue + anotherDirect; // Should return 60 - } - - // Test recursive async calls - recursiveAsync(count: number): number { - if (count <= 0) { - return 0; - } - const currentValue = await Promise.resolve(count); - const restValue = await this.recursiveAsync(count - 1); - return currentValue + restValue; - } - - // Test promise that resolves to another promise - nestedPromiseResolution(): number { - const innerPromise = Promise.resolve(88); - const outerPromise = Promise.resolve(innerPromise); - return await outerPromise; // Should return 88 - } - - // Test error propagation through promise chain - errorPropagation(): number { - return await Promise.resolve(10) - .then(value => { - if (value > 5) { - throw new Error("Value too large"); - } - return value * 2; - }) - .catch(error => 99); // Should return 99 - } -} From 4819ee4fe9a24425c664d03d2325dc7fcd3eae24 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 11 Jul 2025 14:04:43 +0300 Subject: [PATCH 17/21] Add hosts for gitcode --- .github/extra/hosts | 37 +++++++++++++++++++++++++++++++++++++ .github/workflows/ci.yml | 3 +++ 2 files changed, 40 insertions(+) create mode 100644 .github/extra/hosts diff --git a/.github/extra/hosts b/.github/extra/hosts new file mode 100644 index 0000000000..ee4ed48dce --- /dev/null +++ b/.github/extra/hosts @@ -0,0 +1,37 @@ +116.205.2.91 gitcode.com +116.205.2.91 www.gitcode.com +116.205.6.139 ai.gitcode.com +120.46.215.171 ai-ide.gitcode.com +116.205.2.91 aihub-run.gitcode.com +116.205.6.218 api.gitcode.com +114.116.253.149 blog.gitcode.com +90.84.160.24 cdn-img.gitcode.com +221.194.141.163 cdn-news.gitcode.com +90.84.161.29 cdn-static.gitcode.com +116.205.2.45 chat-api.gitcode.com +116.205.6.139 competition.gitcode.com +116.205.2.91 copilot-app.gitcode.com +116.205.2.45 desktop-api.gitcode.com +36.41.168.170 desktop.gitcode.com +221.194.141.170 docs.gitcode.com +90.84.160.17 file-cdn.gitcode.com +116.205.2.91 file.gitcode.com +116.205.2.91 gitcodechat-app.gitcode.com +116.205.2.91 gosim.gitcode.com +116.205.2.91 homepage-app.gitcode.com +116.205.2.91 idea.gitcode.com +90.84.161.17 lfs-cdn.gitcode.com +116.205.6.30 lfs-ai.gitcode.com +90.84.161.18 lfs-ai-cdn.gitcode.com +116.205.6.213 lfs.gitcode.com +116.205.2.91 link.gitcode.com +120.233.178.92 matechat.gitcode.com +116.205.2.91 news.gitcode.com +90.84.160.17 raw-cdn.gitcode.com +113.44.227.73 raw.gitcode.com +116.205.6.153 tianqi-api.gitcode.com +116.205.6.153 tianqi.gitcode.com +116.205.2.91 usercenter-app.gitcode.com +116.205.2.45 web-api.gitcode.com +1.92.135.79 wechat-api.gitcode.com +116.205.2.91 weixin.gitcode.com diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4c9d3960d6..c9e36166a4 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -121,6 +121,9 @@ jobs: with: node-version: 22 + - name: Configure /etc/hosts + run: cat .github/extra/hosts >> /etc/hosts + - name: Set up ArkAnalyzer run: | REPO_URL="https://gitcode.com/Lipen/arkanalyzer.git" From d805cb82e184dfd79c2bf9b4461773905fac03e3 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 11 Jul 2025 14:05:30 +0300 Subject: [PATCH 18/21] sudo --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c9e36166a4..925e58bdf6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -122,7 +122,7 @@ jobs: node-version: 22 - name: Configure /etc/hosts - run: cat .github/extra/hosts >> /etc/hosts + run: sudo cat .github/extra/hosts >> /etc/hosts - name: Set up ArkAnalyzer run: | From 9298ca8fd85e4117248e566c6833caa28fb0e031 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 11 Jul 2025 14:10:55 +0300 Subject: [PATCH 19/21] tee --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 925e58bdf6..c20f3c378d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -122,7 +122,7 @@ jobs: node-version: 22 - name: Configure /etc/hosts - run: sudo cat .github/extra/hosts >> /etc/hosts + run: cat .github/extra/hosts | sudo tee --append /etc/hosts - name: Set up ArkAnalyzer run: | From 661760fa4d456bf3968aa9b03f1b665cec40c208 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 11 Jul 2025 14:51:06 +0300 Subject: [PATCH 20/21] Do not rely on sdk, approximate unresolved constructors --- .../org/usvm/machine/interpreter/TsInterpreter.kt | 11 ++++++++++- usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt | 5 +---- 2 files changed, 11 insertions(+), 5 deletions(-) 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 be8f1e8d63..b89d9156d6 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 @@ -32,6 +32,7 @@ import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsValue import org.jacodb.ets.model.EtsVoidType +import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.jacodb.ets.utils.callExpr import org.jacodb.ets.utils.getDeclaredLocals import org.usvm.StepResult @@ -175,6 +176,14 @@ class TsInterpreter( val classes = graph.hierarchy.classesForType(type) if (classes.isEmpty()) { logger.warn { "Could not resolve class: ${type.typeName}" } + if (stmt.callee.name == CONSTRUCTOR_NAME) { + // Approximate unresolved constructor: + scope.doWithState { + methodResult = TsMethodResult.Success.MockedCall(stmt.callee, unwrappedInstance) + newStmt(stmt.returnSite) + } + return + } scope.assert(falseExpr) return } @@ -225,7 +234,7 @@ class TsInterpreter( scope.calcOnState { newStmt(stmt.returnSite) } - return@with + return } val filteredPossibleTypesSet = possibleTypesSet - EtsAnyType diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt index 2f70730d59..618e8d2a5c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt @@ -14,10 +14,7 @@ class Async : TsMethodTestRunner() { private val className = this::class.simpleName!! - override val scene: EtsScene = loadSampleScene( - className, - sdks = listOf(SDK_TYPESCRIPT_PATH, SDK_OHOS_PATH) - ) + override val scene: EtsScene = loadSampleScene(className) @Test fun `create and await promise`() { From 8862990128554269123f22dacfa00a0e3a8982df Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 11 Jul 2025 15:01:32 +0300 Subject: [PATCH 21/21] Cherry-pick master --- .github/workflows/ci.yml | 2 +- settings.gradle.kts | 37 +++++++++++++++++++++++++++---------- 2 files changed, 28 insertions(+), 11 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c20f3c378d..3d5026c497 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -122,7 +122,7 @@ jobs: node-version: 22 - name: Configure /etc/hosts - run: cat .github/extra/hosts | sudo tee --append /etc/hosts + run: cat .github/extra/hosts | sudo tee -a /etc/hosts - name: Set up ArkAnalyzer run: | diff --git a/settings.gradle.kts b/settings.gradle.kts index a0f5b624aa..b6b98f4490 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -1,5 +1,32 @@ rootProject.name = "usvm" +pluginManagement { + resolutionStrategy { + eachPlugin { + if (requested.id.name == "rdgen") { + useModule("com.jetbrains.rd:rd-gen:${requested.version}") + } + } + } +} + +plugins { + // https://plugins.gradle.org/plugin/com.gradle.develocity + id("com.gradle.develocity") version("4.0.2") +} + +develocity { + buildScan { + // Accept the term of use for the build scan plugin: + termsOfUseUrl.set("https://gradle.com/help/legal-terms-of-use") + termsOfUseAgree.set("yes") + + // In CI, publish build scans automatically. + // Locally, publish build scans on-demand, when `--scan` option is provided: + publishing.onlyIf { System.getenv("CI") != null } + } +} + include("usvm-core") include("usvm-jvm") include("usvm-jvm:usvm-jvm-api") @@ -29,13 +56,3 @@ findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons" // As a workaround, we convert it to a real absolute path. // See IDEA bug: https://youtrack.jetbrains.com/issue/IDEA-329756 // includeBuild(file("../jacodb").toPath().toRealPath().toAbsolutePath()) - -pluginManagement { - resolutionStrategy { - eachPlugin { - if (requested.id.name == "rdgen") { - useModule("com.jetbrains.rd:rd-gen:${requested.version}") - } - } - } -}