diff --git a/buildSrc/src/main/kotlin/Versions.kt b/buildSrc/src/main/kotlin/Versions.kt index 8e56b00e90..bd678600a7 100644 --- a/buildSrc/src/main/kotlin/Versions.kt +++ b/buildSrc/src/main/kotlin/Versions.kt @@ -1,5 +1,5 @@ object Versions { - const val ksmt = "0.4.4" + const val ksmt = "0.5.0" const val collections = "0.3.5" const val coroutines = "1.6.4" const val jcdb = "a5c479bcf8" diff --git a/usvm-core/src/main/kotlin/org/usvm/Composition.kt b/usvm-core/src/main/kotlin/org/usvm/Composition.kt index 51ecbff8f6..bf9463c1b7 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Composition.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Composition.kt @@ -6,7 +6,7 @@ open class UComposer( internal val stackEvaluator: URegistersStackEvaluator, internal val heapEvaluator: UReadOnlySymbolicHeap, internal val typeEvaluator: UTypeEvaluator, - internal val mockEvaluator: UMockEvaluator + internal val mockEvaluator: UMockEvaluator, ) : UExprTransformer(ctx) { open fun compose(expr: UExpr): UExpr = apply(expr) @@ -14,7 +14,7 @@ open class UComposer( error("You must override `transform` function in org.usvm.UComposer for ${expr::class}") override fun transform( - expr: URegisterReading + expr: URegisterReading, ): UExpr = with(expr) { stackEvaluator.eval(idx, sort) } override fun transform(expr: UHeapReading<*, *, *>): UExpr = @@ -24,7 +24,7 @@ open class UComposer( error("You must override `transform` function in org.usvm.UComposer for ${expr::class}") override fun transform( - expr: UIndexedMethodReturnValue + expr: UIndexedMethodReturnValue, ): UExpr = mockEvaluator.eval(expr) override fun transform(expr: UIsExpr): UBoolExpr = with(expr) { @@ -32,19 +32,12 @@ open class UComposer( typeEvaluator.evalIs(composedAddress, type) } - fun , Key, Sort : USort> transformHeapReading( + fun , Key, Sort : USort> transformHeapReading( expr: UHeapReading, - key: Key + key: Key, ): UExpr = with(expr) { - 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) - } - - val mappedRegion = region.map(this@UComposer, instantiator) - val mappedKey = region.regionId.keyMapper(this@UComposer)(key) + val mappedRegion = region.map(this@UComposer) + val mappedKey = mappedRegion.regionId.keyMapper(this@UComposer)(key) mappedRegion.read(mappedKey) } @@ -62,5 +55,5 @@ open class UComposer( override fun transform(expr: UConcreteHeapRef): UExpr = expr - override fun transform(expr: UNullRef): UNullRef = expr + override fun transform(expr: UNullRef): UExpr = heapEvaluator.nullRef() } diff --git a/usvm-core/src/main/kotlin/org/usvm/Context.kt b/usvm-core/src/main/kotlin/org/usvm/Context.kt index 04dca69f85..b51d3237eb 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Context.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Context.kt @@ -2,9 +2,17 @@ package org.usvm import org.ksmt.KAst import org.ksmt.KContext -import org.ksmt.solver.model.DefaultValueSampler.Companion.sampleValue +import org.ksmt.expr.KConst +import org.ksmt.expr.KExpr +import org.ksmt.expr.KUninterpretedSortValue +import org.ksmt.sort.KBoolSort +import org.ksmt.sort.KSort +import org.ksmt.sort.KSortVisitor +import org.ksmt.sort.KUninterpretedSort +import org.ksmt.utils.DefaultValueSampler import org.ksmt.utils.asExpr import org.ksmt.utils.cast +import org.ksmt.utils.sampleValue @Suppress("LeakingThis") open class UContext( @@ -15,9 +23,9 @@ open class UContext( val addressSort: UAddressSort = mkUninterpretedSort("Address") val sizeSort: USizeSort = bv32Sort - val zeroSize: USizeExpr = sizeSort.defaultValue() + val zeroSize: USizeExpr = sizeSort.sampleValue() - val nullRef: USymbolicHeapRef = UNullRef(this) + val nullRef: UNullRef = UNullRef(this) fun mkNullRef(): USymbolicHeapRef { return nullRef @@ -43,10 +51,17 @@ open class UContext( * * @return the new equal rewritten expression without [UConcreteHeapRef]s */ + override fun mkEq(lhs: KExpr, rhs: KExpr, order: Boolean): KExpr = + if (lhs.sort == addressSort) { + mkHeapRefEq(lhs.asExpr(addressSort), rhs.asExpr(addressSort)) + } else { + super.mkEq(lhs, rhs, order) + } + fun mkHeapRefEq(lhs: UHeapRef, rhs: UHeapRef): UBoolExpr = when { // fast checks - lhs is USymbolicHeapRef && rhs is USymbolicHeapRef -> super.mkEq(lhs, rhs) + lhs is USymbolicHeapRef && rhs is USymbolicHeapRef -> super.mkEq(lhs, rhs, order = true) lhs is UConcreteHeapRef && rhs is UConcreteHeapRef -> mkBool(lhs == rhs) // unfolding else -> { @@ -65,7 +80,7 @@ open class UContext( } if (symbolicRefLhs != null && symbolicRefRhs != null) { - val refsEq = symbolicRefLhs.expr eq symbolicRefRhs.expr + val refsEq = super.mkEq(symbolicRefLhs.expr, symbolicRefRhs.expr, order = true) // mkAnd instead of mkAndNoFlat here is OK val conjunct = mkAnd(symbolicRefLhs.guard, symbolicRefRhs.guard, refsEq) conjuncts += conjunct @@ -76,10 +91,6 @@ open class UContext( } } - @Suppress("UNUSED_PARAMETER") - @Deprecated("Use mkHeapRefEq instead.", ReplaceWith("this.mkHeapRefEq(lhs, rhs)"), level = DeprecationLevel.ERROR) - fun mkEq(lhs: UHeapRef, rhs: UHeapRef): Nothing = error("Use mkHeapRefEq instead.") - private val uConcreteHeapRefCache = mkAstInterner() fun mkConcreteHeapRef(address: UConcreteHeapAddress): UConcreteHeapRef = uConcreteHeapRefCache.createIfContextActive { @@ -144,18 +155,19 @@ open class UContext( UIsExpr(this, ref, type.cast()) }.cast() - fun mkDefault(sort: Sort): UExpr = - when (sort) { - addressSort -> nullRef.asExpr(sort) - else -> sort.sampleValue() - } -} + class UDefaultValueSampler(val uctx: UContext) : DefaultValueSampler(uctx) { + override fun visit(sort: KUninterpretedSort): KExpr<*> = + if (sort == uctx.addressSort) { + uctx.nullRef + } else { + super.visit(sort) + } + } -fun Sort.defaultValue() = - when (ctx) { - is UContext -> (ctx as UContext).mkDefault(this) - else -> sampleValue() + override fun mkDefaultValueSampler(): KSortVisitor> { + return UDefaultValueSampler(this) } +} val KAst.uctx get() = ctx as UContext diff --git a/usvm-core/src/main/kotlin/org/usvm/EagerModels.kt b/usvm-core/src/main/kotlin/org/usvm/EagerModels.kt new file mode 100644 index 0000000000..9fac171b7b --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/EagerModels.kt @@ -0,0 +1,156 @@ +package org.usvm + +import org.ksmt.utils.asExpr +import org.ksmt.utils.sampleValue + +/** + * An eager model for registers that stores mapping + * from mock symbols to evaluated expressions. + */ +class URegistersStackEagerModel( + private val nullRef: UConcreteHeapRef, + private val registers: Map> +) : URegistersStackEvaluator { + override fun eval( + registerIndex: Int, + sort: Sort, + ): UExpr = registers.getOrDefault(registerIndex, sort.sampleValue().nullAddress(nullRef)).asExpr(sort) +} + +/** + * An eager model for an indexed mocker that stores mapping + * from mock symbols and invocation indices to expressions. + */ +class UIndexedMockEagerModel( + private val nullRef: UConcreteHeapRef, + private val values: Map, UExpr<*>>, +) : UMockEvaluator { + + override fun eval(symbol: UMockSymbol): UExpr { + require(symbol is UIndexedMethodReturnValue<*, Sort>) + + val sort = symbol.sort + + @Suppress("UNCHECKED_CAST") + val key = symbol.method as Method to symbol.callIndex + + return values.getOrDefault(key, sort.sampleValue().nullAddress(nullRef)).asExpr(sort) + } +} + +/** + * An eager immutable heap model. + * + * Declared as mutable heap for using in regions composition in [UComposer]. Any call to + * modifying operation throws an exception. + * + * Any [UHeapReading] possibly writing to this heap in its [URegionId.instantiate] call actually has empty updates, + * because localization happened, so this heap won't be mutated. + */ +class UHeapEagerModel( + private val nullRef: UConcreteHeapRef, + private val resolvedInputFields: Map>, + private val resolvedInputArrays: Map>, + private val resolvedInputLengths: Map>, +) : USymbolicHeap { + override fun readField(ref: UHeapRef, field: Field, sort: Sort): UExpr { + // All the expressions in the model are interpreted, therefore, they must + // have concrete addresses. Moreover, the model knows only about input values + // which have addresses less or equal than INITIAL_INPUT_ADDRESS + require(ref is UConcreteHeapRef && ref.address <= UAddressCounter.INITIAL_INPUT_ADDRESS) + + @Suppress("UNCHECKED_CAST") + val region = resolvedInputFields.getOrElse(field) { + UMemory1DArray(sort.sampleValue().nullAddress(nullRef)) + } as UMemoryRegion + + return region.read(ref) + } + + override fun readArrayIndex( + ref: UHeapRef, + index: USizeExpr, + arrayType: ArrayType, + sort: Sort, + ): UExpr { + // All the expressions in the model are interpreted, therefore, they must + // have concrete addresses. Moreover, the model knows only about input values + // which have addresses less or equal than INITIAL_INPUT_ADDRESS + require(ref is UConcreteHeapRef && ref.address <= UAddressCounter.INITIAL_INPUT_ADDRESS) + + val key = ref to index + + @Suppress("UNCHECKED_CAST") + val region = resolvedInputArrays.getOrElse(arrayType) { + UMemory2DArray(sort.sampleValue().nullAddress(nullRef)) + } as UMemoryRegion + + return region.read(key) + } + + override fun readArrayLength(ref: UHeapRef, arrayType: ArrayType): USizeExpr { + // All the expressions in the model are interpreted, therefore, they must + // have concrete addresses. Moreover, the model knows only about input values + // which have addresses less or equal than INITIAL_INPUT_ADDRESS + require(ref is UConcreteHeapRef && ref.address <= UAddressCounter.INITIAL_INPUT_ADDRESS) + + val region = resolvedInputLengths.getOrElse>(arrayType) { + UMemory1DArray(ref.uctx.sizeSort.sampleValue()) + } + + return region.read(ref) + } + + override fun writeField( + ref: UHeapRef, + field: Field, + sort: Sort, + value: UExpr, + guard: UBoolExpr, + ) = error("Illegal operation for a model") + + override fun writeArrayIndex( + ref: UHeapRef, + index: USizeExpr, + type: ArrayType, + sort: Sort, + value: UExpr, + guard: UBoolExpr, + ) = error("Illegal operation for a model") + + override fun writeArrayLength(ref: UHeapRef, size: USizeExpr, arrayType: ArrayType) = + error("Illegal operation for a model") + + override fun memcpy( + srcRef: UHeapRef, + dstRef: UHeapRef, + type: ArrayType, + elementSort: Sort, + fromSrcIdx: USizeExpr, + fromDstIdx: USizeExpr, + toDstIdx: USizeExpr, + guard: UBoolExpr, + ) = error("Illegal operation for a model") + + override fun memset( + ref: UHeapRef, + type: ArrayType, + sort: Sort, + contents: Sequence>, + ) = error("Illegal operation for a model") + + override fun allocate() = error("Illegal operation for a model") + + override fun allocateArray(count: USizeExpr) = error("Illegal operation for a model") + + override fun nullRef(): UConcreteHeapRef = nullRef + + override fun toMutableHeap(): UHeapEagerModel = this +} + +fun UExpr.nullAddress(nullRef: UConcreteHeapRef): UExpr = + if (this == uctx.nullRef) { + nullRef.asExpr(sort) + } else { + this + } \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/ExprTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/ExprTranslator.kt new file mode 100644 index 0000000000..8cef18631e --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/ExprTranslator.kt @@ -0,0 +1,181 @@ +package org.usvm + +import org.ksmt.expr.KExpr +import org.ksmt.sort.KBoolSort +import org.ksmt.utils.cast +import org.ksmt.utils.mkConst + +/** + * Translates custom [UExpr] to a [KExpr]. Region readings are translated via [URegionTranslator]s. + * Base version cache everything, but doesn't track translated expressions like register readings, mock symbols, etc. + * Tracking done in the [UCachingExprTranslator]. + * + * To show semantics of the translator, we use [KExpr] as return values, though [UExpr] is a typealias for it. + */ +open class UExprTranslator( + override val ctx: UContext, +) : UExprTransformer(ctx), URegionIdVisitor> { + + open fun translate(expr: UExpr): KExpr = apply(expr) + + override fun transform(expr: USymbol): KExpr = + error("You must override `transform` function in UExprTranslator for ${expr::class}") + + override fun transform(expr: URegisterReading): KExpr { + val registerConst = expr.sort.mkConst("r${expr.idx}_${expr.sort}") + return registerConst + } + + override fun transform(expr: UHeapReading<*, *, *>): KExpr = + error("You must override `transform` function in UExprTranslator for ${expr::class}") + + override fun transform(expr: UMockSymbol): KExpr = + error("You must override `transform` function in UExprTranslator for ${expr::class}") + + override fun transform(expr: UIndexedMethodReturnValue): KExpr { + val const = expr.sort.mkConst("m${expr.method}_${expr.callIndex}_${expr.sort}") + return const + } + + override fun transform(expr: UNullRef): KExpr { + val const = ctx.mkUninterpretedSortValue(ctx.addressSort, valueIdx = 0) + return const + } + + override fun transform(expr: UConcreteHeapRef): KExpr = + error("Unexpected UConcreteHeapRef $expr in UExprTranslator, that has to be impossible by construction!") + + override fun transform(expr: UIsExpr): KExpr = + error("Unexpected UIsExpr $expr in UExprTranslator, that has to be impossible by construction!") + + override fun transform(expr: UInputArrayLengthReading): KExpr = + transformExprAfterTransformed(expr, expr.address) { address -> + translateRegionReading(expr.region, address) + } + + override fun transform(expr: UInputArrayReading): KExpr = + transformExprAfterTransformed(expr, expr.address, expr.index) { address, index -> + translateRegionReading(expr.region, address to index) + } + + override fun transform(expr: UAllocatedArrayReading): KExpr = + transformExprAfterTransformed(expr, expr.index) { index -> + translateRegionReading(expr.region, index) + } + + override fun transform(expr: UInputFieldReading): KExpr = + transformExprAfterTransformed(expr, expr.address) { address -> + translateRegionReading(expr.region, address) + } + + open fun translateRegionReading( + region: USymbolicMemoryRegion, Key, Sort>, + key: Key, + ): KExpr { + val regionTranslator = buildTranslator(region.regionId) + return regionTranslator.translateReading(region, key) + } + + private val regionIdToInitialValue_ = mutableMapOf, KExpr<*>>() + val regionIdToInitialValue: Map, KExpr<*>> get() = regionIdToInitialValue_ + + private inline fun > getOrPutInitialValue( + regionId: URegionId<*, *, *>, + defaultValue: () -> V + ): V = regionIdToInitialValue_.getOrPut(regionId, defaultValue) as V + + override fun visit( + regionId: UInputFieldId, + ): URegionTranslator, UHeapRef, Sort, *> { + require(regionId.defaultValue == null) + val initialValue = getOrPutInitialValue(regionId) { + with(regionId.sort.uctx) { + mkArraySort(addressSort, regionId.sort).mkConst(regionId.toString()) // TODO: replace toString + } + } + val updateTranslator = U1DArrayUpdateTranslate(this, initialValue) + return URegionTranslator(updateTranslator) + } + + override fun visit( + regionId: UAllocatedArrayId, + ): URegionTranslator, USizeExpr, Sort, *> { + requireNotNull(regionId.defaultValue) + val initialValue = getOrPutInitialValue(regionId) { + with(regionId.sort.uctx) { + val sort = mkArraySort(sizeSort, regionId.sort) + val translatedDefaultValue = translate(regionId.defaultValue) + mkArrayConst(sort, translatedDefaultValue) + } + } + val updateTranslator = U1DArrayUpdateTranslate(this, initialValue) + return URegionTranslator(updateTranslator) + } + + override fun visit( + regionId: UInputArrayId, + ): URegionTranslator, USymbolicArrayIndex, Sort, *> { + require(regionId.defaultValue == null) + val initialValue = getOrPutInitialValue(regionId) { + with(regionId.sort.uctx) { + mkArraySort(addressSort, sizeSort, regionId.sort).mkConst(regionId.toString()) // TODO: replace toString + } + } + val updateTranslator = U2DArrayUpdateVisitor(this, initialValue) + return URegionTranslator(updateTranslator) + } + + override fun visit( + regionId: UInputArrayLengthId, + ): URegionTranslator, UHeapRef, USizeSort, *> { + require(regionId.defaultValue == null) + val initialValue = getOrPutInitialValue(regionId) { + with(regionId.sort.uctx) { + mkArraySort(addressSort, sizeSort).mkConst(regionId.toString()) // TODO: replace toString + } + } + val updateTranslator = U1DArrayUpdateTranslate(this, initialValue) + return URegionTranslator(updateTranslator) + } + + open fun buildTranslator( + regionId: URegionId, + ): URegionTranslator, Key, Sort, *> { + @Suppress("UNCHECKED_CAST") + return regionId.accept(this) as URegionTranslator, Key, Sort, *> + } +} + +/** + * Tracks translated symbols. This information used in [ULazyModelDecoder]. + */ +open class UCachingExprTranslator( + ctx: UContext, +) : UExprTranslator(ctx) { + + val registerIdxToTranslated = mutableMapOf>() + + override fun transform(expr: URegisterReading): UExpr = + registerIdxToTranslated.getOrPut(expr.idx) { + super.transform(expr) + }.cast() + + val indexedMethodReturnValueToTranslated = mutableMapOf, UExpr<*>>() + + override fun transform(expr: UIndexedMethodReturnValue): UExpr = + indexedMethodReturnValueToTranslated.getOrPut(expr.method to expr.callIndex) { + super.transform(expr) + }.cast() + + val translatedNullRef = super.transform(ctx.nullRef) + + val regionIdToTranslator = + mutableMapOf, URegionTranslator, *, *, *>>() + + override fun buildTranslator( + regionId: URegionId, + ): URegionTranslator, Key, Sort, *> = + regionIdToTranslator.getOrPut(regionId) { + super.buildTranslator(regionId).cast() + }.cast() +} \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt index 82c7ee47f9..e5eb5927a6 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt @@ -127,9 +127,9 @@ class URegisterReading internal constructor( } } -abstract class UHeapReading, Key, Sort : USort>( +abstract class UHeapReading, Key, Sort : USort>( ctx: UContext, - val region: UMemoryRegion + val region: USymbolicMemoryRegion ) : USymbol(ctx) { override val sort: Sort get() = region.sort } @@ -138,7 +138,7 @@ class UInputFieldReading internal constructor( ctx: UContext, region: UInputFieldRegion, val address: UHeapRef, -) : UHeapReading, UHeapRef, Sort>(ctx, region) { +) : UHeapReading, UHeapRef, Sort>(ctx, region) { @Suppress("UNCHECKED_CAST") override fun accept(transformer: KTransformerBase): KExpr { require(transformer is UExprTransformer<*, *>) @@ -162,7 +162,7 @@ class UAllocatedArrayReading internal constructor( ctx: UContext, region: UAllocatedArrayRegion, val index: USizeExpr, -) : UHeapReading, USizeExpr, Sort>(ctx, region) { +) : UHeapReading, USizeExpr, Sort>(ctx, region) { @Suppress("UNCHECKED_CAST") override fun accept(transformer: KTransformerBase): KExpr { require(transformer is UExprTransformer<*, *>) @@ -192,7 +192,7 @@ class UInputArrayReading internal constructor( region: UInputArrayRegion, val address: UHeapRef, val index: USizeExpr -) : UHeapReading, USymbolicArrayIndex, Sort>(ctx, region) { +) : UHeapReading, USymbolicArrayIndex, Sort>(ctx, region) { @Suppress("UNCHECKED_CAST") override fun accept(transformer: KTransformerBase): KExpr { require(transformer is UExprTransformer<*, *>) @@ -264,7 +264,7 @@ class UIndexedMethodReturnValue internal constructor( } override fun print(printer: ExpressionPrinter) { - TODO("Not yet implemented") + printer.append("$method:#$callIndex") } override fun internEquals(other: Any): Boolean = structurallyEqual(other, { method }, { callIndex }, { sort }) diff --git a/usvm-core/src/main/kotlin/org/usvm/Heap.kt b/usvm-core/src/main/kotlin/org/usvm/Heap.kt index aa9aac1c8a..fbb8e19010 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Heap.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Heap.kt @@ -1,40 +1,25 @@ package org.usvm -import org.ksmt.utils.asExpr import kotlinx.collections.immutable.PersistentMap import kotlinx.collections.immutable.persistentMapOf +import org.ksmt.utils.asExpr +import org.ksmt.utils.sampleValue interface UReadOnlyHeap { fun readField(ref: Ref, field: Field, sort: Sort): Value - fun readArrayIndex(ref: Ref, index: SizeT, arrayType: ArrayType, elementSort: Sort): Value + fun readArrayIndex(ref: Ref, index: SizeT, arrayType: ArrayType, sort: 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 + + fun nullRef(): Ref } typealias UReadOnlySymbolicHeap = UReadOnlyHeap, USizeExpr, Field, ArrayType, UBoolExpr> -class UEmptyHeap(private val ctx: UContext) : UReadOnlySymbolicHeap { - override fun readField(ref: UHeapRef, field: Field, sort: Sort): UExpr = - ctx.mkDefault(sort) - - override fun readArrayIndex( - ref: UHeapRef, - index: USizeExpr, - arrayType: ArrayType, - elementSort: Sort, - ): UExpr = ctx.mkDefault(elementSort) - - 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, guard: Guard) @@ -42,7 +27,7 @@ interface UHeap : ref: Ref, index: SizeT, type: ArrayType, - elementSort: Sort, + sort: Sort, value: Value, guard: Guard, ) @@ -61,10 +46,8 @@ interface UHeap : guard: Guard, ) - fun allocate(): UConcreteHeapAddress - fun allocateArray(count: SizeT): UConcreteHeapAddress - - fun clone(): UHeap + fun allocate(): UConcreteHeapRef + fun allocateArray(count: SizeT): UConcreteHeapRef } typealias USymbolicHeap = UHeap, USizeExpr, Field, ArrayType, UBoolExpr> @@ -76,8 +59,18 @@ typealias USymbolicHeap = UHeap, US * Copying is prohibited. */ class UAddressCounter { - private var lastAddress = 0 + private var lastAddress = INITIAL_CONCRETE_ADDRESS fun freshAddress(): UConcreteHeapAddress = lastAddress++ + + companion object { + // We split all addresses into three parts: + // * input values: [Int.MIN_VALUE..0), + // * null value: [0] + // * allocated values: (0..Int.MAX_VALUE] + const val NULL_ADDRESS = 0 + const val INITIAL_INPUT_ADDRESS = NULL_ADDRESS - 1 + const val INITIAL_CONCRETE_ADDRESS = NULL_ADDRESS + 1 + } } data class URegionHeap( @@ -95,9 +88,7 @@ data class URegionHeap( sort: Sort, ): UInputFieldRegion = inputFields[field].inputFieldsRegionUncheckedCast() - ?: emptyInputFieldRegion(field, sort) { key, region -> - ctx.mkInputFieldReading(region, key) - } + ?: emptyInputFieldRegion(field, sort) private fun allocatedArrayRegion( arrayType: ArrayType, @@ -105,32 +96,26 @@ data class URegionHeap( elementSort: Sort, ): UAllocatedArrayRegion = allocatedArrays[address].allocatedArrayRegionUncheckedCast() - ?: emptyAllocatedArrayRegion(arrayType, address, elementSort) { index, region -> - ctx.mkAllocatedArrayReading(region, index) - } + ?: emptyAllocatedArrayRegion(arrayType, address, elementSort) private fun inputArrayRegion( arrayType: ArrayType, elementSort: Sort, ): UInputArrayRegion = inputArrays[arrayType].inputArrayRegionUncheckedCast() - ?: emptyInputArrayRegion(arrayType, elementSort) { pair, region -> - ctx.mkInputArrayReading(region, pair.first, pair.second) - } + ?: emptyInputArrayRegion(arrayType, elementSort) private fun inputArrayLengthRegion( arrayType: ArrayType, ): UInputArrayLengthRegion = inputLengths[arrayType] - ?: emptyArrayLengthRegion(arrayType, ctx) { ref, region -> - ctx.mkInputArrayLengthReading(region, ref) - } + ?: emptyInputArrayLengthRegion(arrayType, ctx.sizeSort) override fun readField(ref: UHeapRef, field: Field, sort: Sort): UExpr = ref.map( { concreteRef -> allocatedFields - .getOrDefault(concreteRef.address to field, sort.defaultValue()) + .getOrDefault(concreteRef.address to field, sort.sampleValue()) .asExpr(sort) }, { symbolicRef -> inputFieldRegion(field, sort).read(symbolicRef) } @@ -140,11 +125,11 @@ data class URegionHeap( ref: UHeapRef, index: USizeExpr, arrayType: ArrayType, - elementSort: Sort, + sort: Sort, ): UExpr = ref.map( - { concreteRef -> allocatedArrayRegion(arrayType, concreteRef.address, elementSort).read(index) }, - { symbolicRef -> inputArrayRegion(arrayType, elementSort).read(symbolicRef to index) } + { concreteRef -> allocatedArrayRegion(arrayType, concreteRef.address, sort).read(index) }, + { symbolicRef -> inputArrayRegion(arrayType, sort).read(symbolicRef to index) } ) override fun readArrayLength(ref: UHeapRef, arrayType: ArrayType): USizeExpr = @@ -185,23 +170,23 @@ data class URegionHeap( ref: UHeapRef, index: USizeExpr, type: ArrayType, - elementSort: Sort, + sort: Sort, value: UExpr, guard: UBoolExpr, ) { - val valueToWrite = value.asExpr(elementSort) + val valueToWrite = value.asExpr(sort) withHeapRef( ref, guard, { (concreteRef, innerGuard) -> - val oldRegion = allocatedArrayRegion(type, concreteRef.address, elementSort) + val oldRegion = allocatedArrayRegion(type, concreteRef.address, sort) val newRegion = oldRegion.write(index, valueToWrite, innerGuard) allocatedArrays = allocatedArrays.put(concreteRef.address, newRegion) }, { (symbolicRef, innerGuard) -> - val region = inputArrayRegion(type, elementSort) - val newRegion = region.write(symbolicRef to index, valueToWrite, innerGuard) + val oldRegion = inputArrayRegion(type, sort) + val newRegion = oldRegion.write(symbolicRef to index, valueToWrite, innerGuard) inputArrays = inputArrays.put(type, newRegion) } ) @@ -300,23 +285,22 @@ data class URegionHeap( ) } - override fun allocate() = lastAddress.freshAddress() + override fun allocate() = ctx.mkConcreteHeapRef(lastAddress.freshAddress()) - override fun allocateArray(count: USizeExpr): UConcreteHeapAddress { + override fun allocateArray(count: USizeExpr): UConcreteHeapRef { val address = lastAddress.freshAddress() allocatedLengths = allocatedLengths.put(address, count) - return address + return ctx.mkConcreteHeapRef(address) } - override fun clone(): UHeap, USizeExpr, Field, ArrayType, UBoolExpr> = - URegionHeap( - ctx, lastAddress, - allocatedFields, inputFields, - allocatedArrays, inputArrays, - allocatedLengths, inputLengths - ) + override fun nullRef(): UHeapRef = ctx.nullRef - override fun toMutableHeap() = clone() + override fun toMutableHeap() = URegionHeap( + ctx, lastAddress, + allocatedFields, inputFields, + allocatedArrays, inputArrays, + allocatedLengths, inputLengths + ) } @Suppress("UNCHECKED_CAST") diff --git a/usvm-core/src/main/kotlin/org/usvm/HeapRefSplittingUtil.kt b/usvm-core/src/main/kotlin/org/usvm/HeapRefSplitting.kt similarity index 89% rename from usvm-core/src/main/kotlin/org/usvm/HeapRefSplittingUtil.kt rename to usvm-core/src/main/kotlin/org/usvm/HeapRefSplitting.kt index 65b43aea70..76ec02631c 100644 --- a/usvm-core/src/main/kotlin/org/usvm/HeapRefSplittingUtil.kt +++ b/usvm-core/src/main/kotlin/org/usvm/HeapRefSplitting.kt @@ -21,7 +21,10 @@ internal data class SplitHeapRefs( /** * Traverses the [ref] non-recursively and collects [UConcreteHeapRef]s and [USymbolicHeapRef] as well as - * guards for them. The result [SplitHeapRefs.symbolicHeapRef] will be `null` if there are no [USymbolicHeapRef]s as + * guards for them. If the object is not a [UConcreteHeapRef] nor a [USymbolicHeapRef], e.g. KConst, + * treats such an object as a [USymbolicHeapRef]. + * + * The result [SplitHeapRefs.symbolicHeapRef] will be `null` if there are no [USymbolicHeapRef]s as * leafs in the [ref] ite. Otherwise, it will contain an ite with the guard protecting from bubbled up concrete refs. * * @param initialGuard an initial value for the accumulated guard. @@ -30,12 +33,12 @@ internal fun splitUHeapRef(ref: UHeapRef, initialGuard: UBoolExpr = ref.ctx.true val concreteHeapRefs = mutableListOf>() val symbolicHeapRef = filter(ref, initialGuard) { guarded -> - if (guarded.expr is USymbolicHeapRef) { - true - } else { + if (guarded.expr is UConcreteHeapRef) { @Suppress("UNCHECKED_CAST") concreteHeapRefs += (guarded as GuardedExpr) false + } else { + true } } @@ -139,7 +142,7 @@ internal inline fun UHeapRef.map( * Filters [ref] non-recursively with [predicate] and returns the result. A guard in the argument of the * [predicate] consists of a predicate from the root to the passed leaf. * - * It's guaranteed that [predicate] will be called exactly once on each leaf. + * Guarantees that [predicate] will be called exactly once on each leaf. * * @return A guarded expression with the guard indicating that any leaf on which [predicate] returns `false` * is inaccessible. `Null` is returned when all leafs match [predicate]. @@ -150,9 +153,6 @@ internal inline fun filter( crossinline predicate: (GuardedExpr) -> Boolean, ): GuardedExpr? = with(ref.ctx) { when (ref) { - is USymbolicHeapRef, - is UConcreteHeapRef, - -> (ref with initialGuard).takeIf(predicate) is UIteExpr -> { /** * This code simulates DFS on a binary tree without an explicit recursion. Pair.second represents the first @@ -173,12 +173,12 @@ internal inline fun filter( is UIteExpr -> when (state) { LEFT_CHILD -> { nodeToChild += guarded to RIGHT_CHILD - val leftGuard = mkAndNoFlat(guardFromTop, cur.condition) + val leftGuard = mkAnd(guardFromTop, cur.condition, flat = false) nodeToChild += (cur.trueBranch with leftGuard) to LEFT_CHILD } RIGHT_CHILD -> { nodeToChild += guarded to DONE - val guardRhs = mkAndNoFlat(guardFromTop, !cur.condition) + val guardRhs = mkAnd(guardFromTop, !cur.condition, flat = false) nodeToChild += (cur.falseBranch with guardRhs) to LEFT_CHILD } DONE -> { @@ -188,9 +188,9 @@ internal inline fun filter( val lhs = completelyMapped.removeLast() val next = when { lhs != null && rhs != null -> { - val leftPart = mkOrNoFlat(!cur.condition, lhs.guard) + val leftPart = mkOr(!cur.condition, lhs.guard, flat = false) - val rightPart = mkOrNoFlat(cur.condition, rhs.guard) + val rightPart = mkOr(cur.condition, rhs.guard, flat = false) /** *``` @@ -203,15 +203,15 @@ internal inline fun filter( * lhs.expr | lhs.guard rhs.expr | rhs.guard *``` */ - val guard = mkAndNoFlat(leftPart, rightPart) + val guard = mkAnd(leftPart, rightPart, flat = false) mkIte(cur.condition, lhs.expr, rhs.expr) with guard } lhs != null -> { - val guard = mkAndNoFlat(listOf(cur.condition, lhs.guard)) + val guard = mkAnd(cur.condition, lhs.guard, flat = false) lhs.expr with guard } rhs != null -> { - val guard = mkAndNoFlat(listOf(!cur.condition, rhs.guard)) + val guard = mkAnd(!cur.condition, rhs.guard, flat = false) rhs.expr with guard } else -> null @@ -225,7 +225,6 @@ internal inline fun filter( completelyMapped.single()?.withAlso(initialGuard) } - - else -> error("Unexpected ref: $ref") + else -> (ref with initialGuard).takeIf(predicate) } } \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/LazyModelDecoder.kt b/usvm-core/src/main/kotlin/org/usvm/LazyModelDecoder.kt new file mode 100644 index 0000000000..d290132600 --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/LazyModelDecoder.kt @@ -0,0 +1,136 @@ +package org.usvm + +import org.ksmt.expr.KExpr +import org.ksmt.solver.KModel +import org.ksmt.sort.KUninterpretedSort +import org.usvm.UAddressCounter.Companion.INITIAL_INPUT_ADDRESS +import org.usvm.UAddressCounter.Companion.NULL_ADDRESS + +interface UModelDecoder { + fun decode(memory: Memory, model: KModel): Model +} + +/** + * Initializes [UExprTranslator] and [UModelDecoder] and returns them. We can safely reuse them while [UContext] is + * alive. + */ +fun buildTranslatorAndLazyDecoder( + ctx: UContext, +): Pair, ULazyModelDecoder> { + val translator = UCachingExprTranslator(ctx) + + val decoder = with(translator) { + ULazyModelDecoder( + registerIdxToTranslated, + indexedMethodReturnValueToTranslated, + translatedNullRef, + regionIdToTranslator.keys, + regionIdToInitialValue, + ) + } + + return translator to decoder +} + +typealias AddressesMapping = Map, UConcreteHeapRef> + + +/** + * A lazy decoder suitable for decoding [KModel] to [UModelBase]. It can't be reused between different root methods, + * because of a matched translator caches. + * + * Passed parameters updates on the fly in a matched translator, so they are mutable in fact. + * + * @param registerIdxToTranslated a mapping from a register idx to a translated expression. + * @param indexedMethodReturnValueToTranslated a mapping from an indexed mock symbol to a translated expression. + * @param translatedNullRef translated null reference. + * @param translatedRegionIds a set of translated region ids. + * @param regionIdToInitialValue an initial value provider, the same as used in the translator, so we can build + * concrete regions from a [KModel]. + */ +open class ULazyModelDecoder( + protected val registerIdxToTranslated: Map>, + protected val indexedMethodReturnValueToTranslated: Map, UExpr<*>>, + protected val translatedNullRef: UExpr, + protected val translatedRegionIds: Set>, + protected val regionIdToInitialValue: Map, KExpr<*>>, +) : UModelDecoder, UModelBase> { + private val ctx: UContext = translatedNullRef.uctx + + /** + * Build a mapping from instances of an uninterpreted [UAddressSort] + * to [UConcreteHeapRef] with integer addresses. It allows us to enumerate + * equivalence classes of addresses and work with their number in the future. + */ + private fun buildMapping(model: KModel): AddressesMapping { + // Null is a special value that we want to translate in any case. + val interpretedNullRef = model.eval(translatedNullRef, isComplete = true) + + val result = mutableMapOf, UConcreteHeapRef>() + // Except the null value, it has the NULL_ADDRESS + result[interpretedNullRef] = ctx.mkConcreteHeapRef(NULL_ADDRESS) + result[translatedNullRef] = ctx.mkConcreteHeapRef(NULL_ADDRESS) + + val universe = model.uninterpretedSortUniverse(ctx.addressSort) ?: return result + // All the numbers are enumerated from the INITIAL_INPUT_ADDRESS to the Int.MIN_VALUE + var counter = INITIAL_INPUT_ADDRESS + + for (interpretedAddress in universe) { + if (interpretedAddress == interpretedNullRef) { + continue + } + result[interpretedAddress] = ctx.mkConcreteHeapRef(counter--) + } + + return result + } + + /** + * Decodes a [model] from a [memory] to a [UModelBase]. + * + * @param model should be detached. + */ + override fun decode( + memory: UMemoryBase, + model: KModel, + ): UModelBase { + val addressesMapping = buildMapping(model) + + val stack = decodeStack(model, addressesMapping) + val heap = decodeHeap(model, addressesMapping) + val types = UTypeModel(ctx, memory.typeSystem, typeByAddr = emptyMap()) + val mocks = decodeMocker(model, addressesMapping) + + return UModelBase(ctx, stack, heap, types, mocks) + } + + private fun decodeStack(model: KModel, addressesMapping: AddressesMapping): ULazyRegistersStackModel = + ULazyRegistersStackModel( + model, + addressesMapping, + registerIdxToTranslated + ) + + /** + * Constructs a [ULazyHeapModel] for a heap by provided [model] and [addressesMapping]. + */ + private fun decodeHeap( + model: KModel, + addressesMapping: AddressesMapping, + ): ULazyHeapModel = ULazyHeapModel( + model, + addressesMapping.getValue(translatedNullRef), + addressesMapping, + regionIdToInitialValue, + ) + + private fun decodeMocker( + model: KModel, + addressesMapping: AddressesMapping, + ): ULazyIndexedMockModel = + ULazyIndexedMockModel( + model, + addressesMapping, + indexedMethodReturnValueToTranslated + ) +} diff --git a/usvm-core/src/main/kotlin/org/usvm/LazyModels.kt b/usvm-core/src/main/kotlin/org/usvm/LazyModels.kt new file mode 100644 index 0000000000..3a69d235f4 --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/LazyModels.kt @@ -0,0 +1,230 @@ +package org.usvm + +import org.ksmt.expr.KExpr +import org.ksmt.solver.KModel +import org.ksmt.utils.asExpr +import org.ksmt.utils.cast +import org.ksmt.utils.sampleValue + + +/** + * Since expressions from [this] might have the [UAddressSort] and therefore + * they could be uninterpreted constants, we have to replace them with + * corresponding concrete addresses from the [addressesMapping]. + */ +private fun Map>.evalAndReplace( + key: K, + model: KModel, + addressesMapping: AddressesMapping, + sort: T +): UExpr { + val value = get(key) + return if (value != null) { + model.eval(value, isComplete = true).mapAddress(addressesMapping).asExpr(sort) + } else { + sort.sampleValue().mapAddress(addressesMapping) + } +} + +/** + * A lazy model for registers. Firstly, searches for translated symbol, then evaluates it in [model]. + * + * @param registerIdxToTranslated a translated cache. + * @param model has to be detached. + */ +class ULazyRegistersStackModel( + private val model: KModel, + private val addressesMapping: AddressesMapping, + private val registerIdxToTranslated: Map> +) : URegistersStackEvaluator { + override fun eval( + registerIndex: Int, + sort: Sort, + ): UExpr = registerIdxToTranslated.evalAndReplace(key = registerIndex, model, addressesMapping, sort) +} + +/** + * A lazy model for an indexed mocker. Firstly, searches for translated symbol, then evaluates it in [model]. + * + * @param indexedMethodReturnValueToTranslated a translated cache. + * @param model has to be detached. + */ +class ULazyIndexedMockModel( + private val model: KModel, + private val addressesMapping: AddressesMapping, + private val indexedMethodReturnValueToTranslated: Map, UExpr<*>>, +) : UMockEvaluator { + + override fun eval(symbol: UMockSymbol): UExpr { + require(symbol is UIndexedMethodReturnValue<*, Sort>) + + val sort = symbol.sort + + @Suppress("UNCHECKED_CAST") + val key = symbol.method as Method to symbol.callIndex + + return indexedMethodReturnValueToTranslated.evalAndReplace(key = key, model, addressesMapping, sort) + } +} + +/** + * + * A lazy immutable heap model. Firstly, searches for decoded [UMemoryRegion], decodes it from [model] if not found, + * secondly, evaluates a value from it. + * + * Declared as mutable heap for using in regions composition in [UComposer]. Any call to + * modifying operation throws an exception. + * + * Any [UHeapReading] possibly writing to this heap in its [URegionId.instantiate] call actually has empty updates, + * because localization happened, so this heap won't be mutated. + * + * @param regionIdToInitialValue mapping from [URegionId] to initial values. We decode memory regions + * using this cache. + * @param model has to be detached. + */ +class ULazyHeapModel( + private val model: KModel, + private val nullRef: UConcreteHeapRef, + private val addressesMapping: AddressesMapping, + private val regionIdToInitialValue: Map, KExpr<*>>, +) : USymbolicHeap { + private val resolvedInputFields = mutableMapOf>() + private val resolvedInputArrays = mutableMapOf>() + private val resolvedInputLengths = mutableMapOf>() + override fun readField(ref: UHeapRef, field: Field, sort: Sort): UExpr { + // All the expressions in the model are interpreted, therefore, they must + // have concrete addresses. Moreover, the model knows only about input values + // which have addresses less or equal than INITIAL_INPUT_ADDRESS + require(ref is UConcreteHeapRef && ref.address <= UAddressCounter.INITIAL_INPUT_ADDRESS) + + val resolvedRegion = resolvedInputFields[field] + val initialValue = regionIdToInitialValue[UInputFieldId(field, sort, null)] + + return when { + resolvedRegion != null -> resolvedRegion.read(ref).asExpr(sort) + initialValue != null -> { + val region = UMemory1DArray(initialValue.cast(), model, addressesMapping) + resolvedInputFields[field] = region + region.read(ref) + } + + else -> sort.sampleValue().makeNullRefConcrete(nullRef) + } + } + + override fun readArrayIndex( + ref: UHeapRef, + index: USizeExpr, + arrayType: ArrayType, + sort: Sort, + ): UExpr { + // All the expressions in the model are interpreted, therefore, they must + // have concrete addresses. Moreover, the model knows only about input values + // which have addresses less or equal than INITIAL_INPUT_ADDRESS + require(ref is UConcreteHeapRef && ref.address <= UAddressCounter.INITIAL_INPUT_ADDRESS) + + val key = ref to index + + val resolvedRegion = resolvedInputArrays[arrayType] + val initialValue = regionIdToInitialValue[UInputArrayId(arrayType, sort, null)] + + return when { + resolvedRegion != null -> resolvedRegion.read(key).asExpr(sort) + initialValue != null -> { + val region = UMemory2DArray(initialValue.cast(), model, addressesMapping) + resolvedInputArrays[arrayType] = region + region.read(key) + } + + else -> sort.sampleValue().makeNullRefConcrete(nullRef) + } + } + + override fun readArrayLength(ref: UHeapRef, arrayType: ArrayType): USizeExpr { + // All the expressions in the model are interpreted, therefore, they must + // have concrete addresses. Moreover, the model knows only about input values + // which have addresses less or equal than INITIAL_INPUT_ADDRESS + require(ref is UConcreteHeapRef && ref.address <= UAddressCounter.INITIAL_INPUT_ADDRESS) + + val resolvedRegion = resolvedInputLengths[arrayType] + val sizeSort = ref.uctx.sizeSort + val initialValue = regionIdToInitialValue[UInputArrayLengthId(arrayType, sizeSort, null)] + + return when { + resolvedRegion != null -> resolvedRegion.read(ref) + initialValue != null -> { + val region = UMemory1DArray(initialValue.cast(), model, addressesMapping) + resolvedInputLengths[arrayType] = region + region.read(ref) + } + + else -> sizeSort.sampleValue() + } + } + + override fun writeField( + ref: UHeapRef, + field: Field, + sort: Sort, + value: UExpr, + guard: UBoolExpr, + ) = error("Illegal operation for a model") + + override fun writeArrayIndex( + ref: UHeapRef, + index: USizeExpr, + type: ArrayType, + sort: Sort, + value: UExpr, + guard: UBoolExpr, + ) = error("Illegal operation for a model") + + override fun writeArrayLength(ref: UHeapRef, size: USizeExpr, arrayType: ArrayType) = + error("Illegal operation for a model") + + override fun memcpy( + srcRef: UHeapRef, + dstRef: UHeapRef, + type: ArrayType, + elementSort: Sort, + fromSrcIdx: USizeExpr, + fromDstIdx: USizeExpr, + toDstIdx: USizeExpr, + guard: UBoolExpr, + ) = error("Illegal operation for a model") + + override fun memset( + ref: UHeapRef, + type: ArrayType, + sort: Sort, + contents: Sequence>, + ) = error("Illegal operation for a model") + + override fun allocate() = error("Illegal operation for a model") + + override fun allocateArray(count: USizeExpr) = error("Illegal operation for a model") + + override fun nullRef(): UConcreteHeapRef = nullRef + + override fun toMutableHeap(): ULazyHeapModel = this +} + +fun UExpr.makeNullRefConcrete(conreteNullRef: UConcreteHeapRef): UExpr = + if (this == uctx.nullRef) { + conreteNullRef.asExpr(sort) + } else { + this + } + +/** + * If [this] value is an instance of address expression, returns + * an expression with a corresponding concrete address, otherwise + * returns [this] unchanched. + */ +fun UExpr.mapAddress( + addressesMapping: AddressesMapping, +): UExpr = if (sort == uctx.addressSort) { + addressesMapping.getValue(asExpr(uctx.addressSort)).asExpr(sort) +} else { + this +} \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/Memory.kt b/usvm-core/src/main/kotlin/org/usvm/Memory.kt index 34553938c6..f262946b54 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Memory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Memory.kt @@ -60,11 +60,11 @@ typealias USymbolicMemory = UMemory, USizeExpr, @Suppress("MemberVisibilityCanBePrivate") open class UMemoryBase( protected val ctx: UContext, - protected val typeSystem: UTypeSystem, - protected var stack: URegistersStack = URegistersStack(ctx), - protected var heap: USymbolicHeap = URegionHeap(ctx), - protected var types: UTypeStorage = UTypeStorage(ctx, typeSystem), - protected var mocker: UMocker = UIndexedMocker(ctx) + val typeSystem: UTypeSystem, + val stack: URegistersStack = URegistersStack(ctx), + val heap: USymbolicHeap = URegionHeap(ctx), + val types: UTypeStorage = UTypeStorage(ctx, typeSystem), + val mocker: UMocker = UIndexedMocker(ctx) // TODO: we can eliminate mocker by moving compose to UState? ) : USymbolicMemory { @Suppress("UNCHECKED_CAST") @@ -91,15 +91,15 @@ open class UMemoryBase( } override fun alloc(type: Type): UHeapRef { - val address = heap.allocate() - types.allocate(address, type) - return ctx.mkConcreteHeapRef(address) + val concreteHeapRef = heap.allocate() + types.allocate(concreteHeapRef.address, type) + return concreteHeapRef } override fun malloc(arrayType: Type, count: USizeExpr): UHeapRef { - val address = heap.allocateArray(count) - types.allocate(address, arrayType) - return ctx.mkConcreteHeapRef(address) + val concreteHeapRef = heap.allocateArray(count) + types.allocate(concreteHeapRef.address, arrayType) + return concreteHeapRef } override fun memset(ref: UHeapRef, arrayType: Type, elementSort: USort, contents: Sequence>) = @@ -121,5 +121,5 @@ open class UMemoryBase( } override fun clone(): UMemoryBase = - UMemoryBase(ctx, typeSystem, stack.clone(), heap.clone(), types, mocker) + UMemoryBase(ctx, typeSystem, stack.clone(), heap.toMutableHeap(), types, mocker) } diff --git a/usvm-core/src/main/kotlin/org/usvm/MemoryRegions.kt b/usvm-core/src/main/kotlin/org/usvm/MemoryRegions.kt index 0571d139e0..158b6aad53 100644 --- a/usvm-core/src/main/kotlin/org/usvm/MemoryRegions.kt +++ b/usvm-core/src/main/kotlin/org/usvm/MemoryRegions.kt @@ -1,17 +1,18 @@ package org.usvm import org.ksmt.utils.asExpr +import org.ksmt.utils.sampleValue import org.usvm.util.SetRegion import org.usvm.util.emptyRegionTree -import java.util.* //region Memory region -/** - * A typealias for a lambda that takes a key, a region and returns a reading from the region by the key. - */ -typealias UInstantiator = (key: Key, UMemoryRegion) -> UExpr +interface UMemoryRegion { + fun read(key: Key): UExpr + fun write(key: Key, value: UExpr, guard: UBoolExpr): UMemoryRegion +} + /** * A uniform unbounded slice of memory. Indexed by [Key], stores symbolic values. @@ -22,13 +23,16 @@ typealias UInstantiator = (key: Key, UMemoryRegion, Key, Sort : USort>( +data class USymbolicMemoryRegion, Key, Sort : USort>( val regionId: RegionId, - val sort: Sort, val updates: UMemoryUpdates, - private val defaultValue: UExpr?, // If defaultValue = null then this region is filled with symbolics - private val instantiator: UInstantiator, -) { +) : UMemoryRegion { + // to save memory usage + val sort: Sort get() = regionId.sort + + // If we replace it with get(), we have to check for nullability in read function. + val defaultValue = regionId.defaultValue + private fun read(key: Key, updates: UMemoryUpdates): UExpr { val lastUpdatedElement = updates.lastUpdatedElementOrNull() @@ -50,10 +54,10 @@ data class UMemoryRegion, Key, Sort : USort>( this.copy(updates = updates) } - return instantiator(key, localizedRegion) + return regionId.instantiate(localizedRegion, key) } - fun read(key: Key): UExpr { + override fun read(key: Key): UExpr { if (sort == sort.uctx.addressSort) { // Here we split concrete heap addresses from symbolic ones to optimize further memory operations. return splittingRead(key) { it is UConcreteHeapRef } @@ -91,7 +95,7 @@ data class UMemoryRegion, Key, Sort : USort>( return readingWithBubbledWrites } - fun write(key: Key, value: UExpr, guard: UBoolExpr): UMemoryRegion { + override fun write(key: Key, value: UExpr, guard: UBoolExpr): USymbolicMemoryRegion { assert(value.sort == sort) val newUpdates = if (sort == sort.uctx.addressSort) { @@ -116,15 +120,15 @@ data class UMemoryRegion, Key, Sort : USort>( } /** - * Splits this [UMemoryRegion] on two parts: + * Splits this [USymbolicMemoryRegion] on two parts: * * Values of [UUpdateNode]s satisfying [predicate] are added to the [matchingWrites]. * * [UUpdateNode]s unsatisfying [predicate] remain in the result memory region. * * The [guardBuilder] is used to build guards for values added to [matchingWrites]. In the end, the [guardBuilder] * is updated and contains predicate indicating that the [key] can't be included in any of visited [UUpdateNode]s. * - * @return new [UMemoryRegion] without writes satisfying [predicate] or this [UMemoryRegion] if no matching writes - * were found. + * @return new [USymbolicMemoryRegion] without writes satisfying [predicate] or this [USymbolicMemoryRegion] if no + * matching writes were found. * @see [UMemoryUpdates.split], [splittingRead] */ internal fun split( @@ -132,16 +136,14 @@ data class UMemoryRegion, Key, Sort : USort>( predicate: (UExpr) -> Boolean, matchingWrites: MutableList>>, guardBuilder: GuardBuilder, - ): UMemoryRegion { - // TODO: either check in UMemoryRegion constructor that we do not construct memory region with + ): USymbolicMemoryRegion { + // TODO: either check in USymbolicMemoryRegion constructor that we do not construct memory region with // non-null reference as default value, or implement splitting by default value. assert(defaultValue == null || !predicate(defaultValue)) - val count = matchingWrites.size val splitUpdates = updates.read(key).split(key, predicate, matchingWrites, guardBuilder) - val sizeRemainedUnchanged = matchingWrites.size == count - return if (sizeRemainedUnchanged) { + return if (splitUpdates === updates) { this } else { this.copy(updates = splitUpdates) @@ -157,20 +159,16 @@ data class UMemoryRegion, Key, Sort : USort>( */ fun map( composer: UComposer, - instantiator: UInstantiator = this.instantiator, - ): UMemoryRegion { - // Map the updates and the default value + ): USymbolicMemoryRegion { + // Map the updates and the regionId + val mappedRegionId = regionId.map(composer) val mappedUpdates = updates.map(regionId.keyMapper(composer), composer) - val mappedDefaultValue = defaultValue?.let { composer.compose(it) } - // Note that we cannot use optimization with unchanged mappedUpdates and mappedDefaultValues here - // since in a new region we might have an updated instantiator. - // Therefore, we have to check their reference equality as well. - if (mappedUpdates === updates && mappedDefaultValue === defaultValue && instantiator === this.instantiator) { + if (mappedUpdates === updates && mappedRegionId === regionId) { return this } - return UMemoryRegion(regionId, sort, mappedUpdates, mappedDefaultValue, instantiator) + return USymbolicMemoryRegion(mappedRegionId, mappedUpdates) } @Suppress("UNCHECKED_CAST") @@ -178,8 +176,8 @@ data class UMemoryRegion, Key, Sort : USort>( // 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> -> { + is UPinpointUpdateNode -> regionId.write(heap, it.key, it.value, it.guard) + is URangedUpdateNode<*, *, Key, Sort> -> { it.region.applyTo(heap) val (srcFromRef, srcFromIdx) = it.keyConverter.srcSymbolicArrayIndex @@ -198,12 +196,13 @@ data class UMemoryRegion, Key, Sort : USort>( * with values from memory region [fromRegion] read from range * of addresses [[keyConverter].convert([fromKey]) : [keyConverter].convert([toKey])] */ - fun , SrcKey> copyRange( - fromRegion: UMemoryRegion, - fromKey: Key, toKey: Key, + fun , SrcKey> copyRange( + fromRegion: USymbolicMemoryRegion, + fromKey: Key, + toKey: Key, keyConverter: UMemoryKeyConverter, - guard: UBoolExpr, - ): UMemoryRegion { + guard: UBoolExpr + ): USymbolicMemoryRegion { val updatesCopy = updates.copyRange(fromRegion, fromKey, toKey, keyConverter, guard) return this.copy(updates = updatesCopy) } @@ -233,7 +232,7 @@ class GuardBuilder(nonMatchingUpdates: UBoolExpr) { * @return [expr] guarded by this guard builder. Implementation uses [UContext.mkAndNoFlat], because we accumulate * [nonMatchingUpdatesGuard] and otherwise it would take quadratic time. */ - fun guarded(expr: UBoolExpr): UBoolExpr = expr.ctx.mkAndNoFlat(nonMatchingUpdatesGuard, expr) + fun guarded(expr: UBoolExpr): UBoolExpr = expr.ctx.mkAnd(nonMatchingUpdatesGuard, expr, flat = false) } //endregion @@ -243,7 +242,7 @@ class GuardBuilder(nonMatchingUpdates: UBoolExpr) { typealias USymbolicArrayIndex = Pair fun heapRefEq(ref1: UHeapRef, ref2: UHeapRef): UBoolExpr = - ref1.uctx.mkHeapRefEq(ref1, ref2) // TODO: use simplified equality! + ref1.uctx.mkHeapRefEq(ref1, ref2) @Suppress("UNUSED_PARAMETER") fun heapRefCmpSymbolic(ref1: UHeapRef, ref2: UHeapRef): UBoolExpr = @@ -254,17 +253,16 @@ fun heapRefCmpConcrete(ref1: UHeapRef, ref2: UHeapRef): Boolean = error("Heap references should not be compared!") fun indexEq(idx1: USizeExpr, idx2: USizeExpr): UBoolExpr = - idx1.ctx.mkEq(idx1, idx2) // TODO: use simplified equality! + idx1.ctx.mkEq(idx1, idx2) fun indexLeSymbolic(idx1: USizeExpr, idx2: USizeExpr): UBoolExpr = - idx1.ctx.mkBvSignedLessOrEqualExpr(idx1, idx2) // TODO: use simplified comparison! + idx1.ctx.mkBvSignedLessOrEqualExpr(idx1, idx2) fun indexLeConcrete(idx1: USizeExpr, idx2: USizeExpr): Boolean = // TODO: to optimize things up, we could pass path constraints here and lookup the numeric bounds for idx1 and idx2 idx1 == idx2 || (idx1 is UConcreteSize && idx2 is UConcreteSize && idx1.numberValue <= idx2.numberValue) fun refIndexEq(idx1: USymbolicArrayIndex, idx2: USymbolicArrayIndex): UBoolExpr = with(idx1.first.ctx) { - // TODO: use simplified operations! return@with (idx1.first eq idx2.first) and indexEq(idx1.second, idx2.second) } @@ -301,10 +299,10 @@ fun refIndexRangeRegion( idx2: USymbolicArrayIndex, ): UArrayIndexRegion = indexRangeRegion(idx1.second, idx2.second) -typealias UInputFieldRegion = UMemoryRegion, UHeapRef, Sort> -typealias UAllocatedArrayRegion = UMemoryRegion, USizeExpr, Sort> -typealias UInputArrayRegion = UMemoryRegion, USymbolicArrayIndex, Sort> -typealias UInputArrayLengthRegion = UMemoryRegion, UHeapRef, USizeSort> +typealias UInputFieldRegion = USymbolicMemoryRegion, UHeapRef, Sort> +typealias UAllocatedArrayRegion = USymbolicMemoryRegion, USizeExpr, Sort> +typealias UInputArrayRegion = USymbolicMemoryRegion, USymbolicArrayIndex, Sort> +typealias UInputArrayLengthRegion = USymbolicMemoryRegion, UHeapRef, USizeSort> typealias KeyMapper = (Key) -> Key @@ -325,52 +323,43 @@ val UInputArrayLengthRegion.inputLengthArrayType fun emptyInputFieldRegion( field: Field, sort: Sort, - instantiator: UInstantiator, UHeapRef, Sort>, -): UInputFieldRegion = UMemoryRegion( - UInputFieldRegionId(field), - sort, - UEmptyUpdates(::heapRefEq, ::heapRefCmpConcrete, ::heapRefCmpSymbolic), - defaultValue = null, - instantiator -) +): UInputFieldRegion = + USymbolicMemoryRegion( + UInputFieldId(field, sort, contextHeap = null), + UFlatUpdates(::heapRefEq, ::heapRefCmpConcrete, ::heapRefCmpSymbolic) + ) fun emptyAllocatedArrayRegion( arrayType: ArrayType, address: UConcreteHeapAddress, sort: Sort, - instantiator: UInstantiator, USizeExpr, Sort>, ): UAllocatedArrayRegion { val updates = UTreeUpdates( updates = emptyRegionTree(), ::indexRegion, ::indexRangeRegion, ::indexEq, ::indexLeConcrete, ::indexLeSymbolic ) - val regionId = UAllocatedArrayId(arrayType, address) - return UMemoryRegion(regionId, sort, updates, sort.defaultValue(), instantiator) + val regionId = UAllocatedArrayId(arrayType, sort, sort.sampleValue(), address, contextHeap = null) + return USymbolicMemoryRegion(regionId, updates) } fun emptyInputArrayRegion( arrayType: ArrayType, sort: Sort, - instantiator: UInstantiator, USymbolicArrayIndex, Sort>, ): UInputArrayRegion { val updates = UTreeUpdates( updates = emptyRegionTree(), ::refIndexRegion, ::refIndexRangeRegion, ::refIndexEq, ::refIndexCmpConcrete, ::refIndexCmpSymbolic ) - return UMemoryRegion(UInputArrayId(arrayType), sort, updates, defaultValue = null, instantiator) + return USymbolicMemoryRegion(UInputArrayId(arrayType, sort, contextHeap = null), updates) } -fun emptyArrayLengthRegion( +fun emptyInputArrayLengthRegion( arrayType: ArrayType, - ctx: UContext, - instantiator: UInstantiator, UHeapRef, USizeSort>, + sizeSort: USizeSort, ): UInputArrayLengthRegion = - UMemoryRegion( - UInputArrayLengthId(arrayType), - ctx.sizeSort, - UEmptyUpdates(::heapRefEq, ::heapRefCmpConcrete, ::heapRefCmpSymbolic), - defaultValue = null, - instantiator + USymbolicMemoryRegion( + UInputArrayLengthId(arrayType, sizeSort, contextHeap = null), + UFlatUpdates(::heapRefEq, ::heapRefCmpConcrete, ::heapRefCmpSymbolic), ) //endregion diff --git a/usvm-core/src/main/kotlin/org/usvm/MemoryUpdates.kt b/usvm-core/src/main/kotlin/org/usvm/MemoryUpdates.kt index 8d89c95205..886aff7238 100644 --- a/usvm-core/src/main/kotlin/org/usvm/MemoryUpdates.kt +++ b/usvm-core/src/main/kotlin/org/usvm/MemoryUpdates.kt @@ -38,7 +38,7 @@ interface UMemoryUpdates : Sequence> { ): UMemoryUpdates /** - * Returns a mapped [UMemoryRegion] using [keyMapper] and [composer]. + * Returns a mapped [USymbolicMemoryRegion] using [keyMapper] and [composer]. * It is used in [UComposer] during memory composition. */ fun map(keyMapper: KeyMapper, composer: UComposer): UMemoryUpdates @@ -47,10 +47,10 @@ interface UMemoryUpdates : Sequence> { * @return Updates which express copying the slice of [fromRegion] guarded with * condition [guard]. * - * @see UMemoryRegion.copyRange + * @see USymbolicMemoryRegion.copyRange */ - fun , SrcKey> copyRange( - fromRegion: UMemoryRegion, + fun , SrcKey> copyRange( + fromRegion: USymbolicMemoryRegion, fromKey: Key, toKey: Key, keyConverter: UMemoryKeyConverter, @@ -69,92 +69,80 @@ interface UMemoryUpdates : Sequence> { * 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 - ) + /** + * Accepts the [visitor]. Implementations should call [UMemoryUpdatesVisitor.visitInitialValue] firstly, then call + * [UMemoryUpdatesVisitor.visitUpdateNode] in the chronological order + * (from the oldest to the newest) with accumulated [Result]. + * + * Uses [lookupCache] to shortcut the traversal. The actual key is determined by the + * [UMemoryUpdates] implementation. A caller is responsible to maintain the lifetime of the [lookupCache]. + * + * @return the final result. + */ + fun accept( + visitor: UMemoryUpdatesVisitor, + lookupCache: MutableMap, + ): Result +} - override fun split( - key: Key, - predicate: (UExpr) -> Boolean, - matchingWrites: MutableList>>, - guardBuilder: GuardBuilder, - ) = this +/** + * A generic memory updates visitor. Doesn't think about a cache. + */ +interface UMemoryUpdatesVisitor { + fun visitSelect(result: Result, key: Key): UExpr - override fun map( - keyMapper: KeyMapper, - composer: UComposer, - ): UEmptyUpdates = this + fun visitInitialValue(): Result - override fun iterator(): Iterator> = EmptyIterator() + fun visitUpdate(previous: Result, update: UUpdateNode): Result +} - 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 -} +//region Flat memory updates -data class UFlatUpdates( - val node: UUpdateNode, - val next: UMemoryUpdates?, +class UFlatUpdates private constructor( + internal val node: UFlatUpdatesNode?, 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 + constructor( + symbolicEq: (Key, Key) -> UBoolExpr, + concreteCmp: (Key, Key) -> Boolean, + symbolicCmp: (Key, Key) -> UBoolExpr, + ) : this(node = null, symbolicEq, concreteCmp, symbolicCmp) + + internal data class UFlatUpdatesNode( + val update: UUpdateNode, + val next: UFlatUpdates, + ) + + override fun read(key: Key): UFlatUpdates = + when { + node != null && node.update.includesSymbolically(key).isFalse -> node.next.read(key) + else -> this + } override fun write(key: Key, value: UExpr, guard: UBoolExpr): UFlatUpdates = UFlatUpdates( - UPinpointUpdateNode(key, value, symbolicEq, guard), - next = this, + UFlatUpdatesNode(UPinpointUpdateNode(key, value, symbolicEq, guard), this), symbolicEq, concreteCmp, symbolicCmp ) - override fun , SrcKey> copyRange( - fromRegion: UMemoryRegion, + override fun , SrcKey> copyRange( + fromRegion: USymbolicMemoryRegion, fromKey: Key, toKey: Key, keyConverter: UMemoryKeyConverter, guard: UBoolExpr, ): UMemoryUpdates = UFlatUpdates( - URangedUpdateNode(fromKey, toKey, fromRegion, concreteCmp, symbolicCmp, keyConverter, guard), - next = this, + UFlatUpdatesNode( + URangedUpdateNode(fromKey, toKey, fromRegion, concreteCmp, symbolicCmp, keyConverter, guard), + this + ), symbolicEq, concreteCmp, symbolicCmp @@ -165,36 +153,38 @@ data class UFlatUpdates( predicate: (UExpr) -> Boolean, matchingWrites: MutableList>>, guardBuilder: GuardBuilder, - ): UMemoryUpdates { - val splitNode = node.split(key, predicate, matchingWrites, guardBuilder) - val splitNext = next?.split(key, predicate, matchingWrites, guardBuilder) + ): UFlatUpdates { + node ?: return this + val splitNode = node.update.split(key, predicate, matchingWrites, guardBuilder) + val splitNext = node.next.split(key, predicate, matchingWrites, guardBuilder) if (splitNode == null) { - return splitNext ?: UEmptyUpdates(symbolicEq, concreteCmp, symbolicCmp) + return splitNext } - if (splitNext === next) { + if (splitNext === node.next && splitNode === node.update) { return this } - return UFlatUpdates(splitNode, splitNext, symbolicEq, concreteCmp, symbolicCmp) + return UFlatUpdates(UFlatUpdatesNode(splitNode, splitNext), symbolicEq, concreteCmp, symbolicCmp) } override fun map( keyMapper: KeyMapper, - composer: UComposer, + composer: UComposer ): UFlatUpdates { + node ?: return this // Map the current node and the next values recursively - val mappedNode = node.map(keyMapper, composer) - val mappedNext = next?.map(keyMapper, composer) + val mappedNode = node.update.map(keyMapper, composer) + val mappedNext = node.next.map(keyMapper, composer) // If nothing changed, return this updates - if (mappedNode === node && mappedNext === next) { + if (mappedNode === node.update && mappedNext === node.next) { return this } // Otherwise, construct a new one using the mapped values - return UFlatUpdates(mappedNode, mappedNext, symbolicEq, concreteCmp, symbolicCmp) + return UFlatUpdates(UFlatUpdatesNode(mappedNode, mappedNext), symbolicEq, concreteCmp, symbolicCmp) } /** @@ -210,14 +200,13 @@ data class UFlatUpdates( init { val elements = mutableListOf>() - var current: UFlatUpdates? = initialNode + 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 + while (true) { + val node = current.node ?: break + elements += node.update + current = node.next } iterator = elements.asReversed().iterator() @@ -228,9 +217,27 @@ data class UFlatUpdates( override fun next(): UUpdateNode = iterator.next() } - override fun lastUpdatedElementOrNull(): UUpdateNode = node - - override fun isEmpty(): Boolean = false + override fun lastUpdatedElementOrNull(): UUpdateNode? = node?.update + + override fun isEmpty(): Boolean = node == null + + override fun accept( + visitor: UMemoryUpdatesVisitor, + lookupCache: MutableMap, + ): Result = UFlatMemoryUpdatesFolder(visitor, lookupCache).fold() + + private inner class UFlatMemoryUpdatesFolder( + private val visitor: UMemoryUpdatesVisitor, + private val cache: MutableMap, + ) { + fun fold() = foldFlatUpdates(this@UFlatUpdates) + private fun foldFlatUpdates(updates: UFlatUpdates): Result = + cache.getOrPut(updates) { + val node = updates.node ?: return@getOrPut visitor.visitInitialValue() + val accumulated = foldFlatUpdates(node.next) + visitor.visitUpdate(accumulated, node.update) + } + } } //endregion @@ -266,13 +273,13 @@ data class UTreeUpdates, Sort : USort>( return this.copy(updates = newUpdates) } - override fun , SrcKey> copyRange( - fromRegion: UMemoryRegion, + override fun , SrcKey> copyRange( + fromRegion: USymbolicMemoryRegion, fromKey: Key, toKey: Key, keyConverter: UMemoryKeyConverter, - guard: UBoolExpr, - ): UMemoryUpdates { + guard: UBoolExpr + ): UTreeUpdates { val region = keyRangeToRegion(fromKey, toKey) val update = URangedUpdateNode(fromKey, toKey, fromRegion, concreteCmp, symbolicCmp, keyConverter, guard) val newUpdates = updates.write( @@ -289,7 +296,7 @@ data class UTreeUpdates, Sort : USort>( predicate: (UExpr) -> Boolean, matchingWrites: MutableList>>, guardBuilder: GuardBuilder, - ): UMemoryUpdates { + ): UTreeUpdates { // the suffix of the [updates], starting from the earliest update satisfying `predicate(update.value(key))` val updatesSuffix = mutableListOf?>() @@ -300,7 +307,7 @@ data class UTreeUpdates, Sort : USort>( fun applyUpdate(update: UUpdateNode) { val region = when (update) { is UPinpointUpdateNode -> keyToRegion(update.key) - is URangedUpdateNode<*, *, *, Key, Sort> -> keyRangeToRegion(update.fromKey, update.toKey) + is URangedUpdateNode<*, *, Key, Sort> -> keyRangeToRegion(update.fromKey, update.toKey) } splitUpdates = splitUpdates.write(region, update, keyFilter = { it.isIncludedByUpdateConcretely(update) }) } @@ -377,8 +384,8 @@ data class UTreeUpdates, Sort : USort>( oldRegion.intersect(currentRegion) } - is URangedUpdateNode<*, *, *, Key, Sort> -> { - mappedUpdateNode as URangedUpdateNode<*, *, *, Key, Sort> + is URangedUpdateNode<*, *, Key, Sort> -> { + mappedUpdateNode as URangedUpdateNode<*, *, Key, Sort> val currentRegion = keyRangeToRegion(mappedUpdateNode.fromKey, mappedUpdateNode.toKey) oldRegion.intersect(currentRegion) } @@ -424,14 +431,7 @@ data class UTreeUpdates, Sort : USort>( 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 + val wasCloned = checkWasCloned(update, 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, @@ -461,10 +461,96 @@ data class UTreeUpdates, Sort : USort>( } } + internal fun checkWasCloned(update: UUpdateNode, region: Region<*>): Boolean { + // 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 + return wasCloned + } + override fun lastUpdatedElementOrNull(): UUpdateNode? = updates.entries.entries.lastOrNull()?.value?.first override fun isEmpty(): Boolean = updates.entries.isEmpty() + override fun accept( + visitor: UMemoryUpdatesVisitor, + lookupCache: MutableMap, + ): Result = UTreeMemoryUpdatesFolder(visitor, lookupCache).fold() + + private inner class UTreeMemoryUpdatesFolder( + private val visitor: UMemoryUpdatesVisitor, + private val cache: MutableMap, + ) { + fun fold(): Result = + cache.getOrPut(updates) { + leftMostFold(updates) + } + + private val emittedUpdates = hashSetOf>() + + /** + * [leftMostFold] visits only nodes marked by a star `*`. + * Nodes marked by an at `@` visited in [notLeftMostFold]. + * + * ``` + * * @ + * / \ + * / \ + * * @ @ @@ + * / | \ + * / @@ @@ + * * + *``` + */ + private fun leftMostFold(updates: RegionTree, *>): Result { + var result = cache[updates] + + if (result != null) { + return result + } + + val entryIterator = updates.entries.iterator() + if (!entryIterator.hasNext()) { + return visitor.visitInitialValue() + } + val (update, nextUpdates) = entryIterator.next().value + result = leftMostFold(nextUpdates) + result = visitor.visitUpdate(result, update) + return notLeftMostFold(result, entryIterator) + } + + private fun notLeftMostFold( + accumulator: Result, + iterator: Iterator, Pair, RegionTree, *>>>>, + ): Result { + var accumulated = accumulator + while (iterator.hasNext()) { + val (reg, entry) = iterator.next() + val (update, tree) = entry + accumulated = notLeftMostFold(accumulated, tree.entries.iterator()) + + accumulated = addIfNeeded(accumulated, update, reg) + } + return accumulated + } + + private fun addIfNeeded(accumulated: Result, update: UUpdateNode, region: Region<*>): Result { + if (checkWasCloned(update, region)) { + if (update in emittedUpdates) { + return accumulated + } + emittedUpdates += update + visitor.visitUpdate(accumulated, update) + } + + return visitor.visitUpdate(accumulated, update) + } + } } //endregion \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/Mocks.kt b/usvm-core/src/main/kotlin/org/usvm/Mocks.kt index 184e8c926e..48738d5286 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Mocks.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Mocks.kt @@ -1,7 +1,5 @@ package org.usvm -import org.ksmt.solver.KModel -import org.ksmt.utils.asExpr import kotlinx.collections.immutable.PersistentList import kotlinx.collections.immutable.PersistentMap import kotlinx.collections.immutable.persistentListOf @@ -11,18 +9,12 @@ interface UMockEvaluator { fun eval(symbol: UMockSymbol): UExpr } -class UIndexedMockModel(val map: Map, UExpr>) : UMockEvaluator { - override fun eval(symbol: UMockSymbol): UExpr = map.getValue(symbol).asExpr(symbol.sort) -} - interface UMocker : UMockEvaluator { fun call( method: Method, args: Sequence>, sort: Sort ): Pair, UMocker> - - fun decode(model: KModel): UMockEvaluator } class UIndexedMocker( @@ -41,9 +33,5 @@ class UIndexedMocker( return Pair(const, UIndexedMocker(ctx, updatedClauses)) } - override fun decode(model: KModel): UMockEvaluator { - TODO("Not yet implemented") - } - override fun eval(symbol: UMockSymbol): UExpr = symbol } diff --git a/usvm-core/src/main/kotlin/org/usvm/Model.kt b/usvm-core/src/main/kotlin/org/usvm/Model.kt index 444e6f5e94..d2a492783b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Model.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Model.kt @@ -6,17 +6,21 @@ interface UModel { // TODO: Eval visitor +/** + * Consists of decoded components and allows to evaluate any expression. Evaluation is done via generic composition. + * Evaluated expressions are cached within [UModelBase] instance. + * If a symbol from an expression not found inside the model, components return the default value + * of the correct sort. + */ open class UModelBase( - private val ctx: UContext, - val stack: URegistersStackModel, + ctx: UContext, + val stack: ULazyRegistersStackModel, val heap: UReadOnlySymbolicHeap, val types: UTypeModel, val mocks: UMockEvaluator -) - : UModel -{ - override fun eval(expr: UExpr): UExpr { - val composer = UComposer(ctx, stack, heap, types, mocks) - return composer.compose(expr) - } +) : UModel { + private val composer = UComposer(ctx, stack, heap, types, mocks) + + override fun eval(expr: UExpr): UExpr = + composer.compose(expr) } \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/ModelRegions.kt b/usvm-core/src/main/kotlin/org/usvm/ModelRegions.kt new file mode 100644 index 0000000000..27df1e9a1d --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/ModelRegions.kt @@ -0,0 +1,156 @@ +package org.usvm + +import kotlinx.collections.immutable.PersistentMap +import kotlinx.collections.immutable.persistentMapOf +import kotlinx.collections.immutable.toPersistentMap +import org.ksmt.expr.* +import org.ksmt.solver.KModel +import org.ksmt.sort.KArray2Sort +import org.ksmt.sort.KArraySort + + +/** + * A specific [UMemoryRegion] for one-dimensional regions generalized by a single expression of a [KeySort]. + */ +class UMemory1DArray internal constructor( + private val values: PersistentMap, UExpr>, + private val constValue: UExpr, +) : UMemoryRegion, Sort> { + + /** + * A constructor that is used in cases when we try to evaluate + * an expression from a region that was never translated. + */ + constructor( + mappedConstValue: UExpr, + ) : this(persistentMapOf(), mappedConstValue) + + override fun read(key: KExpr): UExpr = values.getOrDefault(key, constValue) + + override fun write( + key: KExpr, + value: UExpr, + guard: UBoolExpr + ): UMemoryRegion, Sort> { + when { + guard.isFalse -> return this + else -> require(guard.isTrue) + } + val newMap = values.put(key, value) + return UMemory1DArray(newMap, constValue) + } + + + companion object { + /** + * A constructor that is used in regular cases for a region + * that has a corresponding translator. It collects information + * required for the region decoding using data about translated expressions, + * resolved values from the [model] and the [mapping] from address expressions + * to their concrete representation. + */ + operator fun invoke( + initialValue: KConst>, + model: KModel, + mapping: Map, + ): UMemory1DArray { + // Since the model contains only information about values we got from the outside, + // we can translate and ask only about an initial value for the region. + // All other values should be resolved earlier without asking the model. + val evaluatedArray = model.eval(initialValue, isComplete = true) + + var valueCopy = evaluatedArray + + val stores = mutableMapOf, UExpr>() + + // Parse stores into the region, then collect a const value for the evaluated region. + while (valueCopy !is KArrayConst<*, *>) { + require(valueCopy is KArrayStore) + + val value = valueCopy.value.mapAddress(mapping) + + val mapAddress = valueCopy.index.mapAddress(mapping) + stores[mapAddress] = value + valueCopy = valueCopy.array + } + @Suppress("UNCHECKED_CAST") + valueCopy as KArrayConst, Sort> + + val constValue = valueCopy.value.mapAddress(mapping) + return UMemory1DArray(stores.toPersistentMap(), constValue) + } + } +} + +/** + * A specific [UMemoryRegion] for two-dimensional regions generalized by a pair + * of two expressions with [Key1Sort] and [Key2Sort] sorts. + */ +class UMemory2DArray internal constructor( + val values: PersistentMap, UExpr>, UExpr>, + val constValue: UExpr, +) : UMemoryRegion, KExpr>, Sort> { + /** + * A constructor that is used in cases when we try to evaluate + * an expression from a region that was never translated. + */ + constructor( + mappedConstValue: UExpr, + ) : this(persistentMapOf(), mappedConstValue) + + override fun read(key: Pair, KExpr>): UExpr { + return values.getOrDefault(key, constValue) + } + + override fun write( + key: Pair, KExpr>, + value: UExpr, + guard: UBoolExpr + ): UMemoryRegion, KExpr>, Sort> { + when { + guard.isFalse -> return this + else -> require(guard.isTrue) + } + val newMap = values.put(key, value) + return UMemory2DArray(newMap, constValue) + } + + companion object { + /** + * A constructor that is used in regular cases for a region + * that has a corresponding translator. It collects information + * required for the region decoding using data about translated expressions, + * resolved values from the [model] and the [mapping] from address expressions + * to their concrete representation. + */ + operator fun invoke( + initialValue: KExpr>, + model: KModel, + mapping: Map, + ): UMemory2DArray { + val evaluatedArray = model.eval(initialValue, isComplete = true) + + var valueCopy = evaluatedArray + + val stores = mutableMapOf, UExpr>, UExpr>() + + while (valueCopy !is KArrayConst<*, *>) { + require(valueCopy is KArray2Store) + + val value = valueCopy.value.mapAddress(mapping) + + val index0 = valueCopy.index0.mapAddress(mapping) + val index1 = valueCopy.index1.mapAddress(mapping) + + stores[index0 to index1] = value + valueCopy = valueCopy.array + } + + @Suppress("UNCHECKED_CAST") + valueCopy as KArrayConst, Sort> + + val constValue = valueCopy.value.mapAddress(mapping) + return UMemory2DArray(stores.toPersistentMap(), constValue) + } + } +} \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/PathCondition.kt b/usvm-core/src/main/kotlin/org/usvm/PathCondition.kt index 9207f865e6..652ecdb9cd 100644 --- a/usvm-core/src/main/kotlin/org/usvm/PathCondition.kt +++ b/usvm-core/src/main/kotlin/org/usvm/PathCondition.kt @@ -3,28 +3,30 @@ package org.usvm import kotlinx.collections.immutable.PersistentSet import kotlinx.collections.immutable.persistentSetOf -interface UPathCondition: Sequence { +interface UPathCondition : Collection { val isFalse: Boolean - fun add(constraint: UBoolExpr): UPathCondition + operator fun plus(constraint: UBoolExpr): UPathCondition } -class UPathConstraintsSet(private val ctx: UContext, - private val constraints: PersistentSet = persistentSetOf() -) - : UPathCondition -{ - fun contradiction() = - UPathConstraintsSet(ctx, persistentSetOf(ctx.mkFalse())) +class UPathConstraintsSet( + private val constraints: PersistentSet = persistentSetOf(), +) : Collection by constraints, UPathCondition { + constructor(constraint: UBoolExpr) : this(persistentSetOf(constraint)) override val isFalse: Boolean get() = constraints.size == 1 && constraints.first() is UFalse - override fun add(constraint: UBoolExpr): UPathCondition { - val notConstraint = constraint.ctx.mkNot(constraint) - if (constraints.contains(notConstraint)) - return contradiction() - return UPathConstraintsSet(ctx, constraints.add(constraint)) + override operator fun plus(constraint: UBoolExpr): UPathCondition { + val ctx = constraint.uctx + val notConstraint = ctx.mkNot(constraint) + if (constraints.contains(notConstraint)) { + return contradiction(ctx) + } + return UPathConstraintsSet(constraints.add(constraint)) } - override fun iterator(): Iterator = constraints.iterator() + companion object { + fun contradiction(ctx: UContext) = + UPathConstraintsSet(persistentSetOf(ctx.mkFalse())) + } } diff --git a/usvm-core/src/main/kotlin/org/usvm/RegionIds.kt b/usvm-core/src/main/kotlin/org/usvm/RegionIds.kt index 1b00f6653f..d36567018f 100644 --- a/usvm-core/src/main/kotlin/org/usvm/RegionIds.kt +++ b/usvm-core/src/main/kotlin/org/usvm/RegionIds.kt @@ -2,60 +2,95 @@ package org.usvm import org.ksmt.utils.asExpr - /** - * An interface that represents any possible type of regions that can be used in the memory. + * Represents any possible type of regions that can be used in the memory. */ -interface URegionId { - fun read( - key: Key, - sort: Sort, - heap: UReadOnlySymbolicHeap, - ): UExpr +interface URegionId> { + val sort: Sort - fun write( - key: Key, - sort: Sort, + val defaultValue: UExpr? + + /** + * Performs a reading from a [region] by a [key]. Inheritors uses context heap in memory regions composition. + */ + fun instantiate(region: USymbolicMemoryRegion<@UnsafeVariance RegionId, Key, Sort>, key: Key): UExpr + + fun write( heap: USymbolicHeap, + key: Key, value: UExpr, guard: UBoolExpr, ) - fun keyMapper(composer: UComposer): KeyMapper + fun keyMapper(transformer: UExprTransformer): KeyMapper + + fun map(composer: UComposer): RegionId + + fun accept(visitor: URegionIdVisitor): R +} + +interface URegionIdVisitor { + fun > visit(regionId: URegionId): Any? = + error("You must provide visit implementation for ${regionId::class} in ${this::class}") + + fun visit(regionId: UInputFieldId): R + + fun visit(regionId: UAllocatedArrayId): R + + fun visit(regionId: UInputArrayId): R + + fun visit(regionId: UInputArrayLengthId): R } /** * A region id for a region storing the specific [field]. */ -data class UInputFieldRegionId internal constructor( +data class UInputFieldId 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) + override val sort: Sort, + val contextHeap: USymbolicHeap?, +) : URegionId> { + + override val defaultValue: UExpr? get() = null + + override fun instantiate( + region: USymbolicMemoryRegion, UHeapRef, Sort>, + key: UHeapRef + ): UExpr = if (contextHeap == null) { + sort.uctx.mkInputFieldReading(region, key) + } else { + region.applyTo(contextHeap) + contextHeap.readField(key, field, sort).asExpr(sort) + } @Suppress("UNCHECKED_CAST") - override fun write( - key: UHeapRef, - sort: Sort, + override fun write( heap: USymbolicHeap, + key: UHeapRef, value: UExpr, guard: UBoolExpr, ) = heap.writeField(key, field as Field, sort, value, guard) override fun keyMapper( - composer: UComposer, - ): KeyMapper = { composer.compose(it) } + transformer: UExprTransformer, + ): KeyMapper = { transformer.apply(it) } + + override fun map(composer: UComposer): UInputFieldId { + check(contextHeap == null) { "contextHeap is not null in composition" } + @Suppress("UNCHECKED_CAST") + return copy(contextHeap = composer.heapEvaluator.toMutableHeap() as USymbolicHeap) + } + + override fun accept(visitor: URegionIdVisitor): R = + visitor.visit(this) override fun toString(): String { return "inputField($field)" } } -interface UArrayId : URegionId { +interface UArrayId> : + URegionId { val arrayType: ArrayType } @@ -63,25 +98,29 @@ interface UArrayId : URegionId { * 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( +data class UAllocatedArrayId internal constructor( override val arrayType: ArrayType, + override val sort: Sort, + override val defaultValue: UExpr, val address: UConcreteHeapAddress, -) : UArrayId { - @Suppress("UNCHECKED_CAST") - override fun read( - key: USizeExpr, - sort: Sort, - heap: UReadOnlySymbolicHeap, - ): UExpr { + val contextHeap: USymbolicHeap<*, ArrayType>?, +) : UArrayId> { + + override fun instantiate( + region: USymbolicMemoryRegion, USizeExpr, Sort>, + key: USizeExpr + ): UExpr = if (contextHeap == null) { + sort.uctx.mkAllocatedArrayReading(region, key) + } else { + region.applyTo(contextHeap) val ref = key.uctx.mkConcreteHeapRef(address) - return heap.readArrayIndex(ref, key, arrayType as ArrayType, sort).asExpr(sort) + contextHeap.readArrayIndex(ref, key, arrayType, sort).asExpr(sort) } @Suppress("UNCHECKED_CAST") - override fun write( - key: USizeExpr, - sort: Sort, + override fun write( heap: USymbolicHeap, + key: USizeExpr, value: UExpr, guard: UBoolExpr, ) { @@ -89,22 +128,37 @@ data class UAllocatedArrayId internal constructor( heap.writeArrayIndex(ref, key, arrayType as ArrayType, sort, value, guard) } + override fun keyMapper( - composer: UComposer, - ): KeyMapper = { composer.compose(it) } + transformer: UExprTransformer, + ): KeyMapper = { transformer.apply(it) } + + + override fun map(composer: UComposer): UAllocatedArrayId { + val composedDefaultValue = composer.compose(defaultValue) + check(contextHeap == null) { "contextHeap is not null in composition" } + @Suppress("UNCHECKED_CAST") + return copy( + contextHeap = composer.heapEvaluator.toMutableHeap() as USymbolicHeap<*, ArrayType>, + defaultValue = composedDefaultValue + ) + } // 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<*> + other as UAllocatedArrayId<*, *> if (address != other.address) return false return true } + override fun accept(visitor: URegionIdVisitor): R = + visitor.visit(this) + override fun hashCode(): Int { return address } @@ -117,33 +171,46 @@ data class UAllocatedArrayId internal constructor( /** * A region id for a region storing arrays retrieved as a symbolic value, contains only its [arrayType]. */ -data class UInputArrayId internal constructor( +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) + override val sort: Sort, + val contextHeap: USymbolicHeap<*, ArrayType>?, +) : UArrayId> { + override val defaultValue: UExpr? get() = null + override fun instantiate( + region: USymbolicMemoryRegion, USymbolicArrayIndex, Sort>, + key: USymbolicArrayIndex + ): UExpr = if (contextHeap == null) { + sort.uctx.mkInputArrayReading(region, key.first, key.second) + } else { + region.applyTo(contextHeap) + contextHeap.readArrayIndex(key.first, key.second, arrayType, sort).asExpr(sort) + } @Suppress("UNCHECKED_CAST") - override fun write( - key: USymbolicArrayIndex, - sort: Sort, + override fun write( heap: USymbolicHeap, + key: USymbolicArrayIndex, value: UExpr, guard: UBoolExpr, ) = heap.writeArrayIndex(key.first, key.second, arrayType as ArrayType, sort, value, guard) override fun keyMapper( - composer: UComposer, + transformer: UExprTransformer, ): KeyMapper = { - val ref = composer.compose(it.first) - val idx = composer.compose(it.second) + val ref = transformer.apply(it.first) + val idx = transformer.apply(it.second) if (ref === it.first && idx === it.second) it else ref to idx } + override fun accept(visitor: URegionIdVisitor): R = + visitor.visit(this) + + override fun map(composer: UComposer): UInputArrayId { + check(contextHeap == null) { "contextHeap is not null in composition" } + @Suppress("UNCHECKED_CAST") + return copy(contextHeap = composer.heapEvaluator.toMutableHeap() as USymbolicHeap<*, ArrayType>) + } override fun toString(): String { return "inputArray($arrayType)" } @@ -154,20 +221,25 @@ data class UInputArrayId internal constructor( */ 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) + override val sort: USizeSort, + val contextHeap: USymbolicHeap<*, ArrayType>?, +) : URegionId> { + override val defaultValue: UExpr? get() = null + override fun instantiate( + region: USymbolicMemoryRegion, UHeapRef, USizeSort>, + key: UHeapRef + ): UExpr = if (contextHeap == null) { + sort.uctx.mkInputArrayLengthReading(region, key) + } else { + region.applyTo(contextHeap) + contextHeap.readArrayLength(key, arrayType) + } @Suppress("UNCHECKED_CAST") - override fun write( - key: UHeapRef, - sort: Sort, + override fun write( heap: USymbolicHeap, - value: UExpr, + key: UHeapRef, + value: UExpr, guard: UBoolExpr, ) { assert(guard.isTrue) @@ -175,8 +247,16 @@ data class UInputArrayLengthId internal constructor( } override fun keyMapper( - composer: UComposer, - ): KeyMapper = { composer.compose(it) } + transformer: UExprTransformer, + ): KeyMapper = { transformer.apply(it) } + + override fun map(composer: UComposer): UInputArrayLengthId { + check(contextHeap == null) { "contextHeap is not null in composition" } + @Suppress("UNCHECKED_CAST") + return copy(contextHeap = composer.heapEvaluator.toMutableHeap() as USymbolicHeap<*, ArrayType>) + } + override fun accept(visitor: URegionIdVisitor): R = + visitor.visit(this) override fun toString(): String { return "length($arrayType)" diff --git a/usvm-core/src/main/kotlin/org/usvm/RegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/RegionTranslator.kt new file mode 100644 index 0000000000..932022c415 --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/RegionTranslator.kt @@ -0,0 +1,147 @@ +package org.usvm + +import org.ksmt.expr.KExpr +import org.ksmt.sort.KArray2Sort +import org.ksmt.sort.KArraySort +import org.ksmt.utils.cast +import java.util.IdentityHashMap + +/** + * [URegionTranslator] defines a template method that translates a region reading to a specific [KExpr] with a sort + * [Sort]. + */ +class URegionTranslator, Key, Sort : USort, Result>( + private val updateTranslator: UMemoryUpdatesVisitor, +) { + fun translateReading(region: USymbolicMemoryRegion, key: Key): KExpr { + val translated = translate(region) + return updateTranslator.visitSelect(translated, key) + } + + private val visitorCache = IdentityHashMap() + + private fun translate(region: USymbolicMemoryRegion): Result = + region.updates.accept(updateTranslator, visitorCache) +} + +/** + * A region translator for 1-dimensional symbolic regions. + * + * @param exprTranslator defines how to perform translation on inner values. + * @param initialValue defines an initial value for a translated array. + */ +internal class U1DArrayUpdateTranslate( + private val exprTranslator: UExprTranslator<*, *>, + private val initialValue: KExpr>, +) : UMemoryUpdatesVisitor, Sort, KExpr>> { + + /** + * [key] is already translated, so we don't have to call it explicitly. + */ + override fun visitSelect(result: KExpr>, key: KExpr): KExpr = + result.ctx.mkArraySelect(result, key) + + override fun visitInitialValue(): KExpr> = initialValue + + override fun visitUpdate( + previous: KExpr>, + update: UUpdateNode, Sort>, + ): KExpr> = with(previous.uctx) { + when (update) { + is UPinpointUpdateNode -> { + val key = update.key.translated + val value = update.value.translated + val guard = update.guard.translated + mkIte(guard, previous.store(key, value), previous) + // or + // previous.store(update.key, mkIte(update.guard, update.value, previous.select(update.key))) + } + + is URangedUpdateNode<*, *, *, *> -> { + when (update.guard) { + falseExpr -> previous + else -> { + @Suppress("UNCHECKED_CAST") + (update as URangedUpdateNode, Any?, UExpr, Sort>) + val key = mkFreshConst("k", previous.sort.domain) + + val from = update.region + + val keyMapper = from.regionId.keyMapper(exprTranslator) + val convertedKey = keyMapper(update.keyConverter.convert(key)) + val isInside = update.includesSymbolically(key).translated // already includes guard + val result = exprTranslator.translateRegionReading(from, convertedKey) + val ite = mkIte(isInside, result, previous.select(key)) + mkArrayLambda(key.decl, ite) + } + } + } + } + } + + private val UExpr.translated get() = exprTranslator.translate(this) +} + +/** + * A region translator for 2-dimensional symbolic regions. + * + * @param exprTranslator defines how to perform translation on inner values. + * @param initialValue defines an initial value for a translated array. + */ +internal class U2DArrayUpdateVisitor< + Key1Sort : USort, + Key2Sort : USort, + Sort : USort, + >( + private val exprTranslator: UExprTranslator<*, *>, + private val initialValue: KExpr>, +) : UMemoryUpdatesVisitor, UExpr>, Sort, KExpr>> { + + /** + * [key] is already translated, so we don't have to call it explicitly. + */ + override fun visitSelect( + result: KExpr>, + key: Pair, KExpr>, + ): KExpr = + result.ctx.mkArraySelect(result, key.first, key.second) + + override fun visitInitialValue(): KExpr> = initialValue + + override fun visitUpdate( + previous: KExpr>, + update: UUpdateNode, UExpr>, Sort>, + ): KExpr> = with(previous.uctx) { + when (update) { + is UPinpointUpdateNode -> { + val key1 = update.key.first.translated + val key2 = update.key.second.translated + val value = update.value.translated + val guard = update.guard.translated + mkIte(guard, previous.store(key1, key2, value), previous) + } + + is URangedUpdateNode<*, *, *, *> -> { + when (update.guard) { + falseExpr -> previous + else -> { + @Suppress("UNCHECKED_CAST") + (update as URangedUpdateNode, Any?, Pair, UExpr>, Sort>) + val key1 = mkFreshConst("k1", previous.sort.domain0) + val key2 = mkFreshConst("k2", previous.sort.domain1) + + val region = update.region + val keyMapper = region.regionId.keyMapper(exprTranslator) + val convertedKey = keyMapper(update.keyConverter.convert(key1 to key2)) + val isInside = update.includesSymbolically(key1 to key2).translated // already includes guard + val result = exprTranslator.translateRegionReading(region, convertedKey) + val ite = mkIte(isInside, result, previous.select(key1, key2)) + mkArrayLambda(key1.decl, key2.decl, ite) + } + } + } + } + } + + private val UExpr.translated get() = exprTranslator.translate(this) +} diff --git a/usvm-core/src/main/kotlin/org/usvm/RegistersStack.kt b/usvm-core/src/main/kotlin/org/usvm/RegistersStack.kt index f8b0ce22d4..0b3f326cde 100644 --- a/usvm-core/src/main/kotlin/org/usvm/RegistersStack.kt +++ b/usvm-core/src/main/kotlin/org/usvm/RegistersStack.kt @@ -1,7 +1,6 @@ package org.usvm import org.ksmt.expr.KExpr -import org.ksmt.solver.KModel import org.ksmt.utils.asExpr import java.util.Stack @@ -54,18 +53,8 @@ class URegistersStack( return URegistersStack(ctx, newStack) } - @Suppress("UNUSED_PARAMETER") - fun decode(model: KModel): URegistersStackModel = TODO() - override fun eval( registerIndex: Int, sort: Sort, ): UExpr = readRegister(registerIndex, sort).asExpr(sort) } - -class URegistersStackModel(private val registers: Array?>) : URegistersStackEvaluator { - override fun eval( - registerIndex: Int, - sort: Sort, - ): UExpr = registers[registerIndex]!!.asExpr(sort) -} \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/Solver.kt b/usvm-core/src/main/kotlin/org/usvm/Solver.kt new file mode 100644 index 0000000000..1ff139ea50 --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/Solver.kt @@ -0,0 +1,54 @@ +package org.usvm + +import org.ksmt.solver.KSolver +import org.ksmt.solver.KSolverStatus + +sealed interface USolverResult + +open class USolverSat( + val model: Model +) : USolverResult + +open class USolverUnsat : USolverResult + +open class USolverUnknown : USolverResult + +abstract class USolver { + abstract fun check(memory: Memory, pc: PathCondition): USolverResult +} + +open class USolverBase( + protected val ctx: UContext, + protected val solver: KSolver<*>, + protected val translator: UExprTranslator, + protected val decoder: UModelDecoder, UModelBase>, +) : USolver, UPathCondition, UModelBase>() { + + override fun check(memory: UMemoryBase, pc: UPathCondition): USolverResult> { + if (pc.isFalse) { + return USolverUnsat() + } + solver.push() + + for (constraint in pc) { + val translated = translator.translate(constraint) + solver.assert(translated) + } + + val status = solver.check() + if (status != KSolverStatus.SAT) { + solver.pop() + + return if (status == KSolverStatus.UNSAT) { + USolverUnsat() + } else { + USolverUnknown() + } + } + val model = solver.model().detach() + val uModel = decoder.decode(memory, model) + solver.pop() + + return USolverSat(uModel) + } +} diff --git a/usvm-core/src/main/kotlin/org/usvm/State.kt b/usvm-core/src/main/kotlin/org/usvm/State.kt index b235d46f22..1a11e23d0a 100644 --- a/usvm-core/src/main/kotlin/org/usvm/State.kt +++ b/usvm-core/src/main/kotlin/org/usvm/State.kt @@ -5,7 +5,7 @@ class UState( ctx: UContext, typeSystem: UTypeSystem, var callStack: UCallStack, - var pathCondition: UPathCondition = UPathConstraintsSet(ctx), + var pathCondition: UPathCondition = UPathConstraintsSet(), var memory: USymbolicMemory = UMemoryBase(ctx, typeSystem), var models: List ) {} diff --git a/usvm-core/src/main/kotlin/org/usvm/TypeStorage.kt b/usvm-core/src/main/kotlin/org/usvm/TypeStorage.kt index 9d0b59ce6f..334c69388b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/TypeStorage.kt +++ b/usvm-core/src/main/kotlin/org/usvm/TypeStorage.kt @@ -4,7 +4,6 @@ import kotlinx.collections.immutable.PersistentMap import kotlinx.collections.immutable.PersistentSet import kotlinx.collections.immutable.persistentMapOf import kotlinx.collections.immutable.persistentSetOf -import java.lang.IllegalArgumentException interface UTypeSystem { // Returns true if t <: u @@ -18,12 +17,10 @@ interface UTypeEvaluator { class UTypeModel( private val ctx: UContext, private val typeSystem: UTypeSystem, - private val map: Map -) - : UTypeEvaluator -{ + private val typeByAddr: Map, +) : UTypeEvaluator { - fun typeOf(address: UConcreteHeapAddress): Type = map.getValue(address) + fun typeOf(address: UConcreteHeapAddress): Type = typeByAddr.getValue(address) override fun evalIs(ref: UHeapRef, type: Type): UBoolExpr = when (ref) { @@ -41,19 +38,17 @@ class UTypeStorage( val typeSystem: UTypeSystem, val isContraditing: Boolean = false, val concreteTypes: PersistentMap = persistentMapOf(), - val supertypes: PersistentMap> = persistentMapOf() -) - : UTypeEvaluator -{ + val supertypes: PersistentMap> = persistentMapOf(), +) : UTypeEvaluator { fun contradiction() = - UTypeStorage(ctx, typeSystem, true, concreteTypes, supertypes) + UTypeStorage(ctx, typeSystem, true, concreteTypes, supertypes) fun allocate(ref: UConcreteHeapAddress, type: Type): UTypeStorage = UTypeStorage(ctx, typeSystem, isContraditing, concreteTypes.put(ref, type), supertypes) fun cast(ref: UHeapRef, type: Type): UTypeStorage { - when(ref) { + when (ref) { is UConcreteHeapRef -> { val concreteType = concreteTypes.getValue(ref.address) if (!typeSystem.isSupertype(type, concreteType)) @@ -61,20 +56,28 @@ class UTypeStorage( else return this } + else -> { val constraints = supertypes.getOrDefault(ref, persistentSetOf()) // TODO: check if we have simple contradiction here - return UTypeStorage(ctx, typeSystem, isContraditing, concreteTypes, supertypes.put(ref, constraints.add(type))) + return UTypeStorage( + ctx, + typeSystem, + isContraditing, + concreteTypes, + supertypes.put(ref, constraints.add(type)) + ) } } } override fun evalIs(ref: UHeapRef, type: Type): UBoolExpr { - when(ref) { + when (ref) { is UConcreteHeapRef -> { val concreteType = concreteTypes.getValue(ref.address) return if (typeSystem.isSupertype(type, concreteType)) ctx.trueExpr else ctx.falseExpr } + else -> { @Suppress("UNUSED_VARIABLE") val constraints = supertypes.getOrDefault(ref, persistentSetOf()) diff --git a/usvm-core/src/main/kotlin/org/usvm/UExprTransformer.kt b/usvm-core/src/main/kotlin/org/usvm/UExprTransformer.kt index 849e4aa4f0..8a2692c3de 100644 --- a/usvm-core/src/main/kotlin/org/usvm/UExprTransformer.kt +++ b/usvm-core/src/main/kotlin/org/usvm/UExprTransformer.kt @@ -9,7 +9,7 @@ abstract class UExprTransformer(ctx: UContext): KNonRecursiveTransf abstract fun transform(expr: UHeapReading<*, *, *>): UExpr abstract fun transform(expr: UInputFieldReading): UExpr - abstract fun transform(expr : UAllocatedArrayReading): UExpr + abstract fun transform(expr: UAllocatedArrayReading): UExpr abstract fun transform(expr: UInputArrayReading): UExpr abstract fun transform(expr: UInputArrayLengthReading): USizeExpr @@ -18,7 +18,7 @@ abstract class UExprTransformer(ctx: UContext): KNonRecursiveTransf abstract fun transform(expr: UIsExpr): UBoolExpr - abstract fun transform(expr: UNullRef): UExpr - abstract fun transform(expr: UConcreteHeapRef): UExpr + + abstract fun transform(expr: UNullRef): UExpr } \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/UpdateNodes.kt b/usvm-core/src/main/kotlin/org/usvm/UpdateNodes.kt index bffac5beeb..a38b843b79 100644 --- a/usvm-core/src/main/kotlin/org/usvm/UpdateNodes.kt +++ b/usvm-core/src/main/kotlin/org/usvm/UpdateNodes.kt @@ -9,7 +9,7 @@ import java.util.* * changes in processing of such nodes inside a core since we expect to have only two implementations: * [UPinpointUpdateNode] and [URangedUpdateNode]. */ -sealed interface UUpdateNode { +sealed interface UUpdateNode { /** * @return will the [key] get overwritten by this write operation in *any* possible concrete state, * assuming [precondition] holds, or not. @@ -19,7 +19,7 @@ sealed interface UUpdateNode { /** * @return will this write get overwritten by [update] operation in *any* possible concrete state or not. */ - fun isIncludedByUpdateConcretely(update: UUpdateNode): Boolean + fun isIncludedByUpdateConcretely(update: UUpdateNode): Boolean /** * @return Symbolic condition expressing that the address [key] got overwritten by this memory write operation. @@ -41,15 +41,15 @@ sealed interface UUpdateNode { */ fun split( key: Key, - predicate: (UExpr) -> Boolean, - matchingWrites: MutableList>>, + predicate: (UExpr) -> Boolean, + matchingWrites: MutableList>>, guardBuilder: GuardBuilder, - ): UUpdateNode? + ): UUpdateNode? /** * @return Value which has been written into the address [key] during this memory write operation. */ - fun value(key: Key): UExpr + 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. @@ -60,18 +60,21 @@ sealed interface UUpdateNode { * Returns a mapped update node using [keyMapper] and [composer]. * It is used in [UComposer] for composition. */ - fun map(keyMapper: KeyMapper, composer: UComposer): UUpdateNode + fun map( + keyMapper: KeyMapper, + composer: UComposer + ): UUpdateNode } /** * Represents a single write of [value] into a memory address [key] */ -class UPinpointUpdateNode( +class UPinpointUpdateNode( val key: Key, - internal val value: UExpr, + internal val value: UExpr, private val keyEqualityComparer: (Key, Key) -> UBoolExpr, override val guard: UBoolExpr, -) : UUpdateNode { +) : UUpdateNode { override fun includesConcretely(key: Key, precondition: UBoolExpr) = this.key == key && (guard == guard.ctx.trueExpr || guard == precondition) // in fact, we can check less strict formulae: `precondition -> guard`, but it is too complex to compute. @@ -79,17 +82,17 @@ class UPinpointUpdateNode( override fun includesSymbolically(key: Key): UBoolExpr = guard.ctx.mkAnd(keyEqualityComparer(this.key, key), guard) - override fun isIncludedByUpdateConcretely(update: UUpdateNode): Boolean = + override fun isIncludedByUpdateConcretely(update: UUpdateNode): Boolean = update.includesConcretely(key, guard) - override fun value(key: Key): UExpr = this.value + override fun value(key: Key): UExpr = this.value override fun split( key: Key, - predicate: (UExpr) -> Boolean, - matchingWrites: MutableList>>, + predicate: (UExpr) -> Boolean, + matchingWrites: MutableList>>, guardBuilder: GuardBuilder, - ): UUpdateNode? { + ): UUpdateNode? { val ctx = value.ctx val nodeIncludesKey = includesSymbolically(key) // includes guard val nodeExcludesKey = ctx.mkNot(nodeIncludesKey) @@ -110,7 +113,7 @@ class UPinpointUpdateNode( override fun map( keyMapper: KeyMapper, composer: UComposer - ): UPinpointUpdateNode { + ): UPinpointUpdateNode { val mappedKey = keyMapper(key) val mappedValue = composer.compose(value) val mappedGuard = composer.compose(guard) @@ -129,7 +132,7 @@ class UPinpointUpdateNode( override fun hashCode(): Int = key.hashCode() * 31 + guard.hashCode() // Ignores value - override fun toString(): String = "{$key <- $value | $guard}" + override fun toString(): String = "{$key <- $value}".takeIf { guard.isTrue } ?: "{$key <- $value | $guard}" } /** @@ -153,7 +156,7 @@ sealed class UMemoryKeyConverter( abstract fun convert(key: DstKey): SrcKey protected fun convertIndex(idx: USizeExpr): USizeExpr = with(srcSymbolicArrayIndex.first.ctx) { - return mkBvSubExpr(mkBvAddExpr(idx, dstFromSymbolicArrayIndex.second), srcSymbolicArrayIndex.second) + mkBvSubExpr(mkBvAddExpr(idx, dstFromSymbolicArrayIndex.second), srcSymbolicArrayIndex.second) } abstract fun clone( @@ -194,15 +197,15 @@ sealed class UMemoryKeyConverter( * with values from memory region [region] read from range * of addresses [[keyConverter].convert([fromKey]) : [keyConverter].convert([toKey])] */ -class URangedUpdateNode, ArrayType, SrcKey, DstKey, ValueSort : USort>( +class URangedUpdateNode, SrcKey, DstKey, Sort : USort>( val fromKey: DstKey, val toKey: DstKey, - val region: UMemoryRegion, + val region: USymbolicMemoryRegion, private val concreteComparer: (DstKey, DstKey) -> Boolean, private val symbolicComparer: (DstKey, DstKey) -> UBoolExpr, val keyConverter: UMemoryKeyConverter, override val guard: UBoolExpr -) : UUpdateNode { +) : UUpdateNode { override fun includesConcretely(key: DstKey, precondition: UBoolExpr): Boolean = concreteComparer(fromKey, key) && concreteComparer(key, toKey) && (guard == guard.ctx.trueExpr || precondition == guard) // TODO: some optimizations here? @@ -216,15 +219,15 @@ class URangedUpdateNode, ArrayType, SrcKe return ctx.mkAnd(leftIsLefter, rightIsRighter, guard) } - override fun isIncludedByUpdateConcretely(update: UUpdateNode): Boolean = + override fun isIncludedByUpdateConcretely(update: UUpdateNode): Boolean = update.includesConcretely(fromKey, guard) && update.includesConcretely(toKey, guard) - override fun value(key: DstKey): UExpr = region.read(keyConverter.convert(key)) + override fun value(key: DstKey): UExpr = region.read(keyConverter.convert(key)) override fun map( - keyMapper: (DstKey) -> DstKey, + keyMapper: KeyMapper, composer: UComposer - ): URangedUpdateNode { + ): URangedUpdateNode { val mappedFromKey = keyMapper(fromKey) val mappedToKey = keyMapper(toKey) val mappedRegion = region.map(composer) @@ -255,10 +258,10 @@ class URangedUpdateNode, ArrayType, SrcKe override fun split( key: DstKey, - predicate: (UExpr) -> Boolean, - matchingWrites: MutableList>>, + predicate: (UExpr) -> Boolean, + matchingWrites: MutableList>>, guardBuilder: GuardBuilder, - ): UUpdateNode { + ): UUpdateNode { val ctx = guardBuilder.nonMatchingUpdatesGuard.ctx val nodeIncludesKey = includesSymbolically(key) // contains guard val nodeExcludesKey = ctx.mkNot(nodeIncludesKey) @@ -304,7 +307,7 @@ class URangedUpdateNode, ArrayType, SrcKe // Ignores update override fun equals(other: Any?): Boolean = - other is URangedUpdateNode<*, *, *, *, *> && + other is URangedUpdateNode<*, *, *, *> && this.fromKey == other.fromKey && this.toKey == other.toKey && this.guard == other.guard @@ -313,7 +316,8 @@ class URangedUpdateNode, ArrayType, SrcKe override fun hashCode(): Int = (17 * fromKey.hashCode() + toKey.hashCode()) * 31 + guard.hashCode() override fun toString(): String { - return "{[$fromKey..$toKey] <- $region[keyConv($fromKey)..keyConv($toKey)] | $guard}" + return "{[$fromKey..$toKey] <- $region[keyConv($fromKey)..keyConv($toKey)]" + + ("}".takeIf { guard.isTrue } ?: " | $guard}") } } @@ -352,7 +356,7 @@ class UAllocatedToInputKeyConverter( } /** - * Used when copying data from allocated input to allocated one. + * Used when copying data from input array to allocated one. */ class UInputToAllocatedKeyConverter( srcSymbolicArrayIndex: USymbolicArrayIndex, @@ -372,11 +376,11 @@ class UInputToAllocatedKeyConverter( * Used when copying data from input array to another input array. */ class UInputToInputKeyConverter( - srcSymbolicArrayIndex: USymbolicArrayIndex, + srcFromSymbolicArrayIndex: USymbolicArrayIndex, dstFromSymbolicArrayIndex: USymbolicArrayIndex, dstToIndex: USizeExpr ) : UMemoryKeyConverter( - srcSymbolicArrayIndex, + srcFromSymbolicArrayIndex, 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 b3b1d813e5..987ce7d98b 100644 --- a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt @@ -12,22 +12,28 @@ import org.ksmt.expr.KExpr import org.ksmt.expr.printer.ExpressionPrinter import org.ksmt.expr.transformer.KTransformerBase import org.ksmt.sort.KBv32Sort +import org.ksmt.utils.sampleValue +import org.usvm.UAddressCounter.Companion.NULL_ADDRESS import kotlin.reflect.KClass import kotlin.test.assertEquals +import kotlin.test.assertIs import kotlin.test.assertSame +import kotlin.test.assertTrue -internal class CompositionTest { +internal class CompositionTest { private lateinit var stackEvaluator: URegistersStackEvaluator private lateinit var heapEvaluator: UReadOnlySymbolicHeap private lateinit var typeEvaluator: UTypeEvaluator private lateinit var mockEvaluator: UMockEvaluator private lateinit var ctx: UContext + private lateinit var concreteNull: UConcreteHeapRef private lateinit var composer: UComposer @BeforeEach fun initializeContext() { ctx = UContext() + concreteNull = ctx.mkConcreteHeapRef(NULL_ADDRESS) stackEvaluator = mockk() heapEvaluator = mockk() typeEvaluator = mockk() @@ -192,20 +198,17 @@ internal class CompositionTest { val fstResultValue = 1.toBv() val sndResultValue = 2.toBv() - val updates = UEmptyUpdates( + val updates = UFlatUpdates( 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 regionId = UInputArrayLengthId(arrayType, bv32Sort, contextHeap = null) val regionArray = UInputArrayLengthRegion( regionId, - bv32Sort, updates, - defaultValue = sizeSort.defaultValue(), - instantiator = { key, region -> mkInputArrayLengthReading(region, key) } ) val fstConcreteAddress = mkConcreteHeapRef(firstAddress) @@ -243,32 +246,21 @@ internal class CompositionTest { val sndIndex = mockk() val keyEqualityComparer = { k1: USymbolicArrayIndex, k2: USymbolicArrayIndex -> - mkAnd(k1.first eq k2.first, k1.second eq k2.second) + mkAnd((k1.first == k2.first).expr, (k1.second == k2.second).expr) } - val initialNode = UPinpointUpdateNode( - fstAddress to fstIndex, - 42.toBv(), - keyEqualityComparer, - trueExpr, - ) - - val updates: UMemoryUpdates = UFlatUpdates( - initialNode, - next = null, + val updates = UFlatUpdates( symbolicCmp = { _, _ -> shouldNotBeCalled() }, concreteCmp = { k1, k2 -> k1 == k2 }, symbolicEq = { k1, k2 -> keyEqualityComparer(k1, k2) } - ).write(sndAddress to sndIndex, 43.toBv(), guard = trueExpr) + ).write(fstAddress to fstIndex, 42.toBv(), guard = trueExpr) + .write(sndAddress to sndIndex, 43.toBv(), guard = trueExpr) val arrayType: KClass> = Array::class val region = UInputArrayRegion( - UInputArrayId(arrayType), - mkBv32Sort(), + UInputArrayId(arrayType, bv32Sort, contextHeap = null), updates, - defaultValue = null, - instantiator = { key, memoryRegion -> mkInputArrayReading(memoryRegion, key.first, key.second) } ) // TODO replace with jacoDB type @@ -307,9 +299,7 @@ internal class CompositionTest { val arrayType: KClass> = Array::class // Create an empty region - val region = emptyInputArrayRegion(arrayType, mkBv32Sort()) { key, memoryRegion -> - mkInputArrayReading(memoryRegion, key.first, key.second) - } + val region = emptyInputArrayRegion(arrayType, mkBv32Sort()) // TODO replace with jacoDB type // create a reading from the region @@ -365,20 +355,17 @@ internal class CompositionTest { val fstSymbolicIndex = mockk() val sndSymbolicIndex = mockk() - val updates = UEmptyUpdates( + val updates = UFlatUpdates( 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 regionId = UAllocatedArrayId(arrayType, bv32Sort, bv32Sort.sampleValue(), address, contextHeap = null) val regionArray = UAllocatedArrayRegion( regionId, - bv32Sort, updates, - defaultValue = 0.toBv(), - instantiator = { key, region -> mkAllocatedArrayReading(region, key) } ) val firstReading = mkAllocatedArrayReading(regionArray, fstSymbolicIndex) @@ -387,7 +374,7 @@ internal class CompositionTest { val fstAddressForCompose = mkConcreteHeapRef(address) val sndAddressForCompose = mkConcreteHeapRef(address) - val concreteIndex = sizeSort.defaultValue() + val concreteIndex = sizeSort.sampleValue() val fstValue = 42.toBv() val sndValue = 43.toBv() @@ -420,8 +407,8 @@ internal class CompositionTest { val aAddress = mockk() val bAddress = mockk() - val updates = UEmptyUpdates( - symbolicEq = { k1, k2 -> k1 eq k2 }, + val updates = UFlatUpdates( + symbolicEq = { k1, k2 -> (k1 == k2).expr }, concreteCmp = { _, _ -> throw UnsupportedOperationException() }, symbolicCmp = { _, _ -> throw UnsupportedOperationException() } ) @@ -429,11 +416,8 @@ internal class CompositionTest { // An empty region with one write in it val region = UInputFieldRegion( - UInputFieldRegionId(field), - bv32Sort, + UInputFieldId(field, bv32Sort, contextHeap = null), updates, - defaultValue = null, - instantiator = { key, region -> mkInputFieldReading(region, key) } ).write(aAddress, 43.toBv(), guard = trueExpr) every { aAddress.accept(any()) } returns aAddress @@ -463,4 +447,111 @@ internal class CompositionTest { assert(composedExpression === answer) } + + @Test + fun testHeapRefEq() = with(ctx) { + val concreteNull = ctx.mkConcreteHeapRef(NULL_ADDRESS) + val stackModel = + URegistersStackEagerModel(concreteNull, mapOf(0 to mkConcreteHeapRef(-1), 1 to mkConcreteHeapRef(-2))) + + val composer = UComposer(this, stackModel, mockk(), mockk(), mockk()) + + val heapRefEvalEq = mkHeapRefEq(mkRegisterReading(0, addressSort), mkRegisterReading(1, addressSort)) + + val expr = composer.compose(heapRefEvalEq) + assertSame(falseExpr, expr) + } + + @Test + fun testHeapRefNullAddress() = with(ctx) { + val concreteNull = ctx.mkConcreteHeapRef(NULL_ADDRESS) + val stackModel = URegistersStackEagerModel(concreteNull, mapOf(0 to mkConcreteHeapRef(0))) + + val heapEvaluator: UReadOnlySymbolicHeap = mockk() + every { heapEvaluator.nullRef() } returns mkConcreteHeapRef(NULL_ADDRESS) + + val composer = UComposer(this, stackModel, heapEvaluator, mockk(), mockk()) + + val heapRefEvalEq = mkHeapRefEq(mkRegisterReading(0, addressSort), nullRef) + + val expr = composer.compose(heapRefEvalEq) + assertSame(trueExpr, expr) + } + + @Test + fun testComposeComplexRangedUpdate() = with(ctx) { + val arrayType = mockk() + + val regionHeap = URegionHeap(ctx) + + val symbolicRef0 = mkRegisterReading(0, addressSort) + val symbolicRef1 = mkRegisterReading(1, addressSort) + val symbolicRef2 = mkRegisterReading(2, addressSort) + val composedSymbolicHeapRef = ctx.mkConcreteHeapRef(1) + + regionHeap.writeArrayIndex(composedSymbolicHeapRef, mkBv(3), arrayType, bv32Sort, mkBv(1337), trueExpr) + + val stackModel = URegistersStackEagerModel( + concreteNull, mapOf( + 0 to composedSymbolicHeapRef, + 1 to composedSymbolicHeapRef, + 2 to composedSymbolicHeapRef, + 3 to ctx.mkRegisterReading(3, bv32Sort), + ) + ) + val composer = UComposer(this, stackModel, regionHeap, mockk(), mockk()) + + val fromRegion0 = emptyInputArrayRegion(arrayType, bv32Sort) + .write(symbolicRef0 to mkBv(0), mkBv(42), trueExpr) + + val keyConverter1 = UInputToInputKeyConverter(symbolicRef0 to mkBv(0), symbolicRef1 to mkBv(0), mkBv(5)) + + val fromRegion1 = fromRegion0 + .copyRange(fromRegion0, symbolicRef0 to mkBv(0), symbolicRef0 to mkBv(5), keyConverter1, trueExpr) + + val keyConverter2 = UInputToInputKeyConverter(symbolicRef1 to mkBv(0), symbolicRef2 to mkBv(0), mkBv(5)) + + val fromRegion2 = fromRegion1 + .copyRange(fromRegion1, symbolicRef1 to mkBv(0), symbolicRef1 to mkBv(5), keyConverter2, trueExpr) + + val idx0 = mkRegisterReading(3, bv32Sort) + + val reading0 = fromRegion2.read(symbolicRef2 to idx0) + + val composedExpr0 = composer.compose(reading0) + val composedReading0 = assertIs>(composedExpr0) + + fun UMemoryUpdates<*, *>.allUpdates(): Collection> = + fold(mutableListOf()) { acc, r -> + acc += r + acc += (r as? URangedUpdateNode<*, *, *, *>)?.region?.updates?.allUpdates() ?: emptyList() + acc + } + + val pinpointUpdates = composedReading0 + .region + .updates + .allUpdates() + .filterIsInstance>() + + assertTrue { pinpointUpdates.any { it.key == mkBv(3) && it.value == mkBv(1337) } } + assertTrue { pinpointUpdates.any { it.key == mkBv(0) && it.value == mkBv(42) } } + } + + @Test + fun testNullRefRegionDefaultValue() = with(ctx) { + val heapEvaluator: UReadOnlySymbolicHeap = mockk() + + every { heapEvaluator.nullRef() } returns concreteNull + + val stackModel = URegistersStackEagerModel(concreteNull, mapOf(0 to mkBv(0), 1 to mkBv(0), 2 to mkBv(2))) + + val composer = UComposer(this, stackModel, heapEvaluator, mockk(), mockk()) + + val region = emptyAllocatedArrayRegion(mockk(), 1, addressSort) + val reading = region.read(mkRegisterReading(0, sizeSort)) + + val expr = composer.compose(reading) + assertSame(concreteNull, expr) + } } diff --git a/usvm-core/src/test/kotlin/org/usvm/HeapRefEqTest.kt b/usvm-core/src/test/kotlin/org/usvm/HeapRefEqTest.kt index f1b1d08e72..abc929933a 100644 --- a/usvm-core/src/test/kotlin/org/usvm/HeapRefEqTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/HeapRefEqTest.kt @@ -7,7 +7,7 @@ import kotlin.test.assertSame class HeapRefEqTest { private lateinit var ctx: UContext - private lateinit var heap: URegionHeap + private lateinit var heap: URegionHeap @BeforeEach fun initializeContext() { @@ -33,7 +33,7 @@ class HeapRefEqTest { @Test fun testSymbolicAndConcreteHeapRefEq() = with(ctx) { - val ref1 = mkConcreteHeapRef(heap.allocate()) + val ref1 = heap.allocate() val ref2 = mkRegisterReading(0, addressSort) val expr = mkHeapRefEq(ref1, ref2) assertSame(falseExpr, expr) @@ -49,15 +49,15 @@ class HeapRefEqTest { @Test fun testConcreteHeapRefEqFalse() = with(ctx) { - val ref1 = mkConcreteHeapRef(heap.allocate()) - val ref2 = mkConcreteHeapRef(heap.allocate()) + val ref1 = heap.allocate() + val ref2 = heap.allocate() val expr = mkHeapRefEq(ref1, ref2) assertSame(falseExpr, expr) } @Test fun testConcreteHeapRefEqTrue() = with(ctx) { - val ref1 = mkConcreteHeapRef(heap.allocate()) + val ref1 = heap.allocate() val ref2 = ref1 val expr = mkHeapRefEq(ref1, ref2) assertSame(trueExpr, expr) @@ -65,7 +65,7 @@ class HeapRefEqTest { @Test fun testInterleavedWithNullHeapRefEq() = with(ctx) { - val ref1 = mkConcreteHeapRef(heap.allocate()) + val ref1 = heap.allocate() val ref2 = mkNullRef() val expr = mkHeapRefEq(ref1, ref2) assertSame(falseExpr, expr) @@ -73,7 +73,7 @@ class HeapRefEqTest { @Test fun testInterleavedHeapRefEq() = with(ctx) { - val ref1 = mkConcreteHeapRef(heap.allocate()) + val ref1 = heap.allocate() val ref2 = mkRegisterReading(0, addressSort) val expr = mkHeapRefEq(ref1, ref2) assertSame(falseExpr, expr) @@ -81,11 +81,11 @@ class HeapRefEqTest { @Test fun testSimpleIteConcreteHeapRefEq() = with(ctx) { - val ref1 = mkConcreteHeapRef(heap.allocate()) + val ref1 = heap.allocate() val ref2 = ref1 val cond1 by boolSort - val ref3 = mkConcreteHeapRef(heap.allocate()) + val ref3 = heap.allocate() val ref4 = ref3 val cond2 by boolSort @@ -110,7 +110,7 @@ class HeapRefEqTest { @Test fun testSimpleIteHeapRefEq() = with(ctx) { - val ref1 = mkConcreteHeapRef(heap.allocate()) + val ref1 = heap.allocate() val ref2 = mkRegisterReading(0, addressSort) val cond1 by boolSort @@ -129,8 +129,8 @@ class HeapRefEqTest { val symbolicRef2 = mkRegisterReading(1, addressSort) val symbolicRef3 = mkRegisterReading(2, addressSort) - val concreteRef1 = mkConcreteHeapRef(heap.allocate()) - val concreteRef2 = mkConcreteHeapRef(heap.allocate()) + val concreteRef1 = heap.allocate() + val concreteRef2 = heap.allocate() val cond1 by boolSort val cond2 by boolSort diff --git a/usvm-core/src/test/kotlin/org/usvm/HeapRefSplittingTest.kt b/usvm-core/src/test/kotlin/org/usvm/HeapRefSplittingTest.kt index 07fd038f94..e8a73eb296 100644 --- a/usvm-core/src/test/kotlin/org/usvm/HeapRefSplittingTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/HeapRefSplittingTest.kt @@ -12,11 +12,11 @@ import kotlin.test.assertSame class HeapRefSplittingTest { private lateinit var ctx: UContext - private lateinit var heap: URegionHeap + private lateinit var heap: URegionHeap private lateinit var valueFieldDescr: Pair private lateinit var addressFieldDescr: Pair - private lateinit var arrayDescr: Pair + private lateinit var arrayDescr: Pair @BeforeEach fun initializeContext() { @@ -24,13 +24,13 @@ class HeapRefSplittingTest { heap = URegionHeap(ctx) valueFieldDescr = mockk() to ctx.bv32Sort addressFieldDescr = mockk() to ctx.addressSort - arrayDescr = mockk() to ctx.addressSort + arrayDescr = mockk() to ctx.addressSort } @Test fun testConcreteWriting() = with(ctx) { - val ref1 = mkConcreteHeapRef(heap.allocate()) - val ref2 = mkConcreteHeapRef(heap.allocate()) + val ref1 = heap.allocate() + val ref2 = heap.allocate() val value1 = mkBv(0) val value2 = mkBv(1) @@ -47,7 +47,7 @@ class HeapRefSplittingTest { @Test fun testIteWriting() = with(ctx) { - val ref1 = mkConcreteHeapRef(heap.allocate()) + val ref1 = heap.allocate() val ref2 = mkRegisterReading(0, addressSort) val cond by boolSort @@ -69,9 +69,9 @@ class HeapRefSplittingTest { @Test fun testInterleavedWritingToArray(): Unit = with(ctx) { - val arrayRef = mkConcreteHeapRef(heap.allocate()) + val arrayRef = heap.allocate() - val ref1 = mkConcreteHeapRef(heap.allocate()) + val ref1 = heap.allocate() val ref2 = mkRegisterReading(0, addressSort) val idx1 by sizeSort @@ -95,15 +95,15 @@ class HeapRefSplittingTest { @Test fun testSeveralWritingsToArray() = with(ctx) { - val ref = mkConcreteHeapRef(heap.allocate()) + val ref = heap.allocate() val idx1 = mkRegisterReading(0, sizeSort) val idx2 = mkRegisterReading(1, sizeSort) val idx3 = mkRegisterReading(2, sizeSort) - val val1 = mkConcreteHeapRef(heap.allocate()) - val val2 = mkConcreteHeapRef(heap.allocate()) - val val3 = mkConcreteHeapRef(heap.allocate()) + val val1 = heap.allocate() + val val2 = heap.allocate() + val val3 = heap.allocate() heap.writeArrayIndex(ref, idx1, arrayDescr.first, arrayDescr.second, val1, trueExpr) heap.writeArrayIndex(ref, idx2, arrayDescr.first, arrayDescr.second, val2, trueExpr) @@ -121,16 +121,16 @@ class HeapRefSplittingTest { @Test fun testWritingIteToArrayByIteIndex() = with(ctx) { - val ref1 = mkConcreteHeapRef(heap.allocate()) - val ref2 = mkConcreteHeapRef(heap.allocate()) + val ref1 = heap.allocate() + val ref2 = heap.allocate() val cond1 by boolSort val ref = mkIte(cond1, ref1, ref2) val idx = mkRegisterReading(0, sizeSort) - val val1 = mkConcreteHeapRef(heap.allocate()) - val val2 = mkConcreteHeapRef(heap.allocate()) + val val1 = heap.allocate() + val val2 = heap.allocate() val cond2 by boolSort val value = mkIte(cond2, val1, val2) @@ -155,9 +155,9 @@ class HeapRefSplittingTest { val ref2 = mkRegisterReading(1, addressSort) val ref3 = mkRegisterReading(2, addressSort) - val val1 = mkConcreteHeapRef(heap.allocate()) + val val1 = heap.allocate() val val2 = mkRegisterReading(3, addressSort) - val val3 = mkConcreteHeapRef(heap.allocate()) + val val3 = heap.allocate() heap.writeField(ref1, addressFieldDescr.first, addressFieldDescr.second, val1, trueExpr) heap.writeField(ref2, addressFieldDescr.first, addressFieldDescr.second, val2, trueExpr) @@ -175,7 +175,7 @@ class HeapRefSplittingTest { @Test fun testInterleavedWritingToArrayButNoMatchedUpdates() = with(ctx) { - val arrayRef = mkConcreteHeapRef(heap.allocate()) + val arrayRef = heap.allocate() val ref1 = mkRegisterReading(0, addressSort) val ref2 = mkRegisterReading(1, addressSort) @@ -198,7 +198,7 @@ class HeapRefSplittingTest { val res2 = heap.readField(ref2, valueFieldDescr.first, valueFieldDescr.second) assertIs>(res2) - assertSame(res1.region, res2.region) + assertEquals(res1.region, res2.region) } @Test @@ -221,7 +221,7 @@ class HeapRefSplittingTest { val res2 = heap.readField(ref2, addressFieldDescr.first, addressFieldDescr.second) assertIs>(res2) - assertSame(res1.region, res2.region) + assertEquals(res1.region, res2.region) val res3 = heap.readField(ref3, addressFieldDescr.first, addressFieldDescr.second) assertSame(val3, res3) @@ -230,7 +230,7 @@ class HeapRefSplittingTest { @Test fun testInterleavedValueWriting() = with(ctx) { val ref1 = mkRegisterReading(0, addressSort) - val ref2 = mkConcreteHeapRef(heap.allocate()) + val ref2 = heap.allocate() val cond by boolSort diff --git a/usvm-core/src/test/kotlin/org/usvm/MapCompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/MapCompositionTest.kt index 79df0060ab..22caf7bf24 100644 --- a/usvm-core/src/test/kotlin/org/usvm/MapCompositionTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/MapCompositionTest.kt @@ -8,7 +8,11 @@ import org.ksmt.expr.KExpr import org.ksmt.utils.mkConst import org.usvm.util.SetRegion import org.usvm.util.emptyRegionTree -import kotlin.test.* +import kotlin.test.assertFalse +import kotlin.test.assertNotNull +import kotlin.test.assertNotSame +import kotlin.test.assertNull +import kotlin.test.assertSame class MapCompositionTest { private lateinit var ctx: UContext @@ -152,7 +156,7 @@ class MapCompositionTest { 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 region = mockk, UExpr, UBv32Sort>>() val guard = boolSort.mkConst("guard") val updateNode = URangedUpdateNode( @@ -172,7 +176,7 @@ class MapCompositionTest { 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 { region.map(composer) } returns region every { composer.compose(guard) } returns guard val mappedUpdateNode = updateNode.map({ k -> composer.compose((k)) }, composer) @@ -185,7 +189,7 @@ class MapCompositionTest { val addr = mkConcreteHeapRef(0) val fromKey = sizeSort.mkConst("fromKey") val toKey = sizeSort.mkConst("toKey") - val region = mockk, USizeExpr, UBv32Sort>>() + val region = mockk, USizeExpr, UBv32Sort>>() val guard = boolSort.mkConst("guard") val updateNode = URangedUpdateNode( @@ -204,13 +208,13 @@ class MapCompositionTest { val composedFromKey = sizeSort.mkConst("composedFromKey") val composedToKey = sizeSort.mkConst("composedToKey") - val composedRegion = mockk, UExpr, UBv32Sort>>() + 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 { region.map(composer) } returns composedRegion every { composer.compose(guard) } returns composedGuard val mappedUpdateNode = updateNode.map({ k -> composer.compose((k)) }, composer) @@ -224,7 +228,7 @@ class MapCompositionTest { @Test fun testEmptyUpdatesMapOperation() { - val emptyUpdates = UEmptyUpdates, UBv32Sort>( + val emptyUpdates = UFlatUpdates, UBv32Sort>( { _, _ -> shouldNotBeCalled() }, { _, _ -> shouldNotBeCalled() }, { _, _ -> shouldNotBeCalled() } @@ -242,7 +246,7 @@ class MapCompositionTest { val sndKey = addressSort.mkConst("sndKey") val sndValue = bv32Sort.mkConst("sndValue") - val flatUpdates = UEmptyUpdates, UBv32Sort>( + val flatUpdates = UFlatUpdates, UBv32Sort>( { _, _ -> shouldNotBeCalled() }, { _, _ -> shouldNotBeCalled() }, { _, _ -> shouldNotBeCalled() } @@ -267,7 +271,7 @@ class MapCompositionTest { val sndKey = addressSort.mkConst("sndKey") val sndValue = bv32Sort.mkConst("sndValue") - val flatUpdates = UEmptyUpdates, UBv32Sort>( + val flatUpdates = UFlatUpdates, UBv32Sort>( { _, _ -> shouldNotBeCalled() }, { _, _ -> shouldNotBeCalled() }, { _, _ -> shouldNotBeCalled() } @@ -289,15 +293,15 @@ class MapCompositionTest { assertNotSame(illegal = flatUpdates, actual = mappedUpdates) - val node = mappedUpdates.node as UPinpointUpdateNode<*, *> - val next = mappedUpdates.next as UFlatUpdates<*, *> - val nextNode = next.node as UPinpointUpdateNode<*, *> + val node = mappedUpdates.node?.update as UPinpointUpdateNode<*, *> + val next = mappedUpdates.node.next as UFlatUpdates<*, *> + val nextNode = next.node?.update 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) + assertNull(next.node.next.node) } @Test @@ -373,7 +377,3 @@ class MapCompositionTest { 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/ModelCompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/ModelCompositionTest.kt new file mode 100644 index 0000000000..f043947387 --- /dev/null +++ b/usvm-core/src/test/kotlin/org/usvm/ModelCompositionTest.kt @@ -0,0 +1,162 @@ +package org.usvm + +import io.mockk.mockk +import kotlinx.collections.immutable.persistentMapOf +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Test +import kotlin.test.assertSame + +class ModelCompositionTest { + private lateinit var ctx: UContext + private lateinit var concreteNull: UConcreteHeapRef + + @BeforeEach + fun initializeContext() { + ctx = UContext() + concreteNull = ctx.mkConcreteHeapRef(UAddressCounter.NULL_ADDRESS) + } + + @Test + fun testComposeAllocatedArray() = with(ctx) { + val heapEvaluator = UHeapEagerModel( + concreteNull, + mapOf(), + mapOf(), + mapOf(), + ) + + val stackModel = URegistersStackEagerModel(concreteNull, mapOf(0 to ctx.mkBv(0), 1 to ctx.mkBv(0), 2 to ctx.mkBv(2))) + + val composer = UComposer(this, stackModel, heapEvaluator, mockk(), mockk()) + + val region = emptyAllocatedArrayRegion(mockk(), 1, bv32Sort) + .write(0.toBv(), 0.toBv(), trueExpr) + .write(1.toBv(), 1.toBv(), trueExpr) + .write(mkRegisterReading(1, sizeSort), 2.toBv(), trueExpr) + .write(mkRegisterReading(2, sizeSort), 3.toBv(), trueExpr) + val reading = region.read(mkRegisterReading(0, sizeSort)) + + val expr = composer.compose(reading) + assertSame(mkBv(2), expr) + } + + @Test + fun testComposeRangedUpdate() = with(ctx) { + val arrayType = mockk() + val composedSymbolicHeapRef = ctx.mkConcreteHeapRef(-1) + val inputArray = UMemory2DArray(persistentMapOf((composedSymbolicHeapRef to mkBv(0)) to mkBv(1)), mkBv(0)) + val heapEvaluator = UHeapEagerModel( + concreteNull, + mapOf(), + mapOf(arrayType to inputArray), + mapOf(), + ) + + val stackModel = + URegistersStackEagerModel(concreteNull, mapOf(0 to composedSymbolicHeapRef, 1 to mkBv(0))) + val composer = UComposer(this, stackModel, heapEvaluator, mockk(), mockk()) + + val symbolicRef = mkRegisterReading(0, addressSort) + + val fromRegion = emptyInputArrayRegion(arrayType, bv32Sort) + + val concreteRef = mkConcreteHeapRef(1) + + val keyConverter = UInputToAllocatedKeyConverter(symbolicRef to mkBv(0), concreteRef to mkBv(0), mkBv(5)) + val concreteRegion = emptyAllocatedArrayRegion(arrayType, concreteRef.address, bv32Sort) + .copyRange(fromRegion, mkBv(0), mkBv(5), keyConverter, trueExpr) + + val idx = mkRegisterReading(1, sizeSort) + + val reading = concreteRegion.read(idx) + + val expr = composer.compose(reading) + assertSame(mkBv(1), expr) + } + + @Test + fun testComposeInputArrayLength() = with(ctx) { + val symbolicRef0 = mkRegisterReading(0, addressSort) + val symbolicRef1 = mkRegisterReading(1, addressSort) + val symbolicRef2 = mkRegisterReading(2, addressSort) + val symbolicRef3 = mkRegisterReading(3, addressSort) + + val composedRef0 = mkConcreteHeapRef(-1) + val composedRef1 = mkConcreteHeapRef(-2) + val composedRef2 = mkConcreteHeapRef(-3) + val composedRef3 = mkConcreteHeapRef(-4) + + val arrayType = mockk() + val inputLength = UMemory1DArray(persistentMapOf(composedRef0 to mkBv(42)), mkBv(0)) + val heapEvaluator = UHeapEagerModel( + concreteNull, + mapOf(), + mapOf(), + mapOf(arrayType to inputLength), + ) + + val stackModel = URegistersStackEagerModel( + concreteNull, + mapOf( + 0 to composedRef0, + 1 to composedRef1, + 2 to composedRef2, + 3 to composedRef3 + ) + ) + + val composer = UComposer(this, stackModel, heapEvaluator, mockk(), mockk()) + + val region = emptyInputArrayLengthRegion(arrayType, bv32Sort) + .write(symbolicRef1, 0.toBv(), trueExpr) + .write(symbolicRef2, 1.toBv(), trueExpr) + .write(symbolicRef3, 2.toBv(), trueExpr) + val reading = region.read(symbolicRef0) + + val expr = composer.compose(reading) + assertSame(mkBv(42), expr) + } + + @Test + fun testComposeInputField() = with(ctx) { + val symbolicRef0 = mkRegisterReading(0, addressSort) + val symbolicRef1 = mkRegisterReading(1, addressSort) + val symbolicRef2 = mkRegisterReading(2, addressSort) + val symbolicRef3 = mkRegisterReading(3, addressSort) + + val composedRef0 = mkConcreteHeapRef(-1) + val composedRef1 = mkConcreteHeapRef(-2) + val composedRef2 = mkConcreteHeapRef(-3) + val composedRef3 = mkConcreteHeapRef(-4) + + val field = mockk() + val inputField = UMemory1DArray(persistentMapOf(composedRef0 to composedRef0), concreteNull) + val heapEvaluator = UHeapEagerModel( + concreteNull, + mapOf(field to inputField), + mapOf(), + mapOf(), + ) + + val stackModel = URegistersStackEagerModel( + concreteNull, + mapOf( + 0 to composedRef0, + 1 to composedRef1, + 2 to composedRef2, + 3 to composedRef3 + ) + ) + + val composer = UComposer(this, stackModel, heapEvaluator, mockk(), mockk()) + + val region = emptyInputFieldRegion(field, addressSort) + .write(symbolicRef1, symbolicRef1, trueExpr) + .write(symbolicRef2, symbolicRef2, trueExpr) + .write(symbolicRef3, symbolicRef3, trueExpr) + val reading = region.read(symbolicRef0) + + val expr = composer.compose(reading) + assertSame(composedRef0, expr) + } +} \ No newline at end of file diff --git a/usvm-core/src/test/kotlin/org/usvm/ModelDecodingTest.kt b/usvm-core/src/test/kotlin/org/usvm/ModelDecodingTest.kt new file mode 100644 index 0000000000..231a879ef9 --- /dev/null +++ b/usvm-core/src/test/kotlin/org/usvm/ModelDecodingTest.kt @@ -0,0 +1,172 @@ +package org.usvm + +import io.mockk.mockk +import org.junit.jupiter.api.Assertions.assertSame +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Test +import org.ksmt.solver.z3.KZ3Solver +import kotlin.test.assertFalse +import kotlin.test.assertIs + +class ModelDecodingTest { + private lateinit var ctx: UContext + private lateinit var solver: USolverBase + + private lateinit var memory: UMemoryBase + private lateinit var stack: URegistersStack + private lateinit var heap: URegionHeap + private lateinit var mocker: UIndexedMocker + + @BeforeEach + fun initializeContext() { + ctx = UContext() + val (translator, decoder) = buildTranslatorAndLazyDecoder(ctx) + solver = USolverBase(ctx, KZ3Solver(ctx), translator, decoder) + + stack = URegistersStack(ctx) + stack.push(10) + heap = URegionHeap(ctx) + mocker = UIndexedMocker(ctx) + + memory = UMemoryBase(ctx, mockk(), stack, heap, mockk(), mocker) + } + + @Test + fun testSmoke(): Unit = with(ctx) { + val status = solver.check(memory, UPathConstraintsSet(trueExpr)) + assertIs>>(status) + } + + @Test + fun testSimpleWritingToFields() = with(ctx) { + val field = mockk() + + val concreteRef = heap.allocate() + val symbolicRef0 = stack.readRegister(0, addressSort) + val symbolicRef1 = stack.readRegister(1, addressSort) + + heap.writeField(concreteRef, field, bv32Sort, mkBv(1), trueExpr) + heap.writeField(symbolicRef0, field, bv32Sort, mkBv(2), trueExpr) + + val pc = heap.readField(symbolicRef1, field, bv32Sort) eq mkBv(42) + + val status = solver.check(memory, UPathConstraintsSet(pc)) + val model = assertIs>>(status).model + + val expr = heap.readField(symbolicRef1, field, bv32Sort) + + assertSame(mkBv(42), model.eval(expr)) + } + + @Test + fun testSimpleWritingToAddressFields() = with(ctx) { + val field = mockk() + + val concreteRef = heap.allocate() + val symbolicRef0 = stack.readRegister(0, addressSort) + val symbolicRef1 = stack.readRegister(1, addressSort) + + heap.writeField(concreteRef, field, addressSort, symbolicRef1, trueExpr) + heap.writeField(symbolicRef0, field, addressSort, symbolicRef0, trueExpr) + + val pc = (symbolicRef1 neq nullRef) and (symbolicRef0 neq nullRef) and + (heap.readField(symbolicRef0, field, addressSort) eq symbolicRef1) + + val status = solver.check(memory, UPathConstraintsSet(pc)) + val model = assertIs>>(status).model + + val expr = heap.readField(symbolicRef1, field, addressSort) + + assertSame(model.eval(symbolicRef0), model.eval(expr)) + } + + @Test + fun testSimpleMock() = with(ctx) { + val field = mockk() + val method = mockk() + + val mockedValue = mocker.call(method, emptySequence(), addressSort).first + val ref1 = heap.readField(mockedValue, field, addressSort) + heap.writeField(ref1, field, addressSort, heap.allocate(), trueExpr) + val ref2 = heap.readField(mockedValue, field, addressSort) + + val pc = (ref1 neq ref2) and (mockedValue neq nullRef) and (ref1 neq nullRef) + + val status = solver.check(memory, UPathConstraintsSet(pc)) + val model = assertIs>>(status).model + + val mockedValueEqualsRef1 = mockedValue eq ref1 + + assertSame(trueExpr, model.eval(mockedValueEqualsRef1)) + } + + @Test + fun testSimpleMockUnsat(): Unit = with(ctx) { + val field = mockk() + val method = mockk() + + val mockedValue = mocker.call(method, emptySequence(), addressSort).first + val ref1 = heap.readField(mockedValue, field, addressSort) + heap.writeField(ref1, field, addressSort, ref1, trueExpr) + val ref2 = heap.readField(mockedValue, field, addressSort) + + val pc = (ref1 neq ref2) and (mockedValue neq nullRef) and (ref1 neq nullRef) + + val status = solver.check(memory, UPathConstraintsSet(pc)) + assertIs>>(status) + } + + @Test + fun testSimpleSeveralWritingsToArray() = with(ctx) { + val array = mockk() + + val concreteRef = heap.allocate() + val symbolicRef0 = stack.readRegister(0, addressSort) + val symbolicRef1 = stack.readRegister(1, addressSort) + val symbolicRef2 = stack.readRegister(2, addressSort) + + val concreteIdx = mkBv(3) + val idx = stack.readRegister(3, bv32Sort) + + heap.writeArrayIndex(concreteRef, concreteIdx, array, addressSort, symbolicRef1, trueExpr) + val readedRef = heap.readArrayIndex(concreteRef, idx, array, addressSort) + + val readedRef1 = heap.readArrayIndex(symbolicRef2, idx, array, addressSort) + + heap.writeArrayIndex(readedRef, idx, array, addressSort, symbolicRef0, trueExpr) + + val readedRef2 = heap.readArrayIndex(symbolicRef2, idx, array, addressSort) + + val pc = (symbolicRef2 neq nullRef) and (readedRef1 neq readedRef2) + + val status = solver.check(memory, UPathConstraintsSet(pc)) + val model = assertIs>>(status).model + + assertSame(model.eval(symbolicRef1), model.eval(symbolicRef2)) + } + + @Test + fun testLoopedWritingsToArray() = with(ctx) { + val array = mockk() + + val symbolicRef0 = stack.readRegister(0, addressSort) + val symbolicRef1 = stack.readRegister(1, addressSort) + val symbolicRef2 = stack.readRegister(2, addressSort) + + val concreteIdx = mkBv(3) + + heap.writeArrayIndex(symbolicRef0, concreteIdx, array, addressSort, symbolicRef1, trueExpr) + heap.writeArrayIndex(symbolicRef1, concreteIdx, array, addressSort, symbolicRef2, trueExpr) + heap.writeArrayIndex(symbolicRef2, concreteIdx, array, addressSort, symbolicRef0, trueExpr) + + val readedRef = heap.readArrayIndex(symbolicRef0, concreteIdx, array, addressSort) + val pc = (symbolicRef0 neq nullRef) and (symbolicRef1 neq nullRef) and (symbolicRef2 neq nullRef) and + (readedRef neq symbolicRef1) and (symbolicRef0 eq symbolicRef1) + + val status = solver.check(memory, UPathConstraintsSet(pc)) + val model = assertIs>>(status).model + + assertSame(falseExpr, model.eval(symbolicRef2 eq symbolicRef0)) + assertSame(model.eval(readedRef), model.eval(symbolicRef2)) + } +} diff --git a/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt b/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt index 73971160ac..c703604668 100644 --- a/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt +++ b/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt @@ -1,4 +1,9 @@ package org.usvm typealias Field = java.lang.reflect.Field -typealias ArrayType = kotlin.reflect.KClass<*> +typealias Type = kotlin.reflect.KClass<*> +typealias Method = kotlin.reflect.KFunction<*> + +fun shouldNotBeCalled(): T { + error("Should not be called") +} \ No newline at end of file diff --git a/usvm-core/src/test/kotlin/org/usvm/TranslationTest.kt b/usvm-core/src/test/kotlin/org/usvm/TranslationTest.kt new file mode 100644 index 0000000000..7cd4d4d401 --- /dev/null +++ b/usvm-core/src/test/kotlin/org/usvm/TranslationTest.kt @@ -0,0 +1,251 @@ +package org.usvm + +import io.mockk.mockk +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.RepeatedTest +import org.junit.jupiter.api.Test +import org.ksmt.solver.KSolverStatus +import org.ksmt.solver.z3.KZ3Solver +import org.ksmt.utils.mkConst +import org.ksmt.utils.sampleValue +import kotlin.test.assertSame + +class TranslationTest { + private lateinit var ctx: UContext + private lateinit var heap: URegionHeap + private lateinit var translator: UExprTranslator + + private lateinit var valueFieldDescr: Pair + private lateinit var addressFieldDescr: Pair + private lateinit var valueArrayDescr: Type + private lateinit var addressArrayDescr: Type + + @BeforeEach + fun initializeContext() { + ctx = UContext() + heap = URegionHeap(ctx) + translator = UExprTranslator(ctx) + + valueFieldDescr = mockk() to ctx.bv32Sort + addressFieldDescr = mockk() to ctx.addressSort + valueArrayDescr = mockk() + addressArrayDescr = mockk() + } + + @Test + fun testTranslateConstAddressSort() = with(ctx) { + val ref = heap.allocate() + val idx = mkRegisterReading(0, sizeSort) + + val expr = heap.readArrayIndex(ref, idx, addressArrayDescr, addressSort) + val translated = translator.translate(expr) + + assertSame(translator.translate(nullRef), translated) + } + + @Test + fun testTranslateConstValueSort() = with(ctx) { + val ref = heap.allocate() + val idx = mkRegisterReading(0, sizeSort) + + val expr = heap.readArrayIndex(ref, idx, valueArrayDescr, bv32Sort) + val translated = translator.translate(expr) + + assertSame(bv32Sort.sampleValue(), translated) + } + + @Test + fun testTranslateWritingsToAllocatedArray() = with(ctx) { + val ref = heap.allocate() + val idx1 = mkRegisterReading(0, sizeSort) + val idx2 = mkRegisterReading(1, sizeSort) + + val val1 = mkBv(1) + val val2 = mkBv(2) + + heap.writeArrayIndex(ref, idx1, valueArrayDescr, bv32Sort, val1, trueExpr) + heap.writeArrayIndex(ref, idx2, valueArrayDescr, bv32Sort, val2, trueExpr) + + val readIdx = mkRegisterReading(2, sizeSort) + + val expr = heap.readArrayIndex(ref, readIdx, valueArrayDescr, bv32Sort) + + val translated = translator.translate(expr) + + val translatedIdx1 = translator.translate(idx1) + val translatedIdx2 = translator.translate(idx2) + val translatedReadIdx = translator.translate(readIdx) + + val expected = mkArrayConst(mkArraySort(sizeSort, bv32Sort), bv32Sort.sampleValue()) + .store(translatedIdx1, val1) + .store(translatedIdx2, val2) + .select(translatedReadIdx) + + assertSame(expected, translated) + } + + @Test + fun testTranslate2DArray() = with(ctx) { + val ref1 = mkRegisterReading(0, addressSort) + val idx1 = mkRegisterReading(1, sizeSort) + val val1 = mkBv(1) + + val ref2 = mkRegisterReading(2, addressSort) + val idx2 = mkRegisterReading(3, sizeSort) + val val2 = mkBv(2) + + + val region = emptyInputArrayRegion(valueArrayDescr, bv32Sort) + .write(ref1 to idx1, val1, trueExpr) + .write(ref2 to idx2, val2, trueExpr) + + val ref3 = mkRegisterReading(4, addressSort) + val idx3 = mkRegisterReading(5, sizeSort) + + val reading = region.read(ref3 to idx3) + + val translated = translator.translate(reading) + + val expected = mkArraySort(addressSort, sizeSort, bv32Sort) + .mkConst(region.regionId.toString()) + .store(translator.translate(ref1), translator.translate(idx1), val1) + .store(translator.translate(ref2), translator.translate(idx2), val2) + .select(translator.translate(ref3), translator.translate(idx3)) + + assertSame(expected, translated) + } + + @RepeatedTest(10) + fun testTranslateInputToAllocatedArrayCopy() = with(ctx) { + + val ref1 = mkRegisterReading(0, addressSort) + val idx1 = mkRegisterReading(1, sizeSort) + val val1 = mkBv(1) + + val ref2 = mkRegisterReading(2, addressSort) + val idx2 = mkRegisterReading(3, sizeSort) + val val2 = mkBv(2) + + val region = emptyInputArrayRegion(valueArrayDescr, bv32Sort) + .write(ref1 to idx1, val1, trueExpr) + .write(ref2 to idx2, val2, trueExpr) + + val concreteRef = heap.allocate() + + + val keyConverter = UInputToAllocatedKeyConverter(ref1 to mkBv(0), concreteRef to mkBv(0), mkBv(5)) + val concreteRegion = emptyAllocatedArrayRegion(valueArrayDescr, concreteRef.address, bv32Sort) + .copyRange(region, mkBv(0), mkBv(5), keyConverter, trueExpr) + + val idx = mkRegisterReading(4, sizeSort) + val reading = concreteRegion.read(idx) + + + val key = region.regionId.keyMapper(translator)(keyConverter.convert(translator.translate(idx))) + val innerReading = + translator.translateRegionReading(region, key) + val guard = + translator.translate((mkBvSignedLessOrEqualExpr(mkBv(0), idx)) and mkBvSignedLessOrEqualExpr(idx, mkBv(5))) + val expected = mkIte(guard, innerReading, bv32Sort.sampleValue()) + + val translated = translator.translate(reading) + + // due to KSMT non-deterministic with reorderings, we have to check it with solver + val solver = KZ3Solver(this) + solver.assert(expected neq translated) + val status = solver.check() + + assertSame(KSolverStatus.UNSAT, status) + } + + @Test + fun testTranslateInputFieldArray() = with(ctx) { + val ref1 = mkRegisterReading(1, addressSort) + val ref2 = mkRegisterReading(2, addressSort) + val ref3 = mkRegisterReading(3, addressSort) + + val g1 = mkRegisterReading(-1, boolSort) + val g2 = mkRegisterReading(-2, boolSort) + val g3 = mkRegisterReading(-3, boolSort) + + val region = emptyInputFieldRegion(mockk(), bv32Sort) + .write(ref1, mkBv(1), g1) + .write(ref2, mkBv(2), g2) + .write(ref3, mkBv(3), g3) + + val ref0 = mkRegisterReading(0, addressSort) + val reading = region.read(ref0) + + val ref0Eq1Or2Or3 = (ref0 eq ref1) or (ref0 eq ref2) or (ref0 eq ref3) + val readingNeq123 = (reading neq mkBv(1)) and (reading neq mkBv(2)) and (reading neq mkBv(3)) + val expr = ref0Eq1Or2Or3 and readingNeq123 + + val translated = translator.translate(expr and g1 and g2 and g3) + + val solver = KZ3Solver(this) + solver.assert(translated) + assertSame(KSolverStatus.UNSAT, solver.check()) + } + + @Test + fun testTranslateInputArrayLengthArray() = with(ctx) { + val ref1 = mkRegisterReading(1, addressSort) + val ref2 = mkRegisterReading(2, addressSort) + val ref3 = mkRegisterReading(3, addressSort) + + val region = emptyInputArrayLengthRegion(mockk(), bv32Sort) + .write(ref1, mkBv(1), trueExpr) + .write(ref2, mkBv(2), trueExpr) + .write(ref3, mkBv(3), trueExpr) + + val ref0 = mkRegisterReading(0, addressSort) + val reading = region.read(ref0) + + val ref0Eq1Or2Or3 = (ref0 eq ref1) or (ref0 eq ref2) or (ref0 eq ref3) + val readingNeq123 = (reading neq mkBv(1)) and (reading neq mkBv(2)) and (reading neq mkBv(3)) + val expr = ref0Eq1Or2Or3 and readingNeq123 + + val translated = translator.translate(expr) + + val solver = KZ3Solver(this) + solver.assert(translated) + assertSame(KSolverStatus.UNSAT, solver.check()) + } + + @Test + fun testTranslateInputToInputArrayCopy() = with(ctx) { + + val ref1 = mkRegisterReading(0, addressSort) + val idx1 = mkRegisterReading(1, sizeSort) + val val1 = mkBv(1) + + val ref2 = mkRegisterReading(2, addressSort) + val idx2 = mkRegisterReading(3, sizeSort) + val val2 = mkBv(2) + + val inputRegion1 = emptyInputArrayRegion(valueArrayDescr, bv32Sort) + .write(ref1 to idx1, val1, trueExpr) + .write(ref2 to idx2, val2, trueExpr) + + + val keyConverter = UInputToInputKeyConverter(ref1 to mkBv(0), ref1 to mkBv(0), mkBv(5)) + var inputRegion2 = emptyInputArrayRegion(mockk(), bv32Sort) + + val idx = mkRegisterReading(4, sizeSort) + val reading1 = inputRegion2.read(ref2 to idx) + + inputRegion2 = inputRegion2 + .copyRange(inputRegion1, ref1 to mkBv(0), ref1 to mkBv(5), keyConverter, trueExpr) + + val reading2 = inputRegion2.read(ref2 to idx) + + val expr = (reading1 neq reading2) and (ref1 neq ref2) + val translated = translator.translate(expr) + + val solver = KZ3Solver(this) + solver.assert(translated) + val status = solver.check() + + assertSame(KSolverStatus.UNSAT, status) + } +} \ 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 4725858c22..1e6eece8f6 100644 --- a/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt @@ -79,8 +79,8 @@ class UContextInterningTest { @Test fun testAllocatedArrayReadingInterning() = with(context) { - val fstRegion = mockk>() - val sndRegion = mockk>() + val fstRegion = mockk>() + val sndRegion = mockk>() every { fstRegion.sort } returns bv32Sort every { sndRegion.sort } returns boolSort @@ -105,8 +105,8 @@ class UContextInterningTest { @Test fun testInputArrayReadingInterning() = with(context) { - val fstRegion = mockk>() - val sndRegion = mockk>() + val fstRegion = mockk>() + val sndRegion = mockk>() every { fstRegion.sort } returns bv32Sort every { sndRegion.sort } returns boolSort @@ -136,8 +136,8 @@ class UContextInterningTest { @Test fun testArrayLengthInterning() = with(context) { - val fstRegion = mockk>() - val sndRegion = mockk>() + val fstRegion = mockk>() + val sndRegion = mockk>() every { fstRegion.sort } returns sizeSort every { sndRegion.sort } returns sizeSort diff --git a/usvm-core/src/test/kotlin/org/usvm/UpdatesIteratorTest.kt b/usvm-core/src/test/kotlin/org/usvm/UpdatesIteratorTest.kt index b51af057f2..a64bd5ae12 100644 --- a/usvm-core/src/test/kotlin/org/usvm/UpdatesIteratorTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/UpdatesIteratorTest.kt @@ -35,20 +35,12 @@ class UpdatesIteratorTest { @Test fun testFlatUpdatesIterator() = with(UContext()) { - val firstUpdateNode = UPinpointUpdateNode( - key = 10, - value = 10.toBv(), - keyEqualityComparer = { k1, k2 -> mkEq(k1.toBv(), k2.toBv()) }, - guard = trueExpr - ) - - val flatUpdates = UFlatUpdates( - node = firstUpdateNode, - next = null, + val flatUpdates = UFlatUpdates( { _, _ -> throw NotImplementedError() }, { _, _ -> throw NotImplementedError() }, { _, _ -> throw NotImplementedError() } - ).write(key = 1, value = 1.toBv(), guard = mkTrue()) + ).write(key = 10, value = 10.toBv(), guard = mkTrue()) + .write(key = 1, value = 1.toBv(), guard = mkTrue()) .write(key = 2, value = 2.toBv(), guard = mkTrue()) .write(key = 3, value = 3.toBv(), guard = mkTrue())