find_symbols: support restriction to non-bound symbols

Adds a new symbol kind to distinguish bound from unbound ones. Add
documentation to all non-deprecated functions and clarify whether or not
bound symbols are included.

Author: tautschnig

src/ansi-c/goto_check_c.cpp

@@ -466,7 +466,7 @@ void goto_check_ct::invalidate(const exprt &lhs)
     for(auto it = assertions.begin(); it != assertions.end();)
     {
       if(
-        has_symbol_expr(it->second, lhs_id) ||
+        has_symbol_expr(it->second, lhs_id, false) ||
         has_subexpr(it->second, ID_dereference))
       {
         it = assertions.erase(it);

src/goto-symex/postcondition.cpp

@@ -167,7 +167,7 @@ bool postconditiont::is_used(
     for(const exprt &e :
         value_set.get_value_set(to_dereference_expr(expr).pointer(), ns))
     {
-      if(has_symbol_expr(get_original_name(e), identifier))
+      if(has_symbol_expr(get_original_name(e), identifier, false))
         return true;
     }
 

src/goto-symex/precondition.cpp

@@ -117,7 +117,7 @@ void preconditiont::compute_rec(exprt &dest)
     for(const exprt &e : value_sets.get_values(
           SSA_step.source.function_id, target, deref_expr.pointer()))
     {
-      if(has_symbol_expr(e, lhs_identifier))
+      if(has_symbol_expr(e, lhs_identifier, false))
       {
         may_alias = true;
         break;

src/util/find_symbols.cpp

@@ -23,8 +23,8 @@ enum class symbol_kindt
   F_TYPE_NON_PTR,
   /// Symbol expressions.
   F_EXPR,
-  /// Symbol expressions, but excluding bindings.
-  F_EXPR_NOT_BOUND,
+  /// Symbol expressions, but excluding bound variables.
+  F_EXPR_FREE,
   /// All of the above.
   F_ALL
 };
@@ -46,33 +46,77 @@ bool has_symbol(const exprt &src, const find_symbols_sett &symbols)
 static bool find_symbols(
   symbol_kindt,
   const typet &,
-  std::function<bool(const symbol_exprt &)>);
+  std::function<bool(const symbol_exprt &)>,
+  std::unordered_set<irep_idt> &bindings);
 
 static bool find_symbols(
   symbol_kindt kind,
   const exprt &src,
-  std::function<bool(const symbol_exprt &)> op)
+  std::function<bool(const symbol_exprt &)> op,
+  std::unordered_set<irep_idt> &bindings)
 {
+  if(kind == symbol_kindt::F_EXPR_FREE)
+  {
+    if(src.id() == ID_forall || src.id() == ID_exists || src.id() == ID_lambda)
+    {
+      const auto &binding_expr = to_binding_expr(src);
+      std::unordered_set<irep_idt> new_bindings{bindings};
+      for(const auto &v : binding_expr.variables())
+        new_bindings.insert(v.get_identifier());
+
+      if(!find_symbols(kind, binding_expr.where(), op, new_bindings))
+        return false;
+
+      return find_symbols(kind, binding_expr.type(), op, bindings);
+    }
+    else if(src.id() == ID_let)
+    {
+      const auto &let_expr = to_let_expr(src);
+      std::unordered_set<irep_idt> new_bindings{bindings};
+      for(const auto &v : let_expr.variables())
+        new_bindings.insert(v.get_identifier());
+
+      if(!find_symbols(kind, let_expr.where(), op, new_bindings))
+        return false;
+
+      if(!find_symbols(kind, let_expr.op1(), op, new_bindings))
+        return false;
+
+      return find_symbols(kind, let_expr.type(), op, bindings);
+    }
+  }
+
   forall_operands(it, src)
   {
-    if(!find_symbols(kind, *it, op))
+    if(!find_symbols(kind, *it, op, bindings))
       return false;
   }
 
-  if(!find_symbols(kind, src.type(), op))
+  if(!find_symbols(kind, src.type(), op, bindings))
     return false;
 
-  if(kind == symbol_kindt::F_ALL || kind == symbol_kindt::F_EXPR)
+  if(src.id() == ID_symbol)
   {
-    if(src.id() == ID_symbol && !op(to_symbol_expr(src)))
-      return false;
+    const symbol_exprt &s = to_symbol_expr(src);
+
+    if(kind == symbol_kindt::F_ALL || kind == symbol_kindt::F_EXPR)
+    {
+      if(!op(s))
+        return false;
+    }
+    else if(kind == symbol_kindt::F_EXPR_FREE)
+    {
+      if(bindings.find(s.get_identifier()) == bindings.end() && !op(s))
+        return false;
+    }
   }
 
   const irept &c_sizeof_type=src.find(ID_C_c_sizeof_type);
 
   if(
     c_sizeof_type.is_not_nil() &&
-    !find_symbols(kind, static_cast<const typet &>(c_sizeof_type), op))
+    !find_symbols(
+      kind, static_cast<const typet &>(c_sizeof_type), op, bindings))
   {
     return false;
   }
@@ -81,7 +125,7 @@ static bool find_symbols(
 
   if(
     va_arg_type.is_not_nil() &&
-    !find_symbols(kind, static_cast<const typet &>(va_arg_type), op))
+    !find_symbols(kind, static_cast<const typet &>(va_arg_type), op, bindings))
   {
     return false;
   }
@@ -92,20 +136,21 @@ static bool find_symbols(
 static bool find_symbols(
   symbol_kindt kind,
   const typet &src,
-  std::function<bool(const symbol_exprt &)> op)
+  std::function<bool(const symbol_exprt &)> op,
+  std::unordered_set<irep_idt> &bindings)
 {
   if(kind != symbol_kindt::F_TYPE_NON_PTR || src.id() != ID_pointer)
   {
     if(
       src.has_subtype() &&
-      !find_symbols(kind, to_type_with_subtype(src).subtype(), op))
+      !find_symbols(kind, to_type_with_subtype(src).subtype(), op, bindings))
     {
       return false;
     }
 
     for(const typet &subtype : to_type_with_subtypes(src).subtypes())
     {
-      if(!find_symbols(kind, subtype, op))
+      if(!find_symbols(kind, subtype, op, bindings))
         return false;
     }
 
@@ -126,26 +171,26 @@ static bool find_symbols(
 
     for(const auto &c : struct_union_type.components())
     {
-      if(!find_symbols(kind, c, op))
+      if(!find_symbols(kind, c, op, bindings))
         return false;
     }
   }
   else if(src.id()==ID_code)
   {
     const code_typet &code_type=to_code_type(src);
-    if(!find_symbols(kind, code_type.return_type(), op))
+    if(!find_symbols(kind, code_type.return_type(), op, bindings))
       return false;
 
     for(const auto &p : code_type.parameters())
     {
-      if(!find_symbols(kind, p, op))
+      if(!find_symbols(kind, p, op, bindings))
         return false;
     }
   }
   else if(src.id()==ID_array)
   {
     // do the size -- the subtype is already done
-    if(!find_symbols(kind, to_array_type(src).size(), op))
+    if(!find_symbols(kind, to_array_type(src).size(), op, bindings))
       return false;
   }
   else if(
@@ -172,6 +217,24 @@ static bool find_symbols(
   return true;
 }
 
+static bool find_symbols(
+  symbol_kindt kind,
+  const typet &type,
+  std::function<bool(const symbol_exprt &)> op)
+{
+  std::unordered_set<irep_idt> bindings;
+  return find_symbols(kind, type, op, bindings);
+}
+
+static bool find_symbols(
+  symbol_kindt kind,
+  const exprt &src,
+  std::function<bool(const symbol_exprt &)> op)
+{
+  std::unordered_set<irep_idt> bindings;
+  return find_symbols(kind, src, op, bindings);
+}
+
 void find_symbols(const exprt &src, std::set<symbol_exprt> &dest)
 {
   find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
@@ -180,11 +243,17 @@ void find_symbols(const exprt &src, std::set<symbol_exprt> &dest)
   });
 }
 
-bool has_symbol_expr(const exprt &src, const irep_idt &identifier)
+bool has_symbol_expr(
+  const exprt &src,
+  const irep_idt &identifier,
+  bool include_bound_symbols)
 {
-  return !find_symbols(symbol_kindt::F_EXPR, src, [&identifier](const symbol_exprt &e) {
-    return e.get_identifier() != identifier;
-  });
+  return !find_symbols(
+    include_bound_symbols ? symbol_kindt::F_EXPR : symbol_kindt::F_EXPR_FREE,
+    src,
+    [&identifier](const symbol_exprt &e) {
+      return e.get_identifier() != identifier;
+    });
 }
 
 void find_type_symbols(const exprt &src, find_symbols_sett &dest)

src/util/find_symbols.h

@@ -24,15 +24,20 @@ class typet;
 typedef std::unordered_set<irep_idt> find_symbols_sett;
 
 /// Returns true if one of the symbol expressions in \p src has identifier
-/// \p identifier.
-bool has_symbol_expr(const exprt &src, const irep_idt &identifier);
+/// \p identifier; if
+/// \p include_bound_symbols is true, then bindings are included in the search.
+bool has_symbol_expr(
+  const exprt &src,
+  const irep_idt &identifier,
+  bool include_bound_symbols);
 
 DEPRECATED(SINCE(2022, 3, 14, "use find_symbols"))
 /// Add to the set \p dest the sub-expressions of \p src with id ID_symbol or
 /// ID_next_symbol
 void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest);
 
-/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol.
+/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol, for
+/// both free and bound variables.
 void find_symbols(const exprt &src, find_symbols_sett &dest);
 
 /// \return set of sub-expressions of the expressions contained in the range
@@ -49,20 +54,23 @@ find_symbols_sett find_symbols_or_nexts(iteratort begin, iteratort end)
   return result;
 }
 
