Skip to content

Commit 7ff8aa1

Browse files
CaelmBleiddCaelmBleidd
committed
Refactoring
1 parent 11f4d12 commit 7ff8aa1

10 files changed

Lines changed: 261 additions & 177 deletions

File tree

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

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

35-
fun <RegionId: URegionId<Key>, Key, Sort : USort> transformHR(
35+
fun <RegionId : URegionId<Key>, Key, Sort : USort> transformHeapReading(
3636
expr: UHeapReading<RegionId, Key, Sort>,
3737
key: Key
3838
): UExpr<Sort> = with(expr) {
@@ -49,16 +49,16 @@ open class UComposer<Field, Type>(
4949
}
5050

5151
override fun transform(expr: UArrayLength<Type>): USizeExpr =
52-
transformHR(expr, expr.address)
52+
transformHeapReading(expr, expr.address)
5353

5454
override fun <Sort : USort> transform(expr: UInputArrayReading<Type, Sort>): UExpr<Sort> =
55-
transformHR(expr, expr.address to expr.index)
55+
transformHeapReading(expr, expr.address to expr.index)
5656

5757
override fun <Sort : USort> transform(expr: UAllocatedArrayReading<Type, Sort>): UExpr<Sort> =
58-
transformHR(expr, expr.index)
58+
transformHeapReading(expr, expr.index)
5959

6060
override fun transform(expr: UConcreteHeapRef): UExpr<UAddressSort> = expr
6161

6262
override fun <Sort : USort> transform(expr: UFieldReading<Field, Sort>): UExpr<Sort> =
63-
transformHR(expr, expr.address)
63+
transformHeapReading(expr, expr.address)
6464
}

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -259,3 +259,10 @@ class UIsExpr<Type> internal constructor(
259259
override fun internHashCode(): Int = hash(ref, type)
260260
}
261261
//endregion
262+
263+
//region Utils
264+
265+
val UBoolExpr.isFalse get() = this === ctx.falseExpr
266+
val UBoolExpr.isTrue get() = !isFalse
267+
268+
//endregion

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

Lines changed: 46 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -37,20 +37,28 @@ class UEmptyHeap<Field, ArrayType>(private val ctx: UContext) : UReadOnlySymboli
3737

3838
interface UHeap<Ref, Value, SizeT, Field, ArrayType, Guard> : UReadOnlyHeap<Ref, Value, SizeT, Field, ArrayType, Guard> {
3939
fun <Sort : USort> writeField(ref: Ref, field: Field, sort: Sort, value: Value, guard: Guard)
40-
fun <Sort : USort> writeArrayIndex(ref: Ref, index: SizeT, type: ArrayType, elementSort: Sort, value: Value, guard: Guard)
40+
fun <Sort : USort> writeArrayIndex(
41+
ref: Ref,
42+
index: SizeT,
43+
type: ArrayType,
44+
elementSort: Sort,
45+
value: Value,
46+
guard: Guard
47+
)
4148

4249
fun writeArrayLength(ref: Ref, size: SizeT, arrayType: ArrayType)
4350

4451
fun <Sort : USort> memset(ref: Ref, type: ArrayType, sort: Sort, contents: Sequence<Value>)
45-
fun <Sort: USort> memcpy(
52+
fun <Sort : USort> memcpy(
4653
srcRef: Ref,
4754
dstRef: Ref,
4855
type: ArrayType,
49-
sort: Sort,
56+
elementSort: Sort,
5057
fromSrcIdx: SizeT,
5158
fromDstIdx: SizeT,
5259
toDstIdx: SizeT,
53-
guard: Guard)
60+
guard: Guard
61+
)
5462

5563
fun allocate(): UConcreteHeapAddress
5664
fun allocateArray(count: SizeT): UConcreteHeapAddress
@@ -143,20 +151,28 @@ data class URegionHeap<Field, ArrayType>(
143151
}
144152

145153
// TODO: Either prohibit merging concrete and symbolic heap addresses, or fork state by ite-refs here
146-
override fun <Sort : USort> writeField(ref: UHeapRef, field: Field, sort: Sort, value: UExpr<out USort>, guard: UBoolExpr) {
147-
if (guard === ctx.falseExpr)
148-
return
154+
override fun <Sort : USort> writeField(
155+
ref: UHeapRef,
156+
field: Field,
157+
sort: Sort,
158+
value: UExpr<out USort>,
159+
guard: UBoolExpr
160+
) {
161+
// A write operation that never succeeds
162+
if (guard.isFalse) return
149163

150164
val valueToWrite = value.asExpr(sort)
151165

152166
when (ref) {
153167
is UConcreteHeapRef -> {
154-
if (guard === guard.ctx.trueExpr) {
155-
allocatedFields = allocatedFields.put(Pair(ref.address, field), valueToWrite)
168+
val key = ref.address to field
169+
val allocatedFieldValue = if (guard.isTrue) {
170+
valueToWrite
156171
} else {
157-
val iteValue = ctx.mkIte(guard, valueToWrite, readField(ref, field, sort))
158-
allocatedFields = allocatedFields.put(ref.address to field, iteValue)
172+
ctx.mkIte(guard, valueToWrite, readField(ref, field, sort))
159173
}
174+
175+
allocatedFields = allocatedFields.put(key, allocatedFieldValue)
160176
}
161177

162178
else -> {
@@ -175,8 +191,8 @@ data class URegionHeap<Field, ArrayType>(
175191
value: UExpr<out USort>,
176192
guard: UBoolExpr
177193
) {
178-
if (guard === ctx.falseExpr)
179-
return
194+
// A write operation that never succeeds
195+
if (guard.isFalse) return
180196

181197
val valueToWrite = value.asExpr(elementSort)
182198

@@ -189,7 +205,7 @@ data class URegionHeap<Field, ArrayType>(
189205

190206
else -> {
191207
val region = inputArrayRegion(type, elementSort)
192-
val newRegion = region.write(Pair(ref, index), valueToWrite, guard)
208+
val newRegion = region.write(ref to index, valueToWrite, guard)
193209
inputArrays = inputArrays.put(type, newRegion)
194210
}
195211
}
@@ -215,34 +231,37 @@ data class URegionHeap<Field, ArrayType>(
215231
TODO("Not yet implemented")
216232
}
217233

218-
override fun <Sort: USort> memcpy(
234+
override fun <Sort : USort> memcpy(
219235
srcRef: UHeapRef,
220236
dstRef: UHeapRef,
221237
type: ArrayType,
222-
sort: Sort,
238+
elementSort: Sort,
223239
fromSrcIdx: USizeExpr,
224240
fromDstIdx: USizeExpr,
225241
toDstIdx: USizeExpr,
226242
guard: UBoolExpr
227243
) {
228-
if (guard === guard.ctx.falseExpr)
229-
return
244+
// A copy operation that never succeeds
245+
if (guard.isFalse) return
230246

231247
val src = srcRef to fromSrcIdx
232248
val dst = dstRef to fromDstIdx
233-
when(srcRef) {
249+
250+
when (srcRef) {
234251
is UConcreteHeapRef -> {
235-
val srcRegion = allocatedArrayRegion(type, srcRef.address, sort)
252+
val srcRegion = allocatedArrayRegion(type, srcRef.address, elementSort)
253+
236254
when (dstRef) {
237255
is UConcreteHeapRef -> {
238-
val dstRegion = allocatedArrayRegion(type, dstRef.address, sort)
256+
val dstRegion = allocatedArrayRegion(type, dstRef.address, elementSort)
239257
val keyConverter = UAllocatedToAllocatedKeyConverter(src, dst, toDstIdx)
240258
val newDstRegion = dstRegion.memcpy(srcRegion, fromDstIdx, toDstIdx, keyConverter, guard)
241259
allocatedArrays = allocatedArrays.put(dstRef.address, newDstRegion)
242260
}
261+
243262
is UIteExpr -> TODO()
244263
else -> {
245-
val dstRegion = inputArrayRegion(type, sort)
264+
val dstRegion = inputArrayRegion(type, elementSort)
246265
val keyConverter = UAllocatedToInputKeyConverter(src, dst, toDstIdx)
247266
val newDstRegion = dstRegion.memcpy(srcRegion, dst, dstRef to toDstIdx, keyConverter, guard)
248267
inputArrays = inputArrays.put(type, newDstRegion)
@@ -253,17 +272,19 @@ data class URegionHeap<Field, ArrayType>(
253272
is UIteExpr -> TODO()
254273

255274
else -> {
256-
val srcRegion = inputArrayRegion(type, sort)
275+
val srcRegion = inputArrayRegion(type, elementSort)
276+
257277
when (dstRef) {
258278
is UConcreteHeapRef -> {
259-
val dstRegion = allocatedArrayRegion(type, dstRef.address, sort)
279+
val dstRegion = allocatedArrayRegion(type, dstRef.address, elementSort)
260280
val keyConverter = UInputToAllocatedKeyConverter(src, dst, toDstIdx)
261281
val newDstRegion = dstRegion.memcpy(srcRegion, fromDstIdx, toDstIdx, keyConverter, guard)
262282
allocatedArrays = allocatedArrays.put(dstRef.address, newDstRegion)
263283
}
284+
264285
is UIteExpr -> TODO()
265286
else -> {
266-
val dstRegion = inputArrayRegion(type, sort)
287+
val dstRegion = inputArrayRegion(type, elementSort)
267288
val keyConverter = UInputToInputKeyConverter(src, dst, toDstIdx)
268289
val newDstRegion = dstRegion.memcpy(srcRegion, dst, dstRef to toDstIdx, keyConverter, guard)
269290
inputArrays = inputArrays.put(type, newDstRegion)

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

Lines changed: 29 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -37,25 +37,27 @@ interface UMemory<LValue, RValue, SizeT, HeapRef, Type> {
3737
* to range of elements [[fromDst]:[fromDst] + [length] - 1] of array with address [dst].
3838
* Both arrays must have type [arrayType].
3939
*/
40-
fun memcpy(src: HeapRef, dst: HeapRef, arrayType: Type, sort: USort, fromSrc: SizeT, fromDst: SizeT, length: SizeT)
40+
fun memcpy(src: HeapRef, dst: HeapRef, arrayType: Type, elementSort: USort, fromSrc: SizeT, fromDst: SizeT, length: SizeT)
4141

4242
/**
4343
* Returns length of an array
4444
*/
4545
fun length(ref: HeapRef, arrayType: Type): SizeT
4646

47-
fun <Sort: USort> compose(expr: UExpr<Sort>): UExpr<Sort>
47+
fun <Sort : USort> compose(expr: UExpr<Sort>): UExpr<Sort>
4848

4949
/**
5050
* Creates new instance of program memory.
51-
* @warning: symbolic engine may use this operation potentially large amount of times.
51+
*
52+
* **Warning**: symbolic engine may use this operation potentially large number of times.
5253
* Implementation must use persistent data structures to speed it up.
5354
*/
5455
fun clone(): UMemory<LValue, RValue, SizeT, HeapRef, Type>
5556
}
5657

5758
typealias USymbolicMemory<Type> = UMemory<ULValue, UExpr<out USort>, USizeExpr, UHeapRef, Type>
5859

60+
@Suppress("MemberVisibilityCanBePrivate")
5961
open class UMemoryBase<Field, Type, Method>(
6062
protected val ctx: UContext,
6163
protected val typeSystem: UTypeSystem<Type>,
@@ -64,25 +66,27 @@ open class UMemoryBase<Field, Type, Method>(
6466
protected var types: UTypeStorage<Type> = UTypeStorage(ctx, typeSystem),
6567
protected var mocker: UMocker<Method> = UIndexedMocker(ctx)
6668
// TODO: we can eliminate mocker by moving compose to UState?
67-
)
68-
: USymbolicMemory<Type>
69-
{
69+
) : USymbolicMemory<Type> {
7070
@Suppress("UNCHECKED_CAST")
71-
override fun read(lvalue: ULValue): UExpr<out USort> =
72-
when(lvalue) {
73-
is URegisterRef -> stack.readRegister(lvalue.idx, lvalue.sort)
74-
is UFieldRef<*> -> heap.readField(lvalue.ref, lvalue.field as Field, lvalue.sort).asExpr(lvalue.sort)
75-
is UArrayIndexRef<*> -> heap.readArrayIndex(lvalue.ref, lvalue.index, lvalue.arrayType as Type, lvalue.sort).asExpr(lvalue.sort)
76-
else -> throw IllegalArgumentException("Unexpected lvalue $lvalue")
71+
override fun read(lvalue: ULValue): UExpr<out USort> = with(lvalue) {
72+
when (this) {
73+
is URegisterRef -> stack.readRegister(idx, sort)
74+
is UFieldRef<*> -> heap.readField(ref, field as Field, sort).asExpr(sort)
75+
is UArrayIndexRef<*> -> heap.readArrayIndex(ref, index, arrayType as Type, sort).asExpr(sort)
76+
77+
else -> throw IllegalArgumentException("Unexpected lvalue $this")
7778
}
79+
}
7880

7981
@Suppress("UNCHECKED_CAST")
80-
override fun write(lvalue: ULValue, rvalue: UExpr<out USort>) {
81-
when(lvalue) {
82-
is URegisterRef -> stack.writeRegister(lvalue.idx, rvalue)
83-
is UFieldRef<*> -> heap.writeField(lvalue.ref, lvalue.field as Field, lvalue.sort, rvalue, rvalue.ctx.trueExpr)
84-
is UArrayIndexRef<*> -> heap.writeArrayIndex(lvalue.ref, lvalue.index, lvalue.arrayType as Type, lvalue.sort, rvalue, rvalue.ctx.trueExpr)
85-
else -> throw IllegalArgumentException("Unexpected lvalue $lvalue")
82+
override fun write(lvalue: ULValue, rvalue: UExpr<out USort>) = with(lvalue) {
83+
when (this) {
84+
is URegisterRef -> stack.writeRegister(idx, rvalue)
85+
is UFieldRef<*> -> heap.writeField(ref, field as Field, sort, rvalue, guard = ctx.trueExpr)
86+
is UArrayIndexRef<*> -> {
87+
heap.writeArrayIndex(ref, index, arrayType as Type, sort, rvalue, guard = ctx.trueExpr)
88+
}
89+
else -> throw IllegalArgumentException("Unexpected lvalue $this")
8690
}
8791
}
8892

@@ -101,16 +105,17 @@ open class UMemoryBase<Field, Type, Method>(
101105
override fun memset(ref: UHeapRef, arrayType: Type, elementSort: USort, contents: Sequence<UExpr<out USort>>) =
102106
heap.memset(ref, arrayType, elementSort, contents)
103107

104-
override fun memcpy(src: UHeapRef, dst: UHeapRef, arrayType: Type, sort: USort,
105-
fromSrc: USizeExpr, fromDst: USizeExpr, length: USizeExpr) = with(src.ctx) {
106-
val toDst = ctx.mkBvAddExpr(fromDst, length)
107-
heap.memcpy(src, dst, arrayType, sort, fromSrc, fromDst, toDst, trueExpr)
108+
override fun memcpy(
109+
src: UHeapRef, dst: UHeapRef, arrayType: Type, elementSort: USort,
110+
fromSrc: USizeExpr, fromDst: USizeExpr, length: USizeExpr
111+
) = with(src.ctx) {
112+
val toDst = mkBvAddExpr(fromDst, length)
113+
heap.memcpy(src, dst, arrayType, elementSort, fromSrc, fromDst, toDst, guard = trueExpr)
108114
}
109115

110-
111116
override fun length(ref: UHeapRef, arrayType: Type): USizeExpr = heap.readArrayLength(ref, arrayType)
112117

113-
override fun <Sort: USort> compose(expr: UExpr<Sort>): UExpr<Sort> {
118+
override fun <Sort : USort> compose(expr: UExpr<Sort>): UExpr<Sort> {
114119
val composer = UComposer(ctx, stack, heap, types, mocker)
115120
return composer.compose(expr)
116121
}

0 commit comments

Comments
 (0)