Fixed bug in abstract interpretation over reals

4 files changed, 34 insertions, 4 deletions

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 4b5ae903..640a50fc 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -166,16 +166,16 @@ namespace Microsoft.Boogie.AbstractInterpretation
           if (Lo != null && Hi != null && Lo + 1 == Hi) {

             // produce an equality

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

-            e = Expr.And(e, BplEq(ide, Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Lo))));

+            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(Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Lo)), ide));

+              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, BplLt(ide, Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Hi))));

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

             }

           }

           return e;

@@ -183,6 +183,17 @@ namespace Microsoft.Boogie.AbstractInterpretation
       }

     }

 

+    static Expr NumberToExpr(BigInteger n, Type ty) {

+      if (n == null) {

+        return null;

+      } else if (ty.IsReal) {

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

+      } else {

+        Contract.Assume(ty.IsInt);

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

+      }

+    }

+

     List<BigInteger> upThresholds;  // invariant: thresholds are sorted

     List<BigInteger> downThresholds;  // invariant: thresholds are sorted

 

diff --git a/Source/Basetypes/BigDec.cs b/Source/Basetypes/BigDec.cs
index 301774f6..beb9ec54 100644
--- a/Source/Basetypes/BigDec.cs
+++ b/Source/Basetypes/BigDec.cs
@@ -48,6 +48,11 @@ namespace Microsoft.Basetypes {
     }

 

     [Pure]

+    public static BigDec FromBigInt(BIM v) {

+      return new BigDec(v, 0);

+    }

+

+    [Pure]

     public static BigDec FromString(string v) {

       if (v == null) throw new FormatException();

 

diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index 961b3c33..cc518d1b 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -165,4 +165,4 @@ Execution trace:
     Intervals.bpl(301,3): anon3_LoopHead

     Intervals.bpl(301,3): anon3_LoopDone

 

-Boogie program verifier finished with 15 verified, 11 errors

+Boogie program verifier finished with 16 verified, 11 errors

diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
index 6a588bbe..c769645f 100644
--- a/Test/aitest0/Intervals.bpl
+++ b/Test/aitest0/Intervals.bpl
@@ -316,3 +316,17 @@ procedure Id17(n: int)
   assert 0 <= i;  // fine: SometimesId2 claims to be an identity and the use of it is int->int

 }

 

+// real numbers

+

+procedure W0(N: real)

+{

+  var i, bf0: real;

+  i := 0.0;

+  while (i < N) {

+    bf0 := N - i;

+    i := i + 1.0;

+    // check termination:

+    assert 0.0 <= bf0;

+    assert N - i <= bf0 - 1.0;

+  }

+}