Updated approximations version (#208)

* updated approximations version * increased 'stepsFromLastCovered' - increased 'stepsFromLastCovered' to suite new approximations * supported final method case in virtual call - added case for approximated interfaces
UnitTestBot · Aug 14, 2024 · 2a277d2 · 2a277d2
1 parent 7a19f2f
commit 2a277d2
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 8 deletions.
diff --git 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"))

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
@@ -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)
             }
 

diff --git 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<JcTest, KFunction<*>, KClass<*>?, J
 private val KFunction<*>.declaringClass: Class<*>?
     get() = (javaMethod ?: javaConstructor)?.declaringClass
 
-private typealias StaticsType = Map<JcClassOrInterface, List<StaticFieldValue>>
+private typealias StaticsType = Map<JcClassOrInterface, List<StaticFieldValue>>
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
@@ -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