Merge pull request #6727 from tautschnig/cleanup/find_symbols

Cleanup find_symbols API

Author: tautschnig

src/ansi-c/expr2c.cpp

@@ -1663,9 +1663,6 @@ std::string expr2ct::convert_symbol(const exprt &src)
     #endif
   }
 
-  if(src.id()==ID_next_symbol)
-    dest="NEXT("+dest+")";
-
   return dest;
 }
 
@@ -3850,9 +3847,6 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_symbol)
     return convert_symbol(src);
 
-  else if(src.id()==ID_next_symbol)
-    return convert_symbol(src);
-
   else if(src.id()==ID_nondet_symbol)
     return convert_nondet_symbol(to_nondet_symbol_expr(src));
 

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_expr(it->second, lhs_id, false) ||
         has_subexpr(it->second, ID_dereference))
       {
         it = assertions.erase(it);

src/goto-instrument/accelerate/accelerate.cpp

@@ -383,21 +383,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->condition(), read);
+      find_symbols(it->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-programs/slice_global_inits.cpp

@@ -64,7 +64,7 @@ void slice_global_inits(
     for(const auto &i : it->second.body.instructions)
     {
       i.apply([&symbols_to_keep](const exprt &expr) {
-        find_symbols(expr, symbols_to_keep, true, false);
+        find_symbols(expr, symbols_to_keep);
       });
     }
   }
@@ -103,7 +103,7 @@ void slice_global_inits(
           symbols_to_keep.find(id) != symbols_to_keep.end())
         {
           fixed_point_reached = false;
-          find_symbols(instruction.assign_rhs(), symbols_to_keep, true, false);
+          find_symbols(instruction.assign_rhs(), symbols_to_keep);
           *seen_it = true;
         }
       }

src/goto-symex/postcondition.cpp

@@ -164,13 +164,14 @@ 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_expr(get_original_name(e), identifier, false))
+        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_expr(e, lhs_identifier, false))
+      {
+        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);