Dafny: translate call statements with fancy LHSs

4 files changed, 178 insertions, 60 deletions

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 7afeda44..bcd1b0c5 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1229,7 +1229,7 @@ namespace Microsoft.Dafny {
           }

         }

         // check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)

-        Dictionary<string, object> lhsNameSet = new Dictionary<string, object>();

+        var lhsNameSet = new Dictionary<string, object>();

         foreach (var lhs in s.Lhss) {

           var ie = lhs.Resolved as IdentifierExpr;

           if (ie != null) {

@@ -1704,6 +1704,10 @@ namespace Microsoft.Dafny {
       return isGhost;

     }

 

+    /// <summary>

+    /// Resolves the given call statement.

+    /// Assumes all LHSs have already been resolved.

+    /// </summary>

     void ResolveCallStmt(CallStmt s, bool specContextOnly, Method method, Type receiverType) {

       Contract.Requires(s != null);

       Contract.Requires(method != null);

@@ -1735,15 +1739,9 @@ namespace Microsoft.Dafny {
         }

       }

 

-      // resolve left-hand side

-      Dictionary<string, object> lhsNameSet = new Dictionary<string, object>();

-      foreach (IdentifierExpr lhs in s.Lhs) {

-        ResolveExpression(lhs, true);

-        if (lhsNameSet.ContainsKey(lhs.Name)) {

-          Error(s, "Duplicate variable in left-hand side of call statement: {0}", lhs.Name);

-        } else {

-          lhsNameSet.Add(lhs.Name, null);

-        }

+      // resolve left-hand sides

+      foreach (var lhs in s.Lhs) {

+        Contract.Assume(lhs.Type != null);  // a sanity check that LHSs have already been resolved

       }

       // resolve arguments

       if (!s.IsGhost) {

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 00071fd8..1f3236c7 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -2567,7 +2567,7 @@ namespace Microsoft.Dafny {
       

       // assign input formals of m (except "this")

       for (int i = 0; i < m.Ins.Count; i++) {        

-        Bpl.LocalVariable arg = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, m.Ins[i].UniqueName,  TrType(m.Ins[i].Type)));

+        Bpl.LocalVariable arg = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, m.Ins[i].UniqueName, TrType(m.Ins[i].Type)));

         localVariables.Add(arg);

         Bpl.Variable var = inParams[i+1];

         Contract.Assert(var != null);

@@ -3023,6 +3023,7 @@ namespace Microsoft.Dafny {
         locals.Add(var);

         

       } else if (stmt is CallStmt) {

+        AddComment(builder, stmt, "call statement");

         TrCallStmt((CallStmt)stmt, builder, locals, etran, null);

         

       } else if (stmt is BlockStmt) {

@@ -3462,16 +3463,54 @@ namespace Microsoft.Dafny {
     }

 

     void TrCallStmt(CallStmt s, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran, Bpl.Expr actualReceiver) {

-      Contract.Requires(s != null);

+      List<AssignToLhs> lhsBuilders;

+      List<Bpl.IdentifierExpr> bLhss;

+      ProcessLhss(s.Lhs, true, builder, locals, etran, out lhsBuilders, out bLhss);

+      Contract.Assert(s.Lhs.Count == lhsBuilders.Count);

+      Contract.Assert(s.Lhs.Count == bLhss.Count);

+      var lhsTypes = new List<Type>();

+      for (int i = 0; i < s.Lhs.Count; i++) {

+        var lhs = s.Lhs[i];

+        lhsTypes.Add(lhs.Type);

+        if (bLhss[i] == null) {  // (in the current implementation, the second parameter "true" to ProcessLhss implies that all bLhss[*] will be null)

+          // create temporary local and assign it to bLhss[i]

+          string nm = "$rhs#" + otherTmpVarCount;

+          otherTmpVarCount++;

+          var ty = TrType(lhs.Type);

+          Bpl.Expr wh = GetWhereClause(lhs.tok, new Bpl.IdentifierExpr(lhs.tok, nm, ty), lhs.Type, etran);

+          Bpl.LocalVariable var = new Bpl.LocalVariable(lhs.tok, new Bpl.TypedIdent(lhs.tok, nm, ty, wh));

+          locals.Add(var);

+          bLhss[i] = new Bpl.IdentifierExpr(lhs.tok, var.Name, ty);

+        }

+      }

+      ProcessCallStmt(s.Tok, s.Receiver, actualReceiver, s.Method, s.Args, bLhss, lhsTypes, builder, locals, etran);

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

+        lhsBuilders[i](bLhss[i], builder, etran);

+      }

+      builder.Add(CaptureState(s.Tok));

+    }

+

+    void ProcessCallStmt(IToken tok,

+      Expression dafnyReceiver, Bpl.Expr bReceiver,

+      Method method, List<Expression> Args,

+      List<Bpl.IdentifierExpr> Lhss, List<Type> LhsTypes,

+      Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {

+

+      Contract.Requires(tok != null);

+      Contract.Requires((dafnyReceiver == null) != (bReceiver == null));

+      Contract.Requires(method != null);

+      Contract.Requires(cce.NonNullElements(Args));

+      Contract.Requires(cce.NonNullElements(Lhss));

+      Contract.Requires(cce.NonNullElements(LhsTypes));

+      Contract.Requires(method.Outs.Count == Lhss.Count);

+      Contract.Requires(method.Outs.Count == LhsTypes.Count);

       Contract.Requires(builder != null);

       Contract.Requires(locals != null);

       Contract.Requires(etran != null);

-

-      Expression receiver = actualReceiver == null ? s.Receiver : new BoogieWrapper(actualReceiver);

-      AddComment(builder, s, actualReceiver == null ? "call statement" : "init call statement");

+      

+      Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver);

       Bpl.ExprSeq ins = new Bpl.ExprSeq();

-      Contract.Assert(s.Method != null);  // follows from the fact that stmt has been successfully resolved

-      if (!s.Method.IsStatic) {

+      if (!method.IsStatic) {

         ins.Add(etran.TrExpr(receiver));

       }

 

@@ -3480,8 +3519,8 @@ namespace Microsoft.Dafny {
       // store the actual parameters.

       // Create a local variable for each formal parameter, and assign each actual parameter to the corresponding local

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

-      for (int i = 0; i < s.Method.Ins.Count; i++) {

-        Formal p = s.Method.Ins[i];

+      for (int i = 0; i < method.Ins.Count; i++) {

+        Formal p = method.Ins[i];

         VarDecl local = new VarDecl(p.tok, p.Name, p.Type, p.IsGhost);

         local.type = local.OptionalType;  // resolve local here

         IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);

@@ -3489,55 +3528,56 @@ namespace Microsoft.Dafny {
         substMap.Add(p, ie);

         locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));

 

-        Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie);  // TODO: is this cast always justified?

-        Expression actual = s.Args[i];

+        Bpl.IdentifierExpr param = (Bpl.IdentifierExpr)etran.TrExpr(ie);  // TODO: is this cast always justified?

+        Expression actual = Args[i];

         TrStmt_CheckWellformed(actual, builder, locals, etran, true);

         var bActual = etran.TrExpr(actual);

         CheckSubrange(actual.tok, bActual, p.Type, builder);

-        Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(s.Tok, bActual, cce.NonNull(actual.Type), s.Method.Ins[i].Type));

+        Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, param, etran.CondApplyBox(actual.tok, bActual, cce.NonNull(actual.Type), method.Ins[i].Type));

         builder.Add(cmd);

-        ins.Add(lhs);

+        ins.Add(param);

+      }

+

+      // Check modifies clause

+      CheckFrameSubset(tok, method.Mod, receiver, substMap, etran, builder, "call may violate caller's modifies clause", null);

+

+      // Check termination

+      ModuleDecl module = cce.NonNull(method.EnclosingClass).Module;

+      if (module == cce.NonNull(currentMethod.EnclosingClass).Module) {

+        if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(currentMethod)) {

+          bool contextDecrInferred, calleeDecrInferred;

+          List<Expression> contextDecreases = MethodDecreasesWithDefault(currentMethod, out contextDecrInferred);

+          List<Expression> calleeDecreases = MethodDecreasesWithDefault(method, out calleeDecrInferred);

+          CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, etran, builder, contextDecrInferred);

+        }

       }

