Added command-line option /warnShadowing, which emits warnings if variables shadow other variables (Issue #86)

4 files changed, 124 insertions, 46 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index af940439..a3b26f2a 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -58,6 +58,7 @@ namespace Microsoft.Dafny
     public bool Optimize = false;

     public bool PrintStats = false;

     public bool PrintFunctionCallGraph = false;

+    public bool WarnShadowing = false;

 

     protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

       var args = ps.args;  // convenient synonym

@@ -183,6 +184,10 @@ namespace Microsoft.Dafny
           PrintFunctionCallGraph = true;

           return true;

 

+        case "warnShadowing":

+          WarnShadowing = true;

+          return true;

+

         case "countVerificationErrors": {

           int countErrors = 1; // defaults to reporting verification errors

           if (ps.GetNumericArgument(ref countErrors, 2)) {

@@ -294,6 +299,8 @@ namespace Microsoft.Dafny
                   - passes /optimize flag to csc.exe.

   /stats        Print interesting statistics about the Dafny files supplied.

   /funcCallGraph Print out the function call graph.  Format is: func,mod=callee*

+  /warnShadowing  Emits a warning if the name of a declared variable caused another variable

+                to be shadowed

 ");

       base.Usage();  // also print the Boogie options

     }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 7c78c1e2..91570a1e 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1374,7 +1374,7 @@ namespace Microsoft.Dafny
             Contract.Assert(dd.Constraint != null);  // follows from NewtypeDecl invariant

             scope.PushMarker();

             var added = scope.Push(dd.Var.Name, dd.Var);

-            Contract.Assert(added);

+            Contract.Assert(added == Scope<IVariable>.PushResult.Success);

             ResolveType(dd.Var.tok, dd.Var.Type, dd, ResolveTypeOptionEnum.DontInfer, null);

             ResolveExpression(dd.Constraint, new ResolveOpts(dd, false, true));

             Contract.Assert(dd.Constraint.Type != null);  // follows from postcondition of ResolveExpression

@@ -3533,12 +3533,43 @@ namespace Microsoft.Dafny
           tp.Parent = parent;

           tp.PositionalIndex = index;

         }

-        if (!allTypeParameters.Push(tp.Name, tp) && emitErrors) {

-          Error(tp, "Duplicate type-parameter name: {0}", tp.Name);

+        var r = allTypeParameters.Push(tp.Name, tp);

+        if (emitErrors) {

+          if (r == Scope<TypeParameter>.PushResult.Duplicate) {

+            Error(tp, "Duplicate type-parameter name: {0}", tp.Name);

+          } else if (r == Scope<TypeParameter>.PushResult.Shadow) {

+            Warning(tp.tok, "Shadowed type-parameter name: {0}", tp.Name);

+          }

         }

       }

     }

 

+    void ScopePushAndReport(Scope<IVariable> scope, IVariable v, string kind) {

+      Contract.Requires(scope != null);

+      Contract.Requires(v != null);

+      Contract.Requires(kind != null);

+      ScopePushAndReport(scope, v.Name, v, v.Tok, kind);

+    }

+

+    void ScopePushAndReport<Thing>(Scope<Thing> scope, string name, Thing thing, IToken tok, string kind) where Thing : class {

+      Contract.Requires(scope != null);

+      Contract.Requires(name != null);

+      Contract.Requires(thing != null);

+      Contract.Requires(tok != null);

+      Contract.Requires(kind != null);

+      var r = scope.Push(name, thing);

+      switch (r) {

+        case Scope<Thing>.PushResult.Success:

+          break;

+        case Scope<Thing>.PushResult.Duplicate:

+          Error(tok, "Duplicate {0} name: {1}", kind, name);

+          break;

+        case Scope<Thing>.PushResult.Shadow:

+          Warning(tok, "Shadowed {0} name: {1}", kind, name);

+          break;

+      }

+    }

+

     /// <summary>

     /// Assumes type parameters have already been pushed

     /// </summary>

@@ -3550,9 +3581,7 @@ namespace Microsoft.Dafny
       }

       var option = f.TypeArgs.Count == 0 ? new ResolveTypeOption(f) : new ResolveTypeOption(ResolveTypeOptionEnum.AllowPrefix);

       foreach (Formal p in f.Formals) {

-        if (!scope.Push(p.Name, p)) {

-          Error(p, "Duplicate parameter name: {0}", p.Name);

-        }

+        ScopePushAndReport(scope, p, "parameter");

         ResolveType(p.tok, p.Type, f, option, f.TypeArgs);

       }

       ResolveType(f.tok, f.ResultType, f, option, f.TypeArgs);

