From f4422a3156109e7773cbbbd64b95eb950117111b Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 23 Jul 2024 18:14:19 +0300 Subject: [PATCH] Introduction of TypeScript symbolic machine (#197) --- buildSrc/src/main/kotlin/Dependencies.kt | 5 + settings.gradle.kts | 1 + usvm-ts/build.gradle.kts | 23 + .../kotlin/org/usvm/TSApplicationGraph.kt | 35 + .../src/main/kotlin/org/usvm/TSComponents.kt | 46 ++ usvm-ts/src/main/kotlin/org/usvm/TSContext.kt | 5 + .../src/main/kotlin/org/usvm/TSInterpreter.kt | 77 +++ usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt | 110 +++ usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt | 6 + usvm-ts/src/main/kotlin/org/usvm/TSTest.kt | 11 + .../src/main/kotlin/org/usvm/TSTypeSystem.kt | 36 + usvm-ts/src/main/kotlin/org/usvm/Util.kt | 8 + .../kotlin/org/usvm/state/TSMethodResult.kt | 35 + .../src/main/kotlin/org/usvm/state/TSState.kt | 56 ++ .../kotlin/org/usvm/state/TSStateUtils.kt | 3 + .../test/kotlin/org/usvm/samples/MinValue.kt | 22 + .../org/usvm/util/TSMethodTestRunner.kt | 177 +++++ .../kotlin/org/usvm/util/TSTestResolver.kt | 12 + usvm-ts/src/test/resources/ir/MinValue.json | 636 ++++++++++++++++++ .../src/test/resources/samples/MinValue.ts | 11 + 20 files changed, 1315 insertions(+) create mode 100644 usvm-ts/build.gradle.kts create mode 100644 usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt 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/TSInterpreter.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/TSTest.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/Util.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 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 create mode 100644 usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt 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/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..f1d7ed9655 --- /dev/null +++ b/usvm-ts/build.gradle.kts @@ -0,0 +1,23 @@ +plugins { + id("usvm.kotlin-conventions") +} + +dependencies { + implementation(project(":usvm-core")) + + implementation(Libs.jacodb_core) + implementation(Libs.jacodb_ets) + + implementation(Libs.ksmt_yices) + implementation(Libs.ksmt_cvc5) + implementation(Libs.ksmt_symfpu) + implementation(Libs.ksmt_runner) + + 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 + testImplementation("org.burningwave:core:12.62.7") +} 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..dc734e37b4 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt @@ -0,0 +1,35 @@ +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 = + method.cfg.stmts.asSequence() +} 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..15671ef2c2 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt @@ -0,0 +1,46 @@ +package org.usvm + +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") + + override fun > mkSizeExprProvider(ctx: Context): USizeExprProvider { + TODO("Not yet implemented") + } + + override fun mkTypeSystem( + ctx: UContext, + ): UTypeSystem = typeSystem + + override fun > mkSolver(ctx: Context): USolverBase { + 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/TSContext.kt b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt new file mode 100644 index 0000000000..8e6660bdb4 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt @@ -0,0 +1,5 @@ +package org.usvm + +typealias TSSizeSort = UBv32Sort + +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 new file mode 100644 index 0000000000..d514bbb2ef --- /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 new file mode 100644 index 0000000000..4e56356488 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt @@ -0,0 +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 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() { + components.close() + } +} 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..4b728f6c74 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTarget.kt @@ -0,0 +1,6 @@ +package org.usvm + +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 new file mode 100644 index 0000000000..16a2ac28c1 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTest.kt @@ -0,0 +1,11 @@ +package org.usvm + +import org.jacodb.ets.base.EtsStmt + +class TSTest( + val parameters: List, + val resultValue: Any?, + val trace: List? = null, +) + +class TSMethodCoverage 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..aa2ccfc21b --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt @@ -0,0 +1,36 @@ +package org.usvm + +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") + } + + 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/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 new file mode 100644 index 0000000000..2936bc6182 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/state/TSMethodResult.kt @@ -0,0 +1,35 @@ +package org.usvm.state + +import org.jacodb.ets.base.EtsType +import org.jacodb.ets.model.EtsMethod +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: EtsMethod, + val value: UExpr, + ) : TSMethodResult + + /** + * A method threw an exception with [type] type. + */ + open class TSException( + val address: UHeapRef, + 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 new file mode 100644 index 0000000000..d22857a653 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt @@ -0,0 +1,56 @@ +package org.usvm.state + +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 +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 = 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 { + 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() = 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/util/TSMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt new file mode 100644 index 0000000000..56944aafcb --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt @@ -0,0 +1,177 @@ +package org.usvm.util + +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, + 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("Not yet implemented") + + override val checkType: (EtsType?, EtsType?) -> Boolean + 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() = { 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 = 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; +}