Merge pull request #4405 from NathanJPhillips/feature/skip-instrs-not-atts

Update Java bytecode parser to always load code attributes

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());
+        }
       }
     }
   }