From 4aa9d64e9ca4b57d32db8fe6f68878113a40b480 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 19 Feb 2025 16:58:54 +0300 Subject: [PATCH] Debug commit --- .../org/usvm/machine/expr/TsExprResolver.kt | 11 ++++++++-- .../usvm/machine/interpreter/TsInterpreter.kt | 4 +++- .../org/usvm/machine/types/AuxiliaryType.kt | 17 +++++++++++++++ .../kotlin/org/usvm/util/TsTestResolver.kt | 21 ++++++++++++------- 4 files changed, 43 insertions(+), 10 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt 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 a28ce6b38..041e9a2d5 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 @@ -546,11 +546,18 @@ class TsExprResolver( checkUndefinedOrNullPropertyRead(instanceRef) ?: return null // TODO: checkNullPointer(instanceRef) - val lValue = UFieldLValue(addressSort, instanceRef, value.field) + val fieldType = scene.fieldLookUp(value.field).type + val sort = typeToSort(fieldType) + val lValue = UFieldLValue(sort, instanceRef, value.field.name) val expr = scope.calcOnState { memory.read(lValue) } + val fakeExpr = expr.toFakeObject(scope) + + val fieldLValue = UFieldLValue(addressSort, instanceRef, value.field.name) + scope.calcOnState { memory.write(fieldLValue, fakeExpr, guard = trueExpr) } + if (assertIsSubtype(expr, value.type)) { - expr + fakeExpr } else { null } 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 da1a50302..343acd921 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 @@ -5,6 +5,7 @@ import mu.KotlinLogging import org.jacodb.ets.base.EtsArrayAccess import org.jacodb.ets.base.EtsAssignStmt import org.jacodb.ets.base.EtsCallStmt +import org.jacodb.ets.base.EtsClassType import org.jacodb.ets.base.EtsGotoStmt import org.jacodb.ets.base.EtsIfStmt import org.jacodb.ets.base.EtsInstanceFieldRef @@ -23,6 +24,7 @@ import org.jacodb.ets.model.EtsMethod import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UInterpreter +import org.usvm.api.evalTypeEquals import org.usvm.api.targets.TsTarget import org.usvm.collection.array.UArrayIndexLValue import org.usvm.collection.field.UFieldLValue @@ -171,7 +173,7 @@ class TsInterpreter( val instance = exprResolver.resolve(lhv.instance)?.asExpr(ctx.addressSort) ?: return@doWithState val exprValue = expr.toFakeObject(scope) - val lValue = UFieldLValue(addressSort, instance, lhv.field) + val lValue = UFieldLValue(addressSort, instance, lhv.field.name) memory.write(lValue, exprValue, guard = ctx.trueExpr) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt new file mode 100644 index 000000000..c93f77a57 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt @@ -0,0 +1,17 @@ +package org.usvm.machine.types + +import com.jetbrains.rd.framework.util.RdCoroutineScope.Companion.override +import org.jacodb.ets.base.EtsRefType +import org.jacodb.ets.base.EtsType +import org.jacodb.ets.model.EtsFieldSignature + +/** + * An artificial type that represents a set of properties. + */ +class AuxiliaryType(val properties: Set) : EtsRefType { + override val typeName: String = "AuxiliaryType" + + override fun accept(visitor: EtsType.Visitor): R { + error("Should not be called") + } +} \ No newline at end of file diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index eca8192fb..f19cd5084 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -121,10 +121,16 @@ open class TsTestStateResolver( fun resolveExpr( expr: UExpr, type: EtsType, - ): TsValue = when (type) { - is EtsPrimitiveType -> resolvePrimitive(expr, type) - is EtsRefType -> resolveRef(expr.asExpr(ctx.addressSort), type) - else -> resolveUnknownExpr(expr) + ): TsValue = with(ctx) { + if (expr.isFakeObject()) { + return resolveFakeObject(expr) + } + + return when (type) { + is EtsPrimitiveType -> resolvePrimitive(expr, type) + is EtsRefType -> resolveRef(expr.asExpr(ctx.addressSort), type) + else -> resolveUnknownExpr(expr) + } } fun resolveUnknownExpr(expr: UExpr): TsValue = with(expr.tctx) { @@ -298,11 +304,12 @@ open class TsTestStateResolver( } val properties = clazz.fields.associate { field -> - val lValue = UFieldLValue(ctx.addressSort, expr.asExpr(ctx.addressSort), field.signature) - val fieldExpr = memory.read(lValue) + val lValue = UFieldLValue(ctx.addressSort, expr.asExpr(ctx.addressSort), field.name) + // read from final state memory since it is a fake object + val fieldExpr = finalStateMemory.read(lValue) with(ctx) { - if (model.eval(mkHeapRefEq(fieldExpr, mkUndefinedValue())).isTrue) { + if (model.eval(mkEq(fieldExpr, mkUndefinedValue())).isTrue) { return@associate field.name to TsValue.TsUndefined }