Remove unnecessary includes

Manual removal of includes based on include-what-you-use's output,
filtered for includes that should be removed. The goal is to avoid
unnecessary build dependencies, reducing the amount of code that needs
to be rebuilt during incremental builds. The build time for fresh
rebuilds decreases by about 7% as the following experiment shows:

```
rm -rf build && ccache -C
cmake -H. -Bbuild -G Ninja \
  -DCMAKE_BUILD_TYPE=Release \
  -DCMAKE_EXE_LINKER_FLAGS="-fuse-ld=lld -Wl,--threads"
/usr/bin/time -v ninja -C build -j32
```

Repeated execution for both develop and this branch producing the
following data, which less than 1s of variation across multiple runs:

develop:
```
  Command being timed: "ninja -C build -j32"
  User time (seconds): 2714.02
  System time (seconds): 203.75
  Percent of CPU this job got: 2833%
  Elapsed (wall clock) time (h:mm:ss or m:ss): 1:42.96
```

this PR:
```
  Command being timed: "ninja -C build -j32"
  User time (seconds): 2507.14
  System time (seconds): 189.95
  Percent of CPU this job got: 2822%
  Elapsed (wall clock) time (h:mm:ss or m:ss): 1:35.56
```

Author: tautschnig

jbmc/src/janalyzer/janalyzer_main.cpp

@@ -11,7 +11,9 @@ Author: Peter Schrammel
 
 #include "janalyzer_parse_options.h"
 
-#include <util/unicode.h>
+#ifdef _MSC_VER
+#  include <util/unicode.h>
+#endif
 
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -19,14 +19,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/ansi_c_language.h>
 
-#include <goto-programs/goto_convert_functions.h>
-#include <goto-programs/goto_inline.h>
-#include <goto-programs/read_goto_binary.h>
-#include <goto-programs/remove_complex.h>
-#include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_skip.h>
-#include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
@@ -36,7 +30,6 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/dependence_graph.h>
 #include <analyses/goto_check.h>
 #include <analyses/interval_domain.h>
-#include <analyses/is_threaded.h>
 #include <analyses/local_may_alias.h>
 
 #include <java_bytecode/java_bytecode_language.h>
@@ -52,7 +45,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/options.h>
-#include <util/unicode.h>
 #include <util/version.h>
 
 #include <goto-analyzer/static_show_domain.h>

jbmc/src/janalyzer/janalyzer_parse_options.h

@@ -102,21 +102,19 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/parse_options.h>
 #include <util/timestamper.h>
-#include <util/ui_message.h>
 
 #include <langapi/language.h>
 
-#include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
-#include <analyses/ai.h>
 #include <analyses/goto_check.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 
-class bmct;
-class goto_functionst;
+class abstract_goto_modelt;
+class ai_baset;
+class goto_model_functiont;
 class optionst;
 
 // clang-format off

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -11,15 +11,19 @@ Author: Diffblue Ltd.
 #include "ci_lazy_methods_needed.h"
 #include "code_with_references.h"
 #include "java_static_initializers.h"
-#include "java_string_library_preprocess.h"
 #include "java_string_literals.h"
+#include "java_types.h"
 #include "java_utils.h"
 
 #include <goto-programs/class_identifier.h>
+
 #include <util/allocate_objects.h>
+#include <util/arith_tools.h>
 #include <util/array_element_from_pointer.h>
 #include <util/expr_initializer.h>
-#include <util/prefix.h>
+#include <util/ieee_float.h>
+#include <util/json.h>
+#include <util/symbol_table_base.h>
 #include <util/unicode.h>
 
 /// Values passed around between most functions of the recursive deterministic

jbmc/src/java_bytecode/assignments_from_json.h

@@ -12,7 +12,6 @@ Author: Diffblue Ltd.
 #define CPROVER_JAVA_BYTECODE_ASSIGNMENTS_FROM_JSON_H
 
 #include "code_with_references.h"
-#include <util/std_code.h>
 
 class jsont;
 class symbol_table_baset;

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -7,13 +7,13 @@ Author: Diffblue Ltd.
 \*******************************************************************/
 
 #include "ci_lazy_methods.h"
-#include "java_entry_point.h"
+#include "java_bytecode_language.h"
 #include "java_class_loader.h"
