Do type-checking as a function pass

After convert each function in convert_lazy_method call instrument and typecheck

Author: NathanJPhillips

src/java_bytecode/java_bytecode_instrument.cpp

@@ -598,7 +598,9 @@ void java_bytecode_instrument_symbol(
     message_handler);
   INVARIANT(
     symbol.value.id()==ID_code,
-    "java_bytecode_instrument expects a code-typed symbol");
+    "java_bytecode_instrument expects a code-typed symbol but was called with"
+      " " + id2string(symbol.name) + " which has a value with an id of " +
+      id2string(symbol.value.id()));
   instrument(symbol.value);
 }
 

src/java_bytecode/java_bytecode_language.cpp

@@ -372,12 +372,33 @@ void java_bytecode_languaget::methods_provided(id_sett &methods) const
 /// to have a value representing the method body identical to that produced
 /// using eager method conversion.
 /// \param function_id: method ID to convert
-/// \param symbol_table: global symbol table
+/// \param symtab: global symbol table
 void java_bytecode_languaget::convert_lazy_method(
   const irep_idt &function_id,
-  symbol_tablet &symbol_table)
+  symbol_tablet &symtab)
 {
+  const symbolt &symbol = symtab.lookup_ref(function_id);
+  if(symbol.value.is_not_nil())
+    return;
+
+  journalling_symbol_tablet symbol_table=
+    journalling_symbol_tablet::wrap(symtab);
+
   convert_single_method(function_id, symbol_table);
+
+  // Instrument runtime exceptions (unless symbol is a stub)
+  if(symbol.value.is_not_nil())
+  {
+    java_bytecode_instrument_symbol(
+      symbol_table,
+      symbol_table.get_writeable_ref(function_id),
+      throw_runtime_exceptions,
+      get_message_handler());
+  }
+
+  // now typecheck this function
+  java_bytecode_typecheck_updated_symbols(
+    symbol_table, get_message_handler(), string_refinement_enabled);
 }
 
 /// \brief Convert a method (one whose type is known but whose body hasn't

src/java_bytecode/java_bytecode_typecheck.cpp

@@ -38,34 +38,35 @@ void java_bytecode_typecheckt::typecheck()
 {
   // The hash table iterators are not stable,
   // and we might add new symbols.
-
-  std::vector<irep_idt> identifiers;
+  journalling_symbol_tablet::changesett identifiers;
   identifiers.reserve(symbol_table.symbols.size());
   forall_symbols(s_it, symbol_table.symbols)
-    identifiers.push_back(s_it->first);
+    identifiers.insert(s_it->first);
+  typecheck(identifiers);
+}
 
+void java_bytecode_typecheckt::typecheck(
+  const journalling_symbol_tablet::changesett &identifiers)
+{
   // We first check all type symbols,
   // recursively doing base classes first.
   for(const irep_idt &id : identifiers)
   {
     symbolt &symbol=*symbol_table.get_writeable(id);
-    if(!symbol.is_type)
-      continue;
-    typecheck_type_symbol(symbol);
+    if(symbol.is_type)
+      typecheck_type_symbol(symbol);
   }
-
   // We now check all non-type symbols
   for(const irep_idt &id : identifiers)
   {
     symbolt &symbol=*symbol_table.get_writeable(id);
-    if(symbol.is_type)
-      continue;
-    typecheck_non_type_symbol(symbol);
+    if(!symbol.is_type)
+      typecheck_non_type_symbol(symbol);
   }
 }
 
 bool java_bytecode_typecheck(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   bool string_refinement_enabled)
 {
@@ -74,6 +75,16 @@ bool java_bytecode_typecheck(
   return java_bytecode_typecheck.typecheck_main();
 }
 
+void java_bytecode_typecheck_updated_symbols(
+  journalling_symbol_tablet &symbol_table,
+  message_handlert &message_handler,
+  bool string_refinement_enabled)
+{
+  java_bytecode_typecheckt java_bytecode_typecheck(
+    symbol_table, message_handler, string_refinement_enabled);
+  return java_bytecode_typecheck.typecheck(symbol_table.get_updated());
+}
+
 bool java_bytecode_typecheck(
   exprt &expr,
   message_handlert &message_handler,

src/java_bytecode/java_bytecode_typecheck.h

@@ -15,15 +15,20 @@ Author: Daniel Kroening, [email protected]
 #include <set>
 #include <map>
 
-#include <util/symbol_table.h>
+#include <util/journalling_symbol_table.h>
 #include <util/typecheck.h>
 #include <util/namespace.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 
 bool java_bytecode_typecheck(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler,
+  bool string_refinement_enabled);
+
+void java_bytecode_typecheck_updated_symbols(
+  journalling_symbol_tablet &symbol_table,
   message_handlert &message_handler,
   bool string_refinement_enabled);
 
@@ -36,7 +41,7 @@ class java_bytecode_typecheckt:public typecheckt
 {
 public:
   java_bytecode_typecheckt(
-    symbol_tablet &_symbol_table,
+    symbol_table_baset &_symbol_table,
     message_handlert &_message_handler,
     bool _string_refinement_enabled):
     typecheckt(_message_handler),
@@ -49,10 +54,11 @@ class java_bytecode_typecheckt:public typecheckt
   virtual ~java_bytecode_typecheckt() { }
 
   virtual void typecheck();
+  void typecheck(const journalling_symbol_tablet::changesett &identifiers);
   virtual void typecheck_expr(exprt &expr);
 
 protected:
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
   const namespacet ns;
   bool string_refinement_enabled;