Move generate_class_stub out of java_bytecode_convert_classt and to java_utils.cpp and use it to generate stubs for exceptions

Author: cristina-david

src/java_bytecode/Makefile

@@ -5,6 +5,7 @@ SRC = bytecode_info.cpp \
       jar_file.cpp \
       java_bytecode_convert_class.cpp \
       java_bytecode_convert_method.cpp \
+      java_bytecode_instrument.cpp \
       java_bytecode_internal_additions.cpp \
       java_bytecode_language.cpp \
       java_bytecode_parse_tree.cpp \
@@ -16,7 +17,6 @@ SRC = bytecode_info.cpp \
       java_class_loader.cpp \
       java_class_loader_limit.cpp \
       java_entry_point.cpp \
-      java_bytecode_instrument.cpp \
       java_local_variable_table.cpp \
       java_object_factory.cpp \
       java_pointer_casts.cpp \

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_types.h"
 #include "java_bytecode_convert_method.h"
 #include "java_bytecode_language.h"
+#include "java_utils.h"
 
 #include <util/arith_tools.h>
 #include <util/namespace.h>
@@ -56,7 +57,10 @@ class java_bytecode_convert_classt:public messaget
       string_preprocess.add_string_type(
         parse_tree.parsed_class.name, symbol_table);
     else if(!loading_success)
-      generate_class_stub(parse_tree.parsed_class.name);
+      generate_class_stub(
+        parse_tree.parsed_class.name,
+        symbol_table,
+        get_message_handler());
   }
 
   typedef java_bytecode_parse_treet::classt classt;
@@ -73,7 +77,6 @@ class java_bytecode_convert_classt:public messaget
   void convert(const classt &c);
   void convert(symbolt &class_symbol, const fieldt &f);
 
-  void generate_class_stub(const irep_idt &class_name);
   void add_array_types();
 };
 
@@ -171,40 +174,6 @@ void java_bytecode_convert_classt::convert(const classt &c)
     java_root_class(*class_symbol);
 }
 
-void java_bytecode_convert_classt::generate_class_stub(
-  const irep_idt &class_name)
-{
-  class_typet class_type;
-
-  class_type.set_tag(class_name);
-  class_type.set(ID_base_name, class_name);
-
-  class_type.set(ID_incomplete_class, true);
-
-  // produce class symbol
-  symbolt new_symbol;
-  new_symbol.base_name=class_name;
-  new_symbol.pretty_name=class_name;
-  new_symbol.name="java::"+id2string(class_name);
-  class_type.set(ID_name, new_symbol.name);
-  new_symbol.type=class_type;
-  new_symbol.mode=ID_java;
-  new_symbol.is_type=true;
-
-  symbolt *class_symbol;
-
-  if(symbol_table.move(new_symbol, class_symbol))
-  {
-    warning() << "stub class symbol " << new_symbol.name
-              << " already exists" << eom;
-  }
-  else
-  {
-    // create the class identifier etc
-    java_root_class(*class_symbol);
-  }
-}
-
 void java_bytecode_convert_classt::convert(
   symbolt &class_symbol,
   const fieldt &f)

src/java_bytecode/java_bytecode_instrument.cpp

@@ -15,21 +15,25 @@ Date:   June 2017
 
 #include <goto-programs/goto_functions.h>
 
+#include "java_bytecode_convert_class.h"
 #include "java_bytecode_instrument.h"
 #include "java_entry_point.h"
 #include "java_object_factory.h"
 #include "java_root_class.h"
 #include "java_types.h"
+#include "java_utils.h"
 
