Added initial support for float addition

9 files changed, 89 insertions, 37 deletions

diff --git a/Binaries/Boogie.vshost.exe.manifest b/Binaries/Boogie.vshost.exe.manifest
index 061c9ca9..f96b1d6b 100644
--- a/Binaries/Boogie.vshost.exe.manifest
+++ b/Binaries/Boogie.vshost.exe.manifest
@@ -1,11 +1,11 @@
-<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
-<assembly xmlns="urn:schemas-microsoft-com:asm.v1" manifestVersion="1.0">
-  <assemblyIdentity version="1.0.0.0" name="MyApplication.app"/>
-  <trustInfo xmlns="urn:schemas-microsoft-com:asm.v2">
-    <security>
-      <requestedPrivileges xmlns="urn:schemas-microsoft-com:asm.v3">
-        <requestedExecutionLevel level="asInvoker" uiAccess="false"/>
-      </requestedPrivileges>
-    </security>
-  </trustInfo>
-</assembly>
+<?xml version="1.0" encoding="UTF-8" standalone="yes"?>

+<assembly xmlns="urn:schemas-microsoft-com:asm.v1" manifestVersion="1.0">

+  <assemblyIdentity version="1.0.0.0" name="MyApplication.app"/>

+  <trustInfo xmlns="urn:schemas-microsoft-com:asm.v2">

+    <security>

+      <requestedPrivileges xmlns="urn:schemas-microsoft-com:asm.v3">

+        <requestedExecutionLevel level="asInvoker" uiAccess="false"/>

+      </requestedPrivileges>

+    </security>

+  </trustInfo>

+</assembly>

diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index 1fb05005..33860a4f 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -17,7 +17,7 @@ namespace Microsoft.Basetypes
     
   /// <summary>
   /// A representation of a 32-bit floating point value
-  /// Note that this value has a 1-bit sign, 8-bit exponent, and 23-bit mantissa
+  /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit mantissa
   /// </summary>
   public struct BigFloat
   {
@@ -85,17 +85,17 @@ namespace Microsoft.Basetypes
 
     [Pure]
     public static BigFloat FromInt(int v) {
-      return new BigFloat(v, 0, 23, 8); //TODO: modify for correct fp representation
+      return new BigFloat(v, 0, 24, 8); //TODO: modify for correct fp representation
     }
 
     [Pure]
     public static BigFloat FromBigInt(BIM v) {
-      return new BigFloat(0, v, 8, 23); //TODO: modify for correct fp representation
+      return new BigFloat(0, v, 8, 24); //TODO: modify for correct fp representation
     }
 
     public static BigFloat FromBigDec(BIM v)
     {
-      return new BigFloat(0, v, 8, 23); //TODO: modify for correct fp representation
+      return new BigFloat(0, v, 8, 24); //TODO: modify for correct fp representation
     }
 
     [Pure]
@@ -107,9 +107,9 @@ namespace Microsoft.Basetypes
       {
         switch (vals.Length) {
           case 1:
-            return Round(vals[0], 8, 23); 
+            return Round(vals[0], 8, 24); 
           case 2:
-            return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 23);
+            return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 24);
           case 3:
             return Round(vals[0], Int32.Parse(vals[1]), Int32.Parse(vals[2]));
           case 4:
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 7e7ed10a..181076a7 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1519,8 +1519,6 @@ namespace Microsoft.Boogie {
             return "mod";

           case Opcode.RealDiv:

             return "/";

-          case Opcode.FloatDiv:

-            return "/";

           case Opcode.Pow:

             return "**";

           case Opcode.Eq:

@@ -1583,10 +1581,6 @@ namespace Microsoft.Boogie {
           opBindingStrength = 0x50;

           fragileRightContext = true;

           break;

-        case Opcode.FloatDiv: //TODO: Modify (potentially)

-          opBindingStrength = 0x50;

-          fragileRightContext = true;

-          break;

         case Opcode.Pow:

           opBindingStrength = 0x60;

           fragileRightContext = true;

@@ -1707,10 +1701,12 @@ 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;

-          //}

+          if (arg0type.IsFloat && arg0type.Unify(arg1type)) {

+            return new FloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa);

+          }

+          if (arg1type.IsFloat && arg1type.Unify(arg0type)) {

+            return new FloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa);

+          }

           goto BAD_TYPE;

         case Opcode.Div:

         case Opcode.Mod:

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 2550c334..889d7be8 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -678,7 +678,7 @@ private class BvBounds : Expr {
      Expect(10);

    }

    else

-    ty = new FloatType(t, 8, 23);

+    ty = new FloatType(t, 8, 24);

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

 			Get();

 			ty = new BasicType(t, SimpleType.Bool); 

@@ -1914,7 +1914,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
    catch (FormatException)

    {

      this.SemErr("incorrectly formatted floating point");

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

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

    }

  }

 

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 4a1331c5..4982d81e 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -93,6 +93,7 @@ namespace Microsoft.Boogie.SMTLib
         log = log.Replace("\r", "").Replace("\n", " ");

         Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);

       }

