Add ability to mark methods as ignored (not loaded)

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -118,7 +118,15 @@ class java_bytecode_convert_classt:public messaget
   // see definition below for more info
   static void add_array_types(symbol_tablet &symbol_table);
 
-  static bool is_overlay_method(const methodt &method);
+  static bool is_overlay_method(const methodt &method)
+  {
+    return method.has_annotation(ID_overlay_method);
+  }
+
+  static bool is_ignored_method(const methodt &method)
+  {
+    return method.has_annotation(ID_ignored_method);
+  }
 
   bool check_field_exists(
     const fieldt &field,
@@ -455,6 +463,8 @@ void java_bytecode_convert_classt::convert(
   {
     for(const methodt &method : overlay_class.get().methods)
     {
+      if(is_ignored_method(method))
+        continue;
       const irep_idt method_identifier =
         qualified_classname + "." + id2string(method.name)
           + ":" + method.descriptor;
@@ -496,6 +506,8 @@ void java_bytecode_convert_classt::convert(
   }
   for(const methodt &method : c.methods)
   {
+    if(is_ignored_method(method))
+      continue;
     const irep_idt method_identifier=
       qualified_classname + "." + id2string(method.name)
         + ":" + method.descriptor;
@@ -877,13 +889,6 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
   }
 }
 
-bool java_bytecode_convert_classt::is_overlay_method(const methodt &method)
-{
-  return java_bytecode_parse_treet::find_annotation(
-           method.annotations, ID_overlay_method)
-    .has_value();
-}
-
 bool java_bytecode_convert_class(
   const java_class_loadert::parse_tree_with_overlayst &parse_trees,
   symbol_tablet &symbol_table,

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -84,6 +84,11 @@ class java_bytecode_parse_treet
       is_private(false), is_static(false), is_final(false)
     {
     }
+
+    bool has_annotation(const irep_idt &annotation_id) const
+    {
+      return find_annotation(annotations, annotation_id).has_value();
+    }
   };
 
   class methodt:public membert

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -168,50 +168,48 @@ java_class_loadert::get_parse_tree(
     }
   }
 
-  if(!parse_trees.empty())
+  auto parse_tree_it = parse_trees.begin();
+  // If the first class implementation is an overlay emit a warning and
+  // skip over it until we find a non-overlay class
+  while(parse_tree_it != parse_trees.end())
   {
-    auto parse_tree_it = parse_trees.begin();
-    // If the first class implementation is an overlay emit a warning and
-    // skip over it until we find a non-overlay class
-    while(parse_tree_it != parse_trees.end())
-    {
-      // Skip parse trees that failed to load - though these shouldn't exist yet
-      if(parse_tree_it->loading_successful)
-      {
-        if(!is_overlay_class(parse_tree_it->parsed_class))
-        {
-          // Keep the non-overlay class
-          ++parse_tree_it;
-          break;
-        }
-        warning()
-          << "Skipping class " << class_name
-          << " marked with OverlayClassImplementation but found before"
-            " original definition"
-          << eom;
-      }
-      auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
-      ++parse_tree_it;
-      parse_trees.erase(unloaded_or_overlay_out_of_order_it);
-    }
-    // Collect overlay classes
-    while(parse_tree_it != parse_trees.end())
+    // Skip parse trees that failed to load - though these shouldn't exist yet
+    if(parse_tree_it->loading_successful)
     {
-      // Remove non-initial classes that aren't overlays
       if(!is_overlay_class(parse_tree_it->parsed_class))
       {
-        warning()
-          << "Skipping duplicate definition of class " << class_name
-          << " not marked with OverlayClassImplementation" << eom;
-        auto duplicate_non_overlay_it = parse_tree_it;
+        // Keep the non-overlay class
         ++parse_tree_it;
-        parse_trees.erase(duplicate_non_overlay_it);
+        break;
       }
-      else
-        ++parse_tree_it;
+      warning()
+        << "Skipping class " << class_name
+        << " marked with OverlayClassImplementation but found before"
+          " original definition"
+        << eom;
     }
-    return parse_trees;
+    auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
+    ++parse_tree_it;
+    parse_trees.erase(unloaded_or_overlay_out_of_order_it);
   }
+  // Collect overlay classes
+  while(parse_tree_it != parse_trees.end())
+  {
+    // Remove non-initial classes that aren't overlays
+    if(!is_overlay_class(parse_tree_it->parsed_class))
+    {
+      warning()
+        << "Skipping duplicate definition of class " << class_name
+        << " not marked with OverlayClassImplementation" << eom;
+      auto duplicate_non_overlay_it = parse_tree_it;
+      ++parse_tree_it;
+      parse_trees.erase(duplicate_non_overlay_it);
+    }
+    else
+      ++parse_tree_it;
+  }
+  if(!parse_trees.empty())
+    return parse_trees;
 
   // Not found or failed to load
   warning() << "failed to load class `" << class_name << '\'' << eom;

src/util/irep_ids.def

@@ -664,6 +664,7 @@ IREP_ID_TWO(overflow_shl, overflow-shl)
 IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)
 IREP_ID_TWO(overlay_class, java::com.diffblue.OverlayClassImplementation)
 IREP_ID_TWO(overlay_method, java::com.diffblue.OverlayMethodImplementation)
+IREP_ID_TWO(ignored_method, java::com.diffblue.IgnoredMethodImplementation)
 IREP_ID_ONE(is_annotation)
 IREP_ID_TWO(C_annotations, #annotations)
 IREP_ID_ONE(final)