From 15aab78e451e7133b6dc750f16a57d3cebd06df8 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 11 Jun 2025 13:11:18 +0300 Subject: [PATCH 1/7] Division operator --- .../kotlin/org/usvm/machine/expr/ExprUtil.kt | 14 ++++ .../org/usvm/machine/expr/TsExprResolver.kt | 3 +- .../usvm/machine/operator/TsBinaryOperator.kt | 51 ++++++++++++ .../org/usvm/samples/operators/Division.kt | 64 +++++++++++++++ .../resources/samples/operators/Division.ts | 79 +++++++++++++++++++ 5 files changed, 209 insertions(+), 2 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/operators/Division.kt create mode 100644 usvm-ts/src/test/resources/samples/operators/Division.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt index 74be6469e5..fcb078fb3b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt @@ -92,6 +92,20 @@ fun TsContext.mkNumericExpr( expr: UExpr, scope: TsStepScope, ): UExpr = scope.calcOnState { + if (expr.isFakeObject()) { + return@calcOnState scope.calcOnState { + val type = expr.getFakeType(scope) + mkIte( + condition = type.fpTypeExpr, + trueBranch = expr.extractFp(scope), + falseBranch = mkIte( + condition = type.boolTypeExpr, + trueBranch = mkNumericExpr(expr.extractBool(scope), scope), + falseBranch = mkNumericExpr(expr.extractRef(scope), scope) + ) + ) + } + } // 7.1.4 ToNumber ( argument ) // 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 6a87491ee9..aebe0a6d9b 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 @@ -328,8 +328,7 @@ class TsExprResolver( } override fun visit(expr: EtsDivExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + return resolveBinaryOperator(TsBinaryOperator.Div, expr) } override fun visit(expr: EtsRemExpr): UExpr? { 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 49da780f13..e7d5d248dc 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 @@ -1215,4 +1215,55 @@ sealed interface TsBinaryOperator { return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right) } } + + data object Div: TsBinaryOperator { + override fun TsContext.onBool( + lhs: UBoolExpr, + rhs: UBoolExpr, + scope: TsStepScope + ): UExpr<*>? { + val left = mkNumericExpr(lhs, scope) + val right = mkNumericExpr(rhs, scope) + return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right) + } + + override fun TsContext.onFp( + lhs: UExpr, + rhs: UExpr, + scope: TsStepScope + ): UExpr<*>? { + return mkFpDivExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) + } + + override fun TsContext.onRef( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope + ): UExpr<*>? { + val left = mkNumericExpr(lhs, scope) + val right = mkNumericExpr(rhs, scope) + return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right) + } + + override fun TsContext.resolveFakeObject( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope + ): UExpr<*>? { + val left = mkNumericExpr(lhs, scope) + val right = mkNumericExpr(rhs, scope) + return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right) + } + + override fun TsContext.internalResolve( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope + ): UExpr<*>? { + val left = mkNumericExpr(lhs, scope) + val right = mkNumericExpr(rhs, scope) + return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right) + } + + } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Division.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Division.kt new file mode 100644 index 0000000000..f8964c6831 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Division.kt @@ -0,0 +1,64 @@ +package org.usvm.samples.operators + +import org.jacodb.ets.model.EtsScene +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.toDouble +import kotlin.test.Test + +class Division : TsMethodTestRunner() { + private val className = this::class.simpleName!! + + override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators") + + @Test + fun testTwoNumbersDivision() { + val method = getMethod(className, "twoNumbersDivision") + discoverProperties( + method = method, + { a, b, r -> a.number / b.number == 4.0 && r.number == 4.0 }, + { a, b, r -> a.number / b.number == Double.POSITIVE_INFINITY && r.number == Double.POSITIVE_INFINITY }, + { a, b, r -> a.number / b.number == Double.NEGATIVE_INFINITY && r.number == Double.NEGATIVE_INFINITY }, + { a, b, r -> (a.number / b.number).isNaN() && r.number.isNaN() }, + { a, b, r -> a.number / b.number != 4.0 && r.number == a.number / b.number } + ) + } + + @Test + fun testBooleanDivision() { + val method = getMethod(className, "booleanDivision") + discoverProperties( + method = method, + { a, b, r -> a.value.toDouble() / b.value.toDouble() == 0.0 && r.number == 0.0 }, + { a, b, r -> + a.value.toDouble() / b.value.toDouble() != 0.0 && (r.number == (a.value.toDouble() / b.value.toDouble()) || r.number.isNaN()) + } + ) + } + + @Test + fun testMixedDivision() { + val method = getMethod(className, "mixedDivision") + discoverProperties( + method = method, + { a, b, r -> a.number / b.value.toDouble() == 4.0 && r.number == 4.0 }, + { a, b, r -> a.number / b.value.toDouble() == Double.POSITIVE_INFINITY && r.number == Double.POSITIVE_INFINITY }, + { a, b, r -> a.number / b.value.toDouble() == Double.NEGATIVE_INFINITY && r.number == Double.NEGATIVE_INFINITY }, + { a, b, r -> (a.number / b.value.toDouble()).isNaN() && r.number.isNaN() }, + { a, b, r -> a.number / b.value.toDouble() != 4.0 && r.number == a.number / b.value.toDouble() } + ) + } + + @Test + fun testUnknownDivision() { + val method = getMethod(className, "unknownDivision") + discoverProperties( + method = method, + { a, b, r -> (a is TsTestValue.TsUndefined || b is TsTestValue.TsUndefined) && r.number.isNaN() }, + { _, _, r -> r.number == 4.0 }, + { _, _, r -> r.number == Double.POSITIVE_INFINITY }, + { _, _, r -> r.number == Double.NEGATIVE_INFINITY }, + { _, _, r -> r.number.isNaN() }, + ) + } +} \ No newline at end of file diff --git a/usvm-ts/src/test/resources/samples/operators/Division.ts b/usvm-ts/src/test/resources/samples/operators/Division.ts new file mode 100644 index 0000000000..11e7a2b7ca --- /dev/null +++ b/usvm-ts/src/test/resources/samples/operators/Division.ts @@ -0,0 +1,79 @@ +class Division { + twoNumbersDivision(a: number, b: number): number { + res = a / b; + if (res == 4) { + return res + } + + if (res == Infinity) { + return res + } + + if (res == -Infinity) { + return res + } + + if (res != res) { + return res + } + + return res + } + + booleanDivision(a: boolean, b: boolean): number { + res = a / b; + + if (res == 0) { + return res + } + + return res + } + + mixedDivision(a: number, b: boolean): number { + res = a / b; + if (res == 4) { + return res + } + + if (res == Infinity) { + return res + } + + if (res == -Infinity) { + return res + } + + if (res != res) { + return res + } + + return res + } + + unknownDivision(a, b): number { + res = a / b; + + if (a === undefined || b === undefined) { + return res; + } + + if (res == 4) { + return res; + } + + if (res == Infinity) { + return res; + } + + if (res == -Infinity) { + return res; + } + + if (res != res) { + return res; + } + + return res; + } +} \ No newline at end of file From 5c7201bbf113a54c7de3b656f6d64b1556ec4fc9 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 11 Jun 2025 14:09:58 +0300 Subject: [PATCH 2/7] Remainder operator --- .../org/usvm/machine/expr/TsExprResolver.kt | 3 +- .../usvm/machine/operator/TsBinaryOperator.kt | 43 ++++++++++ .../org/usvm/samples/operators/Remainder.kt | 80 +++++++++++++++++++ .../org/usvm/util/TsMethodTestRunner.kt | 2 + .../resources/samples/operators/Remainder.ts | 72 +++++++++++++++++ 5 files changed, 198 insertions(+), 2 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/operators/Remainder.kt create mode 100644 usvm-ts/src/test/resources/samples/operators/Remainder.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 aebe0a6d9b..5e7309a003 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 @@ -332,8 +332,7 @@ class TsExprResolver( } override fun visit(expr: EtsRemExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + return resolveBinaryOperator(TsBinaryOperator.Rem, expr) } override fun visit(expr: EtsExpExpr): UExpr? { 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 e7d5d248dc..f31d71a7d8 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 @@ -1264,6 +1264,49 @@ sealed interface TsBinaryOperator { val right = mkNumericExpr(rhs, scope) return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right) } + } + + data object Rem : TsBinaryOperator { + override fun TsContext.onBool( + lhs: UBoolExpr, + rhs: UBoolExpr, + scope: TsStepScope + ): UExpr<*>? { + return internalResolve(lhs, rhs, scope) + } + + override fun TsContext.onFp( + lhs: UExpr, + rhs: UExpr, + scope: TsStepScope + ): UExpr<*>? { + return internalResolve(lhs, rhs, scope) + } + override fun TsContext.onRef( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope + ): UExpr<*>? { + return internalResolve(lhs, rhs, scope) + } + + override fun TsContext.resolveFakeObject( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope + ): UExpr<*>? { + return internalResolve(lhs, rhs, scope) + } + + override fun TsContext.internalResolve( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope + ): UExpr<*>? { + val lhsExpr = mkNumericExpr(lhs, scope) + val rhsExpr = mkNumericExpr(rhs, scope) + return mkFpRemExpr(lhsExpr, rhsExpr) + } } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Remainder.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Remainder.kt new file mode 100644 index 0000000000..682a798722 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Remainder.kt @@ -0,0 +1,80 @@ +package org.usvm.samples.operators + +import org.junit.jupiter.api.Disabled +import org.junit.jupiter.api.Test +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.toDouble + +class Remainder : TsMethodTestRunner() { + private val className = this::class.simpleName!! + + override val scene = loadSampleScene(className, folderPrefix = "operators") + + @Test + @Disabled("Never ends") + fun testTwoNumbersRemainder() { + val method = getMethod(className, "twoNumbersRemainder") + discoverProperties( + method = method, + { a, b, r -> + val res = a.number % b.number + res != res && (a.number.isNaN() || b.number.isNaN()) + }, + { a, b, r -> + val res = a.number % b.number + res != res && (a.number == Double.POSITIVE_INFINITY || a.number == Double.NEGATIVE_INFINITY) + }, + { a, b, r -> a.number == 0.0 && b.number == 0.0 && r.number.isNaN() }, + { a, b, r -> + b.number == 0.0 && a.number != 0.0 && r.number.isNaN() + }, + { a, b, r -> + (b.number == Double.POSITIVE_INFINITY || b.number == Double.NEGATIVE_INFINITY) && r.number == a.number + }, + { a, b, r -> a.number == 0.0 && r.number == a.number }, + { a, b, r -> a.number % b.number == 4.0 && r.number == 4.0 }, + { a, b, r -> + val res = a.number % b.number + !res.isNaN() && res != 4.0 && r.number == res + }, + ) + } + + @Test + fun testBooleanRemainder() { + val method = getMethod(className, "booleanRemainder") + discoverProperties( + method = method, + { a, b, r -> a.value.toDouble() % b.value.toDouble() == 0.0 && r.number == 0.0 }, + { a, b, r -> + a.value.toDouble() % b.value.toDouble() != 0.0 && (r.number == (a.value.toDouble() % b.value.toDouble()) || r.number.isNaN()) + } + ) + } + + @Test + @Disabled("Wrong result") + fun testMixedRemainder() { + val method = getMethod(className, "mixedRemainder") + discoverProperties( + method = method, + { a, b, r -> a.number % b.value.toDouble() == 4.0 && r.number == 4.0 }, + { a, b, r -> (a.number % b.value.toDouble()).isNaN() && r.number.isNaN() }, + { a, b, r -> a.number % b.value.toDouble() != 4.0 && r.number == a.number % b.value.toDouble() } + ) + } + + @Test + @Disabled("Never ends") + fun testUnknownRemainder() { + val method = getMethod(className, "unknownRemainder") + discoverProperties( + method = method, + { a, b, r -> (a is TsTestValue.TsUndefined || b is TsTestValue.TsUndefined) && r.number.isNaN() }, + { _, _, r -> r.number == 4.0 }, + { _, _, r -> r.number.isNaN() }, + { _, _, r -> !r.number.isNaN() && r.number != 4.0 } + ) + } +} \ No newline at end of file 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 889dae0586..afa6ffa8e9 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt @@ -18,6 +18,7 @@ import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.junit.jupiter.api.TestInstance import org.junit.jupiter.api.TestInstance.Lifecycle.PER_CLASS import org.usvm.PathSelectionStrategy +import org.usvm.SolverType import org.usvm.UMachineOptions import org.usvm.api.NoCoverage import org.usvm.api.TsMethodCoverage @@ -234,6 +235,7 @@ abstract class TsMethodTestRunner : TestRunner Date: Wed, 11 Jun 2025 14:36:03 +0300 Subject: [PATCH 3/7] Format --- .../main/kotlin/org/usvm/machine/TsContext.kt | 1 - .../usvm/machine/operator/TsBinaryOperator.kt | 22 +++++++++---------- .../org/usvm/machine/types/TsTypeSystem.kt | 2 +- .../main/kotlin/org/usvm/util/EtsHierarchy.kt | 3 +-- .../src/main/kotlin/org/usvm/util/Utils.kt | 4 ++-- 5 files changed, 15 insertions(+), 17 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 9986128a08..c66130541c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -52,7 +52,6 @@ class TsContext( val voidSort: TsVoidSort by lazy { TsVoidSort(this) } val voidValue: TsVoidValue by lazy { TsVoidValue(this) } - /** * In TS we treat undefined value as a null reference in other objects. * For real null represented in the language we create another reference. 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 f31d71a7d8..3ebc117dab 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 @@ -1216,11 +1216,11 @@ sealed interface TsBinaryOperator { } } - data object Div: TsBinaryOperator { + data object Div : TsBinaryOperator { override fun TsContext.onBool( lhs: UBoolExpr, rhs: UBoolExpr, - scope: TsStepScope + scope: TsStepScope, ): UExpr<*>? { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) @@ -1230,7 +1230,7 @@ sealed interface TsBinaryOperator { override fun TsContext.onFp( lhs: UExpr, rhs: UExpr, - scope: TsStepScope + scope: TsStepScope, ): UExpr<*>? { return mkFpDivExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) } @@ -1238,7 +1238,7 @@ sealed interface TsBinaryOperator { override fun TsContext.onRef( lhs: UHeapRef, rhs: UHeapRef, - scope: TsStepScope + scope: TsStepScope, ): UExpr<*>? { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) @@ -1248,7 +1248,7 @@ sealed interface TsBinaryOperator { override fun TsContext.resolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, - scope: TsStepScope + scope: TsStepScope, ): UExpr<*>? { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) @@ -1258,7 +1258,7 @@ sealed interface TsBinaryOperator { override fun TsContext.internalResolve( lhs: UExpr<*>, rhs: UExpr<*>, - scope: TsStepScope + scope: TsStepScope, ): UExpr<*>? { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) @@ -1270,7 +1270,7 @@ sealed interface TsBinaryOperator { override fun TsContext.onBool( lhs: UBoolExpr, rhs: UBoolExpr, - scope: TsStepScope + scope: TsStepScope, ): UExpr<*>? { return internalResolve(lhs, rhs, scope) } @@ -1278,7 +1278,7 @@ sealed interface TsBinaryOperator { override fun TsContext.onFp( lhs: UExpr, rhs: UExpr, - scope: TsStepScope + scope: TsStepScope, ): UExpr<*>? { return internalResolve(lhs, rhs, scope) } @@ -1286,7 +1286,7 @@ sealed interface TsBinaryOperator { override fun TsContext.onRef( lhs: UHeapRef, rhs: UHeapRef, - scope: TsStepScope + scope: TsStepScope, ): UExpr<*>? { return internalResolve(lhs, rhs, scope) } @@ -1294,7 +1294,7 @@ sealed interface TsBinaryOperator { override fun TsContext.resolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, - scope: TsStepScope + scope: TsStepScope, ): UExpr<*>? { return internalResolve(lhs, rhs, scope) } @@ -1302,7 +1302,7 @@ sealed interface TsBinaryOperator { override fun TsContext.internalResolve( lhs: UExpr<*>, rhs: UExpr<*>, - scope: TsStepScope + scope: TsStepScope, ): UExpr<*>? { val lhsExpr = mkNumericExpr(lhs, scope) val rhsExpr = mkNumericExpr(rhs, scope) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 2ce9755a22..ddb0bb9e6e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -328,4 +328,4 @@ fun EtsClassType.toAuxiliaryType(hierarchy: EtsHierarchy): EtsAuxiliaryType? { return EtsAuxiliaryType( properties = fieldsIntersection + methodsIntersection ) -} \ No newline at end of file +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index 54351714c1..359c64a003 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -108,7 +108,6 @@ class EtsHierarchy(private val scene: EtsScene) { return suitableClasses.values } - companion object { // TODO use real one val OBJECT_CLASS = EtsClassType( @@ -135,4 +134,4 @@ fun ClassName.removeTrashFromTheName(): ClassName { } else { nameWithoutGenerics().removePrefixWithDots() } -} \ No newline at end of file +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt index 9457282d05..6b4f1b2a6b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt @@ -41,7 +41,7 @@ fun EtsType.isResolved(): Boolean = this !is EtsUnclearRefType && (this as? EtsClassType)?.signature?.file != EtsFileSignature.UNKNOWN fun EtsType.getClassesForType( - scene: EtsScene + scene: EtsScene, ): List = if (isResolved()) { scene .projectAndSdkClasses @@ -72,4 +72,4 @@ fun UHeapRef.createFakeField(fieldName: String, scope: TsStepScope): UConcreteHe } return fakeObject -} \ No newline at end of file +} From 05b3d091bad439c506d584763b00c756ed48515e Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 11 Jun 2025 14:40:11 +0300 Subject: [PATCH 4/7] Use concrete return type `UExpr` --- .../usvm/machine/operator/TsBinaryOperator.kt | 30 +++++++++---------- 1 file changed, 15 insertions(+), 15 deletions(-) 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 3ebc117dab..958058275c 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 @@ -1169,7 +1169,7 @@ sealed interface TsBinaryOperator { lhs: UBoolExpr, rhs: UBoolExpr, scope: TsStepScope, - ): UExpr<*> { + ): UExpr { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right) @@ -1179,7 +1179,7 @@ sealed interface TsBinaryOperator { lhs: UExpr, rhs: UExpr, scope: TsStepScope, - ): UExpr<*> { + ): UExpr { return mkFpMulExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) } @@ -1187,7 +1187,7 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UExpr<*> { + ): UExpr { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right) @@ -1197,7 +1197,7 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UExpr { check(lhs.isFakeObject() || rhs.isFakeObject()) val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) @@ -1208,7 +1208,7 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UExpr { check(!lhs.isFakeObject() && !rhs.isFakeObject()) val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) @@ -1221,7 +1221,7 @@ sealed interface TsBinaryOperator { lhs: UBoolExpr, rhs: UBoolExpr, scope: TsStepScope, - ): UExpr<*>? { + ): UExpr { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right) @@ -1231,7 +1231,7 @@ sealed interface TsBinaryOperator { lhs: UExpr, rhs: UExpr, scope: TsStepScope, - ): UExpr<*>? { + ): UExpr { return mkFpDivExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) } @@ -1239,7 +1239,7 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UExpr<*>? { + ): UExpr { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right) @@ -1249,7 +1249,7 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*>? { + ): UExpr { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right) @@ -1259,7 +1259,7 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*>? { + ): UExpr { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right) @@ -1271,7 +1271,7 @@ sealed interface TsBinaryOperator { lhs: UBoolExpr, rhs: UBoolExpr, scope: TsStepScope, - ): UExpr<*>? { + ): UExpr { return internalResolve(lhs, rhs, scope) } @@ -1279,7 +1279,7 @@ sealed interface TsBinaryOperator { lhs: UExpr, rhs: UExpr, scope: TsStepScope, - ): UExpr<*>? { + ): UExpr { return internalResolve(lhs, rhs, scope) } @@ -1287,7 +1287,7 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UExpr<*>? { + ): UExpr { return internalResolve(lhs, rhs, scope) } @@ -1295,7 +1295,7 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*>? { + ): UExpr { return internalResolve(lhs, rhs, scope) } @@ -1303,7 +1303,7 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*>? { + ): UExpr { val lhsExpr = mkNumericExpr(lhs, scope) val rhsExpr = mkNumericExpr(rhs, scope) return mkFpRemExpr(lhsExpr, rhsExpr) From 9b3a07885cb682725f9e57994ced856268cf6810 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 18 Jun 2025 16:22:35 +0300 Subject: [PATCH 5/7] Remove unnecessary 'scope.calcOnState' --- .../kotlin/org/usvm/machine/expr/ExprUtil.kt | 32 +++++++++---------- 1 file changed, 15 insertions(+), 17 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt index fcb078fb3b..be073618a3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt @@ -91,20 +91,18 @@ fun TsContext.mkTruthyExpr( fun TsContext.mkNumericExpr( expr: UExpr, scope: TsStepScope, -): UExpr = scope.calcOnState { +): UExpr { if (expr.isFakeObject()) { - return@calcOnState scope.calcOnState { - val type = expr.getFakeType(scope) - mkIte( - condition = type.fpTypeExpr, - trueBranch = expr.extractFp(scope), - falseBranch = mkIte( - condition = type.boolTypeExpr, - trueBranch = mkNumericExpr(expr.extractBool(scope), scope), - falseBranch = mkNumericExpr(expr.extractRef(scope), scope) - ) + val type = expr.getFakeType(scope) + return mkIte( + condition = type.fpTypeExpr, + trueBranch = expr.extractFp(scope), + falseBranch = mkIte( + condition = type.boolTypeExpr, + trueBranch = mkNumericExpr(expr.extractBool(scope), scope), + falseBranch = mkNumericExpr(expr.extractRef(scope), scope) ) - } + ) } // 7.1.4 ToNumber ( argument ) @@ -121,19 +119,19 @@ fun TsContext.mkNumericExpr( // 10. Return ToNumber(primValue). if (expr.sort == fp64Sort) { - return@calcOnState expr.asExpr(fp64Sort) + return expr.asExpr(fp64Sort) } if (expr == mkUndefinedValue()) { - return@calcOnState mkFp64NaN() + return mkFp64NaN() } if (expr == mkTsNullValue()) { - return@calcOnState mkFp64(0.0) + return mkFp64(0.0) } if (expr.sort == boolSort) { - return@calcOnState boolToFp(expr.asExpr(boolSort)) + return boolToFp(expr.asExpr(boolSort)) } // TODO: ToPrimitive, then ToNumber again @@ -141,7 +139,7 @@ fun TsContext.mkNumericExpr( // TODO incorrect implementation, returns some number that is not equal to 0 and NaN // https://github.com/UnitTestBot/usvm/issues/280 - return@calcOnState mkIte( + return mkIte( condition = mkEq(expr.asExpr(addressSort), mkTsNullValue()), trueBranch = mkFp(0.0, fp64Sort), falseBranch = mkIte( From b6f2db814aa76e09cee6048b23371b28fed560b6 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 18 Jun 2025 16:26:17 +0300 Subject: [PATCH 6/7] Format --- .../org/usvm/samples/arrays/InputArrays.kt | 5 +- .../resources/samples/operators/Division.ts | 16 +++--- .../resources/samples/operators/Remainder.ts | 16 +++--- .../samples/types/StructuralEquality.ts | 56 +++++++++---------- .../resources/samples/types/TypeStream.ts | 12 ++-- 5 files changed, 53 insertions(+), 52 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt index e4a8efd566..14736f7b5b 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt @@ -119,11 +119,12 @@ class InputArrays : TsMethodTestRunner() { method = method, { x, r -> val value = x.values[0] - value is TsTestValue.TsNumber && value.number == 1.0 && r is TsTestValue.TsNull }, + value is TsTestValue.TsNumber && value.number == 1.0 && r is TsTestValue.TsNull + }, { x, r -> val value = x.values[0] value !is TsTestValue.TsNumber || value.number != 1.0 && r == value }, ) } -} \ No newline at end of file +} diff --git a/usvm-ts/src/test/resources/samples/operators/Division.ts b/usvm-ts/src/test/resources/samples/operators/Division.ts index 11e7a2b7ca..c63f0cb95a 100644 --- a/usvm-ts/src/test/resources/samples/operators/Division.ts +++ b/usvm-ts/src/test/resources/samples/operators/Division.ts @@ -20,15 +20,15 @@ class Division { return res } - booleanDivision(a: boolean, b: boolean): number { - res = a / b; + booleanDivision(a: boolean, b: boolean): number { + res = a / b; - if (res == 0) { - return res - } + if (res == 0) { + return res + } - return res - } + return res + } mixedDivision(a: number, b: boolean): number { res = a / b; @@ -76,4 +76,4 @@ class Division { return res; } -} \ No newline at end of file +} diff --git a/usvm-ts/src/test/resources/samples/operators/Remainder.ts b/usvm-ts/src/test/resources/samples/operators/Remainder.ts index 4f28fb88d0..8c1c350b3c 100644 --- a/usvm-ts/src/test/resources/samples/operators/Remainder.ts +++ b/usvm-ts/src/test/resources/samples/operators/Remainder.ts @@ -33,15 +33,15 @@ class Remainder { return res } - booleanRemainder(a: boolean, b: boolean): number { - res = a % b; + booleanRemainder(a: boolean, b: boolean): number { + res = a % b; - if (res == 0) { - return res - } + if (res == 0) { + return res + } - return res - } + return res + } mixedRemainder(a: number, b: boolean): number { res = a % b; @@ -69,4 +69,4 @@ class Remainder { return res; } -} \ No newline at end of file +} diff --git a/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts b/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts index 622f2f0482..8abf3182d3 100644 --- a/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts +++ b/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts @@ -1,49 +1,49 @@ class A { - x: number; + x: number; - constructor(x: number) { - this.x = x; - } + constructor(x: number) { + this.x = x; + } - foo (): number { - return 21; - } + foo(): number { + return 21; + } } class B { - x: number; + x: number; - constructor(x: number) { - this.x = x; - } + constructor(x: number) { + this.x = x; + } - foo (): number { - return this.x; - } + foo(): number { + return this.x; + } } class C { - x: A; + x: A; - constructor(x: A) { - this.x = x; - } + constructor(x: A) { + this.x = x; + } } class D { - x: B; + x: B; - constructor(x: B) { - this.x = x; - } + constructor(x: B) { + this.x = x; + } } class Example { - testFunction() : C { - const obj: A = new B(11); - const number = obj.foo(); + testFunction(): C { + const obj: A = new B(11); + const number = obj.foo(); - const aaa: C = new D(new A(number)); - return aaa - } + const aaa: C = new D(new A(number)); + return aaa + } } diff --git a/usvm-ts/src/test/resources/samples/types/TypeStream.ts b/usvm-ts/src/test/resources/samples/types/TypeStream.ts index 26d0de229a..ea2c6e5e6b 100644 --- a/usvm-ts/src/test/resources/samples/types/TypeStream.ts +++ b/usvm-ts/src/test/resources/samples/types/TypeStream.ts @@ -45,25 +45,25 @@ class TypeStream { } class Parent { + parentField: number = -10 + virtualMethod(): number { return 100; } - - parentField: number = -10 } class FirstChild extends Parent { + firstChildField: number = 10 + override virtualMethod(): number { return 200; } - - firstChildField: number = 10 } class SecondChild extends Parent { + secondChildField: number = 20 + override virtualMethod(): number { return 300; } - - secondChildField: number = 20 } From 81f7d7d6113d2ff1a1e0a7710f921cbfd30c671f Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 18 Jun 2025 16:33:24 +0300 Subject: [PATCH 7/7] Add missing 'let' and headers --- .../src/test/resources/samples/operators/Add.ts | 15 +++++++++------ .../test/resources/samples/operators/Division.ts | 13 +++++++++---- .../test/resources/samples/operators/Remainder.ts | 12 ++++++++---- .../resources/samples/types/StructuralEquality.ts | 3 +++ 4 files changed, 29 insertions(+), 14 deletions(-) diff --git a/usvm-ts/src/test/resources/samples/operators/Add.ts b/usvm-ts/src/test/resources/samples/operators/Add.ts index 682dc22547..50da6ca4f8 100644 --- a/usvm-ts/src/test/resources/samples/operators/Add.ts +++ b/usvm-ts/src/test/resources/samples/operators/Add.ts @@ -1,6 +1,9 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + class Add { addBoolAndBool(a: boolean, b: boolean): number { - res = a + b; + let res = a + b; if (res == 0 && (a || b)) return -1 // unreachable if (res < 0 || res > 2) return -1 // unreachable @@ -16,7 +19,7 @@ class Add { } addBoolAndNumber(a: boolean, b: number): number { - res = a + b; + let res = a + b; if (res == 0 && a) return 1 // true -1 if (res == 0 && !a) return 2 // false 0 @@ -29,7 +32,7 @@ class Add { } addNumberAndNumber(a: number, b: number): number { - res = a + b; + let res = a + b; if (a != a) return res if (b != b) return res @@ -40,7 +43,7 @@ class Add { } addNumberAndUndefined(a: number): number { - res = a + undefined; + let res = a + undefined; if (res == 0) return -1 // unreachable @@ -48,7 +51,7 @@ class Add { } addNumberAndNull(a: number): number { - res = a + null; + let res = a + null; if (res != a) return res @@ -56,7 +59,7 @@ class Add { } addUnknownValues(a, b) { - res = a + b; + let res = a + b; if (a === undefined || b === undefined) return res diff --git a/usvm-ts/src/test/resources/samples/operators/Division.ts b/usvm-ts/src/test/resources/samples/operators/Division.ts index c63f0cb95a..d31c459b78 100644 --- a/usvm-ts/src/test/resources/samples/operators/Division.ts +++ b/usvm-ts/src/test/resources/samples/operators/Division.ts @@ -1,6 +1,10 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + class Division { twoNumbersDivision(a: number, b: number): number { - res = a / b; + let res = a / b; + if (res == 4) { return res } @@ -21,7 +25,7 @@ class Division { } booleanDivision(a: boolean, b: boolean): number { - res = a / b; + let res = a / b; if (res == 0) { return res @@ -31,7 +35,8 @@ class Division { } mixedDivision(a: number, b: boolean): number { - res = a / b; + let res = a / b; + if (res == 4) { return res } @@ -52,7 +57,7 @@ class Division { } unknownDivision(a, b): number { - res = a / b; + let res = a / b; if (a === undefined || b === undefined) { return res; diff --git a/usvm-ts/src/test/resources/samples/operators/Remainder.ts b/usvm-ts/src/test/resources/samples/operators/Remainder.ts index 8c1c350b3c..2e1c6fea16 100644 --- a/usvm-ts/src/test/resources/samples/operators/Remainder.ts +++ b/usvm-ts/src/test/resources/samples/operators/Remainder.ts @@ -1,6 +1,9 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + class Remainder { twoNumbersRemainder(a: number, b: number): number { - res = a % b; + let res = a % b; if (a != a || b != b) { return res // NaN @@ -34,7 +37,7 @@ class Remainder { } booleanRemainder(a: boolean, b: boolean): number { - res = a % b; + let res = a % b; if (res == 0) { return res @@ -44,7 +47,8 @@ class Remainder { } mixedRemainder(a: number, b: boolean): number { - res = a % b; + let res = a % b; + if (res == 4) { return res } @@ -57,7 +61,7 @@ class Remainder { } unknownRemainder(a, b): number { - res = a % b; + let res = a % b; if (res == 4) { return res; diff --git a/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts b/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts index 8abf3182d3..724703393f 100644 --- a/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts +++ b/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts @@ -1,3 +1,6 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + class A { x: number;