Adapt Go prototype with symbolic semantic tests and fixes

.github/workflows/ci.yml

@@ -60,9 +60,9 @@ jobs:
       - name: Setup Gradle
         uses: gradle/actions/setup-gradle@v4
 
-      - name: Compile Go prototype and run lint
+      - name: Run Go regression tests and lint
         run: >-
-          ./gradlew :usvm-go:compileTestKotlin :usvm-go:detektMain :usvm-go:detektTest
+          ./gradlew :usvm-go:check :usvm-go:detektMain :usvm-go:detektTest
           --configure-on-demand --no-daemon --max-workers=1
 
       - name: Check Go exporter variadic method signatures

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

@@ -122,8 +122,6 @@ 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,8 +67,6 @@ 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,7 +21,6 @@ import io.ksmt.sort.KBvSort
 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
@@ -316,30 +315,6 @@ class UIsSupertypeExpr<Type> internal constructor(
 
 //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

@@ -27,22 +27,35 @@ import org.usvm.regions.Region
 import org.usvm.sizeSort
 
 object PrimitiveMapCollectionApi {
-    fun <MapType, KeySort : USort, ValueSort: USort, Reg : Region<Reg>> UState<MapType, *, *, *, *, *>.symbolicPrimitiveMapGet(
+    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(
+    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(
+    fun <
+        MapType,
+        KeySort : USort,
+        Reg : Region<Reg>,
+        > UState<MapType, *, *, *, *, *>.symbolicPrimitiveMapAnyKey(
         mapRef: UHeapRef,
         mapType: MapType,
         keySort: KeySort,
@@ -66,7 +79,14 @@ object PrimitiveMapCollectionApi {
         }
     }
 
-    fun <MapType, USizeSort : USort, Ctx : UContext<USizeSort>, KeySort : USort, ValueSort : USort, Reg : Region<Reg>> UState<MapType, *, *, Ctx, *, *>.symbolicPrimitiveMapPut(
+    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>,
@@ -86,7 +106,13 @@ object PrimitiveMapCollectionApi {
         memory.write(UMapLengthLValue(mapRef, mapType, sizeSort), updatedSize, keyIsNew)
     }
 
-    fun <MapType, USizeSort : USort, Ctx : UContext<USizeSort>, KeySort : USort, Reg : Region<Reg>> UState<MapType, *, *, Ctx, *, *>.symbolicPrimitiveMapRemove(
+    fun <
+        MapType,
+        USizeSort : USort,
+        Ctx : UContext<USizeSort>,
+        KeySort : USort,
+        Reg : Region<Reg>,
+        > UState<MapType, *, *, Ctx, *, *>.symbolicPrimitiveMapRemove(
         mapRef: UHeapRef,
         key: UExpr<KeySort>,
         mapType: MapType,
@@ -97,14 +123,20 @@ object PrimitiveMapCollectionApi {
 
         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(
+    fun <
+        MapType,
+        USizeSort : USort,
+        Ctx : UContext<USizeSort>,
+        KeySort : USort,
+        ValueSort : USort,
+        Reg : Region<Reg>,
+        > UState<MapType, *, *, Ctx, *, *>.symbolicPrimitiveMapCopyIntoEmpty(
         dstRef: UHeapRef,
         srcRef: UHeapRef,
         mapType: MapType,
@@ -114,14 +146,21 @@ object PrimitiveMapCollectionApi {
     ) = 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.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)
+        memory.write(UMapLengthLValue(dstRef, mapType, sizeSort), srcMapSize, guard = trueExpr)
     }
 }

usvm-core/src/main/kotlin/org/usvm/collection/set/ref/USymbolicRefSetUnionAdapter.kt

@@ -157,9 +157,8 @@ class UInputToAllocatedSymbolicRefSetUnionAdapter<SetType>(
 
     override fun collectSetElements(elements: USymbolicSetElementsCollector.Elements<UHeapRef>) {
         val setElements = USymbolicSetElementsCollector.collect(setOfKeys.updates)
-        if (setElements.isInput) {
-            elements.isInput = true
-        }
+        // The initial input collection can contain elements absent from its update tree.
+        elements.isInput = true
         setElements.elements.mapTo(elements.elements) { it.second }
     }
 
@@ -211,9 +210,8 @@ class UInputToInputSymbolicRefSetUnionAdapter<SetType>(
 
     override fun collectSetElements(elements: USymbolicSetElementsCollector.Elements<USymbolicSetElement<UAddressSort>>) {
         val setElements = USymbolicSetElementsCollector.collect(setOfKeys.updates)
-        if (setElements.isInput) {
-            elements.isInput = true
-        }
+        // The initial input collection can contain elements absent from its update tree.
+        elements.isInput = true
         setElements.elements.mapTo(elements.elements) { dstSetRef to it.second }
     }
 

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

@@ -17,7 +17,6 @@ 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
@@ -95,11 +94,6 @@ 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,7 +31,6 @@ 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
@@ -125,8 +124,6 @@ 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-core/src/test/kotlin/org/usvm/api/collections/ObjectMapTest.kt

@@ -253,6 +253,35 @@ class ObjectMapTest : SymbolicCollectionTestBase() {
         testMapMerge(symbolicMap0, symbolicMap1)
     }
 
+    @Test
+    fun testCopiedInputMapCanSelectAnInitialKey() = testInputCopyRetainsUnknownKey(throughSecondCopy = false)
+
+    @Test
+    fun testRepeatedInputMapCopyCanSelectAnInitialKey() = testInputCopyRetainsUnknownKey(throughSecondCopy = true)
+
+    private fun testInputCopyRetainsUnknownKey(throughSecondCopy: Boolean) = scope.doWithState {
+        val source = ctx.mkRegisterReading(idx = 99, sort = ctx.addressSort)
+        val firstCopy = mkSymbolicObjectMap(mapType)
+
+        symbolicObjectMapMergeInto(firstCopy, source, mapType, ctx.sizeSort)
+        val copy = if (throughSecondCopy) {
+            val secondCopy = mkSymbolicObjectMap(mapType)
+            symbolicObjectMapMergeInto(secondCopy, firstCopy, mapType, ctx.sizeSort)
+            secondCopy
+        } else {
+            firstCopy
+        }
+
+        val selectedKey = symbolicObjectMapAnyKey(copy, mapType)
+        val sourceContains = symbolicObjectMapContains(source, selectedKey, mapType)
+        val copyContains = symbolicObjectMapContains(copy, selectedKey, mapType)
+
+        checkWithSolver {
+            assertPossible { mkAnd(mkNot(mkHeapRefEq(source, nullRef)), sourceContains, copyContains) }
+            assertImpossible { mkAnd(copyContains, mkNot(sourceContains)) }
+        }
+    }
+
     @Test
     fun testMapRetrieveAnyKey() = scope.doWithState {
         callStack.push(method = Any(), returnSite = null)

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