diff --git a/.github/workflows/build-and-run-tests.yml b/.github/workflows/build-and-run-tests.yml index 4668424ffb..1c1eae220d 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 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 0000000000..8519dd8449 --- /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/TSComponents.kt b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt index 15671ef2c2..e83cb1e135 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt @@ -15,10 +15,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 UBv32SizeExprProvider(ctx) } override fun mkTypeSystem( diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt index 8e6660bdb4..fa5d8bbd1e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt @@ -1,5 +1,24 @@ 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 -class TSContext(components: TSComponents) : UContext(components) +class TSContext(components: TSComponents) : UContext(components) { + + val undefinedSort: TSUndefinedSort by lazy { TSUndefinedSort(this) } + + private val undefinedValue by lazy { TSUndefinedValue(this) } + + fun typeToSort(type: EtsType): USort = when (type) { + is EtsBooleanType -> boolSort + is EtsNumberType -> fp64Sort + is EtsRefType -> addressSort + else -> TODO("Support all JacoDB types") + } + + 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 new file mode 100644 index 0000000000..108b4ad546 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt @@ -0,0 +1,413 @@ +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.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.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.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 + +@Suppress("UNUSED_PARAMETER") +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? { + return expr.accept(this) + } + + fun resolveLValue(value: EtsValue): ULValue<*, *>? = + when (value) { + is EtsParameterRef, + is EtsLocal -> simpleValueResolver.resolveLocal(value) + 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 { + return simpleValueResolver.visit(value) + } + + override fun visit(value: EtsArrayLiteral): UExpr { + TODO("Not yet implemented") + } + + override fun visit(value: EtsBooleanConstant): UExpr { + return simpleValueResolver.visit(value) + } + + override fun visit(value: EtsNullConstant): UExpr { + return simpleValueResolver.visit(value) + } + + override fun visit(value: EtsNumberConstant): UExpr { + return simpleValueResolver.visit(value) + } + + 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: 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") + } + + override fun visit(expr: EtsCastExpr): UExpr { + 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") + } + + override fun visit(expr: EtsInstanceOfExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsLeftShiftExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsLengthExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsLtEqExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsLtExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsMulExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsNegExpr): 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: EtsNotEqExpr): UExpr? { + return resolveBinaryOperator(TSBinaryOperator.Neq, expr) + } + + override fun visit(expr: EtsNotExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsNullishCoalescingExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsOrExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsPostDecExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsPostIncExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsPreDecExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsPreIncExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsRemExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsRightShiftExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsStaticCallExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsStrictEqExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsStrictNotEqExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsSubExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsTernaryExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsTypeOfExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsUnaryPlusExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsUnsignedRightShiftExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(expr: EtsVoidExpr): UExpr { + TODO("Not yet implemented") + } + + override fun visit(value: EtsArrayAccess): UExpr { + TODO("Not yet implemented") + } + + override fun visit(value: EtsInstanceFieldRef): UExpr { + TODO("Not yet implemented") + } + + override fun visit(value: EtsParameterRef): UExpr { + return simpleValueResolver.visit(value) + } + + override fun visit(value: EtsStaticFieldRef): UExpr { + TODO("Not yet implemented") + } + + 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(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(value: EtsArrayAccess): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(value: EtsInstanceFieldRef): UExpr = with(ctx) { + TODO("Not yet implemented") + } + + override fun visit(value: EtsParameterRef): UExpr = with(ctx) { + val lValue = resolveLocal(value) + return scope.calcOnState { memory.read(lValue) } + } + + override fun visit(value: EtsStaticFieldRef): 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<*> { + 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 0000000000..9019a6ce94 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt @@ -0,0 +1,44 @@ +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 + +val KAst.tctx get() = ctx as TSContext + +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 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") + } +} + +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 d514bbb2ef..1770bdc844 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,13 @@ import org.usvm.solver.USatResult import org.usvm.state.TSMethodResult import org.usvm.state.TSState import org.usvm.state.lastStmt +import org.usvm.state.newStmt +import org.usvm.state.returnValue import org.usvm.targets.UTargetsSet +typealias TSStepScope = StepScope + +@Suppress("UNUSED_PARAMETER") class TSInterpreter( private val ctx: TSContext, private val applicationGraph: TSApplicationGraph, @@ -40,14 +57,112 @@ 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") } return scope.stepResult() } + private fun visitIfStmt(scope: TSStepScope, stmt: EtsIfStmt) { + 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[1] to succs[0] + + scope.forkWithBlackList( + boolExpr, + posStmt, + negStmt, + blockOnTrueState = { newStmt(posStmt) }, + blockOnFalseState = { newStmt(negStmt) } + ) + } + + 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) { + 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) { + 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, localName) -> idx + private val localVarToIdx = mutableMapOf>() + + private fun mapLocalToIdxMapper(method: EtsMethod, local: EtsValue) = + when (local) { + 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") + } + + 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/TSTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt index aa2ccfc21b..9402a88501 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSTypeSystem.kt @@ -10,27 +10,28 @@ class TSTypeSystem( override val typeOperationsTimeout: Duration, val project: EtsFile, ) : UTypeSystem { + override fun isSupertype(supertype: EtsType, type: EtsType): Boolean { - TODO("Not yet implemented") + TODO() } override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean { - TODO("Not yet implemented") + TODO() } override fun isFinal(type: EtsType): Boolean { - TODO("Not yet implemented") + TODO() } override fun isInstantiable(type: EtsType): Boolean { - TODO("Not yet implemented") + TODO() } override fun findSubtypes(type: EtsType): Sequence { - TODO("Not yet implemented") + TODO() } override fun topTypeStream(): UTypeStream { - TODO("Not yet implemented") + TODO() } } 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 47bf55378a..0000000000 --- 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/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/Utils.kt new file mode 100644 index 0000000000..3fe60ae3d4 --- /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/main/kotlin/org/usvm/state/TSStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/state/TSStateUtils.kt index 1d65cdb8c4..3fd15d3011 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,24 @@ package org.usvm.state +import org.jacodb.ets.base.EtsStmt +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) + } +} 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 a100e9def7..7135f38f98 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Arguments.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Arguments.kt @@ -8,14 +8,58 @@ import kotlin.test.Test class Arguments : TSMethodTestRunner() { @Test - @Disabled - fun testMinValue() { + fun testNoArgs() { discoverProperties( methodIdentifier = MethodDescriptor( fileName = "Arguments.ts", className = "SimpleClass", methodName = "noArguments", argumentsNumber = 0 + ), + { r -> r?.number == 42.0 } + ) + } + + @Test + fun testSingleArg() { + discoverProperties( + methodIdentifier = MethodDescriptor( + fileName = "Arguments.ts", + className = "SimpleClass", + methodName = "singleArgument", + argumentsNumber = 1 + ), + { a, r -> a == r } + ) + } + + @Test + fun testManyArgs() { + 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 + }, + ) + } + + @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 new file mode 100644 index 0000000000..261b7ddc5b --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/StaticMethods.kt @@ -0,0 +1,54 @@ +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 + ), + { r -> r?.number == 42.0 } + ) + } + + @Test + fun testSingleArgStaticMethod() { + 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( + 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 f439faeb0e..fa82d2177d 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,7 @@ 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.reflect.KClass import kotlin.time.Duration import kotlin.time.Duration.Companion.milliseconds @@ -89,11 +91,78 @@ 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 + + See https://github.com/UnitTestBot/usvm/issues/203 + */ + override val checkType: (EtsType?, EtsType?) -> Boolean + get() = { _, _ -> true } + override val typeTransformer: (Any?) -> EtsType get() = { - require(it is KClass<*>) { "Only TSObjects are allowed" } + 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 else it::class - when (it) { + when (temp) { TSObject.AnyObject::class -> EtsAnyType TSObject.Array::class -> TODO() TSObject.Boolean::class -> EtsBooleanType @@ -107,9 +176,6 @@ open class TSMethodTestRunner : TestRunner Boolean - get() = TODO("Not yet implemented") - private fun getProject(fileName: String): EtsFile { val jsonWithoutExtension = "/ir/$fileName.json" val sampleFilePath = javaClass.getResourceAsStream(jsonWithoutExtension) @@ -130,10 +196,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("/") + + val fileURL = javaClass.getResource("/samples/${packagePath}/${id.fileName}") + ?: error("No such file found") + val filePath = Paths.get(fileURL.toURI()) + val file = loadEtsFileAutoConvert(filePath) + + val method = file.getMethodByDescriptor(id) - TSMachine(project, options).use { machine -> + TSMachine(file, options).use { machine -> val states = machine.analyze(listOf(method)) states.map { state -> val resolver = TSTestResolver() 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 171ee8281d..8800901e66 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,100 @@ 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 -@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 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) + 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/MinValue.json b/usvm-ts/src/test/resources/ir/MinValue.json deleted file mode 100644 index b15a43a931..0000000000 --- a/usvm-ts/src/test/resources/ir/MinValue.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/samples/Arguments.ts b/usvm-ts/src/test/resources/samples/Arguments.ts index 8f0488e3e6..b39ac7a10a 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 new file mode 100644 index 0000000000..4e9f5b2066 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/StaticMethods.ts @@ -0,0 +1,21 @@ +class StaticMethods { + static noArguments(): number { + return 42 + } + + static singleArgument(a: number): number { + if (a == 1) { + return 100 + } + return 0 + } + + 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 + } +}