+      Console.WriteLine(cmd);

       toProver.WriteLine(cmd);

     }

 

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 250e04c9..8e8b2d55 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -253,7 +253,7 @@ namespace Microsoft.Boogie.SMTLib
             //if (options.Inspector != null)

             //  options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");

 

-            options.AddWeakSmtOption("TYPE_CHECK", "true");

+            options.AddWeakSmtOption("TYPE_CHECK", "false");

             options.AddWeakSmtOption("smt.BV.REFLECT", "true");

 

             if (options.TimeLimit > 0)

@@ -334,7 +334,7 @@ namespace Microsoft.Boogie.SMTLib
             //if (options.Inspector != null)

             //  options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");

 

-            options.AddWeakSmtOption("TYPE_CHECK", "true");

+            options.AddWeakSmtOption("TYPE_CHECK", "false");

             options.AddWeakSmtOption("BV_REFLECT", "true");

 

             if (options.TimeLimit > 0)

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 36692f30..c44800fc 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -357,6 +357,15 @@ namespace Microsoft.Boogie {
       return new VCExprBoogieFunctionOp(func);

     }

 

+    // Float nodes

+

+    public VCExpr AddFOp(VCExpr f1, VCExpr f2)

+    {

+      Contract.Requires(f1 != null);

+      Contract.Requires(f2 != null);

+      return Function(new VCExprFloatOp(f1.Type.FloatExponent, f1.Type.FloatMantissa));

+    }

+

     // Bitvector nodes

 

     public VCExpr Bitvector(BvConst bv) {

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

       ModOp,

       RealDivOp,

-      FloatDivOp,

       PowOp,

       LtOp,

       LeOp,

@@ -1309,8 +1317,6 @@ 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:

@@ -1669,6 +1675,56 @@ namespace Microsoft.Boogie.VCExprAST {
   }

 

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

+  // Float operators

+

+  public class VCExprFloatOp : VCExprOp {

+    public readonly int Mantissa;

+    public readonly int Exponent;

+

+    public override int Arity {

+      get {

+        return 1;

+      }

+    }

+    public override int TypeParamArity {

+      get {

+        return 0;

+      }

+    }

+    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {

+      //Contract.Requires(cce.NonNullElements(typeArgs));

+      //Contract.Requires(cce.NonNullElements(args));

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

+      return Type.GetFloatType(Exponent, Mantissa);

+    }

+

+    [Pure]

+    [Reads(ReadsAttribute.Reads.Nothing)]

+    public override bool Equals(object that) {

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

+        return true;

+      if (that is VCExprFloatOp)

+        return this.Exponent == ((VCExprFloatOp)that).Exponent && this.Mantissa == ((VCExprFloatOp)that).Mantissa;

+      return false;

+    }

+    [Pure]

+    public override int GetHashCode() {

+      return Exponent * 81748912 + Mantissa * 67867979;

+    }

+

+    internal VCExprFloatOp(int exp, int man) {

+      this.Exponent = exp;

+      this.Mantissa = man;

+    }

+    public override Result Accept<Result, Arg>

+           (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {

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

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

+      return visitor.VisitBvOp(expr, arg);

+    }

+  }

+

+  /////////////////////////////////////////////////////////////////////////////////

   // Bitvector operators

 

   public class VCExprBvOp : VCExprOp {

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 1bcce113..a1fb2ff4 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -77,7 +77,6 @@ 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);

diff --git a/float_test5.bpl b/float_test5.bpl
index 2f565b27..c3d279f2 100644
--- a/float_test5.bpl
+++ b/float_test5.bpl
@@ -1,5 +1,5 @@
  procedure F() returns () {
 	var x : float;
-	x := fp (0 0);
-	assert x == fp (0 0 8 30);
+	var y : float;
+	assert x + y == fp(0);
 }
\ No newline at end of file