From e5b74dc963fdafafbe729afe72e2256ca86d9950 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 6 Jun 2025 17:11:58 +0300 Subject: [PATCH 1/4] Input arrays support --- .../main/kotlin/org/usvm/machine/TsContext.kt | 17 +- .../main/kotlin/org/usvm/machine/TsMachine.kt | 5 + .../org/usvm/machine/expr/TsExprResolver.kt | 159 +++++++++++++---- .../org/usvm/machine/expr/TsExpressions.kt | 14 +- .../usvm/machine/interpreter/TsInterpreter.kt | 56 ++++-- .../usvm/machine/operator/TsBinaryOperator.kt | 62 ++++++- .../kotlin/org/usvm/machine/state/TsState.kt | 8 + .../src/main/kotlin/org/usvm/util/Utils.kt | 2 + .../{Arrays.kt => arrays/AllocatedArrays.kt} | 66 ++++--- .../org/usvm/samples/arrays/InputArrays.kt | 129 ++++++++++++++ .../org/usvm/util/TsMethodTestRunner.kt | 109 ++++++++++++ .../kotlin/org/usvm/util/TsTestResolver.kt | 165 ++++++++++++++---- .../{Arrays.ts => arrays/AllocatedArrays.ts} | 15 +- .../resources/samples/arrays/InputArrays.ts | 48 +++++ .../org/usvm/test/util/checkers/Matchers.kt | 5 + 15 files changed, 731 insertions(+), 129 deletions(-) rename usvm-ts/src/test/kotlin/org/usvm/samples/{Arrays.kt => arrays/AllocatedArrays.kt} (65%) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt rename usvm-ts/src/test/resources/samples/{Arrays.ts => arrays/AllocatedArrays.ts} (83%) create mode 100644 usvm-ts/src/test/resources/samples/arrays/InputArrays.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 9986128a08..d6f482d69a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -77,14 +77,15 @@ class TsContext( else -> TODO("${type::class.simpleName} is not yet supported: $type") } - // TODO: for now, ALL descriptors for array are UNKNOWN - // in order to make ALL reading/writing, including '.length' access consistent - // and possible in cases when the array type is not known. - // For example, when we access '.length' of some array, we do not care about its type, - // but we HAVE TO use some type consistent with the type used when this array was created. - // Note: Using UnknownType everywhere does not lead to any errors yet, - // since we do not rely on array types in any way. - fun arrayDescriptorOf(type: EtsArrayType): EtsType = EtsUnknownType + fun arrayDescriptorOf(type: EtsArrayType): EtsType { + return when (type.elementType) { + is EtsBooleanType -> EtsArrayType(EtsBooleanType, dimensions = 1) + is EtsNumberType -> EtsArrayType(EtsNumberType, dimensions = 1) + is EtsArrayType -> TODO("Unsupported yet: $type") + is EtsUnionType -> EtsArrayType(type.elementType, dimensions = 1) + else -> EtsArrayType(EtsUnknownType, dimensions = 1) + } + } fun UConcreteHeapRef.getFakeType(memory: UReadOnlyMemory<*>): EtsFakeType { check(isFakeObject()) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index d040ddd5b7..d82ac0ab88 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -23,6 +23,7 @@ import org.usvm.statistics.UMachineObserver import org.usvm.statistics.collectors.AllStatesCollector import org.usvm.statistics.collectors.CoveredNewStatesCollector import org.usvm.statistics.collectors.TargetsReachedStatesCollector +import org.usvm.statistics.constraints.SoftConstraintsObserver import org.usvm.statistics.distances.CfgStatisticsImpl import org.usvm.statistics.distances.PlainCallGraphStatistics import org.usvm.stopstrategies.createStopStrategy @@ -94,6 +95,10 @@ class TsMachine( val observers = mutableListOf>(coverageStatistics) observers.add(statesCollector) + if (options.useSoftConstraints) { + observers.add(SoftConstraintsObserver()) + } + val stepsStatistics = StepsStatistics() val stopStrategy = createStopStrategy( 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 6a87491ee9..23ad166f9d 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 @@ -5,6 +5,7 @@ import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.model.EtsAddExpr import org.jacodb.ets.model.EtsAndExpr +import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayAccess import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsAwaitExpr @@ -14,6 +15,7 @@ import org.jacodb.ets.model.EtsBitNotExpr import org.jacodb.ets.model.EtsBitOrExpr import org.jacodb.ets.model.EtsBitXorExpr import org.jacodb.ets.model.EtsBooleanConstant +import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsCastExpr import org.jacodb.ets.model.EtsConstant import org.jacodb.ets.model.EtsDeleteExpr @@ -44,6 +46,7 @@ import org.jacodb.ets.model.EtsNotExpr import org.jacodb.ets.model.EtsNullConstant import org.jacodb.ets.model.EtsNullishCoalescingExpr import org.jacodb.ets.model.EtsNumberConstant +import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsOrExpr import org.jacodb.ets.model.EtsParameterRef import org.jacodb.ets.model.EtsPostDecExpr @@ -77,15 +80,16 @@ import org.jacodb.ets.utils.getDeclaredLocals import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UBoolSort +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort import org.usvm.api.allocateArray import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type -import org.usvm.isTrue import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext +import org.usvm.machine.TsSizeSort import org.usvm.machine.TsVirtualMethodCallStmt import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.interpreter.isInitialized @@ -590,6 +594,9 @@ class TsExprResolver( override fun visit(value: EtsArrayAccess): UExpr? = with(ctx) { val array = resolve(value.array)?.asExpr(addressSort) ?: return null + + checkUndefinedOrNullPropertyRead(array) ?: return null + val index = resolve(value.index)?.asExpr(fp64Sort) ?: return null val bvIndex = mkFpToBvExpr( roundingMode = fpRoundingModeSortDefaultValue(), @@ -598,20 +605,74 @@ class TsExprResolver( isSigned = true, ).asExpr(sizeSort) - val lValue = mkArrayIndexLValue( - sort = addressSort, - ref = array, - index = bvIndex, - type = value.array.type as EtsArrayType - ) - val expr = scope.calcOnState { memory.read(lValue) } + val arrayType = value.array.type as? EtsArrayType + ?: error("Expected EtsArrayType, but got ${value.array.type}") + val sort = typeToSort(arrayType.elementType) + + val lengthLValue = mkArrayLengthLValue(array, arrayType) + val length = scope.calcOnState { memory.read(lengthLValue) } + + checkNegativeIndexRead(bvIndex) ?: return null + checkReadingInRange(bvIndex, length) ?: return null + + val expr = if (sort is TsUnresolvedSort) { + // Concrete arrays with the unresolved sort should consist of fake objects only. + if (array is UConcreteHeapRef) { + // Read a fake object from the array. + val lValue = mkArrayIndexLValue( + sort = addressSort, + ref = array, + index = bvIndex, + type = arrayType + ) + + scope.calcOnState { memory.read(lValue) } + } else { + // If the array is not concrete, we need to allocate a fake object + val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1) + val boolLValue = mkArrayIndexLValue(boolSort, array, bvIndex, boolArrayType) - check(expr.isFakeObject()) { "Only fake objects are allowed in arrays" } + val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1) + val fpLValue = mkArrayIndexLValue(fp64Sort, array, bvIndex, numberArrayType) + + val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + val refLValue = mkArrayIndexLValue(addressSort, array, bvIndex, unknownArrayType) + + scope.calcOnState { + val boolValue = memory.read(boolLValue) + val fpValue = memory.read(fpLValue) + val refValue = memory.read(refLValue) + + // Read an object from the memory at first, + // we don't need to recreate it if it is already a fake object. + val fakeObj = if (refValue.isFakeObject()) { + refValue + } else { + mkFakeValue(scope, boolValue, fpValue, refValue).also { + lValuesToAllocatedFakeObjects += refLValue to it + } + } + + memory.write(refLValue, fakeObj.asExpr(addressSort), guard = trueExpr) + + fakeObj + } + + } + } else { + val lValue = mkArrayIndexLValue( + sort = sort, + ref = array, + index = bvIndex, + type = arrayType + ) + scope.calcOnState { memory.read(lValue) } + } return expr } - private fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) { + fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) { val neqNull = mkAnd( mkHeapRefEq(instance, mkUndefinedValue()).not(), mkHeapRefEq(instance, mkTsNullValue()).not() @@ -623,6 +684,24 @@ class TsExprResolver( ) } + fun checkNegativeIndexRead(index: UExpr) = with(ctx) { + val condition = mkBvSignedGreaterOrEqualExpr(index, mkBv(0)) + + scope.fork( + condition, + blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type + ) + } + + fun checkReadingInRange(index: UExpr, length: UExpr) = with(ctx) { + val condition = mkBvSignedLessExpr(index, length) + + scope.fork( + condition, + blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type + ) + } + private fun allocateException(type: EtsType): (TsState) -> Unit = { state -> val address = state.memory.allocConcrete(type) state.throwExceptionWithoutStackFrameDrop(address, type) @@ -675,9 +754,8 @@ class TsExprResolver( val fakeRef = if (ref.isFakeObject()) { ref } else { - mkFakeValue(scope, bool, fp, ref) + mkFakeValue(scope, bool, fp, ref).also { lValuesToAllocatedFakeObjects += refLValue to it } } - memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr) fakeRef @@ -696,32 +774,46 @@ class TsExprResolver( // TODO It is a hack for array's length if (value.field.name == "length") { if (value.instance.type is EtsArrayType) { - val lengthLValue = mkArrayLengthLValue(instanceRef, value.instance.type as EtsArrayType) + val arrayType = value.instance.type as EtsArrayType + val lengthLValue = mkArrayLengthLValue(instanceRef, arrayType) val length = scope.calcOnState { memory.read(lengthLValue) } + scope.doWithState { pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) } + return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), length.asExpr(sizeSort), signed = true) } // TODO: handle "length" property for arrays inside fake objects if (instanceRef.isFakeObject()) { val fakeType = instanceRef.getFakeType(scope) - // TODO: replace '.isTrue' with fork or assert - 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 - ) + + // If we want to get length from a fake object, we assume that it is an array. + scope.assert(fakeType.refTypeExpr) + + val refLValue = getIntermediateRefLValue(instanceRef.address) + val obj = scope.calcOnState { memory.read(refLValue) } + + val type = value.instance.type + val arrayType = type as? EtsArrayType ?: run { + check(type is EtsAnyType || type is EtsUnknownType) { + "Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got $type" + } + + // We don't know the type of the array, since it is a fake object + // If we'd know the type, we would have used it instead of creating a fake object + EtsArrayType(EtsUnknownType, dimensions = 1) } + val lengthLValue = mkArrayLengthLValue(obj, arrayType) + val length = scope.calcOnState { memory.read(lengthLValue) } + + scope.doWithState { pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) } + + return mkBvToFpExpr( + fp64Sort, + fpRoundingModeSortDefaultValue(), + length.asExpr(sizeSort), + signed = true + ) + } } @@ -809,7 +901,12 @@ class TsExprResolver( blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type ) - val arrayType = EtsArrayType(EtsUnknownType, 1) // TODO: expr.type + val arrayType = expr.type as EtsArrayType + + if (arrayType.elementType is EtsArrayType) { + TODO("Multidimensional arrays are not supported yet, https://github.com/UnitTestBot/usvm/issues/287") + } + val address = memory.allocateArray(arrayType, sizeSort, bvSize) address 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 faa522dd62..2baa334243 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 @@ -79,12 +79,20 @@ fun UExpr.toConcreteBoolValue(): Boolean = when (this) { else -> error("Cannot extract boolean from $this") } -fun extractInt(expr: UExpr): Int = - (expr as? KBitVec32Value)?.intValue ?: error("Cannot extract int from $expr") - fun UExpr.extractDouble(): Double { if (this@extractDouble is KFp64Value) { return value } error("Cannot extract double from $this") } + +/** + * Extracts an integer value from [this] expression if possible. + * Otherwise, throws an error. + */ +fun UExpr.extractInt(): Int { + if (this@extractInt is KBitVec32Value) { + return intValue + } + error("Cannot extract int 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 80aebfc83d..c058217923 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 @@ -280,7 +280,8 @@ class TsInterpreter( with(ctx) { it.toFakeObject(scope) } } val array = scope.calcOnState { - val type = EtsArrayType(EtsUnknownType, 1) + // In a common case we cannot determine the type of the array + val type = EtsArrayType(EtsUnknownType, dimensions = 1) memory.allocateArrayInitialized( type = ctx.arrayDescriptorOf(type), sort = ctx.addressSort, @@ -418,6 +419,8 @@ class TsInterpreter( is EtsArrayAccess -> { val instance = exprResolver.resolve(lhv.array)?.asExpr(addressSort) ?: return@doWithState + exprResolver.checkUndefinedOrNullPropertyRead(instance) ?: return@doWithState + val index = exprResolver.resolve(lhv.index)?.asExpr(fp64Sort) ?: return@doWithState // TODO fork on floating point field @@ -428,29 +431,50 @@ class TsInterpreter( isSigned = true ).asExpr(sizeSort) + // We don't allow access by negative indices and treat is as an error. + exprResolver.checkNegativeIndexRead(bvIndex) ?: return@doWithState + // 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 arrayType = lhv.array.type as? EtsArrayType + ?: error("Expected EtsArrayType, got: ${lhv.array.type}") + val lengthLValue = mkArrayLengthLValue(instance, arrayType) val currentLength = memory.read(lengthLValue) - val condition = mkBvSignedGreaterOrEqualExpr(bvIndex, currentLength) - val newLength = mkIte(condition, mkBvAddExpr(bvIndex, mkBv(1)), currentLength) + // We allow readings from the array only in the range [0, length - 1]. + exprResolver.checkReadingInRange(bvIndex, currentLength) ?: return@doWithState - memory.write(lengthLValue, newLength, guard = trueExpr) + val elementSort = typeToSort(arrayType.elementType) - val fakeExpr = expr.toFakeObject(scope) + if (elementSort is TsUnresolvedSort) { + val fakeExpr = expr.toFakeObject(scope) - val lValue = mkArrayIndexLValue( - addressSort, - instance, - bvIndex.asExpr(sizeSort), - lhv.array.type as EtsArrayType - ) - memory.write(lValue, fakeExpr, guard = trueExpr) + val lValue = mkArrayIndexLValue( + addressSort, + instance, + bvIndex.asExpr(sizeSort), + arrayType + ) + + lValuesToAllocatedFakeObjects += lValue to fakeExpr + + memory.write(lValue, fakeExpr, guard = trueExpr) + } else { + val lValue = mkArrayIndexLValue( + elementSort, + instance, + bvIndex.asExpr(sizeSort), + arrayType + ) + + memory.write(lValue, expr.asExpr(elementSort), guard = trueExpr) + } } is EtsInstanceFieldRef -> { val instance = exprResolver.resolve(lhv.instance)?.asExpr(addressSort) ?: return@doWithState + exprResolver.checkUndefinedOrNullPropertyRead(instance) ?: return@doWithState + val etsField = resolveEtsField(lhv.instance, lhv.field, graph.hierarchy) scope.doWithState { // If we access some field, we expect that the object must have this field. @@ -469,6 +493,9 @@ class TsInterpreter( if (sort == unresolvedSort) { val fakeObject = expr.toFakeObject(scope) val lValue = mkFieldLValue(addressSort, instance, lhv.field) + + lValuesToAllocatedFakeObjects += lValue to fakeObject + memory.write(lValue, fakeObject, guard = trueExpr) } else { val lValue = mkFieldLValue(sort, instance, lhv.field) @@ -499,6 +526,9 @@ class TsInterpreter( if (sort == unresolvedSort) { val lValue = mkFieldLValue(addressSort, instance, lhv.field.name) val fakeObject = expr.toFakeObject(scope) + + lValuesToAllocatedFakeObjects += lValue to fakeObject + memory.write(lValue, fakeObject, guard = trueExpr) } else { val lValue = mkFieldLValue(sort, instance, lhv.field.name) 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 49da780f13..61fe75b120 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 @@ -9,6 +9,7 @@ import org.usvm.UBoolExpr import org.usvm.UBoolSort import org.usvm.UExpr import org.usvm.UHeapRef +import org.usvm.UIteExpr import org.usvm.machine.TsContext import org.usvm.machine.expr.mkNumericExpr import org.usvm.machine.expr.mkTruthyExpr @@ -56,6 +57,26 @@ sealed interface TsBinaryOperator { rhs: UExpr<*>, scope: TsStepScope, ): UExpr<*>? { + if (lhs is UIteExpr<*>) { + val trueBranch = resolve(lhs.trueBranch, rhs, scope) ?: return null + val falseBranch = resolve(lhs.falseBranch, rhs, scope) ?: return null + return lhs.ctx.mkIte( + lhs.condition, + trueBranch.asExpr(falseBranch.sort), + falseBranch.asExpr(trueBranch.sort) + ) + } + + if (rhs is UIteExpr<*>) { + val trueBranch = resolve(lhs, rhs.trueBranch, scope) ?: return null + val falseBranch = resolve(lhs, rhs.falseBranch, scope) ?: return null + return lhs.ctx.mkIte( + rhs.condition, + trueBranch.asExpr(falseBranch.sort), + falseBranch.asExpr(trueBranch.sort) + ) + } + val lhsValue = lhs.extractSingleValueFromFakeObjectOrNull(scope) ?: lhs val rhsValue = rhs.extractSingleValueFromFakeObjectOrNull(scope) ?: rhs @@ -530,6 +551,9 @@ sealed interface TsBinaryOperator { ): UBoolExpr { check(lhs.isFakeObject() || rhs.isFakeObject()) + var lhsValue: UExpr<*> = lhs + var rhsValue: UExpr<*> = rhs + val typeConstraint = when { lhs.isFakeObject() && rhs.isFakeObject() -> { val lhsType = lhs.getFakeType(scope) @@ -545,10 +569,19 @@ sealed interface TsBinaryOperator { lhs.isFakeObject() -> { val lhsType = lhs.getFakeType(scope) when (rhs.sort) { - boolSort -> lhsType.boolTypeExpr - fp64Sort -> lhsType.fpTypeExpr + boolSort -> { + lhsValue = lhs.extractBool(scope) + lhsType.boolTypeExpr + } + fp64Sort -> { + lhsValue = lhs.extractFp(scope) + lhsType.fpTypeExpr + } // TODO support type equality - addressSort -> lhsType.refTypeExpr + addressSort -> { + lhsValue = lhs.extractRef(scope) + lhsType.refTypeExpr + } else -> error("Unsupported sort ${rhs.sort}") } } @@ -556,10 +589,19 @@ sealed interface TsBinaryOperator { rhs.isFakeObject() -> { val rhsType = rhs.getFakeType(scope) when (lhs.sort) { - boolSort -> rhsType.boolTypeExpr - fp64Sort -> rhsType.fpTypeExpr + boolSort -> { + rhsValue = rhs.extractBool(scope) + rhsType.boolTypeExpr + } + fp64Sort -> { + rhsValue = rhs.extractFp(scope) + rhsType.fpTypeExpr + } // TODO support type equality - addressSort -> rhsType.refTypeExpr + addressSort -> { + rhsValue = rhs.extractRef(scope) + rhsType.refTypeExpr + } else -> error("Unsupported sort ${lhs.sort}") } } @@ -570,7 +612,7 @@ sealed interface TsBinaryOperator { } val loosyEqualityConstraint = with(Eq) { - resolveFakeObject(lhs, rhs, scope) + resolve(lhsValue, rhsValue, scope)?.asExpr(boolSort) ?: error("Should not be encountered") } return mkAnd(typeConstraint, loosyEqualityConstraint) @@ -581,8 +623,10 @@ sealed interface TsBinaryOperator { rhs: UExpr<*>, scope: TsStepScope, ): UBoolExpr? { - logger.warn { "Not implemented operator: StrictEq" } - error("Not implemented strict eq") + // Strict equality checks that both sides are of the same type, + // therefore they have to be processed in the other methods. + // Otherwise, they would have the same sorts. + return lhs.ctx.mkFalse() } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 34dd06b529..fa69925170 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -21,11 +21,17 @@ import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.constraints.UPathConstraints import org.usvm.machine.TsContext +import org.usvm.memory.ULValue import org.usvm.memory.UMemory import org.usvm.model.UModelBase import org.usvm.targets.UTargetsSet import org.usvm.util.type +/** + * [lValuesToAllocatedFakeObjects] contains records of l-values that were allocated with newly created fake objects. + * It is important for result interpreters to be able to restore the order of fake objects allocation and + * their assignment to evaluated l-values. + */ class TsState( ctx: TsContext, ownership: MutabilityOwnership, @@ -42,6 +48,7 @@ class TsState( var staticStorage: UPersistentHashMap = persistentHashMapOf(), val globalObject: UConcreteHeapRef = memory.allocStatic(EtsClassType(EtsClassSignature.UNKNOWN)), val addedArtificialLocals: MutableSet = hashSetOf(), + val lValuesToAllocatedFakeObjects: MutableList, UConcreteHeapRef>> = mutableListOf(), ) : UState( ctx = ctx, initOwnership = ownership, @@ -144,6 +151,7 @@ class TsState( staticStorage = staticStorage, globalObject = globalObject, addedArtificialLocals = addedArtificialLocals, + lValuesToAllocatedFakeObjects = lValuesToAllocatedFakeObjects.toMutableList(), ) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt index 9457282d05..2e3e147ac9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt @@ -53,6 +53,8 @@ fun EtsType.getClassesForType( .filter { it.type.typeName.removeTrashFromTheName() == name } } +// TODO save info about this field somewhere +// https://github.com/UnitTestBot/usvm/issues/288 fun UHeapRef.createFakeField(fieldName: String, scope: TsStepScope): UConcreteHeapRef { val ctx = this.tctx diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt similarity index 65% rename from usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt rename to usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt index e2c3b93c7b..70d8be3e9d 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt @@ -1,17 +1,16 @@ -package org.usvm.samples +package org.usvm.samples.arrays import org.jacodb.ets.model.EtsScene -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.api.TsTestValue +import org.usvm.test.util.checkers.noResultsExpected import org.usvm.util.TsMethodTestRunner -@Disabled("Arrays are not fully supported, tests are unstable on CI") -class Arrays : TsMethodTestRunner() { +class AllocatedArrays : TsMethodTestRunner() { private val className = this::class.simpleName!! - override val scene: EtsScene = loadSampleScene(className) + override val scene: EtsScene = loadSampleScene(className, folderPrefix = "arrays") @Test fun `test createConstantArrayOfNumbers`() { @@ -87,41 +86,56 @@ class Arrays : TsMethodTestRunner() { @Test fun `test createArrayOfNumbersAndPutDifferentTypes`() { val method = getMethod(className, "createArrayOfNumbersAndPutDifferentTypes") - discoverProperties>( + checkMatches>( method = method, - { r -> - val values = r.values - values.size == 3 - && values[0] is TsTestValue.TsNull - && (values[1] as TsTestValue.TsBoolean).value - && values[2] is TsTestValue.TsUndefined - }, + noResultsExpected ) } @Test fun `test allocatedArrayLengthExpansion`() { val method = getMethod(className, "allocatedArrayLengthExpansion") - discoverProperties>( + discoverProperties( method = method, - { r -> - r.values.size == 6 - && (r.values[0] as TsTestValue.TsNumber).number == 1.0 - && (r.values[1] as TsTestValue.TsNumber).number == 2.0 - && (r.values[2] as TsTestValue.TsNumber).number == 3.0 - && r.values[3] is TsTestValue.TsUndefined - && r.values[4] is TsTestValue.TsUndefined - && (r.values[5] as TsTestValue.TsNumber).number == 5.0 - } + { r -> r is TsTestValue.TsException } ) } @Test fun `test writeInTheIndexEqualToLength`() { val method = getMethod(className, "writeInTheIndexEqualToLength") - discoverProperties>( + discoverProperties( + method = method, + { r -> r is TsTestValue.TsException }, + ) + } + + @Test + fun `test readFakeObjectAndWriteFakeObject`() { + val method = getMethod(className, "readFakeObjectAndWriteFakeObject") + discoverProperties, TsTestValue, TsTestValue>( method = method, - { r -> r.values.map { it.number } == listOf(1.0, 2.0, 3.0, 4.0) }, + { x, y, r -> + val fst = x.values[0] + val fstCondition = fst is TsTestValue.TsNumber && fst.number == 1.0 + val sndCondition = y is TsTestValue.TsNumber && y.number == 2.0 + val resultCondition = r is TsTestValue.TsArray<*> && r.values[0] == y + + fstCondition && sndCondition && resultCondition + }, + { x, y, r -> + val fst = x.values[0] + val fstCondition = fst is TsTestValue.TsNumber && fst.number == 1.0 + val sndCondition = y !is TsTestValue.TsNumber || y.number != 2.0 + val resultCondition = r is TsTestValue.TsArray<*> && r.values[0] == y + + fstCondition && sndCondition && resultCondition + }, + { x, y, r -> + val fst = x.values[0] + val condition = fst !is TsTestValue.TsNumber || fst.number != 1.0 + condition && r is TsTestValue.TsArray<*> && r.values == x.values + }, ) } -} +} \ No newline at end of file diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt new file mode 100644 index 0000000000..e4a8efd566 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt @@ -0,0 +1,129 @@ +package org.usvm.samples.arrays + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner + +class InputArrays : TsMethodTestRunner() { + private val className = this::class.simpleName!! + + override val scene: EtsScene = loadSampleScene(className, folderPrefix = "arrays") + + @Test + fun testInputArrayOfNumbers() { + val method = getMethod(className, "inputArrayOfNumbers") + discoverProperties( + method = method, + { x, r -> x is TsTestValue.TsUndefined && r is TsTestValue.TsException }, + { x, r -> + r as TsTestValue.TsNumber + + x is TsTestValue.TsArray<*> && (x.values[0] as? TsTestValue.TsNumber)?.number == 1.0 && r.number == 1.0 + }, + { x, r -> + r as TsTestValue.TsNumber + + x is TsTestValue.TsArray<*> && (x.values[0] as? TsTestValue.TsNumber)?.number != 1.0 && r.number == 2.0 + }, + invariants = arrayOf( + { _, r -> r !is TsTestValue.TsNumber || r.number != -1.0 } + ) + ) + } + + @Test + fun testWriteIntoInputArray() { + val method = getMethod(className, "writeIntoInputArray") + discoverProperties, TsTestValue.TsNumber>( + method = method, + { x, r -> x.values[0].number == 1.0 && r.number == 1.0 }, + { x, r -> x.values[0].number != 1.0 && r.number == 1.0 }, + ) + } + + @Test + fun testIdForArrayOfNumbers() { + val method = getMethod(className, "idForArrayOfNumbers") + discoverProperties, TsTestValue.TsArray>( + method = method, + { x, r -> x.values == r.values }, + ) + } + + @Test + fun testArrayOfBooleans() { + val method = getMethod(className, "arrayOfBooleans") + discoverProperties, TsTestValue.TsNumber>( + method = method, + { x, r -> x.values[0].value == true && r.number == 1.0 }, + { x, r -> x.values[0].value != true && r.number == -1.0 }, + ) + } + + @Test + fun testArrayOfUnknownValues() { + val method = getMethod(className, "arrayOfUnknownValues") + discoverProperties, TsTestValue.TsArray>( + method = method, + // TODO exception + { x, r -> + val firstElement = x.values[0] + firstElement is TsTestValue.TsNumber && firstElement.number == 1.1 && x.values == r.values + }, + { x, r -> + val firstElement = x.values[0] + val firstElementCondition = firstElement !is TsTestValue.TsNumber || firstElement.number != 1.1 + + val secondElement = x.values[1] + val secondElementCondition = secondElement is TsTestValue.TsBoolean && secondElement.value + + firstElementCondition && secondElementCondition && x.values == r.values + }, + { x, r -> + val firstElement = x.values[0] + val firstElementCondition = firstElement !is TsTestValue.TsNumber || firstElement.number != 1.1 + + val secondElement = x.values[1] + val secondElementCondition = secondElement !is TsTestValue.TsBoolean || !secondElement.value + + val thirdElement = x.values[2] + val thirdElementCondition = thirdElement is TsTestValue.TsUndefined + + firstElementCondition && secondElementCondition && thirdElementCondition && x.values == r.values + } + ) + } + + @Test + fun testWriteIntoArrayOfUnknownValues() { + val method = getMethod(className, "writeIntoArrayOfUnknownValues") + discoverProperties, TsTestValue.TsArray>( + method = method, + { _, r -> + val fst = r.values[0] is TsTestValue.TsNull + val sndElement = r.values[1] + val snd = sndElement is TsTestValue.TsBoolean && sndElement.value + val trd = r.values[2] is TsTestValue.TsUndefined + + fst && snd && trd + }, + // TODO add exceptions + ) + } + + @Test + fun testRewriteFakeValueInArray() { + val method = getMethod(className, "rewriteFakeValueInArray") + discoverProperties, TsTestValue>( + method = method, + { x, r -> + val value = x.values[0] + value is TsTestValue.TsNumber && value.number == 1.0 && r is TsTestValue.TsNull }, + { x, r -> + val value = x.values[0] + value !is TsTestValue.TsNumber || value.number != 1.0 && r == value + }, + ) + } +} \ No newline at end of file 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 889dae0586..8da408fd60 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt @@ -26,6 +26,7 @@ import org.usvm.api.TsTestValue import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.test.util.TestRunner +import org.usvm.test.util.checkers.AnalysisResultsNumberMatcher import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults import kotlin.reflect.KClass import kotlin.time.Duration @@ -78,6 +79,25 @@ abstract class TsMethodTestRunner : TestRunner checkMatches( + method: EtsMethod, + analysisResultNumberMatches: AnalysisResultsNumberMatcher, + vararg analysisResultMatchers: (R) -> Boolean, + invariants: Array<(R) -> Boolean> = emptyArray(), + noinline coverageChecker: CoverageChecker = doNotCheckCoverage, + ) { + internalCheck( + target = method, + analysisResultsNumberMatcher = analysisResultNumberMatches, + analysisResultsMatchers = analysisResultMatchers, + invariants = invariants, + extractValuesToCheck = { r -> r.before.parameters + r.returnValue }, + expectedTypesForExtractedValues = arrayOf(typeTransformer(R::class)), + checkMode = CheckMode.MATCH_EXECUTIONS, + coverageChecker = coverageChecker + ) + } + protected inline fun discoverProperties( method: EtsMethod, vararg analysisResultMatchers: (T, R) -> Boolean, @@ -96,6 +116,25 @@ abstract class TsMethodTestRunner : TestRunner checkMatches( + method: EtsMethod, + analysisResultNumberMatches: AnalysisResultsNumberMatcher, + vararg analysisResultMatchers: (T, R) -> Boolean, + invariants: Array<(T, R) -> Boolean> = emptyArray(), + noinline coverageChecker: CoverageChecker = doNotCheckCoverage, + ) { + internalCheck( + target = method, + analysisResultsNumberMatcher = analysisResultNumberMatches, + analysisResultsMatchers = analysisResultMatchers, + invariants = invariants, + extractValuesToCheck = { r -> r.before.parameters + r.returnValue }, + expectedTypesForExtractedValues = arrayOf(typeTransformer(T::class), typeTransformer(R::class)), + checkMode = CheckMode.MATCH_EXECUTIONS, + coverageChecker = coverageChecker + ) + } + protected inline fun discoverProperties( method: EtsMethod, vararg analysisResultMatchers: (T1, T2, R) -> Boolean, @@ -116,6 +155,27 @@ abstract class TsMethodTestRunner : TestRunner checkMatches( + method: EtsMethod, + analysisResultNumberMatches: AnalysisResultsNumberMatcher, + vararg analysisResultMatchers: (T1, T2, R) -> Boolean, + invariants: Array<(T1, T2, R) -> Boolean> = emptyArray(), + noinline coverageChecker: CoverageChecker = doNotCheckCoverage, + ) { + internalCheck( + target = method, + analysisResultsNumberMatcher = analysisResultNumberMatches, + analysisResultsMatchers = analysisResultMatchers, + invariants = invariants, + extractValuesToCheck = { r -> r.before.parameters + r.returnValue }, + expectedTypesForExtractedValues = arrayOf( + typeTransformer(T1::class), typeTransformer(T2::class), typeTransformer(R::class) + ), + checkMode = CheckMode.MATCH_EXECUTIONS, + coverageChecker = coverageChecker + ) + } + protected inline fun discoverProperties( method: EtsMethod, vararg analysisResultMatchers: (T1, T2, T3, R) -> Boolean, @@ -139,6 +199,30 @@ abstract class TsMethodTestRunner : TestRunner checkMatches( + method: EtsMethod, + analysisResultNumberMatches: AnalysisResultsNumberMatcher, + vararg analysisResultMatchers: (T1, T2, T3, R) -> Boolean, + invariants: Array<(T1, T2, T3, R) -> Boolean> = emptyArray(), + noinline coverageChecker: CoverageChecker = doNotCheckCoverage, + ) { + internalCheck( + target = method, + analysisResultsNumberMatcher = analysisResultNumberMatches, + analysisResultsMatchers = analysisResultMatchers, + invariants = invariants, + extractValuesToCheck = { r -> r.before.parameters + r.returnValue }, + expectedTypesForExtractedValues = arrayOf( + typeTransformer(T1::class), + typeTransformer(T2::class), + typeTransformer(T3::class), + typeTransformer(R::class) + ), + checkMode = CheckMode.MATCH_EXECUTIONS, + coverageChecker = coverageChecker + ) + } + protected inline fun discoverProperties( method: EtsMethod, vararg analysisResultMatchers: (T1, T2, T3, T4, R) -> Boolean, @@ -163,6 +247,31 @@ abstract class TsMethodTestRunner : TestRunner checkMatches( + method: EtsMethod, + analysisResultNumberMatches: AnalysisResultsNumberMatcher, + vararg analysisResultMatchers: (T1, T2, T3, T4, R) -> Boolean, + invariants: Array<(T1, T2, T3, T4, R) -> Boolean> = emptyArray(), + noinline coverageChecker: CoverageChecker = doNotCheckCoverage, + ) { + internalCheck( + target = method, + analysisResultsNumberMatcher = analysisResultNumberMatches, + analysisResultsMatchers = analysisResultMatchers, + invariants = invariants, + extractValuesToCheck = { r -> r.before.parameters + r.returnValue }, + expectedTypesForExtractedValues = arrayOf( + typeTransformer(T1::class), + typeTransformer(T2::class), + typeTransformer(T3::class), + typeTransformer(T4::class), + typeTransformer(R::class) + ), + checkMode = CheckMode.MATCH_EXECUTIONS, + coverageChecker = coverageChecker + ) + } + /* For now type checks are disabled for development purposes 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 32d80e14ea..7ee7b03e55 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -1,6 +1,6 @@ package org.usvm.util -import io.ksmt.expr.KBitVec32Value +import io.ksmt.expr.KFpValue import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanType @@ -22,8 +22,10 @@ import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsVoidType import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME import org.usvm.UAddressSort +import org.usvm.UBoolSort import org.usvm.UConcreteHeapRef import org.usvm.UExpr +import org.usvm.UFpSort import org.usvm.UHeapRef import org.usvm.USort import org.usvm.api.GlobalFieldValue @@ -31,11 +33,14 @@ import org.usvm.api.TsParametersState import org.usvm.api.TsTest import org.usvm.api.TsTestValue import org.usvm.api.typeStreamOf +import org.usvm.collection.array.UArrayIndexLValue +import org.usvm.collection.field.UFieldLValue import org.usvm.isAllocated import org.usvm.isTrue import org.usvm.machine.TsContext import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.expr.extractDouble +import org.usvm.machine.expr.extractInt import org.usvm.machine.expr.toConcreteBoolValue import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -43,16 +48,22 @@ import org.usvm.memory.ULValue import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.URegisterStackLValue import org.usvm.mkSizeExpr +import org.usvm.model.UModel import org.usvm.model.UModelBase +import org.usvm.sizeSort import org.usvm.types.first class TsTestResolver { + private val resolvedLValuesToFakeObjects: MutableList, UConcreteHeapRef>> = mutableListOf() + fun resolve(method: EtsMethod, state: TsState): TsTest = with(state.ctx) { val model = state.models.first() val memory = state.memory - val beforeMemoryScope = MemoryScope(this, model, memory, method) - val afterMemoryScope = MemoryScope(this, model, memory, method) + prepareForResolve(state) + + val beforeMemoryScope = MemoryScope(this, model, memory, method, resolvedLValuesToFakeObjects) + val afterMemoryScope = MemoryScope(this, model, memory, method, resolvedLValuesToFakeObjects) val result = when (val res = state.methodResult) { is TsMethodResult.NoCall -> { @@ -61,7 +72,7 @@ class TsTestResolver { is TsMethodResult.Success -> { afterMemoryScope.withMode(ResolveMode.CURRENT) { - resolveExpr(res.value, res.value) + resolveExpr(res.value) } } @@ -76,6 +87,33 @@ class TsTestResolver { return TsTest(method, before, after, result, trace = emptyList()) } + private fun prepareForResolve(state: TsState) { + state.lValuesToAllocatedFakeObjects.map { (lValue, fakeObject) -> + when (lValue) { + is UFieldLValue<*, *> -> { + val resolvedRef = state.models.first().eval(lValue.ref) + resolvedLValuesToFakeObjects += UFieldLValue(lValue.sort, resolvedRef, lValue.field) to fakeObject + } + + is UArrayIndexLValue<*, *, *> -> { + val model = state.models.first() + val resolvedRef = model.eval(lValue.ref) + val resolvedIndex = model.eval(lValue.index) + + val uArrayIndexLValue = UArrayIndexLValue( + lValue.sort, + resolvedRef, + resolvedIndex, + lValue.arrayType, + ) + resolvedLValuesToFakeObjects += uArrayIndexLValue to fakeObject + } + + else -> error("Unexpected lValue type: ${lValue::class.java.name}") + } + } + } + @Suppress("unused") private fun resolveException( res: TsMethodResult.TsException, @@ -90,7 +128,8 @@ class TsTestResolver { model: UModelBase, finalStateMemory: UReadOnlyMemory, method: EtsMethod, - ) : TsTestStateResolver(ctx, model, finalStateMemory, method) { + resolvedLValuesToFakeObjects: List, UConcreteHeapRef>>, + ) : TsTestStateResolver(ctx, model, finalStateMemory, method, resolvedLValuesToFakeObjects) { fun resolveState(): TsParametersState { val thisInstance = resolveThisInstance() val parameters = resolveParameters() @@ -107,22 +146,18 @@ open class TsTestStateResolver( private val model: UModelBase, private val finalStateMemory: UReadOnlyMemory, val method: EtsMethod, + val resolvedLValuesToFakeObjects: List, UConcreteHeapRef>>, ) { fun resolveLValue( lValue: ULValue<*, *>, ): TsTestValue { val expr = memory.read(lValue) - val symbolicRef = if (lValue.sort == ctx.addressSort) { - finalStateMemory.read(lValue).asExpr(ctx.addressSort) - } else { - null - } - return resolveExpr(expr, symbolicRef) + + return resolveExpr(expr) } fun resolveExpr( expr: UExpr, - symbolicRef: UExpr? = null, ): TsTestValue = with(ctx) { when (expr.sort) { fp64Sort -> { @@ -139,18 +174,20 @@ open class TsTestStateResolver( } else { this@TsTestStateResolver.resolveTsValue( expr.asExpr(this@TsTestStateResolver.ctx.addressSort), - symbolicRef?.asExpr(this@TsTestStateResolver.ctx.addressSort), ) } } + sizeSort -> { + this@TsTestStateResolver.resolvePrimitive(expr, EtsNumberType) + } + else -> TODO("Unsupported sort: ${expr.sort}") } } private fun resolveTsValue( heapRef: UExpr, - finalStateMemoryRef: UExpr?, ): TsTestValue { val concreteRef = evaluateInModel(heapRef) as UConcreteHeapRef @@ -171,19 +208,19 @@ open class TsTestStateResolver( return when (type) { // TODO add better support is EtsUnclearRefType -> { - resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef) + resolveTsClass(concreteRef, heapRef) } is EtsClassType -> { - resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef) + resolveTsClass(concreteRef, heapRef) } is EtsArrayType -> { - resolveTsArray(concreteRef, finalStateMemoryRef ?: heapRef, type) + resolveTsArray(concreteRef, heapRef, type) } is EtsUnknownType -> { - resolveTsValue(heapRef, finalStateMemoryRef) + resolveTsValue(heapRef) } else -> error("Unexpected type: $type") @@ -196,20 +233,56 @@ open class TsTestStateResolver( type: EtsArrayType, ): TsTestValue.TsArray<*> = with(ctx) { val arrayLength = mkArrayLengthLValue(heapRef, type) - val length = model.eval(memory.read(arrayLength)) as KBitVec32Value + val length = resolveLValue(arrayLength) as TsTestValue.TsNumber - val values = (0 until length.intValue).map { + val values = (0 until length.number.toInt()).map { val index = mkSizeExpr(it) - val lValue = mkArrayIndexLValue(addressSort, heapRef, index, type) - val value = memory.read(lValue) + val sort = typeToSort(type.elementType) - if (model.eval(mkHeapRefEq(value, mkUndefinedValue())).isTrue) { - return@map TsTestValue.TsUndefined + if (sort is TsUnresolvedSort) { + val arrayIndexLValue = mkArrayIndexLValue(addressSort, concreteRef, index, type) + val fakeObject = if (memory is UModel) { + resolvedLValuesToFakeObjects.firstOrNull { it.first == arrayIndexLValue }?.second + } else { + resolvedLValuesToFakeObjects.lastOrNull { it.first == arrayIndexLValue }?.second + } + + fakeObject ?: return@map TsTestValue.TsUndefined + + check(fakeObject.isFakeObject()) + + val fakeType = fakeObject.getFakeType(finalStateMemory) + return@map when { + model.eval(fakeType.fpTypeExpr).isTrue -> { + resolveExpr(fakeObject.extractFp(finalStateMemory)) + } + + model.eval(fakeType.boolTypeExpr).isTrue -> { + resolveExpr(fakeObject.extractBool(finalStateMemory)) + } + + model.eval(fakeType.refTypeExpr).isTrue -> { + resolveExpr(fakeObject.extractRef(finalStateMemory)) + } + + else -> error("Unsupported fake object type: $fakeType") + } } - with(ctx) { check(value.isFakeObject()) { "Only fake objects are allowed in arrays" } } + require(sort is UFpSort || sort is UBoolSort) { + "Other sorts must be resolved above, but got: $sort" + } - resolveFakeObject(value as UConcreteHeapRef) + val lValue = mkArrayIndexLValue(sort, concreteRef, index, type) + val value = memory.read(lValue) + + if (value.sort is UAddressSort) { + if (model.eval(mkHeapRefEq(value.asExpr(addressSort), mkUndefinedValue())).isTrue) { + return@map TsTestValue.TsUndefined + } + } + + resolveExpr(value) } return TsTestValue.TsArray(values) @@ -251,20 +324,20 @@ open class TsTestStateResolver( model.eval(type.boolTypeExpr).isTrue -> { val lValue = getIntermediateBoolLValue(expr.address) val value = finalStateMemory.read(lValue) - resolveExpr(model.eval(value), value) + resolveExpr(model.eval(value)) } model.eval(type.fpTypeExpr).isTrue -> { val lValue = getIntermediateFpLValue(expr.address) val value = finalStateMemory.read(lValue) - resolveExpr(model.eval(value), value) + resolveExpr(model.eval(value)) } model.eval(type.refTypeExpr).isTrue -> { val lValue = getIntermediateRefLValue(expr.address) val value = finalStateMemory.read(lValue) val ref = model.eval(value) - resolveExpr(ref, value) + resolveExpr(ref) } else -> error("Unsupported") @@ -281,9 +354,13 @@ open class TsTestStateResolver( if (e.isFakeObject()) { val lValue = getIntermediateFpLValue(e.address) val value = finalStateMemory.read(lValue) - resolveExpr(model.eval(value), value) + resolveExpr(model.eval(value)) } else { - TsTestValue.TsNumber.TsDouble(e.extractDouble()) + if (e is KFpValue<*>) { + TsTestValue.TsNumber.TsDouble(e.extractDouble()) + } else { + TsTestValue.TsNumber.TsInteger(e.extractInt()) + } } } @@ -360,18 +437,30 @@ open class TsTestStateResolver( val sort = typeToSort(field.type) if (sort == unresolvedSort) { val lValue = mkFieldLValue(addressSort, heapRef, field.signature) - 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 - val obj = resolveExpr(fieldExpr, fieldExpr) - field.name to obj + + val fakeObject = if (memory is UModel) { + resolvedLValuesToFakeObjects.firstOrNull { it.first == lValue }?.second + } else { + resolvedLValuesToFakeObjects.lastOrNull { it.first == lValue }?.second + } + + if (fakeObject != null) { + val obj = resolveFakeObject(fakeObject) + field.name to obj + } else { + 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 + val obj = resolveExpr(fieldExpr) + field.name to obj + } } else { val lValue = mkFieldLValue(sort, concreteRef.asExpr(addressSort), field.signature) val fieldExpr = memory.read(lValue) // 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) + val obj = resolveExpr(fieldExpr) field.name to obj } } diff --git a/usvm-ts/src/test/resources/samples/Arrays.ts b/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts similarity index 83% rename from usvm-ts/src/test/resources/samples/Arrays.ts rename to usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts index 6cbcfcb271..cb74a0db8d 100644 --- a/usvm-ts/src/test/resources/samples/Arrays.ts +++ b/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts @@ -1,7 +1,7 @@ // @ts-nocheck // noinspection JSUnusedGlobalSymbols,UnnecessaryLocalVariableJS -class Arrays { +class AllocatedArrays { createConstantArrayOfNumbers() { let x = [1, 2, 3] if (x[0] === 1) return 1 @@ -63,4 +63,17 @@ class Arrays { x[3] = 4 return x } + + readFakeObjectAndWriteFakeObject(x: any[], y) { + if (x[0] === 1) { + x[0] = y + if (x[0] === 2) { + return x + } else { + return x + } + } + + return x + } } diff --git a/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts new file mode 100644 index 0000000000..cfb7838c78 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts @@ -0,0 +1,48 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols,UnnecessaryLocalVariableJS + +class InputArrays { + inputArrayOfNumbers(x: number[]) { + if (x[0] === 1) return 1 + if (x[0] == undefined) return -1 + return 2 + } + + writeIntoInputArray(x: number[]) { + if (x[0] != 1) { + x[0] = 1; + } + + return x[0]; + } + + idForArrayOfNumbers(x: number[]) { + return x + } + + arrayOfBooleans(x: boolean[]) { + if (x[0] === true) return 1 + return -1 + } + + arrayOfUnknownValues(x: any[]) { + if (x[0] === 1.1) return x + if (x[1] === true) return x + if (x[2] === undefined) return x + return x + } + + writeIntoArrayOfUnknownValues(x: any[]) { + x[1] = true + x[2] = undefined + x[0] = null + return x + } + + rewriteFakeValueInArray(x: any[]) { + if (x[0] === 1) { + x[0] = null + } + return x[0] + } +} diff --git a/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt b/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt index 6849fd5d70..33babda68e 100644 --- a/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt +++ b/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt @@ -20,6 +20,11 @@ val ignoreNumberOfAnalysisResults = AnalysisResultsNumberMatcher( matcherFailedMessage = { _ -> "No analysis results received" } ) { it > 0 } +val noResultsExpected = AnalysisResultsNumberMatcher( + description = "No executions expected", + matcherFailedMessage = { it -> "Expected no analysis results, but $it executions were found" } +) { it == 0 } + class AnalysisResultsNumberMatcher( private val description: String, val matcherFailedMessage: (Int) -> String, From fda07ff53e761c5e8de9d9787cb32e46b54d877b Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 9 Jun 2025 16:34:56 +0300 Subject: [PATCH 2/4] Format --- .../main/kotlin/org/usvm/machine/TsContext.kt | 1 - .../org/usvm/machine/expr/TsExprResolver.kt | 5 +++-- .../org/usvm/machine/expr/TsExpressions.kt | 16 ++++++++++------ .../usvm/machine/operator/TsBinaryOperator.kt | 4 ++++ .../kotlin/org/usvm/machine/state/TsState.kt | 2 +- .../org/usvm/machine/types/TsTypeSystem.kt | 2 +- .../main/kotlin/org/usvm/util/EtsHierarchy.kt | 3 +-- usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt | 4 ++-- .../test/kotlin/org/usvm/util/TsTestResolver.kt | 12 ++++++------ 9 files changed, 28 insertions(+), 21 deletions(-) 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 d6f482d69a..45bdcf2833 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -52,7 +52,6 @@ class TsContext( val voidSort: TsVoidSort by lazy { TsVoidSort(this) } val voidValue: TsVoidValue by lazy { TsVoidValue(this) } - /** * In TS we treat undefined value as a null reference in other objects. * For real null represented in the language we create another reference. 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 23ad166f9d..72d8387f95 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 @@ -657,7 +657,6 @@ class TsExprResolver( fakeObj } - } } else { val lValue = mkArrayIndexLValue( @@ -754,7 +753,9 @@ class TsExprResolver( val fakeRef = if (ref.isFakeObject()) { ref } else { - mkFakeValue(scope, bool, fp, ref).also { lValuesToAllocatedFakeObjects += refLValue to it } + mkFakeValue(scope, bool, fp, ref).also { + lValuesToAllocatedFakeObjects += refLValue to it + } } memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr) 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 2baa334243..9a3343b5a5 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 @@ -73,26 +73,30 @@ class TsVoidSort(ctx: TsContext) : USort(ctx) { } } -fun UExpr.toConcreteBoolValue(): Boolean = when (this) { +fun UExpr<*>.toConcreteBoolValue(): Boolean = when (this) { ctx.trueExpr -> true ctx.falseExpr -> false - else -> error("Cannot extract boolean from $this") + else -> error("Cannot extract Boolean from $this") } -fun UExpr.extractDouble(): Double { +/** + * Extracts a double value from [this] expression if possible. + * Otherwise, throws an error. + */ +fun UExpr<*>.extractDouble(): Double { if (this@extractDouble is KFp64Value) { return value } - error("Cannot extract double from $this") + error("Cannot extract Double from $this") } /** * Extracts an integer value from [this] expression if possible. * Otherwise, throws an error. */ -fun UExpr.extractInt(): Int { +fun UExpr<*>.extractInt(): Int { if (this@extractInt is KBitVec32Value) { return intValue } - error("Cannot extract int from $this") + error("Cannot extract Int from $this") } 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 61fe75b120..abd648eda7 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 @@ -573,6 +573,7 @@ sealed interface TsBinaryOperator { lhsValue = lhs.extractBool(scope) lhsType.boolTypeExpr } + fp64Sort -> { lhsValue = lhs.extractFp(scope) lhsType.fpTypeExpr @@ -582,6 +583,7 @@ sealed interface TsBinaryOperator { lhsValue = lhs.extractRef(scope) lhsType.refTypeExpr } + else -> error("Unsupported sort ${rhs.sort}") } } @@ -593,6 +595,7 @@ sealed interface TsBinaryOperator { rhsValue = rhs.extractBool(scope) rhsType.boolTypeExpr } + fp64Sort -> { rhsValue = rhs.extractFp(scope) rhsType.fpTypeExpr @@ -602,6 +605,7 @@ sealed interface TsBinaryOperator { rhsValue = rhs.extractRef(scope) rhsType.refTypeExpr } + else -> error("Unsupported sort ${lhs.sort}") } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index fa69925170..38d8b66d18 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -47,7 +47,7 @@ class TsState( val localToSortStack: MutableList> = mutableListOf(persistentHashMapOf()), var staticStorage: UPersistentHashMap = persistentHashMapOf(), val globalObject: UConcreteHeapRef = memory.allocStatic(EtsClassType(EtsClassSignature.UNKNOWN)), - val addedArtificialLocals: MutableSet = hashSetOf(), + val addedArtificialLocals: MutableSet = hashSetOf(), val lValuesToAllocatedFakeObjects: MutableList, UConcreteHeapRef>> = mutableListOf(), ) : UState( ctx = ctx, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 2ce9755a22..ddb0bb9e6e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -328,4 +328,4 @@ fun EtsClassType.toAuxiliaryType(hierarchy: EtsHierarchy): EtsAuxiliaryType? { return EtsAuxiliaryType( properties = fieldsIntersection + methodsIntersection ) -} \ No newline at end of file +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index 54351714c1..359c64a003 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -108,7 +108,6 @@ class EtsHierarchy(private val scene: EtsScene) { return suitableClasses.values } - companion object { // TODO use real one val OBJECT_CLASS = EtsClassType( @@ -135,4 +134,4 @@ fun ClassName.removeTrashFromTheName(): ClassName { } else { nameWithoutGenerics().removePrefixWithDots() } -} \ No newline at end of file +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt index 2e3e147ac9..b05ba6d4ca 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt @@ -41,7 +41,7 @@ fun EtsType.isResolved(): Boolean = this !is EtsUnclearRefType && (this as? EtsClassType)?.signature?.file != EtsFileSignature.UNKNOWN fun EtsType.getClassesForType( - scene: EtsScene + scene: EtsScene, ): List = if (isResolved()) { scene .projectAndSdkClasses @@ -74,4 +74,4 @@ fun UHeapRef.createFakeField(fieldName: String, scope: TsStepScope): UConcreteHe } return fakeObject -} \ 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 7ee7b03e55..e995509fde 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -92,21 +92,21 @@ class TsTestResolver { when (lValue) { is UFieldLValue<*, *> -> { val resolvedRef = state.models.first().eval(lValue.ref) - resolvedLValuesToFakeObjects += UFieldLValue(lValue.sort, resolvedRef, lValue.field) to fakeObject + val fieldLValue = UFieldLValue(lValue.sort, resolvedRef, lValue.field) + resolvedLValuesToFakeObjects += fieldLValue to fakeObject } is UArrayIndexLValue<*, *, *> -> { val model = state.models.first() val resolvedRef = model.eval(lValue.ref) val resolvedIndex = model.eval(lValue.index) - - val uArrayIndexLValue = UArrayIndexLValue( + val arrayIndexLValue = UArrayIndexLValue( lValue.sort, resolvedRef, resolvedIndex, lValue.arrayType, ) - resolvedLValuesToFakeObjects += uArrayIndexLValue to fakeObject + resolvedLValuesToFakeObjects += arrayIndexLValue to fakeObject } else -> error("Unexpected lValue type: ${lValue::class.java.name}") @@ -235,8 +235,8 @@ open class TsTestStateResolver( val arrayLength = mkArrayLengthLValue(heapRef, type) val length = resolveLValue(arrayLength) as TsTestValue.TsNumber - val values = (0 until length.number.toInt()).map { - val index = mkSizeExpr(it) + val values = (0 until length.number.toInt()).map { i -> + val index = mkSizeExpr(i) val sort = typeToSort(type.elementType) if (sort is TsUnresolvedSort) { From 5f317ecaf8832833cddd971a2b6a37f5a80de5ee Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 9 Jun 2025 16:58:03 +0300 Subject: [PATCH 3/4] Replace map with forEach --- usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 e995509fde..cdef32cfb6 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -88,7 +88,7 @@ class TsTestResolver { } private fun prepareForResolve(state: TsState) { - state.lValuesToAllocatedFakeObjects.map { (lValue, fakeObject) -> + state.lValuesToAllocatedFakeObjects.forEach { (lValue, fakeObject) -> when (lValue) { is UFieldLValue<*, *> -> { val resolvedRef = state.models.first().eval(lValue.ref) From 4994227c9d3967d69883a6a90a7d6c27d41d61f6 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 10 Jun 2025 17:42:44 +0300 Subject: [PATCH 4/4] Review fixes --- .../kotlin/org/usvm/machine/expr/TsExprResolver.kt | 10 +++++++--- .../src/test/kotlin/org/usvm/util/TsTestResolver.kt | 8 ++++++-- .../kotlin/org/usvm/test/util/checkers/Matchers.kt | 2 +- 3 files changed, 14 insertions(+), 6 deletions(-) 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 72d8387f95..dde7a449be 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 @@ -788,7 +788,7 @@ class TsExprResolver( val fakeType = instanceRef.getFakeType(scope) // If we want to get length from a fake object, we assume that it is an array. - scope.assert(fakeType.refTypeExpr) + scope.doWithState { pathConstraints += fakeType.refTypeExpr } val refLValue = getIntermediateRefLValue(instanceRef.address) val obj = scope.calcOnState { memory.read(refLValue) } @@ -872,6 +872,12 @@ class TsExprResolver( } override fun visit(expr: EtsNewArrayExpr): UExpr? = with(ctx) { + val arrayType = expr.type + + require(arrayType is EtsArrayType) { + "Expected EtsArrayType in newArrayExpr, but got ${arrayType::class.simpleName}" + } + scope.calcOnState { val size = resolve(expr.size) ?: return@calcOnState null @@ -902,8 +908,6 @@ class TsExprResolver( blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type ) - val arrayType = expr.type as EtsArrayType - if (arrayType.elementType is EtsArrayType) { TODO("Multidimensional arrays are not supported yet, https://github.com/UnitTestBot/usvm/issues/287") } 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 cdef32cfb6..fcaca8fa1f 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -109,7 +109,9 @@ class TsTestResolver { resolvedLValuesToFakeObjects += arrayIndexLValue to fakeObject } - else -> error("Unexpected lValue type: ${lValue::class.java.name}") + else -> { + error("Unexpected lValue type: ${lValue::class.java.name}") + } } } } @@ -265,7 +267,9 @@ open class TsTestStateResolver( resolveExpr(fakeObject.extractRef(finalStateMemory)) } - else -> error("Unsupported fake object type: $fakeType") + else -> { + error("Unsupported fake object type: $fakeType") + } } } diff --git a/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt b/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt index 33babda68e..b132696cf1 100644 --- a/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt +++ b/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt @@ -22,7 +22,7 @@ val ignoreNumberOfAnalysisResults = AnalysisResultsNumberMatcher( val noResultsExpected = AnalysisResultsNumberMatcher( description = "No executions expected", - matcherFailedMessage = { it -> "Expected no analysis results, but $it executions were found" } + matcherFailedMessage = { "Expected no analysis results, but $it executions were found" } ) { it == 0 } class AnalysisResultsNumberMatcher(