Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit be28b95

Browse files
committedMar 16, 2023
Review fixes
1 parent 7ff8aa1 commit be28b95

File tree

5 files changed

+212
-223
lines changed

5 files changed

+212
-223
lines changed
 

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

Lines changed: 1 addition & 215 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
package org.usvm
22

3-
import org.ksmt.utils.asExpr
43
import org.usvm.util.SetRegion
54
import org.usvm.util.emptyRegionTree
65
import java.util.*
@@ -172,7 +171,7 @@ data class UMemoryRegion<RegionId : URegionId<Key>, Key, Sort : USort>(
172171
keyConverter: UMemoryKeyConverter<SrcKey, Key>,
173172
guard: UBoolExpr
174173
): UMemoryRegion<RegionId, Key, Sort> {
175-
val updatesCopy = updates.copy(fromRegion, fromKey, toKey, keyConverter, guard)
174+
val updatesCopy = updates.copyRange(fromRegion, fromKey, toKey, keyConverter, guard)
176175
return UMemoryRegion(regionId, sort, updatesCopy, defaultValue, instantiator)
177176
}
178177
}
@@ -244,219 +243,6 @@ fun refIndexRangeRegion(
244243
idx2: USymbolicArrayIndex
245244
): UArrayIndexRegion = indexRangeRegion(idx1.second, idx2.second)
246245

