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 76ecce7aab..77e559a869 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 @@ -10,6 +10,7 @@ import org.usvm.UBoolSort import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.UIteExpr +import org.usvm.USort import org.usvm.machine.TsContext import org.usvm.machine.expr.mkNumericExpr import org.usvm.machine.expr.mkTruthyExpr @@ -97,294 +98,307 @@ sealed interface TsBinaryOperator { return internalResolve(lhsValue, rhsValue, scope) } - data object Eq : TsBinaryOperator { - override fun TsContext.onBool( - lhs: UBoolExpr, - rhs: UBoolExpr, - scope: TsStepScope, - ): UBoolExpr { - return mkEq(lhs, rhs) - } + fun TsContext.commonResolveFakeObject( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope, + resultSort: R, + reduce: (List>) -> UExpr, + ): UExpr? { + check(lhs.isFakeObject() || rhs.isFakeObject()) - override fun TsContext.onFp( - lhs: UExpr, - rhs: UExpr, - scope: TsStepScope, - ): UBoolExpr { - return mkFpEqualExpr(lhs, rhs) - } + val conjuncts = mutableListOf>() - override fun TsContext.onRef( - lhs: UHeapRef, - rhs: UHeapRef, - scope: TsStepScope, - ): UBoolExpr { - return mkEq(lhs, rhs) - } + when { + lhs.isFakeObject() && rhs.isFakeObject() -> { + val lhsType = lhs.getFakeType(scope) + val rhsType = rhs.getFakeType(scope) - override fun TsContext.resolveFakeObject( - lhs: UExpr<*>, - rhs: UExpr<*>, - scope: TsStepScope, - ): UBoolExpr { - check(lhs.isFakeObject() || rhs.isFakeObject()) + val lhsBool = lhs.extractBool(scope) + val rhsBool = rhs.extractBool(scope) - val conjuncts = mutableListOf>() + val lhsFp = lhs.extractFp(scope) + val rhsFp = rhs.extractFp(scope) - when { - lhs.isFakeObject() && rhs.isFakeObject() -> { - val lhsType = lhs.getFakeType(scope) - val rhsType = rhs.getFakeType(scope) + val lhsRef = lhs.extractRef(scope) + val rhsRef = rhs.extractRef(scope) + + // fake(bool) + fake(bool) + val boolBoolExpr = onBool(lhsBool, rhsBool, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.boolTypeExpr, rhsType.boolTypeExpr), + expr = boolBoolExpr + ) - // 'fake(bool)' == 'fake(bool)' - conjuncts += ExprWithTypeConstraint( - constraint = mkAnd(lhsType.boolTypeExpr, rhsType.boolTypeExpr), - expr = mkEq( - lhs.extractBool(scope), - rhs.extractBool(scope), + // fake(bool) + fake(fp) + val boolFpExpr = internalResolve(lhsBool, lhsFp, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.boolTypeExpr, rhsType.fpTypeExpr), + expr = boolFpExpr + ) + + // fake(bool) + fake(ref) + val boolRefExpr = internalResolve(lhsBool, lhsRef, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.boolTypeExpr, rhsType.refTypeExpr), + expr = boolRefExpr + ) + + // fake(fp) + fake(bool) + val fpBoolExpr = internalResolve(lhsFp, rhsBool, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.fpTypeExpr, rhsType.boolTypeExpr), + expr = fpBoolExpr + ) + + // fake(fp) + fake(fp) + val fpFpExpr = onFp(lhsFp, rhsFp, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.fpTypeExpr, rhsType.fpTypeExpr), + expr = fpFpExpr + ) + + // fake(fp) + fake(ref) + val fpRefExpr = internalResolve(lhsFp, rhsRef, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.fpTypeExpr, rhsType.refTypeExpr), + expr = fpRefExpr + ) + + // fake(ref) + fake(bool) + val refBoolExpr = internalResolve(lhsRef, rhsBool, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.refTypeExpr, rhsType.boolTypeExpr), + expr = refBoolExpr + ) + + // fake(ref) + fake(fp) + val refFpExpr = internalResolve(lhsRef, rhsFp, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.refTypeExpr, rhsType.fpTypeExpr), + expr = refFpExpr + ) + + // fake(ref) + fake(ref) + val refRefExpr = onRef(lhsRef, rhsRef, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = mkAnd(lhsType.refTypeExpr, rhsType.refTypeExpr), + expr = refRefExpr + ) + } + + lhs.isFakeObject() -> { + val lhsType = lhs.getFakeType(scope) + val lhsBool = lhs.extractBool(scope) + val lhsFp = lhs.extractFp(scope) + val lhsRef = lhs.extractRef(scope) + + when (rhs.sort) { + is UBoolSort -> { + // fake(bool) + bool + val rhsBool = rhs.asExpr(boolSort) + val boolBoolExpr = onBool(lhsBool, rhsBool, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.boolTypeExpr, + expr = boolBoolExpr ) - ) - // 'fake(fp)' == 'fake(fp)' - conjuncts += ExprWithTypeConstraint( - constraint = mkAnd(lhsType.fpTypeExpr, rhsType.fpTypeExpr), - expr = mkFpEqualExpr( - lhs.extractFp(scope), - rhs.extractFp(scope), + // fake(fp) + bool + val fpBoolExpr = internalResolve(lhsFp, rhsBool, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.fpTypeExpr, + expr = fpBoolExpr ) - ) - // 'fake(ref)' == 'fake(ref)' - conjuncts += ExprWithTypeConstraint( - constraint = mkAnd(lhsType.refTypeExpr, rhsType.refTypeExpr), - expr = mkHeapRefEq( - lhs.extractRef(scope), - rhs.extractRef(scope), + // fake(ref) + bool + val refBoolExpr = internalResolve(lhsRef, rhsBool, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.refTypeExpr, + expr = refBoolExpr ) - ) + } - // 'fake(bool)' == 'fake(fp)' - conjuncts += ExprWithTypeConstraint( - constraint = mkAnd(lhsType.boolTypeExpr, rhsType.fpTypeExpr), - expr = mkFpEqualExpr( - boolToFp(lhs.extractBool(scope)), - rhs.extractFp(scope), + is KFp64Sort -> { + // fake(bool) + fp + val rhsFpExpr = rhs.asExpr(fp64Sort) + val boolFpExpr = internalResolve(lhsBool, rhsFpExpr, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.boolTypeExpr, + expr = boolFpExpr ) - ) - // 'fake(fp)' == 'fake(bool)' - conjuncts += ExprWithTypeConstraint( - constraint = mkAnd(lhsType.fpTypeExpr, rhsType.boolTypeExpr), - expr = mkFpEqualExpr( - lhs.extractFp(scope), - boolToFp(rhs.extractBool(scope)), + // fake(fp) + fp + val fpFpExpr = onFp(lhsFp, rhsFpExpr, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.fpTypeExpr, + expr = fpFpExpr ) - ) - // TODO: 'fake(ref)' == 'fake(bool)' - conjuncts += ExprWithTypeConstraint( - constraint = mkAnd(lhsType.refTypeExpr, rhsType.boolTypeExpr), - expr = mkFalse() // TODO mistake, we should coerce the ref object - ) + // fake(ref) + fp + val refFpExpr = internalResolve(lhsRef, rhsFpExpr, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.refTypeExpr, + expr = refFpExpr + ) + } - // TODO: 'fake(ref)' == 'fake(fp)' - conjuncts += ExprWithTypeConstraint( - constraint = mkAnd(lhsType.refTypeExpr, rhsType.fpTypeExpr), - expr = mkFalse() // TODO mistake, we should coerce the ref object - ) + is UAddressSort -> { + // fake(bool) + ref + val rhsRef = rhs.asExpr(addressSort) + val boolRefExpr = internalResolve(lhsBool, rhsRef, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.boolTypeExpr, + expr = boolRefExpr + ) - // TODO: 'fake(bool)' == 'fake(ref)' - conjuncts += ExprWithTypeConstraint( - constraint = mkAnd(lhsType.boolTypeExpr, rhsType.refTypeExpr), - expr = mkFalse() // TODO mistake, we should coerce the ref object - ) + // fake(fp) + ref + val fpRefExpr = internalResolve(lhsFp, rhsRef, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.fpTypeExpr, + expr = fpRefExpr + ) - // TODO: 'fake(fp)' == 'fake(ref)' - conjuncts += ExprWithTypeConstraint( - constraint = mkAnd(lhsType.fpTypeExpr, rhsType.refTypeExpr), - expr = mkFalse() // TODO mistake, we should coerce the ref object - ) + // fake(ref) + ref + val refRefExpr = onRef(lhsRef, rhsRef, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = lhsType.refTypeExpr, + expr = refRefExpr + ) + } + + else -> { + error("Unsupported sort ${rhs.sort}") + } } + } - lhs.isFakeObject() -> { - val lhsType = lhs.getFakeType(scope) + rhs.isFakeObject() -> { + val rhsType = rhs.getFakeType(scope) + val rhsBool = rhs.extractBool(scope) + val rhsFp = rhs.extractFp(scope) + val rhsRef = rhs.extractRef(scope) + + when (lhs.sort) { + is UBoolSort -> { + // bool + fake(bool) + val lhsBool = lhs.asExpr(boolSort) + val boolBoolExpr = onBool(lhsBool, rhsBool, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.boolTypeExpr, + expr = boolBoolExpr + ) - when (rhs.sort) { - boolSort -> { - // 'fake(bool)' == 'fp' - conjuncts += ExprWithTypeConstraint( - constraint = lhsType.boolTypeExpr, - expr = mkEq( - lhs.extractBool(scope), - rhs.asExpr(boolSort), - ) - ) - - // 'fake(fp)' == 'bool' - conjuncts += ExprWithTypeConstraint( - constraint = lhsType.fpTypeExpr, - expr = mkFpEqualExpr( - lhs.extractFp(scope), - boolToFp(rhs.asExpr(boolSort)), - ) - ) - - // TODO: 'fake(ref)' == 'bool' - // 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() - ) - } + // bool + fake(fp) + val boolFpExpr = internalResolve(lhsBool, rhsFp, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.fpTypeExpr, + expr = boolFpExpr + ) - fp64Sort -> { - // 'fake(bool)' == 'fp' - conjuncts += ExprWithTypeConstraint( - constraint = lhsType.boolTypeExpr, - expr = mkFpEqualExpr( - boolToFp(lhs.extractBool(scope)), - rhs.asExpr(fp64Sort), - ) - ) - - // 'fake(fp)' == 'fp' - conjuncts += ExprWithTypeConstraint( - constraint = lhsType.fpTypeExpr, - expr = mkFpEqualExpr( - lhs.extractFp(scope), - rhs.asExpr(fp64Sort), - ) - ) - - // TODO fake(ref) == 'fp' - conjuncts += ExprWithTypeConstraint( - constraint = lhsType.refTypeExpr, - expr = mkFalse() // TODO mistake, we should coerce the ref object - ) - } + // bool + fake(ref) + val boolRefExpr = internalResolve(lhsBool, rhsRef, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.refTypeExpr, + expr = boolRefExpr + ) + } - addressSort -> { - // TODO: 'fake(bool)' == 'ref' - conjuncts += ExprWithTypeConstraint( - constraint = lhsType.boolTypeExpr, - expr = mkFalse() // TODO mistake, we should coerce the ref object - ) - - // TODO: 'fake(fp)' == 'ref' - conjuncts += ExprWithTypeConstraint( - constraint = lhsType.fpTypeExpr, - expr = mkFalse() // TODO mistake, we should coerce the ref object - ) - - // 'fake(ref)' == 'ref' - conjuncts += ExprWithTypeConstraint( - constraint = lhsType.refTypeExpr, - expr = mkHeapRefEq( - lhs.extractRef(scope), - rhs.asExpr(addressSort), - ) - ) - } + is KFp64Sort -> { + // fp + fake(bool) + val lhsFp = lhs.asExpr(fp64Sort) + val fpBoolExpr = internalResolve(lhsFp, rhsBool, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.boolTypeExpr, + expr = fpBoolExpr + ) - else -> { - error("Unsupported sort ${rhs.sort}") - } - } - } + // fp + fake(fp) + val fpFpExpr = onFp(lhsFp, rhsFp, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.fpTypeExpr, + expr = fpFpExpr + ) - rhs.isFakeObject() -> { - val rhsType = rhs.getFakeType(scope) + // fp + fake(ref) + val fpRefExpr = internalResolve(lhsFp, rhsRef, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.refTypeExpr, + expr = fpRefExpr + ) + } - when (lhs.sort) { - boolSort -> { - // 'bool' == 'fake(bool)' - conjuncts += ExprWithTypeConstraint( - constraint = rhsType.boolTypeExpr, - expr = mkEq( - lhs.asExpr(boolSort), - rhs.extractBool(scope), - ) - ) - - // 'bool' == 'fake(fp)' - conjuncts += ExprWithTypeConstraint( - constraint = rhsType.fpTypeExpr, - expr = mkFpEqualExpr( - boolToFp(lhs.asExpr(boolSort)), - rhs.extractFp(scope), - ) - ) - - // TODO: 'bool' == 'fake(ref)' - conjuncts += ExprWithTypeConstraint( - constraint = rhsType.refTypeExpr, - expr = mkFalse() // TODO mistake, we should coerce the ref object - ) - } + is UAddressSort -> { + // ref + fake(bool) + val lhsRef = lhs.asExpr(addressSort) + val refBoolExpr = internalResolve(lhsRef, rhsBool, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.boolTypeExpr, + expr = refBoolExpr + ) - fp64Sort -> { - // 'fp' == 'fake(bool)' - conjuncts += ExprWithTypeConstraint( - constraint = rhsType.boolTypeExpr, - expr = mkFpEqualExpr( - lhs.asExpr(fp64Sort), - boolToFp(rhs.extractBool(scope)), - ) - ) - - // 'fp' == 'fake(fp)' - conjuncts += ExprWithTypeConstraint( - constraint = rhsType.fpTypeExpr, - expr = mkFpEqualExpr( - lhs.asExpr(fp64Sort), - rhs.extractFp(scope), - ) - ) - - // TODO: 'fp' == 'fake(ref)' - conjuncts += ExprWithTypeConstraint( - constraint = rhsType.refTypeExpr, - expr = mkFalse() // TODO mistake, we should coerce the ref object - ) - } + // ref + fake(fp) + val refFpExpr = internalResolve(lhsRef, rhsFp, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.fpTypeExpr, + expr = refFpExpr + ) - addressSort -> { - // TODO: 'ref' == 'fake(bool)' - conjuncts += ExprWithTypeConstraint( - constraint = rhsType.boolTypeExpr, - expr = mkFalse() // TODO mistake, we should coerce the ref object - ) - - // TODO: 'ref' == 'fake(fp)' - conjuncts += ExprWithTypeConstraint( - constraint = rhsType.fpTypeExpr, - expr = mkFalse() // TODO mistake, we should coerce the ref object - ) - - // 'ref' == 'fake(ref)' - conjuncts += ExprWithTypeConstraint( - constraint = rhsType.refTypeExpr, - expr = mkHeapRefEq( - lhs.asExpr(addressSort), - rhs.extractRef(scope), - ) - ) - } + // ref + fake(ref) + val refRefExpr = onRef(lhsRef, rhsRef, scope)?.asExpr(resultSort) ?: return null + conjuncts += ExprWithTypeConstraint( + constraint = rhsType.refTypeExpr, + expr = refRefExpr + ) + } - else -> { - error("Unsupported sort ${rhs.sort}") - } + else -> { + error("Unsupported sort ${lhs.sort}") } } } + } + + return reduce(conjuncts) + } + + data object Eq : TsBinaryOperator { + + override fun TsContext.onBool( + lhs: UBoolExpr, + rhs: UBoolExpr, + scope: TsStepScope, + ): UBoolExpr { + return mkEq(lhs, rhs) + } + + override fun TsContext.onFp( + lhs: UExpr, + rhs: UExpr, + scope: TsStepScope, + ): UBoolExpr { + return mkFpEqualExpr(lhs, rhs) + } - // val ground: UBoolExpr = mkFalse() - // return conjuncts.foldRight(ground) { (condition, value), acc -> - // mkIte(condition, value, acc) - // } - return mkAnd(conjuncts.map { (condition, value) -> mkImplies(condition, value) }) + override fun TsContext.onRef( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope, + ): UBoolExpr { + return mkEq(lhs, rhs) + } + + override fun TsContext.resolveFakeObject( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope, + ): UBoolExpr { + return commonResolveFakeObject( + lhs, + rhs, + scope, + boolSort + ) { conjuncts -> mkAnd(conjuncts.map { (condition, value) -> mkImplies(condition, value) }) } + ?: error("Should not be null") } override fun TsContext.internalResolve( @@ -724,215 +738,16 @@ sealed interface TsBinaryOperator { rhs: UExpr<*>, scope: TsStepScope, ): UExpr { - check(lhs.isFakeObject() || rhs.isFakeObject()) - - 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}") - } - } + return commonResolveFakeObject( + lhs, + rhs, + scope, + fp64Sort + ) { conjuncts -> + conjuncts.foldRight(mkFp(0.0, fp64Sort).asExpr(fp64Sort)) { value, acc -> + mkIte(value.constraint, value.expr, acc) } - - 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) - } + } ?: error("Should not be null") } override fun TsContext.internalResolve( @@ -1133,8 +948,9 @@ sealed interface TsBinaryOperator { rhs: UHeapRef, scope: TsStepScope, ): UBoolExpr { - // TODO: LT operator for references is not fully supported - return mkFalse() + val lhsNumeric = mkNumericExpr(lhs, scope) + val rhsNumeric = mkNumericExpr(rhs, scope) + return mkFpLessExpr(lhsNumeric, rhsNumeric) } override fun TsContext.resolveFakeObject( @@ -1142,8 +958,16 @@ sealed interface TsBinaryOperator { rhs: UExpr<*>, scope: TsStepScope, ): UBoolExpr { - // TODO: LT operator for fake objects is not fully supported - return mkFalse() + return commonResolveFakeObject( + lhs, + rhs, + scope, + boolSort + ) { conjuncts -> + conjuncts.foldRight(mkFalse().asExpr(boolSort)) { value, acc -> + mkIte(value.constraint, value.expr, acc) + } + } ?: error("Should not be null") } override fun TsContext.internalResolve( @@ -1154,9 +978,9 @@ sealed interface TsBinaryOperator { // TODO: the immediate conversion to numbers is not correct, // we first need to try to convert arguments to primitive values, // which might become strings, for which LT has different semantics. - val left = mkNumericExpr(lhs, scope) - val right = mkNumericExpr(rhs, scope) - return mkFpLessExpr(left, right) + val lhsNumeric = mkNumericExpr(lhs, scope) + val rhsNumeric = mkNumericExpr(rhs, scope) + return mkFpLessExpr(lhsNumeric, rhsNumeric) } } @@ -1182,7 +1006,9 @@ sealed interface TsBinaryOperator { rhs: UHeapRef, scope: TsStepScope, ): UBoolExpr { - TODO("Not yet implemented") + val lhsNumeric = mkNumericExpr(lhs, scope) + val rhsNumeric = mkNumericExpr(rhs, scope) + return mkFpGreaterExpr(lhsNumeric, rhsNumeric) } override fun TsContext.resolveFakeObject( @@ -1190,7 +1016,16 @@ sealed interface TsBinaryOperator { rhs: UExpr<*>, scope: TsStepScope, ): UBoolExpr { - TODO("Not yet implemented") + return commonResolveFakeObject( + lhs, + rhs, + scope, + boolSort + ) { conjuncts -> + conjuncts.foldRight(falseExpr.asExpr(boolSort)) { value, acc -> + mkIte(value.constraint, value.expr, acc) + } + } ?: error("Should not be null") } override fun TsContext.internalResolve( @@ -1198,7 +1033,9 @@ sealed interface TsBinaryOperator { rhs: UExpr<*>, scope: TsStepScope, ): UBoolExpr { - TODO("Not yet implemented") + val lhsNumeric = mkNumericExpr(lhs, scope) + val rhsNumeric = mkNumericExpr(rhs, scope) + return mkFpGreaterExpr(lhsNumeric, rhsNumeric) } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt index e63fdc0b8a..a85aeed078 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt @@ -113,7 +113,7 @@ class RunOnDemoPhotosProject : TsMethodTestRunner() { fun `test on particular method`() { val method = scene.projectClasses .flatMap { it.methods } - .single { it.name == "onSelect" && it.enclosingClass?.name == "AlbumSetPage" } + .single { it.name == "onCreate" && it.enclosingClass?.name == "EntryAbility" } val tsOptions = TsOptions() TsMachine(scene, options, tsOptions).use { machine -> 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 c56cc3bcd5..c1ebdb415e 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 @@ -1,6 +1,7 @@ package org.usvm.samples.operators import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Disabled import org.usvm.api.TsTestValue import org.usvm.util.TsMethodTestRunner import org.usvm.util.toDouble @@ -75,12 +76,15 @@ class Add : TsMethodTestRunner() { ) } + @Disabled("Flaky test, see https://github.com/UnitTestBot/usvm/issues/310") @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() }, + // This condition sometimes fails, in case `bool` + `null` + // TODO https://github.com/UnitTestBot/usvm/issues/310 { a, b, r -> (a is TsTestValue.TsClass || b is TsTestValue.TsClass diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Less.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Less.kt new file mode 100644 index 0000000000..a865aab266 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Less.kt @@ -0,0 +1,62 @@ +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 Less : TsMethodTestRunner() { + private val className = this::class.simpleName!! + + override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators") + + @Test + fun testLessNumbers() { + val method = getMethod(className, "lessNumbers") + discoverProperties( + method, + { a, b, r -> a.number < b.number && r.number == a.number }, + { a, b, r -> b.number < a.number && r.number == b.number }, + { a, b, r -> a.number == b.number && r.number == 0.0 }, + ) + } + + @Test + fun testLessBooleans() { + val method = getMethod(className, "lessBooleans") + discoverProperties( + method, + { a, b, r -> !a.value && b.value && !r.value }, + { a, b, r -> a.value && !b.value && !r.value }, + { a, b, r -> a.value == b.value && !r.value }, + ) + } + + @Test + fun testLessMixed() { + val method = getMethod(className, "lessMixed") + discoverProperties( + method, + { a, b, r -> a.number < b.value.toDouble() && r.number == a.number }, + { a, b, r -> b.value.toDouble() < a.number && r.number == b.value.toDouble() }, + { a, b, r -> a.number == b.value.toDouble() && r.number == 0.0 }, + ) + } + + @Test + fun testLessRefs() { + val method = getMethod(className, "lessRefs") + discoverProperties( + method, + ) + } + + @Test + fun testLessUnknown() { + val method = getMethod(className, "lessUnknown") + discoverProperties( + method, + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/operators/Less.ts b/usvm-ts/src/test/resources/samples/operators/Less.ts new file mode 100644 index 0000000000..3122187c40 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/operators/Less.ts @@ -0,0 +1,63 @@ +class Less { + lessNumbers(a: number, b: number): number { + if (a < b) { + return a; + } + + if (b < a) { + return b; + } + + return 0; // Return 0 if they are equal + } + + lessBooleans(a: boolean, b: boolean): boolean { + if (a < b) { + return a; + } + + if (b < a) { + return b; + } + + return false; // Return false if they are equal + } + + lessMixed(a: number, b: boolean): number { + if (a < b) { + return a; + } + + if (b < a) { + return b ? 1 : 0; // Convert boolean to number + } + + return 0; // Return 0 if they are equal + } + + lessRefs(a: object, b: object): boolean { + if (a < b) { + return true; // Reference comparison, not value + } + + if (b < a) { + return false; // Reference comparison, not value + } + + return false; // Return false if they are equal + } + + lessUnknown(a, b): boolean { + if (a < b) { + return true; // Reference comparison, not value + } + + if (b < a) { + return false; // Reference comparison, not value + } + + return false; // Return false if they are equal + } +} + +