JBMC Java Core models library

.gitignore

@@ -45,6 +45,7 @@ src/ansi-c/gcc_builtin_headers_tm.inc
 src/ansi-c/gcc_builtin_headers_mips.inc
 src/ansi-c/gcc_builtin_headers_power.inc
 src/ansi-c/gcc_builtin_headers_ubsan.inc
+src/java_bytecode/java_core_models.inc
 
 # regression/test files
 *.out
@@ -115,6 +116,8 @@ src/ansi-c/file_converter
 src/ansi-c/file_converter.exe
 src/ansi-c/library/converter
 src/ansi-c/library/converter.exe
+src/java_bytecode/converter
+src/java_bytecode/converter.exe
 src/util/irep_ids_convert
 src/util/irep_ids_convert.exe
 build/

regression/cbmc-java/coreModels/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.class
+--show-symbol-table
+^EXIT=0$
+^SIGNAL=0$
+^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<clinit\>\:\(\)V$
+--
+--
+tests that the core models are  being loaded by checking if the static initializer for the CProver class was

regression/cbmc-java/coreModels/test.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+class test
+{
+  public static void main(String[] args)
+  {
+    int i=CProver.nondetInt();
+    assert(i!=0);
+  }
+}
+

regression/jbmc-strings/java_append_char/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_append_char.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --no-core-models
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

src/java_bytecode/CMakeLists.txt

