Move method context check before symbol value assignment

The previous check was right at the beginning of convert_single_method,
meaning that for an "excluded" method, we would have never entered
java_bytecode_convert_method, which assigns more than just the symbol
value (body of a method), e.g. parameter identifiers.
The only information that we want to omit for excluded methods is their
bodies / symbol values. This is why the new check is just before the
assignment of symbol values, making sure that parameter identifiers and
other meta-information of the method are correctly assigned for excluded
methods.

Author: antlechner

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -425,7 +425,8 @@ static irep_idt get_method_identifier(
 
 void java_bytecode_convert_methodt::convert(
   const symbolt &class_symbol,
-  const methodt &m)
+  const methodt &m,
+  const optionalt<prefix_filtert> &method_context)
 {
   // Construct the fully qualified method name
   // (e.g. "my.package.ClassName.myMethodName:(II)I") and query the symbol table
@@ -605,8 +606,12 @@ void java_bytecode_convert_methodt::convert(
   if((!m.is_abstract) && (!m.is_native))
   {
     code_blockt code(convert_parameter_annotations(m, method_type));
-    code.append(convert_instructions(m));
-    method_symbol.value = std::move(code);
+    // Do not convert if method is not in context
+    if(!method_context || (*method_context)(id2string(method_identifier)))
+    {
+      code.append(convert_instructions(m));
+      method_symbol.value = std::move(code);
+    }
   }
 }
 
@@ -3184,7 +3189,8 @@ void java_bytecode_convert_method(
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   java_string_library_preprocesst &string_preprocess,
   const class_hierarchyt &class_hierarchy,
-  bool threading_support)
+  bool threading_support,
+  optionalt<prefix_filtert> method_context)
 
 {
   java_bytecode_convert_methodt java_bytecode_convert_method(
@@ -3197,7 +3203,7 @@ void java_bytecode_convert_method(
     class_hierarchy,
     threading_support);
 
-  java_bytecode_convert_method(class_symbol, method);
+  java_bytecode_convert_method(class_symbol, method, method_context);
 }
 
 /// Returns true iff method \p methodid from class \p classname is

jbmc/src/java_bytecode/java_bytecode_convert_method.h

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol_table.h>
 
 class class_hierarchyt;
+class prefix_filtert;
 
 void java_bytecode_initialize_parameter_names(
   symbolt &method_symbol,
@@ -37,7 +38,8 @@ void java_bytecode_convert_method(
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   java_string_library_preprocesst &string_preprocess,
   const class_hierarchyt &class_hierarchy,
-  bool threading_support);
+  bool threading_support,
+  optionalt<prefix_filtert> method_context);
 
 void create_method_stub_symbol(
   const irep_idt &identifier,

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -61,9 +61,12 @@ class java_bytecode_convert_methodt:public messaget
   typedef methodt::local_variable_tablet local_variable_tablet;
   typedef methodt::local_variablet local_variablet;
 
-  void operator()(const symbolt &class_symbol, const methodt &method)
+  void operator()(
+    const symbolt &class_symbol,
+    const methodt &method,
+    const optionalt<prefix_filtert> method_context)
   {
-    convert(class_symbol, method);
+    convert(class_symbol, method, method_context);
   }
 
   typedef uint16_t method_offsett;
@@ -290,7 +293,10 @@ class java_bytecode_convert_methodt:public messaget
     bool allow_merge = true);
 
   // conversion
-  void convert(const symbolt &class_symbol, const methodt &);
+  void convert(
+    const symbolt &class_symbol,
+    const methodt &,
+    const optionalt<prefix_filtert> &method_context);
 
   code_blockt convert_parameter_annotations(
     const methodt &method,

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1173,12 +1173,6 @@ bool java_bytecode_languaget::convert_single_method(
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
 {
-  // Do not convert if method is not in context
-  if(method_context && !(*method_context)(id2string(function_id)))
-  {
-    return false;
-  }
-
   const symbolt &symbol = symbol_table.lookup_ref(function_id);
 
   // Nothing to do if body is already loaded
@@ -1312,7 +1306,8 @@ bool java_bytecode_languaget::convert_single_method(
       std::move(needed_lazy_methods),
       string_preprocess,
       class_hierarchy,
-      threading_support);
+      threading_support,
+      method_context);
     INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
     return false;
   }