@@ -3660,16 +3689,12 @@ namespace Microsoft.Dafny
       var option = m.TypeArgs.Count == 0 ? new ResolveTypeOption(m) : new ResolveTypeOption(ResolveTypeOptionEnum.AllowPrefix);

       // resolve in-parameters

       foreach (Formal p in m.Ins) {

-        if (!scope.Push(p.Name, p)) {

-          Error(p, "Duplicate parameter name: {0}", p.Name);

-        }

+        ScopePushAndReport(scope, p, "parameter");

         ResolveType(p.tok, p.Type, m, option, m.TypeArgs);

       }

       // resolve out-parameters

       foreach (Formal p in m.Outs) {

-        if (!scope.Push(p.Name, p)) {

-          Error(p, "Duplicate parameter name: {0}", p.Name);

-        }

+        ScopePushAndReport(scope, p, "parameter");

         ResolveType(p.tok, p.Type, m, option, m.TypeArgs);

       }

       scope.PopMarker();

@@ -4828,9 +4853,7 @@ namespace Microsoft.Dafny
         }

         // Add the locals to the scope

         foreach (var local in s.Locals) {

-          if (!scope.Push(local.Name, local)) {

-            Error(local.Tok, "Duplicate local-variable name: {0}", local.Name);

-          }

+          ScopePushAndReport(scope, local, "local-variable");

         }

         // With the new locals in scope, it's now time to resolve the attributes on all the locals

         foreach (var local in s.Locals) {

@@ -5121,9 +5144,7 @@ namespace Microsoft.Dafny
         int prevErrorCount = ErrorCount;

         scope.PushMarker();

         foreach (BoundVar v in s.BoundVars) {

-          if (!scope.Push(v.Name, v)) {

-            Error(v, "Duplicate bound-variable name: {0}", v.Name);

-          }

+          ScopePushAndReport(scope, v, "local-variable");

           ResolveType(v.tok, v.Type, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);

         }

         ResolveExpression(s.Range, new ResolveOpts(codeContext, true, specContextOnly));

@@ -5586,9 +5607,7 @@ namespace Microsoft.Dafny
       if (pat.Var != null) {

         BoundVar v = pat.Var;

         if (topLevel) {

-          if (!scope.Push(v.Name, v)) {

-            Error(v, "Duplicate parameter name: {0}", v.Name);

-          }

+          ScopePushAndReport(scope, v, "parameter");

         } else {

           if (scope.Find(v.Name) != null) {

             Error(v, "Duplicate parameter name: {0}", v.Name);

@@ -6202,8 +6221,8 @@ namespace Microsoft.Dafny
           } else if (prev != null) {

             Error(lnode.Tok, "label shadows an enclosing label");

           } else {

-            bool b = labeledStatements.Push(lnode.Name, ss);

-            Contract.Assert(b);  // since we just checked for duplicates, we expect the Push to succeed

+            var r = labeledStatements.Push(lnode.Name, ss);

+            Contract.Assert(r == Scope<Statement>.PushResult.Success);  // since we just checked for duplicates, we expect the Push to succeed

             if (l == ss.Labels) {  // add it only once

               inSpecOnlyContext.Add(ss, specContextOnly);

             }

@@ -7541,9 +7560,7 @@ namespace Microsoft.Dafny
             // Check for duplicate names now, because not until after resolving the case pattern do we know if identifiers inside it refer to bound variables or nullary constructors

             var c = 0;

             foreach (var v in lhs.Vars) {

-              if (!scope.Push(v.Name, v)) {

-                Error(v, "Duplicate let-variable name: {0}", v.Name);

-              }

+              ScopePushAndReport(scope, v, "let-variable");

               c++;

             }

             if (c == 0) {

@@ -7562,9 +7579,7 @@ namespace Microsoft.Dafny
           foreach (var lhs in e.LHSs) {

             Contract.Assert(lhs.Var != null);  // the parser already checked that every LHS is a BoundVar, not a general pattern

             var v = lhs.Var;

-            if (!scope.Push(v.Name, v)) {

-              Error(v, "Duplicate let-variable name: {0}", v.Name);

-            }

+            ScopePushAndReport(scope, v, "let-variable");

             ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);

           }

           foreach (var rhs in e.RHSs) {

@@ -7596,9 +7611,7 @@ namespace Microsoft.Dafny
         ResolveTypeParameters(e.TypeArgs, true, e);

         scope.PushMarker();

         foreach (BoundVar v in e.BoundVars) {

-          if (!scope.Push(v.Name, v)) {

-            Error(v, "Duplicate bound-variable name: {0}", v.Name);

-          }

+          ScopePushAndReport(scope, v, "bound-variable");

           var option = typeQuantifier ? new ResolveTypeOption(e) : new ResolveTypeOption(ResolveTypeOptionEnum.InferTypeProxies);

           ResolveType(v.tok, v.Type, opts.codeContext, option, typeQuantifier ? e.TypeArgs : null);

         }

@@ -7652,9 +7665,7 @@ namespace Microsoft.Dafny
         int prevErrorCount = ErrorCount;

         scope.PushMarker();

         foreach (BoundVar v in e.BoundVars) {

-          if (!scope.Push(v.Name, v)) {

-            Error(v, "Duplicate bound-variable name: {0}", v.Name);

-          }

+          ScopePushAndReport(scope, v, "bound-variable");

           ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);

         }

         ResolveExpression(e.Range, opts);

@@ -7683,9 +7694,7 @@ namespace Microsoft.Dafny
           Error(e.tok, "a map comprehension must have exactly one bound variable.");

         }

         foreach (BoundVar v in e.BoundVars) {

-          if (!scope.Push(v.Name, v)) {

-            Error(v, "Duplicate bound-variable name: {0}", v.Name);

-          }

+          ScopePushAndReport(scope, v, "bound-variable");

           ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);

         }

         ResolveExpression(e.Range, opts);

@@ -7718,9 +7727,7 @@ namespace Microsoft.Dafny
         int prevErrorCount = ErrorCount;

         scope.PushMarker();

         foreach (BoundVar v in e.BoundVars) {

-          if (!scope.Push(v.Name, v)) {

-            Error(v, "Duplicate bound-variable name: {0}", v.Name);

-          }

+          ScopePushAndReport(scope, v, "bound-variable");

           ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);

         }

 

@@ -10439,17 +10446,27 @@ namespace Microsoft.Dafny
       }

     }

 

