Clean pr java front end

regression/cbmc-java/NullPointer1/test.desc

@@ -3,7 +3,7 @@ NullPointer1.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer1.java line 16$
+^  file NullPointer1.java line 16 function java::NullPointer1.main:(\[Ljava/lang/String;)V$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/NullPointer2/test.desc

@@ -3,7 +3,7 @@ NullPointer2.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer2.java line 9$
+^  file NullPointer2.java line 9 function java::NullPointer2.main:(\[Ljava/lang/String;)V$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/NullPointer3/test.desc

@@ -3,7 +3,7 @@ NullPointer3.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer3.java line 5$
+^  file NullPointer3.java line 5 function java::NullPointer3.main:(\[Ljava/lang/String;)V bytecode_index 1$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/NullPointer4/test.desc

@@ -3,7 +3,7 @@ NullPointer4.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer4.java line 6$
+^  file NullPointer4.java line 6 function java::NullPointer4.main:(\[Ljava/lang/String;)V$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

src/cegis/refactor/constraint/constraint_factory.cpp

@@ -41,7 +41,7 @@ void create_or_redirect_entry(symbol_tablet &st, goto_functionst &gf)
   if (fmap.end() == it)
   {
     config.main=CONSTRAINT_CALLER;
-    assert(!java_entry_point(st, ID_empty, msg));
+    assert(!java_entry_point(st, ID_empty, msg, false, 0));
     goto_convert(CPROVER_INIT, st, gf, msg);
     goto_convert(goto_functionst::entry_point(), st, gf, msg);
   } else

src/java_bytecode/Makefile

@@ -5,7 +5,8 @@ SRC = java_bytecode_language.cpp java_bytecode_parse_tree.cpp \
       java_bytecode_typecheck_type.cpp java_bytecode_internal_additions.cpp \
       java_root_class.cpp java_bytecode_parser.cpp bytecode_info.cpp \
       java_class_loader.cpp jar_file.cpp java_object_factory.cpp \
-      java_bytecode_convert_method.cpp java_local_variable_table.cpp
+      java_bytecode_convert_method.cpp java_local_variable_table.cpp \
+      java_pointer_casts.cpp java_utils.cpp
 
 INCLUDES= -I ..
 

src/java_bytecode/expr2java.cpp

@@ -15,45 +15,12 @@ Author: Daniel Kroening, [email protected]
 #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"
 #include "expr2java.h"
 
-class expr2javat:public expr2ct
-{
-public:
-  expr2javat(const namespacet &_ns):expr2ct(_ns) { }
-
-  std::string convert(const exprt &src) override
-  {
-    return expr2ct::convert(src);
-  }
-
-  std::string convert(const typet &src) override
-  {
-    return expr2ct::convert(src);
-  }
-
-protected:
-  std::string convert(const exprt &src, unsigned &precedence) override;
-  std::string convert_java_this(const exprt &src, unsigned precedence);
-  std::string convert_java_instanceof(const exprt &src, unsigned precedence);
-  std::string convert_java_new(const exprt &src, unsigned precedence);
-  std::string convert_code_java_delete(const exprt &src, unsigned precedence);
-  std::string convert_struct(const exprt &src, unsigned &precedence) override;
-  std::string convert_code(const codet &src, unsigned indent) override;
-  std::string convert_constant(const constant_exprt &src, unsigned &precedence) override;
-  std::string convert_code_function_call(const code_function_callt &src, unsigned indent);
-
-  std::string convert_rec(
-    const typet &src,
-    const c_qualifierst &qualifiers,
-    const std::string &declarator) override;
-
-  typedef std::unordered_set<std::string, string_hash> id_sett;
-};
-
 /*******************************************************************\
 
 Function: expr2javat::convert_code_function_call
@@ -83,7 +50,6 @@ std::string expr2javat::convert_code_function_call(
     unsigned p;
     std::string lhs_str=convert(src.lhs(), p);
 
-    // TODO: ggf. Klammern je nach p
     dest+=lhs_str;
     dest+='=';
   }
@@ -124,8 +90,10 @@ std::string expr2javat::convert_code_function_call(
       unsigned p;
       std::string arg_str=convert(*it, p);
 
-      if(first) first=false; else dest+=", ";
-      // TODO: ggf. Klammern je nach p
+      if(first)
+        first=false;
+      else
+        dest+=", ";
       dest+=arg_str;
     }
   }
@@ -244,15 +212,16 @@ std::string expr2javat::convert_constant(
   else if(src.type()==java_char_type())
   {
     std::string dest;
-    dest.reserve(10);
+    dest.reserve(char_representation_length);
 
     mp_integer int_value;
-    to_integer(src, int_value);
+    if(!to_integer(src, int_value))
+      assert(false);
 
-    dest+='\'';
+    dest+="(char)'";
 
     if(int_value>=' ' && int_value<127)
-      dest+=(char)(int_value.to_long());
+      dest+=static_cast<char>(int_value.to_long());
     else
     {
       std::string hex=integer2string(int_value, 16);
@@ -265,6 +234,26 @@ std::string expr2javat::convert_constant(
     dest+='\'';
     return dest;
   }
+  else if(src.type()==java_byte_type())
+  {
+    // No byte-literals in Java, so just cast:
+    mp_integer int_value;
+    if(!to_integer(src, int_value))
+      assert(false);
+    std::string dest="(byte)";
+    dest+=integer2string(int_value);
+    return dest;
+  }
+  else if(src.type()==java_short_type())
+  {
+    // No short-literals in Java, so just cast:
+    mp_integer int_value;
+    if(!to_integer(src, int_value))
+      assert(false);
+    std::string dest="(short)";
+    dest+=integer2string(int_value);
+    return dest;
+  }
   else if(src.type()==java_long_type())
   {
     // long integer literals must have 'L' at the end
@@ -319,7 +308,7 @@ std::string expr2javat::convert_rec(
   else if(src==java_double_type())
     return q+"double"+d;
   else if(src==java_boolean_type())
-    return q+"bool"+d;
+    return q+"boolean"+d;
   else if(src==java_byte_type())
     return q+"byte"+d;
   else if(src.id()==ID_code)
@@ -348,7 +337,8 @@ std::string expr2javat::convert_rec(
 
     if(code_type.has_ellipsis())
     {
-      if(!parameters.empty()) dest+=", ";
+      if(!parameters.empty())
+        dest+=", ";
       dest+="...";
     }
 
@@ -491,9 +481,10 @@ std::string expr2javat::convert(
   const exprt &src,
   unsigned &precedence)
 {
+  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 ||
@@ -509,9 +500,22 @@ std::string expr2javat::convert(
   else if(src.id()=="pod_constructor")
     return "pod_constructor";
   else if(src.id()==ID_virtual_function)
-    return convert_function(src, "VIRTUAL_FUNCTION", precedence=16);
+  {
+    return "VIRTUAL_FUNCTION(" +
+      id2string(src.get(ID_C_class)) +
+      "." +
+      id2string(src.get(ID_component_name)) +
+      ")";
+  }
   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())
+      return "true";
+    else
+      return "false";
+  }
   else
     return expr2ct::convert(src, precedence);
 }
@@ -536,7 +540,7 @@ std::string expr2javat::convert_code(
 
   if(statement==ID_java_new ||
      statement==ID_java_new_array)
-    return convert_java_new(src,indent);
+    return convert_java_new(src, indent);
 
   if(statement==ID_function_call)
     return convert_code_function_call(to_code_function_call(src), indent);

src/java_bytecode/expr2java.h

@@ -10,10 +10,51 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_JAVA_BYTECODE_EXPR2JAVA_H
 
 #include <string>
-
-class exprt;
-class namespacet;
-class typet;
+#include <ansi-c/expr2c_class.h>
+
+class expr2javat:public expr2ct
+{
+public:
+  explicit expr2javat(const namespacet &_ns):expr2ct(_ns) { }
+
+  virtual std::string convert(const exprt &src)
+  {
+    return expr2ct::convert(src);
+  }
+
+  virtual std::string convert(const typet &src)
+  {
+    return expr2ct::convert(src);
+  }
+
+protected:
+  virtual std::string convert(const exprt &src, unsigned &precedence);
+  virtual std::string convert_java_this(const exprt &src, unsigned precedence);
+  virtual std::string convert_java_instanceof(
+    const exprt &src,
+    unsigned precedence);
+  virtual std::string convert_java_new(const exprt &src, unsigned precedence);
+  virtual std::string convert_code_java_delete(
+    const exprt &src,
+    unsigned precedence);
+  virtual std::string convert_struct(const exprt &src, unsigned &precedence);
+  virtual std::string convert_code(const codet &src, unsigned indent);
+  virtual std::string convert_constant(
+    const constant_exprt &src,
+    unsigned &precedence);
+  virtual std::string convert_code_function_call(
+    const code_function_callt &src,
+    unsigned indent);
+
+  virtual std::string convert_rec(
+    const typet &src,
+    const c_qualifierst &qualifiers,
+    const std::string &declarator);
+
+  // length of string representation of Java Char
+  // representation is '\u0000'
+  const std::size_t char_representation_length=8;
+};
 
 std::string expr2java(const exprt &expr, const namespacet &ns);
 std::string type2java(const typet &type, const namespacet &ns);