Stdlib approximations (#62)

Co-authored-by: Alexey Menshutin <[email protected]>
UnitTestBot · Sep 27, 2023 · f37c4e6 · f37c4e6
1 parent a4123e6
commit f37c4e6
Show file tree

Hide file tree

Showing 19 changed files with 1,019 additions and 67 deletions.
diff --git a/buildSrc/src/main/kotlin/Versions.kt b/buildSrc/src/main/kotlin/Versions.kt
@@ -4,7 +4,7 @@ object Versions {
     const val ksmt = "0.5.7"
     const val collections = "0.3.5"
     const val coroutines = "1.6.4"
-    const val jcdb = "1.2.0"
+    const val jcdb = "1.3.0"
     const val mockk = "1.13.4"
     const val junitParams = "5.9.3"
     const val logback = "1.4.8"

diff --git a/usvm-core/src/main/kotlin/org/usvm/api/EngineApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/EngineApi.kt
@@ -1,14 +1,99 @@
 package org.usvm.api
 
 import org.usvm.UBoolExpr
+import org.usvm.UExpr
 import org.usvm.UHeapRef
+import org.usvm.UNullRef
+import org.usvm.USort
 import org.usvm.UState
+import org.usvm.constraints.UTypeEvaluator
+import org.usvm.memory.mapWithStaticAsConcrete
+import org.usvm.types.UTypeStream
+import org.usvm.types.singleOrNull
+import org.usvm.uctx
 
+fun <Type> UTypeEvaluator<Type>.evalTypeEquals(ref: UHeapRef, type: Type): UBoolExpr =
+    with(ref.uctx) {
+        mkAnd(
+            evalIsSubtype(ref, type),
+            evalIsSupertype(ref, type)
+        )
+    }
 
-fun UState<*, *, *, *, *, *>.assume(expr: UBoolExpr) {
-    pathConstraints += expr
+fun <Type> UState<Type, *, *, *, *, *>.objectTypeEquals(
+    lhs: UHeapRef,
+    rhs: UHeapRef
+): UBoolExpr = with(lhs.uctx) {
+    mapTypeStream(
+        ref = lhs,
+        onNull = {
+            // type(null) = type(null); type(null) <: T /\ T <: type(null) ==> true /\ false
+            mapTypeStream(rhs, onNull = { trueExpr }, { _, _ -> falseExpr })
+        },
+        operation = { lhsRef, lhsTypes ->
+            mapTypeStream(
+                rhs,
+                onNull = { falseExpr },
+                operation = { rhsRef, rhsTypes ->
+                    mkTypeEqualsConstraint(lhsRef, lhsTypes, rhsRef, rhsTypes)
+                }
+            )
+        }
+    )
 }
 
-fun UState<*, *, *, *, *, *>.objectTypeEquals(lhs: UHeapRef, rhs: UHeapRef): UBoolExpr {
-    TODO("Objects types equality check: $lhs, $rhs")
+fun <Type, R : USort> UState<Type, *, *, *, *, *>.mapTypeStream(
+    ref: UHeapRef,
+    operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>?
+): UExpr<R>? = mapTypeStream(
+    ref = ref,
+    onNull = { return null },
+    operation = { expr, types ->
+        operation(expr, types) ?: return null
+    }
+)
+
+private fun <Type> UState<Type, *, *, *, *, *>.mkTypeEqualsConstraint(
+    lhs: UHeapRef,
+    lhsTypes: UTypeStream<Type>,
+    rhs: UHeapRef,
+    rhsTypes: UTypeStream<Type>,
+): UBoolExpr = with(lhs.uctx) {
+    val lhsType = lhsTypes.singleOrNull()
+    val rhsType = rhsTypes.singleOrNull()
+
+    if (lhsType != null) {
+        return if (lhsType == rhsType) {
+            trueExpr
+        } else {
+            memory.types.evalTypeEquals(rhs, lhsType)
+        }
+    }
+
+    if (rhsType != null) {
+        return memory.types.evalTypeEquals(lhs, rhsType)
+    }
+
+    // TODO: don't mock type equals
+    makeSymbolicPrimitive(boolSort)
 }
+
+private inline fun <Type, R : USort> UState<Type, *, *, *, *, *>.mapTypeStream(
+    ref: UHeapRef,
+    onNull: () -> UExpr<R>,
+    operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>
+): UExpr<R> = ref.mapWithStaticAsConcrete(
+    ignoreNullRefs = false,
+    concreteMapper = { concreteRef ->
+        val types = memory.types.getTypeStream(concreteRef)
+        operation(concreteRef, types)
+    },
+    symbolicMapper = { symbolicRef ->
+        if (symbolicRef is UNullRef) {
+            onNull()
+        } else {
+            val types = memory.types.getTypeStream(symbolicRef)
+            operation(symbolicRef, types)
+        }
+    },
+)
diff --git a/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt
@@ -1,8 +1,9 @@
 package org.usvm.api
 
+import org.usvm.StepScope
+import org.usvm.UBoolExpr
 import org.usvm.UExpr
 import org.usvm.UHeapRef
-import org.usvm.USizeExpr
 import org.usvm.USort
 import org.usvm.UState
 import org.usvm.uctx
@@ -16,22 +17,28 @@ fun <Method, T : USort> UState<*, Method, *, *, *, *>.makeSymbolicPrimitive(
     return memory.mock { call(lastEnteredMethod, emptySequence(), sort) }
 }
 
-fun <Type, Method> UState<Type, Method, *, *, *, *>.makeSymbolicRef(type: Type): UHeapRef {
-    val ref = memory.mock { call(lastEnteredMethod, emptySequence(), memory.ctx.addressSort) }
+fun <Type, Method, State> StepScope<State, Type, *>.makeSymbolicRef(
+    type: Type
+): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
+    mockSymbolicRef { memory.types.evalTypeEquals(it, type) }
 
-    memory.types.addSubtype(ref, type)
-    memory.types.addSupertype(ref, type)
+fun <Type, Method, State> StepScope<State, Type, *>.makeSymbolicRefWithSameType(
+    representative: UHeapRef
+): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
+    mockSymbolicRef { objectTypeEquals(it, representative) }
 
-    return ref
-}
-
-fun <Type, Method> UState<Type, Method, *, *, *, *>.makeSymbolicArray(arrayType: Type, size: USizeExpr): UHeapRef {
-    val ref = memory.mock { call(lastEnteredMethod, emptySequence(), memory.ctx.addressSort) }
+private inline fun <Type, Method, State> StepScope<State, Type, *>.mockSymbolicRef(
+    crossinline mkTypeConstraint: State.(UHeapRef) -> UBoolExpr
+): UHeapRef? where State : UState<Type, Method, *, *, *, State> {
+    val ref = calcOnState {
+        memory.mock { call(lastEnteredMethod, emptySequence(), memory.ctx.addressSort) }
+    }
 
-    memory.types.addSubtype(ref, arrayType)
-    memory.types.addSupertype(ref, arrayType)
+    val typeConstraint = calcOnState {
+        mkTypeConstraint(ref)
+    }
 
-    memory.writeArrayLength(ref, size, arrayType)
+    assert(typeConstraint) ?: return null
 
     return ref
 }

diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt
@@ -16,7 +16,17 @@ import org.usvm.types.UTypeSystem
 import org.usvm.uctx
 
 interface UTypeEvaluator<Type> {
+
+    /**
+     * Check that [ref] = `null` or type([ref]) <: [supertype].
+     * Note that T <: T always holds.
+     * */
     fun evalIsSubtype(ref: UHeapRef, supertype: Type): UBoolExpr
+
+    /**
+     * Check that [ref] != `null` and [subtype] <: type([ref]).
+     * Note that T <: T always holds.
+     * */
     fun evalIsSupertype(ref: UHeapRef, subtype: Type): UBoolExpr
     fun getTypeStream(ref: UHeapRef): UTypeStream<Type>
 }

diff --git a/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt b/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt
@@ -75,6 +75,11 @@ fun <Type> UTypeStream<Type>.first(): Type = take(1).first()
 
 fun <Type> UTypeStream<Type>.firstOrNull(): Type? = take(1).firstOrNull()
 
+// Note: we try to take at least two types to ensure that we don't have no more than one type.
+fun <Type> UTypeStream<Type>.single(): Type = take(2).single()
+
+fun <Type> UTypeStream<Type>.singleOrNull(): Type? = take(2).singleOrNull()
+
 /**
  * Consists of just one type [singleType].
  */

diff --git a/usvm-jvm/build.gradle.kts b/usvm-jvm/build.gradle.kts
@@ -2,12 +2,32 @@ plugins {
     id("usvm.kotlin-conventions")
 }
 
+val samples by sourceSets.creating {
+    java {
+        srcDir("src/samples/java")
+    }
+}
+
+val `usvm-api` by sourceSets.creating {
+    java {
+        srcDir("src/usvm-api/java")
+    }
+}
+
+val approximations by configurations.creating
+val approximationsRepo = "com.github.UnitTestBot.java-stdlib-approximations"
+val approximationsVersion = "53ceeb23ea"
+
 dependencies {
     implementation(project(":usvm-core"))
 
     implementation("org.jacodb:jacodb-core:${Versions.jcdb}")
     implementation("org.jacodb:jacodb-analysis:${Versions.jcdb}")
 
+    implementation("org.jacodb:jacodb-approximations:${Versions.jcdb}")
+
+    implementation(`usvm-api`.output)
+
     implementation("io.ksmt:ksmt-yices:${Versions.ksmt}")
     implementation("io.ksmt:ksmt-cvc5:${Versions.ksmt}")
     implementation("io.ksmt:ksmt-symfpu:${Versions.ksmt}")
@@ -16,22 +36,14 @@ dependencies {
     testImplementation("org.junit.jupiter:junit-jupiter-params:${Versions.junitParams}")
     testImplementation("ch.qos.logback:logback-classic:${Versions.logback}")
 
+    testImplementation(samples.output)
+
     // https://mvnrepository.com/artifact/org.burningwave/core
     // Use it to export all modules to all
     testImplementation("org.burningwave:core:12.62.7")
-}
-
-sourceSets {
-    val samples by creating {
-        java {
-            srcDir("src/samples/java")
-        }
-    }
 
-    test {
-        compileClasspath += samples.output
-        runtimeClasspath += samples.output
-    }
+    approximations(approximationsRepo, "approximations", approximationsVersion)
+    testImplementation(approximationsRepo, "tests", approximationsVersion)
 }
 
 val samplesImplementation: Configuration by configurations.getting
@@ -43,3 +55,18 @@ dependencies {
     samplesImplementation("com.github.stephenc.findbugs:findbugs-annotations:${Versions.samplesFindBugs}")
     samplesImplementation("org.jetbrains:annotations:${Versions.samplesJetbrainsAnnotations}")
 }
+
+val `usvm-api-jar` = tasks.register<Jar>("usvm-api-jar") {
+    archiveBaseName.set(`usvm-api`.name)
+    from(`usvm-api`.output)
+}
+
+tasks.withType<Test> {
+    dependsOn(`usvm-api-jar`)
+
+    val usvmApiJarPath = `usvm-api-jar`.get().outputs.files.singleFile
+    val usvmApproximationJarPath = approximations.resolvedConfiguration.files.single()
+
+    environment("usvm.jvm.api.jar.path", usvmApiJarPath.absolutePath)
+    environment("usvm.jvm.approximations.jar.path", usvmApproximationJarPath.absolutePath)
+}