From 080b41c6866e5a6eb68cd0e814f5f7805e06bd92 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Thu, 13 Feb 2025 16:46:29 +0300 Subject: [PATCH 01/12] Resolver draft --- .../ts/test/EtsProjectAnalysisTest.kt | 14 +- .../src/main/kotlin/org/usvm/api/TsTest.kt | 15 +- .../org/usvm/util/TSMethodTestRunner.kt | 14 +- .../kotlin/org/usvm/util/TSTestResolver.kt | 133 +++++++++++++----- 4 files changed, 124 insertions(+), 52 deletions(-) diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt index 194229d18..872e4d64d 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt @@ -45,8 +45,8 @@ import kotlin.time.Duration.Companion.seconds private val logger = KotlinLogging.logger {} class EtsProjectAnalysisTest { - private var tsLinesSuccess = 0L - private var tsLinesFailed = 0L + private var TsLinesSuccess = 0L + private var TsLinesFailed = 0L private var analysisTime: Duration = Duration.ZERO private var totalPathEdges = 0 private var totalSinks: MutableList> = mutableListOf() @@ -93,9 +93,9 @@ class EtsProjectAnalysisTest { private fun makeReport() { logger.info { "Analysis Report On $PROJECT_PATH" } logger.info { "====================" } - logger.info { "Total files processed: ${tsLinesSuccess + tsLinesFailed}" } - logger.info { "Successfully processed lines: $tsLinesSuccess" } - logger.info { "Failed lines: $tsLinesFailed" } + logger.info { "Total files processed: ${TsLinesSuccess + TsLinesFailed}" } + logger.info { "Successfully processed lines: $TsLinesSuccess" } + logger.info { "Failed lines: $TsLinesFailed" } logger.info { "Total analysis time: $analysisTime" } logger.info { "Total path edges: $totalPathEdges" } logger.info { "Found sinks: ${totalSinks.size}" } @@ -130,11 +130,11 @@ class EtsProjectAnalysisTest { runAnalysis(project) val endTime = System.currentTimeMillis() analysisTime += (endTime - startTime).milliseconds - tsLinesSuccess += fileLines + TsLinesSuccess += fileLines } catch (e: Exception) { logger.warn { "Failed to process '$filename': $e" } logger.warn { e.stackTraceToString() } - tsLinesFailed += fileLines + TsLinesFailed += fileLines } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt index 53716b181..731dc69fe 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt @@ -1,13 +1,26 @@ package org.usvm.api import org.jacodb.ets.base.EtsStmt +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsField +import org.jacodb.ets.model.EtsMethod data class TsTest( - val parameters: List, + val method: EtsMethod, + val before: TsParametersState, + val after: TsParametersState, val returnValue: TsObject, val trace: List? = null, ) +data class TsParametersState( + val thisInstance: TsObject?, + val parameters: List, + val globals: Map> +) + +data class GlobalFieldValue(val field: EtsField, val value: TsObject) // TODO is it right????? + open class TsMethodCoverage object NoCoverage : TsMethodCoverage() 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 b7110ab1e..767632fe9 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt @@ -54,7 +54,7 @@ abstract class TsMethodTestRunner : TestRunner r.parameters + r.returnValue }, + extractValuesToCheck = { r -> r.before.parameters + r.returnValue }, expectedTypesForExtractedValues = arrayOf(typeTransformer(R::class)), checkMode = CheckMode.MATCH_PROPERTIES, coverageChecker = coverageChecker @@ -72,7 +72,7 @@ abstract class TsMethodTestRunner : TestRunner r.parameters + r.returnValue }, + extractValuesToCheck = { r -> r.before.parameters + r.returnValue }, expectedTypesForExtractedValues = arrayOf(typeTransformer(T::class), typeTransformer(R::class)), checkMode = CheckMode.MATCH_PROPERTIES, coverageChecker = coverageChecker @@ -90,7 +90,7 @@ abstract class TsMethodTestRunner : TestRunner r.parameters + r.returnValue }, + extractValuesToCheck = { r -> r.before.parameters + r.returnValue }, expectedTypesForExtractedValues = arrayOf( typeTransformer(T1::class), typeTransformer(T2::class), typeTransformer(R::class) ), @@ -110,7 +110,7 @@ abstract class TsMethodTestRunner : TestRunner r.parameters + r.returnValue }, + extractValuesToCheck = { r -> r.before.parameters + r.returnValue }, expectedTypesForExtractedValues = arrayOf( typeTransformer(T1::class), typeTransformer(T2::class), @@ -133,7 +133,7 @@ abstract class TsMethodTestRunner : TestRunner r.parameters + r.returnValue }, + extractValuesToCheck = { r -> r.before.parameters + r.returnValue }, expectedTypesForExtractedValues = arrayOf( typeTransformer(T1::class), typeTransformer(T2::class), @@ -196,8 +196,8 @@ abstract class TsMethodTestRunner : TestRunner val states = machine.analyze(listOf(method)) states.map { state -> - val resolver = TsTestResolver(state) - resolver.resolve(method) + val resolver = TsTestResolver() + resolver.resolve(method, state) } } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt index 814deb800..7a38c103c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt @@ -16,6 +16,7 @@ import org.jacodb.ets.base.EtsType import org.jacodb.ets.base.EtsUndefinedType import org.jacodb.ets.base.EtsUnknownType import org.jacodb.ets.base.EtsVoidType +import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassImpl import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodImpl @@ -24,8 +25,10 @@ import org.jacodb.ets.model.EtsMethodSignature import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.USort +import org.usvm.api.GlobalFieldValue import org.usvm.api.TsObject import org.usvm.api.TsTest +import org.usvm.api.TsParametersState import org.usvm.collection.field.UFieldLValue import org.usvm.isTrue import org.usvm.machine.types.FakeType @@ -36,40 +39,91 @@ import org.usvm.machine.expr.extractDouble import org.usvm.machine.expr.extractInt import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState +import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.URegisterStackLValue import org.usvm.model.UModelBase import org.usvm.types.first import org.usvm.types.single -class TsTestResolver( - private val state: TsState, -) { - private val ctx: TsContext get() = state.ctx - - fun resolve(method: EtsMethod): TsTest = with(ctx) { +class TsTestResolver { + fun resolve(method: EtsMethod, state: TsState): TsTest = with(state.ctx) { val model = state.models.first() - when (val methodResult = state.methodResult) { - is TsMethodResult.Success -> { - val value = methodResult.value - val valueToResolve = model.eval(value) - val returnValue = resolveExpr(valueToResolve, method.returnType, model) - val params = resolveParams(method.parameters, this, model) + val memory = state.memory - return TsTest(params, returnValue) - } + val beforeMemoryScope = MemoryScope(this, model, memory, method) + val afterMemoryScope = MemoryScope(this, model, memory, method) - is TsMethodResult.TsException -> { - val params = resolveParams(method.parameters, this, model) - return TsTest(params, TsObject.TsException) - } + val before = beforeMemoryScope.withMode(ResolveMode.MODEL) { (this as MemoryScope).resolveState() } + val after = afterMemoryScope.withMode(ResolveMode.CURRENT) { (this as MemoryScope).resolveState() } - is TsMethodResult.NoCall -> { - TODO() + val result = when (val res = state.methodResult) { + is TsMethodResult.NoCall -> error("No result found") + is TsMethodResult.Success -> { + afterMemoryScope.withMode(ResolveMode.CURRENT) { + resolveExpr(res.value, method.returnType, model) + } } - else -> error("Should not be called") + is TsMethodResult.TsException -> resolveException(res, afterMemoryScope) + } + + return TsTest(method, before, after, result, trace = emptyList()) + } + + private fun resolveException( + res: TsMethodResult.TsException, + afterMemoryScope: MemoryScope, + ): TsObject.TsException { + TODO() + } + + + private class MemoryScope( + ctx: TsContext, + model: UModelBase, + finalStateMemory: UReadOnlyMemory, + method: EtsMethod, + ) : TsTestStateResolver(ctx, model, finalStateMemory, method) { + fun resolveState(): TsParametersState { + val thisInstance = resolveThisInstance() + val parameters = resolveParameters() + + val globals = resolveGlobals() + + return TsParametersState(thisInstance, parameters, globals) } } +} + +open class TsTestStateResolver( + val ctx: TsContext, + private val model: UModelBase, + private val finalStateMemory: UReadOnlyMemory, + val method: EtsMethod +) { + fun resolveExpr( + expr: UExpr, + type: EtsType, + model: UModelBase<*>, + ): TsObject = when { + type is EtsUnknownType && expr is UConcreteHeapRef -> resolveUnknown(expr, model) + type is EtsPrimitiveType -> resolvePrimitive(expr, type) + type is EtsClassType -> resolveClass(expr, type, model) + type is EtsRefType -> TODO() + else -> TODO() + } + + fun resolveThisInstance(): TsObject? { + TODO() + } + + fun resolveParameters(): List { + TODO() + } + + fun resolveGlobals(): Map> { + TODO() + } private fun resolveParams( params: List, @@ -79,7 +133,7 @@ class TsTestResolver( params.map { param -> val sort = typeToSort(param.type).takeUnless { it is TsUnresolvedSort } ?: addressSort val lValue = URegisterStackLValue(sort, param.index) - val expr = state.memory.read(lValue) // TODO error + val expr = finalStateMemory.read(lValue) // TODO error if (param.type is EtsUnknownType) { resolveFakeObject(expr.cast(), model) } else { @@ -89,23 +143,23 @@ class TsTestResolver( } private fun resolveFakeObject(expr: UConcreteHeapRef, model: UModelBase): TsObject { - val type = state.memory.types.getTypeStream(expr.asExpr(ctx.addressSort)).single() as FakeType + val type = finalStateMemory.types.getTypeStream(expr.asExpr(ctx.addressSort)).single() as FakeType return when { model.eval(type.boolTypeExpr).isTrue -> { val lValue = ctx.getIntermediateBoolLValue(expr.address) - val value = state.memory.read(lValue) + val value = finalStateMemory.read(lValue) resolveExpr(model.eval(value), EtsBooleanType, model) } model.eval(type.fpTypeExpr).isTrue -> { val lValue = ctx.getIntermediateFpLValue(expr.address) - val value = state.memory.read(lValue) + val value = finalStateMemory.read(lValue) resolveExpr(model.eval(value), EtsNumberType, model) } model.eval(type.refTypeExpr).isTrue -> { val lValue = ctx.getIntermediateRefLValue(expr.address) - val value = state.memory.read(lValue) + val value = finalStateMemory.read(lValue) resolveExpr(model.eval(value), EtsClassType(ctx.scene.projectAndSdkClasses.first().signature), model) } @@ -113,17 +167,6 @@ class TsTestResolver( } } - private fun resolveExpr( - expr: UExpr, - type: EtsType, - model: UModelBase<*>, - ): TsObject = when { - type is EtsUnknownType && expr is UConcreteHeapRef -> resolveUnknown(expr, model) - type is EtsPrimitiveType -> resolvePrimitive(expr, type) - type is EtsClassType -> resolveClass(expr, type, model) - type is EtsRefType -> TODO() - else -> TODO() - } private fun resolveUnknown( expr: UConcreteHeapRef, @@ -224,4 +267,20 @@ class TsTestResolver( } return TsObject.TsClass(clazz.name, properties) } + + private var resolveMode: ResolveMode = ResolveMode.ERROR + + fun withMode(resolveMode: ResolveMode, body: TsTestStateResolver.() -> R): R { + val prevValue = this.resolveMode + try { + this.resolveMode = resolveMode + return body() + } finally { + this.resolveMode = prevValue + } + } +} + +enum class ResolveMode { + MODEL, CURRENT, ERROR } From 1ac46c8d2ddb06ccc94c754a924845f594453920 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Thu, 13 Feb 2025 17:45:57 +0300 Subject: [PATCH 02/12] Some fixes --- .../usvm/machine/interpreter/TsInterpreter.kt | 19 ++++ .../src/test/kotlin/org/usvm/samples/Null.kt | 2 +- .../kotlin/org/usvm/util/TSTestResolver.kt | 103 +++++++++++------- 3 files changed, 83 insertions(+), 41 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 1bcc42073..35a07413d 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 @@ -4,6 +4,7 @@ import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.base.EtsAssignStmt import org.jacodb.ets.base.EtsCallStmt +import org.jacodb.ets.base.EtsClassType import org.jacodb.ets.base.EtsGotoStmt import org.jacodb.ets.base.EtsIfStmt import org.jacodb.ets.base.EtsLocal @@ -21,6 +22,7 @@ import org.jacodb.ets.model.EtsMethod import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UInterpreter +import org.usvm.api.evalTypeEquals import org.usvm.api.targets.TsTarget import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.forkblacklists.UForkBlackList @@ -202,6 +204,23 @@ class TsInterpreter( ) val solver = ctx.solver() + + val thisInstanceRef = URegisterStackLValue(ctx.addressSort, method.parameters.count()) // TODO check for statics + val thisRef = state.memory.read(thisInstanceRef).asExpr(ctx.addressSort) + + state.pathConstraints += with (ctx) { + mkNot( + mkOr( + ctx.mkHeapRefEq(thisRef, ctx.mkTsNullValue()), + ctx.mkHeapRefEq(thisRef, ctx.mkUndefinedValue()) + ) + ) + } + + // TODO fix incorrect type streams + // val thisTypeConstraint = state.memory.types.evalTypeEquals(thisRef, EtsClassType(method.enclosingClass)) + // state.pathConstraints += thisTypeConstraint + val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt index 9fbae2a2e..dc5390b4f 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt @@ -16,7 +16,7 @@ class Null : TsMethodTestRunner() { EtsScene(listOf(file)) } - @RepeatedTest(20) + @RepeatedTest(1) fun testIsNull() { val method = getMethod("Null", "isNull") discoverProperties( diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt index 7a38c103c..77dd20be5 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt @@ -18,6 +18,7 @@ import org.jacodb.ets.base.EtsUnknownType import org.jacodb.ets.base.EtsVoidType import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassImpl +import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodImpl import org.jacodb.ets.model.EtsMethodParameter @@ -39,6 +40,7 @@ import org.usvm.machine.expr.extractDouble import org.usvm.machine.expr.extractInt import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState +import org.usvm.memory.ULValue import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.URegisterStackLValue import org.usvm.model.UModelBase @@ -60,7 +62,7 @@ class TsTestResolver { is TsMethodResult.NoCall -> error("No result found") is TsMethodResult.Success -> { afterMemoryScope.withMode(ResolveMode.CURRENT) { - resolveExpr(res.value, method.returnType, model) + resolveExpr(res.value, method.returnType) } } @@ -101,66 +103,78 @@ open class TsTestStateResolver( private val finalStateMemory: UReadOnlyMemory, val method: EtsMethod ) { + fun resolveLValue(lValue: ULValue<*, *>, type: EtsType): TsObject { + val expr = memory.read(lValue) + + return resolveExpr(expr, type) + } + fun resolveExpr( expr: UExpr, type: EtsType, - model: UModelBase<*>, ): TsObject = when { - type is EtsUnknownType && expr is UConcreteHeapRef -> resolveUnknown(expr, model) + type is EtsUnknownType && expr is UConcreteHeapRef -> resolveUnknown(expr) type is EtsPrimitiveType -> resolvePrimitive(expr, type) - type is EtsClassType -> resolveClass(expr, type, model) + type is EtsClassType -> resolveClass(expr, type) type is EtsRefType -> TODO() else -> TODO() } fun resolveThisInstance(): TsObject? { - TODO() + val parametersCount = method.parameters.size + val ref = URegisterStackLValue(ctx.addressSort, idx = parametersCount) // TODO check for statics + val type = EtsClassType( + EtsClassSignature( + name = method.enclosingClass.name, + file = method.enclosingClass.file, + namespace = method.enclosingClass.namespace + ) + ) + + return resolveLValue(ref, type) } - fun resolveParameters(): List { - TODO() - } + fun resolveParameters(): List = method.parameters.mapIndexed { idx, param -> + val sort = ctx.typeToSort(param.type) - fun resolveGlobals(): Map> { - TODO() - } + if (sort is TsUnresolvedSort) { + // this means that a fake object was created, and we need to read it from the current memory + val address = finalStateMemory.read(URegisterStackLValue(ctx.addressSort, idx)).asExpr(ctx.addressSort) - private fun resolveParams( - params: List, - ctx: TsContext, - model: UModelBase, - ): List = with(ctx) { - params.map { param -> - val sort = typeToSort(param.type).takeUnless { it is TsUnresolvedSort } ?: addressSort - val lValue = URegisterStackLValue(sort, param.index) - val expr = finalStateMemory.read(lValue) // TODO error - if (param.type is EtsUnknownType) { - resolveFakeObject(expr.cast(), model) - } else { - resolveExpr(model.eval(expr), param.type, model) - } + check(address is UConcreteHeapRef) + + return@mapIndexed resolveFakeObject(address) } + + val ref = URegisterStackLValue(sort, idx) + resolveLValue(ref, param.type) } - private fun resolveFakeObject(expr: UConcreteHeapRef, model: UModelBase): TsObject { + fun resolveGlobals(): Map> { + // TODO + return emptyMap() + } + + private fun resolveFakeObject(expr: UConcreteHeapRef): TsObject { val type = finalStateMemory.types.getTypeStream(expr.asExpr(ctx.addressSort)).single() as FakeType return when { model.eval(type.boolTypeExpr).isTrue -> { val lValue = ctx.getIntermediateBoolLValue(expr.address) - val value = finalStateMemory.read(lValue) - resolveExpr(model.eval(value), EtsBooleanType, model) + val value = memory.read(lValue) + resolveExpr(model.eval(value), EtsBooleanType) } model.eval(type.fpTypeExpr).isTrue -> { val lValue = ctx.getIntermediateFpLValue(expr.address) - val value = finalStateMemory.read(lValue) - resolveExpr(model.eval(value), EtsNumberType, model) + val value = memory.read(lValue) + resolveExpr(model.eval(value), EtsNumberType) } model.eval(type.refTypeExpr).isTrue -> { val lValue = ctx.getIntermediateRefLValue(expr.address) - val value = finalStateMemory.read(lValue) - resolveExpr(model.eval(value), EtsClassType(ctx.scene.projectAndSdkClasses.first().signature), model) + val value = memory.read(lValue) + val ref = model.eval(value) + resolveExpr(ref, EtsClassType(ctx.scene.projectAndSdkClasses.first().signature)) } else -> error("Unsupported") @@ -170,11 +184,10 @@ open class TsTestStateResolver( private fun resolveUnknown( expr: UConcreteHeapRef, - model: UModelBase<*>, ): TsObject { - val typeStream = model.types.getTypeStream(expr) + val typeStream = memory.types.getTypeStream(expr) return (typeStream.first() as? EtsType)?.let { type -> - resolveExpr(expr, type, model) + resolveExpr(expr, type) } ?: TsObject.TsObject(expr.address) } @@ -184,14 +197,14 @@ open class TsTestStateResolver( ): TsObject = when (type) { EtsNumberType -> { when (expr.sort) { - ctx.fp64Sort -> TsObject.TsNumber.Double(extractDouble(expr)) - ctx.bv32Sort -> TsObject.TsNumber.Integer(extractInt(expr)) + ctx.fp64Sort -> TsObject.TsNumber.Double(extractDouble(evaluateInModel(expr))) + ctx.bv32Sort -> TsObject.TsNumber.Integer(extractInt(evaluateInModel(expr))) else -> error("Unexpected sort: ${expr.sort}") } } EtsBooleanType -> { - TsObject.TsBoolean(expr.extractBool()) + TsObject.TsBoolean(evaluateInModel(expr).extractBool()) } EtsUndefinedType -> { @@ -224,7 +237,6 @@ open class TsTestStateResolver( private fun resolveClass( expr: UExpr, classType: EtsClassType, - model: UModelBase<*>, ): TsObject { if (expr is UConcreteHeapRef && expr.address == 0) { return TsObject.TsUndefinedObject @@ -262,7 +274,7 @@ open class TsTestStateResolver( val sort = ctx.typeToSort(field.type) val lValue = UFieldLValue(sort, expr.asExpr(ctx.addressSort), field.name) val fieldExpr = model.read(lValue) - val obj = resolveExpr(fieldExpr, field.type, model) + val obj = resolveExpr(fieldExpr, field.type) field.name to obj } return TsObject.TsClass(clazz.name, properties) @@ -279,6 +291,17 @@ open class TsTestStateResolver( this.resolveMode = prevValue } } + + fun evaluateInModel(expr: UExpr): UExpr { + return model.eval(expr) + } + + val memory: UReadOnlyMemory + get() = when (resolveMode) { + ResolveMode.MODEL -> model + ResolveMode.CURRENT -> finalStateMemory + ResolveMode.ERROR -> error("Illegal operation for a model") + } } enum class ResolveMode { From 94ee1ab2376dc6d48b16988e11afac204acf658f Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 14 Feb 2025 12:12:16 +0300 Subject: [PATCH 03/12] Fix tests --- .../src/test/kotlin/org/usvm/samples/Null.kt | 2 +- .../kotlin/org/usvm/util/TSTestResolver.kt | 26 +++++++++++++------ 2 files changed, 19 insertions(+), 9 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt index dc5390b4f..9fbae2a2e 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt @@ -16,7 +16,7 @@ class Null : TsMethodTestRunner() { EtsScene(listOf(file)) } - @RepeatedTest(1) + @RepeatedTest(20) fun testIsNull() { val method = getMethod("Null", "isNull") discoverProperties( diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt index 77dd20be5..2bea69f92 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt @@ -55,9 +55,6 @@ class TsTestResolver { val beforeMemoryScope = MemoryScope(this, model, memory, method) val afterMemoryScope = MemoryScope(this, model, memory, method) - val before = beforeMemoryScope.withMode(ResolveMode.MODEL) { (this as MemoryScope).resolveState() } - val after = afterMemoryScope.withMode(ResolveMode.CURRENT) { (this as MemoryScope).resolveState() } - val result = when (val res = state.methodResult) { is TsMethodResult.NoCall -> error("No result found") is TsMethodResult.Success -> { @@ -69,14 +66,20 @@ class TsTestResolver { is TsMethodResult.TsException -> resolveException(res, afterMemoryScope) } + val before = beforeMemoryScope.withMode(ResolveMode.MODEL) { (this as MemoryScope).resolveState() } + val after = afterMemoryScope.withMode(ResolveMode.CURRENT) { (this as MemoryScope).resolveState() } + return TsTest(method, before, after, result, trace = emptyList()) } + + @Suppress("unused") private fun resolveException( res: TsMethodResult.TsException, afterMemoryScope: MemoryScope, ): TsObject.TsException { - TODO() + // TODO support exceptions + return TsObject.TsException } @@ -160,20 +163,27 @@ open class TsTestStateResolver( return when { model.eval(type.boolTypeExpr).isTrue -> { val lValue = ctx.getIntermediateBoolLValue(expr.address) - val value = memory.read(lValue) + // Note that everything about details of fake object we need to read from final state of the memory + // since they are allocated objects + val value = finalStateMemory.read(lValue) resolveExpr(model.eval(value), EtsBooleanType) } model.eval(type.fpTypeExpr).isTrue -> { val lValue = ctx.getIntermediateFpLValue(expr.address) - val value = memory.read(lValue) + // Note that everything about details of fake object we need to read from final state of the memory + // since they are allocated objects + val value = finalStateMemory.read(lValue) resolveExpr(model.eval(value), EtsNumberType) } model.eval(type.refTypeExpr).isTrue -> { val lValue = ctx.getIntermediateRefLValue(expr.address) - val value = memory.read(lValue) + // Note that everything about details of fake object we need to read from final state of the memory + // since they are allocated objects + val value = finalStateMemory.read(lValue) val ref = model.eval(value) + // TODO mistake with signature, use TypeStream instead resolveExpr(ref, EtsClassType(ctx.scene.projectAndSdkClasses.first().signature)) } @@ -273,7 +283,7 @@ open class TsTestStateResolver( val properties = clazz.fields.associate { field -> val sort = ctx.typeToSort(field.type) val lValue = UFieldLValue(sort, expr.asExpr(ctx.addressSort), field.name) - val fieldExpr = model.read(lValue) + val fieldExpr = memory.read(lValue) val obj = resolveExpr(fieldExpr, field.type) field.name to obj } From 361ecc4b0f16e8ba85a59c872109c1f0fc4b9e01 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 14 Feb 2025 12:14:20 +0300 Subject: [PATCH 04/12] Remove redundant changes --- .../org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt index 872e4d64d..7eb970e6f 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt @@ -45,7 +45,7 @@ import kotlin.time.Duration.Companion.seconds private val logger = KotlinLogging.logger {} class EtsProjectAnalysisTest { - private var TsLinesSuccess = 0L + private var tsLinesSuccess = 0L private var TsLinesFailed = 0L private var analysisTime: Duration = Duration.ZERO private var totalPathEdges = 0 @@ -93,8 +93,8 @@ class EtsProjectAnalysisTest { private fun makeReport() { logger.info { "Analysis Report On $PROJECT_PATH" } logger.info { "====================" } - logger.info { "Total files processed: ${TsLinesSuccess + TsLinesFailed}" } - logger.info { "Successfully processed lines: $TsLinesSuccess" } + logger.info { "Total files processed: ${tsLinesSuccess + TsLinesFailed}" } + logger.info { "Successfully processed lines: $tsLinesSuccess" } logger.info { "Failed lines: $TsLinesFailed" } logger.info { "Total analysis time: $analysisTime" } logger.info { "Total path edges: $totalPathEdges" } @@ -130,7 +130,7 @@ class EtsProjectAnalysisTest { runAnalysis(project) val endTime = System.currentTimeMillis() analysisTime += (endTime - startTime).milliseconds - TsLinesSuccess += fileLines + tsLinesSuccess += fileLines } catch (e: Exception) { logger.warn { "Failed to process '$filename': $e" } logger.warn { e.stackTraceToString() } From d657361cab36c81361494c1f69975232f1159ff6 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 14 Feb 2025 12:15:48 +0300 Subject: [PATCH 05/12] Style fixes --- usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt | 2 +- .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 4 +--- usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt | 2 +- 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt index 731dc69fe..33abe9e43 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt @@ -16,7 +16,7 @@ data class TsTest( data class TsParametersState( val thisInstance: TsObject?, val parameters: List, - val globals: Map> + val globals: Map>, ) data class GlobalFieldValue(val field: EtsField, val value: TsObject) // TODO is it right????? 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 35a07413d..e0b5f9b22 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 @@ -4,7 +4,6 @@ import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.base.EtsAssignStmt import org.jacodb.ets.base.EtsCallStmt -import org.jacodb.ets.base.EtsClassType import org.jacodb.ets.base.EtsGotoStmt import org.jacodb.ets.base.EtsIfStmt import org.jacodb.ets.base.EtsLocal @@ -22,7 +21,6 @@ import org.jacodb.ets.model.EtsMethod import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UInterpreter -import org.usvm.api.evalTypeEquals import org.usvm.api.targets.TsTarget import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.forkblacklists.UForkBlackList @@ -208,7 +206,7 @@ class TsInterpreter( val thisInstanceRef = URegisterStackLValue(ctx.addressSort, method.parameters.count()) // TODO check for statics val thisRef = state.memory.read(thisInstanceRef).asExpr(ctx.addressSort) - state.pathConstraints += with (ctx) { + state.pathConstraints += with(ctx) { mkNot( mkOr( ctx.mkHeapRefEq(thisRef, ctx.mkTsNullValue()), diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt index 2bea69f92..9cb20f19a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt @@ -104,7 +104,7 @@ open class TsTestStateResolver( val ctx: TsContext, private val model: UModelBase, private val finalStateMemory: UReadOnlyMemory, - val method: EtsMethod + val method: EtsMethod, ) { fun resolveLValue(lValue: ULValue<*, *>, type: EtsType): TsObject { val expr = memory.read(lValue) From fcaa059239f2d16227f9dcca1138636d51294dd2 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 14 Feb 2025 12:16:55 +0300 Subject: [PATCH 06/12] Rename variable --- .../org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt index 7eb970e6f..194229d18 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt @@ -46,7 +46,7 @@ private val logger = KotlinLogging.logger {} class EtsProjectAnalysisTest { private var tsLinesSuccess = 0L - private var TsLinesFailed = 0L + private var tsLinesFailed = 0L private var analysisTime: Duration = Duration.ZERO private var totalPathEdges = 0 private var totalSinks: MutableList> = mutableListOf() @@ -93,9 +93,9 @@ class EtsProjectAnalysisTest { private fun makeReport() { logger.info { "Analysis Report On $PROJECT_PATH" } logger.info { "====================" } - logger.info { "Total files processed: ${tsLinesSuccess + TsLinesFailed}" } + logger.info { "Total files processed: ${tsLinesSuccess + tsLinesFailed}" } logger.info { "Successfully processed lines: $tsLinesSuccess" } - logger.info { "Failed lines: $TsLinesFailed" } + logger.info { "Failed lines: $tsLinesFailed" } logger.info { "Total analysis time: $analysisTime" } logger.info { "Total path edges: $totalPathEdges" } logger.info { "Found sinks: ${totalSinks.size}" } @@ -134,7 +134,7 @@ class EtsProjectAnalysisTest { } catch (e: Exception) { logger.warn { "Failed to process '$filename': $e" } logger.warn { e.stackTraceToString() } - TsLinesFailed += fileLines + tsLinesFailed += fileLines } } From 44cf9557dcf4685cc17bc31dc03799c325a8df3b Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 14 Feb 2025 13:07:54 +0300 Subject: [PATCH 07/12] Rename TS to Ts, fix braces in when --- ...thodTestRunner.kt => TsMethodTestRunner.kt} | 2 ++ .../{TSTestResolver.kt => TsTestResolver.kt} | 18 +++++++++--------- 2 files changed, 11 insertions(+), 9 deletions(-) rename usvm-ts/src/test/kotlin/org/usvm/util/{TSMethodTestRunner.kt => TsMethodTestRunner.kt} (99%) rename usvm-ts/src/test/kotlin/org/usvm/util/{TSTestResolver.kt => TsTestResolver.kt} (97%) diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt similarity index 99% rename from usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt rename to usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt index 767632fe9..72cbaff3a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt @@ -173,6 +173,7 @@ abstract class TsMethodTestRunner : TestRunner EtsStringType TsObject.TsNumber::class -> EtsNumberType TsObject.TsNumber.Double::class -> EtsNumberType @@ -188,6 +189,7 @@ abstract class TsMethodTestRunner : TestRunner error("Unsupported type: $klass") } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt similarity index 97% rename from usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt rename to usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 9cb20f19a..9f963767f 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -1,7 +1,6 @@ package org.usvm.util import io.ksmt.utils.asExpr -import io.ksmt.utils.cast import org.jacodb.ets.base.CONSTRUCTOR_NAME import org.jacodb.ets.base.EtsBooleanType import org.jacodb.ets.base.EtsClassType @@ -21,18 +20,16 @@ import org.jacodb.ets.model.EtsClassImpl import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodImpl -import org.jacodb.ets.model.EtsMethodParameter import org.jacodb.ets.model.EtsMethodSignature import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.USort import org.usvm.api.GlobalFieldValue import org.usvm.api.TsObject -import org.usvm.api.TsTest import org.usvm.api.TsParametersState +import org.usvm.api.TsTest import org.usvm.collection.field.UFieldLValue import org.usvm.isTrue -import org.usvm.machine.types.FakeType import org.usvm.machine.TsContext import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.expr.extractBool @@ -40,6 +37,7 @@ import org.usvm.machine.expr.extractDouble import org.usvm.machine.expr.extractInt import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState +import org.usvm.machine.types.FakeType import org.usvm.memory.ULValue import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.URegisterStackLValue @@ -56,14 +54,19 @@ class TsTestResolver { val afterMemoryScope = MemoryScope(this, model, memory, method) val result = when (val res = state.methodResult) { - is TsMethodResult.NoCall -> error("No result found") + is TsMethodResult.NoCall -> { + error("No result found") + } + is TsMethodResult.Success -> { afterMemoryScope.withMode(ResolveMode.CURRENT) { resolveExpr(res.value, method.returnType) } } - is TsMethodResult.TsException -> resolveException(res, afterMemoryScope) + is TsMethodResult.TsException -> { + resolveException(res, afterMemoryScope) + } } val before = beforeMemoryScope.withMode(ResolveMode.MODEL) { (this as MemoryScope).resolveState() } @@ -72,7 +75,6 @@ class TsTestResolver { return TsTest(method, before, after, result, trace = emptyList()) } - @Suppress("unused") private fun resolveException( res: TsMethodResult.TsException, @@ -82,7 +84,6 @@ class TsTestResolver { return TsObject.TsException } - private class MemoryScope( ctx: TsContext, model: UModelBase, @@ -191,7 +192,6 @@ open class TsTestStateResolver( } } - private fun resolveUnknown( expr: UConcreteHeapRef, ): TsObject { From d91e84a0a6cbeb70b53d9bbd57a319760e80e554 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 14 Feb 2025 13:18:32 +0300 Subject: [PATCH 08/12] Check via isFakeObject --- .../kotlin/org/usvm/util/TsTestResolver.kt | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 9f963767f..83ab872c3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -138,20 +138,20 @@ open class TsTestStateResolver( return resolveLValue(ref, type) } - fun resolveParameters(): List = method.parameters.mapIndexed { idx, param -> - val sort = ctx.typeToSort(param.type) - - if (sort is TsUnresolvedSort) { - // this means that a fake object was created, and we need to read it from the current memory - val address = finalStateMemory.read(URegisterStackLValue(ctx.addressSort, idx)).asExpr(ctx.addressSort) - - check(address is UConcreteHeapRef) + fun resolveParameters(): List = with(ctx) { + method.parameters.mapIndexed { idx, param -> + val sort = typeToSort(param.type) + + if (sort is TsUnresolvedSort) { + // this means that a fake object was created, and we need to read it from the current memory + val address = finalStateMemory.read(URegisterStackLValue(addressSort, idx)).asExpr(addressSort) + check(address.isFakeObject()) + return@mapIndexed resolveFakeObject(address) + } - return@mapIndexed resolveFakeObject(address) + val ref = URegisterStackLValue(sort, idx) + resolveLValue(ref, param.type) } - - val ref = URegisterStackLValue(sort, idx) - resolveLValue(ref, param.type) } fun resolveGlobals(): Map> { From 12852c76ebbdd8c25a5a0ddb9a4836525e176392 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 14 Feb 2025 13:29:37 +0300 Subject: [PATCH 09/12] Add newline --- usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt index 9fbae2a2e..f035e3db6 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt @@ -25,4 +25,4 @@ class Null : TsMethodTestRunner() { { a, r -> a !is TsObject.TsNull && r.number == 2.0 }, ) } -} \ No newline at end of file +} From d2ada6c075c75868805556e3b96a6e7493214c7f Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 14 Feb 2025 13:30:39 +0300 Subject: [PATCH 10/12] Remove unnecessary branch, use method.enclosingClass --- .../kotlin/org/usvm/util/TsTestResolver.kt | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 83ab872c3..7de8e4dab 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -109,32 +109,23 @@ open class TsTestStateResolver( ) { fun resolveLValue(lValue: ULValue<*, *>, type: EtsType): TsObject { val expr = memory.read(lValue) - return resolveExpr(expr, type) } fun resolveExpr( expr: UExpr, type: EtsType, - ): TsObject = when { - type is EtsUnknownType && expr is UConcreteHeapRef -> resolveUnknown(expr) - type is EtsPrimitiveType -> resolvePrimitive(expr, type) - type is EtsClassType -> resolveClass(expr, type) - type is EtsRefType -> TODO() + ): TsObject = when (type) { + is EtsPrimitiveType -> resolvePrimitive(expr, type) + is EtsClassType -> resolveClass(expr, type) + is EtsRefType -> TODO() else -> TODO() } fun resolveThisInstance(): TsObject? { val parametersCount = method.parameters.size val ref = URegisterStackLValue(ctx.addressSort, idx = parametersCount) // TODO check for statics - val type = EtsClassType( - EtsClassSignature( - name = method.enclosingClass.name, - file = method.enclosingClass.file, - namespace = method.enclosingClass.namespace - ) - ) - + val type = EtsClassType(method.enclosingClass) return resolveLValue(ref, type) } From e426c6f15a35c673eca39b3b6111931ddece4772 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 14 Feb 2025 13:45:22 +0300 Subject: [PATCH 11/12] Remove resolveUnknown --- usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt | 9 --------- 1 file changed, 9 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 7de8e4dab..c02b5c7e4 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -183,15 +183,6 @@ open class TsTestStateResolver( } } - private fun resolveUnknown( - expr: UConcreteHeapRef, - ): TsObject { - val typeStream = memory.types.getTypeStream(expr) - return (typeStream.first() as? EtsType)?.let { type -> - resolveExpr(expr, type) - } ?: TsObject.TsObject(expr.address) - } - private fun resolvePrimitive( expr: UExpr, type: EtsPrimitiveType, From ca7b751b3fa588cd04fcb7173d7df051a9a3bc1d Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 14 Feb 2025 13:49:45 +0300 Subject: [PATCH 12/12] Format --- usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt | 3 --- 1 file changed, 3 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index c02b5c7e4..06c6b1cf2 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -13,11 +13,9 @@ import org.jacodb.ets.base.EtsRefType import org.jacodb.ets.base.EtsStringType import org.jacodb.ets.base.EtsType import org.jacodb.ets.base.EtsUndefinedType -import org.jacodb.ets.base.EtsUnknownType import org.jacodb.ets.base.EtsVoidType import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassImpl -import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodImpl import org.jacodb.ets.model.EtsMethodSignature @@ -42,7 +40,6 @@ import org.usvm.memory.ULValue import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.URegisterStackLValue import org.usvm.model.UModelBase -import org.usvm.types.first import org.usvm.types.single class TsTestResolver {