Skip to content

Commit 710f4ac

Browse files
sergeypospelovsergeypospelov
committed
Rebase
1 parent c05e83a commit 710f4ac

13 files changed

Lines changed: 621 additions & 110 deletions

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,15 +32,15 @@ open class UComposer<Field, Type>(
3232
typeEvaluator.evalIs(composedAddress, type)
3333
}
3434

35-
fun <RegionId : URegionId<Key>, Key, Sort : USort> transformHeapReading(
35+
fun <RegionId : URegionId<Key, Sort>, Key, Sort : USort> transformHeapReading(
3636
expr: UHeapReading<RegionId, Key, Sort>,
3737
key: Key
3838
): UExpr<Sort> = with(expr) {
3939
val instantiator = { key: Key, memoryRegion: UMemoryRegion<RegionId, Key, Sort> ->
4040
// Create a copy of this heap to avoid its modification
4141
val heapToApplyUpdates = heapEvaluator.toMutableHeap()
4242
memoryRegion.applyTo(heapToApplyUpdates)
43-
region.regionId.read(key, sort, heapToApplyUpdates)
43+
region.regionId.read(heapToApplyUpdates, key)
4444
}
4545

4646
val mappedRegion = region.map(this@UComposer, instantiator)

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

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
package org.usvm
2+
3+
import org.ksmt.utils.mkConst
4+
5+
open class UExprTranslator<Field, Type> internal constructor(
6+
ctx: UContext,
7+
) : UExprTransformer<Field, Type>(ctx) {
8+
private val observers = mutableListOf<UTranslationObserver>()
9+
10+
internal fun attachObserver(observer: UTranslationObserver) {
11+
observers += observer
12+
}
13+
14+
open fun <Sort : USort> translate(expr: UExpr<Sort>): UExpr<Sort> = apply(expr)
15+
16+
// TODO: why do we have this function in UExprTransformer?
17+
override fun <Sort : USort> transform(expr: USymbol<Sort>): UExpr<Sort> {
18+
error("You must override `transform` function in org.usvm.UExprTranslator for ${expr::class}")
19+
}
20+
21+
override fun <Sort : USort> transform(expr: URegisterReading<Sort>): UExpr<Sort> {
22+
val registerConst = expr.sort.mkConst("r${expr.idx}")
23+
observers.forEach { it.newRegisterReadingTranslated(expr.idx, registerConst) }
24+
return registerConst
25+
}
26+
27+
// TODO: why do we have this function in UExprTransformer?
28+
override fun <Sort : USort> transform(expr: UHeapReading<*, *, *>): UExpr<Sort> =
29+
error("You must override `transform` function in UExprTranslator for ${expr::class}")
30+
31+
// TODO: why do we have this function in UExprTransformer?
32+
override fun <Sort : USort> transform(expr: UMockSymbol<Sort>): UExpr<Sort> =
33+
error("You must override `transform` function in UExprTranslator for ${expr::class}")
34+
35+
@Suppress("UNREACHABLE_CODE", "UNUSED_VARIABLE")
36+
override fun <Method, Sort : USort> transform(expr: UIndexedMethodReturnValue<Method, Sort>): UExpr<Sort> {
37+
val const: UExpr<Sort> = TODO("Not yet implemented")
38+
observers.forEach { it.newIndexedMethodReturnValueTranslated(expr.method, expr.callIndex, const) }
39+
return const
40+
}
41+
42+
override fun transform(expr: UNullRef): UExpr<UAddressSort> = expr.sort.mkConst("null")
43+
44+
override fun transform(expr: UConcreteHeapRef): UExpr<UAddressSort> {
45+
error("Unexpected UConcreteHeapRef $expr in UExprTranslator, that has to be impossible by construction!")
46+
}
47+
48+
override fun transform(expr: UIsExpr<Type>): UBoolExpr {
49+
error("Unexpected UIsExpr $expr in UExprTranslator, that has to be impossible by construction!")
50+
}
51+
52+
override fun transform(expr: UInputArrayLengthReading<Type>): USizeExpr =
53+
transformExprAfterTransformed(expr, expr.address) { address ->
54+
translateRegionReading(expr.region, address)
55+
}
56+
57+
override fun <Sort : USort> transform(expr: UInputArrayReading<Type, Sort>): UExpr<Sort> =
58+
transformExprAfterTransformed(expr, expr.address, expr.index) { address, index ->
59+
translateRegionReading(expr.region, address to index)
60+
}
61+
62+
override fun <Sort : USort> transform(expr: UAllocatedArrayReading<Type, Sort>): UExpr<Sort> =
63+
transformExprAfterTransformed(expr, expr.index) { index ->
64+
translateRegionReading(expr.region, index)
65+
}
66+
67+
override fun <Sort : USort> transform(expr: UInputFieldReading<Field, Sort>): UExpr<Sort> =
68+
transformExprAfterTransformed(expr, expr.address) { address ->
69+
translateRegionReading(expr.region, address)
70+
}
71+
72+
private val regionToTranslator = mutableMapOf<URegionId<*, *>, URegionTranslator<*, *, *, *>>()
73+
.withDefault { regionId ->
74+
val regionTranslator = regionId.translator(this)
75+
observers.forEach { it.newRegionTranslator(regionId, regionTranslator) }
76+
regionTranslator
77+
}
78+
79+
open fun <Key, Sort : USort> translateRegionReading(
80+
region: UMemoryRegion<URegionId<Key, Sort>, Key, Sort>,
81+
key: Key,
82+
): UExpr<Sort> {
83+
@Suppress("UNCHECKED_CAST")
84+
val translator =
85+
regionToTranslator.getValue(region.regionId) as URegionTranslator<URegionId<Key, Sort>, Key, Sort, *>
86+
return translator.translateReading(region, key)
87+
}
88+
}
89+
90+
internal typealias RegionTranslatorConstructor<T, U> = (UExprTranslator<*, *>) -> URegionTranslator<URegionId<T, U>, T, U, *>
91+
92+
// TODO: maybe split this function into virtual function of URegionID
93+
internal val <Key, Sort : USort> URegionId<Key, Sort>.translator: RegionTranslatorConstructor<Key, Sort>
94+
get() = { translator ->
95+
val ctx = sort.uctx
96+
@Suppress("UNCHECKED_CAST")
97+
when (this) {
98+
is UInputArrayId<*, Sort> -> U2DArrayRegionTranslator(translator, ctx.addressSort, ctx.sizeSort, this)
99+
is UAllocatedArrayId<*, Sort> -> U1DArrayRegionTranslator(translator, ctx.sizeSort, this)
100+
is UInputArrayLengthId<*> -> U1DArrayRegionTranslator(translator, ctx.addressSort, this)
101+
is UInputFieldRegionId<*, Sort> -> U1DArrayRegionTranslator(translator, ctx.addressSort, this)
102+
else -> error("Unexpected regionId: $this")
103+
} as URegionTranslator<URegionId<Key, Sort>, Key, Sort, *>
104+
}
105+
106+
// TODO: looks odd, because we duplicate StackEvaluator::eval, MockEvaluator::eval with slightly changed signature...
107+
internal interface UTranslationObserver {
108+
fun newRegionTranslator(
109+
regionId: URegionId<*, *>,
110+
translator: URegionTranslator<*, *, *, *>,
111+
)
112+
113+
fun <Sort : USort> newRegisterReadingTranslated(idx: Int, translated: UExpr<Sort>)
114+
115+
fun <Method, Sort : USort> newIndexedMethodReturnValueTranslated(
116+
method: Method,
117+
callIndex: Int,
118+
translated: UExpr<Sort>,
119+
)
120+
}

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,7 @@ class URegisterReading<Sort : USort> internal constructor(
127127
}
128128
}
129129

130-
abstract class UHeapReading<RegionId : URegionId<Key>, Key, Sort : USort>(
130+
abstract class UHeapReading<RegionId : URegionId<Key, Sort>, Key, Sort : USort>(
131131
ctx: UContext,
132132
val region: UMemoryRegion<RegionId, Key, Sort>
133133
) : USymbol<Sort>(ctx) {
@@ -138,7 +138,7 @@ class UInputFieldReading<Field, Sort : USort> internal constructor(
138138
ctx: UContext,
139139
region: UInputFieldRegion<Field, Sort>,
140140
val address: UHeapRef,
141-
) : UHeapReading<UInputFieldRegionId<Field>, UHeapRef, Sort>(ctx, region) {
141+
) : UHeapReading<UInputFieldRegionId<Field, Sort>, UHeapRef, Sort>(ctx, region) {
142142
@Suppress("UNCHECKED_CAST")
143143
override fun accept(transformer: KTransformerBase): KExpr<Sort> {
144144
require(transformer is UExprTransformer<*, *>)
@@ -162,7 +162,7 @@ class UAllocatedArrayReading<ArrayType, Sort : USort> internal constructor(
162162
ctx: UContext,
163163
region: UAllocatedArrayRegion<ArrayType, Sort>,
164164
val index: USizeExpr,
165-
) : UHeapReading<UAllocatedArrayId<ArrayType>, USizeExpr, Sort>(ctx, region) {
165+
) : UHeapReading<UAllocatedArrayId<ArrayType, Sort>, USizeExpr, Sort>(ctx, region) {
166166
@Suppress("UNCHECKED_CAST")
167167
override fun accept(transformer: KTransformerBase): KExpr<Sort> {
168168
require(transformer is UExprTransformer<*, *>)
@@ -192,7 +192,7 @@ class UInputArrayReading<ArrayType, Sort : USort> internal constructor(
192192
region: UInputArrayRegion<ArrayType, Sort>,
193193
val address: UHeapRef,
194194
val index: USizeExpr
195-
) : UHeapReading<UInputArrayId<ArrayType>, USymbolicArrayIndex, Sort>(ctx, region) {
195+
) : UHeapReading<UInputArrayId<ArrayType, Sort>, USymbolicArrayIndex, Sort>(ctx, region) {
196196
@Suppress("UNCHECKED_CAST")
197197
override fun accept(transformer: KTransformerBase): KExpr<Sort> {
198198
require(transformer is UExprTransformer<*, *>)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -122,7 +122,7 @@ data class URegionHeap<Field, ArrayType>(
122122
arrayType: ArrayType,
123123
): UInputArrayLengthRegion<ArrayType> =
124124
inputLengths[arrayType]
125-
?: emptyArrayLengthRegion(arrayType, ctx) { ref, region ->
125+
?: emptyArrayLengthRegion(arrayType, ctx.sizeSort) { ref, region ->
126126
ctx.mkInputArrayLengthReading(region, ref)
127127
}
128128

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

Lines changed: 27 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -22,13 +22,14 @@ typealias UInstantiator<RegionId, Key, Sort> = (key: Key, UMemoryRegion<RegionId
2222
* @property defaultValue describes the initial values for the region. If [defaultValue] equals `null` then this region
2323
* is filled with symbolics.
2424
*/
25-
data class UMemoryRegion<RegionId : URegionId<Key>, Key, Sort : USort>(
25+
data class UMemoryRegion<out RegionId : URegionId<Key, Sort>, Key, Sort : USort>(
2626
val regionId: RegionId,
27-
val sort: Sort,
2827
val updates: UMemoryUpdates<Key, Sort>,
29-
private val defaultValue: UExpr<Sort>?, // If defaultValue = null then this region is filled with symbolics
3028
private val instantiator: UInstantiator<RegionId, Key, Sort>,
3129
) {
30+
val sort: Sort get() = regionId.sort
31+
private val defaultValue = regionId.defaultValue
32+
3233
private fun read(key: Key, updates: UMemoryUpdates<Key, Sort>): UExpr<Sort> {
3334
val lastUpdatedElement = updates.lastUpdatedElementOrNull()
3435

@@ -159,26 +160,28 @@ data class UMemoryRegion<RegionId : URegionId<Key>, Key, Sort : USort>(
159160
composer: UComposer<Field, Type>,
160161
instantiator: UInstantiator<RegionId, Key, Sort> = this.instantiator,
161162
): UMemoryRegion<RegionId, Key, Sort> {
162-
// Map the updates and the default value
163+
// Map the updates and the regionId
164+
@Suppress("UNCHECKED_CAST")
165+
val mappedRegionId = regionId.map(composer) as RegionId
163166
val mappedUpdates = updates.map(regionId.keyMapper(composer), composer)
164-
val mappedDefaultValue = defaultValue?.let { composer.compose(it) }
165167

166168
// Note that we cannot use optimization with unchanged mappedUpdates and mappedDefaultValues here
167169
// since in a new region we might have an updated instantiator.
168170
// Therefore, we have to check their reference equality as well.
169-
if (mappedUpdates === updates && mappedDefaultValue === defaultValue && instantiator === this.instantiator) {
171+
if (mappedUpdates === updates && mappedRegionId === regionId && instantiator === this.instantiator) {
170172
return this
171173
}
172174

173-
return UMemoryRegion(regionId, sort, mappedUpdates, mappedDefaultValue, instantiator)
175+
// Otherwise, construct a new region with mapped values and a new instantiator.
176+
return UMemoryRegion(mappedRegionId, mappedUpdates, instantiator)
174177
}
175178

176179
@Suppress("UNCHECKED_CAST")
177180
fun <Field, Type> applyTo(heap: USymbolicHeap<Field, Type>) {
178181
// Apply each update on the copy
179182
updates.forEach {
180183
when (it) {
181-
is UPinpointUpdateNode<Key, Sort> -> regionId.write(it.key, sort, heap, it.value, it.guard)
184+
is UPinpointUpdateNode<Key, Sort> -> regionId.write(heap, it.key, it.value, it.guard)
182185
is URangedUpdateNode<*, *, *, Key, Sort> -> {
183186
it.region.applyTo(heap)
184187

@@ -198,7 +201,7 @@ data class UMemoryRegion<RegionId : URegionId<Key>, Key, Sort : USort>(
198201
* with values from memory region [fromRegion] read from range
199202
* of addresses [[keyConverter].convert([fromKey]) : [keyConverter].convert([toKey])]
200203
*/
201-
fun <ArrayType, OtherRegionId : UArrayId<ArrayType, SrcKey>, SrcKey> copyRange(
204+
fun <ArrayType, OtherRegionId : UArrayId<ArrayType, SrcKey, Sort>, SrcKey> copyRange(
202205
fromRegion: UMemoryRegion<OtherRegionId, SrcKey, Sort>,
203206
fromKey: Key, toKey: Key,
204207
keyConverter: UMemoryKeyConverter<SrcKey, Key>,
@@ -243,7 +246,7 @@ class GuardBuilder(nonMatchingUpdates: UBoolExpr) {
243246
typealias USymbolicArrayIndex = Pair<UHeapRef, USizeExpr>
244247

245248
fun heapRefEq(ref1: UHeapRef, ref2: UHeapRef): UBoolExpr =
246-
ref1.uctx.mkHeapRefEq(ref1, ref2) // TODO: use simplified equality!
249+
ref1.uctx.mkHeapRefEq(ref1, ref2)
247250

248251
@Suppress("UNUSED_PARAMETER")
249252
fun heapRefCmpSymbolic(ref1: UHeapRef, ref2: UHeapRef): UBoolExpr =
@@ -254,17 +257,16 @@ fun heapRefCmpConcrete(ref1: UHeapRef, ref2: UHeapRef): Boolean =
254257
error("Heap references should not be compared!")
255258

256259
fun indexEq(idx1: USizeExpr, idx2: USizeExpr): UBoolExpr =
257-
idx1.ctx.mkEq(idx1, idx2) // TODO: use simplified equality!
260+
idx1.ctx.mkEq(idx1, idx2)
258261

259262
fun indexLeSymbolic(idx1: USizeExpr, idx2: USizeExpr): UBoolExpr =
260-
idx1.ctx.mkBvSignedLessOrEqualExpr(idx1, idx2) // TODO: use simplified comparison!
263+
idx1.ctx.mkBvSignedLessOrEqualExpr(idx1, idx2)
261264

262265
fun indexLeConcrete(idx1: USizeExpr, idx2: USizeExpr): Boolean =
263266
// TODO: to optimize things up, we could pass path constraints here and lookup the numeric bounds for idx1 and idx2
264267
idx1 == idx2 || (idx1 is UConcreteSize && idx2 is UConcreteSize && idx1.numberValue <= idx2.numberValue)
265268

266269
fun refIndexEq(idx1: USymbolicArrayIndex, idx2: USymbolicArrayIndex): UBoolExpr = with(idx1.first.ctx) {
267-
// TODO: use simplified operations!
268270
return@with (idx1.first eq idx2.first) and indexEq(idx1.second, idx2.second)
269271
}
270272

@@ -301,9 +303,9 @@ fun refIndexRangeRegion(
301303
idx2: USymbolicArrayIndex,
302304
): UArrayIndexRegion = indexRangeRegion(idx1.second, idx2.second)
303305

304-
typealias UInputFieldRegion<Field, Sort> = UMemoryRegion<UInputFieldRegionId<Field>, UHeapRef, Sort>
305-
typealias UAllocatedArrayRegion<ArrayType, Sort> = UMemoryRegion<UAllocatedArrayId<ArrayType>, USizeExpr, Sort>
306-
typealias UInputArrayRegion<ArrayType, Sort> = UMemoryRegion<UInputArrayId<ArrayType>, USymbolicArrayIndex, Sort>
306+
typealias UInputFieldRegion<Field, Sort> = UMemoryRegion<UInputFieldRegionId<Field, Sort>, UHeapRef, Sort>
307+
typealias UAllocatedArrayRegion<ArrayType, Sort> = UMemoryRegion<UAllocatedArrayId<ArrayType, Sort>, USizeExpr, Sort>
308+
typealias UInputArrayRegion<ArrayType, Sort> = UMemoryRegion<UInputArrayId<ArrayType, Sort>, USymbolicArrayIndex, Sort>
307309
typealias UInputArrayLengthRegion<ArrayType> = UMemoryRegion<UInputArrayLengthId<ArrayType>, UHeapRef, USizeSort>
308310

309311
typealias KeyMapper<Key> = (Key) -> Key
@@ -325,51 +327,47 @@ val <ArrayType> UInputArrayLengthRegion<ArrayType>.inputLengthArrayType
325327
fun <Field, Sort : USort> emptyInputFieldRegion(
326328
field: Field,
327329
sort: Sort,
328-
instantiator: UInstantiator<UInputFieldRegionId<Field>, UHeapRef, Sort>,
330+
instantiator: UInstantiator<UInputFieldRegionId<Field, Sort>, UHeapRef, Sort>,
329331
): UInputFieldRegion<Field, Sort> = UMemoryRegion(
330-
UInputFieldRegionId(field),
331-
sort,
332+
UInputFieldRegionId(field, sort),
332333
UEmptyUpdates(::heapRefEq, ::heapRefCmpConcrete, ::heapRefCmpSymbolic),
333-
defaultValue = null,
334334
instantiator
335335
)
336336

337337
fun <ArrayType, Sort : USort> emptyAllocatedArrayRegion(
338338
arrayType: ArrayType,
339339
address: UConcreteHeapAddress,
340340
sort: Sort,
341-
instantiator: UInstantiator<UAllocatedArrayId<ArrayType>, USizeExpr, Sort>,
341+
instantiator: UInstantiator<UAllocatedArrayId<ArrayType, Sort>, USizeExpr, Sort>,
342342
): UAllocatedArrayRegion<ArrayType, Sort> {
343343
val updates = UTreeUpdates<USizeExpr, UArrayIndexRegion, Sort>(
344344
updates = emptyRegionTree(),
345345
::indexRegion, ::indexRangeRegion, ::indexEq, ::indexLeConcrete, ::indexLeSymbolic
346346
)
347-
val regionId = UAllocatedArrayId(arrayType, address)
348-
return UMemoryRegion(regionId, sort, updates, sort.defaultValue(), instantiator)
347+
val regionId = UAllocatedArrayId(arrayType, address, sort)
348+
return UMemoryRegion(regionId, updates, instantiator)
349349
}
350350

351351
fun <ArrayType, Sort : USort> emptyInputArrayRegion(
352352
arrayType: ArrayType,
353353
sort: Sort,
354-
instantiator: UInstantiator<UInputArrayId<ArrayType>, USymbolicArrayIndex, Sort>,
354+
instantiator: UInstantiator<UInputArrayId<ArrayType, Sort>, USymbolicArrayIndex, Sort>,
355355
): UInputArrayRegion<ArrayType, Sort> {
356356
val updates = UTreeUpdates<USymbolicArrayIndex, UArrayIndexRegion, Sort>(
357357
updates = emptyRegionTree(),
358358
::refIndexRegion, ::refIndexRangeRegion, ::refIndexEq, ::refIndexCmpConcrete, ::refIndexCmpSymbolic
359359
)
360-
return UMemoryRegion(UInputArrayId(arrayType), sort, updates, defaultValue = null, instantiator)
360+
return UMemoryRegion(UInputArrayId(arrayType, sort), updates, instantiator)
361361
}
362362

363363
fun <ArrayType> emptyArrayLengthRegion(
364364
arrayType: ArrayType,
365-
ctx: UContext,
365+
sizeSort: USizeSort,
366366
instantiator: UInstantiator<UInputArrayLengthId<ArrayType>, UHeapRef, USizeSort>,
367367
): UInputArrayLengthRegion<ArrayType> =
368368
UMemoryRegion(
369-
UInputArrayLengthId(arrayType),
370-
ctx.sizeSort,
369+
UInputArrayLengthId(arrayType, sizeSort),
371370
UEmptyUpdates(::heapRefEq, ::heapRefCmpConcrete, ::heapRefCmpSymbolic),
372-
defaultValue = null,
373371
instantiator
374372
)
375373

0 commit comments

Comments
 (0)