-#include "java_utils.h"
-#include "java_string_library_preprocess.h"
+#include "java_entry_point.h"
 #include "remove_exceptions.h"
 
 #include <util/expr_iterator.h>
+#include <util/namespace.h>
 #include <util/suffix.h>
 
 #include <goto-programs/resolve_inherited_component.h>

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -12,22 +12,21 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H
 #define CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H
 
-#include "ci_lazy_methods_needed.h"
 #include "java_bytecode_parse_tree.h"
-#include "java_class_loader.h"
-#include "select_pointer_type.h"
 #include "synthetic_methods_map.h"
 
-#include <map>
 #include <functional>
+#include <map>
+#include <unordered_set>
 
 #include <util/irep.h>
-#include <util/symbol_table.h>
-#include <util/message.h>
 
 #include <goto-programs/class_hierarchy.h>
 
-class java_string_library_preprocesst;
+class ci_lazy_methods_neededt;
+class java_class_loadert;
+class message_handlert;
+class select_pointer_typet;
 
 // Map from method id to class_method_and_bytecodet
 class method_bytecodet

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -15,10 +15,11 @@ Author: Chris Smowton, [email protected]
 
 #include <util/namespace.h>
 #include <util/std_types.h>
+#include <util/symbol_table.h>
 
-#include <string>
-
+#include "generic_parameter_specialization_map.h"
 #include "java_static_initializers.h"
+#include "java_types.h"
 #include "select_pointer_type.h"
 
 /// Notes `method_symbol_name` is referenced from some reachable function, and

jbmc/src/java_bytecode/ci_lazy_methods_needed.h

@@ -12,14 +12,15 @@ Author: Chris Smowton, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
 #define CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
 
-#include <set>
 #include <unordered_set>
-#include <util/namespace.h>
-#include <util/symbol_table.h>
-#include <vector>
 
-class select_pointer_typet;
+#include <util/irep.h>
+
+class namespacet;
 class pointer_typet;
