fixes for Java virtual method calls

Author: Daniel Kroening

src/cbmc/cbmc_parse_options.cpp

@@ -862,7 +862,7 @@ bool cbmc_parse_optionst::process_goto_program(
         symbol_table, get_message_handler(), goto_functions);
 
     // remove function pointers
-    status() << "Removal of Function Pointers Virtual Functions" << eom;
+    status() << "Removal of function pointers and virtual functions" << eom;
     remove_function_pointers(symbol_table, goto_functions,
       cmdline.isset("pointer-check"));
     remove_virtual_functions(symbol_table, goto_functions);

src/java_bytecode/java_bytecode_convert.cpp

@@ -742,45 +742,40 @@ codet java_bytecode_convertt::convert_instructions(
         // info for that type, and are instances of java.lang.Class
         assert(!call.arguments().empty());
 
-        exprt this_arg=call.arguments().front();
+        exprt &this_arg=call.arguments().front();
 
         if(this_arg.id()==ID_type)
         {
           irep_idt class_id=this_arg.type().get(ID_identifier);
           symbol_typet java_lang_Class("java::java.lang.Class");
-          symbol_exprt symbol_expr("java::"+id2string(class_id)+"@class_model", java_lang_Class);
+          symbol_exprt symbol_expr(id2string(class_id)+"@class_model", java_lang_Class);
           address_of_exprt address_of_expr(symbol_expr);
           this_arg=address_of_expr;
         }
 
         assert(this_arg.type().id()==ID_pointer);
-        
-        std::cout << "F: " << arg0.pretty() << "\n";
       }
 
       const typet &return_type=code_type.return_type();
 
-      if(ID_empty != return_type.id())
+      if(return_type.id()!=ID_empty)
       {
-        call.lhs() = tmp_variable(return_type);
+        call.lhs()=tmp_variable(return_type);
         results.resize(1);
-        results[0] = call.lhs();
+        results[0]=call.lhs();
       }
 
       if(is_virtual)
       {
+        assert(use_this);
         assert(!call.arguments().empty());
         const exprt &this_arg=call.arguments().front();
 
-        #if 0
-        call.function()=make_vtable_function(arg0, this_arg);
-        #else
         call.function()=make_virtual_function(
           to_symbol_expr(arg0), this_arg);
-        #endif
       }
       else
-        call.function() = arg0;
+        call.function()=arg0;
 
       call.function().add_source_location()=i_it->source_location;
       c = call;

src/solvers/flattening/boolbv.h

@@ -243,6 +243,9 @@ class boolbvt:public arrayst
 
   typedef std::vector<std::size_t> offset_mapt;
   void build_offset_map(const struct_typet &src, offset_mapt &dest);
+  
+  // strings
+  numbering<irep_idt> string_numbering;
 };
 
 #endif

src/solvers/flattening/boolbv_constant.cpp

@@ -51,6 +51,13 @@ void boolbvt::convert_constant(const constant_exprt &expr, bvt &bv)
 
     return;
   }
+  else if(expr_type.id()==ID_string)
+  {
+    // we use the numbering for strings
+    std::size_t number=string_numbering(expr.get_value());
+    bv=bv_utils.build_constant(number, bv.size());
+    return;
+  }
   else if(expr_type.id()==ID_range)
   {
     mp_integer from=to_range_type(expr_type).get_from();

src/solvers/flattening/boolbv_get.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
 #include <util/threeval.h>
+#include <util/std_types.h>
 
 #include "boolbv.h"
 #include "boolbv_type.h"
@@ -260,6 +261,17 @@ exprt boolbvt::bv_get_rec(
   switch(bvtype)
   {
   case IS_UNKNOWN:
+    if(type.id()==ID_string)
+    {
+      mp_integer int_value=binary2integer(value, false);
+      irep_idt s;
+      if(int_value>=string_numbering.size())
+        s=irep_idt();
+      else
+        s=string_numbering[int_value.to_long()];
+
+      return constant_exprt(s, type);
+    }
     break;
 
   case IS_RANGE:

src/solvers/flattening/boolbv_struct.cpp

@@ -35,7 +35,7 @@ void boolbvt::convert_struct(const struct_exprt &expr, bvt &bv)
     throw "struct: wrong number of arguments";
 
   bv.resize(width);
-
+  
   std::size_t offset=0, i=0;
 
   for(struct_typet::componentst::const_iterator

src/solvers/flattening/boolbv_width.cpp

@@ -247,6 +247,8 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   {
     entry.total_width=to_c_bit_field_type(type).get_width();
   }
+  else if(type_id==ID_string)
+    entry.total_width=32;
 
   return entry;
 }

src/util/pointer_offset_size.cpp

@@ -224,7 +224,7 @@ mp_integer pointer_offset_bits(
   }
   else if(type.id()==ID_string)
   {
-    return config.ansi_c.int_width;
+    return 32;
   }
   else
     return mp_integer(-1);
@@ -486,7 +486,7 @@ exprt size_of_expr(
   else if(type.id()==ID_string)
   {
     return from_integer(
-      config.ansi_c.int_width, signedbv_typet(config.ansi_c.pointer_width));
+      32/8, signedbv_typet(config.ansi_c.pointer_width));
   }
   else
     return nil_exprt();