-      // Also create variables to hold the output parameters of the call, so that appropriate unboxes can be introduced.

+

+      // Create variables to hold the output parameters of the call, so that appropriate unboxes can be introduced.

       Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();

-      List<Bpl.IdentifierExpr> tmpOuts = new List<Bpl.IdentifierExpr>(s.Lhs.Count);

-      for (int i = 0; i < s.Lhs.Count; i++) {

-        Expression e = s.Lhs[i];

-        if (ExpressionTranslator.ModeledAsBoxType(s.Method.Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType(cce.NonNull(e.Type))) {

+      List<Bpl.IdentifierExpr> tmpOuts = new List<Bpl.IdentifierExpr>();

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

+        var bLhs = Lhss[i];

+        if (ExpressionTranslator.ModeledAsBoxType(method.Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType(LhsTypes[i])) {

           // we need an Unbox

-          Bpl.LocalVariable var = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$tmp#" + otherTmpVarCount, predef.BoxType));

+          Bpl.LocalVariable var = new Bpl.LocalVariable(bLhs.tok, new Bpl.TypedIdent(bLhs.tok, "$tmp#" + otherTmpVarCount, predef.BoxType));

           otherTmpVarCount++;

           locals.Add(var);

-          Bpl.IdentifierExpr varIdE = new Bpl.IdentifierExpr(s.Tok, var.Name, predef.BoxType);

+          Bpl.IdentifierExpr varIdE = new Bpl.IdentifierExpr(bLhs.tok, var.Name, predef.BoxType);

           tmpOuts.Add(varIdE);

           outs.Add(varIdE);

         } else {

           tmpOuts.Add(null);

-          outs.Add(etran.TrExpr(e));

-        }

-      }

-

-      // Check modifies clause

-      CheckFrameSubset(s.Tok, s.Method.Mod, receiver, substMap, etran, builder, "call may violate caller's modifies clause", null);

-

-      // Check termination

-      ModuleDecl module = cce.NonNull(s.Method.EnclosingClass).Module;

-      if (module == cce.NonNull(currentMethod.EnclosingClass).Module) {

-        if (module.CallGraph.GetSCCRepresentative(s.Method) == module.CallGraph.GetSCCRepresentative(currentMethod)) {

-          bool contextDecrInferred, calleeDecrInferred;

-          List<Expression> contextDecreases = MethodDecreasesWithDefault(currentMethod, out contextDecrInferred);

-          List<Expression> calleeDecreases = MethodDecreasesWithDefault(s.Method, out calleeDecrInferred);

-          CheckCallTermination(s.Tok, contextDecreases, calleeDecreases, null, receiver, substMap, etran, builder, contextDecrInferred);

+          outs.Add(bLhs);

         }

       }

 

       // Make the call

-      Bpl.CallCmd call = new Bpl.CallCmd(s.Tok, s.Method.FullName, ins, outs);

+      Bpl.CallCmd call = new Bpl.CallCmd(tok, method.FullName, ins, outs);

       builder.Add(call);

-      for (int i = 0; i < s.Lhs.Count; i++) {

+      // Unbox results as needed

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

+        Bpl.IdentifierExpr bLhs = Lhss[i];

         Bpl.IdentifierExpr tmpVarIdE = tmpOuts[i];

-        var e = (IdentifierExpr)s.Lhs[i];  // TODO: make this work also for non-IdentifierExpr LHSs!

-        Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(e);  // TODO: is this cast always justified?

         if (tmpVarIdE != null) {

           // Instead of an assignment:

           //    e := UnBox(tmpVar);

@@ -3545,13 +3585,12 @@ namespace Microsoft.Dafny {
           //    havoc e; assume e == UnBox(tmpVar);

           // because that will reap the benefits of e's where clause, so that some additional type information will be known about

           // the out-parameter.

-          Bpl.Cmd cmd = new Bpl.HavocCmd(s.Tok, new IdentifierExprSeq(lhs));

+          Bpl.Cmd cmd = new Bpl.HavocCmd(bLhs.tok, new IdentifierExprSeq(bLhs));

           builder.Add(cmd);

-          cmd = new Bpl.AssumeCmd(s.Tok, Bpl.Expr.Eq(lhs, FunctionCall(s.Tok, BuiltinFunction.Unbox, TrType(cce.NonNull(e.Type)), tmpVarIdE)));

+          cmd = new Bpl.AssumeCmd(bLhs.tok, Bpl.Expr.Eq(bLhs, FunctionCall(bLhs.tok, BuiltinFunction.Unbox, TrType(LhsTypes[i]), tmpVarIdE)));

           builder.Add(cmd);

         }

       }

-      builder.Add(CaptureState(s.Tok));

     }

     

     static Expression CreateIntLiteral(IToken tok, int n)

@@ -4006,11 +4045,11 @@ namespace Microsoft.Dafny {
     /// builds code that checks that the LHSs are well-defined, denote different locations,

     /// and are allowed by the enclosing modifies clause.

     /// </summary>

-    List<AssignToLhs> ProcessLhss(List<Expression> lhss, bool rhsCanAffectPreviouslyKnownExpressions,

+    void ProcessLhss(List<Expression> lhss, bool rhsCanAffectPreviouslyKnownExpressions,

       Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran,

       out List<AssignToLhs> lhsBuilders, out List<Bpl.IdentifierExpr/*may be null*/> bLhss) {

+

       Contract.Requires(cce.NonNullElements(lhss));

-      // Contract.Requires(rhs != null);

       Contract.Requires(builder != null);

       Contract.Requires(cce.NonNullElements(locals));

       Contract.Requires(etran != null);

@@ -4132,7 +4171,6 @@ namespace Microsoft.Dafny {
 

         i++;

       }

-      return lhsBuilders;

     }

 

     /// <summary>

@@ -4228,6 +4266,7 @@ namespace Microsoft.Dafny {
         // assume $IsGoodHeap($Heap);

         builder.Add(AssumeGoodHeap(tok, etran));

         if (tRhs.InitCall != null) {

+          AddComment(builder, tRhs.InitCall, "init call statement");

           TrCallStmt(tRhs.InitCall, builder, locals, etran, nw);

         }

         // bLhs := $nw;

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 75025b2f..2edd1c51 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -598,18 +598,18 @@ Execution trace:
     (0,0): anon10

     Basics.dfy(66,95): anon18_Else

     (0,0): anon12

-Basics.dfy(86,16): Error: assertion violation

+Basics.dfy(100,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

-Basics.dfy(99,12): Error: left-hand sides 0 and 1 may refer to the same location

+Basics.dfy(113,12): Error: left-hand sides 0 and 1 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon3

     (0,0): anon11_Else

     (0,0): anon6

     (0,0): anon12_Then

-Basics.dfy(105,10): Error: left-hand sides 0 and 1 may refer to the same location

+Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

@@ -618,11 +618,39 @@ Execution trace:
     (0,0): anon6

     (0,0): anon12_Then

     (0,0): anon9

-Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location

+Basics.dfy(133,10): Error: left-hand sides 0 and 1 may refer to the same location

+Execution trace:

+    (0,0): anon0

+Basics.dfy(145,19): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon11_Then

+Basics.dfy(147,10): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3

+Basics.dfy(147,10): Error: assignment may update an object not in the enclosing method's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3

+Basics.dfy(152,12): Error: left-hand sides 0 and 1 may refer to the same location

 Execution trace:

     (0,0): anon0

+    (0,0): anon11_Then

+    (0,0): anon3

+    (0,0): anon12_Then

+Basics.dfy(163,15): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon11_Then

+    (0,0): anon3

+    (0,0): anon12_Else

+    (0,0): anon6

+    (0,0): anon13_Then

+    (0,0): anon8

+    (0,0): anon14_Then

 

-Dafny program verifier finished with 9 verified, 6 errors

+Dafny program verifier finished with 16 verified, 11 errors

 

 -------------------- ControlStructures.dfy --------------------

 ControlStructures.dfy(5,3): Error: missing case in case statement: Blue

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index b9ba5102..1ae5b9c4 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -71,6 +71,20 @@ method ChallengeTruth(j: int, k: int)
 class Multi {

   var x: int;

   var y: int;

+  var next: Multi;

+  method Mutate(z: int) returns (m: Multi)

+    requires 0 <= z;

+    modifies this;

+    ensures y == old(y);

+  {

+    x := x + z;

+  }

+  method IncX() returns (oldX: int)

+    modifies this;

+    ensures x == old(x) + 1 && oldX == old(x);

+  {

+    x, oldX := x + 1, x;

+  }

 }

 

 method TestMulti(m: Multi, p: Multi)

@@ -117,4 +131,43 @@ method TestBoxAssignment<T>(x: MyBoxyClass<int>, y: MyBoxyClass<T>, t: T)
   x.f := 15;

   // all together now:

   y.f, x.f := t, 15;  // error: duplicate assignment (if T==int and x==y)

+  var k: int := x.f;

+}

+

+method TestCallsWithFancyLhss(m: Multi)

+  requires m != null && m.next != null;

+  modifies m, m.next;

+{

+  m.x := 10;

+  var p := m.next;

+  m.next.next := m.Mutate(m.x);  // fine

+  if (*) {

+    assert m.next == old(m.next);  // error: the call to Mutate may have changed m.next

+  }

+  m.next.next := m.Mutate(20);  // error: LHS may not be well defined (m.next may be null)

+  m.x, m.next := 12, p;

+  m.x, m.y := SwapEm(m.x, m.y);

+  assert m.y == 12;

+  if (*) {

+    m.x, m.x := SwapEm(m.x, m.y);  // error: duplicate among LHSs

+  }

+  m.x := 30;

+  var xx := m.IncX();

+  assert xx == 30;

+  m.y := m.IncX();

+  assert m.y == 31 && m.x == 32;

+  m.x := m.IncX();

+  assert m.x == 32;

+  xx := m.IncX();

+  if (*) {

+    assert xx == 33;  // error: xx will in fact be 32

+  } else {

+    assert xx == 32;  // see!

+  }

+}

+

+method SwapEm(a: int, b: int) returns (x: int, y: int)

+  ensures x == b && y == a;

+{

+  x, y := b, a;

 }