take tautschnig's comments into account

Author: mgudemann

src/java_bytecode/expr2java.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/arith_tools.h>
 
 #include <ansi-c/c_qualifiers.h>
+#include <ansi-c/c_misc.h>
 #include <ansi-c/expr2c_class.h>
 
 #include "java_types.h"
@@ -216,7 +217,8 @@ std::string expr2javat::convert_constant(
     dest.reserve(char_representation_length);
 
     mp_integer int_value;
-    to_integer(src, int_value);
+    if(!to_integer(src, int_value))
+      assert(false);
 
     dest+="(char)'";
 
@@ -238,7 +240,8 @@ std::string expr2javat::convert_constant(
   {
     // No byte-literals in Java, so just cast:
     mp_integer int_value;
-    to_integer(src, int_value);
+    if(!to_integer(src, int_value))
+      assert(false);
     std::string dest="(byte)";
     dest+=integer2string(int_value);
     return dest;
@@ -247,7 +250,8 @@ std::string expr2javat::convert_constant(
   {
     // No short-literals in Java, so just cast:
     mp_integer int_value;
-    to_integer(src, int_value);
+    if(!to_integer(src, int_value))
+      assert(false);
     std::string dest="(short)";
     dest+=integer2string(int_value);
     return dest;
@@ -482,7 +486,7 @@ std::string expr2javat::convert(
   const typet &type=ns.follow(src.type());
   if(src.id()=="java-this")
     return convert_java_this(src, precedence=15);
-  if(src.id()=="java_instanceof")
+  if(src.id()==ID_java_instanceof)
     return convert_java_instanceof(src, precedence=15);
   else if(src.id()==ID_side_effect &&
           (src.get(ID_statement)==ID_java_new ||
@@ -506,7 +510,7 @@ std::string expr2javat::convert(
       ")";
   }
   else if(src.id()==ID_java_string_literal)
-    return '"'+id2string(src.get(ID_value))+'"'; // TODO: add escaping as needed
+    return '"'+MetaString(src.get_string(ID_value))+'"';
   else if(src.id()==ID_constant && (type.id()==ID_bool || type.id()==ID_c_bool))
   {
     if(src.is_true())

src/java_bytecode/expr2java.h

@@ -12,10 +12,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <string>
 #include <ansi-c/expr2c_class.h>
 
-class exprt;
-class namespacet;
-class typet;
-
 class expr2javat:public expr2ct
 {
 public:
@@ -56,7 +52,8 @@ class expr2javat:public expr2ct
     const std::string &declarator);
 
   // length of string representation of Java Char
-  const std::size_t char_representation_length=14;
+  // representation is '\u0000'
+  const std::size_t char_representation_length=8;
 };
 
 std::string expr2java(const exprt &expr, const namespacet &ns);

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -173,8 +173,8 @@ void java_bytecode_convert_classt::generate_class_stub(
 
   if(symbol_table.move(new_symbol, class_symbol))
   {
-    warning() << "stub class symbol "+
-      id2string(new_symbol.name)+" already exists";
+    warning() << "stub class symbol " << new_symbol.name
+              << " already exists" << eom;
   }
   else
   {
@@ -225,10 +225,7 @@ void java_bytecode_convert_classt::convert(
       symbol_table.symbols.erase(s_it); // erase, we stubbed it
 
     if(symbol_table.add(new_symbol))
-    {
-      error() << "failed to add static field symbol" << eom;
-      throw 0;
-    }
+      assert(false && "failed to add static field symbol");
   }
   else
   {
@@ -276,6 +273,8 @@ void java_bytecode_convert_classt::add_array_types()
     // we have the base class, java.lang.Object, length and data
     // of appropriate type
     struct_type.set_tag(symbol_type.get_identifier());
+
+    struct_type.components().reserve(3);
     struct_typet::componentt
       comp0("@java.lang.Object", symbol_typet("java::java.lang.Object"));
     struct_type.components().push_back(comp0);

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -26,7 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_bytecode_convert_method_class.h"
 #include "bytecode_info.h"
 #include "java_types.h"
-#include "java_utils.h"
 
 #include <limits>
 #include <algorithm>
@@ -415,7 +414,7 @@ codet java_bytecode_convert_methodt::get_array_bounds_check(
   const exprt &idx,
   const source_locationt& original_sloc)
 {
-  constant_exprt intzero=as_number(0, java_int_type());
+  constant_exprt intzero=from_integer(0, java_int_type());
   binary_relation_exprt gezero(idx, ID_ge, intzero);
   const member_exprt length_field(arraystruct, "length", java_int_type());
   binary_relation_exprt ltlength(idx, ID_lt, length_field);
@@ -937,7 +936,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
         // The stack isn't modified.
         // TODO: convert assertions to exceptions.
         assert(op.size()==1 && results.size()==1);
-        binary_predicate_exprt check(op[0], "java_instanceof", arg0);
+        binary_predicate_exprt check(op[0], ID_java_instanceof, arg0);
         c=code_assertt(check);
         c.add_source_location().set_comment("Dynamic cast check");
         c.add_source_location().set_property_class("bad-dynamic-cast");
@@ -1011,12 +1010,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
       }
 
       code_function_callt call;
-      source_locationt loc;
-      loc=i_it->source_location;
+      source_locationt loc=i_it->source_location;
       loc.set_function(method_id);
-      source_locationt &source_loc=loc;
 
-      call.add_source_location()=source_loc;
+      call.add_source_location()=loc;
       call.arguments()=pop(parameters.size());
 
       // double-check a bit
@@ -1089,7 +1086,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
         call.function()=symbol_exprt(arg0.get(ID_identifier), arg0.type());
       }
 
-      call.function().add_source_location()=source_loc;
+      call.function().add_source_location()=loc;
       c=call;
     }
     else if(statement=="return")
@@ -1245,7 +1242,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       irep_idt number=to_constant_expr(arg0).get_value();
       code_gotot code_goto(label(number));
       c=code_goto;
-      results[0]=as_number(
+      results[0]=from_integer(
         std::next(i_it)->address,
         pointer_typet(void_typet(), 64));
     }
@@ -1267,9 +1264,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
           branches.move_to_operands(g);
         else
         {
-          code_ifthenelset
-            branch;
-          auto address_ptr=as_number(
+          code_ifthenelset branch;
+          auto address_ptr=from_integer(
             jsr_ret_targets[idx],
             pointer_typet(void_typet(), 64));
           branch.cond()=equal_exprt(retvar, address_ptr);
@@ -1311,9 +1307,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
       }
       else
       {
-        const size_t value(arg0.get_unsigned_int(ID_value));
+        const unsigned value(arg0.get_unsigned_int(ID_value));
         const typet type=java_type_from_char(statement[0]);
-        results[0]=as_number(value, type);
+        results[0]=from_integer(value, type);
       }
     }
     else if(statement==patternt("?ipush"))
@@ -1326,8 +1322,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       irep_idt number=to_constant_expr(arg0).get_value();
       assert(op.size()==2 && results.empty());
 
-      code_ifthenelset
-        code_branch;
+      code_ifthenelset code_branch;
       const irep_idt cmp_op=get_if_cmp_operator(statement);
 
       binary_relation_exprt condition(op[0], cmp_op, op[1]);
@@ -1360,8 +1355,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       irep_idt number=to_constant_expr(arg0).get_value();
       assert(op.size()==1 && results.empty());
 
-      code_ifthenelset
-        code_branch;
+      code_ifthenelset code_branch;
       code_branch.cond()=
         binary_relation_exprt(op[0], id, gen_zero(op[0].type()));
       code_branch.cond().add_source_location()=i_it->source_location;
@@ -1378,8 +1372,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       irep_idt number=to_constant_expr(arg0).get_value();
       assert(op.size()==1 && results.empty());
-      code_ifthenelset
-        code_branch;
+      code_ifthenelset code_branch;
       const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
       const exprt rhs(gen_zero(lhs.type()));
       code_branch.cond()=binary_relation_exprt(lhs, ID_notequal, rhs);
@@ -1393,8 +1386,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       assert(op.size()==1 && results.empty());
       irep_idt number=to_constant_expr(arg0).get_value();
-      code_ifthenelset
-        code_branch;
+      code_ifthenelset code_branch;
       const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
       const exprt rhs(gen_zero(lhs.type()));
       code_branch.cond()=binary_relation_exprt(lhs, ID_equal, rhs);
@@ -1506,7 +1498,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       results[0]=
         if_exprt(
           binary_relation_exprt(op[0], ID_equal, op[1]),
-          gen_zero(t),
+          from_integer(0, t),
           greater);
     }
     else if(statement==patternt("?cmp?"))
@@ -1637,11 +1629,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       // set $assertionDisabled to false
       if(field_name.find("$assertionsDisabled")!=std::string::npos)
-      {
-        exprt e;
-        e.make_false();
-        c=code_assignt(symbol_expr, e);
-      }
+        c=code_assignt(symbol_expr, false_exprt());
     }
     else if(statement=="putfield")
     {
@@ -1721,7 +1709,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       if(!disable_runtime_checks)
       {
         // TODO make this throw NegativeArrayIndexException instead.
-        constant_exprt intzero=as_number(0, java_int_type());
+        constant_exprt intzero=from_integer(0, java_int_type());
         binary_relation_exprt gezero(op[0], ID_ge, intzero);
         code_assertt check(gezero);
         check.add_source_location().set_comment("Array size < 0");
@@ -1731,7 +1719,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       }
       if(max_array_length!=0)
       {
-        constant_exprt size_limit=as_number(max_array_length, java_int_type());
+        constant_exprt size_limit=from_integer(max_array_length, java_int_type());
         binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
         code_assumet assume_le_max_size(le_max_size);
         c.move_to_operands(assume_le_max_size);
@@ -1750,7 +1738,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       op=pop(dimension);
       assert(results.size()==1);
 
-      const pointer_typet ref_type=pointer_typet(arg0.type());
+      const pointer_typet ref_type(arg0.type());
 
       side_effect_exprt java_new_array(ID_java_new_array, ref_type);
       java_new_array.operands()=op;

src/java_bytecode/java_bytecode_language.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "java_class_loader.h"
 
+#define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
+
 class java_bytecode_languaget:public languaget
 {
 public:
@@ -39,7 +41,7 @@ class java_bytecode_languaget:public languaget
 
   virtual ~java_bytecode_languaget();
   java_bytecode_languaget():
-    max_nondet_array_length(5),
+    max_nondet_array_length(MAX_NONDET_ARRAY_LENGTH_DEFAULT),
     max_user_array_length(0) { }
 
   bool from_expr(

src/java_bytecode/java_bytecode_parser.cpp

@@ -1449,16 +1449,16 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
     u2 sourcefile_index=read_u2();
     irep_idt sourcefile_name;
 
-    std::string fqn=std::string(id2string(parsed_class.name));
+    std::string fqn(id2string(parsed_class.name));
     size_t last_index=fqn.find_last_of(".");
     if(last_index==std::string::npos)
       sourcefile_name=pool_entry(sourcefile_index).s;
     else
     {
       std::string packageName=fqn.substr(0, last_index+1);
       std::replace(packageName.begin(), packageName.end(), '.', '/');
-      const std::string &fullFileName=
-        std::string(packageName+id2string(pool_entry(sourcefile_index).s));
+      const std::string
+        &fullFileName=(packageName+id2string(pool_entry(sourcefile_index).s));
       sourcefile_name=fullFileName;
     }
 

src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -93,9 +93,9 @@ void java_bytecode_typecheckt::typecheck_expr_java_new_array(
 
 static void escape_non_alnum(std::string& toescape)
 {
-  for(size_t idx=0, lim=toescape.size(); idx!=lim; ++idx)
-    if(!isalnum(toescape[idx]))
-      toescape[idx]='_';
+  for(auto &ch : toescape)
+  if(!isalnum(ch))
+    ch='_';
 }
 
 /*******************************************************************\