Parses the exception attribute

4.7.5. The Exceptions Attribute

Author: jeannielynnmoulton

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -114,6 +114,8 @@ struct java_bytecode_parse_treet
     typedef std::vector<exceptiont> exception_tablet;
     exception_tablet exception_table;
 
+    std::vector<irep_idt> throws_exception_table;
+
     struct local_variablet
     {
       irep_idt name;

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -121,6 +121,7 @@ class java_bytecode_parsert:public parsert
   void rmethod(classt &parsed_class);
   void
   rinner_classes_attribute(classt &parsed_class, const u4 &attribute_length);
+  std::vector<irep_idt> rexceptions_attribute();
   void rclass_attribute(classt &parsed_class);
   void rRuntimeAnnotation_attribute(annotationst &);
   void rRuntimeAnnotation(annotationt &);
@@ -151,7 +152,7 @@ class java_bytecode_parsert:public parsert
     }
   }
 
-  u8 read_bytes(size_t bytes)
+  u8 read_bytes(size_t bytes) const
   {
     u8 result=0;
     for(size_t i=0; i<bytes; i++)
@@ -167,22 +168,22 @@ class java_bytecode_parsert:public parsert
     return result;
   }
 
-  u1 read_u1()
+  u1 read_u1() const
   {
     return (u1)read_bytes(1);
   }
 
-  inline u2 read_u2()
+  inline u2 read_u2() const
   {
     return (u2)read_bytes(2);
   }
 
-  u4 read_u4()
+  u4 read_u4() const
   {
     return (u4)read_bytes(4);
   }
 
-  u8 read_u8()
+  u8 read_u8() const
   {
     return read_bytes(8);
   }
@@ -1242,6 +1243,10 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
   {
     rRuntimeAnnotation_attribute(method.annotations);
   }
+  else if(attribute_name == "Exceptions")
+  {
+    method.throws_exception_table = rexceptions_attribute();
+  }
   else
     skip_bytes(attribute_length);
 }
@@ -1654,6 +1659,26 @@ void java_bytecode_parsert::rinner_classes_attribute(
   }
 }
 
+/// Corresponds to the element_value structure
+/// Described in Java 8 specification 4.7.5
+/// https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html#jvms-4.7.5
+/// Parses the Exceptions attribute for the current method,
+/// and returns a vector of exceptions.
+std::vector<irep_idt> java_bytecode_parsert::rexceptions_attribute()
+{
+  u2 number_of_exceptions = read_u2();
+
+  std::vector<irep_idt> exceptions;
+  for(size_t i = 0; i < number_of_exceptions; i++)
+  {
+    u2 exception_index_table = read_u2();
+    const irep_idt exception_name =
+      constant(exception_index_table).type().get(ID_C_base_name);
+    exceptions.push_back(exception_name);
+  }
+  return exceptions;
+}
+
 void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
 {
   u2 attribute_name_index=read_u2();

src/util/irep_ids.def

@@ -692,6 +692,7 @@ IREP_ID_TWO(C_temporary_avoided, #temporary_avoided)
 IREP_ID_TWO(C_qualifier, #qualifier)
 IREP_ID_TWO(C_array_ini, #array_ini)
 IREP_ID_ONE(super_class)
+IREP_ID_ONE(exceptions_thrown_list)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.h in their source tree and

src/util/std_types.h

@@ -912,6 +912,16 @@ class code_typet:public typet
     return (parameterst &)add(ID_parameters).get_sub();
   }
 
+  const std::vector<irept> &throws_exceptions() const
+  {
+    return find(ID_exceptions_thrown_list).get_sub();
+  }
+
+  std::vector<irept> &throws_exceptions()
+  {
+    return add(ID_exceptions_thrown_list).get_sub();
+  }
+
   bool get_inlined() const
   {
     return get_bool(ID_C_inlined);