Merge pull request #4806 from romainbrenguier/clean-up/find-symbols

Clean-up find_symbols

Author: romainbrenguier

src/ansi-c/expr2c.cpp

@@ -112,8 +112,7 @@ static std::string clean_identifier(const irep_idt &id)
 
 void expr2ct::get_shorthands(const exprt &expr)
 {
-  find_symbols_sett symbols;
-  find_symbols(expr, symbols);
+  const std::unordered_set<irep_idt> symbols = find_symbol_identifiers(expr);
 
   // avoid renaming parameters, if possible
   for(const auto &symbol_id : symbols)

src/goto-instrument/accelerate/accelerate.cpp

@@ -392,11 +392,11 @@ void acceleratet::add_dirty_checks()
     find_symbols_sett read;
 
     if(it->has_condition())
-      find_symbols(it->get_condition(), read);
+      find_symbols_or_nexts(it->get_condition(), read);
 
     if(it->is_assign())
     {
-      find_symbols(it->get_assign().rhs(), read);
+      find_symbols_or_nexts(it->get_assign().rhs(), read);
     }
 
     for(find_symbols_sett::iterator jt=read.begin();

src/goto-instrument/accelerate/acceleration_utils.cpp

@@ -211,23 +211,15 @@ void acceleration_utilst::stash_variables(
   expr_sett modified,
   substitutiont &substitution)
 {
-  find_symbols_sett vars;
-
-  for(expr_sett::iterator it=modified.begin();
-      it!=modified.end();
-      ++it)
-  {
-    find_symbols(*it, vars);
-  }
-
-  irep_idt loop_counter_name=to_symbol_expr(loop_counter).get_identifier();
+  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);
 
-  for(find_symbols_sett::iterator it=vars.begin();
-      it!=vars.end();
-      ++it)
+  for(const irep_idt &symbol : vars)
   {
-    const symbolt &orig = symbol_table.lookup_ref(*it);
+    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());

src/goto-instrument/accelerate/polynomial_accelerator.cpp

@@ -752,23 +752,14 @@ void polynomial_acceleratort::stash_variables(
   expr_sett modified,
   substitutiont &substitution)
 {
-  find_symbols_sett vars;
-
-  for(expr_sett::iterator it=modified.begin();
-      it!=modified.end();
-      ++it)
-  {
-    find_symbols(*it, vars);
-  }
-
+  find_symbols_sett vars =
+    find_symbols_or_nexts(modified.begin(), modified.end());
   irep_idt loop_counter_name=to_symbol_expr(loop_counter).get_identifier();
   vars.erase(loop_counter_name);
 
-  for(find_symbols_sett::iterator it=vars.begin();
-      it!=vars.end();
-      ++it)
+  for(const irep_idt &id : vars)
   {
-    const symbolt &orig = symbol_table.lookup_ref(*it);
+    const symbolt &orig = symbol_table.lookup_ref(id);
     symbolt stashed_sym=utils.fresh_symbol("polynomial::stash", orig.type);
     substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
     program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());

src/goto-instrument/concurrency.cpp

@@ -78,34 +78,22 @@ class concurrency_instrumentationt
 
 void concurrency_instrumentationt::instrument(exprt &expr)
 {
-  std::set<exprt> symbols;
-
-  find_symbols(expr, symbols);
-
   replace_symbolt replace_symbol;
 
-  for(std::set<exprt>::const_iterator
-      s_it=symbols.begin();
-      s_it!=symbols.end();
-      s_it++)
+  for(const symbol_exprt &s : find_symbols(expr))
   {
-    if(s_it->id()==ID_symbol)
-    {
-      const symbol_exprt &s = to_symbol_expr(*s_it);
+    shared_varst::const_iterator v_it = shared_vars.find(s.get_identifier());
 
-      shared_varst::const_iterator v_it = shared_vars.find(s.get_identifier());
-
-      if(v_it!=shared_vars.end())
-      {
-        UNIMPLEMENTED;
-        // not yet done: neither array_symbol nor w_index_symbol are actually
-        // initialized anywhere
-        const shared_vart &shared_var = v_it->second;
-        const index_exprt new_expr(
-          *shared_var.array_symbol, *shared_var.w_index_symbol);
-
-        replace_symbol.insert(s, new_expr);
-      }
+    if(v_it != shared_vars.end())
+    {
+      UNIMPLEMENTED;
+      // not yet done: neither array_symbol nor w_index_symbol are actually
+      // initialized anywhere
+      const shared_vart &shared_var = v_it->second;
+      const index_exprt new_expr(
+        *shared_var.array_symbol, *shared_var.w_index_symbol);
+
+      replace_symbol.insert(s, new_expr);
     }
   }
 }
@@ -143,42 +131,29 @@ void concurrency_instrumentationt::instrument(
 
 void concurrency_instrumentationt::collect(const exprt &expr)
 {
-  std::set<exprt> symbols;
+  for(const auto &identifier : find_symbol_identifiers(expr))
+  {
+    namespacet ns(symbol_table);
+    const symbolt &symbol = ns.lookup(identifier);
 
-  find_symbols(expr, symbols);
+    if(!symbol.is_state_var)
+      continue;
 
-  for(std::set<exprt>::const_iterator
-      s_it=symbols.begin();
-      s_it!=symbols.end();
-      s_it++)
-  {
-    if(s_it->id()==ID_symbol)
+    if(symbol.is_thread_local)
     {
-      const irep_idt identifier=
-        to_symbol_expr(*s_it).get_identifier();
-
-      namespacet ns(symbol_table);
-      const symbolt &symbol=ns.lookup(identifier);
+      if(thread_local_vars.find(identifier) != thread_local_vars.end())
+        continue;
 
-      if(!symbol.is_state_var)
+      thread_local_vart &thread_local_var = thread_local_vars[identifier];
+      thread_local_var.type = symbol.type;
+    }
+    else
+    {
+      if(shared_vars.find(identifier) != shared_vars.end())
         continue;
 
-      if(symbol.is_thread_local)
-      {
-        if(thread_local_vars.find(identifier)!=thread_local_vars.end())
-          continue;
-
-        thread_local_vart &thread_local_var=thread_local_vars[identifier];
-        thread_local_var.type=symbol.type;
-      }
-      else
-      {
-        if(shared_vars.find(identifier)!=shared_vars.end())
-          continue;
-
-        shared_vart &shared_var=shared_vars[identifier];
-        shared_var.type=symbol.type;
-      }
+      shared_vart &shared_var = shared_vars[identifier];
+      shared_var.type = symbol.type;
     }
   }
 }

src/goto-instrument/dump_c.cpp

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

src/goto-instrument/full_slicer.cpp

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

src/goto-programs/goto_program.cpp

@@ -716,7 +716,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(e, typetags);
+    find_symbols_or_nexts(e, typetags);
     const symbolt *symbol;
     for(const auto &identifier : typetags)
     {

src/goto-symex/postcondition.cpp

@@ -160,16 +160,12 @@ bool postconditiont::is_used(
   else if(expr.id()==ID_dereference)
   {
     // aliasing may happen here
-    std::vector<exprt> expr_set =
+    const std::vector<exprt> expr_set =
       value_set.get_value_set(to_dereference_expr(expr).pointer(), ns);
-    std::unordered_set<irep_idt> symbols;
-
-    for(const exprt &e : expr_set)
-    {
-      const exprt tmp = get_original_name(e);
-      find_symbols(tmp, symbols);
-    }
-
+    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();
   }
   else

src/goto-symex/precondition.cpp

@@ -114,10 +114,8 @@ void preconditiont::compute_rec(exprt &dest)
 
     const std::vector<exprt> expr_set = value_sets.get_values(
       SSA_step.source.function_id, target, deref_expr.pointer());
-    std::unordered_set<irep_idt> symbols;
-
-    for(const exprt &e : expr_set)
-      find_symbols(e, symbols);
+    const std::unordered_set<irep_idt> symbols =
+      find_symbols_or_nexts(expr_set.begin(), expr_set.end());
 
     if(symbols.find(lhs_identifier)!=symbols.end())
     {

src/goto-symex/symex_dead.cpp

@@ -32,7 +32,7 @@ void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)
 
   const exprt fields = state.field_sensitivity.get_fields(ns, state, ssa);
   find_symbols_sett fields_set;
-  find_symbols(fields, fields_set);
+  find_symbols_or_nexts(fields, fields_set);
 
   for(const irep_idt &l1_identifier : fields_set)
   {

src/goto-symex/symex_decl.cpp

@@ -65,10 +65,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
 
   // L2 renaming
   const exprt fields = state.field_sensitivity.get_fields(ns, state, ssa);
-  std::set<symbol_exprt> fields_set;
-  find_symbols(fields, fields_set);
-
-  for(const auto &l1_symbol : fields_set)
+  for(const auto &l1_symbol : find_symbols(fields))
   {
     ssa_exprt field_ssa = to_ssa_expr(l1_symbol);
     std::size_t field_generation =

src/solvers/refinement/refine_arrays.cpp

@@ -111,9 +111,7 @@ void bv_refinementt::freeze_lazy_constraints()
 
   for(const auto &constraint : lazy_array_constraints)
   {
-    std::set<symbol_exprt> symbols_in_constraint;
-    find_symbols(constraint.lazy, symbols_in_constraint);
-    for(const auto &symbol : symbols_in_constraint)
+    for(const auto &symbol : find_symbols(constraint.lazy))
     {
       const bvt bv=convert_bv(symbol);
       forall_literals(b_it, bv)

src/util/find_symbols.cpp

@@ -8,14 +8,14 @@ Author: Daniel Kroening, [email protected]
 
 #include "find_symbols.h"
 
-#include "std_types.h"
+#include "expr_iterator.h"
+#include "range.h"
 #include "std_expr.h"
+#include "std_types.h"
 
 enum class kindt { F_TYPE, F_TYPE_NON_PTR, F_EXPR, F_BOTH };
 
-void find_symbols(
-  const exprt &src,
-  find_symbols_sett &dest)
+void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
 {
   find_symbols(src, dest, true, true);
 }
@@ -81,6 +81,23 @@ void find_symbols(
   });
 }
 
+std::set<symbol_exprt> find_symbols(const exprt &src)
+{
+  return make_range(src.depth_begin(), src.depth_end())
+    .filter([](const exprt &e) { return e.id() == ID_symbol; })
+    .map([](const exprt &e) { return to_symbol_expr(e); });
+}
+
+std::unordered_set<irep_idt> find_symbol_identifiers(const exprt &src)
+{
+  std::unordered_set<irep_idt> result;
+  src.visit_pre([&](const exprt &e) {
+    if(e.id() == ID_symbol)
+      result.insert(to_symbol_expr(e).get_identifier());
+  });
+  return result;
+}
+
 void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest);
 
 void find_symbols(kindt kind, const exprt &src, find_symbols_sett &dest)

src/util/find_symbols.h

@@ -10,9 +10,11 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_FIND_SYMBOLS_H
 #define CPROVER_UTIL_FIND_SYMBOLS_H
 
+#include <algorithm>
 #include <set>
 #include <unordered_set>
 
+#include "deprecate.h"
 #include "irep.h"
 
 class exprt;
@@ -21,24 +23,50 @@ class typet;
 
 typedef std::unordered_set<irep_idt> find_symbols_sett;
 
-void find_symbols(
-  const exprt &src,
-  find_symbols_sett &dest);
-
+/// 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);
+
+/// \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>
+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); });
+  return result;
+}
+
+/// 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,
   bool next);
 
+/// Find sub expressions with id ID_symbol or ID_next_symbol
+DEPRECATED(SINCE(2019, 06, 17, "Unused"))
 void find_symbols(
   const exprt &src,
   std::set<exprt> &dest);
 
+/// Find sub expressions with id ID_symbol
 void find_symbols(
   const exprt &src,
   std::set<symbol_exprt> &dest);
 
+/// Find sub expressions with id ID_symbol
+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);
+
+/// \return true if one of the symbols in \p src is present in \p symbols
 bool has_symbol(
   const exprt &src,
   const find_symbols_sett &symbols);