From 63b1df0df2bd4ef00c4ee7a22c311aac522797c2 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 7 Feb 2025 14:46:54 +0300 Subject: [PATCH 1/4] Support simple calls --- .../org/usvm/machine/expr/TSExprResolver.kt | 308 ++++++++++++------ .../usvm/machine/interpreter/TSInterpreter.kt | 23 +- .../usvm/machine/operator/TSBinaryOperator.kt | 213 +++++++++--- .../org/usvm/machine/state/TSMethodResult.kt | 2 +- .../org/usvm/machine/state/TSStateUtils.kt | 2 +- .../src/test/kotlin/org/usvm/samples/Call.kt | 51 +++ usvm-ts/src/test/resources/samples/Call.ts | 17 + 7 files changed, 460 insertions(+), 156 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt create mode 100644 usvm-ts/src/test/resources/samples/Call.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt index 3e4f85687..9e2b3b451 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt @@ -68,6 +68,7 @@ import org.jacodb.ets.base.EtsValue import org.jacodb.ets.base.EtsVoidExpr import org.jacodb.ets.base.EtsYieldExpr import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsMethodSignature import org.usvm.UAddressSort import org.usvm.UBoolSort import org.usvm.UExpr @@ -78,6 +79,9 @@ import org.usvm.machine.TSContext import org.usvm.machine.interpreter.TSStepScope import org.usvm.machine.operator.TSBinaryOperator import org.usvm.machine.operator.TSUnaryOperator +import org.usvm.machine.state.TSMethodResult +import org.usvm.machine.state.localsCount +import org.usvm.machine.state.newStmt import org.usvm.machine.types.FakeType import org.usvm.machine.types.mkFakeValue import org.usvm.memory.ULValue @@ -109,7 +113,7 @@ class TSExprResolver( lhv: EtsEntity, rhv: EtsEntity, ): UExpr? = resolveAfterResolved(lhv, rhv) { lhs, rhs -> - operator.resolve(lhs, rhs, scope) + with(operator) { ctx.resolve(lhs, rhs, scope) } } private inline fun resolveAfterResolved( @@ -130,6 +134,8 @@ class TSExprResolver( return block(result0, result1) } + // region SIMPLE VALUE + override fun visit(value: EtsLocal): UExpr { return simpleValueResolver.visit(value) } @@ -142,6 +148,10 @@ class TSExprResolver( return simpleValueResolver.visit(value) } + // endregion + + // region CONSTANT + override fun visit(value: EtsBooleanConstant): UExpr { return simpleValueResolver.visit(value) } @@ -150,6 +160,11 @@ class TSExprResolver( return simpleValueResolver.visit(value) } + override fun visit(value: EtsStringConstant): UExpr? { + logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } + error("Not supported $value") + } + override fun visit(value: EtsNullConstant): UExpr { return simpleValueResolver.visit(value) } @@ -158,211 +173,184 @@ class TSExprResolver( return simpleValueResolver.visit(value) } - override fun visit(expr: EtsEqExpr): UExpr? { - return resolveBinaryOperator(TSBinaryOperator.Eq, expr) - } - - override fun visit(expr: EtsAddExpr): UExpr? { - return resolveBinaryOperator(TSBinaryOperator.Add, expr) - } - - override fun visit(expr: EtsAndExpr): UExpr? { - return resolveBinaryOperator(TSBinaryOperator.And, expr) - } + // endregion - override fun visit(expr: EtsOrExpr): UExpr? { - return resolveBinaryOperator(TSBinaryOperator.Or, expr) - } - - override fun visit(expr: EtsNotEqExpr): UExpr? { - return resolveBinaryOperator(TSBinaryOperator.Neq, expr) - } + // region UNARY override fun visit(expr: EtsNotExpr): UExpr? = with(ctx) { resolveAfterResolved(expr.arg) { arg -> if (arg.sort == boolSort) { arg.asExpr(boolSort).not() } else { - TSUnaryOperator.Not(arg, scope) + TSUnaryOperator.Not(arg, scope) } } } - override fun visit(value: EtsStringConstant): UExpr? { - logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } - error("Not supported $value") - } + // TODO move into TSUnaryOperator + override fun visit(expr: EtsNegExpr): UExpr? = with(ctx) { + if (expr.type is EtsNumberType) { + val arg = resolve(expr.arg)?.asExpr(fp64Sort) ?: return null + return mkFpNegationExpr(arg) + } - override fun visit(expr: EtsAwaitExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + if (expr.type is EtsUnknownType) { + TODO() + } + + error("Unsupported expr type ${expr.type} for negation") } - override fun visit(expr: EtsBitAndExpr): UExpr? { + override fun visit(expr: EtsUnaryPlusExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsBitNotExpr): UExpr? { + override fun visit(expr: EtsPostIncExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsBitOrExpr): UExpr? { + override fun visit(expr: EtsPostDecExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsBitXorExpr): UExpr? { + override fun visit(expr: EtsPreIncExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsCastExpr): UExpr? { + override fun visit(expr: EtsPreDecExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsCommaExpr): UExpr? { + override fun visit(expr: EtsBitNotExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsDeleteExpr): UExpr? { + override fun visit(expr: EtsCastExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsDivExpr): UExpr? { + override fun visit(expr: EtsTypeOfExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsExpExpr): UExpr? { + override fun visit(expr: EtsDeleteExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsGtEqExpr): UExpr? { + override fun visit(expr: EtsVoidExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsGtExpr): UExpr? { + override fun visit(expr: EtsAwaitExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsInExpr): UExpr? { + override fun visit(expr: EtsYieldExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsInstanceCallExpr): UExpr? { - // IMPORTANT do not forget to fill sorts of arguments map - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + // endregion + + // region BINARY + + override fun visit(expr: EtsAddExpr): UExpr? { + return resolveBinaryOperator(TSBinaryOperator.Add, expr) } - override fun visit(expr: EtsInstanceOfExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsSubExpr): UExpr? { + return resolveBinaryOperator(TSBinaryOperator.Sub, expr) } - override fun visit(expr: EtsLeftShiftExpr): UExpr? { + override fun visit(expr: EtsMulExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsLengthExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsAndExpr): UExpr? { + return resolveBinaryOperator(TSBinaryOperator.And, expr) } - override fun visit(expr: EtsLtEqExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsOrExpr): UExpr? { + return resolveBinaryOperator(TSBinaryOperator.Or, expr) } - override fun visit(expr: EtsLtExpr): UExpr? { + override fun visit(expr: EtsDivExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsMulExpr): UExpr? { + override fun visit(expr: EtsRemExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - // TODO move into TSUnaryOperator - override fun visit(expr: EtsNegExpr): UExpr? { - if (expr.type is EtsNumberType) { - val arg = resolve(expr.arg)?.asExpr(ctx.fp64Sort) ?: return null - return ctx.mkFpNegationExpr(arg) - } - - if (expr.type is EtsUnknownType) { - TODO() - } - - error("Unsupported expr type ${expr.type} for negation") - } - - override fun visit(expr: EtsNewArrayExpr): UExpr? { + override fun visit(expr: EtsExpExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsNewExpr): UExpr? { + override fun visit(expr: EtsBitAndExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsNullishCoalescingExpr): UExpr? { + override fun visit(expr: EtsBitOrExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsPostDecExpr): UExpr? { + override fun visit(expr: EtsBitXorExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsPostIncExpr): UExpr? { + override fun visit(expr: EtsLeftShiftExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsPreDecExpr): UExpr? { + override fun visit(expr: EtsRightShiftExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsPreIncExpr): UExpr? { + override fun visit(expr: EtsUnsignedRightShiftExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsRemExpr): UExpr? { + override fun visit(expr: EtsNullishCoalescingExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsRightShiftExpr): UExpr? { + override fun visit(expr: EtsCommaExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsStaticCallExpr): UExpr? { - // IMPORTANT do not forget to fill sorts of arguments map - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + // endregion + + // region RELATION + + override fun visit(expr: EtsEqExpr): UExpr? { + return resolveBinaryOperator(TSBinaryOperator.Eq, expr) } - override fun visit(expr: EtsPtrCallExpr): UExpr? { - // IMPORTANT do not forget to fill sorts of arguments map - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsNotEqExpr): UExpr? { + return resolveBinaryOperator(TSBinaryOperator.Neq, expr) } override fun visit(expr: EtsStrictEqExpr): UExpr? { @@ -375,41 +363,134 @@ class TSExprResolver( error("Not supported $expr") } - override fun visit(expr: EtsSubExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsLtExpr): UExpr? { + return resolveBinaryOperator(TSBinaryOperator.Lt, expr) } - override fun visit(expr: EtsTernaryExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsGtExpr): UExpr? { + return resolveBinaryOperator(TSBinaryOperator.Gt, expr) } - override fun visit(expr: EtsTypeOfExpr): UExpr? { + override fun visit(expr: EtsLtEqExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsUnaryPlusExpr): UExpr? { + override fun visit(expr: EtsGtEqExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsUnsignedRightShiftExpr): UExpr? { + override fun visit(expr: EtsInExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsVoidExpr): UExpr? { + override fun visit(expr: EtsInstanceOfExpr): UExpr? { logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } - override fun visit(expr: EtsYieldExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + // endregion + + // region CALL + + override fun visit(expr: EtsInstanceCallExpr): UExpr? { + // TODO: IMPORTANT do not forget to fill sorts of arguments map + return resolveInvoke( + method = expr.method, + instance = expr.instance, + arguments = { expr.args }, + argumentTypes = { expr.method.parameters.map { it.type } }, + ) { args -> + doWithState { + val method = ctx.scene + .projectAndSdkClasses + .flatMap { it.methods } + .singleOrNull { it.signature == expr.method } + ?: error("Couldn't find a unique method with the signature ${expr.method}") + callStack.push(method, currentStatement) + memory.stack.push(args.toTypedArray(), method.localsCount) + newStmt(method.cfg.stmts.first()) + } + } + } + + override fun visit(expr: EtsStaticCallExpr): UExpr? { + // TODO: IMPORTANT do not forget to fill sorts of arguments map + return resolveInvoke( + method = expr.method, + instance = null, + arguments = { expr.args }, + argumentTypes = { expr.method.parameters.map { it.type } }, + ) { args -> + TODO("Unsupported static methods") + } + } + + override fun visit(expr: EtsPtrCallExpr): UExpr? { + // TODO: IMPORTANT do not forget to fill sorts of arguments map + TODO("Not supported ${expr::class.simpleName}: $expr") + } + + private inline fun resolveInvoke( + method: EtsMethodSignature, + instance: EtsLocal?, + arguments: () -> List, + argumentTypes: () -> List, + onNoCallPresent: TSStepScope.(List>) -> Unit, + ): UExpr? { + val instanceExpr = if (instance != null) { + val resolved = resolve(instance) ?: return null + resolved.asExpr(ctx.addressSort) + } else { + null + } + + val args = mutableListOf>() + + for (arg in arguments()) { + val resolved = resolve(arg) ?: return null + args += resolved + } + + // Note: currently, 'this' has index 'n', so we must add it LAST, *after* all other arguments. + // See `TSInterpreter::mapLocalToIdx`. + if (instanceExpr != null) { + // TODO: checkNullPointer(instanceRef) ?: return null + // TODO: if (!assertIsSubtype(instanceRef, method.enclosingType)) return null + + args += instanceExpr + } + + return resolveInvokeNoStaticInitializationCheck { onNoCallPresent(args) } } + private inline fun resolveInvokeNoStaticInitializationCheck( + onNoCallPresent: TSStepScope.() -> Unit, + ): UExpr? { + val result = scope.calcOnState { methodResult } + return when (result) { + is TSMethodResult.NoCall -> { + scope.onNoCallPresent() + null + } + + is TSMethodResult.Success -> { + scope.doWithState { + methodResult = TSMethodResult.NoCall + } + result.value + } + + is TSMethodResult.TSException -> error("Exception should be handled earlier") + } + } + + // endregion + + // region ACCESS + override fun visit(value: EtsArrayAccess): UExpr? { logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } error("Not supported $value") @@ -424,9 +505,9 @@ class TSExprResolver( val expr = scope.calcOnState { memory.read(lValue) } if (assertIsSubtype(expr, value.type)) { - return expr + expr } else { - return null + null } } @@ -435,6 +516,31 @@ class TSExprResolver( error("Not supported $value") } + // endregion + + // region OTHER + + override fun visit(expr: EtsNewExpr): UExpr? = scope.calcOnState { + memory.allocConcrete(expr.type) + } + + override fun visit(expr: EtsNewArrayExpr): UExpr? { + logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } + error("Not supported $expr") + } + + override fun visit(expr: EtsLengthExpr): UExpr? { + logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } + error("Not supported $expr") + } + + override fun visit(expr: EtsTernaryExpr): UExpr? { + logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } + error("Not supported $expr") + } + + // endregion + // TODO incorrect implementation private fun assertIsSubtype(expr: UExpr, type: EtsType): Boolean { return true diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt index c380714d4..51bd4263c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt @@ -89,16 +89,12 @@ class TSInterpreter( private fun visitIfStmt(scope: TSStepScope, stmt: EtsIfStmt) { val exprResolver = exprResolverWithScope(scope) + val expr = exprResolver.resolve(stmt.condition) ?: return - val conditionExpr = exprResolver.resolve(stmt.condition) ?: run { - logger.warn { "Failed to resolve condition: $stmt" } - return - } - - val boolExpr = if (conditionExpr.sort == ctx.boolSort) { - conditionExpr.asExpr(ctx.boolSort) + val boolExpr = if (expr.sort == ctx.boolSort) { + expr.asExpr(ctx.boolSort) } else { - ctx.mkTruthyExpr(conditionExpr, scope) + ctx.mkTruthyExpr(expr, scope) } val (negStmt, posStmt) = applicationGraph.successors(stmt).take(2).toList() @@ -126,7 +122,6 @@ class TSInterpreter( private fun visitAssignStmt(scope: TSStepScope, stmt: EtsAssignStmt) { val exprResolver = exprResolverWithScope(scope) - val expr = exprResolver.resolve(stmt.rhv) ?: return check(expr.sort != ctx.unresolvedSort) { @@ -146,7 +141,15 @@ class TSInterpreter( } private fun visitCallStmt(scope: TSStepScope, stmt: EtsCallStmt) { - TODO() // IMPORTANT do not forget to fill sorts of arguments map + // IMPORTANT do not forget to fill sorts of arguments map + + val exprResolver = exprResolverWithScope(scope) + exprResolver.resolve(stmt.expr) ?: return + + scope.doWithState { + val nextStmt = stmt.nextStmt ?: return@doWithState + newStmt(nextStmt) + } } private fun visitThrowStmt(scope: TSStepScope, stmt: EtsThrowStmt) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt index 225eabf08..b2111d90a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt @@ -12,7 +12,6 @@ import org.usvm.api.typeStreamOf import org.usvm.machine.TSContext import org.usvm.machine.expr.TSUndefinedSort import org.usvm.machine.expr.mkTruthyExpr -import org.usvm.machine.expr.tctx import org.usvm.machine.interpreter.TSStepScope import org.usvm.machine.types.ExprWithTypeConstraint import org.usvm.machine.types.FakeType @@ -40,23 +39,23 @@ sealed interface TSBinaryOperator { scope: TSStepScope, ): UExpr - fun resolveFakeObject( + fun TSContext.resolveFakeObject( lhs: UExpr, rhs: UExpr, scope: TSStepScope, ): UExpr - fun internalResolve( + fun TSContext.internalResolve( lhs: UExpr, rhs: UExpr, scope: TSStepScope, ): UExpr - fun resolve( + fun TSContext.resolve( lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.sort.tctx) { + ): UExpr { if (lhs.isFakeObject() || rhs.isFakeObject()) { return resolveFakeObject(lhs, rhs, scope) } @@ -71,11 +70,10 @@ sealed interface TSBinaryOperator { } } - internalResolve(lhs, rhs, scope) + return internalResolve(lhs, rhs, scope) } data object Eq : TSBinaryOperator { - override fun TSContext.onBool( lhs: UExpr, rhs: UExpr, @@ -100,14 +98,14 @@ sealed interface TSBinaryOperator { return mkEq(lhs, rhs) } - override fun resolveFakeObject( + override fun TSContext.resolveFakeObject( lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.tctx) { + ): UExpr { check(lhs.isFakeObject() || rhs.isFakeObject()) - scope.calcOnState { + return scope.calcOnState { val conjuncts = mutableListOf>() val groundFalseBranch = makeSymbolicPrimitive(boolSort) @@ -165,6 +163,7 @@ sealed interface TSBinaryOperator { // TODO: support objects } + lhs.isFakeObject() -> { val lhsType = memory.typeStreamOf(lhs).single() as FakeType @@ -228,6 +227,7 @@ sealed interface TSBinaryOperator { } } } + rhs.isFakeObject() -> { val rhsType = memory.typeStreamOf(rhs).single() as FakeType @@ -298,11 +298,11 @@ sealed interface TSBinaryOperator { } } - override fun internalResolve( + override fun TSContext.internalResolve( lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.tctx) { + ): UExpr { check(!lhs.isFakeObject() && !rhs.isFakeObject()) // 1. If the operands have the same type, they are compared using `onFp`, `onBool`, etc. @@ -335,13 +335,12 @@ sealed interface TSBinaryOperator { } data object Neq : TSBinaryOperator { - override fun TSContext.onBool( lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.tctx) { - with(Eq) { + ): UExpr { + return with(Eq) { onBool(lhs, rhs, scope).asExpr(boolSort).not() } } @@ -350,8 +349,8 @@ sealed interface TSBinaryOperator { lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.tctx) { - with(Eq) { + ): UExpr { + return with(Eq) { onFp(lhs, rhs, scope).asExpr(boolSort).not() } } @@ -360,31 +359,34 @@ sealed interface TSBinaryOperator { lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.tctx) { - with(Eq) { + ): UExpr { + return with(Eq) { onRef(lhs, rhs, scope).asExpr(boolSort).not() } } - override fun resolveFakeObject( + override fun TSContext.resolveFakeObject( lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.tctx) { - Eq.resolveFakeObject(lhs, rhs, scope).asExpr(boolSort).not() + ): UExpr { + return with(Eq) { + resolveFakeObject(lhs, rhs, scope).asExpr(boolSort).not() + } } - override fun internalResolve( + override fun TSContext.internalResolve( lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.tctx) { - Eq.internalResolve(lhs, rhs, scope).asExpr(boolSort).not() + ): UExpr { + return with(Eq) { + internalResolve(lhs, rhs, scope).asExpr(boolSort).not() + } } } data object Add : TSBinaryOperator { - override fun TSContext.onBool( lhs: UExpr, rhs: UExpr, @@ -395,7 +397,6 @@ sealed interface TSBinaryOperator { boolToFp(lhs), boolToFp(rhs) ) - } override fun TSContext.onFp( @@ -414,20 +415,20 @@ sealed interface TSBinaryOperator { TODO("Not yet implemented") } - override fun resolveFakeObject( + override fun TSContext.resolveFakeObject( lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.tctx) { + ): UExpr { check(lhs.isFakeObject() || rhs.isFakeObject()) TODO("Not yet implemented") } - override fun internalResolve( + override fun TSContext.internalResolve( lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.tctx) { + ): UExpr { check(!lhs.isFakeObject() && !rhs.isFakeObject()) // TODO support string concatenation @@ -457,6 +458,48 @@ sealed interface TSBinaryOperator { } } + data object Sub : TSBinaryOperator { + override fun TSContext.onBool( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + return mkFpSubExpr(fpRoundingModeSortDefaultValue(), boolToFp(lhs), boolToFp(rhs)) + } + + override fun TSContext.onFp( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + return mkFpSubExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) + } + + override fun TSContext.onRef( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + TODO("Not yet implemented") + } + + override fun TSContext.resolveFakeObject( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + TODO("Not yet implemented") + } + + override fun TSContext.internalResolve( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + TODO("Not yet implemented") + } + } + data object And : TSBinaryOperator { override fun TSContext.onBool( lhs: UExpr, @@ -482,28 +525,28 @@ sealed interface TSBinaryOperator { return internalResolve(lhs, rhs, scope) } - override fun resolveFakeObject( + override fun TSContext.resolveFakeObject( lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.tctx) { + ): UExpr { check(lhs.isFakeObject() || rhs.isFakeObject()) - scope.calcOnState { + return scope.calcOnState { val lhsTruthyExpr = mkTruthyExpr(lhs, scope) iteWriteIntoFakeObject(scope, lhsTruthyExpr, rhs, lhs) } } - override fun internalResolve( + override fun TSContext.internalResolve( lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.tctx) { + ): UExpr { check(!lhs.isFakeObject() && !rhs.isFakeObject()) val lhsTruthyExpr = mkTruthyExpr(lhs, scope) - scope.calcOnState { + return scope.calcOnState { iteWriteIntoFakeObject(scope, lhsTruthyExpr, rhs, lhs) } } @@ -534,30 +577,114 @@ sealed interface TSBinaryOperator { return internalResolve(lhs, rhs, scope) } - override fun resolveFakeObject( + override fun TSContext.resolveFakeObject( lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.tctx) { + ): UExpr { check(lhs.isFakeObject() || rhs.isFakeObject()) - scope.calcOnState { + return scope.calcOnState { val lhsTruthyExpr = mkTruthyExpr(lhs, scope) iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs) } } - override fun internalResolve( + override fun TSContext.internalResolve( lhs: UExpr, rhs: UExpr, scope: TSStepScope, - ): UExpr = with(lhs.tctx) { + ): UExpr { check(!lhs.isFakeObject() && !rhs.isFakeObject()) val lhsTruthyExpr = mkTruthyExpr(lhs, scope) - scope.calcOnState { + return scope.calcOnState { iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs) } } } + + data object Lt : TSBinaryOperator { + override fun TSContext.onBool( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + return mkAnd(lhs.not(), rhs) + } + + override fun TSContext.onFp( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + return mkFpLessExpr(lhs.asExpr(fp64Sort), rhs.asExpr(fp64Sort)) + } + + override fun TSContext.onRef( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + TODO("Not yet implemented") + } + + override fun TSContext.resolveFakeObject( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + TODO("Not yet implemented") + } + + override fun TSContext.internalResolve( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + TODO("Not yet implemented") + } + } + + data object Gt : TSBinaryOperator { + override fun TSContext.onBool( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + return mkAnd(lhs, rhs.not()) + } + + override fun TSContext.onFp( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + return mkFpGreaterExpr(lhs.asExpr(fp64Sort), rhs.asExpr(fp64Sort)) + } + + override fun TSContext.onRef( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + TODO("Not yet implemented") + } + + override fun TSContext.resolveFakeObject( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + TODO("Not yet implemented") + } + + override fun TSContext.internalResolve( + lhs: UExpr, + rhs: UExpr, + scope: TSStepScope, + ): UExpr { + TODO("Not yet implemented") + } + } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSMethodResult.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSMethodResult.kt index 5b04c8230..069a27a24 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSMethodResult.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSMethodResult.kt @@ -9,7 +9,7 @@ import org.usvm.USort /** * Represents a result of a method invocation. */ -interface TSMethodResult { +sealed interface TSMethodResult { /** * No call was performed. */ diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSStateUtils.kt index b83422e07..77ee4c6f3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSStateUtils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSStateUtils.kt @@ -26,7 +26,7 @@ fun TSState.returnValue(valueToReturn: UExpr) { } inline val EtsMethod.parametersWithThisCount: Int - get() = /*if (isStatic) parameters.size else*/ parameters.size + 1 // TODO hack, fix after AA fix + get() = parameters.size + 1 inline val EtsMethod.localsCount: Int get() = locals.size diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt new file mode 100644 index 000000000..ac68bba62 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt @@ -0,0 +1,51 @@ +package org.usvm.samples + +import org.jacodb.ets.base.DEFAULT_ARK_CLASS_NAME +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.api.TSObject +import org.usvm.util.TSMethodTestRunner +import org.usvm.util.getResourcePath + +class Call : TSMethodTestRunner() { + + override val scene: EtsScene = run { + val name = "Call.ts" + val path = getResourcePath("/samples/$name") + val file = loadEtsFileAutoConvert(path) + EtsScene(listOf(file)) + } + + @Test + fun `test simpleCall`() { + val method = getMethod("Call", "simpleCall") + discoverProperties( + method = method, + { r -> r.number == 42.0 }, + ) + } + + @Test + fun `test fib`() { + val method = getMethod("Call", "fib") + discoverProperties( + method = method, + { n, r -> n.number < 0.0 && r.number == -1.0 }, + { n, r -> n.number > 10.0 && r.number == -2.0 }, + { n, r -> n.number == 0.0 && r.number == 1.0 }, + { n, r -> n.number == 1.0 && r.number == 1.0 }, + { n, r -> n.number > 0 && n.number != 1.0 && fib(n.number) == r.number }, + ) + } +} + +fun fib(n: Double): Double { + if (n < 0) return -1.0 + if (n > 10) return -2.0 + if (n == 0.0) return 1.0 + if (n == 1.0) return 1.0 + + return fib(n - 1.0) + fib(n - 2.0) +} diff --git a/usvm-ts/src/test/resources/samples/Call.ts b/usvm-ts/src/test/resources/samples/Call.ts new file mode 100644 index 000000000..7fcbb5b8c --- /dev/null +++ b/usvm-ts/src/test/resources/samples/Call.ts @@ -0,0 +1,17 @@ +class Call { + simpleCall(): number { + return this.f() + } + + f(): number { + return 42 + } + + fib(n: number): number { + if (n < 0) return -1 + if (n > 10) return -2 + if (n == 0) return 1 + if (n == 1) return 1 + return this.fib(n - 1) + this.fib(n - 2) + } +} From ec38b5232045eeeac24163e857008052c6c4c704 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 7 Feb 2025 14:46:54 +0300 Subject: [PATCH 2/4] Support simple calls --- .../main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt | 1 - 1 file changed, 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt index b2111d90a..b546bf202 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt @@ -104,7 +104,6 @@ sealed interface TSBinaryOperator { scope: TSStepScope, ): UExpr { check(lhs.isFakeObject() || rhs.isFakeObject()) - return scope.calcOnState { val conjuncts = mutableListOf>() val groundFalseBranch = makeSymbolicPrimitive(boolSort) From 6c922fba947bee166d42526b406f114bbdc36f5e Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 7 Feb 2025 16:27:12 +0300 Subject: [PATCH 3/4] Add pre-saved sort information into nested calls --- .../org/usvm/machine/expr/TSExprResolver.kt | 10 ++-- .../usvm/machine/interpreter/TSInterpreter.kt | 5 +- .../kotlin/org/usvm/machine/state/TSState.kt | 46 +++++++++++++++---- .../org/usvm/machine/state/TSStateUtils.kt | 1 + 4 files changed, 46 insertions(+), 16 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt index 9e2b3b451..3e157419e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt @@ -93,7 +93,7 @@ private val logger = KotlinLogging.logger {} class TSExprResolver( private val ctx: TSContext, private val scope: TSStepScope, - localToIdx: (EtsMethod, EtsValue) -> Int, + private val localToIdx: (EtsMethod, EtsValue) -> Int, ) : EtsEntity.Visitor?> { private val simpleValueResolver: TSSimpleValueResolver = @@ -409,21 +409,25 @@ class TSExprResolver( .flatMap { it.methods } .singleOrNull { it.signature == expr.method } ?: error("Couldn't find a unique method with the signature ${expr.method}") + + pushSortsForArguments(expr.instance, expr.args, localToIdx) + callStack.push(method, currentStatement) memory.stack.push(args.toTypedArray(), method.localsCount) + newStmt(method.cfg.stmts.first()) } } } override fun visit(expr: EtsStaticCallExpr): UExpr? { - // TODO: IMPORTANT do not forget to fill sorts of arguments map return resolveInvoke( method = expr.method, instance = null, arguments = { expr.args }, argumentTypes = { expr.method.parameters.map { it.type } }, ) { args -> + // TODO: IMPORTANT do not forget to fill sorts of arguments map TODO("Unsupported static methods") } } @@ -559,7 +563,7 @@ class TSSimpleValueResolver( val localIdx = localToIdx(currentMethod, local) val sort = scope.calcOnState { - getOrPutSortForLocal(currentMethod, localIdx, local.type) + getOrPutSortForLocal(localIdx, local.type) } // If we are not in the entrypoint, all correct values are already resolved and we can just return diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt index 51bd4263c..664feef15 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt @@ -130,7 +130,7 @@ class TSInterpreter( scope.doWithState { val idx = mapLocalToIdx(lastEnteredMethod, stmt.lhv) - saveSortForLocal(lastEnteredMethod, idx, expr.sort) + saveSortForLocal(idx, expr.sort) val lValue = URegisterStackLValue(expr.sort, idx) memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr) @@ -141,8 +141,6 @@ class TSInterpreter( } private fun visitCallStmt(scope: TSStepScope, stmt: EtsCallStmt) { - // IMPORTANT do not forget to fill sorts of arguments map - val exprResolver = exprResolverWithScope(scope) exprResolver.resolve(stmt.expr) ?: return @@ -153,6 +151,7 @@ class TSInterpreter( } private fun visitThrowStmt(scope: TSStepScope, stmt: EtsThrowStmt) { + // TODO do not forget to pop the sorts call stack in the state TODO() } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSState.kt index 94a39db10..d50a1cd2d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSState.kt @@ -1,7 +1,9 @@ package org.usvm.machine.state +import org.jacodb.ets.base.EtsLocal import org.jacodb.ets.base.EtsStmt import org.jacodb.ets.base.EtsType +import org.jacodb.ets.base.EtsValue import org.jacodb.ets.model.EtsMethod import org.usvm.PathNode import org.usvm.UCallStack @@ -30,7 +32,7 @@ class TSState( forkPoints: PathNode> = PathNode.root(), var methodResult: TSMethodResult = TSMethodResult.NoCall, targets: UTargetsSet = UTargetsSet.empty(), - private var localToSort: UPersistentHashMap> = persistentHashMapOf(), + private var localToSortStack: MutableList> = mutableListOf(persistentHashMapOf()), ) : UState( ctx, ownership, @@ -42,17 +44,41 @@ class TSState( forkPoints, targets ) { - fun getOrPutSortForLocal(method: EtsMethod, localIdx: Int, localType: EtsType): USort { - val (updatedMap, value) = localToSort.getOrPut(method, ownership) { persistentHashMapOf() } - val (updatedIndices, result) = value.getOrPut(localIdx, ownership) { ctx.typeToSort(localType) } - localToSort = updatedMap.put(method, updatedIndices, ownership) + fun getOrPutSortForLocal(localIdx: Int, localType: EtsType): USort { + val localToSort = localToSortStack.last() + val (updatedIndices, result) = localToSort.getOrPut(localIdx, ownership) { ctx.typeToSort(localType) } + localToSortStack[localToSortStack.lastIndex] = updatedIndices return result } - fun saveSortForLocal(method: EtsMethod, localIdx: Int, sort: USort) { - val (updatedMap, sorts) = localToSort.getOrPut(method, ownership) { persistentHashMapOf() } - val updatedSorts = sorts.put(localIdx, sort, ownership) - localToSort = updatedMap.put(method, updatedSorts, ownership) + fun saveSortForLocal(localIdx: Int, sort: USort) { + val localToSort = localToSortStack.last() + val updatedSorts = localToSort.put(localIdx, sort, ownership) + localToSortStack[localToSortStack.lastIndex] = updatedSorts + } + + fun pushLocalToSortStack() { + localToSortStack.add(persistentHashMapOf()) + } + + fun popLocalToSortStack() { + localToSortStack.removeLast() + } + + fun pushSortsForArguments(instance: EtsLocal?, args: List, localToIdx: (EtsMethod, EtsValue) -> Int) { + val argSorts = args.map { arg -> + val localIdx = localToIdx(lastEnteredMethod, arg) + getOrPutSortForLocal(localIdx, arg.type) + } + + val instanceIdx = instance?.let { localToIdx(lastEnteredMethod, it) } + val instanceSort = instanceIdx?.let { getOrPutSortForLocal(it, instance.type) } + + pushLocalToSortStack() + argSorts.forEachIndexed { index, sort -> + saveSortForLocal(index, sort) + } + instanceSort?.let { saveSortForLocal(args.size, it) } } override fun clone(newConstraints: UPathConstraints?): TSState { @@ -76,7 +102,7 @@ class TSState( forkPoints, methodResult, targets.clone(), - localToSort + localToSortStack.toMutableList(), ) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSStateUtils.kt index 77ee4c6f3..f986a05c5 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSStateUtils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TSStateUtils.kt @@ -16,6 +16,7 @@ fun TSState.returnValue(valueToReturn: UExpr) { val returnSite = callStack.pop() if (callStack.isNotEmpty()) { memory.stack.pop() + popLocalToSortStack() } methodResult = TSMethodResult.Success(returnFromMethod, valueToReturn) From 37e032a05a64edb1ce50912e1ec90422fbe2a139 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 7 Feb 2025 16:38:39 +0300 Subject: [PATCH 4/4] Remove implemented TODO --- usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt | 1 - 1 file changed, 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt index 3e157419e..9380bd384 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt @@ -396,7 +396,6 @@ class TSExprResolver( // region CALL override fun visit(expr: EtsInstanceCallExpr): UExpr? { - // TODO: IMPORTANT do not forget to fill sorts of arguments map return resolveInvoke( method = expr.method, instance = expr.instance,