modified floating point syntax and modified floating point constants to use bitvector values

8 files changed, 57 insertions, 74 deletions

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 0c954f9a..d5a5efc9 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -695,10 +695,10 @@ namespace Microsoft.Boogie.AbstractInterpretation
           Lo = floor;

           Hi = ceiling;

         } else if (node.Val is BigFloat) {

-          BigInteger floor, ceiling;

+          BigNum floor, ceiling;

           ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling);

-          Lo = floor;

-          Hi = ceiling;

+          Lo = floor.ToBigInteger;

+          Hi = ceiling.ToBigInteger;

         } else if (node.Val is bool) {

           if ((bool)node.Val) {

             // true

diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index 8cde2cb9..a0ce03a5 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -129,7 +129,7 @@ namespace Microsoft.Basetypes
       this.exponentSize = exponentSize;

       this.exponent = exponent;

       this.significand = significand;

-      this.significandSize = significandSize;

+      this.significandSize = significandSize+1;

       this.isNeg = sign;

       this.value = "";

     }

@@ -141,33 +141,6 @@ namespace Microsoft.Basetypes
       this.significand = BigNum.ZERO;

       this.value = value;

       this.isNeg = value[0] == '-';

-      //Special cases:

-      if (this.value.Equals("+oo") || this.value.Equals("-oo") || this.value.Equals("-zero"))

-        return;

-      if (this.value.ToLower().Equals("nan")) {

-        this.value = "NaN";

-        return;

-      }

-      if (this.value.Equals("INF") || this.value.Equals("+INF"))

-      {

-        this.value = "+oo";

-        return;

-      }

-      if (this.value.Equals("-INF"))

-      {

-        this.value = "-oo";

-        return;

-      }

-      if (this.value.Equals("+zero"))

-      {

-        this.value = "0.0";

-        return;

-      }

-      //End special cases

-      if (this.value.IndexOf('.') == -1 && this.value.IndexOf('e') == -1)

-        this.value += ".0"; //Assures that the decimal value is a "real" number

-      if (this.value.IndexOf('.') == 0)

-        this.value = "0" + this.value; //Assures that decimals always have a 0 in front

     }

 

     private BigNum maxsignificand()

@@ -335,6 +308,18 @@ namespace Microsoft.Basetypes
       }

     }

 

+    public String ToBVString(){

+      if (this.IsSpecialType) {

+        return "_ " + this.value + " " + this.exponentSize + " " + this.significandSize;

+      }

+      else if (this.Value == "") {

+        return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + this.significandSize + ")";

+      }

+      else {

+        return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")";

+      }

+    }

+

     [Pure]

     public string ToDecimalString() {

       Contract.Ensures(Contract.Result<string>() != null);

@@ -430,7 +415,7 @@ namespace Microsoft.Basetypes
       get {

         if (value == "")

           return false;

-        return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("-zero"));

+        return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("zero") || value.Equals("-zero"));

       }

     }

 

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 2345cc1e..fa038803 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -90,7 +90,7 @@ namespace Microsoft.Boogie {
         }

       }

       ExecutionEngine.ProcessFiles(fileList);

-        return 0;