-/// Find sub expressions with id ID_symbol
+/// Find sub expressions with id ID_symbol, considering both free and bound
+/// variables.
 void find_symbols(
   const exprt &src,
   std::set<symbol_exprt> &dest);
 
-/// Find sub expressions with id ID_symbol
+/// Find sub expressions with id ID_symbol, considering both free and bound
+/// variables.
 inline std::set<symbol_exprt> find_symbols(const exprt &src)
 {
   std::set<symbol_exprt> syms;
   find_symbols(src, syms);
   return syms;
 }
 
-/// Find identifiers of the sub expressions with id ID_symbol
+/// Find identifiers of the sub expressions with id ID_symbol, considering both
+/// free and bound variables.
 inline find_symbols_sett find_symbol_identifiers(const exprt &src)
 {
   find_symbols_sett identifiers;
@@ -76,26 +84,36 @@ bool has_symbol(
   const exprt &src,
   const find_symbols_sett &symbols);
 
+/// Collect all type tags contained in \p src and add them to \p dest.
 void find_type_symbols(
   const typet &src,
   find_symbols_sett &dest);
 
+/// Collect all type tags contained in \p src and add them to \p dest.
 void find_type_symbols(
   const exprt &src,
   find_symbols_sett &dest);
 
+/// Collect type tags contained in \p src when the expression of such a type is
+/// not a pointer, and add them to \p dest.
 void find_non_pointer_type_symbols(
   const typet &src,
   find_symbols_sett &dest);
 
+/// Collect type tags contained in \p src when the expression of such a type is
+/// not a pointer, and add them to \p dest.
 void find_non_pointer_type_symbols(
   const exprt &src,
   find_symbols_sett &dest);
 
+/// Find identifiers of the sub expressions with id ID_symbol, considering both
+/// free and bound variables, as well as any type tags.
 void find_type_and_expr_symbols(
   const typet &src,
   find_symbols_sett &dest);
 
+/// Find identifiers of the sub expressions with id ID_symbol, considering both
+/// free and bound variables, as well as any type tags.
 void find_type_and_expr_symbols(
   const exprt &src,
   find_symbols_sett &dest);