@@ -1,5 +1,13 @@
-file(GLOB_RECURSE sources "*.cpp" "*.h")
-add_library(java_bytecode ${sources})
+get_filename_component(JAVA_CORE_MODELS_INC "library/java_core_models.inc" REALPATH BASE_DIR ${CMAKE_CURRENT_SOURCE_DIR})
+set_source_files_properties("library/java_core_models.inc" GENERATED)
+
+file(GLOB sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_subdirectory(library)
+
+add_library(java_bytecode ${sources} ${headers} )
+add_dependencies(java_bytecode core_models_files)
+target_sources(java_bytecode PUBLIC ${sources} ${headers})
 
 generic_includes(java_bytecode)
 

src/java_bytecode/Makefile

@@ -40,6 +40,16 @@ CLEANFILES = java_bytecode$(LIBEXT)
 
 all: java_bytecode$(LIBEXT)
 
+clean: clean_library
+
+.PHONY: clean_library
+clean_library:
+	$(MAKE) clean -C library
+
+library/java_core_models.inc:
+	$(MAKE) -C library java_core_models.inc
+
+java_class_loader$(OBJEXT): library/java_core_models.inc
 ###############################################################################
 
 java_bytecode$(LIBEXT): $(OBJ)

src/java_bytecode/jar_file.cpp

@@ -12,10 +12,7 @@ Author: Diffblue Ltd
 #include <util/invariant.h>
 #include "java_class_loader_limit.h"
 
-jar_filet::jar_filet(
-  java_class_loader_limitt &limit,
-  const std::string &filename):
-  m_zip_archive(filename)
+void jar_filet::initialize_file_index(java_class_loader_limitt &limit)
 {
   const size_t file_count=m_zip_archive.get_num_files();
   for(size_t index=0; index<file_count; index++)
@@ -26,6 +23,29 @@ jar_filet::jar_filet(
   }
 }
 
+/// This constructor creates a jar_file object whose contents
+/// are extracted from a memory buffer (byte array) as opposed
+/// to a jar file.
+jar_filet::jar_filet(
+  java_class_loader_limitt &limit,
+  const std::string &filename):
+  m_zip_archive(filename)
+{
+  initialize_file_index(limit);
+}
+
+/// This constructor creates a jar_file object whose contents
+/// are extracted from a memory buffer (byte array) as opposed
+/// to a jar file.
+jar_filet::jar_filet(
+  java_class_loader_limitt &limit,
+  const void *data,
+  size_t size):
+  m_zip_archive(data, size)
+{
+  initialize_file_index(limit);
+}
+
 // VS: No default move constructors or assigns
 
 jar_filet::jar_filet(jar_filet &&other):

src/java_bytecode/jar_file.h

@@ -21,16 +21,25 @@ class java_class_loader_limitt;
 class jar_filet final
 {
 public:
-  /// Open java file for reading
+  /// Open java file for reading.
   /// \param limit Object limiting number of loaded .class files
   /// \param filename Name of the file
   /// \throw Throws std::runtime_error if file cannot be opened
   jar_filet(java_class_loader_limitt &limit, const std::string &filename);
+
+  /// Open a JAR file of size \p size loaded in memory at address \p data.
+  /// \param limit Object limiting number of loaded .class files
+  /// \param data memory buffer with the contents of the jar file
+  /// \param size size  of the memory buffer
+  /// \throw Throws std::runtime_error if file cannot be opened
+  jar_filet(java_class_loader_limitt &limit, const void *data, size_t size);
+
   jar_filet(const jar_filet &)=delete;
   jar_filet &operator=(const jar_filet &)=delete;
   jar_filet(jar_filet &&);
   jar_filet &operator=(jar_filet &&);
   ~jar_filet()=default;
+
   /// Get contents of a file in the jar archive.
   /// Terminates the program if file doesn't exist
   /// \param filename Name of the file in the archive
@@ -40,8 +49,12 @@ class jar_filet final
   /// Get list of filenames in the archive
   std::vector<std::string> filenames() const;
 private:
+  /// Loads the fileindex (m_name_to_index) with a map of loaded files to
+  /// indices.
+  void initialize_file_index(java_class_loader_limitt &limit);
+
   mz_zip_archivet m_zip_archive;
-  /// Map of filename to the file index in the zip archive
+  /// Map of filename to the file index in the zip archive.
   std::unordered_map<std::string, size_t> m_name_to_index;
 };
 

src/java_bytecode/java_bytecode_language.cpp

@@ -42,6 +42,7 @@ Author: Daniel Kroening, [email protected]
 void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
 {
   assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
+  java_class_loader.use_core_models=!cmd.isset("no-core-models");
   string_refinement_enabled=cmd.isset("refine-strings");
   throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions");
   if(cmd.isset("java-max-input-array-length"))
@@ -267,6 +268,24 @@ bool java_bytecode_languaget::typecheck(
   if(string_refinement_enabled)
     string_preprocess.initialize_conversion_table();
 
+  // Must load java.lang.Object first to avoid stubbing
+  // This ordering could alternatively be enforced by
+  // moving the code below to the class loader.
+  java_class_loadert::class_mapt::const_iterator it=
+    java_class_loader.class_map.find("java.lang.Object");
+  if(it!=java_class_loader.class_map.end())
+  {
+    if(java_bytecode_convert_class(
+     it->second,
+     symbol_table,
+     get_message_handler(),
+     max_user_array_length,
+     method_bytecode,
+     lazy_methods_mode,
+     string_preprocess))
+       return true;
+  }
+
   // first generate a new struct symbol for each class and a new function symbol
   // for every method
   for(java_class_loadert::class_mapt::const_iterator

src/java_bytecode/java_bytecode_language.h

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/select_pointer_type.h>
 
 #define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/                              \
+  "(no-core-models)"                                                           \
   "(java-assume-inputs-non-null)"                                              \
   "(java-throw-runtime-exceptions)"                                            \
   "(java-max-input-array-length):"                                             \
@@ -35,19 +36,21 @@ Author: Daniel Kroening, [email protected]
   "(java-load-class):"
 
 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/                                          \
-  " --java-assume-inputs-non-null    never initialize reference-typed parameter to the\n"       \
-  "                                  entry point with null\n"                                   \
-  " --java-throw-runtime-exceptions  make implicit runtime exceptions explicit\n"               \
-  " --java-max-input-array-length N  limit input array size to <= N\n"                          \
-  " --java-max-input-tree-depth N    object references are (deterministically) set to null in\n"\
-  "                                  the object\n"                                              \
-  " --java-max-vla-length            limit the length of user-code-created arrays\n"            \
-  " --java-cp-include-files          regexp or JSON list of files to load (with '@' prefix)\n"  \
-  " --lazy-methods                   only translate methods that appear to be reachable from\n" \
-  "                                  the --function entry point or main class\n"                \
-  " --lazy-methods-extra-entry-point METHODNAME\n"                                              \
-  "                                  treat METHODNAME as a possible program entry point for\n"  \
-  "                                  the purpose of lazy method loading\n"                      \
+  " --no-core-models                 don't load internally provided models for core classes in\n"/* NOLINT(*) */ \
+  "                                  the Java Class Library\n"                                   /* NOLINT(*) */ \
+  " --java-assume-inputs-non-null    never initialize reference-typed parameter to the\n"        /* NOLINT(*) */ \
+  "                                  entry point with null\n"                                    /* NOLINT(*) */ \
+  " --java-throw-runtime-exceptions  make implicit runtime exceptions explicit\n"                /* NOLINT(*) */ \
+  " --java-max-input-array-length N  limit input array size to <= N\n"                           /* NOLINT(*) */ \
+  " --java-max-input-tree-depth N    object references are (deterministically) set to null in\n" /* NOLINT(*) */ \
+  "                                  the object\n"                                               /* NOLINT(*) */ \
+  " --java-max-vla-length            limit the length of user-code-created arrays\n"             /* NOLINT(*) */ \
+  " --java-cp-include-files          regexp or JSON list of files to load (with '@' prefix)\n"   /* NOLINT(*) */ \
+  " --lazy-methods                   only translate methods that appear to be reachable from\n"  /* NOLINT(*) */ \
+  "                                  the --function entry point or main class\n"                 /* NOLINT(*) */ \
+  " --lazy-methods-extra-entry-point METHODNAME\n"                                               /* NOLINT(*) */ \
+  "                                  treat METHODNAME as a possible program entry point for\n"   /* NOLINT(*) */ \
+  "                                  the purpose of lazy method loading\n"                       /* NOLINT(*) */ \
   "                                  A '.*' wildcard is allowed to specify all class members\n"
 
 #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5