From f24af7d80e7c9406b5e7ffbb6fd4564d9519bb6b Mon Sep 17 00:00:00 2001 From: Yury Kamenev Date: Wed, 15 Nov 2023 03:08:02 -0800 Subject: [PATCH] Enabled some usvm-jvm tests (#103) --- .../org/usvm/types/SupportTypeStream.kt | 3 + .../main/kotlin/org/usvm/types/TypeStream.kt | 11 ++ usvm-jvm/build.gradle.kts | 2 +- .../kotlin/org/usvm/api/util/JcClassLoader.kt | 57 ++++++++++ .../org/usvm/api/util/JcTestInterpreter.kt | 14 ++- .../org/usvm/machine/JcApproximations.kt | 8 +- .../main/kotlin/org/usvm/machine/JcContext.kt | 5 +- .../machine/interpreter/JcExprResolver.kt | 43 ++++++-- .../usvm/machine/interpreter/JcInterpreter.kt | 66 +++++++++-- .../interpreter/JcVirtualInvokeResolver.kt | 103 +++++++++++++++--- .../samples/java/org/usvm/api/mock/UMock.kt | 9 +- .../org/usvm/samples/algorithms/Sort.java | 4 + .../arrays/ArrayStoreExceptionExamples.java | 33 +++++- .../samples/arrays/FinalStaticFieldArray.java | 6 +- .../org/usvm/samples/enums/ClassWithEnum.java | 22 +++- .../usvm/samples/invokes/InvokeExample.java | 5 +- .../usvm/samples/math/DoubleFunctions.java | 7 +- .../usvm/samples/numbers/ArithmeticUtils.java | 2 +- .../objects/ObjectWithRefFieldExample.java | 5 +- .../org/usvm/samples/algorithms/SortTest.kt | 7 +- .../ApproximationsExampleTest.kt | 3 +- .../approximations/ApproximationsTest.kt | 9 +- .../ArrayListSpliteratorApproximationsTest.kt | 30 +++-- .../usvm/samples/arrays/ArrayOfObjectsTest.kt | 4 +- .../arrays/ArrayStoreExceptionExamplesTest.kt | 43 +++++--- .../arrays/ArraysOverwriteValueTest.kt | 2 - .../arrays/FinalStaticFieldArrayTest.kt | 2 - .../usvm/samples/arrays/IntArrayBasicsTest.kt | 23 ++-- .../samples/arrays/PrimitiveArraysTest.kt | 2 - .../samples/arrays/TestMultiDimensional.kt | 2 +- .../samples/casts/ArrayCastExampleTest.kt | 4 - .../org/usvm/samples/casts/CastClassTest.kt | 2 - .../org/usvm/samples/casts/CastExampleTest.kt | 5 +- .../samples/casts/GenericCastExampleTest.kt | 14 ++- .../samples/casts/InstanceOfExampleTest.kt | 2 - .../ClassWithStaticAndInnerClassesTest.kt | 2 - .../codegen/deepequals/DeepEqualsTest.kt | 14 ++- .../usvm/samples/controlflow/CyclesTest.kt | 3 - .../usvm/samples/enums/ClassWithEnumTest.kt | 16 ++- .../usvm/samples/invokes/InvokeExampleTest.kt | 2 - .../invokes/VirtualInvokeExampleTest.kt | 8 +- .../lambda/CustomPredicateExampleTest.kt | 15 +-- .../lambda/SimpleLambdaExamplesTest.kt | 2 +- .../usvm/samples/math/DoubleFunctionsTest.kt | 26 +++-- .../org/usvm/samples/mixed/SimplifierTest.kt | 2 - .../aliasing/AliasingInParamsExampleTest.kt | 3 +- .../samples/numbers/ArithmeticUtilsTest.kt | 9 +- .../objects/ObjectWithRefFieldsExampleTest.kt | 2 - .../samples/primitives/DoubleExamplesTest.kt | 59 +++++----- .../org/usvm/samples/structures/HeapTest.kt | 2 - .../samples/structures/MinStackExampleTest.kt | 13 +-- .../structures/StandardStructuresTest.kt | 11 +- 52 files changed, 511 insertions(+), 237 deletions(-) create mode 100644 usvm-jvm/src/main/kotlin/org/usvm/api/util/JcClassLoader.kt diff --git a/usvm-core/src/main/kotlin/org/usvm/types/SupportTypeStream.kt b/usvm-core/src/main/kotlin/org/usvm/types/SupportTypeStream.kt index 5437547c7c..a68e0e6acc 100644 --- a/usvm-core/src/main/kotlin/org/usvm/types/SupportTypeStream.kt +++ b/usvm-core/src/main/kotlin/org/usvm/types/SupportTypeStream.kt @@ -90,6 +90,9 @@ class USupportTypeStream private constructor( override val isEmpty: Boolean get() = take(1).isEmpty() + override val commonSuperType: Type + get() = supportType + companion object { fun from(typeSystem: UTypeSystem, type: Type): USupportTypeStream { val root = rootSequence(typeSystem, type).filter(typeSystem::isInstantiable) diff --git a/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt b/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt index 216d392836..321e057b07 100644 --- a/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt +++ b/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt @@ -48,6 +48,11 @@ interface UTypeStream { fun take(n: Int): Collection val isEmpty: Boolean + + /** + * Stores a supertype that satisfies current type constraints and other satisfying types are inheritors of this type. + */ + val commonSuperType: Type? } /** @@ -66,6 +71,9 @@ object UEmptyTypeStream : UTypeStream { override val isEmpty: Boolean get() = true + + override val commonSuperType: Nothing? + get() = null } @Suppress("UNCHECKED_CAST") @@ -119,4 +127,7 @@ class USingleTypeStream( override val isEmpty: Boolean get() = false + + override val commonSuperType: Type + get() = singleType } diff --git a/usvm-jvm/build.gradle.kts b/usvm-jvm/build.gradle.kts index d18df61dea..1be7115f75 100644 --- a/usvm-jvm/build.gradle.kts +++ b/usvm-jvm/build.gradle.kts @@ -16,7 +16,7 @@ val `usvm-api` by sourceSets.creating { val approximations by configurations.creating val approximationsRepo = "com.github.UnitTestBot.java-stdlib-approximations" -val approximationsVersion = "53ceeb23ea" +val approximationsVersion = "fcfd10e495" dependencies { implementation(project(":usvm-core")) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcClassLoader.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcClassLoader.kt new file mode 100644 index 0000000000..834a964a0d --- /dev/null +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcClassLoader.kt @@ -0,0 +1,57 @@ +package org.usvm.api.util + +import org.jacodb.api.JcClassOrInterface +import org.jacodb.api.JcRefType +import org.jacodb.api.ext.allSuperHierarchySequence +import org.jacodb.api.ext.toType +import java.nio.ByteBuffer +import java.security.CodeSource +import java.security.SecureClassLoader + +/** + * Loads known classes using [ClassLoader.getSystemClassLoader], or defines them using bytecode from jacodb if they are unknown. + */ +object JcClassLoader : SecureClassLoader(ClassLoader.getSystemClassLoader()) { + fun loadClass(jcClass: JcClassOrInterface): Class<*> = defineClassRecursively(jcClass) + + private fun defineClass(name: String, code: ByteArray): Class<*> { + return defineClass(name, ByteBuffer.wrap(code), null as CodeSource?) + } + + private fun defineClassRecursively(jcClass: JcClassOrInterface): Class<*> = + defineClassRecursively(jcClass, hashSetOf()) + + private fun defineClassRecursively( + jcClass: JcClassOrInterface, + visited: MutableSet + ): Class<*> { + visited += jcClass + + return try { + // We cannot redefine a class that was already defined + loadClass(jcClass.name) + } catch (e: ClassNotFoundException) { + with(jcClass) { + // For unknown class we need to load all its supers, all classes mentioned in its ALL (not only declared) + // fields (as they are used in resolving), and then define the class itself using its bytecode from jacodb + + val notVisitedSupers = allSuperHierarchySequence.filterNot { it in visited } + notVisitedSupers.forEach { defineClassRecursively(it, visited) } + + val classType = toType() + val notVisitedRefFieldTypes = classType + .fields + .asSequence() + .map { it.fieldType } + .filterIsInstance() + .map { it.jcClass } + .filterNot { it in visited } + + notVisitedRefFieldTypes.forEach { defineClassRecursively(it, visited) } + + return defineClass(name, bytecode()) + } + } + } +} + diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestInterpreter.kt index 5cac82d355..dfe4a7e309 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestInterpreter.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestInterpreter.kt @@ -64,7 +64,7 @@ import org.usvm.types.firstOrNull * @param classLoader a class loader to load target classes. */ class JcTestInterpreter( - private val classLoader: ClassLoader = ClassLoader.getSystemClassLoader(), + private val classLoader: ClassLoader = JcClassLoader, ): JcTestResolver { /** * Resolves a [JcTest] from a [method] from a [state]. @@ -122,7 +122,7 @@ class JcTestInterpreter( private val model: UModelBase, private val memory: UReadOnlyMemory, private val method: JcTypedMethod, - private val classLoader: ClassLoader = ClassLoader.getSystemClassLoader(), + private val classLoader: ClassLoader = JcClassLoader, ) { private val resolvedCache = mutableMapOf() @@ -350,7 +350,7 @@ class JcTestInterpreter( else -> error("Unexpected type: $elementType") } - } ?: classLoader.loadClass(type.jcClass.name) + } ?: classLoader.loadClass(type.jcClass) /** * If we resolve state after, [expr] is read from a state memory, so it requires concretization via [model]. @@ -365,4 +365,10 @@ class JcTestInterpreter( private fun JcRefType.getEnumAncestorOrNull(): JcClassOrInterface? = (sequenceOf(jcClass) + jcClass.allSuperHierarchySequence).firstOrNull { it.isEnum } } -} \ No newline at end of file +} + +fun ClassLoader.loadClass(jcClass: JcClassOrInterface): Class<*> = if (this is JcClassLoader) { + loadClass(jcClass) +} else { + loadClass(jcClass.name) +} diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt index 63f7466a63..9737ebd28f 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt @@ -62,7 +62,6 @@ import org.usvm.machine.state.newStmt import org.usvm.machine.state.skipMethodInvocationWithValue import org.usvm.sizeSort import org.usvm.types.first -import org.usvm.types.single import org.usvm.types.singleOrNull import org.usvm.util.allocHeapRef import org.usvm.util.write @@ -353,12 +352,9 @@ class JcMethodApproximationResolver( private fun approximateArrayClone(methodCall: JcMethodCall): Boolean { val instance = methodCall.arguments.first().asExpr(ctx.addressSort) - if (instance !is UConcreteHeapRef) { - return false - } val arrayType = scope.calcOnState { - (memory.types.getTypeStream(instance).single()) + memory.types.getTypeStream(instance).commonSuperType } if (arrayType !is JcArrayType) { return false @@ -370,7 +366,7 @@ class JcMethodApproximationResolver( private fun JcExprResolver.resolveArrayClone( methodCall: JcMethodCall, - instance: UConcreteHeapRef, + instance: UHeapRef, arrayType: JcArrayType, ) = with(ctx) { scope.doWithState { diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt index 1ad83a30d1..b2ab2c2ad0 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt @@ -107,8 +107,9 @@ class JcContext( stringType.jcClass.toType().declaredFields.first { it.name == "value" } } - val stringCoderField: JcTypedField by lazy { - stringType.jcClass.toType().declaredFields.first { it.name == "coder" } + // The `coder` field is not presented in java 8, so return null if is missed + val stringCoderField: JcTypedField? by lazy { + stringType.jcClass.toType().declaredFields.firstOrNull { it.name == "coder" } } // Do not use JcTypedField here as its type is not required, however JcTypedField does not have required overridden `equals` method diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt index 304c879696..6b8674356b 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt @@ -11,6 +11,7 @@ import org.jacodb.api.JcMethod import org.jacodb.api.JcPrimitiveType import org.jacodb.api.JcRefType import org.jacodb.api.JcType +import org.jacodb.api.JcTypeVariable import org.jacodb.api.JcTypedField import org.jacodb.api.JcTypedMethod import org.jacodb.api.PredefinedPrimitives @@ -78,7 +79,6 @@ import org.jacodb.api.ext.enumValues import org.jacodb.api.ext.float import org.jacodb.api.ext.ifArrayGetElementType import org.jacodb.api.ext.int -import org.jacodb.api.ext.isAssignable import org.jacodb.api.ext.isEnum import org.jacodb.api.ext.long import org.jacodb.api.ext.objectType @@ -146,8 +146,9 @@ class JcExprResolver( * @return a symbolic expression, with the sort corresponding to the [type]. */ fun resolveJcExpr(expr: JcExpr, type: JcType = expr.type): UExpr? { - val resolvedExpr = if (expr.type != type) { - resolveCast(expr, type) + val resolvedExpr = if (expr.type != type && type is JcPrimitiveType) { + // Only primitive casts may appear here because reference casts are handled with cast instruction + resolvePrimitiveCast(expr, type) } else { expr.accept(this) } ?: return null @@ -311,7 +312,9 @@ class JcExprResolver( ): UExpr = simpleValueResolver.visitJcClassConstant(value) // endregion - override fun visitJcCastExpr(expr: JcCastExpr): UExpr? = resolveCast(expr.operand, expr.type) + override fun visitJcCastExpr(expr: JcCastExpr): UExpr? = + // Note that primitive types may appear in JcCastExpr + resolveCast(expr.operand, expr.type) override fun visitJcInstanceOfExpr(expr: JcInstanceOfExpr): UExpr? = with(ctx) { val ref = resolveJcExpr(expr.operand)?.asExpr(addressSort) ?: return null @@ -334,7 +337,7 @@ class JcExprResolver( } override fun visitJcNewArrayExpr(expr: JcNewArrayExpr): UExpr? = with(ctx) { - val size = resolveCast(expr.dimensions[0], ctx.cp.int)?.asExpr(bv32Sort) ?: return null + val size = resolvePrimitiveCast(expr.dimensions[0], ctx.cp.int)?.asExpr(bv32Sort) ?: return null // TODO: other dimensions ( > 1) checkNewArrayLength(size) ?: return null @@ -724,7 +727,7 @@ class JcExprResolver( val arrayDescriptor = arrayDescriptorOf(array.type as JcArrayType) - val idx = resolveCast(index, ctx.cp.int)?.asExpr(bv32Sort) ?: return null + val idx = resolvePrimitiveCast(index, ctx.cp.int)?.asExpr(bv32Sort) ?: return null val lengthRef = UArrayLengthLValue(arrayRef, arrayDescriptor, sizeSort) val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) } @@ -859,8 +862,13 @@ class JcExprResolver( typeBefore: JcRefType, type: JcRefType, ): UHeapRef? { - return if (!typeBefore.isAssignable(type)) { + check(type !is JcTypeVariable) { + "Unexpected type variable $type" + } + + return if (!ctx.typeSystem().isSupertype(type, typeBefore)) { val isExpr = scope.calcOnState { memory.types.evalIsSubtype(expr, type) } + scope.fork( isExpr, blockOnFalseState = allocateException(ctx.classCastExceptionType) @@ -871,6 +879,18 @@ class JcExprResolver( } } + private fun resolvePrimitiveCast( + expr: JcExpr, + type: JcPrimitiveType + ): UExpr? = resolveAfterResolved(expr) { + val exprType = expr.type + check(exprType is JcPrimitiveType) { + "Trying cast not primitive type $exprType to primitive type $type" + } + + resolvePrimitiveCast(it, exprType, type) + } + private fun resolvePrimitiveCast( expr: UExpr, typeBefore: JcPrimitiveType, @@ -1032,7 +1052,6 @@ class JcSimpleValueResolver( // Equal string constants always have equal references val ref = resolveStringConstant(value.value) val stringValueLValue = UFieldLValue(addressSort, ref, stringValueField.field) - val stringCoderLValue = UFieldLValue(byteSort, ref, stringCoderField.field) // String.value type depends on the JVM version val charValues = when (stringValueField.fieldType.ifArrayGetElementType) { @@ -1055,7 +1074,13 @@ class JcSimpleValueResolver( // String constants are immutable. Therefore, it is correct to overwrite value, coder and type. memory.write(stringValueLValue, charArrayRef) - memory.write(stringCoderLValue, mkBv(0, byteSort)) + + // Write coder only if it is presented (depends on the JVM version) + stringCoderField?.let { + val stringCoderLValue = UFieldLValue(byteSort, ref, it.field) + memory.write(stringCoderLValue, mkBv(0, byteSort)) + } + memory.types.allocate(ref.address, stringType) ref diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt index 87f949739c..1bf4559ae2 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt @@ -29,6 +29,7 @@ import org.jacodb.api.cfg.JcThis import org.jacodb.api.cfg.JcThrowInst import org.jacodb.api.ext.boolean import org.jacodb.api.ext.cfg.callExpr +import org.jacodb.api.ext.ifArrayGetElementType import org.jacodb.api.ext.isEnum import org.jacodb.api.ext.void import org.usvm.ForkCase @@ -36,10 +37,14 @@ import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UBoolExpr import org.usvm.UConcreteHeapRef +import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.UInterpreter +import org.usvm.USort import org.usvm.api.allocateStaticRef +import org.usvm.api.evalTypeEquals import org.usvm.api.targets.JcTarget +import org.usvm.collection.array.UArrayIndexLValue import org.usvm.forkblacklists.UForkBlackList import org.usvm.machine.JcApplicationGraph import org.usvm.machine.JcConcreteMethodCallInst @@ -63,11 +68,10 @@ import org.usvm.machine.state.returnValue import org.usvm.machine.state.skipMethodInvocationWithValue import org.usvm.machine.state.throwExceptionAndDropStackFrame import org.usvm.machine.state.throwExceptionWithoutStackFrameDrop +import org.usvm.memory.ULValue import org.usvm.memory.URegisterStackLValue import org.usvm.solver.USatResult import org.usvm.targets.UTargetsSet -import org.usvm.types.first -import org.usvm.util.findMethod import org.usvm.util.write typealias JcStepScope = StepScope @@ -97,7 +101,15 @@ class JcInterpreter( val ref = state.memory.read(thisLValue).asExpr(addressSort) state.pathConstraints += mkEq(ref, nullRef).not() val thisType = typedMethod.enclosingType - state.pathConstraints += mkIsSubtypeExpr(ref, thisType) + + // TODO support virtual entrypoints https://github.com/UnitTestBot/usvm/issues/93 + val thisTypeConstraints = if (thisType.jcClass.isAbstract) { + state.memory.types.evalIsSubtype(ref, thisType) + } else { + state.memory.types.evalTypeEquals(ref, thisType) + } + + state.pathConstraints += thisTypeConstraints entrypointArguments += thisType to ref } @@ -291,11 +303,51 @@ class JcInterpreter( val lvalue = exprResolver.resolveLValue(stmt.lhv) ?: return val expr = exprResolver.resolveJcExpr(stmt.rhv, stmt.lhv.type) ?: return - val nextStmt = stmt.nextStmt - scope.doWithState { - memory.write(lvalue, expr) - newStmt(nextStmt) + val noArrayStoreException = checkArrayStoreException(lvalue, expr, scope) + + scope.fork( + noArrayStoreException, + blockOnTrueState = { + val nextStmt = stmt.nextStmt + memory.write(lvalue, expr) + newStmt(nextStmt) + }, + blockOnFalseState = exprResolver.allocateException(ctx.arrayStoreExceptionType) + ) + } + + // Returns `trueExpr` if ArrayStoreException is impossible + private fun checkArrayStoreException( + lvalue: ULValue<*, *>, + rvalue: UExpr, + scope: JcStepScope + ): UBoolExpr { + if (lvalue !is UArrayIndexLValue<*, *, *>) { + return ctx.trueExpr } + + // ArrayStoreException is possible only for references + if (rvalue.sort != ctx.addressSort) { + return ctx.trueExpr + } + + check(lvalue.sort == rvalue.sort) { + "Writing $rvalue with sort ${rvalue.sort} to the array with different sort ${lvalue.sort} by lvalue $lvalue found" + } + + // ArrayStoreException happens if we write a value that is not a subtype of the element type + val isRvalueSubtypeOf = scope.calcOnState { + // The type stored in ULValue is array descriptor and for object arrays it equals just to Object, + // so we need to retrieve the real array type with another way + val arrayType = memory.types.getTypeStream(lvalue.ref).commonSuperType + ?: error("No type found for array ${lvalue.ref}") + val elementType = arrayType.ifArrayGetElementType + ?: error("Not array type $arrayType found for array ${lvalue.ref}") + + memory.types.evalIsSubtype(rvalue.asExpr(ctx.addressSort), elementType) + } + + return isRvalueSubtypeOf } private fun visitIfStmt(scope: JcStepScope, stmt: JcIfInst) { diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcVirtualInvokeResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcVirtualInvokeResolver.kt index 2172f427bb..cdceb228c0 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcVirtualInvokeResolver.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcVirtualInvokeResolver.kt @@ -1,7 +1,13 @@ package org.usvm.machine.interpreter +import io.ksmt.expr.KExpr +import io.ksmt.sort.KBoolSort import io.ksmt.utils.asExpr +import org.jacodb.api.JcClassOrInterface +import org.jacodb.api.JcRefType import org.jacodb.api.JcType +import org.jacodb.api.ext.enumValues +import org.jacodb.api.ext.isEnum import org.jacodb.api.ext.toType import org.usvm.UBoolExpr import org.usvm.UConcreteHeapRef @@ -68,17 +74,25 @@ private fun resolveVirtualInvokeWithModel( if (isAllocatedConcreteHeapRef(concreteRef) || isStaticHeapRef(concreteRef)) { val callSite = findLambdaCallSite(methodCall, scope, concreteRef) - val concreteCall = if (callSite != null) { - makeLambdaCallSiteCall(callSite) + if (callSite != null) { + val lambdaCall = makeLambdaCallSiteCall(callSite) + scope.doWithState { + newStmt(lambdaCall) + } } else { - makeConcreteMethodCall(scope, concreteRef, methodCall) - } - - scope.doWithState { - newStmt(concreteCall) + val concreteInvokes = prepareVirtualInvokeOnConcreteRef( + scope, + concreteRef, + ctx, + methodCall, + instance, + condition = ctx.trueExpr + ) + + scope.forkMulti(concreteInvokes) } - return@with + return } // Resolved lambda call site can't be an input ref @@ -96,6 +110,66 @@ private fun resolveVirtualInvokeWithModel( scope.forkMulti(typeConstraintsWithBlockOnStates) } +private fun JcVirtualMethodCallInst.prepareVirtualInvokeOnConcreteRef( + scope: JcStepScope, + concreteRef: UConcreteHeapRef, + ctx: JcContext, + methodCall: JcVirtualMethodCallInst, + instance: UHeapRef, + condition: UBoolExpr, +): List Unit>> { + // We have only one type for allocated and static heap refs + val type = scope.calcOnState { memory.typeStreamOf(concreteRef) }.single() as JcRefType + val superClass = type.jcClass.superClass + + if (superClass?.isEnum == true) { + // We need to process abstract enums differently - make not type equality conditions + // but ref equalities on enum constant refs + return prepareVirtualInvokeOnAbstractEnum(superClass, ctx, scope, methodCall, instance, condition) + } + + val state = { state: JcState -> + val concreteCall = makeConcreteMethodCall(methodCall, type) + state.newStmt(concreteCall) + } + + return listOf(condition to state) +} + +private fun JcVirtualMethodCallInst.prepareVirtualInvokeOnAbstractEnum( + superClass: JcClassOrInterface, + ctx: JcContext, + scope: JcStepScope, + methodCall: JcVirtualMethodCallInst, + instance: UHeapRef, + condition: UBoolExpr +): List, (JcState) -> Unit>> { + val superType = superClass.toType() + // With enums, we need to fork on all enum types, in spite of type selector + val enumConstantFields = superType.jcClass.enumValues ?: error("No enum constants found at enum type $superType") + val curState = scope.calcOnState { this } + + val enumConstantRefs = enumConstantFields.map { + val staticFieldLValue = JcStaticFieldLValue(it, ctx, ctx.addressSort) + curState.memory.read(staticFieldLValue) + } + + return enumConstantRefs.map { enumRef -> + val enumConstantType = curState.memory.types.getTypeStream(enumRef).single() + + val enumConstantState = { state: JcState -> + val concreteCall = makeConcreteMethodCall(methodCall, enumConstantType) + state.newStmt(concreteCall) + } + + with(ctx) { + val equalToEnumRefCondition = mkHeapRefEq(instance, enumRef) + + mkAnd(condition, equalToEnumRefCondition) to enumConstantState + } + } +} + private fun resolveVirtualInvokeWithoutModel( ctx: JcContext, methodCall: JcVirtualMethodCallInst, @@ -138,8 +212,7 @@ private fun resolveVirtualInvokeWithoutModel( val conditionsWithBlocks = refsWithConditions.flatMapTo(mutableListOf()) { (ref, condition) -> when { isAllocatedConcreteHeapRef(ref) || isStaticHeapRef(ref) -> { - val concreteCall = makeConcreteMethodCall(scope, ref, methodCall) - listOf(condition to { state: JcState -> state.newStmt(concreteCall) }) + prepareVirtualInvokeOnConcreteRef(scope, ref, ctx, methodCall, instance, condition) } ref is USymbolicHeapRef -> { val state = scope.calcOnState { this } @@ -174,13 +247,9 @@ private fun resolveVirtualInvokeWithoutModel( } private fun JcVirtualMethodCallInst.makeConcreteMethodCall( - scope: JcStepScope, - concreteRef: UConcreteHeapRef, methodCall: JcVirtualMethodCallInst, + type: JcType, ): JcConcreteMethodCallInst { - // We have only one type for allocated and static heap refs - val type = scope.calcOnState { memory.typeStreamOf(concreteRef) }.single() - val concreteMethod = type.findMethod(method) ?: error("Can't find method $method in type ${type.typeName}") @@ -216,7 +285,9 @@ private fun JcVirtualMethodCallInst.makeConcreteCallsForPossibleTypes( newState.newStmt(concreteCall) } - with(ctx) { (condition and isExpr) to block } + with(ctx) { + (condition and isExpr) to block + } } if (forkOnRemainingTypes) { diff --git a/usvm-jvm/src/samples/java/org/usvm/api/mock/UMock.kt b/usvm-jvm/src/samples/java/org/usvm/api/mock/UMock.kt index af7c0a9453..41847a1c7c 100644 --- a/usvm-jvm/src/samples/java/org/usvm/api/mock/UMock.kt +++ b/usvm-jvm/src/samples/java/org/usvm/api/mock/UMock.kt @@ -1,9 +1,8 @@ package org.usvm.api.mock -import org.usvm.api.exception.UMockAssumptionViolatedException +import org.usvm.api.Engine fun assume(predicate: Boolean) { - if (!predicate) { - throw UMockAssumptionViolatedException() - } -} \ No newline at end of file + // TODO inline it + Engine.assume(predicate) +} diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/algorithms/Sort.java b/usvm-jvm/src/samples/java/org/usvm/samples/algorithms/Sort.java index 687c83ca59..f438479d37 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/algorithms/Sort.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/algorithms/Sort.java @@ -102,6 +102,10 @@ public int[] defaultSort(int[] array) { throw new IllegalArgumentException(); } + if (array.length > 4) { + throw new IllegalArgumentException(); + } + array[0] = 200; array[1] = 100; array[2] = 0; diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/arrays/ArrayStoreExceptionExamples.java b/usvm-jvm/src/samples/java/org/usvm/samples/arrays/ArrayStoreExceptionExamples.java index 0119e36e03..8e07c1cffb 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/arrays/ArrayStoreExceptionExamples.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/arrays/ArrayStoreExceptionExamples.java @@ -5,9 +5,13 @@ import java.util.TreeSet; public class ArrayStoreExceptionExamples { - public boolean correctAssignmentSamePrimitiveType(int[] data) { - if (data == null || data.length == 0) return false; + // TODO || in if conditions still are not processed correctly https://github.com/UnitTestBot/usvm/issues/95 + if (data == null) { + return false; + } else if (data.length == 0) { + return false; + } data[0] = 1; return true; } @@ -90,6 +94,7 @@ public int[] arrayCopyForIncompatiblePrimitiveTypes(long[] data) { int[] result = new int[data.length]; if (data.length != 0) { + //noinspection SuspiciousSystemArraycopy System.arraycopy(data, 0, result, 0, data.length); } @@ -151,6 +156,14 @@ public Object[] fillWithSomeImplementation(SomeImplementation impl) { return result; } + public String[] arrayStoreExceptionWithEmptyArrayAndUpcast() { + String[] array = new String[1]; + //noinspection DataFlowIssue + ((Object[]) array)[0] = new SomeImplementation(); + + return array; + } + @SuppressWarnings("unchecked") private void genericAssignmentWithCast(T[] data, E element) { if (data == null || data.length == 0) return; @@ -161,4 +174,20 @@ private void genericAssignmentWithExtends(T[] data, E element) if (data == null || data.length == 0) return; data[0] = element; } + + public static class A {} + + @SuppressWarnings("ConstantValue") + public int deduceElementTypeFromArrayType(A[] arr) { + if (arr == null || arr.length == 0 || arr[0] == null) { + return -1; + } + + if (arr[0] instanceof A) { + return 1; + } else { + // Unreachable branch + return 42; + } + } } diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/arrays/FinalStaticFieldArray.java b/usvm-jvm/src/samples/java/org/usvm/samples/arrays/FinalStaticFieldArray.java index 360df2f094..f59e32a775 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/arrays/FinalStaticFieldArray.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/arrays/FinalStaticFieldArray.java @@ -1,16 +1,16 @@ package org.usvm.samples.arrays; public class FinalStaticFieldArray { - static double checkNonNegative(String role, double x) { + static double checkNonNegative(double x) { if (!(x >= 0)) { // not x < 0, to work with NaN. - throw new IllegalArgumentException(role + " (" + x + ") must be >= 0"); + throw new IllegalArgumentException(); } return x; } //This is exact example from Guava where static final array with initialization is presented public static double factorial(int n) { - checkNonNegative("n", n); + checkNonNegative(n); if (n > MAX_FACTORIAL) { return Double.POSITIVE_INFINITY; } else { diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/enums/ClassWithEnum.java b/usvm-jvm/src/samples/java/org/usvm/samples/enums/ClassWithEnum.java index 66cbaef429..20b6dcefd5 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/enums/ClassWithEnum.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/enums/ClassWithEnum.java @@ -94,7 +94,7 @@ public boolean changingStaticWithEnumInit() { return true; } - public int virtualFunction(StatusEnum parameter) { + public int virtualFunctionWithoutPathConstraints(StatusEnum parameter) { int value = parameter.virtualFunction(); if (value > 0) { return value; @@ -103,6 +103,26 @@ public int virtualFunction(StatusEnum parameter) { return Math.abs(value); } + public int virtualFunctionWithPathConstraints(StatusEnum parameter) { + if (parameter == StatusEnum.READY) { + int value = parameter.virtualFunction(); + + if (value > 0) { + return value; + } + + return Math.abs(value); + } else { + int value = parameter.virtualFunction(); + + if (value > 0) { + return value; + } + + return Math.abs(value); + } + } + @SuppressWarnings("LombokGetterMayBeUsed") public enum StatusEnum { READY(0, 10, "200") { diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/invokes/InvokeExample.java b/usvm-jvm/src/samples/java/org/usvm/samples/invokes/InvokeExample.java index 59b9f9ea19..b2fdab1580 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/invokes/InvokeExample.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/invokes/InvokeExample.java @@ -13,7 +13,10 @@ private int half(int a) { } public int simpleFormula(int fst, int snd) { - if (fst < 100 || snd < 100) { + // TODO || in if conditions still are not processed correctly https://github.com/UnitTestBot/usvm/issues/95 + if (fst < 100) { + throw new IllegalArgumentException(); + } else if (snd < 100) { throw new IllegalArgumentException(); } diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/math/DoubleFunctions.java b/usvm-jvm/src/samples/java/org/usvm/samples/math/DoubleFunctions.java index 9ae7b6f958..b53c17b342 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/math/DoubleFunctions.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/math/DoubleFunctions.java @@ -16,7 +16,12 @@ public double max(double a, double b) { } public double circleSquare(double r) { - if (r < 0 || Double.isNaN(r) || r > 10000) { + // TODO || in if conditions still are not processed correctly https://github.com/UnitTestBot/usvm/issues/95 + if (r < 0) { + throw new IllegalArgumentException(); + } else if (Double.isNaN(r)) { + throw new IllegalArgumentException(); + } else if (r > 10000) { throw new IllegalArgumentException(); } double square = Math.PI * r * r; diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/numbers/ArithmeticUtils.java b/usvm-jvm/src/samples/java/org/usvm/samples/numbers/ArithmeticUtils.java index a78ed9757c..ba2ea80c85 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/numbers/ArithmeticUtils.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/numbers/ArithmeticUtils.java @@ -53,7 +53,7 @@ public final class ArithmeticUtils { public int pow(final int k, final int e) { if (e < 0) { - throw new IllegalArgumentException(NEGATIVE_EXPONENT_1 + e + NEGATIVE_EXPONENT_2); + throw new IllegalArgumentException(); } if (k == 0) { diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/objects/ObjectWithRefFieldExample.java b/usvm-jvm/src/samples/java/org/usvm/samples/objects/ObjectWithRefFieldExample.java index 9b7e5f3d31..5b61b671a6 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/objects/ObjectWithRefFieldExample.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/objects/ObjectWithRefFieldExample.java @@ -11,7 +11,10 @@ public ObjectWithRefFieldClass defaultValue() { } public ObjectWithRefFieldClass writeToRefTypeField(ObjectWithRefFieldClass objectExample, int value) { - if (value != 42 || objectExample.refField != null) { + // TODO || in if conditions still are not processed correctly https://github.com/UnitTestBot/usvm/issues/95 + if (value != 42) { + throw new IllegalArgumentException(); + } else if (objectExample.refField != null) { throw new IllegalArgumentException(); } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/algorithms/SortTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/algorithms/SortTest.kt index 8875d37642..205792f834 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/algorithms/SortTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/algorithms/SortTest.kt @@ -41,7 +41,6 @@ internal class SortTest : JavaMethodTestRunner() { } @Test - @Disabled("Some properties were not discovered at positions (from 0): [2, 3]") fun testMergeSort() { checkDiscoveredProperties( Sort::mergeSort, @@ -72,7 +71,6 @@ internal class SortTest : JavaMethodTestRunner() { } @Test - @Disabled("Some properties were not discovered at positions (from 0): [1, 3, 4, 5]. Tune path selectors") fun testMerge() { checkDiscoveredPropertiesWithExceptions( Sort::merge, @@ -105,16 +103,15 @@ internal class SortTest : JavaMethodTestRunner() { } @Test - @Disabled("Some properties were not discovered at positions (from 0): [1, 2]. Tune path selectors") fun testDefaultSort() { checkDiscoveredPropertiesWithExceptions( Sort::defaultSort, ignoreNumberOfAnalysisResults, { _, a, r -> a == null && r.isException() }, - { _, a, r -> a != null && a.size < 4 && r.isException() }, + { _, a, r -> a != null && a.size != 4 && r.isException() }, { _, a, r -> val resultArray = intArrayOf(-100, 0, 100, 200) - a != null && r.getOrNull()!!.size >= 4 && r.getOrNull() contentEquals resultArray + a != null && r.getOrNull()!!.size == 4 && r.getOrNull() contentEquals resultArray } ) } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsExampleTest.kt index dcef9548f7..72f04a7be7 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsExampleTest.kt @@ -2,6 +2,7 @@ package org.usvm.samples.approximations import org.junit.jupiter.api.Test import org.usvm.test.util.checkers.eq +import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults import org.usvm.util.isException class ApproximationsExampleTest : ApproximationsTestRunner() { @@ -26,7 +27,7 @@ class ApproximationsExampleTest : ApproximationsTestRunner() { fun testOptionalDouble() { checkDiscoveredPropertiesWithExceptions( ApproximationsExample::testOptionalDouble, - eq(4), + ignoreNumberOfAnalysisResults, { _, o, _ -> o == 0 }, { _, o, _ -> o == 1 }, { _, o, _ -> o == 2 }, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsTest.kt index 382deeb16a..409402f55a 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsTest.kt @@ -4,6 +4,7 @@ import approximations.java.util.ArrayList_Tests import approximations.java.util.OptionalDouble_Tests import org.junit.jupiter.api.Test import org.usvm.test.util.checkers.eq +import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults import org.usvm.util.isException class ApproximationsTest : ApproximationsTestRunner() { @@ -20,16 +21,16 @@ class ApproximationsTest : ApproximationsTestRunner() { @Test fun testArrayList() { - checkDiscoveredPropertiesWithExceptions( + checkDiscoveredProperties( ArrayList_Tests::test_get_0, - eq(6), - { o, r -> o == 0 && r.isException() }, + ignoreNumberOfAnalysisResults, + { o, _ -> o == 0 }, { o, _ -> o == 1 }, { o, _ -> o == 2 }, { o, _ -> o == 3 }, { o, _ -> o == 4 }, invariants = arrayOf( - { execution, r -> execution !in 1..4 || r.getOrThrow() == execution } + { execution, r -> execution !in 0..4 || r == execution } ) ) } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ArrayListSpliteratorApproximationsTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ArrayListSpliteratorApproximationsTest.kt index 0619f2f21f..4002b9eee0 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ArrayListSpliteratorApproximationsTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ArrayListSpliteratorApproximationsTest.kt @@ -1,16 +1,16 @@ package org.usvm.samples.approximations import approximations.java.util.ArrayListSpliterator_Tests -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.test.util.checkers.eq +import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults class ArrayListSpliteratorApproximationsTest : ApproximationsTestRunner() { @Test fun testCharacteristics() { checkDiscoveredPropertiesWithExceptions( ArrayListSpliterator_Tests::test_characteristics_0, - eq(2), + ignoreNumberOfAnalysisResults, { o, _ -> o == 0 }, invariants = arrayOf( { o, r -> o != 0 || r.getOrThrow() == 0 } @@ -32,7 +32,6 @@ class ArrayListSpliteratorApproximationsTest : ApproximationsTestRunner() { } @Test - @Disabled("Index 3 out of bounds for length 3") fun testForEachRemaining() { checkDiscoveredPropertiesWithExceptions( ArrayListSpliterator_Tests::test_forEachRemaining_0, @@ -47,55 +46,52 @@ class ArrayListSpliteratorApproximationsTest : ApproximationsTestRunner() { @Test fun testGetExactSizeIfKnown() { - checkDiscoveredPropertiesWithExceptions( + checkDiscoveredProperties( ArrayListSpliterator_Tests::test_getExactSizeIfKnown_0, eq(3), { o, _ -> o == 0 }, { o, _ -> o == 1 }, invariants = arrayOf( - { o, r -> o !in 0..1 || r.getOrThrow() == o } + { o, r -> o !in 0..1 || r == o } ) ) } @Test fun testHasCharacteristics() { - checkDiscoveredPropertiesWithExceptions( + checkDiscoveredProperties( ArrayListSpliterator_Tests::test_hasCharacteristics_0, - eq(2), + ignoreNumberOfAnalysisResults, { o, _ -> o == 0 }, invariants = arrayOf( - { o, r -> o != 0 || r.getOrThrow() == 0 } + { o, r -> o != 0 || r == 0 } ) ) } @Test - @Disabled("Unexpected expr of type void: JcLambdaExpr") fun testTryAdvance() { - checkDiscoveredPropertiesWithExceptions( + checkDiscoveredProperties( ArrayListSpliterator_Tests::test_tryAdvance_0, - eq(4), + ignoreNumberOfAnalysisResults, { o, _ -> o == 0 }, { o, _ -> o == 1 }, { o, _ -> o == 2 }, invariants = arrayOf( - { o, r -> o !in 0..2 || r.getOrThrow() == o } + { o, r -> o !in 0..2 || r == o } ) ) } @Test - @Disabled("Unexpected expr of type void: JcLambdaExpr") fun testTrySplit() { checkDiscoveredPropertiesWithExceptions( - ArrayListSpliterator_Tests::test_tryAdvance_0, - eq(4), + ArrayListSpliterator_Tests::test_trySplit_0, + eq(3), { o, _ -> o == 0 }, { o, _ -> o == 1 }, - { o, _ -> o == 2 }, invariants = arrayOf( - { o, r -> o !in 0..2 || r.getOrThrow() == o } + { o, r -> o !in 0..1 || r.getOrThrow() == o } ) ) } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/ArrayOfObjectsTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/ArrayOfObjectsTest.kt index bc1d581241..6bbfd605e6 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/ArrayOfObjectsTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/ArrayOfObjectsTest.kt @@ -80,8 +80,6 @@ internal class ArrayOfObjectsTest : JavaMethodTestRunner() { } @Test - @Disabled("java.lang.ArrayStoreException: org.usvm.samples.arrays.ObjectWithPrimitivesClass." + - "Connect element type and array type") fun testObjectArray() { checkDiscoveredProperties( ArrayOfObjects::objectArray, @@ -95,7 +93,7 @@ internal class ArrayOfObjectsTest : JavaMethodTestRunner() { } @Test - @Disabled("List is empty. java.lang.ArrayStoreException: org.usvm.samples.arrays.ObjectWithPrimitivesClass") + @Disabled("TODO multidimensional array") fun testArrayOfArrays() { checkDiscoveredProperties( ArrayOfObjects::arrayOfArrays, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/ArrayStoreExceptionExamplesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/ArrayStoreExceptionExamplesTest.kt index 50e7639537..49057447ba 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/ArrayStoreExceptionExamplesTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/ArrayStoreExceptionExamplesTest.kt @@ -2,17 +2,17 @@ package org.usvm.samples.arrays import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test -import org.usvm.samples.JavaMethodTestRunner +import org.usvm.samples.approximations.ApproximationsTestRunner import org.usvm.test.util.checkers.eq +import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults import org.usvm.util.isException -class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { +class ArrayStoreExceptionExamplesTest : ApproximationsTestRunner() { @Test - @Disabled("Some properties were not discovered at positions (from 0): [1]. Fix branch coverage") fun testCorrectAssignmentSamePrimitiveType() { checkDiscoveredPropertiesWithExceptions( ArrayStoreExceptionExamples::correctAssignmentSamePrimitiveType, - eq(2), + eq(3), { _, data, result -> result.isSuccess && result.getOrNull() == false && data == null }, { _, data, result -> result.isSuccess && result.getOrNull() == false && data != null && data.isEmpty() }, { _, data, result -> result.isSuccess && result.getOrNull() == true && data != null && data.isNotEmpty() } @@ -20,7 +20,6 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Not implemented: string constant") fun testCorrectAssignmentIntToIntegerArray() { checkDiscoveredPropertiesWithExceptions( ArrayStoreExceptionExamples::correctAssignmentIntToIntegerArray, @@ -30,7 +29,6 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Not implemented: string constant") fun testCorrectAssignmentSubtype() { checkDiscoveredPropertiesWithExceptions( ArrayStoreExceptionExamples::correctAssignmentSubtype, @@ -40,7 +38,7 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Not implemented: string constant") + @Disabled("TODO support constructing approximated objects https://github.com/UnitTestBot/usvm/issues/100") fun testCorrectAssignmentToObjectArray() { checkDiscoveredPropertiesWithExceptions( ArrayStoreExceptionExamples::correctAssignmentToObjectArray, @@ -50,7 +48,6 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Not implemented: string constant") fun testWrongAssignmentUnrelatedType() { checkDiscoveredPropertiesWithExceptions( ArrayStoreExceptionExamples::wrongAssignmentUnrelatedType, @@ -62,7 +59,6 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Not implemented: string constant") fun testCheckGenericAssignmentWithCorrectCast() { checkDiscoveredPropertiesWithExceptions( ArrayStoreExceptionExamples::checkGenericAssignmentWithCorrectCast, @@ -72,7 +68,6 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Not implemented: string constant") fun testCheckGenericAssignmentWithWrongCast() { checkDiscoveredPropertiesWithExceptions( ArrayStoreExceptionExamples::checkGenericAssignmentWithWrongCast, @@ -82,7 +77,6 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Not implemented: string constant") fun testCheckGenericAssignmentWithExtendsSubtype() { checkDiscoveredPropertiesWithExceptions( ArrayStoreExceptionExamples::checkGenericAssignmentWithExtendsSubtype, @@ -92,7 +86,6 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Not implemented: string constant") fun testCheckGenericAssignmentWithExtendsUnrelated() { checkDiscoveredPropertiesWithExceptions( ArrayStoreExceptionExamples::checkGenericAssignmentWithExtendsUnrelated, @@ -102,7 +95,6 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Not implemented: string constant") fun testCheckObjectAssignment() { checkDiscoveredPropertiesWithExceptions( ArrayStoreExceptionExamples::checkObjectAssignment, @@ -112,7 +104,6 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Some properties were not discovered at positions (from 0): [0]. Support generics") fun testCheckWrongAssignmentOfItself() { checkDiscoveredPropertiesWithExceptions( ArrayStoreExceptionExamples::checkWrongAssignmentOfItself, @@ -122,7 +113,6 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Some properties were not discovered at positions (from 0): [0]. Support generics") fun testCheckGoodAssignmentOfItself() { checkDiscoveredPropertiesWithExceptions( ArrayStoreExceptionExamples::checkGoodAssignmentOfItself, @@ -132,7 +122,6 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Not implemented: string constant") fun testCheckAssignmentToObjectArray() { checkDiscoveredPropertiesWithExceptions( ArrayStoreExceptionExamples::checkAssignmentToObjectArray, @@ -166,6 +155,7 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test + @Disabled("TODO support constructing approximated objects https://github.com/UnitTestBot/usvm/issues/100") fun testFillObjectArrayWithList() { checkDiscoveredProperties( ArrayStoreExceptionExamples::fillObjectArrayWithList, @@ -176,6 +166,7 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { } @Test + @Disabled("TODO support constructing approximated objects https://github.com/UnitTestBot/usvm/issues/100") fun testFillWithTreeSet() { checkDiscoveredProperties( ArrayStoreExceptionExamples::fillWithTreeSet, @@ -214,4 +205,24 @@ class ArrayStoreExceptionExamplesTest : JavaMethodTestRunner() { { _, impl, result -> impl != null && result != null && result[0] != null } ) } + + @Test + fun testArrayStoreExceptionWithEmptyArrayAndUpcast() { + checkDiscoveredPropertiesWithExceptions( + ArrayStoreExceptionExamples::arrayStoreExceptionWithEmptyArrayAndUpcast, + eq(1), + { _, r -> r.isException() }, + ) + } + + @Test + fun testDeduceElementTypeFromArrayType() { + checkDiscoveredProperties( + ArrayStoreExceptionExamples::deduceElementTypeFromArrayType, + ignoreNumberOfAnalysisResults, + { _, arr, r -> arr == null || arr.isEmpty() || arr[0] == null && r == -1 }, + { _, arr, r -> arr != null && arr.isNotEmpty() && arr[0] != null && r == 1 }, + invariants = arrayOf({ _, _, r -> r != 42 }) + ) + } } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/ArraysOverwriteValueTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/ArraysOverwriteValueTest.kt index 19f501313a..498a2ad70b 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/ArraysOverwriteValueTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/ArraysOverwriteValueTest.kt @@ -1,11 +1,9 @@ package org.usvm.samples.arrays -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq -@Disabled("Some types don't match at positions (from 0): [1].") class ArraysOverwriteValueTest : JavaMethodTestRunner() { @Test fun testByteArray() { diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/FinalStaticFieldArrayTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/FinalStaticFieldArrayTest.kt index dc863984b8..86ca0a3150 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/FinalStaticFieldArrayTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/FinalStaticFieldArrayTest.kt @@ -1,6 +1,5 @@ package org.usvm.samples.arrays -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults @@ -8,7 +7,6 @@ import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults internal class FinalStaticFieldArrayTest : JavaMethodTestRunner() { @Test - @Disabled("Slow test") fun testFactorial() { checkDiscoveredProperties( FinalStaticFieldArray::factorial, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/IntArrayBasicsTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/IntArrayBasicsTest.kt index 4beb69b91f..d439425943 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/IntArrayBasicsTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/IntArrayBasicsTest.kt @@ -2,6 +2,7 @@ package org.usvm.samples.arrays import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test +import org.usvm.CoverageZone import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq import org.usvm.test.util.checkers.ge @@ -97,7 +98,6 @@ internal class IntArrayBasicsTest : JavaMethodTestRunner() { } @Test - @Disabled("Disjunction in if statement covered by only one execution") fun testEquality() { checkDiscoveredProperties( IntArrayBasics::equality, @@ -123,7 +123,6 @@ internal class IntArrayBasicsTest : JavaMethodTestRunner() { } @Test - @Disabled("Some properties were not discovered at positions (from 0): [3, 4, 5]. Tune path selectors") fun testMergeArrays() { checkDiscoveredProperties( IntArrayBasics::mergeArrays, @@ -179,7 +178,6 @@ internal class IntArrayBasicsTest : JavaMethodTestRunner() { } @Test - @Disabled("Some properties were not discovered at positions (from 0): [3]. Fix branch coverage") fun testReversed() { checkDiscoveredProperties( IntArrayBasics::reversed, @@ -193,7 +191,6 @@ internal class IntArrayBasicsTest : JavaMethodTestRunner() { } @Test - @Disabled("Expected exactly 3 executions, but 6 found") fun testUpdateCloned() { checkDiscoveredProperties( IntArrayBasics::updateCloned, @@ -205,13 +202,15 @@ internal class IntArrayBasicsTest : JavaMethodTestRunner() { } @Test - @Disabled("Not implemented: class constant") + @Disabled("TODO uses the native call jdk.internal.misc.Unsafe.getLong(java.lang.Object, long) in java.util.Arrays.equals(int[], int[])") fun testArraysEqualsExample() { - checkDiscoveredProperties( - IntArrayBasics::arrayEqualsExample, - eq(2), - { _, a, r -> a.size == 3 && a contentEquals intArrayOf(1, 2, 3) && r == 1 }, - { _, a, r -> !(a contentEquals intArrayOf(1, 2, 3)) && r == 2 } - ) + withOptions(options.copy(coverageZone = CoverageZone.METHOD)) { + checkDiscoveredProperties( + IntArrayBasics::arrayEqualsExample, + eq(2), + { _, a, r -> a.size == 3 && a contentEquals intArrayOf(1, 2, 3) && r == 1 }, + { _, a, r -> !(a contentEquals intArrayOf(1, 2, 3)) && r == 2 } + ) + } } -} \ No newline at end of file +} diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/PrimitiveArraysTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/PrimitiveArraysTest.kt index 0b968ce1a5..4c9a3e6a9b 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/PrimitiveArraysTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/PrimitiveArraysTest.kt @@ -1,7 +1,6 @@ package org.usvm.samples.arrays -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq @@ -158,7 +157,6 @@ internal class PrimitiveArraysTest : JavaMethodTestRunner() { } @Test - @Disabled("Some properties were not discovered at positions (from 0): [2]") fun testCharSizeAndIndex() { checkDiscoveredProperties( PrimitiveArrays::charSizeAndIndex, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/TestMultiDimensional.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/TestMultiDimensional.kt index 3dcf8b14ce..bc607fdb87 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/TestMultiDimensional.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/TestMultiDimensional.kt @@ -16,7 +16,7 @@ class TestMultiDimensional : JavaMethodTestRunner() { } @Test - @Disabled("Cannot load from byte/boolean array because \"java.lang.Integer.DigitOnes\" is null") + @Disabled("TODO support multidimensional arrays initialization") fun `Test sumOfMultiNewArray`() { checkDiscoveredProperties( MultiDimensional::sumOfMultiNewArray, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/ArrayCastExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/ArrayCastExampleTest.kt index b990e6e53e..3359ebc3c3 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/ArrayCastExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/ArrayCastExampleTest.kt @@ -100,7 +100,6 @@ internal class ArrayCastExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Support assumptions") fun testCastFromObjectToPrimitivesArray() { checkDiscoveredProperties( ArrayCastExample::castFromObjectToPrimitivesArray, @@ -127,7 +126,6 @@ internal class ArrayCastExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("java.lang.ClassNotFoundException: sun.rmi.rmic.BatchEnvironment\$Path. Fix types priority") fun testCastFromCollections() { checkDiscoveredProperties( ArrayCastExample::castFromCollections, @@ -139,7 +137,6 @@ internal class ArrayCastExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("java.lang.ClassNotFoundException: sun.rmi.rmic.BatchEnvironment\$Path. Fix types priority") fun testCastFromIterable() { checkDiscoveredProperties( ArrayCastExample::castFromIterable, @@ -151,7 +148,6 @@ internal class ArrayCastExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("java.lang.ClassNotFoundException: sun.rmi.rmic.BatchEnvironment\$Path. Fix types priority") fun testCastFromIterableToCollection() { checkDiscoveredProperties( ArrayCastExample::castFromIterableToCollection, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/CastClassTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/CastClassTest.kt index cb128c866a..c78fceca78 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/CastClassTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/CastClassTest.kt @@ -1,7 +1,6 @@ package org.usvm.samples.casts -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq @@ -9,7 +8,6 @@ import org.usvm.test.util.checkers.eq internal class CastClassTest : JavaMethodTestRunner() { @Test - @Disabled("Support assumptions") fun testThisTypeChoice() { checkDiscoveredProperties( CastClass::castToInheritor, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/CastExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/CastExampleTest.kt index af3f1233f1..192b2b1b13 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/CastExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/CastExampleTest.kt @@ -1,7 +1,6 @@ package org.usvm.samples.casts -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq @@ -58,7 +57,6 @@ internal class CastExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Support assumptions") fun testCastFromObjectToInterface() { checkDiscoveredProperties( CastExample::castFromObjectToInterface, @@ -69,7 +67,6 @@ internal class CastExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Support assumptions") fun testComplicatedCast() { checkDiscoveredProperties( CastExample::complicatedCast, @@ -78,4 +75,4 @@ internal class CastExampleTest : JavaMethodTestRunner() { { _, i, a, r -> i == 0 && a != null && a[i] != null && a[i] is CastClassFirstSucc && r is CastClassFirstSucc }, ) } -} \ No newline at end of file +} diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/GenericCastExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/GenericCastExampleTest.kt index 9156498d6a..222f290547 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/GenericCastExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/GenericCastExampleTest.kt @@ -5,6 +5,7 @@ import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.between import org.usvm.test.util.checkers.eq +import org.usvm.util.isException internal class GenericCastExampleTest : JavaMethodTestRunner() { @Test @@ -22,14 +23,17 @@ internal class GenericCastExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("org.jacodb.impl.fs.ByteCodeConverterKt: java.lang.OutOfMemoryError: Java heap space") + @Disabled("TODO violated invariants - process generic fields in type constraints properly") fun testGetGenericFieldValue() { - checkDiscoveredProperties( + checkDiscoveredPropertiesWithExceptions( GenericCastExample::getGenericFieldValue, eq(3), - { _, g, _ -> g == null }, - { _, g, _ -> g.genericField == null }, - { _, g, r -> g?.genericField != null && r == g.genericField }, + invariants = arrayOf( + { _, g, r -> + // Note that we do not expect ClassCastException or any other exceptions (except NPE) + (g == null && r.isException()) || (g != null && r.getOrThrow() == g.genericField) + } + ) ) } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/InstanceOfExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/InstanceOfExampleTest.kt index 51fde1c22f..1c037a8356 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/InstanceOfExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/InstanceOfExampleTest.kt @@ -134,7 +134,6 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("TODO fix type streams: USupportTypeStream.from(Object[]).filterBySupertype(anyType)") fun testInstanceOfAsPartOfInternalExpressionsCastClass() { checkDiscoveredProperties( InstanceOfExample::instanceOfAsPartOfInternalExpressionsCastClass, @@ -264,7 +263,6 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Some properties were not discovered at positions (from 0): [4]. Support connection between array and element type") fun testComplicatedInstanceOf() { checkDiscoveredProperties( InstanceOfExample::complicatedInstanceOf, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/ClassWithStaticAndInnerClassesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/ClassWithStaticAndInnerClassesTest.kt index 9bf196d3d1..50b2958ee2 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/ClassWithStaticAndInnerClassesTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/ClassWithStaticAndInnerClassesTest.kt @@ -1,14 +1,12 @@ package org.usvm.samples.codegen -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq @Suppress("INACCESSIBLE_TYPE") -@Disabled("Expected exactly 2 executions, but 1 found. Fix inner classes") internal class ClassWithStaticAndInnerClassesTest : JavaMethodTestRunner() { @Test fun testUsePrivateStaticClassWithPrivateField() { diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/deepequals/DeepEqualsTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/deepequals/DeepEqualsTest.kt index d767ac1240..687ae37d40 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/deepequals/DeepEqualsTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/deepequals/DeepEqualsTest.kt @@ -144,7 +144,7 @@ class DeepEqualsTest : JavaMethodTestRunner() { } @Test - @Disabled("Support multidimensional arrays initialization") + @Disabled("TODO support multidimensional arrays initialization") fun testIntMultiArray() { checkDiscoveredProperties( DeepEqualsTestingClass::fillIntMultiArrayWithConstValue, @@ -165,26 +165,38 @@ class DeepEqualsTest : JavaMethodTestRunner() { } @Test + @Disabled("TODO support multidimensional arrays initialization") fun testDoubleMultiArray() { checkDiscoveredProperties( DeepEqualsTestingClass::fillDoubleMultiArrayWithConstValue, eq(3), + { _, l, _, r -> l == 0 && r == null }, + { _, l, v, _ -> l == 2 && v.toInt() == 10 }, + { _, l, v, _ -> l == 2 && v.toInt() != 10 }, ) } @Test + @Disabled("TODO support multidimensional arrays initialization") fun testIntegerWrapperMultiArray() { checkDiscoveredProperties( DeepEqualsTestingClass::fillIntegerWrapperMultiArrayWithConstValue, eq(3), + { _, l, _, r -> l == 0 && r == null }, + { _, l, v, _ -> l == 2 && v == 10 }, + { _, l, v, _ -> l == 2 && v != 10 }, ) } @Test + @Disabled("TODO support multidimensional arrays initialization") fun testDoubleWrapperMultiArray() { checkDiscoveredProperties( DeepEqualsTestingClass::fillDoubleWrapperMultiArrayWithConstValue, eq(3), + { _, l, _, r -> l == 0 && r == null }, + { _, l, v, _ -> l == 2 && v.toInt() == 10 }, + { _, l, v, _ -> l == 2 && v.toInt() != 10 }, ) } } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/CyclesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/CyclesTest.kt index 9e0d5e8440..2bb9c0f66b 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/CyclesTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/CyclesTest.kt @@ -71,7 +71,6 @@ internal class CyclesTest : JavaMethodTestRunner() { } @Test - @Disabled("Some properties were not discovered at positions (from 0): [0]. Tune coverage zone") fun testCallInnerWhile() { checkDiscoveredProperties( Cycles::callInnerWhile, @@ -81,8 +80,6 @@ internal class CyclesTest : JavaMethodTestRunner() { } @Test - // fixme: according to the coverage strategy, [0] and [2] are equivalent - @Disabled("Some properties were not discovered at positions (from 0): [2]") fun testInnerLoop() { checkDiscoveredProperties( Cycles::innerLoop, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ClassWithEnumTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ClassWithEnumTest.kt index c1e0bd3a3c..6711d0d964 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ClassWithEnumTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ClassWithEnumTest.kt @@ -122,10 +122,20 @@ class ClassWithEnumTest : JavaMethodTestRunner() { */ @Test - @Disabled("Expected exactly 3 executions, but 2 found") - fun testVirtualFunction() { + fun testVirtualFunctionWithoutPathConstraints() { checkDiscoveredProperties( - ClassWithEnum::virtualFunction, + ClassWithEnum::virtualFunctionWithoutPathConstraints, + eq(3), + { _, parameter, _ -> parameter == null }, + { _, parameter, r -> r == 1 && parameter == ERROR }, + { _, parameter, r -> r == 0 && parameter == READY }, + ) + } + + @Test + fun testVirtualFunctionWithPathConstraints() { + checkDiscoveredProperties( + ClassWithEnum::virtualFunctionWithPathConstraints, eq(3), { _, parameter, _ -> parameter == null }, { _, parameter, r -> r == 1 && parameter == ERROR }, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/InvokeExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/InvokeExampleTest.kt index 3fc26988e5..da17284b35 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/InvokeExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/InvokeExampleTest.kt @@ -1,6 +1,5 @@ package org.usvm.samples.invokes -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq @@ -10,7 +9,6 @@ import org.usvm.util.isException internal class InvokeExampleTest : JavaMethodTestRunner() { @Test - @Disabled("Disjunction in if statement covered by only one execution") fun testSimpleFormula() { checkDiscoveredProperties( InvokeExample::simpleFormula, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/VirtualInvokeExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/VirtualInvokeExampleTest.kt index 8b6b69e331..0a619c3f82 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/VirtualInvokeExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/VirtualInvokeExampleTest.kt @@ -4,12 +4,13 @@ package org.usvm.samples.invokes import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test -import org.usvm.samples.JavaMethodTestRunner +import org.usvm.samples.approximations.ApproximationsTestRunner import org.usvm.test.util.checkers.eq import org.usvm.util.isException import java.lang.Boolean -internal class VirtualInvokeExampleTest : JavaMethodTestRunner() { +// Use approximations for analysis of Integer# +internal class VirtualInvokeExampleTest : ApproximationsTestRunner() { @Test fun testSimpleVirtualInvoke() { checkDiscoveredPropertiesWithExceptions( @@ -40,7 +41,6 @@ internal class VirtualInvokeExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Fix coverage zones") fun testObjectFromOutside() { checkDiscoveredPropertiesWithExceptions( VirtualInvokeExample::objectFromOutside, @@ -66,7 +66,6 @@ internal class VirtualInvokeExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Fix coverage zone") fun testYetAnotherObjectFromOutside() { checkDiscoveredPropertiesWithExceptions( VirtualInvokeExample::yetAnotherObjectFromOutside, @@ -120,7 +119,6 @@ internal class VirtualInvokeExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Unexpected illegal argument exception") fun testNullValueInReturnValue() { checkDiscoveredProperties( VirtualInvokeExample::nullValueInReturnValue, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/lambda/CustomPredicateExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/lambda/CustomPredicateExampleTest.kt index 79ad057596..403728b960 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/lambda/CustomPredicateExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/lambda/CustomPredicateExampleTest.kt @@ -2,13 +2,14 @@ package org.usvm.samples.lambda import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test -import org.usvm.samples.JavaMethodTestRunner +import org.usvm.samples.approximations.ApproximationsTestRunner import org.usvm.test.util.checkers.eq import org.usvm.util.isException -class CustomPredicateExampleTest : JavaMethodTestRunner() { +// Use approximations for analysis of Integer# +class CustomPredicateExampleTest : ApproximationsTestRunner() { @Test - @Disabled("Expected exactly 3 executions, but 2 found") + @Disabled("Expected exactly 3 executions, but 1 found") fun testNoCapturedValuesPredicateCheck() { checkDiscoveredPropertiesWithExceptions( CustomPredicateExample::noCapturedValuesPredicateCheck, @@ -20,7 +21,7 @@ class CustomPredicateExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Expected exactly 3 executions, but 2 found") + @Disabled("Expected exactly 3 executions, but 1 found") fun testCapturedLocalVariablePredicateCheck() { checkDiscoveredPropertiesWithExceptions( CustomPredicateExample::capturedLocalVariablePredicateCheck, @@ -32,7 +33,7 @@ class CustomPredicateExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Expected exactly 3 executions, but 2 found") + @Disabled("Expected exactly 3 executions, but 1 found") fun testCapturedParameterPredicateCheck() { checkDiscoveredPropertiesWithExceptions( CustomPredicateExample::capturedParameterPredicateCheck, @@ -44,7 +45,7 @@ class CustomPredicateExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Expected exactly 3 executions, but 2 found") + @Disabled("Expected exactly 3 executions, but 1 found") fun testCapturedStaticFieldPredicateCheck() { checkDiscoveredPropertiesWithExceptions( CustomPredicateExample::capturedStaticFieldPredicateCheck, @@ -56,7 +57,7 @@ class CustomPredicateExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Expected exactly 3 executions, but 2 found") + @Disabled("Expected exactly 3 executions, but 1 found") fun testCapturedNonStaticFieldPredicateCheck() { checkDiscoveredPropertiesWithExceptions( CustomPredicateExample::capturedNonStaticFieldPredicateCheck, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/lambda/SimpleLambdaExamplesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/lambda/SimpleLambdaExamplesTest.kt index df2cb17e16..0a8f7676c7 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/lambda/SimpleLambdaExamplesTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/lambda/SimpleLambdaExamplesTest.kt @@ -19,7 +19,7 @@ class SimpleLambdaExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("class org.jacodb.api.PredefinedPrimitive cannot be cast to class org.jacodb.api.JcRefType") + @Disabled("TODO cannot instantiate java.util.Predicate in the test resolver") fun testChoosePredicate() { checkDiscoveredProperties( SimpleLambdaExamples::choosePredicate, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/math/DoubleFunctionsTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/math/DoubleFunctionsTest.kt index 10f9d754e7..561b8132ed 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/math/DoubleFunctionsTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/math/DoubleFunctionsTest.kt @@ -2,6 +2,7 @@ package org.usvm.samples.math import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test +import org.usvm.SolverType import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults @@ -12,7 +13,7 @@ import kotlin.math.hypot @Suppress("SimplifyNegatedBinaryExpression") internal class DoubleFunctionsTest : JavaMethodTestRunner() { @Test - @Disabled("Expected exactly 1 executions, but 5 found") + @Disabled("TODO native java.lang.StrictMath::sqrt") fun testHypo() { checkDiscoveredProperties( DoubleFunctions::hypo, @@ -31,18 +32,19 @@ internal class DoubleFunctionsTest : JavaMethodTestRunner() { ) } - @Test // todo: solver timout - @Disabled("Expected exactly 5 executions, but 4 found") + @Test fun testCircleSquare() { - checkDiscoveredPropertiesWithExceptions( - DoubleFunctions::circleSquare, - eq(5), - { _, radius, r -> radius < 0 && r.isException() }, - { _, radius, r -> radius > 10000 && r.isException() }, - { _, radius, r -> radius.isNaN() && r.isException() }, - { _, radius, r -> Math.PI * radius * radius <= 777.85 && r.getOrNull() == 0.0 }, - { _, radius, r -> Math.PI * radius * radius > 777.85 && abs(777.85 - r.getOrNull()!!) >= 1e-5 } - ) + withOptions(options.copy(solverType = SolverType.YICES)) { // Z3 is much slower than Yices in this test + checkDiscoveredPropertiesWithExceptions( + DoubleFunctions::circleSquare, + eq(5), + { _, radius, r -> radius < 0 && r.isException() }, + { _, radius, r -> radius > 10000 && r.isException() }, + { _, radius, r -> radius.isNaN() && r.isException() }, + { _, radius, r -> Math.PI * radius * radius <= 777.85 && r.getOrNull() == 0.0 }, + { _, radius, r -> Math.PI * radius * radius > 777.85 && abs(777.85 - r.getOrNull()!!) >= 1e-5 } + ) + } } @Test diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mixed/SimplifierTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mixed/SimplifierTest.kt index fd2488c8f1..0155cc3ebb 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mixed/SimplifierTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mixed/SimplifierTest.kt @@ -1,6 +1,5 @@ package org.usvm.samples.mixed -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq @@ -8,7 +7,6 @@ import org.usvm.test.util.checkers.eq internal class SimplifierTest: JavaMethodTestRunner() { @Test - @Disabled("Support assumptions") fun testSimplifyAdditionWithZero() { checkDiscoveredProperties( Simplifier::simplifyAdditionWithZero, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/aliasing/AliasingInParamsExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/aliasing/AliasingInParamsExampleTest.kt index abb8b2dc74..f02b1f1a49 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/aliasing/AliasingInParamsExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/aliasing/AliasingInParamsExampleTest.kt @@ -8,7 +8,7 @@ import org.usvm.test.util.checkers.eq internal class AliasingInParamsExampleTest : JavaMethodTestRunner() { @Test - @Disabled("Expected exactly 1 executions, but 3 found") + @Disabled("Unsupported mock strategies") fun testExamplePackageBased() { checkDiscoveredProperties( AliasingInParamsExample::example, @@ -18,7 +18,6 @@ internal class AliasingInParamsExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Expected exactly 2 executions, but 3 found") fun testExample() { checkDiscoveredProperties( AliasingInParamsExample::example, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/numbers/ArithmeticUtilsTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/numbers/ArithmeticUtilsTest.kt index abb5ee250c..b54bd7008d 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/numbers/ArithmeticUtilsTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/numbers/ArithmeticUtilsTest.kt @@ -1,20 +1,17 @@ -package org.usvm.samples.thirdparty.numbers +package org.usvm.samples.numbers -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner -import org.usvm.samples.numbers.ArithmeticUtils -import org.usvm.test.util.checkers.eq +import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults // example from Apache common-numbers internal class ArithmeticUtilsTest : JavaMethodTestRunner() { @Test - @Disabled("Expected exactly 11 executions, but 15 found") fun testPow() { checkDiscoveredProperties( ArithmeticUtils::pow, - eq(11), + ignoreNumberOfAnalysisResults, { _, _, e, _ -> e < 0 }, // IllegalArgumentException { _, k, e, r -> k == 0 && e == 0 && r == 1 }, { _, k, e, r -> k == 0 && e != 0 && r == 0 }, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/ObjectWithRefFieldsExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/ObjectWithRefFieldsExampleTest.kt index 23a3879e88..31f3957766 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/ObjectWithRefFieldsExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/ObjectWithRefFieldsExampleTest.kt @@ -1,6 +1,5 @@ package org.usvm.samples.objects -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq @@ -20,7 +19,6 @@ internal class ObjectWithRefFieldsExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Some properties were not discovered at positions (from 0): [2]. Fix branch coverage") fun testWriteToRefTypeField() { checkDiscoveredProperties( ObjectWithRefFieldExample::writeToRefTypeField, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/primitives/DoubleExamplesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/primitives/DoubleExamplesTest.kt index 5554841586..4b6a8d72dd 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/primitives/DoubleExamplesTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/primitives/DoubleExamplesTest.kt @@ -1,7 +1,7 @@ package org.usvm.samples.primitives -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test +import org.usvm.SolverType import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults @@ -29,7 +29,7 @@ internal class DoubleExamplesTest : JavaMethodTestRunner() { ) } - @Disabled("Timeout Expected exactly 2 executions, but 0 found") + @Test fun testCompareWithDiv() { checkDiscoveredProperties( DoubleExamples::compareWithDiv, @@ -62,30 +62,32 @@ internal class DoubleExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Not enough time") fun testSimpleMul() { - checkDiscoveredProperties( - DoubleExamples::simpleMul, - ignoreNumberOfAnalysisResults, - { _, a, b, r -> (a * b).isNaN() && r == 0.0 }, - { _, a, b, r -> a * b > 33.1 && a * b < 33.875 && r == 1.1 }, - { _, a, b, r -> a * b >= 33.875 || a * b <= 33.1 && r == 1.2 } - ) + withOptions(options.copy(solverType = SolverType.YICES)) { + checkDiscoveredProperties( + DoubleExamples::simpleMul, + ignoreNumberOfAnalysisResults, + { _, a, b, r -> (a * b).isNaN() && r == 0.0 }, + { _, a, b, r -> a * b > 33.1 && a * b < 33.875 && r == 1.1 }, + { _, a, b, r -> a * b >= 33.875 || a * b <= 33.1 && r == 1.2 } + ) + } } @Test - @Disabled("Not enough time") fun testMul() { - checkDiscoveredProperties( - DoubleExamples::mul, - eq(6), - { _, a, b, r -> (a * b).isNaN() && r == 0.0 }, // 0 * inf || a == nan || b == nan - { _, a, b, r -> !(a * b > 33.32) && !(a * b > 33.333) && r == 1.3 }, // 1.3, 1-1 false, 2-1 false - { _, a, b, r -> a * b == 33.333 && r == 1.3 }, // 1.3, 1-1 true, 1-2 false, 2-1 false - { _, a, b, r -> a * b > 33.32 && a * b < 33.333 && r == 1.1 }, // 1.1, 1st true - { _, a, b, r -> a * b > 33.333 && a * b < 33.7592 && r == 1.2 }, // 1.2, 1st false, 2nd true - { _, a, b, r -> a * b >= 33.7592 && r == 1.3 } // 1.3, 1-1 false, 2-1 true, 2-2 false - ) + withOptions(options.copy(solverType = SolverType.YICES)) { + checkDiscoveredProperties( + DoubleExamples::mul, + eq(6), + { _, a, b, r -> (a * b).isNaN() && r == 0.0 }, // 0 * inf || a == nan || b == nan + { _, a, b, r -> !(a * b > 33.32) && !(a * b > 33.333) && r == 1.3 }, // 1.3, 1-1 false, 2-1 false + { _, a, b, r -> a * b == 33.333 && r == 1.3 }, // 1.3, 1-1 true, 1-2 false, 2-1 false + { _, a, b, r -> a * b > 33.32 && a * b < 33.333 && r == 1.1 }, // 1.1, 1st true + { _, a, b, r -> a * b > 33.333 && a * b < 33.7592 && r == 1.2 }, // 1.2, 1st false, 2nd true + { _, a, b, r -> a * b >= 33.7592 && r == 1.3 } // 1.3, 1-1 false, 2-1 true, 2-2 false + ) + } } @Test @@ -118,14 +120,15 @@ internal class DoubleExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Not enough time") fun testSimpleNonLinearEquation() { - checkDiscoveredProperties( - DoubleExamples::simpleNonLinearEquation, - eq(2), - { _, x, r -> 3 * x - 9 == x + 3 && r == 0 }, - { _, x, r -> 3 * x - 9 != x + 3 && r == 1 } - ) + withOptions(options.copy(solverType = SolverType.YICES)) { + checkDiscoveredProperties( + DoubleExamples::simpleNonLinearEquation, + eq(2), + { _, x, r -> 3 * x - 9 == x + 3 && r == 0 }, + { _, x, r -> 3 * x - 9 != x + 3 && r == 1 } + ) + } } @Test diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/HeapTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/HeapTest.kt index ff9f5f6b4b..9c6ff62c3a 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/HeapTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/HeapTest.kt @@ -1,6 +1,5 @@ package org.usvm.samples.structures -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults @@ -8,7 +7,6 @@ import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults internal class HeapTest : JavaMethodTestRunner() { @Test - @Disabled("Some properties were not discovered at positions (from 0): [4]. Fix branch coverage") fun testIsHeap() { val method = Heap::isHeap checkDiscoveredProperties( diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/MinStackExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/MinStackExampleTest.kt index 56cf7a008b..81e66311d4 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/MinStackExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/MinStackExampleTest.kt @@ -1,21 +1,19 @@ package org.usvm.samples.structures -import org.junit.jupiter.api.Disabled + import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.between import org.usvm.test.util.checkers.eq - - +import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults import kotlin.math.min internal class MinStackExampleTest : JavaMethodTestRunner() { @Test - @Disabled("Expected exactly 3 executions, but 4 found") fun testCreate() { checkDiscoveredProperties( MinStackExample::create, - eq(3), + ignoreNumberOfAnalysisResults, { _, initialValues, _ -> initialValues == null }, { _, initialValues, _ -> initialValues != null && initialValues.size < 3 }, { _, initialValues, result -> @@ -34,7 +32,6 @@ internal class MinStackExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Expected exactly 3 executions, but 2 found. Tune coverage zone") fun testAddSingleValue() { checkDiscoveredProperties( MinStackExample::addSingleValue, @@ -54,7 +51,6 @@ internal class MinStackExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Expected exactly 3 executions, but 2 found. Tune coverage zone") fun testGetMinValue() { checkDiscoveredProperties( MinStackExample::getMinValue, @@ -68,11 +64,10 @@ internal class MinStackExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Expected exactly 4 executions, but 5 found") fun testRemoveValue() { checkDiscoveredProperties( MinStackExample::removeValue, - eq(4), + ignoreNumberOfAnalysisResults, { _, initialValues, _ -> initialValues == null }, { _, initialValues, _ -> initialValues != null && initialValues.isEmpty() }, { _, initialValues, result -> diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/StandardStructuresTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/StandardStructuresTest.kt index defc847db7..bd47bcac95 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/StandardStructuresTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/StandardStructuresTest.kt @@ -1,15 +1,12 @@ package org.usvm.samples.structures -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq -import java.util.LinkedList -import java.util.TreeMap +import java.util.* internal class StandardStructuresTest : JavaMethodTestRunner() { @Test - @Disabled("Support creation of collections") fun testGetList() { checkDiscoveredProperties( StandardStructures::getList, @@ -24,7 +21,6 @@ internal class StandardStructuresTest : JavaMethodTestRunner() { } @Test - @Disabled("Support creation of collections") fun testGetMap() { checkDiscoveredProperties( StandardStructures::getMap, @@ -36,16 +32,15 @@ internal class StandardStructuresTest : JavaMethodTestRunner() { } @Test - @Disabled("Support creation of collections") fun testGetDeque() { checkDiscoveredProperties( StandardStructures::getDeque, eq(4), - { _, d, r -> d is ArrayDeque<*> && r is ArrayDeque<*> }, + { _, d, r -> d is java.util.ArrayDeque<*> && r is java.util.ArrayDeque<*> }, { _, d, r -> d is LinkedList && r is LinkedList }, { _, d, r -> d == null && r == null }, { _, d, r -> - d !is ArrayDeque<*> && d !is LinkedList && d != null && r !is ArrayDeque<*> && r !is LinkedList && r != null + d !is java.util.ArrayDeque<*> && d !is LinkedList && d != null && r !is java.util.ArrayDeque<*> && r !is LinkedList && r != null }, ) }