Deprecate find_symbols_or_nexts

Make the two Boolean parameters of find_symbols(expr, set, bool, bool)
optional so that each existing users can safely use that function
(or another, even more suitable, function) instead.

Author: tautschnig

src/goto-instrument/accelerate/accelerate.cpp

@@ -379,21 +379,16 @@ void acceleratet::add_dirty_checks()
 
     // Find which symbols are read, i.e. those appearing in a guard or on
     // the right hand side of an assignment.  Assume each is not dirty.
-    find_symbols_sett read;
+    std::set<symbol_exprt> read;
 
     if(it->has_condition())
-      find_symbols_or_nexts(it->get_condition(), read);
+      find_symbols(it->get_condition(), read);
 
     if(it->is_assign())
-    {
-      find_symbols_or_nexts(it->assign_rhs(), read);
-    }
+      find_symbols(it->assign_rhs(), read);
 
-    for(find_symbols_sett::iterator jt=read.begin();
-        jt!=read.end();
-        ++jt)
+    for(const auto &var : read)
     {
-      const exprt &var=ns.lookup(*jt).symbol_expr();
       expr_mapt::iterator dirty_var=dirty_vars_map.find(var);
 
       if(dirty_var==dirty_vars_map.end())

src/goto-instrument/accelerate/acceleration_utils.cpp

@@ -198,18 +198,19 @@ void acceleration_utilst::stash_variables(
   expr_sett modified,
   substitutiont &substitution)
 {
-  find_symbols_sett vars =
-    find_symbols_or_nexts(modified.begin(), modified.end());
-  const irep_idt &loop_counter_name =
-    to_symbol_expr(loop_counter).get_identifier();
-  vars.erase(loop_counter_name);
+  const symbol_exprt &loop_counter_sym = to_symbol_expr(loop_counter);
 
-  for(const irep_idt &symbol : vars)
+  std::set<symbol_exprt> vars;
+  for(const exprt &expr : modified)
+    find_symbols(expr, vars);
+
+  vars.erase(loop_counter_sym);
+
+  for(const symbol_exprt &orig : vars)
   {
-    const symbolt &orig = symbol_table.lookup_ref(symbol);
-    symbolt stashed_sym=fresh_symbol("polynomial::stash", orig.type);
-    substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
-    program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());
+    symbolt stashed_sym = fresh_symbol("polynomial::stash", orig.type());
+    substitution[orig] = stashed_sym.symbol_expr();
+    program.assign(stashed_sym.symbol_expr(), orig);
   }
 }
 

src/goto-instrument/dump_c.cpp

