Dafny: handle refinement of nested tokens that come from SpliExpr (still need to deal with unsplit expressions, like quantifiers)

2 files changed, 87 insertions, 69 deletions

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 3085fc3b..c97f47aa 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -30,6 +30,16 @@ namespace Microsoft.Dafny {
     }

 

     public static bool IsInherited(IToken tok, ModuleDecl m) {

+      while (tok is NestedToken) {

+        var n = (NestedToken)tok;

+        // check Outer

+        var r = n.Outer as RefinementToken;

+        if (r == null || r.InheritingModule != m) {

+          return false;

+        }

+        // continue to check Inner

+        tok = n.Inner;

+      }

       var rtok = tok as RefinementToken;

       return rtok != null && rtok.InheritingModule == m;

     }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index fc07b3ad..a0e67ad1 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -6323,14 +6323,16 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<List<SplitExprInfo>>() != null);

 

       var splits = new List<SplitExprInfo>();

-      splitHappened = TrSplitExpr(expr, splits, true, true, etran);

+      splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, etran);

       return splits;

     }

 

     /// <summary>

     /// Tries to split the expression into tactical conjuncts (if "position") or disjuncts (if "!position").

+    /// If a (necessarily boolean) function call appears as a top-level conjunct, then inline the function if

+    /// if it declared in the current module and its height is less than "heightLimit".

     /// </summary>

-    internal bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool position, bool expandFunctions, ExpressionTranslator etran) {

+    internal bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool position, int heightLimit, ExpressionTranslator etran) {

       Contract.Requires(expr != null);

       Contract.Requires(expr.Type is BoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type is BoolType));

       Contract.Requires(splits != null);

