Import Emil's experimental Go SSA/JacoDB prototype

.github/workflows/ci.yml

@@ -38,6 +38,49 @@ jobs:
           path: '**/build/reports/'
           retention-days: 1
 
+  ci-go:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Setup Java JDK
+        uses: actions/setup-java@v4
+        with:
+          java-version: ${{ env.JAVA }}
+          distribution: ${{ env.JAVA_DISTRIBUTION }}
+
+      - name: Setup Go
+        uses: actions/setup-go@v5
+        with:
+          go-version: '1.22.3'
+          cache-dependency-path: usvm-go/src/main/go/go.sum
+
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v4
+
+      - name: Compile Go prototype and run lint
+        run: >-
+          ./gradlew :usvm-go:compileTestKotlin :usvm-go:detektMain :usvm-go:detektTest
+          --configure-on-demand --no-daemon --max-workers=1
+
+      - name: Check Go exporter variadic method signatures
+        working-directory: usvm-go/src/main/go
+        env:
+          GOTOOLCHAIN: go1.22.3
+          GOMAXPROCS: 1
+          GOFLAGS: -p=1
+        run: go test . -run '^TestMethodSignaturesPreserveVariadicParameters$' -count=1
+
+      - name: Upload Gradle reports
+        if: (!cancelled())
+        uses: actions/upload-artifact@v4
+        with:
+          name: gradle-reports-go
+          path: '**/build/reports/'
+          retention-days: 1
+
   ci-jvm:
     runs-on: ubuntu-24.04
     steps:

build.gradle.kts

