Extract filter_symbol_table method

Author: romainbrenguier

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -186,11 +186,30 @@ bool ci_lazy_methodst::operator()(
   }
 
   // Remove symbols for methods that were declared but never used:
-  symbol_tablet keep_symbols;
+  symbol_tablet keep_symbols = filter_symbol_table(
+    symbol_table, method_bytecode, methods_already_populated);
+
   // Manually keep @inflight_exception, as it is unused at this stage
   // but will become used when the `remove_exceptions` pass is run:
   keep_symbols.add(symbol_table.lookup_ref(INFLIGHT_EXCEPTION_VARIABLE_NAME));
 
+  debug() << "CI lazy methods: removed "
+          << symbol_table.symbols.size() - keep_symbols.symbols.size()
+          << " unreachable methods and globals" << eom;
+
+  symbol_table.swap(keep_symbols);
+  return false;
+}
+
+/// Only keep functions that have been converted and global variables that are
+/// used in these functions.
+/// \return new symbol table
+symbol_tablet ci_lazy_methodst::filter_symbol_table(
+  const symbol_tablet &symbol_table,
+  const method_bytecodet &method_bytecode,
+  const std::unordered_set<irep_idt> &methods_already_populated)
+{
+  symbol_tablet keep_symbols;
   for(const auto &sym : symbol_table.symbols)
   {
     // Don't keep global variables (unless they're gathered below from a
@@ -213,14 +232,7 @@ bool ci_lazy_methodst::operator()(
     }
     keep_symbols.add(sym.second);
   }
-
-  debug() << "CI lazy methods: removed "
-          << symbol_table.symbols.size() - keep_symbols.symbols.size()
-          << " unreachable methods and globals" << eom;
-
-  symbol_table.swap(keep_symbols);
-
-  return false;
+  return keep_symbols;
 }
 
 /// Look for virtual callsites with no candidate targets. If we have

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -194,6 +194,11 @@ class ci_lazy_methodst:public messaget
     std::unordered_set<irep_idt> &instantiated_classes,
     const std::unordered_set<exprt, irep_hash> &virtual_function_calls,
     symbol_tablet &symbol_table);
+
+  symbol_tablet filter_symbol_table(
+    const symbol_tablet &symbol_table,
+    const method_bytecodet &method_bytecode,
+    const std::unordered_set<irep_idt> &methods_already_populated);
 };
 
 #endif // CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H