Introduced static refs, supported enums (#61)

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

@@ -114,38 +114,54 @@ open class UContext(
         }
 
     fun mkHeapRefEq(lhs: UHeapRef, rhs: UHeapRef): UBoolExpr =
-        when {
-            // fast checks
-            lhs is USymbolicHeapRef && rhs is USymbolicHeapRef -> super.mkEq(lhs, rhs, order = true)
-            lhs is UConcreteHeapRef && rhs is UConcreteHeapRef -> mkBool(lhs == rhs)
+        mkHeapEqWithFastChecks(lhs, rhs) {
             // unfolding
-            else -> {
-                val (concreteRefsLhs, symbolicRefLhs) = splitUHeapRef(lhs, ignoreNullRefs = false)
-                val (concreteRefsRhs, symbolicRefRhs) = splitUHeapRef(rhs, ignoreNullRefs = false)
-
-                val concreteRefLhsToGuard = concreteRefsLhs.associate { it.expr.address to it.guard }
-
-                val conjuncts = mutableListOf<UBoolExpr>(falseExpr)
-
-                concreteRefsRhs.forEach { (concreteRefRhs, guardRhs) ->
-                    val guardLhs = concreteRefLhsToGuard.getOrDefault(concreteRefRhs.address, falseExpr)
-                    // mkAnd instead of mkAnd with flat=false here is OK
-                    val conjunct = mkAnd(guardLhs, guardRhs)
-                    conjuncts += conjunct
-                }
-
-                if (symbolicRefLhs != null && symbolicRefRhs != null) {
-                    val refsEq = super.mkEq(symbolicRefLhs.expr, symbolicRefRhs.expr, order = true)
-                    // mkAnd instead of mkAnd with flat=false here is OK
-                    val conjunct = mkAnd(symbolicRefLhs.guard, symbolicRefRhs.guard, refsEq)
-                    conjuncts += conjunct
-                }
-
-                // it's safe to use mkOr here
-                mkOr(conjuncts)
+            val (concreteRefsLhs, symbolicRefLhs) = splitUHeapRef(lhs, ignoreNullRefs = false)
+            val (concreteRefsRhs, symbolicRefRhs) = splitUHeapRef(rhs, ignoreNullRefs = false)
+
+            val concreteRefLhsToGuard = concreteRefsLhs.associate { it.expr.address to it.guard }
+
+            val conjuncts = mutableListOf<UBoolExpr>(falseExpr)
+
+            concreteRefsRhs.forEach { (concreteRefRhs, guardRhs) ->
+                val guardLhs = concreteRefLhsToGuard.getOrDefault(concreteRefRhs.address, falseExpr)
+                // mkAnd instead of mkAnd with flat=false here is OK
+                val conjunct = mkAnd(guardLhs, guardRhs)
+                conjuncts += conjunct
             }
+
+            if (symbolicRefLhs != null && symbolicRefRhs != null) {
+                val refsEq = super.mkEq(symbolicRefLhs.expr, symbolicRefRhs.expr, order = true)
+                // mkAnd instead of mkAnd with flat=false here is OK
+                val conjunct = mkAnd(symbolicRefLhs.guard, symbolicRefRhs.guard, refsEq)
+                conjuncts += conjunct
+            }
+
+            // it's safe to use mkOr here
+            mkOr(conjuncts)
         }
 
+    private inline fun mkHeapEqWithFastChecks(
+        lhs: UHeapRef,
+        rhs: UHeapRef,
+        blockOnFailedFastChecks: () -> UBoolExpr,
+    ): UBoolExpr = when {
+        lhs is USymbolicHeapRef && rhs is USymbolicHeapRef -> super.mkEq(lhs, rhs, order = true)
+        isAllocatedConcreteHeapRef(lhs) && isAllocatedConcreteHeapRef(rhs) -> mkBool(lhs == rhs)
+        isStaticHeapRef(lhs) && isStaticHeapRef(rhs) -> mkBool(lhs == rhs)
+
+        isAllocatedConcreteHeapRef(lhs) && isStaticHeapRef(rhs) -> falseExpr
+        isStaticHeapRef(lhs) && isAllocatedConcreteHeapRef(rhs) -> falseExpr
+
+        isStaticHeapRef(lhs) && rhs is UNullRef -> falseExpr
+        lhs is UNullRef && isStaticHeapRef(rhs) -> falseExpr
+
+        lhs is USymbolicHeapRef && isStaticHeapRef(rhs) -> super.mkEq(lhs, rhs, order = true)
+        isStaticHeapRef(lhs) && rhs is USymbolicHeapRef -> super.mkEq(lhs, rhs, order = true)
+
+        else -> blockOnFailedFastChecks()
+    }
+
     private val uConcreteHeapRefCache = mkAstInterner<UConcreteHeapRef>()
     fun mkConcreteHeapRef(address: UConcreteHeapAddress): UConcreteHeapRef =
         uConcreteHeapRefCache.createIfContextActive {

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

@@ -26,6 +26,8 @@ import io.ksmt.sort.KSort
 import io.ksmt.sort.KUninterpretedSort
 import org.usvm.memory.USymbolicCollection
 import org.usvm.memory.USymbolicCollectionId
+import kotlin.contracts.ExperimentalContracts
+import kotlin.contracts.contract
 
 //region KSMT aliases
 
@@ -76,8 +78,35 @@ typealias UHeapRef = UExpr<UAddressSort>
 typealias USymbolicHeapRef = USymbol<UAddressSort>
 typealias UConcreteHeapAddress = Int
 
-fun isSymbolicHeapRef(expr: UExpr<*>) =
-    expr.sort == expr.uctx.addressSort && expr is USymbol<*>
+@OptIn(ExperimentalContracts::class)
+fun isSymbolicHeapRef(expr: UExpr<*>): Boolean {
+    contract {
+        returns(true) implies (expr is USymbol<*>)
+    }
+
+    return expr.sort == expr.uctx.addressSort && expr is USymbol<*>
+}
+
+@OptIn(ExperimentalContracts::class)
+fun isAllocatedConcreteHeapRef(expr: UExpr<*>): Boolean {
+    contract {
+        returns(true) implies (expr is UConcreteHeapRef)
+    }
+
+    return expr is UConcreteHeapRef && expr.isAllocated
+}
+
+@OptIn(ExperimentalContracts::class)
+fun isStaticHeapRef(expr: UExpr<*>): Boolean {
+    contract {
+        returns(true) implies (expr is UConcreteHeapRef)
+    }
+
+    return expr is UConcreteHeapRef && expr.isStatic
+}
+
+val UConcreteHeapRef.isAllocated: Boolean get() = address >= INITIAL_CONCRETE_ADDRESS
+val UConcreteHeapRef.isStatic: Boolean get() = address <= INITIAL_STATIC_ADDRESS
 
 class UConcreteHeapRefDecl internal constructor(
     ctx: UContext,
@@ -129,8 +158,9 @@ class UNullRef internal constructor(
     }
 }
 
-// We split all addresses into three parts:
-//     * input values: [Int.MIN_VALUE..0),
+// We split all addresses into four parts:
+//     * static values (represented as allocated but interpreted as input): [Int.MIN_VALUE..INITIAL_STATIC_ADDRESS]
+//     * input values: (INITIAL_STATIC_ADDRESS..0),
 //     * null value: [0]
 //     * allocated values: (0..[Int.MAX_VALUE]
 
@@ -147,10 +177,16 @@ const val INITIAL_INPUT_ADDRESS = NULL_ADDRESS - 1
 
 /**
  * A constant corresponding to the first allocated address in any symbolic memory.
- * Input addresses takes this semi-interval: (0..[Int.MAX_VALUE])
+ * Allocated addresses takes this semi-interval: (0..[Int.MAX_VALUE])
  */
 const val INITIAL_CONCRETE_ADDRESS = NULL_ADDRESS + 1
 
+/**
+ * A constant corresponding to the first static address in any symbolic memory.
+ * Static addresses takes this segment: [[Int.MIN_VALUE]..[INITIAL_STATIC_ADDRESS]]
+ */
+const val INITIAL_STATIC_ADDRESS = -(1 shl 20) // Use value not less than UNINTERPRETED_SORT_MIN_ALLOWED_VALUE in ksmt
+
 
 //endregion
 

usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt

@@ -22,7 +22,8 @@ import org.usvm.collection.array.allocateArrayInitialized as allocateArrayInitia
 fun <Type> UReadOnlyMemory<Type>.typeStreamOf(ref: UHeapRef): UTypeStream<Type> =
     types.getTypeStream(ref)
 
-fun UMemory<*, *>.allocate() = ctx.mkConcreteHeapRef(addressCounter.freshAddress())
+fun UMemory<*, *>.allocateConcreteRef(): UConcreteHeapRef = ctx.mkConcreteHeapRef(addressCounter.freshAllocatedAddress())
+fun UMemory<*, *>.allocateStaticRef(): UConcreteHeapRef = ctx.mkConcreteHeapRef(addressCounter.freshStaticAddress())
 
 fun <Field, Sort : USort> UReadOnlyMemory<*>.readField(
     ref: UHeapRef, field: Field, sort: Sort

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

@@ -11,14 +11,14 @@ import org.usvm.api.readArrayIndex
 import org.usvm.api.readArrayLength
 import org.usvm.api.writeArrayIndex
 import org.usvm.api.writeArrayLength
-import org.usvm.memory.map
+import org.usvm.memory.mapWithStaticAsConcrete
 import org.usvm.uctx
 
 object ListCollectionApi {
     fun <ListType> UState<ListType, *, *, *, *, *>.mkSymbolicList(
         listType: ListType,
     ): UHeapRef = with(memory.ctx) {
-        val ref = memory.alloc(listType)
+        val ref = memory.allocConcrete(listType)
         memory.writeArrayLength(ref, mkSizeExpr(0), listType)
         ref
     }
@@ -36,7 +36,7 @@ object ListCollectionApi {
         listRef: UHeapRef,
         listType: ListType,
     ): Unit? {
-        listRef.map(
+        listRef.mapWithStaticAsConcrete(
             concreteMapper = {
                 // Concrete list size is always correct
                 it

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

@@ -13,14 +13,14 @@ import org.usvm.collection.map.ref.refMapMerge
 import org.usvm.collection.set.ref.URefSetEntryLValue
 import org.usvm.collection.set.ref.URefSetRegionId
 import org.usvm.collection.set.ref.refSetUnion
-import org.usvm.memory.map
+import org.usvm.memory.mapWithStaticAsConcrete
 import org.usvm.uctx
 
 object ObjectMapCollectionApi {
     fun <MapType> UState<MapType, *, *, *, *, *>.mkSymbolicObjectMap(
         mapType: MapType,
     ): UHeapRef = with(memory.ctx) {
-        val ref = memory.alloc(mapType)
+        val ref = memory.allocConcrete(mapType)
         val length = UMapLengthLValue(ref, mapType)
         memory.write(length, mkSizeExpr(0), trueExpr)
         ref
@@ -40,7 +40,7 @@ object ObjectMapCollectionApi {
         mapRef: UHeapRef,
         mapType: MapType,
     ): Unit? {
-        mapRef.map(
+        mapRef.mapWithStaticAsConcrete(
             concreteMapper = {
                 // Concrete map size is always correct
                 it

usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt

@@ -12,10 +12,10 @@ import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.USymbolicCollection
-import org.usvm.memory.foldHeapRef
 import org.usvm.memory.foldHeapRef2
+import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
 import org.usvm.memory.key.USizeExprKeyInfo
-import org.usvm.memory.map
+import org.usvm.memory.mapWithStaticAsSymbolic
 
 data class UArrayIndexLValue<ArrayType, Sort : USort>(
     override val sort: Sort,
@@ -92,32 +92,30 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort>(
     private fun updateInput(updated: UInputArray<ArrayType, Sort>) =
         UArrayMemoryRegion(allocatedArrays, updated)
 
-    override fun read(key: UArrayIndexLValue<ArrayType, Sort>): UExpr<Sort> =
-        key.ref.map(
-            { concreteRef -> getAllocatedArray(key.arrayType, key.sort, concreteRef.address).read(key.index) },
-            { symbolicRef -> getInputArray(key.arrayType, key.sort).read(symbolicRef to key.index) }
-        )
+    override fun read(key: UArrayIndexLValue<ArrayType, Sort>): UExpr<Sort> = key.ref.mapWithStaticAsSymbolic(
+        concreteMapper = { concreteRef -> getAllocatedArray(key.arrayType, key.sort, concreteRef.address).read(key.index) },
+        symbolicMapper = { symbolicRef -> getInputArray(key.arrayType, key.sort).read(symbolicRef to key.index) }
+    )
 
     override fun write(
         key: UArrayIndexLValue<ArrayType, Sort>,
         value: UExpr<Sort>,
         guard: UBoolExpr
-    ): UMemoryRegion<UArrayIndexLValue<ArrayType, Sort>, Sort> =
-        foldHeapRef(
-            key.ref,
-            initial = this,
-            initialGuard = guard,
-            blockOnConcrete = { region, (concreteRef, innerGuard) ->
-                val oldRegion = region.getAllocatedArray(key.arrayType, key.sort, concreteRef.address)
-                val newRegion = oldRegion.write(key.index, value, innerGuard)
-                region.updateAllocatedArray(concreteRef.address, newRegion)
-            },
-            blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
-                val oldRegion = region.getInputArray(key.arrayType, key.sort)
-                val newRegion = oldRegion.write(symbolicRef to key.index, value, innerGuard)
-                region.updateInput(newRegion)
-            }
-        )
+    ): UMemoryRegion<UArrayIndexLValue<ArrayType, Sort>, Sort> = foldHeapRefWithStaticAsSymbolic(
+        key.ref,
+        initial = this,
+        initialGuard = guard,
+        blockOnConcrete = { region, (concreteRef, innerGuard) ->
+            val oldRegion = region.getAllocatedArray(key.arrayType, key.sort, concreteRef.address)
+            val newRegion = oldRegion.write(key.index, value, innerGuard)
+            region.updateAllocatedArray(concreteRef.address, newRegion)
+        },
+        blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
+            val oldRegion = region.getInputArray(key.arrayType, key.sort)
+            val newRegion = oldRegion.write(symbolicRef to key.index, value, innerGuard)
+            region.updateInput(newRegion)
+        }
+    )
 
     override fun memcpy(
         srcRef: UHeapRef,

usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionApi.kt

@@ -60,7 +60,7 @@ internal fun <ArrayType> UWritableMemory<ArrayType>.allocateArray(
     type: ArrayType,
     length: USizeExpr
 ): UConcreteHeapRef {
-    val address = alloc(type)
+    val address = allocConcrete(type)
 
     val lengthRegionRef = UArrayLengthLValue(address, type)
     write(lengthRegionRef, length, guard = length.uctx.trueExpr)

usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegion.kt

@@ -11,9 +11,9 @@ import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.USymbolicCollection
-import org.usvm.memory.foldHeapRef
+import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
 import org.usvm.memory.guardedWrite
-import org.usvm.memory.map
+import org.usvm.memory.mapWithStaticAsSymbolic
 import org.usvm.sampleUValue
 import org.usvm.uctx
 
@@ -60,17 +60,16 @@ internal class UArrayLengthsMemoryRegion<ArrayType>(
     private fun updatedInput(updated: UInputArrayLengths<ArrayType>) =
         UArrayLengthsMemoryRegion(sort, arrayType, allocatedLengths, updated)
 
-    override fun read(key: UArrayLengthLValue<ArrayType>): USizeExpr =
-        key.ref.map(
-            { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
-            { symbolicRef -> getInputLength(key).read(symbolicRef) }
-        )
+    override fun read(key: UArrayLengthLValue<ArrayType>): USizeExpr = key.ref.mapWithStaticAsSymbolic(
+        concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
+        symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef) }
+    )
 
     override fun write(
         key: UArrayLengthLValue<ArrayType>,
         value: USizeExpr,
         guard: UBoolExpr
-    ) = foldHeapRef(
+    ) = foldHeapRefWithStaticAsSymbolic(
         key.ref,
         initial = this,
         initialGuard = guard,

usvm-core/src/main/kotlin/org/usvm/collection/field/FieldsRegion.kt

@@ -11,9 +11,9 @@ import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.USymbolicCollection
-import org.usvm.memory.foldHeapRef
+import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
 import org.usvm.memory.guardedWrite
-import org.usvm.memory.map
+import org.usvm.memory.mapWithStaticAsSymbolic
 import org.usvm.sampleUValue
 
 data class UFieldLValue<Field, Sort : USort>(override val sort: Sort, val ref: UHeapRef, val field: Field) :
@@ -55,31 +55,29 @@ internal class UFieldsMemoryRegion<Field, Sort : USort>(
     private fun updateInput(updated: UInputFields<Field, Sort>) =
         UFieldsMemoryRegion(sort, field, allocatedFields, updated)
 
-    override fun read(key: UFieldLValue<Field, Sort>): UExpr<Sort> =
-        key.ref.map(
-            { concreteRef -> allocatedFields[concreteRef.address] ?: sort.sampleUValue() },
-            { symbolicRef -> getInputFields(key).read(symbolicRef) }
-        )
+    override fun read(key: UFieldLValue<Field, Sort>): UExpr<Sort> = key.ref.mapWithStaticAsSymbolic(
+        concreteMapper = { concreteRef -> allocatedFields[concreteRef.address] ?: sort.sampleUValue() },
+        symbolicMapper = { symbolicRef -> getInputFields(key).read(symbolicRef) }
+    )
 
     override fun write(
         key: UFieldLValue<Field, Sort>,
         value: UExpr<Sort>,
         guard: UBoolExpr
-    ): UMemoryRegion<UFieldLValue<Field, Sort>, Sort> =
-        foldHeapRef(
-            key.ref,
-            initial = this,
-            initialGuard = guard,
-            blockOnConcrete = { region, (concreteRef, innerGuard) ->
-                val newRegion = region.allocatedFields.guardedWrite(concreteRef.address, value, innerGuard) {
-                    sort.sampleUValue()
-                }
-                region.updateAllocated(newRegion)
-            },
-            blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
-                val oldRegion = region.getInputFields(key)
-                val newRegion = oldRegion.write(symbolicRef, value, innerGuard)
-                region.updateInput(newRegion)
+    ): UMemoryRegion<UFieldLValue<Field, Sort>, Sort> = foldHeapRefWithStaticAsSymbolic(
+        key.ref,
+        initial = this,
+        initialGuard = guard,
+        blockOnConcrete = { region, (concreteRef, innerGuard) ->
+            val newRegion = region.allocatedFields.guardedWrite(concreteRef.address, value, innerGuard) {
+                sort.sampleUValue()
             }
-        )
+            region.updateAllocated(newRegion)
+        },
+        blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
+            val oldRegion = region.getInputFields(key)
+            val newRegion = oldRegion.write(symbolicRef, value, innerGuard)
+            region.updateInput(newRegion)
+        }
+    )
 }