Skip to content

Commit 97601ef

Browse files
sergeypospelovsergeypospelov
authored
Region tree renaming and fix (#26)
1 parent 2dc6fc0 commit 97601ef

File tree

9 files changed

+225
-95
lines changed

9 files changed

+225
-95
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -333,6 +333,6 @@ class UIsExpr<Type> internal constructor(
333333
//region Utils
334334

335335
val UBoolExpr.isFalse get() = this === ctx.falseExpr
336-
val UBoolExpr.isTrue get() = !isFalse
336+
val UBoolExpr.isTrue get() = this === ctx.trueExpr
337337

338338
//endregion

‎usvm-core/src/main/kotlin/org/usvm/memory/MemoryRegions.kt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -366,7 +366,7 @@ fun <ArrayType, Sort : USort> initializedAllocatedArrayRegion(
366366
content: Map<USizeExpr, UExpr<Sort>>,
367367
guard: UBoolExpr
368368
): UAllocatedArrayRegion<ArrayType, Sort> {
369-
val emptyRegionTree = emptyRegionTree<UUpdateNode<USizeExpr, Sort>, UArrayIndexRegion>()
369+
val emptyRegionTree = emptyRegionTree<UArrayIndexRegion, UUpdateNode<USizeExpr, Sort>>()
370370

371371
val entries = content.entries.associate { (key, value) ->
372372
val region = indexRegion(key)

‎usvm-core/src/main/kotlin/org/usvm/memory/MemoryUpdates.kt

Lines changed: 22 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ interface UMemoryUpdates<Key, Sort : USort> : Sequence<UUpdateNode<Key, Sort>> {
7777

7878
/**
7979
* Accepts the [visitor]. Implementations should call [UMemoryUpdatesVisitor.visitInitialValue] firstly, then call
80-
* [UMemoryUpdatesVisitor.visitUpdateNode] in the chronological order
80+
* [UMemoryUpdatesVisitor.visitUpdate] in the chronological order
8181
* (from the oldest to the newest) with accumulated [Result].
8282
*
8383
* Uses [lookupCache] to shortcut the traversal. The actual key is determined by the
@@ -183,6 +183,11 @@ class UFlatUpdates<Key, Sort : USort> private constructor(
183183
val mappedNode = node.update.map(keyMapper, composer)
184184
val mappedNext = node.next.map(keyMapper, composer)
185185

186+
// Doesn't apply the node, if its guard maps to `false`
187+
if (mappedNode.guard.isFalse) {
188+
return mappedNext
189+
}
190+
186191
// If nothing changed, return this updates
187192
if (mappedNode === node.update && mappedNext === node.next) {
188193
return this
@@ -250,7 +255,7 @@ class UFlatUpdates<Key, Sort : USort> private constructor(
250255
//region Tree memory updates
251256

252257
data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
253-
private val updates: RegionTree<UUpdateNode<Key, Sort>, Reg>,
258+
private val updates: RegionTree<Reg, UUpdateNode<Key, Sort>>,
254259
private val keyToRegion: (Key) -> Reg,
255260
private val keyRangeToRegion: (Key, Key) -> Reg,
256261
private val symbolicEq: (Key, Key) -> UBoolExpr,
@@ -259,7 +264,7 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
259264
) : UMemoryUpdates<Key, Sort> {
260265
override fun read(key: Key): UTreeUpdates<Key, Reg, Sort> {
261266
val reg = keyToRegion(key)
262-
val updates = updates.localize(reg)
267+
val updates = updates.localize(reg) { it.includesSymbolically(key).isFalse }
263268
if (updates === this.updates) {
264269
return this
265270
}
@@ -272,7 +277,7 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
272277
val newUpdates = updates.write(
273278
keyToRegion(key),
274279
update,
275-
keyFilter = { it.isIncludedByUpdateConcretely(update) }
280+
valueFilter = { it.isIncludedByUpdateConcretely(update) }
276281
)
277282

278283
return this.copy(updates = newUpdates)
@@ -290,7 +295,7 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
290295
val newUpdates = updates.write(
291296
region,
292297
update,
293-
keyFilter = { it.isIncludedByUpdateConcretely(update) }
298+
valueFilter = { it.isIncludedByUpdateConcretely(update) }
294299
)
295300

296301
return this.copy(updates = newUpdates)
@@ -306,15 +311,15 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
306311
val updatesSuffix = mutableListOf<UUpdateNode<Key, Sort>?>()
307312

308313
// reconstructed region tree, including all updates unsatisfying `predicate(update.value(key))` in the same order
309-
var splitUpdates = emptyRegionTree<UUpdateNode<Key, Sort>, Reg>()
314+
var splitUpdates = emptyRegionTree<Reg, UUpdateNode<Key, Sort>>()
310315

311316
// add an update to result tree
312317
fun applyUpdate(update: UUpdateNode<Key, Sort>) {
313318
val region = when (update) {
314319
is UPinpointUpdateNode<Key, Sort> -> keyToRegion(update.key)
315320
is URangedUpdateNode<*, *, Key, Sort> -> keyRangeToRegion(update.fromKey, update.toKey)
316321
}
317-
splitUpdates = splitUpdates.write(region, update, keyFilter = { it.isIncludedByUpdateConcretely(update) })
322+
splitUpdates = splitUpdates.write(region, update, valueFilter = { it.isIncludedByUpdateConcretely(update) })
318323
}
319324

320325
// traverse all updates one by one from the oldest one
@@ -366,31 +371,35 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
366371
var mappedNodeFound = false
367372

368373
// Traverse [updates] using its iterator and fold them into a new updates tree with new mapped nodes
369-
val initialEmptyTree = emptyRegionTree<UUpdateNode<Key, Sort>, Reg>()
374+
val initialEmptyTree = emptyRegionTree<Reg, UUpdateNode<Key, Sort>>()
370375
val mappedUpdates = updates.fold(initialEmptyTree) { mappedUpdatesTree, updateNodeWithRegion ->
371376
val (updateNode, oldRegion) = updateNodeWithRegion
372377
// Map current node
373378
val mappedUpdateNode = updateNode.map(keyMapper, composer)
374379

380+
375381
// Save information about whether something changed in the current node or not
376382
if (mappedUpdateNode !== updateNode) {
377383
mappedNodeFound = true
378384
}
379385

386+
// Doesn't apply the node, if its guard maps to `false`
387+
if (mappedUpdateNode.guard.isFalse) {
388+
return@fold mappedUpdatesTree
389+
}
390+
380391
// Note that following code should be executed after checking for reference equality of a mapped node.
381392
// Otherwise, it is possible that for a tree with several impossible writes
382393
// it will be returned as a result, instead of an empty one.
383394

384395
// Extract a new region by the mapped node
385-
val newRegion = when (updateNode) {
396+
val newRegion = when (mappedUpdateNode) {
386397
is UPinpointUpdateNode -> {
387-
mappedUpdateNode as UPinpointUpdateNode
388398
val currentRegion = keyToRegion(mappedUpdateNode.key)
389399
oldRegion.intersect(currentRegion)
390400
}
391401

392402
is URangedUpdateNode<*, *, Key, Sort> -> {
393-
mappedUpdateNode as URangedUpdateNode<*, *, Key, Sort>
394403
val currentRegion = keyRangeToRegion(mappedUpdateNode.fromKey, mappedUpdateNode.toKey)
395404
oldRegion.intersect(currentRegion)
396405
}
@@ -512,7 +521,7 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
512521
* *
513522
*```
514523
*/
515-
private fun leftMostFold(updates: RegionTree<UUpdateNode<Key, Sort>, *>): Result {
524+
private fun leftMostFold(updates: RegionTree<*, UUpdateNode<Key, Sort>>): Result {
516525
var result = cache[updates]
517526

518527
if (result != null) {
@@ -531,7 +540,7 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
531540

532541
private fun notLeftMostFold(
533542
accumulator: Result,
534-
iterator: Iterator<Map.Entry<Region<*>, Pair<UUpdateNode<Key, Sort>, RegionTree<UUpdateNode<Key, Sort>, *>>>>,
543+
iterator: Iterator<Map.Entry<Region<*>, Pair<UUpdateNode<Key, Sort>, RegionTree<*, UUpdateNode<Key, Sort>>>>>,
535544
): Result {
536545
var accumulated = accumulator
537546
while (iterator.hasNext()) {

‎usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -315,11 +315,11 @@ internal class CompositionTest {
315315

316316
@Test
317317
fun testComposeSeveralTimes() = with(ctx) {
318-
val fstAddress = mockk<USymbolicHeapRef>()
319-
val fstIndex = mockk<USizeExpr>()
318+
val fstAddress = mkRegisterReading(0, addressSort)
319+
val fstIndex = mkRegisterReading(1, sizeSort)
320320

321-
val sndAddress = mockk<USymbolicHeapRef>()
322-
val sndIndex = mockk<USizeExpr>()
321+
val sndAddress = mkRegisterReading(2, addressSort)
322+
val sndIndex = mkRegisterReading(3, sizeSort)
323323

324324
val arrayType: KClass<Array<*>> = Array::class
325325
// Create an empty region

‎usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTests.kt

Lines changed: 26 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,10 @@ package org.usvm.memory
33
import io.ksmt.utils.mkConst
44
import io.mockk.every
55
import io.mockk.mockk
6+
import org.junit.jupiter.api.Assertions.assertEquals
67
import org.junit.jupiter.api.BeforeEach
78
import org.junit.jupiter.api.Test
9+
import org.usvm.Type
810
import org.usvm.UBv32Sort
911
import org.usvm.UComponents
1012
import org.usvm.UContext
@@ -71,14 +73,36 @@ class MemoryRegionTests {
7173
).write(address, 1.toBv(), guard)
7274
.write(address, 2.toBv(), anotherGuard)
7375

74-
assertTrue(treeUpdates.toList().size == 2)
76+
assertEquals(2, treeUpdates.toList().size)
7577

7678
val anotherTreeUpdates = treeUpdates
7779
.write(address, 3.toBv(), anotherGuard)
7880
.write(address, 4.toBv(), guard)
7981

80-
assertTrue(anotherTreeUpdates.toList().size == 2)
82+
assertEquals(3, anotherTreeUpdates.toList().size)
8183
}
8284
}
8385

86+
@Test
87+
fun testKeyFiltering() = with(ctx) {
88+
val idx1 = mkRegisterReading(0, sizeSort)
89+
val idx2 = mkRegisterReading(1, sizeSort)
90+
91+
val memoryRegion = emptyAllocatedArrayRegion(mockk<Type>(), 0, sizeSort)
92+
.write(idx1, mkBv(0), trueExpr)
93+
.write(idx2, mkBv(1), trueExpr)
94+
95+
val updatesBefore = memoryRegion.updates.toList()
96+
assertEquals(2, updatesBefore.size)
97+
assertTrue(updatesBefore.first().includesConcretely(idx1, trueExpr))
98+
assertTrue(updatesBefore.last().includesConcretely(idx2, trueExpr))
99+
100+
val memoryRegionAfter = memoryRegion.write(idx2, mkBv(2), trueExpr)
101+
102+
val updatesAfter = memoryRegionAfter.updates.toList()
103+
assertEquals(2, updatesAfter.size)
104+
assertTrue(updatesAfter.first().includesConcretely(idx1, trueExpr))
105+
assertTrue(updatesAfter.last().includesConcretely(idx2, trueExpr))
106+
}
107+
84108
}

‎usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ package org.usvm.model
33
import io.mockk.every
44
import io.mockk.mockk
55
import kotlinx.collections.immutable.persistentMapOf
6+
import org.junit.jupiter.api.Assertions.assertEquals
67
import org.junit.jupiter.api.BeforeEach
78
import org.junit.jupiter.api.Test
89
import org.usvm.*
@@ -169,4 +170,49 @@ class ModelCompositionTest {
169170
val expr = composer.compose(reading)
170171
assertSame(composedRef0, expr)
171172
}
173+
174+
@Test
175+
fun testComposeAllocatedArrayWithFalseOverwrite() = with(ctx) {
176+
val heapEvaluator = UHeapEagerModel<Field, Type>(
177+
concreteNull,
178+
mapOf(),
179+
mapOf(),
180+
mapOf(),
181+
)
182+
183+
val index0 = 0.toBv()
184+
val index1 = 1.toBv()
185+
186+
val defaultValue = bv32Sort.sampleUValue()
187+
val nonDefaultValue0 = 17.toBv()
188+
val nonDefaultValue1 = 42.toBv()
189+
190+
val stackModel = URegistersStackEagerModel(concreteNull, mapOf(0 to trueExpr, 1 to falseExpr))
191+
val trueGuard = mkRegisterReading(0, boolSort)
192+
val falseGuard = mkRegisterReading(1, boolSort)
193+
194+
val composer = UComposer(this, stackModel, heapEvaluator, mockk(), mockk())
195+
196+
val emptyRegion = emptyAllocatedArrayRegion<Type, UBv32Sort>(mockk(), 1, bv32Sort)
197+
198+
run {
199+
val region = emptyRegion
200+
.write(index0, nonDefaultValue0, trueGuard)
201+
.write(index0, nonDefaultValue1, falseGuard)
202+
val reading = region.read(index0)
203+
204+
val expr = composer.compose(reading)
205+
assertEquals(nonDefaultValue0, expr)
206+
}
207+
208+
run {
209+
val region = emptyRegion
210+
.write(index1, nonDefaultValue0, trueGuard)
211+
.write(index0, nonDefaultValue1, falseGuard)
212+
val reading = region.read(index0)
213+
214+
val expr = composer.compose(reading)
215+
assertEquals(defaultValue, expr)
216+
}
217+
}
172218
}

0 commit comments

Comments
 (0)