K-buitin Floats do not provide any hooks to convert a specific bit pattern into a single precision or double precision floating point value.

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());

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

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)
 

k-distribution/tests/builtins/config.xml

@@ -14,4 +14,5 @@
           skip="pdf" >
     </test>
     <include file="mint/config.xml" directory="mint" skip="pdf" />
+    <include file="float/config.xml" directory="float" skip="pdf" />
 </tests>

k-distribution/tests/builtins/float/config.xml

@@ -0,0 +1,9 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!-- Copyright (c) 2016 K Team. All Rights Reserved. -->
+<tests>
+    <test definition="convertfloatmint/convertfloatmint-test.k"
+          extension="convertfloatmint"
+          programs="convertfloatmint"
+          results="convertfloatmint" >
+    </test>
+</tests>

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 <k>$PGM:Tasks</k>
+
+    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

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)

k-distribution/tests/builtins/float/convertfloatmint/test.convertfloatmint.out

@@ -0,0 +1 @@
+<k> true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( true  ( 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 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) </k>