From 823230fa46ac31fe5565c81e644ebc18c8b2aa6a Mon Sep 17 00:00:00 2001 From: Sandeep Dasgupta Date: Sat, 9 Dec 2017 18:12:19 -0600 Subject: [PATCH 1/7] K-buitin Floats do not provide any hooks to convert a specific bit pattern into a single precision or double precision floating point value. Requirement: We need the ability to do the conversion as shown in examples: Example 1: bit-vector: 32' 01000001 01000110 00000000 00000000 === MInt(32, 1095106560) convert to or from Float(single precision): 12.375f. Example 2: bit-vector: 64' 0b0100000000101000110000000000000000000000000000000000000000000000 === MInt(64, 4623156123728347136) convert to or from Float(single precision): 12.375d. Commit: Provides two following two hooks: 1. float2mint(Float F, Int W): Converts a float point value F(single or double precision) to a BitVector or MInt of bitwidth W. 2. mint2float(MInt MI, Int Precision, Int Exponent): Converts a Bitvector or MInt to an single or double precision float point value. The hooks are tested extensively using corner cases. Note: The available hooks like float2Int or int2Float converts between the float and its integer equivalent and hence not suitable. From example 2, int2Float(4623156123728347136) gives 4.623156123728347136 e+18 Some peculiarities of exiting mpfr library support: 1. While creating the BigFloat using BigFLoat constrcutor, we need to pass the unbiased exponent (mint(e1...e8) - 127) as the callee expects that. This is more evident from https://github.com/kframework/mpfr-java/blob/a24d33c7589e285e840eaaba74368581dc15ebb3/src/main/java/org/kframework/mpfr/BigFloat.java#L357 where exponent is compared with mc.minExponent(-126) and mc.MaxExponent(+127). 2. For zero, BigFloat constructor expects -127 as opposed to -126 (a special exponent used for +/- zero). Inside the constructor, its converted back to 126. This is used to easily distinguish =/- zero and sub normals value from others. https://github.com/kframework/mpfr-java/blob/a24d33c7589e285e840eaaba74368581dc15ebb3/src/main/java/org/kframework/mpfr/BigFloat.java#L364 --- .../java/builtins/BuiltinFloatOperations.java | 142 +++++++++++++++++- .../backend/java/symbolic/hooks.properties | 2 + k-distribution/include/builtin/domains.k | 3 + k-distribution/tests/builtins/config.xml | 1 + .../tests/builtins/float/config.xml | 9 ++ .../convertfloatmint/convertfloatmint-test.k | 21 +++ .../convertfloatmint/test.convertfloatmint | 100 ++++++++++++ .../test.convertfloatmint.out | 1 + 8 files changed, 278 insertions(+), 1 deletion(-) create mode 100644 k-distribution/tests/builtins/float/config.xml create mode 100644 k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k create mode 100644 k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint create mode 100644 k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint.out 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..0406bfcb0a 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. @@ -223,7 +224,7 @@ public static FloatToken int2float(IntToken term, IntToken precision, IntToken e } /** - * Rounds {@code term} to an integer by truncating it. Function is only + * Converts {@code term} to an integer by truncating it. Function is only * defined on ordinary numbers (i.e. not NaN or infinity). */ public static IntToken float2int(FloatToken term, TermContext context) { @@ -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..1d32c2109f --- /dev/null +++ b/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k @@ -0,0 +1,21 @@ +requires "domains.k" + +module CONVERTFLOATMINT-TEST-SYNTAX + imports MINT + imports FLOAT + + syntax Task ::= "test" "(" Int "," Float "," 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)) +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..e42bba3c21 --- /dev/null +++ b/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint @@ -0,0 +1,100 @@ +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(2143289344, NaNf, 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(18442240474082181121, NaNd, 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) 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..af4fb326ba --- /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 ( false ( 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 ( false ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true .Tasks ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) From 66ae1a4fa7c6320a40d05c078c985dd82c98a164 Mon Sep 17 00:00:00 2001 From: Sandeep Dasgupta Date: Sat, 9 Dec 2017 18:57:23 -0600 Subject: [PATCH 2/7] added few more tests --- .../float/convertfloatmint/convertfloatmint-test.k | 8 ++++++++ .../builtins/float/convertfloatmint/test.convertfloatmint | 4 ++++ 2 files changed, 12 insertions(+) diff --git a/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k b/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k index 1d32c2109f..298f759da8 100644 --- a/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k +++ b/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k @@ -5,6 +5,8 @@ module CONVERTFLOATMINT-TEST-SYNTAX 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 @@ -18,4 +20,10 @@ module CONVERTFLOATMINT-TEST 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 index e42bba3c21..204a892901 100644 --- a/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint +++ b/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint @@ -98,3 +98,7 @@ 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) From 15d4351c02dade5e16d429d845357005366ba9d9 Mon Sep 17 00:00:00 2001 From: Sandeep Dasgupta Date: Sat, 9 Dec 2017 18:59:56 -0600 Subject: [PATCH 3/7] Added GOlden Output: added few more tests --- .../builtins/float/convertfloatmint/test.convertfloatmint.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint.out b/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint.out index af4fb326ba..1607c1bf18 100644 --- a/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint.out +++ b/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint.out @@ -1 +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 ( false ( 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 ( false ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true ( true .Tasks ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + 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 ( false ( 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 ( false ( 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 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) From 0cea51447cc3113c5b2e95e5af00e90f5caa3c4e Mon Sep 17 00:00:00 2001 From: Sandeep Dasgupta Date: Wed, 13 Dec 2017 10:44:09 -0600 Subject: [PATCH 4/7] Fixed the erorrs caught by maven-checkstyle-plugin --- .../convertfloatmint/convertfloatmint-test.k | 17 +++++------------ 1 file changed, 5 insertions(+), 12 deletions(-) diff --git a/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k b/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k index 298f759da8..24f188f899 100644 --- a/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k +++ b/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k @@ -1,3 +1,4 @@ +// Copyright (c) 2016 K Team. All Rights Reserved. requires "domains.k" module CONVERTFLOATMINT-TEST-SYNTAX @@ -5,9 +6,7 @@ module CONVERTFLOATMINT-TEST-SYNTAX 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, ""} + syntax Tasks ::= List{Task, ""} endmodule module CONVERTFLOATMINT-TEST @@ -16,14 +15,8 @@ module CONVERTFLOATMINT-TEST 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 + 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 From b3abe11584de509ceb345f860e4c1b5fe50e2e24 Mon Sep 17 00:00:00 2001 From: Sandeep Dasgupta Date: Wed, 13 Dec 2017 12:09:21 -0600 Subject: [PATCH 5/7] reverted the code misstaken ly ommitted from testcase --- .../backend/java/builtins/BuiltinFloatOperations.java | 2 +- .../float/convertfloatmint/convertfloatmint-test.k | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) 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 0406bfcb0a..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 @@ -224,7 +224,7 @@ public static FloatToken int2float(IntToken term, IntToken precision, IntToken e } /** - * Converts {@code term} to an integer by truncating it. Function is only + * Rounds {@code term} to an integer by truncating it. Function is only * defined on ordinary numbers (i.e. not NaN or infinity). */ public static IntToken float2int(FloatToken term, TermContext context) { diff --git a/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k b/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k index 24f188f899..9e8e025628 100644 --- a/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k +++ b/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k @@ -6,6 +6,8 @@ module CONVERTFLOATMINT-TEST-SYNTAX 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 @@ -19,4 +21,10 @@ module CONVERTFLOATMINT-TEST 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 From ccd951a119cf0f3518df04af5f5c5ac32adb87be Mon Sep 17 00:00:00 2001 From: Sandeep Dasgupta Date: Wed, 13 Dec 2017 12:15:20 -0600 Subject: [PATCH 6/7] fixed some more styling isues --- .../builtins/float/convertfloatmint/convertfloatmint-test.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k b/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k index 9e8e025628..41a5c8ed5c 100644 --- a/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k +++ b/k-distribution/tests/builtins/float/convertfloatmint/convertfloatmint-test.k @@ -21,7 +21,7 @@ module CONVERTFLOATMINT-TEST 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)) From 346b7a0b5d1ab4b3b64b551b823daf9751c66f20 Mon Sep 17 00:00:00 2001 From: Sandeep Dasgupta Date: Wed, 13 Dec 2017 14:20:37 -0600 Subject: [PATCH 7/7] remove the tets case which craete a MINT out of NAN; the expected bahaviour is to warn with an exception thrown, but the mvn -e clean verify make the wanr an error --- .../tests/builtins/float/convertfloatmint/test.convertfloatmint | 2 -- .../builtins/float/convertfloatmint/test.convertfloatmint.out | 2 +- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint b/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint index 204a892901..e935344802 100644 --- a/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint +++ b/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint @@ -23,7 +23,6 @@ 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(2143289344, NaNf, 32,24,8) test(-1073741824, -2f, 32,24,8) test(3221225472, -2f, 32,24,8) test(1103626240, 25f, 32,24,8) @@ -76,7 +75,6 @@ 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(18442240474082181121, NaNd, 64,53,11) test(-4611686018427387904, -2d, 64,53,11) test(13835058055282163712, -2d, 64,53,11) test(4627730092099895296, 25d, 64,53,11) diff --git a/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint.out b/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint.out index 1607c1bf18..34029394e4 100644 --- a/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint.out +++ b/k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint.out @@ -1 +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 ( false ( 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 ( false ( 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 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + 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 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )