Internalize core models of the Java Class Library

dcattaruzza · Degiorgio · commit f66288b40452 · 2018-01-29T13:45:22.000Z
The 'core models' is a set of .class files that model core classes from the Java
Class Library, such as java.lang.Object or java.lang.Thread. A minimum is
necessary for CBMC to understand, e.g., when a new thread is created. These core
classes live in `src/java_bytecode/library`.

This commit adds support to compile and pack the core classes into a single jar
file, core-models.jar, and a converter program that transforms that .jar file
into a C-language array of data that can then be linked into CBMC, thus making
the .jar file be present in the data segment of the CBMC ELF.

Other modifications:
- New option --no-core-models, allowing to disable the loading of the internal
  core models
- make and cmake now compile the core models into a single core-models.jar
- Add regression one regression tests ensuring the the core-models.jar is loaded
  by default
diff --git a/.gitignore b/.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/
diff --git a/regression/cbmc-java/coreModels/test.class b/regression/cbmc-java/coreModels/test.class
diff --git a/regression/cbmc-java/coreModels/test.desc b/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
diff --git a/regression/cbmc-java/coreModels/test.java b/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);
+  }
+}
+
diff --git a/regression/jbmc-strings/java_append_char/test.desc b/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$
diff --git a/src/java_bytecode/CMakeLists.txt b/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)
 
diff --git a/src/java_bytecode/Makefile b/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)
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
@@ -42,6 +42,7 @@ Author: Daniel Kroening, kroening@kroening.com
 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
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
@@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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, kroening@kroening.com
   "(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
diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp
@@ -19,6 +19,15 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_bytecode_parser.h"
 #include "jar_file.h"
 
