Dafny: Another bug fix in SplitExpr, having to do with generic results of function calls

4 files changed, 62 insertions, 5 deletions

diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc
index 1ea2e150..a8a93067 100644
--- a/Source/Dafny/DafnyAst.ssc
+++ b/Source/Dafny/DafnyAst.ssc
@@ -1346,6 +1346,19 @@ namespace Microsoft.Dafny
     }

   }

   

+  public class UnboxingCastExpr : Expression {  // an UnboxingCastExpr is used only as a temporary placeholding during translation

+    public readonly Expression! E;

+    public readonly Type! FromType;

+    public readonly Type! ToType;

+    

+    public UnboxingCastExpr(Expression! e, Type! fromType, Type! toType) {

+      base(e.tok);

+      E = e;

+      FromType = fromType;

+      ToType = toType;

+    }

+  }

+  

   public class MaybeFreeExpression {

     public readonly Expression! E;

     public readonly bool IsFree;

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index caa8fb2b..fd757b39 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -3075,6 +3075,10 @@ namespace Microsoft.Dafny {
           BoxingCastExpr e = (BoxingCastExpr)expr;

           return CondApplyBox(e.tok, TrExpr(e.E), e.FromType, e.ToType);

           

+        } else if (expr is UnboxingCastExpr) {

+          UnboxingCastExpr e = (UnboxingCastExpr)expr;

+          return CondApplyUnbox(e.tok, TrExpr(e.E), e.FromType, e.ToType);

+          

         } else {

           assert false;  // unexpected expression

         }

@@ -3551,9 +3555,18 @@ namespace Microsoft.Dafny {
     }

 

     public IEnumerable<Expression!>! SplitExpr(Expression! expr, bool expandFunctions)

-      requires expr.Type is BoolType;

+      requires expr.Type is BoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type is BoolType);

     {

-      if (expr is BinaryExpr) {

+      if (expr is BoxingCastExpr) {

+        BoxingCastExpr bce = (BoxingCastExpr)expr;

+        foreach (Expression e in SplitExpr(bce.E, expandFunctions)) {

+          assert bce != null;  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one

+          Expression r = new BoxingCastExpr(e, bce.FromType, bce.ToType);

+          r.Type = bce.ToType;  // resolve here

+          yield return r;

+        }

+        

+      } else if (expr is BinaryExpr) {

         BinaryExpr bin = (BinaryExpr)expr;

         if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {

           foreach (Expression e in SplitExpr(bin.E0, expandFunctions)) {

@@ -3620,7 +3633,9 @@ namespace Microsoft.Dafny {
           Expression body = Substitute(fexp.Function.Body, fexp.Receiver, substMap);

           foreach (Expression se in SplitExpr(body, false)) {

             assert fexp != null && fexp.Function != null;  // already checked above, but the compiler seems to have forgotten that

-            yield return se;

+            Expression piece = new UnboxingCastExpr(se, fexp.Function.ResultType, (!)expr.Type);

+            piece.Type = expr.Type;  // resolve here

+            yield return piece;

           }

           assert fexp != null && fexp.Function != null;  // already checked above, but the compiler seems to have forgotten that

           yield break;

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 0c152d6e..cc248c20 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -389,8 +389,17 @@ Execution trace:
 TypeParameters.dfy(63,27): Error: assertion violation

 Execution trace:

     (0,0): anon0

+TypeParameters.dfy(130,28): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+TypeParameters.dfy(132,33): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

+    (0,0): anon6_Then

 

-Dafny program verifier finished with 24 verified, 2 errors

+Dafny program verifier finished with 27 verified, 4 errors

 

 -------------------- Datatypes.dfy --------------------

 

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index e199a386..61a0019b 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -103,7 +103,7 @@ static function IsCelebrity<Person>(c: Person, people: set<Person>): bool;
   requires c == c || c in people;

 

 method FindCelebrity3(people: set<int>, ghost c: int)

-  requires IsCelebrity(c, people);

+  requires IsCelebrity(c, people);  // once upon a time, this caused the translator to produce bad Boogie

 {

   ghost var b: bool;

   b := IsCelebrity(c, people);

@@ -112,3 +112,23 @@ method FindCelebrity3(people: set<int>, ghost c: int)
 

 static function F(c: int, people: set<int>): bool;

   requires IsCelebrity(c, people);

+

+function RogerThat<G>(g: G): G

+{

+  g

+}

+

+function Cool(b: bool): bool

+{

+  b

+}

+

+method IsRogerCool(n: int)

+  requires RogerThat(true);  // once upon a time, this caused the translator to produce bad Boogie

+{

+  if (*) {

+    assert Cool(2 < 3 && n < n && n < n+1);  // the error message here will peek into the argument of Cool

+  } else if (*) {

+    assert RogerThat(2 < 3 && n < n && n < n+1);  // same here; cool, huh?

+  }

+}