Enable -Wshadow and fix warnings. (#3909)

Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally. 

Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>

6 files changed, 97 insertions, 69 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 76992e1ba..21d7ff0ea 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -43,21 +43,32 @@ ${includes}
     } \
     ++ *(d_exprStatistics[kind]); \
   }
-  #define INC_STAT_VAR(type, bound_var) \
-  { \
-    TypeNode* typeNode = Type::getTypeNode(type); \
-    TypeConstant type = typeNode->getKind() == kind::TYPE_CONSTANT ? typeNode->getConst<TypeConstant>() : LAST_TYPE; \
-    if (d_exprStatisticsVars[type] == NULL) { \
-      stringstream statName; \
-      if (type == LAST_TYPE) { \
-        statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":Parameterized type"; \
-      } else { \
-        statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" << type; \
-      } \
-      d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \
-      d_nodeManager->getStatisticsRegistry()->registerStat(d_exprStatisticsVars[type]); \
-    } \
-    ++ *(d_exprStatisticsVars[type]); \
+#define INC_STAT_VAR(type, bound_var)                                      \
+  {                                                                        \
+    TypeNode* isv_typeNode = Type::getTypeNode(type);                      \
+    TypeConstant isv_type = isv_typeNode->getKind() == kind::TYPE_CONSTANT \
+                                ? isv_typeNode->getConst<TypeConstant>()   \
+                                : LAST_TYPE;                               \
+    if (d_exprStatisticsVars[isv_type] == NULL)                            \
+    {                                                                      \
+      stringstream statName;                                               \
+      if (isv_type == LAST_TYPE)                                           \
+      {                                                                    \
+        statName << "expr::ExprManager::"                                  \
+                 << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE")          \
+                 << ":Parameterized isv_type";                             \
+      }                                                                    \
+      else                                                                 \
+      {                                                                    \
+        statName << "expr::ExprManager::"                                  \
+                 << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":"   \
+                 << isv_type;                                              \
+      }                                                                    \
+      d_exprStatisticsVars[isv_type] = new IntStat(statName.str(), 0);     \
+      d_nodeManager->getStatisticsRegistry()->registerStat(                \
+          d_exprStatisticsVars[isv_type]);                                 \
+    }                                                                      \
+    ++*(d_exprStatisticsVars[isv_type]);                                   \
   }
 #else
   #define INC_STAT(kind)
@@ -882,13 +893,13 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
  * @param check whether we should check the type as we compute it
  * (default: false)
  */