+#include "library/java_core_models.inc"
+
+/// This variable stores the data of the file core-models.jar. The macro
+/// JAVA_CORE_MODELS_SIZE is defined in the header java_core_models.inc, which
+/// gets generated at compile time by running a small utility (converter.cpp) on
+/// actual .jar file. The number of bytes in the variable is
+/// JAVA_CORE_MODELS_SIZE, another macro defined in java_core_models.inc.
+unsigned char java_core_models[] = { JAVA_CORE_MODELS_DATA };
+
 java_bytecode_parse_treet &java_class_loadert::operator()(
   const irep_idt &class_name)
 {
@@ -105,6 +114,26 @@ bool java_class_loadert::get_class_file(
   return false;
 }
 
+/// Retrieves a class file from the internal jar and loads it into the tree
+bool java_class_loadert::get_internal_class_file(
+  java_class_loader_limitt &class_loader_limit,
+  const irep_idt &class_name,
+  java_bytecode_parse_treet &parse_tree)
+{
+  // Add internal jar file. The name is used to load it once only and
+  // reference it later.
+  std::string core_models="core-models.jar";
+  jar_pool(class_loader_limit,
+           core_models,
+           java_core_models,
+           JAVA_CORE_MODELS_SIZE);
+
+  // This does not read from the jar file but from the jar_filet object
+  // as we've just created it
+  read_jar_file(class_loader_limit, core_models);
+  return
+    get_class_file(class_loader_limit, class_name, core_models, parse_tree);
+}
 
 java_bytecode_parse_treet &java_class_loadert::get_parse_tree(
   java_class_loader_limitt &class_loader_limit,
@@ -120,6 +149,12 @@ java_bytecode_parse_treet &java_class_loadert::get_parse_tree(
       return parse_tree;
   }
 
+  if(use_core_models)
+  {
+    if(get_internal_class_file(class_loader_limit, class_name, parse_tree))
+      return parse_tree;
+  }
+
   // See if we can find it in the class path
   for(const auto &cp : config.java.classpath)
   {
@@ -283,3 +318,20 @@ void java_class_loadert::add_load_classes(const std::vector<irep_idt> &classes)
   for(const auto &id : classes)
     java_load_classes.push_back(id);
 }
+
+jar_filet &java_class_loadert::jar_pool(
+  java_class_loader_limitt &class_loader_limit,
+  const std::string &buffer_name,
+  const void *pmem,
+  size_t size)
+{
+  const auto it=m_archives.find(buffer_name);
+  if(it==m_archives.end())
+  {
+    // VS: Can't construct in place
+    auto file=jar_filet(class_loader_limit, pmem, size);
+    return m_archives.emplace(buffer_name, std::move(file)).first->second;
+  }
+  else
+    return it->second;
+}
diff --git a/src/java_bytecode/java_class_loader.h b/src/java_bytecode/java_class_loader.h
@@ -23,6 +23,12 @@ Author: Daniel Kroening, kroening@kroening.com
 class java_class_loadert:public messaget
 {
 public:
+  // Default constructor does not use core models
+  // for backward compatibility of unit tests
+  java_class_loadert() :
+    use_core_models(true)
+  {}
+
   java_bytecode_parse_treet &operator()(const irep_idt &);
 
   void set_java_cp_include_files(std::string &);
@@ -48,6 +54,13 @@ class java_class_loadert:public messaget
     const std::string &jar_file,
     java_bytecode_parse_treet &parse_tree);
 
+  /// Attempts to load the class from the internal core models.
+  /// Returns true if found and loaded
+  bool get_internal_class_file(
+    java_class_loader_limitt &class_loader_limit,
+    const irep_idt &class_name,
+    java_bytecode_parse_treet &parse_tree);
+
   /// Given a \p class_name (e.g. "java.lang.Thread") try to load the
   /// corresponding .class file by first scanning all .jar files whose
   /// pathname is stored in \ref jar_files, and if that doesn't work, then scan
@@ -68,6 +81,18 @@ class java_class_loadert:public messaget
   jar_filet &jar_pool(java_class_loader_limitt &limit,
                       const std::string &filename);
 
+  /// Load jar archive(from cache if already loaded)
+  /// \param limit
+  /// \param buffer_name name of the original file
+  /// \param pmem memory pointer to the contents of the file
+  /// \param size size of the memory buffer
+  /// Note that this mocks the existence of a file which may
+  /// or may not exist since  the actual data bis retrieved from memory.
+  jar_filet &jar_pool(java_class_loader_limitt &limit,
+                      const std::string &buffer_name,
+                      const void *pmem,
+                      size_t size);
+
   /// An object of this class represents the information of _a single JAR file_
   /// that is relevant for a class loader: a map associating logical class names
   /// with with handles (struct entryt) that describe one .class file inside the
@@ -101,6 +126,10 @@ class java_class_loadert:public messaget
   /// java_class_loader_limitt::setup_class_load_limit() for further
   /// information.
   std::string java_cp_include_files;
+
+  /// Indicates that the core models should be loaded
+  bool use_core_models;
+
 private:
   std::map<std::string, jar_filet> m_archives;
   std::vector<irep_idt> java_load_classes;
diff --git a/src/java_bytecode/library/CMakeLists.txt b/src/java_bytecode/library/CMakeLists.txt
@@ -0,0 +1,19 @@
+find_package(Java REQUIRED)
+include(UseJava)
+set(CMAKE_JAVA_COMPILE_FLAGS -sourcepath "src" -d "classes" -XDignore.symbol.file)
+file(GLOB_RECURSE java_sources "*.java")
+set(JAR_NAME "core-models")
+add_jar(${JAR_NAME} ${java_sources})
+get_filename_component(CORE_MODELS_JAR "core-models.jar" REALPATH BASE_DIR ${CMAKE_CURRENT_SOURCE_DIR})
+get_filename_component(JAVA_CORE_MODELS_INC "java_core_models.inc" REALPATH BASE_DIR ${CMAKE_CURRENT_SOURCE_DIR})
+file(GLOB_RECURSE jars "*.jar")
+add_executable(java-converter converter.cpp)
+
+add_custom_target(core_models_files)
+add_dependencies(core_models_files ${JAR_NAME})
+add_custom_command(TARGET core_models_files
+                   PRE_BUILD
+                   COMMAND java-converter JAVA_CORE_MODELS core-models.jar > ${JAVA_CORE_MODELS_INC}
+                   )
+
+set_source_files_properties("java_core_models.inc" GENERATED)
diff --git a/src/java_bytecode/library/Makefile b/src/java_bytecode/library/Makefile
@@ -1,26 +1,50 @@
-all: org.cprover.jar
+.NOTPARALLEL:
+#javac compiles multiple classes for each source as it will compile dependent sources.
+#Thus we do not allow the make to run concurrently.
+
+SRC = converter.cpp
+
+include ../../config.inc
+include ../../common
 
 SOURCE_DIR := src
 BINARY_DIR := classes
 
 FIND := find
 
 JAVAC := javac
-JFLAGS := -sourcepath $(SOURCE_DIR) -d $(BINARY_DIR)
+JFLAGS := -sourcepath $(SOURCE_DIR) -d $(BINARY_DIR) -XDignore.symbol.file
 
 CLASSPATH := SOURCE_DIR
 
-all_javas := $(shell $(FIND) $(SOURCE_DIR) -name '*.java')
+ALL_JAVAS := $(wildcard $(SOURCE_DIR)/*/*.java $(SOURCE_DIR)/*/*/*.java $(SOURCE_DIR)/*/*/*/*.java)
+ALL_CLASSES := $(patsubst $(SOURCE_DIR)/%.java,$(BINARY_DIR)/%.class,$(ALL_JAVAS))
 
 $(BINARY_DIR):
 	mkdir -p $(BINARY_DIR)
 
-.PHONY: compile
-compile: $(BINARY_DIR)
-	$(JAVAC) $(JFLAGS) $(all_javas)
+.SUFFIXES: .java .class
+
+$(BINARY_DIR)/%.class: $(SOURCE_DIR)/%.java $(BINARY_DIR)
+	$(JAVAC) $(JFLAGS) $(patsubst $(BINARY_DIR)/%.class,$(SOURCE_DIR)/%.java,$@)
 
 JAR := jar
 JARFLAGS := -cf
 
-org.cprover.jar: compile
-	$(JAR) $(JARFLAGS) $@ -C $(BINARY_DIR) org
+core-models.jar: $(ALL_CLASSES)
+	$(JAR) $(JARFLAGS) $@ -C $(BINARY_DIR) .
+
+CLEANFILES = core-models.jar converter$(EXEEXT) java_core_models.inc
+
+all: java_core_models.inc
+
+clean: clean_
+
+clean_:
+	$(RM) -Rf $(BINARY_DIR)
+
+converter$(EXEEXT): converter.cpp
+	$(LINKNATIVE)
+
+java_core_models.inc: converter$(EXEEXT) core-models.jar
+	./converter$(EXEEXT) JAVA_CORE_MODELS core-models.jar > $@
diff --git a/src/java_bytecode/library/converter.cpp b/src/java_bytecode/library/converter.cpp