-class java_bytecode_instrumentt
+class java_bytecode_instrumentt:public messaget
 {
 public:
   java_bytecode_instrumentt(
     symbol_tablet &_symbol_table,
     const bool _throw_runtime_exceptions,
+    message_handlert &_message_handler,
     const size_t _max_array_length):
     symbol_table(_symbol_table),
     throw_runtime_exceptions(_throw_runtime_exceptions),
+    message_handler(_message_handler),
     max_array_length(_max_array_length)
     {
     }
@@ -38,8 +42,9 @@ class java_bytecode_instrumentt
 
 protected:
   symbol_tablet &symbol_table;
-  bool throw_runtime_exceptions;
-  size_t max_array_length;
+  const bool throw_runtime_exceptions;
+  message_handlert &message_handler;
+  const size_t max_array_length;
 
   codet throw_exception(
     const exprt &cond,
@@ -92,25 +97,12 @@ codet java_bytecode_instrumentt::throw_exception(
 
   if(!symbol_table.has_symbol(exc_obj_name))
   {
-    // for now, create a class stub
-    // TODO: model exceptions and use that model
-    class_typet class_type;
-    class_type.set_tag(exc_name);
-    class_type.set(ID_base_name, exc_name);
-    class_type.set(ID_incomplete_class, true);
-
-    // produce class symbol
-    symbolt exc_symbol;
-    exc_symbol.base_name=exc_name;
-    exc_symbol.pretty_name=exc_name;
-    exc_symbol.name="java::"+id2string(exc_name);
-    class_type.set(ID_name, exc_symbol.name);
-    exc_symbol.type=class_type;
-    exc_symbol.mode=ID_java;
-    exc_symbol.is_type=true;
-    symbol_table.add(exc_symbol);
-    // create the class identifier
-    java_root_class(exc_symbol);
+    generate_class_stub(
+      exc_name,
+      symbol_table,
+      get_message_handler());
+    const symbolt &exc_symbol=symbol_table.lookup(
+      "java::"+id2string(exc_name));
 
     // create the exception object
     exc=object_factory(
@@ -512,12 +504,14 @@ void java_bytecode_instrumentt::operator()(exprt &expr)
 /// in order to be able to call the object factory to create exceptions.
 void java_bytecode_instrument(
   symbol_tablet &symbol_table,
-  bool throw_runtime_exceptions,
-  size_t max_array_length)
+  const bool throw_runtime_exceptions,
+  message_handlert &message_handler,
+  const size_t max_array_length)
 {
   java_bytecode_instrumentt instrument(
     symbol_table,
     throw_runtime_exceptions,
+    message_handler,
     max_array_length);
 
   Forall_symbols(s_it, symbol_table.symbols)

src/java_bytecode/java_bytecode_instrument.h

@@ -14,6 +14,6 @@ Date:   June 2017
 void java_bytecode_instrument(
   symbol_tablet &symbol_table,
   const bool throw_runtime_exceptions,
+  message_handlert &_message_handler,
   const size_t max_array_length);
-
 #endif

src/java_bytecode/java_bytecode_language.cpp

@@ -444,6 +444,7 @@ bool java_bytecode_languaget::typecheck(
   java_bytecode_instrument(
     symbol_table,
     throw_runtime_exceptions,
+    get_message_handler(),
     max_nondet_array_length);
 
   // now typecheck all

src/java_bytecode/java_utils.cpp

@@ -6,12 +6,13 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-
+#include <util/invariant.h>
+#include <util/message.h>
 #include <util/prefix.h>
 #include <util/std_types.h>
-#include <util/invariant.h>
 #include <util/string_utils.h>
 
+#include "java_root_class.h"
 #include "java_utils.h"
 #include "java_types.h"
 
@@ -54,7 +55,47 @@ unsigned java_method_parameter_slots(const code_typet &t)
   return slots;
 }
 
+
 const std::string java_class_to_package(const std::string &canonical_classname)
 {
   return trim_from_last_delimiter(canonical_classname, '.');
 }
+
+void generate_class_stub(
+  const irep_idt &class_name,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler)
+{
+  class_typet class_type;
+
+  class_type.set_tag(class_name);
+  class_type.set(ID_base_name, class_name);
+
+  class_type.set(ID_incomplete_class, true);
+
+  // produce class symbol
+  symbolt new_symbol;
+  new_symbol.base_name=class_name;
+  new_symbol.pretty_name=class_name;
+  new_symbol.name="java::"+id2string(class_name);
+  class_type.set(ID_name, new_symbol.name);
+  new_symbol.type=class_type;
+  new_symbol.mode=ID_java;
+  new_symbol.is_type=true;
+
+  symbolt *class_symbol;
+
+  if(symbol_table.move(new_symbol, class_symbol))
+  {
+    messaget message(message_handler);
+    message.warning() <<
+      "stub class symbol " <<
+      new_symbol.name <<
+      " already exists" << messaget::eom;
+  }
+  else
+  {
+    // create the class identifier etc
+    java_root_class(*class_symbol);
+  }
+}

src/java_bytecode/java_utils.h

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 
 #include <util/type.h>
+#include <util/symbol_table.h>
 
 #include "java_bytecode_parse_tree.h"
 
@@ -16,6 +17,11 @@ Author: Daniel Kroening, [email protected]
 
 bool java_is_array_type(const typet &type);
 
+void generate_class_stub(
+  const irep_idt &class_name,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler);
+
 /// Returns the number of JVM local variables (slots) taken by a local variable
 /// that, when translated to goto, has type \p t.
 unsigned java_local_variable_slots(const typet &t);