Generalize front-end checks to check for shadowed variables (#7634)

When using the API, we currently check for free variables in assertions and in terms passed to get-value.

We also require checking for variable shadowing.

This generalizes the utility method so that both free variables and shadowed variables are checked and reported to the user.

4 files changed, 165 insertions, 78 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 4dcfb466e..7976c19ef 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4694,6 +4694,7 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt,
 
 bool Grammar::containsFreeVariables(const Term& rule) const
 {
+  // we allow the argument list and non-terminal symbols to be in scope
   std::unordered_set<TNode> scope;
 
   for (const Term& sygusVar : d_sygusVars)
@@ -4706,8 +4707,7 @@ bool Grammar::containsFreeVariables(const Term& rule) const
     scope.emplace(*ntsymbol.d_node);
   }
 
-  std::unordered_set<Node> fvs;
-  return expr::getFreeVariablesScope(*rule.d_node, fvs, scope, false);
+  return expr::hasFreeVariablesScope(*rule.d_node, scope);
 }
 
 std::ostream& operator<<(std::ostream& out, const Grammar& grammar)
@@ -5079,8 +5079,12 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
 Term Solver::getValueHelper(const Term& term) const
 {
   // Note: Term is checked in the caller to avoid double checks
-  CVC5_API_RECOVERABLE_CHECK(!expr::hasFreeVar(term.getNode()))
-      << "Cannot get value of term containing free variables";
+  bool wasShadow = false;
+  bool freeOrShadowedVar =
+      expr::hasFreeOrShadowedVar(term.getNode(), wasShadow);
+  CVC5_API_RECOVERABLE_CHECK(!freeOrShadowedVar)
+      << "Cannot get value of term containing "
+      << (wasShadow ? "shadowed" : "free") << " variables";
   //////// all checks before this line
   Node value = d_slv->getValue(*term.d_node);
   Term res = Term(this, value);
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 13265db71..badf0b75a 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -281,64 +281,32 @@ bool hasBoundVar(TNode n)
   return n.getAttribute(HasBoundVarAttr());
 }
 
