Add opaque types for Double and Float

Author: mario-bucev

frontends/benchmarks/verification/valid/FPFledging.scala

@@ -0,0 +1,21 @@
+import stainless.math._
+
+object FPFledging {
+  def test1(x: Double): Unit = {
+    assert(Double.longBitsToDouble(Double.doubleToRawLongBits(x)) == x)
+  }
+
+  def test2(x: Long): Unit = {
+    Double.longBitsToDoublePost(x)
+    assert(Double.doubleToRawLongBits(Double.longBitsToDouble(x)) == x)
+  }
+
+  def test3(x: Float): Unit = {
+    assert(Float.intBitsToFloat(Float.floatToRawIntBits(x)) == x)
+  }
+
+  def test4(x: Int): Unit = {
+    Float.intBitsToFloatPost(x)
+    assert(Float.floatToRawIntBits(Float.intBitsToFloat(x)) == x)
+  }
+}

frontends/library/stainless/math/Double.scala

@@ -0,0 +1,26 @@
+package stainless
+package math
+
+import lang.StaticChecks._
+import annotation._
+
+@library
+case class Double(@extern @pure private val value: scala.Double) extends AnyVal
+
+@library
+object Double {
+  @extern @pure
+  def longBitsToDouble(l: Long): Double = {
+    Double(java.lang.Double.longBitsToDouble(l))
+  }
+
+  @extern @pure
+  def longBitsToDoublePost(l: Long): Unit = {
+    ()
+  } ensuring (_ => doubleToRawLongBits(longBitsToDouble(l)) == l)
+
+  @extern @pure
+  def doubleToRawLongBits(d: Double): Long = {
+    java.lang.Double.doubleToRawLongBits(d.value)
+  } ensuring (res => longBitsToDouble(res) == d)
+}

frontends/library/stainless/math/Float.scala

@@ -0,0 +1,26 @@
+package stainless
+package math
+
+import lang.StaticChecks._
+import annotation._
+
+@library
+case class Float(@extern @pure private val value: scala.Float) extends AnyVal
+
+@library
+object Float {
+  @extern @pure
+  def intBitsToFloat(i: Int): Float = {
+    Float(java.lang.Float.intBitsToFloat(i))
+  }
+
+  @extern @pure
+  def intBitsToFloatPost(i: Int): Unit = {
+    ()
+  } ensuring (_ => floatToRawIntBits(intBitsToFloat(i)) == i)
+
+  @extern @pure
+  def floatToRawIntBits(d: Float): Int = {
+    java.lang.Float.floatToRawIntBits(d.value)
+  } ensuring (res => intBitsToFloat(res) == d)
+}