Pass irep_idt by value (C++ Core Guidelines F.16) + CI checker

.github/workflows/syntax-checks.yaml

@@ -59,3 +59,23 @@ jobs:
           rustup toolchain install stable --profile minimal --no-self-update -c clippy -c rustfmt
       - name: Run `cargo fmt` on top of Rust API project
         run: cd src/libcprover-rust; cargo fmt --all -- --check
+
+  # This job takes approximately 3 minutes
+  check-pass-by-value:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@v6
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq \
+            cmake g++ flex bison clang-18 llvm-18-dev libclang-18-dev \
+            libclang-cpp18-dev
+      - name: Configure
+        run: cmake -S . -Bbuild -DCMAKE_EXPORT_COMPILE_COMMANDS=ON
+      - name: Check for pass-by-const-reference of cheap-to-copy types
+        run: ./scripts/run_pass_by_value_check.sh build

.gitignore

@@ -166,3 +166,4 @@ dist/
 
 # auto generated documentation
 doc/html/
+/scripts/check-pass-by-value

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -688,7 +688,8 @@ void janalyzer_parse_optionst::process_goto_function(
   // Java virtual functions -> explicit dispatch tables:
   remove_virtual_functions(function, *class_hierarchy);
 
-  auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
+  auto function_is_stub = [&symbol_table, &model](irep_idt id)
+  {
     return symbol_table.lookup_ref(id).value.is_nil() &&
            !model.can_produce_function(id);
   };
@@ -698,15 +699,15 @@ void janalyzer_parse_optionst::process_goto_function(
   transform_assertions_assumptions(options, function.get_goto_function().body);
 }
 
-bool janalyzer_parse_optionst::can_generate_function_body(const irep_idt &name)
+bool janalyzer_parse_optionst::can_generate_function_body(irep_idt name)
 {
   static const irep_idt initialize_id = INITIALIZE_FUNCTION;
 
   return name != goto_functionst::entry_point() && name != initialize_id;
 }
 
 bool janalyzer_parse_optionst::generate_function_body(
-  const irep_idt &function_name,
+  irep_idt function_name,
   symbol_table_baset &symbol_table,
   goto_functiont &function,
   bool body_available)

jbmc/src/janalyzer/janalyzer_parse_options.h

@@ -164,10 +164,10 @@ class janalyzer_parse_optionst : public parse_options_baset
     const abstract_goto_modelt &model,
     const optionst &options);
 
-  bool can_generate_function_body(const irep_idt &name);
+  bool can_generate_function_body(irep_idt name);
 
   bool generate_function_body(
-    const irep_idt &function_name,
+    irep_idt function_name,
     symbol_table_baset &symbol_table,
     goto_functiont &function,
     bool body_available);

jbmc/src/java_bytecode/README.md

@@ -674,10 +674,10 @@ determine which loading strategy to use.
 If [lazy_methods_mode](\ref java_bytecode_language_optionst::lazy_methods_mode) is
 \ref LAZY_METHODS_MODE_EAGER then eager loading is
 used. Under eager loading
-\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, lazy_class_to_declared_symbols_mapt &, message_handlert &)
+\ref java_bytecode_languaget::convert_single_method(irep_idt, symbol_table_baset &, lazy_class_to_declared_symbols_mapt &, message_handlert &)
 is called once for each method listed in method_bytecode (described above). This
 then calls
