From ce44a11382d3fede9b586441e01768967c69f5c6 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 16 May 2025 12:03:16 +0300 Subject: [PATCH 01/13] Move operators tests into a separate folder --- .../src/test/kotlin/org/usvm/samples/{ => operators}/And.kt | 6 +++--- .../kotlin/org/usvm/samples/{ => operators}/Equality.kt | 6 +++--- .../src/test/kotlin/org/usvm/samples/{ => operators}/Neg.kt | 6 +++--- .../src/test/kotlin/org/usvm/samples/{ => operators}/Or.kt | 6 +++--- usvm-ts/src/test/resources/samples/{ => operators}/And.ts | 0 .../src/test/resources/samples/{ => operators}/Equality.ts | 0 usvm-ts/src/test/resources/samples/{ => operators}/Neg.ts | 0 usvm-ts/src/test/resources/samples/{ => operators}/Or.ts | 0 8 files changed, 12 insertions(+), 12 deletions(-) rename usvm-ts/src/test/kotlin/org/usvm/samples/{ => operators}/And.kt (99%) rename usvm-ts/src/test/kotlin/org/usvm/samples/{ => operators}/Equality.kt (96%) rename usvm-ts/src/test/kotlin/org/usvm/samples/{ => operators}/Neg.kt (91%) rename usvm-ts/src/test/kotlin/org/usvm/samples/{ => operators}/Or.kt (97%) rename usvm-ts/src/test/resources/samples/{ => operators}/And.ts (100%) rename usvm-ts/src/test/resources/samples/{ => operators}/Equality.ts (100%) rename usvm-ts/src/test/resources/samples/{ => operators}/Neg.ts (100%) rename usvm-ts/src/test/resources/samples/{ => operators}/Or.ts (100%) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/And.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/And.kt similarity index 99% rename from usvm-ts/src/test/kotlin/org/usvm/samples/And.kt rename to usvm-ts/src/test/kotlin/org/usvm/samples/operators/And.kt index ea7cd442f9..da4cd04f10 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/And.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/And.kt @@ -1,4 +1,4 @@ -package org.usvm.samples +package org.usvm.samples.operators import org.jacodb.ets.dsl.and import org.jacodb.ets.dsl.const @@ -28,7 +28,7 @@ class And : TsMethodTestRunner() { private val className = this::class.simpleName!! - override val scene: EtsScene = loadSampleScene(className) + override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators") private val classSignature: EtsClassSignature = scene.projectFiles[0].classes.single { it.name != DEFAULT_ARK_CLASS_NAME }.signature @@ -362,4 +362,4 @@ class And : TsMethodTestRunner() { }, ) } -} +} \ No newline at end of file diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Equality.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt similarity index 96% rename from usvm-ts/src/test/kotlin/org/usvm/samples/Equality.kt rename to usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt index 9642946ed2..68aacc8da0 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Equality.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt @@ -1,4 +1,4 @@ -package org.usvm.samples +package org.usvm.samples.operators import org.jacodb.ets.model.EtsScene import org.junit.jupiter.api.Disabled @@ -10,7 +10,7 @@ class Equality : TsMethodTestRunner() { private val className = this::class.simpleName!! - override val scene: EtsScene = loadSampleScene(className) + override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators") @Test fun `test eqBoolWithBool`() { @@ -96,4 +96,4 @@ class Equality : TsMethodTestRunner() { ) ) } -} +} \ No newline at end of file diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Neg.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Neg.kt similarity index 91% rename from usvm-ts/src/test/kotlin/org/usvm/samples/Neg.kt rename to usvm-ts/src/test/kotlin/org/usvm/samples/operators/Neg.kt index 3bf8d05197..b13152a070 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Neg.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Neg.kt @@ -1,4 +1,4 @@ -package org.usvm.samples +package org.usvm.samples.operators import org.jacodb.ets.model.EtsScene import org.junit.jupiter.api.Test @@ -9,7 +9,7 @@ class Neg : TsMethodTestRunner() { private val className = this::class.simpleName!! - override val scene: EtsScene = loadSampleScene(className) + override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators") @Test fun `test negateNumber`() { @@ -44,4 +44,4 @@ class Neg : TsMethodTestRunner() { { r -> r.number.isNaN() }, ) } -} +} \ No newline at end of file diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Or.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Or.kt similarity index 97% rename from usvm-ts/src/test/kotlin/org/usvm/samples/Or.kt rename to usvm-ts/src/test/kotlin/org/usvm/samples/operators/Or.kt index 48cea8d804..0ed5d6eccb 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Or.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Or.kt @@ -1,4 +1,4 @@ -package org.usvm.samples +package org.usvm.samples.operators import org.jacodb.ets.dsl.const import org.jacodb.ets.dsl.eq @@ -26,7 +26,7 @@ class Or : TsMethodTestRunner() { private val className = this::class.simpleName!! - override val scene: EtsScene = loadSampleScene(className) + override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators") private val classSignature: EtsClassSignature = scene.projectFiles[0].classes.single { it.name != DEFAULT_ARK_CLASS_NAME }.signature @@ -140,4 +140,4 @@ class Or : TsMethodTestRunner() { ) ) } -} +} \ No newline at end of file diff --git a/usvm-ts/src/test/resources/samples/And.ts b/usvm-ts/src/test/resources/samples/operators/And.ts similarity index 100% rename from usvm-ts/src/test/resources/samples/And.ts rename to usvm-ts/src/test/resources/samples/operators/And.ts diff --git a/usvm-ts/src/test/resources/samples/Equality.ts b/usvm-ts/src/test/resources/samples/operators/Equality.ts similarity index 100% rename from usvm-ts/src/test/resources/samples/Equality.ts rename to usvm-ts/src/test/resources/samples/operators/Equality.ts diff --git a/usvm-ts/src/test/resources/samples/Neg.ts b/usvm-ts/src/test/resources/samples/operators/Neg.ts similarity index 100% rename from usvm-ts/src/test/resources/samples/Neg.ts rename to usvm-ts/src/test/resources/samples/operators/Neg.ts diff --git a/usvm-ts/src/test/resources/samples/Or.ts b/usvm-ts/src/test/resources/samples/operators/Or.ts similarity index 100% rename from usvm-ts/src/test/resources/samples/Or.ts rename to usvm-ts/src/test/resources/samples/operators/Or.ts From ba6d4a51733d17837f1a2ab610673c7da032806c Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 16 May 2025 13:17:08 +0300 Subject: [PATCH 02/13] Add support --- .../usvm/machine/operator/TsBinaryOperator.kt | 25 ++++-- .../kotlin/org/usvm/samples/operators/Add.kt | 77 +++++++++++++++++++ usvm-ts/src/test/kotlin/org/usvm/util/Util.kt | 3 + .../test/resources/samples/operators/Add.ts | 57 ++++++++++++++ 4 files changed, 154 insertions(+), 8 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/util/Util.kt create mode 100644 usvm-ts/src/test/resources/samples/operators/Add.ts 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 8bca54d21f..a63ff1aac9 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 @@ -4,6 +4,7 @@ import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr import io.ksmt.utils.cast import mu.KotlinLogging +import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UBoolSort import org.usvm.UExpr @@ -644,25 +645,33 @@ sealed interface TsBinaryOperator { // TODO support bigint - val fpValue = when { + return when { lhs.sort is UBoolSort && rhs.sort is KFp64Sort -> { mkFpAddExpr(fpRoundingModeSortDefaultValue(), boolToFp(lhs.cast()), rhs.cast()) } + lhs.sort is UBoolSort && rhs.sort is UAddressSort -> { + mkFpAddExpr(fpRoundingModeSortDefaultValue(), boolToFp(lhs.cast()), mkNumericExpr(rhs, scope)) + } + lhs.sort is KFp64Sort && rhs.sort is UBoolSort -> { mkFpAddExpr(fpRoundingModeSortDefaultValue(), lhs.cast(), boolToFp(rhs.cast())) } - else -> null - } + lhs.sort is KFp64Sort && rhs.sort is UAddressSort -> { + mkFpAddExpr(fpRoundingModeSortDefaultValue(), lhs.cast(), mkNumericExpr(rhs, scope)) + } - if (fpValue != null) { - return fpValue - } + lhs.sort is UAddressSort && rhs.sort is KFp64Sort -> { + mkFpAddExpr(fpRoundingModeSortDefaultValue(), mkNumericExpr(lhs, scope), rhs.cast()) + } - // TODO: support object to primitive + lhs.sort is UAddressSort && rhs.sort is UBoolSort -> { + mkFpAddExpr(fpRoundingModeSortDefaultValue(), mkNumericExpr(lhs, scope), boolToFp(rhs.cast())) + } - TODO() + else -> TODO("Unsupported combination ${lhs.sort} and ${rhs.sort}") + } } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt new file mode 100644 index 0000000000..3506a0378a --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt @@ -0,0 +1,77 @@ +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.toFp +import kotlin.test.Test + +class Add : TsMethodTestRunner() { + private val className = this::class.simpleName!! + + override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators") + + @Test + fun `bool + bool`() { + val method = getMethod(className, "addBoolAndBool") + discoverProperties( + method = method, + { a, b, r -> r.number == 1.0 && !a.value && !b.value }, + { a, b, r -> r.number == 2.0 && !a.value && b.value }, + { a, b, r -> r.number == 3.0 && a.value && !b.value }, + { a, b, r -> r.number == 4.0 && a.value && b.value }, + invariants = arrayOf( + { _, _, r -> r.number != -1.0 } + ) + ) + } + + @Test + fun `bool + number`() { + val method = getMethod(className, "addBoolAndNumber") + discoverProperties( + method = method, + { a, b, r -> r.number == 1.0 && a.value && b.number == -1.0 }, + { a, b, r -> r.number == 2.0 && !a.value && b.number == 0.0 }, + { a, b, r -> r.number == 3.0 && a.value && b.number == 5.0 }, + { _, b, r -> r.number.isNaN() && b.number.isNaN() }, + { a, b, r -> + val result = a.value.toFp() + b.number + r.number == 4.0 && result != 2.2 && !result.isNaN() + } + ) + } + + @Test + fun `number + number`() { + val method = getMethod(className, "addNumberAndNumber") + discoverProperties( + method = method, + { a, b, r -> a.number.isNaN() && r.number.isNaN() }, + { a, b, r -> !a.number.isNaN() && b.number.isNaN() && r.number.isNaN() }, + { a, b, r -> a.number + b.number == r.number }, + { a, b, r -> !a.number.isNaN() && !b.number.isNaN() && r.number == 0.0 }, + ) + } + + @Test + fun `number + undefined`() { + val method = getMethod(className, "addNumberAndUndefined") + discoverProperties( + method = method, + invariants = arrayOf( + { a, r -> r.number != -1.0 }, + ) + ) + } + + @Test + fun `number + null`() { + val method = getMethod(className, "addNumberAndNull") + discoverProperties( + method = method, + { a, r -> a.number.isNaN() && r.number.isNaN() }, + { a, r -> !a.number.isNaN() && r.number == a.number }, + ) + } +} \ No newline at end of file diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt new file mode 100644 index 0000000000..7382af1f30 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt @@ -0,0 +1,3 @@ +package org.usvm.util + +fun Boolean.toFp() = if (this) 1.0 else 0.0 \ No newline at end of file diff --git a/usvm-ts/src/test/resources/samples/operators/Add.ts b/usvm-ts/src/test/resources/samples/operators/Add.ts new file mode 100644 index 0000000000..f01e7a5713 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/operators/Add.ts @@ -0,0 +1,57 @@ +class Add { + addBoolAndBool(a: boolean, b: boolean): number { + res = a + b; + + if (res == 0 && (a || b)) return -1 // unreachable + if (res < 0 || res > 2) return -1 // unreachable + if (res == 1 && a && b) return -1 // unreachable + if (res == 2 && !(a && b)) return -1 // unreachable + + if (res == 0) return 1 // false false + if (res == 1 && !a) return 2 // false true + if (res == 1 && !b) return 3 // true false + if (res == 2) return 4 // true true + + return -1 // unreachable + } + + addBoolAndNumber(a: boolean, b: number): number { + res = a + b; + + if (res == 0 && a) return 1 // true -1 + if (res == 0 && !a) return 2 // false 0 + + if (res == 6 && a) return 3 + + if (b != b) return res // _ NaN + + return 4 + } + + addNumberAndNumber(a: number, b: number): number { + res = a + b; + + if (a != a) return res + if (b != b) return res + + if (res == 1.1) return res + + return 0 + } + + addNumberAndUndefined(a: number): number { + res = a + undefined; + + if (res == 0) return -1 // unreachable + + return res + } + + addNumberAndNull(a: number): number { + res = a + null; + + if (res != a) return res + + return res + } +} \ No newline at end of file From c21205952eccf6988aa29309f5c31b148a213259 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 16 May 2025 14:32:24 +0300 Subject: [PATCH 03/13] Fake objects support in addiction --- .../kotlin/org/usvm/machine/expr/ExprUtil.kt | 8 +- .../org/usvm/machine/expr/TsExpressions.kt | 2 +- .../usvm/machine/operator/TsBinaryOperator.kt | 222 +++++++++++++++++- .../kotlin/org/usvm/samples/operators/Add.kt | 8 + .../kotlin/org/usvm/util/TsTestResolver.kt | 4 +- .../test/resources/samples/operators/Add.ts | 14 ++ 6 files changed, 245 insertions(+), 13 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 afcaedf789..87b77d4190 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 @@ -125,5 +125,11 @@ fun TsContext.mkNumericExpr( // TODO: ToPrimitive, then ToNumber again // TODO: probably we need to implement Object (Ref/Fake) -> Number conversion here directly, without ToPrimitive - error("Unsupported sort: ${expr.sort}") + // TODO incorrect implementation, returns some number that is not equal to 0 and NaN + val result = makeSymbolicPrimitive(fp64Sort) + + pathConstraints += mkFpIsNaNExpr(result).not() + pathConstraints += mkFpEqualExpr(result, mkFp(0.0, fp64Sort)).not() + + return@calcOnState mkFp64(0.0) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt index cc9d109d4f..4c1424c37d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt @@ -49,7 +49,7 @@ class TsUnresolvedSort(ctx: TsContext) : USort(ctx) { } } -fun UExpr.extractBool(): Boolean = when (this) { +fun UExpr.toConcreteBoolValue(): Boolean = when (this) { ctx.trueExpr -> true ctx.falseExpr -> false else -> error("Cannot extract boolean from $this") 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 a63ff1aac9..b34d953b30 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 @@ -600,7 +600,7 @@ sealed interface TsBinaryOperator { lhs: UBoolExpr, rhs: UBoolExpr, scope: TsStepScope, - ): UExpr<*> { + ): UExpr { return mkFpAddExpr( fpRoundingModeSortDefaultValue(), boolToFp(lhs), @@ -612,7 +612,7 @@ sealed interface TsBinaryOperator { lhs: UExpr, rhs: UExpr, scope: TsStepScope, - ): UExpr<*> { + ): UExpr { return mkFpAddExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) } @@ -620,29 +620,233 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UExpr<*> { - TODO("Not yet implemented") + ): UExpr { + return mkFpAddExpr( + fpRoundingModeSortDefaultValue(), + mkNumericExpr(lhs, scope), + mkNumericExpr(rhs, scope) + ) } override fun TsContext.resolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UExpr { check(lhs.isFakeObject() || rhs.isFakeObject()) - TODO("Not yet implemented") + + val conjuncts = mutableListOf>() + + when { + lhs.isFakeObject() && rhs.isFakeObject() -> { + val lhsType = lhs.getFakeType(scope) + val rhsType = rhs.getFakeType(scope) + + // fake(bool) + fake(bool) + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.boolTypeExpr, rhsType.boolTypeExpr), + expr = onBool(lhs.extractBool(scope), rhs.extractBool(scope), scope) + ) + + // fake(bool) + fake(fp) + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.boolTypeExpr, rhsType.fpTypeExpr), + expr = internalResolve(lhs.extractBool(scope), rhs.extractFp(scope), scope) + ) + + // fake(bool) + fake(ref) + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.boolTypeExpr, rhsType.refTypeExpr), + expr = internalResolve(lhs.extractBool(scope), rhs.extractRef(scope), scope) + ) + + // fake(fp) + fake(bool) + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.fpTypeExpr, rhsType.boolTypeExpr), + expr = internalResolve(lhs.extractFp(scope), rhs.extractBool(scope), scope) + ) + + // fake(fp) + fake(fp) + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.fpTypeExpr, rhsType.fpTypeExpr), + expr = onFp(lhs.extractFp(scope), rhs.extractFp(scope), scope) + ) + + // fake(fp) + fake(ref) + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.fpTypeExpr, rhsType.refTypeExpr), + expr = internalResolve(lhs.extractFp(scope), rhs.extractRef(scope), scope) + ) + + // fake(ref) + fake(bool) + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.refTypeExpr, rhsType.boolTypeExpr), + expr = internalResolve(lhs.extractRef(scope), rhs.extractBool(scope), scope) + ) + + // fake(ref) + fake(fp) + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.refTypeExpr, rhsType.fpTypeExpr), + expr = internalResolve(lhs.extractRef(scope), rhs.extractFp(scope), scope) + ) + + // fake(ref) + fake(ref) + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.refTypeExpr, rhsType.refTypeExpr), + expr = onRef(lhs.extractRef(scope), rhs.extractRef(scope), scope) + ) + } + + lhs.isFakeObject() -> { + val lhsType = lhs.getFakeType(scope) + + when (rhs.sort) { + is UBoolSort -> { + // fake(bool) + bool + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.boolTypeExpr, + expr = onBool(lhs.extractBool(scope), rhs.asExpr(boolSort), scope) + ) + + // fake(fp) + bool + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.fpTypeExpr, + expr = internalResolve(lhs.extractFp(scope), rhs.asExpr(boolSort), scope) + ) + + // fake(ref) + bool + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.refTypeExpr, + expr = internalResolve(lhs.extractRef(scope), rhs.asExpr(boolSort), scope) + ) + } + + is KFp64Sort -> { + // fake(bool) + fp + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.boolTypeExpr, + expr = internalResolve(lhs.extractBool(scope), rhs.asExpr(fp64Sort), scope) + ) + + // fake(fp) + fp + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.fpTypeExpr, + expr = onFp(lhs.extractFp(scope), rhs.asExpr(fp64Sort), scope) + ) + + // fake(ref) + fp + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.refTypeExpr, + expr = internalResolve(lhs.extractRef(scope), rhs.asExpr(fp64Sort), scope) + ) + } + + is UAddressSort -> { + // fake(bool) + ref + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.boolTypeExpr, + expr = internalResolve(lhs.extractBool(scope), rhs.asExpr(addressSort), scope) + ) + + // fake(fp) + ref + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.fpTypeExpr, + expr = internalResolve(lhs.extractFp(scope), rhs.asExpr(addressSort), scope) + ) + + // fake(ref) + ref + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.refTypeExpr, + expr = onRef(lhs.extractRef(scope), rhs.asExpr(addressSort), scope) + ) + } + + else -> error("Unsupported sort ${rhs.sort}") + } + } + rhs.isFakeObject() -> { + val rhsType = rhs.getFakeType(scope) + + when (lhs.sort) { + is UBoolSort -> { + // bool + fake(bool) + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.boolTypeExpr, + expr = onBool(lhs.asExpr(boolSort), rhs.extractBool(scope), scope) + ) + + // bool + fake(fp) + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.fpTypeExpr, + expr = internalResolve(lhs.asExpr(boolSort), rhs.extractFp(scope), scope) + ) + + // bool + fake(ref) + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.refTypeExpr, + expr = internalResolve(lhs.asExpr(boolSort), rhs.extractRef(scope), scope) + ) + } + + is KFp64Sort -> { + // fp + fake(bool) + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.boolTypeExpr, + expr = internalResolve(lhs.asExpr(fp64Sort), rhs.extractBool(scope), scope) + ) + + // fp + fake(fp) + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.fpTypeExpr, + expr = onFp(lhs.asExpr(fp64Sort), rhs.extractFp(scope), scope) + ) + + // fp + fake(ref) + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.refTypeExpr, + expr = internalResolve(lhs.asExpr(fp64Sort), rhs.extractRef(scope), scope) + ) + } + + is UAddressSort -> { + // ref + fake(bool) + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.boolTypeExpr, + expr = internalResolve(lhs.asExpr(addressSort), rhs.extractBool(scope), scope) + ) + + // ref + fake(fp) + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.fpTypeExpr, + expr = internalResolve(lhs.asExpr(addressSort), rhs.extractFp(scope), scope) + ) + + // ref + fake(ref) + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.refTypeExpr, + expr = onRef(lhs.asExpr(addressSort), rhs.extractRef(scope), scope) + ) + } + + else -> error("Unsupported sort ${lhs.sort}") + } + } + } + + // if (a is Bool && b is Bool) ... else if (a is Bool && b is Fp) ... else ... + return conjuncts.foldRight(mkFp(0.0, fp64Sort).asExpr(fp64Sort)) { value, acc -> + mkIte(value.constraint, value.expr, acc) + } } override fun TsContext.internalResolve( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UExpr { check(!lhs.isFakeObject() && !rhs.isFakeObject()) // TODO support string concatenation - // TODO support undefined - // TODO support bigint return when { diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt index 3506a0378a..0eeee03ea8 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt @@ -74,4 +74,12 @@ class Add : TsMethodTestRunner() { { a, r -> !a.number.isNaN() && r.number == a.number }, ) } + + @Test + fun `add unknown values`() { + val method = getMethod(className, "addUnknownValues") + discoverProperties( + method = method, + ) + } } \ No newline at end of file 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 48b58be328..a1cc7f3cea 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -34,8 +34,8 @@ import org.usvm.api.typeStreamOf import org.usvm.isTrue import org.usvm.machine.TsContext import org.usvm.machine.expr.TsUnresolvedSort -import org.usvm.machine.expr.extractBool import org.usvm.machine.expr.extractDouble +import org.usvm.machine.expr.toConcreteBoolValue import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.memory.ULValue @@ -306,7 +306,7 @@ open class TsTestStateResolver( } } - EtsBooleanType -> TsTestValue.TsBoolean(evaluateInModel(expr).extractBool()) + EtsBooleanType -> TsTestValue.TsBoolean(evaluateInModel(expr).toConcreteBoolValue()) EtsUndefinedType -> TsTestValue.TsUndefined is EtsLiteralType -> TODO() EtsNullType -> TODO() diff --git a/usvm-ts/src/test/resources/samples/operators/Add.ts b/usvm-ts/src/test/resources/samples/operators/Add.ts index f01e7a5713..4653690237 100644 --- a/usvm-ts/src/test/resources/samples/operators/Add.ts +++ b/usvm-ts/src/test/resources/samples/operators/Add.ts @@ -54,4 +54,18 @@ class Add { return res } + + addUnknownValues(a, b) { + res = a + b; + + if (res != res) return res + + if (res == 7) return res + + if (a === null && b === null) return res + + if (a === undefined || b === undefined) return res + + return 42 + } } \ No newline at end of file From da96668644381cdb82bc31c78f6ba2701e033053 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 16 May 2025 14:37:25 +0300 Subject: [PATCH 04/13] fix --- usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 87b77d4190..6c86cf1713 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 @@ -131,5 +131,5 @@ fun TsContext.mkNumericExpr( pathConstraints += mkFpIsNaNExpr(result).not() pathConstraints += mkFpEqualExpr(result, mkFp(0.0, fp64Sort)).not() - return@calcOnState mkFp64(0.0) + return@calcOnState result } From 154e7dd9b072339b16c86d47a39d11c4bc69c66c Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 16 May 2025 14:42:59 +0300 Subject: [PATCH 05/13] Version with bug in the model --- usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt | 3 ++- .../main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt | 2 +- 2 files changed, 3 insertions(+), 2 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 6c86cf1713..99fef44905 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 @@ -2,6 +2,7 @@ package org.usvm.machine.expr import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr +import io.ksmt.utils.mkConst import org.usvm.UBoolExpr import org.usvm.UBoolSort import org.usvm.UExpr @@ -126,7 +127,7 @@ fun TsContext.mkNumericExpr( // TODO: probably we need to implement Object (Ref/Fake) -> Number conversion here directly, without ToPrimitive // TODO incorrect implementation, returns some number that is not equal to 0 and NaN - val result = makeSymbolicPrimitive(fp64Sort) + val result = fp64Sort.mkConst("${expr}_toNumber") pathConstraints += mkFpIsNaNExpr(result).not() pathConstraints += mkFpEqualExpr(result, mkFp(0.0, fp64Sort)).not() 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 b34d953b30..91ee210bdc 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 @@ -834,7 +834,7 @@ sealed interface TsBinaryOperator { } // if (a is Bool && b is Bool) ... else if (a is Bool && b is Fp) ... else ... - return conjuncts.foldRight(mkFp(0.0, fp64Sort).asExpr(fp64Sort)) { value, acc -> + return conjuncts.drop(2).take(1).foldRight(mkFp(0.0, fp64Sort).asExpr(fp64Sort)) { value, acc -> mkIte(value.constraint, value.expr, acc) } } From ef92eb988f7fcd4a577ae47fad990713dd88aefd Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 16 May 2025 14:47:44 +0300 Subject: [PATCH 06/13] Fix --- .../main/kotlin/org/usvm/machine/expr/ExprUtil.kt | 15 +++++++++------ .../org/usvm/machine/operator/TsBinaryOperator.kt | 2 +- 2 files changed, 10 insertions(+), 7 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 99fef44905..7f857ddbbd 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 @@ -2,7 +2,6 @@ package org.usvm.machine.expr import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr -import io.ksmt.utils.mkConst import org.usvm.UBoolExpr import org.usvm.UBoolSort import org.usvm.UExpr @@ -127,10 +126,14 @@ fun TsContext.mkNumericExpr( // TODO: probably we need to implement Object (Ref/Fake) -> Number conversion here directly, without ToPrimitive // TODO incorrect implementation, returns some number that is not equal to 0 and NaN - val result = fp64Sort.mkConst("${expr}_toNumber") - pathConstraints += mkFpIsNaNExpr(result).not() - pathConstraints += mkFpEqualExpr(result, mkFp(0.0, fp64Sort)).not() - - return@calcOnState result + return@calcOnState mkIte( + condition = mkEq(expr.asExpr(addressSort), mkTsNullValue()), + trueBranch = mkFp(0.0, fp64Sort), + falseBranch = mkIte( + mkEq(expr.asExpr(addressSort), mkUndefinedValue()), + mkFp64NaN(), + makeSymbolicPrimitive(fp64Sort) + ) + ) } 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 91ee210bdc..b34d953b30 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 @@ -834,7 +834,7 @@ sealed interface TsBinaryOperator { } // if (a is Bool && b is Bool) ... else if (a is Bool && b is Fp) ... else ... - return conjuncts.drop(2).take(1).foldRight(mkFp(0.0, fp64Sort).asExpr(fp64Sort)) { value, acc -> + return conjuncts.foldRight(mkFp(0.0, fp64Sort).asExpr(fp64Sort)) { value, acc -> mkIte(value.constraint, value.expr, acc) } } From b68a31f7714eb8b0cb9dbd16bb74234230541fb1 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 16 May 2025 16:28:10 +0300 Subject: [PATCH 07/13] Remove asserts from binary operators resolution --- .../kotlin/org/usvm/machine/expr/ExprUtil.kt | 2 +- .../usvm/machine/operator/TsBinaryOperator.kt | 82 +++++++++++++------ .../test/resources/samples/operators/Add.ts | 4 +- 3 files changed, 62 insertions(+), 26 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 7f857ddbbd..eccbadb02f 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 @@ -133,7 +133,7 @@ fun TsContext.mkNumericExpr( falseBranch = mkIte( mkEq(expr.asExpr(addressSort), mkUndefinedValue()), mkFp64NaN(), - makeSymbolicPrimitive(fp64Sort) + mkFp64NaN() // TODO we should not generalize it this way ) ) } 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 b34d953b30..d2bb2121a3 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 @@ -161,16 +161,28 @@ sealed interface TsBinaryOperator { ) // TODO: 'fake(ref)' == 'fake(bool)' - scope.assert(mkAnd(lhsType.refTypeExpr, rhsType.boolTypeExpr).not()) + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.refTypeExpr, rhsType.boolTypeExpr), + expr = mkFalse() // TODO mistake, we should coerce the ref object + ) // TODO: 'fake(ref)' == 'fake(fp)' - scope.assert(mkAnd(lhsType.refTypeExpr, rhsType.fpTypeExpr).not()) + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.refTypeExpr, rhsType.fpTypeExpr), + expr = mkFalse() // TODO mistake, we should coerce the ref object + ) // TODO: 'fake(bool)' == 'fake(ref)' - scope.assert(mkAnd(lhsType.boolTypeExpr, rhsType.refTypeExpr).not()) + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.boolTypeExpr, rhsType.refTypeExpr), + expr = mkFalse() // TODO mistake, we should coerce the ref object + ) // TODO: 'fake(fp)' == 'fake(ref)' - scope.assert(mkAnd(lhsType.fpTypeExpr, rhsType.refTypeExpr).not()) + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.fpTypeExpr, rhsType.refTypeExpr), + expr = mkFalse() // TODO mistake, we should coerce the ref object + ) } lhs.isFakeObject() -> { @@ -197,7 +209,10 @@ sealed interface TsBinaryOperator { ) // TODO: 'fake(ref)' == 'bool' - scope.assert(lhsType.refTypeExpr.not()) + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.refTypeExpr, + expr = mkFalse() // TODO mistake, we should coerce the ref object + ) } fp64Sort -> { @@ -219,16 +234,25 @@ sealed interface TsBinaryOperator { ) ) - // TODO: 'fake(ref)' == 'fp' - scope.assert(lhsType.refTypeExpr.not()) + // TODO fake(ref) == 'fp' + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.refTypeExpr, + expr = mkFalse() // TODO mistake, we should coerce the ref object + ) } addressSort -> { // TODO: 'fake(bool)' == 'ref' - scope.assert(lhsType.boolTypeExpr.not()) + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.boolTypeExpr, + expr = mkFalse() // TODO mistake, we should coerce the ref object + ) // TODO: 'fake(fp)' == 'ref' - scope.assert(lhsType.fpTypeExpr.not()) + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.fpTypeExpr, + expr = mkFalse() // TODO mistake, we should coerce the ref object + ) // 'fake(ref)' == 'ref' conjuncts += ExprWithTypeConstraint( @@ -270,7 +294,10 @@ sealed interface TsBinaryOperator { ) // TODO: 'bool' == 'fake(ref)' - scope.assert(rhsType.refTypeExpr.not()) + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.refTypeExpr, + expr = mkFalse() // TODO mistake, we should coerce the ref object + ) } fp64Sort -> { @@ -293,15 +320,24 @@ sealed interface TsBinaryOperator { ) // TODO: 'fp' == 'fake(ref)' - scope.assert(rhsType.refTypeExpr.not()) + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.refTypeExpr, + expr = mkFalse() // TODO mistake, we should coerce the ref object + ) } addressSort -> { // TODO: 'ref' == 'fake(bool)' - scope.assert(rhsType.boolTypeExpr.not()) + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.boolTypeExpr, + expr = mkFalse() // TODO mistake, we should coerce the ref object + ) // TODO: 'ref' == 'fake(fp)' - scope.assert(rhsType.fpTypeExpr.not()) + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.fpTypeExpr, + expr = mkFalse() // TODO mistake, we should coerce the ref object + ) // 'ref' == 'fake(ref)' conjuncts += ExprWithTypeConstraint( @@ -489,46 +525,47 @@ sealed interface TsBinaryOperator { ): UBoolExpr { check(lhs.isFakeObject() || rhs.isFakeObject()) - when { + val typeConstraint = when { lhs.isFakeObject() && rhs.isFakeObject() -> { val lhsType = lhs.getFakeType(scope) val rhsType = rhs.getFakeType(scope) - val condition = mkAnd( + mkAnd( lhsType.boolTypeExpr eq rhsType.boolTypeExpr, lhsType.fpTypeExpr eq rhsType.fpTypeExpr, // TODO support type equality lhsType.refTypeExpr eq rhsType.refTypeExpr ) - scope.assert(condition) } lhs.isFakeObject() -> { val lhsType = lhs.getFakeType(scope) - val condition = when (rhs.sort) { + when (rhs.sort) { boolSort -> lhsType.boolTypeExpr fp64Sort -> lhsType.fpTypeExpr // TODO support type equality addressSort -> lhsType.refTypeExpr else -> error("Unsupported sort ${rhs.sort}") } - scope.assert(condition) } rhs.isFakeObject() -> { val rhsType = rhs.getFakeType(scope) - val condition = when (lhs.sort) { + when (lhs.sort) { boolSort -> rhsType.boolTypeExpr fp64Sort -> rhsType.fpTypeExpr // TODO support type equality addressSort -> rhsType.refTypeExpr else -> error("Unsupported sort ${lhs.sort}") } - scope.assert(condition) } + else -> error("Should not be called") } return with(Eq) { - resolveFakeObject(lhs, rhs, scope) + mkAnd( + typeConstraint, + resolveFakeObject(lhs, rhs, scope) + ) } } @@ -538,8 +575,7 @@ sealed interface TsBinaryOperator { scope: TsStepScope, ): UBoolExpr? { logger.warn { "Not implemented operator: StrictEq" } - scope.assert(falseExpr) - return null + error("Not implemented strict eq") } } diff --git a/usvm-ts/src/test/resources/samples/operators/Add.ts b/usvm-ts/src/test/resources/samples/operators/Add.ts index 4653690237..3a2f7e567f 100644 --- a/usvm-ts/src/test/resources/samples/operators/Add.ts +++ b/usvm-ts/src/test/resources/samples/operators/Add.ts @@ -58,14 +58,14 @@ class Add { addUnknownValues(a, b) { res = a + b; + if (a === undefined || b === undefined) return res + if (res != res) return res if (res == 7) return res if (a === null && b === null) return res - if (a === undefined || b === undefined) return res - return 42 } } \ No newline at end of file From c0b2730cc99b0d5458e12998bb4f4f411d0edccb Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 16 May 2025 16:50:48 +0300 Subject: [PATCH 08/13] Add test --- .../test/kotlin/org/usvm/samples/operators/Add.kt | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt index 0eeee03ea8..4274d16ebc 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt @@ -78,8 +78,19 @@ class Add : TsMethodTestRunner() { @Test fun `add unknown values`() { val method = getMethod(className, "addUnknownValues") - discoverProperties( + discoverProperties( method = method, + { a, b, r -> a is TsTestValue.TsUndefined || b is TsTestValue.TsUndefined && r.number.isNaN() }, + { a, b, r -> + (a is TsTestValue.TsClass + || b is TsTestValue.TsClass + || (a as? TsTestValue.TsNumber)?.number?.isNaN() == true + || (b as? TsTestValue.TsNumber)?.number?.isNaN() == true) + && r.number.isNaN() + }, + { a, b, r -> r.number == 7.0 }, + { a, b, r -> a is TsTestValue.TsNull && b is TsTestValue.TsNull && r.number == 0.0 }, + { a, b, r -> r.number == 42.0 } ) } } \ No newline at end of file From 8bcb36927c17986645ceda60354073ca1db15f93 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Mon, 19 May 2025 15:17:48 +0300 Subject: [PATCH 09/13] Fix eof --- usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt | 2 +- usvm-ts/src/test/kotlin/org/usvm/samples/operators/And.kt | 2 +- usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt | 2 +- usvm-ts/src/test/kotlin/org/usvm/samples/operators/Neg.kt | 2 +- usvm-ts/src/test/kotlin/org/usvm/samples/operators/Or.kt | 2 +- usvm-ts/src/test/kotlin/org/usvm/util/Util.kt | 2 +- usvm-ts/src/test/resources/samples/operators/Add.ts | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt index 4274d16ebc..e2d34958ad 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt @@ -93,4 +93,4 @@ class Add : TsMethodTestRunner() { { a, b, r -> r.number == 42.0 } ) } -} \ No newline at end of file +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/And.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/And.kt index da4cd04f10..c26d13e2f9 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/And.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/And.kt @@ -362,4 +362,4 @@ class And : TsMethodTestRunner() { }, ) } -} \ No newline at end of file +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt index 68aacc8da0..6c059657e2 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt @@ -96,4 +96,4 @@ class Equality : TsMethodTestRunner() { ) ) } -} \ No newline at end of file +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Neg.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Neg.kt index b13152a070..eb5d7ab22a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Neg.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Neg.kt @@ -44,4 +44,4 @@ class Neg : TsMethodTestRunner() { { r -> r.number.isNaN() }, ) } -} \ No newline at end of file +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Or.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Or.kt index 0ed5d6eccb..2eea02218c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Or.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Or.kt @@ -140,4 +140,4 @@ class Or : TsMethodTestRunner() { ) ) } -} \ No newline at end of file +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt index 7382af1f30..6a6de775cd 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt @@ -1,3 +1,3 @@ package org.usvm.util -fun Boolean.toFp() = if (this) 1.0 else 0.0 \ No newline at end of file +fun Boolean.toFp() = if (this) 1.0 else 0.0 diff --git a/usvm-ts/src/test/resources/samples/operators/Add.ts b/usvm-ts/src/test/resources/samples/operators/Add.ts index 3a2f7e567f..682dc22547 100644 --- a/usvm-ts/src/test/resources/samples/operators/Add.ts +++ b/usvm-ts/src/test/resources/samples/operators/Add.ts @@ -68,4 +68,4 @@ class Add { return 42 } -} \ No newline at end of file +} From a0657155f450e391ac962ce3bb7e110ec807167e Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Mon, 19 May 2025 15:20:16 +0300 Subject: [PATCH 10/13] fix test --- usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt index ec4e1384a0..d5d8cd3c84 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt @@ -77,8 +77,8 @@ class FieldAccess : TsMethodTestRunner() { x.number == 1.1 && r.number == 14.0 }, { a, r -> - val x = a.properties["x"] as TsTestValue.TsNumber - x.number != 1.1 && r.number == 10.0 + val x = a.properties["x"] as? TsTestValue.TsNumber + x?.number != 1.1 && r.number == 10.0 }, ) } From db150d40b7d72d944d8c0dae0cd91de22ace9440 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 20 May 2025 15:13:39 +0300 Subject: [PATCH 11/13] Format --- .../usvm/machine/operator/TsBinaryOperator.kt | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 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 d2bb2121a3..17ab9f746f 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 @@ -349,7 +349,9 @@ sealed interface TsBinaryOperator { ) } - else -> error("Unsupported sort ${rhs.sort}") + else -> { + error("Unsupported sort ${rhs.sort}") + } } } } @@ -558,7 +560,10 @@ sealed interface TsBinaryOperator { else -> error("Unsupported sort ${lhs.sort}") } } - else -> error("Should not be called") + + else -> { + error("Should not be called") + } } return with(Eq) { @@ -797,9 +802,12 @@ sealed interface TsBinaryOperator { ) } - else -> error("Unsupported sort ${rhs.sort}") + else -> { + error("Unsupported sort ${rhs.sort}") + } } } + rhs.isFakeObject() -> { val rhsType = rhs.getFakeType(scope) @@ -864,7 +872,9 @@ sealed interface TsBinaryOperator { ) } - else -> error("Unsupported sort ${lhs.sort}") + else -> { + error("Unsupported sort ${lhs.sort}") + } } } } From 0f1165054daa653c5fcb72910b35d5a1f4768e1e Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Thu, 22 May 2025 11:41:23 +0300 Subject: [PATCH 12/13] Fix review requests --- .../main/kotlin/org/usvm/machine/expr/ExprUtil.kt | 4 ++-- .../org/usvm/machine/operator/TsBinaryOperator.kt | 14 ++++++++------ .../test/kotlin/org/usvm/samples/operators/Add.kt | 4 ++-- usvm-ts/src/test/kotlin/org/usvm/util/Util.kt | 2 +- 4 files changed, 13 insertions(+), 11 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 eccbadb02f..1b68ef3c1c 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 @@ -126,14 +126,14 @@ fun TsContext.mkNumericExpr( // TODO: probably we need to implement Object (Ref/Fake) -> Number conversion here directly, without ToPrimitive // TODO incorrect implementation, returns some number that is not equal to 0 and NaN - + // https://github.com/UnitTestBot/usvm/issues/280 return@calcOnState mkIte( condition = mkEq(expr.asExpr(addressSort), mkTsNullValue()), trueBranch = mkFp(0.0, fp64Sort), falseBranch = mkIte( mkEq(expr.asExpr(addressSort), mkUndefinedValue()), mkFp64NaN(), - mkFp64NaN() // TODO we should not generalize it this way + mkFp64NaN() ) ) } 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 17ab9f746f..67525a609c 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 @@ -209,9 +209,12 @@ sealed interface TsBinaryOperator { ) // TODO: 'fake(ref)' == 'bool' + // https://github.com/UnitTestBot/usvm/issues/281 conjuncts += ExprWithTypeConstraint( constraint = lhsType.refTypeExpr, - expr = mkFalse() // TODO mistake, we should coerce the ref object + // TODO mistake, we should coerce the ref object + // https://github.com/UnitTestBot/usvm/issues/281 + expr = mkFalse() ) } @@ -566,12 +569,11 @@ sealed interface TsBinaryOperator { } } - return with(Eq) { - mkAnd( - typeConstraint, - resolveFakeObject(lhs, rhs, scope) - ) + val loosyEqualityConstraint with(Eq) { + resolveFakeObject(lhs, rhs, scope) } + + return mkAnd(typeConstraint, loosyEqualityConstraint) } override fun TsContext.internalResolve( diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt index e2d34958ad..c56cc3bcd5 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt @@ -3,7 +3,7 @@ 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.toFp +import org.usvm.util.toDouble import kotlin.test.Test class Add : TsMethodTestRunner() { @@ -36,7 +36,7 @@ class Add : TsMethodTestRunner() { { a, b, r -> r.number == 3.0 && a.value && b.number == 5.0 }, { _, b, r -> r.number.isNaN() && b.number.isNaN() }, { a, b, r -> - val result = a.value.toFp() + b.number + val result = a.value.toDouble() + b.number r.number == 4.0 && result != 2.2 && !result.isNaN() } ) diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt index 6a6de775cd..0bb0ca1e10 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt @@ -1,3 +1,3 @@ package org.usvm.util -fun Boolean.toFp() = if (this) 1.0 else 0.0 +fun Boolean.toDouble() = if (this) 1.0 else 0.0 From b5ec5616365837b1dca63b174ba46f7d19a52235 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Thu, 22 May 2025 11:46:00 +0300 Subject: [PATCH 13/13] Fix compilation error --- .../main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt | 2 +- 1 file changed, 1 insertion(+), 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 67525a609c..a87528e847 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 @@ -569,7 +569,7 @@ sealed interface TsBinaryOperator { } } - val loosyEqualityConstraint with(Eq) { + val loosyEqualityConstraint = with(Eq) { resolveFakeObject(lhs, rhs, scope) }