-Type ExprManager::getType(Expr e, bool check)
+Type ExprManager::getType(Expr expr, bool check)
 {
   NodeManagerScope nms(d_nodeManager);
   Type t;
   try {
     t = Type(d_nodeManager,
-             new TypeNode(d_nodeManager->getType(e.getNode(), check)));
+             new TypeNode(d_nodeManager->getType(expr.getNode(), check)));
   } catch (const TypeCheckingExceptionPrivate& e) {
     throw TypeCheckingException(this, &e);
   }
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 998f58d0c..3ed72e03e 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -156,13 +156,20 @@ static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& v
 class ExportPrivate {
 private:
   typedef std::unordered_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache;
-  ExprManager* from;
-  ExprManager* to;
-  ExprManagerMapCollection& vmap;
-  uint32_t flags;
-  ExportCache exportCache;
-public:
-  ExportPrivate(ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags) : from(from), to(to), vmap(vmap), flags(flags) {}
+  ExprManager* d_from;
+  ExprManager* d_to;
+  ExprManagerMapCollection& d_vmap;
+  uint32_t d_flags;
+  ExportCache d_exportCache;
+
+ public:
+  ExportPrivate(ExprManager* from,
+                ExprManager* to,
+                ExprManagerMapCollection& vmap,
+                uint32_t flags)
+      : d_from(from), d_to(to), d_vmap(vmap), d_flags(flags)
+  {
+  }
   Node exportInternal(TNode n) {
 
     if(n.isNull()) return Node::null();
@@ -173,17 +180,18 @@ public:
 
     if(n.getMetaKind() == metakind::CONSTANT) {
       if(n.getKind() == kind::EMPTYSET) {
-        Type type = from->exportType(n.getConst< ::CVC4::EmptySet >().getType(), to, vmap);
-        return to->mkConst(::CVC4::EmptySet(type));
+        Type type = d_from->exportType(
+            n.getConst< ::CVC4::EmptySet>().getType(), d_to, d_vmap);
+        return d_to->mkConst(::CVC4::EmptySet(type));
       }
-      return exportConstant(n, NodeManager::fromExprManager(to), vmap);
+      return exportConstant(n, NodeManager::fromExprManager(d_to), d_vmap);
     } else if(n.getMetaKind() == metakind::NULLARY_OPERATOR ){
-      Expr from_e(from, new Node(n));
-      Type type = from->exportType(from_e.getType(), to, vmap);
-      return to->mkNullaryOperator(type, n.getKind()); // FIXME thread safety
+      Expr from_e(d_from, new Node(n));
+      Type type = d_from->exportType(from_e.getType(), d_to, d_vmap);
+      return d_to->mkNullaryOperator(type, n.getKind());  // FIXME thread safety
     } else if(n.getMetaKind() == metakind::VARIABLE) {
-      Expr from_e(from, new Node(n));
-      Expr& to_e = vmap.d_typeMap[from_e];
+      Expr from_e(d_from, new Node(n));
+      Expr& to_e = d_vmap.d_typeMap[from_e];
       if(! to_e.isNull()) {
         Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl;
         return to_e.getNode();
@@ -191,20 +199,20 @@ public:
         // construct new variable in other manager:
         // to_e is a ref, so this inserts from_e -> to_e
         std::string name;
-        Type type = from->exportType(from_e.getType(), to, vmap);
+        Type type = d_from->exportType(from_e.getType(), d_to, d_vmap);
         if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) {
           if (n.getKind() == kind::BOUND_VARIABLE)
           {
             // bound vars are only available at the Node level (not the Expr
             // level)
             TypeNode typeNode = TypeNode::fromType(type);
-            NodeManager* to_nm = NodeManager::fromExprManager(to);
-            Node n = to_nm->mkBoundVar(name, typeNode);  // FIXME thread safety
+            NodeManager* to_nm = NodeManager::fromExprManager(d_to);
+            Node nn = to_nm->mkBoundVar(name, typeNode);  // FIXME thread safety
 
             // Make sure that the correct `NodeManager` is in scope while
             // converting the node to an expression.
             NodeManagerScope to_nms(to_nm);
-            to_e = n.toExpr();
+            to_e = nn.toExpr();
           } else if(n.getKind() == kind::VARIABLE) {
             bool isGlobal;
             Node::fromExpr(from_e).getAttribute(GlobalVarAttr(), isGlobal);
@@ -212,17 +220,24 @@ public:
             // Temporarily set the node manager to nullptr; this gets around
             // a check that mkVar isn't called internally
             NodeManagerScope nullScope(nullptr);
-            to_e = to->mkVar(name, type, isGlobal ? ExprManager::VAR_FLAG_GLOBAL : flags);// FIXME thread safety
+            to_e = d_to->mkVar(name,
+                               type,
+                               isGlobal ? ExprManager::VAR_FLAG_GLOBAL
+                                        : d_flags);  // FIXME thread safety
           } else if(n.getKind() == kind::SKOLEM) {
             // skolems are only available at the Node level (not the Expr level)
             TypeNode typeNode = TypeNode::fromType(type);
-            NodeManager* to_nm = NodeManager::fromExprManager(to);
-            Node n = to_nm->mkSkolem(name, typeNode, "is a skolem variable imported from another ExprManager");// FIXME thread safety
+            NodeManager* to_nm = NodeManager::fromExprManager(d_to);
+            Node nn =
+                to_nm->mkSkolem(name,
+                                typeNode,
+                                "is a skolem variable imported from another "
+                                "ExprManager");  // FIXME thread safety
 
             // Make sure that the correct `NodeManager` is in scope while
             // converting the node to an expression.
             NodeManagerScope to_nms(to_nm);
-            to_e = n.toExpr();
+            to_e = nn.toExpr();
           } else {
             Unhandled();
           }
@@ -234,38 +249,39 @@ public:
             // bound vars are only available at the Node level (not the Expr
             // level)
             TypeNode typeNode = TypeNode::fromType(type);
-            NodeManager* to_nm = NodeManager::fromExprManager(to);
-            Node n = to_nm->mkBoundVar(typeNode);  // FIXME thread safety
+            NodeManager* to_nm = NodeManager::fromExprManager(d_to);
+            Node nn = to_nm->mkBoundVar(typeNode);  // FIXME thread safety
 
             // Make sure that the correct `NodeManager` is in scope while
             // converting the node to an expression.
             NodeManagerScope to_nms(to_nm);
-            to_e = n.toExpr();
+            to_e = nn.toExpr();
           }
           else
           {
             // Temporarily set the node manager to nullptr; this gets around
             // a check that mkVar isn't called internally
             NodeManagerScope nullScope(nullptr);
-            to_e = to->mkVar(type);  // FIXME thread safety
+            to_e = d_to->mkVar(type);  // FIXME thread safety
           }
           Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl;
         }
         uint64_t to_int = (uint64_t)(to_e.getNode().d_nv);
         uint64_t from_int = (uint64_t)(from_e.getNode().d_nv);
-        vmap.d_from[to_int] = from_int;
-        vmap.d_to[from_int] = to_int;
-        vmap.d_typeMap[to_e] = from_e;// insert other direction too
+        d_vmap.d_from[to_int] = from_int;
+        d_vmap.d_to[from_int] = to_int;
+        d_vmap.d_typeMap[to_e] = from_e;  // insert other direction too
 
         // Make sure that the expressions are associated with the correct
         // `ExprManager`s.
-        Assert(from_e.getExprManager() == from);
-        Assert(to_e.getExprManager() == to);
+        Assert(from_e.getExprManager() == d_from);
+        Assert(to_e.getExprManager() == d_to);
         return Node::fromExpr(to_e);
       }
     } else {
-      if(exportCache.find(n) != exportCache.end()) {
-        return exportCache[n];
+      if (d_exportCache.find(n) != d_exportCache.end())
+      {
+        return d_exportCache[n];
       }
 
       std::vector<Node> children;
@@ -286,16 +302,17 @@ public:
 
         // `n` belongs to the `from` ExprManager, so begin ExprManagerScope
         // after printing `n`
-        ExprManagerScope ems(*to);
+        ExprManagerScope ems(*d_to);
         for(std::vector<Node>::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) {
           Debug("export") << "  child: " << *i << std::endl;
         }
       }
 
       // FIXME thread safety
-      Node ret = NodeManager::fromExprManager(to)->mkNode(n.getKind(), children);
+      Node ret =
+          NodeManager::fromExprManager(d_to)->mkNode(n.getKind(), children);
 
-      exportCache[n] = ret;
+      d_exportCache[n] = ret;
       return ret;
     }
   }/* exportInternal() */
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 595adda55..0c572f615 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -517,8 +517,7 @@ Node substituteCaptureAvoiding(TNode n,
             (std::distance(src.begin(), itt.base()) - 1) >= 0
             && static_cast<unsigned>(std::distance(src.begin(), itt.base()) - 1)
                    < dest.size());
