Add comments

UnitTestBot · Aug 31, 2023 · 0474f7b · 0474f7b
1 parent 0632cdc
commit 0474f7b
Show file tree

Hide file tree

Showing 4 changed files with 44 additions and 44 deletions.
diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt b/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt
@@ -14,6 +14,8 @@ import org.usvm.util.emptyRegionTree
  */
 interface USymbolicCollectionUpdates<Key, Sort : USort> : Sequence<UUpdateNode<Key, Sort>> {
     /**
+     * Reads from collection updates and composes relevant ones. May filter out irrelevant updates for the [key].
+     *
      * @return Relevant updates for a given key.
      */
     fun read(key: Key, composer: UComposer<*>?): USymbolicCollectionUpdates<Key, Sort>
@@ -236,7 +238,7 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
 ) : USymbolicCollectionUpdates<Key, Sort> {
     override fun read(key: Key, composer: UComposer<*>?): USymbolicCollectionUpdates<Key, Sort> {
         val reg = keyInfo.keyToRegion(key)
-        val updates = updates.localize(reg) { it.includesSymbolically(key, composer).isFalse }
+        val updates = updates.localize(reg) { !it.includesSymbolically(key, composer).isFalse }
         if (updates === this.updates) {
             return this
         }
@@ -253,9 +255,8 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
         val reg = keyInfo.keyToRegion(key)
         val newUpdates = updates.write(
             reg,
-            update,
-            valueFilter = { it.isIncludedByUpdateConcretely(update) }
-        )
+            update
+        ) { !it.isIncludedByUpdateConcretely(update) }
 
         return this.copy(updates = newUpdates)
     }
@@ -268,9 +269,8 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
         val update = URangedUpdateNode(fromCollection, adapter, guard)
         val newUpdates = updates.write(
             adapter.region(),
-            update,
-            valueFilter = { it.isIncludedByUpdateConcretely(update) }
-        )
+            update
+        ) { !it.isIncludedByUpdateConcretely(update) }
 
         return this.copy(updates = newUpdates)
     }
@@ -291,8 +291,8 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
                 is UPinpointUpdateNode<Key, Sort> -> keyInfo.keyToRegion(update.key)
                 is URangedUpdateNode<*, *, Key, Sort> -> update.adapter.region()
             }
-            splitRegionTree =
-                splitRegionTree.write(region, update, valueFilter = { it.isIncludedByUpdateConcretely(update) })
+            splitRegionTree = splitRegionTree
+                .write(region, update) { !it.isIncludedByUpdateConcretely(update) }
         }
 
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt
@@ -47,6 +47,9 @@ data class USymbolicCollection<out CollectionId : USymbolicCollectionId<Key, Sor
         return collectionId.instantiate(localizedRegion, key, composer)
     }
 
+    /**
+     * Reads a [key] from this collection with on-the-fly composition, if the [composer] provided.
+     */
     fun read(key: Key, composer: UComposer<*>?): UExpr<Sort> {
         if (sort == sort.uctx.addressSort) {
             // Here we split concrete heap addresses from symbolic ones to optimize further memory operations.
@@ -147,6 +150,10 @@ data class USymbolicCollection<out CollectionId : USymbolicCollectionId<Key, Sor
         }
     }
 