-    // Pushes name-->thing association and returns "true", if name has not already been pushed since the last marker.

-    // If name already has been pushed since the last marker, does nothing and returns "false".

-    public bool Push(string name, Thing thing) {

+    public enum PushResult { Duplicate, Shadow, Success }

+

+    /// <summary>

+    /// Pushes name-->thing association and returns "Success", if name has not already been pushed since the last marker.

+    /// If name already has been pushed since the last marker, does nothing and returns "Duplicate".

+    /// If the appropriate command-line option is supplied, then this method will also check if "name" shadows a previous

+    /// name; if it does, then it will return "Shadow" instead of "Success".

+    /// </summary>

+    public PushResult Push(string name, Thing thing) {

       Contract.Requires(name != null);

       Contract.Requires(thing != null);

       if (Find(name, true) != null) {

-        return false;

+        return PushResult.Duplicate;

       } else {

+        var r = PushResult.Success;

+        if (DafnyOptions.O.WarnShadowing && Find(name, false) != null) {

+          r = PushResult.Shadow;

+        }

         names.Add(name);

         things.Add(thing);

-        return true;

+        return r;

       }

     }

 

diff --git a/Test/dafny0/Shadows.dfy b/Test/dafny0/Shadows.dfy
new file mode 100644
index 00000000..da1e74d6
--- /dev/null
+++ b/Test/dafny0/Shadows.dfy
@@ -0,0 +1,42 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /warnShadowing "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+module Module0 {

+  class C<alpha> {

+    method M<beta, beta>(x: beta)  // error: duplicate type parameter

+    method P<alpha>(x: alpha)  // shadowed type parameter

+    function F<beta, beta>(x: beta): int  // error: duplicate type parameter

+    function G<alpha>(x: alpha): int  // shadowed type parameter

+

+    method Q0(x: int) returns (x: int)  // error: duplicate variable name

+  }

+}

+module Module1 {

+  class D {

+    method Q1(x: int) returns (y: int)

+    {

+      var x;  // shadowed

+      var y;  // error: duplicate

+    }

+

+    var f: int

+    method R()

+    {

+      var f;  // okay

+      var f;  // error: duplicate

+    }

+    method S()

+    {

+      var x;

+      {

+        var x;  // shadow

+      }

+    }

+    method T()

+    {

+      var x;

+      ghost var b := forall x :: x < 10;  // shadow

+      ghost var c := forall y :: forall y :: y != y + 1;  // shadow

+    }

+  }

+}

diff --git a/Test/dafny0/Shadows.dfy.expect b/Test/dafny0/Shadows.dfy.expect
new file mode 100644
index 00000000..5083ac64
--- /dev/null
+++ b/Test/dafny0/Shadows.dfy.expect
@@ -0,0 +1,12 @@
+Shadows.dfy(6,19): Error: Duplicate type-parameter name: beta

+Shadows.dfy(7,13): Warning: Shadowed type-parameter name: alpha

+Shadows.dfy(8,21): Error: Duplicate type-parameter name: beta

+Shadows.dfy(9,15): Warning: Shadowed type-parameter name: alpha

+Shadows.dfy(11,31): Error: Duplicate parameter name: x

+Shadows.dfy(18,10): Warning: Shadowed local-variable name: x

+Shadows.dfy(19,10): Error: Duplicate local-variable name: y

+Shadows.dfy(26,10): Error: Duplicate local-variable name: f

+Shadows.dfy(32,12): Warning: Shadowed local-variable name: x

+Shadows.dfy(38,28): Warning: Shadowed bound-variable name: x

+Shadows.dfy(39,40): Warning: Shadowed bound-variable name: y

+5 resolution/type errors detected in Shadows.dfy