-\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, std::optional<ci_lazy_methods_neededt>, lazy_class_to_declared_symbols_mapt &, message_handlert &);
+\ref java_bytecode_languaget::convert_single_method(irep_idt, symbol_table_baset &, std::optional<ci_lazy_methods_neededt>, lazy_class_to_declared_symbols_mapt &, message_handlert &);
 
 without a ci_lazy_methods_neededt object, which calls
 \ref java_bytecode_convert_method, passing in the method parse tree. This in

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -914,7 +914,7 @@ code_with_references_listt assign_from_json_rec(
 code_with_references_listt assign_from_json(
   const exprt &expr,
   const jsont &json,
-  const irep_idt &function_id,
+  irep_idt function_id,
   symbol_table_baset &symbol_table,
   std::optional<ci_lazy_methods_neededt> &needed_lazy_methods,
   size_t max_user_array_length,

jbmc/src/java_bytecode/assignments_from_json.h

@@ -98,7 +98,7 @@ class ci_lazy_methods_neededt;
 code_with_references_listt assign_from_json(
   const exprt &expr,
   const jsont &json,
-  const irep_idt &function_id,
+  irep_idt function_id,
   symbol_table_baset &symbol_table,
   std::optional<ci_lazy_methods_neededt> &needed_lazy_methods,
   size_t max_user_array_length,

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -38,7 +38,7 @@ Author: Diffblue Ltd.
 ///   Java bytecode.
 ci_lazy_methodst::ci_lazy_methodst(
   const symbol_table_baset &symbol_table,
-  const irep_idt &main_class,
+  irep_idt main_class,
   const std::vector<irep_idt> &main_jar_classes,
   const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
   java_class_loadert &java_class_loader,
@@ -331,7 +331,7 @@ ci_lazy_methodst::convert_and_analyze_method(
   const method_convertert &method_converter,
   std::unordered_set<irep_idt> &methods_already_populated,
   const bool class_initializer_already_seen,
-  const irep_idt &method_name,
+  irep_idt method_name,
   symbol_table_baset &symbol_table,
   std::unordered_set<irep_idt> &methods_to_convert_later,
   std::unordered_set<irep_idt> &instantiated_classes,
@@ -557,8 +557,8 @@ void ci_lazy_methodst::gather_needed_globals(
 ///   `instantiated_classes`, or irep_idt() otherwise.
 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,
+  irep_idt call_basename,
+  irep_idt classname,
   const symbol_table_baset &symbol_table)
 {
   // Program-wide, is this class ever instantiated?

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -50,7 +50,7 @@ class method_bytecodet
   mapt map;
 
 public:
-  bool contains_method(const irep_idt &method_id) const
+  bool contains_method(irep_idt method_id) const
   {
     return map.count(method_id) != 0;
   }
@@ -63,8 +63,8 @@ class method_bytecodet
   }
 
   void add(
-    const irep_idt &class_id,
-    const irep_idt &method_id,
+    irep_idt class_id,
+    irep_idt method_id,
     const java_bytecode_parse_treet::methodt &method)
   {
     add(class_method_and_bytecodet{class_id, method_id, method});
@@ -79,7 +79,7 @@ class method_bytecodet
     return map.end();
   }
 
-  opt_reft get(const irep_idt &method_id)
+  opt_reft get(irep_idt method_id)
   {
     const auto it = map.find(method_id);
     if(it == map.end())
@@ -88,8 +88,7 @@ class method_bytecodet
   }
 };
 
-typedef std::function<
-  bool(const irep_idt &function_id, ci_lazy_methods_neededt)>
+typedef std::function<bool(irep_idt function_id, ci_lazy_methods_neededt)>
   method_convertert;
 
 typedef std::function<std::vector<irep_idt>(const symbol_table_baset &)>
@@ -100,7 +99,7 @@ class ci_lazy_methodst
 public:
   ci_lazy_methodst(
     const symbol_table_baset &symbol_table,
-    const irep_idt &main_class,
+    irep_idt main_class,
     const std::vector<irep_idt> &main_jar_classes,
     const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
     java_class_loadert &java_class_loader,
@@ -138,13 +137,13 @@ class ci_lazy_methodst
 
   irep_idt get_virtual_method_target(
     const std::unordered_set<irep_idt> &instantiated_classes,
-    const irep_idt &call_basename,
-    const irep_idt &classname,
+    irep_idt call_basename,
+    irep_idt classname,
     const symbol_table_baset &symbol_table);
 
   static irep_idt build_virtual_method_name(
-    const irep_idt &class_name,
-    const irep_idt &component_method_name);
+    irep_idt class_name,
+    irep_idt component_method_name);
 
   class_hierarchyt class_hierarchy;
   irep_idt main_class;
@@ -169,7 +168,7 @@ class ci_lazy_methodst
     const method_convertert &method_converter,
     std::unordered_set<irep_idt> &methods_already_populated,
     const bool class_initializer_already_seen,
-    const irep_idt &method_name,
+    irep_idt method_name,
     symbol_table_baset &symbol_table,
     std::unordered_set<irep_idt> &methods_to_convert_later,
     std::unordered_set<irep_idt> &instantiated_classes,

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -25,8 +25,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 /// Notes `method_symbol_name` is referenced from some reachable function, and
 /// should therefore be elaborated.
 /// \param method_symbol_name: method name; must exist in symbol table.
-void ci_lazy_methods_neededt::add_needed_method(
-  const irep_idt &method_symbol_name)
+void ci_lazy_methods_neededt::add_needed_method(irep_idt method_symbol_name)
 {
   callable_methods.insert(method_symbol_name);
 }
@@ -39,7 +38,7 @@ void ci_lazy_methods_neededt::add_needed_method(
 /// __CPROVER_start in its initial setup, and because return values of opaque
 /// methods need to be considered in ci_lazy_methods too.
 /// \param class_id: The given class id
-void ci_lazy_methods_neededt::add_clinit_call(const irep_idt &class_id)
+void ci_lazy_methods_neededt::add_clinit_call(irep_idt class_id)
 {
   const irep_idt &clinit_wrapper = clinit_wrapper_name(class_id);
   if(symbol_table.symbols.count(clinit_wrapper))
@@ -50,7 +49,7 @@ void ci_lazy_methods_neededt::add_clinit_call(const irep_idt &class_id)
 /// ancestors then note that it is needed.
 /// \param class_id: The given class id
 void ci_lazy_methods_neededt::add_cprover_nondet_initialize_if_it_exists(
-  const irep_idt &class_id)
+  irep_idt class_id)
 {
   resolve_inherited_componentt resolve_inherited_component{symbol_table};
   std::optional<resolve_inherited_componentt::inherited_componentt>
@@ -69,8 +68,7 @@ void ci_lazy_methods_neededt::add_cprover_nondet_initialize_if_it_exists(
 /// therefore reachable.
 /// \param class_symbol_name: class name; must exist in symbol table.
 /// \return Returns true if `class_symbol_name` is new (not seen before).
-bool ci_lazy_methods_neededt::add_needed_class(
-  const irep_idt &class_symbol_name)
+bool ci_lazy_methods_neededt::add_needed_class(irep_idt class_symbol_name)
 {
   if(!instantiated_classes.insert(class_symbol_name).second)
     return false;

jbmc/src/java_bytecode/ci_lazy_methods_needed.h

@@ -36,9 +36,9 @@ class ci_lazy_methods_neededt
       pointer_type_selector(pointer_type_selector)
   {}
 
-  void add_needed_method(const irep_idt &);
+  void add_needed_method(irep_idt);
   // Returns true if new
-  bool add_needed_class(const irep_idt &);
+  bool add_needed_class(irep_idt);
 
   void add_all_needed_classes(const pointer_typet &pointer_type);
 
@@ -57,8 +57,8 @@ class ci_lazy_methods_neededt
 
   const select_pointer_typet &pointer_type_selector;
 
-  void add_clinit_call(const irep_idt &class_id);
-  void add_cprover_nondet_initialize_if_it_exists(const irep_idt &class_id);
+  void add_clinit_call(irep_idt class_id);
+  void add_cprover_nondet_initialize_if_it_exists(irep_idt class_id);
 
   void initialize_instantiated_classes_from_pointer(
     const pointer_typet &pointer_type,

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -44,7 +44,7 @@ static goto_programt get_gen_nondet_init_instructions(
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   const java_object_factory_parameterst &object_factory_parameters,
-  const irep_idt &mode)
+  irep_idt mode)
 {
   code_blockt gen_nondet_init_code;
   const bool skip_classid = true;
@@ -79,13 +79,13 @@ static goto_programt get_gen_nondet_init_instructions(
 /// \return The next instruction to process with this function and a boolean
 ///   indicating whether any changes were made to the goto program.
 static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
-  const irep_idt &function_identifier,
+  irep_idt function_identifier,
   goto_programt &goto_program,
   const goto_programt::targett &target,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   java_object_factory_parameterst object_factory_parameters,
-  const irep_idt &mode)
+  irep_idt mode)
 {
   const auto next_instr = std::next(target);
 
@@ -164,12 +164,12 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
 ///   nondet objects.
 /// \param mode: Language mode
 void convert_nondet(
-  const irep_idt &function_identifier,
+  irep_idt function_identifier,
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   const java_object_factory_parameterst &user_object_factory_parameters,
-  const irep_idt &mode)
+  irep_idt mode)
 {
   java_object_factory_parameterst object_factory_parameters =
     user_object_factory_parameters;
@@ -202,7 +202,7 @@ void convert_nondet(
   goto_model_functiont &function,
   message_handlert &message_handler,
   const java_object_factory_parameterst &object_factory_parameters,
-  const irep_idt &mode)
+  irep_idt mode)
 {
   convert_nondet(
     function.get_function_id(),

jbmc/src/java_bytecode/convert_java_nondet.h

@@ -64,6 +64,6 @@ void convert_nondet(
   goto_model_functiont &function,
   message_handlert &message_handler,
   const java_object_factory_parameterst &object_factory_parameters,
-  const irep_idt &mode);
+  irep_idt mode);
 
 #endif // CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H

jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp

@@ -39,7 +39,7 @@ irep_idt get_create_array_with_type_name()
 /// \param message_handler: any GOTO program conversion errors are logged here
 /// \return new GOTO program body for `org.cprover.CProver.createArrayWithType`.
 codet create_array_with_type_body(
-  const irep_idt &function_id,
+  irep_idt function_id,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler)
 {

jbmc/src/java_bytecode/create_array_with_type_intrinsic.h

@@ -20,7 +20,7 @@ class symbol_table_baset;
 irep_idt get_create_array_with_type_name();
 
 codet create_array_with_type_body(
-  const irep_idt &function_id,
+  irep_idt function_id,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler);
 

jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp

@@ -52,7 +52,7 @@ void generic_parameter_specialization_mapt::pop(std::size_t container_index)
 }
 
 std::optional<reference_typet>
-generic_parameter_specialization_mapt::pop(const irep_idt &parameter_name)
+generic_parameter_specialization_mapt::pop(irep_idt parameter_name)
 {
   const auto types_it = param_to_container.find(parameter_name);
   if(types_it == param_to_container.end())

jbmc/src/java_bytecode/generic_parameter_specialization_map.h

@@ -54,7 +54,7 @@ class generic_parameter_specialization_mapt
   /// \param parameter_name: The name of the type parameter
   /// \returns: The specialization for the given type parameter, if there was
   ///   one before the pop, or an empty std::optional if the stack was empty
-  std::optional<reference_typet> pop(const irep_idt &parameter_name);
+  std::optional<reference_typet> pop(irep_idt parameter_name);
 
   /// A wrapper for a generic_parameter_specialization_mapt and a namespacet
   /// that can be output to a stream

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -35,8 +35,8 @@ const std::string thread_id = CPROVER_PREFIX "_thread_id";// NOLINT(*)
 /// /return returns new or existing symbol.
 static symbolt add_or_get_symbol(
   symbol_table_baset &symbol_table,
-  const irep_idt &name,
-  const irep_idt &base_name,
+  irep_idt name,
+  irep_idt base_name,
   const typet &type,
   const exprt &value,
   const bool is_thread_local,