Began adding the float type to VC expression

9 files changed, 148 insertions, 8 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index a8c82f08..9297bcbc 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1706,6 +1706,10 @@ namespace Microsoft.Boogie {
           if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {

             return Type.Real;

           }

+          if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float))

+          {

+            return Type.Float;

+          }

           goto BAD_TYPE;

         case Opcode.Div:

         case Opcode.Mod:

@@ -1757,6 +1761,10 @@ namespace Microsoft.Boogie {
           if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {

             return Type.Bool;

           }

+          if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float))

+          {

+            return Type.Bool;

+          }

           goto BAD_TYPE;

         case Opcode.And:

         case Opcode.Or:

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index f431c3d5..6accf79f 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -678,6 +678,12 @@ namespace Microsoft.Boogie.SMTLib
         return true;

       }

 

+      public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("/f", node, options);

+        return true;

+      }

+

       public bool VisitPowOp(VCExprNAry node, LineariserOptions options) {

         WriteApplication("real_pow", node, options);

         return true;

@@ -729,6 +735,12 @@ namespace Microsoft.Boogie.SMTLib
         return true;

       }

 

+      public bool VisitToFloatOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("to_float", node, options);

+        return true;

+      }

+

       private string ExtractDatatype(Function func) {

         if (func is DatatypeSelector) {

           DatatypeSelector selector = (DatatypeSelector) func;

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 8674f8c0..aa246c37 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -334,7 +334,10 @@ namespace Microsoft.Boogie.VCExprAST {
         return Gen.Integer(node.asBigNum);

       } else if (node.Val is BigDec) {

         return Gen.Real(node.asBigDec);

-      } else if (node.Val is BvConst) {

+      } else if (node.Val is BigFloat) {

+        return Gen.Float(node.asBigFloat);

+      }

+      else if (node.Val is BvConst) {

         return Gen.Bitvector((BvConst)node.Val);

       } else {

         System.Diagnostics.Debug.Assert(false, "unknown kind of literal " + node.tok.ToString());

@@ -1002,9 +1005,12 @@ namespace Microsoft.Boogie.VCExprAST {
         if (cce.NonNull(e.Type).IsInt) {

           return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e);

         }

-        else {

+        else if (cce.NonNull(e.Type).IsReal) {

           return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e);

         }

+        else  {//is float

+          return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO), e);

+        } 

       }

       else {

         return Gen.Not(this.args);

diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index e0a4b4c6..0ff6d67f 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -380,9 +380,14 @@ namespace Microsoft.Boogie.VCExprAST {
     internal const string realSubName = "realSub";

     internal const string realMulName = "realMul";

     internal const string realDivName = "realDiv";

+    internal const string floatAddName = "floatAdd";

+    internal const string floatSubName = "floatSub";

+    internal const string floatMulName = "floatMul";

+    internal const string floatDivName = "floatDiv";

     internal const string realPowName = "realPow";

     internal const string toIntName = "toIntCoercion";

     internal const string toRealName = "toRealCoercion";

+    internal const string toFloatName = "toFloatCoercion";

 

     internal void AssertAsTerm(string x, LineariserOptions options) {

       Contract.Requires(options != null);

@@ -943,9 +948,12 @@ namespace Microsoft.Boogie.VCExprAST {
             WriteTermApplication(intAddName, node, options);

           }

         }

-        else {

+        else if (node.Type.IsReal) {

           WriteTermApplication(realAddName, node, options);

         }

+        else {

+          WriteTermApplication(floatAddName, node, options);

+        }

         return true;

       }

 

@@ -955,9 +963,12 @@ namespace Microsoft.Boogie.VCExprAST {
         if (node.Type.IsInt) {

           WriteTermApplication(intSubName, node, options);

         }

-        else {

+        else if (node.Type.IsReal) {

           WriteTermApplication(realSubName, node, options);

         }

+        else {

+          WriteTermApplication(floatSubName, node, options);

+        }

         return true;

       }

 

@@ -967,9 +978,12 @@ namespace Microsoft.Boogie.VCExprAST {
         if (node.Type.IsInt) {

           WriteTermApplication(intMulName, node, options);

         }

-        else {

+        else if (node.Type.IsReal) {

           WriteTermApplication(realMulName, node, options);

         }

+        else {

+          WriteTermApplication(floatMulName, node, options);

+        }

         return true;

       }

 

@@ -994,6 +1008,14 @@ namespace Microsoft.Boogie.VCExprAST {
         return true;

       }

 

+      public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)

+      {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        WriteTermApplication(floatDivName, node, options);

+        return true;

+      }

+

       public bool VisitPowOp(VCExprNAry node, LineariserOptions options) {

         //Contract.Requires(options != null);

         //Contract.Requires(node != null);

@@ -1057,6 +1079,14 @@ namespace Microsoft.Boogie.VCExprAST {
         return true;

       }

 

+      public bool VisitToFloatOp(VCExprNAry node, LineariserOptions options)

+      {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        WriteApplication(toFloatName, node, options);

+        return true;

+      }

+

       public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) {

         //Contract.Requires(options != null);

         //Contract.Requires(node != null);

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 4f8dc08e..291d6d42 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -55,6 +55,13 @@ namespace Microsoft.Boogie {
       return new VCExprRealLit(x);

     }

 

+    public VCExpr/*!*/ Float(BigFloat x)

+    {

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

+

+      return new VCExprFloatLit(x);

+    }

+

     public VCExpr/*!*/ Function(VCExprOp/*!*/ op,

                             List<VCExpr/*!*/>/*!*/ arguments,

                             List<Type/*!*/>/*!*/ typeArguments) {

@@ -317,12 +324,16 @@ namespace Microsoft.Boogie {
 

     public static readonly VCExprOp AddIOp = new VCExprNAryOp(2, Type.Int);

     public static readonly VCExprOp AddROp = new VCExprNAryOp(2, Type.Real);

+    public static readonly VCExprOp AddFOp = new VCExprNAryOp(2, Type.Float);

     public static readonly VCExprOp SubIOp = new VCExprNAryOp(2, Type.Int);

     public static readonly VCExprOp SubROp = new VCExprNAryOp(2, Type.Real);

+    public static readonly VCExprOp SubFOp = new VCExprNAryOp(2, Type.Float);

     public static readonly VCExprOp MulIOp = new VCExprNAryOp(2, Type.Int);

     public static readonly VCExprOp MulROp = new VCExprNAryOp(2, Type.Real);

+    public static readonly VCExprOp MulFOp = new VCExprNAryOp(2, Type.Float);

     public static readonly VCExprOp DivIOp = new VCExprNAryOp(2, Type.Int);

     public static readonly VCExprOp DivROp = new VCExprNAryOp(2, Type.Real);

+    public static readonly VCExprOp DivFOp = new VCExprNAryOp(2, Type.Float);

     public static readonly VCExprOp ModOp = new VCExprNAryOp(2, Type.Int);

     public static readonly VCExprOp PowOp = new VCExprNAryOp(2, Type.Real);

     public static readonly VCExprOp LtOp = new VCExprNAryOp(2, Type.Bool);

@@ -336,6 +347,7 @@ namespace Microsoft.Boogie {
     public static readonly VCExprOp IfThenElseOp = new VCExprIfThenElseOp();

     public static readonly VCExprOp ToIntOp = new VCExprNAryOp(1, Type.Int);

     public static readonly VCExprOp ToRealOp = new VCExprNAryOp(1, Type.Real);

+    public static readonly VCExprOp ToFloatOp = new VCExprNAryOp(1, Type.Float);

 

     public static readonly VCExprOp TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool);

 

@@ -391,6 +403,7 @@ namespace Microsoft.Boogie {
       DivOp,

       ModOp,

       RealDivOp,

+      FloatDivOp,

       PowOp,

       LtOp,

       LeOp,

@@ -400,7 +413,8 @@ namespace Microsoft.Boogie {
       Subtype3Op,

       BvConcatOp,

       ToIntOp,

-      ToRealOp

+      ToRealOp,

+      ToFloatOp

     };

     internal static Dictionary<VCExprOp/*!*/, SingletonOp>/*!*/ SingletonOpDict;

     [ContractInvariantMethod]

@@ -425,6 +439,7 @@ namespace Microsoft.Boogie {
       SingletonOpDict.Add(MulROp, SingletonOp.MulOp);

       SingletonOpDict.Add(DivIOp, SingletonOp.DivOp);

       SingletonOpDict.Add(DivROp, SingletonOp.RealDivOp);

+      SingletonOpDict.Add(DivFOp, SingletonOp.FloatDivOp);

       SingletonOpDict.Add(ModOp, SingletonOp.ModOp);

       SingletonOpDict.Add(PowOp, SingletonOp.PowOp);

       SingletonOpDict.Add(LtOp, SingletonOp.LtOp);

@@ -435,6 +450,7 @@ namespace Microsoft.Boogie {
       SingletonOpDict.Add(Subtype3Op, SingletonOp.Subtype3Op);

       SingletonOpDict.Add(ToIntOp, SingletonOp.ToIntOp);

       SingletonOpDict.Add(ToRealOp, SingletonOp.ToRealOp);

+      SingletonOpDict.Add(ToFloatOp, SingletonOp.ToFloatOp);

     }

 

     ////////////////////////////////////////////////////////////////////////////////

@@ -856,6 +872,31 @@ namespace Microsoft.Boogie.VCExprAST {
     }

   }

 

+  public class VCExprFloatLit : VCExprLiteral

+  {

+    public readonly BigFloat Val;

+    internal VCExprFloatLit(BigFloat val)

+      : base(Type.Float)

+    {

+      this.Val = val;

+    }

+    [Pure]

+    [Reads(ReadsAttribute.Reads.Nothing)]

+    public override bool Equals(object that)

+    {

+      if (Object.ReferenceEquals(this, that))

+        return true;

+      if (that is VCExprFloatLit)

+        return Val == ((VCExprFloatLit)that).Val;

+      return false;

+    }

+    [Pure]

+    public override int GetHashCode()

+    {

+      return Val.GetHashCode() * 72321;

+    }

+  }

+

   /////////////////////////////////////////////////////////////////////////////////

   // Operator expressions with fixed arity

   [ContractClassFor(typeof(VCExprNAry))]

@@ -1265,6 +1306,8 @@ namespace Microsoft.Boogie.VCExprAST {
             return visitor.VisitModOp(expr, arg);

           case VCExpressionGenerator.SingletonOp.RealDivOp:

             return visitor.VisitRealDivOp(expr, arg);

+          case VCExpressionGenerator.SingletonOp.FloatDivOp:

+            return visitor.VisitFloatDivOp(expr, arg);

           case VCExpressionGenerator.SingletonOp.PowOp:

             return visitor.VisitPowOp(expr, arg);

           case VCExpressionGenerator.SingletonOp.LtOp:

diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs
index 00e6fb9c..8b79b0e5 100644
--- a/Source/VCExpr/VCExprASTPrinter.cs
+++ b/Source/VCExpr/VCExprASTPrinter.cs
@@ -302,6 +302,12 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);

       return PrintNAry("/", node, wr);

     }

+    public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr)

+    {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      return PrintNAry("/f", node, wr);

+    }

     public bool VisitPowOp(VCExprNAry node, TextWriter wr) {

       //Contract.Requires(wr != null);

       //Contract.Requires(node != null);

@@ -347,6 +353,12 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);

       return PrintNAry("real", node, wr);

     }

+    public bool VisitToFloatOp(VCExprNAry node, TextWriter wr)

+    {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      return PrintNAry("float", node, wr);

+    }

     public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {

       //Contract.Requires(wr != null);

       //Contract.Requires(node != null);

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index ad0c270d..1bcce113 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -77,6 +77,7 @@ namespace Microsoft.Boogie.VCExprAST {
     Result VisitDivOp(VCExprNAry node, Arg arg);

     Result VisitModOp(VCExprNAry node, Arg arg);

     Result VisitRealDivOp(VCExprNAry node, Arg arg);

+    Result VisitFloatDivOp(VCExprNAry node, Arg arg); //TODO: Add this to references from above and below

     Result VisitPowOp(VCExprNAry node, Arg arg);

     Result VisitLtOp(VCExprNAry node, Arg arg);

     Result VisitLeOp(VCExprNAry node, Arg arg);

@@ -189,6 +190,12 @@ namespace Microsoft.Boogie.VCExprAST {
       throw new NotImplementedException();

     }

 

+    public Result VisitFloatDivOp(VCExprNAry node, Arg arg)

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

     public Result VisitPowOp(VCExprNAry node, Arg arg) {

       Contract.Requires(node != null);

       throw new NotImplementedException();

@@ -234,6 +241,12 @@ namespace Microsoft.Boogie.VCExprAST {
       throw new NotImplementedException();

     }

 

+    public Result VisitToFloat(VCExprNAry node, Arg arg) //TODO: modify later

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

     public Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {

       Contract.Requires(node != null);

       throw new NotImplementedException();

@@ -1482,6 +1495,11 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);

       return StandardResult(node, arg);

     }

+    public virtual Result VisitFloatDivOp(VCExprNAry node, Arg arg)

+    {

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

     public virtual Result VisitPowOp(VCExprNAry node, Arg arg) {

       //Contract.Requires(node != null);

       return StandardResult(node, arg);

@@ -1518,6 +1536,11 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);

       return StandardResult(node, arg);

     }

+    public virtual Result VisitToFloatOp(VCExprNAry node, Arg arg)

+    {

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

     public virtual Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {

       //Contract.Requires(node != null);

       return StandardResult(node, arg);

diff --git a/Test/test1/IntReal.bpl.expect b/Test/test1/IntReal.bpl.expect
index 021a8389..b532d22a 100644
--- a/Test/test1/IntReal.bpl.expect
+++ b/Test/test1/IntReal.bpl.expect
@@ -12,8 +12,8 @@ IntReal.bpl(19,12): Error: invalid argument types (real and int) to binary opera
 IntReal.bpl(25,8): Error: invalid argument types (int and real) to binary operator **
 IntReal.bpl(29,14): Error: invalid argument types (real and int) to binary operator ==
 IntReal.bpl(31,13): Error: invalid argument types (int and real) to binary operator ==
-IntReal.bpl(34,6): Error: argument type int does not match expected type real
-IntReal.bpl(35,6): Error: argument type real does not match expected type int
+IntReal.bpl(34,6): Error: argument type int does not match expected type real or type float
+IntReal.bpl(35,6): Error: argument type real does not match expected type int or type float
 IntReal.bpl(47,8): Error: invalid argument types (real and int) to binary operator div
 IntReal.bpl(48,8): Error: invalid argument types (real and int) to binary operator mod
 18 type checking errors detected in IntReal.bpl
diff --git a/float_test3.bpl b/float_test3.bpl
new file mode 100644
index 00000000..cd0ea59e
--- /dev/null
+++ b/float_test3.bpl
@@ -0,0 +1,6 @@
+ procedure F() returns () {
+	var x : float;
+	var y : float;
+	y := x - x;
+	assert y != x;
+}
\ No newline at end of file