fix: Avoid name capture in :- desugaring (#1095)

Author: RustanLeino

Source/Dafny/Resolver.cs

@@ -12353,8 +12353,8 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ICodeContext codeCo
 
       // We need to figure out whether we are using a status type that has Extract or not,
       // as that determines how the AssignOrReturnStmt is desugared. Thus if the Rhs is a
-      // method call we need to know which one (to inpsectx its first output); if RHs is a
-      // list of expressions, we need to know the type of the first one. FOr all of this we have
+      // method call we need to know which one (to inspect its first output); if RHs is a
+      // list of expressions, we need to know the type of the first one. For all of this we have
       // to do some partial type resolution.
 
       bool expectExtract = s.Lhss.Count != 0; // default value if we cannot determine and inspect the type
@@ -12514,13 +12514,20 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ICodeContext codeCo
         }
         s.ResolvedStatements.Add(ss);
       } else {
+        var enclosingOutParameter = ((Method)codeContext).Outs[0];
+        var ident = new IdentifierExpr(s.Tok, enclosingOutParameter.Name);
+        // resolve it here to avoid capture into more closely declared local variables
+        Contract.Assert(enclosingOutParameter.Type != null);  // this confirms our belief that the out-parameter has already been resolved
+        ident.Var = enclosingOutParameter;
+        ident.Type = ident.Var.Type;
+
         s.ResolvedStatements.Add(
           // "if temp.IsFailure()"
           new IfStmt(s.Tok, s.Tok, false, VarDotMethod(s.Tok, temp, "IsFailure"),
             // THEN: { out := temp.PropagateFailure(); return; }
             new BlockStmt(s.Tok, s.Tok, new List<Statement>() {
               new UpdateStmt(s.Tok, s.Tok,
-                new List<Expression>() {new IdentifierExpr(s.Tok, (codeContext as Method).Outs[0].CompileName)},
+                new List<Expression>() { ident },
                 new List<AssignmentRhs>() {new ExprRhs(VarDotMethod(s.Tok, temp, "PropagateFailure"))}
                 ),
               new ReturnStmt(s.Tok, s.Tok, null),

Test/git-issues/git-issue-1094.dfy

@@ -0,0 +1,146 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// ----- Type error -----
+
+method FP() returns (r: FStatus)
+{
+  {
+    var r: int;  // this variable shadows the out-parameter r
+    :- FTry();  // regression: this once gave an error saying RHS (of type FStatus) not assignable to LHS (of type int)
+  }
+}
+
+method MP() returns (r: MStatus)
+{
+  {
+    var r: int;  // this variable shadows the out-parameter r
+    :- MTry();  // regression: this once gave an error saying RHS (of type MStatus) not assignable to LHS (of type int)
+  }
+}
+
+method FQ() returns (r: FResult<int>)
+  ensures r == FResult.Failure(5)
+{
+  {
+    var r: int;  // this variable shadows the out-parameter r
+    var x :- FCompute();  // regression: this once gave an error saying RHS (of type FResult<?>) not assignable to LHS (of type int)
+  }
+}
+
+method MQ() returns (r: MResult<int>)
+  ensures r == MResult.Failure(5)
+{
+  {
+    var r: int;  // this variable shadows the out-parameter r
+    var x :- MCompute();  // regression: this once gave an error saying RHS (of type MResult<?>) not assignable to LHS (of type int)
+  }
+}
+
+// ----- Verification error -----
+
+method FS() returns (r: FStatus)
+  ensures r == FStatus.Error(5)
+{
+  {
+    var r: FStatus;  // this variable shadows the out-parameter r
+    :- FTry();  // regression: this once resulted in a reported postcondition violation
+  }
+}
+
+method MS() returns (r: MStatus)
+  ensures r == MStatus.Error(5)
+{
+  {
+    var r: MStatus;  // this variable shadows the out-parameter r
+    :- MTry();  // regression: this once resulted in a reported postcondition violation
+  }
+}
+
+method FR() returns (r: FResult<int>)
+  ensures r == FResult.Failure(5)
+{
+  {
+    var r: FResult<int>;  // this variable shadows the out-parameter r
+    var x :- FCompute();  // regression: this once resulted in a reported postcondition violation
+  }
+}
+
+method MR() returns (r: MResult<int>)
+  ensures r == MResult.Failure(5)
+{
+  {
+    var r: MResult<int>;  // this variable shadows the out-parameter r
+    var x :- MCompute();  // regression: this once resulted in a reported postcondition violation
+  }
+}
+
+// ----- Aux definitions -----
+
+method FTry() returns (status: FStatus)
+  ensures status == FStatus.Error(5)
+
+method MTry() returns (status: MStatus)
+  ensures status == MStatus.Error(5)
+
+datatype FStatus = Okay | Error(code: int) {
+  predicate method IsFailure() {
+    Error?
+  }
+  function method PropagateFailure(): FStatus
+    requires Error?
+  {
+    this
+  }
+}
+
+datatype MStatus = Okay | Error(code: int) {
+  predicate method IsFailure() {
+    Error?
+  }
+  method PropagateFailure() returns (m: MStatus)
+    requires Error?
+    ensures m == this
+  {
+    return this;
+  }
+}
+
+method FCompute() returns (result: FResult<int>)
+  ensures result == FResult.Failure(5)
+
+method MCompute() returns (result: MResult<int>)
+  ensures result == MResult.Failure(5)
+
+datatype FResult<X> = Success(x: X) | Failure(code: int) {
+  predicate method IsFailure() {
+    Failure?
+  }
+  function method PropagateFailure<U>(): FResult<U>
+    requires Failure?
+  {
+    FResult.Failure(code)
+  }
+  function method Extract(): X
+    requires Success?
+  {
+    x
+  }
+}
+
+datatype MResult<X> = Success(x: X) | Failure(code: int) {
+  predicate method IsFailure() {
+    Failure?
+  }
+  method PropagateFailure<U>() returns (result: MResult<U>)
+    requires Failure?
+    ensures result.Failure? && result.code == code
+  {
+    return MResult.Failure(code);
+  }
+  method Extract() returns (result: X)
+    requires Success?
+  {
+    return x;
+  }
+}

Test/git-issues/git-issue-1094.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 14 verified, 0 errors