@@ -913,9 +913,7 @@ void dump_ct::convert_global_variable(
 
   code_frontend_declt d(symbol.symbol_expr());
 
-  find_symbols_sett syms;
-  if(symbol.value.is_not_nil())
-    find_symbols_or_nexts(symbol.value, syms);
+  find_symbols_sett syms = find_symbol_identifiers(symbol.value);
 
   // add a tentative declaration to cater for symbols in the initializer
   // relying on it this symbol

src/goto-instrument/full_slicer.cpp

@@ -62,7 +62,7 @@ void full_slicert::add_decl_dead(
 
   find_symbols_sett syms;
 
-  node.PC->apply([&syms](const exprt &e) { find_symbols_or_nexts(e, syms); });
+  node.PC->apply([&syms](const exprt &e) { find_symbols(e, syms); });
 
   for(find_symbols_sett::const_iterator
       it=syms.begin();

src/goto-programs/goto_program.cpp

@@ -760,8 +760,7 @@ void goto_programt::instructiont::validate(
 
   auto expr_symbol_finder = [&](const exprt &e) {
     find_symbols_sett typetags;
-    find_type_symbols(e.type(), typetags);
-    find_symbols_or_nexts(e, typetags);
+    find_type_and_expr_symbols(e, typetags);
     const symbolt *symbol;
     for(const auto &identifier : typetags)
     {
@@ -873,7 +872,7 @@ void goto_programt::instructiont::validate(
       "assert instruction should not have a target",
       source_location());
 
-    std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
+    expr_symbol_finder(guard);
     std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
     break;
   case OTHER:
@@ -940,7 +939,7 @@ void goto_programt::instructiont::validate(
       "function call instruction should contain a call statement",
       source_location());
 
-    std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder);
+    expr_symbol_finder(code);
     std::for_each(code.depth_begin(), code.depth_end(), type_finder);
     break;
   case THROW:

src/goto-symex/postcondition.cpp

@@ -164,12 +164,13 @@ 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());
+    find_symbols_sett symbols;
+    for(const exprt &e :
+        value_set.get_value_set(to_dereference_expr(expr).pointer(), ns))
+    {
+      find_symbols(get_original_name(e), symbols);
+    }
+
     return symbols.find(identifier)!=symbols.end();
   }
   else

src/goto-symex/precondition.cpp

@@ -113,10 +113,12 @@ 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());
+    find_symbols_sett symbols;
+    for(const exprt &e : value_sets.get_values(
+          SSA_step.source.function_id, target, deref_expr.pointer()))
+    {
+      find_symbols(e, symbols);
+    }
 
     if(symbols.find(lhs_identifier)!=symbols.end())
     {

src/util/find_symbols.cpp

@@ -23,25 +23,6 @@ enum class kindt
   F_ALL
 };
 
-void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
-{
-  find_symbols(src, dest, true, true);
-}
-
-void find_symbols(
-  const exprt &src,
-  find_symbols_sett &dest,
-  bool current,
-  bool next)
-{
-  src.visit_pre([&dest, current, next](const exprt &e) {
-    if(e.id() == ID_symbol && current)
-      dest.insert(to_symbol_expr(e).get_identifier());
-    else if(e.id() == ID_next_symbol && next)
-      dest.insert(e.get(ID_identifier));
-  });
-}
-
 bool has_symbol(
   const exprt &src,
   const find_symbols_sett &symbols,
@@ -218,3 +199,25 @@ void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest)
 {
   find_symbols(kindt::F_ALL, src, dest);
 }
+
+void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
+{
+  find_symbols(kindt::F_EXPR_BOTH, src, dest);
+}
+
+void find_symbols(
+  const exprt &src,
+  find_symbols_sett &dest,
+  bool current,
+  bool next)
+{
+  if(current)
+  {
+    if(next)
+      find_symbols(kindt::F_EXPR_BOTH, src, dest);
+    else
+      find_symbols(kindt::F_EXPR_CURRENT, src, dest);
+  }
+  else if(next)
+    find_symbols(kindt::F_EXPR_NEXT, src, dest);
+}

src/util/find_symbols.h

@@ -23,21 +23,30 @@ class typet;
 
 typedef std::unordered_set<irep_idt> find_symbols_sett;
 
+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 if
+/// \p current is true, and ID_next_symbol if \p next is true
+void find_symbols(
+  const exprt &src,
+  find_symbols_sett &dest,
+  bool current = true,
+  bool next = true);
+
 /// \return set of sub-expressions of the expressions contained in the range
 ///   defined by \p begin and \p end which have id ID_symbol or ID_next_symbol
 template <typename iteratort>
+DEPRECATED(SINCE(2022, 3, 14, "use find_symbols and a local iteration"))
 find_symbols_sett find_symbols_or_nexts(iteratort begin, iteratort end)
 {
   static_assert(
     std::is_base_of<exprt, typename iteratort::value_type>::value,
     "find_symbols takes exprt iterators as arguments");
   find_symbols_sett result;
-  std::for_each(
-    begin, end, [&](const exprt &e) { find_symbols_or_nexts(e, result); });
+  std::for_each(begin, end, [&](const exprt &e) { find_symbols(e, result); });
   return result;
 }