diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 3fb83282b..012702dbb 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -1,6 +1,7 @@ package org.usvm.machine import io.ksmt.sort.KFp64Sort +import io.ksmt.utils.asExpr import org.jacodb.ets.base.EtsBooleanType import org.jacodb.ets.base.EtsNullType import org.jacodb.ets.base.EtsNumberType @@ -20,6 +21,8 @@ import org.usvm.USort import org.usvm.collection.field.UFieldLValue import org.usvm.machine.expr.TsUndefinedSort import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.types.FakeType import kotlin.contracts.ExperimentalContracts import kotlin.contracts.contract @@ -60,6 +63,40 @@ class TsContext( return sort == addressSort && this is UConcreteHeapRef && address > MAGIC_OFFSET } + fun UExpr.toFakeObject(scope: TsStepScope): UConcreteHeapRef { + if (isFakeObject()) { + return this + } + + val ref = createFakeObjectRef() + + scope.calcOnState { + when (sort) { + boolSort -> { + val lvalue = getIntermediateBoolLValue(ref.address) + memory.write(lvalue, this@toFakeObject.asExpr(boolSort), guard = trueExpr) + memory.types.allocate(ref.address, FakeType.fromBool(this@TsContext)) + } + + fp64Sort -> { + val lValue = getIntermediateFpLValue(ref.address) + memory.write(lValue, this@toFakeObject.asExpr(fp64Sort), guard = trueExpr) + memory.types.allocate(ref.address, FakeType.fromFp(this@TsContext)) + } + + addressSort -> { + val lValue = getIntermediateRefLValue(ref.address) + memory.types.allocate(ref.address, FakeType.fromRef(this@TsContext)) + memory.write(lValue, this@toFakeObject.asExpr(addressSort), guard = trueExpr) + } + + else -> TODO("Not yet supported") + } + } + + return ref + } + fun createFakeObjectRef(): UConcreteHeapRef { val address = mkAddressCounter().freshAllocatedAddress() + MAGIC_OFFSET return mkConcreteHeapRef(address) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index a73e24ee6..107ade977 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -6,6 +6,7 @@ import mu.KotlinLogging import org.jacodb.ets.base.EtsAddExpr import org.jacodb.ets.base.EtsAndExpr import org.jacodb.ets.base.EtsArrayAccess +import org.jacodb.ets.base.EtsArrayType import org.jacodb.ets.base.EtsAwaitExpr import org.jacodb.ets.base.EtsBinaryExpr import org.jacodb.ets.base.EtsBitAndExpr @@ -63,7 +64,6 @@ import org.jacodb.ets.base.EtsTypeOfExpr import org.jacodb.ets.base.EtsUnaryExpr import org.jacodb.ets.base.EtsUnaryPlusExpr import org.jacodb.ets.base.EtsUndefinedConstant -import org.jacodb.ets.base.EtsUnknownType import org.jacodb.ets.base.EtsUnsignedRightShiftExpr import org.jacodb.ets.base.EtsValue import org.jacodb.ets.base.EtsVoidExpr @@ -78,6 +78,7 @@ import org.usvm.USort import org.usvm.api.allocateArray import org.usvm.api.makeSymbolicPrimitive import org.usvm.collection.array.UArrayIndexLValue +import org.usvm.collection.array.length.UArrayLengthLValue import org.usvm.collection.field.UFieldLValue import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope @@ -497,20 +498,22 @@ class TsExprResolver( // region ACCESS - override fun visit(value: EtsArrayAccess): UExpr? { + override fun visit(value: EtsArrayAccess): UExpr? = with(ctx) { val instance = resolve(value.array)?.asExpr(ctx.addressSort) ?: return null val index = resolve(value.index)?.asExpr(ctx.fp64Sort) ?: return null - val bvIndex = ctx.mkFpToBvExpr( - roundingMode = ctx.fpRoundingModeSortDefaultValue(), + val bvIndex = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), value = index, bvSize = 32, isSigned = true ) - val sort = if (value.type is EtsUnknownType) ctx.addressSort else ctx.typeToSort(value.type) - val lValue = UArrayIndexLValue(sort, instance, bvIndex, value.array.type) + val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, value.array.type) + val expr = scope.calcOnState { memory.read(lValue) } + + check(expr.isFakeObject()) { "Only fake objects are allowed in arrays" } - return scope.calcOnState { memory.read(lValue) } + return expr } private fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) { @@ -535,7 +538,16 @@ class TsExprResolver( checkUndefinedOrNullPropertyRead(instanceRef) ?: return null - // TODO: checkNullPointer(instanceRef) + // TODO It is a hack for array's length + if (value.instance.type is EtsArrayType && value.field.name == "length") { + val lValue = UArrayLengthLValue(instanceRef, value.instance.type, ctx.sizeSort) + val expr = scope.calcOnState { memory.read(lValue) } + + check(expr.sort == ctx.sizeSort) + + return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), expr.asExpr(sizeSort), signed = true) + } + val fieldType = scene.fieldLookUp(value.field).type val sort = typeToSort(fieldType) val lValue = UFieldLValue(sort, instanceRef, value.field.name) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index b3ec5d025..56b52981c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -24,6 +24,7 @@ import org.usvm.StepScope import org.usvm.UInterpreter import org.usvm.api.targets.TsTarget import org.usvm.collection.array.UArrayIndexLValue +import org.usvm.collection.array.length.UArrayLengthLValue import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.forkblacklists.UForkBlackList import org.usvm.machine.TsApplicationGraph @@ -38,6 +39,7 @@ import org.usvm.machine.state.newStmt import org.usvm.machine.state.parametersWithThisCount import org.usvm.machine.state.returnValue import org.usvm.memory.URegisterStackLValue +import org.usvm.sizeSort import org.usvm.targets.UTargetsSet import org.usvm.utils.ensureSat @@ -123,11 +125,11 @@ class TsInterpreter( } } - private fun visitAssignStmt(scope: TsStepScope, stmt: EtsAssignStmt) { + private fun visitAssignStmt(scope: TsStepScope, stmt: EtsAssignStmt) = with(ctx) { val exprResolver = exprResolverWithScope(scope) val expr = exprResolver.resolve(stmt.rhv) ?: return - check(expr.sort != ctx.unresolvedSort) { + check(expr.sort != unresolvedSort) { "A value of the unresolved sort should never be returned from `resolve` function" } @@ -138,31 +140,33 @@ class TsInterpreter( saveSortForLocal(idx, expr.sort) val lValue = URegisterStackLValue(expr.sort, idx) - memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr) + memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr) } is EtsArrayAccess -> { - // TODO save sorts? - val instance = exprResolver.resolve(lhv.array)?.asExpr(ctx.addressSort) ?: return@doWithState - val index = exprResolver.resolve(lhv.index)?.asExpr(ctx.fp64Sort) ?: return@doWithState + val instance = exprResolver.resolve(lhv.array)?.asExpr(addressSort) ?: return@doWithState + val index = exprResolver.resolve(lhv.index)?.asExpr(fp64Sort) ?: return@doWithState // TODO fork on floating point field - val bvIndex = ctx.mkFpToBvExpr( - roundingMode = ctx.fpRoundingModeSortDefaultValue(), + val bvIndex = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), value = index, bvSize = 32, isSigned = true - ) - - if (stmt.lhv.type == stmt.rhv.type) { - val lValue = UArrayIndexLValue(expr.sort, instance, bvIndex, lhv.array.type) - // TODO error with array values type - memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr) - } else { - val lValue = UArrayIndexLValue(ctx.unresolvedSort, instance, bvIndex, lhv.array.type) - // TODO create fake object, probably the type of the array should be modified as well - memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr) - } + ).asExpr(sizeSort) + + val lengthLValue = UArrayLengthLValue(instance, lhv.array.type, sizeSort) + val currentLength = memory.read(lengthLValue).asExpr(sizeSort) + + val condition = mkBvSignedGreaterOrEqualExpr(bvIndex, currentLength) + val newLength = mkIte(condition, mkBvAddExpr(bvIndex, mkBv(1)), currentLength) + + memory.write(lengthLValue, newLength, guard = trueExpr) + + val fakeExpr = expr.toFakeObject(scope) + + val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, lhv.array.type) + memory.write(lValue, fakeExpr, guard = trueExpr) } else -> TODO("Not yet implemented") 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 3b9b444e6..b114efb70 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 @@ -421,9 +421,57 @@ sealed interface TsBinaryOperator { scope: TsStepScope, ): UExpr { check(lhs.isFakeObject() || rhs.isFakeObject()) - // TODO: delegating to '==' is not correct in general case - return with(Eq) { - resolveFakeObject(lhs, rhs, scope) + + return scope.calcOnState { + when { + lhs.isFakeObject() && rhs.isFakeObject() -> { + val lhsType = memory.typeStreamOf(lhs).single() as FakeType + val rhsType = memory.typeStreamOf(rhs).single() as FakeType + + scope.assert( + mkAnd( + lhsType.boolTypeExpr eq rhsType.boolTypeExpr, + lhsType.fpTypeExpr eq rhsType.fpTypeExpr, + // TODO support type equality + lhsType.refTypeExpr eq rhsType.refTypeExpr + ) + ) + } + + lhs.isFakeObject() -> { + val lhsType = memory.typeStreamOf(lhs).single() as FakeType + + val condition = 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 = memory.typeStreamOf(rhs).single() as FakeType + + scope.assert(rhsType.mkExactlyOneTypeConstraint(ctx)) + + val condition = 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) + } + } + + return@calcOnState with(Eq) { + resolveFakeObject(lhs, rhs, scope) + } } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeType.kt index 3d20150d4..efe0acf42 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeType.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeType.kt @@ -27,6 +27,20 @@ class FakeType( mkOr(boolTypeExpr, fpTypeExpr, refTypeExpr), ) } + + companion object { + fun fromBool(ctx: TsContext): FakeType { + return FakeType(ctx.mkTrue(), ctx.mkFalse(), ctx.mkFalse()) + } + + fun fromFp(ctx: TsContext): FakeType { + return FakeType(ctx.mkFalse(), ctx.mkTrue(), ctx.mkFalse()) + } + + fun fromRef(ctx: TsContext): FakeType { + return FakeType(ctx.mkFalse(), ctx.mkFalse(), ctx.mkTrue()) + } + } } -data class ExprWithTypeConstraint(val constraint: UBoolExpr, val expr: UExpr) \ No newline at end of file +data class ExprWithTypeConstraint(val constraint: UBoolExpr, val expr: UExpr) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt index c8aecf78c..93ae613ee 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt @@ -2,7 +2,6 @@ package org.usvm.samples import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.loadEtsFileAutoConvert -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.api.TsValue import org.usvm.util.TsMethodTestRunner @@ -59,7 +58,6 @@ class Arrays : TsMethodTestRunner() { } @Test - @Disabled("Arrays should contain only fake objects") fun testCreateMixedArray() { val method = getMethod("Arrays", "createMixedArray") discoverProperties>( @@ -75,7 +73,7 @@ class Arrays : TsMethodTestRunner() { } @Test - fun testCreateArrayOfUnknown() { + fun testCreateArrayOfUnknownValues() { val method = getMethod("Arrays", "createArrayOfUnknownValues") discoverProperties>( method = method, @@ -89,7 +87,6 @@ class Arrays : TsMethodTestRunner() { } @Test - @Disabled("Arrays should contain only fake objects") fun testCreateArrayOfNumbersAndPutDifferentTypes() { val method = getMethod("Arrays", "createArrayOfNumbersAndPutDifferentTypes") discoverProperties>( @@ -97,10 +94,36 @@ class Arrays : TsMethodTestRunner() { { r -> val values = r.values values.size == 3 - && (values[0] as TsValue.TsClass).properties.size == 1 + && values[0] is TsValue.TsNull && (values[1] as TsValue.TsBoolean).value && values[2] is TsValue.TsUndefined }, ) } + + @Test + fun testAllocatedArrayLengthExpansion() { + val method = getMethod("Arrays", "allocatedArrayLengthExpansion") + discoverProperties>( + method = method, + { r -> + r.values.size == 6 + && (r.values[0] as TsValue.TsNumber).number == 1.0 + && (r.values[1] as TsValue.TsNumber).number == 2.0 + && (r.values[2] as TsValue.TsNumber).number == 3.0 + && r.values[3] is TsValue.TsUndefined + && r.values[4] is TsValue.TsUndefined + && (r.values[5] as TsValue.TsNumber).number == 5.0 + } + ) + } + + @Test + fun testWriteInTheIndexEqualToLength() { + val method = getMethod("Arrays", "writeInTheIndexEqualToLength") + discoverProperties>( + method = method, + { r -> r.values.map { it.number } == listOf(1.0, 2.0, 3.0, 4.0) }, + ) + } } 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 752f69d36..f5bc1209b 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -138,6 +138,7 @@ open class TsTestStateResolver( resolveRef(expr.asExpr(ctx.addressSort), EtsUnknownType) } } + else -> TODO() } } @@ -160,6 +161,7 @@ open class TsTestStateResolver( val type = finalStateMemory.types.getTypeStream(expr).first() resolveRef(expr, type) } + else -> error("Unexpected type: $type") } } @@ -170,14 +172,16 @@ open class TsTestStateResolver( val values = (0 until length.intValue).map { val index = ctx.mkSizeExpr(it) - // TODO wrong sort - val lValue = if (type.elementType is EtsUnknownType) { - UArrayIndexLValue(ctx.addressSort, expr, index, type) - } else { - UArrayIndexLValue(ctx.typeToSort(type.elementType), expr, index, type) + val lValue = UArrayIndexLValue(ctx.addressSort, expr, index, type) + val value = memory.read(lValue) + + if (model.eval(ctx.mkHeapRefEq(value, ctx.mkUndefinedValue())).isTrue) { + return@map TsValue.TsUndefined } - val value = memory.read(lValue) // TODO write reading??? - resolveExpr(value, type.elementType) + + with(ctx) { check(value.isFakeObject()) { "Only fake objects are allowed in arrays" } } + + resolveFakeObject(value as UConcreteHeapRef) } return TsValue.TsArray(values) diff --git a/usvm-ts/src/test/resources/samples/Arrays.ts b/usvm-ts/src/test/resources/samples/Arrays.ts index 7f613ec89..62697b08c 100644 --- a/usvm-ts/src/test/resources/samples/Arrays.ts +++ b/usvm-ts/src/test/resources/samples/Arrays.ts @@ -1,7 +1,7 @@ class Arrays { createConstantArrayOfNumbers() { let x = [1, 2, 3] - if (x[0] == 1) return 1 + if (x[0] === 1) return 1 return -1 } @@ -11,7 +11,7 @@ class Arrays { createAndAccessArrayOfBooleans() { let x = [true, false, true] - if (x[0] == true) return 1 + if (x[0] === true) return 1 return -1 } @@ -27,17 +27,39 @@ class Arrays { createArrayOfUnknownValues(a, b, c) { let x = [a, b, c] - if (x[0] == 1.1) return x - if (x[1] == true) return x - if (x[2] == undefined) return x + if (x[0] === 1.1) return x + if (x[1] === true) return x + if (x[2] === undefined) return x return x } createArrayOfNumbersAndPutDifferentTypes() { let x = [1, 2, 3] + // @ts-ignore x[1] = true x[2] = undefined x[0] = null return x } + + allocatedArrayLengthExpansion() { + let x = [1, 2, 3] + if (x.length == 3) { + x[5] = 5 + // @ts-ignore + if (x.length == 6) { + return x + } else { + return -1 // unreachable + } + } else { + return -1 // unreachable + } + } + + writeInTheIndexEqualToLength() { + let x = [1, 2, 3] + x[3] = 4 + return x + } }