Memory rework (#51)

--------- Co-authored-by: Sergey Pospelov <[email protected]> Co-authored-by: Dmitry Mordvinov <[email protected]>
UnitTestBot · Aug 29, 2023 · 29a3340 · 29a3340
1 parent 65eeeba
commit 29a3340
Show file tree

Hide file tree

Showing 125 changed files with 8,430 additions and 2,888 deletions.
diff --git a/docs/meeting-minutes/2023-08-18.md b/docs/meeting-minutes/2023-08-18.md
@@ -0,0 +1,18 @@
+# TODOs for refactoring
+
+- Elaborate on API
+- Make everything internal
+- [+] Implement model decoding: use interfaces for MemoryRegions (arrays, field, etc.)
+- Reimplement map merging into UMapRegions
+- [+] Add (exceptional) `URegisterRef` into `UMemory`
+- `Regions.kt`: implement unions? 
+- Implement symbolic sets: `memory/collections/SymbolicCollectionIds.kt`. Encoding/decoding?
+- Include element remove information into `SymbolicSetRegionBuilder`. For symbolic set do not traverse updates.
+- [+] Interpreter uses new API
+- [+] Think about getting rid of unchecked casts in ranged update adapters
+- [+] Think about moving `contextMemory` from each collectionId to `USymbolicCollectionId`
+- [+] Remove all commented out code
+- [+] Make everything compilable
+- [+] Rebase onto new master
+- [+] Repair tests
+- [+] collection id equals, hash
diff --git a/usvm-core/src/main/kotlin/org/usvm/Composition.kt b/usvm-core/src/main/kotlin/org/usvm/Composition.kt
@@ -1,27 +1,31 @@
 package org.usvm
 
-import io.ksmt.expr.KExpr
-import io.ksmt.expr.KIteExpr
-import io.ksmt.sort.KSort
-import org.usvm.constraints.UTypeEvaluator
-import org.usvm.memory.UReadOnlySymbolicHeap
-import org.usvm.memory.URegionId
-import org.usvm.memory.URegistersStackEvaluator
+import org.usvm.collection.array.UAllocatedArrayReading
+import org.usvm.collection.array.UInputArrayReading
+import org.usvm.collection.array.length.UInputArrayLengthReading
+import org.usvm.collection.field.UInputFieldReading
+import org.usvm.collection.map.length.UInputMapLengthReading
+import org.usvm.collection.map.primitive.UAllocatedMapReading
+import org.usvm.collection.map.primitive.UInputMapReading
+import org.usvm.collection.map.ref.UAllocatedRefMapWithInputKeysReading
+import org.usvm.collection.map.ref.UInputRefMapWithAllocatedKeysReading
+import org.usvm.collection.map.ref.UInputRefMapWithInputKeysReading
+import org.usvm.memory.UReadOnlyMemory
+import org.usvm.memory.USymbolicCollection
+import org.usvm.memory.USymbolicCollectionId
+import org.usvm.util.Region
 
 @Suppress("MemberVisibilityCanBePrivate")
-open class UComposer<Field, Type>(
+open class UComposer<Type>(
     ctx: UContext,
-    internal val stackEvaluator: URegistersStackEvaluator,
-    internal val heapEvaluator: UReadOnlySymbolicHeap<Field, Type>,
-    internal val typeEvaluator: UTypeEvaluator<Type>,
-    internal val mockEvaluator: UMockEvaluator,
-) : UExprTransformer<Field, Type>(ctx) {
+    internal val memory: UReadOnlyMemory<Type>
+) : UExprTransformer<Type>(ctx) {
     open fun <Sort : USort> compose(expr: UExpr<Sort>): UExpr<Sort> = apply(expr)
 
     override fun <Sort : USort> transform(expr: USymbol<Sort>): UExpr<Sort> =
         error("You must override `transform` function in org.usvm.UComposer for ${expr::class}")
 
-    override fun <T : KSort> transform(expr: KIteExpr<T>): KExpr<T> =
+    override fun <T : USort> transform(expr: UIteExpr<T>): UExpr<T> =
         transformExprAfterTransformed(expr, expr.condition) { condition ->
             when {
                 condition.isTrue -> apply(expr.trueBranch)
@@ -32,50 +36,82 @@ open class UComposer<Field, Type>(
 
     override fun <Sort : USort> transform(
         expr: URegisterReading<Sort>,
-    ): UExpr<Sort> = with(expr) { stackEvaluator.readRegister(idx, sort) }
+    ): UExpr<Sort> = with(expr) { memory.stack.readRegister(idx, sort) }
 
-    override fun <Sort : USort> transform(expr: UHeapReading<*, *, *>): UExpr<Sort> =
+    override fun <Sort : USort> transform(expr: UCollectionReading<*, *, *>): UExpr<Sort> =
         error("You must override `transform` function in org.usvm.UComposer for ${expr::class}")
 
     override fun <Sort : USort> transform(expr: UMockSymbol<Sort>): UExpr<Sort> =
         error("You must override `transform` function in org.usvm.UComposer for ${expr::class}")
 
     override fun <Method, Sort : USort> transform(
         expr: UIndexedMethodReturnValue<Method, Sort>,
-    ): UExpr<Sort> = mockEvaluator.eval(expr)
+    ): UExpr<Sort> = memory.mocker.eval(expr)
 
     override fun transform(expr: UIsSubtypeExpr<Type>): UBoolExpr =
         transformExprAfterTransformed(expr, expr.ref) { ref ->
-            typeEvaluator.evalIsSubtype(ref, expr.supertype)
+            memory.types.evalIsSubtype(ref, expr.supertype)
         }
 
     override fun transform(expr: UIsSupertypeExpr<Type>): UBoolExpr =
         transformExprAfterTransformed(expr, expr.ref) { ref ->
-            typeEvaluator.evalIsSupertype(ref, expr.subtype)
+            memory.types.evalIsSupertype(ref, expr.subtype)
         }
 
-    fun <RegionId : URegionId<Key, Sort, RegionId>, Key, Sort : USort> transformHeapReading(
-        expr: UHeapReading<RegionId, Key, Sort>,
+    fun <CollectionId : USymbolicCollectionId<Key, Sort, CollectionId>, Key, Sort : USort> transformCollectionReading(
+        expr: UCollectionReading<CollectionId, Key, Sort>,
         key: Key,
     ): UExpr<Sort> = with(expr) {
-        val mappedRegion = region.map(this@UComposer)
-        val mappedKey = mappedRegion.regionId.keyMapper(this@UComposer)(key)
-        mappedRegion.read(mappedKey)
+        val mappedCollectionId = collection.collectionId.map(this@UComposer)
+        val mappedKey = mappedCollectionId.keyMapper(this@UComposer)(key)
+        val decomposedKey = mappedCollectionId.rebindKey(mappedKey)
+        if (decomposedKey != null) {
+            @Suppress("UNCHECKED_CAST")
+            // I'm terribly sorry to do this cast, but it's impossible to do it type safe way :(
+            val mappedCollection =
+                collection.mapTo(this@UComposer, decomposedKey.collectionId) as USymbolicCollection<*, Any?, Sort>
+            return mappedCollection.read(decomposedKey.key)
+        }
+        val mappedCollection = collection.mapTo(this@UComposer, mappedCollectionId)
+        return mappedCollection.read(mappedKey)
     }
 
     override fun transform(expr: UInputArrayLengthReading<Type>): USizeExpr =
-        transformHeapReading(expr, expr.address)
+        transformCollectionReading(expr, expr.address)
 
     override fun <Sort : USort> transform(expr: UInputArrayReading<Type, Sort>): UExpr<Sort> =
-        transformHeapReading(expr, expr.address to expr.index)
+        transformCollectionReading(expr, expr.address to expr.index)
 
     override fun <Sort : USort> transform(expr: UAllocatedArrayReading<Type, Sort>): UExpr<Sort> =
-        transformHeapReading(expr, expr.index)
+        transformCollectionReading(expr, expr.index)
+
+    override fun <Field, Sort : USort> transform(expr: UInputFieldReading<Field, Sort>): UExpr<Sort> =
+        transformCollectionReading(expr, expr.address)
+
+    override fun <KeySort : USort, Sort : USort, Reg : Region<Reg>> transform(
+        expr: UAllocatedMapReading<Type, KeySort, Sort, Reg>
+    ): UExpr<Sort> = transformCollectionReading(expr, expr.key)
+
+    override fun <KeySort : USort, Sort : USort, Reg : Region<Reg>> transform(
+        expr: UInputMapReading<Type, KeySort, Sort, Reg>
+    ): UExpr<Sort> = transformCollectionReading(expr, expr.address to expr.key)
+
+    override fun <Sort : USort> transform(
+        expr: UAllocatedRefMapWithInputKeysReading<Type, Sort>
+    ): UExpr<Sort> = transformCollectionReading(expr, expr.keyRef)
+
+    override fun <Sort : USort> transform(
+        expr: UInputRefMapWithAllocatedKeysReading<Type, Sort>
+    ): UExpr<Sort> = transformCollectionReading(expr, expr.mapRef)
+
+    override fun <Sort : USort> transform(
+        expr: UInputRefMapWithInputKeysReading<Type, Sort>
+    ): UExpr<Sort> = transformCollectionReading(expr, expr.mapRef to expr.keyRef)
 
-    override fun <Sort : USort> transform(expr: UInputFieldReading<Field, Sort>): UExpr<Sort> =
-        transformHeapReading(expr, expr.address)
+    override fun transform(expr: UInputMapLengthReading<Type>): USizeExpr =
+        transformCollectionReading(expr, expr.address)
 
     override fun transform(expr: UConcreteHeapRef): UExpr<UAddressSort> = expr
 
-    override fun transform(expr: UNullRef): UExpr<UAddressSort> = heapEvaluator.nullRef()
+    override fun transform(expr: UNullRef): UExpr<UAddressSort> = memory.nullRef()
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/Context.kt b/usvm-core/src/main/kotlin/org/usvm/Context.kt
@@ -12,17 +12,34 @@ import io.ksmt.utils.DefaultValueSampler
 import io.ksmt.utils.asExpr
 import io.ksmt.utils.cast
 import io.ksmt.utils.uncheckedCast
-import org.usvm.memory.UAllocatedArrayRegion
-import org.usvm.memory.UInputArrayLengthRegion
-import org.usvm.memory.UInputArrayRegion
-import org.usvm.memory.UInputFieldRegion
+import org.usvm.collection.array.UAllocatedArray
+import org.usvm.collection.array.UAllocatedArrayReading
+import org.usvm.collection.array.UInputArray
+import org.usvm.collection.array.UInputArrayReading
+import org.usvm.collection.array.length.UInputArrayLengthReading
+import org.usvm.collection.array.length.UInputArrayLengths
+import org.usvm.collection.field.UInputFieldReading
+import org.usvm.collection.field.UInputFields
+import org.usvm.collection.map.length.UInputMapLengthCollection
+import org.usvm.collection.map.length.UInputMapLengthReading
+import org.usvm.collection.map.primitive.UAllocatedMap
+import org.usvm.collection.map.primitive.UAllocatedMapReading
+import org.usvm.collection.map.primitive.UInputMap
+import org.usvm.collection.map.primitive.UInputMapReading
+import org.usvm.collection.map.ref.UAllocatedRefMapWithInputKeys
+import org.usvm.collection.map.ref.UAllocatedRefMapWithInputKeysReading
+import org.usvm.collection.map.ref.UInputRefMap
+import org.usvm.collection.map.ref.UInputRefMapWithAllocatedKeys
+import org.usvm.collection.map.ref.UInputRefMapWithAllocatedKeysReading
+import org.usvm.collection.map.ref.UInputRefMapWithInputKeysReading
 import org.usvm.memory.splitUHeapRef
 import org.usvm.solver.USolverBase
 import org.usvm.types.UTypeSystem
+import org.usvm.util.Region
 
 @Suppress("LeakingThis")
 open class UContext(
-    components: UComponents<*, *, *>,
+    components: UComponents<*>,
     operationMode: OperationMode = OperationMode.CONCURRENT,
     astManagementMode: AstManagementMode = AstManagementMode.GC,
     simplificationMode: SimplificationMode = SimplificationMode.SIMPLIFY,
@@ -41,8 +58,8 @@ open class UContext(
     }
 
     @Suppress("UNCHECKED_CAST")
-    fun <Field, Type, Method, Context : UContext> solver(): USolverBase<Field, Type, Method, Context> =
-        this.solver as USolverBase<Field, Type, Method, Context>
+    fun <Type, Context : UContext> solver(): USolverBase<Type, Context> =
+        this.solver as USolverBase<Type, Context>
 
     @Suppress("UNCHECKED_CAST")
     fun <Type> typeSystem(): UTypeSystem<Type> =
@@ -102,14 +119,14 @@ open class UContext(
 
                 concreteRefsRhs.forEach { (concreteRefRhs, guardRhs) ->
                     val guardLhs = concreteRefLhsToGuard.getOrDefault(concreteRefRhs.address, falseExpr)
-                    // mkAnd instead of mkAndNoFlat here is OK
+                    // 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 mkAndNoFlat here is OK
+                    // mkAnd instead of mkAnd with flat=false here is OK
                     val conjunct = mkAnd(symbolicRefLhs.guard, symbolicRefRhs.guard, refsEq)
                     conjuncts += conjunct
                 }
@@ -132,7 +149,7 @@ open class UContext(
     private val inputFieldReadingCache = mkAstInterner<UInputFieldReading<*, out USort>>()
 
     fun <Field, Sort : USort> mkInputFieldReading(
-        region: UInputFieldRegion<Field, Sort>,
+        region: UInputFields<Field, Sort>,
         address: UHeapRef,
     ): UInputFieldReading<Field, Sort> = inputFieldReadingCache.createIfContextActive {
         UInputFieldReading(this, region, address)
@@ -141,7 +158,7 @@ open class UContext(
     private val allocatedArrayReadingCache = mkAstInterner<UAllocatedArrayReading<*, out USort>>()
 
     fun <ArrayType, Sort : USort> mkAllocatedArrayReading(
-        region: UAllocatedArrayRegion<ArrayType, Sort>,
+        region: UAllocatedArray<ArrayType, Sort>,
         index: USizeExpr,
     ): UAllocatedArrayReading<ArrayType, Sort> = allocatedArrayReadingCache.createIfContextActive {
         UAllocatedArrayReading(this, region, index)
@@ -150,7 +167,7 @@ open class UContext(
     private val inputArrayReadingCache = mkAstInterner<UInputArrayReading<*, out USort>>()
 
     fun <ArrayType, Sort : USort> mkInputArrayReading(
-        region: UInputArrayRegion<ArrayType, Sort>,
+        region: UInputArray<ArrayType, Sort>,
         address: UHeapRef,
         index: USizeExpr,
     ): UInputArrayReading<ArrayType, Sort> = inputArrayReadingCache.createIfContextActive {
@@ -160,12 +177,77 @@ open class UContext(
     private val inputArrayLengthReadingCache = mkAstInterner<UInputArrayLengthReading<*>>()
 
     fun <ArrayType> mkInputArrayLengthReading(
-        region: UInputArrayLengthRegion<ArrayType>,
+        region: UInputArrayLengths<ArrayType>,
         address: UHeapRef,
     ): UInputArrayLengthReading<ArrayType> = inputArrayLengthReadingCache.createIfContextActive {
         UInputArrayLengthReading(this, region, address)
     }.cast()
 
+    private val allocatedSymbolicMapReadingCache = mkAstInterner<UAllocatedMapReading<*, *, *, *>>()
+
+    fun <MapType, KeySort : USort, Sort : USort, Reg : Region<Reg>> mkAllocatedMapReading(
+        region: UAllocatedMap<MapType, KeySort, Sort, Reg>,
+        key: UExpr<KeySort>
+    ): UAllocatedMapReading<MapType, KeySort, Sort, Reg> =
+        allocatedSymbolicMapReadingCache.createIfContextActive {
+            UAllocatedMapReading(this, region, key)
+        }.cast()
+
+    private val inputSymbolicMapReadingCache = mkAstInterner<UInputMapReading<*, *, *, *>>()
+
+    fun <MapType, KeySort : USort, Reg : Region<Reg>, Sort : USort> mkInputMapReading(
+        region: UInputMap<MapType, KeySort, Sort, Reg>,
+        address: UHeapRef,
+        key: UExpr<KeySort>
+    ): UInputMapReading<MapType, KeySort, Sort, Reg> =
+        inputSymbolicMapReadingCache.createIfContextActive {
+            UInputMapReading(this, region, address, key)
+        }.cast()
+
+    private val allocatedSymbolicRefMapWithInputKeysReadingCache =
+        mkAstInterner<UAllocatedRefMapWithInputKeysReading<*, *>>()
+
+    fun <MapType, Sort : USort> mkAllocatedRefMapWithInputKeysReading(
+        region: UAllocatedRefMapWithInputKeys<MapType, Sort>,
+        keyRef: UHeapRef
+    ): UAllocatedRefMapWithInputKeysReading<MapType, Sort> =
+        allocatedSymbolicRefMapWithInputKeysReadingCache.createIfContextActive {
+            UAllocatedRefMapWithInputKeysReading(this, region, keyRef)
+        }.cast()
+
+    private val inputSymbolicRefMapWithAllocatedKeysReadingCache =
+        mkAstInterner<UInputRefMapWithAllocatedKeysReading<*, *>>()
+
+    fun <MapType, Sort : USort> mkInputRefMapWithAllocatedKeysReading(
+        region: UInputRefMapWithAllocatedKeys<MapType, Sort>,
+        mapRef: UHeapRef
+    ): UInputRefMapWithAllocatedKeysReading<MapType, Sort> =
+        inputSymbolicRefMapWithAllocatedKeysReadingCache.createIfContextActive {
+            UInputRefMapWithAllocatedKeysReading(this, region, mapRef)
+        }.cast()
+
+    private val inputSymbolicRefMapWithInputKeysReadingCache =
+        mkAstInterner<UInputRefMapWithInputKeysReading<*, *>>()
+
+    fun <MapType, Sort : USort> mkInputRefMapWithInputKeysReading(
+        region: UInputRefMap<MapType, Sort>,
+        mapRef: UHeapRef,
+        keyRef: UHeapRef
+    ): UInputRefMapWithInputKeysReading<MapType, Sort> =
+        inputSymbolicRefMapWithInputKeysReadingCache.createIfContextActive {
+            UInputRefMapWithInputKeysReading(this, region, mapRef, keyRef)
+        }.cast()
+
+    private val inputSymbolicMapLengthReadingCache = mkAstInterner<UInputMapLengthReading<*>>()
+
+    fun <MapType> mkInputMapLengthReading(
+        region: UInputMapLengthCollection<MapType>,
+        address: UHeapRef
+    ): UInputMapLengthReading<MapType> =
+        inputSymbolicMapLengthReadingCache.createIfContextActive {
+            UInputMapLengthReading<MapType>(this, region, address)
+        }.cast()
+
     private val indexedMethodReturnValueCache = mkAstInterner<UIndexedMethodReturnValue<Any, out USort>>()
 
     fun <Method, Sort : USort> mkIndexedMethodReturnValue(
@@ -200,8 +282,8 @@ open class UContext(
     // Type hack to be able to intern the initial location for inheritors.
     private val initialLocation = RootNode<Nothing, Nothing>()
 
-    fun <State : UState<*, *, *, Statement, *, State>, Statement> mkInitialLocation()
-        : PathsTrieNode<State, Statement> = initialLocation.uncheckedCast()
+    fun <State : UState<*, *, Statement, *, State>, Statement> mkInitialLocation()
+            : PathsTrieNode<State, Statement> = initialLocation.uncheckedCast()
 
     fun mkUValueSampler(): KSortVisitor<KExpr<*>> {
         return UValueSampler(this)
@@ -217,6 +299,17 @@ open class UContext(
                 super.visit(sort)
             }
     }
+
+    inline fun <T : KSort> mkIte(
+        condition: KExpr<KBoolSort>,
+        trueBranch: () -> KExpr<T>,
+        falseBranch: () -> KExpr<T>
+    ): KExpr<T> =
+        when (condition) {
+            is UTrue -> trueBranch()
+            is UFalse -> falseBranch()
+            else -> mkIte(condition, trueBranch(), falseBranch())
+        }
 }