Added several test cases and some basic documentation for fp usage

3 files changed, 48 insertions, 13 deletions

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index a27ae68d..0c954f9a 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -180,8 +180,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
             }

           }

           return e;

-        } else {

-          Contract.Assert(V.TypedIdent.Type.IsReal);

+        } else if (V.TypedIdent.Type.IsReal){

           Expr e = Expr.True;

           if (Lo != null && Hi != null && Lo == Hi) {

             // produce an equality

@@ -199,6 +198,30 @@ namespace Microsoft.Boogie.AbstractInterpretation
             }

           }

           return e;

+        } else {

+          Contract.Assert(V.TypedIdent.Type.IsFloat);

+          Expr e = Expr.True;

+          if (Lo != null && Hi != null && Lo == Hi)

+          {

+            // produce an equality

+            var ide = new IdentifierExpr(Token.NoToken, V);

+            e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type)));

+          }

+          else

+          {

+            // produce a (possibly empty) conjunction of inequalities

+            if (Lo != null)

+            {

+              var ide = new IdentifierExpr(Token.NoToken, V);

+              e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide));

+            }

+            if (Hi != null)

+            {

+              var ide = new IdentifierExpr(Token.NoToken, V);

+              e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type)));

+            }

+          }

+          return e;

         }

       }

     }

@@ -209,7 +232,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
       } else if (ty.IsReal) {

         return Expr.Literal(Basetypes.BigDec.FromBigInt(n));

       } else if (ty.IsFloat) {

-        return Expr.Literal(Basetypes.BigFloat.FromBigInt(n));

+        return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatMantissa));

       } else {

         Contract.Assume(ty.IsInt);

         return Expr.Literal(Basetypes.BigNum.FromBigInt(n));

diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index 6cf94feb..5b169263 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -92,16 +92,21 @@ namespace Microsoft.Basetypes
 

     [Pure]

     public static BigFloat FromInt(int v) {

-      return new BigFloat(v, 0, 24, 8);

+      return new BigFloat(v.ToString(), 8, 24);

     }

 

-    [Pure]

-    public static BigFloat FromLong(long v) {

-      return new BigFloat(0, v, 8, 24);

+    public static BigFloat FromInt(int v, int exponentSize, int mantissaSize)

+    {

+      return new BigFloat(v.ToString(), exponentSize, mantissaSize);

     }

 

     public static BigFloat FromBigInt(BIM v) {

-      return FromLong(Int64.Parse(v.ToString())); //Sketchy.  Hope this doesn't cause problems

+      return new BigFloat(v.ToString(), 8, 24);

+    }

+

+    public static BigFloat FromBigInt(BIM v, int exponentSize, int mantissaSize)

+    {

+      return new BigFloat(v.ToString(), exponentSize, mantissaSize);

     }

 

     public static BigFloat FromBigDec(BigDec v)

@@ -109,6 +114,11 @@ namespace Microsoft.Basetypes
       return new BigFloat(v.ToDecimalString(), 8, 24);

     }

 

+    public static BigFloat FromBigDec(BigDec v, int exponentSize, int mantissaSize)

+    {

+      return new BigFloat(v.ToDecimalString(), exponentSize, mantissaSize);

+    }

+

     [Pure]

     public static BigFloat FromString(string v) {

       String[] vals = v.Split(' ');

@@ -170,9 +180,9 @@ namespace Microsoft.Basetypes
         return;

       }

       //End special cases

-      if (this.dec_value.IndexOf(".") == -1)

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

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

-      if (this.dec_value.IndexOf(".") == 0)

+      if (this.dec_value.IndexOf('.') == 0)

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

     }

 

@@ -369,16 +379,18 @@ namespace Microsoft.Basetypes
 

     [Pure]

     public BigFloat Abs {

-      //TODO: fix for fp functionality

       get {

+        if (IsDec)

+          return dec_value[0] == '-' ? new BigFloat(dec_value.Remove(0, 1), ExponentSize, MantissaSize) : this;

         return new BigFloat(Exponent, Math.Abs(Mantissa), ExponentSize, MantissaSize);

       }

     }

 

     [Pure]

     public BigFloat Negate {

-      //TODO: Modify for correct fp functionality

       get {

+        if (IsDec)

+          return dec_value[0] == '-' ? new BigFloat(dec_value.Remove(0, 1), ExponentSize, MantissaSize) : new BigFloat("-" + dec_value, ExponentSize, MantissaSize);

         return new BigFloat(Exponent, -Mantissa, ExponentSize, MantissaSize);

       }

     }

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index cba74bc5..2345cc1e 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) {