+    /**
+     * Applies this collection to the [memory], with applying composition via [composer] to the updates. May filter out
+     * updates, which are irrelevant for the [key] reading.
+     */
     fun <Type> applyTo(memory: UWritableMemory<Type>, key: Key, composer: UComposer<*>) {
         // Apply each update on the copy
         for (update in updates) {

diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt b/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt
@@ -213,6 +213,9 @@ class URangedUpdateNode<CollectionId : USymbolicCollectionId<SrcKey, Sort, Colle
     // Ignores update
     override fun hashCode(): Int = adapter.hashCode() * 31 + guard.hashCode()
 
+    /**
+     * Applies this update node to the [memory] with applying composition via [composer].
+     */
     fun applyTo(
         memory: UWritableMemory<*>,
         dstCollectionId: USymbolicCollectionId<DstKey, *, *>,

diff --git a/usvm-util/src/main/kotlin/org/usvm/util/RegionTree.kt b/usvm-util/src/main/kotlin/org/usvm/util/RegionTree.kt
@@ -25,19 +25,15 @@ class RegionTree<Reg, Value>(
     /**
      * Splits the region tree into two trees: completely covered by the [region] and disjoint with it.
      *
-     * [valueFilter] is an arbitrary predicate suitable to filter out values from the results of the function.
+     * [filterPredicate] is a predicate suitable to filter out particular nodes if their `value` don't satisfy it.
      * Examples:
-     * * `{ it != 10 }` removes nodes with `value` equal to 10
-     * * `{ false }` doesn't remove anything
-     *
-     * **NB**: it doesn't filter out all the values satisfying [valueFilter], only those, that were touched during
-     * recursive split.
-     *
+     * * `{ true }` doesn't filter anything
+     * * `{ it != value }` writes into a tree and restrict for it to contain non-unique values.
      * @see localize
      */
     private fun splitRecursively(
         region: Reg,
-        valueFilter: (Value) -> Boolean,
+        filterPredicate: (Value) -> Boolean,
     ): RecursiveSplitResult {
         if (isEmpty) {
             return RecursiveSplitResult(completelyCoveredRegionTree = this, disjointRegionTree = this)
@@ -51,15 +47,16 @@ class RegionTree<Reg, Value>(
             val value = entry.first
             // IMPORTANT: usage of linked versions of maps is mandatory here, since
             // it is required for correct order of values returned by `iterator.next()` method
-            val completelyCoveredRegionTree = if (!valueFilter(value)) {
+            val completelyCoveredRegionTree = if (filterPredicate(value)) {
                 val inside = persistentMapOf(region to entry)
                 if (entries.size == 1) {
                     this
                 } else {
                     RegionTree(inside)
                 }
             } else {
-                entry.second.splitRecursively(region, valueFilter).completelyCoveredRegionTree
+                // fixme: here we might have a deep recursion, maybe we should rewrite it
+                entry.second.splitRecursively(region, filterPredicate).completelyCoveredRegionTree
             }
             val outside = entries.remove(region)
             val disjointRegionTree = RegionTree(outside)
@@ -86,31 +83,31 @@ class RegionTree<Reg, Value>(
         fun MutableMap<Reg, Pair<Value, RegionTree<Reg, Value>>>.addWithFilter(
             nodeRegion: Reg,
             valueWithRegionTree: Pair<Value, RegionTree<Reg, Value>>,
-            valueFilter: (Value) -> Boolean,
+            filterPredicate: (Value) -> Boolean,
         ) {
             val (value, childRegionTree) = valueWithRegionTree
-            if (valueFilter(value)) {
-                putAll(childRegionTree.entries)
-            } else {
+            if (filterPredicate(value)) {
                 put(nodeRegion, valueWithRegionTree)
+            } else {
+                putAll(childRegionTree.entries)
             }
         }
 
         entries.entries.forEach { (nodeRegion, valueWithRegionTree) ->
             when (region.compare(nodeRegion)) {
-                RegionComparisonResult.INCLUDES -> included.addWithFilter(nodeRegion, valueWithRegionTree, valueFilter)
+                RegionComparisonResult.INCLUDES -> included.addWithFilter(nodeRegion, valueWithRegionTree, filterPredicate)
 
-                RegionComparisonResult.DISJOINT -> disjoint.addWithFilter(nodeRegion, valueWithRegionTree, valueFilter)
+                RegionComparisonResult.DISJOINT -> disjoint.addWithFilter(nodeRegion, valueWithRegionTree, filterPredicate)
                 // For nodes with intersection, repeat process recursively.
                 RegionComparisonResult.INTERSECTS -> {
                     val (value, childRegionTree) = valueWithRegionTree
-                    val (splitIncluded, splitDisjoint) = childRegionTree.splitRecursively(region, valueFilter)
+                    val (splitIncluded, splitDisjoint) = childRegionTree.splitRecursively(region, filterPredicate)
 
                     val includedReg = nodeRegion.intersect(region)
                     val disjointReg = nodeRegion.subtract(region)
 
-                    included.addWithFilter(includedReg, value to splitIncluded, valueFilter)
-                    disjoint.addWithFilter(disjointReg, value to splitDisjoint, valueFilter)
+                    included.addWithFilter(includedReg, value to splitIncluded, filterPredicate)
+                    disjoint.addWithFilter(disjointReg, value to splitDisjoint, filterPredicate)
                 }
             }
         }
@@ -126,45 +123,38 @@ class RegionTree<Reg, Value>(
     /**
      * Returns a subtree completely included into the [region].
      *
-     * [valueFilter] is a predicate suitable to filter out particular nodes if their `value` satisfies it.
+     * [filterPredicate] is a predicate suitable to filter out particular nodes if their `value` don't satisfy it.
      * Examples:
-     * * `{ false }` doesn't filter anything
+     * * `{ true }` doesn't filter anything
      * * `{ it != value }` writes into a tree and restrict for it to contain non-unique values.
      *   Suitable for deduplication.
      *
-     * **NB**: it doesn't filter out all the values satisfying [valueFilter], only those, that were touched during
-     * recursive split. Consider this example:
-     * ```
      * r := some region
      * tree := {r -> 1}
      *             {r -> 2}
      *                 {r -> 3}
      * tree.localize(r) { it % 2 == 1) =
      *     // first will be filtered out
      *         {r -> 2}
-     *             {r -> 3} // this one won't be filtered out, though it satisfies `valueFilter`
+     *            // third will be filtered out
      *
      * ```
      */
-    fun localize(region: Reg, valueFilter: (Value) -> Boolean = { false }): RegionTree<Reg, Value> =
-        splitRecursively(region, valueFilter).completelyCoveredRegionTree
+    fun localize(region: Reg, filterPredicate: (Value) -> Boolean = { true }): RegionTree<Reg, Value> =
+        splitRecursively(region, filterPredicate).completelyCoveredRegionTree
 
     /**
      * Places a Pair([region], [value]) into the tree, preserving its invariants.
      *
-     * [valueFilter] is a predicate suitable to filter out particular nodes if their `value` satisfies it.
+     * [filterPredicate] is a predicate suitable to filter out particular nodes if their `value` don't satisfy it.
      * Examples:
-     * * `{ false }` doesn't filter anything
+     * * `{ true }` doesn't filter anything
      * * `{ it != value }` writes into a tree and restrict for it to contain non-unique values.
      *   Suitable for deduplication.
-     *
-     * **NB**: it doesn't filter out all the values satisfying [valueFilter], only those, that were touched during
-     * recursive split.
-     *
      * @see localize
      */
-    fun write(region: Reg, value: Value, valueFilter: (Value) -> Boolean = { false }): RegionTree<Reg, Value> {
-        val (included, disjoint) = splitRecursively(region, valueFilter)
+    fun write(region: Reg, value: Value, filterPredicate: (Value) -> Boolean = { true }): RegionTree<Reg, Value> {
+        val (included, disjoint) = splitRecursively(region, filterPredicate)
         // A new node for a tree we construct accordingly to the (2) invariant.
         val node = value to included