Update Java bytecode parser to always load code attributes

Previously it didn't load code attributes when skip_instructions was set
Now this flag just skips the actual instructions and the exceptions table
This means it will have the local variable table, which will allow us to retrieve parameter names
Updated unit test to check for this

Author: NathanJPhillips

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1222,35 +1222,44 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
 
   irep_idt attribute_name=pool_entry(attribute_name_index).s;
 
-  if(attribute_name == "Code" && !skip_instructions)
+  if(attribute_name == "Code")
   {
     UNUSED_u2(max_stack);
     UNUSED_u2(max_locals);
 
-    rbytecode(method.instructions);
+    if(skip_instructions)
+      skip_bytes(read_u4());
+    else
+      rbytecode(method.instructions);
 
     u2 exception_table_length=read_u2();
-    method.exception_table.resize(exception_table_length);
-
-    for(std::size_t e=0; e<exception_table_length; e++)
+    if(skip_instructions)
+      skip_bytes(exception_table_length * 8u);
+    else
     {
-      u2 start_pc=read_u2();
-      u2 end_pc=read_u2();
+      method.exception_table.resize(exception_table_length);
 
-      // from the class file format spec ("4.7.3. The Code Attribute" for Java8)
-      INVARIANT(
-        start_pc < end_pc,
-        "The start_pc must be less than the end_pc as this is the range the "
-        "exception is active");
-
-      u2 handler_pc=read_u2();
-      u2 catch_type=read_u2();
-      method.exception_table[e].start_pc=start_pc;
-      method.exception_table[e].end_pc=end_pc;
-      method.exception_table[e].handler_pc=handler_pc;
-      if(catch_type!=0)
-        method.exception_table[e].catch_type =
-          to_struct_tag_type(pool_entry(catch_type).expr.type());
+      for(std::size_t e = 0; e < exception_table_length; e++)
+      {
+        u2 start_pc = read_u2();
+        u2 end_pc = read_u2();
+
+        // From the class file format spec ("4.7.3. The Code Attribute" for
+        // Java8)
+        INVARIANT(
+          start_pc < end_pc,
+          "The start_pc must be less than the end_pc as this is the range the "
+          "exception is active");
+
+        u2 handler_pc = read_u2();
+        u2 catch_type = read_u2();
+        method.exception_table[e].start_pc = start_pc;
+        method.exception_table[e].end_pc = end_pc;
+        method.exception_table[e].handler_pc = handler_pc;
+        if(catch_type != 0)
+          method.exception_table[e].catch_type =
+            to_struct_tag_type(pool_entry(catch_type).expr.type());
+      }
     }
 
     u2 attributes_count=read_u2();

jbmc/unit/java_bytecode/java_bytecode_parser/Trivial$Inner.class

@@ -3,8 +3,15 @@ public class Trivial {
   public class Inner {
     @Annotation
     private int x;
+
     public Inner() { x = 1; }
+
     @Annotation
-    public void f() { x++; };
+    public void f(int y) {
+        try {
+            x++;
+        } catch(Exception ex) {
+        }
+    }
   }
 }

jbmc/unit/java_bytecode/java_bytecode_parser/Trivial.class

@@ -41,8 +41,14 @@ static void check_class_structure(
 
   REQUIRE(method_f.is_public);
   REQUIRE(method_f.annotations.size() == 1);
+  REQUIRE(method_f.local_variable_table.size() == 2);
+  REQUIRE(method_f.local_variable_table[0].name == "this");
+  REQUIRE(method_f.local_variable_table[1].name == "y");
   REQUIRE(method_constructor.is_public);
   REQUIRE(method_constructor.annotations.size() == 0);
+  REQUIRE(method_f.local_variable_table.size() == 2);
+  REQUIRE(method_constructor.local_variable_table[0].name == "this");
+  REQUIRE(method_constructor.local_variable_table[1].name == "this$0");
 }
 
 SCENARIO(
@@ -72,6 +78,12 @@ SCENARIO(
           REQUIRE(methodone.instructions.size() == 0);
           REQUIRE(methodtwo.instructions.size() == 0);
         }
+
+        THEN("Neither method should have an exception table")
+        {
+          REQUIRE(methodone.exception_table.empty());
+          REQUIRE(methodtwo.exception_table.empty());
+        }
       }
     }
   }
@@ -99,6 +111,12 @@ SCENARIO(
           REQUIRE(methodone.instructions.size() != 0);
           REQUIRE(methodtwo.instructions.size() != 0);
         }
+
+        const auto &method_f = methodone.name == "f" ? methodone : methodtwo;
+        THEN("f should have an exception table")
+        {
+          REQUIRE(!method_f.exception_table.empty());
+        }
       }
     }
   }