-bool hasFreeVar(TNode n)
-{
-  // optimization for variables and constants
-  if (n.getNumChildren() == 0)
-  {
-    return n.getKind() == kind::BOUND_VARIABLE;
-  }
-  std::unordered_set<Node> fvs;
-  return getFreeVariables(n, fvs, false);
-}
-
-struct HasClosureTag
-{
-};
-struct HasClosureComputedTag
-{
-};
-/** Attribute true for expressions with closures in them */
-typedef expr::Attribute<HasClosureTag, bool> HasClosureAttr;
-typedef expr::Attribute<HasClosureComputedTag, bool> HasClosureComputedAttr;
-
-bool hasClosure(Node n)
-{
-  if (!n.getAttribute(HasClosureComputedAttr()))
-  {
-    bool hasC = false;
-    if (n.isClosure())
-    {
-      hasC = true;
-    }
-    else
-    {
-      for (auto i = n.begin(); i != n.end() && !hasC; ++i)
-      {
-        hasC = hasClosure(*i);
-      }
-    }
-    if (!hasC && n.hasOperator())
-    {
-      hasC = hasClosure(n.getOperator());
-    }
-    n.setAttribute(HasClosureAttr(), hasC);
-    n.setAttribute(HasClosureComputedAttr(), true);
-    return hasC;
-  }
-  return n.getAttribute(HasClosureAttr());
-}
-
-bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs, bool computeFv)
-{
-  std::unordered_set<TNode> scope;
-  return getFreeVariablesScope(n, fvs, scope, computeFv);
-}
-
-bool getFreeVariablesScope(TNode n,
-                           std::unordered_set<Node>& fvs,
-                           std::unordered_set<TNode>& scope,
-                           bool computeFv)
+/**
+ * Check variables internal, which is used as a helper to implement many of the
+ * methods in this file.
+ *
+ * This computes the free variables in n, that is, the subterms of n of kind
+ * BOUND_VARIABLE that are not bound in n or occur in scope, adds these to fvs
+ * if computeFv is true.
+ *
+ * @param n The node under investigation
+ * @param fvs The set which free variables are added to
+ * @param scope The scope we are considering.
+ * @param wasShadow Flag set to true if variable shadowing was encountered.
+ * Only computed if checkShadow is true.
+ * @param computeFv If this flag is false, then we only return true/false and
+ * do not add to fvs.
+ * @param checkShadow If this flag is true, we immediately return true if a
+ * variable is shadowing. If this flag is false, we give an assertion failure
+ * when this occurs.
+ * @return true iff this node contains a free variable.
+ */
+bool checkVariablesInternal(TNode n,
+                            std::unordered_set<Node>& fvs,
+                            std::unordered_set<TNode>& scope,
+                            bool& wasShadow,
+                            bool computeFv = true,
+                            bool checkShadow = false)
 {
   std::unordered_set<TNode> visited;
   std::vector<TNode> visit;
@@ -376,13 +344,26 @@ bool getFreeVariablesScope(TNode n,
         // add to scope
         for (const TNode& cn : cur[0])
         {
-          // should not shadow
-          Assert(scope.find(cn) == scope.end())
-              << "Shadowed variable " << cn << " in " << cur << "\n";
+          if (checkShadow)
+          {
+            if (scope.find(cn) != scope.end())
+            {
+              wasShadow = true;
+              return true;
+            }
+          }
+          else
+          {
+            // should not shadow
+            Assert(scope.find(cn) == scope.end())
+                << "Shadowed variable " << cn << " in " << cur << "\n";
+          }
           scope.insert(cn);
         }
         // must make recursive call to use separate cache
-        if (getFreeVariablesScope(cur[1], fvs, scope, computeFv) && !computeFv)
+        if (checkVariablesInternal(
+                cur[1], fvs, scope, wasShadow, computeFv, checkShadow)
+            && !computeFv)
         {
           return true;
         }
@@ -406,6 +387,95 @@ bool getFreeVariablesScope(TNode n,
   return !fvs.empty();
 }
 
+/** Same as above, without checking for shadowing */
+bool getVariablesInternal(TNode n,
+                          std::unordered_set<Node>& fvs,
+                          std::unordered_set<TNode>& scope,
+                          bool computeFv = true)
+{
+  bool wasShadow = false;
+  return checkVariablesInternal(n, fvs, scope, wasShadow, computeFv, false);
+}
+
+bool hasFreeVar(TNode n)
+{
+  // optimization for variables and constants
+  if (n.getNumChildren() == 0)
+  {
+    return n.getKind() == kind::BOUND_VARIABLE;
+  }
+  std::unordered_set<Node> fvs;
+  std::unordered_set<TNode> scope;
+  return getVariablesInternal(n, fvs, scope, false);
+}
+
+bool hasFreeOrShadowedVar(TNode n, bool& wasShadow)
+{
+  // optimization for variables and constants
+  if (n.getNumChildren() == 0)
+  {
+    return n.getKind() == kind::BOUND_VARIABLE;
+  }
+  std::unordered_set<Node> fvs;
+  std::unordered_set<TNode> scope;
+  return checkVariablesInternal(n, fvs, scope, wasShadow, false, true);
+}
+
+struct HasClosureTag
+{
+};
+struct HasClosureComputedTag
+{
+};
+/** Attribute true for expressions with closures in them */
+typedef expr::Attribute<HasClosureTag, bool> HasClosureAttr;
+typedef expr::Attribute<HasClosureComputedTag, bool> HasClosureComputedAttr;
+
+bool hasClosure(Node n)
+{
+  if (!n.getAttribute(HasClosureComputedAttr()))
+  {
+    bool hasC = false;
+    if (n.isClosure())
+    {
+      hasC = true;
+    }
+    else
+    {
+      for (auto i = n.begin(); i != n.end() && !hasC; ++i)
+      {
+        hasC = hasClosure(*i);
+      }
+    }
+    if (!hasC && n.hasOperator())
+    {
+      hasC = hasClosure(n.getOperator());
+    }
+    n.setAttribute(HasClosureAttr(), hasC);
+    n.setAttribute(HasClosureComputedAttr(), true);
+    return hasC;
+  }
+  return n.getAttribute(HasClosureAttr());
+}
+
+bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs)
+{
+  std::unordered_set<TNode> scope;
+  return getVariablesInternal(n, fvs, scope);
+}
+
+bool getFreeVariablesScope(TNode n,
+                           std::unordered_set<Node>& fvs,
+                           std::unordered_set<TNode>& scope)
+{
+  return getVariablesInternal(n, fvs, scope);
+}
+bool hasFreeVariablesScope(TNode n, std::unordered_set<TNode>& scope)
+{
+  std::unordered_set<Node> fvs;
+  return getVariablesInternal(n, fvs, scope, false);
+}
+
 bool getVariables(TNode n, std::unordered_set<TNode>& vs)
 {
   std::unordered_set<TNode> visited;
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 72ea03176..c3ee4b604 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -85,6 +85,16 @@ bool hasBoundVar(TNode n);
 bool hasFreeVar(TNode n);
 
 /**
+ * Returns true iff the node n contains a free variable, that is, a node
+ * of kind BOUND_VARIABLE that is not bound in n, or a BOUND_VARIABLE that
+ * is shadowed (e.g. it is bound twice in the same context).
+ * @param n The node under investigation
+ * @param wasShadow Set to true if n had a shadowed variable.
+ * @return true iff this node contains a free or shadowed variable.
+ */
+bool hasFreeOrShadowedVar(TNode n, bool& wasShadow);
+
+/**
  * Returns true iff the node n contains a closure, that is, a node
  * whose kind is FORALL, EXISTS, WITNESS, LAMBDA, or any other closure currently
  * supported.
@@ -98,27 +108,27 @@ bool hasClosure(Node n);
  * BOUND_VARIABLE that are not bound in n, adds these to fvs.
  * @param n The node under investigation
  * @param fvs The set which free variables are added to
- * @param computeFv If this flag is false, then we only return true/false and
- * do not add to fvs.
  * @return true iff this node contains a free variable.
  */
-bool getFreeVariables(TNode n,
-                      std::unordered_set<Node>& fvs,
-                      bool computeFv = true);
+bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs);
 /**
  * Get the free variables in n, that is, the subterms of n of kind
  * BOUND_VARIABLE that are not bound in n or occur in scope, adds these to fvs.
  * @param n The node under investigation
  * @param fvs The set which free variables are added to
  * @param scope The scope we are considering.
- * @param computeFv If this flag is false, then we only return true/false and
- * do not add to fvs.
  * @return true iff this node contains a free variable.
  */
 bool getFreeVariablesScope(TNode n,
                            std::unordered_set<Node>& fvs,
-                           std::unordered_set<TNode>& scope,
-                           bool computeFv = true);
+                           std::unordered_set<TNode>& scope);
+/**
+ * Return true if n has any free variables in the given scope.
+ * @param n The node under investigation
+ * @param scope The scope we are considering.
+ * @return true iff this node contains a free variable.
+ */
+bool hasFreeVariablesScope(TNode n, std::unordered_set<TNode>& scope);
 
 /**
  * Get all variables in n.
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 9c24dd690..8d066c1ba 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -190,16 +190,19 @@ void Assertions::addFormula(TNode n,
   // Ensure that it does not contain free variables
   if (maybeHasFv)
   {
-    if (expr::hasFreeVar(n))
+    bool wasShadow = false;
+    if (expr::hasFreeOrShadowedVar(n, wasShadow))
     {
+      std::string varType(wasShadow ? "shadowed" : "free");
       std::stringstream se;
       if (isFunDef)
       {
-        se << "Cannot process function definition with free variable.";
+        se << "Cannot process function definition with " << varType
+           << " variable.";
       }
       else
       {
-        se << "Cannot process assertion with free variable.";
+        se << "Cannot process assertion with " << varType << " variable.";
         if (language::isLangSygus(options().base.inputLanguage))
         {
           // Common misuse of SyGuS is to use top-level assert instead of