+class select_pointer_typet;
+class symbol_tablet;
+class typet;
 
 class ci_lazy_methods_neededt
 {

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -15,11 +15,8 @@ Author: Reuben Thomas, [email protected]
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
-#include <util/irep_ids.h>
-
-#include <memory>
-
 #include "java_object_factory.h" // gen_nondet_init
+#include "java_object_factory_parameters.h"
 #include "java_utils.h"
 
 /// Returns true if `expr` is a nondet pointer that isn't a function pointer or

jbmc/src/java_bytecode/convert_java_nondet.h

@@ -12,7 +12,6 @@ Author: Reuben Thomas, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
 #define CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
 
-#include <cstddef> // size_t
 #include <util/irep.h>
 
 class goto_functionst;

jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp

@@ -11,8 +11,6 @@ Author: Diffblue Ltd.
 
 #include "create_array_with_type_intrinsic.h"
 
-#include <goto-programs/class_identifier.h>
-
 #include <java_bytecode/java_types.h>
 
 #include <util/fresh_symbol.h>

jbmc/src/java_bytecode/create_array_with_type_intrinsic.h

@@ -12,9 +12,10 @@ 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/message.h>
 #include <util/std_code.h>
-#include <util/symbol_table_base.h>
+
+class message_handlert;
+class symbol_table_baset;
 
 irep_idt get_create_array_with_type_name();
 

jbmc/src/java_bytecode/expr2java.cpp

@@ -8,12 +8,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "expr2java.h"
 
-#include <sstream>
-
 #include <util/namespace.h>
-#include <util/std_types.h>
 #include <util/std_expr.h>
-#include <util/symbol.h>
 #include <util/unicode.h>
 #include <util/arith_tools.h>
 #include <util/ieee_float.h>

jbmc/src/java_bytecode/expr2java.h

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_JAVA_BYTECODE_EXPR2JAVA_H
 
 #include <cmath>
-#include <limits>
-#include <numeric>
 #include <sstream>
 #include <string>
 

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp

@@ -2,8 +2,6 @@
 
 #include "generic_parameter_specialization_map_keys.h"
 
-#include <util/range.h>
-
 /// Add the parameters and their types for each generic parameter of the
 /// given generic pointer type to the map.
 /// Own the keys and pop from their stack on destruction.

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h

@@ -3,8 +3,7 @@
 #ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
 #define CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
 
-#include "select_pointer_type.h"
-#include "java_types.h"
+#include "generic_parameter_specialization_map.h"
 
 /// \file
 /// Generic-parameter-specialization-map entries owner class.

jbmc/src/java_bytecode/jar_file.cpp

@@ -10,11 +10,7 @@ Author: Diffblue Ltd
 
 #include <algorithm>
 #include <cctype>
-
-#include <util/invariant.h>
-#include <util/suffix.h>
-
-#include "java_class_loader_limit.h"
+#include <sstream>
 
 void jar_filet::initialize_file_index()
 {

jbmc/src/java_bytecode/jar_file.h

@@ -10,7 +10,6 @@ Author: Diffblue Ltd
 #define CPROVER_JAVA_BYTECODE_JAR_FILE_H
 
 #include <unordered_map>
-#include <memory>
 #include <string>
 #include <vector>
 

jbmc/src/java_bytecode/jar_pool.h

@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include <map>
 #include <string>
 
-class jar_filet;
+#include "jar_file.h"
 
 /// A chache for jar_filet objects, by file name
 class jar_poolt

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -11,11 +11,13 @@ Author: Kurt Degiogrio, [email protected]
 #include "java_types.h"
 #include "java_utils.h"
 
+#include <util/arith_tools.h>
+#include <util/cprover_prefix.h>
 #include <util/expr_iterator.h>
+#include <util/message.h>
 #include <util/namespace.h>
-#include <util/cprover_prefix.h>
 #include <util/std_types.h>
-#include <util/arith_tools.h>
+#include <util/symbol_table.h>
 
 // Disable linter to allow an std::string constant.
 const std::string next_thread_id = CPROVER_PREFIX "_next_thread_id";// NOLINT(*)

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.h

@@ -8,8 +8,8 @@ Author: Kurt Degiogrio, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONCURRENCY_INSTRUMENTATION_H
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONCURRENCY_INSTRUMENTATION_H
 
-#include <util/symbol_table.h>
-#include <util/message.h>
+class message_handlert;
+class symbol_tablet;
 
 void convert_threadblock(symbol_tablet &symbol_table);
 void convert_synchronized_methods(

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -15,21 +15,17 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #endif
 
+#include "ci_lazy_methods.h"
+#include "java_bytecode_convert_method.h"
 #include "java_root_class.h"
 #include "java_types.h"
-#include "java_bytecode_convert_method.h"
-#include "java_bytecode_language.h"
 #include "java_utils.h"
 
-#include <goto-programs/class_identifier.h>
-
 #include <util/arith_tools.h>
-#include <util/c_types.h>
 #include <util/expr_initializer.h>
 #include <util/namespace.h>
 #include <util/prefix.h>
 #include <util/std_expr.h>
-#include <util/suffix.h>
 
 class java_bytecode_convert_classt
 {

jbmc/src/java_bytecode/java_bytecode_convert_class.h

@@ -13,11 +13,13 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H
 
 #include <unordered_set>
-#include <util/symbol_table.h>
-#include <util/message.h>
 
 #include "java_bytecode_parse_tree.h"
-#include "java_bytecode_language.h"
+#include "java_class_loader.h"
+
+class java_string_library_preprocesst;
+class method_bytecodet;
+class symbol_tablet;
 
 /// See class \ref java_bytecode_convert_classt
 bool java_bytecode_convert_class(

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -24,34 +24,26 @@ Author: Daniel Kroening, [email protected]
 #include "java_utils.h"
 #include "lambda_synthesis.h"
 #include "pattern.h"
-#include "remove_exceptions.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
 #include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/prefix.h>
-#include <util/simplify_expr.h>
+#include <util/prefix_filter.h>
 #include <util/std_expr.h>
-#include <util/string2int.h>
 #include <util/threeval.h>
 
-#include <goto-programs/cfg.h>
-#include <goto-programs/class_hierarchy.h>
-#include <goto-programs/remove_returns.h>
 #include <goto-programs/resolve_inherited_component.h>
 
-#include <analyses/cfg_dominators.h>
 #include <analyses/uncaught_exceptions_analysis.h>
 
 #include <algorithm>
-#include <functional>
 #include <limits>
-#include <regex>
-#include <unordered_set>
 
 /// Iterates through the parameters of the function type \p ftype, finds a new
 /// new name for each parameter and renames them in `ftype.parameters()` as