From df9c1034c0180a057a1c2bd74510ed118d61f0d5 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 18 Feb 2025 11:24:20 +0300 Subject: [PATCH] Add support for arrays (#256) --------- Co-authored-by: Konstantin Chukharev --- .../src/main/kotlin/org/usvm/api/TsTest.kt | 4 +- .../main/kotlin/org/usvm/machine/TsContext.kt | 2 + .../org/usvm/machine/expr/TsExprResolver.kt | 63 ++++++++-- .../usvm/machine/interpreter/TsInterpreter.kt | 40 +++++- .../test/kotlin/org/usvm/samples/Arrays.kt | 106 ++++++++++++++++ .../test/kotlin/org/usvm/samples/MinValue.kt | 2 +- .../org/usvm/util/TsMethodTestRunner.kt | 10 +- .../kotlin/org/usvm/util/TsTestResolver.kt | 116 ++++++++++++------ usvm-ts/src/test/resources/samples/Arrays.ts | 43 +++++++ 9 files changed, 329 insertions(+), 57 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt create mode 100644 usvm-ts/src/test/resources/samples/Arrays.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt index 659e6efe1..9f1e936df 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt @@ -55,7 +55,7 @@ sealed interface TsValue { val properties: Map, ) : TsValue - data class TsArray( - val values: List, + data class TsArray( + val values: List, ) : TsValue } 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 2352089f9..3fb83282b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -7,6 +7,7 @@ import org.jacodb.ets.base.EtsNumberType import org.jacodb.ets.base.EtsRefType import org.jacodb.ets.base.EtsType import org.jacodb.ets.base.EtsUndefinedType +import org.jacodb.ets.base.EtsUnionType import org.jacodb.ets.base.EtsUnknownType import org.jacodb.ets.model.EtsScene import org.usvm.UAddressSort @@ -46,6 +47,7 @@ class TsContext( is EtsNullType -> addressSort is EtsUndefinedType -> addressSort is EtsUnknownType -> unresolvedSort + is EtsUnionType -> unresolvedSort else -> TODO("Support all JacoDB types, encountered $type") } 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 d2bcb5f92..a73e24ee6 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 @@ -63,6 +63,7 @@ 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 @@ -74,7 +75,9 @@ import org.usvm.UBoolSort 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.field.UFieldLValue import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope @@ -88,6 +91,7 @@ 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.util.fieldLookUp import org.usvm.util.throwExceptionWithoutStackFrameDrop @@ -494,8 +498,19 @@ class TsExprResolver( // region ACCESS override fun visit(value: EtsArrayAccess): UExpr? { - logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } - error("Not supported $value") + 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(), + 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) + + return scope.calcOnState { memory.read(lValue) } } private fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) { @@ -546,9 +561,42 @@ class TsExprResolver( memory.allocConcrete(expr.type) } - override fun visit(expr: EtsNewArrayExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsNewArrayExpr): UExpr? = with(ctx) { + scope.calcOnState { + val size = resolve(expr.size) ?: return@calcOnState null + + if (size.sort != fp64Sort) { + TODO() + } + + val bvSize = mkFpToBvExpr( + fpRoundingModeSortDefaultValue(), + size.asExpr(fp64Sort), + bvSize = 32, + isSigned = true + ) + + val condition = mkAnd( + mkEq( + mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), bvSize, signed = true), + size.asExpr(fp64Sort) + ), + mkAnd( + mkBvSignedLessOrEqualExpr(0.toBv(), bvSize.asExpr(bv32Sort)), + mkBvSignedLessOrEqualExpr(bvSize, Int.MAX_VALUE.toBv().asExpr(bv32Sort)) + ) + ) + + scope.fork( + condition, + blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type + ) + + val address = memory.allocateArray(expr.type, sizeSort, bvSize) + memory.types.allocate(address.address, expr.type) + + address + } } override fun visit(expr: EtsLengthExpr): UExpr? { @@ -665,9 +713,8 @@ class TsSimpleValueResolver( mkUndefinedValue() } - override fun visit(value: EtsArrayAccess): UExpr = with(ctx) { - logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } - error("Not supported $value") + override fun visit(value: EtsArrayAccess): UExpr? = with(ctx) { + error("Should not be called") } override fun visit(value: EtsInstanceFieldRef): UExpr = with(ctx) { 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 e0b5f9b22..b3ec5d025 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 @@ -2,6 +2,7 @@ package org.usvm.machine.interpreter import io.ksmt.utils.asExpr 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.EtsGotoStmt @@ -22,6 +23,7 @@ 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.collections.immutable.internal.MutabilityOwnership import org.usvm.forkblacklists.UForkBlackList import org.usvm.machine.TsApplicationGraph @@ -130,11 +132,41 @@ class TsInterpreter( } scope.doWithState { - val idx = mapLocalToIdx(lastEnteredMethod, stmt.lhv) - saveSortForLocal(idx, expr.sort) + when (val lhv = stmt.lhv) { + is EtsLocal -> { + val idx = mapLocalToIdx(lastEnteredMethod, lhv) + saveSortForLocal(idx, expr.sort) - val lValue = URegisterStackLValue(expr.sort, idx) - memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr) + val lValue = URegisterStackLValue(expr.sort, idx) + memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.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 + + // TODO fork on floating point field + val bvIndex = ctx.mkFpToBvExpr( + roundingMode = ctx.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) + } + } + + else -> TODO("Not yet implemented") + } val nextStmt = stmt.nextStmt ?: return@doWithState newStmt(nextStmt) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt new file mode 100644 index 000000000..c8aecf78c --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt @@ -0,0 +1,106 @@ +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 +import org.usvm.util.getResourcePath + +class Arrays : TsMethodTestRunner() { + override val scene: EtsScene = run { + val name = "Arrays.ts" + val path = getResourcePath("/samples/$name") + val file = loadEtsFileAutoConvert(path) + EtsScene(listOf(file)) + } + + @Test + fun testCreateConstantArrayOfNumbers() { + val method = getMethod("Arrays", "createConstantArrayOfNumbers") + discoverProperties( + method = method, + { r -> r.number == 1.0 }, + invariants = arrayOf( + { r -> r.number != -1.0 } + ) + ) + } + + @Test + fun testCreateAndReturnConstantArrayOfNumbers() { + val method = getMethod("Arrays", "createAndReturnConstantArrayOfNumbers") + discoverProperties>( + method = method, + { r -> r.values.map { it.number } == listOf(1.0, 2.0, 3.0) }, + ) + } + + @Test + fun testCreateAndAccessArrayOfBooleans() { + val method = getMethod("Arrays", "createAndAccessArrayOfBooleans") + discoverProperties( + method = method, + { r -> r.number == 1.0 }, + invariants = arrayOf( + { r -> r.number != -1.0 } + ) + ) + } + + @Test + fun testCreateArrayOfBooleans() { + val method = getMethod("Arrays", "createArrayOfBooleans") + discoverProperties>( + method = method, + { r -> r.values.map { it.value } == listOf(true, false, true) }, + ) + } + + @Test + @Disabled("Arrays should contain only fake objects") + fun testCreateMixedArray() { + val method = getMethod("Arrays", "createMixedArray") + discoverProperties>( + method = method, + { r -> + if (r.values.size != 3) return@discoverProperties false + val cond0 = r.values[0] is TsValue.TsNumber.TsDouble + val cond1 = r.values[1] is TsValue.TsBoolean + val cond2 = r.values[2] is TsValue.TsUndefined + cond0 && cond1 && cond2 + }, + ) + } + + @Test + fun testCreateArrayOfUnknown() { + val method = getMethod("Arrays", "createArrayOfUnknownValues") + discoverProperties>( + method = method, + { a, _, _, r -> r.values[0] == a && (a as TsValue.TsNumber).number == 1.1 }, + { _, b, _, r -> r.values[1] == b && (b as TsValue.TsBoolean).value }, + { _, _, c, r -> r.values[2] == c && c is TsValue.TsUndefined }, + invariants = arrayOf( + { a, b, c, r -> r.values == listOf(a, b, c) } + ) + ) + } + + @Test + @Disabled("Arrays should contain only fake objects") + fun testCreateArrayOfNumbersAndPutDifferentTypes() { + val method = getMethod("Arrays", "createArrayOfNumbersAndPutDifferentTypes") + discoverProperties>( + method = method, + { r -> + val values = r.values + values.size == 3 + && (values[0] as TsValue.TsClass).properties.size == 1 + && (values[1] as TsValue.TsBoolean).value + && values[2] is TsValue.TsUndefined + }, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/MinValue.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/MinValue.kt index 90673899f..50b6db149 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/MinValue.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/MinValue.kt @@ -21,7 +21,7 @@ class MinValue : TsMethodTestRunner() { @Disabled fun testMinValue() { val method = getMethod("MinValue", "findMinValue") - discoverProperties( + discoverProperties, TsValue.TsNumber>( method, ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt index e47bb9c89..e24abe68b 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt @@ -1,6 +1,7 @@ package org.usvm.util import org.jacodb.ets.base.EtsAnyType +import org.jacodb.ets.base.EtsArrayType import org.jacodb.ets.base.EtsBooleanType import org.jacodb.ets.base.EtsClassType import org.jacodb.ets.base.EtsNullType @@ -166,14 +167,18 @@ abstract class TsMethodTestRunner : TestRunner EtsAnyType TsValue.TsAny::class -> EtsAnyType - TsValue.TsArray::class -> TODO() - TsValue.TsBoolean::class -> EtsBooleanType + + TsValue.TsArray::class -> { + EtsArrayType(EtsAnyType, dimensions = 1) // TODO incorrect + } + TsValue.TsClass::class -> { // TODO incorrect val signature = EtsClassSignature(it.toString(), EtsFileSignature.DEFAULT) EtsClassType(signature) } + TsValue.TsBoolean::class -> EtsBooleanType TsValue.TsString::class -> EtsStringType TsValue.TsNumber::class -> EtsNumberType TsValue.TsNumber.TsDouble::class -> EtsNumberType @@ -184,6 +189,7 @@ abstract class TsMethodTestRunner : TestRunner EtsUnknownType TsValue.TsNull::class -> EtsNullType + TsValue.TsException::class -> { // TODO incorrect val signature = EtsClassSignature("Exception", EtsFileSignature.DEFAULT) 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 10da86f21..752f69d36 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -1,7 +1,9 @@ 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 import org.jacodb.ets.base.EtsLiteralType @@ -13,12 +15,14 @@ import org.jacodb.ets.base.EtsRefType import org.jacodb.ets.base.EtsStringType import org.jacodb.ets.base.EtsType import org.jacodb.ets.base.EtsUndefinedType +import org.jacodb.ets.base.EtsUnknownType import org.jacodb.ets.base.EtsVoidType 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.USort @@ -26,20 +30,25 @@ import org.usvm.api.GlobalFieldValue import org.usvm.api.TsParametersState import org.usvm.api.TsTest import org.usvm.api.TsValue +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.expr.TsUnresolvedSort import org.usvm.machine.expr.extractBool import org.usvm.machine.expr.extractDouble -import org.usvm.machine.expr.extractInt +import org.usvm.machine.expr.tctx import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.machine.types.FakeType import org.usvm.memory.ULValue import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.URegisterStackLValue +import org.usvm.mkSizeExpr import org.usvm.model.UModelBase +import org.usvm.sizeSort +import org.usvm.types.first import org.usvm.types.single class TsTestResolver { @@ -114,9 +123,64 @@ open class TsTestStateResolver( type: EtsType, ): TsValue = when (type) { is EtsPrimitiveType -> resolvePrimitive(expr, type) - is EtsClassType -> resolveClass(expr, type) - is EtsRefType -> TODO() - else -> TODO() + is EtsRefType -> resolveRef(expr.asExpr(ctx.addressSort), type) + else -> resolveUnknownExpr(expr) + } + + fun resolveUnknownExpr(expr: UExpr): TsValue = with(expr.tctx) { + when (expr.sort) { + fp64Sort -> resolvePrimitive(expr, EtsNumberType) + boolSort -> resolvePrimitive(expr, EtsBooleanType) + addressSort -> { + if (expr.isFakeObject()) { + resolveFakeObject(expr) + } else { + resolveRef(expr.asExpr(ctx.addressSort), EtsUnknownType) + } + } + else -> TODO() + } + } + + private fun resolveRef(expr: UExpr, type: EtsType): TsValue { + val instance = model.eval(expr) as UConcreteHeapRef + + if (instance.address == 0) { + return TsValue.TsUndefined + } + + if (model.eval(ctx.mkHeapRefEq(expr, ctx.mkTsNullValue())).isTrue) { + return TsValue.TsNull + } + + return when (type) { + is EtsClassType -> resolveClass(instance, type) + is EtsArrayType -> resolveArray(instance, type) + is EtsUnknownType -> { + val type = finalStateMemory.types.getTypeStream(expr).first() + resolveRef(expr, type) + } + else -> error("Unexpected type: $type") + } + } + + private fun resolveArray(expr: UConcreteHeapRef, type: EtsArrayType): TsValue.TsArray<*> { + val arrayLengthLValue = UArrayLengthLValue(expr, type, ctx.sizeSort) + val length = model.eval(memory.read(arrayLengthLValue)) as KBitVec32Value + + 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 value = memory.read(lValue) // TODO write reading??? + resolveExpr(value, type.elementType) + } + + return TsValue.TsArray(values) } fun resolveThisInstance(): TsValue? { @@ -184,42 +248,14 @@ open class TsTestStateResolver( expr: UExpr, type: EtsPrimitiveType, ): TsValue = when (type) { - EtsNumberType -> { - when (expr.sort) { - ctx.fp64Sort -> TsValue.TsNumber.TsDouble(extractDouble(evaluateInModel(expr))) - ctx.bv32Sort -> TsValue.TsNumber.TsInteger(extractInt(evaluateInModel(expr))) - else -> error("Unexpected sort: ${expr.sort}") - } - } - - EtsBooleanType -> { - TsValue.TsBoolean(evaluateInModel(expr).extractBool()) - } - - EtsUndefinedType -> { - TsValue.TsUndefined - } - - is EtsLiteralType -> { - TODO() - } - - EtsNullType -> { - TODO() - } - - EtsNeverType -> { - TODO() - } - - EtsStringType -> { - TODO() - } - - EtsVoidType -> { - TODO() - } - + 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") } diff --git a/usvm-ts/src/test/resources/samples/Arrays.ts b/usvm-ts/src/test/resources/samples/Arrays.ts new file mode 100644 index 000000000..7f613ec89 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/Arrays.ts @@ -0,0 +1,43 @@ +class Arrays { + createConstantArrayOfNumbers() { + let x = [1, 2, 3] + if (x[0] == 1) return 1 + return -1 + } + + createAndReturnConstantArrayOfNumbers() { + return [1, 2, 3] + } + + createAndAccessArrayOfBooleans() { + let x = [true, false, true] + if (x[0] == true) return 1 + return -1 + } + + createArrayOfBooleans() { + let x = [true, false, true] + return x + } + + createMixedArray() { + let x = [1.1, true, undefined] + return x + } + + 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 + return x + } + + createArrayOfNumbersAndPutDifferentTypes() { + let x = [1, 2, 3] + x[1] = true + x[2] = undefined + x[0] = null + return x + } +}