247-
/**
248-
* An interface that represents any possible type of regions that can be used in the memory.
249-
*/
250-
interface URegionId<Key> {
251-
fun <Field, ArrayType, Sort : USort> read(
252-
key: Key,
253-
sort: Sort,
254-
heap: UReadOnlySymbolicHeap<Field, ArrayType>
255-
): UExpr<Sort>
256-
257-
fun <Field, ArrayType, Sort : USort> write(
258-
key: Key,
259-
sort: Sort,
260-
heap: USymbolicHeap<Field, ArrayType>,
261-
value: UExpr<Sort>,
262-
guard: UBoolExpr
263-
)
264-
265-
fun <Field, ArrayType, SrcKey, Sort : USort> copy(
266-
from: Key,
267-
to: Key,
268-
sort: Sort,
269-
heap: USymbolicHeap<Field, ArrayType>,
270-
converter: UMemoryKeyConverter<Key, SrcKey>,
271-
guard: UBoolExpr
272-
)
273-
274-
fun <Field, ArrayType> keyMapper(composer: UComposer<Field, ArrayType>): KeyMapper<Key>
275-
}
276-
277-
/**
278-
* A region id for a region storing the specific [field].
279-
*/
280-
data class UInputFieldRegionId<Field> internal constructor(
281-
val field: Field
282-
) : URegionId<UHeapRef> {
283-
@Suppress("UNCHECKED_CAST")
284-
override fun <Field, ArrayType, Sort : USort> read(
285-
key: UHeapRef,
286-
sort: Sort,
287-
heap: UReadOnlySymbolicHeap<Field, ArrayType>
288-
) = heap.readField(key, field as Field, sort).asExpr(sort)
289-
290-
@Suppress("UNCHECKED_CAST")
291-
override fun <Field, ArrayType, Sort : USort> write(
292-
key: UHeapRef,
293-
sort: Sort,
294-
heap: USymbolicHeap<Field, ArrayType>,
295-
value: UExpr<Sort>,
296-
guard: UBoolExpr
297-
) = heap.writeField(key, field as Field, sort, value, guard)
298-
299-
override fun <Field, ArrayType, SrcKey, Sort : USort> copy(
300-
from: UHeapRef,
301-
to: UHeapRef,
302-
sort: Sort,
303-
heap: USymbolicHeap<Field, ArrayType>,
304-
converter: UMemoryKeyConverter<UHeapRef, SrcKey>,
305-
guard: UBoolExpr
306-
) = error("Fields region copying should never happen")
307-
308-
override fun <Field, ArrayType> keyMapper(
309-
composer: UComposer<Field, ArrayType>
310-
): KeyMapper<UHeapRef> = { composer.compose(it) }
311-
}
312-
313-
interface UArrayId<ArrayType, Key> : URegionId<Key> {
314-
val arrayType: ArrayType
315-
}
316-
317-
/**
318-
* A region id for a region storing arrays allocated during execution.
319-
* Each identifier contains information about its [arrayType] and [address].
320-
*/
321-
data class UAllocatedArrayId<ArrayType> internal constructor(
322-
override val arrayType: ArrayType,
323-
val address: UConcreteHeapAddress,
324-
) : UArrayId<ArrayType, USizeExpr> {
325-
@Suppress("UNCHECKED_CAST")
326-
override fun <Field, ArrayType, Sort : USort> read(
327-
key: USizeExpr,
328-
sort: Sort,
329-
heap: UReadOnlySymbolicHeap<Field, ArrayType>
330-
): UExpr<Sort> {
331-
val ref = key.uctx.mkConcreteHeapRef(address)
332-
return heap.readArrayIndex(ref, key, arrayType as ArrayType, sort).asExpr(sort)
333-
}
334-
335-
@Suppress("UNCHECKED_CAST")
336-
override fun <Field, ArrayType, Sort : USort> write(
337-
key: USizeExpr,
338-
sort: Sort,
339-
heap: USymbolicHeap<Field, ArrayType>,
340-
value: UExpr<Sort>,
341-
guard: UBoolExpr
342-
) {
343-
val ref = key.uctx.mkConcreteHeapRef(address)
344-
heap.writeArrayIndex(ref, key, arrayType as ArrayType, sort, value, guard)
345-
}
346-
347-
override fun <Field, ArrayType, SrcKey, Sort : USort> copy(
348-
from: USizeExpr,
349-
to: USizeExpr,
350-
sort: Sort,
351-
heap: USymbolicHeap<Field, ArrayType>,
352-
converter: UMemoryKeyConverter<USizeExpr, SrcKey>,
353-
guard: UBoolExpr
354-
) {
355-
TODO("Not yet implemented")
356-
}
357-
358-
override fun <Field, ArrayType> keyMapper(
359-
composer: UComposer<Field, ArrayType>
360-
): KeyMapper<USizeExpr> = { composer.compose(it) }
361-
362-
// we don't include arrayType into hashcode and equals, because [address] already defines unambiguously
363-
override fun equals(other: Any?): Boolean {
364-
if (this === other) return true
365-
if (javaClass != other?.javaClass) return false
366-
367-
other as UAllocatedArrayId<*>
368-
369-
if (address != other.address) return false
370-
371-
return true
372-
}
373-
374-
override fun hashCode(): Int {
375-
return address
376-
}
377-
}
378-
379-
/**
380-
* A region id for a region storing arrays retrieved as a symbolic value, contains only its [arrayType].
381-
*/
382-
data class UInputArrayId<ArrayType> internal constructor(
383-
override val arrayType: ArrayType
384-
) : UArrayId<ArrayType, USymbolicArrayIndex> {
385-
@Suppress("UNCHECKED_CAST")
386-
override fun <Field, ArrayType, Sort : USort> read(
387-
key: USymbolicArrayIndex,
388-
sort: Sort,
389-
heap: UReadOnlySymbolicHeap<Field, ArrayType>
390-
): UExpr<Sort> = heap.readArrayIndex(key.first, key.second, arrayType as ArrayType, sort).asExpr(sort)
391-
392-
@Suppress("UNCHECKED_CAST")
393-
override fun <Field, ArrayType, Sort : USort> write(
394-
key: USymbolicArrayIndex,
395-
sort: Sort,
396-
heap: USymbolicHeap<Field, ArrayType>,
397-
value: UExpr<Sort>,
398-
guard: UBoolExpr
399-
) = heap.writeArrayIndex(key.first, key.second, arrayType as ArrayType, sort, value, guard)
400-
401-
override fun <Field, ArrayType, SrcKey, Sort : USort> copy(
402-
from: USymbolicArrayIndex,
403-
to: USymbolicArrayIndex,
404-
sort: Sort,
405-
heap: USymbolicHeap<Field, ArrayType>,
406-
converter: UMemoryKeyConverter<USymbolicArrayIndex, SrcKey>,
407-
guard: UBoolExpr
408-
) {
409-
TODO("Not yet implemented")
410-
}
411-
412-
override fun <Field, ArrayType> keyMapper(
413-
composer: UComposer<Field, ArrayType>
414-
): KeyMapper<USymbolicArrayIndex> = {
415-
val ref = composer.compose(it.first)
416-
val idx = composer.compose(it.second)
417-
if (ref === it.first && idx === it.second) it else ref to idx
418-
}
419-
}
420-
421-
/**
422-
* A region id for a region storing array lengths for arrays of a specific [arrayType].
423-
*/
424-
data class UInputArrayLengthId<ArrayType> internal constructor(
425-
val arrayType: ArrayType
426-
) : URegionId<UHeapRef> {
427-
@Suppress("UNCHECKED_CAST")
428-
override fun <Field, ArrayType, Sort : USort> read(
429-
key: UHeapRef,
430-
sort: Sort,
431-
heap: UReadOnlySymbolicHeap<Field, ArrayType>
432-
): UExpr<Sort> = heap.readArrayLength(key, arrayType as ArrayType).asExpr(sort)
433-
434-
@Suppress("UNCHECKED_CAST")
435-
override fun <Field, ArrayType, Sort : USort> write(
436-
key: UHeapRef,
437-
sort: Sort,
438-
heap: USymbolicHeap<Field, ArrayType>,
439-
value: UExpr<Sort>,
440-
guard: UBoolExpr
441-
) {
442-
assert(guard.isTrue)
443-
heap.writeArrayLength(key, value.asExpr(key.uctx.sizeSort), arrayType as ArrayType)
444-
}
445-
446-
override fun <Field, ArrayType, SrcKey, Sort : USort> copy(
447-
from: UHeapRef,
448-
to: UHeapRef,
449-
sort: Sort,
450-
heap: USymbolicHeap<Field, ArrayType>,
451-
converter: UMemoryKeyConverter<UHeapRef, SrcKey>,
452-
guard: UBoolExpr
453-
) = error("Lengths region copying should never happen")
454-
455-
override fun <Field, ArrayType> keyMapper(
456-
composer: UComposer<Field, ArrayType>
457-
): KeyMapper<UHeapRef> = { composer.compose(it) }
458-
}
459-
460246
typealias UInputFieldMemoryRegion<Field, Sort> = UMemoryRegion<UInputFieldRegionId<Field>, UHeapRef, Sort>
461247
typealias UAllocatedArrayMemoryRegion<ArrayType, Sort> = UMemoryRegion<UAllocatedArrayId<ArrayType>, USizeExpr, Sort>
462248
typealias UInputArrayMemoryRegion<ArrayType, Sort> = UMemoryRegion<UInputArrayId<ArrayType>, USymbolicArrayIndex, Sort>

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ interface UMemoryUpdates<Key, Sort : USort> : Sequence<UUpdateNode<Key, Sort>> {
3939
/**
4040
* @return Updates expressing copying the slice of [fromRegion] (see UMemoryRegion.copy)
4141
*/
42-
fun <ArrayType, RegionId : UArrayId<ArrayType, SrcKey>, SrcKey> copy(
42+
fun <ArrayType, RegionId : UArrayId<ArrayType, SrcKey>, SrcKey> copyRange(
4343
fromRegion: UMemoryRegion<RegionId, SrcKey, Sort>,
4444
fromKey: Key,
4545
toKey: Key,
@@ -80,7 +80,7 @@ class UEmptyUpdates<Key, Sort : USort>(
8080
symbolicCmp
8181
)
8282

83-
override fun <ArrayType, RegionId : UArrayId<ArrayType, SrcKey>, SrcKey> copy(
83+
override fun <ArrayType, RegionId : UArrayId<ArrayType, SrcKey>, SrcKey> copyRange(
8484
fromRegion: UMemoryRegion<RegionId, SrcKey, Sort>,
8585
fromKey: Key,
8686
toKey: Key,
@@ -136,7 +136,7 @@ data class UFlatUpdates<Key, Sort : USort>(
136136
symbolicCmp
137137
)
138138

139-
override fun <ArrayType, RegionId : UArrayId<ArrayType, SrcKey>, SrcKey> copy(
139+
override fun <ArrayType, RegionId : UArrayId<ArrayType, SrcKey>, SrcKey> copyRange(
140140
fromRegion: UMemoryRegion<RegionId, SrcKey, Sort>,
141141
fromKey: Key,
142142
toKey: Key,
@@ -253,7 +253,7 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
253253
return UTreeUpdates(newUpdates, keyToRegion, keyRangeToRegion, symbolicEq, concreteCmp, symbolicCmp)
254254
}
255255

256-
override fun <ArrayType, RegionId : UArrayId<ArrayType, SrcKey>, SrcKey> copy(
256+
override fun <ArrayType, RegionId : UArrayId<ArrayType, SrcKey>, SrcKey> copyRange(
257257
fromRegion: UMemoryRegion<RegionId, SrcKey, Sort>,
258258
fromKey: Key,
259259
toKey: Key,
Lines changed: 168 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,168 @@
1+
package org.usvm
2+
3+
import org.ksmt.utils.asExpr
4+
5+
6+
/**
7+
* An interface that represents any possible type of regions that can be used in the memory.
8+
*/
9+
interface URegionId<Key> {
10+
fun <Field, ArrayType, Sort : USort> read(
11+
key: Key,
12+
sort: Sort,
13+
heap: UReadOnlySymbolicHeap<Field, ArrayType>
14+
): UExpr<Sort>
15+
16+
fun <Field, ArrayType, Sort : USort> write(
17+
key: Key,
18+
sort: Sort,
19+
heap: USymbolicHeap<Field, ArrayType>,
20+
value: UExpr<Sort>,
21+
guard: UBoolExpr
22+
)
23+
24+
fun <Field, ArrayType> keyMapper(composer: UComposer<Field, ArrayType>): KeyMapper<Key>
25+
}
26+
27+
/**
28+
* A region id for a region storing the specific [field].
29+
*/
30+
data class UInputFieldRegionId<Field> internal constructor(
31+
val field: Field
32+
) : URegionId<UHeapRef> {
33+
@Suppress("UNCHECKED_CAST")
34+
override fun <Field, ArrayType, Sort : USort> read(
35+
key: UHeapRef,
36+
sort: Sort,
37+
heap: UReadOnlySymbolicHeap<Field, ArrayType>
38+
) = heap.readField(key, field as Field, sort).asExpr(sort)
39+
40+
@Suppress("UNCHECKED_CAST")
41+
override fun <Field, ArrayType, Sort : USort> write(
42+
key: UHeapRef,
43+
sort: Sort,
44+
heap: USymbolicHeap<Field, ArrayType>,
45+
value: UExpr<Sort>,
46+
guard: UBoolExpr
47+
) = heap.writeField(key, field as Field, sort, value, guard)
48+
49+
override fun <Field, ArrayType> keyMapper(
50+
composer: UComposer<Field, ArrayType>
51+
): KeyMapper<UHeapRef> = { composer.compose(it) }
52+
}
53+
54+
interface UArrayId<ArrayType, Key> : URegionId<Key> {
55+
val arrayType: ArrayType
56+
}
57+
58+
/**
59+
* A region id for a region storing arrays allocated during execution.
60+
* Each identifier contains information about its [arrayType] and [address].
61+
*/
62+
data class UAllocatedArrayId<ArrayType> internal constructor(
63+
override val arrayType: ArrayType,
64+
val address: UConcreteHeapAddress,
65+
) : UArrayId<ArrayType, USizeExpr> {
66+
@Suppress("UNCHECKED_CAST")
67+
override fun <Field, ArrayType, Sort : USort> read(
68+
key: USizeExpr,
69+
sort: Sort,
70+
heap: UReadOnlySymbolicHeap<Field, ArrayType>
71+
): UExpr<Sort> {
72+
val ref = key.uctx.mkConcreteHeapRef(address)
73+
return heap.readArrayIndex(ref, key, arrayType as ArrayType, sort).asExpr(sort)
74+
}
75+
76+
@Suppress("UNCHECKED_CAST")
77+
override fun <Field, ArrayType, Sort : USort> write(
78+
key: USizeExpr,
79+
sort: Sort,
80+
heap: USymbolicHeap<Field, ArrayType>,
81+
value: UExpr<Sort>,
82+
guard: UBoolExpr
83+
) {
84+
val ref = key.uctx.mkConcreteHeapRef(address)
85+
heap.writeArrayIndex(ref, key, arrayType as ArrayType, sort, value, guard)
86+
}
87+
88+
override fun <Field, ArrayType> keyMapper(
89+
composer: UComposer<Field, ArrayType>
90+
): KeyMapper<USizeExpr> = { composer.compose(it) }
91+
92+
// we don't include arrayType into hashcode and equals, because [address] already defines unambiguously
93+
override fun equals(other: Any?): Boolean {
94+
if (this === other) return true
95+
if (javaClass != other?.javaClass) return false
96+
97+
other as UAllocatedArrayId<*>
98+
99+
if (address != other.address) return false
100+
101+
return true
102+
}
103+
104+
override fun hashCode(): Int {
105+
return address
106+
}
107+
}
108+
109+
/**
110+
* A region id for a region storing arrays retrieved as a symbolic value, contains only its [arrayType].
111+
*/
112+
data class UInputArrayId<ArrayType> internal constructor(
113+
override val arrayType: ArrayType
114+
) : UArrayId<ArrayType, USymbolicArrayIndex> {
115+
@Suppress("UNCHECKED_CAST")
116+
override fun <Field, ArrayType, Sort : USort> read(
117+
key: USymbolicArrayIndex,
118+
sort: Sort,
119+
heap: UReadOnlySymbolicHeap<Field, ArrayType>
120+
): UExpr<Sort> = heap.readArrayIndex(key.first, key.second, arrayType as ArrayType, sort).asExpr(sort)
121+
122+
@Suppress("UNCHECKED_CAST")
123+
override fun <Field, ArrayType, Sort : USort> write(
124+
key: USymbolicArrayIndex,
125+
sort: Sort,
126+
heap: USymbolicHeap<Field, ArrayType>,
127+
value: UExpr<Sort>,
128+
guard: UBoolExpr
129+
) = heap.writeArrayIndex(key.first, key.second, arrayType as ArrayType, sort, value, guard)
130+
131+
override fun <Field, ArrayType> keyMapper(
132+
composer: UComposer<Field, ArrayType>
133+
): KeyMapper<USymbolicArrayIndex> = {
134+
val ref = composer.compose(it.first)
135+
val idx = composer.compose(it.second)
136+
if (ref === it.first && idx === it.second) it else ref to idx
137+
}
138+
}
139+
140+
/**
141+
* A region id for a region storing array lengths for arrays of a specific [arrayType].
142+
*/
143+
data class UInputArrayLengthId<ArrayType> internal constructor(
144+
val arrayType: ArrayType
145+
) : URegionId<UHeapRef> {
146+
@Suppress("UNCHECKED_CAST")
147+
override fun <Field, ArrayType, Sort : USort> read(
148+
key: UHeapRef,
149+
sort: Sort,
150+
heap: UReadOnlySymbolicHeap<Field, ArrayType>
151+
): UExpr<Sort> = heap.readArrayLength(key, arrayType as ArrayType).asExpr(sort)
152+
153+
@Suppress("UNCHECKED_CAST")
154+
override fun <Field, ArrayType, Sort : USort> write(
155+
key: UHeapRef,
156+
sort: Sort,
157+
heap: USymbolicHeap<Field, ArrayType>,
158+
value: UExpr<Sort>,
159+
guard: UBoolExpr
160+
) {
161+
assert(guard.isTrue)
162+
heap.writeArrayLength(key, value.asExpr(key.uctx.sizeSort), arrayType as ArrayType)
163+
}
164+
165+
override fun <Field, ArrayType> keyMapper(
166+
composer: UComposer<Field, ArrayType>
167+
): KeyMapper<UHeapRef> = { composer.compose(it) }
168+
}

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

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -100,9 +100,9 @@ class UPinpointUpdateNode<Key, ValueSort : USort>(
100100
}
101101

102102
override fun equals(other: Any?): Boolean =
103-
other is UPinpointUpdateNode<*, *> && this.key == other.key // Ignores value
103+
other is UPinpointUpdateNode<*, *> && this.key == other.key && this.guard == other.guard
104104

105-
override fun hashCode(): Int = key.hashCode() // Ignores value
105+
override fun hashCode(): Int = key.hashCode() * 31 + guard.hashCode() // Ignores value
106106

107107
override fun toString(): String = "{$key <- $value}"
108108
}
@@ -223,10 +223,15 @@ class URangedUpdateNode<RegionId : UArrayId<ArrayType, SrcKey>, ArrayType, SrcKe
223223
)
224224
}
225225

226+
// Ignores update
226227
override fun equals(other: Any?): Boolean =
227-
other is URangedUpdateNode<*, *, *, *, *> && this.fromKey == other.fromKey && this.toKey == other.toKey // Ignores update
228+
other is URangedUpdateNode<*, *, *, *, *> &&
229+
this.fromKey == other.fromKey &&
230+
this.toKey == other.toKey &&
231+
this.guard == other.guard
228232

229-
override fun hashCode(): Int = 31 * fromKey.hashCode() + toKey.hashCode() // Ignores update
233+
// Ignores update
234+
override fun hashCode(): Int = (17 * fromKey.hashCode() + toKey.hashCode()) * 31 + guard.hashCode()
230235

231236
override fun split(
232237
key: DstKey, predicate: (UExpr<ValueSort>) -> Boolean,

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

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ package org.usvm
22

33
import org.junit.jupiter.api.BeforeEach
44
import org.junit.jupiter.api.Test
5+
import org.ksmt.utils.mkConst
56
import org.usvm.util.SetRegion
67
import org.usvm.util.emptyRegionTree
78
import kotlin.test.assertNotNull
@@ -41,4 +42,33 @@ class MemoryRegionTests {
4142
assertNotNull(treeUpdates.singleOrNull())
4243
}
4344
}
45+
46+
@Test
47+
fun testMultipleWriteTheSameNodesWithDifferentGuards() {
48+
with(ctx) {
49+
val address = mkConcreteHeapRef(address = 1)
50+
51+
val guard = boolSort.mkConst("boolConst")
52+
val anotherGuard = boolSort.mkConst("anotherBoolConst")
53+
54+
val treeUpdates = UTreeUpdates<UHeapRef, SetRegion<UHeapRef>, UBv32Sort>(
55+
updates = emptyRegionTree(),
56+
keyToRegion = { SetRegion.universe() },
57+
keyRangeToRegion = { _, _ -> shouldNotBeCalled() },
58+
symbolicEq = { _, _ -> shouldNotBeCalled() },
59+
concreteCmp = { _, _ -> shouldNotBeCalled() },
60+
symbolicCmp = { _, _ -> shouldNotBeCalled() }
61+
).write(address, 1.toBv(), guard)
62+
.write(address, 2.toBv(), anotherGuard)
63+
64+
assert(treeUpdates.toList().size == 2)
65+
66+
val anotherTreeUpdates = treeUpdates
67+
.write(address, 3.toBv(), anotherGuard)
68+
.write(address, 4.toBv(), guard)
69+
70+
assert(anotherTreeUpdates.toList().size == 2)
71+
}
72+
}
73+
4474
}

0 commit comments

Comments
 (0)
Please sign in to comment.