From bea19ecb50e10b24a25cf0160e95fa718a971eb0 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 3 Jul 2024 12:02:44 +0300 Subject: [PATCH 1/6] Initial commit for a TS machine --- buildSrc/src/main/kotlin/Versions.kt | 0 settings.gradle.kts | 1 + usvm-ts/build.gradle.kts | 23 ++++++++++++ .../src/main/kotlin/org/usvm/TSComponents.kt | 25 +++++++++++++ usvm-ts/src/main/kotlin/org/usvm/TSContext.kt | 7 ++++ usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt | 11 ++++++ usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt | 7 ++++ .../src/main/kotlin/org/usvm/TSTypeSystem.kt | 34 ++++++++++++++++++ .../kotlin/org/usvm/state/TSMethodResult.kt | 35 ++++++++++++++++++ .../src/main/kotlin/org/usvm/state/TSState.kt | 36 +++++++++++++++++++ 10 files changed, 179 insertions(+) create mode 100644 buildSrc/src/main/kotlin/Versions.kt create mode 100644 usvm-ts/build.gradle.kts create mode 100644 usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/TSContext.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/state/TSMethodResult.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt diff --git a/buildSrc/src/main/kotlin/Versions.kt b/buildSrc/src/main/kotlin/Versions.kt new file mode 100644 index 0000000000..e69de29bb2 diff --git a/settings.gradle.kts b/settings.gradle.kts index e2dbbba1c3..121c7fcbd5 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -2,6 +2,7 @@ rootProject.name = "usvm" include("usvm-core") include("usvm-jvm") +include("usvm-ts") include("usvm-util") include("usvm-jvm-instrumentation") include("usvm-sample-language") diff --git a/usvm-ts/build.gradle.kts b/usvm-ts/build.gradle.kts new file mode 100644 index 0000000000..3e75f264ca --- /dev/null +++ b/usvm-ts/build.gradle.kts @@ -0,0 +1,23 @@ +plugins { + id("usvm.kotlin-conventions") +} + +dependencies { + implementation(project(":usvm-core")) + + implementation("${Versions.jacodbPackage}:jacodb-core:${Versions.jacodb}") + implementation("${Versions.jacodbPackage}:jacodb-panda-dynamic:${Versions.jacodb}") + + implementation("io.ksmt:ksmt-yices:${Versions.ksmt}") + implementation("io.ksmt:ksmt-cvc5:${Versions.ksmt}") + implementation("io.ksmt:ksmt-symfpu:${Versions.ksmt}") + implementation("io.ksmt:ksmt-runner:${Versions.ksmt}") + + testImplementation("io.mockk:mockk:${Versions.mockk}") + testImplementation("org.junit.jupiter:junit-jupiter-params:${Versions.junitParams}") + testImplementation("ch.qos.logback:logback-classic:${Versions.logback}") + + // https://mvnrepository.com/artifact/org.burningwave/core + // Use it to export all modules to all + testImplementation("org.burningwave:core:12.62.7") +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt new file mode 100644 index 0000000000..7329747405 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt @@ -0,0 +1,25 @@ +package org.usvm + +import org.jacodb.panda.dynamic.ets.base.EtsType +import org.usvm.solver.USolverBase +import org.usvm.types.UTypeSystem + +class TSComponents( + private val typeSystem: TSTypeSystem, + private val options: UMachineOptions +) : UComponents { + override val useSolverForForks: Boolean + get() = TODO("Not yet implemented") + + override fun > mkSizeExprProvider(ctx: Context): USizeExprProvider { + TODO("Not yet implemented") + } + + override fun mkTypeSystem(ctx: UContext): UTypeSystem { + TODO("Not yet implemented") + } + + override fun > mkSolver(ctx: Context): USolverBase { + TODO("Not yet implemented") + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt new file mode 100644 index 0000000000..26269b4793 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt @@ -0,0 +1,7 @@ +package org.usvm + +typealias TSSizeSort = UBv32Sort + +class TSContext(components: TSComponents) : UContext(components) { + +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt new file mode 100644 index 0000000000..62c5c5a1e1 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt @@ -0,0 +1,11 @@ +package org.usvm + +import org.usvm.state.TSState + +class TSMachine( + private val options: UMachineOptions +) : UMachine() { + override fun close() { + TODO("Not yet implemented") + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt new file mode 100644 index 0000000000..9539dba8af --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt @@ -0,0 +1,7 @@ +package org.usvm + +import org.jacodb.panda.dynamic.ets.base.EtsStmt +import org.usvm.targets.UTarget + +class TSTarget : UTarget() { +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt new file mode 100644 index 0000000000..670b106ae2 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt @@ -0,0 +1,34 @@ +package org.usvm + +import org.jacodb.panda.dynamic.ets.base.EtsType +import org.usvm.types.UTypeStream +import org.usvm.types.UTypeSystem +import kotlin.time.Duration + +class TSTypeSystem( + override val typeOperationsTimeout: Duration, +) : UTypeSystem { + override fun isSupertype(supertype: EtsType, type: EtsType): Boolean { + TODO("Not yet implemented") + } + + override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean { + TODO("Not yet implemented") + } + + override fun isFinal(type: EtsType): Boolean { + TODO("Not yet implemented") + } + + override fun isInstantiable(type: EtsType): Boolean { + TODO("Not yet implemented") + } + + override fun findSubtypes(type: EtsType): Sequence { + TODO("Not yet implemented") + } + + override fun topTypeStream(): UTypeStream { + TODO("Not yet implemented") + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/state/TSMethodResult.kt b/usvm-ts/src/main/kotlin/org/usvm/state/TSMethodResult.kt new file mode 100644 index 0000000000..40f72c664e --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/state/TSMethodResult.kt @@ -0,0 +1,35 @@ +package org.usvm.state + +import org.jacodb.panda.dynamic.api.PandaMethod +import org.jacodb.panda.dynamic.api.PandaType +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.USort + +/** + * Represents a result of a method invocation. + */ +interface TSMethodResult { + /** + * No call was performed. + */ + object NoCall : TSMethodResult + + /** + * A [method] successfully returned a [value]. + */ + class Success( + val method: PandaMethod, + val value: UExpr, + ) : TSMethodResult + + /** + * A method threw an exception with [type] type. + */ + open class TSException( + val address: UHeapRef, + val type: PandaType, + ) : TSMethodResult { + override fun toString(): String = "${this::class.simpleName}: Address: $address, type: ${type.typeName}" + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt b/usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt new file mode 100644 index 0000000000..57dd2393b0 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt @@ -0,0 +1,36 @@ +package org.usvm.state + +import org.jacodb.panda.dynamic.ets.base.EtsStmt +import org.jacodb.panda.dynamic.ets.base.EtsType +import org.jacodb.panda.dynamic.ets.model.EtsMethod +import org.usvm.PathNode +import org.usvm.TSContext +import org.usvm.TSTarget +import org.usvm.UCallStack +import org.usvm.UState +import org.usvm.constraints.UPathConstraints +import org.usvm.memory.UMemory +import org.usvm.model.UModelBase +import org.usvm.targets.UTargetsSet + +class TSState( + ctx: TSContext, + override val entrypoint: EtsMethod, + callStack: UCallStack, + pathConstraints: UPathConstraints = UPathConstraints(ctx), + memory: UMemory = UMemory(ctx, pathConstraints.typeConstraints), + models: List> = listOf(), + pathNode: PathNode = PathNode.root(), + forkPoints: PathNode> = PathNode.root(), + var methodResult: TSMethodResult = TSMethodResult.NoCall, + targets: UTargetsSet = UTargetsSet.empty(), +) : UState( + ctx, callStack, pathConstraints, memory, models, pathNode, forkPoints, targets +) { + override fun clone(newConstraints: UPathConstraints?): TSState { + TODO("Not yet implemented") + } + + override val isExceptional: Boolean + get() = TODO("Not yet implemented") +} From 04c16caf1145758c0a9763b15a531ccfccfda779 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 3 Jul 2024 18:05:25 +0300 Subject: [PATCH 2/6] Add a template for a test framework --- usvm-ts/src/main/kotlin/org/usvm/TSTest.kt | 11 ++ .../org/usvm/samples/TSMethodTestRunner.kt | 131 ++++++++++++++++++ 2 files changed, 142 insertions(+) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/TSTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/TSMethodTestRunner.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSTest.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTest.kt new file mode 100644 index 0000000000..308347c5da --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTest.kt @@ -0,0 +1,11 @@ +package org.usvm + +import org.jacodb.panda.dynamic.ets.base.EtsStmt + +class TSTest( + val parameters: List, + val resultValue: Any?, + val trace: List? = null +) + +class TSMethodCoverage \ No newline at end of file diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/TSMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/TSMethodTestRunner.kt new file mode 100644 index 0000000000..ce49e23685 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/TSMethodTestRunner.kt @@ -0,0 +1,131 @@ +package org.usvm.samples + +import org.jacodb.panda.dynamic.ets.base.EtsType +import org.usvm.TSMethodCoverage +import org.usvm.TSTest +import org.usvm.UMachineOptions +import org.usvm.test.util.TestRunner +import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults + +open class TSMethodTestRunner : TestRunner() { + + protected inline fun discoverProperties( + methodIdentifier: MethodDescriptor, + vararg analysisResultMatchers: (R?) -> Boolean, + invariants: Array> = emptyArray(), + ) { + internalCheck( + target = methodIdentifier, + analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults, + analysisResultsMatchers = analysisResultMatchers, + invariants = invariants, + extractValuesToCheck = { r -> r.parameters + r.resultValue }, + expectedTypesForExtractedValues = arrayOf(typeTransformer(R::class)), + checkMode = CheckMode.MATCH_PROPERTIES, + coverageChecker = { _ -> true } + ) + } + + protected inline fun discoverProperties( + methodIdentifier: MethodDescriptor, + vararg analysisResultMatchers: (T, R?) -> Boolean, + invariants: Array> = emptyArray(), + ) { + internalCheck( + target = methodIdentifier, + analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults, + analysisResultsMatchers = analysisResultMatchers, + invariants = invariants, + extractValuesToCheck = { r -> r.parameters + r.resultValue }, + expectedTypesForExtractedValues = arrayOf(typeTransformer(T::class), typeTransformer(R::class)), + checkMode = CheckMode.MATCH_PROPERTIES, + coverageChecker = { _ -> true } + ) + } + + protected inline fun discoverProperties( + methodIdentifier: MethodDescriptor, + vararg analysisResultMatchers: (T1, T2, R?) -> Boolean, + invariants: Array> = emptyArray(), + ) { + internalCheck( + target = methodIdentifier, + analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults, + analysisResultsMatchers = analysisResultMatchers, + invariants = invariants, + extractValuesToCheck = { r -> r.parameters + r.resultValue }, + expectedTypesForExtractedValues = arrayOf( + typeTransformer(T1::class), + typeTransformer(T2::class), + typeTransformer(R::class) + ), + checkMode = CheckMode.MATCH_PROPERTIES, + coverageChecker = { _ -> true } + ) + } + + protected inline fun discoverProperties( + methodIdentifier: MethodDescriptor, + vararg analysisResultMatchers: (T1, T2, T3, R?) -> Boolean, + invariants: Array> = emptyArray(), + ) { + internalCheck( + target = methodIdentifier, + analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults, + analysisResultsMatchers = analysisResultMatchers, + invariants = invariants, + extractValuesToCheck = { r -> r.parameters + r.resultValue }, + expectedTypesForExtractedValues = arrayOf( + typeTransformer(T1::class), + typeTransformer(T2::class), + typeTransformer(T3::class), + typeTransformer(R::class) + ), + checkMode = CheckMode.MATCH_PROPERTIES, + coverageChecker = { _ -> true } + ) + } + + protected inline fun discoverProperties( + methodIdentifier: MethodDescriptor, + vararg analysisResultMatchers: (T1, T2, T3, T4, R?) -> Boolean, + invariants: Array> = emptyArray(), + ) { + internalCheck( + target = methodIdentifier, + analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults, + analysisResultsMatchers = analysisResultMatchers, + invariants = invariants, + extractValuesToCheck = { r -> r.parameters + r.resultValue }, + expectedTypesForExtractedValues = arrayOf( + typeTransformer(T1::class), + typeTransformer(T2::class), + typeTransformer(T3::class), + typeTransformer(T4::class), + typeTransformer(R::class) + ), + checkMode = CheckMode.MATCH_PROPERTIES, + coverageChecker = { _ -> true } + ) + } + + override val typeTransformer: (Any?) -> EtsType + get() = TODO() + + @Suppress("UNUSED_ANONYMOUS_PARAMETER") + override val checkType: (EtsType?, EtsType?) -> Boolean + get() = TODO() + + override val runner: (MethodDescriptor, UMachineOptions) -> List + get() = TODO() + + override val coverageRunner: (List) -> TSMethodCoverage = TODO() + + override var options: UMachineOptions = TODO() +} + +data class MethodDescriptor( + val className: String, + val methodName: String, + val argumentsNumber: Int, +) From ad8209cbbcff8d358ef0c840f043cb0328ac36ab Mon Sep 17 00:00:00 2001 From: Sergey Loktev <71882967+zishkaz@users.noreply.github.com> Date: Thu, 18 Jul 2024 15:14:50 +0300 Subject: [PATCH 3/6] USVM API implementation for TypeScript (#195) * USVM TS expansion * USVM API implementation for TS * Remove redundant gradle line --------- Co-authored-by: Alexey Menshutin --- buildSrc/src/main/kotlin/Dependencies.kt | 5 + usvm-ts/build.gradle.kts | 18 +- .../kotlin/org/usvm/TSApplicationGraph.kt | 36 + .../src/main/kotlin/org/usvm/TSComponents.kt | 31 +- .../src/main/kotlin/org/usvm/TSInterpreter.kt | 77 +++ usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt | 103 ++- usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt | 2 +- usvm-ts/src/main/kotlin/org/usvm/TSTest.kt | 2 +- .../src/main/kotlin/org/usvm/TSTypeSystem.kt | 4 +- usvm-ts/src/main/kotlin/org/usvm/Util.kt | 8 + .../kotlin/org/usvm/state/TSMethodResult.kt | 8 +- .../src/main/kotlin/org/usvm/state/TSState.kt | 25 +- .../kotlin/org/usvm/state/TSStateUtils.kt | 3 + .../test/kotlin/org/usvm/samples/MinValue.kt | 22 + .../{samples => util}/TSMethodTestRunner.kt | 61 +- .../kotlin/org/usvm/util/TSTestResolver.kt | 12 + usvm-ts/src/test/resources/ir/MinValue.json | 636 ++++++++++++++++++ .../src/test/resources/samples/MinValue.ts | 11 + 18 files changed, 1028 insertions(+), 36 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/Util.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/MinValue.kt rename usvm-ts/src/test/kotlin/org/usvm/{samples => util}/TSMethodTestRunner.kt (69%) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt create mode 100644 usvm-ts/src/test/resources/ir/MinValue.json create mode 100644 usvm-ts/src/test/resources/samples/MinValue.ts diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index a2ae9c8bfe..613ed75c4f 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -126,6 +126,11 @@ object Libs { name = "jacodb-api-jvm", version = Versions.jacodb ) + val jacodb_ets = dep( + group = jacodbPackage, + name = "jacodb-ets", + version = Versions.jacodb + ) val jacodb_api_common = dep( group = jacodbPackage, name = "jacodb-api-common", diff --git a/usvm-ts/build.gradle.kts b/usvm-ts/build.gradle.kts index 3e75f264ca..f1d7ed9655 100644 --- a/usvm-ts/build.gradle.kts +++ b/usvm-ts/build.gradle.kts @@ -5,17 +5,17 @@ plugins { dependencies { implementation(project(":usvm-core")) - implementation("${Versions.jacodbPackage}:jacodb-core:${Versions.jacodb}") - implementation("${Versions.jacodbPackage}:jacodb-panda-dynamic:${Versions.jacodb}") + implementation(Libs.jacodb_core) + implementation(Libs.jacodb_ets) - implementation("io.ksmt:ksmt-yices:${Versions.ksmt}") - implementation("io.ksmt:ksmt-cvc5:${Versions.ksmt}") - implementation("io.ksmt:ksmt-symfpu:${Versions.ksmt}") - implementation("io.ksmt:ksmt-runner:${Versions.ksmt}") + implementation(Libs.ksmt_yices) + implementation(Libs.ksmt_cvc5) + implementation(Libs.ksmt_symfpu) + implementation(Libs.ksmt_runner) - testImplementation("io.mockk:mockk:${Versions.mockk}") - testImplementation("org.junit.jupiter:junit-jupiter-params:${Versions.junitParams}") - testImplementation("ch.qos.logback:logback-classic:${Versions.logback}") + testImplementation(Libs.mockk) + testImplementation(Libs.junit_jupiter_params) + testImplementation(Libs.logback) // https://mvnrepository.com/artifact/org.burningwave/core // Use it to export all modules to all diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt b/usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt new file mode 100644 index 0000000000..fdfcf48b4a --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt @@ -0,0 +1,36 @@ +package org.usvm + +import org.jacodb.ets.base.EtsStmt +import org.jacodb.ets.graph.EtsApplicationGraph +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsMethod +import org.usvm.statistics.ApplicationGraph + +class TSApplicationGraph(project: EtsFile) : ApplicationGraph { + private val applicationGraph = EtsApplicationGraph(project) + + override fun predecessors(node: EtsStmt): Sequence = + applicationGraph.predecessors(node) + + override fun successors(node: EtsStmt): Sequence = + applicationGraph.successors(node) + + override fun callees(node: EtsStmt): Sequence = + applicationGraph.callees(node) + + override fun callers(method: EtsMethod): Sequence = + applicationGraph.callers(method) + + override fun entryPoints(method: EtsMethod): Sequence = + applicationGraph.entryPoints(method) + + override fun exitPoints(method: EtsMethod): Sequence = + applicationGraph.exitPoints(method) + + override fun methodOf(node: EtsStmt): EtsMethod = + applicationGraph.methodOf(node) + + override fun statementsOf(method: EtsMethod): Sequence = sequence { + method.cfg.stmts.forEach { yield(it) } + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt index 7329747405..f0b1cab323 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt @@ -1,13 +1,19 @@ package org.usvm -import org.jacodb.panda.dynamic.ets.base.EtsType +import io.ksmt.solver.yices.KYicesSolver +import io.ksmt.solver.z3.KZ3Solver +import io.ksmt.symfpu.solver.KSymFpuSolver +import org.jacodb.ets.base.EtsType import org.usvm.solver.USolverBase +import org.usvm.solver.UTypeSolver import org.usvm.types.UTypeSystem class TSComponents( private val typeSystem: TSTypeSystem, private val options: UMachineOptions ) : UComponents { + private val closeableResources = mutableListOf() + override val useSolverForForks: Boolean get() = TODO("Not yet implemented") @@ -15,11 +21,26 @@ class TSComponents( TODO("Not yet implemented") } - override fun mkTypeSystem(ctx: UContext): UTypeSystem { - TODO("Not yet implemented") - } + override fun mkTypeSystem( + ctx: UContext + ): UTypeSystem = typeSystem override fun > mkSolver(ctx: Context): USolverBase { - TODO("Not yet implemented") + val (translator, decoder) = buildTranslatorAndLazyDecoder(ctx) + + val smtSolver = when (options.solverType) { + SolverType.YICES -> KSymFpuSolver(KYicesSolver(ctx), ctx) + SolverType.Z3 -> KZ3Solver(ctx) + } + + closeableResources += smtSolver + + val typeSolver = UTypeSolver(typeSystem) + + return USolverBase(ctx, smtSolver, typeSolver, translator, decoder, options.solverTimeout) + } + + fun close() { + closeableResources.forEach(AutoCloseable::close) } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt new file mode 100644 index 0000000000..66a241b5b3 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt @@ -0,0 +1,77 @@ +package org.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.base.EtsStmt +import org.jacodb.ets.base.EtsType +import org.jacodb.ets.model.EtsMethod +import org.usvm.forkblacklists.UForkBlackList +import org.usvm.memory.URegisterStackLValue +import org.usvm.solver.USatResult +import org.usvm.state.TSMethodResult +import org.usvm.state.TSState +import org.usvm.state.lastStmt +import org.usvm.targets.UTargetsSet + +class TSInterpreter( + private val ctx: TSContext, + private val applicationGraph: TSApplicationGraph +) : UInterpreter() { + private val forkBlackList: UForkBlackList = UForkBlackList.createDefault() + + override fun step(state: TSState): StepResult { + val stmt = state.lastStmt + val scope = StepScope(state, forkBlackList) + + val result = state.methodResult + if (result is TSMethodResult.TSException) { + // TODO catch processing + scope.doWithState { + val returnSite = callStack.pop() + + if (callStack.isNotEmpty()) { + memory.stack.pop() + } + + if (returnSite != null) { + newStmt(returnSite) + } + } + + return scope.stepResult() + } + + // TODO: interpreter + stmt.nextStmt?.let { nextStmt -> + scope.doWithState { newStmt(nextStmt) } + } + + return scope.stepResult() + } + + fun getInitialState(method: EtsMethod, targets: List): TSState { + val state = TSState(ctx, method, targets = UTargetsSet.from(targets)) + + with(ctx) { + val params = List(method.parameters.size) { idx -> + URegisterStackLValue(addressSort, idx) + } + val refs = params.map { state.memory.read(it) } + + // TODO check correctness of constraints and process this instance + state.pathConstraints += mkAnd(refs.map { mkEq(it.asExpr(addressSort), nullRef).not() }) + } + + val solver = ctx.solver() + val model = (solver.check(state.pathConstraints) as USatResult).model + state.models = listOf(model) + + state.callStack.push(method, returnSite = null) + state.memory.stack.push(method.parameters.size, method.localsCount) + state.pathNode += method.cfg.instructions.first() + + return state + } + + // TODO: expand with interpreter implementation + private val EtsStmt.nextStmt get() = applicationGraph.successors(this).firstOrNull() +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt index 62c5c5a1e1..4e56356488 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt @@ -1,11 +1,110 @@ package org.usvm +import org.jacodb.ets.base.EtsStmt +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsMethod +import org.usvm.ps.createPathSelector +import org.usvm.state.TSMethodResult import org.usvm.state.TSState +import org.usvm.statistics.CompositeUMachineObserver +import org.usvm.statistics.CoverageStatistics +import org.usvm.statistics.StepsStatistics +import org.usvm.statistics.TimeStatistics +import org.usvm.statistics.UMachineObserver +import org.usvm.statistics.collectors.AllStatesCollector +import org.usvm.statistics.collectors.CoveredNewStatesCollector +import org.usvm.statistics.collectors.TargetsReachedStatesCollector +import org.usvm.statistics.distances.CfgStatisticsImpl +import org.usvm.statistics.distances.PlainCallGraphStatistics +import org.usvm.stopstrategies.createStopStrategy +import kotlin.time.Duration.Companion.seconds class TSMachine( - private val options: UMachineOptions + private val project: EtsFile, + private val options: UMachineOptions, ) : UMachine() { + private val typeSystem = TSTypeSystem(typeOperationsTimeout = 1.seconds, project) + private val components = TSComponents(typeSystem, options) + private val ctx = TSContext(components) + private val applicationGraph = TSApplicationGraph(project) + private val interpreter = TSInterpreter(ctx, applicationGraph) + private val cfgStatistics = CfgStatisticsImpl(applicationGraph) + + fun analyze( + methods: List, + targets: List = emptyList(), + ): List { + val initialStates = mutableMapOf() + methods.forEach { initialStates[it] = interpreter.getInitialState(it, targets) } + + val methodsToTrackCoverage = + when (options.coverageZone) { + CoverageZone.METHOD, CoverageZone.TRANSITIVE -> methods.toHashSet() + CoverageZone.CLASS -> TODO("Unsupported yet") + } + + val coverageStatistics = CoverageStatistics( + methodsToTrackCoverage, + applicationGraph + ) + + val callGraphStatistics: PlainCallGraphStatistics = + when (options.targetSearchDepth) { + 0u -> PlainCallGraphStatistics() + else -> TODO("Unsupported yet") + } + + val timeStatistics = TimeStatistics() + + val pathSelector = createPathSelector( + initialStates, + options, + applicationGraph, + timeStatistics, + { coverageStatistics }, + { cfgStatistics }, + { callGraphStatistics }, + ) + + val statesCollector = + when (options.stateCollectionStrategy) { + StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector(coverageStatistics) { + it.methodResult is TSMethodResult.TSException + } + + StateCollectionStrategy.REACHED_TARGET -> TargetsReachedStatesCollector() + StateCollectionStrategy.ALL -> AllStatesCollector() + } + + val observers = mutableListOf>(coverageStatistics) + observers.add(statesCollector) + + val stepsStatistics = StepsStatistics() + + val stopStrategy = createStopStrategy( + options, + targets, + timeStatisticsFactory = { timeStatistics }, + stepsStatisticsFactory = { stepsStatistics }, + coverageStatisticsFactory = { coverageStatistics }, + getCollectedStatesCount = { statesCollector.collectedStates.size } + ) + + observers.add(timeStatistics) + observers.add(stepsStatistics) + + run( + interpreter, + pathSelector, + observer = CompositeUMachineObserver(observers), + isStateTerminated = { state -> state.callStack.isEmpty() }, + stopStrategy = stopStrategy + ) + + return statesCollector.collectedStates + } + override fun close() { - TODO("Not yet implemented") + components.close() } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt index 9539dba8af..d47255e6f2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt @@ -1,6 +1,6 @@ package org.usvm -import org.jacodb.panda.dynamic.ets.base.EtsStmt +import org.jacodb.ets.base.EtsStmt import org.usvm.targets.UTarget class TSTarget : UTarget() { diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSTest.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTest.kt index 308347c5da..4b994ca1a0 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSTest.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTest.kt @@ -1,6 +1,6 @@ package org.usvm -import org.jacodb.panda.dynamic.ets.base.EtsStmt +import org.jacodb.ets.base.EtsStmt class TSTest( val parameters: List, diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt index 670b106ae2..cbf9748444 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt @@ -1,12 +1,14 @@ package org.usvm -import org.jacodb.panda.dynamic.ets.base.EtsType +import org.jacodb.ets.base.EtsType +import org.jacodb.ets.model.EtsFile import org.usvm.types.UTypeStream import org.usvm.types.UTypeSystem import kotlin.time.Duration class TSTypeSystem( override val typeOperationsTimeout: Duration, + val project: EtsFile ) : UTypeSystem { override fun isSupertype(supertype: EtsType, type: EtsType): Boolean { TODO("Not yet implemented") diff --git a/usvm-ts/src/main/kotlin/org/usvm/Util.kt b/usvm-ts/src/main/kotlin/org/usvm/Util.kt new file mode 100644 index 0000000000..47bf55378a --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/Util.kt @@ -0,0 +1,8 @@ +package org.usvm + +import org.jacodb.ets.base.EtsStmt +import org.usvm.state.TSState + +fun TSState.newStmt(stmt: EtsStmt) { + pathNode += stmt +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/state/TSMethodResult.kt b/usvm-ts/src/main/kotlin/org/usvm/state/TSMethodResult.kt index 40f72c664e..2936bc6182 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/state/TSMethodResult.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/state/TSMethodResult.kt @@ -1,7 +1,7 @@ package org.usvm.state -import org.jacodb.panda.dynamic.api.PandaMethod -import org.jacodb.panda.dynamic.api.PandaType +import org.jacodb.ets.base.EtsType +import org.jacodb.ets.model.EtsMethod import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort @@ -19,7 +19,7 @@ interface TSMethodResult { * A [method] successfully returned a [value]. */ class Success( - val method: PandaMethod, + val method: EtsMethod, val value: UExpr, ) : TSMethodResult @@ -28,7 +28,7 @@ interface TSMethodResult { */ open class TSException( val address: UHeapRef, - val type: PandaType, + val type: EtsType, ) : TSMethodResult { override fun toString(): String = "${this::class.simpleName}: Address: $address, type: ${type.typeName}" } diff --git a/usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt b/usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt index 57dd2393b0..519422b531 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt @@ -1,8 +1,8 @@ package org.usvm.state -import org.jacodb.panda.dynamic.ets.base.EtsStmt -import org.jacodb.panda.dynamic.ets.base.EtsType -import org.jacodb.panda.dynamic.ets.model.EtsMethod +import org.jacodb.ets.base.EtsStmt +import org.jacodb.ets.base.EtsType +import org.jacodb.ets.model.EtsMethod import org.usvm.PathNode import org.usvm.TSContext import org.usvm.TSTarget @@ -16,7 +16,7 @@ import org.usvm.targets.UTargetsSet class TSState( ctx: TSContext, override val entrypoint: EtsMethod, - callStack: UCallStack, + callStack: UCallStack = UCallStack(), pathConstraints: UPathConstraints = UPathConstraints(ctx), memory: UMemory = UMemory(ctx, pathConstraints.typeConstraints), models: List> = listOf(), @@ -28,9 +28,22 @@ class TSState( ctx, callStack, pathConstraints, memory, models, pathNode, forkPoints, targets ) { override fun clone(newConstraints: UPathConstraints?): TSState { - TODO("Not yet implemented") + val clonedConstraints = newConstraints ?: pathConstraints.clone() + + return TSState( + ctx, + entrypoint, + callStack.clone(), + clonedConstraints, + memory.clone(clonedConstraints.typeConstraints), + models, + pathNode, + forkPoints, + methodResult, + targets.clone(), + ) } override val isExceptional: Boolean - get() = TODO("Not yet implemented") + get() = methodResult is TSMethodResult.TSException } diff --git a/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt new file mode 100644 index 0000000000..1d65cdb8c4 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt @@ -0,0 +1,3 @@ +package org.usvm.state + +val TSState.lastStmt get() = pathNode.statement diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/MinValue.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/MinValue.kt new file mode 100644 index 0000000000..9d82eb926f --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/MinValue.kt @@ -0,0 +1,22 @@ +package org.usvm.samples + +import org.junit.jupiter.api.Disabled +import org.usvm.util.MethodDescriptor +import org.usvm.util.TSMethodTestRunner +import kotlin.test.Test + +@Disabled("Not yet implemented") +class MinValue : TSMethodTestRunner() { + + @Test + fun testMinValue() { + discoverProperties( + methodIdentifier = MethodDescriptor( + fileName = "MinValue", + className = globalClassName, + methodName = "findMinValue", + argumentsNumber = 1 + ) + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/TSMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt similarity index 69% rename from usvm-ts/src/test/kotlin/org/usvm/samples/TSMethodTestRunner.kt rename to usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt index ce49e23685..03da7ee23a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/TSMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt @@ -1,14 +1,24 @@ -package org.usvm.samples +package org.usvm.util -import org.jacodb.panda.dynamic.ets.base.EtsType +import org.jacodb.ets.base.EtsType +import org.jacodb.ets.dto.EtsFileDto +import org.jacodb.ets.dto.convertToEtsFile +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsMethod +import org.usvm.PathSelectionStrategy +import org.usvm.TSMachine import org.usvm.TSMethodCoverage import org.usvm.TSTest import org.usvm.UMachineOptions import org.usvm.test.util.TestRunner import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults +import kotlin.time.Duration +import kotlin.time.Duration.Companion.milliseconds open class TSMethodTestRunner : TestRunner() { + protected val globalClassName = "_DEFAULT_ARK_CLASS" + protected inline fun discoverProperties( methodIdentifier: MethodDescriptor, vararg analysisResultMatchers: (R?) -> Boolean, @@ -110,21 +120,58 @@ open class TSMethodTestRunner : TestRunner EtsType - get() = TODO() + get() = TODO("Not yet implemented") - @Suppress("UNUSED_ANONYMOUS_PARAMETER") override val checkType: (EtsType?, EtsType?) -> Boolean - get() = TODO() + get() = TODO("Not yet implemented") + + private fun getProject(fileName: String): EtsFile { + val jsonWithoutExtension = "/ir/${fileName}.json" + val sampleFilePath = javaClass.getResourceAsStream(jsonWithoutExtension) + ?: error("Resource not found: $jsonWithoutExtension") + + val etsFileDto = EtsFileDto.loadFromJson(sampleFilePath) + + return convertToEtsFile(etsFileDto) + } + + private fun EtsFile.getMethodByDescriptor(desc: MethodDescriptor): EtsMethod { + val cls = classes.find { it.name == desc.className } + ?: error("No class ${desc.className} in project $name") + + return cls.methods.find { it.name == desc.methodName && it.parameters.size == desc.argumentsNumber } + ?: error("No method matching $desc found in $name") + + } override val runner: (MethodDescriptor, UMachineOptions) -> List - get() = TODO() + get() = { id, options -> + val project = getProject(id.fileName) + val method = project.getMethodByDescriptor(id) + + TSMachine(project, options).use { machine -> + val states = machine.analyze(listOf(method)) + states.map { state -> + val resolver = TSTestResolver() + resolver.resolve(method, state).also { println(it) } + } + } + } override val coverageRunner: (List) -> TSMethodCoverage = TODO() - override var options: UMachineOptions = TODO() + override var options: UMachineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM), + exceptionsPropagation = true, + timeout = 60_000.milliseconds, + stepsFromLastCovered = 3500L, + solverTimeout = Duration.INFINITE, // we do not need the timeout for a solver in tests + typeOperationsTimeout = Duration.INFINITE, // we do not need the timeout for type operations in tests + ) } data class MethodDescriptor( + val fileName: String, val className: String, val methodName: String, val argumentsNumber: Int, diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt new file mode 100644 index 0000000000..171ee8281d --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt @@ -0,0 +1,12 @@ +package org.usvm.util + +import org.jacodb.ets.model.EtsMethod +import org.usvm.TSTest +import org.usvm.state.TSState + +@Suppress("UNUSED_PARAMETER") +class TSTestResolver { + fun resolve(method: EtsMethod, state: TSState): TSTest { + TODO() + } +} diff --git a/usvm-ts/src/test/resources/ir/MinValue.json b/usvm-ts/src/test/resources/ir/MinValue.json new file mode 100644 index 0000000000..b15a43a931 --- /dev/null +++ b/usvm-ts/src/test/resources/ir/MinValue.json @@ -0,0 +1,636 @@ +{ + "name": "MinValue.ts", + "namespaces": [], + "classes": [ + { + "signature": { + "name": "_DEFAULT_ARK_CLASS" + }, + "modifiers": [], + "typeParameters": [], + "superClassName": "", + "implementedInterfaceNames": [], + "fields": [], + "methods": [ + { + "signature": { + "enclosingClass": { + "name": "_DEFAULT_ARK_CLASS" + }, + "name": "_DEFAULT_ARK_METHOD", + "parameters": [], + "returnType": { + "_": "UnknownType" + } + }, + "modifiers": [], + "typeParameters": [], + "body": { + "locals": [ + { + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "_DEFAULT_ARK_CLASS" + } + } + } + ], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "_DEFAULT_ARK_CLASS" + } + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "_DEFAULT_ARK_CLASS" + } + } + } + }, + { + "_": "ReturnVoidStmt" + } + ] + } + ] + } + } + }, + { + "signature": { + "enclosingClass": { + "name": "_DEFAULT_ARK_CLASS" + }, + "name": "findMinValue", + "parameters": [ + { + "name": "arr", + "type": { + "_": "UnclearReferenceType", + "name": "ArrayType" + }, + "isOptional": false + } + ], + "returnType": { + "_": "NumberType" + } + }, + "modifiers": [], + "typeParameters": [], + "body": { + "locals": [ + { + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "_DEFAULT_ARK_CLASS" + } + } + }, + { + "name": "arr", + "type": { + "_": "UnclearReferenceType", + "name": "ArrayType" + } + }, + { + "name": "$temp0", + "type": { + "_": "UnknownType" + } + }, + { + "name": "$temp1", + "type": { + "_": "ClassType", + "signature": { + "name": "Error" + } + } + }, + { + "name": "minValue", + "type": { + "_": "UnknownType" + } + }, + { + "name": "i", + "type": { + "_": "NumberType" + } + }, + { + "name": "$temp2", + "type": { + "_": "UnknownType" + } + }, + { + "name": "$temp3", + "type": { + "_": "UnknownType" + } + } + ], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [ + 1, + 6 + ], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "arr", + "type": { + "_": "UnclearReferenceType", + "name": "ArrayType" + } + }, + "right": { + "_": "ParameterRef", + "index": 0, + "type": { + "_": "UnclearReferenceType", + "name": "ArrayType" + } + } + }, + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "_DEFAULT_ARK_CLASS" + } + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "_DEFAULT_ARK_CLASS" + } + } + } + }, + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "$temp0", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "InstanceFieldRef", + "instance": { + "_": "Local", + "name": "arr", + "type": { + "_": "UnclearReferenceType", + "name": "ArrayType" + } + }, + "field": { + "enclosingClass": { + "name": "" + }, + "name": "length", + "fieldType": { + "_": "UnknownType" + } + } + } + }, + { + "_": "IfStmt", + "condition": { + "_": "ConditionExpr", + "op": "!==", + "left": { + "_": "Local", + "name": "$temp0", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "Constant", + "value": "0", + "type": { + "_": "NumberType" + } + }, + "type": { + "_": "BooleanType" + } + } + } + ] + }, + { + "id": 1, + "successors": [ + 2 + ], + "predecessors": [ + 0, + 6 + ], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "minValue", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "InstanceFieldRef", + "instance": { + "_": "Local", + "name": "arr", + "type": { + "_": "UnclearReferenceType", + "name": "ArrayType" + } + }, + "field": { + "enclosingClass": { + "name": "" + }, + "name": "0", + "fieldType": { + "_": "UnknownType" + } + } + } + } + ] + }, + { + "id": 2, + "successors": [ + 3, + 4 + ], + "predecessors": [ + 1, + 4, + 5 + ], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "i", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "Constant", + "value": "1", + "type": { + "_": "NumberType" + } + } + }, + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "$temp2", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "InstanceFieldRef", + "instance": { + "_": "Local", + "name": "arr", + "type": { + "_": "UnclearReferenceType", + "name": "ArrayType" + } + }, + "field": { + "enclosingClass": { + "name": "" + }, + "name": "length", + "fieldType": { + "_": "UnknownType" + } + } + } + }, + { + "_": "IfStmt", + "condition": { + "_": "ConditionExpr", + "op": ">=", + "left": { + "_": "Local", + "name": "i", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "Local", + "name": "$temp2", + "type": { + "_": "UnknownType" + } + }, + "type": { + "_": "BooleanType" + } + } + }, + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "i", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "BinopExpr", + "op": "+", + "left": { + "_": "Local", + "name": "i", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "Constant", + "value": "1", + "type": { + "_": "NumberType" + } + } + } + } + ] + }, + { + "id": 3, + "successors": [], + "predecessors": [ + 2 + ], + "stmts": [ + { + "_": "ReturnStmt", + "arg": { + "_": "Local", + "name": "minValue", + "type": { + "_": "UnknownType" + } + } + } + ] + }, + { + "id": 4, + "successors": [ + 2, + 5 + ], + "predecessors": [ + 2 + ], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "$temp3", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "InstanceFieldRef", + "instance": { + "_": "Local", + "name": "arr", + "type": { + "_": "UnclearReferenceType", + "name": "ArrayType" + } + }, + "field": { + "enclosingClass": { + "name": "" + }, + "name": "i", + "fieldType": { + "_": "UnknownType" + } + } + } + }, + { + "_": "IfStmt", + "condition": { + "_": "ConditionExpr", + "op": ">=", + "left": { + "_": "Local", + "name": "$temp3", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "Local", + "name": "minValue", + "type": { + "_": "UnknownType" + } + }, + "type": { + "_": "BooleanType" + } + } + } + ] + }, + { + "id": 5, + "successors": [ + 2 + ], + "predecessors": [ + 4 + ], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "minValue", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "InstanceFieldRef", + "instance": { + "_": "Local", + "name": "arr", + "type": { + "_": "UnclearReferenceType", + "name": "ArrayType" + } + }, + "field": { + "enclosingClass": { + "name": "" + }, + "name": "i", + "fieldType": { + "_": "UnknownType" + } + } + } + } + ] + }, + { + "id": 6, + "successors": [ + 1 + ], + "predecessors": [ + 0 + ], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "$temp1", + "type": { + "_": "ClassType", + "signature": { + "name": "Error" + } + } + }, + "right": { + "_": "NewExpr", + "classType": { + "_": "ClassType", + "signature": { + "name": "Error" + } + } + } + }, + { + "_": "CallStmt", + "expr": { + "_": "InstanceCallExpr", + "instance": { + "_": "Local", + "name": "$temp1", + "type": { + "_": "ClassType", + "signature": { + "name": "Error" + } + } + }, + "method": { + "enclosingClass": { + "name": "Error" + }, + "name": "constructor", + "parameters": [], + "returnType": { + "_": "UnknownType" + } + }, + "args": [ + { + "_": "Constant", + "value": "Array is empty!", + "type": { + "_": "StringType" + } + } + ] + } + }, + { + "_": "ThrowStmt", + "arg": { + "_": "Local", + "name": "$temp1", + "type": { + "_": "ClassType", + "signature": { + "name": "Error" + } + } + } + } + ] + } + ] + } + } + } + ] + } + ], + "importInfos": [], + "exportInfos": [] +} diff --git a/usvm-ts/src/test/resources/samples/MinValue.ts b/usvm-ts/src/test/resources/samples/MinValue.ts new file mode 100644 index 0000000000..58d7531344 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/MinValue.ts @@ -0,0 +1,11 @@ +function findMinValue(arr: number[]): number { + if (arr.length === 0) throw new Error("Array is empty!"); + + let minValue = arr[0]; + for (let i = 1; i < arr.length; i++) { + if (arr[i] < minValue) { + minValue = arr[i]; + } + } + return minValue; +} From db8b0f7e7ada57698330b3da4a91a7d1f8349b09 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Thu, 18 Jul 2024 15:22:35 +0300 Subject: [PATCH 4/6] Remove a redundant file --- buildSrc/src/main/kotlin/Versions.kt | 0 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 buildSrc/src/main/kotlin/Versions.kt diff --git a/buildSrc/src/main/kotlin/Versions.kt b/buildSrc/src/main/kotlin/Versions.kt deleted file mode 100644 index e69de29bb2..0000000000 From 080b6176e214a2316cf5f7c571b572eeb29ed67e Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 23 Jul 2024 11:49:06 +0300 Subject: [PATCH 5/6] Remove yield from the code --- usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt b/usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt index fdfcf48b4a..dc734e37b4 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt @@ -30,7 +30,6 @@ class TSApplicationGraph(project: EtsFile) : ApplicationGraph = sequence { - method.cfg.stmts.forEach { yield(it) } - } + override fun statementsOf(method: EtsMethod): Sequence = + method.cfg.stmts.asSequence() } From 4eb7c06dbf47b77c1060edb4789cb712f063794c Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 23 Jul 2024 12:08:09 +0300 Subject: [PATCH 6/6] Detekt fixes --- usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt | 4 ++-- usvm-ts/src/main/kotlin/org/usvm/TSContext.kt | 4 +--- usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt | 2 +- usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt | 3 +-- usvm-ts/src/main/kotlin/org/usvm/TSTest.kt | 4 ++-- usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt | 2 +- usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt | 9 ++++++++- .../src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt | 3 +-- 8 files changed, 17 insertions(+), 14 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt index f0b1cab323..15671ef2c2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt @@ -10,7 +10,7 @@ import org.usvm.types.UTypeSystem class TSComponents( private val typeSystem: TSTypeSystem, - private val options: UMachineOptions + private val options: UMachineOptions, ) : UComponents { private val closeableResources = mutableListOf() @@ -22,7 +22,7 @@ class TSComponents( } override fun mkTypeSystem( - ctx: UContext + ctx: UContext, ): UTypeSystem = typeSystem override fun > mkSolver(ctx: Context): USolverBase { diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt index 26269b4793..8e6660bdb4 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt @@ -2,6 +2,4 @@ package org.usvm typealias TSSizeSort = UBv32Sort -class TSContext(components: TSComponents) : UContext(components) { - -} +class TSContext(components: TSComponents) : UContext(components) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt index 66a241b5b3..d514bbb2ef 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt @@ -14,7 +14,7 @@ import org.usvm.targets.UTargetsSet class TSInterpreter( private val ctx: TSContext, - private val applicationGraph: TSApplicationGraph + private val applicationGraph: TSApplicationGraph, ) : UInterpreter() { private val forkBlackList: UForkBlackList = UForkBlackList.createDefault() diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt index d47255e6f2..4b728f6c74 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt @@ -3,5 +3,4 @@ package org.usvm import org.jacodb.ets.base.EtsStmt import org.usvm.targets.UTarget -class TSTarget : UTarget() { -} +class TSTarget : UTarget() diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSTest.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTest.kt index 4b994ca1a0..16a2ac28c1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSTest.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTest.kt @@ -5,7 +5,7 @@ import org.jacodb.ets.base.EtsStmt class TSTest( val parameters: List, val resultValue: Any?, - val trace: List? = null + val trace: List? = null, ) -class TSMethodCoverage \ No newline at end of file +class TSMethodCoverage diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt index cbf9748444..aa2ccfc21b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt @@ -8,7 +8,7 @@ import kotlin.time.Duration class TSTypeSystem( override val typeOperationsTimeout: Duration, - val project: EtsFile + val project: EtsFile, ) : UTypeSystem { override fun isSupertype(supertype: EtsType, type: EtsType): Boolean { TODO("Not yet implemented") diff --git a/usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt b/usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt index 519422b531..d22857a653 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt @@ -25,7 +25,14 @@ class TSState( var methodResult: TSMethodResult = TSMethodResult.NoCall, targets: UTargetsSet = UTargetsSet.empty(), ) : UState( - ctx, callStack, pathConstraints, memory, models, pathNode, forkPoints, targets + ctx, + callStack, + pathConstraints, + memory, + models, + pathNode, + forkPoints, + targets ) { override fun clone(newConstraints: UPathConstraints?): TSState { val clonedConstraints = newConstraints ?: pathConstraints.clone() 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 03da7ee23a..56944aafcb 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt @@ -126,7 +126,7 @@ open class TSMethodTestRunner : TestRunner List