Remove unnecessary includes

.github/workflows/pull-request-checks.yaml

@@ -785,6 +785,33 @@ jobs:
       - name: Smoke test goto-analyzer
         run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc goto-analyzer /mnt/smoke/test.goto --unreachable-functions
 
+  include-what-you-use:
+    runs-on: ubuntu-22.04
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison iwyu
+      - name: Configure using CMake
+        run: |
+          mkdir build
+          cd build
+          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
+      - name: Run include-what-you-use
+        run: |
+          iwyu_tool -p build/compile_commands.json -j2 | tee includes.txt
+          if sed '/minisat2-src/,/^--$/d' includes.txt | grep '^- ' -B1 ; then
+            echo "Unnecessary includes found. Use '// IWYU pragma: keep' to override this."
+            exit 1
+          fi
+
   codecov-coverage-report:
     runs-on: ubuntu-20.04
     steps:

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -43,7 +43,7 @@ Author: Daniel Kroening, [email protected]
 #include <linking/static_lifetime_init.h>
 
 #include <cstdlib> // exit()
-#include <fstream>
+#include <fstream> // IWYU pragma: keep
 #include <iostream>
 #include <memory>
 

jbmc/src/java_bytecode/character_refine_preprocess.cpp

@@ -19,6 +19,8 @@ Date:   March 2017
 #include <util/bitvector_expr.h>
 #include <util/std_expr.h>
 
+#include <goto-programs/goto_instruction_code.h>
+
 /// converts based on a function on expressions
 /// \param expr_function: A reference to a function on expressions
 /// \param target: A position in a goto program

jbmc/src/java_bytecode/character_refine_preprocess.h

@@ -20,13 +20,13 @@ Date:   March 2017
 #ifndef CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H
 #define CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H
 
-#include <goto-programs/goto_instruction_code.h>
-
 #include <util/mp_arith.h>
-#include <util/std_code.h>
+#include <util/std_code_base.h>
 
 #include <unordered_map>
 
