Make has_symbol configurable and deprecate the existing has_symbol

The existing code did not permit configuring what kinds of symbols are
to be found. It had a single user within the code base, and even that
one was not a good use of it for it constructed a single-element set.

The new implementation does not yet make use of potential efficiency
advantages of "has a symbol" over "find the existing symbols," but such
improvements will be done based on further cleanup of find_symbols code.

Author: tautschnig

src/ansi-c/goto_check_c.cpp

@@ -461,12 +461,12 @@ void goto_check_ct::invalidate(const exprt &lhs)
   else if(lhs.id() == ID_symbol)
   {
     // clear all assertions about 'symbol'
-    find_symbols_sett find_symbols_set{to_symbol_expr(lhs).get_identifier()};
+    const irep_idt &lhs_id = to_symbol_expr(lhs).get_identifier();
 
     for(auto it = assertions.begin(); it != assertions.end();)
     {
       if(
-        has_symbol(it->second, find_symbols_set) ||
+        has_symbol(it->second, lhs_id, kindt::F_EXPR) ||
         has_subexpr(it->second, ID_dereference))
       {
         it = assertions.erase(it);

src/goto-symex/postcondition.cpp

@@ -164,13 +164,16 @@ bool postconditiont::is_used(
   else if(expr.id()==ID_dereference)
   {
     // aliasing may happen here
-    const std::vector<exprt> expr_set =
-      value_set.get_value_set(to_dereference_expr(expr).pointer(), ns);
-    const auto original_names = make_range(expr_set).map(
-      [](const exprt &e) { return get_original_name(e); });
-    const std::unordered_set<irep_idt> symbols =
-      find_symbols_or_nexts(original_names.begin(), original_names.end());
-    return symbols.find(identifier)!=symbols.end();
+    for(const exprt &e :
+        value_set.get_value_set(to_dereference_expr(expr).pointer(), ns))
+    {
+      if(has_symbol(get_original_name(e), identifier, kindt::F_BOTH))
+      {
+        return true;
+      }
+    }
+
+    return false;
   }
   else
     forall_operands(it, expr)

src/goto-symex/precondition.cpp

@@ -113,14 +113,19 @@ void preconditiont::compute_rec(exprt &dest)
 
     // aliasing may happen here
 
-    const std::vector<exprt> expr_set = value_sets.get_values(
-      SSA_step.source.function_id, target, deref_expr.pointer());
-    const std::unordered_set<irep_idt> symbols =
-      find_symbols_or_nexts(expr_set.begin(), expr_set.end());
+    bool may_alias = false;
+    for(const exprt &e : value_sets.get_values(
+          SSA_step.source.function_id, target, deref_expr.pointer()))
+    {
+      if(has_symbol(e, lhs_identifier, kindt::F_BOTH))
+      {
+        may_alias = true;
+        break;
+      }
+    }
 
-    if(symbols.find(lhs_identifier)!=symbols.end())
+    if(may_alias)
     {
-      // may alias!
       exprt tmp;
       tmp.swap(deref_expr.pointer());
       dereference(SSA_step.source.function_id, target, tmp, ns, value_sets);

src/util/find_symbols.cpp

@@ -13,8 +13,6 @@ Author: Daniel Kroening, [email protected]
 #include "range.h"
 #include "std_expr.h"
 
-enum class kindt { F_TYPE, F_TYPE_NON_PTR, F_EXPR, F_BOTH };
-
 void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
 {
   find_symbols(src, dest, true, true);
@@ -173,6 +171,13 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
   }
 }
 
+bool has_symbol(const exprt &src, const irep_idt &identifier, kindt kind)
+{
+  find_symbols_sett tmp_dest;
+  find_symbols(kind, src, tmp_dest);
+  return tmp_dest.find(identifier) != tmp_dest.end();
+}
+
 void find_type_symbols(const exprt &src, find_symbols_sett &dest)
 {
   find_symbols(kindt::F_TYPE, src, dest);

src/util/find_symbols.h

@@ -10,18 +10,37 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_FIND_SYMBOLS_H
 #define CPROVER_UTIL_FIND_SYMBOLS_H
 
+#include "deprecate.h"
+#include "irep.h"
+
 #include <algorithm>
 #include <set>
 #include <unordered_set>
 
-#include "irep.h"
-
 class exprt;
 class symbol_exprt;
 class typet;
 
 typedef std::unordered_set<irep_idt> find_symbols_sett;
 
+/// Kinds of symbols to be considered by \ref has_symbol or \ref find_symbols.
+enum class kindt
+{
+  /// Struct, union, or enum tag symbols.
+  F_TYPE,
+  /// Struct, union, or enum tag symbols when the expression using them is not a
+  /// pointer.
+  F_TYPE_NON_PTR,
+  /// Symbol expressions.
+  F_EXPR,
+  /// Current or next-state symbol expressions.
+  F_BOTH,
+};
+
+/// Returns true if one of the symbols in \p src with identifier \p identifier
+/// is of kind \p kind.
+bool has_symbol(const exprt &src, const irep_idt &identifier, kindt kind);
+
 /// 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);
@@ -59,6 +78,7 @@ std::set<symbol_exprt> find_symbols(const exprt &src);
 /// Find identifiers of the sub expressions with id ID_symbol
 std::unordered_set<irep_idt> find_symbol_identifiers(const exprt &src);
 
+DEPRECATED(SINCE(2022, 3, 14, "use has_symbol(exprt, irep_idt, symbol_kindt)"))
 /// \return true if one of the symbols in \p src is present in \p symbols
 bool has_symbol(
   const exprt &src,