From 1b5aa882510af3c0eb0fcf879abaeccc972d67c2 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Sun, 27 Jul 2025 15:36:13 +0300 Subject: [PATCH 1/6] [feat] added `Engine.arrayEquals` method --- .../org/usvm/machine/JcApproximations.kt | 82 +++++++++++++++++++ .../org/usvm/machine/state/JcStateUtils.kt | 30 +++++++ .../src/main/java/org/usvm/api/Engine.java | 23 ++++++ 3 files changed, 135 insertions(+) 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 0d01d3c196..8534b4a7d8 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt @@ -76,11 +76,14 @@ import org.usvm.api.mapTypeStreamNotNull import org.usvm.api.memcpy import org.usvm.api.objectTypeEquals import org.usvm.api.objectTypeSubtype +import org.usvm.api.readArrayIndex +import org.usvm.api.readArrayLength import org.usvm.api.readField import org.usvm.api.writeField import org.usvm.collection.array.UArrayIndexLValue import org.usvm.collection.array.length.UArrayLengthLValue import org.usvm.collection.field.UFieldLValue +import org.usvm.getIntValue import org.usvm.jvm.util.allInstanceFields import org.usvm.jvm.util.javaName import org.usvm.machine.interpreter.JcExprResolver @@ -88,7 +91,9 @@ import org.usvm.machine.interpreter.JcStepScope import org.usvm.machine.mocks.mockMethod import org.usvm.machine.state.JcState import org.usvm.machine.state.newStmt +import org.usvm.machine.state.skipMethodInvocationAndBoxIfNeeded import org.usvm.machine.state.skipMethodInvocationWithValue +import org.usvm.mkSizeExpr import org.usvm.sizeSort import org.usvm.types.first import org.usvm.types.singleOrNull @@ -571,6 +576,77 @@ class JcMethodApproximationResolver( return false } + private fun JcState.arrayContentEquals( + firstArray: UHeapRef, + secondArray: UHeapRef, + arrayType: JcArrayType, + ): UBoolExpr? = with(ctx) { + val arrayDesciptor = arrayDescriptorOf(arrayType) + val elementType = arrayType.elementType + val elementSort = typeToSort(elementType) + + val firstLength = memory.readArrayLength(firstArray, arrayDesciptor, sizeSort) + val secondLength = memory.readArrayLength(secondArray, arrayDesciptor, sizeSort) + + val concreteLength = + getIntValue(firstLength) + ?: getIntValue(secondLength) + ?: return@with null + + return@with mkIte(mkEq(firstLength, secondLength).not(), { falseExpr }) { + val arrayEquals = List(concreteLength) { + val idx = mkSizeExpr(it) + val first = memory.readArrayIndex(firstArray, idx, arrayDesciptor, elementSort) + val second = + memory.readArrayIndex(secondArray, idx, arrayDesciptor, elementSort) + mkEq(first, second) + } + mkAnd(arrayEquals) + } + } + + private fun JcState.arrayEquals(methodCall: JcMethodCall, firstArray: UHeapRef, secondArray: UHeapRef) = with(ctx) { + val possibleElementTypes = primitiveTypes + cp.objectType + val possibleArrayTypes = possibleElementTypes.map { cp.arrayTypeOf(it) } + + val branches = mutableListOf Unit>>() + var typeDiffersConstraint: UBoolExpr = trueExpr + + val arrayRefsEqual = mkEq(firstArray, secondArray) + val oneArrayIsNull = mkOr(mkEq(firstArray, nullRef), mkEq(secondArray, nullRef)) + branches += arrayRefsEqual to { state -> + state.skipMethodInvocationAndBoxIfNeeded(methodCall, cp.boolean, trueExpr) + } + branches += mkAnd(mkNot(arrayRefsEqual), oneArrayIsNull) to { state -> + state.skipMethodInvocationAndBoxIfNeeded(methodCall, cp.boolean, falseExpr) + } + val needToCheckContent = mkAnd(mkNot(arrayRefsEqual), mkNot(oneArrayIsNull)) + for (arrayType in possibleArrayTypes) { + val typeConstraint = scope.calcOnState { + mkAnd( + memory.types.evalIsSubtype(firstArray, arrayType), + memory.types.evalIsSubtype(secondArray, arrayType) + ) + } + typeDiffersConstraint = mkAnd(typeDiffersConstraint, ctx.mkNot(typeConstraint)) + branches += mkAnd(needToCheckContent, typeConstraint) to { state -> + val checkResult = state.arrayContentEquals(firstArray, secondArray, arrayType) + if (checkResult == null) { + // Unable to check + state.skipMethodInvocationWithValue(methodCall, nullRef) + } else { + state.skipMethodInvocationAndBoxIfNeeded(methodCall, cp.boolean, checkResult) + } + } + } + + branches += typeDiffersConstraint to { state -> + state.skipMethodInvocationAndBoxIfNeeded(methodCall, cp.boolean, falseExpr) + } + + scope.forkMulti(branches) + } + private sealed interface StringConcatElement private data class StringConcatStrElement(val str: String) : StringConcatElement private data class StringConcatRefElement(val ref: UHeapRef) : StringConcatElement @@ -1098,6 +1174,12 @@ class JcMethodApproximationResolver( makeSymbolicArray(ctx.cp.objectType, sizeExpr) } } + dispatchUsvmApiMethod(Engine::arrayEquals) { + val first = it.arguments[0].asExpr(ctx.addressSort) + val second = it.arguments[1].asExpr(ctx.addressSort) + scope.doWithState { arrayEquals(it, first, second) } + null + } dispatchMkList(Engine::makeSymbolicList) { scope.calcOnState { mkSymbolicList(symbolicListType) } } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt index ad0f6e77ce..f84c88ffc6 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt @@ -1,11 +1,15 @@ package org.usvm.machine.state +import org.jacodb.api.jvm.JcClassType import org.jacodb.api.jvm.JcMethod +import org.jacodb.api.jvm.JcPrimitiveType import org.jacodb.api.jvm.JcType import org.jacodb.api.jvm.cfg.JcArgument import org.jacodb.api.jvm.cfg.JcDynamicCallExpr import org.jacodb.api.jvm.cfg.JcInst +import org.jacodb.api.jvm.ext.autoboxIfNeeded import org.jacodb.api.jvm.ext.cfg.locals +import org.jacodb.api.jvm.ext.findType import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort @@ -88,3 +92,29 @@ fun JcState.skipMethodInvocationWithValue(methodCall: JcMethodCall, value: UExpr methodResult = JcMethodResult.Success(methodCall.method, value) newStmt(methodCall.returnSite) } + +fun JcState.skipMethodInvocationAndBoxIfNeeded(methodCall: JcMethodCall, valueType: JcType, value: UExpr) { + val typeSystem = ctx.typeSystem() + val methodReturnType = ctx.cp.findType(methodCall.method.returnType.typeName) + when { + valueType is JcPrimitiveType && methodReturnType is JcClassType -> { + val boxedType = valueType.autoboxIfNeeded() as JcClassType + check(typeSystem.isSupertype(methodReturnType, boxedType)) { + "skipMethodInvocationAndBoxIfNeeded: Incorrect method return type" + } + val boxMethod = boxedType.declaredMethods.find { + it.name == "valueOf" && it.isStatic && it.parameters.singleOrNull()?.type == valueType + }!! + methodResult = JcMethodResult.NoCall + newStmt(JcConcreteMethodCallInst(methodCall.location, boxMethod.method, listOf(value), methodCall.returnSite)) + } + + else -> { + // TODO: implement unboxing if needed + check(typeSystem.isSupertype(methodReturnType, valueType)) { + "skipMethodInvocationAndBoxIfNeeded: Incorrect method return type" + } + skipMethodInvocationWithValue(methodCall, value) + } + } +} diff --git a/usvm-jvm/usvm-jvm-api/src/main/java/org/usvm/api/Engine.java b/usvm-jvm/usvm-jvm-api/src/main/java/org/usvm/api/Engine.java index 706ab361da..306fb70c65 100644 --- a/usvm-jvm/usvm-jvm-api/src/main/java/org/usvm/api/Engine.java +++ b/usvm-jvm/usvm-jvm-api/src/main/java/org/usvm/api/Engine.java @@ -5,6 +5,7 @@ import org.usvm.api.internal.SymbolicMapImpl; import java.lang.reflect.Array; +import java.util.Arrays; public class Engine { @@ -103,6 +104,28 @@ public static double[] makeSymbolicDoubleArray(int size) { return new double[size]; } + public static Boolean arrayEquals(Object first, Object second) { + if (first instanceof byte[] && second instanceof byte[]) + return Arrays.equals((byte[])first, (byte[])second); + if (first instanceof char[] && second instanceof char[]) + return Arrays.equals((char[])first, (char[])second); + if (first instanceof int[] && second instanceof int[]) + return Arrays.equals((int[])first, (int[])second); + if (first instanceof long[] && second instanceof long[]) + return Arrays.equals((long[])first, (long[])second); + if (first instanceof boolean[] && second instanceof boolean[]) + return Arrays.equals((boolean[])first, (boolean[])second); + if (first instanceof float[] && second instanceof float[]) + return Arrays.equals((float[])first, (float[])second); + if (first instanceof double[] && second instanceof double[]) + return Arrays.equals((double[])first, (double[])second); + if (first instanceof short[] && second instanceof short[]) + return Arrays.equals((short[])first, (short[])second); + if (first instanceof Object[] && second instanceof Object[]) + return Arrays.equals((Object[])first, (Object[])second); + return false; + } + public static SymbolicList makeSymbolicList() { return new SymbolicListImpl<>(); } From e60e432cd416a1c073e0129eab04375c3e98e2a8 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Sun, 27 Jul 2025 15:48:18 +0300 Subject: [PATCH 2/6] [feat] added `Engine.assumeSymbolic` method --- .../main/kotlin/org/usvm/machine/JcApproximations.kt | 10 ++++++++++ .../src/main/java/org/usvm/api/Engine.java | 4 ++++ 2 files changed, 14 insertions(+) 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 8534b4a7d8..3d0a25bc47 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt @@ -39,6 +39,7 @@ import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UFpSort import org.usvm.UHeapRef +import org.usvm.UNullRef import org.usvm.USort import org.usvm.api.Engine import org.usvm.api.SymbolicIdentityMap @@ -1032,6 +1033,15 @@ class JcMethodApproximationResolver( val arg = it.arguments.single().asExpr(ctx.booleanSort) scope.assert(arg)?.let { ctx.voidValue } } + dispatchUsvmApiMethod(Engine::assumeSymbolic) { + val instance = it.arguments[0].asExpr(ctx.addressSort) + if (instance is UConcreteHeapRef || instance is UNullRef) { + ctx.voidValue + } else { + val condition = it.arguments[1].asExpr(ctx.booleanSort) + scope.assert(condition)?.let { ctx.voidValue } + } + } dispatchUsvmApiMethod(Engine::makeSymbolicBoolean) { scope.calcOnState { makeSymbolicPrimitive(ctx.booleanSort) } } diff --git a/usvm-jvm/usvm-jvm-api/src/main/java/org/usvm/api/Engine.java b/usvm-jvm/usvm-jvm-api/src/main/java/org/usvm/api/Engine.java index 306fb70c65..d03fe027c4 100644 --- a/usvm-jvm/usvm-jvm-api/src/main/java/org/usvm/api/Engine.java +++ b/usvm-jvm/usvm-jvm-api/src/main/java/org/usvm/api/Engine.java @@ -13,6 +13,10 @@ public static void assume(boolean expr) { assert expr; } + public static void assumeSymbolic(Object instance, boolean expr) { + assert expr; + } + @SuppressWarnings("unused") public static T makeSymbolic(Class clazz) { return null; From 93ad851411fe474e841674d2f71718f98788db0c Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Tue, 29 Jul 2025 18:21:16 +0300 Subject: [PATCH 3/6] [fix] added fixes - added `isConcrete` predicate for heap reference - fixed `arrayEquals` --- .../src/main/kotlin/org/usvm/Expressions.kt | 13 ++++++ .../org/usvm/memory/HeapRefSplitting.kt | 19 +++++++++ .../org/usvm/machine/JcApproximations.kt | 40 +++++++++++-------- 3 files changed, 56 insertions(+), 16 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt index 927c8168ba..061405b7b5 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt @@ -23,6 +23,7 @@ import io.ksmt.sort.KSort import io.ksmt.sort.KUninterpretedSort import org.usvm.memory.USymbolicCollection import org.usvm.memory.USymbolicCollectionId +import org.usvm.memory.foldHeapRefWithStaticAsConcrete import kotlin.contracts.ExperimentalContracts import kotlin.contracts.contract @@ -100,6 +101,18 @@ fun isStaticHeapRef(expr: UExpr<*>): Boolean { val UConcreteHeapRef.isAllocated: Boolean get() = address.isAllocated val UConcreteHeapRef.isStatic: Boolean get() = address.isStatic +val UHeapRef.isConcrete: Boolean get() { + return foldHeapRefWithStaticAsConcrete( + ref = this, + initial = true, + initialGuard = this.ctx.trueExpr, + ignoreNullRefs = true, + collapseHeapRefs = true, + blockOnConcrete = { acc, _ -> acc }, + blockOnSymbolic = { _, _ -> return false } + ) +} + class UConcreteHeapRefDecl internal constructor( ctx: UContext<*>, val address: UConcreteHeapAddress, diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt b/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt index c73ea2ea01..7ba39b77aa 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt @@ -163,6 +163,25 @@ inline fun foldHeapRefWithStaticAsSymbolic( blockOnSymbolic = blockOnSymbolic ) +inline fun foldHeapRefWithStaticAsConcrete( + ref: UHeapRef, + initial: R, + initialGuard: UBoolExpr, + ignoreNullRefs: Boolean = true, + collapseHeapRefs: Boolean = true, + blockOnConcrete: (R, GuardedExpr) -> R, + blockOnSymbolic: (R, GuardedExpr) -> R, +): R = foldHeapRef( + ref, + initial, + initialGuard, + ignoreNullRefs, + collapseHeapRefs, + staticIsConcrete = true, + blockOnConcrete = blockOnConcrete, + blockOnSymbolic = blockOnSymbolic +) + inline fun foldHeapRef2( ref0: UHeapRef, ref1: UHeapRef, 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 3d0a25bc47..3f95cb5c78 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt @@ -85,6 +85,7 @@ import org.usvm.collection.array.UArrayIndexLValue import org.usvm.collection.array.length.UArrayLengthLValue import org.usvm.collection.field.UFieldLValue import org.usvm.getIntValue +import org.usvm.isConcrete import org.usvm.jvm.util.allInstanceFields import org.usvm.jvm.util.javaName import org.usvm.machine.interpreter.JcExprResolver @@ -580,30 +581,28 @@ class JcMethodApproximationResolver( private fun JcState.arrayContentEquals( firstArray: UHeapRef, secondArray: UHeapRef, + firstLength: UExpr, + secondLength: UExpr, arrayType: JcArrayType, ): UBoolExpr? = with(ctx) { val arrayDesciptor = arrayDescriptorOf(arrayType) val elementType = arrayType.elementType val elementSort = typeToSort(elementType) - val firstLength = memory.readArrayLength(firstArray, arrayDesciptor, sizeSort) - val secondLength = memory.readArrayLength(secondArray, arrayDesciptor, sizeSort) - val concreteLength = getIntValue(firstLength) ?: getIntValue(secondLength) ?: return@with null - return@with mkIte(mkEq(firstLength, secondLength).not(), { falseExpr }) { - val arrayEquals = List(concreteLength) { - val idx = mkSizeExpr(it) - val first = memory.readArrayIndex(firstArray, idx, arrayDesciptor, elementSort) - val second = - memory.readArrayIndex(secondArray, idx, arrayDesciptor, elementSort) - mkEq(first, second) - } - mkAnd(arrayEquals) + val arrayEquals = List(concreteLength) { + val idx = mkSizeExpr(it) + val first = memory.readArrayIndex(firstArray, idx, arrayDesciptor, elementSort) + val second = + memory.readArrayIndex(secondArray, idx, arrayDesciptor, elementSort) + mkEq(first, second) } + + return@with mkAnd(arrayEquals) } private fun JcState.arrayEquals(methodCall: JcMethodCall, firstArray: UHeapRef, secondArray: UHeapRef) = with(ctx) { @@ -629,9 +628,18 @@ class JcMethodApproximationResolver( memory.types.evalIsSubtype(secondArray, arrayType) ) } - typeDiffersConstraint = mkAnd(typeDiffersConstraint, ctx.mkNot(typeConstraint)) - branches += mkAnd(needToCheckContent, typeConstraint) to { state -> - val checkResult = state.arrayContentEquals(firstArray, secondArray, arrayType) + typeDiffersConstraint = mkAnd(typeDiffersConstraint, mkNot(typeConstraint)) + val arrayDesciptor = arrayDescriptorOf(arrayType) + val firstLength = memory.readArrayLength(firstArray, arrayDesciptor, sizeSort) + val secondLength = memory.readArrayLength(secondArray, arrayDesciptor, sizeSort) + val lengthsEqual = mkEq(firstLength, secondLength) + + branches += mkAnd(needToCheckContent, typeConstraint, mkNot(lengthsEqual)) to { state -> + state.skipMethodInvocationAndBoxIfNeeded(methodCall, cp.boolean, falseExpr) + } + + branches += mkAnd(needToCheckContent, typeConstraint, lengthsEqual) to { state -> + val checkResult = state.arrayContentEquals(firstArray, secondArray, firstLength, secondLength, arrayType) if (checkResult == null) { // Unable to check state.skipMethodInvocationWithValue(methodCall, nullRef) @@ -1035,7 +1043,7 @@ class JcMethodApproximationResolver( } dispatchUsvmApiMethod(Engine::assumeSymbolic) { val instance = it.arguments[0].asExpr(ctx.addressSort) - if (instance is UConcreteHeapRef || instance is UNullRef) { + if (instance.isConcrete) { ctx.voidValue } else { val condition = it.arguments[1].asExpr(ctx.booleanSort) From df8dcd5b85731f47d6b175a678855357d43912d0 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Wed, 30 Jul 2025 14:35:56 +0300 Subject: [PATCH 4/6] [fix] fixed `assumeSymbolic` --- .../src/main/kotlin/org/usvm/Expressions.kt | 13 ------------- .../org/usvm/machine/JcApproximations.kt | 18 +++++++++++------- 2 files changed, 11 insertions(+), 20 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt index 061405b7b5..927c8168ba 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt @@ -23,7 +23,6 @@ import io.ksmt.sort.KSort import io.ksmt.sort.KUninterpretedSort import org.usvm.memory.USymbolicCollection import org.usvm.memory.USymbolicCollectionId -import org.usvm.memory.foldHeapRefWithStaticAsConcrete import kotlin.contracts.ExperimentalContracts import kotlin.contracts.contract @@ -101,18 +100,6 @@ fun isStaticHeapRef(expr: UExpr<*>): Boolean { val UConcreteHeapRef.isAllocated: Boolean get() = address.isAllocated val UConcreteHeapRef.isStatic: Boolean get() = address.isStatic -val UHeapRef.isConcrete: Boolean get() { - return foldHeapRefWithStaticAsConcrete( - ref = this, - initial = true, - initialGuard = this.ctx.trueExpr, - ignoreNullRefs = true, - collapseHeapRefs = true, - blockOnConcrete = { acc, _ -> acc }, - blockOnSymbolic = { _, _ -> return false } - ) -} - class UConcreteHeapRefDecl internal constructor( ctx: UContext<*>, val address: UConcreteHeapAddress, 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 3f95cb5c78..212f97afe9 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt @@ -85,7 +85,6 @@ import org.usvm.collection.array.UArrayIndexLValue import org.usvm.collection.array.length.UArrayLengthLValue import org.usvm.collection.field.UFieldLValue import org.usvm.getIntValue -import org.usvm.isConcrete import org.usvm.jvm.util.allInstanceFields import org.usvm.jvm.util.javaName import org.usvm.machine.interpreter.JcExprResolver @@ -95,6 +94,7 @@ import org.usvm.machine.state.JcState import org.usvm.machine.state.newStmt import org.usvm.machine.state.skipMethodInvocationAndBoxIfNeeded import org.usvm.machine.state.skipMethodInvocationWithValue +import org.usvm.memory.foldHeapRefWithStaticAsConcrete import org.usvm.mkSizeExpr import org.usvm.sizeSort import org.usvm.types.first @@ -1043,12 +1043,16 @@ class JcMethodApproximationResolver( } dispatchUsvmApiMethod(Engine::assumeSymbolic) { val instance = it.arguments[0].asExpr(ctx.addressSort) - if (instance.isConcrete) { - ctx.voidValue - } else { - val condition = it.arguments[1].asExpr(ctx.booleanSort) - scope.assert(condition)?.let { ctx.voidValue } - } + val condition = it.arguments[1].asExpr(ctx.booleanSort) + foldHeapRefWithStaticAsConcrete( + ref = instance, + initial = Unit, + initialGuard = ctx.trueExpr, + ignoreNullRefs = true, + collapseHeapRefs = true, + blockOnConcrete = { _, _ -> Unit }, + blockOnSymbolic = { acc, ref -> scope.assert(ctx.mkImplies(ref.guard, condition)) ?: acc } + )?.let { ctx.voidValue } } dispatchUsvmApiMethod(Engine::makeSymbolicBoolean) { scope.calcOnState { makeSymbolicPrimitive(ctx.booleanSort) } From e80e48f8935d2edbb4310f50ddd7626160f0fca6 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Wed, 30 Jul 2025 17:02:55 +0300 Subject: [PATCH 5/6] [chore] updated approximations version --- usvm-jvm/build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-jvm/build.gradle.kts b/usvm-jvm/build.gradle.kts index 59cbffcdf3..9beb55db37 100644 --- a/usvm-jvm/build.gradle.kts +++ b/usvm-jvm/build.gradle.kts @@ -24,7 +24,7 @@ val `sample-approximations` by sourceSets.creating { val approximations by configurations.creating val approximationsRepo = "com.github.UnitTestBot.java-stdlib-approximations" -val approximationsVersion = "88c6be3469" +val approximationsVersion = "aa9e358446" dependencies { implementation(project(":usvm-core")) From 3643c865828797507388ef513224c3e2df2da1ef Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Wed, 30 Jul 2025 17:07:42 +0300 Subject: [PATCH 6/6] [style] fixed style --- usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt | 1 - .../src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt | 4 ++-- 2 files changed, 2 insertions(+), 3 deletions(-) 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 212f97afe9..1db286af01 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt @@ -39,7 +39,6 @@ import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UFpSort import org.usvm.UHeapRef -import org.usvm.UNullRef import org.usvm.USort import org.usvm.api.Engine import org.usvm.api.SymbolicIdentityMap diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt index f84c88ffc6..cc6dad55fd 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt @@ -102,9 +102,9 @@ fun JcState.skipMethodInvocationAndBoxIfNeeded(methodCall: JcMethodCall, valueTy check(typeSystem.isSupertype(methodReturnType, boxedType)) { "skipMethodInvocationAndBoxIfNeeded: Incorrect method return type" } - val boxMethod = boxedType.declaredMethods.find { + val boxMethod = boxedType.declaredMethods.first { it.name == "valueOf" && it.isStatic && it.parameters.singleOrNull()?.type == valueType - }!! + } methodResult = JcMethodResult.NoCall newStmt(JcConcreteMethodCallInst(methodCall.location, boxMethod.method, listOf(value), methodCall.returnSite)) }