When guessing decreases clauses for loops, convert numeric values to their ultimate base type (int or real) before subtracting

5 files changed, 128 insertions, 16 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index c328f7b7..b3994f40 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -604,7 +604,7 @@ namespace Microsoft.Dafny {
       return "int";

     }

     public override bool Equals(Type that) {

-      return that.NormalizeExpand() is IntType;

+      return that.IsIntegerType;

     }

   }

 

@@ -622,7 +622,7 @@ namespace Microsoft.Dafny {
       return "real";

     }

     public override bool Equals(Type that) {

-      return that.NormalizeExpand() is RealType;

+      return that.IsRealType;

     }

   }

 

@@ -4745,7 +4745,7 @@ namespace Microsoft.Dafny {
     public static Expression CreateAdd(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      Contract.Requires((e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType) || (e0.Type.NormalizeExpand() is RealType && e1.Type.NormalizeExpand() is RealType));

+      Contract.Requires((e0.Type.IsIntegerType && e1.Type.IsIntegerType) || (e0.Type.IsRealType && e1.Type.IsRealType));

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

       var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Add, e0, e1);

       s.ResolvedOp = BinaryExpr.ResolvedOpcode.Add;  // resolve here

@@ -4754,15 +4754,33 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

-    /// Create a resolved expression of the form "e0 - e1"

+    /// Create a resolved expression of the form "CVT(e0) - CVT(e1)", where "CVT" is either "int" (if

+    /// e0.Type is an integer-based numeric type) or "real" (if e0.Type is a real-based numeric type).

     /// </summary>

-    public static Expression CreateSubtract(Expression e0, Expression e1) {

+    public static Expression CreateSubtract_TypeConvert(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

       Contract.Requires(

         (e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int)) ||

         (e0.Type.IsNumericBased(Type.NumericPersuation.Real) && e1.Type.IsNumericBased(Type.NumericPersuation.Real)));

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

+

+      Type toType = e0.Type.IsNumericBased(Type.NumericPersuation.Int) ? (Type)Type.Int : Type.Real;

+      e0 = new ConversionExpr(e0.tok, e0, toType);

+      e0.Type = toType;

+      e1 = new ConversionExpr(e1.tok, e1, toType);

+      e1.Type = toType;

+      return CreateSubtract(e0, e1);

+    }

+

+    /// <summary>

+    /// Create a resolved expression of the form "e0 - e1"

+    /// </summary>

+    public static Expression CreateSubtract(Expression e0, Expression e1) {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Requires((e0.Type.IsIntegerType && e1.Type.IsIntegerType) || (e0.Type.IsRealType && e1.Type.IsRealType));

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

       var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Sub, e0, e1);

       s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;  // resolve here

       s.Type = e0.Type;  // resolve here

@@ -4774,7 +4792,7 @@ namespace Microsoft.Dafny {
     /// </summary>

     public static Expression CreateIncrement(Expression e, int n) {

       Contract.Requires(e != null);

-      Contract.Requires(e.Type.NormalizeExpand() is IntType);

+      Contract.Requires(e.Type.IsIntegerType);

       Contract.Requires(0 <= n);

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

       if (n == 0) {

@@ -4789,7 +4807,7 @@ namespace Microsoft.Dafny {
     /// </summary>

     public static Expression CreateDecrement(Expression e, int n) {

       Contract.Requires(e != null);

-      Contract.Requires(e.Type.NormalizeExpand() is IntType);

+      Contract.Requires(e.Type.IsIntegerType);

       Contract.Requires(0 <= n);

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

       if (n == 0) {

@@ -4848,7 +4866,7 @@ namespace Microsoft.Dafny {
     public static Expression CreateLess(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      Contract.Requires(e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType);

+      Contract.Requires(e0.Type.IsIntegerType && e1.Type.IsIntegerType);

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

       var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Lt, e0, e1);

       s.ResolvedOp = BinaryExpr.ResolvedOpcode.Lt;  // resolve here

@@ -4862,7 +4880,7 @@ namespace Microsoft.Dafny {
     public static Expression CreateAtMost(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      Contract.Requires((e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType) || (e0.Type.NormalizeExpand() is RealType && e1.Type.NormalizeExpand() is RealType));

+      Contract.Requires((e0.Type.IsIntegerType && e1.Type.IsIntegerType) || (e0.Type.IsRealType && e1.Type.IsRealType));

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

       var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Le, e0, e1);

       s.ResolvedOp = BinaryExpr.ResolvedOpcode.Le;  // resolve here

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1486f403..59bb9afc 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -5004,18 +5004,18 @@ namespace Microsoft.Dafny
               case BinaryExpr.ResolvedOpcode.Lt:

               case BinaryExpr.ResolvedOpcode.Le:

                 // for A < B and A <= B, use the decreases B - A

-                guess = Expression.CreateSubtract(bin.E1, bin.E0);

+                guess = Expression.CreateSubtract_TypeConvert(bin.E1, bin.E0);

                 break;

               case BinaryExpr.ResolvedOpcode.Ge:

               case BinaryExpr.ResolvedOpcode.Gt:

                 // for A >= B and A > B, use the decreases A - B

-                guess = Expression.CreateSubtract(bin.E0, bin.E1);

+                guess = Expression.CreateSubtract_TypeConvert(bin.E0, bin.E1);

                 break;

               case BinaryExpr.ResolvedOpcode.NeqCommon:

                 if (bin.E0.Type.IsNumericBased()) {

                   // for A != B where A and B are numeric, use the absolute difference between A and B (that is: if A <= B then B-A else A-B)

-                  var AminusB = Expression.CreateSubtract(bin.E0, bin.E1);

-                  var BminusA = Expression.CreateSubtract(bin.E1, bin.E0);

+                  var AminusB = Expression.CreateSubtract_TypeConvert(bin.E0, bin.E1);

+                  var BminusA = Expression.CreateSubtract_TypeConvert(bin.E1, bin.E0);

                   var test = Expression.CreateAtMost(bin.E0, bin.E1);

                   guess = Expression.CreateITE(test, BminusA, AminusB);

                 }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 1086a79b..4f0f3b61 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -7805,7 +7805,7 @@ namespace Microsoft.Dafny {
         }

       } else if (F is BinaryExpr) {

         var bin = (BinaryExpr)F;

-        if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add) {

+        if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) {

           if (!ContainsFreeVariable(bin.E1, false, i)) {

             // We're looking at:  R(i) && j == f(i) + K.

             // By a recursive call, we'll ask to invert:  R(i) && j' == f(i).

@@ -7823,7 +7823,7 @@ namespace Microsoft.Dafny {
               yield return val.Subst(j, jMinusK, this);

             }

           }

-        } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub) {

+        } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) {

           if (!ContainsFreeVariable(bin.E1, false, i)) {

             // We're looking at:  R(i) && j == f(i) - K

             // Recurse on f(i) and then replace j := j + K

diff --git a/Test/dafny0/Newtypes.dfy b/Test/dafny0/Newtypes.dfy
index bab42378..db737f68 100644
--- a/Test/dafny0/Newtypes.dfy
+++ b/Test/dafny0/Newtypes.dfy
@@ -227,3 +227,85 @@ module IntegerBasedValues {
     }

   }

 }

+

+module Guessing_Termination_Metrics {

+  newtype N = x | x == 0 || x == 3 || x == 7

+

+  method M_Bad() {

+    var x: N, y: N;

+    while x < y

+      decreases y - x;  // error: y-x may not be an N

+    {

+      if 3 < y {

+        y := 3;

+      } else {

+        x := 3;

+      }

+    }

+  }

+

+  method M_Good() {

+    var x: N, y: N;

+    while x < y

+      decreases int(y) - int(x);

+    {

+      if 3 < y {

+        y := 3;

+      } else {

+        x := 3;

+      }

+    }

+  }

+

+  method M_Inferred() {

+    var x: N, y: N;

+    while x < y  // the inferred decreases clause includes the type conversion to int

+    {

+      if 3 < y {

+        y := 3;

+      } else {

+        x := 3;

+      }

+    }

+  }

+

+  newtype R = r | r == 0.0 || 10.0 <= r <= 20.0

+

+  method P_Bad() {

+    var x: R, y: R;

+    while x < y

+      decreases y - x;  // error: y-x may not be an R

+    {

+      if 12.0 < y {

+        y := 10.0;

+      } else {

+        x := 14.2;

+      }

+    }

+  }

+

+  method P_Good() {

+    var x: R, y: R;

+    while x < y

+      decreases real(y) - real(x);

+    {

+      if 12.0 < y {

+        y := 10.0;

+      } else {

+        x := 14.2;

+      }

+    }

+  }

+

+  method P_Inferred() {

+    var x: R, y: R;

+    while x < y  // the inferred decreases clause includes the type conversion to real

+    {

+      if 12.0 < y {

+        y := 10.0;

+      } else {

+        x := 14.2;

+      }

+    }

+  }

+}

diff --git a/Test/dafny0/Newtypes.dfy.expect b/Test/dafny0/Newtypes.dfy.expect
index 7af53142..3ca77f1d 100644
--- a/Test/dafny0/Newtypes.dfy.expect
+++ b/Test/dafny0/Newtypes.dfy.expect
@@ -42,5 +42,17 @@ Newtypes.dfy(225,40): Error: result of operation might violate newtype constrain
 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

+Newtypes.dfy(237,19): Error: result of operation might violate newtype constraint

+Execution trace:

+    (0,0): anon0

+    Newtypes.dfy(236,5): anon9_LoopHead

+    (0,0): anon9_LoopBody

+    (0,0): anon10_Then

+Newtypes.dfy(277,19): Error: result of operation might violate newtype constraint

+Execution trace:

+    (0,0): anon0

+    Newtypes.dfy(276,5): anon9_LoopHead

+    (0,0): anon9_LoopBody

+    (0,0): anon10_Then

 

-Dafny program verifier finished with 35 verified, 11 errors

+Dafny program verifier finished with 47 verified, 13 errors