From bf7d30f3c51ba3127dc50bcefc38c99738067506 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 19 Feb 2025 12:33:50 +0300 Subject: [PATCH 1/4] Constructors support --- .../org/usvm/machine/expr/TsExprResolver.kt | 26 +++++++++----- .../usvm/machine/interpreter/TsInterpreter.kt | 10 ++++++ .../test/kotlin/org/usvm/samples/Objects.kt | 35 +++++++++++++++++++ .../kotlin/org/usvm/util/TsTestResolver.kt | 15 +++++--- usvm-ts/src/test/resources/samples/Objects.ts | 17 +++++++++ 5 files changed, 90 insertions(+), 13 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt create mode 100644 usvm-ts/src/test/resources/samples/Objects.ts 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 107ade977..8d9fd9d80 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 @@ -407,16 +407,26 @@ class TsExprResolver( argumentTypes = { expr.method.parameters.map { it.type } }, ) { args -> doWithState { - val method = ctx.scene - .projectAndSdkClasses - .flatMap { it.methods } - .singleOrNull { it.signature == expr.method } - ?: error("Couldn't find a unique method with the signature ${expr.method}") + val method = if (expr.method.name == "constructor") { + ctx.scene + .projectAndSdkClasses + .map { it.ctor } + .singleOrNull { it.signature == expr.method } + ?: error("Couldn't find a unique constructor with the signature ${expr.method}") + } else { + ctx.scene + .projectAndSdkClasses + .flatMap { it.methods } + .singleOrNull { it.signature == expr.method } + ?: error("Couldn't find a unique method with the signature ${expr.method}") + } pushSortsForArguments(expr.instance, expr.args, localToIdx) callStack.push(method, currentStatement) - memory.stack.push(args.toTypedArray(), method.localsCount) + + val count = if (method.name == "%instInit") method.localsCount + 1 else method.localsCount + memory.stack.push(args.toTypedArray(), count) newStmt(method.cfg.stmts.first()) } @@ -548,9 +558,7 @@ class TsExprResolver( 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) + val lValue = UFieldLValue(addressSort, instanceRef, value.field) val expr = scope.calcOnState { memory.read(lValue) } if (assertIsSubtype(expr, value.type)) { 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..ae9cc2f32 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 @@ -7,6 +7,7 @@ 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 @@ -24,6 +25,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.field.UFieldLValue import org.usvm.collection.array.length.UArrayLengthLValue import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.forkblacklists.UForkBlackList @@ -169,6 +171,14 @@ class TsInterpreter( memory.write(lValue, fakeExpr, guard = trueExpr) } + is EtsInstanceFieldRef -> { + val instance = exprResolver.resolve(lhv.instance)?.asExpr(ctx.addressSort) ?: return@doWithState + val exprValue = expr.toFakeObject(scope) + + val lValue = UFieldLValue(addressSort, instance, lhv.field) + memory.write(lValue, exprValue, guard = ctx.trueExpr) + } + else -> TODO("Not yet implemented") } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt new file mode 100644 index 000000000..acc368798 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt @@ -0,0 +1,35 @@ +package org.usvm.samples + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.api.TsValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.getResourcePath +import kotlin.test.Test + +class Objects : TsMethodTestRunner() { + override val scene: EtsScene = run { + val name = "Objects.ts" + val path = getResourcePath("/samples/$name") + val file = loadEtsFileAutoConvert(path) + EtsScene(listOf(file)) + } + + @Test + fun testCreateClassInstance() { + val method = getMethod("Example", "createClassInstance") + discoverProperties( + method = method, + { r -> r.number == 5.0 } + ) + } + + @Test + fun testCreateClassInstanceAndWriteField() { + val method = getMethod("Example", "createClassInstanceAndWriteField") + discoverProperties( + method = method, + { r -> (r.properties.toList().single().second as TsValue.TsNumber).number == 14.0 } + ) + } +} \ 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 f5bc1209b..a623a4626 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -300,11 +300,18 @@ open class TsTestStateResolver( } val properties = clazz.fields.associate { field -> - val sort = ctx.typeToSort(field.type) - val lValue = UFieldLValue(sort, expr.asExpr(ctx.addressSort), field.name) + val lValue = UFieldLValue(ctx.addressSort, expr.asExpr(ctx.addressSort), field.signature) val fieldExpr = memory.read(lValue) - val obj = resolveExpr(fieldExpr, field.type) - field.name to obj + + with(ctx) { + if (model.eval(mkHeapRefEq(fieldExpr, mkUndefinedValue())).isTrue) { + return@associate field.name to TsValue.TsUndefined + } + + check(fieldExpr.isFakeObject()) + val obj = resolveFakeObject(fieldExpr) + field.name to obj + } } return TsValue.TsClass(clazz.name, properties) } diff --git a/usvm-ts/src/test/resources/samples/Objects.ts b/usvm-ts/src/test/resources/samples/Objects.ts new file mode 100644 index 000000000..446f1238e --- /dev/null +++ b/usvm-ts/src/test/resources/samples/Objects.ts @@ -0,0 +1,17 @@ +class SimpleClass { + x = 5; +} + +class Example { + createClassInstance() { + let x = new SimpleClass(); + return x.x; + } + + createClassInstanceAndWriteField() { + let x = new SimpleClass(); + x.x = 14; + + return x; + } +} \ No newline at end of file From b312b295d0495257d1440bf78079ccad8d37dd4d Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 19 Feb 2025 12:36:00 +0300 Subject: [PATCH 2/4] Add test with different types at the same field --- usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt | 9 +++++++++ usvm-ts/src/test/resources/samples/Objects.ts | 11 +++++++++++ 2 files changed, 20 insertions(+) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt index acc368798..7ad40fc74 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt @@ -32,4 +32,13 @@ class Objects : TsMethodTestRunner() { { r -> (r.properties.toList().single().second as TsValue.TsNumber).number == 14.0 } ) } + + @Test + fun testCreateClassInstanceAndWriteValueOfAnotherType() { + val method = getMethod("Example", "createClassInstanceAndWriteValueOfAnotherType") + discoverProperties( + method = method, + { r -> r.properties.toList().single().second is TsValue.TsNull } + ) + } } \ No newline at end of file diff --git a/usvm-ts/src/test/resources/samples/Objects.ts b/usvm-ts/src/test/resources/samples/Objects.ts index 446f1238e..a82de21f2 100644 --- a/usvm-ts/src/test/resources/samples/Objects.ts +++ b/usvm-ts/src/test/resources/samples/Objects.ts @@ -14,4 +14,15 @@ class Example { return x; } + + createClassInstanceAndWriteValueOfAnotherType() { + let x = new SimpleClass(); + x.x = true; + + if (x.x === true) { + x.x = null + } + + return x; + } } \ No newline at end of file From fcc0e0e8c79279e2b50082b137d77347a9badc26 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 19 Feb 2025 12:41:13 +0300 Subject: [PATCH 3/4] Add example of anonymous class --- usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt | 9 +++++++++ usvm-ts/src/test/resources/samples/Objects.ts | 4 ++++ 2 files changed, 13 insertions(+) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt index 7ad40fc74..8e873ecf3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt @@ -41,4 +41,13 @@ class Objects : TsMethodTestRunner() { { r -> r.properties.toList().single().second is TsValue.TsNull } ) } + + @Test + fun testCreateAnonymousClass() { + val method = getMethod("Example", "createAnonymousClass") + discoverProperties( + method = method, + { r -> (r.properties.toList().single().second as TsValue.TsNumber).number == 15.0 } + ) + } } \ No newline at end of file diff --git a/usvm-ts/src/test/resources/samples/Objects.ts b/usvm-ts/src/test/resources/samples/Objects.ts index a82de21f2..31a9333a0 100644 --- a/usvm-ts/src/test/resources/samples/Objects.ts +++ b/usvm-ts/src/test/resources/samples/Objects.ts @@ -25,4 +25,8 @@ class Example { return x; } + + createAnonymousClass() { + return { a : 15 }; + } } \ No newline at end of file From 271dfacf65ec579f75ff60482a914fb4c2c4829c Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 19 Feb 2025 16:58:54 +0300 Subject: [PATCH 4/4] 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 8d9fd9d80..d22cbd67d 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 @@ -558,11 +558,18 @@ class TsExprResolver( return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), expr.asExpr(sizeSort), signed = true) } - 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 ae9cc2f32..6f63e04a9 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 @@ -175,7 +177,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 a623a4626..cbdc7190b 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) { @@ -300,11 +306,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 }