diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt index 395b1a797..137d7a8c5 100644 --- a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt +++ b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt @@ -91,6 +91,7 @@ import org.ksmt.sort.KBv32Sort import org.ksmt.sort.KBv64Sort import org.ksmt.sort.KBv8Sort import org.ksmt.sort.KBvSort +import org.ksmt.sort.KFpSort import org.ksmt.sort.KIntSort import org.ksmt.sort.KRealSort import org.ksmt.sort.KSort @@ -587,6 +588,9 @@ open class KBitwuzlaExprInternalizer( override fun visit(sort: KUninterpretedSort): BitwuzlaSort = throw KSolverUnsupportedFeatureException("Unsupported sort $sort") + + override fun visit(sort: S): BitwuzlaSort = + TODO("We do not support KFP sort yet") } open class FunctionSortInternalizer( diff --git a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt index 7e4b33e74..c2a214371 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt @@ -1,5 +1,7 @@ package org.ksmt +import java.lang.Double.longBitsToDouble +import java.lang.Float.intBitsToFloat import org.ksmt.cache.Cache0 import org.ksmt.cache.Cache1 import org.ksmt.cache.Cache2 @@ -183,6 +185,12 @@ import org.ksmt.sort.KBv8Sort import org.ksmt.sort.KBvCustomSizeSort import org.ksmt.sort.KBvSort import org.ksmt.sort.KBoolSort +import org.ksmt.sort.KFp128Sort +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpCustomSizeSort +import org.ksmt.sort.KFpSort import org.ksmt.sort.KIntSort import org.ksmt.sort.KRealSort import org.ksmt.sort.KSort @@ -192,6 +200,12 @@ import kotlin.reflect.KProperty import org.ksmt.decl.KBvRotateLeftIndexedDecl import org.ksmt.decl.KBvRotateRightIndexedDecl import org.ksmt.decl.KBvSubNoUnderflowDecl +import org.ksmt.decl.KFp128Decl +import org.ksmt.decl.KFp16Decl +import org.ksmt.decl.KFp32Decl +import org.ksmt.decl.KFp64Decl +import org.ksmt.decl.KFpCustomSizeDecl +import org.ksmt.decl.KFpDecl import org.ksmt.expr.KBitVec16Value import org.ksmt.expr.KBitVec1Value import org.ksmt.expr.KBitVec32Value @@ -201,8 +215,18 @@ import org.ksmt.expr.KBitVecCustomValue import org.ksmt.expr.KBvRotateLeftIndexedExpr import org.ksmt.expr.KBvRotateRightIndexedExpr import org.ksmt.expr.KBvSubNoUnderflowExpr +import org.ksmt.expr.KFp128Value +import org.ksmt.expr.KFp16Value +import org.ksmt.expr.KFp32Value +import org.ksmt.expr.KFp64Value +import org.ksmt.expr.KFpCustomSizeValue +import org.ksmt.expr.KFpValue import org.ksmt.expr.KFunctionAsArray +import org.ksmt.utils.booleanSignBit import org.ksmt.utils.cast +import org.ksmt.utils.extendWithLeadingZeros +import org.ksmt.utils.extractExponent +import org.ksmt.utils.extractSignificand import org.ksmt.utils.toBinary import org.ksmt.utils.uncheckedCast @@ -266,6 +290,25 @@ open class KContext : AutoCloseable { private val uninterpretedSortCache = mkClosableCache { name: String -> KUninterpretedSort(name, this) } fun mkUninterpretedSort(name: String): KUninterpretedSort = uninterpretedSortCache.createIfContextActive(name) + // floating point + private val fpSortCache = mkCache { exponentBits: UInt, significandBits: UInt -> + when { + exponentBits == KFp16Sort.exponentBits && significandBits == KFp16Sort.significandBits -> KFp16Sort(this) + exponentBits == KFp32Sort.exponentBits && significandBits == KFp32Sort.significandBits -> KFp32Sort(this) + exponentBits == KFp64Sort.exponentBits && significandBits == KFp64Sort.significandBits -> KFp64Sort(this) + exponentBits == KFp128Sort.exponentBits && significandBits == KFp128Sort.significandBits -> KFp128Sort(this) + else -> KFpCustomSizeSort(this, exponentBits, significandBits) + } + } + + fun mkFp16Sort(): KFp16Sort = fpSortCache.create(KFp16Sort.exponentBits, KFp16Sort.significandBits).cast() + fun mkFp32Sort(): KFp32Sort = fpSortCache.create(KFp32Sort.exponentBits, KFp32Sort.significandBits).cast() + fun mkFp64Sort(): KFp64Sort = fpSortCache.create(KFp64Sort.exponentBits, KFp64Sort.significandBits).cast() + fun mkFp128Sort(): KFp128Sort = fpSortCache.create(KFp128Sort.exponentBits, KFp128Sort.significandBits).cast() + fun mkFpSort(exponentBits: UInt, significandBits: UInt): KFpSort = + fpSortCache.create(exponentBits, significandBits) + + // utils val boolSort: KBoolSort get() = mkBoolSort() @@ -627,33 +670,53 @@ open class KContext : AutoCloseable { private val bvCache = mkClosableCache { value: String, sizeBits: UInt -> KBitVecCustomValue(this, value, sizeBits) } fun mkBv(value: Boolean): KBitVec1Value = bv1Cache.createIfContextActive(value) + fun mkBv(value: Boolean, sizeBits: UInt): KBitVecValue = mkBv((if (value) 1 else 0) as Number, sizeBits) fun Boolean.toBv(): KBitVec1Value = mkBv(this) + fun Boolean.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) + + fun mkBv(value: Byte): KBitVec8Value = bv8Cache.createIfContextActive(value) + fun mkBv(value: Byte, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) fun Byte.toBv(): KBitVec8Value = mkBv(this) + fun Byte.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) fun UByte.toBv(): KBitVec8Value = mkBv(toByte()) + fun mkBv(value: Short): KBitVec16Value = bv16Cache.createIfContextActive(value) + fun mkBv(value: Short, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) fun Short.toBv(): KBitVec16Value = mkBv(this) + fun Short.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) fun UShort.toBv(): KBitVec16Value = mkBv(toShort()) + fun mkBv(value: Int): KBitVec32Value = bv32Cache.createIfContextActive(value) + fun mkBv(value: Int, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) fun Int.toBv(): KBitVec32Value = mkBv(this) + fun Int.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) fun UInt.toBv(): KBitVec32Value = mkBv(toInt()) + fun mkBv(value: Long): KBitVec64Value = bv64Cache.createIfContextActive(value) + fun mkBv(value: Long, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) fun Long.toBv(): KBitVec64Value = mkBv(this) + fun Long.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) fun ULong.toBv(): KBitVec64Value = mkBv(toLong()) - fun mkBv(value: Number, sizeBits: UInt): KBitVecValue { - val binaryString = value.toBinary() - - require(binaryString.length <= sizeBits.toInt()) { - "Cannot create a bitvector of size $sizeBits from the given number $value" + - " since its binary representation requires at least ${binaryString.length} bits" - } + /** + * Constructs a bit vector from the given [value] containing of [sizeBits] bits. + * + * Note: if [sizeBits] is less than is required to represent the [value], + * the last [sizeBits] bits of the [value] will be taken. + * + * At the same time, if [sizeBits] is greater than it is required, + * binary representation of the [value] will be padded from the start with its sign bit. + */ + private fun mkBv(value: Number, sizeBits: UInt): KBitVecValue { + val binaryString = value.toBinary().takeLast(sizeBits.toInt()) val paddedString = binaryString.padStart(sizeBits.toInt(), binaryString.first()) return mkBv(paddedString, sizeBits) } - fun Number.toBv(sizeBits: UInt) = mkBv(this, sizeBits) + private fun Number.toBv(sizeBits: UInt) = mkBv(this, sizeBits) + fun mkBv(value: String, sizeBits: UInt): KBitVecValue = when (sizeBits.toInt()) { 1 -> mkBv(value.toUInt(radix = 2).toInt() != 0).cast() Byte.SIZE_BITS -> mkBv(value.toUByte(radix = 2).toByte()).cast() @@ -1015,6 +1078,147 @@ open class KContext : AutoCloseable { fun mkBvMulNoUnderflowExpr(arg0: KExpr, arg1: KExpr): KBvMulNoUnderflowExpr = bvMulNoUnderflowExprCache.createIfContextActive(arg0.cast(), arg1.cast()).cast() + // fp values + private val fp16Cache = mkCache { value: Float -> KFp16Value(this, value) } + private val fp32Cache = mkCache { value: Float -> KFp32Value(this, value) } + private val fp64Cache = mkCache { value: Double -> KFp64Value(this, value) } + private val fp128Cache = mkCache { significand: Long, exponent: Long, signBit: Boolean -> + KFp128Value(this, significand, exponent, signBit) + } + private val fpCustomSizeCache = + mkCache { significandSize: UInt, exponentSize: UInt, significand: Long, exponent: Long, signBit: Boolean -> + KFpCustomSizeValue(this, significandSize, exponentSize, significand, exponent, signBit) + } + + /** + * Creates FP16 from the [value]. + * + * Important: we suppose that [value] has biased exponent, but FP16 will be created from the unbiased one. + * So, at first, we'll subtract [KFp16Sort.exponentShiftSize] from the [value]'s exponent, + * take required for FP16 bits, and this will be **unbiased** FP16 exponent. + * The same is true for other methods but [mkFpCustomSize]. + * */ + fun mkFp16(value: Float): KFp16Value = fp16Cache.create(value) + fun mkFp32(value: Float): KFp32Value = fp32Cache.create(value) + fun mkFp64(value: Double): KFp64Value = fp64Cache.create(value) + fun mkFp128(significand: Long, exponent: Long, signBit: Boolean): KFp128Value = + fp128Cache.create(significand, exponent, signBit) + + /** + * Creates FP with a custom size. + * Important: [exponent] here is an **unbiased** value. + */ + fun mkFpCustomSize( + exponentSize: UInt, + significandSize: UInt, + exponent: Long, + significand: Long, + signBit: Boolean + ): KFpValue { + val intSignBit = if (signBit) 1 else 0 + + return when (mkFpSort(exponentSize, significandSize)) { + is KFp16Sort -> { + val number = constructFp16Number(exponent, significand, intSignBit) + + mkFp16(number).cast() + } + is KFp32Sort -> { + val number = constructFp32Number(exponent, significand, intSignBit) + + mkFp32(number).cast() + } + is KFp64Sort -> { + val number = constructFp64Number(exponent, significand, intSignBit) + + mkFp64(number).cast() + } + is KFp128Sort -> mkFp128(significand, exponent, signBit).cast() + else -> fpCustomSizeCache.create(significandSize, exponentSize, significand, exponent, signBit).cast() + } + } + + fun mkFpCustomSize( + exponent: KBitVecValue, + significand: KBitVecValue, + signBit: Boolean + ): KFpValue { + // TODO we should not use numbers and work with bitvectors. Change it later + val exponentLongValue = exponent.stringValue.toULong(radix = 2).toLong() + val significandLongValue = significand.stringValue.toULong(radix = 2).toLong() + + return mkFpCustomSize( + exponent.sort.sizeBits, + significand.sort.sizeBits, + exponentLongValue, + significandLongValue, + signBit + ) + } + + private fun constructFp16Number(exponent: Long, significand: Long, intSignBit: Int): Float { + // get sign and `body` of the unbiased exponent + val exponentSign = (exponent.toInt() shr 4) and 1 + val otherExponent = exponent.toInt() and 0b1111 + + // get fp16 significand part -- last teb bits (eleventh stored implicitly) + val significandBits = significand.toInt() and 0b1111_1111_11 + + // Transform fp16 exponent into fp32 exponent adding three zeroes between the sign and the body + // Then add the bias for fp32 and apply the mask to avoid overflow of the eight bits + val biasedFloatExponent = (((exponentSign shl 8) or otherExponent) + KFp32Sort.exponentShiftSize) and 0xff + + val bits = (intSignBit shl 31) or (biasedFloatExponent shl 23) or (significandBits shl 13) + + return intBitsToFloat(bits) + } + + private fun constructFp32Number(exponent: Long, significand: Long, intSignBit: Int): Float { + // `and 0xff` here is to avoid overloading when we have a number greater than 255, + // and the result of the addition will affect the sign bit + val biasedExponent = (exponent.toInt() + KFp32Sort.exponentShiftSize) and 0xff + val intValue = (intSignBit shl 31) or (biasedExponent shl 23) or significand.toInt() + + return intBitsToFloat(intValue) + } + + private fun constructFp64Number(exponent: Long, significand: Long, intSignBit: Int): Double { + // `and 0b111_1111_1111` here is to avoid overloading when we have a number greater than 255, + // and the result of the addition will affect the sign bit + val biasedExponent = (exponent + KFp64Sort.exponentShiftSize) and 0b111_1111_1111 + val longValue = (intSignBit.toLong() shl 63) or (biasedExponent shl 52) or significand + + return longBitsToDouble(longValue) + } + + fun mkFp(value: Float, sort: T): KExpr { + val significand = value.extractSignificand(sort) + val exponent = value.extractExponent(sort, isBiased = false).extendWithLeadingZeros() + val sign = value.booleanSignBit + + return mkFpCustomSize(sort.exponentBits, sort.significandBits, exponent, significand.extendWithLeadingZeros(), sign) + } + + fun mkFp(value: Double, sort: T): KExpr { + val significand = value.extractSignificand(sort) + val exponent = value.extractExponent(sort, isBiased = false) + val sign = value.booleanSignBit + + return mkFpCustomSize(sort.exponentBits, sort.significandBits, exponent, significand, sign) + } + + fun mkFp(significand: Int, exponent: Int, signBit: Boolean, sort: T): KExpr = + mkFpCustomSize( + sort.exponentBits, + sort.significandBits, + exponent.extendWithLeadingZeros(), + significand.extendWithLeadingZeros(), + signBit + ) + + fun mkFp(significand: Long, exponent: Long, signBit: Boolean, sort: T): KExpr = + mkFpCustomSize(sort.exponentBits, sort.significandBits, exponent, significand, signBit) + // quantifiers private val existentialQuantifierCache = mkClosableCache { body: KExpr, bounds: List> -> ensureContextMatch(body) @@ -1551,6 +1755,67 @@ open class KContext : AutoCloseable { fun mkBvMulNoUnderflowDecl(arg0: T, arg1: T): KBvMulNoUnderflowDecl = bvMulNoUnderflowDeclCache.createIfContextActive(arg0, arg1).cast() + // FP + private val fp16DeclCache = mkCache { value: Float -> KFp16Decl(this, value) } + fun mkFp16Decl(value: Float): KFp16Decl = fp16DeclCache.create(value) + + private val fp32DeclCache = mkCache { value: Float -> KFp32Decl(this, value) } + fun mkFp32Decl(value: Float): KFp32Decl = fp32DeclCache.create(value) + + private val fp64DeclCache = mkCache { value: Double -> KFp64Decl(this, value) } + fun mkFp64Decl(value: Double): KFp64Decl = fp64DeclCache.create(value) + + private val fp128DeclCache = mkCache { significand: Long, exponent: Long, signBit: Boolean -> + KFp128Decl(this, significand, exponent, signBit) + } + + fun mkFp128Decl(significandBits: Long, exponent: Long, signBit: Boolean): KFp128Decl = + fp128DeclCache.create(significandBits, exponent, signBit) + + private val fpCustomSizeDeclCache = + mkCache { significandSize: UInt, exponentSize: UInt, significand: Long, exponent: Long, signBit: Boolean -> + KFpCustomSizeDecl(this, significandSize, exponentSize, significand, exponent, signBit) + } + + fun mkFpCustomSizeDecl( + significandSize: UInt, + exponentSize: UInt, + significand: Long, + exponent: Long, + signBit: Boolean + ): KFpDecl { + val sort = mkFpSort(exponentSize, significandSize) + + if (sort is KFpCustomSizeSort) { + return fpCustomSizeDeclCache.create(significandSize, exponentSize, significand, exponent, signBit).cast() + } + + if (sort is KFp128Sort) { + return fp128DeclCache.create(significand, exponent, signBit).cast() + } + + val intSignBit = if (signBit) 1 else 0 + + return when (sort) { + is KFp16Sort -> { + val fp16Number = constructFp16Number(exponent, significand, intSignBit) + + mkFp16Decl(fp16Number).cast() + } + is KFp32Sort -> { + val fp32Number = constructFp32Number(exponent, significand, intSignBit) + + mkFp32Decl(fp32Number).cast() + } + is KFp64Sort -> { + val fp64Number = constructFp64Number(exponent, significand, intSignBit) + + mkFp64Decl(fp64Number).cast() + } + else -> error("Sort declaration for an unknown $sort") + } + } + /* * KAst * */ diff --git a/ksmt-core/src/main/kotlin/org/ksmt/cache/Cache.kt b/ksmt-core/src/main/kotlin/org/ksmt/cache/Cache.kt index 6af903d55..9747dce84 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/cache/Cache.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/cache/Cache.kt @@ -55,6 +55,13 @@ class Cache4(val builder: (A0, A1, A2, A3) -> T) : AutoClosea } } +class Cache5(val builder: (A0, A1, A2, A3, A4) -> T) { + private val cache = HashMap, T>() + + @Suppress("unused") + fun create(a0: A0, a1: A1, a2: A2, a3: A3, a4: A4): T = cache.getOrPut(listOf(a0, a1, a2, a3, a4)) { builder(a0, a1, a2, a3, a4) } +} + fun mkCache(builder: () -> T) = Cache0(builder) fun mkCache(builder: (A0) -> T) = Cache1(builder) fun mkCache(builder: (A0, A1) -> T) = Cache2(builder) @@ -62,3 +69,4 @@ fun mkCache(builder: (A0, A1, A2) -> T) = Cache3(builder) @Suppress("unused") fun mkCache(builder: (A0, A1, A2, A3) -> T) = Cache4(builder) +fun mkCache(builder: (A0, A1, A2, A3, A4) -> T) = Cache5(builder) \ No newline at end of file diff --git a/ksmt-core/src/main/kotlin/org/ksmt/decl/KFloatingPointDecl.kt b/ksmt-core/src/main/kotlin/org/ksmt/decl/KFloatingPointDecl.kt new file mode 100644 index 000000000..d516a0bc8 --- /dev/null +++ b/ksmt-core/src/main/kotlin/org/ksmt/decl/KFloatingPointDecl.kt @@ -0,0 +1,116 @@ +package org.ksmt.decl + +import org.ksmt.KContext +import org.ksmt.expr.KApp +import org.ksmt.expr.KExpr +import org.ksmt.sort.KFp128Sort +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpSort +import org.ksmt.utils.getHalfPrecisionExponent +import org.ksmt.utils.booleanSignBit +import org.ksmt.utils.getExponent +import org.ksmt.utils.halfPrecisionSignificand +import org.ksmt.utils.significand +import org.ksmt.utils.toBinary + +abstract class KFpDecl internal constructor( + ctx: KContext, + sort: T, + val sign: Boolean, + val significand: N, + val exponent: N +) : KConstDecl( + ctx, + constructNameForDeclaration(sign, sort, exponent, significand), + sort +) + +private fun constructNameForDeclaration( + sign: Boolean, + sort: T, + exponent: N, + significand: N +): String { + val exponentBits = sort.exponentBits + val binaryExponent = exponent.toBinary().takeLast(exponentBits.toInt()) + val significandBits = sort.significandBits + val binarySignificand = significand + .toBinary() + .takeLast(significandBits.toInt() - 1) + .let { it.padStart(significandBits.toInt() - 1, it[0]) } + + return "FP (sign $sign) ($exponentBits $binaryExponent) ($significandBits $binarySignificand)" +} + +class KFp16Decl internal constructor(ctx: KContext, val value: Float) : + KFpDecl( + ctx, + ctx.mkFp16Sort(), + value.booleanSignBit, + value.halfPrecisionSignificand, + value.getHalfPrecisionExponent(isBiased = false) + ) { + override fun apply(args: List>): KApp = ctx.mkFp16(value) + + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} + +class KFp32Decl internal constructor(ctx: KContext, val value: Float) : + KFpDecl( + ctx, + ctx.mkFp32Sort(), + value.booleanSignBit, + value.significand, + value.getExponent(isBiased = false) + ) { + override fun apply(args: List>): KApp = ctx.mkFp32(value) + + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} + +class KFp64Decl internal constructor(ctx: KContext, val value: Double) : + KFpDecl( + ctx, + ctx.mkFp64Sort(), + value.booleanSignBit, + value.significand, + value.getExponent(isBiased = false) + ) { + override fun apply(args: List>): KApp = ctx.mkFp64(value) + + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} + +// TODO replace significand with bit vector and change KFpDecl accordingly +class KFp128Decl internal constructor( + ctx: KContext, + significand: Long, + exponent: Long, + signBit: Boolean +) : KFpDecl(ctx, ctx.mkFp128Sort(), signBit, significand, exponent) { + override fun apply(args: List>): KApp = ctx.mkFp128(significand, exponent, sign) + + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} + +class KFpCustomSizeDecl internal constructor( + ctx: KContext, + significandSize: UInt, + exponentSize: UInt, + significand: Long, + exponent: Long, + signBit: Boolean +) : KFpDecl(ctx, ctx.mkFpSort(exponentSize, significandSize), signBit, significand, exponent) { + override fun apply(args: List>): KApp = + ctx.mkFpCustomSize( + sort.exponentBits, + sort.significandBits, + exponent, + significand, + sign + ) + + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/KBitVecExprs.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/KBitVecExprs.kt index c51b4be29..adc9eddd0 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/expr/KBitVecExprs.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/KBitVecExprs.kt @@ -11,16 +11,21 @@ import org.ksmt.sort.KBv64Sort import org.ksmt.sort.KBv8Sort import org.ksmt.sort.KBvSort import org.ksmt.sort.KIntSort +import org.ksmt.utils.toBinary abstract class KBitVecValue( ctx: KContext ) : KApp>(ctx) { override val args: List> = emptyList() + + abstract val stringValue: String } class KBitVec1Value internal constructor(ctx: KContext, val value: Boolean) : KBitVecValue(ctx) { override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) + override val stringValue: String = if (value) "1" else "0" + override fun decl(): KDecl = ctx.mkBvDecl(value) override fun sort(): KBv1Sort = ctx.mkBv1Sort() @@ -29,7 +34,9 @@ class KBitVec1Value internal constructor(ctx: KContext, val value: Boolean) : KB abstract class KBitVecNumberValue( ctx: KContext, val numberValue: N -) : KBitVecValue(ctx) +) : KBitVecValue(ctx) { + override val stringValue: String = numberValue.toBinary() +} class KBitVec8Value internal constructor(ctx: KContext, byteValue: Byte) : KBitVecNumberValue(ctx, byteValue) { @@ -81,6 +88,8 @@ class KBitVecCustomValue internal constructor( override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) + override val stringValue: String = binaryStringValue + override fun decl(): KDecl = ctx.mkBvDecl(binaryStringValue, sizeBits) override fun sort(): KBvSort = ctx.mkBvSort(sizeBits) diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/KFloatingPointExpr.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/KFloatingPointExpr.kt new file mode 100644 index 000000000..9d7d9c816 --- /dev/null +++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/KFloatingPointExpr.kt @@ -0,0 +1,138 @@ +package org.ksmt.expr + +import org.ksmt.KContext +import org.ksmt.decl.KDecl +import org.ksmt.sort.KBvSort +import org.ksmt.sort.KFp128Sort +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpSort +import org.ksmt.utils.booleanSignBit +import org.ksmt.utils.getExponent +import org.ksmt.utils.getHalfPrecisionExponent +import org.ksmt.utils.halfPrecisionSignificand +import org.ksmt.utils.significand + +abstract class KFpValue( + ctx: KContext, + val significand: KBitVecValue, + val exponent: KBitVecValue, + val signBit: Boolean +) : KApp>(ctx) { + override val args: List> = emptyList() +} + +/** + * Fp16 value. Note that [value] should has biased Fp32 exponent, + * but a constructed Fp16 will have an unbiased one. + * + * Fp32 to Fp16 transformation: + * sign exponent significand + * 0 00000000 00000000000000000000000 (1 8 23) + * x x___xxxx xxxxxxxxxx_____________ (1 5 10) + */ +class KFp16Value internal constructor(ctx: KContext, val value: Float) : + KFpValue( + ctx, + significand = with(ctx) { value.halfPrecisionSignificand.toBv(KFp16Sort.significandBits - 1u) }, + exponent = with(ctx) { value.getHalfPrecisionExponent(isBiased = false).toBv(KFp16Sort.exponentBits) }, + signBit = value.booleanSignBit + ) { + + init { + // TODO add checks for the bounds + } + + override fun decl(): KDecl = ctx.mkFp16Decl(value) + + override fun sort(): KFp16Sort = ctx.mkFp16Sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFp32Value internal constructor(ctx: KContext, val value: Float) : + KFpValue( + ctx, + significand = with(ctx) { value.significand.toBv(KFp32Sort.significandBits - 1u) }, + exponent = with(ctx) { value.getExponent(isBiased = false).toBv(KFp32Sort.exponentBits) }, + signBit = value.booleanSignBit + ) { + override fun decl(): KDecl = ctx.mkFp32Decl(value) + + override fun sort(): KFp32Sort = ctx.mkFp32Sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFp64Value internal constructor(ctx: KContext, val value: Double) : + KFpValue( + ctx, + significand = with(ctx) { value.significand.toBv(KFp64Sort.significandBits - 1u) }, + exponent = with(ctx) { value.getExponent(isBiased = false).toBv(KFp64Sort.exponentBits) }, + signBit = value.booleanSignBit + ) { + override fun decl(): KDecl = ctx.mkFp64Decl(value) + + override fun sort(): KFp64Sort = ctx.mkFp64Sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +/** + * KFp128 value. + * + * Note: if [exponentValue] contains more than [KFp128Sort.exponentBits] meaningful bits, + * only the last [KFp128Sort.exponentBits] of then will be taken. + */ +class KFp128Value internal constructor( + ctx: KContext, + val significandValue: Long, + val exponentValue: Long, + signBit: Boolean +) : KFpValue( + ctx, + significand = with(ctx) { significandValue.toBv(KFp128Sort.significandBits - 1u) }, + exponent = with(ctx) { exponentValue.toBv(KFp128Sort.exponentBits) }, + signBit +) { + override fun decl(): KDecl = ctx.mkFp128Decl(significandValue, exponentValue, signBit) + + override fun sort(): KFp128Sort = ctx.mkFp128Sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +/** + * KFp value of custom size. + * + * Note: if [exponentValue] contains more than [KFp128Sort.exponentBits] meaningful bits, + * only the last [KFp128Sort.exponentBits] of then will be taken. + * The same is true for the significand. + */ +class KFpCustomSizeValue internal constructor( + ctx: KContext, + val significandSize: UInt, + val exponentSize: UInt, + val significandValue: Long, + val exponentValue: Long, + signBit: Boolean +) : KFpValue( + ctx, + significand = with(ctx) { significandValue.toBv(significandSize - 1u) }, + exponent = with(ctx) { exponentValue.toBv(exponentSize) }, + signBit +) { + init { + require(exponentSize.toInt() <= 63) { "Maximum number of exponent bits is 63" } + } + + override fun decl(): KDecl = + ctx.mkFpCustomSizeDecl(significandSize, exponentSize, significandValue, exponentValue, signBit) + + override fun sort(): KFpSort = ctx.mkFpSort(exponentSize, significandSize) + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + + diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformer.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformer.kt index 164f70f90..97e96775b 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformer.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformer.kt @@ -96,17 +96,22 @@ import org.ksmt.expr.KTrue import org.ksmt.expr.KUnaryMinusArithExpr import org.ksmt.expr.KUniversalQuantifier import org.ksmt.expr.KXorExpr -import org.ksmt.sort.KArraySort import org.ksmt.sort.KArithSort +import org.ksmt.sort.KArraySort +import org.ksmt.sort.KBoolSort import org.ksmt.sort.KBv16Sort import org.ksmt.sort.KBv1Sort import org.ksmt.sort.KBv32Sort import org.ksmt.sort.KBv64Sort import org.ksmt.sort.KBv8Sort +import org.ksmt.sort.KBvSort +import org.ksmt.sort.KFp128Sort +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpSort import org.ksmt.sort.KIntSort import org.ksmt.sort.KRealSort -import org.ksmt.sort.KBvSort -import org.ksmt.sort.KBoolSort import org.ksmt.sort.KSort @@ -146,53 +151,61 @@ interface KTransformer { fun transform(expr: KBitVecCustomValue): KExpr = transformBitVecValue(expr) // bit-vec expressions transformers - fun transform(expr: KBvNotExpr): KExpr = transformApp(expr) - fun transform(expr: KBvReductionAndExpr): KExpr = transformApp(expr) - fun transform(expr: KBvReductionOrExpr): KExpr = transformApp(expr) - fun transform(expr: KBvAndExpr): KExpr = transformApp(expr) - fun transform(expr: KBvOrExpr): KExpr = transformApp(expr) - fun transform(expr: KBvXorExpr): KExpr = transformApp(expr) - fun transform(expr: KBvNAndExpr): KExpr = transformApp(expr) - fun transform(expr: KBvNorExpr): KExpr = transformApp(expr) - fun transform(expr: KBvXNorExpr): KExpr = transformApp(expr) - fun transform(expr: KBvNegationExpr): KExpr = transformApp(expr) - fun transform(expr: KBvAddExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSubExpr): KExpr = transformApp(expr) - fun transform(expr: KBvMulExpr): KExpr = transformApp(expr) - fun transform(expr: KBvUnsignedDivExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedDivExpr): KExpr = transformApp(expr) - fun transform(expr: KBvUnsignedRemExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedRemExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedModExpr): KExpr = transformApp(expr) - fun transform(expr: KBvUnsignedLessExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedLessExpr): KExpr = transformApp(expr) - fun transform(expr: KBvUnsignedLessOrEqualExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedLessOrEqualExpr): KExpr = transformApp(expr) - fun transform(expr: KBvUnsignedGreaterOrEqualExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedGreaterOrEqualExpr): KExpr = transformApp(expr) - fun transform(expr: KBvUnsignedGreaterExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedGreaterExpr): KExpr = transformApp(expr) + fun transform(expr: KBvNotExpr): KExpr = transformApp(expr) + fun transform(expr: KBvReductionAndExpr): KExpr = transformApp(expr) + fun transform(expr: KBvReductionOrExpr): KExpr = transformApp(expr) + fun transform(expr: KBvAndExpr): KExpr = transformApp(expr) + fun transform(expr: KBvOrExpr): KExpr = transformApp(expr) + fun transform(expr: KBvXorExpr): KExpr = transformApp(expr) + fun transform(expr: KBvNAndExpr): KExpr = transformApp(expr) + fun transform(expr: KBvNorExpr): KExpr = transformApp(expr) + fun transform(expr: KBvXNorExpr): KExpr = transformApp(expr) + fun transform(expr: KBvNegationExpr): KExpr = transformApp(expr) + fun transform(expr: KBvAddExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSubExpr): KExpr = transformApp(expr) + fun transform(expr: KBvMulExpr): KExpr = transformApp(expr) + fun transform(expr: KBvUnsignedDivExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedDivExpr): KExpr = transformApp(expr) + fun transform(expr: KBvUnsignedRemExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedRemExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedModExpr): KExpr = transformApp(expr) + fun transform(expr: KBvUnsignedLessExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedLessExpr): KExpr = transformApp(expr) + fun transform(expr: KBvUnsignedLessOrEqualExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedLessOrEqualExpr): KExpr = transformApp(expr) + fun transform(expr: KBvUnsignedGreaterOrEqualExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedGreaterOrEqualExpr): KExpr = transformApp(expr) + fun transform(expr: KBvUnsignedGreaterExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedGreaterExpr): KExpr = transformApp(expr) fun transform(expr: KBvConcatExpr): KExpr = transformApp(expr) fun transform(expr: KBvExtractExpr): KExpr = transformApp(expr) fun transform(expr: KBvSignExtensionExpr): KExpr = transformApp(expr) fun transform(expr: KBvZeroExtensionExpr): KExpr = transformApp(expr) fun transform(expr: KBvRepeatExpr): KExpr = transformApp(expr) - fun transform(expr: KBvShiftLeftExpr): KExpr = transformApp(expr) - fun transform(expr: KBvLogicalShiftRightExpr): KExpr = transformApp(expr) - fun transform(expr: KBvArithShiftRightExpr): KExpr = transformApp(expr) - fun transform(expr: KBvRotateLeftExpr): KExpr = transformApp(expr) - fun transform(expr: KBvRotateLeftIndexedExpr): KExpr = transformApp(expr) - fun transform(expr: KBvRotateRightExpr): KExpr = transformApp(expr) - fun transform(expr: KBvRotateRightIndexedExpr): KExpr = transformApp(expr) + fun transform(expr: KBvShiftLeftExpr): KExpr = transformApp(expr) + fun transform(expr: KBvLogicalShiftRightExpr): KExpr = transformApp(expr) + fun transform(expr: KBvArithShiftRightExpr): KExpr = transformApp(expr) + fun transform(expr: KBvRotateLeftExpr): KExpr = transformApp(expr) + fun transform(expr: KBvRotateLeftIndexedExpr): KExpr = transformApp(expr) + fun transform(expr: KBvRotateRightExpr): KExpr = transformApp(expr) + fun transform(expr: KBvRotateRightIndexedExpr): KExpr = transformApp(expr) fun transform(expr: KBv2IntExpr): KExpr = transformApp(expr) - fun transform(expr: KBvAddNoOverflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvAddNoUnderflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSubNoOverflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSubNoUnderflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvDivNoOverflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvNegNoOverflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvMulNoOverflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvMulNoUnderflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvAddNoOverflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvAddNoUnderflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSubNoOverflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSubNoUnderflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvDivNoOverflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvNegNoOverflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvMulNoOverflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvMulNoUnderflowExpr): KExpr = transformApp(expr) + + // fp value transformers + fun transformFpValue(expr: KFpValue): KExpr = transformApp(expr) + fun transform(expr: KFp16Value): KExpr = transformFpValue(expr) + fun transform(expr: KFp32Value): KExpr = transformFpValue(expr) + fun transform(expr: KFp64Value): KExpr = transformFpValue(expr) + fun transform(expr: KFp128Value): KExpr = transformFpValue(expr) + fun transform(expr: KFpCustomSizeValue): KExpr = transformFpValue(expr) // array transformers fun transform(expr: KArrayStore): KExpr> = transformApp(expr) diff --git a/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt b/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt index b5f0968b6..7d7533bb1 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt @@ -21,6 +21,7 @@ import org.ksmt.expr.KTrue import org.ksmt.sort.KArraySort import org.ksmt.sort.KBvSort import org.ksmt.sort.KBoolSort +import org.ksmt.sort.KFpSort import org.ksmt.sort.KIntSort import org.ksmt.sort.KRealSort import org.ksmt.sort.KSort @@ -162,6 +163,7 @@ open class KModelEvaluator( override fun visit(sort: KIntSort): KExpr = 0.intExpr as KExpr override fun visit(sort: KRealSort): KExpr = mkRealNum(0) as KExpr override fun visit(sort: S): KExpr = mkBv("0", sort.sizeBits) as KExpr + override fun visit(sort: S): KExpr = mkFp(0f, sort) as KExpr override fun visit(sort: KArraySort): KExpr = mkArrayConst(sort, sort.range.sampleValue()) as KExpr override fun visit(sort: KUninterpretedSort): KExpr = diff --git a/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt b/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt index bb9d63578..b9cc20013 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt @@ -95,3 +95,56 @@ class KUninterpretedSort internal constructor(val name: String, ctx: KContext) : builder.append(name) } } + +sealed class KFpSort(ctx: KContext, val exponentBits: UInt, val significandBits: UInt) : KSort(ctx) { + override fun print(builder: StringBuilder) { + builder.append("FP (eBits: $exponentBits) (sBits: $significandBits)") + } + override fun accept(visitor: KSortVisitor): T = visitor.visit(this) + abstract fun exponentShiftSize(): Int +} + +class KFp16Sort(ctx: KContext) : KFpSort(ctx, exponentBits, significandBits) { + override fun exponentShiftSize(): Int = exponentShiftSize + + companion object { + val exponentBits: UInt = 5.toUInt() + val significandBits: UInt = 11.toUInt() + const val exponentShiftSize: Int = 15 + } +} + +class KFp32Sort(ctx: KContext) : KFpSort(ctx, exponentBits, significandBits) { + override fun exponentShiftSize(): Int = exponentShiftSize + + companion object { + val exponentBits: UInt = 8.toUInt() + val significandBits: UInt = 24.toUInt() + const val exponentShiftSize: Int = 127 + } +} + +class KFp64Sort(ctx: KContext) : KFpSort(ctx, exponentBits, significandBits) { + override fun exponentShiftSize(): Int = exponentShiftSize + + companion object { + val exponentBits: UInt = 11.toUInt() + val significandBits: UInt = 53.toUInt() + const val exponentShiftSize: Int = 1023 + } +} + +class KFp128Sort(ctx: KContext) : KFpSort(ctx, exponentBits, significandBits) { + override fun exponentShiftSize(): Int = exponentShiftSize + + companion object { + val exponentBits: UInt = 15.toUInt() + val significandBits: UInt = 113.toUInt() + const val exponentShiftSize: Int = 16383 + } +} + +class KFpCustomSizeSort(ctx: KContext, exponentBits: UInt, significandBits: UInt) : + KFpSort(ctx, exponentBits, significandBits) { + override fun exponentShiftSize(): Int = (1 shl (exponentBits.toInt() - 1)) - 1 +} \ No newline at end of file diff --git a/ksmt-core/src/main/kotlin/org/ksmt/sort/KSortVisitor.kt b/ksmt-core/src/main/kotlin/org/ksmt/sort/KSortVisitor.kt index 5d71ff6ad..95ffc8be6 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/sort/KSortVisitor.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/sort/KSortVisitor.kt @@ -6,6 +6,7 @@ interface KSortVisitor { fun visit(sort: KIntSort): T fun visit(sort: KRealSort): T fun visit(sort: S): T + fun visit(sort: S): T fun visit(sort: KArraySort): T fun visit(sort: KUninterpretedSort): T } diff --git a/ksmt-core/src/main/kotlin/org/ksmt/utils/Utils.kt b/ksmt-core/src/main/kotlin/org/ksmt/utils/Utils.kt index 42725cb73..90ef0935c 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/utils/Utils.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/utils/Utils.kt @@ -1,5 +1,10 @@ package org.ksmt.utils +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpSort + // We can have here `0` as a pad symbol since `toString` can return a string // containing fewer symbols than `sizeBits` only for non-negative numbers fun Number.toBinary(): String = when (this) { @@ -7,9 +12,161 @@ fun Number.toBinary(): String = when (this) { is Short -> toUShort().toString(radix = 2).padStart(Short.SIZE_BITS, '0') is Int -> toUInt().toString(radix = 2).padStart(Int.SIZE_BITS, '0') is Long -> toULong().toString(radix = 2).padStart(Long.SIZE_BITS, '0') + is Float -> toRawBits().toBinary() + is Double -> toRawBits().toBinary() else -> error("Unsupported type for transformation into a binary string: ${this::class.simpleName}") } +/** + * Significand for Fp16 takes 10 bits from the float value: from 14 to 23 bits + */ +val Float.halfPrecisionSignificand: Int + get() = (toRawBits() and 0b0000_0000_0111_1111_1110_0000_0000_0000) shr 13 + +/** + * Take an exponent from the float value. Depending on the [isBiased] is can be either shifted by + * [KFp16Sort.exponentShiftSize] or not. + */ +fun Float.getHalfPrecisionExponent(isBiased: Boolean): Int { + // take an unbiased exponent from the given value + val unbiasedFloatExponent = getExponent(isBiased = false) + // extract a sign bit from it -- fifth one + val signBit = (unbiasedFloatExponent shr 4) and 1 + // take remaining bits of the exponent + val otherBits = unbiasedFloatExponent and 0b1111 + // create an unbiased fp16 exponent containing five bits + val unbiasedFp16Exponent = (signBit shl 4) or otherBits + + return if (isBiased) unbiasedFp16Exponent + KFp16Sort.exponentShiftSize else unbiasedFp16Exponent +} + +/** + * Extracts a significand from the float value. + * + * @see [Float.toRawBits] + */ +val Float.significand: Int get() = toRawBits() and 0x7fffff + +/** + * Extracts an exponent from the float value. + * Depending on the [isBiased] it can be either biased or not. + * + * @see [Float.toRawBits] + */ +fun Float.getExponent(isBiased: Boolean): Int { + // extract exponent using the mask and move it to the right without saving the sign + val exponent = (toRawBits() and 0x7f80_0000) ushr 23 + + return if (isBiased) exponent else exponent - KFp32Sort.exponentShiftSize +} + +val Float.signBit: Int get() = (toRawBits() shr 31) and 1 +val Float.booleanSignBit: Boolean get() = signBit == 1 + +/** + * Extracts a significand from the float value. + * + * @see [Double.toRawBits] + */ +val Double.significand: Long get() = toRawBits() and 0x000f_ffff_ffff_ffff + +/** + * Extracts an exponent from the float value. + * Depending on the [isBiased] it can be either biased or not. + * + * @see [Double.toRawBits] + */ +fun Double.getExponent(isBiased: Boolean): Long { + // extract exponent using the mask and move it to the right without saving the sign + val exponent = (toRawBits() and 0x7ff0_0000_0000_0000) ushr 52 + + return if (isBiased) exponent else exponent - KFp64Sort.exponentShiftSize +} + +val Double.signBit: Int get() = (toRawBits() shr 63).toInt() and 1 +val Double.booleanSignBit: Boolean get() = signBit == 1 + +/** + * Extracts a significand of the specific [sort] from a float value. + */ +fun Float.extractSignificand(sort: KFpSort): Int { + val sizeBits = sort.significandBits.toInt() + // If we need more bits in significand than we have in Fp32's significand, take all ones + // Otherwise, take `sizeBits - 1` of them. + val fp32SignificandBits = KFp32Sort.significandBits.toInt() + val significandMask = if (sizeBits >= fp32SignificandBits) -1 else (1 shl sizeBits - 1) - 1 + + // we want to take first `n` bits from the float significand. + // We take at least zero to avoid incorrect shift for sorts with a large significand bits number. + val shiftForSortSpecificSignificandBits = maxOf(0, fp32SignificandBits - sizeBits) + + return (toRawBits() shr shiftForSortSpecificSignificandBits) and significandMask +} + +/** + * Extends the given 32-bits value to a new 64-bits one with zeroes. + * + * We should use this function instead of [Int.toLong] to avoid moving size bit from its place. + * + * It is important in situations when we want to create a bitvector from (-1) -- it is 32 ones in binary representation. + * Then we want to extend it to 64 bits, but [Int.toLong] will move sign one into the first place in a new value, + * therefore we will have not a value of 32 zeros following by 32 ones, but 100...0011..11, that will change + * the value of the bitvector we wanted to construct. + */ +fun Int.extendWithLeadingZeros(): Long = toLong().let { + ((((it shr 63) and 1) shl 31) or it) and 0xffff_ffff +} + +/** + * Extracts an exponent of the specific [sort] from the fp32 value. + */ +fun Float.extractExponent(sort: KFpSort, isBiased: Boolean): Int { + // extract an exponent from the value in fp32 format + val exponent = getExponent(isBiased = false) + + // find a sign of the exponent + val sign = (exponent shr 7) and 1 + + // take last (exponentBits - 1) bits of the exponent, where exponentBits is specific for the sort + val exponentBits = exponent and ((1 shl (sort.exponentBits.toInt() - 1)) - 1) + + // construct a sort specific exponent + val constructedExponent = (sign shl sort.exponentBits.toInt() - 1) or exponentBits + + return if (isBiased) constructedExponent + sort.exponentShiftSize() else constructedExponent +} + + +/** + * Extracts a significand of the specific [sort] from a double value. + */ +fun Double.extractSignificand(sort: KFpSort): Long { + val significandBits = sort.significandBits.toInt() + val fp64Bits = KFp64Sort.significandBits.toInt() + + // If we need more bits in significand than we have in Fp32's significand, take all ones + // Otherwise, take `sizeBits - 1` of them. + val significandMask = if (significandBits >= fp64Bits) -1 else (1L shl significandBits - 1) - 1 + // we want to take first `n` bits from the float significand. + // We take at least zero to avoid incorrect shift for sorts with a large significand bits number. + val shiftForSortSpecificSignificandBits = maxOf(0, 53 - significandBits) + + return (toRawBits() shr shiftForSortSpecificSignificandBits) and significandMask +} + +/** + * Extracts an exponent of the specific [sort] from the fp64 value. + */ +fun Double.extractExponent(sort: KFpSort, isBiased: Boolean): Long { + val exponent = getExponent(isBiased = false) + val sign = (exponent shr 10) and 1 + val exponentBits = exponent and (1L shl (sort.exponentBits.toInt() - 1)) - 1 + + val constructedExponent = (sign shl sort.exponentBits.toInt() - 1) or exponentBits + + return if (isBiased) constructedExponent + sort.exponentShiftSize() else constructedExponent +} + inline fun Base.cast(): T where T : Base = this as T @Suppress("UNCHECKED_CAST") diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprConverter.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprConverter.kt index f15f5411c..1ab071991 100644 --- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprConverter.kt +++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprConverter.kt @@ -4,6 +4,8 @@ import com.microsoft.z3.ArraySort import com.microsoft.z3.BitVecNum import com.microsoft.z3.BitVecSort import com.microsoft.z3.Expr +import com.microsoft.z3.FPNum +import com.microsoft.z3.FPSort import com.microsoft.z3.FuncDecl import com.microsoft.z3.IntNum import com.microsoft.z3.Quantifier @@ -28,6 +30,8 @@ import org.ksmt.sort.KArithSort import org.ksmt.sort.KArraySort import org.ksmt.sort.KBoolSort import org.ksmt.sort.KBvSort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpSort import org.ksmt.sort.KSort open class KZ3ExprConverter( @@ -70,11 +74,14 @@ open class KZ3ExprConverter( mkArraySort(convertSort(it.domain), convertSort(it.range)) } Z3_sort_kind.Z3_BV_SORT -> mkBvSort((sort as BitVecSort).size.toUInt()) + Z3_sort_kind.Z3_FLOATING_POINT_SORT -> { + val fpSort = sort as FPSort + mkFpSort(fpSort.eBits.toUInt(), fpSort.sBits.toUInt()) + } Z3_sort_kind.Z3_UNINTERPRETED_SORT -> mkUninterpretedSort(sort.name.toString()) Z3_sort_kind.Z3_DATATYPE_SORT, Z3_sort_kind.Z3_RELATION_SORT, Z3_sort_kind.Z3_FINITE_DOMAIN_SORT, - Z3_sort_kind.Z3_FLOATING_POINT_SORT, Z3_sort_kind.Z3_ROUNDING_MODE_SORT, Z3_sort_kind.Z3_SEQ_SORT, Z3_sort_kind.Z3_RE_SORT, @@ -244,6 +251,23 @@ open class KZ3ExprConverter( ?: error("unexpected as-array decl $z3Decl") mkFunctionAsArray(decl) } + Z3_decl_kind.Z3_OP_FPA_NUM -> convert { + with(expr as FPNum) { + val sort = convertSort(sort) as KFpSort + val sBits = sort.significandBits.toInt() + val fp64SizeBits = KFp64Sort.exponentBits.toInt() + KFp64Sort.significandBits.toInt() + + // if we have sBits greater than long size bits, take it all, otherwise take last (sBits - 1) bits + val significandMask = if (sBits < fp64SizeBits) (1L shl (sBits - 1)) - 1 else -1 + // TODO it is not right if we have significand with number of bits greater than 64 + val significand = significandUInt64 and significandMask + + val exponentMask = (1L shl sort.exponentBits.toInt()) - 1 + val exponent = getExponentInt64(false) and exponentMask + + mkFp(significand, exponent, sign, sort) + } + } else -> TODO("${expr.funcDecl} (${expr.funcDecl.declKind}) is not supported") } } diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprInternalizer.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprInternalizer.kt index e9eaadd62..9b788eab0 100644 --- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprInternalizer.kt +++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprInternalizer.kt @@ -8,6 +8,7 @@ import com.microsoft.z3.BoolExpr import com.microsoft.z3.BoolSort import com.microsoft.z3.Context import com.microsoft.z3.Expr +import com.microsoft.z3.FPSort import com.microsoft.z3.FuncDecl import com.microsoft.z3.IntExpr import com.microsoft.z3.Sort @@ -76,7 +77,6 @@ import org.ksmt.expr.KBvUnsignedLessOrEqualExpr import org.ksmt.expr.KBvUnsignedRemExpr import org.ksmt.expr.KBvXNorExpr import org.ksmt.expr.KBvXorExpr -import org.ksmt.expr.KBvZeroExtensionExpr import org.ksmt.expr.KConst import org.ksmt.expr.KDistinctExpr import org.ksmt.expr.KDivArithExpr @@ -108,11 +108,24 @@ import org.ksmt.expr.KToRealIntExpr import org.ksmt.expr.KTrue import org.ksmt.expr.KUnaryMinusArithExpr import org.ksmt.expr.KUniversalQuantifier +import org.ksmt.expr.KBvZeroExtensionExpr +import org.ksmt.expr.KFp128Value +import org.ksmt.expr.KFp16Value +import org.ksmt.expr.KFp32Value +import org.ksmt.expr.KFp64Value +import org.ksmt.expr.KFpCustomSizeValue +import org.ksmt.expr.KFpValue import org.ksmt.expr.KXorExpr import org.ksmt.solver.util.KExprInternalizerBase import org.ksmt.sort.KArithSort import org.ksmt.sort.KBoolSort import org.ksmt.sort.KBvSort +import org.ksmt.sort.KFp128Sort +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpSort +import org.ksmt.sort.KIntSort import org.ksmt.sort.KSort @Suppress("SpreadOperator") @@ -366,6 +379,34 @@ open class KZ3ExprInternalizer( override fun transform(expr: KBvMulNoUnderflowExpr) = with(expr) { transform(arg0, arg1, z3Ctx::mkBVMulNoUnderflow) } + override fun transformFpValue(expr: KFpValue): KExpr = expr.transform { + with(expr) { + when (this) { + is KFp16Value -> z3Ctx.mkFP(value, z3Ctx.mkFPSort16()) + is KFp32Value -> z3Ctx.mkFP(value, z3Ctx.mkFPSort32()) + is KFp64Value -> z3Ctx.mkFP(value, z3Ctx.mkFPSort64()) + is KFp128Value -> z3Ctx.mkFP(signBit, exponentValue, significandValue, z3Ctx.mkFPSort128()) + is KFpCustomSizeValue -> z3Ctx.mkFP( + signBit, + exponentValue, + significandValue, + z3Ctx.mkFPSort(sort().exponentBits.toInt(), sort().significandBits.toInt()) + ) + else -> error("Unexpected KFpValue type: ${this::class.qualifiedName}") + } + } + } + + override fun transform(expr: KFp16Value): KExpr = transformFpValue(expr) + + override fun transform(expr: KFp32Value): KExpr = transformFpValue(expr) + + override fun transform(expr: KFp64Value): KExpr = transformFpValue(expr) + + override fun transform(expr: KFp128Value): KExpr = transformFpValue(expr) + + override fun transform(expr: KFpCustomSizeValue): KExpr = transformFpValue(expr) + override fun transform(expr: KArrayStore) = with(expr) { transform, Expr, Expr, KArrayStore>( array, index, value, z3Ctx::mkStore diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt index 301ac2710..0eb0fc068 100644 --- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt +++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt @@ -121,7 +121,9 @@ open class KZ3Solver(private val ctx: KContext) : KSolver { } override fun model(): KModel = z3Try { - require(lastCheckStatus == KSolverStatus.SAT) { "Model are only available after SAT checks" } + require(lastCheckStatus == KSolverStatus.SAT) { + "Model are only available after SAT checks, current solver status: $lastCheckStatus" + } val model = solver.model KZ3Model(model, ctx, z3InternCtx, exprInternalizer, exprConverter) } diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SortInternalizer.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SortInternalizer.kt index 8254b10b8..3daca1b7e 100644 --- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SortInternalizer.kt +++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SortInternalizer.kt @@ -8,6 +8,12 @@ import org.ksmt.sort.KRealSort import org.ksmt.sort.KBvSort import org.ksmt.sort.KArraySort import org.ksmt.sort.KBoolSort +import org.ksmt.sort.KFp128Sort +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpCustomSizeSort +import org.ksmt.sort.KFpSort import org.ksmt.sort.KSort import org.ksmt.sort.KUninterpretedSort @@ -36,6 +42,16 @@ open class KZ3SortInternalizer( override fun visit(sort: T): Sort = z3InternCtx.internalizeSort(sort) { z3Ctx.mkBitVecSort(sort.sizeBits.toInt()) } + override fun visit(sort: S): Sort = z3InternCtx.internalizeSort(sort) { + when (sort) { + is KFp16Sort -> z3Ctx.mkFPSort16() + is KFp32Sort -> z3Ctx.mkFPSort32() + is KFp64Sort -> z3Ctx.mkFPSort64() + is KFp128Sort -> z3Ctx.mkFPSort128() + is KFpCustomSizeSort -> z3Ctx.mkFPSort(sort.exponentBits.toInt(), sort.significandBits.toInt()) + else -> error("Unsupported sort: $sort") + } + } override fun visit(sort: KUninterpretedSort): Sort = z3InternCtx.internalizeSort(sort) { z3Ctx.mkUninterpretedSort(sort.name) diff --git a/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/BitVecTest.kt b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/BitVecTest.kt index 3a04e2f8a..26e36c793 100644 --- a/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/BitVecTest.kt +++ b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/BitVecTest.kt @@ -3,7 +3,6 @@ package org.ksmt.solver.z3 import kotlin.random.Random import kotlin.random.nextUInt import kotlin.test.assertEquals -import kotlin.test.assertFailsWith import kotlin.test.assertFalse import kotlin.test.assertTrue import org.junit.jupiter.api.AfterEach @@ -178,12 +177,26 @@ class BitVecTest { } @Test - fun testCreateIllegalBv(): Unit = with(context) { + fun testCreateBvNarrowingTransformation(): Unit = with(context) { val sizeBits = 42u - val stringValue = "0".repeat(sizeBits.toInt() - 1) + val bitvector = mkBv(Long.MAX_VALUE, sizeBits) as KBitVecCustomValue - assertFailsWith(IllegalArgumentException::class) { mkBv(stringValue, sizeBits) } - assertFailsWith(IllegalArgumentException::class) { mkBv(Long.MAX_VALUE, sizeBits) } + assertEquals(bitvector.binaryStringValue, Long.MAX_VALUE.toBinary().takeLast(sizeBits.toInt())) + } + + @Test + fun testCreateBvWithGreaterSize(): Unit = with(context) { + val sizeBits = 100u + val positiveBv = mkBv(Long.MAX_VALUE, sizeBits) as KBitVecCustomValue + val negativeBv = mkBv(Long.MIN_VALUE, sizeBits) as KBitVecCustomValue + + val sizeDifference = sizeBits.toInt() - Long.SIZE_BITS + + assertEquals(positiveBv.binaryStringValue.take(sizeDifference), "0".repeat(sizeDifference)) + assertEquals(negativeBv.binaryStringValue.take(sizeDifference), "1".repeat(sizeDifference)) + + assertEquals(positiveBv.binaryStringValue.takeLast(Long.SIZE_BITS), Long.MAX_VALUE.toBinary()) + assertEquals(negativeBv.binaryStringValue.takeLast(Long.SIZE_BITS), Long.MIN_VALUE.toBinary()) } @Test diff --git a/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/FloatingPointTest.kt b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/FloatingPointTest.kt new file mode 100644 index 000000000..e6ac54604 --- /dev/null +++ b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/FloatingPointTest.kt @@ -0,0 +1,217 @@ +package org.ksmt.solver.z3 + +import java.lang.Float.intBitsToFloat +import kotlin.math.sign +import kotlin.random.Random +import kotlin.random.nextUInt +import kotlin.test.assertTrue +import org.junit.jupiter.api.AfterEach +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Disabled +import org.junit.jupiter.api.Test +import org.ksmt.KContext +import org.ksmt.expr.KExpr +import org.ksmt.sort.KFpSort +import org.ksmt.utils.booleanSignBit +import org.ksmt.utils.extractExponent +import org.ksmt.utils.extractSignificand + + +class FloatingPointTest { + private var context = KContext() + private var solver = KZ3Solver(context) + + @BeforeEach + fun createNewEnvironment() { + context = KContext() + solver = KZ3Solver(context) + } + + @AfterEach + fun clearResources() { + solver.close() + } + + private fun KContext.symbolicValuesCheck(symbolicValues: List>, sort: S) { + val symbolicConsts = symbolicValues.indices.map { sort.mkConst("const_${it}") } + val pairs = symbolicValues.zip(symbolicConsts) + + pairs.forEach { (value, const) -> + solver.assert(value eq const) + } + + solver.check() + val model = solver.model() + + pairs.forEach { (value, const) -> + assertTrue( + "Values for $const are different: ${System.lineSeparator()}" + + "expected: $value ${System.lineSeparator()}" + + "found: ${model.eval(const)}" + ) { model.eval(const) === value } + } + } + + private fun KContext.createSymbolicValues( + it: Float, + sort: S, + mkSpecificSort: (Float) -> KExpr + ): List> = listOf( + mkSpecificSort(it), + mkFp(it, sort), + mkFp( + it.extractSignificand(sort), + it.extractExponent(sort, isBiased = false), + signBit = it.booleanSignBit, + sort + ), + mkFp( + it.extractSignificand(sort).toLong(), + it.extractExponent(sort, isBiased = false).toLong(), + signBit = it.booleanSignBit, + sort + ) + ) + + private fun KContext.createSymbolicValues( + it: Double, + sort: S, + mkSpecificSort: (Double) -> KExpr + ): List> = listOf( + mkSpecificSort(it), + mkFp(it, sort), + mkFp( + it.extractSignificand(sort), + it.extractExponent(sort, isBiased = false), + signBit = it.booleanSignBit, + sort + ), + mkFp( + it.extractSignificand(sort), + it.extractExponent(sort, isBiased = false), + signBit = it.booleanSignBit, + sort + ) + ) + + @Test + fun testCreateFp16(): Unit = with(context) { + val values = (0..10000) + .map { + val sign = Random.nextInt(from = 0, until = 2) + val exponent = Random.nextInt(from = 128, until = 142) + val significand = Random.nextInt(from = 0, until = 1024) + intBitsToFloat(((sign shl 31) or (exponent shl 23) or (significand shl 13))) + }.distinct() + + val sort = mkFp16Sort() + + val symbolicValues = values.map { + createSymbolicValues(it, sort, context::mkFp16).distinct().single() + } + + symbolicValuesCheck(symbolicValues, sort) + } + + @Test + fun testCreateFp32(): Unit = with(context) { + val values = (0..10000).map { Random.nextFloat() } + + val sort = mkFp32Sort() + + val symbolicValues = values.map { + createSymbolicValues(it, sort, context::mkFp32).distinct().single() + } + + symbolicValuesCheck(symbolicValues, sort) + } + + @Test + fun testCreateFp64(): Unit = with(context) { + val values = (0..1000).map { + Random.nextFloat().toDouble() + } + + val sort = mkFp64Sort() + + val symbolicValues = values.map { + createSymbolicValues(it, sort, context::mkFp64).distinct().single() + } + + symbolicValuesCheck(symbolicValues, sort) + } + + @Test + fun testCreateFp128(): Unit = with(context) { + val values = (0..1000) + .map { + Random.nextLong() to Random.nextLong( + from = 0b000000000000000.toLong(), + until = 0b011111111111111.toLong() + ) * sign(Random.nextInt().toDouble()).toLong() + } + + val randomDoubles = (0..1000).map { Random.nextDouble() } + val randomFloats = (0..1000).map { Random.nextFloat() } + + val signBit = Random.nextBoolean() + + val sort = mkFp128Sort() + + val symbolicValues = values.map { + listOf( + mkFp128(it.first, it.second, signBit), + mkFp(it.first, it.second, signBit, sort) + ).distinct().single() + }.toMutableList() + + symbolicValues += randomDoubles.map { mkFp(it, sort) } + symbolicValues += randomFloats.map { mkFp(it, sort) } + + symbolicValuesCheck(symbolicValues, sort) + } + + @Test + @Disabled("Not supported yet, doesn't work with particular sorts, for example, FP 32 132") + fun testCreateFpCustomSize(): Unit = + repeat(10) { + createNewEnvironment() + with(context) { + // mkFpSort(3u, 127u) listOf(mkFp(-1054027720, sort)) and 2u don't work + val sort = mkFpSort( + Random.nextInt(from = 2, until = 64).toUInt(), + Random.nextUInt(from = 10u, until = 150u) + ) + // val sort = mkFpSort(4u, 92u) + + println("${it + 1} run, sort: $sort") + + val values = (0..100) + .map { + val (significand, exponent) = Random.nextLong() to Random.nextLong() + val finalSignificand = significand and ((1L shl sort.significandBits.toInt() - 1) - 1) + val finalExponent = exponent and ((1L shl sort.exponentBits.toInt()) - 1) + + finalSignificand to finalExponent + } + // TODO this combination doesn't work + // 7 run, sort: FP (eBits: 6) (sBits: 109) + // val values = listOf((-8634236606667726792L to 33L)) + + // TODO here we should apply masks to avoid exponents that are not in [min..max] range + val randomDoubles = (0..1000).map { Random.nextDouble() } + val randomFloats = (0..1000).map { Random.nextFloat() } + + val signBit = Random.nextBoolean() + + // TODO not supported yet + val symbolicValues = values.mapTo(mutableListOf()) { (significand, exponent) -> + mkFp(significand, exponent, signBit, sort) + } + symbolicValues += randomDoubles.mapTo(mutableListOf()) { value -> mkFp(value, sort) } + symbolicValues += randomFloats.map { value -> mkFp(value, sort) } + + symbolicValuesCheck(symbolicValues, sort) + } + } +}