+          return 0;

 

     END:

       if (CommandLineOptions.Clo.XmlSink != null) {

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index ad537288..6b2e1201 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -561,7 +561,7 @@ namespace Microsoft.Boogie {
     {

       Contract.Requires(tok != null);

       Val = v;

-      Type = Type.GetFloatType(v.ExponentSize, v.MantissaSize);

+      Type = Type.GetFloatType(v.ExponentSize, v.SignificandSize);

       if (immutable)

         CachedHashCode = ComputeHashCode();

     }

@@ -639,7 +639,7 @@ namespace Microsoft.Boogie {
           return Type.Real;

         } else if (Val is BigFloat) {

           BigFloat temp = (BigFloat)Val;

-          return Type.GetFloatType(temp.ExponentSize, temp.MantissaSize);

+          return Type.GetFloatType(temp.ExponentSize, temp.SignificandSize);

         } else if (Val is BvConst) {

           return Type.GetBvType(((BvConst)Val).Bits);

         } else {

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index bf35ccbe..77100d1c 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -669,7 +669,7 @@ private class BvBounds : Expr {
   } else if (la.kind == 98) {

    Get();

    if (la.kind == 3) {

-    Expect(3);

+     Get();

     switch (Int32.Parse(t.val)) {

     case 16:

         ty = new FloatType(t, 5, 11);

@@ -689,13 +689,14 @@ private class BvBounds : Expr {
     }

    }

    else {

-    Expect(19);

+    Expect(19); //<

     Expect(3);

     int exp = Int32.Parse(t.val);

+    Expect(12); //,

     Expect(3);

     int man = Int32.Parse(t.val);

     ty = new FloatType(t, exp, man);

-    Expect(20);

+    Expect(20); //>

    }

   } else if (la.kind == 16) {

 			Get();

@@ -1909,32 +1910,39 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
    {

      if (la.kind == 97) {

        bool negative = false;

-       int exp, sig;

+       int exp, sig, size;

        BigNum exp_val, sig_val, value;

-       //Expected format = fp(sign exp_val sig_val) || fp<exp sig>(value)

-       Get(); //Skip the fp token

-       Get();

-       if (t.val == "(") {

+       //Expected format = float(sign exp_val sig_val) || float<exp sig>(value)

+       Get(); //Skip the float token

+       if (la.val == "(") {

          Get();

+         Expect(16); //bool

          negative = Boolean.Parse(t.val);

+         Expect(12); //,

          BvLit(out exp_val, out exp);

+         Expect(12);

          BvLit(out sig_val, out sig);

          n = new BigFloat(negative, exp_val, sig_val, exp, sig);

+         Expect(10); //)

        }

-       else if (t.val == "<") {

-         Expect(14);

+       else if (la.val == "<") {

+         Get();

+         Expect(3);

          exp = Int32.Parse(t.val);

-         Expect(14);

+         Expect(12);

+         Expect(3);

          sig = Int32.Parse(t.val);

-         int size;

-         BvLit(out value, out size);

-         if (size != exp + sig)

-         {

-           this.SemErr("The given bitvector size of " + size + "does not match the provided floating-point size of " + (exp + sig));

-           n = BigFloat.ZERO(8, 24);

-           return;

+         Expect(20); //>

+         Expect(9); //(

+         if (la.kind == 4) {

+           Get();

+           n = new BigFloat(t.val, exp, sig);

+         }

+         else {

+           BvLit(out value, out size);

+           n = new BigFloat(value.ToString(), exp, sig);

          }

-         n = new BigFloat(t.val, exp, sig);

+         Expect(10); //)

        }

        else {

          throw new FormatException();

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 59b6b7e7..96d5b290 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -204,17 +204,7 @@ namespace Microsoft.Boogie.SMTLib
       else if (node is VCExprFloatLit)

       {

         BigFloat lit = ((VCExprFloatLit)node).Val;

-        if (lit.IsSpecialType) {

-          wr.Write("(_ " + lit.Decimal + " " + lit.ExponentSize.ToString() + " " + lit.SignificandSize.ToString() + ")");

-          return true;

-        }

-        wr.Write("((_ to_fp " + lit.ExponentSize.ToString() + " " + lit.SignificandSize.ToString() + ") RNE ");

-        if (lit.IsNegative)

-          // In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")

-          wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString());

-        else

-          wr.Write(lit.ToDecimalString());

-        wr.Write(")");

+        wr.Write("(" + lit.ToBVString() + ")");

       }

       else {

         Contract.Assert(false);

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 3f6e3b7a..b22853ce 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -887,7 +887,7 @@ namespace Microsoft.Boogie.VCExprAST {
   {

     public readonly BigFloat Val;

     internal VCExprFloatLit(BigFloat val)

-      : base(Type.GetFloatType(val.ExponentSize, val.MantissaSize))

+      : base(Type.GetFloatType(val.ExponentSize, val.SignificandSize))

     {

       this.Val = val;

     }

diff --git a/float_test.bpl b/float_test.bpl
index fbf8e4e3..e893e098 100644
--- a/float_test.bpl
+++ b/float_test.bpl
@@ -1,13 +1,13 @@
 //Translation from addsub_double_exact.c
 //Should Verify
 procedure main() returns () {
-	var x : float(11 53);
-	var y : float(11 53);
-	var z : float(11 53);
-	var r : float(11 53);
-	x := fp(10000000 11 53);
-	y := x + fp(1 11 53);
-	z := x - fp(1 11 53);
+	var x : float<11, 53>;
+	var y : float<11, 53>;
+	var z : float<11, 53>;
+	var r : float<11, 53>;
+	x := fp<11, 53> (10000000bv64);
+	y := x + fp<11, 53>(1bv64);
+	z := x - fp<11, 53>(1bv64);
 	r := y - z;
-	assert r == fp(2 11 53);
+	assert r == fp<11, 53> (2bv64);
 }
\ No newline at end of file