diff --git a/java-backend/src/main/java/org/kframework/backend/java/builtins/BuiltinFloatOperations.java b/java-backend/src/main/java/org/kframework/backend/java/builtins/BuiltinFloatOperations.java index 90cd0e9120..1f6ab4def5 100644 --- a/java-backend/src/main/java/org/kframework/backend/java/builtins/BuiltinFloatOperations.java +++ b/java-backend/src/main/java/org/kframework/backend/java/builtins/BuiltinFloatOperations.java @@ -6,6 +6,7 @@ import org.kframework.backend.java.kil.*; import org.kframework.mpfr.BigFloat; import org.kframework.mpfr.BinaryMathContext; +import java.math.BigInteger; /** * Table of {@code public static} methods on builtin floats. @@ -231,6 +232,145 @@ public static IntToken float2int(FloatToken term, TermContext context) { .withRoundingMode(RoundingMode.DOWN)).toBigIntegerExact()); } + /** + * mint2float converts a Bitvector or MInt {@code term} to an single or double precision float point value. + */ + public static FloatToken mint2float(BitVector term, IntToken precision, IntToken exponentBits, TermContext context) { + + + int termBitwidth = term.bitwidth(); + int expectedPrecision = precision.intValue(); + int expectedExponentBits = exponentBits.intValue(); + + // Sanity Checks. + if(termBitwidth != expectedExponentBits + expectedPrecision) { + throw new IllegalArgumentException("A float with requested precision and exponentBit cannot be obtained from the input MInt"); + } + + if(termBitwidth != 32 && termBitwidth != 64) { + throw new IllegalArgumentException("Illegal bitwidth provided: " + + "Only 32 or 64 are supported in order to obtain a single precision or double precision floating point value"); + } + + // Determine the sign. + boolean sign = !term.extract(0,1).isZero(); + + // Determine if a double or single precision floating point is requested and fix constants + // based on them. + boolean isDoublePrecision = (precision.intValue() == 53 && exponentBits.intValue() == 11); + int beginExponent = 1, endExponent = 0 , beginSignificand = 0 , endSignificand = 0; + if(isDoublePrecision) { + endExponent = 12; + beginSignificand = 12; + endSignificand = 64; + } else { + endExponent = 9; + beginSignificand = 9; + endSignificand = 32; + } + + BitVector biasedExponentBV = term.extract(beginExponent, endExponent); + BitVector significandBV = term.extract(beginSignificand, endSignificand); + + // Case I: biasedExponentBV == 0H and significand == 0H, return +0 or -0. + if(biasedExponentBV.isZero() && significandBV.isZero()) { + if(sign) { + return FloatToken.of(BigFloat.negativeZero(precision.intValue()), exponentBits.intValue()); + } else { + return FloatToken.of(BigFloat.zero(precision.intValue()), exponentBits.intValue()); + } + } + + // Case II: biasedExponentBV == all Ones and significandBV == 0H, return +inf/-inf + // biasedExponentBV == all Ones and significandBV != 0H, return nan. + if(biasedExponentBV.eq(BitVector.of(-1, expectedExponentBits)).booleanValue()) { + if(significandBV.isZero()) { + if(sign) { + return FloatToken.of(BigFloat.negativeInfinity(precision.intValue()), exponentBits.intValue()); + } else { + return FloatToken.of(BigFloat.positiveInfinity(precision.intValue()), exponentBits.intValue()); + } + } else { + return FloatToken.of(BigFloat.NaN(precision.intValue()), exponentBits.intValue()); + } + } + + // Case III: Sub-Nornals: biasedExponentBV == 0H and significand != 0H + // Normals: biasedExponentBV > 0H and biasedExponentBV < all Ones + // For sub-normals, 0 need to be prepended to significandBV. + // For Normals, 1 need to be appended. + if(biasedExponentBV.isZero()) { + significandBV = BitVector.of(0,1).concatenate(significandBV); + } else { + significandBV = BitVector.of(1,1).concatenate(significandBV); + } + + + // Compute the unbiased exponent. + BigInteger bias = BigInteger.valueOf(2).pow( exponentBits.intValue() - 1 ).subtract(BigInteger.ONE); + long exponent = biasedExponentBV.unsignedValue().longValue()- bias.longValue(); + + // Compute the BigFloat. + BinaryMathContext mc = new BinaryMathContext(precision.intValue(), exponentBits.intValue()); + return FloatToken.of(new BigFloat(sign, + significandBV.unsignedValue(), exponent, mc), + exponentBits.intValue()); + } + + /** + * float2mint converts a float point value (single or double precision) {@code term} to a BitVector or MInt + * of bitwidth {@code bitwidth}. + */ + public static BitVector float2mint(FloatToken term, IntToken bitwidth, TermContext context) { + BinaryMathContext mc = getMathContext(term); + + int termPrecision = term.bigFloatValue().precision(); + long termExponent = term.bigFloatValue().exponent(mc.minExponent, mc.maxExponent); + int termExponentBits = term.exponent(); + + // Sanity Checks. + if(bitwidth.intValue() != 32 && bitwidth.intValue() != 64) { + throw new IllegalArgumentException("Illegal bitwidth provided: Only 32 or 64 are supported"); + } + + int expectedPrecision = (bitwidth.intValue() == 32)? 24 : 53; + int expectedExponentBits = (bitwidth.intValue() == 32)? 8 : 11; + + if(termPrecision != expectedPrecision || termExponentBits != expectedExponentBits) { + throw new IllegalArgumentException("mismatch precision or exponent bits: " + + "input floating point precision " + termPrecision + "whereas expected precision based on bitwidth " + expectedPrecision + + "input floating point exponent bits " + termExponentBits + "whereas expected exponent bits " + expectedExponentBits); + } + + + BigInteger bias = BigInteger.valueOf(2).pow( termExponentBits - 1 ).subtract(BigInteger.ONE); + + // Compute MInt for sign. + boolean sign = term.bigFloatValue().sign(); + BitVector signBV = BitVector.of((sign)?1:0,1); + + // Compute MInt for significand. + BitVector termSignificand = BitVector.of(term.bigFloatValue().significand(mc.minExponent, mc.maxExponent), mc.precision); + BitVector significandBV = termSignificand.extract(1, mc.precision); + + BigFloat termBigFloat = term.bigFloatValue(); + // Case I: positive/negative zero and sub-normals + if(termBigFloat.isNegativeZero() || termBigFloat.isPositiveZero() || termBigFloat.isSubnormal(mc.minExponent)) { + BitVector exponentBV = BitVector.of(0, termExponentBits); + return signBV.concatenate(exponentBV.concatenate(significandBV)); + } + + // Case II: Nan and Infinite(Positive or Negative) + if(termBigFloat.isNaN() || termBigFloat.isInfinite()) { + BitVector exponentBV = BitVector.of(-1, termExponentBits); + return signBV.concatenate(exponentBV.concatenate(significandBV)); + } + + // Case III: Normalized values + BitVector exponentBV = BitVector.of(termExponent + bias.longValue(), termExponentBits); + return signBV.concatenate(exponentBV.concatenate(significandBV)); + } + public static FloatToken ceil(FloatToken term, TermContext context) { return FloatToken.of(term.bigFloatValue().rint(getMathContext(term) .withRoundingMode(RoundingMode.CEILING)), term.exponent()); diff --git a/java-backend/src/main/resources/org/kframework/backend/java/symbolic/hooks.properties b/java-backend/src/main/resources/org/kframework/backend/java/symbolic/hooks.properties index 1cbd526b64..eb1979320f 100644 --- a/java-backend/src/main/resources/org/kframework/backend/java/symbolic/hooks.properties +++ b/java-backend/src/main/resources/org/kframework/backend/java/symbolic/hooks.properties @@ -155,6 +155,8 @@ STRING.float2string : org.kframework.backend.java.builtins.BuiltinStringOperatio STRING.floatFormat : org.kframework.backend.java.builtins.BuiltinStringOperations.floatFormat FLOAT.int2float : org.kframework.backend.java.builtins.BuiltinFloatOperations.int2float FLOAT.float2int : org.kframework.backend.java.builtins.BuiltinFloatOperations.float2int +FLOAT.mint2float : org.kframework.backend.java.builtins.BuiltinFloatOperations.mint2float +FLOAT.float2mint : org.kframework.backend.java.builtins.BuiltinFloatOperations.float2mint STRING.token2string : org.kframework.backend.java.builtins.BuiltinStringOperations.token2string STRING.string2token : org.kframework.backend.java.builtins.BuiltinStringOperations.string2token STRING.string2id : org.kframework.backend.java.builtins.BuiltinStringOperations.string2id diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index 67fe96eb8f..05d6fe85d7 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -359,6 +359,7 @@ endmodule module FLOAT imports FLOAT-SYNTAX imports BOOL + imports MINT imports INT-SYNTAX syntax Int ::= precisionFloat(Float) [function, hook(FLOAT.precision)] @@ -416,6 +417,8 @@ module FLOAT syntax Float ::= Int2Float(Int, Int, Int) [function, latex({\\it{}Int2Float}), hook(FLOAT.int2float)] syntax Int ::= Float2Int(Float) [function, latex({\\it{}Float2Int}), hook(FLOAT.float2int)] + syntax Float ::= MInt2Float(MInt, Int, Int) [function, latex({\\it{}MInt2Float}), hook(FLOAT.mint2float)] + syntax MInt ::= Float2MInt(Float, Int) [function, latex({\\it{}Float2MInt}), hook(FLOAT.float2mint)] rule sqrtFloat(F:Float) => rootFloat(F, 2) diff --git a/k-distribution/tests/builtins/config.xml b/k-distribution/tests/builtins/config.xml index 11e3989c44..cacb0de9bc 100644 --- a/k-distribution/tests/builtins/config.xml +++ b/k-distribution/tests/builtins/config.xml @@ -14,4 +14,5 @@ skip="pdf" > + diff --git a/k-distribution/tests/builtins/float/config.xml b/k-distribution/tests/builtins/float/config.xml new file mode 100644 index 0000000000..3cf4395228 --- /dev/null +++ b/k-distribution/tests/builtins/float/config.xml @@ -0,0 +1,9 @@ + + + + + + diff --git a/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k b/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k new file mode 100644 index 0000000000..41a5c8ed5c --- /dev/null +++ b/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k @@ -0,0 +1,30 @@ +// Copyright (c) 2016 K Team. All Rights Reserved. +requires "domains.k" + +module CONVERTFLOATMINT-TEST-SYNTAX + imports MINT + imports FLOAT + + syntax Task ::= "test" "(" Int "," Float "," Int "," Int "," Int ")" [function] + | "sub" "(" Int "," Int "," Int "," Int "," Int "," Int")" [function] + | "add" "(" Int "," Int "," Int "," Int "," Int "," Int")" [function] + syntax Tasks ::= List{Task, ""} +endmodule + +module CONVERTFLOATMINT-TEST + imports CONVERTFLOATMINT-TEST-SYNTAX + + configuration $PGM:Tasks + + rule T:Task Ts:Tasks => T ~> Ts + rule test(I, F, W, P, E) => eqMInt(mi(W, I), Float2MInt(MInt2Float(mi(W,I), P,E), W)) + andBool F ==Float MInt2Float(Float2MInt(F,W), P, E) + andBool MInt2Float(mi(W,I), P,E) ==Float F + andBool eqMInt(Float2MInt(F,W), mi(W,I)) + + //To test that the precision and exponent information are not modified over Float operations. + rule sub(I, J, K, W, P, E) => eqMInt(Float2MInt(MInt2Float(mi(W, I), P, E) -Float MInt2Float(mi(W, J), P, E), W), + mi(W, K)) + rule add(I, J, K, W, P, E) => eqMInt(Float2MInt(MInt2Float(mi(W, I), P, E) +Float MInt2Float(mi(W, J), P, E), W), + mi(W, K)) +endmodule diff --git a/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint b/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint new file mode 100644 index 0000000000..e935344802 --- /dev/null +++ b/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint @@ -0,0 +1,102 @@ +test(0, 0f,32,24,8) +test(2147483648, -0f, 32,24,8) +test(-2147483648, -0f, 32,24,8) +test(1040187392, 0.125f, 32,24,8) +test(1048576000, 0.25f, 32,24,8) +test(1056964608, 0.5f, 32,24,8) +test(1065353216, 1f, 32,24,8) +test(1073741824, 2f, 32,24,8) +test(1082130432, 4f, 32,24,8) +test(1090519040, 8f, 32,24,8) +test(1052770304, 0.375f, 32,24,8) +test(1061158912, 0.75f, 32,24,8) +test(1069547520, 1.5f, 32,24,8) +test(1077936128, 3f, 32,24,8) +test(1086324736, 6f, 32,24,8) +test(1036831949,0.10000000149011612f, 32,24,8) +test(1045220557, 0.20000000298023224f, 32,24,8) +test(1053609165, 0.40000000596046448f, 32,24,8) +test(1061997773, 0.80000001192092896f, 32,24,8) +test(1399379109, 999999995904f, 32,24,8) +test(1733542428, 1.0000000138484279e+24f, 32,24,8) +test(2067830734, 9.9999996169031625e+35f, 32,24,8) +test(2139095040, Infinityf, 32,24,8) +test(-8388608, -Infinityf, 32,24,8) +test(4286578688, -Infinityf, 32,24,8) +test(-1073741824, -2f, 32,24,8) +test(3221225472, -2f, 32,24,8) +test(1103626240, 25f, 32,24,8) +test(2139095039, 3.402823466E+38f, 32,24,8) +test(8388608, 1.17549435E-38f, 32,24,8) +test(1078530011, 3.1415927410f, 32,24,8) +test(1051372203, 0.333333333333333f, 32,24,8) +test(1095106560, 12.375f, 32,24,8) +test(1116225274, 68.123f, 32,24,8) +test(1077936128, 3f, 32,24,8) +test(3225419776, -3f, 32,24,8) +test(-1069547520, -3f, 32,24,8) +test(1073741825, 2.0000002f, 32,24,8) +test(3221225473, -2.0000002f, 32,24,8) +test(-1073741823, -2.0000002f, 32,24,8) +test(4194304, 5.877472E-39f, 32,24,8) +test(-2143289343, -5.877473E-39f, 32,24,8) +test(2151677953, -5.877473E-39f, 32,24,8) +test(2139095039, 3.4028235E38f, 32,24,8) +test(-8388609, -3.4028235E38f, 32,24,8) +test(4286578687, -3.4028235E38f, 32,24,8) +test(8388607, 1.1754942E-38f, 32,24,8) +test(-2139095041, -1.1754942E-38f, 32,24,8) +test(2155872255, -1.1754942E-38f, 32,24,8) +test(8388608, 1.17549435E-38f, 32,24,8) +test(12582912, 1.7632415E-38f, 32,24,8) +test(16777215, 2.3509886E-38f, 32,24,8) +test(0, 0d,64,53,11) +test(9223372036854775808, -0d, 64,53,11) +test(-9223372036854775808, -0d, 64,53,11) +test(4593671619917905920, 0.125d, 64,53,11) +test(4598175219545276416, 0.25d, 64,53,11) +test(4602678819172646912, 0.5d, 64,53,11) +test(4607182418800017408, 1d, 64,53,11) +test(4611686018427387904, 2d, 64,53,11) +test(4616189618054758400, 4d, 64,53,11) +test(4620693217682128896, 8d, 64,53,11) +test(4600427019358961664, 0.375d, 64,53,11) +test(4604930618986332160, 0.75d, 64,53,11) +test(4609434218613702656, 1.5d, 64,53,11) +test(4613937818241073152, 3d, 64,53,11) +test(4618441417868443648, 6d, 64,53,11) +test(4591870180174331904, 0.10000000149011612d, 64,53,11) +test(4596373779801702400, 0.20000000298023224d, 64,53,11) +test(4600877379429072896, 0.40000000596046448d, 64,53,11) +test(4605380979056443392, 0.80000001192092896d, 64,53,11) +test(4786511204606541824, 999999995904d, 64,53,11) +test(4965913770435018752, 1.0000000138484279e+24d, 64,53,11) +test(5145383438148173824, 9.9999996169031625e+35d, 64,53,11) +test(9218868437227405312, Infinityd, 64,53,11) +test(-4503599627370496, -Infinityd, 64,53,11) +test(18442240474082181120, -Infinityd, 64,53,11) +test(-4611686018427387904, -2d, 64,53,11) +test(13835058055282163712, -2d, 64,53,11) +test(4627730092099895296, 25d, 64,53,11) +test(5183643170565550134, 3.402823466E+38d, 64,53,11) +test(4039728865745034152, 1.17549435E-38d, 64,53,11) +test(4614256656748876136, 3.1415927410d, 64,53,11) +test(4599676419421066575, 0.333333333333333d, 64,53,11) +test(4623156123728347136, 12.375d, 64,53,11) +test(4634494146896484893, 68.123d, 64,53,11) +test(4503599627370496, 2.2250738585072014E-308d, 64,53,11) +test(9227875636482146304, -2.2250738585072014E-308d, 64,53,11) +test(-9218868437227405312, -2.2250738585072014E-308d, 64,53,11) +test(9007199254740991, 4.4501477170144023E-308d, 64,53,11) +test(9232379236109516799, -4.4501477170144023E-308d, 64,53,11) +test(-9214364837600034817, -4.4501477170144023E-308d, 64,53,11) +test(9227875636482146303, -2.225073858507201E-308d, 64,53,11) +test(-9218868437227405313, -2.225073858507201E-308d, 64,53,11) +test(9218868437227405311, 1.7976931348623157E308d, 64,53,11) +test(9214364837600034816, 8.98846567431158E307d, 64,53,11) +test(2251799813685248, 1.1125369292536007E-308d, 64,53,11) +test(9216616637413720064, 1.348269851146737E308d, 64,53,11) +sub(4623156123728347136, 4600427019358961664, 4622945017495814144, 64, 53, 11) +add(4623156123728347136, 4603804719079489536, 4623507967449235456, 64, 53, 11) +sub(1095106560, 1052770304, 1094713344, 32, 24, 8) +add(1095106560, 1059061760, 1095761920, 32, 24, 8) diff --git a/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint.out b/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint.out new file mode 100644 index 0000000000..34029394e4 --- /dev/null +++ b/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint.out @@ -0,0 +1 @@ + true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true .Tasks ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )