From eb5f2d56d2e1ef0904c968cae96f2debc8f3de30 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Tue, 13 Aug 2024 16:49:02 +0300 Subject: [PATCH 1/3] 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 daad5aa69b..0cf77dc8ac 100644 --- a/usvm-jvm/build.gradle.kts +++ b/usvm-jvm/build.gradle.kts @@ -24,7 +24,7 @@ val `usvm-api` by sourceSets.creating { val approximations by configurations.creating val approximationsRepo = "com.github.UnitTestBot.java-stdlib-approximations" -val approximationsVersion = "0f081f101e" +val approximationsVersion = "5f137507d6" dependencies { implementation(project(":usvm-core")) From 82b5e1e84ce81da508f41671069e8dbcc613cabf Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Tue, 13 Aug 2024 16:49:54 +0300 Subject: [PATCH 2/3] increased 'stepsFromLastCovered' - increased 'stepsFromLastCovered' to suite new approximations --- .../org/usvm/samples/JavaMethodTestRunner.kt | 2 +- .../org/usvm/samples/recursion/RecursionTest.kt | 16 ++++++++++------ 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt index 228578dfb3..cd6769afc9 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt @@ -842,4 +842,4 @@ open class JavaMethodTestRunner : TestRunner, KClass<*>?, J private val KFunction<*>.declaringClass: Class<*>? get() = (javaMethod ?: javaConstructor)?.declaringClass -private typealias StaticsType = Map> \ No newline at end of file +private typealias StaticsType = Map> diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt index dd7e3717d4..2aa5de47a7 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt @@ -17,6 +17,7 @@ import org.usvm.util.isException import kotlin.math.pow internal class RecursionTest : ApproximationsTestRunner() { + @UsvmTest([Options([PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM])]) fun testFactorial(options: UMachineOptions) { withOptions(options) { @@ -81,12 +82,15 @@ internal class RecursionTest : ApproximationsTestRunner() { @Test fun vertexSumTest() { - checkDiscoveredProperties( - Recursion::vertexSum, - between(2..3), - { _, x, _ -> x <= 10 }, - { _, x, _ -> x > 10 } - ) + val options = options.copy(stepsFromLastCovered = 4500L) + withOptions(options) { + checkDiscoveredProperties( + Recursion::vertexSum, + between(2..3), + { _, x, _ -> x <= 10 }, + { _, x, _ -> x > 10 } + ) + } } @Test From 04f1e4730e906c7fd9eab62846251080d9df844f Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Tue, 13 Aug 2024 16:55:48 +0300 Subject: [PATCH 3/3] supported final method case in virtual call - added case for approximated interfaces --- .../org/usvm/machine/interpreter/JcInterpreter.kt | 10 ++++++++++ 1 file changed, 10 insertions(+) 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 cc42ff352b..128dfefae1 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 @@ -307,6 +307,16 @@ class JcInterpreter( return } + if (method.isFinal) { + // Case for approximated interfaces + with (stmt) { + scope.doWithState { + newStmt(JcConcreteMethodCallInst(location, method, arguments, returnSite)) + } + } + return + } + resolveVirtualInvoke(stmt, scope) }