Lazy function loading

regression/jbmc-strings/StaticCharMethods05/test.desc

@@ -3,7 +3,6 @@ StaticCharMethods05.class
 --refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
-null-pointer-exception\.14\] Throw null: FAILURE
 ^\[.*assertion\.1\] .* line 12 .* FAILURE$
 ^\[.*assertion\.2\] .* line 22 .* FAILURE$
 ^VERIFICATION FAILED$

src/clobber/clobber_parse_options.cpp

@@ -32,6 +32,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/xml_goto_trace.h>
+#include <goto-programs/remove_java_new.h>
 
 #include <goto-instrument/dump_c.h>
 
@@ -207,6 +208,8 @@ bool clobber_parse_optionst::process_goto_program(
   goto_modelt &goto_model)
 {
   {
+    remove_java_new(goto_model, get_message_handler());
+
     // do partial inlining
     status() << "Partial Inlining" << eom;
     goto_partial_inline(goto_model, get_message_handler());

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -37,6 +37,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/link_to_library.h>
+#include <goto-programs/remove_java_new.h>
 
 #include <analyses/is_threaded.h>
 #include <analyses/goto_check.h>
@@ -735,6 +736,8 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     link_to_library(goto_model, ui_message_handler);
     #endif
 
+    remove_java_new(goto_model, get_message_handler());
+
     // remove function pointers
     status() << "Removing function pointers and virtual functions" << eom;
     remove_function_pointers(

src/goto-cc/compile.cpp

@@ -483,14 +483,7 @@ bool compilet::parse(const std::string &file_name)
 
   languagep->set_message_handler(get_message_handler());
 
-  language_filet language_file;
-
-  std::pair<language_filest::file_mapt::iterator, bool>
-  res=language_files.file_map.insert(
-    std::pair<std::string, language_filet>(file_name, language_file));
-
-  language_filet &lf=res.first->second;
-  lf.filename=file_name;
+  language_filet &lf=language_files.add_file(file_name);
   lf.language=std::move(languagep);
 
   if(mode==PREPROCESS_ONLY)
@@ -640,7 +633,7 @@ bool compilet::parse_source(const std::string &file_name)
     return true;
 
   // so we remove it from the list afterwards
-  language_files.file_map.erase(file_name);
+  language_files.remove_file(file_name);
   return false;
 }
 
@@ -691,7 +684,7 @@ void compilet::add_compiler_specific_defines(configt &config) const
 
 void compilet::convert_symbols(goto_functionst &dest)
 {
-  goto_convert_functionst converter(symbol_table, dest, get_message_handler());
+  goto_convert_functionst converter(symbol_table, get_message_handler());
 
   // the compilation may add symbols!
 
@@ -724,7 +717,7 @@ void compilet::convert_symbols(goto_functionst &dest)
           s_it->second.value.is_not_nil())
       {
         debug() << "Compiling " << s_it->first << eom;
-        converter.convert_function(s_it->first);
+        converter.convert_function(s_it->first, dest.function_map[s_it->first]);
         symbol_table.get_writeable_ref(*it).value=exprt("compiled");
       }
     }

src/goto-diff/goto_diff_parse_options.cpp

@@ -37,6 +37,7 @@ Author: Peter Schrammel
 #include <goto-programs/string_instrumentation.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/link_to_library.h>
+#include <goto-programs/remove_java_new.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
 
@@ -394,9 +395,11 @@ bool goto_diff_parse_optionst::process_goto_program(
   {
     namespacet ns(symbol_table);
 
+    remove_java_new(goto_model, get_message_handler());
+
     // Remove inline assembler; this needs to happen before
     // adding the library.
-    remove_asm(symbol_table, goto_functions);
+    remove_asm(goto_model);
 
     // add the library
     link_to_library(symbol_table, goto_functions, ui_message_handler);

src/goto-programs/Makefile

@@ -27,6 +27,7 @@ SRC = basic_blocks.cpp \
       interpreter.cpp \
       interpreter_evaluate.cpp \
       json_goto_trace.cpp \
+      lazy_goto_model.cpp \
       link_goto_model.cpp \
       link_to_library.cpp \
       loop_ids.cpp \
@@ -44,6 +45,7 @@ SRC = basic_blocks.cpp \
       remove_exceptions.cpp \
       remove_function_pointers.cpp \
       remove_instanceof.cpp \
+      remove_java_new.cpp \
       remove_returns.cpp \
       remove_skip.cpp \
       remove_static_init_loops.cpp \

src/goto-programs/builtin_functions.cpp

@@ -33,6 +33,7 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/string_constant.h>
 
 #include "format_strings.h"
+#include "class_identifier.h"
 
 void goto_convertt::do_prob_uniform(
   const exprt &lhs,
@@ -539,68 +540,6 @@ void goto_convertt::do_cpp_new(
   dest.destructive_append(tmp_initializer);
 }
 
-void set_class_identifier(
-  struct_exprt &expr,
-  const namespacet &ns,
-  const symbol_typet &class_type)
-{
-  const struct_typet &struct_type=
-    to_struct_type(ns.follow(expr.type()));
-  const struct_typet::componentst &components=struct_type.components();
-
-  if(components.empty())
-    return;
-  assert(!expr.operands().empty());
-
-  if(components.front().get_name()=="@class_identifier")
-  {
-    assert(expr.op0().id()==ID_constant);
-    expr.op0()=constant_exprt(class_type.get_identifier(), string_typet());
-  }
-  else
-  {
-    assert(expr.op0().id()==ID_struct);
-    set_class_identifier(to_struct_expr(expr.op0()), ns, class_type);
-  }
-}
-
-void goto_convertt::do_java_new(
-  const exprt &lhs,
-  const side_effect_exprt &rhs,
-  goto_programt &dest)
-{
-  PRECONDITION(!lhs.is_nil());
-  PRECONDITION(rhs.operands().empty());
-  PRECONDITION(rhs.type().id() == ID_pointer);
-  source_locationt location=rhs.source_location();
-  typet object_type=rhs.type().subtype();
-
-  // build size expression
-  exprt object_size=size_of_expr(object_type, ns);
-  CHECK_RETURN(object_size.is_not_nil());
-
-  // we produce a malloc side-effect, which stays
-  side_effect_exprt malloc_expr(ID_allocate);
-  malloc_expr.copy_to_operands(object_size);
-  // could use true and get rid of the code below
-  malloc_expr.copy_to_operands(false_exprt());
-  malloc_expr.type()=rhs.type();
-
-  goto_programt::targett t_n=dest.add_instruction(ASSIGN);
-  t_n->code=code_assignt(lhs, malloc_expr);
-  t_n->source_location=location;
-
-  // zero-initialize the object
-  dereference_exprt deref(lhs, object_type);
-  exprt zero_object=
-    zero_initializer(object_type, location, ns, get_message_handler());
-  set_class_identifier(
-    to_struct_expr(zero_object), ns, to_symbol_type(object_type));
-  goto_programt::targett t_i=dest.add_instruction(ASSIGN);
-  t_i->code=code_assignt(deref, zero_object);
-  t_i->source_location=location;
-}
-
 void goto_convertt::do_java_new_array(
   const exprt &lhs,
   const side_effect_exprt &rhs,

src/goto-programs/class_identifier.cpp

@@ -71,3 +71,39 @@ exprt get_class_identifier_field(
   exprt deref=dereference_exprt(this_expr, this_expr.type().subtype());
   return build_class_identifier(deref, ns);
 }
+
+/// If expr has its components filled in then sets the `@class_identifier`
+/// member of the struct
+/// \remarks Follows through base class members until it gets to the object
+/// type that contains the `@class_identifier` member
+/// \param expr: An expression that represents a struct
+/// \param ns: The namespace used to resolve symbol referencess in the type of
+/// the struct
+/// \param class_type: A symbol whose identifier is the name of the class
+void set_class_identifier(
+  struct_exprt &expr,
+  const namespacet &ns,
+  const symbol_typet &class_type)
+{
+  const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
+  const struct_typet::componentst &components=struct_type.components();
+
+  if(components.empty())
+    // Presumably this means the type has not yet been determined
+    return;
+  PRECONDITION(!expr.operands().empty());
+
+  if(components.front().get_name()=="@class_identifier")
+  {
+    INVARIANT(
+      expr.op0().id()==ID_constant, "@class_identifier must be a constant");
+    expr.op0()=constant_exprt(class_type.get_identifier(), string_typet());
+  }
+  else
+  {
+    // The first member must be the base class
+    INVARIANT(
+      expr.op0().id()==ID_struct, "Non @class_identifier must be a structure");
+    set_class_identifier(to_struct_expr(expr.op0()), ns, class_type);
+  }
+}

src/goto-programs/class_identifier.h

@@ -15,10 +15,16 @@ Author: Chris Smowton, [email protected]
 class exprt;
 class namespacet;
 class symbol_typet;
+class struct_exprt;
 
 exprt get_class_identifier_field(
   const exprt &this_expr,
   const symbol_typet &suggested_type,
   const namespacet &ns);
 
+void set_class_identifier(
+  struct_exprt &expr,
+  const namespacet &ns,
+  const symbol_typet &class_type);
+
 #endif

src/goto-programs/goto_convert.cpp

@@ -756,10 +756,7 @@ void goto_convertt::convert_assign(
   else if(rhs.id()==ID_side_effect &&
           rhs.get(ID_statement)==ID_java_new)
   {
-    Forall_operands(it, rhs)
-      clean_expr(*it, dest);
-
-    do_java_new(lhs, to_side_effect_expr(rhs), dest);
+    copy(code, ASSIGN, dest);
   }
   else if(rhs.id()==ID_side_effect &&
           rhs.get(ID_statement)==ID_java_new_array)

src/goto-programs/goto_convert_class.h

@@ -142,11 +142,6 @@ class goto_convertt:public messaget
     const side_effect_exprt &rhs,
     goto_programt &dest);
 
-  void do_java_new(
-    const exprt &lhs,
-    const side_effect_exprt &rhs,
-    goto_programt &dest);
-
   void do_java_new_array(
     const exprt &lhs,
     const side_effect_exprt &rhs,

src/goto-programs/goto_convert_functions.cpp

@@ -21,18 +21,16 @@ Date: June 2003
 
 goto_convert_functionst::goto_convert_functionst(
   symbol_tablet &_symbol_table,
-  goto_functionst &_functions,
   message_handlert &_message_handler):
-  goto_convertt(_symbol_table, _message_handler),
-  functions(_functions)
+  goto_convertt(_symbol_table, _message_handler)
 {
 }
 
 goto_convert_functionst::~goto_convert_functionst()
 {
 }
 
-void goto_convert_functionst::goto_convert()
+void goto_convert_functionst::goto_convert(goto_functionst &functions)
 {
   // warning! hash-table iterators are not stable
 
@@ -53,7 +51,7 @@ void goto_convert_functionst::goto_convert()
 
   for(const auto &id : symbol_list)
   {
-    convert_function(id);
+    convert_function(id, functions.function_map[id]);
   }
 
   functions.compute_location_numbers();
@@ -135,10 +133,11 @@ void goto_convert_functionst::add_return(
   t->source_location=source_location;
 }
 
-void goto_convert_functionst::convert_function(const irep_idt &identifier)
+void goto_convert_functionst::convert_function(
+  const irep_idt &identifier,
+  goto_functionst::goto_functiont &f)
 {
   const symbolt &symbol=ns.lookup(identifier);
-  goto_functionst::goto_functiont &f=functions.function_map[identifier];
 
   if(f.body_available())
     return; // already converted
@@ -240,12 +239,11 @@ void goto_convert(
   const unsigned errors_before=
     message_handler.get_message_count(messaget::M_ERROR);
 
-  goto_convert_functionst goto_convert_functions(
-    symbol_table, functions, message_handler);
+  goto_convert_functionst goto_convert_functions(symbol_table, message_handler);
 
   try
   {
-    goto_convert_functions.goto_convert();
+    goto_convert_functions.goto_convert(functions);
   }
 
   catch(int)
@@ -276,12 +274,12 @@ void goto_convert(
   const unsigned errors_before=
     message_handler.get_message_count(messaget::M_ERROR);
 
-  goto_convert_functionst goto_convert_functions(
-    symbol_table, functions, message_handler);
+  goto_convert_functionst goto_convert_functions(symbol_table, message_handler);
 
   try
   {
-    goto_convert_functions.convert_function(identifier);
+    goto_convert_functions.convert_function(
+      identifier, functions.function_map[identifier]);
   }
 
   catch(int)

src/goto-programs/goto_convert_functions.h

@@ -16,6 +16,7 @@ Date: June 2003
 
 #include "goto_model.h"
 #include "goto_convert_class.h"
+#include "goto_functions.h"
 
 // convert it all!
 void goto_convert(
@@ -38,19 +39,18 @@ void goto_convert(
 class goto_convert_functionst:public goto_convertt
 {
 public:
-  void goto_convert();
-  void convert_function(const irep_idt &identifier);
+  void goto_convert(goto_functionst &functions);
+  void convert_function(
+    const irep_idt &identifier,
+    goto_functionst::goto_functiont &result);
 
   goto_convert_functionst(
     symbol_tablet &_symbol_table,
-    goto_functionst &_functions,
     message_handlert &_message_handler);
 
   virtual ~goto_convert_functionst();
 
 protected:
-  goto_functionst &functions;
-
   static bool hide(const goto_programt &);
 
   //

src/goto-programs/goto_functions_template.h

@@ -121,6 +121,8 @@ class goto_functions_templatet
     return *this;
   }
 
+  void unload(const irep_idt &name) { function_map.erase(name); }
+
   void clear()
   {
     function_map.clear();