From 4c8f74b46f418897c001fb65a6ee72122b3aaf02 Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Wed, 24 Jul 2024 17:24:25 +0300 Subject: [PATCH 01/22] [WIP] TSTypeSystem --- .../src/main/kotlin/org/usvm/TSComponents.kt | 32 ++++- usvm-ts/src/main/kotlin/org/usvm/TSContext.kt | 3 + .../main/kotlin/org/usvm/TSExprResolver.kt | 136 ++++++++++++++++++ .../src/main/kotlin/org/usvm/TSTypeSystem.kt | 6 +- 4 files changed, 174 insertions(+), 3 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt index 15671ef2c..8961ca4a6 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt @@ -1,5 +1,6 @@ package org.usvm +import io.ksmt.expr.KBitVec32Value import io.ksmt.solver.yices.KYicesSolver import io.ksmt.solver.z3.KZ3Solver import io.ksmt.symfpu.solver.KSymFpuSolver @@ -15,10 +16,10 @@ class TSComponents( private val closeableResources = mutableListOf() override val useSolverForForks: Boolean - get() = TODO("Not yet implemented") + get() = options.useSolverForForks override fun > mkSizeExprProvider(ctx: Context): USizeExprProvider { - TODO("Not yet implemented") + return TSFpSortSizeExprProvider(ctx as TSContext) } override fun mkTypeSystem( @@ -44,3 +45,30 @@ class TSComponents( closeableResources.forEach(AutoCloseable::close) } } + +class TSFpSortSizeExprProvider( + override val ctx: TSContext, +) : USizeExprProvider { + override val sizeSort: TSSizeSort = ctx.sizeSort + + override fun mkSizeExpr(size: Int): UExpr = ctx.mkBv(size, sizeSort) + override fun getIntValue(expr: UExpr): Int? = (expr as? KBitVec32Value)?.numberValue + + override fun mkSizeSubExpr(lhs: UExpr, rhs: UExpr): UExpr = + ctx.mkBvSubExpr(lhs, rhs) + + override fun mkSizeAddExpr(lhs: UExpr, rhs: UExpr): UExpr = + ctx.mkBvAddExpr(lhs, rhs) + + override fun mkSizeGtExpr(lhs: UExpr, rhs: UExpr): UBoolExpr = + ctx.mkBvUnsignedGreaterExpr(lhs, rhs) + + override fun mkSizeGeExpr(lhs: UExpr, rhs: UExpr): UBoolExpr = + ctx.mkBvUnsignedGreaterOrEqualExpr(lhs, rhs) + + override fun mkSizeLtExpr(lhs: UExpr, rhs: UExpr): UBoolExpr = + ctx.mkBvUnsignedLessExpr(lhs, rhs) + + override fun mkSizeLeExpr(lhs: UExpr, rhs: UExpr): UBoolExpr = + ctx.mkBvUnsignedLessOrEqualExpr(lhs, rhs) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt index 8e6660bdb..866e704bb 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt @@ -1,5 +1,8 @@ package org.usvm +import io.ksmt.sort.KFp64Sort + typealias TSSizeSort = UBv32Sort +typealias TSNumberSort = KFp64Sort class TSContext(components: TSComponents) : UContext(components) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt new file mode 100644 index 000000000..4dcd0bef5 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt @@ -0,0 +1,136 @@ +package org.usvm + +import org.jacodb.ets.base.EtsArrayAccess +import org.jacodb.ets.base.EtsArrayLiteral +import org.jacodb.ets.base.EtsBinaryOperation +import org.jacodb.ets.base.EtsBooleanConstant +import org.jacodb.ets.base.EtsCastExpr +import org.jacodb.ets.base.EtsDeleteExpr +import org.jacodb.ets.base.EtsEntity +import org.jacodb.ets.base.EtsInstanceCallExpr +import org.jacodb.ets.base.EtsInstanceFieldRef +import org.jacodb.ets.base.EtsInstanceOfExpr +import org.jacodb.ets.base.EtsLengthExpr +import org.jacodb.ets.base.EtsLocal +import org.jacodb.ets.base.EtsNewArrayExpr +import org.jacodb.ets.base.EtsNewExpr +import org.jacodb.ets.base.EtsNullConstant +import org.jacodb.ets.base.EtsNumberConstant +import org.jacodb.ets.base.EtsObjectLiteral +import org.jacodb.ets.base.EtsParameterRef +import org.jacodb.ets.base.EtsPhiExpr +import org.jacodb.ets.base.EtsRelationOperation +import org.jacodb.ets.base.EtsStaticCallExpr +import org.jacodb.ets.base.EtsStaticFieldRef +import org.jacodb.ets.base.EtsStringConstant +import org.jacodb.ets.base.EtsThis +import org.jacodb.ets.base.EtsTypeOfExpr +import org.jacodb.ets.base.EtsUnaryOperation +import org.jacodb.ets.base.EtsUndefinedConstant + +class TSExprResolver : EtsEntity.Visitor> { + + override fun visit(value: EtsLocal): UExpr { + TODO("Not yet implemented") + } + + override fun visit(value: EtsArrayLiteral): UExpr { + TODO("Not yet implemented") + } + + override fun visit(value: EtsBooleanConstant): UExpr { + TODO("Not yet implemented") + } + + override fun visit(value: EtsNullConstant): UExpr { + TODO("Not yet implemented") + } + + override fun visit(value: EtsNumberConstant): UExpr { + TODO("Not yet implemented") + } + + override fun visit(value: EtsObjectLiteral): UExpr { + TODO("Not yet implemented") + } + + override fun visit(value: EtsStringConstant): UExpr { + TODO("Not yet implemented") + } + + override fun visit(value: EtsUndefinedConstant): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsBinaryOperation): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsCastExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsDeleteExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsInstanceCallExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsInstanceOfExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsLengthExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsNewArrayExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsNewExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsPhiExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsRelationOperation): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsStaticCallExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsTypeOfExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsUnaryOperation): UExpr { + TODO("Not yet implemented") + } + + override fun visit(ref: EtsArrayAccess): UExpr { + TODO("Not yet implemented") + } + + override fun visit(ref: EtsInstanceFieldRef): UExpr { + TODO("Not yet implemented") + } + + override fun visit(ref: EtsParameterRef): UExpr { + TODO("Not yet implemented") + } + + override fun visit(ref: EtsStaticFieldRef): UExpr { + TODO("Not yet implemented") + } + + override fun visit(ref: EtsThis): UExpr { + TODO("Not yet implemented") + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt index aa2ccfc21..46a20adf3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt @@ -1,5 +1,6 @@ package org.usvm +import org.jacodb.ets.base.EtsPrimitiveType import org.jacodb.ets.base.EtsType import org.jacodb.ets.model.EtsFile import org.usvm.types.UTypeStream @@ -10,8 +11,11 @@ class TSTypeSystem( override val typeOperationsTimeout: Duration, val project: EtsFile, ) : UTypeSystem { + override fun isSupertype(supertype: EtsType, type: EtsType): Boolean { - TODO("Not yet implemented") + if (supertype == type) return true + + if (type is EtsPrimitiveType) return false } override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean { From b15d48248f3d361be8215e02af132b5641f73f6f Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Mon, 29 Jul 2024 13:22:26 +0300 Subject: [PATCH 02/22] Enhance TSTypeSystem + jacodb version update --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- .../src/main/kotlin/org/usvm/TSTypeSystem.kt | 127 ++++++++++++++++-- 2 files changed, 115 insertions(+), 14 deletions(-) diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 61810835b..0b9c55d58 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -5,7 +5,7 @@ import org.gradle.plugin.use.PluginDependenciesSpec object Versions { const val detekt = "1.18.1" const val ini4j = "0.5.4" - const val jacodb = "30594f5f7c" + const val jacodb = "c2453bce3d" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "1.9.20" diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt index 46a20adf3..761bcc770 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt @@ -1,10 +1,12 @@ package org.usvm -import org.jacodb.ets.base.EtsPrimitiveType -import org.jacodb.ets.base.EtsType +import kotlinx.collections.immutable.PersistentList +import kotlinx.collections.immutable.persistentListOf +import org.jacodb.ets.base.* +import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFile -import org.usvm.types.UTypeStream -import org.usvm.types.UTypeSystem +import org.usvm.types.* +import org.usvm.types.TypesResult.Companion.toTypesResult import kotlin.time.Duration class TSTypeSystem( @@ -13,28 +15,127 @@ class TSTypeSystem( ) : UTypeSystem { override fun isSupertype(supertype: EtsType, type: EtsType): Boolean { - if (supertype == type) return true - - if (type is EtsPrimitiveType) return false + return when { + supertype == type -> return true + type is EtsPrimitiveType -> return false + type is EtsClassType -> supertype.checkSubtype(type.classSignature) + else -> false + } } override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean { - TODO("Not yet implemented") + when (type) { + is EtsPrimitiveType -> return types.isEmpty() + is EtsClassType -> return types.all { isSupertype(it, type) } + is EtsArrayType -> { + val elementTypes = types.map { + when { + it is EtsArrayType -> it.elementType + else -> return false + } + } + return hasCommonSubtype(type.elementType, elementTypes) + } + else -> TODO() + } } override fun isFinal(type: EtsType): Boolean { - TODO("Not yet implemented") + // No final modifier in jacodb IR + return false } override fun isInstantiable(type: EtsType): Boolean { - TODO("Not yet implemented") + return true } - override fun findSubtypes(type: EtsType): Sequence { - TODO("Not yet implemented") + override fun findSubtypes(type: EtsType): Sequence = when (type) { + is EtsPrimitiveType -> emptySequence() + is EtsArrayType -> findSubtypes(type.elementType).map { EtsArrayType(it, type.dimensions) } + is EtsClassType -> TODO() + else -> TODO() } override fun topTypeStream(): UTypeStream { - TODO("Not yet implemented") + return TSTopTypeStream(this) + } + + private fun EtsType.checkSubtype(typeClassSignature: EtsClassSignature?): Boolean { + if (typeClassSignature == null) return false + + return this.typeName == typeClassSignature.name || + this.checkSubtype(project.getClassBySignature(typeClassSignature)?.superClass) + } +} + +class TSTopTypeStream( + private val typeSystem: TSTypeSystem, + val primitiveTypes: PersistentList = persistentListOf( + EtsNumberType, + EtsBooleanType, + EtsStringType + ), +) : UTypeStream { + override fun filterBySupertype(type: EtsType): UTypeStream { + if (type is EtsPrimitiveType) { + if (type !in primitiveTypes) { + return emptyTypeStream() + } + + return USingleTypeStream(typeSystem, type) + } + + return emptyTypeStream() + } + + override fun filterBySubtype(type: EtsType): UTypeStream { + if (type is EtsPrimitiveType) { + if (type !in primitiveTypes) { + return emptyTypeStream() + } + + return USingleTypeStream(typeSystem, type) + } + + return emptyTypeStream() + } + + override fun filterByNotSupertype(type: EtsType): UTypeStream { + if (type is EtsPrimitiveType && type in primitiveTypes) { + val updatedPrimitiveTypes = primitiveTypes.remove(type) + + if (updatedPrimitiveTypes.isEmpty()) { + return emptyTypeStream() + } + + return TSTopTypeStream(typeSystem, updatedPrimitiveTypes) + } + + return TSTopTypeStream(typeSystem, primitiveTypes) + } + + override fun filterByNotSubtype(type: EtsType): UTypeStream { + if (type is EtsPrimitiveType && type in primitiveTypes) { + val updatedPrimitiveTypes = primitiveTypes.remove(type) + + if (updatedPrimitiveTypes.isEmpty()) { + return emptyTypeStream() + } + + return TSTopTypeStream(typeSystem, updatedPrimitiveTypes) + } + + return TSTopTypeStream(typeSystem, primitiveTypes) + } + + override fun take(n: Int): TypesResult { + return primitiveTypes.take(n).toTypesResult(wasTimeoutExpired = false) } + + override val isEmpty: Boolean + get() = primitiveTypes.isEmpty() + + override val commonSuperType: EtsType + get() = EtsAnyType + } From f89c0e1a0780028ee344020b685d5a204b6d527f Mon Sep 17 00:00:00 2001 From: Sergey Loktev <71882967+zishkaz@users.noreply.github.com> Date: Thu, 25 Jul 2024 06:47:07 +0300 Subject: [PATCH 03/22] TSTypeSystem + TSInterpreter skeleton + TSSimpleValueResolver --- usvm-ts/src/main/kotlin/org/usvm/TSContext.kt | 32 +++- .../main/kotlin/org/usvm/TSExprResolver.kt | 141 +++++++++++++++++- .../src/main/kotlin/org/usvm/TSExpressions.kt | 51 +++++++ .../src/main/kotlin/org/usvm/TSInterpreter.kt | 103 ++++++++++++- usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt | 2 +- .../src/main/kotlin/org/usvm/TSTypeSystem.kt | 17 ++- usvm-ts/src/main/kotlin/org/usvm/Util.kt | 8 - .../kotlin/org/usvm/state/TSStateUtils.kt | 26 ++++ 8 files changed, 356 insertions(+), 24 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt delete mode 100644 usvm-ts/src/main/kotlin/org/usvm/Util.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt index 866e704bb..97902dbf8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt @@ -1,8 +1,34 @@ package org.usvm -import io.ksmt.sort.KFp64Sort +import org.jacodb.ets.base.EtsAnyType +import org.jacodb.ets.base.EtsBooleanType +import org.jacodb.ets.base.EtsNumberType +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.EtsVoidType typealias TSSizeSort = UBv32Sort -typealias TSNumberSort = KFp64Sort -class TSContext(components: TSComponents) : UContext(components) +class TSContext(components: TSComponents) : UContext(components) { + + val voidSort: TSVoidSort by lazy { TSVoidSort(this) } + val undefinedSort: TSUndefinedSort by lazy { TSUndefinedSort(this) } + val stringSort: TSStringSort by lazy { TSStringSort(this) } + + private val undefinedValue by lazy { TSUndefinedValue(this) } + + fun typeToSort(type: EtsType): USort = when (type) { + is EtsAnyType -> addressSort + is EtsVoidType -> voidSort + is EtsUndefinedType -> undefinedSort + is EtsRefType -> addressSort + is EtsBooleanType -> boolSort + is EtsNumberType -> fp64Sort + is EtsStringType -> stringSort + else -> error("Unknown type: $type") + } + + fun mkUndefinedValue(): TSUndefinedValue = undefinedValue +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt index 4dcd0bef5..611cb9de3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt @@ -18,17 +18,34 @@ import org.jacodb.ets.base.EtsNullConstant import org.jacodb.ets.base.EtsNumberConstant import org.jacodb.ets.base.EtsObjectLiteral import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsPhiExpr import org.jacodb.ets.base.EtsRelationOperation import org.jacodb.ets.base.EtsStaticCallExpr import org.jacodb.ets.base.EtsStaticFieldRef import org.jacodb.ets.base.EtsStringConstant import org.jacodb.ets.base.EtsThis +import org.jacodb.ets.base.EtsType import org.jacodb.ets.base.EtsTypeOfExpr import org.jacodb.ets.base.EtsUnaryOperation import org.jacodb.ets.base.EtsUndefinedConstant +import org.jacodb.ets.base.EtsValue +import org.jacodb.ets.model.EtsMethod +import org.usvm.memory.URegisterStackLValue -class TSExprResolver : EtsEntity.Visitor> { +class TSExprResolver( + private val ctx: TSContext, + private val scope: TSStepScope, + private val localToIdx: (EtsMethod, EtsValue) -> Int, +) : EtsEntity.Visitor> { + + val simpleValueResolver: TSSimpleValueResolver = TSSimpleValueResolver( + ctx, + scope, + localToIdx + ) + + fun resolveTSExpr(expr: EtsEntity, type: EtsType = expr.type): UExpr? { + TODO() + } override fun visit(value: EtsLocal): UExpr { TODO("Not yet implemented") @@ -94,10 +111,6 @@ class TSExprResolver : EtsEntity.Visitor> { TODO("Not yet implemented") } - override fun visit(expr: EtsPhiExpr): UExpr { - TODO("Not yet implemented") - } - override fun visit(expr: EtsRelationOperation): UExpr { TODO("Not yet implemented") } @@ -134,3 +147,119 @@ class TSExprResolver : EtsEntity.Visitor> { TODO("Not yet implemented") } } + +class TSSimpleValueResolver( + private val ctx: TSContext, + private val scope: TSStepScope, + private val localToIdx: (EtsMethod, EtsValue) -> Int, +) : EtsEntity.Visitor> { + override fun visit(value: EtsLocal): UExpr = with(ctx) { + val lValue = resolveLocal(value) + return scope.calcOnState { memory.read(lValue) } + } + + override fun visit(value: EtsArrayLiteral): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(value: EtsBooleanConstant): UExpr = with(ctx) { + mkBool(value.value) + } + + override fun visit(value: EtsNullConstant): UExpr = with(ctx) { + nullRef + } + + override fun visit(value: EtsNumberConstant): UExpr = with(ctx) { + mkFp64(value.value) + } + + override fun visit(value: EtsObjectLiteral): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(value: EtsStringConstant): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(value: EtsUndefinedConstant): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsBinaryOperation): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsCastExpr): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsDeleteExpr): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsInstanceCallExpr): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsInstanceOfExpr): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsLengthExpr): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsNewArrayExpr): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsNewExpr): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsRelationOperation): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsStaticCallExpr): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsTypeOfExpr): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsUnaryOperation): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(ref: EtsArrayAccess): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(ref: EtsInstanceFieldRef): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(ref: EtsParameterRef): UExpr = with(ctx) { + val lValue = resolveLocal(ref) + return scope.calcOnState { memory.read(lValue) } + } + + override fun visit(ref: EtsStaticFieldRef): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(ref: EtsThis): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + fun resolveLocal(local: EtsValue): URegisterStackLValue<*> { + val method = requireNotNull(scope.calcOnState { lastEnteredMethod }) + val localIdx = localToIdx(method, local) + val sort = ctx.typeToSort(local.type) + return URegisterStackLValue(sort, localIdx) + } + +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt new file mode 100644 index 000000000..452060770 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt @@ -0,0 +1,51 @@ +package org.usvm + +import io.ksmt.KAst +import io.ksmt.cache.hash +import io.ksmt.cache.structurallyEqual +import io.ksmt.expr.KExpr +import io.ksmt.expr.printer.ExpressionPrinter +import io.ksmt.expr.transformer.KTransformerBase +import io.ksmt.sort.KSortVisitor + +val KAst.tctx get() = ctx as TSContext + +class TSVoidSort(ctx: TSContext) : USort(ctx) { + override fun print(builder: StringBuilder) { + builder.append("void sort") + } + + override fun accept(visitor: KSortVisitor): T = error("Should not be called") +} + +class TSUndefinedSort(ctx: TSContext) : USort(ctx) { + override fun print(builder: StringBuilder) { + builder.append("undefined sort") + } + + override fun accept(visitor: KSortVisitor): T = error("Should not be called") +} + +class TSStringSort(ctx: TSContext) : USort(ctx) { + override fun print(builder: StringBuilder) { + builder.append("string sort") + } + + override fun accept(visitor: KSortVisitor): T = TODO("Not yet implemented") +} + +class TSUndefinedValue(ctx: TSContext) : UExpr(ctx) { + override val sort: TSUndefinedSort + get() = tctx.undefinedSort + + override fun accept(transformer: KTransformerBase): TSUndefinedValue = this + + override fun internEquals(other: Any): Boolean = structurallyEqual(other) + + override fun internHashCode(): Int = hash() + + override fun print(printer: ExpressionPrinter) { + printer.append("undefined") + } + +} \ No newline at end of file diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt index d514bbb2e..e673a4339 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt @@ -1,8 +1,20 @@ package org.usvm import io.ksmt.utils.asExpr +import org.jacodb.ets.base.EtsAssignStmt +import org.jacodb.ets.base.EtsCallStmt +import org.jacodb.ets.base.EtsGotoStmt +import org.jacodb.ets.base.EtsIfStmt +import org.jacodb.ets.base.EtsLocal +import org.jacodb.ets.base.EtsNopStmt +import org.jacodb.ets.base.EtsParameterRef +import org.jacodb.ets.base.EtsReturnStmt import org.jacodb.ets.base.EtsStmt +import org.jacodb.ets.base.EtsSwitchStmt +import org.jacodb.ets.base.EtsThis +import org.jacodb.ets.base.EtsThrowStmt import org.jacodb.ets.base.EtsType +import org.jacodb.ets.base.EtsValue import org.jacodb.ets.model.EtsMethod import org.usvm.forkblacklists.UForkBlackList import org.usvm.memory.URegisterStackLValue @@ -10,8 +22,14 @@ import org.usvm.solver.USatResult import org.usvm.state.TSMethodResult import org.usvm.state.TSState import org.usvm.state.lastStmt +import org.usvm.state.localIdx +import org.usvm.state.newStmt +import org.usvm.state.parametersWithThisCount +import org.usvm.state.returnValue import org.usvm.targets.UTargetsSet +typealias TSStepScope = StepScope + class TSInterpreter( private val ctx: TSContext, private val applicationGraph: TSApplicationGraph, @@ -40,14 +58,93 @@ class TSInterpreter( return scope.stepResult() } - // TODO: interpreter - stmt.nextStmt?.let { nextStmt -> - scope.doWithState { newStmt(nextStmt) } + when (stmt) { + is EtsIfStmt -> visitIfStmt(scope, stmt) + is EtsReturnStmt -> visitReturnStmt(scope, stmt) + is EtsAssignStmt -> visitAssignStmt(scope, stmt) + is EtsCallStmt -> visitCallStmt(scope, stmt) + is EtsThrowStmt -> visitThrowStmt(scope, stmt) + is EtsGotoStmt -> visitGotoStmt(scope, stmt) + is EtsNopStmt -> visitNopStmt(scope, stmt) + is EtsSwitchStmt -> visitSwitchStmt(scope, stmt) + else -> error("Unknown stmt: $stmt") } +// stmt.nextStmt?.let { nextStmt -> +// scope.doWithState { newStmt(nextStmt) } +// } + return scope.stepResult() } + private fun visitIfStmt(scope: TSStepScope, stmt: EtsIfStmt) { + TODO() + } + + private fun visitReturnStmt(scope: TSStepScope, stmt: EtsReturnStmt) { + val exprResolver = exprResolverWithScope(scope) + + val method = requireNotNull(scope.calcOnState { callStack.lastMethod() }) + val returnType = method.returnType + + val valueToReturn = stmt.returnValue + ?.let { exprResolver.resolveTSExpr(it, returnType) ?: return } + ?: ctx.mkUndefinedValue() + + scope.doWithState { + returnValue(valueToReturn) + } + } + + private fun visitAssignStmt(scope: TSStepScope, stmt: EtsAssignStmt) { + TODO() + } + + private fun visitCallStmt(scope: TSStepScope, stmt: EtsCallStmt) { + TODO() + } + + private fun visitThrowStmt(scope: TSStepScope, stmt: EtsThrowStmt) { + TODO() + } + + private fun visitGotoStmt(scope: TSStepScope, stmt: EtsGotoStmt) { + TODO() + } + + private fun visitNopStmt(scope: TSStepScope, stmt: EtsNopStmt) { + TODO() + } + + private fun visitSwitchStmt(scope: TSStepScope, stmt: EtsSwitchStmt) { + TODO() + } + + private fun exprResolverWithScope(scope: TSStepScope) = + TSExprResolver( + ctx, + scope, + ::mapLocalToIdxMapper, + ) + + // (method, localIdx) -> idx + private val localVarToIdx = mutableMapOf>() + + // TODO: now we need to explicitly evaluate indices of registers, because we don't have specific ULValues + private fun mapLocalToIdxMapper(method: EtsMethod, local: EtsValue) = + when (local) { + is EtsLocal -> localVarToIdx + .getOrPut(method) { mutableMapOf() } + .run { + getOrPut(local.name) { method.parametersWithThisCount + size } + } + + is EtsThis -> 0 + is EtsParameterRef -> method.localIdx(local.index) + else -> error("Unexpected local: $local") + } + + fun getInitialState(method: EtsMethod, targets: List): TSState { val state = TSState(ctx, method, targets = UTargetsSet.from(targets)) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt index 4e5635648..c6251e0cb 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt @@ -1,5 +1,6 @@ package org.usvm +import kotlin.time.Duration.Companion.seconds import org.jacodb.ets.base.EtsStmt import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsMethod @@ -17,7 +18,6 @@ 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, diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt index 761bcc770..ef097d845 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt @@ -1,13 +1,24 @@ package org.usvm +import kotlin.time.Duration import kotlinx.collections.immutable.PersistentList import kotlinx.collections.immutable.persistentListOf -import org.jacodb.ets.base.* +import org.jacodb.ets.base.EtsAnyType +import org.jacodb.ets.base.EtsArrayType +import org.jacodb.ets.base.EtsBooleanType +import org.jacodb.ets.base.EtsClassType +import org.jacodb.ets.base.EtsNumberType +import org.jacodb.ets.base.EtsPrimitiveType +import org.jacodb.ets.base.EtsStringType +import org.jacodb.ets.base.EtsType import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFile -import org.usvm.types.* +import org.usvm.types.TypesResult import org.usvm.types.TypesResult.Companion.toTypesResult -import kotlin.time.Duration +import org.usvm.types.USingleTypeStream +import org.usvm.types.UTypeStream +import org.usvm.types.UTypeSystem +import org.usvm.types.emptyTypeStream class TSTypeSystem( override val typeOperationsTimeout: Duration, diff --git a/usvm-ts/src/main/kotlin/org/usvm/Util.kt b/usvm-ts/src/main/kotlin/org/usvm/Util.kt deleted file mode 100644 index 47bf55378..000000000 --- a/usvm-ts/src/main/kotlin/org/usvm/Util.kt +++ /dev/null @@ -1,8 +0,0 @@ -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/TSStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt index 1d65cdb8c..16eb596a5 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt @@ -1,3 +1,29 @@ package org.usvm.state +import org.jacodb.ets.base.EtsStmt +import org.jacodb.ets.model.EtsMethod +import org.usvm.UExpr +import org.usvm.USort + val TSState.lastStmt get() = pathNode.statement +fun TSState.newStmt(stmt: EtsStmt) { + pathNode += stmt +} + +fun TSState.returnValue(valueToReturn: UExpr) { + val returnFromMethod = callStack.lastMethod() + val returnSite = callStack.pop() + if (callStack.isNotEmpty()) { + memory.stack.pop() + } + + methodResult = TSMethodResult.Success(returnFromMethod, valueToReturn) + + if (returnSite != null) { + newStmt(returnSite) + } +} + +fun EtsMethod.localIdx(idx: Int) = if (TODO("isStatic")) idx else idx + 1 + +inline val EtsMethod.parametersWithThisCount get() = localIdx(parameters.size) \ No newline at end of file From 73b13bd63686484b990cfa152dfe3d04ab3497b9 Mon Sep 17 00:00:00 2001 From: Sergey Loktev <71882967+zishkaz@users.noreply.github.com> Date: Mon, 29 Jul 2024 04:20:25 +0300 Subject: [PATCH 04/22] Version hotfix --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 0b9c55d58..0376f0a0e 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -5,7 +5,7 @@ import org.gradle.plugin.use.PluginDependenciesSpec object Versions { const val detekt = "1.18.1" const val ini4j = "0.5.4" - const val jacodb = "c2453bce3d" + const val jacodb = "4b15fc6452" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "1.9.20" diff --git a/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt index 16eb596a5..87bfe1c87 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt @@ -24,6 +24,6 @@ fun TSState.returnValue(valueToReturn: UExpr) { } } -fun EtsMethod.localIdx(idx: Int) = if (TODO("isStatic")) idx else idx + 1 +fun EtsMethod.localIdx(idx: Int) = if (isStatic) idx else idx + 1 inline val EtsMethod.parametersWithThisCount get() = localIdx(parameters.size) \ No newline at end of file From b8c9f43c81339d73aeb04881d9aa6e1841071498 Mon Sep 17 00:00:00 2001 From: Sergey Loktev <71882967+zishkaz@users.noreply.github.com> Date: Mon, 29 Jul 2024 04:37:21 +0300 Subject: [PATCH 05/22] Minor polishing --- usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt | 2 ++ usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt | 3 +-- usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt | 4 ++-- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt index 611cb9de3..051a9d57b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt @@ -31,6 +31,7 @@ import org.jacodb.ets.base.EtsValue import org.jacodb.ets.model.EtsMethod import org.usvm.memory.URegisterStackLValue +@Suppress("UNUSED_PARAMETER") class TSExprResolver( private val ctx: TSContext, private val scope: TSStepScope, @@ -153,6 +154,7 @@ class TSSimpleValueResolver( private val scope: TSStepScope, private val localToIdx: (EtsMethod, EtsValue) -> Int, ) : EtsEntity.Visitor> { + override fun visit(value: EtsLocal): UExpr = with(ctx) { val lValue = resolveLocal(value) return scope.calcOnState { memory.read(lValue) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt index 452060770..887bfc85d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt @@ -3,7 +3,6 @@ package org.usvm import io.ksmt.KAst import io.ksmt.cache.hash import io.ksmt.cache.structurallyEqual -import io.ksmt.expr.KExpr import io.ksmt.expr.printer.ExpressionPrinter import io.ksmt.expr.transformer.KTransformerBase import io.ksmt.sort.KSortVisitor @@ -31,7 +30,7 @@ class TSStringSort(ctx: TSContext) : USort(ctx) { builder.append("string sort") } - override fun accept(visitor: KSortVisitor): T = TODO("Not yet implemented") + override fun accept(visitor: KSortVisitor): T = error("Should not be called") } class TSUndefinedValue(ctx: TSContext) : UExpr(ctx) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt index e673a4339..052e7eeaa 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt @@ -30,6 +30,7 @@ import org.usvm.targets.UTargetsSet typealias TSStepScope = StepScope +@Suppress("UNUSED_PARAMETER") class TSInterpreter( private val ctx: TSContext, private val applicationGraph: TSApplicationGraph, @@ -127,10 +128,9 @@ class TSInterpreter( ::mapLocalToIdxMapper, ) - // (method, localIdx) -> idx + // (method, localName) -> idx private val localVarToIdx = mutableMapOf>() - // TODO: now we need to explicitly evaluate indices of registers, because we don't have specific ULValues private fun mapLocalToIdxMapper(method: EtsMethod, local: EtsValue) = when (local) { is EtsLocal -> localVarToIdx From ff99b4c8328072e718759bb13a7e90172326b180 Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Mon, 29 Jul 2024 13:26:26 +0300 Subject: [PATCH 06/22] Remove TSTypeSystem --- .../src/main/kotlin/org/usvm/TSTypeSystem.kt | 131 ++---------------- 1 file changed, 8 insertions(+), 123 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt index ef097d845..9402a8850 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt @@ -1,24 +1,10 @@ package org.usvm -import kotlin.time.Duration -import kotlinx.collections.immutable.PersistentList -import kotlinx.collections.immutable.persistentListOf -import org.jacodb.ets.base.EtsAnyType -import org.jacodb.ets.base.EtsArrayType -import org.jacodb.ets.base.EtsBooleanType -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsNumberType -import org.jacodb.ets.base.EtsPrimitiveType -import org.jacodb.ets.base.EtsStringType import org.jacodb.ets.base.EtsType -import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFile -import org.usvm.types.TypesResult -import org.usvm.types.TypesResult.Companion.toTypesResult -import org.usvm.types.USingleTypeStream import org.usvm.types.UTypeStream import org.usvm.types.UTypeSystem -import org.usvm.types.emptyTypeStream +import kotlin.time.Duration class TSTypeSystem( override val typeOperationsTimeout: Duration, @@ -26,127 +12,26 @@ class TSTypeSystem( ) : UTypeSystem { override fun isSupertype(supertype: EtsType, type: EtsType): Boolean { - return when { - supertype == type -> return true - type is EtsPrimitiveType -> return false - type is EtsClassType -> supertype.checkSubtype(type.classSignature) - else -> false - } + TODO() } override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean { - when (type) { - is EtsPrimitiveType -> return types.isEmpty() - is EtsClassType -> return types.all { isSupertype(it, type) } - is EtsArrayType -> { - val elementTypes = types.map { - when { - it is EtsArrayType -> it.elementType - else -> return false - } - } - return hasCommonSubtype(type.elementType, elementTypes) - } - else -> TODO() - } + TODO() } override fun isFinal(type: EtsType): Boolean { - // No final modifier in jacodb IR - return false + TODO() } override fun isInstantiable(type: EtsType): Boolean { - return true + TODO() } - override fun findSubtypes(type: EtsType): Sequence = when (type) { - is EtsPrimitiveType -> emptySequence() - is EtsArrayType -> findSubtypes(type.elementType).map { EtsArrayType(it, type.dimensions) } - is EtsClassType -> TODO() - else -> TODO() + override fun findSubtypes(type: EtsType): Sequence { + TODO() } override fun topTypeStream(): UTypeStream { - return TSTopTypeStream(this) - } - - private fun EtsType.checkSubtype(typeClassSignature: EtsClassSignature?): Boolean { - if (typeClassSignature == null) return false - - return this.typeName == typeClassSignature.name || - this.checkSubtype(project.getClassBySignature(typeClassSignature)?.superClass) + TODO() } } - -class TSTopTypeStream( - private val typeSystem: TSTypeSystem, - val primitiveTypes: PersistentList = persistentListOf( - EtsNumberType, - EtsBooleanType, - EtsStringType - ), -) : UTypeStream { - override fun filterBySupertype(type: EtsType): UTypeStream { - if (type is EtsPrimitiveType) { - if (type !in primitiveTypes) { - return emptyTypeStream() - } - - return USingleTypeStream(typeSystem, type) - } - - return emptyTypeStream() - } - - override fun filterBySubtype(type: EtsType): UTypeStream { - if (type is EtsPrimitiveType) { - if (type !in primitiveTypes) { - return emptyTypeStream() - } - - return USingleTypeStream(typeSystem, type) - } - - return emptyTypeStream() - } - - override fun filterByNotSupertype(type: EtsType): UTypeStream { - if (type is EtsPrimitiveType && type in primitiveTypes) { - val updatedPrimitiveTypes = primitiveTypes.remove(type) - - if (updatedPrimitiveTypes.isEmpty()) { - return emptyTypeStream() - } - - return TSTopTypeStream(typeSystem, updatedPrimitiveTypes) - } - - return TSTopTypeStream(typeSystem, primitiveTypes) - } - - override fun filterByNotSubtype(type: EtsType): UTypeStream { - if (type is EtsPrimitiveType && type in primitiveTypes) { - val updatedPrimitiveTypes = primitiveTypes.remove(type) - - if (updatedPrimitiveTypes.isEmpty()) { - return emptyTypeStream() - } - - return TSTopTypeStream(typeSystem, updatedPrimitiveTypes) - } - - return TSTopTypeStream(typeSystem, primitiveTypes) - } - - override fun take(n: Int): TypesResult { - return primitiveTypes.take(n).toTypesResult(wasTimeoutExpired = false) - } - - override val isEmpty: Boolean - get() = primitiveTypes.isEmpty() - - override val commonSuperType: EtsType - get() = EtsAnyType - -} From 1cbde1eb9bd6429a641e078201b561048c09be3b Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Mon, 29 Jul 2024 13:28:22 +0300 Subject: [PATCH 07/22] Remove redundant class --- .../src/main/kotlin/org/usvm/TSComponents.kt | 30 +------------------ 1 file changed, 1 insertion(+), 29 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt index 8961ca4a6..e83cb1e13 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt @@ -1,6 +1,5 @@ package org.usvm -import io.ksmt.expr.KBitVec32Value import io.ksmt.solver.yices.KYicesSolver import io.ksmt.solver.z3.KZ3Solver import io.ksmt.symfpu.solver.KSymFpuSolver @@ -19,7 +18,7 @@ class TSComponents( get() = options.useSolverForForks override fun > mkSizeExprProvider(ctx: Context): USizeExprProvider { - return TSFpSortSizeExprProvider(ctx as TSContext) + return UBv32SizeExprProvider(ctx) } override fun mkTypeSystem( @@ -45,30 +44,3 @@ class TSComponents( closeableResources.forEach(AutoCloseable::close) } } - -class TSFpSortSizeExprProvider( - override val ctx: TSContext, -) : USizeExprProvider { - override val sizeSort: TSSizeSort = ctx.sizeSort - - override fun mkSizeExpr(size: Int): UExpr = ctx.mkBv(size, sizeSort) - override fun getIntValue(expr: UExpr): Int? = (expr as? KBitVec32Value)?.numberValue - - override fun mkSizeSubExpr(lhs: UExpr, rhs: UExpr): UExpr = - ctx.mkBvSubExpr(lhs, rhs) - - override fun mkSizeAddExpr(lhs: UExpr, rhs: UExpr): UExpr = - ctx.mkBvAddExpr(lhs, rhs) - - override fun mkSizeGtExpr(lhs: UExpr, rhs: UExpr): UBoolExpr = - ctx.mkBvUnsignedGreaterExpr(lhs, rhs) - - override fun mkSizeGeExpr(lhs: UExpr, rhs: UExpr): UBoolExpr = - ctx.mkBvUnsignedGreaterOrEqualExpr(lhs, rhs) - - override fun mkSizeLtExpr(lhs: UExpr, rhs: UExpr): UBoolExpr = - ctx.mkBvUnsignedLessExpr(lhs, rhs) - - override fun mkSizeLeExpr(lhs: UExpr, rhs: UExpr): UBoolExpr = - ctx.mkBvUnsignedLessOrEqualExpr(lhs, rhs) -} From 9fba9e7afb79207762c1234d15f0691137ffc66d Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Mon, 29 Jul 2024 13:36:24 +0300 Subject: [PATCH 08/22] Remove unfinished types processing --- usvm-ts/src/main/kotlin/org/usvm/TSContext.kt | 14 +------------- .../src/main/kotlin/org/usvm/TSExpressions.kt | 18 +----------------- .../src/main/kotlin/org/usvm/TSInterpreter.kt | 4 ---- 3 files changed, 2 insertions(+), 34 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt index 97902dbf8..fee2c9d9d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt @@ -1,33 +1,21 @@ package org.usvm -import org.jacodb.ets.base.EtsAnyType import org.jacodb.ets.base.EtsBooleanType import org.jacodb.ets.base.EtsNumberType -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.EtsVoidType typealias TSSizeSort = UBv32Sort class TSContext(components: TSComponents) : UContext(components) { - val voidSort: TSVoidSort by lazy { TSVoidSort(this) } val undefinedSort: TSUndefinedSort by lazy { TSUndefinedSort(this) } - val stringSort: TSStringSort by lazy { TSStringSort(this) } private val undefinedValue by lazy { TSUndefinedValue(this) } fun typeToSort(type: EtsType): USort = when (type) { - is EtsAnyType -> addressSort - is EtsVoidType -> voidSort - is EtsUndefinedType -> undefinedSort - is EtsRefType -> addressSort is EtsBooleanType -> boolSort is EtsNumberType -> fp64Sort - is EtsStringType -> stringSort - else -> error("Unknown type: $type") + else -> TODO("Support all JacoDB types") } fun mkUndefinedValue(): TSUndefinedValue = undefinedValue diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt index 887bfc85d..6d48e8823 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt @@ -9,14 +9,6 @@ import io.ksmt.sort.KSortVisitor val KAst.tctx get() = ctx as TSContext -class TSVoidSort(ctx: TSContext) : USort(ctx) { - override fun print(builder: StringBuilder) { - builder.append("void sort") - } - - override fun accept(visitor: KSortVisitor): T = error("Should not be called") -} - class TSUndefinedSort(ctx: TSContext) : USort(ctx) { override fun print(builder: StringBuilder) { builder.append("undefined sort") @@ -25,14 +17,6 @@ class TSUndefinedSort(ctx: TSContext) : USort(ctx) { override fun accept(visitor: KSortVisitor): T = error("Should not be called") } -class TSStringSort(ctx: TSContext) : USort(ctx) { - override fun print(builder: StringBuilder) { - builder.append("string sort") - } - - override fun accept(visitor: KSortVisitor): T = error("Should not be called") -} - class TSUndefinedValue(ctx: TSContext) : UExpr(ctx) { override val sort: TSUndefinedSort get() = tctx.undefinedSort @@ -47,4 +31,4 @@ class TSUndefinedValue(ctx: TSContext) : UExpr(ctx) { printer.append("undefined") } -} \ No newline at end of file +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt index 052e7eeaa..99e7d0fdc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt @@ -71,10 +71,6 @@ class TSInterpreter( else -> error("Unknown stmt: $stmt") } -// stmt.nextStmt?.let { nextStmt -> -// scope.doWithState { newStmt(nextStmt) } -// } - return scope.stepResult() } From a22bec019ccac57830b694ff008fda60d9545edf Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Mon, 29 Jul 2024 14:34:37 +0300 Subject: [PATCH 09/22] Detekt fix --- usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt | 1 - usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt | 1 - usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt | 2 +- usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt | 2 +- 4 files changed, 2 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt index 051a9d57b..03dddb795 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt @@ -263,5 +263,4 @@ class TSSimpleValueResolver( val sort = ctx.typeToSort(local.type) return URegisterStackLValue(sort, localIdx) } - } diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt index 6d48e8823..4808809e7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt @@ -30,5 +30,4 @@ class TSUndefinedValue(ctx: TSContext) : UExpr(ctx) { override fun print(printer: ExpressionPrinter) { printer.append("undefined") } - } diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt index c6251e0cb..4e5635648 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSMachine.kt @@ -1,6 +1,5 @@ package org.usvm -import kotlin.time.Duration.Companion.seconds import org.jacodb.ets.base.EtsStmt import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsMethod @@ -18,6 +17,7 @@ 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, diff --git a/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt index 87bfe1c87..223ff4e21 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt @@ -26,4 +26,4 @@ fun TSState.returnValue(valueToReturn: UExpr) { fun EtsMethod.localIdx(idx: Int) = if (isStatic) idx else idx + 1 -inline val EtsMethod.parametersWithThisCount get() = localIdx(parameters.size) \ No newline at end of file +inline val EtsMethod.parametersWithThisCount get() = localIdx(parameters.size) From ceb7ec57f2997ccf1a4d591a9de10924241bea85 Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Mon, 29 Jul 2024 15:45:18 +0300 Subject: [PATCH 10/22] [WIP] Args location tests --- .../main/kotlin/org/usvm/TSExprResolver.kt | 10 +- .../src/main/kotlin/org/usvm/TSInterpreter.kt | 11 +- usvm-ts/src/main/kotlin/org/usvm/Utils.kt | 9 + .../kotlin/org/usvm/samples/StaticMethods.kt | 20 + .../ir/{MinValue.json => MinValue.ts.json} | 0 .../test/resources/ir/StaticMethods.ts.json | 638 ++++++++++++++++++ .../test/resources/samples/StaticMethods.ts | 13 + 7 files changed, 699 insertions(+), 2 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/Utils.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/StaticMethods.kt rename usvm-ts/src/test/resources/ir/{MinValue.json => MinValue.ts.json} (100%) create mode 100644 usvm-ts/src/test/resources/ir/StaticMethods.ts.json create mode 100644 usvm-ts/src/test/resources/samples/StaticMethods.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt index 03dddb795..f61e4592d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt @@ -29,6 +29,7 @@ import org.jacodb.ets.base.EtsUnaryOperation import org.jacodb.ets.base.EtsUndefinedConstant import org.jacodb.ets.base.EtsValue import org.jacodb.ets.model.EtsMethod +import org.usvm.memory.ULValue import org.usvm.memory.URegisterStackLValue @Suppress("UNUSED_PARAMETER") @@ -45,9 +46,16 @@ class TSExprResolver( ) fun resolveTSExpr(expr: EtsEntity, type: EtsType = expr.type): UExpr? { - TODO() + return expr.accept(this) } + fun resolveLValue(value: EtsValue): ULValue<*, *>? = + when (value) { + is EtsParameterRef, + is EtsLocal -> simpleValueResolver.resolveLocal(value) + else -> error("Unexpected value: $value") + } + override fun visit(value: EtsLocal): UExpr { TODO("Not yet implemented") } diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt index 99e7d0fdc..408c32b51 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt @@ -94,7 +94,16 @@ class TSInterpreter( } private fun visitAssignStmt(scope: TSStepScope, stmt: EtsAssignStmt) { - TODO() + val exprResolver = exprResolverWithScope(scope) + + val lvalue = exprResolver.resolveLValue(stmt.lhv) ?: return + val expr = exprResolver.resolveTSExpr(stmt.rhv, stmt.lhv.type) ?: return + + scope.doWithState { + memory.write(lvalue, expr) + val nextStmt = stmt.nextStmt ?: return@doWithState + newStmt(nextStmt) + } } private fun visitCallStmt(scope: TSStepScope, stmt: EtsCallStmt) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/Utils.kt new file mode 100644 index 000000000..3fe60ae3d --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/Utils.kt @@ -0,0 +1,9 @@ +package org.usvm + +import org.usvm.memory.ULValue +import org.usvm.memory.UWritableMemory + +@Suppress("UNCHECKED_CAST") +fun UWritableMemory<*>.write(ref: ULValue<*, *>, value: UExpr<*>) { + write(ref as ULValue<*, USort>, value as UExpr, value.uctx.trueExpr) +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/StaticMethods.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/StaticMethods.kt new file mode 100644 index 000000000..72f548bd7 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/StaticMethods.kt @@ -0,0 +1,20 @@ +package org.usvm.samples + +import org.usvm.TSObject +import org.usvm.util.MethodDescriptor +import org.usvm.util.TSMethodTestRunner +import kotlin.test.Test + +class StaticMethods : TSMethodTestRunner() { + @Test + fun testNoArgsStaticMethod() { + discoverProperties( + methodIdentifier = MethodDescriptor( + fileName = "StaticMethods.ts", + className = "StaticMethods", + methodName = "noArguments", + argumentsNumber = 0 + ) + ) + } +} diff --git a/usvm-ts/src/test/resources/ir/MinValue.json b/usvm-ts/src/test/resources/ir/MinValue.ts.json similarity index 100% rename from usvm-ts/src/test/resources/ir/MinValue.json rename to usvm-ts/src/test/resources/ir/MinValue.ts.json diff --git a/usvm-ts/src/test/resources/ir/StaticMethods.ts.json b/usvm-ts/src/test/resources/ir/StaticMethods.ts.json new file mode 100644 index 000000000..163624c53 --- /dev/null +++ b/usvm-ts/src/test/resources/ir/StaticMethods.ts.json @@ -0,0 +1,638 @@ +{ + "name": "StaticMethods.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": { + "name": "StaticMethods" + }, + "modifiers": [], + "typeParameters": [], + "superClassName": "", + "implementedInterfaceNames": [], + "fields": [], + "methods": [ + { + "signature": { + "enclosingClass": { + "name": "StaticMethods" + }, + "name": "@instance_init", + "parameters": [], + "returnType": { + "_": "UnknownType" + } + }, + "modifiers": [], + "typeParameters": [], + "body": { + "locals": [], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "StaticMethods" + } + } + } + }, + { + "_": "ReturnVoidStmt" + } + ] + } + ] + } + } + }, + { + "signature": { + "enclosingClass": { + "name": "StaticMethods" + }, + "name": "@static_init", + "parameters": [], + "returnType": { + "_": "UnknownType" + } + }, + "modifiers": [], + "typeParameters": [], + "body": { + "locals": [], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "StaticMethods" + } + } + } + }, + { + "_": "ReturnVoidStmt" + } + ] + } + ] + } + } + }, + { + "signature": { + "enclosingClass": { + "name": "StaticMethods" + }, + "name": "constructor", + "parameters": [], + "returnType": { + "_": "UnknownType" + } + }, + "modifiers": [], + "typeParameters": [], + "body": { + "locals": [], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "StaticMethods" + } + } + } + }, + { + "_": "CallStmt", + "expr": { + "_": "InstanceCallExpr", + "instance": { + "_": "Local", + "name": "this", + "type": { + "_": "UnknownType" + } + }, + "method": { + "enclosingClass": { + "name": "StaticMethods" + }, + "name": "@instance_init", + "parameters": [], + "returnType": { + "_": "UnknownType" + } + }, + "args": [] + } + }, + { + "_": "ReturnVoidStmt" + } + ] + } + ] + } + } + }, + { + "signature": { + "enclosingClass": { + "name": "StaticMethods" + }, + "name": "noArguments", + "parameters": [], + "returnType": { + "_": "UnclearReferenceType", + "name": "Number" + } + }, + "modifiers": [ + "StaticKeyword" + ], + "typeParameters": [], + "body": { + "locals": [ + { + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "StaticMethods" + } + } + } + ], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "StaticMethods" + } + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "StaticMethods" + } + } + } + }, + { + "_": "ReturnStmt", + "arg": { + "_": "Constant", + "value": "42", + "type": { + "_": "NumberType" + } + } + } + ] + } + ] + } + } + }, + { + "signature": { + "enclosingClass": { + "name": "StaticMethods" + }, + "name": "singleArgument", + "parameters": [ + { + "name": "a", + "type": { + "_": "UnknownType" + }, + "isOptional": false + } + ], + "returnType": { + "_": "UnknownType" + } + }, + "modifiers": [ + "StaticKeyword" + ], + "typeParameters": [], + "body": { + "locals": [ + { + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "StaticMethods" + } + } + }, + { + "name": "a", + "type": { + "_": "UnknownType" + } + } + ], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "a", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "ParameterRef", + "index": 0, + "type": { + "_": "UnknownType" + } + } + }, + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "StaticMethods" + } + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "StaticMethods" + } + } + } + }, + { + "_": "ReturnStmt", + "arg": { + "_": "Local", + "name": "a", + "type": { + "_": "UnknownType" + } + } + } + ] + } + ] + } + } + }, + { + "signature": { + "enclosingClass": { + "name": "StaticMethods" + }, + "name": "manyArguments", + "parameters": [ + { + "name": "a", + "type": { + "_": "UnknownType" + }, + "isOptional": false + }, + { + "name": "b", + "type": { + "_": "UnknownType" + }, + "isOptional": false + }, + { + "name": "c", + "type": { + "_": "UnknownType" + }, + "isOptional": false + }, + { + "name": "d", + "type": { + "_": "UnknownType" + }, + "isOptional": false + } + ], + "returnType": { + "_": "UnknownType" + } + }, + "modifiers": [ + "StaticKeyword" + ], + "typeParameters": [], + "body": { + "locals": [ + { + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "StaticMethods" + } + } + }, + { + "name": "a", + "type": { + "_": "UnknownType" + } + }, + { + "name": "b", + "type": { + "_": "UnknownType" + } + }, + { + "name": "c", + "type": { + "_": "UnknownType" + } + }, + { + "name": "d", + "type": { + "_": "UnknownType" + } + } + ], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "a", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "ParameterRef", + "index": 0, + "type": { + "_": "UnknownType" + } + } + }, + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "b", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "ParameterRef", + "index": 1, + "type": { + "_": "UnknownType" + } + } + }, + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "c", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "ParameterRef", + "index": 2, + "type": { + "_": "UnknownType" + } + } + }, + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "d", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "ParameterRef", + "index": 3, + "type": { + "_": "UnknownType" + } + } + }, + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "StaticMethods" + } + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "StaticMethods" + } + } + } + }, + { + "_": "ReturnStmt", + "arg": { + "_": "Local", + "name": "d", + "type": { + "_": "UnknownType" + } + } + } + ] + } + ] + } + } + } + ] + } + ], + "importInfos": [], + "exportInfos": [] +} \ No newline at end of file diff --git a/usvm-ts/src/test/resources/samples/StaticMethods.ts b/usvm-ts/src/test/resources/samples/StaticMethods.ts new file mode 100644 index 000000000..051489b65 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/StaticMethods.ts @@ -0,0 +1,13 @@ +class StaticMethods { + static noArguments(): Number { + return 42 + } + + static singleArgument(a) { + return a + } + + static manyArguments(a, b, c, d) { + return d + } +} From 9a6e1a6ca35f2fde8bf975ef3e75cbc4c3a36eef Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Wed, 31 Jul 2024 18:50:09 +0300 Subject: [PATCH 11/22] Implement parameters resolver with tests --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- .../kotlin/org/usvm/TSApplicationGraph.kt | 4 +- .../main/kotlin/org/usvm/TSBinaryOperator.kt | 42 + usvm-ts/src/main/kotlin/org/usvm/TSContext.kt | 2 + .../main/kotlin/org/usvm/TSExprResolver.kt | 257 ++++-- .../src/main/kotlin/org/usvm/TSExpressions.kt | 11 + .../src/main/kotlin/org/usvm/TSInterpreter.kt | 32 +- .../test/kotlin/org/usvm/samples/Arguments.kt | 40 +- .../kotlin/org/usvm/samples/StaticMethods.kt | 24 + .../org/usvm/util/TSMethodTestRunner.kt | 11 +- .../kotlin/org/usvm/util/TSTestResolver.kt | 86 +- .../src/test/resources/ir/Arguments.ts.json | 849 ++++++++++++++++++ .../test/resources/ir/StaticMethods.ts.json | 351 +++++++- .../src/test/resources/samples/Arguments.ts | 12 +- .../test/resources/samples/StaticMethods.ts | 18 +- 15 files changed, 1627 insertions(+), 114 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt create mode 100644 usvm-ts/src/test/resources/ir/Arguments.ts.json diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 0376f0a0e..5ed9390ec 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -5,7 +5,7 @@ import org.gradle.plugin.use.PluginDependenciesSpec object Versions { const val detekt = "1.18.1" const val ini4j = "0.5.4" - const val jacodb = "4b15fc6452" + const val jacodb = "4164b3cc64" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "1.9.20" diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt b/usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt index dc734e37b..b49d4033e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt @@ -1,13 +1,13 @@ package org.usvm import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.graph.EtsApplicationGraph +import org.jacodb.ets.graph.EtsApplicationGraphImpl 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) + private val applicationGraph = EtsApplicationGraphImpl(project) override fun predecessors(node: EtsStmt): Sequence = applicationGraph.predecessors(node) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt new file mode 100644 index 000000000..8519dd844 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt @@ -0,0 +1,42 @@ +package org.usvm + +import io.ksmt.utils.cast + +sealed class TSBinaryOperator( + val onBool: TSContext.(UExpr, UExpr) -> UExpr = shouldNotBeCalled, + val onBv: TSContext.(UExpr, UExpr) -> UExpr = shouldNotBeCalled, + val onFp: TSContext.(UExpr, UExpr) -> UExpr = shouldNotBeCalled, +) { + + object Eq : TSBinaryOperator( + onBool = UContext::mkEq, + onBv = UContext::mkEq, + onFp = UContext::mkFpEqualExpr, + ) + + object Neq : TSBinaryOperator( + onBool = { lhs, rhs -> lhs.neq(rhs) }, + onBv = { lhs, rhs -> lhs.neq(rhs) }, + onFp = { lhs, rhs -> mkFpEqualExpr(lhs, rhs).not() }, + ) + + internal operator fun invoke(lhs: UExpr, rhs: UExpr): UExpr { + val lhsSort = lhs.sort + val rhsSort = rhs.sort + + if (lhsSort != rhsSort) TODO("Implement type coercion") + + return when { + lhsSort is UBoolSort -> lhs.tctx.onBool(lhs.cast(), rhs.cast()) + lhsSort is UBvSort -> lhs.tctx.onBv(lhs.cast(), rhs.cast()) + lhsSort is UFpSort -> lhs.tctx.onFp(lhs.cast(), rhs.cast()) + + else -> error("Unexpected sorts: $lhsSort, $rhsSort") + } + } + + companion object { + private val shouldNotBeCalled: TSContext.(UExpr, UExpr) -> UExpr = + { _, _ -> error("Should not be called") } + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt index fee2c9d9d..fa5d8bbd1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt @@ -2,6 +2,7 @@ package org.usvm import org.jacodb.ets.base.EtsBooleanType import org.jacodb.ets.base.EtsNumberType +import org.jacodb.ets.base.EtsRefType import org.jacodb.ets.base.EtsType typealias TSSizeSort = UBv32Sort @@ -15,6 +16,7 @@ class TSContext(components: TSComponents) : UContext(components) { fun typeToSort(type: EtsType): USort = when (type) { is EtsBooleanType -> boolSort is EtsNumberType -> fp64Sort + is EtsRefType -> addressSort else -> TODO("Support all JacoDB types") } diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt index f61e4592d..108b4ad54 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt @@ -1,33 +1,66 @@ package org.usvm +import org.jacodb.ets.base.EtsAddExpr +import org.jacodb.ets.base.EtsAndExpr import org.jacodb.ets.base.EtsArrayAccess import org.jacodb.ets.base.EtsArrayLiteral -import org.jacodb.ets.base.EtsBinaryOperation +import org.jacodb.ets.base.EtsBinaryExpr +import org.jacodb.ets.base.EtsBitAndExpr +import org.jacodb.ets.base.EtsBitNotExpr +import org.jacodb.ets.base.EtsBitOrExpr +import org.jacodb.ets.base.EtsBitXorExpr import org.jacodb.ets.base.EtsBooleanConstant import org.jacodb.ets.base.EtsCastExpr +import org.jacodb.ets.base.EtsCommaExpr import org.jacodb.ets.base.EtsDeleteExpr +import org.jacodb.ets.base.EtsDivExpr import org.jacodb.ets.base.EtsEntity +import org.jacodb.ets.base.EtsEqExpr +import org.jacodb.ets.base.EtsExpExpr +import org.jacodb.ets.base.EtsGtEqExpr +import org.jacodb.ets.base.EtsGtExpr +import org.jacodb.ets.base.EtsInExpr import org.jacodb.ets.base.EtsInstanceCallExpr import org.jacodb.ets.base.EtsInstanceFieldRef import org.jacodb.ets.base.EtsInstanceOfExpr +import org.jacodb.ets.base.EtsLeftShiftExpr import org.jacodb.ets.base.EtsLengthExpr import org.jacodb.ets.base.EtsLocal +import org.jacodb.ets.base.EtsLtEqExpr +import org.jacodb.ets.base.EtsLtExpr +import org.jacodb.ets.base.EtsMulExpr +import org.jacodb.ets.base.EtsNegExpr import org.jacodb.ets.base.EtsNewArrayExpr import org.jacodb.ets.base.EtsNewExpr +import org.jacodb.ets.base.EtsNotEqExpr +import org.jacodb.ets.base.EtsNotExpr import org.jacodb.ets.base.EtsNullConstant +import org.jacodb.ets.base.EtsNullishCoalescingExpr import org.jacodb.ets.base.EtsNumberConstant import org.jacodb.ets.base.EtsObjectLiteral +import org.jacodb.ets.base.EtsOrExpr import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsRelationOperation +import org.jacodb.ets.base.EtsPostDecExpr +import org.jacodb.ets.base.EtsPostIncExpr +import org.jacodb.ets.base.EtsPreDecExpr +import org.jacodb.ets.base.EtsPreIncExpr +import org.jacodb.ets.base.EtsRemExpr +import org.jacodb.ets.base.EtsRightShiftExpr import org.jacodb.ets.base.EtsStaticCallExpr import org.jacodb.ets.base.EtsStaticFieldRef +import org.jacodb.ets.base.EtsStrictEqExpr +import org.jacodb.ets.base.EtsStrictNotEqExpr import org.jacodb.ets.base.EtsStringConstant +import org.jacodb.ets.base.EtsSubExpr +import org.jacodb.ets.base.EtsTernaryExpr import org.jacodb.ets.base.EtsThis import org.jacodb.ets.base.EtsType import org.jacodb.ets.base.EtsTypeOfExpr -import org.jacodb.ets.base.EtsUnaryOperation +import org.jacodb.ets.base.EtsUnaryPlusExpr import org.jacodb.ets.base.EtsUndefinedConstant +import org.jacodb.ets.base.EtsUnsignedRightShiftExpr import org.jacodb.ets.base.EtsValue +import org.jacodb.ets.base.EtsVoidExpr import org.jacodb.ets.model.EtsMethod import org.usvm.memory.ULValue import org.usvm.memory.URegisterStackLValue @@ -37,7 +70,7 @@ class TSExprResolver( private val ctx: TSContext, private val scope: TSStepScope, private val localToIdx: (EtsMethod, EtsValue) -> Int, -) : EtsEntity.Visitor> { +) : EtsEntity.Visitor?> { val simpleValueResolver: TSSimpleValueResolver = TSSimpleValueResolver( ctx, @@ -56,8 +89,33 @@ class TSExprResolver( else -> error("Unexpected value: $value") } + private fun resolveBinaryOperator( + operator: TSBinaryOperator, + expr: EtsBinaryExpr, + ): UExpr? = resolveBinaryOperator(operator, expr.left, expr.right) + + private fun resolveBinaryOperator( + operator: TSBinaryOperator, + lhv: EtsEntity, + rhv: EtsEntity, + ): UExpr? = resolveAfterResolved(lhv, rhv) { lhs, rhs -> + operator(lhs, rhs) + } + + private inline fun resolveAfterResolved( + dependency0: EtsEntity, + dependency1: EtsEntity, + block: (UExpr, UExpr) -> T, + ): T? { + val result0 = resolveTSExpr(dependency0) ?: return null + val result1 = resolveTSExpr(dependency1) ?: return null + return block(result0, result1) + } + + + override fun visit(value: EtsLocal): UExpr { - TODO("Not yet implemented") + return simpleValueResolver.visit(value) } override fun visit(value: EtsArrayLiteral): UExpr { @@ -65,15 +123,15 @@ class TSExprResolver( } override fun visit(value: EtsBooleanConstant): UExpr { - TODO("Not yet implemented") + return simpleValueResolver.visit(value) } override fun visit(value: EtsNullConstant): UExpr { - TODO("Not yet implemented") + return simpleValueResolver.visit(value) } override fun visit(value: EtsNumberConstant): UExpr { - TODO("Not yet implemented") + return simpleValueResolver.visit(value) } override fun visit(value: EtsObjectLiteral): UExpr { @@ -88,7 +146,27 @@ class TSExprResolver( TODO("Not yet implemented") } - override fun visit(expr: EtsBinaryOperation): UExpr { + override fun visit(expr: EtsAddExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsAndExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsBitAndExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsBitNotExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsBitOrExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsBitXorExpr): UExpr { TODO("Not yet implemented") } @@ -96,10 +174,38 @@ class TSExprResolver( TODO("Not yet implemented") } + override fun visit(expr: EtsCommaExpr): UExpr { + TODO("Not yet implemented") + } + override fun visit(expr: EtsDeleteExpr): UExpr { TODO("Not yet implemented") } + override fun visit(expr: EtsDivExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsEqExpr): UExpr? { + return resolveBinaryOperator(TSBinaryOperator.Eq, expr) + } + + override fun visit(expr: EtsExpExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsGtEqExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsGtExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsInExpr): UExpr { + TODO("Not yet implemented") + } + override fun visit(expr: EtsInstanceCallExpr): UExpr { TODO("Not yet implemented") } @@ -108,161 +214,194 @@ class TSExprResolver( TODO("Not yet implemented") } - override fun visit(expr: EtsLengthExpr): UExpr { + override fun visit(expr: EtsLeftShiftExpr): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsNewArrayExpr): UExpr { + override fun visit(expr: EtsLengthExpr): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsNewExpr): UExpr { + override fun visit(expr: EtsLtEqExpr): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsRelationOperation): UExpr { + override fun visit(expr: EtsLtExpr): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsStaticCallExpr): UExpr { + override fun visit(expr: EtsMulExpr): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsTypeOfExpr): UExpr { + override fun visit(expr: EtsNegExpr): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsUnaryOperation): UExpr { + override fun visit(expr: EtsNewArrayExpr): UExpr { TODO("Not yet implemented") } - override fun visit(ref: EtsArrayAccess): UExpr { + override fun visit(expr: EtsNewExpr): UExpr { TODO("Not yet implemented") } - override fun visit(ref: EtsInstanceFieldRef): UExpr { + override fun visit(expr: EtsNotEqExpr): UExpr? { + return resolveBinaryOperator(TSBinaryOperator.Neq, expr) + } + + override fun visit(expr: EtsNotExpr): UExpr { TODO("Not yet implemented") } - override fun visit(ref: EtsParameterRef): UExpr { + override fun visit(expr: EtsNullishCoalescingExpr): UExpr { TODO("Not yet implemented") } - override fun visit(ref: EtsStaticFieldRef): UExpr { + override fun visit(expr: EtsOrExpr): UExpr { TODO("Not yet implemented") } - override fun visit(ref: EtsThis): UExpr { + override fun visit(expr: EtsPostDecExpr): UExpr { TODO("Not yet implemented") } -} -class TSSimpleValueResolver( - private val ctx: TSContext, - private val scope: TSStepScope, - private val localToIdx: (EtsMethod, EtsValue) -> Int, -) : EtsEntity.Visitor> { + override fun visit(expr: EtsPostIncExpr): UExpr { + TODO("Not yet implemented") + } - override fun visit(value: EtsLocal): UExpr = with(ctx) { - val lValue = resolveLocal(value) - return scope.calcOnState { memory.read(lValue) } + override fun visit(expr: EtsPreDecExpr): UExpr { + TODO("Not yet implemented") } - override fun visit(value: EtsArrayLiteral): UExpr = with(ctx) { + override fun visit(expr: EtsPreIncExpr): UExpr { TODO("Not yet implemented") } - override fun visit(value: EtsBooleanConstant): UExpr = with(ctx) { - mkBool(value.value) + override fun visit(expr: EtsRemExpr): UExpr { + TODO("Not yet implemented") } - override fun visit(value: EtsNullConstant): UExpr = with(ctx) { - nullRef + override fun visit(expr: EtsRightShiftExpr): UExpr { + TODO("Not yet implemented") } - override fun visit(value: EtsNumberConstant): UExpr = with(ctx) { - mkFp64(value.value) + override fun visit(expr: EtsStaticCallExpr): UExpr { + TODO("Not yet implemented") } - override fun visit(value: EtsObjectLiteral): UExpr = with(ctx) { + override fun visit(expr: EtsStrictEqExpr): UExpr { TODO("Not yet implemented") } - override fun visit(value: EtsStringConstant): UExpr = with(ctx) { + override fun visit(expr: EtsStrictNotEqExpr): UExpr { TODO("Not yet implemented") } - override fun visit(value: EtsUndefinedConstant): UExpr = with(ctx) { + override fun visit(expr: EtsSubExpr): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsBinaryOperation): UExpr = with(ctx) { + override fun visit(expr: EtsTernaryExpr): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsCastExpr): UExpr = with(ctx) { + override fun visit(expr: EtsTypeOfExpr): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsDeleteExpr): UExpr = with(ctx) { + override fun visit(expr: EtsUnaryPlusExpr): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsInstanceCallExpr): UExpr = with(ctx) { + override fun visit(expr: EtsUnsignedRightShiftExpr): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsInstanceOfExpr): UExpr = with(ctx) { + override fun visit(expr: EtsVoidExpr): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsLengthExpr): UExpr = with(ctx) { + override fun visit(value: EtsArrayAccess): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsNewArrayExpr): UExpr = with(ctx) { + override fun visit(value: EtsInstanceFieldRef): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsNewExpr): UExpr = with(ctx) { + override fun visit(value: EtsParameterRef): UExpr { + return simpleValueResolver.visit(value) + } + + override fun visit(value: EtsStaticFieldRef): UExpr { TODO("Not yet implemented") } - override fun visit(expr: EtsRelationOperation): UExpr = with(ctx) { + override fun visit(value: EtsThis): UExpr { + return simpleValueResolver.visit(value) + } +} + +class TSSimpleValueResolver( + private val ctx: TSContext, + private val scope: TSStepScope, + private val localToIdx: (EtsMethod, EtsValue) -> Int, +) : EtsValue.Visitor?> { + + override fun visit(value: EtsLocal): UExpr = with(ctx) { + val lValue = resolveLocal(value) + return scope.calcOnState { memory.read(lValue) } + } + + override fun visit(value: EtsArrayLiteral): UExpr = with(ctx) { TODO("Not yet implemented") } - override fun visit(expr: EtsStaticCallExpr): UExpr = with(ctx) { + override fun visit(value: EtsBooleanConstant): UExpr = with(ctx) { + mkBool(value.value) + } + + override fun visit(value: EtsNullConstant): UExpr = with(ctx) { + nullRef + } + + override fun visit(value: EtsNumberConstant): UExpr = with(ctx) { + mkFp64(value.value) + } + + override fun visit(value: EtsObjectLiteral): UExpr = with(ctx) { TODO("Not yet implemented") } - override fun visit(expr: EtsTypeOfExpr): UExpr = with(ctx) { + override fun visit(value: EtsStringConstant): UExpr = with(ctx) { TODO("Not yet implemented") } - override fun visit(expr: EtsUnaryOperation): UExpr = with(ctx) { + override fun visit(value: EtsUndefinedConstant): UExpr = with(ctx) { TODO("Not yet implemented") } - override fun visit(ref: EtsArrayAccess): UExpr = with(ctx) { + override fun visit(value: EtsArrayAccess): UExpr = with(ctx) { TODO("Not yet implemented") } - override fun visit(ref: EtsInstanceFieldRef): UExpr = with(ctx) { + override fun visit(value: EtsInstanceFieldRef): UExpr = with(ctx) { TODO("Not yet implemented") } - override fun visit(ref: EtsParameterRef): UExpr = with(ctx) { - val lValue = resolveLocal(ref) + override fun visit(value: EtsParameterRef): UExpr = with(ctx) { + val lValue = resolveLocal(value) return scope.calcOnState { memory.read(lValue) } } - override fun visit(ref: EtsStaticFieldRef): UExpr = with(ctx) { + override fun visit(value: EtsStaticFieldRef): UExpr = with(ctx) { TODO("Not yet implemented") } - override fun visit(ref: EtsThis): UExpr = with(ctx) { - TODO("Not yet implemented") + override fun visit(value: EtsThis): UExpr = with(ctx) { + val lValue = resolveLocal(value) + scope.calcOnState { memory.read(lValue) } } fun resolveLocal(local: EtsValue): URegisterStackLValue<*> { diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt index 4808809e7..9019a6ce9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt @@ -3,6 +3,8 @@ package org.usvm import io.ksmt.KAst import io.ksmt.cache.hash import io.ksmt.cache.structurallyEqual +import io.ksmt.expr.KBitVec32Value +import io.ksmt.expr.KFp64Value import io.ksmt.expr.printer.ExpressionPrinter import io.ksmt.expr.transformer.KTransformerBase import io.ksmt.sort.KSortVisitor @@ -31,3 +33,12 @@ class TSUndefinedValue(ctx: TSContext) : UExpr(ctx) { printer.append("undefined") } } + +fun extractBool(expr: UExpr): Boolean = when (expr) { + expr.ctx.trueExpr -> true + expr.ctx.falseExpr -> false + else -> error("Expression $expr is not boolean") +} + +fun extractInt(expr: UExpr): Int = (expr as? KBitVec32Value)?.intValue ?: 0 +fun extractDouble(expr: UExpr): Double = (expr as? KFp64Value)?.value ?: 0.0 diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt index 408c32b51..9501f2128 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt @@ -75,7 +75,23 @@ class TSInterpreter( } private fun visitIfStmt(scope: TSStepScope, stmt: EtsIfStmt) { - TODO() + val exprResolver = exprResolverWithScope(scope) + + val boolExpr = exprResolver + .resolveTSExpr(stmt.condition) + ?.asExpr(ctx.boolSort) + ?: return + + val succs = applicationGraph.successors(stmt).take(2).toList() + val (posStmt, negStmt) = succs[0] to succs[1] + + scope.forkWithBlackList( + boolExpr, + posStmt, + negStmt, + blockOnTrueState = { newStmt(posStmt) }, + blockOnFalseState = { newStmt(negStmt) } + ) } private fun visitReturnStmt(scope: TSStepScope, stmt: EtsReturnStmt) { @@ -138,11 +154,15 @@ class TSInterpreter( private fun mapLocalToIdxMapper(method: EtsMethod, local: EtsValue) = when (local) { - is EtsLocal -> localVarToIdx - .getOrPut(method) { mutableMapOf() } - .run { - getOrPut(local.name) { method.parametersWithThisCount + size } - } + is EtsLocal -> { + // See https://github.com/UnitTestBot/usvm/issues/202 + if (local.name == "this") 0 else + localVarToIdx + .getOrPut(method) { mutableMapOf() } + .run { + getOrPut(local.name) { method.parametersWithThisCount + size } + } + } is EtsThis -> 0 is EtsParameterRef -> method.localIdx(local.index) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Arguments.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Arguments.kt index a100e9def..bd43346c6 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Arguments.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Arguments.kt @@ -8,8 +8,7 @@ import kotlin.test.Test class Arguments : TSMethodTestRunner() { @Test - @Disabled - fun testMinValue() { + fun testNoArgs() { discoverProperties( methodIdentifier = MethodDescriptor( fileName = "Arguments.ts", @@ -19,4 +18,41 @@ class Arguments : TSMethodTestRunner() { ) ) } + + @Test + fun testSingleArg() { + discoverProperties( + methodIdentifier = MethodDescriptor( + fileName = "Arguments.ts", + className = "SimpleClass", + methodName = "singleArgument", + argumentsNumber = 1 + ) + ) + } + + @Test + fun testManyArgs() { + discoverProperties( + methodIdentifier = MethodDescriptor( + fileName = "Arguments.ts", + className = "SimpleClass", + methodName = "manyArguments", + argumentsNumber = 3 + ) + ) + } + + @Test + @Disabled + fun testThisArg() { + discoverProperties( + methodIdentifier = MethodDescriptor( + fileName = "Arguments.ts", + className = "SimpleClass", + methodName = "thisArgument", + argumentsNumber = 0 + ) + ) + } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/StaticMethods.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/StaticMethods.kt index 72f548bd7..afe7f3ac7 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/StaticMethods.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/StaticMethods.kt @@ -17,4 +17,28 @@ class StaticMethods : TSMethodTestRunner() { ) ) } + + @Test + fun testSingleArgStaticMethod() { + discoverProperties( + methodIdentifier = MethodDescriptor( + fileName = "StaticMethods.ts", + className = "StaticMethods", + methodName = "singleArgument", + argumentsNumber = 1 + ) + ) + } + + @Test + fun testManyArgsStaticMethod() { + discoverProperties( + methodIdentifier = MethodDescriptor( + fileName = "StaticMethods.ts", + className = "StaticMethods", + methodName = "manyArguments", + argumentsNumber = 4 + ) + ) + } } 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 f439faeb0..59a30b97c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt @@ -91,9 +91,10 @@ open class TSMethodTestRunner : TestRunner EtsType get() = { - require(it is KClass<*>) { "Only TSObjects are allowed" } + // Both KClass and TSObject instances come here + val temp = if (it is KClass<*> || it == null) it else it::class - when (it) { + when (temp) { TSObject.AnyObject::class -> EtsAnyType TSObject.Array::class -> TODO() TSObject.Boolean::class -> EtsBooleanType @@ -107,8 +108,12 @@ open class TSMethodTestRunner : TestRunner Boolean - get() = TODO("Not yet implemented") + get() = { _, _ -> true } private fun getProject(fileName: String): EtsFile { val jsonWithoutExtension = "/ir/$fileName.json" 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 171ee8281..9c6f0952b 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt @@ -1,12 +1,92 @@ package org.usvm.util +import org.jacodb.ets.base.EtsBooleanType +import org.jacodb.ets.base.EtsLiteralType +import org.jacodb.ets.base.EtsNeverType +import org.jacodb.ets.base.EtsNullType +import org.jacodb.ets.base.EtsNumberType +import org.jacodb.ets.base.EtsPrimitiveType +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.EtsVoidType import org.jacodb.ets.model.EtsMethod +import org.usvm.TSObject import org.usvm.TSTest +import org.usvm.UExpr +import org.usvm.USort +import org.usvm.extractBool +import org.usvm.extractDouble +import org.usvm.extractInt +import org.usvm.memory.URegisterStackLValue +import org.usvm.state.TSMethodResult import org.usvm.state.TSState +import org.usvm.state.localIdx -@Suppress("UNUSED_PARAMETER") class TSTestResolver { - fun resolve(method: EtsMethod, state: TSState): TSTest { - TODO() + + fun resolve(method: EtsMethod, state: TSState): TSTest = with(state.ctx) { + val model = state.models.first() + when (val methodResult = state.methodResult) { + is TSMethodResult.Success -> { + val returnValue = resolveExpr(model.eval(methodResult.value), method.returnType) + val params = method.parameters.mapIndexed { idx, param -> + val registerIdx = method.localIdx(idx) + val lValue = URegisterStackLValue(typeToSort(param.type), registerIdx) + val expr = model.read(lValue) + resolveExpr(expr, param.type) + } + + return TSTest(params, returnValue) + } + is TSMethodResult.TSException -> { + TODO() + } + is TSMethodResult.NoCall -> { + TODO() + } + + else -> error("Should not be called") + } + } + + private fun resolveExpr(expr: UExpr, type: EtsType): TSObject = when (type) { + is EtsPrimitiveType -> resolvePrimitive(expr, type) + is EtsRefType -> TODO() + else -> TODO() + } + + private fun resolvePrimitive(expr: UExpr, type: EtsPrimitiveType): TSObject = when(type) { + EtsNumberType -> { + when (expr.sort) { + expr.ctx.fp64Sort -> TSObject.TSNumber.Double(extractDouble(expr)) + expr.ctx.bv32Sort -> TSObject.TSNumber.Integer(extractInt(expr)) + else -> error("Unexpected sort: ${expr.sort}") + } + } + EtsBooleanType -> { + TSObject.Boolean(extractBool(expr)) + } + EtsUndefinedType -> { + TSObject.UndefinedObject + } + is EtsLiteralType -> { + TODO() + } + EtsNullType -> { + TODO() + } + EtsNeverType -> { + TODO() + } + EtsStringType -> { + TODO() + } + EtsVoidType -> { + TODO() + } + + else -> error("Unexpected type: $type") } } diff --git a/usvm-ts/src/test/resources/ir/Arguments.ts.json b/usvm-ts/src/test/resources/ir/Arguments.ts.json new file mode 100644 index 000000000..cba1c97b3 --- /dev/null +++ b/usvm-ts/src/test/resources/ir/Arguments.ts.json @@ -0,0 +1,849 @@ +{ + "name": "Arguments.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": { + "name": "SimpleClass" + }, + "modifiers": [], + "typeParameters": [], + "superClassName": "", + "implementedInterfaceNames": [], + "fields": [], + "methods": [ + { + "signature": { + "enclosingClass": { + "name": "SimpleClass" + }, + "name": "@instance_init", + "parameters": [], + "returnType": { + "_": "UnknownType" + } + }, + "modifiers": [], + "typeParameters": [], + "body": { + "locals": [], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + } + }, + { + "_": "ReturnVoidStmt" + } + ] + } + ] + } + } + }, + { + "signature": { + "enclosingClass": { + "name": "SimpleClass" + }, + "name": "@static_init", + "parameters": [], + "returnType": { + "_": "UnknownType" + } + }, + "modifiers": [], + "typeParameters": [], + "body": { + "locals": [], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + } + }, + { + "_": "ReturnVoidStmt" + } + ] + } + ] + } + } + }, + { + "signature": { + "enclosingClass": { + "name": "SimpleClass" + }, + "name": "noArguments", + "parameters": [], + "returnType": { + "_": "NumberType" + } + }, + "modifiers": [], + "typeParameters": [], + "body": { + "locals": [ + { + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + } + ], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + } + }, + { + "_": "ReturnStmt", + "arg": { + "_": "Constant", + "value": "42", + "type": { + "_": "NumberType" + } + } + } + ] + } + ] + } + } + }, + { + "signature": { + "enclosingClass": { + "name": "SimpleClass" + }, + "name": "singleArgument", + "parameters": [ + { + "name": "a", + "type": { + "_": "NumberType" + }, + "isOptional": false + } + ], + "returnType": { + "_": "NumberType" + } + }, + "modifiers": [], + "typeParameters": [], + "body": { + "locals": [ + { + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + }, + { + "name": "a", + "type": { + "_": "NumberType" + } + } + ], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "a", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "ParameterRef", + "index": 0, + "type": { + "_": "NumberType" + } + } + }, + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + } + }, + { + "_": "ReturnStmt", + "arg": { + "_": "Local", + "name": "a", + "type": { + "_": "NumberType" + } + } + } + ] + } + ] + } + } + }, + { + "signature": { + "enclosingClass": { + "name": "SimpleClass" + }, + "name": "manyArguments", + "parameters": [ + { + "name": "a", + "type": { + "_": "NumberType" + }, + "isOptional": false + }, + { + "name": "b", + "type": { + "_": "NumberType" + }, + "isOptional": false + }, + { + "name": "c", + "type": { + "_": "NumberType" + }, + "isOptional": false + } + ], + "returnType": { + "_": "NumberType" + } + }, + "modifiers": [], + "typeParameters": [], + "body": { + "locals": [ + { + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + }, + { + "name": "a", + "type": { + "_": "NumberType" + } + }, + { + "name": "b", + "type": { + "_": "NumberType" + } + }, + { + "name": "c", + "type": { + "_": "NumberType" + } + } + ], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [ + 1, + 6 + ], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "a", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "ParameterRef", + "index": 0, + "type": { + "_": "NumberType" + } + } + }, + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "b", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "ParameterRef", + "index": 1, + "type": { + "_": "NumberType" + } + } + }, + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "c", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "ParameterRef", + "index": 2, + "type": { + "_": "NumberType" + } + } + }, + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + } + }, + { + "_": "IfStmt", + "condition": { + "_": "ConditionExpr", + "op": "!=", + "left": { + "_": "Local", + "name": "a", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "Constant", + "value": "1", + "type": { + "_": "NumberType" + } + }, + "type": { + "_": "UnknownType" + } + } + } + ] + }, + { + "id": 1, + "successors": [ + 2, + 5 + ], + "predecessors": [ + 0, + 6 + ], + "stmts": [ + { + "_": "IfStmt", + "condition": { + "_": "ConditionExpr", + "op": "!=", + "left": { + "_": "Local", + "name": "b", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "Constant", + "value": "2", + "type": { + "_": "NumberType" + } + }, + "type": { + "_": "UnknownType" + } + } + } + ] + }, + { + "id": 2, + "successors": [ + 3, + 4 + ], + "predecessors": [ + 1, + 5 + ], + "stmts": [ + { + "_": "IfStmt", + "condition": { + "_": "ConditionExpr", + "op": "!=", + "left": { + "_": "Local", + "name": "c", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "Constant", + "value": "3", + "type": { + "_": "NumberType" + } + }, + "type": { + "_": "UnknownType" + } + } + } + ] + }, + { + "id": 3, + "successors": [], + "predecessors": [ + 2, + 4 + ], + "stmts": [ + { + "_": "ReturnStmt", + "arg": { + "_": "Constant", + "value": "100", + "type": { + "_": "NumberType" + } + } + } + ] + }, + { + "id": 4, + "successors": [ + 3 + ], + "predecessors": [ + 2 + ], + "stmts": [ + { + "_": "ReturnStmt", + "arg": { + "_": "Local", + "name": "c", + "type": { + "_": "NumberType" + } + } + } + ] + }, + { + "id": 5, + "successors": [ + 2 + ], + "predecessors": [ + 1 + ], + "stmts": [ + { + "_": "ReturnStmt", + "arg": { + "_": "Local", + "name": "b", + "type": { + "_": "NumberType" + } + } + } + ] + }, + { + "id": 6, + "successors": [ + 1 + ], + "predecessors": [ + 0 + ], + "stmts": [ + { + "_": "ReturnStmt", + "arg": { + "_": "Local", + "name": "a", + "type": { + "_": "NumberType" + } + } + } + ] + } + ] + } + } + }, + { + "signature": { + "enclosingClass": { + "name": "SimpleClass" + }, + "name": "thisArgument", + "parameters": [], + "returnType": { + "_": "UnclearReferenceType", + "name": "SimpleClass" + } + }, + "modifiers": [], + "typeParameters": [], + "body": { + "locals": [ + { + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + } + ], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + } + }, + { + "_": "ReturnStmt", + "arg": { + "_": "Local", + "name": "this", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + } + } + ] + } + ] + } + } + }, + { + "signature": { + "enclosingClass": { + "name": "SimpleClass" + }, + "name": "constructor", + "parameters": [], + "returnType": { + "_": "UnknownType" + } + }, + "modifiers": [], + "typeParameters": [], + "body": { + "locals": [], + "cfg": { + "blocks": [ + { + "id": 0, + "successors": [], + "predecessors": [], + "stmts": [ + { + "_": "AssignStmt", + "left": { + "_": "Local", + "name": "this", + "type": { + "_": "UnknownType" + } + }, + "right": { + "_": "ThisRef", + "type": { + "_": "ClassType", + "signature": { + "name": "SimpleClass" + } + } + } + }, + { + "_": "CallStmt", + "expr": { + "_": "InstanceCallExpr", + "instance": { + "_": "Local", + "name": "this", + "type": { + "_": "UnknownType" + } + }, + "method": { + "enclosingClass": { + "name": "SimpleClass" + }, + "name": "@instance_init", + "parameters": [], + "returnType": { + "_": "UnknownType" + } + }, + "args": [] + } + }, + { + "_": "ReturnVoidStmt" + } + ] + } + ] + } + } + } + ] + } + ], + "importInfos": [], + "exportInfos": [] +} diff --git a/usvm-ts/src/test/resources/ir/StaticMethods.ts.json b/usvm-ts/src/test/resources/ir/StaticMethods.ts.json index 163624c53..df5a828f3 100644 --- a/usvm-ts/src/test/resources/ir/StaticMethods.ts.json +++ b/usvm-ts/src/test/resources/ir/StaticMethods.ts.json @@ -269,8 +269,7 @@ "name": "noArguments", "parameters": [], "returnType": { - "_": "UnclearReferenceType", - "name": "Number" + "_": "NumberType" } }, "modifiers": [ @@ -344,13 +343,13 @@ { "name": "a", "type": { - "_": "UnknownType" + "_": "NumberType" }, "isOptional": false } ], "returnType": { - "_": "UnknownType" + "_": "NumberType" } }, "modifiers": [ @@ -371,7 +370,7 @@ { "name": "a", "type": { - "_": "UnknownType" + "_": "NumberType" } } ], @@ -379,7 +378,10 @@ "blocks": [ { "id": 0, - "successors": [], + "successors": [ + 1, + 2 + ], "predecessors": [], "stmts": [ { @@ -388,14 +390,14 @@ "_": "Local", "name": "a", "type": { - "_": "UnknownType" + "_": "NumberType" } }, "right": { "_": "ParameterRef", "index": 0, "type": { - "_": "UnknownType" + "_": "NumberType" } } }, @@ -421,13 +423,68 @@ } } }, + { + "_": "IfStmt", + "condition": { + "_": "ConditionExpr", + "op": "!=", + "left": { + "_": "Local", + "name": "a", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "Constant", + "value": "1", + "type": { + "_": "NumberType" + } + }, + "type": { + "_": "UnknownType" + } + } + } + ] + }, + { + "id": 1, + "successors": [], + "predecessors": [ + 0, + 2 + ], + "stmts": [ { "_": "ReturnStmt", "arg": { - "_": "Local", - "name": "a", + "_": "Constant", + "value": "0", "type": { - "_": "UnknownType" + "_": "NumberType" + } + } + } + ] + }, + { + "id": 2, + "successors": [ + 1 + ], + "predecessors": [ + 0 + ], + "stmts": [ + { + "_": "ReturnStmt", + "arg": { + "_": "Constant", + "value": "100", + "type": { + "_": "NumberType" } } } @@ -447,34 +504,34 @@ { "name": "a", "type": { - "_": "UnknownType" + "_": "NumberType" }, "isOptional": false }, { "name": "b", "type": { - "_": "UnknownType" + "_": "NumberType" }, "isOptional": false }, { "name": "c", "type": { - "_": "UnknownType" + "_": "NumberType" }, "isOptional": false }, { "name": "d", "type": { - "_": "UnknownType" + "_": "NumberType" }, "isOptional": false } ], "returnType": { - "_": "UnknownType" + "_": "NumberType" } }, "modifiers": [ @@ -495,25 +552,25 @@ { "name": "a", "type": { - "_": "UnknownType" + "_": "NumberType" } }, { "name": "b", "type": { - "_": "UnknownType" + "_": "NumberType" } }, { "name": "c", "type": { - "_": "UnknownType" + "_": "NumberType" } }, { "name": "d", "type": { - "_": "UnknownType" + "_": "NumberType" } } ], @@ -521,7 +578,10 @@ "blocks": [ { "id": 0, - "successors": [], + "successors": [ + 1, + 8 + ], "predecessors": [], "stmts": [ { @@ -530,14 +590,14 @@ "_": "Local", "name": "a", "type": { - "_": "UnknownType" + "_": "NumberType" } }, "right": { "_": "ParameterRef", "index": 0, "type": { - "_": "UnknownType" + "_": "NumberType" } } }, @@ -547,14 +607,14 @@ "_": "Local", "name": "b", "type": { - "_": "UnknownType" + "_": "NumberType" } }, "right": { "_": "ParameterRef", "index": 1, "type": { - "_": "UnknownType" + "_": "NumberType" } } }, @@ -564,14 +624,14 @@ "_": "Local", "name": "c", "type": { - "_": "UnknownType" + "_": "NumberType" } }, "right": { "_": "ParameterRef", "index": 2, "type": { - "_": "UnknownType" + "_": "NumberType" } } }, @@ -581,14 +641,14 @@ "_": "Local", "name": "d", "type": { - "_": "UnknownType" + "_": "NumberType" } }, "right": { "_": "ParameterRef", "index": 3, "type": { - "_": "UnknownType" + "_": "NumberType" } } }, @@ -614,13 +674,242 @@ } } }, + { + "_": "IfStmt", + "condition": { + "_": "ConditionExpr", + "op": "!=", + "left": { + "_": "Local", + "name": "a", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "Constant", + "value": "1", + "type": { + "_": "NumberType" + } + }, + "type": { + "_": "UnknownType" + } + } + } + ] + }, + { + "id": 1, + "successors": [ + 2, + 7 + ], + "predecessors": [ + 0, + 8 + ], + "stmts": [ + { + "_": "IfStmt", + "condition": { + "_": "ConditionExpr", + "op": "!=", + "left": { + "_": "Local", + "name": "b", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "Constant", + "value": "2", + "type": { + "_": "NumberType" + } + }, + "type": { + "_": "UnknownType" + } + } + } + ] + }, + { + "id": 2, + "successors": [ + 3, + 6 + ], + "predecessors": [ + 1, + 7 + ], + "stmts": [ + { + "_": "IfStmt", + "condition": { + "_": "ConditionExpr", + "op": "!=", + "left": { + "_": "Local", + "name": "c", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "Constant", + "value": "3", + "type": { + "_": "NumberType" + } + }, + "type": { + "_": "UnknownType" + } + } + } + ] + }, + { + "id": 3, + "successors": [ + 4, + 5 + ], + "predecessors": [ + 2, + 6 + ], + "stmts": [ + { + "_": "IfStmt", + "condition": { + "_": "ConditionExpr", + "op": "!=", + "left": { + "_": "Local", + "name": "d", + "type": { + "_": "NumberType" + } + }, + "right": { + "_": "Constant", + "value": "4", + "type": { + "_": "NumberType" + } + }, + "type": { + "_": "UnknownType" + } + } + } + ] + }, + { + "id": 4, + "successors": [], + "predecessors": [ + 3, + 5 + ], + "stmts": [ + { + "_": "ReturnStmt", + "arg": { + "_": "Constant", + "value": "100", + "type": { + "_": "NumberType" + } + } + } + ] + }, + { + "id": 5, + "successors": [ + 4 + ], + "predecessors": [ + 3 + ], + "stmts": [ { "_": "ReturnStmt", "arg": { "_": "Local", "name": "d", "type": { - "_": "UnknownType" + "_": "NumberType" + } + } + } + ] + }, + { + "id": 6, + "successors": [ + 3 + ], + "predecessors": [ + 2 + ], + "stmts": [ + { + "_": "ReturnStmt", + "arg": { + "_": "Local", + "name": "c", + "type": { + "_": "NumberType" + } + } + } + ] + }, + { + "id": 7, + "successors": [ + 2 + ], + "predecessors": [ + 1 + ], + "stmts": [ + { + "_": "ReturnStmt", + "arg": { + "_": "Local", + "name": "b", + "type": { + "_": "NumberType" + } + } + } + ] + }, + { + "id": 8, + "successors": [ + 1 + ], + "predecessors": [ + 0 + ], + "stmts": [ + { + "_": "ReturnStmt", + "arg": { + "_": "Local", + "name": "a", + "type": { + "_": "NumberType" } } } @@ -635,4 +924,4 @@ ], "importInfos": [], "exportInfos": [] -} \ No newline at end of file +} diff --git a/usvm-ts/src/test/resources/samples/Arguments.ts b/usvm-ts/src/test/resources/samples/Arguments.ts index 8f0488e3e..b39ac7a10 100644 --- a/usvm-ts/src/test/resources/samples/Arguments.ts +++ b/usvm-ts/src/test/resources/samples/Arguments.ts @@ -1,12 +1,20 @@ class SimpleClass { - noArguments(): Number { + noArguments(): number { return 42 } - singleArgument(a) { + singleArgument(a: number): number { return a } + manyArguments(a: number, b: number, c: number): number { + if (a == 1) return a + if (b == 2) return b + if (c == 3) return c + + return 100 + } + thisArgument(): SimpleClass { return this } diff --git a/usvm-ts/src/test/resources/samples/StaticMethods.ts b/usvm-ts/src/test/resources/samples/StaticMethods.ts index 051489b65..4e9f5b206 100644 --- a/usvm-ts/src/test/resources/samples/StaticMethods.ts +++ b/usvm-ts/src/test/resources/samples/StaticMethods.ts @@ -1,13 +1,21 @@ class StaticMethods { - static noArguments(): Number { + static noArguments(): number { return 42 } - static singleArgument(a) { - return a + static singleArgument(a: number): number { + if (a == 1) { + return 100 + } + return 0 } - static manyArguments(a, b, c, d) { - return d + static manyArguments(a: number, b: number, c: number, d: number): number { + if (a == 1) return a + if (b == 2) return b + if (c == 3) return c + if (d == 4) return d + + return 100 } } From 8d8ed58da1f214627e86cf0a378bd275cee51ada Mon Sep 17 00:00:00 2001 From: Sergey Loktev <71882967+zishkaz@users.noreply.github.com> Date: Tue, 6 Aug 2024 01:22:34 +0300 Subject: [PATCH 12/22] Remove EtsMethod.localIdx method --- usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt | 10 ++++------ usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt | 5 ----- .../src/test/kotlin/org/usvm/util/TSTestResolver.kt | 4 +--- 3 files changed, 5 insertions(+), 14 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt index 9501f2128..1344c9bae 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt @@ -22,9 +22,7 @@ import org.usvm.solver.USatResult import org.usvm.state.TSMethodResult import org.usvm.state.TSState import org.usvm.state.lastStmt -import org.usvm.state.localIdx import org.usvm.state.newStmt -import org.usvm.state.parametersWithThisCount import org.usvm.state.returnValue import org.usvm.targets.UTargetsSet @@ -155,17 +153,17 @@ class TSInterpreter( private fun mapLocalToIdxMapper(method: EtsMethod, local: EtsValue) = when (local) { is EtsLocal -> { - // See https://github.com/UnitTestBot/usvm/issues/202 - if (local.name == "this") 0 else +// // See https://github.com/UnitTestBot/usvm/issues/202 +// if (local.name == "this") 0 else localVarToIdx .getOrPut(method) { mutableMapOf() } .run { - getOrPut(local.name) { method.parametersWithThisCount + size } + getOrPut(local.name) { method.parameters.size + size } } } is EtsThis -> 0 - is EtsParameterRef -> method.localIdx(local.index) + is EtsParameterRef -> local.index else -> error("Unexpected local: $local") } diff --git a/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt index 223ff4e21..3fd15d301 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt @@ -1,7 +1,6 @@ package org.usvm.state import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.model.EtsMethod import org.usvm.UExpr import org.usvm.USort @@ -23,7 +22,3 @@ fun TSState.returnValue(valueToReturn: UExpr) { newStmt(returnSite) } } - -fun EtsMethod.localIdx(idx: Int) = if (isStatic) idx else idx + 1 - -inline val EtsMethod.parametersWithThisCount get() = localIdx(parameters.size) 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 9c6f0952b..dae64ad01 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt @@ -22,7 +22,6 @@ import org.usvm.extractInt import org.usvm.memory.URegisterStackLValue import org.usvm.state.TSMethodResult import org.usvm.state.TSState -import org.usvm.state.localIdx class TSTestResolver { @@ -32,8 +31,7 @@ class TSTestResolver { is TSMethodResult.Success -> { val returnValue = resolveExpr(model.eval(methodResult.value), method.returnType) val params = method.parameters.mapIndexed { idx, param -> - val registerIdx = method.localIdx(idx) - val lValue = URegisterStackLValue(typeToSort(param.type), registerIdx) + val lValue = URegisterStackLValue(typeToSort(param.type), idx) val expr = model.read(lValue) resolveExpr(expr, param.type) } From 979e1e5753dac18548a13216a0711cd38e157e7c Mon Sep 17 00:00:00 2001 From: Sergey Loktev <71882967+zishkaz@users.noreply.github.com> Date: Wed, 7 Aug 2024 15:14:39 +0300 Subject: [PATCH 13/22] [WIP] Dev sync --- .../src/main/kotlin/org/usvm/TSExprResolver.kt | 2 +- .../kotlin/org/usvm/util/TSMethodTestRunner.kt | 15 ++++++++------- .../test/kotlin/org/usvm/util/TSTestResolver.kt | 3 ++- 3 files changed, 11 insertions(+), 9 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt index 108b4ad54..24d39f5fc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt @@ -85,7 +85,7 @@ class TSExprResolver( fun resolveLValue(value: EtsValue): ULValue<*, *>? = when (value) { is EtsParameterRef, - is EtsLocal -> simpleValueResolver.resolveLocal(value) + is EtsLocal, -> simpleValueResolver.resolveLocal(value) else -> error("Unexpected value: $value") } 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 59a30b97c..45a10d918 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt @@ -89,6 +89,14 @@ open class TSMethodTestRunner : TestRunner Boolean + get() = { _, _ -> true } + override val typeTransformer: (Any?) -> EtsType get() = { // Both KClass and TSObject instances come here @@ -108,13 +116,6 @@ open class TSMethodTestRunner : TestRunner Boolean - get() = { _, _ -> true } - private fun getProject(fileName: String): EtsFile { val jsonWithoutExtension = "/ir/$fileName.json" val sampleFilePath = javaClass.getResourceAsStream(jsonWithoutExtension) 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 dae64ad01..bd473cc7c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt @@ -29,7 +29,8 @@ class TSTestResolver { val model = state.models.first() when (val methodResult = state.methodResult) { is TSMethodResult.Success -> { - val returnValue = resolveExpr(model.eval(methodResult.value), method.returnType) + val valueToResolve = model.eval(methodResult.value) + val returnValue = resolveExpr(valueToResolve, method.returnType) val params = method.parameters.mapIndexed { idx, param -> val lValue = URegisterStackLValue(typeToSort(param.type), idx) val expr = model.read(lValue) From b5d68e553dea91eae0a345bf4e8b5af469fb0cfd Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Wed, 7 Aug 2024 16:20:54 +0300 Subject: [PATCH 14/22] Implement property matchers --- .../test/kotlin/org/usvm/samples/Arguments.kt | 18 +++++-- .../kotlin/org/usvm/samples/StaticMethods.kt | 20 ++++++-- .../org/usvm/util/TSMethodTestRunner.kt | 51 +++++++++++++++++++ 3 files changed, 79 insertions(+), 10 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Arguments.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Arguments.kt index bd43346c6..7135f38f9 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Arguments.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Arguments.kt @@ -15,31 +15,39 @@ class Arguments : TSMethodTestRunner() { className = "SimpleClass", methodName = "noArguments", argumentsNumber = 0 - ) + ), + { r -> r?.number == 42.0 } ) } @Test fun testSingleArg() { - discoverProperties( + discoverProperties( methodIdentifier = MethodDescriptor( fileName = "Arguments.ts", className = "SimpleClass", methodName = "singleArgument", argumentsNumber = 1 - ) + ), + { a, r -> a == r } ) } @Test fun testManyArgs() { - discoverProperties( + discoverProperties( methodIdentifier = MethodDescriptor( fileName = "Arguments.ts", className = "SimpleClass", methodName = "manyArguments", argumentsNumber = 3 - ) + ), + { a, _, _, r -> a.number == 1.0 && r == a }, + { _, b, _, r -> b.number == 2.0 && r == b }, + { _, _, c, r -> c.number == 3.0 && r == c }, + { a, b, c, r -> + a.number != 1.0 && b.number != 2.0 && c.number != 3.0 && r?.number == 100.0 + }, ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/StaticMethods.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/StaticMethods.kt index afe7f3ac7..261b7ddc5 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/StaticMethods.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/StaticMethods.kt @@ -14,31 +14,41 @@ class StaticMethods : TSMethodTestRunner() { className = "StaticMethods", methodName = "noArguments", argumentsNumber = 0 - ) + ), + { r -> r?.number == 42.0 } ) } @Test fun testSingleArgStaticMethod() { - discoverProperties( + discoverProperties( methodIdentifier = MethodDescriptor( fileName = "StaticMethods.ts", className = "StaticMethods", methodName = "singleArgument", argumentsNumber = 1 - ) + ), + { a, r -> a.number == 1.0 && r?.number == 100.0 }, + { a, r -> a.number != 1.0 && r?.number == 0.0 }, ) } @Test fun testManyArgsStaticMethod() { - discoverProperties( + discoverProperties( methodIdentifier = MethodDescriptor( fileName = "StaticMethods.ts", className = "StaticMethods", methodName = "manyArguments", argumentsNumber = 4 - ) + ), + { a, _, _, _, r -> a.number == 1.0 && r == a }, + { _, b, _, _, r -> b.number == 2.0 && r == b }, + { _, _, c, _, r -> c.number == 3.0 && r == c }, + { _, _, _, d, r -> d.number == 4.0 && r == d }, + { a, b, c, d, r -> + a.number != 1.0 && b.number != 2.0 && c.number != 3.0 && d.number != 4.0 && r?.number == 100.0 + }, ) } } 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 45a10d918..4c853e5f4 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt @@ -89,6 +89,57 @@ open class TSMethodTestRunner : TestRunner + discoverProperties( + methodIdentifier: MethodDescriptor, + vararg analysisResultMatchers: (T1, T2, T3, R?) -> Boolean, + invariants: Array> = emptyArray(), + noinline coverageChecker: CoverageChecker = doNotCheckCoverage, + ) { + 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 = coverageChecker + ) + } + + protected inline fun + discoverProperties( + methodIdentifier: MethodDescriptor, + vararg analysisResultMatchers: (T1, T2, T3, T4, R?) -> Boolean, + invariants: Array> = emptyArray(), + noinline coverageChecker: CoverageChecker = doNotCheckCoverage, + ) { + 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 = coverageChecker + ) + } + /* For now type checks are disabled for development purposes From 3b831252f8ccad7cd3e13d9173816d81a0428bba Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Wed, 7 Aug 2024 16:25:07 +0300 Subject: [PATCH 15/22] Detekt fix --- .../src/main/kotlin/org/usvm/TSExprResolver.kt | 2 +- .../test/kotlin/org/usvm/util/TSTestResolver.kt | 17 +++++++++++++---- 2 files changed, 14 insertions(+), 5 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt index 24d39f5fc..108b4ad54 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt @@ -85,7 +85,7 @@ class TSExprResolver( fun resolveLValue(value: EtsValue): ULValue<*, *>? = when (value) { is EtsParameterRef, - is EtsLocal, -> simpleValueResolver.resolveLocal(value) + is EtsLocal -> simpleValueResolver.resolveLocal(value) else -> error("Unexpected value: $value") } 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 bd473cc7c..8800901e6 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt @@ -39,9 +39,11 @@ class TSTestResolver { return TSTest(params, returnValue) } + is TSMethodResult.TSException -> { TODO() } + is TSMethodResult.NoCall -> { TODO() } @@ -51,12 +53,12 @@ class TSTestResolver { } private fun resolveExpr(expr: UExpr, type: EtsType): TSObject = when (type) { - is EtsPrimitiveType -> resolvePrimitive(expr, type) - is EtsRefType -> TODO() - else -> TODO() + is EtsPrimitiveType -> resolvePrimitive(expr, type) + is EtsRefType -> TODO() + else -> TODO() } - private fun resolvePrimitive(expr: UExpr, type: EtsPrimitiveType): TSObject = when(type) { + private fun resolvePrimitive(expr: UExpr, type: EtsPrimitiveType): TSObject = when (type) { EtsNumberType -> { when (expr.sort) { expr.ctx.fp64Sort -> TSObject.TSNumber.Double(extractDouble(expr)) @@ -64,24 +66,31 @@ class TSTestResolver { else -> error("Unexpected sort: ${expr.sort}") } } + EtsBooleanType -> { TSObject.Boolean(extractBool(expr)) } + EtsUndefinedType -> { TSObject.UndefinedObject } + is EtsLiteralType -> { TODO() } + EtsNullType -> { TODO() } + EtsNeverType -> { TODO() } + EtsStringType -> { TODO() } + EtsVoidType -> { TODO() } From 0965ab88ce10b2c0bd94204fc95d5af4136de1cf Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Thu, 8 Aug 2024 04:48:37 +0300 Subject: [PATCH 16/22] Refactor comment --- .../src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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 4c853e5f4..49fd040e5 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt @@ -150,7 +150,12 @@ open class TSMethodTestRunner : TestRunner EtsType get() = { - // Both KClass and TSObject instances come here + /* + Both KClass and TSObject instances come here because + only KClass is available to match different objects. + However, this method is also used in parent TestRunner class + and passes here TSObject instances. So this check on current level is required. + */ val temp = if (it is KClass<*> || it == null) it else it::class when (temp) { From fd5cecb150d5aacceaeb4f0b50a62de93ac21a62 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 9 Aug 2024 11:41:21 +0300 Subject: [PATCH 17/22] TypeTransformer change with null --- usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 49fd040e5..890760ad8 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt @@ -150,13 +150,15 @@ open class TSMethodTestRunner : TestRunner EtsType get() = { + requireNotNull(it) { "Raw null value should not be passed here" } + /* Both KClass and TSObject instances come here because only KClass is available to match different objects. However, this method is also used in parent TestRunner class and passes here TSObject instances. So this check on current level is required. */ - val temp = if (it is KClass<*> || it == null) it else it::class + val temp = if (it is KClass<*>) it else it::class when (temp) { TSObject.AnyObject::class -> EtsAnyType From 00d83c1a536086737ecd54571aaf94ad70170d4b Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 9 Aug 2024 12:46:25 +0300 Subject: [PATCH 18/22] Auto conversion for tests --- .../org/usvm/util/TSMethodTestRunner.kt | 18 +- .../src/test/resources/ir/Arguments.ts.json | 849 ---------------- .../src/test/resources/ir/MinValue.ts.json | 636 ------------ .../test/resources/ir/StaticMethods.ts.json | 927 ------------------ 4 files changed, 15 insertions(+), 2415 deletions(-) delete mode 100644 usvm-ts/src/test/resources/ir/Arguments.ts.json delete mode 100644 usvm-ts/src/test/resources/ir/MinValue.ts.json delete mode 100644 usvm-ts/src/test/resources/ir/StaticMethods.ts.json 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 890760ad8..a1c8670d9 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt @@ -10,6 +10,7 @@ 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.jacodb.ets.utils.loadEtsFileAutoConvert import org.usvm.NoCoverage import org.usvm.PathSelectionStrategy import org.usvm.TSMachine @@ -19,6 +20,8 @@ import org.usvm.TSTest import org.usvm.UMachineOptions import org.usvm.test.util.TestRunner import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults +import java.nio.file.Paths +import kotlin.io.path.pathString import kotlin.reflect.KClass import kotlin.time.Duration import kotlin.time.Duration.Companion.milliseconds @@ -194,10 +197,19 @@ open class TSMethodTestRunner : TestRunner List get() = { id, options -> - val project = getProject(id.fileName) - val method = project.getMethodByDescriptor(id) + val packagePath = this.javaClass.`package`.name + .split(".") + .drop(3) // drop org.usvm.samples + .joinToString("/") - TSMachine(project, options).use { machine -> + val fileURL = javaClass.getResource("/samples/${packagePath}/${id.fileName}") + ?: error("No such file found") + val filePath = Paths.get(fileURL.toURI()) + val file = loadEtsFileAutoConvert(filePath.pathString) + + val method = file.getMethodByDescriptor(id) + + TSMachine(file, options).use { machine -> val states = machine.analyze(listOf(method)) states.map { state -> val resolver = TSTestResolver() diff --git a/usvm-ts/src/test/resources/ir/Arguments.ts.json b/usvm-ts/src/test/resources/ir/Arguments.ts.json deleted file mode 100644 index cba1c97b3..000000000 --- a/usvm-ts/src/test/resources/ir/Arguments.ts.json +++ /dev/null @@ -1,849 +0,0 @@ -{ - "name": "Arguments.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": { - "name": "SimpleClass" - }, - "modifiers": [], - "typeParameters": [], - "superClassName": "", - "implementedInterfaceNames": [], - "fields": [], - "methods": [ - { - "signature": { - "enclosingClass": { - "name": "SimpleClass" - }, - "name": "@instance_init", - "parameters": [], - "returnType": { - "_": "UnknownType" - } - }, - "modifiers": [], - "typeParameters": [], - "body": { - "locals": [], - "cfg": { - "blocks": [ - { - "id": 0, - "successors": [], - "predecessors": [], - "stmts": [ - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "this", - "type": { - "_": "UnknownType" - } - }, - "right": { - "_": "ThisRef", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - } - }, - { - "_": "ReturnVoidStmt" - } - ] - } - ] - } - } - }, - { - "signature": { - "enclosingClass": { - "name": "SimpleClass" - }, - "name": "@static_init", - "parameters": [], - "returnType": { - "_": "UnknownType" - } - }, - "modifiers": [], - "typeParameters": [], - "body": { - "locals": [], - "cfg": { - "blocks": [ - { - "id": 0, - "successors": [], - "predecessors": [], - "stmts": [ - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "this", - "type": { - "_": "UnknownType" - } - }, - "right": { - "_": "ThisRef", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - } - }, - { - "_": "ReturnVoidStmt" - } - ] - } - ] - } - } - }, - { - "signature": { - "enclosingClass": { - "name": "SimpleClass" - }, - "name": "noArguments", - "parameters": [], - "returnType": { - "_": "NumberType" - } - }, - "modifiers": [], - "typeParameters": [], - "body": { - "locals": [ - { - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - } - ], - "cfg": { - "blocks": [ - { - "id": 0, - "successors": [], - "predecessors": [], - "stmts": [ - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - }, - "right": { - "_": "ThisRef", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - } - }, - { - "_": "ReturnStmt", - "arg": { - "_": "Constant", - "value": "42", - "type": { - "_": "NumberType" - } - } - } - ] - } - ] - } - } - }, - { - "signature": { - "enclosingClass": { - "name": "SimpleClass" - }, - "name": "singleArgument", - "parameters": [ - { - "name": "a", - "type": { - "_": "NumberType" - }, - "isOptional": false - } - ], - "returnType": { - "_": "NumberType" - } - }, - "modifiers": [], - "typeParameters": [], - "body": { - "locals": [ - { - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - }, - { - "name": "a", - "type": { - "_": "NumberType" - } - } - ], - "cfg": { - "blocks": [ - { - "id": 0, - "successors": [], - "predecessors": [], - "stmts": [ - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "a", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "ParameterRef", - "index": 0, - "type": { - "_": "NumberType" - } - } - }, - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - }, - "right": { - "_": "ThisRef", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - } - }, - { - "_": "ReturnStmt", - "arg": { - "_": "Local", - "name": "a", - "type": { - "_": "NumberType" - } - } - } - ] - } - ] - } - } - }, - { - "signature": { - "enclosingClass": { - "name": "SimpleClass" - }, - "name": "manyArguments", - "parameters": [ - { - "name": "a", - "type": { - "_": "NumberType" - }, - "isOptional": false - }, - { - "name": "b", - "type": { - "_": "NumberType" - }, - "isOptional": false - }, - { - "name": "c", - "type": { - "_": "NumberType" - }, - "isOptional": false - } - ], - "returnType": { - "_": "NumberType" - } - }, - "modifiers": [], - "typeParameters": [], - "body": { - "locals": [ - { - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - }, - { - "name": "a", - "type": { - "_": "NumberType" - } - }, - { - "name": "b", - "type": { - "_": "NumberType" - } - }, - { - "name": "c", - "type": { - "_": "NumberType" - } - } - ], - "cfg": { - "blocks": [ - { - "id": 0, - "successors": [ - 1, - 6 - ], - "predecessors": [], - "stmts": [ - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "a", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "ParameterRef", - "index": 0, - "type": { - "_": "NumberType" - } - } - }, - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "b", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "ParameterRef", - "index": 1, - "type": { - "_": "NumberType" - } - } - }, - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "c", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "ParameterRef", - "index": 2, - "type": { - "_": "NumberType" - } - } - }, - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - }, - "right": { - "_": "ThisRef", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - } - }, - { - "_": "IfStmt", - "condition": { - "_": "ConditionExpr", - "op": "!=", - "left": { - "_": "Local", - "name": "a", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "Constant", - "value": "1", - "type": { - "_": "NumberType" - } - }, - "type": { - "_": "UnknownType" - } - } - } - ] - }, - { - "id": 1, - "successors": [ - 2, - 5 - ], - "predecessors": [ - 0, - 6 - ], - "stmts": [ - { - "_": "IfStmt", - "condition": { - "_": "ConditionExpr", - "op": "!=", - "left": { - "_": "Local", - "name": "b", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "Constant", - "value": "2", - "type": { - "_": "NumberType" - } - }, - "type": { - "_": "UnknownType" - } - } - } - ] - }, - { - "id": 2, - "successors": [ - 3, - 4 - ], - "predecessors": [ - 1, - 5 - ], - "stmts": [ - { - "_": "IfStmt", - "condition": { - "_": "ConditionExpr", - "op": "!=", - "left": { - "_": "Local", - "name": "c", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "Constant", - "value": "3", - "type": { - "_": "NumberType" - } - }, - "type": { - "_": "UnknownType" - } - } - } - ] - }, - { - "id": 3, - "successors": [], - "predecessors": [ - 2, - 4 - ], - "stmts": [ - { - "_": "ReturnStmt", - "arg": { - "_": "Constant", - "value": "100", - "type": { - "_": "NumberType" - } - } - } - ] - }, - { - "id": 4, - "successors": [ - 3 - ], - "predecessors": [ - 2 - ], - "stmts": [ - { - "_": "ReturnStmt", - "arg": { - "_": "Local", - "name": "c", - "type": { - "_": "NumberType" - } - } - } - ] - }, - { - "id": 5, - "successors": [ - 2 - ], - "predecessors": [ - 1 - ], - "stmts": [ - { - "_": "ReturnStmt", - "arg": { - "_": "Local", - "name": "b", - "type": { - "_": "NumberType" - } - } - } - ] - }, - { - "id": 6, - "successors": [ - 1 - ], - "predecessors": [ - 0 - ], - "stmts": [ - { - "_": "ReturnStmt", - "arg": { - "_": "Local", - "name": "a", - "type": { - "_": "NumberType" - } - } - } - ] - } - ] - } - } - }, - { - "signature": { - "enclosingClass": { - "name": "SimpleClass" - }, - "name": "thisArgument", - "parameters": [], - "returnType": { - "_": "UnclearReferenceType", - "name": "SimpleClass" - } - }, - "modifiers": [], - "typeParameters": [], - "body": { - "locals": [ - { - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - } - ], - "cfg": { - "blocks": [ - { - "id": 0, - "successors": [], - "predecessors": [], - "stmts": [ - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - }, - "right": { - "_": "ThisRef", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - } - }, - { - "_": "ReturnStmt", - "arg": { - "_": "Local", - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - } - } - ] - } - ] - } - } - }, - { - "signature": { - "enclosingClass": { - "name": "SimpleClass" - }, - "name": "constructor", - "parameters": [], - "returnType": { - "_": "UnknownType" - } - }, - "modifiers": [], - "typeParameters": [], - "body": { - "locals": [], - "cfg": { - "blocks": [ - { - "id": 0, - "successors": [], - "predecessors": [], - "stmts": [ - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "this", - "type": { - "_": "UnknownType" - } - }, - "right": { - "_": "ThisRef", - "type": { - "_": "ClassType", - "signature": { - "name": "SimpleClass" - } - } - } - }, - { - "_": "CallStmt", - "expr": { - "_": "InstanceCallExpr", - "instance": { - "_": "Local", - "name": "this", - "type": { - "_": "UnknownType" - } - }, - "method": { - "enclosingClass": { - "name": "SimpleClass" - }, - "name": "@instance_init", - "parameters": [], - "returnType": { - "_": "UnknownType" - } - }, - "args": [] - } - }, - { - "_": "ReturnVoidStmt" - } - ] - } - ] - } - } - } - ] - } - ], - "importInfos": [], - "exportInfos": [] -} diff --git a/usvm-ts/src/test/resources/ir/MinValue.ts.json b/usvm-ts/src/test/resources/ir/MinValue.ts.json deleted file mode 100644 index b15a43a93..000000000 --- a/usvm-ts/src/test/resources/ir/MinValue.ts.json +++ /dev/null @@ -1,636 +0,0 @@ -{ - "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/ir/StaticMethods.ts.json b/usvm-ts/src/test/resources/ir/StaticMethods.ts.json deleted file mode 100644 index df5a828f3..000000000 --- a/usvm-ts/src/test/resources/ir/StaticMethods.ts.json +++ /dev/null @@ -1,927 +0,0 @@ -{ - "name": "StaticMethods.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": { - "name": "StaticMethods" - }, - "modifiers": [], - "typeParameters": [], - "superClassName": "", - "implementedInterfaceNames": [], - "fields": [], - "methods": [ - { - "signature": { - "enclosingClass": { - "name": "StaticMethods" - }, - "name": "@instance_init", - "parameters": [], - "returnType": { - "_": "UnknownType" - } - }, - "modifiers": [], - "typeParameters": [], - "body": { - "locals": [], - "cfg": { - "blocks": [ - { - "id": 0, - "successors": [], - "predecessors": [], - "stmts": [ - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "this", - "type": { - "_": "UnknownType" - } - }, - "right": { - "_": "ThisRef", - "type": { - "_": "ClassType", - "signature": { - "name": "StaticMethods" - } - } - } - }, - { - "_": "ReturnVoidStmt" - } - ] - } - ] - } - } - }, - { - "signature": { - "enclosingClass": { - "name": "StaticMethods" - }, - "name": "@static_init", - "parameters": [], - "returnType": { - "_": "UnknownType" - } - }, - "modifiers": [], - "typeParameters": [], - "body": { - "locals": [], - "cfg": { - "blocks": [ - { - "id": 0, - "successors": [], - "predecessors": [], - "stmts": [ - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "this", - "type": { - "_": "UnknownType" - } - }, - "right": { - "_": "ThisRef", - "type": { - "_": "ClassType", - "signature": { - "name": "StaticMethods" - } - } - } - }, - { - "_": "ReturnVoidStmt" - } - ] - } - ] - } - } - }, - { - "signature": { - "enclosingClass": { - "name": "StaticMethods" - }, - "name": "constructor", - "parameters": [], - "returnType": { - "_": "UnknownType" - } - }, - "modifiers": [], - "typeParameters": [], - "body": { - "locals": [], - "cfg": { - "blocks": [ - { - "id": 0, - "successors": [], - "predecessors": [], - "stmts": [ - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "this", - "type": { - "_": "UnknownType" - } - }, - "right": { - "_": "ThisRef", - "type": { - "_": "ClassType", - "signature": { - "name": "StaticMethods" - } - } - } - }, - { - "_": "CallStmt", - "expr": { - "_": "InstanceCallExpr", - "instance": { - "_": "Local", - "name": "this", - "type": { - "_": "UnknownType" - } - }, - "method": { - "enclosingClass": { - "name": "StaticMethods" - }, - "name": "@instance_init", - "parameters": [], - "returnType": { - "_": "UnknownType" - } - }, - "args": [] - } - }, - { - "_": "ReturnVoidStmt" - } - ] - } - ] - } - } - }, - { - "signature": { - "enclosingClass": { - "name": "StaticMethods" - }, - "name": "noArguments", - "parameters": [], - "returnType": { - "_": "NumberType" - } - }, - "modifiers": [ - "StaticKeyword" - ], - "typeParameters": [], - "body": { - "locals": [ - { - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "StaticMethods" - } - } - } - ], - "cfg": { - "blocks": [ - { - "id": 0, - "successors": [], - "predecessors": [], - "stmts": [ - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "StaticMethods" - } - } - }, - "right": { - "_": "ThisRef", - "type": { - "_": "ClassType", - "signature": { - "name": "StaticMethods" - } - } - } - }, - { - "_": "ReturnStmt", - "arg": { - "_": "Constant", - "value": "42", - "type": { - "_": "NumberType" - } - } - } - ] - } - ] - } - } - }, - { - "signature": { - "enclosingClass": { - "name": "StaticMethods" - }, - "name": "singleArgument", - "parameters": [ - { - "name": "a", - "type": { - "_": "NumberType" - }, - "isOptional": false - } - ], - "returnType": { - "_": "NumberType" - } - }, - "modifiers": [ - "StaticKeyword" - ], - "typeParameters": [], - "body": { - "locals": [ - { - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "StaticMethods" - } - } - }, - { - "name": "a", - "type": { - "_": "NumberType" - } - } - ], - "cfg": { - "blocks": [ - { - "id": 0, - "successors": [ - 1, - 2 - ], - "predecessors": [], - "stmts": [ - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "a", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "ParameterRef", - "index": 0, - "type": { - "_": "NumberType" - } - } - }, - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "StaticMethods" - } - } - }, - "right": { - "_": "ThisRef", - "type": { - "_": "ClassType", - "signature": { - "name": "StaticMethods" - } - } - } - }, - { - "_": "IfStmt", - "condition": { - "_": "ConditionExpr", - "op": "!=", - "left": { - "_": "Local", - "name": "a", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "Constant", - "value": "1", - "type": { - "_": "NumberType" - } - }, - "type": { - "_": "UnknownType" - } - } - } - ] - }, - { - "id": 1, - "successors": [], - "predecessors": [ - 0, - 2 - ], - "stmts": [ - { - "_": "ReturnStmt", - "arg": { - "_": "Constant", - "value": "0", - "type": { - "_": "NumberType" - } - } - } - ] - }, - { - "id": 2, - "successors": [ - 1 - ], - "predecessors": [ - 0 - ], - "stmts": [ - { - "_": "ReturnStmt", - "arg": { - "_": "Constant", - "value": "100", - "type": { - "_": "NumberType" - } - } - } - ] - } - ] - } - } - }, - { - "signature": { - "enclosingClass": { - "name": "StaticMethods" - }, - "name": "manyArguments", - "parameters": [ - { - "name": "a", - "type": { - "_": "NumberType" - }, - "isOptional": false - }, - { - "name": "b", - "type": { - "_": "NumberType" - }, - "isOptional": false - }, - { - "name": "c", - "type": { - "_": "NumberType" - }, - "isOptional": false - }, - { - "name": "d", - "type": { - "_": "NumberType" - }, - "isOptional": false - } - ], - "returnType": { - "_": "NumberType" - } - }, - "modifiers": [ - "StaticKeyword" - ], - "typeParameters": [], - "body": { - "locals": [ - { - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "StaticMethods" - } - } - }, - { - "name": "a", - "type": { - "_": "NumberType" - } - }, - { - "name": "b", - "type": { - "_": "NumberType" - } - }, - { - "name": "c", - "type": { - "_": "NumberType" - } - }, - { - "name": "d", - "type": { - "_": "NumberType" - } - } - ], - "cfg": { - "blocks": [ - { - "id": 0, - "successors": [ - 1, - 8 - ], - "predecessors": [], - "stmts": [ - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "a", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "ParameterRef", - "index": 0, - "type": { - "_": "NumberType" - } - } - }, - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "b", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "ParameterRef", - "index": 1, - "type": { - "_": "NumberType" - } - } - }, - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "c", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "ParameterRef", - "index": 2, - "type": { - "_": "NumberType" - } - } - }, - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "d", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "ParameterRef", - "index": 3, - "type": { - "_": "NumberType" - } - } - }, - { - "_": "AssignStmt", - "left": { - "_": "Local", - "name": "this", - "type": { - "_": "ClassType", - "signature": { - "name": "StaticMethods" - } - } - }, - "right": { - "_": "ThisRef", - "type": { - "_": "ClassType", - "signature": { - "name": "StaticMethods" - } - } - } - }, - { - "_": "IfStmt", - "condition": { - "_": "ConditionExpr", - "op": "!=", - "left": { - "_": "Local", - "name": "a", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "Constant", - "value": "1", - "type": { - "_": "NumberType" - } - }, - "type": { - "_": "UnknownType" - } - } - } - ] - }, - { - "id": 1, - "successors": [ - 2, - 7 - ], - "predecessors": [ - 0, - 8 - ], - "stmts": [ - { - "_": "IfStmt", - "condition": { - "_": "ConditionExpr", - "op": "!=", - "left": { - "_": "Local", - "name": "b", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "Constant", - "value": "2", - "type": { - "_": "NumberType" - } - }, - "type": { - "_": "UnknownType" - } - } - } - ] - }, - { - "id": 2, - "successors": [ - 3, - 6 - ], - "predecessors": [ - 1, - 7 - ], - "stmts": [ - { - "_": "IfStmt", - "condition": { - "_": "ConditionExpr", - "op": "!=", - "left": { - "_": "Local", - "name": "c", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "Constant", - "value": "3", - "type": { - "_": "NumberType" - } - }, - "type": { - "_": "UnknownType" - } - } - } - ] - }, - { - "id": 3, - "successors": [ - 4, - 5 - ], - "predecessors": [ - 2, - 6 - ], - "stmts": [ - { - "_": "IfStmt", - "condition": { - "_": "ConditionExpr", - "op": "!=", - "left": { - "_": "Local", - "name": "d", - "type": { - "_": "NumberType" - } - }, - "right": { - "_": "Constant", - "value": "4", - "type": { - "_": "NumberType" - } - }, - "type": { - "_": "UnknownType" - } - } - } - ] - }, - { - "id": 4, - "successors": [], - "predecessors": [ - 3, - 5 - ], - "stmts": [ - { - "_": "ReturnStmt", - "arg": { - "_": "Constant", - "value": "100", - "type": { - "_": "NumberType" - } - } - } - ] - }, - { - "id": 5, - "successors": [ - 4 - ], - "predecessors": [ - 3 - ], - "stmts": [ - { - "_": "ReturnStmt", - "arg": { - "_": "Local", - "name": "d", - "type": { - "_": "NumberType" - } - } - } - ] - }, - { - "id": 6, - "successors": [ - 3 - ], - "predecessors": [ - 2 - ], - "stmts": [ - { - "_": "ReturnStmt", - "arg": { - "_": "Local", - "name": "c", - "type": { - "_": "NumberType" - } - } - } - ] - }, - { - "id": 7, - "successors": [ - 2 - ], - "predecessors": [ - 1 - ], - "stmts": [ - { - "_": "ReturnStmt", - "arg": { - "_": "Local", - "name": "b", - "type": { - "_": "NumberType" - } - } - } - ] - }, - { - "id": 8, - "successors": [ - 1 - ], - "predecessors": [ - 0 - ], - "stmts": [ - { - "_": "ReturnStmt", - "arg": { - "_": "Local", - "name": "a", - "type": { - "_": "NumberType" - } - } - } - ] - } - ] - } - } - } - ] - } - ], - "importInfos": [], - "exportInfos": [] -} From 7f404f118b5277c831c85dd927a044f663f2dfa7 Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Fri, 9 Aug 2024 16:58:49 +0300 Subject: [PATCH 19/22] Remove check --- usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt index 1344c9bae..6497def83 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt @@ -152,16 +152,11 @@ class TSInterpreter( private fun mapLocalToIdxMapper(method: EtsMethod, local: EtsValue) = when (local) { - is EtsLocal -> { -// // See https://github.com/UnitTestBot/usvm/issues/202 -// if (local.name == "this") 0 else - localVarToIdx - .getOrPut(method) { mutableMapOf() } - .run { - getOrPut(local.name) { method.parameters.size + size } - } - } - + is EtsLocal -> localVarToIdx + .getOrPut(method) { mutableMapOf() } + .run { + getOrPut(local.name) { method.parameters.size + size } + } is EtsThis -> 0 is EtsParameterRef -> local.index else -> error("Unexpected local: $local") From e88d50a8810fb2e4df803342a016e19280bcfee9 Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Fri, 9 Aug 2024 17:18:34 +0300 Subject: [PATCH 20/22] Update jacodb version --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 5ed9390ec..7df850fae 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -5,7 +5,7 @@ import org.gradle.plugin.use.PluginDependenciesSpec object Versions { const val detekt = "1.18.1" const val ini4j = "0.5.4" - const val jacodb = "4164b3cc64" + const val jacodb = "ae2716b3f8" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "1.9.20" From 9480e9c93ef274b10b0b4af3a830d7a2e115f2bc Mon Sep 17 00:00:00 2001 From: Sergey Loktev Date: Fri, 9 Aug 2024 17:29:33 +0300 Subject: [PATCH 21/22] Fix if branch index order --- usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt | 2 +- usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt index 6497def83..1770bdc84 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt @@ -81,7 +81,7 @@ class TSInterpreter( ?: return val succs = applicationGraph.successors(stmt).take(2).toList() - val (posStmt, negStmt) = succs[0] to succs[1] + val (posStmt, negStmt) = succs[1] to succs[0] scope.forkWithBlackList( boolExpr, 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 a1c8670d9..fa82d2177 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt @@ -21,7 +21,6 @@ import org.usvm.UMachineOptions import org.usvm.test.util.TestRunner import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults import java.nio.file.Paths -import kotlin.io.path.pathString import kotlin.reflect.KClass import kotlin.time.Duration import kotlin.time.Duration.Companion.milliseconds @@ -205,7 +204,7 @@ open class TSMethodTestRunner : TestRunner Date: Fri, 9 Aug 2024 17:43:11 +0300 Subject: [PATCH 22/22] Update CI --- .github/workflows/build-and-run-tests.yml | 32 +++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/.github/workflows/build-and-run-tests.yml b/.github/workflows/build-and-run-tests.yml index 4668424ff..1c1eae220 100644 --- a/.github/workflows/build-and-run-tests.yml +++ b/.github/workflows/build-and-run-tests.yml @@ -29,6 +29,38 @@ jobs: - name: Setup Gradle uses: gradle/gradle-build-action@v2 + - name: Set up Node + uses: actions/setup-node@v4 + with: + node-version: '22' + + - name: Set up ArkAnalyzer + run: | + REPO_URL="https://gitee.com/Lipenx/arkanalyzer.git" + DEST_DIR="arkanalyzer" + MAX_RETRIES=10 + RETRY_DELAY=3 # Delay between retries in seconds + BRANCH="neo/2024-08-07" + + for ((i=1; i<=MAX_RETRIES; i++)); do + git clone --depth=1 --branch $BRANCH $REPO_URL $DEST_DIR && break + echo "Clone failed, retrying in $RETRY_DELAY seconds..." + sleep "$RETRY_DELAY" + done + + if [[ $i -gt $MAX_RETRIES ]]; then + echo "Failed to clone the repository after $MAX_RETRIES attempts." + exit 1 + else + echo "Repository cloned successfully." + fi + + echo "ARKANALYZER_DIR=$(realpath $DEST_DIR)" >> $GITHUB_ENV + cd $DEST_DIR + + npm install + npm run build + - name: Install CPython optional dependencies run: | sudo apt-get update