diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 700801642a..7444014151 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 = "ddb127d9ef" + const val jacodb = "147d3b2797b693755c1d09fc28047ba43577a609" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0" 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 6b9179e3e7..b9de281c8e 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 @@ -1161,8 +1161,8 @@ class TsExprResolver( override fun visit(value: EtsStaticFieldRef): UExpr<*>? = handleStaticFieldRef(value) override fun visit(value: EtsCaughtExceptionRef): UExpr? { - logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } - error("Not supported $value") + return scope.calcOnState { caughtException } + ?: throw UnsupportedOperationException("Caught exception value is unavailable") } override fun visit(value: EtsGlobalRef): UExpr? { 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 9d42276687..71962c6ceb 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 @@ -113,11 +113,18 @@ class TsInterpreter( val result = state.methodResult if (result is TsMethodResult.TsException) { - // TODO catch processing scope.doWithState { + val catchers = stmt.location.method.cfg.catchers(stmt) + val catcher = catchers.singleOrNull() + if (catcher != null) { + caughtException = result.value + methodResult = TsMethodResult.NoCall + newStmt(catcher) + return@doWithState + } + leaveUnknownCallModelIfReturning() val returnSite = callStack.pop() - if (callStack.isNotEmpty()) { memory.stack.pop() popLocalToSortStack() @@ -706,37 +713,16 @@ class TsInterpreter( observer?.onThrowStatement(exprResolver.simpleValueResolver, stmt, scope) - val exception = exprResolver.resolve(stmt.exception) - - // Pop the call stack to return to the caller - scope.doWithState { - memory.stack.pop() + val exception = exprResolver.resolve(stmt.exception) ?: return + val exceptionType: EtsType = when (exception.sort) { + ctx.addressSort -> EtsStringType // TODO: improve object type detection + ctx.fp64Sort -> EtsNumberType + ctx.boolSort -> EtsBooleanType + else -> EtsStringType } - if (exception != null) { - val exceptionType: EtsType = when (exception.sort) { - ctx.addressSort -> { - // If it's an object reference, try to determine its type - val ref = exception.asExpr(ctx.addressSort) - // For now, assume it's a generic error type - EtsStringType // TODO: improve type detection - } - - ctx.fp64Sort -> EtsNumberType - - ctx.boolSort -> EtsBooleanType - - else -> EtsStringType - } - - scope.doWithState { - methodResult = TsMethodResult.TsException(exception, exceptionType) - } - } else { - scope.doWithState { - // If we couldn't resolve the exception value, throw a generic exception - methodResult = TsMethodResult.TsException(ctx.mkUndefinedValue(), EtsStringType) - } + scope.doWithState { + methodResult = TsMethodResult.TsException(exception, exceptionType) } } 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 c5b244ee33..4d8890772d 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 @@ -89,6 +89,8 @@ class TsState( var boundedStringBackingRefs: Set = emptySet(), /** Unresolved reference payloads that may acquire string backing after type refinement. */ var symbolicStringCandidates: Set = emptySet(), + /** Exception delivered to the current catch block, before its binding is initialized. */ + var caughtException: UExpr<*>? = null, var unsupportedReason: String? = null, private val activeUnknownCallModels: MutableList> = mutableListOf(), ) : UState( @@ -326,6 +328,7 @@ class TsState( stringConstantAllocatedRefs = stringConstantAllocatedRefs, boundedStringBackingRefs = boundedStringBackingRefs, symbolicStringCandidates = symbolicStringCandidates, + caughtException = caughtException, unsupportedReason = unsupportedReason, activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/ImportExportResolution.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/ImportExportResolution.kt index 660b670a17..017a8f55a0 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/ImportExportResolution.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/ImportExportResolution.kt @@ -153,7 +153,8 @@ class ImportExportResolutionTest { assertIs(result) assertTrue(result.exportInfo.isDefaultExport) assertEquals("default", result.exportInfo.name) - assertEquals("Helper", result.exportInfo.originalName) + assertEquals(expected = "default", actual = result.exportInfo.originalName) + assertEquals(expected = "Helper", actual = result.exportInfo.nameBeforeAs) assertEquals(EtsExportType.CLASS, result.exportInfo.type) } @@ -319,7 +320,8 @@ class ImportExportResolutionTest { val result = scene.resolveImportInfo(currentFile, importInfo) assertIs(result) assertEquals("default", result.exportInfo.name) - assertEquals("Helper", result.exportInfo.originalName) + assertEquals(expected = "default", actual = result.exportInfo.originalName) + assertEquals(expected = "Helper", actual = result.exportInfo.nameBeforeAs) } @Test diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt new file mode 100644 index 0000000000..da171b11a3 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt @@ -0,0 +1,127 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.state.TsMethodResult +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsCatchRoutingTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/samples/lang/Exceptions.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + private val analysisOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + ) + + @Test + fun `catch paths retain the thrown value and replay in Node`() { + val conditionalCatch = getMethod(methodName = "conditionalCatch", className = "Exceptions") + discoverProperties( + method = conditionalCatch, + { input, result -> input.number == 0.0 && result.number == 2.0 }, + { input, result -> input.number != 0.0 && result.number == 1.0 }, + invariants = arrayOf({ input, result -> result.number == (if (input.number == 0.0) 2.0 else 1.0) }), + ) + + for (name in listOf("caughtValue", "nestedCatch", "catchesCall", "rethrowToOuter")) { + val method = getMethod(methodName = name, className = "Exceptions") + discoverProperties( + method = method, + { input, result -> result.number == input.number + 1.0 }, + invariants = arrayOf({ input, result -> result.number == input.number + 1.0 }), + ) + } + + val tests = listOf("conditionalCatch", "caughtValue", "nestedCatch", "catchesCall", "rethrowToOuter") + .associateWith(::analyze) + + assertEquals(setOf(1, 2), tests.getValue("conditionalCatch").map(::resultNumber).toSet()) + tests.forEach { (name, generated) -> + generated.forEach { test -> assertExpectedResult(name, test) } + } + + replay(tests) + } + + private fun assertExpectedResult(name: String, test: TsTest) { + val input = assertIs(test.before.parameters.single()).number + val expected = when (name) { + "conditionalCatch" -> if (input == 0.0) 2.0 else 1.0 + "caughtValue", "nestedCatch", "catchesCall", "rethrowToOuter" -> input + 1.0 + else -> error("Unexpected method $name") + } + + assertEquals(expected, assertIs(test.returnValue).number, "$name: $test") + } + + private fun analyze(name: String): List { + val method = scene.projectClasses.single { it.name == "Exceptions" } + .methods + .single { it.name == name } + val result = TsMachine( + scene = scene, + options = analysisOptions, + tsOptions = TsOptions(), + ).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason, name) + assertTrue(result.unsupportedPaths.isEmpty(), "$name: ${result.unsupportedPaths}") + assertTrue(result.states.isNotEmpty(), name) + assertTrue(result.states.all { it.methodResult is TsMethodResult.Success }, name) + + return result.states.map { state -> TsTestResolver().resolve(method, state) } + } + + private fun resultNumber(test: TsTest): Int = + assertIs(test.returnValue).number.toInt() + + private fun replay(tests: Map>) { + val script = buildString { + appendLine(source.readText()) + tests.forEach { (name, generated) -> + generated.forEachIndexed { index, test -> + val input = assertIs(test.before.parameters.single()).number + val expected = assertIs(test.returnValue).number + + appendLine("if (new Exceptions().$name($input) !== $expected) {") + appendLine(" throw Error('$name witness $index');") + appendLine("}") + } + } + } + assertNodeReplay( + source = script, + directory = directory, + name = "catch-routing", + timeoutMessage = "Node replay timed out", + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Exceptions.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Exceptions.kt index 9bf6919809..b243547c85 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Exceptions.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Exceptions.kt @@ -98,4 +98,44 @@ class Exceptions : TsMethodTestRunner() { }, ) } + + @Test + fun `conditional catch only handles the throwing path`() { + val method = getMethod("conditionalCatch") + + discoverProperties( + method = method, + { value, result -> (value eq 0) && (result eq 2) }, + { value, result -> !(value eq 0) && (result eq 1) }, + invariants = arrayOf( + { value, result -> if (value eq 0) result eq 2 else result eq 1 }, + ), + ) + } + + @Test + fun `catch binding receives the thrown number`() { + val method = getMethod("caughtValue") + + discoverProperties( + method = method, + { value, result -> result eq (value.number + 1.0) }, + invariants = arrayOf( + { value, result -> result eq (value.number + 1.0) }, + ), + ) + } + + @Test + fun `nested catch uses the nearest handler`() { + val method = getMethod("nestedCatch") + + discoverProperties( + method = method, + { value, result -> result eq (value.number + 1.0) }, + invariants = arrayOf( + { value, result -> result eq (value.number + 1.0) }, + ), + ) + } } diff --git a/usvm-ts/src/test/resources/samples/lang/Exceptions.ts b/usvm-ts/src/test/resources/samples/lang/Exceptions.ts index 898ae1a3e2..cb2d27af54 100644 --- a/usvm-ts/src/test/resources/samples/lang/Exceptions.ts +++ b/usvm-ts/src/test/resources/samples/lang/Exceptions.ts @@ -38,4 +38,59 @@ class Exceptions { } return 42; } + + conditionalCatch(value: number): number { + try { + if (value === 0) { + throw 7; + } + return 1; + } catch { + return 2; + } + } + + caughtValue(value: number): number { + try { + throw value; + } catch (error) { + return error + 1; + } + } + + nestedCatch(value: number): number { + try { + try { + throw value; + } catch (inner) { + return inner + 1; + } + } catch (outer) { + return 99; + } + } + + throwsValue(value: number): number { + throw value; + } + + catchesCall(value: number): number { + try { + return this.throwsValue(value); + } catch (error) { + return error + 1; + } + } + + rethrowToOuter(value: number): number { + try { + try { + throw value; + } catch (inner) { + throw inner; + } + } catch (outer) { + return outer + 1; + } + } }