@@ -6339,7 +6341,7 @@ namespace Microsoft.Dafny {
       if (expr is BoxingCastExpr) {

         var bce = (BoxingCastExpr)expr;

         var ss = new List<SplitExprInfo>();

-        if (TrSplitExpr(bce.E, ss, position, expandFunctions, etran)) {

+        if (TrSplitExpr(bce.E, ss, position, heightLimit, etran)) {

           foreach (var s in ss) {

             splits.Add(new SplitExprInfo(s.IsFree, etran.CondApplyBox(s.E.tok, s.E, bce.FromType, bce.ToType)));

           }

@@ -6348,17 +6350,17 @@ namespace Microsoft.Dafny {
 

       } else if (expr is ConcreteSyntaxExpression) {

         var e = (ConcreteSyntaxExpression)expr;

-        return TrSplitExpr(e.ResolvedExpression, splits, position, expandFunctions, etran);

+        return TrSplitExpr(e.ResolvedExpression, splits, position, heightLimit, etran);

 

       } else if (expr is LetExpr) {

         var e = (LetExpr)expr;

-        return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, expandFunctions, etran);

+        return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, heightLimit, etran);

 

       } else if (expr is UnaryExpr) {

         var e = (UnaryExpr)expr;

         if (e.Op == UnaryExpr.Opcode.Not) {

           var ss = new List<SplitExprInfo>();

-          if (TrSplitExpr(e.E, ss, !position, expandFunctions, etran)) {

+          if (TrSplitExpr(e.E, ss, !position, heightLimit, etran)) {

             foreach (var s in ss) {

               splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Unary(s.E.tok, UnaryOperator.Opcode.Not, s.E)));

             }

@@ -6369,13 +6371,13 @@ namespace Microsoft.Dafny {
       } else if (expr is BinaryExpr) {

         var bin = (BinaryExpr)expr;

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

-          TrSplitExpr(bin.E0, splits, position, expandFunctions, etran);

-          TrSplitExpr(bin.E1, splits, position, expandFunctions, etran);

+          TrSplitExpr(bin.E0, splits, position, heightLimit, etran);

+          TrSplitExpr(bin.E1, splits, position, heightLimit, etran);

           return true;

 

         } else  if (!position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) {

-          TrSplitExpr(bin.E0, splits, position, expandFunctions, etran);

-          TrSplitExpr(bin.E1, splits, position, expandFunctions, etran);

+          TrSplitExpr(bin.E0, splits, position, heightLimit, etran);

+          TrSplitExpr(bin.E1, splits, position, heightLimit, etran);

           return true;

 

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

@@ -6383,14 +6385,14 @@ namespace Microsoft.Dafny {
           if (position) {

             var lhs = etran.TrExpr(bin.E0);

             var ss = new List<SplitExprInfo>();

-            TrSplitExpr(bin.E1, ss, position, expandFunctions, etran);

+            TrSplitExpr(bin.E1, ss, position, heightLimit, etran);

             foreach (var s in ss) {

               // as the source location in the following implication, use that of the translated "s"

               splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, lhs, s.E)));

             }

           } else {

             var ss = new List<SplitExprInfo>();

-            TrSplitExpr(bin.E0, ss, !position, expandFunctions, etran);

+            TrSplitExpr(bin.E0, ss, !position, heightLimit, etran);

             var lhs = etran.TrExpr(bin.E1);

             foreach (var s in ss) {

               // as the source location in the following implication, use that of the translated "s"

@@ -6406,7 +6408,7 @@ namespace Microsoft.Dafny {
         var ssThen = new List<SplitExprInfo>();

         var ssElse = new List<SplitExprInfo>();

         // Note: The following lines intentionally uses | instead of ||, because we need both calls to TrSplitExpr

-        if (TrSplitExpr(ite.Thn, ssThen, position, expandFunctions, etran) | TrSplitExpr(ite.Els, ssElse, position, expandFunctions, etran)) {

+        if (TrSplitExpr(ite.Thn, ssThen, position, heightLimit, etran) | TrSplitExpr(ite.Els, ssElse, position, heightLimit, etran)) {

           var op = position ? BinaryOperator.Opcode.Imp : BinaryOperator.Opcode.And;

           var test = etran.TrExpr(ite.Test);

           foreach (var s in ssThen) {

@@ -6431,14 +6433,14 @@ namespace Microsoft.Dafny {
         if (position) {

           var guard = etran.TrExpr(e.Guard);

           var ss = new List<SplitExprInfo>();

-          TrSplitExpr(e.Body, ss, position, expandFunctions, etran);

+          TrSplitExpr(e.Body, ss, position, heightLimit, etran);

           foreach (var s in ss) {

             // as the source location in the following implication, use that of the translated "s"

             splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, guard, s.E)));

           }

         } else {

           var ss = new List<SplitExprInfo>();

-          TrSplitExpr(e.Guard, ss, !position, expandFunctions, etran);

+          TrSplitExpr(e.Guard, ss, !position, heightLimit, etran);

           var rhs = etran.TrExpr(e.Body);

           foreach (var s in ss) {

             // as the source location in the following implication, use that of the translated "s"

@@ -6449,59 +6451,65 @@ namespace Microsoft.Dafny {
 

       } else if (expr is OldExpr) {

         var e = (OldExpr)expr;

-        return TrSplitExpr(e.E, splits, position, expandFunctions, etran.Old);

-

-      } else if (expandFunctions && position && expr is FunctionCallExpr) {

-        var fexp = (FunctionCallExpr)expr;

-        Contract.Assert(fexp.Function != null);  // filled in during resolution

-        if (fexp.Function is Predicate && fexp.Function.EnclosingClass.Module != currentModule) {

-          // don't trace into foreign predicates

-        } else if (fexp.Function.Body != null && !(fexp.Function.Body.Resolved is MatchExpr)) {

-          // inline this body

-          Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();

-          Contract.Assert(fexp.Args.Count == fexp.Function.Formals.Count);

-          for (int i = 0; i < fexp.Function.Formals.Count; i++) {

-            Formal p = fexp.Function.Formals[i];

-            Expression arg = fexp.Args[i];

-            arg = new BoxingCastExpr(arg, cce.NonNull(arg.Type), p.Type);

-            arg.Type = p.Type;  // resolve here

-            substMap.Add(p, arg);

-          }

-          Expression body = Substitute(fexp.Function.Body, fexp.Receiver, substMap);

-

-          // Produce, for a "body" split into b0, b1, b2:

-          //     free F#canCall(args) && F(args) && (b0 && b1 && b2)

-          //     checked F#canCall(args) ==> F(args) || b0

-          //     checked F#canCall(args) ==> F(args) || b1

-          //     checked F#canCall(args) ==> F(args) || b2

-          // Note that "body" does not contain limited calls.

-

-          // F#canCall(args)

-          Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, fexp.Function.FullName + "#canCall", Bpl.Type.Bool);

-          ExprSeq args = etran.FunctionInvocationArguments(fexp);

-          Bpl.Expr canCall = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

-

-          // F(args)

-          Bpl.Expr fargs = etran.TrExpr(fexp);

-

-          // body

-          Bpl.Expr trBody = etran.TrExpr(body);

-          trBody = etran.CondApplyUnbox(trBody.tok, trBody, fexp.Function.ResultType, expr.Type);

+        return TrSplitExpr(e.E, splits, position, heightLimit, etran.Old);

 

-          // here goes the free piece:

-          splits.Add(new SplitExprInfo(true, BplAnd(canCall, BplAnd(fargs, trBody))));

+      } else if (expr is FunctionCallExpr) {

+        if (position) {

+          var fexp = (FunctionCallExpr)expr;

+          var f = fexp.Function;

+          Contract.Assert(f != null);  // filled in during resolution

+          var module = f.EnclosingClass.Module;

+          var functionHeight = module.CallGraph.GetSCCRepresentativeId(f);

+

+          if (module == currentModule && functionHeight < heightLimit) {

+            if (f.Body != null && !(f.Body.Resolved is MatchExpr)) {

+              // inline this body

+              Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();

+              Contract.Assert(fexp.Args.Count == f.Formals.Count);

+              for (int i = 0; i < f.Formals.Count; i++) {

+                Formal p = f.Formals[i];

+                Expression arg = fexp.Args[i];

+                arg = new BoxingCastExpr(arg, cce.NonNull(arg.Type), p.Type);

+                arg.Type = p.Type;  // resolve here

+                substMap.Add(p, arg);

+              }

+              Expression body = Substitute(f.Body, fexp.Receiver, substMap);

+

+              // Produce, for a "body" split into b0, b1, b2:

+              //     free F#canCall(args) && F(args) && (b0 && b1 && b2)

+              //     checked F#canCall(args) ==> F(args) || b0

+              //     checked F#canCall(args) ==> F(args) || b1

+              //     checked F#canCall(args) ==> F(args) || b2

+              // Note that "body" does not contain limited calls.

+

+              // F#canCall(args)

+              Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullName + "#canCall", Bpl.Type.Bool);

+              ExprSeq args = etran.FunctionInvocationArguments(fexp);

+              Bpl.Expr canCall = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

+

+              // F(args)

+              Bpl.Expr fargs = etran.TrExpr(fexp);

+

+              // body

+              Bpl.Expr trBody = etran.TrExpr(body);

+              trBody = etran.CondApplyUnbox(trBody.tok, trBody, f.ResultType, expr.Type);

+

+              // here goes the free piece:

+              splits.Add(new SplitExprInfo(true, Bpl.Expr.Binary(trBody.tok, BinaryOperator.Opcode.And, canCall, BplAnd(fargs, trBody))));

+

+              // recurse on body

+              var ss = new List<SplitExprInfo>();

+              TrSplitExpr(body, ss, position, functionHeight, etran);

+              foreach (var s in ss) {

+                var unboxedConjunct = etran.CondApplyUnbox(s.E.tok, s.E, f.ResultType, expr.Type);

+                var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct);

+                var p = Bpl.Expr.Binary(new NestedToken(fexp.tok, s.E.tok), BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct);

+                splits.Add(new SplitExprInfo(s.IsFree, p));

+              }

 

-          // recurse on body

-          var ss = new List<SplitExprInfo>();

-          TrSplitExpr(body, ss, position, false, etran);

-          foreach (var s in ss) {

-            var unboxedConjunct = etran.CondApplyUnbox(s.E.tok, s.E, fexp.Function.ResultType, expr.Type);

-            var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct);

-            var p = Bpl.Expr.Binary(new NestedToken(fexp.tok, s.E.tok), BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct);

-            splits.Add(new SplitExprInfo(s.IsFree, p));

+              return true;

+            }

           }

-

-          return true;

         }

 

       } else if ((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) {

@@ -6589,13 +6597,13 @@ namespace Microsoft.Dafny {
         }

       }

 

-      if (expandFunctions && !(position && expr is ExistsExpr) && !(!position && expr is ForallExpr)) {

-        etran = etran.LayerOffset(1);

+      if ((position && expr is ExistsExpr) || (!position && expr is ForallExpr)) {

         splits.Add(new SplitExprInfo(false, etran.TrExpr(expr)));

-        return etran.Statistics_CustomLayerFunctionCount != 0;  // return true if the LayerOffset(1) came into play

+        return false;

       } else {

+        etran = etran.LayerOffset(1);

         splits.Add(new SplitExprInfo(false, etran.TrExpr(expr)));

-        return false;

+        return etran.Statistics_CustomLayerFunctionCount != 0;  // return true if the LayerOffset(1) came into play

       }

     }