From 93871de8996bd4a444e78988d91df3c14b7b2674 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Thu, 27 Feb 2025 13:31:40 +0300 Subject: [PATCH] Field writing support (#263) --------- Co-authored-by: Konstantin Chukharev --- .../main/kotlin/org/usvm/machine/TsContext.kt | 44 +++- .../org/usvm/machine/expr/TsExprResolver.kt | 175 +++++++++++---- .../org/usvm/machine/expr/TsExpressions.kt | 8 +- .../usvm/machine/interpreter/TsInterpreter.kt | 44 +++- .../usvm/machine/operator/TsBinaryOperator.kt | 74 ++++++- .../org/usvm/machine/state/TsStateUtils.kt | 3 +- .../org/usvm/machine/types/FakeExprUtil.kt | 18 +- .../main/kotlin/org/usvm/util/LValueUtil.kt | 44 ++++ .../kotlin/org/usvm/samples/FieldAccess.kt | 123 +++++++++++ .../test/kotlin/org/usvm/util/ObjectClass.kt | 27 +++ .../kotlin/org/usvm/util/TsTestResolver.kt | 209 ++++++++++++------ .../src/test/resources/samples/FieldAccess.ts | 92 ++++++++ 12 files changed, 716 insertions(+), 145 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/util/ObjectClass.kt create mode 100644 usvm-ts/src/test/resources/samples/FieldAccess.ts 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 012702dbb..3b45d71f3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -2,6 +2,7 @@ package org.usvm.machine import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr +import org.jacodb.ets.base.EtsAnyType import org.jacodb.ets.base.EtsBooleanType import org.jacodb.ets.base.EtsNullType import org.jacodb.ets.base.EtsNumberType @@ -19,10 +20,13 @@ import org.usvm.UContext import org.usvm.UExpr import org.usvm.USort import org.usvm.collection.field.UFieldLValue +import org.usvm.isTrue 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 org.usvm.types.single +import org.usvm.util.mkFieldLValue import kotlin.contracts.ExperimentalContracts import kotlin.contracts.contract @@ -51,6 +55,7 @@ class TsContext( is EtsUndefinedType -> addressSort is EtsUnknownType -> unresolvedSort is EtsUnionType -> unresolvedSort + is EtsAnyType -> unresolvedSort else -> TODO("Support all JacoDB types, encountered $type") } @@ -70,7 +75,7 @@ class TsContext( val ref = createFakeObjectRef() - scope.calcOnState { + scope.doWithState { when (sort) { boolSort -> { val lvalue = getIntermediateBoolLValue(ref.address) @@ -86,8 +91,8 @@ class 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) + memory.types.allocate(ref.address, FakeType.fromRef(this@TsContext)) } else -> TODO("Not yet supported") @@ -97,6 +102,35 @@ class TsContext( return ref } + fun UExpr.extractSingleValueFromFakeObjectOrNull(scope: TsStepScope): UExpr? { + if (!isFakeObject()) return null + + val type = scope.calcOnState { + memory.types.getTypeStream(this@extractSingleValueFromFakeObjectOrNull).single() as FakeType + } + + return scope.calcOnState { + when { + type.boolTypeExpr.isTrue -> { + val lValue = getIntermediateBoolLValue(address) + memory.read(lValue).asExpr(boolSort) + } + + type.fpTypeExpr.isTrue -> { + val lValue = getIntermediateFpLValue(address) + memory.read(lValue).asExpr(fp64Sort) + } + + type.refTypeExpr.isTrue -> { + val lValue = getIntermediateRefLValue(address) + memory.read(lValue).asExpr(addressSort) + } + + else -> null + } + } + } + fun createFakeObjectRef(): UConcreteHeapRef { val address = mkAddressCounter().freshAllocatedAddress() + MAGIC_OFFSET return mkConcreteHeapRef(address) @@ -108,15 +142,15 @@ class TsContext( private val nullValue: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress()) fun getIntermediateBoolLValue(addr: Int): UFieldLValue { - return UFieldLValue(boolSort, mkConcreteHeapRef(addr), IntermediateLValueField.BOOL) + return mkFieldLValue(boolSort, mkConcreteHeapRef(addr), IntermediateLValueField.BOOL) } fun getIntermediateFpLValue(addr: Int): UFieldLValue { - return UFieldLValue(fp64Sort, mkConcreteHeapRef(addr), IntermediateLValueField.FP) + return mkFieldLValue(fp64Sort, mkConcreteHeapRef(addr), IntermediateLValueField.FP) } fun getIntermediateRefLValue(addr: Int): UFieldLValue { - return UFieldLValue(addressSort, mkConcreteHeapRef(addr), IntermediateLValueField.REF) + return mkFieldLValue(addressSort, mkConcreteHeapRef(addr), IntermediateLValueField.REF) } } 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 8213ad375..b8c575775 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 @@ -64,7 +64,9 @@ import org.jacodb.ets.base.EtsType import org.jacodb.ets.base.EtsTypeOfExpr import org.jacodb.ets.base.EtsUnaryExpr import org.jacodb.ets.base.EtsUnaryPlusExpr +import org.jacodb.ets.base.EtsUnclearRefType 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 @@ -80,10 +82,7 @@ import org.usvm.UExpr import org.usvm.UHeapRef 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.isTrue import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.operator.TsBinaryOperator @@ -95,8 +94,12 @@ import org.usvm.machine.state.newStmt import org.usvm.machine.types.FakeType import org.usvm.machine.types.mkFakeValue import org.usvm.memory.ULValue -import org.usvm.memory.URegisterStackLValue import org.usvm.sizeSort +import org.usvm.types.single +import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkArrayLengthLValue +import org.usvm.util.mkFieldLValue +import org.usvm.util.mkRegisterStackLValue import org.usvm.util.throwExceptionWithoutStackFrameDrop private val logger = KotlinLogging.logger {} @@ -282,8 +285,7 @@ class TsExprResolver( } override fun visit(expr: EtsMulExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + return resolveBinaryOperator(TsBinaryOperator.Mul, expr) } override fun visit(expr: EtsAndExpr): UExpr? { @@ -402,8 +404,30 @@ class TsExprResolver( // region CALL - override fun visit(expr: EtsInstanceCallExpr): UExpr? { - return resolveInvoke( + override fun visit(expr: EtsInstanceCallExpr): UExpr? = with(ctx) { + if (expr.instance.name == "Number") { + if (expr.method.name == "isNaN") { + val arg = resolve(expr.args.single()) ?: return null + if (arg.sort == fp64Sort) { + return mkFpIsNaNExpr(arg.asExpr(fp64Sort)) + } + if (arg.isFakeObject()) { + val fakeType = scope.calcOnState { + memory.types.getTypeStream(arg).single() as FakeType + } + scope.calcOnState { + if (fakeType.fpTypeExpr.isTrue) { + val lValue = getIntermediateFpLValue(arg.address) + val value = memory.read(lValue).asExpr(fp64Sort) + return@calcOnState mkFpIsNaNExpr(value) + } + null + }?.let { return it } + } + } + } + + resolveInvoke( method = expr.method, instance = expr.instance, arguments = { expr.args }, @@ -422,15 +446,15 @@ class TsExprResolver( } } - override fun visit(expr: EtsStaticCallExpr): UExpr? { + override fun visit(expr: EtsStaticCallExpr): UExpr? = with(ctx) { if (expr.method.name == "Number" && expr.method.enclosingClass.name == "") { check(expr.args.size == 1) { "Number constructor should have exactly one argument" } return resolveAfterResolved(expr.args.single()) { - ctx.mkNumericExpr(it, scope) + mkNumericExpr(it, scope) } } - return resolveInvoke( + resolveInvoke( method = expr.method, instance = null, arguments = { expr.args }, @@ -453,21 +477,26 @@ class TsExprResolver( // Perfect signature: if (method.enclosingClass.name != UNKNOWN_CLASS_NAME) { val clazz = ctx.scene.projectAndSdkClasses.single { it.name == method.enclosingClass.name } - return clazz.methods.single { it.name == method.name } + return (clazz.methods + clazz.ctor).single { it.name == method.name } } // Unknown signature: val instanceType = instance.type if (instanceType is EtsClassType) { - val classes = ctx.scene.projectAndSdkClasses.filter { it.name == instanceType.signature.name } + val classes = ctx.scene.projectAndSdkClasses + .filter { it.name == instanceType.signature.name } if (classes.size == 1) { val clazz = classes.single() - return clazz.methods.single { it.name == method.name } + return (clazz.methods + clazz.ctor).single { it.name == method.name } } - val methods = classes.flatMap { it.methods }.filter { it.name == method.name } + val methods = classes + .flatMap { it.methods + it.ctor } + .filter { it.name == method.name } if (methods.size == 1) return methods.single() } else { - val methods = ctx.scene.projectAndSdkClasses.flatMap { it.methods }.filter { it.name == method.name } + val methods = ctx.scene.projectAndSdkClasses + .flatMap { it.methods + it.ctor } + .filter { it.name == method.name } if (methods.size == 1) return methods.single() } error("Cannot resolve method $method") @@ -541,7 +570,12 @@ class TsExprResolver( isSigned = true ) - val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, value.array.type) + val lValue = mkArrayIndexLValue( + addressSort, + instance, + bvIndex.asExpr(ctx.sizeSort), + value.array.type as EtsArrayType + ) val expr = scope.calcOnState { memory.read(lValue) } check(expr.isFakeObject()) { "Only fake objects are allowed in arrays" } @@ -566,8 +600,10 @@ class TsExprResolver( state.throwExceptionWithoutStackFrameDrop(address, type) } - private fun resolveInstanceField(instance: EtsLocal, field: EtsFieldSignature): EtsField { - + private fun resolveInstanceField( + instance: EtsLocal, + field: EtsFieldSignature, + ): EtsField { // Perfect signature: if (field.enclosingClass.name != UNKNOWN_CLASS_NAME) { val clazz = ctx.scene.projectAndSdkClasses.single { it.name == field.enclosingClass.name } @@ -584,10 +620,24 @@ class TsExprResolver( return clazz.fields.single { it.name == field.name } } val fields = classes.flatMap { it.fields.filter { it.name == field.name } } - if (fields.size == 1) return fields.single() + if (fields.size == 1) { + return fields.single() + } + } else if (instanceType is EtsUnclearRefType) { + val classes = ctx.scene.projectAndSdkClasses.filter { it.name == instanceType.name } + if (classes.size == 1) { + val clazz = classes.single() + return clazz.fields.single { it.name == field.name } + } + val fields = classes.flatMap { it.fields.filter { it.name == field.name } } + if (fields.size == 1) { + return fields.single() + } } else { val fields = ctx.scene.projectAndSdkClasses.flatMap { it.fields.filter { it.name == field.name } } - if (fields.size == 1) return fields.single() + if (fields.size == 1) { + return fields.single() + } } error("Cannot resolve field $field") } @@ -599,18 +649,59 @@ class TsExprResolver( // 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) + val lengthLValue = mkArrayLengthLValue(instanceRef, value.instance.type as EtsArrayType) + val length = scope.calcOnState { memory.read(lengthLValue) } + return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), length.asExpr(sizeSort), signed = true) + } - return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), expr.asExpr(sizeSort), signed = true) + // TODO: handle "length" property for arrays inside fake objects + if (value.field.name == "length" && instanceRef.isFakeObject()) { + val fakeType = scope.calcOnState { + memory.types.getTypeStream(instanceRef).single() as FakeType + } + if (fakeType.refTypeExpr.isTrue) { + val refLValue = getIntermediateRefLValue(instanceRef.address) + val obj = scope.calcOnState { memory.read(refLValue) } + // TODO: fix array type. It should be the same as the type used when "writing" the length. + // However, current value.instance typically has 'unknown' type, and the best we can do here is + // to pretend that this is an array-like object (with "array length", not just "length" field), + // and "cast" instance to "unknown[]". The same could be done for any length writes, making + // the array type (for length) consistent (unknown everywhere), but less precise. + val lengthLValue = mkArrayLengthLValue(obj, EtsArrayType(EtsUnknownType, 1)) + val length = scope.calcOnState { memory.read(lengthLValue) } + return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), length.asExpr(sizeSort), signed = true) + } } val field = resolveInstanceField(value.instance, value.field) val sort = typeToSort(field.type) - val lValue = UFieldLValue(sort, instanceRef, value.field.name) - val expr = scope.calcOnState { memory.read(lValue) } + + val expr = if (sort == unresolvedSort) { + val boolLValue = mkFieldLValue(boolSort, instanceRef, value.field) + val fpLValue = mkFieldLValue(fp64Sort, instanceRef, value.field) + val refLValue = mkFieldLValue(addressSort, instanceRef, value.field) + + scope.calcOnState { + val bool = memory.read(boolLValue) + val fp = memory.read(fpLValue) + val ref = memory.read(refLValue) + + // If a fake object is already created and assigned to the field, + // there is no need to recreate another one + val fakeRef = if (ref.isFakeObject()) { + ref + } else { + mkFakeValue(scope, bool, fp, ref) + } + + memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr) + + fakeRef + } + } else { + val lValue = mkFieldLValue(sort, instanceRef, value.field) + scope.calcOnState { memory.read(lValue) } + } if (assertIsSubtype(expr, value.type)) { expr @@ -706,20 +797,20 @@ class TsSimpleValueResolver( // If we are not in the entrypoint, all correct values are already resolved and we can just return // a registerStackLValue for the local if (currentMethod != entrypoint) { - return URegisterStackLValue(sort, localIdx) + return mkRegisterStackLValue(sort, localIdx) } // arguments and this for the first stack frame return when (sort) { - is UBoolSort -> URegisterStackLValue(sort, localIdx) - is KFp64Sort -> URegisterStackLValue(sort, localIdx) - is UAddressSort -> URegisterStackLValue(sort, localIdx) + is UBoolSort -> mkRegisterStackLValue(sort, localIdx) + is KFp64Sort -> mkRegisterStackLValue(sort, localIdx) + is UAddressSort -> mkRegisterStackLValue(sort, localIdx) is TsUnresolvedSort -> { check(local is EtsThis || local is EtsParameterRef) { "Only This and ParameterRef are expected here" } - val lValue = URegisterStackLValue(ctx.addressSort, localIdx) + val lValue = mkRegisterStackLValue(ctx.addressSort, localIdx) val boolRValue = ctx.mkRegisterReading(localIdx, ctx.boolSort) val fpRValue = ctx.mkRegisterReading(localIdx, ctx.fp64Sort) @@ -728,15 +819,6 @@ class TsSimpleValueResolver( val fakeObject = ctx.mkFakeValue(scope, boolRValue, fpRValue, refRValue) scope.calcOnState { with(ctx) { - val type = FakeType( - boolTypeExpr = makeSymbolicPrimitive(boolSort), - fpTypeExpr = makeSymbolicPrimitive(boolSort), - refTypeExpr = makeSymbolicPrimitive(boolSort) - ) - - scope.assert(type.mkExactlyOneTypeConstraint(ctx)) - - memory.types.allocate(fakeObject.address, type) memory.write(lValue, fakeObject.asExpr(addressSort), guard = trueExpr) } } @@ -749,6 +831,13 @@ class TsSimpleValueResolver( } override fun visit(value: EtsLocal): UExpr { + if (value.name == "NaN") { + return ctx.mkFp64NaN() + } + if (value.name == "Infinity") { + return ctx.mkFpInf(false, ctx.fp64Sort) + } + val lValue = resolveLocal(value) return scope.calcOnState { memory.read(lValue) } } 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 dd1869823..cc9d109d4 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 @@ -58,5 +58,9 @@ fun UExpr.extractBool(): Boolean = when (this) { fun extractInt(expr: UExpr): Int = (expr as? KBitVec32Value)?.intValue ?: error("Cannot extract int from $expr") -fun extractDouble(expr: UExpr): Double = - (expr as? KFp64Value)?.value ?: error("Cannot extract double from $expr") +fun UExpr.extractDouble(): Double { + if (this@extractDouble is KFp64Value) { + return value + } + error("Cannot extract double from $this") +} 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 56b52981c..e27ef8511 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 @@ -1,12 +1,13 @@ package org.usvm.machine.interpreter import io.ksmt.utils.asExpr -import mu.KotlinLogging import org.jacodb.ets.base.EtsArrayAccess +import org.jacodb.ets.base.EtsArrayType import org.jacodb.ets.base.EtsAssignStmt import org.jacodb.ets.base.EtsCallStmt import org.jacodb.ets.base.EtsGotoStmt import org.jacodb.ets.base.EtsIfStmt +import org.jacodb.ets.base.EtsInstanceFieldRef import org.jacodb.ets.base.EtsLocal import org.jacodb.ets.base.EtsNopStmt import org.jacodb.ets.base.EtsNullType @@ -23,8 +24,6 @@ import org.usvm.StepResult 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,13 +37,14 @@ import org.usvm.machine.state.localsCount 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.util.mkArrayIndexLValue +import org.usvm.util.mkArrayLengthLValue +import org.usvm.util.mkFieldLValue +import org.usvm.util.mkRegisterStackLValue import org.usvm.utils.ensureSat -private val logger = KotlinLogging.logger {} - typealias TsStepScope = StepScope @Suppress("UNUSED_PARAMETER") @@ -139,7 +139,7 @@ class TsInterpreter( val idx = mapLocalToIdx(lastEnteredMethod, lhv) saveSortForLocal(idx, expr.sort) - val lValue = URegisterStackLValue(expr.sort, idx) + val lValue = mkRegisterStackLValue(expr.sort, idx) memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr) } @@ -155,8 +155,10 @@ class TsInterpreter( isSigned = true ).asExpr(sizeSort) - val lengthLValue = UArrayLengthLValue(instance, lhv.array.type, sizeSort) - val currentLength = memory.read(lengthLValue).asExpr(sizeSort) + // TODO: handle the case when `lhv.array.type` is NOT an array. + // In this case, it could be created manually: `EtsArrayType(EtsUnknownType, 1)`. + val lengthLValue = mkArrayLengthLValue(instance, lhv.array.type as EtsArrayType) + val currentLength = memory.read(lengthLValue) val condition = mkBvSignedGreaterOrEqualExpr(bvIndex, currentLength) val newLength = mkIte(condition, mkBvAddExpr(bvIndex, mkBv(1)), currentLength) @@ -165,10 +167,29 @@ class TsInterpreter( val fakeExpr = expr.toFakeObject(scope) - val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, lhv.array.type) + val lValue = mkArrayIndexLValue( + addressSort, + instance, + bvIndex.asExpr(sizeSort), + lhv.array.type as EtsArrayType + ) memory.write(lValue, fakeExpr, guard = trueExpr) } + is EtsInstanceFieldRef -> { + val instance = exprResolver.resolve(lhv.instance)?.asExpr(addressSort) ?: return@doWithState + + val sort = typeToSort(lhv.type) + if (sort == unresolvedSort) { + val fakeObject = expr.toFakeObject(scope) + val lValue = mkFieldLValue(addressSort, instance, lhv.field) + memory.write(lValue, fakeObject, guard = trueExpr) + } else { + val lValue = mkFieldLValue(sort, instance, lhv.field) + memory.write(lValue, expr.asExpr(sort), guard = trueExpr) + } + } + else -> TODO("Not yet implemented") } @@ -239,7 +260,8 @@ class TsInterpreter( val solver = ctx.solver() - val thisInstanceRef = URegisterStackLValue(ctx.addressSort, method.parameters.count()) // TODO check for statics + // TODO check for statics + val thisInstanceRef = mkRegisterStackLValue(ctx.addressSort, method.parameters.count()) val thisRef = state.memory.read(thisInstanceRef).asExpr(ctx.addressSort) state.pathConstraints += with(ctx) { 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 b114efb70..048d18cbf 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 @@ -11,6 +11,7 @@ import org.usvm.api.makeSymbolicPrimitive import org.usvm.api.typeStreamOf import org.usvm.machine.TsContext import org.usvm.machine.expr.TsUndefinedSort +import org.usvm.machine.expr.mkNumericExpr import org.usvm.machine.expr.mkTruthyExpr import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.ExprWithTypeConstraint @@ -56,21 +57,24 @@ sealed interface TsBinaryOperator { rhs: UExpr, scope: TsStepScope, ): UExpr { - if (lhs.isFakeObject() || rhs.isFakeObject()) { - return resolveFakeObject(lhs, rhs, scope) + val lhsValue = lhs.extractSingleValueFromFakeObjectOrNull(scope) ?: lhs + val rhsValue = rhs.extractSingleValueFromFakeObjectOrNull(scope) ?: rhs + + if (lhsValue.isFakeObject() || rhsValue.isFakeObject()) { + return resolveFakeObject(lhsValue, rhsValue, scope) } - val lhsSort = lhs.sort - if (lhsSort == rhs.sort) { + val lhsSort = lhsValue.sort + if (lhsSort == rhsValue.sort) { return when (lhsSort) { - boolSort -> onBool(lhs.asExpr(boolSort), rhs.asExpr(boolSort), scope) - fp64Sort -> onFp(lhs.asExpr(fp64Sort), rhs.asExpr(fp64Sort), scope) - addressSort -> onRef(lhs.asExpr(addressSort), rhs.asExpr(addressSort), scope) + boolSort -> onBool(lhsValue.asExpr(boolSort), rhsValue.asExpr(boolSort), scope) + fp64Sort -> onFp(lhsValue.asExpr(fp64Sort), rhsValue.asExpr(fp64Sort), scope) + addressSort -> onRef(lhsValue.asExpr(addressSort), rhsValue.asExpr(addressSort), scope) else -> TODO("Unsupported sort $lhsSort") } } - return internalResolve(lhs, rhs, scope) + return internalResolve(lhsValue, rhsValue, scope) } data object Eq : TsBinaryOperator { @@ -412,7 +416,7 @@ sealed interface TsBinaryOperator { rhs: UExpr, scope: TsStepScope, ): UExpr { - TODO("Not yet implemented") + return mkHeapRefEq(lhs, rhs) } override fun TsContext.resolveFakeObject( @@ -785,4 +789,56 @@ sealed interface TsBinaryOperator { TODO("Not yet implemented") } } + + data object Mul : TsBinaryOperator { + override fun TsContext.onBool( + lhs: UExpr, + rhs: UExpr, + scope: TsStepScope, + ): UExpr { + val left = mkNumericExpr(lhs, scope) + val right = mkNumericExpr(rhs, scope) + return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right) + } + + override fun TsContext.onFp( + lhs: UExpr, + rhs: UExpr, + scope: TsStepScope, + ): UExpr { + return mkFpMulExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) + } + + override fun TsContext.onRef( + lhs: UExpr, + rhs: UExpr, + scope: TsStepScope, + ): UExpr { + val left = mkNumericExpr(lhs, scope) + val right = mkNumericExpr(rhs, scope) + return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right) + } + + override fun TsContext.resolveFakeObject( + lhs: UExpr, + rhs: UExpr, + scope: TsStepScope, + ): UExpr { + check(lhs.isFakeObject() || rhs.isFakeObject()) + val left = mkNumericExpr(lhs, scope) + val right = mkNumericExpr(rhs, scope) + return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right) + } + + override fun TsContext.internalResolve( + lhs: UExpr, + rhs: UExpr, + scope: TsStepScope, + ): UExpr { + check(!lhs.isFakeObject() && !rhs.isFakeObject()) + val left = mkNumericExpr(lhs, scope) + val right = mkNumericExpr(rhs, scope) + return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right) + } + } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt index 62ee89f22..cf34fc2fb 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt @@ -2,6 +2,7 @@ package org.usvm.machine.state import org.jacodb.ets.base.EtsStmt import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.utils.getDeclaredLocals import org.usvm.UExpr import org.usvm.USort @@ -30,4 +31,4 @@ inline val EtsMethod.parametersWithThisCount: Int get() = parameters.size + 1 inline val EtsMethod.localsCount: Int - get() = locals.size + get() = getDeclaredLocals().size diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt index 4f42e7602..cb26e5633 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt @@ -7,6 +7,7 @@ import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort +import org.usvm.api.makeSymbolicPrimitive import org.usvm.api.typeStreamOf import org.usvm.collection.field.UFieldLValue import org.usvm.machine.IntermediateLValueField @@ -30,12 +31,23 @@ fun TsContext.mkFakeValue( val fakeValueRef = createFakeObjectRef() val address = fakeValueRef.address + val boolTypeExpr = trueExpr + .takeIf { boolValue != null && fpValue == null && refValue == null } + ?: makeSymbolicPrimitive(boolSort) + val fpTypeExpr = trueExpr + .takeIf { boolValue == null && fpValue != null && refValue == null } + ?: makeSymbolicPrimitive(boolSort) + val refTypeExpr = trueExpr + .takeIf { boolValue == null && fpValue == null && refValue != null } + ?: makeSymbolicPrimitive(boolSort) + val type = FakeType( - boolTypeExpr = mkBool(boolValue != null), - fpTypeExpr = mkBool(fpValue != null), - refTypeExpr = mkBool(refValue != null), + boolTypeExpr = boolTypeExpr, + fpTypeExpr = fpTypeExpr, + refTypeExpr = refTypeExpr, ) memory.types.allocate(address, type) + scope.assert(type.mkExactlyOneTypeConstraint(ctx)) if (boolValue != null) { val boolLValue = ctx.getIntermediateBoolLValue(address) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt new file mode 100644 index 000000000..08c33868f --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt @@ -0,0 +1,44 @@ +package org.usvm.util + +import org.jacodb.ets.base.EtsArrayType +import org.jacodb.ets.model.EtsFieldSignature +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.USort +import org.usvm.collection.array.UArrayIndexLValue +import org.usvm.collection.array.length.UArrayLengthLValue +import org.usvm.collection.field.UFieldLValue +import org.usvm.machine.IntermediateLValueField +import org.usvm.machine.TsSizeSort +import org.usvm.machine.expr.tctx +import org.usvm.memory.URegisterStackLValue +import org.usvm.sizeSort + +fun mkFieldLValue( + sort: Sort, + ref: UHeapRef, + field: IntermediateLValueField, +): UFieldLValue = UFieldLValue(sort, ref, field) + +fun mkFieldLValue( + sort: Sort, + ref: UHeapRef, + field: EtsFieldSignature, +): UFieldLValue = UFieldLValue(sort, ref, field.name) + +fun mkArrayIndexLValue( + sort: Sort, + ref: UHeapRef, + index: UExpr, + type: EtsArrayType, +): UArrayIndexLValue = UArrayIndexLValue(sort, ref, index, type) + +fun mkArrayLengthLValue( + ref: UHeapRef, + type: EtsArrayType, +): UArrayLengthLValue = UArrayLengthLValue(ref, type, ref.tctx.sizeSort) + +fun mkRegisterStackLValue( + sort: Sort, + idx: Int, +): URegisterStackLValue = URegisterStackLValue(sort, idx) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt new file mode 100644 index 000000000..3416e9b5d --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt @@ -0,0 +1,123 @@ +package org.usvm.samples + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Disabled +import org.usvm.api.TsValue +import org.usvm.util.TsMethodTestRunner +import kotlin.test.Test + +class FieldAccess : TsMethodTestRunner() { + + private val className = this::class.simpleName!! + + override val scene: EtsScene = loadSampleScene(className) + + @Test + fun `test readDefaultField`() { + val method = getMethod(className, "readDefaultField") + discoverProperties( + method = method, + { r -> r.number == 5.0 }, + ) + } + + @Test + fun `test writeAndReadNumeric`() { + val method = getMethod(className, "writeAndReadNumeric") + discoverProperties( + method = method, + { r -> r.number == 14.0 }, + ) + } + + @Test + fun `test writeDifferentTypes`() { + val method = getMethod(className, "writeDifferentTypes") + discoverProperties( + method = method, + { r -> r.number == 5.0 }, + ) + } + + @Test + fun `test handleNumericEdges`() { + val method = getMethod(className, "handleNumericEdges") + discoverProperties( + method = method, + { r -> r.number == 1.0 }, + ) + } + + @Test + fun `test createWithField`() { + val method = getMethod(className, "createWithField") + discoverProperties( + method = method, + { r -> r.number == 15.0 }, + ) + } + + @Disabled("Return types are not propagated to locals, need type stream") + @Test + fun `test factoryCreatedObject`() { + val method = getMethod(className, "factoryCreatedObject") + discoverProperties( + method = method, + { r -> r.number == 42.0 }, + ) + } + + @Test + fun `test conditionalFieldAccess`() { + val method = getMethod(className, "conditionalFieldAccess") + discoverProperties( + method = method, + { a, r -> + val x = a.properties["x"] as TsValue.TsNumber + x.number == 1.1 && r.number == 14.0 + }, + { a, r -> + val x = a.properties["x"] as TsValue.TsNumber + x.number != 1.1 && r.number == 10.0 + }, + ) + } + + @Disabled("Nested field types are not propagated to locals, need type stream") + @Test + fun `test nestedFieldAccess`() { + val method = getMethod(className, "nestedFieldAccess") + discoverProperties( + method = method, + { r -> r.number == 7.0 }, + ) + } + + @Disabled("Nested arrays inside objects are accessed via field properties ('.1') instead of indices ([1])") + @Test + fun `test arrayFieldAccess`() { + val method = getMethod(className, "arrayFieldAccess") + discoverProperties( + method = method, + { r -> r.number == 5.0 }, + ) + } + + @Test + fun `test multipleFieldInteraction`() { + val method = getMethod(className, "multipleFieldInteraction") + discoverProperties( + method = method, + { r -> r.number == 9.0 }, // (2*2=4) + (4+1=5) == 9 + ) + } + + @Test + fun `test circularTypeChanges`() { + val method = getMethod(className, "circularTypeChanges") + discoverProperties( + method = method, + { r -> r.number == 1.0 }, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/ObjectClass.kt b/usvm-ts/src/test/kotlin/org/usvm/util/ObjectClass.kt new file mode 100644 index 000000000..9bb0f4698 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/util/ObjectClass.kt @@ -0,0 +1,27 @@ +package org.usvm.util + +import org.jacodb.ets.base.CONSTRUCTOR_NAME +import org.jacodb.ets.base.EtsClassType +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassImpl +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsMethodImpl +import org.jacodb.ets.model.EtsMethodSignature + +fun createObjectClass(): EtsClass { + val cls = EtsClassSignature("Object", EtsFileSignature.DEFAULT) + return EtsClassImpl( + signature = cls, + fields = emptyList(), + methods = emptyList(), + ctor = EtsMethodImpl( + EtsMethodSignature( + enclosingClass = cls, + name = CONSTRUCTOR_NAME, + parameters = emptyList(), + returnType = EtsClassType(cls), + ) + ), + ) +} 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 f5bc1209b..a684eaab6 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -2,7 +2,6 @@ package org.usvm.util import io.ksmt.expr.KBitVec32Value import io.ksmt.utils.asExpr -import org.jacodb.ets.base.CONSTRUCTOR_NAME import org.jacodb.ets.base.EtsArrayType import org.jacodb.ets.base.EtsBooleanType import org.jacodb.ets.base.EtsClassType @@ -14,17 +13,17 @@ import org.jacodb.ets.base.EtsPrimitiveType import org.jacodb.ets.base.EtsRefType import org.jacodb.ets.base.EtsStringType import org.jacodb.ets.base.EtsType +import org.jacodb.ets.base.EtsUnclearRefType import org.jacodb.ets.base.EtsUndefinedType import org.jacodb.ets.base.EtsUnknownType import org.jacodb.ets.base.EtsVoidType +import org.jacodb.ets.base.UNKNOWN_CLASS_NAME import org.jacodb.ets.model.EtsClass -import org.jacodb.ets.model.EtsClassImpl import org.jacodb.ets.model.EtsMethod -import org.jacodb.ets.model.EtsMethodImpl -import org.jacodb.ets.model.EtsMethodSignature import org.usvm.UAddressSort import org.usvm.UConcreteHeapRef import org.usvm.UExpr +import org.usvm.UHeapRef import org.usvm.USort import org.usvm.api.GlobalFieldValue import org.usvm.api.TsParametersState @@ -38,7 +37,6 @@ 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.tctx import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.machine.types.FakeType @@ -66,7 +64,7 @@ class TsTestResolver { is TsMethodResult.Success -> { afterMemoryScope.withMode(ResolveMode.CURRENT) { - resolveExpr(res.value, method.returnType) + resolveExpr(res.value, res.value, method.returnType) } } @@ -115,64 +113,112 @@ open class TsTestStateResolver( ) { fun resolveLValue(lValue: ULValue<*, *>, type: EtsType): TsValue { val expr = memory.read(lValue) - return resolveExpr(expr, type) + val symbolicRef = if (lValue.sort == ctx.addressSort) { + finalStateMemory.read(lValue).asExpr(ctx.addressSort) + } else { + null + } + return resolveExpr(expr, symbolicRef, type) } fun resolveExpr( expr: UExpr, + symbolicRef: UExpr? = null, type: EtsType, ): TsValue = when (type) { - is EtsPrimitiveType -> resolvePrimitive(expr, type) - is EtsRefType -> resolveRef(expr.asExpr(ctx.addressSort), type) - else -> resolveUnknownExpr(expr) + is EtsPrimitiveType -> { + resolvePrimitive(expr, type) + } + + is EtsRefType -> { + val finalStateMemoryRef = symbolicRef?.asExpr(ctx.addressSort) ?: expr.asExpr(ctx.addressSort) + resolveTsValue(expr.asExpr(ctx.addressSort), finalStateMemoryRef, type) + } + + else -> { + resolveUnknownExpr(expr, symbolicRef) + } } - fun resolveUnknownExpr(expr: UExpr): TsValue = with(expr.tctx) { - when (expr.sort) { - fp64Sort -> resolvePrimitive(expr, EtsNumberType) - boolSort -> resolvePrimitive(expr, EtsBooleanType) + fun resolveUnknownExpr( + heapRef: UExpr, + finalStateMemoryRef: UExpr?, + ): TsValue = with(ctx) { + when (heapRef.sort) { + fp64Sort -> { + resolvePrimitive(heapRef, EtsNumberType) + } + + boolSort -> { + resolvePrimitive(heapRef, EtsBooleanType) + } + addressSort -> { - if (expr.isFakeObject()) { - resolveFakeObject(expr) + if (heapRef.isFakeObject()) { + resolveFakeObject(heapRef) } else { - resolveRef(expr.asExpr(ctx.addressSort), EtsUnknownType) + resolveTsValue( + heapRef.asExpr(ctx.addressSort), + finalStateMemoryRef?.asExpr(ctx.addressSort), + EtsUnknownType + ) } } - else -> TODO() + else -> TODO("Unsupported sort: ${heapRef.sort}") } } - private fun resolveRef(expr: UExpr, type: EtsType): TsValue { - val instance = model.eval(expr) as UConcreteHeapRef + private fun resolveTsValue( + heapRef: UExpr, + finalStateMemoryRef: UExpr?, + type: EtsType, + ): TsValue { + val concreteRef = evaluateInModel(heapRef) as UConcreteHeapRef - if (instance.address == 0) { + if (concreteRef.address == 0) { return TsValue.TsUndefined } - if (model.eval(ctx.mkHeapRefEq(expr, ctx.mkTsNullValue())).isTrue) { + if (model.eval(ctx.mkHeapRefEq(heapRef, ctx.mkTsNullValue())).isTrue) { return TsValue.TsNull } return when (type) { - is EtsClassType -> resolveClass(instance, type) - is EtsArrayType -> resolveArray(instance, type) + // TODO add better support + is EtsUnclearRefType -> { + val classType = ctx.scene.projectAndSdkClasses.single { it.name == type.name } + resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef, EtsClassType(classType.signature)) + } + + is EtsClassType -> { + resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef, type) + } + + is EtsArrayType -> { + resolveTsArray(concreteRef, finalStateMemoryRef ?: heapRef, type) + } + is EtsUnknownType -> { - val type = finalStateMemory.types.getTypeStream(expr).first() - resolveRef(expr, type) + val finalType = finalStateMemory.types.getTypeStream(heapRef).first() + resolveTsValue(heapRef, finalStateMemoryRef, finalType) } else -> error("Unexpected type: $type") } } - private fun resolveArray(expr: UConcreteHeapRef, type: EtsArrayType): TsValue.TsArray<*> { - val arrayLengthLValue = UArrayLengthLValue(expr, type, ctx.sizeSort) + private fun resolveTsArray( + concreteRef: UConcreteHeapRef, + heapRef: UHeapRef, + type: EtsArrayType, + ): TsValue.TsArray<*> { + val arrayLengthLValue = UArrayLengthLValue(heapRef, type, ctx.sizeSort) val length = model.eval(memory.read(arrayLengthLValue)) as KBitVec32Value val values = (0 until length.intValue).map { val index = ctx.mkSizeExpr(it) - val lValue = UArrayIndexLValue(ctx.addressSort, expr, index, type) + val lValue = UArrayIndexLValue(ctx.addressSort, heapRef, index, type) val value = memory.read(lValue) if (model.eval(ctx.mkHeapRefEq(value, ctx.mkUndefinedValue())).isTrue) { @@ -223,7 +269,7 @@ open class TsTestStateResolver( // Note that everything about details of fake object we need to read from final state of the memory // since they are allocated objects val value = finalStateMemory.read(lValue) - resolveExpr(model.eval(value), EtsBooleanType) + resolveExpr(model.eval(value), value, EtsBooleanType) } model.eval(type.fpTypeExpr).isTrue -> { @@ -231,7 +277,7 @@ open class TsTestStateResolver( // Note that everything about details of fake object we need to read from final state of the memory // since they are allocated objects val value = finalStateMemory.read(lValue) - resolveExpr(model.eval(value), EtsNumberType) + resolveExpr(model.eval(value), value, EtsNumberType) } model.eval(type.refTypeExpr).isTrue -> { @@ -241,7 +287,7 @@ open class TsTestStateResolver( val value = finalStateMemory.read(lValue) val ref = model.eval(value) // TODO mistake with signature, use TypeStream instead - resolveExpr(ref, EtsClassType(ctx.scene.projectAndSdkClasses.first().signature)) + resolveExpr(ref, value, EtsClassType(ctx.scene.projectAndSdkClasses.first().signature)) } else -> error("Unsupported") @@ -251,59 +297,80 @@ open class TsTestStateResolver( private fun resolvePrimitive( expr: UExpr, type: EtsPrimitiveType, - ): TsValue = when (type) { - EtsNumberType -> TsValue.TsNumber.TsDouble(extractDouble(evaluateInModel(expr))) - EtsBooleanType -> TsValue.TsBoolean(evaluateInModel(expr).extractBool()) - EtsUndefinedType -> TsValue.TsUndefined - is EtsLiteralType -> TODO() - EtsNullType -> TODO() - EtsNeverType -> TODO() - EtsStringType -> TODO() - EtsVoidType -> TODO() - else -> error("Unexpected type: $type") + ): TsValue = with(ctx) { + when (type) { + EtsNumberType -> { + val e = evaluateInModel(expr) + if (e.isFakeObject()) { + val lValue = getIntermediateFpLValue(e.address) + val value = finalStateMemory.read(lValue) + resolveExpr(model.eval(value), value, EtsNumberType) + } else { + TsValue.TsNumber.TsDouble(e.extractDouble()) + } + } + + EtsBooleanType -> TsValue.TsBoolean(evaluateInModel(expr).extractBool()) + EtsUndefinedType -> TsValue.TsUndefined + is EtsLiteralType -> TODO() + EtsNullType -> TODO() + EtsNeverType -> TODO() + EtsStringType -> TODO() + EtsVoidType -> TODO() + else -> error("Unexpected type: $type") + } } private fun resolveClass( - expr: UExpr, classType: EtsClassType, - ): TsValue { - if (expr is UConcreteHeapRef && expr.address == 0) { - return TsValue.TsUndefined + ): EtsClass { + // Special case for Object: + if (classType.signature.name == "Object") { + return createObjectClass() } - val nullRef = ctx.mkTsNullValue() - if (model.eval(ctx.mkHeapRefEq(expr.asExpr(ctx.addressSort), nullRef)).isTrue) { - return TsValue.TsNull + // Perfect signature: + if (classType.signature.name != UNKNOWN_CLASS_NAME) { + val classes = ctx.scene.projectAndSdkClasses.filter { it.signature == classType.signature } + if (classes.size == 1) { + return classes.single() + } } - check(expr.sort == ctx.addressSort) { - "Expected address sort, but got ${expr.sort}" + // Sad signature: + val classes = ctx.scene.projectAndSdkClasses.filter { it.signature.name == classType.signature.name } + if (classes.size == 1) { + return classes.single() } - val clazz = ctx.scene.projectAndSdkClasses.firstOrNull { it.signature == classType.signature } - ?: if (classType.signature.name == "Object") { - EtsClassImpl( - signature = classType.signature, - fields = emptyList(), - methods = emptyList(), - ctor = EtsMethodImpl( - EtsMethodSignature( - enclosingClass = classType.signature, - name = CONSTRUCTOR_NAME, - parameters = emptyList(), - returnType = classType, - ) - ), - ) - } else { - error("Class not found: ${classType.signature}") - } + error("Could not resolve class: ${classType.signature}") + } + + private fun resolveTsClass( + concreteRef: UConcreteHeapRef, + heapRef: UHeapRef, + classType: EtsClassType, + ): TsValue.TsClass { + val clazz = resolveClass(classType) val properties = clazz.fields.associate { field -> val sort = ctx.typeToSort(field.type) - val lValue = UFieldLValue(sort, expr.asExpr(ctx.addressSort), field.name) + + if (sort == ctx.unresolvedSort) { + val lValue = UFieldLValue(ctx.addressSort, heapRef, field.name) + val fieldExpr = finalStateMemory.read(lValue) as? UConcreteHeapRef + ?: error("UnresolvedSort should be represented by a fake object instance") + + // TODO check values if fieldExpr is correct here + // Probably we have to pass fieldExpr as symbolic value and something as a concrete one + return@associate field.name to resolveExpr(fieldExpr, fieldExpr, field.type) + } + + val lValue = UFieldLValue(sort, concreteRef.asExpr(ctx.addressSort), field.name) val fieldExpr = memory.read(lValue) - val obj = resolveExpr(fieldExpr, field.type) + // TODO check values if fieldExpr is correct here + // Probably we have to pass fieldExpr as symbolic value and something as a concrete one + val obj = resolveExpr(fieldExpr, fieldExpr, field.type) field.name to obj } return TsValue.TsClass(clazz.name, properties) diff --git a/usvm-ts/src/test/resources/samples/FieldAccess.ts b/usvm-ts/src/test/resources/samples/FieldAccess.ts new file mode 100644 index 000000000..f4acd6377 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/FieldAccess.ts @@ -0,0 +1,92 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class SimpleClass { + x: any = 5; +} + +class MultiFieldClass { + a = 1; + b = 2; +} + +class FieldAccess { + readDefaultField(): number { + const obj = new SimpleClass(); + return obj.x; + } + + writeAndReadNumeric(): number { + const obj = new SimpleClass(); + obj.x = 14; + return obj.x; + } + + writeDifferentTypes(): number { + const obj = new SimpleClass(); + obj.x = true; + if (obj.x === true) { + obj.x = undefined; + } + if (obj.x === undefined) { + obj.x = null; + } + if (obj.x === null) { + obj.x = 5; + } + return obj.x; + } + + handleNumericEdges(): number { + const obj = new SimpleClass(); + obj.x = NaN; + if (Number.isNaN(obj.x)) { + obj.x = Infinity; + } + return (obj.x === Infinity) ? 1 : 0; + } + + createWithField(): number { + return {a: 15}.a; + } + + factoryCreatedObject(): number { + return this.createObject().x; + } + + private createObject(): {x: number} { + return {x: 42}; + } + + conditionalFieldAccess(a: SimpleClass): number { + if (a.x === 1.1) return 14; + return 10; + } + + nestedFieldAccess(): number { + const obj = {inner: new SimpleClass()}; + obj.inner.x = 7; + return obj.inner.x; + } + + arrayFieldAccess(): number { + const obj = {arr: [7, 3, 6]}; + obj.arr[1] = 5; + return obj.arr[1]; + } + + multipleFieldInteraction(): number { + const obj = new MultiFieldClass(); + obj.a = obj.b * 2; + obj.b = obj.a + 1; + return obj.a + obj.b; + } + + circularTypeChanges(): number { + const obj = new SimpleClass(); + obj.x = {value: 5}; + obj.x = obj.x.value; + obj.x = [obj.x]; + return obj.x.length; + } +}