diff --git a/usvm-core/src/main/kotlin/org/usvm/Composition.kt b/usvm-core/src/main/kotlin/org/usvm/Composition.kt index 56ebf4aa31..cceeb0b30d 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Composition.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Composition.kt @@ -1,7 +1,5 @@ package org.usvm -import org.ksmt.utils.asExpr - @Suppress("MemberVisibilityCanBePrivate") open class UComposer( ctx: UContext, @@ -34,41 +32,33 @@ open class UComposer( typeEvaluator.evalIs(composedAddress, type) } - override fun transform(expr: UArrayLength): USizeExpr = with(expr) { - val composedAddress = compose(address) - heapEvaluator.readArrayLength(composedAddress, region.regionId.arrayType) - } - - override fun transform( - expr: UInputArrayReading + fun , Key, Sort : USort> transformHeapReading( + expr: UHeapReading, + key: Key ): UExpr = with(expr) { - val composedAddress = compose(address) - val composedIndex = compose(index) - // TODO compose the region + val instantiator = { key: Key, memoryRegion: UMemoryRegion -> + // Create a copy of this heap to avoid its modification + val heapToApplyUpdates = heapEvaluator.toMutableHeap() + memoryRegion.applyTo(heapToApplyUpdates) + region.regionId.read(key, sort, heapToApplyUpdates) + } - heapEvaluator.readArrayIndex( - composedAddress, - composedIndex, - region.regionId.arrayType, - sort - ).asExpr(sort) + val mappedRegion = region.map(this@UComposer, instantiator) + val mappedKey = region.regionId.keyMapper(this@UComposer)(key) + mappedRegion.read(mappedKey) } - override fun transform( - expr: UAllocatedArrayReading - ): UExpr = with(expr) { - val composedIndex = compose(index) - // TODO compose the region - val heapRef = uctx.mkConcreteHeapRef(region.regionId.address) + override fun transform(expr: UArrayLength): USizeExpr = + transformHeapReading(expr, expr.address) - heapEvaluator.readArrayIndex(heapRef, composedIndex, region.regionId.arrayType, sort).asExpr(sort) - } + override fun transform(expr: UInputArrayReading): UExpr = + transformHeapReading(expr, expr.address to expr.index) - override fun transform(expr: UFieldReading): UExpr = with(expr) { - val composedAddress = compose(address) - // TODO compose the region - heapEvaluator.readField(composedAddress, region.regionId.field, sort).asExpr(sort) - } + override fun transform(expr: UAllocatedArrayReading): UExpr = + transformHeapReading(expr, expr.index) override fun transform(expr: UConcreteHeapRef): UExpr = expr + + override fun transform(expr: UFieldReading): UExpr = + transformHeapReading(expr, expr.address) } diff --git a/usvm-core/src/main/kotlin/org/usvm/Context.kt b/usvm-core/src/main/kotlin/org/usvm/Context.kt index f1833b78dd..3b18d96ec4 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Context.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Context.kt @@ -8,9 +8,9 @@ import org.ksmt.utils.cast @Suppress("LeakingThis") open class UContext( - private val operationMode: OperationMode = OperationMode.CONCURRENT, // TODO replace it when we have KSMT 0.3.3 version - private val astManagementMode: AstManagementMode = AstManagementMode.GC, // TODO replace it when we have KSMT 0.3.3 version - private val simplificationMode: SimplificationMode = SimplificationMode.SIMPLIFY + operationMode: OperationMode = OperationMode.CONCURRENT, + astManagementMode: AstManagementMode = AstManagementMode.GC, + simplificationMode: SimplificationMode = SimplificationMode.SIMPLIFY ) : KContext(operationMode, astManagementMode, simplificationMode) { val addressSort: UAddressSort = mkUninterpretedSort("Address") @@ -31,7 +31,7 @@ open class UContext( private val inputFieldReadingCache = mkAstInterner>() - fun mkFieldReading( + fun mkInputFieldReading( region: UInputFieldMemoryRegion, address: UHeapRef, ): UFieldReading = inputFieldReadingCache.createIfContextActive { @@ -57,12 +57,12 @@ open class UContext( UInputArrayReading(this, region, address, index) }.cast() - private val arrayLengthCache = mkAstInterner>() + private val inputArrayLengthCache = mkAstInterner>() - fun mkArrayLength( + fun mkInputArrayLength( region: UInputArrayLengthMemoryRegion, address: UHeapRef, - ): UArrayLength = arrayLengthCache.createIfContextActive { + ): UArrayLength = inputArrayLengthCache.createIfContextActive { UArrayLength(this, region, address) }.cast() diff --git a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt index b8c5ca8119..6b33054d0d 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt @@ -49,7 +49,7 @@ class UConcreteHeapRef internal constructor(ctx: UContext, val address: UConcret } override fun print(printer: ExpressionPrinter) { - TODO("Not yet implemented") + printer.append("(concreteAddr $address)") } val isNull = (address == nullAddress) @@ -85,7 +85,6 @@ class UArrayIndexRef( abstract class USymbol(ctx: UContext) : UExpr(ctx) { } -@Suppress("UNUSED_PARAMETER") class URegisterReading internal constructor( ctx: UContext, val idx: Int, @@ -105,7 +104,7 @@ class URegisterReading internal constructor( override fun internHashCode(): Int = hash(idx, sort) } -abstract class UHeapReading( +abstract class UHeapReading, Key, Sort : USort>( ctx: UContext, val region: UMemoryRegion ) : USymbol(ctx) { @@ -128,7 +127,7 @@ class UFieldReading internal constructor( return (transformer as UExprTransformer).transform(this) } - override fun toString(): String = "$address.${region.regionId.field}" + override fun toString(): String = "$address.${region.field}" override fun internEquals(other: Any): Boolean = structurallyEqual(other, { region }, { address }) @@ -156,7 +155,7 @@ class UAllocatedArrayReading internal constructor( override fun internHashCode(): Int = hash(region, index) - override fun toString(): String = "0x${region.regionId.address}[$index]" + override fun toString(): String = "0x${region.allocatedAddress}[$index]" } class UInputArrayReading internal constructor( @@ -260,3 +259,10 @@ class UIsExpr internal constructor( override fun internHashCode(): Int = hash(ref, type) } //endregion + +//region Utils + +val UBoolExpr.isFalse get() = this === ctx.falseExpr +val UBoolExpr.isTrue get() = !isFalse + +//endregion \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/Heap.kt b/usvm-core/src/main/kotlin/org/usvm/Heap.kt index 4521a56647..db3964c9a7 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Heap.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Heap.kt @@ -1,17 +1,22 @@ package org.usvm -import org.ksmt.solver.KModel -import org.ksmt.utils.asExpr import kotlinx.collections.immutable.PersistentMap import kotlinx.collections.immutable.persistentMapOf +import org.ksmt.solver.KModel +import org.ksmt.utils.asExpr -interface UReadOnlyHeap { +interface UReadOnlyHeap { fun readField(ref: Ref, field: Field, sort: Sort): Value fun readArrayIndex(ref: Ref, index: SizeT, arrayType: ArrayType, elementSort: Sort): Value fun readArrayLength(ref: Ref, arrayType: ArrayType): SizeT + + /** + * Returns a copy of the current map to be able to modify it without changing the original one. + */ + fun toMutableHeap(): UHeap } -typealias UReadOnlySymbolicHeap = UReadOnlyHeap, USizeExpr, Field, ArrayType> +typealias UReadOnlySymbolicHeap = UReadOnlyHeap, USizeExpr, Field, ArrayType, UBoolExpr> class UEmptyHeap(private val ctx: UContext) : UReadOnlySymbolicHeap { override fun readField(ref: UHeapRef, field: Field, sort: Sort): UExpr = @@ -26,24 +31,44 @@ class UEmptyHeap(private val ctx: UContext) : UReadOnlySymboli override fun readArrayLength(ref: UHeapRef, arrayType: ArrayType) = ctx.zeroSize + + override fun toMutableHeap(): UHeap, USizeExpr, Field, ArrayType, UBoolExpr> = URegionHeap(ctx) } -interface UHeap : UReadOnlyHeap { - fun writeField(ref: Ref, field: Field, sort: Sort, value: Value) - fun writeArrayIndex(ref: Ref, index: SizeT, type: ArrayType, elementSort: Sort, value: Value) +interface UHeap : UReadOnlyHeap { + fun writeField(ref: Ref, field: Field, sort: Sort, value: Value, guard: Guard) + fun writeArrayIndex( + ref: Ref, + index: SizeT, + type: ArrayType, + elementSort: Sort, + value: Value, + guard: Guard + ) + + fun writeArrayLength(ref: Ref, size: SizeT, arrayType: ArrayType) fun memset(ref: Ref, type: ArrayType, sort: Sort, contents: Sequence) - fun memcpy(src: Ref, dst: Ref, type: ArrayType, fromSrc: SizeT, fromDst: SizeT, length: SizeT) + fun memcpy( + srcRef: Ref, + dstRef: Ref, + type: ArrayType, + elementSort: Sort, + fromSrcIdx: SizeT, + fromDstIdx: SizeT, + toDstIdx: SizeT, + guard: Guard + ) fun allocate(): UConcreteHeapAddress fun allocateArray(count: SizeT): UConcreteHeapAddress - fun decode(model: KModel): UReadOnlyHeap + fun decode(model: KModel): UReadOnlyHeap - fun clone(): UHeap + fun clone(): UHeap } -typealias USymbolicHeap = UHeap, USizeExpr, Field, ArrayType> +typealias USymbolicHeap = UHeap, USizeExpr, Field, ArrayType, UBoolExpr> /** * Current heap address holder. Calling [freshAddress] advances counter globally. @@ -72,7 +97,7 @@ data class URegionHeap( ): UInputFieldMemoryRegion = inputFields[field].inputFieldsRegionUncheckedCast() ?: emptyInputFieldRegion(field, sort) { key, region -> - ctx.mkFieldReading(region, key) + ctx.mkInputFieldReading(region, key) } private fun allocatedArrayRegion( @@ -99,7 +124,7 @@ data class URegionHeap( ): UInputArrayLengthMemoryRegion = inputLengths[arrayType] ?: emptyArrayLengthRegion(arrayType, ctx) { ref, region -> - ctx.mkArrayLength(region, ref) + ctx.mkInputArrayLength(region, ref) } override fun readField(ref: UHeapRef, field: Field, sort: Sort): UExpr = @@ -126,17 +151,33 @@ data class URegionHeap( } // TODO: Either prohibit merging concrete and symbolic heap addresses, or fork state by ite-refs here - override fun writeField(ref: UHeapRef, field: Field, sort: Sort, value: UExpr) { + override fun writeField( + ref: UHeapRef, + field: Field, + sort: Sort, + value: UExpr, + guard: UBoolExpr + ) { + // A write operation that never succeeds + if (guard.isFalse) return + val valueToWrite = value.asExpr(sort) when (ref) { is UConcreteHeapRef -> { - allocatedFields = allocatedFields.put(Pair(ref.address, field), valueToWrite) + val key = ref.address to field + val allocatedFieldValue = if (guard.isTrue) { + valueToWrite + } else { + ctx.mkIte(guard, valueToWrite, readField(ref, field, sort)) + } + + allocatedFields = allocatedFields.put(key, allocatedFieldValue) } else -> { val oldRegion = fieldsRegion(field, sort) - val newRegion = oldRegion.write(ref, valueToWrite) + val newRegion = oldRegion.write(ref, valueToWrite, guard) inputFields = inputFields.put(field, newRegion) } } @@ -147,25 +188,40 @@ data class URegionHeap( index: USizeExpr, type: ArrayType, elementSort: Sort, - value: UExpr + value: UExpr, + guard: UBoolExpr ) { + // A write operation that never succeeds + if (guard.isFalse) return + val valueToWrite = value.asExpr(elementSort) when (ref) { is UConcreteHeapRef -> { val oldRegion = allocatedArrayRegion(type, ref.address, elementSort) - val newRegion = oldRegion.write(index, valueToWrite) + val newRegion = oldRegion.write(index, valueToWrite, guard) allocatedArrays = allocatedArrays.put(ref.address, newRegion) } else -> { val region = inputArrayRegion(type, elementSort) - val newRegion = region.write(Pair(ref, index), valueToWrite) + val newRegion = region.write(ref to index, valueToWrite, guard) inputArrays = inputArrays.put(type, newRegion) } } } + override fun writeArrayLength(ref: UHeapRef, size: USizeExpr, arrayType: ArrayType) { + when (ref) { + is UConcreteHeapRef -> allocatedLengths = allocatedLengths.put(ref.address, size) + else -> { + val region = inputArrayLengthRegion(arrayType) + val newRegion = region.write(ref, size, ctx.trueExpr) + inputLengths = inputLengths.put(arrayType, newRegion) + } + } + } + override fun memset( ref: UHeapRef, type: ArrayType, @@ -175,15 +231,67 @@ data class URegionHeap( TODO("Not yet implemented") } - override fun memcpy( - src: UHeapRef, - dst: UHeapRef, + override fun memcpy( + srcRef: UHeapRef, + dstRef: UHeapRef, type: ArrayType, - fromSrc: USizeExpr, - fromDst: USizeExpr, - length: USizeExpr + elementSort: Sort, + fromSrcIdx: USizeExpr, + fromDstIdx: USizeExpr, + toDstIdx: USizeExpr, + guard: UBoolExpr ) { - TODO() + // A copy operation that never succeeds + if (guard.isFalse) return + + val src = srcRef to fromSrcIdx + val dst = dstRef to fromDstIdx + + when (srcRef) { + is UConcreteHeapRef -> { + val srcRegion = allocatedArrayRegion(type, srcRef.address, elementSort) + + when (dstRef) { + is UConcreteHeapRef -> { + val dstRegion = allocatedArrayRegion(type, dstRef.address, elementSort) + val keyConverter = UAllocatedToAllocatedKeyConverter(src, dst, toDstIdx) + val newDstRegion = dstRegion.memcpy(srcRegion, fromDstIdx, toDstIdx, keyConverter, guard) + allocatedArrays = allocatedArrays.put(dstRef.address, newDstRegion) + } + + is UIteExpr -> TODO() + else -> { + val dstRegion = inputArrayRegion(type, elementSort) + val keyConverter = UAllocatedToInputKeyConverter(src, dst, toDstIdx) + val newDstRegion = dstRegion.memcpy(srcRegion, dst, dstRef to toDstIdx, keyConverter, guard) + inputArrays = inputArrays.put(type, newDstRegion) + } + } + } + + is UIteExpr -> TODO() + + else -> { + val srcRegion = inputArrayRegion(type, elementSort) + + when (dstRef) { + is UConcreteHeapRef -> { + val dstRegion = allocatedArrayRegion(type, dstRef.address, elementSort) + val keyConverter = UInputToAllocatedKeyConverter(src, dst, toDstIdx) + val newDstRegion = dstRegion.memcpy(srcRegion, fromDstIdx, toDstIdx, keyConverter, guard) + allocatedArrays = allocatedArrays.put(dstRef.address, newDstRegion) + } + + is UIteExpr -> TODO() + else -> { + val dstRegion = inputArrayRegion(type, elementSort) + val keyConverter = UInputToInputKeyConverter(src, dst, toDstIdx) + val newDstRegion = dstRegion.memcpy(srcRegion, dst, dstRef to toDstIdx, keyConverter, guard) + inputArrays = inputArrays.put(type, newDstRegion) + } + } + } + } } override fun allocate() = lastAddress.freshAddress() @@ -198,13 +306,15 @@ data class URegionHeap( TODO("Not yet implemented") } - override fun clone(): UHeap, USizeExpr, Field, ArrayType> = + override fun clone(): UHeap, USizeExpr, Field, ArrayType, UBoolExpr> = URegionHeap( ctx, lastAddress, allocatedFields, inputFields, allocatedArrays, inputArrays, allocatedLengths, inputLengths ) + + override fun toMutableHeap() = clone() } @Suppress("UNCHECKED_CAST") @@ -217,4 +327,4 @@ fun UAllocatedArrayMemoryRegion?.allocat @Suppress("UNCHECKED_CAST") fun UInputArrayMemoryRegion?.inputArrayRegionUncheckedCast(): UInputArrayMemoryRegion? = - this as? UInputArrayMemoryRegion \ No newline at end of file + this as? UInputArrayMemoryRegion diff --git a/usvm-core/src/main/kotlin/org/usvm/Memory.kt b/usvm-core/src/main/kotlin/org/usvm/Memory.kt index 58924c338a..34553938c6 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Memory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Memory.kt @@ -37,18 +37,19 @@ interface UMemory { * to range of elements [[fromDst]:[fromDst] + [length] - 1] of array with address [dst]. * Both arrays must have type [arrayType]. */ - fun memcpy(src: HeapRef, dst: HeapRef, arrayType: Type, fromSrc: SizeT, fromDst: SizeT, length: SizeT) + fun memcpy(src: HeapRef, dst: HeapRef, arrayType: Type, elementSort: USort, fromSrc: SizeT, fromDst: SizeT, length: SizeT) /** * Returns length of an array */ fun length(ref: HeapRef, arrayType: Type): SizeT - fun compose(expr: UExpr): UExpr + fun compose(expr: UExpr): UExpr /** * Creates new instance of program memory. - * @warning: symbolic engine may use this operation potentially large amount of times. + * + * **Warning**: symbolic engine may use this operation potentially large number of times. * Implementation must use persistent data structures to speed it up. */ fun clone(): UMemory @@ -56,6 +57,7 @@ interface UMemory { typealias USymbolicMemory = UMemory, USizeExpr, UHeapRef, Type> +@Suppress("MemberVisibilityCanBePrivate") open class UMemoryBase( protected val ctx: UContext, protected val typeSystem: UTypeSystem, @@ -64,25 +66,27 @@ open class UMemoryBase( protected var types: UTypeStorage = UTypeStorage(ctx, typeSystem), protected var mocker: UMocker = UIndexedMocker(ctx) // TODO: we can eliminate mocker by moving compose to UState? -) - : USymbolicMemory -{ +) : USymbolicMemory { @Suppress("UNCHECKED_CAST") - override fun read(lvalue: ULValue): UExpr = - when(lvalue) { - is URegisterRef -> stack.readRegister(lvalue.idx, lvalue.sort) - is UFieldRef<*> -> heap.readField(lvalue.ref, lvalue.field as Field, lvalue.sort).asExpr(lvalue.sort) - is UArrayIndexRef<*> -> heap.readArrayIndex(lvalue.ref, lvalue.index, lvalue.arrayType as Type, lvalue.sort).asExpr(lvalue.sort) - else -> throw IllegalArgumentException("Unexpected lvalue $lvalue") + override fun read(lvalue: ULValue): UExpr = with(lvalue) { + when (this) { + is URegisterRef -> stack.readRegister(idx, sort) + is UFieldRef<*> -> heap.readField(ref, field as Field, sort).asExpr(sort) + is UArrayIndexRef<*> -> heap.readArrayIndex(ref, index, arrayType as Type, sort).asExpr(sort) + + else -> throw IllegalArgumentException("Unexpected lvalue $this") } + } @Suppress("UNCHECKED_CAST") - override fun write(lvalue: ULValue, rvalue: UExpr) { - when(lvalue) { - is URegisterRef -> stack.writeRegister(lvalue.idx, rvalue) - is UFieldRef<*> -> heap.writeField(lvalue.ref, lvalue.field as Field, lvalue.sort, rvalue) - is UArrayIndexRef<*> -> heap.writeArrayIndex(lvalue.ref, lvalue.index, lvalue.arrayType as Type, lvalue.sort, rvalue) - else -> throw IllegalArgumentException("Unexpected lvalue $lvalue") + override fun write(lvalue: ULValue, rvalue: UExpr) = with(lvalue) { + when (this) { + is URegisterRef -> stack.writeRegister(idx, rvalue) + is UFieldRef<*> -> heap.writeField(ref, field as Field, sort, rvalue, guard = ctx.trueExpr) + is UArrayIndexRef<*> -> { + heap.writeArrayIndex(ref, index, arrayType as Type, sort, rvalue, guard = ctx.trueExpr) + } + else -> throw IllegalArgumentException("Unexpected lvalue $this") } } @@ -101,13 +105,17 @@ open class UMemoryBase( override fun memset(ref: UHeapRef, arrayType: Type, elementSort: USort, contents: Sequence>) = heap.memset(ref, arrayType, elementSort, contents) - override fun memcpy(src: UHeapRef, dst: UHeapRef, arrayType: Type, - fromSrc: USizeExpr, fromDst: USizeExpr, length: USizeExpr) = - heap.memcpy(src, dst, arrayType, fromSrc, fromDst, length) + override fun memcpy( + src: UHeapRef, dst: UHeapRef, arrayType: Type, elementSort: USort, + fromSrc: USizeExpr, fromDst: USizeExpr, length: USizeExpr + ) = with(src.ctx) { + val toDst = mkBvAddExpr(fromDst, length) + heap.memcpy(src, dst, arrayType, elementSort, fromSrc, fromDst, toDst, guard = trueExpr) + } override fun length(ref: UHeapRef, arrayType: Type): USizeExpr = heap.readArrayLength(ref, arrayType) - override fun compose(expr: UExpr): UExpr { + override fun compose(expr: UExpr): UExpr { val composer = UComposer(ctx, stack, heap, types, mocker) return composer.compose(expr) } diff --git a/usvm-core/src/main/kotlin/org/usvm/MemoryRegions.kt b/usvm-core/src/main/kotlin/org/usvm/MemoryRegions.kt index 4a3d6660ab..2f12cc81c7 100644 --- a/usvm-core/src/main/kotlin/org/usvm/MemoryRegions.kt +++ b/usvm-core/src/main/kotlin/org/usvm/MemoryRegions.kt @@ -1,97 +1,16 @@ package org.usvm -import org.usvm.util.Region -import org.usvm.util.RegionTree import org.usvm.util.SetRegion import org.usvm.util.emptyRegionTree -import java.util.LinkedList -import java.util.NoSuchElementException +import java.util.* //region Memory region -/** - * Represents the result of memory write operation. - */ -interface UUpdateNode { - /** - * @returns True if the address [key] got overwritten by this write operation in *any* possible concrete state. - */ - fun includesConcretely(key: Key): Boolean - - /** - * @return Symbolic condition expressing that the address [key] got overwritten by this memory write operation. - * If [includesConcretely] returns true, then this method is obligated to return [UTrue]. - * Returned condition must imply [guard]. - */ - fun includesSymbolically(key: Key): UBoolExpr - - /** - * @see [UMemoryRegion.split] - */ - fun split( - key: Key, - predicate: (UExpr) -> Boolean, - matchingWrites: LinkedList>>, - guardBuilder: GuardBuilder - ): UUpdateNode? - - /** - * @return Value which has been written into the address [key] during this memory write operation. - */ - fun value(key: Key): UExpr - - /** - * Guard is a symbolic condition for this update. That is, this update is done only in states satisfying this guard. - */ - val guard: UBoolExpr - - /** - * Returns node with updated [guard] condition. - */ - fun guardWith(guard: UBoolExpr): UUpdateNode -} /** - * Represents a sequence of memory writes. + * A typealias for a lambda that takes a key, a region and returns a reading from the region by the key. */ -interface UMemoryUpdates : Sequence> { - /** - * @return Relevant updates for a given key - */ - fun read(key: Key): UMemoryUpdates - - /** - * @return Memory region which obtained from this one by overwriting the address [key] with value [value]. - */ - fun write(key: Key, value: UExpr): UMemoryUpdates - - /** - * @return Memory region which obtained from this one by overwriting the address [key] with value [value] - * guarded with condition [guard]. - */ - fun guardedWrite(key: Key, value: UExpr, guard: UBoolExpr): UMemoryUpdates - - /** - * @see [UMemoryRegion.split] - */ - fun split( - key: Key, - predicate: (UExpr) -> Boolean, - matchingWrites: LinkedList>>, - guardBuilder: GuardBuilder - ): UMemoryUpdates - - /** - * @return Updates expressing copying the slice of [fromRegion] (see UMemoryRegion.copy) - */ - fun copy( - fromRegion: UMemoryRegion, - fromKey: Key, toKey: Key, - keyConverter: (Key) -> Key - ): UMemoryUpdates -} - -typealias UInstantiator = (key: Key, UMemoryRegion) -> USymbol +typealias UInstantiator = (key: Key, UMemoryRegion) -> UExpr /** * A uniform unbounded slice of memory. Indexed by [Key], stores symbolic values. @@ -99,7 +18,7 @@ typealias UInstantiator = (key: Key, UMemoryRegion( +data class UMemoryRegion, Key, Sort : USort>( val regionId: RegionId, val sort: Sort, private val updates: UMemoryUpdates, @@ -107,19 +26,17 @@ data class UMemoryRegion( private val instantiator: UInstantiator ) { private fun read(key: Key, updates: UMemoryUpdates): UExpr { - val iterator = updates.iterator() + val lastUpdatedElement = updates.lastUpdatedElementOrNull() - val hasUpdates = iterator.hasNext() - if (!hasUpdates && defaultValue != null) { + if (lastUpdatedElement == null && defaultValue != null) { // Reading from untouched array filled with defaultValue return defaultValue } - if (hasUpdates) { - val entry = iterator.next() - if (entry.includesConcretely(key)) { + if (lastUpdatedElement != null) { + if (lastUpdatedElement.includesConcretely(key)) { // The last write has overwritten the key - return entry.value(key) + return lastUpdatedElement.value(key) } } @@ -172,10 +89,10 @@ data class UMemoryRegion( return iteAcc } - fun write(key: Key, value: UExpr): UMemoryRegion { + fun write(key: Key, value: UExpr, guard: UBoolExpr): UMemoryRegion { assert(value.sort == sort) - val newUpdates = updates.write(key, value) + val newUpdates = updates.write(key, value, guard) return UMemoryRegion(regionId, sort, newUpdates, defaultValue, instantiator) } @@ -192,408 +109,75 @@ data class UMemoryRegion( val splittingUpdates = updates.read(key).split(key, predicate, matchingWrites, guardBuilder) val sizeRemainedUnchanged = matchingWrites.size == count - return if (sizeRemainedUnchanged) this else UMemoryRegion(regionId, sort, splittingUpdates, defaultValue, instantiator) - } - - /** - * @return Memory region which obtained from this one by overwriting the range of addresses [[fromKey] : [toKey]] - * with values from memory region [fromRegion] read from range - * of addresses [[keyConverter] ([fromKey]) : [keyConverter] ([toKey])] - */ - fun copy( - fromRegion: UMemoryRegion, - fromKey: Key, toKey: Key, - keyConverter: (Key) -> Key - ): UMemoryRegion { - val updatesCopy = updates.copy(fromRegion, fromKey, toKey, keyConverter) - return UMemoryRegion(regionId, sort, updatesCopy, defaultValue, instantiator) - } -} - -class GuardBuilder(var matchingUpdatesGuard: UBoolExpr, var nonMatchingUpdatesGuard: UBoolExpr) - -//endregion - -//region Flat memory updates - -/** - * Represents a single write of [value] into a memory address [key] - */ -class UPinpointUpdateNode( - val key: Key, - private val value: UExpr, - private val keyEqualityComparer: (Key, Key) -> UBoolExpr, - override val guard: UBoolExpr = value.ctx.trueExpr -) : UUpdateNode { - override fun includesConcretely(key: Key) = this.key == key && guard == guard.ctx.trueExpr - - override fun includesSymbolically(key: Key): UBoolExpr = - guard.ctx.mkAnd(keyEqualityComparer(this.key, key), guard) // TODO: use simplifying and! - - override fun value(key: Key): UExpr = this.value - - override fun split( - key: Key, - predicate: (UExpr) -> Boolean, - matchingWrites: LinkedList>>, - guardBuilder: GuardBuilder - ): UUpdateNode? { - val keyEq = keyEqualityComparer(key, this.key) - val ctx = value.ctx - val keyDiseq = ctx.mkNot(keyEq) - - if (predicate(value)) { - val guard = ctx.mkAnd(guardBuilder.nonMatchingUpdatesGuard, keyEq) - matchingWrites.add(Pair(guard, value)) - guardBuilder.matchingUpdatesGuard = ctx.mkAnd(guardBuilder.matchingUpdatesGuard, keyDiseq) - return null - } - - val hadNonMatchingUpdates = guardBuilder.nonMatchingUpdatesGuard != ctx.trueExpr - guardBuilder.nonMatchingUpdatesGuard = ctx.mkAnd(guardBuilder.nonMatchingUpdatesGuard, ctx.mkNot(keyEq)) - - return if (hadNonMatchingUpdates) this.guardWith(guardBuilder.matchingUpdatesGuard) else this - } - - override fun guardWith(guard: UBoolExpr): UUpdateNode = - if (guard == guard.ctx.trueExpr) { - this - } else { - val guardExpr = guard.ctx.mkAnd(this.guard, guard) - UPinpointUpdateNode(key, value, keyEqualityComparer, guardExpr) - } - - override fun equals(other: Any?): Boolean = - other is UPinpointUpdateNode<*, *> && this.key == other.key // Ignores value - - override fun hashCode(): Int = key.hashCode() // Ignores value - - override fun toString(): String = "{$key <- $value}" -} - -/** - * Represents a synchronous overwriting the range of addresses [[fromKey] : [toKey]] - * with values from memory region [region] read from range - * of addresses [[keyConverter] ([fromKey]) : [keyConverter] ([toKey])] - */ -class URangedUpdateNode( - val fromKey: Key, - val toKey: Key, - private val region: UMemoryRegion<*, Key, ValueSort>, - private val concreteComparer: (Key, Key) -> Boolean, - private val symbolicComparer: (Key, Key) -> UBoolExpr, - private val keyConverter: (Key) -> Key, - override val guard: UBoolExpr = region.sort.ctx.trueExpr -) : UUpdateNode { - override fun includesConcretely(key: Key): Boolean = - concreteComparer(fromKey, key) && concreteComparer(key, toKey) && guard == guard.ctx.trueExpr - - override fun includesSymbolically(key: Key): UBoolExpr { - val leftIsLefter = symbolicComparer(fromKey, key) - val rightIsRighter = symbolicComparer(key, toKey) - val ctx = leftIsLefter.ctx - - return ctx.mkAnd(leftIsLefter, rightIsRighter, guard) // TODO: use simplifying and! - } - - override fun value(key: Key): UExpr = region.read(keyConverter(key)) - - override fun guardWith(guard: UBoolExpr): UUpdateNode = - if (guard == guard.ctx.trueExpr) { - this - } else { - val guardExpr = guard.ctx.mkAnd(this.guard, guard) - URangedUpdateNode(fromKey, toKey, region, concreteComparer, symbolicComparer, keyConverter, guardExpr) - } - - override fun equals(other: Any?): Boolean = - other is URangedUpdateNode<*, *> && this.fromKey == other.fromKey && this.toKey == other.toKey // Ignores update - - override fun hashCode(): Int = 31 * fromKey.hashCode() + toKey.hashCode() // Ignores update - - override fun split( - key: Key, predicate: (UExpr) -> Boolean, - matchingWrites: LinkedList>>, - guardBuilder: GuardBuilder - ): UUpdateNode { - val splittedRegion = region.split(key, predicate, matchingWrites, guardBuilder) - if (splittedRegion === region) { + if (sizeRemainedUnchanged) { return this } - return URangedUpdateNode(fromKey, toKey, splittedRegion, concreteComparer, symbolicComparer, keyConverter) - } -} - -class UEmptyUpdates( - private val symbolicEq: (Key, Key) -> UBoolExpr, - private val concreteCmp: (Key, Key) -> Boolean, - private val symbolicCmp: (Key, Key) -> UBoolExpr -) : UMemoryUpdates { - override fun read(key: Key): UMemoryUpdates = this - - override fun write(key: Key, value: UExpr): UMemoryUpdates = - UFlatUpdates( - UPinpointUpdateNode(key, value, symbolicEq), - next = null, - symbolicEq, - concreteCmp, - symbolicCmp - ) - - override fun guardedWrite(key: Key, value: UExpr, guard: UBoolExpr): UMemoryUpdates = - UFlatUpdates( - UPinpointUpdateNode(key, value, symbolicEq, guard), - next = null, - symbolicEq, - concreteCmp, - symbolicCmp - ) - - override fun copy( - fromRegion: UMemoryRegion, - fromKey: Key, - toKey: Key, - keyConverter: (Key) -> Key, - ) = UFlatUpdates( - URangedUpdateNode(fromKey, toKey, fromRegion, concreteCmp, symbolicCmp, keyConverter), - next = null, - symbolicEq, - concreteCmp, - symbolicCmp - ) - - override fun split( - key: Key, - predicate: (UExpr) -> Boolean, - matchingWrites: LinkedList>>, - guardBuilder: GuardBuilder - ) = this - - override fun iterator(): Iterator> = EmptyIterator() - - private class EmptyIterator : Iterator> { - override fun hasNext(): Boolean = false - override fun next(): UUpdateNode = error("Advancing empty iterator") - } -} - -data class UFlatUpdates( - val node: UUpdateNode, - val next: UMemoryUpdates?, - private val symbolicEq: (Key, Key) -> UBoolExpr, - private val concreteCmp: (Key, Key) -> Boolean, - private val symbolicCmp: (Key, Key) -> UBoolExpr -) : UMemoryUpdates { - override fun read(key: Key): UMemoryUpdates = this - - override fun write(key: Key, value: UExpr): UMemoryUpdates = - UFlatUpdates( - UPinpointUpdateNode(key, value, symbolicEq), - next = this, - symbolicEq, - concreteCmp, - symbolicCmp - ) - - override fun guardedWrite(key: Key, value: UExpr, guard: UBoolExpr): UMemoryUpdates = - UFlatUpdates( - UPinpointUpdateNode(key, value, symbolicEq, guard), - next = this, - symbolicEq, - concreteCmp, - symbolicCmp - ) - - override fun copy( - fromRegion: UMemoryRegion, - fromKey: Key, - toKey: Key, - keyConverter: (Key) -> Key, - ) = UFlatUpdates( - URangedUpdateNode(fromKey, toKey, fromRegion, concreteCmp, symbolicCmp, keyConverter), - next = this, - symbolicEq, - concreteCmp, - symbolicCmp - ) - - override fun split( - key: Key, predicate: (UExpr) -> Boolean, - matchingWrites: LinkedList>>, - guardBuilder: GuardBuilder - ): UMemoryUpdates { - val splittingNode = node.split(key, predicate, matchingWrites, guardBuilder) - val splittingNext = next?.split(key, predicate, matchingWrites, guardBuilder) - - if (splittingNode == null) { - return splittingNext ?: UEmptyUpdates(symbolicEq, concreteCmp, symbolicCmp) - } - - if (splittingNext === next) { - return this - } - - return UFlatUpdates(splittingNode, splittingNext, symbolicEq, concreteCmp, symbolicCmp) + return UMemoryRegion(regionId, sort, splittingUpdates, defaultValue, instantiator) } /** - * Returns updates in the FIFO order: the iterator emits updates from the oldest updates to the most recent one. - * It means that the `initialNode` from the [UFlatUpdatesIterator] will be returned as the last element. + * Maps the region using [composer]. + * It is used in [UComposer] for composition operation. + * + * Note: after this operation a region returned as a result might be in `broken` state: + * it might have both symbolic and concrete values as keys in it. */ - override fun iterator(): Iterator> = UFlatUpdatesIterator(initialNode = this) - - private class UFlatUpdatesIterator( - initialNode: UFlatUpdates, - ) : Iterator> { - private val iterator: Iterator> - - init { - val elements = mutableListOf>() - var current: UFlatUpdates? = initialNode - - // Traverse over linked list of updates nodes and extract them into an array list - while (current != null) { - elements += current.node - // We can safely apply `as?` since we are interested only in non-empty updates - // and there are no `treeUpdates` as a `next` element of the `UFlatUpdates` - current = current.next as? UFlatUpdates - } - - iterator = elements.asReversed().iterator() - } - - override fun hasNext(): Boolean = iterator.hasNext() - - override fun next(): UUpdateNode = iterator.next() - } -} - -//endregion + fun map( + composer: UComposer, + instantiator: UInstantiator = this.instantiator + ): UMemoryRegion { + // Map the updates and the default value + val mappedUpdates = updates.map(regionId.keyMapper(composer), composer) + val mappedDefaultValue = defaultValue?.let { composer.compose(it) } -//region Tree memory updates - -data class UTreeUpdates, Sort : USort>( - private val updates: RegionTree, Reg>, - private val keyToRegion: (Key) -> Reg, - private val keyRangeToRegion: (Key, Key) -> Reg, - private val symbolicEq: (Key, Key) -> UBoolExpr, - private val concreteCmp: (Key, Key) -> Boolean, - private val symbolicCmp: (Key, Key) -> UBoolExpr -) : UMemoryUpdates { - override fun read(key: Key): UTreeUpdates { - val reg = keyToRegion(key) - val updates = updates.localize(reg) - if (updates === this.updates) { + // If there is no changes after their composition, return unchecked region + if (mappedUpdates === updates && mappedDefaultValue === defaultValue) { return this } - return UTreeUpdates(updates, keyToRegion, keyRangeToRegion, symbolicEq, concreteCmp, symbolicCmp) + // Otherwise, construct a new region with mapped values and a new instantiator. + return UMemoryRegion(regionId, sort, mappedUpdates, mappedDefaultValue, instantiator) } - override fun write(key: Key, value: UExpr): UTreeUpdates { - val update = UPinpointUpdateNode(key, value, symbolicEq) - val newUpdates = updates.write(keyToRegion(key), update, keyFilter = { it == key }) - - return UTreeUpdates(newUpdates, keyToRegion, keyRangeToRegion, symbolicEq, concreteCmp, symbolicCmp) - } - - override fun guardedWrite(key: Key, value: UExpr, guard: UBoolExpr): UTreeUpdates { - val update = UPinpointUpdateNode(key, value, symbolicEq, guard) - val newUpdates = updates.write(keyToRegion(key), update, keyFilter = { it == key }) - - return UTreeUpdates(newUpdates, keyToRegion, keyRangeToRegion, symbolicEq, concreteCmp, symbolicCmp) - } - - override fun copy( - fromRegion: UMemoryRegion, - fromKey: Key, - toKey: Key, - keyConverter: (Key) -> Key - ): UTreeUpdates { - val region = keyRangeToRegion(fromKey, toKey) - val update = URangedUpdateNode(fromKey, toKey, fromRegion, concreteCmp, symbolicCmp, keyConverter) - val newUpdates = updates.write(region, update, keyFilter = { it == update }) - - return UTreeUpdates(newUpdates, keyToRegion, keyRangeToRegion, symbolicEq, concreteCmp, symbolicCmp) - } - - override fun split( - key: Key, - predicate: (UExpr) -> Boolean, - matchingWrites: LinkedList>>, - guardBuilder: GuardBuilder - ): UMemoryUpdates { - TODO("Not yet implemented") - } - - /** - * Returns updates in the FIFO order: the iterator emits updates from the oldest updates to the most recent one. - * Note that if some key in the tree is presented in more than one node, it will be returned exactly ones. - */ - override fun iterator(): Iterator> = TreeIterator(updates.iterator()) - - override fun toString(): String { - return "$updates" - } - - private inner class TreeIterator( - private val treeUpdatesIterator: Iterator, Reg>> - ) : Iterator> { - // A set of values we already emitted by this iterator. - // Note that it contains ONLY elements that have duplicates by key in the RegionTree. - private val emittedUpdates = hashSetOf>() - - // We can return just `hasNext` value without checking for duplicates since - // the last node contains a unique key (because non-unique keys might occur only - // as a result of splitting because of some other write operation). - override fun hasNext(): Boolean = treeUpdatesIterator.hasNext() - - override fun next(): UUpdateNode { - while (treeUpdatesIterator.hasNext()) { - val (update, region) = treeUpdatesIterator.next() - - // To check, whether we have a duplicate for a particular key, - // we have to check if an initial region (by USVM estimation) is equal - // to the one stored in the current node. - val initialRegion = when (update) { - is UPinpointUpdateNode -> keyToRegion(update.key) - is URangedUpdateNode -> keyRangeToRegion(update.fromKey, update.toKey) - else -> error("An unsupported type of UpdateNode is provided: ${update::class}") + @Suppress("UNCHECKED_CAST") + fun applyTo(heap: USymbolicHeap) { + // Apply each update on the copy + updates.forEach { + when (it) { + is UPinpointUpdateNode -> regionId.write(it.key, sort, heap, it.value, it.guard) + is URangedUpdateNode<*, *, *, Key, Sort> -> { + it.region.applyTo(heap) + + val (srcFromRef, srcFromIdx) = it.keyConverter.srcSymbolicArrayIndex + val (dstFromRef, dstFromIdx) = it.keyConverter.dstFromSymbolicArrayIndex + val dstTo = it.keyConverter.dstToIndex + val arrayType = it.region.regionId.arrayType as Type + + heap.memcpy(srcFromRef, dstFromRef, arrayType, sort, srcFromIdx, dstFromIdx, dstTo, it.guard) } - val wasCloned = initialRegion != region - - // If a region from the current node is equal to the initial region, - // it means that there were no write operation that caused nodes split, - // and the node doesn't have `duplicates` in the tree. - if (!wasCloned) { - return update - } - - // If there are duplicates, we have to emit exactly one of them -- the first we encountered. - // Otherwise, we might have a problem. For example, we write by key `j` that belongs to {1, 2} region. - // Then we wrote 1 with region {1} and 2 with region {2}. We have the following tree: - // ({1} -> (1, {1} -> j), {2} -> (2, {2} -> j)). Without any additional actions, its iterator - // will emit the following values: (j, 1, j, 2). We don't want to deal with their region - // during encoding, so, we want to go through this sequence and apply updates, but we cannot do it. - // We write by key `j`, then by `1`, then again by `j`, which overwrites a more recent update - // in the region {1} and causes the following memory: [j, 2] instead of [1, 2]. - if (update in emittedUpdates) { - continue - } - - emittedUpdates += update - - return update } - - throw NoSuchElementException() } } - + /** + * @return Memory region which obtained from this one by overwriting the range of addresses [[fromKey] : [toKey]] + * with values from memory region [fromRegion] read from range + * of addresses [[keyConverter].convert([fromKey]) : [keyConverter].convert([toKey])] + */ + fun , SrcKey> memcpy( + fromRegion: UMemoryRegion, + fromKey: Key, toKey: Key, + keyConverter: UMemoryKeyConverter, + guard: UBoolExpr + ): UMemoryRegion { + val updatesCopy = updates.copyRange(fromRegion, fromKey, toKey, keyConverter, guard) + return UMemoryRegion(regionId, sort, updatesCopy, defaultValue, instantiator) + } } +class GuardBuilder(var matchingUpdatesGuard: UBoolExpr, var nonMatchingUpdatesGuard: UBoolExpr) + //endregion //region Instantiations @@ -659,43 +243,26 @@ fun refIndexRangeRegion( idx2: USymbolicArrayIndex ): UArrayIndexRegion = indexRangeRegion(idx1.second, idx2.second) -data class UInputFieldRegionId internal constructor( - val field: Field -) - -data class UAllocatedArrayId internal constructor( - val arrayType: ArrayType, - val address: UConcreteHeapAddress, -) { - // we don't include arrayType into hashcode and equals, because [address] already defines unambiguously - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UAllocatedArrayId<*> - - if (address != other.address) return false +typealias UInputFieldMemoryRegion = UMemoryRegion, UHeapRef, Sort> +typealias UAllocatedArrayMemoryRegion = UMemoryRegion, USizeExpr, Sort> +typealias UInputArrayMemoryRegion = UMemoryRegion, USymbolicArrayIndex, Sort> +typealias UInputArrayLengthMemoryRegion = UMemoryRegion, UHeapRef, USizeSort> - return true - } +typealias KeyMapper = (Key) -> Key - override fun hashCode(): Int { - return address - } -} +val UInputFieldMemoryRegion.field + get() = regionId.field -data class UInputArrayId internal constructor( - val arrayType: ArrayType -) +val UAllocatedArrayMemoryRegion.allocatedArrayType + get() = regionId.arrayType +val UAllocatedArrayMemoryRegion.allocatedAddress + get() = regionId.address -data class UInputArrayLengthId internal constructor( - val arrayType: ArrayType -) +val UInputArrayMemoryRegion.inputArrayType + get() = regionId.arrayType -typealias UInputFieldMemoryRegion = UMemoryRegion, UHeapRef, Sort> -typealias UAllocatedArrayMemoryRegion = UMemoryRegion, USizeExpr, Sort> -typealias UInputArrayMemoryRegion = UMemoryRegion, USymbolicArrayIndex, Sort> -typealias UInputArrayLengthMemoryRegion = UMemoryRegion, UHeapRef, USizeSort> +val UInputArrayLengthMemoryRegion.inputLengthArrayType + get() = regionId.arrayType fun emptyInputFieldRegion( field: Field, diff --git a/usvm-core/src/main/kotlin/org/usvm/MemoryUpdates.kt b/usvm-core/src/main/kotlin/org/usvm/MemoryUpdates.kt new file mode 100644 index 0000000000..2ad0f44beb --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/MemoryUpdates.kt @@ -0,0 +1,399 @@ +package org.usvm + +import org.usvm.util.Region +import org.usvm.util.RegionTree +import org.usvm.util.emptyRegionTree +import java.util.* + +/** + * Represents a sequence of memory writes. + */ +interface UMemoryUpdates : Sequence> { + /** + * @return Relevant updates for a given key + */ + fun read(key: Key): UMemoryUpdates + + /** + * @return Memory region which obtained from this one by overwriting the address [key] with value [value] + * guarded with condition [guard]. + */ + fun write(key: Key, value: UExpr, guard: UBoolExpr): UMemoryUpdates + + /** + * @see [UMemoryRegion.split] + */ + fun split( + key: Key, + predicate: (UExpr) -> Boolean, + matchingWrites: LinkedList>>, + guardBuilder: GuardBuilder + ): UMemoryUpdates + + /** + * Returns a mapped [UMemoryRegion] using [keyMapper] and [composer]. + * It is used in [UComposer] during memory composition. + */ + fun map(keyMapper: KeyMapper, composer: UComposer): UMemoryUpdates + + /** + * @return Updates expressing copying the slice of [fromRegion] (see UMemoryRegion.copy) + */ + fun , SrcKey> copyRange( + fromRegion: UMemoryRegion, + fromKey: Key, + toKey: Key, + keyConverter: UMemoryKeyConverter, + guard: UBoolExpr + ): UMemoryUpdates + + /** + * Returns the last updated element if there were any updates or null otherwise. + * + * Note: this operation might significantly affect performance, it should be implemented + * considering that it will be called very often. + */ + fun lastUpdatedElementOrNull(): UUpdateNode? + + /** + * Returns true if there were any updates and false otherwise. + */ + fun isEmpty(): Boolean +} + + +//region Flat memory updates + +class UEmptyUpdates( + private val symbolicEq: (Key, Key) -> UBoolExpr, + private val concreteCmp: (Key, Key) -> Boolean, + private val symbolicCmp: (Key, Key) -> UBoolExpr +) : UMemoryUpdates { + override fun read(key: Key): UEmptyUpdates = this + + override fun write(key: Key, value: UExpr, guard: UBoolExpr): UFlatUpdates = + UFlatUpdates( + UPinpointUpdateNode(key, value, symbolicEq, guard), + next = null, + symbolicEq, + concreteCmp, + symbolicCmp + ) + + override fun , SrcKey> copyRange( + fromRegion: UMemoryRegion, + fromKey: Key, + toKey: Key, + keyConverter: UMemoryKeyConverter, + guard: UBoolExpr + ): UFlatUpdates = UFlatUpdates( + URangedUpdateNode(fromKey, toKey, fromRegion, concreteCmp, symbolicCmp, keyConverter, guard), + next = null, + symbolicEq, + concreteCmp, + symbolicCmp + ) + + override fun split( + key: Key, + predicate: (UExpr) -> Boolean, + matchingWrites: LinkedList>>, + guardBuilder: GuardBuilder + ): UEmptyUpdates = this + + override fun map( + keyMapper: KeyMapper, + composer: UComposer + ): UEmptyUpdates = this + + override fun iterator(): Iterator> = EmptyIterator() + + private class EmptyIterator : Iterator> { + override fun hasNext(): Boolean = false + override fun next(): UUpdateNode = error("Advancing empty iterator") + } + + override fun lastUpdatedElementOrNull(): UUpdateNode? = null + + override fun isEmpty(): Boolean = true +} + +data class UFlatUpdates( + val node: UUpdateNode, + val next: UMemoryUpdates?, + private val symbolicEq: (Key, Key) -> UBoolExpr, + private val concreteCmp: (Key, Key) -> Boolean, + private val symbolicCmp: (Key, Key) -> UBoolExpr +) : UMemoryUpdates { + override fun read(key: Key): UMemoryUpdates = this + + override fun write(key: Key, value: UExpr, guard: UBoolExpr): UFlatUpdates = + UFlatUpdates( + UPinpointUpdateNode(key, value, symbolicEq, guard), + next = this, + symbolicEq, + concreteCmp, + symbolicCmp + ) + + override fun , SrcKey> copyRange( + fromRegion: UMemoryRegion, + fromKey: Key, + toKey: Key, + keyConverter: UMemoryKeyConverter, + guard: UBoolExpr + ): UMemoryUpdates = UFlatUpdates( + URangedUpdateNode(fromKey, toKey, fromRegion, concreteCmp, symbolicCmp, keyConverter, guard), + next = this, + symbolicEq, + concreteCmp, + symbolicCmp + ) + + override fun split( + key: Key, predicate: (UExpr) -> Boolean, + matchingWrites: LinkedList>>, + guardBuilder: GuardBuilder + ): UMemoryUpdates { + val splittingNode = node.split(key, predicate, matchingWrites, guardBuilder) + val splittingNext = next?.split(key, predicate, matchingWrites, guardBuilder) + + if (splittingNode == null) { + return splittingNext ?: UEmptyUpdates(symbolicEq, concreteCmp, symbolicCmp) + } + + if (splittingNext === next) { + return this + } + + return UFlatUpdates(splittingNode, splittingNext, symbolicEq, concreteCmp, symbolicCmp) + } + + override fun map( + keyMapper: KeyMapper, + composer: UComposer + ): UFlatUpdates { + // Map the current node and the next values recursively + val mappedNode = node.map(keyMapper, composer) + val mappedNext = next?.map(keyMapper, composer) + + // If nothing changed, return this updates + if (mappedNode === node && mappedNext === next) { + return this + } + + // Otherwise, construct a new one using the mapped values + return UFlatUpdates(mappedNode, mappedNext, symbolicEq, concreteCmp, symbolicCmp) + } + + /** + * Returns updates in the FIFO order: the iterator emits updates from the oldest updates to the most recent one. + * It means that the `initialNode` from the [UFlatUpdatesIterator] will be returned as the last element. + */ + override fun iterator(): Iterator> = UFlatUpdatesIterator(initialNode = this) + + private class UFlatUpdatesIterator( + initialNode: UFlatUpdates, + ) : Iterator> { + private val iterator: Iterator> + + init { + val elements = mutableListOf>() + var current: UFlatUpdates? = initialNode + + // Traverse over linked list of updates nodes and extract them into an array list + while (current != null) { + elements += current.node + // We can safely apply `as?` since we are interested only in non-empty updates + // and there are no `treeUpdates` as a `next` element of the `UFlatUpdates` + current = current.next as? UFlatUpdates + } + + iterator = elements.asReversed().iterator() + } + + override fun hasNext(): Boolean = iterator.hasNext() + + override fun next(): UUpdateNode = iterator.next() + } + + override fun lastUpdatedElementOrNull(): UUpdateNode = node + + override fun isEmpty(): Boolean = false +} + +//endregion + +//region Tree memory updates + +data class UTreeUpdates, Sort : USort>( + private val updates: RegionTree, Reg>, + private val keyToRegion: (Key) -> Reg, + private val keyRangeToRegion: (Key, Key) -> Reg, + private val symbolicEq: (Key, Key) -> UBoolExpr, + private val concreteCmp: (Key, Key) -> Boolean, + private val symbolicCmp: (Key, Key) -> UBoolExpr +) : UMemoryUpdates { + override fun read(key: Key): UTreeUpdates { + val reg = keyToRegion(key) + val updates = updates.localize(reg) + if (updates === this.updates) { + return this + } + + return UTreeUpdates(updates, keyToRegion, keyRangeToRegion, symbolicEq, concreteCmp, symbolicCmp) + } + + override fun write(key: Key, value: UExpr, guard: UBoolExpr): UTreeUpdates { + val update = UPinpointUpdateNode(key, value, symbolicEq, guard) + val region = keyToRegion(key) + + val newUpdates = updates.write(region, update, keyFilter = { it == update }) + + return UTreeUpdates(newUpdates, keyToRegion, keyRangeToRegion, symbolicEq, concreteCmp, symbolicCmp) + } + + override fun , SrcKey> copyRange( + fromRegion: UMemoryRegion, + fromKey: Key, + toKey: Key, + keyConverter: UMemoryKeyConverter, + guard: UBoolExpr + ): UMemoryUpdates { + val region = keyRangeToRegion(fromKey, toKey) + val update = URangedUpdateNode(fromKey, toKey, fromRegion, concreteCmp, symbolicCmp, keyConverter, guard) + val newUpdates = updates.write(region, update, keyFilter = { it == update }) + + return UTreeUpdates(newUpdates, keyToRegion, keyRangeToRegion, symbolicEq, concreteCmp, symbolicCmp) + } + + override fun split( + key: Key, + predicate: (UExpr) -> Boolean, + matchingWrites: LinkedList>>, + guardBuilder: GuardBuilder + ): UMemoryUpdates { + TODO("Not yet implemented") + } + + override fun map( + keyMapper: KeyMapper, + composer: UComposer + ): UTreeUpdates { + var mappedNodeFound = false + + // Traverse [updates] using its iterator and fold them into a new updates tree with new mapped nodes + val initialEmptyTree = emptyRegionTree, Reg>() + val mappedUpdates = updates.fold(initialEmptyTree) { mappedUpdatesTree, updateNodeWithRegion -> + val (updateNode, oldRegion) = updateNodeWithRegion + // Map current node + val mappedUpdateNode = updateNode.map(keyMapper, composer) + + // Save information about whether something changed in the current node or not + if (mappedUpdateNode !== updateNode) { + mappedNodeFound = true + } + + // Note that following code should be executed after checking for reference equality of a mapped node. + // Otherwise, it is possible that for a tree with several impossible writes + // it will be returned as a result, instead of an empty one. + + // Extract a new region by the mapped node + val newRegion = when (updateNode) { + is UPinpointUpdateNode -> { + mappedUpdateNode as UPinpointUpdateNode + val currentRegion = keyToRegion(mappedUpdateNode.key) + oldRegion.intersect(currentRegion) + } + + is URangedUpdateNode<*, *, *, Key, Sort> -> { + mappedUpdateNode as URangedUpdateNode<*, *, *, Key, Sort> + val currentRegion = keyRangeToRegion(mappedUpdateNode.fromKey, mappedUpdateNode.toKey) + oldRegion.intersect(currentRegion) + } + } + + // Ignore nodes estimated with an empty region + if (newRegion.isEmpty) { + return@fold mappedUpdatesTree + } + + // Otherwise, write the mapped node by a new region with a corresponding + // key filter for deduplication + mappedUpdatesTree.write(newRegion, mappedUpdateNode) { it == mappedUpdateNode } + } + + // If at least one node was changed, return a new updates, otherwise return this + return if (mappedNodeFound) copy(updates = mappedUpdates) else this + } + + /** + * Returns updates in the FIFO order: the iterator emits updates from the oldest updates to the most recent one. + * Note that if some key in the tree is presented in more than one node, it will be returned exactly ones. + */ + override fun iterator(): Iterator> = TreeIterator(updates.iterator()) + + override fun toString(): String { + return "$updates" + } + + private inner class TreeIterator( + private val treeUpdatesIterator: Iterator, Reg>> + ) : Iterator> { + // A set of values we already emitted by this iterator. + // Note that it contains ONLY elements that have duplicates by key in the RegionTree. + private val emittedUpdates = hashSetOf>() + + // We can return just `hasNext` value without checking for duplicates since + // the last node contains a unique key (because non-unique keys might occur only + // as a result of splitting because of some other write operation). + override fun hasNext(): Boolean = treeUpdatesIterator.hasNext() + + override fun next(): UUpdateNode { + while (treeUpdatesIterator.hasNext()) { + val (update, region) = treeUpdatesIterator.next() + + // To check, whether we have a duplicate for a particular key, + // we have to check if an initial region (by USVM estimation) is equal + // to the one stored in the current node. + val initialRegion = when (update) { + is UPinpointUpdateNode -> keyToRegion(update.key) + is URangedUpdateNode<*, *, *, Key, Sort> -> keyRangeToRegion(update.fromKey, update.toKey) + } + val wasCloned = initialRegion != region + + // If a region from the current node is equal to the initial region, + // it means that there were no write operation that caused nodes split, + // and the node doesn't have `duplicates` in the tree. + if (!wasCloned) { + return update + } + + // If there are duplicates, we have to emit exactly one of them -- the first we encountered. + // Otherwise, we might have a problem. For example, we write by key `j` that belongs to {1, 2} region. + // Then we wrote 1 with region {1} and 2 with region {2}. We have the following tree: + // ({1} -> (1, {1} -> j), {2} -> (2, {2} -> j)). Without any additional actions, its iterator + // will emit the following values: (j, 1, j, 2). We don't want to deal with their region + // during encoding, so, we want to go through this sequence and apply updates, but we cannot do it. + // We write by key `j`, then by `1`, then again by `j`, which overwrites a more recent update + // in the region {1} and causes the following memory: [j, 2] instead of [1, 2]. + if (update in emittedUpdates) { + continue + } + + emittedUpdates += update + + return update + } + + throw NoSuchElementException() + } + } + + override fun lastUpdatedElementOrNull(): UUpdateNode? = + updates.entries.entries.lastOrNull()?.value?.first + + override fun isEmpty(): Boolean = updates.entries.isEmpty() +} + +//endregion \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/RegionId.kt b/usvm-core/src/main/kotlin/org/usvm/RegionId.kt new file mode 100644 index 0000000000..1a1e96733e --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/RegionId.kt @@ -0,0 +1,168 @@ +package org.usvm + +import org.ksmt.utils.asExpr + + +/** + * An interface that represents any possible type of regions that can be used in the memory. + */ +interface URegionId { + fun read( + key: Key, + sort: Sort, + heap: UReadOnlySymbolicHeap + ): UExpr + + fun write( + key: Key, + sort: Sort, + heap: USymbolicHeap, + value: UExpr, + guard: UBoolExpr + ) + + fun keyMapper(composer: UComposer): KeyMapper +} + +/** + * A region id for a region storing the specific [field]. + */ +data class UInputFieldRegionId internal constructor( + val field: Field +) : URegionId { + @Suppress("UNCHECKED_CAST") + override fun read( + key: UHeapRef, + sort: Sort, + heap: UReadOnlySymbolicHeap + ) = heap.readField(key, field as Field, sort).asExpr(sort) + + @Suppress("UNCHECKED_CAST") + override fun write( + key: UHeapRef, + sort: Sort, + heap: USymbolicHeap, + value: UExpr, + guard: UBoolExpr + ) = heap.writeField(key, field as Field, sort, value, guard) + + override fun keyMapper( + composer: UComposer + ): KeyMapper = { composer.compose(it) } +} + +interface UArrayId : URegionId { + val arrayType: ArrayType +} + +/** + * A region id for a region storing arrays allocated during execution. + * Each identifier contains information about its [arrayType] and [address]. + */ +data class UAllocatedArrayId internal constructor( + override val arrayType: ArrayType, + val address: UConcreteHeapAddress, +) : UArrayId { + @Suppress("UNCHECKED_CAST") + override fun read( + key: USizeExpr, + sort: Sort, + heap: UReadOnlySymbolicHeap + ): UExpr { + val ref = key.uctx.mkConcreteHeapRef(address) + return heap.readArrayIndex(ref, key, arrayType as ArrayType, sort).asExpr(sort) + } + + @Suppress("UNCHECKED_CAST") + override fun write( + key: USizeExpr, + sort: Sort, + heap: USymbolicHeap, + value: UExpr, + guard: UBoolExpr + ) { + val ref = key.uctx.mkConcreteHeapRef(address) + heap.writeArrayIndex(ref, key, arrayType as ArrayType, sort, value, guard) + } + + override fun keyMapper( + composer: UComposer + ): KeyMapper = { composer.compose(it) } + + // we don't include arrayType into hashcode and equals, because [address] already defines unambiguously + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (javaClass != other?.javaClass) return false + + other as UAllocatedArrayId<*> + + if (address != other.address) return false + + return true + } + + override fun hashCode(): Int { + return address + } +} + +/** + * A region id for a region storing arrays retrieved as a symbolic value, contains only its [arrayType]. + */ +data class UInputArrayId internal constructor( + override val arrayType: ArrayType +) : UArrayId { + @Suppress("UNCHECKED_CAST") + override fun read( + key: USymbolicArrayIndex, + sort: Sort, + heap: UReadOnlySymbolicHeap + ): UExpr = heap.readArrayIndex(key.first, key.second, arrayType as ArrayType, sort).asExpr(sort) + + @Suppress("UNCHECKED_CAST") + override fun write( + key: USymbolicArrayIndex, + sort: Sort, + heap: USymbolicHeap, + value: UExpr, + guard: UBoolExpr + ) = heap.writeArrayIndex(key.first, key.second, arrayType as ArrayType, sort, value, guard) + + override fun keyMapper( + composer: UComposer + ): KeyMapper = { + val ref = composer.compose(it.first) + val idx = composer.compose(it.second) + if (ref === it.first && idx === it.second) it else ref to idx + } +} + +/** + * A region id for a region storing array lengths for arrays of a specific [arrayType]. + */ +data class UInputArrayLengthId internal constructor( + val arrayType: ArrayType +) : URegionId { + @Suppress("UNCHECKED_CAST") + override fun read( + key: UHeapRef, + sort: Sort, + heap: UReadOnlySymbolicHeap + ): UExpr = heap.readArrayLength(key, arrayType as ArrayType).asExpr(sort) + + @Suppress("UNCHECKED_CAST") + override fun write( + key: UHeapRef, + sort: Sort, + heap: USymbolicHeap, + value: UExpr, + guard: UBoolExpr + ) { + assert(guard.isTrue) + heap.writeArrayLength(key, value.asExpr(key.uctx.sizeSort), arrayType as ArrayType) + } + + override fun keyMapper( + composer: UComposer + ): KeyMapper = { composer.compose(it) } +} diff --git a/usvm-core/src/main/kotlin/org/usvm/UpdateNodes.kt b/usvm-core/src/main/kotlin/org/usvm/UpdateNodes.kt new file mode 100644 index 0000000000..1ef94266f4 --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/UpdateNodes.kt @@ -0,0 +1,329 @@ +package org.usvm + +import java.util.* + +/** + * Represents the result of memory write operation. + * + * Note that it should not be extended by external users. Otherwise, it would require + * changes in processing of such nodes inside a core since we expect to have only two implementations: + * [UPinpointUpdateNode] and [URangedUpdateNode]. + */ +sealed interface UUpdateNode { + /** + * @returns True if the address [key] got overwritten by this write operation in *any* possible concrete state. + */ + fun includesConcretely(key: Key): Boolean + + /** + * @return Symbolic condition expressing that the address [key] got overwritten by this memory write operation. + * If [includesConcretely] returns true, then this method is obligated to return [UTrue]. + */ + fun includesSymbolically(key: Key): UBoolExpr + + /** + * @see [UMemoryRegion.split] + */ + fun split( + key: Key, + predicate: (UExpr) -> Boolean, + matchingWrites: LinkedList>>, + guardBuilder: GuardBuilder + ): UUpdateNode? + + /** + * @return Value which has been written into the address [key] during this memory write operation. + */ + fun value(key: Key): UExpr + + /** + * Returns a mapped update node using [keyMapper] and [composer]. + * It is used in [UComposer] for composition. + */ + fun map(keyMapper: KeyMapper, composer: UComposer): UUpdateNode +} + +/** + * Represents a single write of [value] into a memory address [key] + */ +class UPinpointUpdateNode( + val key: Key, + internal val value: UExpr, + private val keyEqualityComparer: (Key, Key) -> UBoolExpr, + val guard: UBoolExpr = value.ctx.trueExpr +) : UUpdateNode { + override fun includesConcretely(key: Key) = this.key == key && guard == guard.ctx.trueExpr + + override fun includesSymbolically(key: Key): UBoolExpr = + guard.ctx.mkAnd(keyEqualityComparer(this.key, key), guard) // TODO: use simplifying and! + + override fun value(key: Key): UExpr = this.value + + override fun split( + key: Key, + predicate: (UExpr) -> Boolean, + matchingWrites: LinkedList>>, + guardBuilder: GuardBuilder + ): UUpdateNode? { + val keyEq = keyEqualityComparer(key, this.key) + val ctx = value.ctx + val keyDiseq = ctx.mkNot(keyEq) + + if (predicate(value)) { + val guard = ctx.mkAnd(guardBuilder.nonMatchingUpdatesGuard, keyEq) + matchingWrites.add(Pair(guard, value)) + guardBuilder.matchingUpdatesGuard = ctx.mkAnd(guardBuilder.matchingUpdatesGuard, keyDiseq) + return null + } + + guardBuilder.nonMatchingUpdatesGuard = ctx.mkAnd(guardBuilder.nonMatchingUpdatesGuard, ctx.mkNot(keyEq)) + + // TODO: @sergeypospelov: fix this split + return this + } + + override fun map( + keyMapper: KeyMapper, + composer: UComposer + ): UPinpointUpdateNode { + val mappedKey = keyMapper(key) + val mappedValue = composer.compose(value) + val mappedGuard = composer.compose(guard) + + // If nothing changed, return this value + if (mappedKey === key && mappedValue === value && mappedGuard === guard) { + return this + } + + // Otherwise, construct a new one update node + return UPinpointUpdateNode(mappedKey, mappedValue, keyEqualityComparer, mappedGuard) + } + + override fun equals(other: Any?): Boolean = + other is UPinpointUpdateNode<*, *> && this.key == other.key && this.guard == other.guard + + override fun hashCode(): Int = key.hashCode() * 31 + guard.hashCode() // Ignores value + + override fun toString(): String = "{$key <- $value}" +} + +/** + * Composable converter of memory region keys. Helps to transparently copy content of various regions + * each into other without eager address conversion. + * For instance, when we copy array slice [i : i + len] to destination memory slice [j : j + len], + * we emulate it by memorizing the source memory updates as-is, but read the destination memory by + * 'redirecting' the index k to k + j - i of the source memory. + * This conversion is done by [convert]. + * Do not be confused: it converts [DstKey] to [SrcKey] (not vice-versa), as we use it when we + * read from destination buffer index to source memory. + */ +sealed class UMemoryKeyConverter( + val srcSymbolicArrayIndex: USymbolicArrayIndex, + val dstFromSymbolicArrayIndex: USymbolicArrayIndex, + val dstToIndex: USizeExpr +) { + /** + * Converts source memory key into destination memory key + */ + abstract fun convert(key: DstKey): SrcKey + + protected fun convertIndex(idx: USizeExpr): USizeExpr = with(srcSymbolicArrayIndex.first.ctx) { + return mkBvSubExpr(mkBvAddExpr(idx, dstFromSymbolicArrayIndex.second), srcSymbolicArrayIndex.second) + } + + abstract fun clone( + srcSymbolicArrayIndex: USymbolicArrayIndex, + dstFromSymbolicArrayIndex: USymbolicArrayIndex, + dstToIndex: USizeExpr + ): UMemoryKeyConverter + + fun map(composer: UComposer): UMemoryKeyConverter { + val (srcRef, srcIdx) = srcSymbolicArrayIndex + val (dstRef, dstIdx) = dstFromSymbolicArrayIndex + + val newSrcHeapAddr = composer.compose(srcRef) + val newSrcArrayIndex = composer.compose(srcIdx) + val newDstHeapAddress = composer.compose(dstRef) + val newDstFromIndex = composer.compose(dstIdx) + val newDstToIndex = composer.compose(dstToIndex) + + if (newSrcHeapAddr === srcRef && + newSrcArrayIndex === srcIdx && + newDstHeapAddress === dstRef && + newDstFromIndex === dstIdx && + newDstToIndex === dstToIndex + ) { + return this + } + + return clone( + srcSymbolicArrayIndex = newSrcHeapAddr to newSrcArrayIndex, + dstFromSymbolicArrayIndex = newDstHeapAddress to newDstFromIndex, + dstToIndex = newDstToIndex + ) + } +} + +/** + * Represents a synchronous overwriting the range of addresses [[fromKey] : [toKey]] + * with values from memory region [region] read from range + * of addresses [[keyConverter].convert([fromKey]) : [keyConverter].convert([toKey])] + */ +class URangedUpdateNode, ArrayType, SrcKey, DstKey, ValueSort : USort>( + val fromKey: DstKey, + val toKey: DstKey, + val region: UMemoryRegion, + private val concreteComparer: (DstKey, DstKey) -> Boolean, + private val symbolicComparer: (DstKey, DstKey) -> UBoolExpr, + val keyConverter: UMemoryKeyConverter, + val guard: UBoolExpr +) : UUpdateNode { + override fun includesConcretely(key: DstKey): Boolean = + concreteComparer(fromKey, key) && concreteComparer(key, toKey) && guard.isTrue + + override fun includesSymbolically(key: DstKey): UBoolExpr { + val leftIsLefter = symbolicComparer(fromKey, key) + val rightIsRighter = symbolicComparer(key, toKey) + val ctx = leftIsLefter.ctx + + return ctx.mkAnd(leftIsLefter, rightIsRighter, guard) + } + + override fun value(key: DstKey): UExpr = region.read(keyConverter.convert(key)) + + override fun map( + keyMapper: (DstKey) -> DstKey, + composer: UComposer + ): URangedUpdateNode { + val mappedFromKey = keyMapper(fromKey) + val mappedToKey = keyMapper(toKey) + val mappedRegion = region.map(composer) + val mappedKeyConverter = keyConverter.map(composer) + val mappedGuard = composer.compose(guard) + + // If nothing changed, return this + if (mappedFromKey === fromKey + && mappedToKey === toKey + && mappedRegion === region + && mappedKeyConverter === keyConverter + && mappedGuard === guard + ) { + return this + } + + // Otherwise, construct a new one updated node + return URangedUpdateNode( + mappedFromKey, + mappedToKey, + mappedRegion, + concreteComparer, + symbolicComparer, + mappedKeyConverter, + mappedGuard + ) + } + + // Ignores update + override fun equals(other: Any?): Boolean = + other is URangedUpdateNode<*, *, *, *, *> && + this.fromKey == other.fromKey && + this.toKey == other.toKey && + this.guard == other.guard + + // Ignores update + override fun hashCode(): Int = (17 * fromKey.hashCode() + toKey.hashCode()) * 31 + guard.hashCode() + + override fun split( + key: DstKey, predicate: (UExpr) -> Boolean, + matchingWrites: LinkedList>>, + guardBuilder: GuardBuilder + ): UUpdateNode { + val splitRegion = region.split(keyConverter.convert(key), predicate, matchingWrites, guardBuilder) + if (splitRegion === region) { + return this + } + + return URangedUpdateNode( + fromKey, + toKey, + splitRegion, + concreteComparer, + symbolicComparer, + keyConverter, + guard + ) + } +} + +/** + * Used when copying data from allocated array to another allocated array. + */ +class UAllocatedToAllocatedKeyConverter( + srcSymbolicArrayIndex: USymbolicArrayIndex, + dstFromSymbolicArrayIndex: USymbolicArrayIndex, + dstToIndex: USizeExpr +) : UMemoryKeyConverter(srcSymbolicArrayIndex, dstFromSymbolicArrayIndex, dstToIndex) { + override fun convert(key: USizeExpr): USizeExpr = convertIndex(key) + + override fun clone( + srcSymbolicArrayIndex: USymbolicArrayIndex, + dstFromSymbolicArrayIndex: USymbolicArrayIndex, + dstToIndex: USizeExpr + ) = UAllocatedToAllocatedKeyConverter(srcSymbolicArrayIndex, dstFromSymbolicArrayIndex, dstToIndex) +} + +/** + * Used when copying data from allocated array to input one. + */ +class UAllocatedToInputKeyConverter( + srcSymbolicArrayIndex: USymbolicArrayIndex, + dstFromSymbolicArrayIndex: USymbolicArrayIndex, + dstToIndex: USizeExpr +) : UMemoryKeyConverter(srcSymbolicArrayIndex, dstFromSymbolicArrayIndex, dstToIndex) { + override fun convert(key: USymbolicArrayIndex): USizeExpr = convertIndex(key.second) + + override fun clone( + srcSymbolicArrayIndex: USymbolicArrayIndex, + dstFromSymbolicArrayIndex: USymbolicArrayIndex, + dstToIndex: USizeExpr + ) = UAllocatedToInputKeyConverter(srcSymbolicArrayIndex, dstFromSymbolicArrayIndex, dstToIndex) +} + +/** + * Used when copying data from allocated input to allocated one. + */ +class UInputToAllocatedKeyConverter( + srcSymbolicArrayIndex: USymbolicArrayIndex, + dstFromSymbolicArrayIndex: USymbolicArrayIndex, + dstToIndex: USizeExpr +) : UMemoryKeyConverter(srcSymbolicArrayIndex, dstFromSymbolicArrayIndex, dstToIndex) { + override fun convert(key: USizeExpr): USymbolicArrayIndex = srcSymbolicArrayIndex.first to convertIndex(key) + + override fun clone( + srcSymbolicArrayIndex: USymbolicArrayIndex, + dstFromSymbolicArrayIndex: USymbolicArrayIndex, + dstToIndex: USizeExpr + ) = UInputToAllocatedKeyConverter(srcSymbolicArrayIndex, dstFromSymbolicArrayIndex, dstToIndex) +} + +/** + * Used when copying data from input array to another input array. + */ +class UInputToInputKeyConverter( + srcSymbolicArrayIndex: USymbolicArrayIndex, + dstFromSymbolicArrayIndex: USymbolicArrayIndex, + dstToIndex: USizeExpr +) : UMemoryKeyConverter( + srcSymbolicArrayIndex, + dstFromSymbolicArrayIndex, + dstToIndex +) { + override fun convert(key: USymbolicArrayIndex): USymbolicArrayIndex = + srcSymbolicArrayIndex.first to convertIndex(key.second) + + override fun clone( + srcSymbolicArrayIndex: USymbolicArrayIndex, + dstFromSymbolicArrayIndex: USymbolicArrayIndex, + dstToIndex: USizeExpr + ) = UInputToInputKeyConverter(srcSymbolicArrayIndex, dstFromSymbolicArrayIndex, dstToIndex) +} diff --git a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt index 3047f25e15..2e427cc9fb 100644 --- a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt @@ -2,7 +2,6 @@ package org.usvm import io.mockk.every import io.mockk.mockk -import kotlin.reflect.KClass import org.junit.jupiter.api.BeforeEach import org.junit.jupiter.api.Test import org.junit.jupiter.api.assertThrows @@ -13,7 +12,9 @@ import org.ksmt.expr.KExpr import org.ksmt.expr.printer.ExpressionPrinter import org.ksmt.expr.transformer.KTransformerBase import org.ksmt.sort.KBv32Sort +import kotlin.reflect.KClass import kotlin.test.assertEquals +import kotlin.test.assertSame internal class CompositionTest { private lateinit var stackEvaluator: URegistersStackEvaluator @@ -99,7 +100,6 @@ internal class CompositionTest { assert(composedExpression === bvValue) } - @Suppress("UNCHECKED_CAST") @Test fun testReplacementOnSecondLevelOfExpression() = with(ctx) { val bv32Sort = mkBv32Sort() @@ -118,7 +118,6 @@ internal class CompositionTest { } - @Suppress("UNCHECKED_CAST") @Test fun testReplacementInTwoExpressions() = with(ctx) { val bv32Sort = mkBv32Sort() @@ -183,131 +182,227 @@ internal class CompositionTest { @Test fun testUArrayLength() = with(ctx) { - val region = mockk>>() - val address = mockk() + val arrayType: KClass> = Array::class + val firstAddress = 1 + val secondAddress = 2 + + val fstAddress = mockk() + val sndAddress = mockk() + + val fstResultValue = 1.toBv() + val sndResultValue = 2.toBv() + + val updates = UEmptyUpdates( + symbolicEq = { k1, k2 -> k1 eq k2 }, + concreteCmp = { _, _ -> throw UnsupportedOperationException() }, + symbolicCmp = { _, _ -> throw UnsupportedOperationException() } + ).write(fstAddress, fstResultValue, guard = trueExpr) + .write(sndAddress, sndResultValue, guard = trueExpr) + + val regionId = UInputArrayLengthId(arrayType) + val regionArray = UInputArrayLengthMemoryRegion( + regionId, + bv32Sort, + updates, + defaultValue = sizeSort.defaultValue(), + instantiator = { key, region -> mkInputArrayLength(region, key) } + ) - every { region.sort } returns bv32Sort + val fstConcreteAddress = mkConcreteHeapRef(firstAddress) + val sndConcreteAddress = mkConcreteHeapRef(secondAddress) - val arrayLength = ctx.mkArrayLength(region, address) - val arrayBvLength = 32.toBv() + val firstReading = mkInputArrayLength(regionArray, fstConcreteAddress) + val secondReading = mkInputArrayLength(regionArray, sndConcreteAddress) - val typeEvaluator = mockk>>() // TODO replace with jacoDB type - val heapEvaluator = mockk>>() // TODO replace with jacoDB type - val composer = - UComposer(ctx, stackEvaluator, heapEvaluator, typeEvaluator, mockEvaluator) // TODO replace with jacoDB type + val fstValueFromHeap = 42.toBv() + val sndValueFromHeap = 43.toBv() - val addressFromMemory = object : UHeapRef(ctx) { - override val sort: UAddressSort = addressSort + val heapToComposeWith = URegionHeap>>(ctx) - override fun accept(transformer: KTransformerBase): KExpr = this + heapToComposeWith.writeArrayLength(fstConcreteAddress, fstValueFromHeap, arrayType) + heapToComposeWith.writeArrayLength(sndConcreteAddress, sndValueFromHeap, arrayType) - override fun internEquals(other: Any): Boolean = structurallyEqual(other) { sort } + val typeEvaluator = mockk>>>() + val composer = UComposer(ctx, stackEvaluator, heapToComposeWith, typeEvaluator, mockEvaluator) - override fun internHashCode(): Int = hash(sort) + every { fstAddress.accept(composer) } returns fstConcreteAddress + every { sndAddress.accept(composer) } returns sndConcreteAddress - override fun print(printer: ExpressionPrinter) { - printer.append("Test arrayLength object") - } - } - - every { address.accept(any()) } returns addressFromMemory - every { heapEvaluator.readArrayLength(addressFromMemory, arrayLength.region.regionId.arrayType) } returns arrayBvLength + val fstComposedValue = composer.compose(firstReading) + val sndComposedValue = composer.compose(secondReading) - val composedExpression = composer.compose(arrayLength) - - assert(composedExpression === arrayBvLength) + assertSame(fstResultValue, fstComposedValue) + assertSame(sndResultValue, sndComposedValue) } - @Suppress("UNCHECKED_CAST") @Test fun testUInputArrayIndexReading() = with(ctx) { - val region = mockk, UBv32Sort>>() + val fstAddress = mockk() + val sndAddress = mockk() + val fstIndex = mockk() + val sndIndex = mockk() - val arrayType: KClass<*> = Array::class // TODO replace with jacoDB type + val keyEqualityComparer = { k1: USymbolicArrayIndex, k2: USymbolicArrayIndex -> + mkAnd(k1.first eq k2.first, k1.second eq k2.second) + } - every { region.sort } returns bv32Sort - every { region.regionId } returns UInputArrayId(arrayType) + val initialNode = UPinpointUpdateNode( + fstAddress to fstIndex, + 42.toBv(), + keyEqualityComparer + ) - val address = mockk() - val index = mockk() + val updates: UMemoryUpdates = UFlatUpdates( + initialNode, + next = null, + symbolicCmp = { _, _ -> shouldNotBeCalled() }, + concreteCmp = { k1, k2 -> k1 == k2 }, + symbolicEq = { k1, k2 -> keyEqualityComparer(k1, k2) } + ).write(sndAddress to sndIndex, 43.toBv(), guard = trueExpr) + + val arrayType: KClass> = Array::class + + val region = UInputArrayMemoryRegion( + UInputArrayId(arrayType), + mkBv32Sort(), + updates, + defaultValue = null, + instantiator = { key, memoryRegion -> mkInputArrayReading(memoryRegion, key.first, key.second) } + ) - val arrayIndexReading = - mkInputArrayReading(region, address, index) + // TODO replace with jacoDB type + val fstArrayIndexReading = mkInputArrayReading(region, fstAddress, fstIndex) + // TODO replace with jacoDB type + val sndArrayIndexReading = mkInputArrayReading(region, sndAddress, sndIndex) - val arrayAddress = mkConcreteHeapRef(address = 12) - val arrayIndex = mkBv(10) - val answer = 42.toBv() + val answer = 43.toBv() val typeEvaluator = mockk>>() // TODO replace with jacoDB type - val heapEvaluator = mockk>>() // TODO replace with jacoDB type - val composer = - UComposer(ctx, stackEvaluator, heapEvaluator, typeEvaluator, mockEvaluator) // TODO replace with jacoDB type + val heapEvaluator = URegionHeap>(ctx) // TODO replace with jacoDB type - every { address.accept(any()) } returns arrayAddress - every { index.accept(any()) } returns arrayIndex - every { heapEvaluator.readArrayIndex(arrayAddress, arrayIndex, arrayType, bv32Sort) } returns answer + val composer = UComposer( + ctx, stackEvaluator, heapEvaluator, typeEvaluator, mockEvaluator + ) // TODO replace with jacoDB type - val composedExpression = composer.compose(arrayIndexReading) + every { fstAddress.accept(composer) } returns sndAddress + every { fstIndex.accept(composer) } returns sndIndex + every { sndAddress.accept(composer) } returns sndAddress + every { sndIndex.accept(composer) } returns sndIndex - assert(composedExpression === answer) + val fstComposedExpression = composer.compose(fstArrayIndexReading) + val sndComposedExpression = composer.compose(sndArrayIndexReading) + + assert(fstComposedExpression === answer) + assert(sndComposedExpression === answer) } @Test fun testUAllocatedArrayIndexReading() = with(ctx) { - val region = mockk, UBv32Sort>>() - - val arrayType: KClass<*> = Array::class + val arrayType: KClass> = Array::class val address = 1 - every { region.sort } returns bv32Sort - every { region.regionId } returns UAllocatedArrayId(arrayType, address) + val fstIndex = mockk() + val sndIndex = mockk() + + val fstSymbolicIndex = mockk() + val sndSymbolicIndex = mockk() + + val updates = UEmptyUpdates( + symbolicEq = { k1, k2 -> k1 eq k2 }, + concreteCmp = { _, _ -> throw UnsupportedOperationException() }, + symbolicCmp = { _, _ -> throw UnsupportedOperationException() } + ).write(fstIndex, 1.toBv(), guard = trueExpr) + .write(sndIndex, 2.toBv(), guard = trueExpr) + + val regionId = UAllocatedArrayId(arrayType, address) + val regionArray = UAllocatedArrayMemoryRegion( + regionId, + bv32Sort, + updates, + defaultValue = 0.toBv(), + instantiator = { key, region -> mkAllocatedArrayReading(region, key) } + ) - val index = mockk() + val firstReading = mkAllocatedArrayReading(regionArray, fstSymbolicIndex) + val secondReading = mkAllocatedArrayReading(regionArray, sndSymbolicIndex) - val arrayIndexReading = mkAllocatedArrayReading(region, index) + val fstAddressForCompose = mkConcreteHeapRef(address) + val sndAddressForCompose = mkConcreteHeapRef(address) - val composedIndex = 5.toBv() + val concreteIndex = sizeSort.defaultValue() + val fstValue = 42.toBv() + val sndValue = 43.toBv() - val typeEvaluator = mockk>>() // TODO replace with jacoDB type - val heapEvaluator = mockk>>() // TODO replace with jacoDB type - val composer = - UComposer(ctx, stackEvaluator, heapEvaluator, typeEvaluator, mockEvaluator) // TODO replace with jacoDB type + val heapToComposeWith = URegionHeap>>(ctx) - val answer = 42.toBv() - val heapRef = mkConcreteHeapRef(address) + heapToComposeWith.writeArrayIndex( + fstAddressForCompose, concreteIndex, arrayType, regionArray.sort, fstValue, guard = trueExpr + ) + heapToComposeWith.writeArrayIndex( + sndAddressForCompose, concreteIndex, arrayType, regionArray.sort, sndValue, guard = trueExpr + ) - every { index.accept(composer) } returns composedIndex - every { heapEvaluator.readArrayIndex(heapRef, composedIndex, arrayType, bv32Sort) } returns answer + val typeEvaluator = mockk>>>() + val composer = UComposer(ctx, stackEvaluator, heapToComposeWith, typeEvaluator, mockEvaluator) - val composedExpression = composer.compose(arrayIndexReading) + every { fstSymbolicIndex.accept(composer) } returns concreteIndex + every { sndSymbolicIndex.accept(composer) } returns concreteIndex + every { fstIndex.accept(composer) } returns concreteIndex + every { sndIndex.accept(composer) } returns concreteIndex - assert(composedExpression === answer) + val fstComposedValue = composer.compose(firstReading) + val sndComposedValue = composer.compose(secondReading) + + assertSame(2.toBv(), fstComposedValue) + assertSame(fstComposedValue, sndComposedValue) } - @Suppress("UNCHECKED_CAST") @Test fun testUFieldReading() = with(ctx) { - val region = mockk>() - val address = mockk() + val aAddress = mockk() + val bAddress = mockk() - val fieldAddress = mkConcreteHeapRef(address = 12) + val updates = UEmptyUpdates( + symbolicEq = { k1, k2 -> k1 eq k2 }, + concreteCmp = { _, _ -> throw UnsupportedOperationException() }, + symbolicCmp = { _, _ -> throw UnsupportedOperationException() } + ) val field = mockk() // TODO replace with jacoDB field - every { region.sort } returns bv32Sort - every { region.regionId } returns UInputFieldRegionId(field) - every { address.accept(any()) } returns fieldAddress + // An empty region with one write in it + val region = UInputFieldMemoryRegion( + UInputFieldRegionId(field), + bv32Sort, + updates, + defaultValue = null, + instantiator = { key, region -> mkInputFieldReading(region, key) } + ).write(aAddress, 43.toBv(), guard = trueExpr) + + every { aAddress.accept(any()) } returns aAddress + every { bAddress.accept(any()) } returns aAddress + + val expression = mkInputFieldReading(region, bAddress) + + /* Compose: + fun foo(a: A, b: A) { + b = a + a.f = 42 + ------------------- + a.f = 43 + read b.f + */ - val expression = mkFieldReading(region, address) + val answer = 43.toBv() + // TODO replace with jacoDB type - val answer = 42.toBv() - val heapEvaluator = mockk>() // TODO replace with jacoDB type - val composer = - UComposer(ctx, stackEvaluator, heapEvaluator, typeEvaluator, mockEvaluator) // TODO replace with jacoDB type + val heapEvaluator = URegionHeap(ctx) + heapEvaluator.writeField(aAddress, field, bv32Sort, 42.toBv(), guard = trueExpr) - every { heapEvaluator.readField(fieldAddress, field, bv32Sort) } returns answer + // TODO replace with jacoDB type + val composer = UComposer(ctx, stackEvaluator, heapEvaluator, typeEvaluator, mockEvaluator) val composedExpression = composer.compose(expression) assert(composedExpression === answer) } -} \ No newline at end of file +} diff --git a/usvm-core/src/test/kotlin/org/usvm/MapCompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/MapCompositionTest.kt new file mode 100644 index 0000000000..79df0060ab --- /dev/null +++ b/usvm-core/src/test/kotlin/org/usvm/MapCompositionTest.kt @@ -0,0 +1,379 @@ +package org.usvm + +import io.mockk.every +import io.mockk.mockk +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Test +import org.ksmt.expr.KExpr +import org.ksmt.utils.mkConst +import org.usvm.util.SetRegion +import org.usvm.util.emptyRegionTree +import kotlin.test.* + +class MapCompositionTest { + private lateinit var ctx: UContext + private lateinit var composer: UComposer + + @BeforeEach + fun initializeContext() { + ctx = UContext() + composer = mockk() + } + + @Test + fun testWriteIntoEmptyTreeRegionAfterComposition() = with(ctx) { + val concreteAddr = UConcreteHeapRef(this, address = 1) + val symbolicAddr = addressSort.mkConst("addr") + val value = bv32Sort.mkConst("value") + + val updatesToCompose = UTreeUpdates, UBv32Sort>( + updates = emptyRegionTree(), + keyToRegion = { + val singleRegion: SetRegion> = SetRegion.singleton(concreteAddr) + + if (it == symbolicAddr) { + // Z \ {1} + SetRegion.universe().subtract(singleRegion) + } else { + // {1} + singleRegion + } + }, + keyRangeToRegion = { _, _ -> error("Should not be called") }, + symbolicEq = { _, _ -> error("Should not be called") }, + concreteCmp = { _, _ -> error("Should not be called") }, + symbolicCmp = { _, _ -> error("Should not be called") } + ).write(symbolicAddr, value, guard = trueExpr) + + val composer = mockk>() + + every { composer.compose(symbolicAddr) } returns concreteAddr + every { composer.compose(value) } returns 1.toBv() + every { composer.compose(mkTrue()) } returns mkTrue() + + val composedUpdates = updatesToCompose.map(keyMapper = { composer.compose(it) }, composer) + + assert(composedUpdates.isEmpty()) + } + + @Test + fun testWriteIntoIntersectionAfterComposition() { + with(ctx) { + val fstConcreteAddr = mkConcreteHeapRef(address = 1) + val sndConcreteAddr = mkConcreteHeapRef(address = 2) + val thirdConcreteAddr = mkConcreteHeapRef(address = 3) + + val symbolicAddr = addressSort.mkConst("addr") + + val value = bv32Sort.mkConst("value") + + val updatesToCompose = UTreeUpdates, UBv32Sort>( + updates = emptyRegionTree(), + keyToRegion = { + when (it) { + // Z \ {1, 2} + symbolicAddr -> { + SetRegion.universe().subtract(SetRegion.ofSet(fstConcreteAddr, sndConcreteAddr)) + } + // {1, 2, 3} + thirdConcreteAddr -> SetRegion.ofSet(fstConcreteAddr, sndConcreteAddr, thirdConcreteAddr) + else -> SetRegion.singleton(it) + } + }, + keyRangeToRegion = { _, _ -> shouldNotBeCalled() }, + symbolicEq = { _, _ -> shouldNotBeCalled() }, + concreteCmp = { _, _ -> shouldNotBeCalled() }, + symbolicCmp = { _, _ -> shouldNotBeCalled() } + ).write(symbolicAddr, value, guard = trueExpr) + + val composer = mockk>() + + every { composer.compose(symbolicAddr) } returns thirdConcreteAddr + every { composer.compose(value) } returns 1.toBv() + every { composer.compose(mkTrue()) } returns mkTrue() + + // ComposedUpdates contains only one update in a region {3} + val composedUpdates = updatesToCompose.map(keyMapper = { composer.compose(it) }, composer) + + assertFalse(composedUpdates.isEmpty()) + + // Write in the composedUpdates by a key with estimated region {3} + // If we'd have an initial region for the third address, it'd contain an update by region {1, 2, 3} + // Therefore, such writings cause updates splitting. Otherwise, it contains only one update. + val updatedByTheSameRegion = composedUpdates + .copy(keyToRegion = { SetRegion.singleton(thirdConcreteAddr) }) + .write(thirdConcreteAddr, 42.toBv(), guard = trueExpr) + + assertNotNull(updatedByTheSameRegion.singleOrNull()) + } + } + + @Test + fun testPinpointUpdateMapOperationWithoutCompositionEffect() = with(ctx) { + val key = addressSort.mkConst("key") as UExpr + val value = bv32Sort.mkConst("value") + val guard = boolSort.mkConst("guard") + + val updateNode = UPinpointUpdateNode(key, value, { k1, k2 -> k1 eq k2 }, guard) + + every { composer.compose(key) } returns key + every { composer.compose(value) } returns value + every { composer.compose(guard) } returns guard + + val mappedNode = updateNode.map({ k -> composer.compose(k) }, composer) + + assertSame(expected = updateNode, actual = mappedNode) + } + + @Test + fun testPinpointUpdateMapOperation() = with(ctx) { + val key = addressSort.mkConst("key") as UExpr + val value = bv32Sort.mkConst("value") + val guard = boolSort.mkConst("guard") + + val updateNode = UPinpointUpdateNode(key, value, { k1, k2 -> k1 eq k2 }, guard) + + val composedKey = addressSort.mkConst("interpretedKey") + + every { composer.compose(key) } returns composedKey + every { composer.compose(value) } returns 1.toBv() + every { composer.compose(guard) } returns mkTrue() + + val mappedNode = updateNode.map({ k -> composer.compose(k) }, composer) + + assertNotSame(illegal = updateNode, actual = mappedNode) + assertSame(expected = composedKey, actual = mappedNode.key) + assertSame(expected = 1.toBv(), actual = mappedNode.value) + assertSame(expected = mkTrue(), actual = mappedNode.guard) + } + + @Test + fun testRangeUpdateNodeWithoutCompositionEffect() = with(ctx) { + val addr = addressSort.mkConst("addr") + val fromKey = sizeSort.mkConst("fromKey") as UExpr + val toKey = sizeSort.mkConst("toKey") as UExpr + val region = mockk, UExpr, UBv32Sort>>() + val guard = boolSort.mkConst("guard") + + val updateNode = URangedUpdateNode( + fromKey, + toKey, + region = region, + concreteComparer = { _, _ -> shouldNotBeCalled() }, + symbolicComparer = { _, _ -> shouldNotBeCalled() }, + keyConverter = UAllocatedToAllocatedKeyConverter( + srcSymbolicArrayIndex = addr to fromKey, + dstFromSymbolicArrayIndex = addr to fromKey, + dstToIndex = toKey + ), + guard + ) + + every { composer.compose(addr) } returns addr + every { composer.compose(fromKey) } returns fromKey + every { composer.compose(toKey) } returns toKey + every { region.map(composer, any()) } returns region + every { composer.compose(guard) } returns guard + + val mappedUpdateNode = updateNode.map({ k -> composer.compose((k)) }, composer) + + assertSame(expected = updateNode, actual = mappedUpdateNode) + } + + @Test + fun testRangeUpdateNodeMapOperation() = with(ctx) { + val addr = mkConcreteHeapRef(0) + val fromKey = sizeSort.mkConst("fromKey") + val toKey = sizeSort.mkConst("toKey") + val region = mockk, USizeExpr, UBv32Sort>>() + val guard = boolSort.mkConst("guard") + + val updateNode = URangedUpdateNode( + fromKey, + toKey, + region = region, + concreteComparer = { _, _ -> shouldNotBeCalled() }, + symbolicComparer = { _, _ -> shouldNotBeCalled() }, + keyConverter = UAllocatedToAllocatedKeyConverter( + srcSymbolicArrayIndex = addr to fromKey, + dstFromSymbolicArrayIndex = addr to fromKey, + dstToIndex = toKey + ), + guard + ) + + val composedFromKey = sizeSort.mkConst("composedFromKey") + val composedToKey = sizeSort.mkConst("composedToKey") + val composedRegion = mockk, UExpr, UBv32Sort>>() + val composedGuard = mkTrue() + + every { composer.compose(addr) } returns addr + every { composer.compose(fromKey) } returns composedFromKey + every { composer.compose(toKey) } returns composedToKey + every { region.map(composer, any()) } returns composedRegion + every { composer.compose(guard) } returns composedGuard + + val mappedUpdateNode = updateNode.map({ k -> composer.compose((k)) }, composer) + + assertNotSame(illegal = updateNode, actual = mappedUpdateNode) + assertSame(expected = composedFromKey, actual = mappedUpdateNode.fromKey) + assertSame(expected = composedToKey, actual = mappedUpdateNode.toKey) + assertSame(expected = composedRegion, actual = mappedUpdateNode.region) + assertSame(expected = composedGuard, actual = mappedUpdateNode.guard) + } + + @Test + fun testEmptyUpdatesMapOperation() { + val emptyUpdates = UEmptyUpdates, UBv32Sort>( + { _, _ -> shouldNotBeCalled() }, + { _, _ -> shouldNotBeCalled() }, + { _, _ -> shouldNotBeCalled() } + ) + + val mappedUpdates = emptyUpdates.map({ k -> composer.compose(k) }, composer) + + assertSame(expected = emptyUpdates, actual = mappedUpdates) + } + + @Test + fun testFlatUpdatesMapOperationWithoutEffect() = with(ctx) { + val fstKey = addressSort.mkConst("fstKey") + val fstValue = bv32Sort.mkConst("fstValue") + val sndKey = addressSort.mkConst("sndKey") + val sndValue = bv32Sort.mkConst("sndValue") + + val flatUpdates = UEmptyUpdates, UBv32Sort>( + { _, _ -> shouldNotBeCalled() }, + { _, _ -> shouldNotBeCalled() }, + { _, _ -> shouldNotBeCalled() } + ).write(fstKey, fstValue, guard = trueExpr) + .write(sndKey, sndValue, guard = trueExpr) + + every { composer.compose(fstKey) } returns fstKey + every { composer.compose(sndKey) } returns sndKey + every { composer.compose(fstValue) } returns fstValue + every { composer.compose(sndValue) } returns sndValue + every { composer.compose(mkTrue()) } returns mkTrue() + + val mappedUpdates = flatUpdates.map({ k -> composer.compose(k) }, composer) + + assertSame(expected = flatUpdates, actual = mappedUpdates) + } + + @Test + fun testFlatUpdatesMapOperation() = with(ctx) { + val fstKey = addressSort.mkConst("fstKey") + val fstValue = bv32Sort.mkConst("fstValue") + val sndKey = addressSort.mkConst("sndKey") + val sndValue = bv32Sort.mkConst("sndValue") + + val flatUpdates = UEmptyUpdates, UBv32Sort>( + { _, _ -> shouldNotBeCalled() }, + { _, _ -> shouldNotBeCalled() }, + { _, _ -> shouldNotBeCalled() } + ).write(fstKey, fstValue, guard = trueExpr) + .write(sndKey, sndValue, guard = trueExpr) + + val composedFstKey = addressSort.mkConst("composedFstKey") + val composedSndKey = addressSort.mkConst("composedSndKey") + val composedFstValue = 1.toBv() + val composedSndValue = 2.toBv() + + every { composer.compose(fstKey) } returns composedFstKey + every { composer.compose(sndKey) } returns composedSndKey + every { composer.compose(fstValue) } returns composedFstValue + every { composer.compose(sndValue) } returns composedSndValue + every { composer.compose(mkTrue()) } returns mkTrue() + + val mappedUpdates = flatUpdates.map({ k -> composer.compose(k) }, composer) + + assertNotSame(illegal = flatUpdates, actual = mappedUpdates) + + val node = mappedUpdates.node as UPinpointUpdateNode<*, *> + val next = mappedUpdates.next as UFlatUpdates<*, *> + val nextNode = next.node as UPinpointUpdateNode<*, *> + + assertSame(expected = composedSndKey, actual = node.key) + assertSame(expected = composedSndValue, actual = node.value) + assertSame(expected = composedFstKey, actual = nextNode.key) + assertSame(expected = composedFstValue, actual = nextNode.value) + assertNull(next.next) + } + + @Test + fun testTreeUpdatesMapOperationWithoutEffect() = with(ctx) { + val fstKey = addressSort.mkConst("fstKey") + val fstValue = bv32Sort.mkConst("fstValue") + val sndKey = addressSort.mkConst("sndKey") + val sndValue = bv32Sort.mkConst("sndValue") + + val treeUpdates = UTreeUpdates, SetRegion>, UBv32Sort>( + emptyRegionTree(), + { k -> SetRegion.singleton(k) }, + { k1, k2 -> SetRegion.ofSet(k1, k2) }, + { _, _ -> shouldNotBeCalled() }, + { _, _ -> shouldNotBeCalled() }, + { _, _ -> shouldNotBeCalled() } + ).write(fstKey, fstValue, guard = trueExpr) + .write(sndKey, sndValue, guard = trueExpr) + + every { composer.compose(fstKey) } returns fstKey + every { composer.compose(sndKey) } returns sndKey + every { composer.compose(fstValue) } returns fstValue + every { composer.compose(sndValue) } returns sndValue + every { composer.compose(mkTrue()) } returns mkTrue() + + val mappedUpdates = treeUpdates.map({ k -> composer.compose(k) }, composer) + + assertSame(expected = treeUpdates, actual = mappedUpdates) + } + + @Test + fun testTreeUpdatesMapOperation() = with(ctx) { + val fstKey = addressSort.mkConst("fstKey") + val fstValue = bv32Sort.mkConst("fstValue") + val sndKey = addressSort.mkConst("sndKey") + val sndValue = bv32Sort.mkConst("sndValue") + + val treeUpdates = UTreeUpdates, SetRegion>, UBv32Sort>( + emptyRegionTree(), + { SetRegion.universe() }, + { _, _ -> SetRegion.universe() }, + { _, _ -> shouldNotBeCalled() }, + { _, _ -> shouldNotBeCalled() }, + { _, _ -> shouldNotBeCalled() } + ).write(fstKey, fstValue, guard = trueExpr) + .write(sndKey, sndValue, guard = trueExpr) + + val composedFstKey = addressSort.mkConst("composedFstKey") + val composedSndKey = addressSort.mkConst("composedSndKey") + val composedFstValue = 1.toBv() + val composedSndValue = 2.toBv() + + every { composer.compose(fstKey) } returns composedFstKey + every { composer.compose(sndKey) } returns composedSndKey + every { composer.compose(fstValue) } returns composedFstValue + every { composer.compose(sndValue) } returns composedSndValue + every { composer.compose(mkTrue()) } returns mkTrue() + + val mappedUpdates = treeUpdates.map({ k -> composer.compose(k) }, composer) + + assertNotSame(illegal = treeUpdates, actual = mappedUpdates) + + val elements = mappedUpdates.toList() + + assert(elements.size == 2) + + val fstElement = elements.first() as UPinpointUpdateNode<*, *> + val sndElement = elements.last() as UPinpointUpdateNode<*, *> + + assertSame(expected = composedFstKey, actual = fstElement.key) + assertSame(expected = composedFstValue, actual = fstElement.value) + assertSame(expected = composedSndKey, actual = sndElement.key) + assertSame(expected = composedSndValue, actual = sndElement.value) + } +} + +fun shouldNotBeCalled(): T { + error("Should not be called") +} \ No newline at end of file diff --git a/usvm-core/src/test/kotlin/org/usvm/MemoryRegionTests.kt b/usvm-core/src/test/kotlin/org/usvm/MemoryRegionTests.kt new file mode 100644 index 0000000000..7f983fa5f0 --- /dev/null +++ b/usvm-core/src/test/kotlin/org/usvm/MemoryRegionTests.kt @@ -0,0 +1,74 @@ +package org.usvm + +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Test +import org.ksmt.utils.mkConst +import org.usvm.util.SetRegion +import org.usvm.util.emptyRegionTree +import kotlin.test.assertNotNull + +class MemoryRegionTests { + private lateinit var ctx: UContext + + @BeforeEach + fun initializeContext() { + ctx = UContext() + } + + @Test + fun testMultipleWriteTheSameUpdateNode() { + /* + This test verifies that key deduplication works as expected: + the most recent writings for update nodes with the same key should + override the previous ones (ignoring their value) + */ + + with(ctx) { + val address = mkConcreteHeapRef(address = 1) + + val treeUpdates = UTreeUpdates, UBv32Sort>( + updates = emptyRegionTree(), + keyToRegion = { SetRegion.universe() }, + keyRangeToRegion = { _, _ -> shouldNotBeCalled() }, + symbolicEq = { _, _ -> shouldNotBeCalled() }, + concreteCmp = { _, _ -> shouldNotBeCalled() }, + symbolicCmp = { _, _ -> shouldNotBeCalled() } + ).write(address, 1.toBv(), mkTrue()) + .write(address, 2.toBv(), mkTrue()) + .write(address, 3.toBv(), mkTrue()) + .write(address, 4.toBv(), mkTrue()) + .write(address, 5.toBv(), mkTrue()) + + assertNotNull(treeUpdates.singleOrNull()) + } + } + + @Test + fun testMultipleWriteTheSameNodesWithDifferentGuards() { + with(ctx) { + val address = mkConcreteHeapRef(address = 1) + + val guard = boolSort.mkConst("boolConst") + val anotherGuard = boolSort.mkConst("anotherBoolConst") + + val treeUpdates = UTreeUpdates, UBv32Sort>( + updates = emptyRegionTree(), + keyToRegion = { SetRegion.universe() }, + keyRangeToRegion = { _, _ -> shouldNotBeCalled() }, + symbolicEq = { _, _ -> shouldNotBeCalled() }, + concreteCmp = { _, _ -> shouldNotBeCalled() }, + symbolicCmp = { _, _ -> shouldNotBeCalled() } + ).write(address, 1.toBv(), guard) + .write(address, 2.toBv(), anotherGuard) + + assert(treeUpdates.toList().size == 2) + + val anotherTreeUpdates = treeUpdates + .write(address, 3.toBv(), anotherGuard) + .write(address, 4.toBv(), guard) + + assert(anotherTreeUpdates.toList().size == 2) + } + } + +} \ No newline at end of file diff --git a/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt b/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt index 37f9c2d28b..970cd77eff 100644 --- a/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt @@ -4,7 +4,6 @@ import io.mockk.every import io.mockk.mockk import org.junit.jupiter.api.BeforeEach import org.junit.jupiter.api.Test -import org.ksmt.utils.cast private typealias Field = java.lang.reflect.Field private typealias ArrayType = kotlin.reflect.KClass<*> @@ -58,9 +57,8 @@ class UContextInterningTest { @Test fun testFieldReadingInterning() = with(context) { - // TODO replace after making `out` type in MemoryRegion - val fstRegion: UInputFieldMemoryRegion = mockk>().cast() - val sndRegion: UInputFieldMemoryRegion = mockk>().cast() + val fstRegion = mockk>() + val sndRegion = mockk>() every { fstRegion.sort } returns bv32Sort every { sndRegion.sort } returns boolSort @@ -68,14 +66,14 @@ class UContextInterningTest { val fstAddress = mkConcreteHeapRef(address = 1) val sndAddress = mkConcreteHeapRef(address = 2) - val equal = List(10) { mkFieldReading(fstRegion, fstAddress) } + val equal = List(10) { mkInputFieldReading(fstRegion, fstAddress) } val createdWithoutContext = UFieldReading(this, fstRegion, fstAddress) val distinct = listOf( - mkFieldReading(fstRegion, fstAddress), - mkFieldReading(fstRegion, sndAddress), - mkFieldReading(sndRegion, fstAddress), - mkFieldReading(sndRegion, sndAddress), + mkInputFieldReading(fstRegion, fstAddress), + mkInputFieldReading(fstRegion, sndAddress), + mkInputFieldReading(sndRegion, fstAddress), + mkInputFieldReading(sndRegion, sndAddress), createdWithoutContext ) @@ -84,9 +82,8 @@ class UContextInterningTest { @Test fun testAllocatedArrayReadingInterning() = with(context) { - // TODO replace after making `out` type in regions - val fstRegion: UAllocatedArrayMemoryRegion = mockk>().cast() - val sndRegion: UAllocatedArrayMemoryRegion = mockk>().cast() + val fstRegion = mockk>() + val sndRegion = mockk>() every { fstRegion.sort } returns bv32Sort every { sndRegion.sort } returns boolSort @@ -94,12 +91,10 @@ class UContextInterningTest { val fstIndex = mockk() val sndIndex = mockk() - val equal = List(10) { - mkAllocatedArrayReading(fstRegion, fstIndex) - } + val equal = List(10) { mkAllocatedArrayReading(fstRegion, fstIndex) } + + val createdWithoutContext = UAllocatedArrayReading(this, fstRegion, fstIndex) - val createdWithoutContext = - UAllocatedArrayReading(this, fstRegion, fstIndex) val distinct = listOf( mkAllocatedArrayReading(fstRegion, fstIndex), mkAllocatedArrayReading(fstRegion, sndIndex), @@ -113,9 +108,8 @@ class UContextInterningTest { @Test fun testInputArrayReadingInterning() = with(context) { - // TODO replace after making `out` type in regions - val fstRegion: UInputArrayMemoryRegion = mockk>().cast() - val sndRegion: UInputArrayMemoryRegion = mockk>().cast() + val fstRegion = mockk>() + val sndRegion = mockk>() every { fstRegion.sort } returns bv32Sort every { sndRegion.sort } returns boolSort @@ -126,12 +120,10 @@ class UContextInterningTest { val fstIndex = mockk() val sndIndex = mockk() - val equal = List(10) { - mkInputArrayReading(fstRegion, fstAddress, fstIndex) - } + val equal = List(10) { mkInputArrayReading(fstRegion, fstAddress, fstIndex) } + + val createdWithoutContext = UInputArrayReading(this, fstRegion, fstAddress, fstIndex) - val createdWithoutContext = - UInputArrayReading(this, fstRegion, fstAddress, fstIndex) val distinct = listOf( mkInputArrayReading(fstRegion, fstAddress, fstIndex), mkInputArrayReading(fstRegion, fstAddress, sndIndex), @@ -156,13 +148,14 @@ class UContextInterningTest { val fstAddress = mkConcreteHeapRef(address = 1) val sndAddress = mkConcreteHeapRef(address = 2) - val equal = List(10) { mkArrayLength(fstRegion, fstAddress) } + val equal = List(10) { mkInputArrayLength(fstRegion, fstAddress) } val createdWithoutContext = UArrayLength(this, fstRegion, fstAddress) + val distinct = listOf( - mkArrayLength(fstRegion, fstAddress), - mkArrayLength(fstRegion, sndAddress), - mkArrayLength(sndRegion, sndAddress), + mkInputArrayLength(fstRegion, fstAddress), + mkInputArrayLength(fstRegion, sndAddress), + mkInputArrayLength(sndRegion, sndAddress), createdWithoutContext ) @@ -183,6 +176,7 @@ class UContextInterningTest { val equal = List(10) { mkIndexedMethodReturnValue(fstMethod, fstCallIndex, fstSort) } val createdWithoutContext = UIndexedMethodReturnValue(this, fstMethod, fstCallIndex, fstSort) + val distinct = listOf( mkIndexedMethodReturnValue(fstMethod, fstCallIndex, fstSort), mkIndexedMethodReturnValue(fstMethod, sndCallIndex, fstSort), @@ -205,6 +199,7 @@ class UContextInterningTest { val equal = List(10) { mkIsExpr(fstRef, fstSort) } val createdWithoutContext = UIsExpr(this, fstRef, fstSort) + val distinct = listOf( mkIsExpr(fstRef, fstSort), mkIsExpr(fstRef, sndSort), diff --git a/usvm-core/src/test/kotlin/org/usvm/UpdatesIteratorTest.kt b/usvm-core/src/test/kotlin/org/usvm/UpdatesIteratorTest.kt index c515a80c7b..2742b0b0e3 100644 --- a/usvm-core/src/test/kotlin/org/usvm/UpdatesIteratorTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/UpdatesIteratorTest.kt @@ -4,7 +4,6 @@ import org.junit.jupiter.api.Test import org.junit.jupiter.api.assertThrows import org.usvm.util.SetRegion import org.usvm.util.emptyRegionTree -import java.lang.UnsupportedOperationException import kotlin.test.assertTrue class UpdatesIteratorTest { @@ -24,10 +23,10 @@ class UpdatesIteratorTest { { k1, k2 -> mkEq(k1.toBv(), k2.toBv()) }, { k1, k2 -> k1 == k2 }, { _, _ -> throw UnsupportedOperationException() } - ).write(10, 10.toBv()) - .write(1, 1.toBv()) - .write(2, 2.toBv()) - .write(3, 3.toBv()) + ).write(10, 10.toBv(), guard = mkTrue()) + .write(1, 1.toBv(), guard = mkTrue()) + .write(2, 2.toBv(), guard = mkTrue()) + .write(3, 3.toBv(), guard = mkTrue()) val iterator = treeUpdates.iterator() checkResult(iterator) @@ -48,9 +47,9 @@ class UpdatesIteratorTest { { _, _ -> throw NotImplementedError() }, { _, _ -> throw NotImplementedError() }, { _, _ -> throw NotImplementedError() } - ).write(key = 1, value = 1.toBv()) - .write(key = 2, value = 2.toBv()) - .write(key = 3, value = 3.toBv()) + ).write(key = 1, value = 1.toBv(), guard = mkTrue()) + .write(key = 2, value = 2.toBv(), guard = mkTrue()) + .write(key = 3, value = 3.toBv(), guard = mkTrue()) val iterator = flatUpdates.iterator() checkResult(iterator) @@ -83,5 +82,4 @@ class UpdatesIteratorTest { assertTrue { key == expectedKeyWithValue.first && value == expectedKeyWithValue.second } } } - -} \ No newline at end of file +} diff --git a/usvm-util/src/main/kotlin/org/usvm/util/RegionTree.kt b/usvm-util/src/main/kotlin/org/usvm/util/RegionTree.kt index 91a57c4ffe..6ce5b889db 100644 --- a/usvm-util/src/main/kotlin/org/usvm/util/RegionTree.kt +++ b/usvm-util/src/main/kotlin/org/usvm/util/RegionTree.kt @@ -3,7 +3,6 @@ package org.usvm.util import kotlinx.collections.immutable.PersistentMap import kotlinx.collections.immutable.persistentMapOf import kotlinx.collections.immutable.toPersistentMap -import java.util.NoSuchElementException /** * Region tree is a data structure storing collection of keys by abstract regions. @@ -59,7 +58,7 @@ class RegionTree( // it is required for correct order of keys returned by `iterator.next()` method // We have to support the following order: assume that we had entries [e0, e1, e2, e3, e4] // and a write operation into a region R that is a subregion of `e1` and `e3`, and covers e2 completely. - // The correct order of the result is:\ + // The correct order of the result is: // included = [R ∩ e1, e2, R ∩ e3], disjoint = [e0, e1\R, e3\R, e4] // That allows us to move recently updates region to the right side of the `entries` map and // leave the oldest ones in the left part of it. @@ -124,8 +123,6 @@ class RegionTree( return RegionTree(disjointEntries) } - // TODO: add collection operations, like map, fold, filter, flatten, etc... - private fun checkInvariantRecursively(parentRegion: Reg?): Boolean { // Invariant (2): all child regions are included into parent region val secondInvariant = parentRegion == null || entries.entries.all { (key, _) -> diff --git a/usvm-util/src/main/kotlin/org/usvm/util/Regions.kt b/usvm-util/src/main/kotlin/org/usvm/util/Regions.kt index 3d356b0753..3f1f2e053c 100644 --- a/usvm-util/src/main/kotlin/org/usvm/util/Regions.kt +++ b/usvm-util/src/main/kotlin/org/usvm/util/Regions.kt @@ -1,7 +1,5 @@ package org.usvm.util -import java.lang.UnsupportedOperationException - enum class RegionComparisonResult { INCLUDES, INTERSECTS, DISJOINT } @@ -110,7 +108,8 @@ data class SetRegion(private val points: Set, private val thrown: fun universe() = SetRegion(emptySet(), true) } - override val isEmpty: Boolean = points.isEmpty() + override val isEmpty: Boolean = points.isEmpty() && !thrown + override fun compare(other: SetRegion): RegionComparisonResult = when { !this.thrown && !other.thrown -> setsComparisonToResult(compareSets(this.points, other.points)) @@ -123,6 +122,7 @@ data class SetRegion(private val points: Set, private val thrown: else RegionComparisonResult.INTERSECTS else -> throw Exception("Unreachable") } + override fun subtract(other: SetRegion): SetRegion = when { !this.thrown && !other.thrown -> SetRegion(this.points.minus(other.points), false)