@@ -10,6 +10,7 @@ tasks.register("validateProjectList") {
         // Define the expected subprojects here.
         val expectedProjects = setOf(
             project(":usvm-core"),
+            project(":usvm-go"),
             project(":usvm-detekt-rules"),
             project(":usvm-util"),
             project(":usvm-dataflow"),

buildSrc/src/main/kotlin/Dependencies.kt

@@ -117,6 +117,12 @@ object Libs {
 
     // https://github.com/UnitTestBot/jacodb
     private const val jacodbPackage = "com.github.UnitTestBot.jacodb" // use "org.jacodb" with includeBuild
+    val jacodb_go = dep(
+        group = jacodbPackage,
+        name = "jacodb-go",
+        version = "a839f86ca8"
+    )
+
     val jacodb_core = dep(
         group = jacodbPackage,
         name = "jacodb-core",

settings.gradle.kts

@@ -28,6 +28,7 @@ develocity {
 }
 
 include("usvm-core")
+include("usvm-go")
 include("usvm-detekt-rules")
 include("usvm-jvm")
 include("usvm-jvm:usvm-jvm-api")

usvm-core/src/main/kotlin/org/usvm/Composition.kt

@@ -122,6 +122,8 @@ open class UComposer<Type, USizeSort : USort>(
     override fun transform(expr: UConcreteHeapRef): UExpr<UAddressSort> = expr
 
     override fun transform(expr: UNullRef): UExpr<UAddressSort> = memory.nullRef()
+
+    override fun transform(expr: ULValuePointer): UExpr<UAddressSort> = expr
 }
 
 @Suppress("NOTHING_TO_INLINE")

usvm-core/src/main/kotlin/org/usvm/ExprTransformer.kt

@@ -67,6 +67,8 @@ interface UTransformer<Type, USizeSort : USort> : KTransformer {
     fun transform(expr: UConcreteHeapRef): UExpr<UAddressSort>
 
     fun transform(expr: UNullRef): UExpr<UAddressSort>
+
+    fun transform(expr: ULValuePointer): UExpr<UAddressSort>
 }
 
 abstract class UExprTransformer<Type, USizeSort : USort>(

usvm-core/src/main/kotlin/org/usvm/Expressions.kt

@@ -21,6 +21,7 @@
 import io.ksmt.sort.KFpSort
 import io.ksmt.sort.KSort
 import io.ksmt.sort.KUninterpretedSort
+import org.usvm.memory.ULValue
 import org.usvm.memory.USymbolicCollection
 import org.usvm.memory.USymbolicCollectionId
 import kotlin.contracts.ExperimentalContracts
@@ -315,6 +316,30 @@
 
 //endregion
 
+//region Pointer Semantics
+
+class ULValuePointer(
+    ctx: UContext<*>,
+    var lvalue: ULValue<*, *>
+) : UExpr<UAddressSort>(ctx) {
+    override val sort: UAddressSort = ctx.addressSort
+
+    override fun accept(transformer: KTransformerBase): KExpr<UAddressSort> {
+        require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" }
+        return transformer.transform(this)
+    }
+
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other) { lvalue }
+
+    override fun internHashCode(): Int = hash(lvalue)
+
+    override fun print(printer: ExpressionPrinter) {
+        printer.append("&$lvalue")
+    }
+}
+
+//endregion
+
 //region Utils
 
 val UBoolExpr.isFalse get() = this == ctx.falseExpr

usvm-core/src/main/kotlin/org/usvm/api/collection/PrimitiveMapCollectionApi.kt

@@ -0,0 +1,127 @@
+package org.usvm.api.collection
+
+import io.ksmt.utils.uncheckedCast
+import org.usvm.UBoolExpr
+import org.usvm.UContext
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.USort
+import org.usvm.UState
+import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapSize
+import org.usvm.api.makeSymbolicPrimitive
+import org.usvm.api.setContainsElement
+import org.usvm.collection.map.length.UMapLengthLValue
+import org.usvm.collection.map.primitive.UMapEntryLValue
+import org.usvm.collection.map.primitive.mapMerge
+import org.usvm.collection.set.primitive.USetEntryLValue
+import org.usvm.collection.set.primitive.USetRegionId
+import org.usvm.collection.set.primitive.setEntries
+import org.usvm.collection.set.primitive.setUnion
+import org.usvm.isFalse
+import org.usvm.isTrue
+import org.usvm.memory.USymbolicCollectionKeyInfo
+import org.usvm.mkSizeAddExpr
+import org.usvm.mkSizeExpr
+import org.usvm.mkSizeSubExpr
+import org.usvm.regions.Region
+import org.usvm.sizeSort
+
+object PrimitiveMapCollectionApi {
+    fun <MapType, KeySort : USort, ValueSort: USort, Reg : Region<Reg>> UState<MapType, *, *, *, *, *>.symbolicPrimitiveMapGet(
+        mapRef: UHeapRef,
+        key: UExpr<KeySort>,
+        mapType: MapType,
+        valueSort: ValueSort,
+        keyInfo: USymbolicCollectionKeyInfo<UExpr<KeySort>, Reg>,
+    ): UExpr<ValueSort> = memory.read(UMapEntryLValue(key.sort, valueSort, mapRef, key, mapType, keyInfo))
+
+    fun <MapType, KeySort : USort, Reg : Region<Reg>> UState<MapType, *, *, *, *, *>.symbolicPrimitiveMapContains(
+        mapRef: UHeapRef,
+        key: UExpr<KeySort>,
+        mapType: MapType,
+        keyInfo: USymbolicCollectionKeyInfo<UExpr<KeySort>, Reg>,
+    ): UBoolExpr = memory.setContainsElement(mapRef, key, mapType, keyInfo)
+
+    fun <MapType, KeySort : USort, Reg : Region<Reg>> UState<MapType, *, *, *, *, *>.symbolicPrimitiveMapAnyKey(
+        mapRef: UHeapRef,
+        mapType: MapType,
+        keySort: KeySort,
+        keyInfo: USymbolicCollectionKeyInfo<UExpr<KeySort>, Reg>,
+    ): UExpr<KeySort> {
+        val allKeys = memory.setEntries(mapRef, mapType, keySort, keyInfo)
+        val symbolicKeys = mutableListOf<Pair<UExpr<KeySort>, UBoolExpr>>()
+        for (entry in allKeys.entries) {
+            val key = entry.setElement
+            val contains = symbolicPrimitiveMapContains(mapRef, key, mapType, keyInfo)
+            when {
+                contains.isTrue -> return key
+                contains.isFalse -> continue
+                else -> symbolicKeys += key to contains
+            }
+        }
+
+        val defaultKey = makeSymbolicPrimitive(keySort)
+        return symbolicKeys.fold(defaultKey) { result, (key, contains) ->
+            ctx.mkIte(contains, key, result)
+        }
+    }
+
+    fun <MapType, USizeSort : USort, Ctx : UContext<USizeSort>, KeySort : USort, ValueSort : USort, Reg : Region<Reg>> UState<MapType, *, *, Ctx, *, *>.symbolicPrimitiveMapPut(
+        mapRef: UHeapRef,
+        key: UExpr<KeySort>,
+        value: UExpr<ValueSort>,
+        mapType: MapType,
+        keyInfo: USymbolicCollectionKeyInfo<UExpr<KeySort>, Reg>,
+    ) = with(ctx) {
+        val mapContainsLValue = USetEntryLValue(key.sort, mapRef, key, mapType, keyInfo)
+        val currentSize = symbolicObjectMapSize(mapRef, mapType)
+
+        val keyIsInMap = memory.read(mapContainsLValue)
+        val keyIsNew = mkNot(keyIsInMap)
+
+        memory.write(UMapEntryLValue(key.sort, value.sort, mapRef, key, mapType, keyInfo), value, guard = trueExpr)
+        memory.write(mapContainsLValue, rvalue = trueExpr, guard = trueExpr)
+
+        val updatedSize = mkSizeAddExpr(currentSize, mkSizeExpr(1))
+        memory.write(UMapLengthLValue(mapRef, mapType, sizeSort), updatedSize, keyIsNew)
+    }
+
+    fun <MapType, USizeSort : USort, Ctx : UContext<USizeSort>, KeySort : USort, Reg : Region<Reg>> UState<MapType, *, *, Ctx, *, *>.symbolicPrimitiveMapRemove(
+        mapRef: UHeapRef,
+        key: UExpr<KeySort>,
+        mapType: MapType,
+        keyInfo: USymbolicCollectionKeyInfo<UExpr<KeySort>, Reg>,
+    ) = with(ctx) {
+        val mapContainsLValue = USetEntryLValue(key.sort, mapRef, key, mapType, keyInfo)
+        val currentSize = symbolicObjectMapSize(mapRef, mapType)
+
+        val keyIsInMap = memory.read(mapContainsLValue)
+
+        // todo: skip values update?
+        memory.write(mapContainsLValue, rvalue = falseExpr, guard = trueExpr)
+
+        val updatedSize = mkSizeSubExpr(currentSize, mkSizeExpr(1))
+        memory.write(UMapLengthLValue(mapRef, mapType, sizeSort), updatedSize, keyIsInMap)
+    }
+
+    fun <MapType, USizeSort : USort, Ctx: UContext<USizeSort>, KeySort : USort, ValueSort : USort, Reg : Region<Reg>> UState<MapType, *, *, Ctx, *, *>.symbolicPrimitiveMapMergeInto(
+        dstRef: UHeapRef,
+        srcRef: UHeapRef,
+        mapType: MapType,
+        keySort: KeySort,
+        valueSort: ValueSort,
+        keyInfo: USymbolicCollectionKeyInfo<UExpr<KeySort>, Reg>,
+    ) = with(ctx) {
+        val srcMapSize = symbolicObjectMapSize(srcRef, mapType)
+        val dstMapSize = symbolicObjectMapSize(dstRef, mapType)
+
+        val containsSetId = USetRegionId(keySort, mapType, keyInfo)
+        memory.mapMerge(srcRef, dstRef, mapType, keySort, valueSort, keyInfo, containsSetId.uncheckedCast(), guard = trueExpr)
+        memory.setUnion(srcRef, dstRef, mapType, keySort, keyInfo, guard = trueExpr)
+
+        // todo: precise map size approximation?
+        // val sizeLowerBound = mkIte(mkBvSignedGreaterExpr(srcMapSize, dstMapSize), srcMapSize, dstMapSize)
+        val sizeUpperBound = mkSizeAddExpr(srcMapSize, dstMapSize)
+        memory.write(UMapLengthLValue(dstRef, mapType, sizeSort), sizeUpperBound, guard = trueExpr)
+    }
+}

usvm-core/src/main/kotlin/org/usvm/solver/ExprTranslator.kt

@@ -17,6 +17,7 @@ import org.usvm.UIndexedMethodReturnValue
 import org.usvm.UIsExpr
 import org.usvm.UIsSubtypeExpr
 import org.usvm.UIsSupertypeExpr
+import org.usvm.ULValuePointer
 import org.usvm.UNullRef
 import org.usvm.URegisterReading
 import org.usvm.USort
@@ -94,6 +95,11 @@ open class UExprTranslator<Type, USizeSort : USort>(
         return const
     }
 
+    override fun transform(expr: ULValuePointer): KExpr<UAddressSort> {
+        val const = expr.sort.mkConst("&${expr.lvalue}")
+        return const
+    }
+
     override fun transform(expr: UConcreteHeapRef): KExpr<UAddressSort> {
         require(isStaticHeapRef(expr)) { "Unexpected ref: $expr" }
 

usvm-core/src/main/kotlin/org/usvm/solver/USoftConstraintsProvider.kt

@@ -31,6 +31,7 @@ import org.usvm.UExpr
 import org.usvm.UIndexedMethodReturnValue
 import org.usvm.UIsSubtypeExpr
 import org.usvm.UIsSupertypeExpr
+import org.usvm.ULValuePointer
 import org.usvm.UNullRef
 import org.usvm.URegisterReading
 import org.usvm.USort
@@ -124,6 +125,8 @@ open class USoftConstraintsProvider<Type, USizeSort : USort>(
 
     override fun transform(expr: UNullRef): UExpr<UAddressSort> = expr
 
+    override fun transform(expr: ULValuePointer): UExpr<UAddressSort> = expr
+
     override fun transform(expr: UIsSubtypeExpr<Type>): UBoolExpr = expr
 
     override fun transform(expr: UIsSupertypeExpr<Type>): UBoolExpr = expr

usvm-go/.gitignore

@@ -0,0 +1,3 @@
+src/**/gen
+src/main/go/dump/
+out/

usvm-go/build.gradle.kts

@@ -0,0 +1,29 @@
+import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
+
+plugins {
+    kotlin("jvm")
+    id("org.gradle.application")
+    id("usvm.kotlin-conventions")
+    id("org.jetbrains.kotlin.plugin.serialization") version "2.0.20"
+}
+
+tasks {
+    withType<KotlinCompile> {
+        kotlinOptions {
+            allWarningsAsErrors = false
+        }
+    }
+}
+
+dependencies {
+    implementation(project(":usvm-core"))
+
+    implementation(Libs.jacodb_go)
+    implementation(Libs.kotlinx_serialization_core)
+    implementation(Libs.kotlinx_serialization_json)
+    implementation(Libs.kotlinx_collections)
+    implementation(Libs.ksmt_yices)
+    implementation(Libs.slf4j_simple)
+
+    testImplementation(Libs.logback)
+}

usvm-go/src/main/go/examples/array.go

@@ -0,0 +1,15 @@
+package examples
+
+func arrayIndex(arr [3]int, i int) int {
+	return arr[i]
+}
+
+func arrayIndexMake(i int) int {
+	arr := [3]int{1, 2, 3}
+	return arr[i]
+}
+
+func arraySlice() []int {
+	arr := [3]int{1, 2, 3}
+	return arr[1:2]
+}

usvm-go/src/main/go/examples/constraint.go

@@ -0,0 +1,13 @@
+package examples
+
+func checkGoodString(s string) {
+	if len(s) < 3 {
+		panic("string too small")
+	}
+
+	for _, r := range s {
+		if r < 97 || r > 122 {
+			panic("bad char")
+		}
+	}
+}