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..3d5026c497 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 | sudo tee -a /etc/hosts + - name: Set up ArkAnalyzer run: | REPO_URL="https://gitcode.com/Lipen/arkanalyzer.git" diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 17f3f22abc..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" 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}") - } - } - } -} 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..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 @@ -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 @@ -25,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 @@ -77,6 +79,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,18 +91,25 @@ 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.allocateConcreteRef 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 +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 @@ -120,6 +130,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 +378,87 @@ 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) + check(isAllocatedConcreteHeapRef(promise)) { + "Promise instance should be allocated, but it is not: $promise" + } + + val promiseState = scope.calcOnState { + promiseStates[promise] ?: PromiseState.PENDING + } + + val isResolved = scope.calcOnState { isResolved(promise) } + 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") + } + check(executor.cfg.stmts.isNotEmpty()) + scope.doWithState { + // 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) + memory.stack.push(args.toTypedArray(), executor.localsCount) + registerCallee(currentStatement, executor.cfg) + callStack.push(executor, currentStatement) + newStmt(executor.cfg.stmts.first()) + } + null + } else { + when (promiseState) { + PromiseState.PENDING -> { + error("Promise state should not be PENDING, but it is for $promise") + } + + 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 { + // TODO: create proper exception + methodResult = TsMethodResult.TsException(reason, EtsStringType) + } + null + } + } + } } override fun visit(expr: EtsYieldExpr): UExpr? { @@ -507,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. @@ -530,47 +631,137 @@ 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) } + // Handle `valueOf()` method calls + if (expr.callee.name == "valueOf") { + return handleValueOf(expr) + } + + // Handle `Number.isNaN(...)` calls + if (expr.instance.name == "Number") { + if (expr.callee.name == "isNaN") { + return handleNumberIsNaN(expr) + } + } + + // 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 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) - 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) + return handleArrayPush(expr) + } - newLength + // Handle `Promise` constructor calls + if (expr.callee.enclosingClass.name == "Promise" && expr.callee.name == CONSTRUCTOR_NAME) { + return handlePromiseConstructor(expr) + } + + // Handle `Promise.resolve(value)` and `Promise.reject(reason)` calls + if (expr.instance.name == "Promise") { + if (expr.callee.name in listOf("resolve", "reject")) { + return handlePromiseResolveReject(expr) } } @@ -589,11 +780,16 @@ 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" } + logger.warn { "Calling method on non-ref instance is not yet supported: $expr" } scope.assert(falseExpr) return null } @@ -618,17 +814,51 @@ 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 in listOf("resolve", "reject")) { + val promise = resolve( + EtsThis( + EtsClassType( + EtsClassSignature( + "Promise", + EtsFileSignature("typescript", "lib.es5.d.ts") + ) + ) + ) + )?.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) { + "${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.asExpr(addressSort)) + setPromiseState(promise, newState) + setResolvedValue(promise.asExpr(addressSort), fakeValue) + } + return mkUndefinedValue() } if (expr.callee.name == "\$r") { 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..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,12 +32,12 @@ 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 import org.usvm.StepScope import org.usvm.UAddressSort -import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UInterpreter import org.usvm.UIteExpr @@ -157,42 +157,49 @@ 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()) { 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 } 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 +220,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() @@ -227,7 +234,7 @@ class TsInterpreter( scope.calcOnState { newStmt(stmt.returnSite) } - return@with + return } val filteredPossibleTypesSet = possibleTypesSet - EtsAnyType @@ -246,7 +253,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 @@ -264,7 +271,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<*>) { @@ -290,7 +297,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) { @@ -299,8 +316,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 +584,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 +604,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..f91f2dcc6b --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsPromise.kt @@ -0,0 +1,62 @@ +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 + +enum class PromiseState { + PENDING, + FULFILLED, + REJECTED; +} + +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..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 @@ -22,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 @@ -54,6 +55,8 @@ class TsState( val addedArtificialLocals: MutableSet = hashSetOf(), val lValuesToAllocatedFakeObjects: MutableList, UConcreteHeapRef>> = mutableListOf(), var discoveredCallees: UPersistentHashMap, EtsBlockCfg> = persistentHashMapOf(), + var promiseStates: UPersistentHashMap = persistentHashMapOf(), + var promiseExecutors: UPersistentHashMap = persistentHashMapOf(), ) : UState( ctx = ctx, initOwnership = ownership, @@ -141,6 +144,20 @@ class TsState( return result } + fun setPromiseState( + promise: UConcreteHeapRef, + state: PromiseState, + ) { + promiseStates = promiseStates.put(promise, state, ownership) + } + + fun setPromiseExecutor( + promise: UConcreteHeapRef, + method: EtsMethod, + ) { + promiseExecutors = promiseExecutors.put(promise, method, ownership) + } + override fun clone(newConstraints: UPathConstraints?): TsState { val newThisOwnership = MutabilityOwnership() val cloneOwnership = MutabilityOwnership() @@ -168,6 +185,8 @@ class TsState( addedArtificialLocals = addedArtificialLocals, lValuesToAllocatedFakeObjects = lValuesToAllocatedFakeObjects.toMutableList(), discoveredCallees = discoveredCallees, + promiseStates = promiseStates, + 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..430b9cdc02 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,20 +11,26 @@ 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() } } -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") @@ -40,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() } } 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..e63fdc0b8a 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..618e8d2a5c --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt @@ -0,0 +1,59 @@ +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) + + @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 }, + ) + ) + } + + @Test + fun `create and await rejecting promise`() { + val method = getMethod(className, "createAndAwaitRejectingPromise") + discoverProperties( + method = method, + { 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/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..8f2d67c70c --- /dev/null +++ b/usvm-ts/src/test/resources/samples/Async.ts @@ -0,0 +1,33 @@ +// @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 + } + } + + createAndAwaitRejectingPromise(): number { + const promise = new Promise((resolve, reject) => { + reject(new Error("An error occurred")); + }); + 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 + } +}