+class code_function_callt;
+
 class character_refine_preprocesst
 {
 public:

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -7,17 +7,19 @@ Author: Diffblue Ltd.
 \*******************************************************************/
 
 #include "ci_lazy_methods.h"
-#include "java_bytecode_language.h"
-#include "java_class_loader.h"
-#include "java_entry_point.h"
-#include "remove_exceptions.h"
 
 #include <util/expr_iterator.h>
 #include <util/namespace.h>
 #include <util/suffix.h>
+#include <util/symbol_table.h>
 
 #include <goto-programs/resolve_inherited_component.h>
 
+#include "java_bytecode_language.h"
+#include "java_class_loader.h"
+#include "java_entry_point.h"
+#include "remove_exceptions.h"
+
 /// Constructor for lazy-method loading
 /// \param symbol_table: the symbol table to use
 /// \param main_class: identifier of the entry point / main class
@@ -34,7 +36,7 @@ Author: Diffblue Ltd.
 ///   these method bodies are produced internally, rather than generated from
 ///   Java bytecode.
 ci_lazy_methodst::ci_lazy_methodst(
-  const symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   const irep_idt &main_class,
   const std::vector<irep_idt> &main_jar_classes,
   const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
@@ -96,7 +98,7 @@ static bool references_class_model(const exprt &expr)
 /// \param message_handler: the message handler to use for output
 /// \return Returns false on success
 bool ci_lazy_methodst::operator()(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   method_bytecodet &method_bytecode,
   const method_convertert &method_converter,
   message_handlert &message_handler)
@@ -221,7 +223,16 @@ bool ci_lazy_methodst::operator()(
               << symbol_table.symbols.size() - keep_symbols.symbols.size()
               << " unreachable methods and globals" << messaget::eom;
 
-  symbol_table.swap(keep_symbols);
+  auto sorted_to_keep = keep_symbols.sorted_symbol_names();
+  auto all_sorted = symbol_table.sorted_symbol_names();
+  auto it = sorted_to_keep.cbegin();
+  for(const auto &id : all_sorted)
+  {
+    if(it == sorted_to_keep.cend() || id != *it)
+      symbol_table.remove(id);
+    else
+      ++it;
+  }
 
   return false;
 }
@@ -238,7 +249,7 @@ bool ci_lazy_methodst::handle_virtual_methods_with_no_callees(
   std::unordered_set<irep_idt> &instantiated_classes,
   const std::unordered_set<class_method_descriptor_exprt, irep_hash>
     &virtual_functions,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   ci_lazy_methods_neededt lazy_methods_loader(
     methods_to_convert_later,
@@ -321,7 +332,7 @@ ci_lazy_methodst::convert_and_analyze_method(
   std::unordered_set<irep_idt> &methods_already_populated,
   const bool class_initializer_already_seen,
   const irep_idt &method_name,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   std::unordered_set<irep_idt> &methods_to_convert_later,
   std::unordered_set<irep_idt> &instantiated_classes,
   std::unordered_set<class_method_descriptor_exprt, irep_hash>
@@ -367,7 +378,7 @@ ci_lazy_methodst::convert_and_analyze_method(
 ///   * all the methods of the main jar file
 /// \return set of identifiers of entry point methods
 std::unordered_set<irep_idt> ci_lazy_methodst::entry_point_methods(
-  const symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   message_handlert &message_handler)
 {
   std::unordered_set<irep_idt> methods_to_convert_later;
@@ -481,7 +492,7 @@ void ci_lazy_methodst::get_virtual_method_targets(
   const class_method_descriptor_exprt &called_function,
   const std::unordered_set<irep_idt> &instantiated_classes,
   std::unordered_set<irep_idt> &callable_methods,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   const auto &call_class = called_function.class_id();
   const auto &method_name = called_function.mangled_method_name();
@@ -506,8 +517,8 @@ void ci_lazy_methodst::get_virtual_method_targets(
 ///   `e` or its children.
 void ci_lazy_methodst::gather_needed_globals(
   const exprt &e,
-  const symbol_tablet &symbol_table,
-  symbol_tablet &needed)
+  const symbol_table_baset &symbol_table,
+  symbol_table_baset &needed)
 {
   if(e.id()==ID_symbol)
   {
@@ -546,7 +557,7 @@ irep_idt ci_lazy_methodst::get_virtual_method_target(
   const std::unordered_set<irep_idt> &instantiated_classes,
   const irep_idt &call_basename,
   const irep_idt &classname,
-  const symbol_tablet &symbol_table)
+  const symbol_table_baset &symbol_table)
 {
   // Program-wide, is this class ever instantiated?
   if(!instantiated_classes.count(classname))

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -27,6 +27,7 @@ class ci_lazy_methods_neededt;
 class java_class_loadert;
 class message_handlert;
 class select_pointer_typet;
+class symbol_table_baset;
 
 // Map from method id to class_method_and_bytecodet
 class method_bytecodet
@@ -90,14 +91,14 @@ typedef std::function<
   bool(const irep_idt &function_id, ci_lazy_methods_neededt)>
   method_convertert;
 
-typedef std::function<std::vector<irep_idt>(const symbol_tablet &)>
+typedef std::function<std::vector<irep_idt>(const symbol_table_baset &)>
   load_extra_methodst;
 
 class ci_lazy_methodst
 {
 public:
   ci_lazy_methodst(
-    const symbol_tablet &symbol_table,
+    const symbol_table_baset &symbol_table,
     const irep_idt &main_class,
     const std::vector<irep_idt> &main_jar_classes,
     const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
@@ -108,7 +109,7 @@ class ci_lazy_methodst
 
   // not const since messaget
   bool operator()(
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     method_bytecodet &method_bytecode,
     const method_convertert &method_converter,
     message_handlert &message_handler);
@@ -127,18 +128,18 @@ class ci_lazy_methodst
     const class_method_descriptor_exprt &called_function,
     const std::unordered_set<irep_idt> &instantiated_classes,
     std::unordered_set<irep_idt> &callable_methods,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   void gather_needed_globals(
     const exprt &e,
-    const symbol_tablet &symbol_table,
-    symbol_tablet &needed);
+    const symbol_table_baset &symbol_table,
+    symbol_table_baset &needed);
 
   irep_idt get_virtual_method_target(
     const std::unordered_set<irep_idt> &instantiated_classes,
     const irep_idt &call_basename,
     const irep_idt &classname,
-    const symbol_tablet &symbol_table);
+    const symbol_table_baset &symbol_table);
 
   static irep_idt build_virtual_method_name(
     const irep_idt &class_name,
@@ -154,7 +155,7 @@ class ci_lazy_methodst
   const synthetic_methods_mapt &synthetic_methods;
 
   std::unordered_set<irep_idt> entry_point_methods(
-    const symbol_tablet &symbol_table,
+    const symbol_table_baset &symbol_table,
     message_handlert &message_handler);
 
   struct convert_method_resultt
@@ -168,7 +169,7 @@ class ci_lazy_methodst
     std::unordered_set<irep_idt> &methods_already_populated,
     const bool class_initializer_already_seen,
     const irep_idt &method_name,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     std::unordered_set<irep_idt> &methods_to_convert_later,
     std::unordered_set<irep_idt> &instantiated_classes,
     std::unordered_set<class_method_descriptor_exprt, irep_hash>
@@ -180,7 +181,7 @@ class ci_lazy_methodst
     std::unordered_set<irep_idt> &instantiated_classes,
     const std::unordered_set<class_method_descriptor_exprt, irep_hash>
       &virtual_functions,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 };
 
 #endif // CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -11,13 +11,13 @@ Author: Chris Smowton, [email protected]
 
 #include "ci_lazy_methods_needed.h"
 
-#include <goto-programs/resolve_inherited_component.h>
-
 #include <util/namespace.h>
 #include <util/std_types.h>
-#include <util/symbol_table.h>
+#include <util/symbol_table_base.h>
+
+#include <goto-programs/resolve_inherited_component.h>
 
-#include "generic_parameter_specialization_map.h"
+#include "generic_parameter_specialization_map.h" // IWYU pragma: keep
 #include "java_static_initializers.h"
 #include "java_types.h"
 #include "select_pointer_type.h"

jbmc/src/java_bytecode/ci_lazy_methods_needed.h

@@ -19,7 +19,7 @@ Author: Chris Smowton, [email protected]
 class namespacet;
 class pointer_typet;
 class select_pointer_typet;
-class symbol_tablet;
+class symbol_table_baset;
 class typet;
 
 class ci_lazy_methods_neededt
@@ -28,7 +28,7 @@ class ci_lazy_methods_neededt
   ci_lazy_methods_neededt(
     std::unordered_set<irep_idt> &_callable_methods,
     std::unordered_set<irep_idt> &_instantiated_classes,
-    const symbol_tablet &_symbol_table,
+    const symbol_table_baset &_symbol_table,
     const select_pointer_typet &pointer_type_selector)
     : callable_methods(_callable_methods),
       instantiated_classes(_instantiated_classes),
@@ -53,7 +53,7 @@ class ci_lazy_methods_neededt
   // found so far, so we can use a membership test to avoid
   // repeatedly exploring a class hierarchy.
   std::unordered_set<irep_idt> &instantiated_classes;
-  const symbol_tablet &symbol_table;
+  const symbol_table_baset &symbol_table;
 
   const select_pointer_typet &pointer_type_selector;
 

jbmc/src/java_bytecode/code_with_references.cpp

@@ -9,8 +9,6 @@ Author: Romain Brenguier, [email protected]
 #include "code_with_references.h"
 #include "java_types.h"
 
-#include <goto-programs/goto_instruction_code.h>
-
 #include <util/arith_tools.h>
 
 codet allocate_array(

jbmc/src/java_bytecode/create_array_with_type_intrinsic.h

@@ -12,7 +12,7 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_JAVA_BYTECODE_CREATE_ARRAY_WITH_TYPE_INTRINSIC_H
 #define CPROVER_JAVA_BYTECODE_CREATE_ARRAY_WITH_TYPE_INTRINSIC_H
 
-#include <util/std_code.h>
+#include <util/std_code_base.h>
 
 class message_handlert;
 class symbol_table_baset;

jbmc/src/java_bytecode/java_bmc_util.cpp

@@ -4,7 +4,7 @@ Module: Bounded Model Checking Utils for Java
 
 Author: Daniel Kroening, Peter Schrammel
 
- \*******************************************************************/
+\*******************************************************************/
 
 /// \file
 /// Bounded Model Checking Utils for Java

jbmc/src/java_bytecode/java_bmc_util.h

@@ -4,7 +4,7 @@ Module: Bounded Model Checking Utils for Java
 
 Author: Daniel Kroening, Peter Schrammel
 
- \*******************************************************************/
+\*******************************************************************/
 
 /// \file
 /// Bounded Model Checking Utils for Java