-        Node n = dest[std::distance(src.begin(), itt.base()) - 1];
-        visited[curr] = n;
+        visited[curr] = dest[std::distance(src.begin(), itt.base()) - 1];
         continue;
       }
       if (curr.getNumChildren() == 0)
@@ -568,8 +567,7 @@ Node substituteCaptureAvoiding(TNode n,
         Assert(visited.find(curr[i]) != visited.end());
         nb << visited[curr[i]];
       }
-      Node n = nb;
-      visited[curr] = n;
+      visited[curr] = nb;
 
       // remove renaming
       if (curr.isClosure())
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 367162420..5d409f748 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -330,8 +330,9 @@ void NodeManager::reclaimZombies() {
         TNode n;
         n.d_nv = nv;
         nv->d_rc = 1; // so that TNode doesn't assert-fail
-        for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-          (*i)->nmNotifyDeleteNode(n);
+        for (NodeManagerListener* listener : d_listeners)
+        {
+          listener->nmNotifyDeleteNode(n);
         }
         // this would mean that one of the listeners stowed away
         // a reference to this node!
diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp
index 516870e9c..f99c8a2da 100644
--- a/src/expr/type_matcher.cpp
+++ b/src/expr/type_matcher.cpp
@@ -86,9 +86,9 @@ bool TypeMatcher::doMatching(TypeNode pattern, TypeNode tn)
   {
     return false;
   }
-  for (size_t i = 0, nchild = pattern.getNumChildren(); i < nchild; i++)
+  for (size_t j = 0, nchild = pattern.getNumChildren(); j < nchild; j++)
   {
-    if (!doMatching(pattern[i], tn[i]))
+    if (!doMatching(pattern[j], tn[j]))
     {
       return false;
     }
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 945462dd6..0aa622bfb 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -46,14 +46,15 @@ TypeNode TypeNode::substitute(const TypeNode& type,
     // push the operator
     nb << TypeNode(d_nv->d_children[0]);
   }
-  for(TypeNode::const_iterator i = begin(),
-        iend = end();
-      i != iend;
-      ++i) {
-    if(*i == type) {
+  for (TypeNode::const_iterator j = begin(), iend = end(); j != iend; ++j)
+  {
+    if (*j == type)
+    {
       nb << replacement;
-    } else {
-      (*i).substitute(type, replacement);
+    }
+    else
+    {
+      (*j).substitute(type, replacement);
     }
   }