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..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 @@ -125,5 +125,15 @@ 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 + // 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() + ) + ) } 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 8bca54d21f..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 @@ -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 @@ -160,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() -> { @@ -196,7 +209,13 @@ sealed interface TsBinaryOperator { ) // TODO: 'fake(ref)' == 'bool' - scope.assert(lhsType.refTypeExpr.not()) + // https://github.com/UnitTestBot/usvm/issues/281 + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.refTypeExpr, + // TODO mistake, we should coerce the ref object + // https://github.com/UnitTestBot/usvm/issues/281 + expr = mkFalse() + ) } fp64Sort -> { @@ -218,16 +237,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( @@ -269,7 +297,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 -> { @@ -292,15 +323,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( @@ -312,7 +352,9 @@ sealed interface TsBinaryOperator { ) } - else -> error("Unsupported sort ${rhs.sort}") + else -> { + error("Unsupported sort ${rhs.sort}") + } } } } @@ -488,47 +530,50 @@ 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) { + val loosyEqualityConstraint = with(Eq) { resolveFakeObject(lhs, rhs, scope) } + + return mkAnd(typeConstraint, loosyEqualityConstraint) } override fun TsContext.internalResolve( @@ -537,8 +582,7 @@ sealed interface TsBinaryOperator { scope: TsStepScope, ): UBoolExpr? { logger.warn { "Not implemented operator: StrictEq" } - scope.assert(falseExpr) - return null + error("Not implemented strict eq") } } @@ -599,7 +643,7 @@ sealed interface TsBinaryOperator { lhs: UBoolExpr, rhs: UBoolExpr, scope: TsStepScope, - ): UExpr<*> { + ): UExpr { return mkFpAddExpr( fpRoundingModeSortDefaultValue(), boolToFp(lhs), @@ -611,7 +655,7 @@ sealed interface TsBinaryOperator { lhs: UExpr, rhs: UExpr, scope: TsStepScope, - ): UExpr<*> { + ): UExpr { return mkFpAddExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) } @@ -619,50 +663,267 @@ 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 - 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/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 }, ) } 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..c56cc3bcd5 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Add.kt @@ -0,0 +1,96 @@ +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 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.toDouble() + 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 }, + ) + } + + @Test + fun `add unknown values`() { + val method = getMethod(className, "addUnknownValues") + 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 } + ) + } +} 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..c26d13e2f9 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 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..6c059657e2 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`() { 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..eb5d7ab22a 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`() { 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..2eea02218c 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 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/kotlin/org/usvm/util/Util.kt b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt new file mode 100644 index 0000000000..0bb0ca1e10 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt @@ -0,0 +1,3 @@ +package org.usvm.util + +fun Boolean.toDouble() = 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 new file mode 100644 index 0000000000..682dc22547 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/operators/Add.ts @@ -0,0 +1,71 @@ +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 + } + + 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 + + return 42 + } +} 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