Integrate experimental Go frontend with symbolic semantic expectations

.github/workflows/ci.yml

@@ -39,6 +39,39 @@ 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: Run Go regression tests and lint
+        run: ./gradlew :usvm-go:check :usvm-go:detektMain :usvm-go:detektTest --configure-on-demand
+
+      - 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 = "816194b963"
+    )
+
     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/api/collection/PrimitiveMapCollectionApi.kt

@@ -0,0 +1,166 @@
+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)
+
+        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, *, *>.symbolicPrimitiveMapCopyIntoEmpty(
+        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)
+        require(dstMapSize == mkSizeExpr(0)) { "Map copy requires an empty destination" }
+
+        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)
+
+        memory.write(UMapLengthLValue(dstRef, mapType, sizeSort), srcMapSize, guard = trueExpr)
+    }
+}

usvm-core/src/test/kotlin/org/usvm/api/collections/PrimitiveMapTest.kt

@@ -0,0 +1,89 @@
+package org.usvm.api.collections
+
+import io.ksmt.utils.asExpr
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.assertThrows
+import org.usvm.UBv32Sort
+import org.usvm.api.collection.ObjectMapCollectionApi.mkSymbolicObjectMap
+import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapSize
+import org.usvm.api.collection.PrimitiveMapCollectionApi.symbolicPrimitiveMapContains
+import org.usvm.api.collection.PrimitiveMapCollectionApi.symbolicPrimitiveMapCopyIntoEmpty
+import org.usvm.api.collection.PrimitiveMapCollectionApi.symbolicPrimitiveMapGet
+import org.usvm.api.collection.PrimitiveMapCollectionApi.symbolicPrimitiveMapPut
+import org.usvm.api.collection.PrimitiveMapCollectionApi.symbolicPrimitiveMapRemove
+import org.usvm.memory.key.USizeExprKeyInfo
+import org.usvm.mkSizeExpr
+import org.usvm.sizeSort
+import org.usvm.types.single.SingleTypeSystem
+import kotlin.test.assertEquals
+
+class PrimitiveMapTest : SymbolicCollectionTestBase() {
+    private val mapType = SingleTypeSystem.SingleType
+
+    @Test
+    fun overwriteAndRepeatedRemovalPreserveSize() = scope.doWithState {
+        val map = mkSymbolicObjectMap(mapType)
+        val key = ctx.mkBv(7)
+        val keyInfo = USizeExprKeyInfo<UBv32Sort>()
+
+        symbolicPrimitiveMapPut(map, key, ctx.mkBv(1), mapType, keyInfo)
+        symbolicPrimitiveMapPut(map, key, ctx.mkBv(2), mapType, keyInfo)
+
+        assertEquals(ctx.mkSizeExpr(1), symbolicObjectMapSize(map, mapType))
+        assertEquals(ctx.mkBv(2), symbolicPrimitiveMapGet(map, key, mapType, ctx.bv32Sort, keyInfo))
+
+        symbolicPrimitiveMapRemove(map, key, mapType, keyInfo)
+        symbolicPrimitiveMapRemove(map, key, mapType, keyInfo)
+
+        assertEquals(ctx.mkSizeExpr(0), symbolicObjectMapSize(map, mapType))
+        assertEquals(ctx.falseExpr, symbolicPrimitiveMapContains(map, key, mapType, keyInfo))
+    }
+
+    @Test
+    fun symbolicKeyEqualityControlsSize() = scope.doWithState {
+        val map = mkSymbolicObjectMap(mapType)
+        val first = ctx.mkRegisterReading(idx = 0, sort = ctx.bv32Sort)
+        val second = ctx.mkRegisterReading(idx = 1, sort = ctx.bv32Sort)
+        val keyInfo = USizeExprKeyInfo<UBv32Sort>()
+
+        symbolicPrimitiveMapPut(map, first, ctx.mkBv(1), mapType, keyInfo)
+        symbolicPrimitiveMapPut(map, second, ctx.mkBv(2), mapType, keyInfo)
+        val size = symbolicObjectMapSize(map, mapType).asExpr(ctx.sizeSort)
+
+        checkWithSolver {
+            assertImpossible {
+                mkAnd(mkEq(first, second), mkNot(mkEq(size, mkBv(1))))
+            }
+            assertImpossible {
+                mkAnd(mkNot(mkEq(first, second)), mkNot(mkEq(size, mkBv(2))))
+            }
+        }
+    }
+
+    @Test
+    fun copyPreservesEntriesAndSize() = scope.doWithState {
+        val source = mkSymbolicObjectMap(mapType)
+        val destination = mkSymbolicObjectMap(mapType)
+        val key = ctx.mkBv(7)
+        val keyInfo = USizeExprKeyInfo<UBv32Sort>()
+        symbolicPrimitiveMapPut(source, key, ctx.mkBv(42), mapType, keyInfo)
+
+        symbolicPrimitiveMapCopyIntoEmpty(destination, source, mapType, ctx.bv32Sort, ctx.bv32Sort, keyInfo)
+
+        assertEquals(ctx.mkSizeExpr(1), symbolicObjectMapSize(destination, mapType))
+        assertEquals(ctx.trueExpr, symbolicPrimitiveMapContains(destination, key, mapType, keyInfo))
+        assertEquals(ctx.mkBv(42), symbolicPrimitiveMapGet(destination, key, mapType, ctx.bv32Sort, keyInfo))
+    }
+
+    @Test
+    fun copyingIntoNonemptyMapIsRejected() = scope.doWithState {
+        val source = mkSymbolicObjectMap(mapType)
+        val destination = mkSymbolicObjectMap(mapType)
+        val keyInfo = USizeExprKeyInfo<UBv32Sort>()
+        symbolicPrimitiveMapPut(destination, ctx.mkBv(1), ctx.mkBv(42), mapType, keyInfo)
+
+        assertThrows<IllegalArgumentException> {
+            symbolicPrimitiveMapCopyIntoEmpty(destination, source, mapType, ctx.bv32Sort, ctx.bv32Sort, keyInfo)
+        }
+    }
+}

usvm-go/.gitignore

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